(* $Id$ *)
-exception IncludedFileNotCompiled of string (* file name *)
+let out = ref ignore
+
+let set_callback f = out := f
+
+(* lexicon file name * ma file name *)
+exception IncludedFileNotCompiled of string * string
exception MetadataNotFound of string (* file name *)
type status = {
- aliases: DisambiguateTypes.environment; (** disambiguation aliases *)
- multi_aliases: DisambiguateTypes.multiple_environment;
+ aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t;
+ multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t;
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 =
let content = status.lexicon_content_rev in
let content' =
List.fold_right
- (fun cmd acc -> cmd :: (List.filter ((<>) cmd) acc))
+ (fun cmd acc ->
+ match cmd with
+ | LexiconAst.Alias _
+ | LexiconAst.Include _
+ | LexiconAst.Notation _ -> cmd :: (List.filter ((<>) cmd) acc)
+ | LexiconAst.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc)
cmds content
in
(* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map
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 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 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 LexiconAst.description_of_alias
+ d c acc)
+ status.multi_aliases new_aliases
+ in
+ let new_status =
+ { status with multi_aliases = multi_aliases ; aliases = 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
+ if new_aliases = [] then
+ new_status
+ else
+ let status =
+ add_lexicon_content (commands_of_aliases new_aliases) new_status
+ in
+ status
+
-let rec eval_command status cmd =
+let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
+ let cmd =
+ match cmd with
+ | LexiconAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
+ let rec disambiguate =
+ function
+ CicNotationPt.ApplPattern l ->
+ CicNotationPt.ApplPattern (List.map disambiguate l)
+ | CicNotationPt.VarPattern id
+ when not
+ (List.exists
+ (function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
+ ->
+ let item = DisambiguateTypes.Id id in
+ (try
+ let uri =
+ match DisambiguateTypes.Environment.find item status.aliases with
+ LexiconAst.Ident_alias (_, uri)-> UriManager.uri_of_string uri
+ | _ -> assert false
+ in
+ CicNotationPt.UriPattern uri
+ with Not_found ->
+ prerr_endline ("Domain item not found: " ^
+ (DisambiguateTypes.string_of_domain_item item));
+ assert false)
+ | p -> p
+ in
+ LexiconAst.Interpretation
+ (loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
+ | _-> cmd
+ in
+ !out cmd;
let notation_ids' = CicNotation.process_notation cmd in
let status =
{ status with notation_ids = notation_ids' @ status.notation_ids } in
match cmd with
- | LexiconAst.Include (loc, baseuri) ->
+ | LexiconAst.Include (loc, baseuri, mode, fullpath) ->
let lexiconpath_rw, lexiconpath_r =
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~writable:true ~baseuri,
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)
+ raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath))
in
let lexicon = LexiconMarshal.load_lexicon lexiconpath in
- let status = List.fold_left eval_command 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
+ let status = List.fold_left (eval_command ~mode) status lexicon in
+ status
| LexiconAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
code in DisambiguatePp *)
match spec with
| LexiconAst.Ident_alias (id,uri) ->
- [DisambiguateTypes.Id id,
- (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))]
+ [DisambiguateTypes.Id id,spec]
| LexiconAst.Symbol_alias (symb, instance, desc) ->
- [DisambiguateTypes.Symbol (symb,instance),
- DisambiguateChoices.lookup_symbol_by_dsc symb desc]
+ [DisambiguateTypes.Symbol (symb,instance),spec]
| LexiconAst.Number_alias (instance,desc) ->
- [DisambiguateTypes.Num instance,
- DisambiguateChoices.lookup_num_by_dsc desc]
+ [DisambiguateTypes.Num instance,spec]
in
- set_proof_aliases status diff
- | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
+ set_proof_aliases mode status diff
+ | LexiconAst.Interpretation (_, dsc, (symbol, _), _) 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]
+ try
+ [DisambiguateTypes.Symbol (symbol, 0),
+ LexiconAst.Symbol_alias (symbol,0,dsc)]
+ with
+ DisambiguateChoices.Choice_not_found msg ->
+ prerr_endline (Lazy.force msg);
+ assert false
in
- let status = set_proof_aliases status diff in
- let status = add_metadata uris status in
+ let status = set_proof_aliases mode status diff in
status
- | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] 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
+