pattern.ml 6.15 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 ConstructorExpected of lsymbol
32
exception NonExhaustive of pattern list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33

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

37
  let rec compile constructors tl rl = match tl,rl with
38 39
    | _, [] -> (* no actions *)
        let pl = List.map (fun t -> pat_wild t.t_ty) tl in
40
        raise (NonExhaustive pl)
41 42 43
    | [], (_,a) :: _ -> (* no terms, at least one action *)
        a
    | t :: tl, _ -> (* process the leftmost column *)
44 45 46 47 48 49 50 51
        (* extract the set of constructors *)
        let ty = t.t_ty in
        let css = match ty.ty_node with
          | Tyapp (ts,_) ->
              let s_add s cs = Sls.add cs s in
              List.fold_left s_add Sls.empty (constructors ts)
          | Tyvar _ -> Sls.empty
        in
52 53 54 55
        (* map constructors to argument types *)
        let rec populate types p = match p.pat_node with
          | Pwild | Pvar _ -> types
          | Pas (p,_) -> populate types p
Andrei Paskevich's avatar
Andrei Paskevich committed
56
          | Por (p,q) -> populate (populate types p) q
57 58 59
          | Papp (fs,pl) ->
              if Sls.mem fs css then Mls.add fs pl types
              else raise (ConstructorExpected fs)
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
        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
Andrei Paskevich's avatar
Andrei Paskevich committed
77 78
            | Por (p,q) ->
                dispatch (p::pl, a) (dispatch (q::pl, a) (cases,wilds))
79 80 81 82 83 84 85 86 87 88
            | 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 *)
89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
        let pat_cont cs vl pl =
          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
          cont [] vl pl
        in
    match t.t_node with
    | Tapp (cs,al) when Sls.mem cs css ->
        if Mls.mem cs cases then
          let tl = List.rev_append al tl in
          try compile constructors tl (Mls.find cs cases)
          with NonExhaustive pl -> raise (NonExhaustive (pat_cont cs al pl))
        else begin
          try compile constructors tl wilds
          with NonExhaustive pl ->
106 107
            let al = List.map (fun t -> pat_wild t.t_ty) al in
            raise (NonExhaustive (pat_app cs al ty :: pl))
108 109
        end
    | _ -> begin
110
        let pw = pat_wild ty in
111 112 113 114 115 116
        let nopat =
          if Sls.is_empty css then Some pw else
          let test cs = not (Mls.mem cs types) in
          let unused = Sls.filter test css in
          if Sls.is_empty unused then None else
          let cs = Sls.choose unused in
117 118 119
          let tm = ty_match Mtv.empty (of_option cs.ls_value) ty in
          let wild ty = pat_wild (ty_inst tm ty) in
          Some (pat_app cs (List.map wild cs.ls_args) ty)
120
        in
121 122 123 124 125
        let base = match nopat with
          | None -> []
          | Some pat ->
              (try [pw, compile constructors tl wilds]
              with NonExhaustive pl -> raise (NonExhaustive (pat::pl)))
126 127 128 129 130 131
        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
132
          try (pat, compile constructors tl (Mls.find fs cases)) :: acc
133
          with NonExhaustive pl -> raise (NonExhaustive (pat_cont fs vl pl))
134 135 136 137
        in
        match Mls.fold add types base with
        | [{ pat_node = Pwild }, a] -> a
        | bl -> mk_case t bl
138
    end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139 140 141

end

142 143 144
module CompileTerm = Compile (struct
  type action = term
  let mk_let v s t = t_let v s t
Andrei Paskevich's avatar
Andrei Paskevich committed
145
  let mk_case t bl = t_case t bl (snd (List.hd bl)).t_ty
146 147 148 149 150
end)

module CompileFmla = Compile (struct
  type action = fmla
  let mk_let v t f = f_let v t f
Andrei Paskevich's avatar
Andrei Paskevich committed
151
  let mk_case t bl = f_case t bl
152 153
end)