src/HOL/Matrix/codegen_prep.ML
author obua
Fri Sep 03 17:10:36 2004 +0200 (2004-09-03)
changeset 15178 5f621aa35c25
child 15531 08c8dad8e399
permissions -rw-r--r--
Matrix theory, linear programming
obua@15178
     1
structure codegen_prep = 
obua@15178
     2
struct
obua@15178
     3
obua@15178
     4
exception Prepare_thms of string;
obua@15178
     5
obua@15178
     6
fun is_meta_eq th =
obua@15178
     7
    let
obua@15178
     8
	fun check ((Const ("==", _)) $ _ $ _) = true
obua@15178
     9
	  | check _ = false
obua@15178
    10
    in
obua@15178
    11
	check (concl_of th)
obua@15178
    12
    end
obua@15178
    13
obua@15178
    14
fun printty ty = 
obua@15178
    15
    let
obua@15178
    16
	fun immerse s [] = []
obua@15178
    17
	  | immerse s [x] = [x]
obua@15178
    18
	  | immerse s (x::xs) = x::s::(immerse s xs)
obua@15178
    19
obua@15178
    20
	fun py t = 
obua@15178
    21
	    let
obua@15178
    22
		val (name, args) =  dest_Type t
obua@15178
    23
		val args' = map printty args
obua@15178
    24
	    in
obua@15178
    25
		concat (immerse "_" (name::args'))
obua@15178
    26
	    end
obua@15178
    27
obua@15178
    28
	val (args, res) = strip_type ty
obua@15178
    29
	val tystrs = map py (args@[res])
obua@15178
    30
			  
obua@15178
    31
	val s = "'"^(concat (immerse "_" tystrs))^"'"
obua@15178
    32
    in
obua@15178
    33
	s
obua@15178
    34
    end
obua@15178
    35
obua@15178
    36
fun head_name th = 
obua@15178
    37
    let val s = 
obua@15178
    38
	    let
obua@15178
    39
		val h = fst (strip_comb (hd (snd (strip_comb (concl_of th)))))
obua@15178
    40
		val n = fst (dest_Const h)
obua@15178
    41
		val ty = snd (dest_Const h)
obua@15178
    42
		val hn = fst (dest_Const h)
obua@15178
    43
	    in
obua@15178
    44
		hn^"_"^(printty ty) handle _ => (writeln ("warning: polymorphic "^hn); hn)	
obua@15178
    45
	    end
obua@15178
    46
    in
obua@15178
    47
	s
obua@15178
    48
    end
obua@15178
    49
	    
obua@15178
    50
val mangle_id  = 
obua@15178
    51
    let
obua@15178
    52
	fun tr #"=" = "_eq_"
obua@15178
    53
	  | tr #"." = "_"
obua@15178
    54
	  | tr #" " = "_"
obua@15178
    55
	  | tr #"<" = "_le_"
obua@15178
    56
	  | tr #">" = "_ge_"
obua@15178
    57
	  | tr #"(" = "_bro_"
obua@15178
    58
	  | tr #")" = "_brc_"
obua@15178
    59
	  | tr #"+" = "_plus_"
obua@15178
    60
	  | tr #"*" = "_mult_"
obua@15178
    61
	  | tr #"-" = "_minus_"
obua@15178
    62
	  | tr #"|" = "_or_"
obua@15178
    63
	  | tr #"&" = "_and_"
obua@15178
    64
	  | tr x = Char.toString x
obua@15178
    65
	fun m s = "simp_"^(String.translate tr s)
obua@15178
    66
    in
obua@15178
    67
	m
obua@15178
    68
    end
obua@15178
    69
obua@15178
    70
fun group f [] = []
obua@15178
    71
  | group f (x::xs) = 
obua@15178
    72
    let
obua@15178
    73
	val g = group f xs
obua@15178
    74
	val key = f x
obua@15178
    75
    in
obua@15178
    76
	case assoc (g, key) of
obua@15178
    77
	    None => (key, [x])::g
obua@15178
    78
	  | Some l => overwrite (g, (key, x::l))
obua@15178
    79
    end
obua@15178
    80
    
obua@15178
    81
fun prepare_thms ths = 
obua@15178
    82
    let
obua@15178
    83
	val ths = (filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (filter (not o is_meta_eq) ths))		      
obua@15178
    84
	val _ = if forall Thm.no_prems ths then () else raise (Prepare_thms "premisse found")
obua@15178
    85
	val thmgroups = group head_name ths
obua@15178
    86
	val test_clashgroups = group (fn (a,b) => mangle_id a) thmgroups
obua@15178
    87
	val _ = if (length thmgroups <> length test_clashgroups) then raise (Prepare_thms "clash after name mangling") else ()	
obua@15178
    88
		
obua@15178
    89
	fun prep (name, ths) = 
obua@15178
    90
	    let
obua@15178
    91
		val m = mangle_id name
obua@15178
    92
			
obua@15178
    93
	    in
obua@15178
    94
		(m, true, ths)
obua@15178
    95
	    end
obua@15178
    96
	    
obua@15178
    97
	val thmgroups = map prep thmgroups
obua@15178
    98
    in
obua@15178
    99
	(thmgroups)
obua@15178
   100
    end
obua@15178
   101
    
obua@15178
   102
fun writestr filename s = 
obua@15178
   103
    let 
obua@15178
   104
	val f = TextIO.openOut filename
obua@15178
   105
	val _ = TextIO.output(f, s)
obua@15178
   106
	val _ = TextIO.closeOut f
obua@15178
   107
    in 
obua@15178
   108
	() 
obua@15178
   109
    end
obua@15178
   110
end