No Description
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

MyCommentedIsabelle.thy 73KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695169616971698169917001701170217031704170517061707170817091710171117121713171417151716171717181719172017211722172317241725172617271728172917301731173217331734173517361737173817391740174117421743
  1. (*<*)
  2. theory MyCommentedIsabelle
  3. imports "Isabelle_DOF.technical_report"
  4. begin
  5. open_monitor*[this::report]
  6. (*>*)
  7. title*[tit::title]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close>
  8. subtitle*[stit::subtitle]\<open>Version : Isabelle 2017\<close>
  9. text*[bu::author,
  10. email = "''wolff@lri.fr''",
  11. affiliation = "''Universit\\'e Paris-Saclay, Paris, France''"]\<open>Burkhart Wolff\<close>
  12. text*[abs::abstract,
  13. keywordlist="[''LCF-Architecture'',''Isabelle'',''SML'',''PIDE'',''Tactic Programming'']"]\<open>
  14. While Isabelle is mostly known as part of Isabelle/HOL (an interactive
  15. theorem prover), it actually provides a system framework for developing a wide
  16. spectrum of applications. A particular strength of the Isabelle framework is the
  17. combination of text editing, formal verification, and code generation.
  18. This is a programming-tutorial of Isabelle and Isabelle/HOL, a complementary
  19. text to the unfortunately somewhat outdated "The Isabelle Cookbook" in
  20. \url{https://nms.kcl.ac.uk/christian.urban/Cookbook/}. The reader is encouraged
  21. not only to consider the generated .pdf, but also consult the loadable version in Isabelle/jedit
  22. in order to make experiments on the running code.
  23. This text is written itself in Isabelle/Isar using a specific document ontology
  24. for technical reports. It is intended to be a "living document", i.e. it is not only
  25. used for generating a static, conventional .pdf, but also for direct interactive
  26. exploration in Isabelle/jedit. This way, types, intermediate results of computations and
  27. checks can be repeated by the reader who is invited to interact with this document.
  28. Moreover, the textual parts have been enriched with a maximum of formal content
  29. which makes this text re-checkable at each load and easier maintainable.
  30. \<close>
  31. chapter*[intro::introduction]\<open> Introduction \<close>
  32. chapter*[t1::technical]\<open> SML and Fundamental SML libraries \<close>
  33. section*[t11::technical] "ML, Text and Antiquotations"
  34. text\<open>Isabelle is written in SML, the "Standard Meta-Language", which is
  35. is an impure functional programming language allowing, in principle, mutable variables and side-effects.
  36. The following Isabelle/Isar commands allow for accessing the underlying SML interpreter
  37. of Isabelle directly. In the example, a mutable variable X is declared, defined to 0 and updated;
  38. and finally re-evaluated leading to output: \<close>
  39. ML\<open> val X = Unsynchronized.ref 0;
  40. X:= !X + 1;
  41. X
  42. \<close>
  43. text\<open>However, since Isabelle is a platform involving parallel execution, concurrent computing, and,
  44. as an interactive environment, involves backtracking / re-evaluation as a consequence of user-
  45. interaction, imperative programming is discouraged and nearly never used in the entire Isabelle
  46. code-base. The preferred programming style is purely functional: \<close>
  47. ML\<open> fun fac x = if x = 0 then 1 else x * fac(x-1) ;
  48. fac 10;
  49. \<close>
  50. -- or
  51. ML\<open> type state = { a : int, b : string}
  52. fun incr_state ({a, b}:state) = {a=a+1, b=b}
  53. \<close>
  54. text\<open> The faculty function is defined and executed; the (sub)-interpreter in Isar
  55. works in the conventional read-execute-print loop for each statement separated by a ";".
  56. Functions, types, data-types etc. can be grouped to modules (called \<^emph>\<open>structures\<close>) which can
  57. be constrained to interfaces (called \<^emph>\<open>signatures\<close>) and even be parametric structures
  58. (called \<^emph>\<open>functors\<close>). \<close>
  59. text\<open> The Isabelle/Isar interpreter (called \<^emph>\<open>toplevel\<close> ) is extensible; by a mixture of SML
  60. and Isar-commands, domain-specific components can be developed and integrated into the system
  61. on the fly. Actually, the Isabelle system code-base consists mainly of SML and \<^verbatim>\<open>.thy\<close>-files
  62. containing such mixtures of Isar commands and SML. \<close>
  63. text\<open> Besides the ML-command used in the above examples, there are a number of commands
  64. representing text-elements in Isabelle/Isar; text commands can be interleaved arbitraryly
  65. with other commands. Text in text-commands may use LaTeX and is used for type-setting
  66. documentations in a kind of literate programming style. \<close>
  67. text\<open>So: the text command for:\<close>
  68. text\<open>\<^emph>\<open>This is a text.\<close>\<close>
  69. text\<open>... is represented in an \<^verbatim>\<open>.thy\<close> file by:\<close>
  70. text\<open>\verb+text\<open>\<^emph>\<open>This is a text.\<close>\<close>+\<close>
  71. text\<open>and desplayed in the Isabelle/jedit front-end at the sceen by:\<close>
  72. figure*[fig2::figure, relative_width="100",src="''figures/text-element''"]
  73. \<open>A text-element as presented in Isabelle/jedit. \<close>
  74. text\<open> text-commands, ML- commands (and in principle any other command) can be seen as
  75. \<^emph>\<open>quotations\<close> over the underlying SML environment (similar to OCaml or Haskell).
  76. Linking these different sorts of quotations with each other and the underlying SML-envirnment
  77. is supported via \<^emph>\<open>antiquotations\<close>'s. Generally speaking, antiquotations are a programming technique
  78. to specify expressions or patterns in a quotation, parsed in the context of the enclosing expression
  79. or pattern where the quotation is.
  80. The way an antiquotation is specified depends on the quotation expander: typically a specific
  81. character and an identifier, or specific parentheses and a complete expression or pattern.\<close>
  82. text\<open> In Isabelle documentations, antiquotation's were heavily used to enrich literate explanations
  83. and documentations by "formal content", i.e. machine-checked, typed references
  84. to all sorts of entities in the context of the interpreting environment.
  85. Formal content allows for coping with sources that rapidly evolve and were developed by
  86. distributed teams as is typical in open-source developments.
  87. A paradigmatic example for antiquotation in Texts and Program snippets is here:
  88. \<close>
  89. text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
  90. ML\<open> val x = @{thm refl};
  91. val y = @{term "A \<longrightarrow> B"}
  92. val y = @{typ "'a list"}
  93. \<close>
  94. text\<open>... which we will describe in more detail later. \<close>
  95. text\<open>In a way, literate specification attempting to maximize its formal content is a way to
  96. ensure "Agile Development" in a (theory)-document development, at least for its objectives,
  97. albeit not for its popular methods and processes like SCRUM. \<close>
  98. paragraph\<open>
  99. A maximum of formal content inside text documentation also ensures the
  100. consistency of this present text with the underlying Isabelle version.\<close>
  101. section\<open>The Isabelle/Pure bootstrap\<close>
  102. text\<open>It is instructive to study the fundamental bootstrapping sequence of the Isabelle system;
  103. it is written in the Isar format and gives an idea of the global module dependencies:
  104. @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}. Loading this file
  105. (for example by hovering over this hyperlink in the antiquotation holding control or
  106. command key in Isabelle/jedit and activating it) allows the Isabelle IDE
  107. to support hyperlinking \<^emph>\<open>inside\<close> the Isabelle source.\<close>
  108. text\<open>The bootstrapping sequence is also reflected in the following diagram: \<close>
  109. figure*[architecture::figure,relative_width="100",src="''figures/isabelle-architecture''"]\<open>
  110. The system architecture of Isabelle (left-hand side) and the
  111. asynchronous communication between the Isabelle system and
  112. the IDE (right-hand side). \<close>
  113. section*[t12::technical] "Elements of the SML library";
  114. text\<open>Elements of the @{file "$ISABELLE_HOME/src/Pure/General/basics.ML"} SML library
  115. are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions
  116. except those generated by the specific "error" function are discouraged in Isabelle
  117. source programming since they might produce races. Finally, a number of commonly
  118. used "squigglish" combinators is listed:
  119. \<close>
  120. ML\<open>
  121. Bind : exn;
  122. Chr : exn;
  123. Div : exn;
  124. Domain : exn;
  125. Fail : string -> exn;
  126. Match : exn;
  127. Overflow : exn;
  128. Size : exn;
  129. Span : exn;
  130. Subscript : exn;
  131. exnName : exn -> string ; (* -- very interesting to query an unknown exception *)
  132. exnMessage : exn -> string ;
  133. \<close>
  134. ML\<open>
  135. op ! : 'a Unsynchronized.ref -> 'a;
  136. op := : ('a Unsynchronized.ref * 'a) -> unit;
  137. op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c; (* reversed function composition *)
  138. op o : (('b -> 'c) * ('a -> 'b)) -> 'a -> 'c;
  139. op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e;
  140. op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e;
  141. op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
  142. op ? : bool * ('a -> 'a) -> 'a -> 'a;
  143. ignore: 'a -> unit;
  144. op before : ('a * unit) -> 'a;
  145. I: 'a -> 'a;
  146. K: 'a -> 'b -> 'a
  147. \<close>
  148. text\<open>Some basic examples for the programming style using these combinators can be found in the
  149. "The Isabelle Cookbook" section 2.3.\<close>
  150. text\<open>An omnipresent data-structure in the Isabelle SML sources are tables
  151. implemented in @{file "$ISABELLE_HOME/src/Pure/General/table.ML"}. These
  152. generic tables are presented in an efficient purely functional implementation using
  153. balanced 2-3 trees. Key operations are:\<close>
  154. ML\<open>
  155. signature TABLE_reduced =
  156. sig
  157. type key
  158. type 'a table
  159. exception DUP of key
  160. exception SAME
  161. exception UNDEF of key
  162. val empty: 'a table
  163. val dest: 'a table -> (key * 'a) list
  164. val keys: 'a table -> key list
  165. val lookup_key: 'a table -> key -> (key * 'a) option
  166. val lookup: 'a table -> key -> 'a option
  167. val defined: 'a table -> key -> bool
  168. val update: key * 'a -> 'a table -> 'a table
  169. (* ... *)
  170. end
  171. \<close>
  172. text\<open>... where \<^verbatim>\<open>key\<close> is usually just a synonym for string.\<close>
  173. chapter*[t2::technical] \<open> Prover Architecture \<close>
  174. section*[t21::technical] \<open> The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts \<close>
  175. text\<open> What I call the 'Nano-Kernel' in Isabelle can also be seen as an acyclic theory graph.
  176. The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}.
  177. My notion is a bit criticisable since this component, which provides the type of @{ML_type theory}
  178. and @{ML_type Proof.context}, is not that Nano after all.
  179. However, these type are pretty empty place-holders at that level and the content of
  180. @{file "$ISABELLE_HOME/src/Pure/theory.ML"} is registered much later.
  181. The sources themselves mention it as "Fundamental Structure".
  182. In principle, theories and proof contexts could be REGISTERED as user data inside contexts.
  183. The chosen specialization is therefore an acceptable meddling of the abstraction "Nano-Kernel"
  184. and its application context: Isabelle.
  185. Makarius himself says about this structure:
  186. "Generic theory contexts with unique identity, arbitrarily typed data,
  187. monotonic development graph and history support. Generic proof
  188. contexts with arbitrarily typed data."
  189. In my words: a context is essentially a container with
  190. \<^item> an id
  191. \<^item> a list of parents (so: the graph structure)
  192. \<^item> a time stamp and
  193. \<^item> a sub-context relation (which uses a combination of the id and the time-stamp to
  194. establish this relation very fast whenever needed; it plays a crucial role for the
  195. context transfer in the kernel.
  196. A context comes in form of three 'flavours':
  197. \<^item> theories : @{ML_type theory}'s, containing a syntax and axioms, but also
  198. user-defined data and configuration information.
  199. \<^item> Proof-Contexts: @{ML_type Proof.context}
  200. containing theories but also additional information if Isar goes into prove-mode.
  201. In general a richer structure than theories coping also with fixes, facts, goals,
  202. in order to support the structured Isar proof-style.
  203. \<^item> Generic: @{ML_type Context.generic }, i.e. the sum of both.
  204. All context have to be seen as mutable; so there are usually transformations defined on them
  205. which are possible as long as a particular protocol (\<^verbatim>\<open>begin_thy\<close> - \<^verbatim>\<open>end_thy\<close> etc) are respected.
  206. Contexts come with type user-defined data which is mutable through the entire lifetime of
  207. a context.
  208. \<close>
  209. subsection*[t212::technical]\<open> Mechanism 1 : Core Interface. \<close>
  210. text\<open>To be found in @{file "$ISABELLE_HOME/src/Pure/context.ML"}:\<close>
  211. ML\<open>
  212. Context.parents_of: theory -> theory list;
  213. Context.ancestors_of: theory -> theory list;
  214. Context.proper_subthy : theory * theory -> bool;
  215. Context.Proof: Proof.context -> Context.generic; (*constructor*)
  216. Context.proof_of : Context.generic -> Proof.context;
  217. Context.certificate_theory_id : Context.certificate -> Context.theory_id;
  218. Context.theory_name : theory -> string;
  219. Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic;
  220. \<close>
  221. text\<open>ML structure @{ML_structure Proof_Context}:\<close>
  222. ML\<open>
  223. Proof_Context.init_global: theory -> Proof.context;
  224. Context.Proof: Proof.context -> Context.generic; (* the path to a generic Context *)
  225. Proof_Context.get_global: theory -> string -> Proof.context
  226. \<close>
  227. subsection*[t213::example]\<open>Mechanism 2 : global arbitrary data structure that is attached to the global and
  228. local Isabelle context $\theta$ \<close>
  229. ML \<open>
  230. datatype X = mt
  231. val init = mt;
  232. val ext = I
  233. fun merge (X,Y) = mt
  234. structure Data = Generic_Data
  235. (
  236. type T = X
  237. val empty = init
  238. val extend = ext
  239. val merge = merge
  240. );
  241. Data.get : Context.generic -> Data.T;
  242. Data.put : Data.T -> Context.generic -> Context.generic;
  243. Data.map : (Data.T -> Data.T) -> Context.generic -> Context.generic;
  244. (* there are variants to do this on theories ... *)
  245. \<close>
  246. section\<open> The LCF-Kernel: terms, types, theories, proof\_contexts, thms \<close>
  247. text\<open>The classical LCF-style \<^emph>\<open>kernel\<close> is about
  248. \<^enum> Types and terms of a typed $\lambda$-Calculus including constant symbols,
  249. free variables, $\lambda$-binder and application,
  250. \<^enum> An infrastructure to define types and terms, a \<^emph>\<open>signature\<close>,
  251. that also assigns to constant symbols types
  252. \<^enum> An abstract type of \<^emph>\<open>theorem\<close> and logical operations on them
  253. \<^enum> (Isabelle specific): a notion of \<^emph>\<open>theory\<close>, i.e. a container
  254. providing a signature and set (list) of theorems.
  255. \<close>
  256. subsection\<open> Terms and Types \<close>
  257. text \<open>A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \<close>
  258. ML\<open> open Term;
  259. signature TERM' = sig
  260. (* ... *)
  261. type indexname = string * int
  262. type class = string
  263. type sort = class list
  264. type arity = string * sort list * sort
  265. datatype typ =
  266. Type of string * typ list |
  267. TFree of string * sort |
  268. TVar of indexname * sort
  269. datatype term =
  270. Const of string * typ |
  271. Free of string * typ |
  272. Var of indexname * typ |
  273. Bound of int |
  274. Abs of string * typ * term |
  275. $ of term * term
  276. exception TYPE of string * typ list * term list
  277. exception TERM of string * term list
  278. (* ... *)
  279. end
  280. \<close>
  281. text\<open>This core-data structure of the Isabelle Kernel is accessible in the Isabelle/ML environment
  282. and serves as basis for programmed extensions concerning syntax, type-checking, and advanced
  283. tactic programming over kernel primitives and higher API's. There are a number of anti-quotations
  284. giving support for this task; since @{ML Const}-names are long-names revealing information
  285. of the potentially evolving library structure, the use of anti-quotations leads to a safer programming
  286. style of tactics and became therefore standard in the entire Isabelle code-base.
  287. \<close>
  288. text\<open>The following examples show how term- and type-level antiquotations are used and that
  289. they can both be used for term-construction as well as term-destruction (pattern-matching):\<close>
  290. ML\<open> val Const ("HOL.implies", @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"})
  291. $ Free ("A", @{typ "bool"})
  292. $ Free ("B", @{typ "bool"})
  293. = @{term "A \<longrightarrow> B"};
  294. val "HOL.bool" = @{type_name "bool"};
  295. (* three ways to write type bool:@ *)
  296. val Type("fun",[s,Type("fun",[@{typ "bool"},Type(@{type_name "bool"},[])])]) = @{typ "bool \<Rightarrow> bool \<Rightarrow> bool"};
  297. \<close>
  298. text\<open>Note that the SML interpreter is configured that he will actually print a type
  299. \<^verbatim>\<open>Type("HOL.bool",[])\<close> just as \<^verbatim>\<open>"bool": typ\<close>, so a compact notation looking
  300. pretty much like a string. This can be confusing at times.\<close>
  301. text\<open>Note, furthermore, that there is a programming API for the HOL-instance of Isabelle:
  302. it is contained in @{file "$ISABELLE_HOME/src/HOL/Tools/hologic.ML"}. It offers for many
  303. operators of the HOL logic specific constructors and destructors:
  304. \<close>
  305. ML\<open>
  306. HOLogic.boolT : typ;
  307. HOLogic.mk_Trueprop: term -> term;
  308. HOLogic.dest_Trueprop: term -> term;
  309. HOLogic.Trueprop_conv: conv -> conv;
  310. HOLogic.mk_setT: typ -> typ;
  311. HOLogic.dest_setT: typ -> typ;
  312. HOLogic.Collect_const: typ -> term;
  313. HOLogic.mk_Collect: string * typ * term -> term;
  314. HOLogic.mk_mem: term * term -> term;
  315. HOLogic.dest_mem: term -> term * term;
  316. HOLogic.mk_set: typ -> term list -> term;
  317. HOLogic.conj_intr: Proof.context -> thm -> thm -> thm;
  318. HOLogic.conj_elim: Proof.context -> thm -> thm * thm;
  319. HOLogic.conj_elims: Proof.context -> thm -> thm list;
  320. HOLogic.conj: term;
  321. HOLogic.disj: term;
  322. HOLogic.imp: term;
  323. HOLogic.Not: term;
  324. HOLogic.mk_not: term -> term;
  325. HOLogic.mk_conj: term * term -> term;
  326. HOLogic.dest_conj: term -> term list;
  327. HOLogic.conjuncts: term -> term list;
  328. (* ... *)
  329. \<close>
  330. subsection\<open> Type-Certification (=checking that a type annotation is consistent) \<close>
  331. ML\<open> Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) \<close>
  332. text\<open> there is a joker type that can be added as place-holder during term construction.
  333. Jokers can be eliminated by the type inference. \<close>
  334. ML\<open> Term.dummyT : typ \<close>
  335. ML\<open>
  336. Sign.typ_instance: theory -> typ * typ -> bool;
  337. Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv;
  338. Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int;
  339. Sign.const_type: theory -> string -> typ option;
  340. Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*)
  341. Sign.cert_term: theory -> term -> term; (* short-cut for the latter *)
  342. Sign.tsig_of: theory -> Type.tsig (* projects the type signature *)
  343. \<close>
  344. text\<open>
  345. @{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure
  346. @{ML_structure "Type"}
  347. which contains the heart of the type inference.
  348. It also contains the type substitution type @{ML_type "Type.tyenv"} which is
  349. is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"}
  350. which in itself is a synonym for @{ML_type "'a Symtab.table"}, so
  351. possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. \<close>
  352. text\<open>Note that @{emph \<open>polymorphic variables\<close>} are treated like constant symbols
  353. in the type inference; thus, the following test, that one type is an instance of the
  354. other, yields false:
  355. \<close>
  356. ML\<open>
  357. val ty = @{typ "'a option"};
  358. val ty' = @{typ "int option"};
  359. val Type("List.list",[S]) = @{typ "('a) list"}; (* decomposition example *)
  360. val false = Sign.typ_instance @{theory}(ty', ty);
  361. \<close>
  362. text\<open>In order to make the type inference work, one has to consider @{emph \<open>schematic\<close>}
  363. type variables, which are more and more hidden from the Isar interface. Consequently,
  364. the typ antiquotation above will not work for schematic type variables and we have
  365. to construct them by hand on the SML level: \<close>
  366. ML\<open>
  367. val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]);
  368. \<close>
  369. text\<open> MIND THE "'" !!!\<close>
  370. text \<open>On this basis, the following @{ML_type "Type.tyenv"} is constructed: \<close>
  371. ML\<open>
  372. val tyenv = Sign.typ_match ( @{theory})
  373. (t_schematic, @{typ "int list"})
  374. (Vartab.empty);
  375. val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv;
  376. \<close>
  377. text\<open> Type generalization --- the conversion between free type variables and schematic
  378. type variables --- is apparently no longer part of the standard API (there is a slightly
  379. more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to
  380. overcome this by a self-baked generalization function:\<close>
  381. ML\<open>
  382. val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
  383. val generalize_term = Term.map_types generalize_typ;
  384. val true = Sign.typ_instance @{theory} (ty', generalize_typ ty)
  385. \<close>
  386. text\<open>... or more general variants thereof that are parameterized by the indexes for schematic
  387. type variables instead of assuming just @{ML "0"}. \<close>
  388. text\<open> Example:\<close>
  389. ML\<open>val t = generalize_term @{term "[]"}\<close>
  390. text
  391. \<open>Now we turn to the crucial issue of type-instantiation and with a given type environment
  392. @{ML "tyenv"}. For this purpose, one has to switch to the low-level interface
  393. @{ML_structure "Term_Subst"}.
  394. \<close>
  395. ML\<open>
  396. Term_Subst.map_types_same : (typ -> typ) -> term -> term;
  397. Term_Subst.map_aterms_same : (term -> term) -> term -> term;
  398. Term_Subst.instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term -> term;
  399. Term_Subst.instantiateT: ((indexname * sort) * typ) list -> typ -> typ;
  400. Term_Subst.generalizeT: string list -> int -> typ -> typ;
  401. (* this is the standard type generalisation function !!!
  402. only type-frees in the string-list were taken into account. *)
  403. Term_Subst.generalize: string list * string list -> int -> term -> term
  404. (* this is the standard term generalisation function !!!
  405. only type-frees and frees in the string-lists were taken
  406. into account. *)
  407. \<close>
  408. text \<open>Apparently, a bizarre conversion between the old-style interface and
  409. the new-style @{ML "tyenv"} is necessary. See the following example.\<close>
  410. ML\<open>
  411. val S = Vartab.dest tyenv;
  412. val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
  413. (* it took me quite some time to find out that these two type representations,
  414. obscured by a number of type-synonyms, where actually identical. *)
  415. val ty = t_schematic;
  416. val ty' = Term_Subst.instantiateT S' t_schematic;
  417. val t = (generalize_term @{term "[]"});
  418. val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
  419. (* or alternatively : *)
  420. val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
  421. \<close>
  422. subsection\<open> Type-Inference (= inferring consistent type information if possible) \<close>
  423. text\<open> Type inference eliminates also joker-types such as @{ML dummyT} and produces
  424. instances for schematic type variables where necessary. In the case of success,
  425. it produces a certifiable term. \<close>
  426. ML\<open>
  427. Type_Infer_Context.infer_types: Proof.context -> term list -> term list
  428. \<close>
  429. subsection\<open> thy and the signature interface\<close>
  430. ML\<open>
  431. Sign.tsig_of: theory -> Type.tsig;
  432. Sign.syn_of : theory -> Syntax.syntax;
  433. Sign.of_sort : theory -> typ * sort -> bool ;
  434. \<close>
  435. subsection\<open> Thm's and the LCF-Style, "Mikro"-Kernel \<close>
  436. text\<open>
  437. The basic constructors and operations on theorems@{file "$ISABELLE_HOME/src/Pure/thm.ML"},
  438. a set of derived (Pure) inferences can be found in @{file "$ISABELLE_HOME/src/Pure/drule.ML"}.
  439. The main types provided by structure \<^verbatim>\<open>thm\<close> are certified types @{ML_type ctyp},
  440. certified terms @{ML_type cterm}, @{ML_type thm} as well as conversions @{ML_type conv}.
  441. \<close>
  442. ML\<open>
  443. signature BASIC_THM =
  444. sig
  445. type ctyp
  446. type cterm
  447. exception CTERM of string * cterm list
  448. type thm
  449. type conv = cterm -> thm
  450. exception THM of string * int * thm list
  451. end;
  452. \<close>
  453. text\<open>Certification of types and terms on the kernel-level is done by the generators:\<close>
  454. ML\<open>
  455. Thm.global_ctyp_of: theory -> typ -> ctyp;
  456. Thm.ctyp_of: Proof.context -> typ -> ctyp;
  457. Thm.global_cterm_of: theory -> term -> cterm;
  458. Thm.cterm_of: Proof.context -> term -> cterm;
  459. \<close>
  460. text\<open>... which perform type-checking in the given theory context in order to make a type
  461. or term "admissible" for the kernel.\<close>
  462. text\<open> We come now to the very heart of the LCF-Kernel of Isabelle, which
  463. provides the fundamental inference rules of Isabelle/Pure.
  464. Besides a number of destructors on @{ML_type thm}'s,
  465. the abstract data-type \<^verbatim>\<open>thm\<close> is used for logical objects of the form
  466. $\Gamma \vdash_\theta \phi$, where $\Gamma$ represents a set of local assumptions,
  467. $\theta$ the "theory" or more precisely the global context in which a formula $\phi$
  468. has been constructed just by applying the following operations representing
  469. logical inference rules:
  470. \<close>
  471. ML\<open>
  472. (*inference rules*)
  473. Thm.assume: cterm -> thm;
  474. Thm.implies_intr: cterm -> thm -> thm;
  475. Thm.implies_elim: thm -> thm -> thm;
  476. Thm.forall_intr: cterm -> thm -> thm;
  477. Thm.forall_elim: cterm -> thm -> thm;
  478. Thm.transfer : theory -> thm -> thm;
  479. Thm.generalize: string list * string list -> int -> thm -> thm;
  480. Thm.instantiate: ((indexname*sort)*ctyp)list * ((indexname*typ)*cterm) list -> thm -> thm;
  481. \<close>
  482. text\<open> They reflect the Pure logic depicted in a number of presentations such as
  483. M. Wenzel, \<^emph>\<open>Parallel Proof Checking in Isabelle/Isar\<close>, PLMMS 2009, or simiular papers.
  484. Notated as logical inference rules, these operations were presented as follows:
  485. \<close>
  486. side_by_side_figure*["text-elements"::side_by_side_figure,anchor="''fig-kernel1''",
  487. caption="''Pure Kernel Inference Rules I ''",relative_width="48",
  488. src="''figures/pure-inferences-I''",anchor2="''fig-kernel2''",
  489. caption2="''Pure Kernel Inference Rules II''",relative_width2="47",
  490. src2="''figures/pure-inferences-II''"]\<open> \<close>
  491. (*
  492. figure*[kir1::figure,relative_width="100",src="''figures/pure-inferences-I''"]
  493. \<open> Pure Kernel Inference Rules I.\<close>
  494. figure*[kir2::figure,relative_width="100",src="''figures/pure-inferences-II''"]
  495. \<open> Pure Kernel Inference Rules II. \<close>
  496. *)
  497. text\<open>Note that the transfer rule:
  498. \[
  499. \begin{prooftree}
  500. \Gamma \vdash_\theta \phi \qquad \qquad \theta \sqsubseteq \theta'
  501. \justifies
  502. \Gamma \vdash_{\theta'} \phi \qquad \qquad
  503. \end{prooftree}
  504. \]
  505. which is a consequence of explicit theories characteristic for Isabelle's LCF-kernel design
  506. and a remarkable difference to its sisters HOL-Light and HOL4; instead of transfer, these systems
  507. reconstruct proofs in an enlarged global context instead of taking the result and converting it.\<close>
  508. text\<open>Besides the meta-logical (Pure) implication $\_\Longrightarrow \_$, the Kernel axiomatizes
  509. also a Pure-Equality $\_ \equiv \_ $ used for definitions of constant symbols: \<close>
  510. ML\<open>
  511. Thm.reflexive: cterm -> thm;
  512. Thm.symmetric: thm -> thm;
  513. Thm.transitive: thm -> thm -> thm;
  514. \<close>
  515. text\<open>The operation:\<close>
  516. ML\<open> Thm.trivial: cterm -> thm; \<close>
  517. text\<open>... produces the elementary tautologies of the form @{prop "A \<Longrightarrow> A"},
  518. an operation used to start a backward-style proof.\<close>
  519. text\<open>The elementary conversions are:\<close>
  520. ML\<open>
  521. Thm.beta_conversion: bool -> conv;
  522. Thm.eta_conversion: conv;
  523. Thm.eta_long_conversion: conv;
  524. \<close>
  525. text\<open>On the level of @{ML_structure "Drule"}, a number of higher-level operations is established,
  526. which is in part accessible by a number of forward-reasoning notations on Isar-level.\<close>
  527. ML\<open>
  528. op RSN: thm * (int * thm) -> thm;
  529. op RS: thm * thm -> thm;
  530. op RLN: thm list * (int * thm list) -> thm list;
  531. op RL: thm list * thm list -> thm list;
  532. op MRS: thm list * thm -> thm;
  533. op OF: thm * thm list -> thm;
  534. op COMP: thm * thm -> thm;
  535. \<close>
  536. subsection\<open> Theories \<close>
  537. text \<open> This structure yields the datatype \verb*thy* which becomes the content of
  538. \verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
  539. which inspired me (bu) to this naming.
  540. \<close>
  541. ML\<open>
  542. (* intern Theory.Thy;
  543. datatype thy = Thy of
  544. {pos: Position.T,
  545. id: serial,
  546. axioms: term Name_Space.table,
  547. defs: Defs.T,
  548. wrappers: wrapper list * wrapper list};
  549. *)
  550. Theory.check: Proof.context -> string * Position.T -> theory;
  551. Theory.local_setup: (Proof.context -> Proof.context) -> unit;
  552. Theory.setup: (theory -> theory) -> unit; (* The thing to extend the table of "command"s with parser - callbacks. *)
  553. Theory.get_markup: theory -> Markup.T;
  554. Theory.axiom_table: theory -> term Name_Space.table;
  555. Theory.axiom_space: theory -> Name_Space.T;
  556. Theory.axioms_of: theory -> (string * term) list;
  557. Theory.all_axioms_of: theory -> (string * term) list;
  558. Theory.defs_of: theory -> Defs.T;
  559. Theory.at_begin: (theory -> theory option) -> theory -> theory;
  560. Theory.at_end: (theory -> theory option) -> theory -> theory;
  561. Theory.begin_theory: string * Position.T -> theory list -> theory;
  562. Theory.end_theory: theory -> theory;
  563. \<close>
  564. section\<open>Backward Proofs: Tactics, Tacticals and Goal-States\<close>
  565. text\<open>At this point, we leave the Pure-Kernel and start to describe the first layer on top
  566. of it, involving support for specific styles of reasoning and automation of reasoning.\<close>
  567. text\<open> \<^verbatim>\<open>tactic\<close>'s are in principle \<^emph>\<open>relations\<close> on theorems @{ML_type "thm"}; this gives a natural way
  568. to represent the fact that HO-Unification (and therefore the mechanism of rule-instantiation)
  569. are non-deterministic in principle. Heuristics may choose particular preferences between
  570. the theorems in the range of this relation, but the Isabelle Design accepts this fundamental
  571. fact reflected at this point in the prover architecture.
  572. This potentially infinite relation is implemented by a function of theorems to lazy lists
  573. over theorems, which gives both sufficient structure for heuristic
  574. considerations as well as a nice algebra, called \<^verbatim>\<open>TACTICAL\<close>'s, providing a bottom element
  575. @{ML "no_tac"} (the function that always fails), the top-element @{ML "all_tac"}
  576. (the function that never fails), sequential composition @{ML "op THEN"}, (serialized)
  577. non-deterministic composition @{ML "op ORELSE"}, conditionals, repetitions over lists, etc.
  578. The following is an excerpt of @{file "~~/src/Pure/tactical.ML"}:
  579. \<close>
  580. ML\<open>
  581. signature TACTICAL =
  582. sig
  583. type tactic = thm -> thm Seq.seq
  584. val all_tac: tactic
  585. val no_tac: tactic
  586. val COND: (thm -> bool) -> tactic -> tactic -> tactic
  587. val THEN: tactic * tactic -> tactic
  588. val ORELSE: tactic * tactic -> tactic
  589. val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
  590. val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
  591. val TRY: tactic -> tactic
  592. val EVERY: tactic list -> tactic
  593. val EVERY': ('a -> tactic) list -> 'a -> tactic
  594. val FIRST: tactic list -> tactic
  595. (* ... *)
  596. end
  597. \<close>
  598. text\<open>The next layer in the architecture describes @{ML_type \<open>tactic\<close>}'s, i.e. basic operations on
  599. theorems in a backward reasoning style (bottom up development of proof-trees). An initial goal-state
  600. for some property @{term A} --- the \<^emph>\<open>goal\<close> --- is constructed via the kernel
  601. @{ML "Thm.trivial"}-operation into @{term "A \<Longrightarrow> A"}, and tactics either refine the premises
  602. --- the \<^emph>\<open>subgoals\<close> the of this meta-implication ---
  603. producing more and more of them or eliminate them in subsequent goal-states. Subgoals of the form
  604. @{term "B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A \<Longrightarrow> B\<^sub>3 \<Longrightarrow> B\<^sub>4 \<Longrightarrow> A"} can be eliminated via
  605. the @{ML Tactic.assume_tac} - tactic,
  606. and a subgoal @{term C\<^sub>m} can be refined via the theorem
  607. @{term "E\<^sub>1 \<Longrightarrow> E\<^sub>2 \<Longrightarrow> E\<^sub>3 \<Longrightarrow> C\<^sub>m"} the @{ML Tactic.resolve_tac} - tactic to new subgoals
  608. @{term "E\<^sub>1"},@{term "E\<^sub>2"}, @{term "E\<^sub>3"}. In case that a theorem used for resolution
  609. has no premise @{term "E\<^sub>i"}, the subgoal @{term C\<^sub>m} is also eliminated ("closed").
  610. The following abstract of the most commonly used @{ML_type \<open>tactic\<close>}'s drawn from
  611. @{file "~~/src/Pure/tactic.ML"} looks as follows:
  612. \<close>
  613. ML\<open>
  614. (* ... *)
  615. assume_tac: Proof.context -> int -> tactic;
  616. compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic;
  617. resolve_tac: Proof.context -> thm list -> int -> tactic;
  618. eresolve_tac: Proof.context -> thm list -> int -> tactic;
  619. forward_tac: Proof.context -> thm list -> int -> tactic;
  620. dresolve_tac: Proof.context -> thm list -> int -> tactic;
  621. rotate_tac: int -> int -> tactic;
  622. defer_tac: int -> tactic;
  623. prefer_tac: int -> tactic;
  624. (* ... *)
  625. \<close>
  626. text\<open>Note that "applying a rule" is a fairly complex operation in the Extended Isabelle Kernel,
  627. i.e. the tactic layer. It involves at least four phases, interfacing a theorem
  628. coming from the global context $\theta$ (=theory), be it axiom or derived, into a given goal-state.
  629. \<^item> \<^emph>\<open>generalization\<close>. All free variables in the theorem were replaced by schematic variables.
  630. For example, @{term "x + y = y + x"} is converted into
  631. @{emph \<open>?x + ?y = ?y + ?x\<close> }.
  632. By the way, type variables were treated equally.
  633. \<^item> \<^emph>\<open>lifting over assumptions\<close>. If a subgoal is of the form:
  634. @{term "B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A"} and we have a theorem @{term "D\<^sub>1 \<Longrightarrow> D\<^sub>2 \<Longrightarrow> A"}, then before
  635. applying the theorem, the premisses were \<^emph>\<open>lifted\<close> resulting in the logical refinement:
  636. @{term "(B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>1) \<Longrightarrow> (B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>2) \<Longrightarrow> A"}. Now, @{ML "resolve_tac"}, for example,
  637. will replace the subgoal @{term "B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> A"} by the subgoals
  638. @{term "B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>1"} and @{term "B\<^sub>1 \<Longrightarrow> B\<^sub>2 \<Longrightarrow> D\<^sub>2"}. Of course, if the theorem wouldn't
  639. have assumptions @{term "D\<^sub>1"} and @{term "D\<^sub>2"}, the subgoal @{term "A"} would be replaced by
  640. \<^bold>\<open>nothing\<close>, i.e. deleted.
  641. \<^item> \<^emph>\<open>lifting over parameters\<close>. If a subgoal is meta-quantified like in:
  642. @{term "\<And> x y z. A x y z"}, then a theorem like @{term "D\<^sub>1 \<Longrightarrow> D\<^sub>2 \<Longrightarrow> A"} is \<^emph>\<open>lifted\<close>
  643. to @{term "\<And> x y z. D\<^sub>1' \<Longrightarrow> D\<^sub>2' \<Longrightarrow> A'"}, too. Since free variables occurring in @{term "D\<^sub>1"},
  644. @{term "D\<^sub>2"} and @{term "A"} have been replaced by schematic variables (see phase one),
  645. they must be replaced by parameterized schematic variables, i. e. a kind of skolem function.
  646. For example, @{emph \<open>?x + ?y = ?y + ?x\<close> } would be lifted to
  647. @{emph \<open>!! x y z. ?x x y z + ?y x y z = ?y x y z + ?x x y z\<close>}. This way, the lifted theorem
  648. can be instantiated by the parameters @{term "x y z"} representing "fresh free variables"
  649. used for this sub-proof. This mechanism implements their logically correct bookkeeping via
  650. kernel primitives.
  651. \<^item> \<^emph>\<open>Higher-order unification (of schematic type and term variables)\<close>.
  652. Finally, for all these schematic variables, a solution must be found.
  653. In the case of @{ML resolve_tac}, the conclusion of the (doubly lifted) theorem must
  654. be equal to the conclusion of the subgoal, so @{term A} must be $\alpha/\beta$-equivalent to
  655. @{term A'} in the example above, which is established by a higher-order unification
  656. process. It is a bit unfortunate that for implementation efficiency reasons, a very substantial
  657. part of the code for HO-unification is in the kernel module @{ML_type "thm"}, which makes this
  658. critical component of the architecture larger than necessary.
  659. \<close>
  660. text\<open>In a way, the two lifting processes represent an implementation of the conversion between
  661. Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and
  662. Gentzen Sequent Deduction.\<close>
  663. section\<open>The classical goal package\<close>
  664. ML\<open> open Goal;
  665. Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm;
  666. Goal.prove_global : theory -> string list -> term list -> term ->
  667. ({context: Proof.context, prems: thm list} -> tactic) -> thm
  668. \<close>
  669. section\<open>The Isar Engine\<close>
  670. ML\<open>
  671. Toplevel.theory;
  672. Toplevel.presentation_context_of; (* Toplevel is a kind of table with call-back functions *)
  673. Consts.the_const; (* T is a kind of signature ... *)
  674. Variable.import_terms;
  675. Vartab.update;
  676. fun control_antiquotation name s1 s2 =
  677. Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
  678. (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
  679. Output.output;
  680. Syntax.read_input ;
  681. Input.source_content;
  682. (*
  683. basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
  684. *)
  685. \<close>
  686. ML\<open>
  687. Config.get @{context} Thy_Output.display;
  688. Config.get @{context} Thy_Output.source;
  689. Config.get @{context} Thy_Output.modes;
  690. Thy_Output.document_command;
  691. (* is:
  692. fun document_command markdown (loc, txt) =
  693. Toplevel.keep (fn state =>
  694. (case loc of
  695. NONE => ignore (output_text state markdown txt)
  696. | SOME (_, pos) =>
  697. error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  698. Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
  699. end;
  700. *)
  701. \<close>
  702. ML\<open> Thy_Output.document_command {markdown = true} \<close>
  703. (* Structures related to LaTeX Generation *)
  704. ML\<open> Latex.output_ascii;
  705. Latex.output_token
  706. (* Hm, generierter output for
  707. subsection*[Shaft_Encoder_characteristics]{ * Shaft Encoder Characteristics * } :
  708. \begin{isamarkuptext}%
  709. \isa{{\isacharbackslash}label{\isacharbraceleft}general{\isacharunderscore}hyps{\isacharbraceright}}%
  710. \end{isamarkuptext}\isamarkuptrue%
  711. \isacommand{subsection{\isacharasterisk}}\isamarkupfalse%
  712. {\isacharbrackleft}Shaft{\isacharunderscore}Encoder{\isacharunderscore}characteristics{\isacharbrackright}{\isacharverbatimopen}\ Shaft\ Encoder\ Characteristics\ {\isacharverbatimclose}%
  713. Generierter output for: text\<open>\label{sec:Shaft-Encoder-characteristics}\<close>
  714. \begin{isamarkuptext}%
  715. \label{sec:Shaft-Encoder-characteristics}%
  716. \end{isamarkuptext}\isamarkuptrue%
  717. *)
  718. \<close>
  719. ML\<open>
  720. Thy_Output.maybe_pretty_source :
  721. (Proof.context -> 'a -> Pretty.T) -> Proof.context -> Token.src -> 'a list -> Pretty.T list;
  722. Thy_Output.output: Proof.context -> Pretty.T list -> string;
  723. (* nuescht besonderes *)
  724. fun document_antiq check_file ctxt (name, pos) =
  725. let
  726. (* val dir = master_directory (Proof_Context.theory_of ctxt); *)
  727. (* val _ = check_path check_file ctxt dir (name, pos); *)
  728. in
  729. space_explode "/" name
  730. |> map Latex.output_ascii
  731. |> space_implode (Latex.output_ascii "/" ^ "\\discretionary{}{}{}")
  732. |> enclose "\\isatt{" "}"
  733. end;
  734. \<close>
  735. ML\<open> Type_Infer_Context.infer_types \<close>
  736. ML\<open> Type_Infer_Context.prepare_positions \<close>
  737. subsection \<open>Transaction Management in the Isar-Engine : The Toplevel \<close>
  738. ML\<open>
  739. Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
  740. Thy_Output.document_command;
  741. Toplevel.exit: Toplevel.transition -> Toplevel.transition;
  742. Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
  743. Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
  744. Toplevel.ignored: Position.T -> Toplevel.transition;
  745. Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition;
  746. Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition;
  747. Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
  748. Toplevel.present_local_theory:
  749. (xstring * Position.T) option ->
  750. (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
  751. (* where text treatment and antiquotation parsing happens *)
  752. (*fun document_command markdown (loc, txt) =
  753. Toplevel.keep (fn state =>
  754. (case loc of
  755. NONE => ignore (output_text state markdown txt)
  756. | SOME (_, pos) =>
  757. error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  758. Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *)
  759. Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
  760. Toplevel.transition -> Toplevel.transition;
  761. (* Isar Toplevel Steuerung *)
  762. Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
  763. (* val keep' = add_trans o Keep;
  764. fun keep f = add_trans (Keep (fn _ => f));
  765. *)
  766. Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) ->
  767. Toplevel.transition -> Toplevel.transition;
  768. (* fun present_local_theory target = present_transaction (fn int =>
  769. (fn Theory (gthy, _) =>
  770. let val (finish, lthy) = Named_Target.switch target gthy;
  771. in Theory (finish lthy, SOME lthy) end
  772. | _ => raise UNDEF));
  773. fun present_transaction f g = add_trans (Transaction (f, g));
  774. fun transaction f = present_transaction f (K ());
  775. *)
  776. Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
  777. (* fun theory' f = transaction (fn int =>
  778. (fn Theory (Context.Theory thy, _) =>
  779. let val thy' = thy
  780. |> Sign.new_group
  781. |> f int
  782. |> Sign.reset_group;
  783. in Theory (Context.Theory thy', NONE) end
  784. | _ => raise UNDEF));
  785. fun theory f = theory' (K f); *)
  786. Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
  787. Toplevel.transition -> Toplevel.transition;
  788. (* fun document_command markdown (loc, txt) =
  789. Toplevel.keep (fn state =>
  790. (case loc of
  791. NONE => ignore (output_text state markdown txt)
  792. | SOME (_, pos) =>
  793. error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  794. Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
  795. *)
  796. Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ;
  797. (* this is where antiquotation expansion happens : uses eval_antiquote *)
  798. \<close>
  799. ML\<open>
  800. (* Isar Toplevel Steuerung *)
  801. Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition;
  802. (* val keep' = add_trans o Keep;
  803. fun keep f = add_trans (Keep (fn _ => f));
  804. *)
  805. Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) ->
  806. Toplevel.transition -> Toplevel.transition;
  807. (* fun present_local_theory target = present_transaction (fn int =>
  808. (fn Theory (gthy, _) =>
  809. let val (finish, lthy) = Named_Target.switch target gthy;
  810. in Theory (finish lthy, SOME lthy) end
  811. | _ => raise UNDEF));
  812. fun present_transaction f g = add_trans (Transaction (f, g));
  813. fun transaction f = present_transaction f (K ());
  814. *)
  815. Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition;
  816. (* fun theory' f = transaction (fn int =>
  817. (fn Theory (Context.Theory thy, _) =>
  818. let val thy' = thy
  819. |> Sign.new_group
  820. |> f int
  821. |> Sign.reset_group;
  822. in Theory (Context.Theory thy', NONE) end
  823. | _ => raise UNDEF));
  824. fun theory f = theory' (K f); *)
  825. Thy_Output.document_command : {markdown: bool} -> (xstring * Position.T) option * Input.source ->
  826. Toplevel.transition -> Toplevel.transition;
  827. (* fun document_command markdown (loc, txt) =
  828. Toplevel.keep (fn state =>
  829. (case loc of
  830. NONE => ignore (output_text state markdown txt)
  831. | SOME (_, pos) =>
  832. error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  833. Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
  834. *)
  835. Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> string ;
  836. (* this is where antiquotation expansion happens : uses eval_antiquote *)
  837. \<close>
  838. subsection\<open> Configuration flags of fixed type in the Isar-engine. \<close>
  839. ML\<open>
  840. Config.get @{context} Thy_Output.quotes;
  841. Config.get @{context} Thy_Output.display;
  842. val C = Synchronized.var "Pretty.modes" "latEEex";
  843. (* Synchronized: a mechanism to bookkeep global
  844. variables with synchronization mechanism included *)
  845. Synchronized.value C;
  846. (*
  847. fun output ctxt prts =
  848. 603 prts
  849. 604 |> Config.get ctxt quotes ? map Pretty.quote
  850. 605 |> (if Config.get ctxt display then
  851. 606 map (Pretty.indent (Config.get ctxt indent) #> string_of_margin ctxt #> Output.output)
  852. 607 #> space_implode "\\isasep\\isanewline%\n"
  853. 608 #> Latex.environment "isabelle"
  854. 609 else
  855. 610 map
  856. 611 ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of)
  857. 612 #> Output.output)
  858. 613 #> space_implode "\\isasep\\isanewline%\n"
  859. 614 #> enclose "\\isa{" "}");
  860. *)
  861. \<close>
  862. chapter\<open>Front-End \<close>
  863. text\<open>In the following chapter, we turn to the right part of the system architecture
  864. shown in @{docitem \<open>architecture\<close>}:
  865. The PIDE ("Prover-IDE") layer consisting of a part written in SML and another in SCALA.
  866. Roughly speaking, PIDE implements "continuous build - continuous check" - functionality
  867. over a textual, albeit generic document model. It transforms user modifications
  868. of text elements in an instance of this model into increments (edits) and communicates
  869. them to the Isabelle system. The latter reacts by the creation of a multitude of light-weight
  870. reevaluation threads resulting in an asynchronous stream of markup that is used to annotate text
  871. elements. Such markup is used to highlight, e.g., variables
  872. or keywords with specific colors, to hyper-linking bound variables to their defining occurrences,
  873. or to annotate type-information to terms which becomes displayed by specific
  874. user-gestures on demand (hovering), etc.
  875. Note that PIDE is not an editor, it is the framework that
  876. coordinates these asynchronous information streams and optimizes it to a certain
  877. extent (outdated markup referring to modified text is dropped, and
  878. corresponding re-calculations are oriented to the user focus, for example).
  879. Four concrete editors --- also called PIDE applications --- have been implemented:
  880. \<^enum>an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version),
  881. \<^enum>a Visual-Studio Code plugin (developed by Makarius Wenzel),
  882. currently based on a fairly old PIDE version,
  883. \<^enum>clide, a web-client supporting javascript and HTML5
  884. (developed by a group at University Bremen, based on a very old PIDE version), and
  885. \<^enum>the most commonly used: the plugin in JEdit - Editor,
  886. (developed by Makarius Wenzel, current PIDE version.)
  887. \<close>
  888. text\<open>The document model forsees a number of text files, which are organized in form of an acyclic graph. Such graphs can be
  889. grouped into \<^emph>\<open>sessions\<close> and "frozen" to binaries in order to avoid long compilation
  890. times. Text files have an abstract name serving as identity (the mapping to file-paths
  891. in an underlying file-system is done in an own build management).
  892. The primary format of the text files is \<^verbatim>\<open>.thy\<close> (historically for: theory),
  893. secondary formats can be \<^verbatim>\<open>.sty\<close>,\<^verbatim>\<open>.tex\<close>, \<^verbatim>\<open>.png\<close>, \<^verbatim>\<open>.pdf\<close>, or other files processed
  894. by Isabelle and listed in a configuration processed by the build system.
  895. \<close>
  896. figure*[fig3::figure, relative_width="100",src="''figures/document-model''"]
  897. \<open>A Theory-Graph in the Document Model\<close>
  898. text\<open>A \<^verbatim>\<open>.thy\<close> file consists of a \<^emph>\<open>header\<close>, a \<^emph>\<open>context-definition\<close> and
  899. a \<^emph>\<open>body\<close> consisting of a sequence of \<^emph>\<open>commands\<close>. Even the header consists of
  900. a sequence of commands used for introductory text elements not depending on any context
  901. information (so: practically excluding any form of text antiquotation (see above)).
  902. The context-definition contains an \<^emph>\<open>import\<close> and a \<^emph>\<open>keyword\<close> section;
  903. for example:
  904. \begin{verbatim}
  905. theory Isa_DOF (* Isabelle Document Ontology Framework *)
  906. imports Main
  907. RegExpInterface (* Interface to functional regular automata for monitoring *)
  908. Assert
  909. keywords "+=" ":=" "accepts" "rejects"
  910. \end{verbatim}
  911. where \<^verbatim>\<open>Isa_DOF\<close> is the abstract name of the text-file, \<^verbatim>\<open>Main\<close> etc. refer to imported
  912. text files (recall that the import relation must be acyclic). \<^emph>\<open>keyword\<close>s are used to separate
  913. commands form each other;
  914. predefined commands allow for the dynamic creation of new commands similarly
  915. to the definition of new functions in an interpreter shell (or: toplevel, see above.).
  916. A command starts with a pre-declared keyword and specific syntax of this command;
  917. the declaration of a keyword is only allowed in the same \<^verbatim>\<open>.thy\<close>-file where the
  918. the corresponding new command is defined. The semantics of the command is expressed
  919. in ML and consists of a @{ML_type "Toplevel.transition -> Toplevel.transition"}
  920. function. Thus, the Isar-toplevel supports the generic document model
  921. and allows for user-programmed extensions.
  922. \<close>
  923. text\<open>Isabelle \<^verbatim>\<open>.thy\<close>-files were processed by two types of parsers:
  924. \<^enum> the "outer-syntax" (i.e. the syntax for commands) is processed
  925. by a lexer-library and parser combinators built on top, and
  926. \<^enum> the "inner-syntax" (i.e. the syntax for @{term \<open>\<Lambda>\<close>} - terms)
  927. with an evolved, eight-layer parsing and pretty-printing process.
  928. \<close>
  929. section\<open>Basics: string, bstring and xstring\<close>
  930. text\<open>@{ML_type "string"} is the basic library type from the SML library
  931. in structure @{ML_structure "String"}. Many Isabelle operations produce
  932. or require formats thereof introduced as type synonyms
  933. @{ML_type "bstring"} (defined in structure @{ML_structure "Binding"}
  934. and @{ML_type "xstring"} (defined in structure @{ML_structure "Name_Space"}.
  935. Unfortunately, the abstraction is not tight and combinations with
  936. elementary routines might produce quite crappy results.
  937. \<close>
  938. ML\<open>val b = Binding.name_of@{binding "here"}\<close>
  939. text\<open>... produces the system output \verb+val it = "here": bstring+,
  940. but note that it is misleading to believe it is just a string.
  941. \<close>
  942. ML\<open>String.explode b\<close> (* is harmless, but *)
  943. ML\<open>String.explode(Binding.name_of
  944. (Binding.conglomerate[Binding.qualified_name "X.x",
  945. @{binding "here"}] ))\<close>
  946. (* Somehow it is possible to smuggle markup into bstrings; and this leads
  947. ML\<open>(((String.explode(!ODL_Command_Parser.SPY6))))\<close>
  948. to something like
  949. val it = [#"\^E", #"\^F", #"i", #"n", #"p", #"u", #"t", #"\^F", #"d", #"e", #"l", #"i", #"m", #"i", #"t", #"e", #"d", #"=", #"f", #"a", ...]: char list
  950. *)
  951. text\<open> However, there is an own XML parser for this format. See Section Markup.
  952. \<close>
  953. ML\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
  954. (* MORE TO COME *)
  955. section\<open>Positions\<close>
  956. text\<open>A basic data-structure relevant for PIDE are \<^emph>\<open>positions\<close>; beyond the usual line- and column
  957. information they can represent ranges, list of ranges, and the name of the atomic sub-document
  958. in which they are contained. In the command:\<close>
  959. ML\<open>
  960. val pos = @{here};
  961. val markup = Position.here pos;
  962. writeln ("And a link to the declaration of 'here' is "^markup)
  963. \<close>
  964. (* \<^here> *)
  965. text\<open> ... uses the antiquotation @{ML "@{here}"} to infer from the system lexer the actual position
  966. of itself in the global document, converts it to markup (a string-representation of it) and sends
  967. it via the usual @{ML "writeln"} to the interface. \<close>
  968. figure*[hyplinkout::figure,relative_width="40",src="''figures/markup-demo''"]
  969. \<open>Output with hyperlinked position.\<close>
  970. text\<open>@{docitem \<open>hyplinkout\<close>} shows the produced output where the little house-like symbol in the
  971. display is hyperlinked to the position of @{ML "@{here}"} in the ML sample above.\<close>
  972. section\<open>Markup and Low-level Markup Reporting\<close>
  973. text\<open>The structures @{ML_structure Markup} and @{ML_structure Properties} represent the basic
  974. annotation data which is part of the protocol sent from Isabelle to the frontend.
  975. They are qualified as "quasi-abstract", which means they are intended to be an abstraction of
  976. the serialized, textual presentation of the protocol. Markups are structurally a pair of a key
  977. and properties; @{ML_structure Markup} provides a number of of such \<^emph>\<open>key\<close>s for annotation classes
  978. such as "constant", "fixed", "cartouche", some of them quite obscure. Here is a code sample
  979. from \<^theory_text>\<open>Isabelle_DOF\<close>. A markup must be tagged with an id; this is done by the @{ML serial}-function
  980. discussed earlier.\<close>
  981. ML\<open>
  982. local
  983. val docclassN = "doc_class";
  984. (* derived from: theory_markup; def for "defining occurrence" (true) in contrast to
  985. "referring occurence" (false). *)
  986. fun docclass_markup def name id pos =
  987. if id = 0 then Markup.empty
  988. else Markup.properties (Position.entity_properties_of def id pos)
  989. (Markup.entity docclassN name);
  990. in
  991. fun report_defining_occurrence pos cid =
  992. let val id = serial ()
  993. val markup_of_cid = docclass_markup true cid id pos
  994. in Position.report pos markup_of_cid end;
  995. end
  996. \<close>
  997. text\<open>The @\<open>ML report_defining_occurrence\<close>-function above takes a position and a "cid" parsed
  998. in the Front-End, converts this into markup together with a unique number identifying this
  999. markup, and sends this as a report to the Front-End. \<close>
  1000. section\<open>Environment Structured Reporting\<close>
  1001. text\<open> @{ML_type "'a Name_Space.table"} \<close>
  1002. section\<open> Parsing issues \<close>
  1003. text\<open> Parsing combinators represent the ground building blocks of both generic input engines
  1004. as well as the specific Isar framework. They are implemented in the structure \verb+Token+
  1005. providing core type \verb+Token.T+.
  1006. \<close>
  1007. ML\<open> open Token\<close>
  1008. ML\<open>
  1009. (* Provided types : *)
  1010. (*
  1011. type 'a parser = T list -> 'a * T list
  1012. type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
  1013. *)
  1014. (* conversion between these two : *)
  1015. fun parser2contextparser pars (ctxt, toks) = let val (a, toks') = pars toks
  1016. in (a,(ctxt, toks')) end;
  1017. val _ = parser2contextparser : 'a parser -> 'a context_parser;
  1018. (* bah, is the same as Scan.lift *)
  1019. val _ = Scan.lift Args.cartouche_input : Input.source context_parser;
  1020. Token.is_command;
  1021. Token.content_of; (* textueller kern eines Tokens. *)
  1022. \<close>
  1023. text\<open> Tokens and Bindings \<close>
  1024. ML\<open>
  1025. val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position,
  1026. where \<dieresis>positions\<dieresis> are absolute references to a file *)
  1027. Binding.make: bstring * Position.T -> binding;
  1028. Binding.pos_of @{binding erzerzer};
  1029. Position.here: Position.T -> string;
  1030. (* Bindings *)
  1031. ML\<open>val X = @{here};\<close>
  1032. \<close>
  1033. subsection \<open>Input streams. \<close>
  1034. ML\<open>
  1035. Input.source_explode : Input.source -> Symbol_Pos.T list;
  1036. (* conclusion: Input.source_explode converts " f @{thm refl}"
  1037. into:
  1038. [(" ", {offset=14, id=-2769}), ("f", {offset=15, id=-2769}), (" ", {offset=16, id=-2769}),
  1039. ("@", {offset=17, id=-2769}), ("{", {offset=18, id=-2769}), ("t", {offset=19, id=-2769}),
  1040. ("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}),
  1041. ("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}),
  1042. ("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})]
  1043. *)\<close>
  1044. subsection \<open>Scanning and combinator parsing. \<close>
  1045. text\<open>Is used on two levels:
  1046. \<^enum> outer syntax, that is the syntax in which Isar-commands are written, and
  1047. \<^enum> inner-syntax, that is the syntax in which lambda-terms, and in particular HOL-terms were written.
  1048. \<close>
  1049. text\<open> A constant problem for newbies is this distinction, which makes it necessary that
  1050. the " ... " quotes have to be used when switching to inner-syntax, except when only one literal
  1051. is expected when an inner-syntax term is expected.
  1052. \<close>
  1053. ML\<open>
  1054. Scan.peek : ('a -> 'b -> 'c * 'd) -> 'a * 'b -> 'c * ('a * 'd);
  1055. Scan.optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a;
  1056. Scan.option: ('a -> 'b * 'a) -> 'a -> 'b option * 'a;
  1057. Scan.repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a;
  1058. Scan.lift : ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c);
  1059. Scan.lift (Parse.position Args.cartouche_input);
  1060. \<close>
  1061. text\<open> "parsers" are actually interpreters; an 'a parser is a function that parses
  1062. an input stream and computes(=evaluates, computes) it into 'a.
  1063. Since the semantics of an Isabelle command is a transition => transition
  1064. or theory $\Rightarrow$ theory function, i.e. a global system transition.
  1065. parsers of that type can be constructed and be bound as call-back functions
  1066. to a table in the Toplevel-structure of Isar.
  1067. The type 'a parser is already defined in the structure Token.
  1068. \<close>
  1069. text\<open> Syntax operations : Interface for parsing, type-checking, "reading"
  1070. (both) and pretty-printing.
  1071. Note that this is a late-binding interface, i.e. a collection of "hooks".
  1072. The real work is done ... see below.
  1073. Encapsulates the data structure "syntax" --- the table with const symbols,
  1074. print and ast translations, ... The latter is accessible, e.g. from a Proof
  1075. context via @{ML Proof_Context.syn_of}.
  1076. \<close>
  1077. ML\<open>
  1078. Parse.nat: int parser;
  1079. Parse.int: int parser;
  1080. Parse.enum_positions: string -> 'a parser -> ('a list * Position.T list) parser;
  1081. Parse.enum: string -> 'a parser -> 'a list parser;
  1082. Parse.input: 'a parser -> Input.source parser;
  1083. Parse.enum : string -> 'a parser -> 'a list parser;
  1084. Parse.!!! : (T list -> 'a) -> T list -> 'a;
  1085. Parse.position: 'a parser -> ('a * Position.T) parser;
  1086. (* Examples *)
  1087. Parse.position Args.cartouche_input;
  1088. \<close>
  1089. text\<open> Inner Syntax Parsing combinators for elementary Isabelle Lexems\<close>
  1090. ML\<open>
  1091. Syntax.parse_sort : Proof.context -> string -> sort;
  1092. Syntax.parse_typ : Proof.context -> string -> typ;
  1093. Syntax.parse_term : Proof.context -> string -> term;
  1094. Syntax.parse_prop : Proof.context -> string -> term;
  1095. Syntax.check_term : Proof.context -> term -> term;
  1096. Syntax.check_props: Proof.context -> term list -> term list;
  1097. Syntax.uncheck_sort: Proof.context -> sort -> sort;
  1098. Syntax.uncheck_typs: Proof.context -> typ list -> typ list;
  1099. Syntax.uncheck_terms: Proof.context -> term list -> term list;\<close>
  1100. text\<open>In contrast to mere parsing, the following operators provide also type-checking
  1101. and internal reporting to PIDE --- see below. I did not find a mechanism to address
  1102. the internal serial-numbers used for the PIDE protocol, however, rumours have it
  1103. that such a thing exists. The variants \<^verbatim>\<open>_global\<close> work on theories instead on
  1104. @{ML_type "Proof.context"}s.\<close>
  1105. ML\<open>
  1106. Syntax.read_sort: Proof.context -> string -> sort;
  1107. Syntax.read_typ : Proof.context -> string -> typ;
  1108. Syntax.read_term: Proof.context -> string -> term;
  1109. Syntax.read_typs: Proof.context -> string list -> typ list;
  1110. Syntax.read_sort_global: theory -> string -> sort;
  1111. Syntax.read_typ_global: theory -> string -> typ;
  1112. Syntax.read_term_global: theory -> string -> term;
  1113. Syntax.read_prop_global: theory -> string -> term;
  1114. \<close>
  1115. text \<open>The following operations are concerned with the conversion of pretty-prints
  1116. and, from there, the generation of (non-layouted) strings.\<close>
  1117. ML\<open>
  1118. Syntax.pretty_term:Proof.context -> term -> Pretty.T;
  1119. Syntax.pretty_typ:Proof.context -> typ -> Pretty.T;
  1120. Syntax.pretty_sort:Proof.context -> sort -> Pretty.T;
  1121. Syntax.pretty_classrel: Proof.context -> class list -> Pretty.T;
  1122. Syntax.pretty_arity: Proof.context -> arity -> Pretty.T;
  1123. Syntax.string_of_term: Proof.context -> term -> string;
  1124. Syntax.string_of_typ: Proof.context -> typ -> string;
  1125. Syntax.lookup_const : Syntax.syntax -> string -> string option;
  1126. \<close>
  1127. ML\<open>
  1128. fun read_terms ctxt =
  1129. grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt;
  1130. \<close>
  1131. ML\<open>
  1132. (* More High-level, more Isar-specific Parsers *)
  1133. Args.name;
  1134. Args.const;
  1135. Args.cartouche_input: Input.source parser;
  1136. Args.text_token: Token.T parser;
  1137. val Z = let val attribute = Parse.position Parse.name --
  1138. Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
  1139. in (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) end ;
  1140. (* this leads to constructions like the following, where a parser for a *)
  1141. fn name => (Thy_Output.antiquotation name (Scan.lift (Parse.position Args.cartouche_input)));
  1142. \<close>
  1143. section\<open>\<close>
  1144. ML\<open>Sign.add_trrules\<close>
  1145. section\<open> The PIDE Framework \<close>
  1146. subsection\<open> Markup \<close>
  1147. text\<open> Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR.
  1148. Markup operation send via side-effect annotations to the GUI (precisely:
  1149. to the PIDE Framework) that were used for hyperlinking applicating to binding
  1150. occurrences, info for hovering, ... \<close>
  1151. ML\<open>
  1152. (* Position.report is also a type consisting of a pair of a position and markup. *)
  1153. (* It would solve all my problems if I find a way to infer the defining Position.report
  1154. from a type definition occurence ... *)
  1155. Position.report: Position.T -> Markup.T -> unit;
  1156. Position.reports: Position.report list -> unit;
  1157. (* ? ? ? I think this is the magic thing that sends reports to the GUI. *)
  1158. Markup.entity : string -> string -> Markup.T;
  1159. Markup.properties : Properties.T -> Markup.T -> Markup.T ;
  1160. Properties.get : Properties.T -> string -> string option;
  1161. Markup.enclose : Markup.T -> string -> string;
  1162. (* example for setting a link, the def flag controls if it is a defining or a binding
  1163. occurence of an item *)
  1164. fun theory_markup (def:bool) (name:string) (id:serial) (pos:Position.T) =
  1165. if id = 0 then Markup.empty
  1166. else
  1167. Markup.properties (Position.entity_properties_of def id pos)
  1168. (Markup.entity Markup.theoryN name);
  1169. Markup.theoryN : string;
  1170. serial(); (* A global, lock-guarded seriel counter used to produce unique identifiers,
  1171. be it on the level of thy-internal states or as reference in markup in
  1172. PIDE *)
  1173. (* From Theory:
  1174. fun check ctxt (name, pos) =
  1175. let
  1176. val thy = Proof_Context.theory_of ctxt;
  1177. val thy' =
  1178. Context.get_theory thy name
  1179. handle ERROR msg =>
  1180. let
  1181. val completion =
  1182. Completion.make (name, pos)
  1183. (fn completed =>
  1184. map Context.theory_name (ancestors_of thy)
  1185. |> filter completed
  1186. |> sort_strings
  1187. |> map (fn a => (a, (Markup.theoryN, a))));
  1188. val report = Markup.markup_report (Completion.reported_text completion);
  1189. in error (msg ^ Position.here pos ^ report) end;
  1190. val _ = Context_Position.report ctxt pos (get_markup thy');
  1191. in thy' end;
  1192. fun init_markup (name, pos) thy =
  1193. let
  1194. val id = serial ();
  1195. val _ = Position.report pos (theory_markup true name id pos);
  1196. in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
  1197. fun get_markup thy =
  1198. let val {pos, id, ...} = rep_theory thy
  1199. in theory_markup false (Context.theory_name thy) id pos end;
  1200. *)
  1201. (*
  1202. fun theory_markup def thy_name id pos =
  1203. if id = 0 then Markup.empty
  1204. else
  1205. Markup.properties (Position.entity_properties_of def id pos)
  1206. (Markup.entity Markup.theoryN thy_name);
  1207. fun get_markup thy =
  1208. let val {pos, id, ...} = rep_theory thy
  1209. in theory_markup false (Context.theory_name thy) id pos end;
  1210. fun init_markup (name, pos) thy =
  1211. let
  1212. val id = serial ();
  1213. val _ = Position.report pos (theory_markup true name id pos);
  1214. in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end;
  1215. fun check ctxt (name, pos) =
  1216. let
  1217. val thy = Proof_Context.theory_of ctxt;
  1218. val thy' =
  1219. Context.get_theory thy name
  1220. handle ERROR msg =>
  1221. let
  1222. val completion =
  1223. Completion.make (name, pos)
  1224. (fn completed =>
  1225. map Context.theory_name (ancestors_of thy)
  1226. |> filter completed
  1227. |> sort_strings
  1228. |> map (fn a => (a, (Markup.theoryN, a))));
  1229. val report = Markup.markup_report (Completion.reported_text completion);
  1230. in error (msg ^ Position.here pos ^ report) end;
  1231. val _ = Context_Position.report ctxt pos (get_markup thy');
  1232. in thy' end;
  1233. *)
  1234. \<close>
  1235. section \<open> Output: Very Low Level \<close>
  1236. ML\<open>
  1237. Output.output; (* output is the structure for the "hooks" with the target devices. *)
  1238. Output.output "bla_1:";
  1239. \<close>
  1240. section \<open> Output: LaTeX \<close>
  1241. ML\<open>
  1242. Thy_Output.verbatim_text;
  1243. Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
  1244. Thy_Output.antiquotation:
  1245. binding ->
  1246. 'a context_parser ->
  1247. ({context: Proof.context, source: Token.src, state: Toplevel.state} -> 'a -> string) ->
  1248. theory -> theory;
  1249. Thy_Output.output: Proof.context -> Pretty.T list -> string;
  1250. Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
  1251. Thy_Output.output : Proof.context -> Pretty.T list -> string;
  1252. \<close>
  1253. ML\<open>
  1254. Syntax_Phases.reports_of_scope;
  1255. \<close>
  1256. (* Pretty.T, pretty-operations. *)
  1257. ML\<open>
  1258. (* interesting piece for LaTeX Generation:
  1259. fun verbatim_text ctxt =
  1260. if Config.get ctxt display then
  1261. split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
  1262. Latex.output_ascii #> Latex.environment "isabellett"
  1263. else
  1264. split_lines #>
  1265. map (Latex.output_ascii #> enclose "\\isatt{" "}") #>
  1266. space_implode "\\isasep\\isanewline%\n";
  1267. (* From structure Thy_Output *)
  1268. fun pretty_const ctxt c =
  1269. let
  1270. val t = Const (c, Consts.type_scheme (Proof_Context.consts_of ctxt) c)
  1271. handle TYPE (msg, _, _) => error msg;
  1272. val ([t'], _) = Variable.import_terms true [t] ctxt;
  1273. in pretty_term ctxt t' end;
  1274. basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
  1275. *)
  1276. Pretty.enclose : string -> string -> Pretty.T list -> Pretty.T; (* not to confuse with: String.enclose *)
  1277. (* At times, checks where attached to Pretty - functions and exceptions used to
  1278. stop the execution/validation of a command *)
  1279. fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
  1280. Pretty.enclose;
  1281. Pretty.str;
  1282. Pretty.mark_str;
  1283. Pretty.text "bla_d";
  1284. Pretty.quote; (* Pretty.T transformation adding " " *)
  1285. Pretty.unformatted_string_of : Pretty.T -> string ;
  1286. Latex.output_ascii;
  1287. Latex.environment "isa" "bg";
  1288. Latex.output_ascii "a_b:c'é";
  1289. (* Note: *)
  1290. space_implode "sd &e sf dfg" ["qs","er","alpa"];
  1291. (*
  1292. fun pretty_command (cmd as (name, Command {comment, ...})) =
  1293. Pretty.block
  1294. (Pretty.marks_str
  1295. ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
  1296. command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
  1297. *)
  1298. \<close>
  1299. ML\<open>
  1300. Thy_Output.output_text;
  1301. (* is:
  1302. fun output_text state {markdown} source =
  1303. let
  1304. val is_reported =
  1305. (case try Toplevel.context_of state of
  1306. SOME ctxt => Context_Position.is_visible ctxt
  1307. | NONE => true);
  1308. val pos = Input.pos_of source;
  1309. val syms = Input.source_explode source;
  1310. val _ =
  1311. if is_reported then
  1312. Position.report pos (Markup.language_document (Input.is_delimited source))
  1313. else ();
  1314. val output_antiquotes = map (eval_antiquote state) #> implode;
  1315. fun output_line line =
  1316. (if Markdown.line_is_item line then "\\item " else "") ^
  1317. output_antiquotes (Markdown.line_content line);
  1318. fun output_blocks blocks = space_implode "\n\n" (map output_block blocks)
  1319. and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
  1320. | output_block (Markdown.List {kind, body, ...}) =
  1321. Latex.environment (Markdown.print_kind kind) (output_blocks body);
  1322. in
  1323. if Toplevel.is_skipped_proof state then ""
  1324. else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
  1325. then
  1326. let
  1327. val ants = Antiquote.parse pos syms;
  1328. val reports = Antiquote.antiq_reports ants;
  1329. val blocks = Markdown.read_antiquotes ants;
  1330. val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
  1331. in output_blocks blocks end
  1332. else
  1333. let
  1334. val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
  1335. val reports = Antiquote.antiq_reports ants;
  1336. val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
  1337. in output_antiquotes ants end
  1338. end;
  1339. *)
  1340. \<close>
  1341. ML\<open>
  1342. Outer_Syntax.print_commands @{theory};
  1343. Outer_Syntax.command : Outer_Syntax.command_keyword -> string ->
  1344. (Toplevel.transition -> Toplevel.transition) parser -> unit;
  1345. (* creates an implicit thy_setup with an entry for a call-back function, which happens
  1346. to be a parser that must have as side-effect a Toplevel-transition-transition.
  1347. Registers "Toplevel.transition -> Toplevel.transition" parsers to the Isar interpreter.
  1348. *)
  1349. (*Example: text is :
  1350. val _ =
  1351. Outer_Syntax.command ("text", @{here}) "formal comment (primary style)"
  1352. (Parse.opt_target -- Parse.document_source >> Thy_Output.document_command {markdown = true});
  1353. *)
  1354. (* not exported: Thy_Output.output_token; Ich glaub, da passierts ... *)
  1355. Thy_Output.present_thy;
  1356. \<close>
  1357. text\<open> Even the parsers and type checkers stemming from the theory-structure are registered via
  1358. hooks (this can be confusing at times). Main phases of inner syntax processing, with standard
  1359. implementations of parse/unparse operations were treated this way.
  1360. At the very very end in @{file "~~/src/Pure/Syntax/syntax_phases.ML"}, it sets up the entire syntax engine
  1361. (the hooks) via:
  1362. \<close>
  1363. (*
  1364. val _ =
  1365. Theory.setup
  1366. (Syntax.install_operations
  1367. {parse_sort = parse_sort,
  1368. parse_typ = parse_typ,
  1369. parse_term = parse_term false,
  1370. parse_prop = parse_term true,
  1371. unparse_sort = unparse_sort,
  1372. unparse_typ = unparse_typ,
  1373. unparse_term = unparse_term,
  1374. check_typs = check_typs,
  1375. check_terms = check_terms,
  1376. check_props = check_props,
  1377. uncheck_typs = uncheck_typs,
  1378. uncheck_terms = uncheck_terms});
  1379. *)
  1380. text\<open> Thus, Syntax\_Phases does the actual work, including
  1381. markup generation and generation of reports. Look at: \<close>
  1382. (*
  1383. fun check_typs ctxt raw_tys =
  1384. let
  1385. val (sorting_report, tys) = Proof_Context.prepare_sortsT ctxt raw_tys;
  1386. val _ = if Context_Position.is_visible ctxt then Output.report sorting_report else ();
  1387. in
  1388. tys
  1389. |> apply_typ_check ctxt
  1390. |> Term_Sharing.typs (Proof_Context.theory_of ctxt)
  1391. end;
  1392. which is the real implementation behind Syntax.check_typ
  1393. or:
  1394. fun check_terms ctxt raw_ts =
  1395. let
  1396. val (sorting_report, raw_ts') = Proof_Context.prepare_sorts ctxt raw_ts;
  1397. val (ts, ps) = Type_Infer_Context.prepare_positions ctxt raw_ts';
  1398. val tys = map (Logic.mk_type o snd) ps;
  1399. val (ts', tys') = ts @ tys
  1400. |> apply_term_check ctxt
  1401. |> chop (length ts);
  1402. val typing_report =
  1403. fold2 (fn (pos, _) => fn ty =>
  1404. if Position.is_reported pos then
  1405. cons (Position.reported_text pos Markup.typing
  1406. (Syntax.string_of_typ ctxt (Logic.dest_type ty)))
  1407. else I) ps tys' [];
  1408. val _ =
  1409. if Context_Position.is_visible ctxt then Output.report (sorting_report @ typing_report)
  1410. else ();
  1411. in Term_Sharing.terms (Proof_Context.theory_of ctxt) ts' end;
  1412. which is the real implementation behind Syntax.check_term
  1413. As one can see, check-routines internally generate the markup.
  1414. *)
  1415. section*[c::conclusion]\<open>Conclusion\<close>
  1416. text\<open>More to come\<close>
  1417. section*[bib::bibliography]\<open>Bibliography\<close>
  1418. (*<*)
  1419. close_monitor*[this]
  1420. check_doc_global
  1421. (*>*)
  1422. end