Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF

This commit is contained in:
Achim D. Brucker 2024-04-02 08:34:13 +01:00
parent 5d5eef1a46 291b2e258f
commit f0c379a5d2
2 changed files with 40 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
Isabelle_DOF-Unit-Tests/Test_Polymorphic_Classes.thy
View File

@ -693,4 +693,27 @@ lemma*[e5::E] testtest : "xx + testtest_level = yy + testtest_level \<Longrighta
text\<open>Indeed this fails:\<close>
(*lemma*[e6::E] testtest : "xx + the (level @{test2 \<open>testtest2''\<close>}) = yy + the (level @{test2 \<open>testtest2''\<close>}) \<Longrightarrow> xx = yy" by simp*)
text\<open>Bug: Checking of \<^theory_text>\<open>text*\<close> type against \<^theory_text>\<open>declare_reference*\<close> is not done.
Should be compatible with type unification mechanism. See the record package\<close>
doc_class 'a AAA_test =
aaa::"'a list"
doc_class 'a BBB_test =
bbb::"'a list"
declare_reference*[aaa_test::"'a::one AAA_test"]
text\<open>@{AAA_test (unchecked) \<open>aaa_test\<close>}\<close>
text\<open>\<open>aaa_test\<close> should fail and trigger an error because its type was \<^typ>\<open>'a::one AAA_test\<close>
in the \<^theory_text>\<open>declare_reference*\<close> command:\<close>
(*text*[aaa_test::"'a::one BBB_test"]\<open>\<close>*)
text*[aaa_test::"int AAA_test"]\<open>\<close>
text\<open>\<open>aaa_test'\<close> should fail and trigger an error because its type \<^typ>\<open>string AAA_test\<close>
is not compatible with its type \<^typ>\<open>'a::one AAA_test\<close> declared in
the \<^theory_text>\<open>declare_reference*\<close> command:\<close>
text*[aaa_test'::"string AAA_test"]\<open>\<close>
end

28
Isabelle_DOF/thys/Isa_DOF.thy
View File

@ -1821,7 +1821,12 @@ fun check_invariants thy binding =
let val ctxt = Proof_Context.init_global thy
val trivial_true = \<^term>\<open>True\<close> |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
val evaluated_term = value ctxt term
handle ERROR e =>
handle Match => error ("exception Match raised when checking "
^ inv_name ^ " invariant." ^ Position.here pos ^ "\n"
^ "You might want to check the definition of the invariant\n"
^ "against the value specified in the instance\n"
^ "or the default value declared in the instance class.")
| ERROR e =>
if (String.isSubstring "Wellsortedness error" e)
andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
then (warning("Invariants checking uses proof tactics");
@ -2905,6 +2910,7 @@ fun compute_trace_ML ctxt oid pos_opt pos' =
val parse_oid = Scan.lift(Parse.position Args.name)
val parse_cid = Scan.lift(Parse.position Args.name)
val parse_oid' = Term_Style.parse -- parse_oid
val parse_oid'' = Scan.lift(Parse.embedded_position)
val parse_cid' = Term_Style.parse -- parse_cid
@ -2949,13 +2955,6 @@ fun compute_cid_repr ctxt cid _ =
let val _ = DOF_core.get_onto_class_name_global cid (Proof_Context.theory_of ctxt)
in Const(cid,dummyT) end
fun compute_name_repr ctxt oid pos =
let val instances = DOF_core.get_instances ctxt
val markup = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt)
|> Name_Space.markup (Name_Space.space_of_table instances)
val _ = Context_Position.report ctxt pos markup;
in HOLogic.mk_string oid end
local
fun pretty_attr_access_style ctxt (style, ((attr,pos),(oid,pos'))) =
@ -2965,8 +2964,15 @@ fun pretty_trace_style ctxt (style, (oid,pos)) =
Document_Output.pretty_term ctxt (style (ISA_core.compute_attr_access (Context.Proof ctxt)
traceN oid NONE pos));
fun pretty_name_style ctxt (style, (oid,pos)) =
Document_Output.pretty_term ctxt (style (compute_name_repr ctxt oid pos))
fun pretty_name_style ctxt (oid,pos) =
let
val instances = DOF_core.get_instances ctxt
val ns = Name_Space.space_of_table instances
val name = DOF_core.get_instance_name_global oid (Proof_Context.theory_of ctxt)
val ctxt' = Config.put Name_Space.names_unique true ctxt
val _ = name |> Name_Space.markup ns
|> Context_Position.report ctxt pos
in Name_Space.pretty ctxt' ns name end
fun pretty_cid_style ctxt (style, (cid,pos)) =
Document_Output.pretty_term ctxt (style (compute_cid_repr ctxt cid pos));
@ -3004,7 +3010,7 @@ val _ = Theory.setup
basic_entity \<^binding>\<open>doc_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>onto_class\<close> parse_cid' pretty_cid_style #>
basic_entity \<^binding>\<open>docitem_attribute\<close> parse_attribute_access' pretty_attr_access_style #>
basic_entity \<^binding>\<open>docitem_name\<close> parse_oid' pretty_name_style
basic_entity \<^binding>\<open>docitem_name\<close> parse_oid'' pretty_name_style
)
end
end