Mercurial > urweb

changeset 84:e86370850c30

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness assumptions
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 12:10:46 -0400
parents 0a1baddd8ab2
children 1f85890c9846
files src/disjoint.sml src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/source.sml src/source_print.sml tests/disjoint.lac
diffstat 11 files changed, 73 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/disjoint.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/disjoint.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -114,7 +114,7 @@
                 CName s => NameC s :: acc
               | CRel n => NameR n :: acc
               | CNamed n => NameN n :: acc
-              | _ => Unknown :: acc
+              | _ => (print "Unknown name\n"; Unknown :: acc)
                      
         fun decomposeRow (c, acc) =
             case #1 (hnormCon env c) of
@@ -122,7 +122,7 @@
               | CConcat (c1, c2) => decomposeRow (c1, decomposeRow (c2, acc))
               | CRel n => RowR n :: acc
               | CNamed n => RowN n :: acc
-              | _ => Unknown :: acc
+              | _ => (print "Unknown row\n"; Unknown :: acc)
     in
         decomposeRow (c, [])
     end
@@ -265,6 +265,7 @@
 fun prove1 denv (p1, p2) =
     case (p1, p2) of
         (NameC s1, NameC s2) => s1 <> s2
+      | (NameC _, _) => prove1' denv (p2, p1)
       | (_, RowR _) => prove1' denv (p2, p1)
       | (_, RowN _) => prove1' denv (p2, p1)
       | _ => prove1' denv (p1, p2)
--- a/src/elab.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -55,6 +55,7 @@
        | CModProj of int * string list * string
        | CApp of con * con
        | CAbs of string * kind * con
+       | CDisjoint of con * con * con
 
        | CName of string
 
--- a/src/elab_print.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab_print.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -126,6 +126,15 @@
                                             string "=>",
                                             space,
                                             p_con (E.pushCRel env x k) c])
+      | CDisjoint (c1, c2, c3) => parenIf par (box [p_con env c1,
+                                                    space,
+                                                    string "~",
+                                                    space,
+                                                    p_con env c2,
+                                                    space,
+                                                    string "=>",
+                                                    space,
+                                                    p_con env c3])
 
       | CName s => box [string "#", string s]
 
--- a/src/elab_util.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elab_util.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -124,6 +124,14 @@
                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
                               fn c' =>
                                  (CAbs (x, k', c'), loc)))
+              | CDisjoint (c1, c2, c3) =>
+                S.bind2 (mfc ctx c1,
+                      fn c1' =>
+                         S.bind2 (mfc ctx c2,
+                              fn c2' =>
+                                 S.map2 (mfc ctx c3,
+                                         fn c3' =>
+                                            (CDisjoint (c1', c2', c3'), loc))))
 
               | CName _ => S.return2 cAll
 
--- a/src/elaborate.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/elaborate.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -306,6 +306,23 @@
              gs)
         end
 
+      | L.CDisjoint (c1, c2, c) =>
+        let
+            val (c1', k1, gs1) = elabCon (env, denv) c1
+            val (c2', k2, gs2) = elabCon (env, denv) c2
+
+            val ku1 = kunif loc
+            val ku2 = kunif loc
+
+            val denv' = D.assert env denv (c1', c2')
+            val (c', k, gs3) = elabCon (env, denv') c
+        in
+            checkKind env c1' k1 (L'.KRecord ku1, loc);
+            checkKind env c2' k2 (L'.KRecord ku2, loc);
+
+            ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3)
+        end
+
       | L.CName s =>
         ((L'.CName s, loc), kname, [])
 
@@ -498,6 +515,7 @@
            | L'.KError => kerror
            | _ => raise CUnify' (CKindof c))
       | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
+      | L'.CDisjoint (_, _, c) => kindof env c
 
       | L'.CName _ => kname
 
@@ -1761,13 +1779,16 @@
 
         val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
     in
-        app (fn (loc, env, denv, (c1, c2)) =>
-                case D.prove env denv (c1, c2, loc) of
-                    [] => ()
-                  | _ =>
-                    (ErrorMsg.errorAt loc "Remaining constraint";
-                     eprefaces' [("Con 1", p_con env c1),
-                                 ("Con 2", p_con env c2)])) gs;
+        if ErrorMsg.anyErrors () then
+            ()
+        else
+            app (fn (loc, env, denv, (c1, c2)) =>
+                    case D.prove env denv (c1, c2, loc) of
+                        [] => ()
+                      | _ =>
+                        (ErrorMsg.errorAt loc "Remaining constraint";
+                         eprefaces' [("Con 1", p_con env c1),
+                                     ("Con 2", p_con env c2)])) gs;
 
         (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
     end
--- a/src/explify.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/explify.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -56,6 +56,7 @@
 
       | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc)
       | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc)
+      | L.CDisjoint _ => raise Fail "Explify CDisjoint"
 
       | L.CName s => (L'.CName s, loc)
 
--- a/src/lacweb.grm	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/lacweb.grm	Tue Jul 01 12:10:46 2008 -0400
@@ -43,7 +43,7 @@
  | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
  | TYPE | NAME
  | ARROW | LARROW | DARROW
- | FN | PLUSPLUS | DOLLAR
+ | FN | PLUSPLUS | DOLLAR | TWIDDLE
  | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | INCLUDE | OPEN
 
 %nonterm
@@ -93,6 +93,7 @@
 %right COMMA
 %right ARROW LARROW
 %right PLUSPLUS
+%nonassoc TWIDDLE
 %nonassoc DOLLAR
 %left DOT
 
@@ -194,6 +195,7 @@
 
        | FN SYMBOL DARROW cexp          (CAbs (SYMBOL, NONE, cexp), s (FNleft, cexpright))
        | FN SYMBOL DCOLON kind DARROW cexp (CAbs (SYMBOL, SOME kind, cexp), s (FNleft, cexpright))
+       | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
 
        | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
 
--- a/src/lacweb.lex	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/lacweb.lex	Tue Jul 01 12:10:46 2008 -0400
@@ -142,6 +142,7 @@
 <INITIAL> "#"         => (Tokens.HASH (pos yypos, pos yypos + size yytext));
 <INITIAL> "__"        => (Tokens.UNDERUNDER (pos yypos, pos yypos + size yytext));
 <INITIAL> "_"         => (Tokens.UNDER (pos yypos, pos yypos + size yytext));
+<INITIAL> "~"         => (Tokens.TWIDDLE (pos yypos, pos yypos + size yytext));
 
 <INITIAL> "con"       => (Tokens.CON (pos yypos, pos yypos + size yytext));
 <INITIAL> "type"      => (Tokens.LTYPE (pos yypos, pos yypos + size yytext));
--- a/src/source.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/source.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -53,6 +53,7 @@
        | CVar of string list * string
        | CApp of con * con
        | CAbs of string * kind option * con
+       | CDisjoint of con * con * con
 
        | CName of string
 
--- a/src/source_print.sml	Tue Jul 01 11:39:14 2008 -0400
+++ b/src/source_print.sml	Tue Jul 01 12:10:46 2008 -0400
@@ -111,6 +111,15 @@
                                                  string "=>",
                                                  space,
                                                  p_con c])
+      | CDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
+                                                    space,
+                                                    string "~",
+                                                    space,
+                                                    p_con c2,
+                                                    space,
+                                                    string "=>",
+                                                    space,
+                                                    p_con c3])
 
       | CName s => box [string "#", string s]
 
--- a/tests/disjoint.lac	Tue Jul 01 11:39:14 2008 -0400
+++ b/tests/disjoint.lac	Tue Jul 01 12:10:46 2008 -0400
@@ -1,1 +1,9 @@
-con c = fn x :: Name => [x, A]
+con c1 = fn x :: Name => [x] ~ [A] => [x, A]
+con c2 = fn x :: Name => [x] ~ [A] => [A, x]
+con c3 = fn x :: Name => [A] ~ [x] => [x, A]
+con c4 = fn x :: Name => [A] ~ [x] => [A, x]
+
+con c5 = fn r1 :: {Type} => fn r2 => r1 ~ r2 => r1 ++ r2
+con c6 = fn r1 :: {Type} => fn r2 => r2 ~ r1 => r1 ++ r2
+
+con c7 = fn x :: Name => fn r => [x] ~ r => [x] ++ r