forked from roconnor-blockstream/fiat-crypto
-
Notifications
You must be signed in to change notification settings - Fork 2
/
MapCastByDeBruijn.v
24 lines (22 loc) · 881 Bytes
/
MapCastByDeBruijn.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.Syntax.Util.
Require Import Crypto.Compilers.Z.Bounds.Interpretation.
Section language.
Context (round_up : nat -> option nat)
{t : type base_type}.
Definition MapCastCompile := @MapCastCompile t.
Definition MapCastDoCast
:= @MapCastDoCast
(@Bounds.interp_base_type) (@Bounds.interp_op)
(@Bounds.bounds_to_base_type round_up)
(fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _)
t.
Definition MapCastDoInterp
:= @MapCastDoInterp
(@Bounds.interp_base_type) (@Bounds.bounds_to_base_type round_up)
t.
Definition MapCast e input_bounds
:= MapCastDoInterp input_bounds (MapCastDoCast input_bounds (MapCastCompile e)).
End language.