From: Ferruccio Guidi Date: Thu, 14 May 2009 13:43:55 +0000 (+0000) Subject: - libraryObjects: new default "natural numbers" with the uri of nat. X-Git-Tag: make_still_working~3979 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68dbcd02022874a025a9444aa1125b0458816fbb;p=helm.git - libraryObjects: new default "natural numbers" with the uri of nat. alias num "natural number" uses this one instead of the hardcoded uri (removed) also destroy_nat (moved to termAcicContent) looks at this default --- diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml index c350f38c4..fb8909152 100644 --- a/helm/software/components/acic_content/termAcicContent.ml +++ b/helm/software/components/acic_content/termAcicContent.ml @@ -28,6 +28,7 @@ open Printf module Ast = CicNotationPt +module Obj = LibraryObjects let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -70,6 +71,21 @@ let constructor_of_inductive_type uri i j = 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 @@ -124,7 +140,7 @@ let ast_of_acic0 ~output_type term_info acic k = | 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 diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index 0364803c7..a397de41e 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -99,7 +99,9 @@ let rec opt_letin g st es c name v w t = | 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 diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml index e402f4db2..c523a60de 100644 --- a/helm/software/components/cic/libraryObjects.ml +++ b/helm/software/components/cic/libraryObjects.ml @@ -31,6 +31,7 @@ let default_eq_URIs = [] 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;; @@ -38,6 +39,7 @@ 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 ****) @@ -70,6 +72,8 @@ let set_default what l = 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")) @@ -79,25 +83,29 @@ let reset_defaults () = 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 ****) @@ -213,31 +221,7 @@ let false_URI () = 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 diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli index b4e19dff8..248893002 100644 --- a/helm/software/components/cic/libraryObjects.mli +++ b/helm/software/components/cic/libraryObjects.mli @@ -66,6 +66,5 @@ val false_URI : unit -> UriManager.uri option 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 diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml index 06099dcfe..c41a9aab0 100644 --- a/helm/software/components/cic_disambiguation/number_notation.ml +++ b/helm/software/components/cic_disambiguation/number_notation.ml @@ -25,10 +25,31 @@ (* $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))); @@ -39,8 +60,8 @@ let _ = ("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 diff --git a/helm/software/matita/library/nat/nat.ma b/helm/software/matita/library/nat/nat.ma index 5e3e769ec..83b489f06 100644 --- a/helm/software/matita/library/nat/nat.ma +++ b/helm/software/matita/library/nat/nat.ma @@ -19,6 +19,9 @@ inductive nat : Set \def | 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