From 9673359688d6ef7403aec4cac27d1f190fb2c306 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Fri, 27 May 2022 17:14:17 +0200
Subject: [PATCH] Enable high level invariants checking for some commands

Enable high level invariants checking for the update_instance*
and close_monitor* commands
---
 src/DOF/Isa_DOF.thy                        |  6 ++++++
 src/tests/High_Level_Syntax_Invariants.thy | 14 +++++++++++++-
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy
index e90abf3..e4a0492 100644
--- a/src/DOF/Isa_DOF.thy
+++ b/src/DOF/Isa_DOF.thy
@@ -1699,6 +1699,9 @@ fun update_instance_command  (((oid:string,pos),cid_pos),
             in     
                 thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value
                     |> check_inv
+                    |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
+                                  then Value_Command.Docitem_Parser.check_invariants thy oid
+                                  else thy)
             end
 
 
@@ -1755,6 +1758,9 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
                            o Context.Theory 
     in  thy |> update_instance_command args
             |> (fn thy => (check_inv thy; thy))
+            |> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
+                          then Value_Command.Docitem_Parser.check_invariants thy oid
+                          else thy)
             |> delete_monitor_entry
     end 
 
diff --git a/src/tests/High_Level_Syntax_Invariants.thy b/src/tests/High_Level_Syntax_Invariants.thy
index 5063220..204626f 100644
--- a/src/tests/High_Level_Syntax_Invariants.thy
+++ b/src/tests/High_Level_Syntax_Invariants.thy
@@ -34,6 +34,11 @@ text\<open>The  symbol \<^term>\<open>\<sigma>\<close> is reserved and reference
   Now let's define two instances, one of each class:\<close>
 
 text*[testinv1::class_inv1, int1=4]\<open>lorem ipsum...\<close>
+update_instance*[testinv1::class_inv1, int1:="3"]
+(* When not commented, should violated the invariant:
+update_instance*[testinv1::class_inv1, int1:=1]
+*)
+
 text*[testinv2::class_inv2, int1=3, int2=1]\<open>lorem ipsum...\<close>
 
 text\<open>
@@ -98,7 +103,6 @@ text\<open>Next we define some instances (docitems): \<close>
 declare[[invariants_checking_with_tactics = true]]
 
 text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
-(*text*[introduction1::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 0"]\<open>\<close>*)
 
 text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
 text*[resultArgument::result, evidence = "argument"]\<open>\<close>
@@ -112,6 +116,12 @@ declare[[invariants_checking_with_tactics = true]]
 
 text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
 text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
+(* When not commented, should violated the invariant:
+update_instance*[introduction2::introduction
+                  , authored_by := "{@{author \<open>church\<close>}}"
+                  , level := "Some 1"]
+*)
+
 text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
 text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
 
@@ -134,4 +144,6 @@ value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \
 
 declare[[invariants_checking_with_tactics = false]]
 
+declare[[invariants_checking = false]]
+
 end