pattern.ml 6.65 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
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
(*                                                                  *)
10
(********************************************************************)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
11 12 13 14 15

open Ident
open Ty
open Term

16
exception ConstructorExpected of lsymbol * ty
17
exception NonExhaustive of pattern list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
18

19 20
exception Bare

21
let compile ~get_constructors ~mk_case ~mk_let tl rl =
22
  let rec compile tl rl = match tl,rl with
23
    | _, [] -> (* no actions *)
24
        let pl = List.map (fun t -> pat_wild (t_type t)) tl in
25
        raise (NonExhaustive pl)
26 27 28
    | [], (_,a) :: _ -> (* no terms, at least one action *)
        a
    | t :: tl, _ -> (* process the leftmost column *)
29
        let ty = t_type t in
Andrei Paskevich's avatar
Andrei Paskevich committed
30
        (* extract the set of constructors *)
31
        let bare,css = match ty.ty_node with
32
          | Tyapp (ts,_) ->
33
              begin try false, Sls.of_list (get_constructors ts)
34 35 36 37 38 39
              with Bare -> true, Sls.empty end
          | Tyvar _ -> false, Sls.empty
        in
        (* if bare, only check fs.ls_constr *)
        let is_constr fs =
          fs.ls_constr > 0 && (bare || Sls.mem fs css)
40
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
41 42
        (* map every constructor occurring at the head
         * of the pattern list to the list of its args *)
43 44
        let types, cslist =
          let rec populate (css,csl as acc) p = match p.pat_node with
Andrei Paskevich's avatar
Andrei Paskevich committed
45 46 47
            | Pwild | Pvar _ -> acc
            | Pas (p,_) -> populate acc p
            | Por (p,q) -> populate (populate acc p) q
48 49 50
            | Papp (fs,pl) when is_constr fs ->
                if Mls.mem fs css then acc else
                Mls.add fs pl css, (fs,pl) :: csl
51
            | Papp (fs,_) -> raise (ConstructorExpected (fs,ty))
Andrei Paskevich's avatar
Andrei Paskevich committed
52 53
          in
          let populate acc (pl,_) = populate acc (List.hd pl) in
54
          List.fold_left populate (Mls.empty,[]) rl
55
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
56 57
        (* dispatch every case to a primitive constructor/wild case *)
        let cases,wilds =
58
          let add_case fs pl a cases =
59
            Mls.change (function
60
              | None -> Some [pl,a]
61
              | Some rl -> Some ((pl,a)::rl)) fs cases
62
          in
63
          let union_cases pl a types cases =
64 65 66 67 68
            let add pl q = pat_wild q.pat_ty :: pl in
            let wild ql = [List.fold_left add pl ql, a] in
            let join _ wl rl = Some (List.append wl rl) in
            Mls.union join (Mls.map wild types) cases
          in
Andrei Paskevich's avatar
Andrei Paskevich committed
69 70 71 72
          let rec dispatch (pl,a) (cases,wilds) =
            let p = List.hd pl in let pl = List.tl pl in
            match p.pat_node with
              | Papp (fs,pl') ->
73
                  add_case fs (List.rev_append pl' pl) a cases, wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
74 75 76 77 78 79
              | Por (p,q) ->
                  dispatch (p::pl, a) (dispatch (q::pl, a) (cases,wilds))
              | Pas (p,x) ->
                  dispatch (p::pl, mk_let x t a) (cases,wilds)
              | Pvar x ->
                  let a = mk_let x t a in
80
                  union_cases pl a types cases, (pl,a)::wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
81
              | Pwild ->
82
                  union_cases pl a types cases, (pl,a)::wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
83 84
          in
          List.fold_right dispatch rl (Mls.empty,[])
85
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
86 87
        (* how to proceed if [t] is [Tapp(cs,al)] and [cs] is in [cases] *)
        let comp_cases cs al =
88
          try compile (List.rev_append al tl) (Mls.find cs cases)
89
          with NonExhaustive pl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
90 91 92 93 94 95
            let rec cont acc vl pl = match vl,pl with
              | (_::vl), (p::pl) -> cont (p::acc) vl pl
              | [], pl -> pat_app cs acc ty :: pl
              | _, _ -> assert false
            in
            raise (NonExhaustive (cont [] cs.ls_args pl))
96
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
97 98
        (* how to proceed if [t] is not covered by [cases] *)
        let comp_wilds () =
99
          try compile tl wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
100 101 102
          with NonExhaustive pl ->
            let find_cs cs =
              if Mls.mem cs types then () else
103
              let tm = ty_match Mtv.empty (Opt.get cs.ls_value) ty in
Andrei Paskevich's avatar
Andrei Paskevich committed
104 105 106 107 108 109
              let wild ty = pat_wild (ty_inst tm ty) in
              let pw = pat_app cs (List.map wild cs.ls_args) ty in
              raise (NonExhaustive (pw :: pl))
            in
            Sls.iter find_cs css;
            raise (NonExhaustive (pat_wild ty :: pl))
110
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
111 112 113 114
        (* assemble the primitive case statement *)
        match t.t_node with
        | _ when Mls.is_empty types ->
            comp_wilds ()
115
        | Tapp (cs,al) when is_constr cs ->
Andrei Paskevich's avatar
Andrei Paskevich committed
116 117
            if Mls.mem cs types then comp_cases cs al else comp_wilds ()
        | _ ->
118 119 120 121 122 123 124 125
            let no_wilds =
              if bare then
                let cs,_ = Mls.choose types in
                Mls.cardinal types = cs.ls_constr
              else
                Mls.set_submap css types
            in
            let base = if no_wilds then []
126
              else [pat_wild ty, comp_wilds ()]
Andrei Paskevich's avatar
Andrei Paskevich committed
127
            in
128
            let add acc (cs,ql) =
Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131 132
              let get_vs q = create_vsymbol (id_fresh "x") q.pat_ty in
              let vl = List.rev_map get_vs ql in
              let pl = List.rev_map pat_var vl in
              let al = List.rev_map t_var vl in
133
              (pat_app cs pl ty, comp_cases cs al) :: acc
Andrei Paskevich's avatar
Andrei Paskevich committed
134
            in
135
            mk_case t (List.fold_left add base cslist)
136 137 138
  in
  compile tl rl

139 140 141
let compile_bare ~mk_case ~mk_let tl rl =
  let get_constructors _ = raise Bare in
  try compile ~get_constructors ~mk_case ~mk_let tl rl
142
  with NonExhaustive _ -> raise (NonExhaustive [])
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
143

144 145 146 147 148 149 150 151 152 153
let check_compile ~get_constructors tl = function
  | [] ->
      let pl = List.map (fun t -> pat_wild (t_type t)) tl in
      raise (NonExhaustive pl)
  | (pl::_) as ppl ->
      let mkt p = t_var (create_vsymbol (id_fresh "_") p.pat_ty) in
      let tl = if tl = [] then List.map mkt pl else tl in
      let rl = List.map (fun pl -> pl, ()) ppl in
      let mk_case _ _ = () and mk_let _ _ _ = () in
      compile ~get_constructors ~mk_case ~mk_let tl rl
154

155 156 157 158 159 160 161 162 163 164
let is_exhaustive tl = function
  | [] -> false
  | (pl::_) as ppl ->
      let mkt p = t_var (create_vsymbol (id_fresh "_") p.pat_ty) in
      let tl = if tl = [] then List.map mkt pl else tl in
      let rl = List.map (fun pl -> pl, true) ppl in
      let get_constructors _ = raise Bare in
      let mk_case _ _ = true and mk_let _ _ _ = true in
      try compile ~get_constructors ~mk_case ~mk_let tl rl
      with NonExhaustive _ -> false