diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /plugins/cc | |
parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'plugins/cc')
-rw-r--r-- | plugins/cc/ccalgo.ml | 25 | ||||
-rw-r--r-- | plugins/cc/cctac.ml | 34 |
2 files changed, 46 insertions, 13 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 (_,_) -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b7358121..ca1a9085 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: cctac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *) (* This file is the interface between the c-c algorithm and Coq *) @@ -74,11 +74,21 @@ let rec decompose_term env sigma t= decompose_term env sigma a), decompose_term env sigma b) | Construct c-> - let (oib,_)=Global.lookup_inductive (fst c) in - let nargs=mis_constructor_nargs_env env c in - Constructor {ci_constr=c; + let (mind,i_ind),i_con = c in + let canon_mind = mind_of_kn (canonical_mind mind) in + let canon_ind = canon_mind,i_ind in + let (oib,_)=Global.lookup_inductive (canon_ind) in + let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in + Constructor {ci_constr= (canon_ind,i_con); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} + | Ind c -> + let mind,i_ind = c in + let canon_mind = mind_of_kn (canonical_mind mind) in + let canon_ind = canon_mind,i_ind in (Symb (mkInd canon_ind)) + | Const c -> + let canon_const = constant_of_kn (canonical_con c) in + (Symb (mkConst canon_const)) | _ ->if closed0 t then (Symb t) else raise Not_found (* decompose equality in members and type *) @@ -106,7 +116,7 @@ let rec pattern_of_constr env sigma c = | Prod (_,a,_b) when not (dependent (mkRel 1) _b) -> let b =pop _b in let pa,sa = pattern_of_constr env sigma a in - let pb,sb = pattern_of_constr env sigma (pop b) in + let pb,sb = pattern_of_constr env sigma b in let sort_b = sf_of env sigma b in let sort_a = sf_of env sigma a in PApp(Product (sort_a,sort_b), @@ -143,27 +153,27 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match kind_of_term (whd_delta env term) with - Prod (_,atom,ff) -> + Prod (id,atom,ff) -> if eq_constr ff (Lazy.force _False) then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts - else - quantified_atom_of_constr env sigma (succ nrels) ff - | _ -> + else + quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma (succ nrels) ff + | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts let litteral_of_constr env sigma term= match kind_of_term (whd_delta env term) with - | Prod (_,atom,ff) -> + | Prod (id,atom,ff) -> if eq_constr ff (Lazy.force _False) then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) else begin - try - quantified_atom_of_constr env sigma 1 ff + try + quantified_atom_of_constr (Environ.push_rel (id,None,atom) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end |