From f2bb4f6e31d24a9ba3c2d02882281fb70123e34c Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 15 Jul 2019 17:12:10 +0200 Subject: [PATCH 01/10] Modifications / evolutions for the second TR example. Arrived at page 34. --- .../MyCommentedIsabelle.thy | 212 +- .../TR_my_commented_isabelle/ROOT | 5 +- .../TR_MyCommentedIsabelle.thy | 2013 +++++++++++++++++ .../document/root.bib | 528 +++++ 4 files changed, 2736 insertions(+), 22 deletions(-) create mode 100644 examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy create mode 100644 examples/technical_report/TR_my_commented_isabelle/document/root.bib diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 60e2d122..ca889f75 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -8,15 +8,16 @@ begin open_monitor*[this::report] (*>*) -title*[tit::title]\An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\ -subtitle*[stit::subtitle]\Version : Isabelle 2017\ +title*[tit::title]\My Personal, Ecclectic Isabelle Programming Manual\ +subtitle*[stit::subtitle]\Version : Isabelle 2019\ text*[bu::author, email = "''wolff@lri.fr''", - affiliation = "''Universit\\'e Paris-Saclay, Paris, France''"]\Burkhart Wolff\ + affiliation = "\Université Paris-Saclay, LRI, France\"]\Burkhart Wolff\ text*[abs::abstract, - keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Tactic Programming'']"]\ + keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Programming Guide'', + ''Tactic Programming'']"]\ While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a system framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the @@ -127,9 +128,11 @@ figure*[fig2::figure, relative_width="100",src="''figures/text-element''"] text\ text-commands, ML- commands (and in principle any other command) can be seen as \<^emph>\quotations\ over the underlying SML environment (similar to OCaml or Haskell). Linking these different sorts of quotations with each other and the underlying SML-envirnment -is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a programming technique -to specify expressions or patterns in a quotation, parsed in the context of the enclosing expression -or pattern where the quotation is. +is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a programming +technique to specify expressions or patterns in a quotation, parsed in the context of the +enclosing expression or pattern where the quotation is. Another way to understand this concept: +anti-quotations are "semantic macros" that produce a value for the surrounding context +(ML, text, HOL, whatever) depending on local arguments and the underlying logical context. The way an antiquotation is specified depends on the quotation expander: typically a specific character and an identifier, or specific parentheses and a complete expression or pattern.\ @@ -306,8 +309,8 @@ ML\ \ -subsection*[t213::example]\Mechanism 2 : global arbitrary data structure that is attached to the global and - local Isabelle context $\theta$ \ +subsection*[t213::example]\Mechanism 2 : global arbitrary data structure that is attached to + the global and local Isabelle context $\theta$ \ ML \ datatype X = mt @@ -1048,11 +1051,31 @@ function. Thus, the Isar-toplevel supports the generic document model and allows for user-programmed extensions. \ -text\Isabelle \<^verbatim>\.thy\-files were processed by two types of parsers: +text\In the traditional literature, Isabelle \<^verbatim>\.thy\-files were +were said to be processed by processed by two types of parsers: \<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed by a lexer-library and parser combinators built on top, and \<^enum> the "inner-syntax" (i.e. the syntax for @{term \\\} - terms) - with an evolved, eight-layer parsing and pretty-printing process. + with an evolved, eight-layer parsing and pretty-printing process + based on an Early-algorithm. +\ + +text\This picture is less and less true for a number of reasons: +\<^enum> With the advent of \inlineisar+\ ... \+, a mechanism for + \<^emph>\cascade-syntax\ came to the Isabelle platform that introduce a flexible means + to change parsing contexts \<^emph>\and\ parsing technologies. +\<^enum> Inside the term-parser levels, the concept of \<^emph>\cartouche\ can be used + to escape the parser and its underlying parsing technology. +\<^enum> Outside, in the traditional toplevel-parsers, the + \inlineisar+\ ... \+ is becoming more and more enforced + (some years ago, syntax like \term{* ... *}\ was replaced by + syntax \term(\)... (\)\. This makes technical support of cascade syntax + more and more easy. +\<^enum> The Lexer infra-structure is already rather generic; nothing prevents to + add beside the lexer - configurations for ML-Parsers, Toplevel Command Syntax + parsers, mathematical notation parsers for $\lambda$-terms new pillars + of parsing technologies, say, for parsing C or Rust or JavaScript inside + Isabelle. \ @@ -1116,7 +1139,8 @@ and properties; @{ML_structure Markup} provides a number of of such \<^emph>\\Isabelle_DOF\. A markup must be tagged with an id; this is done by the @{ML serial}-function discussed earlier.\ -ML\ +subsection\A simple Example\ +ML\ local val docclassN = "doc_class"; @@ -1143,17 +1167,167 @@ in the Front-End, converts this into markup together with a unique number identi markup, and sends this as a report to the Front-End. \ -section\Environment Structured Reporting\ +subsection\A Slightly more Complex Example\ +ML \ + +fun markup_tvar def_name ps (name, id) = + let + fun markup_elem name = (name, (name, []): Markup.T); + val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is"); + val entity = Markup.entity tvarN name + val def = def_name = NONE + in + tvar :: + (if def then I else cons (Markup.keyword_properties Markup.ML_keyword3)) + (map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps) + end + +fun report [] _ _ = I + | report ps markup x = + let val ms = markup x + in fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps end +\ + +ML \ +local +val data = \ \Derived from Yakoub's example ;-)\ + + [ (\Frédéric 1er\, \King of Naples\) + , (\Frédéric II\, \King of Sicily\) + , (\Frédéric III\, \the Handsome\) + , (\Frédéric IV\, \of the Empty Pockets\) + , (\Frédéric V\, \King of Denmark–Norway\) + , (\Frédéric VI\, \the Knight\) + , (\Frédéric VII\, \Count of Toggenburg\) + , (\Frédéric VIII\, \Count of Zollern\) + , (\Frédéric IX\, \the Old\) + , (\Frédéric X\, \the Younger\) ] + +val (tab0, markup) = + fold_map (fn (name, msg) => fn reports => + let val id = serial () + val pos = [Input.pos_of name] + in + ( (fst(Input.source_content msg), (name, pos, id)) + , report pos (markup_tvar NONE pos) (fst(Input.source_content name), id) reports) + end) + data + [] + +val () = Position.reports_text markup +in +val tab = Symtab.make tab0 +end +\ + +ML \ +val _ = + fold (fn input => + let + val pos1' = Input.pos_of input + fun ctnt name0 = fst(Input.source_content name0) + val pos1 = [pos1'] + val msg1 = fst(Input.source_content input) + val msg2 = "No persons were found to have such nickname" + in + case Symtab.lookup tab (fst(Input.source_content input)) of + NONE => tap (fn _ => Output.information (msg2 ^ Position.here_list pos1)) + (cons ((pos1', Markup.bad ()), "")) + | SOME (name0, pos0, id) => report pos1 (markup_tvar (SOME (ctnt name0)) pos0) (msg1, id) + end) + [ \the Knight\ \ \Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\ + , \the Handsome\ \ \Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\ + , \the Spy\ \ \Example of a failure to retrieve the person in \<^ML>\tab\\ + ] + [] + |> Position.reports_text +\ + +text\The pudding comes with the eating: \ + +subsection\Environment Structured Reporting\ + +text\ The structure @{ML_structure \Name_Space\} offers an own infra-structure for names and +manages the markup accordingly. MORE TO COME\ text\ @{ML_type "'a Name_Space.table"} \ -section\ Parsing issues \ -text\ Parsing combinators represent the ground building blocks of both generic input engines -as well as the specific Isar framework. They are implemented in the structure \verb+Token+ -providing core type \verb+Token.T+. +section\ The System Lexer and Token Issues\ +text\Four syntactic contexts are predefined in Isabelle (others can be added): +the ML context, the text context, the Isar-command context and the teerm-context, referring +to different needs of the Isabelle Framework as an extensible framework supporting incremental, +partially programmable extensions and as a Framework geared towards Formal Proofs and therefore +mathematical notations. The basic data-structure for the lexical treatment of these + \ -ML\ open Token\ + +subsection\Tokens\ + +text\The basic entity that lexers treat are \<^emph>\tokens\. defined in @{ML_structure "Token"}} +It provides a classification infrastructure, the references to positions and Markup +as well as way's to annotate tokens with (some) values they denote: +\ + +ML\ +local + open Token + + type dummy = Token.T + type src = Token.T list + type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} + + type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} + + + val _ = Token.is_command : Token.T -> bool; + val _ = Token.content_of : Token.T -> string; (* textueller kern eines Tokens. *) + + + val _ = pos_of: T -> Position.T + +(* +datatype kind = + (*immediate source*) + Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | + Float | Space | + (*delimited content*) + String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | + (*special content*) + Error of string | EOF + + datatype value = + Source of src | + Literal of bool * Markup.T | + Name of name_value * morphism | + Typ of typ | + Term of term | + Fact of string option * thm list | + Attribute of morphism -> attribute | + Declaration of declaration | + Files of file Exn.result list + + +*) +in val _ = () +end +\ + + + +subsection\A Lexer Configuration Example\ + +ML\ + +\ + + +section\ Combinator Parsing \ +text\Parsing Combinators go back to monadic programming as advocated by Wadler et. al, and has been +worked out @{cite "DBLP:journals/jfp/Hutton92"}\ + + +ML\ \ ML\ @@ -1172,8 +1346,6 @@ val _ = parser2contextparser : 'a parser -> 'a context_parser; (* bah, is the same as Scan.lift *) val _ = Scan.lift Args.cartouche_input : Input.source context_parser; -Token.is_command; -Token.content_of; (* textueller kern eines Tokens. *) \ diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index c57b3d69..8a75e642 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -1,8 +1,9 @@ -session "TR_mycommentedisabelle" = "Isabelle_DOF" + +session "TR_MyCommentedIsabelle" = "Isabelle_DOF" + options [document = pdf, document_output = "output",quick_and_dirty = true] theories - "MyCommentedIsabelle" + "TR_MyCommentedIsabelle" document_files + "root.bib" "isadof.cfg" "preamble.tex" "prooftree.sty" diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy new file mode 100644 index 00000000..5a482456 --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -0,0 +1,2013 @@ +(*<*) +theory TR_MyCommentedIsabelle + imports "Isabelle_DOF.technical_report" + (*imports "../../../ontologies/technical_report"*) +begin + + +open_monitor*[this::report] +(*>*) + +title*[tit::title]\My Personal, Ecclectic Isabelle Programming Manual\ +subtitle*[stit::subtitle]\Version : Isabelle 2019\ +text*[bu::author, + email = "''wolff@lri.fr''", + affiliation = "\Université Paris-Saclay, LRI, France\"]\Burkhart Wolff\ + + +text*[abs::abstract, + keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Programming Guide'', + ''Tactic Programming'']"]\ +While Isabelle is mostly known as part of Isabelle/HOL (an interactive +theorem prover), it actually provides a system framework for developing a wide +spectrum of applications. A particular strength of the Isabelle framework is the +combination of text editing, formal verification, and code generation. + +This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary +text to the unfortunately somewhat outdated "The Isabelle Cookbook" in +\url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged +not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jedit +in order to make experiments on the running code. + +This text is written itself in Isabelle/Isar using a specific document ontology +for technical reports. It is intended to be a "living document", i.e. it is not only +used for generating a static, conventional .pdf, but also for direct interactive +exploration in Isabelle/jedit. This way, types, intermediate results of computations and +checks can be repeated by the reader who is invited to interact with this document. +Moreover, the textual parts have been enriched with a maximum of formal content +which makes this text re-checkable at each load and easier maintainable. +\ + +chapter*[intro::introduction]\ Introduction \ + +text\ +While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually +provides a system framework for developing a wide spectrum of applications. A particular strength of +the Isabelle framework is the combination of text editing, formal verification, and code generation. +This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary text to the +unfortunately somewhat outdated "The Isabelle Cookbook" in +\url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged not only to consider +the generated .pdf, but also consult the loadable version in Isabelle/jedit in order to make +experiments on the running code. This text is written itself in Isabelle/Isar using a specific +document ontology for technical reports. It is intended to be a "living document", i.e. it is not +only used for generating a static, conventional .pdf, but also for direct interactive exploration +in Isabelle/jedit. This way, types, intermediate results of computations and checks can be +repeated by the reader who is invited to interact with this document. Moreover, the textual +parts have been enriched with a maximum of formal content which makes this text re-checkable at +each load and easier maintainable.\ + +figure*[architecture::figure,relative_width="80",src="''figures/isabelle-architecture''"]\ + The system architecture of Isabelle (left-hand side) and the + asynchronous communication between the Isabelle system and + the IDE (right-hand side). \ + +text\This cookbook roughly follows the Isabelle system architecture shown in +@{figure "architecture"}, and, to be more precise, more or less in the bottom-up order. + +We start from the basic underlying SML platform over the Kernels to the tactical layer +and end with a discussion over the front-end technologies. +\ + +chapter*[t1::technical]\ SML and Fundamental SML libraries \ + +section*[t11::technical] "ML, Text and Antiquotations" + +text\Isabelle is written in SML, the "Standard Meta-Language", which is is an impure functional +programming language allowing, in principle, mutable variables and side-effects. +The following Isabelle/Isar commands allow for accessing the underlying SML interpreter +of Isabelle directly. In the example, a mutable variable X is declared, defined to 0 and updated; +and finally re-evaluated leading to output: \ + +ML\ val X = Unsynchronized.ref 0; + X:= !X + 1; + X + \ + +text\However, since Isabelle is a platform involving parallel execution, concurrent computing, and, +as an interactive environment, involves backtracking / re-evaluation as a consequence of user- +interaction, imperative programming is discouraged and nearly never used in the entire Isabelle +code-base. The preferred programming style is purely functional: \ + +ML\ fun fac x = if x = 0 then 1 else x * fac(x-1) ; + fac 10; + \ +(* or *) +ML\ type state = { a : int, b : string} + fun incr_state ({a, b}:state) = {a=a+1, b=b} + \ + +text\ The faculty function is defined and executed; the (sub)-interpreter in Isar +works in the conventional read-execute-print loop for each statement separated by a ";". +Functions, types, data-types etc. can be grouped to modules (called \<^emph>\structures\) which can +be constrained to interfaces (called \<^emph>\signatures\) and even be parametric structures +(called \<^emph>\functors\). \ + +text\ The Isabelle/Isar interpreter (called \<^emph>\toplevel\ ) is extensible; by a mixture of SML +and Isar-commands, domain-specific components can be developed and integrated into the system +on the fly. Actually, the Isabelle system code-base consists mainly of SML and \<^verbatim>\.thy\-files +containing such mixtures of Isar commands and SML. \ + +text\ Besides the ML-command used in the above examples, there are a number of commands +representing text-elements in Isabelle/Isar; text commands can be interleaved arbitraryly +with other commands. Text in text-commands may use LaTeX and is used for type-setting +documentations in a kind of literate programming style. \ + +text\So: the text command for:\ + +text\\<^emph>\This is a text.\\ + +text\... is represented in an \<^verbatim>\.thy\ file by:\ + +text\\verb+text\\<^emph>\This is a text.\\+\ + +text\and desplayed in the Isabelle/jedit front-end at the sceen by:\ + +figure*[fig2::figure, relative_width="100",src="''figures/text-element''"] + \A text-element as presented in Isabelle/jedit. \ + +text\ text-commands, ML- commands (and in principle any other command) can be seen as +\<^emph>\quotations\ over the underlying SML environment (similar to OCaml or Haskell). +Linking these different sorts of quotations with each other and the underlying SML-envirnment +is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a programming +technique to specify expressions or patterns in a quotation, parsed in the context of the +enclosing expression or pattern where the quotation is. Another way to understand this concept: +anti-quotations are "semantic macros" that produce a value for the surrounding context +(ML, text, HOL, whatever) depending on local arguments and the underlying logical context. + +The way an antiquotation is specified depends on the quotation expander: typically a specific +character and an identifier, or specific parentheses and a complete expression or pattern.\ + +text\ In Isabelle documentations, antiquotation's were heavily used to enrich literate explanations +and documentations by "formal content", i.e. machine-checked, typed references +to all sorts of entities in the context of the interpreting environment. +Formal content allows for coping with sources that rapidly evolve and were developed by +distributed teams as is typical in open-source developments. +A paradigmatic example for antiquotation in Texts and Program snippets is here: +\ + +text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ +ML\ val x = @{thm refl}; + val y = @{term "A \ B"} + val y = @{typ "'a list"} + \ + +text\... which we will describe in more detail later. \ + +text\In a way, literate specification attempting to maximize its formal content is a way to +ensure "Agile Development" in a (theory)-document development, at least for its objectives, +albeit not for its popular methods and processes like SCRUM. \ + +paragraph\ + A maximum of formal content inside text documentation also ensures the + consistency of this present text with the underlying Isabelle version.\ + +section\The Isabelle/Pure bootstrap\ + +text\It is instructive to study the fundamental bootstrapping sequence of the Isabelle system; + it is written in the Isar format and gives an idea of the global module dependencies: + @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}. Loading this file + (for example by hovering over this hyperlink in the antiquotation holding control or + command key in Isabelle/jedit and activating it) allows the Isabelle IDE + to support hyperlinking \<^emph>\inside\ the Isabelle source.\ + +text\The bootstrapping sequence is also reflected in the following diagram +@{figure "architecture"}. \ + + +section*[t12::technical] "Elements of the SML library"; +text\Elements of the @{file "$ISABELLE_HOME/src/Pure/General/basics.ML"} SML library +are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions +except those generated by the specific "error" function are discouraged in Isabelle +source programming since they might produce races. Finally, a number of commonly +used "squigglish" combinators is listed: +\ +ML\ + Bind : exn; + Chr : exn; + Div : exn; + Domain : exn; + Fail : string -> exn; + Match : exn; + Overflow : exn; + Size : exn; + Span : exn; + Subscript : exn; + + exnName : exn -> string ; (* -- very interesting to query an unknown exception *) + exnMessage : exn -> string ; +\ + +ML\ +op ! : 'a Unsynchronized.ref -> 'a; +op := : ('a Unsynchronized.ref * 'a) -> unit; + +op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c; (* reversed function composition *) +op o : (('b -> 'c) * ('a -> 'b)) -> 'a -> 'c; +op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e; +op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e; +op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e; +op ? : bool * ('a -> 'a) -> 'a -> 'a; +ignore: 'a -> unit; +op before : ('a * unit) -> 'a; +I: 'a -> 'a; +K: 'a -> 'b -> 'a +\ + +text\Some basic examples for the programming style using these combinators can be found in the + "The Isabelle Cookbook" section 2.3.\ + +text\An omnipresent data-structure in the Isabelle SML sources are tables +implemented in @{file "$ISABELLE_HOME/src/Pure/General/table.ML"}. These +generic tables are presented in an efficient purely functional implementation using +balanced 2-3 trees. Key operations are:\ +ML\ +signature TABLE_reduced = +sig + type key + type 'a table + exception DUP of key + exception SAME + exception UNDEF of key + val empty: 'a table + val dest: 'a table -> (key * 'a) list + val keys: 'a table -> key list + val lookup_key: 'a table -> key -> (key * 'a) option + val lookup: 'a table -> key -> 'a option + val defined: 'a table -> key -> bool + val update: key * 'a -> 'a table -> 'a table + (* ... *) +end +\ +text\... where \<^verbatim>\key\ is usually just a synonym for string.\ + +chapter*[t2::technical] \ Prover Architecture \ + +section*[t21::technical] \ The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts \ + +text\ What I call the 'Nano-Kernel' in Isabelle can also be seen as an acyclic theory graph. +The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}. +My notion is a bit criticisable since this component, which provides the type of @{ML_type theory} +and @{ML_type Proof.context}, is not that Nano after all. +However, these type are pretty empty place-holders at that level and the content of +@{file "$ISABELLE_HOME/src/Pure/theory.ML"} is registered much later. +The sources themselves mention it as "Fundamental Structure". +In principle, theories and proof contexts could be REGISTERED as user data inside contexts. +The chosen specialization is therefore an acceptable meddling of the abstraction "Nano-Kernel" +and its application context: Isabelle. + +Makarius himself says about this structure: + +"Generic theory contexts with unique identity, arbitrarily typed data, +monotonic development graph and history support. Generic proof +contexts with arbitrarily typed data." + +In my words: a context is essentially a container with +\<^item> an id +\<^item> a list of parents (so: the graph structure) +\<^item> a time stamp and +\<^item> a sub-context relation (which uses a combination of the id and the time-stamp to + establish this relation very fast whenever needed; it plays a crucial role for the + context transfer in the kernel. + + +A context comes in form of three 'flavours': +\<^item> theories : @{ML_type theory}'s, containing a syntax and axioms, but also + user-defined data and configuration information. +\<^item> Proof-Contexts: @{ML_type Proof.context} + containing theories but also additional information if Isar goes into prove-mode. + In general a richer structure than theories coping also with fixes, facts, goals, + in order to support the structured Isar proof-style. +\<^item> Generic: @{ML_type Context.generic }, i.e. the sum of both. + +All context have to be seen as mutable; so there are usually transformations defined on them +which are possible as long as a particular protocol (\<^verbatim>\begin_thy\ - \<^verbatim>\end_thy\ etc) are respected. + +Contexts come with type user-defined data which is mutable through the entire lifetime of +a context. +\ + +subsection*[t212::technical]\ Mechanism 1 : Core Interface. \ +text\To be found in @{file "$ISABELLE_HOME/src/Pure/context.ML"}:\ + +ML\ +Context.parents_of: theory -> theory list; +Context.ancestors_of: theory -> theory list; +Context.proper_subthy : theory * theory -> bool; +Context.Proof: Proof.context -> Context.generic; (*constructor*) +Context.proof_of : Context.generic -> Proof.context; +Context.certificate_theory_id : Context.certificate -> Context.theory_id; +Context.theory_name : theory -> string; +Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic; +\ + + +text\ML structure @{ML_structure Proof_Context}:\ +ML\ + Proof_Context.init_global: theory -> Proof.context; + Context.Proof: Proof.context -> Context.generic; (* the path to a generic Context *) + Proof_Context.get_global: theory -> string -> Proof.context +\ + + +subsection*[t213::example]\Mechanism 2 : global arbitrary data structure that is attached to + the global and local Isabelle context $\theta$ \ +ML \ + +datatype X = mt +val init = mt; +val ext = I +fun merge (X,Y) = mt + +structure Data = Generic_Data +( + type T = X + val empty = init + val extend = ext + val merge = merge +); + + + Data.get : Context.generic -> Data.T; + Data.put : Data.T -> Context.generic -> Context.generic; + Data.map : (Data.T -> Data.T) -> Context.generic -> Context.generic; + (* there are variants to do this on theories ... *) +\ + + +section\ The LCF-Kernel: terms, types, theories, proof\_contexts, thms \ +text\The classical LCF-style \<^emph>\kernel\ is about +\<^enum> Types and terms of a typed $\lambda$-Calculus including constant symbols, + free variables, $\lambda$-binder and application, +\<^enum> An infrastructure to define types and terms, a \<^emph>\signature\, + that also assigns to constant symbols types +\<^enum> An abstract type of \<^emph>\theorem\ and logical operations on them +\<^enum> (Isabelle specific): a notion of \<^emph>\theory\, i.e. a container + providing a signature and set (list) of theorems. +\ + + +subsection\ Terms and Types \ +text \A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \ +ML\ open Term; +signature TERM' = sig + (* ... *) + type indexname = string * int + type class = string + type sort = class list + type arity = string * sort list * sort + datatype typ = + Type of string * typ list | + TFree of string * sort | + TVar of indexname * sort + datatype term = + Const of string * typ | + Free of string * typ | + Var of indexname * typ | + Bound of int | + Abs of string * typ * term | + $ of term * term + exception TYPE of string * typ list * term list + exception TERM of string * term list + (* ... *) +end +\ + +text\This core-data structure of the Isabelle Kernel is accessible in the Isabelle/ML environment +and serves as basis for programmed extensions concerning syntax, type-checking, and advanced +tactic programming over kernel primitives and higher API's. There are a number of anti-quotations +giving support for this task; since @{ML Const}-names are long-names revealing information +of the potentially evolving library structure, the use of anti-quotations leads to a safer programming +style of tactics and became therefore standard in the entire Isabelle code-base. +\ + +text\The following examples show how term- and type-level antiquotations are used and that + they can both be used for term-construction as well as term-destruction (pattern-matching):\ + +ML\ val Const ("HOL.implies", @{typ "bool \ bool \ bool"}) + $ Free ("A", @{typ "bool"}) + $ Free ("B", @{typ "bool"}) + = @{term "A \ B"}; + + val "HOL.bool" = @{type_name "bool"}; + + (* three ways to write type bool:@ *) + val Type("fun",[s,Type("fun",[@{typ "bool"},Type(@{type_name "bool"},[])])]) = @{typ "bool \ bool \ bool"}; + +\ + +text\Note that the SML interpreter is configured that he will actually print a type + \<^verbatim>\Type("HOL.bool",[])\ just as \<^verbatim>\"bool": typ\, so a compact notation looking + pretty much like a string. This can be confusing at times.\ + +text\Note, furthermore, that there is a programming API for the HOL-instance of Isabelle: +it is contained in @{file "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers for many +operators of the HOL logic specific constructors and destructors: +\ + +ML\ +HOLogic.boolT : typ; +HOLogic.mk_Trueprop: term -> term; +HOLogic.dest_Trueprop: term -> term; +HOLogic.Trueprop_conv: conv -> conv; +HOLogic.mk_setT: typ -> typ; +HOLogic.dest_setT: typ -> typ; +HOLogic.Collect_const: typ -> term; +HOLogic.mk_Collect: string * typ * term -> term; +HOLogic.mk_mem: term * term -> term; +HOLogic.dest_mem: term -> term * term; +HOLogic.mk_set: typ -> term list -> term; +HOLogic.conj_intr: Proof.context -> thm -> thm -> thm; +HOLogic.conj_elim: Proof.context -> thm -> thm * thm; +HOLogic.conj_elims: Proof.context -> thm -> thm list; +HOLogic.conj: term; +HOLogic.disj: term; +HOLogic.imp: term; +HOLogic.Not: term; +HOLogic.mk_not: term -> term; +HOLogic.mk_conj: term * term -> term; +HOLogic.dest_conj: term -> term list; +HOLogic.conjuncts: term -> term list; +(* ... *) +\ + + + +subsection\ Type-Certification (=checking that a type annotation is consistent) \ + +ML\ Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) \ +text\ there is a joker type that can be added as place-holder during term construction. + Jokers can be eliminated by the type inference. \ + +ML\ Term.dummyT : typ \ + +ML\ +Sign.typ_instance: theory -> typ * typ -> bool; +Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv; +Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int; +Sign.const_type: theory -> string -> typ option; +Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*) +Sign.cert_term: theory -> term -> term; (* short-cut for the latter *) +Sign.tsig_of: theory -> Type.tsig (* projects the type signature *) +\ +text\ +@{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure +@{ML_structure "Type"} +which contains the heart of the type inference. +It also contains the type substitution type @{ML_type "Type.tyenv"} which is +is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"} +which in itself is a synonym for @{ML_type "'a Symtab.table"}, so +possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. \ + +text\Note that @{emph \polymorphic variables\} are treated like constant symbols +in the type inference; thus, the following test, that one type is an instance of the +other, yields false: +\ +ML\ +val ty = @{typ "'a option"}; +val ty' = @{typ "int option"}; + +val Type("List.list",[S]) = @{typ "('a) list"}; (* decomposition example *) + +val false = Sign.typ_instance @{theory}(ty', ty); +\ +text\In order to make the type inference work, one has to consider @{emph \schematic\} +type variables, which are more and more hidden from the Isar interface. Consequently, +the typ antiquotation above will not work for schematic type variables and we have +to construct them by hand on the SML level: \ +ML\ +val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); +\ +text\ MIND THE "'" !!!\ +text \On this basis, the following @{ML_type "Type.tyenv"} is constructed: \ +ML\ +val tyenv = Sign.typ_match ( @{theory}) + (t_schematic, @{typ "int list"}) + (Vartab.empty); +val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv; +\ + +text\ Type generalization --- the conversion between free type variables and schematic +type variables --- is apparently no longer part of the standard API (there is a slightly +more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to +overcome this by a self-baked generalization function:\ + +ML\ +val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort)); +val generalize_term = Term.map_types generalize_typ; +val true = Sign.typ_instance @{theory} (ty', generalize_typ ty) +\ +text\... or more general variants thereof that are parameterized by the indexes for schematic +type variables instead of assuming just @{ML "0"}. \ + +text\ Example:\ +ML\val t = generalize_term @{term "[]"}\ + +text +\Now we turn to the crucial issue of type-instantiation and with a given type environment +@{ML "tyenv"}. For this purpose, one has to switch to the low-level interface +@{ML_structure "Term_Subst"}. +\ + +ML\ +Term_Subst.map_types_same : (typ -> typ) -> term -> term; +Term_Subst.map_aterms_same : (term -> term) -> term -> term; +Term_Subst.instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term -> term; +Term_Subst.instantiateT: ((indexname * sort) * typ) list -> typ -> typ; +Term_Subst.generalizeT: string list -> int -> typ -> typ; + (* this is the standard type generalisation function !!! + only type-frees in the string-list were taken into account. *) +Term_Subst.generalize: string list * string list -> int -> term -> term + (* this is the standard term generalisation function !!! + only type-frees and frees in the string-lists were taken + into account. *) +\ + +text \Apparently, a bizarre conversion between the old-style interface and +the new-style @{ML "tyenv"} is necessary. See the following example.\ +ML\ +val S = Vartab.dest tyenv; +val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list; + (* it took me quite some time to find out that these two type representations, + obscured by a number of type-synonyms, where actually identical. *) +val ty = t_schematic; +val ty' = Term_Subst.instantiateT S' t_schematic; +val t = (generalize_term @{term "[]"}); + +val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t) +(* or alternatively : *) +val t'' = Term.map_types (Term_Subst.instantiateT S') (t) +\ + +subsection\ Type-Inference (= inferring consistent type information if possible) \ + +text\ Type inference eliminates also joker-types such as @{ML dummyT} and produces + instances for schematic type variables where necessary. In the case of success, + it produces a certifiable term. \ +ML\ +Type_Infer_Context.infer_types: Proof.context -> term list -> term list +\ + +subsection\ thy and the signature interface\ +ML\ +Sign.tsig_of: theory -> Type.tsig; +Sign.syn_of : theory -> Syntax.syntax; +Sign.of_sort : theory -> typ * sort -> bool ; +\ + +subsection\ Thm's and the LCF-Style, "Mikro"-Kernel \ +text\ + The basic constructors and operations on theorems@{file "$ISABELLE_HOME/src/Pure/thm.ML"}, + a set of derived (Pure) inferences can be found in @{file "$ISABELLE_HOME/src/Pure/drule.ML"}. + + The main types provided by structure \<^verbatim>\thm\ are certified types @{ML_type ctyp}, + certified terms @{ML_type cterm}, @{ML_type thm} as well as conversions @{ML_type conv}. +\ + +ML\ +signature BASIC_THM = +sig + type ctyp + type cterm + exception CTERM of string * cterm list + type thm + type conv = cterm -> thm + exception THM of string * int * thm list +end; +\ + +text\Certification of types and terms on the kernel-level is done by the generators:\ +ML\ + Thm.global_ctyp_of: theory -> typ -> ctyp; + Thm.ctyp_of: Proof.context -> typ -> ctyp; + Thm.global_cterm_of: theory -> term -> cterm; + Thm.cterm_of: Proof.context -> term -> cterm; +\ +text\... which perform type-checking in the given theory context in order to make a type + or term "admissible" for the kernel.\ + +text\ We come now to the very heart of the LCF-Kernel of Isabelle, which + provides the fundamental inference rules of Isabelle/Pure. + + Besides a number of destructors on @{ML_type thm}'s, + the abstract data-type \<^verbatim>\thm\ is used for logical objects of the form + $\Gamma \vdash_\theta \phi$, where $\Gamma$ represents a set of local assumptions, + $\theta$ the "theory" or more precisely the global context in which a formula $\phi$ + has been constructed just by applying the following operations representing + logical inference rules: + +\ +ML\ + (*inference rules*) + Thm.assume: cterm -> thm; + Thm.implies_intr: cterm -> thm -> thm; + Thm.implies_elim: thm -> thm -> thm; + Thm.forall_intr: cterm -> thm -> thm; + Thm.forall_elim: cterm -> thm -> thm; + + Thm.transfer : theory -> thm -> thm; + + Thm.generalize: string list * string list -> int -> thm -> thm; + Thm.instantiate: ((indexname*sort)*ctyp)list * ((indexname*typ)*cterm) list -> thm -> thm; +\ +text\ They reflect the Pure logic depicted in a number of presentations such as + M. Wenzel, \<^emph>\Parallel Proof Checking in Isabelle/Isar\, PLMMS 2009, or simiular papers. + Notated as logical inference rules, these operations were presented as follows: +\ + +side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''", + caption="''Pure Kernel Inference Rules I ''",relative_width="48", + src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''", + caption2="''Pure Kernel Inference Rules II''",relative_width2="47", + src2="''figures/pure-inferences-II''"]\ \ + +(* +figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"] + \ Pure Kernel Inference Rules I.\ +figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"] + \ Pure Kernel Inference Rules II. \ + *) + +text\Note that the transfer rule: +\[ +\begin{prooftree} + \Gamma \vdash_\theta \phi \qquad \qquad \theta \sqsubseteq \theta' +\justifies + \Gamma \vdash_{\theta'} \phi \qquad \qquad +\end{prooftree} +\] +which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design +and a remarkable difference to its sisters HOL-Light and HOL4; instead of transfer, these systems +reconstruct proofs in an enlarged global context instead of taking the result and converting it.\ + +text\Besides the meta-logical (Pure) implication $\_\Longrightarrow \_$, the Kernel axiomatizes +also a Pure-Equality $\_ \equiv \_ $ used for definitions of constant symbols: \ +ML\ + Thm.reflexive: cterm -> thm; + Thm.symmetric: thm -> thm; + Thm.transitive: thm -> thm -> thm; +\ +text\The operation:\ +ML\ Thm.trivial: cterm -> thm; \ +text\... produces the elementary tautologies of the form @{prop "A \ A"}, + an operation used to start a backward-style proof.\ + +text\The elementary conversions are:\ +ML\ + Thm.beta_conversion: bool -> conv; + Thm.eta_conversion: conv; + Thm.eta_long_conversion: conv; +\ + +text\On the level of @{ML_structure "Drule"}, a number of higher-level operations is established, + which is in part accessible by a number of forward-reasoning notations on Isar-level.\ +ML\ + op RSN: thm * (int * thm) -> thm; + op RS: thm * thm -> thm; + op RLN: thm list * (int * thm list) -> thm list; + op RL: thm list * thm list -> thm list; + op MRS: thm list * thm -> thm; + op OF: thm * thm list -> thm; + op COMP: thm * thm -> thm; +\ + + +subsection\ Theories \ + +text \ This structure yields the datatype \verb*thy* which becomes the content of +\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel, +which inspired me (bu) to this naming. + +\ +ML\ + +(* intern Theory.Thy; + +datatype thy = Thy of + {pos: Position.T, + id: serial, + axioms: term Name_Space.table, + defs: Defs.T, + wrappers: wrapper list * wrapper list}; + +*) + +Theory.check: {long: bool} -> Proof.context -> string * Position.T -> theory; + +Theory.local_setup: (Proof.context -> Proof.context) -> unit; +Theory.setup: (theory -> theory) -> unit; (* The thing to extend the table of "command"s with parser - callbacks. *) +Theory.get_markup: theory -> Markup.T; +Theory.axiom_table: theory -> term Name_Space.table; +Theory.axiom_space: theory -> Name_Space.T; +Theory.axioms_of: theory -> (string * term) list; +Theory.all_axioms_of: theory -> (string * term) list; +Theory.defs_of: theory -> Defs.T; +Theory.at_begin: (theory -> theory option) -> theory -> theory; +Theory.at_end: (theory -> theory option) -> theory -> theory; +Theory.begin_theory: string * Position.T -> theory list -> theory; +Theory.end_theory: theory -> theory; + +\ + + +section\Backward Proofs: Tactics, Tacticals and Goal-States\ + +text\At this point, we leave the Pure-Kernel and start to describe the first layer on top +of it, involving support for specific styles of reasoning and automation of reasoning.\ + +text\ \<^verbatim>\tactic\'s are in principle \<^emph>\relations\ on theorems @{ML_type "thm"}; this gives a natural way +to represent the fact that HO-Unification (and therefore the mechanism of rule-instantiation) +are non-deterministic in principle. Heuristics may choose particular preferences between +the theorems in the range of this relation, but the Isabelle Design accepts this fundamental +fact reflected at this point in the prover architecture. +This potentially infinite relation is implemented by a function of theorems to lazy lists +over theorems, which gives both sufficient structure for heuristic +considerations as well as a nice algebra, called \<^verbatim>\TACTICAL\'s, providing a bottom element +@{ML "no_tac"} (the function that always fails), the top-element @{ML "all_tac"} + (the function that never fails), sequential composition @{ML "op THEN"}, (serialized) +non-deterministic composition @{ML "op ORELSE"}, conditionals, repetitions over lists, etc. +The following is an excerpt of @{file "~~/src/Pure/tactical.ML"}: +\ + +ML\ +signature TACTICAL = +sig + type tactic = thm -> thm Seq.seq + + val all_tac: tactic + val no_tac: tactic + val COND: (thm -> bool) -> tactic -> tactic -> tactic + + val THEN: tactic * tactic -> tactic + val ORELSE: tactic * tactic -> tactic + val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic + + val TRY: tactic -> tactic + val EVERY: tactic list -> tactic + val EVERY': ('a -> tactic) list -> 'a -> tactic + val FIRST: tactic list -> tactic + (* ... *) +end +\ + +text\The next layer in the architecture describes @{ML_type \tactic\}'s, i.e. basic operations on +theorems in a backward reasoning style (bottom up development of proof-trees). An initial goal-state +for some property @{term A} --- the \<^emph>\goal\ --- is constructed via the kernel +@{ML "Thm.trivial"}-operation into @{term "A \ A"}, and tactics either refine the premises +--- the \<^emph>\subgoals\ the of this meta-implication --- +producing more and more of them or eliminate them in subsequent goal-states. Subgoals of the form +@{term "B\<^sub>1 \ B\<^sub>2 \ A \ B\<^sub>3 \ B\<^sub>4 \ A"} can be eliminated via +the @{ML Tactic.assume_tac} - tactic, +and a subgoal @{term C\<^sub>m} can be refined via the theorem +@{term "E\<^sub>1 \ E\<^sub>2 \ E\<^sub>3 \ C\<^sub>m"} the @{ML Tactic.resolve_tac} - tactic to new subgoals +@{term "E\<^sub>1"},@{term "E\<^sub>2"}, @{term "E\<^sub>3"}. In case that a theorem used for resolution +has no premise @{term "E\<^sub>i"}, the subgoal @{term C\<^sub>m} is also eliminated ("closed"). + +The following abstract of the most commonly used @{ML_type \tactic\}'s drawn from +@{file "~~/src/Pure/tactic.ML"} looks as follows: +\ + +ML\ + (* ... *) + assume_tac: Proof.context -> int -> tactic; + compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic; + resolve_tac: Proof.context -> thm list -> int -> tactic; + eresolve_tac: Proof.context -> thm list -> int -> tactic; + forward_tac: Proof.context -> thm list -> int -> tactic; + dresolve_tac: Proof.context -> thm list -> int -> tactic; + rotate_tac: int -> int -> tactic; + defer_tac: int -> tactic; + prefer_tac: int -> tactic; + (* ... *) +\ +text\Note that "applying a rule" is a fairly complex operation in the Extended Isabelle Kernel, +i.e. the tactic layer. It involves at least four phases, interfacing a theorem +coming from the global context $\theta$ (=theory), be it axiom or derived, into a given goal-state. +\<^item> \<^emph>\generalization\. All free variables in the theorem were replaced by schematic variables. + For example, @{term "x + y = y + x"} is converted into + @{emph \?x + ?y = ?y + ?x\ }. + By the way, type variables were treated equally. +\<^item> \<^emph>\lifting over assumptions\. If a subgoal is of the form: + @{term "B\<^sub>1 \ B\<^sub>2 \ A"} and we have a theorem @{term "D\<^sub>1 \ D\<^sub>2 \ A"}, then before + applying the theorem, the premisses were \<^emph>\lifted\ resulting in the logical refinement: + @{term "(B\<^sub>1 \ B\<^sub>2 \ D\<^sub>1) \ (B\<^sub>1 \ B\<^sub>2 \ D\<^sub>2) \ A"}. Now, @{ML "resolve_tac"}, for example, + will replace the subgoal @{term "B\<^sub>1 \ B\<^sub>2 \ A"} by the subgoals + @{term "B\<^sub>1 \ B\<^sub>2 \ D\<^sub>1"} and @{term "B\<^sub>1 \ B\<^sub>2 \ D\<^sub>2"}. Of course, if the theorem wouldn't + have assumptions @{term "D\<^sub>1"} and @{term "D\<^sub>2"}, the subgoal @{term "A"} would be replaced by + \<^bold>\nothing\, i.e. deleted. +\<^item> \<^emph>\lifting over parameters\. If a subgoal is meta-quantified like in: + @{term "\ x y z. A x y z"}, then a theorem like @{term "D\<^sub>1 \ D\<^sub>2 \ A"} is \<^emph>\lifted\ + to @{term "\ x y z. D\<^sub>1' \ D\<^sub>2' \ A'"}, too. Since free variables occurring in @{term "D\<^sub>1"}, + @{term "D\<^sub>2"} and @{term "A"} have been replaced by schematic variables (see phase one), + they must be replaced by parameterized schematic variables, i. e. a kind of skolem function. + For example, @{emph \?x + ?y = ?y + ?x\ } would be lifted to + @{emph \!! x y z. ?x x y z + ?y x y z = ?y x y z + ?x x y z\}. This way, the lifted theorem + can be instantiated by the parameters @{term "x y z"} representing "fresh free variables" + used for this sub-proof. This mechanism implements their logically correct bookkeeping via + kernel primitives. +\<^item> \<^emph>\Higher-order unification (of schematic type and term variables)\. + Finally, for all these schematic variables, a solution must be found. + In the case of @{ML resolve_tac}, the conclusion of the (doubly lifted) theorem must + be equal to the conclusion of the subgoal, so @{term A} must be $\alpha/\beta$-equivalent to + @{term A'} in the example above, which is established by a higher-order unification + process. It is a bit unfortunate that for implementation efficiency reasons, a very substantial + part of the code for HO-unification is in the kernel module @{ML_type "thm"}, which makes this + critical component of the architecture larger than necessary. +\ + +text\In a way, the two lifting processes represent an implementation of the conversion between +Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and +Gentzen Sequent Deduction.\ + + +section\The classical goal package\ + +ML\ open Goal; +Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm; + +Goal.prove_global : theory -> string list -> term list -> term -> + ({context: Proof.context, prems: thm list} -> tactic) -> thm +\ + +section\The Isar Engine\ + +text\The main structure of the Isar-engine is @{ ML_structure Toplevel} and provides and +internal @{ ML_type state} with the necessary infrastructure --- +i.e. the operations to pack and unpack theories and Proof.contexts --- on it: +\ +ML\ + Toplevel.theory_toplevel: theory -> Toplevel.state; + Toplevel.init_toplevel: unit -> Toplevel.state; + Toplevel.is_toplevel: Toplevel.state -> bool; + Toplevel.is_theory: Toplevel.state -> bool; + Toplevel.is_proof: Toplevel.state -> bool; + Toplevel.is_skipped_proof: Toplevel.state -> bool; + Toplevel.level: Toplevel.state -> int; + Toplevel.context_of: Toplevel.state -> Proof.context; + Toplevel.generic_theory_of: Toplevel.state -> generic_theory; + Toplevel.theory_of: Toplevel.state -> theory; + Toplevel.proof_of: Toplevel.state -> Proof.state; + Toplevel.presentation_context: Toplevel.state -> Proof.context; + +\ + +subsection \Transaction Management in the Isar-Engine : The Toplevel \ + +ML\ + +Toplevel.exit: Toplevel.transition -> Toplevel.transition; +Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; +Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; +Toplevel.ignored: Position.T -> Toplevel.transition; +Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition; +Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition; +Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition; + +Toplevel.present_local_theory: +(xstring * Position.T) option -> + (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; +(* where text treatment and antiquotation parsing happens *) + + +(*fun document_command markdown (loc, txt) = + Toplevel.keep (fn state => + (case loc of + NONE => ignore (output_text state markdown txt) + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *) + +(* Isar Toplevel Steuerung *) +Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + (* val keep' = add_trans o Keep; + fun keep f = add_trans (Keep (fn _ => f)); + *) + +Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) -> + Toplevel.transition -> Toplevel.transition; + (* fun present_local_theory target = present_transaction (fn int => + (fn Theory (gthy, _) => + let val (finish, lthy) = Named_Target.switch target gthy; + in Theory (finish lthy, SOME lthy) end + | _ => raise UNDEF)); + + fun present_transaction f g = add_trans (Transaction (f, g)); + fun transaction f = present_transaction f (K ()); + *) + +Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition; + (* fun theory' f = transaction (fn int => + (fn Theory (Context.Theory thy, _) => + let val thy' = thy + |> Sign.new_group + |> f int + |> Sign.reset_group; + in Theory (Context.Theory thy', NONE) end + | _ => raise UNDEF)); + + fun theory f = theory' (K f); *) + +\ + + +ML\ + + +(* Isar Toplevel Steuerung *) +Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + (* val keep' = add_trans o Keep; + fun keep f = add_trans (Keep (fn _ => f)); + *) + +Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) -> + Toplevel.transition -> Toplevel.transition; + (* fun present_local_theory target = present_transaction (fn int => + (fn Theory (gthy, _) => + let val (finish, lthy) = Named_Target.switch target gthy; + in Theory (finish lthy, SOME lthy) end + | _ => raise UNDEF)); + + fun present_transaction f g = add_trans (Transaction (f, g)); + fun transaction f = present_transaction f (K ()); + *) + +Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition; + (* fun theory' f = transaction (fn int => + (fn Theory (Context.Theory thy, _) => + let val thy' = thy + |> Sign.new_group + |> f int + |> Sign.reset_group; + in Theory (Context.Theory thy', NONE) end + | _ => raise UNDEF)); + + fun theory f = theory' (K f); *) + + +\ + + +subsection\ Configuration flags of fixed type in the Isar-engine. \ +text\The toplevel also provides an infrastructure for managing configuration options +for system components. Based on a sum-type @{ML_type Config.value } +with the alternatives \<^verbatim>\ Bool of bool | Int of int | Real of real | String of string\ +and building the parametric configuration types @{ML_type "'a Config.T" } and the +instance \<^verbatim>\type raw = value T\, for all registered configurations the protocol: +\ +ML\ + Config.get: Proof.context -> 'a Config.T -> 'a; + Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context; + Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context; + Config.get_global: theory -> 'a Config.T -> 'a; + Config.map_global: 'a Config.T -> ('a -> 'a) -> theory -> theory; + Config.put_global: 'a Config.T -> 'a -> theory -> theory; +\ +text\... etc. is defined.\ + +text\Example registration of an config attribute XS232: \ +ML\ +val (XS232, XS232_setup) + = Attrib.config_bool \<^binding>\XS232\ (K false); + +val _ = Theory.setup XS232_setup; +\ + +(* or: just command: + +setup\XS232_setup\ + +*) + +text\Another mechanism are global synchronised variables:\ +ML\ (* For example *) + +val C = Synchronized.var "Pretty.modes" "latEEex"; +(* Synchronized: a mechanism to bookkeep global + variables with synchronization mechanism included *) +Synchronized.value C; +\ + +chapter\Front-End \ +text\In the following chapter, we turn to the right part of the system architecture +shown in @{docitem \architecture\}: +The PIDE ("Prover-IDE") layer consisting of a part written in SML and another in SCALA. +Roughly speaking, PIDE implements "continuous build - continuous check" - functionality +over a textual, albeit generic document model. It transforms user modifications +of text elements in an instance of this model into increments (edits) and communicates +them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight +reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text +elements. Such markup is used to highlight, e.g., variables +or keywords with specific colors, to hyper-linking bound variables to their defining occurrences, +or to annotate type-information to terms which becomes displayed by specific +user-gestures on demand (hovering), etc. +Note that PIDE is not an editor, it is the framework that +coordinates these asynchronous information streams and optimizes it to a certain +extent (outdated markup referring to modified text is dropped, and +corresponding re-calculations are oriented to the user focus, for example). +Four concrete editors --- also called PIDE applications --- have been implemented: +\<^enum>an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version), +\<^enum>a Visual-Studio Code plugin (developed by Makarius Wenzel), + currently based on a fairly old PIDE version, +\<^enum>clide, a web-client supporting javascript and HTML5 + (developed by a group at University Bremen, based on a very old PIDE version), and +\<^enum>the most commonly used: the plugin in JEdit - Editor, + (developed by Makarius Wenzel, current PIDE version.) +\ + +text\The document model forsees a number of text files, which are organized in form of an acyclic graph. Such graphs can be +grouped into \<^emph>\sessions\ and "frozen" to binaries in order to avoid long compilation +times. Text files have an abstract name serving as identity (the mapping to file-paths +in an underlying file-system is done in an own build management). +The primary format of the text files is \<^verbatim>\.thy\ (historically for: theory), +secondary formats can be \<^verbatim>\.sty\,\<^verbatim>\.tex\, \<^verbatim>\.png\, \<^verbatim>\.pdf\, or other files processed +by Isabelle and listed in a configuration processed by the build system. +\ +figure*[fig3::figure, relative_width="100",src="''figures/document-model''"] + \A Theory-Graph in the Document Model\ +text\A \<^verbatim>\.thy\ file consists of a \<^emph>\header\, a \<^emph>\context-definition\ and +a \<^emph>\body\ consisting of a sequence of \<^emph>\commands\. Even the header consists of +a sequence of commands used for introductory text elements not depending on any context +information (so: practically excluding any form of text antiquotation (see above)). +The context-definition contains an \<^emph>\import\ and a \<^emph>\keyword\ section; +for example: +\begin{verbatim} +theory Isa_DOF (* Isabelle Document Ontology Framework *) + imports Main + RegExpInterface (* Interface to functional regular automata for monitoring *) + Assert + + keywords "+=" ":=" "accepts" "rejects" +\end{verbatim} +where \<^verbatim>\Isa_DOF\ is the abstract name of the text-file, \<^verbatim>\Main\ etc. refer to imported +text files (recall that the import relation must be acyclic). \<^emph>\keyword\s are used to separate +commands form each other; +predefined commands allow for the dynamic creation of new commands similarly +to the definition of new functions in an interpreter shell (or: toplevel, see above.). +A command starts with a pre-declared keyword and specific syntax of this command; +the declaration of a keyword is only allowed in the same \<^verbatim>\.thy\-file where the +the corresponding new command is defined. The semantics of the command is expressed +in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"} +function. Thus, the Isar-toplevel supports the generic document model +and allows for user-programmed extensions. +\ + +text\In the traditional literature, Isabelle \<^verbatim>\.thy\-files were +were said to be processed by processed by two types of parsers: +\<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed + by a lexer-library and parser combinators built on top, and +\<^enum> the "inner-syntax" (i.e. the syntax for @{term \\\} - terms) + with an evolved, eight-layer parsing and pretty-printing process + based on an Early-algorithm. +\ + +text\This picture is less and less true for a number of reasons: +\<^enum> With the advent of \(\)... (\)\, a mechanism for + \<^emph>\cascade-syntax\ came to the Isabelle platform that introduce a flexible means + to change parsing contexts \<^emph>\and\ parsing technologies. +\<^enum> Inside the term-parser levels, the concept of \<^emph>\cartouche\ can be used + to escape the parser and its underlying parsing technology. +\<^enum> Outside, in the traditional toplevel-parsers, the + \(\)... (\)\ is becoming more and more enforced + (some years ago, syntax like \term{* ... *}\ was replaced by + syntax \term(\)... (\)\. This makes technical support of cascade syntax + more and more easy. +\<^enum> The Lexer infra-structure is already rather generic; nothing prevents to + add beside the lexer - configurations for ML-Parsers, Toplevel Command Syntax + parsers, mathematical notation parsers for $\lambda$-terms new pillars + of parsing technologies, say, for parsing C or Rust or JavaScript inside + Isabelle. +\ + + +section\Basics: string, bstring and xstring\ +text\@{ML_type "string"} is the basic library type from the SML library +in structure @{ML_structure "String"}. Many Isabelle operations produce +or require formats thereof introduced as type synonyms +@{ML_type "bstring"} (defined in structure @{ML_structure "Binding"} +and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}. +Unfortunately, the abstraction is not tight and combinations with +elementary routines might produce quite crappy results. +\ + +ML\val b = Binding.name_of@{binding "here"}\ +text\... produces the system output \verb+val it = "here": bstring+, + but note that it is misleading to believe it is just a string. +\ + +ML\String.explode b\ (* is harmless, but *) +ML\String.explode(Binding.name_of +(Binding.conglomerate[Binding.qualified_name "X.x", + @{binding "here"}] ))\ +(* Somehow it is possible to smuggle markup into bstrings; and this leads + ML\(((String.explode(!ODL_Command_Parser.SPY6))))\ + to something like + val it = [#"\^E", #"\^F", #"i", #"n", #"p", #"u", #"t", #"\^F", #"d", #"e", #"l", #"i", #"m", #"i", #"t", #"e", #"d", #"=", #"f", #"a", ...]: char list +*) + +text\ However, there is an own XML parser for this format. See Section Markup. +\ +ML\ fun dark_matter x = XML.content_of (YXML.parse_body x)\ + +(* MORE TO COME *) + +section\Positions\ +text\A basic data-structure relevant for PIDE are \<^emph>\positions\; beyond the usual line- and column +information they can represent ranges, list of ranges, and the name of the atomic sub-document +in which they are contained. In the command:\ +ML\ +val pos = @{here}; +val markup = Position.here pos; +writeln ("And a link to the declaration of 'here' is "^markup) +\ +(* \<^here> *) +text\ ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position +of itself in the global document, converts it to markup (a string-representation of it) and sends +it via the usual @{ML "writeln"} to the interface. \ + +figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"] +\Output with hyperlinked position.\ + +text\@{docitem \hyplinkout\} shows the produced output where the little house-like symbol in the +display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\ + +section\Markup and Low-level Markup Reporting\ +text\The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic +annotation data which is part of the protocol sent from Isabelle to the frontend. +They are qualified as "quasi-abstract", which means they are intended to be an abstraction of +the serialized, textual presentation of the protocol. Markups are structurally a pair of a key +and properties; @{ML_structure Markup} provides a number of of such \<^emph>\key\s for annotation classes +such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample +from \<^theory_text>\Isabelle_DOF\. A markup must be tagged with an id; this is done by the @{ML serial}-function +discussed earlier.\ +subsection\A simple Example\ +ML\ +local + +val docclassN = "doc_class"; + +(* derived from: theory_markup; def for "defining occurrence" (true) in contrast to + "referring occurence" (false). *) +fun docclass_markup def name id pos = + if id = 0 then Markup.empty + else Markup.properties (Position.entity_properties_of def id pos) + (Markup.entity docclassN name); + +in + +fun report_defining_occurrence pos cid = + let val id = serial () + val markup_of_cid = docclass_markup true cid id pos + in Position.report pos markup_of_cid end; + +end +\ + +text\The @\ML report_defining_occurrence\-function above takes a position and a "cid" parsed +in the Front-End, converts this into markup together with a unique number identifying this +markup, and sends this as a report to the Front-End. \ + + +subsection\A Slightly more Complex Example\ + +ML \ + +fun markup_tvar def_name ps (name, id) = + let + fun markup_elem name = (name, (name, []): Markup.T); + val (tvarN, tvar) = markup_elem ((case def_name of SOME name => name | _ => "") ^ "'s nickname is"); + val entity = Markup.entity tvarN name + val def = def_name = NONE + in + tvar :: + (if def then I else cons (Markup.keyword_properties Markup.ML_keyword3)) + (map (fn pos => Markup.properties (Position.entity_properties_of def id pos) entity) ps) + end + +fun report [] _ _ = I + | report ps markup x = + let val ms = markup x + in fold (fn p => fold (fn m => cons ((p, m), "")) ms) ps end +\ + +ML \ +local +val data = \ \Derived from Yakoub's example ;-)\ + + [ (\Frédéric 1er\, \King of Naples\) + , (\Frédéric II\, \King of Sicily\) + , (\Frédéric III\, \the Handsome\) + , (\Frédéric IV\, \of the Empty Pockets\) + , (\Frédéric V\, \King of Denmark–Norway\) + , (\Frédéric VI\, \the Knight\) + , (\Frédéric VII\, \Count of Toggenburg\) + , (\Frédéric VIII\, \Count of Zollern\) + , (\Frédéric IX\, \the Old\) + , (\Frédéric X\, \the Younger\) ] + +val (tab0, markup) = + fold_map (fn (name, msg) => fn reports => + let val id = serial () + val pos = [Input.pos_of name] + in + ( (fst(Input.source_content msg), (name, pos, id)) + , report pos (markup_tvar NONE pos) (fst(Input.source_content name), id) reports) + end) + data + [] + +val () = Position.reports_text markup +in +val tab = Symtab.make tab0 +end +\ + +ML \ +val _ = + fold (fn input => + let + val pos1' = Input.pos_of input + fun ctnt name0 = fst(Input.source_content name0) + val pos1 = [pos1'] + val msg1 = fst(Input.source_content input) + val msg2 = "No persons were found to have such nickname" + in + case Symtab.lookup tab (fst(Input.source_content input)) of + NONE => tap (fn _ => Output.information (msg2 ^ Position.here_list pos1)) + (cons ((pos1', Markup.bad ()), "")) + | SOME (name0, pos0, id) => report pos1 (markup_tvar (SOME (ctnt name0)) pos0) (msg1, id) + end) + [ \the Knight\ \ \Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\ + , \the Handsome\ \ \Example of a correct retrieval (CTRL + Hovering shows what we are expecting)\ + , \the Spy\ \ \Example of a failure to retrieve the person in \<^ML>\tab\\ + ] + [] + |> Position.reports_text +\ + +text\The pudding comes with the eating: \ + +subsection\Environment Structured Reporting\ + +text\ The structure @{ML_structure \Name_Space\} offers an own infra-structure for names and +manages the markup accordingly. MORE TO COME\ +text\ @{ML_type "'a Name_Space.table"} \ + + +section\ The System Lexer and Token Issues\ +text\Four syntactic contexts are predefined in Isabelle (others can be added): +the ML context, the text context, the Isar-command context and the teerm-context, referring +to different needs of the Isabelle Framework as an extensible framework supporting incremental, +partially programmable extensions and as a Framework geared towards Formal Proofs and therefore +mathematical notations. The basic data-structure for the lexical treatment of these + +\ + +subsection\Tokens\ + +text\The basic entity that lexers treat are \<^emph>\tokens\. defined in @{ML_structure "Token"} +It provides a classification infrastructure, the references to positions and Markup +as well as way's to annotate tokens with (some) values they denote: +\ + +ML\ +local + open Token + + type dummy = Token.T + type src = Token.T list + type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T} + + type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring} + + + val _ = Token.is_command : Token.T -> bool; + val _ = Token.content_of : Token.T -> string; (* textueller kern eines Tokens. *) + + + val _ = pos_of: T -> Position.T + +(* +datatype kind = + (*immediate source*) + Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat | + Float | Space | + (*delimited content*) + String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option | + (*special content*) + Error of string | EOF + + datatype value = + Source of src | + Literal of bool * Markup.T | + Name of name_value * morphism | + Typ of typ | + Term of term | + Fact of string option * thm list | + Attribute of morphism -> attribute | + Declaration of declaration | + Files of file Exn.result list + + +*) +in val _ = () +end +\ + + + +subsection\A Lexer Configuration Example\ + +ML\ + +\ + + +section\ Combinator Parsing \ +text\Parsing Combinators go back to monadic programming as advocated by Wadler et. al, and has been +worked out @{cite "DBLP:journals/jfp/Hutton92"}. Parsing combinators are one of the two +major parsing technologies of the Isabelle front-end, in particular for the outer-syntax used +for the parsing of toplevel-commands. The core of the combinator library is +@{ML_structure \Scan\} providing the @{ML_type "'a parser"} which is a synonym for +@{ML_type " Token.T list -> 'a * Token.T list"}. The library also provides a bunch of +infix parsing combinators, notably:\ + +ML\ + val _ = op !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b + (*apply function*) + val _ = op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c + (*alternative*) + val _ = op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b + (*sequential pairing*) + val _ = op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e + (*dependent pairing*) + val _ = op :-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e + (*projections*) + val _ = op :|-- : ('a -> 'b * 'c) * ('b -> 'c -> 'd * 'e) -> 'a -> 'd * 'e + val _ = op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e + val _ = op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e + (*concatenation*) + val _ = op ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c + val _ = op ::: : ('a -> 'b * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd + val _ = op @@@ : ('a -> 'b list * 'c) * ('c -> 'b list * 'd) -> 'a -> 'b list * 'd + (*one element literal*) + val _ = op $$ : string -> string list -> string * string list + val _ = op ~$$ : string -> string list -> string * string list + \ + +text\Usually, combinators were used in one of these following instances:\ + +ML\ + + type 'a parser = Token.T list -> 'a * Token.T list + type 'a context_parser = Context.generic * Token.T list -> 'a * (Context.generic * Token.T list) + + +(* conversion between these two : *) + +fun parser2contextparser pars (ctxt, toks) = let val (a, toks') = pars toks + in (a,(ctxt, toks')) end; +val _ = parser2contextparser : 'a parser -> 'a context_parser; + +(* bah, is the same as Scan.lift *) +val _ = Scan.lift Args.cartouche_input : Input.source context_parser; + + +\ + +subsection\ Bindings \ + + +ML\ +val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position, + where \positions\ are absolute references to a file *) + +Binding.make: bstring * Position.T -> binding; +Binding.pos_of @{binding erzerzer}; +Position.here: Position.T -> string; +(* Bindings *) +ML\val X = @{here};\ + +\ + +subsection \Input streams. \ +ML\ + Input.source_explode : Input.source -> Symbol_Pos.T list; + (* conclusion: Input.source_explode converts " f @{thm refl}" + into: + [(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}), + ("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}), + ("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}), + ("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}), + ("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})] + *)\ + +subsection \Scanning and combinator parsing. \ +text\Is used on two levels: +\<^enum> outer syntax, that is the syntax in which Isar-commands are written, and +\<^enum> inner-syntax, that is the syntax in which lambda-terms, and in particular HOL-terms were written. +\ +text\ A constant problem for newbies is this distinction, which makes it necessary that + the " ... " quotes have to be used when switching to inner-syntax, except when only one literal + is expected when an inner-syntax term is expected. +\ + +ML\ +Scan.peek : ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd); +Scan.optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a; +Scan.option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a; +Scan.repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a; +Scan.lift : ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c); +Scan.lift (Parse.position Args.cartouche_input); +\ + +text\ "parsers" are actually interpreters; an 'a parser is a function that parses + an input stream and computes(=evaluates, computes) it into 'a. + Since the semantics of an Isabelle command is a transition => transition + or theory $\Rightarrow$ theory function, i.e. a global system transition. + parsers of that type can be constructed and be bound as call-back functions + to a table in the Toplevel-structure of Isar. + + The type 'a parser is already defined in the structure Token. +\ + +text\ Syntax operations : Interface for parsing, type-checking, "reading" + (both) and pretty-printing. + Note that this is a late-binding interface, i.e. a collection of "hooks". + The real work is done ... see below. + + Encapsulates the data structure "syntax" --- the table with const symbols, + print and ast translations, ... The latter is accessible, e.g. from a Proof + context via @{ML Proof_Context.syn_of}. +\ + +ML\ +Parse.nat: int parser; +Parse.int: int parser; +Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser; +Parse.enum: string -> 'a parser -> 'a list parser; +Parse.input: 'a parser -> Input.source parser; + +Parse.enum : string -> 'a parser -> 'a list parser; +Parse.!!! : (Token.T list -> 'a) -> Token.T list -> 'a; +Parse.position: 'a parser -> ('a * Position.T) parser; + +(* Examples *) +Parse.position Args.cartouche_input; +\ + +text\ Inner Syntax Parsing combinators for elementary Isabelle Lexems\ +ML\ +Syntax.parse_sort : Proof.context -> string -> sort; +Syntax.parse_typ : Proof.context -> string -> typ; +Syntax.parse_term : Proof.context -> string -> term; +Syntax.parse_prop : Proof.context -> string -> term; +Syntax.check_term : Proof.context -> term -> term; +Syntax.check_props: Proof.context -> term list -> term list; +Syntax.uncheck_sort: Proof.context -> sort -> sort; +Syntax.uncheck_typs: Proof.context -> typ list -> typ list; +Syntax.uncheck_terms: Proof.context -> term list -> term list;\ + +text\In contrast to mere parsing, the following operators provide also type-checking + and internal reporting to PIDE --- see below. I did not find a mechanism to address + the internal serial-numbers used for the PIDE protocol, however, rumours have it + that such a thing exists. The variants \<^verbatim>\_global\ work on theories instead on + @{ML_type "Proof.context"}s.\ + +ML\ +Syntax.read_sort: Proof.context -> string -> sort; +Syntax.read_typ : Proof.context -> string -> typ; +Syntax.read_term: Proof.context -> string -> term; +Syntax.read_typs: Proof.context -> string list -> typ list; +Syntax.read_sort_global: theory -> string -> sort; +Syntax.read_typ_global: theory -> string -> typ; +Syntax.read_term_global: theory -> string -> term; +Syntax.read_prop_global: theory -> string -> term; +\ +text \The following operations are concerned with the conversion of pretty-prints +and, from there, the generation of (non-layouted) strings.\ +ML\ +Syntax.pretty_term:Proof.context -> term -> Pretty.T; +Syntax.pretty_typ:Proof.context -> typ -> Pretty.T; +Syntax.pretty_sort:Proof.context -> sort -> Pretty.T; +Syntax.pretty_classrel: Proof.context -> class list -> Pretty.T; +Syntax.pretty_arity: Proof.context -> arity -> Pretty.T; +Syntax.string_of_term: Proof.context -> term -> string; +Syntax.string_of_typ: Proof.context -> typ -> string; +Syntax.lookup_const : Syntax.syntax -> string -> string option; +\ + +ML\ +fun read_terms ctxt = + grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt; +\ + +ML\ +(* More High-level, more Isar-specific Parsers *) +Args.name; +Args.const; +Args.cartouche_input: Input.source parser; +Args.text_token: Token.T parser; + +val Z = let val attribute = Parse.position Parse.name -- + Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; + in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ; +(* this leads to constructions like the following, where a parser for a *) + + + +Thy_Output.antiquotation_pretty_source \<^binding>\theory\ (Scan.lift (Parse.position Args.embedded)); + +Thy_Output.antiquotation_raw \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) ; + +fn name => (Thy_Output.antiquotation_pretty_source name (Scan.lift (Parse.position Args.cartouche_input))); +\ + + +section\ The PIDE Framework \ +subsection\ Markup \ +text\ Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR. + Markup operation send via side-effect annotations to the GUI (precisely: + to the PIDE Framework) that were used for hyperlinking applicating to binding + occurrences, info for hovering, ... \ +ML\ + +(* Position.report is also a type consisting of a pair of a position and markup. *) +(* It would solve all my problems if I find a way to infer the defining Position.report + from a type definition occurence ... *) + +Position.report: Position.T -> Markup.T -> unit; +Position.reports: Position.report list -> unit; + (* ? ? ? I think this is the magic thing that sends reports to the GUI. *) +Markup.entity : string -> string -> Markup.T; +Markup.properties : Properties.T -> Markup.T -> Markup.T ; +Properties.get : Properties.T -> string -> string option; +Markup.enclose : Markup.T -> string -> string; + +(* example for setting a link, the def flag controls if it is a defining or a binding +occurence of an item *) +fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) = + if id = 0 then Markup.empty + else + Markup.properties (Position.entity_properties_of def id pos) + (Markup.entity Markup.theoryN name); +Markup.theoryN : string; + +serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers, + be it on the level of thy-internal states or as reference in markup in + PIDE *) + +(* From Theory: +fun check ctxt (name, pos) = + let + val thy = Proof_Context.theory_of ctxt; + val thy' = + Context.get_theory thy name + handle ERROR msg => + let + val completion = + Completion.make (name, pos) + (fn completed => + map Context.theory_name (ancestors_of thy) + |> filter completed + |> sort_strings + |> map (fn a => (a, (Markup.theoryN, a)))); + val report = Markup.markup_report (Completion.reported_text completion); + in error (msg ^ Position.here pos ^ report) end; + val _ = Context_Position.report ctxt pos (get_markup thy'); + in thy' end; + +fun init_markup (name, pos) thy = + let + val id = serial (); + val _ = Position.report pos (theory_markup true name id pos); + in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; + +fun get_markup thy = + let val {pos, id, ...} = rep_theory thy + in theory_markup false (Context.theory_name thy) id pos end; + + +*) + +(* +fun theory_markup def thy_name id pos = + if id = 0 then Markup.empty + else + Markup.properties (Position.entity_properties_of def id pos) + (Markup.entity Markup.theoryN thy_name); + +fun get_markup thy = + let val {pos, id, ...} = rep_theory thy + in theory_markup false (Context.theory_name thy) id pos end; + + +fun init_markup (name, pos) thy = + let + val id = serial (); + val _ = Position.report pos (theory_markup true name id pos); + in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; + + +fun check ctxt (name, pos) = + let + val thy = Proof_Context.theory_of ctxt; + val thy' = + Context.get_theory thy name + handle ERROR msg => + let + val completion = + Completion.make (name, pos) + (fn completed => + map Context.theory_name (ancestors_of thy) + |> filter completed + |> sort_strings + |> map (fn a => (a, (Markup.theoryN, a)))); + val report = Markup.markup_report (Completion.reported_text completion); + in error (msg ^ Position.here pos ^ report) end; + val _ = Context_Position.report ctxt pos (get_markup thy'); + in thy' end; + + +*) + +\ + + + +section \ Output: Very Low Level \ +ML\ +Output.output; (* output is the structure for the "hooks" with the target devices. *) +Output.output "bla_1:"; +\ + +section \ Output: LaTeX \ + + +ML\ open Thy_Output; + + output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list; + output_token: Proof.context -> Token.T -> Latex.text list; + output_source: Proof.context -> string -> Latex.text list; + present_thy: Options.T -> theory -> segment list -> Latex.text list; + pretty_term: Proof.context -> term -> Pretty.T; + pretty_thm: Proof.context -> thm -> Pretty.T; + lines: Latex.text list -> Latex.text list; + items: Latex.text list -> Latex.text list; + isabelle: Proof.context -> Latex.text list -> Latex.text; + isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text; + typewriter: Proof.context -> string -> Latex.text; + verbatim: Proof.context -> string -> Latex.text; + source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text; + pretty: Proof.context -> Pretty.T -> Latex.text; + pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text; + pretty_items: Proof.context -> Pretty.T list -> Latex.text; + pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text; + antiquotation_pretty: + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; + antiquotation_pretty_source: + binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; + antiquotation_raw: + binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory; + antiquotation_verbatim: + binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory; + +\ + + + +ML\ +Syntax_Phases.reports_of_scope; +\ + +(* STOP HERE JUNK ZONE : + +(* Pretty.T, pretty-operations. *) +ML\ + +(* interesting piece for LaTeX Generation: +fun verbatim_text ctxt = + if Config.get ctxt display then + split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #> + Latex.output_ascii #> Latex.environment "isabellett" + else + split_lines #> + map (Latex.output_ascii #> enclose "\\isatt{" "}") #> + space_implode "\\isasep\\isanewline%\n"; + +(* From structure Thy_Output *) +fun pretty_const ctxt c = + let + val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) + handle TYPE (msg, _, _) => error msg; + val ([t'], _) = Variable.import_terms true [t] ctxt; + in pretty_term ctxt t' end; + + basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #> + +*) + +Pretty.enclose : string -> string -> Pretty.T list -> Pretty.T; (* not to confuse with: String.enclose *) + +(* At times, checks where attached to Pretty - functions and exceptions used to + stop the execution/validation of a command *) +fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); +Pretty.enclose; +Pretty.str; +Pretty.mark_str; +Pretty.text "bla_d"; + +Pretty.quote; (* Pretty.T transformation adding " " *) +Pretty.unformatted_string_of : Pretty.T -> string ; + +Latex.output_ascii; +Latex.environment "isa" "bg"; +Latex.output_ascii "a_b:c'é"; +(* Note: *) +space_implode "sd &e sf dfg" ["qs","er","alpa"]; + + +(* +fun pretty_command (cmd as (name, Command {comment, ...})) = + Pretty.block + (Pretty.marks_str + ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]}, + command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); +*) + + +\ + +ML\ +Thy_Output.output_text; +(* is: +fun output_text state {markdown} source = + let + val is_reported = + (case try Toplevel.context_of state of + SOME ctxt => Context_Position.is_visible ctxt + | NONE => true); + + val pos = Input.pos_of source; + val syms = Input.source_explode source; + + val _ = + if is_reported then + Position.report pos (Markup.language_document (Input.is_delimited source)) + else (); + + val output_antiquotes = map (eval_antiquote state) #> implode; + + fun output_line line = + (if Markdown.line_is_item line then "\\item " else "") ^ + output_antiquotes (Markdown.line_content line); + + fun output_blocks blocks = space_implode "\n\n" (map output_block blocks) + and output_block (Markdown.Par lines) = cat_lines (map output_line lines) + | output_block (Markdown.List {kind, body, ...}) = + Latex.environment (Markdown.print_kind kind) (output_blocks body); + in + if Toplevel.is_skipped_proof state then "" + else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms + then + let + val ants = Antiquote.parse pos syms; + val reports = Antiquote.antiq_reports ants; + val blocks = Markdown.read_antiquotes ants; + val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else (); + in output_blocks blocks end + else + let + val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms); + val reports = Antiquote.antiq_reports ants; + val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else (); + in output_antiquotes ants end + end; +*) + +\ + + +ML\ +Outer_Syntax.print_commands @{theory}; + +Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> + (Toplevel.transition -> Toplevel.transition) parser -> unit; +(* creates an implicit thy_setup with an entry for a call-back function, which happens + to be a parser that must have as side-effect a Toplevel-transition-transition. + Registers "Toplevel.transition -> Toplevel.transition" parsers to the Isar interpreter. + *) + +(*Example: text is : + +val _ = + Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" + (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true}); +*) + +(* not exported: Thy_Output.output_token; Ich glaub, da passierts ... *) +Thy_Output.present_thy; +\ + +text\ Even the parsers and type checkers stemming from the theory-structure are registered via +hooks (this can be confusing at times). Main phases of inner syntax processing, with standard +implementations of parse/unparse operations were treated this way. +At the very very end in @{file "~~/src/Pure/Syntax/syntax_phases.ML"}, it sets up the entire syntax engine +(the hooks) via: +\ + + +(* +val _ = + Theory.setup + (Syntax.install_operations + {parse_sort = parse_sort, + parse_typ = parse_typ, + parse_term = parse_term false, + parse_prop = parse_term true, + unparse_sort = unparse_sort, + unparse_typ = unparse_typ, + unparse_term = unparse_term, + check_typs = check_typs, + check_terms = check_terms, + check_props = check_props, + uncheck_typs = uncheck_typs, + uncheck_terms = uncheck_terms}); +*) + +text\ Thus, Syntax\_Phases does the actual work, including + markup generation and generation of reports. Look at: \ +(* +fun check_typs ctxt raw_tys = + let + val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys; + val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else (); + in + tys + |> apply_typ_check ctxt + |> Term_Sharing.typs (Proof_Context.theory_of ctxt) + end; + +which is the real implementation behind Syntax.check_typ + +or: + +fun check_terms ctxt raw_ts = + let + val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts; + val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts'; + + val tys = map (Logic.mk_type o snd) ps; + val (ts', tys') = ts @ tys + |> apply_term_check ctxt + |> chop (length ts); + val typing_report = + fold2 (fn (pos, _) => fn ty => + if Position.is_reported pos then + cons (Position.reported_text pos Markup.typing + (Syntax.string_of_typ ctxt (Logic.dest_type ty))) + else I) ps tys' []; + + val _ = + if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report) + else (); + in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end; + +which is the real implementation behind Syntax.check_term + +As one can see, check-routines internally generate the markup. + +*) + + + +Consts.the_const; (* T is a kind of signature ... *) +Variable.import_terms; +Vartab.update; + +fun control_antiquotation name s1 s2 = + Thy_Output.antiquotation name (Scan.lift Args.cartouche_input) + (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false}); + +Output.output; + +Syntax.read_input ; +Input.source_content; + +(* + basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #> +*) + + + + +chapter\LaTeX Document Generation\ +text\MORE TO COME\ + + +ML\ Thy_Output.document_command {markdown = true} \ +(* Structures related to LaTeX Generation *) +ML\ Latex.output_ascii; + + Latex.output_token +(* Hm, generierter output for +subsection*[Shaft_Encoder_characteristics]{ * Shaft Encoder Characteristics * } : + +\begin{isamarkuptext}% +\isa{{\isacharbackslash}label{\isacharbraceleft}general{\isacharunderscore}hyps{\isacharbraceright}}% +\end{isamarkuptext}\isamarkuptrue% +\isacommand{subsection{\isacharasterisk}}\isamarkupfalse% +{\isacharbrackleft}Shaft{\isacharunderscore}Encoder{\isacharunderscore}characteristics{\isacharbrackright}{\isacharverbatimopen}\ Shaft\ Encoder\ Characteristics\ {\isacharverbatimclose}% + +Generierter output for: text\\label{sec:Shaft-Encoder-characteristics}\ + +\begin{isamarkuptext}% +\label{sec:Shaft-Encoder-characteristics}% +\end{isamarkuptext}\isamarkuptrue% + + +*) + + +\ + +ML\ +Thy_Output.maybe_pretty_source : + (Proof.context -> 'a -> Pretty.T) -> Proof.context -> Token.src -> 'a list -> Pretty.T list; + +Thy_Output.output: Proof.context -> Pretty.T list -> string; + + (* nuescht besonderes *) + +fun document_antiq check_file ctxt (name, pos) = + let + (* val dir = master_directory (Proof_Context.theory_of ctxt); *) + (* val _ = check_path check_file ctxt dir (name, pos); *) + in + space_explode "/" name + |> map Latex.output_ascii + |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}") + |> enclose "\\isatt{" "}" + end; + +\ + +ML\ + +Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string; +Thy_Output.document_command; + +Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source -> + Toplevel.transition -> Toplevel.transition; + (* fun document_command markdown (loc, txt) = + Toplevel.keep (fn state => + (case loc of + NONE => ignore (output_text state markdown txt) + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); + + *) + +Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ; + (* this is where antiquotation expansion happens : uses eval_antiquote *) + + +Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source -> + Toplevel.transition -> Toplevel.transition; + (* fun document_command markdown (loc, txt) = + Toplevel.keep (fn state => + (case loc of + NONE => ignore (output_text state markdown txt) + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); + + *) + +Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ; + (* this is where antiquotation expansion happens : uses eval_antiquote *) + +*) +(* stuff over global environment : *) +(* +ML\ Document.state();\ +ML\ Session.get_keywords(); (* this looks to be really session global. *) + Outer_Syntax.command; \ +ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \ +*) + + +section\Inner Syntax\ +text\MORE TO COME\ +ML\Sign.add_trrules\ + + +section*[c::conclusion]\Conclusion\ +text\More to come\ +section*[bib::bibliography]\Bibliography\ + +(*<*) +close_monitor*[this] +check_doc_global +(*>*) +end diff --git a/examples/technical_report/TR_my_commented_isabelle/document/root.bib b/examples/technical_report/TR_my_commented_isabelle/document/root.bib new file mode 100644 index 00000000..4eca4be6 --- /dev/null +++ b/examples/technical_report/TR_my_commented_isabelle/document/root.bib @@ -0,0 +1,528 @@ +@misc{bockenek:hal-02069705, + TITLE = {{Using Isabelle/UTP for the Verification of Sorting Algorithms A Case Study}}, + AUTHOR = {Bockenek, Joshua A and Lammich, Peter and Nemouchi, Yakoub and Wolff, Burkhart}, + URL = {https://easychair.org/publications/preprint/CxRV}, + NOTE = {Isabelle Workshop 2018, Colocated with Interactive Theorem Proving. As part of FLOC 2018, Oxford, GB.}, + YEAR = {2018}, + MONTH = Jul +} + +@book{DBLP:books/sp/NipkowPW02, + author = {Tobias Nipkow and + Lawrence C. Paulson and + Markus Wenzel}, + title = {Isabelle/HOL - {A} Proof Assistant for Higher-Order Logic}, + series = {Lecture Notes in Computer Science}, + volume = {2283}, + publisher = {Springer}, + year = {2002}, + url = {https://doi.org/10.1007/3-540-45949-9}, + deactivated_doi = {10.1007/3-540-45949-9}, + isbn = {3-540-43376-7}, + timestamp = {Tue, 14 May 2019 10:00:35 +0200}, + biburl = {https://dblp.org/rec/bib/books/sp/NipkowPW02}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/sosp/KleinEHACDEEKNSTW09, + author = {Gerwin Klein and + Kevin Elphinstone and + Gernot Heiser and + June Andronick and + David Cock and + Philip Derrin and + Dhammika Elkaduwe and + Kai Engelhardt and + Rafal Kolanski and + Michael Norrish and + Thomas Sewell and + Harvey Tuch and + Simon Winwood}, + title = {seL4: formal verification of an {OS} kernel}, + deactivated_booktitle = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles + 2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009}, + pages = {207--220}, + year = {2009}, + crossref = {DBLP:conf/sosp/2009}, + url = {https://doi.org/10.1145/1629575.1629596}, + deactivated_doi = {10.1145/1629575.1629596}, + timestamp = {Tue, 06 Nov 2018 16:59:32 +0100}, + biburl = {https://dblp.org/rec/bib/conf/sosp/KleinEHACDEEKNSTW09}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:conf/sosp/2009, + editor = {Jeanna Neefe Matthews and + Thomas E. Anderson}, + title = {Proceedings of the 22nd {ACM} Symposium on Operating Systems Principles + 2009, {SOSP} 2009, Big Sky, Montana, USA, October 11-14, 2009}, + publisher = {{ACM}}, + year = {2009}, + url = {https://doi.org/10.1145/1629575}, + deactivated_doi = {10.1145/1629575}, + isbn = {978-1-60558-752-3}, + timestamp = {Tue, 06 Nov 2018 16:59:32 +0100}, + biburl = {https://dblp.org/rec/bib/conf/sosp/2009}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/tphol/CohenDHLMSST09, + author = {Ernie Cohen and + Markus Dahlweid and + Mark A. Hillebrand and + Dirk Leinenbach and + Michal Moskal and + Thomas Santen and + Wolfram Schulte and + Stephan Tobies}, + title = {{VCC:} {A} Practical System for Verifying Concurrent {C}}, + deactivated_booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, + TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, + pages = {23--42}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-03359-9_2}, + deactivated_doi = {10.1007/978-3-642-03359-9_2}, + timestamp = {Tue, 23 May 2017 01:12:08 +0200}, + biburl = {https://dblp.org/rec/bib/conf/tphol/CohenDHLMSST09}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/cacm/Leroy09, + author = {Xavier Leroy}, + title = {Formal verification of a realistic compiler}, + journal = {Commun. {ACM}}, + volume = {52}, + number = {7}, + pages = {107--115}, + year = {2009}, + url = {http://doi.acm.org/10.1145/1538788.1538814}, + deactivated_doi = {10.1145/1538788.1538814}, + timestamp = {Thu, 02 Jul 2009 13:36:32 +0200}, + biburl = {https://dblp.org/rec/bib/journals/cacm/Leroy09}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/itp/Wenzel14, + author = {Makarius Wenzel}, + title = {Asynchronous User Interaction and Tool Integration in Isabelle/PIDE}, + deactivated_booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP} + 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, + Austria, July 14-17, 2014. Proceedings}, + pages = {515--530}, + year = {2014}, + crossref = {DBLP:conf/itp/2014}, + url = {https://doi.org/10.1007/978-3-319-08970-6\_33}, + deactivated_doi = {10.1007/978-3-319-08970-6\_33}, + timestamp = {Tue, 14 May 2019 10:00:37 +0200}, + biburl = {https://dblp.org/rec/bib/conf/itp/Wenzel14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:conf/itp/2014, + editor = {Gerwin Klein and + Ruben Gamboa}, + title = {Interactive Theorem Proving - 5th International Conference, {ITP} + 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, + Austria, July 14-17, 2014. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {8558}, + publisher = {Springer}, + year = {2014}, + url = {https://doi.org/10.1007/978-3-319-08970-6}, + deactivated_doi = {10.1007/978-3-319-08970-6}, + isbn = {978-3-319-08969-0}, + timestamp = {Tue, 14 May 2019 10:00:37 +0200}, + biburl = {https://dblp.org/rec/bib/conf/itp/2014}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:journals/corr/Wenzel14, + author = {Makarius Wenzel}, + title = {System description: Isabelle/jEdit in 2014}, + deactivated_booktitle = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, + {UITP} 2014, Vienna, Austria, 17th July 2014.}, + pages = {84--94}, + year = {2014}, + crossref = {DBLP:journals/corr/BenzmullerP14}, + url = {https://doi.org/10.4204/EPTCS.167.10}, + deactivated_doi = {10.4204/EPTCS.167.10}, + timestamp = {Wed, 12 Sep 2018 01:05:15 +0200}, + biburl = {https://dblp.org/rec/bib/journals/corr/Wenzel14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:journals/corr/BenzmullerP14, + editor = {Christoph Benzm{\"{u}}ller and + Bruno {Woltzenlogel Paleo}}, + title = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, + {UITP} 2014, Vienna, Austria, 17th July 2014}, + series = {{EPTCS}}, + volume = {167}, + year = {2014}, + url = {https://doi.org/10.4204/EPTCS.167}, + deactivated_doi = {10.4204/EPTCS.167}, + timestamp = {Wed, 12 Sep 2018 01:05:15 +0200}, + biburl = {https://dblp.org/rec/bib/journals/corr/BenzmullerP14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/mkm/BarrasGHRTWW13, + author = {Bruno Barras and + Lourdes Del Carmen Gonz{\'{a}}lez{-}Huesca and + Hugo Herbelin and + Yann R{\'{e}}gis{-}Gianas and + Enrico Tassi and + Makarius Wenzel and + Burkhart Wolff}, + title = {Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving + Systems}, + deactivated_booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems + and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12, + 2013. Proceedings}, + pages = {359--363}, + year = {2013}, + crossref = {DBLP:conf/mkm/2013}, + url = {https://doi.org/10.1007/978-3-642-39320-4\_29}, + deactivated_doi = {10.1007/978-3-642-39320-4\_29}, + timestamp = {Sun, 02 Jun 2019 21:17:34 +0200}, + biburl = {https://dblp.org/rec/bib/conf/mkm/BarrasGHRTWW13}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:conf/mkm/2013, + editor = {Jacques Carette and + David Aspinall and + Christoph Lange and + Petr Sojka and + Wolfgang Windsteiger}, + title = {Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems + and Projects 2013, Held as Part of {CICM} 2013, Bath, UK, July 8-12, + 2013. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {7961}, + publisher = {Springer}, + year = {2013}, + url = {https://doi.org/10.1007/978-3-642-39320-4}, + deactivated_doi = {10.1007/978-3-642-39320-4}, + isbn = {978-3-642-39319-8}, + timestamp = {Sun, 02 Jun 2019 21:17:34 +0200}, + biburl = {https://dblp.org/rec/bib/conf/mkm/2013}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/afp/LammichW19, + author = {Peter Lammich and + Simon Wimmer}, + title = {{IMP2} - Simple Program Verification in Isabelle/HOL}, + journal = {Archive of Formal Proofs}, + volume = {2019}, + year = {2019}, + url = {https://www.isa-afp.org/entries/IMP2.html}, + timestamp = {Mon, 20 May 2019 11:45:07 +0200}, + biburl = {https://dblp.org/rec/bib/journals/afp/LammichW19}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@misc{frama-c-home-page, + title = {The Frama-C Home Page}, + author = {CEA LIST}, + year = 2019, + month = jan, + day = 10, + url = {https://frama-c.com}, + note = {Accessed \DTMdate{2019-03-24}} +} + +@inproceedings{DBLP:conf/fm/LeinenbachS09, + author = {Dirk Leinenbach and Thomas Santen}, + title = {Verifying the Microsoft Hyper-V Hypervisor with {VCC}}, + deactivated_booktitle = {{FM} 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, + November 2-6, 2009. Proceedings}, + pages = {806--809}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-05089-3_51}, + deactivated_doi = {10.1007/978-3-642-05089-3_51}, + timestamp = {Mon, 22 May 2017 17:11:19 +0200}, + biburl = {https://dblp.org/rec/bib/conf/fm/LeinenbachS09}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/tap/Keller18, + author = {Chantal Keller}, + title = {Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL}, + deactivated_booktitle = {Tests and Proofs - 12th International Conference, {TAP} 2018, Held + as Part of {STAF} 2018, Toulouse, France, June 27-29, 2018, Proceedings}, + pages = {103--119}, + year = {2018}, + url = {https://doi.org/10.1007/978-3-319-92994-1\_6}, + deactivated_doi = {10.1007/978-3-319-92994-1\_6}, + timestamp = {Mon, 18 Jun 2018 13:57:50 +0200}, + biburl = {https://dblp.org/rec/bib/conf/tap/Keller18}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/itp/AissatVW16, + author = {Romain A{\"{\i}}ssat and + Fr{\'{e}}d{\'{e}}ric Voisin and + Burkhart Wolff}, + title = {Infeasible Paths Elimination by Symbolic Execution Techniques - Proof + of Correctness and Preservation of Paths}, + deactivated_booktitle = {Interactive Theorem Proving - 7th International Conference, {ITP} + 2016, Nancy, France, August 22-25, 2016, Proceedings}, + pages = {36--51}, + year = {2016}, + url = {https://doi.org/10.1007/978-3-319-43144-4\_3}, + deactivated_doi = {10.1007/978-3-319-43144-4\_3}, + timestamp = {Thu, 17 Aug 2017 16:22:01 +0200}, + biburl = {https://dblp.org/rec/bib/conf/itp/AissatVW16}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/tocs/KleinAEMSKH14, + author = {Gerwin Klein and + June Andronick and + Kevin Elphinstone and + Toby C. Murray and + Thomas Sewell and + Rafal Kolanski and + Gernot Heiser}, + title = {Comprehensive formal verification of an {OS} microkernel}, + journal = {{ACM} Trans. Comput. Syst.}, + volume = {32}, + number = {1}, + pages = {2:1--2:70}, + year = {2014}, + url = {http://doi.acm.org/10.1145/2560537}, + deactivated_doi = {10.1145/2560537}, + timestamp = {Tue, 03 Jan 2017 11:51:57 +0100}, + biburl = {https://dblp.org/rec/bib/journals/tocs/KleinAEMSKH14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/pldi/GreenawayLAK14, + author = {David Greenaway and + Japheth Lim and + June Andronick and + Gerwin Klein}, + title = {Don't sweat the small stuff: formal verification of {C} code without + the pain}, + deactivated_booktitle = {{ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, + {PLDI} '14, Edinburgh, United Kingdom - June 09 - 11, 2014}, + pages = {429--439}, + year = {2014}, + url = {http://doi.acm.org/10.1145/2594291.2594296}, + deactivated_doi = {10.1145/2594291.2594296}, + timestamp = {Tue, 20 Dec 2016 10:12:01 +0100}, + biburl = {https://dblp.org/rec/bib/conf/pldi/GreenawayLAK14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/mkm/BruckerACW18, + author = {Achim D. Brucker and + Idir A{\"{\i}}t{-}Sadoune and + Paolo Crisafulli and + Burkhart Wolff}, + title = {Using the Isabelle Ontology Framework - Linking the Formal with the + Informal}, + deactivated_booktitle = {Intelligent Computer Mathematics - 11th International Conference, + {CICM} 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings}, + pages = {23--38}, + year = {2018}, + url = {https://doi.org/10.1007/978-3-319-96812-4\_3}, + deactivated_doi = {10.1007/978-3-319-96812-4\_3}, + timestamp = {Sat, 11 Aug 2018 00:57:41 +0200}, + biburl = {https://dblp.org/rec/bib/conf/mkm/BruckerACW18}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/afp/TuongW15, + author = {Fr{\'{e}}d{\'{e}}ric Tuong and + Burkhart Wolff}, + title = {A Meta-Model for the Isabelle {API}}, + journal = {Archive of Formal Proofs}, + volume = {2015}, + year = {2015}, + url = {https://www.isa-afp.org/entries/Isabelle\_Meta\_Model.shtml}, + timestamp = {Mon, 07 Jan 2019 11:16:33 +0100}, + biburl = {https://dblp.org/rec/bib/journals/afp/TuongW15}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/tphol/WinwoodKSACN09, + author = {Simon Winwood and + Gerwin Klein and + Thomas Sewell and + June Andronick and + David Cock and + Michael Norrish}, + title = {Mind the Gap}, + deactivated_booktitle = {Theorem Proving in Higher Order Logics, 22nd International Conference, + TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, + pages = {500--515}, + year = {2009}, + crossref = {DBLP:conf/tphol/2009}, + url = {https://doi.org/10.1007/978-3-642-03359-9\_34}, + deactivated_doi = {10.1007/978-3-642-03359-9\_34}, + timestamp = {Fri, 02 Nov 2018 09:49:05 +0100}, + biburl = {https://dblp.org/rec/bib/conf/tphol/WinwoodKSACN09}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:conf/tphol/2009, + editor = {Stefan Berghofer and + Tobias Nipkow and + Christian Urban and + Makarius Wenzel}, + title = {Theorem Proving in Higher Order Logics, 22nd International Conference, + TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {5674}, + publisher = {Springer}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-03359-9}, + deactivated_doi = {10.1007/978-3-642-03359-9}, + isbn = {978-3-642-03358-2}, + timestamp = {Tue, 23 May 2017 01:12:08 +0200}, + biburl = {https://dblp.org/rec/bib/conf/tphol/2009}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/afp/BruckerTW14, + author = {Achim D. Brucker and + Fr{\'{e}}d{\'{e}}ric Tuong and + Burkhart Wolff}, + title = {Featherweight {OCL:} {A} Proposal for a Machine-Checked Formal Semantics + for {OCL} 2.5}, + journal = {Archive of Formal Proofs}, + volume = {2014}, + year = {2014}, + url = {https://www.isa-afp.org/entries/Featherweight\_OCL.shtml}, + timestamp = {Mon, 07 Jan 2019 11:16:33 +0100}, + biburl = {https://dblp.org/rec/bib/journals/afp/BruckerTW14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/tacas/SananZHZTL17, + author = {David San{\'{a}}n and + Yongwang Zhao and + Zhe Hou and + Fuyuan Zhang and + Alwen Tiu and + Yang Liu}, + title = {CSimpl: {A} Rely-Guarantee-Based Framework for Verifying Concurrent + Programs}, + deactivated_booktitle = {Tools and Algorithms for the Construction and Analysis of Systems + - 23rd International Conference, {TACAS} 2017, Held as Part of the + European Joint Conferences on Theory and Practice of Software, {ETAPS} + 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}}, + pages = {481--498}, + year = {2017}, + crossref = {DBLP:conf/tacas/2017-1}, + url = {https://doi.org/10.1007/978-3-662-54577-5\_28}, + deactivated_doi = {10.1007/978-3-662-54577-5\_28}, + timestamp = {Mon, 18 Sep 2017 08:38:37 +0200}, + biburl = {https://dblp.org/rec/bib/conf/tacas/SananZHZTL17}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:conf/tacas/2017-1, + editor = {Axel Legay and + Tiziana Margaria}, + title = {Tools and Algorithms for the Construction and Analysis of Systems + - 23rd International Conference, {TACAS} 2017, Held as Part of the + European Joint Conferences on Theory and Practice of Software, {ETAPS} + 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}}, + series = {Lecture Notes in Computer Science}, + volume = {10205}, + year = {2017}, + url = {https://doi.org/10.1007/978-3-662-54577-5}, + deactivated_doi = {10.1007/978-3-662-54577-5}, + isbn = {978-3-662-54576-8}, + timestamp = {Wed, 24 May 2017 08:28:32 +0200}, + biburl = {https://dblp.org/rec/bib/conf/tacas/2017-1}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@inproceedings{DBLP:conf/itp/HouSTL17, + author = {Zhe Hou and + David San{\'{a}}n and + Alwen Tiu and + Yang Liu}, + title = {Proof Tactics for Assertions in Separation Logic}, + deactivated_booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP} + 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings}, + pages = {285--303}, + year = {2017}, + crossref = {DBLP:conf/itp/2017}, + url = {https://doi.org/10.1007/978-3-319-66107-0\_19}, + deactivated_doi = {10.1007/978-3-319-66107-0\_19}, + timestamp = {Mon, 18 Sep 2017 08:38:37 +0200}, + biburl = {https://dblp.org/rec/bib/conf/itp/HouSTL17}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@proceedings{DBLP:conf/itp/2017, + editor = {Mauricio Ayala{-}Rinc{\'{o}}n and + C{\'{e}}sar A. Mu{\~{n}}oz}, + title = {Interactive Theorem Proving - 8th International Conference, {ITP} + 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {10499}, + publisher = {Springer}, + year = {2017}, + url = {https://doi.org/10.1007/978-3-319-66107-0}, + deactivated_doi = {10.1007/978-3-319-66107-0}, + isbn = {978-3-319-66106-3}, + timestamp = {Wed, 06 Sep 2017 14:53:52 +0200}, + biburl = {https://dblp.org/rec/bib/conf/itp/2017}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/sigbed/CarrascosaCMBC14, + author = {E. Carrascosa and + Javier Coronel and + Miguel Masmano and + Patricia Balbastre and + Alfons Crespo}, + title = {XtratuM hypervisor redesign for {LEON4} multicore processor}, + journal = {{SIGBED} Review}, + volume = {11}, + number = {2}, + pages = {27--31}, + year = {2014}, + url = {https://doi.org/10.1145/2668138.2668142}, + deactivated_doi = {10.1145/2668138.2668142}, + timestamp = {Tue, 06 Nov 2018 12:51:31 +0100}, + biburl = {https://dblp.org/rec/bib/journals/sigbed/CarrascosaCMBC14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/cacm/Earley70, + author = {Jay Earley}, + title = {An Efficient Context-Free Parsing Algorithm}, + journal = {Commun. {ACM}}, + volume = {13}, + number = {2}, + pages = {94--102}, + year = {1970}, + url = {https://doi.org/10.1145/362007.362035}, + deactivated_doi = {10.1145/362007.362035}, + timestamp = {Wed, 14 Nov 2018 10:22:30 +0100}, + biburl = {https://dblp.org/rec/bib/journals/cacm/Earley70}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{DBLP:journals/jfp/Hutton92, + author = {Graham Hutton}, + title = {Higher-Order Functions for Parsing}, + journal = {J. Funct. Program.}, + volume = {2}, + number = {3}, + pages = {323--343}, + year = {1992}, + url = {https://doi.org/10.1017/S0956796800000411}, + deactivated_doi = {10.1017/S0956796800000411}, + timestamp = {Sat, 27 May 2017 14:24:34 +0200}, + biburl = {https://dblp.org/rec/bib/journals/jfp/Hutton92}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} \ No newline at end of file From 8acd482b96ce9d5476b9f8bb7c66cdf748f1a163 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 15 Jul 2019 17:45:46 +0200 Subject: [PATCH 02/10] Continued pass till pp 36. --- .../TR_MyCommentedIsabelle.thy | 161 +++++++++++++----- 1 file changed, 118 insertions(+), 43 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 5a482456..01c0f7b8 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -1328,8 +1328,16 @@ worked out @{cite "DBLP:journals/jfp/Hutton92"}. Parsing combinators are one of major parsing technologies of the Isabelle front-end, in particular for the outer-syntax used for the parsing of toplevel-commands. The core of the combinator library is @{ML_structure \Scan\} providing the @{ML_type "'a parser"} which is a synonym for -@{ML_type " Token.T list -> 'a * Token.T list"}. The library also provides a bunch of -infix parsing combinators, notably:\ +@{ML_type " Token.T list -> 'a * Token.T list"}. + + "parsers" are actually interpreters; an 'a parser is a function that parses +an input stream and computes(=evaluates, computes) it into 'a. +Since the semantics of an Isabelle command is a transition => transition +or theory $\Rightarrow$ theory function, i.e. a global system transition. +parsers of that type can be constructed and be bound as call-back functions +to a table in the Toplevel-structure of Isar. + +The library also provides a bunch of infix parsing combinators, notably:\ ML\ val _ = op !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b @@ -1369,11 +1377,114 @@ fun parser2contextparser pars (ctxt, toks) = let val (a, toks') = pars toks val _ = parser2contextparser : 'a parser -> 'a context_parser; (* bah, is the same as Scan.lift *) -val _ = Scan.lift Args.cartouche_input : Input.source context_parser; +val _ = Scan.lift Args.cartouche_input : Input.source context_parser;\ +subsection\Advanced Parser Library\ + +text\There are two parts. A general multi-purpose parsing combinator library is +found under @{ML_structure "Parse"}, providing basic functionality for parsing strings +or integers. There is also an important combinator that reads the current position information +out of the input stream:\ +ML\ +Parse.nat: int parser; +Parse.int: int parser; +Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser; +Parse.enum: string -> 'a parser -> 'a list parser; +Parse.input: 'a parser -> Input.source parser; + +Parse.enum : string -> 'a parser -> 'a list parser; +Parse.!!! : (Token.T list -> 'a) -> Token.T list -> 'a; +Parse.position: 'a parser -> ('a * Position.T) parser; + +(* Examples *) +Parse.position Args.cartouche_input; +\ + +text\The second part is much more high-level, and can be found under @{ML_structure Args}. +In parts, these combinators are again based on more low-level combinators, in parts they serve as +an an interface to the underlying Earley-parser for mathematical notation used in types and terms. +This is perhaps meant with the fairly cryptic comment: +"Quasi-inner syntax based on outer tokens: concrete argument syntax of +attributes, methods etc." at the beginning of this structure. +\ + +ML\ + +local + + open Args + + (* some more combinaotrs *) + val _ = symbolic: Token.T parser + val _ = $$$ : string -> string parser + val _ = maybe: 'a parser -> 'a option parser + val _ = name_token: Token.T parser + + + (* common isar syntax *) + val _ = colon: string parser + val _ = query: string parser + val _ = bang: string parser + val _ = query_colon: string parser + val _ = bang_colon: string parser + val _ = parens: 'a parser -> 'a parser + val _ = bracks: 'a parser -> 'a parser + val _ = mode: string -> bool parser + val _ = name: string parser + val _ = name_position: (string * Position.T) parser + val _ = cartouche_inner_syntax: string parser + val _ = cartouche_input: Input.source parser + val _ = text_token: Token.T parser + + (* advanced string stuff *) + val _ = embedded_token: Token.T parser + val _ = embedded_inner_syntax: string parser + val _ = embedded_input: Input.source parser + val _ = embedded: string parser + val _ = embedded_position: (string * Position.T) parser + val _ = text_input: Input.source parser + val _ = text: string parser + val _ = binding: binding parser + + (* stuff related to INNER SYNTAX PARSING *) + val _ = alt_name: string parser + val _ = liberal_name: string parser + val _ = var: indexname parser + val _ = internal_source: Token.src parser + val _ = internal_name: Token.name_value parser + val _ = internal_typ: typ parser + val _ = internal_term: term parser + val _ = internal_fact: thm list parser + val _ = internal_attribute: (morphism -> attribute) parser + val _ = internal_declaration: declaration parser + + + val _ = named_source: (Token.T -> Token.src) -> Token.src parser + val _ = named_typ: (string -> typ) -> typ parser + val _ = named_term: (string -> term) -> term parser + + val _ = text_declaration: (Input.source -> declaration) -> declaration parser + val _ = cartouche_declaration: (Input.source -> declaration) -> declaration parser + val _ = typ_abbrev: typ context_parser + + val _ = typ: typ context_parser + val _ = term: term context_parser + val _ = term_pattern: term context_parser + val _ = term_abbrev: term context_parser + + (* syntax for some major Pure commands in Isar *) + val _ = prop: term context_parser + val _ = type_name: {proper: bool, strict: bool} -> string context_parser + val _ = const: {proper: bool, strict: bool} -> string context_parser + val _ = goal_spec: ((int -> tactic) -> tactic) context_parser + val _ = context: Proof.context context_parser + val _ = theory: theory context_parser + +in val _ = () end \ + subsection\ Bindings \ @@ -1401,34 +1512,9 @@ ML\ ("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})] *)\ -subsection \Scanning and combinator parsing. \ -text\Is used on two levels: -\<^enum> outer syntax, that is the syntax in which Isar-commands are written, and -\<^enum> inner-syntax, that is the syntax in which lambda-terms, and in particular HOL-terms were written. -\ -text\ A constant problem for newbies is this distinction, which makes it necessary that - the " ... " quotes have to be used when switching to inner-syntax, except when only one literal - is expected when an inner-syntax term is expected. -\ -ML\ -Scan.peek : ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd); -Scan.optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a; -Scan.option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a; -Scan.repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a; -Scan.lift : ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c); -Scan.lift (Parse.position Args.cartouche_input); -\ -text\ "parsers" are actually interpreters; an 'a parser is a function that parses - an input stream and computes(=evaluates, computes) it into 'a. - Since the semantics of an Isabelle command is a transition => transition - or theory $\Rightarrow$ theory function, i.e. a global system transition. - parsers of that type can be constructed and be bound as call-back functions - to a table in the Toplevel-structure of Isar. - The type 'a parser is already defined in the structure Token. -\ text\ Syntax operations : Interface for parsing, type-checking, "reading" (both) and pretty-printing. @@ -1440,20 +1526,7 @@ text\ Syntax operations : Interface for parsing, type-checking, "reading" context via @{ML Proof_Context.syn_of}. \ -ML\ -Parse.nat: int parser; -Parse.int: int parser; -Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser; -Parse.enum: string -> 'a parser -> 'a list parser; -Parse.input: 'a parser -> Input.source parser; -Parse.enum : string -> 'a parser -> 'a list parser; -Parse.!!! : (Token.T list -> 'a) -> Token.T list -> 'a; -Parse.position: 'a parser -> ('a * Position.T) parser; - -(* Examples *) -Parse.position Args.cartouche_input; -\ text\ Inner Syntax Parsing combinators for elementary Isabelle Lexems\ ML\ @@ -2004,10 +2077,12 @@ ML\Sign.add_trrules\ section*[c::conclusion]\Conclusion\ text\More to come\ +(*<*) + section*[bib::bibliography]\Bibliography\ -(*<*) close_monitor*[this] check_doc_global -(*>*) + end +(*>*) \ No newline at end of file From 6f2dabbdd2396f12e9571da7cc28a721c6017ac8 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 15 Jul 2019 17:56:13 +0200 Subject: [PATCH 03/10] Markup section aufgeraeumt. --- .../TR_MyCommentedIsabelle.thy | 149 +++++------------- 1 file changed, 36 insertions(+), 113 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 01c0f7b8..c4bc4842 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -1132,13 +1132,45 @@ display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above section\Markup and Low-level Markup Reporting\ text\The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic -annotation data which is part of the protocol sent from Isabelle to the frontend. +annotation data which is part of the protocol sent from Isabelle to the front-end. They are qualified as "quasi-abstract", which means they are intended to be an abstraction of the serialized, textual presentation of the protocol. Markups are structurally a pair of a key and properties; @{ML_structure Markup} provides a number of of such \<^emph>\key\s for annotation classes such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample from \<^theory_text>\Isabelle_DOF\. A markup must be tagged with an id; this is done by the @{ML serial}-function -discussed earlier.\ +discussed earlier. Markup Operations, were used for hyperlinking applications to binding +occurrences, info for hovering, infors for type ... \ +ML\ + +(* Position.report is also a type consisting of a pair of a position and markup. *) +(* It would solve all my problems if I find a way to infer the defining Position.report + from a type definition occurence ... *) + +Position.report: Position.T -> Markup.T -> unit; +Position.reports: Position.report list -> unit; + (* ? ? ? I think this is the magic thing that sends reports to the GUI. *) +Markup.entity : string -> string -> Markup.T; +Markup.properties : Properties.T -> Markup.T -> Markup.T ; +Properties.get : Properties.T -> string -> string option; +Markup.enclose : Markup.T -> string -> string; + +(* example for setting a link, the def flag controls if it is a defining or a binding +occurence of an item *) +fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) = + if id = 0 then Markup.empty + else + Markup.properties (Position.entity_properties_of def id pos) + (Markup.entity Markup.theoryN name); +Markup.theoryN : string; + +serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers, + be it on the level of thy-internal states or as reference in markup in + PIDE *) + +\ + + + subsection\A simple Example\ ML\ local @@ -1596,115 +1628,6 @@ fn name => (Thy_Output.antiquotation_pretty_source name (Scan.lift (Parse.positi \ -section\ The PIDE Framework \ -subsection\ Markup \ -text\ Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR. - Markup operation send via side-effect annotations to the GUI (precisely: - to the PIDE Framework) that were used for hyperlinking applicating to binding - occurrences, info for hovering, ... \ -ML\ - -(* Position.report is also a type consisting of a pair of a position and markup. *) -(* It would solve all my problems if I find a way to infer the defining Position.report - from a type definition occurence ... *) - -Position.report: Position.T -> Markup.T -> unit; -Position.reports: Position.report list -> unit; - (* ? ? ? I think this is the magic thing that sends reports to the GUI. *) -Markup.entity : string -> string -> Markup.T; -Markup.properties : Properties.T -> Markup.T -> Markup.T ; -Properties.get : Properties.T -> string -> string option; -Markup.enclose : Markup.T -> string -> string; - -(* example for setting a link, the def flag controls if it is a defining or a binding -occurence of an item *) -fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) = - if id = 0 then Markup.empty - else - Markup.properties (Position.entity_properties_of def id pos) - (Markup.entity Markup.theoryN name); -Markup.theoryN : string; - -serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers, - be it on the level of thy-internal states or as reference in markup in - PIDE *) - -(* From Theory: -fun check ctxt (name, pos) = - let - val thy = Proof_Context.theory_of ctxt; - val thy' = - Context.get_theory thy name - handle ERROR msg => - let - val completion = - Completion.make (name, pos) - (fn completed => - map Context.theory_name (ancestors_of thy) - |> filter completed - |> sort_strings - |> map (fn a => (a, (Markup.theoryN, a)))); - val report = Markup.markup_report (Completion.reported_text completion); - in error (msg ^ Position.here pos ^ report) end; - val _ = Context_Position.report ctxt pos (get_markup thy'); - in thy' end; - -fun init_markup (name, pos) thy = - let - val id = serial (); - val _ = Position.report pos (theory_markup true name id pos); - in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; - -fun get_markup thy = - let val {pos, id, ...} = rep_theory thy - in theory_markup false (Context.theory_name thy) id pos end; - - -*) - -(* -fun theory_markup def thy_name id pos = - if id = 0 then Markup.empty - else - Markup.properties (Position.entity_properties_of def id pos) - (Markup.entity Markup.theoryN thy_name); - -fun get_markup thy = - let val {pos, id, ...} = rep_theory thy - in theory_markup false (Context.theory_name thy) id pos end; - - -fun init_markup (name, pos) thy = - let - val id = serial (); - val _ = Position.report pos (theory_markup true name id pos); - in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; - - -fun check ctxt (name, pos) = - let - val thy = Proof_Context.theory_of ctxt; - val thy' = - Context.get_theory thy name - handle ERROR msg => - let - val completion = - Completion.make (name, pos) - (fn completed => - map Context.theory_name (ancestors_of thy) - |> filter completed - |> sort_strings - |> map (fn a => (a, (Markup.theoryN, a)))); - val report = Markup.markup_report (Completion.reported_text completion); - in error (msg ^ Position.here pos ^ report) end; - val _ = Context_Position.report ctxt pos (get_markup thy'); - in thy' end; - - -*) - -\ - section \ Output: Very Low Level \ @@ -2071,11 +1994,11 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl section\Inner Syntax\ -text\MORE TO COME\ +text\MORE TO COME : cartouches\ ML\Sign.add_trrules\ -section*[c::conclusion]\Conclusion\ +chapter*[c::conclusion]\Conclusion\ text\More to come\ (*<*) From a7f6ab4fbd93b45adf43357d3637d7ad50bac22b Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 16 Jul 2019 16:40:40 +0200 Subject: [PATCH 04/10] Para on Antiquotation Registration --- .../TR_MyCommentedIsabelle.thy | 172 +++++++++++------- 1 file changed, 108 insertions(+), 64 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index c4bc4842..38069763 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -540,12 +540,22 @@ val t'' = Term.map_types (Term_Subst.instantiateT S') (t) subsection\ Type-Inference (= inferring consistent type information if possible) \ +ML\ +Consts.the_const; (* T is a kind of signature ... *) +Variable.import_terms; +Vartab.update; +\ + +subsection\ Type-Inference (= inferring consistent type information if possible) \ + text\ Type inference eliminates also joker-types such as @{ML dummyT} and produces instances for schematic type variables where necessary. In the case of success, it produces a certifiable term. \ ML\ Type_Infer_Context.infer_types: Proof.context -> term list -> term list \ + + subsection\ thy and the signature interface\ ML\ @@ -1519,46 +1529,66 @@ in val _ = () end subsection\ Bindings \ +text\ The structure @{ML_structure "Binding"} serves as +\structured name bindings\, as says the description, i.e. a mechanism to basically +associate an input string-fragment to its position. This concept is vital in all parsing processes +and the interaction with PIDE. +Key are two things: +\<^enum> the type-synonym @{ML_type "bstring"} which is synonym to @{ML_type "string"} + and intended for "primitive names to be bound" +\<^enum> the projection @{ML "Binding.pos_of : binding -> Position.T"} +\<^enum> the constructor establishing a binding @{ML "Binding.make: bstring * Position.T -> binding"} + +\ + +text\Since this is so common in interface programming, there are a number of antiquotations\ ML\ val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position, - where \positions\ are absolute references to a file *) + where \positions\ are absolute references to a file *) -Binding.make: bstring * Position.T -> binding; -Binding.pos_of @{binding erzerzer}; -Position.here: Position.T -> string; -(* Bindings *) -ML\val X = @{here};\ +Binding.pos_of H; (* clicking on "H" activates the hyperlink to the defining occ of "H" above *) +(* {offset=23, end_offset=27, id=-17214}: Position.T *) + +(* a modern way to construct a binding is by the following code antiquotation : *) +\<^binding>\theory\ \ subsection \Input streams. \ +text\Reads as : Generic input with position information.\ + ML\ Input.source_explode : Input.source -> Symbol_Pos.T list; - (* conclusion: Input.source_explode converts " f @{thm refl}" - into: + Input.source_explode (Input.string " f @{thm refl}"); + + (* If stemming from the input window, this can be s th like: + [(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}), ("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}), ("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}), ("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}), ("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})] - *)\ - + *) - - - -text\ Syntax operations : Interface for parsing, type-checking, "reading" - (both) and pretty-printing. - Note that this is a late-binding interface, i.e. a collection of "hooks". - The real work is done ... see below. - - Encapsulates the data structure "syntax" --- the table with const symbols, - print and ast translations, ... The latter is accessible, e.g. from a Proof - context via @{ML Proof_Context.syn_of}. \ +section\Term Parsing\ + +text\The heart of the parsers for mathematical notation, based on an Earley parser that can cope +with incremental changes of the grammar as required for sophisticated mathematical output, is hidden +behind the API described in this section.\ + +text\ Note that the naming underlies the following convention : + there are: + \<^enum> "parser"s and type-"checker"s + \<^enum> "reader"s which do both together with pretty-printing + + This is encapsulated the data structure @{ML_structure Syntax} --- + the table with const symbols, print and ast translations, ... The latter is accessible, e.g. + from a Proof context via @{ML Proof_Context.syn_of}. +\ text\ Inner Syntax Parsing combinators for elementary Isabelle Lexems\ ML\ @@ -1600,35 +1630,77 @@ Syntax.string_of_term: Proof.context -> term -> string; Syntax.string_of_typ: Proof.context -> typ -> string; Syntax.lookup_const : Syntax.syntax -> string -> string option; \ + +text\ + Note that @{ML "Syntax.install_operations"} is a late-binding interface, i.e. a collection of + "hooks" used to resolve an apparent architectural cycle. + The real work is done in @{file "~~/src/Pure/Syntax/syntax_phases.ML"} + + Even the parsers and type checkers stemming from the theory-structure are registered via + hooks (this can be confusing at times). Main phases of inner syntax processing, with standard + implementations of parse/unparse operations were treated this way. + At the very very end in , it sets up the entire syntax engine + (the hooks) via: +\ + + +(* +val _ = + Theory.setup + (Syntax.install_operations + {parse_sort = parse_sort, + parse_typ = parse_typ, + parse_term = parse_term false, + parse_prop = parse_term true, + unparse_sort = unparse_sort, + unparse_typ = unparse_typ, + unparse_term = unparse_term, + check_typs = check_typs, + check_terms = check_terms, + check_props = check_props, + uncheck_typs = uncheck_typs, + uncheck_terms = uncheck_terms}); +*) + +subsection \Example\ ML\ -fun read_terms ctxt = - grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt; -\ - -ML\ -(* More High-level, more Isar-specific Parsers *) -Args.name; -Args.const; +(* Recall the Arg-interface to the more high-level, more Isar-specific parsers: *) +Args.name : string parser ; +Args.const : {proper: bool, strict: bool} -> string context_parser; Args.cartouche_input: Input.source parser; -Args.text_token: Token.T parser; +Args.text_token : Token.T parser; + +(* here follows the definition of the attribute parser : *) val Z = let val attribute = Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; - in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ; -(* this leads to constructions like the following, where a parser for a *) - + in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ; +(* Here is the code to register the above parsers as text antiquotations into the Isabelle + Framework: *) Thy_Output.antiquotation_pretty_source \<^binding>\theory\ (Scan.lift (Parse.position Args.embedded)); Thy_Output.antiquotation_raw \<^binding>\file\ (Scan.lift (Parse.position Parse.path)) ; -fn name => (Thy_Output.antiquotation_pretty_source name (Scan.lift (Parse.position Args.cartouche_input))); + +(* where we have the registration of the action + + (Scan.lift (Parse.position Args.cartouche_input)))) + + to be bound to the + + name + + as a whole is a system transaction that, of course, has the type + + theory -> theory : *) +(fn name => (Thy_Output.antiquotation_pretty_source name + (Scan.lift (Parse.position Args.cartouche_input)))) + : binding -> (Proof.context -> Input.source * Position.T -> Pretty.T) -> theory -> theory; \ - - section \ Output: Very Low Level \ ML\ @@ -1804,31 +1876,6 @@ val _ = Thy_Output.present_thy; \ -text\ Even the parsers and type checkers stemming from the theory-structure are registered via -hooks (this can be confusing at times). Main phases of inner syntax processing, with standard -implementations of parse/unparse operations were treated this way. -At the very very end in @{file "~~/src/Pure/Syntax/syntax_phases.ML"}, it sets up the entire syntax engine -(the hooks) via: -\ - - -(* -val _ = - Theory.setup - (Syntax.install_operations - {parse_sort = parse_sort, - parse_typ = parse_typ, - parse_term = parse_term false, - parse_prop = parse_term true, - unparse_sort = unparse_sort, - unparse_typ = unparse_typ, - unparse_term = unparse_term, - check_typs = check_typs, - check_terms = check_terms, - check_props = check_props, - uncheck_typs = uncheck_typs, - uncheck_terms = uncheck_terms}); -*) text\ Thus, Syntax\_Phases does the actual work, including markup generation and generation of reports. Look at: \ @@ -1876,9 +1923,6 @@ As one can see, check-routines internally generate the markup. -Consts.the_const; (* T is a kind of signature ... *) -Variable.import_terms; -Vartab.update; fun control_antiquotation name s1 s2 = Thy_Output.antiquotation name (Scan.lift Args.cartouche_input) From 58c31b59e8d1926d044d1c55788697a8343ab699 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 16 Jul 2019 19:33:24 +0200 Subject: [PATCH 05/10] completed first draft. Checks till page 47. --- .../TR_MyCommentedIsabelle.thy | 454 ++++++++---------- 1 file changed, 200 insertions(+), 254 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 38069763..d5105ed2 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -26,8 +26,8 @@ combination of text editing, formal verification, and code generation. This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated "The Isabelle Cookbook" in \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged -not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jedit -in order to make experiments on the running code. +not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jEdit +@{cite "DBLP:journals/corr/Wenzel14"}in order to make experiments on the running code. This text is written itself in Isabelle/Isar using a specific document ontology for technical reports. It is intended to be a "living document", i.e. it is not only @@ -41,7 +41,7 @@ which makes this text re-checkable at each load and easier maintainable. chapter*[intro::introduction]\ Introduction \ text\ -While Isabelle is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually +While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually provides a system framework for developing a wide spectrum of applications. A particular strength of the Isabelle framework is the combination of text editing, formal verification, and code generation. This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary text to the @@ -86,7 +86,8 @@ ML\ val X = Unsynchronized.ref 0; text\However, since Isabelle is a platform involving parallel execution, concurrent computing, and, as an interactive environment, involves backtracking / re-evaluation as a consequence of user- interaction, imperative programming is discouraged and nearly never used in the entire Isabelle -code-base. The preferred programming style is purely functional: \ +code-base @{cite "DBLP:conf/mkm/BarrasGHRTWW13"}. +The preferred programming style is purely functional: \ ML\ fun fac x = if x = 0 then 1 else x * fac(x-1) ; fac 10; @@ -309,8 +310,7 @@ ML\ \ -subsection*[t213::example]\Mechanism 2 : global arbitrary data structure that is attached to - the global and local Isabelle context $\theta$ \ +subsection*[t213::example]\Mechanism 2 : Extending the Global Context $\theta$ by User Data \ ML \ datatype X = mt @@ -860,7 +860,42 @@ ML\ Toplevel.presentation_context: Toplevel.state -> Proof.context; \ - + +text\ The extensibility of Isabelle as a system framework depends on a number of tables, + into which various concepts commands, ML-antiquotations, text-antiquotations, cartouches, ... + can be entered via a late-binding on the fly. + + A paradigmatic example is the @{ML "Outer_Syntax.command"}-operation, which --- + representing in itself a toplevel system transition --- allows to define a new + command section and bind its syntax and semantics at a specific keyword. + Calling @{ML "Outer_Syntax.command"} + creates an implicit @{ML Theory.setup} with an entry for a call-back function, which happens + to be a parser that must have as side-effect a Toplevel-transition-transition. + Registers @{ML_type "Toplevel.transition -> Toplevel.transition"} parsers to the + Isar interpreter. +\ + + +ML\ Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> + (Toplevel.transition -> Toplevel.transition) parser -> unit;\ + +text\A paradigmatic example: "text" is defined by: \ + +(* +val _ = + Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" + (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true}); +*) + + +text\Here are a few queries relevant for the global config of the isar engine:\ +ML\ Document.state();\ +ML\ Session.get_keywords(); (* this looks to be really session global. *) \ +ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \ + + + + subsection \Transaction Management in the Isar-Engine : The Toplevel \ ML\ @@ -1000,7 +1035,8 @@ Synchronized.value C; chapter\Front-End \ text\In the following chapter, we turn to the right part of the system architecture shown in @{docitem \architecture\}: -The PIDE ("Prover-IDE") layer consisting of a part written in SML and another in SCALA. +The PIDE ("Prover-IDE") layer @{cite "DBLP:conf/itp/Wenzel14"} +consisting of a part written in SML and another in SCALA. Roughly speaking, PIDE implements "continuous build - continuous check" - functionality over a textual, albeit generic document model. It transforms user modifications of text elements in an instance of this model into increments (edits) and communicates @@ -1703,33 +1739,91 @@ Thy_Output.antiquotation_raw \<^binding>\file\ (Scan.lift (Parse.po section \ Output: Very Low Level \ +text\ For re-directing the output channels, the structure @{ML_structure Output} may be relevant:\ + ML\ Output.output; (* output is the structure for the "hooks" with the target devices. *) Output.output "bla_1:"; \ +text\It provides a number of hooks that can be used for redirection hacks ...\ + section \ Output: LaTeX \ +text\The heart of the LaTeX generator is to be found in the structure @{ML_structure Thy_Output}. +This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing +process can not be parsed for the LaTeX Generator. The reason is twofold: +\<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut if the thy-file; thus, its + spacing is relevant. +\<^enum> there is a special bracket \(*<*)\ ... \(*>*)\ that allows to specify input that is checked by + Isabelle, but excluded from the LaTeX generator (this is handled in an own sub-parser + called @{ML "Document_Source.improper"} where also other forms of comment parsers are provided. +Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to +@{ML_structure "Pretty"}. Key functions of this structure @{ML_structure "Latex"} are: +\ -ML\ open Thy_Output; +ML\ +local + open Latex + + type dummy = text + + val _ = string: string -> text; + val _ = text: string * Position.T -> text + + val _ = output_text: text list -> string + val _ = output_positions: Position.T -> text list -> string + val _ = output_name: string -> string + val _ = output_ascii: string -> string + val _ = output_symbols: Symbol.symbol list -> string + + val _ = begin_delim: string -> string + val _ = end_delim: string -> string + val _ = begin_tag: string -> string + val _ = end_tag: string -> string + val _ = environment_block: string -> text list -> text + val _ = environment: string -> string -> string + + val _ = block: text list -> text + val _ = enclose_body: string -> string -> text list -> text list + val _ = enclose_block: string -> string -> text list -> text + +in val _ = () +end; + +Latex.output_ascii; +Latex.environment "isa" "bg"; +Latex.output_ascii "a_b:c'é"; +(* Note: *) +space_implode "sd &e sf dfg" ["qs","er","alpa"]; + +\ + +text\Here is an abstract of the main interface to @{ML_structure Thy_Output}:\ + +ML\ output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list; output_token: Proof.context -> Token.T -> Latex.text list; output_source: Proof.context -> string -> Latex.text list; present_thy: Options.T -> theory -> segment list -> Latex.text list; - pretty_term: Proof.context -> term -> Pretty.T; - pretty_thm: Proof.context -> thm -> Pretty.T; - lines: Latex.text list -> Latex.text list; - items: Latex.text list -> Latex.text list; + isabelle: Proof.context -> Latex.text list -> Latex.text; + isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text; + typewriter: Proof.context -> string -> Latex.text; + verbatim: Proof.context -> string -> Latex.text; + source: Proof.context -> {embedded: bool} -> Token.src -> Latex.text; + pretty: Proof.context -> Pretty.T -> Latex.text; pretty_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T -> Latex.text; pretty_items: Proof.context -> Pretty.T list -> Latex.text; pretty_items_source: Proof.context -> {embedded: bool} -> Token.src -> Pretty.T list -> Latex.text; + +(* finally a number of antiquotation registries : *) antiquotation_pretty: binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory; antiquotation_pretty_source: @@ -1742,143 +1836,9 @@ ML\ open Thy_Output; \ - +text\ Thus, @{ML_structure Syntax_Phases} does the actual work of markup generation, including + markup generation and generation of reports. Look at the following snippet: \ ML\ -Syntax_Phases.reports_of_scope; -\ - -(* STOP HERE JUNK ZONE : - -(* Pretty.T, pretty-operations. *) -ML\ - -(* interesting piece for LaTeX Generation: -fun verbatim_text ctxt = - if Config.get ctxt display then - split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #> - Latex.output_ascii #> Latex.environment "isabellett" - else - split_lines #> - map (Latex.output_ascii #> enclose "\\isatt{" "}") #> - space_implode "\\isasep\\isanewline%\n"; - -(* From structure Thy_Output *) -fun pretty_const ctxt c = - let - val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c) - handle TYPE (msg, _, _) => error msg; - val ([t'], _) = Variable.import_terms true [t] ctxt; - in pretty_term ctxt t' end; - - basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #> - -*) - -Pretty.enclose : string -> string -> Pretty.T list -> Pretty.T; (* not to confuse with: String.enclose *) - -(* At times, checks where attached to Pretty - functions and exceptions used to - stop the execution/validation of a command *) -fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name); -Pretty.enclose; -Pretty.str; -Pretty.mark_str; -Pretty.text "bla_d"; - -Pretty.quote; (* Pretty.T transformation adding " " *) -Pretty.unformatted_string_of : Pretty.T -> string ; - -Latex.output_ascii; -Latex.environment "isa" "bg"; -Latex.output_ascii "a_b:c'é"; -(* Note: *) -space_implode "sd &e sf dfg" ["qs","er","alpa"]; - - -(* -fun pretty_command (cmd as (name, Command {comment, ...})) = - Pretty.block - (Pretty.marks_str - ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]}, - command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); -*) - - -\ - -ML\ -Thy_Output.output_text; -(* is: -fun output_text state {markdown} source = - let - val is_reported = - (case try Toplevel.context_of state of - SOME ctxt => Context_Position.is_visible ctxt - | NONE => true); - - val pos = Input.pos_of source; - val syms = Input.source_explode source; - - val _ = - if is_reported then - Position.report pos (Markup.language_document (Input.is_delimited source)) - else (); - - val output_antiquotes = map (eval_antiquote state) #> implode; - - fun output_line line = - (if Markdown.line_is_item line then "\\item " else "") ^ - output_antiquotes (Markdown.line_content line); - - fun output_blocks blocks = space_implode "\n\n" (map output_block blocks) - and output_block (Markdown.Par lines) = cat_lines (map output_line lines) - | output_block (Markdown.List {kind, body, ...}) = - Latex.environment (Markdown.print_kind kind) (output_blocks body); - in - if Toplevel.is_skipped_proof state then "" - else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms - then - let - val ants = Antiquote.parse pos syms; - val reports = Antiquote.antiq_reports ants; - val blocks = Markdown.read_antiquotes ants; - val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else (); - in output_blocks blocks end - else - let - val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms); - val reports = Antiquote.antiq_reports ants; - val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else (); - in output_antiquotes ants end - end; -*) - -\ - - -ML\ -Outer_Syntax.print_commands @{theory}; - -Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> - (Toplevel.transition -> Toplevel.transition) parser -> unit; -(* creates an implicit thy_setup with an entry for a call-back function, which happens - to be a parser that must have as side-effect a Toplevel-transition-transition. - Registers "Toplevel.transition -> Toplevel.transition" parsers to the Isar interpreter. - *) - -(*Example: text is : - -val _ = - Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" - (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true}); -*) - -(* not exported: Thy_Output.output_token; Ich glaub, da passierts ... *) -Thy_Output.present_thy; -\ - - -text\ Thus, Syntax\_Phases does the actual work, including - markup generation and generation of reports. Look at: \ (* fun check_typs ctxt raw_tys = let @@ -1920,130 +1880,116 @@ which is the real implementation behind Syntax.check_term As one can see, check-routines internally generate the markup. *) - - - - -fun control_antiquotation name s1 s2 = - Thy_Output.antiquotation name (Scan.lift Args.cartouche_input) - (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false}); - -Output.output; - -Syntax.read_input ; -Input.source_content; - -(* - basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #> -*) - - - - -chapter\LaTeX Document Generation\ -text\MORE TO COME\ - - -ML\ Thy_Output.document_command {markdown = true} \ -(* Structures related to LaTeX Generation *) -ML\ Latex.output_ascii; - - Latex.output_token -(* Hm, generierter output for -subsection*[Shaft_Encoder_characteristics]{ * Shaft Encoder Characteristics * } : - -\begin{isamarkuptext}% -\isa{{\isacharbackslash}label{\isacharbraceleft}general{\isacharunderscore}hyps{\isacharbraceright}}% -\end{isamarkuptext}\isamarkuptrue% -\isacommand{subsection{\isacharasterisk}}\isamarkupfalse% -{\isacharbrackleft}Shaft{\isacharunderscore}Encoder{\isacharunderscore}characteristics{\isacharbrackright}{\isacharverbatimopen}\ Shaft\ Encoder\ Characteristics\ {\isacharverbatimclose}% - -Generierter output for: text\\label{sec:Shaft-Encoder-characteristics}\ - -\begin{isamarkuptext}% -\label{sec:Shaft-Encoder-characteristics}% -\end{isamarkuptext}\isamarkuptrue% - - -*) - - \ -ML\ -Thy_Output.maybe_pretty_source : - (Proof.context -> 'a -> Pretty.T) -> Proof.context -> Token.src -> 'a list -> Pretty.T list; -Thy_Output.output: Proof.context -> Pretty.T list -> string; - - (* nuescht besonderes *) - -fun document_antiq check_file ctxt (name, pos) = - let - (* val dir = master_directory (Proof_Context.theory_of ctxt); *) - (* val _ = check_path check_file ctxt dir (name, pos); *) - in - space_explode "/" name - |> map Latex.output_ascii - |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}") - |> enclose "\\isatt{" "}" - end; +section\Inner Syntax Cartouches\ +text\ The cascade-syntax principle underlying recent isabelle versions requires a +particular mechanism, called "cartouche" by Makarius who was influenced by French +Wine and French culture when designing this. +When parsing terms or types (via the Earley Parser), a standard mechanism for +calling another parser inside the current process is needed that is bound to the +\(\)\ ... \(\)\ paranthesis'. \ -ML\ +text\The following example --- drawn from the Isabelle/DOF implementation --- allows +to parse UTF8 - Unicode strings as alternative to @{term "''abc''"} HOL-strings.\ -Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string; -Thy_Output.document_command; - -Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source -> - Toplevel.transition -> Toplevel.transition; - (* fun document_command markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_text state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); - - *) - -Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ; - (* this is where antiquotation expansion happens : uses eval_antiquote *) +ML\\ \Dynamic setup of inner syntax cartouche\ -Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source -> - Toplevel.transition -> Toplevel.transition; - (* fun document_command markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_text state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); +(* Author: Frédéric Tuong, Université Paris-Saclay *) +(* Title: HOL/ex/Cartouche_Examples.thy + Author: Makarius *) + local + fun mk_char (f_char, f_cons, _) (s, _) accu = + fold + (fn c => fn (accu, l) => + (f_char c accu, f_cons c l)) + (rev (map Char.ord (String.explode s))) + accu; - *) + fun mk_string (_, _, f_nil) accu [] = (accu, f_nil) + | mk_string f accu (s :: ss) = mk_char f s (mk_string f accu ss); + in + fun string_tr f f_mk accu content args = + let fun err () = raise TERM ("string_tr", args) in + (case args of + [(c as Const (@{syntax_const "_constrain"}, _)) $ Free (s, _) $ p] => + (case Term_Position.decode_position p of + SOME (pos, _) => c $ f (mk_string f_mk accu (content (s, pos))) $ p + | NONE => err ()) + | _ => err ()) + end; + end; +\ -Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ; - (* this is where antiquotation expansion happens : uses eval_antiquote *) +syntax "_cartouche_string" :: "cartouche_position \ _" ("_") -*) -(* stuff over global environment : *) +ML\ +structure Cartouche_Grammar = struct + fun list_comb_mk cst n c = list_comb (Syntax.const cst, String_Syntax.mk_bits_syntax n c) + val nil1 = Syntax.const @{const_syntax String.empty_literal} + fun cons1 c l = list_comb_mk @{const_syntax String.Literal} 7 c $ l + + val default = + [ ( "char list" + , ( Const (@{const_syntax Nil}, @{typ "char list"}) + , fn c => fn l => Syntax.const @{const_syntax Cons} $ list_comb_mk @{const_syntax Char} 8 c $ l + , snd)) + , ( "String.literal", (nil1, cons1, snd))] +end +\ + +ML\ +fun parse_translation_cartouche binding l f_integer accu = + let val cartouche_type = Attrib.setup_config_string binding (K (fst (hd l))) + (* if there is no type specified, by default we set the first element + to be the default type of cartouches *) in + fn ctxt => + let val cart_type = Config.get ctxt cartouche_type in + case List.find (fn (s, _) => s = cart_type) l of + NONE => error ("Unregistered return type for the cartouche: \"" ^ cart_type ^ "\"") + | SOME (_, (nil0, cons, f)) => + string_tr f (f_integer, cons, nil0) accu (Symbol_Pos.cartouche_content o Symbol_Pos.explode) + end + end +\ + +text\The following registration of this cartouche for strings is fails because it has + already been done in the surrounding Isabelle/DOF environment... \ (* -ML\ Document.state();\ -ML\ Session.get_keywords(); (* this looks to be really session global. *) - Outer_Syntax.command; \ -ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \ +parse_translation \ + [( @{syntax_const "_cartouche_string"} + , parse_translation_cartouche \<^binding>\cartouche_type\ Cartouche_Grammar.default (K I) ())] +\ *) +(* test for this cartouche... *) +term "\A \ B\ = ''''" -section\Inner Syntax\ -text\MORE TO COME : cartouches\ -ML\Sign.add_trrules\ chapter*[c::conclusion]\Conclusion\ -text\More to come\ +text\ This interactive Isabelle Programming Cook-Book represents my current way +to view and explain Isabelle programming API's to students and collaborators. +It differs from the reference manual in some places on purpose, since I believe +that a lot of internal Isabelle API's need a more conceptual view on what is happening +(even if this conceptual view is at times over-abstracting a little). +It also offers a deliberately different abstraction to the explanations in form of comments +in the sources or in the Reference Manual. + +The descriptions of some sources may appear lengthy and repetitive and redundant - but this kind +of repetition not only give an idea of the chosen abstraction levels on some interfaces, but also +represents --- since this is a "living document" (a notion I owe Simon Foster) --- a continuous check +for each port of our material to each more recent Isabelle version, where the first attempts +to load it will fail, but give another source of information over the modifications of +the system interface for parts relevant to our own development work. + +All hints and contributions of collegues and collaborators are greatly welcomed; all errors +and the roughness of this presentation is entirely my fault. +\ (*<*) section*[bib::bibliography]\Bibliography\ From 4329bd2602456a13a375042932c3d465a2fdd935 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 17 Jul 2019 08:23:54 +0200 Subject: [PATCH 06/10] A little more explanations, more ontolgical control --- .../TR_MyCommentedIsabelle.thy | 97 +++++++++++-------- 1 file changed, 54 insertions(+), 43 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index d5105ed2..7927aa7e 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -124,7 +124,7 @@ text\\verb+text\\<^emph>\This is a text.\\+\and desplayed in the Isabelle/jedit front-end at the sceen by:\ figure*[fig2::figure, relative_width="100",src="''figures/text-element''"] - \A text-element as presented in Isabelle/jedit. \ + \A text-element as presented in Isabelle/jedit.\ text\ text-commands, ML- commands (and in principle any other command) can be seen as \<^emph>\quotations\ over the underlying SML environment (similar to OCaml or Haskell). @@ -311,8 +311,14 @@ ML\ subsection*[t213::example]\Mechanism 2 : Extending the Global Context $\theta$ by User Data \ +text\A central mechanism for constructing user-defined data is by the \<^verbatim>\Generic_Data\ SML functor. +A plugin needing some data \<^verbatim>\T\ and providing it with implementations for an +\<^verbatim>\empty\, and operations \<^verbatim>\merge\ and \<^verbatim>\extend\, can construct a lense with operations +\<^verbatim>\get\ and \<^verbatim>\put\ that attach this data into the generic system context. Rather than using +unsynchronized SML mutable variables, this is the mechanism to introduce component local +data in Isabelle, which allows to manage this data for the necessary backtrack- and synchronization +features in the pervasively parallel evaluation framework that Isabelle as a system represents.\ ML \ - datatype X = mt val init = mt; val ext = I @@ -334,7 +340,7 @@ structure Data = Generic_Data \ -section\ The LCF-Kernel: terms, types, theories, proof\_contexts, thms \ +section*[lcfk::technical]\ The LCF-Kernel: terms, types, theories, proof\_contexts, thms \ text\The classical LCF-style \<^emph>\kernel\ is about \<^enum> Types and terms of a typed $\lambda$-Calculus including constant symbols, free variables, $\lambda$-binder and application, @@ -346,7 +352,7 @@ text\The classical LCF-style \<^emph>\kernel\ is about \ -subsection\ Terms and Types \ +subsection*[termstypes::technical]\ Terms and Types \ text \A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \ ML\ open Term; signature TERM' = sig @@ -405,28 +411,28 @@ operators of the HOL logic specific constructors and destructors: \ ML\ -HOLogic.boolT : typ; -HOLogic.mk_Trueprop: term -> term; -HOLogic.dest_Trueprop: term -> term; -HOLogic.Trueprop_conv: conv -> conv; -HOLogic.mk_setT: typ -> typ; -HOLogic.dest_setT: typ -> typ; -HOLogic.Collect_const: typ -> term; -HOLogic.mk_Collect: string * typ * term -> term; -HOLogic.mk_mem: term * term -> term; -HOLogic.dest_mem: term -> term * term; -HOLogic.mk_set: typ -> term list -> term; -HOLogic.conj_intr: Proof.context -> thm -> thm -> thm; -HOLogic.conj_elim: Proof.context -> thm -> thm * thm; -HOLogic.conj_elims: Proof.context -> thm -> thm list; -HOLogic.conj: term; -HOLogic.disj: term; -HOLogic.imp: term; -HOLogic.Not: term; -HOLogic.mk_not: term -> term; -HOLogic.mk_conj: term * term -> term; -HOLogic.dest_conj: term -> term list; -HOLogic.conjuncts: term -> term list; +HOLogic.boolT : typ; +HOLogic.mk_Trueprop : term -> term; (* the embedder of bool to prop fundamenyal for HOL *) +HOLogic.dest_Trueprop : term -> term; +HOLogic.Trueprop_conv : conv -> conv; +HOLogic.mk_setT : typ -> typ; (* ML level type constructor set *) +HOLogic.dest_setT : typ -> typ; +HOLogic.Collect_const : typ -> term; +HOLogic.mk_Collect : string * typ * term -> term; +HOLogic.mk_mem : term * term -> term; +HOLogic.dest_mem : term -> term * term; +HOLogic.mk_set : typ -> term list -> term; +HOLogic.conj_intr : Proof.context -> thm -> thm -> thm; (* some HOL-level derived-inferences *) +HOLogic.conj_elim : Proof.context -> thm -> thm * thm; +HOLogic.conj_elims : Proof.context -> thm -> thm list; +HOLogic.conj : term; (* some ML level logical constructors *) +HOLogic.disj : term; +HOLogic.imp : term; +HOLogic.Not : term; +HOLogic.mk_not : term -> term; +HOLogic.mk_conj : term * term -> term; +HOLogic.dest_conj : term -> term list; +HOLogic.conjuncts : term -> term list; (* ... *) \ @@ -499,7 +505,7 @@ val true = Sign.typ_instance @{theory} (ty', generalize_typ ty) text\... or more general variants thereof that are parameterized by the indexes for schematic type variables instead of assuming just @{ML "0"}. \ -text\ Example:\ +text*[exo4::example]\ Example:\ ML\val t = generalize_term @{term "[]"}\ text @@ -538,7 +544,8 @@ val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t) val t'' = Term.map_types (Term_Subst.instantiateT S') (t) \ -subsection\ Type-Inference (= inferring consistent type information if possible) \ +text\A more abstract env for variable management in tactic proofs. A bit difficult to use +outside the very closed-up tracks of conventional use...\ ML\ Consts.the_const; (* T is a kind of signature ... *) @@ -546,7 +553,7 @@ Variable.import_terms; Vartab.update; \ -subsection\ Type-Inference (= inferring consistent type information if possible) \ +subsection*[t232::technical]\ Type-Inference (= inferring consistent type information if possible) \ text\ Type inference eliminates also joker-types such as @{ML dummyT} and produces instances for schematic type variables where necessary. In the case of success, @@ -557,14 +564,14 @@ Type_Infer_Context.infer_types: Proof.context -> term list -> term list -subsection\ thy and the signature interface\ +subsection*[t233::technical]\ theories and the signature interface\ ML\ Sign.tsig_of: theory -> Type.tsig; Sign.syn_of : theory -> Syntax.syntax; Sign.of_sort : theory -> typ * sort -> bool ; \ -subsection\ Thm's and the LCF-Style, "Mikro"-Kernel \ +subsection*[t234::technical]\Thm's and the LCF-Style, "Mikro"-Kernel \ text\ The basic constructors and operations on theorems@{file "$ISABELLE_HOME/src/Pure/thm.ML"}, a set of derived (Pure) inferences can be found in @{file "$ISABELLE_HOME/src/Pure/drule.ML"}. @@ -681,7 +688,7 @@ ML\ \ -subsection\ Theories \ +subsection*[t235::technical]\ Theories \ text \ This structure yields the datatype \verb*thy* which becomes the content of \verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel, @@ -719,7 +726,7 @@ Theory.end_theory: theory -> theory; \ -section\Backward Proofs: Tactics, Tacticals and Goal-States\ +section*[t24::technical]\Backward Proofs: Tactics, Tacticals and Goal-States\ text\At this point, we leave the Pure-Kernel and start to describe the first layer on top of it, involving support for specific styles of reasoning and automation of reasoning.\ @@ -830,9 +837,13 @@ Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and Gentzen Sequent Deduction.\ -section\The classical goal package\ - -ML\ open Goal; +section*[goalp::technical]\The classical goal package\ +text\The main mechanism in Isabelle as an LCF-style system is to produce @{ML_type thm}'s +in backward-style via tactics as described in @{technical "t24"}. Given a context +--- be it global as @{ML_type theory} or be it inside a proof-context as @{ML_type Proof.context}, +user-programmed verification of (type-checked) terms or just strings can be done via the operations: +\ +ML\ Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm; Goal.prove_global : theory -> string list -> term list -> term -> @@ -881,7 +892,7 @@ ML\ Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> text\A paradigmatic example: "text" is defined by: \ -(* +(* --- commented out since this code is not re-executable val _ = Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true}); @@ -896,7 +907,7 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl -subsection \Transaction Management in the Isar-Engine : The Toplevel \ +subsection*[transmgt::technical] \Transaction Management in the Isar-Engine : The Toplevel \ ML\ @@ -992,7 +1003,7 @@ Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transiti \ -subsection\ Configuration flags of fixed type in the Isar-engine. \ +subsection*[conf::technical]\ Configuration flags of fixed type in the Isar-engine. \ text\The toplevel also provides an infrastructure for managing configuration options for system components. Based on a sum-type @{ML_type Config.value } with the alternatives \<^verbatim>\ Bool of bool | Int of int | Real of real | String of string\ @@ -1032,7 +1043,7 @@ val C = Synchronized.var "Pretty.modes" "latEEex"; Synchronized.value C; \ -chapter\Front-End \ +chapter*[frontend::technical]\Front-End \ text\In the following chapter, we turn to the right part of the system architecture shown in @{docitem \architecture\}: The PIDE ("Prover-IDE") layer @{cite "DBLP:conf/itp/Wenzel14"} @@ -1396,7 +1407,7 @@ end subsection\A Lexer Configuration Example\ ML\ - +(* MORE TO COME *) \ @@ -1698,7 +1709,7 @@ val _ = uncheck_terms = uncheck_terms}); *) -subsection \Example\ +subsection*[ex33::example] \Example\ ML\ (* Recall the Arg-interface to the more high-level, more Isar-specific parsers: *) @@ -1883,7 +1894,7 @@ As one can see, check-routines internally generate the markup. \ -section\Inner Syntax Cartouches\ +section*[cartouches::technical]\Inner Syntax Cartouches\ text\ The cascade-syntax principle underlying recent isabelle versions requires a particular mechanism, called "cartouche" by Makarius who was influenced by French Wine and French culture when designing this. From 4c4194d468a15856ad8b8e221e5ea9fea528e908 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 17 Jul 2019 10:21:34 +0200 Subject: [PATCH 07/10] Proof Example --- Isa_DOF.thy | 2 -- .../TR_MyCommentedIsabelle.thy | 35 +++++++++++++++++-- 2 files changed, 33 insertions(+), 4 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 5e3ff4bc..e640c511 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -744,8 +744,6 @@ consts ISA_docitem_attr :: "string \ string \ 'a" ( \ \Dynamic setup of inner syntax cartouche\ - -(* PORT TO ISABELLE2018 *) ML \ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: HOL/ex/Cartouche_Examples.thy diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 7927aa7e..98a7da24 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -843,11 +843,42 @@ in backward-style via tactics as described in @{technical "t24"}. Given a contex --- be it global as @{ML_type theory} or be it inside a proof-context as @{ML_type Proof.context}, user-programmed verification of (type-checked) terms or just strings can be done via the operations: \ -ML\ + + +ML\ Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm; Goal.prove_global : theory -> string list -> term list -> term -> - ({context: Proof.context, prems: thm list} -> tactic) -> thm + ({context: Proof.context, prems: thm list} -> tactic) -> thm; +(* ... and many more variants. *) +\ + +subsection*[ex211::example]\Proof example\ + +text\The proof:\ + +lemma "(10::int) + 2 = 12" by simp + +text\... represents itself at the SML interface as follows:\ + +ML\val tt = HOLogic.mk_Trueprop (Syntax.read_term @{context} "(10::int) + 2 = 12"); + (* read_term parses and type-checks its string argument; + HOLogic.mk_Trueprop wraps the embedder from @{ML_type "bool"} to + @{ML_type "prop"} from Pure. *) + +val thm1 = Goal.prove_global @{theory} (* global context *) + [] (* name ? *) + [] (* local assumption context *) + (tt) (* parsed goal *) + (fn _ => simp_tac @{context} 1) (* proof tactic *) +\ + + + +subsection*[exo44::example]\Example\ + +ML\ +Goal.prove_global @{theory} ["2::int + 3 = 5"] \ section\The Isar Engine\ From 869644e3b58d6766a15b910417e3593f4a0b8904 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 17 Jul 2019 10:24:41 +0200 Subject: [PATCH 08/10] Proof Example --- .../TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 98a7da24..d133aab4 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -564,10 +564,10 @@ Type_Infer_Context.infer_types: Proof.context -> term list -> term list -subsection*[t233::technical]\ theories and the signature interface\ +subsection*[t233::technical]\ Theories and the Signature API\ ML\ -Sign.tsig_of: theory -> Type.tsig; -Sign.syn_of : theory -> Syntax.syntax; +Sign.tsig_of : theory -> Type.tsig; +Sign.syn_of : theory -> Syntax.syntax; Sign.of_sort : theory -> typ * sort -> bool ; \ From 5ff3217493f7ac6e32ece447ef8adaf4f7ec40e3 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 17 Jul 2019 10:47:25 +0200 Subject: [PATCH 09/10] Internal Layout Polishing --- .../TR_MyCommentedIsabelle.thy | 1018 ++++++++--------- 1 file changed, 488 insertions(+), 530 deletions(-) diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index d133aab4..97df321b 100644 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -18,43 +18,43 @@ text*[bu::author, text*[abs::abstract, keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Programming Guide'', ''Tactic Programming'']"]\ -While Isabelle is mostly known as part of Isabelle/HOL (an interactive -theorem prover), it actually provides a system framework for developing a wide -spectrum of applications. A particular strength of the Isabelle framework is the -combination of text editing, formal verification, and code generation. - -This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary -text to the unfortunately somewhat outdated "The Isabelle Cookbook" in -\url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged -not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jEdit -@{cite "DBLP:journals/corr/Wenzel14"}in order to make experiments on the running code. - -This text is written itself in Isabelle/Isar using a specific document ontology -for technical reports. It is intended to be a "living document", i.e. it is not only -used for generating a static, conventional .pdf, but also for direct interactive -exploration in Isabelle/jedit. This way, types, intermediate results of computations and -checks can be repeated by the reader who is invited to interact with this document. -Moreover, the textual parts have been enriched with a maximum of formal content -which makes this text re-checkable at each load and easier maintainable. + While Isabelle is mostly known as part of Isabelle/HOL (an interactive + theorem prover), it actually provides a system framework for developing a wide + spectrum of applications. A particular strength of the Isabelle framework is the + combination of text editing, formal verification, and code generation. + + This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary + text to the unfortunately somewhat outdated "The Isabelle Cookbook" in + \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged + not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jEdit + @{cite "DBLP:journals/corr/Wenzel14"}in order to make experiments on the running code. + + This text is written itself in Isabelle/Isar using a specific document ontology + for technical reports. It is intended to be a "living document", i.e. it is not only + used for generating a static, conventional .pdf, but also for direct interactive + exploration in Isabelle/jedit. This way, types, intermediate results of computations and + checks can be repeated by the reader who is invited to interact with this document. + Moreover, the textual parts have been enriched with a maximum of formal content + which makes this text re-checkable at each load and easier maintainable. \ chapter*[intro::introduction]\ Introduction \ -text\ -While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as part of Isabelle/HOL (an interactive theorem prover), it actually -provides a system framework for developing a wide spectrum of applications. A particular strength of -the Isabelle framework is the combination of text editing, formal verification, and code generation. -This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary text to the -unfortunately somewhat outdated "The Isabelle Cookbook" in -\url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged not only to consider -the generated .pdf, but also consult the loadable version in Isabelle/jedit in order to make -experiments on the running code. This text is written itself in Isabelle/Isar using a specific -document ontology for technical reports. It is intended to be a "living document", i.e. it is not -only used for generating a static, conventional .pdf, but also for direct interactive exploration -in Isabelle/jedit. This way, types, intermediate results of computations and checks can be -repeated by the reader who is invited to interact with this document. Moreover, the textual -parts have been enriched with a maximum of formal content which makes this text re-checkable at -each load and easier maintainable.\ +text\ While Isabelle @{cite "DBLP:books/sp/NipkowPW02"} is mostly known as part of Isabelle/HOL + (an interactive theorem prover), it actually provides a system framework for developing a wide + spectrum of applications. A particular strength of the Isabelle framework is the combination + of text editing, formal verification, and code generation. This is a programming-tutorial of + Isabelle and Isabelle/HOL, a complementary text to the unfortunately somewhat outdated + "The Isabelle Cookbook" in \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader + is encouraged not only to consider the generated .pdf, but also consult the loadable version + in Isabelle/jedit in order to make experiments on the running code. This text is written + itself in Isabelle/Isar using a specific document ontology for technical reports. It is + intended to be a "living document", i.e. it is not only used for generating a static, + conventional .pdf, but also for direct interactive exploration in Isabelle/jedit. This way, + types, intermediate results of computations and checks can be repeated by the reader who is + invited to interact with this document. Moreover, the textual parts have been enriched with a + maximum of formal content which makes this text re-checkable at each load and easier + maintainable.\ figure*[architecture::figure,relative_width="80",src="''figures/isabelle-architecture''"]\ The system architecture of Isabelle (left-hand side) and the @@ -62,10 +62,10 @@ figure*[architecture::figure,relative_width="80",src="''figures/isabelle-archite the IDE (right-hand side). \ text\This cookbook roughly follows the Isabelle system architecture shown in -@{figure "architecture"}, and, to be more precise, more or less in the bottom-up order. + @{figure "architecture"}, and, to be more precise, more or less in the bottom-up order. -We start from the basic underlying SML platform over the Kernels to the tactical layer -and end with a discussion over the front-end technologies. + We start from the basic underlying SML platform over the Kernels to the tactical layer + and end with a discussion over the front-end technologies. \ chapter*[t1::technical]\ SML and Fundamental SML libraries \ @@ -73,10 +73,10 @@ chapter*[t1::technical]\ SML and Fundamental SML libraries \ section*[t11::technical] "ML, Text and Antiquotations" text\Isabelle is written in SML, the "Standard Meta-Language", which is is an impure functional -programming language allowing, in principle, mutable variables and side-effects. -The following Isabelle/Isar commands allow for accessing the underlying SML interpreter -of Isabelle directly. In the example, a mutable variable X is declared, defined to 0 and updated; -and finally re-evaluated leading to output: \ + programming language allowing, in principle, mutable variables and side-effects. + The following Isabelle/Isar commands allow for accessing the underlying SML interpreter + of Isabelle directly. In the example, a mutable variable X is declared, defined to 0 and updated; + and finally re-evaluated leading to output: \ ML\ val X = Unsynchronized.ref 0; X:= !X + 1; @@ -84,10 +84,10 @@ ML\ val X = Unsynchronized.ref 0; \ text\However, since Isabelle is a platform involving parallel execution, concurrent computing, and, -as an interactive environment, involves backtracking / re-evaluation as a consequence of user- -interaction, imperative programming is discouraged and nearly never used in the entire Isabelle -code-base @{cite "DBLP:conf/mkm/BarrasGHRTWW13"}. -The preferred programming style is purely functional: \ + as an interactive environment, involves backtracking / re-evaluation as a consequence of user- + interaction, imperative programming is discouraged and nearly never used in the entire Isabelle + code-base @{cite "DBLP:conf/mkm/BarrasGHRTWW13"}. + The preferred programming style is purely functional: \ ML\ fun fac x = if x = 0 then 1 else x * fac(x-1) ; fac 10; @@ -98,20 +98,20 @@ ML\ type state = { a : int, b : string} \ text\ The faculty function is defined and executed; the (sub)-interpreter in Isar -works in the conventional read-execute-print loop for each statement separated by a ";". -Functions, types, data-types etc. can be grouped to modules (called \<^emph>\structures\) which can -be constrained to interfaces (called \<^emph>\signatures\) and even be parametric structures -(called \<^emph>\functors\). \ + works in the conventional read-execute-print loop for each statement separated by a ";". + Functions, types, data-types etc. can be grouped to modules (called \<^emph>\structures\) which can + be constrained to interfaces (called \<^emph>\signatures\) and even be parametric structures + (called \<^emph>\functors\). \ text\ The Isabelle/Isar interpreter (called \<^emph>\toplevel\ ) is extensible; by a mixture of SML -and Isar-commands, domain-specific components can be developed and integrated into the system -on the fly. Actually, the Isabelle system code-base consists mainly of SML and \<^verbatim>\.thy\-files -containing such mixtures of Isar commands and SML. \ + and Isar-commands, domain-specific components can be developed and integrated into the system + on the fly. Actually, the Isabelle system code-base consists mainly of SML and \<^verbatim>\.thy\-files + containing such mixtures of Isar commands and SML. \ text\ Besides the ML-command used in the above examples, there are a number of commands -representing text-elements in Isabelle/Isar; text commands can be interleaved arbitraryly -with other commands. Text in text-commands may use LaTeX and is used for type-setting -documentations in a kind of literate programming style. \ + representing text-elements in Isabelle/Isar; text commands can be interleaved arbitraryly + with other commands. Text in text-commands may use LaTeX and is used for type-setting + documentations in a kind of literate programming style. \ text\So: the text command for:\ @@ -127,24 +127,23 @@ figure*[fig2::figure, relative_width="100",src="''figures/text-element''"] \A text-element as presented in Isabelle/jedit.\ text\ text-commands, ML- commands (and in principle any other command) can be seen as -\<^emph>\quotations\ over the underlying SML environment (similar to OCaml or Haskell). -Linking these different sorts of quotations with each other and the underlying SML-envirnment -is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a programming -technique to specify expressions or patterns in a quotation, parsed in the context of the -enclosing expression or pattern where the quotation is. Another way to understand this concept: -anti-quotations are "semantic macros" that produce a value for the surrounding context -(ML, text, HOL, whatever) depending on local arguments and the underlying logical context. - -The way an antiquotation is specified depends on the quotation expander: typically a specific -character and an identifier, or specific parentheses and a complete expression or pattern.\ + \<^emph>\quotations\ over the underlying SML environment (similar to OCaml or Haskell). + Linking these different sorts of quotations with each other and the underlying SML-envirnment + is supported via \<^emph>\antiquotations\'s. Generally speaking, antiquotations are a programming + technique to specify expressions or patterns in a quotation, parsed in the context of the + enclosing expression or pattern where the quotation is. Another way to understand this concept: + anti-quotations are "semantic macros" that produce a value for the surrounding context + (ML, text, HOL, whatever) depending on local arguments and the underlying logical context. + + The way an antiquotation is specified depends on the quotation expander: typically a specific + character and an identifier, or specific parentheses and a complete expression or pattern.\ text\ In Isabelle documentations, antiquotation's were heavily used to enrich literate explanations -and documentations by "formal content", i.e. machine-checked, typed references -to all sorts of entities in the context of the interpreting environment. -Formal content allows for coping with sources that rapidly evolve and were developed by -distributed teams as is typical in open-source developments. -A paradigmatic example for antiquotation in Texts and Program snippets is here: -\ + and documentations by "formal content", i.e. machine-checked, typed references + to all sorts of entities in the context of the interpreting environment. + Formal content allows for coping with sources that rapidly evolve and were developed by + distributed teams as is typical in open-source developments. + A paradigmatic example for antiquotation in Texts and Program snippets is here:\ text\ @{footnote \sdf\}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\ ML\ val x = @{thm refl}; @@ -155,48 +154,45 @@ ML\ val x = @{thm refl}; text\... which we will describe in more detail later. \ text\In a way, literate specification attempting to maximize its formal content is a way to -ensure "Agile Development" in a (theory)-document development, at least for its objectives, -albeit not for its popular methods and processes like SCRUM. \ + ensure "Agile Development" in a (theory)-document development, at least for its objectives, + albeit not for its popular methods and processes like SCRUM. \ paragraph\ - A maximum of formal content inside text documentation also ensures the - consistency of this present text with the underlying Isabelle version.\ + A maximum of formal content inside text documentation also ensures the + consistency of this present text with the underlying Isabelle version.\ section\The Isabelle/Pure bootstrap\ text\It is instructive to study the fundamental bootstrapping sequence of the Isabelle system; - it is written in the Isar format and gives an idea of the global module dependencies: - @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}. Loading this file - (for example by hovering over this hyperlink in the antiquotation holding control or - command key in Isabelle/jedit and activating it) allows the Isabelle IDE - to support hyperlinking \<^emph>\inside\ the Isabelle source.\ + it is written in the Isar format and gives an idea of the global module dependencies: + @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}. Loading this file + (for example by hovering over this hyperlink in the antiquotation holding control or + command key in Isabelle/jedit and activating it) allows the Isabelle IDE + to support hyperlinking \<^emph>\inside\ the Isabelle source.\ -text\The bootstrapping sequence is also reflected in the following diagram -@{figure "architecture"}. \ +text\The bootstrapping sequence is also reflected in the following diagram @{figure "architecture"}.\ section*[t12::technical] "Elements of the SML library"; text\Elements of the @{file "$ISABELLE_HOME/src/Pure/General/basics.ML"} SML library -are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions -except those generated by the specific "error" function are discouraged in Isabelle -source programming since they might produce races. Finally, a number of commonly -used "squigglish" combinators is listed: -\ -ML\ - Bind : exn; - Chr : exn; - Div : exn; - Domain : exn; - Fail : string -> exn; - Match : exn; - Overflow : exn; - Size : exn; - Span : exn; - Subscript : exn; + are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions + except those generated by the specific "error" function are discouraged in Isabelle + source programming since they might produce races. Finally, a number of commonly + used "squigglish" combinators is listed:\ - exnName : exn -> string ; (* -- very interesting to query an unknown exception *) - exnMessage : exn -> string ; -\ +ML\ Bind : exn; + Chr : exn; + Div : exn; + Domain : exn; + Fail : string -> exn; + Match : exn; + Overflow : exn; + Size : exn; + Span : exn; + Subscript : exn; + + exnName : exn -> string ; (* -- very interesting to query an unknown exception *) + exnMessage : exn -> string ;\ ML\ op ! : 'a Unsynchronized.ref -> 'a; @@ -215,12 +211,12 @@ K: 'a -> 'b -> 'a \ text\Some basic examples for the programming style using these combinators can be found in the - "The Isabelle Cookbook" section 2.3.\ + "The Isabelle Cookbook" section 2.3.\ text\An omnipresent data-structure in the Isabelle SML sources are tables -implemented in @{file "$ISABELLE_HOME/src/Pure/General/table.ML"}. These -generic tables are presented in an efficient purely functional implementation using -balanced 2-3 trees. Key operations are:\ + implemented in @{file "$ISABELLE_HOME/src/Pure/General/table.ML"}. These + generic tables are presented in an efficient purely functional implementation using + balanced 2-3 trees. Key operations are:\ ML\ signature TABLE_reduced = sig @@ -246,45 +242,45 @@ chapter*[t2::technical] \ Prover Architecture \ section*[t21::technical] \ The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts \ text\ What I call the 'Nano-Kernel' in Isabelle can also be seen as an acyclic theory graph. -The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}. -My notion is a bit criticisable since this component, which provides the type of @{ML_type theory} -and @{ML_type Proof.context}, is not that Nano after all. -However, these type are pretty empty place-holders at that level and the content of -@{file "$ISABELLE_HOME/src/Pure/theory.ML"} is registered much later. -The sources themselves mention it as "Fundamental Structure". -In principle, theories and proof contexts could be REGISTERED as user data inside contexts. -The chosen specialization is therefore an acceptable meddling of the abstraction "Nano-Kernel" -and its application context: Isabelle. - -Makarius himself says about this structure: - -"Generic theory contexts with unique identity, arbitrarily typed data, -monotonic development graph and history support. Generic proof -contexts with arbitrarily typed data." - -In my words: a context is essentially a container with -\<^item> an id -\<^item> a list of parents (so: the graph structure) -\<^item> a time stamp and -\<^item> a sub-context relation (which uses a combination of the id and the time-stamp to - establish this relation very fast whenever needed; it plays a crucial role for the - context transfer in the kernel. - - -A context comes in form of three 'flavours': -\<^item> theories : @{ML_type theory}'s, containing a syntax and axioms, but also - user-defined data and configuration information. -\<^item> Proof-Contexts: @{ML_type Proof.context} - containing theories but also additional information if Isar goes into prove-mode. - In general a richer structure than theories coping also with fixes, facts, goals, - in order to support the structured Isar proof-style. -\<^item> Generic: @{ML_type Context.generic }, i.e. the sum of both. - -All context have to be seen as mutable; so there are usually transformations defined on them -which are possible as long as a particular protocol (\<^verbatim>\begin_thy\ - \<^verbatim>\end_thy\ etc) are respected. - -Contexts come with type user-defined data which is mutable through the entire lifetime of -a context. + The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}. + My notion is a bit criticisable since this component, which provides the type of @{ML_type theory} + and @{ML_type Proof.context}, is not that Nano after all. + However, these type are pretty empty place-holders at that level and the content of + @{file "$ISABELLE_HOME/src/Pure/theory.ML"} is registered much later. + The sources themselves mention it as "Fundamental Structure". + In principle, theories and proof contexts could be REGISTERED as user data inside contexts. + The chosen specialization is therefore an acceptable meddling of the abstraction "Nano-Kernel" + and its application context: Isabelle. + + Makarius himself says about this structure: + + "Generic theory contexts with unique identity, arbitrarily typed data, + monotonic development graph and history support. Generic proof + contexts with arbitrarily typed data." + + In my words: a context is essentially a container with + \<^item> an id + \<^item> a list of parents (so: the graph structure) + \<^item> a time stamp and + \<^item> a sub-context relation (which uses a combination of the id and the time-stamp to + establish this relation very fast whenever needed; it plays a crucial role for the + context transfer in the kernel. + + + A context comes in form of three 'flavours': + \<^item> theories : @{ML_type theory}'s, containing a syntax and axioms, but also + user-defined data and configuration information. + \<^item> Proof-Contexts: @{ML_type Proof.context} + containing theories but also additional information if Isar goes into prove-mode. + In general a richer structure than theories coping also with fixes, facts, goals, + in order to support the structured Isar proof-style. + \<^item> Generic: @{ML_type Context.generic }, i.e. the sum of both. + + All context have to be seen as mutable; so there are usually transformations defined on them + which are possible as long as a particular protocol (\<^verbatim>\begin_thy\ - \<^verbatim>\end_thy\ etc) are respected. + + Contexts come with type user-defined data which is mutable through the entire lifetime of + a context. \ subsection*[t212::technical]\ Mechanism 1 : Core Interface. \ @@ -311,13 +307,15 @@ ML\ subsection*[t213::example]\Mechanism 2 : Extending the Global Context $\theta$ by User Data \ + text\A central mechanism for constructing user-defined data is by the \<^verbatim>\Generic_Data\ SML functor. -A plugin needing some data \<^verbatim>\T\ and providing it with implementations for an -\<^verbatim>\empty\, and operations \<^verbatim>\merge\ and \<^verbatim>\extend\, can construct a lense with operations -\<^verbatim>\get\ and \<^verbatim>\put\ that attach this data into the generic system context. Rather than using -unsynchronized SML mutable variables, this is the mechanism to introduce component local -data in Isabelle, which allows to manage this data for the necessary backtrack- and synchronization -features in the pervasively parallel evaluation framework that Isabelle as a system represents.\ + A plugin needing some data \<^verbatim>\T\ and providing it with implementations for an + \<^verbatim>\empty\, and operations \<^verbatim>\merge\ and \<^verbatim>\extend\, can construct a lense with operations + \<^verbatim>\get\ and \<^verbatim>\put\ that attach this data into the generic system context. Rather than using + unsynchronized SML mutable variables, this is the mechanism to introduce component local + data in Isabelle, which allows to manage this data for the necessary backtrack- and synchronization + features in the pervasively parallel evaluation framework that Isabelle as a system represents.\ + ML \ datatype X = mt val init = mt; @@ -354,7 +352,7 @@ text\The classical LCF-style \<^emph>\kernel\ is about subsection*[termstypes::technical]\ Terms and Types \ text \A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \ -ML\ open Term; +ML\ (* open Term; *) signature TERM' = sig (* ... *) type indexname = string * int @@ -406,34 +404,33 @@ text\Note that the SML interpreter is configured that he will actually pri pretty much like a string. This can be confusing at times.\ text\Note, furthermore, that there is a programming API for the HOL-instance of Isabelle: -it is contained in @{file "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers for many -operators of the HOL logic specific constructors and destructors: -\ + it is contained in @{file "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers for many + operators of the HOL logic specific constructors and destructors:\ ML\ -HOLogic.boolT : typ; -HOLogic.mk_Trueprop : term -> term; (* the embedder of bool to prop fundamenyal for HOL *) -HOLogic.dest_Trueprop : term -> term; -HOLogic.Trueprop_conv : conv -> conv; -HOLogic.mk_setT : typ -> typ; (* ML level type constructor set *) -HOLogic.dest_setT : typ -> typ; -HOLogic.Collect_const : typ -> term; -HOLogic.mk_Collect : string * typ * term -> term; -HOLogic.mk_mem : term * term -> term; -HOLogic.dest_mem : term -> term * term; -HOLogic.mk_set : typ -> term list -> term; -HOLogic.conj_intr : Proof.context -> thm -> thm -> thm; (* some HOL-level derived-inferences *) -HOLogic.conj_elim : Proof.context -> thm -> thm * thm; -HOLogic.conj_elims : Proof.context -> thm -> thm list; -HOLogic.conj : term; (* some ML level logical constructors *) -HOLogic.disj : term; -HOLogic.imp : term; -HOLogic.Not : term; -HOLogic.mk_not : term -> term; -HOLogic.mk_conj : term * term -> term; -HOLogic.dest_conj : term -> term list; -HOLogic.conjuncts : term -> term list; -(* ... *) + HOLogic.boolT : typ; + HOLogic.mk_Trueprop : term -> term; (* the embedder of bool to prop fundamenyal for HOL *) + HOLogic.dest_Trueprop : term -> term; + HOLogic.Trueprop_conv : conv -> conv; + HOLogic.mk_setT : typ -> typ; (* ML level type constructor set *) + HOLogic.dest_setT : typ -> typ; + HOLogic.Collect_const : typ -> term; + HOLogic.mk_Collect : string * typ * term -> term; + HOLogic.mk_mem : term * term -> term; + HOLogic.dest_mem : term -> term * term; + HOLogic.mk_set : typ -> term list -> term; + HOLogic.conj_intr : Proof.context -> thm -> thm -> thm; (* some HOL-level derived-inferences *) + HOLogic.conj_elim : Proof.context -> thm -> thm * thm; + HOLogic.conj_elims : Proof.context -> thm -> thm list; + HOLogic.conj : term; (* some ML level logical constructors *) + HOLogic.disj : term; + HOLogic.imp : term; + HOLogic.Not : term; + HOLogic.mk_not : term -> term; + HOLogic.mk_conj : term * term -> term; + HOLogic.dest_conj : term -> term list; + HOLogic.conjuncts : term -> term list; + (* ... *) \ @@ -447,27 +444,27 @@ text\ there is a joker type that can be added as place-holder during term ML\ Term.dummyT : typ \ ML\ -Sign.typ_instance: theory -> typ * typ -> bool; -Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv; -Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int; -Sign.const_type: theory -> string -> typ option; -Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*) -Sign.cert_term: theory -> term -> term; (* short-cut for the latter *) -Sign.tsig_of: theory -> Type.tsig (* projects the type signature *) + Sign.typ_instance: theory -> typ * typ -> bool; + Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv; + Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int; + Sign.const_type: theory -> string -> typ option; + Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*) + Sign.cert_term: theory -> term -> term; (* short-cut for the latter *) + Sign.tsig_of: theory -> Type.tsig (* projects the type signature *) \ text\ -@{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure -@{ML_structure "Type"} -which contains the heart of the type inference. -It also contains the type substitution type @{ML_type "Type.tyenv"} which is -is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"} -which in itself is a synonym for @{ML_type "'a Symtab.table"}, so -possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. \ + @{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure + @{ML_structure "Type"} + which contains the heart of the type inference. + It also contains the type substitution type @{ML_type "Type.tyenv"} which is + is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"} + which in itself is a synonym for @{ML_type "'a Symtab.table"}, so + possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. \ text\Note that @{emph \polymorphic variables\} are treated like constant symbols -in the type inference; thus, the following test, that one type is an instance of the -other, yields false: -\ + in the type inference; thus, the following test, that one type is an instance of the + other, yields false:\ + ML\ val ty = @{typ "'a option"}; val ty' = @{typ "int option"}; @@ -477,13 +474,14 @@ val Type("List.list",[S]) = @{typ "('a) list"}; (* decomposition example *) val false = Sign.typ_instance @{theory}(ty', ty); \ text\In order to make the type inference work, one has to consider @{emph \schematic\} -type variables, which are more and more hidden from the Isar interface. Consequently, -the typ antiquotation above will not work for schematic type variables and we have -to construct them by hand on the SML level: \ -ML\ -val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); -\ + type variables, which are more and more hidden from the Isar interface. Consequently, + the typ antiquotation above will not work for schematic type variables and we have + to construct them by hand on the SML level: \ + +ML\ val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); \ + text\ MIND THE "'" !!!\ + text \On this basis, the following @{ML_type "Type.tyenv"} is constructed: \ ML\ val tyenv = Sign.typ_match ( @{theory}) @@ -493,9 +491,9 @@ val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv; \ text\ Type generalization --- the conversion between free type variables and schematic -type variables --- is apparently no longer part of the standard API (there is a slightly -more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to -overcome this by a self-baked generalization function:\ + type variables --- is apparently no longer part of the standard API (there is a slightly + more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to + overcome this by a self-baked generalization function:\ ML\ val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort)); @@ -503,16 +501,14 @@ val generalize_term = Term.map_types generalize_typ; val true = Sign.typ_instance @{theory} (ty', generalize_typ ty) \ text\... or more general variants thereof that are parameterized by the indexes for schematic -type variables instead of assuming just @{ML "0"}. \ + type variables instead of assuming just @{ML "0"}. \ text*[exo4::example]\ Example:\ ML\val t = generalize_term @{term "[]"}\ -text -\Now we turn to the crucial issue of type-instantiation and with a given type environment -@{ML "tyenv"}. For this purpose, one has to switch to the low-level interface -@{ML_structure "Term_Subst"}. -\ +text\Now we turn to the crucial issue of type-instantiation and with a given type environment + @{ML "tyenv"}. For this purpose, one has to switch to the low-level interface + @{ML_structure "Term_Subst"}. \ ML\ Term_Subst.map_types_same : (typ -> typ) -> term -> term; @@ -529,7 +525,7 @@ Term_Subst.generalize: string list * string list -> int -> term -> term \ text \Apparently, a bizarre conversion between the old-style interface and -the new-style @{ML "tyenv"} is necessary. See the following example.\ + the new-style @{ML "tyenv"} is necessary. See the following example.\ ML\ val S = Vartab.dest tyenv; val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list; @@ -545,23 +541,18 @@ val t'' = Term.map_types (Term_Subst.instantiateT S') (t) \ text\A more abstract env for variable management in tactic proofs. A bit difficult to use -outside the very closed-up tracks of conventional use...\ + outside the very closed-up tracks of conventional use...\ -ML\ -Consts.the_const; (* T is a kind of signature ... *) -Variable.import_terms; -Vartab.update; -\ +ML\ Consts.the_const; (* T is a kind of signature ... *) + Variable.import_terms; + Vartab.update;\ subsection*[t232::technical]\ Type-Inference (= inferring consistent type information if possible) \ text\ Type inference eliminates also joker-types such as @{ML dummyT} and produces instances for schematic type variables where necessary. In the case of success, it produces a certifiable term. \ -ML\ -Type_Infer_Context.infer_types: Proof.context -> term list -> term list -\ - +ML\ Type_Infer_Context.infer_types: Proof.context -> term list -> term list \ subsection*[t233::technical]\ Theories and the Signature API\ @@ -652,12 +643,12 @@ text\Note that the transfer rule: \Gamma \vdash_{\theta'} \phi \qquad \qquad \end{prooftree} \] -which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design -and a remarkable difference to its sisters HOL-Light and HOL4; instead of transfer, these systems -reconstruct proofs in an enlarged global context instead of taking the result and converting it.\ + which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design + and a remarkable difference to its sisters HOL-Light and HOL4; instead of transfer, these systems + reconstruct proofs in an enlarged global context instead of taking the result and converting it.\ text\Besides the meta-logical (Pure) implication $\_\Longrightarrow \_$, the Kernel axiomatizes -also a Pure-Equality $\_ \equiv \_ $ used for definitions of constant symbols: \ + also a Pure-Equality $\_ \equiv \_ $ used for definitions of constant symbols: \ ML\ Thm.reflexive: cterm -> thm; Thm.symmetric: thm -> thm; @@ -691,10 +682,9 @@ ML\ subsection*[t235::technical]\ Theories \ text \ This structure yields the datatype \verb*thy* which becomes the content of -\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel, -which inspired me (bu) to this naming. + \verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel, + which inspired me (bu) to this naming. \ -\ ML\ (* intern Theory.Thy; @@ -721,29 +711,26 @@ Theory.defs_of: theory -> Defs.T; Theory.at_begin: (theory -> theory option) -> theory -> theory; Theory.at_end: (theory -> theory option) -> theory -> theory; Theory.begin_theory: string * Position.T -> theory list -> theory; -Theory.end_theory: theory -> theory; - -\ +Theory.end_theory: theory -> theory;\ section*[t24::technical]\Backward Proofs: Tactics, Tacticals and Goal-States\ text\At this point, we leave the Pure-Kernel and start to describe the first layer on top -of it, involving support for specific styles of reasoning and automation of reasoning.\ + of it, involving support for specific styles of reasoning and automation of reasoning.\ text\ \<^verbatim>\tactic\'s are in principle \<^emph>\relations\ on theorems @{ML_type "thm"}; this gives a natural way -to represent the fact that HO-Unification (and therefore the mechanism of rule-instantiation) -are non-deterministic in principle. Heuristics may choose particular preferences between -the theorems in the range of this relation, but the Isabelle Design accepts this fundamental -fact reflected at this point in the prover architecture. -This potentially infinite relation is implemented by a function of theorems to lazy lists -over theorems, which gives both sufficient structure for heuristic -considerations as well as a nice algebra, called \<^verbatim>\TACTICAL\'s, providing a bottom element -@{ML "no_tac"} (the function that always fails), the top-element @{ML "all_tac"} - (the function that never fails), sequential composition @{ML "op THEN"}, (serialized) -non-deterministic composition @{ML "op ORELSE"}, conditionals, repetitions over lists, etc. -The following is an excerpt of @{file "~~/src/Pure/tactical.ML"}: -\ + to represent the fact that HO-Unification (and therefore the mechanism of rule-instantiation) + are non-deterministic in principle. Heuristics may choose particular preferences between + the theorems in the range of this relation, but the Isabelle Design accepts this fundamental + fact reflected at this point in the prover architecture. + This potentially infinite relation is implemented by a function of theorems to lazy lists + over theorems, which gives both sufficient structure for heuristic + considerations as well as a nice algebra, called \<^verbatim>\TACTICAL\'s, providing a bottom element + @{ML "no_tac"} (the function that always fails), the top-element @{ML "all_tac"} + (the function that never fails), sequential composition @{ML "op THEN"}, (serialized) + non-deterministic composition @{ML "op ORELSE"}, conditionals, repetitions over lists, etc. + The following is an excerpt of @{file "~~/src/Pure/tactical.ML"}:\ ML\ signature TACTICAL = @@ -768,21 +755,20 @@ end \ text\The next layer in the architecture describes @{ML_type \tactic\}'s, i.e. basic operations on -theorems in a backward reasoning style (bottom up development of proof-trees). An initial goal-state -for some property @{term A} --- the \<^emph>\goal\ --- is constructed via the kernel -@{ML "Thm.trivial"}-operation into @{term "A \ A"}, and tactics either refine the premises ---- the \<^emph>\subgoals\ the of this meta-implication --- -producing more and more of them or eliminate them in subsequent goal-states. Subgoals of the form -@{term "B\<^sub>1 \ B\<^sub>2 \ A \ B\<^sub>3 \ B\<^sub>4 \ A"} can be eliminated via -the @{ML Tactic.assume_tac} - tactic, -and a subgoal @{term C\<^sub>m} can be refined via the theorem -@{term "E\<^sub>1 \ E\<^sub>2 \ E\<^sub>3 \ C\<^sub>m"} the @{ML Tactic.resolve_tac} - tactic to new subgoals -@{term "E\<^sub>1"},@{term "E\<^sub>2"}, @{term "E\<^sub>3"}. In case that a theorem used for resolution -has no premise @{term "E\<^sub>i"}, the subgoal @{term C\<^sub>m} is also eliminated ("closed"). - -The following abstract of the most commonly used @{ML_type \tactic\}'s drawn from -@{file "~~/src/Pure/tactic.ML"} looks as follows: -\ + theorems in a backward reasoning style (bottom up development of proof-trees). An initial goal-state + for some property @{term A} --- the \<^emph>\goal\ --- is constructed via the kernel + @{ML "Thm.trivial"}-operation into @{term "A \ A"}, and tactics either refine the premises + --- the \<^emph>\subgoals\ the of this meta-implication --- + producing more and more of them or eliminate them in subsequent goal-states. Subgoals of the form + @{term "B\<^sub>1 \ B\<^sub>2 \ A \ B\<^sub>3 \ B\<^sub>4 \ A"} can be eliminated via + the @{ML Tactic.assume_tac} - tactic, + and a subgoal @{term C\<^sub>m} can be refined via the theorem + @{term "E\<^sub>1 \ E\<^sub>2 \ E\<^sub>3 \ C\<^sub>m"} the @{ML Tactic.resolve_tac} - tactic to new subgoals + @{term "E\<^sub>1"},@{term "E\<^sub>2"}, @{term "E\<^sub>3"}. In case that a theorem used for resolution + has no premise @{term "E\<^sub>i"}, the subgoal @{term C\<^sub>m} is also eliminated ("closed"). + + The following abstract of the most commonly used @{ML_type \tactic\}'s drawn from + @{file "~~/src/Pure/tactic.ML"} looks as follows:\ ML\ (* ... *) @@ -798,8 +784,8 @@ ML\ (* ... *) \ text\Note that "applying a rule" is a fairly complex operation in the Extended Isabelle Kernel, -i.e. the tactic layer. It involves at least four phases, interfacing a theorem -coming from the global context $\theta$ (=theory), be it axiom or derived, into a given goal-state. + i.e. the tactic layer. It involves at least four phases, interfacing a theorem + coming from the global context $\theta$ (=theory), be it axiom or derived, into a given goal-state. \<^item> \<^emph>\generalization\. All free variables in the theorem were replaced by schematic variables. For example, @{term "x + y = y + x"} is converted into @{emph \?x + ?y = ?y + ?x\ }. @@ -833,16 +819,16 @@ coming from the global context $\theta$ (=theory), be it axiom or derived, into \ text\In a way, the two lifting processes represent an implementation of the conversion between -Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and -Gentzen Sequent Deduction.\ + Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and + Gentzen Sequent Deduction.\ section*[goalp::technical]\The classical goal package\ text\The main mechanism in Isabelle as an LCF-style system is to produce @{ML_type thm}'s -in backward-style via tactics as described in @{technical "t24"}. Given a context ---- be it global as @{ML_type theory} or be it inside a proof-context as @{ML_type Proof.context}, -user-programmed verification of (type-checked) terms or just strings can be done via the operations: -\ + in backward-style via tactics as described in @{technical "t24"}. Given a context + --- be it global as @{ML_type theory} or be it inside a proof-context as @{ML_type Proof.context}, + user-programmed verification of (type-checked) terms or just strings can be done via the + operations:\ ML\ @@ -853,7 +839,7 @@ Goal.prove_global : theory -> string list -> term list -> term -> (* ... and many more variants. *) \ -subsection*[ex211::example]\Proof example\ +subsection*[ex211::example]\Proof Example\ text\The proof:\ @@ -870,17 +856,9 @@ val thm1 = Goal.prove_global @{theory} (* global context [] (* name ? *) [] (* local assumption context *) (tt) (* parsed goal *) - (fn _ => simp_tac @{context} 1) (* proof tactic *) -\ + (fn _ => simp_tac @{context} 1) (* proof tactic *)\ - -subsection*[exo44::example]\Example\ - -ML\ -Goal.prove_global @{theory} ["2::int + 3 = 5"] -\ - section\The Isar Engine\ text\The main structure of the Isar-engine is @{ ML_structure Toplevel} and provides and @@ -888,20 +866,19 @@ internal @{ ML_type state} with the necessary infrastructure --- i.e. the operations to pack and unpack theories and Proof.contexts --- on it: \ ML\ - Toplevel.theory_toplevel: theory -> Toplevel.state; - Toplevel.init_toplevel: unit -> Toplevel.state; - Toplevel.is_toplevel: Toplevel.state -> bool; - Toplevel.is_theory: Toplevel.state -> bool; - Toplevel.is_proof: Toplevel.state -> bool; - Toplevel.is_skipped_proof: Toplevel.state -> bool; - Toplevel.level: Toplevel.state -> int; - Toplevel.context_of: Toplevel.state -> Proof.context; - Toplevel.generic_theory_of: Toplevel.state -> generic_theory; - Toplevel.theory_of: Toplevel.state -> theory; - Toplevel.proof_of: Toplevel.state -> Proof.state; - Toplevel.presentation_context: Toplevel.state -> Proof.context; - -\ + Toplevel.theory_toplevel: theory -> Toplevel.state; + Toplevel.init_toplevel: unit -> Toplevel.state; + Toplevel.is_toplevel: Toplevel.state -> bool; + Toplevel.is_theory: Toplevel.state -> bool; + Toplevel.is_proof: Toplevel.state -> bool; + Toplevel.is_skipped_proof: Toplevel.state -> bool; + Toplevel.level: Toplevel.state -> int; + Toplevel.context_of: Toplevel.state -> Proof.context; + Toplevel.generic_theory_of: Toplevel.state -> generic_theory; + Toplevel.theory_of: Toplevel.state -> theory; + Toplevel.proof_of: Toplevel.state -> Proof.state; + Toplevel.presentation_context: Toplevel.state -> Proof.context; + (* ... *) \ text\ The extensibility of Isabelle as a system framework depends on a number of tables, into which various concepts commands, ML-antiquotations, text-antiquotations, cartouches, ... @@ -914,8 +891,7 @@ text\ The extensibility of Isabelle as a system framework depends on a num creates an implicit @{ML Theory.setup} with an entry for a call-back function, which happens to be a parser that must have as side-effect a Toplevel-transition-transition. Registers @{ML_type "Toplevel.transition -> Toplevel.transition"} parsers to the - Isar interpreter. -\ + Isar interpreter.\ ML\ Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> @@ -940,31 +916,62 @@ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory gl subsection*[transmgt::technical] \Transaction Management in the Isar-Engine : The Toplevel \ +ML\Toplevel.exit: Toplevel.transition -> Toplevel.transition; + Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + Toplevel.ignored: Position.T -> Toplevel.transition; + Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition; + Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition; + Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition; + + Toplevel.present_local_theory: + (xstring * Position.T) option -> + (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + (* where text treatment and antiquotation parsing happens *) + + + (*fun document_command markdown (loc, txt) = + Toplevel.keep (fn state => + (case loc of + NONE => ignore (output_text state markdown txt) + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *) + + (* Isar Toplevel Steuerung *) + Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; + (* val keep' = add_trans o Keep; + fun keep f = add_trans (Keep (fn _ => f)); + *) + + Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) -> + Toplevel.transition -> Toplevel.transition; + (* fun present_local_theory target = present_transaction (fn int => + (fn Theory (gthy, _) => + let val (finish, lthy) = Named_Target.switch target gthy; + in Theory (finish lthy, SOME lthy) end + | _ => raise UNDEF)); + + fun present_transaction f g = add_trans (Transaction (f, g)); + fun transaction f = present_transaction f (K ()); + *) + + Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition; + (* fun theory' f = transaction (fn int => + (fn Theory (Context.Theory thy, _) => + let val thy' = thy + |> Sign.new_group + |> f int + |> Sign.reset_group; + in Theory (Context.Theory thy', NONE) end + | _ => raise UNDEF)); + + fun theory f = theory' (K f); *)\ + + ML\ -Toplevel.exit: Toplevel.transition -> Toplevel.transition; -Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; -Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; -Toplevel.ignored: Position.T -> Toplevel.transition; -Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition; -Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition; -Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition; - -Toplevel.present_local_theory: -(xstring * Position.T) option -> - (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; -(* where text treatment and antiquotation parsing happens *) - - -(*fun document_command markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_text state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *) - -(* Isar Toplevel Steuerung *) +(* Isar Toplevel Control *) Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; (* val keep' = add_trans o Keep; fun keep f = add_trans (Keep (fn _ => f)); @@ -993,62 +1000,23 @@ Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transiti | _ => raise UNDEF)); fun theory f = theory' (K f); *) - -\ - - -ML\ - - -(* Isar Toplevel Steuerung *) -Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - (* val keep' = add_trans o Keep; - fun keep f = add_trans (Keep (fn _ => f)); - *) - -Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) -> - Toplevel.transition -> Toplevel.transition; - (* fun present_local_theory target = present_transaction (fn int => - (fn Theory (gthy, _) => - let val (finish, lthy) = Named_Target.switch target gthy; - in Theory (finish lthy, SOME lthy) end - | _ => raise UNDEF)); - - fun present_transaction f g = add_trans (Transaction (f, g)); - fun transaction f = present_transaction f (K ()); - *) - -Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition; - (* fun theory' f = transaction (fn int => - (fn Theory (Context.Theory thy, _) => - let val thy' = thy - |> Sign.new_group - |> f int - |> Sign.reset_group; - in Theory (Context.Theory thy', NONE) end - | _ => raise UNDEF)); - - fun theory f = theory' (K f); *) - - \ subsection*[conf::technical]\ Configuration flags of fixed type in the Isar-engine. \ text\The toplevel also provides an infrastructure for managing configuration options -for system components. Based on a sum-type @{ML_type Config.value } -with the alternatives \<^verbatim>\ Bool of bool | Int of int | Real of real | String of string\ -and building the parametric configuration types @{ML_type "'a Config.T" } and the -instance \<^verbatim>\type raw = value T\, for all registered configurations the protocol: -\ + for system components. Based on a sum-type @{ML_type Config.value } + with the alternatives \<^verbatim>\ Bool of bool | Int of int | Real of real | String of string\ + and building the parametric configuration types @{ML_type "'a Config.T" } and the + instance \<^verbatim>\type raw = value T\, for all registered configurations the protocol:\ ML\ - Config.get: Proof.context -> 'a Config.T -> 'a; - Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context; - Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context; - Config.get_global: theory -> 'a Config.T -> 'a; - Config.map_global: 'a Config.T -> ('a -> 'a) -> theory -> theory; - Config.put_global: 'a Config.T -> 'a -> theory -> theory; -\ + Config.get: Proof.context -> 'a Config.T -> 'a; + Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context; + Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context; + Config.get_global: theory -> 'a Config.T -> 'a; + Config.map_global: 'a Config.T -> ('a -> 'a) -> theory -> theory; + Config.put_global: 'a Config.T -> 'a -> theory -> theory;\ + text\... etc. is defined.\ text\Example registration of an config attribute XS232: \ @@ -1056,8 +1024,7 @@ ML\ val (XS232, XS232_setup) = Attrib.config_bool \<^binding>\XS232\ (K false); -val _ = Theory.setup XS232_setup; -\ +val _ = Theory.setup XS232_setup;\ (* or: just command: @@ -1068,79 +1035,77 @@ setup\XS232_setup\ text\Another mechanism are global synchronised variables:\ ML\ (* For example *) -val C = Synchronized.var "Pretty.modes" "latEEex"; -(* Synchronized: a mechanism to bookkeep global - variables with synchronization mechanism included *) -Synchronized.value C; -\ + val C = Synchronized.var "Pretty.modes" "latEEex"; + (* Synchronized: a mechanism to bookkeep global + variables with synchronization mechanism included *) + Synchronized.value C;\ chapter*[frontend::technical]\Front-End \ text\In the following chapter, we turn to the right part of the system architecture -shown in @{docitem \architecture\}: -The PIDE ("Prover-IDE") layer @{cite "DBLP:conf/itp/Wenzel14"} -consisting of a part written in SML and another in SCALA. -Roughly speaking, PIDE implements "continuous build - continuous check" - functionality -over a textual, albeit generic document model. It transforms user modifications -of text elements in an instance of this model into increments (edits) and communicates -them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight -reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text -elements. Such markup is used to highlight, e.g., variables -or keywords with specific colors, to hyper-linking bound variables to their defining occurrences, -or to annotate type-information to terms which becomes displayed by specific -user-gestures on demand (hovering), etc. -Note that PIDE is not an editor, it is the framework that -coordinates these asynchronous information streams and optimizes it to a certain -extent (outdated markup referring to modified text is dropped, and -corresponding re-calculations are oriented to the user focus, for example). -Four concrete editors --- also called PIDE applications --- have been implemented: -\<^enum>an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version), -\<^enum>a Visual-Studio Code plugin (developed by Makarius Wenzel), - currently based on a fairly old PIDE version, -\<^enum>clide, a web-client supporting javascript and HTML5 - (developed by a group at University Bremen, based on a very old PIDE version), and -\<^enum>the most commonly used: the plugin in JEdit - Editor, - (developed by Makarius Wenzel, current PIDE version.) -\ + shown in @{docitem \architecture\}: + The PIDE ("Prover-IDE") layer @{cite "DBLP:conf/itp/Wenzel14"} + consisting of a part written in SML and another in SCALA. + Roughly speaking, PIDE implements "continuous build - continuous check" - functionality + over a textual, albeit generic document model. It transforms user modifications + of text elements in an instance of this model into increments (edits) and communicates + them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight + reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text + elements. Such markup is used to highlight, e.g., variables + or keywords with specific colors, to hyper-linking bound variables to their defining occurrences, + or to annotate type-information to terms which becomes displayed by specific + user-gestures on demand (hovering), etc. + Note that PIDE is not an editor, it is the framework that + coordinates these asynchronous information streams and optimizes it to a certain + extent (outdated markup referring to modified text is dropped, and + corresponding re-calculations are oriented to the user focus, for example). + Four concrete editors --- also called PIDE applications --- have been implemented: +\<^enum> an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version), +\<^enum> a Visual-Studio Code plugin (developed by Makarius Wenzel), + currently based on a fairly old PIDE version, +\<^enum> clide, a web-client supporting javascript and HTML5 + (developed by a group at University Bremen, based on a very old PIDE version), and +\<^enum> the most commonly used: the plugin in JEdit - Editor, + (developed by Makarius Wenzel, current PIDE version.)\ + +text\The document model forsees a number of text files, which are organized in form of an + acyclic graph. Such graphs can be grouped into \<^emph>\sessions\ and "frozen" to binaries in order + to avoid long compilation times. Text files have an abstract name serving as identity (the + mapping to file-paths in an underlying file-system is done in an own build management). + The primary format of the text files is \<^verbatim>\.thy\ (historically for: theory), + secondary formats can be \<^verbatim>\.sty\,\<^verbatim>\.tex\, \<^verbatim>\.png\, \<^verbatim>\.pdf\, or other files processed + by Isabelle and listed in a configuration processed by the build system.\ -text\The document model forsees a number of text files, which are organized in form of an acyclic graph. Such graphs can be -grouped into \<^emph>\sessions\ and "frozen" to binaries in order to avoid long compilation -times. Text files have an abstract name serving as identity (the mapping to file-paths -in an underlying file-system is done in an own build management). -The primary format of the text files is \<^verbatim>\.thy\ (historically for: theory), -secondary formats can be \<^verbatim>\.sty\,\<^verbatim>\.tex\, \<^verbatim>\.png\, \<^verbatim>\.pdf\, or other files processed -by Isabelle and listed in a configuration processed by the build system. -\ figure*[fig3::figure, relative_width="100",src="''figures/document-model''"] \A Theory-Graph in the Document Model\ -text\A \<^verbatim>\.thy\ file consists of a \<^emph>\header\, a \<^emph>\context-definition\ and -a \<^emph>\body\ consisting of a sequence of \<^emph>\commands\. Even the header consists of -a sequence of commands used for introductory text elements not depending on any context -information (so: practically excluding any form of text antiquotation (see above)). -The context-definition contains an \<^emph>\import\ and a \<^emph>\keyword\ section; -for example: -\begin{verbatim} -theory Isa_DOF (* Isabelle Document Ontology Framework *) - imports Main - RegExpInterface (* Interface to functional regular automata for monitoring *) - Assert - - keywords "+=" ":=" "accepts" "rejects" -\end{verbatim} -where \<^verbatim>\Isa_DOF\ is the abstract name of the text-file, \<^verbatim>\Main\ etc. refer to imported -text files (recall that the import relation must be acyclic). \<^emph>\keyword\s are used to separate -commands form each other; -predefined commands allow for the dynamic creation of new commands similarly -to the definition of new functions in an interpreter shell (or: toplevel, see above.). -A command starts with a pre-declared keyword and specific syntax of this command; -the declaration of a keyword is only allowed in the same \<^verbatim>\.thy\-file where the -the corresponding new command is defined. The semantics of the command is expressed -in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"} -function. Thus, the Isar-toplevel supports the generic document model -and allows for user-programmed extensions. -\ + +text\A \<^verbatim>\.thy\ file consists of a \<^emph>\header\, a \<^emph>\context-definition\ and + a \<^emph>\body\ consisting of a sequence of \<^emph>\commands\. Even the header consists of + a sequence of commands used for introductory text elements not depending on any context + information (so: practically excluding any form of text antiquotation (see above)). + The context-definition contains an \<^emph>\import\ and a \<^emph>\keyword\ section; + for example: + \begin{verbatim} + theory Isa_DOF (* Isabelle Document Ontology Framework *) + imports Main + RegExpInterface (* Interface to functional regular automata for monitoring *) + Assert + + keywords "+=" ":=" "accepts" "rejects" + \end{verbatim} + where \<^verbatim>\Isa_DOF\ is the abstract name of the text-file, \<^verbatim>\Main\ etc. refer to imported + text files (recall that the import relation must be acyclic). \<^emph>\keyword\s are used to separate + commands form each other; + predefined commands allow for the dynamic creation of new commands similarly + to the definition of new functions in an interpreter shell (or: toplevel, see above.). + A command starts with a pre-declared keyword and specific syntax of this command; + the declaration of a keyword is only allowed in the same \<^verbatim>\.thy\-file where the + the corresponding new command is defined. The semantics of the command is expressed + in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"} + function. Thus, the Isar-toplevel supports the generic document model + and allows for user-programmed extensions.\ text\In the traditional literature, Isabelle \<^verbatim>\.thy\-files were -were said to be processed by processed by two types of parsers: + were said to be processed by processed by two types of parsers: \<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed by a lexer-library and parser combinators built on top, and \<^enum> the "inner-syntax" (i.e. the syntax for @{term \\\} - terms) @@ -1169,13 +1134,12 @@ text\This picture is less and less true for a number of reasons: section\Basics: string, bstring and xstring\ text\@{ML_type "string"} is the basic library type from the SML library -in structure @{ML_structure "String"}. Many Isabelle operations produce -or require formats thereof introduced as type synonyms -@{ML_type "bstring"} (defined in structure @{ML_structure "Binding"} -and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}. -Unfortunately, the abstraction is not tight and combinations with -elementary routines might produce quite crappy results. -\ + in structure @{ML_structure "String"}. Many Isabelle operations produce + or require formats thereof introduced as type synonyms + @{ML_type "bstring"} (defined in structure @{ML_structure "Binding"} + and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}. + Unfortunately, the abstraction is not tight and combinations with + elementary routines might produce quite crappy results.\ ML\val b = Binding.name_of@{binding "here"}\ text\... produces the system output \verb+val it = "here": bstring+, @@ -1200,36 +1164,35 @@ ML\ fun dark_matter x = XML.content_of (YXML.parse_body x)\ section\Positions\ text\A basic data-structure relevant for PIDE are \<^emph>\positions\; beyond the usual line- and column -information they can represent ranges, list of ranges, and the name of the atomic sub-document -in which they are contained. In the command:\ + information they can represent ranges, list of ranges, and the name of the atomic sub-document + in which they are contained. In the command:\ ML\ val pos = @{here}; val markup = Position.here pos; -writeln ("And a link to the declaration of 'here' is "^markup) -\ +writeln ("And a link to the declaration of 'here' is "^markup)\ + (* \<^here> *) text\ ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position -of itself in the global document, converts it to markup (a string-representation of it) and sends -it via the usual @{ML "writeln"} to the interface. \ + of itself in the global document, converts it to markup (a string-representation of it) and sends + it via the usual @{ML "writeln"} to the interface. \ figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"] \Output with hyperlinked position.\ text\@{docitem \hyplinkout\} shows the produced output where the little house-like symbol in the -display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\ + display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\ section\Markup and Low-level Markup Reporting\ text\The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic -annotation data which is part of the protocol sent from Isabelle to the front-end. -They are qualified as "quasi-abstract", which means they are intended to be an abstraction of -the serialized, textual presentation of the protocol. Markups are structurally a pair of a key -and properties; @{ML_structure Markup} provides a number of of such \<^emph>\key\s for annotation classes -such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample -from \<^theory_text>\Isabelle_DOF\. A markup must be tagged with an id; this is done by the @{ML serial}-function -discussed earlier. Markup Operations, were used for hyperlinking applications to binding -occurrences, info for hovering, infors for type ... \ + annotation data which is part of the protocol sent from Isabelle to the front-end. + They are qualified as "quasi-abstract", which means they are intended to be an abstraction of + the serialized, textual presentation of the protocol. Markups are structurally a pair of a key + and properties; @{ML_structure Markup} provides a number of of such \<^emph>\key\s for annotation classes + such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample + from \<^theory_text>\Isabelle_DOF\. A markup must be tagged with an id; this is done by the @{ML serial}-function + discussed earlier. Markup Operations, were used for hyperlinking applications to binding + occurrences, info for hovering, infors for type ... \ ML\ - (* Position.report is also a type consisting of a pair of a position and markup. *) (* It would solve all my problems if I find a way to infer the defining Position.report from a type definition occurence ... *) @@ -1254,7 +1217,6 @@ Markup.theoryN : string; serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers, be it on the level of thy-internal states or as reference in markup in PIDE *) - \ @@ -1283,8 +1245,8 @@ end \ text\The @\ML report_defining_occurrence\-function above takes a position and a "cid" parsed -in the Front-End, converts this into markup together with a unique number identifying this -markup, and sends this as a report to the Front-End. \ + in the Front-End, converts this into markup together with a unique number identifying this + markup, and sends this as a report to the Front-End. \ subsection\A Slightly more Complex Example\ @@ -1369,25 +1331,23 @@ text\The pudding comes with the eating: \ subsection\Environment Structured Reporting\ text\ The structure @{ML_structure \Name_Space\} offers an own infra-structure for names and -manages the markup accordingly. MORE TO COME\ + manages the markup accordingly. MORE TO COME\ text\ @{ML_type "'a Name_Space.table"} \ section\ The System Lexer and Token Issues\ text\Four syntactic contexts are predefined in Isabelle (others can be added): -the ML context, the text context, the Isar-command context and the teerm-context, referring -to different needs of the Isabelle Framework as an extensible framework supporting incremental, -partially programmable extensions and as a Framework geared towards Formal Proofs and therefore -mathematical notations. The basic data-structure for the lexical treatment of these - -\ + the ML context, the text context, the Isar-command context and the teerm-context, referring + to different needs of the Isabelle Framework as an extensible framework supporting incremental, + partially programmable extensions and as a Framework geared towards Formal Proofs and therefore + mathematical notations. The basic data-structure for the lexical treatment of these elemens + are @{ML_structure "Token"}'s. \ subsection\Tokens\ text\The basic entity that lexers treat are \<^emph>\tokens\. defined in @{ML_structure "Token"} -It provides a classification infrastructure, the references to positions and Markup -as well as way's to annotate tokens with (some) values they denote: -\ + It provides a classification infrastructure, the references to positions and Markup + as well as way's to annotate tokens with (some) values they denote:\ ML\ local @@ -1444,20 +1404,20 @@ ML\ section\ Combinator Parsing \ text\Parsing Combinators go back to monadic programming as advocated by Wadler et. al, and has been -worked out @{cite "DBLP:journals/jfp/Hutton92"}. Parsing combinators are one of the two -major parsing technologies of the Isabelle front-end, in particular for the outer-syntax used -for the parsing of toplevel-commands. The core of the combinator library is -@{ML_structure \Scan\} providing the @{ML_type "'a parser"} which is a synonym for -@{ML_type " Token.T list -> 'a * Token.T list"}. - - "parsers" are actually interpreters; an 'a parser is a function that parses -an input stream and computes(=evaluates, computes) it into 'a. -Since the semantics of an Isabelle command is a transition => transition -or theory $\Rightarrow$ theory function, i.e. a global system transition. -parsers of that type can be constructed and be bound as call-back functions -to a table in the Toplevel-structure of Isar. - -The library also provides a bunch of infix parsing combinators, notably:\ + worked out @{cite "DBLP:journals/jfp/Hutton92"}. Parsing combinators are one of the two + major parsing technologies of the Isabelle front-end, in particular for the outer-syntax used + for the parsing of toplevel-commands. The core of the combinator library is + @{ML_structure \Scan\} providing the @{ML_type "'a parser"} which is a synonym for + @{ML_type " Token.T list -> 'a * Token.T list"}. + + "parsers" are actually interpreters; an 'a parser is a function that parses + an input stream and computes(=evaluates, computes) it into 'a. + Since the semantics of an Isabelle command is a transition => transition + or theory $\Rightarrow$ theory function, i.e. a global system transition. + parsers of that type can be constructed and be bound as call-back functions + to a table in the Toplevel-structure of Isar. + + The library also provides a bunch of infix parsing combinators, notably:\ ML\ val _ = op !! : ('a * message option -> message) -> ('a -> 'b) -> 'a -> 'b @@ -1502,9 +1462,9 @@ val _ = Scan.lift Args.cartouche_input : Input.source context_parser;\ subsection\Advanced Parser Library\ text\There are two parts. A general multi-purpose parsing combinator library is -found under @{ML_structure "Parse"}, providing basic functionality for parsing strings -or integers. There is also an important combinator that reads the current position information -out of the input stream:\ + found under @{ML_structure "Parse"}, providing basic functionality for parsing strings + or integers. There is also an important combinator that reads the current position information + out of the input stream:\ ML\ Parse.nat: int parser; Parse.int: int parser; @@ -1521,12 +1481,11 @@ Parse.position Args.cartouche_input; \ text\The second part is much more high-level, and can be found under @{ML_structure Args}. -In parts, these combinators are again based on more low-level combinators, in parts they serve as -an an interface to the underlying Earley-parser for mathematical notation used in types and terms. -This is perhaps meant with the fairly cryptic comment: -"Quasi-inner syntax based on outer tokens: concrete argument syntax of -attributes, methods etc." at the beginning of this structure. -\ + In parts, these combinators are again based on more low-level combinators, in parts they serve as + an an interface to the underlying Earley-parser for mathematical notation used in types and terms. + This is perhaps meant with the fairly cryptic comment: + "Quasi-inner syntax based on outer tokens: concrete argument syntax of + attributes, methods etc." at the beginning of this structure.\ ML\ @@ -1608,11 +1567,11 @@ in val _ = () end subsection\ Bindings \ text\ The structure @{ML_structure "Binding"} serves as -\structured name bindings\, as says the description, i.e. a mechanism to basically -associate an input string-fragment to its position. This concept is vital in all parsing processes -and the interaction with PIDE. + \structured name bindings\, as says the description, i.e. a mechanism to basically + associate an input string-fragment to its position. This concept is vital in all parsing processes + and the interaction with PIDE. -Key are two things: + Key are two things: \<^enum> the type-synonym @{ML_type "bstring"} which is synonym to @{ML_type "string"} and intended for "primitive names to be bound" \<^enum> the projection @{ML "Binding.pos_of : binding -> Position.T"} @@ -1655,8 +1614,8 @@ ML\ section\Term Parsing\ text\The heart of the parsers for mathematical notation, based on an Earley parser that can cope -with incremental changes of the grammar as required for sophisticated mathematical output, is hidden -behind the API described in this section.\ + with incremental changes of the grammar as required for sophisticated mathematical output, is hidden + behind the API described in this section.\ text\ Note that the naming underlies the following convention : there are: @@ -1792,16 +1751,16 @@ text\It provides a number of hooks that can be used for redirection hacks section \ Output: LaTeX \ text\The heart of the LaTeX generator is to be found in the structure @{ML_structure Thy_Output}. -This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing -process can not be parsed for the LaTeX Generator. The reason is twofold: + This is an own parsing and writing process, with the risc that a parsed file in the IDE parsing + process can not be parsed for the LaTeX Generator. The reason is twofold: \<^enum> The LaTeX Generator makes a rough attempt to mimic the LayOut if the thy-file; thus, its spacing is relevant. \<^enum> there is a special bracket \(*<*)\ ... \(*>*)\ that allows to specify input that is checked by Isabelle, but excluded from the LaTeX generator (this is handled in an own sub-parser called @{ML "Document_Source.improper"} where also other forms of comment parsers are provided. -Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to -@{ML_structure "Pretty"}. Key functions of this structure @{ML_structure "Latex"} are: + Since Isabelle2018, an own AST is provided for the LaTeX syntax, analogously to + @{ML_structure "Pretty"}. Key functions of this structure @{ML_structure "Latex"} are: \ ML\ @@ -1927,16 +1886,15 @@ As one can see, check-routines internally generate the markup. section*[cartouches::technical]\Inner Syntax Cartouches\ text\ The cascade-syntax principle underlying recent isabelle versions requires a -particular mechanism, called "cartouche" by Makarius who was influenced by French -Wine and French culture when designing this. + particular mechanism, called "cartouche" by Makarius who was influenced by French + Wine and French culture when designing this. -When parsing terms or types (via the Earley Parser), a standard mechanism for -calling another parser inside the current process is needed that is bound to the -\(\)\ ... \(\)\ paranthesis'. -\ + When parsing terms or types (via the Earley Parser), a standard mechanism for + calling another parser inside the current process is needed that is bound to the + \(\)\ ... \(\)\ paranthesis'. \ text\The following example --- drawn from the Isabelle/DOF implementation --- allows -to parse UTF8 - Unicode strings as alternative to @{term "''abc''"} HOL-strings.\ + to parse UTF8 - Unicode strings as alternative to @{term "''abc''"} HOL-strings.\ ML\\ \Dynamic setup of inner syntax cartouche\ @@ -2000,13 +1958,13 @@ fun parse_translation_cartouche binding l f_integer accu = \ text\The following registration of this cartouche for strings is fails because it has - already been done in the surrounding Isabelle/DOF environment... \ -(* -parse_translation \ - [( @{syntax_const "_cartouche_string"} - , parse_translation_cartouche \<^binding>\cartouche_type\ Cartouche_Grammar.default (K I) ())] -\ -*) + already been done in the surrounding Isabelle/DOF environment... \ + (* + parse_translation \ + [( @{syntax_const "_cartouche_string"} + , parse_translation_cartouche \<^binding>\cartouche_type\ Cartouche_Grammar.default (K I) ())] + \ + *) (* test for this cartouche... *) term "\A \ B\ = ''''" @@ -2015,22 +1973,22 @@ term "\A \ B\ = ''''" chapter*[c::conclusion]\Conclusion\ text\ This interactive Isabelle Programming Cook-Book represents my current way -to view and explain Isabelle programming API's to students and collaborators. -It differs from the reference manual in some places on purpose, since I believe -that a lot of internal Isabelle API's need a more conceptual view on what is happening -(even if this conceptual view is at times over-abstracting a little). -It also offers a deliberately different abstraction to the explanations in form of comments -in the sources or in the Reference Manual. - -The descriptions of some sources may appear lengthy and repetitive and redundant - but this kind -of repetition not only give an idea of the chosen abstraction levels on some interfaces, but also -represents --- since this is a "living document" (a notion I owe Simon Foster) --- a continuous check -for each port of our material to each more recent Isabelle version, where the first attempts -to load it will fail, but give another source of information over the modifications of -the system interface for parts relevant to our own development work. - -All hints and contributions of collegues and collaborators are greatly welcomed; all errors -and the roughness of this presentation is entirely my fault. + to view and explain Isabelle programming API's to students and collaborators. + It differs from the reference manual in some places on purpose, since I believe + that a lot of internal Isabelle API's need a more conceptual view on what is happening + (even if this conceptual view is at times over-abstracting a little). + It also offers a deliberately different abstraction to the explanations in form of comments + in the sources or in the Reference Manual. + + The descriptions of some sources may appear lengthy and repetitive and redundant - but this kind + of repetition not only give an idea of the chosen abstraction levels on some interfaces, but also + represents --- since this is a "living document" (a notion I owe Simon Foster) --- a continuous check + for each port of our material to each more recent Isabelle version, where the first attempts + to load it will fail, but give another source of information over the modifications of + the system interface for parts relevant to our own development work. + + All hints and contributions of collegues and collaborators are greatly welcomed; all errors + and the roughness of this presentation is entirely my fault. \ (*<*) From 67d6caf2ad8264dc05bcf4081fe6ea6b7fec7812 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 17 Jul 2019 14:51:45 +0200 Subject: [PATCH 10/10] Reworked/Synced Background chapter with SEFM paper --- .../IsaDof_Manual/01_Introduction.thy | 4 +- .../IsaDof_Manual/02_Background.thy | 148 +++++++++++++++++- .../IsaDof_Manual/IsaDofManual.thy | 3 +- examples/technical_report/IsaDof_Manual/ROOT | 17 +- .../IsaDof_Manual/document/preamble.tex | 3 + .../IsaDof_Manual/document/root.bib | 75 ++++++++- 6 files changed, 242 insertions(+), 8 deletions(-) diff --git a/examples/technical_report/IsaDof_Manual/01_Introduction.thy b/examples/technical_report/IsaDof_Manual/01_Introduction.thy index ac869819..8b479c84 100644 --- a/examples/technical_report/IsaDof_Manual/01_Introduction.thy +++ b/examples/technical_report/IsaDof_Manual/01_Introduction.thy @@ -34,7 +34,7 @@ types, terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle IDE, a document is checked to be \<^emph>\conform\ to a particular ontology---\isadof is designed to give fast user-feedback \<^emph>\during the capture of content\. This is particularly valuable in case of document -changes, where the \<^emph>\coherence\ between the formal and the informal parts of the +evolution, where the \<^emph>\coherence\ between the formal and the informal parts of the content can be mechanically checked. To avoid any misunderstanding: \isadof is \<^emph>\not a theory in HOL\ @@ -46,6 +46,8 @@ itself. \isadof is a plugin into the Isabelle/Isar framework in the style of~@{cite "wenzel.ea:building:2007"}. \ + + (* declaring the forward references used in the subsequent section *) (*<*) declare_reference*[bgrnd::text_section] diff --git a/examples/technical_report/IsaDof_Manual/02_Background.thy b/examples/technical_report/IsaDof_Manual/02_Background.thy index a654cdaa..e8713f31 100644 --- a/examples/technical_report/IsaDof_Manual/02_Background.thy +++ b/examples/technical_report/IsaDof_Manual/02_Background.thy @@ -6,8 +6,9 @@ begin chapter*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"] \ Background: The Isabelle System \ +section*[bgrnd1::introduction]\Document Processing in Isabelle\ text*[background::introduction]\ -While Isabelle is widely perceived as an interactive theorem prover +While Isabelle @{cite "nipkow.ea:isabelle:2002"} is widely perceived as an interactive theorem prover for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we would like to emphasize the view that Isabelle is far more than that: it is the \<^emph>\Eclipse of Formal Methods Tools\. This refers to the @@ -43,10 +44,20 @@ resides in the SML structure \texttt{Context}. This structure provides a kind of for components (plugins) such as \isadof. On top of the latter, the LCF-Kernel, tactics, automated proof procedures as well as specific support for higher specification constructs were built. \ - -text\ We would like to detail the documentation generation of the architecture, + + +text\ Of particular interest for \dof is documentation generation of the architecture, which is based on literate specification commands such as \inlineisar+section+ \ldots, -\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc. +\inlineisar+subsection+ \ldots, \inlineisar+text+ \ldots, etc. Moreover, we assume that +\<^emph>\inside\ text-elements, there are generic and extendible ways to add "semantic", i.e. +machine-checked sub-elements. + +In the sequel, we will outline the general assumptions that \dof makes for the underlying +document model, and than explain how Isabelle as a framework fits into this picture. +\ + + +(* Thus, a user can add a simple text: \begin{isar} text\This is a description.\ @@ -71,8 +82,137 @@ text*[anti]\ Thus, antiquotations can refer to formal content, can be type displayed and can be used for calculations before actually being typeset. When editing, Isabelle's PIDE offers auto-completion and error-messages while typing the above \<^emph>\semi-formal\ content. \ +*) +section*["sec:background"::introduction]\The Document Model\ +text\ +In this section, we explain the assumed document model underlying +\dof in general; in particular the concepts \<^emph>\integrated document\, +\<^emph>\sub-document\ , \<^emph>\text-element\ and \<^emph>\semantic macros\ occurring +inside text-elements. Furthermore, we assume two different levels of +parsers (for \<^emph>\outer\ and \<^emph>\inner syntax\) where the inner-syntax is basically a typed +$\lambda$-calculus and some Higher-order Logic (HOL).\ + +figure*["fig:dependency"::figure,relative_width="50",src="''figures/document-hierarchy''"]\ + A Theory-Graph in the Document Model. \ + + +text\ +We assume a hierarchical document model, \ie, an \<^emph>\integrated\ +document consist of a hierarchy \<^emph>\sub-documents\ (files) that +can depend acyclically on each other. 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>\theory\-files. A theory file consists of a +\<^emph>\header\, a \<^emph>\context definition\, and a body consisting of a +sequence of \<^emph>\command\s (@{figure "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 \inlineisar{import} and a \inlineisar{keyword} section, +for example: +\begin{isar} +theory Example (* Name of the "theory" *) + imports (* Declaration of "theory" dependencies *) + Main (* Imports a library called "Main" *) + keywords (* Registration of keywords defined locally *) + requirement (* A command for describing requirements *) +\end{isar} +where \inlineisar{Example} is the abstract name of the text-file, +\texttt{Main} refers to an imported theory (recall that the import +relation must be acyclic) and \inlineisar{keywords} are used to +separate commands from each other.\ + +text\We distinguish fundamentally two different syntactic levels: +\begin{compactenum} +\item the \emph{outer-syntax} (\ie, the syntax for commands) is processed + by a lexer-library and parser combinators built on top, and +\item the \emph{inner-syntax} (\ie, the syntax for $\lambda$-terms in + HOL) with its own parametric polymorphism type checking. +\end{compactenum} +On the semantic level, we assume a validation process for an +integrated document, where the semantics of a command is a +transformation \inlineisar+\ \ \+ for some +system state \inlineisar+\+. This document model can be +instantiated with outer-syntax commands for common text elements, \eg, + \inlineisar+section{*...*}+ or \inlineisar+text{*...*}+. Thus, users can add informal text to a +sub-document using a text command: +\begin{isar} + text\This is a description.\ +\end{isar} +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{semantic macros}, called antiquotations: +\begin{isar} + text\According to the reflexivity axiom @{thm refl}, we obtain in \ + for @{term "fac 5"} the result @{value "fac 5"}.\ +\end{isar} +which is represented in the final document (\eg, a PDF) by: +\begin{out} + According to the reflexivity axiom $x = x$, we obtain in $\Gamma$ for $\operatorname{fac} 5$ the result $120$. +\end{out} +Semantic macros are partial functions of type % +\inlineisar+\ \ text+; since they can use the +system state, they can perform all sorts of specific checks or +evaluations (type-checks, executions of code-elements, references to +text-elements or proven theorems such as \inlineisar+refl+, which is +the reference to the axiom of reflexivity). + +Semantic macros establish \<^emph>\formal content\ inside informal content; they can be +type-checked before being displayed and can be used for calculations before being +typeset. They represent the device for linking the formal with the informal. \ + + + +subsection*[bgrnd21::introduction]\Implementability of the Assumed Document Model.\ +text\ +Batch-mode checkers for \dof can be implemented in all systems of the +LCF-style prover family, \ie, systems with a type-checked +\inlinesml{term}, and abstract \inlinesml{thm}-type for +theorems (protected by a kernel). This includes, \eg, ProofPower, +HOL4, HOL-light, Isabelle, as well as Coq and its derivatives. \dof +is, however, designed for fast interaction in an IDE. If a user wants +to benefit from this experience, only Isabelle and Coq have the +necessary infrastructure of asynchronous proof-processing and support +by a PIDE +@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and "DBLP:conf/mkm/BarrasGHRTWW13" + and "Faithfull:2018:COQ:3204179.3204223"} which in many features +over-accomplishes the required features of \dof. For example, current Isabelle versions +offer cascade-syntaxes (different syntaxes and even parser-technologies +which can be nested along the \inlineisar+ \ ... \ + barriers, while +\dof actually only requires a 2-level syntax model.\ + +figure*["fig:dof-ide"::figure,relative_width="80",src="''figures/cicm2018-combined''"]\ + The \isadof IDE (left) and the corresponding PDF (right).% , showing the first page + % of~\cite{brucker.ea:isabelle-ontologies:2018}. \ + +text\ We call the present implementation of \dof on the + Isabelle platform \isadof. In +@{docitem "fig:dof-ide"}, a screen-shot of an introductory paper on \isadof +@{cite "brucker.ea:isabelle-ontologies:2018"} is shown; +this paper focusses on a number of application scenarios and user-interface aspects. +In @{docitem "fig:dof-ide"}, the \isadof PIDE can be seen on the left, while +the generated presentation in PDF is shown on the right. + +Isabelle provides, beyond the features required for \dof, a lot of +additional benefits. For example, it also allows the asynchronous +evaluation and checking of the document content +@{cite "DBLP:conf/itp/Wenzel14" and "DBLP:journals/corr/Wenzel14" and + "DBLP:conf/mkm/BarrasGHRTWW13"} +and is dynamically extensible. Its PIDE provides a \<^emph>\continuous build, continuous check\ +functionality, syntax highlighting, and IntelliSense-like auto-completion. +It also provides infrastructure for +displaying meta-information (\eg, binding and type annotation) as +pop-ups, while hovering over sub-expressions. A fine-grained +dependency analysis allows the processing of individual parts of +theory files asynchronously, allowing Isabelle to interactively +process large (hundreds of theory files) documents. Isabelle can +group sub-documents into sessions, \ie, sub-graphs of the +document-structure that can be ``pre-compiled'' and loaded +instantaneously, \ie, without re-processing. \ + (*<*) end (*>*) diff --git a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy index fc19a954..3e310b79 100644 --- a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy +++ b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy @@ -6,13 +6,14 @@ begin text*[bib::bibliography]\References\ +(*<*) + close_monitor*[this] text\Resulting trace in doc\_item ''this'': \ ML\@{trace_attribute this}\ -(*<*) end (*>*) diff --git a/examples/technical_report/IsaDof_Manual/ROOT b/examples/technical_report/IsaDof_Manual/ROOT index fbbd4391..98af32fc 100644 --- a/examples/technical_report/IsaDof_Manual/ROOT +++ b/examples/technical_report/IsaDof_Manual/ROOT @@ -1,4 +1,4 @@ -session "IsaDof_Manual" = "Isabelle_DOF" + +session "IsaDofManual" = "Isabelle_DOF" + options [document = pdf, document_output = "output", quick_and_dirty = true] theories IsaDofManual @@ -21,3 +21,18 @@ session "IsaDof_Manual" = "Isabelle_DOF" + "figures/srac-as-es-application.png" "figures/Dogfood-figures.png" + "figures/IsaArchGlobal.png" + "figures/document-hierarchy.svg" + "figures/IsaArchInteract.png" + "figures/document-model.key" + "figures/PIDE-interaction.pdf" + "figures/document-model.pdf" + "figures/cicm2018-combined.png" + "figures/isabelle-architecture.svg" + "figures/Dogfood-figures.png" + "figures/cicm2018-dof.png" + "figures/isadof.png" + "figures/cicm2018-pdf.png" + "figures/IsaArch.odp" + "figures/document-hierarchy.pdf" + "figures/srac-definition.png" diff --git a/examples/technical_report/IsaDof_Manual/document/preamble.tex b/examples/technical_report/IsaDof_Manual/document/preamble.tex index 62e8060b..a57336ec 100644 --- a/examples/technical_report/IsaDof_Manual/document/preamble.tex +++ b/examples/technical_report/IsaDof_Manual/document/preamble.tex @@ -57,3 +57,6 @@ \title{} \author{<AUTHOR>} + +\newcommand{\dof}{DOF\xspace} + diff --git a/examples/technical_report/IsaDof_Manual/document/root.bib b/examples/technical_report/IsaDof_Manual/document/root.bib index de3c5c63..602e100e 100644 --- a/examples/technical_report/IsaDof_Manual/document/root.bib +++ b/examples/technical_report/IsaDof_Manual/document/root.bib @@ -138,7 +138,17 @@ timestap = {2008-05-26} } - +@InProceedings{ brucker.ea:isabelle-ontologies:2018, + author = {Brucker, Achim D. and Ait-Sadoune, Idir and Crisafulli, Paolo and Wolff, Burkhart}, + title = {Using the {Isabelle} ontology framework: Linking the formal with the informal.}, + publisher = pub-springer, + address = pub-springer:adr, + series = s-lncs, + volume = 11006, + year = 2018, + doi = {10.1007/978-3-319-96812-4_3}, + booktitle = {Conference on Intelligent Computer Mathematics (CICM)} +} @InProceedings{ wenzel:asynchronous:2014, author = {Makarius Wenzel}, @@ -279,3 +289,66 @@ year = {2018} } +@InProceedings{ DBLP:conf/itp/Wenzel14, + author = {Makarius Wenzel}, + title = {Asynchronous User Interaction and Tool Integration in + Isabelle/PIDE}, + booktitle = {Interactive Theorem Proving (ITP)}, + pages = {515--530}, + year = 2014, + doi = {10.1007/978-3-319-08970-6_33}, + timestamp = {Sun, 21 May 2017 00:18:59 +0200}, + biburl = {https://dblp.org/rec/bib/conf/itp/Wenzel14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + + +@InProceedings{ DBLP:journals/corr/Wenzel14, + author = {Makarius Wenzel}, + title = {System description: Isabelle/jEdit in 2014}, + booktitle = {Proceedings Eleventh Workshop on User Interfaces for + Theorem Provers, {UITP} 2014, Vienna, Austria, 17th July + 2014.}, + pages = {84--94}, + year = 2014, + doi = {10.4204/EPTCS.167.10}, + timestamp = {Wed, 03 May 2017 14:47:58 +0200}, + biburl = {https://dblp.org/rec/bib/journals/corr/Wenzel14}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@InProceedings{ DBLP:conf/mkm/BarrasGHRTWW13, + author = {Bruno Barras and Lourdes Del Carmen + Gonz{\'{a}}lez{-}Huesca and Hugo Herbelin and Yann + R{\'{e}}gis{-}Gianas and Enrico Tassi and Makarius Wenzel + and Burkhart Wolff}, + title = {Pervasive Parallelism in Highly-Trustable Interactive + Theorem Proving Systems}, + booktitle = {Intelligent Computer Mathematics - MKM, Calculemus, DML, + and Systems and Projects}, + pages = {359--363}, + year = 2013, + doi = {10.1007/978-3-642-39320-4_29}, + timestamp = {Sun, 04 Jun 2017 10:10:26 +0200}, + biburl = {https://dblp.org/rec/bib/conf/mkm/BarrasGHRTWW13}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@article{Faithfull:2018:COQ:3204179.3204223, + author = {Faithfull, Alexander and Bengtson, Jesper and Tassi, Enrico and Tankink, Carst}, + title = {Coqoon}, + journal = {Int. J. Softw. Tools Technol. Transf.}, + issue_date = {April 2018}, + volume = {20}, + number = {2}, + month = apr, + year = {2018}, + issn = {1433-2779}, + pages = {125--137}, + numpages = {13}, + url = {https://doi.org/10.1007/s10009-017-0457-2}, + doi = {10.1007/s10009-017-0457-2}, + acmid = {3204223}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} \ No newline at end of file