task.ml 8.82 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(**************************************************************************)
(*                                                                        *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

open Util
open Ident
open Ty
open Term
open Decl
25
open Theory
26

27
28
29
(** Clone and meta history *)

type tdecl_set = {
30
31
32
  tds_set  : Stdecl.t;
  tds_weak : Hashweak.key;
  tds_tag  : int;
33
34
35
36
37
38
39
40
41
42
}

module Hstds = Hashcons.Make (struct
  type t = tdecl_set
  let equal s1 s2 = Stdecl.equal s1.tds_set s2.tds_set
  let hs_td td acc = Hashcons.combine acc td.td_tag
  let hash s = Stdecl.fold hs_td s.tds_set 0
  let tag n s = { s with tds_tag = n }
end)

43
44
45
46
47
let mk_tds s = Hstds.hashcons {
  tds_set  = s;
  tds_weak = Hashweak.create_key ();
  tds_tag  = -1
}
48

49
50
let empty_tds = mk_tds Stdecl.empty
let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
51
52
53
let tds_singleton td = mk_tds (Stdecl.singleton td)

let tds_equal = (==)
54

55
type clone_map = tdecl_set Mid.t
56
type meta_map = tdecl_set Mmeta.t
57
58

let cm_find cm th = try Mid.find th.th_name cm with Not_found -> empty_tds
59
60

let mm_find mm t =
61
  try Mmeta.find t mm with Not_found -> empty_tds
62
63

let cm_add cm th td = Mid.add th.th_name (tds_add td (cm_find cm th)) cm
64

65
let mm_add mm t td = if t.meta_excl
66
67
  then Mmeta.add t (tds_singleton td) mm
  else Mmeta.add t (tds_add td (mm_find mm t)) mm
68
69

(** Task *)
70

71
72
73
type task = task_hd option

and task_hd = {
74
75
76
77
78
79
80
  task_decl  : tdecl;        (* last declaration *)
  task_prev  : task;         (* context *)
  task_known : known_map;    (* known identifiers *)
  task_clone : clone_map;    (* cloning history *)
  task_meta  : meta_map;     (* meta properties *)
  task_weak  : Hashweak.key; (* weak hashtable key *)
  task_tag   : int;          (* unique task tag *)
81
82
}

83
84
let task_hd_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
85
let task_equal t1 t2 = match t1, t2 with
86
  | Some t1, Some t2 -> task_hd_equal t1 t2
Andrei Paskevich's avatar
Andrei Paskevich committed
87
  | None, None -> true
88
  | _ -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
89

90
module Hstask = Hashcons.Make (struct
91
  type t = task_hd
92

93
94
  let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
                  task_equal t1.task_prev t2.task_prev
95

96
  let hash task =
97
98
    let decl = task.task_decl.td_tag in
    let prev = option_apply 0 (fun t -> t.task_tag + 1) task.task_prev in
99
    Hashcons.combine decl prev
100
101

  let tag i task = { task with task_tag = i }
102
end)
103

104
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
105
106
107
  task_decl  = decl;
  task_prev  = prev;
  task_known = known;
108
  task_clone = clone;
109
  task_meta  = meta;
110
  task_weak  = Hashweak.create_key ();
111
  task_tag   = -1;
112
})
113

114
115
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
116
let task_meta  = option_apply Mmeta.empty (fun t -> t.task_meta)
117

118
119
let find_clone task th = cm_find (task_clone task) th
let find_meta  task t  = mm_find (task_meta  task) t
120

121
(* constructors with checks *)
122

Andrei Paskevich's avatar
Andrei Paskevich committed
123
exception LemmaFound
124
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
125
exception GoalFound
126
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
127

128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
let find_goal = function
  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,_)}}} -> Some p
  | _ -> None

let task_goal task  = match find_goal task with
  | Some pr -> pr
  | None    -> raise GoalNotFound

let check_task task = match find_goal task with
  | Some _  -> raise GoalFound
  | None    -> task

let check_decl = function
  | { d_node = Dprop (Plemma,_,_)} -> raise LemmaFound
  | { d_node = Dprop (Pskip,_,_)}  -> raise SkipFound
  | d -> d

let new_decl task d td =
  let kn = known_add_decl (task_known task) (check_decl d) in
  mk_task td (check_task task) kn (task_clone task) (task_meta task)

let new_decl task d td = try new_decl task d td with KnownIdent _ -> task

let new_clone task th td =
  let cl = cm_add (task_clone task) th td in
  mk_task td (check_task task) (task_known task) cl (task_meta task)

let new_meta task t td =
  let mt = mm_add (task_meta task) t td in
  mk_task td (check_task task) (task_known task) (task_clone task) mt
Andrei Paskevich's avatar
Andrei Paskevich committed
158

159
160
(* declaration constructors + add_decl *)

161
162
let add_decl task d = new_decl task d (create_decl d)

163
164
165
166
167
168
169
170
171
let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)
let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
let add_prop_decl tk k p f = add_decl tk (create_prop_decl k p f)

let add_ty_decls tk dl = List.fold_left add_decl tk (create_ty_decls dl)
let add_logic_decls tk dl = List.fold_left add_decl tk (create_logic_decls dl)
let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)

172
173
174
175
176
(* task constructors *)

let rec add_tdecl task td = match td.td_node with
  | Decl d -> new_decl task d td
  | Use th -> use_export task th
177
178
  | Clone (th,_,_,_) -> new_clone task th td
  | Meta (t,_) -> new_meta task t td
179

180
181
182
183
and flat_tdecl task td = match td.td_node with
  | Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
  | Decl { d_node = Dprop ((Pgoal|Pskip),_,_) } -> task
  | _ -> add_tdecl task td
184

185
186
and use_export task th =
  let td = create_null_clone th in
187
  if Stdecl.mem td (find_clone task th).tds_set then task else
188
  let task = List.fold_left flat_tdecl task th.th_decls in
189
  new_clone task th td
190
191
192

let clone_export = clone_theory flat_tdecl

193
let add_meta task t al = new_meta task t (create_meta t al)
194
195
196
197
198

(* split theory *)

let split_tdecl names (res,task) td = match td.td_node with
  | Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
199
    when option_apply true (Spr.mem pr) names ->
200
201
202
203
      let res = add_prop_decl task Pgoal pr f :: res in
      res, flat_tdecl task td
  | _ ->
      res, flat_tdecl task td
Andrei Paskevich's avatar
Andrei Paskevich committed
204

205
let split_theory th names init =
206
  fst (List.fold_left (split_tdecl names) ([],init) th.th_decls)
Andrei Paskevich's avatar
Andrei Paskevich committed
207

208
209
(* Generic utilities *)

210
211
212
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
213

214
215
216
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
217

218
219
220
221
222
let task_tdecls = task_fold (fun acc td -> td::acc) []

let task_decls  = task_fold (fun acc td ->
  match td.td_node with Decl d -> d::acc | _ -> acc) []

223
(* special selector for metaproperties of a single ident *)
224

225
exception NotTaggingMeta of meta
226

227
let find_tagged_ts t tds acc =
228
  begin match t.meta_type with
229
    | [MTtysymbol] -> ()
230
231
232
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
233
    | Meta (s, [MAts ts]) when meta_equal s t -> Sts.add ts acc
234
235
236
    | _ -> assert false) tds.tds_set acc

let find_tagged_ls t tds acc =
237
  begin match t.meta_type with
238
239
240
241
    | [MTlsymbol] -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
242
    | Meta (s, [MAls ls]) when meta_equal s t -> Sls.add ls acc
243
244
245
    | _ -> assert false) tds.tds_set acc

let find_tagged_pr t tds acc =
246
  begin match t.meta_type with
247
248
249
250
    | [MTprsymbol] -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
251
    | Meta (s, [MApr pr]) when meta_equal s t -> Spr.add pr acc
252
    | _ -> assert false) tds.tds_set acc
253

254
exception NotExclusiveMeta of meta
255

256
let get_meta_excl t tds =
257
  if not t.meta_excl then raise (NotExclusiveMeta t);
258
  Stdecl.fold (fun td _ -> match td.td_node with
259
    | Meta (s,arg) when s = t -> Some arg
260
261
    | _ -> assert false) tds.tds_set None

262
263
(* Exception reporting *)

264
let () = Exn_printer.register (fun fmt exn -> match exn with
265
  | LemmaFound ->   Format.fprintf fmt "Task cannot contain a lemma"
266
  | SkipFound ->    Format.fprintf fmt "Task cannot contain a skip"
267
268
  | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
  | GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
269
  | NotTaggingMeta m ->
270
      Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" m.meta_name
271
  | NotExclusiveMeta m ->
272
      Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
273
  | _ -> raise exn)
274