snapshot, notably history no longer remember annotations: they are

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 45332107fd0efdc06c5b813c0bb7b8a6bae3cb0b..3e505c28e1b1b18bdcfc35171100b79567cc0413 100644 (file)
--- 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
@@ -83,11 +86,10 @@ class virtual interpreterState ~(console: MatitaConsole.console) =
     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 +108,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 +137,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 +200,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 +212,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 +241,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;