split_goal.ml 12.8 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
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 13 14 15

open Ident
open Term
open Decl

16 17 18 19
let apply_rev_append fn acc l =
  List.fold_left (fun l e -> fn e :: l) acc l

let apply_append fn acc l = apply_rev_append fn acc (List.rev l)
20 21

let apply_append2 fn acc l1 l2 =
22
  Lists.fold_product (fun l e1 e2 -> fn e1 e2 :: l)
23
    acc (List.rev l1) (List.rev l2)
24

25 26
let split_case forig spl pos acc tl bl =
  let c = if pos then t_true else t_false in
27
  let bl = List.rev_map t_open_branch_cb bl in
28
  let bll,_ = List.fold_left (fun (bll,el) (pl,f,close) ->
29
    let spf = spl [] f in
Andrei Paskevich's avatar
Andrei Paskevich committed
30
    let brc = close pl c in
MARCHE Claude's avatar
MARCHE Claude committed
31
    let bll = List.map (fun rl -> brc::rl) bll in
32
    let bll = apply_append (fun f -> close pl f :: el) bll spf in
33
    bll, brc::el) ([],[]) bl
34
  in
35
  let fn bl = t_label_copy forig (t_case tl bl) in
Andrei Paskevich's avatar
Andrei Paskevich committed
36
  apply_append fn acc bll
37

38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
let compiled = Ident.create_label "split_goal: compiled match"

let split_case_2 kn forig spl pos acc t bl =
  let vs = create_vsymbol (id_fresh "q") (t_type t) in
  let tv = t_var vs in
  let conn f = t_label_copy forig (t_let_close_simp vs t f) in
  let qn = if pos then t_forall_close_simp else t_exists_close_simp in
  let jn = if pos then t_implies_simp else t_and_simp in
  let _, bll = List.fold_left (fun (cseen,acc) b ->
    let p, f = t_open_branch b in
    match p.pat_node with
    | Pwild ->
        let csl = match p.pat_ty.Ty.ty_node with
          | Ty.Tyapp (ts,_) -> Decl.find_constructors kn ts
          | _ -> assert false in
        let csall = Sls.of_list (List.rev_map fst csl) in
        let csnew = Sls.diff csall cseen in
        assert (not (Sls.is_empty csnew));
        let add_cs cs g =
          let vl = List.map (create_vsymbol (id_fresh "w")) cs.ls_args in
          let f = t_equ tv (fs_app cs (List.map t_var vl) p.pat_ty) in
          t_or_simp g (t_exists_close_simp vl [] f) in
        let g = Sls.fold add_cs csnew t_false in
        let conn f = conn (jn g f) in
        csall, apply_rev_append conn acc (spl [] f)
    | Papp (cs, pl) ->
        let vl = List.map (function
          | {pat_node = Pvar v} -> v | _ -> assert false) pl in
        let g = t_equ tv (fs_app cs (List.map t_var vl) p.pat_ty) in
        let conn f = conn (qn vl [] (jn g f)) in
        assert (not (Sls.mem cs cseen));
        Sls.add cs cseen, apply_rev_append conn acc (spl [] f)
    | _ -> assert false) (Sls.empty,[]) bl
  in
  List.rev_append bll acc

let split_case_2 kn forig spl pos acc t bl =
  if Slab.mem compiled forig.t_label then
    let lab = Slab.remove compiled forig.t_label in
    let forig = t_label ?loc:forig.t_loc lab forig in
    split_case_2 kn forig spl pos acc t bl
  else
80 81
    let mk_let = t_let_close_simp in
    let mk_case t bl = t_label_add compiled (t_case_close t bl) in
82
    let mk_b b = let p,f = t_open_branch b in [p], f in
83
    let f = Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl) in
84 85
    spl acc f

Andrei Paskevich's avatar
Andrei Paskevich committed
86
let stop_split = Ident.create_label "stop_split"
87

88
let stop f = Slab.mem stop_split f.t_label
89 90
let asym f = Slab.mem Term.asym_label f.t_label
let keep f = Slab.mem Term.keep_on_simp_label f.t_label
91 92

let unstop f =
93
  t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f
94

95 96 97
type split = {
  right_only : bool;
  stop_label : bool;
98
  respect_as : bool;
99
  comp_match : known_map option;
100 101
}

102
let rec split_pos ro acc f = match f.t_node with
103
  | _ when ro.stop_label && stop f -> unstop f :: acc
104
  | Ttrue -> if keep f then f::acc else acc
105
  | Tfalse -> f::acc
106
  | Tapp _ -> f::acc
107
  | Tbinop (Tand,f1,f2) when ro.respect_as && asym f1 ->
108 109
      split_pos ro (split_pos ro acc (t_implies f1 f2)) f1
  | Tbinop (Tand,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
110
      split_pos ro (split_pos ro acc f2) f1
111
  | Tbinop (Timplies,f1,f2) when ro.right_only ->
112
      let fn f2 = t_label_copy f (t_implies f1 f2) in
Andrei Paskevich's avatar
Andrei Paskevich committed
113
      apply_append fn acc (split_pos ro [] f2)
114 115
  | Tbinop (Timplies,f1,f2) ->
      let fn f1 f2 = t_label_copy f (t_implies f1 f2) in
Andrei Paskevich's avatar
Andrei Paskevich committed
116
      apply_append2 fn acc (split_neg ro [] f1) (split_pos ro [] f2)
117 118 119
  | Tbinop (Tiff,f1,f2) ->
      let f12 = t_label_copy f (t_implies f1 f2) in
      let f21 = t_label_copy f (t_implies f2 f1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
120
      split_pos ro (split_pos ro acc f21) f12
121
  | Tbinop (Tor,_,_) when ro.right_only -> f::acc
122 123
  | Tbinop (Tor,f1,f2) ->
      let fn f1 f2 = t_label_copy f (t_or f1 f2) in
Andrei Paskevich's avatar
Andrei Paskevich committed
124
      apply_append2 fn acc (split_pos ro [] f1) (split_pos ro [] f2)
125 126
  | Tnot f1 ->
      let fn f1 = t_label_copy f (t_not f1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
127
      apply_append fn acc (split_neg ro [] f1)
128
  | Tif (fif,fthen,felse) ->
129 130
      let fit = t_label_copy f (t_implies fif fthen) in
      let fie = t_label_copy f (t_implies (t_not fif) felse) in
Andrei Paskevich's avatar
Andrei Paskevich committed
131
      split_pos ro (split_pos ro acc fie) fit
132
  | Tlet (t,fb) ->
133 134
      let vs,f1,close = t_open_bound_cb fb in
      let fn f1 = t_label_copy f (t_let t (close vs f1)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
135
      apply_append fn acc (split_pos ro [] f1)
136 137
  | Tcase (tl,bl) when ro.comp_match <> None ->
      split_case_2 (Opt.get ro.comp_match) f (split_pos ro) true acc tl bl
138
  | Tcase (tl,bl) ->
139
      split_case f (split_pos ro) true acc tl bl
140 141 142
  | Tquant (Tforall,fq) ->
      let vsl,trl,f1,close = t_open_quant_cb fq in
      let fn f1 = t_label_copy f (t_forall (close vsl trl f1)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
143
      apply_append fn acc (split_pos ro [] f1)
144
  | Tquant (Texists,_) -> f::acc
145
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
146

147
and split_neg ro acc f = match f.t_node with
148
  | _ when ro.stop_label && stop f -> unstop f :: acc
149
  | Ttrue -> f::acc
150
  | Tfalse -> if keep f then f::acc else acc
151
  | Tapp _ -> f::acc
152
  | Tbinop (Tand,_,_) when ro.right_only -> f::acc
153 154
  | Tbinop (Tand,f1,f2) ->
      let fn f1 f2 = t_label_copy f (t_and f1 f2) in
Andrei Paskevich's avatar
Andrei Paskevich committed
155
      apply_append2 fn acc (split_neg ro [] f1) (split_neg ro [] f2)
156
  | Tbinop (Timplies,f1,f2) when ro.respect_as && asym f1 ->
157 158 159 160 161 162
      split_neg ro (split_neg ro acc (t_and f1 f2)) (t_not f1)
  | Tbinop (Timplies,f1,f2) ->
      split_neg ro (split_neg ro acc f2) (t_not f1)
  | Tbinop (Tiff,f1,f2) ->
      let f12 = t_label_copy f (t_and f1 f2) in
      let f21 = t_label_copy f (t_and (t_not f1) (t_not f2)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
163
      split_neg ro (split_neg ro acc f21) f12
164
  | Tbinop (Tor,f1,f2) when ro.respect_as && asym f1 ->
165 166
      split_neg ro (split_neg ro acc (t_and (t_not f1) f2)) f1
  | Tbinop (Tor,f1,f2) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
167
      split_neg ro (split_neg ro acc f2) f1
168 169
  | Tnot f1 ->
      let fn f1 = t_label_copy f (t_not f1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
170
      apply_append fn acc (split_pos ro [] f1)
171
  | Tif (fif,fthen,felse) ->
172 173
      let fit = t_label_copy f (t_and fif fthen) in
      let fie = t_label_copy f (t_and (t_not fif) felse) in
Andrei Paskevich's avatar
Andrei Paskevich committed
174
      split_neg ro (split_neg ro acc fie) fit
175
  | Tlet (t,fb) ->
176 177
      let vs,f1,close = t_open_bound_cb fb in
      let fn f1 = t_label_copy f (t_let t (close vs f1)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
178
      apply_append fn acc (split_neg ro [] f1)
179 180
  | Tcase (tl,bl) when ro.comp_match <> None ->
      split_case_2 (Opt.get ro.comp_match) f (split_neg ro) false acc tl bl
181
  | Tcase (tl,bl) ->
182
      split_case f (split_neg ro) false acc tl bl
183 184 185
  | Tquant (Texists,fq) ->
      let vsl,trl,f1,close = t_open_quant_cb fq in
      let fn f1 = t_label_copy f (t_exists (close vsl trl f1)) in
Andrei Paskevich's avatar
Andrei Paskevich committed
186
      apply_append fn acc (split_neg ro [] f1)
187
  | Tquant (Tforall,_) -> f::acc
188
  | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
189

Andrei Paskevich's avatar
Andrei Paskevich committed
190
let split_goal ro pr f =
191
  let make_prop f = [create_prop_decl Pgoal pr f] in
Andrei Paskevich's avatar
Andrei Paskevich committed
192
  List.map make_prop (split_pos ro [] f)
193

Andrei Paskevich's avatar
Andrei Paskevich committed
194
let split_axiom ro pr f =
195 196
  let make_prop f =
    let pr = create_prsymbol (id_clone pr.pr_name) in
197
    create_prop_decl Paxiom pr f in
198
  let ro = { ro with respect_as = false } in
199 200 201
  match split_pos ro [] f with
    | [f] -> [create_prop_decl Paxiom pr f]
    | fl  -> List.map make_prop fl
202

Andrei Paskevich's avatar
Andrei Paskevich committed
203 204 205
let split_all ro d = match d.d_node with
  | Dprop (Pgoal, pr,f) ->  split_goal  ro pr f
  | Dprop (Paxiom,pr,f) -> [split_axiom ro pr f]
206 207
  | _ -> [[d]]

Andrei Paskevich's avatar
Andrei Paskevich committed
208 209
let split_premise ro d = match d.d_node with
  | Dprop (Paxiom,pr,f) ->  split_axiom ro pr f
210 211
  | _ -> [d]

212 213 214 215 216 217 218 219 220 221
let full_split = {
  right_only = false;
  stop_label = false;
  respect_as = true;
  comp_match = None;
}

let right_split = { full_split with right_only = true }
let wp_split    = { right_split with stop_label = true }
let intro_split = { wp_split with respect_as = false }
222 223 224 225 226 227 228 229 230

let split_pos_full  = split_pos full_split []
let split_neg_full  = split_neg full_split []

let split_pos_right = split_pos right_split []
let split_neg_right = split_neg right_split []

let split_pos_wp    = split_pos wp_split []
let split_neg_wp    = split_neg wp_split []
Andrei Paskevich's avatar
Andrei Paskevich committed
231

232 233 234
let split_pos_intro = split_pos intro_split []
let split_neg_intro = split_neg intro_split []

235 236 237
let split_goal_full  = Trans.goal_l (split_goal full_split)
let split_goal_right = Trans.goal_l (split_goal right_split)
let split_goal_wp    = Trans.goal_l (split_goal wp_split)
Andrei Paskevich's avatar
Andrei Paskevich committed
238

239 240 241
let split_all_full  = Trans.decl_l (split_all full_split) None
let split_all_right = Trans.decl_l (split_all right_split) None
let split_all_wp    = Trans.decl_l (split_all wp_split) None
Andrei Paskevich's avatar
Andrei Paskevich committed
242

243 244 245
let split_premise_full  = Trans.decl (split_premise full_split) None
let split_premise_right = Trans.decl (split_premise right_split) None
let split_premise_wp    = Trans.decl (split_premise wp_split) None
246

247
let () = Trans.register_transform_l "split_goal_full" split_goal_full
Andrei Paskevich's avatar
Andrei Paskevich committed
248
  ~desc:"Put@ the@ goal@ in@ a@ conjunctive@ form,@ \
249 250
  returns@ the@ corresponding@ set@ of@ subgoals.@ The@ number@ of@ subgoals@ \
  generated@ may@ be@ exponential@ in@ the@ size@ of@ the@ initial@ goal."
251
let () = Trans.register_transform_l "split_all_full" split_all_full
Andrei Paskevich's avatar
Andrei Paskevich committed
252
  ~desc:"Same@ as@ split_goal_full,@ but@ also@ split@ premises."
253
let () = Trans.register_transform "split_premise_full" split_premise_full
Andrei Paskevich's avatar
Andrei Paskevich committed
254
  ~desc:"Same@ as@ split_all_full,@ but@ split@ only@ premises."
255 256

let () = Trans.register_transform_l "split_goal_right" split_goal_right
257 258
  ~desc:"@[<hov 2>Same@ as@ split_goal_full,@ but@ don't@ split:@,\
      - @[conjunctions under disjunctions@]@\n\
259 260
      - @[conjunctions on the left of implications.@]@]"
let () = Trans.register_transform_l "split_all_right" split_all_right
Andrei Paskevich's avatar
Andrei Paskevich committed
261
  ~desc:"Same@ as@ split_goal_right,@ but@ also@ split@ premises."
262
let () = Trans.register_transform "split_premise_right" split_premise_right
Andrei Paskevich's avatar
Andrei Paskevich committed
263
  ~desc:"Same@ as@ split_all_right,@ but@ split@ only@ premises."
264 265

let () = Trans.register_transform_l "split_goal_wp" split_goal_wp
266 267
  ~desc:"Same@ as@ split_goal_right,@ but@ stops@ at@ \
    the@ `stop_split'@ label@ and@ removes@ the@ label."
268
let () = Trans.register_transform_l "split_all_wp" split_all_wp
Andrei Paskevich's avatar
Andrei Paskevich committed
269
  ~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises."
270
let () = Trans.register_transform "split_premise_wp" split_premise_wp
Andrei Paskevich's avatar
Andrei Paskevich committed
271
  ~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises."
272 273

let () = Trans.register_transform_l "split_goal" split_goal_wp
274
  ~desc:"The@ deprecated@ name@ of@ split_goal_wp,@ \
275
    kept@ for@ compatibility@ purposes."
Andrei Paskevich's avatar
Andrei Paskevich committed
276

277 278 279
let ls_of_var v =
  create_fsymbol (id_fresh ("spl_" ^ v.vs_name.id_string)) [] v.vs_ty

Andrei Paskevich's avatar
Andrei Paskevich committed
280 281
let rec split_intro pr dl acc f =
  let rsp = split_intro pr dl in
282
  match f.t_node with
283
  | Ttrue when not (keep f) -> acc
284
  | Tbinop (Tand,f1,f2) when asym f1 ->
285 286
      rsp (rsp acc (t_implies f1 f2)) f1
  | Tbinop (Tand,f1,f2) ->
287
      rsp (rsp acc f2) f1
288
  | Tbinop (Timplies,f1,f2) ->
289 290
      let pp = create_prsymbol (id_fresh (pr.pr_name.id_string ^ "_spl")) in
      let dl = create_prop_decl Paxiom pp f1 :: dl in
Andrei Paskevich's avatar
Andrei Paskevich committed
291
      split_intro pr dl acc f2
292 293
  | Tbinop (Tiff,f1,f2) ->
      rsp (rsp acc (t_implies f2 f1)) (t_implies f1 f2)
294
  | Tif (fif,fthen,felse) ->
295
      rsp (rsp acc (t_implies (t_not fif) felse)) (t_implies fif fthen)
296
  | Tlet (t,fb) -> let vs,f = t_open_bound fb in
297
      let ls = ls_of_var vs in
298 299
      let f  = t_subst_single vs (fs_app ls [] vs.vs_ty) f in
      let dl = create_logic_decl [make_ls_defn ls [] t] :: dl in
Andrei Paskevich's avatar
Andrei Paskevich committed
300
      split_intro pr dl acc f
301
  | Tquant (Tforall,fq) -> let vsl,_,f = t_open_quant fq in
302
      let lls = List.map ls_of_var vsl in
303
      let add s vs ls = Mvs.add vs (fs_app ls [] vs.vs_ty) s in
304
      let f = t_subst (List.fold_left2 add Mvs.empty vsl lls) f in
305
      let add dl ls = create_param_decl ls :: dl in
306
      let dl = List.fold_left add dl lls in
Andrei Paskevich's avatar
Andrei Paskevich committed
307
      split_intro pr dl acc f
308 309
  | _ ->
      let goal f = List.rev (create_prop_decl Pgoal pr f :: dl) in
310
      List.rev_append (List.rev_map goal (split_pos_wp f)) acc
311

Andrei Paskevich's avatar
Andrei Paskevich committed
312
let split_intro = Trans.goal_l (fun pr f -> split_intro pr [] [] f)
313

Andrei Paskevich's avatar
Andrei Paskevich committed
314
let () = Trans.register_transform_l "split_intro" split_intro
315
  ~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
316
    the@ implication@ antecedents@ to@ premises."