src/Tools/Compute_Oracle/am_compiler.ML
changeset 23174 3913451b0418
child 23663 84b5c89b8b49
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Thu May 31 20:55:33 2007 +0200
     1.3 @@ -0,0 +1,238 @@
     1.4 +(*  Title:      Tools/Compute_Oracle/am_compiler.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Steven Obua
     1.7 +*)
     1.8 +
     1.9 +signature COMPILING_AM = 
    1.10 +sig
    1.11 +  include ABSTRACT_MACHINE
    1.12 +
    1.13 +  datatype closure = CVar of int | CConst of int
    1.14 +    | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
    1.15 +
    1.16 +  val set_compiled_rewriter : (term -> closure) -> unit
    1.17 +  val list_nth : 'a list * int -> 'a
    1.18 +  val list_map : ('a -> 'b) -> 'a list -> 'b list
    1.19 +end
    1.20 +
    1.21 +structure AM_Compiler : COMPILING_AM = struct
    1.22 +
    1.23 +val list_nth = List.nth;
    1.24 +val list_map = map;
    1.25 +
    1.26 +datatype term = Var of int | Const of int | App of term * term | Abs of term
    1.27 +
    1.28 +datatype pattern = PVar | PConst of int * (pattern list)
    1.29 +
    1.30 +datatype closure = CVar of int | CConst of int
    1.31 +	         | CApp of closure * closure | CAbs of closure
    1.32 +                 | Closure of (closure list) * closure
    1.33 +
    1.34 +val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
    1.35 +
    1.36 +fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
    1.37 +
    1.38 +type program = (term -> term)
    1.39 +
    1.40 +datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
    1.41 +
    1.42 +exception Compile of string;
    1.43 +exception Run of string;
    1.44 +
    1.45 +fun clos_of_term (Var x) = CVar x
    1.46 +  | clos_of_term (Const c) = CConst c
    1.47 +  | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
    1.48 +  | clos_of_term (Abs u) = CAbs (clos_of_term u)
    1.49 +
    1.50 +fun term_of_clos (CVar x) = Var x
    1.51 +  | term_of_clos (CConst c) = Const c
    1.52 +  | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
    1.53 +  | term_of_clos (CAbs u) = Abs (term_of_clos u)
    1.54 +  | term_of_clos (Closure (e, u)) =
    1.55 +      raise (Run "internal error: closure in normalized term found")
    1.56 +
    1.57 +fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
    1.58 +  | strip_closure args x = (x, args)
    1.59 +
    1.60 +(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
    1.61 +  check_freevars 0 t iff t is closed*)
    1.62 +fun check_freevars free (Var x) = x < free
    1.63 +  | check_freevars free (Const c) = true
    1.64 +  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
    1.65 +  | check_freevars free (Abs m) = check_freevars (free+1) m
    1.66 +
    1.67 +fun count_patternvars PVar = 1
    1.68 +  | count_patternvars (PConst (_, ps)) =
    1.69 +      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
    1.70 +
    1.71 +fun print_rule (p, t) = 
    1.72 +    let	
    1.73 +	fun str x = Int.toString x		    
    1.74 +	fun print_pattern n PVar = (n+1, "x"^(str n))
    1.75 +	  | print_pattern n (PConst (c, [])) = (n, "c"^(str c))
    1.76 +	  | print_pattern n (PConst (c, args)) = 
    1.77 +	    let
    1.78 +		val h = print_pattern n (PConst (c,[]))
    1.79 +	    in
    1.80 +		print_pattern_list h args
    1.81 +	    end
    1.82 +	and print_pattern_list r [] = r
    1.83 +	  | print_pattern_list (n, p) (t::ts) = 
    1.84 +	    let
    1.85 +		val (n, t) = print_pattern n t
    1.86 +	    in
    1.87 +		print_pattern_list (n, "App ("^p^", "^t^")") ts
    1.88 +	    end
    1.89 +
    1.90 +	val (n, pattern) = print_pattern 0 p
    1.91 +	val pattern =
    1.92 +            if exists_string Symbol.is_ascii_blank pattern then "(" ^ pattern ^")"
    1.93 +            else pattern
    1.94 +	
    1.95 +	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
    1.96 +              "Var " ^ str x
    1.97 +	  | print_term d (Const c) = "c" ^ str c
    1.98 +	  | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
    1.99 +	  | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
   1.100 +
   1.101 +	fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))
   1.102 +
   1.103 +	val term = print_term 0 t
   1.104 +	val term =
   1.105 +            if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
   1.106 +            else "Closure ([], "^term^")"
   1.107 +			   
   1.108 +    in
   1.109 +	"lookup stack "^pattern^" = weak stack ("^term^")"
   1.110 +    end
   1.111 +
   1.112 +fun constants_of PVar = []
   1.113 +  | constants_of (PConst (c, ps)) = c :: maps constants_of ps
   1.114 +
   1.115 +fun constants_of_term (Var _) = []
   1.116 +  | constants_of_term (Abs m) = constants_of_term m
   1.117 +  | constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b)
   1.118 +  | constants_of_term (Const c) = [c]
   1.119 +    
   1.120 +fun load_rules sname name prog = 
   1.121 +    let
   1.122 +        (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
   1.123 +	val buffer = ref ""
   1.124 +	fun write s = (buffer := (!buffer)^s)
   1.125 +	fun writeln s = (write s; write "\n")
   1.126 +	fun writelist [] = ()
   1.127 +	  | writelist (s::ss) = (writeln s; writelist ss)
   1.128 +	fun str i = Int.toString i
   1.129 +	val _ = writelist [
   1.130 +		"structure "^name^" = struct",
   1.131 +		"",
   1.132 +		"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
   1.133 +	val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
   1.134 +	val _ = map (fn x => write (" | c"^(str x))) constants
   1.135 +	val _ = writelist [
   1.136 +		"",
   1.137 +		"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",
   1.138 +		""]
   1.139 +	val _ = (case prog of
   1.140 +		    r::rs => (writeln ("fun "^(print_rule r)); 
   1.141 +			      map (fn r => writeln("  | "^(print_rule r))) rs; 
   1.142 +			      writeln ("  | lookup stack clos = weak_last stack clos"); ())								
   1.143 +		  | [] => (writeln "fun lookup stack clos = weak_last stack clos"))
   1.144 +	val _ = writelist [
   1.145 +		"and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))",
   1.146 +		"  | weak (SAppL (b, stack)) (Closure (e, Abs m)) =  weak stack (Closure (b::e, m))",
   1.147 +		"  | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos",
   1.148 +		"  | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))",
   1.149 +		"  | weak stack (Closure (e, c)) = weak stack c",
   1.150 +		"  | weak stack clos = lookup stack clos",
   1.151 +		"and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))",
   1.152 +		"  | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b",
   1.153 +		"  | weak_last stack c = (stack, c)",
   1.154 +		"",
   1.155 +		"fun lift n (v as Var m) = if m < n then v else Var (m+1)",
   1.156 +		"  | lift n (Abs t) = Abs (lift (n+1) t)",
   1.157 +		"  | lift n (App (a,b)) = App (lift n a, lift n b)",
   1.158 +		"  | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)",
   1.159 +		"  | lift n c = c",
   1.160 +		"and lift_env n e = map (lift n) e",
   1.161 +		"",
   1.162 +		"fun strong stack (Closure (e, Abs m)) = ",
   1.163 +		"    let",
   1.164 +		"      val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))",
   1.165 +		"    in",
   1.166 +		"      case stack' of",
   1.167 +		"           SEmpty => strong (SAbs stack) wnf",
   1.168 +		"         | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
   1.169 +		"    end",
   1.170 +		"  | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u",
   1.171 +		"  | strong stack clos = strong_last stack clos",
   1.172 +		"and strong_last (SAbs stack) m = strong stack (Abs m)",
   1.173 +		"  | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b",
   1.174 +		"  | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))",
   1.175 +		"  | strong_last stack clos = (stack, clos)",
   1.176 +		""]
   1.177 +	
   1.178 +	val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"						  	
   1.179 +	val _ = writelist [
   1.180 +		"fun importTerm ("^sname^".Var x) = Var x",
   1.181 +		"  | importTerm ("^sname^".Const c) =  "^ic,
   1.182 +		"  | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)",
   1.183 +		"  | importTerm ("^sname^".Abs m) = Abs (importTerm m)",
   1.184 +		""]
   1.185 +
   1.186 +	fun ec c = "  | exportTerm c"^(str c)^" = "^sname^".CConst "^(str c)
   1.187 +	val _ = writelist [
   1.188 +		"fun exportTerm (Var x) = "^sname^".CVar x",
   1.189 +		"  | exportTerm (Const c) = "^sname^".CConst c",
   1.190 +		"  | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)",
   1.191 +		"  | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)",
   1.192 +		"  | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"]
   1.193 +	val _ = writelist (map ec constants)
   1.194 +		
   1.195 +	val _ = writelist [
   1.196 +		"",
   1.197 +		"fun rewrite t = ",
   1.198 +		"    let",
   1.199 +		"      val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))",
   1.200 +		"    in",
   1.201 +		"      case stack of ",
   1.202 +		"           SEmpty => (case strong SEmpty wnf of",
   1.203 +		"                          (SEmpty, snf) => exportTerm snf",
   1.204 +		"                        | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",
   1.205 +		"         | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",
   1.206 +		"    end",
   1.207 +		"",
   1.208 +		"val _ = "^sname^".set_compiled_rewriter rewrite",
   1.209 +		"",
   1.210 +		"end;"]
   1.211 +
   1.212 +	val _ = 
   1.213 +	    let
   1.214 +		(*val fout = TextIO.openOut "gen_code.ML"
   1.215 +		val _ = TextIO.output (fout, !buffer)
   1.216 +		val _  = TextIO.closeOut fout*)
   1.217 +	    in
   1.218 +		()
   1.219 +	    end
   1.220 +    in
   1.221 +	compiled_rewriter := NONE;	
   1.222 +	use_text "" Output.ml_output false (!buffer);
   1.223 +	case !compiled_rewriter of 
   1.224 +	    NONE => raise (Compile "cannot communicate with compiled function")
   1.225 +	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
   1.226 +    end	
   1.227 +
   1.228 +fun compile eqs = 
   1.229 +    let
   1.230 +	val _ = map (fn (p, r) => 
   1.231 +                  (check_freevars (count_patternvars p) r; 
   1.232 +                   case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs
   1.233 +    in
   1.234 +	load_rules "AM_Compiler" "AM_compiled_code" eqs
   1.235 +    end	
   1.236 +
   1.237 +fun run prog t = (prog t)
   1.238 +			 	  
   1.239 +end
   1.240 +
   1.241 +structure AbstractMachine = AM_Compiler