Very experimental commit: the type of the source is now required in LetIns

[helm.git] / helm / software / components / tactics / proofEngineReduction.ml

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 68a2a0a3daf9bb335a74fa5a57a1b92489b5695e..3892ace35a14e49b9ad834b2f9de08ee5c93bc14 100644 (file)
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -86,7 +86,7 @@ let replace ~equality ~what ~with_what ~where =
      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
-     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+     | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t)
      | C.Appl l ->
         (* Invariant enforced: no application of an application *)
         (match List.map aux l with
@@ -139,7 +139,7 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
     find_image_aux (what,with_what)
   in
   let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
-  let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+  let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
   let rec substaux k ctx what t =
    try
     S.lift (k-1) (find_image ctx what t)
@@ -169,9 +169,9 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
     | C.Lambda (n,s,t) ->
        C.Lambda
         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
-    | C.LetIn (n,s,t) ->
+    | C.LetIn (n,s,ty,t) ->
        C.LetIn
-        (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+        (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k ctx what) tl in
@@ -268,8 +268,8 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
         C.Prod (n, substaux k s, substaux (k + 1) t)
      | C.Lambda (n,s,t) ->
         C.Lambda (n, substaux k s, substaux (k + 1) t)
-     | C.LetIn (n,s,t) ->
-        C.LetIn (n, substaux k s, substaux (k + 1) t)
+     | C.LetIn (n,s,ty,t) ->
+        C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
      | C.Appl (he::tl) ->
         (* Invariant: no Appl applied to another Appl *)
         let tl' = List.map (substaux k) tl in
@@ -358,8 +358,8 @@ let replace_with_rel_1_from ~equality ~what =
         C.Prod (n, subst_term k v, subst_term (succ k) t)
      | C.Lambda (n, v, t) ->
         C.Lambda (n, subst_term k v, subst_term (succ k) t)
-     | C.LetIn (n, v, t) ->
-        C.LetIn (n, subst_term k v, subst_term (succ k) t)
+     | C.LetIn (n, v, ty, t) ->
+        C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t)
      | C.Fix (i, fixes) ->
         let fixesno = List.length fixes in
         let fixes = List.map (subst_fix fixesno k) fixes in
@@ -543,7 +543,7 @@ let simpl context =
          | he::tl -> reduceaux context tl (S.subst he t)
            (* when name is Anonimous the substitution should be superfluous *)
        )
-    | C.LetIn (n,s,t) ->
+    | C.LetIn (n,s,ty,t) ->
        reduceaux context l (S.subst (reduceaux context [] s) t)
     | C.Appl (he::tl) ->
        let tl' = List.map (reduceaux context []) tl in
@@ -726,7 +726,7 @@ let simpl context =
                (* be superfluous                                 *)
                aux (he::rev_constant_args) tl (S.subst he t)
           end
-       | C.LetIn (_,s,t) ->
+       | C.LetIn (_,s,_,t) ->
           aux rev_constant_args l (S.subst s t)
        | C.Fix (i,fl) ->
            let (_,recindex,_,body) = List.nth fl i in
@@ -804,7 +804,7 @@ let simpl context =
                  (* when name is Anonimous the substitution should *)
                  (* be superfluous                                 *)
                  aux tl (S.subst he t))
-         | C.LetIn (_,s,t) -> aux l (S.subst s t)
+         | C.LetIn (_,s,_,t) -> aux l (S.subst s t)
          | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
              let recno =
                prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)