let sort_of_id id =
try
Hashtbl.find term_info.sort id
- with Not_found -> assert false
+ with Not_found ->
+ prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
+ `Type
in
let aux_substs substs =
Some
with Not_found -> assert false
in
let ast = instantiate32 term_info env' symbol args in
- match uris with
- | [] -> ast
- | _ -> Ast.AttributedTerm (`Href uris, ast)
+ Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm),
+ (match uris with
+ | [] -> ast
+ | _ -> Ast.AttributedTerm (`Href uris, ast)))
let load_patterns32 t =
set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
exception Interpretation_not_found
exception Pretty_printer_not_found
+let rec list_uniq = function
+ | [] -> []
+ | h::[] -> [h]
+ | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl)
+ | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
+
let lookup_interpretations symbol =
try
- List.map
+ list_uniq
+ (List.sort Pervasives.compare
+ (List.map
(fun id ->
let (dsc, _, args, appl_pattern, _) =
try
with Not_found -> assert false
in
dsc, args, appl_pattern)
- !(Hashtbl.find interpretations symbol)
+ !(Hashtbl.find interpretations symbol)))
with Not_found -> raise Interpretation_not_found
let add_pretty_printer ~precedence ~associativity l2 l1 =