| 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 disambiguate_term status_ref term =
let status = !status_ref in
- let (aliases, metasenv, cic, _) =
+ let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases)
~metasenv:(MatitaMisc.get_proof_metasenv status) term)
in
let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status_ref := status;
cic
let disambiguate_lazy_term status_ref term =
(fun context metasenv ugraph ->
let status = !status_ref in
- let (aliases, metasenv, cic, ugraph) =
+ let (diff, metasenv, cic, ugraph) =
singleton
(MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
~initial_ugraph:ugraph ~aliases:status.aliases
~universe:(Some status.multi_aliases) ~context ~metasenv term)
in
let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status_ref := status;
cic, metasenv, ugraph)
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
in
let ty_src,ty_tgt = extract_last_two_p coer_ty in
let context = [] in
- let src_uri =
- let ty_src = CicReduction.whd context ty_src in
- CicUtil.uri_of_term ty_src
- in
- let tgt_uri =
- let ty_tgt = CicReduction.whd context ty_tgt in
- CicUtil.uri_of_term ty_tgt
- in
+ let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_src) in
+ let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_tgt) in
let new_coercions =
- (* also adds them to the Db *)
CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
let status =
- List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
+ List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
status new_coercions in
let statement_of name =
GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
{ status with proof_status = No_proof }
let generate_elimination_principles uri status =
- let elim sort status =
- try
- let uri,obj = CicElim.elim_of ~sort uri 0 in
- MatitaSync.add_obj uri obj status
- with CicElim.Can_t_eliminate -> status
- in
- List.fold_left (fun status sort -> elim sort status) status
- [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
+ let status' = ref status in
+ let elim sort =
+ try
+ let uri,obj = CicElim.elim_of ~sort uri 0 in
+ status' := MatitaSync.add_obj uri obj !status'
+ with CicElim.Can_t_eliminate -> ()
+ in
+ try
+ List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+ !status'
+ with exn ->
+ MatitaSync.time_travel ~present:!status' ~past:status;
+ raise exn
let generate_projections uri fields status =
let projections = CicRecord.projections_of uri fields in
with
CicTypeChecker.TypeCheckerFailure s ->
MatitaLog.message
- ("Unable to create projection " ^ name ^ " cause: " ^ s);
+ ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s));
status
| CicEnvironment.Object_not_found uri ->
let depend = UriManager.name_of_uri uri 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 =
Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
| GrafiteAst.Inductive _ -> assert false
| GrafiteAst.Theorem _ -> None in
- let (aliases, metasenv, cic, _) =
+ let (diff, metasenv, cic, _) =
singleton
(MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
| Intermediate _ -> assert false
in
let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status aliases in
+ let status = MatitaSync.set_proof_aliases status diff in
status, cic
-let disambiguate_command status = function
+let disambiguate_command status =
+ function
| GrafiteAst.Alias _
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Dump _
| GrafiteAst.Include _
| GrafiteAst.Interpretation _
+ | GrafiteAst.Metadata _
| GrafiteAst.Notation _
| GrafiteAst.Qed _
| GrafiteAst.Render _
with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
;;
-let profiler_include = CicUtil.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 = Stream.of_channel ic in
let status = ref status in
- profiler_include.CicUtil.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.Metadata (loc, m) ->
+ (match m with
+ | GrafiteAst.Dependency uri -> MatitaTypes.add_moo_metadata [m] status
+ | GrafiteAst.Baseuri _ -> status)
| GrafiteAst.Set (loc, name, value) ->
- let value =
- if name = "baseuri" then
- let v = MatitaMisc.strip_trailing_slash value in
- try
- ignore (String.index v ' ');
- command_error "baseuri can't contain spaces"
- with Not_found -> v
- else
- value
+ let status =
+ if name = "baseuri" then begin
+ let value =
+ let v = MatitaMisc.strip_trailing_slash value in
+ try
+ ignore (String.index v ' ');
+ command_error "baseuri can't contain spaces"
+ with Not_found -> v
+ in
+ if not (MatitaMisc.is_empty value) && opts.clean_baseuri then begin
+ MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
+ MatitaLog.message ("cleaning baseuri " ^ value);
+ MatitacleanLib.clean_baseuris [value]
+ end;
+ add_moo_metadata [GrafiteAst.Baseuri value] status
+ end else
+ status
in
- if not (MatitaMisc.is_empty value) then
- begin
- MatitaLog.warn ("baseuri " ^ value ^ " is not empty");
- if opts.clean_baseuri then
- begin
- MatitaLog.message ("cleaning baseuri " ^ value);
- MatitacleanLib.clean_baseuris [value]
- end
- end;
set_option status name value
| GrafiteAst.Drop loc -> raise Drop
| GrafiteAst.Qed loc ->
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 aliases =
+ let diff =
(*CSC: Warning: this code should be factorized with the corresponding
code in DisambiguatePp *)
match spec with
| GrafiteAst.Ident_alias (id,uri) ->
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Id id)
- (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
- status.aliases
+ [DisambiguateTypes.Id id,
+ (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))]
| GrafiteAst.Symbol_alias (symb, instance, desc) ->
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Symbol (symb,instance))
- (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
- status.aliases
+ [DisambiguateTypes.Symbol (symb,instance),
+ DisambiguateChoices.lookup_symbol_by_dsc symb desc]
| GrafiteAst.Number_alias (instance,desc) ->
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Num instance)
- (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
+ [DisambiguateTypes.Num instance,
+ DisambiguateChoices.lookup_num_by_dsc desc]
in
- MatitaSync.set_proof_aliases status aliases
+ MatitaSync.set_proof_aliases status diff
| GrafiteAst.Render _ -> assert false (* ZACK: to be removed *)
| GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *)
- | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
- let status' = add_moo_content [stm] status in
- let aliases' =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Symbol (symbol, 0))
- (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc)
- status.aliases
+ | GrafiteAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
+ let status = add_moo_content [stm] status in
+ let uris =
+ List.map
+ (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri))
+ (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
+ in
+ let diff =
+ [DisambiguateTypes.Symbol (symbol, 0),
+ DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
in
- MatitaSync.set_proof_aliases status' aliases'
+ let status = MatitaSync.set_proof_aliases status diff in
+ let status = MatitaTypes.add_moo_metadata uris status in
+ status
| GrafiteAst.Notation _ as stm -> add_moo_content [stm] status
| GrafiteAst.Obj (loc,obj) ->
let ext,name =
command_error (
"metasenv not empty while giving a definition with body: " ^
CicMetaSubst.ppmetasenv [] metasenv);
- let status = MatitaSync.add_obj uri obj status in
- match obj with
- Cic.Constant _ -> status
+ let status' = ref status in
+ (try
+ status' := MatitaSync.add_obj uri obj !status';
+ (match obj with
+ | Cic.Constant _ -> ()
| Cic.InductiveDefinition (_,_,_,attrs) ->
- let status = generate_elimination_principles uri status in
- let rec get_record_attrs =
- function
- [] -> None
- | (`Class (`Record fields))::_ -> Some fields
- | _::tl -> get_record_attrs tl
- in
+ status' := generate_elimination_principles uri !status';
+ let rec get_record_attrs =
+ function
+ | [] -> None
+ | (`Class (`Record fields))::_ -> Some fields
+ | _::tl -> get_record_attrs tl
+ in
(match get_record_attrs attrs with
- None -> status (* not a record *)
- | Some fields -> generate_projections uri fields status)
+ | None -> () (* not a record *)
+ | Some fields ->
+ status' := generate_projections uri fields !status')
| Cic.CurrentProof _
- | Cic.Variable _ -> assert false
+ | Cic.Variable _ -> assert false);
+ !status'
+ with exn ->
+ MatitaSync.time_travel ~present:!status' ~past:status;
+ raise exn)
let eval_executable opts status ex =
match ex with
let eval_comment status c = status
-
let eval_ast
?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st
=
| 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 ast_of_cmd cmd =
+ GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
+ GrafiteAst.Command (DisambiguateTypes.dummy_floc,
+ (GrafiteAst.reash_cmd_uris cmd)))
+ in
+ let moo, metadata = MatitaMoo.load_moo fname in
+ List.iter
+ (fun ast ->
+ let ast = ast_of_cmd ast in
+ cb !status ast;
+ status :=
+ eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
+ moo;
+ List.iter
+ (fun m ->
+ let ast =
+ ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
+ in
+ cb !status ast;
+ status :=
+ eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast)
+ metadata
+
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
let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str =
eval_from_stream
- ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->())
+ ?do_heavy_checks ?include_paths ?clean_baseuri status
+ (Ulexing.from_utf8_string str) (fun _ _ ->())
let default_options () =
(*
lazy {
aliases = DisambiguateTypes.Environment.empty;
multi_aliases = DisambiguateTypes.Environment.empty;
- moo_content_rev = [];
+ moo_content_rev = [], [];
proof_status = No_proof;
options = default_options ();
objects = [];
projects / helm.git / blobdiff