open Printf
module Ast = CicNotationPt
+module Obj = LibraryObjects
let debug = false
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
let left_params_no_of_inductive_type uri =
snd (get_types uri)
+let destroy_nat annterm =
+ let is_zero = function
+ | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
+ | _ -> false
+ in
+ let is_succ = function
+ | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
+ | _ -> false
+ in
+ let rec aux acc = function
+ | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
+ | t when is_zero t -> Some acc
+ | _ -> None in
+ aux 0 annterm
+
let ast_of_acic0 ~output_type term_info acic k =
let k = k term_info in
let id_to_uris = term_info.uri in
| Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
| Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t ->
- (match LibraryObjects.destroy_nat t with
+ (match destroy_nat t with
| Some n -> idref aid (Ast.Num (string_of_int n, -1))
| None ->
let deannot_he = Deannotate.deannotate_term he in
exception Interpretation_not_found
-let lookup_interpretations symbol =
+let lookup_interpretations ?(sorted=true) symbol =
try
- HExtlib.list_uniq
- (List.sort Pervasives.compare
- (List.map
- (fun id ->
- let (dsc, _, args, appl_pattern) =
- try
- Hashtbl.find !level2_patterns32 id
- with Not_found -> assert false
- in
- dsc, args, appl_pattern)
- !(Hashtbl.find !interpretations symbol)))
+ let raw =
+ List.map (
+ fun id ->
+ let (dsc, _, args, appl_pattern) =
+ try
+ Hashtbl.find !level2_patterns32 id
+ with Not_found -> assert false
+ in
+ dsc, args, appl_pattern
+ )
+ !(Hashtbl.find !interpretations symbol)
+ in
+ if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+ else raw
with Not_found -> raise Interpretation_not_found
let remove_interpretation id =