* new binary matitatop

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 37c96ce4e70f6e14a5613ee74e3daea1d837fa5d..95de73528cf8ba1b273002e395026d11c2935d59 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -2,6 +2,8 @@
 open Printf
 open MatitaTypes
 
+exception Drop;;
+
 let debug = false ;;
 let debug_print = if debug then prerr_endline else ignore ;;
 
@@ -25,7 +27,8 @@ let tactic_of_ast = function
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Auto (_,depth,width) -> 
       AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
-  | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
+  | TacticAst.Change (_, what, with_what, pattern) ->
+     Tactics.change ~what ~with_what ~pattern
   | TacticAst.Clear (_,id) -> Tactics.clear id
   | TacticAst.ClearBody (_,id) -> Tactics.clearbody id
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -66,8 +69,9 @@ let tactic_of_ast = function
   | TacticAst.Intros (_, Some num, names) ->
       PrimitiveTactics.intros_tac ~howmany:num
         ~mk_fresh_name_callback:(namer_of names) ()
-  | TacticAst.LApply (_, to_what, what) ->
-     Tactics.lapply ?to_what what
+  | TacticAst.LApply (_, to_what, what, ident) ->
+     let names = match ident with None -> [] | Some id -> [id] in
+     Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?to_what what
   | TacticAst.Left _ -> Tactics.left
   | TacticAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
@@ -221,6 +225,7 @@ let generate_projections uri fields status =
 let eval_command status cmd =
   match cmd with
   | TacticAst.Set (loc, name, value) -> set_option status name value
+  | TacticAst.Drop loc -> raise Drop
   | TacticAst.Qed loc ->
       let uri, metasenv, bo, ty = 
         match status.proof_status with
@@ -448,7 +453,7 @@ let disambiguate_tactic status = function
       status, TacticAst.Injection (loc,term)
   | TacticAst.Intros (loc, num, names) ->
       status, TacticAst.Intros (loc, num, names)
-  | TacticAst.LApply (loc, to_what, what) ->
+  | TacticAst.LApply (loc, to_what, what, ident) ->
      let status, to_what =
       match to_what with
          None -> status,None
@@ -457,7 +462,7 @@ let disambiguate_tactic status = function
            status, Some to_what
      in
      let status, what = disambiguate_term status what in
-     status, TacticAst.LApply (loc, to_what, what)
+     status, TacticAst.LApply (loc, to_what, what, ident)
   | TacticAst.Left loc -> status, TacticAst.Left loc
   | TacticAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in
@@ -523,7 +528,7 @@ let disambiguate_command status = function
   | TacticAst.Coercion (loc, term) ->
       let status, term = disambiguate_term status term in
       status, TacticAst.Coercion (loc,term)
-  | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
+  | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
       status, cmd
   | TacticAst.Alias _ as x -> status, x
   | TacticAst.Obj (loc,obj) ->
@@ -565,9 +570,16 @@ let eval_ast status ast =
 
 let eval_from_stream status str cb =
   let stl = CicTextualParser2.parse_statements str in
-  List.fold_left 
-    (fun status ast -> cb status ast;eval_ast status ast) status 
-  stl
+  List.iter (fun ast -> cb !status ast;status := eval_ast !status ast) stl
+
+let eval_from_stream_greedy status str cb =
+  while true do
+    print_string "matita> ";
+    flush stdout;
+    let ast = CicTextualParser2.parse_statement str in
+    cb !status ast;
+    status := eval_ast !status ast 
+  done
   
 let eval_string status str =
   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())