open Printf
-open GrafiteTypes
-
let debug = false ;;
let debug_print = if debug then prerr_endline else ignore ;;
-let eval_from_stream
- ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+let disambiguate_command lexicon_status_ref status cmd =
+ let lexicon_status,metasenv,cmd =
+ GrafiteDisambiguate.disambiguate_command
+ ~baseuri:(
+ try
+ Some (GrafiteTypes.get_string_option status "baseuri")
+ with
+ GrafiteTypes.Option_error _ -> None)
+ !lexicon_status_ref (GrafiteTypes.get_proof_metasenv status) cmd
+ in
+ lexicon_status_ref := lexicon_status;
+ GrafiteTypes.set_metasenv metasenv status,cmd
+
+let disambiguate_tactic lexicon_status_ref status goal tac =
+ let metasenv,tac =
+ GrafiteDisambiguate.disambiguate_tactic
+ lexicon_status_ref
+ (GrafiteTypes.get_proof_context status goal)
+ (GrafiteTypes.get_proof_metasenv status)
+ tac
+ in
+ GrafiteTypes.set_metasenv metasenv status,tac
+
+let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
+ status ast
=
- try
- while true do
- let ast = GrafiteParser.parse_statement str in
- cb !status ast;
- status :=
- GrafiteEngine.eval_ast
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
- done
- with End_of_file -> ()
+ let lexicon_status_ref = ref lexicon_status in
+ let status,new_objs =
+ GrafiteEngine.eval_ast
+ ~disambiguate_tactic:(disambiguate_tactic lexicon_status_ref)
+ ~disambiguate_command:(disambiguate_command lexicon_status_ref)
+ ?do_heavy_checks ?clean_baseuri status ast
+ in
+ let lexicon_status =
+ LexiconSync.add_aliases_for_objs !lexicon_status_ref new_objs
+ in
+ lexicon_status,status
-let eval_from_stream_greedy
- ?do_heavy_checks ?include_paths ?clean_baseuri status str cb
+let eval_from_stream ~include_paths ?(prompt=false) ?do_heavy_checks
+ ?clean_baseuri lexicon_status status str cb
=
- while true do
- print_string "matita> ";
- flush stdout;
- let ast = GrafiteParser.parse_statement str in
- cb !status ast;
- status :=
- GrafiteEngine.eval_ast
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
- done
+ let rec loop lexicon_status status =
+ if prompt then (print_string "matita> "; flush stdout);
+ try
+ let lexicon_status,ast = GrafiteParser.parse_statement ~include_paths str lexicon_status in
+ (match ast with
+ GrafiteParser.LNone _ -> loop lexicon_status status
+ | GrafiteParser.LSome ast ->
+ cb status ast;
+ let lexicon_status,status =
+ eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status status ast
+ in
+ loop lexicon_status status)
+ with
+ End_of_file -> lexicon_status,status
+in
+ loop lexicon_status status
;;
-let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
- eval_from_stream
- ?do_heavy_checks ?include_paths ?clean_baseuri status
- (Ulexing.from_utf8_string str) (fun _ _ -> ())
-
-let default_options () = no_options
-
-let initial_status =
- lazy {
- aliases = DisambiguateTypes.Environment.empty;
- multi_aliases = DisambiguateTypes.Environment.empty;
- moo_content_rev = [], [];
- proof_status = No_proof;
- options = default_options ();
- objects = [];
- coercions = [];
- notation_ids = [];
- }
-
+let eval_string ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
+ status str
+=
+ eval_from_stream ~include_paths ?do_heavy_checks ?clean_baseuri lexicon_status
+ status (Ulexing.from_utf8_string str) (fun _ _ -> ())