X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=3a24b0d5fd737624da42532c8d4bba173b998f51;hb=bd277786d78d49594b3ada1c3c9c28cba5dc03b9;hp=a1c8cab690d2bc8c8e5915e44d371653d969a1ec;hpb=82183b138d009e90a2d3381eb84bab6f46dbc728;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index a1c8cab69..3a24b0d5f 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -24,39 +24,48 @@
  *)
 
 let assume id t =
- Tacticals.then_
-  ~start:
-    (Tactics.intros ~howmany:1
-      ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
-  ~continuation:
-    (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
-     (fun _ metasenv ugraph -> t,metasenv,ugraph))
+  Tacticals.then_
+     ~start:
+       (Tactics.intros ~howmany:1
+        ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
+     ~continuation:
+       (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)
+         (fun _ metasenv ugraph -> t,metasenv,ugraph))
 ;;
 
-let suppose t id =
+let suppose t id ty =
+(*BUG: ty not used *)
  Tacticals.then_
    ~start:
        (Tactics.intros ~howmany:1
              ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ())
    ~continuation:
-	    (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
-	      (fun _ metasenv ugraph -> t,metasenv,ugraph))
+            (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None)  
+              (fun _ metasenv ugraph -> t,metasenv,ugraph))
 ;;
 
-let by_term_we_proved t ty id =
- Tacticals.thens
- ~start:
-   (Tactics.cut ty
-     ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
- ~continuations:
-   [ Tacticals.id_tac ; Tactics.apply t ]
+let by_term_we_proved t ty id ty' =
+(*BUG: ty' not used *)
+ match t with
+    None -> assert false
+  | Some t ->
+     Tacticals.thens
+     ~start:
+       (Tactics.cut ty
+         ~mk_fresh_name_callback:(fun _ _ _  ~typ -> Cic.Name id))
+     ~continuations:
+       [ Tacticals.id_tac ; Tactics.apply t ]
 ;;
 
 let bydone t =
-   (Tactics.apply ~term:t)
+   match t with
+    None -> assert false
+  | Some t ->
+    (Tactics.apply ~term:t)
 ;;
 
-let we_need_to_prove t id =
+let we_need_to_prove t id ty =
+(*BUG: ty not used *)
  let aux status =
   let proof,goals =
    ProofEngineTypes.apply_tactic
@@ -73,3 +82,104 @@ let we_need_to_prove t id =
  in
   ProofEngineTypes.mk_tactic aux
 ;;
+
+let existselim t id1 t1 id2 t2 =
+(*BUG: t1 and t2 not used *)
+(*PARSING BUG: t2 is parsed in the current context, but it may
+  have occurrences of id1 in it *)
+ Tactics.elim_intros t
+  ~mk_fresh_name_callback:
+    (let i = ref 0 in
+      fun _ _ _  ~typ ->
+       incr i;
+       if !i = 1 then Cic.Name id1 else Cic.Name id2)
+
+let andelim = existselim;;
+
+let rewritingstep lhs rhs just conclude =
+ let aux ((proof,goal) as status) =
+  let (curi,metasenv,proofbo,proofty) = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let eq,trans =
+   match LibraryObjects.eq_URI () with
+      None -> assert false (*TODO*)
+    | Some uri ->
+      Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
+  in
+  let ty,_ =
+   CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+  let just =
+   match just with
+      None -> assert false (*TOOD*)
+    | Some just -> just
+  in
+   match lhs with
+      None ->
+       let plhs,prhs =
+        match 
+         fst
+          (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1)
+            CicUniv.empty_ugraph)
+        with
+           Cic.Appl [_;_;plhs;prhs] -> plhs,prhs
+         | _ -> assert false in
+       let last_hyp_name =
+        match context with
+           (Some (Cic.Name id,_))::_ -> id
+         | _ -> assert false
+       in
+        (match conclude with
+            None ->
+             ProofEngineTypes.apply_tactic
+              (Tacticals.thens
+                ~start:(Tactics.apply ~term:trans)
+                ~continuations:
+                  [ Tactics.apply prhs ;
+                    Tactics.apply (Cic.Rel 1) ;
+                    Tactics.apply just]) status
+          | Some name ->
+             let mk_fresh_name_callback =
+	      fun metasenv context _ ~typ ->
+	        FreshNamesGenerator.mk_fresh_name ~subst:[]
+	         metasenv context name ~typ
+	     in
+              ProofEngineTypes.apply_tactic
+               (Tacticals.thens
+                 ~start:(Tactics.cut ~mk_fresh_name_callback
+		  (Cic.Appl [eq ; ty ; plhs ; rhs]))
+                 ~continuations:
+                   [ Tactics.clear ~hyps:[last_hyp_name] ;
+                     Tacticals.thens
+                      ~start:(Tactics.apply ~term:trans)
+                      ~continuations:
+                        [ Tactics.apply prhs ;
+                          Tactics.apply (Cic.Rel 1) ;
+                          Tactics.apply just]
+                   ]) status)
+    | Some lhs ->
+       match conclude with
+          None -> ProofEngineTypes.apply_tactic (Tactics.apply just) status
+        | Some name ->
+            let mk_fresh_name_callback =
+	     fun metasenv context _ ~typ ->
+	       FreshNamesGenerator.mk_fresh_name ~subst:[]
+	        metasenv context name ~typ
+	    in
+             ProofEngineTypes.apply_tactic
+              (Tacticals.thens
+                ~start:
+                  (Tactics.cut ~mk_fresh_name_callback
+                    (Cic.Appl [eq ; ty ; lhs ; rhs]))
+                ~continuations:[ Tacticals.id_tac ; Tactics.apply just ]) status
+ in
+  ProofEngineTypes.mk_tactic aux
+;;
+
+let case _ = assert false
+;;
+let thesisbecomes _ = assert false
+;;
+let byinduction _ = assert false
+;;
+let we_proceed_by_induction_on _ = assert false
+;;