blob: d99133e5160c6d9e2fe88480c817ad71e08ad9c9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Z.MapCastByDeBruijn.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Reflection.Z.Syntax.Util.
Require Import Crypto.Reflection.Z.Bounds.Interpretation.
Section language.
Context {t : type base_type}.
Definition MapCastCompile := @MapCastCompile t.
Definition MapCastDoCast
:= @MapCastDoCast
(@Bounds.interp_base_type) (@Bounds.interp_op)
(fun _ => @Bounds.bounds_to_base_type)
(fun _ _ opc _ => @genericize_op _ _ _ opc _ _ _)
t.
Definition MapCastDoInterp
:= @MapCastDoInterp
(@Bounds.interp_base_type) (fun _ => @Bounds.bounds_to_base_type)
t.
Definition MapCast e input_bounds
:= MapCastDoInterp input_bounds (MapCastDoCast input_bounds (MapCastCompile e)).
End language.
|
