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
| v when H.is_proof c v && H.is_atomic v ->
let x = S.subst v t in
opt_proof g (info st "Optimizer: remove 5") true c x
- | v ->
+(* | v when t = C.Rel 1 ->
+ g (info st "Optimizer: remove 6") v
+*) | v ->
g st (C.LetIn (name, v, w, t))
in
if es then opt_term g st es c v else g st v
let default_true_URIs = []
let default_false_URIs = []
let default_absurd_URIs = []
+let default_nat_URIs = []
(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
let eq_URIs_ref = ref default_eq_URIs;;
let true_URIs_ref = ref default_true_URIs
let false_URIs_ref = ref default_false_URIs
let absurd_URIs_ref = ref default_absurd_URIs
+let nat_URIs_ref = ref default_nat_URIs
(**** SET_DEFAULT ****)
false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
| "absurd",[absurd_URI] ->
absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
+ | "natural numbers",[nat_URI] ->
+ nat_URIs_ref := insert_unique nat_URI (fun x -> x) !nat_URIs_ref
| _,l ->
raise
(NotRecognized (what^" with "^string_of_int(List.length l)^" params"))
eq_URIs_ref := default_eq_URIs;
true_URIs_ref := default_true_URIs;
false_URIs_ref := default_false_URIs;
- absurd_URIs_ref := default_absurd_URIs
+ absurd_URIs_ref := default_absurd_URIs;
+ nat_URIs_ref := default_nat_URIs
;;
let stack = ref [];;
let push () =
- stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref)::!stack;
+ stack := (!eq_URIs_ref, !true_URIs_ref, !false_URIs_ref, !absurd_URIs_ref,
+ !nat_URIs_ref
+ )::!stack;
reset_defaults ()
;;
let pop () =
match !stack with
| [] -> raise (Failure "Unable to POP in libraryObjects.ml")
- | (eq,t,f,a)::tl ->
+ | (eq,t,f,a,n)::tl ->
stack := tl;
eq_URIs_ref := eq;
true_URIs_ref := t;
false_URIs_ref := f;
- absurd_URIs_ref := a
+ absurd_URIs_ref := a;
+ nat_URIs_ref := n
;;
(**** LOOKUP FUNCTIONS ****)
let absurd_URI () =
try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
-let nat_URI = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind"
-
-let zero = Cic.MutConstruct (nat_URI,0,1,[])
-let succ = Cic.MutConstruct (nat_URI,0,2,[])
-
-let is_zero = function
- | Cic.AMutConstruct (_, uri, 0, 1, _) when UriManager.eq uri nat_URI -> true
- | _ -> false
-
-let is_succ = function
- | Cic.AMutConstruct (_, uri, 0, 2, _) when UriManager.eq uri nat_URI -> true
- | _ -> false
-
-let build_nat n =
- if n < 0 then assert false;
- let rec aux = function
- | 0 -> zero
- | n -> Cic.Appl [ succ; (aux (n - 1)) ]
- in
- aux n
-
-let destroy_nat annterm =
- 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 nat_URI () =
+ try Some (List.hd !nat_URIs_ref) with Failure "hd" -> None
+let is_nat_URI uri =
+ List.exists (fun nat -> UriManager.eq nat uri) !nat_URIs_ref
val true_URI : unit -> UriManager.uri option
val absurd_URI : unit -> UriManager.uri option
-val build_nat : int -> Cic.term
-val destroy_nat : Cic.annterm -> int option
-
+val nat_URI : unit -> UriManager.uri option
+val is_nat_URI : UriManager.uri -> bool
(* $Id$ *)
+module C = Cic
+module Obj = LibraryObjects
+module DT = DisambiguateTypes
+
+let error msg =
+ raise (DT.Invalid_choice (lazy (Stdpp.dummy_loc, msg)))
+
+let build_nat o s str =
+ let n = int_of_string str in
+ if n < 0 then error (str ^ " is not a valid natural number number") else
+ let rec aux n = if n = 0 then o () else s (aux (pred n)) in
+ aux n
+
+let interp_natural_number num =
+ let nat_URI = match Obj.nat_URI () with
+ | Some uri -> uri
+ | None -> error "no default natural numbers"
+ in
+ let o () = C.MutConstruct (nat_URI,0,1,[]) in
+ let s t = C.Appl [C.MutConstruct (nat_URI,0,2,[]); t] in
+ build_nat o s num
+
let _ =
DisambiguateChoices.add_num_choice
- ("natural number",
- `Num_interp (fun num -> LibraryObjects.build_nat (int_of_string num)));
+ ("natural number", `Num_interp interp_natural_number);
DisambiguateChoices.add_num_choice
("Coq natural number",
`Num_interp (fun num -> HelmLibraryObjects.build_nat (int_of_string num)));
("binary positive number",
`Num_interp (fun num ->
let num = int_of_string num in
- if num = 0 then
- raise (DisambiguateTypes.Invalid_choice (lazy (Stdpp.dummy_loc, "0 is not a valid positive number")))
+ if num = 0 then
+ error "0 is not a valid positive number"
else
HelmLibraryObjects.build_bin_pos num));
DisambiguateChoices.add_num_choice
| S : nat \to nat.
interpretation "Natural numbers" 'N = nat.
+
+default "natural numbers" cic:/matita/nat/nat/nat.ind.
+
alias num (instance 0) = "natural number".
definition pred: nat \to nat \def
projects / helm.git / commitdiff