Mercurial > urweb
diff src/elab_print.sml @ 31:1c91c5e6840f
Simple signature matching
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 12 Jun 2008 17:16:20 -0400 |
parents | 537db4ee89f4 |
children | 0ff8c2728634 |
line wrap: on
line diff
--- a/src/elab_print.sml Thu Jun 12 14:04:22 2008 -0400 +++ b/src/elab_print.sml Thu Jun 12 17:16:20 2008 -0400 @@ -228,57 +228,119 @@ and p_exp env = p_exp' false env +fun p_named x n = + if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + +fun p_sgn_item env (sgi, _) = + case sgi of + SgiConAbs (x, n, k) => box [string "con", + space, + p_named x n, + space, + string "::", + space, + p_kind k] + | SgiCon (x, n, k, c) => box [string "con", + space, + p_named x n, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + | SgiVal (x, n, c) => box [string "val", + space, + p_named x n, + space, + string ":", + space, + p_con env c] + | SgiStr (x, n, sgn) => box [string "structure", + space, + p_named x n, + space, + string ":", + space, + p_sgn env sgn] + +and p_sgn env (sgn, _) = + case sgn of + SgnConst sgis => box [string "sig", + newline, + p_list_sep newline (p_sgn_item env) sgis, + newline, + string "end"] + | SgnVar n => string (#1 (E.lookupSgnNamed env n)) + | SgnError => string "<ERROR>" + fun p_decl env ((d, _) : decl) = case d of - DCon (x, n, k, c) => - let - val xp = if !debug then - box [string x, - string "__", - string (Int.toString n)] - else - string x - in - box [string "con", - space, - xp, - space, - string "::", - space, - p_kind k, - space, - string "=", - space, - p_con env c] - end - | DVal (x, n, t, e) => - let - val xp = if !debug then - box [string x, - string "__", - string (Int.toString n)] - else - string x - in - box [string "val", - space, - xp, - space, - string ":", - space, - p_con env t, - space, - string "=", - space, - p_exp env e] - end + DCon (x, n, k, c) => box [string "con", + space, + p_named x n, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + | DVal (x, n, t, e) => box [string "val", + space, + p_named x n, + space, + string ":", + space, + p_con env t, + space, + string "=", + space, + p_exp env e] + + | DSgn (x, n, sgn) => box [string "signature", + space, + p_named x n, + space, + string "=", + space, + p_sgn env sgn] + | DStr (x, n, sgn, str) => box [string "structure", + space, + p_named x n, + space, + string ":", + space, + p_sgn env sgn, + space, + string "=", + space, + p_str env str] + +and p_str env (str, _) = + case str of + StrConst ds => box [string "struct", + newline, + p_list_sep newline (p_decl env) ds, + newline, + string "end"] + | StrVar n => string (#1 (E.lookupStrNamed env n)) + | StrError => string "<ERROR>" fun p_file env file = let - val (_, pds) = ListUtil.mapfoldl (fn (d, env) => - (E.declBinds env d, - p_decl env d)) - env file + val (pds, _) = ListUtil.foldlMap (fn (d, env) => + (p_decl env d, + E.declBinds env d)) + env file in p_list_sep newline (fn x => x) pds end