diff options
Diffstat (limited to 'plugins/syntax')
-rw-r--r-- | plugins/syntax/ascii_syntax.ml | 12 | ||||
-rw-r--r-- | plugins/syntax/nat_syntax.ml | 10 | ||||
-rw-r--r-- | plugins/syntax/numbers_syntax.ml | 46 | ||||
-rw-r--r-- | plugins/syntax/r_syntax.ml | 39 | ||||
-rw-r--r-- | plugins/syntax/string_syntax.ml | 12 | ||||
-rw-r--r-- | plugins/syntax/z_syntax.ml | 46 |
6 files changed, 83 insertions, 82 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 790e1970b..5c060c3d6 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -37,9 +37,9 @@ let interp_ascii dloc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - GRef (dloc,if Int.equal mp 0 then glob_false else glob_true) + GRef (dloc,if Int.equal mp 0 then glob_false else glob_true,None) :: (aux (n-1) (p/2)) in - GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p) + GApp (dloc,GRef(dloc,force glob_Ascii,None), aux 8 p) let interp_ascii_string dloc s = let p = @@ -55,12 +55,12 @@ let interp_ascii_string dloc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | GRef (_,k)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | GRef (_,k)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) + | GRef (_,k,_)::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | GRef (_,k,_)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l) | _ -> raise Non_closed_ascii in try let aux = function - | GApp (_,GRef (_,k),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l + | GApp (_,GRef (_,k,_),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -76,4 +76,4 @@ let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([GRef (Loc.ghost,static_glob_Ascii)], uninterp_ascii_string, true) + ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c3dad0a10..bad099d4f 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -30,8 +30,8 @@ let nat_of_int dloc n = 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 = GRef (dloc, glob_O) in - let ref_S = GRef (dloc, glob_S) in + let ref_O = GRef (dloc, glob_O, None) in + let ref_S = GRef (dloc, glob_S, None) in let rec mk_nat acc n = if n <> zero then mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) @@ -50,8 +50,8 @@ let nat_of_int dloc n = exception Non_closed_number let rec int_of_nat = function - | GApp (_,GRef (_,s),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) - | GRef (_,z) when Globnames.eq_gr z glob_O -> zero + | GApp (_,GRef (_,s,_),[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | GRef (_,z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number let uninterp_nat p = @@ -67,4 +67,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S); GRef (Loc.ghost,glob_O)], uninterp_nat, true) + ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index 8e09c974a..a6b3d9038 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -83,9 +83,9 @@ exception Non_closed (* 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 = GRef (dloc, int31_construct) in - let ref_0 = GRef (dloc, int31_0) in - let ref_1 = GRef (dloc, int31_1) in + let ref_construct = GRef (dloc, int31_construct, None) in + let ref_0 = GRef (dloc, int31_0, None) in + let ref_1 = GRef (dloc, int31_1, None) in let rec args counter n = if counter <= 0 then [] @@ -110,12 +110,12 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | (GRef (_,b))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | (GRef (_,b))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | (GRef (_,b,_))::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) + | (GRef (_,b,_))::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur)) | _ -> raise Non_closed in function - | GApp (_, GRef (_, c), args) when eq_gr c int31_construct -> args_parsing args zero + | GApp (_, GRef (_, c, _), args) when eq_gr c int31_construct -> args_parsing args zero | _ -> raise Non_closed let uninterp_int31 i = @@ -128,7 +128,7 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([GRef (Loc.ghost, int31_construct)], + ([GRef (Loc.ghost, int31_construct, None)], uninterp_int31, true) @@ -159,8 +159,8 @@ let height bi = (* n must be a non-negative integer (from bigint.ml) *) let word_of_pos_bigint dloc hght n = - let ref_W0 = GRef (dloc, zn2z_W0) in - let ref_WW = GRef (dloc, zn2z_WW) in + let ref_W0 = GRef (dloc, zn2z_W0, None) in + let ref_WW = GRef (dloc, zn2z_WW, None) in let rec decomp hgt n = if hgt <= 0 then int31_of_pos_bigint dloc n @@ -176,7 +176,7 @@ let word_of_pos_bigint dloc hght n = let bigN_of_pos_bigint dloc n = let h = height n in - let ref_constructor = GRef (dloc, bigN_constructor h) in + let ref_constructor = GRef (dloc, bigN_constructor h, None) in let word = word_of_pos_bigint dloc h n in let args = if h < n_inlined then [word] @@ -199,14 +199,14 @@ let interp_bigN dloc n = let bigint_of_word = let rec get_height rc = match rc with - | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW -> + | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW -> 1+max (get_height lft) (get_height rght) | _ -> 0 in let rec transform hght rc = match rc with - | GApp (_,GRef(_,c),_) when eq_gr c zn2z_W0-> zero - | GApp (_,GRef(_,c), [_;lft;rght]) when eq_gr c zn2z_WW-> + | GApp (_,GRef(_,c,_),_) when eq_gr c zn2z_W0-> zero + | GApp (_,GRef(_,c,_), [_;lft;rght]) when eq_gr c zn2z_WW-> let new_hght = hght-1 in add (mult (rank new_hght) (transform new_hght lft)) @@ -236,7 +236,7 @@ let uninterp_bigN rc = let bigN_list_of_constructors = let rec build i = if i < n_inlined+1 then - GRef (Loc.ghost, bigN_constructor i)::(build (i+1)) + GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1)) else [] in @@ -253,8 +253,8 @@ let _ = Notation.declare_numeral_interpreter bigN_scope (*** Parsing for bigZ in digital notation ***) let interp_bigZ dloc n = - let ref_pos = GRef (dloc, bigZ_pos) in - let ref_neg = GRef (dloc, bigZ_neg) in + let ref_pos = GRef (dloc, bigZ_pos, None) in + let ref_neg = GRef (dloc, bigZ_neg, None) in if is_pos_or_zero n then GApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n]) else @@ -262,8 +262,8 @@ let interp_bigZ dloc n = (* pretty printing functions for bigZ *) let bigint_of_bigZ = function - | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg - | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigZ_neg -> + | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_pos -> bigint_of_bigN one_arg + | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigZ_neg -> let opp_val = bigint_of_bigN one_arg in if equal opp_val zero then raise Non_closed @@ -282,19 +282,19 @@ let uninterp_bigZ rc = let _ = Notation.declare_numeral_interpreter bigZ_scope (bigZ_path, bigZ_module) interp_bigZ - ([GRef (Loc.ghost, bigZ_pos); - GRef (Loc.ghost, bigZ_neg)], + ([GRef (Loc.ghost, bigZ_pos, None); + GRef (Loc.ghost, bigZ_neg, None)], uninterp_bigZ, true) (*** Parsing for bigQ in digital notation ***) let interp_bigQ dloc n = - let ref_z = GRef (dloc, bigQ_z) in + let ref_z = GRef (dloc, bigQ_z, None) in GApp (dloc, ref_z, [interp_bigZ dloc n]) let uninterp_bigQ rc = try match rc with - | GApp (_, GRef(_,c), [one_arg]) when eq_gr c bigQ_z -> + | GApp (_, GRef(_,c,_), [one_arg]) when eq_gr c bigQ_z -> Some (bigint_of_bigZ one_arg) | _ -> None (* we don't pretty-print yet fractions *) with Non_closed -> None @@ -303,5 +303,5 @@ let uninterp_bigQ rc = let _ = Notation.declare_numeral_interpreter bigQ_scope (bigQ_path, bigQ_module) interp_bigQ - ([GRef (Loc.ghost, bigQ_z)], uninterp_bigQ, + ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ, true) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 545f205db..dac70c673 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -42,24 +42,24 @@ let four = mult_2 two (* Unary representation of strictly positive numbers *) let rec small_r dloc n = - if equal one n then GRef (dloc, glob_R1) - else GApp(dloc,GRef (dloc,glob_Rplus), - [GRef (dloc, glob_R1);small_r dloc (sub_1 n)]) + if equal one n then GRef (dloc, glob_R1, None) + else GApp(dloc,GRef (dloc,glob_Rplus, None), + [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)]) let r_of_posint dloc n = - let r1 = GRef (dloc, glob_R1) in + let r1 = GRef (dloc, glob_R1, None) 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 = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in - if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in - if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0) + let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in + if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in + if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None) let r_of_int dloc z = if is_strictly_neg z then - GApp (dloc, GRef(dloc,glob_Ropp), [r_of_posint dloc (neg z)]) + GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)]) else r_of_posint dloc z @@ -71,33 +71,33 @@ let bignat_of_r = (* for numbers > 1 *) let rec bignat_of_pos = function (* 1+1 *) - | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)]) + | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)]) when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two (* 1+(1+1) *) - | GApp (_,GRef (_,p1), [GRef (_,o1); - GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])]) + | GApp (_,GRef (_,p1,_), [GRef (_,o1,_); + GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])]) when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three (* (1+1)*b *) - | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult -> + | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult -> if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number; mult_2 (bignat_of_pos b) (* 1+(1+1)*b *) - | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])]) + | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])]) when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1 -> if not (Bigint.equal (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 - | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero - | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one + | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero + | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one | r -> bignat_of_pos r in bignat_of_r let bigint_of_r = function - | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp -> + | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp -> let n = bignat_of_r a in if Bigint.equal n zero then raise Non_closed_number; neg n @@ -109,11 +109,12 @@ let uninterp_r p = with Non_closed_number -> None +let mkGRef gr = GRef (Loc.ghost,gr,None) + let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([GRef(Loc.ghost,glob_Ropp);GRef(Loc.ghost,glob_R0); - GRef(Loc.ghost,glob_Rplus);GRef(Loc.ghost,glob_Rmult); - GRef(Loc.ghost,glob_R1)], + (List.map mkGRef + [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index 54206b453..2e696f391 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -32,8 +32,8 @@ open Lazy let interp_string dloc s = let le = String.length s in let rec aux n = - if n = le then GRef (dloc, force glob_EmptyString) else - GApp (dloc,GRef (dloc, force glob_String), + if n = le then GRef (dloc, force glob_EmptyString, None) else + GApp (dloc,GRef (dloc, force glob_String, None), [interp_ascii dloc (int_of_char s.[n]); aux (n+1)]) in aux 0 @@ -41,11 +41,11 @@ let uninterp_string r = try let b = Buffer.create 16 in let rec aux = function - | GApp (_,GRef (_,k),[a;s]) when eq_gr k (force glob_String) -> + | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) -> (match uninterp_ascii a with | Some c -> Buffer.add_char b (Char.chr c); aux s | _ -> raise Non_closed_string) - | GRef (_,z) when eq_gr z (force glob_EmptyString) -> + | GRef (_,z,_) when eq_gr z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -57,6 +57,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([GRef (Loc.ghost,static_glob_String); - GRef (Loc.ghost,static_glob_EmptyString)], + ([GRef (Loc.ghost,static_glob_String,None); + GRef (Loc.ghost,static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 67e54c017..5131a5f38 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -41,9 +41,9 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat dloc x = - let ref_xI = GRef (dloc, glob_xI) in - let ref_xH = GRef (dloc, glob_xH) in - let ref_xO = GRef (dloc, glob_xO) in + let ref_xI = GRef (dloc, glob_xI, None) in + let ref_xH = GRef (dloc, glob_xH, None) in + let ref_xO = GRef (dloc, glob_xO, None) in let rec pos_of x = match div2_with_rest x with | (q,false) -> GApp (dloc, ref_xO,[pos_of q]) @@ -65,9 +65,9 @@ let interp_positive dloc n = (**********************************************************************) let rec bignat_of_pos = function - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (_, a) when Globnames.eq_gr a glob_xH -> Bigint.one + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) + | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one | _ -> raise Non_closed_number let uninterp_positive p = @@ -83,9 +83,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([GRef (Loc.ghost, glob_xI); - GRef (Loc.ghost, glob_xO); - GRef (Loc.ghost, glob_xH)], + ([GRef (Loc.ghost, glob_xI, None); + GRef (Loc.ghost, glob_xO, None); + GRef (Loc.ghost, glob_xH, None)], uninterp_positive, true) @@ -104,9 +104,9 @@ let n_path = make_path binnums "N" let n_of_binnat dloc pos_or_neg n = if not (Bigint.equal n zero) then - GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n]) + GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n]) else - GRef (dloc, glob_N0) + GRef (dloc, glob_N0, None) let error_negative dloc = user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") @@ -120,8 +120,8 @@ let n_of_int dloc n = (**********************************************************************) let bignat_of_n = function - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a - | GRef (_, a) when Globnames.eq_gr a glob_N0 -> Bigint.zero + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a + | GRef (_, a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number let uninterp_n p = @@ -134,8 +134,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([GRef (Loc.ghost, glob_N0); - GRef (Loc.ghost, glob_Npos)], + ([GRef (Loc.ghost, glob_N0, None); + GRef (Loc.ghost, glob_Npos, None)], uninterp_n, true) @@ -157,18 +157,18 @@ let z_of_int dloc n = if not (Bigint.equal n zero) then let sgn, n = if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n]) + GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n]) else - GRef (dloc, glob_ZERO) + GRef (dloc, glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) let bigint_of_z = function - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (_, a) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a + | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number let uninterp_z p = @@ -182,8 +182,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([GRef (Loc.ghost, glob_ZERO); - GRef (Loc.ghost, glob_POS); - GRef (Loc.ghost, glob_NEG)], + ([GRef (Loc.ghost, glob_ZERO, None, None); + GRef (Loc.ghost, glob_POS, None, None); + GRef (Loc.ghost, glob_NEG, None, None)], uninterp_z, true) |