Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 87 lines (72 sloc) 2.357 kB
fccc685 Initial open-source release
MLstate authored
1 (*
2 Copyright © 2011 MLstate
3
4 This file is part of OPA.
5
6 OPA is free software: you can redistribute it and/or modify it under the
7 terms of the GNU Affero General Public License, version 3, as published by
8 the Free Software Foundation.
9
10 OPA is distributed in the hope that it will be useful, but WITHOUT ANY
11 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
12 FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
13 more details.
14
15 You should have received a copy of the GNU Affero General Public License
16 along with OPA. If not, see <http://www.gnu.org/licenses/>.
17 *)
18 (*
19 Authors: 2009, Vincent Benayoun <Vincent.Benayoun@mlstate.com>
20 *)
21
22 type ident = string
23
24 type hoop =
25 | HOAdd
26 | HOSubs
27 | HOMult
28 | HODiv
29 (* TODO : extend with mult, minus, ... *)
30
31 let hoop_arity o =
32 match o with
33 | HOAdd -> 2
34 | HOSubs -> 2
35 | HOMult -> 2
36 | HODiv -> 2
37
38 type hopred =
39 | HOEq
40 | HONeq
41 | HOLe
42 | HOLt
43
44
45 (* implicit database properties *)
46 type hoterm =
47 (* basic terms *)
48 | HO_Const of QmlAst.const_expr
49 | HO_ApplyOp of hoop * (hoterm list)
50 (* variables : term, property or predicate *)
51 | HO_Var of ident
52 (* predifined predicates *)
53 | HO_Pred of hopred * (hoterm list)
54 (* abstraction and application *)
55 | HO_Lambda of ident * hoterm
56 | HO_Apply of hoterm * hoterm
57 (* logical connectives *)
58 | HO_True
59 | HO_Not of hoterm
60 | HO_And of hoterm * hoterm
61 | HO_Or of hoterm * hoterm
62 | HO_Implies of hoterm * hoterm
63 | HO_Forall of ident * hoterm
64 | HO_Exists of ident * hoterm
65 (* property on evaluation of possibly impure qml expression
66 in which database is implicit *)
67 | HO_Exec of QmlAst.expr * (QmlAst.expr option) * hoterm (* exec e1 [returns e2] -> f *)
68 (* if [e1] is evaluated (in the value [e2]), the property [f] is true *)
69
70 type pcode_elt =
71 | Code_elt of QmlAst.code_elt
72 | Precondition of string * string * hoterm
73 | Postcondition of string * string * string * hoterm
74 | Property of string * hoterm
75 | Invariant of hoterm
76
77 type pcode = pcode_elt list
78
79
80 (* let pcode_to_code l = *)
81 (* let fold_fun acc c = *)
82 (* match c with *)
83 (* | Code_elt c -> c::acc *)
84 (* | _ -> acc *)
85 (* in *)
86 (* List.fold_left fold_fun [] l *)
Something went wrong with that request. Please try again.