eval_match.ml 6.05 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
19 20 21 22 23 24 25 26

open Format
open Ident
open Ty
open Term
open Decl
open Pretty

27
type inline = known_map -> lsymbol -> ty list -> ty option -> bool
28 29 30 31 32 33 34 35 36 37 38 39

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
  | { d_node = Dtype _ } -> true
  | _ -> false

Andrei Paskevich's avatar
Andrei Paskevich committed
40 41 42
let rec dive env t = match t.t_node with
  | Tvar x ->
      (try dive env (Mvs.find x env) with Not_found -> t)
Andrei Paskevich's avatar
Andrei Paskevich committed
43
  | Tlet (t1, tb) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
44 45 46
      let x, t2 = t_open_bound tb in
      dive (Mvs.add x t1 env) t2
  | _ -> t_map (dive env) t
Andrei Paskevich's avatar
Andrei Paskevich committed
47

Andrei Paskevich's avatar
Andrei Paskevich committed
48 49
let make_flat_case kn t bl =
  let mk_b b = let p,t = t_open_branch b in [p],t in
Andrei Paskevich's avatar
Andrei Paskevich committed
50 51
  Pattern.CompileTerm.compile (find_constructors kn) [t] (List.map mk_b bl)

52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69
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
    | [ls] ->
        let s = ty_match Mtv.empty (Util.of_option 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
    | _ ->
        (v::vl, tl, f)

70 71 72 73
let t_label_merge { t_label = l; t_loc = p } t =
  let p = if t.t_loc = None then p else t.t_loc in
  t_label ?loc:p (l @ t.t_label) t

74 75
let eval_match ~inline kn t =
  let rec eval env t = match t.t_node with
76
    | Tapp (ls, tl) when inline kn ls (List.map t_type tl) t.t_ty ->
77 78 79 80
        begin match find_logic_definition kn ls with
          | None ->
              t_map (eval env) t
          | Some def ->
81
              t_label_merge t (eval env (unfold def tl t.t_ty))
82
        end
83
    | Tlet (t1, tb2) ->
84 85 86
        let t1 = eval env t1 in
        let x, t2, close = t_open_bound_cb tb2 in
        let t2 = eval (Mvs.add x t1 env) t2 in
87
        t_label_merge t (t_let_simp t1 (close x t2))
Andrei Paskevich's avatar
Andrei Paskevich committed
88
    | Tcase (t1, bl1) ->
Andrei Paskevich's avatar
Andrei Paskevich committed
89
        let t1 = eval env t1 in
Andrei Paskevich's avatar
Andrei Paskevich committed
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110
        let t1flat = dive env t1 in
        let r = try match t1flat.t_node with
          | Tapp (ls,_) when is_constructor kn ls ->
              eval env (make_flat_case kn t1flat bl1)
          | Tcase (t2, bl2) ->
              let mk_b b =
                let p,t = t_open_branch b in
                match t.t_node with
                  | Tapp (ls,_) when is_constructor kn ls ->
                      t_close_branch p (eval env (make_flat_case kn t bl1))
                  | _ -> raise Exit
              in
              t_case t2 (List.map mk_b bl2)
          | _ -> raise Exit
        with
          | Exit ->
              let mk_b b =
                let p,t,close = t_open_branch_cb b in
                close p (eval env t)
              in
              t_case t1 (List.map mk_b bl1)
Andrei Paskevich's avatar
Andrei Paskevich committed
111
        in
112
        t_label_merge t r
113 114 115
    | Tquant (q, qf) ->
        let vl,tl,f,close = t_open_quant_cb qf in
        let vl,tl,f = List.fold_left (add_quant kn) ([],tl,f) vl in
116
        t_label_merge t (t_quant_simp q (close (List.rev vl) tl (eval env f)))
117
    | _ ->
118
        t_map (eval env) t
119 120 121 122 123 124 125 126 127 128 129 130 131 132
  in
  eval Mvs.empty t

let rec linear vars t = match t.t_node with
  | Tvar x when Svs.mem x vars ->
      raise Exit
  | Tvar x ->
      Svs.add x vars
  | _ ->
      t_fold linear vars t

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

133 134 135 136
let is_algebraic_type kn ty = match ty.ty_node with
  | Tyapp (ts, _) -> find_constructors kn ts <> []
  | Tyvar _ -> false

137 138 139 140 141 142 143 144 145
(* 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
146
let rec inline_nonrec_linear kn ls tyl ty =
147 148 149
  (* 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 *)
150
  let d = Mid.find ls.ls_name kn in
151
  if Mid.mem ls.ls_name d.d_syms then false else
152
  match d.d_node with
153 154 155
    | Dlogic [_, Some def] ->
        begin try Wdecl.find inline_cache d with Not_found ->
          let _, t = open_ls_defn def in
156 157
          let t = eval_match ~inline:inline_nonrec_linear kn t in
          let res = linear t in
158 159 160 161
          Wdecl.set inline_cache d res;
          res
        end
    | _ -> false