326 Written with naive application, an addition of constant |
326 Written with naive application, an addition of constant |
327 @{text bar} with type @{typ "foo \<Rightarrow> foo"} and |
327 @{text bar} with type @{typ "foo \<Rightarrow> foo"} and |
328 a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like: |
328 a corresponding definition @{term "bar \<equiv> \<lambda>x. x"} would look like: |
329 |
329 |
330 \begin{quotation} |
330 \begin{quotation} |
331 @{ML "(fn (t, thy) => Thm.add_def false |
331 @{ML "(fn (t, thy) => Thm.add_def false |
332 (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy) |
332 (\"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy) |
333 (Sign.declare_const [] |
333 (Sign.declare_const [] |
334 (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"}. |
334 (\"bar\", @{typ \"foo => foo\"}, NoSyn) thy)"} |
335 \end{quotation} |
335 \end{quotation} |
336 |
336 |
337 With increasing numbers of applications, this code gets quite |
337 With increasing numbers of applications, this code gets quite |
338 unreadable. Further, it is unintuitive that things are |
338 unreadable. Further, it is unintuitive that things are |
339 written down in the opposite order as they actually ``happen''. |
339 written down in the opposite order as they actually ``happen''. |
340 *} |
340 *} |
341 |
|
342 (*<*) |
|
343 ML {* |
|
344 val thy = Theory.copy @{theory} |
|
345 *} |
|
346 (*>*) |
|
347 |
341 |
348 text {* |
342 text {* |
349 \noindent At this stage, Isabelle offers some combinators which allow |
343 \noindent At this stage, Isabelle offers some combinators which allow |
350 for more convenient notation, most notably reverse application: |
344 for more convenient notation, most notably reverse application: |
351 \begin{quotation} |
345 \begin{quotation} |
420 |
414 |
421 text {* |
415 text {* |
422 \noindent This principles naturally lift to @{text lists} using |
416 \noindent This principles naturally lift to @{text lists} using |
423 the @{ML fold} and @{ML fold_map} combinators. |
417 the @{ML fold} and @{ML fold_map} combinators. |
424 The first lifts a single function |
418 The first lifts a single function |
425 @{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"} |
419 \[ |
|
420 \mbox{@{text "f \<Colon> 'a -> 'b -> 'b"} to @{text "'a list -> 'b -> 'b"}} |
|
421 \] |
426 such that |
422 such that |
427 @{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"}; |
423 \[ |
428 the second accumulates side results in a list by lifting |
424 \mbox{@{text "y |> fold f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 |> f x\<^isub>2 |> \<dots> |> f x\<^isub>n"}} |
|
425 \] |
|
426 The second accumulates side results in a list by lifting |
429 a single function |
427 a single function |
430 @{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"} |
428 \[ |
|
429 \mbox{@{text "f \<Colon> 'a -> 'b -> 'c \<times> 'b"} to @{text "'a list -> 'b -> 'c list \<times> 'b"}} |
|
430 \] |
431 such that |
431 such that |
432 @{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv> y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \<dots> ||>> f x\<^isub>n |
432 \[ |
433 ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"}; |
433 \mbox{@{text "y |> fold_map f [x\<^isub>1, x\<^isub>2, \<dots> x\<^isub>n] \<equiv>"}} \\ |
434 |
434 ~~\mbox{@{text "y |> f x\<^isub>1 ||>> f x\<^isub>2 ||>> \<dots> ||>> f x\<^isub>n ||> (fn ((z\<^isub>1, z\<^isub>2), \<dots> z\<^isub>n) => [z\<^isub>1, z\<^isub>2, \<dots> z\<^isub>n])"}} |
435 Example: FIXME |
435 \] |
436 \begin{quotation} |
436 |
|
437 Example: |
|
438 \begin{quotation} |
|
439 @{ML "let |
|
440 val consts = [\"foo\", \"bar\"]; |
|
441 in |
|
442 thy |
|
443 |> fold_map (fn const => Sign.declare_const [] |
|
444 (const, @{typ \"foo => foo\"}, NoSyn)) consts |
|
445 |>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"})) |
|
446 |-> (fn defs => fold_map (fn def => |
|
447 Thm.add_def false (\"\", def)) defs) |
|
448 end |
|
449 "} |
437 \end{quotation} |
450 \end{quotation} |
438 *} |
451 *} |
439 |
452 |
440 text %mlref {* |
453 text %mlref {* |
441 \begin{mldecls} |
454 \begin{mldecls} |
459 @{index_ML tap: "('b -> 'a) -> 'b -> 'b"} \\ |
472 @{index_ML tap: "('b -> 'a) -> 'b -> 'b"} \\ |
460 \end{mldecls} |
473 \end{mldecls} |
461 *} |
474 *} |
462 |
475 |
463 text {* |
476 text {* |
464 \noindent FIXME |
477 \noindent These operators allow to ``query'' a context |
|
478 in a series of context transformations: |
|
479 |
|
480 \begin{quotation} |
|
481 @{ML "thy |
|
482 |> tap (fn _ => writeln \"now adding constant\") |
|
483 |> Sign.declare_const [] (\"bar\", @{typ \"foo => foo\"}, NoSyn) |
|
484 ||>> `(fn thy => Sign.declared_const thy |
|
485 (Sign.full_name thy \"foobar\")) |
|
486 |-> (fn (t, b) => if b then I |
|
487 else Sign.declare_const [] |
|
488 (\"foobar\", @{typ \"foo => foo\"}, NoSyn) #> snd) |
|
489 "} |
|
490 \end{quotation} |
465 *} |
491 *} |
466 |
492 |
467 section {* Options and partiality *} |
493 section {* Options and partiality *} |
468 |
494 |
469 text %mlref {* |
495 text %mlref {* |