eval_match.ml 6.25 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 13 14 15

open Ident
open Ty
open Term
open Decl
16
open Expr
Andrei Paskevich's avatar
Andrei Paskevich committed
17
open Pdecl
18

19 20
(* helper functions for algebraic types *)

Andrei Paskevich's avatar
Andrei Paskevich committed
21 22 23
let is_projection ls = ls.ls_constr = 0 &&
  try (restore_rs ls).rs_field <> None
  with Not_found -> false
24

25
let ts_constructors kn ({ts_name = id} as ts) =
Andrei Paskevich's avatar
Andrei Paskevich committed
26 27 28 29 30 31
  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

32 33
let ty_constructors kn ty = match ty.ty_node with
  | Tyapp (ts, _) -> ts_constructors kn ts
Andrei Paskevich's avatar
Andrei Paskevich committed
34 35
  | _ -> []

36
let ls_definition kn ({ls_name = id} as ls) =
Andrei Paskevich's avatar
Andrei Paskevich committed
37 38 39 40 41
  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
42

43
let cs_fields kn cs =
Andrei Paskevich's avatar
Andrei Paskevich committed
44
  let ty = Opt.get cs.ls_value in
45
  List.assq cs (ty_constructors kn ty)
Andrei Paskevich's avatar
Andrei Paskevich committed
46

47
let select_field pj pjl tl =
Andrei Paskevich's avatar
Andrei Paskevich committed
48 49 50
  let rec find tl pjl = match tl, pjl with
    | t::_, Some ls::_ when ls_equal pj ls -> t
    | _::tl, _::pjl -> find tl pjl
51
    | _ -> raise Not_found in
Andrei Paskevich's avatar
Andrei Paskevich committed
52 53
  find tl pjl

Andrei Paskevich's avatar
Andrei Paskevich committed
54 55
(* we destruct tuples, units, and singleton records *)
let destructible kn ty =
56
  match ty_constructors kn ty with
Andrei Paskevich's avatar
Andrei Paskevich committed
57 58 59 60
  | [ls,_] when is_fs_tuple ls -> Some ls
  | [{ls_args = [_]} as ls, _] -> Some ls
  | [{ls_args = []}  as ls, _] -> Some ls
  | _ -> None
Andrei Paskevich's avatar
Andrei Paskevich committed
61 62 63 64

(* we inline projections of destructed types *)
let find_inlineable kn ls = match ls.ls_args with
  | [arg] when destructible kn arg <> None ->
65
      begin match ls_definition kn ls with
Andrei Paskevich's avatar
Andrei Paskevich committed
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
      | 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
89 90 91 92 93 94 95 96 97 98
  | 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)
99

Andrei Paskevich's avatar
Andrei Paskevich committed
100 101 102
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
103 104
  (* 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
105 106 107 108 109 110 111
  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)

112 113
let rec dive_to_constructor fn env t =
  let dive env t = dive_to_constructor fn env t in
Andrei Paskevich's avatar
Andrei Paskevich committed
114
  t_attr_copy t (match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
115 116 117 118
    | 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)
119
    | Tapp (ls,tl) when ls.ls_constr > 0 -> fn env t ls tl
Andrei Paskevich's avatar
Andrei Paskevich committed
120 121
    | _ -> raise Exit)

Andrei Paskevich's avatar
Andrei Paskevich committed
122
let rec cs_equ env t1 t2 =
123 124 125 126 127 128 129 130
  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
131

132 133 134 135 136
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
137
let rec eval_match kn stop env t =
138
  let stop = stop || t.t_ty <> None ||
Andrei Paskevich's avatar
Andrei Paskevich committed
139
             Sattr.mem Ity.annot_attr t.t_attrs in
Andrei Paskevich's avatar
Andrei Paskevich committed
140
  let eval env t = eval_match kn stop env t in
Andrei Paskevich's avatar
Andrei Paskevich committed
141
  t_attr_copy t (match t.t_node with
142
    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
143
        cs_equ env (eval env t1) (eval env t2)
144 145
    | Tnot { t_node = Tapp (ls, [t1;t2]) } when ls_equal ls ps_equ ->
        t_not_simp (cs_equ env (eval env t1) (eval env t2))
Andrei Paskevich's avatar
Andrei Paskevich committed
146
    | Tapp (ls, [t1]) when is_projection ls ->
147
        let t1 = eval env t1 in
148 149
        let fn _env _t2 cs tl =
          select_field ls (cs_fields kn cs) tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
150
        begin try dive_to_constructor fn env t1
151
        with Exit -> t_app ls [t1] t.t_ty end
Andrei Paskevich's avatar
Andrei Paskevich committed
152 153 154 155
    | 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
156
        end
157
    | Tlet (t1, tb2) ->
158
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
159
        let_map eval env t1 tb2
Andrei Paskevich's avatar
Andrei Paskevich committed
160
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
161
        let t1 = eval env t1 in
162 163
        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
164
        begin try dive_to_constructor fn env t1
Andrei Paskevich's avatar
Andrei Paskevich committed
165
        with Exit -> branch_map eval env t1 bl1 end
166 167
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
Andrei Paskevich's avatar
Andrei Paskevich committed
168 169
        let vl,tl,f = if stop then List.rev vl,tl,f else
          List.fold_left (add_quant kn) ([],tl,f) vl in
170
        t_quant_simp q (close (List.rev vl) tl (eval env f))
171
    | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
172 173 174
        t_map (eval env) t)

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