(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.3                                 *)
(*                               July 1st 1999                              *)
(*                                                                          *)
(****************************************************************************)
(*                               g_zsyntax.ml                               *)
(****************************************************************************)

open CoqAst
open Pcoq
open Std
open Pp
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
      
      
(******** OLD
let z_of_string s dloc =
  let ((astxI,astxO,astxH),(astZERO,astPOS,astNEG),_) = get_z_sign dloc in
  if String.get s 0 = '-' then
    let v = int_array_of_string (String.sub s 1 (String.length s - 1)) in
    if is_nonzero v then
      ope("APPLIST",[astNEG; pos_of_int_array astxI astxO astxH v])
    else astZERO
  else
    let v = int_array_of_string s in
    if is_nonzero v then
      ope("APPLIST",[astPOS; 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 *)
Esyntax.Ppprim.add ("positive_printer", (outside_printer true));;
Esyntax.Ppprim.add ("negative_printer", (outside_printer false));;
Esyntax.Ppprim.add ("positive_printer_inside", (inside_printer true));;
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"
;; 

Gram.extend number None
 [None, None,
  [[Gramext.Stoken ("INT", "")],
   Gramext.action (z_of_string true)]]
;;

Gram.extend negnumber None
 [None, None,
  [[Gramext.Stoken ("INT", "")],
   Gramext.action (z_of_string false)]]
;;
