Skip to content
Newer
Older
100644 96 lines (81 sloc) 2.57 KB
fccc685 Initial open-source release
MLstate authored Jun 21, 2011
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 (* cf mli *)
19
20 (* shorthands *)
21 module Q = QmlAst
22 module Qp = QmlpAst
23
24 (* -- *)
25 type t =
26 {
27 database : Q.code_elt list;
28 new_type : Q.code_elt list;
29 new_db_value : Q.code_elt list;
30 new_val : Q.code_elt list;
31 new_prop : Qp.pcode_elt list;
32 new_pre : Qp.pcode_elt list;
33 new_post : Qp.pcode_elt list
34 }
35
36 let empty =
37 {
38 database = [];
39 new_type = [];
40 new_db_value = [];
41 new_val = [];
42 new_prop = [];
43 new_pre = [];
44 new_post = [];
45 }
46
47 let add_elt env elt = match elt with
48 | Q.Database _ -> { env with database = elt::env.database }
49 | Q.NewDbValue _ -> { env with new_db_value = elt::env.new_db_value }
50 | Q.NewType _ -> { env with new_type = elt::env.new_type }
51 | Q.NewVal _
52 | Q.NewValRec _ -> { env with new_val = elt::env.new_val }
53
54 let add = List.fold_left add_elt
55
56 let add_pcode_elt env elt =
57 match elt with
58 | Qp.Code_elt elt -> add_elt env elt
59 | Qp.Precondition _ -> { env with new_pre = elt::env.new_pre }
60 | Qp.Postcondition _ -> { env with new_post = elt::env.new_post }
61 | Qp.Property _
62 | Qp.Invariant _ -> { env with new_prop = elt::env.new_prop }
63
64 let add_pcode = List.fold_left add_pcode_elt
65
66 let get t = (* tail without @ *)
67 let rec rev acc = function
68 | [] -> acc
69 | t::q -> rev (t::acc) q in
70 let acc = [] in
71 let acc = rev acc t.new_val in
72 let acc = rev acc t.new_db_value in
73 let acc = rev acc t.new_type in
74 rev acc t.database
75
76 module Get =
77 struct
78 let all = get
79 let database t = List.rev t.database
80 let new_type t = List.rev t.new_type
81 let new_db_value t = List.rev t.new_db_value
82 let new_val t = List.rev t.new_val
83 let new_prop t = List.rev t.new_prop
84 let new_pre t = List.rev t.new_pre
85 let new_post t = List.rev t.new_post
86 end
87
88 (** need a Rev-Get for custom concat (e.g. in a filter Ast) *)
89 module RevGet =
90 struct
91 let database t = t.database
92 let new_type t = t.new_type
93 let new_db_value t = t.new_db_value
94 let new_val t = t.new_val
95 end
Something went wrong with that request. Please try again.