X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=a649d4a23e2df518e77f37f96662fd02a3fb718e;hb=0c6a5aadb1a7746681a8e26fc0b009f847c10557;hp=0e9f72b0f96b73d65ea5644a85dbdceda93913d6;hpb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;p=helm.git

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 0e9f72b0f..a649d4a23 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -23,119 +23,132 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-let rewrite_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let eq_ind_r,ty,t1,t2 =
-    match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
-        when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
-         let eq_ind_r =
-          C.Const
-           (HelmLibraryObjects.Logic.eq_ind_r_URI,[])
-         in
-          eq_ind_r,ty,t1,t2
-     | _ ->
-       raise
-        (ProofEngineTypes.Fail
-          "Rewrite: the argument is not a proof of an equality")
-   in
-    let pred =
-     let gty' = CicSubstitution.lift 1 gty in
-     let t1' = CicSubstitution.lift 1 t1 in
-     let gty'' =
-      ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
-     in
-      C.Lambda
-       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
-         ty, gty'')
+let rewrite_tac ~term:equality =
+ let rewrite_tac ~term:equality (proof,goal) =
+  let module C = Cic in
+  let module U = UriManager in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+    let eq_ind_r,ty,t1,t2 =
+     match CicTypeChecker.type_of_aux' metasenv context equality with
+        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
+         when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
+          let eq_ind_r =
+           C.Const
+            (HelmLibraryObjects.Logic.eq_ind_r_URI,[])
+          in
+           eq_ind_r,ty,t1,t2
+      | _ ->
+        raise
+         (ProofEngineTypes.Fail
+           "Rewrite: the argument is not a proof of an equality")
     in
-    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-    let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-
-     let (proof',goals) =
-      PrimitiveTactics.exact_tac
-       ~term:(C.Appl
-         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-          ((curi,metasenv',pbo,pty),goal)
+     let pred =
+      let gty' = CicSubstitution.lift 1 gty in
+      let t1' = CicSubstitution.lift 1 t1 in
+      let gty'' =
+       ProofEngineReduction.replace_lifting
+        ~equality:ProofEngineReduction.alpha_equivalence
+        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
+      in
+       C.Lambda
+        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+          ty, gty'')
      in
-      assert (List.length goals = 0) ;
-      (proof',[fresh_meta])
+     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+     let irl =CicMkImplicit.identity_relocation_list_for_metavariable context in
+     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+ 
+      let (proof',goals) =
+       ProofEngineTypes.apply_tactic 
+        (PrimitiveTactics.exact_tac
+         ~term:(C.Appl
+          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))        ((curi,metasenv',pbo,pty),goal)
+      in
+       assert (List.length goals = 0) ;
+       (proof',[fresh_meta])
+ in
+  ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
 ;;
 
 
-let rewrite_simpl_tac ~term status =
- Tacticals.then_ 
-  ~start:(rewrite_tac ~term)
-  ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  status
+let rewrite_simpl_tac ~term =
+ let rewrite_simpl_tac ~term status =
+  ProofEngineTypes.apply_tactic
+  (Tacticals.then_ 
+   ~start:(rewrite_tac ~term)
+   ~continuation:
+    (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+   status
+ in
+  ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
 ;;
 
 
-let rewrite_back_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let eq_ind_r,ty,t1,t2 =
-    match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
-        when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
-         let eq_ind_r =
-          C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[])
-         in
-          eq_ind_r,ty,t2,t1
-     | _ ->
-       raise
-        (ProofEngineTypes.Fail
-          "Rewrite: the argument is not a proof of an equality")
-   in
-    let pred =
-     let gty' = CicSubstitution.lift 1 gty in
-     let t1' = CicSubstitution.lift 1 t1 in
-     let gty'' =
-      ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
-     in
-      C.Lambda
-       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
-         ty, gty'')
+let rewrite_back_tac ~term:equality =
+ let rewrite_back_tac equality (proof,goal) =
+  let module C = Cic in
+  let module U = UriManager in
+   let curi,metasenv,pbo,pty = proof in
+   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+    let eq_ind_r,ty,t1,t2 =
+     match CicTypeChecker.type_of_aux' metasenv context equality with
+        C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
+         when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
+          let eq_ind_r =
+           C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[])
+          in
+           eq_ind_r,ty,t2,t1
+      | _ ->
+        raise
+         (ProofEngineTypes.Fail
+           "Rewrite: the argument is not a proof of an equality")
     in
-    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-    let irl =
-     CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-
-     let (proof',goals) =
-      PrimitiveTactics.exact_tac
-       ~term:(C.Appl
-         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-        ((curi,metasenv',pbo,pty),goal)
+     let pred =
+      let gty' = CicSubstitution.lift 1 gty in
+      let t1' = CicSubstitution.lift 1 t1 in
+      let gty'' =
+       ProofEngineReduction.replace_lifting
+        ~equality:ProofEngineReduction.alpha_equivalence
+        ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
+      in
+       C.Lambda
+        (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
+          ty, gty'')
      in
-      assert (List.length goals = 0) ;
-      (proof',[fresh_meta])
-
+     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
+     let irl =
+      CicMkImplicit.identity_relocation_list_for_metavariable context in
+     let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+ 
+      let (proof',goals) =
+       ProofEngineTypes.apply_tactic
+        (PrimitiveTactics.exact_tac
+         ~term:(C.Appl
+          [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))
+         ((curi,metasenv',pbo,pty),goal)
+      in
+       assert (List.length goals = 0) ;
+       (proof',[fresh_meta])
+ in
+  ProofEngineTypes.mk_tactic (rewrite_back_tac equality)
 ;;
 
 
-let rewrite_back_simpl_tac ~term status =
- Tacticals.then_ 
-  ~start:(rewrite_back_tac ~term)
-  ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  status
+let rewrite_back_simpl_tac ~term =
+ let rewrite_back_simpl_tac ~term status =
+  ProofEngineTypes.apply_tactic
+   (Tacticals.then_ 
+    ~start:(rewrite_back_tac ~term)
+    ~continuation:
+     (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
+   status
+ in
+  ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
 ;;
 
-
-let replace_tac ~what ~with_what status =
+let replace_tac ~what ~with_what =
+ let replace_tac ~what ~with_what status =
   let (proof, goal) = status in
   let module C = Cic in
   let module U = UriManager in
@@ -147,7 +160,8 @@ let replace_tac ~what ~with_what status =
       try
       if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
        then
-         T.thens
+        ProofEngineTypes.apply_tactic
+         (T.thens
           ~start:(
             P.cut_tac 
              (C.Appl [
@@ -161,10 +175,13 @@ let replace_tac ~what ~with_what status =
                ~continuation:(
                  ProofEngineStructuralRules.clear
                   ~hyp:(List.hd context)) ;
-            T.id_tac]
+            T.id_tac])
           status
        else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
-       with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
+       with (Failure "hd") -> 
+            raise (ProofEngineTypes.Fail "Replace: empty context")
+ in
+  ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
 ;;
 
 
@@ -174,23 +191,28 @@ let reflexivity_tac =
   IntroductionTactics.constructor_tac ~n:1
 ;;
 
-
-let symmetry_tac (proof, goal) =
+let symmetry_tac =
+ let symmetry_tac (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
    let (_,metasenv,_,_) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
-         PrimitiveTactics.apply_tac (proof,goal)
-          ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))
+        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
+	 when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
+	  ProofEngineTypes.apply_tactic 
+           (PrimitiveTactics.apply_tac 
+	    ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))) 
+	   (proof,goal)
 
       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
+ in
+  ProofEngineTypes.mk_tactic symmetry_tac
 ;;
 
-
-let transitivity_tac ~term status =
+let transitivity_tac ~term =
+ let transitivity_tac ~term status =
   let (proof, goal) = status in
   let module C = Cic in
   let module R = CicReduction in
@@ -199,15 +221,19 @@ let transitivity_tac ~term status =
    let (_,metasenv,_,_) = proof in
     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      match (R.whd context ty) with
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = HelmLibraryObjects.Logic.eq_URI) ->
-         T.thens
+        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) 
+	when (uri = HelmLibraryObjects.Logic.eq_URI) ->
+         ProofEngineTypes.apply_tactic 
+	 (T.thens
           ~start:(PrimitiveTactics.apply_tac
             ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, [])))
           ~continuations:
-            [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]
+            [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac])
           status
 
       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
+ in
+  ProofEngineTypes.mk_tactic (transitivity_tac ~term)
 ;;