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,1203 +1,1203 @@ (****************************************************************************** * 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 Analogous to: (* 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 Analogous to: (* 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, Bytes.string 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\\ \ signature C_MODULE = sig structure Data_Accept : GENERIC_DATA structure Data_In_Env : GENERIC_DATA structure Data_In_Source : GENERIC_DATA structure Data_Term : GENERIC_DATA structure C_Term: sig val key0_default: string val key0_expression: string val key0_external_declaration: string val key0_statement: string val key0_translation_unit: string val key_default: Input.source val key_expression: Input.source val key_external_declaration: Input.source val key_statement: Input.source val key_translation_unit: Input.source val map_default: (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_expression: (C_Grammar_Rule_Lib.CExpr -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_external_declaration: (C_Grammar_Rule_Lib.CExtDecl -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_statement: (C_Grammar_Rule_Lib.CStat -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val map_translation_unit: (C_Grammar_Rule_Lib.CTranslUnit -> C_Env.env_lang -> local_theory -> term) -> theory -> theory val tok0_expression: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok0_external_declaration: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok0_statement: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok0_translation_unit: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_expression: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_external_declaration: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_statement: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tok_translation_unit: Input.source * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token) val tokens: (string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)) list end structure C_Term': sig val accept: local_theory -> (Input.source * (Position.range -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token)) option -> (Input.source -> Context.generic -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token) * (Data_In_Env.T -> 'a * (C_Grammar_Rule.ast_generic * 'b * 'c) -> {context: Context.generic, error_lines: 'd, reports_text: 'e} -> term * {context: Context.generic, error_lines: 'd, reports_text: 'e}) val err: C_Env.env_lang -> (LALR_Table.state * (C_Grammar_Parser.svalue0 * Position.T * Position.T)) list -> Position.T -> {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} -> term * {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} val eval_in: Input.source -> Context.generic -> (Context.generic -> C_Env.env_lang) -> (Input.source * (Position.range -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token)) option -> C_Lex.token list * (C_Env.error_lines -> string list) -> term val parse_translation: ('a * (Input.source * (Position.range -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token)) option) list -> ('a * (Proof.context -> term list -> term)) list end val accept: Data_In_Env.T -> 'a * (C_Grammar_Rule.ast_generic * 'b * 'c) -> {context: Context.generic, error_lines: 'd, reports_text: 'e} -> unit * {context: Context.generic, error_lines: 'd, reports_text: 'e} val accept0: (Context.generic -> C_Grammar_Rule.ast_generic -> Data_In_Env.T -> Context.generic -> 'a) -> Data_In_Env.T -> C_Grammar_Rule.ast_generic -> Context.generic -> 'a val c_enclose: string -> string -> Input.source -> C_Lex.token list * (string list -> string list) val env: Context.generic -> Data_In_Env.T val env0: Proof.context -> Data_In_Env.T val err: C_Env.env_lang -> (LALR_Table.state * (C_Grammar_Parser.svalue0 * Position.T * Position.T)) list -> Position.T -> {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} -> unit * {context: Context.generic, error_lines: string list, reports_text: Position.report_text list} val err0: 'a -> 'b -> Position.T -> {context: 'c, error_lines: string list, reports_text: 'd} -> {context: 'c, error_lines: string list, reports_text: 'd} val eval_in: Input.source -> Context.generic option -> C_Lex.token list * (C_Env.error_lines -> string list) -> unit val eval_source: Input.source -> unit val exec_eval: Input.source -> Context.generic -> Context.generic val start: Input.source -> Context.generic -> (C_Grammar.Tokens.svalue, Position.T) LALR_Parser_Eval.Token.token (* toplevel command semantics of Isabelle_C *) val C: Input.source -> Context.generic -> Context.generic val C': C_Env.env_lang option -> Input.source -> Context.generic -> Context.generic val C_export_boot: Input.source -> Context.generic -> generic_theory val C_export_file: Position.T * 'a -> Proof.context -> Proof.context val C_prf: Input.source -> Proof.state -> Proof.state end structure C_Module : C_MODULE = struct structure Data_In_Source = Generic_Data ( type T = Input.source list val empty = [] val merge = K empty ) structure Data_In_Env = Generic_Data ( type T = C_Env.env_lang val empty = C_Env.empty_env_lang val merge = K empty ) structure Data_Accept = Generic_Data ( type T = C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> Context.generic fun empty _ _ = I val merge = #2 ) structure Data_Term = Generic_Data ( type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) Symtab.table val empty = Symtab.empty val merge = #2 ) (* keys for major syntactic categories *) 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.get_CTranslUnit val map_external_declaration = map_upd key0_external_declaration C_Grammar_Rule.get_CExtDecl val map_statement = map_upd key0_statement C_Grammar_Rule.get_CStat val map_expression = map_upd key0_expression C_Grammar_Rule.get_CExpr 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 val C' = let 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)) in fn NONE => (fn src => C (env (Context.the_generic_context ())) src) | SOME env_lang => C env_lang end 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 C11 Directives as C-commands\ subsubsection \Initialization\ ML \ \\<^theory>\Pure\\ \ structure C_Directive : sig val setup_define: Position.T -> (C_Lex.token list -> string * Position.range -> Context.generic -> C_Lex.token list * Context.generic) -> (string * Position.range -> Context.generic -> Context.generic) -> theory -> theory end = 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 C 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 => command00 (drop2 f) kind scan) 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 get_file gthy = command_c (get_file (Context.theory_of gthy)) gthy; fun command_ml environment debug get_file gthy = let val file = get_file (Context.theory_of gthy); val source = Token.file_source file; 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.command_spec (Keyword.prf_script, ["proof"])) , (("by", \<^here>, \<^here>, \<^here>), Keyword.command_spec (Keyword.qed, ["proof"])) , (("done", \<^here>, \<^here>, \<^here>), Keyword.command_spec (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 (C_Resources.parse_file --| semi) ("ML_file", \<^here>, \<^here>, \<^here>) #> C_Inner_Syntax.command0' (C_Inner_Toplevel.generic_theory o C_Inner_File.C) Keyword.thy_load (C_Resources.parse_file --| 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 Analogous to: (* 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.embedded) 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 ()); + | NONE => Toplevel.make_state NONE); 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 get_file gthy = command_c (get_file (Context.theory_of gthy)) gthy; end; \ subsubsection \Setup for \<^verbatim>\C\ and \<^verbatim>\C_file\ Command Syntax\ 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_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 \Term-Cartouches for C Syntax\ 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) ] \ (*test*) ML\C_Module.env (Context.the_generic_context())\ ML\open Args\ subsection\C-env related ML-Antiquotations as Programming Support\ ML\ (* was in Isabelle2020: (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => with: val embedded_token = ident || string || cartouche; val embedded_inner_syntax = embedded_token >> Token.inner_syntax_of; val embedded_input = embedded_token >> Token.input_of; val embedded = embedded_token >> Token.content_of; val embedded_position = embedded_input >> Input.source_content; defined in args. Setting it to : (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => makes this syntactically more restrictive. *) val _ = Theory.setup( ML_Antiquotation.value_embedded \<^binding>\C\<^sub>e\<^sub>n\<^sub>v\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"C_Module.env (Context.the_generic_context())")) || Scan.succeed "C_Module.env (Context.the_generic_context())")) \ text\Note that this anti-quotation is controlled by the \<^verbatim>\C_starting_env\ - flag. \ declare[[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]] ML\@{C\<^sub>e\<^sub>n\<^sub>v}\ declare[[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = empty]] ML\@{C\<^sub>e\<^sub>n\<^sub>v}\ subsection\The Standard Store C11-AST's generated from C-commands\ text\Each call of the C command will register the parsed root AST in this theory-name indexed table.\ ML\ structure Root_Ast_Store = Generic_Data (type T = C_Grammar_Rule.ast_generic list Symtab.table val empty = Symtab.empty val merge = K empty); Root_Ast_Store.map: ( C_Grammar_Rule.ast_generic list Symtab.table -> C_Grammar_Rule.ast_generic list Symtab.table) -> Context.generic -> Context.generic; fun update_Root_Ast filter ast _ ctxt = let val theory_id = Context.theory_long_name(Context.theory_of ctxt) val insert_K_ast = Symtab.map_default (theory_id,[]) (cons ast) in case filter ast of NONE => (warning "No appropriate c11 ast found - store unchanged."; ctxt) |SOME _ => (Root_Ast_Store.map insert_K_ast) ctxt end; fun get_Root_Ast filter thy = let val ctxt = Context.Theory thy val thid = Context.theory_long_name(Context.theory_of ctxt) val ast = case Symtab.lookup (Root_Ast_Store.get ctxt) (thid) of SOME (a::_) => (case filter a of NONE => error "Last C command is not of appropriate AST-class." | SOME x => x) | _ => error"No C command in the current theory." in ast end val get_CExpr = get_Root_Ast C_Grammar_Rule.get_CExpr; val get_CStat = get_Root_Ast C_Grammar_Rule.get_CStat; val get_CExtDecl = get_Root_Ast C_Grammar_Rule.get_CExtDecl; val get_CTranslUnit = get_Root_Ast C_Grammar_Rule.get_CTranslUnit; \ setup \Context.theory_map (C_Module.Data_Accept.put (update_Root_Ast SOME))\ ML\ (* Was : Args.embedded_position changed to : Args.name_position. See comment above. *) val _ = Theory.setup( ML_Antiquotation.value_embedded \<^binding>\C11_CTranslUnit\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CTranslUnit (Context.the_global_context())")) || Scan.succeed "get_CTranslUnit (Context.the_global_context())") #> ML_Antiquotation.value_embedded \<^binding>\C11_CExtDecl\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CExtDecl (Context.the_global_context())")) || Scan.succeed "get_CExtDecl (Context.the_global_context())") #> ML_Antiquotation.value_embedded \<^binding>\C11_CStat\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CStat (Context.the_global_context())")) || Scan.succeed "get_CStat (Context.the_global_context())") #> ML_Antiquotation.value_embedded \<^binding>\C11_CExpr\ (Args.context -- Scan.lift Args.name_position >> (fn (ctxt, (name, pos)) => (warning"arg variant not implemented";"get_CExpr (Context.the_global_context())")) || Scan.succeed "get_CExpr (Context.the_global_context())") ) \ end