summaryrefslogtreecommitdiffstats
path: root/interpret/interpret.ml
blob: dd0ffb0dbaf6299f1f1ecdb4e149c061f72f9d2a (plain) (blame)
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
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507

open Ast
open Util
open Ast_util
open Typing

module I : sig

  exception Bad_datatype
  type value

  val int_value : int -> value
  val bool_value : bool -> value
  val real_value : float -> value

  val as_int : value -> int
  val as_bool : value -> bool
  val as_real : value -> float

  val str_repr_of_val : value -> string

  type state

  val print_state : Format.formatter -> state -> unit

  type io = (id * value) list

  (*
    Get the constants only
  *)
  val consts : rooted_prog -> value VarMap.t

  (*
    Construct initial state for a program.
    The id is the root node of the program evaluation.
  *)
  val init_state : rooted_prog -> state

  (*
    Run a step of the program (not necessary to specify the program,
      it should be encoded in the state).
    State -> Inputs -> Next state, Outputs
  *)
  val step : state -> io -> (state * io)

end = struct

  (* Values for variables *)

  exception Bad_datatype

  type value =
    | VInt of int
    | VBool of bool
    | VReal of float
    | VState of id
    | VPrevious of value list
    | VBusy   (* intermediate value : calculating ! *)
    | VCalc of (unit -> unit)

  let int_value i = VInt i
  let bool_value b = VBool b
  let real_value r = VReal r

  let as_int = function
    | VInt i -> i
    | _ -> raise Bad_datatype
  let as_bool = function
    | VBool b -> b
    | _ -> raise Bad_datatype
  let as_real = function
    | VReal r -> r
    | _ -> raise Bad_datatype

  let rec str_repr_of_val = function
    | VInt i -> string_of_int i
    | VReal r -> string_of_float r
    | VBool b -> if b then "true" else "false"
    | VState s -> "state " ^ s
    | VPrevious p ->
      "[" ^
        List.fold_left (fun s v ->
            (if s = "" then "" else s ^ ", ") ^ str_repr_of_val v)
          "" p
      ^ "]"
    | VBusy -> "#"
    | VCalc _ -> "()"

  (* States of the interpret *)


  type state = {
    rp         : rooted_prog;
    p          : prog;
    root_scope : scope;
    outputs    : id list;
    save       : value VarMap.t;
  }

  let print_state fmt st =
    VarMap.iter
      (fun id v -> Format.fprintf fmt "%s = %s@." id (str_repr_of_val v))
      st.save

  type io = (id * value) list


  (* Internal type env : contains the environment for state calculation *)
  type env = {
    st      : state;
    vars    : (id, value) Hashtbl.t;
  }


  (*
    get_var : env -> id -> id -> value

    Gets the value of a variable relative to a node path.
  *)
  let rec get_var env node id =
    let p = node^"/"^id in
    try match Hashtbl.find env.vars p with
      | VCalc f ->
        Hashtbl.replace env.vars p VBusy;
        f ();
        get_var env node id
      | VBusy -> combinatorial_cycle p
      | x -> x
    with
      | Not_found -> no_variable p

  (*
    eval_expr : env -> (id * id) -> expr ext -> value list
  *)
  let rec eval_expr env (node, prefix) exp =
    let sub_eval = eval_expr env (node, prefix) in
    match fst exp with
    | AST_identifier (id, _) ->
      [loc_error (snd exp) (get_var env node) id]
    | AST_idconst (id, _) ->
      begin try [VarMap.find ("cst/"^id) env.st.save]
      with Not_found -> loc_error (snd exp) no_variable id end
    (* on numerical values *)
    | AST_int_const (i, _) -> [VInt (int_of_string i)]
    | AST_real_const (r, _) -> [VReal (float_of_string r)]
    | AST_unary(AST_UPLUS, e) -> sub_eval e
    | AST_unary(AST_UMINUS, e) ->
      begin match sub_eval e with
      | [VInt x] -> [VInt (-x)]
      | [VReal x] -> [VReal(-. x)]
      | _ -> type_error "Unary on non-numerical."
      end
    | AST_binary(op, e1, e2) ->
      let iop, fop = match op with
      | AST_PLUS -> (+), (+.)
      | AST_MINUS -> (-), (-.)
      | AST_MUL -> ( * ), ( *. )
      | AST_DIV -> (/), (/.)
      | AST_MOD -> (mod), mod_float
      in
      begin match sub_eval e1, sub_eval e2 with
      | [VInt a], [VInt b] -> [VInt (iop a b)]
      | [VReal a], [VReal b] -> [VReal(fop a b)]
      | _ -> type_error "Invalid arguments for numerical binary."
      end
    | AST_cast(e, ty) ->
      begin match sub_eval e, ty with
      | [VInt i], AST_TINT -> [VInt i]
      | [VReal r], AST_TINT -> [VInt (int_of_float r)]
      | [VInt i], AST_TREAL -> [VReal (float_of_int i)]
      | [VReal r], AST_TREAL -> [VReal r]
      | _ -> type_error "Invalid arguments in cast."
      end
    (* on boolean values *)
    | AST_bool_const b -> [VBool b]
    | AST_binary_rel(op, e1, e2) ->
      let r = match op with
      | AST_EQ -> (=)     | AST_NE -> (<>)
      | AST_LT -> (<)     | AST_LE -> (<=)
      | AST_GT -> (>)     | AST_GE -> (>=)
      in
      begin match sub_eval e1, sub_eval e2 with
      | [VInt a], [VInt b] -> [VBool (r a b)]
      | [VReal a], [VReal b] -> [VBool (r a b)]
      | [VBool a], [VBool b] -> [VBool (r a b)]
      | _ -> type_error "Invalid arguments for binary relation."
      end
    | AST_binary_bool(op, e1, e2) ->
      let r = match op with
      | AST_AND -> (&&)   | AST_OR -> (||)
      in
      begin match sub_eval e1, sub_eval e2 with
      | [VBool a], [VBool b] -> [VBool (r a b)]
      | _ -> type_error "Invalid arguments for boolean relation."
      end
    | AST_not(e) ->
      begin match sub_eval e with
      | [VBool b] -> [VBool (not b)]
      | _ -> type_error "Invalid arguments for boolean negation."
      end
    (* temporal primitives *)
    | AST_pre(exp, n) ->
      begin try match VarMap.find (node^"/"^prefix^n) env.st.save with
        | VPrevious x -> x
        | _ -> assert false
      with Not_found -> []
      end
    | AST_arrow(before, after) -> 
      begin try match VarMap.find (node^"/"^prefix^"init") env.st.save with
      | VBool true -> sub_eval before
      | VBool false -> sub_eval after
      | _ -> assert false
      with Not_found -> assert false
      end
    (* other *)
    | AST_if(cond, a, b) ->
      begin match sub_eval cond with
      | [VBool true] -> sub_eval a
      | [VBool false] -> sub_eval b
      | _ -> type_error "Invalid condition in if."
      end
    | AST_tuple x -> List.flatten (List.map sub_eval x)
    | AST_instance((f, _), args, nid) ->
      let (n, _) = find_node_decl env.st.p f in
      List.map
        (fun (_, id, _) -> get_var env (node^"/"^nid) id)
        n.ret

  (*
    reset_scope : env -> scope -> unit

    Sets all the init variables to true, and all the state variables
    to initial state. Does this recursively.
    The state reset done by this on the environment is only applied on the
    next iteration, when the state info has been extracted by extract_st.
  *)
  let rec reset_scope env (node, prefix, eqs) =
    Hashtbl.replace env.vars (node^"/"^prefix^"init") (VBool true);
    let do_exp e =
      List.iter
        (fun (_, id, eqs, _) -> reset_scope env (node^"/"^id, "", eqs))
        (extract_instances env.st.p e)
    in
    let do_eq (e, _) = match e with
      | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) -> do_exp e
      | AST_automaton (aid, states, _) ->
        let (init_state, _) = List.find (fun (st, _) -> st.initial) states in
        Hashtbl.replace env.vars (node^"/"^aid^".state") (VState init_state.st_name);
        List.iter
          (fun (st, _) -> reset_scope env (node, aid^"."^st.st_name^".", st.body))
          states
      | AST_activate (x, _) ->
        let rec aux = function
          | AST_activate_if (_, a, b) -> aux a; aux b
          | AST_activate_body b ->
            reset_scope env (node, b.act_id^".", b.body)
        in aux x
    in
    List.iter do_eq eqs

  (*
    activate_scope : env -> scope -> unit

    Adds functions for calculating the variables in this scope.
    For assign : simple !
    For automaton : lazily select+activate automaton state (would enable
        implementation of strong transitions)
    For activate : lazily select+activate active block
  *)
  let rec activate_scope env (node, prefix, eqs) =
    Hashtbl.replace env.vars (node^"/"^prefix^"act") (VBool true);
    let do_expr e =
      List.iter
        (fun (_, id, eqs, args) ->
          activate_scope env (node^"/"^id, "", eqs);
          let do_arg ((_,name,_), expr) =
            let apath = node^"/"^id^"/"^name in
            let calc () =
              match eval_expr env (node, prefix) expr with
              | [v] -> Hashtbl.replace env.vars apath v
              | _ -> loc_error (snd expr) error "Unsupported arity for argument."
            in
            Hashtbl.replace env.vars apath (VCalc calc)
          in
          List.iter do_arg args)
        (extract_instances env.st.p e)
    in
    let do_eq (e, _) = match e with
      | AST_assign(vars, e) ->
        do_expr e;
        let calc () =
          let vals = eval_expr env (node, prefix) e in
          List.iter2 (fun (id, _) v ->
            Hashtbl.replace env.vars (node^"/"^id) v) vars vals
        in
        List.iter
          (fun (id, _) ->
              Hashtbl.replace env.vars (node^"/"^id) (VCalc (calc)))
          vars
      | AST_assume(_,e) | AST_guarantee(_,e) -> do_expr e
      | AST_activate(t, vars) ->
        let rec do_tree = function
          | AST_activate_body _ -> ()
          | AST_activate_if(c, a, b) ->
            do_expr c; do_tree a; do_tree b
        in do_tree t;
        let rec needed x () = match x with
          | AST_activate_body b ->
            activate_scope env (node, b.act_id^".", b.body)
          | AST_activate_if (c, t, f) ->
            begin match eval_expr env (node, prefix) c with
            | [VBool true] -> needed t ()
            | [VBool false] -> needed f ()
            | _ -> error "Invalid value in activate if condition."
            end
        in
        List.iter (fun id ->
            Hashtbl.replace env.vars (node^"/"^id) (VCalc (needed t)))
          vars
      | AST_automaton(aid, states, vars) ->
        let asn = match VarMap.find (node^"/"^aid^".state") env.st.save with
          | VState s -> s
          | _ -> assert false
        in
        let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
        activate_scope env (node, aid^"."^st.st_name^".", st.body);
        List.iter (fun (c, _, _) -> do_expr c) st.until
    in
    List.iter do_eq eqs

  (*
    is_scope_active : env -> scope -> bool
  *)
  let is_scope_active env (node, prefix, _) =
    try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"act"))
    with Not_found -> false | Bad_datatype -> assert false

  (*
    do_weak_transitions : env -> scope -> unit
  *)
  let rec do_weak_transitions env (node, prefix, eqs) =
    let do_expr e =
      List.iter
        (fun (_, id, eqs, args) ->
          do_weak_transitions env (node^"/"^id, "", eqs))
        (extract_instances env.st.p e)
    in
    let do_eq (e, _) = match e with
      | AST_assign(_, e) -> do_expr e
      | AST_assume (_, e) | AST_guarantee (_, e) -> do_expr e
      | AST_activate(t, _) ->
        let rec do_tree = function
          | AST_activate_body b -> do_weak_transitions env (node, b.act_id^".", b.body)
          | AST_activate_if(c, a, b) ->
            do_expr c; do_tree a; do_tree b
        in do_tree t
      | AST_automaton(aid, states, vars) ->
        let svn = node^"/"^aid^".state" in
        let stv = VarMap.find svn env.st.save in
        let new_st =
          if is_scope_active env (node, prefix, eqs) then begin
            let asn = match stv with
              | VState s -> s
              | _ -> assert false
            in
            let (st, _) = List.find (fun (st, _) -> st.st_name = asn) states in
            try
              let (_, (next_st,_), rst) = List.find
                (fun (c, _, _) -> eval_expr env (node, aid^"."^st.st_name^".") c = [VBool true])
                st.until
              in
                if rst then begin
                  let (st, _) = List.find (fun (st, _) -> st.st_name = next_st) states in
                  reset_scope env (node, aid^"."^next_st^".", st.body)
                end;
                VState(next_st)
            with
              | _ -> stv
          end else
            stv
        in
            Hashtbl.replace env.vars svn new_st
    in
    List.iter do_eq eqs

  (*
    extract_st : env -> state
  *)
  let extract_st env =
    let rec aux (node, prefix, eqs) save =

      let init =
        try as_bool (Hashtbl.find env.vars (node^"/"^prefix^"init"))
        with
        | Not_found ->
          let pre_init = as_bool (VarMap.find (node^"/"^prefix^"init") env.st.save)
          in pre_init && (not (is_scope_active env (node, prefix, eqs)))
        | Bad_datatype ->
            Format.eprintf "%s@."
              (str_repr_of_val (Hashtbl.find env.vars (node^"/"^prefix^"init")));
            assert false
      in
      let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in

      let save_expr save e =
        (* Save pre expressions *)
        let save = List.fold_left
          (fun save (id, expr) ->
            let n = node^"/"^prefix^id in
            if is_scope_active env (node, prefix, eqs) then
              VarMap.add
                n
                (VPrevious (eval_expr env (node, prefix) expr))
                save
            else
              try VarMap.add n
                (VarMap.find n env.st.save)
                save
              with Not_found -> save
          )
          save (extract_pre e) in
        (* Save recursively in sub instances of nodes *)
        let save = List.fold_left
          (fun save (_, n, eqs, _) ->
            aux (node^"/"^n, "", eqs) save)
          save (extract_instances env.st.p e)
        in save
      in
      let save_eq save eq = match fst eq with
        | AST_assign(_, e) | AST_assume(_, e) | AST_guarantee(_, e) ->
            save_expr save e
        | AST_automaton(aid, states, _) ->
          let svn = node^"/"^aid^".state" in
          let st = Hashtbl.find env.vars svn in
          let save = VarMap.add (node^"/"^aid^".state") st save in
          List.fold_left (fun save (st, _) ->
              let save = 
                List.fold_left (fun save (c, _, _) -> save_expr save c) save st.until in
              aux (node, aid^"."^st.st_name^".", st.body) save)
            save states
        | AST_activate(r, _) ->
          let rec do_t save = function
            | AST_activate_if(c, t, f) ->
              let save = save_expr save c in
              let save = do_t save t in
              do_t save f
            | AST_activate_body b ->
              aux (node, b.act_id^".", b.body) save
          in
          do_t save r
      in
      List.fold_left save_eq save eqs

    in
    let consts = VarMap.filter (fun k _ -> k.[0] <> '/') env.st.save in
    { env.st with save = aux env.st.root_scope consts }
      
  (*
    init_state : prog -> id -> state
  *)
  let init_state rp =
    let st = {
        rp = rp;
        p = rp.p;
        root_scope = rp.root_scope;
        save = VarMap.empty;
        outputs = (List.map (fun (_,n,_) -> n) rp.root_node.ret);
    } in

    let env = { st = st; vars = Hashtbl.create 42 } in

    (* calculate constants *)
    List.iter (function
        | AST_const_decl(d, l) ->
          let cpath = "cst/" ^ d.c_name in
          Hashtbl.replace env.vars cpath (VCalc (fun () ->
            match eval_expr env ("cst", "") d.value with
            | [v] -> Hashtbl.replace env.vars cpath v
            | _ -> loc_error l error "Arity error in constant expression."))
        | _ -> ())
      rp.p;
    List.iter (function
        | AST_const_decl(d, l) -> ignore (get_var env "cst" d.c_name)
        | _ -> ())
      rp.p;

    reset_scope env st.root_scope;
    { st with save = Hashtbl.fold VarMap.add env.vars VarMap.empty }

  (*
    step : state -> io -> (state * io)
  *)
  let step st i =
    let vars = Hashtbl.create 10 in
    List.iter (fun (k, v) -> Hashtbl.replace vars ("/"^k) v) i;
    let env = { st = st; vars = vars } in
    
    activate_scope env st.root_scope; 
    if false then
      Hashtbl.iter (fun k v -> Format.printf "%s : %s@." k (str_repr_of_val v)) env.vars;
    let out = List.map (fun id -> id, get_var env "" id) st.outputs in
    do_weak_transitions env st.root_scope;
    extract_st env, out

  let consts rp =
    (init_state rp).save

end