nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix scheduling problem for term* and value* 

Toplevel transition only allows atomic transactions.
So we avoid sequantial combinators
This commit is contained in:
Nicolas Méric 2022-03-14 15:27:13 +01:00
parent 5af219469d
commit a332109dca
1 changed files with 21 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
src/DOF/Isa_DOF.thy
View File

@ -1746,7 +1746,8 @@ signature VALUE_COMMAND =
sig sig
val value: Proof.context -> term -> term val value: Proof.context -> term -> term
val value_select: string -> Proof.context -> term -> term val value_select: string -> Proof.context -> term -> term
val value_cmd: xstring -> string list -> string -> Toplevel.state -> Toplevel.transition -> unit val value_cmd: (ODL_Command_Parser.meta_args_t option) -> xstring -> string list -> string
-> Toplevel.state -> Toplevel.transition -> unit
val add_evaluator: binding * (Proof.context -> term -> term) val add_evaluator: binding * (Proof.context -> term -> term)
-> theory -> string * theory -> theory -> string * theory
end; end;
@ -1788,9 +1789,15 @@ fun value_select name ctxt =
fun value ctxt term = value_select "" ctxt fun value ctxt term = value_select "" ctxt
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>) (DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
(Proof_Context.theory_of ctxt)) (Proof_Context.theory_of ctxt))
fun meta_args_exec NONE thy = thy
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy =
thy |> (ODL_Command_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false}
oid pos (I cid_pos) (I doc_attrs))
fun value_cmd raw_name modes raw_t state trans = fun value_cmd meta_args_opt raw_name modes raw_t state trans =
let let
val _ = meta_args_exec meta_args_opt
val ctxt = Toplevel.context_of state; val ctxt = Toplevel.context_of state;
val name = intern_evaluator ctxt raw_name; val name = intern_evaluator ctxt raw_name;
val t = Syntax.read_term ctxt raw_t; val t = Syntax.read_term ctxt raw_t;
@ -1817,22 +1824,17 @@ val opt_evaluator =
val opt_attributes = Scan.option ODL_Command_Parser.attributes val opt_attributes = Scan.option ODL_Command_Parser.attributes
fun meta_args_exec NONE thy = thy fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans =
|meta_args_exec (SOME ((((oid,pos),cid_pos), doc_attrs) : ODL_Command_Parser.meta_args_t)) thy = Toplevel.keep (fn state => value_cmd meta_args_opt name modes t state trans) trans
thy |> (ODL_Command_Parser.create_and_check_docitem
{is_monitor = false} {is_inline = false}
oid pos (I cid_pos) (I doc_attrs))
fun pass_trans_to_value_cmd ((name, modes), t) trans =
Toplevel.keep (fn state => value_cmd name modes t state trans) trans
(* (*
term* command uses the same code as term command term* command uses the same code as term command
and adds the possibility to check Term Annotation Antiquotations (TA) and adds the possibility to check Term Annotation Antiquotations (TA)
with the help of DOF_core.transduce_term_global function with the help of DOF_core.transduce_term_global function
*) *)
fun string_of_term ctxt s trans = fun string_of_term meta_args_opt ctxt s trans =
let let
val _ = meta_args_exec meta_args_opt
val t = Syntax.read_term ctxt s; val t = Syntax.read_term ctxt s;
val T = Term.type_of t; val T = Term.type_of t;
val ctxt' = Proof_Context.augment t ctxt; val ctxt' = Proof_Context.augment t ctxt;
@ -1851,25 +1853,24 @@ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
We want to have the current position to pass it to transduce_term_global in We want to have the current position to pass it to transduce_term_global in
string_of_term, so we pass the Toplevel.transition string_of_term, so we pass the Toplevel.transition
*) *)
fun print_term (string_list, string) trans = print_item fun print_term meta_args_opt (string_list, string) trans = print_item
(fn state => fn string => string_of_term (Toplevel.context_of state) string trans) (fn state =>
(string_list, string) trans; fn string =>
string_of_term meta_args_opt (Toplevel.context_of state) string trans)
(string_list, string) trans;
val _ = val _ =
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term" Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
(opt_attributes -- (opt_modes -- Parse.term) (opt_attributes -- (opt_modes -- Parse.term)
>> (fn (meta_args_opt, eval_args ) => >> (fn (meta_args_opt, eval_args ) => print_term meta_args_opt eval_args));
Toplevel.theory (meta_args_exec meta_args_opt)
#>
print_term eval_args));
val _ = val _ =
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term" Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term) (opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
>> (fn (meta_args_opt, eval_args ) => >> (fn (meta_args_opt, eval_args ) =>
Toplevel.theory (meta_args_exec meta_args_opt) Toplevel.theory (meta_args_exec meta_args_opt)
#> #>
pass_trans_to_value_cmd eval_args)); pass_trans_to_value_cmd meta_args_opt eval_args));
val _ = Theory.setup val _ = Theory.setup
(Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close> (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>