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