trans.ml 10.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11

12
open Stdlib
Andrei Paskevich's avatar
Andrei Paskevich committed
13 14 15
open Ty
open Term
open Decl
16
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
17
open Task
18

19
let debug = Debug.register_info_flag "transform"
Andrei Paskevich's avatar
Andrei Paskevich committed
20 21
  ~desc:"Print@ debugging@ messages@ about@ application@ \
         of@ proof@ task@ transformations."
22

Andrei Paskevich's avatar
Andrei Paskevich committed
23
(** Task transformation *)
24

Andrei Paskevich's avatar
Andrei Paskevich committed
25 26
type 'a trans = task -> 'a
type 'a tlist = 'a list trans
27

28 29
let apply f x = f x

30
let identity   x =  x
Andrei Paskevich's avatar
Andrei Paskevich committed
31
let identity_l x = [x]
32

33 34
let return x = fun _ -> x

Andrei Paskevich's avatar
Andrei Paskevich committed
35
let conv_res c f x = c (f x)
36

Andrei Paskevich's avatar
Andrei Paskevich committed
37
let singleton f x = [f x]
38

39 40
let compose   f g x =             g (f x)
let compose_l f g x = Lists.apply g (f x)
Andrei Paskevich's avatar
Andrei Paskevich committed
41

42
let seq l x   = List.fold_left (fun x f -> f x) x l
43
let seq_l l x = List.fold_left (fun x f -> Lists.apply f x) [x] l
44

45
module Wtask = Weakhtbl.Make (struct
46
  type t = task_hd
47
  let tag t = t.task_tag
48
end)
49

50 51 52
let store fn = let tr = Wtask.memoize_option 63 fn in fun t -> match t with
  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}}} -> fn t
  | _ -> tr t
Andrei Paskevich's avatar
Andrei Paskevich committed
53

54 55
let bind f g = store (fun task -> g (f task) task)

56
let fold fn v =
57
  let h = Wtask.create 63 in
58
  let rewind acc task =
59
(*
60
    Format.eprintf "%c%d." (match task.task_decl.td_node with
61
    | Decl _ -> 'D' | Clone _ -> 'C'
62
    | Use _  -> 'U' | Meta _  -> 'M') (task.task_decl.td_tag);
63
*)
64
    let acc = fn task acc in
65 66 67
    match task.task_decl.td_node with
    | Decl {d_node = Dprop (Pgoal,_,_)} -> acc
    | _ -> Wtask.set h task acc; acc
68
  in
69
  let current task =
70
    try Some (Wtask.find h task)
71 72
    with Not_found -> None
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
73
  let rec accum todo = function
74
    | None -> List.fold_left rewind v todo
75
    | Some task -> begin match current task with
76 77 78
        | Some v -> List.fold_left rewind v todo
        | None   -> accum (task::todo) task.task_prev
      end
79
  in
80
  accum []
Andrei Paskevich's avatar
Andrei Paskevich committed
81

82
let fold_l fn v = fold (fun task -> Lists.apply (fn task)) [v]
Andrei Paskevich's avatar
Andrei Paskevich committed
83

84
let fold_map   fn v t = conv_res snd            (fold   fn (v, t))
85
let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t))
86
(* we use List.map instead of List.map_rev to preserve the order *)
Andrei Paskevich's avatar
Andrei Paskevich committed
87

88 89 90 91
let store_decl fn = let tr = Wdecl.memoize 63 fn in function
  | {d_node = Dprop (Pgoal,_,_)} as d -> fn d
  | d -> tr d

92
let gen_decl add fn =
93
  let fn = store_decl fn in
94 95 96
  let fn task acc = match task.task_decl.td_node with
    | Decl d -> List.fold_left add acc (fn d)
    | _ -> add_tdecl acc task.task_decl
97
  in
98
  fold fn
Andrei Paskevich's avatar
Andrei Paskevich committed
99

100
let gen_decl_l add fn =
101
  let fn = store_decl fn in
102
  let fn task acc = match task.task_decl.td_node with
103
    | Decl d -> List.map (List.fold_left add acc) (fn d)
104
    | _ -> [add_tdecl acc task.task_decl]
105
  in
106
  fold_l fn
107

108 109
let decl    = gen_decl   Task.add_decl
let decl_l  = gen_decl_l Task.add_decl
110 111
let tdecl   = gen_decl   add_tdecl
let tdecl_l = gen_decl_l add_tdecl
Andrei Paskevich's avatar
Andrei Paskevich committed
112

113 114 115 116
let apply_to_goal fn d = match d.d_node with
  | Dprop (Pgoal,pr,f) -> fn pr f
  | _ -> assert false

117 118 119 120 121 122 123 124 125
let gen_goal add fn = function
  | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
      List.fold_left add prev (apply_to_goal fn d)
  | _ -> assert false

let gen_goal_l add fn = function
  | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
      List.map (List.fold_left add prev) (apply_to_goal fn d)
  | _ -> assert false
126

127 128
let goal    = gen_goal   Task.add_decl
let goal_l  = gen_goal_l Task.add_decl
129 130 131
let tgoal   = gen_goal   add_tdecl
let tgoal_l = gen_goal_l add_tdecl

132
let rewrite fn = decl (fun d -> [decl_map fn d])
133
let rewriteTF fnT fnF = rewrite (TermTF.t_select fnT fnF)
134

135
let gen_add_decl add decls = store (function
136
  | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
137
      Task.add_decl (List.fold_left add prev decls) d
138
  | _ -> assert false)
139

140
let add_decls  = gen_add_decl Task.add_decl
141 142
let add_tdecls = gen_add_decl add_tdecl

143 144
(** dependent transformations *)

145
module Wtds = Weakhtbl.Make (struct
146
  type t = tdecl_set
147
  let tag s = s.tds_tag
148 149
end)

150
let on_theory_tds th fn =
151
  let fn = Wtds.memoize 17 fn in
152
  fun task -> fn (find_clone_tds task th) task
153

154
let on_meta_tds t fn =
155
  let fn = Wtds.memoize 17 fn in
156
  fun task -> fn (find_meta_tds task t) task
157

158
let on_theory th fn =
159
  let add td acc = match td.td_node with
160 161 162
    | Clone (_,sm) -> sm::acc
    | _ -> assert false
  in
163
  on_theory_tds th (fun tds -> fn (Stdecl.fold add tds.tds_set []))
164 165

let on_meta t fn =
166
  let add td acc = match td.td_node with
167 168 169
    | Meta (_,ma) -> ma::acc
    | _ -> assert false
  in
170
  on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set []))
171

172 173 174 175
let on_used_theory th fn =
  let td = create_null_clone th in
  on_theory_tds th (fun tds -> fn (Stdecl.mem td tds.tds_set))

176
let on_meta_excl t fn =
177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
  if not t.meta_excl then raise (NotExclusiveMeta t);
  let add td _ = match td.td_node with
    | Meta (_,ma) -> Some ma
    | _ -> assert false
  in
  on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set None))

let on_tagged_ty t fn =
  begin match t.meta_type with
    | MTty :: _ -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  let add td acc = match td.td_node with
    | Meta (_, MAty ty :: _) -> Sty.add ty acc
    | _ -> assert false
  in
  on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Sty.empty))
194 195

let on_tagged_ts t fn =
196 197 198 199 200 201 202 203 204
  begin match t.meta_type with
    | MTtysymbol :: _ -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  let add td acc = match td.td_node with
    | Meta (_, MAts ts :: _) -> Sts.add ts acc
    | _ -> assert false
  in
  on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Sts.empty))
205 206

let on_tagged_ls t fn =
207 208 209 210 211 212 213 214 215
  begin match t.meta_type with
    | MTlsymbol :: _ -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  let add td acc = match td.td_node with
    | Meta (_, MAls ls :: _) -> Sls.add ls acc
    | _ -> assert false
  in
  on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Sls.empty))
216 217

let on_tagged_pr t fn =
218 219 220 221 222 223 224 225 226
  begin match t.meta_type with
    | MTprsymbol :: _ -> ()
    | _ -> raise (NotTaggingMeta t)
  end;
  let add td acc = match td.td_node with
    | Meta (_, MApr pr :: _) -> Spr.add pr acc
    | _ -> assert false
  in
  on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Spr.empty))
227

228 229
(** debug *)
let print_meta f m task =
230 231 232 233
  let print_tds fmt m =
    Pp.print_iter1 Stdecl.iter Pp.newline Pretty.print_tdecl fmt
      (find_meta_tds task m).tds_set
  in
Andrei Paskevich's avatar
Andrei Paskevich committed
234
  Debug.dprintf f "@[<hov 2>meta %s :@\n%a@]@." m.Theory.meta_name print_tds m;
235 236
  task

237 238 239 240
(** register transformations *)

open Env

241
module Wenv = Weakhtbl.Make (struct
242
  type t = env
243
  let tag = env_tag
244 245 246 247
end)

exception UnknownTrans of string
exception KnownTrans of string
248
exception TransFailure of string * exn
249 250 251 252 253

let named s f (x : task) =
  Debug.dprintf debug "Apply transformation %s@." s;
  if Debug.test_flag Debug.stack_trace then f x
  else try f x with e -> raise (TransFailure (s,e))
254

255
type 'a reg_trans = Pp.formatted * (env -> 'a trans)
256

257 258
let transforms   : (task reg_trans) Hstr.t = Hstr.create 17
let transforms_l : (task list reg_trans) Hstr.t = Hstr.create 17
259

260
let register_transform ~desc s p =
261
  if Hstr.mem transforms s then raise (KnownTrans s);
262
  Hstr.replace transforms s (desc, fun _ -> named s p)
263

264
let register_transform_l ~desc s p =
265
  if Hstr.mem transforms_l s then raise (KnownTrans s);
266
  Hstr.replace transforms_l s (desc, fun _ -> named s p)
267

268
let register_env_transform ~desc s p =
269
  if Hstr.mem transforms s then raise (KnownTrans s);
270
  Hstr.replace transforms s (desc, Wenv.memoize 3 (fun e -> named s (p e)))
271

272
let register_env_transform_l ~desc s p =
273
  if Hstr.mem transforms_l s then raise (KnownTrans s);
274
  Hstr.replace transforms_l s (desc, Wenv.memoize 3 (fun e -> named s (p e)))
275 276

let lookup_transform s =
277
  try snd (Hstr.find transforms s)
278
  with Not_found -> raise (UnknownTrans s)
279 280

let lookup_transform_l s =
281
  try snd (Hstr.find transforms_l s)
282 283
  with Not_found -> raise (UnknownTrans s)

284 285
let list_transforms () =
  Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms []
286

287 288
let list_transforms_l () =
  Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms_l []
289

François Bobot's avatar
François Bobot committed
290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307
(** fast transform *)
type gentrans =
  | Trans_one of Task.task trans
  | Trans_list of Task.task tlist

let lookup_trans env name =
  try
    let t = lookup_transform name env in
    Trans_one t
  with UnknownTrans _ ->
    let t = lookup_transform_l name env in
    Trans_list t

let apply_transform tr_name env task =
   match lookup_trans env tr_name with
    | Trans_one t -> [apply t task]
    | Trans_list t -> apply t task

308
(** Flag-dependent transformations *)
309

310 311
exception UnknownFlagTrans of meta * string * string list
exception IllegalFlagTrans of meta
312

313
type ('a,'b) flag_trans = ('a -> 'b trans) Hstr.t
314

315 316
let on_flag m ft def arg =
  on_meta_excl m (fun alo ->
317
    let s = match alo with
318
      | None -> def
319
      | Some [MAstr s] -> s
320 321
      | _ -> raise (IllegalFlagTrans m)
    in
322
    let t = try Hstr.find ft s with
323
      | Not_found ->
324
          let l = Hstr.fold (fun s _ l -> s :: l) ft [] in
325 326
          raise (UnknownFlagTrans (m,s,l))
    in
327 328
    let tr_name = Printf.sprintf "%s : %s" m.meta_name s in
    named tr_name (t arg))
329

330 331 332 333 334
let () = Exn_printer.register (fun fmt exn -> match exn with
  | KnownTrans s ->
      Format.fprintf fmt "Transformation '%s' is already registered" s
  | UnknownTrans s ->
      Format.fprintf fmt "Unknown transformation '%s'" s
335 336 337 338 339 340
  | UnknownFlagTrans (m,s,l) ->
      Format.fprintf fmt "Bad parameter %s for the meta %s@." s m.meta_name;
      Format.fprintf fmt "Known parameters: %a"
        (Pp.print_list Pp.space Pp.string) l
  | IllegalFlagTrans m ->
      Format.fprintf fmt "Meta %s must be exclusive string-valued" m.meta_name
341 342 343
  | TransFailure (s,e) ->
      Format.fprintf fmt "Failure in transformation %s@\n%a" s
        Exn_printer.exn_printer e
344
  | e -> raise e)