From 4f171cba0be2e0543cf49b221ee22b553305488a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 27 Jun 2003 17:18:18 +0000
Subject: [PATCH] The type of a LetIn is now a LetIn if and only if the bound
 variable really occurs.

---
 helm/gTopLevel/doubleTypeInference.ml | 68 ++++++++++++++++++++++++++-
 1 file changed, 66 insertions(+), 2 deletions(-)

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index 4afe0e475..71422ced1 100644
--- 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 *)
-- 
2.39.2