+ 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
+ (* we remove the defined object since we consider them "automathic aliases" *)
+ let new_aliases =
+ let module DTE = DisambiguateTypes.Environment in
+ let module UM = UriManager in
+ DTE.fold (
+ fun k ((v,_) as value) acc ->
+ let b =
+ try
+ let v = UM.strip_xpointer (UM.uri_of_string v) in
+ List.exists (fun (s,_) -> s = v) new_status.objects
+ with UM.IllFormedUri _ -> false
+ in
+ if b then
+ acc
+ else
+ DTE.add k value acc
+ ) new_aliases DTE.empty
+ 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
+
+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
+ | 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
+ | 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
+ | TA.WElim (loc, term) ->
+ let term = disambiguate term status in
+ let uri =
+ match term with
+ | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
+ | _ -> 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
+ | 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
+ (* 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
+ | [uri] ->
+ let ast =
+ (TA.Executable (loc,
+ (TA.Tactical (loc,
+ TA.Tactic (loc,
+ TA.Apply (loc, CicAst.Uri (UriManager.string_of_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
+ | _ ->
+ MatitaLog.error
+ "The result of the urichooser should be only 1 uri, not:\n";
+ List.iter (
+ fun u -> MatitaLog.error (UriManager.string_of_uri u ^ "\n")
+ ) selected;
+ 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