pattern.ml 6.44 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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
        (* dispatch every case to a primitive constructor/wild case *)
        let cases,wilds =
70
          let add_case fs pl a cases =
71 72
            Mls.change fs (function
              | None -> Some [pl,a]
73 74
              | Some rl -> Some ((pl,a)::rl)) cases
          in
75
          let union_cases pl a types cases =
76 77 78 79 80
            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
81 82 83 84
          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') ->
85
                  add_case fs (List.rev_append pl' pl) a cases, wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
86 87 88 89 90 91
              | 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
92
                  union_cases pl a types cases, (pl,a)::wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
93
              | Pwild ->
94
                  union_cases pl a types cases, (pl,a)::wilds
Andrei Paskevich's avatar
Andrei Paskevich committed
95 96
          in
          List.fold_right dispatch rl (Mls.empty,[])
97
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
98 99 100
        (* 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)
101
          with NonExhaustive pl ->
Andrei Paskevich's avatar
Andrei Paskevich committed
102 103 104 105 106 107
            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))
108
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
109 110 111 112 113 114 115 116 117 118 119 120 121
        (* 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))
122
        in
Andrei Paskevich's avatar
Andrei Paskevich committed
123 124 125 126 127 128 129 130
        (* 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 =
131 132
              if Mls.submap (const3 true) css types then []
              else [mk_branch (pat_wild ty) (comp_wilds ())]
Andrei Paskevich's avatar
Andrei Paskevich committed
133 134 135 136 137 138
            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
139
              mk_branch (pat_app cs pl ty) (comp_cases cs al) :: acc
Andrei Paskevich's avatar
Andrei Paskevich committed
140 141
            in
            mk_case t (Mls.fold add types base)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142 143 144

end

145
module CompileTerm  = Compile (struct
146
  type action = term
147 148 149 150
  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
151 152
end)

153
module CompileFmla  = Compile (struct
154
  type action = fmla
155 156 157 158
  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
159 160
end)