oblivion ugraph everywhere outside the kernel

[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..53bfc39a9cf0e236a0a1bc1d5159ea0fb105571e 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
@@ -136,7 +136,7 @@ let eta_expand metasenv context t arg =
    List.map (function uri,t -> uri,aux n t)
   in
    let argty,_ = 
-    T.type_of_aux' metasenv context arg CicUniv.empty_ugraph (* TASSI: FIXME *)
+    T.type_of_aux' metasenv context arg CicUniv.oblivion_ugraph (* TASSI: FIXME *)
    in
     let fresh_name =
      FreshNamesGenerator.mk_fresh_name ~subst:[]
@@ -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 []
@@ -184,7 +182,7 @@ let
 =
  let module C = Cic in
   let params =
-    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
     CicUtil.params_of_obj o
   in
    let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
@@ -196,7 +194,7 @@ let
          [],[] -> []
        | uri::tl,[] ->
           let ty =
-            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+            let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
               match o with
                   C.Variable (_,_,ty,_,_) ->
                     CicSubstitution.subst_vars !exp_named_subst_diff ty
@@ -244,7 +242,7 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termt
     goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif_subst 
-     subst context newmetasenv consthead ty CicUniv.empty_ugraph
+     subst context newmetasenv consthead ty CicUniv.oblivion_ugraph
   in
   let t = 
     if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
@@ -298,7 +296,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
    in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty in
@@ -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'
@@ -445,18 +436,18 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
        (ProofEngineTypes.Fail (lazy
          "You can't letin a term containing the current goal"));
     let tty,_ =
-      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+      CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      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]
@@ -473,7 +464,7 @@ let exact_tac ~term =
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
-  let ty_term,u = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
   if b then
    begin
@@ -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
@@ -623,7 +614,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       | None, [], Some cpattern -> cpattern
       | _                       -> raise (PET.Fail (lazy "not implemented"))
    in    
-   let ugraph = CicUniv.empty_ugraph in
+   let ugraph = CicUniv.oblivion_ugraph in
    let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
    let conjecture = CicUtil.lookup_meta goal metasenv in
    let metano, context, ty = conjecture in 
@@ -730,7 +721,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
   let module C = Cic in
   let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let termty = CicReduction.whd context termty in
   let (termty,metasenv',arguments,fresh_meta) =
    TermUtil.saturate_term
@@ -744,7 +735,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     | _ -> raise NotAnInductiveTypeToEliminate
   in
   let paramsno,itty,patterns,right_args =
-    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
     | C.InductiveDefinition (tys,_,paramsno,_),_ ->
        let _,left_parameters,right_args = 
          List.fold_right 
@@ -833,7 +824,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
   let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
   let refined_term,_,metasenv'',_ = 
     CicRefine.type_of_aux' metasenv' context term_to_refine
-      CicUniv.empty_ugraph
+      CicUniv.oblivion_ugraph
   in
   let new_goals =
     ProofEngineHelpers.compare_metasenvs
@@ -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