pattern.ml 6.32 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
module type Action = sig
  type action
27
  type branch
28
  val mk_let : vsymbol -> term -> action -> action
29 30
  val mk_branch : pattern -> action -> branch
  val mk_case : term -> branch list -> action
31
end
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
32

33
exception ConstructorExpected of lsymbol
34
exception NonExhaustive of pattern list
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
35

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

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

end

142
module CompileTerm  = Compile (struct
143
  type action = term
144 145 146 147
  type branch = term_branch
  let mk_let v s t  = t_let_close v s t
  let mk_branch p t = t_close_branch p t
  let mk_case t bl  = t_case t bl
148 149
end)

150
module CompileFmla  = Compile (struct
151
  type action = fmla
152 153 154 155
  type branch = fmla_branch
  let mk_let v t f  = f_let_close v t f
  let mk_branch p f = f_close_branch p f
  let mk_case t bl  = f_case t bl
156 157
end)