The type of a LetIn is now a LetIn if and only if the bound variable really

occurs.

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index 4afe0e47549d0e959d44442d23c98e78564b4d4e..71422ced12d6190d09b2829d2f80d1fcffaef6c5 100644 (file)
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -33,6 +33,62 @@ exception RelToHiddenHypothesis;;
 
 type types = {synthesized : Cic.term ; expected : Cic.term option};;
 
+(* does_not_occur n te                              *)
+(* returns [true] if [Rel n] does not occur in [te] *)
+let rec does_not_occur n =
+ let module C = Cic in
+  function
+     C.Rel m when m = n -> false
+   | C.Rel _
+   | C.Meta _
+   | C.Sort _
+   | C.Implicit -> true 
+   | C.Cast (te,ty) ->
+      does_not_occur n te && does_not_occur n ty
+   | C.Prod (name,so,dest) ->
+      does_not_occur n so &&
+       does_not_occur (n + 1) dest
+   | C.Lambda (name,so,dest) ->
+      does_not_occur n so &&
+       does_not_occur (n + 1) dest
+   | C.LetIn (name,so,dest) ->
+      does_not_occur n so &&
+       does_not_occur (n + 1) dest
+   | C.Appl l ->
+      List.fold_right (fun x i -> i && does_not_occur n x) l true
+   | C.Var (_,exp_named_subst)
+   | C.Const (_,exp_named_subst)
+   | C.MutInd (_,_,exp_named_subst)
+   | C.MutConstruct (_,_,_,exp_named_subst) ->
+      List.fold_right (fun (_,x) i -> i && does_not_occur n x)
+       exp_named_subst true
+   | C.MutCase (_,_,out,te,pl) ->
+      does_not_occur n out && does_not_occur n te &&
+       List.fold_right (fun x i -> i && does_not_occur n x) pl true
+   | C.Fix (_,fl) ->
+      let len = List.length fl in
+       let n_plus_len = n + len in
+       let tys =
+        List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+       in
+        List.fold_right
+         (fun (_,_,ty,bo) i ->
+           i && does_not_occur n ty &&
+           does_not_occur n_plus_len bo
+         ) fl true
+   | C.CoFix (_,fl) ->
+      let len = List.length fl in
+       let n_plus_len = n + len in
+       let tys =
+        List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
+       in
+        List.fold_right
+         (fun (_,ty,bo) i ->
+           i && does_not_occur n ty &&
+           does_not_occur n_plus_len bo
+         ) fl true
+;;
+
 (*CSC: potrebbe creare applicazioni di applicazioni *)
 (*CSC: ora non e' piu' head, ma completa!!! *)
 let rec head_beta_reduce =
@@ -356,8 +412,16 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
 (*CSC: target of a LetIn? None used.                        *)
         (* Let's visit all the subterms that will not be visited later *)
         let _ = type_of_aux context s None in
-         (* Checks suppressed *)
-         C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
+         let t_typ =
+          (* Checks suppressed *)
+          type_of_aux ((Some (n,(C.Def s)))::context) t None
+         in
+          if does_not_occur 1 t_typ then
+           (* since [Rel 1] does not occur in typ, substituting any term *)
+           (* in place of [Rel 1] is equivalent to delifting once        *)
+           CicSubstitution.subst C.Implicit t_typ
+          else
+           C.LetIn (n,s,t_typ)
      | C.Appl (he::tl) when List.length tl > 0 ->
         let expected_hetype =
          (* Inefficient, the head is computed twice. But I know *)