src/HOL/Tools/function_package/sum_tools.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 19770 be5c23ebe1eb
child 20523 36a59e5d0039
permissions -rw-r--r--
adding case theorems for code generator
krauss@19770
     1
(*  Title:      HOL/Tools/function_package/sum_tools.ML
krauss@19770
     2
    ID:         $Id$
krauss@19770
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@19770
     4
krauss@19770
     5
A package for general recursive function definitions. 
krauss@19770
     6
Tools for mutual recursive definitions. This could actually be useful for other packages, too, but needs
krauss@19770
     7
some cleanup first...
krauss@19770
     8
krauss@19770
     9
*)
krauss@19770
    10
krauss@19770
    11
signature SUM_TOOLS =
krauss@19770
    12
sig
krauss@19770
    13
  type sum_tree
krauss@19770
    14
  type sum_path
krauss@19770
    15
krauss@19770
    16
  val projl_inl: thm
krauss@19770
    17
  val projr_inr: thm
krauss@19770
    18
krauss@19770
    19
  val mk_tree : typ list -> typ * sum_tree * sum_path list
krauss@19770
    20
krauss@19770
    21
  val mk_proj: sum_tree -> sum_path -> term -> term
krauss@19770
    22
  val mk_inj: sum_tree -> sum_path -> term -> term
krauss@19770
    23
krauss@19770
    24
  val mk_sumcases: sum_tree -> typ -> term list -> term
krauss@19770
    25
end
krauss@19770
    26
krauss@19770
    27
krauss@19770
    28
structure SumTools: SUM_TOOLS =
krauss@19770
    29
struct
krauss@19770
    30
krauss@19770
    31
val inlN = "Sum_Type.Inl"
krauss@19770
    32
val inrN = "Sum_Type.Inr"
krauss@19770
    33
val sumcaseN = "Datatype.sum.sum_case"
krauss@19770
    34
krauss@19770
    35
val projlN = "FunDef.lproj"
krauss@19770
    36
val projrN = "FunDef.rproj"
krauss@19770
    37
val projl_inl = thm "FunDef.lproj_inl"
krauss@19770
    38
val projr_inr = thm "FunDef.rproj_inr"
krauss@19770
    39
krauss@19770
    40
krauss@19770
    41
krauss@19770
    42
fun mk_sumT LT RT = Type ("+", [LT, RT])
krauss@19770
    43
fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
krauss@19770
    44
krauss@19770
    45
krauss@19770
    46
datatype sum_tree 
krauss@19770
    47
  = Leaf of typ
krauss@19770
    48
  | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
krauss@19770
    49
krauss@19770
    50
type sum_path = bool list (* true: left, false: right *)
krauss@19770
    51
krauss@19770
    52
fun sum_type_of (Leaf T) = T
krauss@19770
    53
  | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST
krauss@19770
    54
krauss@19770
    55
krauss@19770
    56
fun mk_tree Ts =
krauss@19770
    57
    let 
krauss@19770
    58
	fun mk_tree' 1 [T] = (T, Leaf T, [[]])
krauss@19770
    59
	  | mk_tree' n Ts =
krauss@19770
    60
	    let 
krauss@19770
    61
		val n2 = n div 2
krauss@19770
    62
		val (lTs, rTs) = chop n2 Ts
krauss@19770
    63
		val (TL, ltree, lpaths) = mk_tree' n2 lTs
krauss@19770
    64
		val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs
krauss@19770
    65
		val T = mk_sumT TL TR
krauss@19770
    66
		val pths = map (cons true) lpaths @ map (cons false) rpaths 
krauss@19770
    67
	    in
krauss@19770
    68
		(T, Branch (T, (TL, ltree), (TR, rtree)), pths)
krauss@19770
    69
	    end
krauss@19770
    70
    in
krauss@19770
    71
	mk_tree' (length Ts) Ts
krauss@19770
    72
    end
krauss@19770
    73
krauss@19770
    74
krauss@19770
    75
fun mk_inj (Leaf _) [] t = t
krauss@19770
    76
  | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = 
krauss@19770
    77
    Const (inlN, LT --> ST) $ mk_inj tr pth t
krauss@19770
    78
  | mk_inj (Branch (ST, _, (RT, tr))) (false::pth) t = 
krauss@19770
    79
    Const (inrN, RT --> ST) $ mk_inj tr pth t
krauss@19770
    80
  | mk_inj _ _ _ = sys_error "mk_inj"
krauss@19770
    81
krauss@19770
    82
fun mk_proj (Leaf _) [] t = t
krauss@19770
    83
  | mk_proj (Branch (ST, (LT, tr), _)) (true::pth) t = 
krauss@19770
    84
    mk_proj tr pth (Const (projlN, ST --> LT) $ t)
krauss@19770
    85
  | mk_proj (Branch (ST, _, (RT, tr))) (false::pth) t = 
krauss@19770
    86
    mk_proj tr pth (Const (projrN, ST --> RT) $ t)
krauss@19770
    87
  | mk_proj _ _ _ = sys_error "mk_proj"
krauss@19770
    88
krauss@19770
    89
krauss@19770
    90
fun mk_sumcases tree T ts =
krauss@19770
    91
    let
krauss@19770
    92
	fun mk_sumcases' (Leaf _) (t::ts) = (t,ts)
krauss@19770
    93
	  | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts =
krauss@19770
    94
	    let
krauss@19770
    95
		val (lcase, ts') = mk_sumcases' ltr ts
krauss@19770
    96
		val (rcase, ts'') = mk_sumcases' rtr ts'
krauss@19770
    97
	    in
krauss@19770
    98
		(mk_sumcase LT RT T lcase rcase, ts'')
krauss@19770
    99
	    end
krauss@19770
   100
	  | mk_sumcases' _ [] = sys_error "mk_sumcases"
krauss@19770
   101
    in
krauss@19770
   102
	fst (mk_sumcases' tree ts)
krauss@19770
   103
    end
krauss@19770
   104
krauss@19770
   105
end
krauss@19770
   106
krauss@19770
   107
krauss@19770
   108
krauss@19770
   109