1.1 --- a/src/Pure/Tools/am_interpreter.ML Thu Jul 14 19:28:23 2005 +0200
1.2 +++ b/src/Pure/Tools/am_interpreter.ML Thu Jul 14 19:28:24 2005 +0200
1.3 @@ -3,7 +3,9 @@
1.4 Author: Steven Obua
1.5 *)
1.6
1.7 -signature ABSTRACT_MACHINE = sig
1.8 +signature ABSTRACT_MACHINE =
1.9 +sig
1.10 +
1.11 datatype term = Var of int | Const of int | App of term * term | Abs of term
1.12
1.13 datatype pattern = PVar | PConst of int * (pattern list)
1.14 @@ -12,7 +14,7 @@
1.15
1.16 exception Compile of string;
1.17 val compile : (pattern * term) list -> program
1.18 -
1.19 +
1.20 exception Run of string;
1.21 val run : program -> term -> term
1.22
1.23 @@ -25,8 +27,8 @@
1.24 datatype pattern = PVar | PConst of int * (pattern list)
1.25
1.26 datatype closure = CVar of int | CConst of int
1.27 - | CApp of closure * closure | CAbs of closure
1.28 - | Closure of (closure list) * closure
1.29 + | CApp of closure * closure | CAbs of closure
1.30 + | Closure of (closure list) * closure
1.31
1.32 structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
1.33
1.34 @@ -57,22 +59,22 @@
1.35
1.36 (* earlier occurrence of PVar corresponds to higher de Bruijn index *)
1.37 fun pattern_match args PVar clos = SOME (clos::args)
1.38 - | pattern_match args (PConst (c, patterns)) clos =
1.39 + | pattern_match args (PConst (c, patterns)) clos =
1.40 let
1.41 - val (f, closargs) = strip_closure [] clos
1.42 + val (f, closargs) = strip_closure [] clos
1.43 in
1.44 - case f of
1.45 - CConst d =>
1.46 - if c = d then
1.47 - pattern_match_list args patterns closargs
1.48 - else
1.49 - NONE
1.50 - | _ => NONE
1.51 + case f of
1.52 + CConst d =>
1.53 + if c = d then
1.54 + pattern_match_list args patterns closargs
1.55 + else
1.56 + NONE
1.57 + | _ => NONE
1.58 end
1.59 and pattern_match_list args [] [] = SOME args
1.60 - | pattern_match_list args (p::ps) (c::cs) =
1.61 + | pattern_match_list args (p::ps) (c::cs) =
1.62 (case pattern_match args p c of
1.63 - NONE => NONE
1.64 + NONE => NONE
1.65 | SOME args => pattern_match_list args ps cs)
1.66 | pattern_match_list _ _ _ = NONE
1.67
1.68 @@ -88,26 +90,26 @@
1.69 fun pattern_key (PConst (c, ps)) = (c, length ps)
1.70 | pattern_key _ = raise (Compile "pattern reduces to variable")
1.71
1.72 -fun compile eqs =
1.73 +fun compile eqs =
1.74 let
1.75 - val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
1.76 - (pattern_key p, (p, clos_of_term r)))) eqs
1.77 + val eqs = map (fn (p, r) => (check_freevars (count_patternvars p) r;
1.78 + (pattern_key p, (p, clos_of_term r)))) eqs
1.79 in
1.80 - prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
1.81 - end
1.82 + prog_struct.make (map (fn (k, a) => (k, [a])) eqs)
1.83 + end
1.84
1.85 fun match_rules n [] clos = NONE
1.86 | match_rules n ((p,eq)::rs) clos =
1.87 case pattern_match [] p clos of
1.88 - NONE => match_rules (n+1) rs clos
1.89 + NONE => match_rules (n+1) rs clos
1.90 | SOME args => SOME (Closure (args, eq))
1.91
1.92 -fun match_closure prog clos =
1.93 +fun match_closure prog clos =
1.94 case len_head_of_closure 0 clos of
1.95 - (len, CConst c) =>
1.96 - (case prog_struct.lookup (prog, (c, len)) of
1.97 - NONE => NONE
1.98 - | SOME rules => match_rules 0 rules clos)
1.99 + (len, CConst c) =>
1.100 + (case prog_struct.lookup (prog, (c, len)) of
1.101 + NONE => NONE
1.102 + | SOME rules => match_rules 0 rules clos)
1.103 | _ => NONE
1.104
1.105 fun lift n (c as (CConst _)) = c
1.106 @@ -121,21 +123,21 @@
1.107 | weak prog (SAppL (b, stack)) (Closure (e, CAbs m)) = weak prog stack (Closure (b::e, m))
1.108 | weak prog stack (Closure (e, CVar n)) = weak prog stack (List.nth (e, n) handle Subscript => (CVar (n-(length e))))
1.109 | weak prog stack (Closure (e, c as CConst _)) = weak prog stack c
1.110 - | weak prog stack clos =
1.111 + | weak prog stack clos =
1.112 case match_closure prog clos of
1.113 - NONE => weak_last prog stack clos
1.114 + NONE => weak_last prog stack clos
1.115 | SOME r => weak prog stack r
1.116 and weak_last prog (SAppR (a, stack)) b = weak prog stack (CApp (a,b))
1.117 | weak_last prog (s as (SAppL (b, stack))) a = weak prog (SAppR (a, stack)) b
1.118 - | weak_last prog stack c = (stack, c)
1.119 + | weak_last prog stack c = (stack, c)
1.120
1.121 -fun strong prog stack (Closure (e, CAbs m)) =
1.122 +fun strong prog stack (Closure (e, CAbs m)) =
1.123 let
1.124 - val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
1.125 + val (stack', wnf) = weak prog SEmpty (Closure ((CVar 0)::(lift_env 0 e), m))
1.126 in
1.127 - case stack' of
1.128 - SEmpty => strong prog (SAbs stack) wnf
1.129 - | _ => raise (Run "internal error in strong: weak failed")
1.130 + case stack' of
1.131 + SEmpty => strong prog (SAbs stack) wnf
1.132 + | _ => raise (Run "internal error in strong: weak failed")
1.133 end
1.134 | strong prog stack (clos as (CApp (u, v))) = strong prog (SAppL (v, stack)) u
1.135 | strong prog stack clos = strong_last prog stack clos
1.136 @@ -144,17 +146,17 @@
1.137 | strong_last prog (SAppR (a, stack)) b = strong_last prog stack (CApp (a, b))
1.138 | strong_last prog stack clos = (stack, clos)
1.139
1.140 -fun run prog t =
1.141 +fun run prog t =
1.142 let
1.143 - val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
1.144 + val (stack, wnf) = weak prog SEmpty (Closure ([], clos_of_term t))
1.145 in
1.146 - case stack of
1.147 - SEmpty => (case strong prog SEmpty wnf of
1.148 - (SEmpty, snf) => term_of_clos snf
1.149 - | _ => raise (Run "internal error in run: strong failed"))
1.150 - | _ => raise (Run "internal error in run: weak failed")
1.151 + case stack of
1.152 + SEmpty => (case strong prog SEmpty wnf of
1.153 + (SEmpty, snf) => term_of_clos snf
1.154 + | _ => raise (Run "internal error in run: strong failed"))
1.155 + | _ => raise (Run "internal error in run: weak failed")
1.156 end
1.157 -
1.158 +
1.159 end
1.160
1.161 structure AbstractMachine = AM_Interpreter