summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 11:04:24 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 11:04:24 -0400
commit52c51b876af9e05d8eec78c356419c0c4a811ff5 (patch)
tree64be28827149823a9f84eb7e5221f9bad07b0969 /src
parentce5158acc101774d5a264ae7154e9e0799e3848c (diff)
gt, ge
Diffstat (limited to 'src')
-rw-r--r--src/monoize.sml32
1 files changed, 32 insertions, 0 deletions
diff --git a/src/monoize.sml b/src/monoize.sml
index 8c9094b6..4e92c02e 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -683,6 +683,38 @@ fun monoExp (env, st, fm) (all as (e, loc)) =
((L'.EAbs ("r", ordTy t, (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc),
(L'.EField ((L'.ERel 0, loc), "Le"), loc)), loc), fm)
end
+ | L.ECApp ((L.EFfi ("Basis", "gt"), _), t) =>
+ let
+ val t = monoType env t
+ val b = (L'.TFfi ("Basis", "bool"), loc)
+ in
+ ((L'.EAbs ("f", ordTy t, (L'.TFun (t, (L'.TFun (t, b), loc)), loc),
+ (L'.EAbs ("x", t, (L'.TFun (t, b), loc),
+ (L'.EAbs ("y", t, b,
+ (L'.EUnop ("!",
+ (L'.EApp ((L'.EApp ((L'.EField ((L'.ERel 2, loc),
+ "Le"), loc),
+ (L'.ERel 1, loc)), loc),
+ (L'.ERel 0, loc)), loc)), loc)), loc)),
+ loc)),
+ loc), fm)
+ end
+ | L.ECApp ((L.EFfi ("Basis", "ge"), _), t) =>
+ let
+ val t = monoType env t
+ val b = (L'.TFfi ("Basis", "bool"), loc)
+ in
+ ((L'.EAbs ("f", ordTy t, (L'.TFun (t, (L'.TFun (t, b), loc)), loc),
+ (L'.EAbs ("x", t, (L'.TFun (t, b), loc),
+ (L'.EAbs ("y", t, b,
+ (L'.EUnop ("!",
+ (L'.EApp ((L'.EApp ((L'.EField ((L'.ERel 2, loc),
+ "Lt"), loc),
+ (L'.ERel 1, loc)), loc),
+ (L'.ERel 0, loc)), loc)), loc)), loc)),
+ loc)),
+ loc), fm)
+ end
| L.EFfi ("Basis", "ord_int") =>
let
fun intBin s =