adamc@38: (* Copyright (c) 2008, Adam Chlipala adamc@38: * All rights reserved. adamc@38: * adamc@38: * Redistribution and use in source and binary forms, with or without adamc@38: * modification, are permitted provided that the following conditions are met: adamc@38: * adamc@38: * - Redistributions of source code must retain the above copyright notice, adamc@38: * this list of conditions and the following disclaimer. adamc@38: * - Redistributions in binary form must reproduce the above copyright notice, adamc@38: * this list of conditions and the following disclaimer in the documentation adamc@38: * and/or other materials provided with the distribution. adamc@38: * - The names of contributors may not be used to endorse or promote products adamc@38: * derived from this software without specific prior written permission. adamc@38: * adamc@38: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@38: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@38: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@38: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@38: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@38: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@38: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@38: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@38: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@38: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@38: * POSSIBILITY OF SUCH DAMAGE. adamc@38: *) adamc@38: adamc@38: (* Pretty-printing elaborated Laconic/Web *) adamc@38: adamc@38: structure ExplPrint :> EXPL_PRINT = struct adamc@38: adamc@38: open Print.PD adamc@38: open Print adamc@38: adamc@38: open Expl adamc@38: adamc@38: structure E = ExplEnv adamc@38: adamc@38: val debug = ref false adamc@38: adamc@38: fun p_kind' par (k, _) = adamc@38: case k of adamc@38: KType => string "Type" adamc@38: | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, adamc@38: space, adamc@38: string "->", adamc@38: space, adamc@38: p_kind k2]) adamc@38: | KName => string "Name" adamc@38: | KRecord k => box [string "{", p_kind k, string "}"] adamc@87: | KUnit => string "Unit" adamc@38: adamc@38: and p_kind k = p_kind' false k adamc@38: adamc@38: fun p_con' par env (c, _) = adamc@38: case c of adamc@38: TFun (t1, t2) => parenIf par (box [p_con' true env t1, adamc@38: space, adamc@38: string "->", adamc@38: space, adamc@38: p_con env t2]) adamc@38: | TCFun (x, k, c) => parenIf par (box [string x, adamc@38: space, adamc@38: string "::", adamc@38: space, adamc@38: p_kind k, adamc@38: space, adamc@38: string "->", adamc@38: space, adamc@38: p_con (E.pushCRel env x k) c]) adamc@38: | TRecord (CRecord (_, xcs), _) => box [string "{", adamc@38: p_list (fn (x, c) => adamc@38: box [p_name env x, adamc@38: space, adamc@38: string ":", adamc@38: space, adamc@38: p_con env c]) xcs, adamc@38: string "}"] adamc@38: | TRecord c => box [string "$", adamc@38: p_con' true env c] adamc@38: adamc@38: | CRel n => adamc@38: if !debug then adamc@38: string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) adamc@38: else adamc@38: string (#1 (E.lookupCRel env n)) adamc@38: | CNamed n => adamc@38: ((if !debug then adamc@38: string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) adamc@38: else adamc@38: string (#1 (E.lookupCNamed env n))) adamc@38: handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) adamc@38: | CModProj (m1, ms, x) => adamc@38: let adamc@109: val m1x = #1 (E.lookupStrNamed env m1) adamc@109: handle E.UnboundNamed _ => "UNBOUND" adamc@38: adamc@38: val m1s = if !debug then adamc@38: m1x ^ "__" ^ Int.toString m1 adamc@38: else adamc@38: m1x adamc@38: in adamc@146: p_list_sep (string ".") string (m1s :: ms @ [x]) adamc@38: end adamc@38: adamc@38: | CApp (c1, c2) => parenIf par (box [p_con env c1, adamc@38: space, adamc@38: p_con' true env c2]) adamc@38: | CAbs (x, k, c) => parenIf par (box [string "fn", adamc@38: space, adamc@38: string x, adamc@38: space, adamc@38: string "::", adamc@38: space, adamc@38: p_kind k, adamc@38: space, adamc@38: string "=>", adamc@38: space, adamc@38: p_con (E.pushCRel env x k) c]) adamc@38: adamc@38: | CName s => box [string "#", string s] adamc@38: adamc@38: | CRecord (k, xcs) => adamc@38: if !debug then adamc@38: parenIf par (box [string "[", adamc@38: p_list (fn (x, c) => adamc@38: box [p_con env x, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: p_con env c]) xcs, adamc@38: string "]::", adamc@38: p_kind k]) adamc@38: else adamc@38: parenIf par (box [string "[", adamc@38: p_list (fn (x, c) => adamc@38: box [p_con env x, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: p_con env c]) xcs, adamc@38: string "]"]) adamc@38: | CConcat (c1, c2) => parenIf par (box [p_con' true env c1, adamc@38: space, adamc@38: string "++", adamc@38: space, adamc@38: p_con env c2]) adamc@68: | CFold _ => string "fold" adamc@87: | CUnit => string "()" adamc@38: adamc@38: and p_con env = p_con' false env adamc@38: adamc@38: and p_name env (all as (c, _)) = adamc@38: case c of adamc@38: CName s => string s adamc@38: | _ => p_con env all adamc@38: adamc@176: fun p_patCon env pc = adamc@176: case pc of adamc@176: PConVar n => adamc@176: ((if !debug then adamc@176: string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) adamc@176: else adamc@176: string (#1 (E.lookupENamed env n))) adamc@176: handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n)) adamc@176: | PConProj (m1, ms, x) => adamc@176: let adamc@176: val m1x = #1 (E.lookupStrNamed env m1) adamc@176: handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 adamc@176: adamc@176: val m1s = if !debug then adamc@176: m1x ^ "__" ^ Int.toString m1 adamc@176: else adamc@176: m1x adamc@176: in adamc@176: p_list_sep (string ".") string (m1x :: ms @ [x]) adamc@176: end adamc@176: adamc@176: fun p_pat' par env (p, _) = adamc@176: case p of adamc@176: PWild => string "_" adamc@176: | PVar s => string s adamc@176: | PPrim p => Prim.p_t p adamc@176: | PCon (pc, NONE) => p_patCon env pc adamc@176: | PCon (pc, SOME p) => parenIf par (box [p_patCon env pc, adamc@176: space, adamc@176: p_pat' true env p]) adamc@176: | PRecord xps => adamc@176: box [string "{", adamc@176: p_list_sep (box [string ",", space]) (fn (x, p) => adamc@176: box [string x, adamc@176: space, adamc@176: string "=", adamc@176: space, adamc@176: p_pat env p]) xps, adamc@176: string "}"] adamc@176: adamc@176: and p_pat x = p_pat' false x adamc@176: adamc@146: fun p_exp' par env (e, loc) = adamc@38: case e of adamc@38: EPrim p => Prim.p_t p adamc@38: | ERel n => adamc@38: if !debug then adamc@38: string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) adamc@38: else adamc@38: string (#1 (E.lookupERel env n)) adamc@38: | ENamed n => adamc@38: if !debug then adamc@38: string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) adamc@38: else adamc@38: string (#1 (E.lookupENamed env n)) adamc@38: | EModProj (m1, ms, x) => adamc@38: let adamc@38: val (m1x, sgn) = E.lookupStrNamed env m1 adamc@146: handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc)) adamc@38: adamc@38: val m1s = if !debug then adamc@38: m1x ^ "__" ^ Int.toString m1 adamc@38: else adamc@38: m1x adamc@38: in adamc@146: p_list_sep (string ".") string (m1s :: ms @ [x]) adamc@38: end adamc@38: adamc@38: | EApp (e1, e2) => parenIf par (box [p_exp env e1, adamc@38: space, adamc@38: p_exp' true env e2]) adamc@38: | EAbs (x, t, _, e) => parenIf par (box [string "fn", adamc@38: space, adamc@38: string x, adamc@38: space, adamc@38: string ":", adamc@38: space, adamc@38: p_con env t, adamc@38: space, adamc@38: string "=>", adamc@38: space, adamc@38: p_exp (E.pushERel env x t) e]) adamc@38: | ECApp (e, c) => parenIf par (box [p_exp env e, adamc@38: space, adamc@38: string "[", adamc@38: p_con env c, adamc@38: string "]"]) adamc@38: | ECAbs (x, k, e) => parenIf par (box [string "fn", adamc@38: space, adamc@38: string x, adamc@38: space, adamc@38: string "::", adamc@38: space, adamc@38: p_kind k, adamc@38: space, adamc@38: string "=>", adamc@38: space, adamc@38: p_exp (E.pushCRel env x k) e]) adamc@38: adamc@38: | ERecord xes => box [string "{", adamc@38: p_list (fn (x, e, _) => adamc@38: box [p_name env x, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: p_exp env e]) xes, adamc@38: string "}"] adamc@38: | EField (e, c, {field, rest}) => adamc@38: if !debug then adamc@38: box [p_exp' true env e, adamc@38: string ".", adamc@38: p_con' true env c, adamc@38: space, adamc@38: string "[", adamc@38: p_con env field, adamc@38: space, adamc@38: string " in ", adamc@38: space, adamc@38: p_con env rest, adamc@38: string "]"] adamc@38: else adamc@38: box [p_exp' true env e, adamc@38: string ".", adamc@38: p_con' true env c] adamc@149: | ECut (e, c, {field, rest}) => adamc@149: parenIf par (if !debug then adamc@149: box [p_exp' true env e, adamc@149: space, adamc@149: string "--", adamc@149: space, adamc@149: p_con' true env c, adamc@149: space, adamc@149: string "[", adamc@149: p_con env field, adamc@149: space, adamc@149: string " in ", adamc@149: space, adamc@149: p_con env rest, adamc@149: string "]"] adamc@149: else adamc@149: box [p_exp' true env e, adamc@149: space, adamc@149: string "--", adamc@149: space, adamc@149: p_con' true env c]) adamc@72: | EFold _ => string "fold" adamc@38: adamc@109: | EWrite e => box [string "write(", adamc@109: p_exp env e, adamc@109: string ")"] adamc@109: adamc@176: | ECase (e, pes, _) => parenIf par (box [string "case", adamc@176: space, adamc@176: p_exp env e, adamc@176: space, adamc@176: string "of", adamc@176: space, adamc@176: p_list_sep (box [space, string "|", space]) adamc@176: (fn (p, e) => box [p_pat env p, adamc@176: space, adamc@176: string "=>", adamc@176: space, adamc@176: p_exp env e]) pes]) adamc@176: adamc@38: and p_exp env = p_exp' false env adamc@38: adamc@38: fun p_named x n = adamc@38: if !debug then adamc@38: box [string x, adamc@38: string "__", adamc@38: string (Int.toString n)] adamc@38: else adamc@38: string x adamc@38: adamc@162: fun p_datatype env (x, n, cons) = adamc@162: let adamc@162: val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE adamc@162: in adamc@162: box [string "datatype", adamc@162: space, adamc@162: string x, adamc@162: space, adamc@162: string "=", adamc@162: space, adamc@162: p_list_sep (box [space, string "|", space]) adamc@163: (fn (x, n, NONE) => if !debug then (string (x ^ "__" ^ Int.toString n)) adamc@163: else string x adamc@163: | (x, _, SOME t) => box [if !debug then (string (x ^ "__" ^ Int.toString n)) adamc@163: else string x, space, string "of", space, p_con env t]) adamc@162: cons] adamc@162: end adamc@162: adamc@38: fun p_sgn_item env (sgi, _) = adamc@38: case sgi of adamc@38: SgiConAbs (x, n, k) => box [string "con", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string "::", adamc@38: space, adamc@38: p_kind k] adamc@38: | SgiCon (x, n, k, c) => box [string "con", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string "::", adamc@38: space, adamc@38: p_kind k, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: p_con env c] adamc@162: | SgiDatatype x => p_datatype env x adamc@162: | SgiDatatypeImp (x, _, m1, ms, x', _) => adamc@162: let adamc@162: val m1x = #1 (E.lookupStrNamed env m1) adamc@162: handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 adamc@162: in adamc@162: box [string "datatype", adamc@162: space, adamc@162: string x, adamc@162: space, adamc@162: string "=", adamc@162: space, adamc@162: string "datatype", adamc@162: space, adamc@162: p_list_sep (string ".") string (m1x :: ms @ [x'])] adamc@162: end adamc@38: | SgiVal (x, n, c) => box [string "val", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string ":", adamc@38: space, adamc@38: p_con env c] adamc@38: | SgiStr (x, n, sgn) => box [string "structure", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string ":", adamc@38: space, adamc@38: p_sgn env sgn] adamc@64: | SgiSgn (x, n, sgn) => box [string "signature", adamc@64: space, adamc@64: p_named x n, adamc@64: space, adamc@64: string "=", adamc@64: space, adamc@64: p_sgn env sgn] adamc@38: adamc@146: and p_sgn env (sgn, loc) = adamc@38: case sgn of adamc@38: SgnConst sgis => box [string "sig", adamc@38: newline, adamc@38: let adamc@38: val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) => adamc@38: (p_sgn_item env sgi, adamc@38: E.sgiBinds env sgi)) adamc@38: env sgis adamc@38: in adamc@38: p_list_sep newline (fn x => x) psgis adamc@38: end, adamc@38: newline, adamc@38: string "end"] adamc@146: | SgnVar n => string ((#1 (E.lookupSgnNamed env n)) adamc@146: handle E.UnboundNamed _ => "UNBOUND") adamc@45: | SgnFun (x, n, sgn, sgn') => box [string "functor", adamc@45: space, adamc@45: string "(", adamc@45: string x, adamc@45: space, adamc@45: string ":", adamc@45: space, adamc@45: p_sgn env sgn, adamc@45: string ")", adamc@45: space, adamc@45: string ":", adamc@45: space, adamc@45: p_sgn (E.pushStrNamed env x n sgn) sgn'] adamc@45: | SgnWhere (sgn, x, c) => box [p_sgn env sgn, adamc@45: space, adamc@45: string "where", adamc@45: space, adamc@45: string "con", adamc@45: space, adamc@45: string x, adamc@45: space, adamc@45: string "=", adamc@45: space, adamc@45: p_con env c] adamc@64: | SgnProj (m1, ms, x) => adamc@64: let adamc@64: val (m1x, sgn) = E.lookupStrNamed env m1 adamc@146: handle E.UnboundNamed _ => ("UNBOUND", (SgnConst [], loc)) adamc@64: adamc@64: val m1s = if !debug then adamc@64: m1x ^ "__" ^ Int.toString m1 adamc@64: else adamc@64: m1x adamc@64: in adamc@64: p_list_sep (string ".") string (m1x :: ms @ [x]) adamc@64: end adamc@38: adamc@124: fun p_vali env (x, n, t, e) = box [p_named x n, adamc@124: space, adamc@124: string ":", adamc@124: space, adamc@124: p_con env t, adamc@124: space, adamc@124: string "=", adamc@124: space, adamc@124: p_exp env e] adamc@124: adamc@124: fun p_decl env (dAll as (d, _) : decl) = adamc@38: case d of adamc@38: DCon (x, n, k, c) => box [string "con", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string "::", adamc@38: space, adamc@38: p_kind k, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: p_con env c] adamc@162: | DDatatype x => p_datatype env x adamc@162: | DDatatypeImp (x, _, m1, ms, x', _) => adamc@162: let adamc@162: val m1x = #1 (E.lookupStrNamed env m1) adamc@162: handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 adamc@162: in adamc@162: box [string "datatype", adamc@162: space, adamc@162: string x, adamc@162: space, adamc@162: string "=", adamc@162: space, adamc@162: string "datatype", adamc@162: space, adamc@162: p_list_sep (string ".") string (m1x :: ms @ [x'])] adamc@162: end adamc@124: | DVal vi => box [string "val", adamc@124: space, adamc@124: p_vali env vi] adamc@124: | DValRec vis => adamc@124: let adamc@124: val env = E.declBinds env dAll adamc@124: in adamc@124: box [string "val", adamc@124: space, adamc@124: string "rec", adamc@124: space, adamc@124: p_list_sep (box [newline, string "and", space]) (p_vali env) vis] adamc@124: end adamc@38: adamc@38: | DSgn (x, n, sgn) => box [string "signature", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: p_sgn env sgn] adamc@38: | DStr (x, n, sgn, str) => box [string "structure", adamc@38: space, adamc@38: p_named x n, adamc@38: space, adamc@38: string ":", adamc@38: space, adamc@38: p_sgn env sgn, adamc@38: space, adamc@38: string "=", adamc@38: space, adamc@38: 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@109: | DExport (_, sgn, str) => box [string "export", adamc@109: space, adamc@109: p_str env str, adamc@109: space, adamc@109: string ":", adamc@109: space, adamc@109: p_sgn env sgn] adamc@38: adamc@38: and p_str env (str, _) = adamc@38: case str of adamc@38: StrConst ds => box [string "struct", adamc@38: newline, adamc@38: p_file env ds, adamc@38: newline, adamc@38: string "end"] adamc@146: | StrVar n => adamc@146: let adamc@146: val x = #1 (E.lookupStrNamed env n) adamc@146: handle E.UnboundNamed _ => "UNBOUND" adamc@146: adamc@146: val s = if !debug then adamc@146: x ^ "__" ^ Int.toString n adamc@146: else adamc@146: x adamc@146: in adamc@146: string s adamc@146: end adamc@38: | StrProj (str, s) => box [p_str env str, adamc@38: string ".", adamc@38: string s] adamc@45: | StrFun (x, n, sgn, sgn', str) => adamc@45: let adamc@45: val env' = E.pushStrNamed env x n sgn adamc@45: in adamc@45: box [string "functor", adamc@45: space, adamc@45: string "(", adamc@45: string x, adamc@45: space, adamc@45: string ":", adamc@45: space, adamc@45: p_sgn env sgn, adamc@45: string ")", adamc@45: space, adamc@45: string ":", adamc@45: space, adamc@45: p_sgn env' sgn', adamc@45: space, adamc@45: string "=>", adamc@45: space, adamc@45: p_str env' str] adamc@45: end adamc@45: | StrApp (str1, str2) => box [p_str env str1, adamc@45: string "(", adamc@45: p_str env str2, adamc@45: string ")"] adamc@38: adamc@38: and p_file env file = adamc@38: let adamc@38: val (pds, _) = ListUtil.foldlMap (fn (d, env) => adamc@38: (p_decl env d, adamc@38: E.declBinds env d)) adamc@38: env file adamc@38: in adamc@38: p_list_sep newline (fn x => x) pds adamc@38: end adamc@38: adamc@38: end