(* ID: $Id$
Author: Klaus Aehlig, Tobias Nipkow
*)
(* ------------------------------ Evaluator ------------------------------ *)
(* Optimizations:
int instead of string in Constr
treat int via ML ints
*)
signature NBE_EVAL =
sig
(* named terms used for output only *)
datatype nterm =
C of string (* Named Constants *)
| V of string (* Free Variable *)
| B of int (* Named(!!) Bound Variables *)
| A of nterm*nterm (* Application *)
| AbsN of int*nterm ; (* Binding of named Variables *)
datatype Univ =
Constr of string*(Univ list) (* Named Constructors *)
| Var of string*(Univ list) (* Free variables *)
| BVar of int*(Univ list) (* Bound named variables *)
| Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
(* Functions *)
val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
val apply: Univ -> Univ -> Univ;
val to_term: Univ -> nterm;
val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
val new_name: unit -> int;
(* For testing
val eval: term -> (Univ list) -> Univ
*)
end;
(* FIXME add_funs and relatives should NOT be exported. Eventually it
should work like for quickcheck: Eval generates code which leaves the
function values in a public reference variable, the code is executed,
and the value of the reference variable is added to the internal
tables, all in one go, w/o interruption. *)
structure NBE_Eval:NBE_EVAL =
struct
datatype nterm =
C of string (* Named Constants *)
| V of string (* Free Variable *)
| B of int (* Named(!!) Variables *)
| A of nterm * nterm (* Application *)
| AbsN of int * nterm (* Binding of named Variables *);
fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
(* ------------------------------ The semantical universe --------------------- *)
(*
Functions are given by their semantical function value. To avoid
trouble with the ML-type system, these functions have the most
generic type, that is "Univ list -> Univ". The calling convention is
that the arguments come as a list, the last argument first. In
other words, a function call that usually would look like
f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n)
would be in our convention called as
f [x_n,..,x_2,x_1]
Moreover, to handle functions that are still waiting for some
arguments we have additionally a list of arguments collected to far
and the number of arguments we're still waiting for.
Finally, it might happen, that a function does not get all the
arguments it needs. In this case the function must provide means to
present itself as a string. As this might be a heavy-wight
operation, we delay it.
*)
datatype Univ =
Constr of string*(Univ list) (* Named Constructors *)
| Var of string*(Univ list) (* Free variables *)
| BVar of int*(Univ list) (* Bound named variables *)
| Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
fun to_term (Constr(name, args)) = apps (C name) (map to_term args)
| to_term (Var (name, args)) = apps (V name) (map to_term args)
| to_term (BVar (name, args)) = apps (B name) (map to_term args)
| to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
(*
A typical operation, why functions might be good for, is
application. Moreover, functions are the only values that can
reasonably we applied in a semantical way.
*)
fun apply (Fun(f,xs,1,name)) x = f (x::xs)
| apply (Fun(f,xs,n,name)) x = Fun(f,x::xs,n-1,name)
| apply (Constr(name,args)) x = Constr(name,x::args)
| apply (Var(name,args)) x = Var(name,x::args)
| apply (BVar(name,args)) x = BVar(name,x::args);
fun mk_Fun(name,v,0) = (name,v [])
| mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
(* ---------------- table with the meaning of constants -------------------- *)
val xfun_tab: Univ Symtab.table ref = ref Symtab.empty;
fun lookup s = case Symtab.lookup (!xfun_tab) s of
SOME x => x
| NONE => Constr(s,[]);
(* ------------------ evaluation with greetings to Tarski ------------------ *)
(* generation of fresh names *)
val counter = ref 0;
fun new_name() = (counter := !counter +1; !counter);
(* greetings to Tarski *)
open BasicCodegenThingol;
fun eval xs (IConst ((f, _), _)) = lookup f
| eval xs (IVar n) =
AList.lookup (op =) xs n
|> the_default (Var (n, []))
| eval xs (s `$ t) = apply (eval xs s) (eval xs t)
| eval xs ((n, _) `|-> t) =
Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t,
[], 1,
fn () => let val var = new_name() in
AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end)
| eval xs (IAbs (_, t)) = eval xs t
| eval xs (ICase (_, t)) = eval xs t;
(* finally... *)
fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));
end;