eval_match.ml 7.17 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
16

open Ident
open Ty
open Term
open Decl

17
type inline = known_map -> lsymbol -> ty list -> ty option -> bool
18
19
20
21
22
23
24
25
26

let unfold def tl ty =
  let vl, e = open_ls_defn def in
  let add (mt,mv) x y = ty_match mt x.vs_ty (t_type y), Mvs.add x y mv in
  let (mt,mv) = List.fold_left2 add (Mtv.empty, Mvs.empty) vl tl in
  let mt = oty_match mt e.t_ty ty in
  t_ty_subst mt mv e

let is_constructor kn ls = match Mid.find ls.ls_name kn with
27
28
  | { d_node = Ddata dl } ->
      let constr (_,csl) = List.exists (fun (cs,_) -> ls_equal cs ls) csl in
29
      List.exists constr dl
30
31
  | _ -> false

32
let is_projection kn ls = match Mid.find ls.ls_name kn with
33
34
  | { d_node = Ddata dl } ->
      let constr (_,csl) = List.exists (fun (cs,_) -> ls_equal cs ls) csl in
35
36
37
      not (List.exists constr dl)
  | _ -> false

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

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

57
58
59
60
61
62
63
let rec add_quant kn (vl,tl,f) v =
  let ty = v.vs_ty in
  let cl = match ty.ty_node with
    | Tyapp (ts, _) -> find_constructors kn ts
    | _ -> []
  in
  match cl with
64
    | [ls,pjl] ->
65
        let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
        let mk_v ty pj =
	  (* The name of the field corresponding to the variable that is created  *)
	  let field_name = begin match pj with
	    | Some pj_ls ->
	      begin
		try
		  Ident.get_model_element_name ~labels:pj_ls.ls_name.id_label
		with Not_found -> pj_ls.ls_name.id_string
	      end
	    | _ -> ""
	  end in
	  let label = Ident.append_to_model_element_name
	    ~labels:v.vs_name.id_label ~to_append:("." ^ field_name) in
	  create_vsymbol (id_clone ~label v.vs_name) (ty_inst s ty) in

        let nvl = List.map2 mk_v ls.ls_args pjl in
82
83
84
85
86
87
88
        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
    | _ ->
        (v::vl, tl, f)

Andrei Paskevich's avatar
Andrei Paskevich committed
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
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
  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)

let dive_to_constructor kn fn env t =
  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)
    | Tapp (ls,_) when is_constructor kn ls -> fn env t
    | _ -> raise Exit)
  in
  dive env t

110
111
112
113
114
115
116
117
118
119
120
121
let rec cs_equ kn env t1 t2 =
  if t_equal t1 t2 then t_true
  else match t1,t2 with
    | { t_node = Tapp (cs,tl) }, t
    | t, { t_node = Tapp (cs,tl) } when is_constructor kn cs ->
        let fn = apply_cs_equ kn cs tl in
        begin try dive_to_constructor kn fn env t
        with Exit -> t_equ t1 t2 end
    | _ -> t_equ t1 t2

and apply_cs_equ kn cs1 tl1 env t = match t.t_node with
  | Tapp (cs2,tl2) when ls_equal cs1 cs2 ->
122
123
      let merge t1 t2 f = t_and_simp (cs_equ kn env t1 t2) f in
      List.fold_right2 merge tl1 tl2 t_true
124
125
126
  | Tapp _ -> t_false
  | _ -> assert false

127
let eval_match ~inline kn t =
128
129
130
  let rec eval stop env t =
    let stop = stop || Slab.mem Split_goal.stop_split t.t_label in
    let eval = eval stop in
131
    match t.t_node with
132
133
    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
        cs_equ kn env (eval env t1) (eval env t2)
134
135
136
137
138
    | Tapp (ls, [t1]) when is_projection kn ls ->
        let t1 = eval env t1 in
        let fn _env t = apply_projection kn ls t in
        begin try dive_to_constructor kn fn env t1
        with Exit -> t_app ls [t1] t.t_ty end
139
    | Tapp (ls, tl) when inline kn ls (List.map t_type tl) t.t_ty ->
140
        begin match find_logic_definition kn ls with
Andrei Paskevich's avatar
Andrei Paskevich committed
141
142
          | None -> t_map (eval env) t
          | Some def -> eval env (unfold def tl t.t_ty)
143
        end
144
    | Tlet (t1, tb2) ->
145
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
146
        let_map eval env t1 tb2
Andrei Paskevich's avatar
Andrei Paskevich committed
147
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
148
        let t1 = eval env t1 in
149
        let fn env t2 = eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
Andrei Paskevich's avatar
Andrei Paskevich committed
150
151
        begin try dive_to_constructor kn fn env t1
        with Exit -> branch_map eval env t1 bl1 end
152
153
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
154
155
156
        let vl,tl,f = if stop
          then (List.rev vl,tl,f)
          else List.fold_left (add_quant kn) ([],tl,f) vl in
157
        t_quant_simp q (close (List.rev vl) tl (eval env f))
158
    | _ ->
159
        t_map_simp (eval env) t
160
  in
161
  eval false Mvs.empty t
162
163

let rec linear vars t = match t.t_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
164
  | Tvar x -> Svs.add_new Exit x vars
165
  | Tif _ | Teps _ -> raise Exit
166
  | _ -> t_fold linear vars t
167
168
169
170

let linear t =
  try ignore (linear Svs.empty t); true with Exit -> false

171
172
173
174
let is_algebraic_type kn ty = match ty.ty_node with
  | Tyapp (ts, _) -> find_constructors kn ts <> []
  | Tyvar _ -> false

175
176
177
178
179
180
181
182
183
(* The following memoization by function definition is unsafe,
   since the same definition can be used in different contexts.
   If we could produce the record updates {| x with field = v |}
   that were linear (by eliminating occurrences of x.field in v),
   inline_nonrec_linear might not call eval_match at all and so
   be independent of the context. FIXME/TODO *)

let inline_cache = Wdecl.create 17

Andrei Paskevich's avatar
Andrei Paskevich committed
184
let rec inline_nonrec_linear kn ls tyl ty =
185
186
187
  (* at least one actual parameter (or the result) has an algebraic type *)
  List.exists (is_algebraic_type kn) (oty_cons tyl ty) &&
  (* and ls is not recursively defined and is linear *)
188
  let d = Mid.find ls.ls_name kn in
189
  if Mid.mem ls.ls_name d.d_syms then false else
190
  match d.d_node with
191
    | Dlogic [_,def] ->
192
        begin try Wdecl.find inline_cache d with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
193
194
          let vl,t = open_ls_defn def in
          let _,_,t = List.fold_left (add_quant kn) ([],[],t) vl in
195
196
          let t = eval_match ~inline:inline_nonrec_linear kn t in
          let res = linear t in
197
198
199
200
          Wdecl.set inline_cache d res;
          res
        end
    | _ -> false