131 in a theory is that the code can contain references to entities defined |
131 in a theory is that the code can contain references to entities defined |
132 on the logical level of Isabelle. This is done using antiquotations. |
132 on the logical level of Isabelle. This is done using antiquotations. |
133 For example, one can print out the name of |
133 For example, one can print out the name of |
134 the current theory by typing |
134 the current theory by typing |
135 |
135 |
136 @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps : string"} |
136 @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"} |
137 |
137 |
138 where @{text "@{theory}"} is an antiquotation that is substituted with the |
138 where @{text "@{theory}"} is an antiquotation that is substituted with the |
139 current theory (remember that we assumed we are inside the theory CookBook). |
139 current theory (remember that we assumed we are inside the theory CookBook). |
140 The name of this theory can be extracted using the function |
140 The name of this theory can be extracted using the function |
141 @{ML "Context.theory_name"}. |
141 @{ML "Context.theory_name"}. |
355 |
354 |
356 Type checking is always relative to a theory context. For now we can use |
355 Type checking is always relative to a theory context. For now we can use |
357 the @{ML "@{theory}"} antiquotation to get hold of the current theory. |
356 the @{ML "@{theory}"} antiquotation to get hold of the current theory. |
358 For example we can write: |
357 For example we can write: |
359 |
358 |
360 (FIXME ML-response-unchecked needed) |
359 @{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"} |
361 |
|
362 @{ML [display] "@{term \"(a::nat) + b = c\"}"} |
|
363 |
360 |
364 and |
361 and |
365 |
362 |
366 @{ML [display] |
363 @{ML_response_fake [display] |
367 "let |
364 "let |
368 val natT = @{typ \"nat\"} |
365 val natT = @{typ \"nat\"} |
369 val zero = @{term \"0::nat\"} |
366 val zero = @{term \"0::nat\"} |
370 in |
367 in |
371 cterm_of @{theory} |
368 cterm_of @{theory} |
372 (Const (@{const_name plus}, natT --> natT --> natT) |
369 (Const (@{const_name plus}, natT --> natT --> natT) |
373 $ zero $ zero) |
370 $ zero $ zero) |
374 end"} |
371 end" "0 + 0"} |
375 |
372 |
376 \begin{exercise} |
373 \begin{exercise} |
377 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
374 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
378 result that type checks. |
375 result that type checks. |
379 \end{exercise} |
376 \end{exercise} |
557 |
554 |
558 section {* Storing Theorems *} |
555 section {* Storing Theorems *} |
559 |
556 |
560 section {* Theorem Attributes *} |
557 section {* Theorem Attributes *} |
561 |
558 |
562 ML {* |
|
563 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
|
564 |
|
565 fun ml_val ys txt = "fn " ^ |
|
566 (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ |
|
567 " => (" ^ txt ^ ");"; |
|
568 |
|
569 fun ml_val_open (ys, []) txt = ml_val ys txt |
|
570 | ml_val_open (ys, xs) txt = |
|
571 ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); |
|
572 |
|
573 fun ml_pat (rhs, pat) = |
|
574 let val pat' = implode (map (fn "\<dots>" => "_" | s => s) |
|
575 (Symbol.explode pat)) |
|
576 in |
|
577 "val " ^ pat' ^ " = " ^ rhs |
|
578 end; |
|
579 |
|
580 (* modified from original *) |
|
581 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
|
582 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"; |
|
583 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
|
584 |
|
585 *} |
|
586 |
|
587 ML {* ml_pat *} |
|
588 ML {* K ml_pat *} |
|
589 |
|
590 ML {* |
|
591 fun output_verbatim ml src ctxt (txt, pos) = |
|
592 let val txt = ml ctxt (txt, pos) |
|
593 in |
|
594 (if ! ThyOutput.source then str_of_source src else txt) |
|
595 |> (if ! ThyOutput.quotes then quote else I) |
|
596 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt |
|
597 end; |
|
598 *} |
|
599 |
|
600 ML {* |
|
601 fun output_ml ml = output_verbatim |
|
602 (fn ctxt => fn ((txt, p), pos) => |
|
603 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
|
604 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
|
605 Chunks.transform_cmts |> implode)); |
|
606 *} |
|
607 |
|
608 ML {* |
|
609 fun output_ml_checked ml src ctxt (txt, pos) = |
|
610 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
|
611 (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) |
|
612 |> (if ! ThyOutput.quotes then quote else I) |
|
613 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) |
|
614 |
|
615 *} |
|
616 |
559 |
617 |
560 |
618 |
561 |
619 end |
562 end |