blob: 77790eec875a4ef22800a293d77d137d4d9409d6 (
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.InSet.Syntax.
Require Import Crypto.Compilers.InSet.Typeify.
Local Ltac t :=
repeat first [ reflexivity
| progress simpl in *
| apply (f_equal2 (@pair _ _))
| solve [ auto ]
| progress cbv [LetIn.Let_In]
| progress autorewrite with core
| progress intros
| match goal with
| [ v : _ * _ |- _ ] => destruct v
| [ H : _ |- _ ] => rewrite H
end ].
Section language.
Context {base_type_code : Set}
{op : flat_type base_type_code -> flat_type base_type_code -> Set}
{interp_base_type : base_type_code -> Set}.
Lemma typeify_untypeify_interp_flat_type {t} v
: @typeify_interp_flat_type base_type_code interp_base_type t (untypeify_interp_flat_type v) = v.
Proof using Type. induction t; t. Qed.
Lemma untypeify_typeify_interp_flat_type {t} v
: @untypeify_interp_flat_type base_type_code interp_base_type t (typeify_interp_flat_type v) = v.
Proof using Type. induction t; t. Qed.
Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type.
Section gen.
Context {interp_op : forall s d, op s d -> Compilers.Syntax.interp_flat_type interp_base_type s -> Compilers.Syntax.interp_flat_type interp_base_type d}
{interp_op' : forall s d, op s d -> InSet.Syntax.interp_flat_type interp_base_type s -> InSet.Syntax.interp_flat_type interp_base_type d}
(untypeify_interp_op
: forall s d opc args,
untypeify_interp_flat_type (interp_op s d opc args)
= interp_op' s d opc (untypeify_interp_flat_type args))
(typeify_interp_op
: forall s d opc args,
typeify_interp_flat_type (interp_op' s d opc args)
= interp_op s d opc (typeify_interp_flat_type args)).
Local Notation interpf := (Compilers.Syntax.interpf interp_op).
Local Notation interpf' := (InSet.Syntax.interpf interp_op').
Local Notation typeify := (typeify (var:=interp_base_type)).
Lemma interpf_typeify {t} e
: interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e).
Proof using typeify_interp_op. induction e; t. Qed.
Lemma interpf_untypeify {t} e
: interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e).
Proof using untypeify_interp_op. induction e; t. Qed.
Lemma interpf_typeify_untypeify {t} e
: interpf (typeify (untypeify (t:=t) e)) = interpf e.
Proof using Type. induction e; t. Qed.
Lemma interpf_untypeify_typeify {t} e
: interpf' (untypeify (t:=t) (typeify e)) = interpf' e.
Proof using Type. induction e; t. Qed.
End gen.
End language.
Module Compilers.
Import Compilers.Syntax.
Section language.
Context {base_type_code : Set}
{op : flat_type base_type_code -> flat_type base_type_code -> Set}
{interp_base_type : base_type_code -> Set}
{interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}.
Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type.
Local Notation interp_op' :=
(fun s d opc args => untypeify_interp_flat_type (interp_op s d opc (typeify_interp_flat_type args))).
Local Notation interpf := (Compilers.Syntax.interpf interp_op).
Local Notation interpf' := (InSet.Syntax.interpf interp_op').
Local Notation typeify := (typeify (var:=interp_base_type)).
Lemma interpf_typeify {t} e
: interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e).
Proof using Type. apply interpf_typeify; t. Qed.
Lemma interpf_untypeify {t} e
: interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e).
Proof using Type. apply interpf_untypeify; t. Qed.
End language.
End Compilers.
Module InSet.
Import InSet.Syntax.
Section language.
Context {base_type_code : Set}
{op : flat_type base_type_code -> flat_type base_type_code -> Set}
{interp_base_type : base_type_code -> Set}
{interp_op' : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}.
Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type.
Local Notation interp_op :=
(fun s d opc args => typeify_interp_flat_type (interp_op' s d opc (untypeify_interp_flat_type args))).
Local Notation interpf := (Compilers.Syntax.interpf interp_op).
Local Notation interpf' := (InSet.Syntax.interpf interp_op').
Local Notation typeify := (typeify (var:=interp_base_type)).
Lemma interpf_typeify {t} e
: interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e).
Proof using Type. apply interpf_typeify; t. Qed.
Lemma interpf_untypeify {t} e
: interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e).
Proof using Type. apply interpf_untypeify; t. Qed.
End language.
End InSet.
|
