## latex-print-package-language.pkg
## Copyright 2003 by The SML/NJ Fellowship
# Compiled by:
# src/lib/compiler/front/typer/typer.sublib# Invoked from src/lib/compiler/front/typer-stuff/symbolmapstack/latex-print-symbolmapstack.pkg# This is a clone of unparse-package-language.pkg
# specialized to produce LaTeX output intended to be
# run through Hevea to produce online HTML docs of
# our interfaces.
#
# Modified to use Mythryl stdlib prettyprinter. [dbm, 7/30/03])
stipulate
package mld = module_level_declarations; # module_level_declarations is from src/lib/compiler/front/typer-stuff/modules/module-level-declarations.pkg package mtt = more_type_types; # more_type_types is from src/lib/compiler/front/typer/types/more-type-types.pkg package pp = standard_prettyprinter; # standard_prettyprinter is from src/lib/prettyprint/big/src/standard-prettyprinter.pkg package sxe = symbolmapstack_entry; # symbolmapstack_entry is from src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack-entry.pkg package syx = symbolmapstack; # symbolmapstack is from src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack.pkgherein
api Latex_Print_Package_Language {
#
latex_print_api
:
pp::Prettyprinter
->
( mld::Api,
syx::Symbolmapstack,
Int, # Max prettyprint recursion depth
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
latex_print_package
:
pp::Prettyprinter
->
( mld::Package,
syx::Symbolmapstack,
Int, # Max prettyprint recursion depth
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
latex_print_open
:
pp::Prettyprinter
->
( symbol_path::Symbol_Path,
mld::Package,
syx::Symbolmapstack,
Int, # Max prettyprint recursion depth
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
latex_print_package_name
:
pp::Prettyprinter
->
( mld::Package,
syx::Symbolmapstack
)
->
Void;
latex_print_generic
:
pp::Prettyprinter
->
( mld::Generic,
syx::Symbolmapstack,
Int, # Max prettyprint recursion depth
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
latex_print_generic_api
:
pp::Prettyprinter
->
( mld::Generic_Api,
syx::Symbolmapstack,
Int, # Max prettyprint recursion depth
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
latex_print_naming
:
pp::Prettyprinter
->
( symbol::Symbol,
sxe::Symbolmapstack_Entry,
syx::Symbolmapstack,
Int, # Max prettyprint recursion depth
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
latex_print_dictionary
:
pp::Prettyprinter
->
( syx::Symbolmapstack,
syx::Symbolmapstack,
Int,
Null_Or( List( symbol::Symbol ) ),
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
->
Void;
# module internals
latex_print_elements
:
( syx::Symbolmapstack,
Int,
Null_Or( mld::Typerstore ),
Ref( List( String ) ) # index_entries -- a return value list of strings like "(backslash)index[fun]{foo}" her
)
-> pp::Prettyprinter
-> mld::Api_Elements
-> Void;
latex_print_typechecked_package
:
pp::Prettyprinter
->
( mld::Typerstore_Entry,
syx::Symbolmapstack,
Int
)
->
Void;
latex_print_typerstore
:
pp::Prettyprinter
->
( mld::Typerstore,
syx::Symbolmapstack,
Int
)
->
Void;
};
end;
stipulate
package a = varhome; # varhome is from src/lib/compiler/front/typer-stuff/basics/varhome.pkg package b = symbolmapstack_entry; # symbolmapstack_entry is from src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack-entry.pkg package id = inlining_data; # inlining_data is from src/lib/compiler/front/typer-stuff/basics/inlining-data.pkg package ip = inverse_path; # inverse_path is from src/lib/compiler/front/typer-stuff/basics/symbol-path.pkg package lu = find_in_symbolmapstack; # find_in_symbolmapstack is from src/lib/compiler/front/typer-stuff/symbolmapstack/find-in-symbolmapstack.pkg package mj = module_junk; # module_junk is from src/lib/compiler/front/typer-stuff/modules/module-junk.pkg package mld = module_level_declarations; # module_level_declarations is from src/lib/compiler/front/typer-stuff/modules/module-level-declarations.pkg package mtt = more_type_types; # more_type_types is from src/lib/compiler/front/typer/types/more-type-types.pkg package pp = standard_prettyprinter; # standard_prettyprinter is from src/lib/prettyprint/big/src/standard-prettyprinter.pkg package s = symbol; # symbol is from src/lib/compiler/front/basics/map/symbol.pkg package sp = symbol_path; # symbol_path is from src/lib/compiler/front/typer-stuff/basics/symbol-path.pkg package syx = symbolmapstack; # symbolmapstack is from src/lib/compiler/front/typer-stuff/symbolmapstack/symbolmapstack.pkg package tdt = type_declaration_types; # type_declaration_types is from src/lib/compiler/front/typer-stuff/types/type-declaration-types.pkg package tro = typerstore; # typerstore is from src/lib/compiler/front/typer-stuff/modules/typerstore.pkg package tu = type_junk; # type_junk is from src/lib/compiler/front/typer-stuff/types/type-junk.pkg package uj = unparse_junk; # unparse_junk is from src/lib/compiler/front/typer/print/unparse-junk.pkg package vac = variables_and_constructors; # variables_and_constructors is from src/lib/compiler/front/typer-stuff/deep-syntax/variables-and-constructors.pkg # package id = inlining_data
#
Pp = pp::Pp;
herein
package latex_print_package_language
: (weak) Latex_Print_Package_Language
{
# typer_control is from src/lib/compiler/front/typer/basics/typer-control.pkg# internals = typer_control::internals;
internals = log::internals;
fun bug msg
=
error_message::impossible("latex_print_package_language: " + msg);
fun by f x y
=
f y x;
latex_print_some_type = latex_print_type::latex_print_some_type;
latex_print_type = latex_print_type::latex_print_type;
latex_print_typescheme = latex_print_type::latex_print_typescheme;
latex_print_formals = latex_print_type::latex_print_formals;
backslash_latex_special_chars = latex_print_value::backslash_latex_special_chars;
result_id
=
s::make_package_symbol "<result_package>";
fun str_to_dictionary ( mld::API { api_elements, ... }, entities)
=>
fold_forward bind_element syx::empty api_elements
where
fun bind_element ((symbol, spec), symbolmapstack)
=
case spec
#
mld::TYPE_IN_API { module_stamp, ... }
=>
{ type = tro::find_type_by_module_stamp (entities, module_stamp);
#
syx::bind (symbol, b::NAMED_TYPE type, symbolmapstack );
};
mld::PACKAGE_IN_API { module_stamp, an_api, ... }
=>
{ typechecked_package
=
tro::find_package_by_module_stamp (entities, module_stamp);
syx::bind (
symbol,
b::NAMED_PACKAGE (
mld::A_PACKAGE {
an_api,
typechecked_package,
varhome => a::null_varhome,
inlining_data => id::NIL
}
),
symbolmapstack
);
};
mld::VALCON_IN_API { sumtype, ... }
=>
syx::bind (symbol, b::NAMED_CONSTRUCTOR sumtype, symbolmapstack);
_ => symbolmapstack;
esac;
end;
str_to_dictionary _
=>
syx::empty;
end;
fun api_to_symbolmapstack ( mld::API { api_elements, ... } )
=>
fold_forward bind_element syx::empty api_elements
where
fun bind_element ((symbol, spec), symbolmapstack)
=
case spec
#
mld::TYPE_IN_API { type, ... }
=>
syx::bind (symbol, b::NAMED_TYPE type, symbolmapstack);
mld::PACKAGE_IN_API { an_api, slot, definition, module_stamp=>ev }
=>
syx::bind (
symbol,
b::NAMED_PACKAGE (
mld::PACKAGE_API {
an_api,
stamppath => [ev]
}
),
symbolmapstack
);
mld::VALCON_IN_API { sumtype, ... }
=>
syx::bind (symbol, b::NAMED_CONSTRUCTOR sumtype, symbolmapstack);
_ =>
symbolmapstack;
esac;
end;
api_to_symbolmapstack _
=>
bug "api_to_symbolmapstack";
end;
# Support for a hack to make sure that non-visible ConNamings don't
# cause spurious blank lines when latex_print-ing apis.
#
fun is_latex_printable_valcon_naming (tdt::VALCON { form=>a::EXCEPTION _, ... }, _)
=>
TRUE;
is_latex_printable_valcon_naming (con, symbolmapstack)
=>
{ exception HIDDEN;
visible_valcon_type
=
{ type = tu::sumtype_to_type con;
( tu::type_equality
( lu::find_type_via_symbol_path
( symbolmapstack,
sp::SYMBOL_PATH [ ip::last (tu::namepath_of_type type) ],
\\ _ = raise exception HIDDEN
),
type
)
except
HIDDEN = FALSE
);
};
( *internals or
not visible_valcon_type
);
};
end;
fun all_latex_printable_namings alist symbolmapstack
=
list::filter
\\ (name, b::NAMED_CONSTRUCTOR con)
=>
is_latex_printable_valcon_naming (con, symbolmapstack);
b =>
TRUE;
end
alist;
fun latex_print_lty (pp:Pp) ( /* lambdaty, depth */ )
=
pp.lit "<lambdaty>";
fun latex_print_typechecked_package_variable (pp:Pp) module_stamp
=
pp.lit (stamppath::module_stamp_to_string module_stamp);
fun latex_print_stamppath (pp:Pp) stamppath
=
pp.lit (stamppath::stamppath_to_string stamppath);
/* prettyprintClosedSequence pp
{ front=(\\ pp => pp.lit "["),
sep=(\\ pp => (pp.lit ", "; break pp { blanks=0, indent_on_wrap=0 } )),
back=(\\ pp => pp.lit "]"),
style= uj::INCONSISTENT,
pr=prettyprintMacroExpansionVariable }
*/
fun latex_print_type_expression pp (type_expression, depth)
=
if (depth <= 0)
pp.lit "<typeConstructorExpression>";
else
case type_expression
#
mld::TYPEVAR_TYPE ep
=>
{ pp.lit "te::V:";
pp::break pp { blanks=>1, indent_on_wrap=>1 };
latex_print_stamppath pp ep;
};
mld::CONSTANT_TYPE type
=>
{ pp.lit "te::C:";
pp::break pp { blanks=>1, indent_on_wrap=>1 };
latex_print_type syx::empty pp type;
};
mld::FORMAL_TYPE type
=>
{ pp.lit "te::FM:";
pp::break pp { blanks=>1, indent_on_wrap=>1 };
latex_print_type syx::empty pp type;
};
esac;
fi;
fun latex_print_package_name (pp:Pp) (str, symbolmapstack)
=
{ inverse_path
=
case str
#
mld::A_PACKAGE { typechecked_package, ... }
=>
typechecked_package.inverse_path;
_ => bug "latex_print_package_name";
esac;
fun get a
=
lu::find_package_via_symbol_path (
symbolmapstack,
a,
(\\ _ = raise exception syx::UNBOUND)
);
fun check str'
=
mj::eq_origin (str', str);
my (syms, found)
=
uj::find_path (inverse_path, check, get);
pp.lit ( found ?? sp::to_string (sp::SYMBOL_PATH syms)
:: "?" + (sp::to_string (sp::SYMBOL_PATH syms))
);
};
fun latex_print_variable pp
=
latex_print_v
where
fun latex_print_v ( vac::PLAIN_VARIABLE { path, varhome, vartypoid_ref, inlining_data },
symbolmapstack: syx::Symbolmapstack
)
=>
{ pp.box' 0 -1 {. pp.rulename "lppl1";
pp.lit (sp::to_string path);
if *internals
latex_print_value::latex_print_varhome pp varhome;
fi;
pp.txt " : ";
latex_print_some_type symbolmapstack pp *vartypoid_ref;
};
};
latex_print_v (vac::OVERLOADED_VARIABLE { name, alternatives, typescheme=>tdt::TYPESCHEME { body, ... } }, symbolmapstack)
=>
{ pp.box' 0 -1 {. pp.rulename "lppl2";
uj::unparse_symbol pp (name);
pp.txt " : ";
latex_print_some_type symbolmapstack pp body;
pp.txt " as ";
uj::unparse_sequence pp
{ separator => \\ pp = pp.txt " ",
print_one => (\\ pp = \\ { variant, ... } = latex_print_v (variant, symbolmapstack)),
breakstyle => uj::ALIGN
}
*alternatives;
};
};
latex_print_v (vac::ERROR_VARIABLE, _)
=>
pp.lit "<ERROR_VARIABLE>";
end;
end;
fun latex_print_con_naming pp
=
latex_print_con
where
fun latex_print_con (tdt::VALCON { name, typoid, form=>a::EXCEPTION _, ... }, symbolmapstack)
=>
{ pp.wrap {. pp.rulename "pphctw13";
pp.lit "exception "; uj::unparse_symbol pp name;
if (mtt::is_arrow_type typoid)
#
# pp.txt " of ";
pp.txt " ";
latex_print_some_type symbolmapstack pp (mtt::domain typoid);
fi;
};
};
latex_print_con (con as tdt::VALCON { name, typoid, ... }, symbolmapstack)
=>
if *internals
#
pp.wrap {. pp.rulename "pphctw14";
pp.txt "Constructor ";
uj::unparse_symbol pp name;
pp.txt " : ";
latex_print_some_type symbolmapstack pp typoid;
};
fi;
end;
end;
fun latex_print_package pp (pkg, symbolmapstack, depth, index_entries)
=
case pkg
#
mld::A_PACKAGE { an_api, typechecked_package as { typerstore, ... }, ... }
=>
if *internals
#
pp.box' 0 2 {. pp.rulename "lppl3";
pp.lit "A_PACKAGE";
uj::newline_indent pp 2;
pp.box' 0 -1 {. pp.rulename "lppl4";
pp.txt' 1 2 "an_api: ";
latex_print_api0 pp (an_api, symbolmapstack, depth - 1, THE typerstore, index_entries);
pp.newline();
pp.txt' 1 2 "typechecked_package:";
latex_print_generics_expansion pp (typechecked_package, symbolmapstack, depth - 1);
};
};
else
case an_api
#
mld::API { name => THE symbol, ... }
=>
( ( if (mj::apis_equal (
an_api,
lu::find_api_by_symbol (
symbolmapstack,
symbol,
(\\ _ = raise exception syx::UNBOUND)
)
)
)
uj::unparse_symbol pp symbol;
else
uj::unparse_symbol pp symbol;
pp.lit "?";
fi
)
except
syx::UNBOUND
=
{ uj::unparse_symbol pp symbol;
pp.lit "?";
}
);
mld::API { name => NULL, ... }
=>
if (depth <= 1)
#
pp.lit "<sig>";
else
latex_print_api0 pp
(an_api, symbolmapstack, depth - 1, THE typerstore, index_entries);
fi;
mld::ERRONEOUS_API
=>
pp.lit "<error sig>";
esac;
fi;
mld::PACKAGE_API _ => pp.lit "<pkg api>";
mld::ERRONEOUS_PACKAGE => pp.lit "<error str>";
esac
also
fun latex_print_elements (symbolmapstack, depth, typechecked_package_env_op, index_entries) (pp:Pp) elements
=
{ fun pr first (symbol, spec)
=
case spec
#
mld::PACKAGE_IN_API { an_api, module_stamp, definition, slot }
=>
{ if (not first)
pp.newline();
fi;
pp.box {. pp.rulename "lppl5";
pp.lit "package ";
uj::unparse_symbol pp symbol;
pp.txt' 1 2 " : ";
pp.box {. pp.rulename "lppl6";
case typechecked_package_env_op
#
NULL
=>
latex_print_api0
pp
( an_api,
symbolmapstack,
depth - 1,
NULL,
index_entries
);
THE eenv
=>
{ my { typerstore, ... }
=
case (tro::find_entry_by_module_stamp (eenv, module_stamp))
#
mld::PACKAGE_ENTRY e
=>
e;
_ => bug "latex_print_elements: PACKAGE_ENTRY";
esac;
latex_print_api0 pp (an_api, symbolmapstack, depth - 1, THE typerstore, index_entries);
};
esac;
if *internals
#
pp.newline();
pp.txt "module_stamp: ";
pp.lit (stamppath::module_stamp_to_string module_stamp);
fi;
pp.endlit ";";
};
};
};
mld::GENERIC_IN_API { a_generic_api, module_stamp, slot }
=>
{ if (not first)
pp.newline();
fi;
pp.box {. pp.rulename "lppl7";
pp.lit "generic package ";
uj::unparse_symbol pp symbol;
pp.lit " :";
pp.txt' 0 2 " ";
pp.box {. pp.rulename "lppl8";
#
latex_print_generic_api pp (a_generic_api, symbolmapstack, depth - 1, index_entries);
if *internals
pp.newline();
pp.lit "module_stamp: ";
pp.lit (stamppath::module_stamp_to_string module_stamp);
fi;
pp.lit ";";
};
};
};
mld::TYPE_IN_API { type=>spec, module_stamp, is_a_replica, scope }
=>
{ if (not first)
pp.newline();
fi;
pp.box {. pp.rulename "lppl9";
#
case typechecked_package_env_op
#
NULL =>
if is_a_replica latex_print_replicate_naming pp (spec, symbolmapstack);
else latex_print_type_bind pp (spec, symbolmapstack);
fi;
THE eenv
=>
case (tro::find_entry_by_module_stamp (eenv, module_stamp))
#
mld::TYPE_ENTRY type
=>
if is_a_replica
#
latex_print_replicate_naming pp (type, symbolmapstack);
else
latex_print_type_bind pp (type, symbolmapstack);
fi;
mld::ERRONEOUS_ENTRY
=>
pp.lit "<ERRONEOUS_ENTRY>";
_ =>
bug "latex_print_elements: TYPE_ENTRY";
esac;
esac;
if *internals
pp.newline();
pp.lit "module_stamp: ";
pp.lit (stamppath::module_stamp_to_string module_stamp);
pp.newline();
pp.lit "scope: ";
pp.lit (int::to_string scope);
fi;
pp.endlit ";";
};
};
mld::VALUE_IN_API { typoid, ... }
=>
{ if first ();
else pp.newline();
fi;
pp.cwrap {. pp.rulename "lpplcw1";
pp.lit /*2007-12-08CrT:"my "*/ "";
uj::unparse_symbol pp symbol; pp.txt " : ";
latex_print_some_type symbolmapstack pp typoid;
pp.endlit ";";
# Add an appropriate TeX index entry for the value,
# for our html manual. We break the string up a
# bit to avoid irritating Mythryl or HeVea with
# apparent keywords in their respective syntaxes:
#
index_entries
:=
( (string::cat [ "\\inde", "x[fu", "n]{", (backslash_latex_special_chars (symbol::name symbol)), "}\n" ])
!
(*index_entries)
);
};
};
mld::VALCON_IN_API {
sumtype => valcon as tdt::VALCON {
form => a::EXCEPTION _,
...
},
...
}
=>
{ if (not first)
pp.newline();
fi;
latex_print_con_naming pp (valcon, symbolmapstack);
pp.endlit ";";
};
mld::VALCON_IN_API { sumtype, ... }
=>
if *internals
#
if (not first)
pp.newline();
fi;
latex_print_con_naming pp (sumtype, symbolmapstack);
pp.endlit ";";
fi; # Ordinary data constructor -- don't print.
esac;
pp.box {. pp.rulename "lppl11";
#
case elements
#
NIL => ();
first ! rest => { pr TRUE first;
apply (pr FALSE) rest;
};
esac;
};
}
also
fun latex_print_api0 (pp:Pp) (an_api, symbolmapstack, depth, typechecked_package_env_op, index_entries)
=
{
symbolmapstack = syx::atop (
case typechecked_package_env_op
#
NULL => api_to_symbolmapstack an_api;
#
THE typerstore => str_to_dictionary (an_api, typerstore);
esac,
symbolmapstack
);
fun latex_print_constraints (variety, constraints: List( mld::Share_Spec ))
=
{
pp.box' 0 -1 {. pp.rulename "lppl12";
#
uj::ppvseq pp 0 ""
(\\ pp =
\\ paths =
{ pp.box' 0 2 {. pp.rulename "lppl13";
pp.txt "sharing "; pp.lit variety;
uj::unparse_sequence pp
{ separator => (\\ pp = { pp.txt' 0 -1 " = "; }),
print_one => uj::unparse_symbol_path,
breakstyle => uj::WRAP
}
paths;
};
}
)
constraints;
};
};
some_print = REF FALSE;
if (depth <= 0)
pp.lit "<api>;";
else
case an_api
#
mld::API { stamp, name, api_elements, type_sharing, package_sharing, ... }
=>
if *internals
#
pp.box' 0 -1 {. pp.rulename "lppl14";
pp.lit "BEGIN_API:";
uj::newline_indent pp 2;
pp.box' 0 -1 {. pp.rulename "lppl15";
pp.lit "stamp: "; pp.lit (stamp::to_short_string stamp);
pp.newline();
pp.lit "name: ";
case name
#
NULL => pp.lit "ANONYMOUS";
#
THE p => { pp.lit "NAMED ";
uj::unparse_symbol pp p;
};
esac;
case api_elements
#
NIL => ();
#
_ => { pp.newline();
pp.lit "elements:";
uj::newline_indent pp 2;
latex_print_elements (symbolmapstack, depth, typechecked_package_env_op, index_entries) pp api_elements;
};
esac;
case package_sharing
#
NIL => ();
_ => { pp.newline();
pp.lit "package_sharing:";
uj::newline_indent pp 2;
latex_print_constraints("", package_sharing);
};
esac;
case type_sharing
NIL => ();
_ => { pp.newline();
pp.lit "typesharing:";
uj::newline_indent pp 2;
latex_print_constraints(/*2007-12-07CrT"type "*/"", type_sharing);
};
esac;
pp.endlit ";";
};
};
else # not *internals
pp.box' 0 -1 {. pp.rulename "lppl16";
#
pp.lit "api {";
pp.newline(); # 2008-01-03 CrT: Was: break { blanks=>1, indent_on_wrap=>2 };
pp.box' 0 -1 {. pp.rulename "lppl17";
#
pp.lit " ";
case api_elements
#
NIL => ();
_ => { latex_print_elements (symbolmapstack, depth, typechecked_package_env_op, index_entries) pp api_elements;
some_print := TRUE;
};
esac;
case package_sharing
#
NIL => ();
#
_ => { if *some_print pp.newline(); fi;
latex_print_constraints("", package_sharing);
some_print := TRUE;
};
esac;
case type_sharing
#
NIL => ();
#
_ => { if *some_print pp.newline(); fi;
latex_print_constraints(/*2007-12-07CrT"type "*/"", type_sharing);
some_print := TRUE;
};
esac;
};
if *some_print
#
pp.newline();
# break { blanks => 1, indent_on_wrap => 0 };
fi;
pp.endlit "};";
};
fi;
mld::ERRONEOUS_API
=>
pp.lit "<error api>;";
esac;
fi;
}
also
fun latex_print_generic_api pp (an_api, symbolmapstack, depth, index_entries)
=
{
fun true_body_sig (orig as mld::API { api_elements => [(symbol, mld::PACKAGE_IN_API { an_api, ... } )],
...
}
)
=>
if (symbol::eq (symbol, result_id)) an_api;
else orig;
fi;
true_body_sig orig
=>
orig;
end;
if (depth <= 0)
#
pp.lit "<fctsig>";
else
case an_api
#
mld::GENERIC_API { parameter_api, parameter_variable, parameter_symbol, body_api, ... }
=>
if *internals
#
pp.box' 0 -1 {. pp.rulename "lppl18";
#
pp.lit "GENERIC_API:";
uj::newline_indent pp 2;
pp.box' 0 -1 {. pp.rulename "lppl19";
pp.lit "psig: ";
latex_print_api0 pp (parameter_api, symbolmapstack, depth - 1, NULL, index_entries);
pp.newline();
pp.lit "pvar: ";
pp.lit (stamppath::module_stamp_to_string parameter_variable);
pp.newline();
pp.lit "psym: ";
case parameter_symbol
NULL => pp.lit "<anonymous>";
THE symbol => uj::unparse_symbol pp symbol;
esac;
pp.newline();
pp.lit "bsig: ";
latex_print_api0 pp (body_api, symbolmapstack, depth - 1, NULL, index_entries);
};
};
else
pp.box' 0 -1 {. pp.rulename "lppl20";
#
pp.lit "(";
case parameter_symbol
#
THE x => pp.lit (s::name x);
_ => pp.lit "<parameter>";
esac;
pp.txt ": ";
latex_print_api0 pp (parameter_api, symbolmapstack, depth - 1, NULL, index_entries);
pp.txt ") : ";
latex_print_api0 pp (true_body_sig body_api, symbolmapstack, depth - 1, NULL, index_entries);
};
fi;
mld::ERRONEOUS_GENERIC_API
=>
pp.lit "<error fsig>";
esac;
fi;
}
also
fun latex_print_generics_expansion pp (e, symbolmapstack, depth)
=
{ e -> { stamp, typerstore, property_list, inverse_path, stub };
if (depth <= 1)
pp.lit "<package typechecked_package>";
else
pp.box' 0 -1 {. pp.rulename "lppl21";
pp.lit "Typechecked_Package:";
uj::newline_indent pp 2;
pp.box' 0 -1 {. pp.rulename "lppl22";
pp.lit "inverse_path: ";
pp.lit (ip::to_string inverse_path);
pp.newline();
pp.lit "stamp: ";
pp.lit (stamp::to_short_string stamp);
pp.newline();
pp.lit "typerstore:";
uj::newline_indent pp 2;
latex_print_typerstore pp (typerstore, symbolmapstack, depth - 1);
pp.newline();
pp.lit "lambdaty:";
uj::newline_indent pp 2;
latex_print_lty pp ( /* ModulePropLists::packageMacroExpansionLambdatype e, depth - 1 */);
};
};
fi;
}
also
fun latex_print_typechecked_generic pp (e, symbolmapstack, depth)
=
{ e -> { stamp, generic_closure, property_list, typepath, inverse_path, stub };
#
if (depth <= 1)
pp.lit "<generic typechecked_package>";
else
pp.box' 0 -1 {. pp.rulename "lppl23";
pp.lit "Typechecked_Generic:";
uj::newline_indent pp 2;
pp.box' 0 -1 {. pp.rulename "lppl24";
pp.lit "inverse_path: ";
pp.lit (ip::to_string inverse_path);
pp.newline();
pp.lit "stamp: ";
pp.lit (stamp::to_short_string stamp);
pp.newline();
pp.txt' 0 2 "generic_closure: ";
latex_print_closure pp (generic_closure, depth - 1);
pp.newline();
pp.txt' 0 2 "lambdaty: ";
latex_print_lty pp ( /* ModulePropLists::genericMacroExpansionLty e, depth - 1 */ );
pp.txt' 0 2 "typepath:";
pp.lit "--printing of Typepath not implemented yet--";
};
};
fi;
}
also
fun latex_print_generic pp
=
latex_print_f
where
fun latex_print_f (mld::GENERIC { a_generic_api, typechecked_generic, ... }, symbolmapstack, depth, index_entries)
=>
if (depth <= 1)
#
pp.lit "<generic package>";
else
pp.box' 0 -1 {. pp.rulename "lppl25";
pp.lit "a_generic_api:";
uj::newline_indent pp 2;
latex_print_generic_api pp (a_generic_api, symbolmapstack, depth - 1, index_entries);
pp.newline();
pp.lit "typechecked_generic:";
uj::newline_indent pp 2;
latex_print_typechecked_generic pp (typechecked_generic, symbolmapstack, depth - 1);
};
fi;
latex_print_f (mld::ERRONEOUS_GENERIC, _, _, _)
=>
pp.lit "<error generic package>";
end;
end
also
fun latex_print_type_bind pp (type, symbolmapstack)
=
{
fun visible_dcons (type, dcons)
=
find dcons
where
fun check_con (vac::CONSTRUCTOR c) => c;
check_con _ => raise exception syx::UNBOUND;
end;
fun find ((actual as { name, form, domain } ) ! rest)
=>
{ found
=
check_con (lu::find_value_by_symbol
(symbolmapstack, name,
\\ _ = raise exception syx::UNBOUND));
# Test whether the sumtypes of actual and
# found constructor agree:
case (tu::sumtype_to_type found)
#
type1 as tdt::SUM_TYPE _
=>
# The expected form in packages
if (tu::types_are_equal (type, type1))
found ! find rest;
else find rest;
fi;
tdt::TYPE_BY_STAMPPATH _
=>
/* the expected form in apis;
we won't check visibility [dbm] */
found ! find rest;
d_found
=>
# something's weird
{ old_internals = *internals;
internals := TRUE;
pp.box' 0 -1 {. pp.rulename "lppl26";
#
pp.lit "latex_print_type_bind failure: ";
pp.newline();
latex_print_type symbolmapstack pp type;
pp.newline();
latex_print_type symbolmapstack pp d_found;
pp.newline();
};
internals := old_internals;
find rest;
};
esac;
}
except
syx::UNBOUND = find rest;
find []
=>
[];
end;
end; # fun visible_dcons
fun strip_poly (tdt::TYPESCHEME_TYPOID { typescheme => tdt::TYPESCHEME { body, ... }, ... } )
=>
body;
strip_poly type
=>
type;
end;
fun latex_print_valcon (tdt::VALCON { name, typoid, ... } )
=
{ uj::unparse_symbol pp name;
#
typoid = strip_poly typoid;
if (mtt::is_arrow_type typoid)
#
# pp.txt " of ";
pp.txt " ";
latex_print_some_type symbolmapstack pp (mtt::domain typoid);
fi;
};
if *internals
#
pp.box' 0 -1 {. pp.rulename "lppl27";
pp.lit /*2007-12-07CrT"type "*/"";
latex_print_type symbolmapstack pp type;
};
else
case type
#
tdt::SUM_TYPE { namepath, arity, is_eqtype, kind, ... }
=>
case (*is_eqtype, kind) # Used to have tdt::e::EQ_ABSTRACT case here ("abstype" support).
#
(_, tdt::SUMTYPE { index, family => { members, ... }, ... } )
=>
# Ordinary sumtype:
#
{ (vector::get (members, index))
->
{ valcons, ... };
visdcons = visible_dcons (type, valcons);
incomplete = length visdcons < length valcons;
pp.box' 0 -1 {. pp.rulename "lppl29";
# pp.lit "sumtype";
uj::unparse_symbol pp (ip::last namepath);
pp.txt " ";
latex_print_formals pp arity;
case visdcons
#
NIL => pp.txt " = ...";
first ! rest
=>
{ pp.txt' 0 2 " ";
pp.box' 0 -1 {. pp.rulename "lppl30";
pp.lit "= "; latex_print_valcon first;
apply (\\ d = { pp.txt " | ";
latex_print_valcon d;
}
)
rest;
if incomplete
pp.txt " ... ";
fi;
};
};
esac;
};
};
_ =>
{ pp.box' 0 -1 {. pp.rulename "lppl31";
#
if (eq_types::is_equality_type type) pp.txt "eqtype ";
else pp.lit /*2007-12-07CrT"type "*/"";
fi;
uj::unparse_symbol pp (ip::last namepath);
pp.txt " ";
latex_print_formals pp arity;
};
};
esac;
tdt::NAMED_TYPE { namepath, typescheme => tdt::TYPESCHEME { arity, body }, ... }
=>
{ pp.wrap' 0 2 {. pp.rulename "ppplw1";
pp.lit /*2007-12-07CrT"type "*/"";
uj::unparse_symbol pp (ip::last namepath);
pp.txt " ";
latex_print_formals pp arity;
pp.txt " = ";
latex_print_some_type symbolmapstack pp body;
};
};
type => { pp.txt "strange type: ";
latex_print_type symbolmapstack pp type;
};
esac;
fi;
} # fun latex_print_type_bind pp
also
fun latex_print_replicate_naming
pp
( tdt::NAMED_TYPE {
typescheme => tdt::TYPESCHEME {
body => tdt::TYPCON_TYPOID (right_type, _),
...
},
namepath,
...
},
symbolmapstack
)
=>
{
pp.wrap' 0 2 {. pp.rulename "ppplw2";
# pp.txt "sumtype ";
uj::unparse_symbol pp (ip::last namepath);
pp.txt " = ";
# pp.txt "sumtype ";
latex_print_type symbolmapstack pp right_type;
};
};
latex_print_replicate_naming _ _
=>
error_message::impossible "latex_print_replicate_naming";
end
also
fun latex_print_typechecked_package pp (typechecked_package, symbolmapstack, depth)
=
case typechecked_package
#
mld::TYPE_ENTRY type
=>
latex_print_type symbolmapstack pp type;
mld::PACKAGE_ENTRY typechecked_package
=>
latex_print_generics_expansion pp (typechecked_package, symbolmapstack, depth - 1);
mld::GENERIC_ENTRY typechecked_generic
=>
latex_print_typechecked_generic pp (typechecked_generic, symbolmapstack, depth - 1);
mld::ERRONEOUS_ENTRY
=>
pp.lit "ERRONEOUS_ENTRY";
esac
also
fun latex_print_typerstore pp (typerstore, symbolmapstack, depth)
=
if (depth <= 1)
#
pp.lit "<typerstore>";
else
(uj::ppvseq
pp 2 ""
(\\ pp =
\\ (module_stamp, typechecked_package)
=
{
pp.box' 0 2 {. pp.rulename "lppl32";
pp.lit (stamppath::module_stamp_to_string module_stamp);
pp.lit ":";
uj::newline_indent pp 2;
latex_print_typechecked_package pp (typechecked_package, symbolmapstack, depth - 1);
pp.newline();
};
}
)
(tro::to_list typerstore));
fi
also
fun latex_print_module_declaration pp (module_declaration, depth)
=
if (depth <= 0)
pp.lit "<module_declaration>";
else
case module_declaration
#
mld::TYPE_DECLARATION ( module_stamp, type_expression )
=>
{ pp.lit "ed::T: ";
latex_print_typechecked_package_variable pp module_stamp;
pp.txt' 1 -1 " ";
latex_print_type_expression pp (type_expression, depth - 1);
};
mld::PACKAGE_DECLARATION (module_stamp, package_expression, symbol)
=>
{ pp.lit "ed::S: ";
latex_print_typechecked_package_variable pp module_stamp;
pp.txt' 1 -1 " ";
latex_print_package_expression pp (package_expression, depth - 1);
pp.txt' 1 -1 " ";
uj::unparse_symbol pp symbol;
};
mld::GENERIC_DECLARATION (module_stamp, generic_expression)
=>
{ pp.lit "ed::F: ";
latex_print_typechecked_package_variable pp module_stamp;
pp.txt' 1 -1 " ";
latex_print_generic_expression pp (generic_expression, depth - 1);
};
mld::SEQUENTIAL_DECLARATIONS typechecked_package_decs
=>
uj::ppvseq pp 0 ""
(\\ pp =
\\ module_declaration =
latex_print_module_declaration pp (module_declaration, depth)
)
typechecked_package_decs;
mld::LOCAL_DECLARATION (typechecked_package_dec_l, typechecked_package_dec_b)
=>
pp.lit "ed::L:";
mld::ERRONEOUS_ENTRY_DECLARATION
=>
pp.lit "ed::ER:";
mld::EMPTY_GENERIC_EVALUATION_DECLARATION
=>
pp.lit "ed::EM:";
esac;
fi
also
fun latex_print_package_expression pp (package_expression, depth)
=
if (depth <= 0)
pp.lit "<packageexpression>";
else
case package_expression
#
mld::VARIABLE_PACKAGE ep
=>
{ pp.lit "syx::VARIABLE_PACKAGE:";
pp.txt' 1 -1 " ";
latex_print_stamppath pp ep;
};
mld::CONSTANT_PACKAGE { stamp, inverse_path, ... }
=>
{ pp.lit "syx::CONSTANT_PACKAGE:"; pp.txt' 1 -1 " ";
uj::unparse_inverse_path pp inverse_path;
};
mld::PACKAGE { stamp, module_declaration }
=>
{ pp.lit "syx::PACKAGE:";
pp.txt' 1 -1 " ";
latex_print_module_declaration pp (module_declaration, depth - 1);
};
mld::APPLY (generic_expression, package_expression)
=>
{ pp.box {. pp.rulename "lppl33";
pp.lit "syx::APPLY:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl34";
pp.lit "fct:"; latex_print_generic_expression pp (generic_expression, depth - 1);
pp.txt " ";
pp.lit "arg:"; latex_print_package_expression pp (package_expression, depth - 1);
};
};
};
mld::PACKAGE_LET { declaration => module_declaration, expression => package_expression }
=>
{ pp.box {. pp.rulename "lppl35";
pp.lit "syx::PACKAGE_LET:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl36";
pp.lit "stipulate:"; latex_print_module_declaration pp (module_declaration, depth - 1);
pp.txt " ";
pp.lit "herein:"; latex_print_package_expression pp (package_expression, depth - 1);
};
};
};
mld::ABSTRACT_PACKAGE (an_api, package_expression)
=>
{ pp.box {. pp.rulename "lppl37";
pp.lit "syx::ABSTRACT_PACKAGE:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl38";
pp.lit "an_api: <omitted>";
pp.txt " ";
pp.lit "sexp:"; latex_print_package_expression pp (package_expression, depth - 1);
};
};
};
mld::COERCED_PACKAGE { boundvar, raw, coercion }
=>
{ pp.box {. pp.rulename "lppl39";
pp.lit "syx::COERCED_PACKAGE:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl40";
latex_print_typechecked_package_variable pp boundvar;
pp.txt' 1 -1 " ";
pp.lit "src:"; latex_print_package_expression pp (raw, depth - 1);
pp.txt " ";
pp.lit "tgt:"; latex_print_package_expression pp (coercion, depth - 1);
};
};
};
mld::FORMAL_PACKAGE (an_api)
=>
pp.lit "syx::FORMAL_PACKAGE:";
esac;
fi
also
fun latex_print_generic_expression pp (generic_expression, depth)
=
if (depth <= 0)
pp.lit "<genericexpression>";
else
case generic_expression
#
mld::VARIABLE_GENERIC ep
=>
{ pp.lit "fe::VARIABLE_GENERIC:";
latex_print_stamppath pp ep;
};
mld::CONSTANT_GENERIC { inverse_path, ... }
=>
{ pp.lit "fe::CONSTANT_GENERIC:";
uj::unparse_inverse_path pp inverse_path;
};
mld::LAMBDA_TP { parameter, body, ... }
=>
{ pp.box {. pp.rulename "lppl41";
pp.lit "fe::LAMBDA_TP:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl42";
pp.lit "par:"; latex_print_typechecked_package_variable pp parameter;
pp.txt " ";
pp.lit "bod:"; latex_print_package_expression pp (body, depth - 1);
};
};
};
mld::LAMBDA { parameter, body }
=>
{ pp.box {. pp.rulename "lppl43";
pp.lit "fe::LAMBDA:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl44";
pp.lit "par:"; latex_print_typechecked_package_variable pp parameter;
pp.txt " ";
pp.lit "bod:"; latex_print_package_expression pp (body, depth - 1);
};
};
};
mld::LET_GENERIC (module_declaration, generic_expression)
=>
{ pp.box {. pp.rulename "lppl45";
pp.lit "fe::LET_GENERIC:"; pp.txt' 1 -1 " ";
pp.box {. pp.rulename "lppl46";
pp.lit "stipulate:"; latex_print_module_declaration pp (module_declaration, depth - 1);
pp.txt " ";
pp.lit "herein:"; latex_print_generic_expression pp (generic_expression, depth - 1);
};
};
};
esac;
fi
/*
also prettyprintBodyExpression pp (bodyExpression, depth) =
if depth <= 0 then pp.lit "<bodyExpression>" else
case bodyExpression
of mld::FLEX an_api => pp.lit "be::F:"
| mld::OPAQ (an_api, packageexpression) =>
(begin_align_box pp;
pp.lit "be::O:"; break pp { blanks=1, indent_on_wrap=1 };
prettyprintPackageexpression pp (packageexpression, depth - 1);
end_box pp)
| mld::TNSP (an_api, packageexpression) =>
(begin_align_box pp;
pp.lit "be::T:"; break pp { blanks=1, indent_on_wrap=1 };
prettyprintPackageexpression pp (packageexpression, depth - 1);
end_box pp)
*/
also
fun latex_print_closure pp (mld::GENERIC_CLOSURE { parameter_module_stamp => parameter,
body_package_expression => body,
typerstore => symbolmapstack
},
depth
)
=
{
pp.box' 0 -1 {. pp.rulename "lppl47";
pp.lit "CL:"; pp.txt' 1 -1 " ";
pp.box' 0 -1 {. pp.rulename "lppl48";
pp.lit "parameter: ";
latex_print_typechecked_package_variable pp parameter;
pp.newline();
pp.lit "body: ";
latex_print_package_expression pp (body, depth - 1);
pp.newline();
pp.lit "dictionary: ";
latex_print_typerstore pp (symbolmapstack, syx::empty, depth - 1);
};
};
}
# Assumes no newline is needed before latex-printing:
also
fun latex_print_naming pp (name, naming: b::Symbolmapstack_Entry, symbolmapstack: syx::Symbolmapstack, depth: Int, index_entries)
=
case naming
#
b::NAMED_VARIABLE var
=>
{ pp.lit /*2007-12-08CrT:"my "*/"";
latex_print_variable pp (var, symbolmapstack);
};
b::NAMED_CONSTRUCTOR con
=>
latex_print_con_naming pp (con, symbolmapstack);
b::NAMED_TYPE type
=>
latex_print_type_bind pp (type, symbolmapstack);
b::NAMED_API an_api
=>
{
pp.box' 0 -1 {. pp.rulename "lppl49";
pp.lit "api ";
uj::unparse_symbol pp name;
pp.txt " =";
pp.txt' 0 2 " ";
latex_print_api0 pp (an_api, symbolmapstack, depth, NULL, index_entries);
};
};
b::NAMED_GENERIC_API fs
=>
pp.box' 0 2 {. pp.rulename "lppl50";
pp.lit "funsig ";
uj::unparse_symbol pp name;
latex_print_generic_api pp (fs, symbolmapstack, depth, index_entries);
};
b::NAMED_PACKAGE str
=>
pp.box' 0 -1 {. pp.rulename "lppl51";
pp.lit "packageX ";
uj::unparse_symbol pp name;
pp.txt " :";
pp.txt' 0 2 " ";
latex_print_package pp (str, symbolmapstack, depth, index_entries);
};
b::NAMED_GENERIC fct
=>
pp.box' 0 -1 {. pp.rulename "lppl52";
pp.lit "generic package ";
uj::unparse_symbol pp name;
pp.lit " : <sig>"; # David B MacQueen -- should print the api XXX SUCKO FIXME
};
b::NAMED_FIXITY fixity
=>
{ pp.lit (fixity::fixity_to_string fixity);
uj::unparse_symbol pp name;
};
esac
# latex_print_dictionary: latex-print a symbol table
# in the context of the top-level symbol table.
# The symbol table must either be for a api or be absolute (i.e.
# all types and packages have been interpreted)
# Note: I made a preliminary pass over namings to remove
# invisible con_namings -- Konrad.
# and invisible packages too -- PC
also
fun latex_print_dictionary pp (symbolmapstack, topenv, depth, boundsyms, index_entries)
=
{ namings
=
case boundsyms
#
NULL => syx::to_sorted_list symbolmapstack;
THE l => fold_backward
(\\ (x, bs)
=
(x, syx::get (symbolmapstack, x)) ! bs
except
syx::UNBOUND = bs
)
[]
l;
esac;
pp_env = syx::atop (symbolmapstack, topenv);
uj::unparse_sequence pp
{ separator => pp::newline,
breakstyle => uj::ALIGN,
print_one => (\\ pp =
\\ (name, naming)
=
latex_print_naming pp (name, naming, pp_env, depth, index_entries)
)
}
(all_latex_printable_namings namings pp_env);
};
fun latex_print_open pp (path, pkg, symbolmapstack, depth, index_entries)
=
pp.box' 0 -1 {. pp.rulename "lppl53";
#
pp.box' 0 2 {. pp.rulename "lppl54";
#
pp.lit "inCluding ";
uj::unparse_symbol_path pp path;
if (depth >= 1)
#
case pkg
#
mld::A_PACKAGE { an_api, typechecked_package as { typerstore, ... }, ... }
=>
case an_api
#
mld::API { api_elements => [], ... }
=>
();
mld::API { api_elements, ... }
=>
{ pp.newline();
pp.box' 0 -1 {. pp.rulename "lppl55";
#
latex_print_elements
( syx::atop (api_to_symbolmapstack an_api, symbolmapstack),
depth,
THE typerstore,
index_entries
)
pp
api_elements;
};
};
mld::ERRONEOUS_API
=>
();
esac;
mld::ERRONEOUS_PACKAGE => ();
mld::PACKAGE_API _ => bug "latex_print_open";
esac;
fi;
};
pp.newline();
};
fun latex_print_api pp (an_api, symbolmapstack, depth, index_entries)
=
latex_print_api0 pp (an_api, symbolmapstack, depth, NULL, index_entries);
}; # package latex_print_package_language
end; # stipulate