-
Notifications
You must be signed in to change notification settings - Fork 0
/
RegStruct.v
119 lines (99 loc) · 4.7 KB
/
RegStruct.v
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
115
116
117
118
Require Import Kami.AllNotations.
Require Import Kami.Utila.
Local Open Scope kami_expr.
Local Open Scope kami_action.
Definition Struct_RegReads' ty n (sk: Fin.t n -> string * Kind) : ActionT ty (Struct sk) :=
fold_left (fun acc i =>
LETA tmp <- acc;
Read val: snd (sk i) <- fst (sk i);
Ret (UpdateStruct #tmp i #val))%kami_action
(getFins n) (Ret (Const ty (getDefaultConst (Struct sk)))).
Definition Struct_RegWrites' ty n (sk: Fin.t n -> string * Kind) (e: Struct sk @# ty): ActionT ty Void :=
fold_left (fun acc i =>
LETA _ <- acc;
Write (fst (sk i)) : snd (sk i) <- ReadStruct e i ;
Retv)
(getFins n) Retv.
Definition Struct_RegReads ty k: ActionT ty k :=
match k return ActionT ty k with
| Struct _ ski => Struct_RegReads' ty ski
| Bool => Ret (Const ty Default)
| Bit n => Ret (Const ty Default)
| Array n k => Ret (Const ty Default)
end.
Definition Struct_RegWrites ty k (e: k @# ty): ActionT ty Void:=
match k return k @# ty -> ActionT ty Void with
| Struct _ ski => fun e => Struct_RegWrites' e
| Bool => fun _ => Retv
| Bit n => fun _ => Retv
| Array n k => fun _ => Retv
end e.
Definition MayStruct_RegReads' ty n (s: Fin.t n -> string) (vals: Fin.t n -> {k: Kind & option (ConstT k)}):
ActionT ty (Struct (fun i => (s i, projT1 (vals i)))) :=
fold_left (fun (acc: ActionT ty (Struct (fun i => (s i, projT1 (vals i))))) i =>
LETA tmp <- acc;
match projT2 (vals i) with
| Some uval =>
LET val: projT1 (vals i) <- Const ty uval;
Ret (UpdateStruct #tmp i #val)
| None =>
Read val : projT1 (vals i) <- s i;
Ret (UpdateStruct #tmp i #val)
end)%kami_action
(getFins n) (Ret (Const ty Default)).
Definition MayStruct_RegWrites' ty n (s: Fin.t n -> string) (vals: Fin.t n -> {k: Kind & option (ConstT k)})
(e: Struct (fun i => (s i, projT1 (vals i))) @# ty):
ActionT ty Void :=
fold_left (fun acc i =>
LETA _ <- acc;
match projT2 (vals i) with
| Some uval =>
Retv
| None =>
Write (s i) : projT1 (vals i) <- ReadStruct e i ;
Retv
end)%kami_action
(getFins n) Retv.
Local Close Scope kami_action.
Local Close Scope kami_expr.
Declare Scope kami_maystruct_scope.
Notation "name :: ty" := (name%string, existT (fun k => option (ConstT k)) ty None) (only parsing) : kami_maystruct_scope.
Notation "name ::# ty #:: val " := (name%string, existT (fun k => option (ConstT k)) ty (Some val))
(only parsing, at level 99): kami_maystruct_scope.
Delimit Scope kami_maystruct_scope with kami_maystruct.
Record MayStruct n := { vals : Fin.t n -> {k: Kind & option (ConstT k)} ;
names : Fin.t n -> string }.
Definition getMayStruct ls: MayStruct (length ls) :=
{| vals := fun i => snd (nth_Fin ls i) ;
names := fun i => fst (nth_Fin ls i)
|}.
Notation "'MAYSTRUCT' { s1 ; .. ; sN }" :=
(getMayStruct (cons s1%kami_maystruct .. (cons sN%kami_maystruct nil) ..)).
Definition MayStruct_RegReads ty n (v: MayStruct n) := MayStruct_RegReads' ty (names v) (vals v).
Definition MayStruct_RegWrites (ty: Kind -> Type) n (v: MayStruct n) e := @MayStruct_RegWrites' ty n (names v) (vals v) e.
(* Definition MayStruct_RegReads' ty n (k: Fin.t n -> Kind) (s: Fin.t n -> string) (vals: forall i, option (ConstT (k i))): *)
(* ActionT ty (Struct k s) := *)
(* fold_left (fun acc i => *)
(* LETA tmp <- acc; *)
(* match vals i with *)
(* | Some uval => *)
(* LET val : (k i) <- $$ uval; *)
(* Ret (UpdateStruct #tmp i #val) *)
(* | None => *)
(* Read val : (k i) <- s i; *)
(* Ret (UpdateStruct #tmp i #val) *)
(* end)%kami_action *)
(* (getFins n) (Ret (Const ty (getDefaultConst (Struct _ _)))). *)
(* Definition MayStruct_RegWrites' ty n (k: Fin.t n -> Kind) (s: Fin.t n -> string) (vals: forall i, option (ConstT (k i))) *)
(* (e: Struct k s @# ty): *)
(* ActionT ty Void := *)
(* fold_left (fun acc i => *)
(* LETA _ <- acc; *)
(* match vals i with *)
(* | Some uval => *)
(* Retv *)
(* | None => *)
(* Write (s i) : (k i) <- ReadStruct e i ; *)
(* Retv *)
(* end)%kami_action *)
(* (getFins n) Retv. *)