+ 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.string_of_uriref (uri,[n])
+ | _ -> failwith "Not a MutInd"