summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 15:04:07 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-07 15:04:07 -0400
commit98370da7e9f70e3d83f666019b765e15f617b846 (patch)
tree24ba2b9bca09a5a9c9236d096b13998d77a97ab9 /src
parentfd1a963a81327f7b6a20a0f2ac131d2525649400 (diff)
Enhance table sig item support and get demo compiling again
Diffstat (limited to 'src')
-rw-r--r--src/elab_err.sig2
-rw-r--r--src/elab_err.sml6
-rw-r--r--src/elaborate.sml111
-rw-r--r--src/source.sml73
-rw-r--r--src/source_print.sml11
-rw-r--r--src/urweb.grm40
6 files changed, 147 insertions, 96 deletions
diff --git a/src/elab_err.sig b/src/elab_err.sig
index 3b14406b..c0a90e19 100644
--- a/src/elab_err.sig
+++ b/src/elab_err.sig
@@ -109,7 +109,7 @@ signature ELAB_ERR = sig
| NotFunctor of Elab.sgn
| FunctorRebind of ErrorMsg.span
| UnOpenable of Elab.sgn
- | NotType of Elab.kind * (Elab.kind * Elab.kind * kunify_error)
+ | NotType of ErrorMsg.span * Elab.kind * (Elab.kind * Elab.kind * kunify_error)
| DuplicateConstructor of string * ErrorMsg.span
| NotDatatype of ErrorMsg.span
diff --git a/src/elab_err.sml b/src/elab_err.sml
index 221e4981..4f24e225 100644
--- a/src/elab_err.sml
+++ b/src/elab_err.sml
@@ -328,7 +328,7 @@ datatype str_error =
| NotFunctor of sgn
| FunctorRebind of ErrorMsg.span
| UnOpenable of sgn
- | NotType of kind * (kind * kind * kunify_error)
+ | NotType of ErrorMsg.span * kind * (kind * kind * kunify_error)
| DuplicateConstructor of string * ErrorMsg.span
| NotDatatype of ErrorMsg.span
@@ -344,8 +344,8 @@ fun strError env err =
| UnOpenable sgn =>
(ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
eprefaces' [("Signature", p_sgn env sgn)])
- | NotType (k, (k1, k2, ue)) =>
- (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
+ | NotType (loc, k, (k1, k2, ue)) =>
+ (ErrorMsg.errorAt loc "'val' type kind is not 'Type'";
eprefaces' [("Kind", p_kind env k),
("Subkind 1", p_kind env k1),
("Subkind 2", p_kind env k2)];
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 224c3e50..d83af65b 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -871,16 +871,7 @@
let
fun err f = raise CUnify' (f (c1All, c2All))
- fun isRecord () = unifyRecordCons env (c1All, c2All)
- in
- (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
- ("c2All", p_con env c2All)];*)
-
- case (c1, c2) of
- (L'.CError, _) => ()
- | (_, L'.CError) => ()
-
- | (L'.CProj (c1, n1), _) =>
+ fun projSpecial1 (c1, n1, onFail) =
let
fun trySnd () =
case #1 (hnormCon env c2All) of
@@ -890,7 +881,7 @@
if n1 = n2 then
unifyCons' env c1 c2
else
- err CIncompatible
+ onFail ()
in
case #1 (hnormCon env c2) of
L'.CUnif (_, k, _, r) =>
@@ -906,7 +897,7 @@
| _ => tryNormal ())
| _ => tryNormal ()
end
- | _ => err CIncompatible
+ | _ => onFail ()
in
case #1 (hnormCon env c1) of
L'.CUnif (_, k, _, r) =>
@@ -923,20 +914,35 @@
| _ => trySnd ()
end
- | (_, L'.CProj (c2, n2)) =>
- (case #1 (hnormCon env c2) of
- L'.CUnif (_, k, _, r) =>
- (case #1 (hnormKind k) of
- L'.KTuple ks =>
- let
- val loc = #2 c2
- val us = map (fn k => cunif (loc, k)) ks
- in
- r := SOME (L'.CTuple us, loc);
- unifyCons' env c1All (List.nth (us, n2 - 1))
- end
- | _ => err CIncompatible)
- | _ => err CIncompatible)
+ fun projSpecial2 (c2, n2, onFail) =
+ case #1 (hnormCon env c2) of
+ L'.CUnif (_, k, _, r) =>
+ (case #1 (hnormKind k) of
+ L'.KTuple ks =>
+ let
+ val loc = #2 c2
+ val us = map (fn k => cunif (loc, k)) ks
+ in
+ r := SOME (L'.CTuple us, loc);
+ unifyCons' env c1All (List.nth (us, n2 - 1))
+ end
+ | _ => onFail ())
+ | _ => onFail ()
+
+ fun isRecord' () = unifyRecordCons env (c1All, c2All)
+
+ fun isRecord () =
+ case (c1, c2) of
+ (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord')
+ | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord')
+ | _ => isRecord' ()
+ in
+ (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
+ ("c2All", p_con env c2All)];*)
+
+ case (c1, c2) of
+ (L'.CError, _) => ()
+ | (_, L'.CError) => ()
| (L'.CRecord _, _) => isRecord ()
| (_, L'.CRecord _) => isRecord ()
@@ -1020,6 +1026,9 @@
((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
handle ListPair.UnequalLengths => err CIncompatible)
+ | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible)
+ | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible)
+
| (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
(unifyKinds env dom1 dom2;
unifyKinds env ran1 ran2)
@@ -2013,11 +2022,43 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
val c' = normClassConstraint env c'
in
(unifyKinds env ck ktype
- handle KUnify ue => strError env (NotType (ck, ue)));
+ handle KUnify ue => strError env (NotType (loc, ck, ue)));
([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
end
+ | L.SgiTable (x, c, e) =>
+ let
+ val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
+ val x' = x ^ "_hidden_constraints"
+ val (env', hidden_n) = E.pushCNamed env x' cstK NONE
+ val hidden = (L'.CNamed hidden_n, loc)
+
+ val (c', ck, gs') = elabCon (env, denv) c
+ val visible = cunif (loc, cstK)
+ val uniques = (L'.CConcat (visible, hidden), loc)
+
+ val ct = tableOf ()
+ val ct = (L'.CApp (ct, c'), loc)
+ val ct = (L'.CApp (ct, uniques), loc)
+
+ val (env', n) = E.pushENamed env' x ct
+
+ val (e', et, gs'') = elabExp (env, denv) e
+ val gs'' = List.mapPartial (fn Disjoint x => SOME x
+ | _ => NONE) gs''
+
+ val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc)
+ val cst = (L'.CApp (cst, c'), loc)
+ val cst = (L'.CApp (cst, visible), loc)
+ in
+ checkKind env c' ck (L'.KRecord (L'.KType, loc), loc);
+ checkCon env' e' et cst;
+
+ ([(L'.SgiConAbs (x', hidden_n, cstK), loc),
+ (L'.SgiVal (x, n, ct), loc)], (env', denv, gs'' @ gs' @ gs))
+ end
+
| L.SgiStr (x, sgn) =>
let
val (sgn', gs') = elabSgn (env, denv) sgn
@@ -2213,7 +2254,7 @@ and elabSgn (env, denv) (sgn, loc) =
end)
-fun selfify env {str, strs, sgn} =
+and selfify env {str, strs, sgn} =
case #1 (hnormSgn env sgn) of
L'.SgnError => sgn
| L'.SgnVar _ => sgn
@@ -2238,7 +2279,7 @@ fun selfify env {str, strs, sgn} =
NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE"
| SOME sgn => selfify env {str = str, strs = strs, sgn = sgn}
-fun selfifyAt env {str, sgn} =
+and selfifyAt env {str, sgn} =
let
fun self (str, _) =
case str of
@@ -2254,7 +2295,7 @@ fun selfifyAt env {str, sgn} =
| SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs}
end
-fun dopen env {str, strs, sgn} =
+and dopen env {str, strs, sgn} =
let
val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn))
(L'.StrVar str, #2 sgn) strs
@@ -2307,7 +2348,7 @@ fun dopen env {str, strs, sgn} =
([], env))
end
-fun sgiOfDecl (d, loc) =
+and sgiOfDecl (d, loc) =
case d of
L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
| L'.DDatatype x => [(L'.SgiDatatype x, loc)]
@@ -2326,7 +2367,7 @@ fun sgiOfDecl (d, loc) =
| L'.DDatabase _ => []
| L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
-fun subSgn env sgn1 (sgn2 as (_, loc2)) =
+and subSgn env sgn1 (sgn2 as (_, loc2)) =
((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
("sgn2", p_sgn env sgn2)];*)
case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
@@ -2694,7 +2735,7 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
| _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
-fun positive self =
+and positive self =
let
open L
@@ -2760,7 +2801,7 @@ fun positive self =
pos
end
-fun wildifyStr env (str, sgn) =
+and wildifyStr env (str, sgn) =
case #1 (hnormSgn env sgn) of
L'.SgnConst sgis =>
(case #1 str of
@@ -2922,7 +2963,7 @@ fun wildifyStr env (str, sgn) =
| _ => str)
| _ => str
-fun elabDecl (dAll as (d, loc), (env, denv, gs)) =
+and elabDecl (dAll as (d, loc), (env, denv, gs)) =
let
(*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
(*val befor = Time.now ()*)
diff --git a/src/source.sml b/src/source.sml
index 42927ef3..0dca39ab 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -77,12 +77,18 @@ datatype con' =
withtype con = con' located
+datatype inference =
+ Infer
+ | DontInfer
+ | TypesOnly
+
datatype sgn_item' =
SgiConAbs of string * kind
| SgiCon of string * kind option * con
| SgiDatatype of string * string list * (string * con option) list
| SgiDatatypeImp of string * string list * string
| SgiVal of string * con
+ | SgiTable of string * con * exp
| SgiStr of string * sgn
| SgiSgn of string * sgn
| SgiInclude of sgn
@@ -97,56 +103,51 @@ and sgn' =
| SgnWhere of sgn * string * con
| SgnProj of string * string list * string
-withtype sgn_item = sgn_item' located
-and sgn = sgn' located
-
-datatype pat' =
- PWild
- | PVar of string
- | PPrim of Prim.t
- | PCon of string list * string * pat option
- | PRecord of (string * pat) list * bool
-
-withtype pat = pat' located
+and pat' =
+ PWild
+ | PVar of string
+ | PPrim of Prim.t
+ | PCon of string list * string * pat option
+ | PRecord of (string * pat) list * bool
-datatype inference =
- Infer
- | DontInfer
- | TypesOnly
-
-datatype exp' =
- EAnnot of exp * con
+and exp' =
+ EAnnot of exp * con
- | EPrim of Prim.t
- | EVar of string list * string * inference
- | EApp of exp * exp
- | EAbs of string * con option * exp
- | ECApp of exp * con
- | ECAbs of explicitness * string * kind * exp
- | EDisjoint of con * con * exp
- | EDisjointApp of exp
+ | EPrim of Prim.t
+ | EVar of string list * string * inference
+ | EApp of exp * exp
+ | EAbs of string * con option * exp
+ | ECApp of exp * con
+ | ECAbs of explicitness * string * kind * exp
+ | EDisjoint of con * con * exp
+ | EDisjointApp of exp
- | EKAbs of string * exp
+ | EKAbs of string * exp
- | ERecord of (con * exp) list
- | EField of exp * con
- | EConcat of exp * exp
- | ECut of exp * con
- | ECutMulti of exp * con
+ | ERecord of (con * exp) list
+ | EField of exp * con
+ | EConcat of exp * exp
+ | ECut of exp * con
+ | ECutMulti of exp * con
- | EWild
+ | EWild
- | ECase of exp * (pat * exp) list
+ | ECase of exp * (pat * exp) list
- | ELet of edecl list * exp
+ | ELet of edecl list * exp
and edecl' =
EDVal of string * con option * exp
| EDValRec of (string * con option * exp) list
-withtype exp = exp' located
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+and pat = pat' located
+and exp = exp' located
and edecl = edecl' located
+
+
datatype decl' =
DCon of string * kind option * con
| DDatatype of string * string list * (string * con option) list
diff --git a/src/source_print.sml b/src/source_print.sml
index d1c9b6df..c145dc63 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -417,6 +417,17 @@ fun p_sgn_item (sgi, _) =
string ":",
space,
p_con c]
+ | SgiTable (x, c, e) => box [string "table",
+ space,
+ string x,
+ space,
+ string ":",
+ space,
+ p_con c,
+ space,
+ string "constraints",
+ space,
+ p_exp e]
| SgiStr (x, sgn) => box [string "structure",
space,
string x,
diff --git a/src/urweb.grm b/src/urweb.grm
index ad92ff11..0f4b58d7 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -532,34 +532,32 @@ sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright))
| sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright))
| LPAREN sgn RPAREN (sgn)
-sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, kindright))
- | LTYPE SYMBOL (SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
- s (LTYPEleft, SYMBOLright))
- | CON SYMBOL EQ cexp (SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright))
- | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright))
- | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
- s (LTYPEleft, cexpright))
- | DATATYPE SYMBOL dargs EQ barOpt dcons(SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright))
+sgi : CON SYMBOL DCOLON kind ((SgiConAbs (SYMBOL, kind), s (CONleft, kindright)))
+ | LTYPE SYMBOL ((SgiConAbs (SYMBOL, (KType, s (LTYPEleft, SYMBOLright))),
+ s (LTYPEleft, SYMBOLright)))
+ | CON SYMBOL EQ cexp ((SgiCon (SYMBOL, NONE, cexp), s (CONleft, cexpright)))
+ | CON SYMBOL DCOLON kind EQ cexp ((SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)))
+ | LTYPE SYMBOL EQ cexp ((SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp),
+ s (LTYPEleft, cexpright)))
+ | DATATYPE SYMBOL dargs EQ barOpt dcons((SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright)))
| DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path
(case dargs of
[] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright))
| _ => raise Fail "Arguments specified for imported datatype")
- | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright))
+ | VAL SYMBOL COLON cexp ((SgiVal (SYMBOL, cexp), s (VALleft, cexpright)))
- | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright))
- | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright))
+ | STRUCTURE CSYMBOL COLON sgn ((SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)))
+ | SIGNATURE CSYMBOL EQ sgn ((SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)))
| FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn
- (SgiStr (CSYMBOL1,
- (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
- s (FUNCTORleft, sgn2right))
- | INCLUDE sgn (SgiInclude sgn, s (INCLUDEleft, sgnright))
- | CONSTRAINT cterm TWIDDLE cterm (SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright))
- | TABLE SYMBOL COLON cexp (let
- val loc = s (TABLEleft, cexpright)
- val t = (CApp ((CVar (["Basis"], "sql_table"), loc),
- entable cexp), loc)
+ ((SgiStr (CSYMBOL1,
+ (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))),
+ s (FUNCTORleft, sgn2right)))
+ | INCLUDE sgn ((SgiInclude sgn, s (INCLUDEleft, sgnright)))
+ | CONSTRAINT cterm TWIDDLE cterm ((SgiConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)))
+ | TABLE SYMBOL COLON cterm cstopt(let
+ val loc = s (TABLEleft, ctermright)
in
- (SgiVal (SYMBOL, t), loc)
+ (SgiTable (SYMBOL, entable cterm, cstopt), loc)
end)
| SEQUENCE SYMBOL (let
val loc = s (SEQUENCEleft, SYMBOLright)