From f750e27d0e16da032227dbc71ecb7c63f5b77bc7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 21 Oct 2008 09:50:19 -0400 Subject: Binops; equality tested on int; lame 404 substitute --- src/cjr.sml | 3 +++ src/cjr_print.sml | 21 +++++++++++++++++++++ src/cjrize.sml | 14 ++++++++++++++ src/mono.sml | 3 +++ src/mono_print.sml | 9 +++++++++ src/mono_reduce.sml | 6 ++++++ src/mono_util.sml | 11 +++++++++++ src/monoize.sml | 39 +++++++++++++++++++++++++++++++++++++++ src/prepare.sml | 14 ++++++++++++++ tests/eq.ur | 11 ++++------- tests/eq.urp | 3 +++ 11 files changed, 127 insertions(+), 7 deletions(-) create mode 100644 tests/eq.urp diff --git a/src/cjr.sml b/src/cjr.sml index 8dca6b46..dc700a56 100644 --- a/src/cjr.sml +++ b/src/cjr.sml @@ -66,6 +66,9 @@ datatype exp' = | 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 --git a/src/cjr_print.sml b/src/cjr_print.sml index aee23717..5f430ccf 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -609,6 +609,25 @@ fun p_exp' par env (e, loc) = 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 @@ fun p_file env (ds, ps) = newline, p_list_sep newline (fn x => x) pds', newline, + string "uw_error(ctx, FATAL, \"Unknown page\");", + newline, string "}", newline, newline, diff --git a/src/cjrize.sml b/src/cjrize.sml index 606be3eb..05ceb0f9 100644 --- a/src/cjrize.sml +++ b/src/cjrize.sml @@ -249,6 +249,20 @@ fun cifyExp (eAll as (e, loc), sm) = 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 --git a/src/mono.sml b/src/mono.sml index 4742c541..b7ac6346 100644 --- a/src/mono.sml +++ b/src/mono.sml @@ -67,6 +67,9 @@ datatype exp' = | 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 --git a/src/mono_print.sml b/src/mono_print.sml index f7adfd70..5d9f8007 100644 --- a/src/mono_print.sml +++ b/src/mono_print.sml @@ -158,6 +158,15 @@ fun p_exp' par env (e, _) = 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 --git a/src/mono_reduce.sml b/src/mono_reduce.sml index e288e34e..e97f3461 100644 --- a/src/mono_reduce.sml +++ b/src/mono_reduce.sml @@ -54,6 +54,9 @@ fun impure (e, _) = | 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 @@ fun summarize d (e, _) = | 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 --git a/src/mono_util.sml b/src/mono_util.sml index a56e5287..080c3dc9 100644 --- a/src/mono_util.sml +++ b/src/mono_util.sml @@ -175,6 +175,17 @@ fun mapfoldB {typ = fc, exp = fe, bind} = 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 --git a/src/monoize.sml b/src/monoize.sml index 720a9485..7428b7fa 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -94,6 +94,12 @@ fun monoType env = | 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 @@ fun monoExp (env, st, fm) (all as (e, loc)) = 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 --git a/src/prepare.sml b/src/prepare.sml index 3c5aa2aa..6bf929f0 100644 --- a/src/prepare.sml +++ b/src/prepare.sml @@ -88,6 +88,20 @@ fun prepExp (e as (_, loc), sns) = ((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 --git a/tests/eq.ur b/tests/eq.ur index 14c50e3a..1a780a57 100644 --- a/tests/eq.ur +++ b/tests/eq.ur @@ -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 --git a/tests/eq.urp b/tests/eq.urp new file mode 100644 index 00000000..948e8684 --- /dev/null +++ b/tests/eq.urp @@ -0,0 +1,3 @@ +debug + +eq -- cgit v1.2.3