(************************************************************************)
(*  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 $ $ i*)

(* digit-based syntax for int31, bigN bigZ and bigQ *)

open Bigint
open Libnames
open Rawterm

(*** Constants for locating the int31 and bigN ***)



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)

(* copied on g_zsyntax.ml, where it is said to be a temporary hack*)
(* takes a path an identifier in the form of a string list and a string, 
   returns a kernel_name *)
let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id)


(* int31 stuff *)
let int31_module = ["Coq"; "Ints"; "Int31"]
let int31_path = make_path int31_module "int31"
let int31_id = make_kn 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"; "Ints"; "Basic_type"]
let zn2z_path = make_path zn2z_module "zn2z"
let zn2z_id = make_kn zn2z_module

let zn2z_W0 = ConstructRef ((zn2z_id "zn2z",0),1)
let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2)

let bigN_module = ["Coq"; "Ints"; "BigN"]
let bigN_path = make_path bigN_module "bigN"
(* big ugly hack *)
let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), 
                             Names.mk_label "BigN")),
              [], Names.id_of_string id) : Names.kernel_name)
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 "13"
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_id "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"; "Ints"; "BigZ"]
let bigZ_path = make_path bigZ_module "bigZ"
(* big ugly hack bis *)
let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), 
                             Names.mk_label "BigZ")),
              [], Names.id_of_string id) : Names.kernel_name)
let bigZ_scope = "bigZ_scope"

let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1)
let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2)


(*bigQ stuff*)
let bigQ_module = ["Coq"; "Ints"; "num"; "BigQ"]
let qmake_module = ["Coq"; "Ints"; "num"; "QMake_base"]
let bigQ_path = make_path bigQ_module "bigQ"
(* big ugly hack bis *)
let bigQ_id = make_kn qmake_module
let bigQ_scope = "bigQ_scope"

let bigQ_z =  ConstructRef ((bigQ_id "q_type",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
				                      [RHole (dloc, Evd.InternalHole);
						       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 bigN *)
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
  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_z,
       [RApp (dloc, ref_pos, [bigN_of_pos_bigint dloc n])])
  else
    RApp (dloc, ref_z,
       [RApp (dloc, ref_neg, [bigN_of_pos_bigint dloc (neg n)])])

let uninterp_bigQ rc = None


(* Actually declares the interpreter for bigQ *)
let _ = Notation.declare_numeral_interpreter bigQ_scope
  (bigQ_path, bigQ_module)
  interp_bigQ
  ([], uninterp_bigQ,
   true)