diff options
| -rw-r--r-- | lib/basis.urs | 10 | ||||
| -rw-r--r-- | src/elaborate.sml | 5 | ||||
| -rw-r--r-- | src/urweb.grm | 10 | ||||
| -rw-r--r-- | tests/eq.ur | 5 |
4 files changed, 28 insertions, 2 deletions
diff --git a/lib/basis.urs b/lib/basis.urs index f53ee1c1..bc4c9481 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -7,6 +7,16 @@ type unit = {} datatype bool = False | True +(** Basic type classes *) + +class eq +val eq : t ::: Type -> eq t -> t -> t -> bool +val eq_int : eq int +val eq_float : eq float +val eq_string : eq string +val eq_bool : eq bool + + (** SQL *) con sql_table :: {Type} -> Type diff --git a/src/elaborate.sml b/src/elaborate.sml index 9fa22026..27b3e3fe 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1584,11 +1584,12 @@ fun elabExp (env, denv) (eAll as (e, loc)) = checkKind env t' tk ktype; (t', gs) end - val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e + val (dom, gs2) = normClassConstraint (env, denv) t' + val (e', et, gs3) = elabExp (E.pushERel env x dom, denv) e in ((L'.EAbs (x, t', et, e'), loc), (L'.TFun (t', et), loc), - enD gs1 @ gs2) + enD gs1 @ enD gs2 @ gs3) end | L.ECApp (e, c) => let diff --git a/src/urweb.grm b/src/urweb.grm index aa062516..9d619fca 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -141,6 +141,15 @@ fun sql_relop (oper, sqlexp1, sqlexp2, loc) = (EApp (e, sqlexp2), loc) end +fun native_op (oper, e1, e2, loc) = + let + val e = (EVar (["Basis"], oper), loc) + val e = (EApp (e, (EWild, loc)), loc) + val e = (EApp (e, e1), loc) + in + (EApp (e, e2), loc) + end + %% %header (functor UrwebLrValsFn(structure Token : TOKEN)) @@ -595,6 +604,7 @@ eexp : eapps (eapps) in (EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc) end) + | eexp EQ eexp (native_op ("eq", eexp1, eexp2, s (eexp1left, eexp2right))) eargs : earg (earg) | eargl (eargl) diff --git a/tests/eq.ur b/tests/eq.ur new file mode 100644 index 00000000..0c5cde60 --- /dev/null +++ b/tests/eq.ur @@ -0,0 +1,5 @@ +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 |