forked from Isabelle_DOF/Isabelle_DOF
Parallelization of assert*, term*, value*, first try
This commit is contained in:
Nicolas Méric
parent
4f8e588138
commit
203b19ff8b
|
|
@ -152,10 +152,10 @@ val _ =
|
|||
|
||||
|
||||
val _ =
|
||||
let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) trans =
|
||||
(Value_Command.value_cmd {assert=false} args name modes t @{here} trans
|
||||
let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) thy =
|
||||
(Value_Command.value_cmd' {assert=false} args name modes t @{here} thy
|
||||
handle ERROR msg => (if error_match src msg
|
||||
then (writeln ("Correct error: "^msg^": reported.");trans)
|
||||
then (writeln ("Correct error: "^msg^": reported.");thy)
|
||||
else error"Wrong error reported"))
|
||||
in Outer_Syntax.command \<^command_keyword>\<open>value-assert-error\<close> "evaluate and print term"
|
||||
(ODL_Meta_Args_Parser.opt_attributes --
|
||||
|
|
|
|||
|
|
@ -1837,31 +1837,36 @@ fun meta_args_exec (meta_args as (((oid, pos), cid_pos), doc_attrs) : ODL_Meta_A
|
|||
{is_monitor = false} {is_inline = true} {define = true}
|
||||
oid pos (I cid_pos) (I doc_attrs))
|
||||
|
||||
fun value_cmd {assert=assert} meta_args_opt raw_name modes raw_t pos thy =
|
||||
let
|
||||
val thy' = meta_args_exec meta_args_opt thy
|
||||
val name = intern_evaluator thy' raw_name;
|
||||
val t = Syntax.read_term_global thy' raw_t;
|
||||
val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos)
|
||||
(thy');
|
||||
val t' = value_select name (Proof_Context.init_global thy') term';
|
||||
val ty' = Term.type_of t';
|
||||
val ty' = if assert
|
||||
then case ty' of
|
||||
\<^typ>\<open>bool\<close> => ty'
|
||||
| _ => error "Assertion expressions must be boolean."
|
||||
else ty'
|
||||
val t' = if assert
|
||||
then case t' of
|
||||
\<^term>\<open>True\<close> => t'
|
||||
| _ => error "Assertion failed."
|
||||
else t'
|
||||
val ctxt' = Proof_Context.augment t' (Proof_Context.init_global thy');
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
||||
val _ = Pretty.writeln p
|
||||
in thy' end;
|
||||
fun value_cmd {assert=assert} raw_name modes raw_t pos state =
|
||||
let
|
||||
val thy' = Toplevel.theory_of state;
|
||||
val name = intern_evaluator thy' raw_name;
|
||||
val t = Syntax.read_term_global thy' raw_t;
|
||||
val term' = DOF_core.transduce_term_global {mk_elaboration=true} (t , pos)
|
||||
(thy');
|
||||
val t' = value_select name (Proof_Context.init_global thy') term';
|
||||
val ty' = Term.type_of t';
|
||||
val ty' = if assert
|
||||
then case ty' of
|
||||
\<^typ>\<open>bool\<close> => ty'
|
||||
| _ => error "Assertion expressions must be boolean."
|
||||
else ty'
|
||||
val t'' = if assert
|
||||
then case t' of
|
||||
\<^term>\<open>True\<close> => t'
|
||||
| _ => error "Assertion failed."
|
||||
else t'
|
||||
val ctxt' = Proof_Context.augment t'' (Proof_Context.init_global thy');
|
||||
val p = Print_Mode.with_modes modes (fn () =>
|
||||
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t''), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
|
||||
in Pretty.writeln p end;
|
||||
|
||||
fun value_cmd' assert meta_args_opt raw_name modes raw_t pos thy =
|
||||
let
|
||||
val thy' = meta_args_exec meta_args_opt thy
|
||||
val _ = value_cmd assert raw_name modes raw_t pos (Toplevel.theory_toplevel thy')
|
||||
in thy' end;
|
||||
|
||||
val opt_modes =
|
||||
Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\<open>)\<close>)) [];
|
||||
|
|
@ -1871,8 +1876,9 @@ val opt_evaluator =
|
|||
|
||||
fun pass_trans_to_value_cmd meta_args_opt ((name, modes), t) trans =
|
||||
let val pos = Toplevel.pos_of trans
|
||||
in
|
||||
trans |> Toplevel.theory (value_cmd {assert=false} meta_args_opt name modes t pos)
|
||||
in if meta_args_opt = ODL_Meta_Args_Parser.empty_meta_args
|
||||
then trans |> Toplevel.keep (value_cmd {assert=false} name modes t pos)
|
||||
else trans |> Toplevel.theory (value_cmd' {assert=false} meta_args_opt name modes t pos)
|
||||
end
|
||||
|
||||
\<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/isar_cmd.ML\<close>\<close>
|
||||
|
|
@ -1882,7 +1888,7 @@ end
|
|||
and adds the possibility to check Term Annotation Antiquotations (TA)
|
||||
with the help of DOF_core.transduce_term_global function
|
||||
*)
|
||||
fun string_of_term s pos ctxt =
|
||||
fun string_of_term ctxt pos s =
|
||||
let
|
||||
val t = Syntax.read_term ctxt s;
|
||||
val T = Term.type_of t;
|
||||
|
|
@ -1898,14 +1904,16 @@ end;
|
|||
fun print_item string_of (modes, arg) state =
|
||||
Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ();
|
||||
|
||||
fun prin t pos state _ = string_of_term t pos (Toplevel.context_of state)
|
||||
fun prin s pos state _ = string_of_term (Toplevel.context_of state) pos s
|
||||
|
||||
fun print_term meta_args_opt (string_list, string) trans =
|
||||
let
|
||||
val pos = Toplevel.pos_of trans
|
||||
in meta_args_exec meta_args_opt
|
||||
#> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.theory_toplevel thy))
|
||||
|> (fn thy => Toplevel.theory thy trans)
|
||||
in if meta_args_opt = ODL_Meta_Args_Parser.empty_meta_args
|
||||
then Toplevel.keep (print_item (prin string pos) (string_list, string)) trans
|
||||
else meta_args_exec meta_args_opt
|
||||
#> tap (fn thy => print_item (prin string pos) (string_list, string) (Toplevel.theory_toplevel thy))
|
||||
|> (fn thy => Toplevel.theory thy trans)
|
||||
end
|
||||
|
||||
val (disable_assert_evaluation, disable_assert_evaluation_setup)
|
||||
|
|
@ -1915,14 +1923,20 @@ val _ = Theory.setup disable_assert_evaluation_setup
|
|||
|
||||
fun pass_trans_to_assert_value_cmd meta_args_opt ((name, modes), t) trans =
|
||||
let val pos = Toplevel.pos_of trans
|
||||
in trans
|
||||
|> Toplevel.theory
|
||||
(fn thy =>
|
||||
if Config.get_global thy disable_assert_evaluation
|
||||
then (meta_args_exec meta_args_opt
|
||||
#> tap (fn thy => print_item (prin t pos) (modes, t) (Toplevel.theory_toplevel thy)))
|
||||
thy
|
||||
else value_cmd {assert=true} meta_args_opt name modes t pos thy)
|
||||
in if meta_args_opt = ODL_Meta_Args_Parser.empty_meta_args
|
||||
then trans |> Toplevel.keep
|
||||
(fn state =>
|
||||
let val thy = Toplevel.theory_of state
|
||||
in if Config.get_global thy disable_assert_evaluation
|
||||
then print_item (prin t pos) (modes, t) state
|
||||
else value_cmd {assert=true} name modes t pos state end)
|
||||
else trans |> Toplevel.theory
|
||||
(fn thy =>
|
||||
if Config.get_global thy disable_assert_evaluation
|
||||
then thy |> (meta_args_exec meta_args_opt
|
||||
#> tap (fn thy => (Toplevel.theory_toplevel thy)
|
||||
|> print_item (prin t pos) (modes, t)))
|
||||
else (value_cmd' {assert=true} meta_args_opt name modes t pos) thy)
|
||||
end
|
||||
|
||||
(* setup ontology aware commands *)
|
||||
|
|
|
|||
Loading…
Reference in New Issue