Mercurial > urweb

comparison src/reduce.sml @ 1544:a99b743a3087

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basis.mkMonad
author Adam Chlipala <adam@chlipala.net>
date Fri, 19 Aug 2011 15:23:01 -0400
parents 89d7b1c3199a
children 0577be31a435
comparison
equal deleted inserted replaced
1543:6f046b4bad24 1544:a99b743a3087
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
34 structure IS = IntBinarySet 34 structure IS = IntBinarySet
35 structure IM = IntBinaryMap 35 structure IM = IntBinaryMap
36 36
37 structure E = CoreEnv 37 structure E = CoreEnv
38 38
39 fun multiLiftConInCon n c =
40 if n = 0 then
41 c
42 else
43 multiLiftConInCon (n - 1) (E.liftConInCon 0 c)
44
39 fun multiLiftExpInExp n e = 45 fun multiLiftExpInExp n e =
40 if n = 0 then 46 if n = 0 then
41 e 47 e
42 else 48 else
43 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e) 49 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
201 207
202 | _ => Maybe 208 | _ => Maybe
203 in 209 in
204 match (env, p, e) 210 match (env, p, e)
205 end 211 end
212
213 fun returnType m loc =
214 (TCFun ("a", (KType, loc),
215 (TFun ((CRel 0, loc),
216 (CApp (multiLiftConInCon 1 m, (CRel 0, loc)), loc)), loc)), loc)
217
218 fun bindType m loc =
219 (TCFun ("a", (KType, loc),
220 (TCFun ("b", (KType, loc),
221 (TFun ((CApp (multiLiftConInCon 2 m, (CRel 1, loc)), loc),
222 (TFun ((TFun ((CRel 1, loc),
223 (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)),
224 loc),
225 (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)), loc)),
226 loc)), loc)), loc)
227
228 fun monadRecord m loc =
229 (TRecord (CRecord ((KType, loc),
230 [((CName "Return", loc),
231 returnType m loc),
232 ((CName "Bind", loc),
233 bindType m loc)]), loc), loc)
206 234
207 fun kindConAndExp (namedC, namedE) = 235 fun kindConAndExp (namedC, namedE) =
208 let 236 let
209 fun kind env (all as (k, loc)) = 237 fun kind env (all as (k, loc)) =
210 case k of 238 case k of
271 find (n' - 1, rest, nudge - 1, liftK, liftC) 299 find (n' - 1, rest, nudge - 1, liftK, liftC)
272 in 300 in
273 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) 301 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
274 find (n, env, 0, 0, 0) 302 find (n, env, 0, 0, 0)
275 end 303 end
304
276 | CNamed n => 305 | CNamed n =>
277 (case IM.find (namedC, n) of 306 (case IM.find (namedC, n) of
278 NONE => all 307 NONE => all
279 | SOME c => c) 308 | SOME c => c)
309
310 | CFfi ("Basis", "monad") => (CAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), monadRecord (CRel 0, loc) loc), loc)
311
280 | CFfi _ => all 312 | CFfi _ => all
281 | CApp (c1, c2) => 313 | CApp (c1, c2) =>
282 let 314 let
283 val c1 = con env c1 315 val c1 = con env c1
284 val c2 = con env c2 316 val c2 = con env c2
413 (case IM.find (namedE, n) of 445 (case IM.find (namedE, n) of
414 NONE => all 446 NONE => all
415 | SOME e => e) 447 | SOME e => e)
416 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, 448 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
417 map (con env) cs, Option.map (exp env) eo), loc) 449 map (con env) cs, Option.map (exp env) eo), loc)
450
451 | EFfi ("Basis", "return") =>
452 (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
453 (ECAbs ("a", (KType, loc),
454 (EAbs ("m", monadRecord (CRel 1, loc) loc, returnType (CRel 1, loc) loc,
455 (ECApp ((EField ((ERel 0, loc), (CName "Return", loc),
456 {field = returnType (CRel 1, loc) loc,
457 rest = (CRecord ((KType, loc),
458 [((CName "Bind", loc), bindType (CRel 1, loc) loc)]),
459 loc)}), loc), (CRel 0, loc)), loc)), loc)), loc)), loc)
460
461 | EFfi ("Basis", "bind") =>
462 (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
463 (ECAbs ("a", (KType, loc),
464 (ECAbs ("b", (KType, loc),
465 (EAbs ("m", monadRecord (CRel 2, loc) loc, bindType (CRel 2, loc) loc,
466 (ECApp ((ECApp ((EField ((ERel 0, loc), (CName "Bind", loc),
467 {field = bindType (CRel 2, loc) loc,
468 rest = (CRecord ((KType, loc),
469 [((CName "Return", loc),
470 returnType (CRel 2, loc) loc)]),
471 loc)}), loc), (CRel 1, loc)), loc),
472 (CRel 0, loc)), loc)), loc)), loc)), loc)), loc)
473
474 | EFfi ("Basis", "mkMonad") =>
475 (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
476 (EAbs ("m", monadRecord (CRel 0, loc) loc, monadRecord (CRel 0, loc) loc,
477 (ERel 0, loc)), loc)), loc)
478
479 | EFfi ("Basis", "transaction_monad") =>
480 (ERecord [((CName "Return", loc),
481 (EFfi ("Basis", "transaction_return"), loc),
482 returnType (CFfi ("Basis", "transaction"), loc) loc),
483 ((CName "Bind", loc),
484 (EFfi ("Basis", "transaction_bind"), loc),
485 bindType (CFfi ("Basis", "transaction"), loc) loc)], loc)
486
487 | EFfi ("Basis", "signal_monad") =>
488 (ERecord [((CName "Return", loc),
489 (EFfi ("Basis", "signal_return"), loc),
490 returnType (CFfi ("Basis", "signal"), loc) loc),
491 ((CName "Bind", loc),
492 (EFfi ("Basis", "signal_bind"), loc),
493 bindType (CFfi ("Basis", "signal"), loc) loc)], loc)
494
418 | EFfi _ => all 495 | EFfi _ => all
419 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) 496 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
420 497
421 (*| EApp ( 498 (*| EApp (
422 (EApp 499 (EApp