diff options
Diffstat (limited to 'pretyping/cbv.ml')
| -rw-r--r-- | pretyping/cbv.ml | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 43b94aed3d..520bcd6b41 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -220,14 +220,29 @@ module VNativeEntries = | _ -> raise Primred.NativeDestKO) | _ -> raise Primred.NativeDestKO + let get_float () e = + match e with + | VAL(_, cf) -> + (match kind cf with + | Float f -> f + | _ -> raise Primred.NativeDestKO) + | _ -> raise Primred.NativeDestKO + + let mkInt env i = VAL(0, mkInt i) + let mkFloat env f = VAL(0, mkFloat f) + let mkBool env b = let (ct,cf) = get_bool_constructors env in CONSTR(Univ.in_punivs (if b then ct else cf), [||]) let int_ty env = VAL(0, mkConst @@ get_int_type env) + let float_ty env = VAL(0, mkConst @@ get_float_type env) + + let cmp_ty env = VAL(0, mkConst @@ get_cmp_type env) + let mkCarry env b e = let (c0,c1) = get_carry_constructors env in CONSTR(Univ.in_punivs (if b then c1 else c0), [|int_ty env;e|]) @@ -237,6 +252,12 @@ module VNativeEntries = let c = get_pair_constructor env in CONSTR(Univ.in_punivs c, [|int_ty;int_ty;e1;e2|]) + let mkFloatIntPair env f i = + let float_ty = float_ty env in + let int_ty = int_ty env in + let c = get_pair_constructor env in + CONSTR(Univ.in_punivs c, [|float_ty;int_ty;f;i|]) + let mkLt env = let (_eq,lt,_gt) = get_cmp_constructors env in CONSTR(Univ.in_punivs lt, [||]) @@ -249,6 +270,15 @@ module VNativeEntries = let (_eq,_lt,gt) = get_cmp_constructors env in CONSTR(Univ.in_punivs gt, [||]) + let mkSomeCmp env v = + let cmp_ty = cmp_ty env in + let (some,_none) = get_option_constructors env in + CONSTR(Univ.in_punivs some, [|cmp_ty;v|]) + + let mkNoneCmp env = + let cmp_ty = cmp_ty env in + let (_some,none) = get_option_constructors env in + CONSTR(Univ.in_punivs none, [|cmp_ty|]) end module VredNative = RedNative(VNativeEntries) @@ -381,7 +411,7 @@ let rec norm_head info env t stack = | Construct c -> (CONSTR(c, [||]), stack) (* neutral cases *) - | (Sort _ | Meta _ | Ind _ | Int _) -> (VAL(0, t), stack) + | (Sort _ | Meta _ | Ind _ | Int _ | Float _) -> (VAL(0, t), stack) | Prod _ -> (CBN(t,env), stack) and norm_head_ref k info env stack normt t = |