+ let disambiguate ast =
+ let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
+ term
+ in
+ (** 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 -> 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) ->
+ Tactics.replace ~what:(disambiguate what)
+ ~with_what:(disambiguate with_what)
+ | TacticAst.Auto -> Tactics.auto_new ~dbd
+ (*
+ (* 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 None) ->
+ (* 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
+ 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;
+ (MatitaMathView.proof_viewer_instance ())#unload;
+ (* 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