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