Revision 75c459f4
Added by LĂ©lio Brun about 2 years ago
src/spec_types.ml  

4  4 
 In 
5  5 
 Out 
6  6  
7 
type expression_t = 

8 
 Cst of constant 

7 
type 'a expression_t = 

8 
 Val of 'a 

9 
 Tag of ident 

9  10 
 Var of var_decl 
10  11 
 Instance of state_t * ident 
11  12 
 Memory of state_t * ident 
12  13  
13  14 
type predicate_t = 
14 
 Atom of expression_t 

15 
 Equal of predicate_t * predicate_t 

16 
 Imply of predicate_t * predicate_t 

17 
 Exists of var_decl list * predicate_t list 

18 
 Forall of var_decl list * predicate_t list 

15 
(*  Memory_pack *) 

16 
 Clocked_on of ident 

17 
 Transition 

18 
 Initialization 

19  19  
20 
type transition_t = { 

20 
type 'a formula_t = 

21 
 True 

22 
 False 

23 
 Equal of 'a expression_t * 'a expression_t 

24 
 And of 'a formula_t list 

25 
 Or of 'a formula_t list 

26 
 Imply of 'a formula_t * 'a formula_t 

27 
 Exists of var_decl list * 'a formula_t 

28 
 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 

31  
32 
(* type 'a simulation_t = { 

33 
* sname: node_desc; 

34 
* sindex: option int; 

35 
* sformula: 'a formula_t; 

36 
* } *) 

37  
38 
type 'a transition_t = { 

21  39 
tname: node_desc; 
22 
tindex: int; 

40 
tindex: int option;


23  41 
tlocals: var_decl list; 
24  42 
toutputs: var_decl list; 
25 
tpredicate: predicate_t list;


43 
tformula: 'a formula_t;


26  44 
} 
45 
Also available in: Unified diff
start with Spec AST generation