Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

ptree.ml 6.17 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
59
  | PPptuple of pattern list
Andrei Paskevich's avatar
Andrei Paskevich committed
60
  | PPpor of pattern * pattern
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62
  | PPpas of pattern * ident

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

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

(*s Declarations. *)

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

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

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

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

type type_def =
107
  | TDabstract
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
108
  | TDalias     of pty
109
  | TDalgebraic of (loc * ident * param list) list
110 111

type type_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
112 113
  td_loc    : loc;
  td_ident  : ident;
114
  td_params : ident list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
115
  td_def    : type_def;
116 117
}

118
type logic_decl = {
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
119 120
  ld_loc    : loc;
  ld_ident  : ident;
121
  ld_params : param list;
Jean-Christophe Filliâtre's avatar
logic  
Jean-Christophe Filliâtre committed
122 123
  ld_type   : pty option;
  ld_def    : lexpr option;
124 125
}

126 127 128
type ind_decl = {
  in_loc    : loc;
  in_ident  : ident;
129
  in_params : param list;
Andrei Paskevich's avatar
Andrei Paskevich committed
130
  in_def    : (loc * ident * lexpr) list;
131 132
}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
133 134 135
type prop_kind =
  | Kaxiom | Klemma | Kgoal

136 137 138 139 140 141 142 143
type metarg =
  | PMAts  of qualid
  | PMAls  of qualid
  | PMApr  of qualid
  | PMAstr of string
  | PMAint of string

type decl =
144 145 146 147
  | TypeDecl of type_decl list
  | LogicDecl of logic_decl list
  | IndDecl of ind_decl list
  | PropDecl of loc * prop_kind * ident * lexpr
148
  | UseClone of loc * use * clone_subst list option
149
  | Meta of loc * ident * metarg list
150

151 152 153 154 155 156 157

(* program files *)

type assertion_kind = Aassert | Aassume | Acheck

type lazy_op = LazyAnd | LazyOr

158
type variant = lexpr * qualid option
159 160 161 162 163 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

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

224 225
type is_mutable = bool

226 227 228 229 230 231 232 233
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
234
  | Dnamespace of loc * ident option * (* import: *) bool * program_decl list
235 236
  | Dmodel_type of is_mutable * ident * ident list * pty option
  | Drecord_type of ident * ident list * (is_mutable * ident * pty) list
237 238 239 240 241 242 243 244 245

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

type program_file = module_ list