diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_ascii_syntax.ml | 83 | ||||
| -rw-r--r-- | parsing/g_intsyntax.ml | 342 | ||||
| -rw-r--r-- | parsing/g_natsyntax.ml | 78 | ||||
| -rw-r--r-- | parsing/g_rsyntax.ml | 125 | ||||
| -rw-r--r-- | parsing/g_string_syntax.ml | 69 | ||||
| -rw-r--r-- | parsing/g_zsyntax.ml | 194 | ||||
| -rw-r--r-- | parsing/highparsing.mllib | 6 |
7 files changed, 0 insertions, 897 deletions
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml deleted file mode 100644 index f9ca94ff6c..0000000000 --- a/parsing/g_ascii_syntax.ml +++ /dev/null @@ -1,83 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -open Pp -open Util -open Names -open Pcoq -open Rawterm -open Topconstr -open Libnames -open Coqlib -open Bigint - -exception Non_closed_ascii - -let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let make_kn dir id = Libnames.encode_kn (make_dir dir) (id_of_string id) -let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) - -let ascii_module = ["Coq";"Strings";"Ascii"] - -let ascii_path = make_path ascii_module "ascii" - -let ascii_kn = make_kn ascii_module "ascii" -let path_of_Ascii = ((ascii_kn,0),1) -let static_glob_Ascii = ConstructRef path_of_Ascii - -let make_reference id = find_reference "Ascii interpretation" ascii_module id -let glob_Ascii = lazy (make_reference "Ascii") - -open Lazy - -let interp_ascii dloc p = - let rec aux n p = - if n = 0 then [] else - let mp = p mod 2 in - RRef (dloc,if mp = 0 then glob_false else glob_true) - :: (aux (n-1) (p/2)) in - RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p) - -let interp_ascii_string dloc s = - let p = - if String.length s = 1 then int_of_char s.[0] - else - if String.length s = 3 & is_digit s.[0] & is_digit s.[1] & is_digit s.[2] - then int_of_string s - else - user_err_loc (dloc,"interp_ascii_string", - str "Expects a single character or a three-digits ascii code.") in - interp_ascii dloc p - -let uninterp_ascii r = - let rec uninterp_bool_list n = function - | [] when n = 0 -> 0 - | RRef (_,k)::l when k = glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l) - | _ -> raise Non_closed_ascii in - try - let rec aux = function - | RApp (_,RRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l - | _ -> raise Non_closed_ascii in - Some (aux r) - with - Non_closed_ascii -> None - -let make_ascii_string n = - if n>=32 && n<=126 then String.make 1 (char_of_int n) - else Printf.sprintf "%03d" n - -let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) - -let _ = - Notation.declare_string_interpreter "char_scope" - (ascii_path,ascii_module) - interp_ascii_string - ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true) diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml deleted file mode 100644 index 7cef2fac00..0000000000 --- a/parsing/g_intsyntax.ml +++ /dev/null @@ -1,342 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -(* digit-based syntax for int31, bigN bigZ and bigQ *) - -open Bigint -open Libnames -open Rawterm - -(*** Constants for locating the int31 and bigN ***) - - - -let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l)) -let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id) - -(* copied on g_zsyntax.ml, where it is said to be a temporary hack*) -(* takes a path an identifier in the form of a string list and a string, - returns a kernel_name *) -let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id) - - -(* int31 stuff *) -let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"] -let int31_path = make_path int31_module "int31" -let int31_id = make_kn int31_module -let int31_scope = "int31_scope" - -let int31_construct = ConstructRef ((int31_id "int31",0),1) - -let int31_0 = ConstructRef ((int31_id "digits",0),1) -let int31_1 = ConstructRef ((int31_id "digits",0),2) - - -(* bigN stuff*) -let zn2z_module = ["Coq"; "Numbers"; "Cyclic"; "DoubleCyclic"; "DoubleType"] -let zn2z_path = make_path zn2z_module "zn2z" -let zn2z_id = make_kn zn2z_module - -let zn2z_W0 = ConstructRef ((zn2z_id "zn2z",0),1) -let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2) - -let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ] -let bigN_path = make_path (bigN_module@["BigN"]) "t" -(* big ugly hack *) -let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), - Names.mk_label "BigN")), - [], Names.id_of_string id) : Names.kernel_name) -let bigN_scope = "bigN_scope" - -(* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *) -let n_inlined = of_string "7" -let bigN_constructor = - (* converts a bigint into an int the ugly way *) - let rec to_int i = - if equal i zero then - 0 - else - let (quo,rem) = div2_with_rest i in - if rem then - 2*(to_int quo)+1 - else - 2*(to_int quo) - in - fun i -> - ConstructRef ((bigN_id "t_",0), - if less_than i n_inlined then - (to_int i)+1 - else - (to_int n_inlined)+1 - ) - -(*bigZ stuff*) -let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ] -let bigZ_path = make_path (bigZ_module@["BigZ"]) "t" -(* big ugly hack bis *) -let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), - Names.mk_label "BigZ")), - [], Names.id_of_string id) : Names.kernel_name) -let bigZ_scope = "bigZ_scope" - -let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1) -let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2) - - -(*bigQ stuff*) -let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"] -let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"] -let bigQ_path = make_path (bigQ_module@["BigQ"]) "t" -(* big ugly hack bis *) -let bigQ_id = make_kn qmake_module -let bigQ_scope = "bigQ_scope" - -let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1) - - -(*** Definition of the Non_closed exception, used in the pretty printing ***) -exception Non_closed - -(*** Parsing for int31 in digital notation ***) - -(* parses a *non-negative* integer (from bigint.ml) into an int31 - wraps modulo 2^31 *) -let int31_of_pos_bigint dloc n = - let ref_construct = RRef (dloc, int31_construct) in - let ref_0 = RRef (dloc, int31_0) in - let ref_1 = RRef (dloc, int31_1) in - let rec args counter n = - if counter <= 0 then - [] - else - let (q,r) = div2_with_rest n in - (if r then ref_1 else ref_0)::(args (counter-1) q) - in - RApp (dloc, ref_construct, List.rev (args 31 n)) - -let error_negative dloc = - Util.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.") - -let interp_int31 dloc n = - if is_pos_or_zero n then - int31_of_pos_bigint dloc n - else - error_negative dloc - -(* Pretty prints an int31 *) - -let bigint_of_int31 = - let rec args_parsing args cur = - match args with - | [] -> cur - | (RRef (_,b))::l when b = int31_0 -> args_parsing l (mult_2 cur) - | (RRef (_,b))::l when b = int31_1 -> args_parsing l (add_1 (mult_2 cur)) - | _ -> raise Non_closed - in - function - | RApp (_, RRef (_, c), args) when c=int31_construct -> args_parsing args zero - | _ -> raise Non_closed - -let uninterp_int31 i = - try - Some (bigint_of_int31 i) - with Non_closed -> - None - -(* Actually declares the interpreter for int31 *) -let _ = Notation.declare_numeral_interpreter int31_scope - (int31_path, int31_module) - interp_int31 - ([RRef (Util.dummy_loc, int31_construct)], - uninterp_int31, - true) - - -(*** Parsing for bigN in digital notation ***) -(* the base for bigN (in Coq) that is 2^31 in our case *) -let base = pow two (of_string "31") - -(* base of the bigN of height N : *) -let rank n = pow base (pow two n) - -(* splits a number bi at height n, that is the rest needs 2^n int31 to be stored - it is expected to be used only when the quotient would also need 2^n int31 to be - stored *) -let split_at n bi = - euclid bi (rank (sub_1 n)) - -(* search the height of the Coq bigint needed to represent the integer bi *) -let height bi = - let rec height_aux n = - if less_than bi (rank n) then - n - else - height_aux (add_1 n) - in - height_aux zero - - -(* n must be a non-negative integer (from bigint.ml) *) -let word_of_pos_bigint dloc hght n = - let ref_W0 = RRef (dloc, zn2z_W0) in - let ref_WW = RRef (dloc, zn2z_WW) in - let rec decomp hgt n = - if is_neg_or_zero hgt then - int31_of_pos_bigint dloc n - else if equal n zero then - RApp (dloc, ref_W0, [RHole (dloc, Evd.InternalHole)]) - else - let (h,l) = split_at hgt n in - RApp (dloc, ref_WW, [RHole (dloc, Evd.InternalHole); - decomp (sub_1 hgt) h; - decomp (sub_1 hgt) l]) - in - decomp hght n - -let bigN_of_pos_bigint dloc n = - let ref_constructor i = RRef (dloc, bigN_constructor i) in - let result h word = RApp (dloc, ref_constructor h, if less_than h n_inlined then - [word] - else - [G_natsyntax.nat_of_int dloc (sub h n_inlined); - word]) - in - let hght = height n in - result hght (word_of_pos_bigint dloc hght n) - -let bigN_error_negative dloc = - Util.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.") - -let interp_bigN dloc n = - if is_pos_or_zero n then - bigN_of_pos_bigint dloc n - else - bigN_error_negative dloc - - -(* Pretty prints a bigN *) - -let bigint_of_word = - let rec get_height rc = - match rc with - | RApp (_,RRef(_,c), [_;lft;rght]) when c = zn2z_WW -> - let hleft = get_height lft in - let hright = get_height rght in - add_1 - (if less_than hleft hright then - hright - else - hleft) - | _ -> zero - in - let rec transform hght rc = - match rc with - | RApp (_,RRef(_,c),_) when c = zn2z_W0-> zero - | RApp (_,RRef(_,c), [_;lft;rght]) when c=zn2z_WW-> let new_hght = sub_1 hght in - add (mult (rank new_hght) - (transform (new_hght) lft)) - (transform (new_hght) rght) - | _ -> bigint_of_int31 rc - in - fun rc -> - let hght = get_height rc in - transform hght rc - -let bigint_of_bigN rc = - match rc with - | RApp (_,_,[one_arg]) -> bigint_of_word one_arg - | RApp (_,_,[_;second_arg]) -> bigint_of_word second_arg - | _ -> raise Non_closed - -let uninterp_bigN rc = - try - Some (bigint_of_bigN rc) - with Non_closed -> - None - - -(* declare the list of constructors of bigN used in the declaration of the - numeral interpreter *) - -let bigN_list_of_constructors = - let rec build i = - if less_than i (add_1 n_inlined) then - RRef (Util.dummy_loc, bigN_constructor i)::(build (add_1 i)) - else - [] - in - build zero - -(* Actually declares the interpreter for bigN *) -let _ = Notation.declare_numeral_interpreter bigN_scope - (bigN_path, bigN_module) - interp_bigN - (bigN_list_of_constructors, - uninterp_bigN, - true) - - -(*** Parsing for bigZ in digital notation ***) -let interp_bigZ dloc n = - let ref_pos = RRef (dloc, bigZ_pos) in - let ref_neg = RRef (dloc, bigZ_neg) in - if is_pos_or_zero n then - RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) - else - RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)]) - -(* pretty printing functions for bigZ *) -let bigint_of_bigZ = function - | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_pos -> bigint_of_bigN one_arg - | RApp (_, RRef(_,c), [one_arg]) when c = bigZ_neg -> - let opp_val = bigint_of_bigN one_arg in - if equal opp_val zero then - raise Non_closed - else - neg opp_val - | _ -> raise Non_closed - - -let uninterp_bigZ rc = - try - Some (bigint_of_bigZ rc) - with Non_closed -> - None - -(* Actually declares the interpreter for bigN *) -let _ = Notation.declare_numeral_interpreter bigZ_scope - (bigZ_path, bigZ_module) - interp_bigZ - ([RRef (Util.dummy_loc, bigZ_pos); - RRef (Util.dummy_loc, bigZ_neg)], - uninterp_bigZ, - true) - -(*** Parsing for bigQ in digital notation ***) -let interp_bigQ dloc n = - let ref_z = RRef (dloc, bigQ_z) in - let ref_pos = RRef (dloc, bigZ_pos) in - let ref_neg = RRef (dloc, bigZ_neg) in - if is_pos_or_zero n then - RApp (dloc, ref_z, - [RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])]) - else - RApp (dloc, ref_z, - [RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])]) - -let uninterp_bigQ rc = None - - -(* Actually declares the interpreter for bigQ *) -let _ = Notation.declare_numeral_interpreter bigQ_scope - (bigQ_path, bigQ_module) - interp_bigQ - ([], uninterp_bigQ, - true) diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml deleted file mode 100644 index c62c813778..0000000000 --- a/parsing/g_natsyntax.ml +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -(* This file defines the printer for natural numbers in [nat] *) - -(*i*) -open Pcoq -open Pp -open Util -open Names -open Coqlib -open Rawterm -open Libnames -open Bigint -open Coqlib -open Notation -open Pp -open Util -open Names -(*i*) - -(**********************************************************************) -(* Parsing via scopes *) -(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) - -let nat_of_int dloc n = - if is_pos_or_zero n then begin - if less_than (of_string "5000") n then - Flags.if_warn msg_warning - (strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in nat (observed threshold " ++ - strbrk "may vary from 5000 to 70000 depending on your system " ++ - strbrk "limits and on the command executed)."); - let ref_O = RRef (dloc, glob_O) in - let ref_S = RRef (dloc, glob_S) in - let rec mk_nat acc n = - if n <> zero then - mk_nat (RApp (dloc,ref_S, [acc])) (sub_1 n) - else - acc - in - mk_nat ref_O n - end - else - user_err_loc (dloc, "nat_of_int", - str "Cannot interpret a negative number as a number of type nat") - -(************************************************************************) -(* Printing via scopes *) - -exception Non_closed_number - -let rec int_of_nat = function - | RApp (_,RRef (_,s),[a]) when s = glob_S -> add_1 (int_of_nat a) - | RRef (_,z) when z = glob_O -> zero - | _ -> raise Non_closed_number - -let uninterp_nat p = - try - Some (int_of_nat p) - with - Non_closed_number -> None - -(************************************************************************) -(* Declare the primitive parsers and printers *) - -let _ = - Notation.declare_numeral_interpreter "nat_scope" - (nat_path,["Coq";"Init";"Datatypes"]) - nat_of_int - ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, true) diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml deleted file mode 100644 index 4a5972cc71..0000000000 --- a/parsing/g_rsyntax.ml +++ /dev/null @@ -1,125 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id$ i*) - -open Pp -open Util -open Names -open Pcoq -open Topconstr -open Libnames - -exception Non_closed_number - -(**********************************************************************) -(* Parsing R via scopes *) -(**********************************************************************) - -open Libnames -open Rawterm -open Bigint - -let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"] -let make_path dir id = Libnames.make_path dir (id_of_string id) - -let r_path = make_path rdefinitions "R" - -(* TODO: temporary hack *) -let make_path dir id = Libnames.encode_con dir (id_of_string id) - -let r_kn = make_path rdefinitions "R" -let glob_R = ConstRef r_kn -let glob_R1 = ConstRef (make_path rdefinitions "R1") -let glob_R0 = ConstRef (make_path rdefinitions "R0") -let glob_Ropp = ConstRef (make_path rdefinitions "Ropp") -let glob_Rplus = ConstRef (make_path rdefinitions "Rplus") -let glob_Rmult = ConstRef (make_path rdefinitions "Rmult") - -let two = mult_2 one -let three = add_1 two -let four = mult_2 two - -(* Unary representation of strictly positive numbers *) -let rec small_r dloc n = - if equal one n then RRef (dloc, glob_R1) - else RApp(dloc,RRef (dloc,glob_Rplus), - [RRef (dloc, glob_R1);small_r dloc (sub_1 n)]) - -let r_of_posint dloc n = - let r1 = RRef (dloc, glob_R1) in - let r2 = small_r dloc two in - let rec r_of_pos n = - if less_than n four then small_r dloc n - else - let (q,r) = div2_with_rest n in - let b = RApp(dloc,RRef(dloc,glob_Rmult),[r2;r_of_pos q]) in - if r then RApp(dloc,RRef(dloc,glob_Rplus),[r1;b]) else b in - if n <> zero then r_of_pos n else RRef(dloc,glob_R0) - -let r_of_int dloc z = - if is_strictly_neg z then - RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) - else - r_of_posint dloc z - -(**********************************************************************) -(* Printing R via scopes *) -(**********************************************************************) - -let bignat_of_r = -(* for numbers > 1 *) -let rec bignat_of_pos = function - (* 1+1 *) - | RApp (_,RRef (_,p), [RRef (_,o1); RRef (_,o2)]) - when p = glob_Rplus & o1 = glob_R1 & o2 = glob_R1 -> two - (* 1+(1+1) *) - | RApp (_,RRef (_,p1), [RRef (_,o1); - RApp(_,RRef (_,p2),[RRef(_,o2);RRef(_,o3)])]) - when p1 = glob_Rplus & p2 = glob_Rplus & - o1 = glob_R1 & o2 = glob_R1 & o3 = glob_R1 -> three - (* (1+1)*b *) - | RApp (_,RRef (_,p), [a; b]) when p = glob_Rmult -> - if bignat_of_pos a <> two then raise Non_closed_number; - mult_2 (bignat_of_pos b) - (* 1+(1+1)*b *) - | RApp (_,RRef (_,p1), [RRef (_,o); RApp (_,RRef (_,p2),[a;b])]) - when p1 = glob_Rplus & p2 = glob_Rmult & o = glob_R1 -> - if bignat_of_pos a <> two then raise Non_closed_number; - add_1 (mult_2 (bignat_of_pos b)) - | _ -> raise Non_closed_number -in -let bignat_of_r = function - | RRef (_,a) when a = glob_R0 -> zero - | RRef (_,a) when a = glob_R1 -> one - | r -> bignat_of_pos r -in -bignat_of_r - -let bigint_of_r = function - | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> - let n = bignat_of_r a in - if n = zero then raise Non_closed_number; - neg n - | a -> bignat_of_r a - -let uninterp_r p = - try - Some (bigint_of_r p) - with Non_closed_number -> - None - -let _ = Notation.declare_numeral_interpreter "R_scope" - (r_path,["Coq";"Reals";"Rdefinitions"]) - r_of_int - ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0); - RRef(dummy_loc,glob_Rplus);RRef(dummy_loc,glob_Rmult); - RRef(dummy_loc,glob_R1)], - uninterp_r, - false) diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml deleted file mode 100644 index a936485d9b..0000000000 --- a/parsing/g_string_syntax.ml +++ /dev/null @@ -1,69 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -open Pp -open Util -open Names -open Pcoq -open Libnames -open Topconstr -open G_ascii_syntax -open Rawterm -open Coqlib - -exception Non_closed_string - -(* make a string term from the string s *) - -let string_module = ["Coq";"Strings";"String"] - -let string_path = make_path string_module "string" - -let string_kn = make_kn string_module "string" -let static_glob_EmptyString = ConstructRef ((string_kn,0),1) -let static_glob_String = ConstructRef ((string_kn,0),2) - -let make_reference id = find_reference "String interpretation" string_module id -let glob_String = lazy (make_reference "String") -let glob_EmptyString = lazy (make_reference "EmptyString") - -open Lazy - -let interp_string dloc s = - let le = String.length s in - let rec aux n = - if n = le then RRef (dloc, force glob_EmptyString) else - RApp (dloc,RRef (dloc, force glob_String), - [interp_ascii dloc (int_of_char s.[n]); aux (n+1)]) - in aux 0 - -let uninterp_string r = - try - let b = Buffer.create 16 in - let rec aux = function - | RApp (_,RRef (_,k),[a;s]) when k = force glob_String -> - (match uninterp_ascii a with - | Some c -> Buffer.add_char b (Char.chr c); aux s - | _ -> raise Non_closed_string) - | RRef (_,z) when z = force glob_EmptyString -> - Some (Buffer.contents b) - | _ -> - raise Non_closed_string - in aux r - with - Non_closed_string -> None - -let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([RRef (dummy_loc,static_glob_String); - RRef (dummy_loc,static_glob_EmptyString)], - uninterp_string, true) diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml deleted file mode 100644 index bfbe54c28c..0000000000 --- a/parsing/g_zsyntax.ml +++ /dev/null @@ -1,194 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* $Id$ *) - -open Pcoq -open Pp -open Util -open Names -open Topconstr -open Libnames -open Bigint - -exception Non_closed_number - -(**********************************************************************) -(* Parsing positive via scopes *) -(**********************************************************************) - -open Libnames -open Rawterm -let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let positive_module = ["Coq";"NArith";"BinPos"] -let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) - -let positive_path = make_path positive_module "positive" - -(* TODO: temporary hack *) -let make_kn dir id = Libnames.encode_kn dir id - -let positive_kn = - make_kn (make_dir positive_module) (id_of_string "positive") -let glob_positive = IndRef (positive_kn,0) -let path_of_xI = ((positive_kn,0),1) -let path_of_xO = ((positive_kn,0),2) -let path_of_xH = ((positive_kn,0),3) -let glob_xI = ConstructRef path_of_xI -let glob_xO = ConstructRef path_of_xO -let glob_xH = ConstructRef path_of_xH - -let pos_of_bignat dloc x = - let ref_xI = RRef (dloc, glob_xI) in - let ref_xH = RRef (dloc, glob_xH) in - let ref_xO = RRef (dloc, glob_xO) in - let rec pos_of x = - match div2_with_rest x with - | (q,false) -> RApp (dloc, ref_xO,[pos_of q]) - | (q,true) when q <> zero -> RApp (dloc,ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive dloc = - user_err_loc (dloc, "interp_positive", - str "Only strictly positive numbers in type \"positive\".") - -let interp_positive dloc n = - if is_strictly_pos n then pos_of_bignat dloc n - else error_non_positive dloc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let rec bignat_of_pos = function - | RApp (_, RRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a) - | RApp (_, RRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a)) - | RRef (_, a) when a = glob_xH -> Bigint.one - | _ -> raise Non_closed_number - -let uninterp_positive p = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,positive_module) - interp_positive - ([RRef (dummy_loc, glob_xI); - RRef (dummy_loc, glob_xO); - RRef (dummy_loc, glob_xH)], - uninterp_positive, - true) - -(**********************************************************************) -(* Parsing N via scopes *) -(**********************************************************************) - -let binnat_module = ["Coq";"NArith";"BinNat"] -let n_kn = make_kn (make_dir binnat_module) (id_of_string "N") -let glob_n = IndRef (n_kn,0) -let path_of_N0 = ((n_kn,0),1) -let path_of_Npos = ((n_kn,0),2) -let glob_N0 = ConstructRef path_of_N0 -let glob_Npos = ConstructRef path_of_Npos - -let n_path = make_path binnat_module "N" - -let n_of_binnat dloc pos_or_neg n = - if n <> zero then - RApp(dloc, RRef (dloc,glob_Npos), [pos_of_bignat dloc n]) - else - RRef (dloc, glob_N0) - -let error_negative dloc = - user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") - -let n_of_int dloc n = - if is_pos_or_zero n then n_of_binnat dloc true n - else error_negative dloc - -(**********************************************************************) -(* Printing N via scopes *) -(**********************************************************************) - -let bignat_of_n = function - | RApp (_, RRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a - | RRef (_, a) when a = glob_N0 -> Bigint.zero - | _ -> raise Non_closed_number - -let uninterp_n p = - try Some (bignat_of_n p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for N *) - -let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnat_module) - n_of_int - ([RRef (dummy_loc, glob_N0); - RRef (dummy_loc, glob_Npos)], - uninterp_n, - true) - -(**********************************************************************) -(* Parsing Z via scopes *) -(**********************************************************************) - -let binint_module = ["Coq";"ZArith";"BinInt"] -let z_path = make_path binint_module "Z" -let z_kn = make_kn (make_dir binint_module) (id_of_string "Z") -let glob_z = IndRef (z_kn,0) -let path_of_ZERO = ((z_kn,0),1) -let path_of_POS = ((z_kn,0),2) -let path_of_NEG = ((z_kn,0),3) -let glob_ZERO = ConstructRef path_of_ZERO -let glob_POS = ConstructRef path_of_POS -let glob_NEG = ConstructRef path_of_NEG - -let z_of_int dloc n = - if n <> zero then - let sgn, n = - if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - RApp(dloc, RRef (dloc,sgn), [pos_of_bignat dloc n]) - else - RRef (dloc, glob_ZERO) - -(**********************************************************************) -(* Printing Z via scopes *) -(**********************************************************************) - -let bigint_of_z = function - | RApp (_, RRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a - | RApp (_, RRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a) - | RRef (_, a) when a = glob_ZERO -> Bigint.zero - | _ -> raise Non_closed_number - -let uninterp_z p = - try - Some (bigint_of_z p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for Z *) - -let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binint_module) - z_of_int - ([RRef (dummy_loc, glob_ZERO); - RRef (dummy_loc, glob_POS); - RRef (dummy_loc, glob_NEG)], - uninterp_z, - true) diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib index 03fb9c6295..3eb27abbb6 100644 --- a/parsing/highparsing.mllib +++ b/parsing/highparsing.mllib @@ -4,10 +4,4 @@ G_prim G_proofs G_tactic G_ltac -G_natsyntax -G_zsyntax -G_rsyntax -G_ascii_syntax -G_string_syntax G_decl_mode -G_intsyntax |