--- a/src/Tools/Compute_Oracle/am_compiler.ML Mon Jul 09 11:44:23 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Mon Jul 09 17:36:25 2007 +0200
@@ -1,4 +1,4 @@
-(* Title: Tools/Compute_Oracle/am_compiler.ML
+(* Title: Pure/Tools/am_compiler.ML
ID: $Id$
Author: Steven Obua
*)
@@ -7,10 +7,7 @@
sig
include ABSTRACT_MACHINE
- datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure | Closure of (closure list) * closure
-
- val set_compiled_rewriter : (term -> closure) -> unit
+ val set_compiled_rewriter : (term -> term) -> unit
val list_nth : 'a list * int -> 'a
val list_map : ('a -> 'b) -> 'a list -> 'b list
end
@@ -20,39 +17,14 @@
val list_nth = List.nth;
val list_map = map;
-datatype term = Var of int | Const of int | App of term * term | Abs of term
-
-datatype pattern = PVar | PConst of int * (pattern list)
+open AbstractMachine;
-datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure
- | Closure of (closure list) * closure
-
-val compiled_rewriter = ref (NONE:(term -> closure)Option.option)
+val compiled_rewriter = ref (NONE:(term -> term)Option.option)
fun set_compiled_rewriter r = (compiled_rewriter := SOME r)
type program = (term -> term)
-datatype stack = SEmpty | SAppL of closure * stack | SAppR of closure * stack | SAbs of stack
-
-exception Compile of string;
-exception Run of string;
-
-fun clos_of_term (Var x) = CVar x
- | clos_of_term (Const c) = CConst c
- | clos_of_term (App (u, v)) = CApp (clos_of_term u, clos_of_term v)
- | clos_of_term (Abs u) = CAbs (clos_of_term u)
-
-fun term_of_clos (CVar x) = Var x
- | term_of_clos (CConst c) = Const c
- | term_of_clos (CApp (u, v)) = App (term_of_clos u, term_of_clos v)
- | term_of_clos (CAbs u) = Abs (term_of_clos u)
- | term_of_clos (Closure (e, u)) =
- raise (Run "internal error: closure in normalized term found")
-
-fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
- | strip_closure args x = (x, args)
(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
check_freevars 0 t iff t is closed*)
@@ -103,7 +75,7 @@
else "Closure ([], "^term^")"
in
- "lookup stack "^pattern^" = weak stack ("^term^")"
+ " | weak_reduce (false, stack, "^pattern^") = Continue (false, stack, "^term^")"
end
fun constants_of PVar = []
@@ -116,7 +88,6 @@
fun load_rules sname name prog =
let
- (* FIXME consider using more readable/efficient Buffer.empty |> fold Buffer.add etc. *)
val buffer = ref ""
fun write s = (buffer := (!buffer)^s)
fun writeln s = (write s; write "\n")
@@ -126,50 +97,62 @@
val _ = writelist [
"structure "^name^" = struct",
"",
- "datatype term = App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
+ "datatype term = Dummy | App of term * term | Abs of term | Var of int | Const of int | Closure of term list * term"]
val constants = distinct (op =) (maps (fn (p, r) => ((constants_of p)@(constants_of_term r))) prog)
val _ = map (fn x => write (" | c"^(str x))) constants
val _ = writelist [
"",
"datatype stack = SEmpty | SAppL of term * stack | SAppR of term * stack | SAbs of stack",
- ""]
- val _ = (case prog of
- r::rs => (writeln ("fun "^(print_rule r));
- map (fn r => writeln(" | "^(print_rule r))) rs;
- writeln (" | lookup stack clos = weak_last stack clos"); ())
- | [] => (writeln "fun lookup stack clos = weak_last stack clos"))
- val _ = writelist [
- "and weak stack (Closure (e, App (a, b))) = weak (SAppL (Closure (e, b), stack)) (Closure (e, a))",
- " | weak (SAppL (b, stack)) (Closure (e, Abs m)) = weak stack (Closure (b::e, m))",
- " | weak stack (clos as Closure (_, Abs _)) = weak_last stack clos",
- " | weak stack (Closure (e, Var n)) = weak stack ("^sname^".list_nth (e, n) handle _ => (Var (n-(length e))))",
- " | weak stack (Closure (e, c)) = weak stack c",
- " | weak stack clos = lookup stack clos",
- "and weak_last (SAppR (a, stack)) b = weak stack (App(a, b))",
- " | weak_last (SAppL (b, stack)) a = weak (SAppR (a, stack)) b",
- " | weak_last stack c = (stack, c)",
+ "",
+ "type state = bool * stack * term",
+ "",
+ "datatype loopstate = Continue of state | Stop of stack * term",
+ "",
+ "fun proj_C (Continue s) = s",
+ " | proj_C _ = raise Match",
+ "",
+ "fun proj_S (Stop s) = s",
+ " | proj_S _ = raise Match",
+ "",
+ "fun cont (Continue _) = true",
+ " | cont _ = false",
"",
- "fun lift n (v as Var m) = if m < n then v else Var (m+1)",
- " | lift n (Abs t) = Abs (lift (n+1) t)",
- " | lift n (App (a,b)) = App (lift n a, lift n b)",
- " | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)",
- " | lift n c = c",
- "and lift_env n e = map (lift n) e",
+ "fun do_reduction reduce p =",
+ " let",
+ " val s = ref (Continue p)",
+ " val _ = while cont (!s) do (s := reduce (proj_C (!s)))",
+ " in",
+ " proj_S (!s)",
+ " end",
+ ""]
+
+ val _ = writelist [
+ "fun weak_reduce (false, stack, Closure (e, App (a, b))) = Continue (false, SAppL (Closure (e, b), stack), Closure (e, a))",
+ " | weak_reduce (false, SAppL (b, stack), Closure (e, Abs m)) = Continue (false, stack, Closure (b::e, m))",
+ " | weak_reduce (false, stack, c as Closure (e, Abs m)) = Continue (true, stack, c)",
+ " | weak_reduce (false, stack, Closure (e, Var n)) = Continue (false, stack, case "^sname^".list_nth (e, n) of Dummy => Var n | r => r)",
+ " | weak_reduce (false, stack, Closure (e, c)) = Continue (false, stack, c)"]
+ val _ = writelist (map print_rule prog)
+ val _ = writelist [
+ " | weak_reduce (false, stack, clos) = Continue (true, stack, clos)",
+ " | weak_reduce (true, SAppR (a, stack), b) = Continue (false, stack, App (a,b))",
+ " | weak_reduce (true, s as (SAppL (b, stack)), a) = Continue (false, SAppR (a, stack), b)",
+ " | weak_reduce (true, stack, c) = Stop (stack, c)",
"",
- "fun strong stack (Closure (e, Abs m)) = ",
+ "fun strong_reduce (false, stack, Closure (e, Abs m)) =",
" let",
- " val (stack', wnf) = weak SEmpty (Closure ((Var 0)::(lift_env 0 e), m))",
+ " val (stack', wnf) = do_reduction weak_reduce (false, SEmpty, Closure (Dummy::e, m))",
" in",
- " case stack' of",
- " SEmpty => strong (SAbs stack) wnf",
- " | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
- " end",
- " | strong stack (clos as (App (u, v))) = strong (SAppL (v, stack)) u",
- " | strong stack clos = strong_last stack clos",
- "and strong_last (SAbs stack) m = strong stack (Abs m)",
- " | strong_last (SAppL (b, stack)) a = strong (SAppR (a, stack)) b",
- " | strong_last (SAppR (a, stack)) b = strong_last stack (App (a, b))",
- " | strong_last stack clos = (stack, clos)",
+ " case stack' of",
+ " SEmpty => Continue (false, SAbs stack, wnf)",
+ " | _ => raise ("^sname^".Run \"internal error in strong: weak failed\")",
+ " end",
+ " | strong_reduce (false, stack, clos as (App (u, v))) = Continue (false, SAppL (v, stack), u)",
+ " | strong_reduce (false, stack, clos) = Continue (true, stack, clos)",
+ " | strong_reduce (true, SAbs stack, m) = Continue (false, stack, Abs m)",
+ " | strong_reduce (true, SAppL (b, stack), a) = Continue (false, SAppR (a, stack), b)",
+ " | strong_reduce (true, SAppR (a, stack), b) = Continue (true, stack, App (a, b))",
+ " | strong_reduce (true, stack, clos) = Stop (stack, clos)",
""]
val ic = "(case c of "^(implode (map (fn c => (str c)^" => c"^(str c)^" | ") constants))^" _ => Const c)"
@@ -180,23 +163,24 @@
" | importTerm ("^sname^".Abs m) = Abs (importTerm m)",
""]
- fun ec c = " | exportTerm c"^(str c)^" = "^sname^".CConst "^(str c)
+ fun ec c = " | exportTerm c"^(str c)^" = "^sname^".Const "^(str c)
val _ = writelist [
- "fun exportTerm (Var x) = "^sname^".CVar x",
- " | exportTerm (Const c) = "^sname^".CConst c",
- " | exportTerm (App (a,b)) = "^sname^".CApp (exportTerm a, exportTerm b)",
- " | exportTerm (Abs m) = "^sname^".CAbs (exportTerm m)",
- " | exportTerm (Closure (closlist, clos)) = "^sname^".Closure ("^sname^".list_map exportTerm closlist, exportTerm clos)"]
+ "fun exportTerm (Var x) = "^sname^".Var x",
+ " | exportTerm (Const c) = "^sname^".Const c",
+ " | exportTerm (App (a,b)) = "^sname^".App (exportTerm a, exportTerm b)",
+ " | exportTerm (Abs m) = "^sname^".Abs (exportTerm m)",
+ " | exportTerm (Closure (closlist, clos)) = raise ("^sname^".Run \"internal error, cannot export Closure\")",
+ " | exportTerm Dummy = raise ("^sname^".Run \"internal error, cannot export Dummy\")"]
val _ = writelist (map ec constants)
val _ = writelist [
"",
"fun rewrite t = ",
" let",
- " val (stack, wnf) = weak SEmpty (Closure ([], importTerm t))",
+ " val (stack, wnf) = do_reduction weak_reduce (false, SEmpty, Closure ([], importTerm t))",
" in",
" case stack of ",
- " SEmpty => (case strong SEmpty wnf of",
+ " SEmpty => (case do_reduction strong_reduce (false, SEmpty, wnf) of",
" (SEmpty, snf) => exportTerm snf",
" | _ => raise ("^sname^".Run \"internal error in rewrite: strong failed\"))",
" | _ => (raise ("^sname^".Run \"internal error in rewrite: weak failed\"))",
@@ -206,33 +190,29 @@
"",
"end;"]
- val _ =
- let
- (*val fout = TextIO.openOut "gen_code.ML"
- val _ = TextIO.output (fout, !buffer)
- val _ = TextIO.closeOut fout*)
- in
- ()
- end
in
compiled_rewriter := NONE;
use_text "" Output.ml_output false (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
- | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
+ | SOME r => (compiled_rewriter := NONE; r)
end
fun compile eqs =
let
+ val _ = if exists (fn (a,b,c) => not (null a)) eqs then raise Compile ("cannot deal with guards") else ()
+ val eqs = map (fn (a,b,c) => (b,c)) eqs
+ fun check (p, r) = if check_freevars (count_patternvars p) r then () else raise Compile ("unbound variables in rule")
val _ = map (fn (p, r) =>
- (check_freevars (count_patternvars p) r;
- case p of PVar => raise (Compile "pattern reduces to a variable") | _ => ())) eqs
+ (check (p, r);
+ case p of PVar => raise (Compile "pattern is just a variable") | _ => ())) eqs
in
load_rules "AM_Compiler" "AM_compiled_code" eqs
end
fun run prog t = (prog t)
+
+fun discard p = ()
end
-structure AbstractMachine = AM_Compiler