new universes implementation

[helm.git] / helm / ocaml / tactics / ring.ml

diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml
index e2de0459193e91339b562f4f3a27075781585d78..cf6950c4be9776a7d4de1ad309c1a29d4da8b6e2 100644 (file)
--- a/helm/ocaml/tactics/ring.ml
+++ b/helm/ocaml/tactics/ring.ml
@@ -389,11 +389,15 @@ let elim_type_tac ~term status =
     @param term term to cut
     @param proof term used to prove second subgoal generated by elim_type
   *)
-let elim_type2_tac ~term ~proof status =
+let elim_type2_tac ~term ~proof =
+ let elim_type2_tac ~term ~proof status =
   let module E = EliminationTactics in
   warn "in Ring.elim_type2";
-  Tacticals.thens ~start:(E.elim_type_tac ~term)
-   ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status
+  ProofEngineTypes.apply_tactic 
+   (Tacticals.thens ~start:(E.elim_type_tac ~term)
+    ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
+ in
+  ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
 
 (* Galla: spostata in variousTactics.ml
   (**
@@ -423,7 +427,8 @@ let lift ~n (a,b,c,d,e,f,g,h) =
     @param count number of hypotheses to remove
     @param status current proof engine status
   *)
-let purge_hyps_tac ~count status =
+let purge_hyps_tac ~count =
+ let purge_hyps_tac ~count status =
   let module S = ProofEngineStructuralRules in
   let (proof, goal) = status in
   let rec aux n context status =
@@ -432,7 +437,8 @@ let purge_hyps_tac ~count status =
     | (0, _) -> status
     | (n, hd::tl) ->
         aux (n-1) tl
-         (status_of_single_goal_tactic_result (S.clear ~hyp:hd status))
+         (status_of_single_goal_tactic_result 
+         (ProofEngineTypes.apply_tactic (S.clear ~hyp:hd) status))
     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
   in
    let (_, metasenv, _, _) = proof in
@@ -440,6 +446,8 @@ let purge_hyps_tac ~count status =
      let proof',goal' = aux count context status in
       assert (goal = goal') ;
       proof',[goal']
+ in
+  ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
 
 (** THE TACTIC! *)
 
@@ -447,6 +455,7 @@ let purge_hyps_tac ~count status =
     Ring tactic, does associative and commutative rewritings in Reals ring
     @param status current proof engine status
   *)
+ 
 let ring_tac status =
   let (proof, goal) = status in
   warn "in Ring tactic";
@@ -467,8 +476,8 @@ let ring_tac status =
            t2; t2'; t2''; t2'_eq_t2'']);
       try
         let new_hyps = ref 0 in  (* number of new hypotheses created *)
-        Tacticals.try_tactics
-          status
+       ProofEngineTypes.apply_tactic 
+         (Tacticals.try_tactics
           ~tactics:[
             "reflexivity", EqualityTactics.reflexivity_tac ;
             "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
@@ -483,15 +492,17 @@ let ring_tac status =
                  ] ;
                 t1'_eq_t1''
                ]) ;
-            "elim_type eqt su t1 ...", (fun status ->
+            "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
               let status' = (* status after 1st elim_type use *)
                 let context = context_of_status status in
                 if not (are_convertible context t1'' t1) then begin
                   warn "t1'' and t1 are NOT CONVERTIBLE";
                   let newstatus =
-                    elim_type2_tac  (* 1st elim_type use *)
-                      status ~proof:t1'_eq_t1''
-                      ~term:(Cic.Appl [eqt; r; t1''; t1])
+                   ProofEngineTypes.apply_tactic 
+                    (elim_type2_tac  (* 1st elim_type use *)
+                      ~proof:t1'_eq_t1''
+                      ~term:(Cic.Appl [eqt; r; t1''; t1]))
+                   status 
                   in
                    incr new_hyps; (* elim_type add an hyp *)
                    match newstatus with
@@ -506,8 +517,8 @@ let ring_tac status =
                 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
               in
               let status'' =
-                Tacticals.try_tactics (* try to solve 1st subgoal *)
-                  status'
+              ProofEngineTypes.apply_tactic
+                (Tacticals.try_tactics (* try to solve 1st subgoal *)
                   ~tactics:[
                     "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
                     "exact sym_eqt su t2 ...",
@@ -521,15 +532,18 @@ let ring_tac status =
                             ] ;
                            t2'_eq_t2''
                           ]) ;
-                    "elim_type eqt su t2 ...", (fun status ->
+                    "elim_type eqt su t2 ...", 
+                    ProofEngineTypes.mk_tactic (fun status ->
                       let status' =
                         let context = context_of_status status in
                         if not (are_convertible context t2'' t2) then begin
                           warn "t2'' and t2 are NOT CONVERTIBLE";
                           let newstatus =
-                            elim_type2_tac  (* 2nd elim_type use *)
-                              status ~proof:t2'_eq_t2''
-                              ~term:(Cic.Appl [eqt; r; t2''; t2])
+                           ProofEngineTypes.apply_tactic 
+                             (elim_type2_tac  (* 2nd elim_type use *)
+                              ~proof:t2'_eq_t2''
+                              ~term:(Cic.Appl [eqt; r; t2''; t2]))
+                            status
                           in
                           incr new_hyps; (* elim_type add an hyp *)
                           match newstatus with
@@ -542,12 +556,16 @@ let ring_tac status =
                       in
                       try (* try to solve main goal *)
                         warn "trying reflexivity ....";
-                        EqualityTactics.reflexivity_tac status'
+                        ProofEngineTypes.apply_tactic 
+                        EqualityTactics.reflexivity_tac status'
                       with (Fail _) ->  (* leave conclusion to the user *)
                         warn "reflexivity failed, solution's left as an ex :-)";
-                        purge_hyps_tac ~count:!new_hyps status')]
+                        ProofEngineTypes.apply_tactic 
+                        (purge_hyps_tac ~count:!new_hyps) status')])
+                 status'       
               in
-              status'')]
+              status'')])
+        status      
       with (Fail s) ->
         raise (Fail ("Ring failure: " ^ s))
     end
@@ -555,9 +573,12 @@ let ring_tac status =
     assert false
 
   (* wrap ring_tac catching GoalUnringable and raising Fail *)
+
 let ring_tac status =
   try
     ring_tac status
   with GoalUnringable ->
     raise (Fail "goal unringable")
 
+let ring_tac = ProofEngineTypes.mk_tactic ring_tac
+