blob: 1985653d4619fc4a1e5b4207c87f1ab15289b4a7 (
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
28
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.MapCastByDeBruijn.
Require Import Crypto.Compilers.Z.Syntax.
Section language.
Context {interp_base_type_bounds : base_type -> Type}
(interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
(pick_typeb : forall t, interp_base_type_bounds t -> base_type).
Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
Context (cast_op : forall t tR (opc : op t tR) args_bs,
op (pick_type args_bs) (pick_type (interp_op_bounds t tR opc args_bs))).
Context {t : type base_type}.
Definition MapCastCompile := @MapCastCompile base_type op t.
Definition MapCastDoCast
:= @MapCastDoCast
base_type op base_type_beq internal_base_type_dec_bl
interp_base_type_bounds interp_op_bounds pick_typeb cast_op t.
Definition MapCastDoInterp
:= @MapCastDoInterp
base_type op base_type_beq internal_base_type_dec_bl
(fun _ t => Op (OpConst 0%Z) TT)
interp_base_type_bounds pick_typeb t.
Definition MapCast e input_bounds
:= MapCastDoInterp input_bounds (MapCastDoCast input_bounds (MapCastCompile e)).
End language.
|
