src/HOL/Matrix/codegen_prep.ML
changeset 15178 5f621aa35c25
child 15531 08c8dad8e399
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Matrix/codegen_prep.ML	Fri Sep 03 17:10:36 2004 +0200
     1.3 @@ -0,0 +1,110 @@
     1.4 +structure codegen_prep = 
     1.5 +struct
     1.6 +
     1.7 +exception Prepare_thms of string;
     1.8 +
     1.9 +fun is_meta_eq th =
    1.10 +    let
    1.11 +	fun check ((Const ("==", _)) $ _ $ _) = true
    1.12 +	  | check _ = false
    1.13 +    in
    1.14 +	check (concl_of th)
    1.15 +    end
    1.16 +
    1.17 +fun printty ty = 
    1.18 +    let
    1.19 +	fun immerse s [] = []
    1.20 +	  | immerse s [x] = [x]
    1.21 +	  | immerse s (x::xs) = x::s::(immerse s xs)
    1.22 +
    1.23 +	fun py t = 
    1.24 +	    let
    1.25 +		val (name, args) =  dest_Type t
    1.26 +		val args' = map printty args
    1.27 +	    in
    1.28 +		concat (immerse "_" (name::args'))
    1.29 +	    end
    1.30 +
    1.31 +	val (args, res) = strip_type ty
    1.32 +	val tystrs = map py (args@[res])
    1.33 +			  
    1.34 +	val s = "'"^(concat (immerse "_" tystrs))^"'"
    1.35 +    in
    1.36 +	s
    1.37 +    end
    1.38 +
    1.39 +fun head_name th = 
    1.40 +    let val s = 
    1.41 +	    let
    1.42 +		val h = fst (strip_comb (hd (snd (strip_comb (concl_of th)))))
    1.43 +		val n = fst (dest_Const h)
    1.44 +		val ty = snd (dest_Const h)
    1.45 +		val hn = fst (dest_Const h)
    1.46 +	    in
    1.47 +		hn^"_"^(printty ty) handle _ => (writeln ("warning: polymorphic "^hn); hn)	
    1.48 +	    end
    1.49 +    in
    1.50 +	s
    1.51 +    end
    1.52 +	    
    1.53 +val mangle_id  = 
    1.54 +    let
    1.55 +	fun tr #"=" = "_eq_"
    1.56 +	  | tr #"." = "_"
    1.57 +	  | tr #" " = "_"
    1.58 +	  | tr #"<" = "_le_"
    1.59 +	  | tr #">" = "_ge_"
    1.60 +	  | tr #"(" = "_bro_"
    1.61 +	  | tr #")" = "_brc_"
    1.62 +	  | tr #"+" = "_plus_"
    1.63 +	  | tr #"*" = "_mult_"
    1.64 +	  | tr #"-" = "_minus_"
    1.65 +	  | tr #"|" = "_or_"
    1.66 +	  | tr #"&" = "_and_"
    1.67 +	  | tr x = Char.toString x
    1.68 +	fun m s = "simp_"^(String.translate tr s)
    1.69 +    in
    1.70 +	m
    1.71 +    end
    1.72 +
    1.73 +fun group f [] = []
    1.74 +  | group f (x::xs) = 
    1.75 +    let
    1.76 +	val g = group f xs
    1.77 +	val key = f x
    1.78 +    in
    1.79 +	case assoc (g, key) of
    1.80 +	    None => (key, [x])::g
    1.81 +	  | Some l => overwrite (g, (key, x::l))
    1.82 +    end
    1.83 +    
    1.84 +fun prepare_thms ths = 
    1.85 +    let
    1.86 +	val ths = (filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (filter (not o is_meta_eq) ths))		      
    1.87 +	val _ = if forall Thm.no_prems ths then () else raise (Prepare_thms "premisse found")
    1.88 +	val thmgroups = group head_name ths
    1.89 +	val test_clashgroups = group (fn (a,b) => mangle_id a) thmgroups
    1.90 +	val _ = if (length thmgroups <> length test_clashgroups) then raise (Prepare_thms "clash after name mangling") else ()	
    1.91 +		
    1.92 +	fun prep (name, ths) = 
    1.93 +	    let
    1.94 +		val m = mangle_id name
    1.95 +			
    1.96 +	    in
    1.97 +		(m, true, ths)
    1.98 +	    end
    1.99 +	    
   1.100 +	val thmgroups = map prep thmgroups
   1.101 +    in
   1.102 +	(thmgroups)
   1.103 +    end
   1.104 +    
   1.105 +fun writestr filename s = 
   1.106 +    let 
   1.107 +	val f = TextIO.openOut filename
   1.108 +	val _ = TextIO.output(f, s)
   1.109 +	val _ = TextIO.closeOut f
   1.110 +    in 
   1.111 +	() 
   1.112 +    end
   1.113 +end