split_goal.ml 6.63 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 25 26
(**************************************************************************)
(*                                                                        *)
(*  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 Ident
open Term
open Decl

let apply_append  fn = List.fold_left (fun l e -> fn e :: l)
let apply_append2 fn = Util.list_fold_product (fun l e1 e2 -> fn e1 e2 :: l)

27 28 29
let split_case spl c acc tl bl =
  let bl = List.rev_map f_open_branch bl in
  let bll,_ = List.fold_left (fun (bll,el) (pl,f) ->
30 31 32 33 34
    let spf = spl [] f in
    let brc = f_close_branch pl c in
    let bll = List.rev_map (fun rl -> brc::rl) bll in
    let bll = apply_append (fun f -> f_close_branch pl f :: el) bll spf in
    bll, brc::el) ([],[]) bl
35 36 37
  in
  apply_append (f_case tl) acc bll

MARCHE Claude's avatar
MARCHE Claude committed
38
let asym_split = Ident.label "asym_split"
39 40

let to_split f = List.exists (fun (l,_) -> l = "asym_split") f.f_label
41

42 43 44 45
let rec split_pos acc f = match f.f_node with
  | Ftrue -> acc
  | Ffalse -> f::acc
  | Fapp _ -> f::acc
46
  | Fbinop (Fand,f1,f2) when to_split f ->
47
      split_pos (split_pos acc (f_implies f1 f2)) f1
48 49 50 51 52 53 54 55 56 57 58
  | Fbinop (Fand,f1,f2) ->
      split_pos (split_pos acc f2) f1
  | Fbinop (Fimplies,f1,f2) ->
      apply_append2 f_implies acc (split_neg [] f1) (split_pos [] f2)
  | Fbinop (Fiff,f1,f2) ->
      split_pos (split_pos acc (f_implies f1 f2)) (f_implies f2 f1)
  | Fbinop (For,f1,f2) ->
      apply_append2 f_or acc (split_pos [] f1) (split_pos [] f2)
  | Fnot f ->
      apply_append f_not acc (split_neg [] f)
  | Fif (fif,fthen,felse) ->
59 60
      split_pos (split_pos acc (f_implies fif fthen)) 
        (f_implies (f_not fif) felse)
61
  | Flet (t,fb) -> let vs,f = f_open_bound fb in
62
      apply_append (f_let_close vs t) acc (split_pos [] f)
63 64
  | Fcase (tl,bl) ->
      split_case split_pos f_true acc tl bl
65 66
  | Fquant (Fforall,fq) -> let vsl,trl,f = f_open_quant fq in
      (* TODO : Remove unused variable *)
67
      apply_append (f_forall_close vsl trl) acc (split_pos [] f)
68 69 70 71 72 73 74 75
  | Fquant (Fexists,_) -> f::acc

and split_neg acc f = match f.f_node with
  | Ftrue -> f::acc
  | Ffalse -> acc
  | Fapp _ -> f::acc
  | Fbinop (Fand,f1,f2) ->
      apply_append2 f_and acc (split_neg [] f1) (split_neg [] f2)
76
  | Fbinop (Fimplies,f1,f2) when to_split f ->
77
      split_neg (split_neg acc (f_and f1 f2)) (f_not f1)
78 79 80 81
  | Fbinop (Fimplies,f1,f2) ->
      split_neg (split_neg acc f2) (f_not f1)
  | Fbinop (Fiff,f1,f2) ->
      split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
82
  | Fbinop (For,f1,f2) when to_split f ->
83
      split_neg (split_neg acc (f_and (f_not f1) f2)) f1
84 85 86 87 88 89 90
  | Fbinop (For,f1,f2) ->
      split_neg (split_neg acc f2) f1
  | Fnot f ->
      apply_append f_not acc (split_pos [] f)
  | Fif (fif,fthen,felse) ->
      split_neg (split_neg acc (f_and fif fthen)) (f_and (f_not fif) felse)
  | Flet (t,fb) -> let vs,f = f_open_bound fb in
91
      apply_append (f_let_close vs t) acc (split_neg [] f)
92 93
  | Fcase (tl,bl) ->
      split_case split_neg f_false acc tl bl
94 95
  | Fquant (Fexists,fq) -> let vsl,trl,f = f_open_quant fq in
      (* TODO : Remove unused variable *)
96
      apply_append (f_exists_close vsl trl) acc (split_neg [] f)
97 98
  | Fquant (Fforall,_) -> f::acc

99 100 101
let split_goal pr f =
  let make_prop f = [create_prop_decl Pgoal pr f] in
  List.map make_prop (split_pos [] f)
102

103 104 105 106 107 108
let split_axiom pr f =
  let make_prop f =
    let pr = create_prsymbol (id_clone pr.pr_name) in
    create_prop_decl Paxiom pr f
  in
  List.map make_prop (split_pos [] f)
109

110 111 112
let split_all d = match d.d_node with
  | Dprop (Pgoal, pr,f) ->  split_goal  pr f
  | Dprop (Paxiom,pr,f) -> [split_axiom pr f]
113 114
  | _ -> [[d]]

115 116 117 118 119 120 121
let split_premise d = match d.d_node with
  | Dprop (Paxiom,pr,f) ->  split_axiom pr f
  | _ -> [d]

let split_goal    = Trans.goal_l split_goal
let split_all     = Trans.decl_l split_all     None
let split_premise = Trans.decl   split_premise None
122

123 124 125
let () = Trans.register_transform_l "split_goal"    split_goal
let () = Trans.register_transform_l "split_all"     split_all
let () = Trans.register_transform   "split_premise" split_premise
126

127 128 129 130 131 132 133
let ls_of_var v =
  create_fsymbol (id_fresh ("spl_" ^ v.vs_name.id_string)) [] v.vs_ty

let rec rsplit pr dl acc f =
  let rsp = rsplit pr dl in
  match f.f_node with
  | Ftrue -> acc
134
  | Fbinop (Fand,f1,f2) when to_split f ->
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
      rsp (rsp acc (f_implies f1 f2)) f1
  | Fbinop (Fand,f1,f2) ->
      rsp (rsp acc f2) f1
  | Fbinop (Fimplies,f1,f2) ->
      let pp = create_prsymbol (id_fresh (pr.pr_name.id_string ^ "_spl")) in
      let dl = create_prop_decl Paxiom pp f1 :: dl in
      rsplit pr dl acc f2
  | Fbinop (Fiff,f1,f2) ->
      rsp (rsp acc (f_implies f1 f2)) (f_implies f2 f1)
  | Fif (fif,fthen,felse) ->
      rsp (rsp acc (f_implies fif fthen)) (f_implies (f_not fif) felse)
  | Flet (t,fb) -> let vs,f = f_open_bound fb in
      let ls = ls_of_var vs in
      let f  = f_subst_single vs (t_app ls [] vs.vs_ty) f in
      let dl = create_logic_decl [make_fs_defn ls [] t] :: dl in
      rsplit pr dl acc f
  | Fquant (Fforall,fq) -> let vsl,_,f = f_open_quant fq in
      let lls = List.map ls_of_var vsl in
      let add s vs ls = Mvs.add vs (t_app ls [] vs.vs_ty) s in
      let f = f_subst (List.fold_left2 add Mvs.empty vsl lls) f in
      let add dl ls = create_logic_decl [ls, None] :: dl in
      let dl = List.fold_left add dl lls in
      rsplit pr dl acc f
  | _ ->
      let goal f = List.rev (create_prop_decl Pgoal pr f :: dl) in
      List.rev_append (List.rev_map goal (split_pos [] f)) acc

let right_split = Trans.goal_l (fun pr f -> rsplit pr [] [] f)

let () = Trans.register_transform_l "right_split" right_split