pattern.ml 5.23 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Util
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
21 22 23 24
open Ident
open Ty
open Term

25 26 27 28 29
module type Action = sig
  type action
  val mk_let : vsymbol -> term -> action -> action
  val mk_case : term -> (pattern * action) list -> action
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30

31
exception NonExhaustive of pattern list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32

33 34
module Compile (X : Action) = struct
  open X
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
35

36
  let rec compile css tl rl = match tl,rl with
37 38
    | _, [] -> (* no actions *)
        let pl = List.map (fun t -> pat_wild t.t_ty) tl in
39
        raise (NonExhaustive pl)
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 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
    | [], (_,a) :: _ -> (* no terms, at least one action *)
        a
    | t :: tl, _ -> (* process the leftmost column *)
        (* map constructors to argument types *)
        let rec populate types p = match p.pat_node with
          | Pwild | Pvar _ -> types
          | Pas (p,_) -> populate types p
          | Papp (fs,pl) -> Mls.add fs pl types
        in
        let populate types (pl,_) = populate types (List.hd pl) in
        let types = List.fold_left populate Mls.empty rl in
        (* map constructors to subordinate matrices *)
        let add_case fs pl a cases =
          let rl = try Mls.find fs cases with Not_found -> [] in
          Mls.add fs ((pl,a)::rl) cases
        in
        let add_wild pl a fs ql cases =
          let add pl q = pat_wild q.pat_ty :: pl in
          add_case fs (List.fold_left add pl ql) a cases
        in
        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') ->
                add_case fs (List.rev_append pl' 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
                Mls.fold (add_wild pl a) types cases, (pl,a)::wilds
            | Pwild ->
                Mls.fold (add_wild pl a) types cases, (pl,a)::wilds
        in
        let cases,wilds = List.fold_right dispatch rl (Mls.empty,[]) in
        (* assemble the primitive case statement *)
        let ty = t.t_ty in
        let pw = pat_wild ty in
        let exhaustive, nopat = match ty.ty_node with
          | Tyapp (ts,_) ->
              begin match css ts with
              | [] -> false, pw
              | cl ->
                  let test cs = not (Mls.mem cs types) in
                  begin match List.filter test cl with
                  | cs :: _ ->
                      (* FIXME? specialize types to t.t_ty *)
                      let pl = List.map pat_wild cs.ls_args in
                      false, pat_app cs pl (of_option cs.ls_value)
                  | _ -> true, pw
                  end
              end
          | Tyvar _ -> false, pw
        in
        let base = if exhaustive then [] else
94 95
          try [pw, compile css tl wilds]
          with NonExhaustive pl -> raise (NonExhaustive (nopat::pl))
96 97 98 99 100 101
        in
        let add fs ql acc =
          let id = id_fresh "x" in
          let vl = List.map (fun q -> create_vsymbol id q.pat_ty) ql in
          let tl = List.fold_left (fun tl v -> t_var v :: tl) tl vl in
          let pat = pat_app fs (List.map pat_var vl) ty in
102 103 104
          let rec pat_cont acc vl pl = match vl,pl with
            | (_::vl), (p::pl) -> pat_cont (p::acc) vl pl
            | [], pl -> pat_app fs acc ty :: pl
105 106
            | _, _ -> assert false
          in
107 108
          try (pat, compile css tl (Mls.find fs cases)) :: acc
          with NonExhaustive pl -> raise (NonExhaustive (pat_cont [] vl pl))
109 110 111 112
        in
        match Mls.fold add types base with
        | [{ pat_node = Pwild }, a] -> a
        | bl -> mk_case t bl
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
113 114 115

end

116 117 118 119 120 121 122 123 124 125 126 127 128 129 130
module CompileTerm = Compile (struct
  type action = term
  let mk_let v s t = t_let v s t
  let mk_case t bl =
    let ty = (snd (List.hd bl)).t_ty in
    t_case [t] (List.map (fun (p,a) -> [p],a) bl) ty
end)

module CompileFmla = Compile (struct
  type action = fmla
  let mk_let v t f = f_let v t f
  let mk_case t bl =
    f_case [t] (List.map (fun (p,a) -> [p],a) bl)
end)