diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-09-17 17:11:23 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-09-17 17:11:23 -0400 |
| commit | ee157f852b85fc9350619ad6266a74846fd6cdf6 (patch) | |
| tree | e331cb18c6b95e0eff9d5dc00133c88cec62613b /src/reduce.sml | |
| parent | 13e3b7139dcee90106332ff4fb5b3c63fcf4a892 (diff) | |
tail example working
Diffstat (limited to 'src/reduce.sml')
| -rw-r--r-- | src/reduce.sml | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/src/reduce.sml b/src/reduce.sml index 137dd02f..c2becb2b 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -456,6 +456,54 @@ fun kindConAndExp (namedC, namedE) = | EApp ((EApp + ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), + t1), + _), t2), _), + (EFfi ("Basis", "transaction_monad"), _)), _), + (ETailCall (n, es, (EAbs (_, _, _, ke), _), dom, ran), _)), _), + trans3) => + let + val e' = (EFfi ("Basis", "bind"), loc) + val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc) + val e' = (ECApp (e', dom), loc) + val e' = (ECApp (e', t2), loc) + val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc) + val e' = (EApp (e', ke), loc) + val e' = (EApp (e', E.liftExpInExp 0 trans3), loc) + val e' = reassoc e' + val e' = (EAbs ("x", dom, t2, e'), loc) + val e' = (ETailCall (n, es, e', dom, t2), loc) + in + e' + end + + | EApp + ((EApp + ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), + t1), + _), t2), _), + (EFfi ("Basis", "transaction_monad"), _)), _), + (ETailCall (n, es, ke, dom, ran), _)), _), + trans3) => + let + val e' = (EFfi ("Basis", "bind"), loc) + val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc) + val e' = (ECApp (e', dom), loc) + val e' = (ECApp (e', t2), loc) + val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc) + val e' = (EApp (e', exp (UnknownE :: env') + (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), + loc) + val e' = (EApp (e', E.liftExpInExp 0 trans3), loc) + val e' = reassoc e' + val e' = (EAbs ("x", dom, t2, e'), loc) + val e' = (ETailCall (n, es, e', dom, t2), loc) + in + e' + end + + | EApp + ((EApp ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt), _), _), _), t3), _), me), _), |