diff options
Diffstat (limited to 'plugins/cc/ccalgo.ml')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4171aceb..82b4143e 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ccalgo.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: ccalgo.ml 13409 2010-09-13 07:53:13Z soubiran $ *) (* This file implements the basic congruence-closure algorithm by *) (* Downey,Sethi and Tarjan. *) @@ -339,6 +339,28 @@ and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 | other -> applistc (constr_of_term other) l +let rec canonize_name c = + let func = canonize_name in + match kind_of_term c with + | Const kn -> + let canon_const = constant_of_kn (canonical_con kn) in + (mkConst canon_const) + | Ind (kn,i) -> + let canon_mind = mind_of_kn (canonical_mind kn) in + (mkInd (canon_mind,i)) + | Construct ((kn,i),j) -> + let canon_mind = mind_of_kn (canonical_mind kn) in + mkConstruct ((canon_mind,i),j) + | Prod (na,t,ct) -> + mkProd (na,func t, func ct) + | Lambda (na,t,ct) -> + mkLambda (na, func t,func ct) + | LetIn (na,b,t,ct) -> + mkLetIn (na, func b,func t,func ct) + | App (ct,l) -> + mkApp (func ct,array_smartmap func l) + | _ -> c + (* rebuild a term from a pattern and a substitution *) let build_subst uf subst = @@ -366,6 +388,7 @@ let rec add_term state t= Not_found -> let b=next uf in let typ = pf_type_of state.gls (constr_of_term t) in + let typ = canonize_name typ in let new_node= match t with Symb _ | Product (_,_) -> |