Merged.
--- a/doc-src/IsarAdvanced/Classes/classes.tex Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/classes.tex Mon Dec 08 14:22:42 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
@@ -10,40 +8,10 @@
\usepackage{../../pdfsetup}
-%% setup
-
-% hyphenation
\hyphenation{Isabelle}
\hyphenation{Isar}
-
-% logical markup
-\newcommand{\strong}[1]{{\bfseries {#1}}}
-\newcommand{\qn}[1]{\emph{#1}}
-
-% typographic conventions
-\newcommand{\qt}[1]{``{#1}''}
-
-% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
-% invisibility
\isadroptag{theory}
-% quoted segments
-\makeatletter
-\isakeeptag{quote}
-\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquote}{\begin{quotesegment}}
-\renewcommand{\endisatagquote}{\end{quotesegment}}
-\makeatother
-
-%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
-%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
-%\renewcommand{\isasymotimes}{\isamath{\circ}}
-
-
-%% content
-
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Haskell-style type classes with Isabelle/Isar}
\author{\emph{Florian Haftmann}}
@@ -69,7 +37,6 @@
\input{Thy/document/Classes.tex}
\begingroup
-%\tocentry{\bibname}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../../manual}
\endgroup
--- a/doc-src/IsarAdvanced/Classes/style.sty Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/style.sty Mon Dec 08 14:22:42 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
%% toc
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
@@ -7,54 +5,37 @@
%% references
\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\chref}[1]{chapter~\ref{#1}}
\newcommand{\figref}[1]{figure~\ref{#1}}
-%% glossary
-\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
-\newcommand{\seeglossary}[1]{\emph{#1}}
-\newcommand{\glossaryname}{Glossary}
-\renewcommand{\nomname}{\glossaryname}
-\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+%% verbatim text
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-%% index
-\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
-\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
-\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
-\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
+%% quoted segments
+\makeatletter
+\isakeeptag{quote}
+\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquote}{\begin{quotesegment}}
+\renewcommand{\endisatagquote}{\end{quotesegment}}
+\makeatother
-%% math
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\isasymvartheta}{\isamath{\theta}}
-\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
-
+%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
\pagestyle{headings}
-\sloppy
\binperiod
\underscoreon
\renewcommand{\isadigit}[1]{\isamath{#1}}
-\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
-
-\isafoldtag{FIXME}
-\isakeeptag{mlref}
-\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
-\renewcommand{\endisatagmlref}{\endgroup}
+\isabellestyle{it}
-\newcommand{\isasymGUESS}{\isakeyword{guess}}
-\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
-\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymEND}{\isakeyword{end}}
-\newcommand{\isasymCONSTS}{\isakeyword{consts}}
-\newcommand{\isasymDEFS}{\isakeyword{defs}}
-\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
-\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
-
-\isabellestyle{it}
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/codegen.tex Mon Dec 08 14:22:42 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
\documentclass[12pt,a4paper,fleqn]{report}
\usepackage{latexsym,graphicx}
@@ -12,43 +10,10 @@
\usepackage{tikz}
\usepackage{../../pdfsetup}
-%% setup
-
-% hyphenation
\hyphenation{Isabelle}
\hyphenation{Isar}
-
-% logical markup
-\newcommand{\strong}[1]{{\bfseries {#1}}}
-\newcommand{\qn}[1]{\emph{#1}}
-
-% typographic conventions
-\newcommand{\qt}[1]{``{#1}''}
-
-% verbatim text
-\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-
-% invisibility
\isadroptag{theory}
-% quoted segments
-\makeatletter
-\isakeeptag{quote}
-\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquote}{\begin{quotesegment}}
-\renewcommand{\endisatagquote}{\end{quotesegment}}
-\makeatother
-
-\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
-
-% hack
-\newcommand{\isasymSML}{SML}
-
-
-%% contents
-
\title{\includegraphics[scale=0.5]{isabelle_isar}
\\[4ex] Code generation from Isabelle/HOL theories}
\author{\emph{Florian Haftmann}}
@@ -75,7 +40,6 @@
\input{Thy/document/ML.tex}
\begingroup
-%\tocentry{\bibname}
\bibliographystyle{plain} \small\raggedright\frenchspacing
\bibliography{../../manual}
\endgroup
--- a/doc-src/IsarAdvanced/Codegen/style.sty Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarAdvanced/Codegen/style.sty Mon Dec 08 14:22:42 2008 +0100
@@ -1,5 +1,3 @@
-
-%% $Id$
%% toc
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
@@ -7,15 +5,6 @@
%% references
\newcommand{\secref}[1]{\S\ref{#1}}
-\newcommand{\chref}[1]{chapter~\ref{#1}}
-\newcommand{\figref}[1]{figure~\ref{#1}}
-
-%% glossary
-\renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
-\newcommand{\seeglossary}[1]{\emph{#1}}
-\newcommand{\glossaryname}{Glossary}
-\renewcommand{\nomname}{\glossaryname}
-\renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
%% index
\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
@@ -23,38 +12,49 @@
\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
-%% math
-\newcommand{\text}[1]{\mbox{#1}}
-\newcommand{\isasymvartheta}{\isamath{\theta}}
-\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+
+%% verbatim text
+\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
+%% quoted segments
+\makeatletter
+\isakeeptag{quote}
+\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquote}{\begin{quotesegment}}
+\renewcommand{\endisatagquote}{\end{quotesegment}}
+\makeatother
+
+\isakeeptag{quotett}
+\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
+
+%% a trick
+\newcommand{\isasymSML}{SML}
+
+%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
\pagestyle{headings}
-\sloppy
\binperiod
\underscoreon
\renewcommand{\isadigit}[1]{\isamath{#1}}
+%% ml reference
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
-\isafoldtag{FIXME}
\isakeeptag{mlref}
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
\renewcommand{\endisatagmlref}{\endgroup}
-\newcommand{\isasymGUESS}{\isakeyword{guess}}
-\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
-\newcommand{\isasymTHEORY}{\isakeyword{theory}}
-\newcommand{\isasymUSES}{\isakeyword{uses}}
-\newcommand{\isasymEND}{\isakeyword{end}}
-\newcommand{\isasymCONSTS}{\isakeyword{consts}}
-\newcommand{\isasymDEFS}{\isakeyword{defs}}
-\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
-\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
+\isabellestyle{it}
-\isabellestyle{it}
%%% Local Variables:
%%% mode: latex
--- a/doc-src/IsarImplementation/Thy/ML.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Dec 08 14:22:42 2008 +0100
@@ -306,7 +306,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- @{ML "Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix
+ @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
-> theory -> term * theory"} \\
@{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
\end{mldecls}
@@ -319,7 +319,7 @@
@{ML "(fn (t, thy) => Thm.add_def false false
(\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
(Sign.declare_const []
- ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
+ ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
\end{mldecls}
\noindent With increasing numbers of applications, this code gets quite
@@ -333,7 +333,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|> (fn (t, thy) => thy
|> Thm.add_def false false
(\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
@@ -357,7 +357,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|-> (fn t => Thm.add_def false false
(\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
"}
@@ -367,7 +367,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
|-> (fn def => Thm.add_def false false (\"bar_def\", def))
"}
@@ -378,7 +378,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
||> Sign.add_path \"foobar\"
|-> (fn t => Thm.add_def false false
(\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
@@ -390,8 +390,8 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> Sign.declare_const [] ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
|-> (fn (t1, t2) => Thm.add_def false false
(\"bar_def\", Logic.mk_equals (t1, t2)))
"}
@@ -437,7 +437,7 @@
in
thy
|> fold_map (fn const => Sign.declare_const []
- ((Name.binding const, @{typ \"foo => foo\"}), NoSyn)) consts
+ ((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
|>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
|-> (fn defs => fold_map (fn def =>
Thm.add_def false false (\"\", def)) defs)
@@ -475,12 +475,12 @@
\smallskip\begin{mldecls}
@{ML "thy
|> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const [] ((Name.binding \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
||>> `(fn thy => Sign.declared_const thy
- (Sign.full_name thy \"foobar\"))
+ (Sign.full_name thy (Binding.name \"foobar\")))
|-> (fn (t, b) => if b then I
else Sign.declare_const []
- ((Name.binding \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
+ ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
"}
\end{mldecls}
*}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Dec 08 14:22:42 2008 +0100
@@ -358,7 +358,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- \verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix|\isasep\isanewline%
+ \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
\verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
\end{mldecls}
@@ -371,7 +371,7 @@
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
\verb| (Sign.declare_const []|\isasep\isanewline%
-\verb| ((Name.binding "bar", @{typ "foo => foo"}), NoSyn) thy)|
+\verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
\end{mldecls}
\noindent With increasing numbers of applications, this code gets quite
@@ -386,7 +386,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
@@ -425,7 +425,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -435,7 +435,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false ("bar_def", def))|\isasep\isanewline%
@@ -446,7 +446,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
\verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -458,8 +458,8 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
\verb| ("bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
@@ -520,7 +520,7 @@
\verb|in|\isasep\isanewline%
\verb| thy|\isasep\isanewline%
\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
-\verb| ((Name.binding const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
+\verb| ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
\verb| Thm.add_def false false ("", def)) defs)|\isasep\isanewline%
@@ -588,12 +588,12 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Name.binding "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
-\verb| (Sign.full_name thy "foobar"))|\isasep\isanewline%
+\verb| (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
\verb| else Sign.declare_const []|\isasep\isanewline%
-\verb| ((Name.binding "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
+\verb| ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
\end{mldecls}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/document/logic.tex Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Mon Dec 08 14:22:42 2008 +0100
@@ -3,9 +3,6 @@
\def\isabellecontext{logic}%
%
\isadelimtheory
-\isanewline
-\isanewline
-\isanewline
%
\endisadelimtheory
%
@@ -328,9 +325,9 @@
\indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexml{lambda}\verb|lambda: term -> term -> term| \\
\indexml{betapply}\verb|betapply: term * term -> term| \\
- \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Name.binding * typ) * mixfix ->|\isasep\isanewline%
+ \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Name.binding * term ->|\isasep\isanewline%
+ \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
\indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Mon Dec 08 14:22:42 2008 +0100
@@ -816,13 +816,13 @@
\indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
\indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
\indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
- \indexml{NameSpace.full}\verb|NameSpace.full: NameSpace.naming -> string -> string| \\
+ \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
\end{mldecls}
\begin{mldecls}
\indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
\indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
\indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
- \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> string -> NameSpace.T -> NameSpace.T| \\
+ \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
\indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
\indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
\end{mldecls}
@@ -851,9 +851,9 @@
\item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
naming policy by extending its path component.
- \item \verb|NameSpace.full|\isa{naming\ name} turns a name
- specification (usually a basic name) into the fully qualified
- internal version, according to the given naming policy.
+ \item \verb|NameSpace.full_name|\isa{naming\ binding} turns a name
+ binding (usually a basic name) into the fully qualified
+ internal name, according to the given naming policy.
\item \verb|NameSpace.T| represents name spaces.
@@ -861,15 +861,16 @@
maintaining name spaces according to theory data management
(\secref{sec:context-data}).
- \item \verb|NameSpace.declare|~\isa{naming\ name\ space} enters a
- fully qualified name into the name space, with external accesses
- determined by the naming policy.
+ \item \verb|NameSpace.declare|~\isa{naming\ bindings\ space} enters a
+ name binding as fully qualified internal name into the name space,
+ with external accesses determined by the naming policy.
\item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
(partially qualified) external name.
This operation is mostly for parsing! Note that fully qualified
- names stemming from declarations are produced via \verb|NameSpace.full| (or its derivatives for \verb|theory| and
+ names stemming from declarations are produced via \verb|NameSpace.full_name| and \verb|NameSpace.declare|
+ (or their derivatives for \verb|theory| and
\verb|Proof.context|).
\item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
--- a/doc-src/IsarImplementation/Thy/logic.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy Mon Dec 08 14:22:42 2008 +0100
@@ -1,6 +1,3 @@
-
-(* $Id$ *)
-
theory logic imports base begin
chapter {* Primitive logic \label{ch:logic} *}
@@ -326,9 +323,9 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.declare_const: "Properties.T -> (Name.binding * typ) * mixfix ->
+ @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
theory -> term * theory"} \\
- @{index_ML Sign.add_abbrev: "string -> Properties.T -> Name.binding * term ->
+ @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
theory -> (term * term) * theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
--- a/doc-src/IsarImplementation/Thy/prelim.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy Mon Dec 08 14:22:42 2008 +0100
@@ -707,13 +707,13 @@
@{index_ML_type NameSpace.naming} \\
@{index_ML NameSpace.default_naming: NameSpace.naming} \\
@{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
- @{index_ML NameSpace.full: "NameSpace.naming -> string -> string"} \\
+ @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML_type NameSpace.T} \\
@{index_ML NameSpace.empty: NameSpace.T} \\
@{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
- @{index_ML NameSpace.declare: "NameSpace.naming -> string -> NameSpace.T -> NameSpace.T"} \\
+ @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
@{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
@{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
\end{mldecls}
@@ -743,9 +743,9 @@
\item @{ML NameSpace.add_path}~@{text "path naming"} augments the
naming policy by extending its path component.
- \item @{ML NameSpace.full}@{text "naming name"} turns a name
- specification (usually a basic name) into the fully qualified
- internal version, according to the given naming policy.
+ \item @{ML NameSpace.full_name}@{text "naming binding"} turns a name
+ binding (usually a basic name) into the fully qualified
+ internal name, according to the given naming policy.
\item @{ML_type NameSpace.T} represents name spaces.
@@ -754,16 +754,17 @@
maintaining name spaces according to theory data management
(\secref{sec:context-data}).
- \item @{ML NameSpace.declare}~@{text "naming name space"} enters a
- fully qualified name into the name space, with external accesses
- determined by the naming policy.
+ \item @{ML NameSpace.declare}~@{text "naming bindings space"} enters a
+ name binding as fully qualified internal name into the name space,
+ with external accesses determined by the naming policy.
\item @{ML NameSpace.intern}~@{text "space name"} internalizes a
(partially qualified) external name.
This operation is mostly for parsing! Note that fully qualified
names stemming from declarations are produced via @{ML
- "NameSpace.full"} (or its derivatives for @{ML_type theory} and
+ "NameSpace.full_name"} and @{ML "NameSpace.declare"}
+ (or their derivatives for @{ML_type theory} and
@{ML_type Proof.context}).
\item @{ML NameSpace.extern}~@{text "space name"} externalizes a
--- a/etc/settings Mon Dec 08 14:18:29 2008 +0100
+++ b/etc/settings Mon Dec 08 14:22:42 2008 +0100
@@ -75,8 +75,11 @@
ISABELLE_SCALA="scala"
ISABELLE_JAVA="java"
-[ -e "$ISABELLE_HOME/contrib/scala" ] && \
+if [ -e "$ISABELLE_HOME/contrib/scala" ]; then
classpath "$ISABELLE_HOME/contrib/scala/lib/scala-library.jar"
+elif [ -e "$ISABELLE_HOME/../scala" ]; then
+ classpath "$ISABELLE_HOME/../scala/lib/scala-library.jar"
+fi
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
@@ -232,10 +235,22 @@
## Set HOME only for tools you have installed!
# External provers
-E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
-VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" \
- "$ISABELLE_HOME/contrib/SystemOnTPTP" "")
-SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
+E_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
+ "$ISABELLE_HOME/../E/$ML_PLATFORM" \
+ "/usr/local/E" \
+ "")
+VAMPIRE_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
+ "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
+ "/usr/local/Vampire" \
+ "$ISABELLE_HOME/contrib/SystemOnTPTP" \
+ "")
+SPASS_HOME=$(choosefrom \
+ "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
+ "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
+ "/usr/local/SPASS" \
+ "")
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
--- a/src/HOL/Arith_Tools.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Arith_Tools.thy Mon Dec 08 14:22:42 2008 +0100
@@ -40,7 +40,7 @@
text{*No longer required as a simprule because of the @{text inverse_fold}
simproc*}
lemma Suc_diff_number_of:
- "neg (number_of (uminus v)::int) ==>
+ "Int.Pls < v ==>
Suc m - (number_of v) = m - (number_of (Int.pred v))"
apply (subst Suc_diff_eq_diff_pred)
apply simp
--- a/src/HOL/Library/Nat_Infinity.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Dec 08 14:22:42 2008 +0100
@@ -146,8 +146,8 @@
by (simp_all add: plus_inat_def zero_inat_def split: inat.splits)
lemma plus_inat_number [simp]:
- "(number_of k \<Colon> inat) + number_of l = (if neg (number_of k \<Colon> int) then number_of l
- else if neg (number_of l \<Colon> int) then number_of k else number_of (k + l))"
+ "(number_of k \<Colon> inat) + number_of l = (if k < Int.Pls then number_of l
+ else if l < Int.Pls then number_of k else number_of (k + l))"
unfolding number_of_inat_def plus_inat_simps nat_arith(1) if_distrib [symmetric, of _ Fin] ..
lemma iSuc_number [simp]:
@@ -165,6 +165,58 @@
unfolding iSuc_plus_1 by (simp_all add: add_ac)
+subsection {* Multiplication *}
+
+instantiation inat :: comm_semiring_1
+begin
+
+definition
+ times_inat_def [code del]:
+ "m * n = (case m of \<infinity> \<Rightarrow> if n = 0 then 0 else \<infinity> | Fin m \<Rightarrow>
+ (case n of \<infinity> \<Rightarrow> if m = 0 then 0 else \<infinity> | Fin n \<Rightarrow> Fin (m * n)))"
+
+lemma times_inat_simps [simp, code]:
+ "Fin m * Fin n = Fin (m * n)"
+ "\<infinity> * \<infinity> = \<infinity>"
+ "\<infinity> * Fin n = (if n = 0 then 0 else \<infinity>)"
+ "Fin m * \<infinity> = (if m = 0 then 0 else \<infinity>)"
+ unfolding times_inat_def zero_inat_def
+ by (simp_all split: inat.split)
+
+instance proof
+ fix a b c :: inat
+ show "(a * b) * c = a * (b * c)"
+ unfolding times_inat_def zero_inat_def
+ by (simp split: inat.split)
+ show "a * b = b * a"
+ unfolding times_inat_def zero_inat_def
+ by (simp split: inat.split)
+ show "1 * a = a"
+ unfolding times_inat_def zero_inat_def one_inat_def
+ by (simp split: inat.split)
+ show "(a + b) * c = a * c + b * c"
+ unfolding times_inat_def zero_inat_def
+ by (simp split: inat.split add: left_distrib)
+ show "0 * a = 0"
+ unfolding times_inat_def zero_inat_def
+ by (simp split: inat.split)
+ show "a * 0 = 0"
+ unfolding times_inat_def zero_inat_def
+ by (simp split: inat.split)
+ show "(0::inat) \<noteq> 1"
+ unfolding zero_inat_def one_inat_def
+ by simp
+qed
+
+end
+
+lemma mult_iSuc: "iSuc m * n = n + m * n"
+ unfolding iSuc_plus_1 by (simp add: ring_simps)
+
+lemma mult_iSuc_right: "m * iSuc n = m + m * n"
+ unfolding iSuc_plus_1 by (simp add: ring_simps)
+
+
subsection {* Ordering *}
instantiation inat :: ordered_ab_semigroup_add
@@ -201,6 +253,15 @@
end
+instance inat :: pordered_comm_semiring
+proof
+ fix a b c :: inat
+ assume "a \<le> b" and "0 \<le> c"
+ thus "c * a \<le> c * b"
+ unfolding times_inat_def less_eq_inat_def zero_inat_def
+ by (simp split: inat.splits)
+qed
+
lemma inat_ord_number [simp]:
"(number_of m \<Colon> inat) \<le> number_of n \<longleftrightarrow> (number_of m \<Colon> nat) \<le> number_of n"
"(number_of m \<Colon> inat) < number_of n \<longleftrightarrow> (number_of m \<Colon> nat) < number_of n"
--- a/src/HOL/NatBin.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/NatBin.thy Mon Dec 08 14:22:42 2008 +0100
@@ -141,10 +141,10 @@
(*"neg" is used in rewrite rules for binary comparisons*)
lemma add_nat_number_of [simp]:
"(number_of v :: nat) + number_of v' =
- (if neg (number_of v :: int) then number_of v'
- else if neg (number_of v' :: int) then number_of v
+ (if v < Int.Pls then number_of v'
+ else if v' < Int.Pls then number_of v
else number_of (v + v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
+ unfolding nat_number_of_def number_of_is_id numeral_simps
by (simp add: nat_add_distrib)
@@ -160,19 +160,19 @@
lemma diff_nat_number_of [simp]:
"(number_of v :: nat) - number_of v' =
- (if neg (number_of v' :: int) then number_of v
+ (if v' < Int.Pls then number_of v
else let d = number_of (v + uminus v') in
if neg d then 0 else nat d)"
-by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def)
-
+ unfolding nat_number_of_def number_of_is_id numeral_simps neg_def
+ by auto
subsubsection{*Multiplication *}
lemma mult_nat_number_of [simp]:
"(number_of v :: nat) * number_of v' =
- (if neg (number_of v :: int) then 0 else number_of (v * v'))"
- unfolding nat_number_of_def number_of_is_id neg_def
+ (if v < Int.Pls then 0 else number_of (v * v'))"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
by (simp add: nat_mult_distrib)
@@ -258,15 +258,21 @@
subsubsection{*Less-than (<) *}
-(*"neg" is used in rewrite rules for binary comparisons*)
lemma less_nat_number_of [simp]:
- "((number_of v :: nat) < number_of v') =
- (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)
- else neg (number_of (v + uminus v') :: int))"
- unfolding neg_def nat_number_of_def number_of_is_id
+ "(number_of v :: nat) < number_of v' \<longleftrightarrow>
+ (if v < v' then Int.Pls < v' else False)"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
by auto
+subsubsection{*Less-than-or-equal *}
+
+lemma le_nat_number_of [simp]:
+ "(number_of v :: nat) \<le> number_of v' \<longleftrightarrow>
+ (if v \<le> v' then True else v \<le> Int.Pls)"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
+
(*Maps #n to n for n = 0, 1, 2*)
lemmas numerals = nat_numeral_0_eq_0 nat_numeral_1_eq_1 numeral_2_eq_2
@@ -440,17 +446,18 @@
text{*Simplification already does @{term "n<0"}, @{term "n\<le>0"} and @{term "0\<le>n"}.*}
lemma eq_number_of_0 [simp]:
- "number_of v = (0::nat) \<longleftrightarrow> number_of v \<le> (0::int)"
- unfolding nat_number_of_def number_of_is_id by auto
+ "number_of v = (0::nat) \<longleftrightarrow> v \<le> Int.Pls"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by auto
lemma eq_0_number_of [simp]:
- "(0::nat) = number_of v \<longleftrightarrow> number_of v \<le> (0::int)"
+ "(0::nat) = number_of v \<longleftrightarrow> v \<le> Int.Pls"
by (rule trans [OF eq_sym_conv eq_number_of_0])
lemma less_0_number_of [simp]:
- "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
-by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
-
+ "(0::nat) < number_of v \<longleftrightarrow> Int.Pls < v"
+ unfolding nat_number_of_def number_of_is_id numeral_simps
+ by simp
lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
@@ -699,7 +706,7 @@
lemma nat_number_of_mult_left:
"number_of v * (number_of v' * (k::nat)) =
- (if neg (number_of v :: int) then 0
+ (if v < Int.Pls then 0
else number_of (v * v') * k)"
by simp
--- a/src/HOL/Nominal/nominal_primrec.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Mon Dec 08 14:22:42 2008 +0100
@@ -230,7 +230,7 @@
fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
let
val (raw_eqns, atts) = split_list eqns_atts;
- val eqns = map (apfst Name.name_of) raw_eqns;
+ val eqns = map (apfst Binding.base_name) raw_eqns;
val dt_info = NominalPackage.get_nominal_datatypes thy;
val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
--- a/src/HOL/ROOT.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/ROOT.ML Mon Dec 08 14:22:42 2008 +0100
@@ -3,7 +3,7 @@
Classical Higher-order Logic -- batteries included.
*)
-use_thy "Complex/Complex_Main";
+use_thy "Complex_Main";
val HOL_proofs = ! Proofterm.proofs;
--- a/src/HOL/Tools/ComputeNumeral.thy Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy Mon Dec 08 14:22:42 2008 +0100
@@ -129,7 +129,8 @@
(* Addition for nat *)
lemma natadd: "number_of x + ((number_of y)::nat) = (if neg x then (number_of y) else (if neg y then number_of x else (number_of (x + y))))"
- by (auto simp add: number_of_is_id)
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by auto
(* Subtraction for nat *)
lemma natsub: "(number_of x) - ((number_of y)::nat) =
@@ -140,18 +141,14 @@
(* Multiplication for nat *)
lemma natmul: "(number_of x) * ((number_of y)::nat) =
(if neg x then 0 else (if neg y then 0 else number_of (x * y)))"
- apply (auto simp add: number_of_is_id neg_def iszero_def)
- apply (case_tac "x > 0")
- apply auto
- apply (rule order_less_imp_le)
- apply (simp add: mult_strict_left_mono[where a=y and b=0 and c=x, simplified])
- done
+ unfolding nat_number_of_def number_of_is_id neg_def
+ by (simp add: nat_mult_distrib)
lemma nateq: "(((number_of x)::nat) = (number_of y)) = ((lezero x \<and> lezero y) \<or> (x = y))"
by (auto simp add: iszero_def lezero_def neg_def number_of_is_id)
lemma natless: "(((number_of x)::nat) < (number_of y)) = ((x < y) \<and> (\<not> (lezero y)))"
- by (auto simp add: number_of_is_id neg_def lezero_def)
+ by (simp add: lezero_def numeral_simps not_le)
lemma natle: "(((number_of x)::nat) \<le> (number_of y)) = (y < x \<longrightarrow> lezero x)"
by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
--- a/src/HOL/Tools/function_package/fundef_common.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML Mon Dec 08 14:22:42 2008 +0100
@@ -82,7 +82,7 @@
psimps, pinducts, termination, defname}) phi =
let
val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
- val name = Name.name_of o Morphism.binding phi o Binding.name
+ val name = Binding.base_name o Morphism.binding phi o Binding.name
in
FundefCtxData { add_simps = add_simps, case_names = case_names,
fs = map term fs, R = term R, psimps = fact psimps,
--- a/src/HOL/Tools/function_package/fundef_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -96,8 +96,8 @@
fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
let
val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
- val fixes = map (apfst (apfst Name.name_of)) fixes0;
- val spec = map (apfst (apfst Name.name_of)) spec0;
+ val fixes = map (apfst (apfst Binding.base_name)) fixes0;
+ val spec = map (apfst (apfst Binding.base_name)) spec0;
val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
--- a/src/HOL/Tools/inductive_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -260,7 +260,7 @@
fun check_rule ctxt cs params ((binding, att), rule) =
let
- val name = Name.name_of binding;
+ val err_name = Binding.display binding;
val params' = Term.variant_frees rule (Logic.strip_params rule);
val frees = rev (map Free params');
val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
@@ -278,7 +278,7 @@
fun check_prem' prem t =
if head_of t mem cs then
- check_ind (err_in_prem ctxt name rule prem) t
+ check_ind (err_in_prem ctxt err_name rule prem) t
else (case t of
Abs (_, _, t) => check_prem' prem t
| t $ u => (check_prem' prem t; check_prem' prem u)
@@ -286,15 +286,15 @@
fun check_prem (prem, aprem) =
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
- else err_in_prem ctxt name rule prem "Non-atomic premise";
+ else err_in_prem ctxt err_name rule prem "Non-atomic premise";
in
(case concl of
Const ("Trueprop", _) $ t =>
if head_of t mem cs then
- (check_ind (err_in_rule ctxt name rule') t;
+ (check_ind (err_in_rule ctxt err_name rule') t;
List.app check_prem (prems ~~ aprems))
- else err_in_rule ctxt name rule' bad_concl
- | _ => err_in_rule ctxt name rule' bad_concl);
+ else err_in_rule ctxt err_name rule' bad_concl
+ | _ => err_in_rule ctxt err_name rule' bad_concl);
((binding, att), arule)
end;
@@ -638,7 +638,7 @@
val rec_name =
if Binding.is_empty alt_name then
- Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
else alt_name;
val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
@@ -671,9 +671,9 @@
fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
elims raw_induct ctxt =
let
- val rec_name = Name.name_of rec_binding;
+ val rec_name = Binding.base_name rec_binding;
val rec_qualified = Binding.qualify rec_name;
- val intr_names = map Name.name_of intr_bindings;
+ val intr_names = map Binding.base_name intr_bindings;
val ind_case_names = RuleCases.case_names intr_names;
val induct =
if coind then
@@ -730,11 +730,11 @@
cs intros monos params cnames_syn ctxt =
let
val _ = null cnames_syn andalso error "No inductive predicates given";
- val names = map (Name.name_of o fst) cnames_syn;
+ val names = map (Binding.base_name o fst) cnames_syn;
val _ = message (quiet_mode andalso not verbose)
("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
- val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn; (* FIXME *)
+ val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *)
val ((intr_names, intr_atts), intr_ts) =
apfst split_list (split_list (map (check_rule ctxt cs params) intros));
@@ -745,7 +745,7 @@
val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
params intr_ts rec_preds_defs ctxt1;
val elims = if no_elim then [] else
- prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
+ prove_elims quiet_mode cs params intr_ts (map Binding.base_name intr_names)
unfold rec_preds_defs ctxt1;
val raw_induct = zero_var_indexes
(if no_ind then Drule.asm_rl else
@@ -789,16 +789,16 @@
(* abbrevs *)
- val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
+ val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
fun get_abbrev ((name, atts), t) =
if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
let
- val _ = Name.name_of name = "" andalso null atts orelse
+ val _ = Binding.is_empty name andalso null atts orelse
error "Abbreviations may not have names or attributes";
val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
val var =
- (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
+ (case find_first (fn ((c, _), _) => Binding.base_name c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)
| SOME ((b, T'), mx) =>
if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
@@ -807,17 +807,17 @@
else NONE;
val abbrevs = map_filter get_abbrev spec;
- val bs = map (Name.name_of o fst o fst) abbrevs;
+ val bs = map (Binding.base_name o fst o fst) abbrevs;
(* predicates *)
val pre_intros = filter_out (is_some o get_abbrev) spec;
- val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
- val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
+ val cnames_syn' = filter_out (member (op =) bs o Binding.base_name o fst o fst) cnames_syn;
+ val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
val ps = map Free pnames;
- val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
+ val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
@@ -849,7 +849,7 @@
in
lthy
|> LocalTheory.set_group (serial_string ())
- |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
+ |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
end;
val add_inductive_i = gen_add_inductive_i add_ind_def;
@@ -857,7 +857,7 @@
fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
let
- val name = Sign.full_bname thy (Name.name_of (fst (fst (hd cnames_syn))));
+ val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
val ctxt' = thy
|> TheoryTarget.init NONE
|> LocalTheory.set_group group
@@ -945,11 +945,11 @@
fun flatten_specification specs = specs |> maps
(fn (a, (concl, [])) => concl |> map
(fn ((b, atts), [B]) =>
- if Name.name_of a = "" then ((b, atts), B)
- else if Name.name_of b = "" then ((a, atts), B)
+ if Binding.is_empty a then ((b, atts), B)
+ else if Binding.is_empty b then ((a, atts), B)
else error "Illegal nested case names"
| ((b, _), _) => error "Illegal simultaneous specification")
- | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
+ | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.base_name a)));
fun gen_ind_decl mk_def coind =
P.fixes -- P.for_fixes --
--- a/src/HOL/Tools/inductive_set_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -499,9 +499,9 @@
(* convert theorems to set notation *)
val rec_name =
if Binding.is_empty alt_name then
- Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+ Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
else alt_name;
- val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn; (* FIXME *)
+ val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn; (* FIXME *)
val (intr_names, intr_atts) = split_list (map fst intros);
val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
val (intrs', elims', induct, ctxt4) =
--- a/src/HOL/Tools/primrec_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -194,7 +194,7 @@
val def_name = Thm.def_name (Sign.base_name fname);
val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
val SOME var = get_first (fn ((b, _), mx) =>
- if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
+ if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
in (var, ((Binding.name def_name, []), rhs)) end;
@@ -231,7 +231,7 @@
let
val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
- orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
+ orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes) o snd) spec [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
val main_fns = map (fn (tname, {index, ...}) =>
@@ -298,7 +298,7 @@
P.name >> pair false) --| P.$$$ ")")) (false, "");
val old_primrec_decl =
- opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
+ opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
fun pipe_error t = P.!!! (Scan.fail_with (K
(cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
--- a/src/HOL/Tools/recdef_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/recdef_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -299,7 +299,7 @@
val recdef_decl =
Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
- P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+ P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
-- Scan.option hints
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
@@ -320,7 +320,7 @@
val _ =
OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
K.thy_goal
- ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
+ ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
--- a/src/HOL/Tools/record_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -346,19 +346,14 @@
val get_updates = Symtab.lookup o #updates o get_sel_upd;
fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
-fun put_sel_upd names simps thy =
- let
- val sels = map (rpair ()) names;
- val upds = map (suffix updateN) names ~~ names;
-
- val {records, sel_upd = {selectors, updates, simpset},
- equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
- val data = make_record_data records
- {selectors = Symtab.extend (selectors, sels),
- updates = Symtab.extend (updates, upds),
- simpset = Simplifier.addsimps (simpset, simps)}
- equalities extinjects extsplit splits extfields fieldext;
- in RecordsData.put data thy end;
+fun put_sel_upd names simps = RecordsData.map (fn {records,
+ sel_upd = {selectors, updates, simpset},
+ equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+ make_record_data records
+ {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
+ updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
+ simpset = Simplifier.addsimps (simpset, simps)}
+ equalities extinjects extsplit splits extfields fieldext);
(* access 'equalities' *)
--- a/src/HOL/Tools/refute.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/refute.ML Mon Dec 08 14:22:42 2008 +0100
@@ -313,18 +313,10 @@
(* (string * string) -> theory -> theory *)
- fun set_default_param (name, value) thy =
- let
- val {interpreters, printers, parameters} = RefuteData.get thy
- in
- RefuteData.put (case Symtab.lookup parameters name of
- NONE =>
+ fun set_default_param (name, value) = RefuteData.map
+ (fn {interpreters, printers, parameters} =>
{interpreters = interpreters, printers = printers,
- parameters = Symtab.extend (parameters, [(name, value)])}
- | SOME _ =>
- {interpreters = interpreters, printers = printers,
- parameters = Symtab.update (name, value) parameters}) thy
- end;
+ parameters = Symtab.update (name, value) parameters});
(* ------------------------------------------------------------------------- *)
(* get_default_param: retrieves the value associated with 'name' from *)
--- a/src/HOL/Tools/specification_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -233,7 +233,7 @@
val specification_decl =
P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+ Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
val _ =
OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -244,7 +244,7 @@
val ax_specification_decl =
P.name --
(P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
+ Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
val _ =
OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
--- a/src/HOLCF/Tools/fixrec_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -226,7 +226,7 @@
val lengths = map length blocks;
val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
- val names = map Name.name_of bindings;
+ val names = map Binding.base_name bindings;
val atts = map (map (prep_attrib thy)) srcss;
val eqn_ts = map (prep_prop thy) strings;
val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
@@ -278,7 +278,7 @@
val ts = map (prep_term thy) strings;
val simps = map (fix_pat thy) ts;
in
- (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
+ (snd o PureThy.add_thmss [((Binding.base_name name, simps), atts)]) thy
end;
val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
--- a/src/Pure/Concurrent/future.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Concurrent/future.ML Mon Dec 08 14:22:42 2008 +0100
@@ -36,6 +36,7 @@
val group_of: 'a future -> group
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
+ val value: 'a -> 'a future
val fork: (unit -> 'a) -> 'a future
val fork_group: group -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
@@ -84,6 +85,11 @@
fun peek (Future {result, ...}) = ! result;
fun is_finished x = is_some (peek x);
+fun value x = Future
+ {task = TaskQueue.new_task (),
+ group = TaskQueue.new_group (),
+ result = ref (SOME (Exn.Result x))};
+
(** scheduling **)
--- a/src/Pure/Concurrent/task_queue.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Mon Dec 08 14:22:42 2008 +0100
@@ -8,6 +8,7 @@
signature TASK_QUEUE =
sig
eqtype task
+ val new_task: unit -> task
val str_of_task: task -> string
eqtype group
val new_group: unit -> group
@@ -34,8 +35,11 @@
(* identifiers *)
datatype task = Task of serial;
+fun new_task () = Task (serial ());
+
fun str_of_task (Task i) = string_of_int i;
+
datatype group = Group of serial * bool ref;
fun new_group () = Group (serial (), ref true);
@@ -81,8 +85,7 @@
fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
let
- val id = serial ();
- val task = Task id;
+ val task as Task id = new_task ();
val groups' = Inttab.cons_list (gid, task) groups;
val jobs' = jobs
|> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;
--- a/src/Pure/General/binding.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/General/binding.ML Mon Dec 08 14:22:42 2008 +0100
@@ -23,6 +23,7 @@
val add_prefix: bool -> string -> T -> T
val map_prefix: ((string * bool) list -> T -> T) -> T -> T
val is_empty: T -> bool
+ val base_name: T -> string
val pos_of: T -> Position.T
val dest: T -> (string * bool) list * string
val display: T -> string
@@ -56,7 +57,7 @@
else path ^ "." ^ name;
val qualify = map_base o qualify_base;
- (*FIXME should all operations on bare names moved here from name_space.ML ?*)
+ (*FIXME should all operations on bare names move here from name_space.ML ?*)
fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
else (map_binding o apfst) (cons (prfx, sticky)) b;
@@ -65,6 +66,7 @@
f prefix (name_pos (name, pos));
fun is_empty (Binding ((_, name), _)) = name = "";
+fun base_name (Binding ((_, name), _)) = name;
fun pos_of (Binding (_, pos)) = pos;
fun dest (Binding (prefix_name, _)) = prefix_name;
--- a/src/Pure/General/name_space.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/General/name_space.ML Mon Dec 08 14:22:42 2008 +0100
@@ -48,7 +48,6 @@
-> 'a table * 'a table -> 'a table
val dest_table: 'a table -> (string * 'a) list
val extern_table: 'a table -> (xstring * 'a) list
- val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
end;
structure NameSpace: NAME_SPACE =
@@ -303,10 +302,6 @@
val (name, space') = declare naming b space;
in (name, (space', Symtab.update_new (name, x) tab)) end;
-fun extend_table naming bentries (space, tab) =
- let val entries = map (apfst (full_internal naming)) bentries
- in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
-
fun merge_tables eq ((space1, tab1), (space2, tab2)) =
(merge (space1, space2), Symtab.merge eq (tab1, tab2));
--- a/src/Pure/General/table.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/General/table.ML Mon Dec 08 14:22:42 2008 +0100
@@ -41,7 +41,6 @@
val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUP*)
- val extend: 'a table * (key * 'a) list -> 'a table (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
'a table * 'a table -> 'a table (*exception DUP*)
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*)
@@ -364,9 +363,7 @@
(* simultaneous modifications *)
-fun extend (table, args) = fold update_new args table;
-
-fun make entries = extend (empty, entries);
+fun make entries = fold update_new entries empty;
fun join f (table1, table2) =
let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
--- a/src/Pure/Isar/attrib.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Dec 08 14:22:42 2008 +0100
@@ -146,8 +146,8 @@
fun add_attributes raw_attrs thy =
let
val new_attrs =
- raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
- fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
+ raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
+ fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
in Attributes.map add thy end;
--- a/src/Pure/Isar/class.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/class.ML Mon Dec 08 14:22:42 2008 +0100
@@ -545,7 +545,7 @@
val constrain = Element.Constrains ((map o apsnd o map_atyps)
(K (TFree (Name.aT, base_sort))) supparams);
fun fork_syn (Element.Fixes xs) =
- fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
+ fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
#>> Element.Fixes
| fork_syn x = pair x;
fun fork_syntax elems =
--- a/src/Pure/Isar/constdefs.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/constdefs.ML Mon Dec 08 14:22:42 2008 +0100
@@ -38,7 +38,7 @@
val prop = prep_prop var_ctxt raw_prop;
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ =
- (case Option.map Name.name_of d of
+ (case Option.map Binding.base_name d of
NONE => ()
| SOME c' =>
if c <> c' then
@@ -46,7 +46,7 @@
else ());
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
- val name = Thm.def_name_optional c (Name.name_of raw_name);
+ val name = Thm.def_name_optional c (Binding.base_name raw_name);
val atts = map (prep_att thy) raw_atts;
val thy' =
--- a/src/Pure/Isar/element.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/element.ML Mon Dec 08 14:22:42 2008 +0100
@@ -113,7 +113,7 @@
fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
| Constrains xs => Constrains (xs |> map (fn (x, T) =>
- let val x' = Name.name_of (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
+ let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
| Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
| Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -136,7 +136,7 @@
(* logical content *)
fun params_of (Fixes fixes) = fixes |> map
- (fn (x, SOME T, _) => (Name.name_of x, T)
+ (fn (x, SOME T, _) => (Binding.base_name x, T)
| (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
| params_of _ = [];
@@ -182,8 +182,8 @@
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
fun prt_var (x, SOME T) = Pretty.block
- [Pretty.str (Name.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
- | prt_var (x, NONE) = Pretty.str (Name.name_of x);
+ [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
+ | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
val prt_vars = separate (Pretty.keyword "and") o map prt_var;
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
@@ -207,9 +207,9 @@
fun prt_mixfix NoSyn = []
| prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
- fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Name.name_of x ^ " ::") ::
+ fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") ::
Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
- | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
+ | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
Pretty.brk 1 :: prt_mixfix mx);
fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
@@ -395,7 +395,7 @@
fun rename_var ren (b, mx) =
let
- val x = Name.name_of b;
+ val x = Binding.base_name b;
val (x', mx') = rename_var_name ren (x, mx);
in (Binding.name x', mx') end;
--- a/src/Pure/Isar/expression.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/expression.ML Mon Dec 08 14:22:42 2008 +0100
@@ -132,8 +132,8 @@
if null dups then () else error (message ^ commas dups)
end;
- fun match_bind (n, b) = (n = Name.name_of b);
- fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
+ fun match_bind (n, b) = (n = Binding.base_name b);
+ fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
(* FIXME: cannot compare bindings for equality. *)
fun params_loc loc =
@@ -175,8 +175,8 @@
val (implicit, expr') = params_expr expr;
- val implicit' = map (#1 #> Name.name_of) implicit;
- val fixed' = map (#1 #> Name.name_of) fixed;
+ val implicit' = map (#1 #> Binding.base_name) implicit;
+ val fixed' = map (#1 #> Binding.base_name) fixed;
val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
val implicit'' = if strict then []
else let val _ = reject_dups
@@ -384,7 +384,7 @@
end;
fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
- let val x = Name.name_of binding
+ let val x = Binding.base_name binding
in (binding, AList.lookup (op =) parms x, mx) end) fixes)
| finish_primitive _ _ (Constrains _) = Constrains []
| finish_primitive _ close (Assumes asms) = close (Assumes asms)
@@ -395,7 +395,7 @@
let
val thy = ProofContext.theory_of ctxt;
val (parm_names, parm_types) = NewLocale.params_of thy loc |>
- map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
+ map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
val (asm, defs) = NewLocale.specification_of thy loc;
val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
val asm' = Option.map (Morphism.term morph) asm;
@@ -439,7 +439,7 @@
fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = NewLocale.params_of thy loc |>
- map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
+ map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
val inst' = parse_inst parm_names inst ctxt;
val parm_types' = map (TypeInfer.paramify_vars o
Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
@@ -472,7 +472,7 @@
val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
(* Retrieve parameter types *)
- val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
+ val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
_ => fn ps => ps) (Fixes fors :: elems) [];
val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt;
val parms = xs ~~ Ts; (* params from expression and elements *)
--- a/src/Pure/Isar/isar_cmd.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Mon Dec 08 14:22:42 2008 +0100
@@ -167,7 +167,7 @@
(* axioms *)
fun add_axms f args thy =
- f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+ f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
--- a/src/Pure/Isar/isar_syn.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Dec 08 14:22:42 2008 +0100
@@ -413,7 +413,7 @@
opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
>> (fn ((name, expr), insts) => Toplevel.print o
Toplevel.theory_to_proof
- (Locale.interpretation_cmd (Name.name_of name) expr insts)));
+ (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
val _ =
OuterSyntax.command "interpret"
@@ -422,7 +422,7 @@
(opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
>> (fn ((name, expr), insts) => Toplevel.print o
Toplevel.proof'
- (fn int => Locale.interpret_cmd (Name.name_of name) expr insts int)));
+ (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
(* classes *)
--- a/src/Pure/Isar/local_defs.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/local_defs.ML Mon Dec 08 14:22:42 2008 +0100
@@ -91,7 +91,7 @@
let
val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
- val xs = map Name.name_of bvars;
+ val xs = map Binding.base_name bvars;
val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
val eqs = mk_def ctxt (xs ~~ rhss);
val lhss = map (fst o Logic.dest_equals) eqs;
--- a/src/Pure/Isar/locale.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/locale.ML Mon Dec 08 14:22:42 2008 +0100
@@ -646,7 +646,7 @@
| unify _ env = env;
val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
val Vs = map (Option.map (Envir.norm_type unifier)) Us';
- val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
+ val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
in map (Option.map (Envir.norm_type unifier')) Vs end;
fun params_of elemss =
@@ -711,7 +711,7 @@
(Vartab.empty, maxidx);
val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
- val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
+ val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
fun inst_parms (i, ps) =
List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
@@ -1100,15 +1100,15 @@
*)
fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
- val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
+ val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
in
((ids',
merge_syntax ctxt ids'
- (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
+ (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
handle Symtab.DUP x => err_in_locale ctxt
("Conflicting syntax for parameter: " ^ quote x)
(map #1 ids')),
- [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
+ [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
end
| flatten _ ((ids, syn), Elem elem) =
((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
@@ -1252,7 +1252,7 @@
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
- let val x = Name.name_of b
+ let val x = Binding.base_name b
in (b, AList.lookup (op =) parms x, mx) end) fixes)
| finish_ext_elem parms _ (Constrains _, _) = Constrains []
| finish_ext_elem _ close (Assumes asms, propp) =
--- a/src/Pure/Isar/method.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/method.ML Mon Dec 08 14:22:42 2008 +0100
@@ -448,9 +448,9 @@
fun add_methods raw_meths thy =
let
val new_meths = raw_meths |> map (fn (name, f, comment) =>
- (name, ((f, comment), stamp ())));
+ (Binding.name name, ((f, comment), stamp ())));
- fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
+ fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
in Methods.map add thy end;
--- a/src/Pure/Isar/new_locale.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Mon Dec 08 14:22:42 2008 +0100
@@ -173,7 +173,7 @@
fun instance_of thy name morph =
params_of thy name |>
- map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
+ map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
fun specification_of thy name =
let
--- a/src/Pure/Isar/obtain.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Dec 08 14:22:42 2008 +0100
@@ -122,7 +122,7 @@
(*obtain vars*)
val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
- val xs = map (Name.name_of o #1) vars;
+ val xs = map (Binding.base_name o #1) vars;
(*obtain asms*)
val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -261,7 +261,7 @@
fun inferred_type (binding, _, mx) ctxt =
let
- val x = Name.name_of binding;
+ val x = Binding.base_name binding;
val (T, ctxt') = ProofContext.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
--- a/src/Pure/Isar/proof_context.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Dec 08 14:22:42 2008 +0100
@@ -1012,7 +1012,7 @@
fun prep_vars prep_typ internal =
fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
let
- val raw_x = Name.name_of raw_b;
+ val raw_x = Binding.base_name raw_b;
val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
val _ = Syntax.is_identifier (no_skolem internal x) orelse
error ("Illegal variable name: " ^ quote x);
@@ -1122,7 +1122,7 @@
fun gen_fixes prep raw_vars ctxt =
let
val (vars, _) = prep raw_vars ctxt;
- val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
+ val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
val ctxt'' =
ctxt'
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
--- a/src/Pure/Isar/specification.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/specification.ML Mon Dec 08 14:22:42 2008 +0100
@@ -153,7 +153,7 @@
fun gen_axioms do_print prep raw_vars raw_specs thy =
let
val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
- val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
+ val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
(*consts*)
val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -161,7 +161,7 @@
(*axioms*)
val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
- fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
+ fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
@@ -187,7 +187,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Name.name_of b;
+ val y = Binding.base_name b;
val _ = x = y orelse
error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -220,7 +220,7 @@
[] => (Binding.name x, NoSyn)
| [((b, _), mx)] =>
let
- val y = Name.name_of b;
+ val y = Binding.base_name b;
val _ = x = y orelse
error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
Position.str_of (Binding.pos_of b));
@@ -281,11 +281,11 @@
| Element.Obtains obtains =>
let
val case_names = obtains |> map_index (fn (i, (b, _)) =>
- let val name = Name.name_of b
+ let val name = Binding.base_name b
in if name = "" then string_of_int (i + 1) else name end);
val constraints = obtains |> map (fn (_, (vars, _)) =>
Element.Constrains
- (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
+ (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -295,7 +295,7 @@
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
val bs = map fst vars;
- val xs = map Name.name_of bs;
+ val xs = map Binding.base_name bs;
val props = map fst asms;
val (Ts, _) = ctxt'
|> fold Variable.declare_term props
--- a/src/Pure/Isar/theory_target.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML Mon Dec 08 14:22:42 2008 +0100
@@ -200,7 +200,7 @@
val similar_body = Type.similar_types (rhs, rhs');
(* FIXME workaround based on educated guess *)
val (prefix', _) = Binding.dest b';
- val class_global = Name.name_of b = Name.name_of b'
+ val class_global = Binding.base_name b = Binding.base_name b'
andalso not (null prefix')
andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
in
@@ -219,7 +219,7 @@
fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
let
- val c = Name.name_of b;
+ val c = Binding.base_name b;
val tags = LocalTheory.group_position_of lthy;
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
val U = map #2 xs ---> T;
@@ -252,7 +252,7 @@
fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
let
- val c = Name.name_of b;
+ val c = Binding.base_name b;
val tags = LocalTheory.group_position_of lthy;
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
val target_ctxt = LocalTheory.target_of lthy;
@@ -289,7 +289,7 @@
val thy = ProofContext.theory_of lthy;
val thy_ctxt = ProofContext.init thy;
- val c = Name.name_of b;
+ val c = Binding.base_name b;
val name' = Binding.map_base (Thm.def_name_optional c) name;
val (rhs', rhs_conv) =
LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
@@ -310,7 +310,7 @@
then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
val (global_def, lthy3) = lthy2
- |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
+ |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
val def = LocalDefs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
--- a/src/Pure/Isar/toplevel.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Dec 08 14:22:42 2008 +0100
@@ -744,7 +744,7 @@
val (future_results, end_state) = fold_map (proof_result immediate) input toplevel;
val _ =
(case end_state of
- State (NONE, SOME (Theory (Context.Theory thy, _), _)) => PureThy.force_proofs thy
+ State (NONE, SOME (Theory (Context.Theory _, _), _)) => ()
| _ => error "Unfinished development at end of input");
val results = maps Lazy.force future_results;
in (results, fn () => ignore (command (commit_exit end_pos) end_state)) end);
--- a/src/Pure/Syntax/syntax.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Syntax/syntax.ML Mon Dec 08 14:22:42 2008 +0100
@@ -173,7 +173,7 @@
fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
-fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
+fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
handle Symtab.DUP c => err_dup_trfun name c;
fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
--- a/src/Pure/Thy/thy_info.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Dec 08 14:22:42 2008 +0100
@@ -322,11 +322,22 @@
fun future (name, body) tab =
let
- val deps = map_filter (Symtab.lookup tab) (Graph.imm_preds task_graph name);
- val x = Future.fork_deps deps body;
+ val deps = Graph.imm_preds task_graph name
+ |> map_filter (fn parent =>
+ (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
+ fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
+
+ val x = Future.fork_deps (map #2 deps) (fn () =>
+ (case map_filter failed deps of
+ [] => body ()
+ | bad => error (loader_msg
+ ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+
in (x, Symtab.update (name, x) tab) end;
- val _ = ignore (Exn.release_all (Future.join_results (#1 (fold_map future tasks Symtab.empty))));
- in () end;
+
+ val thy_results = Future.join_results (#1 (fold_map future tasks Symtab.empty));
+ val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
+ in ignore (Exn.release_all (thy_results @ proof_results)) end;
local
--- a/src/Pure/Tools/invoke.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/Tools/invoke.ML Mon Dec 08 14:22:42 2008 +0100
@@ -120,7 +120,7 @@
(K.tag_proof K.prf_goal)
(SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
>> (fn ((((name, atts), expr), (insts, _)), fixes) =>
- Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
+ Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
end;
--- a/src/Pure/context.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/context.ML Mon Dec 08 14:22:42 2008 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/context.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generic theory contexts with unique identity, arbitrarily typed data,
@@ -392,14 +391,11 @@
fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
let
- val {name, version, intermediates} = history_of thy;
- val rs = map ((fn TheoryRef r => r) o check_thy) intermediates;
- val thy' as Theory ({self, id, ids, ...}, data', ancestry', _) = name_thy name thy;
- val identity' = make_identity self id ids Inttab.empty;
+ val {name, ...} = history_of thy;
+ val Theory (identity', data', ancestry', _) = name_thy name thy;
val history' = make_history name 0 [];
- val thy'' = vitalize (Theory (identity', data', ancestry', history'));
- val _ = List.app (fn r => r := thy'') rs;
- in thy'' end);
+ val thy' = vitalize (Theory (identity', data', ancestry', history'));
+ in thy' end);
(* theory data *)
--- a/src/Pure/name.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/name.ML Mon Dec 08 14:22:42 2008 +0100
@@ -27,8 +27,6 @@
val variants: string list -> context -> string list * context
val variant_list: string list -> string list -> string list
val variant: string list -> string -> string
-
- val name_of: Binding.T -> string (*FIMXE legacy*)
end;
structure Name: NAME =
@@ -140,9 +138,4 @@
fun variant_list used names = #1 (make_context used |> variants names);
fun variant used = singleton (variant_list used);
-
-(** generic name bindings -- legacy **)
-
-val name_of = snd o Binding.dest;
-
end;
--- a/src/Pure/pure_thy.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/pure_thy.ML Mon Dec 08 14:22:42 2008 +0100
@@ -11,7 +11,7 @@
val intern_fact: theory -> xstring -> string
val defined_fact: theory -> string -> bool
val hide_fact: bool -> string -> theory -> theory
- val force_proofs: theory -> unit
+ val join_proofs: theory list -> unit Exn.result list
val get_fact: Context.generic -> theory -> Facts.ref -> thm list
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
@@ -79,10 +79,9 @@
(* proofs *)
-fun lazy_proof thm = Lazy.lazy (fn () => Thm.force_proof thm);
+fun lazy_proof thm = Lazy.lazy (fn () => Thm.join_proof thm);
-fun force_proofs thy =
- ignore (Exn.release_all (map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy)))));
+val join_proofs = maps (fn thy => map (Exn.capture Lazy.force) (rev (#2 (FactsData.get thy))));
--- a/src/Pure/sign.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/sign.ML Mon Dec 08 14:22:42 2008 +0100
@@ -508,10 +508,10 @@
val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
fun prep (raw_b, raw_T, raw_mx) =
let
- val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
+ val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
val b = Binding.map_base (K mx_name) raw_b;
val c = full_name thy b;
- val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
+ val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
val T' = Logic.varifyT T;
--- a/src/Pure/theory.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/theory.ML Mon Dec 08 14:22:42 2008 +0100
@@ -178,8 +178,8 @@
fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
let
- val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
- val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
+ val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
+ val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
handle Symtab.DUP dup => err_dup_axm dup;
in axioms' end);
--- a/src/Pure/thm.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/Pure/thm.ML Mon Dec 08 14:22:42 2008 +0100
@@ -149,7 +149,7 @@
val future: thm future -> cterm -> thm
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
- val force_proof: thm -> unit
+ val join_proof: thm -> unit
val extern_oracles: theory -> xstring list
val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
@@ -346,7 +346,8 @@
tpairs: (term * term) list, (*flex-flex pairs*)
prop: term} (*conclusion*)
and deriv = Deriv of
- {all_promises: (serial * thm future) OrdList.T,
+ {max_promise: serial,
+ open_promises: (serial * thm future) OrdList.T,
promises: (serial * thm future) OrdList.T,
body: Pt.proof_body};
@@ -501,12 +502,11 @@
(** derivations **)
-fun make_deriv all_promises promises oracles thms proof =
- Deriv {all_promises = all_promises, promises = promises,
+fun make_deriv max_promise open_promises promises oracles thms proof =
+ Deriv {max_promise = max_promise, open_promises = open_promises, promises = promises,
body = PBody {oracles = oracles, thms = thms, proof = proof}};
-val closed_deriv = make_deriv [] [] [] [];
-val empty_deriv = closed_deriv Pt.MinProof;
+val empty_deriv = make_deriv ~1 [] [] [] [] Pt.MinProof;
(* inference rules *)
@@ -514,12 +514,13 @@
fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
fun deriv_rule2 f
- (Deriv {all_promises = all_ps1, promises = ps1,
+ (Deriv {max_promise = max1, open_promises = open_ps1, promises = ps1,
body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
- (Deriv {all_promises = all_ps2, promises = ps2,
+ (Deriv {max_promise = max2, open_promises = open_ps2, promises = ps2,
body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
let
- val all_ps = OrdList.union promise_ord all_ps1 all_ps2;
+ val max = Int.max (max1, max2);
+ val open_ps = OrdList.union promise_ord open_ps1 open_ps2;
val ps = OrdList.union promise_ord ps1 ps2;
val oras = Pt.merge_oracles oras1 oras2;
val thms = Pt.merge_thms thms1 thms2;
@@ -529,10 +530,10 @@
| 1 => MinProof
| 0 => MinProof
| i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
- in make_deriv all_ps ps oras thms prf end;
+ in make_deriv max open_ps ps oras thms prf end;
fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
-fun deriv_rule0 prf = deriv_rule1 I (closed_deriv prf);
+fun deriv_rule0 prf = deriv_rule1 I (make_deriv ~1 [] [] [] [] prf);
@@ -1597,12 +1598,12 @@
val _ = Theory.check_thy orig_thy;
fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
- val Thm (Deriv {all_promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
+ val Thm (Deriv {max_promise, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
val _ = prop aconv orig_prop orelse err "bad prop";
val _ = null tpairs orelse err "bad tpairs";
val _ = null hyps orelse err "bad hyps";
val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
- val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
+ val _ = max_promise < i orelse err "bad dependencies";
in thm end;
fun future future_thm ct =
@@ -1615,7 +1616,7 @@
val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
val promise = (i, future);
in
- Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
+ Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),
{thy_ref = thy_ref,
tags = [],
maxidx = maxidx,
@@ -1630,14 +1631,14 @@
fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
-fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
+fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
let
- val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
+ val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
val ps = map (apsnd (raw_proof_of o Future.join)) promises;
in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
val proof_of = Proofterm.proof_of o proof_body_of;
-val force_proof = ignore o proof_body_of;
+val join_proof = ignore o proof_body_of;
(* closed derivations with official name *)
@@ -1647,14 +1648,17 @@
fun put_name name (thm as Thm (der, args)) =
let
- val Deriv {promises, body, ...} = der;
+ val Deriv {max_promise, open_promises, promises, body, ...} = der;
val {thy_ref, hyps, prop, tpairs, ...} = args;
- val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
+ val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
val thy = Theory.deref thy_ref;
val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
- val der' = make_deriv [] [] [] [pthm] proof;
+
+ val open_promises' = open_promises |> filter (fn (_, p) =>
+ (case Future.peek p of SOME (Exn.Result _) => false | _ => true));
+ val der' = make_deriv max_promise open_promises' [] [] [pthm] proof;
val _ = Theory.check_thy thy;
in Thm (der', args) end;
@@ -1670,7 +1674,7 @@
raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
else
let val prf = Pt.oracle_proof name prop in
- Thm (make_deriv [] [] (Pt.make_oracles prf) [] prf,
+ Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
{thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
tags = [],
maxidx = maxidx,
--- a/src/ZF/Tools/inductive_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -67,7 +67,7 @@
val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
val ctxt = ProofContext.init thy;
- val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs;
+ val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
val case_names = RuleCases.case_names intr_names;
--- a/src/ZF/Tools/primrec_package.ML Mon Dec 08 14:18:29 2008 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Dec 08 14:22:42 2008 +0100
@@ -180,7 +180,7 @@
val (eqn_thms', thy2) =
thy1
- |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
+ |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
val (_, thy3) =
thy2
|> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]