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