--- a/src/Tools/Compute_Oracle/am_interpreter.ML Mon Jul 09 11:44:23 2007 +0200
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML Mon Jul 09 17:36:25 2007 +0200
@@ -1,32 +1,13 @@
-(* Title: Tools/Compute_Oracle/am_interpreter.ML
+(* Title: Pure/Tools/am_interpreter.ML
ID: $Id$
Author: Steven Obua
*)
-signature ABSTRACT_MACHINE =
-sig
-
-datatype term = Var of int | Const of int | App of term * term | Abs of term
-
-datatype pattern = PVar | PConst of int * (pattern list)
-
-type program
-
-exception Compile of string;
-val compile : (pattern * term) list -> program
-
-exception Run of string;
-val run : program -> term -> term
-
-end
-
structure AM_Interpreter : ABSTRACT_MACHINE = struct
-datatype term = Var of int | Const of int | App of term * term | Abs of term
+open AbstractMachine;
-datatype pattern = PVar | PConst of int * (pattern list)
-
-datatype closure = CVar of int | CConst of int
+datatype closure = CDummy | CVar of int | CConst of int
| CApp of closure * closure | CAbs of closure
| Closure of (closure list) * closure
@@ -36,9 +17,6 @@
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)
@@ -49,6 +27,7 @@
| 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")
+ | term_of_clos CDummy = raise (Run "internal error: dummy in normalized term found")
fun strip_closure args (CApp (a,b)) = strip_closure (b::args) a
| strip_closure args x = (x, args)
@@ -78,24 +57,29 @@
| SOME args => pattern_match_list args ps cs)
| pattern_match_list _ _ _ = NONE
-(* Returns true iff at most 0 .. (free-1) occur unbound. therefore check_freevars 0 t iff t is closed *)
-fun check_freevars free (Var x) = x < free
- | check_freevars free (Const c) = true
- | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
- | check_freevars free (Abs m) = check_freevars (free+1) m
-
fun count_patternvars PVar = 1
| count_patternvars (PConst (_, ps)) = List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps
fun pattern_key (PConst (c, ps)) = (c, length ps)
| pattern_key _ = raise (Compile "pattern reduces to variable")
+(*Returns true iff at most 0 .. (free-1) occur unbound. therefore
+ check_freevars 0 t iff t is closed*)
+fun check_freevars free (Var x) = x < free
+ | check_freevars free (Const c) = true
+ | check_freevars free (App (u, v)) = check_freevars free u andalso check_freevars free v
+ | check_freevars free (Abs m) = check_freevars (free+1) m
+
fun compile eqs =
let
- val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
- (pattern_key p, (p, clos_of_term r)))) eqs
+ 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 eqs = map (fn (p, r) => (check (p,r); (pattern_key p, (p, clos_of_term r)))) eqs
+ fun merge (k, a) table = prog_struct.update (k, case prog_struct.lookup table k of NONE => [a] | SOME l => a::l) table
+ val p = fold merge eqs prog_struct.empty
in
- Program (prog_struct.make (map (fn (k, a) => (k, [a])) eqs))
+ Program p
end
fun match_rules n [] clos = NONE
@@ -112,51 +96,66 @@
| SOME rules => match_rules 0 rules clos)
| _ => NONE
-fun lift n (c as (CConst _)) = c
- | lift n (v as CVar m) = if m < n then v else CVar (m+1)
- | lift n (CAbs t) = CAbs (lift (n+1) t)
- | lift n (CApp (a,b)) = CApp (lift n a, lift n b)
- | lift n (Closure (e, a)) = Closure (lift_env n e, lift (n+(length e)) a)
-and lift_env n e = map (lift n) e
+
+type state = bool * program * stack * closure
+
+datatype loopstate = Continue of state | Stop of stack * closure
+
+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 weak prog stack (Closure (e, CApp (a, b))) = weak prog (SAppL (Closure (e, b), stack)) (Closure (e, a))
- | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
- | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
- | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
- | weak prog stack clos =
- case match_closure prog clos of
- NONE => weak_last prog stack clos
- | SOME r => weak prog stack r
-and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
- | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
- | weak_last prog stack c = (stack, c)
+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
-fun strong prog stack (Closure (e, CAbs m)) =
+fun weak_reduce (false, prog, stack, Closure (e, CApp (a, b))) = Continue (false, prog, SAppL (Closure (e, b), stack), Closure (e, a))
+ | weak_reduce (false, prog, SAppL (b, stack), Closure (e, CAbs m)) = Continue (false, prog, stack, Closure (b::e, m))
+ | weak_reduce (false, prog, stack, Closure (e, CVar n)) = Continue (false, prog, stack, case List.nth (e, n) of CDummy => CVar n | r => r)
+ | weak_reduce (false, prog, stack, Closure (e, c as CConst _)) = Continue (false, prog, stack, c)
+ | weak_reduce (false, prog, stack, clos) =
+ (case match_closure prog clos of
+ NONE => Continue (true, prog, stack, clos)
+ | SOME r => Continue (false, prog, stack, r))
+ | weak_reduce (true, prog, SAppR (a, stack), b) = Continue (false, prog, stack, CApp (a,b))
+ | weak_reduce (true, prog, s as (SAppL (b, stack)), a) = Continue (false, prog, SAppR (a, stack), b)
+ | weak_reduce (true, prog, stack, c) = Stop (stack, c)
+
+fun strong_reduce (false, prog, stack, Closure (e, CAbs m)) =
let
- val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
+ val (stack', wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure (CDummy::e, m))
in
case stack' of
- SEmpty => strong prog (SAbs stack) wnf
+ SEmpty => Continue (false, prog, SAbs stack, wnf)
| _ => raise (Run "internal error in strong: weak failed")
end
- | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
- | strong prog stack clos = strong_last prog stack clos
-and strong_last prog (SAbs stack) m = strong prog stack (CAbs m)
- | strong_last prog (SAppL (b, stack)) a = strong prog (SAppR (a, stack)) b
- | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
- | strong_last prog stack clos = (stack, clos)
+ | strong_reduce (false, prog, stack, clos as (CApp (u, v))) = Continue (false, prog, SAppL (v, stack), u)
+ | strong_reduce (false, prog, stack, clos) = Continue (true, prog, stack, clos)
+ | strong_reduce (true, prog, SAbs stack, m) = Continue (false, prog, stack, CAbs m)
+ | strong_reduce (true, prog, SAppL (b, stack), a) = Continue (false, prog, SAppR (a, stack), b)
+ | strong_reduce (true, prog, SAppR (a, stack), b) = Continue (true, prog, stack, CApp (a, b))
+ | strong_reduce (true, prog, stack, clos) = Stop (stack, clos)
fun run prog t =
let
- val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
+ val (stack, wnf) = do_reduction weak_reduce (false, prog, SEmpty, Closure ([], clos_of_term t))
in
case stack of
- SEmpty => (case strong prog SEmpty wnf of
+ SEmpty => (case do_reduction strong_reduce (false, prog, SEmpty, wnf) of
(SEmpty, snf) => term_of_clos snf
| _ => raise (Run "internal error in run: strong failed"))
| _ => raise (Run "internal error in run: weak failed")
end
-end
+fun discard p = ()
-structure AbstractMachine = AM_Interpreter
+end