firs wrking (?) version of lapply

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 5127f21383b222e6bac568c79f73e777f6282582..d5a06db88ade6983a7c15c6697239e77ffd85ff5 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -66,7 +66,7 @@ let keywords = Hashtbl.create 17
 let _ =
   List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword))
     [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with";
-      "in"; "and" ]
+      "in"; "and"; "to" ]
 
 let error lexbuf msg =
   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index e54185a1b2fd9e368673caa9f923c30c12bbfe4a..9a88a2cbef3e792ad49d154cfc06fc0ef89efd11 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -417,8 +417,8 @@ EXTEND
         TacticAst.Transitivity (loc, t)
     | [ IDENT "fwd" ]; t = term ->
         TacticAst.FwdSimpl (loc, t)
-    | [ IDENT "lapply" ]; t = term ->
-        TacticAst.LApply (loc, t)
+    | [ IDENT "lapply" ]; what = tactic_term; to_what = OPT [ "to" ; t = tactic_term -> t ] ->
+        TacticAst.LApply (loc, to_what, what)
     ]
   ];
   tactical:

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 269ba553a22467ae74bec15eda5229154ce71e87..3c659bb6063dc15790d6ce64a9edce0c2c8a2669 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -63,7 +63,7 @@ type ('term, 'ident) tactic =
   | Symmetry of loc
   | Transitivity of loc * 'term
   | FwdSimpl of loc * 'term
-  | LApply of loc * 'term
+  | LApply of loc * 'term option * 'term
 
 type thm_flavour =
   [ `Definition

diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml
index 918ecd60597e1ebfff35fe5b1704b2c5d3e9d824..d75a7c5f8a7bb1ec624415677d6268b3774e1140 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.ml
+++ b/helm/ocaml/tactics/fwdSimplTactic.ml
@@ -30,6 +30,7 @@ module PEH = ProofEngineHelpers
 module U  = CicUniv
 module S = CicSubstitution
 module PT = PrimitiveTactics
+module T = Tacticals
 
 let fail_msg1 = "no applicable simplification"
 
@@ -38,7 +39,60 @@ let error msg = raise (PET.Fail msg)
 (* lapply *******************************************************************)
 
 let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
-               (* ?(substs = []) *) what =
+               (* ?(substs = []) *) ?to_what what =
+   let cut_tac term = PT.cut_tac ~mk_fresh_name_callback term in
+   let apply_tac term = PT.apply_tac term in
+   let strip_dependent_prods metasenv context t =
+      let irl = MI.identity_relocation_list_for_metavariable context in
+      let rec aux metasenv p xcontext = function
+         | Cic.Prod (name, t1, t2) when not (TC.does_not_occur xcontext 0 1 t2) ->  
+            let index = MI.new_meta metasenv [] in
+            let metasenv = [index, context, t1] @ metasenv in
+            let e, s = Some (name, Cic.Decl t1), Cic.Meta (index, irl) in    
+           aux metasenv (succ p) (e :: xcontext) (S.subst s t2)
+         | Cic.Prod (name, t1, t2) -> metasenv, p, Some t1, t2
+         | t                       -> metasenv, p, None, t 
+      in
+      aux metasenv 0 context t
+   in
+   let rec mk_continuations p l =
+      if p <= 0 then l else mk_continuations (pred p) (T.id_tac :: l)
+   in
+   let lapply_tac (proof, goal) =
+      let xuri, metasenv, u, t = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+      match strip_dependent_prods metasenv context lemma with
+         | metasenv, p, Some premise, conclusion ->
+           let premise_tac = 
+              match to_what with
+                 | None      -> T.id_tac 
+                 | Some term -> PT.apply_tac term 
+           in
+           let status = (xuri, metasenv, u, t), goal in
+            let tac = T.thens ~start:(cut_tac premise)
+                             ~continuations:[  
+                     T.thens ~start:(cut_tac conclusion)
+                             ~continuations:[ T.id_tac; 
+                     T.thens ~start:(PT.apply_tac what)
+                             ~continuations:(mk_continuations p [PT.apply_tac ~term:(Cic.Rel 1)])
+                                            ]; premise_tac ]
+           in
+           PET.apply_tactic tac status
+         | metasenv, p, None, conclusion         ->
+           failwith "lapply_tac: not implemented"
+   in
+   PET.mk_tactic lapply_tac
+   
+   
+   
+   
+   
+   
+   
+   
+   
+(*   
    let count_dependent_prods context t =
       let rec aux context p = function
          | Cic.Prod (name, t1, t2) -> 
@@ -92,7 +146,7 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       PET.apply_tactic (PT.cut_tac ~mk_fresh_name_callback holed_lemma) status
    in
    PET.mk_tactic lapply_tac
-
+*)
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac ~what ~dbd =

diff --git a/helm/ocaml/tactics/fwdSimplTactic.mli b/helm/ocaml/tactics/fwdSimplTactic.mli
index 1c221ee010b7143e132ecd93b958ce03ee3ef2da..7d3355e97f45650df6b85d5e19d2af8644c04c94 100644 (file)
--- a/helm/ocaml/tactics/fwdSimplTactic.mli
+++ b/helm/ocaml/tactics/fwdSimplTactic.mli
@@ -25,7 +25,7 @@
 
 val lapply_tac:
    ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-   Cic.term -> ProofEngineTypes.tactic
+   ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic
 
 val fwd_simpl_tac:
    what:Cic.term -> dbd:Mysql.dbd -> ProofEngineTypes.tactic

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 4e0e04914bd1ac9bcafa04f8c9d1c1c4cff14308..62f1ce322c4a98be3b42ef890700b6588e903de5 100644 (file)
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -94,7 +94,12 @@ let thens ~start ~continuations =
        (proof',goals@new_goals')
     ) (proof,[]) new_goals continuations
   with
-   Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+   Invalid_argument _ -> 
+(* FG: more debugging information *)
+    let debug = Printf.sprintf "thens: expected %i new goals, found %i"
+     (List.length continuations) (List.length new_goals)
+    in
+    raise (Fail debug)
  in
   mk_tactic (thens ~start ~continuations )
 

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 9e5a4ce47fa686bdb57de1918bde1c37dfde61db..2fbb409cdf35b4a79733d6766645b59177b75240 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -43,7 +43,7 @@ val intros :
   unit -> ProofEngineTypes.tactic
 val lapply :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-  Cic.term -> ProofEngineTypes.tactic
+  ?to_what:Cic.term -> Cic.term -> ProofEngineTypes.tactic
 val left : ProofEngineTypes.tactic
 val letin :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->