"Insert Query (Experts only)" menu item added.

[helm.git] / helm / gTopLevel / variousTactics.ml

diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml
index 9e8b18b7d96b077d7074230d2c31148ba569f82e..604307cd35cb662b16631efb40cc16044b3d7a00 100644 (file)
--- a/helm/gTopLevel/variousTactics.ml
+++ b/helm/gTopLevel/variousTactics.ml
@@ -65,88 +65,33 @@ let assumption_tac ~status:(proof,goal)=
 
 (* ANCORA DA DEBUGGARE *)
 
-
-(* IN FASE DI IMPLEMENTAZIONE *)
-
+(* serve una funzione che cerchi nel ty dal basso a partire da term, i lambda
+e li aggiunga nel context, poi si conta la lunghezza di questo nuovo
+contesto e si lifta *)
 let generalize_tac ~term ~status:((proof,goal) as status) =
   let module C = Cic in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    let _,metasenv,_,_ = proof in
     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-(*
-let uno = (C.Appl [
-             C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ; 
-             C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])])  in 
- let tuno = CicTypeChecker.type_of_aux' metasenv context uno in
-prerr_endline ("#### uno: " ^ CicPp.ppterm uno);
-prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno);
-*)
-prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term)));
-prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1));
-prerr_endline ("#### term: " ^ CicPp.ppterm term);
-prerr_endline ("#### ty: " ^ CicPp.ppterm ty);
-
-
      T.thens 
       ~start:(P.cut_tac 
        ~term:(
-         C.Prod (
+         C.Prod(
           (C.Name "dummy_for_gen"), 
-          (CicTypeChecker.type_of_aux' metasenv context term), 
-          (ProofEngineReduction.replace_lifting
+          (CicTypeChecker.type_of_aux' metasenv context term),
+          (ProofEngineReduction.replace_lifting_csc 1
             ~equality:(==) 
-            ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)  
             ~what:term 
-            ~where:ty))))
-      ~continuations: 
-       [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))]     (* in quest'ordine o viceversa? provare *)
-(*       [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac]   (* in quest'ordine o viceversa? provare *)*)
+            ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)  
+            ~where:ty)
+        )))    
+      ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
       ~status
 ;;
 
-(*
-let generalize_tac ~term ~status:((proof,goal) as status) =
-  let module C = Cic in
-  let module H = ProofEngineHelpers in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-     let add_decl_tac ~term ~status:(proof, goal) =
-      let module C = Cic in
-      let curi,metasenv,pbo,pty = proof in
-      let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-       let _ = CicTypeChecker.type_of_aux' metasenv context term in
-        let newmeta = H.new_meta ~proof in
-        let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in
-        let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in
-         let newmetaty = CicSubstitution.lift 1 ty in
-         let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in
-          let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty]
-         in
-          (newproof, [newmeta])
-       
-     in
-      T.then_ 
-       ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term)) 
-       ~continuation:(
-T.id_tac) (*         T.thens 
-          ~start:(P.cut_tac ~term:(ProofEngineReduction.replace
-            ~equality:(==)
-            ~with_what:(C.Rel 1) (* dummy_for_gen *)
-            ~what:term
-            ~where:ty))
-          ~continuations:
-            [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))])      (* in quest'ordine o viceversa? provare *)
-(*            [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac])     in quest'ordine o viceversa? provare *)
-*)      ~status
-;;
-*)
-
 
+(* IN FASE DI IMPLEMENTAZIONE *)
 
 let decide_equality_tac =
   Tacticals.id_tac
@@ -170,14 +115,3 @@ let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
 ;;
 *)
 
-
-
-(*** DOMANDE ***
-
-- come faccio clear di un ipotesi di cui non so il nome?
-- differenza tra elim e induction ...e inversion?
-- come passo a decompose la lista di termini?
-- ma la rewrite funzionava?
-- come implemento la generalize?
-
-*)