X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=3e505c28e1b1b18bdcfc35171100b79567cc0413;hb=c73f6a661af7adbf91370232b555f31d413ce6ac;hp=f5dd123f53ef6a18c6e29a43c7a9587621d7888e;hpb=4cf419a2e770f4971be7b03b1d73e585d973dc1b;p=helm.git diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index f5dd123f5..3e505c28e 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -23,11 +23,56 @@ * http://helm.cs.unibo.it/ *) +(** Interpreter for textual phrases coming from matita's console (textual entry +* window at the bottom of the main window). +* +* Interpreter is either in `Command state or in `Proof state (see state_tag type +* below). In `Command state commands for starting proofs are accepted, but +* tactic and tactical applications are not. In `Proof state both +* tactic/tacticals and commands are accepted. +*) + 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) -exception Command_not_found of string +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) @@ -41,64 +86,193 @@ 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) + ~(proof_handler: MatitaTypes.proof_handler) + ~(console: MatitaConsole.console) + () += + object (self) + inherit interpreterState ~console + method evalTactical = function + | TacticAst.Command TacticAst.Quit -> + proof_handler.MatitaTypes.quit (); + Some `Command (* dummy answer, useless *) + | TacticAst.Command TacticAst.Proof -> + (* do nothing, just for compatibility with coq syntax *) + 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 + + (** Implements phrases that should be accepted only in `Command state *) class commandState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) () = + let shared = new sharedState ~disambiguator ~proof_handler ~console () in object (self) inherit interpreterState ~console method evalTactical = function -(* - | TacticAst.Command _ -> failwith "1" - | TacticAst.Tactic _ -> failwith "2" - | TacticAst.LocatedTactical _ -> failwith "3" - | TacticAst.Fail -> failwith "4" - | TacticAst.Do (_, _) -> failwith "5" - | TacticAst.IdTac -> failwith "6" - | TacticAst.Repeat _ -> failwith "7" - | TacticAst.Seq _ -> failwith "8" - | TacticAst.Then (_, _) -> failwith "9" - | TacticAst.Tries _ -> failwith "10" - | TacticAst.Try _ -> failwith "11" -*) | 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 _ = CicTypeChecker.type_of_aux' metasenv [] expr 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 - | tactical -> - raise (Command_not_found (TacticAstPp.pp_tactical tactical)) + Some `Command + | tactical -> shared#evalTactical tactical end + (** 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 *) +let namer_of names = + let len = List.length names in + let count = ref 0 in + fun metasenv context name ~typ -> + if !count < len then begin + let name = Cic.Name (List.nth names !count) in + incr count; + name + end else + FreshNamesGenerator.mk_fresh_name metasenv context name ~typ + + (** Implements phrases that should be accepted only in `Proof state, basically + * tacticals *) class proofState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) () = - let commandState = - new commandState ~disambiguator ~proof_handler ~console () + let disambiguate ast = + let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in + term in - object + (** tactic AST -> ProofEngineTypes.tactic *) + let rec lookup_tactic = function + | 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.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) -> + EqualityTactics.replace_tac ~what:(disambiguate what) + ~with_what:(disambiguate with_what) + (* + (* TODO Zack a lot more of tactics to be implemented here ... *) + | 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.Fold of reduction_kind * 'term + | TacticAst.Injection of 'ident + | TacticAst.LetIn of 'term * 'ident + | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option + | TacticAst.Replace_pattern of 'term pattern * 'term + | TacticAst.Rewrite of direction * 'term * 'ident option + *) + | _ -> + MatitaTypes.not_implemented "some tactic" + in + let shared = new sharedState ~disambiguator ~proof_handler ~console () in + object (self) inherit interpreterState ~console method evalTactical = function + | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical | TacticAst.Command TacticAst.Abort -> + proof_handler.MatitaTypes.abort_proof (); + Some `Command + | TacticAst.Command (TacticAst.Undo steps) -> + (proof_handler.MatitaTypes.get_proof ())#undo ?steps (); + Some `Proof + | 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; - `Command - | tactical -> (* fallback on command state *) - commandState#evalTactical tactical + (* 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; + Some `Proof + | TacticAst.Tactic tactic_phrase -> + let tactic = lookup_tactic tactic_phrase in + (proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic; + Some `Proof + | tactical -> shared#evalTactical tactical end class interpreter @@ -114,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))