src/Pure/Tools/nbe_eval.ML
author nipkow
Mon Feb 27 14:03:31 2006 +0100 (2006-02-27)
changeset 19147 0f584853b6a4
parent 19116 d065ec558092
child 19167 f237c0cb3882
permissions -rwxr-xr-x
added nbe, updated neb_*
     1 (*  ID:         $Id$
     2     Author:     Klaus Aehlig, Tobias Nipkow
     3 *)
     4 
     5 (* ------------------------------ Evaluator  ------------------------------ *)
     6 
     7 (* Optimizations:
     8  int instead of string in Constr
     9  treat int via ML ints
    10 *)
    11 
    12 signature NBE_EVAL =
    13 sig
    14 (* named terms used for output only *)
    15 datatype nterm =
    16     C of string (* Named Constants *)
    17   | V of string (* Free Variable *)
    18   | B of int (* Named(!!) Bound Variables *)
    19   | A of nterm*nterm (* Application *)
    20   | AbsN of int*nterm ; (* Binding of named Variables *)
    21 
    22 datatype Univ = 
    23     Constr of string*(Univ list)       (* Named Constructors *)
    24   | Var of string*(Univ list)          (* Free variables *)
    25   | BVar of int*(Univ list)            (* Bound named variables *)
    26   | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    27                                             (* Functions *)
    28 val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
    29 
    30 val apply: Univ -> Univ -> Univ;
    31 val to_term: Univ -> nterm;
    32 
    33 val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
    34 val new_name: unit -> int;
    35 
    36 (* For testing
    37 val eval: term -> (Univ list) -> Univ
    38 *)
    39 
    40 end;
    41 
    42 (* FIXME add_funs and relatives should NOT be exported. Eventually it
    43 should work like for quickcheck: Eval generates code which leaves the
    44 function values in a public reference variable, the code is executed,
    45 and the value of the reference variable is added to the internal
    46 tables, all in one go, w/o interruption. *)
    47 
    48 
    49 structure NBE_Eval:NBE_EVAL =
    50 struct
    51 
    52 datatype nterm =
    53     C of string (* Named Constants *)
    54   | V of string (* Free Variable *)
    55   | B of int (* Named(!!) Variables *)
    56   | A of nterm * nterm (* Application *)
    57   | AbsN of int * nterm (* Binding of named Variables *);
    58 
    59 fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
    60 
    61 (* ------------------------------ The semantical universe --------------------- *)
    62 
    63 (*
    64    Functions are given by their semantical function value. To avoid
    65    trouble with the ML-type system, these functions have the most
    66    generic type, that is "Univ list -> Univ". The calling convention is
    67    that the arguments come as a list, the last argument first. In
    68    other words, a function call that usually would look like
    69 
    70    f x_1 x_2 ... x_n   or   f(x_1,x_2, ..., x_n)
    71 
    72    would be in our convention called as
    73 
    74               f [x_n,..,x_2,x_1]
    75 
    76    Moreover, to handle functions that are still waiting for some
    77    arguments we have additionally a list of arguments collected to far
    78    and the number of arguments we're still waiting for.
    79 
    80    Finally, it might happen, that a function does not get all the
    81    arguments it needs. In this case the function must provide means to
    82    present itself as a string. As this might be a heavy-wight
    83    operation, we delay it.
    84 *)
    85 
    86 datatype Univ = 
    87     Constr of string*(Univ list)       (* Named Constructors *)
    88   | Var of string*(Univ list)          (* Free variables *)
    89   | BVar of int*(Univ list)         (* Bound named variables *)
    90   | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    91 
    92 fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
    93   |	to_term (Var   (name, args))    = apps (V name) (map to_term args)
    94   |	to_term (BVar  (name, args))    = apps (B name) (map to_term args)
    95   |	to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    96 
    97 (*
    98    A typical operation, why functions might be good for, is
    99    application. Moreover, functions are the only values that can
   100    reasonably we applied in a semantical way.
   101 *)
   102 
   103 fun  apply (Fun(f,xs,1,name))  x = f (x::xs)
   104    | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   105    | apply (Constr(name,args)) x = Constr(name,x::args)
   106    | apply (Var(name,args))    x = Var(name,x::args)
   107    | apply (BVar(name,args))   x = BVar(name,x::args);
   108 
   109 fun mk_Fun(name,v,0) = (name,v [])
   110   | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
   111 
   112 (* ---------------- table with the meaning of constants -------------------- *)
   113 
   114 val xfun_tab: Univ Symtab.table ref = ref Symtab.empty;
   115 
   116 fun lookup s = case Symtab.lookup (!xfun_tab) s of
   117     SOME x => x
   118   | NONE   => Constr(s,[]);
   119 
   120 (* ------------------ evaluation with greetings to Tarski ------------------ *)
   121 
   122 (* generation of fresh names *)
   123 
   124 val counter = ref 0;
   125 
   126 fun new_name() = (counter := !counter +1; !counter);
   127 
   128 (* greetings to Tarski *)
   129 
   130 structure IL = CodegenThingol
   131 
   132 fun eval(IL.IConst((f,_),_)) xs = lookup f
   133   | eval(IL.IVarE(n,_)) xs =
   134       (case AList.lookup (op =) xs n of NONE => Var(n,[])
   135        | SOME v => v)
   136   | eval(IL.IApp(s,t)) xs = apply (eval s xs) (eval t xs)
   137   | eval(IL.IAbs(IL.IVarE(n,_), t)) xs =
   138       Fun (fn [x] => eval t ((n,x)::xs), [], 1,
   139            fn () => let val var = new_name() in
   140                  AbsN(var, to_term (eval t ((n,BVar(var,[])) :: xs))) end);
   141 
   142 
   143 (* finally... *)
   144 
   145 fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval t []));
   146 
   147 end;