aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_natsyntax.ml81
-rw-r--r--parsing/g_natsyntax.mli4
-rw-r--r--parsing/g_zsyntax.ml157
-rw-r--r--parsing/g_zsyntax.mli4
4 files changed, 246 insertions, 0 deletions
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
new file mode 100644
index 000000000..1c5b64623
--- /dev/null
+++ b/parsing/g_natsyntax.ml
@@ -0,0 +1,81 @@
+
+(* $Id$ *)
+
+(* This file to allow writing (3) for (S (S (S O)))
+ and still write (S y) for (S y) *)
+
+open Pcoq
+open Pp
+open Util
+open Names
+open Coqast
+open Ast
+
+exception Non_closed_number
+
+let get_nat_sign loc =
+ let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in
+ (ast_of_id "O", ast_of_id "S", ast_of_id "My_special_variable")
+
+(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
+let nat_of_int n dloc =
+ let (astO,astS,_) = get_nat_sign dloc in
+ let rec mk_nat n =
+ if n <= 0 then
+ astO
+ else
+ Node(dloc,"APPLIST", [astS; mk_nat (n-1)])
+ in
+ mk_nat n
+
+let nat_of_string s dloc =
+ nat_of_int (int_of_string s) dloc
+
+let rec int_of_nat_rec astS astO p =
+ match p with
+ | Node (_,"APPLIST", [b; a]) when alpha_eq(b,astS) ->
+ (int_of_nat_rec astS astO a)+1
+ | a when alpha_eq(a,astO) -> 1
+ (***** YES, 1, non 0 ... to print the successor of p *)
+ | _ -> raise Non_closed_number
+
+let int_of_nat p =
+ let (astO,astS,_) = get_nat_sign dummy_loc in
+ try
+ Some (int_of_nat_rec astS astO p)
+ with
+ Non_closed_number -> None
+
+let replace_S p =
+ let (_,astS,astmyvar) = get_nat_sign dummy_loc in
+ let rec aux p =
+ match p with
+ | Node (l,"APPLIST", [b; a]) when b = astS ->
+ Node (l, "APPLIST", [astmyvar; (aux a)])
+ | _ -> p
+ in
+ ope("APPLIST", [astmyvar; (aux p)])
+
+
+(* Declare the primitive printer *)
+
+(* Prints not p, but the SUCCESSOR of p !!!!! *)
+let nat_printer std_pr p =
+ match (int_of_nat p) with
+ | Some i -> [< 'sTR (string_of_int i) >]
+ | None -> std_pr (replace_S p)
+
+let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
+
+(* Declare the primitive parser *)
+
+let number =
+ match create_entry (get_univ "nat") "number" ETast with
+ | Ast n -> n
+ | _ -> anomaly "G_natsyntax : create_entry number failed"
+
+let _ =
+ Gram.extend number None
+ [None, None,
+ [[Gramext.Stoken ("INT", "")],
+ Gramext.action nat_of_string]]
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
new file mode 100644
index 000000000..61f305ad9
--- /dev/null
+++ b/parsing/g_natsyntax.mli
@@ -0,0 +1,4 @@
+
+(* $Id$ *)
+
+(* Nice syntax for naturals. *)
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
new file mode 100644
index 000000000..8128cb3d9
--- /dev/null
+++ b/parsing/g_zsyntax.ml
@@ -0,0 +1,157 @@
+
+(* $Id$ *)
+
+open Coqast
+open Pcoq
+open Pp
+open Util
+open Names
+open Ast
+
+let get_z_sign loc =
+ let ast_of_id id = Astterm.globalize_command (Nvar(loc,id)) in
+ ((ast_of_id "xI", ast_of_id "xO", ast_of_id "xH"),
+ (ast_of_id "ZERO", ast_of_id "POS", ast_of_id "NEG"),
+ (ast_of_id "My_special_variable0", ast_of_id "My_special_variable1"))
+
+let int_array_of_string s =
+ let a = Array.create (String.length s) 0 in
+ for i = 0 to String.length s - 1 do
+ a.(i) <- int_of_string (String.sub s i 1)
+ done;
+ a
+
+let string_of_int_array s =
+ String.concat "" (Array.to_list (Array.map string_of_int s))
+
+let is_nonzero a =
+ let b = ref false in Array.iter (fun x -> b := x <> 0 || !b) a; !b
+
+let div2_with_rest n =
+ let len = Array.length n in
+ let q = Array.create len 0 in
+ for i = 0 to len - 2 do
+ q.(i) <- q.(i) + n.(i) / 2; q.(i + 1) <- 5 * (n.(i) mod 2)
+ done;
+ q.(len - 1) <- q.(len - 1) + n.(len - 1) / 2;
+ q, n.(len - 1) mod 2
+
+let add_1 n =
+ let m = Array.copy n
+ and i = ref (Array.length n - 1) in
+ m.(!i) <- m.(!i) + 1;
+ while m.(!i) = 10 && !i > 0 do
+ m.(!i) <- 0; decr i; m.(!i) <- m.(!i) + 1
+ done;
+ if !i = 0 && m.(0) = 10 then begin
+ m.(0) <- 0; Array.concat [[| 1 |]; m]
+ end else
+ m
+
+let rec mult_2 n =
+ let m = Array.copy n in
+ m.(Array.length n - 1) <- 2 * m.(Array.length n - 1);
+ for i = Array.length n - 2 downto 0 do
+ m.(i) <- 2 * m.(i);
+ if m.(i + 1) >= 10 then begin
+ m.(i + 1) <- m.(i + 1) - 10; m.(i) <- m.(i) + 1
+ end
+ done;
+ if m.(0) >= 10 then begin
+ m.(0) <- m.(0) - 10; Array.concat [[| 1 |]; m]
+ end else
+ m
+
+let pos_of_int_array astxI astxO astxH x =
+ let rec pos_of x =
+ match div2_with_rest x with
+ | (q, 1) ->
+ if is_nonzero q then ope("APPLIST", [astxI; pos_of q]) else astxH
+ | (q, 0) -> ope("APPLIST", [astxO; pos_of q])
+ | _ -> anomaly "n mod 2 is neither 1 nor 0. Do you bielive that ?"
+ in
+ pos_of x
+
+let z_of_string pos_or_neg s dloc =
+ let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG),_) = get_z_sign dloc in
+ let v = int_array_of_string s in
+ if is_nonzero v then
+ if pos_or_neg then
+ ope("APPLIST",[astPOS; pos_of_int_array astxI astxO astxH v])
+ else
+ ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v])
+ else
+ astZERO
+
+exception Non_closed_number
+
+let rec int_array_of_pos c1 c2 c3 p =
+ match p with
+ | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c1) ->
+ mult_2 (int_array_of_pos c1 c2 c3 a)
+ | Node (_,"APPLIST", [b; a]) when alpha_eq(b,c2) ->
+ add_1 (mult_2 (int_array_of_pos c1 c2 c3 a))
+ | a when alpha_eq(a,c3) -> [| 1 |]
+ | _ -> raise Non_closed_number
+
+let int_array_option_of_pos astxI astxO astxH p =
+ try
+ Some (int_array_of_pos astxO astxI astxH p)
+ with Non_closed_number ->
+ None
+
+let inside_printer posneg std_pr p =
+ let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in
+ match (int_array_option_of_pos astxI astxO astxH p) with
+ | Some n ->
+ if posneg then
+ [< 'sTR (string_of_int_array n) >]
+ else
+ [< 'sTR "(-"; 'sTR (string_of_int_array n); 'sTR ")" >]
+ | None ->
+ let c = if posneg then myvar0 else myvar1 in
+ std_pr (ope("ZEXPR",[ope("APPLIST",[c; p])]))
+
+let outside_printer posneg std_pr p =
+ let ((astxI,astxO,astxH),_,(myvar0,myvar1)) = get_z_sign dummy_loc in
+ match (int_array_option_of_pos astxI astxO astxH p) with
+ | Some n ->
+ if posneg then
+ [< 'sTR "`"; 'sTR (string_of_int_array n); 'sTR "`">]
+ else
+ [< 'sTR "`-"; 'sTR (string_of_int_array n); 'sTR "`" >]
+ | None ->
+ let c = if posneg then myvar0 else myvar1 in
+ [< 'sTR "("; std_pr (ope("APPLIST",[c; p])); 'sTR ")" >]
+
+(* Declare pretty-printers for integers *)
+let _ = Esyntax.Ppprim.add ("positive_printer", (outside_printer true))
+let _ = Esyntax.Ppprim.add ("negative_printer", (outside_printer false))
+let _ = Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true))
+let _ = Esyntax.Ppprim.add ("negative_printer_inside", (inside_printer false))
+
+(* Declare the primitive parser *)
+open Pcoq
+
+let number =
+ match create_entry (get_univ "znatural") "number" ETast with
+ | Ast n -> n
+ | _ -> anomaly "G_zsyntax.number"
+
+let negnumber =
+ match create_entry (get_univ "znatural") "negnumber" ETast with
+ | Ast n -> n
+ | _ -> anomaly "G_zsyntax.negnumber"
+
+let _ =
+ Gram.extend number None
+ [None, None,
+ [[Gramext.Stoken ("INT", "")],
+ Gramext.action (z_of_string true)]]
+
+let _ =
+ Gram.extend negnumber None
+ [None, None,
+ [[Gramext.Stoken ("INT", "")],
+ Gramext.action (z_of_string false)]]
+
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
new file mode 100644
index 000000000..310d09a12
--- /dev/null
+++ b/parsing/g_zsyntax.mli
@@ -0,0 +1,4 @@
+
+(* $Id$ *)
+
+(* Nice syntax for integers. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 04:54:52 +0000