summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/Tools/nbe_eval.ML

changeset 19202 | 0b9eb4b0ad98 |

parent 19177 | 68c6824d8bb6 |

child 19795 | 746274ca400b |

1.1 --- a/src/Pure/Tools/nbe_eval.ML Tue Mar 07 04:06:02 2006 +0100 1.2 +++ b/src/Pure/Tools/nbe_eval.ML Tue Mar 07 14:09:48 2006 +0100 1.3 @@ -121,18 +121,19 @@ 1.4 1.5 open BasicCodegenThingol; 1.6 1.7 -fun eval xs (IConst ((f, _), _)) = lookup f 1.8 - | eval xs (IVar n) = 1.9 - AList.lookup (op =) xs n 1.10 - |> the_default (Var (n, [])) 1.11 - | eval xs (s `$ t) = apply (eval xs s) (eval xs t) 1.12 - | eval xs ((n, _) `|-> t) = 1.13 - Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t, 1.14 +fun eval xs = 1.15 + let 1.16 + fun evl (IConst (c, _)) = lookup c 1.17 + | evl (IVar n) = 1.18 + AList.lookup (op =) xs n 1.19 + |> the_default (Var (n, [])) 1.20 + | evl (s `$ t) = apply (eval xs s) (eval xs t) 1.21 + | evl ((n, _) `|-> t) = 1.22 + Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t, 1.23 [], 1, 1.24 fn () => let val var = new_name() in 1.25 AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end) 1.26 - | eval xs (IAbs (_, t)) = eval xs t 1.27 - | eval xs (ICase (_, t)) = eval xs t; 1.28 + in CodegenThingol.map_pure evl end; 1.29 1.30 (* finally... *) 1.31