From: Claudio Sacerdoti Coen Date: Thu, 5 Feb 2004 12:29:49 +0000 (+0000) Subject: dummy dependent types and dummy letins are now removed from the refined X-Git-Tag: V_0_2_3~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d8a1a68b8b7e53ba43fcad55e928a99ef5e08b8e;p=helm.git dummy dependent types and dummy letins are now removed from the refined term. --- diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test index 1665098f7..8391ea568 100644 --- a/helm/gTopLevel/tests/forall00.cic.test +++ b/helm/gTopLevel/tests/forall00.cic.test @@ -2,8 +2,8 @@ ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) -(n:nat)(m:nat)(eq nat (plus n m) n) +(n:nat)(nat->(eq nat (plus n __1) n)) ### (* TYPE_OF the disambiguated term *) Prop ### (* REDUCED disambiguated term *) -(n:nat)(m:nat)(eq nat (plus n m) n) +(n:nat)(nat->(eq nat (plus n __1) n)) diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test index ee8c6b118..fde5288f9 100644 --- a/helm/gTopLevel/tests/lambda02.cic.test +++ b/helm/gTopLevel/tests/lambda02.cic.test @@ -2,8 +2,8 @@ ### (* METASENV after disambiguation *) ### (* TERM after disambiguation *) -[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O)) +[f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O)) ### (* TYPE_OF the disambiguated term *) -(f:(n:nat)(H:(le O n))(eq nat n n))(eq nat O O) +(f:(n:nat)((le O n)->(eq nat n n)))(eq nat O O) ### (* REDUCED disambiguated term *) -[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O)) +[f:(n:nat)((le O n)->(eq nat n n))](f O (le_n O)) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 060d2bd1f..85c171b14 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -511,7 +511,14 @@ and type_of_aux' metasenv context t = context) in let newmeta = Cic.Meta (idx, irl) in - let prod = Cic.Prod (Cic.Anonymous, argty, newmeta) in + let prod = + Cic.Prod + (FreshNamesGenerator.mk_fresh_name + (CicMetaSubst.apply_subst_metasenv subst metasenv) + (CicMetaSubst.apply_subst_context subst context) + Cic.Anonymous + (CicMetaSubst.apply_subst subst argty), + argty, newmeta) in let (_, subst, metasenv) = type_of_aux subst metasenv context prod in let (subst, metasenv) = CicUnification.fo_unif_subst subst context metasenv resty prod @@ -525,8 +532,10 @@ and type_of_aux' metasenv context t = let ty,subst',metasenv' = type_of_aux [] metasenv context t in - (CicMetaSubst.apply_subst subst' t, - CicMetaSubst.apply_subst subst' ty, + (FreshNamesGenerator.clean_dummy_dependent_types + (CicMetaSubst.apply_subst subst' t), + FreshNamesGenerator.clean_dummy_dependent_types + (CicMetaSubst.apply_subst subst' ty), CicMetaSubst.apply_subst_metasenv subst' metasenv') ;; diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.ml b/helm/ocaml/cic_unification/freshNamesGenerator.ml index 3f4d777c9..3664b4a72 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.ml +++ b/helm/ocaml/cic_unification/freshNamesGenerator.ml @@ -60,3 +60,139 @@ let mk_fresh_name metasenv context name ~typ = in try_next 1 ;; + +(* clean_dummy_dependent_types term *) +(* returns a copy of [term] where every dummy dependent product *) +(* have been replaced with a non-dependent product and where *) +(* dummy let-ins have been removed. *) +let clean_dummy_dependent_types t = + let module C = Cic in + let rec aux k = + function + C.Rel m as t -> t,[m - k] + | C.Var (uri,exp_named_subst) -> + let exp_named_subst',rels = + List.fold_right + (fun (uri,t) (exp_named_subst,rels) -> + let t',rels' = aux k t in + (uri,t')::exp_named_subst, rels' @ rels + ) exp_named_subst ([],[]) + in + C.Var (uri,exp_named_subst'),rels + | C.Meta (i,l) -> + let l',rels = + List.fold_right + (fun t (l,rels) -> + let t',rels' = + match t with + None -> None,[] + | Some t -> + let t',rels' = aux k t in + Some t', rels' + in + t'::l, rels' @ rels + ) l ([],[]) + in + C.Meta(i,l'),rels + | C.Sort _ as t -> t,[] + | C.Implicit as t -> t,[] + | C.Cast (te,ty) -> + let te',rels1 = aux k te in + let ty',rels2 = aux k ty in + C.Cast (te', ty'), rels1@rels2 + | C.Prod (n,s,t) -> + let s',rels1 = aux k s in + let t',rels2 = aux (k+1) t in + let n' = + match n with + C.Anonymous -> + if List.mem k rels2 then assert false else C.Anonymous + | C.Name _ as n -> + if List.mem k rels2 then n else C.Anonymous + in + C.Prod (n', s', t'), rels1@rels2 + | C.Lambda (n,s,t) -> + let s',rels1 = aux k s in + let t',rels2 = aux (k+1) t in + C.Lambda (n, s', t'), rels1@rels2 + | C.LetIn (n,s,t) -> + let s',rels1 = aux k s in + let t',rels2 = aux (k+1) t in + let rels = rels1 @ rels2 in + if List.mem k rels2 then + C.LetIn (n, s', t'), rels + else + (* (C.Rel 1) is just a dummy term; any term would fit *) + CicSubstitution.subst (C.Rel 1) t', rels + | C.Appl l -> + let l',rels = + List.fold_right + (fun t (exp_named_subst,rels) -> + let t',rels' = aux k t in + t'::exp_named_subst, rels' @ rels + ) l ([],[]) + in + C.Appl l', rels + | C.Const (uri,exp_named_subst) -> + let exp_named_subst',rels = + List.fold_right + (fun (uri,t) (exp_named_subst,rels) -> + let t',rels' = aux k t in + (uri,t')::exp_named_subst, rels' @ rels + ) exp_named_subst ([],[]) + in + C.Const (uri,exp_named_subst'),rels + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst',rels = + List.fold_right + (fun (uri,t) (exp_named_subst,rels) -> + let t',rels' = aux k t in + (uri,t')::exp_named_subst, rels' @ rels + ) exp_named_subst ([],[]) + in + C.MutInd (uri,tyno,exp_named_subst'),rels + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst',rels = + List.fold_right + (fun (uri,t) (exp_named_subst,rels) -> + let t',rels' = aux k t in + (uri,t')::exp_named_subst, rels' @ rels + ) exp_named_subst ([],[]) + in + C.MutConstruct (uri,tyno,consno,exp_named_subst'),rels + | C.MutCase (sp,i,outty,t,pl) -> + let outty',rels1 = aux k outty in + let t',rels2 = aux k t in + let pl',rels3 = + List.fold_right + (fun t (exp_named_subst,rels) -> + let t',rels' = aux k t in + t'::exp_named_subst, rels' @ rels + ) pl ([],[]) + in + C.MutCase (sp, i, outty', t', pl'), rels1 @ rels2 @rels3 + | C.Fix (i, fl) -> + let len = List.length fl in + let fl',rels = + List.fold_right + (fun (name,i,ty,bo) (fl,rels) -> + let ty',rels1 = aux k ty in + let bo',rels2 = aux (k + len) bo in + (name,i,ty',bo')::fl, rels1 @ rels2 @ rels + ) fl ([],[]) + in + C.Fix (i, fl'),rels + | C.CoFix (i, fl) -> + let len = List.length fl in + let fl',rels = + List.fold_right + (fun (name,ty,bo) (fl,rels) -> + let ty',rels1 = aux k ty in + let bo',rels2 = aux (k + len) bo in + (name,ty',bo')::fl, rels1 @ rels2 @ rels + ) fl ([],[]) + in + C.CoFix (i, fl'),rels + in + fst (aux 0 t) +;; diff --git a/helm/ocaml/cic_unification/freshNamesGenerator.mli b/helm/ocaml/cic_unification/freshNamesGenerator.mli index 371ca99fa..02acf9b03 100644 --- a/helm/ocaml/cic_unification/freshNamesGenerator.mli +++ b/helm/ocaml/cic_unification/freshNamesGenerator.mli @@ -29,3 +29,9 @@ (* [typ] will be the type of the variable *) val mk_fresh_name : Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + +(* clean_dummy_dependent_types term *) +(* returns a copy of [term] where every dummy dependent product *) +(* have been replaced with a non-dependent product and where *) +(* dummy let-ins have been removed. *) +val clean_dummy_dependent_types : Cic.term -> Cic.term