From 8efc1300b42a59a06a5f2e231f317cf187fbd219 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 11 Mar 2022 11:30:34 +0000 Subject: [PATCH] Manual import of changes from /2021-ITP-PMTI. --- src/DOF/Isa_DOF.thy | 205 ++++++++++++++++++++++++++++++-------------- 1 file changed, 141 insertions(+), 64 deletions(-) diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index f163c05..777ca02 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -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>\True\ 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>\term*\ "read and print term" - (opt_modes -- Parse.term >> print_term); (* This is just a stub at present *) val _ = @@ -1744,13 +1728,15 @@ end \ -ML \ \\<^file>\~~/src/HOL/Tools/value_command.ML\\ + +ML \ \c.f. \<^file>\~~/src/HOL/Tools/value_command.ML\\ (* 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>\term*\ "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>\value*\ "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>\value*\ (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>\simp\, Code_Simp.dynamic_value) #> snd - #> add_evaluator (\<^binding>\nbe\, Nbe.dynamic_value) #> snd - #> add_evaluator (\<^binding>\code\, 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>\simp\, Code_Simp.dynamic_value) #> snd + #> add_evaluator (\<^binding>\nbe\, Nbe.dynamic_value) #> snd + #> add_evaluator (\<^binding>\code\, Code_Evaluation.dynamic_value_strict) + #> snd); end; \ + + +ML \ \c.f. \<^file>\~~/src/Pure/Isar/outer_syntax.ML\\ +(* + The ML* generates an "ontology-aware" version of the SML code-execution command. +*) +\ +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 +\ + + ML\ 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 \ char list \ char list"}) $ t1 $ t2) - = HOLogic.dest_string (Const ("List.list.Cons", @{typ "char \ char list \ char list"}) $ t1 $ t2) - | ltx_of_term _ _ (Const ("List.list.Nil", _)) = "" + fun ltx_of_term _ _ (Const (@{const_name \Cons\}, + @{typ "char \ char list \ char list"}) $ t1 $ t2) + = HOLogic.dest_string (Const (@{const_name \Cons\}, + @{typ "char \ char list \ char list"}) $ t1 $ t2) + | ltx_of_term _ _ (Const (@{const_name \Nil\}, _)) = "" | ltx_of_term _ _ (@{term "numeral :: _ \ _"} $ 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 \Cons\}, _) $ t1) $ t2) = + let val inner = (case t2 of + Const (@{const_name \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 (@{const_name \None\}, _)) = "" + | ltx_of_term ctxt _ (Const (@{const_name \Some\}, _)$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>\define_macro*\ "d \ + + + (* ML\ Pretty.text;