metadata: LibraryNoDb.metadata list;
}
+let initial_status = {
+ aliases = DisambiguateTypes.Environment.empty;
+ multi_aliases = DisambiguateTypes.Environment.empty;
+ lexicon_content_rev = [];
+ notation_ids = [];
+ metadata = [];
+}
+
let add_lexicon_content cmds status =
let content = status.lexicon_content_rev in
let content' =
else
status
-let set_proof_aliases status new_aliases =
- let commands_of_aliases =
- List.map
- (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
- in
- let deps_of_aliases =
- HExtlib.filter_map
- (function
- | LexiconAst.Ident_alias (_, suri) ->
- let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
- Some (LibraryNoDb.Dependency buri)
- | _ -> None)
- in
- let aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status.aliases new_aliases in
- let multi_aliases =
- List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
- status.multi_aliases new_aliases in
- let new_status =
- { status with multi_aliases = multi_aliases ; aliases = aliases}
- in
- if new_aliases = [] then
- new_status
+let set_proof_aliases mode status new_aliases =
+ if mode = LexiconAst.WithoutPreferences then
+ status
else
- let aliases =
- DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+ let commands_of_aliases =
+ List.map
+ (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
+ in
+ let deps_of_aliases =
+ HExtlib.filter_map
+ (function
+ | LexiconAst.Ident_alias (_, suri) ->
+ let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
+ Some (LibraryNoDb.Dependency buri)
+ | _ -> None)
in
- let status = add_lexicon_content (commands_of_aliases aliases) new_status in
- let status = add_metadata (deps_of_aliases aliases) status in
- status
+ let aliases =
+ List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
+ status.aliases new_aliases in
+ let multi_aliases =
+ List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc)
+ status.multi_aliases new_aliases in
+ let new_status =
+ { status with multi_aliases = multi_aliases ; aliases = aliases}
+ in
+ if new_aliases = [] then
+ new_status
+ else
+ let aliases =
+ DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases
+ in
+ let status =
+ add_lexicon_content (commands_of_aliases aliases) new_status
+ in
+ let status = add_metadata (deps_of_aliases aliases) status in
+ status
+
-let rec eval_command status cmd =
+let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
let notation_ids' = CicNotation.process_notation cmd in
let status =
{ status with notation_ids = notation_ids' @ status.notation_ids } in
- let basedir = Helm_registry.get "matita.basedir" in
match cmd with
- | LexiconAst.Include (loc, baseuri) ->
- let lexiconpath = LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri in
- if not (Sys.file_exists lexiconpath) then
- raise (IncludedFileNotCompiled lexiconpath);
+ | LexiconAst.Include (loc, baseuri, mode) ->
+ let lexiconpath_rw, lexiconpath_r =
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~writable:true ~baseuri,
+ LibraryMisc.lexicon_file_of_baseuri
+ ~must_exist:false ~writable:false ~baseuri
+ in
+ let lexiconpath =
+ if Sys.file_exists lexiconpath_rw then lexiconpath_rw else
+ if Sys.file_exists lexiconpath_r then lexiconpath_r else
+ raise (IncludedFileNotCompiled lexiconpath_rw)
+ in
let lexicon = LexiconMarshal.load_lexicon lexiconpath in
- let status = List.fold_left eval_command status lexicon in
+ let status = List.fold_left (eval_command ~mode) status lexicon in
if Helm_registry.get_bool "db.nodb" then
- let metadatapath = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
- if not (Sys.file_exists metadatapath) then
- raise (MetadataNotFound metadatapath)
- else
- add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status
+ let metadatapath_rw, metadatapath_r =
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:true,
+ LibraryMisc.metadata_file_of_baseuri
+ ~must_exist:false ~baseuri ~writable:false
+ in
+ let metadatapath =
+ if Sys.file_exists metadatapath_rw then metadatapath_rw else
+ if Sys.file_exists metadatapath_r then metadatapath_r else
+ raise (MetadataNotFound metadatapath_rw)
+ in
+ add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status
else
status
| LexiconAst.Alias (loc, spec) ->
[DisambiguateTypes.Num instance,
DisambiguateChoices.lookup_num_by_dsc desc]
in
- set_proof_aliases status diff
+ set_proof_aliases mode status diff
| LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
let status = add_lexicon_content [stm] status in
let uris =
[DisambiguateTypes.Symbol (symbol, 0),
DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
in
- let status = set_proof_aliases status diff in
+ let status = set_proof_aliases mode status diff in
let status = add_metadata uris status in
status
| LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status
+let eval_command = eval_command ?mode:None
+
+let set_proof_aliases = set_proof_aliases LexiconAst.WithPreferences
+