added script support a la coqide

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 4d3137d55e74e56bea5de9e36979a7993b2a2e74..96b765c704350d95307b70f220d1d6e1cdcd8a70 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -63,7 +63,8 @@ let split_obj = function
 class virtual interpreterState = 
     (* static values, shared by all states inheriting this class *)
   let loc = ref None in
-  let history = ref [] in
+  let last_item = ref None in
+  let evalAstCallback = ref None in
   fun ~(console: #MatitaTypes.console) ->
   object (self)
 
@@ -74,34 +75,37 @@ class virtual interpreterState =
       (** eval a toplevel phrase in the current state and return the new state
       *)
     method parsePhrase s =
-      match CicTextualParser2.parse_tactical s with
+      match disambiguator#parserr#parseTactical s with
       | (TacticAst.LocatedTactical (loc', tac)) as tactical ->
           loc := Some loc';
-          (match tac with (* update interpreter history *)
-          | TacticAst.Command (TacticAst.Qed None) ->
-              history := `Qed :: !history
-          | TacticAst.Command (TacticAst.Theorem (_, Some name, _, None)) ->
-              history := `Theorem name :: !history
-          | TacticAst.Command (TacticAst.Qed _)
-          | TacticAst.Command (TacticAst.Theorem _) -> assert false
-          | _ -> history := `Tactic :: !history);
           tactical
       | _ -> assert false
 
     method virtual evalTactical:
       (CicAst.term, string) TacticAst.tactical -> outcome
 
+    method private _evalTactical ast =
+      self#setLastItem None;
+      let res = self#evalTactical ast in
+      (match !evalAstCallback with Some f -> f ast | None -> ());
+      res
+
     method evalPhrase s =
       debug_print (sprintf "evaluating '%s'" s);
-      self#evalTactical (self#parsePhrase (Stream.of_string s))
+      self#_evalTactical (self#parsePhrase (Stream.of_string s))
 
-    method evalAst ast = self#evalTactical ast
+    method evalAst ast = self#_evalTactical ast
 
     method endOffset =
       match !loc with
       | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum
       | None -> failwith "MatitaInterpreter: no offset recorded"
 
+    method lastItem: script_item option = !last_item
+    method private setLastItem item = last_item := item
+
+    method setEvalAstCallback f = evalAstCallback := Some f
+
   end
 
   (** Implements phrases that should be accepted in all states *)
@@ -380,6 +384,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () =
           let uri = UriManager.uri_of_string (qualify name ^ ".con") in
           let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in
           currentProof#start proof;
+          self#setLastItem (Some `Theorem);
           New_state Proof
       | TacticAst.Command
         (TacticAst.Theorem (_, Some name, type_ast, Some body_ast)) ->
@@ -399,6 +404,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () =
           let body = CicMetaSubst.apply_subst subst body_cic in
           let ty = CicMetaSubst.apply_subst subst type_cic in
           add_constant_to_world ~console ~dbd ~uri ~body ~ty ~ugraph ();
+          self#setLastItem (Some (`Def uri));
           Quiet
       | TacticAst.Command (TacticAst.Inductive (params, indTypes)) ->
           
@@ -412,6 +418,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () =
           in
           add_inductive_def_to_world ~console
             ~dbd ~uri ~indTypes ~params ~leftno ~ugraph ();
+          self#setLastItem (Some (`Inductive uri));
           Quiet
       | TacticAst.Command TacticAst.Quit ->
           currentProof#quit ();
@@ -471,8 +478,7 @@ class commandState ~(console: #MatitaTypes.console) ?mathViewer () =
                   UriManager.uri_of_string (base ^ xp)
             | Cic.Appl (he::_) -> uri_of_term he
             | t -> 
-                prerr_endline ("Fallisco a estrarre la uri di " ^ 
-                  (CicPp.ppterm t));
+                error ("can't extract uri from " ^ (CicPp.ppterm t));
                 assert false 
           in
           let ty_src,ty_tgt = extract_last_two_p coer_ty in
@@ -605,14 +611,21 @@ class proofState ~(console: #MatitaTypes.console) ?mathViewer () =
           add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph ();
           currentProof#abort ();
           console#echo_message (sprintf "%s defined" suri);
+          self#setLastItem (Some (`Qed uri));
           New_state Command
       | TacticAst.Seq tacticals ->
-          (* TODO Zack check for proof completed at each step? *)
+          (* TODO ZACK check for proof completed at each step? *)
+          (* TODO ZACK code completely broken here: we must build logic level
+          * tacticals instead of iterating interpreter evaluation *)
+          if (List.length tacticals > 1) then
+            warning "tacticals are broken: see matitaInterpreter.ml";
           List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
+          self#setLastItem (Some `Tactic);
           New_state Proof
       | TacticAst.Tactic tactic_phrase ->
           let tactic = self#lookup_tactic tactic_phrase in
           currentProof#proof#apply_tactic tactic;
+          self#setLastItem (Some `Tactic);
           New_state Proof
       | tactical -> shared#evalTactical tactical
   end
@@ -623,9 +636,10 @@ class interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
   object (self)
     val mutable state = commandState
 
-    method reset = state <- commandState
-
-    method endOffset = state#endOffset
+    method setState (tag: [`Proof | `Command]) =
+      match tag with
+      | `Proof -> (state <- proofState)
+      | `Command -> (state <- commandState)
 
     method private updateState = function
       | New_state Command -> (state <- commandState)
@@ -643,6 +657,12 @@ class interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
 
     method evalPhrase s = self#eval (fun () -> state#evalPhrase s)
     method evalAst ast = self#eval (fun () -> state#evalAst ast)
+
+      (** {2 methods delegated to current state} *)
+
+    method endOffset = state#endOffset
+    method lastItem = state#lastItem
+    method setEvalAstCallback = state#setEvalAstCallback
   end
 
 let interpreter ~(console: #MatitaTypes.console) ?mathViewer () =