Mercurial > urweb
diff src/elab_print.sml @ 623:588b9d16b00a
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 22 Feb 2009 16:10:25 -0500 |
| parents | 8998114760c1 |
| children | 354800878b4d |
line wrap: on
line diff
--- a/src/elab_print.sml Sat Feb 21 16:11:56 2009 -0500 +++ b/src/elab_print.sml Sun Feb 22 16:10:25 2009 -0500 @@ -38,25 +38,36 @@ val debug = ref false -fun p_kind' par (k, _) = +fun p_kind' par env (k, _) = case k of KType => string "Type" - | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, + | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1, space, string "->", space, - p_kind k2]) + p_kind env k2]) | KName => string "Name" - | KRecord k => box [string "{", p_kind k, string "}"] + | KRecord k => box [string "{", p_kind env k, string "}"] | KUnit => string "Unit" | KTuple ks => box [string "(", - p_list_sep (box [space, string "*", space]) p_kind ks, + p_list_sep (box [space, string "*", space]) (p_kind env) ks, string ")"] | KError => string "<ERROR>" - | KUnif (_, _, ref (SOME k)) => p_kind' par k + | KUnif (_, _, ref (SOME k)) => p_kind' par env k | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">") + | KRel n => ((if !debug then + string (E.lookupKRel env n ^ "_" ^ Int.toString n) + else + string (E.lookupKRel env n)) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) + | KFun (x, k) => box [string x, + space, + string "-->", + space, + p_kind (E.pushKRel env x) k] + and p_kind k = p_kind' false k fun p_explicitness e = @@ -66,7 +77,7 @@ fun p_con' par env (c, _) = case c of - TFun (t1, t2) => parenIf par (box [p_con' true env t1, + TFun (t1, t2) => parenIf true (box [p_con' true env t1, space, string "->", space, @@ -75,20 +86,22 @@ space, p_explicitness e, space, - p_kind k, + p_kind env k, space, 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]) + | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1, + space, + string (case ai of + Instantiate => "~" + | LeaveAlone => "~~"), + space, + p_con env c2, + space, + string "=>", + space, + p_con env c3]) | TRecord (CRecord (_, xcs), _) => box [string "{", p_list (fn (x, c) => box [p_name env x, @@ -134,7 +147,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -152,7 +165,7 @@ space, p_con env c]) xcs, string "]::", - p_kind k]) + p_kind env k]) else parenIf par (box [string "[", p_list (fn (x, c) => @@ -181,8 +194,24 @@ | CError => string "<ERROR>" | CUnif (_, _, _, ref (SOME c)) => p_con' par env c | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"), - p_kind k, + p_kind env k, string ">"] + + | CKAbs (x, c) => box [string x, + space, + string "==>", + space, + p_con (E.pushKRel env x) c] + | CKApp (c, k) => box [p_con env c, + string "[[", + p_kind env k, + string "]]"] + | TKFun (x, c) => box [string x, + space, + string "-->", + space, + p_con (E.pushKRel env x) c] + and p_con env = p_con' false env @@ -286,7 +315,7 @@ space, p_explicitness exp, space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -377,8 +406,6 @@ space, p_con' true env c]) - | EFold _ => string "fold" - | ECase (e, pes, _) => parenIf par (box [string "case", space, p_exp env e, @@ -415,6 +442,16 @@ string "end"] end + | EKAbs (x, e) => box [string x, + space, + string "==>", + space, + p_exp (E.pushKRel env x) e] + | EKApp (e, k) => box [p_exp env e, + string "[[", + p_kind env k, + string "]]"] + and p_exp env = p_exp' false env and p_edecl env (dAll as (d, _)) = @@ -478,14 +515,14 @@ space, string "::", space, - p_kind k] + p_kind env k] | SgiCon (x, n, k, c) => box [string "con", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -540,14 +577,14 @@ space, string "::", space, - p_kind k] + p_kind env k] | SgiClass (x, n, k, c) => box [string "class", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -627,7 +664,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -719,7 +756,7 @@ space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space,