X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=3e505c28e1b1b18bdcfc35171100b79567cc0413;hb=c73f6a661af7adbf91370232b555f31d413ce6ac;hp=2f475f748f2246640072175e7648c615fd83af71;hpb=1fa0472bfe2ed04c7adf166fa48df687f0022226;p=helm.git diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 2f475f748..3e505c28e 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -34,10 +34,46 @@ open Printf -type state_tag = [ `Command | `Proof ] + (** 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 canonical_context metano metasenv = + try + let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in + context + with Not_found -> + failwith (sprintf "Can't find canonical context for %d" metano) + +let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) = + if proof_handler.MatitaTypes.has_proof () then + let proof = proof_handler.MatitaTypes.get_proof () in + let metasenv = proof#metasenv in + let goal = proof#goal in + (canonical_context goal metasenv, metasenv) + else + ([], []) + + (** term AST -> Cic.term. Uses disambiguator and change imperatively the + * metasenv as needed *) +let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast = + if proof_handler.MatitaTypes.has_proof () then begin + let proof = proof_handler.MatitaTypes.get_proof () in + let metasenv = proof#metasenv in + let goal = proof#goal in + let context = canonical_context goal metasenv in + let (_, metasenv, term) as retval = + disambiguator#disambiguateTermAst ~context ~metasenv ast + in + proof#set_metasenv metasenv; + retval + end else + disambiguator#disambiguateTermAst ast + class virtual interpreterState ~(console: MatitaConsole.console) = object (self) (** eval a toplevel phrase in the current state and return the new state @@ -50,6 +86,11 @@ class virtual interpreterState ~(console: MatitaConsole.console) = method evalPhrase s = self#evalTactical (self#parsePhrase s) end +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 ~(disambiguator: MatitaTypes.disambiguator) @@ -62,10 +103,23 @@ class sharedState method evalTactical = function | TacticAst.Command TacticAst.Quit -> proof_handler.MatitaTypes.quit (); - `Command (* dummy answer, useless *) + Some `Command (* dummy answer, useless *) | TacticAst.Command TacticAst.Proof -> (* do nothing, just for compatibility with coq syntax *) - `Command + Some `Command + | TacticAst.Command (TacticAst.Check term) -> + let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in + let (context, metasenv) = get_context_and_metasenv proof_handler 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#load_sequent (sequent::metasenv) dummyno; + None | tactical -> raise (Command_error (TacticAstPp.pp_tactical tactical)) end @@ -83,27 +137,25 @@ 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; - `Proof + Some `Proof | TacticAst.Command TacticAst.Quit -> proof_handler.MatitaTypes.quit (); - `Command (* dummy answer, useless *) + Some `Command (* dummy answer, useless *) | TacticAst.Command TacticAst.Proof -> (* do nothing, just for compatibility with coq syntax *) - `Command + Some `Command | tactical -> shared#evalTactical tactical end -let canonical_context metano metasenv = - try - let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in - context - with Not_found -> - failwith (sprintf "Can't find canonical context for %d" metano) - (** create a ProofEngineTypes.mk_fresh_name_type function which uses given * names as long as they are available, then it fallbacks to name generation * using FreshNamesGenerator module *) @@ -126,17 +178,8 @@ class proofState ~(console: MatitaConsole.console) () = - (** term AST -> Cic.term. Uses disambiguator and change imperatively the - * metasenv as needed *) let disambiguate ast = - let proof = proof_handler.MatitaTypes.get_proof () in - let metasenv = proof#metasenv in - let goal = proof#goal in - let context = canonical_context goal metasenv in - let (_, metasenv, term) = - disambiguator#disambiguateTermAst ~context ~metasenv ast - in - proof#set_metasenv metasenv; + let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in term in (** tactic AST -> ProofEngineTypes.tactic *) @@ -157,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) -> @@ -166,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 @@ -190,21 +234,44 @@ class proofState | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command TacticAst.Abort -> proof_handler.MatitaTypes.abort_proof (); - `Command + Some `Command | TacticAst.Command (TacticAst.Undo steps) -> (proof_handler.MatitaTypes.get_proof ())#undo ?steps (); - `Proof + Some `Proof | TacticAst.Command (TacticAst.Redo steps) -> (proof_handler.MatitaTypes.get_proof ())#redo ?steps (); - `Proof + 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; - `Proof + Some `Proof | TacticAst.Tactic tactic_phrase -> let tactic = lookup_tactic tactic_phrase in (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic; - `Proof + Some `Proof | tactical -> shared#evalTactical tactical end @@ -221,11 +288,14 @@ class interpreter object val mutable state = commandState + method reset = state <- commandState + method evalPhrase s = try (match state#evalPhrase s with - | `Command -> state <- commandState - | `Proof -> state <- proofState) + | Some `Command -> state <- commandState + | Some `Proof -> state <- proofState + | None -> ()) with exn -> console#echo_error (sprintf "Uncaught exception: %s" (Printexc.to_string exn))