src/Pure/Tools/nbe_eval.ML
author haftmann
Tue Sep 19 15:22:03 2006 +0200 (2006-09-19)
changeset 20596 3950e65f48f8
parent 20105 454f4be984b7
child 20846 5fde744176d7
permissions -rwxr-xr-x
(void)
     1 (*  ID:         $Id$
     2     Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
     3 
     4 Evaluator infrastructure for "normalization by evaluation".
     5 *)
     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   datatype Univ = 
    22       Constr of string*(Univ list)       (*named constructors*)
    23     | Var of string*(Univ list)          (*free variables*)
    24     | BVar of int*(Univ list)            (*bound named variables*)
    25     | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
    26                                          (*functions*);
    27 
    28   val nbe: Univ Symtab.table -> CodegenThingol.iterm -> nterm
    29   val apply: Univ -> Univ -> Univ
    30 
    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   val string_of_nterm: nterm -> string
    37 end;
    38 
    39 structure NBE_Eval: NBE_EVAL =
    40 struct
    41 
    42 datatype nterm =
    43     C of string
    44   | V of string
    45   | B of int
    46   | A of nterm * nterm
    47   | AbsN of int * nterm;
    48 
    49 fun string_of_nterm(C s) = "(C \"" ^ s ^ "\")"
    50   | string_of_nterm(V s) = "(V \"" ^ s ^ "\")"
    51   | string_of_nterm(B n) = "(B " ^ string_of_int n ^ ")"
    52   | string_of_nterm(A(s,t)) =
    53        "(A " ^ string_of_nterm s ^ string_of_nterm t ^ ")"
    54   | string_of_nterm(AbsN(n,t)) =
    55       "(Abs " ^ string_of_int n ^ " " ^ string_of_nterm t ^ ")";
    56 
    57 fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
    58 
    59 (* ------------------------------ The semantical universe --------------------- *)
    60 
    61 (*
    62    Functions are given by their semantical function value. To avoid
    63    trouble with the ML-type system, these functions have the most
    64    generic type, that is "Univ list -> Univ". The calling convention is
    65    that the arguments come as a list, the last argument first. In
    66    other words, a function call that usually would look like
    67 
    68    f x_1 x_2 ... x_n   or   f(x_1,x_2, ..., x_n)
    69 
    70    would be in our convention called as
    71 
    72               f [x_n,..,x_2,x_1]
    73 
    74    Moreover, to handle functions that are still waiting for some
    75    arguments we have additionally a list of arguments collected to far
    76    and the number of arguments we're still waiting for.
    77 
    78    Finally, it might happen, that a function does not get all the
    79    arguments it needs. In this case the function must provide means to
    80    present itself as a string. As this might be a heavy-wight
    81    operation, we delay it.
    82 *)
    83 
    84 datatype Univ = 
    85     Constr of string*(Univ list)       (* Named Constructors *)
    86   | Var of string*(Univ list)          (* Free variables *)
    87   | BVar of int*(Univ list)         (* Bound named variables *)
    88   | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    89 
    90 fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
    91   | to_term (Var   (name, args))    = apps (V name) (map to_term args)
    92   | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
    93   | to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
    94 
    95 (*
    96    A typical operation, why functions might be good for, is
    97    application. Moreover, functions are the only values that can
    98    reasonably we applied in a semantical way.
    99 *)
   100 
   101 fun apply (Fun(f,xs,1,name))  x = f (x::xs)
   102   | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   103   | apply (Constr(name,args)) x = Constr(name,x::args)
   104   | apply (Var(name,args))    x = Var(name,x::args)
   105   | apply (BVar(name,args))   x = BVar(name,x::args);
   106 
   107 fun mk_Fun(name,v,0) = (name,v [])
   108   | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
   109 
   110 (* ---------------- table with the meaning of constants -------------------- *)
   111 
   112 val xfun_tab: Univ Symtab.table ref = ref Symtab.empty;
   113 
   114 fun lookup s = case Symtab.lookup (!xfun_tab) s of
   115     SOME x => x
   116   | NONE   => Constr(s,[]);
   117 
   118 (* ------------------ evaluation with greetings to Tarski ------------------ *)
   119 
   120 (* generation of fresh names *)
   121 
   122 val counter = ref 0;
   123 
   124 fun new_name () = (counter := !counter +1; !counter);
   125 
   126 (* greetings to Tarski *)
   127 
   128 open BasicCodegenThingol;
   129 
   130 fun eval xs =
   131   let
   132     fun evl (IConst (c, _)) = lookup c
   133       | evl (IVar n) =
   134           AList.lookup (op =) xs n
   135           |> the_default (Var (n, []))
   136       | evl (s `$ t) = apply (eval xs s) (eval xs t)
   137       | evl ((n, _) `|-> t) =
   138           Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t,
   139              [], 1,
   140              fn () => let val var = new_name() in
   141                  AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end)
   142   in CodegenThingol.map_pure evl end;
   143 
   144 (* finally... *)
   145 
   146 fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));
   147 
   148 end;