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