% \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>
\def\libfolder#1{../../lib/#1}
\input{../../doc/stex-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/stex-metatheory}
% \fi
%
% \begin{documentation}\label{pkg:metatheory:doc}
%
% \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/meta}
\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,op=:]{#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,assoc=pre]
  \notation{bind}[depfun,prec=nobrackets,op={(\cdot)\;\to\;\cdot}]{\comp( #1 \comp{)\;\to\;} #2}{##1 \comp, ##2}
  \notation{bind}[forall]{\comp\forall #1.\;#2}{##1 \comp, ##2}
  \notation{bind}[Pi]{\comp\prod_{#1}#2}{##1 \comp, ##2}

  % implicit bind
  \symdecl{implicitbind}[args=Bi,assoc=pre]
  \notation{implicitbind}[braces,prec=nobrackets,op={\{\cdot\}_I\;\cdot}]{\comp\{ #1 \comp{\}_I\;} #2}{##1 \comp, ##2}
  \notation{implicitbind}[depfun,prec=nobrackets]{\comp( #1 \comp{)\;\to_I\;} #2}{##1 \comp, ##2}
  \notation{implicitbind}[Pi]{\comp\prod^I_{#1}#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,op=\cdot(\cdot)]{#1 \comp( #2 \comp)}{##1 \comp, ##2}
  \notation{apply}[prec=0;0x\infprec,lambda]{#1 \; #2 }{##1 \; ##2}

  % collection of propositions/booleans/truth values
  \symdecl{prop}[name=proposition]
  \notation{prop}[prop]{\comp{{\rm prop}}}
  \notation{prop}[BOOL]{\comp{{\rm BOOL}}}

  \symdecl{judgmentholds}[args=1]
  \notation{judgmentholds}[vdash,op=\vdash]{\comp\vdash\; #1}

  % sequences
  \symdecl{seqtype}[args=1]
  \notation{seqtype}[kleene]{#1^{\comp\ast}}

  \symdecl{seqexpr}[args=a]
  \notation{seqexpr}[angle,prec=nobrackets]{\comp\langle #1\comp\rangle}{##1\comp,##2}

  \symdef{seqmap}[args=abi,setlike]{\comp\{#3 \comp| #2\comp\in \dobrackets{#1} \comp\}}{##1 \comp, ##2}
  \symdef{seqprepend}[args=ia]{#1 \comp{::} #2}{##1 \comp, ##2}
  \symdef{seqappend}[args=ai]{#1 \comp{::} #2}{##1 \comp, ##2}
  \symdef{seqfoldleft}[args=iabbi]{ \comp{foldl}\dobrackets{#1,#2}\dobrackets{#3\comp,#4\comp\mapsto#5}}{##1 \comp, ##2}
  \symdef{seqfoldright}[args=iabbi,op=foldr]{ \comp{foldr}\dobrackets{#1,#2}\dobrackets{#3\comp,#4\comp\mapsto#5}}{##1 \comp, ##2}
  \symdef{seqhead}[args=a]{\comp{head}\dobrackets{#1}}{##1 \comp, ##2}
  \symdef{seqtail}[args=a]{\comp{tail}\dobrackets{#1}}{##1 \comp, ##2}
  \symdef{seqlast}[args=a]{\comp{last}\dobrackets{#1}}{##1 \comp, ##2}
  \symdef{seqinit}[args=a]{\comp{tail}\dobrackets{#1}}{##1 \comp, ##2}

  \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}

  % nat literals
  \symdef{natliteral}{\comp{\mathtt{Ord}}}

  % 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}{\comp{\mathtt{MOD}} #1}
  \symdecl{mathstruct}[name=mathematical-structure,args=a] % TODO
  \notation{mathstruct}[angle,prec=nobrackets]{\comp\langle #1 \comp\rangle}{##1 \comp, ##2}

  % objects
  \symdecl{object}
  \notation{object}{\comp{\mathtt{OBJECT}}}

}

% The following are abbreviations in the sTeX corpus that are left over from earlier
% developments. They will eventually be phased out. 

  \ExplSyntaxOn
  \stex_add_to_current_module:n{
    \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}}}
  }
\_@@_end_module:
\endgroup
%    \end{macrocode}
%
%
%    \begin{macrocode}
%</package>
%    \end{macrocode}
%
% \end{implementation}
%
% \PrintIndex
% \ifinfulldoc\else\printbibliography\fi
% \endinput
% Local Variables:
% mode: doctex
% TeX-master: t
% End:
