Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update firgure* implementation
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Nicolas Méric 2023-05-15 09:34:35 +02:00
parent fb69f05ac0
commit cd311d8a3a
5 changed files with 43 additions and 89 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
Isabelle_DOF-Unit-Tests/Attributes.thy
View File

@ -178,69 +178,30 @@ section\<open>Simulation of a Monitor\<close>
declare[[free_class_in_monitor_checking]] declare[[free_class_in_monitor_checking]]
open_monitor*[figs1::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
text*[testFreeA::A]\<open>\<close>
figure*[fig_A::figure,
relative_width="90",
file_src="''figures/A.png''"]
\<open> The A train \ldots \<close>
figure*[fig_B::figure,
relative_width="90",
file_src="''figures/B.png''"]
\<open> The B train \ldots \<close>
open_monitor*[figs2::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close> ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
figure*[fig_C::figure, figure*[fig_C::figure,
relative_width="90", relative_width="90",
file_src="''figures/A.png''"] file_src="''figures/A.png''"]
\<open> The C train \ldots \<close> \<open> The C train \ldots \<close>
open_monitor*[figs3::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close> ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
figure*[fig_D::figure,
relative_width="90",
file_src="''figures/B.png''"]
\<open> The D train \ldots \<close>
close_monitor*[figs3]
open_monitor*[figs4::figure_group,
caption="''Sample ''"]
ML\<open>val monitor_infos = DOF_core.get_monitor_infos \<^context>\<close>
text*[testRejected1::figure_group, caption="''document/figures/A.png''"]
\<open> The A train \ldots \<close>
figure*[fig_E::figure,
relative_width="90",
file_src="''figures/B.png''"]
\<open> The E train \ldots \<close>
close_monitor*[figs4]
close_monitor*[figs2]
text*[testRejected2::figure_group, caption="''document/figures/A.png''"]
\<open> The A train \ldots \<close>
close_monitor*[figs1]
declare[[free_class_in_monitor_checking = false]] declare[[free_class_in_monitor_checking = false]]
text\<open>Resulting trace of figs1 as ML antiquotation: \<close> text\<open>Resulting trace of figs1 as ML antiquotation: \<close>
ML \<open>@{trace_attribute figs1}\<close>
text\<open>Resulting trace of figs as text antiquotation:\<close> text\<open>Resulting trace of figs as text antiquotation:\<close>
text\<open>@{trace_attribute figs1}\<close>
section\<open>A Complex Evaluation involving Automatas\<close> section\<open>A Complex Evaluation involving Automatas\<close>
text\<open>Test trace\_attribute term antiquotation:\<close> text\<open>Test trace\_attribute term antiquotation:\<close>
term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*" definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close> value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>

BIN
Isabelle_DOF/document/figures/isabelle-architecture.pdf
View File

Binary file not shown.

51
Isabelle_DOF/thys/Isa_COL.thy
View File

@ -300,12 +300,6 @@ fun fig_content_modes (ctxt, toks) =
(toks) (toks)
in (y, (ctxt, toks')) end 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 = fun get_session_dir ctxt path =
Resources.check_session_dir ctxt Resources.check_session_dir ctxt
(SOME (path)) (SOME (path))
@ -345,13 +339,13 @@ fun fig_content ctxt (cfg_trans,file:Input.source) =
in if Input.string_of(caption) = "" then in if Input.string_of(caption) = "" then
file file
|> (Latex.string o Input.string_of) |> (Latex.string o Input.string_of)
|> (XML.enclose ("\\includegraphics"^arg_single^"{") "}") |> Latex.macro ("includegraphics"^arg_single)
else else
file file
|> (Latex.string o Input.string_of) |> (Latex.string o Input.string_of)
|> (fn X => (Latex.string ("{"^wdth_val_s^"}")) |> (fn X => (Latex.string ("{"^wdth_val_s^"}"))
@ (Latex.string "\\centering") @ (Latex.macro0 "centering")
@ (XML.enclose ("\\includegraphics"^arg^"{") "}" X) @ (Latex.macro ("includegraphics"^arg) X)
@ (Latex.macro "caption" (generate_caption ctxt caption))) @ (Latex.macro "caption" (generate_caption ctxt caption)))
|> (Latex.environment ("subcaptionblock") ) |> (Latex.environment ("subcaptionblock") )
(* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *) (* BUG: newline at the end of subcaptionlbock, making side-by-side a figure-below-figure setup *)
@ -373,25 +367,25 @@ val _ = Theory.setup
ML\<open> ML\<open>
fun convert_meta_args (X, (((str,_),value) :: R)) = fun convert_meta_args ctxt (X, (((str,_),value) :: R)) =
let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term @{context} x)) let fun conv_int x = snd(HOLogic.dest_number(Syntax.read_term ctxt x))
handle TERM x => error "Illegal int format." handle TERM _ => error "Illegal int format."
in in
(case YXML.content_of str of (case YXML.content_of str of
"relative_width" => upd_relative_width (conv_int value) "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) | "relative_height" => upd_relative_height (conv_int value)
o convert_meta_args (X, R ) o convert_meta_args ctxt (X, R )
| "file_src" => convert_meta_args (X, R) | "file_src" => convert_meta_args ctxt (X, R)
| s => error("!undefined attribute:"^s)) | s => error("!undefined attribute:"^s))
end 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 (case YXML.content_of str of
"file_src" => Input.string (HOLogic.dest_string (Syntax.read_term @{context} value)) "file_src" => Input.string (HOLogic.dest_string (Syntax.read_term ctxt value))
| _ => convert_src_from_margs(X,R)) | _ => convert_src_from_margs ctxt (X,R))
|convert_src_from_margs (X, []) = error("No file_src provided.") |convert_src_from_margs _ (_, []) = error("No file_src provided.")
fun float_command (name, pos) descr cid = fun float_command (name, pos) descr cid =
let fun set_default_class NONE = SOME(cid,pos) let fun set_default_class NONE = SOME(cid,pos)
@ -401,16 +395,15 @@ fun float_command (name, pos) descr cid =
{is_monitor = false} {is_monitor = false}
{is_inline = true} {is_inline = true}
{define = true} oid pos (set_default_class cid_pos) doc_attrs {define = true} oid pos (set_default_class cid_pos) doc_attrs
val opts = {markdown = false, body = true} fun parse_and_tex (margs, text) ctxt = (convert_src_from_margs ctxt margs)
fun parse_and_tex _ (margs, text) ctxt = (fig_content ctxt |> pair (upd_caption Input.empty #> convert_meta_args ctxt margs)
(convert_meta_args margs o upd_caption Input.empty, |> fig_content ctxt
convert_src_from_margs margs)) |> (fn X => (Latex.macro0 "centering"
|> (fn X => (Latex.macro0 "centering" @ X
@ X @ Latex.macro "caption" (generate_caption ctxt text)))
@ Latex.macro "caption" (generate_caption ctxt text)))
(* TODO: add label *) (* TODO: add label *)
|> (Latex.environment ("figure") ) |> (Latex.environment ("figure") )
in Monitor_Command_Parser.float_command (name, pos) descr opts create_instance parse_and_tex in Monitor_Command_Parser.float_command (name, pos) descr create_instance parse_and_tex
end end

10
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -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 (* General criticism : attributes like "level" were treated here in the kernel instead of dragging
them out into the COL -- bu *) 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 = let fun o_m_c oid pos cid_pos doc_attrs thy =
Value_Command.Docitem_Parser.create_and_check_docitem Value_Command.Docitem_Parser.create_and_check_docitem
{is_monitor=true} (* this is a monitor *) {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 DOF_core.Onto_Class X = DOF_core.get_onto_class_global' cid thy
val ralph = RegExpInterface.alphabet (#rejectS X) val ralph = RegExpInterface.alphabet (#rejectS X)
val aalph = RegExpInterface.alphabet (#rex 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 = fun create_monitor_entry oid thy =
let val cid = case cid_pos of let val cid = case cid_pos of
NONE => ISA_core.err ("You must specified a monitor class.") pos 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 (DOF_core.make_monitor_info (accS, rejectS, aS)) thy
end end
in 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; end;
@ -2194,14 +2194,14 @@ fun document_command (name, pos) descr mark cmd sem_attrs transform_attr =
#> SOME): Toplevel.state -> Latex.text option)) ); #> 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 = cmd output_figure =
Outer_Syntax.command (name, pos) descr Outer_Syntax.command (name, pos) descr
(ODL_Meta_Args_Parser.attributes -- Parse.document_source >> (ODL_Meta_Args_Parser.attributes -- Parse.document_source >>
(fn (meta_args, text) => (fn (meta_args, text) =>
Toplevel.theory' (fn _ => cmd meta_args) Toplevel.theory' (fn _ => cmd meta_args)
(Toplevel.presentation_context (Toplevel.presentation_context
#> (fn ctxt => (output_figure mark (meta_args, text)) ctxt) #> output_figure (meta_args, text)
#> SOME))) #> SOME)))

24
Isabelle_DOF/thys/RegExpInterface.thy
View File

@ -161,8 +161,8 @@ structure RegExpInterface : sig
type cid type cid
val alphabet : term list -> env val alphabet : term list -> env
val ext_alphabet: env -> term list -> env val ext_alphabet: env -> term list -> env
val conv : term -> env -> int RegExpChecker.rexp (* for debugging *) val conv : theory -> term -> env -> int RegExpChecker.rexp (* for debugging *)
val rexp_term2da: env -> term -> automaton val rexp_term2da: theory -> env -> term -> automaton
val enabled : automaton -> env -> cid list val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton val next : automaton -> env -> cid -> automaton
val final : automaton -> bool val final : automaton -> bool
@ -187,23 +187,23 @@ local open RegExpChecker in
else () else ()
in res end; in res end;
fun conv \<^Const_>\<open>Regular_Exp.rexp.Zero _\<close> _ = Zero fun conv _ \<^Const_>\<open>Regular_Exp.rexp.Zero _\<close> _ = Zero
|conv \<^Const_>\<open>Regular_Exp.rexp.One _\<close> _ = Onea |conv _ \<^Const_>\<open>Regular_Exp.rexp.One _\<close> _ = Onea
|conv \<^Const_>\<open>Regular_Exp.rexp.Times _ for X Y\<close> env = Times(conv X env, conv Y env) |conv thy \<^Const_>\<open>Regular_Exp.rexp.Times _ for X Y\<close> env = Times(conv thy X env, conv thy Y env)
|conv \<^Const_>\<open>Regular_Exp.rexp.Plus _ for X Y\<close> env = Plus(conv X env, conv Y env) |conv thy \<^Const_>\<open>Regular_Exp.rexp.Plus _ for X Y\<close> env = Plus(conv thy X env, conv thy Y env)
|conv \<^Const_>\<open>Regular_Exp.rexp.Star _ for X\<close> env = Star(conv X env) |conv thy \<^Const_>\<open>Regular_Exp.rexp.Star _ for X\<close> env = Star(conv thy X env)
|conv \<^Const_>\<open>RegExpInterface.opt _ for X\<close> env = Plus(conv X env, Onea) |conv thy \<^Const_>\<open>RegExpInterface.opt _ for X\<close> env = Plus(conv thy X env, Onea)
|conv \<^Const_>\<open>RegExpInterface.rep1 _ for X\<close> env = Times(conv X env, Star(conv X env)) |conv thy \<^Const_>\<open>RegExpInterface.rep1 _ for X\<close> env = Times(conv thy X env, Star(conv thy X env))
|conv (Const (s, \<^Type>\<open>rexp _\<close>)) env = |conv _ (Const (s, \<^Type>\<open>rexp _\<close>)) env =
let val n = find_index (fn x => x = s) env let val n = find_index (fn x => x = s) env
val _ = if n<0 then error"conversion error of regexp." else () val _ = if n<0 then error"conversion error of regexp." else ()
in Atom(n) end 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_int = {equal = curry(op =) : Int.int -> Int.int -> bool};
val eq_bool_list = {equal = curry(op =) : bool list -> bool list -> 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 nda = RegExpChecker.rexp2na eq_int rexp;
val da = RegExpChecker.na2da eq_bool_list nda; val da = RegExpChecker.na2da eq_bool_list nda;
in da end; in da end;