src/Pure/Tools/am_compiler.ML
author wenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14)
changeset 16842 5979c46853d1
parent 16782 b214f21ae396
child 17795 5b18c3343028
permissions -rw-r--r--
tuned;
obua@16781
     1
(*  Title:      Pure/Tools/am_compiler.ML
obua@16781
     2
    ID:         $Id$
obua@16781
     3
    Author:     Steven Obua
obua@16781
     4
*)
obua@16781
     5
obua@16781
     6
signature COMPILING_AM = 
obua@16781
     7
sig
wenzelm@16842
     8
  include ABSTRACT_MACHINE
obua@16781
     9
wenzelm@16842
    10
  datatype closure = CVar of int | CConst of int
wenzelm@16842
    11
    | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
obua@16781
    12
wenzelm@16842
    13
  val set_compiled_rewriter : (term -> closure) -> unit
wenzelm@16842
    14
  val list_nth : 'a list * int -> 'a
wenzelm@16842
    15
  val list_map : ('a -> 'b) -> 'a list -> 'b list
obua@16781
    16
end
obua@16781
    17
obua@16781
    18
structure AM_Compiler :> COMPILING_AM = struct
obua@16781
    19
obua@16782
    20
val list_nth = List.nth;
obua@16782
    21
val list_map = map;
obua@16782
    22
obua@16781
    23
datatype term = Var of int | Const of int | App of term * term | Abs of term
obua@16781
    24
obua@16781
    25
datatype pattern = PVar | PConst of int * (pattern list)
obua@16781
    26
obua@16781
    27
datatype closure = CVar of int | CConst of int
wenzelm@16842
    28
	         | CApp of closure * closure | CAbs of closure
wenzelm@16842
    29
                 | Closure of (closure list) * closure
obua@16781
    30
obua@16781
    31
val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
obua@16781
    32
obua@16781
    33
fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
obua@16781
    34
obua@16781
    35
type program = (term -> term)
obua@16781
    36
obua@16781
    37
datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
obua@16781
    38
obua@16781
    39
exception Compile of string;
obua@16781
    40
exception Run of string;
obua@16781
    41
obua@16781
    42
fun clos_of_term (Var x) = CVar x
obua@16781
    43
  | clos_of_term (Const c) = CConst c
obua@16781
    44
  | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
obua@16781
    45
  | clos_of_term (Abs u) = CAbs (clos_of_term u)
obua@16781
    46
obua@16781
    47
fun term_of_clos (CVar x) = Var x
obua@16781
    48
  | term_of_clos (CConst c) = Const c
obua@16781
    49
  | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
obua@16781
    50
  | term_of_clos (CAbs u) = Abs (term_of_clos u)
wenzelm@16842
    51
  | term_of_clos (Closure (e, u)) =
wenzelm@16842
    52
      raise (Run "internal error: closure in normalized term found")
obua@16781
    53
obua@16781
    54
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
obua@16781
    55
  | strip_closure args x = (x, args)
obua@16781
    56
wenzelm@16842
    57
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
wenzelm@16842
    58
  check_freevars 0 t iff t is closed*)
obua@16781
    59
fun check_freevars free (Var x) = x < free
obua@16781
    60
  | check_freevars free (Const c) = true
obua@16781
    61
  | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
obua@16781
    62
  | check_freevars free (Abs m) = check_freevars (free+1) m
obua@16781
    63
obua@16781
    64
fun count_patternvars PVar = 1
wenzelm@16842
    65
  | count_patternvars (PConst (_, ps)) =
wenzelm@16842
    66
      List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
obua@16781
    67
obua@16781
    68
fun print_rule (p, t) = 
obua@16781
    69
    let	
obua@16781
    70
	fun str x = Int.toString x		    
obua@16781
    71
	fun print_pattern n PVar = (n+1, "x"^(str n))
obua@16781
    72
	  | print_pattern n (PConst (c, [])) = (n, "c"^(str c))
obua@16781
    73
	  | print_pattern n (PConst (c, args)) = 
obua@16781
    74
	    let
obua@16781
    75
		val h = print_pattern n (PConst (c,[]))
obua@16781
    76
	    in
obua@16781
    77
		print_pattern_list h args
obua@16781
    78
	    end
obua@16781
    79
	and print_pattern_list r [] = r
obua@16781
    80
	  | print_pattern_list (n, p) (t::ts) = 
obua@16781
    81
	    let
obua@16781
    82
		val (n, t) = print_pattern n t
obua@16781
    83
	    in
obua@16781
    84
		print_pattern_list (n, "App ("^p^", "^t^")") ts
obua@16781
    85
	    end
obua@16781
    86
obua@16781
    87
	val (n, pattern) = print_pattern 0 p
wenzelm@16842
    88
	val pattern =
wenzelm@16842
    89
            if List.exists Char.isSpace (String.explode pattern) then "("^pattern^")"
wenzelm@16842
    90
            else pattern
obua@16781
    91
	
wenzelm@16842
    92
	fun print_term d (Var x) = (*if x < d then "Var "^(str x) else "x"^(str (n-(x-d)-1))*)
wenzelm@16842
    93
              "Var " ^ str x
wenzelm@16842
    94
	  | print_term d (Const c) = "c" ^ str c
wenzelm@16842
    95
	  | print_term d (App (a,b)) = "App (" ^ print_term d a ^ ", " ^ print_term d b ^ ")"
wenzelm@16842
    96
	  | print_term d (Abs c) = "Abs (" ^ print_term (d + 1) c ^ ")"
obua@16781
    97
obua@16781
    98
	fun listvars n = if n = 0 then "x0" else "x"^(str n)^", "^(listvars (n-1))
obua@16781
    99
obua@16781
   100
	val term = print_term 0 t
wenzelm@16842
   101
	val term =
wenzelm@16842
   102
            if n > 0 then "Closure (["^(listvars (n-1))^"], "^term^")"
wenzelm@16842
   103
            else "Closure ([], "^term^")"
obua@16781
   104
			   
obua@16781
   105
    in
obua@16781
   106
	"lookup stack "^pattern^" = weak stack ("^term^")"
obua@16781
   107
    end
obua@16781
   108
obua@16781
   109
fun remove_dups (c::cs) = 
obua@16781
   110
    let val cs = remove_dups cs in
obua@16781
   111
	if (List.exists (fn x => x=c) cs) then cs else c::cs
obua@16781
   112
    end
obua@16781
   113
  | remove_dups [] = []
obua@16781
   114
obua@16781
   115
fun constants_of PVar = []
wenzelm@16842
   116
  | constants_of (PConst (c, ps)) = c :: List.concat (map constants_of ps)
obua@16781
   117
obua@16781
   118
fun constants_of_term (Var _) = []
obua@16781
   119
  | constants_of_term (Abs m) = constants_of_term m
obua@16781
   120
  | constants_of_term (App (a,b)) = (constants_of_term a)@(constants_of_term b)
obua@16781
   121
  | constants_of_term (Const c) = [c]
obua@16781
   122
    
obua@16781
   123
fun load_rules sname name prog = 
obua@16781
   124
    let
wenzelm@16842
   125
        (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
obua@16781
   126
	val buffer = ref ""
obua@16781
   127
	fun write s = (buffer := (!buffer)^s)
obua@16781
   128
	fun writeln s = (write s; write "\n")
obua@16781
   129
	fun writelist [] = ()
obua@16781
   130
	  | writelist (s::ss) = (writeln s; writelist ss)
obua@16781
   131
	fun str i = Int.toString i
obua@16781
   132
	val _ = writelist [
obua@16781
   133
		"structure "^name^" = struct",
obua@16781
   134
		"",
obua@16781
   135
		"datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
obua@16781
   136
	val constants = remove_dups (List.concat (map (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog))
obua@16781
   137
	val _ = map (fn x => write (" | c"^(str x))) constants
obua@16781
   138
	val _ = writelist [
obua@16781
   139
		"",
obua@16781
   140
		"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",
obua@16781
   141
		""]
obua@16781
   142
	val _ = (case prog of
obua@16781
   143
		    r::rs => (writeln ("fun "^(print_rule r)); 
obua@16781
   144
			      map (fn r => writeln("  | "^(print_rule r))) rs; 
obua@16781
   145
			      writeln ("  | lookup stack clos = weak_last stack clos"); ())								
obua@16781
   146
		  | [] => (writeln "fun lookup stack clos = weak_last stack clos"))
obua@16781
   147
	val _ = writelist [
obua@16781
   148
		"and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))",
obua@16781
   149
		"  | weak (SAppL (b, stack)) (Closure (e, Abs m)) =  weak stack (Closure (b::e, m))",
obua@16781
   150
		"  | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos",
obua@16782
   151
		"  | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))",
obua@16781
   152
		"  | weak stack (Closure (e, c)) = weak stack c",
obua@16781
   153
		"  | weak stack clos = lookup stack clos",
obua@16781
   154
		"and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))",
obua@16781
   155
		"  | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b",
obua@16781
   156
		"  | weak_last stack c = (stack, c)",
obua@16781
   157
		"",
obua@16781
   158
		"fun lift n (v as Var m) = if m < n then v else Var (m+1)",
obua@16781
   159
		"  | lift n (Abs t) = Abs (lift (n+1) t)",
obua@16781
   160
		"  | lift n (App (a,b)) = App (lift n a, lift n b)",
obua@16781
   161
		"  | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)",
obua@16781
   162
		"  | lift n c = c",
obua@16781
   163
		"and lift_env n e = map (lift n) e",
obua@16781
   164
		"",
obua@16781
   165
		"fun strong stack (Closure (e, Abs m)) = ",
obua@16781
   166
		"    let",
obua@16781
   167
		"      val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))",
obua@16781
   168
		"    in",
obua@16781
   169
		"      case stack' of",
obua@16781
   170
		"           SEmpty => strong (SAbs stack) wnf",
obua@16781
   171
		"         | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
obua@16781
   172
		"    end",
obua@16781
   173
		"  | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u",
obua@16781
   174
		"  | strong stack clos = strong_last stack clos",
obua@16781
   175
		"and strong_last (SAbs stack) m = strong stack (Abs m)",
obua@16781
   176
		"  | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b",
obua@16781
   177
		"  | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))",
obua@16781
   178
		"  | strong_last stack clos = (stack, clos)",
obua@16781
   179
		""]
obua@16781
   180
	
obua@16781
   181
	val ic = "(case c of "^(String.concat (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"						  	
obua@16781
   182
	val _ = writelist [
obua@16781
   183
		"fun importTerm ("^sname^".Var x) = Var x",
obua@16781
   184
		"  | importTerm ("^sname^".Const c) =  "^ic,
obua@16781
   185
		"  | importTerm ("^sname^".App (a, b)) = App (importTerm a, importTerm b)",
obua@16781
   186
		"  | importTerm ("^sname^".Abs m) = Abs (importTerm m)",
obua@16781
   187
		""]
obua@16781
   188
obua@16781
   189
	fun ec c = "  | exportTerm c"^(str c)^" = "^sname^".CConst "^(str c)
obua@16781
   190
	val _ = writelist [
obua@16781
   191
		"fun exportTerm (Var x) = "^sname^".CVar x",
obua@16781
   192
		"  | exportTerm (Const c) = "^sname^".CConst c",
obua@16781
   193
		"  | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)",
obua@16781
   194
		"  | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)",
obua@16782
   195
		"  | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"]
obua@16781
   196
	val _ = writelist (map ec constants)
obua@16781
   197
		
obua@16781
   198
	val _ = writelist [
obua@16781
   199
		"",
obua@16781
   200
		"fun rewrite t = ",
obua@16781
   201
		"    let",
obua@16781
   202
		"      val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))",
obua@16781
   203
		"    in",
obua@16781
   204
		"      case stack of ",
obua@16781
   205
		"           SEmpty => (case strong SEmpty wnf of",
obua@16781
   206
		"                          (SEmpty, snf) => exportTerm snf",
obua@16781
   207
		"                        | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",
obua@16781
   208
		"         | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",
obua@16781
   209
		"    end",
obua@16781
   210
		"",
obua@16781
   211
		"val _ = "^sname^".set_compiled_rewriter rewrite",
obua@16781
   212
		"",
obua@16781
   213
		"end;"]
obua@16781
   214
obua@16781
   215
	val _ = 
obua@16781
   216
	    let
obua@16782
   217
		(*val fout = TextIO.openOut "gen_code.ML"
obua@16781
   218
		val _ = TextIO.output (fout, !buffer)
obua@16782
   219
		val _  = TextIO.closeOut fout*)
obua@16781
   220
	    in
obua@16781
   221
		()
obua@16781
   222
	    end
obua@16781
   223
    in
obua@16781
   224
	compiled_rewriter := NONE;	
wenzelm@16842
   225
	use_text (K (), K ()) false (!buffer);
obua@16781
   226
	case !compiled_rewriter of 
obua@16781
   227
	    NONE => raise (Compile "cannot communicate with compiled function")
obua@16781
   228
	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
obua@16781
   229
    end	
obua@16781
   230
obua@16781
   231
fun compile eqs = 
obua@16781
   232
    let
obua@16781
   233
	val _ = map (fn (p, r) => 
obua@16781
   234
                  (check_freevars (count_patternvars p) r; 
obua@16781
   235
                   case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs
obua@16781
   236
    in
obua@16781
   237
	load_rules "AM_Compiler" "AM_compiled_code" eqs
obua@16781
   238
    end	
obua@16781
   239
obua@16781
   240
fun run prog t = (prog t)
obua@16781
   241
			 	  
obua@16781
   242
end
obua@16781
   243
obua@16781
   244
structure AbstractMachine = AM_Compiler