Mercurial > urweb

changeset 256:e52243e20858

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'eq' type class
author Adam Chlipala <adamc@hcoop.net>
date Sun, 31 Aug 2008 15:15:41 -0400
parents 69d337f186eb
children 32f9212583b2
files lib/basis.urs src/elaborate.sml src/urweb.grm tests/eq.ur
diffstat 4 files changed, 28 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/lib/basis.urs	Sun Aug 31 15:04:10 2008 -0400
+++ b/lib/basis.urs	Sun Aug 31 15:15:41 2008 -0400
@@ -7,6 +7,16 @@
 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
--- a/src/elaborate.sml	Sun Aug 31 15:04:10 2008 -0400
+++ b/src/elaborate.sml	Sun Aug 31 15:15:41 2008 -0400
@@ -1584,11 +1584,12 @@
                                         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
--- a/src/urweb.grm	Sun Aug 31 15:04:10 2008 -0400
+++ b/src/urweb.grm	Sun Aug 31 15:15:41 2008 -0400
@@ -141,6 +141,15 @@
         (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 @@
                                          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)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/eq.ur	Sun Aug 31 15:15:41 2008 -0400
@@ -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