eval_match.ml 12 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
11

12
open Stdlib
13 14 15 16
open Ident
open Ty
open Term
open Decl
17 18
open Ity
open Expr
Andrei Paskevich's avatar
Andrei Paskevich committed
19
open Pdecl
20

21 22
(* helper functions for algebraic types *)

23 24 25
let ls_of_rs s = match s.rs_logic with
  RLls ls -> ls | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
26 27 28
let is_projection kn ls = ls.ls_constr = 0 &&
  match Mid.find ls.ls_name kn with
  | { pd_node = PDtype _ } -> true
29 30
  | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
31 32 33 34 35 36 37 38 39 40 41 42 43
let find_constructors kn ({ts_name = id} as ts) =
  let rec find = function
    | {d_news = s}::dl when not (Mid.mem id s) -> find dl
    | {d_node = Ddata dl}::_ -> List.assq ts dl
    | _ -> [] in
  find (Mid.find id kn).pd_pure

let find_logic_definition kn ({ls_name = id} as ls) =
  let rec find = function
    | {d_news = s}::dl when not (Mid.mem id s) -> find dl
    | {d_node = Dlogic dl}::_ -> Some (List.assq ls dl)
    | _ -> None in
  find (Mid.find id kn).pd_pure
44

45 46 47 48 49 50 51 52 53 54 55
let apply_projection kn ls cs tl =
  let ts = match cs.ls_value with
    | Some { ty_node = Tyapp (ts,_) } -> ts
    | _ -> assert false in
  let pjl =
    try List.assq cs (find_constructors kn ts)
    with Not_found -> assert false in
  let find acc v = function
    | Some pj when ls_equal pj ls -> v
    | _ -> acc in
  List.fold_left2 find t_true tl pjl
56

57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
(* Part I - Invariant handling *)

let ls_valid =
  let v = create_tvsymbol (id_fresh "a") in
  create_psymbol (id_fresh "valid") [ty_var v]

(* Integer "points" represent individual values whose invariant
   may be broken. The special point 0 represents any value with
   verified invariant. Fresh points are assigned to values from
   top to bottom, so that a lesser point can never be reached
   from a greater point. Each point is associated to a list of
   fresh variables that correspond to the "temporary fields" of
   the point. Committing a point means that we prove that the
   temporary fields satisfy the invariant and then assume that
   the temporary fields are equal to the respective projections.

   Recursive "caps" represent deconstructible values from which
   points can be reached. Each variable is associated to a cap.
   A cap is either a zero point (committed value), a non-zero
   point (a record with a breakable invariant), a constructible
   value (characterized by the set of possible constructors),
   or a record with an unbreakable invariant. *)

type cap =
  | P of int            (* point *)
  | C of cap list Mls.t (* algebraic type *)
Andrei Paskevich's avatar
Andrei Paskevich committed
83
  | R of cap Mls.t      (* record with an unbreakable invariant *)
84 85

type point = {
86 87
  p_leaf   : term;                  (* term we can be reached from *)
  p_stem   : (term * pattern) list; (* deconstruction from a root *)
88 89 90
  p_fields : (vsymbol * cap) Mls.t; (* temporary fields *)
}

91 92 93 94 95 96 97 98 99 100 101 102 103
type binding =
  | E of point  (* endpoint *)
  | L of int    (* link *)

type state = {
  s_roots  : cap Mvs.t;       (* non-broken roots may be unbound *)
  s_points : binding Mint.t;  (* non-broken points may be unbound *)
}

let new_point =
  let c = ref 0 in
  fun () -> incr c; !c

Andrei Paskevich's avatar
Andrei Paskevich committed
104
(* TODO:
105 106
  - do not collapse on Eif and Ecase in k_expr when the type is fragile
*)
107 108 109 110 111

let add_var kn st v =
  let rp = ref st.s_points in
  let rec down stem leaf ty = match ty.ty_node with
    | Tyvar _ -> P 0
Andrei Paskevich's avatar
Andrei Paskevich committed
112
    | Tyapp (s,tl) ->
113 114
        let s = restore_its s in
        if not s.its_fragile && (* no need to go any further *)
115 116
           List.for_all (fun f -> f.its_frozen) s.its_arg_flg &&
           List.for_all (fun f -> f.its_frozen) s.its_reg_flg then P 0 else
117 118
        let sbs = List.fold_right2 Mtv.add s.its_ts.ts_args tl Mtv.empty in
        let d = find_its_defn kn s in
119
        if s.its_nonfree then if s.its_fragile then (* breakable record *)
Andrei Paskevich's avatar
Andrei Paskevich committed
120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
          let rec name t = match t.t_node with
            | Tapp (pj,[t]) -> name t ^ "_" ^ pj.ls_name.id_string
            | Tvar v -> v.vs_name.id_string
            | _ -> assert false (* never *) in
          let bn = name leaf in
          let add_field m f =
            let ty = Ty.ty_inst sbs (Opt.get f.rs_field).pv_vs.vs_ty in
            let nm = bn ^ "_" ^ f.rs_name.id_string in
            let v = create_vsymbol (id_fresh nm) ty in
            Mls.add (ls_of_rs f) (v, down [] (t_var v) ty) m in
          let pjs = List.fold_left add_field Mls.empty d.itd_fields in
          let bd = E {p_leaf = leaf; p_stem = stem; p_fields = pjs} in
          let np = new_point () in
          rp := Mint.add np bd !rp;
          P np
135
        else (* unbreakable record *)
136 137 138 139 140 141 142
          let add_field m f =
            let pj = ls_of_rs f in
            let ty = Ty.ty_inst sbs (Opt.get f.rs_field).pv_vs.vs_ty in
            match down stem (fs_app pj [leaf] ty) ty with
            | P 0 -> m | c -> Mls.add pj c m in
          let pjs = List.fold_left add_field Mls.empty d.itd_fields in
          if Mls.is_empty pjs then P 0 else R pjs
143
        else (* constructible type *)
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
          let add_field m f = Mpv.add (Opt.get f.rs_field) (ls_of_rs f) m in
          let pjm = List.fold_left add_field Mpv.empty d.itd_fields in
          let add_constr m c =
            let cs = ls_of_rs c in
            let inst f = Ty.ty_inst sbs f.pv_vs.vs_ty in
            let tyl = List.map inst c.rs_cty.cty_args in
            let conv_field f ty_f =
              match Mpv.find_opt f pjm with
              | Some pj -> down stem (fs_app pj [leaf] ty_f) ty_f
              | None ->
                  let pat_arg ({pv_vs = v} as a) ty = if pv_equal a f
                    then pat_var (create_vsymbol (id_clone v.vs_name) ty)
                    else pat_wild ty in
                  let pl = List.map2 pat_arg c.rs_cty.cty_args tyl in
                  let pat = pat_app cs pl ty in
                  let v = Svs.choose pat.pat_vars in
                  down ((leaf, pat)::stem) (t_var v) ty_f in
161
            Mls.add cs (List.map2 conv_field c.rs_cty.cty_args tyl) m in
162
          let css = List.fold_left add_constr Mls.empty d.itd_constructors in
163 164
          let chk _ l = List.for_all (function P 0 -> true | _ -> false) l in
          if Mls.for_all chk css then P 0 else C css
165 166 167 168 169
  in
  match down [] (t_var v) v.vs_ty with
  | P 0 -> st (* not broken *)
  | c -> { s_roots = Mvs.add v c st.s_roots; s_points = !rp }

Andrei Paskevich's avatar
Andrei Paskevich committed
170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193
let is_committed {s_points = sp} c =
  let rec down = function
    | P 0 -> ()
    | P n -> begin match Mint.find_opt n sp with
        | Some (L n) -> down (P n)
        | Some (E _) -> raise Exit
        | None -> () end
    | C css -> Mls.iter (fun _ fl -> List.iter down fl) css
    | R pjs -> Mls.iter (fun _ c -> down c) pjs in
  try down c; true with Exit -> false

let add_pat st c p =
  let rec down rt c p = match p.pat_node with
    | Pwild -> rt
    | Pvar v -> Mvs.add v c rt
    | Papp (cs, pl) -> begin match c with
        | C css -> begin match Mls.find_opt cs css with
            | Some cl -> List.fold_left2 down rt cl pl
            | None -> rt (* all fields are committed *) end
        | _ -> assert false (* should never happen *) end
    | Por _ -> assert (is_committed st c); rt
    | Pas (p,v) -> Mvs.add v c (down rt c p) in
  { st with s_roots = down st.s_roots c p }

194
(* Part II - EvalMatch simplification *)
Andrei Paskevich's avatar
Andrei Paskevich committed
195

Andrei Paskevich's avatar
Andrei Paskevich committed
196 197
(* we destruct tuples, units, and singleton records *)
let destructible kn ty =
198 199
  let cl = match ty.ty_node with
    | Tyapp (ts, _) -> find_constructors kn ts
Andrei Paskevich's avatar
Andrei Paskevich committed
200
    | _ -> [] in
201
  match cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233
    | [ls,_] when is_fs_tuple ls -> Some ls
    | [{ls_args = [_]} as ls, _] -> Some ls
    | [{ls_args = []}  as ls, _] -> Some ls
    | _ -> None

(* we inline projections of destructed types *)
let find_inlineable kn ls = match ls.ls_args with
  | [arg] when destructible kn arg <> None ->
      begin match find_logic_definition kn ls with
      | Some def ->
          let res = open_ls_defn def in
          begin match (snd res).t_node with
          | Tvar _ | Tconst _
          | Tapp (_, [{t_node = Tvar _}]) -> Some res
          | Tcase ({t_node = Tvar _}, [bt]) ->
              begin match t_open_branch bt with
              | _, {t_node = Tvar _} -> Some res
              | _ -> None end
          | _ -> None end
      | _ -> None end
  | _ -> None

let unfold_inlineable kn ls tl ty = match find_inlineable kn ls with
  | Some (vl, e) ->
      let mt = List.fold_left2 (fun mt x y ->
        ty_match mt x.vs_ty (t_type y)) Mtv.empty vl tl in
      let mv = List.fold_right2 Mvs.add vl tl Mvs.empty in
      Some (t_ty_subst (oty_match mt e.t_ty ty) mv e)
  | None -> None

let rec add_quant kn (vl,tl,f) ({vs_ty = ty} as v) =
  match destructible kn ty with
234 235 236 237 238 239 240 241 242 243
  | Some ls ->
      let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
      let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in
      let nvl = List.map mk_v ls.ls_args in
      let t = fs_app ls (List.map t_var nvl) ty in
      let f = t_let_close_simp v t f in
      let tl = tr_map (t_subst_single v t) tl in
      List.fold_left (add_quant kn) (vl,tl,f) nvl
  | None ->
      (v::vl, tl, f)
244

Andrei Paskevich's avatar
Andrei Paskevich committed
245 246 247
let let_map fn env t1 tb =
  let x,t2,close = t_open_bound_cb tb in
  let t2 = fn (Mvs.add x t1 env) t2 in
248 249
  (* TODO/FIXME? convert (let x = if f then True else False in h)
     into (forall x. (x = True <-> f) -> h) ? *)
Andrei Paskevich's avatar
Andrei Paskevich committed
250 251 252 253 254 255 256
  t_let_simp t1 (close x t2)

let branch_map fn env t1 bl =
  let mk_b b =
    let p,t2,close = t_open_branch_cb b in close p (fn env t2) in
  t_case t1 (List.map mk_b bl)

257 258 259
let rec dive_to_constructor fn env t =
  let dive env t = dive_to_constructor fn env t in
  t_label_copy t (match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
260 261 262 263
    | Tvar x -> dive env (Mvs.find_exn Exit x env)
    | Tlet (t1,tb) -> let_map dive env t1 tb
    | Tcase (t1,bl) -> branch_map dive env t1 bl
    | Tif (f,t1,t2) -> t_if_simp f (dive env t1) (dive env t2)
264
    | Tapp (ls,tl) when ls.ls_constr > 0 -> fn env t ls tl
Andrei Paskevich's avatar
Andrei Paskevich committed
265 266
    | _ -> raise Exit)

Andrei Paskevich's avatar
Andrei Paskevich committed
267
let rec cs_equ env t1 t2 =
268 269 270 271 272 273 274 275
  if t_equal t1 t2 then t_true else
  let right cs1 tl1 env _t2 cs2 tl2 =
    if not (ls_equal cs1 cs2) then t_false else
    t_and_simp_l (List.map2 (cs_equ env) tl1 tl2) in
  let left t2 env _t1 cs1 tl1 =
    dive_to_constructor (right cs1 tl1) env t2 in
  try dive_to_constructor (left t2) env t1
  with Exit -> t_equ t1 t2
276

277 278 279 280 281
let flat_case t bl =
  let mk_b b = let p,t = t_open_branch b in [p],t in
  let mk_case = t_case_close and mk_let = t_let_close_simp in
  Pattern.compile_bare ~mk_case ~mk_let [t] (List.map mk_b bl)

Andrei Paskevich's avatar
Andrei Paskevich committed
282 283 284 285
let rec eval_match kn stop env t =
  let stop = stop || Slab.mem Term.stop_split t.t_label in
  let eval env t = eval_match kn stop env t in
  t_label_copy t (match t.t_node with
286
    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
287
        cs_equ env (eval env t1) (eval env t2)
288 289
    | Tapp (ls, [t1]) when is_projection kn ls ->
        let t1 = eval env t1 in
290
        let fn _env _t2 cs tl = apply_projection kn ls cs tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
291
        begin try dive_to_constructor fn env t1
292
        with Exit -> t_app ls [t1] t.t_ty end
Andrei Paskevich's avatar
Andrei Paskevich committed
293 294 295 296
    | Tapp (ls, tl) ->
        begin match unfold_inlineable kn ls tl t.t_ty with
        | Some t -> eval env t
        | None -> t_map (eval env) t
297
        end
298
    | Tlet (t1, tb2) ->
299
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
300
        let_map eval env t1 tb2
Andrei Paskevich's avatar
Andrei Paskevich committed
301
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
302
        let t1 = eval env t1 in
303 304
        let fn env t2 _cs _tl =
          eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
305
        begin try dive_to_constructor fn env t1
Andrei Paskevich's avatar
Andrei Paskevich committed
306
        with Exit -> branch_map eval env t1 bl1 end
307 308
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
Andrei Paskevich's avatar
Andrei Paskevich committed
309 310
        let vl,tl,f = if stop then List.rev vl,tl,f else
          List.fold_left (add_quant kn) ([],tl,f) vl in
311
        t_quant_simp q (close (List.rev vl) tl (eval env f))
312
    | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
313 314 315
        t_map (eval env) t)

let eval_match kn t = eval_match kn false Mvs.empty t