diff options
Diffstat (limited to 'src/reduce.sml')
| -rw-r--r-- | src/reduce.sml | 79 |
1 files changed, 78 insertions, 1 deletions
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) |