|
|
|
@ -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 *)
|
|
|
|
|