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