src/Pure/Tools/nbe_eval.ML
changeset 19177 68c6824d8bb6
parent 19167 f237c0cb3882
child 19202 0b9eb4b0ad98
     1.1 --- a/src/Pure/Tools/nbe_eval.ML	Thu Mar 02 18:51:11 2006 +0100
     1.2 +++ b/src/Pure/Tools/nbe_eval.ML	Fri Mar 03 08:52:39 2006 +0100
     1.3 @@ -1,9 +1,9 @@
     1.4  (*  ID:         $Id$
     1.5 -    Author:     Klaus Aehlig, Tobias Nipkow
     1.6 +    Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
     1.7 +
     1.8 +Evaluator infrastructure for "normalization by evaluation".
     1.9  *)
    1.10  
    1.11 -(* ------------------------------ Evaluator  ------------------------------ *)
    1.12 -
    1.13  (* Optimizations:
    1.14   int instead of string in Constr
    1.15   treat int via ML ints
    1.16 @@ -11,50 +11,42 @@
    1.17  
    1.18  signature NBE_EVAL =
    1.19  sig
    1.20 -(* named terms used for output only *)
    1.21 -datatype nterm =
    1.22 -    C of string (* Named Constants *)
    1.23 -  | V of string (* Free Variable *)
    1.24 -  | B of int (* Named(!!) Bound Variables *)
    1.25 -  | A of nterm*nterm (* Application *)
    1.26 -  | AbsN of int*nterm ; (* Binding of named Variables *)
    1.27 +  (*named terms used for output only*)
    1.28 +  datatype nterm =
    1.29 +      C of string         (*named constants*)
    1.30 +    | V of string         (*free variable*)
    1.31 +    | B of int            (*named(!!) bound variables*)
    1.32 +    | A of nterm * nterm  (*application*)
    1.33 +    | AbsN of int * nterm (*binding of named variables*);
    1.34 +  datatype Univ = 
    1.35 +      Constr of string*(Univ list)       (*named constructors*)
    1.36 +    | Var of string*(Univ list)          (*free variables*)
    1.37 +    | BVar of int*(Univ list)            (*bound named variables*)
    1.38 +    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
    1.39 +                                         (*functions*);
    1.40  
    1.41 -datatype Univ = 
    1.42 -    Constr of string*(Univ list)       (* Named Constructors *)
    1.43 -  | Var of string*(Univ list)          (* Free variables *)
    1.44 -  | BVar of int*(Univ list)            (* Bound named variables *)
    1.45 -  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    1.46 -                                            (* Functions *)
    1.47 -val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
    1.48 +  val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm;
    1.49 +  val apply: Univ -> Univ -> Univ;
    1.50 +
    1.51 +  val to_term: Univ -> nterm;
    1.52  
    1.53 -val apply: Univ -> Univ -> Univ;
    1.54 -val to_term: Univ -> nterm;
    1.55 +  val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ;
    1.56 +  val new_name: unit -> int;
    1.57  
    1.58 -val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
    1.59 -val new_name: unit -> int;
    1.60 -
    1.61 -(* For testing
    1.62 -val eval: term -> (Univ list) -> Univ
    1.63 -*)
    1.64 -
    1.65 +  (* For testing
    1.66 +  val eval: (Univ list) -> term -> Univ
    1.67 +  *)
    1.68  end;
    1.69  
    1.70 -(* FIXME add_funs and relatives should NOT be exported. Eventually it
    1.71 -should work like for quickcheck: Eval generates code which leaves the
    1.72 -function values in a public reference variable, the code is executed,
    1.73 -and the value of the reference variable is added to the internal
    1.74 -tables, all in one go, w/o interruption. *)
    1.75 -
    1.76 -
    1.77 -structure NBE_Eval:NBE_EVAL =
    1.78 +structure NBE_Eval: NBE_EVAL =
    1.79  struct
    1.80  
    1.81  datatype nterm =
    1.82 -    C of string (* Named Constants *)
    1.83 -  | V of string (* Free Variable *)
    1.84 -  | B of int (* Named(!!) Variables *)
    1.85 -  | A of nterm * nterm (* Application *)
    1.86 -  | AbsN of int * nterm (* Binding of named Variables *);
    1.87 +    C of string
    1.88 +  | V of string
    1.89 +  | B of int
    1.90 +  | A of nterm * nterm
    1.91 +  | AbsN of int * nterm;
    1.92  
    1.93  fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
    1.94  
    1.95 @@ -100,11 +92,11 @@
    1.96     reasonably we applied in a semantical way.
    1.97  *)
    1.98  
    1.99 -fun  apply (Fun(f,xs,1,name))  x = f (x::xs)
   1.100 -   | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   1.101 -   | apply (Constr(name,args)) x = Constr(name,x::args)
   1.102 -   | apply (Var(name,args))    x = Var(name,x::args)
   1.103 -   | apply (BVar(name,args))   x = BVar(name,x::args);
   1.104 +fun apply (Fun(f,xs,1,name))  x = f (x::xs)
   1.105 +  | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   1.106 +  | apply (Constr(name,args)) x = Constr(name,x::args)
   1.107 +  | apply (Var(name,args))    x = Var(name,x::args)
   1.108 +  | apply (BVar(name,args))   x = BVar(name,x::args);
   1.109  
   1.110  fun mk_Fun(name,v,0) = (name,v [])
   1.111    | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
   1.112 @@ -123,7 +115,7 @@
   1.113  
   1.114  val counter = ref 0;
   1.115  
   1.116 -fun new_name() = (counter := !counter +1; !counter);
   1.117 +fun new_name () = (counter := !counter +1; !counter);
   1.118  
   1.119  (* greetings to Tarski *)
   1.120  
   1.121 @@ -142,7 +134,6 @@
   1.122    | eval xs (IAbs (_, t)) = eval xs t
   1.123    | eval xs (ICase (_, t)) = eval xs t;
   1.124  
   1.125 -
   1.126  (* finally... *)
   1.127  
   1.128  fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));