compilation native

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@201 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 157 insertions, 0 deletions

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)]]
+