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 *)
}
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
else
let commands_of_aliases =
List.map
- (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
+ (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 d c acc)
- status.multi_aliases new_aliases in
+ 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
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
+ add_lexicon_content (commands_of_aliases new_aliases) new_status
in
status
->
let item = DisambiguateTypes.Id id in
(try
- let t =
- snd (DisambiguateTypes.Environment.find item status.aliases)
- status.aliases "" [] in
- let uri = CicUtil.uri_of_term t in
+ 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: " ^
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 mode status diff
| LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
let status = add_lexicon_content [stm] status 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 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