eval_match.ml 7.22 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
      | 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

87 88
exception FoundIdl of preid list

Andrei Paskevich's avatar
Andrei Paskevich committed
89 90
let rec add_quant kn (vl,tl,f) ({vs_ty = ty} as v) =
  match destructible kn ty with
91 92
  | Some ls ->
      let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112
      let mk_v id ty = create_vsymbol id (ty_inst s ty) in
      let clone id = List.map (fun _ -> id_clone id) ls.ls_args in
      let rec lookup_names f = match f.t_node with
        | Tcase ({t_node = Tvar u}, [bt]) when vs_equal u v ->
            begin match (fst (t_open_branch bt)).pat_node with
              | Pvar x -> raise (FoundIdl (clone x.vs_name))
              | Papp (cs, pl) when ls_equal ls cs ->
                  let name p = match p.pat_node with
                    | Pvar x -> id_clone x.vs_name
                    | _ -> id_clone v.vs_name in
                  raise (FoundIdl (List.map name pl))
              | Papp _ | Pwild | Por _ | Pas _ -> ()
            end
        | Tcase (t, [bt]) ->
            lookup_names t; lookup_names (snd (t_open_branch bt))
        | Tcase (t, _) | Tbinop (Timplies, _, t) -> lookup_names t
        | Tquant (_, qf) -> let _,_,f = t_open_quant qf in lookup_names f
        | _ -> () in
      let idl = try lookup_names f; clone v.vs_name with FoundIdl idl -> idl in
      let nvl = List.map2 mk_v idl ls.ls_args in
113 114 115 116 117 118
      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)
119

Andrei Paskevich's avatar
Andrei Paskevich committed
120 121 122
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
123 124
  (* 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
125 126 127 128 129 130 131
  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)

132 133
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
134
  t_attr_copy t (match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
135 136 137 138
    | 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)
139
    | Tapp (ls,tl) when ls.ls_constr > 0 -> fn env t ls tl
Andrei Paskevich's avatar
Andrei Paskevich committed
140 141
    | _ -> raise Exit)

Andrei Paskevich's avatar
Andrei Paskevich committed
142
let rec cs_equ env t1 t2 =
143 144 145 146 147 148 149 150
  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
151

152 153 154 155 156
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
157
let rec eval_match kn stop env t =
158
  let stop = stop || t.t_ty <> None ||
Andrei Paskevich's avatar
Andrei Paskevich committed
159
             Sattr.mem Ity.annot_attr t.t_attrs in
Andrei Paskevich's avatar
Andrei Paskevich committed
160
  let eval env t = eval_match kn stop env t in
Andrei Paskevich's avatar
Andrei Paskevich committed
161
  t_attr_copy t (match t.t_node with
162
    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
163
        cs_equ env (eval env t1) (eval env t2)
164 165
    | 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
166
    | Tapp (ls, [t1]) when is_projection ls ->
167
        let t1 = eval env t1 in
168 169
        let fn _env _t2 cs tl =
          select_field ls (cs_fields kn cs) tl in
Andrei Paskevich's avatar
Andrei Paskevich committed
170
        begin try dive_to_constructor fn env t1
171
        with Exit -> t_app ls [t1] t.t_ty end
Andrei Paskevich's avatar
Andrei Paskevich committed
172 173 174 175
    | 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
176
        end
177
    | Tlet (t1, tb2) ->
178
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
179
        let_map eval env t1 tb2
Andrei Paskevich's avatar
Andrei Paskevich committed
180
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
181
        let t1 = eval env t1 in
182 183
        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
184
        begin try dive_to_constructor fn env t1
Andrei Paskevich's avatar
Andrei Paskevich committed
185
        with Exit -> branch_map eval env t1 bl1 end
186 187
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
Andrei Paskevich's avatar
Andrei Paskevich committed
188 189
        let vl,tl,f = if stop then List.rev vl,tl,f else
          List.fold_left (add_quant kn) ([],tl,f) vl in
190
        t_quant_simp q (close (List.rev vl) tl (eval env f))
191
    | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
192 193 194
        t_map (eval env) t)

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