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