From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/syntax/ascii_syntax.ml | 47 +++-- plugins/syntax/int31_syntax.ml | 105 ++++++++++ plugins/syntax/int31_syntax_plugin.mlpack | 1 + plugins/syntax/nat_syntax.ml | 38 ++-- plugins/syntax/numbers_syntax.ml | 311 ---------------------------- plugins/syntax/numbers_syntax_plugin.mlpack | 1 - plugins/syntax/r_syntax.ml | 181 ++++++++-------- plugins/syntax/string_syntax.ml | 40 ++-- plugins/syntax/z_syntax.ml | 107 +++++----- 9 files changed, 335 insertions(+), 496 deletions(-) create mode 100644 plugins/syntax/int31_syntax.ml create mode 100644 plugins/syntax/int31_syntax_plugin.mlpack delete mode 100644 plugins/syntax/numbers_syntax.ml delete mode 100644 plugins/syntax/numbers_syntax_plugin.mlpack (limited to 'plugins/syntax') diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index e18d19ce..acb297dd 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -1,10 +1,13 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Globnames.eq_gr r gr +| _ -> false + let ascii_module = ["Coq";"Strings";"Ascii"] let ascii_path = make_path ascii_module "ascii" @@ -37,34 +44,34 @@ let glob_Ascii = lazy (make_reference "Ascii") open Lazy -let interp_ascii dloc p = +let interp_ascii ?loc 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),None) + (DAst.make ?loc @@ GRef ((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,None), aux 8 p) + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p) -let interp_ascii_string dloc s = +let interp_ascii_string ?loc s = let p = if Int.equal (String.length s) 1 then int_of_char s.[0] else if Int.equal (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 + user_err ?loc ~hdr:"interp_ascii_string" + (str "Expects a single character or a three-digits ascii code.") in + interp_ascii ?loc p 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) + | r::l when is_gr r glob_true -> 1+2*(uninterp_bool_list (n-1) l) + | r::l when is_gr r 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 + let aux c = match DAst.get c with + | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l | _ -> raise Non_closed_ascii in Some (aux r) with @@ -74,10 +81,10 @@ 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 uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" (ascii_path,ascii_module) interp_ascii_string - ([GRef (Loc.ghost,static_glob_Ascii,None)], uninterp_ascii_string, true) + ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml new file mode 100644 index 00000000..5529ea70 --- /dev/null +++ b/plugins/syntax/int31_syntax.ml @@ -0,0 +1,105 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Globnames.eq_gr r gr +| _ -> false + +let make_mind mp id = Names.MutInd.make2 mp (Label.make id) +let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id +let make_mind_mpdot dir modname id = + let mp = ModPath.MPdot (ModPath.MPfile (make_dir dir), Label.make modname) + in make_mind mp id + + +(* int31 stuff *) +let int31_module = ["Coq"; "Numbers"; "Cyclic"; "Int31"; "Int31"] +let int31_path = make_path int31_module "int31" +let int31_id = make_mind_mpfile 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) + +(*** 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 ?loc n = + let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in + let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in + let ref_1 = DAst.make ?loc (GRef (int31_1, None)) 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 + DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) + +let error_negative ?loc = + CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.") + +let interp_int31 ?loc n = + if is_pos_or_zero n then + int31_of_pos_bigint ?loc n + else + error_negative ?loc + +(* Pretty prints an int31 *) + +let bigint_of_int31 = + let rec args_parsing args cur = + match args with + | [] -> cur + | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur) + | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur)) + | _ -> raise Non_closed + in + fun c -> match DAst.get c with + | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero + | _ -> raise Non_closed + +let uninterp_int31 (AnyGlobConstr 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 + ([DAst.make (GRef (int31_construct, None))], + uninterp_int31, + true) diff --git a/plugins/syntax/int31_syntax_plugin.mlpack b/plugins/syntax/int31_syntax_plugin.mlpack new file mode 100644 index 00000000..54a5bc0c --- /dev/null +++ b/plugins/syntax/int31_syntax_plugin.mlpack @@ -0,0 +1 @@ +Int31_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index a9eb126b..ad8b54d4 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -1,11 +1,14 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* zero then - mk_nat (GApp (dloc,ref_S, [acc])) (sub_1 n) + mk_nat (DAst.make ?loc @@ GApp (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") + user_err ?loc ~hdr:"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 - | 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 +let rec int_of_nat x = DAst.with_val (function + | GApp (r, [a]) -> + begin match DAst.get r with + | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a) + | _ -> raise Non_closed_number + end + | GRef (z,_) when Globnames.eq_gr z glob_O -> zero | _ -> raise Non_closed_number + ) x -let uninterp_nat p = +let uninterp_nat (AnyGlobConstr p) = try Some (int_of_nat p) with @@ -73,4 +81,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([GRef (Loc.ghost,glob_S,None); GRef (Loc.ghost,glob_O,None)], uninterp_nat, true) + ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml deleted file mode 100644 index f65f9b79..00000000 --- a/plugins/syntax/numbers_syntax.ml +++ /dev/null @@ -1,311 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 - | _ -> 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 - ([GRef (Loc.ghost, int31_construct, None)], - 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 31 - -(* base of the bigN of height N : (2^31)^(2^n) *) -let rank n = - let rec rk n pow2 = - if n <= 0 then pow2 - else rk (n-1) (mult pow2 pow2) - in rk n base - -(* 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 (n-1)) - -(* search the height of the Coq bigint needed to represent the integer bi *) -let height bi = - let rec hght n pow2 = - if less_than bi pow2 then n - else hght (n+1) (mult pow2 pow2) - in hght 0 base - -(* 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, 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 - else if equal n zero then - GApp (dloc, ref_W0, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None)]) - else - let (h,l) = split_at hgt n in - GApp (dloc, ref_WW, [GHole (dloc, Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None); - decomp (hgt-1) h; - decomp (hgt-1) l]) - in - decomp hght n - -let bigN_of_pos_bigint dloc n = - let h = height n 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] - else [Nat_syntax_plugin.Nat_syntax.nat_of_int dloc (of_int (h-n_inlined));word] - in - GApp (dloc, ref_constructor, args) - -let bigN_error_negative dloc = - CErrors.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 - | 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-> - let new_hght = hght-1 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 - | GApp (_,_,[one_arg]) -> bigint_of_word one_arg - | GApp (_,_,[_;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 i < n_inlined+1 then - GRef (Loc.ghost, bigN_constructor i,None)::(build (i+1)) - else - [] - in - build 0 - -(* 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 = 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 - GApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg 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 -> - 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 bigZ *) -let _ = Notation.declare_numeral_interpreter bigZ_scope - (bigZ_path, bigZ_module) - interp_bigZ - ([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, 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 -> - Some (bigint_of_bigZ one_arg) - | _ -> None (* we don't pretty-print yet fractions *) - with Non_closed -> None - -(* Actually declares the interpreter for bigQ *) -let _ = Notation.declare_numeral_interpreter bigQ_scope - (bigQ_path, bigQ_module) - interp_bigQ - ([GRef (Loc.ghost, bigQ_z, None)], uninterp_bigQ, - true) diff --git a/plugins/syntax/numbers_syntax_plugin.mlpack b/plugins/syntax/numbers_syntax_plugin.mlpack deleted file mode 100644 index e48c00a0..00000000 --- a/plugins/syntax/numbers_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Numbers_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 3ae2d45f..372e8ff3 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -1,14 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Globnames.eq_gr r gr +| _ -> false + +let positive_path = make_path binnums "positive" + +(* TODO: temporary hack *) +let make_kn dir id = Globnames.encode_mind dir id + +let positive_kn = make_kn (make_dir binnums) (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 ?loc x = + let ref_xI = DAst.make @@ GRef (glob_xI, None) in + let ref_xH = DAst.make @@ GRef (glob_xH, None) in + let ref_xO = DAst.make @@ GRef (glob_xO, None) in + let rec pos_of x = + match div2_with_rest x with + | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) + | (q,true) -> ref_xH + in + pos_of x + +(**********************************************************************) +(* Printing positive via scopes *) +(**********************************************************************) + +let rec bignat_of_pos c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r, [a]) when is_gr r 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 + +(**********************************************************************) +(* Parsing Z via scopes *) +(**********************************************************************) + +let z_path = make_path binnums "Z" +let z_kn = make_kn (make_dir binnums) (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 ?loc 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 + DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) + else + DAst.make @@ GRef (glob_ZERO, None) + +(**********************************************************************) +(* Printing Z via scopes *) +(**********************************************************************) + +let bigint_of_z c = match DAst.get c with + | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero + | _ -> raise Non_closed_number +(**********************************************************************) +(* Parsing R via scopes *) +(**********************************************************************) + +let rdefinitions = ["Coq";"Reals";"Rdefinitions"] let r_path = make_path rdefinitions "R" (* TODO: temporary hack *) let make_path dir id = Globnames.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 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, 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,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,None), [r_of_posint dloc (neg z)]) - else - r_of_posint dloc z +let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") + +let r_of_int ?loc z = + DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bignat_of_r = -(* for numbers > 1 *) -let rec bignat_of_pos = function - (* 1+1 *) - | 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,_)])]) - 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 -> - 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])]) - 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)) +let bigint_of_r c = match DAst.get c with + | GApp (r, [a]) when is_gr r glob_IZR -> + bigint_of_z a | _ -> 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 - | 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 -> - let n = bignat_of_r a in - if Bigint.equal n zero then raise Non_closed_number; - neg n - | a -> bignat_of_r a - -let uninterp_r p = + +let uninterp_r (AnyGlobConstr p) = try Some (bigint_of_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 - (List.map mkGRef - [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1], + ([DAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index de0fa77e..2421cc12 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -1,10 +1,12 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Globnames.eq_gr r gr +| _ -> false + open Lazy -let interp_string dloc s = +let interp_string ?loc s = let le = String.length s in let rec aux n = - 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)]) + if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else + DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None), + [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)]) in aux 0 -let uninterp_string r = +let uninterp_string (AnyGlobConstr r) = try let b = Buffer.create 16 in - let rec aux = function - | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) -> + let rec aux c = match DAst.get c with + | GApp (k,[a;s]) when is_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 @@ -61,6 +67,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([GRef (Loc.ghost,static_glob_String,None); - GRef (Loc.ghost,static_glob_EmptyString,None)], + ([DAst.make @@ GRef (static_glob_String,None); + DAst.make @@ GRef (static_glob_EmptyString,None)], uninterp_string, true) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 60803a36..d5300e47 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* GApp (dloc, ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q]) + | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) + | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (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 error_non_positive ?loc = + user_err ?loc ~hdr:"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 +let interp_positive ?loc n = + if is_strictly_pos n then pos_of_bignat ?loc n + else error_non_positive ?loc (**********************************************************************) (* Printing positive via scopes *) (**********************************************************************) -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 +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false + +let rec bignat_of_pos x = DAst.with_val (function + | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) + | GApp (r ,[a]) when is_gr r 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 + ) x -let uninterp_positive p = +let uninterp_positive (AnyGlobConstr p) = try Some (bignat_of_pos p) with Non_closed_number -> @@ -87,9 +94,9 @@ let uninterp_positive p = let _ = Notation.declare_numeral_interpreter "positive_scope" (positive_path,binnums) interp_positive - ([GRef (Loc.ghost, glob_xI, None); - GRef (Loc.ghost, glob_xO, None); - GRef (Loc.ghost, glob_xH, None)], + ([DAst.make @@ GRef (glob_xI, None); + DAst.make @@ GRef (glob_xO, None); + DAst.make @@ GRef (glob_xH, None)], uninterp_positive, true) @@ -106,29 +113,30 @@ let glob_Npos = ConstructRef path_of_Npos let n_path = make_path binnums "N" -let n_of_binnat dloc pos_or_neg n = +let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ if not (Bigint.equal n zero) then - GApp(dloc, GRef (dloc,glob_Npos,None), [pos_of_bignat dloc n]) + GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) else - GRef (dloc, glob_N0, None) + GRef(glob_N0, None) -let error_negative dloc = - user_err_loc (dloc, "interp_N", str "No negative numbers in type \"N\".") +let error_negative ?loc = + user_err ?loc ~hdr:"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 +let n_of_int ?loc n = + if is_pos_or_zero n then n_of_binnat ?loc true n + else error_negative ?loc (**********************************************************************) (* Printing N via scopes *) (**********************************************************************) -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 +let bignat_of_n n = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a + | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero | _ -> raise Non_closed_number + ) n -let uninterp_n p = +let uninterp_n (AnyGlobConstr p) = try Some (bignat_of_n p) with Non_closed_number -> None @@ -138,8 +146,8 @@ let uninterp_n p = let _ = Notation.declare_numeral_interpreter "N_scope" (n_path,binnums) n_of_int - ([GRef (Loc.ghost, glob_N0, None); - GRef (Loc.ghost, glob_Npos, None)], + ([DAst.make @@ GRef (glob_N0, None); + DAst.make @@ GRef (glob_Npos, None)], uninterp_n, true) @@ -157,25 +165,26 @@ 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 = +let z_of_int ?loc 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,None), [pos_of_bignat dloc n]) + DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - GRef (dloc, glob_ZERO, None) + DAst.make ?loc @@ GRef(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 +let bigint_of_z z = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a + | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) + | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number + ) z -let uninterp_z p = +let uninterp_z (AnyGlobConstr p) = try Some (bigint_of_z p) with Non_closed_number -> None @@ -186,8 +195,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([GRef (Loc.ghost, glob_ZERO, None); - GRef (Loc.ghost, glob_POS, None); - GRef (Loc.ghost, glob_NEG, None)], + ([DAst.make @@ GRef (glob_ZERO, None); + DAst.make @@ GRef (glob_POS, None); + DAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) -- cgit v1.2.3