(* Reduction of native operators *)
open Names
open CPrimitives
open Retroknowledge
open Environ
open CErrors

type _ action_kind =
  | IncompatTypes : _ prim_type -> Constant.t action_kind
  | IncompatInd : _ prim_ind -> inductive action_kind

type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn

let check_same_types typ c1 c2 =
  if not (Constant.equal c1 c2)
  then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))

let check_same_inds ind i1 i2 =
  if not (eq_ind i1 i2)
  then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))

let add_retroknowledge retro action =
  match action with
  | Register_type(typ,c) ->
    begin match typ with
      | PT_int63 ->
        (match retro.retro_int63 with
         | None -> { retro with retro_int63 = Some c }
         | Some c' -> check_same_types typ c c'; retro)

      | PT_float64 ->
        (match retro.retro_float64 with
         | None -> { retro with retro_float64 = Some c }
         | Some c' -> check_same_types typ c c'; retro)

      | PT_array ->
        (match retro.retro_array with
         | None -> { retro with retro_array = Some c }
         | Some c' -> check_same_types typ c c'; retro)
    end

  | Register_ind(pit,ind) ->
    begin match pit with
      | PIT_bool ->
        let r =
          match retro.retro_bool with
          | None -> ((ind,1), (ind,2))
          | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
        { retro with retro_bool = Some r }
      | PIT_carry ->
        let r =
          match retro.retro_carry with
          | None -> ((ind,1), (ind,2))
          | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
        { retro with retro_carry = Some r }
      | PIT_pair ->
        let r =
          match retro.retro_pair with
          | None -> (ind,1)
          | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in
        { retro with retro_pair = Some r }
      | PIT_cmp ->
        let r =
          match retro.retro_cmp with
          | None -> ((ind,1), (ind,2), (ind,3))
          | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in
        { retro with retro_cmp = Some r }
      | PIT_f_cmp ->
        let r =
          match retro.retro_f_cmp with
          | None -> ((ind,1), (ind,2), (ind,3), (ind,4))
          | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in
        { retro with retro_f_cmp = Some r }
      | PIT_f_class ->
        let r =
          match retro.retro_f_class with
          | None -> ((ind,1), (ind,2), (ind,3), (ind,4),
                     (ind,5), (ind,6), (ind,7), (ind,8),
                     (ind,9))
          | Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
            check_same_inds pit ind ind'; t in
        { retro with retro_f_class = Some r }
    end

let add_retroknowledge env action =
  set_retroknowledge env (add_retroknowledge env.retroknowledge action)

let get_int_type env =
  match env.retroknowledge.retro_int63 with
  | Some c -> c
  | None -> anomaly Pp.(str"Reduction of primitive: int63 not registered")

let get_float_type env =
  match env.retroknowledge.retro_float64 with
  | Some c -> c
  | None -> anomaly Pp.(str"Reduction of primitive: float64 not registered")

let get_cmp_type env =
  match env.retroknowledge.retro_cmp with
  | Some (((mindcmp,_),_),_,_) ->
     Constant.make (MutInd.user mindcmp) (MutInd.canonical mindcmp)
  | None -> anomaly Pp.(str"Reduction of primitive: comparison not registered")

let get_bool_constructors env =
  match env.retroknowledge.retro_bool with
  | Some r -> r
  | None -> anomaly Pp.(str"Reduction of primitive: bool not registered")

let get_carry_constructors env =
  match env.retroknowledge.retro_carry with
  | Some r -> r
  | None -> anomaly Pp.(str"Reduction of primitive: carry not registered")

let get_pair_constructor env =
  match env.retroknowledge.retro_pair with
  | Some c  -> c
  | None -> anomaly Pp.(str"Reduction of primitive: pair not registered")

let get_cmp_constructors env =
  match env.retroknowledge.retro_cmp with
  | Some r -> r
  | None -> anomaly Pp.(str"Reduction of primitive: cmp not registered")

let get_f_cmp_constructors env =
  match env.retroknowledge.retro_f_cmp with
  | Some r -> r
  | None -> anomaly Pp.(str"Reduction of primitive: fcmp not registered")

let get_f_class_constructors env =
  match env.retroknowledge.retro_f_class with
  | Some r -> r
  | None -> anomaly Pp.(str"Reduction of primitive: fclass not registered")

exception NativeDestKO

module type RedNativeEntries =
  sig
    type elem
    type args
    type evd (* will be unit in kernel, evar_map outside *)
    type uinstance

    val get : args -> int -> elem
    val get_int : evd -> elem -> Uint63.t
    val get_float : evd -> elem -> Float64.t
    val get_parray : evd -> elem -> elem Parray.t
    val mkInt : env -> Uint63.t -> elem
    val mkFloat : env -> Float64.t -> elem
    val mkBool : env -> bool -> elem
    val mkCarry : env -> bool -> elem -> elem (* true if carry *)
    val mkIntPair : env -> elem -> elem -> elem
    val mkFloatIntPair : env -> elem -> elem -> elem
    val mkLt : env -> elem
    val mkEq : env -> elem
    val mkGt : env -> elem
    val mkFLt : env -> elem
    val mkFEq : env -> elem
    val mkFGt : env -> elem
    val mkFNotComparable : env -> elem
    val mkPNormal : env -> elem
    val mkNNormal : env -> elem
    val mkPSubn : env -> elem
    val mkNSubn : env -> elem
    val mkPZero : env -> elem
    val mkNZero : env -> elem
    val mkPInf : env -> elem
    val mkNInf : env -> elem
    val mkNaN : env -> elem
    val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem
  end

module type RedNative =
 sig
   type elem
   type args
   type evd
   type uinstance
   val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option
 end

module RedNative (E:RedNativeEntries) :
  RedNative with type elem = E.elem
  with type args = E.args
  with type evd = E.evd
  with type uinstance = E.uinstance =
struct
  type elem = E.elem
  type args = E.args
  type evd = E.evd
  type uinstance = E.uinstance

  let get_int evd args i = E.get_int evd (E.get args i)

  let get_int1 evd args = get_int evd args 0

  let get_int2 evd args = get_int evd args 0, get_int evd args 1

  let get_int3 evd args =
    get_int evd args 0, get_int evd args 1, get_int evd args 2

  let get_float evd args i = E.get_float evd (E.get args i)

  let get_float1 evd args = get_float evd args 0

  let get_float2 evd args = get_float evd args 0, get_float evd args 1

  let get_parray evd args i = E.get_parray evd (E.get args i)

  let red_prim_aux env evd op u args =
    let open CPrimitives in
    match op with
    | Int63head0 ->
      let i = get_int1 evd args in E.mkInt env (Uint63.head0 i)
    | Int63tail0 ->
      let i = get_int1 evd args in E.mkInt env (Uint63.tail0 i)
    | Int63add ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.add i1 i2)
    | Int63sub ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.sub i1 i2)
    | Int63mul ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.mul i1 i2)
    | Int63div ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2)
    | Int63mod ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2)
    | Int63lsr ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2)
    | Int63lsl ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2)
    | Int63land ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2)
    | Int63lor ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_or i1 i2)
    | Int63lxor ->
      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_xor i1 i2)
    | Int63addc ->
      let i1, i2 = get_int2 evd args in
      let s = Uint63.add i1 i2 in
      E.mkCarry env (Uint63.lt s i1) (E.mkInt env s)
    | Int63subc ->
      let i1, i2 = get_int2 evd args in
      let s = Uint63.sub i1 i2 in
      E.mkCarry env (Uint63.lt i1 i2) (E.mkInt env s)
    | Int63addCarryC  ->
      let i1, i2 = get_int2 evd args in
      let s = Uint63.add (Uint63.add i1 i2) (Uint63.of_int 1) in
      E.mkCarry env (Uint63.le s i1) (E.mkInt env s)
    | Int63subCarryC  ->
      let i1, i2 = get_int2 evd args in
      let s = Uint63.sub (Uint63.sub i1 i2) (Uint63.of_int 1) in
      E.mkCarry env (Uint63.le i1 i2) (E.mkInt env s)
    | Int63mulc ->
      let i1, i2 = get_int2 evd args in
      let (h, l) = Uint63.mulc i1 i2 in
      E.mkIntPair env (E.mkInt env h) (E.mkInt env l)
    | Int63diveucl ->
      let i1, i2 = get_int2 evd args in
      let q,r = Uint63.div i1 i2, Uint63.rem i1 i2 in
      E.mkIntPair env (E.mkInt env q) (E.mkInt env r)
    | Int63div21 ->
      let i1, i2, i3 = get_int3 evd args in
      let q,r = Uint63.div21 i1 i2 i3 in
      E.mkIntPair env (E.mkInt env q) (E.mkInt env r)
    | Int63addMulDiv ->
      let p, i, j = get_int3 evd args in
      E.mkInt env
        (Uint63.l_or
           (Uint63.l_sl i p)
           (Uint63.l_sr j (Uint63.sub (Uint63.of_int Uint63.uint_size) p)))
    | Int63eq ->
      let i1, i2 = get_int2 evd args in
      E.mkBool env (Uint63.equal i1 i2)
    | Int63lt ->
      let i1, i2 = get_int2 evd args in
      E.mkBool env (Uint63.lt i1 i2)
    | Int63le ->
      let i1, i2 = get_int2 evd args in
      E.mkBool env (Uint63.le i1 i2)
    | Int63compare ->
      let i1, i2 = get_int2 evd args in
      begin match Uint63.compare i1 i2 with
        | x when x < 0 ->  E.mkLt env
        | 0 -> E.mkEq env
        | _ -> E.mkGt env
      end
    | Float64opp ->
      let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
    | Float64abs ->
      let f = get_float1 evd args in E.mkFloat env (Float64.abs f)
    | Float64eq ->
      let i1, i2 = get_float2 evd args in
      E.mkBool env (Float64.eq i1 i2)
    | Float64lt ->
      let i1, i2 = get_float2 evd args in
      E.mkBool env (Float64.lt i1 i2)
    | Float64le ->
      let i1, i2 = get_float2 evd args in
      E.mkBool env (Float64.le i1 i2)
    | Float64compare ->
      let f1, f2 = get_float2 evd args in
      (match Float64.compare f1 f2 with
      | Float64.FEq -> E.mkFEq env
      | Float64.FLt -> E.mkFLt env
      | Float64.FGt -> E.mkFGt env
      | Float64.FNotComparable -> E.mkFNotComparable env)
    | Float64classify ->
      let f = get_float1 evd args in
      (match Float64.classify f with
      | Float64.PNormal -> E.mkPNormal env
      | Float64.NNormal -> E.mkNNormal env
      | Float64.PSubn -> E.mkPSubn env
      | Float64.NSubn -> E.mkNSubn env
      | Float64.PZero -> E.mkPZero env
      | Float64.NZero -> E.mkNZero env
      | Float64.PInf -> E.mkPInf env
      | Float64.NInf -> E.mkNInf env
      | Float64.NaN -> E.mkNaN env)
    | Float64add ->
      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.add f1 f2)
    | Float64sub ->
      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.sub f1 f2)
    | Float64mul ->
      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.mul f1 f2)
    | Float64div ->
      let f1, f2 = get_float2 evd args in E.mkFloat env (Float64.div f1 f2)
    | Float64sqrt ->
      let f = get_float1 evd args in E.mkFloat env (Float64.sqrt f)
    | Float64ofInt63 ->
      let i = get_int1 evd args in E.mkFloat env (Float64.of_int63 i)
    | Float64normfr_mantissa ->
      let f = get_float1 evd args in E.mkInt env (Float64.normfr_mantissa f)
    | Float64frshiftexp ->
      let f = get_float1 evd args in
      let (m,e) = Float64.frshiftexp f in
      E.mkFloatIntPair env (E.mkFloat env m) (E.mkInt env e)
    | Float64ldshiftexp ->
      let f = get_float evd args 0 in
      let e = get_int evd args 1 in
      E.mkFloat env (Float64.ldshiftexp f e)
    | Float64next_up ->
      let f = get_float1 evd args in E.mkFloat env (Float64.next_up f)
    | Float64next_down ->
      let f = get_float1 evd args in E.mkFloat env (Float64.next_down f)
    | Arraymake ->
      let ty = E.get args 0 in
      let i = get_int evd args 1 in
      let d = E.get args 2 in
      E.mkArray env u (Parray.make i d) ty
    | Arrayget ->
      let t = get_parray evd args 1 in
      let i = get_int evd args 2 in
      Parray.get t i
    | Arraydefault ->
      let t = get_parray evd args 1 in
      Parray.default t
    | Arrayset ->
      let ty = E.get args 0 in
      let t = get_parray evd args 1 in
      let i = get_int evd args 2 in
      let a = E.get args 3 in
      let t' = Parray.set t i a in
      E.mkArray env u t' ty
    | Arraycopy ->
      let ty = E.get args 0 in
      let t = get_parray evd args 1 in
      let t' = Parray.copy t in
      E.mkArray env u t' ty
    | Arraylength ->
      let t = get_parray evd args 1 in
      E.mkInt env (Parray.length t)

  let red_prim env evd p u args =
    try
      let r =
        red_prim_aux env evd p u args
      in Some r
    with NativeDestKO -> None

end