blob: 791e338867c3c3d5248de4d80980009a78385beb (
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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Relations.
Require Import Crypto.Compilers.MapCastByDeBruijnWf.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
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)))
(cast_backb: forall t b, interp_base_type (pick_typeb t b) -> interp_base_type t).
Let cast_back : forall t b, interp_flat_type interp_base_type (pick_type b) -> interp_flat_type interp_base_type t
:= fun t b => SmartFlatTypeMapUnInterp cast_backb.
Context (inboundsb : forall t, interp_base_type_bounds t -> interp_base_type t -> Prop).
Let inbounds : forall t, interp_flat_type interp_base_type_bounds t -> interp_flat_type interp_base_type t -> Prop
:= fun t => interp_flat_type_rel_pointwise inboundsb (t:=t).
Context (interp_op_bounds_correct
: forall t tR opc bs
(v : interp_flat_type interp_base_type t)
(H : inbounds t bs v),
inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v))
(pull_cast_back
: forall t tR opc bs
(v : interp_flat_type interp_base_type (pick_type bs))
(H : inbounds t bs (cast_back t bs v)),
interp_op t tR opc (cast_back t bs v)
=
cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v)).
Local Notation MapCast
:= (@MapCast interp_base_type_bounds interp_op_bounds pick_typeb cast_op).
Definition Wf_MapCast
{t} (e : Expr t)
(input_bounds : interp_flat_type interp_base_type_bounds (domain t))
{b} e' (He' : MapCast e input_bounds = Some (existT _ b e'))
(Hwf : Wf e)
: Wf e'
:= @Wf_MapCast
_ _ _ internal_base_type_dec_bl internal_base_type_dec_lb _ _ _ _ _
t e input_bounds b e' He' Hwf.
Definition Wf_MapCast_arrow
{s d} (e : Expr (Arrow s d))
(input_bounds : interp_flat_type interp_base_type_bounds s)
{b} e' (He' : MapCast e input_bounds = Some (existT _ b e'))
(Hwf : Wf e)
: Wf e'
:= @Wf_MapCast_arrow
_ _ _ internal_base_type_dec_bl internal_base_type_dec_lb _ _ _ _ _
s d e input_bounds b e' He' Hwf.
End language.
|
