Project

General

Profile

Download (2.12 KB) Statistics
| Branch: | Tag: | Revision:
1
open Utils
2
open Lustre_types
3

    
4
type register_t = ResetFlag | StateVar of var_decl
5

    
6
type left_v
7

    
8
type right_v
9

    
10
type ('a, _) expression_t =
11
  | Val : 'a -> ('a, right_v) expression_t
12
  | Tag : ident -> ('a, right_v) expression_t
13
  | Var : var_decl -> ('a, left_v) expression_t
14
  | Memory : register_t -> ('a, left_v) expression_t
15

    
16
(** TODO: why moving this elsewhere makes the exhaustiveness check fail? *)
17
let type_of_l_value : type a. (a, left_v) expression_t -> Types.t = function
18
  | Var v ->
19
    v.var_type
20
  | Memory ResetFlag ->
21
    Type_predef.type_bool
22
  | Memory (StateVar v) ->
23
    v.var_type
24

    
25
type 'a predicate_t =
26
  | Transition :
27
      bool (* stateless *)
28
      * ident (* node name *)
29
      * ident option
30
      (* instance *)
31
      * int option
32
      (* transition index *)
33
      * ('a, 'b) expression_t list
34
      (* variables *)
35
      * bool (* reset *)
36
      * Utils.ISet.t (* memory footprint *)
37
      * ident Utils.IMap.t
38
      (* memory instances footprint *)
39
      -> 'a predicate_t
40
  | Reset of ident * ident * 'a
41
  | MemoryPack of ident * ident option * int option
42
  | Initialization
43
  | ResetCleared of ident
44

    
45
type 'a formula_t =
46
  | True
47
  | False
48
  | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
49
  | GEqual : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
50
  | And of 'a formula_t list
51
  | Or of 'a formula_t list
52
  | Imply of 'a formula_t * 'a formula_t
53
  | Exists of var_decl list * 'a formula_t
54
  | Forall of var_decl list * 'a formula_t
55
  | Ternary :
56
      ('a, 'b) expression_t * 'a formula_t * 'a formula_t
57
      -> 'a formula_t
58
  | Predicate : 'a predicate_t -> 'a formula_t
59
  | StateVarPack of register_t
60
  | ExistsMem of ident * 'a formula_t * 'a formula_t
61
  | Value of 'a
62

    
63
(* type 'a simulation_t = {
64
 *   sname: node_desc;
65
 *   sindex: option int;
66
 *   sformula: 'a formula_t;
67
 * } *)
68

    
69
type 'a memory_pack_t = {
70
  mpname : node_desc;
71
  mpindex : int option;
72
  mpformula : 'a formula_t;
73
}
74

    
75
type 'a transition_t = {
76
  tname : node_desc;
77
  tindex : int option;
78
  tvars : var_decl list;
79
  tformula : 'a formula_t;
80
  tmem_footprint : Utils.ISet.t;
81
  tinst_footprint : ident Utils.IMap.t;
82
}
(83-83/99)