# HG changeset patch # User haftmann # Date 1193313118 -7200 # Node ID 762ed22d15c737b60698853c0f22d25c2b7e57cc # Parent 712ab7bd95121da9d4cbf0abd8465a24be82be8f continued diff -r 712ab7bd9512 -r 762ed22d15c7 doc-src/IsarImplementation/Thy/ML.thy --- a/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 25 10:24:32 2007 +0200 +++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 25 13:51:58 2007 +0200 @@ -328,10 +328,10 @@ a corresponding definition @{term "bar \ \x. x"} would look like: \begin{quotation} - @{ML "(fn (t, thy) => Thm.add_def false + @{ML "(fn (t, thy) => Thm.add_def false (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy) (Sign.declare_const [] - (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}. + (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"} \end{quotation} With increasing numbers of applications, this code gets quite @@ -339,12 +339,6 @@ written down in the opposite order as they actually ``happen''. *} -(*<*) -ML {* -val thy = Theory.copy @{theory} -*} -(*>*) - text {* \noindent At this stage, Isabelle offers some combinators which allow for more convenient notation, most notably reverse application: @@ -422,18 +416,37 @@ \noindent This principles naturally lift to @{text lists} using the @{ML fold} and @{ML fold_map} combinators. The first lifts a single function - @{text "f \ 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"} + \[ + \mbox{@{text "f \ 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}} + \] such that - @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \ y |> f x\<^isub>1 |> f x\<^isub>2 |> \ |> f x\<^isub>n"}; - the second accumulates side results in a list by lifting + \[ + \mbox{@{text "y |> fold f [x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \ y |> f x\<^isub>1 |> f x\<^isub>2 |> \ |> f x\<^isub>n"}} + \] + The second accumulates side results in a list by lifting a single function - @{text "f \ 'a -> 'b -> 'c \ 'b"} to @{text "'a list -> 'b -> 'c list \ 'b"} + \[ + \mbox{@{text "f \ 'a -> 'b -> 'c \ 'b"} to @{text "'a list -> 'b -> 'c list \ 'b"}} + \] such that - @{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \ y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \ ||>> f x\<^isub>n - ||> (fn ((z\<^isub>1, z\<^isub>2), \ z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \ z\<^isub>n])"}; - - Example: FIXME + \[ + \mbox{@{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \ x\<^isub>n] \"}} \\ + ~~\mbox{@{text "y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \ ||>> f x\<^isub>n ||> (fn ((z\<^isub>1, z\<^isub>2), \ z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \ z\<^isub>n])"}} + \] + + Example: \begin{quotation} +@{ML "let + val consts = [\"foo\", \"bar\"]; +in + thy + |> fold_map (fn const => Sign.declare_const [] + (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 (\"\", def)) defs) +end +"} \end{quotation} *} @@ -461,7 +474,20 @@ *} text {* - \noindent FIXME + \noindent These operators allow to ``query'' a context + in a series of context transformations: + + \begin{quotation} +@{ML "thy +|> tap (fn _ => writeln \"now adding constant\") +|> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn) +||>> `(fn thy => Sign.declared_const thy + (Sign.full_name thy \"foobar\")) +|-> (fn (t, b) => if b then I + else Sign.declare_const [] + (\"foobar\", @{typ \"foo => foo\"}, NoSyn) #> snd) +"} + \end{quotation} *} section {* Options and partiality *} diff -r 712ab7bd9512 -r 762ed22d15c7 doc-src/IsarImplementation/Thy/document/ML.tex --- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 25 10:24:32 2007 +0200 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 25 13:51:58 2007 +0200 @@ -384,10 +384,10 @@ a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like: \begin{quotation} - \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline% + \verb|(fn (t, thy) => Thm.add_def false|\isasep\isanewline% \verb| ("bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline% \verb| (Sign.declare_const []|\isasep\isanewline% -\verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)|. +\verb| ("bar", @{typ "foo => foo"}, NoSyn) thy)| \end{quotation} With increasing numbers of applications, this code gets quite @@ -396,19 +396,6 @@ \end{isamarkuptext}% \isamarkuptrue% % -\isadelimML -% -\endisadelimML -% -\isatagML -% -\endisatagML -{\isafoldML}% -% -\isadelimML -% -\endisadelimML -% \begin{isamarkuptext}% \noindent At this stage, Isabelle offers some combinators which allow for more convenient notation, most notably reverse application: @@ -516,17 +503,37 @@ \noindent This principles naturally lift to \isa{lists} using the \verb|fold| and \verb|fold_map| combinators. The first lifts a single function - \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} + \[ + \mbox{\isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}b}} + \] such that - \isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}; - the second accumulates side results in a list by lifting + \[ + \mbox{\isa{y\ {\isacharbar}{\isachargreater}\ fold\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub n}} + \] + The second accumulates side results in a list by lifting a single function - \isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b} + \[ + \mbox{\isa{f\ {\isasymColon}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b} to \isa{{\isacharprime}a\ list\ {\isacharminus}{\isachargreater}\ {\isacharprime}b\ {\isacharminus}{\isachargreater}\ {\isacharprime}c\ list\ {\isasymtimes}\ {\isacharprime}b}} + \] such that - \isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}\ y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}}; + \[ + \mbox{\isa{y\ {\isacharbar}{\isachargreater}\ fold{\isacharunderscore}map\ f\ {\isacharbrackleft}x\isactrlisub {\isadigit{1}}{\isacharcomma}\ x\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ x\isactrlisub n{\isacharbrackright}\ {\isasymequiv}}} \\ + ~~\mbox{\isa{y\ {\isacharbar}{\isachargreater}\ f\ x\isactrlisub {\isadigit{1}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub {\isadigit{2}}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isacharbar}{\isachargreater}{\isachargreater}\ f\ x\isactrlisub n\ {\isacharbar}{\isacharbar}{\isachargreater}\ {\isacharparenleft}fn\ {\isacharparenleft}{\isacharparenleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharparenright}\ {\isacharequal}{\isachargreater}\ {\isacharbrackleft}z\isactrlisub {\isadigit{1}}{\isacharcomma}\ z\isactrlisub {\isadigit{2}}{\isacharcomma}\ {\isasymdots}\ z\isactrlisub n{\isacharbrackright}{\isacharparenright}}} + \] + + Example: + \begin{quotation} +\verb|let|\isasep\isanewline% +\verb| val consts = ["foo", "bar"];|\isasep\isanewline% +\verb|in|\isasep\isanewline% +\verb| thy|\isasep\isanewline% +\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline% +\verb| (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 ("", def)) defs)|\isasep\isanewline% +\verb|end|\isasep\isanewline% - Example: FIXME - \begin{quotation} \end{quotation}% \end{isamarkuptext}% \isamarkuptrue% @@ -584,7 +591,20 @@ \endisadelimmlref % \begin{isamarkuptext}% -\noindent FIXME% +\noindent These operators allow to ``query'' a context + in a series of context transformations: + + \begin{quotation} +\verb|thy|\isasep\isanewline% +\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline% +\verb||\verb,|,\verb|> Sign.declare_const [] ("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||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline% +\verb| else Sign.declare_const []|\isasep\isanewline% +\verb| ("foobar", @{typ "foo => foo"}, NoSyn) #> snd)|\isasep\isanewline% + + \end{quotation}% \end{isamarkuptext}% \isamarkuptrue% %