src/Pure/Tools/am_compiler.ML
changeset 23174 3913451b0418
parent 23173 51179ca0c429
child 23175 267ba70e7a9d
     1.1 --- a/src/Pure/Tools/am_compiler.ML	Thu May 31 20:55:32 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,238 +0,0 @@
     1.4 -(*  Title:      Pure/Tools/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