multi_aliases: DisambiguateTypes.multiple_environment;
lexicon_content_rev: LexiconMarshal.lexicon;
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
- metadata: LibraryNoDb.metadata list;
}
let initial_status = {
multi_aliases = DisambiguateTypes.Environment.empty;
lexicon_content_rev = [];
notation_ids = [];
- metadata = [];
}
let add_lexicon_content cmds status =
LexiconAstPp.pp_command content')); *)
{ status with lexicon_content_rev = content' }
-let add_metadata new_metadata status =
- if Helm_registry.get_bool "db.nodb" then
- let metadata = status.metadata in
- let metadata' =
- List.fold_left
- (fun acc m ->
- match m with
- | LibraryNoDb.Dependency buri ->
- if List.exists (LibraryNoDb.eq_metadata m) metadata
- then acc
- else m :: acc)
- metadata new_metadata
- in
- { status with metadata = metadata' }
- else
- status
-
let set_proof_aliases mode status new_aliases =
if mode = LexiconAst.WithoutPreferences then
status
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 status =
add_lexicon_content (commands_of_aliases aliases) new_status
in
- let status = add_metadata (deps_of_aliases aliases) status in
status
in
let lexicon = LexiconMarshal.load_lexicon lexiconpath in
let status = List.fold_left (eval_command ~mode) status lexicon in
- if Helm_registry.get_bool "db.nodb" then
- 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
+ status
| LexiconAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
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 =
- List.map
- (fun uri -> LibraryNoDb.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
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