From 207029e70ea7980f34229d9a0aff70ff96803865 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Wed, 14 Feb 2024 11:15:13 +0100
Subject: [PATCH] Enable term anti-quotations in class invariants

---
 .../Concept_High_Level_Invariants.thy         | 36 +++++++++++++++++++
 Isabelle_DOF/thys/Isa_DOF.thy                 |  3 +-
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy b/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy
index 7393db5..d798623 100644
--- a/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy
+++ b/Isabelle_DOF-Unit-Tests/Concept_High_Level_Invariants.thy
@@ -241,4 +241,40 @@ declare[[invariants_checking_with_tactics = false]]
 
 declare[[invariants_strict_checking = false]]
 
+text\<open>Invariants can have term anti-quotations\<close>
+doc_class invA =
+a :: int
+
+text*[invA_inst::invA, a = 3]\<open>\<close>
+
+doc_class invB = invA +
+b :: int
+invariant a_pos :: "a \<sigma> \<ge> 0"
+
+text*[invB_inst::invB, a = 3]\<open>\<close>
+
+doc_class invC =
+c :: invB
+invariant a_invB_pos :: "a (c \<sigma>) \<ge> a @{invA \<open>invA_inst\<close>}"
+
+text*[invC_inst::invC, c = "@{invB \<open>invB_inst\<close>}"]\<open>\<close>
+
+text\<open>Bug:
+With the polymorphic class implementation, invariants type inference is to permissive:
+\<close>
+doc_class invA' =
+a :: int
+
+doc_class invB' = invA' +
+b :: int
+invariant a_pos :: "a \<sigma> \<ge> 0"
+
+doc_class ('a, 'b) invC' =
+c :: invB'
+d :: "'a list"
+e :: "'b list"
+invariant a_pos :: "a \<sigma> \<ge> 0"
+text\<open>The \<^const>\<open>a\<close> selector in the \<^const>\<open>a_pos_inv\<close> invariant of the class \<^doc_class>\<open>('a, 'b) invC'\<close>
+should be rejected as the class does not have nor inherit an \<^const>\<open>a\<close> attribute
+\<close>
 end
diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy
index d383f8d..56f4a0b 100644
--- a/Isabelle_DOF/thys/Isa_DOF.thy
+++ b/Isabelle_DOF/thys/Isa_DOF.thy
@@ -3056,7 +3056,8 @@ fun define_cond bind eq (ctxt:local_theory) =
        in def_cmd args ctxt end
 
 fun define_inv (bind, inv) thy = 
-    let val inv_parsed_term = Syntax.parse_term (Proof_Context.init_global thy) inv
+    let val ctxt = Proof_Context.init_global thy
+        val inv_parsed_term = Syntax.parse_term ctxt inv |> DOF_core.elaborate_term' ctxt
         val abs_term = Term.lambda (Free (instance_placeholderN, dummyT)) inv_parsed_term
         val eq = Logic.mk_equals (Free(Binding.name_of bind, dummyT), abs_term)
                  |> Syntax.check_term (Proof_Context.init_global thy)