adamc@3: (* Copyright (c) 2008, Adam Chlipala adamc@3: * All rights reserved. adamc@3: * adamc@3: * Redistribution and use in source and binary forms, with or without adamc@3: * modification, are permitted provided that the following conditions are met: adamc@3: * adamc@3: * - Redistributions of source code must retain the above copyright notice, adamc@3: * this list of conditions and the following disclaimer. adamc@3: * - Redistributions in binary form must reproduce the above copyright notice, adamc@3: * this list of conditions and the following disclaimer in the documentation adamc@3: * and/or other materials provided with the distribution. adamc@3: * - The names of contributors may not be used to endorse or promote products adamc@3: * derived from this software without specific prior written permission. adamc@3: * adamc@3: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@3: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@3: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@3: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@3: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@3: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@3: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@3: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@3: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@3: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@3: * POSSIBILITY OF SUCH DAMAGE. adamc@3: *) adamc@3: adamc@3: (* Pretty-printing elaborated Laconic/Web *) adamc@3: adamc@3: structure ElabPrint :> ELAB_PRINT = struct adamc@3: adamc@3: open Print.PD adamc@3: open Print adamc@3: adamc@3: open Elab adamc@3: adamc@3: structure E = ElabEnv adamc@3: adamc@11: val debug = ref false adamc@11: adamc@3: fun p_kind' par (k, _) = adamc@3: case k of adamc@3: KType => string "Type" adamc@3: | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, adamc@3: space, adamc@3: string "->", adamc@3: space, adamc@3: p_kind k2]) adamc@3: | KName => string "Name" adamc@3: | KRecord k => box [string "{", p_kind k, string "}"] adamc@3: adamc@3: | KError => string "" adamc@3: | KUnif (_, ref (SOME k)) => p_kind' par k adamc@3: | KUnif (s, _) => string ("") adamc@3: adamc@3: and p_kind k = p_kind' false k adamc@3: adamc@3: fun p_explicitness e = adamc@3: case e of adamc@3: Explicit => string "::" adamc@3: | Implicit => string ":::" adamc@3: adamc@3: fun p_con' par env (c, _) = adamc@3: case c of adamc@3: TFun (t1, t2) => parenIf par (box [p_con' true env t1, adamc@3: space, adamc@3: string "->", adamc@3: space, adamc@3: p_con env t2]) adamc@3: | TCFun (e, x, k, c) => parenIf par (box [string x, adamc@3: space, adamc@3: p_explicitness e, adamc@3: space, adamc@3: p_kind k, adamc@3: space, adamc@3: string "->", adamc@3: space, adamc@3: p_con (E.pushCRel env x k) c]) adamc@3: | TRecord (CRecord (_, xcs), _) => box [string "{", adamc@3: p_list (fn (x, c) => adamc@20: box [p_name env x, adamc@3: space, adamc@3: string ":", adamc@3: space, adamc@3: p_con env c]) xcs, adamc@3: string "}"] adamc@3: | TRecord c => box [string "$", adamc@3: p_con' true env c] adamc@3: adamc@11: | CRel n => adamc@11: if !debug then adamc@11: string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) adamc@11: else adamc@11: string (#1 (E.lookupCRel env n)) adamc@11: | CNamed n => adamc@34: ((if !debug then adamc@34: string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) adamc@34: else adamc@34: string (#1 (E.lookupCNamed env n))) adamc@34: handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) adamc@34: | CModProj (m1, ms, x) => adamc@34: let adamc@34: val (m1x, sgn) = E.lookupStrNamed env m1 adamc@34: adamc@34: val m1s = if !debug then adamc@34: m1x ^ "__" ^ Int.toString m1 adamc@34: else adamc@34: m1x adamc@34: in adamc@34: p_list_sep (string ".") string (m1x :: ms @ [x]) adamc@34: end adamc@3: adamc@3: | CApp (c1, c2) => parenIf par (box [p_con env c1, adamc@3: space, adamc@3: p_con' true env c2]) adamc@8: | CAbs (x, k, c) => parenIf par (box [string "fn", adamc@8: space, adamc@8: string x, adamc@8: space, adamc@8: string "::", adamc@8: space, adamc@8: p_kind k, adamc@8: space, adamc@8: string "=>", adamc@8: space, adamc@8: p_con (E.pushCRel env x k) c]) adamc@3: adamc@3: | CName s => box [string "#", string s] adamc@3: adamc@12: | CRecord (k, xcs) => adamc@12: if !debug then adamc@12: parenIf par (box [string "[", adamc@12: p_list (fn (x, c) => adamc@12: box [p_con env x, adamc@12: space, adamc@12: string "=", adamc@12: space, adamc@12: p_con env c]) xcs, adamc@12: string "]::", adamc@12: p_kind k]) adamc@12: else adamc@12: parenIf par (box [string "[", adamc@12: p_list (fn (x, c) => adamc@12: box [p_con env x, adamc@12: space, adamc@12: string "=", adamc@12: space, adamc@12: p_con env c]) xcs, adamc@12: string "]"]) adamc@3: | CConcat (c1, c2) => parenIf par (box [p_con' true env c1, adamc@3: space, adamc@3: string "++", adamc@3: space, adamc@3: p_con env c2]) adamc@3: adamc@3: | CError => string "" adamc@6: | CUnif (_, _, ref (SOME c)) => p_con' par env c adamc@6: | CUnif (k, s, _) => box [string (""] adamc@3: adamc@3: and p_con env = p_con' false env adamc@3: adamc@20: and p_name env (all as (c, _)) = adamc@20: case c of adamc@20: CName s => string s adamc@20: | _ => p_con env all adamc@20: adamc@9: fun p_exp' par env (e, _) = adamc@9: case e of adamc@14: EPrim p => Prim.p_t p adamc@14: | ERel n => adamc@11: if !debug then adamc@11: string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) adamc@11: else adamc@11: string (#1 (E.lookupERel env n)) adamc@11: | ENamed n => adamc@11: if !debug then adamc@11: string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) adamc@11: else adamc@11: string (#1 (E.lookupENamed env n)) adamc@34: | EModProj (m1, ms, x) => adamc@34: let adamc@34: val (m1x, sgn) = E.lookupStrNamed env m1 adamc@34: adamc@34: val m1s = if !debug then adamc@34: m1x ^ "__" ^ Int.toString m1 adamc@34: else adamc@34: m1x adamc@34: in adamc@34: p_list_sep (string ".") string (m1x :: ms @ [x]) adamc@34: end adamc@34: adamc@9: | EApp (e1, e2) => parenIf par (box [p_exp env e1, adamc@9: space, adamc@9: p_exp' true env e2]) adamc@26: | EAbs (x, t, _, e) => parenIf par (box [string "fn", adamc@26: space, adamc@26: string x, adamc@26: space, adamc@26: string ":", adamc@26: space, adamc@26: p_con env t, adamc@26: space, adamc@26: string "=>", adamc@26: space, adamc@26: p_exp (E.pushERel env x t) e]) adamc@9: | ECApp (e, c) => parenIf par (box [p_exp env e, adamc@9: space, adamc@9: string "[", adamc@9: p_con env c, adamc@9: string "]"]) adamc@9: | ECAbs (exp, x, k, e) => parenIf par (box [string "fn", adamc@9: space, adamc@9: string x, adamc@9: space, adamc@9: p_explicitness exp, adamc@9: space, adamc@9: p_kind k, adamc@9: space, adamc@9: string "=>", adamc@9: space, adamc@9: p_exp (E.pushCRel env x k) e]) adamc@9: adamc@12: | ERecord xes => box [string "{", adamc@29: p_list (fn (x, e, _) => adamc@21: box [p_name env x, adamc@12: space, adamc@12: string "=", adamc@12: space, adamc@12: p_exp env e]) xes, adamc@12: string "}"] adamc@12: | EField (e, c, {field, rest}) => adamc@12: if !debug then adamc@12: box [p_exp' true env e, adamc@12: string ".", adamc@12: p_con' true env c, adamc@12: space, adamc@12: string "[", adamc@12: p_con env field, adamc@12: space, adamc@12: string " in ", adamc@12: space, adamc@12: p_con env rest, adamc@12: string "]"] adamc@12: else adamc@12: box [p_exp' true env e, adamc@12: string ".", adamc@12: p_con' true env c] adamc@12: adamc@9: | EError => string "" adamc@9: adamc@9: and p_exp env = p_exp' false env adamc@9: adamc@31: fun p_named x n = adamc@31: if !debug then adamc@31: box [string x, adamc@31: string "__", adamc@31: string (Int.toString n)] adamc@31: else adamc@31: string x adamc@31: adamc@31: fun p_sgn_item env (sgi, _) = adamc@31: case sgi of adamc@31: SgiConAbs (x, n, k) => box [string "con", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string "::", adamc@31: space, adamc@31: p_kind k] adamc@31: | SgiCon (x, n, k, c) => box [string "con", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string "::", adamc@31: space, adamc@31: p_kind k, adamc@31: space, adamc@31: string "=", adamc@31: space, adamc@31: p_con env c] adamc@31: | SgiVal (x, n, c) => box [string "val", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string ":", adamc@31: space, adamc@31: p_con env c] adamc@31: | SgiStr (x, n, sgn) => box [string "structure", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string ":", adamc@31: space, adamc@31: p_sgn env sgn] adamc@59: | SgiSgn (x, n, sgn) => box [string "signature", adamc@59: space, adamc@59: p_named x n, adamc@59: space, adamc@59: string "=", adamc@59: space, adamc@59: p_sgn env sgn] adamc@31: adamc@31: and p_sgn env (sgn, _) = adamc@31: case sgn of adamc@31: SgnConst sgis => box [string "sig", adamc@31: newline, adamc@32: let adamc@32: val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) => adamc@32: (p_sgn_item env sgi, adamc@32: E.sgiBinds env sgi)) adamc@32: env sgis adamc@32: in adamc@32: p_list_sep newline (fn x => x) psgis adamc@32: end, adamc@31: newline, adamc@31: string "end"] adamc@31: | SgnVar n => string (#1 (E.lookupSgnNamed env n)) adamc@41: | SgnFun (x, n, sgn, sgn') => box [string "functor", adamc@41: space, adamc@41: string "(", adamc@41: string x, adamc@41: space, adamc@41: string ":", adamc@41: space, adamc@41: p_sgn env sgn, adamc@41: string ")", adamc@41: space, adamc@41: string ":", adamc@41: space, adamc@41: p_sgn (E.pushStrNamedAs env x n sgn) sgn'] adamc@42: | SgnWhere (sgn, x, c) => box [p_sgn env sgn, adamc@42: space, adamc@42: string "where", adamc@42: space, adamc@42: string "con", adamc@42: space, adamc@42: string x, adamc@42: space, adamc@42: string "=", adamc@42: space, adamc@42: p_con env c] adamc@59: | SgnProj (m1, ms, x) => adamc@59: let adamc@59: val (m1x, sgn) = E.lookupStrNamed env m1 adamc@59: adamc@59: val m1s = if !debug then adamc@59: m1x ^ "__" ^ Int.toString m1 adamc@59: else adamc@59: m1x adamc@59: in adamc@59: p_list_sep (string ".") string (m1x :: ms @ [x]) adamc@59: end adamc@31: | SgnError => string "" adamc@31: adamc@3: fun p_decl env ((d, _) : decl) = adamc@3: case d of adamc@31: DCon (x, n, k, c) => box [string "con", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string "::", adamc@31: space, adamc@31: p_kind k, adamc@31: space, adamc@31: string "=", adamc@31: space, adamc@31: p_con env c] adamc@31: | DVal (x, n, t, e) => box [string "val", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string ":", adamc@31: space, adamc@31: p_con env t, adamc@31: space, adamc@31: string "=", adamc@31: space, adamc@31: p_exp env e] adamc@31: adamc@31: | DSgn (x, n, sgn) => box [string "signature", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string "=", adamc@31: space, adamc@31: p_sgn env sgn] adamc@31: | DStr (x, n, sgn, str) => box [string "structure", adamc@31: space, adamc@31: p_named x n, adamc@31: space, adamc@31: string ":", adamc@31: space, adamc@31: p_sgn env sgn, adamc@31: space, adamc@31: string "=", adamc@31: space, adamc@31: p_str env str] adamc@48: | DFfiStr (x, n, sgn) => box [string "extern", adamc@48: space, adamc@48: string "structure", adamc@48: space, adamc@48: p_named x n, adamc@48: space, adamc@48: string ":", adamc@48: space, adamc@48: p_sgn env sgn] adamc@31: adamc@31: and p_str env (str, _) = adamc@31: case str of adamc@31: StrConst ds => box [string "struct", adamc@31: newline, adamc@32: p_file env ds, adamc@31: newline, adamc@31: string "end"] adamc@31: | StrVar n => string (#1 (E.lookupStrNamed env n)) adamc@34: | StrProj (str, s) => box [p_str env str, adamc@34: string ".", adamc@34: string s] adamc@41: | StrFun (x, n, sgn, sgn', str) => adamc@41: let adamc@41: val env' = E.pushStrNamedAs env x n sgn adamc@41: in adamc@41: box [string "functor", adamc@41: space, adamc@41: string "(", adamc@41: string x, adamc@41: space, adamc@41: string ":", adamc@41: space, adamc@41: p_sgn env sgn, adamc@41: string ")", adamc@41: space, adamc@41: string ":", adamc@41: space, adamc@41: p_sgn env' sgn', adamc@41: space, adamc@41: string "=>", adamc@41: space, adamc@41: p_str env' str] adamc@41: end adamc@44: | StrApp (str1, str2) => box [p_str env str1, adamc@44: string "(", adamc@44: p_str env str2, adamc@44: string ")"] adamc@31: | StrError => string "" adamc@3: adamc@32: and p_file env file = adamc@3: let adamc@31: val (pds, _) = ListUtil.foldlMap (fn (d, env) => adamc@31: (p_decl env d, adamc@31: E.declBinds env d)) adamc@31: env file adamc@3: in adamc@3: p_list_sep newline (fn x => x) pds adamc@3: end adamc@3: adamc@3: end