author | haftmann |
Fri, 10 Aug 2007 17:04:34 +0200 | |
changeset 24219 | e558fe311376 |
parent 23397 | 2cc3352f6c3c |
permissions | -rwxr-xr-x |
20856 | 1 |
(* Title: Pure/nbe_codegen.ML |
2 |
ID: $Id$ |
|
19177 | 3 |
Author: Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen |
4 |
||
5 |
Code generator for "normalization by evaluation". |
|
19116 | 6 |
*) |
7 |
||
8 |
(* Global asssumptions: |
|
9 |
For each function: there is at least one defining eqns and |
|
10 |
all defining equations have same number of arguments. |
|
11 |
||
12 |
FIXME |
|
19147 | 13 |
fun MLname |
19116 | 14 |
val quote = quote; |
15 |
||
16 |
*) |
|
17 |
||
19118 | 18 |
signature NBE_CODEGEN = |
19 |
sig |
|
20846 | 20 |
val generate: theory -> (string -> bool) -> (string * thm list) list -> string option; |
19177 | 21 |
val nterm_to_term: theory -> NBE_Eval.nterm -> term; |
19118 | 22 |
end |
23 |
||
24 |
||
25 |
structure NBE_Codegen: NBE_CODEGEN = |
|
26 |
struct |
|
27 |
||
19116 | 28 |
val Eval = "NBE_Eval"; |
19147 | 29 |
val Eval_mk_Fun = Eval ^ ".mk_Fun"; |
19116 | 30 |
val Eval_apply = Eval ^ ".apply"; |
31 |
val Eval_Constr = Eval ^ ".Constr"; |
|
32 |
val Eval_C = Eval ^ ".C"; |
|
33 |
val Eval_AbsN = Eval ^ ".AbsN"; |
|
34 |
val Eval_Fun = Eval ^ ".Fun"; |
|
35 |
val Eval_BVar = Eval ^ ".BVar"; |
|
36 |
val Eval_new_name = Eval ^ ".new_name"; |
|
37 |
val Eval_to_term = Eval ^ ".to_term"; |
|
38 |
||
19147 | 39 |
fun MLname s = "nbe_" ^ translate_string (fn "." => "_" | c => c) s; |
19116 | 40 |
fun MLvname s = "v_" ^ MLname s; |
41 |
fun MLparam n = "p_" ^ string_of_int n; |
|
42 |
fun MLintern s = "i_" ^ MLname s; |
|
43 |
||
44 |
fun MLparams n = map MLparam (1 upto n); |
|
45 |
||
46 |
structure S = |
|
47 |
struct |
|
48 |
||
49 |
val quote = quote; (* FIXME *) |
|
50 |
||
51 |
fun app e1 e2 = "(" ^ e1 ^ " " ^ e2 ^ ")"; |
|
52 |
fun abs v e = "(fn" ^ v ^ " => " ^ e ^ ")"; |
|
53 |
fun tup es = "(" ^ commas es ^ ")"; |
|
54 |
fun list es = "[" ^ commas es ^ "]"; |
|
55 |
||
56 |
fun apps s ss = Library.foldl (uncurry app) (s, ss); |
|
57 |
fun nbe_apps s ss = |
|
58 |
Library.foldr (fn (s,e) => app (app Eval_apply e) s) (ss,s); |
|
59 |
||
60 |
fun eqns name ees = |
|
61 |
let fun eqn (es,e) = name ^ " " ^ space_implode " " es ^ " = " ^ e |
|
20846 | 62 |
in space_implode "\n | " (map eqn ees) end; |
19116 | 63 |
|
20846 | 64 |
fun eqnss (es :: ess) = prefix "fun " es :: map (prefix "and ") ess |
65 |
|> space_implode "\n" |
|
66 |
|> suffix "\n"; |
|
19116 | 67 |
|
68 |
fun Val v s = "val " ^ v ^ " = " ^ s; |
|
69 |
fun Let ds e = "let\n" ^ (space_implode "\n" ds) ^ " in " ^ e ^ " end" |
|
70 |
||
71 |
end |
|
72 |
||
19177 | 73 |
val tab_lookup = S.app "NBE.lookup"; |
74 |
val tab_update = S.app "NBE.update"; |
|
19147 | 75 |
|
19116 | 76 |
fun mk_nbeFUN(nm,e) = |
23397 | 77 |
S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1" (*, |
19116 | 78 |
S.abs(S.tup [])(S.Let |
79 |
[S.Val (MLintern "var") (S.app Eval_new_name (S.tup [])), |
|
80 |
S.Val (MLvname nm) (S.app Eval_BVar (S.tup [(MLintern "var"), S.list []]))] |
|
23397 | 81 |
(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))*)]); |
19116 | 82 |
|
83 |
fun take_last n xs = rev (Library.take(n, rev xs)); |
|
84 |
fun drop_last n xs = rev (Library.drop(n, rev xs)); |
|
85 |
||
86 |
fun selfcall nm ar args = |
|
87 |
if (ar <= length args) then |
|
88 |
S.nbe_apps (S.app (MLname nm) (S.list (take_last ar args))) |
|
89 |
(drop_last ar args) |
|
23397 | 90 |
else S.app Eval_Fun (S.tup [MLname nm,S.list args(*, |
19116 | 91 |
string_of_int(ar - (length args)), |
23397 | 92 |
S.abs (S.tup []) (S.app Eval_C (S.quote nm))*)]); |
19116 | 93 |
|
20846 | 94 |
fun mk_rexpr defined names ar = |
19202 | 95 |
let |
20846 | 96 |
fun mk args (Const (c, _)) = |
97 |
if member (op =) names c then selfcall c ar args |
|
98 |
else if defined c then S.nbe_apps (MLname c) args |
|
99 |
else S.app Eval_Constr (S.tup [S.quote c, S.list args]) |
|
100 |
| mk args (Free (v, _)) = S.nbe_apps (MLvname v) args |
|
101 |
| mk args (t1 $ t2) = mk (args @ [mk [] t2]) t1 |
|
102 |
| mk args (Abs (v, _, t)) = S.nbe_apps (mk_nbeFUN (v, mk [] t)) args; |
|
19116 | 103 |
in mk [] end; |
104 |
||
105 |
val mk_lexpr = |
|
19202 | 106 |
let |
20846 | 107 |
fun mk args (Const (c, _)) = |
19202 | 108 |
S.app Eval_Constr (S.tup [S.quote c, S.list args]) |
20846 | 109 |
| mk args (Free (v, _)) = if null args then MLvname v else |
19202 | 110 |
sys_error "NBE mk_lexpr illegal higher order pattern" |
20846 | 111 |
| mk args (t1 $ t2) = mk (args @ [mk [] t2]) t1 |
112 |
| mk args (Abs _) = |
|
19202 | 113 |
sys_error "NBE mk_lexpr illegal pattern"; |
19116 | 114 |
in mk [] end; |
115 |
||
19147 | 116 |
fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm)); |
19116 | 117 |
|
20846 | 118 |
fun generate thy defined [(_, [])] = NONE |
119 |
| generate thy defined raw_eqnss = |
|
19177 | 120 |
let |
20846 | 121 |
val eqnss0 = map (fn (name, thms as thm :: _) => |
122 |
(name, ((length o snd o strip_comb o fst o Logic.dest_equals o prop_of) thm, |
|
123 |
map (apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify |
|
124 |
o prop_of) thms))) |
|
125 |
raw_eqnss; |
|
126 |
val eqnss = (map o apsnd o apsnd o map) (fn (args, t) => |
|
127 |
(map (NBE_Eval.prep_term thy) args, NBE_Eval.prep_term thy t)) eqnss0 |
|
128 |
val names = map fst eqnss; |
|
129 |
val used_funs = |
|
19202 | 130 |
[] |
20846 | 131 |
|> fold (fold (fold_aterms (fn Const (c, _) => insert (op =) c |
132 |
| _ => I)) o map snd o snd o snd) eqnss |
|
133 |
|> subtract (op =) names; |
|
134 |
fun mk_def (name, (ar, eqns)) = |
|
135 |
let |
|
136 |
fun mk_eqn (args, t) = ([S.list (map mk_lexpr (rev args))], |
|
137 |
mk_rexpr defined names ar t); |
|
138 |
val default_params = (S.list o rev o MLparams) ar; |
|
139 |
val default_eqn = ([default_params], S.app Eval_Constr (S.tup [S.quote name, default_params])); |
|
140 |
in S.eqns (MLname name) (map mk_eqn eqns @ [default_eqn]) end; |
|
141 |
val globals = map lookup (filter defined used_funs); |
|
142 |
fun register (name, (ar, _)) = tab_update |
|
143 |
(S.app Eval_mk_Fun (S.tup [S.quote name, MLname name, string_of_int ar])) |
|
144 |
in SOME (S.Let (globals @ [S.eqnss (map mk_def eqnss)]) (space_implode "; " (map register eqnss))) end; |
|
19177 | 145 |
|
146 |
open NBE_Eval; |
|
147 |
||
148 |
fun nterm_to_term thy t = |
|
19116 | 149 |
let |
20856 | 150 |
fun to_term bounds (C s) tcount = |
151 |
let |
|
24219 | 152 |
val SOME (const as (c, _)) = CodeNames.const_rev thy s; |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
21883
diff
changeset
|
153 |
val ty = CodegenData.default_typ thy const; |
20856 | 154 |
val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty; |
155 |
val tcount' = tcount + maxidx_of_typ ty + 1; |
|
156 |
in (Const (c, ty'), tcount') end |
|
157 |
| to_term bounds (V s) tcount = (Free (s, dummyT), tcount) |
|
158 |
| to_term bounds (B i) tcount = (Bound (find_index (fn j => i = j) bounds), tcount) |
|
159 |
| to_term bounds (A (t1, t2)) tcount = |
|
160 |
tcount |
|
161 |
|> to_term bounds t1 |
|
162 |
||>> to_term bounds t2 |
|
163 |
|-> (fn (t1', t2') => pair (t1' $ t2')) |
|
164 |
| to_term bounds (AbsN (i, t)) tcount = |
|
165 |
tcount |
|
166 |
|> to_term (i :: bounds) t |
|
167 |
|-> (fn t' => pair (Abs ("u", dummyT, t'))); |
|
168 |
in fst (to_term [] t 0) end; |
|
19116 | 169 |
|
19118 | 170 |
end; |