ptree.ml 6.3 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
7
(*    Andrei Paskevich                                                    *)
8 9 10 11 12 13 14 15 16 17 18
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25

(*s Parse trees. *)

type loc = Loc.position

(*s Logical expressions (for both terms and predicates) *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
26 27
type real_constant = Term.real_constant
type constant = Term.constant
MARCHE Claude's avatar
MARCHE Claude committed
28
type label = Ident.label
29

30
type pp_quant =
31
  | PPforall | PPexists | PPlambda | PPfunc | PPpred
32

33 34
type pp_binop =
  | PPand | PPor | PPimplies | PPiff
35

36
type pp_unop =
37
  | PPnot
38

39
type ident = { id : string; id_lab : label list; id_loc : loc }
40 41 42

type qualid =
  | Qident of ident
43
  | Qdot of qualid * ident
44

45 46 47
type pty =
  | PPTtyvar of ident
  | PPTtyapp of pty list * qualid
48
  | PPTtuple of pty list
49

50 51
type param = ident option * pty

Andrei Paskevich's avatar
Andrei Paskevich committed
52 53 54 55 56 57 58
type pattern =
  { pat_loc : loc; pat_desc : pat_desc }

and pat_desc =
  | PPpwild
  | PPpvar of ident
  | PPpapp of qualid * pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
59
  | PPprec of (qualid * pattern) list
60
  | PPptuple of pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
61
  | PPpor of pattern * pattern
Andrei Paskevich's avatar
Andrei Paskevich committed
62 63
  | PPpas of pattern * ident

64
type lexpr =
65 66 67
  { pp_loc : loc; pp_desc : pp_desc }

and pp_desc =
68 69
  | PPvar of qualid
  | PPapp of qualid * lexpr list
70 71 72
  | PPtrue
  | PPfalse
  | PPconst of constant
73 74 75
  | PPinfix of lexpr * ident * lexpr
  | PPbinop of lexpr * pp_binop * lexpr
  | PPunop of pp_unop * lexpr
76
  | PPif of lexpr * lexpr * lexpr
77
  | PPquant of pp_quant * param list * lexpr list list * lexpr
78
  | PPnamed of label * lexpr
79
  | PPlet of ident * lexpr * lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
80
  | PPeps of ident * pty * lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  | PPmatch of lexpr * (pattern * lexpr) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82
  | PPcast of lexpr * pty
83
  | PPtuple of lexpr list
84
  | PPrecord of (qualid * lexpr) list
85 86 87 88

(*s Declarations. *)

type plogic_type =
89
  | PPredicate of pty list
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
90
  | PFunction  of pty list * pty
91

92 93
type imp_exp =
  | Import | Export | Nothing
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
94

95
type use = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
96
  use_theory  : qualid;
97
  use_as      : ident option option;
98
  use_imp_exp : imp_exp;
Jean-Christophe Filliâtre's avatar
uses  
Jean-Christophe Filliâtre committed
99 100
}

101
type clone_subst =
102
  | CSns    of qualid option * qualid option
103 104 105 106
  | CStsym  of qualid * qualid
  | CSlsym  of qualid * qualid
  | CSlemma of qualid
  | CSgoal  of qualid
107

108 109
type is_mutable = bool

110
type type_def =
111
  | TDabstract
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
112
  | TDalias     of pty
113
  | TDalgebraic of (loc * ident * param list) list
114
  | TDrecord    of (loc * is_mutable * ident * pty) list
115 116

type type_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
117 118
  td_loc    : loc;
  td_ident  : ident;
119
  td_params : ident list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
120
  td_def    : type_def;
121 122
}

123
type logic_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
124 125
  ld_loc    : loc;
  ld_ident  : ident;
126
  ld_params : param list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
127 128
  ld_type   : pty option;
  ld_def    : lexpr option;
129 130
}

131 132 133
type ind_decl = {
  in_loc    : loc;
  in_ident  : ident;
134
  in_params : param list;
Andrei Paskevich's avatar
Andrei Paskevich committed
135
  in_def    : (loc * ident * lexpr) list;
136 137
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
138 139 140
type prop_kind =
  | Kaxiom | Klemma | Kgoal

141 142 143 144 145 146 147 148
type metarg =
  | PMAts  of qualid
  | PMAls  of qualid
  | PMApr  of qualid
  | PMAstr of string
  | PMAint of string

type decl =
149 150 151 152
  | TypeDecl of type_decl list
  | LogicDecl of logic_decl list
  | IndDecl of ind_decl list
  | PropDecl of loc * prop_kind * ident * lexpr
153
  | UseClone of loc * use * clone_subst list option
154
  | Meta of loc * ident * metarg list
155

156 157 158 159 160 161 162

(* program files *)

type assertion_kind = Aassert | Aassume | Acheck

type lazy_op = LazyAnd | LazyOr

163
type variant = lexpr * qualid option
164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236

type loop_annotation = {
  loop_invariant : lexpr option;
  loop_variant   : variant option;
}

type for_direction = To | Downto

type effect = {
  pe_reads  : qualid list;
  pe_writes : qualid list;
  pe_raises : qualid list;
}

type pre = lexpr

type post = lexpr * (qualid * lexpr) list

type type_v =
  | Tpure of pty
  | Tarrow of binder list * type_c

and type_c =
  { pc_result_type : type_v;
    pc_effect      : effect;
    pc_pre         : pre;
    pc_post        : post; }

and binder = ident * type_v option

type expr = {
  expr_desc : expr_desc;
  expr_loc  : loc;
}

and expr_desc =
  (* lambda-calculus *)
  | Econstant of constant
  | Eident of qualid
  | Eapply of expr * expr
  | Efun of binder list * triple
  | Elet of ident * expr * expr
  | Eletrec of (ident * binder list * variant option * triple) list * expr
  | Etuple of expr list
  (* control *)
  | Esequence of expr * expr
  | Eif of expr * expr * expr
  | Eloop of loop_annotation * expr
  | Elazy of lazy_op * expr * expr
  | Ematch of expr * (pattern * expr) list
  | Eskip
  | Eabsurd
  | Eraise of qualid * expr option
  | Etry of expr * (qualid * ident option * expr) list
  | Efor of ident * expr * for_direction * expr * lexpr option * expr
  (* annotations *)
  | Eassert of assertion_kind * lexpr
  | Elabel of ident * expr
  | Ecast of expr * pty
  | Eany of type_c

  (* TODO: ghost *)

and triple = pre * expr * post

type program_decl =
  | Dlet    of ident * expr
  | Dletrec of (ident * binder list * variant option * triple) list
  | Dlogic  of decl
  | Dparam  of ident * type_v
  | Dexn    of ident * pty option
  (* modules *)
  | Duse    of qualid * imp_exp * (*as:*) ident option
237
  | Dnamespace of loc * ident option * (* import: *) bool * program_decl list
238 239
  | Dmodel_type of is_mutable * ident * ident list * pty option
  | Drecord_type of ident * ident list * (is_mutable * ident * pty) list
240 241 242 243 244 245 246 247 248

type module_ = {
  mod_name   : ident;
  mod_labels : Ident.label list;
  mod_decl   : program_decl list;
}

type program_file = module_ list