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