summaryrefslogtreecommitdiff
path: root/plugins/syntax
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/ascii_syntax.ml83
-rw-r--r--plugins/syntax/ascii_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/nat_syntax.ml78
-rw-r--r--plugins/syntax/nat_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/numbers_syntax.ml330
-rw-r--r--plugins/syntax/numbers_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/r_syntax.ml125
-rw-r--r--plugins/syntax/r_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/string_syntax.ml69
-rw-r--r--plugins/syntax/string_syntax_plugin.mllib2
-rw-r--r--plugins/syntax/z_syntax.ml194
-rw-r--r--plugins/syntax/z_syntax_plugin.mllib2
12 files changed, 891 insertions, 0 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
new file mode 100644
index 00000000..19473dfa
--- /dev/null
+++ b/plugins/syntax/ascii_syntax.ml
@@ -0,0 +1,83 @@
+(***********************************************************************)
+(* 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_mind (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/plugins/syntax/ascii_syntax_plugin.mllib b/plugins/syntax/ascii_syntax_plugin.mllib
new file mode 100644
index 00000000..b00f9250
--- /dev/null
+++ b/plugins/syntax/ascii_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Ascii_syntax
+Ascii_syntax_plugin_mod
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
new file mode 100644
index 00000000..5d20c2a3
--- /dev/null
+++ b/plugins/syntax/nat_syntax.ml
@@ -0,0 +1,78 @@
+(************************************************************************)
+(* 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/plugins/syntax/nat_syntax_plugin.mllib b/plugins/syntax/nat_syntax_plugin.mllib
new file mode 100644
index 00000000..69b0cb20
--- /dev/null
+++ b/plugins/syntax/nat_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Nat_syntax
+Nat_syntax_plugin_mod
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
new file mode 100644
index 00000000..4375d5e0
--- /dev/null
+++ b/plugins/syntax/numbers_syntax.ml
@@ -0,0 +1,330 @@
+(************************************************************************)
+(* 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 int31 / bigN / bigZ / bigQ constructors ***)
+
+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)
+
+let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
+let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
+let make_mind_mpdot dir modname id =
+ let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label 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)
+
+
+(* bigN stuff*)
+let zn2z_module = ["Coq"; "Numbers"; "Cyclic"; "DoubleCyclic"; "DoubleType"]
+let zn2z_path = make_path zn2z_module "zn2z"
+let zn2z_id = make_mind_mpfile 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"
+let bigN_t = make_mind_mpdot bigN_module "BigN" "t_"
+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_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"
+let bigZ_t = make_mind_mpdot bigZ_module "BigZ" "t_"
+let bigZ_scope = "bigZ_scope"
+
+let bigZ_pos = ConstructRef ((bigZ_t,0),1)
+let bigZ_neg = ConstructRef ((bigZ_t,0),2)
+
+
+(*bigQ stuff*)
+let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"]
+let bigQ_path = make_path (bigQ_module@["BigQ"]) "t"
+let bigQ_t = make_mind_mpdot bigQ_module "BigQ" "t_"
+let bigQ_scope = "bigQ_scope"
+
+let bigQ_z = ConstructRef ((bigQ_t,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
+ [Nat_syntax.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 bigZ *)
+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
+ RApp (dloc, ref_z, [interp_bigZ dloc n])
+
+let uninterp_bigQ rc =
+ try match rc with
+ | RApp (_, RRef(_,c), [one_arg]) when 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
+ ([RRef (Util.dummy_loc, bigQ_z)], uninterp_bigQ,
+ true)
diff --git a/plugins/syntax/numbers_syntax_plugin.mllib b/plugins/syntax/numbers_syntax_plugin.mllib
new file mode 100644
index 00000000..ebc0bb20
--- /dev/null
+++ b/plugins/syntax/numbers_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Numbers_syntax
+Numbers_syntax_plugin_mod
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
new file mode 100644
index 00000000..f85309e6
--- /dev/null
+++ b/plugins/syntax/r_syntax.ml
@@ -0,0 +1,125 @@
+(************************************************************************)
+(* 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/plugins/syntax/r_syntax_plugin.mllib b/plugins/syntax/r_syntax_plugin.mllib
new file mode 100644
index 00000000..5c173a14
--- /dev/null
+++ b/plugins/syntax/r_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+R_syntax
+R_syntax_plugin_mod
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
new file mode 100644
index 00000000..bc02357a
--- /dev/null
+++ b/plugins/syntax/string_syntax.ml
@@ -0,0 +1,69 @@
+(***********************************************************************)
+(* 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 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/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib
new file mode 100644
index 00000000..b108c9e0
--- /dev/null
+++ b/plugins/syntax/string_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+String_syntax
+String_syntax_plugin_mod
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
new file mode 100644
index 00000000..f6afd080
--- /dev/null
+++ b/plugins/syntax/z_syntax.ml
@@ -0,0 +1,194 @@
+(************************************************************************)
+(* 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_mind 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/plugins/syntax/z_syntax_plugin.mllib b/plugins/syntax/z_syntax_plugin.mllib
new file mode 100644
index 00000000..36d41acc
--- /dev/null
+++ b/plugins/syntax/z_syntax_plugin.mllib
@@ -0,0 +1,2 @@
+Z_syntax
+Z_syntax_plugin_mod
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 20:23:29 +0000