src/Pure/Tools/nbe_eval.ML
author nipkow
Tue, 21 Feb 2006 16:18:50 +0100
changeset 19116 d065ec558092
child 19147 0f584853b6a4
permissions -rwxr-xr-x
New normalization-by-evaluation package

(*  ID:         $Id$
    Author:     Klaus Aehlig, Tobias Nipkow
*)

(* ------------------------------ Evaluator  ------------------------------ *)

(* Optimizations:
 int instead of string in Constr
 xtab as real table
 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 *)

val nbe: term -> nterm

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 apply: Univ -> Univ -> Univ;
val to_term: Univ -> nterm;

val lookup: string -> Univ;
val is_constr: string -> bool;
val register: string * (Univ list -> Univ) * int -> unit
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);

(* ---------------- table with the meaning of constants -------------------- *)

val xfun_tab: (string * Univ)list ref = ref [];
fun do_register sx = (xfun_tab := sx :: !xfun_tab);
fun register(name,v,0) = do_register(name,v [])
  | register(name,v,n) = do_register(name,Fun(v,[],n, fn () => C name));

fun do_lookup [] s          = NONE
  |	do_lookup ((n,v)::xs) s = if (s=n) then SOME v else do_lookup xs s;

fun lookup s = case do_lookup (!xfun_tab) s of
    SOME x => x
  | NONE   => Constr(s,[]);

fun is_constr s = is_none (do_lookup (!xfun_tab) s);

(* ------------------ evaluation with greetings to Tarski ------------------ *)

(* generation of fresh names *)

val counter = ref 0;

fun new_name() = (counter := !counter +1; !counter);

(* greetings to Tarski *)

fun eval(Const(f,_)) xs = lookup f
  | eval(Free(x,_)) xs = Var(x,[])
  | eval(Bound n) xs = List.nth(xs,n)
  | eval(s $ t) xs = apply (eval s xs) (eval t xs)
  | eval(Abs(_,_, t)) xs = Fun ((fn [x] => eval t (x::xs)),[],1,
                           fn () => let val var = new_name() in
                         AbsN(var, to_term (eval t ((BVar(var,[]) :: xs)))) end);


(* finally... *)

fun nbe t = (counter :=0; to_term(eval t []));

end;