diff --git a/thys/Huffman/ROOT b/thys/Huffman/ROOT --- a/thys/Huffman/ROOT +++ b/thys/Huffman/ROOT @@ -1,117 +1,117 @@ chapter AFP session Huffman (AFP) = HOL + - options [timeout = 600] + options [timeout = 600, document_preprocessor = "preprocessor"] theories Huffman document_files - "build" "forest-a.eps" "forest-a.pdf" "forest-a.svg" "forest-flat.eps" "forest-flat.pdf" "forest-flat.svg" "forest-optimal.eps" "forest-optimal.pdf" "forest-optimal.svg" "forest-splitLeaf-ab.eps" "forest-splitLeaf-ab.pdf" "forest-splitLeaf-ab.svg" "forest-uniteTrees-flat.eps" "forest-uniteTrees-flat.pdf" "forest-uniteTrees-flat.svg" "forest-uniteTrees.eps" "forest-uniteTrees.pdf" "forest-uniteTrees.svg" "forest-zigzag.eps" "forest-zigzag.pdf" "forest-zigzag.svg" + "preprocessor" "root.tex" "tree-abc-full.eps" "tree-abc-full.pdf" "tree-abc-full.svg" "tree-abc-non-full.eps" "tree-abc-non-full.pdf" "tree-abc-non-full.svg" "tree-abcd-balanced-weighted.eps" "tree-abcd-balanced-weighted.pdf" "tree-abcd-balanced-weighted.svg" "tree-abcd-balanced.eps" "tree-abcd-balanced.pdf" "tree-abcd-balanced.svg" "tree-abcd-non-prefix.eps" "tree-abcd-non-prefix.pdf" "tree-abcd-non-prefix.svg" "tree-abcd-unbalanced-weighted.eps" "tree-abcd-unbalanced-weighted.pdf" "tree-abcd-unbalanced-weighted.svg" "tree-abcd-unbalanced.eps" "tree-abcd-unbalanced.pdf" "tree-abcd-unbalanced.svg" "tree-huffman-splitLeaf-ab.eps" "tree-huffman-splitLeaf-ab.pdf" "tree-huffman-splitLeaf-ab.svg" "tree-minima-abcd.eps" "tree-minima-abcd.pdf" "tree-minima-abcd.svg" "tree-minima.eps" "tree-minima.pdf" "tree-minima.svg" "tree-optimal.eps" "tree-optimal.pdf" "tree-optimal.svg" "tree-prime-step1.eps" "tree-prime-step1.pdf" "tree-prime-step1.svg" "tree-prime-step2.eps" "tree-prime-step2.pdf" "tree-prime-step2.svg" "tree-prime-step3.eps" "tree-prime-step3.pdf" "tree-prime-step3.svg" "tree-prime-step4.eps" "tree-prime-step4.pdf" "tree-prime-step4.svg" "tree-prime-step5.eps" "tree-prime-step5.pdf" "tree-prime-step5.svg" "tree-sibling.eps" "tree-sibling.pdf" "tree-sibling.svg" "tree-splitLeaf-a.eps" "tree-splitLeaf-a.pdf" "tree-splitLeaf-a.svg" "tree-splitLeaf-ab.eps" "tree-splitLeaf-ab.pdf" "tree-splitLeaf-ab.svg" "tree-splitLeaf-abcd-aba.eps" "tree-splitLeaf-abcd-aba.pdf" "tree-splitLeaf-abcd-aba.svg" "tree-splitLeaf-abcd.eps" "tree-splitLeaf-abcd.pdf" "tree-splitLeaf-abcd.svg" "tree-splitLeaf-ba.eps" "tree-splitLeaf-ba.pdf" "tree-splitLeaf-ba.svg" "tree-splitLeaf-cd.eps" "tree-splitLeaf-cd.pdf" "tree-splitLeaf-cd.svg" "tree-suboptimal.eps" "tree-suboptimal.pdf" "tree-suboptimal.svg" "tree-w1-plus-w2.eps" "tree-w1-plus-w2.pdf" "tree-w1-plus-w2.svg" "tree-w1-w2-leaves.eps" "tree-w1-w2-leaves.pdf" "tree-w1-w2-leaves.svg" "tree-w1-w2.eps" "tree-w1-w2.pdf" "tree-w1-w2.svg" "tree-w1.eps" "tree-w1.pdf" "tree-w1.svg" "tree-w2.eps" "tree-w2.pdf" "tree-w2.svg" diff --git a/thys/Huffman/document/build b/thys/Huffman/document/preprocessor rename from thys/Huffman/document/build rename to thys/Huffman/document/preprocessor --- a/thys/Huffman/document/build +++ b/thys/Huffman/document/preprocessor @@ -1,37 +1,29 @@ -#!/bin/bash +#!/usr/bin/env bash set -e -FMT="$1" -VARIANT="$2" - export HUFFMAN_TEX=Huffman.tex -perl -pi -i.bak -e 's/\{\\isacharprime\}a/\$\\alpha\$/g' $HUFFMAN_TEX -perl -pi -i.bak -e 's/\{\\isacharprime\}b/\$\\beta\$/g' $HUFFMAN_TEX -perl -pi -i.bak -e 's/\{\\isacharbraceleft\}\{\\isacharbraceright\}/\{\\ensuremath\{\\emptyset\}\}/g' $HUFFMAN_TEX -perl -pi -i.bak -e 's/\{\\isacharunderscore\}\{\\isadigit\{([0-9])\}\}/\{\\isacharunderscore\}\{\1\}/g' $HUFFMAN_TEX +perl -pi -i.bak -e 's/\{\\isacharprime\}\{\\kern0pt\}a/\$\\alpha\$/g' $HUFFMAN_TEX +perl -pi -i.bak -e 's/\{\\isacharprime\}\{\\kern0pt\}b/\$\\beta\$/g' $HUFFMAN_TEX +perl -pi -i.bak -e 's/\{\\isacharbraceleft\}\{\\kern0pt\}\{\\isacharbraceright\}\{\\kern0pt\}/\{\\ensuremath\{\\emptyset\}\}/g' $HUFFMAN_TEX +perl -pi -i.bak -e 's/\{\\isacharunderscore\}\{\\kern0pt\}\{\\isadigit\{([0-9])\}\}/\{\\isacharunderscore\}\{\1\}/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/([a-z]|\{\\isacharparenright\})\{\\isacharplus\}/\1\$\{\}^+\$/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\b(if|then|else(\\ if)?)\\( |isanewline)/\\ensuremath\{\\mathrm\{\1\}\}\\vthinspace\\\3/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\\isactrlisub F/\\isactrlisub\{\\ensuremath\{\\mathsf\{\\scriptscriptstyle F\}\}\}/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/mergeSibling/merge\\-Sibling/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/swapFourSyms/swap\\-Four\\-Syms/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\{\\isasymSum\}(.*)\\ \{\\isasymin\}\\ (.*)\{\\isachardot\}/\\ensuremath\{\\sum_\{\1\\in\2\}\}/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\\sum(.*)\\ \{\\isasymunion\}\\ /\\sum\1\\isasymunion/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\\isacommand\{by\}/\\nopagebreak\\isacommand\{by\}/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/(\{assumes\})\\ /\1\\ \\ /g' $HUFFMAN_TEX perl -pi -i.bak -e 's/(\{shows\})\\ /\1\\ \\ /g' $HUFFMAN_TEX perl -pi -i.bak -e 's/(\\isachardoublequoteclose\})\\ (\{\\isachardoublequoteopen\})/\1\\ \\ \\,\2/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/(\{\\isacharparenright\}\{\\isachardoublequoteclose\}\\ )\\ \\,(\{\\isachardoublequoteopen\}\{\\isacharparenleft\})/\1\2/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\\isactrlisub u\\isactrlisub *\{\\isacharprime\}/\\isactrlisub\{u\\isacharprime\}/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\\isanewline$/%\ \\isanewline/' $HUFFMAN_TEX sed '/\\isanewline$/,// s/^\(\(\\ \)*\)/\1\1/' $HUFFMAN_TEX > $HUFFMAN_TEX.bak mv $HUFFMAN_TEX.bak $HUFFMAN_TEX perl -pi -i.bak -e 's/\{\\isacharcolon\}%/\{\\isacharcolon\}\\nopagebreak%/g' $HUFFMAN_TEX perl -pi -i.bak -e 's/\\isakeyword\{where\}/\\isakeyword\{where\}\\nopagebreak/' $HUFFMAN_TEX perl -pi -i.bak -e 's/(\{\\isacharbrackleft\})(\{\\isacharbrackright\})/\1\\vthinspace\2/g' $HUFFMAN_TEX - -"$ISABELLE_TOOL" latex -o sty -"$ISABELLE_TOOL" latex -o "$FMT" -"$ISABELLE_TOOL" latex -o "$FMT" - diff --git a/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy b/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy --- a/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy +++ b/thys/Isabelle_C/C11-FrontEnd/C_Appendices.thy @@ -1,842 +1,842 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) chapter \Annexes\ theory C_Appendices imports "examples/C1" Isar_Ref.Base begin (*<*) ML \ \\<^file>\~~/src/Doc/antiquote_setup.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Doc/antiquote_setup.ML Author: Makarius Auxiliary antiquotations for the Isabelle manuals. *) \ structure C_Antiquote_Setup = struct (* misc utils *) fun translate f = Symbol.explode #> map f #> implode; val clean_string = translate (fn "_" => "\\_" | "#" => "\\#" | "$" => "\\$" | "%" => "\\%" | "<" => "$<$" | ">" => "$>$" | "{" => "\\{" | "|" => "$\\mid$" | "}" => "\\}" | "\" => "-" | c => c); fun clean_name "\" = "dots" | clean_name ".." = "ddot" | clean_name "." = "dot" | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | "#" => "symbol-hash" | "\" => "symbol-lower-approx" | "\" => "symbol-upper-down" | c => c); (* Isabelle/Isar entities (with index) *) local val arg = enclose "{" "}" o clean_string; fun entity check markup binding index = - Thy_Output.antiquotation_raw + Document_Output.antiquotation_raw (binding |> Binding.map_name (fn name => name ^ (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) (fn ctxt => fn (logic, (name, pos)) => let val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; val hyper = enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; val idx = (case index of NONE => "" | SOME is_def => "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); val _ = if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); val latex = idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |> hyper o enclose "\\mbox{\\isa{" "}}"); in Latex.string latex end); fun entity_antiqs check markup kind = entity check markup kind NONE #> entity check markup kind (SOME true) #> entity check markup kind (SOME false); in val _ = Theory.setup (entity_antiqs C_Annotation.check_command "isacommand" \<^binding>\annotation\); end; end; \ (*>*) section \Syntax Commands for Isabelle/C\ subsection \Outer Classical Commands\ text \ \begin{matharray}{rcl} @{command_def "C_file"} & : & \local_theory \ local_theory\ \\ @{command_def "C"} & : & \local_theory \ local_theory\ \\ @{command_def "C_export_boot"} & : & \local_theory \ local_theory\ \\ @{command_def "C_prf"} & : & \proof \ proof\ \\ @{command_def "C_val"} & : & \any \\ \\ @{command_def "C_export_file"} & : & \any \\ \\ \end{matharray} \begin{tabular}{rcll} @{attribute_def C_lexer_trace} & : & \attribute\ & default \false\ \\ @{attribute_def C_parser_trace} & : & \attribute\ & default \false\ \\ @{attribute_def C_ML_verbose} & : & \attribute\ & default \true\ \\ @{attribute_def C_starting_env} & : & \attribute\ & default \empty\ \\ @{attribute_def C_starting_rule} & : & \attribute\ & default \translation_unit\ \\ \end{tabular} \<^rail>\ @@{command C_file} @{syntax name} ';'? ; (@@{command C} | @@{command C_export_boot} | @@{command C_prf} | @@{command C_val}) @{syntax text} ; @@{command C_export_file} ; \ \<^descr> \<^theory_text>\C_file name\ reads the given C file, and let any attached semantic back-ends to proceed for further subsequent evaluation. Top-level C bindings are stored within the (global or local) theory context; the initial environment is set by default to be an empty one, or the one returned by a previous \<^theory_text>\C_file\ (depending on @{attribute_def C_starting_env}). The entry-point of the grammar taken as initial starting parser is read from @{attribute_def C_starting_rule} (see \<^url>\https://www.haskell.org/happy/doc/html/sec-directives.html#sec-parser-name\). Multiple \<^theory_text>\C_file\ commands may be used to build larger C projects if they are all written in a single theory file (existing parent theories are ignored, and not affecting the current working theory). \<^descr> \<^theory_text>\C\ is similar to \<^theory_text>\C_file\, but evaluates directly the given \text\. Top-level resulting bindings are stored within the (global or local) theory context. \<^descr> \<^theory_text>\C_export_boot\ is similar to \<^theory_text>\ML_export\, except that the code in input is understood as being processed by \<^theory_text>\C\ instead of \<^theory_text>\ML\. \<^descr> \<^theory_text>\C_prf\ is similar to \<^theory_text>\ML_prf\, except that the code in input is understood as being processed by \<^theory_text>\C\ instead of \<^theory_text>\ML\. \<^descr> \<^theory_text>\C_val\ is similar to \<^theory_text>\ML_val\, except that the code in input is understood as being processed by \<^theory_text>\C\ instead of \<^theory_text>\ML\. \<^descr> \<^theory_text>\C_export_file\ is similar to \<^theory_text>\generate_file fic = \code\ export_generated_files fic\, except that \<^item> \code\ refers to the dump of all existing previous C code in the current theory (parent theories are ignored), \<^item> and any ML antiquotations in \code\ are not analyzed by \<^theory_text>\generate_file\ (in contrast with its default behavior). \ text \ \<^descr> @{attribute C_lexer_trace} indicates whether the list of C tokens associated to the source text should be output (that list is computed during the lexing phase). \<^descr> @{attribute C_parser_trace} indicates whether the stack forest of Shift-Reduce node should be output (it is the final stack which is printed, i.e., the one taken as soon as the parsing terminates). \<^descr> @{attribute C_ML_verbose} indicates whether nested \<^theory_text>\ML\ commands are acting similarly as their default verbose configuration in top-level. \<^descr> @{attribute C_starting_env} makes the start of a C command (e.g., \<^theory_text>\C_file\, \<^theory_text>\C\) initialized with the environment of the previous C command if existing. \<^descr> @{attribute C_starting_rule} sets which parsing function will be used to parse the next C commands (e.g., \<^theory_text>\C_file\, \<^theory_text>\C\). \ subsection \Inner Annotation Commands\ text \ \<^rail>\ (@@{annotation "#ML_file"} | @@{annotation ML_file} | @@{annotation "ML_file\"} | @@{annotation "#C_file"} | @@{annotation C_file} | @@{annotation "C_file\"}) @{syntax name} ';'? ; (@@{annotation "#ML"} | @@{annotation ML} | @@{annotation "ML\"} | @@{annotation "#setup"} | @@{annotation setup} | @@{annotation "setup\"} | @@{annotation "\setup"} | @@{annotation "\setup\"} | @@{annotation "#C"} | @@{annotation C} | @@{annotation "C\"} | @@{annotation "#C_export_boot"} | @@{annotation C_export_boot} | @@{annotation "C_export_boot\"}) @{syntax text} ; (@@{annotation "#C_export_file"} | @@{annotation C_export_file} | @@{annotation "C_export_file\"} | @@{annotation highlight} | @@{annotation "highlight\"}) ; \ \<^descr> \<^C_theory_text>\ML_file\, \<^C_theory_text>\C_file\, \<^C_theory_text>\ML\, \<^C_theory_text>\setup\, \<^C_theory_text>\C\, \<^C_theory_text>\C_export_boot\, and \<^C_theory_text>\C_export_file\ behave similarly as the respective outer commands \<^theory_text>\ML_file\, \<^theory_text>\C_file\, \<^theory_text>\ML\, \<^theory_text>\setup\, \<^theory_text>\C\, \<^theory_text>\C_export_boot\, \<^theory_text>\C_export_file\. \<^descr> \<^C_theory_text>\\setup \f'\\ has the same semantics as \<^C_theory_text>\setup \f\\ whenever \<^term>\\ stack top env. f' stack top env = f\. In particular, depending on where the annotation \<^C_theory_text>\\setup \f'\\ is located in the C code, the additional values \stack\, \top\ and \env\ can drastically vary, and then can be possibly used in the body of \f'\ for implementing new interactive features (e.g., in contrast to \f\, which by default does not have the possibility to directly use the information provided by \stack\, \top\ and \env\). \<^descr> \<^C_theory_text>\highlight\ changes the background color of the C tokens pointed by the command. \<^descr> \<^C_theory_text>\#ML_file\, \<^C_theory_text>\#C_file\, \<^C_theory_text>\#ML\, \<^C_theory_text>\#setup\, \<^C_theory_text>\#C\, \<^C_theory_text>\#C_export_boot\, and \<^C_theory_text>\#C_export_file\ behave similarly as the respective (above inner) commands \<^C_theory_text>\ML_file\, \<^C_theory_text>\C_file\, \<^C_theory_text>\ML\, \<^C_theory_text>\setup\, \<^C_theory_text>\C\, \<^C_theory_text>\C_export_boot\, and \<^C_theory_text>\C_export_file\ except that their evaluations happen as earliest as possible. \<^descr> \<^C_theory_text>\ML_file\\, \<^C_theory_text>\C_file\\, \<^C_theory_text>\ML\\, \<^C_theory_text>\setup\\, \<^C_theory_text>\\setup\\, \<^C_theory_text>\C\\, \<^C_theory_text>\C_export_boot\\, \<^C_theory_text>\C_export_file\\, and \<^C_theory_text>\highlight\\ behave similarly as the respective (above inner) commands \<^C_theory_text>\ML_file\, \<^C_theory_text>\C_file\, \<^C_theory_text>\ML\, \<^C_theory_text>\setup\, \<^C_theory_text>\\setup\, \<^C_theory_text>\C\, \<^C_theory_text>\C_export_boot\, \<^C_theory_text>\C_export_file\, and \<^C_theory_text>\highlight\ except that their evaluations happen as latest as possible. \ subsection \Inner Directive Commands\ text \ \<^descr> Among the directives provided as predefined in Isabelle/C, we currently have: \<^C>\#define _\ and \<^C>\#undef _\. In particular, for the case of \<^C>\#define _\, rewrites are restricted to variable-form macros: support of functional macros is not yet provided. \<^descr> In Isabelle/C, not-yet-defined directives (such as \<^C>\#include _\ or \<^C>\#if #endif\, etc.) do not make the parsing fail, but are treated as ``free variable commands''. \ section \Quick Start (for People More Familiar with C than Isabelle)\ text \ \<^item> Assuming we are working with Isabelle 2019 \<^url>\http://isabelle.in.tum.de/dist/Isabelle2019_app.tar.gz\, the shortest way to start programming in C is to open a new theory file with the shell-command: \<^verbatim>\$ISABELLE_HOME/bin/isabelle jedit -d $AFP_HOME/thys Scratch.thy\ where \<^verbatim>\$ISABELLE_HOME\ is the path of the above extracted Isabelle source, and \<^verbatim>\$AFP_HOME\ is the downloaded content of \<^url>\https://bitbucket.org/isa-afp/afp-2019\.\<^footnote>\This folder particularly contains the Isabelle/C project, located in \<^url>\https://bitbucket.org/isa-afp/afp-2019/src/default/thys/Isabelle_C\. To inspect the latest developper version, one can also replace \<^verbatim>\$AFP_HOME/thys\ by the content downloaded from \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c\.\ \<^item> The next step is to copy this minimal content inside the newly opened window: \<^verbatim>\theory Scratch imports Isabelle_C.C_Main begin C \ // C code \ end\ \<^item> \<^emph>\Quod Erat Demonstrandum!\ This already enables the support of C code inside the special brackets ``\<^verbatim>\\\\'', now depicted as ``\\\\'' for readability reasons. \ text_raw \ \begin{figure} \centering \includegraphics[width=\textwidth]{figures/C-export-example} \caption{Making the File Browser Pointing to the Virtual File System} \label{fig:file-bro} \end{figure} \ text \ Additionally, Isabelle/C comes with several functionalities that can be alternatively explored: \<^item> To write theorems and proofs along with C code, the special C comment \<^C>\/*@ (* Isabelle content *) */\ can be used at any position where C comments are usually regularly allowed. At the time of writing, not yet all Isabelle commands can be written in C comments, and certain proof-solving-command combinations are also not yet implemented --- manual registration of commands to retrieve some more or less native user-experience remains possible though. Generally, the kind of content one can write in C comments should be arbitrary. The exhaustive list of Isabelle commands is provided in the accompanying above archive, for example in \<^dir>\$ISABELLE_HOME/src/Doc/Isar_Ref\ or \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\. \<^item> Instead of starting from scratch, any existing C files can also be opened with Isabelle/C, it suffices to replace: \begin{tabular}{c} \<^verbatim>\C\ \<^theory_text>\\ /* C */ \\ \\ by \\ \<^verbatim>\C_file\ \<^theory_text>\\~/file.c\\ \end{tabular} Once done, one can press a CTRL-like key while hovering the mouse over the file name, then followed by a click on it to open a new window loading that file. \<^item> After a \<^verbatim>\C\ \<^theory_text>\\ /* C */ \\ command, one has either the possibility to keep the content as such in the theory file, or use \<^verbatim>\C_export_file\ to export all previous C content into a ``real'' C file. Note that since Isabelle2019, Isabelle/C uses a virtual file-system. This has the consequence, that some extra operations are needed to export a file generated into the virtual file-system of Isabelle into the ``real'' file-system. First, the \<^verbatim>\C_export_file\ command needs to be activated, by putting the cursor on the command. This leads to the following message in the output window: \<^verbatim>\See theory exports "C/*/*.c"\ (see \autoref{fig:file-bro}). By clicking on \theory exports\ in this message, Isabelle opens a \File Browser\ showing the content of the virtual file-system in the left window. Selecting and opening a generated file in the latter lets jEdit display it in a new buffer, which gives the possibility to export this file via ``\File \ Save As\\'' into the real file-system. \ section \Case Study: Mapping on the Parsed AST\ text \ In this section, we give a concrete example of a situation where one is interested to do some automated transformations on the parsed AST, such as changing the type of every encountered variables from \<^C>\int _;\ to \<^C>\int _ [];\. The main theory of interest here is \<^theory>\Isabelle_C.C_Parser_Language\, where the C grammar is loaded, in contrast to \<^theory>\Isabelle_C.C_Lexer_Language\ which is only dedicated to build a list of C tokens. As another example, \<^theory>\Isabelle_C.C_Parser_Language\ also contains the portion of the code implementing the report to the user of various characteristics of encountered variables during parsing: if a variable is bound or free, or if the declaration of a variable is made in the global topmost space or locally declared in a function. \ subsection \Prerequisites\ text \ Even if \<^file>\generated/c_grammar_fun.grm.sig\ and \<^file>\generated/c_grammar_fun.grm.sml\ are files written in ML syntax, we have actually modified \<^dir>\../src_ext/mlton/lib/mlyacc-lib\ in such a way that at run time, the overall loading and execution of \<^theory>\Isabelle_C.C_Parser_Language\ will mimic all necessary features of the Haskell parser generator Happy \<^footnote>\\<^url>\https://www.haskell.org/happy/doc/html/index.html\\, including any monadic interactions between the lexing (\<^theory>\Isabelle_C.C_Lexer_Language\) and parsing part (\<^theory>\Isabelle_C.C_Parser_Language\). This is why in the remaining part, we will at least assume a mandatory familiarity with Happy (e.g., the reading of ML-Yacc's manual can happen later if wished \<^footnote>\\<^url>\https://www.cs.princeton.edu/~appel/modern/ml/ml-yacc/manual.html\\). In particular, we will use the term \<^emph>\rule code\ to designate \<^emph>\a Haskell expression enclosed in braces\ \<^footnote>\\<^url>\https://www.haskell.org/happy/doc/html/sec-grammar.html\\. \ subsection \Structure of \<^theory>\Isabelle_C.C_Parser_Language\\ text \ In more detail, \<^theory>\Isabelle_C.C_Parser_Language\ can be seen as being principally divided into two parts: \<^item> a first part containing the implementation of \<^ML_structure>\C_Grammar_Rule_Lib\, which provides the ML implementation library used by any rule code written in the C grammar \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (\<^file>\generated/c_grammar_fun.grm.sml\). \<^item> a second part implementing \<^ML_structure>\C_Grammar_Rule_Wrap\, providing one wrapping function for each rule code, for potentially complementing the rule code with an additional action to be executed after its call. The use of wrapping functions is very optional: by default, they are all assigned as identity functions. The difference between \<^ML_structure>\C_Grammar_Rule_Lib\ and \<^ML_structure>\C_Grammar_Rule_Wrap\ relies in how often functions in the two structures are called: while building subtree pieces of the final AST, grammar rules are free to call any functions in \<^ML_structure>\C_Grammar_Rule_Lib\ for completing their respective tasks, but also free to not use \<^ML_structure>\C_Grammar_Rule_Lib\ at all. On the other hand, irrespective of the actions done by a rule code, the function associated to the rule code in \<^ML_structure>\C_Grammar_Rule_Wrap\ is retrieved and always executed (but a visible side-effect will likely mostly happen whenever one has provided an implementation far different from \<^ML>\I\). \ text \ Because the grammar \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (\<^file>\generated/c_grammar_fun.grm.sml\) has been defined in such a way that computation of variable scopes are completely handled by functions in \<^ML_structure>\C_Grammar_Rule_Lib\ and not in rule code (which are just calling functions in \<^ML_structure>\C_Grammar_Rule_Lib\), it is enough to overload functions in \<^ML_structure>\C_Grammar_Rule_Lib\ whenever it is wished to perform new actions depending on variable scopes, for example to do a specific PIDE report at the first time when a C variable is being declared. In particular, functions in \<^ML_structure>\C_Grammar_Rule_Lib\ are implemented in monadic style, making a subsequent modification on the parsing environment \<^theory>\Isabelle_C.C_Environment\ possible (whenever appropriate) as this last is carried in the monadic state. Fundamentally, this is feasible because the monadic environment fulfills the property of being always properly enriched with declared variable information at any time, because we assume \<^item> working with a language where a used variable must be at most declared or redeclared somewhere before its actual usage, \<^item> and using a parser scanning tokens uniquely, from left to right, in the same order as the execution of rule code actions. \ subsubsection \Example\ text \ As illustration, \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Left\ is (implicitly) called by a rule code while a variable being declared is encountered. Later, a call to \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Right\ in \<^ML_structure>\C_Grammar_Rule_Wrap\ (actually, in \<^ML_structure>\C_Grammar_Rule_Wrap_Overloading\) is made after the execution of another rule code to signal the position of a variable in use, together with the information retrieved from the environment of the position of where it is declared. \ text \ In more detail, the second argument of \<^ML>\C_Grammar_Rule_Lib.markup_var\ is among other of the form: \<^ML_type>\Position.T * {global: bool}\, where particularly the field \<^ML>\#global : C_Env.markup_ident -> bool\ of the record is informing \<^ML>\C_Grammar_Rule_Lib.markup_var\ if the variable being reported (at either first declaration time, or first use time) is global or local (inside a function for instance). Because once declared, the property \<^ML>\#global : C_Env.markup_ident -> bool\ of a variable does not change afterwards, it is enough to store that information in the monadic environment: \<^item> \<^bold>\Storing the information at declaration time\ The part deciding if a variable being declared is global or not is implemented in \<^ML>\C_Grammar_Rule_Lib.doDeclIdent\ and \<^ML>\C_Grammar_Rule_Lib.doFuncParamDeclIdent\. The two functions come from \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (so do any functions in \<^ML_structure>\C_Grammar_Rule_Lib\). Ultimately, they are both calling \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Left\ at some point. \<^item> \<^bold>\Retrieving the information at use time\ \<^ML>\C_Grammar_Rule_Lib.markup_var o C_Ast.Right\ is only called by \<^ML>\C_Grammar_Rule_Wrap.primary_expression1\, while treating a variable being already declared. In particular the second argument of \<^ML>\C_Grammar_Rule_Lib.markup_var\ is just provided by what has been computed by the above point when the variable was declared (e.g., the globality versus locality information). \ subsection \Rewriting of AST node\ text \ For the case of rewriting a specific AST node, from subtree \T1\ to subtree \T2\, it is useful to zoom on the different parsing evaluation stages, as well as make precise when the evaluation of semantic back-ends are starting. \<^enum> Whereas annotations in Isabelle/C code have the potential of carrying arbitrary ML code (as in \<^theory>\Isabelle_C.C1\), the moment when they are effectively evaluated will not be discussed here, because to closely follow the semantics of the language in embedding (so C), we suppose comments --- comprising annotations --- may not affect any parsed tokens living outside comments. So no matter when annotations are scheduled to be future evaluated in Isabelle/C, the design decision of Isabelle/C is to not let a code do directive-like side-effects in annotations, such as changing \T1\ to \T2\ inside annotations. \<^enum> To our knowledge, the sole category of code having the capacity to affect incoming stream of tokens are directives, which are processed and evaluated before the ``major'' parsing step occurs. Since in Isabelle/C, directives are relying on ML code, changing an AST node from \T1\ to \T2\ can then be perfectly implemented in directives. \<^enum> After the directive (pre)processing step, the main parsing happens. But since what are driving the parsing engine are principally rule code, this step means to execute \<^ML_structure>\C_Grammar_Rule_Lib\ and \<^ML_structure>\C_Grammar_Rule_Wrap\, i.e., rules in \<^file>\generated/c_grammar_fun.grm.sml\. \<^enum> Once the parsing finishes, we have a final AST value, which topmost root type entry-point constitutes the last node built before the grammar parser \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ ever entered in a stop state. For the case of a stop acceptance state, that moment happens when we reach the first rule code building the type \<^ML_type>\C_Ast.CTranslUnit\, since there is only one possible node making the parsing stop, according to what is currently written in the C grammar. (For the case of a state stopped due to an error, it is the last successfully built value that is returned, but to simplify the discussion, we will assume in the rest of the document the parser is taking in input a fully well-parsed C code.) \<^enum> By \<^emph>\semantic back-ends\, we denote any kind of ``relatively efficient'' compiled code generating Isabelle/HOL theorems, proofs, definitions, and so with the potential of generally generating Isabelle packages. In our case, the input of semantic back-ends will be the type \<^ML_type>\C_Ast.CTranslUnit\ (actually, whatever value provided by the above parser). But since our parser is written in monadic style, it is as well possible to give slightly more information to semantic back-ends, such as the last monadic computed state, so including the last state of the parsing environment. \ text \ Generally, semantic back-ends can be written in full ML starting from \<^ML_type>\C_Ast.CTranslUnit\, but to additionally support formalizing tasks requiring to start from an AST defined in Isabelle/HOL, we provide an equivalent AST in HOL in the project, such as the one obtained after loading \<^url>\https://gitlri.lri.fr/ftuong/citadelle-devel/blob/master/doc/Meta_C_generated.thy\. (In fact, the ML AST is just generated from the HOL one.) \ text \ Based on the above information, there are now several \<^emph>\equivalent\ ways to proceed for the purpose of having an AST node be mapped from \T1\ to \T2\. The next bullets providing several possible solutions to follow are particularly sorted in increasing action time. \<^item> \<^emph>\Before even starting the Isabelle system.\ A first approach would be to modify the C code in input, by adding a directive \<^C>\#define _ _\ performing the necessary rewrite. \<^item> \<^emph>\Before even starting the Isabelle system.\ As an alternative of changing the C code, one can modify \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ by hand, by explicitly writing \T2\ at the specific position of the rule code generating \T1\. However, this solution implies to re-generate \<^file>\generated/c_grammar_fun.grm.sml\. \<^item> \<^emph>\At grammar loading time, while the source of Isabelle/C is still being processed.\ Instead of modifying the grammar, it should be possible to first locate which rule code is building \T1\. Then it would remain to retrieve and modify the respective function of \<^ML_structure>\C_Grammar_Rule_Wrap\ executed after that rule code, by providing a replacement function to be put in \<^ML_structure>\C_Grammar_Rule_Wrap_Overloading\. However, as a design decision, wrapping functions generated in \<^file>\generated/c_grammar_fun.grm.sml\ have only been generated to affect monadic states, not AST values. This is to prevent an erroneous replacement of an end-user while parsing C code. (It is currently left open about whether this feature will be implemented in future versions of the parser...) \<^item> \<^emph>\At directive setup time, before executing any \<^theory_text>\C\ command of interest.\ Since the behavior of directives can be dynamically modified, this solution amounts to change the semantics of any wished directive, appearing enough earlier in the code. (But for the overall code be in the end mostly compatible with any other C preprocessors, the implementation change has to be somehow at least consistent with how a preprocessor is already expected to treat an initial C un(pre)processed code.) For example, the current semantics of \<^C>\#undef _\ depends on what has been registered in \<^ML>\C_Context.directive_update\ (see \<^theory>\Isabelle_C.C_Command\). \<^item> \<^emph>\After parsing and obtaining a constructive value.\ Another solution consists in directly writing a mapping function acting on the full AST, so writing a ML function of type \<^ML_type>\C_Ast.CTranslUnit -> C_Ast.CTranslUnit\ (or a respective HOL function) which has to act on every constructor of the AST (so in the worst case about hundred of constructors for the considered AST, i.e., whenever a node has to be not identically returned). However, as we have already implemented a conversion function from \<^ML_type>\C_Ast.CTranslUnit\ (subset of C11) to a subset AST of C99, it might be useful to save some effort by starting from this conversion function, locate where \T1\ is pattern-matched by the conversion function, and generate \T2\ instead. As example, the conversion function \<^ML>\C_Ast.main\ is particularly used to connect the C11 front-end to the entry-point of AutoCorres in \<^verbatim>\l4v/src/tools/c-parser/StrictCParser.ML\. \<^item> \<^emph>\At semantic back-ends execution time.\ The above points were dealing with the cases where modification actions were all occurring before getting a final \<^ML_type>\C_Ast.CTranslUnit\ value. But this does not mean it is forbidden to make some slight adjustments once that resulting \<^ML_type>\C_Ast.CTranslUnit\ value obtained. In particular, it is the tasks of semantic back-ends to precisely work with \<^ML_type>\C_Ast.CTranslUnit\ as starting point, and possibly translate it to another different type. So letting a semantic back-end implement the mapping from \T1\ to \T2\ would mean here to first understand the back-end of interest's architecture, to see where the necessary minimal modifications must be made. By taking l4v as a back-end example, its integration with Isabelle/C first starts with translating \<^ML_type>\C_Ast.CTranslUnit\ to l4v's default C99 AST. Then various analyses on the obtained AST are performed in \<^url>\https://github.com/seL4/l4v/tree/master/tools/c-parser\ (the reader interested in the details can start by further exploring the ML files loaded by \<^url>\https://github.com/seL4/l4v/blob/master/tools/c-parser/CTranslation.thy\). In short, to implement the mapping from \T1\ to \T2\ in the back-end part, one can either: \<^item> modify the translation from \<^ML_type>\C_Ast.CTranslUnit\ to C99, \<^item> or modify the necessary ML files of interests in the l4v project. \ text \ More generally, to better inspect the list of rule code really executed when a C code is parsed, it might be helpful to proceed as in \<^theory>\Isabelle_C.C1\, by activating \<^theory_text>\declare[[C_parser_trace]]\. Then, the output window will display the sequence of Shift Reduce actions associated to the \<^theory_text>\C\ command of interest. \ section \Known Limitations, Troubleshooting\ subsection \The Document Model of the Isabelle/PIDE (applying for Isabelle 2019)\ subsubsection \Introduction\ text \ Embedding C directives in C code is an act of common practice in numerous applications, as well as largely highlighted in the C standard. As an example of frequently encountered directives, \#include \ is used to insert the content of \some_file.c\ at the place where it is written. In Isabelle/C, we can also write a C code containing directives like \#include\, and generally the PIDE reporting of directives is supported to a certain extent. Yet, the dynamic inclusion of arbitrary file with \#include\ is hurting a certain technological barrier. This is related to how the document model of Isabelle 2019 is functioning, but also to the design decisions behind the implementation of \<^theory_text>\C\ .. \\. Thus, providing a complete semantic implementation of \#include\ might be not as evident as usual, if not more dangerous, i.e. ``something requiring a manual intervention in the source of Isabelle 2019''. In the next part, we show why in our current implementation of Isabelle/C there is no way for user programmed extensions to exploit implicit dependencies between sub-documents in pure ML: a sub-document referred to via \#include \ will not lead to a reevaluation of a \<^theory_text>\C\ .. \\ command whenever modified.\ subsubsection \Embedding a language in Isabelle/PIDE\ text \ To clarify why the way a language being embedded in Isabelle is influencing the interaction between a future parser of the language with the Isabelle's document model, we recall the two ``different'' ways of embedding a language in Isabelle/PIDE. At its most basic form, the general syntactic scope of an Isabelle/Isar document can be seen as being composed of two syntactic alternations of editing space: fragments of the inner syntax language, themselves part of the more general outer syntax (the inner syntax is implemented as an atomic entity of the outer language); see \<^file>\~~/src/Doc/Isar_Ref/Outer_Syntax.thy\. So strictly speaking, when attempting to support a new language \L\ in Isabelle, there is always the question of fine-grain estimating which subsets of \L\ will be represented in the outer syntax part, and if it possibly remains any left subsets to be represented on the more inner (syntactic) part. Generally, to answer this question, there are several criteria to consider: \<^item> Are there any escaping symbols conflicting between \L\ and the outer (syntax) language, including for example the ASCII \<^verbatim>\"\ or \<^verbatim>\`\? \<^item> Is \L\ a realistic language, i.e. more complex than any combinations of outer named tokens that can be ever covered in terms of expressivity power (where the list of outer named tokens is provided in \<^file>\~~/src/Doc/Isar_Ref/Outer_Syntax.thy\)? \<^item> Is it preferable of not altering the outer syntax language with too specific and challenging features of \L\? This is particularly true since in Isabelle 2019, there is no way of modifying the outer syntax without making the modifications irremediably happen on its source code. For the above reasons, we have come up in Isabelle/C with the choice of making the full C language be supported inside the inner syntax allocated space. In particular, this has become all the more syntactically easy with the introduction of cartouches since Isabelle 2014.\<^footnote>\Fortunately, parsing tokens of C do not strongly conflict with cartouche delimiter symbols. For example, it should not be ethically wrong in C to write an opening cartouche symbol (possibly in a C comment) without writing any closing cartouche symbol afterwards. However, we have not encountered such C code in our tested codebase, and it is a functionality implicitly rejected by the current parser of Isabelle/C, as it is relying on Isabelle 2019's parser combinator library for the lexing part.\ However, for the case of the C language, certain C directives like \#include\ are meant to heavily interact with external files. In particular, resources would be best utilized if we were taking advantage of the Isabelle's asynchronous document model for such interaction task. Unfortunately, the inner syntax space only has a minimum interaction with the document model, compared to the outer syntax one. Otherwise said, be it for experimenting the inner syntax layer and see how far it can deal with the document layer, or otherwise reimplementing parts of Isabelle/C in the outer syntax layer, the two solutions are conducting to do modifications in the Isabelle 2019 source code. \ text \ Note that the language embedding space of \<^theory_text>\C\ closely resembles to how ML sources are delimited within a \<^theory_text>\ML\ command. Additionally, in ML, one can use antiquotations to also refer to external files (particularly in formal comments). Still, the problem is still present in ML: referred files are not loaded in the document model. \ subsubsection \Examples\ text \ \<^item> Commands declared as of type \thy_decl\ in the theory header are scheduled to be executed once. Additionally, they are not tracking the content of file names provided in argument, so a change there will not trigger a reevaluation of the associated command. For example, even if the type of \<^theory_text>\ML_file\ is not \thy_decl\, nothing prevents one to set it with \thy_decl\ as type. In particular, by doing so, it is no more possible to CTRL-hover-click on the file name written after \<^theory_text>\ML_file\. \<^item> To make a command \C\ track the content of \file\, whenever the file is changing, setting \C\ to be of type \thy_load\ in the theory header is a first step, but not enough. To be effective, \file\ must also be loaded, by either explicitly opening it, or clicking on its name after the command. Examples of commands in this situation requiring a preliminary one-time-click include: \<^theory_text>\external_file\, \<^theory_text>\bibtex_file\, \<^theory_text>\ML_file\. Internally, the click is bound to a Scala code invoking a request to make an asynchronous dependency to the newly opened document at ML side. \<^item> In terms of recursivity, for the case of a chain of sub-documents of the form (a theory file containing: \<^theory_text>\C_file \file0.c\\) \\\ (C file \<^verbatim>\file0.c\ containing: \<^C>\#include \) \\\ (C file \<^verbatim>\file1.c\ containing: \<^C>\#include \) \\\ (C file \<^verbatim>\file2.c\ containing: \<^C>\#include \), we ideally expect a modification in \<^verbatim>\file3.c\ be taken into account in all ancestor files including the initial theory, provoking the associated command of the theory be reevaluated. However in C, directives resolving might be close to Turing-complete. For instance, one can also include files based on particular conditional situations: \<^C>\#if _ #include #else #include #include #endif\ \<^item> When a theory is depending on other theories (such as \<^theory>\Isabelle_C.C_Eval\ depending on \<^theory>\Isabelle_C.C_Parser_Language\ and \<^theory>\Isabelle_C.C_Parser_Annotation\), modifying the list of theories in importation automatically triggers what the user is expecting: for example, the newly added theories are dynamically imported, any change by another external editor makes everything consequently propagated. Following the internal implementation of the document model engine, we basically distinguish two phases of document importation: either at start-up time, or dynamically on user requests. Although the case of start-up time can be handled in pure ML side, the language dedicated to express which Isabelle theory files to import is less powerful than the close-to-Turing-completeness expressivity of C directives. On the other hand, the dynamic importation of files on user requests seems to be performed (at the time of writing) through a too high level ML protocol, mostly called from Scala side. Due to the fact that Isabelle/C is currently implemented in pure ML, a solution also in pure ML would thus sound more natural (although we are not excluding solutions interacting with Scala, as long as the resulting can be implemented in Isabelle, preferably outside of its own source).\ subsection \Parsing Error versus Parsing Correctness\ text \ When trying to decide if the next parsing action is a Shift or Reduce action to perform, the grammar simulator \<^ML>\LALR_Parser_Eval.parse\ can actually decide to do another action: ignore everything and immediately stop the simulation. If the parser ever decides to stop, this can only be for two reasons: \<^item> The parser is supposed to have correctly finished its parsing task, making it be in an acceptance state. As acceptance states are encoded in the grammar, it is easy to find if this information is correct, or if it has to be adjusted in more detail by inspecting \<^url>\https://github.com/visq/language-c/blob/master/src/Language/C/Parser/Parser.y\ (\<^file>\generated/c_grammar_fun.grm.sml\). \<^item> The parser seems to be unable to correctly finish its parsing task. In this case, the user will see an error be explicitly raised by the prover IDE. However raising an error is just the default behavior of Isabelle/C: the decision to whether raise interruptive errors ultimately depends on how front-end commands are implemented (such as \<^theory_text>\C\, \<^theory_text>\C_file\, etc.). For instance, similarly as to how outer syntax commands are implemented, we can imagine a tool implementing a kind of partial parsing, analyzing the longest sequence of well-formed input, and discarding some strategic next set of faulty tokens with a well suited informative message, so that the parsing process could be maximally repeated on what is coming afterwards. Currently, the default behavior of Isabelle/C is to raise the error defined in \<^ML>\C_Module.err\ at the very first opportunity \<^footnote>\At the time of writing it is: \<^emph>\No matching grammar rule\.\. The possible solutions to make the error disappear at the position the error is indicated can be detailed as follows: \<^item> Modifying the C code in input would be a first solution whenever we suspect something is making it erroneous (and when we have a reason to believe that the grammar is behaving as it should). \<^item> However, we could still get the above error in front of an input where one is usually expecting to see not causing a failure. In particular, there are several C features (such as C directives) explicitly left for semantic back-ends (pre-) processing, so in general not fully semantically processed at parsing time. For example, whereas the code \<^C>\#define i int i a;\ succeeds, replacing its first line with the directive \<^C>\#include \ will not initially work, even if \file.c\ contains \<^C>\#define i int\, as the former directive has been left for semantic back-end treatment. One way of solving this would be to modify the C code in input for it to be already preprocessed (without directives, for example the C example of \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/TestSEL4.thy\ is already provided as preprocessed). Another way would be adding a specific new semantic back-end implementing the automation of the preprocessing task (as done in \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/blob/C/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_TEC.thy\, where the back-end explicitly makes a call to \cpp\ at run-time). \<^item> Ultimately, modifying the grammar with new rules cancelling the exception would only work if the problem really relies on the grammar, as it was mentioned for the acceptance state. \ text \ In terms of parsing correctness, Isabelle/C provides at least two different parsers: \<^item> a parser limited to C99/C11 code provided in \<^dir>\../C11-FrontEnd\ that can parse certain liberal extensions out of the C standard~\<^footnote>\\<^url>\http://hackage.haskell.org/package/language-c\\; \<^item> and another parser accepting C99/C11/C18 code in \<^url>\https://gitlri.lri.fr/ftuong/isabelle_c/tree/C/C18-FrontEnd\ that is close to the C standard while focusing on resolving ambiguities of the standard~\<^footnote>\\<^url>\https://github.com/jhjourdan/C11parser\\~\cite{DBLP:journals/toplas/JourdanP17}. \ text \ Note that the two parsers are not accepting/rejecting the same range of arbitrary C code. We have actually already encountered situations where an error is raised by one parser, while a success is happening with the other parser (and vice-versa). Consequently, in front of a C code, it can be a good recommendation to try out the parsing with all possible parsers of Isabelle/C. In any cases, a failure in one or several activated parsers might not be necessarily harmful: it might also indicate that a wrong parser has been selected, or a semantic back-end not yet supporting aspects of the C code being parsed. \ subsection \Exporting C Files to the File-System\ text \ From the Isabelle/C side, the task is easy, just type:\ C_export_file text \ ... which does the trick and generates a file \<^verbatim>\C_Appendices.c\. But hold on --- where is it? Well, Isabelle/C uses since version Isabelle2019 a virtual file-system. Exporting from it to the real file-system requires a few mouse-clicks (unfortunately). So activating the command \<^theory_text>\C_export_file\ leads to the output \<^verbatim>\See theory exports "C/*/C_Appendices.c"\ (see \autoref{fig:file-bro}), and clicking on the highlighted \<^verbatim>\theory exports\ lets Isabelle display a part of the virtual file-system (see subwidget left). Activating it in the subwidget lets jEdit open it as an editable file, which can be exported via ``\File \ Save As\\'' into the real file-system. \ end diff --git a/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy b/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy --- a/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy +++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Command.thy @@ -1,963 +1,963 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section \Interface: Inner and Outer Commands\ theory C_Command imports C_Eval keywords "C" :: thy_decl % "ML" and "C_file" :: thy_load % "ML" and "C_export_boot" :: thy_decl % "ML" and "C_export_file" :: thy_decl and "C_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "C_val" :: diag % "ML" begin subsection \Parsing Entry-Point: Error and Acceptance Cases\ ML \ \\<^file>\~~/src/Pure/Tools/ghc.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Tools/ghc.ML Author: Makarius Support for GHC: Glasgow Haskell Compiler. *) \ structure C_Serialize = struct (** string literals **) fun print_codepoint c = (case c of 10 => "\\n" | 9 => "\\t" | 11 => "\\v" | 8 => "\\b" | 13 => "\\r" | 12 => "\\f" | 7 => "\\a" | 27 => "\\e" | 92 => "\\\\" | 63 => "\\?" | 39 => "\\'" | 34 => "\\\"" | c => if c >= 32 andalso c < 127 then chr c else error "Not yet implemented"); fun print_symbol sym = (case Symbol.decode sym of Symbol.Char s => print_codepoint (ord s) | Symbol.UTF8 s => UTF8.decode_permissive s |> map print_codepoint |> implode | Symbol.Sym s => "\\092<" ^ s ^ ">" | Symbol.Control s => "\\092<^" ^ s ^ ">" | _ => translate_string (print_codepoint o ord) sym); val print_string = quote o implode o map print_symbol o Symbol.explode; end \ ML \ \\<^file>\~~/src/Pure/Tools/generated_files.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Tools/generated_files.ML Author: Makarius Generated source files for other languages: with antiquotations, without Isabelle symbols. *) \ structure C_Generated_Files = struct val c_dir = "C"; val c_ext = "c"; val c_make_comment = enclose "/*" "*/"; (** context data **) (* file types *) fun get_file_type ext = if ext = "" then error "Bad file extension" else if c_ext = ext then () else error ("Unknown file type for extension " ^ quote ext); (** Isar commands **) (* generate_file *) fun generate_file (binding, src_content) lthy = let val (path, pos) = Path.dest_binding binding; val () = get_file_type (#2 (Path.split_ext path)) handle ERROR msg => error (msg ^ Position.here pos); val header = c_make_comment " generated by Isabelle "; val content = header ^ "\n" ^ src_content; in lthy |> (Local_Theory.background_theory o Generated_Files.add_files) (binding, content) end; (** concrete file types **) val _ = Theory.setup (Generated_Files.file_type \<^binding>\C\ {ext = c_ext, make_comment = c_make_comment, make_string = C_Serialize.print_string}); end \ ML \ \\<^theory>\Isabelle_C.C_Eval\\ \ structure C_Module = struct structure Data_In_Source = Generic_Data (type T = Input.source list val empty = [] val extend = I val merge = K empty) structure Data_In_Env = Generic_Data (type T = C_Env.env_lang val empty = C_Env.empty_env_lang val extend = I val merge = K empty) structure Data_Accept = Generic_Data (type T = C_Grammar_Rule.start_happy -> C_Env.env_lang -> Context.generic -> Context.generic fun empty _ _ = I val extend = I val merge = #2) structure Data_Term = Generic_Data (type T = (C_Grammar_Rule.start_happy -> C_Env.env_lang -> local_theory -> term) Symtab.table val empty = Symtab.empty val extend = I val merge = #2) structure C_Term = struct val key_translation_unit = \translation_unit\ val key_external_declaration = \external_declaration\ val key_statement = \statement\ val key_expression = \expression\ val key_default = \default\ local val source_content = Input.source_content #> #1 in val key0_translation_unit = source_content key_translation_unit val key0_external_declaration = source_content key_external_declaration val key0_statement = source_content key_statement val key0_expression = source_content key_expression val key0_default = source_content key_default end val tok0_translation_unit = (key0_translation_unit, C_Grammar.Tokens.start_translation_unit) val tok0_external_declaration = ( key0_external_declaration , C_Grammar.Tokens.start_external_declaration) val tok0_statement = (key0_statement, C_Grammar.Tokens.start_statement) val tok0_expression = (key0_expression, C_Grammar.Tokens.start_expression) val tok_translation_unit = (key_translation_unit, C_Grammar.Tokens.start_translation_unit) val tok_external_declaration = ( key_external_declaration , C_Grammar.Tokens.start_external_declaration) val tok_statement = (key_statement, C_Grammar.Tokens.start_statement) val tok_expression = (key_expression, C_Grammar.Tokens.start_expression) val tokens = [ tok0_translation_unit , tok0_external_declaration , tok0_statement , tok0_expression ] local fun map_upd0 key v = Context.theory_map (Data_Term.map (Symtab.update (key, v))) fun map_upd key start f = map_upd0 key (f o the o start) in val map_translation_unit = map_upd key0_translation_unit C_Grammar_Rule.start_happy1 val map_external_declaration = map_upd key0_external_declaration C_Grammar_Rule.start_happy2 val map_statement = map_upd key0_statement C_Grammar_Rule.start_happy3 val map_expression = map_upd key0_expression C_Grammar_Rule.start_happy4 val map_default = map_upd0 key0_default end end fun env0 ctxt = case Config.get ctxt C_Options.starting_env of "last" => Data_In_Env.get (Context.Proof ctxt) | "empty" => C_Env.empty_env_lang | s => error ("Unknown option: " ^ s ^ Position.here (Config.pos_of C_Options.starting_env)) val env = env0 o Context.proof_of fun start source context = Input.range_of source |> let val s = Config.get (Context.proof_of context) C_Options.starting_rule in case AList.lookup (op =) C_Term.tokens s of SOME tok => tok | NONE => error ("Unknown option: " ^ s ^ Position.here (Config.pos_of C_Options.starting_rule)) end fun err0 _ _ pos = C_Env.map_error_lines (cons ("Parser: No matching grammar rule" ^ Position.here pos)) val err = pair () oooo err0 fun accept0 f env_lang ast = Data_In_Env.put env_lang #> (fn context => f context ast env_lang (Data_Accept.get context ast env_lang context)) fun accept env_lang (_, (ast, _, _)) = pair () o C_Env.map_context (accept0 (K (K (K I))) env_lang ast) val eval_source = C_Context.eval_source env start err accept fun c_enclose bg en source = C_Lex.@@ ( C_Lex.@@ (C_Lex.read bg, C_Lex.read_source source) , C_Lex.read en); structure C_Term' = struct val err = pair Term.dummy oooo err0 fun accept ctxt start_rule = let val (key, start) = case start_rule of NONE => (C_Term.key_default, start) | SOME (key, start_rule) => (key, fn source => fn _ => start_rule (Input.range_of source)) val (key, pos) = Input.source_content key in ( start , fn env_lang => fn (_, (ast, _, _)) => C_Env.map_context' (accept0 (fn context => pair oo (case Symtab.lookup (Data_Term.get context) key of NONE => tap (fn _ => warning ("Representation function associated to\ \ \"" ^ key ^ "\"" ^ Position.here pos ^ " not found (returning a dummy term)")) (fn _ => fn _ => @{term "()"}) | SOME f => fn ast => fn env_lang => f ast env_lang ctxt)) env_lang ast)) end fun eval_in text context env start_rule = let val (start, accept) = accept (Context.proof_of context) start_rule in C_Context.eval_in (SOME context) env (start text) err accept end fun parse_translation l = l |> map (apsnd (fn start_rule => fn ctxt => fn args => let val msg = (case start_rule of NONE => C_Term.key_default | SOME (key, _) => key) |> Input.source_content |> #1 fun err () = raise TERM (msg, args) in case args of [(c as Const (\<^syntax_const>\_constrain\, _)) $ Free (s, _) $ p] => (case Term_Position.decode_position p of SOME (pos, _) => c $ let val src = uncurry (Input.source false) let val s0 = Symbol_Pos.explode (s, pos) val s = Symbol_Pos.cartouche_content s0 in ( Symbol_Pos.implode s , case s of [] => Position.no_range | (_, pos0) :: _ => Position.range (pos0, s0 |> List.last |> snd)) end in eval_in src (case Context.get_generic_context () of NONE => Context.Proof ctxt | SOME context => Context.mapping I (K ctxt) context) (C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt | SOME (_, env_lang) => env_lang)) start_rule (c_enclose "" "" src) end $ p | NONE => err ()) | _ => err () end)) end fun eval_in text ctxt = C_Context.eval_in ctxt env (start text) err accept fun exec_eval source = Data_In_Source.map (cons source) #> ML_Context.exec (fn () => eval_source source) fun C_prf source = Proof.map_context (Context.proof_map (exec_eval source)) #> Proof.propagate_ml_env fun C_export_boot source context = context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> exec_eval source |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env fun C source = exec_eval source #> Local_Theory.propagate_ml_env fun C' env_lang src context = context |> C_Env.empty_env_tree |> C_Context.eval_source' env_lang (fn src => start src context) err accept src |> (fn (_, {context, reports_text, error_lines}) => tap (fn _ => case error_lines of [] => () | l => warning (cat_lines (rev l))) (C_Stack.Data_Tree.map (curry C_Stack.Data_Tree_Args.merge (reports_text, [])) context)) fun C_export_file (pos, _) lthy = let val c_sources = Data_In_Source.get (Context.Proof lthy) val binding = Path.binding ( Path.appends [ Path.basic C_Generated_Files.c_dir , Path.basic (string_of_int (length c_sources)) , lthy |> Proof_Context.theory_of |> Context.theory_name |> Path.explode |> Path.ext C_Generated_Files.c_ext ] , pos) in lthy |> C_Generated_Files.generate_file (binding, rev c_sources |> map (Input.source_content #> #1) |> cat_lines) |> tap (Proof_Context.theory_of #> (fn thy => let val file = Generated_Files.get_file thy binding in Generated_Files.export_file thy file; writeln (Export.message thy Path.current); writeln (prefix " " (Generated_Files.print_file file)) end)) end end \ subsection \Definitions of Inner Directive Commands\ subsubsection \Initialization\ ML \ \\<^theory>\Pure\\ \ structure C_Directive = struct local fun directive_update keyword data = C_Context.directive_update keyword (data, K (K (K I))) fun return f (env_cond, env) = ([], (env_cond, f env)) fun directive_update_define pos f_toks f_antiq = directive_update ("define", pos) (return o (fn C_Lex.Define (_, C_Lex.Group1 ([], [tok3]), NONE, C_Lex.Group1 ([], toks)) => let val map_ctxt = case (tok3, toks) of (C_Lex.Token ((pos, _), (C_Lex.Ident, ident)), [C_Lex.Token (_, (C_Lex.Integer (_, C_Lex.Repr_decimal, []), integer))]) => C_Env.map_context (Context.map_theory (Named_Target.theory_map (Specification.definition_cmd (SOME (Binding.make (ident, pos), NONE, NoSyn)) [] [] (Binding.empty_atts, ident ^ " \ " ^ integer) true #> tap (fn ((_, (_, t)), ctxt) => Output.information ("Generating " ^ Pretty.string_of (Syntax.pretty_term ctxt (Thm.prop_of t)) ^ Position.here (Position.range_position ( C_Lex.pos_of tok3 , C_Lex.end_pos_of (List.last toks))))) #> #2))) | _ => I in fn (env_dir, env_tree) => let val name = C_Lex.content_of tok3 val pos = [C_Lex.pos_of tok3] val data = (pos, serial (), (C_Scan.Left (f_toks toks), f_antiq)) in ( Symtab.update (name, data) env_dir , env_tree |> C_Context.markup_directive_define false (C_Ast.Left (data, C_Env_Ext.list_lookup env_dir name)) pos name |> map_ctxt) end end | C_Lex.Define (_, C_Lex.Group1 ([], [tok3]), SOME (C_Lex.Group1 (_ :: toks_bl, _)), _) => tap (fn _ => (* not yet implemented *) warning ("Ignored functional macro directive" ^ Position.here (Position.range_position (C_Lex.pos_of tok3, C_Lex.end_pos_of (List.last toks_bl))))) | _ => I)) in val setup_define = Context.theory_map o C_Context0.Directives.map ooo directive_update_define val _ = Theory.setup (Context.theory_map (C_Context0.Directives.map (directive_update_define \<^here> (K o pair) (K I) #> directive_update ("undef", \<^here>) (return o (fn C_Lex.Undef (C_Lex.Group2 (_, _, [tok])) => (fn (env_dir, env_tree) => let val name = C_Lex.content_of tok val pos1 = [C_Lex.pos_of tok] val data = Symtab.lookup env_dir name in ( (case data of NONE => env_dir | SOME _ => Symtab.delete name env_dir) , C_Context.markup_directive_define true (C_Ast.Right (pos1, data)) pos1 name env_tree) end) | _ => I))))) end end \ subsection \Definitions of Inner Annotation Commands\ subsubsection \Library\ ML \ \\<^file>\~~/src/Pure/Isar/toplevel.ML\\ \ structure C_Inner_Toplevel = struct val theory = Context.map_theory fun local_theory' target f gthy = let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val lthy' = lthy |> Local_Theory.new_group |> f false |> Local_Theory.reset_group; in finish lthy' end val generic_theory = I fun keep'' f = tap (f o Context.proof_of) end \ ML \ \\<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ \ structure C_Inner_Isar_Cmd = struct (** theory declarations **) (* generic setup *) fun setup0 f_typ f_val src = fn NONE => let val setup = "setup" in C_Context.expression "C_Ast" (Input.range_of src) setup (f_typ "C_Stack.stack_data" "C_Stack.stack_data_elem -> C_Env.env_lang -> Context.generic -> Context.generic") ("fn context => \ \let val (stack, env_lang) = C_Stack.Data_Lang.get' context \ \in " ^ f_val setup "stack" ^ " (stack |> hd) env_lang end context") (ML_Lex.read_source src) end | SOME rule => let val hook = "hook" in C_Context.expression "C_Ast" (Input.range_of src) hook (f_typ "C_Stack.stack_data" (C_Grammar_Rule.type_reduce rule ^ " C_Stack.stack_elem -> C_Env.env_lang -> Context.generic -> Context.generic")) ("fn context => \ \let val (stack, env_lang) = C_Stack.Data_Lang.get' context \ \in " ^ f_val hook "stack" ^ " " ^ "(stack \ \|> hd \ \|> C_Stack.map_svalue0 C_Grammar_Rule.reduce" ^ Int.toString rule ^ ")\ \env_lang \ \end \ \ context") (ML_Lex.read_source src) end val setup = setup0 (fn a => fn b => a ^ " -> " ^ b) (fn a => fn b => a ^ " " ^ b) val setup' = setup0 (K I) K (* print theorems, terms, types etc. *) local fun string_of_term ctxt s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; in Pretty.string_of (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) end; fun print_item string_of (modes, arg) ctxt = Print_Mode.with_modes modes (fn () => writeln (string_of ctxt arg)) (); in val print_term = print_item string_of_term; end; end \ ML \ \\<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ \ structure C_Inner_Syntax = struct val drop1 = fn C_Scan.Left f => C_Scan.Left (K o f) | C_Scan.Right (f, dir) => C_Scan.Right (K o f, dir) val drop2 = fn C_Scan.Left f => C_Scan.Left (K o K o f) | C_Scan.Right (f, dir) => C_Scan.Right (K o K o f, dir) val bottom_up = C_Env.Bottom_up o C_Env.Exec_annotation (**) fun pref_lex name = "#" ^ name val pref_bot = I fun pref_top name = name ^ "\" (**) fun command2' cmd f (pos_bot, pos_top) = let fun cmd' dir = cmd (C_Scan.Right (f, dir)) Keyword.thy_decl in cmd' bottom_up (pref_bot, pos_bot) #> cmd' C_Env.Top_down (pref_top, pos_top) end fun command3' cmd f (pos_lex, pos_bot, pos_top) = cmd (C_Scan.Left f) (pref_lex, pos_lex) #> command2' (K o cmd) f (pos_bot, pos_top) fun command2 cmd f (name, pos_bot, pos_top) = command2' (fn f => fn kind => fn (name_pref, pos) => cmd f kind (name_pref name, pos)) f (pos_bot, pos_top) fun command3 cmd f (name, pos_lex, pos_bot, pos_top) = command3' (fn f => fn (name_pref, pos) => cmd f (name_pref name, pos)) f (pos_lex, pos_bot, pos_top) (**) fun command00 f kind scan name = C_Annotation.command'' kind name "" (case f of C_Scan.Left f => (fn _ => C_Parse.range scan >> (fn (src, range) => C_Env.Lexing (range, f src range))) | C_Scan.Right (f, dir) => fn ((stack1, (to_delay, stack2)), _) => C_Parse.range scan >> (fn (src, range) => C_Env.Parsing ((stack1, stack2), (range, dir (f src range), Symtab.empty, to_delay)))) fun command00_no_range f kind name = C_Annotation.command'' kind name "" (case f of C_Scan.Left f => (fn (_, range) => Scan.succeed () >> K (C_Env.Lexing (range, f range))) | C_Scan.Right (f, dir) => fn ((stack1, (to_delay, stack2)), range) => Scan.succeed () >> K (C_Env.Parsing ((stack1, stack2), (range, dir (f range), Symtab.empty, to_delay)))) (**) fun command' f = command00 (drop1 f) Keyword.thy_decl fun command f scan = command2 (fn f => fn kind => command00 f kind scan) (K o f) fun command_range f = command00_no_range f Keyword.thy_decl val command_range' = command3 (command_range o drop1) fun command_no_range' f = command00_no_range (drop1 f) Keyword.thy_decl fun command_no_range f = command2 command00_no_range (K f) fun command0 f scan = command3 (fn f => command' (drop1 f) scan) f fun local_command' (name, pos_lex, pos_bot, pos_top) scan f = command3' (fn f => fn (name_pref, pos) => command' (drop1 f) (C_Token.syntax' (Parse.opt_target -- scan name_pref)) (name_pref name, pos)) (fn (target, arg) => C_Inner_Toplevel.local_theory' target (f arg)) (pos_lex, pos_bot, pos_top) fun local_command'' spec = local_command' spec o K val command0_no_range = command_no_range' o drop1 fun command0' f kind scan = command3 (fn f => fn (name, pos) => command00 (drop2 f) kind (scan name) (name, pos)) f end \ ML \ \\<^file>\~~/src/Pure/ML/ml_file.ML\\ \ structure C_Inner_File = struct fun command_c ({lines, pos, ...}: Token.file) = C_Module.C (Input.source true (cat_lines lines) (pos, pos)); fun C files gthy = command_c (hd (files (Context.theory_of gthy))) gthy; fun command_ml environment debug files gthy = let val file: Token.file = hd (files (Context.theory_of gthy)); val source = Token.file_source file; - val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); + val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); val flags: ML_Compiler.flags = {environment = environment, redirect = true, verbose = true, debug = debug, writeln = writeln, warning = warning}; in gthy |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |> Local_Theory.propagate_ml_env end; val ML = command_ml ""; val SML = command_ml ML_Env.SML; end; \ subsubsection \Initialization\ setup \ \\<^theory>\Pure\\ \ C_Thy_Header.add_keywords_minor (maps (fn ((name, pos_lex, pos_bot, pos_top), ty) => [ ((C_Inner_Syntax.pref_lex name, pos_lex), ty) , ((C_Inner_Syntax.pref_bot name, pos_bot), ty) , ((C_Inner_Syntax.pref_top name, pos_top), ty) ]) [ (("apply", \<^here>, \<^here>, \<^here>), ((Keyword.prf_script, []), ["proof"])) , (("by", \<^here>, \<^here>, \<^here>), ((Keyword.qed, []), ["proof"])) , (("done", \<^here>, \<^here>, \<^here>), ((Keyword.qed_script, []), ["proof"])) ]) \ ML \ \\<^theory>\Pure\\ \ local val semi = Scan.option (C_Parse.$$$ ";"); structure C_Isar_Cmd = struct fun ML source = ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> Local_Theory.propagate_ml_env fun theorem schematic ((long, binding, includes, elems, concl), (l_meth, o_meth)) int lthy = (if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl int lthy |> fold (fn m => tap (fn _ => Method.report m) #> Proof.apply m #> Seq.the_result "") l_meth |> (case o_meth of NONE => Proof.global_done_proof | SOME (m1, m2) => tap (fn _ => (Method.report m1; Option.map Method.report m2)) #> Proof.global_terminal_proof (m1, m2)) fun definition (((decl, spec), prems), params) = #2 oo Specification.definition_cmd decl params prems spec fun declare (facts, fixes) = #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes end local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); in fun theorem spec schematic = C_Inner_Syntax.local_command' spec (fn name_pref => (long_statement || short_statement) -- let val apply = Parse.$$$ (name_pref "apply") |-- Method.parse in Scan.repeat1 apply -- (Parse.$$$ (name_pref "done") >> K NONE) || Scan.repeat apply -- (Parse.$$$ (name_pref "by") |-- Method.parse -- Scan.option Method.parse >> SOME) end) (C_Isar_Cmd.theorem schematic) end val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Theory.setup ( C_Inner_Syntax.command (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup) C_Parse.ML_source ("\setup", \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.theory o Isar_Cmd.setup) C_Parse.ML_source ("setup", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Isar_Cmd.ML) C_Parse.ML_source ("ML", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Module.C) C_Parse.C_source ("C", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.ML NONE) Keyword.thy_load (fn name => C_Resources.parse_files name --| semi) ("ML_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.C) Keyword.thy_load (fn name => C_Resources.parse_files name --| semi) ("C_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.generic_theory o C_Module.C_export_boot) C_Parse.C_source ("C_export_boot", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command_range' (Context.map_theory o Named_Target.theory_map o C_Module.C_export_file) ("C_export_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command_no_range (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup \fn ((_, (_, pos1, pos2)) :: _) => (fn _ => fn _ => tap (fn _ => Position.reports_text [((Position.range (pos1, pos2) |> Position.range_position, Markup.intensify), "")])) | _ => fn _ => fn _ => I\) ("highlight", \<^here>, \<^here>) #> theorem ("theorem", \<^here>, \<^here>, \<^here>) false #> theorem ("lemma", \<^here>, \<^here>, \<^here>) false #> theorem ("corollary", \<^here>, \<^here>, \<^here>) false #> theorem ("proposition", \<^here>, \<^here>, \<^here>) false #> theorem ("schematic_goal", \<^here>, \<^here>, \<^here>) true #> C_Inner_Syntax.local_command'' ("definition", \<^here>, \<^here>, \<^here>) (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes) C_Isar_Cmd.definition #> C_Inner_Syntax.local_command'' ("declare", \<^here>, \<^here>, \<^here>) (Parse.and_list1 Parse.thms1 -- Parse.for_fixes) C_Isar_Cmd.declare #> C_Inner_Syntax.command0 (C_Inner_Toplevel.keep'' o C_Inner_Isar_Cmd.print_term) (C_Token.syntax' (opt_modes -- Parse.term)) ("term", \<^here>, \<^here>, \<^here>)) in end \ subsection \Definitions of Outer Classical Commands\ subsubsection \Library\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) ML \ \\<^file>\~~/src/Pure/Isar/parse.ML\\ \ structure C_Outer_Parse = struct val C_source = Parse.input (Parse.group (fn () => "C source") Parse.text) end \ ML \ \\<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ \ structure C_Outer_Syntax = struct val _ = Outer_Syntax.command \<^command_keyword>\C\ "" (C_Outer_Parse.C_source >> (Toplevel.generic_theory o C_Module.C)); end \ ML \ \\<^file>\~~/src/Pure/Isar/isar_cmd.ML\\ \ structure C_Outer_Isar_Cmd = struct (* diagnostic ML evaluation *) structure Diag_State = Proof_Data ( type T = Toplevel.state option; fun init _ = NONE; ); fun C_diag source state = let val opt_ctxt = try Toplevel.generic_theory_of state |> Option.map (Context.proof_of #> Diag_State.put (SOME state)); in Context.setmp_generic_context (Option.map Context.Proof opt_ctxt) (fn () => C_Module.eval_source source) () end; fun diag_state ctxt = (case Diag_State.get ctxt of SOME st => st | NONE => Toplevel.init_toplevel ()); val diag_goal = Proof.goal o Toplevel.proof_of o diag_state; val _ = Theory.setup (ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\C_state\) (Scan.succeed "C_Outer_Isar_Cmd.diag_state ML_context") #> ML_Antiquotation.value (Binding.qualify true "Isar" \<^binding>\C_goal\) (Scan.succeed "C_Outer_Isar_Cmd.diag_goal ML_context")); end \ ML \ \\<^file>\~~/src/Pure/ML/ml_file.ML\\ \ structure C_Outer_File = struct fun command_c ({src_path, lines, digest, pos}: Token.file) = let val provide = Resources.provide (src_path, digest); in I #> C_Module.C (Input.source true (cat_lines lines) (pos, pos)) #> Context.mapping provide (Local_Theory.background_theory provide) end; fun C files gthy = command_c (hd (files (Context.theory_of gthy))) gthy; end; \ subsubsection \Initialization\ ML \ \\<^theory>\Pure\\ \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\C_file\ "read and evaluate Isabelle/C file" (Resources.parse_files single --| semi >> (Toplevel.generic_theory o C_Outer_File.C)); val _ = Outer_Syntax.command \<^command_keyword>\C_export_boot\ "C text within theory or local theory, and export to bootstrap environment" (C_Outer_Parse.C_source >> (Toplevel.generic_theory o C_Module.C_export_boot)); val _ = Outer_Syntax.command \<^command_keyword>\C_prf\ "C text within proof" (C_Outer_Parse.C_source >> (Toplevel.proof o C_Module.C_prf)); val _ = Outer_Syntax.command \<^command_keyword>\C_val\ "diagnostic C text" (C_Outer_Parse.C_source >> (Toplevel.keep o C_Outer_Isar_Cmd.C_diag)); val _ = Outer_Syntax.local_theory \<^command_keyword>\C_export_file\ "diagnostic C text" (Scan.succeed () >> K (C_Module.C_export_file Position.no_range)); in end\ subsection \Syntax for Pure Term\ syntax "_C_translation_unit" :: \cartouche_position \ string\ ("\<^C>\<^sub>u\<^sub>n\<^sub>i\<^sub>t _") syntax "_C_external_declaration" :: \cartouche_position \ string\ ("\<^C>\<^sub>d\<^sub>e\<^sub>c\<^sub>l _") syntax "_C_expression" :: \cartouche_position \ string\ ("\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r _") syntax "_C_statement" :: \cartouche_position \ string\ ("\<^C>\<^sub>s\<^sub>t\<^sub>m\<^sub>t _") syntax "_C" :: \cartouche_position \ string\ ("\<^C> _") parse_translation \ C_Module.C_Term'.parse_translation [ (\<^syntax_const>\_C_translation_unit\, SOME C_Module.C_Term.tok_translation_unit) , (\<^syntax_const>\_C_external_declaration\, SOME C_Module.C_Term.tok_external_declaration) , (\<^syntax_const>\_C_expression\, SOME C_Module.C_Term.tok_expression) , (\<^syntax_const>\_C_statement\, SOME C_Module.C_Term.tok_statement) , (\<^syntax_const>\_C\, NONE) ] \ end diff --git a/thys/Isabelle_C/C11-FrontEnd/src/C_Document.thy b/thys/Isabelle_C/C11-FrontEnd/src/C_Document.thy --- a/thys/Isabelle_C/C11-FrontEnd/src/C_Document.thy +++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Document.thy @@ -1,238 +1,238 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section \Interface: Ontology Document\ theory C_Document imports C_Command begin -ML \ \\<^file>\~~/src/Pure/Thy/thy_output.ML\\ +ML \ \\<^file>\~~/src/Pure/Thy/document_output.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Thy/thy_output.ML Author: Makarius Theory document output. *) \ -structure C_Thy_Output = +structure C_Document_Output = struct (* output document source *) val output_symbols = single o Latex.symbols_output; fun output_comment ctxt (kind, syms) = (case kind of Comment.Comment => Input.cartouche_content syms |> output_document (ctxt |> Config.put Document_Antiquotation.thy_output_display false) {markdown = false} |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" | Comment.Cancel => Symbol_Pos.cartouche_content syms |> output_symbols |> Latex.enclose_body "%\n\\isamarkupcancel{" "}" | Comment.Latex => [Latex.symbols (Symbol_Pos.cartouche_content syms)] | Comment.Marker => []) and output_comment_document ctxt (comment, syms) = (case comment of SOME kind => output_comment ctxt (kind, syms) | NONE => [Latex.symbols syms]) and output_document_text ctxt syms = Comment.read_body syms |> maps (output_comment_document ctxt) and output_document ctxt {markdown} source = let val pos = Input.pos_of source; val syms = Input.source_explode source; val output_antiquotes = maps (Document_Antiquotation.evaluate (output_document_text ctxt) ctxt); fun output_line line = (if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ output_antiquotes (Markdown.line_content line); fun output_block (Markdown.Par lines) = Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines)) | output_block (Markdown.List {kind, body, ...}) = Latex.environment_block (Markdown.print_kind kind) (output_blocks body) and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks); in if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then [] else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms then let val ants = Antiquote.parse_comments pos syms; val reports = Antiquote.antiq_reports ants; val blocks = Markdown.read_antiquotes ants; val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks); in output_blocks blocks end else let val ants = Antiquote.parse_comments pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); val reports = Antiquote.antiq_reports ants; val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants); in output_antiquotes ants end end; (* output tokens with formal comments *) local val output_symbols_antiq = (fn Antiquote.Text syms => output_symbols syms | Antiquote.Control {name = (name, _), body, ...} => Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) :: output_symbols body | Antiquote.Antiq {body, ...} => Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); fun output_comment_symbols ctxt {antiq} (comment, syms) = (case (comment, antiq) of (NONE, false) => output_symbols syms | (NONE, true) => Antiquote.parse_comments (#1 (Symbol_Pos.range syms)) syms |> maps output_symbols_antiq | (SOME comment, _) => output_comment ctxt (comment, syms)); fun output_body ctxt antiq bg en syms = Comment.read_body syms |> maps (output_comment_symbols ctxt {antiq = antiq}) |> Latex.enclose_body bg en; in fun output_token ctxt tok = let fun output antiq bg en = output_body ctxt antiq bg en (Input.source_explode (C_Token.input_of tok)); in (case C_Token.kind_of tok of Token.Comment NONE => [] | Token.Comment (SOME Comment.Marker) => [] | Token.Command => output false "\\isacommand{" "}" | Token.Keyword => if Symbol.is_ascii_identifier (C_Token.content_of tok) then output false "\\isakeyword{" "}" else output false "" "" | Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}" | _ => output false "" "") end handle ERROR msg => error (msg ^ Position.here (C_Token.pos_of tok)); end; end; \ ML \ \\<^file>\~~/src/Pure/Thy/document_antiquotations.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Thy/document_antiquotations.ML Author: Makarius Miscellaneous document antiquotations. *) \ structure C_Document_Antiquotations = struct (* quasi-formal text (unchecked) *) local fun report_text ctxt text = let val pos = Input.pos_of text in Context_Position.reports ctxt [(pos, Markup.language_text (Input.is_delimited text)), (pos, Markup.raw_text)] end; fun prepare_text ctxt = Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt; val theory_text_antiquotation = - Thy_Output.antiquotation_raw_embedded \<^binding>\C_theory_text\ (Scan.lift Args.text_input) + Document_Output.antiquotation_raw_embedded \<^binding>\C_theory_text\ (Scan.lift Args.text_input) (fn ctxt => fn text => let val keywords = C_Thy_Header.get_keywords' ctxt; val _ = report_text ctxt text; val _ = Input.source_explode text |> C_Token.tokenize keywords {strict = true} |> maps (C_Token.reports keywords) |> Context_Position.reports_text ctxt; in prepare_text ctxt text |> C_Token.explode0 keywords - |> maps (C_Thy_Output.output_token ctxt) - |> Thy_Output.isabelle ctxt + |> maps (C_Document_Output.output_token ctxt) + |> Document_Output.isabelle ctxt end); in val _ = Theory.setup theory_text_antiquotation; end; (* C text *) local fun c_text name c = - Thy_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input) + Document_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input) (fn ctxt => fn text => let val _ = C_Module.eval_in text (SOME (Context.Proof ctxt)) (c text) in #1 (Input.source_content text) end); in val _ = Theory.setup (c_text \<^binding>\C\ (C_Module.c_enclose "" "") #> c_text \<^binding>\C_text\ (K C_Lex.read_init)); end; end; \ end diff --git a/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy b/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy --- a/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy +++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy @@ -1,1364 +1,1364 @@ (****************************************************************************** * Isabelle/C * * Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section \Core Language: Parsing Support (C Language without Annotations)\ theory C_Parser_Language imports C_Environment begin text \ As mentioned in \<^theory>\Isabelle_C.C_Ast\, Isabelle/C depends on certain external parsing libraries, such as \<^dir>\../../src_ext/mlton\, and more specifically \<^dir>\../../src_ext/mlton/lib/mlyacc-lib\. Actually, the sole theory making use of the files in \<^dir>\../../src_ext/mlton/lib/mlyacc-lib\ is the present \<^file>\C_Parser_Language.thy\. (Any other remaining files in \<^dir>\../../src_ext/mlton\ are not used by Isabelle/C, they come from the original repository of MLton: \<^url>\https://github.com/MLton/mlton\.) \ subsection \Parsing Library (Including Semantic Functions)\ ML \ \\<^file>\../generated/c_grammar_fun.grm.sml\\ (* * Modified by Frédéric Tuong, Université Paris-Saclay * * * * * * * * * * * * * * * * * * * * * * * * * * * * * Language.C * https://hackage.haskell.org/package/language-c * * Copyright (c) 1999-2017 Manuel M T Chakravarty * Duncan Coutts * Benedikt Huber * Portions Copyright (c) 1989,1990 James A. Roskind * * * * * * * * * * * * * * * * * * * * * * * * * * * * * Language.C.Comments * https://hackage.haskell.org/package/language-c-comments * * Copyright (c) 2010-2014 Geoff Hulette *) \ signature C_GRAMMAR_RULE_LIB = sig type arg = C_Env.T type 'a monad = arg -> 'a * arg (* type aliases *) type class_Pos = C_Ast.class_Pos type reports_text0' = { markup : Markup.T, markup_body : string } type reports_text0 = reports_text0' list -> reports_text0' list type ('a, 'b) reports_base = ('a C_Env.markup_store * Position.T list, Position.T list * 'a C_Env.markup_store option) C_Ast.either -> Position.T list -> string -> 'b -> 'b (**) type NodeInfo = C_Ast.nodeInfo type CStorageSpec = NodeInfo C_Ast.cStorageSpecifier type CFunSpec = NodeInfo C_Ast.cFunctionSpecifier type CConst = NodeInfo C_Ast.cConstant type 'a CInitializerList = ('a C_Ast.cPartDesignator List.list * 'a C_Ast.cInitializer) List.list type CTranslUnit = NodeInfo C_Ast.cTranslationUnit type CExtDecl = NodeInfo C_Ast.cExternalDeclaration type CFunDef = NodeInfo C_Ast.cFunctionDef type CDecl = NodeInfo C_Ast.cDeclaration type CDeclr = NodeInfo C_Ast.cDeclarator type CDerivedDeclr = NodeInfo C_Ast.cDerivedDeclarator type CArrSize = NodeInfo C_Ast.cArraySize type CStat = NodeInfo C_Ast.cStatement type CAsmStmt = NodeInfo C_Ast.cAssemblyStatement type CAsmOperand = NodeInfo C_Ast.cAssemblyOperand type CBlockItem = NodeInfo C_Ast.cCompoundBlockItem type CDeclSpec = NodeInfo C_Ast.cDeclarationSpecifier type CTypeSpec = NodeInfo C_Ast.cTypeSpecifier type CTypeQual = NodeInfo C_Ast.cTypeQualifier type CAlignSpec = NodeInfo C_Ast.cAlignmentSpecifier type CStructUnion = NodeInfo C_Ast.cStructureUnion type CEnum = NodeInfo C_Ast.cEnumeration type CInit = NodeInfo C_Ast.cInitializer type CInitList = NodeInfo CInitializerList type CDesignator = NodeInfo C_Ast.cPartDesignator type CAttr = NodeInfo C_Ast.cAttribute type CExpr = NodeInfo C_Ast.cExpression type CBuiltin = NodeInfo C_Ast.cBuiltinThing type CStrLit = NodeInfo C_Ast.cStringLiteral (**) type ClangCVersion = C_Ast.clangCVersion type Ident = C_Ast.ident type Position = C_Ast.positiona type PosLength = Position * int type Name = C_Ast.namea type Bool = bool type CString = C_Ast.cString type CChar = C_Ast.cChar type CInteger = C_Ast.cInteger type CFloat = C_Ast.cFloat type CStructTag = C_Ast.cStructTag type CUnaryOp = C_Ast.cUnaryOp type 'a CStringLiteral = 'a C_Ast.cStringLiteral type 'a CConstant = 'a C_Ast.cConstant type ('a, 'b) Either = ('a, 'b) C_Ast.either type CIntRepr = C_Ast.cIntRepr type CIntFlag = C_Ast.cIntFlag type CAssignOp = C_Ast.cAssignOp type Comment = C_Ast.comment (**) type 'a Reversed = 'a C_Ast.Reversed type CDeclrR = C_Ast.CDeclrR type 'a Maybe = 'a C_Ast.optiona type 'a Located = 'a C_Ast.Located (**) structure List : sig val reverse : 'a list -> 'a list end (* monadic operations *) val return : 'a -> 'a monad val bind : 'a monad -> ('a -> 'b monad) -> 'b monad val bind' : 'b monad -> ('b -> unit monad) -> 'b monad val >> : unit monad * 'a monad -> 'a monad (* position reports *) val markup_make : ('a -> reports_text0' option) -> ('a -> 'b) -> ('b option -> string) -> ((Markup.T -> reports_text0) -> bool -> ('b, 'b option * string * reports_text0) C_Ast.either -> reports_text0) -> ('a, C_Position.reports_text) reports_base val markup_tvar : (C_Env.markup_global, C_Position.reports_text) reports_base val markup_var_enum : (C_Env.markup_global, C_Position.reports_text) reports_base val markup_var : (C_Env.markup_ident, C_Position.reports_text) reports_base val markup_var_bound : (C_Env.markup_ident, C_Position.reports_text) reports_base val markup_var_improper : (C_Env.markup_ident, C_Position.reports_text) reports_base (* Language.C.Data.RList *) val empty : 'a list Reversed val singleton : 'a -> 'a list Reversed val snoc : 'a list Reversed -> 'a -> 'a list Reversed val rappend : 'a list Reversed -> 'a list -> 'a list Reversed val rappendr : 'a list Reversed -> 'a list Reversed -> 'a list Reversed val rmap : ('a -> 'b) -> 'a list Reversed -> 'b list Reversed (* Language.C.Data.Position *) val posOf : 'a -> Position val posOf' : bool -> class_Pos -> Position * int val make_comment : Symbol_Pos.T list -> Symbol_Pos.T list -> Symbol_Pos.T list -> Position.range -> Comment (* Language.C.Data.Node *) val mkNodeInfo' : Position -> PosLength -> Name -> NodeInfo val decode : NodeInfo -> (class_Pos, string) Either val decode_error' : NodeInfo -> Position.range (* Language.C.Data.Ident *) val quad : string list -> int val ident_encode : string -> int val ident_decode : int -> string val mkIdent : Position * int -> string -> Name -> Ident val internalIdent : string -> Ident (* Language.C.Syntax.AST *) val liftStrLit : 'a CStringLiteral -> 'a CConstant (* Language.C.Syntax.Constants *) val concatCStrings : CString list -> CString (* Language.C.Parser.ParserMonad *) val getNewName : Name monad val shadowTypedef0'''' : string -> Position.T list -> C_Env.markup_ident -> C_Env.env_lang -> C_Env.env_tree -> C_Env.env_lang * C_Env.env_tree val shadowTypedef0' : C_Ast.CDeclSpec list C_Env.parse_status -> bool -> C_Ast.ident * C_Ast.CDerivedDeclr list -> C_Env.env_lang -> C_Env.env_tree -> C_Env.env_lang * C_Env.env_tree val isTypeIdent : string -> arg -> bool val enterScope : unit monad val leaveScope : unit monad val getCurrentPosition : Position monad (* Language.C.Parser.Tokens *) val CTokCLit : CChar -> (CChar -> 'a) -> 'a val CTokILit : CInteger -> (CInteger -> 'a) -> 'a val CTokFLit : CFloat -> (CFloat -> 'a) -> 'a val CTokSLit : CString -> (CString -> 'a) -> 'a (* Language.C.Parser.Parser *) val reverseList : 'a list -> 'a list Reversed val L : 'a -> int -> 'a Located monad val unL : 'a Located -> 'a val withNodeInfo : int -> (NodeInfo -> 'a) -> 'a monad val withNodeInfo_CExtDecl : CExtDecl -> (NodeInfo -> 'a) -> 'a monad val withNodeInfo_CExpr : CExpr list Reversed -> (NodeInfo -> 'a) -> 'a monad val withLength : NodeInfo -> (NodeInfo -> 'a) -> 'a monad val reverseDeclr : CDeclrR -> CDeclr val withAttribute : int -> CAttr list -> (NodeInfo -> CDeclrR) -> CDeclrR monad val withAttributePF : int -> CAttr list -> (NodeInfo -> CDeclrR -> CDeclrR) -> (CDeclrR -> CDeclrR) monad val appendObjAttrs : CAttr list -> CDeclr -> CDeclr val withAsmNameAttrs : CStrLit Maybe * CAttr list -> CDeclrR -> CDeclrR monad val appendDeclrAttrs : CAttr list -> CDeclrR -> CDeclrR val ptrDeclr : CDeclrR -> CTypeQual list -> NodeInfo -> CDeclrR val funDeclr : CDeclrR -> (Ident list, (CDecl list * Bool)) Either -> CAttr list -> NodeInfo -> CDeclrR val arrDeclr : CDeclrR -> CTypeQual list -> Bool -> Bool -> CExpr Maybe -> NodeInfo -> CDeclrR val liftTypeQuals : CTypeQual list Reversed -> CDeclSpec list val liftCAttrs : CAttr list -> CDeclSpec list val addTrailingAttrs : CDeclSpec list Reversed -> CAttr list -> CDeclSpec list Reversed val emptyDeclr : CDeclrR val mkVarDeclr : Ident -> NodeInfo -> CDeclrR val doDeclIdent : CDeclSpec list -> CDeclrR -> unit monad val ident_of_decl : (Ident list, CDecl list * bool) C_Ast.either -> (Ident * CDerivedDeclr list * CDeclSpec list) list val doFuncParamDeclIdent : CDeclr -> unit monad end structure C_Grammar_Rule_Lib : C_GRAMMAR_RULE_LIB = struct open C_Ast type arg = C_Env.T type 'a monad = arg -> 'a * arg (**) type reports_text0' = { markup : Markup.T, markup_body : string } type reports_text0 = reports_text0' list -> reports_text0' list type 'a reports_store = Position.T list * serial * 'a type ('a, 'b) reports_base = ('a C_Env.markup_store * Position.T list, Position.T list * 'a C_Env.markup_store option) C_Ast.either -> Position.T list -> string -> 'b -> 'b fun markup_init markup = { markup = markup, markup_body = "" } val look_idents = C_Env_Ext.list_lookup o C_Env_Ext.get_idents val look_idents' = C_Env_Ext.list_lookup o C_Env_Ext.get_idents' val look_tyidents_typedef = C_Env_Ext.list_lookup o C_Env_Ext.get_tyidents_typedef val look_tyidents'_typedef = C_Env_Ext.list_lookup o C_Env_Ext.get_tyidents'_typedef val To_string0 = meta_of_logic val ident_encode = Word8Vector.foldl (fn (w, acc) => Word8.toInt w + acc * 256) 0 o Byte.stringToBytes fun ident_decode nb = radixpand (256, nb) |> map chr |> implode fun reverse l = rev l fun report _ [] _ = I | report markup ps x = let val ms = markup x in fold (fn p => fold (fn {markup, markup_body} => cons ((p, markup), markup_body)) ms) ps end fun markup_make typing get_global desc report' data = report (fn name => let val (def, ps, id, global, typing) = case data of Left ((ps, id, param), ps' as _ :: _) => ( true , ps , id , Right ( SOME (get_global param) , "Redefinition of " ^ quote name ^ Position.here_list ps \ \Any positions provided here will be explicitly reported, which might not be the desired effect. So we explicitly refer the reader to a separate tooltip.\ ^ " (more details in the command modifier tooltip)" , cons { markup = Markup.class_parameter , markup_body = "redefining this" ^ Position.here_list ps' }) , typing param) | Left ((ps, id, param), _) => (true, ps, id, Left (get_global param), typing param) | Right (_, SOME (ps, id, param)) => (false, ps, id, Left (get_global param), typing param) | Right (ps, _) => ( true , ps , serial () , Right (NONE, "Undeclared " ^ quote name ^ Position.here_list ps, I) , NONE) fun markup_elem name = (name, (name, []): Markup.T) val (varN, var) = markup_elem (desc (case global of Left b => SOME b | Right (SOME b, _, _) => SOME b | _ => NONE)); val entity = Markup.entity varN name val cons' = cons o markup_init in (cons' var #> report' cons' def global #> (case typing of NONE => I | SOME x => cons x)) (map (fn pos => markup_init (Markup.properties (Position.entity_properties_of def id pos) entity)) ps) end) fun markup_make' typing get_global desc report = markup_make typing get_global (fn global => "C " ^ (case global of SOME true => "global " | SOME false => "local " | NONE => "") ^ desc) (fn cons' => fn def => fn Left b => report cons' def b | Right (b, msg, f) => tap (fn _ => Output.information msg) #> f #> (case b of NONE => cons' Markup.free | SOME b => report cons' def b)) fun markup_tvar0 desc = markup_make' (K NONE) I desc (fn cons' => fn def => fn true => cons' (if def then Markup.free else Markup.ML_keyword3) | false => cons' Markup.skolem) val markup_tvar = markup_tvar0 "type variable" val markup_var_enum = markup_tvar0 "enum tag" fun string_of_list f = (fn [] => NONE | [s] => SOME s | s => SOME ("[" ^ String.concatWith ", " s ^ "]")) o map f val string_of_cDeclarationSpecifier = fn C_Ast.CStorageSpec0 _ => "storage" | C_Ast.CTypeSpec0 t => (case t of CVoidType0 _ => "void" | CCharType0 _ => "char" | CShortType0 _ => "short" | CIntType0 _ => "int" | CLongType0 _ => "long" | CFloatType0 _ => "float" | CDoubleType0 _ => "double" | CSignedType0 _ => "signed" | CUnsigType0 _ => "unsig" | CBoolType0 _ => "bool" | CComplexType0 _ => "complex" | CInt128Type0 _ => "int128" | CSUType0 _ => "SU" | CEnumType0 _ => "enum" | CTypeDef0 _ => "typedef" | CTypeOfExpr0 _ => "type_of_expr" | CTypeOfType0 _ => "type_of_type" | CAtomicType0 _ => "atomic") | C_Ast.CTypeQual0 _ => "type_qual" | C_Ast.CFunSpec0 _ => "fun" | C_Ast.CAlignSpec0 _ => "align" fun typing {params, ret, ...} = SOME { markup = Markup.typing , markup_body = case ( string_of_list (fn C_Ast.CPtrDeclr0 _ => "pointer" | C_Ast.CArrDeclr0 _ => "array" | C_Ast.CFunDeclr0 (C_Ast.Left _, _, _) => "function [...] ->" | C_Ast.CFunDeclr0 (C_Ast.Right (l_decl, _), _, _) => "function " ^ (String.concatWith " -> " (map (fn CDecl0 ([decl], _, _) => string_of_cDeclarationSpecifier decl | CDecl0 (l, _, _) => "(" ^ String.concatWith " " (map string_of_cDeclarationSpecifier l) ^ ")" | CStaticAssert0 _ => "static_assert") l_decl)) ^ " ->") params , case ret of C_Env.Previous_in_stack => SOME "..." | C_Env.Parsed ret => string_of_list string_of_cDeclarationSpecifier ret) of (NONE, NONE) => let val _ = warning "markup_var: Not yet implemented" in "" end | (SOME params, NONE) => params | (NONE, SOME ret) => ret | (SOME params, SOME ret) => params ^ " " ^ ret } val markup_var = markup_make' typing #global "variable" (fn cons' => fn def => fn true => if def then cons' Markup.free else cons' Markup.delimiter (*explicit black color, otherwise the default color of constants might be automatically chosen (especially in term cartouches)*) | false => cons' Markup.bound) val markup_var_bound = markup_make' typing #global "variable" (fn cons' => K (K (cons' Markup.bound))) val markup_var_improper = markup_make' typing #global "variable" (fn cons' => K (K (cons' Markup.improper))) (**) val return = pair fun bind f g = f #-> g fun bind' f g = bind f (fn r => bind (g r) (fn () => return r)) fun a >> b = a #> b o #2 fun sequence_ f = fn [] => return () | x :: xs => f x >> sequence_ f xs (* Language.C.Data.RList *) val empty = [] fun singleton x = [x] fun snoc xs x = x :: xs fun rappend xs ys = rev ys @ xs fun rappendr xs ys = ys @ xs val rmap = map val viewr = fn [] => error "viewr: empty RList" | x :: xs => (xs, x) (* Language.C.Data.Position *) val nopos = NoPosition fun posOf _ = NoPosition fun posOf' mk_range = (if mk_range then Position.range else I) #> (fn (pos1, pos2) => let val {offset = offset, end_offset = end_offset, ...} = Position.dest pos1 in ( Position offset (From_string (C_Env.encode_positions [pos1, pos2])) 0 0 , end_offset - offset) end) fun posOf'' node env = let val (stack, len) = #rule_input env val (mk_range, (pos1a, pos1b)) = case node of Left i => (true, nth stack (len - i - 1)) | Right range => (false, range) val (pos2a, pos2b) = nth stack 0 in ( (posOf' mk_range (pos1a, pos1b) |> #1, posOf' true (pos2a, pos2b)) , env |> C_Env_Ext.map_output_pos (K (SOME (pos1a, pos2b))) |> C_Env_Ext.map_output_vacuous (K false)) end val posOf''' = posOf'' o Left val internalPos = InternalPosition fun make_comment body_begin body body_end range = Commenta ( posOf' false range |> #1 , From_string (Symbol_Pos.implode (body_begin @ body @ body_end)) , case body_end of [] => SingleLine | _ => MultiLine) (* Language.C.Data.Node *) val undefNode = OnlyPos nopos (nopos, ~1) fun mkNodeInfoOnlyPos pos = OnlyPos pos (nopos, ~1) fun mkNodeInfo pos name = NodeInfo pos (nopos, ~1) name val mkNodeInfo' = NodeInfo val decode = (fn OnlyPos0 range => range | NodeInfo0 (pos1, (pos2, len2), _) => (pos1, (pos2, len2))) #> (fn (Position0 (_, s1, _, _), (Position0 (_, s2, _, _), _)) => (case (C_Env.decode_positions (To_string0 s1), C_Env.decode_positions (To_string0 s2)) of ([pos1, _], [_, pos2]) => Left (Position.range (pos1, pos2)) | _ => Right "Expecting 2 elements") | _ => Right "Invalid position") fun decode_error' x = case decode x of Left x => x | Right msg => error msg fun decode_error x = Right (decode_error' x) val nameOfNode = fn OnlyPos0 _ => NONE | NodeInfo0 (_, _, name) => SOME name (* Language.C.Data.Ident *) local val bits7 = Integer.pow 7 2 val bits14 = Integer.pow 14 2 val bits21 = Integer.pow 21 2 val bits28 = Integer.pow 28 2 in fun quad s = case s of [] => 0 | c1 :: [] => ord c1 | c1 :: c2 :: [] => ord c2 * bits7 + ord c1 | c1 :: c2 :: c3 :: [] => ord c3 * bits14 + ord c2 * bits7 + ord c1 | c1 :: c2 :: c3 :: c4 :: s => ((ord c4 * bits21 + ord c3 * bits14 + ord c2 * bits7 + ord c1) mod bits28) + (quad s mod bits28) end local fun internalIdent0 pos s = Ident (From_string s, ident_encode s, pos) in fun mkIdent (pos, len) s name = internalIdent0 (mkNodeInfo' pos (pos, len) name) s val internalIdent = internalIdent0 (mkNodeInfoOnlyPos internalPos) end (* Language.C.Syntax.AST *) fun liftStrLit (CStrLit0 (str, at)) = CStrConst str at (* Language.C.Syntax.Constants *) fun concatCStrings cs = CString0 (flattena (map (fn CString0 (s,_) => s) cs), exists (fn CString0 (_, b) => b) cs) (* Language.C.Parser.ParserMonad *) fun getNewName env = (Namea (C_Env_Ext.get_namesupply env), C_Env_Ext.map_namesupply (fn x => x + 1) env) fun addTypedef (Ident0 (_, i, node)) env = let val name = ident_decode i val pos1 = [decode_error' node |> #1] val data = (pos1, serial (), null (C_Env_Ext.get_scopes env)) in ((), env |> C_Env_Ext.map_idents (Symtab.delete_safe name) |> C_Env_Ext.map_tyidents_typedef (Symtab.update (name, data)) |> C_Env_Ext.map_reports_text (markup_tvar (Left (data, flat [ look_idents env name, look_tyidents_typedef env name ])) pos1 name)) end fun shadowTypedef0''' name pos data0 env_lang env_tree = let val data = (pos, serial (), data0) val update_id = Symtab.update (name, data) in ( env_lang |> C_Env_Ext.map_tyidents'_typedef (Symtab.delete_safe name) |> C_Env_Ext.map_idents' update_id , update_id , env_tree |> C_Env.map_reports_text (markup_var (Left (data, flat [ look_idents' env_lang name , look_tyidents'_typedef env_lang name ])) pos name)) end fun shadowTypedef0'''' name pos data0 env_lang env_tree = let val (env_lang, _, env_tree) = shadowTypedef0''' name pos data0 env_lang env_tree in ( env_lang, env_tree) end fun shadowTypedef0'' ret global (Ident0 (_, i, node), params) = shadowTypedef0''' (ident_decode i) [decode_error' node |> #1] {global = global, params = params, ret = ret} fun shadowTypedef0' ret global ident env_lang env_tree = let val (env_lang, _, env_tree) = shadowTypedef0'' ret global ident env_lang env_tree in (env_lang, env_tree) end fun shadowTypedef0 ret global f ident env = let val (update_id, env) = C_Env.map_env_lang_tree' (fn env_lang => fn env_tree => let val (env_lang, update_id, env_tree) = shadowTypedef0'' ret global ident env_lang env_tree in (update_id, (env_lang, env_tree)) end) env in ((), f update_id env) end fun shadowTypedef_fun ident env = shadowTypedef0 C_Env.Previous_in_stack (case C_Env_Ext.get_scopes env of _ :: [] => true | _ => false) (fn update_id => C_Env_Ext.map_scopes (fn (NONE, x) :: xs => (SOME (fst ident), C_Env.map_idents update_id x) :: xs | (SOME _, _) :: _ => error "Not yet implemented" | [] => error "Not expecting an empty scope")) ident env fun shadowTypedef (i, params, ret) env = shadowTypedef0 (C_Env.Parsed ret) (List.null (C_Env_Ext.get_scopes env)) (K I) (i, params) env fun isTypeIdent s0 = Symtab.exists (fn (s1, _) => s0 = s1) o C_Env_Ext.get_tyidents_typedef fun enterScope env = ((), C_Env_Ext.map_scopes (cons (NONE, C_Env_Ext.get_var_table env)) env) fun leaveScope env = case C_Env_Ext.get_scopes env of [] => error "leaveScope: already in global scope" | (_, var_table) :: scopes => ((), env |> C_Env_Ext.map_scopes (K scopes) |> C_Env_Ext.map_var_table (K var_table)) val getCurrentPosition = return NoPosition (* Language.C.Parser.Tokens *) fun CTokCLit x f = x |> f fun CTokILit x f = x |> f fun CTokFLit x f = x |> f fun CTokSLit x f = x |> f (* Language.C.Parser.Parser *) fun reverseList x = rev x fun L a i = posOf''' i #>> curry Located a fun unL (Located (a, _)) = a fun withNodeInfo00 (pos1, (pos2, len2)) mkAttrNode name = return (mkAttrNode (NodeInfo pos1 (pos2, len2) name)) fun withNodeInfo0 x = x |> bind getNewName oo withNodeInfo00 fun withNodeInfo0' node mkAttrNode env = let val (range, env) = posOf'' node env in withNodeInfo0 range mkAttrNode env end fun withNodeInfo x = x |> withNodeInfo0' o Left fun withNodeInfo' x = x |> withNodeInfo0' o decode_error fun withNodeInfo_CExtDecl x = x |> withNodeInfo' o (fn CDeclExt0 (CDecl0 (_, _, node)) => node | CDeclExt0 (CStaticAssert0 (_, _, node)) => node | CFDefExt0 (CFunDef0 (_, _, _, _, node)) => node | CAsmExt0 (_, node) => node) val get_node_CExpr = fn CComma0 (_, a) => a | CAssign0 (_, _, _, a) => a | CCond0 (_, _, _, a) => a | CBinary0 (_, _, _, a) => a | CCast0 (_, _, a) => a | CUnary0 (_, _, a) => a | CSizeofExpr0 (_, a) => a | CSizeofType0 (_, a) => a | CAlignofExpr0 (_, a) => a | CAlignofType0 (_, a) => a | CComplexReal0 (_, a) => a | CComplexImag0 (_, a) => a | CIndex0 (_, _, a) => a | CCall0 (_, _, a) => a | CMember0 (_, _, _, a) => a | CVar0 (_, a) => a | CConst0 c => (case c of CIntConst0 (_, a) => a | CCharConst0 (_, a) => a | CFloatConst0 (_, a) => a | CStrConst0 (_, a) => a) | CCompoundLit0 (_, _, a) => a | CGenericSelection0 (_, _, a) => a | CStatExpr0 (_, a) => a | CLabAddrExpr0 (_, a) => a | CBuiltinExpr0 cBuiltinThing => (case cBuiltinThing of CBuiltinVaArg0 (_, _, a) => a | CBuiltinOffsetOf0 (_, _, a) => a | CBuiltinTypesCompatible0 (_, _, a) => a) fun withNodeInfo_CExpr x = x |> withNodeInfo' o get_node_CExpr o hd fun withLength node mkAttrNode = bind (posOf'' (decode_error node)) (fn range => withNodeInfo00 range mkAttrNode (case nameOfNode node of NONE => error "nameOfNode" | SOME name => name)) fun reverseDeclr (CDeclrR0 (ide, reversedDDs, asmname, cattrs, at)) = CDeclr ide (rev reversedDDs) asmname cattrs at fun appendDeclrAttrs newAttrs (CDeclrR0 (ident, l, asmname, cattrs, at)) = case l of [] => CDeclrR ident empty asmname (cattrs @ newAttrs) at | x :: xs => let val appendAttrs = fn CPtrDeclr0 (typeQuals, at) => CPtrDeclr (typeQuals @ map CAttrQual newAttrs) at | CArrDeclr0 (typeQuals, arraySize, at) => CArrDeclr (typeQuals @ map CAttrQual newAttrs) arraySize at | CFunDeclr0 (parameters, cattrs, at) => CFunDeclr parameters (cattrs @ newAttrs) at in CDeclrR ident (appendAttrs x :: xs) asmname cattrs at end fun withAttribute node cattrs mkDeclrNode = bind (posOf''' node) (fn (pos, _) => bind getNewName (fn name => let val attrs = mkNodeInfo pos name val newDeclr = appendDeclrAttrs cattrs (mkDeclrNode attrs) in return newDeclr end)) fun withAttributePF node cattrs mkDeclrCtor = bind (posOf''' node) (fn (pos, _) => bind getNewName (fn name => let val attrs = mkNodeInfo pos name val newDeclr = appendDeclrAttrs cattrs o mkDeclrCtor attrs in return newDeclr end)) fun appendObjAttrs newAttrs (CDeclr0 (ident, indirections, asmname, cAttrs, at)) = CDeclr ident indirections asmname (cAttrs @ newAttrs) at fun appendObjAttrsR newAttrs (CDeclrR0 (ident, indirections, asmname, cAttrs, at)) = CDeclrR ident indirections asmname (cAttrs @ newAttrs) at fun setAsmName mAsmName (CDeclrR0 (ident, indirections, oldName, cattrs, at)) = case (case (mAsmName, oldName) of (None, None) => Right None | (None, oldname as Some _) => Right oldname | (newname as Some _, None) => Right newname | (Some n1, Some n2) => Left (n1, n2)) of Left (n1, n2) => let fun showName (CStrLit0 (CString0 (s, _), _)) = To_string0 s in error ("Duplicate assembler name: " ^ showName n1 ^ " " ^ showName n2) end | Right newName => return (CDeclrR ident indirections newName cattrs at) fun withAsmNameAttrs (mAsmName, newAttrs) declr = setAsmName mAsmName (appendObjAttrsR newAttrs declr) fun ptrDeclr (CDeclrR0 (ident, derivedDeclrs, asmname, cattrs, dat)) tyquals at = CDeclrR ident (snoc derivedDeclrs (CPtrDeclr tyquals at)) asmname cattrs dat fun funDeclr (CDeclrR0 (ident, derivedDeclrs, asmname, dcattrs, dat)) params cattrs at = CDeclrR ident (snoc derivedDeclrs (CFunDeclr params cattrs at)) asmname dcattrs dat fun arrDeclr (CDeclrR0 (ident, derivedDeclrs, asmname, cattrs, dat)) tyquals var_sized static_size size_expr_opt at = CDeclrR ident (snoc derivedDeclrs (CArrDeclr tyquals (case size_expr_opt of Some e => CArrSize static_size e | None => CNoArrSize var_sized) at)) asmname cattrs dat val liftTypeQuals = map CTypeQual o reverse val liftCAttrs = map (CTypeQual o CAttrQual) fun addTrailingAttrs declspecs new_attrs = case viewr declspecs of (specs_init, CTypeSpec0 (CSUType0 (CStruct0 (tag, name, Some def, def_attrs, su_node), node))) => snoc specs_init (CTypeSpec (CSUType (CStruct tag name (Just def) (def_attrs @ new_attrs) su_node) node)) | (specs_init, CTypeSpec0 (CEnumType0 (CEnum0 (name, Some def, def_attrs, e_node), node))) => snoc specs_init (CTypeSpec (CEnumType (CEnum name (Just def) (def_attrs @ new_attrs) e_node) node)) | _ => rappend declspecs (liftCAttrs new_attrs) val emptyDeclr = CDeclrR Nothing empty Nothing [] undefNode fun mkVarDeclr ident = CDeclrR (Some ident) empty Nothing [] fun doDeclIdent declspecs (decl as CDeclrR0 (mIdent, _, _, _, _)) = case mIdent of None => return () | Some ident => if exists (fn CStorageSpec0 (CTypedef0 _) => true | _ => false) declspecs then addTypedef ident else shadowTypedef ( ident , case reverseDeclr decl of CDeclr0 (_, params, _, _, _) => params , declspecs) val ident_of_decl = fn Left params => map (fn i => (i, [], [])) params | Right (params, _) => maps (fn CDecl0 (ret, l, _) => maps (fn ((Some (CDeclr0 (Some mIdent, params, _, _, _)),_),_) => [(mIdent, params, ret)] | _ => []) l | _ => []) params local fun sequence_' f = sequence_ f o ident_of_decl val is_fun = fn CFunDeclr0 _ => true | _ => false in fun doFuncParamDeclIdent (CDeclr0 (mIdent0, param0, _, _, node0)) = let val (param_not_fun, param0') = chop_prefix (not o is_fun) param0 val () = if null param_not_fun then () else Output.information ("Not a function" ^ Position.here (decode_error' (case mIdent0 of None => node0 | Some (Ident0 (_, _, node)) => node) |> #1)) val (param_fun, param0') = chop_prefix is_fun param0' in (case mIdent0 of None => return () | Some mIdent0 => shadowTypedef_fun (mIdent0, param0)) >> sequence_ shadowTypedef (maps (fn CFunDeclr0 (params, _, _) => ident_of_decl params | _ => []) param_fun) >> sequence_ (fn CFunDeclr0 (params, _, _) => C_Env.map_env_tree (pair Symtab.empty #> sequence_' (fn (Ident0 (_, i, node), params, ret) => fn (env_lang, env_tree) => pair () let val name = ident_decode i val pos = [decode_error' node |> #1] val data = ( pos , serial () , {global = false, params = params, ret = C_Env.Parsed ret}) in ( env_lang |> Symtab.update (name, data) , env_tree |> C_Env.map_reports_text (markup_var_improper (Left (data, C_Env_Ext.list_lookup env_lang name)) pos name)) end) params #> #2 o #2) #> pair () | _ => return ()) param0' end end (**) structure List = struct val reverse = rev end end \ subsection \Miscellaneous\ ML \ \\<^file>\~~/src/Pure/Thy/document_antiquotations.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/Thy/document_antiquotations.ML Author: Makarius Miscellaneous document antiquotations. *) \ structure ML_Document_Antiquotations = struct (* ML text *) local fun ml_text name ml = - Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input \ \TODO: enable reporting with \<^ML_type>\Token.file\ as in \<^ML>\Resources.parse_files\\) + Document_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input \ \TODO: enable reporting with \<^ML_type>\Token.file\ as in \<^ML>\Resources.parse_files\\) (fn ctxt => fn text => let val file_content = Token.file_source (Command.read_file (Resources.master_directory (Proof_Context.theory_of ctxt)) Position.none false (Path.explode (#1 (Input.source_content text)))) val _ = (*TODO: avoid multiple file scanning*) ML_Context.eval_in (SOME ctxt) ML_Compiler.flags Position.none (* \ (optionally) disabling a potential double report*) (ml file_content) in file_content |> Input.source_explode |> Source.of_list |> Source.source Symbol_Pos.stopper (Scan.bulk (Symbol_Pos.scan_comment "" >> (C_Scan.Left o pair true) || Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol) >> (C_Scan.Left o pair false) || Scan.one (not o Symbol_Pos.is_eof) >> C_Scan.Right)) |> Source.exhaust |> drop_prefix (fn C_Scan.Left _ => true | _ => false) |> drop_suffix (fn C_Scan.Left (false, _) => true | _ => false) |> maps (fn C_Scan.Left (_, x) => x | C_Scan.Right x => [x]) |> Symbol_Pos.implode |> enclose "\n" "\n" |> cartouche - |> Thy_Output.output_source ctxt - |> Thy_Output.isabelle ctxt + |> Document_Output.output_source ctxt + |> Document_Output.isabelle ctxt end); fun ml_enclose bg en source = ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en; in val _ = Theory.setup (ml_text \<^binding>\ML_file\ (ml_enclose "" "")); end; end; \ subsection \Loading the Grammar Simulator\ text \ The parser consists of a generic module \<^file>\../../src_ext/mlton/lib/mlyacc-lib/base.sig\, which interprets an automata-like format generated from ML-Yacc. \ ML_file "../../src_ext/mlton/lib/mlyacc-lib/base.sig" \ \\<^ML_file>\../../src_ext/mlton/lib/mlyacc-lib/base.sig\\ ML_file "../../src_ext/mlton/lib/mlyacc-lib/join.sml" \ \\<^ML_file>\../../src_ext/mlton/lib/mlyacc-lib/join.sml\\ ML_file "../../src_ext/mlton/lib/mlyacc-lib/lrtable.sml" \ \\<^ML_file>\../../src_ext/mlton/lib/mlyacc-lib/lrtable.sml\\ ML_file "../../src_ext/mlton/lib/mlyacc-lib/stream.sml" \ \\<^ML_file>\../../src_ext/mlton/lib/mlyacc-lib/stream.sml\\ ML_file "../../src_ext/mlton/lib/mlyacc-lib/parser1.sml" \ \\<^ML_file>\../../src_ext/mlton/lib/mlyacc-lib/parser1.sml\\ subsection \Loading the Generated Grammar (SML signature)\ ML_file "../generated/c_grammar_fun.grm.sig" subsection \Overloading Grammar Rules (Optional Part)\ ML \ \\<^file>\../generated/c_grammar_fun.grm.sml\\ \ structure C_Grammar_Rule_Wrap_Overloading = struct open C_Grammar_Rule_Lib fun update_env_bottom_up f x arg = ((), C_Env.map_env_lang_tree (f x) arg) fun update_env_top_down f x = pair () ##> (fn arg => C_Env_Ext.map_output_env (K (SOME (f x (#env_lang arg)))) arg) (*type variable (report bound)*) val specifier3 : (CDeclSpec list) -> unit monad = update_env_bottom_up (fn l => fn env_lang => fn env_tree => ( env_lang , fold let open C_Ast in fn CTypeSpec0 (CTypeDef0 (Ident0 (_, i, node), _)) => let val name = ident_decode i val pos1 = [decode_error' node |> #1] in C_Env.map_reports_text (markup_tvar (Right (pos1, Symtab.lookup (C_Env_Ext.get_tyidents'_typedef env_lang) name)) pos1 name) end | _ => I end l env_tree)) val declaration_specifier3 : (CDeclSpec list) -> unit monad = specifier3 val type_specifier3 : (CDeclSpec list) -> unit monad = specifier3 (*basic variable (report bound)*) val primary_expression1 : (CExpr) -> unit monad = update_env_bottom_up (fn e => fn env_lang => fn env_tree => ( env_lang , let open C_Ast in fn CVar0 (Ident0 (_, i, node), _) => let val name = ident_decode i val pos1 = [decode_error' node |> #1] in C_Env.map_reports_text (markup_var (Right (pos1, Symtab.lookup (C_Env_Ext.get_idents' env_lang) name)) pos1 name) end | _ => I end e env_tree)) (*basic variable, parameter functions (report bound)*) val declarator1 : (CDeclrR) -> unit monad = update_env_bottom_up (fn d => fn env_lang => fn env_tree => ( env_lang , let open C_Ast fun markup markup_var params = pair Symtab.empty #> fold (fn (Ident0 (_, i, node), params, ret) => fn (env_lang, env_tree) => let val name = ident_decode i val pos = [decode_error' node |> #1] val data = ( pos , serial () , {global = false, params = params, ret = C_Env.Parsed ret}) in ( env_lang |> Symtab.update (name, data) , env_tree |> C_Env.map_reports_text (markup_var (Left (data, C_Env_Ext.list_lookup env_lang name)) pos name)) end) (ident_of_decl params) #> #2 in fn CDeclrR0 (_, param0, _, _, _) => (case rev param0 of CFunDeclr0 (params, _, _) :: param0 => pair param0 o markup markup_var_bound params | param0 => pair param0) #-> fold (fn CFunDeclr0 (params, _, _) => markup markup_var_improper params | _ => I) end d env_tree)) (*old style syntax for functions (legacy feature)*) val external_declaration1 : (CExtDecl) -> unit monad = update_env_bottom_up (fn f => fn env_lang => fn env_tree => ( env_lang , let open C_Ast in fn CFDefExt0 (CFunDef0 (_, _, l, _, node)) => if null l then I else tap (fn _ => legacy_feature ("Scope analysing for old function syntax not implemented" ^ Position.here (decode_error' node |> #1))) | _ => I end f env_tree)) (*(type) enum, struct, union (report define & report bound)*) fun report_enum_bound i' node env_lang = let open C_Ast val name = ident_decode i' val pos1 = [decode_error' node |> #1] in C_Env.map_reports_text (markup_var_enum (Right (pos1, Symtab.lookup (C_Env_Ext.get_tyidents'_enum env_lang) name)) pos1 name) end local val look_tyidents'_enum = C_Env_Ext.list_lookup o C_Env_Ext.get_tyidents'_enum val declaration : (CDecl) -> unit monad = update_env_bottom_up (fn decl => fn env_lang => fn env_tree => let open C_Ast in fn CDecl0 (l, _, _) => fold (fn CTypeSpec0 (CEnumType0 (CEnum0 (Some (Ident0 (_, i, node)), body, _, _), _)) => (case body of None => (fn (env_lang, env_tree) => (env_lang, report_enum_bound i node env_lang env_tree)) | Some _ => fn (env_lang, env_tree) => let val name = ident_decode i val pos1 = [decode_error' node |> #1] val data = (pos1, serial (), null (C_Env.get_scopes env_lang)) in ( C_Env_Ext.map_tyidents'_enum (Symtab.update (name, data)) env_lang , C_Env.map_reports_text (markup_var_enum (Left (data, look_tyidents'_enum env_lang name)) pos1 name) env_tree) end) | _ => I) l | _ => I end decl (env_lang, env_tree)) in val declaration1 = declaration val declaration2 = declaration val declaration3 = declaration end (*(basic) enum, struct, union (report define)*) local val enumerator : ( ( Ident * CExpr Maybe ) ) -> unit monad = update_env_bottom_up (fn id => fn env_lang => let open C_Ast in fn (ident as Ident0 (_, _, node), _) => C_Grammar_Rule_Lib.shadowTypedef0' (C_Env.Parsed [CTypeSpec0 (CIntType0 node)]) (null (C_Env.get_scopes env_lang)) (ident, []) env_lang end id) in val enumerator1 = enumerator val enumerator2 = enumerator val enumerator3 = enumerator val enumerator4 = enumerator end (*(type) enum, struct, union (report bound)*) local fun declaration_specifier env_lang = let open C_Ast in fold (fn CTypeSpec0 (CEnumType0 (CEnum0 (Some (Ident0 (_, i, node)), _, _, _), _)) => report_enum_bound i node env_lang | _ => I) end in val declaration_specifier2 : (CDeclSpec list) -> unit monad = update_env_bottom_up (fn d => fn env_lang => fn env_tree => let open C_Ast in ( env_lang , env_tree |> (if exists (fn CStorageSpec0 (CTypedef0 _) => true | _ => false) d then I else declaration_specifier env_lang d)) end) local val f_definition : (CFunDef) -> unit monad = update_env_bottom_up (fn d => fn env_lang => fn env_tree => ( env_lang , let open C_Ast in fn CFunDef0 (l, _, _, _, _) => declaration_specifier env_lang l end d env_tree)) in val function_definition4 = f_definition val nested_function_definition2 = f_definition end local val parameter_type_list : ( ( CDecl list * Bool ) ) -> unit monad = update_env_bottom_up (fn d => fn env_lang => fn env_tree => ( env_lang , let open C_Ast in #1 #> fold (fn CDecl0 (l, _, _) => declaration_specifier env_lang l | _ => I) end d env_tree)) in val parameter_type_list2 = parameter_type_list val parameter_type_list3 = parameter_type_list end end end \ ML \ \\<^file>\../generated/c_grammar_fun.grm.sml\\ \ structure C_Grammar_Rule_Wrap = struct open C_Grammar_Rule_Wrap open C_Grammar_Rule_Wrap_Overloading end \ subsection \Loading the Generated Grammar (SML structure)\ ML_file "../generated/c_grammar_fun.grm.sml" subsection \Grammar Initialization\ subsubsection \Functor Application\ ML \ \\<^file>\../generated/c_grammar_fun.grm.sml\\ \ structure C_Grammar = C_Grammar_Fun (structure Token = LALR_Parser_Eval.Token) \ subsubsection \Mapping Strings to Structured Tokens\ ML \ \\<^file>\../generated/c_grammar_fun.grm.sml\\ \ structure C_Grammar_Tokens = struct local open C_Grammar.Tokens in fun token_of_string error ty_ClangCVersion ty_cChar ty_cFloat ty_cInteger ty_cString ty_ident ty_string a1 a2 = fn "(" => x28 (ty_string, a1, a2) | ")" => x29 (ty_string, a1, a2) | "[" => x5b (ty_string, a1, a2) | "]" => x5d (ty_string, a1, a2) | "->" => x2d_x3e (ty_string, a1, a2) | "." => x2e (ty_string, a1, a2) | "!" => x21 (ty_string, a1, a2) | "~" => x7e (ty_string, a1, a2) | "++" => x2b_x2b (ty_string, a1, a2) | "--" => x2d_x2d (ty_string, a1, a2) | "+" => x2b (ty_string, a1, a2) | "-" => x2d (ty_string, a1, a2) | "*" => x2a (ty_string, a1, a2) | "/" => x2f (ty_string, a1, a2) | "%" => x25 (ty_string, a1, a2) | "&" => x26 (ty_string, a1, a2) | "<<" => x3c_x3c (ty_string, a1, a2) | ">>" => x3e_x3e (ty_string, a1, a2) | "<" => x3c (ty_string, a1, a2) | "<=" => x3c_x3d (ty_string, a1, a2) | ">" => x3e (ty_string, a1, a2) | ">=" => x3e_x3d (ty_string, a1, a2) | "==" => x3d_x3d (ty_string, a1, a2) | "!=" => x21_x3d (ty_string, a1, a2) | "^" => x5e (ty_string, a1, a2) | "|" => x7c (ty_string, a1, a2) | "&&" => x26_x26 (ty_string, a1, a2) | "||" => x7c_x7c (ty_string, a1, a2) | "?" => x3f (ty_string, a1, a2) | ":" => x3a (ty_string, a1, a2) | "=" => x3d (ty_string, a1, a2) | "+=" => x2b_x3d (ty_string, a1, a2) | "-=" => x2d_x3d (ty_string, a1, a2) | "*=" => x2a_x3d (ty_string, a1, a2) | "/=" => x2f_x3d (ty_string, a1, a2) | "%=" => x25_x3d (ty_string, a1, a2) | "&=" => x26_x3d (ty_string, a1, a2) | "^=" => x5e_x3d (ty_string, a1, a2) | "|=" => x7c_x3d (ty_string, a1, a2) | "<<=" => x3c_x3c_x3d (ty_string, a1, a2) | ">>=" => x3e_x3e_x3d (ty_string, a1, a2) | "," => x2c (ty_string, a1, a2) | ";" => x3b (ty_string, a1, a2) | "{" => x7b (ty_string, a1, a2) | "}" => x7d (ty_string, a1, a2) | "..." => x2e_x2e_x2e (ty_string, a1, a2) | x => let val alignof = alignof (ty_string, a1, a2) val alignas = alignas (ty_string, a1, a2) val atomic = x5f_Atomic (ty_string, a1, a2) val asm = asm (ty_string, a1, a2) val auto = auto (ty_string, a1, a2) val break = break (ty_string, a1, a2) val bool = x5f_Bool (ty_string, a1, a2) val case0 = case0 (ty_string, a1, a2) val char = char (ty_string, a1, a2) val const = const (ty_string, a1, a2) val continue = continue (ty_string, a1, a2) val complex = x5f_Complex (ty_string, a1, a2) val default = default (ty_string, a1, a2) val do0 = do0 (ty_string, a1, a2) val double = double (ty_string, a1, a2) val else0 = else0 (ty_string, a1, a2) val enum = enum (ty_string, a1, a2) val extern = extern (ty_string, a1, a2) val float = float (ty_string, a1, a2) val for0 = for0 (ty_string, a1, a2) val generic = x5f_Generic (ty_string, a1, a2) val goto = goto (ty_string, a1, a2) val if0 = if0 (ty_string, a1, a2) val inline = inline (ty_string, a1, a2) val int = int (ty_string, a1, a2) val int128 = x5f_x5f_int_x31_x32_x38 (ty_string, a1, a2) val long = long (ty_string, a1, a2) val label = x5f_x5f_label_x5f_x5f (ty_string, a1, a2) val noreturn = x5f_Noreturn (ty_string, a1, a2) val nullable = x5f_Nullable (ty_string, a1, a2) val nonnull = x5f_Nonnull (ty_string, a1, a2) val register = register (ty_string, a1, a2) val restrict = restrict (ty_string, a1, a2) val return0 = return0 (ty_string, a1, a2) val short = short (ty_string, a1, a2) val signed = signed (ty_string, a1, a2) val sizeof = sizeof (ty_string, a1, a2) val static = static (ty_string, a1, a2) val staticassert = x5f_Static_assert (ty_string, a1, a2) val struct0 = struct0 (ty_string, a1, a2) val switch = switch (ty_string, a1, a2) val typedef = typedef (ty_string, a1, a2) val typeof = typeof (ty_string, a1, a2) val thread = x5f_x5f_thread (ty_string, a1, a2) val union = union (ty_string, a1, a2) val unsigned = unsigned (ty_string, a1, a2) val void = void (ty_string, a1, a2) val volatile = volatile (ty_string, a1, a2) val while0 = while0 (ty_string, a1, a2) val cchar = cchar (ty_cChar, a1, a2) val cint = cint (ty_cInteger, a1, a2) val cfloat = cfloat (ty_cFloat, a1, a2) val cstr = cstr (ty_cString, a1, a2) val ident = ident (ty_ident, a1, a2) val tyident = tyident (ty_ident, a1, a2) val attribute = x5f_x5f_attribute_x5f_x5f (ty_string, a1, a2) val extension = x5f_x5f_extension_x5f_x5f (ty_string, a1, a2) val real = x5f_x5f_real_x5f_x5f (ty_string, a1, a2) val imag = x5f_x5f_imag_x5f_x5f (ty_string, a1, a2) val builtinvaarg = x5f_x5f_builtin_va_arg (ty_string, a1, a2) val builtinoffsetof = x5f_x5f_builtin_offsetof (ty_string, a1, a2) val builtintypescompatiblep = x5f_x5f_builtin_types_compatible_p (ty_string, a1, a2) val clangcversion = clangcversion (ty_ClangCVersion, a1, a2) in case x of "_Alignas" => alignas | "_Alignof" => alignof | "__alignof" => alignof | "alignof" => alignof | "__alignof__" => alignof | "__asm" => asm | "asm" => asm | "__asm__" => asm | "_Atomic" => atomic | "__attribute" => attribute | "__attribute__" => attribute | "auto" => auto | "_Bool" => bool | "break" => break | "__builtin_offsetof" => builtinoffsetof | "__builtin_types_compatible_p" => builtintypescompatiblep | "__builtin_va_arg" => builtinvaarg | "case" => case0 | "char" => char | "_Complex" => complex | "__complex__" => complex | "__const" => const | "const" => const | "__const__" => const | "continue" => continue | "default" => default | "do" => do0 | "double" => double | "else" => else0 | "enum" => enum | "__extension__" => extension | "extern" => extern | "float" => float | "for" => for0 | "_Generic" => generic | "goto" => goto | "if" => if0 | "__imag" => imag | "__imag__" => imag | "__inline" => inline | "inline" => inline | "__inline__" => inline | "int" => int | "__int128" => int128 | "__label__" => label | "long" => long | "_Nonnull" => nonnull | "__nonnull" => nonnull | "_Noreturn" => noreturn | "_Nullable" => nullable | "__nullable" => nullable | "__real" => real | "__real__" => real | "register" => register | "__restrict" => restrict | "restrict" => restrict | "__restrict__" => restrict | "return" => return0 | "short" => short | "__signed" => signed | "signed" => signed | "__signed__" => signed | "sizeof" => sizeof | "static" => static | "_Static_assert" => staticassert | "struct" => struct0 | "switch" => switch | "__thread" => thread | "_Thread_local" => thread | "typedef" => typedef | "__typeof" => typeof | "typeof" => typeof | "__typeof__" => typeof | "union" => union | "unsigned" => unsigned | "void" => void | "__volatile" => volatile | "volatile" => volatile | "__volatile__" => volatile | "while" => while0 | _ => error end end end \ end diff --git a/thys/Refine_Imperative_HOL/Sepref_Combinator_Setup.thy b/thys/Refine_Imperative_HOL/Sepref_Combinator_Setup.thy --- a/thys/Refine_Imperative_HOL/Sepref_Combinator_Setup.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Combinator_Setup.thy @@ -1,581 +1,581 @@ section \Setup for Combinators\ theory Sepref_Combinator_Setup imports Sepref_Rules Sepref_Monadify keywords "sepref_register" :: thy_decl and "sepref_decl_intf" :: thy_decl begin subsection \Interface Types\ text \ This tool allows the declaration of interface types. An interface type is a new type, and a rewriting rule to an existing (logic) type, which is used to encode objects of the interface type in the logic. \ context begin private definition T :: "string \ unit list \ unit" where "T _ _ \ ()" private lemma unit_eq: "(a::unit) \ b" by simp named_theorems "__itype_rewrite" ML \ signature SEPREF_INTF_TYPES = sig (* Declare new interface type *) val decl_intf_type_cmd: ((string list * binding) * mixfix) * string -> local_theory -> local_theory (* Register interface type rewrite rule *) val register_itype_rewrite: typ -> typ -> Proof.context -> local_theory (* Convert interface type to logical type*) val norm_intf_type: Proof.context -> typ -> typ (* Check whether interface type matches operation's type *) val check_intf_type: Proof.context -> typ -> typ -> bool (* Invoke msg with (normalized) non-matching types in case of no-match *) val check_intf_type_msg: (typ * typ -> unit) -> Proof.context -> typ -> typ -> unit (* Trigger error message if no match *) val check_intf_type_err: Proof.context -> typ -> typ -> unit end structure Sepref_Intf_Types: SEPREF_INTF_TYPES = struct fun t2t (Type(name,args)) = @{term T} $HOLogic.mk_string name $HOLogic.mk_list @{typ unit} (map t2t args) | t2t (TFree (name,_)) = Var (("F"^name,0),HOLogic.unitT) | t2t (TVar ((name,i),_)) = Var (("V"^name,i),HOLogic.unitT) fun tt2 (t as (Var ((name,i),_))) = if match_string "F*" name then TFree (unprefix "F" name, dummyS) else if match_string "V*" name then TVar ((unprefix "V" name,i), dummyS) else raise TERM("tt2: Invalid var",[t]) | tt2 @{mpat "T ?name ?args"} = Type (HOLogic.dest_string name, HOLogic.dest_list args |> map tt2) | tt2 t = raise TERM("tt2: Invalid",[t]) fun mk_t2t_rew ctxt T1 T2 = let fun chk_vars T = exists_subtype is_TVar T andalso raise TYPE("Type must not contain schematics",[T],[]) val _ = chk_vars T1 val _ = chk_vars T2 val free1 = Term.add_tfreesT T1 [] val free2 = Term.add_tfreesT T2 [] val _ = subset (=) (free2,free1) orelse raise TYPE("Free variables on RHS must also occur on LHS",[T1,T2],[]) in Thm.instantiate' [] [ t2t T1 |> Thm.cterm_of ctxt |> SOME, t2t T2 |> Thm.cterm_of ctxt |> SOME ] @{thm unit_eq} end fun register_itype_rewrite T1 T2 lthy = lthy |> Local_Theory.note ((Binding.empty,@{attributes ["__itype_rewrite"]}),[mk_t2t_rew lthy T1 T2]) |> #2 val decl_intf_type_parser = Parse.type_args -- Parse.binding -- Parse.opt_mixfix --| @{keyword "is"} -- Parse.typ fun decl_intf_type_cmd (((args,a),mx),T2_raw) lthy = let val (T1,lthy) = Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) lthy val T2 = Syntax.read_typ lthy T2_raw in register_itype_rewrite T1 T2 lthy end fun norm_intf_typet ctxt T = let val rew_rls = Named_Theorems.get ctxt @{named_theorems "__itype_rewrite"} in t2t T |> Thm.cterm_of ctxt |> Drule.mk_term |> Local_Defs.unfold0 ctxt rew_rls |> Drule.dest_term |> Thm.term_of end fun norm_intf_type ctxt T = norm_intf_typet ctxt T |> tt2 fun check_intf_type ctxt iT cT = let val it = norm_intf_typet ctxt iT val ct = t2t cT val thy = Proof_Context.theory_of ctxt in Pattern.matches thy (it,ct) end fun check_intf_type_msg msg ctxt iT cT = let val it = norm_intf_typet ctxt iT val ct = t2t cT val thy = Proof_Context.theory_of ctxt in if Pattern.matches thy (it,ct) then () else msg (tt2 it, tt2 ct) end fun check_intf_type_err ctxt iT cT = let fun msg (iT',cT') = Pretty.block [ Pretty.str "Interface type and logical type do not match", Pretty.fbrk, Pretty.str "Interface: ",Syntax.pretty_typ ctxt iT, Pretty.brk 1, Pretty.str " is ", Syntax.pretty_typ ctxt iT', Pretty.fbrk, Pretty.str "Logical: ",Syntax.pretty_typ ctxt cT, Pretty.brk 1, Pretty.str " is ", Syntax.pretty_typ ctxt cT', Pretty.fbrk ] |> Pretty.string_of |> error in check_intf_type_msg msg ctxt iT cT end val _ = Outer_Syntax.local_theory @{command_keyword "sepref_decl_intf"} "Declare interface type" ( decl_intf_type_parser >> decl_intf_type_cmd); end \ end subsection \Rewriting Inferred Interface Types\ definition map_type_eq :: "'a itself \ 'b itself \ bool" (infixr "\\<^sub>n\<^sub>t" 60) where [simp]: "map_type_eq _ _ \ True" lemma map_type_eqI: "map_type_eq L R" by auto named_theorems_rev map_type_eqs subsection \ML-Code\ context begin private lemma start_eval: "x \ SP x" by auto private lemma add_eval: "f x \ (\)$(EVAL$x)$(\\<^sub>2x. f x)" by auto private lemma init_mk_arity: "f \ id (SP f)" by simp private lemma add_mk_arity: "id f \ (\\<^sub>2x. id (f$x))" by auto private lemma finish_mk_arity: "id f \ f" by simp ML \ structure Sepref_Combinator_Setup = struct (* Check whether this term is a valid abstract operation *) fun is_valid_abs_op _ (Const _) = true | is_valid_abs_op ctxt (Free (name,_)) = Variable.is_fixed ctxt name | is_valid_abs_op _ @{mpat "PR_CONST _"} = true | is_valid_abs_op _ _ = false fun mk_itype ctxt t tyt = let val cert = Thm.cterm_of ctxt val t = cert t val tyt = cert tyt in Drule.infer_instantiate' ctxt [SOME t, SOME tyt] @{thm itypeI} end (* Generate mcomb-theorem, required for monadify transformation. t$x1$...$xn = x1\EVAL x1; ...; xn\EVAL xn; SP (t$x1$...$xn) *) fun mk_mcomb ctxt t n = let val T = fastype_of t val (argsT,_) = strip_type T val _ = length argsT >= n orelse raise TERM("Too few arguments",[t]) val effT = take n argsT val orig_ctxt = ctxt val names = map (fn i => "x"^string_of_int i) (1 upto n) val (names,ctxt) = Variable.variant_fixes names ctxt val vars = map Free (names ~~ effT) val lhs = Autoref_Tagging.list_APP (t,vars) |> Thm.cterm_of ctxt fun add_EVAL x thm = case Thm.prop_of thm of @{mpat "_ \ ?rhs"} => let val f = lambda x rhs |> Thm.cterm_of ctxt val x = Thm.cterm_of ctxt x val eval_thm = Drule.infer_instantiate' ctxt [SOME f, SOME x] @{thm add_eval} val thm = @{thm transitive} OF [thm,eval_thm] in thm end | _ => raise THM ("mk_mcomb internal: Expected lhs==rhs",~1,[thm]) val thm = Drule.infer_instantiate' ctxt [SOME lhs] @{thm start_eval} val thm = fold add_EVAL (rev vars) thm val thm = singleton (Proof_Context.export ctxt orig_ctxt) thm in thm end; (* Generate arity-theorem: t = \x1...xn. SP t$x1$...$xn *) fun mk_arity ctxt t n = let val t = Thm.cterm_of ctxt t val thm = Drule.infer_instantiate' ctxt [SOME t] @{thm init_mk_arity} val add_mk_arity = Conv.fconv_rule ( Refine_Util.ftop_conv (K (Conv.rewr_conv @{thm add_mk_arity})) ctxt) val thm = funpow n add_mk_arity thm val thm = Conv.fconv_rule ( Refine_Util.ftop_conv (K (Conv.rewr_conv @{thm finish_mk_arity})) ctxt) thm in thm end; datatype opkind = PURE | COMB fun analyze_decl c tyt = let fun add_tcons_of (Type (name,args)) l = fold add_tcons_of args (name::l) | add_tcons_of _ l = l fun all_tcons_of P T = forall P (add_tcons_of T []) val T = Logic.dest_type tyt val (argsT,resT) = strip_type T val _ = forall (all_tcons_of (fn tn => tn <> @{type_name nres})) argsT orelse raise TYPE ( "Arguments contain nres-type " ^ "(currently not supported by this attribute)", argsT,[c,tyt]) val kind = case resT of Type (@{type_name nres},_) => COMB | T => let val _ = all_tcons_of (fn tn => tn <> @{type_name nres}) T orelse raise TYPE ( "Result contains inner nres-type", argsT,[c,tyt]) in PURE end in (kind,(argsT,resT)) end fun analyze_itype_thm thm = case Thm.prop_of thm of @{mpat (typs) "Trueprop (intf_type ?c (_::?'v_T itself))"} => let val tyt = Logic.mk_type T val (kind,(argsT,resT)) = analyze_decl c tyt in (c,kind,(argsT,resT)) end | _ => raise THM("Invalid itype-theorem",~1,[thm]) (*fun register_combinator itype_thm context = let val ctxt = Context.proof_of context val (t,kind,(argsT,_)) = analyze_itype_thm itype_thm val n = length argsT in case kind of PURE => context |> Named_Theorems_Rev.add_thm @{named_theorems_rev id_rules} itype_thm | COMB => let val arity_thm = mk_arity ctxt t n (*val skel_thm = mk_skel ctxt t n*) val mcomb_thm = mk_mcomb ctxt t n in context |> Named_Theorems_Rev.add_thm @{named_theorems_rev id_rules} itype_thm |> Named_Theorems_Rev.add_thm @{named_theorems_rev sepref_monadify_arity} arity_thm |> Named_Theorems_Rev.add_thm @{named_theorems_rev sepref_monadify_comb} mcomb_thm (*|> Named_Theorems_Rev.add_thm @{named_theorems_rev sepref_la_skel} skel_thm*) end end *) fun generate_basename ctxt t = let fun fail () = raise TERM ("Basename generation heuristics failed. Specify a basename.",[t]) fun gb (Const (n,_)) = (* TODO: There should be a cleaner way than handling this on string level!*) n |> space_explode "." |> List.last | gb (@{mpat "PR_CONST ?t"}) = gb t | gb (t as (_$_)) = let val h = head_of t val _ = is_Const h orelse is_Free h orelse fail () in gb h end | gb (Free (n,_)) = if Variable.is_fixed ctxt n then n else fail () | gb _ = fail () in gb t end fun map_type_raw ctxt rls T = let val thy = Proof_Context.theory_of ctxt fun rewr_this (lhs,rhs) T = let val env = Sign.typ_match thy (lhs,T) Vartab.empty in Envir.norm_type env rhs end fun map_Targs f (Type (name,args)) = Type (name,map f args) | map_Targs _ T = T fun rewr_thiss (r::rls) T = (SOME (rewr_this r T) handle Type.TYPE_MATCH => rewr_thiss rls T) | rewr_thiss [] _ = NONE fun map_type_aux T = let val T = map_Targs map_type_aux T in case rewr_thiss rls T of SOME T => map_type_aux T | NONE => T end in map_type_aux T end fun get_nt_rule thm = case Thm.prop_of thm of @{mpat (typs) "Trueprop (map_type_eq (_::?'v_L itself) (_::?'v_R itself))"} => let val Lvars = Term.add_tvar_namesT L [] val Rvars = Term.add_tvar_namesT R [] val _ = subset (=) (Rvars, Lvars) orelse ( let val frees = subtract (=) Lvars Rvars |> map (Term.string_of_vname) |> Pretty.str_list "[" "]" |> Pretty.string_of in raise THM ("Free variables on RHS: "^frees,~1,[thm]) end) in (L,R) end | _ => raise THM("No map_type_eq theorem",~1,[thm]) fun map_type ctxt T = let val rls = Named_Theorems_Rev.get ctxt @{named_theorems_rev map_type_eqs} |> map get_nt_rule in map_type_raw ctxt rls T end fun read_term_type ts tys lthy = case tys of SOME ty => let val ty = Syntax.read_typ lthy ty val ctxt = Variable.declare_typ ty lthy val t = Syntax.read_term ctxt ts val ctxt = Variable.declare_term t ctxt in ((t,ty),ctxt) end | NONE => let val t = Syntax.read_term lthy ts val ctxt = Variable.declare_term t lthy val tyt = fastype_of t |> map_type ctxt |> Logic.mk_type val tyt = tyt |> singleton (Variable.export_terms ctxt lthy) val (tyt,ctxt) = yield_singleton (Variable.import_terms true) tyt ctxt val ty = Logic.dest_type tyt in ((t,ty),ctxt) end fun check_type_intf ctxt Tc Ti = let fun type2term (TFree (name,_)) = Var (("F"^name,0),HOLogic.unitT) | type2term (TVar ((name,i),_)) = Var (("V"^name,i),HOLogic.unitT) | type2term (Type (@{type_name "fun"},[T1,T2])) = Free ("F",HOLogic.unitT --> HOLogic.unitT --> HOLogic.unitT) $type2term T1$type2term T2 | type2term (Type (name,argsT)) = let val args = map type2term argsT val n = length args val T = replicate n HOLogic.unitT ---> HOLogic.unitT val v = Var (("T"^name,0),T) in list_comb (v, args) end val c = type2term Tc val i = type2term Ti val thy = Proof_Context.theory_of ctxt in Pattern.matches thy (i,c) end (* Import all terms into context, with disjoint free variables *) fun import_terms_disj ts ctxt = let fun exp ctxt t = let val new_ctxt = Variable.declare_term t ctxt val t = singleton (Variable.export_terms new_ctxt ctxt) t in t end val ts = map (exp ctxt) ts fun cons_fst f a (l,b) = let val (a,b) = f a b in (a::l,b) end val (ts,ctxt) = fold_rev (cons_fst (yield_singleton (Variable.import_terms true))) ts ([],ctxt) in (ts,ctxt) end type reg_thms = { itype_thm: thm, arity_thm: thm option, mcomb_thm: thm option } fun cr_reg_thms t ty ctxt = let val orig_ctxt = ctxt val tyt = Logic.mk_type ty val ([t,tyt],ctxt) = import_terms_disj [t,tyt] ctxt val (kind,(argsT,_)) = analyze_decl t tyt val n = length argsT val _ = Sepref_Intf_Types.check_intf_type_err ctxt ty (fastype_of t) val _ = is_valid_abs_op ctxt t orelse raise TERM("Malformed abstract operation. Use PR_CONST for complex terms.",[t]) val itype_thm = mk_itype ctxt t tyt |> singleton (Variable.export ctxt orig_ctxt) in case kind of PURE => {itype_thm = itype_thm, arity_thm = NONE, mcomb_thm = NONE} | COMB => let val arity_thm = mk_arity ctxt t n |> singleton (Variable.export ctxt orig_ctxt) val mcomb_thm = mk_mcomb ctxt t n |> singleton (Variable.export ctxt orig_ctxt) in {itype_thm = itype_thm, arity_thm = SOME arity_thm, mcomb_thm = SOME mcomb_thm} end end fun gen_pr_const_pat ctxt t = if is_valid_abs_op ctxt t then (NONE,t) else let val ct = Thm.cterm_of ctxt t val thm = Drule.infer_instantiate' ctxt [SOME ct] @{thm UNPROTECT_def[symmetric]} |> Conv.fconv_rule (Conv.arg1_conv (Id_Op.protect_conv ctxt)) in (SOME thm,@{mk_term "PR_CONST ?t"}) end fun sepref_register_single basename t ty lthy = let fun mk_qualified basename q = Binding.qualify true basename (Binding.name q); fun do_note _ _ NONE = I | do_note q attrs (SOME thm) = Local_Theory.note ((mk_qualified basename q,attrs),[thm]) #> snd val (pat_thm,t) = gen_pr_const_pat lthy t val {itype_thm, arity_thm, mcomb_thm} = cr_reg_thms t ty lthy val lthy = lthy |> do_note "pat" @{attributes [def_pat_rules]} pat_thm |> do_note "itype" @{attributes [id_rules]} (SOME itype_thm) |> do_note "arity" @{attributes [sepref_monadify_arity]} arity_thm |> do_note "mcomb" @{attributes [sepref_monadify_comb]} mcomb_thm in (((arity_thm,mcomb_thm),itype_thm),lthy) end fun sepref_register_single_cmd ((basename,ts),tys) lthy = let val t = Syntax.read_term lthy ts val ty = map_option (Syntax.read_typ lthy) tys val ty = case ty of SOME ty => ty | NONE => fastype_of t |> map_type lthy val basename = case basename of NONE => generate_basename lthy t | SOME n => n val ((_,itype_thm),lthy) = sepref_register_single basename t ty lthy - val _ = Thy_Output.pretty_thm lthy itype_thm |> Pretty.string_of |> writeln + val _ = Document_Output.pretty_thm lthy itype_thm |> Pretty.string_of |> writeln in lthy end val sepref_register_cmd = fold sepref_register_single_cmd val sepref_register_parser = Scan.repeat1 ( Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term -- Scan.option (@{keyword "::"} |-- Parse.typ) ) val _ = Outer_Syntax.local_theory @{command_keyword "sepref_register"} "Register operation for sepref" ( sepref_register_parser >> sepref_register_cmd); val sepref_register_adhoc_parser = Scan.repeat1 ( Args.term -- Scan.option (Scan.lift (Args.$$$ "::") |-- Args.typ) ) fun sepref_register_adhoc_single (t,ty) context = let val ctxt = Context.proof_of context (* TODO: Map-type probably not clean, as it draws info from (current) context, which may have changed if registered elsewhere ... *) val ty = case ty of SOME ty => ty | NONE => fastype_of t |> map_type ctxt val (pat_thm,t) = gen_pr_const_pat ctxt t val {itype_thm, arity_thm, mcomb_thm} = cr_reg_thms t ty ctxt fun app _ NONE = I | app attr (SOME thm) = Thm.apply_attribute attr thm #> snd in context |> app (Named_Theorems_Rev.add @{named_theorems_rev def_pat_rules}) pat_thm |> app (Named_Theorems_Rev.add @{named_theorems_rev id_rules}) (SOME itype_thm) |> app (Named_Theorems_Rev.add @{named_theorems_rev sepref_monadify_arity}) arity_thm |> app (Named_Theorems_Rev.add @{named_theorems_rev sepref_monadify_comb}) mcomb_thm end val sepref_register_adhoc = fold sepref_register_adhoc_single fun sepref_register_adhoc_attr ttys = Thm.declaration_attribute (K (sepref_register_adhoc ttys)) val sepref_register_adhoc_attr_decl = sepref_register_adhoc_parser >> sepref_register_adhoc_attr end \ end attribute_setup sepref_register_adhoc = Sepref_Combinator_Setup.sepref_register_adhoc_attr_decl \Register operations in ad-hoc manner. Improper if this gets exported!\ (* attribute_setup sepref_register_combinator = \Scan.succeed (Thm.declaration_attribute Sepref_Combinator_Setup.register_combinator)\ \Register combinator by its itype-rule. Set up itype,skel,arity, and mcomb rules.\ *) subsection \Obsolete Manual Setup Rules\ lemma mk_mcomb1: "\c. c$x1 \ (\)$(EVAL$x1)$(\\<^sub>2x1. SP (c$x1))" and mk_mcomb2: "\c. c$x1$x2 \ (\)$(EVAL$x1)$(\\<^sub>2x1. (\)$(EVAL$x2)$(\\<^sub>2x2. SP (c$x1$x2)))" and mk_mcomb3: "\c. c$x1$x2$x3 \ (\)$(EVAL$x1)$(\\<^sub>2x1. (\)$(EVAL$x2)$(\\<^sub>2x2. (\)$(EVAL$x3)$(\\<^sub>2x3. SP (c$x1$x2$x3))))" by auto end diff --git a/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy b/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy --- a/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy +++ b/thys/Refine_Imperative_HOL/Sepref_Intf_Util.thy @@ -1,1378 +1,1378 @@ section \Utilities for Interface Specifications and Implementations\ theory Sepref_Intf_Util imports Sepref_Rules Sepref_Translate "Lib/Term_Synth" Sepref_Combinator_Setup "Lib/Concl_Pres_Clarification" keywords "sepref_decl_op" :: thy_goal and "sepref_decl_impl" :: thy_goal begin subsection \Relation Interface Binding\ definition INTF_OF_REL :: "('a\'b) set \ 'c itself \ bool" where [simp]: "INTF_OF_REL R I \ True" lemma intf_of_relI: "INTF_OF_REL (R::(_\'a) set) TYPE('a)" by simp declare intf_of_relI[synth_rules] \ \Declare as fallback rule\ lemma [synth_rules]: "INTF_OF_REL unit_rel TYPE(unit)" "INTF_OF_REL nat_rel TYPE(nat)" "INTF_OF_REL int_rel TYPE(int)" "INTF_OF_REL bool_rel TYPE(bool)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\option_rel) TYPE('a option)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\list_rel) TYPE('a list)" "INTF_OF_REL R TYPE('a) \ INTF_OF_REL (\R\nres_rel) TYPE('a nres)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (R\\<^sub>rS) TYPE('a\'b)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (\R,S\sum_rel) TYPE('a+'b)" "\INTF_OF_REL R TYPE('a); INTF_OF_REL S TYPE('b)\ \ INTF_OF_REL (R\S) TYPE('a\'b)" by simp_all lemma synth_intf_of_relI: "INTF_OF_REL R I \ SYNTH_TERM R I" by simp subsection \Operations with Precondition\ definition mop :: "('a\bool) \ ('a\'b nres) \ 'a \ 'b nres" \ \Package operation with precondition\ where [simp]: "mop P f \ \x. ASSERT (P x) \ f x" lemma param_op_mop_iff: assumes "(Q,P)\R\bool_rel" shows "(f, g) \ [P]\<^sub>f R \ \S\nres_rel \ (mop Q f, mop P g) \ R \\<^sub>f \S\nres_rel " using assms by (auto simp: mop_def fref_def pw_nres_rel_iff refine_pw_simps dest: fun_relD) lemma param_mopI: assumes "(f,g) \ [P]\<^sub>f R \ \S\nres_rel" assumes "(Q,P) \ R \ bool_rel" shows "(mop Q f, mop P g) \ R \\<^sub>f \S\nres_rel" using assms by (simp add: param_op_mop_iff) lemma mop_spec_rl: "P x \ mop P f x \ f x" by simp lemma mop_spec_rl_from_def: assumes "f \ mop P g" assumes "P x" assumes "g x \ z" shows "f x \ z" using assms mop_spec_rl by simp lemma mop_leof_rl_from_def: assumes "f \ mop P g" assumes "P x \ g x \\<^sub>n z" shows "f x \\<^sub>n z" using assms by (simp add: pw_leof_iff refine_pw_simps) lemma assert_true_bind_conv: "ASSERT True \ m = m" by simp lemmas mop_alt_unfolds = curry_def curry0_def mop_def uncurry_apply uncurry0_apply o_apply assert_true_bind_conv subsection \Constraints\ lemma add_is_pure_constraint: "\PROP P; CONSTRAINT is_pure A\ \ PROP P" . lemma sepref_relpropI: "P R = CONSTRAINT P R" by simp subsubsection \Purity\ lemmas [constraint_simps] = the_pure_pure definition [constraint_abbrevs]: "IS_PURE P R \ is_pure R \ P (the_pure R)" lemma IS_PURE_pureI: "P R \ IS_PURE P (pure R)" by (auto simp: IS_PURE_def) lemma [fcomp_norm_simps]: "CONSTRAINT (IS_PURE \) P \ pure (the_pure P) = P" by (simp add: IS_PURE_def) lemma [fcomp_norm_simps]: "CONSTRAINT (IS_PURE P) A \ P (the_pure A)" by (auto simp: IS_PURE_def) lemma handle_purity1: "CONSTRAINT (IS_PURE \) A \ CONSTRAINT \ (the_pure A)" by (auto simp: IS_PURE_def) lemma handle_purity2: "CONSTRAINT (IS_PURE \) A \ CONSTRAINT is_pure A" by (auto simp: IS_PURE_def) subsection \Composition\ (* TODO/FIXME: Overlaps with FCOMP! *) subsubsection \Preconditions\ definition [simp]: "tcomp_pre Q T P \ \a. Q a \ (\a'. (a', a) \ T \ P a')" definition "and_pre P1 P2 \ \x. P1 x \ P2 x" definition "imp_pre P1 P2 \ \x. P1 x \ P2 x" lemma and_pre_beta: "PP \ P x \ Q x \ PP \ and_pre P Q x" by (auto simp: and_pre_def) lemma imp_pre_beta: "PP \ P x \ Q x \ PP \ imp_pre P Q x" by (auto simp: imp_pre_def) definition "IMP_PRE P1 P2 \ \x. P1 x \ P2 x" lemma IMP_PRED: "IMP_PRE P1 P2 \ P1 x \ P2 x" unfolding IMP_PRE_def by auto lemma IMP_PRE_refl: "IMP_PRE P P" unfolding IMP_PRE_def by auto definition "IMP_PRE_CUSTOM \ IMP_PRE" lemma IMP_PRE_CUSTOMD: "IMP_PRE_CUSTOM P1 P2 \ IMP_PRE P1 P2" by (simp add: IMP_PRE_CUSTOM_def) lemma IMP_PRE_CUSTOMI: "\\x. P1 x \ P2 x\ \ IMP_PRE_CUSTOM P1 P2" by (simp add: IMP_PRE_CUSTOM_def IMP_PRE_def) lemma imp_and_triv_pre: "IMP_PRE P (and_pre (\_. True) P)" unfolding IMP_PRE_def and_pre_def by auto subsubsection \Premises\ definition "ALL_LIST A \ (\x\set A. x)" definition "IMP_LIST A B \ ALL_LIST A \ B" lemma to_IMP_LISTI: "P \ IMP_LIST [] P" by (auto simp: IMP_LIST_def) lemma to_IMP_LIST: "(P \ IMP_LIST Ps Q) \ Trueprop (IMP_LIST (P#Ps) Q)" by (auto simp: IMP_LIST_def ALL_LIST_def intro!: equal_intr_rule) lemma from_IMP_LIST: "Trueprop (IMP_LIST As B) \ (ALL_LIST As \ B)" "(ALL_LIST [] \ B) \ Trueprop B" "(ALL_LIST (A#As) \ B) \ (A \ ALL_LIST As \ B)" by (auto simp: IMP_LIST_def ALL_LIST_def intro!: equal_intr_rule) lemma IMP_LIST_trivial: "IMP_LIST A B \ IMP_LIST A B" . subsubsection \Composition Rules\ lemma hfcomp_tcomp_pre: assumes B: "(g,h) \ [Q]\<^sub>f T \ \U\nres_rel" assumes A: "(f,g) \ [P]\<^sub>a RR' \ S" shows "(f,h) \ [tcomp_pre Q T P]\<^sub>a hrp_comp RR' T \ hr_comp S U" using hfcomp[OF A B] by simp lemma transform_pre_param: assumes A: "IMP_LIST Cns ((f, h) \ [tcomp_pre Q T P]\<^sub>a hrp_comp RR' T \ hr_comp S U)" assumes P: "IMP_LIST Cns ((P,P') \ T \ bool_rel)" assumes C: "IMP_PRE PP' (and_pre P' Q)" shows "IMP_LIST Cns ((f,h) \ [PP']\<^sub>a hrp_comp RR' T \ hr_comp S U)" unfolding from_IMP_LIST apply (rule hfref_cons) apply (rule A[unfolded from_IMP_LIST]) apply assumption apply (drule IMP_PRED[OF C]) using P[unfolded from_IMP_LIST] unfolding and_pre_def apply (auto dest: fun_relD) [] by simp_all lemma hfref_mop_conv: "((g,mop P f) \ [Q]\<^sub>a R \ S) \ (g,f) \ [\x. P x \ Q x]\<^sub>a R \ S" apply (simp add: hfref_to_ASSERT_conv) apply (fo_rule arg_cong fun_cong)+ by (auto intro!: ext simp: pw_eq_iff refine_pw_simps) lemma hfref_op_to_mop: assumes R: "(impl,f) \ [Q]\<^sub>a R \ S" assumes DEF: "mf \ mop P f" assumes C: "IMP_PRE PP' (imp_pre P Q)" shows "(impl,mf) \ [PP']\<^sub>a R \ S" unfolding DEF hfref_mop_conv apply (rule hfref_cons[OF R]) using C by (auto simp: IMP_PRE_def imp_pre_def) lemma hfref_mop_to_op: assumes R: "(impl,mf) \ [Q]\<^sub>a R \ S" assumes DEF: "mf \ mop P f" assumes C: "IMP_PRE PP' (and_pre Q P)" shows "(impl,f) \ [PP']\<^sub>a R \ S" using R unfolding DEF hfref_mop_conv apply (rule hfref_cons) using C apply (auto simp: and_pre_def IMP_PRE_def) done subsubsection \Precondition Simplification\ lemma IMP_PRE_eqI: assumes "\x. P x \ Q x" assumes "CNV P P'" shows "IMP_PRE P' Q" using assms by (auto simp: IMP_PRE_def) lemma simp_and1: assumes "Q \ CNV P P'" assumes "PP \ P' \ Q" shows "PP \ P \ Q" using assms by auto lemma simp_and2: assumes "P \ CNV Q Q'" assumes "PP \ P \ Q'" shows "PP \ P \ Q" using assms by auto lemma triv_and1: "Q \ True \ Q" by blast lemma simp_imp: assumes "P \ CNV Q Q'" assumes "PP \ Q'" shows "PP \ (P \ Q)" using assms by auto lemma CNV_split: assumes "CNV A A'" assumes "CNV B B'" shows "CNV (A \ B) (A' \ B')" using assms by auto lemma CNV_prove: assumes "P" shows "CNV P True" using assms by auto lemma simp_pre_final_simp: assumes "CNV P P'" shows "P' \ P" using assms by auto lemma auto_weaken_pre_uncurry_step': assumes "PROTECT f a \ f'" shows "PROTECT (uncurry f) (a,b) \ f' b" using assms by (auto simp: curry_def dest!: meta_eq_to_obj_eq intro!: eq_reflection) subsection \Protected Constants\ lemma add_PR_CONST_to_def: "x\y \ PR_CONST x \ y" by simp subsection \Rule Collections\ named_theorems_rev sepref_mop_def_thms \Sepref: mop - definition theorems\ named_theorems_rev sepref_fref_thms \Sepref: fref-theorems\ named_theorems sepref_relprops_transform \Sepref: Simp-rules to transform relator properties\ named_theorems sepref_relprops \Sepref: Simp-rules to add CONSTRAINT-tags to relator properties\ named_theorems sepref_relprops_simps \Sepref: Simp-rules to simplify relator properties\ subsubsection \Default Setup\ subsection \ML-Level Declarations\ ML \ signature SEPREF_INTF_UTIL = sig (* Miscellaneous*) val list_filtered_subterms: (term -> 'a option) -> term -> 'a list (* Interface types for relations *) val get_intf_of_rel: Proof.context -> term -> typ (* Constraints *) (* Convert relations to pure assertions *) val to_assns_rl: bool -> Proof.context -> thm -> thm (* Recognize, summarize and simplify CONSTRAINT - premises *) val cleanup_constraints: Proof.context -> thm -> thm (* Preconditions *) (* Simplify precondition. Goal must be in IMP_PRE or IMP_PRE_CUSTOM form. *) val simp_precond_tac: Proof.context -> tactic' (* Configuration options *) val cfg_def: bool Config.T (* decl_op: Define constant *) val cfg_ismop: bool Config.T (* decl_op: Specified term is mop *) val cfg_mop: bool Config.T (* decl_op, decl_impl: Derive mop *) val cfg_rawgoals: bool Config.T (* decl_op, decl_impl: Do not pre-process/solve goals *) (* TODO: Make do_cmd usable from ML-level! *) end structure Sepref_Intf_Util: SEPREF_INTF_UTIL = struct val cfg_debug = Attrib.setup_config_bool @{binding sepref_debug_intf_util} (K false) val dbg_trace = Sepref_Debugging.dbg_trace_msg cfg_debug val dbg_msg_tac = Sepref_Debugging.dbg_msg_tac cfg_debug fun list_filtered_subterms f t = let fun r t = case f t of SOME a => [a] | NONE => ( case t of t1$t2 => r t1 @ r t2 | Abs (_,_,t) => r t | _ => [] ) in r t end fun get_intf_of_rel ctxt R = Term_Synth.synth_term @{thms synth_intf_of_relI} ctxt R |> fastype_of |> Refine_Util.dest_itselfT local fun add_is_pure_constraint ctxt v thm = let val v = Thm.cterm_of ctxt v val rl = Drule.infer_instantiate' ctxt [NONE, SOME v] @{thm add_is_pure_constraint} in thm RS rl end in fun to_assns_rl add_pure_constr ctxt thm = let val orig_ctxt = ctxt val (thm,ctxt) = yield_singleton (apfst snd oo Variable.importT) thm ctxt val (R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\fref _ ?R ?S)"} => (R,S) | _ => raise THM("to_assns_rl: expected fref-thm",~1,[thm]) fun mk_cn_subst (fname,(iname,C,A)) = let val T' = A --> C --> @{typ assn} val v' = Free (fname,T') val ct' = @{mk_term "the_pure ?v'"} |> Thm.cterm_of ctxt in (v',(iname,ct')) end fun relation_flt (name,Type (@{type_name set},[Type (@{type_name prod},[C,A])])) = SOME (name,C,A) | relation_flt _ = NONE val vars = [] |> Term.add_vars R |> Term.add_vars S |> map_filter (relation_flt) val (names,ctxt) = Variable.variant_fixes (map (#1 #> fst) vars) ctxt val cn_substs = map mk_cn_subst (names ~~ vars) val thm = Drule.infer_instantiate ctxt (map snd cn_substs) thm val thm = thm |> add_pure_constr ? fold (fn (v,_) => fn thm => add_is_pure_constraint ctxt v thm) cn_substs val thm = singleton (Variable.export ctxt orig_ctxt) thm in thm end fun cleanup_constraints ctxt thm = let val orig_ctxt = ctxt val (thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) thm ctxt val xform_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops_transform} val rprops_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops} val simp_thms = Named_Theorems.get ctxt @{named_theorems sepref_relprops_simps} fun simp thms = Conv.fconv_rule ( Simplifier.asm_full_rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)) (* Check for pure (the_pure R) - patterns *) local val (_,R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\hfref ?P ?R ?S)"} => (P,R,S) | @{mpat "Trueprop (_\fref ?P ?R ?S)"} => (P,R,S) | _ => raise THM("cleanup_constraints: Expected hfref or fref-theorem",~1,[thm]) fun flt_pat @{mpat "pure (the_pure ?A)"} = SOME A | flt_pat _ = NONE val purify_terms = (list_filtered_subterms flt_pat R @ list_filtered_subterms flt_pat S) |> distinct op aconv val thm = fold (add_is_pure_constraint ctxt) purify_terms thm in val thm = thm end val thm = thm |> Local_Defs.unfold0 ctxt xform_thms |> Local_Defs.unfold0 ctxt rprops_thms val insts = map (fn @{mpat "Trueprop (CONSTRAINT _ (the_pure _))"} => @{thm handle_purity1} | _ => asm_rl ) (Thm.prems_of thm) val thm = (thm OF insts) |> Conv.fconv_rule Thm.eta_conversion |> simp @{thms handle_purity2} |> simp simp_thms val thm = singleton (Variable.export ctxt orig_ctxt) thm in thm end end fun simp_precond_tac ctxt = let fun simp_only thms = asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps thms) val rtac = resolve_tac ctxt val cnv_ss = ctxt delsimps @{thms CNV_def} (*val uncurry_tac = SELECT_GOAL (ALLGOALS (DETERM o SOLVED' ( REPEAT' (rtac @{thms auto_weaken_pre_uncurry_step'}) THEN' rtac @{thms auto_weaken_pre_uncurry_finish} )))*) val prove_cnv_tac = SOLVED' (rtac @{thms CNV_prove} THEN' SELECT_GOAL (auto_tac ctxt)) val do_cnv_tac = (cp_clarsimp_tac cnv_ss) THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (match_tac ctxt @{thms CNV_split})) THEN_ALL_NEW (prove_cnv_tac ORELSE' rtac @{thms CNV_I}) val final_simp_tac = rtac @{thms simp_pre_final_simp} THEN' cp_clarsimp_tac cnv_ss THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "final_simp_tac: Before CNV_I") ctxt THEN' rtac @{thms CNV_I} THEN' dbg_msg_tac (Sepref_Debugging.msg_text "Final-Simp done") ctxt (*val curry_tac = let open Conv in CONVERSION (Refine_Util.HOL_concl_conv (fn ctxt => arg1_conv ( top_conv ( fn _ => try_conv (rewr_conv @{thm uncurry_def})) ctxt)) ctxt) THEN' REPEAT' (EqSubst.eqsubst_tac ctxt [1] @{thms case_prod_eta}) THEN' rtac @{thms CNV_I} end*) val simp_tupled_pre_tac = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms prod_casesK uncurry0_hfref_post}) THEN' REPEAT' (EqSubst.eqsubst_tac ctxt [1] @{thms case_prod_eta}) THEN' rtac @{thms CNV_I} val unfold_and_tac = rtac @{thms and_pre_beta} THEN_ALL_NEW simp_only @{thms split} val simp_and1_tac = rtac @{thms simp_and1} THEN' do_cnv_tac val simp_and2_tac = rtac @{thms simp_and2} THEN' do_cnv_tac val and_plan_tac = simp_and1_tac THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "State after and1") ctxt THEN' ( rtac @{thms triv_and1} ORELSE' dbg_msg_tac (Sepref_Debugging.msg_subgoal "Invoking and2 on") ctxt THEN' simp_and2_tac THEN' dbg_msg_tac (Sepref_Debugging.msg_subgoal "State before final_simp_tac") ctxt THEN' final_simp_tac ) val unfold_imp_tac = rtac @{thms imp_pre_beta} THEN_ALL_NEW simp_only @{thms split} val simp_imp1_tac = rtac @{thms simp_imp} THEN' do_cnv_tac val imp_plan_tac = simp_imp1_tac THEN' final_simp_tac val imp_pre_tac = APPLY_LIST [ simp_only @{thms split_tupled_all} THEN' Refine_Util.instantiate_tuples_subgoal_tac ctxt THEN' CASES' [ (unfold_and_tac, ALLGOALS and_plan_tac), (unfold_imp_tac, ALLGOALS imp_plan_tac) ] , simp_tupled_pre_tac ] val imp_pre_custom_tac = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms and_pre_def}) THEN' TRY o SOLVED' (SELECT_GOAL (auto_tac ctxt)) in CASES' [ (rtac @{thms IMP_PRE_eqI}, imp_pre_tac 1), (rtac @{thms IMP_PRE_CUSTOMI}, ALLGOALS imp_pre_custom_tac) ] end local fun inf_bn_aux name = case String.tokens (fn c => c = #".") name of [] => NONE | [a] => SOME (Binding.name a) | (_::a::_) => SOME (Binding.name a) in fun infer_basename (Const ("_type_constraint_",_)$t) = infer_basename t | infer_basename (Const (name,_)) = inf_bn_aux name | infer_basename (Free (name,_)) = inf_bn_aux name | infer_basename _ = NONE end val cfg_mop = Attrib.setup_config_bool @{binding sepref_register_mop} (K true) val cfg_ismop = Attrib.setup_config_bool @{binding sepref_register_ismop} (K false) val cfg_rawgoals = Attrib.setup_config_bool @{binding sepref_register_rawgoals} (K false) val cfg_transfer = Attrib.setup_config_bool @{binding sepref_decl_impl_transfer} (K true) val cfg_def = Attrib.setup_config_bool @{binding sepref_register_def} (K true) val cfg_register = Attrib.setup_config_bool @{binding sepref_decl_impl_register} (K true) local open Refine_Util val flags = parse_bool_config' "mop" cfg_mop || parse_bool_config' "ismop" cfg_ismop || parse_bool_config' "rawgoals" cfg_rawgoals || parse_bool_config' "def" cfg_def val parse_flags = parse_paren_list' flags val parse_name = Scan.option (Parse.binding --| @{keyword ":"}) val parse_relconds = Scan.optional (@{keyword "where"} |-- Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat) [] in val do_parser = parse_flags -- parse_name -- Parse.term --| @{keyword "::"} -- Parse.term -- parse_relconds end fun do_cmd ((((flags,name),opt_raw), relt_raw),relconds_raw) lthy = let local val ctxt = Refine_Util.apply_configs flags lthy in val flag_ismop = Config.get ctxt cfg_ismop val flag_mop = Config.get ctxt cfg_mop andalso not flag_ismop val flag_rawgoals = Config.get ctxt cfg_rawgoals val flag_def = Config.get ctxt cfg_def end open Sepref_Basic Sepref_Rules val relt = Syntax.parse_term lthy relt_raw val relconds = map (Syntax.parse_prop lthy) relconds_raw val _ = dbg_trace lthy "Parse relation and relation conditions together" val relt = Const (@{const_name "Pure.term"}, dummyT) $ relt local val l = Syntax.check_props lthy (relt::relconds) in val (relt, relconds) = (hd l, tl l) end val relt = Logic.dest_term relt val opt_pre = Syntax.parse_term lthy opt_raw val _ = dbg_trace lthy "Infer basename" val name = case name of SOME name => name | NONE => ( case infer_basename opt_pre of NONE => (error "Could not infer basename: You have to specify a basename"; Binding.empty) | SOME name => name ) fun qname s n = Binding.qualify true (Binding.name_of n) (Binding.name s) fun def name t_pre attribs lthy = let val t = Syntax.check_term lthy t_pre (*|> Thm.cterm_of lthy |> Drule.mk_term |> Local_Defs.unfold0 lthy @{thms PR_CONST_def} |> Drule.dest_term |> Thm.term_of*) val lthy = (snd o Local_Theory.begin_nested) lthy val ((dt,(_,thm)),lthy) = Local_Theory.define ((name,Mixfix.NoSyn),((Thm.def_binding name,@{attributes [code]}@attribs),t)) lthy; val (lthy, lthy_old) = `Local_Theory.end_nested lthy val phi = Proof_Context.export_morphism lthy_old lthy val thm = Morphism.thm phi thm val dt = Morphism.term phi dt in ((dt,thm),lthy) end val _ = dbg_trace lthy "Analyze Relation" val (pre,args,res) = analyze_rel relt val specified_pre = is_some pre val pre = the_default (mk_triv_precond args) pre val def_thms = @{thms PR_CONST_def} val _ = dbg_trace lthy "Define op" val op_name = Binding.prefix_name (if flag_ismop then "mop_" else "op_") name val (def_thms,opc,lthy) = if flag_def then let val ((opc,op_def_thm),lthy) = def op_name opt_pre @{attributes [simp]} lthy val opc = Refine_Util.dummify_tvars opc val def_thms = op_def_thm::def_thms in (def_thms,opc,lthy) end else let val _ = dbg_trace lthy "Refine type of opt_pre to get opc" val opc = Syntax.check_term lthy opt_pre val new_ctxt = Variable.declare_term opc lthy val opc = singleton (Variable.export_terms new_ctxt lthy) opc |> Refine_Util.dummify_tvars in (def_thms,opc,lthy) end (* PR_CONST Heuristics *) fun pr_const_heuristics basename c_pre lthy = let val _ = dbg_trace lthy ("PR_CONST heuristics " ^ @{make_string} c_pre) val c = Syntax.check_term lthy c_pre in case c of @{mpat "PR_CONST _"} => ((c_pre,false),lthy) | Const _ => ((c_pre,false),lthy) | _ => let val (f,args) = strip_comb c val lthy = case f of Const _ => let val ctxt = Variable.declare_term c lthy val lhs = Autoref_Tagging.list_APP (f,args) val rhs = @{mk_term "UNPROTECT ?c"} val goal = Logic.mk_equals (lhs,rhs) |> Thm.cterm_of ctxt val tac = Local_Defs.unfold0_tac ctxt @{thms APP_def UNPROTECT_def} THEN ALLGOALS (simp_tac (put_simpset HOL_basic_ss ctxt)) val thm = Goal.prove_internal ctxt [] goal (K tac) |> singleton (Variable.export ctxt lthy) val (_,lthy) = Local_Theory.note ((Binding.suffix_name "_def_pat" basename,@{attributes [def_pat_rules]}),[thm]) lthy val _ = Thm.pretty_thm lthy thm |> Pretty.string_of |> writeln in lthy end | _ => ( Pretty.block [ Pretty.str "Complex operation pattern. Added PR_CONST but no pattern rules:", Pretty.brk 1,Syntax.pretty_term lthy c] |> Pretty.string_of |> warning ; lthy) val c_pre = Const(@{const_name PR_CONST},dummyT)$c_pre in ((c_pre,true),lthy) end end val ((opc,_),lthy) = pr_const_heuristics op_name opc lthy (* Register *) val arg_intfs = map (get_intf_of_rel lthy) args val res_intf = get_intf_of_rel lthy res fun register basename c lthy = let val _ = dbg_trace lthy "Register" open Sepref_Basic val c = Syntax.check_term lthy c val ri = case (is_nresT (body_type (fastype_of c)), is_nresT res_intf) of (true,false) => mk_nresT res_intf | (false,true) => dest_nresT res_intf | _ => res_intf val iT = arg_intfs ---> ri val ((_,itype_thm),lthy) = Sepref_Combinator_Setup.sepref_register_single (Binding.name_of basename) c iT lthy - val _ = Thy_Output.pretty_thm lthy itype_thm |> Pretty.string_of |> writeln + val _ = Document_Output.pretty_thm lthy itype_thm |> Pretty.string_of |> writeln in lthy end val lthy = register op_name opc lthy val _ = dbg_trace lthy "Define pre" val pre_name = Binding.prefix_name "pre_" name val ((prec,pre_def_thm),lthy) = def pre_name pre @{attributes [simp]} lthy val prec = Refine_Util.dummify_tvars prec val def_thms = pre_def_thm::def_thms (* Re-integrate pre-constant into type-context of relation. TODO: This is probably not clean/robust *) val pre = constrain_type_pre (fastype_of pre) prec |> Syntax.check_term lthy val _ = dbg_trace lthy "Convert both, relation and operation to uncurried form, and add nres" val _ = dbg_trace lthy "Convert relation (arguments have already been separated by analyze-rel)" val res = case res of @{mpat "\_\nres_rel"} => res | _ => @{mk_term "\?res\nres_rel"} val relt = mk_rel (SOME pre,args,res) val _ = dbg_trace lthy "Convert operation" val opcT = fastype_of (Syntax.check_term lthy opc) val op_is_nres = Sepref_Basic.is_nresT (body_type opcT) val (opcu, op_ar) = let val arity = binder_types #> length (* Arity of operation is number of arguments before result (which may be a fun-type! )*) val res_ar = arity (Relators.rel_absT res |> not op_is_nres ? dest_nresT) val op_ar = arity opcT - res_ar val _ = op_ar = length args orelse raise TERM("Operation/relation arity mismatch: " ^ string_of_int op_ar ^ " vs " ^ string_of_int (length args),[opc,relt]) (* Add RETURN o...o if necessary*) val opc = if op_is_nres then opc else mk_compN_pre op_ar (Const(@{const_name Refine_Basic.RETURN},dummyT)) opc (* Add uncurry if necessary *) val opc = mk_uncurryN_pre op_ar opc in (opc, op_ar) end (* Build mop-variant *) val declare_mop = (specified_pre orelse not op_is_nres) andalso flag_mop val (mop_data,lthy) = if declare_mop then let val _ = dbg_trace lthy "mop definition" val mop_rhs = Const(@{const_name mop},dummyT) $ prec $ opcu |> mk_curryN_pre op_ar val mop_name = Binding.prefix_name "mop_" name val ((mopc,mop_def_thm),lthy) = def mop_name mop_rhs [] lthy val mopc = Refine_Util.dummify_tvars mopc val ((mopc,added_pr_const),lthy) = pr_const_heuristics mop_name mopc lthy val mop_def_thm' = if added_pr_const then mop_def_thm RS @{thm add_PR_CONST_to_def} else mop_def_thm val (_,lthy) = Local_Theory.note ((Binding.empty, @{attributes [sepref_mop_def_thms]}),[mop_def_thm']) lthy val _ = dbg_trace lthy "mop alternative definition" val alt_unfolds = @{thms mop_alt_unfolds} |> not specified_pre ? curry op :: pre_def_thm val mop_alt_thm = Local_Defs.unfold0 lthy alt_unfolds mop_def_thm |> Refine_Util.shift_lambda_leftN op_ar val (_,lthy) = Local_Theory.note ((Binding.suffix_name "_alt" mop_name,@{attributes [simp]}),[mop_alt_thm]) lthy val _ = dbg_trace lthy "mop: register" val lthy = register mop_name mopc lthy val _ = dbg_trace lthy "mop: vcg theorem" local val Ts = map Relators.rel_absT args val ctxt = Variable.declare_thm mop_def_thm lthy val ctxt = fold Variable.declare_typ Ts ctxt val (x,ctxt) = Refine_Util.fix_left_tuple_from_Ts "x" Ts ctxt val mop_def_thm = mop_def_thm |> Local_Defs.unfold0 ctxt @{thms curry_shl} fun prep_thm thm = (thm OF [mop_def_thm]) |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt x)] |> Local_Defs.unfold0 ctxt @{thms uncurry_apply uncurry0_apply o_apply} |> Local_Defs.unfold0 ctxt (def_thms @ @{thms Product_Type.split HOL.True_implies_equals}) |> singleton (Variable.export ctxt lthy) val thms = map prep_thm @{thms mop_spec_rl_from_def mop_leof_rl_from_def} in val (_,lthy) = Local_Theory.note ((qname "vcg" mop_name,@{attributes [refine_vcg]}),thms) lthy end in (SOME (mop_name,mopc,mop_def_thm),lthy) end else (NONE,lthy) val _ = dbg_trace lthy "Build Parametricity Theorem" val param_t = mk_pair_in_pre opcu opcu relt |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds val _ = dbg_trace lthy "Build Parametricity Theorem for Precondition" val param_pre_t = let val pre_relt = Relators.mk_fun_rel (Relators.list_prodrel_left args) @{term bool_rel} val param_pre_t = mk_pair_in_pre prec prec pre_relt |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds in param_pre_t end val _ = dbg_trace lthy "Build goals" val goals = [[ (param_t, []), (param_pre_t, []) ]] fun after_qed [[p_thm, pp_thm]] _ (*ctxt*) = let val _ = dbg_trace lthy "after_qed" val p_thm' = p_thm |> not specified_pre ? Local_Defs.unfold0 lthy [pre_def_thm] val (_,lthy) = Local_Theory.note ((qname "fref" op_name,@{attributes [sepref_fref_thms]}), [p_thm']) lthy val (_,lthy) = Local_Theory.note ((qname "param" pre_name,@{attributes [param]}), [pp_thm]) lthy val p'_unfolds = pre_def_thm :: @{thms True_implies_equals} val (_,lthy) = Local_Theory.note ((qname "fref'" op_name,[]), [Local_Defs.unfold0 lthy p'_unfolds p_thm]) lthy val lthy = case mop_data of NONE => lthy | SOME (mop_name,mopc,mop_def_thm) => let val _ = dbg_trace lthy "Build and prove mop-stuff" (* mop - parametricity theorem: (uncurry\<^sup>n mopc,uncurry\<^sup>n mopc) \ args \\<^sub>f res *) val mopcu = mk_uncurryN_pre op_ar mopc val param_mop_t = mk_pair_in_pre mopcu mopcu (mk_rel (NONE,args,res)) |> Syntax.check_term lthy |> HOLogic.mk_Trueprop |> curry Logic.list_implies relconds val ctxt = Proof_Context.augment param_mop_t lthy val tac = let val p_thm = Local_Defs.unfold0 ctxt @{thms PR_CONST_def} p_thm in Local_Defs.unfold0_tac ctxt (mop_def_thm :: @{thms PR_CONST_def uncurry_curry_id uncurry_curry0_id}) THEN FIRSTGOAL ( dbg_msg_tac (Sepref_Debugging.msg_subgoal "Mop-param thm goal after unfolding") ctxt THEN' resolve_tac ctxt @{thms param_mopI} THEN' SOLVED' (resolve_tac ctxt [p_thm] THEN_ALL_NEW assume_tac ctxt) THEN' SOLVED' (resolve_tac ctxt [pp_thm] THEN_ALL_NEW assume_tac ctxt) ) end val pm_thm = Goal.prove_internal lthy [] (Thm.cterm_of ctxt param_mop_t) (K tac) |> singleton (Variable.export ctxt lthy) val (_,lthy) = Local_Theory.note ((qname "fref" mop_name,@{attributes [sepref_fref_thms]}), [pm_thm]) lthy val (_,lthy) = Local_Theory.note ((qname "fref'" mop_name,[]), [Local_Defs.unfold0 lthy p'_unfolds pm_thm]) lthy in lthy end in lthy end | after_qed thmss _ = raise THM ("After-qed: Wrong thmss structure",~1,flat thmss) fun std_tac ctxt = let val ptac = REPEAT_ALL_NEW_FWD (Parametricity.net_tac (Parametricity.get_dflt ctxt) ctxt) (* Massage simpset a bit *) val ctxt = ctxt |> Context_Position.set_visible false |> Context.proof_map (Thm.attribute_declaration Clasimp.iff_del @{thm pair_in_Id_conv}) in if flag_rawgoals then all_tac else Local_Defs.unfold0_tac ctxt def_thms THEN ALLGOALS ( TRY o SOLVED' ( TRY o resolve_tac ctxt @{thms frefI} THEN' TRY o REPEAT_ALL_NEW (ematch_tac ctxt @{thms prod_relE}) THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split uncurry_apply uncurry0_apply}) THEN' ( SOLVED' (ptac THEN_ALL_NEW asm_full_simp_tac ctxt) ORELSE' SOLVED' (cp_clarsimp_tac ctxt THEN_ALL_NEW_FWD ptac THEN_ALL_NEW SELECT_GOAL (auto_tac ctxt)) ) ) ) end val rf_std = Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (std_tac ctxt))) #> Seq.the_result "do_cmd: Standard proof tactic returned empty result sequence" in Proof.theorem NONE after_qed goals lthy |> rf_std end val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "sepref_decl_op"} "" (do_parser >> do_cmd) local fun unfold_PR_CONST_tac ctxt = SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms PR_CONST_def}) fun transfer_precond_rl ctxt t R = let (*val tfrees = Term.add_tfreesT (fastype_of t) [] val t' = map_types (map_type_tfree (fn x => if member op= tfrees x then dummyT else TFree x)) t *) (* TODO: Brute force approach, that may generalize too much! *) val t' = map_types (K dummyT) t val goal = Sepref_Basic.mk_pair_in_pre t t' R |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val thm = Drule.infer_instantiate' ctxt [NONE,SOME goal] @{thm IMP_LIST_trivial} in thm end (* Generate a hnr-thm for mop given one for op *) fun generate_mop_thm ctxt op_thm = let val orig_ctxt = ctxt val (op_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) op_thm ctxt (* Convert mop_def_thms to form uncurry^n f \ mop P g *) val mop_def_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_mop_def_thms} |> map (Local_Defs.unfold0 ctxt @{thms curry_shl}) fun fail_hnr_tac _ _ = raise THM("Invalid hnr-theorem",~1,[op_thm]) fun fail_mop_def_tac i st = let val g = nth (Thm.prems_of st) (i-1) in raise TERM("Found no matching mop-definition",[g]) end (* Tactic to solve preconditions of hfref_op_to_mop *) val tac = APPLY_LIST [ resolve_tac ctxt [op_thm] ORELSE' fail_hnr_tac, ((*unfold_PR_CONST_tac ctxt THEN'*) resolve_tac ctxt mop_def_thms) ORELSE' fail_mop_def_tac, simp_precond_tac ctxt ORELSE' Sepref_Debugging.error_tac' "precond simplification failed" ctxt ] 1 (* Do synthesis *) val st = @{thm hfref_op_to_mop} val st = Goal.protect (Thm.nprems_of st) st val mop_thm = tac st |> Seq.hd |> Goal.conclude val mop_thm = singleton (Variable.export ctxt orig_ctxt) mop_thm |> Sepref_Rules.norm_fcomp_rule orig_ctxt in mop_thm end (* Generate a hnr-thm for op given one for mop *) fun generate_op_thm ctxt mop_thm = let (* TODO: Almost-clone of generate_mop_thm *) val orig_ctxt = ctxt val (mop_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) mop_thm ctxt (* Convert mop_def_thms to form uncurry^n f \ mop P g *) val mop_def_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_mop_def_thms} |> map (Local_Defs.unfold0 ctxt @{thms curry_shl}) fun fail_hnr_tac _ _ = raise THM("Invalid hnr-theorem",~1,[mop_thm]) fun fail_mop_def_tac i st = let val g = nth (Thm.prems_of st) (i-1) in raise TERM("Found no matching mop-definition",[g]) end (* Tactic to solve preconditions of hfref_mop_to_op *) val tac = APPLY_LIST [ resolve_tac ctxt [mop_thm] ORELSE' fail_hnr_tac, ((*unfold_PR_CONST_tac ctxt THEN'*) resolve_tac ctxt mop_def_thms) ORELSE' fail_mop_def_tac, simp_precond_tac ctxt ORELSE' Sepref_Debugging.error_tac' "precond simplification failed" ctxt ] 1 (* Do synthesis *) val st = @{thm hfref_mop_to_op} val st = Goal.protect (Thm.nprems_of st) st val op_thm = tac st |> Seq.hd |> Goal.conclude val op_thm = singleton (Variable.export ctxt orig_ctxt) op_thm |> Sepref_Rules.norm_fcomp_rule orig_ctxt in op_thm end fun chk_result ctxt thm = let val (_,R,S) = case Thm.concl_of thm of @{mpat "Trueprop (_\hfref ?P ?R ?S)"} => (P,R,S) | _ => raise THM("chk_result: Expected hfref-theorem",~1,[thm]) fun err t = let val ts = Syntax.pretty_term ctxt t |> Pretty.string_of in raise THM ("chk_result: Invalid pattern left in assertions: " ^ ts,~1,[thm]) end fun check_invalid (t as @{mpat "hr_comp _ _"}) = err t | check_invalid (t as @{mpat "hrp_comp _ _"}) = err t | check_invalid (t as @{mpat "pure (the_pure _)"}) = err t | check_invalid (t as @{mpat "_ O _"}) = err t | check_invalid _ = false val _ = exists_subterm check_invalid R val _ = exists_subterm check_invalid S in () end fun to_IMP_LIST ctxt thm = (thm RS @{thm to_IMP_LISTI}) |> Local_Defs.unfold0 ctxt @{thms to_IMP_LIST} fun from_IMP_LIST ctxt thm = thm |> Local_Defs.unfold0 ctxt @{thms from_IMP_LIST} in local open Refine_Util val flags = parse_bool_config' "mop" cfg_mop || parse_bool_config' "ismop" cfg_ismop || parse_bool_config' "transfer" cfg_transfer || parse_bool_config' "rawgoals" cfg_rawgoals || parse_bool_config' "register" cfg_register val parse_flags = parse_paren_list' flags val parse_precond = Scan.option (@{keyword "["} |-- Parse.term --| @{keyword "]"}) val parse_fref_thm = Scan.option (@{keyword "uses"} |-- Parse.thm) in val di_parser = parse_flags -- Scan.optional (Parse.binding --| @{keyword ":"}) Binding.empty -- parse_precond -- Parse.thm -- parse_fref_thm end fun di_cmd ((((flags,name), precond_raw), i_thm_raw), p_thm_raw) lthy = let val i_thm = singleton (Attrib.eval_thms lthy) i_thm_raw val p_thm = map_option (singleton (Attrib.eval_thms lthy)) p_thm_raw local val ctxt = Refine_Util.apply_configs flags lthy in val flag_mop = Config.get ctxt cfg_mop val flag_ismop = Config.get ctxt cfg_ismop val flag_rawgoals = Config.get ctxt cfg_rawgoals val flag_transfer = Config.get ctxt cfg_transfer val flag_register = Config.get ctxt cfg_register end val fr_attribs = if flag_register then @{attributes [sepref_fr_rules]} else [] val ctxt = lthy (* Compose with fref-theorem *) val _ = dbg_trace lthy "Compose with fref" local val hf_tcomp_pre = @{thm hfcomp_tcomp_pre} OF [asm_rl,i_thm] fun compose p_thm = let val p_thm = p_thm |> to_assns_rl false lthy in hf_tcomp_pre OF [p_thm] end in val thm = case p_thm of SOME p_thm => compose p_thm | NONE => let val p_thms = Named_Theorems_Rev.get ctxt @{named_theorems_rev sepref_fref_thms} fun err () = let val prem_s = nth (Thm.prems_of hf_tcomp_pre) 0 |> Syntax.pretty_term ctxt |> Pretty.string_of in error ("Found no fref-theorem matching " ^ prem_s) end in case get_first (try compose) p_thms of NONE => err () | SOME thm => thm end end val (thm,ctxt) = yield_singleton (apfst snd oo Variable.import true) thm ctxt val _ = dbg_trace lthy "Transfer Precond" val thm = to_IMP_LIST ctxt thm val thm = thm RS @{thm transform_pre_param} local val (pre,R,pp_name,pp_type) = case Thm.prems_of thm of [@{mpat "Trueprop (IMP_LIST _ ((?pre,_)\?R))"}, @{mpat "Trueprop (IMP_PRE (mpaq_STRUCT (mpaq_Var ?pp_name ?pp_type)) _)"}] => (pre,R,pp_name,pp_type) | _ => raise THM("di_cmd: Cannot recognize first prems of transform_pre_param: ", ~1,[thm]) in val thm = if flag_transfer then thm OF [transfer_precond_rl ctxt pre R] else thm val thm = case precond_raw of NONE => thm | SOME precond_raw => let val precond = Syntax.parse_term ctxt precond_raw |> Sepref_Basic.constrain_type_pre pp_type |> Syntax.check_term ctxt |> Thm.cterm_of ctxt val thm = Drule.infer_instantiate ctxt [(pp_name,precond)] thm val thm = thm OF [asm_rl,@{thm IMP_PRE_CUSTOMD}] in thm end end val _ = dbg_trace lthy "Build goals" val goals = [map (fn x => (x,[])) (Thm.prems_of thm)] fun after_qed thmss _ = let val _ = dbg_trace lthy "After QED" val prems_thms = hd thmss val thm = thm OF prems_thms val thm = from_IMP_LIST ctxt thm (* Two rounds of cleanup-constraints, norm_fcomp *) val _ = dbg_trace lthy "Cleanup" val thm = thm |> cleanup_constraints ctxt |> Sepref_Rules.norm_fcomp_rule ctxt |> cleanup_constraints ctxt |> Sepref_Rules.norm_fcomp_rule ctxt val thm = thm |> singleton (Variable.export ctxt lthy) |> zero_var_indexes val _ = dbg_trace lthy "Check Result" val _ = chk_result lthy thm fun qname suffix = if Binding.is_empty name then name else Binding.suffix_name suffix name val thm_name = if flag_ismop then qname "_hnr_mop" else qname "_hnr" val (_,lthy) = Local_Theory.note ((thm_name,fr_attribs),[thm]) lthy val _ = Thm.pretty_thm lthy thm |> Pretty.string_of |> writeln (* Create mop theorem from op-theorem *) val cr_mop_thm = flag_mop andalso not flag_ismop val lthy = if cr_mop_thm then let val _ = dbg_trace lthy "Create mop-thm" val mop_thm = thm |> generate_mop_thm lthy |> zero_var_indexes val (_,lthy) = Local_Theory.note ((qname "_hnr_mop",fr_attribs),[mop_thm]) lthy val _ = Thm.pretty_thm lthy mop_thm |> Pretty.string_of |> writeln in lthy end else lthy (* Create op theorem from mop-theorem *) val cr_op_thm = flag_ismop val lthy = if cr_op_thm then let val _ = dbg_trace lthy "Create op-thm" val op_thm = thm |> generate_op_thm lthy |> zero_var_indexes val (_,lthy) = Local_Theory.note ((qname "_hnr",fr_attribs),[op_thm]) lthy val _ = Thm.pretty_thm lthy op_thm |> Pretty.string_of |> writeln in lthy end else lthy in lthy end fun std_tac ctxt = let val ptac = REPEAT_ALL_NEW_FWD ( Parametricity.net_tac (Parametricity.get_dflt ctxt) ctxt ORELSE' assume_tac ctxt ) in if flag_rawgoals orelse not flag_transfer then all_tac else APPLY_LIST [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms from_IMP_LIST}) THEN' TRY o SOLVED' ptac, simp_precond_tac ctxt ] 1 end val rf_std = Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (std_tac ctxt))) #> Seq.the_result "di_cmd: Standard proof tactic returned empty result sequence" in Proof.theorem NONE after_qed goals ctxt |> rf_std end val _ = Outer_Syntax.local_theory_to_proof @{command_keyword "sepref_decl_impl"} "" (di_parser >> di_cmd) end end \ subsection \Obsolete Manual Specification Helpers\ (* Generate VCG-rules for operations *) lemma vcg_of_RETURN_np: assumes "f \ RETURN r" shows "SPEC (\x. x=r) \ m \ f \ m" and "SPEC (\x. x=r) \\<^sub>n m \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff) lemma vcg_of_RETURN: assumes "f \ do { ASSERT \; RETURN r }" shows "\\; SPEC (\x. x=r) \ m\ \ f \ m" and "\\ \ SPEC (\x. x=r) \\<^sub>n m\ \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps) lemma vcg_of_SPEC: assumes "f \ do { ASSERT pre; SPEC post }" shows "\pre; SPEC post \ m\ \ f \ m" and "\pre \ SPEC post \\<^sub>n m\ \ f \\<^sub>n m" using assms by (auto simp: pw_le_iff pw_leof_iff refine_pw_simps) lemma vcg_of_SPEC_np: assumes "f \ SPEC post" shows "SPEC post \ m \ f \ m" and "SPEC post \\<^sub>n m \ f \\<^sub>n m" using assms by auto (* Generate parametricity rules to generalize plain operations to monadic ones. Use with FCOMP. *) lemma mk_mop_rl1: assumes "\x. mf x \ ASSERT (P x) \ RETURN (f x)" shows "(RETURN o f, mf) \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl2: assumes "\x y. mf x y \ ASSERT (P x y) \ RETURN (f x y)" shows "(RETURN oo f, mf) \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl3: assumes "\x y z. mf x y z \ ASSERT (P x y z) \ RETURN (f x y z)" shows "(RETURN ooo f, mf) \ Id \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl0_np: assumes "mf \ RETURN f" shows "(RETURN f, mf) \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl1_np: assumes "\x. mf x \ RETURN (f x)" shows "(RETURN o f, mf) \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl2_np: assumes "\x y. mf x y \ RETURN (f x y)" shows "(RETURN oo f, mf) \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_mop_rl3_np: assumes "\x y z. mf x y z \ RETURN (f x y z)" shows "(RETURN ooo f, mf) \ Id \ Id \ Id \ \Id\nres_rel" unfolding assms[abs_def] by (auto intro!: nres_relI simp: pw_le_iff refine_pw_simps) lemma mk_op_rl0_np: assumes "mf \ RETURN f" shows "(uncurry0 mf, uncurry0 (RETURN f)) \ unit_rel \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl1: assumes "\x. mf x \ ASSERT (P x) \ RETURN (f x)" shows "(mf, RETURN o f) \ [P]\<^sub>f Id \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl1_np: assumes "\x. mf x \ RETURN (f x)" shows "(mf, (RETURN o f)) \ Id \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl2: assumes "\x y. mf x y \ ASSERT (P x y) \ RETURN (f x y)" shows "(uncurry mf, uncurry (RETURN oo f)) \ [uncurry P]\<^sub>f Id\\<^sub>rId \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl2_np: assumes "\x y. mf x y \ RETURN (f x y)" shows "(uncurry mf, uncurry (RETURN oo f)) \ Id\\<^sub>rId \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl3: assumes "\x y z. mf x y z \ ASSERT (P x y z) \ RETURN (f x y z)" shows "(uncurry2 mf, uncurry2 (RETURN ooo f)) \ [uncurry2 P]\<^sub>f (Id\\<^sub>rId)\\<^sub>rId \ \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done lemma mk_op_rl3_np: assumes "\x y z. mf x y z \ RETURN (f x y z)" shows "(uncurry2 mf, uncurry2 (RETURN ooo f)) \ (Id\\<^sub>rId)\\<^sub>rId \\<^sub>f \Id\nres_rel" apply (intro frefI nres_relI) apply (auto simp: assms) done end diff --git a/thys/Sturm_Sequences/ROOT b/thys/Sturm_Sequences/ROOT --- a/thys/Sturm_Sequences/ROOT +++ b/thys/Sturm_Sequences/ROOT @@ -1,20 +1,20 @@ chapter AFP session Sturm_Sequences (AFP) = "HOL-Computational_Algebra" + - options [timeout = 600, document_variants = "document:outline=/proof,/ML:userguide"] + options [timeout = 600, document_logo = "_", + document_variants = "document:outline=/proof,/ML:userguide"] directories "Lib" "Examples" theories "Lib/Sturm_Library_Document" "Lib/Misc_Polynomial" theories [document = false] "Lib/Sturm_Library" theories Sturm_Theorem Sturm_Method "Examples/Sturm_Ex" document_files - "build" "root.tex" "root_userguide.tex" diff --git a/thys/Sturm_Sequences/document/build b/thys/Sturm_Sequences/document/build deleted file mode 100755 --- a/thys/Sturm_Sequences/document/build +++ /dev/null @@ -1,18 +0,0 @@ -#!/usr/bin/env bash - -set -e - -FORMAT="$1" -VARIANT="$2" - -isabelle logo -isabelle latex -o sty - -if [ "$VARIANT" = "userguide" ]; then - ROOT="root_userguide.tex" -else - ROOT="root.tex" -fi - -isabelle latex -o "$FORMAT" "$ROOT" -isabelle latex -o "$FORMAT" "$ROOT" diff --git a/thys/Sturm_Sequences/document/root_userguide.tex b/thys/Sturm_Sequences/document/root_userguide.tex --- a/thys/Sturm_Sequences/document/root_userguide.tex +++ b/thys/Sturm_Sequences/document/root_userguide.tex @@ -1,143 +1,143 @@ \documentclass[11pt,a4paper,oneside]{article} \usepackage[T1]{fontenc} \usepackage[english]{babel} \usepackage{geometry} \usepackage{color} \usepackage{graphicx} \usepackage{pifont} \usepackage[babel]{csquotes} \usepackage{textcomp} \usepackage{upgreek} \usepackage{amsmath} \usepackage{textcomp} \usepackage{amssymb} \usepackage{latexsym} \usepackage{pgf} \usepackage{nicefrac} \usepackage{enumerate} \usepackage{stmaryrd} \usepackage{tgpagella} \DeclareFontFamily{OT1}{pzc}{} \DeclareFontShape{OT1}{pzc}{m}{it}{<-> s * [1.10] pzcmi7t}{} \DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it} \newcommand{\ie}{i.\,e.} \newcommand{\wuppdi}[0]{\hfill\ensuremath{\square}} \newcommand{\qed}[0]{\vspace{-3mm}\begin{flushright}\textit{q.e.d.}\end{flushright}\vspace{3mm}} \newcommand{\bred}{\ensuremath{\longrightarrow_\beta}} \newcommand{\acos}{\textrm{arccos}} \newcommand{\determ}[1]{\textrm{det}(#1)} \newcommand{\RR}{\mathbb{R}} \newcommand{\BB}{\mathbb{B}} \newcommand{\NN}{\mathbb{N}} \newcommand{\QQ}{\mathbb{Q}} \newcommand{\ZZ}{\mathbb{Z}} \newcommand{\CC}{\mathbb{C}} \newcommand{\II}{\mathbb{I}} \newcommand{\kernel}[1]{\textrm{ker}(#1)} \renewcommand{\epsilon}{\varepsilon} \renewcommand{\phi}{\varphi} \renewcommand{\theta}{\vartheta} \newcommand{\atan}{\mathrm{arctan}} \newcommand{\rot}{\mathrm{rot}} \newcommand{\vdiv}{\mathrm{div}} \newcommand{\shouldbe}{\stackrel{!}{=}} \newcommand{\sturm}{\texttt{sturm}} \newcommand{\lemma}{\textbf{lemma}} \newcommand{\card}{\textrm{card}} \newcommand{\real}{\textrm{real}} \newcommand{\isabellehol}{\mbox{Isabelle}\slash HOL} \geometry{a4paper,left=30mm,right=30mm, top=25mm, bottom=30mm} \title{\LARGE User's Guide for the \texttt{sturm} Method\\[4mm]} \author{\Large Manuel Eberl \\[1mm]\large Institut für Informatik, Technische Universität München\\[4mm]} \begin{document} \begin{center} \vspace*{20mm} -\includegraphics[width=4cm]{isabelle.pdf} +\includegraphics[width=4cm]{isabelle_logo} \end{center} \vspace*{-5mm} {\let\newpage\relax\maketitle} \vspace*{10mm} \tableofcontents \newpage \section{Introduction} The \sturm\ method uses Sturm's theorem to determine the number of distinct real roots of a polynomial (with rational coefficients) within a certain interval. It also provides some preprocessing to decide a number of statements that can be reduced to real roots of polynomials, such as simple polynomial inequalities and logical combinations of polynomial equations. \vspace*{10mm} \section{Usage} \subsection{Examples} The following examples should give a good overview of what the \sturm\ method can do: \begin{align*} &\lemma\ "\card\ \{x::\real.\ (x - 1)^2 * (x + 1) = 0\}\ =\ 2"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "\mathrm{card}\ \{x::\mathrm{real}.\ -0.010831 < x\ \wedge\ x < 0.010831\ \wedge\\ &\hskip20mm \mathrm{poly}\ [:0, -17/2097152, -49/16777216, 1/6, 1/24, 1/120:]\ \ x\ =\ 0\}\ =\ 3"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "\card\ \{x::\real.\ x^3 + x = 2*x^2\ \wedge\ x^3-6*x^2+11*x=6\}\ =\ 1"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "\card\ \{x::\real.\ x^3 + x = 2*x^2\ \vee\ x^3-6*x^2+11*x=6\}\ =\ 4"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "(x::\real)^2+1 > 0"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "(x::\real) > 0\ \Longrightarrow\ x^2+1 > 0"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "\llbracket (x::\real) > 0; x \leq 2/3\rrbracket\ \Longrightarrow\ x*x \neq\ x"\ \textrm{\textbf{by}\ sturm}\\ &\lemma\ "(x::\real) > 1\ \Longrightarrow\ x*x > x"\ \textrm{\textbf{by}\ sturm}\\ \end{align*} \subsection{Determining the number of real roots} The \enquote{classical} application of Sturm's theorem is to count the number of real roots of a polynomial in a certain interval. The \sturm\ method supports this for any polynomial with rational coefficients and any real interval, \ie $[a;b]$, $(a;b]$, $[a;b)$, and $(a;b)$ where $a\in\QQ\cup\{-\infty\}$ and $b\in\QQ\cup\{\infty\}$.\footnote{The restriction to rational numbers for the coefficients and interval bounds is to the fact that the code generator is used internally, which, of course, does not support computations on irrational real numbers.} The general form of the theorems the method expects is: $$\card\ \{x::\real.\ a < x \wedge x < b \wedge p\ x = 0\}\ =\ ?n$$ $?n$ should be replaced by the actual number of such roots and $p$ may be any polynomial real function in $x$ with rational coefficients. The bounds $a < x$ and $x < b$ can be omitted for the \enquote{$\infty$} case.\\ Furthermore, the \sturm\ method can instantiate the number $?n$ on the right-hand side automatically if it is left unspecified (as a schematic variable in a schematic lemma). However, due to technical restrictions this also takes twice as long as simply proving that the specified number is correct. \newpage \subsection{Inequalities} A simple special case of root counting is the statement that a polynomial $p\in\RR[X]$ has no roots in a certain interval, which can be written as: $$\forall x::\real.\ x > a \wedge x < b \longrightarrow p\ x \neq 0$$ The \sturm\ method can be directly applied to statements such as this and prove them. \subsection{More complex expressions} By using some simple preprocessing, the \sturm\ method can also decide more complex statements: $$\card\ \{x::\real.\ x > a\ \wedge\ x < b\ \wedge\ P\ x\}\ =\ n$$ where $P\ x$ is a \enquote{polynomial expression}, which is defined as: \begin{enumerate} \item $p\ x= q\ x$, where $p$ and $q$ are polynomial functions, such as $\lambda x.\ a$, $\lambda x.\ x$, $\lambda x.\ x^2$, $\mathrm{poly}\ p$, and so on \item $P\ x\ \wedge\ Q\ x$ or $P\ x\ \vee\ Q\ x$, where $P\ x$ and $Q\ x$ are polynomial expressions \end{enumerate} Of course, by reduction to the case of zero roots, the following kind of statement is also provable by \sturm\ : $$\forall x::\real.\ x > a\ \wedge\ x < b\ \longrightarrow\ P\ x$$ where $P\ x$ is a \enquote{negated polynomial expression}, which is defined as: \begin{enumerate} \item $p\ x\neq q\ x$, where $p$ and $q$ are polynomial functions \item $P\ x\ \wedge\ Q\ x$ or $P\ x\ \vee\ Q\ x$, where $P\ x$ and $Q\ x$ are negated polynomial expressions \end{enumerate} \subsection{Simple ordered inequalities} For any polynomial $p\in\RR[X]$, the question whether $p(x) > 0$ for all $x\in I$ for a non-empty real interval $I$ can obviously be reduced to the question of whether $p(x) \neq 0$ for all $x\in I$, \ie $p$ has no roots in $I$, and $p(x) > 0$ for some arbitrary fixed $x\in I$, the first of which can be decided using Sturm's theorem and the second by choosing an arbitrary $x\in I$ and evaluating $p(x)$.\\ Using this reduction, the \sturm\ method can also decide single \enquote{less than}/\enquote{greater than} inequalities of the form $$\forall x::\real.\ x > a\ \wedge\ x < b\ \longrightarrow\ p\ x < q\ x$$ \subsection{A note on meta logic versus object logic} While statements like $\forall x::\real.\ x^2+1>0$ were expressed in their HOL notation in this guide, the \sturm\ method can also prove the meta logic equivalents $\bigwedge x::\real.\ x^2+1>0$ and $(x::\real)^2+1>0$ directly. \section{Troubleshooting} Should you find that the \sturm\ method fails to prove a statement that it should, according to the above text, be able to prove, please go through the following steps: \begin{enumerate} \item ensure that your function is indeed a \emph{real} polynomial. Add an appropriate type annotation if necessary. \item use a computer algebra system to ensure that the property is indeed correct \item if this did not help, send the statement in question to \texttt{eberlm@in.tum.de}; it may be a bug in the preprocessing of the proof method. \end{enumerate} \end{document} diff --git a/thys/WorkerWrapper/FixedPointTheorems.thy b/thys/WorkerWrapper/FixedPointTheorems.thy --- a/thys/WorkerWrapper/FixedPointTheorems.thy +++ b/thys/WorkerWrapper/FixedPointTheorems.thy @@ -1,271 +1,271 @@ (*<*) (* * The worker/wrapper transformation, following Gill and Hutton. * (C)opyright 2009-2011, Peter Gammie, peteg42 at gmail.com. * License: BSD *) theory FixedPointTheorems imports HOLCF begin setup \ - Thy_Output.antiquotation_raw \<^binding>\haskell\ (Scan.lift Args.name) + Document_Output.antiquotation_raw \<^binding>\haskell\ (Scan.lift Args.name) (fn _ => fn s => Latex.string ("\\" ^ "<" ^ s ^ "\\>")) \ (* LaTeXsugar fights with HOLCF syntax: at least cdot *) (* THEOREMS *) notation (Rule output) Pure.imp ("\<^latex>\\\mbox{}\\inferrule{\\mbox{\_\<^latex>\}}\\<^latex>\{\\mbox{\_\<^latex>\}}\") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" ("\<^latex>\\\mbox{}\\inferrule{\_\<^latex>\}\\<^latex>\{\\mbox{\_\<^latex>\}}\") "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\\\\\/ _") "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") (*>*) section\Fixed-point theorems for program transformation\ text\ We begin by recounting some standard theorems from the early days of denotational semantics. The origins of these results are lost to history; the interested reader can find some of it in \citet{Bekic:1969, Manna:1974, Greibach:1975, Stoy:1977, DBLP:books/daglib/0002432, Harel:1980, Plotkin:1983, Winskel:1993, DBLP:journals/toplas/Sangiorgi09}. \ subsection\The rolling rule\ text\ The \emph{rolling rule} captures what intuitively happens when we re-order a recursive computation consisting of two parts. This theorem dates from the 1970s at the latest -- see \citet[p210]{Stoy:1977} and \citet{Plotkin:1983}. The following proofs were provided by \citet{GillHutton:2009}. \ lemma rolling_rule_ltr: "fix\(g oo f) \ g\(fix\(f oo g))" proof - have "g\(fix\(f oo g)) \ g\(fix\(f oo g))" by (rule below_refl) \ \reflexivity\ hence "g\((f oo g)\(fix\(f oo g))) \ g\(fix\(f oo g))" using fix_eq[where F="f oo g"] by simp \ \computation\ hence "(g oo f)\(g\(fix\(f oo g))) \ g\(fix\(f oo g))" by simp \ \re-associate @{term "(oo)"}\ thus "fix\(g oo f) \ g\(fix\(f oo g))" using fix_least_below by blast \ \induction\ qed lemma rolling_rule_rtl: "g\(fix\(f oo g)) \ fix\(g oo f)" proof - have "fix\(f oo g) \ f\(fix\(g oo f))" by (rule rolling_rule_ltr) hence "g\(fix\(f oo g)) \ g\(f\(fix\(g oo f)))" by (rule monofun_cfun_arg) \ \g is monotonic\ thus "g\(fix\(f oo g)) \ fix\(g oo f)" using fix_eq[where F="g oo f"] by simp \ \computation\ qed lemma rolling_rule: "fix\(g oo f) = g\(fix\(f oo g))" by (rule below_antisym[OF rolling_rule_ltr rolling_rule_rtl]) (* This property of a fixed-point operator is termed \emph{dinaturality} by \citet{DBLP:conf/lics/SimpsonP00}. *) subsection\Least-fixed-point fusion\ text\ \label{sec:lfp-fusion} \emph{Least-fixed-point fusion} provides a kind of induction that has proven to be very useful in calculational settings. Intuitively it lifts the step-by-step correspondence between @{term "f"} and @{term "h"} witnessed by the strict function @{term "g"} to the fixed points of @{term "f"} and @{term "g"}: \[ \begin{diagram} \node{\bullet} \arrow{e,t}{h} \node{\bullet}\\ \node{\bullet} \arrow{n,l}{g} \arrow{e,b}{f} \node{\bullet} \arrow{n,r}{g} \end{diagram} \qquad \Longrightarrow \qquad \begin{diagram} \node{\mathsf{fix}\ h}\\ \node{\mathsf{fix}\ f} \arrow{n,r}{g} \end{diagram} \] \citet*{FokkingaMeijer:1991}, and also their later \citet*{barbed-wire:1991}, made extensive use of this rule, as did \citet{Tullsen:PhDThesis} in his program transformation tool PATH. This diagram is strongly reminiscent of the simulations used to establish refinement relations between imperative programs and their specifications \citep*{EdR:cup98}. The following proof is close to the third variant of \citet[p215]{Stoy:1977}. We relate the two fixpoints using the rule \texttt{parallel\_fix\_ind}: \begin{center} @{thm[mode=Rule] parallel_fix_ind} \end{center} in a very straightforward way: \ lemma lfp_fusion: assumes "g\\ = \" assumes "g oo f = h oo g" shows "g\(fix\f) = fix\h" proof(induct rule: parallel_fix_ind) case 2 show "g\\ = \" by fact case (3 x y) from \g\x = y\ \g oo f = h oo g\ show "g\(f\x) = h\y" by (simp add: cfun_eq_iff) qed simp text\ This lemma also goes by the name of \emph{Plotkin's axiom} \citep{PittsAM:relpod} or \emph{uniformity} \citep{DBLP:conf/lics/SimpsonP00}. \ (*<*) (* The rest of this theory is only of historical interest. *) text \Some may find the pointed version easier to read.\ lemma lfp_fusion_pointed: assumes Cfg: "\f. C\(F\f) = G\(C\f)" and strictC: "C\\ = \" shows "C\(fix\F) = fix\G" using lfp_fusion[where f=F and g=C and h=G] assms by (simp add: cfcomp1) subsubsection\More about \lfp-fusion\\ text\ Alternative proofs. This is the ``intuitive'' one \citet[p125]{Gunter:1992} and \citet[p46]{Tullsen:PhDThesis}, where we can shuffle @{term "g"} to the end of the the iteration of @{term "f"} using @{term "fgh"}. \ lemma lfp_fusion2_aux: assumes fgh: "g oo f = h oo g" shows "g\(iterate i\f\\) = iterate i\h\(g\\)" proof(induct i) case (Suc i) have "g\(iterate (Suc i)\f\\) = (g oo f)\(iterate i\f\\)" by simp also have "... = h\(g\(iterate i\f\\))" using fgh by (simp add: cfcomp1) also have "... = h\(iterate i\h\(g\\))" using Suc by simp also have "... = iterate (Suc i)\h\(g\\)" by simp finally show ?case . qed simp lemma lfp_fusion2: assumes fgh: "g oo f = h oo g" and strictg: "g\\ = \" shows "g\(fix\f) = fix\h" proof - have "g\(fix\f) = g\(\i. iterate i\f\\)" by (simp only: fix_def2) also have "... = (\i. g\(iterate i\f\\))" by (simp add: contlub_cfun_arg) also have "... = (\i. (iterate i\h\(g\\)))" by (simp only: lfp_fusion2_aux[OF fgh]) also have "... = fix\h" using strictg by (simp only: fix_def2) finally show ?thesis . qed text\This is the first one by \citet[p213]{Stoy:1977}, almost identical to the above.\ lemma lfp_fusion3_aux: assumes fgh: "g oo f = h oo g" and strictg: "g\\ = \" shows "g\(iterate i\f\\) = iterate i\h\\" proof(induct i) case 0 from strictg show ?case by simp next case (Suc i) have "g\(iterate (Suc i)\f\\) = (g oo f)\(iterate i\f\\)" by simp also have "... = h\(g\(iterate i\f\\))" using fgh by (simp add: cfcomp1) also have "... = h\(iterate i\h\\)" using Suc by simp also have "... = iterate (Suc i)\h\\" by simp finally show ?case . qed lemma lfp_fusion3: assumes fgh: "g oo f = h oo g" and strictg: "g\\ = \" shows "g\(fix\f) = fix\h" proof - have "g\(fix\f) = g\(\i. iterate i\f\\)" by (simp only: fix_def2) also have "... = (\i. g\(iterate i\f\\))" by (simp add: contlub_cfun_arg) also have "... = (\i. (iterate i\h\\))" by (simp only: lfp_fusion3_aux[OF fgh strictg]) also have "... = fix\h" by (simp only: fix_def2) finally show ?thesis . qed text\Stoy's second proof \citep[p214]{Stoy:1977} is similar to the original proof using fixed-point induction.\ lemma lfp_fusion4: assumes fgh: "g oo f = h oo g" and strictg: "g\\ = \" shows "g\(fix\f) = fix\h" proof(rule below_antisym) show "fix\h \ g\(fix\f)" proof - have "h\(g\(fix\f)) = (g oo f)\(fix\f)" using fgh by simp also have "... = g\(fix\f)" by (subst fix_eq, simp) finally show ?thesis by (rule fix_least) qed let ?P = "\x. g\x \ fix\h" show "?P (fix\f)" proof(induct rule: fix_ind[where P="?P"]) case 2 with strictg show ?case by simp next case (3 x) hence indhyp: "g\x \ fix\h" . have "g\(f\x) = (h oo g)\x" using fgh[symmetric] by simp with indhyp show "g\(f\x) \ fix\h" by (subst fix_eq, simp add: monofun_cfun) qed simp qed text\A wrinkly variant from \citet[p11]{barbed-wire:1991}.\ lemma lfp_fusion_barbed_variant: assumes ff': "f\\ = f'\\" and fgh: "f oo g = h oo f" and f'g'h: "f' oo g' = h oo f'" shows "f\(fix\g) = f'\(fix\g')" proof(induct rule: parallel_fix_ind) case 2 show "f\\ = f'\\" by (rule ff') case (3 x y) from \f\x = f'\y\ have "h\(f\x) = h\(f'\y)" by simp with fgh f'g'h have "f\(g\x) = f'\(g'\y)" using cfcomp2[where f="f" and g="g", symmetric] cfcomp2[where f="f'" and g="g'", symmetric] by simp thus ?case by simp qed simp (*>*) (*<*) end (*>*)