Project

General

Profile

« Previous | Next » 

Revision 6d1693b9

Added by LĂ©lio Brun 7 months ago

work on spec generation almost done

View differences:

src/spec_types.ml
1 1
open Lustre_types
2 2

  
3
type state_t =
4
  | In
5
  | Out
6

  
7
type 'a expression_t =
8
  | Val of 'a
9
  | Tag of ident
10
  | Var of var_decl
11
  | Instance of state_t * ident
12
  | Memory of state_t * ident
13

  
14
type predicate_t =
15
  (* | Memory_pack *)
16
  | Clocked_on of ident
17
  | Transition of ident * int option
3
type register_t =
4
  | ResetFlag
5
  | StateVar of var_decl
6

  
7
type left_v
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.type_expr =
18
  function
19
  | Var v -> v.var_type
20
  | Memory ResetFlag -> Type_predef.type_bool
21
  | Memory (StateVar v) -> v.var_type
22

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

  
25
type 'a predicate_t =
26
  | Transition: ident * ident option * int option
27
                * ('a, 'b) expressions_t
28
                * ('a, 'b) expressions_t
29
                * ('a, 'b) expressions_t -> 'a predicate_t
30
  | MemoryPack of ident * ident option * int option
18 31
  | Initialization
32
  | ResetCleared of ident
19 33

  
20 34
type 'a formula_t =
21 35
  | True
22 36
  | False
23
  | Equal of 'a expression_t * 'a expression_t
37
  | Equal: ('a, left_v) expression_t * ('a, 'b) expression_t -> 'a formula_t
24 38
  | And of 'a formula_t list
25 39
  | Or of 'a formula_t list
26 40
  | Imply of 'a formula_t * 'a formula_t
27 41
  | Exists of var_decl list * 'a formula_t
28 42
  | Forall of var_decl list * 'a formula_t
29
  | Ternary of 'a expression_t * 'a formula_t * 'a formula_t
30
  | Predicate of predicate_t * 'a expression_t list
43
  | Ternary: ('a, 'b) expression_t * 'a formula_t * 'a formula_t -> 'a formula_t
44
  | Predicate: 'a predicate_t -> 'a formula_t
45
  | StateVarPack of register_t
46
  | ExistsMem of 'a formula_t * 'a formula_t
31 47

  
32 48
(* type 'a simulation_t = {
33 49
 *   sname: node_desc;
......
35 51
 *   sformula: 'a formula_t;
36 52
 * } *)
37 53

  
54
type 'a memory_pack_t = {
55
  mpname: node_desc;
56
  mpindex: int option;
57
  mpformula: 'a formula_t;
58
}
59

  
38 60
type 'a transition_t = {
39 61
  tname: node_desc;
40 62
  tindex: int option;
63
  tinputs: var_decl list;
41 64
  tlocals: var_decl list;
42 65
  toutputs: var_decl list;
43 66
  tformula: 'a formula_t;

Also available in: Unified diff