141 |
| ("fixfix", _) => (fixfix f, fk, p) |
| ("fixfix", _) => (fixfix f, fk, p) |
142 |
| ("loopify", _) => (loopify f, fk, p) |
| ("loopify", _) => (loopify f, fk, p) |
143 |
| ("specialize",FK_NAMED) => (specialize f, fk, p) |
| ("specialize",FK_NAMED) => (specialize f, fk, p) |
|
| ("typelift",FK_DEBRUIJN) => (typelift f, fk, p) |
|
144 |
| ("wrap",FK_NAMED) => (wrapping f, FK_WRAP, p) |
| ("wrap",FK_NAMED) => (wrapping f, FK_WRAP, p) |
145 |
| ("reify",FK_WRAP) => (reify f, FK_REIFY, p) |
| ("reify",FK_WRAP) => (reify f, FK_REIFY, p) |
146 |
| ("deb2names",FK_DEBRUIJN) => (deb2names f, FK_NAMED, p) |
| ("deb2names",FK_DEBRUIJN) => (deb2names f, FK_NAMED, p) |
147 |
| ("names2deb",FK_NAMED) => (names2deb f, FK_DEBRUIJN, p) |
| ("names2deb",FK_NAMED) => (names2deb f, FK_DEBRUIJN, p) |
148 |
|
| ("typelift", _) => |
149 |
|
let val f' = typelift f |
150 |
|
in if !CTRL.check then wff(f', p) else (); (f', fk, p) end |
151 |
|
|
152 |
(* pseudo FLINT phases *) |
(* pseudo FLINT phases *) |
153 |
| ("id",_) => (f,fk,l) |
| ("id",_) => (f,fk,l) |
156 |
(say("\n\n[ After "^l^"... ]\n\n"); |
(say("\n\n[ After "^l^"... ]\n\n"); |
157 |
PPFlint.printFundec f; |
PPFlint.printFundec f; |
158 |
(f, fk, l) before say "\n") |
(f, fk, l) before say "\n") |
159 |
| ("wellformed",FK_DEBRUIJN) => (wff(f,l); (f,fk,p)) |
| ("wellformed",_) => (wff(f,l); (f,fk,p)) |
160 |
| ("check",_) => |
| ("check",_) => |
161 |
(check (ChkFlint.checkTop, PPFlint.printFundec, "FLINT") |
(check (ChkFlint.checkTop, PPFlint.printFundec, "FLINT") |
162 |
(ref true, fk = FK_REIFY, l) f; (f,fk,l)) |
(ref true, fk = FK_REIFY, l) f; (f,fk,l)) |
179 |
|
|
180 |
(* the "id" phase is just added to do the print/check at the entrance *) |
(* the "id" phase is just added to do the print/check at the entrance *) |
181 |
val (flint,fk,_) = foldl runphase' |
val (flint,fk,_) = foldl runphase' |
182 |
(flint, FK_DEBRUIJN, "flintnm") |
(deb2names flint, FK_NAMED, "flintnm") |
183 |
((* "id" :: *) !CTRL.phases) |
((* "id" :: *) !CTRL.phases) |
184 |
|
|
185 |
(* run any missing phases *) |
(* run any missing phases *) |
186 |
val (flint,fk) = |
val (flint,fk) = |
187 |
if fk = FK_NAMED |
if fk = FK_DEBRUIJN |
188 |
then (say "\n!!Forgot deb2names!!\n"; (deb2names flint, FK_DEBRUIJN)) |
then (say "\n!!Forgot deb2names!!\n"; (deb2names flint, FK_NAMED)) |
189 |
else (flint,fk) |
else (flint,fk) |
190 |
val (flint,fk) = |
val (flint,fk) = |
191 |
if fk = FK_DEBRUIJN |
if fk = FK_NAMED |
192 |
then (say "\n!!Forgot wrap!!\n"; (wrapping flint, FK_WRAP)) |
then (say "\n!!Forgot wrap!!\n"; (wrapping flint, FK_WRAP)) |
193 |
else (flint,fk) |
else (flint,fk) |
194 |
val (flint,fk) = |
val (flint,fk) = |