aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/basis.urs26
-rw-r--r--lib/top.ur16
-rw-r--r--lib/top.urs20
-rw-r--r--src/disjoint.sml3
-rw-r--r--src/elab.sml3
-rw-r--r--src/elab_ops.sml2
-rw-r--r--src/elab_print.sml13
-rw-r--r--src/elab_util.sml12
-rw-r--r--src/elaborate.sml36
-rw-r--r--src/explify.sml3
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml9
-rw-r--r--src/urweb.grm1
13 files changed, 47 insertions, 98 deletions
diff --git a/lib/basis.urs b/lib/basis.urs
index 3fe80d38..3dec0461 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -189,7 +189,7 @@ val bind : t1 ::: Type -> t2 ::: Type
-> transaction t2
val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps
- -> state ::: Type
+ => state ::: Type
-> sql_query tables exps
-> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
-> state
@@ -210,7 +210,7 @@ val insert : fields ::: {Type}
-> dml
val update : changed :: {Type} -> unchanged ::: {Type} -> changed ~ unchanged
- -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
+ => $(fold (fn nm (t :: Type) acc => [nm] ~ acc =>
[nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed)
-> sql_table (changed ++ unchanged)
-> sql_exp [T = changed ++ unchanged] [] [] bool
@@ -235,22 +235,22 @@ con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type
con xml :: {Unit} -> {Type} -> {Type} -> Type
val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use []
val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent
- -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
+ => ctxOuter ::: {Unit} -> ctxInner ::: {Unit}
-> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner
- -> bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
- -> $attrsGiven
+ => bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner
+ => $attrsGiven
-> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter
-> xml ctxInner useInner bindInner
-> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner)
val join : ctx ::: {Unit}
-> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type}
- -> use1 ~ bind1 -> bind1 ~ bind2
- -> xml ctx use1 bind1
+ -> use1 ~ bind1 => bind1 ~ bind2
+ => xml ctx use1 bind1
-> xml ctx (use1 ++ bind1) bind2
-> xml ctx use1 (bind1 ++ bind2)
val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type}
-> use1 ~ use2
- -> xml ctx use1 bind
+ => xml ctx use1 bind
-> xml ctx (use1 ++ use2) bind
con xhtml = xml [Html]
@@ -272,9 +272,9 @@ val head : unit -> tag [] html head [] []
val title : unit -> tag [] head [] [] []
val body : unit -> tag [] html body [] []
-con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
+con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
-> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] []
-con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx -> unit
+con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit
-> tag attrs ([Body] ++ ctx) [] [] []
val br : bodyTagStandalone []
@@ -289,12 +289,12 @@ val li : bodyTag []
val a : bodyTag [Link = transaction page]
-val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type}
+val lform : ctx ::: {Unit} -> [Body] ~ ctx => bind ::: {Type}
-> xml form [] bind
-> xml ([Body] ++ ctx) [] []
con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} =>
ctx ::: {Unit} -> [LForm] ~ ctx
- -> nm :: Name -> unit
+ => nm :: Name -> unit
-> tag attrs ([LForm] ++ ctx) inner [] [nm = ty]
val textbox : lformTag string [] [Value = string]
val password : lformTag string [] []
@@ -311,7 +311,7 @@ val lselect : lformTag string select []
val loption : unit -> tag [Value = string] select [] [] []
val submit : ctx ::: {Unit} -> [LForm] ~ ctx
- -> use ::: {Type} -> unit
+ => use ::: {Type} -> unit
-> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use []
(*** Tables *)
diff --git a/lib/top.ur b/lib/top.ur
index 990a18fa..e7c4a988 100644
--- a/lib/top.ur
+++ b/lib/top.ur
@@ -22,7 +22,7 @@ fun txt (t ::: Type) (ctx ::: {Unit}) (use ::: {Type}) (sh : show t) (v : t) = c
fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
(f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf t -> tr rest -> tr ([nm = t] ++ rest))
(i : tr []) =
fold [fn r :: {Type} => $(mapTT tf r) -> tr r]
(fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) =>
@@ -32,7 +32,7 @@ fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type)
fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
(f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf t -> tr rest -> tr ([nm = t] ++ rest))
(i : tr []) =
fold [fn r :: {(Type * Type)} => $(mapT2T tf r) -> tr r]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> tr rest) =>
@@ -42,7 +42,7 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
(f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
(i : tr []) =
fold [fn r :: {Type} => $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r]
(fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> _ -> tr rest) =>
@@ -52,7 +52,7 @@ fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type)
fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type)
(f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
(i : tr []) =
fold [fn r :: {(Type * Type)} => $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) (acc : _ -> _ -> tr rest) =>
@@ -62,7 +62,7 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (tr :
fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
(f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf t -> xml ctx [] []) =
+ => tf t -> xml ctx [] []) =
foldTR [tf] [fn _ => xml ctx [] []]
(fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
[[nm] ~ rest] =>
@@ -71,7 +71,7 @@ fun foldTRX (tf :: Type -> Type) (ctx :: {Unit})
fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
(f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf t -> xml ctx [] []) =
+ => tf t -> xml ctx [] []) =
foldT2R [tf] [fn _ => xml ctx [] []]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
[[nm] ~ rest] =>
@@ -80,7 +80,7 @@ fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit})
fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
(f : nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> xml ctx [] []) =
+ => tf1 t -> tf2 t -> xml ctx [] []) =
foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []]
(fn (nm :: Name) (t :: Type) (rest :: {Type}) =>
[[nm] ~ rest] =>
@@ -89,7 +89,7 @@ fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit})
fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) (ctx :: {Unit})
(f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> xml ctx [] []) =
+ => tf1 t -> tf2 t -> xml ctx [] []) =
foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []]
(fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) =>
[[nm] ~ rest] =>
diff --git a/lib/top.urs b/lib/top.urs
index add94578..684ebfb8 100644
--- a/lib/top.urs
+++ b/lib/top.urs
@@ -22,52 +22,52 @@ val txt : t ::: Type -> ctx ::: {Unit} -> use ::: {Type} -> show t -> t
val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type)
-> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf t -> tr rest -> tr ([nm = t] ++ rest))
-> tr [] -> r :: {Type} -> $(mapTT tf r) -> tr r
val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type)
-> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf t -> tr rest -> tr ([nm = t] ++ rest))
-> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r
val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type)
-> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-> tr [] -> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> tr r
val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type)
-> tr :: ({(Type * Type)} -> Type)
-> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
+ => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest))
-> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r
val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf t -> xml ctx [] [])
+ => tf t -> xml ctx [] [])
-> r :: {Type} -> $(mapTT tf r) -> xml ctx [] []
val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf t -> xml ctx [] [])
+ => tf t -> xml ctx [] [])
-> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] []
val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: Type -> rest :: {Type} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> xml ctx [] [])
+ => tf1 t -> tf2 t -> xml ctx [] [])
-> r :: {Type} -> $(mapTT tf1 r) -> $(mapTT tf2 r) -> xml ctx [] []
val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> ctx :: {Unit}
-> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} -> [nm] ~ rest
- -> tf1 t -> tf2 t -> xml ctx [] [])
+ => tf1 t -> tf2 t -> xml ctx [] [])
-> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] []
val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit}
-> sql_query tables exps -> tables ~ exps
- -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
+ => ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables)
-> xml ctx [] [])
-> transaction (xml ctx [] [])
val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} -> sql_query tables exps
-> tables ~ exps
- -> transaction
+ => transaction
(option $(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables))
diff --git a/src/disjoint.sml b/src/disjoint.sml
index f3a98b51..808d8413 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -315,8 +315,7 @@ and hnormCon (env, denv) c =
end
in
case c of
- CDisjoint cs => doDisj cs
- | TDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
+ CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c)
| _ => (cAll, [])
end
diff --git a/src/elab.sml b/src/elab.sml
index 0ce86726..9bb609bf 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -53,7 +53,6 @@ datatype auto_instantiate =
datatype con' =
TFun of con * con
| TCFun of explicitness * string * kind * con
- | TDisjoint of auto_instantiate * con * con * con
| TRecord of con
| CRel of int
@@ -61,7 +60,7 @@ datatype con' =
| CModProj of int * string list * string
| CApp of con * con
| CAbs of string * kind * con
- | CDisjoint of con * con * con
+ | CDisjoint of auto_instantiate * con * con * con
| CName of string
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index e236e62d..95ad971f 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -146,7 +146,7 @@ fun hnormCon env (cAll as (c, loc)) =
val c = (CApp (c, r), loc)
fun unconstraint c =
case hnormCon env c of
- (CDisjoint (_, _, c), _) => unconstraint c
+ (CDisjoint (_, _, _, c), _) => unconstraint c
| c => c
val c = unconstraint c
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 36d6a48e..c1bc5938 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -80,13 +80,13 @@ fun p_con' par env (c, _) =
string "->",
space,
p_con (E.pushCRel env x k) c])
- | TDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
+ | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1,
space,
string "~",
space,
p_con env c2,
space,
- string "->",
+ string "=>",
space,
p_con env c3])
| TRecord (CRecord (_, xcs), _) => box [string "{",
@@ -139,15 +139,6 @@ fun p_con' par env (c, _) =
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]
diff --git a/src/elab_util.sml b/src/elab_util.sml
index cc4fbe4a..69ed3248 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -119,14 +119,14 @@ fun mapfoldB {kind = fk, con = fc, bind} =
S.map2 (mfc (bind (ctx, Rel (x, k))) c,
fn c' =>
(TCFun (e, x, k', c'), loc)))
- | TDisjoint (ai, c1, c2, c3) =>
+ | CDisjoint (ai, c1, c2, c3) =>
S.bind2 (mfc ctx c1,
fn c1' =>
S.bind2 (mfc ctx c2,
fn c2' =>
S.map2 (mfc ctx c3,
fn c3' =>
- (TDisjoint (ai, c1', c2', c3'), loc))))
+ (CDisjoint (ai, c1', c2', c3'), loc))))
| TRecord c =>
S.map2 (mfc ctx c,
fn c' =>
@@ -147,14 +147,6 @@ fun mapfoldB {kind = fk, con = fc, bind} =
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
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 7702e0ff..d7dc6ebe 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -225,7 +225,7 @@ fun elabCon (env, denv) (c, loc) =
checkKind env t' tk ktype;
((L'.TCFun (e', x, k', t'), loc), ktype, gs)
end
- | L.TDisjoint (c1, c2, c) =>
+ | L.CDisjoint (c1, c2, c) =>
let
val (c1', k1, gs1) = elabCon (env, denv) c1
val (c2', k2, gs2) = elabCon (env, denv) c2
@@ -239,7 +239,7 @@ fun elabCon (env, denv) (c, loc) =
checkKind env c1' k1 (L'.KRecord ku1, loc);
checkKind env c2' k2 (L'.KRecord ku2, loc);
- ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
+ ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
end
| L.TRecord c =>
let
@@ -304,23 +304,6 @@ fun elabCon (env, denv) (c, loc) =
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', gs3) = D.assert env denv (c1', c2')
- val (c', k, gs4) = 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 @ gs4)
- end
-
| L.CName s =>
((L'.CName s, loc), kname, [])
@@ -476,7 +459,6 @@ fun kindof env (c, loc) =
case c of
L'.TFun _ => ktype
| L'.TCFun _ => ktype
- | L'.TDisjoint _ => ktype
| L'.TRecord _ => ktype
| L'.CRel xn => #2 (E.lookupCRel env xn)
@@ -501,7 +483,7 @@ fun kindof env (c, loc) =
| (L'.KError, _) => kerror
| k => raise CUnify' (CKindof (k, c)))
| L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
- | L'.CDisjoint (_, _, c) => kindof env c
+ | L'.CDisjoint (_, _, _, c) => kindof env c
| L'.CName _ => kname
@@ -541,7 +523,7 @@ fun summarizeCon (env, denv) c =
L'.CRecord (_, []) => (Nil, gs)
| L'.CRecord (_, _ :: _) => (Cons, gs)
| L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
- | L'.CDisjoint (_, _, c) =>
+ | L'.CDisjoint (_, _, _, c) =>
let
val (s, gs') = summarizeCon (env, denv) c
in
@@ -824,7 +806,7 @@ and guessFold (env, denv) (c1, c2, gs, ex) =
and unifyCons' (env, denv) c1 c2 =
case (#1 c1, #1 c2) of
- (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) =>
+ (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
let
val gs1 = unifyCons' (env, denv) x1 x2
val gs2 = unifyCons' (env, denv) y1 y2
@@ -983,7 +965,7 @@ fun foldType (dom, loc) =
(L'.TCFun (L'.Explicit, "v", dom,
(L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
(L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
- (L'.TDisjoint (L'.Instantiate,
+ (L'.CDisjoint (L'.Instantiate,
(L'.CRecord
((L'.KUnit, loc),
[((L'.CRel 2, loc),
@@ -1524,7 +1506,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
checkKind env c1' k1 (L'.KRecord ku1, loc);
checkKind env c2' k2 (L'.KRecord ku2, loc);
- (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
+ (e', (L'.CDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
end
| L.ERecord xes =>
@@ -2572,7 +2554,6 @@ fun positive self =
| TFun (c1, c2) => none c1 andalso none c2
| TCFun (_, _, _, c) => none c
- | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
| TRecord c => none c
| CVar ([], x) => x <> self
@@ -2600,7 +2581,6 @@ fun positive self =
| TFun (c1, c2) => none c1 andalso pos c2
| TCFun (_, _, _, c) => pos c
- | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
| TRecord c => pos c
| CVar _ => true
@@ -2721,7 +2701,7 @@ val makeInstantiable =
fun kind k = k
fun con c =
case c of
- L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c)
+ L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
| _ => c
in
U.Con.map {kind = kind, con = con}
diff --git a/src/explify.sml b/src/explify.sml
index 573ddf51..72531d7a 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -49,7 +49,7 @@ fun explifyCon (c, loc) =
case c of
L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
| L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
- | L.TDisjoint (_, _, _, c) => explifyCon c
+ | L.CDisjoint (_, _, _, c) => explifyCon c
| L.TRecord c => (L'.TRecord (explifyCon c), loc)
| L.CRel n => (L'.CRel n, loc)
@@ -58,7 +58,6 @@ fun explifyCon (c, loc) =
| 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 (_, _, c) => explifyCon c
| L.CName s => (L'.CName s, loc)
diff --git a/src/source.sml b/src/source.sml
index 14d4d6f8..d99907ae 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -49,7 +49,6 @@ datatype con' =
| TFun of con * con
| TCFun of explicitness * string * kind * con
- | TDisjoint of con * con * con
| TRecord of con
| CVar of string list * string
diff --git a/src/source_print.sml b/src/source_print.sml
index e1a8de7a..324b50d5 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -81,15 +81,6 @@ fun p_con' par (c, _) =
string "->",
space,
p_con c])
- | TDisjoint (c1, c2, c3) => parenIf par (box [p_con c1,
- space,
- string "~",
- space,
- p_con c2,
- space,
- string "->",
- space,
- p_con c3])
| TRecord (CRecord xcs, _) => box [string "{",
p_list (fn (x, c) =>
box [p_name x,
diff --git a/src/urweb.grm b/src/urweb.grm
index 9c8c0251..b7b09227 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -530,7 +530,6 @@ cexp : capps (capps)
| FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright)))))
| cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
- | cterm TWIDDLE cterm ARROW cexp (TDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright))
| LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:39:21 +0000