Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / lustreSpec.ml @ 6a6abd76

History | View | Annotate | Download (2.93 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_struct of (ident * type_dec_desc) list
37
  | Tydec_array of Dimension.dim_expr * type_dec_desc
38

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

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

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

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

    
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)
86

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

    
93

    
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

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