src/HOL/Tools/Function/pattern_split.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32952 aeb1e44fbc19
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      HOL/Tools/Function/pattern_split.ML
     2     Author:     Alexander Krauss, TU Muenchen
     3 
     4 A package for general recursive function definitions.
     5 
     6 Automatic splitting of overlapping constructor patterns. This is a preprocessing step which
     7 turns a specification with overlaps into an overlap-free specification.
     8 
     9 *)
    10 
    11 signature FUNDEF_SPLIT =
    12 sig
    13   val split_some_equations :
    14       Proof.context -> (bool * term) list -> term list list
    15 
    16   val split_all_equations :
    17       Proof.context -> term list -> term list list
    18 end
    19 
    20 structure FundefSplit : FUNDEF_SPLIT =
    21 struct
    22 
    23 open FundefLib
    24 
    25 (* We use proof context for the variable management *)
    26 (* FIXME: no __ *)
    27 
    28 fun new_var ctx vs T =
    29     let
    30       val [v] = Variable.variant_frees ctx vs [("v", T)]
    31     in
    32       (Free v :: vs, Free v)
    33     end
    34 
    35 fun saturate ctx vs t =
    36     fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
    37          (binder_types (fastype_of t)) (vs, t)
    38          
    39          
    40 (* This is copied from "fundef_datatype.ML" *)
    41 fun inst_constrs_of thy (T as Type (name, _)) =
    42     map (fn (Cn,CT) =>
    43           Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    44         (the (Datatype.get_constrs thy name))
    45   | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])
    46                             
    47                             
    48                             
    49 
    50 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
    51 fun join_product (xs, ys) = map_product (curry join) xs ys
    52 
    53 fun join_list [] = []
    54   | join_list xs = foldr1 (join_product) xs
    55 
    56 
    57 exception DISJ
    58 
    59 fun pattern_subtract_subst ctx vs t t' =
    60     let
    61       exception DISJ
    62       fun pattern_subtract_subst_aux vs _ (Free v2) = []
    63         | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
    64           let
    65             fun foo constr =
    66                 let
    67                   val (vs', t) = saturate ctx vs constr
    68                   val substs = pattern_subtract_subst ctx vs' t t'
    69                 in
    70                   map (fn (vs, subst) => (vs, (v,t)::subst)) substs
    71                 end
    72           in
    73             maps foo (inst_constrs_of (ProofContext.theory_of ctx) T)
    74           end
    75         | pattern_subtract_subst_aux vs t t' =
    76           let
    77             val (C, ps) = strip_comb t
    78             val (C', qs) = strip_comb t'
    79           in
    80             if C = C'
    81             then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
    82             else raise DISJ
    83           end
    84     in
    85       pattern_subtract_subst_aux vs t t'
    86       handle DISJ => [(vs, [])]
    87     end
    88 
    89 
    90 (* p - q *)
    91 fun pattern_subtract ctx eq2 eq1 =
    92     let
    93       val thy = ProofContext.theory_of ctx
    94                 
    95       val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
    96       val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
    97                                      
    98       val substs = pattern_subtract_subst ctx vs lhs1 lhs2
    99                    
   100       fun instantiate (vs', sigma) =
   101           let
   102             val t = Pattern.rewrite_term thy sigma [] feq1
   103           in
   104             fold_rev Logic.all (gen_inter (op =) (map Free (frees_in_term ctx t), vs')) t
   105           end
   106     in
   107       map instantiate substs
   108     end
   109       
   110 
   111 (* ps - p' *)
   112 fun pattern_subtract_from_many ctx p'=
   113     maps (pattern_subtract ctx p')
   114 
   115 (* in reverse order *)
   116 fun pattern_subtract_many ctx ps' =
   117     fold_rev (pattern_subtract_from_many ctx) ps'
   118 
   119 
   120 
   121 fun split_some_equations ctx eqns =
   122     let
   123       fun split_aux prev [] = []
   124         | split_aux prev ((true, eq) :: es) = pattern_subtract_many ctx prev [eq]
   125                                               :: split_aux (eq :: prev) es
   126         | split_aux prev ((false, eq) :: es) = [eq]
   127                                                :: split_aux (eq :: prev) es
   128     in
   129       split_aux [] eqns
   130     end
   131     
   132 fun split_all_equations ctx =
   133     split_some_equations ctx o map (pair true)
   134 
   135 
   136 
   137 
   138 end