diff -r 228d663cc9b3 -r 5979c46853d1 src/Pure/Tools/am_interpreter.ML --- 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