From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 plugins/syntax/ascii_syntax.ml             |  83 ++++++++
 plugins/syntax/ascii_syntax_plugin.mllib   |   2 +
 plugins/syntax/nat_syntax.ml               |  78 +++++++
 plugins/syntax/nat_syntax_plugin.mllib     |   2 +
 plugins/syntax/numbers_syntax.ml           | 330 +++++++++++++++++++++++++++++
 plugins/syntax/numbers_syntax_plugin.mllib |   2 +
 plugins/syntax/r_syntax.ml                 | 125 +++++++++++
 plugins/syntax/r_syntax_plugin.mllib       |   2 +
 plugins/syntax/string_syntax.ml            |  69 ++++++
 plugins/syntax/string_syntax_plugin.mllib  |   2 +
 plugins/syntax/z_syntax.ml                 | 194 +++++++++++++++++
 plugins/syntax/z_syntax_plugin.mllib       |   2 +
 12 files changed, 891 insertions(+)
 create mode 100644 plugins/syntax/ascii_syntax.ml
 create mode 100644 plugins/syntax/ascii_syntax_plugin.mllib
 create mode 100644 plugins/syntax/nat_syntax.ml
 create mode 100644 plugins/syntax/nat_syntax_plugin.mllib
 create mode 100644 plugins/syntax/numbers_syntax.ml
 create mode 100644 plugins/syntax/numbers_syntax_plugin.mllib
 create mode 100644 plugins/syntax/r_syntax.ml
 create mode 100644 plugins/syntax/r_syntax_plugin.mllib
 create mode 100644 plugins/syntax/string_syntax.ml
 create mode 100644 plugins/syntax/string_syntax_plugin.mllib
 create mode 100644 plugins/syntax/z_syntax.ml
 create mode 100644 plugins/syntax/z_syntax_plugin.mllib

(limited to 'plugins/syntax')

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
-- 
cgit v1.2.3