+ A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))))
+
+let eval_with_engine status user_goal parsed_text st =
+ let module TA = TacticAst in
+ let module TAPp = TacticAstPp in
+ let parsed_text_length = String.length parsed_text in
+ let loc, ex =
+ match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false
+ in
+ let goal_changed = ref false in
+ let status =
+ match status.proof_status with
+ | Incomplete_proof (_, goal) when goal <> user_goal ->
+ goal_changed := true;
+ MatitaEngine.eval_ast status (goal_ast user_goal)
+ | _ -> status
+ in
+ let new_status = MatitaEngine.eval_ast status st in
+ let new_aliases =
+ match ex with
+ | TA.Command (_, TA.Alias _) ->
+ DisambiguateTypes.Environment.empty
+ | _ -> MatitaSync.alias_diff ~from:status new_status
+ in
+ let new_text =
+ if DisambiguateTypes.Environment.is_empty new_aliases then
+ parsed_text
+ else
+ prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases)
+ parsed_text
+ in
+ let new_text =
+ if !goal_changed then
+ prepend_text
+ (TAPp.pp_tactic (TA.Goal (loc, user_goal))(* ^ "\n"*))
+ new_text
+ else
+ new_text
+ in
+ [ new_status, new_text ], parsed_text_length, None
+
+let disambiguate term status =
+ let module MD = MatitaDisambiguator in
+ let dbd = MatitaDb.instance () in
+ let metasenv = MatitaMisc.get_proof_metasenv status in
+ let context = MatitaMisc.get_proof_context status in
+ let aliases = MatitaMisc.get_proof_aliases status in
+ let interps = MD.disambiguate_term dbd context metasenv aliases term in
+ match interps with
+ | [_,_,x,_] -> x
+ | _ -> assert false
+
+let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text
+script mac =
+ let module TA = TacticAst in
+ let module TAPp = TacticAstPp in
+ let module MQ = MetadataQuery in
+ let module MDB = MatitaDb in
+ let module CTC = CicTypeChecker in
+ let module CU = CicUniv in
+ (* no idea why ocaml wants this *)
+ let advance ?statement () = script#advance ?statement () in
+ let parsed_text_length = String.length parsed_text in
+ let dbd = MatitaDb.instance () in
+ match mac with
+ (* WHELP's stuff *)
+ | TA.WMatch (loc, term) ->
+ let term = disambiguate term status in
+ let l = MQ.match_term ~dbd term in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in
+ mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length, None
+ | TA.WInstance (loc, term) ->
+ let term = disambiguate term status in
+ let l = MQ.instance ~dbd term in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+ mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length, None
+ | TA.WLocate (loc, s) ->
+ let l = MQ.locate ~dbd s in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+ mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length, None
+ | TA.WElim (loc, term) ->
+ let term = disambiguate term status in
+ let uri =
+ match term with
+ | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n])
+ | _ -> failwith "Not a MutInd"
+ in
+ let l = MQ.elim ~dbd uri in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
+ mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length, None
+ | TA.WHint (loc, term) ->
+ let term = disambiguate term status in
+ let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+ let l = List.map fst (MQ.experimental_hint ~dbd s) in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
+ mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length, None
+ (* REAL macro *)
+ | TA.Hint loc ->
+ let s = MatitaMisc.get_proof_status status in
+ let l = List.map fst (MQ.experimental_hint ~dbd s) in
+ let selected = urichooser l in
+ (match selected with
+ | [] -> [], parsed_text_length, None
+ | [uri] ->
+ let ast =
+ (TA.Executable (loc,
+ (TA.Tactical (loc,
+ TA.Tactic (loc,
+ TA.Apply (loc, CicAst.Uri (uri,None)))))))
+ in
+ let new_status = MatitaEngine.eval_ast status ast in
+ let extra_text =
+ comment parsed_text ^
+ "\n" ^ TAPp.pp_statement ast
+ in
+ [ new_status , extra_text ], parsed_text_length, None
+ | _ -> assert false)
+ | TA.Check (_,term) ->
+ let metasenv = MatitaMisc.get_proof_metasenv status in
+ let context = MatitaMisc.get_proof_context status in
+ let aliases = MatitaMisc.get_proof_aliases status in
+ let interps =
+ MatitaDisambiguator.disambiguate_term
+ dbd context metasenv aliases term