added ML* plus updated the RefMan accordingly.
This commit is contained in:
parent
c2e39edd99
commit
01c196086b
|
|
@ -70,13 +70,20 @@ declare_reference*["fig:dependency"::text_section]
|
|||
|
||||
|
||||
text\<open>
|
||||
We assume a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files) that can depend acyclically on each other.
|
||||
The Isabelle Framework is based on a \<^emph>\<open>document-centric view\<close> bindex>\<open>document-centric view\<close> of
|
||||
a document, treating the input in its integrality as set of (user-programmable) \<^emph>\<open>document element\<close>
|
||||
that may mutually depend and link to each other; A \<^emph>\<open>document\<close> in our sense is what is configured in a set of
|
||||
\<^verbatim>\<open>ROOT\<close>- and \<^verbatim>\<open>ROOTS\<close>-files.
|
||||
|
||||
Isabelle assumes a hierarchical document model\<^index>\<open>document model\<close>, \<^ie>, an \<^emph>\<open>integrated\<close> document
|
||||
consist of a hierarchy \<^emph>\<open>sub-documents\<close> (files); dependencies are restricted to be
|
||||
acyclic at this level.
|
||||
Sub-documents can have different document types in order to capture documentations consisting of
|
||||
documentation, models, proofs, code of various forms and other technical artifacts. We call the
|
||||
main sub-document type, for historical reasons, \<^emph>\<open>theory\<close>-files. A theory file\<^bindex>\<open>theory!file\<close>
|
||||
consists of a \<^emph>\<open>header\<close>\<^bindex>\<open>header\<close>, a \<^emph>\<open>context definition\<close>\<^index>\<open>context\<close>, and a body
|
||||
consisting of a sequence of \<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||
consisting of a sequence of document elements called
|
||||
\<^emph>\<open>command\<close>s (see @{figure (unchecked) "fig:dependency"}). Even
|
||||
the header consists of a sequence of commands used for introductory text elements not depending on
|
||||
any context. The context-definition contains an \<^boxed_theory_text>\<open>import\<close> and a
|
||||
\<^boxed_theory_text>\<open>keyword\<close> section, for example:
|
||||
|
|
@ -96,30 +103,43 @@ text\<open> A text-element \<^index>\<open>text-element\<close> may look like th
|
|||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl},
|
||||
we obtain in \<Gamma> for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>}
|
||||
so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
... so it is a command \<^theory_text>\<open>text\<close> followed by an argument (here in \<open>\<open> ... \<close>\<close> paranthesis) which
|
||||
contains characters and and a special notation for semantic macros \<^bindex>\<open>semantic macros\<close>
|
||||
(here \<^theory_text>\<open>@{term "fac 5"}).\<close>
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
We distinguish fundamentally two different syntactic levels:
|
||||
\<^item> the \<^emph>\<open>outer-syntax\<close>\<^bindex>\<open>syntax!outer\<close>\<^index>\<open>outer syntax|see {syntax, outer}\<close> (\<^ie>, the
|
||||
syntax for commands) is processed by a lexer-library and parser combinators built on top, and
|
||||
\<^item> the \<^emph>\<open>inner-syntax\<close>\<^bindex>\<open>syntax!inner\<close>\<^index>\<open>inner syntax|see {syntax, inner}\<close> (\<^ie>, the
|
||||
syntax for \<open>\<lambda>\<close>-terms in HOL) with its own parametric polymorphism type checking.
|
||||
text\<open>While we concentrate in this manual on \<^theory_text>\<open>text\<close>-document elements --- this is the main
|
||||
use of \<^dof> in its current stage --- it is important to note that there are actually three
|
||||
families of ``ontology aware'' document elements with analogous
|
||||
syntax to standard ones. The difference is a bracket with meta-data of the form:
|
||||
@{theory_text [display,indent=5, margin=70]
|
||||
\<open>
|
||||
text*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some semi-formal text \<close>
|
||||
ML*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some SML code \<close>
|
||||
value*[label::classid, attr\<^sub>1=E\<^sub>1, ... attr\<^sub>n=E\<^sub>n]\<open> some annotated \<lambda>-term \<close>
|
||||
\<close>}
|
||||
|
||||
Depending on the family, we will speak about \<^emph>\<open>(formal) text-contexts\<close>,\<^index>\<open>formal text-contexts\<close>
|
||||
\<^emph>\<open>(ML) code-contexts\<close>\<^index>\<open>code-contexts\<close> and \<^emph>\<open>term-contexts\<close>\<^index>\<open>term-contexts\<close> if we refer
|
||||
to sub-elements inside the \<open>\<open>...\<close>\<close> cartouches of these command families. Note that the Isabelle
|
||||
framework allows for nesting cartouches that permits to support to switch into a different
|
||||
context. In general, this has also the effect that the evaluation of antiquotations changes.
|
||||
\<^footnote>\<open>In the literature, this concept has been referred to \<open>Cascade-Syntax\<close> and was used in the
|
||||
Centaur-system and is existing in some limited form in some Emacs-implementations these days. \<close>
|
||||
\<close>
|
||||
text\<open>
|
||||
On the semantic level, we assume a validation process for an integrated document, where the
|
||||
semantics of a command is a transformation \<open>\<theta> \<rightarrow> \<theta>\<close> for some system state \<open>\<theta>\<close>.
|
||||
This document model can be instantiated with outer-syntax commands for common
|
||||
text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>.
|
||||
Thus, users can add informal text to a sub-document using a text command:
|
||||
This document model can be instantiated depending on the text-code-, or term-contexts.
|
||||
For common text elements, \<^eg>, \<^theory_text>\<open>section\<open>...\<close>\<close> or \<^theory_text>\<open>text\<open>...\<close>\<close>,
|
||||
users can add informal text to a sub-document using a text command:
|
||||
@{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
|
||||
This will type-set the corresponding text in, for example, a PDF document. However, this
|
||||
translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>,
|
||||
machine-checked content via \<^emph>\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm refl}, we obtain in \<Gamma>
|
||||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
|
||||
\<open>text\<open> According to the \<^emph>\<open>reflexivity\<close> axiom @{thm "refl"}, we obtain in \<Gamma>
|
||||
for @{term \<open>fac 5\<close>} the result @{value \<open>fac 5\<close>}.\<close>\<close>
|
||||
}
|
||||
which is represented in the final document (\<^eg>, a PDF) by:
|
||||
@{boxed_pdf [display]
|
||||
|
|
@ -137,10 +157,12 @@ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\<cl
|
|||
typeset. They represent the device for linking the formal with the informal.
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
figure*["fig:dependency"::figure,relative_width="70",src="''figures/document-hierarchy''"]
|
||||
\<open>A Theory-Graph in the Document Model. \<close>
|
||||
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Required Document Model\<close>
|
||||
section*[bgrnd21::introduction]\<open>Implementability of the Document Model in other ITP's\<close>
|
||||
text\<open>
|
||||
Batch-mode checkers for \<^dof> can be implemented in all systems of the LCF-style prover family,
|
||||
\<^ie>, systems with a type-checked \<open>term\<close>, and abstract \<open>thm\<close>-type for theorems
|
||||
|
|
|
|||
|
|
@ -100,7 +100,8 @@ text\<open>
|
|||
to instances, and class-invariants. Some concepts like advanced type-checking, referencing to
|
||||
formal entities of Isabelle, and monitors are due to its specific application in the
|
||||
Isabelle context. Conceptually, ontologies specified in ODL consist of:
|
||||
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) that describe concepts;
|
||||
\<^item> \<^emph>\<open>document classes\<close> (\<^boxed_theory_text>\<open>doc_class\<close>) \<^index>\<open>doc\_class\<close> that describe concepts;
|
||||
the keyword (\<^boxed_theory_text>\<open>onto_class\<close>) \<^index>\<open>onto\_class\<close> is accpted equally;
|
||||
\<^item> an optional document base class expressing single inheritance
|
||||
class extensions;
|
||||
\<^item> \<^emph>\<open>attributes\<close> specific to document classes, where
|
||||
|
|
@ -233,7 +234,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
|
|||
\<^item> \<open>doc_class_specification\<close>:\<^index>\<open>doc\_class\_specification@\<open>doc_class_specification\<close>\<close>
|
||||
We call document classes with an \<open>accepts_clause\<close>
|
||||
\<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
|
||||
\<^rail>\<open> @@{command "doc_class"} class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
\<^rail>\<open> (@@{command "doc_class"}| @@{command "onto_class"}) class_id '=' (class_id '+')? (attribute_decl+) \<newline>
|
||||
(invariant_decl *)
|
||||
(accepts_clause rejects_clause?)?\<close>
|
||||
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
|
||||
|
|
@ -319,12 +320,17 @@ supported on the Isabelle/Isar level. Note that some more advanced functionality
|
|||
is currently only available in the SML API's of the kernel.
|
||||
|
||||
\<^item> \<open>meta_args\<close> :
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' term) *) \<close>
|
||||
\<^rail>\<open>obj_id ('::' class_id) ((',' attribute '=' HOL_term) *) \<close>
|
||||
\<^item> \<open>upd_meta_args\<close> :
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') term) * ))\<close>
|
||||
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
|
||||
\<^item> \<open>annotated_text_element\<close> :
|
||||
\<^rail>\<open>
|
||||
( @@{command "text*"}'[' meta_args ']' '\<open>' text '\<close>' |
|
||||
\<^rail>\<open>
|
||||
( ( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'
|
||||
| @@{command "ML*"} '[' meta_args ']' '\<open>' SML_code '\<close>'
|
||||
| @@{command "term*"} '[' meta_args ']' '\<open>' HOL_term '\<close>'
|
||||
| @@{command "value*"}'[' meta_args ']' '\<open>' HOL_term '\<close>'
|
||||
)
|
||||
|
|
||||
( @@{command "open_monitor*"}
|
||||
| @@{command "close_monitor*"}
|
||||
| @@{command "declare_reference*"}
|
||||
|
|
@ -350,10 +356,14 @@ text\<open>Recall that with the exception of \<^theory_text>\<open>text* \<dots>
|
|||
layout (such as \<^LaTeX>); these commands have to be wrapped into
|
||||
\<^verbatim>\<open>(*<*) ... (*>*)\<close> brackets if this is undesired. \<close>
|
||||
|
||||
subsection\<open>Ontologic Text-Elements and their Management\<close>
|
||||
text\<open> \<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
subsection\<open>Ontologic Text-Contexts and their Management\<close>
|
||||
text\<open> With respect to the family of text elements,
|
||||
\<^theory_text>\<open>text*[oid::cid, ...] \<open> \<dots> text \<dots> \<close> \<close> is the core-command of \<^isadof>: it permits to create
|
||||
an object of meta-data belonging to the class \<^theory_text>\<open>cid\<close>. This is viewed as the \<^emph>\<open>definition\<close> of
|
||||
an instance of a document class. This instance object is attached to the text-element
|
||||
an instance of a document class. The class invariants were checked for all attribute values
|
||||
at creation time if not specified otherwise. Unspecified attributed values were represented
|
||||
by fresh free variables.
|
||||
This instance object is attached to the text-element
|
||||
and makes it thus "trackable" for \<^isadof>, \<^ie>, it can be referenced via the \<^theory_text>\<open>oid\<close>, its attributes
|
||||
can be set by defaults in the class-definitions, or set at creation time, or modified at any
|
||||
point after creation via \<^theory_text>\<open>update_instance*[oid, ...]\<close>. The \<^theory_text>\<open>class_id\<close> is syntactically optional;
|
||||
|
|
@ -374,6 +384,35 @@ The precise presentation is decided in the \<^emph>\<open>layout definitions\<cl
|
|||
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Code-Contexts and their Management\<close>
|
||||
|
||||
text\<open>The \<^theory_text>\<open>ML*[oid::cid, ...] \<open> \<dots> SML-code \<dots> \<close>\<close>-document elements proceed similarly :
|
||||
a referentiable meta-object of class \<^theory_text>\<open>cid\<close> is created, initialized with the optional
|
||||
attributes and bound to \<^theory_text>\<open>oid\<close>. The SML-code is type-checked and executed
|
||||
in the context of the SML toplevel of the Isabelle system as in the corresponding
|
||||
\<^theory_text>\<open>ML\<open> \<dots> SML-code \<dots> \<close>\<close>-command.
|
||||
\<close>
|
||||
|
||||
subsection\<open>Ontologic Term-Contexts and their Management\<close>
|
||||
text\<open>The major commands providing term-contexts are
|
||||
\<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
|
||||
\<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>\<^footnote>\<open>Note that the meta-argument list is optional.\<close>.
|
||||
Wrt. to creation, track-ability and checking they are analogous to the ontological text and
|
||||
code-commands. However the argument terms may contain term-antiquotations stemming from an
|
||||
ontology definition. Both term-contexts ware type-checked and \<^emph>\<open>validated\<close> against
|
||||
the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers
|
||||
to a meta-object belonging to the document class \<open>A\<close>, for example).
|
||||
The term-context in the \<open>value*\<close>-command is additionally expanded (\<^eg> replaced) by a term
|
||||
denoting the meta-object. This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
|
||||
executable HOL-functions to interact with meta-objects.
|
||||
|
||||
Note unspecified attribute values were represented by free fresh variables which constrains \<^dof>
|
||||
to choose either to the normalisation-by-evaluation strategy \<^theory_text>\<open>nbe\<close> or to a proof attempt via
|
||||
the \<^theory_text>\<open>auto\<close>. A failure of these strategies will be reported and regarded as non-validation
|
||||
of this meta-object. The latter leads to a failure of the entire command.
|
||||
|
||||
\<close>
|
||||
|
||||
(*<*)
|
||||
declare_reference*["sec:advanced"::technical]
|
||||
(*>*)
|
||||
|
|
|
|||
|
|
@ -37,8 +37,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
|
||||
and "open_monitor*" "close_monitor*"
|
||||
"declare_reference*" "update_instance*"
|
||||
"doc_class"
|
||||
"onto_class" (* a wish from Idir *)
|
||||
"doc_class" "onto_class" (* a syntactic alternative *)
|
||||
"ML*"
|
||||
"define_shortcut*" "define_macro*" :: thy_decl
|
||||
|
||||
and "text*" "text-macro*" :: document_body
|
||||
|
|
@ -1217,108 +1217,7 @@ fun document_command markdown (loc, txt) =
|
|||
*)
|
||||
|
||||
|
||||
ML \<comment> \<open>\<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close>
|
||||
(*
|
||||
The value* command uses the same code as the value command
|
||||
and adds the possibility to evaluate Term Annotation Antiquotations (TA)
|
||||
with the help of the DOF_core.transduce_term_global function.
|
||||
*)
|
||||
(* Title: HOL/Tools/value_command.ML
|
||||
Author: Florian Haftmann, TU Muenchen
|
||||
|
||||
Generic value command for arbitrary evaluators, with default using nbe or SML.
|
||||
*)
|
||||
\<open>
|
||||
signature VALUE_COMMAND =
|
||||
sig
|
||||
val value: Proof.context -> term -> term
|
||||
val value_select: string -> Proof.context -> term -> term
|
||||
val value_cmd: xstring -> string list -> string -> Toplevel.state -> Toplevel.transition -> unit
|
||||
val add_evaluator: binding * (Proof.context -> term -> term)
|
||||
-> theory -> string * theory
|
||||
end;
|
||||
|
||||
|
||||
structure Value_Command : VALUE_COMMAND =
|
||||
struct
|
||||
|
||||
structure Evaluators = Theory_Data
|
||||
(
|
||||
type T = (Proof.context -> term -> term) Name_Space.table;
|
||||
val empty = Name_Space.empty_table "evaluator";
|
||||
val extend = I;
|
||||
val merge = Name_Space.merge_tables;
|
||||
)
|
||||
|
||||
fun add_evaluator (b, evaluator) thy =
|
||||
let
|
||||
val (name, tab') = Name_Space.define (Context.Theory thy) true
|
||||
(b, evaluator) (Evaluators.get thy);
|
||||
val thy' = Evaluators.put tab' thy;
|
||||
in (name, thy') end;
|
||||
|
||||
fun intern_evaluator ctxt raw_name =
|
||||
if raw_name = "" then ""
|
||||
else Name_Space.intern (Name_Space.space_of_table
|
||||
(Evaluators.get (Proof_Context.theory_of ctxt))) raw_name;
|
||||
|
||||
fun default_value ctxt t =
|
||||
if null (Term.add_frees t [])
|
||||
then Code_Evaluation.dynamic_value_strict ctxt t
|
||||
else Nbe.dynamic_value ctxt t;
|
||||
|
||||
fun value_select name ctxt =
|
||||
if name = ""
|
||||
then default_value ctxt
|
||||
else Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt;
|
||||
|
||||
fun value ctxt term = value_select "" ctxt
|
||||
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
|
||||
(Proof_Context.theory_of ctxt))
|
||||
|
||||
fun value_cmd raw_name modes raw_t state trans =
|
||||
let
|
||||
val ctxt = Toplevel.context_of state;
|
||||
val name = intern_evaluator ctxt raw_name;
|
||||
val t = Syntax.read_term ctxt raw_t;
|
||||
val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , Toplevel.pos_of trans)
|
||||
(Proof_Context.theory_of ctxt);
|
||||
val t' = value_select name ctxt term';
|
||||
val ty' = Term.type_of t';
|
||||
val ctxt' = Proof_Context.augment t' ctxt;
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
||||
in Pretty.writeln p end;
|
||||
|
||||
val opt_modes =
|
||||
Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
|
||||
|
||||
val opt_evaluator =
|
||||
Scan.optional (\<^keyword>\<open>[\<close> |-- Parse.name --| \<^keyword>\<open>]\<close>) "";
|
||||
|
||||
(*
|
||||
We want to have the current position to pass it to transduce_term_global in
|
||||
value_cmd, so we pass the Toplevel.transition
|
||||
*)
|
||||
fun pass_trans_to_value_cmd ((name, modes), t) trans =
|
||||
Toplevel.keep (fn state => value_cmd name modes t state trans) trans
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
|
||||
(opt_evaluator -- opt_modes -- Parse.term >> pass_trans_to_value_cmd);
|
||||
|
||||
val _ = Theory.setup
|
||||
(Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>
|
||||
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
|
||||
(fn ctxt => fn ((name, style), t) =>
|
||||
Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
|
||||
#> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
|
||||
|
||||
end;
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
structure ODL_Command_Parser =
|
||||
|
|
@ -1595,7 +1494,7 @@ fun check_invariants thy oid =
|
|||
|
||||
fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy =
|
||||
let
|
||||
val id = serial ();
|
||||
val id = serial ();
|
||||
val _ = Position.report pos (docref_markup true oid id pos);
|
||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
|
|
@ -1862,6 +1761,141 @@ end
|
|||
\<close>
|
||||
|
||||
|
||||
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close>
|
||||
(*
|
||||
The value* command uses the same code as the value command
|
||||
and adds the evaluation Term Annotation Antiquotations (TA)
|
||||
with the help of the DOF_core.transduce_term_global function.
|
||||
*)
|
||||
(* Based on:
|
||||
Title: HOL/Tools/value_command.ML
|
||||
Author: Florian Haftmann, TU Muenchen
|
||||
|
||||
Generic value command for arbitrary evaluators, with default using nbe or SML.
|
||||
*)
|
||||
\<open>
|
||||
signature VALUE_COMMAND =
|
||||
sig
|
||||
val value: Proof.context -> term -> term
|
||||
val value_select: string -> Proof.context -> term -> term
|
||||
val value_cmd: xstring -> string list -> string -> Toplevel.state -> Toplevel.transition -> unit
|
||||
val add_evaluator: binding * (Proof.context -> term -> term)
|
||||
-> theory -> string * theory
|
||||
end;
|
||||
|
||||
|
||||
structure Value_Command : VALUE_COMMAND =
|
||||
struct
|
||||
|
||||
structure Evaluators = Theory_Data
|
||||
(
|
||||
type T = (Proof.context -> term -> term) Name_Space.table;
|
||||
val empty = Name_Space.empty_table "evaluator";
|
||||
val extend = I;
|
||||
val merge = Name_Space.merge_tables;
|
||||
)
|
||||
|
||||
fun add_evaluator (b, evaluator) thy =
|
||||
let
|
||||
val (name, tab') = Name_Space.define (Context.Theory thy) true
|
||||
(b, evaluator) (Evaluators.get thy);
|
||||
val thy' = Evaluators.put tab' thy;
|
||||
in (name, thy') end;
|
||||
|
||||
fun intern_evaluator ctxt raw_name =
|
||||
if raw_name = "" then ""
|
||||
else Name_Space.intern (Name_Space.space_of_table
|
||||
(Evaluators.get (Proof_Context.theory_of ctxt))) raw_name;
|
||||
|
||||
fun default_value ctxt t =
|
||||
if null (Term.add_frees t [])
|
||||
then Code_Evaluation.dynamic_value_strict ctxt t
|
||||
else Nbe.dynamic_value ctxt t;
|
||||
|
||||
fun value_select name ctxt =
|
||||
if name = ""
|
||||
then default_value ctxt
|
||||
else Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt;
|
||||
|
||||
fun value ctxt term = value_select "" ctxt
|
||||
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
|
||||
(Proof_Context.theory_of ctxt))
|
||||
|
||||
fun value_cmd raw_name modes raw_t state trans =
|
||||
let
|
||||
val ctxt = Toplevel.context_of state;
|
||||
val name = intern_evaluator ctxt raw_name;
|
||||
val t = Syntax.read_term ctxt raw_t;
|
||||
val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , Toplevel.pos_of trans)
|
||||
(Proof_Context.theory_of ctxt);
|
||||
val t' = value_select name ctxt term';
|
||||
val ty' = Term.type_of t';
|
||||
val ctxt' = Proof_Context.augment t' ctxt;
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
||||
in Pretty.writeln p end;
|
||||
|
||||
val opt_modes =
|
||||
Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
|
||||
|
||||
val opt_evaluator =
|
||||
Scan.optional (\<^keyword>\<open>[\<close> |-- Parse.name --| \<^keyword>\<open>]\<close>) "";
|
||||
|
||||
(*
|
||||
We want to have the current position to pass it to transduce_term_global in
|
||||
value_cmd, so we pass the Toplevel.transition
|
||||
*)
|
||||
fun pass_trans_to_value_cmd ((name, modes), t) trans =
|
||||
Toplevel.keep (fn state => value_cmd name modes t state trans) trans
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
|
||||
(opt_evaluator -- opt_modes -- Parse.term >> pass_trans_to_value_cmd);
|
||||
|
||||
val _ = Theory.setup
|
||||
(Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>
|
||||
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
|
||||
(fn ctxt => fn ((name, style), t) =>
|
||||
Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
|
||||
#> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
|
||||
|
||||
end;
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
|
||||
(*
|
||||
The ML* generates an "ontology-aware" version of the SML code-execution command.
|
||||
*)
|
||||
\<open>
|
||||
structure ML_star_Command =
|
||||
struct
|
||||
|
||||
fun meta_args_exec NONE thy = thy
|
||||
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
|
||||
thy |> (ODL_Command_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline = false}
|
||||
oid pos (I cid_pos) (I doc_attrs))
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("ML*", \<^here>) "ODL annotated ML text within theory or local theory"
|
||||
(((Scan.option ODL_Command_Parser.attributes) -- Parse.ML_source)
|
||||
>> (fn (meta_args_opt, source) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
Toplevel.generic_theory
|
||||
(ML_Context.exec (fn () =>
|
||||
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
|
||||
Local_Theory.propagate_ml_env)));
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
structure ODL_LTX_Converter =
|
||||
|
|
@ -2553,6 +2587,9 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>define_macro*\<close> "d
|
|||
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
ML\<open>
|
||||
Pretty.text;
|
||||
|
|
|
|||
|
|
@ -8,6 +8,16 @@ imports
|
|||
"Isabelle_DOF-tests.TermAntiquotations"
|
||||
begin
|
||||
|
||||
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
|
||||
|
||||
ML*[the_function::C,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1)\<close>
|
||||
ML*\<open>3+4\<close> (* meta-args are optional *)
|
||||
|
||||
text\<open>... and here we reference @{B [display] "the_function"}.\<close>
|
||||
|
||||
section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
|
||||
|
||||
|
||||
text\<open>The value* command uses the same code as the value command
|
||||
and adds the possibility to evaluate Term Annotation Antiquotations (TA).
|
||||
For that an elaboration of the term referenced by a TA must be done before
|
||||
|
|
@ -155,4 +165,5 @@ to update the instance @{docitem \<open>xcv4\<close>}:
|
|||
(* Error:
|
||||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{G ''xcv5''})}"]*)
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue