| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
| GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,depth,width,paramodulation) ->
- AutoTactic.auto_tac ?depth ?width ?paramodulation
+ | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
+ AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
~dbd:(MatitaDb.instance ()) ()
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
let cic = disambiguate_term status_ref term in
GrafiteAst.Apply (loc, cic)
| GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,depth,width,paramodulation) ->
- GrafiteAst.Auto (loc,depth,width,paramodulation)
+ | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
+ GrafiteAst.Auto (loc,depth,width,paramodulation,full)
| GrafiteAst.Change (loc, pattern, with_what) ->
let with_what = disambiguate_lazy_term status_ref with_what in
let pattern = disambiguate_pattern status_ref pattern in
) status projections
(* to avoid a long list of recursive functions *)
-let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
+let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
let disambiguate_obj status obj =
let uri =
with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
;;
-let profiler_include = HExtlib.profile "include"
-
let eval_command opts status cmd =
let status,cmd = disambiguate_command status cmd in
let cmd,notation_ids' = CicNotation.process_notation cmd in
| GrafiteAst.Include (loc, path) ->
let absolute_path = make_absolute opts.include_paths path in
let moopath = MatitaMisc.obj_file_of_script absolute_path in
- let ic =
- try open_in moopath with Sys_error _ ->
- raise (IncludedFileNotCompiled moopath) in
- let stream = Ulexing.from_utf8_channel ic in
let status = ref status in
- profiler_include.HExtlib.profile
- (!eval_from_stream_ref status stream) (fun _ _ -> ());
- close_in ic;
- !status
+ if not (Sys.file_exists moopath) then
+ raise (IncludedFileNotCompiled moopath);
+ !eval_from_moo_ref status moopath (fun _ _ -> ());
+ !status
| GrafiteAst.Set (loc, name, value) ->
let value =
if name = "baseuri" then
let name = UriManager.name_of_uri uri in
let obj = Cic.Constant (name,Some bo,ty,[],[]) in
MatitaSync.add_obj uri obj status
- | GrafiteAst.Coercion (loc, coercion) ->
- eval_coercion status coercion
+ | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion
| GrafiteAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
| GrafiteAst.Executable (_,ex) -> eval_executable opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c
+let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname
+ cb
+=
+ let moo = MatitaMoo.load_moo fname in
+ List.iter
+ (fun ast ->
+ let ast =
+ GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
+ GrafiteAst.Command (DisambiguateTypes.dummy_floc,
+ (GrafiteAst.reash_cmd_uris ast)))
+ in
+ cb !status ast;
+ status :=
+ eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
+ moo
+
let eval_from_stream
?do_heavy_checks ?include_paths ?clean_baseuri status str cb
=
while true do
let ast = GrafiteParser.parse_statement str in
cb !status ast;
- status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
+ status :=
+ eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast
done
with End_of_file -> ()
(* to avoid a long list of recursive functions *)
-let _ = eval_from_stream_ref := eval_from_stream
+let _ = eval_from_moo_ref := eval_from_moo
let eval_from_stream_greedy
?do_heavy_checks ?include_paths ?clean_baseuri status str cb