|
(* Reduction of native operators *)
open Names
open CPrimitives
open Retroknowledge
open Environ
open CErrors
let add_retroknowledge env action =
match action with
| Register_type(PT_int63,c) ->
let retro = env.retroknowledge in
let retro =
match retro.retro_int63 with
| None -> { retro with retro_int63 = Some c }
| Some c' -> assert (Constant.equal c c'); retro in
set_retroknowledge env retro
| Register_ind(pit,ind) ->
let retro = env.retroknowledge in
let retro =
match pit with
| PIT_bool ->
let r =
match retro.retro_bool with
| None -> ((ind,1), (ind,2))
| Some (((ind',_),_) as t) -> assert (eq_ind 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) -> assert (eq_ind 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) -> assert (eq_ind 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) -> assert (eq_ind ind ind'); t in
{ retro with retro_cmp = Some r }
in
set_retroknowledge env retro
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_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")
exception NativeDestKO
module type RedNativeEntries =
sig
type elem
type args
type evd (* will be unit in kernel, evar_map outside *)
val get : args -> int -> elem
val get_int : evd -> elem -> Uint63.t
val mkInt : env -> Uint63.t -> elem
val mkBool : env -> bool -> elem
val mkCarry : env -> bool -> elem -> elem (* true if carry *)
val mkIntPair : env -> elem -> elem -> elem
val mkLt : env -> elem
val mkEq : env -> elem
val mkGt : env -> elem
end
module type RedNative =
sig
type elem
type args
type evd
val red_prim : env -> evd -> CPrimitives.t -> args -> elem option
end
module RedNative (E:RedNativeEntries) :
RedNative with type elem = E.elem
with type args = E.args
with type evd = E.evd =
struct
type elem = E.elem
type args = E.args
type evd = E.evd
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 red_prim_aux env evd op 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
let red_prim env evd p args =
try
let r =
red_prim_aux env evd p args
in Some r
with NativeDestKO -> None
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
