Module Kernel.AcSource

Sourcetype ac_ident = Basic.name * Term.algebra
Sourceval ac_ident_eq : ac_ident -> ac_ident -> bool
Sourceval pp_ac_ident : ac_ident Basic.printer
Sourceval force_flatten_AC_term : (Term.term -> Term.term) -> (Term.term -> Term.term -> bool) -> ac_ident -> Term.term -> Term.term list

force_flatten_AC_term snf are_convertible aci t returns the list t1 ; ... ; tn where t is convertible with t1 + ... + tn and aci represents the AC(U) operator + while whnf is used to reduce to head normal form to check for + symbol at the head. All ti are reduced with whnf. are_convertible checks convertibility to neutral element if needed.

Sourceval flatten_AC_terms : Basic.name -> Term.term list -> Term.term list
Sourceval flatten_AC_term : Basic.name -> Term.term -> Term.term list
Sourceval unflatten_AC : ac_ident -> Term.term list -> Term.term