- "linear" flag added to lapply (automatic clearing)

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 8b83bcff0fcf3569af351757165b11b88cd3dfbc..d7343c98c1447c5831ace4066798c6828e37fd09 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -60,10 +60,11 @@ let tactic_of_ast ast =
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
+  | GrafiteAst.ApplyS (_, term) ->
+     Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
-      AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
-        ~dbd:(LibraryDb.instance ()) ()
+  | GrafiteAst.Auto (_,params) ->
+      AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -81,7 +82,7 @@ let tactic_of_ast ast =
       let user_types = List.rev_map to_type types in
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
-      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+      Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -129,10 +130,10 @@ let tactic_of_ast ast =
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
-  | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+  | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
       let names = match ident with None -> [] | Some id -> [id] in
-      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
-        ~to_what what
+      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
+        ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
@@ -480,15 +481,16 @@ let eval_tactical ~disambiguate_tactic status tac =
         MatitaTacticals.solve_tactics
          ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
 
-    | GrafiteAst.Skip loc -> MatitaTacticals.skip
-    | GrafiteAst.Dot loc -> MatitaTacticals.dot
-    | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
-    | GrafiteAst.Branch loc -> MatitaTacticals.branch
-    | GrafiteAst.Shift loc -> MatitaTacticals.shift
-    | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
-    | GrafiteAst.Merge loc -> MatitaTacticals.merge
-    | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
-    | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+    | GrafiteAst.Skip _loc -> MatitaTacticals.skip
+    | GrafiteAst.Dot _loc -> MatitaTacticals.dot
+    | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
+    | GrafiteAst.Branch _loc -> MatitaTacticals.branch
+    | GrafiteAst.Shift _loc -> MatitaTacticals.shift
+    | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
+    | GrafiteAst.Merge _loc -> MatitaTacticals.merge
+    | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
+    | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
+    | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
   in
   let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
   let status =  (* is proof completed? *)