src/Pure/Tools/nbe_eval.ML
changeset 19116 d065ec558092
child 19147 0f584853b6a4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/nbe_eval.ML	Tue Feb 21 16:18:50 2006 +0100
     1.3 @@ -0,0 +1,151 @@
     1.4 +(*  ID:         $Id$
     1.5 +    Author:     Klaus Aehlig, Tobias Nipkow
     1.6 +*)
     1.7 +
     1.8 +(* ------------------------------ Evaluator  ------------------------------ *)
     1.9 +
    1.10 +(* Optimizations:
    1.11 + int instead of string in Constr
    1.12 + xtab as real table
    1.13 + treat int via ML ints
    1.14 +*)
    1.15 +
    1.16 +signature NBE_EVAL =
    1.17 +sig
    1.18 +(* named terms used for output only *)
    1.19 +datatype nterm =
    1.20 +    C of string (* Named Constants *)
    1.21 +  | V of string (* Free Variable *)
    1.22 +  | B of int (* Named(!!) Bound Variables *)
    1.23 +  | A of nterm*nterm (* Application *)
    1.24 +  | AbsN of int*nterm ; (* Binding of named Variables *)
    1.25 +
    1.26 +val nbe: term -> nterm
    1.27 +
    1.28 +datatype Univ = 
    1.29 +    Constr of string*(Univ list)       (* Named Constructors *)
    1.30 +  | Var of string*(Univ list)          (* Free variables *)
    1.31 +  | BVar of int*(Univ list)            (* Bound named variables *)
    1.32 +  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    1.33 +                                            (* Functions *)
    1.34 +val apply: Univ -> Univ -> Univ;
    1.35 +val to_term: Univ -> nterm;
    1.36 +
    1.37 +val lookup: string -> Univ;
    1.38 +val is_constr: string -> bool;
    1.39 +val register: string * (Univ list -> Univ) * int -> unit
    1.40 +val new_name: unit -> int;
    1.41 +
    1.42 +(* For testing
    1.43 +val eval: term -> (Univ list) -> Univ
    1.44 +*)
    1.45 +
    1.46 +end;
    1.47 +
    1.48 +(* FIXME add_funs and relatives should NOT be exported. Eventually it
    1.49 +should work like for quickcheck: Eval generates code which leaves the
    1.50 +function values in a public reference variable, the code is executed,
    1.51 +and the value of the reference variable is added to the internal
    1.52 +tables, all in one go, w/o interruption. *)
    1.53 +
    1.54 +
    1.55 +structure NBE_Eval:NBE_EVAL =
    1.56 +struct
    1.57 +
    1.58 +datatype nterm =
    1.59 +    C of string (* Named Constants *)
    1.60 +  | V of string (* Free Variable *)
    1.61 +  | B of int (* Named(!!) Variables *)
    1.62 +  | A of nterm * nterm (* Application *)
    1.63 +  | AbsN of int * nterm (* Binding of named Variables *);
    1.64 +
    1.65 +fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
    1.66 +
    1.67 +(* ------------------------------ The semantical universe --------------------- *)
    1.68 +
    1.69 +(*
    1.70 +   Functions are given by their semantical function value. To avoid
    1.71 +   trouble with the ML-type system, these functions have the most
    1.72 +   generic type, that is "Univ list -> Univ". The calling convention is
    1.73 +   that the arguments come as a list, the last argument first. In
    1.74 +   other words, a function call that usually would look like
    1.75 +
    1.76 +   f x_1 x_2 ... x_n   or   f(x_1,x_2, ..., x_n)
    1.77 +
    1.78 +   would be in our convention called as
    1.79 +
    1.80 +              f [x_n,..,x_2,x_1]
    1.81 +
    1.82 +   Moreover, to handle functions that are still waiting for some
    1.83 +   arguments we have additionally a list of arguments collected to far
    1.84 +   and the number of arguments we're still waiting for.
    1.85 +
    1.86 +   Finally, it might happen, that a function does not get all the
    1.87 +   arguments it needs. In this case the function must provide means to
    1.88 +   present itself as a string. As this might be a heavy-wight
    1.89 +   operation, we delay it.
    1.90 +*)
    1.91 +
    1.92 +datatype Univ = 
    1.93 +    Constr of string*(Univ list)       (* Named Constructors *)
    1.94 +  | Var of string*(Univ list)          (* Free variables *)
    1.95 +  | BVar of int*(Univ list)         (* Bound named variables *)
    1.96 +  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    1.97 +
    1.98 +fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
    1.99 +  |	to_term (Var   (name, args))    = apps (V name) (map to_term args)
   1.100 +  |	to_term (BVar  (name, args))    = apps (B name) (map to_term args)
   1.101 +  |	to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
   1.102 +
   1.103 +(*
   1.104 +   A typical operation, why functions might be good for, is
   1.105 +   application. Moreover, functions are the only values that can
   1.106 +   reasonably we applied in a semantical way.
   1.107 +*)
   1.108 +
   1.109 +fun  apply (Fun(f,xs,1,name))  x = f (x::xs)
   1.110 +   | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   1.111 +   | apply (Constr(name,args)) x = Constr(name,x::args)
   1.112 +   | apply (Var(name,args))    x = Var(name,x::args)
   1.113 +   | apply (BVar(name,args))   x = BVar(name,x::args);
   1.114 +
   1.115 +(* ---------------- table with the meaning of constants -------------------- *)
   1.116 +
   1.117 +val xfun_tab: (string * Univ)list ref = ref [];
   1.118 +fun do_register sx = (xfun_tab := sx :: !xfun_tab);
   1.119 +fun register(name,v,0) = do_register(name,v [])
   1.120 +  | register(name,v,n) = do_register(name,Fun(v,[],n, fn () => C name));
   1.121 +
   1.122 +fun do_lookup [] s          = NONE
   1.123 +  |	do_lookup ((n,v)::xs) s = if (s=n) then SOME v else do_lookup xs s;
   1.124 +
   1.125 +fun lookup s = case do_lookup (!xfun_tab) s of
   1.126 +    SOME x => x
   1.127 +  | NONE   => Constr(s,[]);
   1.128 +
   1.129 +fun is_constr s = is_none (do_lookup (!xfun_tab) s);
   1.130 +
   1.131 +(* ------------------ evaluation with greetings to Tarski ------------------ *)
   1.132 +
   1.133 +(* generation of fresh names *)
   1.134 +
   1.135 +val counter = ref 0;
   1.136 +
   1.137 +fun new_name() = (counter := !counter +1; !counter);
   1.138 +
   1.139 +(* greetings to Tarski *)
   1.140 +
   1.141 +fun eval(Const(f,_)) xs = lookup f
   1.142 +  | eval(Free(x,_)) xs = Var(x,[])
   1.143 +  | eval(Bound n) xs = List.nth(xs,n)
   1.144 +  | eval(s $ t) xs = apply (eval s xs) (eval t xs)
   1.145 +  | eval(Abs(_,_, t)) xs = Fun ((fn [x] => eval t (x::xs)),[],1,
   1.146 +                           fn () => let val var = new_name() in
   1.147 +                         AbsN(var, to_term (eval t ((BVar(var,[]) :: xs)))) end);
   1.148 +
   1.149 +
   1.150 +(* finally... *)
   1.151 +
   1.152 +fun nbe t = (counter :=0; to_term(eval t []));
   1.153 +
   1.154 +end;