pgm_ptree.ml 3.18 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  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
open Why

22 23
type loc = Loc.position

24 25
type ident = Ptree.ident

26 27 28 29 30 31
type qualid = Ptree.qualid

type constant = Term.constant

type assertion_kind = Aassert | Aassume | Acheck

32 33
type lazy_op = LazyAnd | LazyOr

34 35 36 37
type logic = Lexing.position * string

type lexpr = logic

38
type loop_annotation = {
39 40
  loop_invariant : lexpr option;
  loop_variant   : lexpr option;
41 42
}

43 44 45 46 47
type effect = {
  pe_reads  : ident list;
  pe_writes : ident list;
  pe_raises : ident list;
}
48

49 50 51 52
type pre = lexpr

type post = lexpr * (ident * lexpr) list

53 54
type type_v =
  | Tpure of Ptree.pty
55
  | Tarrow of binder list * type_c
56 57

and type_c =
58 59 60
  { pc_result_name : ident;
    pc_result_type : type_v;
    pc_effect      : effect;
61 62
    pc_pre         : pre;
    pc_post        : post; }
63

64
and binder = ident * type_v option
65

66
type variant = lexpr 
67

68 69
type expr = {
  expr_desc : expr_desc;
70 71 72
  expr_loc  : loc;
}

73
and expr_desc =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
74
  (* lambda-calculus *)
75 76
  | Econstant of constant
  | Eident of qualid
77
  | Eapply of expr * expr
78
  | Efun of binder list * triple
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
79
  | Elet of ident * expr * expr
80
  | Eletrec of (ident * binder list * variant option * triple) list * expr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
81
  (* control *)
82 83
  | Esequence of expr * expr
  | Eif of expr * expr * expr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
84 85
  | Ewhile of expr * loop_annotation * expr
  | Elazy of lazy_op * expr * expr
86
  | Ematch of expr list * (Ptree.pattern list * expr) list
87
  | Eskip 
88
  | Eabsurd
89
  | Eraise of ident * expr option
90
  | Etry of expr * (ident * ident option * expr) list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
91
  (* annotations *)
92
  | Eassert of assertion_kind * lexpr
93 94
  | Eghost of expr
  | Elabel of ident * expr
95
  | Ecast of expr * Ptree.pty
96
  | Eany of type_c
97

98
  (* TODO: ghost *)
99

100
and triple = pre * expr * post
101

102
type decl =
103 104
  | Dlet    of ident * expr
  | Dletrec of (ident * binder list * variant option * triple) list
105
  | Dlogic  of logic
106
  | Dparam  of ident * type_v
107
  | Dexn    of ident * Ptree.pty option
108 109

type file = decl list
110