This is only a temporary patch. The typecheker raises a

[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 e09f0a1f7dc890ecbee234b53042677fea3aab91..b016eb85f6141cc7445bb75dcdcc306d5657c4c3 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -25,7 +25,6 @@
 
 (* $Id$ *)
 
-open ProofEngineHelpers
 open ProofEngineTypes
 
 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
@@ -232,7 +231,8 @@ let
 
 let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
-   saturate_term newmeta' metasenv' context termty goal_arity in
+   ProofEngineHelpers.saturate_term newmeta' metasenv' context termty
+    goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
   in
@@ -246,14 +246,14 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_with_subst ~term ~subst (proof, goal) =
+let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
  let module C = Cic in
   let (_,metasenv,_,_) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let newmeta = CicMkImplicit.new_meta metasenv subst in
+  let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
     match term with
        C.Var (uri,exp_named_subst) ->
@@ -298,7 +298,8 @@ let apply_with_subst ~term ~subst (proof, goal) =
      try
       new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
         termty n
-     with CicUnification.UnificationFailure _ when n > 0 ->
+     with (CicUnification.UnificationFailure _ 
+     | CicUniv.UniverseInconsistency _ ) when n > 0 ->
       add_one_argument (n - 1)
     in
      add_one_argument goal_arity
@@ -318,27 +319,29 @@ let apply_with_subst ~term ~subst (proof, goal) =
      CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
    in
    let (newproof, newmetasenv''') = 
-     subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
+    ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
+     newmetasenv''
    in
-   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
-    (newproof, 
-     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   subst,
+   (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+   max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
 
 
 (* ALB *)
-let apply_with_subst ~term ?(subst=[]) status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
   try
 (*     apply_tac_verbose ~term status *)
-    apply_with_subst ~term ~subst status
+    apply_with_subst ~term ~subst ~maxmeta status
       (* TODO cacciare anche altre eccezioni? *)
   with 
   | CicUnification.UnificationFailure msg
-  | CicTypeChecker.TypeCheckerFailure msg ->
-      raise (Fail msg)
+  | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
+  | CicUniv.UniverseInconsistency msg  -> raise (Fail (lazy msg))
 
 (* ALB *)
 let apply_tac_verbose ~term status =
-  let subst, status = apply_with_subst ~term status in
+  let subst, status, _ = apply_with_subst ~term status in
   (CicMetaSubst.apply_subst subst), status
 
 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
@@ -366,12 +369,13 @@ let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let newmeta = new_meta_of_proof ~proof in
+    let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let (context',ty',bo') =
       lambda_abstract ?howmany metasenv context newmeta ty mk_fresh_name_callback
      in
       let (newproof, _) =
-        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
+       ProofEngineHelpers.subst_meta_in_proof proof metano bo'
+        [newmeta,context',ty']
       in
        (newproof, [newmeta])
  in
@@ -385,7 +389,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
   let module C = Cic in
    let curi,metasenv,pbo,pty = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-    let newmeta1 = new_meta_of_proof ~proof in
+    let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
     let newmeta2 = newmeta1 + 1 in
     let fresh_name =
      mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
@@ -405,7 +409,7 @@ let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:
         C.Meta (newmeta2,irl2)]
      in
       let (newproof, _) =
-       subst_meta_in_proof proof metano bo'
+       ProofEngineHelpers.subst_meta_in_proof proof metano bo'
         [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
       in
        (newproof, [newmeta1 ; newmeta2])
@@ -431,7 +435,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
          "You can't letin a term containing the current goal"));
     let _,_ =
       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
-     let newmeta = new_meta_of_proof ~proof 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 =
@@ -443,7 +447,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
       let newmetaty = CicSubstitution.lift 1 ty in
       let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
        let (newproof, _) =
-         subst_meta_in_proof
+         ProofEngineHelpers.subst_meta_in_proof
            proof metano bo'[newmeta,context_for_newmeta,newmetaty]
        in
         (newproof, [newmeta])
@@ -463,7 +467,7 @@ let exact_tac ~term =
   if b then
    begin
     let (newproof, metasenv') =
-      subst_meta_in_proof proof metano term [] in
+      ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
     (newproof, [])
    end
   else
@@ -586,13 +590,13 @@ let letout_tac =
    let letout_tac (proof, goal) =
       let curi, metasenv, pbo, pty = proof in
       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
-      let newmeta = new_meta_of_proof ~proof 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, _ = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+      let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
       newproof, [newmeta]
    in
    mk_tactic letout_tac