eval_match.ml 6.38 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   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
Andrei Paskevich's avatar
Andrei Paskevich committed
16
open Pdecl
17

Andrei Paskevich's avatar
Andrei Paskevich committed
18 19 20
let is_projection kn ls = ls.ls_constr = 0 &&
  match Mid.find ls.ls_name kn with
  | { pd_node = PDtype _ } -> true
21 22
  | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
23 24 25 26 27 28 29 30 31 32 33 34 35
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
36

37
let apply_projection kn ls t = match t.t_node with
38 39 40 41 42 43 44 45 46 47 48
  | Tapp (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
49
  | _ -> assert false
50

51
let flat_case t bl =
Andrei Paskevich's avatar
Andrei Paskevich committed
52
  let mk_b b = let p,t = t_open_branch b in [p],t in
53 54
  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
55

Andrei Paskevich's avatar
Andrei Paskevich committed
56 57
(* we destruct tuples, units, and singleton records *)
let destructible kn ty =
58 59
  let cl = match ty.ty_node with
    | Tyapp (ts, _) -> find_constructors kn ts
Andrei Paskevich's avatar
Andrei Paskevich committed
60
    | _ -> [] in
61
  match cl with
Andrei Paskevich's avatar
Andrei Paskevich committed
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94
    | [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
    | Some ls ->
95
        let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
96 97 98 99 100 101
        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
Andrei Paskevich's avatar
Andrei Paskevich committed
102
    | None ->
103 104
        (v::vl, tl, f)

Andrei Paskevich's avatar
Andrei Paskevich committed
105 106 107
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
108 109
  (* 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
110 111 112 113 114 115 116
  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)

Andrei Paskevich's avatar
Andrei Paskevich committed
117
let dive_to_constructor fn env t =
Andrei Paskevich's avatar
Andrei Paskevich committed
118 119 120 121 122
  let rec dive env t = t_label_copy t (match t.t_node with
    | 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)
Andrei Paskevich's avatar
Andrei Paskevich committed
123
    | Tapp (ls,_) when ls.ls_constr > 0 -> fn env t
Andrei Paskevich's avatar
Andrei Paskevich committed
124 125 126 127
    | _ -> raise Exit)
  in
  dive env t

Andrei Paskevich's avatar
Andrei Paskevich committed
128
let rec cs_equ env t1 t2 =
129 130 131
  if t_equal t1 t2 then t_true
  else match t1,t2 with
    | { t_node = Tapp (cs,tl) }, t
Andrei Paskevich's avatar
Andrei Paskevich committed
132 133 134
    | t, { t_node = Tapp (cs,tl) } when cs.ls_constr > 0 ->
        let fn = apply_cs_equ cs tl in
        begin try dive_to_constructor fn env t
135 136 137
        with Exit -> t_equ t1 t2 end
    | _ -> t_equ t1 t2

Andrei Paskevich's avatar
Andrei Paskevich committed
138
and apply_cs_equ cs1 tl1 env t = match t.t_node with
139
  | Tapp (cs2,tl2) when ls_equal cs1 cs2 ->
Andrei Paskevich's avatar
Andrei Paskevich committed
140
      let merge t1 t2 f = t_and_simp (cs_equ env t1 t2) f in
141
      List.fold_right2 merge tl1 tl2 t_true
142 143 144
  | Tapp _ -> t_false
  | _ -> assert false

Andrei Paskevich's avatar
Andrei Paskevich committed
145 146 147 148
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
149
    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
150
        cs_equ env (eval env t1) (eval env t2)
151 152 153
    | Tapp (ls, [t1]) when is_projection kn ls ->
        let t1 = eval env t1 in
        let fn _env t = apply_projection kn ls t in
Andrei Paskevich's avatar
Andrei Paskevich committed
154
        begin try dive_to_constructor fn env t1
155
        with Exit -> t_app ls [t1] t.t_ty end
Andrei Paskevich's avatar
Andrei Paskevich committed
156 157 158 159
    | 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
160
        end
161
    | Tlet (t1, tb2) ->
162
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
163
        let_map eval env t1 tb2
Andrei Paskevich's avatar
Andrei Paskevich committed
164
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
165
        let t1 = eval env t1 in
166
        let fn env t2 = eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
167
        begin try dive_to_constructor fn env t1
Andrei Paskevich's avatar
Andrei Paskevich committed
168
        with Exit -> branch_map eval env t1 bl1 end
169 170
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
Andrei Paskevich's avatar
Andrei Paskevich committed
171 172
        let vl,tl,f = if stop then List.rev vl,tl,f else
          List.fold_left (add_quant kn) ([],tl,f) vl in
173
        t_quant_simp q (close (List.rev vl) tl (eval env f))
174
    | _ ->
Andrei Paskevich's avatar
Andrei Paskevich committed
175 176 177
        t_map (eval env) t)

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