summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-08-19 15:23:01 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-08-19 15:23:01 -0400
commited93f02f2bad4c97b361025ebe851331f7640cad (patch)
tree49a42ce8909e7f3df3a9fe122d4da57b21f67108 /src
parent7144b7ff351ce55fe39d107342ba2778331700e6 (diff)
Basis.mkMonad
Diffstat (limited to 'src')
-rw-r--r--src/core_print.sml7
-rw-r--r--src/monoize.sml52
-rw-r--r--src/reduce.sml79
3 files changed, 103 insertions, 35 deletions
diff --git a/src/core_print.sml b/src/core_print.sml
index ca8066b3..8e46db04 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -281,7 +281,7 @@ fun p_exp' par env (e, _) =
| EApp (e1, e2) => parenIf par (box [p_exp' true env e1,
space,
p_exp' true env e2])
- | EAbs (x, t, _, e) => parenIf par (box [string "fn",
+ | EAbs (x, t, _, e) => parenIf par (box [string "(fn",
space,
string x,
space,
@@ -291,7 +291,8 @@ fun p_exp' par env (e, _) =
space,
string "=>",
space,
- p_exp (E.pushERel env x t) e])
+ p_exp (E.pushERel env x t) e,
+ string ")"])
| ECApp (e, c) => parenIf par (box [p_exp env e,
space,
string "[",
diff --git a/src/monoize.sml b/src/monoize.sml
index 337e198c..7849e1cd 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -1315,20 +1315,17 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
fm)
end
- | L.EFfi ("Basis", "transaction_monad") => ((L'.ERecord [], loc), fm)
- | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "return"), _), (L.CFfi ("Basis", "transaction"), _)), _), t) =>
+ | L.ECApp ((L.EFfi ("Basis", "transaction_return"), _), t) =>
let
val t = monoType env t
in
- ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (t, (L'.TFun ((L'.TRecord [], loc), t), loc)), loc),
- (L'.EAbs ("x", t,
+ ((L'.EAbs ("x", t,
(L'.TFun ((L'.TRecord [], loc), t), loc),
(L'.EAbs ("_", (L'.TRecord [], loc), t,
- (L'.ERel 1, loc)), loc)), loc)), loc),
+ (L'.ERel 1, loc)), loc)), loc),
fm)
end
- | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), (L.CFfi ("Basis", "transaction"), _)), _),
- t1), _), t2) =>
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "transaction_bind"), _), t1), _), t2) =>
let
val t1 = monoType env t1
val t2 = monoType env t2
@@ -1336,17 +1333,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
val mt1 = (L'.TFun (un, t1), loc)
val mt2 = (L'.TFun (un, t2), loc)
in
- ((L'.EAbs ("_", un,
- (L'.TFun (mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc)), loc)), loc),
- (L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc)), loc),
- (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc),
- (L'.EAbs ("_", un, un,
- (L'.ELet ("r", t1, (L'.EApp ((L'.ERel 2, loc),
- (L'.ERecord [], loc)), loc),
- (L'.EApp (
- (L'.EApp ((L'.ERel 2, loc), (L'.ERel 0, loc)), loc),
- (L'.ERecord [], loc)),
- loc)), loc)), loc)), loc)), loc)), loc),
+ ((L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc)), loc),
+ (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), (L'.TFun (un, un), loc),
+ (L'.EAbs ("_", un, un,
+ (L'.ELet ("r", t1, (L'.EApp ((L'.ERel 2, loc),
+ (L'.ERecord [], loc)), loc),
+ (L'.EApp (
+ (L'.EApp ((L'.ERel 2, loc), (L'.ERel 0, loc)), loc),
+ (L'.ERecord [], loc)),
+ loc)), loc)), loc)), loc)), loc),
fm)
end
@@ -1427,18 +1422,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
((L'.ESpawn e, loc), fm)
end
- | L.EFfi ("Basis", "signal_monad") => ((L'.ERecord [], loc), fm)
- | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "return"), _), (L.CFfi ("Basis", "signal"), _)), _), t) =>
+ | L.ECApp ((L.EFfi ("Basis", "signal_return"), _), t) =>
let
val t = monoType env t
in
- ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun (t, (L'.TSignal t, loc)), loc),
- (L'.EAbs ("x", t, (L'.TSignal t, loc),
- (L'.ESignalReturn (L'.ERel 0, loc), loc)), loc)), loc),
+ ((L'.EAbs ("x", t, (L'.TSignal t, loc),
+ (L'.ESignalReturn (L'.ERel 0, loc), loc)), loc),
fm)
end
- | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "bind"), _), (L.CFfi ("Basis", "signal"), _)), _),
- t1), _), t2) =>
+ | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "signal_bind"), _), t1), _), t2) =>
let
val t1 = monoType env t1
val t2 = monoType env t2
@@ -1446,11 +1438,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
val mt1 = (L'.TSignal t1, loc)
val mt2 = (L'.TSignal t2, loc)
in
- ((L'.EAbs ("_", un, (L'.TFun (mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), mt2), loc)), loc),
- (L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), mt2), loc),
- (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), mt2,
- (L'.ESignalBind ((L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc)),
- loc),
+ ((L'.EAbs ("m1", mt1, (L'.TFun ((L'.TFun (t1, mt2), loc), mt2), loc),
+ (L'.EAbs ("m2", (L'.TFun (t1, mt2), loc), mt2,
+ (L'.ESignalBind ((L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc),
fm)
end
| L.ECApp ((L.EFfi ("Basis", "signal"), _), t) =>
diff --git a/src/reduce.sml b/src/reduce.sml
index b2462695..9371e9bd 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -36,6 +36,12 @@ structure IM = IntBinaryMap
structure E = CoreEnv
+fun multiLiftConInCon n c =
+ if n = 0 then
+ c
+ else
+ multiLiftConInCon (n - 1) (E.liftConInCon 0 c)
+
fun multiLiftExpInExp n e =
if n = 0 then
e
@@ -204,6 +210,28 @@ fun match (env, p : pat, e : exp) =
match (env, p, e)
end
+fun returnType m loc =
+ (TCFun ("a", (KType, loc),
+ (TFun ((CRel 0, loc),
+ (CApp (multiLiftConInCon 1 m, (CRel 0, loc)), loc)), loc)), loc)
+
+fun bindType m loc =
+ (TCFun ("a", (KType, loc),
+ (TCFun ("b", (KType, loc),
+ (TFun ((CApp (multiLiftConInCon 2 m, (CRel 1, loc)), loc),
+ (TFun ((TFun ((CRel 1, loc),
+ (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)),
+ loc),
+ (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)), loc)),
+ loc)), loc)), loc)
+
+fun monadRecord m loc =
+ (TRecord (CRecord ((KType, loc),
+ [((CName "Return", loc),
+ returnType m loc),
+ ((CName "Bind", loc),
+ bindType m loc)]), loc), loc)
+
fun kindConAndExp (namedC, namedE) =
let
fun kind env (all as (k, loc)) =
@@ -273,10 +301,14 @@ fun kindConAndExp (namedC, namedE) =
(*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
find (n, env, 0, 0, 0)
end
+
| CNamed n =>
(case IM.find (namedC, n) of
NONE => all
| SOME c => c)
+
+ | CFfi ("Basis", "monad") => (CAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), monadRecord (CRel 0, loc) loc), loc)
+
| CFfi _ => all
| CApp (c1, c2) =>
let
@@ -415,6 +447,51 @@ fun kindConAndExp (namedC, namedE) =
| SOME e => e)
| ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
map (con env) cs, Option.map (exp env) eo), loc)
+
+ | EFfi ("Basis", "return") =>
+ (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
+ (ECAbs ("a", (KType, loc),
+ (EAbs ("m", monadRecord (CRel 1, loc) loc, returnType (CRel 1, loc) loc,
+ (ECApp ((EField ((ERel 0, loc), (CName "Return", loc),
+ {field = returnType (CRel 1, loc) loc,
+ rest = (CRecord ((KType, loc),
+ [((CName "Bind", loc), bindType (CRel 1, loc) loc)]),
+ loc)}), loc), (CRel 0, loc)), loc)), loc)), loc)), loc)
+
+ | EFfi ("Basis", "bind") =>
+ (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
+ (ECAbs ("a", (KType, loc),
+ (ECAbs ("b", (KType, loc),
+ (EAbs ("m", monadRecord (CRel 2, loc) loc, bindType (CRel 2, loc) loc,
+ (ECApp ((ECApp ((EField ((ERel 0, loc), (CName "Bind", loc),
+ {field = bindType (CRel 2, loc) loc,
+ rest = (CRecord ((KType, loc),
+ [((CName "Return", loc),
+ returnType (CRel 2, loc) loc)]),
+ loc)}), loc), (CRel 1, loc)), loc),
+ (CRel 0, loc)), loc)), loc)), loc)), loc)), loc)
+
+ | EFfi ("Basis", "mkMonad") =>
+ (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc),
+ (EAbs ("m", monadRecord (CRel 0, loc) loc, monadRecord (CRel 0, loc) loc,
+ (ERel 0, loc)), loc)), loc)
+
+ | EFfi ("Basis", "transaction_monad") =>
+ (ERecord [((CName "Return", loc),
+ (EFfi ("Basis", "transaction_return"), loc),
+ returnType (CFfi ("Basis", "transaction"), loc) loc),
+ ((CName "Bind", loc),
+ (EFfi ("Basis", "transaction_bind"), loc),
+ bindType (CFfi ("Basis", "transaction"), loc) loc)], loc)
+
+ | EFfi ("Basis", "signal_monad") =>
+ (ERecord [((CName "Return", loc),
+ (EFfi ("Basis", "signal_return"), loc),
+ returnType (CFfi ("Basis", "signal"), loc) loc),
+ ((CName "Bind", loc),
+ (EFfi ("Basis", "signal_bind"), loc),
+ bindType (CFfi ("Basis", "signal"), loc) loc)], loc)
+
| EFfi _ => all
| EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 05:39:07 +0000