# HG changeset patch # User ballarin # Date 1228742562 -3600 # Node ID 3e95d28114a1ffe29a856e6c3dd1e182a9d8e483 # Parent 8e7d6f959bd74a57d486f2f009f25f1fe29720e7# Parent 9a1eaad4a7bb3d3d294adc85ff273a97257718a4 Merged. diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarAdvanced/Classes/classes.tex --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarAdvanced/Classes/style.sty --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarAdvanced/Codegen/codegen.tex --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarAdvanced/Codegen/style.sty --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarImplementation/Thy/ML.thy --- 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} *} diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarImplementation/Thy/document/ML.tex --- 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}% diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarImplementation/Thy/document/logic.tex --- 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| \\ diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarImplementation/Thy/document/prelim.tex --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarImplementation/Thy/logic.thy --- 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"} \\ diff -r 8e7d6f959bd7 -r 3e95d28114a1 doc-src/IsarImplementation/Thy/prelim.thy --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 etc/settings --- 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" diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Arith_Tools.thy --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Library/Nat_Infinity.thy --- 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 \ inat) + number_of l = (if neg (number_of k \ int) then number_of l - else if neg (number_of l \ int) then number_of k else number_of (k + l))" + "(number_of k \ 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 \ \ if n = 0 then 0 else \ | Fin m \ + (case n of \ \ if m = 0 then 0 else \ | Fin n \ Fin (m * n)))" + +lemma times_inat_simps [simp, code]: + "Fin m * Fin n = Fin (m * n)" + "\ * \ = \" + "\ * Fin n = (if n = 0 then 0 else \)" + "Fin m * \ = (if m = 0 then 0 else \)" + 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) \ 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 \ b" and "0 \ c" + thus "c * a \ 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 \ inat) \ number_of n \ (number_of m \ nat) \ number_of n" "(number_of m \ inat) < number_of n \ (number_of m \ nat) < number_of n" diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/NatBin.thy --- 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' \ + (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) \ number_of v' \ + (if v \ v' then True else v \ 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\0"} and @{term "0\n"}.*} lemma eq_number_of_0 [simp]: - "number_of v = (0::nat) \ number_of v \ (0::int)" - unfolding nat_number_of_def number_of_is_id by auto + "number_of v = (0::nat) \ v \ 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 \ number_of v \ (0::int)" + "(0::nat) = number_of v \ v \ 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 \ 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Nominal/nominal_primrec.ML --- 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)) => diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/ROOT.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/ComputeNumeral.thy --- 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 \ lezero y) \ (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) \ (\ (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) \ (number_of y)) = (y < x \ lezero x)" by (auto simp add: number_of_is_id lezero_def nat_number_of_def) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/function_package/fundef_common.ML --- 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, diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/function_package/fundef_package.ML --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/inductive_package.ML --- 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 -- diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/inductive_set_package.ML --- 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) = diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/primrec_package.ML --- 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]))); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/recdef_package.ML --- 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)); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/record_package.ML --- 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' *) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/refute.ML --- 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 *) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOL/Tools/specification_package.ML --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/HOLCF/Tools/fixrec_package.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Concurrent/future.ML --- 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 **) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Concurrent/task_queue.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/General/binding.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/General/name_space.ML --- 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)); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/General/table.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/attrib.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/class.ML --- 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 = diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/constdefs.ML --- 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' = diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/element.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/expression.ML --- 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 *) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/isar_cmd.ML --- 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); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/isar_syn.ML --- 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 *) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/local_defs.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/locale.ML --- 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) = diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/method.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/new_locale.ML --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/obtain.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/proof_context.ML --- 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) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/specification.ML --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/theory_target.ML --- 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, diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Isar/toplevel.ML --- 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); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Syntax/syntax.ML --- 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) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Thy/thy_info.ML --- 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 diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/Tools/invoke.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/context.ML --- 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 *) diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/name.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/pure_thy.ML --- 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)))); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/sign.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/theory.ML --- 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); diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/Pure/thm.ML --- 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, diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/ZF/Tools/inductive_package.ML --- 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; diff -r 8e7d6f959bd7 -r 3e95d28114a1 src/ZF/Tools/primrec_package.ML --- 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])]