From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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