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

open Coqast
open Ast
open Pp
open Util
open Names
open Pcoq
open Extend
open Topconstr
open Libnames

(**********************************************************************)
(* Parsing R via scopes                                               *)
(**********************************************************************)

open Libnames
open Rawterm
open Bignat

let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]

(* TODO: temporary hack *)
let make_path dir id = Libnames.encode_kn dir (id_of_string id)

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 is_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 is_nonzero n then r_of_pos n else RRef(dloc,glob_R0)

let r_of_int dloc z =
  match z with
  | NEG n -> RApp (dloc, RRef(dloc,glob_Ropp), [r_of_posint dloc n]) 
  | POS n -> r_of_posint dloc n

(**********************************************************************)
(* Printing R via scopes                                              *)
(**********************************************************************)

exception Non_closed_number

(* 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

let bignat_of_r = function
  | RRef (_,a) when a = glob_R0 -> zero
  | RRef (_,a) when a = glob_R1 -> one
  | r -> bignat_of_pos r

let bigint_of_r = function
  | RApp (_,RRef (_,o), [a]) when o = glob_Ropp -> NEG (bignat_of_r a)
  | a -> POS (bignat_of_r a)

let uninterp_r p =
  try
    Some (bigint_of_r p)
  with Non_closed_number ->
    None

let _ = Symbols.declare_numeral_interpreter "R_scope"
  ["Coq";"Reals";"Rsyntax"]
  (r_of_int,None)
  ([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,
    None)