- fixed some metasenv issues

- remove closed goals from todo and dot continuations
- use more basic functions for mapping/filtering

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index 1cc0dadd99e6fa090ef4e4e082ed3f99975b1254..32c6832df2ee83d0e4e65e55e0fa2ae8ddfad6de 100644 (file)
--- a/helm/ocaml/tactics/doc/main.tex
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -26,6 +26,7 @@
 \newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
 \newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
 \newcommand{\LIST}{\ensuremath{\mathtt{list}}}
+\newcommand{\BOOL}{\ensuremath{\mathtt{bool}}}
 \newcommand{\STACK}{\ensuremath{\mathtt{stack}}}
 \newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}}
 \newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#1}}
@@ -36,9 +37,14 @@
 \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
 
 \newcommand{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}}
-\newcommand{\FILTEROPEN}[1]{\FUN{filter\_open}{#1}}
-\newcommand{\MAPOPEN}[1]{\FUN{map\_open}{#1}}
-\newcommand{\DEEPCLOSE}[1]{\FUN{deep\_close}{#1}}
+\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}}}
 
 \begin{document}
 \maketitle
@@ -84,20 +90,23 @@
  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
   \mbox{(continuationals semantics)} \\
  \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH ->
-  \GOAL~\LIST \times \GOAL~\LIST & \mbox{(tacticals semantics)} \\
+  \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tacticals semantics)} \\
 \end{array}
 \]
 
 \[
 \begin{array}{rcl}
  \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
-  \GOAL~\LIST\times\GOAL~\LIST \\
- \mathit{map\_open} & : & \GOAL~\LIST -> \GOALSWITCH~\LIST \\
- \mathit{filter\_open} & : & \GOALSWITCH~\LIST -> \GOAL~\LIST \\
- \mathit{deep\_close} & :
- & \GOAL~\LIST -> \GOALSWITCH~\LIST~\STACK -> \GOALSWITCH~\LIST~\STACK \\
- \cup & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
- \setminus & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
+  \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]
+%  \ISCLOSEDFUN & : & \GOALSWITCH -> \BOOL \\
+ \ISOPENFUN & : & \GOALSWITCH -> \BOOL \\
+ \CLOSEFUN & : & \GOALSWITCH -> \GOALSWITCH \\[1ex]
+%  \OPENFUN & : & \GOAL -> \GOALSWITCH \\[1ex]
+ \GOALOFFUN & : & \GOALSWITCH -> \GOAL \\
 \end{array}
 \]
 
@@ -105,7 +114,7 @@
 \begin{array}{rlcc}
  \TSEM{\APPLY{tac}}{\xi}{\OPEN{n}} & =
  & \mathit{apply\_tac}(\mathit{tac},\xi,n) & \\
- \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle [], [n]\rangle & \\
+ \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle \xi, [], [n]\rangle & \\
 \end{array}
 \]
 
@@ -113,7 +122,9 @@
 \begin{array}{rcl}
  \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
  & =
- & \langle\xi_n,\MAPOPEN{G^O_n}::\DEEPCLOSE{G^C_n,\Gamma},\tau,\kappa\rangle
+ & \langle\xi_n,
+   \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPMAPFUN{\CLOSEFUN}{G^C_n,\Gamma},
+   \tau\setminus G^C_n,\kappa\setminus G^O_n\rangle
  \\[1ex]
 
  \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
@@ -148,7 +159,7 @@
  \SEM{~\DOT~}{\xi}{(g::G)::\Gamma}{\tau}{K::\kappa}
  & =
  & \langle\xi, [g]::\Gamma, \tau,
-   (\FILTEROPEN{G}\cup K)::\kappa\rangle
+   (\MAPFUN{\mathtt{Open}}{\FILTERFUN{\ISOPENFUN}{G}}\cup K)::\kappa\rangle
  \\[2ex]
 
  \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(n::N)::\kappa}
@@ -165,25 +176,28 @@
  & =
  & \langle\xi,
    [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
-   (T\cup\FILTEROPEN{G}\cup K)::\tau,
+   (T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K)::\tau,
    []::\kappa\rangle
  \\[2ex]
 
  \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
  & =
  & \langle\xi,
-   (T\cup G\cup[g_i;\dots;g_n]\cup\MAPOPEN{K})::\Gamma,
+   (T
+    \cup\FILTERFUN{\ISOPENFUN}{G}
+    \cup[g_i;\dots;g_n]
+    \cup\MAPFUN{\mathtt{Open}}{K})::\Gamma,
    \tau,
    \kappa\rangle
  \\[2ex]
 
  \SEM{\GOTO{n}{C}}{\xi}{\Gamma}{\tau}{\kappa}
  & = 
- & \langle\xi',\Gamma',\tau\setminus[n],\kappa\setminus[n]\rangle
+ & \langle \xi',\Gamma',\tau',\kappa' \rangle
  \\[1ex]
 
  & & \mathit{where} ~
- \langle \xi', []::\Gamma', []::\tau, []::\kappa\rangle
+ \langle \xi', []::\Gamma', []::\tau', []::\kappa' \rangle
  = \SEM{C}{\xi}{[\OPEN{n}]::\Gamma}{[]::\tau}{[]::\kappa}
  \\[2ex]