# HG changeset patch # User Adam Chlipala # Date 1224597019 14400 # Node ID 7abb28e9d51fcba962557c874fa0296bde8d4af3 # Parent ef43ed6cd1de6c37da1a3012b7f37ee39b264355 Binops; equality tested on int; lame 404 substitute diff -r ef43ed6cd1de -r 7abb28e9d51f src/cjr.sml --- a/src/cjr.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/cjr.sml Tue Oct 21 09:50:19 2008 -0400 @@ -66,6 +66,9 @@ | EFfiApp of string * string * exp list | EApp of exp * exp list + | EUnop of string * exp + | EBinop of string * exp * exp + | ERecord of int * (string * exp) list | EField of exp * string diff -r ef43ed6cd1de -r 7abb28e9d51f src/cjr_print.sml --- a/src/cjr_print.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/cjr_print.sml Tue Oct 21 09:50:19 2008 -0400 @@ -609,6 +609,25 @@ p_list_sep (box [string ",", space]) (p_exp env) args, string ")"]) + | EUnop (s, e1) => + parenIf par (box [string s, + space, + p_exp' true env e1]) + + | EBinop ("!strcmp", e1, e2) => + box [string "!strcmp(", + p_exp env e1, + string ",", + space, + p_exp env e2, + string ")"] + | EBinop (s, e1, e2) => + parenIf par (box [p_exp' true env e1, + space, + string s, + space, + p_exp' true env e2]) + | ERecord (i, xes) => box [string "({", space, string "struct", @@ -2060,6 +2079,8 @@ newline, p_list_sep newline (fn x => x) pds', newline, + string "uw_error(ctx, FATAL, \"Unknown page\");", + newline, string "}", newline, newline, diff -r ef43ed6cd1de -r 7abb28e9d51f src/cjrize.sml --- a/src/cjrize.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/cjrize.sml Tue Oct 21 09:50:19 2008 -0400 @@ -249,6 +249,20 @@ Print.prefaces' [("Function", MonoPrint.p_exp MonoEnv.empty eAll)]; (dummye, sm)) + | L.EUnop (s, e1) => + let + val (e1, sm) = cifyExp (e1, sm) + in + ((L'.EUnop (s, e1), loc), sm) + end + | L.EBinop (s, e1, e2) => + let + val (e1, sm) = cifyExp (e1, sm) + val (e2, sm) = cifyExp (e2, sm) + in + ((L'.EBinop (s, e1, e2), loc), sm) + end + | L.ERecord xes => let val old_xts = map (fn (x, _, t) => (x, t)) xes diff -r ef43ed6cd1de -r 7abb28e9d51f src/mono.sml --- a/src/mono.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/mono.sml Tue Oct 21 09:50:19 2008 -0400 @@ -67,6 +67,9 @@ | EApp of exp * exp | EAbs of string * typ * typ * exp + | EUnop of string * exp + | EBinop of string * exp * exp + | ERecord of (string * exp * typ) list | EField of exp * string diff -r ef43ed6cd1de -r 7abb28e9d51f src/mono_print.sml --- a/src/mono_print.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/mono_print.sml Tue Oct 21 09:50:19 2008 -0400 @@ -158,6 +158,15 @@ space, p_exp (E.pushERel env x t NONE) e]) + | EUnop (s, e) => parenIf true (box [string s, + space, + p_exp' true env e]) + | EBinop (s, e1, e2) => parenIf true (box [p_exp' true env e1, + space, + string s, + space, + p_exp' true env e2]) + | ERecord xes => box [string "{", p_list (fn (x, e, _) => box [string x, diff -r ef43ed6cd1de -r 7abb28e9d51f src/mono_reduce.sml --- a/src/mono_reduce.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/mono_reduce.sml Tue Oct 21 09:50:19 2008 -0400 @@ -54,6 +54,9 @@ | EApp ((EFfi _, _), _) => false | EApp _ => true + | EUnop (_, e) => impure e + | EBinop (_, e1, e2) => impure e1 orelse impure e2 + | ERecord xes => List.exists (fn (_, e, _) => impure e) xes | EField (e, _) => impure e @@ -233,6 +236,9 @@ | EApp _ => [Unsure] | EAbs _ => [] + | EUnop (_, e) => summarize d e + | EBinop (_, e1, e2) => summarize d e1 @ summarize d e2 + | ERecord xets => List.concat (map (summarize d o #2) xets) | EField (e, _) => summarize d e diff -r ef43ed6cd1de -r 7abb28e9d51f src/mono_util.sml --- a/src/mono_util.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/mono_util.sml Tue Oct 21 09:50:19 2008 -0400 @@ -175,6 +175,17 @@ fn e' => (EAbs (x, dom', ran', e'), loc)))) + | EUnop (s, e) => + S.map2 (mfe ctx e, + fn e' => + (EUnop (s, e'), loc)) + | EBinop (s, e1, e2) => + S.bind2 (mfe ctx e1, + fn e1' => + S.map2 (mfe ctx e2, + fn e2' => + (EBinop (s, e1', e2'), loc))) + | ERecord xes => S.map2 (ListUtil.mapfold (fn (x, e, t) => S.bind2 (mfe ctx e, diff -r ef43ed6cd1de -r 7abb28e9d51f src/monoize.sml --- a/src/monoize.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/monoize.sml Tue Oct 21 09:50:19 2008 -0400 @@ -94,6 +94,12 @@ | L.CApp ((L.CFfi ("Basis", "option"), _), t) => (L'.TOption (mt env dtmap t), loc) + | L.CApp ((L.CFfi ("Basis", "eq"), _), t) => + let + val t = mt env dtmap t + in + (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc) + end | L.CApp ((L.CFfi ("Basis", "show"), _), t) => (L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc) | L.CApp ((L.CFfi ("Basis", "read"), _), t) => @@ -492,6 +498,39 @@ end | L.ECon _ => poly () + | L.ECApp ((L.EFfi ("Basis", "eq"), _), t) => + let + val t = monoType env t + val b = (L'.TFfi ("Basis", "bool"), loc) + val dom = (L'.TFun (t, (L'.TFun (t, b), loc)), loc) + in + ((L'.EAbs ("f", dom, dom, + (L'.ERel 0, loc)), loc), fm) + end + | L.ECApp ((L.EFfi ("Basis", "ne"), _), t) => + let + val t = monoType env t + val b = (L'.TFfi ("Basis", "bool"), loc) + val dom = (L'.TFun (t, (L'.TFun (t, b), loc)), loc) + in + ((L'.EAbs ("f", dom, dom, + (L'.EAbs ("x", t, (L'.TFun (t, b), loc), + (L'.EAbs ("y", t, b, + (L'.EUnop ("!", (L'.EApp ((L'.EApp ((L'.ERel 2, loc), + (L'.ERel 1, loc)), loc), + (L'.ERel 0, loc)), loc)), loc)), + loc)), + loc)), + loc), fm) + end + | L.EFfi ("Basis", "eq_int") => + ((L'.EAbs ("x", (L'.TFfi ("Basis", "int"), loc), + (L'.TFun ((L'.TFfi ("Basis", "int"), loc), (L'.TFfi ("Basis", "bool"), loc)), loc), + (L'.EAbs ("y", (L'.TFfi ("Basis", "int"), loc), + (L'.TFfi ("Basis", "bool"), loc), + (L'.EBinop ("==", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc), + fm) + | L.ECApp ((L.EFfi ("Basis", "show"), _), t) => let val t = monoType env t diff -r ef43ed6cd1de -r 7abb28e9d51f src/prepare.sml --- a/src/prepare.sml Sun Oct 19 16:49:09 2008 -0400 +++ b/src/prepare.sml Tue Oct 21 09:50:19 2008 -0400 @@ -88,6 +88,20 @@ ((EApp (e1, es), loc), sns) end + | EUnop (s, e1) => + let + val (e1, sns) = prepExp (e1, sns) + in + ((EUnop (s, e1), loc), sns) + end + | EBinop (s, e1, e2) => + let + val (e1, sns) = prepExp (e1, sns) + val (e2, sns) = prepExp (e2, sns) + in + ((EBinop (s, e1, e2), loc), sns) + end + | ERecord (rn, xes) => let val (xes, sns) = ListUtil.foldlMap (fn ((x, e), sns) => diff -r ef43ed6cd1de -r 7abb28e9d51f tests/eq.ur --- a/tests/eq.ur Sun Oct 19 16:49:09 2008 -0400 +++ b/tests/eq.ur Tue Oct 21 09:50:19 2008 -0400 @@ -1,7 +1,4 @@ -val b1 = 1 = 1 -val b2 = "Good" = "Bad" - -fun eq_pair (t1 :: Type) (t2 :: Type) (eq1 : eq t1) (eq2 : eq t2) (x : t1 * t2) (y : t1 * t2) = - x.1 = y.1 - -val b3 = True <> False +fun main () : transaction page = return + {txt _ (1 = 1)}, {txt _ (1 = 2)}
+ {txt _ (1 <> 1)}, {txt _ (1 <> 2)} +
diff -r ef43ed6cd1de -r 7abb28e9d51f tests/eq.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/eq.urp Tue Oct 21 09:50:19 2008 -0400 @@ -0,0 +1,3 @@ +debug + +eq