Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 22fe1c93

History | View | Annotate | Download (2.84 KB)

1
open Format
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
type ident = Utils.ident
13
type rat = Utils.rat
14
type tag = Utils.tag
15

    
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
type type_dec =
24
    {ty_dec_desc: type_dec_desc;
25
     ty_dec_loc: Location.t}
26

    
27
and type_dec_desc =
28
  | Tydec_any
29
  | Tydec_int
30
  | Tydec_real
31
  | Tydec_float
32
  | Tydec_bool
33
  | Tydec_clock of type_dec_desc
34
  | Tydec_const of ident
35
  | Tydec_enum of ident list
36
  | Tydec_array of Dimension.dim_expr * type_dec_desc
37

    
38
type clock_dec =
39
    {ck_dec_desc: clock_dec_desc;
40
     ck_dec_loc: Location.t}
41

    
42
and clock_dec_desc =
43
  | Ckdec_any
44
  | Ckdec_bool of (ident * ident) list 
45
  | Ckdec_pclock of int * rat
46

    
47
type var_decl = 
48
    {var_id: ident;
49
     var_dec_type: type_dec;
50
     var_dec_clock: clock_dec;
51
     var_dec_const: bool;
52
     mutable var_type: Types.type_expr;
53
     mutable var_clock: Clocks.clock_expr;
54
     var_loc: Location.t}
55

    
56
(* The tag of an expression is a unique identifier used to distinguish
57
   different instances of the same node *)
58
type eexpr =
59
    {eexpr_tag: tag;
60
     eexpr_desc: eexpr_desc;
61
     mutable eexpr_type: Types.type_expr;
62
     mutable eexpr_clock: Clocks.clock_expr;
63
     eexpr_loc: Location.t}
64

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

    
84
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list)
85

    
86
type node_annot = {
87
  requires: eexpr list;
88
  ensures: ensures_t list;
89
  behaviors: (string * eexpr list * ensures_t list) list
90
}
91

    
92

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

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

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

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

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

    
114
(* Local Variables: *)
115
(* compile-command:"make -C .." *)
116
(* End: *)