forked from Isabelle_DOF/Isabelle_DOF
Manual import of changes from /2021-ITP-PMTI.
This commit is contained in:
parent
4c0d3ccee3
commit
8efc1300b4
|
|
@ -37,8 +37,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
|||
|
||||
and "open_monitor*" "close_monitor*"
|
||||
"declare_reference*" "update_instance*"
|
||||
"doc_class"
|
||||
"onto_class" (* a wish from Idir *)
|
||||
"doc_class" "onto_class" (* a syntactic alternative *)
|
||||
"ML*"
|
||||
"define_shortcut*" "define_macro*" :: thy_decl
|
||||
|
||||
and "text*" "text-macro*" :: document_body
|
||||
|
|
@ -208,7 +208,7 @@ struct
|
|||
end)
|
||||
type ISA_transformers = {check :
|
||||
(theory -> term * typ * Position.T -> string -> term option),
|
||||
elaborate : (theory -> string -> typ -> term option -> term)
|
||||
elaborate : (theory -> string -> typ -> term option -> Position.T -> term)
|
||||
}
|
||||
|
||||
type ISA_transformer_tab = ISA_transformers Symtab.table
|
||||
|
|
@ -678,7 +678,7 @@ fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
|
|||
NONE => Const(s,ty) $ t
|
||||
(* checking isa, may raise error though. *)
|
||||
| SOME t => if mk_elaboration
|
||||
then elaborate thy s ty (SOME t)
|
||||
then elaborate thy s ty (SOME t) pos
|
||||
else Const(s,ty) $ t
|
||||
(* transforming isa *)
|
||||
else (Const(s,ty) $ (T t))
|
||||
|
|
@ -688,7 +688,7 @@ fun transduce_term_global {mk_elaboration=mk_elaboration} (term,pos) thy =
|
|||
NONE => error("undefined inner syntax antiquotation: "^s)
|
||||
| SOME({elaborate=elaborate, ...}) =>
|
||||
if mk_elaboration
|
||||
then elaborate thy s ty NONE
|
||||
then elaborate thy s ty NONE pos
|
||||
else Const(s, ty)
|
||||
(* transforming isa *)
|
||||
else Const(s, ty)
|
||||
|
|
@ -1039,19 +1039,28 @@ fun ML_isa_check_docitem thy (term, req_ty, pos) _ =
|
|||
else err ("faulty reference to docitem: "^name) pos
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option =
|
||||
fun ML_isa_elaborate_generic (_:theory) isa_name ty term_option pos =
|
||||
case term_option of
|
||||
NONE => error("Wrong term option. You must use a defined term")
|
||||
| SOME term => Const (isa_name, ty) $ term
|
||||
|
||||
fun elaborate_instance thy _ _ term_option =
|
||||
fun elaborate_instance thy _ _ term_option pos =
|
||||
case term_option of
|
||||
NONE => error ("Malformed term annotation")
|
||||
| SOME term => let val instance_name = HOLogic.dest_string term
|
||||
(*val _ = writeln("In elaborate_instance term: " ^ @{make_string} term)
|
||||
val _ = writeln("In elaborate_instance term: " ^ Syntax.string_of_term_global thy term)
|
||||
val _ = writeln("In elaborate_instance instance_name: " ^ instance_name)*)
|
||||
in case DOF_core.get_value_global instance_name thy of
|
||||
NONE => error ("No class instance: " ^ instance_name)
|
||||
| SOME(value) => value
|
||||
| SOME(value) =>
|
||||
let
|
||||
(*val _ = writeln("In elaborate_instance value: " ^ @{make_string} value)
|
||||
val _ = writeln("In elaborate_instance value: " ^ Syntax.string_of_term_global thy value)*)
|
||||
(*in value end*)
|
||||
in DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy end
|
||||
end
|
||||
(*DOF_core.transduce_term_global {mk_elaboration=true} (value, pos) thy*)
|
||||
|
||||
(*
|
||||
The function declare_ISA_class_accessor_and_check_instance uses a prefix
|
||||
|
|
@ -1082,7 +1091,7 @@ fun declare_ISA_class_accessor_and_check_instance doc_class_name =
|
|||
end)
|
||||
end
|
||||
|
||||
fun elaborate_instances_list thy isa_name _ _ =
|
||||
fun elaborate_instances_list thy isa_name _ _ pos =
|
||||
let
|
||||
val base_name = Long_Name.base_name isa_name
|
||||
fun get_isa_name_without_intances_suffix s =
|
||||
|
|
@ -1430,6 +1439,7 @@ fun check_invariants thy oid =
|
|||
let
|
||||
val value = the (DOF_core.get_value_global oid thy)
|
||||
val cid = #cid (the (DOF_core.get_object_global oid thy))
|
||||
(*val _ = writeln ("cid: " ^ @{make_string} (Long_Name.base_name cid))*)
|
||||
fun get_all_invariants cid thy =
|
||||
let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
|
||||
in case DOF_core.get_doc_class_global cid thy of
|
||||
|
|
@ -1465,10 +1475,16 @@ fun check_invariants thy oid =
|
|||
val _ = Goal.prove ctxt [] [] prop_term
|
||||
(K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
|
||||
|> Thm.close_derivation \<^here>
|
||||
handle ERROR e =>
|
||||
ISA_core.err ("Invariant "
|
||||
^ inv_name
|
||||
^ " failed to be checked using proof tactics"
|
||||
^ " with error: "
|
||||
^ e) pos
|
||||
(* If Goal.prove does not fail, then the evaluation is considered True,
|
||||
else an error is triggered by Goal.prove *)
|
||||
in @{term True} end)
|
||||
else (error e)
|
||||
else ISA_core.err ("Invariant " ^ inv_name ^ " violated." ) pos
|
||||
in (if evaluated_term = \<^term>\<open>True\<close>
|
||||
then ((inv_name, pos), term)
|
||||
else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos)
|
||||
|
|
@ -1478,7 +1494,7 @@ fun check_invariants thy oid =
|
|||
|
||||
fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy =
|
||||
let
|
||||
val id = serial ();
|
||||
val id = serial ();
|
||||
val _ = Position.report pos (docref_markup true oid id pos);
|
||||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
|
|
@ -1693,38 +1709,6 @@ val _ =
|
|||
(attributes -- Parse.opt_target -- Parse.document_source
|
||||
>> (Toplevel.theory o (gen_enriched_document_cmd {inline=true} I I {markdown = true} )));
|
||||
|
||||
(*
|
||||
term* command uses the same code as term command
|
||||
and adds the possibility to check Term Annotation Antiquotations (TA)
|
||||
with the help of DOF_core.transduce_term_global function
|
||||
*)
|
||||
fun string_of_term ctxt s trans =
|
||||
let
|
||||
val t = Syntax.read_term ctxt s;
|
||||
val T = Term.type_of t;
|
||||
val ctxt' = Proof_Context.augment t ctxt;
|
||||
val _ = DOF_core.transduce_term_global {mk_elaboration=false} (t , Toplevel.pos_of trans)
|
||||
(Proof_Context.theory_of ctxt');
|
||||
in
|
||||
Pretty.string_of
|
||||
(Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
|
||||
end;
|
||||
|
||||
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
|
||||
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
|
||||
string_of_term, so we pass the Toplevel.transition
|
||||
*)
|
||||
fun print_term (string_list, string) trans = print_item
|
||||
(fn state => fn string => string_of_term (Toplevel.context_of state) string trans)
|
||||
(string_list, string) trans;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
||||
(opt_modes -- Parse.term >> print_term);
|
||||
|
||||
(* This is just a stub at present *)
|
||||
val _ =
|
||||
|
|
@ -1744,13 +1728,15 @@ end
|
|||
|
||||
\<close>
|
||||
|
||||
ML \<comment> \<open>\<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close>
|
||||
|
||||
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/HOL/Tools/value_command.ML\<close>\<close>
|
||||
(*
|
||||
The value* command uses the same code as the value command
|
||||
and adds the possibility to evaluate Term Annotation Antiquotations (TA)
|
||||
and adds the evaluation Term Annotation Antiquotations (TA)
|
||||
with the help of the DOF_core.transduce_term_global function.
|
||||
*)
|
||||
(* Title: HOL/Tools/value_command.ML
|
||||
(* Based on:
|
||||
Title: HOL/Tools/value_command.ML
|
||||
Author: Florian Haftmann, TU Muenchen
|
||||
|
||||
Generic value command for arbitrary evaluators, with default using nbe or SML.
|
||||
|
|
@ -1799,7 +1785,9 @@ fun value_select name ctxt =
|
|||
then default_value ctxt
|
||||
else Name_Space.get (Evaluators.get (Proof_Context.theory_of ctxt)) name ctxt;
|
||||
|
||||
val value = value_select "";
|
||||
fun value ctxt term = value_select "" ctxt
|
||||
(DOF_core.transduce_term_global {mk_elaboration=true} (term , \<^here>)
|
||||
(Proof_Context.theory_of ctxt))
|
||||
|
||||
fun value_cmd raw_name modes raw_t state trans =
|
||||
let
|
||||
|
|
@ -1826,25 +1814,109 @@ val opt_evaluator =
|
|||
We want to have the current position to pass it to transduce_term_global in
|
||||
value_cmd, so we pass the Toplevel.transition
|
||||
*)
|
||||
|
||||
val opt_attributes = Scan.option ODL_Command_Parser.attributes
|
||||
|
||||
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 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
|
||||
and adds the possibility to check Term Annotation Antiquotations (TA)
|
||||
with the help of DOF_core.transduce_term_global function
|
||||
*)
|
||||
fun string_of_term ctxt s trans =
|
||||
let
|
||||
val t = Syntax.read_term ctxt s;
|
||||
val T = Term.type_of t;
|
||||
val ctxt' = Proof_Context.augment t ctxt;
|
||||
val _ = DOF_core.transduce_term_global {mk_elaboration=false} (t , Toplevel.pos_of trans)
|
||||
(Proof_Context.theory_of ctxt');
|
||||
in
|
||||
Pretty.string_of
|
||||
(Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
|
||||
Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
|
||||
end;
|
||||
|
||||
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
|
||||
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
|
||||
string_of_term, so we pass the Toplevel.transition
|
||||
*)
|
||||
fun print_term (string_list, string) trans = print_item
|
||||
(fn state => fn string => string_of_term (Toplevel.context_of state) string trans)
|
||||
(string_list, string) trans;
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
||||
(opt_attributes -- (opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
print_term eval_args));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
|
||||
(opt_evaluator -- opt_modes -- Parse.term >> pass_trans_to_value_cmd);
|
||||
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
pass_trans_to_value_cmd eval_args));
|
||||
|
||||
val _ = Theory.setup
|
||||
(Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value*\<close>
|
||||
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
|
||||
(fn ctxt => fn ((name, style), t) =>
|
||||
Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
|
||||
#> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
|
||||
(fn ctxt => fn ((name, style), t) =>
|
||||
Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
|
||||
#> add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict)
|
||||
#> snd);
|
||||
|
||||
end;
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
ML \<comment> \<open>c.f. \<^file>\<open>~~/src/Pure/Isar/outer_syntax.ML\<close>\<close>
|
||||
(*
|
||||
The ML* generates an "ontology-aware" version of the SML code-execution command.
|
||||
*)
|
||||
\<open>
|
||||
structure ML_star_Command =
|
||||
struct
|
||||
|
||||
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))
|
||||
|
||||
val attributes_opt = Scan.option ODL_Command_Parser.attributes
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("ML*", \<^here>) "ODL annotated ML text within theory or local theory"
|
||||
((attributes_opt -- Parse.ML_source)
|
||||
>> (fn (meta_args_opt, source) =>
|
||||
Toplevel.theory (meta_args_exec meta_args_opt)
|
||||
#>
|
||||
Toplevel.generic_theory
|
||||
(ML_Context.exec (fn () =>
|
||||
ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #>
|
||||
Local_Theory.propagate_ml_env)));
|
||||
|
||||
end
|
||||
\<close>
|
||||
|
||||
|
||||
ML\<open>
|
||||
structure ODL_LTX_Converter =
|
||||
struct
|
||||
|
|
@ -1862,18 +1934,20 @@ fun meta_args_2_string thy ((((lab, _), cid_opt), attr_list) : ODL_Command_Parse
|
|||
(* val _ = writeln("meta_args_2_string cid_long:"^ cid_long ) *)
|
||||
val cid_txt = "type = " ^ (enclose "{" "}" cid_long);
|
||||
|
||||
fun ltx_of_term _ _ (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2)
|
||||
= HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2)
|
||||
| ltx_of_term _ _ (Const ("List.list.Nil", _)) = ""
|
||||
fun ltx_of_term _ _ (Const (@{const_name \<open>Cons\<close>},
|
||||
@{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2)
|
||||
= HOLogic.dest_string (Const (@{const_name \<open>Cons\<close>},
|
||||
@{typ "char \<Rightarrow> char list \<Rightarrow> char list"}) $ t1 $ t2)
|
||||
| ltx_of_term _ _ (Const (@{const_name \<open>Nil\<close>}, _)) = ""
|
||||
| ltx_of_term _ _ (@{term "numeral :: _ \<Rightarrow> _"} $ t) = Int.toString(HOLogic.dest_numeral t)
|
||||
| ltx_of_term ctx encl ((Const ("List.list.Cons", _) $ t1) $ t2) =
|
||||
let val inner = (case t2 of
|
||||
Const ("List.list.Nil", _) => (ltx_of_term ctx true t1)
|
||||
| _ => ((ltx_of_term ctx false t1)^", " ^(ltx_of_term ctx false t2))
|
||||
)
|
||||
in if encl then enclose "{" "}" inner else inner end
|
||||
| ltx_of_term _ _ (Const ("Option.option.None", _)) = ""
|
||||
| ltx_of_term ctxt _ (Const ("Option.option.Some", _)$t) = ltx_of_term ctxt true t
|
||||
| ltx_of_term ctx encl ((Const (@{const_name \<open>Cons\<close>}, _) $ t1) $ t2) =
|
||||
let val inner = (case t2 of
|
||||
Const (@{const_name \<open>Nil\<close>}, _) => (ltx_of_term ctx true t1)
|
||||
| _ => ((ltx_of_term ctx false t1)^", " ^(ltx_of_term ctx false t2))
|
||||
)
|
||||
in if encl then enclose "{" "}" inner else inner end
|
||||
| ltx_of_term _ _ (Const (@{const_name \<open>None\<close>}, _)) = ""
|
||||
| ltx_of_term ctxt _ (Const (@{const_name \<open>Some\<close>}, _)$t) = ltx_of_term ctxt true t
|
||||
| ltx_of_term ctxt _ t = ""^(Sledgehammer_Util.hackish_string_of_term ctxt t)
|
||||
|
||||
|
||||
|
|
@ -2533,6 +2607,9 @@ val _ = Outer_Syntax.command \<^command_keyword>\<open>define_macro*\<close> "d
|
|||
|
||||
\<close>
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
ML\<open>
|
||||
Pretty.text;
|
||||
|
|
|
|||
Loading…
Reference in New Issue