blob: f3e501008370d2be767dd30be7492943c05c2fb6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
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 (genericize_op : forall t tR (opc : op t tR)
(args_bs : interp_flat_type Bounds.interp_base_type t),
op (SmartMap.SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) args_bs)
(SmartMap.SmartFlatTypeMap (fun _ => Bounds.bounds_to_base_type) (Bounds.interp_op opc args_bs))).
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.
|
