Project

General

Profile

Download (2.09 KB) Statistics
| Branch: | Tag: | Revision:
1 7a1b2819 Lélio Brun
open Lustre_types
2
3 ca7ff3f7 Lélio Brun
type register_t = ResetFlag | StateVar of var_decl
4 6d1693b9 Lélio Brun
5
type left_v
6 ca7ff3f7 Lélio Brun
7 6d1693b9 Lélio Brun
type right_v
8
9
type ('a, _) expression_t =
10 ca7ff3f7 Lélio Brun
  | Val : 'a -> ('a, right_v) expression_t
11
  | Tag : ident -> ('a, right_v) expression_t
12
  | Var : var_decl -> ('a, left_v) expression_t
13
  | Memory : register_t -> ('a, left_v) expression_t
14 6d1693b9 Lélio Brun
15
(** TODO: why moving this elsewhere makes the exhaustiveness check fail? *)
16 ca7ff3f7 Lélio Brun
let type_of_l_value : type a. (a, left_v) expression_t -> Types.type_expr =
17 6d1693b9 Lélio Brun
  function
18 ca7ff3f7 Lélio Brun
  | Var v ->
19
    v.var_type
20
  | Memory ResetFlag ->
21
    Type_predef.type_bool
22
  | Memory (StateVar v) ->
23
    v.var_type
24 6d1693b9 Lélio Brun
25
type ('a, 'b) expressions_t = ('a, 'b) expression_t list
26
27
type 'a predicate_t =
28 ca7ff3f7 Lélio Brun
  | Transition :
29
      ident (* node name *)
30
      * ident option
31
      (* instance *)
32
      * int option
33
      (* transition index *)
34
      * ('a, 'b) expressions_t
35
      (* inputs *)
36
      * ('a, 'b) expressions_t
37
      (* locals *)
38
      * ('a, 'b) expressions_t
39
      (* outputs *)
40
      * bool (* reset *)
41
      * Utils.ISet.t (* memory footprint *)
42 aaa8e454 Lélio Brun
      -> 'a predicate_t
43
  | Reset of ident * ident * 'a
44 6d1693b9 Lélio Brun
  | MemoryPack of ident * ident option * int option
45 75c459f4 Lélio Brun
  | Initialization
46 6d1693b9 Lélio Brun
  | ResetCleared of ident
47 7a1b2819 Lélio Brun
48 75c459f4 Lélio Brun
type 'a formula_t =
49
  | True
50
  | False
51 ca7ff3f7 Lélio Brun
  | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
52 75c459f4 Lélio Brun
  | And of 'a formula_t list
53
  | Or of 'a formula_t list
54
  | Imply of 'a formula_t * 'a formula_t
55
  | Exists of var_decl list * 'a formula_t
56
  | Forall of var_decl list * 'a formula_t
57 ca7ff3f7 Lélio Brun
  | Ternary :
58
      ('a, 'b) expression_t * 'a formula_t * 'a formula_t
59
      -> 'a formula_t
60
  | Predicate : 'a predicate_t -> 'a formula_t
61 6d1693b9 Lélio Brun
  | StateVarPack of register_t
62 aaa8e454 Lélio Brun
  | ExistsMem of ident * 'a formula_t * 'a formula_t
63 75c459f4 Lélio Brun
64
(* type 'a simulation_t = {
65
 *   sname: node_desc;
66
 *   sindex: option int;
67
 *   sformula: 'a formula_t;
68
 * } *)
69
70 6d1693b9 Lélio Brun
type 'a memory_pack_t = {
71 ca7ff3f7 Lélio Brun
  mpname : node_desc;
72
  mpindex : int option;
73
  mpformula : 'a formula_t;
74 6d1693b9 Lélio Brun
}
75
76 75c459f4 Lélio Brun
type 'a transition_t = {
77 ca7ff3f7 Lélio Brun
  tname : node_desc;
78
  tindex : int option;
79
  tinputs : var_decl list;
80
  tlocals : var_decl list;
81
  toutputs : var_decl list;
82
  tformula : 'a formula_t;
83
  tfootprint : Utils.ISet.t;
84 7a1b2819 Lélio Brun
}