task.ml 8.58 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
30
31
32
33
34
35
36
37
38
39
40
41
42
(** Clone and meta history *)

type tdecl_set = {
  tds_set : Stdecl.t;
  tds_tag : int;
}

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)

let mk_tds s = Hstds.hashcons { tds_set = s; tds_tag = -1 }
43

44
45
let empty_tds = mk_tds Stdecl.empty
let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
46
47
48
let tds_singleton td = mk_tds (Stdecl.singleton td)

let tds_equal = (==)
49

50
51
52
53
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mstr.t

let cm_find cm th = try Mid.find th.th_name cm with Not_found -> empty_tds
54
55
56

let mm_find mm t =
  try Mstr.find t mm with Not_found -> ignore (lookup_meta t); empty_tds
57
58

let cm_add cm th td = Mid.add th.th_name (tds_add td (cm_find cm th)) cm
59
60
61
62

let mm_add mm t td = if is_meta_exc t
  then Mstr.add t (tds_singleton td) mm
  else Mstr.add t (tds_add td (mm_find mm t)) mm
63
64

(** Task *)
65

66
67
68
type task = task_hd option

and task_hd = {
69
70
71
72
  task_decl  : tdecl;       (* last declaration *)
  task_prev  : task;        (* context *)
  task_known : known_map;   (* known identifiers *)
  task_clone : clone_map;   (* cloning history *)
73
  task_meta  : meta_map;    (* meta properties *)
74
  task_tag   : int;         (* unique task tag *)
75
76
}

77
78
let task_hd_equal = (==)

Andrei Paskevich's avatar
Andrei Paskevich committed
79
let task_equal t1 t2 = match t1, t2 with
80
  | Some t1, Some t2 -> task_hd_equal t1 t2
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  | None, None -> true
82
  | _ -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
83

84
module Hstask = Hashcons.Make (struct
85
  type t = task_hd
86

87
88
  let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
                  task_equal t1.task_prev t2.task_prev
89

90
  let hash task =
91
92
    let decl = task.task_decl.td_tag in
    let prev = option_apply 0 (fun t -> t.task_tag + 1) task.task_prev in
93
    Hashcons.combine decl prev
94
95

  let tag i task = { task with task_tag = i }
96
end)
97

98
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
99
100
101
  task_decl  = decl;
  task_prev  = prev;
  task_known = known;
102
  task_clone = clone;
103
  task_meta  = meta;
104
  task_tag   = -1;
105
})
106

107
108
109
110
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_meta  = option_apply Mstr.empty (fun t -> t.task_meta)

111
112
let find_clone task th = cm_find (task_clone task) th
let find_meta  task t  = mm_find (task_meta  task) t
113
114
115
116
117
118

let add_decl task d td =
  let kn = known_add_decl (task_known task) d in
  mk_task td task kn (task_clone task) (task_meta task)

let add_clone task th td =
119
  let cl = cm_add (task_clone task) th td in
120
121
122
  mk_task td task (task_known task) cl (task_meta task)

let add_meta task t td =
123
  let mt = mm_add (task_meta task) t td in
124
125
126
127
  mk_task td task (task_known task) (task_clone task) mt

(* add_decl with checks *)

Andrei Paskevich's avatar
Andrei Paskevich committed
128
exception LemmaFound
129
exception SkipFound
Andrei Paskevich's avatar
Andrei Paskevich committed
130
exception GoalFound
131
exception GoalNotFound
Andrei Paskevich's avatar
Andrei Paskevich committed
132

133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
let rec task_goal = function
  | Some task ->
      begin match task.task_decl.td_node with
        | Decl { d_node = Dprop (Pgoal,pr,_) } -> pr
        | Decl _ -> raise GoalNotFound
        | _ -> task_goal task.task_prev
      end
  | None -> raise GoalNotFound

let new_decl task d td = match d.d_node with
  | Dprop (Plemma,_,_) -> raise LemmaFound
  | Dprop (Pskip,_,_)  -> raise SkipFound
  | _ ->
      try ignore (task_goal task); raise GoalFound
      with GoalNotFound -> try add_decl task d td
      with KnownIdent _ -> task
Andrei Paskevich's avatar
Andrei Paskevich committed
149

150
151
(* declaration constructors + add_decl *)

152
153
let add_decl task d = new_decl task d (create_decl d)

154
155
156
157
158
159
160
161
162
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)

163
164
165
166
167
(* 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
168
  | Clone (th,_,_,_) -> add_clone task th td
169
  | Meta (t,_) -> add_meta task t td
170

171
172
173
174
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
175

176
177
and use_export task th =
  let td = create_null_clone th in
178
  if Stdecl.mem td (find_clone task th).tds_set then task else
179
180
  let task = List.fold_left flat_tdecl task th.th_decls in
  add_clone task th td
181
182
183

let clone_export = clone_theory flat_tdecl

184
185
186
187
188
189
let add_meta task t al = add_meta task t (create_meta t al)

(* split theory *)

let split_tdecl names (res,task) td = match td.td_node with
  | Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
190
    when option_apply true (Spr.mem pr) names ->
191
192
193
194
      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
195

Andrei Paskevich's avatar
Andrei Paskevich committed
196
let split_theory th names =
197
  fst (List.fold_left (split_tdecl names) ([],None) th.th_decls)
Andrei Paskevich's avatar
Andrei Paskevich committed
198

199
200
(* Generic utilities *)

201
202
203
let rec task_fold fn acc = function
  | Some task -> task_fold fn (fn acc task.task_decl) task.task_prev
  | None      -> acc
204

205
206
207
let rec task_iter fn = function
  | Some task -> fn task.task_decl; task_iter fn task.task_prev
  | None      -> ()
208

209
210
211
212
213
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) []

214
(* special selector for metaproperties of a single ident *)
215

216
exception NotTaggingMeta of string
217

218
let find_tagged_ts t tds acc =
219
  begin match lookup_meta t with
220
    | [MTtysymbol] -> ()
221
222
223
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
    | Meta (s, [MAts ts]) when s = t -> Sts.add ts acc
    | _ -> assert false) tds.tds_set acc

let find_tagged_ls t tds acc =
  begin match lookup_meta t with
    | [MTlsymbol] -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
    | Meta (s, [MAls ls]) when s = t -> Sls.add ls acc
    | _ -> assert false) tds.tds_set acc

let find_tagged_pr t tds acc =
  begin match lookup_meta t with
    | [MTprsymbol] -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  Stdecl.fold (fun td acc -> match td.td_node with
    | Meta (s, [MApr pr]) when s = t -> Spr.add pr acc
243
    | _ -> assert false) tds.tds_set acc
244

245
246
247
248
249
250
251
252
exception NotExclusiveMeta of string

let get_meta_exc t tds =
  if not (is_meta_exc t) then raise (NotExclusiveMeta t);
  Stdecl.fold (fun td _ -> match td.td_node with
    | Meta (s,_) when s = t -> Some td
    | _ -> assert false) tds.tds_set None

253
254
(* Exception reporting *)

255
let () = Exn_printer.register (fun fmt exn -> match exn with
256
  | LemmaFound ->   Format.fprintf fmt "Task cannot contain a lemma"
257
  | SkipFound ->    Format.fprintf fmt "Task cannot contain a skip"
258
259
  | GoalFound ->    Format.fprintf fmt "The task already ends with a goal"
  | GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
260
261
  | NotTaggingMeta s ->
      Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" s
262
263
  | NotExclusiveMeta s ->
      Format.fprintf fmt "Metaproperty '%s' is not exclusive" s
264
  | _ -> raise exn)
265