Newer
Older
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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
(** Time-stamp: <modified the 01/06/2016 (at 17:34) by Erwan Jahier> *)
open Lxm
open Lic
open AstPredef
let dbg = (Lv6Verbose.get_flag "woi")
(********************************************************************************)
(** The functions below accumulate
(1) the assertions
(2) the new equations
(3) the fresh variables
*)
type acc =
Lic.var_info list (* new local vars *)
* Lic.eq_info srcflagged list (* equations *)
* Lic.val_exp srcflagged list (* assertions *)
let new_var = FreshName.var_info
let new_var str type_eff clock_eff =
let id = Lv6Id.of_string (FreshName.local_var str) in
let var =
{
var_name_eff = id;
var_nature_eff = AstCore.VarLocal;
var_number_eff = -1;
var_type_eff = type_eff;
var_clock_eff = id,clock_eff;
} in
var
(********************************************************************************)
(* The one that perform the real work, namely:
- invent a fresh var name NV
- replace 'when Idle(st)' by 'when NV'
- generate the equation defining NV (NV=(Idle=st);)
*)
let (gen_ident : Lxm.t -> Lv6Id.long -> Lv6Id.t -> type_ -> Lic.clock -> acc ->
Lic.by_pos_op srcflagged * acc ) =
fun lxm cc cv ct clk (vl,eql,al) -> (* On(Idle, st, enum_t) *)
let nv_base = (snd cc) ^ "_" ^ cv in
let nv = new_var nv_base Bool_type_eff clk in
let ve1 = {
ve_typ = [ct];
ve_clk = [clk];
ve_core = CallByPosLic(Lxm.flagit (Lic.CONST_REF cc) lxm,[])
}
in
let ve2 = {
ve_typ = [ct];
ve_clk = [clk];
ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[])
}
in
let ve = (* Idle=st *){
ve_typ = [Bool_type_eff];
ve_clk = [clk];
ve_core =
CallByPosLic({it=Lic.PREDEF_CALL({it=(("Lustre","eq"),[]);src=lxm});src=lxm},
[ve1;ve2])
}
in
let new_eq = (* NV=(Idle=st) *) {src=lxm;it=[LeftVarLic (nv, lxm)], ve} in
let true_cc = "Lustre","true" in
let op = WHEN (On((true_cc, nv.var_name_eff, Bool_type_eff),clk)) in
Lxm.flagit op lxm, (nv::vl,new_eq::eql,al)
(********************************************************************************)
(* All the remaining are admnistrative functions *)
let rec (do_eq : LicPrg.t -> Lic.eq_info srcflagged -> acc -> acc) =
fun licprg { src = lxm_eq ; it = (left_list, ve) } acc ->
let ve, (nv,neqs,nass) = do_val_exp licprg ve acc in
nv, { src = lxm_eq ; it = (left_list, ve) }::neqs, nass
and (do_val_exp: LicPrg.t -> val_exp -> acc -> val_exp * acc) =
fun licprg ve acc ->
let ve_core, acc =
match ve.ve_core with
| Merge(ce,cl) -> (
let cl,acc =
List.fold_left
(fun (ncl,acc) (c, ve) ->
let ve, acc = do_val_exp licprg ve acc in
((c, ve)::ncl), acc
)
([],acc)
cl
in
Merge(ce,cl),acc
)
| CallByNameLic(op, fl) -> (
let fl,acc = List.fold_left
(fun (nfl,acc) (id,ve) ->
let nf, acc = do_val_exp licprg ve acc in
((id,nf)::nfl), acc
)
([],acc)
fl
in
CallByNameLic(op, fl), acc
)
| CallByPosLic (op, vel) -> (
let vel, acc = List.fold_left
(fun (vel,acc) ve ->
let ve, acc = do_val_exp licprg ve acc in
(ve::vel), acc
)
([],acc)
(List.rev vel)
in
match op.it with
| WHEN (On((_,_,Bool_type_eff),_)) -> (* nothing to do in this case *)
CallByPosLic(op, vel), acc
| WHEN (On((cc,cv,ct),clk)) ->
let op, acc = gen_ident op.src cc cv ct clk acc in
CallByPosLic(op, vel), acc
| _ -> CallByPosLic(op, vel), acc
)
in
{ ve with ve_core = ve_core },acc
and (do_val_exp_flag: LicPrg.t -> val_exp srcflagged -> acc ->
val_exp srcflagged * acc) =
fun licprg ve_f acc ->
let ve, acc = do_val_exp licprg ve_f.it acc in
{ ve_f with it = ve }, acc
and (do_node : LicPrg.t -> Lic.node_exp -> Lic.node_exp) =
fun licprg n ->
match n.def_eff with
| ExternLic | MetaOpLic | AbstractLic _ -> n
| BodyLic b ->
let acc = List.fold_left
(fun acc eq -> do_eq licprg eq acc)
([],[],[])
(List.rev b.eqs_eff)
in
let acc = List.fold_left
(fun acc ve ->
let ve,(nv,neq,nass) = do_val_exp_flag licprg ve acc in
(nv,neq,ve::nass)
)
acc
b.asserts_eff
in
let (nv,neqs,nass) = acc in
let nlocs = match n.loclist_eff with
| None -> nv (* SNO, but eats no bread *)
| Some v -> List.rev_append nv v
in
{ n with
def_eff = BodyLic {
eqs_eff = neqs;
asserts_eff = nass;
};
loclist_eff = Some nlocs;
}
(* exported *)
let rec (doit : LicPrg.t -> LicPrg.t) =
fun inprg ->
let outprg = LicPrg.empty in
(** types and constants do not change *)
let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in
let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
(** transform nodes *)
let rec (doit_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) =
fun nk ne outprg ->
Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf "#DBG: L2lWhenOnId '%s'\n"
(Lic.string_of_node_key nk));
let ne = do_node inprg ne in
LicPrg.add_node nk ne outprg
in
let outprg = LicPrg.fold_nodes doit_node inprg outprg in
outprg