src/HOL/Tools/function_package/pattern_split.ML
author krauss
Wed Sep 20 09:08:35 2006 +0200 (2006-09-20)
changeset 20636 ddddf0b7d322
parent 20523 36a59e5d0039
child 20654 d80502f0d701
permissions -rw-r--r--
Fixed error in pattern splitting algorithm
     1 (*  Title:      HOL/Tools/function_package/fundef_package.ML
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 A package for general recursive function definitions.
     6 
     7 Automatic splitting of overlapping constructor patterns. This is a preprocessing step which
     8 turns a specification with overlaps into an overlap-free specification.
     9 
    10 *)
    11 
    12 signature FUNDEF_SPLIT =
    13 sig
    14   val split_some_equations :
    15     Proof.context -> (bool * term) list -> term list list
    16 
    17   val split_all_equations :
    18     Proof.context -> term list -> term list list
    19 end
    20 
    21 structure FundefSplit : FUNDEF_SPLIT =
    22 struct
    23 
    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) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
    43             (the (DatatypePackage.get_datatype_constrs thy name))
    44   | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
    45 
    46 
    47 
    48 
    49 fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
    50 fun join_product (xs, ys) = map join (product xs ys)
    51 
    52 fun join_list [] = []
    53   | join_list xs = foldr1 (join_product) xs
    54 
    55 
    56 exception DISJ
    57 
    58 fun pattern_subtract_subst ctx vs t t' =
    59     let
    60       exception DISJ
    61       fun pattern_subtract_subst_aux vs _ (Free v2) = []
    62         | pattern_subtract_subst_aux vs (v as (Free (_, T))) t' =
    63           let
    64             fun foo constr =
    65                 let
    66                   val (vs', t) = saturate ctx vs constr
    67                   val substs = pattern_subtract_subst ctx vs' t t'
    68                 in
    69                   map (fn (vs, subst) => (vs, (v,t)::subst)) substs
    70                 end
    71           in
    72             flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
    73           end
    74         | pattern_subtract_subst_aux vs t t' =
    75           let
    76             val (C, ps) = strip_comb t
    77             val (C', qs) = strip_comb t'
    78           in
    79             if C = C'
    80             then flat (map2 (pattern_subtract_subst_aux vs) ps qs)
    81             else raise DISJ
    82           end
    83     in
    84       pattern_subtract_subst_aux vs t t'
    85       handle DISJ => [(vs, [])]
    86     end
    87 
    88 
    89 (* p - q *)
    90 fun pattern_subtract ctx eq2 eq1 =
    91     let
    92       val thy = ProofContext.theory_of ctx
    93       
    94       val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1
    95       val (_,  _ $ (_ $ lhs2 $ _)) = dest_all_all eq2
    96 
    97       val _ = print (cterm_of thy eq1)
    98       val _ = print (cterm_of thy eq2)
    99 
   100       val substs = pattern_subtract_subst ctx vs lhs1 lhs2
   101 
   102       fun instantiate (vs', sigma) =
   103           let
   104             val t = Pattern.rewrite_term thy sigma [] feq1
   105           in
   106             fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
   107           end
   108 
   109       fun prtrm t = let val _ = print (map (cterm_of thy) t) in t end
   110     in
   111       prtrm (map instantiate substs)
   112     end
   113 
   114 
   115 (* ps - p' *)
   116 fun pattern_subtract_from_many ctx p'=
   117     flat o map (pattern_subtract ctx p')
   118 
   119 (* in reverse order *)
   120 fun pattern_subtract_many ctx ps' =
   121     fold_rev (pattern_subtract_from_many ctx) ps'
   122 
   123 
   124 
   125 fun split_some_equations ctx eqns =
   126     let
   127       fun split_aux prev [] = []
   128         | split_aux prev ((true, eq) :: es) = pattern_subtract_many ctx prev [eq]
   129                                               :: split_aux (eq :: prev) es
   130         | split_aux prev ((false, eq) :: es) = [eq]
   131                                                :: split_aux (eq :: prev) es
   132     in
   133       split_aux [] eqns
   134     end
   135 
   136 fun split_all_equations ctx =
   137     split_some_equations ctx o map (pair true)
   138 
   139 
   140 
   141 
   142 end