+ (** 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 ~subst:[] metasenv context name ~typ
+
+ (** Implements phrases that should be accepted only in Proof state, basically
+ * tacticals *)
+class proofState ~(console: #MatitaTypes.console) ?mathViewer () =
+ let shared = new sharedState ~console ?mathViewer () in
+ object (self)
+ inherit interpreterState ~console
+
+ method private disambiguate ast =
+ let (_, _, term, _) =
+ MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
+ in
+ term
+
+ (** tactic AST -> ProofEngineTypes.tactic *)
+ method private lookup_tactic = function
+ | TacticAst.LocatedTactic (_, tactic) -> self#lookup_tactic tactic
+ | TacticAst.Intros (_, names) -> (* TODO Zack implement intros length *)
+ PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names)
+ ()
+ | 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 (self#disambiguate term)
+ | TacticAst.Apply term -> Tactics.apply (self#disambiguate term)
+ | TacticAst.Absurd term -> Tactics.absurd (self#disambiguate term)
+ | TacticAst.Exact term -> Tactics.exact (self#disambiguate term)
+ | TacticAst.Cut term -> Tactics.cut (self#disambiguate term)
+ | TacticAst.Elim (term, _) -> (* TODO Zack implement "using" argument *)
+ Tactics.elim_intros_simpl (self#disambiguate term)
+ | TacticAst.ElimType term -> Tactics.elim_type (self#disambiguate term)
+ | TacticAst.Replace (what, with_what) ->
+ Tactics.replace ~what:(self#disambiguate what)
+ ~with_what:(self#disambiguate with_what)
+ | TacticAst.Auto -> Tactics.auto_new ~dbd
+ | TacticAst.Hint ->
+ let l = List.map fst
+ (MetadataQuery.experimental_hint ~dbd
+ (currentProof#proof#proof,currentProof#proof#goal))
+ in
+ let u = console#choose_uri l in
+ Tactics.apply (CicUtil.term_of_uri u)
+ | TacticAst.Change (what, with_what, _) ->
+ let what = self#disambiguate what in
+ let with_what = self#disambiguate with_what in
+ Tactics.change ~what ~with_what
+ (*
+ (* TODO Zack a lot more of tactics to be implemented here ... *)
+ | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
+ | TacticAst.Change of 'term * '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"
+
+ method evalTactical = function
+ | TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
+ | TacticAst.Command TacticAst.Abort ->
+ currentProof#abort ();
+ New_state Command
+ | TacticAst.Command (TacticAst.Undo steps) ->
+ currentProof#proof#undo ?steps ();
+ New_state Proof
+ | TacticAst.Command (TacticAst.Redo steps) ->
+ currentProof#proof#redo ?steps ();
+ New_state Proof
+ | TacticAst.Command (TacticAst.Qed None) ->
+ if not (currentProof#onGoing ()) then assert false;
+ let proof = currentProof#proof in
+ let (uri, metasenv, bo, ty) = proof#proof in
+ let uri = MatitaTypes.unopt_uri uri in
+ let suri = UriManager.string_of_uri uri in
+ (* TODO Zack this function probably should not simply fail with
+ * Failure, but rather raise some more meaningful exception *)
+ if metasenv <> [] then failwith "Proof not completed";
+ let proved_ty,ugraph =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
+ in
+ let b,ugraph =
+ CicReduction.are_convertible [] proved_ty ty ugraph
+ in
+ if not b then failwith "Wrong proof";
+ add_constant_to_world ~console ~dbd ~uri ~body:bo ~ty ~ugraph ();
+ currentProof#abort ();
+ console#echo_message (sprintf "%s defined" suri);
+ self#setLastItem (Some (`Qed uri));
+ New_state Command
+ | TacticAst.Seq tacticals ->
+ (* TODO ZACK check for proof completed at each step? *)
+ (* TODO ZACK code completely broken here: we must build logic level
+ * tacticals instead of iterating interpreter evaluation *)
+ if (List.length tacticals > 1) then
+ warning "tacticals are broken: see matitaInterpreter.ml";
+ List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
+ self#setLastItem (Some `Tactic);
+ New_state Proof
+ | TacticAst.Tactic tactic_phrase ->
+ let tactic = self#lookup_tactic tactic_phrase in
+ currentProof#proof#apply_tactic tactic;
+ self#setLastItem (Some `Tactic);
+ New_state Proof
+ | tactical -> shared#evalTactical tactical
+ end
+
+class interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
+ let commandState = new commandState ~console ?mathViewer () in
+ let proofState = new proofState ~console ?mathViewer () in
+ object (self)
+ val mutable state = commandState
+
+ method setState (tag: [`Proof | `Command]) =
+ match tag with
+ | `Proof -> (state <- proofState)
+ | `Command -> (state <- commandState)
+
+ method endOffset = state#endOffset
+
+ method private updateState = function
+ | New_state Command -> (state <- commandState)
+ | New_state Proof -> (state <- proofState)
+ | _ -> ()
+
+ method private eval f =
+ let ok () = (* console#clear (); *) (true, true) in
+ match console#wrap_exn f with
+ | Some (New_state Command) -> (state <- commandState); ok ()
+ | Some (New_state Proof) -> (state <- proofState); ok ()
+ | Some (Echo msg) -> console#echo_message msg; (true, false)
+ | Some Quiet -> ok ()
+ | None -> (false, false)
+
+ method evalPhrase s = self#eval (fun () -> state#evalPhrase s)
+ method evalAst ast = self#eval (fun () -> state#evalAst ast)
+
+ (** {2 methods delegated to current state} *)
+
+ method endOffset = state#endOffset
+ method lastItem = state#lastItem
+ method setEvalAstCallback = state#setEvalAstCallback
+ end
+
+let interpreter ~(console: #MatitaTypes.console) ?mathViewer () =
+ new interpreter ~console ?mathViewer ()
+