author | haftmann |
Tue, 07 Mar 2006 14:09:48 +0100 | |
changeset 19202 | 0b9eb4b0ad98 |
parent 19177 | 68c6824d8bb6 |
child 19795 | 746274ca400b |
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 |
|
19177 | 28 |
val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm; |
29 |
val apply: Univ -> Univ -> Univ; |
|
30 |
||
31 |
val to_term: Univ -> nterm; |
|
19147 | 32 |
|
19177 | 33 |
val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ; |
34 |
val new_name: unit -> int; |
|
19116 | 35 |
|
19177 | 36 |
(* For testing |
37 |
val eval: (Univ list) -> term -> Univ |
|
38 |
*) |
|
19116 | 39 |
end; |
40 |
||
19177 | 41 |
structure NBE_Eval: NBE_EVAL = |
19116 | 42 |
struct |
43 |
||
44 |
datatype nterm = |
|
19177 | 45 |
C of string |
46 |
| V of string |
|
47 |
| B of int |
|
48 |
| A of nterm * nterm |
|
49 |
| AbsN of int * nterm; |
|
19116 | 50 |
|
51 |
fun apps t args = foldr (fn (y,x) => A(x,y)) t args; |
|
52 |
||
53 |
(* ------------------------------ The semantical universe --------------------- *) |
|
54 |
||
55 |
(* |
|
56 |
Functions are given by their semantical function value. To avoid |
|
57 |
trouble with the ML-type system, these functions have the most |
|
58 |
generic type, that is "Univ list -> Univ". The calling convention is |
|
59 |
that the arguments come as a list, the last argument first. In |
|
60 |
other words, a function call that usually would look like |
|
61 |
||
62 |
f x_1 x_2 ... x_n or f(x_1,x_2, ..., x_n) |
|
63 |
||
64 |
would be in our convention called as |
|
65 |
||
66 |
f [x_n,..,x_2,x_1] |
|
67 |
||
68 |
Moreover, to handle functions that are still waiting for some |
|
69 |
arguments we have additionally a list of arguments collected to far |
|
70 |
and the number of arguments we're still waiting for. |
|
71 |
||
72 |
Finally, it might happen, that a function does not get all the |
|
73 |
arguments it needs. In this case the function must provide means to |
|
74 |
present itself as a string. As this might be a heavy-wight |
|
75 |
operation, we delay it. |
|
76 |
*) |
|
77 |
||
78 |
datatype Univ = |
|
79 |
Constr of string*(Univ list) (* Named Constructors *) |
|
80 |
| Var of string*(Univ list) (* Free variables *) |
|
81 |
| BVar of int*(Univ list) (* Bound named variables *) |
|
82 |
| Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm); |
|
83 |
||
84 |
fun to_term (Constr(name, args)) = apps (C name) (map to_term args) |
|
85 |
| to_term (Var (name, args)) = apps (V name) (map to_term args) |
|
86 |
| to_term (BVar (name, args)) = apps (B name) (map to_term args) |
|
87 |
| to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args); |
|
88 |
||
89 |
(* |
|
90 |
A typical operation, why functions might be good for, is |
|
91 |
application. Moreover, functions are the only values that can |
|
92 |
reasonably we applied in a semantical way. |
|
93 |
*) |
|
94 |
||
19177 | 95 |
fun apply (Fun(f,xs,1,name)) x = f (x::xs) |
96 |
| apply (Fun(f,xs,n,name)) x = Fun(f,x::xs,n-1,name) |
|
97 |
| apply (Constr(name,args)) x = Constr(name,x::args) |
|
98 |
| apply (Var(name,args)) x = Var(name,x::args) |
|
99 |
| apply (BVar(name,args)) x = BVar(name,x::args); |
|
19116 | 100 |
|
19147 | 101 |
fun mk_Fun(name,v,0) = (name,v []) |
102 |
| mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name)); |
|
103 |
||
19116 | 104 |
(* ---------------- table with the meaning of constants -------------------- *) |
105 |
||
19147 | 106 |
val xfun_tab: Univ Symtab.table ref = ref Symtab.empty; |
19116 | 107 |
|
19147 | 108 |
fun lookup s = case Symtab.lookup (!xfun_tab) s of |
19116 | 109 |
SOME x => x |
110 |
| NONE => Constr(s,[]); |
|
111 |
||
112 |
(* ------------------ evaluation with greetings to Tarski ------------------ *) |
|
113 |
||
114 |
(* generation of fresh names *) |
|
115 |
||
116 |
val counter = ref 0; |
|
117 |
||
19177 | 118 |
fun new_name () = (counter := !counter +1; !counter); |
19116 | 119 |
|
120 |
(* greetings to Tarski *) |
|
121 |
||
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
122 |
open BasicCodegenThingol; |
19147 | 123 |
|
19202 | 124 |
fun eval xs = |
125 |
let |
|
126 |
fun evl (IConst (c, _)) = lookup c |
|
127 |
| evl (IVar n) = |
|
128 |
AList.lookup (op =) xs n |
|
129 |
|> the_default (Var (n, [])) |
|
130 |
| evl (s `$ t) = apply (eval xs s) (eval xs t) |
|
131 |
| evl ((n, _) `|-> t) = |
|
132 |
Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t, |
|
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
133 |
[], 1, |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
134 |
fn () => let val var = new_name() in |
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
135 |
AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end) |
19202 | 136 |
in CodegenThingol.map_pure evl end; |
19116 | 137 |
|
138 |
(* finally... *) |
|
139 |
||
19167
f237c0cb3882
refined representation of codegen intermediate language
haftmann
parents:
19147
diff
changeset
|
140 |
fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t)); |
19116 | 141 |
|
142 |
end; |