diff --git a/thys/Isabelle_C/C11-FrontEnd/examples/C1.thy b/thys/Isabelle_C/C11-FrontEnd/examples/C1.thy --- a/thys/Isabelle_C/C11-FrontEnd/examples/C1.thy +++ b/thys/Isabelle_C/C11-FrontEnd/examples/C1.thy @@ -1,864 +1,864 @@ (****************************************************************************** * 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 \Example: Annotation Navigation and Context Serialization\ theory C1 imports "../C_Main" "HOL-ex.Cartouche_Examples" begin text \ Operationally, the \<^theory_text>\C\ command can be thought of as behaving as \<^theory_text>\ML\, where it is for example possible to recursively nest C code in C. Generally, the present chapter assumes a familiarity with all advance concepts of ML as described in \<^file>\~~/src/HOL/Examples/ML.thy\, as well as the concept of ML antiquotations (\<^file>\~~/src/Doc/Implementation/ML.thy\). However, even if \<^theory_text>\C\ might resemble to \<^theory_text>\ML\, we will now see in detail that there are actually subtle differences between the two commands.\ section \Setup of ML Antiquotations Displaying the Environment (For Debugging) \ ML\ fun print_top make_string f _ (_, (value, _, _)) _ = tap (fn _ => writeln (make_string value)) o f fun print_top' _ f _ _ env = tap (fn _ => writeln ("ENV " ^ C_Env.string_of env)) o f fun print_stack s make_string stack _ _ thy = let val () = Output.information ("SHIFT " ^ (case s of NONE => "" | SOME s => "\"" ^ s ^ "\" ") ^ Int.toString (length stack - 1) ^ " +1 ") val () = stack |> split_list |> #2 |> map_index I |> app (fn (i, (value, pos1, pos2)) => writeln (" " ^ Int.toString (length stack - i) ^ " " ^ make_string value ^ " " ^ Position.here pos1 ^ " " ^ Position.here pos2)) in thy end fun print_stack' s _ stack _ env thy = let val () = Output.information ("SHIFT " ^ (case s of NONE => "" | SOME s => "\"" ^ s ^ "\" ") ^ Int.toString (length stack - 1) ^ " +1 ") val () = writeln ("ENV " ^ C_Env.string_of env) in thy end \ setup \ML_Antiquotation.inline @{binding print_top} (Args.context >> K ("print_top " ^ ML_Pretty.make_string_fn ^ " I"))\ setup \ML_Antiquotation.inline @{binding print_top'} (Args.context >> K ("print_top' " ^ ML_Pretty.make_string_fn ^ " I"))\ setup \ML_Antiquotation.inline @{binding print_stack} (Scan.peek (fn _ => Scan.option Args.text) >> (fn name => ("print_stack " ^ (case name of NONE => "NONE" | SOME s => "(SOME \"" ^ s ^ "\")") ^ " " ^ ML_Pretty.make_string_fn)))\ setup \ML_Antiquotation.inline @{binding print_stack'} (Scan.peek (fn _ => Scan.option Args.text) >> (fn name => ("print_stack' " ^ (case name of NONE => "NONE" | SOME s => "(SOME \"" ^ s ^ "\")") ^ " " ^ ML_Pretty.make_string_fn)))\ declare[[C_lexer_trace]] section \Introduction to C Annotations: Navigating in the Parsing Stack\ subsection \Basics\ text \ Since the present theory \<^file>\C1.thy\ is depending on \<^theory>\Isabelle_C.C_Lexer_Language\ and \<^theory>\Isabelle_C.C_Parser_Language\, the syntax one is writing in the \<^theory_text>\C\ command is C11. Additionally, \<^file>\C1.thy\ also depends on \<^theory>\Isabelle_C.C_Parser_Annotation\, making it possible to write commands in C comments, called annotation commands, such as \<^theory_text>\\setup\. \ C \ \Nesting ML code in C comments\ \ int a = (((0))); /*@ highlight */ /*@ \setup \@{print_stack}\ */ /*@ \setup \@{print_top}\ */ \ text \ In terms of execution order, nested annotation commands are not pre-filtered out of the C code, but executed when the C code is still being parsed. Since the parser implemented is a LALR parser \<^footnote>\\<^url>\https://en.wikipedia.org/wiki/LALR\\, C tokens are uniquely read and treated from left to right. Thus, each nested command is (supposed by default to be) executed when the parser has already read all C tokens before the comment associated to the nested command, so when the parser is in a particular intermediate parsing step (not necessarily final) \<^footnote>\\<^url>\https://en.wikipedia.org/wiki/Shift-reduce_parser\\. \ text \The command \<^theory_text>\\setup\ is similar to the command \<^theory_text>\setup\ except that the former takes a function with additional arguments. These arguments are precisely depending on the current parsing state. To better examine these arguments, it is convenient to use ML antiquotations (be it for printing, or for doing any regular ML actions like PIDE reporting). Note that, in contrast with \<^theory_text>\setup\, the return type of the \<^theory_text>\\setup\ function is not \<^ML_type>\theory -> theory\ but \<^ML_type>\Context.generic -> Context.generic\. \ C \ \Positional navigation: referring to any previous parsed sub-tree in the stack\ \ int a = (((0 + 5))) /*@@ \setup \print_top @{make_string} I\ @ highlight */ * 4; float b = 7 / 3; \ text \The special \@\ symbol makes the command be executed whenever the first element \E\ in the stack is about to be irremediably replaced by a more structured parent element (having \E\ as one of its direct children). It is the parent element which is provided to the ML code. Instead of always referring to the first element of the stack, \N\ consecutive occurrences of \@\ will make the ML code getting as argument the direct parent of the \N\-th element.\ C \ \Positional navigation: referring to any previous parsed sub-tree in the stack\ \ int a = (((0 + 5))) /*@@ highlight */ * 4; int a = (((0 + 5))) /*@& highlight */ * 4; int a = (((0 + 5))) /*@@@@@ highlight */ * 4; int a = (((0 + 5))) /*@&&&& highlight */ * 4; \ text \\&\ behaves as \@\, but instead of always giving the designated direct parent to the ML code, it finds the first parent ancestor making non-trivial changes in the respective grammar rule (a non-trivial change can be for example the registration of the position of the current AST node being built).\ C \ \Positional navigation: moving the comment after a number of C token\ \ int b = 7 / (3) * 50; /*@+++@@ highlight */ long long f (int a) { while (0) { return 0; } } int b = 7 / (3) * 50; \ text \\N\ consecutive occurrences of \+\ will delay the interpretation of the comment, which is ignored at the place it is written. The comment is only really considered after the C parser has treated \N\ more tokens.\ C \ \Closing C comments \*/\ must close anything, even when editing ML code\ \ int a = (((0 //@ (* inline *) \setup \fn _ => fn _ => fn _ => fn context => let in (* */ *) context end\ /*@ \setup \(K o K o K) I\ (* * / *) */ ))); \ C \ \Inline comments with antiquotations\ \ /*@ \setup\(K o K o K) (fn x => K x @{con\ text (**)})\ */ // break of line activated everywhere (also in antiquotations) int a = 0; //\ @ \setup\(K o K o K) (fn x => K x @{term \a \ + b\ (* (**) *\ \ )})\ \ subsection \Erroneous Annotations Treated as Regular C Comments\ C \ \Permissive Types of Antiquotations\ \ int a = 0; /*@ \setup (* Errors: Explicit warning + Explicit markup reporting *) */ /** \setup (* Errors: Turned into tracing report information *) */ /** \setup \fn _ => fn _ => fn _ => I\ (* An example of correct syntax accepted as usual *) */ \ C \ \Permissive Types of Antiquotations\ \ int a = 0; /*@ \setup \fn _ => fn _ => fn _ => I\ \setup (* Parsing error of a single command does not propagate to other commands *) \setup \fn _ => fn _ => fn _ => I\ context */ /** \setup \fn _ => fn _ => fn _ => I\ \setup (* Parsing error of a single command does not propagate to other commands *) \setup \fn _ => fn _ => fn _ => I\ context */ /*@ \setup (* Errors in all commands are all rendered *) \setup (* Errors in all commands are all rendered *) \setup (* Errors in all commands are all rendered *) */ /** \setup (* Errors in all commands makes the whole comment considered as an usual comment *) \setup (* Errors in all commands makes the whole comment considered as an usual comment *) \setup (* Errors in all commands makes the whole comment considered as an usual comment *) */ \ subsection \Bottom-Up vs. Top-Down Evaluation\ ML\ structure Example_Data = Generic_Data (type T = string list - val empty = [] val extend = K empty val merge = K empty) + val empty = [] val extend = I val merge = K empty) fun add_ex s1 s2 = Example_Data.map (cons s2) #> (fn context => let val () = Output.information (s1 ^ s2) val () = app (fn s => writeln (" Data content: " ^ s)) (Example_Data.get context) in context end) \ setup \Context.theory_map (Example_Data.put [])\ declare[[ML_source_trace]] declare[[C_parser_trace]] C \ \Arbitrary interleaving of effects: \\setup\ vs \\setup\\\ \ int b,c,d/*@@ \setup \fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "3_print_top"\ */,e = 0; /*@@ \setup \fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "4_print_top"\ */ int b,c,d/*@@ \setup\ \fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "6_print_top"\ */,e = 0; /*@@ \setup\ \fn s => fn x => fn env => @{print_top} s x env #> add_ex "evaluation of " "5_print_top"\ */ \ section \Reporting of Positions and Contextual Update of Environment\ text \ To show the content of the parsing environment, the ML antiquotations \print_top'\ and \print_stack'\ will respectively be used instead of \print_top\ and \print_stack\. This example suite allows to explore the bindings represented in the C environment and made accessible in PIDE for hovering. \ subsection \Reporting: \typedef\, \enum\\ (*\struct\*) declare [[ML_source_trace = false]] declare [[C_lexer_trace = false]] C \ \Reporting of Positions\ \ typedef int i, j; /*@@ \setup \@{print_top'}\ @highlight */ //@ +++++@ \setup \@{print_top'}\ +++++@highlight int j = 0; typedef int i, j; j jj1 = 0; j jj = jj1; j j = jj1 + jj; typedef i j; typedef i j; typedef i j; i jj = jj; j j = jj; \ C \ \Nesting type definitions\ \ typedef int j; j a = 0; typedef int k; int main (int c) { j b = 0; typedef int k; typedef k l; k a = c; l a = 0; } k a = a; \ C \ \Reporting \enum\\ \ enum a b; // bound case: undeclared enum a {aaa}; // define case enum a {aaa}; // define case: redefined enum a _; // bound case __thread (f ( enum a, enum a vv)); enum a /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.function_definition4\\*/ f (enum a a) { } __thread enum a /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.declaration_specifier2\\*/ f (enum a a) { enum c {ccc}; // define case __thread enum c f (enum c a) { return 0; } enum c /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.nested_function_definition2\\*/ f (enum c a) { return 0; } return 0; } enum z {zz}; // define case int main (enum z *x) /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.parameter_type_list2\\*/ { return zz; } int main (enum a *x, ...) /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.parameter_type_list3\\*/ { return zz; } \ subsection \Continuation Calculus with the C Environment: Presentation in ML\ declare [[C_parser_trace = false]] ML\ val C = tap o C_Module.C val C' = C_Module.C' \ C \ \Nesting C code without propagating the C environment\ \ int a = 0; int b = 7 / (3) * 50 /*@@@@@ \setup \fn _ => fn _ => fn _ => C \int b = a + a + a + a + a + a + a ;\ \ */; \ C \ \Nesting C code and propagating the C environment\ \ int a = 0; int b = 7 / (3) * 50 /*@@@@@ \setup \fn _ => fn _ => fn env => C' env \int b = a + a + a + a + a + a + a ;\ \ */; \ subsection \Continuation Calculus with the C Environment: Presentation with Outer Commands\ ML\ val _ = Theory.setup (C_Inner_Syntax.command0 (fn src => fn context => C' (C_Stack.Data_Lang.get' context |> #2) src context) C_Parse.C_source ("C'", \<^here>, \<^here>, \<^here>)) \ C \ \Nesting C code without propagating the C environment\ \ int f (int a) { int b = 7 / (3) * 50 /*@ C \int b = a + a + a + a + a + a + a;\ */; int c = b + a + a + a + a + a + a; } \ C \ \Nesting C code and propagating the C environment\ \ int f (int a) { int b = 7 / (3) * 50 /*@ C' \int b = a + a + a + a + a + a + a;\ */; int c = b + b + b + b + a + a + a + a + a + a; } \ C \ \Miscellaneous\ \ int f (int a) { int b = 7 / (3) * 50 /*@ C \int b = a + a + a + a + a; //@ C' \int c = b + b + b + b + a;\ \ */; int b = 7 / (3) * 50 /*@ C' \int b = a + a + a + a + a; //@ C' \int c = b + b + b + b + a;\ \ */; int c = b + b + b + b + a + a + a + a + a + a; } \ subsection \Continuation Calculus with the C Environment: Deep-First Nesting vs Breadth-First Folding: Propagation of \<^ML_type>\C_Env.env_lang\\ C \ \Propagation of report environment while manually composing at ML level (with \#>\)\ \ \In \c1 #> c2\, \c1\ and \c2\ should not interfere each other.\ \ //@ ML \fun C_env src _ _ env = C' env src\ int a; int f (int b) { int c = 0; /*@ \setup \fn _ => fn _ => fn env => C' env \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ #> C \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ #> C' env \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ #> C \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ \ */ int e = a + b + c + d; }\ C \ \Propagation of directive environment (evaluated before parsing) to any other annotations (evaluated at parsing time)\ \ #undef int #define int(a,b) int #define int int int a; int f (int b) { int c = 0; /*@ \setup \fn _ => fn _ => fn env => C' env \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ #> C \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ #> C' env \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ #> C \int d = a + b + c + d; //@ \setup \C_env \int e = a + b + c + d;\\\ \ */ #undef int int e = a + b + c + d; } \ subsection \Continuation Calculus with the C Environment: Deep-First Nesting vs Breadth-First Folding: Propagation of \<^ML_type>\C_Env.env_tree\\ ML\ structure Data_Out = Generic_Data (type T = int val empty = 0 - val extend = K empty + val extend = I val merge = K empty) fun show_env0 make_string f msg context = Output.information ("(" ^ msg ^ ") " ^ make_string (f (Data_Out.get context))) val show_env = tap o show_env0 @{make_string} I \ setup \Context.theory_map (C_Module.Data_Accept.put (fn _ => fn _ => Data_Out.map (fn x => x + 1)))\ C \ \Propagation of Updates\ \ typedef int i, j; int j = 0; typedef int i, j; j jj1 = 0; j jj = jj1; /*@@ \setup \fn _ => fn _ => fn _ => show_env "POSITION 0"\ @\setup \@{print_top'}\ */ typedef int k; /*@@ \setup \fn _ => fn _ => fn env => C' env \k jj = jj; //@@ \setup \@{print_top'}\ k jj = jj + jj1; typedef k l; //@@ \setup \@{print_top'}\\ #> show_env "POSITION 1"\ */ j j = jj1 + jj; //@@ \setup \@{print_top'}\ typedef i j; /*@@ \setup \fn _ => fn _ => fn _ => show_env "POSITION 2"\ */ typedef i j; typedef i j; i jj = jj; j j = jj; \ ML\show_env "POSITION 3" (Context.Theory @{theory})\ setup \Context.theory_map (C_Module.Data_Accept.put (fn _ => fn _ => I))\ subsection \Reporting: Scope of Recursive Functions\ declare [[C_starting_env = last]] C \ \Propagation of Updates\ \ int a = 0; int b = a * a + 0; int jjj = b; int main (void main(int *x,int *y),int *jjj) { return a + jjj + main(); } int main2 () { int main3 () { main2() + main(); } int main () { main2() + main(); } return a + jjj + main3() + main(); } \ C \ int main3 () { main2 (); } \ declare [[C_starting_env = empty]] subsection \Reporting: Extensions to Function Types, Array Types\ C \int f (int z);\ C \int * f (int z);\ C \int (* f) (int z /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.declarator1\\*/);\ C \typedef int (* f) (int z);\ C \int f (int z) {}\ C \int * f (int z) {return z;}\ C \int ((* f) (int z1, int z2)) {return z1 + z2;}\ C \int (* (* f) (int z1, int z2)) {return z1 + z2;}\ C \typedef int (* f) (int z); f uuu (int b) {return b;};\ C \typedef int (* (* f) (int z, int z)) (int a); f uuu (int b) {return b;};\ C \struct z { int (* f) (int z); int (* (* ff) (int z)) (int a); };\ C \double (* (* f (int a /* \\ \\<^ML>\C_Grammar_Rule_Wrap_Overloading.declarator1\\*/)) (int a, double d)) (char a);\ C \double (* (((* f) []) (int a)) (int b, double c)) (char d) {int a = b + c + d;}\ C \double ((*((f) (int a))) (int a /* \\ \\<^ML>\C_Grammar_Rule_Lib.doFuncParamDeclIdent\\*/, double)) (char c) {int a = 0;}\ C \ \Nesting functions\ \ double (* (* f (int a)) (int a, double)) (char c) { double (* (* f (int a)) (double a, int a)) (char) { return a; } } \ C \ \Old function syntax\ \ f (x) int x; {return x;} \ section \General Isar Commands\ locale zz begin definition "z' = ()" end C \ \Mixing arbitrary commands\ \ int a = 0; int b = a * a + 0; int jjj = b; /*@ @@@ ML \@{lemma \A \ B \ B \ A\ by (ml_tactic \blast_tac ctxt 1\)}\ definition "a' = ()" declare [[ML_source_trace]] lemma (in zz) \A \ B \ B \ A\ by (ml_tactic \blast_tac ctxt 1\) definition (in zz) "z = ()" corollary "zz.z' = ()" apply (unfold zz.z'_def) by blast theorem "True &&& True" by (auto, presburger?) */ \ declare [[ML_source_trace = false]] C \ \Backslash newlines must be supported by \<^ML>\C_Token.syntax'\ (in particular in keywords)\ \ //@ lem\ ma (i\ n z\ z) \ \\ AA \ B\ \\ B \ A\ \ A\ b\ y (ml_t\ actic \\ bla\ st_tac c\ txt\ 0\ 001\) \ section \Starting Parsing Rule\ subsection \Basics\ C \ \Parameterizing starting rule\ \ /*@ declare [[C_starting_rule = "statement"]] C \while (a) {}\ C \a = 2;\ declare [[C_starting_rule = "expression"]] C \2 + 3\ C \a = 2\ C \a[1]\ C \&a\ C \a\ */ \ subsection \Embedding in Inner Terms\ term \\<^C> \ \default behavior of parsing depending on the activated option\ \0\\ term \\<^C>\<^sub>u\<^sub>n\<^sub>i\<^sub>t \ \force the explicit parsing\ \f () {while (a) {}; return 0;} int a = 0;\\ term \\<^C>\<^sub>d\<^sub>e\<^sub>c\<^sub>l \ \force the explicit parsing\ \int a = 0; \\ term \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r \ \force the explicit parsing\ \a\\ term \\<^C>\<^sub>s\<^sub>t\<^sub>m\<^sub>t \ \force the explicit parsing\ \while (a) {}\\ declare [[C_starting_rule = "translation_unit"]] term \\<^C> \ \default behavior of parsing depending on the current option\ \int a = 0;\\ subsection \User Defined Setup of Syntax\ setup \C_Module.C_Term.map_expression (fn _ => fn _ => fn _ => @{term "10 :: nat"})\ setup \C_Module.C_Term.map_statement (fn _ => fn _ => fn _ => @{term "20 :: nat"})\ value \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\1\ + \<^C>\<^sub>s\<^sub>t\<^sub>m\<^sub>t\for (;;);\\ setup \ \redefinition\ \C_Module.C_Term.map_expression (fn _ => fn _ => fn _ => @{term "1000 :: nat"})\ value \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\1\ + \<^C>\<^sub>s\<^sub>t\<^sub>m\<^sub>t\for (;;);\\ setup \C_Module.C_Term.map_default (fn _ => fn _ => fn _ => @{term "True"})\ subsection \Validity of Context for Annotations\ ML \fun fac x = if x = 0 then 1 else x * fac (x - 1)\ ML \ \Execution of annotations in term possible in (the outermost) \<^theory_text>\ML\\ \ \<^term>\ \<^C> \int c = 0; /*@ ML \fac 100\ */\ \ \ definition \ \Execution of annotations in term possible in \<^ML_type>\local_theory\ commands (such as \<^theory_text>\definition\)\ \ term = \<^C> \int c = 0; /*@ ML \fac 100\ */\ \ section \Scopes of Inner and Outer Terms\ ML \ local fun bind scan ((stack1, (to_delay, stack2)), _) = C_Parse.range scan >> (fn (src, range) => C_Env.Parsing ( (stack1, stack2) , ( range , C_Inner_Syntax.bottom_up (fn _ => fn context => ML_Context.exec (tap (fn _ => Syntax.read_term (Context.proof_of context) (Token.inner_syntax_of src))) context) , Symtab.empty , to_delay))) in val _ = Theory.setup ( C_Annotation.command' ("term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r", \<^here>) "" (bind (C_Token.syntax' (Parse.token Parse.cartouche))) #> C_Inner_Syntax.command0 (C_Inner_Toplevel.keep'' o C_Inner_Isar_Cmd.print_term) (C_Token.syntax' (Scan.succeed [] -- Parse.term)) ("term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r", \<^here>, \<^here>, \<^here>)) end \ C \ int z = z; /*@ C \//@ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ C' \//@ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ C \//@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ C' \//@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ */\ term(*outer*) \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ C \ int z = z; /*@ C \//@ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ C' \//@ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ C \//@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ C' \//@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ */\ term(*outer*) \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ declare [[C_starting_env = last]] C \ int z = z; /*@ C \//@ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ C' \//@ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ C \//@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ C' \//@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\\ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ */\ term(*outer*) \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\z\\ declare [[C_starting_env = empty]] C \ \Propagation of report environment while manually composing at ML level\ \ int a; int f (int b) { int c = 0; /*@ \setup \fn _ => fn _ => fn env => C' env \int d = a + b + c + d; //@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\\ #> C \int d = a + b + c + d; //@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\\ #> C' env \int d = a + b + c + d; //@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\\ #> C \int d = a + b + c + d; //@ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\\ \ term\<^sub>i\<^sub>n\<^sub>n\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\ term\<^sub>o\<^sub>u\<^sub>t\<^sub>e\<^sub>r \\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\c\ + \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\d\\ */ int e = a + b + c + d; }\ section \Calculation in Directives\ subsection \Annotation Command Classification\ C \ \Lexing category vs. parsing category\ \ int a = 0; // \ \Category 2: only parsing\ //@ \setup \K (K (K I))\ (* evaluation at parsing *) //@@ \setup\ \K (K (K I))\ (* evaluation at parsing *) //@ highlight (* evaluation at parsing *) //@@ highlight\ (* evaluation at parsing *) // \ \Category 3: with lexing\ //@ #setup I (* evaluation at lexing (and directives resolving) *) //@ setup I (* evaluation at parsing *) //@@ setup\ I (* evaluation at parsing *) //@ #ML I (* evaluation at lexing (and directives resolving) *) //@ ML I (* evaluation at parsing *) //@@ ML\ I (* evaluation at parsing *) //@ #C \\ (* evaluation at lexing (and directives resolving) *) //@ C \\ (* evaluation at parsing *) //@@ C\ \\ (* evaluation at parsing *) \ C \ \Scheduling example\ \ //@+++++ ML \writeln "2"\ int a = 0; //@@ ML\ \writeln "3"\ //@ #ML \writeln "1"\ \ C \ \Scheduling example\ \ //* lemma True by simp //* #lemma True #by simp //* #lemma True by simp //* lemma True #by simp \ C \ \Scheduling example\ \ /*@ lemma \1 = one\ \2 = two\ \two + one = three\ by auto #definition [simp]: \three = 3\ #definition [simp]: \two = 2\ #definition [simp]: \one = 1\ */ \ subsection \Generalizing ML Antiquotations with C Directives\ ML \ structure Directive_setup_define = Generic_Data (type T = int val empty = 0 - val extend = K empty + val extend = I val merge = K empty) fun setup_define1 pos f = C_Directive.setup_define pos (fn toks => fn (name, (pos1, _)) => tap (fn _ => writeln ("Executing " ^ name ^ Position.here pos1 ^ " (only once)")) #> pair (f toks)) (K I) fun setup_define2 pos = C_Directive.setup_define pos (K o pair) \ C \ \General scheme of C antiquotations\ \ /*@ #setup \ \Overloading \#define\\ \ setup_define2 \<^here> (fn (name, (pos1, _)) => op ` Directive_setup_define.get #>> (case name of "f3" => curry op * 152263 | _ => curry op + 1) #> tap (fn (nb, _) => tracing ("Executing antiquotation " ^ name ^ Position.here pos1 ^ " (number = " ^ Int.toString nb ^ ")")) #> uncurry Directive_setup_define.put) \ */ #define f1 #define f2 int a = 0; #define f3 f1 f2 f1 f3 //@ #setup \ \Resetting \#define\\ \setup_define2 \<^here> (K I)\ f3 #define f3 f3 \ C \ \Dynamic token computing in \#define\\ \ //@ #setup \setup_define1 \<^here> (K [])\ #define f int a = 0; f f f f //@ #setup \setup_define1 \<^here> (fn toks => toks @ toks)\ #define f int b = a; f f //@ #setup \setup_define1 \<^here> I\ #define f int a = 0; f f \ section \Miscellaneous\ C \ \Antiquotations acting on a parsed-subtree\ \ # /**/ include // backslash rendered unescaped f(){0 + 0;} /**/ // val _ : theory => 'a => theory # /* context */ if if elif #include if then else ; # /* zzz */ elif /**/ #else\ #define FOO 00 0 "" (( FOO(FOO(a,b,c)) #endif\ C \ \Header-names in directives\ \ #define F #define G "stdio\h" // expecting an error whenever expanded #define H "stdio_h" // can be used anywhere without errors int f = /*F*/ ""; int g = /*G*/ ""; int h = H ""; #include F \ C \ \Parsing tokens as directives only when detecting space symbols before \#\\ \/* */ \ \ // # /* */ define /**/ \ a a a /*#include <>*/ // must not be considered as a directive \ C \ \Universal character names in identifiers and Isabelle symbols\ \ #include int main () { char * ó\<^url>ò = "ó\<^url>ò"; printf ("%s", ó\<^url>ò); } \ end diff --git a/thys/Isabelle_C/C11-FrontEnd/examples/C2.thy b/thys/Isabelle_C/C11-FrontEnd/examples/C2.thy --- a/thys/Isabelle_C/C11-FrontEnd/examples/C2.thy +++ b/thys/Isabelle_C/C11-FrontEnd/examples/C2.thy @@ -1,502 +1,502 @@ (****************************************************************************** * 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 \Example: A Simple C Program with Directives and Annotations\ theory C2 imports "../C_Main" begin section \A Simplistic Setup: Parse and Store\ text\The following setup just stores the result of the parsed values in the environment.\ ML\ structure Data_Out = Generic_Data (type T = (C_Grammar_Rule.start_happy * C_Antiquote.antiq C_Env.stream) list val empty = [] - val extend = K empty + val extend = I val merge = K empty) fun get_module thy = let val context = Context.Theory thy in (Data_Out.get context |> map (apfst (C_Grammar_Rule.start_happy1 #> the)), C_Module.Data_In_Env.get context) end \ setup \Context.theory_map (C_Module.Data_Accept.put (fn ast => fn env_lang => Data_Out.map (cons (ast, #stream_ignored env_lang |> rev))))\ section \Example of a Possible Semantics for \#include\\ subsection \Implementation\ text \ The CPP directive \<^C>\#include _\ is used to import signatures of modules in C. This has the effect that imported identifiers are included in the C environment and, as a consequence, appear as constant symbols and not as free variables in the output. \ text \ The following structure is an extra mechanism to define the effect of \<^C>\#include _\ wrt. to its definition in its environment. \ ML \ structure Directive_include = Generic_Data (type T = (Input.source * C_Env.markup_ident) list Symtab.table val empty = Symtab.empty - val extend = K empty + val extend = I val merge = K empty) \ ML \ \\<^theory>\Pure\\ \ local fun return f (env_cond, env) = ([], (env_cond, f env)) val _ = Theory.setup (Context.theory_map (C_Context0.Directives.map (C_Context.directive_update ("include", \<^here>) ( (return o K I) , fn C_Lex.Include (C_Lex.Group2 (toks_bl, _, tok :: _)) => let fun exec file = if exists (fn C_Scan.Left _ => false | C_Scan.Right _ => true) file then K (error ("Unsupported character" ^ Position.here (Position.range_position (C_Lex.pos_of tok, C_Lex.end_pos_of (List.last toks_bl))))) else fn (env_lang, env_tree) => fold (fn (src, data) => fn (env_lang, env_tree) => let val (name, pos) = Input.source_content src in C_Grammar_Rule_Lib.shadowTypedef0'''' name [pos] data env_lang env_tree end) (these (Symtab.lookup (Directive_include.get (#context env_tree)) (String.concat (maps (fn C_Scan.Left s => [s] | _ => []) file)))) (env_lang, env_tree) in case tok of C_Lex.Token (_, (C_Lex.String (_, file), _)) => exec file | C_Lex.Token (_, (C_Lex.File (_, file), _)) => exec file | _ => tap (fn _ => (* not yet implemented *) warning ("Ignored directive" ^ Position.here (Position.range_position ( C_Lex.pos_of tok , C_Lex.end_pos_of (List.last toks_bl))))) end |> K |> K | _ => K (K I))))) in end \ ML \ structure Include = struct fun init name vars = Context.theory_map (Directive_include.map (Symtab.update (name, map (rpair {global = true, params = [], ret = C_Env.Previous_in_stack}) vars))) fun append name vars = Context.theory_map (Directive_include.map (Symtab.map_default (name, []) (rev o fold (cons o rpair {global = true, params = [], ret = C_Env.Previous_in_stack}) vars o rev))) val show = Context.theory_map (Directive_include.map (tap (Symtab.dest #> app (fn (fic, vars) => writeln ("Content of \"" ^ fic ^ "\": " ^ String.concat (map (fn (i, _) => let val (name, pos) = Input.source_content i in name ^ Position.here pos ^ " " end) vars)))))) end \ setup \Include.append "stdio.h" [\printf\, \scanf\]\ subsection \Tests\ C \ //@ setup \Include.append "tmp" [\b\]\ #include "tmp" int a = b; \ C \ int b = 0; //@ setup \Include.init "tmp" [\b\]\ #include "tmp" int a = b; \ C \ int c = 0; //@ setup \Include.append "tmp" [\c\]\ //@ setup \Include.append "tmp" [\c\]\ #include "tmp" int a = b + c; //@ setup \Include.show\ \ section \Working with Pragmas\ C\ #include #include /*sdfsdf */ #define a B #define b(C) #pragma /* just exists syntaxically */ \ text\In the following, we retrieve the C11 AST parsed above. \ ML\ val ((C_Ast.CTranslUnit0 (t,u), v)::R, env) = get_module @{theory}; val u = C_Grammar_Rule_Lib.decode u; C_Ast.CTypeSpec0; \ section \Working with Annotation Commands\ ML \ \\<^theory>\Isabelle_C.C_Command\\ \ \ \setup for a dummy ensures : the "Hello World" of Annotation Commands\ local datatype antiq_hol = Term of string (* term *) val scan_opt_colon = Scan.option (C_Parse.$$$ ":") fun msg cmd_name call_pos cmd_pos = tap (fn _ => tracing ("\Hello World\ reported by \"" ^ cmd_name ^ "\" here" ^ call_pos cmd_pos)) fun command (cmd as (cmd_name, _)) scan0 scan f = C_Annotation.command' cmd "" (fn (_, (cmd_pos, _)) => (scan0 -- (scan >> f) >> (fn _ => C_Env.Never |> msg cmd_name Position.here cmd_pos))) in val _ = Theory.setup ( C_Inner_Syntax.command_no_range (C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup \K (K (K I))\) ("loop", \<^here>, \<^here>) #> command ("ensures", \<^here>) scan_opt_colon C_Parse.term Term #> command ("invariant", \<^here>) scan_opt_colon C_Parse.term Term #> command ("assigns", \<^here>) scan_opt_colon C_Parse.term Term #> command ("requires", \<^here>) scan_opt_colon C_Parse.term Term #> command ("variant", \<^here>) scan_opt_colon C_Parse.term Term) end \ C\ /*@ ensures "result >= x && result >= y" */ int max(int x, int y) { if (x > y) return x; else return y; } \ ML\ val ((C_Ast.CTranslUnit0 (t,u), v)::R, env) = get_module @{theory}; val u = C_Grammar_Rule_Lib.decode u \ section \C Code: Various Examples\ text\This example suite is drawn from Frama-C and used in our GLA - TPs. \ C\ int sqrt(int a) { int i = 0; int tm = 1; int sum = 1; /*@ loop invariant "1 <= sum <= a+tm" loop invariant "(i+1)*(i+1) == sum" loop invariant "tm+(i*i) == sum" loop invariant "1<=tm<=sum" loop assigns "i, tm, sum" loop variant "a-sum" */ while (sum <= a) { i++; tm = tm + 2; sum = sum + tm; } return i; } \ C\ /*@ requires "n >= 0" requires "valid(t+(0..n-1))" ensures "exists integer i; (0<=i result == 0" ensures "(forall integer i; 0<=i t[i] == 0) <==> result == 1" assigns nothing */ int allzeros(int t[], int n) { int k = 0; /*@ loop invariant "0 <= k <= n" loop invariant "forall integer i; 0<=i t[i] == 0" loop assigns k loop variant "n-k" */ while(k < n) { if (t[k]) return 0; k = k + 1; } return 1; } \ C\ /*@ requires "n >= 0" requires "valid(t+(0..n-1))" ensures "(forall integer i; 0<=i t[i] != v) <==> result == -1" ensures "(exists integer i; 0<=i result == v" assigns nothing */ int binarysearch(int t[], int n, int v) { int l = 0; int u = n-1; /*@ loop invariant false */ while (l <= u) { int m = (l + u) / 2; if (t[m] < v) { l = m + 1; } else if (t[m] > v) { u = m - 1; } else return m; } return -1; } \ C\ /*@ requires "n >= 0" requires "valid(t+(0..n-1))" requires "(forall integer i,j; 0<=i<=j t[i] <= t[j])" ensures "exists integer i; (0<=i result == 1" ensures "(forall integer i; 0<=i t[i] != x) <==> result == 0" assigns nothing */ int linearsearch(int x, int t[], int n) { int i = 0; /*@ loop invariant "0<=i<=n" loop invariant "forall integer j; 0<=j (t[j] != x)" loop assigns i loop variant "n-i" */ while (i < n) { if (t[i] < x) { i++; } else { return (t[i] == x); } } return 0; } \ section \C Code: A Sorting Algorithm\ C\ #include int main() { int array[100], n, c, d, position, swap; printf("Enter number of elements\n"); scanf("%d", &n); printf("Enter %d integers\n", n); for (c = 0; c < n; c++) scanf("%d", &array[c]); for (c = 0; c < (n - 1); c++) { position = c; for (d = c + 1; d < n; d++) { if (array[position] > array[d]) position = d; } if (position != c) { swap = array[c]; array[c] = array[position]; array[position] = swap; } } printf("Sorted list in ascending order:\n"); for (c = 0; c < n; c++) printf("%d\n", array[c]); return 0; } \ text\A better example implementation:\ C\ #include #include #define SIZE 10 void swap(int *x,int *y); void selection_sort(int* a, const int n); void display(int a[],int size); void main() { int a[SIZE] = {8,5,2,3,1,6,9,4,0,7}; int i; printf("The array before sorting:\n"); display(a,SIZE); selection_sort(a,SIZE); printf("The array after sorting:\n"); display(a,SIZE); } /* swap two integers */ void swap(int *x,int *y) { int temp; temp = *x; *x = *y; *y = temp; } /* perform selection sort */ void selection_sort(int* a,const int size) { int i, j, min; for (i = 0; i < size - 1; i++) { min = i; for (j = i + 1; j < size; j++) { if (a[j] < a[min]) { min = j; } } swap(&a[i], &a[min]); } } /* display array content */ void display(int a[],const int size) { int i; for(i=0; i text\Accessing the underlying C11-AST's via the ML Interface.\ ML\ local open C_Ast in val _ = CTranslUnit0 val ((CTranslUnit0 (t,u), v)::_, _) = get_module @{theory}; val u = C_Grammar_Rule_Lib.decode u val _ = case u of Left (p1,p2) => writeln (Position.here p1 ^ " " ^ Position.here p2) | Right _ => error "Not expecting that value" val CDeclExt0(x1)::_ = t; val _ = CDecl0 end \ section \C Code: Floats Exist\ C\ int a; float b; int m() {return 0;} \ end \ No newline at end of file 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 = K 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 = K empty + 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) = Named_Target.switch 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 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 "C_file" --| 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_Eval.thy b/thys/Isabelle_C/C11-FrontEnd/src/C_Eval.thy --- a/thys/Isabelle_C/C11-FrontEnd/src/C_Eval.thy +++ b/thys/Isabelle_C/C11-FrontEnd/src/C_Eval.thy @@ -1,767 +1,767 @@ (****************************************************************************** * 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 \Evaluation Scheduling\ theory C_Eval imports C_Parser_Language C_Parser_Annotation begin subsection \Evaluation Engine for the Core Language\ \ \\<^file>\~~/src/Pure/Thy/thy_info.ML\: \<^theory>\Isabelle_C.C_Parser_Language\\ ML \ \\<^theory>\Isabelle_C.C_Environment\\ \ structure C_Stack = struct type 'a stack_elem = (LALR_Table.state, 'a, Position.T) C_Env.stack_elem0 type stack_data = (LALR_Table.state, C_Grammar.Tokens.svalue0, Position.T) C_Env.stack0 type stack_data_elem = (LALR_Table.state, C_Grammar.Tokens.svalue0, Position.T) C_Env.stack_elem0 fun map_svalue0 f (st, (v, pos1, pos2)) = (st, (f v, pos1, pos2)) structure Data_Lang = struct val empty' = ([], C_Env.empty_env_lang) structure Data_Lang = Generic_Data (type T = (stack_data * C_Env.env_lang) option val empty = NONE - val extend = K empty + val extend = I val merge = K empty) open Data_Lang fun get' context = case get context of NONE => empty' | SOME data => data fun setmp data f context = put (get context) (f (put data context)) end structure Data_Tree_Args : GENERIC_DATA_ARGS = struct type T = C_Position.reports_text * C_Env.error_lines val empty = ([], []) val extend = I fun merge ((l11, l12), (l21, l22)) = (l11 @ l21, l12 @ l22) end structure Data_Tree = Generic_Data (Data_Tree_Args) fun setmp_tree f context = let val x = Data_Tree.get context val context = f (Data_Tree.put Data_Tree_Args.empty context) in (Data_Tree.get context, Data_Tree.put x context) end fun stack_exec0 f {context, reports_text, error_lines} = let val ((reports_text', error_lines'), context) = setmp_tree f context in { context = context , reports_text = append reports_text' reports_text , error_lines = append error_lines' error_lines } end fun stack_exec env_dir data_put = stack_exec0 o Data_Lang.setmp (SOME (apsnd (C_Env.map_env_directives (K env_dir)) data_put)) end \ ML \ \\<^file>\~~/src/Pure/ML/ml_context.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/ML/ml_context.ML Author: Makarius ML context and antiquotations. *) \ structure C_Context0 = struct (* theory data *) type env_direct = bool (* internal result for conditional directives: branch skipping *) * (C_Env.env_directives * C_Env.env_tree) structure Directives = Generic_Data (type T = (Position.T list * serial * ( (* evaluated during lexing phase *) (C_Lex.token_kind_directive -> env_direct -> C_Env.antiq_language list (* nested annotations from the input *) * env_direct (*NOTE: remove the possibility of returning a too modified env?*)) * (* evaluated during parsing phase *) (C_Lex.token_kind_directive -> C_Env.env_propagation_directive))) Symtab.table val empty = Symtab.empty val extend = I val merge = Symtab.join (K #2)); end \ ML \ \\<^theory>\Isabelle_C.C_Lexer_Language\\ \ structure C_Grammar_Lexer : ARG_LEXER1 = struct structure LALR_Lex_Instance = struct type ('a,'b) token = ('a, 'b) C_Grammar.Tokens.token type pos = Position.T type arg = C_Grammar.Tokens.arg type svalue0 = C_Grammar.Tokens.svalue0 type svalue = arg -> svalue0 * arg type state = C_Grammar.ParserData.LALR_Table.state end type stack = (LALR_Lex_Instance.state, LALR_Lex_Instance.svalue0, LALR_Lex_Instance.pos) C_Env.stack' fun advance_hook stack = (fn f => fn (arg, stack_ml) => f (#stream_hook arg) (arg, stack_ml)) (fn [] => I | l :: ls => I #> fold_rev (fn (_, syms, ml_exec) => let val len = length syms in if len = 0 then I #>> (case ml_exec of (_, C_Env.Bottom_up (C_Env.Exec_annotation exec), env_dir, _) => (fn arg => C_Env.map_env_tree (C_Stack.stack_exec env_dir (stack, #env_lang arg) (exec NONE)) arg) | (_, C_Env.Bottom_up (C_Env.Exec_directive exec), env_dir, _) => C_Env.map_env_lang_tree (curry (exec NONE env_dir)) | ((pos, _), _, _, _) => C_Env_Ext.map_context (fn _ => error ( "Style of evaluation not yet implemented" ^ Position.here pos))) else I ##> let val len = len - 1 in fn stack_ml => stack_ml |> (if length stack_ml <= len then tap (fn _ => warning ("Maximum depth reached (" ^ Int.toString (len - length stack_ml + 1) ^ " in excess)" ^ Position.here (Symbol_Pos.range syms |> Position.range_position))) #> tap (fn _ => warning ("Unevaluated code" ^ Position.here (ml_exec |> #1 |> Position.range_position))) #> I else if length stack_ml - len <= 2 then tap (fn _ => warning ("Unevaluated code\ \ as the hook is pointing to an internal initial value" ^ Position.here (ml_exec |> #1 |> Position.range_position))) #> I else nth_map len (cons ml_exec)) end end) l #>> C_Env.map_stream_hook (K ls)) fun add_stream_hook (syms_shift, syms, ml_exec) = C_Env.map_stream_hook (fn stream_hook => case fold (fn _ => fn (eval1, eval2) => (case eval2 of e2 :: eval2 => (e2, eval2) | [] => ([], [])) |>> (fn e1 => e1 :: eval1)) syms_shift ([], stream_hook) of (eval1, eval2) => fold cons eval1 (case eval2 of e :: es => ((syms_shift, syms, ml_exec) :: e) :: es | [] => [[(syms_shift, syms, ml_exec)]])) fun makeLexer ((stack, stack_ml, stack_pos, stack_tree), arg) = let val (token, arg) = C_Env_Ext.map_stream_lang' (fn (st, []) => (NONE, (st, [])) | (st, x :: xs) => (SOME x, (st, xs))) arg fun return0' f = (arg, stack_ml) |> advance_hook stack |> f |> (fn (arg, stack_ml) => rpair ((stack, stack_ml, stack_pos, stack_tree), arg)) fun return0 x = \ \Warning: \advance_hook\ must not be early evaluated here, as it might generate undesirable markup reporting (in annotation commands).\ \ \Todo: Arrange \advance_hook\ as a pure function, so that the overall could be eta-simplified.\ return0' I x val encoding = fn C_Lex.Encoding_L => true | _ => false open C_Ast fun token_err pos1 pos2 src = C_Grammar_Tokens.token_of_string (C_Grammar.Tokens.error (pos1, pos2)) (ClangCVersion0 (From_string src)) (CChar (From_char_hd "0") false) (CFloat (From_string src)) (CInteger 0 DecRepr (Flags 0)) (CString0 (From_string src, false)) (Ident (From_string src, 0, OnlyPos NoPosition (NoPosition, 0))) src pos1 pos2 src open C_Scan in case token of NONE => return0' (tap (fn (arg, _) => fold (uncurry (fn pos => fold_rev (fn (syms, _, _) => fn () => let val () = error ("Maximum depth reached (" ^ Int.toString (pos + 1) ^ " in excess)" ^ Position.here (Symbol_Pos.range syms |> Position.range_position)) in () end))) (map_index I (#stream_hook arg)) ())) (C_Grammar.Tokens.x25_eof (Position.none, Position.none)) | SOME (Left (antiq_raw, l_antiq)) => makeLexer ( (stack, stack_ml, stack_pos, stack_tree) , (arg, false) |> fold (fn C_Env.Antiq_stack (_, C_Env.Parsing ((syms_shift, syms), ml_exec)) => I #>> add_stream_hook (syms_shift, syms, ml_exec) | C_Env.Antiq_stack (_, C_Env.Never) => I ##> K true | _ => I) l_antiq |> (fn (arg, false) => arg | (arg, true) => C_Env_Ext.map_stream_ignored (cons (Left antiq_raw)) arg)) | SOME (Right (tok as C_Lex.Token (_, (C_Lex.Directive dir, _)))) => makeLexer ( (stack, stack_ml, stack_pos, stack_tree) , arg |> let val context = C_Env_Ext.get_context arg in fold (fn dir_tok => add_stream_hook ( [] , [] , ( Position.no_range , C_Env.Bottom_up (C_Env.Exec_directive (dir |> (case Symtab.lookup (C_Context0.Directives.get context) (C_Lex.content_of dir_tok) of NONE => K (K (K I)) | SOME (_, _, (_, exec)) => exec))) , Symtab.empty , true))) (C_Lex.directive_cmds dir) end |> C_Env_Ext.map_stream_ignored (cons (Right tok))) | SOME (Right (C_Lex.Token ((pos1, pos2), (tok, src)))) => case tok of C_Lex.String (C_Lex.Encoding_file (SOME err), _) => return0' (apfst (C_Env.map_env_tree (C_Env.map_error_lines (cons (err ^ Position.here pos1))))) (token_err pos1 pos2 src) | _ => return0 (case tok of C_Lex.Char (b, [c]) => C_Grammar.Tokens.cchar (CChar (From_char_hd (case c of Left c => c | _ => chr 0)) (encoding b), pos1, pos2) | C_Lex.String (b, s) => C_Grammar.Tokens.cstr (CString0 ( From_string ( implode (map (fn Left s => s | Right _ => chr 0) s)) , encoding b) , pos1 , pos2) | C_Lex.Integer (i, repr, flag) => C_Grammar.Tokens.cint ( CInteger i (case repr of C_Lex.Repr_decimal => DecRepr0 | C_Lex.Repr_hexadecimal => HexRepr0 | C_Lex.Repr_octal => OctalRepr0) (C_Lex.read_bin (fold (fn flag => map (fn (bit, flag0) => ( if flag0 = (case flag of C_Lex.Flag_unsigned => FlagUnsigned0 | C_Lex.Flag_long => FlagLong0 | C_Lex.Flag_long_long => FlagLongLong0 | C_Lex.Flag_imag => FlagImag0) then "1" else bit , flag0))) flag ([FlagUnsigned, FlagLong, FlagLongLong, FlagImag] |> rev |> map (pair "0")) |> map #1) |> Flags) , pos1 , pos2) | C_Lex.Float s => C_Grammar.Tokens.cfloat (CFloat (From_string (implode (map #1 s))), pos1, pos2) | C_Lex.Ident => let val (name, arg) = C_Grammar_Rule_Lib.getNewName arg val ident0 = C_Grammar_Rule_Lib.mkIdent (C_Grammar_Rule_Lib.posOf' false (pos1, pos2)) src name in if C_Grammar_Rule_Lib.isTypeIdent src arg then C_Grammar.Tokens.tyident (ident0, pos1, pos2) else C_Grammar.Tokens.ident (ident0, pos1, pos2) end | _ => token_err pos1 pos2 src) end end \ text \ This is where the instancing of the parser functor (from \<^theory>\Isabelle_C.C_Parser_Language\) with the lexer (from \<^theory>\Isabelle_C.C_Lexer_Language\) actually happens ... \ ML \ \\<^theory>\Isabelle_C.C_Parser_Language\\ \ structure C_Grammar_Parser = LALR_Parser_Join (structure LrParser = LALR_Parser_Eval structure ParserData = C_Grammar.ParserData structure Lex = C_Grammar_Lexer) \ ML \ \\<^file>\~~/src/Pure/ML/ml_compiler.ML\\ \ structure C_Language = struct open C_Env fun exec_tree write msg (Tree ({rule_pos, rule_type}, l_tree)) = case rule_type of Void => write msg rule_pos "VOID" NONE | Shift => write msg rule_pos "SHIFT" NONE | Reduce (rule_static, (rule0, vacuous, rule_antiq)) => write msg rule_pos ("REDUCE " ^ Int.toString rule0 ^ " " ^ (if vacuous then "X" else "O")) (SOME (C_Grammar_Rule.string_reduce rule0 ^ " " ^ C_Grammar_Rule.type_reduce rule0)) #> (case rule_static of SOME rule_static => rule_static #>> SOME | NONE => pair NONE) #-> (fn env_lang => fold (fn (stack0, env_lang0, (_, C_Env.Top_down exec, env_dir, _)) => C_Stack.stack_exec env_dir (stack0, Option.getOpt (env_lang, env_lang0)) (exec (SOME rule0)) | _ => I) rule_antiq) #> fold (exec_tree write (msg ^ " ")) l_tree fun exec_tree' l env_tree = env_tree |> fold (exec_tree let val ctxt = Context.proof_of (#context env_tree) val write = if Config.get ctxt C_Options.parser_trace andalso Context_Position.is_visible ctxt then fn f => tap (tracing o f) else K I in fn msg => fn (p1, p2) => fn s1 => fn s2 => write (fn _ => msg ^ s1 ^ " " ^ Position.here p1 ^ " " ^ Position.here p2 ^ (case s2 of SOME s2 => " " ^ s2 | NONE => "")) end "") l fun uncurry_context f pos = uncurry (fn x => fn arg => map_env_tree' (f pos x (#env_lang arg)) arg) fun eval env_lang start err accept stream_lang = make env_lang stream_lang #> C_Grammar_Parser.makeLexer #> C_Grammar_Parser.parse ( 0 , uncurry_context (fn (next_pos1, next_pos2) => fn (stack, _, _, stack_tree) => fn env_lang => C_Env.map_reports_text (cons ( ( Position.range_position (case hd stack of (_, (_, pos1, pos2)) => (pos1, pos2)) , Markup.bad ()) , "") #> (case rev (tl stack) of _ :: _ :: stack => append (map_filter (fn (pos1, pos2) => if Position.offset_of pos1 = Position.offset_of pos2 then NONE else SOME ((Position.range_position (pos1, pos2), Markup.intensify), "")) ((next_pos1, next_pos2) :: map (fn (_, (_, pos1, pos2)) => (pos1, pos2)) stack)) | _ => I)) #> exec_tree' (rev stack_tree) #> err env_lang stack (Position.range_position (case hd stack_tree of Tree ({rule_pos = (rule_pos1, _), ...}, _) => (rule_pos1, next_pos2)))) , Position.none , start , uncurry_context (fn _ => fn (stack, _, _, stack_tree) => fn env_lang => exec_tree' stack_tree #> accept env_lang (stack |> hd |> C_Stack.map_svalue0 C_Grammar_Rule.reduce0)) , fn (stack, arg) => arg |> map_rule_input (K stack) |> map_rule_output (K empty_rule_output) , fn (rule0, stack0, pre_ml) => fn arg => let val rule_output = #rule_output arg val env_lang = #env_lang arg val (delayed, actual) = if #output_vacuous rule_output then let fun f (_, _, _, to_delay) = to_delay in (map (filter f) pre_ml, map (filter_out f) pre_ml) end else ([], pre_ml) val actual = flat (map rev actual) in ( (delayed, map (fn x => (stack0, env_lang, x)) actual, rule_output) , fold (fn (_, C_Env.Bottom_up (C_Env.Exec_annotation exec), env_dir, _) => C_Env.map_env_tree (C_Stack.stack_exec env_dir (stack0, env_lang) (exec (SOME rule0))) | (_, C_Env.Bottom_up (C_Env.Exec_directive exec), env_dir, _) => C_Env.map_env_lang_tree (curry (exec (SOME rule0) env_dir)) | _ => I) actual arg) end) #> snd #> apsnd #env_tree end \ subsection \Full Evaluation Engine (Core Language with Annotations)\ \ \\<^file>\~~/src/Pure/Thy/thy_info.ML\: \<^theory>\Isabelle_C.C_Parser_Language\, \<^theory>\Isabelle_C.C_Parser_Annotation\\ ML \ \\<^file>\~~/src/Pure/ML/ml_context.ML\\ (* Author: Frédéric Tuong, Université Paris-Saclay *) (* Title: Pure/ML/ml_context.ML Author: Makarius ML context and antiquotations. *) \ structure C_Context = struct fun fun_decl a v s ctxt = let val (b, ctxt') = ML_Context.variant a ctxt; val env = "fun " ^ b ^ " " ^ v ^ " = " ^ s ^ " " ^ v ^ ";\n"; val body = ML_Context.struct_name ctxt ^ "." ^ b; fun decl (_: Proof.context) = (env, body); in (decl, ctxt') end; (* parsing and evaluation *) local fun scan_antiq context syms = let val keywords = C_Thy_Header.get_keywords' (Context.proof_of context) in ( C_Token.read_antiq' keywords (C_Parse.!!! (Scan.trace (C_Annotation.parse_command (Context.theory_of context)) >> (I #>> C_Env.Antiq_stack))) syms , C_Token.read_with_commands'0 keywords syms) end fun print0 s = maps (fn C_Lex.Token (_, (t as C_Lex.Directive d, _)) => (s ^ @{make_string} t) :: print0 (s ^ " ") (C_Lex.token_list_of d) | C_Lex.Token (_, t) => [case t of (C_Lex.Char _, _) => "Text Char" | (C_Lex.String _, _) => "Text String" | _ => let val t' = @{make_string} (#2 t) in if String.size t' <= 2 then @{make_string} (#1 t) else s ^ @{make_string} (#1 t) ^ " " ^ (String.substring (t', 1, String.size t' - 2) |> Markup.markup Markup.intensify) end]) val print = tracing o cat_lines o print0 "" open C_Scan fun markup_directive ty = C_Grammar_Rule_Lib.markup_make (K NONE) (K ()) (K ty) in fun markup_directive_command data = markup_directive "directive command" (fn cons' => fn def => fn C_Ast.Left _ => cons' (Markup.keyword_properties (if def then Markup.free else Markup.keyword1)) | C_Ast.Right (_, msg, f) => tap (fn _ => Output.information msg) #> f #> cons' (Markup.keyword_properties Markup.free)) data fun directive_update (name, pos) f tab = let val pos = [pos] val data = (pos, serial (), f) val _ = Position.reports_text (markup_directive_command (C_Ast.Left (data, C_Env_Ext.list_lookup tab name)) pos name []) in Symtab.update (name, data) tab end fun markup_directive_define in_direct = C_Env.map_reports_text ooo markup_directive "directive define" (fn cons' => fn def => fn err => (if def orelse in_direct then I else cons' Markup.language_antiquotation) #> (case err of C_Ast.Left _ => I | C_Ast.Right (_, msg, f) => tap (fn _ => Output.information msg) #> f) #> (if def then cons' Markup.free else if in_direct then I else cons' Markup.antiquote)) fun eval env start err accept (ants, ants_err) {context, reports_text, error_lines} = let val error_lines = ants_err error_lines fun scan_comment tag pos (antiq as {explicit, body, ...}) cts = let val (res, l_comm) = scan_antiq context body in Left ( tag , antiq , l_comm , if forall (fn Right _ => true | _ => false) res then let val (l_msg, res) = split_list (map_filter (fn Right (msg, l_report, l_tok) => SOME (msg, (l_report, l_tok)) | _ => NONE) res) val (l_report, l_tok) = split_list res in [( C_Env.Antiq_none (C_Lex.Token (pos, ( (C_Lex.Comment o C_Lex.Comment_suspicious o SOME) ( explicit , cat_lines l_msg , if explicit then flat l_report else []) , cts))) , l_tok)] end else map (fn Left x => x | Right (msg, l_report, tok) => (C_Env.Antiq_none (C_Lex.Token ( C_Token.range_of [tok] , ( (C_Lex.Comment o C_Lex.Comment_suspicious o SOME) (explicit, msg, l_report) , C_Token.content_of tok))) , [tok])) res) end val ants = map (fn C_Lex.Token (pos, (C_Lex.Comment (C_Lex.Comment_formal antiq), cts)) => scan_comment C_Env.Comment_language pos antiq cts | tok => Right tok) ants fun map_ants f1 f2 = maps (fn Left x => f1 x | Right tok => f2 tok) val ants_none = map_ants (fn (_, _, _, l) => maps (fn (C_Env.Antiq_none x, _) => [x] | _ => []) l) (K []) ants val _ = Position.reports (maps (fn Left (_, _, _, [(C_Env.Antiq_none _, _)]) => [] | Left (_, {start, stop, range = (pos, _), ...}, _, _) => (case stop of SOME stop => cons (stop, Markup.antiquote) | NONE => I) [(start, Markup.antiquote), (pos, Markup.language_antiquotation)] | _ => []) ants); val _ = Position.reports_text (maps C_Lex.token_report ants_none @ maps (fn Left (_, _, _, [(C_Env.Antiq_none _, _)]) => [] | Left (_, _, l, ls) => maps (fn (C_Env.Antiq_stack (pos, _), _) => pos | _ => []) ls @ maps (maps (C_Token.reports (C_Thy_Header.get_keywords (Context.theory_of context)))) (l :: map #2 ls) | _ => []) ants); val error_lines = C_Lex.check ants_none error_lines; val ((ants, {context, reports_text, error_lines}), env) = C_Env_Ext.map_env_directives' (fn env_dir => let val (ants, (env_dir, env_tree)) = fold_map let fun subst_directive tok (range1 as (pos1, _)) name (env_dir, env_tree) = case Symtab.lookup env_dir name of NONE => (Right (Left tok), (env_dir, env_tree)) | SOME (data as (_, _, (exec_toks, exec_antiq))) => env_tree |> markup_directive_define false (C_Ast.Right ([pos1], SOME data)) [pos1] name |> (case exec_toks of Left exec_toks => C_Env.map_context' (exec_toks (name, range1)) #> apfst (fn toks => (toks, Symtab.update (name, ( #1 data , #2 data , (Right toks, exec_antiq))) env_dir)) | Right toks => pair (toks, env_dir)) ||> C_Env.map_context (exec_antiq (name, range1)) |-> (fn (toks, env_dir) => pair (Right (Right (pos1, map (C_Lex.set_range range1) toks))) o pair env_dir) in fn Left (tag, antiq, toks, l_antiq) => fold_map (fn antiq as (C_Env.Antiq_stack (_, C_Env.Lexing (_, exec)), _) => apsnd (C_Stack.stack_exec0 (exec C_Env.Comment_language)) #> pair antiq | (C_Env.Antiq_stack (rep, C_Env.Parsing (syms, (range, exec, _, skip))), toks) => (fn env as (env_dir, _) => ( ( C_Env.Antiq_stack (rep, C_Env.Parsing (syms, (range, exec, env_dir, skip))) , toks) , env)) | antiq => pair antiq) l_antiq #> apfst (fn l_antiq => Left (tag, antiq, toks, l_antiq)) | Right tok => case tok of C_Lex.Token (_, (C_Lex.Directive dir, _)) => pair false #> fold (fn dir_tok => let val name = C_Lex.content_of dir_tok val pos1 = [C_Lex.pos_of dir_tok] in fn env_tree as (_, (_, {context = context, ...})) => let val data = Symtab.lookup (C_Context0.Directives.get context) name in env_tree |> apsnd (apsnd (C_Env.map_reports_text (markup_directive_command (C_Ast.Right (pos1, data)) pos1 name))) |> (case data of NONE => I | SOME (_, _, (exec, _)) => exec dir #> #2) end end) (C_Lex.directive_cmds dir) #> snd #> tap (fn _ => app (fn C_Lex.Token ( (pos, _) , (C_Lex.Comment (C_Lex.Comment_formal _), _)) => (Position.reports_text [((pos, Markup.ML_comment), "")]; (* not yet implemented *) warning ("Ignored annotation in directive" ^ Position.here pos)) | _ => ()) (C_Lex.token_list_of dir)) #> pair (Right (Left tok)) | C_Lex.Token (pos, (C_Lex.Keyword, cts)) => subst_directive tok pos cts | C_Lex.Token (pos, (C_Lex.Ident, cts)) => subst_directive tok pos cts | _ => pair (Right (Left tok)) end ants ( env_dir , {context = context, reports_text = reports_text, error_lines = error_lines}) in ((ants, env_tree), env_dir) end) env val ants_stack = map_ants (single o Left o (fn (_, a, _, l) => (a, maps (single o #1) l))) (map Right o (fn Left tok => [tok] | Right (_, toks) => toks)) ants val _ = Position.reports_text (maps (fn Right (Left tok) => C_Lex.token_report tok | Right (Right (pos, [])) => [((pos, Markup.intensify), "")] | _ => []) ants); val ctxt = Context.proof_of context val () = if Config.get ctxt C_Options.lexer_trace andalso Context_Position.is_visible ctxt then print (map_filter (fn Right x => SOME x | _ => NONE) ants_stack) else () in C_Language.eval env start err accept ants_stack {context = context, reports_text = reports_text, error_lines = error_lines} end (* derived versions *) fun eval' env start err accept ants = Context.>>> (fn context => C_Env_Ext.context_map' (eval (env context) (start context) err accept ants #> apsnd (tap (Position.reports_text o #reports_text) #> tap (#error_lines #> (fn [] => () | l => error (cat_lines (rev l)))) #> (C_Env.empty_env_tree o #context))) context) end; fun eval_source env start err accept source = eval' env (start source) err accept (C_Lex.read_source source); fun eval_source' env start err accept source = eval env (start source) err accept (C_Lex.read_source source); fun eval_in o_context env start err accept toks = Context.setmp_generic_context o_context (fn () => eval' env start err accept toks) (); fun expression struct_open range name constraint body ants context = context |> ML_Context.exec let val verbose = Config.get (Context.proof_of context) C_Options.ML_verbose in fn () => ML_Context.eval (ML_Compiler.verbose verbose ML_Compiler.flags) (#1 range) (ML_Lex.read ("Context.put_generic_context (SOME (let open " ^ struct_open ^ " val ") @ ML_Lex.read_set_range range name @ ML_Lex.read (": " ^ constraint ^ " =") @ ants @ ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")) end; end \ end