first working (?) version of lapply

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a9c85e7d86f1ccd3b0dc6ddcb4b336ca5b725e9c..4373b9be73927c201d67ba3c09553fcdcfc44959 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -30,8 +30,10 @@ let tactic_of_ast = function
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
+  | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
   | TacticAst.Exists _ -> Tactics.exists
   | TacticAst.Fourier _ -> Tactics.fourier
+  | TacticAst.Generalize (_,term,pat) -> Tactics.generalize term pat
   | TacticAst.Goal (_, n) -> Tactics.set_goal n
   | TacticAst.Left _ -> Tactics.left
   | TacticAst.Right _ -> Tactics.right
@@ -58,7 +60,6 @@ let tactic_of_ast = function
   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
   | TacticAst.Change of 'term * 'term * 'ident option
   | TacticAst.Decompose of 'ident * 'ident list
-  | TacticAst.Discriminate of 'ident
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
   | TacticAst.Replace_pattern of 'term pattern * 'term
@@ -76,12 +77,10 @@ let tactic_of_ast = function
         EqualityTactics.rewrite_tac ~where:pattern ~term:t ()
       else
         EqualityTactics.rewrite_back_tac ~where:pattern ~term:t ()
-  | TacticAst.FwdSimpl (_, name) -> 
-     Tactics.fwd_simpl ~hyp:(Cic.Name name) ~dbd:(MatitaDb.instance ())
-  | TacticAst.LApply (_, term, substs) ->
-     let f (name, term) = Cic.Name name, term in
-     Tactics.lapply ~substs:(List.map f substs) term
-  | _ -> assert false
+  | TacticAst.FwdSimpl (_, term) -> 
+     Tactics.fwd_simpl ~what:term ~dbd:(MatitaDb.instance ())
+  | TacticAst.LApply (_, to_what, what) ->
+     Tactics.lapply ?to_what what
 
 let eval_tactical status tac =
   let apply_tactic tactic =
@@ -404,16 +403,23 @@ let disambiguate_tactic status = function
       let status, cic1 = disambiguate_term status what in
       let status, cic2 = disambiguate_term status with_what in
       status, TacticAst.Replace (loc, cic1, cic2)
-  | TacticAst.Change (loc, what, with_what, ident) -> 
+  | TacticAst.Change (loc, what, with_what, pattern) -> 
       let status, cic1 = disambiguate_term status what in
       let status, cic2 = disambiguate_term status with_what in
-      status, TacticAst.Change (loc, cic1, cic2, ident)
+      let pattern = disambiguate_pattern status.aliases pattern in
+      status, TacticAst.Change (loc, cic1, cic2, pattern)
+  | TacticAst.Generalize (loc,term,pattern) ->
+      let status,term = disambiguate_term status term in
+      let pattern = disambiguate_pattern status.aliases pattern in
+      status, TacticAst.Generalize(loc,term,pattern)
+  | TacticAst.Discriminate (loc,term) ->
+      let status,term = disambiguate_term status term in
+      status, TacticAst.Discriminate(loc,term)
 (*
   (* TODO Zack a lot more of tactics to be implemented here ... *)
   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
   | TacticAst.Change of 'term * 'term * 'ident option
   | TacticAst.Decompose of 'ident * 'ident list
-  | TacticAst.Discriminate of 'ident
   | TacticAst.Fold of reduction_kind * 'term
   | TacticAst.Injection of 'ident
   | TacticAst.Replace_pattern of 'term pattern * 'term
@@ -442,19 +448,16 @@ let disambiguate_tactic status = function
   | TacticAst.Split loc -> status, TacticAst.Split loc
   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
-  | TacticAst.FwdSimpl (loc, name) -> status, TacticAst.FwdSimpl (loc, name)  
-  | TacticAst.LApply (loc, term, substs) ->
-     let f (status, substs) (name, term) =
-        let status, term = disambiguate_term status term in
-       status, (name, term) :: substs
-     in
+  | TacticAst.FwdSimpl (loc, term) ->
      let status, term = disambiguate_term status term in
-     let status, substs = List.fold_left f (status, []) substs in 
-     status, TacticAst.LApply (loc, term, substs)
-  
-  | x -> 
-      print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
-      assert false
+     status, TacticAst.FwdSimpl (loc, term)  
+  | TacticAst.LApply (loc, Some to_what, what) ->
+     let status, to_what = disambiguate_term status to_what in
+     let status, what = disambiguate_term status what in
+     status, TacticAst.LApply (loc, Some to_what, what)
+  | TacticAst.LApply (loc, None, what) ->
+     let status, what = disambiguate_term status what in
+     status, TacticAst.LApply (loc, None, what)
 
 let rec disambiguate_tactical status = function 
   | TacticAst.Tactic (loc, tactic) ->