\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
\title{Continuationals semantics for \MATITA}
-\author{Enrico Tassi \qquad Stefano Zacchiroli \\
+\author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
\small Department of Computer Science, University of Bologna \\
\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
-\small \{\texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
+\small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
\newcommand{\DOT}{\mbox{\textbf{.}}}
\newcommand{\SEMICOLON}{\mbox{\textbf{;}}}
\newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
\newcommand{\SKIP}{\ensuremath{\mathtt{skip}}}
\newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}}
-\newcommand{\GOTO}[2]{\ensuremath{\mathtt{goal} ~ #1 ~ #2}}
+\newcommand{\SELECT}[2]{\ensuremath{\mathtt{select} ~ #1 ~ #2}}
\newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
\newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
\newcommand{\FILTERFUN}[2]{\FUN{filter}{#1,#2}}
\newcommand{\MAPFUN}[2]{\FUN{map}{#1,#2}}
\newcommand{\DEEPMAPFUN}[2]{\FUN{deep\_map}{#1,#2}}
-% \newcommand{\ISCLOSEDFUN}{\ensuremath{\mathit{is\_closed}}}
\newcommand{\ISOPENFUN}{\ensuremath{\mathit{is\_open}}}
-% \newcommand{\OPENFUN}{\ensuremath{\mathit{open}}}
\newcommand{\CLOSEFUN}{\ensuremath{\mathit{close}}}
\newcommand{\GOALOFFUN}{\ensuremath{\mathit{goal\_of}}}
+\newcommand{\DEEPCLOSEFUN}[2]{\FUN{deep\_close}{#1,#2}}
\begin{document}
\maketitle
\[
\begin{array}{rcll}
C & ::= & & \mbox{(\textbf{continuationals})} \\
- & & \DOT & \mbox{(dot)} \\
+ & & C ~ \DOT & \mbox{(dot)} \\
& | & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\
& | & \BRANCH & \mbox{(branch)} \\
& | & \SHIFT & \mbox{(shift)} \\
& | & \MERGE & \mbox{(merge)} \\
- & | & \GOTO{n}{C} & \mbox{(goto)} \\
+ & | & \SELECT{n_1,\dots,n_k}{C} & \mbox{(select)} \\
& | & \TACTICAL{T} & \mbox{(tactical)} \\[2ex]
T & ::= & & \mbox{(\textbf{tacticals})} \\
\[
\begin{array}{rcll}
\mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\
- \xi & & & \mbox{(metasenv)} \\
+ \xi & = & \langle n,\alpha\rangle~\LIST& \mbox{(metasenv)} \\
\Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\
\GOALSWITCH & = & \OPEN{n} \quad | \quad \CLOSED{n} & \\
\tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\
\[
\begin{array}{rcl}
- \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
- \xi\times\GOAL~\LIST\times\GOAL~\LIST \\[1ex]
\mathit{filter} & : & (\alpha->\BOOL)->\alpha~\LIST->\alpha~\LIST \\
\mathit{map} & : & (\alpha->\beta)->\alpha~\LIST->\beta~\LIST \\
\mathit{deep\_map} & :
- & (\alpha->\beta)->\alpha~\LIST~\STACK->\beta~\LIST~\STACK \\[1ex]
+ & (\alpha->\beta)->\alpha~\LIST~\STACK->\beta~\LIST~\STACK \\
+ \in & : & \alpha->\alpha~\LIST->\BOOL \\
+ \cup & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\
+ \setminus & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\
+\end{array}
+\]
+
+\[
+\begin{array}{rcl}
+ \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
+ \xi\times\GOAL~\LIST\times\GOAL~\LIST \\[1ex]
% \ISCLOSEDFUN & : & \GOALSWITCH -> \BOOL \\
\ISOPENFUN & : & \GOALSWITCH -> \BOOL \\
\CLOSEFUN & : & \GOALSWITCH -> \GOALSWITCH \\[1ex]
% \OPENFUN & : & \GOAL -> \GOALSWITCH \\[1ex]
- \GOALOFFUN & : & \GOALSWITCH -> \GOAL \\
+ \GOALOFFUN & : & \GOALSWITCH -> \GOAL \\[1ex]
+ \mathit{deep\_close} & :
+ & \GOAL~\LIST -> \GOALSWITCH~\STACK -> \GOALSWITCH~\STACK \\[1ex]
+\end{array}
+\]
+
+\[
+\begin{array}{rcl}
+ \DEEPCLOSEFUN{G}{\Gamma}
+ & =
+ & \MAPFUN{\mathit{fold}
+ (\lambda g.\lambda acc.
+ \mathit{if}~\GOALOFFUN(g)\in G~\land\ISOPENFUN(g)~
+ \mathit{then}~[]~
+ \mathit{else}~[g]\cup\mathit{acc})
+ []}{\Gamma}
\end{array}
\]
\[
\begin{array}{rcl}
\SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
+ \quad (n\geq 1)
& =
& \langle\xi_n,
- \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPMAPFUN{\CLOSEFUN}{G^C_n,\Gamma},
+ \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPCLOSEFUN{G^C_n}{\Gamma},
\tau\setminus G^C_n,\kappa\setminus G^O_n\rangle
\\[1ex]
\SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
\\[2ex]
- \SEM{~\DOT~}{\xi}{(g::G)::\Gamma}{\tau}{K::\kappa}
+ \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa}
& =
- & \langle\xi, [g]::\Gamma, \tau,
- (\MAPFUN{\mathtt{Open}}{\FILTERFUN{\ISOPENFUN}{G}}\cup K)::\kappa\rangle
- \\[2ex]
+ & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle
+ \\[1ex]
- \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(n::N)::\kappa}
- & =
- & \langle\xi, [\OPEN{n}]::\Gamma, \tau, N::\kappa\rangle
+ \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
+ \langle \xi',G::\Gamma',\tau',K::\kappa' \rangle
+ = \SEM{C}{\xi}{\Gamma}{\tau}{\kappa}}
+ \\[1ex]
+
+ \multicolumn{3}{l}{\hspace{2em}\mathit{and} ~
+ \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle =
+ \left\{
+ \begin{array}{ll}
+ \langle \xi', [g]::\Gamma', \tau', (\MAPFUN{\GOALOFFUN}{G'}\cup K)::\kappa'
+ \rangle
+ & \FILTERFUN{\ISOPENFUN}{G} = g::G'
+ \\
+ \langle \xi', [\mathtt{Open}~n]::\Gamma', \tau', K'::\kappa' \rangle
+ & \FILTERFUN{\ISOPENFUN}{G} = []~\land~K=n::K'
+ \end{array}
+ \right.}
\\[2ex]
\SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
+ \quad (n\geq 2)
& =
& \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
\\[2ex]
& =
& \langle\xi,
[g_i]::[g_{i+1};\dots;g_n]::\Gamma,
- (T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K)::\tau,
+ \tau'::\tau,
[]::\kappa\rangle
+ \\[1ex]
+
+ & & \mathit{where} ~
+ \tau' = T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K
\\[2ex]
\SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
& =
- & \langle\xi,
- (T
- \cup\FILTERFUN{\ISOPENFUN}{G}
- \cup[g_i;\dots;g_n]
- \cup\MAPFUN{\mathtt{Open}}{K})::\Gamma,
- \tau,
- \kappa\rangle
+ & \langle \xi, \Gamma'::\Gamma, \tau, \kappa \rangle
+ \\[1ex]
+
+ & & \mathit{where} ~
+ \Gamma' =
+ T \cup\FILTERFUN{\ISOPENFUN}{G}
+ \cup[g_i;\dots;g_n]
+ \cup\MAPFUN{\mathtt{Open}}{K}
\\[2ex]
- \SEM{\GOTO{n}{C}}{\xi}{\Gamma}{\tau}{\kappa}
+ \SEM{\SELECT{n_1,\dots,n_k}{C}}{\xi}{\Gamma}{\tau}{\kappa}
& =
& \langle \xi',\Gamma',\tau',\kappa' \rangle
\\[1ex]
& & \mathit{where} ~
+ \forall ~ i=1,\dots,k,~\exists ~ \alpha_i,~\langle n_i,\alpha_i\rangle \in \xi
+ \\[1ex]
+
+ & & \mathit{and} ~
\langle \xi', []::\Gamma', []::\tau', []::\kappa' \rangle
- = \SEM{C}{\xi}{[\OPEN{n}]::\Gamma}{[]::\tau}{[]::\kappa}
+ = \SEM{C}{\xi}{\MAPFUN{\mathtt{Open}}{[n_1;\dots;n_k]}::\Gamma}{[]::\tau}{[]::\kappa}
\\[2ex]
\end{array}
projects / helm.git / commitdiff