diff options
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 37 | ||||
| -rw-r--r-- | plugins/syntax/int31_syntax.ml | 35 | ||||
| -rw-r--r-- | plugins/syntax/n_syntax.ml | 81 | ||||
| -rw-r--r-- | plugins/syntax/n_syntax_plugin.mlpack | 1 | ||||
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 36 | ||||
| -rw-r--r-- | plugins/syntax/positive_syntax.ml | 101 | ||||
| -rw-r--r-- | plugins/syntax/positive_syntax_plugin.mlpack | 1 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 55 | ||||
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 38 | ||||
| -rw-r--r-- | plugins/syntax/z_syntax.ml | 157 |
10 files changed, 317 insertions, 225 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 6bf5b8cfca..47a59ba631 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -1,12 +1,13 @@ -(***********************************************************************) -(* 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 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "ascii_syntax_plugin" @@ -26,6 +27,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> GlobRef.equal r gr +| _ -> false + let ascii_module = ["Coq";"Strings";"Ascii"] let ascii_path = make_path ascii_module "ascii" @@ -43,9 +48,9 @@ let interp_ascii ?loc p = let rec aux n p = if Int.equal n 0 then [] else let mp = p mod 2 in - (CAst.make ?loc @@ GRef ((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 - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(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 ?loc s = let p = @@ -61,12 +66,12 @@ let interp_ascii_string ?loc s = let uninterp_ascii r = let rec uninterp_bool_list n = function | [] when Int.equal n 0 -> 0 - | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true -> 1+2*(uninterp_bool_list (n-1) l) - | { CAst.v = 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 - | { CAst.v = GApp ({ CAst.v = 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 @@ -76,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 - ([CAst.make @@ GRef (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 index fe1eef866c..f10f98e23b 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "int31_syntax_plugin" @@ -24,6 +25,10 @@ open Glob_term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> GlobRef.equal 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 = @@ -50,9 +55,9 @@ exception Non_closed (* 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 = CAst.make ?loc (GRef (int31_construct, None)) in - let ref_0 = CAst.make ?loc (GRef (int31_0, None)) in - let ref_1 = CAst.make ?loc (GRef (int31_1, None)) in + 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 [] @@ -60,7 +65,7 @@ let int31_of_pos_bigint ?loc n = let (q,r) = div2_with_rest n in (if r then ref_1 else ref_0)::(args (counter-1) q) in - CAst.make ?loc (GApp (ref_construct, List.rev (args 31 n))) + 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.") @@ -77,15 +82,15 @@ let bigint_of_int31 = let rec args_parsing args cur = match args with | [] -> cur - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur) - | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 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 - function - | { CAst.v = GApp ({ CAst.v = GRef (c, _) }, args) } when eq_gr c int31_construct -> args_parsing args zero + 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 i = +let uninterp_int31 (AnyGlobConstr i) = try Some (bigint_of_int31 i) with Non_closed -> @@ -95,6 +100,6 @@ let uninterp_int31 i = let _ = Notation.declare_numeral_interpreter int31_scope (int31_path, int31_module) interp_int31 - ([CAst.make (GRef (int31_construct, None))], + ([DAst.make (GRef (int31_construct, None))], uninterp_int31, true) diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml new file mode 100644 index 0000000000..0e202be47f --- /dev/null +++ b/plugins/syntax/n_syntax.ml @@ -0,0 +1,81 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Names +open Bigint +open Positive_syntax_plugin.Positive_syntax + +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "n_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + +(**********************************************************************) +(* Parsing N via scopes *) +(**********************************************************************) + +open Globnames +open Glob_term + +let binnums = ["Coq";"Numbers";"BinNums"] + +let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +(* TODO: temporary hack *) +let make_kn dir id = Globnames.encode_mind dir id + +let n_kn = make_kn (make_dir binnums) (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 binnums "N" + +let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ + if not (Bigint.equal n zero) then + GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) + else + GRef(glob_N0, None) + +let error_negative ?loc = + user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") + +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 n = DAst.with_val (function + | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a + | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero + | _ -> raise Non_closed_number + ) n + +let uninterp_n (AnyGlobConstr 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,binnums) + n_of_int + ([DAst.make @@ GRef (glob_N0, None); + DAst.make @@ GRef (glob_Npos, None)], + uninterp_n, + true) diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack new file mode 100644 index 0000000000..4c56645f07 --- /dev/null +++ b/plugins/syntax/n_syntax_plugin.mlpack @@ -0,0 +1 @@ +N_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c6ee899ed7..e158e0b516 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "nat_syntax_plugin" @@ -15,11 +16,12 @@ let () = Mltop.add_known_module __coq_plugin_name (* This file defines the printer for natural numbers in [nat] *) (*i*) +open Pp +open CErrors +open Names open Glob_term open Bigint open Coqlib -open Pp -open CErrors (*i*) (**********************************************************************) @@ -38,11 +40,11 @@ let warn_large_nat = let nat_of_int ?loc n = if is_pos_or_zero n then begin if less_than threshold n then warn_large_nat (); - let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in + let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in + let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in let rec mk_nat acc n = if n <> zero then - mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) + mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) else acc in @@ -57,13 +59,17 @@ let nat_of_int ?loc n = exception Non_closed_number -let rec int_of_nat x = CAst.with_val (function - | GApp ({ CAst.v = 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 GlobRef.equal s glob_S -> add_1 (int_of_nat a) + | _ -> raise Non_closed_number + end + | GRef (z,_) when GlobRef.equal 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 @@ -76,4 +82,4 @@ let _ = Notation.declare_numeral_interpreter "nat_scope" (nat_path,datatypes_module_name) nat_of_int - ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (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/positive_syntax.ml b/plugins/syntax/positive_syntax.ml new file mode 100644 index 0000000000..0c82e47445 --- /dev/null +++ b/plugins/syntax/positive_syntax.ml @@ -0,0 +1,101 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Pp +open CErrors +open Util +open Names +open Bigint + +(* Poor's man DECLARE PLUGIN *) +let __coq_plugin_name = "positive_syntax_plugin" +let () = Mltop.add_known_module __coq_plugin_name + +exception Non_closed_number + +(**********************************************************************) +(* Parsing positive via scopes *) +(**********************************************************************) + +open Globnames +open Glob_term + +let binnums = ["Coq";"Numbers";"BinNums"] + +let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) + +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 ?loc @@ GRef (glob_xI, None) in + let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in + let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in + let rec pos_of x = + match div2_with_rest x with + | (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 ?loc = + user_err ?loc ~hdr:"interp_positive" + (str "Only strictly positive numbers in type \"positive\".") + +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 is_gr c gr = match DAst.get c with +| GRef (r, _) -> GlobRef.equal 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 GlobRef.equal a glob_xH -> Bigint.one + | _ -> raise Non_closed_number + ) x + +let uninterp_positive (AnyGlobConstr 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,binnums) + interp_positive + ([DAst.make @@ GRef (glob_xI, None); + DAst.make @@ GRef (glob_xO, None); + DAst.make @@ GRef (glob_xH, None)], + uninterp_positive, + true) diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack new file mode 100644 index 0000000000..ac8f3c425c --- /dev/null +++ b/plugins/syntax/positive_syntax_plugin.mlpack @@ -0,0 +1 @@ +Positive_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 9cfa50071e..94aa143350 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -1,12 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API open Util open Names open Globnames @@ -28,6 +29,10 @@ let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> GlobRef.equal r gr +| _ -> false + let positive_path = make_path binnums "positive" (* TODO: temporary hack *) @@ -43,13 +48,13 @@ let glob_xO = ConstructRef path_of_xO let glob_xH = ConstructRef path_of_xH let pos_of_bignat ?loc x = - let ref_xI = CAst.make @@ GRef (glob_xI, None) in - let ref_xH = CAst.make @@ GRef (glob_xH, None) in - let ref_xO = CAst.make @@ GRef (glob_xO, None) in + 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) -> CAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q]) + | (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 @@ -58,10 +63,10 @@ let pos_of_bignat ?loc x = (* Printing positive via scopes *) (**********************************************************************) -let rec bignat_of_pos = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a)) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one +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 GlobRef.equal a glob_xH -> Bigint.one | _ -> raise Non_closed_number (**********************************************************************) @@ -82,18 +87,18 @@ 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 - CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) + DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else - CAst.make @@ GRef (glob_ZERO, None) + DAst.make @@ GRef (glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = function - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a) - | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero +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 GlobRef.equal a glob_ZERO -> Bigint.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -109,18 +114,18 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id) let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR") let r_of_int ?loc z = - CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) + DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z]) (**********************************************************************) (* Printing R via scopes *) (**********************************************************************) -let bigint_of_r = function - | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR -> +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 -let uninterp_r p = +let uninterp_r (AnyGlobConstr p) = try Some (bigint_of_r p) with Non_closed_number -> @@ -129,6 +134,6 @@ let uninterp_r p = let _ = Notation.declare_numeral_interpreter "R_scope" (r_path,["Coq";"Reals";"Rdefinitions"]) r_of_int - ([CAst.make @@ GRef (glob_IZR, None)], + ([DAst.make @@ GRef (glob_IZR, None)], uninterp_r, false) diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index a4335a508b..c22869f4d6 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -1,12 +1,14 @@ -(***********************************************************************) -(* 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 *) -(***********************************************************************) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) -open API +open Names open Globnames open Ascii_syntax_plugin.Ascii_syntax open Glob_term @@ -32,25 +34,29 @@ 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") +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> GlobRef.equal r gr +| _ -> false + open Lazy let interp_string ?loc s = let le = String.length s in let rec aux n = - if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else - CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None), + 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 - | { CAst.v = GApp ({ CAst.v = 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) - | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) -> + | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) -> Some (Buffer.contents b) | _ -> raise Non_closed_string @@ -62,6 +68,6 @@ let _ = Notation.declare_string_interpreter "string_scope" (string_path,["Coq";"Strings";"String"]) interp_string - ([CAst.make @@ GRef (static_glob_String,None); - CAst.make @@ GRef (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 719d8b1ccb..2534162e36 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -1,26 +1,23 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API -open Pp -open CErrors -open Util open Names open Bigint +open Positive_syntax_plugin.Positive_syntax (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "z_syntax_plugin" let () = Mltop.add_known_module __coq_plugin_name -exception Non_closed_number - (**********************************************************************) -(* Parsing positive via scopes *) +(* Parsing Z via scopes *) (**********************************************************************) open Globnames @@ -31,125 +28,9 @@ let binnums = ["Coq";"Numbers";"BinNums"] let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) -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 = CAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in - let rec pos_of x = - match div2_with_rest x with - | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -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 x = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a) - | GApp ({ CAst.v = 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 - ) x - -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,binnums) - interp_positive - ([CAst.make @@ GRef (glob_xI, None); - CAst.make @@ GRef (glob_xO, None); - CAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) - -(**********************************************************************) -(* Parsing N via scopes *) -(**********************************************************************) - -let n_kn = make_kn (make_dir binnums) (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 binnums "N" - -let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@ - if not (Bigint.equal n zero) then - GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) - else - GRef(glob_N0, None) - -let error_negative ?loc = - user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") - -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 = CAst.with_val (function - | GApp ({ CAst.v = 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 = - 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,binnums) - n_of_int - ([CAst.make @@ GRef (glob_N0, None); - CAst.make @@ GRef (glob_Npos, None)], - uninterp_n, - true) - -(**********************************************************************) -(* 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) @@ -164,22 +45,22 @@ 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 - CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) + DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) else - CAst.make ?loc @@ GRef(glob_ZERO, None) + DAst.make ?loc @@ GRef(glob_ZERO, None) (**********************************************************************) (* Printing Z via scopes *) (**********************************************************************) -let bigint_of_z = CAst.with_val (function - | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a - | GApp ({ CAst.v = 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 GlobRef.equal 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 @@ -190,8 +71,8 @@ let uninterp_z p = let _ = Notation.declare_numeral_interpreter "Z_scope" (z_path,binnums) z_of_int - ([CAst.make @@ GRef (glob_ZERO, None); - CAst.make @@ GRef (glob_POS, None); - CAst.make @@ GRef (glob_NEG, None)], + ([DAst.make @@ GRef (glob_ZERO, None); + DAst.make @@ GRef (glob_POS, None); + DAst.make @@ GRef (glob_NEG, None)], uninterp_z, true) |