src/Pure/Tools/nbe_eval.ML
changeset 19147 0f584853b6a4
parent 19116 d065ec558092
child 19167 f237c0cb3882
     1.1 --- a/src/Pure/Tools/nbe_eval.ML	Mon Feb 27 14:03:15 2006 +0100
     1.2 +++ b/src/Pure/Tools/nbe_eval.ML	Mon Feb 27 14:03:31 2006 +0100
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  (* Optimizations:
     1.6   int instead of string in Constr
     1.7 - xtab as real table
     1.8   treat int via ML ints
     1.9  *)
    1.10  
    1.11 @@ -20,20 +19,18 @@
    1.12    | A of nterm*nterm (* Application *)
    1.13    | AbsN of int*nterm ; (* Binding of named Variables *)
    1.14  
    1.15 -val nbe: term -> nterm
    1.16 -
    1.17  datatype Univ = 
    1.18      Constr of string*(Univ list)       (* Named Constructors *)
    1.19    | Var of string*(Univ list)          (* Free variables *)
    1.20    | BVar of int*(Univ list)            (* Bound named variables *)
    1.21    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    1.22                                              (* Functions *)
    1.23 +val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
    1.24 +
    1.25  val apply: Univ -> Univ -> Univ;
    1.26  val to_term: Univ -> nterm;
    1.27  
    1.28 -val lookup: string -> Univ;
    1.29 -val is_constr: string -> bool;
    1.30 -val register: string * (Univ list -> Univ) * int -> unit
    1.31 +val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
    1.32  val new_name: unit -> int;
    1.33  
    1.34  (* For testing
    1.35 @@ -109,22 +106,17 @@
    1.36     | apply (Var(name,args))    x = Var(name,x::args)
    1.37     | apply (BVar(name,args))   x = BVar(name,x::args);
    1.38  
    1.39 +fun mk_Fun(name,v,0) = (name,v [])
    1.40 +  | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
    1.41 +
    1.42  (* ---------------- table with the meaning of constants -------------------- *)
    1.43  
    1.44 -val xfun_tab: (string * Univ)list ref = ref [];
    1.45 -fun do_register sx = (xfun_tab := sx :: !xfun_tab);
    1.46 -fun register(name,v,0) = do_register(name,v [])
    1.47 -  | register(name,v,n) = do_register(name,Fun(v,[],n, fn () => C name));
    1.48 +val xfun_tab: Univ Symtab.table ref = ref Symtab.empty;
    1.49  
    1.50 -fun do_lookup [] s          = NONE
    1.51 -  |	do_lookup ((n,v)::xs) s = if (s=n) then SOME v else do_lookup xs s;
    1.52 -
    1.53 -fun lookup s = case do_lookup (!xfun_tab) s of
    1.54 +fun lookup s = case Symtab.lookup (!xfun_tab) s of
    1.55      SOME x => x
    1.56    | NONE   => Constr(s,[]);
    1.57  
    1.58 -fun is_constr s = is_none (do_lookup (!xfun_tab) s);
    1.59 -
    1.60  (* ------------------ evaluation with greetings to Tarski ------------------ *)
    1.61  
    1.62  (* generation of fresh names *)
    1.63 @@ -135,17 +127,21 @@
    1.64  
    1.65  (* greetings to Tarski *)
    1.66  
    1.67 -fun eval(Const(f,_)) xs = lookup f
    1.68 -  | eval(Free(x,_)) xs = Var(x,[])
    1.69 -  | eval(Bound n) xs = List.nth(xs,n)
    1.70 -  | eval(s $ t) xs = apply (eval s xs) (eval t xs)
    1.71 -  | eval(Abs(_,_, t)) xs = Fun ((fn [x] => eval t (x::xs)),[],1,
    1.72 -                           fn () => let val var = new_name() in
    1.73 -                         AbsN(var, to_term (eval t ((BVar(var,[]) :: xs)))) end);
    1.74 +structure IL = CodegenThingol
    1.75 +
    1.76 +fun eval(IL.IConst((f,_),_)) xs = lookup f
    1.77 +  | eval(IL.IVarE(n,_)) xs =
    1.78 +      (case AList.lookup (op =) xs n of NONE => Var(n,[])
    1.79 +       | SOME v => v)
    1.80 +  | eval(IL.IApp(s,t)) xs = apply (eval s xs) (eval t xs)
    1.81 +  | eval(IL.IAbs(IL.IVarE(n,_), t)) xs =
    1.82 +      Fun (fn [x] => eval t ((n,x)::xs), [], 1,
    1.83 +           fn () => let val var = new_name() in
    1.84 +                 AbsN(var, to_term (eval t ((n,BVar(var,[])) :: xs))) end);
    1.85  
    1.86  
    1.87  (* finally... *)
    1.88  
    1.89 -fun nbe t = (counter :=0; to_term(eval t []));
    1.90 +fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval t []));
    1.91  
    1.92  end;