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