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
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 t =
+ snd (DisambiguateTypes.Environment.find item status.aliases)
+ status.aliases "" [] in
+ let uri = CicUtil.uri_of_term t 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 =
DisambiguateChoices.lookup_num_by_dsc desc]
in
set_proof_aliases mode status diff
- | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
+ | 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),
+ DisambiguateChoices.lookup_symbol_by_dsc symbol 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