graph generation phase fixed

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

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index 2447fe1ef64d7c10e9ab70d80da9da79d92588f0..e7632ebf4bf40c4bad2678b5ea23916b9e899796 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -62,11 +62,11 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
            collect_context ctx (howmany - 1) do_whd t 
           in
            (context',ty,C.Lambda(n',s,bo))
-      | C.LetIn (n,s,t) ->
+      | C.LetIn (n,s,sty,t) ->
          let (context',ty,bo) =
-          collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t
+          collect_context ((Some (n,(C.Def (s,sty))))::context) (howmany - 1) do_whd t
          in
-          (context',ty,C.LetIn(n,s,bo))
+          (context',ty,C.LetIn(n,s,sty,bo))
       | _ as t ->
         if howmany <= 0 then
          let irl =
@@ -102,7 +102,7 @@ let eta_expand metasenv context t arg =
     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
-    | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
+    | C.LetIn (nn,s,ty,t) -> C.LetIn (nn, aux n s, aux n ty, aux (n+1) t)
     | C.Appl l -> C.Appl (List.map (aux n) l)
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
@@ -159,15 +159,13 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
            match entry with
               Some (n,Cic.Decl s) ->
                Some (n,Cic.Decl (subst_in canonical_context' s))
-            | Some (n,Cic.Def (s,None)) ->
-               Some (n,Cic.Def ((subst_in canonical_context' s),None))
             | None -> None
-            | Some (n,Cic.Def (bo,Some ty)) ->
+            | Some (n,Cic.Def (bo,ty)) ->
                Some
                 (n,
                   Cic.Def
                    (subst_in canonical_context' bo,
-                    Some (subst_in canonical_context' ty)))
+                    subst_in canonical_context' ty))
           in
            entry'::canonical_context'
         ) canonical_context []
@@ -409,15 +407,8 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
       CicMkImplicit.identity_relocation_list_for_metavariable context
     in
      let newmeta1ty = CicSubstitution.lift 1 ty in
-(* This is the pre-letin implementation
-     let bo' =
-      C.Appl
-       [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
-        C.Meta (newmeta2,irl2)]
-     in
-*)
       let bo' = 
-        Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), C.Meta (newmeta1,irl1))
+        Cic.LetIn (fresh_name, C.Meta (newmeta2,irl2), term, C.Meta (newmeta1,irl1))
       in
       let (newproof, _) =
        ProofEngineHelpers.subst_meta_in_proof proof metano bo'
@@ -450,13 +441,13 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
      let fresh_name =
       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
      let context_for_newmeta =
-      (Some (fresh_name,C.Def (term,Some tty)))::context in
+      (Some (fresh_name,C.Def (term,tty)))::context in
      let irl =
       CicMkImplicit.identity_relocation_list_for_metavariable
        context_for_newmeta
      in
       let newmetaty = CicSubstitution.lift 1 ty in
-      let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
+      let bo' = C.LetIn (fresh_name,term,tty,C.Meta (newmeta,irl)) in
        let (newproof, _) =
          ProofEngineHelpers.subst_meta_in_proof
            proof metano bo'[newmeta,context_for_newmeta,newmetaty]
@@ -602,9 +593,9 @@ let beta_after_elim_tac upto predicate =
             | C.Lambda (_, s, t) ->
                let s, t = gen_term k s, gen_term (succ k) t in
                if is_meta [s; t] then meta else C.Lambda (anon, s, t)
-            | C.LetIn (_, s, t) -> 
-               let s, t = gen_term k s, gen_term (succ k) t in
-               if is_meta [s; t] then meta else C.LetIn (anon, s, t)
+            | C.LetIn (_, s, ty, t) -> 
+               let s,ty,t = gen_term k s, gen_term k ty, gen_term (succ k) t in
+               if is_meta [s; t] then meta else C.LetIn (anon, s, ty, t)
             | C.Fix (i, fl) -> C.Fix (i, List.map (gen_fix (List.length fl) k) fl)
             | C.CoFix (i, fl) -> C.CoFix (i, List.map (gen_cofix (List.length fl) k) fl)
          in
@@ -873,22 +864,3 @@ let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fres
        [ReductionTactics.simpl_tac
          ~pattern:(ProofEngineTypes.conclusion_pattern None)])
 ;;
-
-(* FG: insetrts a "hole" in the context (derived from letin_tac) *)
-
-let letout_tac =
-   let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
-   let term = C.Sort C.Set in
-   let letout_tac (proof, goal) =
-      let curi, metasenv, _subst, pbo, pty, attrs = proof in
-      let metano, context, ty = CicUtil.lookup_meta goal metasenv in
-      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
-      let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
-      let context_for_newmeta = None :: context in
-      let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
-      let newmetaty = CicSubstitution.lift 1 ty in
-      let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
-      let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
-      newproof, [newmeta]
-   in
-   PET.mk_tactic letout_tac