Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/spec_types.ml
1 1
open Lustre_types
2 2

  
3
type register_t =
4
  | ResetFlag
5
  | StateVar of var_decl
3
type register_t = ResetFlag | StateVar of var_decl
6 4

  
7 5
type left_v
6

  
8 7
type right_v
9 8

  
10 9
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
10
  | 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
15 14

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

  
23 25
type ('a, 'b) expressions_t = ('a, 'b) expression_t list
24 26

  
25 27
type 'a predicate_t =
26
  | Transition: ident                        (* node name *)
27
                * ident option               (* instance *)
28
                * int option                 (* transition index *)
29
                * ('a, 'b) expressions_t       (* inputs *)
30
                * ('a, 'b) expressions_t       (* locals *)
31
                * ('a, 'b) expressions_t       (* outputs *)
32
                * bool                       (* reset *)
33
                * Utils.ISet.t               (* memory footprint *)
28
  | 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 *)
34 42
      -> 'a predicate_t
35 43
  | Reset of ident * ident * 'a
36 44
  | MemoryPack of ident * ident option * int option
......
40 48
type 'a formula_t =
41 49
  | True
42 50
  | False
43
  | Equal: ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
51
  | Equal : ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
44 52
  | And of 'a formula_t list
45 53
  | Or of 'a formula_t list
46 54
  | Imply of 'a formula_t * 'a formula_t
47 55
  | Exists of var_decl list * 'a formula_t
48 56
  | Forall of var_decl list * 'a formula_t
49
  | Ternary: ('a, 'b) expression_t * 'a formula_t * 'a formula_t -> 'a formula_t
50
  | Predicate: 'a predicate_t -> 'a formula_t
57
  | Ternary :
58
      ('a, 'b) expression_t * 'a formula_t * 'a formula_t
59
      -> 'a formula_t
60
  | Predicate : 'a predicate_t -> 'a formula_t
51 61
  | StateVarPack of register_t
52 62
  | ExistsMem of ident * 'a formula_t * 'a formula_t
53 63

  
......
58 68
 * } *)
59 69

  
60 70
type 'a memory_pack_t = {
61
  mpname: node_desc;
62
  mpindex: int option;
63
  mpformula: 'a formula_t;
71
  mpname : node_desc;
72
  mpindex : int option;
73
  mpformula : 'a formula_t;
64 74
}
65 75

  
66 76
type 'a transition_t = {
67
  tname: node_desc;
68
  tindex: int option;
69
  tinputs: var_decl list;
70
  tlocals: var_decl list;
71
  toutputs: var_decl list;
72
  tformula: 'a formula_t;
73
  tfootprint: Utils.ISet.t;
77
  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;
74 84
}
75

  

Also available in: Unified diff