--- a/src/Pure/Tools/am_interpreter.ML Thu Jul 14 19:28:23 2005 +0200
+++ b/src/Pure/Tools/am_interpreter.ML Thu Jul 14 19:28:24 2005 +0200
@@ -3,7 +3,9 @@
Author: Steven Obua
*)
-signature ABSTRACT_MACHINE = sig
+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)
@@ -12,7 +14,7 @@
exception Compile of string;
val compile : (pattern * term) list -> program
-
+
exception Run of string;
val run : program -> term -> term
@@ -25,8 +27,8 @@
datatype pattern = PVar | PConst of int * (pattern list)
datatype closure = CVar of int | CConst of int
- | CApp of closure * closure | CAbs of closure
- | Closure of (closure list) * closure
+ | CApp of closure * closure | CAbs of closure
+ | Closure of (closure list) * closure
structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
@@ -57,22 +59,22 @@
(* earlier occurrence of PVar corresponds to higher de Bruijn index *)
fun pattern_match args PVar clos = SOME (clos::args)
- | pattern_match args (PConst (c, patterns)) clos =
+ | pattern_match args (PConst (c, patterns)) clos =
let
- val (f, closargs) = strip_closure [] clos
+ val (f, closargs) = strip_closure [] clos
in
- case f of
- CConst d =>
- if c = d then
- pattern_match_list args patterns closargs
- else
- NONE
- | _ => NONE
+ case f of
+ CConst d =>
+ if c = d then
+ pattern_match_list args patterns closargs
+ else
+ NONE
+ | _ => NONE
end
and pattern_match_list args [] [] = SOME args
- | pattern_match_list args (p::ps) (c::cs) =
+ | pattern_match_list args (p::ps) (c::cs) =
(case pattern_match args p c of
- NONE => NONE
+ NONE => NONE
| SOME args => pattern_match_list args ps cs)
| pattern_match_list _ _ _ = NONE
@@ -88,26 +90,26 @@
fun pattern_key (PConst (c, ps)) = (c, length ps)
| pattern_key _ = raise (Compile "pattern reduces to variable")
-fun compile eqs =
+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 eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
+ (pattern_key p, (p, clos_of_term r)))) eqs
in
- prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
- end
+ prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
+ end
fun match_rules n [] clos = NONE
| match_rules n ((p,eq)::rs) clos =
case pattern_match [] p clos of
- NONE => match_rules (n+1) rs clos
+ NONE => match_rules (n+1) rs clos
| SOME args => SOME (Closure (args, eq))
-fun match_closure prog clos =
+fun match_closure prog clos =
case len_head_of_closure 0 clos of
- (len, CConst c) =>
- (case prog_struct.lookup (prog, (c, len)) of
- NONE => NONE
- | SOME rules => match_rules 0 rules clos)
+ (len, CConst c) =>
+ (case prog_struct.lookup (prog, (c, len)) of
+ NONE => NONE
+ | SOME rules => match_rules 0 rules clos)
| _ => NONE
fun lift n (c as (CConst _)) = c
@@ -121,21 +123,21 @@
| 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 =
+ | weak prog stack clos =
case match_closure prog clos of
- NONE => weak_last prog stack clos
+ 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)
+ | weak_last prog stack c = (stack, c)
-fun strong prog stack (Closure (e, CAbs m)) =
+fun strong prog stack (Closure (e, CAbs m)) =
let
- val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
+ val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
in
- case stack' of
- SEmpty => strong prog (SAbs stack) wnf
- | _ => raise (Run "internal error in strong: weak failed")
+ case stack' of
+ SEmpty => strong 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
@@ -144,17 +146,17 @@
| strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
| strong_last prog stack clos = (stack, clos)
-fun run prog t =
+fun run prog t =
let
- val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
+ val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
in
- case stack of
- SEmpty => (case strong 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")
+ case stack of
+ SEmpty => (case strong 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
structure AbstractMachine = AM_Interpreter