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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 45332107f..17a055174 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -39,6 +39,9 @@ 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 canonical_context metano metasenv =
   try
     let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
@@ -81,13 +84,13 @@ class virtual interpreterState ~(console: MatitaConsole.console) =
       (CicAst.term, string) TacticAst.tactical -> state_tag
 
     method evalPhrase s = self#evalTactical (self#parsePhrase s)
+
   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
@@ -106,18 +109,17 @@ class sharedState
             (* do nothing, just for compatibility with coq syntax *)
           Some `Command
       | 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))
@@ -136,9 +138,14 @@ class commandState
 
     method evalTactical = function
       | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
-      | TacticAst.Command (TacticAst.Theorem (_, Some name, ast, None)) ->
+      | TacticAst.Command (TacticAst.Theorem (_, name_opt, ast, None)) ->
           let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
-          let proof = MatitaProof.proof ~typ:expr ~metasenv () in
+          let uri =
+            match name_opt with
+            | None -> None
+            | Some name -> Some (uri name)
+          in
+          let proof = MatitaProof.proof ~typ:expr ?uri ~metasenv () in
           proof_handler.MatitaTypes.new_proof proof;
           Some `Proof
       | TacticAst.Command TacticAst.Quit ->
@@ -194,8 +201,11 @@ class proofState
     | TacticAst.Transitivity term ->
         EqualityTactics.transitivity_tac (disambiguate term)
     | TacticAst.Apply term -> PrimitiveTactics.apply_tac (disambiguate term)
+    | TacticAst.Absurd term -> NegationTactics.absurd_tac (disambiguate term)
     | TacticAst.Exact term -> PrimitiveTactics.exact_tac (disambiguate term)
     | TacticAst.Cut term -> PrimitiveTactics.cut_tac (disambiguate term)
+    | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
+        PrimitiveTactics.elim_intros_simpl_tac (disambiguate term)
     | TacticAst.ElimType term ->
         EliminationTactics.elim_type_tac (disambiguate term)
     | TacticAst.Replace (what, with_what) ->
@@ -203,12 +213,10 @@ class proofState
           ~with_what:(disambiguate with_what)
   (*
     (* 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 +242,29 @@ class proofState
       | TacticAst.Command (TacticAst.Redo steps) ->
           (proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
           Some `Proof
+      | TacticAst.Command (TacticAst.Qed name_opt) ->
+          (* 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
+          (match name_opt with
+          | None -> ()
+          | Some name -> proof#set_uri (uri name));
+          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;
+          (* 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;
@@ -255,19 +286,39 @@ class interpreter
     new commandState ~disambiguator ~proof_handler ~console ()
   in
   let proofState = new proofState ~disambiguator ~proof_handler ~console () in
-  object
+  object (self)
     val mutable state = commandState
 
     method reset = state <- commandState
 
+    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 -> ())
+        self#updateState (state#evalPhrase s)
       with exn ->
         console#echo_error (sprintf "Uncaught exception: %s"
           (Printexc.to_string exn))
+
+(*
+    method evalAll s =
+      let get_end_pos = function
+        | TacticAst.LocatedTactical ((_, end_pos), _) -> end_pos.Lexing.pos_cnum
+        | _ -> assert false
+      in
+      let str_len = String.length s in
+      let rec aux offset =
+        let tactical =
+          self#parsePhrase (String.sub s offset (str_len - offset))
+        in
+        self#updateState (state#evalTactical tactical);
+        let next_offset = get_end_pos tactical + offset in
+        if next_offset = str_len - 1 then
+      in
+*)
+
   end