src/HOL/Tools/function_package/pattern_split.ML
author krauss
Fri, 04 Aug 2006 18:01:45 +0200
changeset 20338 ecdfc96cf4d0
parent 20289 ba7a7c56bed5
child 20344 d02b43ea722e
permissions -rw-r--r--
Added Keywords: "otherwise" and "sequential", needed for function package's sequential mode.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     1
(*  Title:      HOL/Tools/function_package/fundef_package.ML
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     2
    ID:         $Id$
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     3
    Author:     Alexander Krauss, TU Muenchen
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     4
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     5
A package for general recursive function definitions. 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     6
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     7
Automatic splitting of overlapping constructor patterns. This is a preprocessing step which 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     8
turns a specification with overlaps into an overlap-free specification.
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
     9
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    10
*)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    11
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    12
signature FUNDEF_SPLIT = 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    13
sig
20289
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20270
diff changeset
    14
  val split_some_equations :
ba7a7c56bed5 normalized Proof.context/method type aliases;
wenzelm
parents: 20270
diff changeset
    15
    Proof.context -> (('a * ('b * bool)) * term) list -> (('a * 'b) * term list) list
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    16
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    17
end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    18
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    19
structure FundefSplit : FUNDEF_SPLIT = 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    20
struct
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    21
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    22
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    23
(* We use proof context for the variable management *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    24
(* FIXME: no __ *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    25
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    26
fun new_var ctx vs T = 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    27
    let 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    28
      val [v] = Variable.variant_frees ctx vs [("v", T)]
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    29
    in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    30
      (Free v :: vs, Free v)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    31
    end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    32
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    33
fun saturate ctx vs t =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    34
    fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t))
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    35
         (binder_types (fastype_of t)) (vs, t)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    36
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    37
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    38
(* This is copied from "fundef_datatype.ML" *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    39
fun inst_constrs_of thy (T as Type (name, _)) =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    40
	map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    41
	    (the (DatatypePackage.get_datatype_constrs thy name))
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    42
  | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    43
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    44
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    45
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    46
fun pattern_subtract_subst ctx vs _ (Free v2) = []
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    47
  | pattern_subtract_subst ctx vs (v as (Free (_, T))) t' =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    48
    let 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    49
      fun foo constr = 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    50
          let 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    51
            val (vs', t) = saturate ctx vs constr
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    52
            val substs = pattern_subtract_subst ctx vs' t t'
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    53
          in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    54
            map (cons (v, t)) substs
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    55
          end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    56
    in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    57
      flat (map foo (inst_constrs_of (ProofContext.theory_of ctx) T))
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    58
    end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    59
  | pattern_subtract_subst ctx vs t t' =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    60
    let
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    61
      val (C, ps) = strip_comb t
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    62
      val (C', qs) = strip_comb t'
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    63
    in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    64
      if C = C'
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    65
      then flat (map2 (pattern_subtract_subst ctx vs) ps qs)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    66
      else [[]]
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    67
    end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    68
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    69
fun pattern_subtract_parallel ctx vs ps qs =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    70
    flat (map2 (pattern_subtract_subst ctx vs) ps qs)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    71
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    72
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    73
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    74
(* ps - qs *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    75
fun pattern_subtract ctx eq2 eq1 =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    76
    let
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    77
      val _ $ (_ $ lhs1 $ _) = eq1
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    78
      val _ $ (_ $ lhs2 $ _) = eq2
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    79
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    80
      val thy = ProofContext.theory_of ctx
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    81
      val vs = term_frees eq1
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    82
    in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    83
      map (fn sigma => Pattern.rewrite_term thy sigma [] eq1) (pattern_subtract_subst ctx vs lhs1 lhs2)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    84
    end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    85
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    86
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    87
(* ps - p' *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    88
fun pattern_subtract_from_many ctx p'=
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    89
    flat o map (pattern_subtract ctx p')
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    90
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    91
(* in reverse order *)
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    92
fun pattern_subtract_many ctx ps' =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    93
    fold_rev (pattern_subtract_from_many ctx) ps'
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    94
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    95
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    96
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    97
fun split_all_equations ctx eqns =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    98
    let 
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
    99
      fun split_aux prev [] = []
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   100
        | split_aux prev (e::es) = pattern_subtract_many ctx prev [e] @ split_aux (e::prev) es
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   101
    in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   102
      split_aux [] eqns
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   103
end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   104
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   105
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   106
fun split_some_equations ctx eqns =
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   107
    let
20338
ecdfc96cf4d0 Added Keywords: "otherwise" and "sequential", needed for function package's
krauss
parents: 20289
diff changeset
   108
      fun split_aux prev [] = []
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   109
        | split_aux prev (((n, (att, true)), eq) :: es) = ((n, att), pattern_subtract_many ctx prev [eq])
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   110
                                                          :: split_aux (eq :: prev) es
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   111
        | split_aux prev (((n, (att, false)), eq) :: es) = ((n, att), [eq]) 
20338
ecdfc96cf4d0 Added Keywords: "otherwise" and "sequential", needed for function package's
krauss
parents: 20289
diff changeset
   112
                                                           :: split_aux (eq :: prev) es
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   113
    in
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   114
      split_aux [] eqns
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   115
    end
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   116
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff changeset
   117
end