X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=5933f6227124a6f3709d3c90e5d7b0e551747c1e;hb=a482ae2ca1849bfe49b057411b6d0af98440e9c0;hp=45332107fd0efdc06c5b813c0bb7b8a6bae3cb0b;hpb=fd96ce8e13f4f9adbeef2d9feb32f94dfcfaadad;p=helm.git

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 45332107f..5933f6227 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -34,11 +34,26 @@
 
 open Printf
 
+open MatitaTypes
+
   (** None means: "same state as before" *)
 type state_tag = [ `Command | `Proof ] option
 
 exception Command_error of string
 
+(*
+let uri name =
+  UriManager.uri_of_string (sprintf "%s/%s" BuildTimeConf.base_uri name)
+*)
+
+let baseuri = ref "cic:/matita"
+let qualify name =
+  let baseuri = !baseuri in
+  if baseuri.[String.length baseuri - 1] = '/' then
+    baseuri ^ name
+  else
+    String.concat "/" [baseuri; name]
+
 let canonical_context metano metasenv =
   try
     let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
@@ -71,23 +86,50 @@ let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast =
   end else
     disambiguator#disambiguateTermAst ast
 
-class virtual interpreterState ~(console: MatitaConsole.console) =
+class virtual interpreterState = 
+    (* static values, shared by all states inheriting this class *)
+  let loc = ref None in
+  let history = ref [] in
+  fun ~(console: MatitaConsole.console) ->
   object (self)
+
       (** eval a toplevel phrase in the current state and return the new state
       *)
-    method parsePhrase s = CicTextualParser2.parse_tactical (Stream.of_string s)
+    method parsePhrase s =
+      match CicTextualParser2.parse_tactical (Stream.of_string 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 -> state_tag
 
-    method evalPhrase s = self#evalTactical (self#parsePhrase s)
+    method evalPhrase s =
+      debug_print (sprintf "evaluating '%s'" s);
+      self#evalTactical (self#parsePhrase s)
+
+    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"
+
   end
 
-let check_widget: MatitaTypes.sequents_viewer lazy_t = lazy (
-  let gui = MatitaGui.instance () in
-  let notebook = GPack.notebook ~show:true ~packing:gui#check#checkWin#add () in
-  let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () in
-  MatitaMathView.sequents_viewer ~notebook ~sequent_viewer ())
+let check_widget: MatitaTypes.sequent_viewer lazy_t = lazy
+  (let gui = MatitaGui.instance () in
+  MatitaMathView.sequent_viewer ~show:true ~packing:gui#check#scrolledCheck#add
+    ())
 
   (** Implements phrases that should be accepted in all states *)
 class sharedState
@@ -105,19 +147,25 @@ class sharedState
       | TacticAst.Command TacticAst.Proof ->
             (* do nothing, just for compatibility with coq syntax *)
           Some `Command
+      | TacticAst.Command (TacticAst.Baseuri (Some uri)) ->
+          baseuri := uri;
+          console#echo_message (sprintf "base uri set to \"%s\"" uri);
+          None
+      | TacticAst.Command (TacticAst.Baseuri None) ->
+          console#echo_message (sprintf "base uri is \"%s\"" !baseuri);
+          None
       | TacticAst.Command (TacticAst.Check term) ->
-          let dummyno = 1023 in
           let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
           let (context, metasenv) = get_context_and_metasenv proof_handler in
-          let sequent = (dummyno, context, term) in
-          let metadata = Cic2acic.asequent_of_sequent metasenv sequent in
+          let dummyno = CicMkImplicit.new_meta metasenv [] in
+          let ty = CicTypeChecker.type_of_aux' metasenv context term in
+          let expr = Cic.Cast (term, ty) in
+          let sequent = (dummyno, context, expr) in
           let widget = Lazy.force check_widget in
           let gui = MatitaGui.instance () in
           gui#check#checkWin#show ();
           gui#main#showCheckMenuItem#set_active true;
-          widget#reset;
-          widget#load_sequents [dummyno, metadata];
-          widget#goto_sequent dummyno;
+          widget#load_sequent (sequent::metasenv) dummyno;
           None
       | tactical ->
           raise (Command_error (TacticAstPp.pp_tactical tactical))
@@ -138,7 +186,8 @@ class commandState
       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
       | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
-          let proof = MatitaProof.proof ~typ:expr ~metasenv () in
+          let uri = UriManager.uri_of_string (qualify name) in
+          let proof = MatitaProof.proof ~typ:expr ~uri ~metasenv () in
           proof_handler.MatitaTypes.new_proof proof;
           Some `Proof
       | TacticAst.Command TacticAst.Quit ->
@@ -170,6 +219,7 @@ class proofState
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
+  ~(dbd: Mysql.dbd)
   ()
 =
   let disambiguate ast =
@@ -181,34 +231,34 @@ class proofState
     | TacticAst.LocatedTactic (_, tactic) -> lookup_tactic tactic
     | TacticAst.Intros (_, names) ->  (* TODO Zack implement intros length *)
         PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
-    | TacticAst.Reflexivity -> EqualityTactics.reflexivity_tac
-    | TacticAst.Assumption -> VariousTactics.assumption_tac
-    | TacticAst.Contradiction -> NegationTactics.contradiction_tac
-    | TacticAst.Exists -> IntroductionTactics.exists_tac
-    | TacticAst.Fourier -> FourierR.fourier_tac
-    | TacticAst.Left -> IntroductionTactics.left_tac
-    | TacticAst.Right -> IntroductionTactics.right_tac
-    | TacticAst.Ring -> Ring.ring_tac
-    | TacticAst.Split -> IntroductionTactics.split_tac
-    | TacticAst.Symmetry -> EqualityTactics.symmetry_tac
-    | TacticAst.Transitivity term ->
-        EqualityTactics.transitivity_tac (disambiguate term)
-    | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
-    | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
-    | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
-    | TacticAst.ElimType term ->
-        EliminationTactics.elim_type_tac (disambiguate term)
+    | TacticAst.Reflexivity -> Tactics.reflexivity
+    | TacticAst.Assumption -> Tactics.assumption
+    | TacticAst.Contradiction -> Tactics.contradiction
+    | TacticAst.Exists -> Tactics.exists
+    | TacticAst.Fourier -> Tactics.fourier
+    | TacticAst.Left -> Tactics.left
+    | TacticAst.Right -> Tactics.right
+    | TacticAst.Ring -> Tactics.ring
+    | TacticAst.Split -> Tactics.split
+    | TacticAst.Symmetry -> Tactics.symmetry
+    | TacticAst.Transitivity term -> Tactics.transitivity (disambiguate term)
+    | TacticAst.Apply term -> Tactics.apply (disambiguate term)
+    | TacticAst.Absurd term -> Tactics.absurd (disambiguate term)
+    | TacticAst.Exact term -> Tactics.exact (disambiguate term)
+    | TacticAst.Cut term -> Tactics.cut (disambiguate term)
+    | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
+        Tactics.elim_intros_simpl (disambiguate term)
+    | TacticAst.ElimType term -> Tactics.elim_type (disambiguate term)
     | TacticAst.Replace (what, with_what) ->
-        EqualityTactics.replace_tac ~what:(disambiguate what)
+        Tactics.replace ~what:(disambiguate what)
           ~with_what:(disambiguate with_what)
+    | TacticAst.Auto -> Tactics.auto_new ~dbd
   (*
     (* TODO Zack a lot more of tactics to be implemented here ... *)
-    | TacticAst.Absurd
     | TacticAst.Change of 'term * 'term * 'ident option
     | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
     | TacticAst.Decompose of 'ident * 'ident list
     | TacticAst.Discriminate of 'ident
-    | TacticAst.Elim of 'term * 'term option
     | TacticAst.Fold of reduction_kind * 'term
     | TacticAst.Injection of 'ident
     | TacticAst.LetIn of 'term * 'ident
@@ -234,6 +284,27 @@ class proofState
       | TacticAst.Command (TacticAst.Redo steps) ->
           (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
           Some `Proof
+      | TacticAst.Command (TacticAst.Qed None) ->
+          (* TODO Zack this function probably should not simply fail with
+          * Failure, but rather raise some more meaningful exception *)
+          if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
+          let proof = proof_handler.MatitaTypes.get_proof () in
+          let (uri, metasenv, bo, ty) = proof#proof in
+          let uri = MatitaTypes.unopt_uri uri in
+          if metasenv <> [] then failwith "Proof not completed";
+          let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
+          if not (CicReduction.are_convertible [] proved_ty ty) then
+            failwith "Wrong proof";
+          (* TODO Zack [] probably wrong *)
+          CicEnvironment.add_type_checked_term uri
+            (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+          proof_handler.MatitaTypes.set_proof None;
+          (MatitaMathView.proof_viewer_instance ())#unload;
+          (* TODO Zack a lot more to be done here:
+            * - save object to disk in xml format
+            * - collect metadata
+            * - register uri to the getter *)
+          Some `Command
       | TacticAst.Seq tacticals ->
           (* TODO Zack check for proof completed at each step? *)
           List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
@@ -249,25 +320,39 @@ class interpreter
   ~(disambiguator: MatitaTypes.disambiguator)
   ~(proof_handler: MatitaTypes.proof_handler)
   ~(console: MatitaConsole.console)
+  ~(dbd: Mysql.dbd)
   ()
 =
   let commandState =
     new commandState ~disambiguator ~proof_handler ~console ()
   in
-  let proofState = new proofState ~disambiguator ~proof_handler ~console () in
-  object
+  let proofState =
+    new proofState ~disambiguator ~proof_handler ~console ~dbd ()
+  in
+  object (self)
     val mutable state = commandState
 
     method reset = state <- commandState
 
+    method endOffset = state#endOffset
+
+    method private updateState = function
+      | Some `Command -> state <- commandState
+      | Some `Proof -> state <- proofState
+      | None -> ()
+
     method evalPhrase s =
-      try
-        (match state#evalPhrase s with
-        | Some `Command -> state <- commandState
-        | Some `Proof -> state <- proofState
-        | None -> ())
-      with exn ->
-        console#echo_error (sprintf "Uncaught exception: %s"
-          (Printexc.to_string exn))
+      let success =
+        console#wrap_exn (fun () -> self#updateState (state#evalPhrase s))
+      in
+      if success then console#clear ();
+      success
+
+    method evalAst ast =
+      let success =
+        console#wrap_exn (fun () -> self#updateState (state#evalAst ast))
+      in
+      if success then console#clear ();
+      success
   end