X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=d5ca65d22bebddf4dddaf3aa131bc807e1703b93;hb=6b7f04b45232e6c690cacf5815c85c39de1f52b3;hp=2f475f748f2246640072175e7648c615fd83af71;hpb=1fa0472bfe2ed04c7adf166fa48df687f0022226;p=helm.git diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 2f475f748..d5ca65d22 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 @@ -48,8 +84,14 @@ 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.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 +104,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 +138,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 +179,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 *) @@ -144,34 +188,33 @@ 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) (* (* 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 +233,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 @@ -218,16 +284,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 - | `Command -> state <- commandState - | `Proof -> state <- proofState) + 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