From 2eca16323e58b01a70ea734e2825765ebe239dc0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 4 Oct 2008 15:50:28 -0400 Subject: Merge CDisjoint and TDisjoint --- src/disjoint.sml | 3 +-- src/elab.sml | 3 +-- src/elab_ops.sml | 2 +- src/elab_print.sml | 13 ++----------- src/elab_util.sml | 12 ++---------- src/elaborate.sml | 36 ++++++++---------------------------- src/explify.sml | 3 +-- src/source.sml | 1 - src/source_print.sml | 9 --------- src/urweb.grm | 1 - 10 files changed, 16 insertions(+), 67 deletions(-) (limited to 'src') 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)) -- cgit v1.2.3