From cd311d8a3ae258f9682332518e72cd19cc8d2b18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Mon, 15 May 2023 09:34:35 +0200 Subject: [PATCH] Update firgure* implementation --- Isabelle_DOF-Unit-Tests/Attributes.thy | 47 ++-------------- .../figures/isabelle-architecture.pdf | Bin 36026 -> 35434 bytes Isabelle_DOF/thys/Isa_COL.thy | 51 ++++++++---------- Isabelle_DOF/thys/Isa_DOF.thy | 10 ++-- Isabelle_DOF/thys/RegExpInterface.thy | 24 ++++----- 5 files changed, 43 insertions(+), 89 deletions(-) diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index 5bada7e..cac9eb5 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -178,69 +178,30 @@ section\Simulation of a Monitor\ declare[[free_class_in_monitor_checking]] -open_monitor*[figs1::figure_group, - caption="''Sample ''"] -ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ -text*[testFreeA::A]\\ -figure*[fig_A::figure, - relative_width="90", - file_src="''figures/A.png''"] - \ The A train \ldots \ -figure*[fig_B::figure, - relative_width="90", - file_src="''figures/B.png''"] - \ The B train \ldots \ -open_monitor*[figs2::figure_group, - caption="''Sample ''"] ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ figure*[fig_C::figure, relative_width="90", file_src="''figures/A.png''"] \ The C train \ldots \ -open_monitor*[figs3::figure_group, - caption="''Sample ''"] + + ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ -figure*[fig_D::figure, - relative_width="90", - file_src="''figures/B.png''"] - \ The D train \ldots \ -close_monitor*[figs3] -open_monitor*[figs4::figure_group, - caption="''Sample ''"] -ML\val monitor_infos = DOF_core.get_monitor_infos \<^context>\ - -text*[testRejected1::figure_group, caption="''document/figures/A.png''"] - \ The A train \ldots \ - -figure*[fig_E::figure, - relative_width="90", - file_src="''figures/B.png''"] - \ The E train \ldots \ -close_monitor*[figs4] -close_monitor*[figs2] -text*[testRejected2::figure_group, caption="''document/figures/A.png''"] - \ The A train \ldots \ - -close_monitor*[figs1] declare[[free_class_in_monitor_checking = false]] text\Resulting trace of figs1 as ML antiquotation: \ -ML \@{trace_attribute figs1}\ + text\Resulting trace of figs as text antiquotation:\ -text\@{trace_attribute figs1}\ + section\A Complex Evaluation involving Automatas\ text\Test trace\_attribute term antiquotation:\ -term*\map snd @{trace-attribute \figs1\}\ -value*\map snd @{trace-attribute \figs1\}\ - definition example_expression where "example_expression \ \\''Conceptual.A''\ || \''Conceptual.F''\\\<^sup>*" value* \ DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \aaa\}) \ diff --git a/Isabelle_DOF/document/figures/isabelle-architecture.pdf b/Isabelle_DOF/document/figures/isabelle-architecture.pdf index 826297f002c5911f196fd24c02c798156c54a24e..6082333781c05595fa0bfb847291a6a27950194f 100644 GIT binary patch delta 9 Qcmdlrlj+qIrVUwL02e<5dH?_b delta 480 zcmYL`&1%~~6onzHGP`WrEKe7qHU!U~MwWsw*pVH)C`s**MUoPPJqDLXBSs_VXA|6I zw(6#D(RCgo50a1(lRJ+}1T8zZrYevmp3Fg0y;(2x?05uvc3)`F z7SlPQXEw{rqN%&M2PIQDTWJgisBgEQA8)e7$sFg}mTQxP%bx6UTy?UmuD?gs`sWft zjQf2Na@HijRhe}UI87&Sg6`Y_hDD+Cz8e(KKS(^A?$x3R7xtWKm>T3mnx8c?k13f#PK@_MO5!TecVh_Tqc7g z9LF(Fr5X-nF&YJGJPhJgh=`^AqcC7{@MgO)&hLS>PR`d4UOD65eXBQ+Qi=d{ny(Ce aqh>AMEK)i@_?^`&B2~mAvcEq*nUH^Dr-Bmz diff --git a/Isabelle_DOF/thys/Isa_COL.thy b/Isabelle_DOF/thys/Isa_COL.thy index 981f779..573081f 100644 --- a/Isabelle_DOF/thys/Isa_COL.thy +++ b/Isabelle_DOF/thys/Isa_COL.thy @@ -300,12 +300,6 @@ fun fig_content_modes (ctxt, toks) = (toks) in (y, (ctxt, toks')) end -fun document_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = - Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => - (check ctxt NONE source; - Latex.string (Latex.output_ascii_breakable "/" (Input.string_of source)) - |> Latex.macro "isatt")); - fun get_session_dir ctxt path = Resources.check_session_dir ctxt (SOME (path)) @@ -345,13 +339,13 @@ fun fig_content ctxt (cfg_trans,file:Input.source) = in if Input.string_of(caption) = "" then file |> (Latex.string o Input.string_of) - |> (XML.enclose ("\\includegraphics"^arg_single^"{") "}") + |> Latex.macro ("includegraphics"^arg_single) else file |> (Latex.string o Input.string_of) |> (fn X => (Latex.string ("{"^wdth_val_s^"}")) - @ (Latex.string "\\centering") - @ (XML.enclose ("\\includegraphics"^arg^"{") "}" X) + @ (Latex.macro0 "centering") + @ (Latex.macro ("includegraphics"^arg) X) @ (Latex.macro "caption" (generate_caption ctxt caption))) |> (Latex.environment ("subcaptionblock") ) (* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *) @@ -373,25 +367,25 @@ val _ = Theory.setup ML\ -fun convert_meta_args (X, (((str,_),value) :: R)) = - let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term @{context} x)) - handle TERM x => error "Illegal int format." +fun convert_meta_args ctxt (X, (((str,_),value) :: R)) = + let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term ctxt x)) + handle TERM _ => error "Illegal int format." in (case YXML.content_of str of "relative_width" => upd_relative_width (conv_int value) - o convert_meta_args (X, R) + o convert_meta_args ctxt (X, R) | "relative_height" => upd_relative_height (conv_int value) - o convert_meta_args (X, R ) - | "file_src" => convert_meta_args (X, R) + o convert_meta_args ctxt (X, R ) + | "file_src" => convert_meta_args ctxt (X, R) | s => error("!undefined attribute:"^s)) end - |convert_meta_args (X,[]) = I + |convert_meta_args _ (_,[]) = I -fun convert_src_from_margs (X, (((str,_),value)::R)) = +fun convert_src_from_margs ctxt (X, (((str,_),value)::R)) = (case YXML.content_of str of - "file_src" => Input.string (HOLogic.dest_string (Syntax.read_term @{context} value)) - | _ => convert_src_from_margs(X,R)) - |convert_src_from_margs (X, []) = error("No file_src provided.") + "file_src" => Input.string (HOLogic.dest_string (Syntax.read_term ctxt value)) + | _ => convert_src_from_margs ctxt (X,R)) + |convert_src_from_margs _ (_, []) = error("No file_src provided.") fun float_command (name, pos) descr cid = let fun set_default_class NONE = SOME(cid,pos) @@ -401,16 +395,15 @@ fun float_command (name, pos) descr cid = {is_monitor = false} {is_inline = true} {define = true} oid pos (set_default_class cid_pos) doc_attrs - val opts = {markdown = false, body = true} - fun parse_and_tex _ (margs, text) ctxt = (fig_content ctxt - (convert_meta_args margs o upd_caption Input.empty, - convert_src_from_margs margs)) - |> (fn X => (Latex.macro0 "centering" - @ X - @ Latex.macro "caption" (generate_caption ctxt text))) + fun parse_and_tex (margs, text) ctxt = (convert_src_from_margs ctxt margs) + |> pair (upd_caption Input.empty #> convert_meta_args ctxt margs) + |> fig_content ctxt + |> (fn X => (Latex.macro0 "centering" + @ X + @ Latex.macro "caption" (generate_caption ctxt text))) (* TODO: add label *) - |> (Latex.environment ("figure") ) - in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex + |> (Latex.environment ("figure") ) + in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex end diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index ccb4774..df19e11 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -2007,7 +2007,7 @@ fun update_instance_command (((oid, pos), cid_pos), (* General criticism : attributes like "level" were treated here in the kernel instead of dragging them out into the COL -- bu *) -fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) = +fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t) thy = let fun o_m_c oid pos cid_pos doc_attrs thy = Value_Command.Docitem_Parser.create_and_check_docitem {is_monitor=true} (* this is a monitor *) @@ -2019,7 +2019,7 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par val DOF_core.Onto_Class X = DOF_core.get_onto_class_global' cid thy val ralph = RegExpInterface.alphabet (#rejectS X) val aalph = RegExpInterface.alphabet (#rex X) - in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end + in (aalph, ralph, map (RegExpInterface.rexp_term2da thy aalph)(#rex X)) end fun create_monitor_entry oid thy = let val cid = case cid_pos of NONE => ISA_core.err ("You must specified a monitor class.") pos @@ -2029,7 +2029,7 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par (DOF_core.make_monitor_info (accS, rejectS, aS)) thy end in - o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry oid + thy |> o_m_c oid pos cid_pos doc_attrs |> create_monitor_entry oid end; @@ -2194,14 +2194,14 @@ fun document_command (name, pos) descr mark cmd sem_attrs transform_attr = #> SOME): Toplevel.state -> Latex.text option)) ); -fun float_command (name, pos) descr (mark: {body: bool, markdown: bool}) +fun float_command (name, pos) descr cmd output_figure = Outer_Syntax.command (name, pos) descr (ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (fn (meta_args, text) => Toplevel.theory' (fn _ => cmd meta_args) (Toplevel.presentation_context - #> (fn ctxt => (output_figure mark (meta_args, text)) ctxt) + #> output_figure (meta_args, text) #> SOME))) diff --git a/Isabelle_DOF/thys/RegExpInterface.thy b/Isabelle_DOF/thys/RegExpInterface.thy index 797884f..c28e96b 100644 --- a/Isabelle_DOF/thys/RegExpInterface.thy +++ b/Isabelle_DOF/thys/RegExpInterface.thy @@ -161,8 +161,8 @@ structure RegExpInterface : sig type cid val alphabet : term list -> env val ext_alphabet: env -> term list -> env - val conv : term -> env -> int RegExpChecker.rexp (* for debugging *) - val rexp_term2da: env -> term -> automaton + val conv : theory -> term -> env -> int RegExpChecker.rexp (* for debugging *) + val rexp_term2da: theory -> env -> term -> automaton val enabled : automaton -> env -> cid list val next : automaton -> env -> cid -> automaton val final : automaton -> bool @@ -187,23 +187,23 @@ local open RegExpChecker in else () in res end; - fun conv \<^Const_>\Regular_Exp.rexp.Zero _\ _ = Zero - |conv \<^Const_>\Regular_Exp.rexp.One _\ _ = Onea - |conv \<^Const_>\Regular_Exp.rexp.Times _ for X Y\ env = Times(conv X env, conv Y env) - |conv \<^Const_>\Regular_Exp.rexp.Plus _ for X Y\ env = Plus(conv X env, conv Y env) - |conv \<^Const_>\Regular_Exp.rexp.Star _ for X\ env = Star(conv X env) - |conv \<^Const_>\RegExpInterface.opt _ for X\ env = Plus(conv X env, Onea) - |conv \<^Const_>\RegExpInterface.rep1 _ for X\ env = Times(conv X env, Star(conv X env)) - |conv (Const (s, \<^Type>\rexp _\)) env = + fun conv _ \<^Const_>\Regular_Exp.rexp.Zero _\ _ = Zero + |conv _ \<^Const_>\Regular_Exp.rexp.One _\ _ = Onea + |conv thy \<^Const_>\Regular_Exp.rexp.Times _ for X Y\ env = Times(conv thy X env, conv thy Y env) + |conv thy \<^Const_>\Regular_Exp.rexp.Plus _ for X Y\ env = Plus(conv thy X env, conv thy Y env) + |conv thy \<^Const_>\Regular_Exp.rexp.Star _ for X\ env = Star(conv thy X env) + |conv thy \<^Const_>\RegExpInterface.opt _ for X\ env = Plus(conv thy X env, Onea) + |conv thy \<^Const_>\RegExpInterface.rep1 _ for X\ env = Times(conv thy X env, Star(conv thy X env)) + |conv _ (Const (s, \<^Type>\rexp _\)) env = let val n = find_index (fn x => x = s) env val _ = if n<0 then error"conversion error of regexp." else () in Atom(n) end - |conv S _ = error("conversion error of regexp:" ^ (Syntax.string_of_term (@{context})S)) + |conv thy S _ = error("conversion error of regexp:" ^ (Syntax.string_of_term_global thy S)) val eq_int = {equal = curry(op =) : Int.int -> Int.int -> bool}; val eq_bool_list = {equal = curry(op =) : bool list -> bool list -> bool}; - fun rexp_term2da env term = let val rexp = conv term env; + fun rexp_term2da thy env term = let val rexp = conv thy term env; val nda = RegExpChecker.rexp2na eq_int rexp; val da = RegExpChecker.na2da eq_bool_list nda; in da end;