changeset 12:d89477f07c1e

Fun with records
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Mar 2008 17:34:57 -0400 (2008-03-28)
parents e97c6d335869
children 6049e2193bf2
files src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/lacweb.grm src/source.sml src/source_print.sml tests/stuff.lac
diffstat 8 files changed, 373 insertions(+), 55 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab.sml	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/elab.sml	Fri Mar 28 17:34:57 2008 -0400
@@ -72,6 +72,9 @@
        | ECApp of exp * con
        | ECAbs of explicitness * string * kind * exp
 
+       | ERecord of (con * exp) list
+       | EField of exp * con * { field : con, rest : con }
+
        | EError
 
 withtype exp = exp' located
--- a/src/elab_print.sml	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/elab_print.sml	Fri Mar 28 17:34:57 2008 -0400
@@ -115,15 +115,26 @@
 
       | CName s => box [string "#", string s]
 
-      | CRecord (k, xcs) => parenIf par (box [string "[",
-                                              p_list (fn (x, c) =>
-                                                         box [p_con env x,
-                                                              space,
-                                                              string "=",
-                                                              space,
-                                                              p_con env c]) xcs,
-                                              string "]::",
-                                              p_kind k])
+      | CRecord (k, xcs) =>
+        if !debug then
+            parenIf par (box [string "[",
+                              p_list (fn (x, c) =>
+                                         box [p_con env x,
+                                              space,
+                                              string "=",
+                                              space,
+                                              p_con env c]) xcs,
+                              string "]::",
+                              p_kind k])
+        else
+            parenIf par (box [string "[",
+                              p_list (fn (x, c) =>
+                                         box [p_con env x,
+                                              space,
+                                              string "=",
+                                              space,
+                                              p_con env c]) xcs,
+                              string "]"])
       | CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
                                               space,
                                               string "++",
@@ -181,6 +192,32 @@
                                                   space,
                                                   p_exp (E.pushCRel env x k) e])
 
+      | ERecord xes => box [string "{",
+                            p_list (fn (x, e) =>
+                                       box [p_con env x,
+                                            space,
+                                            string "=",
+                                            space,
+                                            p_exp env e]) xes,
+                            string "}"]
+      | EField (e, c, {field, rest}) =>
+        if !debug then
+            box [p_exp' true env e,
+                 string ".",
+                 p_con' true env c,
+                 space,
+                 string "[",
+                 p_con env field,
+                 space,
+                 string " in ",
+                 space,
+                 p_con env rest,
+                 string "]"]
+        else
+            box [p_exp' true env e,
+                 string ".",
+                 p_con' true env c]
+            
       | EError => string "<ERROR>"
 
 and p_exp env = p_exp' false env
--- a/src/elab_util.sml	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/elab_util.sml	Fri Mar 28 17:34:57 2008 -0400
@@ -233,6 +233,27 @@
                               fn e' =>
                                  (ECAbs (expl, x, k', e'), loc)))
 
+              | ERecord xes =>
+                S.map2 (ListUtil.mapfold (fn (x, e) =>
+                                             S.bind2 (mfc ctx x,
+                                                   fn x' =>
+                                                      S.map2 (mfe ctx e,
+                                                           fn e' =>
+                                                              (x', e'))))
+                                         xes,
+                     fn xes' =>
+                        (ERecord xes', loc))
+              | EField (e, c, {field, rest}) =>
+                S.bind2 (mfe ctx e,
+                      fn e' =>
+                         S.bind2 (mfc ctx c,
+                              fn c' =>
+                                 S.bind2 (mfc ctx field,
+                                          fn field' =>
+                                             S.map2 (mfc ctx rest,
+                                                  fn rest' =>
+                                                     (EField (e', c', {field = field', rest = rest'}), loc)))))
+
               | EError => S.return2 eAll
     in
         mfe
--- a/src/elaborate.sml	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/elaborate.sml	Fri Mar 28 17:34:57 2008 -0400
@@ -136,6 +136,7 @@
 
 val ktype = (L'.KType, dummy)
 val kname = (L'.KName, dummy)
+val ktype_record = (L'.KRecord ktype, dummy)
 
 val cerror = (L'.CError, dummy)
 val kerror = (L'.KError, dummy)
@@ -313,6 +314,8 @@
        | COccursCheckFailed of L'.con * L'.con
        | CIncompatible of L'.con * L'.con
        | CExplicitness of L'.con * L'.con
+       | CKindof of L'.con
+       | CRecordFailure
 
 exception CUnify' of cunify_error
 
@@ -335,8 +338,212 @@
         eprefaces "Differing constructor function explicitness"
                   [("Con 1", p_con env c1),
                    ("Con 2", p_con env c2)]
+      | CKindof c =>
+        eprefaces "Kind unification variable blocks kindof calculation"
+                  [("Con", p_con env c)]
+      | CRecordFailure =>
+        eprefaces "Can't unify record constructors" []
 
-fun hnormCon env (cAll as (c, _)) =
+exception SynUnif
+
+val liftConInCon =
+    U.Con.mapB {kind = fn k => k,
+                con = fn bound => fn c =>
+                                     case c of
+                                         L'.CRel xn =>
+                                         if xn < bound then
+                                             c
+                                         else
+                                             L'.CRel (xn + 1)
+                                       | L'.CUnif _ => raise SynUnif
+                                       | _ => c,
+                bind = fn (bound, U.Con.Rel _) => bound + 1
+                        | (bound, _) => bound}
+
+val subConInCon =
+    U.Con.mapB {kind = fn k => k,
+                con = fn (xn, rep) => fn c =>
+                                  case c of
+                                      L'.CRel xn' =>
+                                      if xn = xn' then
+                                          #1 rep
+                                      else
+                                          c
+                                    | L'.CUnif _ => raise SynUnif
+                                    | _ => c,
+                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+                        | (ctx, _) => ctx}
+
+type record_summary = {
+     fields : (L'.con * L'.con) list,
+     unifs : (L'.con * L'.con option ref) list,
+     others : L'.con list
+}
+
+fun summaryToCon {fields, unifs, others} =
+    let
+        val c = (L'.CRecord (ktype, []), dummy)
+        val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
+        val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
+    in
+        (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
+    end
+
+fun p_summary env s = p_con env (summaryToCon s)
+
+exception CUnify of L'.con * L'.con * cunify_error
+
+fun hnormKind (kAll as (k, _)) =
+    case k of
+        L'.KUnif (_, ref (SOME k)) => hnormKind k
+      | _ => kAll
+
+fun kindof env (c, loc) =
+    case c of
+        L'.TFun _ => ktype
+      | L'.TCFun _ => ktype
+      | L'.TRecord _ => ktype
+
+      | L'.CRel xn => #2 (E.lookupCRel env xn)
+      | L'.CNamed xn => #2 (E.lookupCNamed env xn)
+      | L'.CApp (c, _) =>
+        (case #1 (hnormKind (kindof env c)) of
+             L'.KArrow (_, k) => k
+           | L'.KError => kerror
+           | _ => raise CUnify' (CKindof c))
+      | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
+
+      | L'.CName _ => kname
+
+      | L'.CRecord (k, _) => (L'.KRecord k, loc)
+      | L'.CConcat (c, _) => kindof env c
+
+      | L'.CError => kerror
+      | L'.CUnif (k, _, _) => k
+
+fun unifyRecordCons env (c1, c2) =
+    let
+        val k1 = kindof env c1
+        val k2 = kindof env c2
+    in
+        unifyKinds k1 k2;
+        unifySummaries env (k1, recordSummary env c1, recordSummary env c2)
+    end
+
+and recordSummary env c : record_summary =
+    case hnormCon env c of
+        (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []}
+      | (L'.CConcat (c1, c2), _) =>
+        let
+            val s1 = recordSummary env c1
+            val s2 = recordSummary env c2
+        in
+            {fields = #fields s1 @ #fields s2,
+             unifs = #unifs s1 @ #unifs s2,
+             others = #others s1 @ #others s2}
+        end
+      | (L'.CUnif (_, _, ref (SOME c)), _) => recordSummary env c
+      | c' as (L'.CUnif (_, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
+      | c' => {fields = [], unifs = [], others = [c']}
+
+and consEq env (c1, c2) =
+    (unifyCons env c1 c2;
+     true)
+    handle CUnify _ => false
+
+and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
+    let
+        val () = eprefaces "Summaries" [("#1", p_summary env s1),
+                                        ("#2", p_summary env s2)]
+
+        fun eatMatching p (ls1, ls2) =
+            let
+                fun em (ls1, ls2, passed1) =
+                    case ls1 of
+                        [] => (rev passed1, ls2)
+                      | h1 :: t1 =>
+                        let
+                            fun search (ls2', passed2) =
+                                case ls2' of
+                                    [] => em (t1, ls2, h1 :: passed1)
+                                  | h2 :: t2 =>
+                                    if p (h1, h2) then
+                                        em (t1, List.revAppend (passed2, t2), passed1)
+                                    else
+                                        search (t2, h2 :: passed2)
+                        in
+                            search (ls2, [])
+                        end
+            in
+                em (ls1, ls2, [])
+            end
+
+        val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
+                                         if consEq env (x1, x2) then
+                                             (unifyCons env c1 c2;
+                                              true)
+                                         else
+                                             false) (#fields s1, #fields s2)
+        val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
+                                         ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]
+        val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
+        val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
+
+        fun unifFields (fs, others, unifs) =
+            case (fs, others, unifs) of
+                ([], [], _) => ([], [], unifs)
+              | (_, _, []) => (fs, others, [])
+              | (_, _, (_, r) :: rest) =>
+                let
+                    val r' = ref NONE
+                    val cr' = (L'.CUnif (k, "recd", r'), dummy)
+
+                    val prefix = case (fs, others) of
+                                     ([], other :: others) =>
+                                     List.foldl (fn (other, c) =>
+                                                    (L'.CConcat (c, other), dummy))
+                                                other others
+                                   | (fs, []) =>
+                                     (L'.CRecord (k, fs), dummy)
+                                   | (fs, others) =>
+                                     List.foldl (fn (other, c) =>
+                                                    (L'.CConcat (c, other), dummy))
+                                                (L'.CRecord (k, fs), dummy) others
+                in
+                    r := SOME (L'.CConcat (prefix, cr'), dummy);
+                    ([], [], (cr', r') :: rest)
+                end
+
+        val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
+        val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
+
+        val clear1 = case (fs1, others1) of
+                         ([], []) => true
+                       | _ => false
+        val clear2 = case (fs2, others2) of
+                         ([], []) => true
+                       | _ => false
+        val empty = (L'.CRecord (k, []), dummy)
+        fun pairOffUnifs (unifs1, unifs2) =
+            case (unifs1, unifs2) of
+                ([], _) =>
+                if clear1 then
+                    List.app (fn (_, r) => r := SOME empty) unifs2
+                else
+                    raise CUnify' CRecordFailure
+              | (_, []) =>
+                if clear2 then
+                    List.app (fn (_, r) => r := SOME empty) unifs1
+                else
+                    raise CUnify' CRecordFailure
+              | ((c1, _) :: rest1, (_, r2) :: rest2) =>
+                (r2 := SOME c1;
+                 pairOffUnifs (rest1, rest2))
+    in
+        pairOffUnifs (unifs1, unifs2)
+    end
+
+and hnormCon env (cAll as (c, _)) =
     case c of
         L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
 
@@ -345,14 +552,29 @@
              (_, _, SOME c') => hnormCon env c'
            | _ => cAll)
 
+      | L'.CApp (c1, c2) =>
+        (case hnormCon env c1 of
+             (L'.CAbs (_, _, cb), _) =>
+             ((hnormCon env (subConInCon (0, c2) cb))
+              handle SynUnif => cAll)
+           | _ => cAll)
+
+      | L'.CConcat (c1, c2) =>
+        (case (hnormCon env c1, hnormCon env c2) of
+             ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
+             (L'.CRecord (k, xcs1 @ xcs2), loc)
+           | _ => cAll)
+
       | _ => cAll
 
-fun unifyCons' env c1 c2 =
+and unifyCons' env c1 c2 =
     unifyCons'' env (hnormCon env c1) (hnormCon env c2)
     
 and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
     let
         fun err f = raise CUnify' (f (c1All, c2All))
+
+        fun isRecord () = unifyRecordCons env (c1All, c2All)
     in
         case (c1, c2) of
             (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
@@ -390,17 +612,6 @@
             else
                 err CIncompatible
 
-          | (L'.CRecord (k1, rs1), L'.CRecord (k2, rs2)) =>
-            (unifyKinds k1 k2;
-             ((ListPair.appEq (fn ((n1, v1), (n2, v2)) =>
-                                  (unifyCons' env n1 n2;
-                                   unifyCons' env v1 v2)) (rs1, rs2))
-              handle ListPair.UnequalLengths => err CIncompatible))
-          | (L'.CConcat (d1, r1), L'.CConcat (d2, r2)) =>
-            (unifyCons' env d1 d2;
-             unifyCons' env r1 r2)
-             
-
           | (L'.CError, _) => ()
           | (_, L'.CError) => ()
 
@@ -425,12 +636,15 @@
             else
                 r := SOME c1All
 
+          | (L'.CRecord _, _) => isRecord ()
+          | (_, L'.CRecord _) => isRecord ()
+          | (L'.CConcat _, _) => isRecord ()
+          | (_, L'.CConcat _) => isRecord ()
+
           | _ => err CIncompatible
     end
 
-exception CUnify of L'.con * L'.con * cunify_error
-
-fun unifyCons env c1 c2 =
+and unifyCons env c1 c2 =
     unifyCons' env c1 c2
     handle CUnify' err => raise CUnify (c1, c2, err)
          | KUnify args => raise CUnify (c1, c2, CKind args)
@@ -464,36 +678,6 @@
     handle CUnify (c1, c2, err) =>
            expError env (Unify (e, c1, c2, err))
 
-exception SynUnif
-
-val liftConInCon =
-    U.Con.mapB {kind = fn k => k,
-                con = fn bound => fn c =>
-                                     case c of
-                                         L'.CRel xn =>
-                                         if xn < bound then
-                                             c
-                                         else
-                                             L'.CRel (xn + 1)
-                                       | L'.CUnif _ => raise SynUnif
-                                       | _ => c,
-                bind = fn (bound, U.Con.Rel _) => bound + 1
-                        | (bound, _) => bound}
-
-val subConInCon =
-    U.Con.mapB {kind = fn k => k,
-                con = fn (xn, rep) => fn c =>
-                                  case c of
-                                      L'.CRel xn' =>
-                                      if xn = xn' then
-                                          #1 rep
-                                      else
-                                          c
-                                    | L'.CUnif _ => raise SynUnif
-                                    | _ => c,
-                bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
-                        | (ctx, _) => ctx}
-                                                         
 fun elabExp env (e, loc) =
     case e of
         L.EAnnot (e, t) =>
@@ -576,6 +760,35 @@
              (L'.TCFun (expl', x, k', et), loc))
         end
 
+      | L.ERecord xes =>
+        let
+            val xes' = map (fn (x, e) =>
+                               let
+                                   val (x', xk) = elabCon env x
+                                   val (e', et) = elabExp env e
+                               in
+                                   checkKind env x' xk kname;
+                                   (x', e', et)
+                               end) xes
+        in
+            ((L'.ERecord (map (fn (x', e', _) => (x', e')) xes'), loc),
+             (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc))
+        end
+
+      | L.EField (e, c) =>
+        let
+            val (e', et) = elabExp env e
+            val (c', ck) = elabCon env c
+
+            val ft = cunif ktype
+            val rest = cunif ktype_record
+        in
+            checkKind env c' ck kname;
+            checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
+            ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft)
+        end
+            
+
 datatype decl_error =
          KunifsRemainKind of ErrorMsg.span * L'.kind
        | KunifsRemainCon of ErrorMsg.span * L'.con
@@ -603,6 +816,7 @@
 
 fun elabDecl env (d, loc) =
     (resetKunif ();
+     resetCunif ();
      case d of
          L.DCon (x, ko, c) =>
          let
--- a/src/lacweb.grm	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/lacweb.grm	Fri Mar 28 17:34:57 2008 -0400
@@ -62,6 +62,7 @@
  | eexp of exp
  | eapps of exp
  | eterm of exp
+ | rexp of (con * exp) list
 
 %verbose                                (* print summary of errors *)
 %pos int                                (* positions *)
@@ -147,7 +148,13 @@
        | FN SYMBOL DARROW eexp          (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))
 
        | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
+       | eterm DOT ident                (EField (eterm, ident), s (etermleft, identright))
 
 eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
 
        | SYMBOL                         (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+       | LBRACE rexp RBRACE             (ERecord rexp, s (LBRACEleft, RBRACEright))
+
+rexp   :                                ([])
+       | ident EQ eexp                  ([(ident, eexp)])
+       | ident EQ eexp COMMA rexp       ((ident, eexp) :: rexp)
--- a/src/source.sml	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/source.sml	Fri Mar 28 17:34:57 2008 -0400
@@ -68,6 +68,9 @@
        | ECApp of exp * con
        | ECAbs of explicitness * string * kind * exp
 
+       | ERecord of (con * exp) list
+       | EField of exp * con
+
 withtype exp = exp' located
 
 datatype decl' =
--- a/src/source_print.sml	Fri Mar 28 15:20:46 2008 -0400
+++ b/src/source_print.sml	Fri Mar 28 17:34:57 2008 -0400
@@ -170,6 +170,19 @@
                                                   space,
                                                   p_exp e])
 
+      | ERecord xes => box [string "{",
+                            p_list (fn (x, e) =>
+                                       box [p_con x,
+                                            space,
+                                            string "=",
+                                            space,
+                                            p_exp e]) xes,
+                            string "}"]
+      | EField (e, c) => box [p_exp' true e,
+                              string ".",
+                              p_con' true c]
+
+
 and p_exp e = p_exp' false e
 
 fun p_decl ((d, _) : decl) =
--- a/tests/stuff.lac	Fri Mar 28 15:20:46 2008 -0400
+++ b/tests/stuff.lac	Fri Mar 28 17:34:57 2008 -0400
@@ -16,3 +16,23 @@
 
 val v1 = fn t :: Type => fn x : t => x
 val v2 = v1 [t :: Type -> t -> t] v1
+
+val r = {X = v1, Y = v2}
+val v1_again = r.X
+val v2_again = r.Y
+
+val r2 = {X = {}, Y = v2, Z = {}}
+val r2_X = r2.X
+val r2_Y = r2.Y
+val r2_Z = r2.Z
+
+val f = fn fs :: {Type} => fn x : $([X = {}] ++ fs) => x.X
+val f2 = fn fs :: {Type} => fn x : $(fs ++ [X = {}]) => x.X
+val f3 = fn fs :: {Type} => fn x : $([X = {}, Y = {Z : {}}] ++ fs) => x.X
+val f4 = fn fs :: {Type} => fn x : $([X = {}, Y = {Z : {}}] ++ fs) => x.Y
+val f5 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2) => x.X
+val f6 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2 ++ [Y = {Z : {}}]) => x.X
+val f7 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2 ++ [Y = {Z : {}}]) => x.Y
+
+val test = f [[Y = t :: Type -> t -> t, Z = {}]] r2
+val test = f7 [[Y = t :: Type -> t -> t]] [[Z = {}]] r2