\documentclass[a4paper]{article}

\usepackage{manfnt}
\usepackage{a4wide}
\usepackage{pifont}
\usepackage{semantic}
\usepackage{stmaryrd,latexsym}

\newcommand{\BLOB}{\raisebox{0ex}{\small\manstar}}

\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}

\title{Extensible notation for \MATITA}
\author{Luca Padovani \qquad Stefano Zacchiroli \\
\small Department of Computer Science, University of Bologna \\
\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
\small \{\texttt{lpadovan}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}

\newcommand{\BREAK}{\mathtt{break}}
\newcommand{\TVAR}[1]{#1:\mathtt{term}}
\newcommand{\NVAR}[1]{#1:\mathtt{number}}
\newcommand{\IVAR}[1]{#1:\mathtt{name}}
\newcommand{\FENCED}[1]{\texttt{\char'050}#1\texttt{\char'051}}
\newcommand{\IOT}[2]{|[#1|]_{\mathcal#2}^1}
\newcommand{\ADDPARENS}[2]{\llparenthesis#1\rrparenthesis^{#2}}
\newcommand{\NAMES}{\mathit{names}}
\newcommand{\DOMAIN}{\mathit{domain}}

\mathlig{~>}{\leadsto}
\mathlig{|->}{\mapsto}

\begin{document}
  \maketitle

\section{Environment}

\[
\begin{array}{rcll}
  V & ::= & & \mbox{(\bf values)} \\
    &     & \verb+Term+~T & \mbox{(term)} \\
    &  |  & \verb+String+~s & \mbox{(string)} \\
    &  |  & \verb+Number+~n & \mbox{(number)} \\
    &  |  & \verb+None+ & \mbox{(optional value)} \\
    &  |  & \verb+Some+~V & \mbox{(optional value)} \\
    &  |  & [V_1,\dots,V_n] & \mbox{(list value)} \\[2ex]
\end{array}
\]

An environment is a map $\mathcal E : \mathit{Name} -> V$.

\section{Level 1: concrete syntax}

\begin{table}
\caption{\label{tab:l1c} Concrete syntax of level 1 patterns.\strut}
\hrule
\[
\begin{array}{rcll}
  P & ::= & & \mbox{(\bf patterns)} \\
    &     & S^{+} \\[2ex]
  S & ::= & & \mbox{(\bf simple patterns)} \\
    &     & l \\
    &  |  & S~\verb+\sub+~S\\
    &  |  & S~\verb+\sup+~S\\
    &  |  & S~\verb+\below+~S\\
    &  |  & S~\verb+\atop+~S\\
    &  |  & S~\verb+\over+~S\\
    &  |  & S~\verb+\atop+~S\\
    &  |  & \verb+\frac+~S~S \\
    &  |  & \verb+\sqrt+~S \\
    &  |  & \verb+\root+~S~\verb+\of+~S \\
    &  |  & \verb+(+~P~\verb+)+ \\
    &  |  & \verb+hbox (+~P~\verb+)+ \\
    &  |  & \verb+vbox (+~P~\verb+)+ \\
    &  |  & \verb+hvbox (+~P~\verb+)+ \\
    &  |  & \verb+hovbox (+~P~\verb+)+ \\
    &  |  & \verb+break+ \\
    &  |  & \verb+list0+~S~[\verb+sep+~l] \\
    &  |  & \verb+list1+~S~[\verb+sep+~l] \\
    &  |  & \verb+opt+~S \\
    &  |  & [\verb+term+]~x \\
    &  |  & \verb+number+~x \\
    &  |  & \verb+ident+~x \\
\end{array}
\]
\hrule
\end{table}

Rationale: while the layout schemata can occur in the concrete syntax
used by user, the box schemata and the magic patterns can only occur
when defining the notation. This is why the layout schemata are
``escaped'' with a backslash, so that they cannot be confused with
plain identifiers, wherease the others are not. Alternatively, they
could be defined as keywords, but this would prevent their names to be
used in different contexts.

\begin{table}
\caption{\label{tab:l1a} Abstract syntax of level 1 terms and patterns.\strut}
\hrule
\[
\begin{array}{@{}ll@{}}
\begin{array}[t]{rcll}
  T & ::= & & \mbox{(\bf terms)} \\
    &     & L_\kappa[T_1,\dots,T_n] & \mbox{(layout)} \\
    &  |  & B_\kappa^{ab}[T_1\cdots T_n] & \mbox{(box)} \\
    &  |  & \BREAK & \mbox{(breakpoint)} \\
    &  |  & \FENCED{T_1\cdots T_n} & \mbox{(fenced)} \\
    &  |  & l & \mbox{(literal)} \\[2ex]
  P & ::= & & \mbox{(\bf patterns)} \\
    &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
    &  |  & B_\kappa^{ab}[P_1\cdots P_n] & \mbox{(box)} \\
    &  |  & \BREAK & \mbox{(breakpoint)} \\
    &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
    &  |  & M & \mbox{(magic)} \\
    &  |  & V & \mbox{(variable)} \\
    &  |  & l & \mbox{(literal)} \\
\end{array} &
\begin{array}[t]{rcll}
  V & ::= & & \mbox{(\bf variables)} \\
    &     & \TVAR{x} & \mbox{(term variable)} \\
    &  |  & \NVAR{x} & \mbox{(number variable)} \\
    &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
  M & ::= & & \mbox{(\bf magic patterns)} \\
    &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
    &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
    &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
\end{array}
\end{array}
\]
\hrule
\end{table}

\[
\IOT{\cdot}{{}} : P -> \mathit{Env} -> T
\]

\begin{table}
\caption{\label{tab:il1} Instantiation of level 1 patterns.\strut}
\hrule
\[
\begin{array}{rcll}
  \IOT{L_\kappa[P_1,\dots,P_n]}{E} & = & L_\kappa[\IOT{(P_1)}{E},\dots,\IOT{(P_n)}{E} ] \\
  \IOT{B_\kappa^{ab}[P_1\cdots P_n]}{E} & = & B_\kappa^{ab}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
  \IOT{\BREAK}{E} & = & \BREAK \\
  \IOT{(P)}{E} & = & \IOT{P}{E} \\
  \IOT{(P_1\cdots P_n)}{E} & = & B_H^{00}[\IOT{P_1}{E}\cdots\IOT{P_n}{E}] \\
  \IOT{\TVAR{x}}{E} & = & t & \mathcal{E}(x) = \verb+Term+~t \\
  \IOT{\NVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+Number+~l \\
  \IOT{\IVAR{x}}{E} & = & l & \mathcal{E}(x) = \verb+String+~l \\
  \IOT{\mathtt{opt}~P}{E} & = & \varepsilon & \mathcal{E}(\NAMES(P)) = \{\mathtt{None}\} \\
  \IOT{\mathtt{opt}~P}{E} & = & \IOT{P}{E'} & \mathcal{E}(\NAMES(P)) = \{\mathtt{Some}~v_1,\dots,\mathtt{Some}~v_n\} \\
  & & & \mathcal{E}'(x)=\left\{
  \begin{array}{@{}ll}
    v, & \mathcal{E}(x) = \mathtt{Some}~v \\
    \mathcal{E}(x), & \mbox{otherwise}
  \end{array}
  \right. \\
  \IOT{\mathtt{list}k~P~l?}{E} & = & \IOT{P}{{E}_1}~{l?}\cdots {l?}~\IOT{P}{{E}_n} &
    \mathcal{E}(\NAMES(P)) = \{[v_{11},\dots,v_{1n}],\dots,[v_{m1},\dots,v_{mn}]\} \\
    & & & n\ge k \\
  & & & \mathcal{E}_i(x) = \left\{
  \begin{array}{@{}ll}
    v_i, & \mathcal{E}(x) = [v_1,\dots,v_n] \\
    \mathcal{E}(x), & \mbox{otherwise}
  \end{array}
  \right. \\
  \IOT{l}{E} & = & l \\

%%     &  |  & (P) & \mbox{(fenced)} \\
%%     &  |  & M & \mbox{(magic)} \\
%%     &  |  & V & \mbox{(variable)} \\
%%     &  |  & l & \mbox{(literal)} \\[2ex]
%%   V & ::= & & \mbox{(\bf variables)} \\
%%     &     & \TVAR{x} & \mbox{(term variable)} \\
%%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
%%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
%%   M & ::= & & \mbox{(\bf magic patterns)} \\
%%     &     & \verb+list0+~S~l? & \mbox{(possibly empty list)} \\
%%     &  |  & \verb+list1+~S~l? & \mbox{(non-empty list)} \\
%%     &  |  & \verb+opt+~S & \mbox{(option)} \\[2ex]  
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:wfl0} Well-formedness rules for level 1 patterns.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}[t]{@{}c@{}}
  \inference[\sc layout]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {L_\kappa[P_1,\dots,P_n] :: D_1\oplus\cdots\oplus D_n}
  \\
  \inference[\sc box]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {B_\kappa^{ab}[P_1\cdots P_n] :: D_1\oplus\cdots\oplus D_n}
  \\
  \inference[\sc fenced]
    {P_i :: D_i & \forall i,j, i\ne j => \DOMAIN(D_i) \cap \DOMAIN(D_j) = \emptyset}
    {\FENCED{P_1\cdots P_n} :: D_1\oplus\cdots\oplus D_n}
  \\
  \inference[\sc breakpoint]
    {}
    {\BREAK :: \emptyset}
  \qquad
  \inference[\sc literal]
    {}
    {l :: \emptyset}
  \qquad
  \inference[\sc tvar]
    {}
    {\TVAR{x} :: \TVAR{x}}
  \\
  \inference[\sc nvar]
    {}
    {\NVAR{x} :: \NVAR{x}}
  \qquad
  \inference[\sc ivar]
    {}
    {\IVAR{x} :: \IVAR{x}}
  \\
  \inference[\sc list0]
    {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
    {\mathtt{list0}~P~l? :: D'}
  \\
  \inference[\sc list1]
    {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{List}}
    {\mathtt{list1}~P~l? :: D'}
  \\
  \inference[\sc opt]
    {P :: D & \forall x\in\DOMAIN(D), D'(x) = D(x)~\mathtt{Option}}
    {\mathtt{opt}~P :: D'}
\end{array}
\]
\hrule
\end{table}

\newcommand{\ATTRS}[1]{\langle#1\rangle}
\newcommand{\ANNPOS}[2]{\mathit{pos}(#1)_{#2}}

\begin{table}
\caption{\label{tab:addparens} Where are parentheses added? Look here.\strut}
\hrule
\[
\begin{array}{rcll}
  \ADDPARENS{l}{n} & = & l \\
  \ADDPARENS{\BREAK}{n} & = & \BREAK \\
  \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \ADDPARENS{T}{m} & n < m \\
  \ADDPARENS{\ATTRS{\mathit{prec}=m}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} & n > m \\
  \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=L,\mathit{pos}=R}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
  \ADDPARENS{\ATTRS{\mathit{prec}=n,\mathit{assoc}=R,\mathit{pos}=L}T}{n} & = & \FENCED{\ADDPARENS{T}{\bot}} \\
  \ADDPARENS{\ATTRS{\cdots}T}{n} & = & \ADDPARENS{T}{n} \\
  \ADDPARENS{L_\kappa[T_1,\dots,\underline{T_k},\dots,T_m]}{n} & = & L_\kappa[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_k}{\bot},\dots,\ADDPARENS{T_m}{n}] \\
  \ADDPARENS{B_\kappa^{ab}[T_1,\dots,T_m]}{n} & = & B_\kappa^{ab}[\ADDPARENS{T_1}{n},\dots,\ADDPARENS{T_m}{n}]
\end{array}
\]
\hrule
\end{table}

\begin{table}
\caption{\label{tab:annpos} Annotation of level 1 meta variable with position information.\strut}
\hrule
\[
\begin{array}{rcll}
  \ANNPOS{l}{p,q} & = & l \\
  \ANNPOS{\BREAK}{p,q} & = & \BREAK \\
  \ANNPOS{x}{1,0} & = & \ATTRS{\mathit{pos}=L}{x} \\
  \ANNPOS{x}{0,1} & = & \ATTRS{\mathit{pos}=R}{x} \\
  \ANNPOS{x}{p,q} & = & \ATTRS{\mathit{pos}=I}{x} \\
  \ANNPOS{B_\kappa^{ab}[P]}{p,q} & = & B_\kappa^{ab}[\ANNPOS{P}{p,q}] \\
  \ANNPOS{B_\kappa^{ab}[\{\BREAK\} P_1\cdots P_n\{\BREAK\}]}{p,q} & = & B_\kappa^{ab}[\begin{array}[t]{@{}l}
      \{\BREAK\} \ANNPOS{P_1}{p,0} \\
      \ANNPOS{P_2}{0,0}\cdots\ANNPOS{P_{n-1}}{0,0} \\
      \ANNPOS{P_n}{0,q}\{\BREAK\}]
  \end{array}

%%     &     & L_\kappa[P_1,\dots,P_n] & \mbox{(layout)} \\
%%     &  |  & \BREAK & \mbox{(breakpoint)} \\
%%     &  |  & \FENCED{P_1\cdots P_n} & \mbox{(fenced)} \\
%%   V & ::= & & \mbox{(\bf variables)} \\
%%     &     & \TVAR{x} & \mbox{(term variable)} \\
%%     &  |  & \NVAR{x} & \mbox{(number variable)} \\
%%     &  |  & \IVAR{x} & \mbox{(name variable)} \\[2ex]
%%   M & ::= & & \mbox{(\bf magic patterns)} \\
%%     &     & \verb+list0+~P~l? & \mbox{(possibly empty list)} \\
%%     &  |  & \verb+list1+~P~l? & \mbox{(non-empty list)} \\
%%     &  |  & \verb+opt+~P & \mbox{(option)} \\[2ex]
\end{array}
\]
\hrule
\end{table}

\section{Level 2: abstract syntax}

\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}

\begin{table}
\[
\begin{array}{@{}rcll@{}}
  \NT{term} & ::= & & \mbox{(\bf terms)} \\
    &     & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
    &  |  & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
    &  |  & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
    &  |  & \NT{term}~\NT{term} & \mbox{(application)} \\
    &  |  & x & \mbox{(identifier)} \\
    &  |  & \mathrm{URI} & \mbox{(URI)} \\
    &  |  & n & \mbox{(number)} \\
    &  |  & \verb+?+ & \mbox{(implicit)} \\
    &  |  & \verb+%+ & \mbox{(placeholder)} \\
    &  |  & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
    &  |  & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
    &  |  & [\verb+[+~\NT{term}~\verb+]+]~\verb+match+~\NT{term}~\verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \mbox{(pattern match)} \\
    &  |  & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
    &  |  & \verb+(+~\NT{term}~\verb+)+ \\
    &  |  & \BLOB & \mbox{(blob)} \\
  \NT{defs}  & ::= & & \mbox{(\bf mutual definitions)} \\
    &     & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
  \NT{fun} & ::= & & \mbox{(\bf function)} \\
    &     & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
  \NT{binder} & ::= & & \mbox{(\bf binders)} \\
    &     & \verb+\Pi+ \mid \verb+\exists+ \mid \verb+\forall+ \mid \verb+\lambda+ \\
  \NT{arg} & ::= & & \mbox{(\bf single argument)} \\
    &     & \verb+_+ \mid x \mid \BLOB \\
  \NT{ptname} & ::= & & \mbox{(\bf possibly typed name)} \\
    &     & \NT{arg} \\
    &  |  & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
  \NT{ptnames} & ::= & & \mbox{(\bf bound variables)} \\
    &     & \NT{arg} \\
    &  |  & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
  \NT{kind} & ::= & & \mbox{(\bf induction kind)} \\
    &     & \verb+rec+ \mid \verb+corec+ \\
  \NT{rule} & ::= & & \mbox{(\bf rules)} \\
    &     & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term} \\[10ex]

  \NT{meta} & ::= & & \mbox{(\bf meta)} \\
    &     & \BLOB \\
    &  |  & [\verb+term+]~x \\
    &  |  & \verb+number+~x \\
    &  |  & \verb+ident+~x \\
    &  |  & \verb+fresh+~x \\
    &  |  & \verb+anonymous+ \\
    &  |  & \verb+fold+~[\verb+left+\mid\verb+right+]~\NT{meta}~\verb+rec+~x~\NT{meta} \\
    &  |  & \verb+default+~\NT{meta}~\NT{meta} \\
    &  |  & \verb+if+~\NT{meta}~\verb+then+~\NT{meta}~\verb+else+~\NT{meta} \\
    &  |  & \verb+fail+ 
\end{array}
\]
\end{table}

\begin{table}
\caption{\label{tab:l2match} Pattern matching of level 2 terms.\strut}
\hrule
\[
\renewcommand{\arraystretch}{3.5}
\begin{array}{@{}c@{}}
  \inference[\sc Constr]
    {t_i \in P_i ~> \mathcal E_i & i\ne j => \DOMAIN(\mathcal E_i)\cap\DOMAIN(\mathcal E_j)=\emptyset}
    {C[t_1,\dots,t_n] \in C[P_1,\dots,P_n] ~> \mathcal E_1 \oplus \cdots \oplus \mathcal E_n}
  \\
  \inference[\sc TermVar]
    {}
    {t \in [\mathtt{term}]~x ~> [x |-> \mathtt{Term}~t]}
  \quad
  \inference[\sc NumVar]
    {}
    {n \in \mathtt{number}~x ~> [x |-> \mathtt{Number}~n]}
  \\
  \inference[\sc IdentVar]
    {}
    {x \in \mathtt{ident}~x ~> [x |-> \mathtt{String}~x]}
  \quad
  \inference[\sc Success]
    {}
    {t \in \mathtt{anonymous} ~> \emptyset}
  \\
  \inference[\sc DefaultT]
    {t \in P_1 ~> \mathcal E}
    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
    \quad
    \mathcal E'(x) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathtt{Some}~\mathcal{E}(x) & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
      \mathcal{E}(x) & \mbox{otherwise}
    \end{array}
    \right.
  \\
  \inference[\sc DefaultF]
    {t \not\in P_1 & t \in P_2 ~> \mathcal E}
    {t \in \mathtt{default}~P_1~P_2 ~> \mathcal E'}
    \quad
    \mathcal E'(x) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathtt{None} & x \in \NAMES(P_1) \setminus \NAMES(P_2) \\
      \mathcal{E}(x) & \mbox{otherwise}
    \end{array}
    \right.
  \\
  \inference[\sc IfT]
    {t \in P_1 ~> \mathcal E' & t \in P_2 ~> \mathcal E}
    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
  \quad
  \inference[\sc IfF]
    {t \not\in P_1 & t \in P_3 ~> \mathcal E}
    {t \in \mathtt{if}~P_1~\mathtt{then}~P_2~\mathtt{else}~P_3 ~> \mathcal E}
  \\
  \inference[\sc FoldR]
    {t \in P_2 ~> \mathcal E & \mathcal{E}(x) \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E''}
  \quad
  \mathcal E''(y) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      \mathcal{E}(y)::\mathcal{E}'(y) & y \in \NAMES(P_2) \setminus \{x\} \\
      \mathcal{E}'(y) & \mbox{otherwise}
    \end{array}  
  \right.
  \\
  \inference[\sc FoldB]
    {t \not\in P_2 & t \in P_1 ~> \mathcal E}
    {t \in \mathtt{fold}~P_1~\mathtt{rec}~x~P_2 ~> \mathcal E'}
  \quad
  \mathcal E'(y) = \left\{
    \renewcommand{\arraystretch}{1}
    \begin{array}{ll}
      [] & y \in \NAMES(P_2) \setminus \{x\} \\
      \mathcal{E}(y) & \mbox{otherwise}
    \end{array}  
  \right.
\end{array}
\]
\hrule
\end{table}

\end{document}