summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/source/stex/metatheory.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/source/stex/metatheory.dtx')
-rw-r--r--macros/latex/contrib/stex/source/stex/metatheory.dtx179
1 files changed, 179 insertions, 0 deletions
diff --git a/macros/latex/contrib/stex/source/stex/metatheory.dtx b/macros/latex/contrib/stex/source/stex/metatheory.dtx
new file mode 100644
index 0000000000..a477e67f63
--- /dev/null
+++ b/macros/latex/contrib/stex/source/stex/metatheory.dtx
@@ -0,0 +1,179 @@
+% \iffalse meta-comment
+% An Infrastructure for Semantic Macros and Module Scoping
+% Copyright (c) 2019 Michael Kohlhase, all rights reserved
+% this file is released under the
+% LaTeX Project Public License (LPPL)
+%
+% The original of this file is in the public repository at
+% http://github.com/sLaTeX/sTeX/
+%
+% TODO update copyright
+%
+%<*driver>
+\providecommand\bibfolder{../../lib/bib}
+\input{../../doc/docheader}
+
+\begin{document}
+ \DocInput{\jobname.dtx}
+\end{document}
+%</driver>
+% \fi
+%
+% \title{ \sTeX-Metatheory
+% \thanks{Version {\fileversion} (last revised {\filedate})}
+% }
+%
+% \author{Michael Kohlhase, Dennis Müller\\
+% FAU Erlangen-Nürnberg\\
+% \url{http://kwarc.info/}
+% }
+%
+% \maketitle
+%
+%\ifinfulldoc\else
+% This is the documentation for the \pkg{stex-metatheory} package.
+% For a more high-level introduction,
+% see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the
+% \href{\basedocurl/stex.pdf}{full \sTeX documentation}.
+%
+% \input{../../doc/packages/metatheory}
+% \fi
+%
+% \begin{documentation}\label{pkg:metatheory:doc}
+%
+% The default meta theory for an \sTeX module. Contains
+% symbols so ubiquitous, that it is virtually impossible
+% to describe any flexiformal content without them, or
+% that are required to annotate even the most primitive symbols
+% with meaningful (foundation-independent) ``type''-annotations,
+% or required for basic structuring principles (theorems, definitions).
+%
+% Foundations should ideally instantiate these symbols
+% with their formal counterparts, e.g. |isa| corresponds
+% to a typing operation in typed setting, or the $\in$-operator
+% in set-theoretic contexts; |bind| corresponds to a universal
+% quantifier in ($n$th-order) logic, or a $\Pi$ in dependent type
+% theories.
+%
+% \section{Symbols}\label{pkg:metatheory:symbols}
+%
+% \end{documentation}
+%
+% \begin{implementation}\label{pkg:metatheory:impl}
+%
+% \section{\sTeX-Metatheory Implementation}
+%
+% \begin{macrocode}
+%<*package>
+%<@@=stex_modules>
+
+%%%%%%%%%%%%% metatheory.dtx %%%%%%%%%%%%%
+
+\str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX}
+\begingroup
+\stex_module_setup:nn{
+ ns=\c_stex_metatheory_ns_str,
+ meta=NONE
+}{Metatheory}
+\stex_reactivate_macro:N \symdecl
+\stex_reactivate_macro:N \notation
+\stex_reactivate_macro:N \symdef
+\ExplSyntaxOff
+\csname stex_suppress_html:n\endcsname{
+ % is-a (a:A, a \in A, a is an A, etc.)
+ \symdecl{isa}[args=ai]
+ \notation{isa}[typed]{#1 \comp{:} #2}{##1 \comp, ##2}
+ \notation{isa}[in]{#1 \comp\in #2}{##1 \comp, ##2}
+ \notation{isa}[pred]{#2\comp(#1 \comp)}{##1 \comp, ##2}
+
+ % bind (\forall, \Pi, \lambda etc.)
+ \symdecl{bind}[args=Bi]
+ \notation{bind}[forall]{\comp\forall #1.\;#2}{##1 \comp, ##2}
+ \notation{bind}[Pi]{\comp\prod_{#1}#2}{##1 \comp, ##2}
+ \notation{bind}[depfun]{\comp( #1 \comp{)\;\to\;} #2}{##1 \comp, ##2}
+
+ % dummy variable
+ \symdecl{dummyvar}
+ \notation{dummyvar}[underscore]{\comp\_}
+ \notation{dummyvar}[dot]{\comp\cdot}
+ \notation{dummyvar}[dash]{\comp{{\rm --}}}
+
+ %fromto (function space, Hom-set, implication etc.)
+ \symdecl{fromto}[args=ai]
+ \notation{fromto}[xarrow]{#1 \comp\to #2}{##1 \comp\times ##2}
+ \notation{fromto}[arrow]{#1 \comp\to #2}{##1 \comp\to ##2}
+
+ % mapto (lambda etc.)
+ %\symdecl{mapto}[args=Bi]
+ %\notation{mapto}[mapsto]{#1 \comp\mapsto #2}{#1 \comp, #2}
+ %\notation{mapto}[lambda]{\comp\lambda #1 \comp.\; #2}{#1 \comp, #2}
+ %\notation{mapto}[lambdau]{\comp\lambda_{#1} \comp.\; #2}{#1 \comp, #2}
+
+ % function/operator application
+ \symdecl{apply}[args=ia]
+ \notation{apply}[prec=0;0x\infprec,parens]{#1 \comp( #2 \comp)}{##1 \comp, ##2}
+ \notation{apply}[prec=0;0x\infprec,lambda]{#1 \; #2 }{##1 \; ##2}
+
+ % ``type'' of all collections (sets,classes,types,kinds)
+ \symdecl{collection}
+ \notation{collection}[U]{\comp{\mathcal{U}}}
+ \notation{collection}[set]{\comp{\textsf{Set}}}
+
+ % collection of propositions/booleans/truth values
+ \symdecl{prop}[name=proposition]
+ \notation{prop}[prop]{\comp{{\rm prop}}}
+ \notation{prop}[BOOL]{\comp{{\rm BOOL}}}
+
+ % sequences
+ \symdecl{seqtype}[args=1]
+ \notation{seqtype}[kleene]{#1^{\comp\ast}}
+
+ \symdef{sequence-index}[args=2,li,prec=nobrackets]{{#1}_{#2}}
+ \notation{sequence-index}[ui,prec=nobrackets]{{#1}^{#2}}
+
+ \symdef{aseqdots}[args=a,prec=nobrackets]{#1\comp{,\ellipses}}{##1\comp,##2}
+ \symdef{aseqfromto}[args=ai,prec=nobrackets]{#1\comp{,\ellipses,}#2}{##1\comp,##2}
+ \symdef{aseqfromtovia}[args=aii,prec=nobrackets]{#1\comp{,\ellipses,}#2\comp{,\ellipses,}#3}{##1\comp,##2}
+
+ % letin (``let'', local definitions, variable substitution)
+ \symdecl{letin}[args=bii]
+ \notation{letin}[let]{\comp{{\rm let}}\;#1\comp{=}#2\;\comp{{\rm in}}\;#3}
+ \notation{letin}[subst]{#3 \comp[ #1 \comp/ #2 \comp]}
+ \notation{letin}[frac]{#3 \comp[ \frac{#2}{#1} \comp]}
+
+ % structures
+ \symdecl*{module-type}[args=1]
+ \notation{module-type}{\mathtt{MOD} #1}
+ \symdecl{mathstruct}[name=mathematical-structure,args=a] % TODO
+ \notation{mathstruct}[angle,prec=nobrackets]{\comp\langle #1 \comp\rangle}{##1 \comp, ##2}
+
+}
+ \ExplSyntaxOn
+ \stex_add_to_current_module:n{
+ \let\nappa\apply
+ \def\nappli#1#2#3#4{\apply{#1}{\naseqli{#2}{#3}{#4}}}
+ \def\nappui#1#2#3#4{\apply{#1}{\nasequi{#2}{#3}{#4}}}
+ \def\livar{\csname sequence-index\endcsname[li]}
+ \def\uivar{\csname sequence-index\endcsname[ui]}
+ \def\naseqli#1#2#3{\aseqfromto{\livar{#1}{#2}}{\livar{#1}{#3}}}
+ \def\nasequi#1#2#3{\aseqfromto{\uivar{#1}{#2}}{\uivar{#1}{#3}}}
+ \def\nappe#1#2#3{\apply{#1}{\aseqfromto{#2}{#3}}}
+ }
+\_@@_end_module:
+\endgroup
+% \end{macrocode}
+%
+%
+% \begin{macrocode}
+%</package>
+% \end{macrocode}
+%
+% \end{implementation}
+%
+% \PrintIndex
+
+% \endinput
+% Local Variables:
+% mode: doctex
+% TeX-master: t
+% End: