+module TA = GrafiteAst
+
+let debug = false
+let debug_print = if debug then prerr_endline else ignore
+
+ (** raised when one of the script margins (top or bottom) is reached *)
+exception Margin
+
+let safe_substring s i j =
+ try String.sub s i j with Invalid_argument _ -> assert false
+
+let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
+let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)((.|\n)*)"
+let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
+let multiline_RE = Pcre.regexp "^\n[^\n]+$"
+let newline_RE = Pcre.regexp "\n"
+
+let comment str =
+ if Pcre.pmatch ~rex:multiline_RE str then
+ "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " *)"
+ else
+ "\n(**\n" ^ str ^ "\n*)"
+
+let first_line s =
+ let s = Pcre.replace ~rex:heading_nl_RE s in
+ try
+ let nl_pos = String.index s '\n' in
+ String.sub s 0 nl_pos
+ with Not_found -> s
+
+ (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
+let goal_ast n =
+ let module A = GrafiteAst in
+ let loc = DisambiguateTypes.dummy_floc in
+ A.Executable (loc, A.Tactical (loc,
+ A.Tactic (loc, A.Goal (loc, n)),
+ Some (A.Dot loc)))
+
+type guistuff = {
+ mathviewer:MatitaTypes.mathViewer;
+ urichooser: UriManager.uri list -> UriManager.uri list;
+ ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
+ develcreator: containing:string option -> unit;
+ mutable filenamedata: string option * MatitamakeLib.development option
+}
+
+let eval_with_engine guistuff status user_goal parsed_text st =
+ let module TAPp = GrafiteAstPp in
+ let include_ =
+ match guistuff.filenamedata with
+ | None,None -> []
+ | None,Some devel -> [MatitamakeLib.root_for_development devel ]
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel ]
+ 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 initial_space,parsed_text =
+ try
+ let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
+ pieces.(1), pieces.(2)
+ with
+ Not_found -> "", parsed_text in
+ (* we add the goal command if needed *)
+ let inital_space,new_status,new_status_and_text_list' =
+ match status.proof_status with
+(* | Incomplete_proof { stack = stack }
+ when not (List.mem user_goal (Continuationals.head_goals stack)) ->
+ let status =
+ MatitaEngine.eval_ast
+ ~do_heavy_checks:true status (goal_ast user_goal)
+ in
+ let initial_space = if initial_space = "" then "\n" else initial_space
+ in
+ "\n", status,
+ [ status,
+ initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *)
+ | _ -> initial_space,status,[] in
+ let new_status =
+ GrafiteEngine.eval_ast
+ ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
+ ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
+ ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
+ ~do_heavy_checks:true new_status st
+ in
+ let new_aliases =
+ match ex with
+ | TA.Command (_, TA.Alias _)
+ | TA.Command (_, TA.Include _)
+ | TA.Command (_, TA.Interpretation _) -> []
+ | _ -> MatitaSync.alias_diff ~from:status new_status
+ in
+ (* we remove the defined object since we consider them "automatic aliases" *)
+ let dummy_st =
+ TA.Comment (DisambiguateTypes.dummy_floc,
+ TA.Note (DisambiguateTypes.dummy_floc, ""))
+ in
+ let initial_space,status,new_status_and_text_list_rev =
+ let module DTE = DisambiguateTypes.Environment in
+ let module UM = UriManager in
+ let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in
+ List.fold_left (
+ fun (initial_space,status,acc) (k,((v,_) as value)) ->
+ let b =
+ try
+ UM.buri_of_uri (UM.uri_of_string v) = baseuri
+ with
+ UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
+ in
+ if b then
+ initial_space,status,acc
+ else
+ let new_text =
+ let initial_space =
+ if initial_space = "" then "\n" else initial_space in
+ initial_space ^
+ DisambiguatePp.pp_environment
+ (DisambiguateTypes.Environment.add k value
+ DisambiguateTypes.Environment.empty) in
+ let new_status =
+ MatitaSync.set_proof_aliases status [k,value]
+ in
+ "\n",new_status,((new_status, (new_text, dummy_st))::acc)
+ ) (initial_space,status,[]) new_aliases in
+ let parsed_text = initial_space ^ parsed_text in
+ let res =
+ List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
+ [new_status, (parsed_text, st)]
+ in
+ res,parsed_text_length
+
+let eval_with_engine guistuff status user_goal parsed_text st =
+ try
+ eval_with_engine guistuff status user_goal parsed_text st
+ with
+ | GrafiteParserMisc.UnableToInclude what
+ | GrafiteEngine.IncludedFileNotCompiled what as exc ->
+ let compile_needed_and_go_on d =
+ let target = what in
+ let refresh_cb () =
+ while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
+ in
+ if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
+ raise exc
+ else
+ eval_with_engine guistuff status user_goal parsed_text st
+ in
+ let do_nothing () = [], 0 in
+ let handle_with_devel d =
+ let name = MatitamakeLib.name_for_development d in
+ let title = "Unable to include " ^ what in
+ let message =
+ what ^ " is handled by development <b>" ^ name ^ "</b>.\n\n" ^
+ "<i>Should I compile it and Its dependencies?</i>"
+ in
+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES -> compile_needed_and_go_on d
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing ())
+ in
+ let handle_without_devel filename =
+ let title = "Unable to include " ^ what in
+ let message =
+ what ^ " is <b>not</b> handled by a development.\n" ^
+ "All dependencies are automatically solved for a development.\n\n" ^
+ "<i>Do you want to set up a development?</i>"
+ in
+ (match guistuff.ask_confirmation ~title ~message with
+ | `YES ->
+ (match filename with
+ | Some f ->
+ guistuff.develcreator ~containing:(Some (Filename.dirname f))
+ | None -> guistuff.develcreator ~containing:None);
+ do_nothing ()
+ | `NO -> raise exc
+ | `CANCEL -> do_nothing())
+ in
+ match guistuff.filenamedata with
+ | None,None -> handle_without_devel None
+ | None,Some d -> handle_with_devel d
+ | Some f,_ ->
+ match MatitamakeLib.development_for_dir (Filename.dirname f) with
+ | None -> handle_without_devel (Some f)
+ | Some d -> handle_with_devel d
+;;
+
+let disambiguate_macro_term term status user_goal =
+ let module MD = MatitaDisambiguator in
+ let dbd = LibraryDb.instance () in
+ let metasenv = GrafiteTypes.get_proof_metasenv status in
+ let context = GrafiteTypes.get_proof_context status user_goal in
+ let interps =
+ MD.disambiguate_term ~dbd ~context ~metasenv ~aliases:status.aliases
+ ~universe:(Some status.multi_aliases) term in
+ match interps with
+ | [_,_,x,_], _ -> x
+ | _ -> assert false
+
+let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
+ let module TAPp = GrafiteAstPp in
+ let module MQ = MetadataQuery in
+ let module MDB = LibraryDb in
+ let module CTC = CicTypeChecker in
+ let module CU = CicUniv in
+ (* no idea why ocaml wants this *)
+ let parsed_text_length = String.length parsed_text in
+ let dbd = LibraryDb.instance () in
+ match mac with
+ (* WHELP's stuff *)
+ | TA.WMatch (loc, term) ->
+ let term = disambiguate_macro_term term status user_goal in
+ let l = Whelp.match_term ~dbd term in
+ let query_url =
+ MatitaMisc.strip_suffix ~suffix:"."
+ (HExtlib.trim_blanks unparsed_text)
+ in
+ let entry = `Whelp (query_url, l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WInstance (loc, term) ->
+ let term = disambiguate_macro_term term status user_goal in
+ let l = Whelp.instance ~dbd term in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WLocate (loc, s) ->
+ let l = Whelp.locate ~dbd s in
+ let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
+ | TA.WElim (loc, term) ->
+ let term = disambiguate_macro_term term status user_goal in