Project

General

Profile

Revision 0038002e src/lustreSpec.ml

View differences:

src/lustreSpec.ml
1 1
open Format
2 2

  
3

  
4
let merge_expr_annot ann1 ann2 =
5
  match ann1, ann2 with
6
    | None, None -> assert false
7
    | Some _, None -> ann1
8
    | None, Some _ -> ann2
9
    | Some ann1, Some ann2 -> Some (ann1@ann2)
10

  
11

  
12 3
type ident = Utils.ident
4
type label = Utils.ident
13 5
type rat = Utils.rat
14 6
type tag = Utils.tag
15 7

  
16
type constant =
17
  | EConst_int of int
18
  | EConst_real of string
19
  | EConst_float of float
20
  | EConst_bool of bool
21
  | EConst_string of string
22

  
23 8
type type_dec =
24 9
    {ty_dec_desc: type_dec_desc;
25 10
     ty_dec_loc: Location.t}
......
54 39
     mutable var_clock: Clocks.clock_expr;
55 40
     var_loc: Location.t}
56 41

  
42
(** The core language and its ast. Every element of the ast contains its
43
    location in the program text. The type and clock of an ast element
44
    is mutable (and initialized to dummy values). This avoids to have to
45
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
46

  
47

  
48
type constant =
49
  | Const_int of int
50
  | Const_real of string
51
  | Const_float of float
52
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55
  | Const_struct of (label * constant) list
56

  
57
type quantifier_type = Exists | Forall
58

  
59

  
60

  
57 61
(* The tag of an expression is a unique identifier used to distinguish
58 62
   different instances of the same node *)
59
type eexpr =
63
type expr =
64
    {expr_tag: tag;
65
     expr_desc: expr_desc;
66
     mutable expr_type: Types.type_expr;
67
     mutable expr_clock: Clocks.clock_expr;
68
     mutable expr_delay: Delay.delay_expr;
69
     mutable expr_annot: expr_annot option;
70
     expr_loc: Location.t}
71

  
72
and expr_desc =
73
  | Expr_const of constant
74
  | Expr_ident of ident
75
  | Expr_tuple of expr list
76
  | Expr_ite   of expr * expr * expr
77
  | Expr_arrow of expr * expr
78
  | Expr_fby of expr * expr
79
  | Expr_array of expr list
80
  | Expr_access of expr * Dimension.dim_expr
81
  | Expr_power of expr * Dimension.dim_expr
82
  | Expr_pre of expr
83
  | Expr_when of expr * ident * label
84
  | Expr_merge of ident * (label * expr) list
85
  | Expr_appl of call_t
86
 and call_t = ident * expr * (ident * label) option 
87
     (* The third part denotes the reseting clock label and value *)
88
and 
89
  (* The tag of an expression is a unique identifier used to distinguish
90
     different instances of the same node *)
91
  eexpr =
60 92
    {eexpr_tag: tag;
61
     eexpr_desc: eexpr_desc;
93
     eexpr_qfexpr: expr;
94
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
62 95
     mutable eexpr_type: Types.type_expr;
63 96
     mutable eexpr_clock: Clocks.clock_expr;
97
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
64 98
     eexpr_loc: Location.t}
65 99

  
66
and eexpr_desc =
67
  | EExpr_const of constant
68
  | EExpr_ident of ident
69
  | EExpr_tuple of eexpr list
70
  | EExpr_arrow of eexpr * eexpr
71
  | EExpr_fby of eexpr * eexpr
72
  (* | EExpr_concat of eexpr * eexpr *)
73
  (* | EExpr_tail of eexpr *)
74
  | EExpr_pre of eexpr
75
  | EExpr_when of eexpr * ident
76
  (* | EExpr_whennot of eexpr * ident *)
77
  | EExpr_merge of ident * eexpr * eexpr
78
  | EExpr_appl of ident * eexpr * ident option
79
  (* | EExpr_uclock of eexpr * int *)
80
  (* | EExpr_dclock of eexpr * int *)
81
  (* | EExpr_phclock of eexpr * rat *)
82
  | EExpr_exists of var_decl list * eexpr
83
  | EExpr_forall of var_decl list * eexpr
84

  
85
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list)
100
and expr_annot = {
101
  annots: (string list * eexpr) list;
102
  annot_loc: Location.t
103
}
104
and 
105
 eq =
106
    {eq_lhs: ident list;
107
     eq_rhs: expr;
108
     eq_loc: Location.t}
109

  
86 110

  
87 111
type node_annot = {
88 112
  requires: eexpr list;
89
  ensures: ensures_t list;
90
  behaviors: (string * eexpr list * ensures_t list) list
113
  ensures: eexpr list;
114
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
115
  spec_loc: Location.t;
91 116
}
117
type assert_t = 
118
    {
119
      assert_expr: expr;
120
      assert_loc: Location.t
121
    } 
122

  
123
type node_desc =
124
    {node_id: ident;
125
     mutable node_type: Types.type_expr;
126
     mutable node_clock: Clocks.clock_expr;
127
     node_inputs: var_decl list;
128
     node_outputs: var_decl list;
129
     node_locals: var_decl list;
130
     mutable node_gencalls: expr list;
131
     mutable node_checks: Dimension.dim_expr list;
132
     node_asserts: assert_t list; 
133
     node_eqs: eq list;
134
     mutable node_dec_stateless: bool;
135
     mutable node_stateless: bool option;
136
     node_spec: node_annot option;
137
     node_annot: expr_annot list;
138
    }
139

  
140
type imported_node_desc =
141
    {nodei_id: ident;
142
     mutable nodei_type: Types.type_expr;
143
     mutable nodei_clock: Clocks.clock_expr;
144
     nodei_inputs: var_decl list;
145
     nodei_outputs: var_decl list;
146
     nodei_stateless: bool;
147
     nodei_spec: node_annot option;
148
     nodei_prototype: string option;
149
     nodei_in_lib: string option;
150
    }
151

  
152
type const_desc = 
153
    {const_id: ident; 
154
     const_loc: Location.t; 
155
     const_value: constant;      
156
     mutable const_type: Types.type_expr;
157
    }
158

  
159
type top_decl_desc =
160
| Node of node_desc
161
| Consts of const_desc list
162
| ImportedNode of imported_node_desc
163
| Open of bool * string (* the boolean set to true denotes a local 
164
			   lusi vs a lusi installed at system level *)
165

  
166
type top_decl =
167
    {top_decl_desc: top_decl_desc;
168
     top_decl_loc: Location.t}
169

  
170
type program = top_decl list
171

  
172
type error =
173
    Main_not_found
174
  | Main_wrong_kind
175
  | No_main_specified
176
  | Unbound_symbol of ident
177
  | Already_bound_symbol of ident
92 178

  
93 179

  
94
type expr_annot = (string list * eexpr) list 
95

  
96
let merge_node_annot ann1 ann2 =
97
  { requires = ann1.requires @ ann2.requires;
98
    ensures = ann1.ensures @ ann2.ensures;
99
    behaviors = ann1.behaviors @ ann2.behaviors;
100
  }
101

  
102
let mkeexpr loc d =
103
  { eexpr_tag = Utils.new_tag ();
104
    eexpr_desc = d;
105
    eexpr_type = Types.new_var ();
106
    eexpr_clock = Clocks.new_var true;
107
    eexpr_loc = loc }
108

  
109
let mkepredef_call loc funname args =
110
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
111

  
112
let mkepredef_unary_call loc funname arg =
113
  mkeexpr loc (EExpr_appl (funname, arg, None))
114 180

  
115 181
(* Local Variables: *)
116 182
(* compile-command:"make -C .." *)

Also available in: Unified diff