From 8dedf86f228e2ce5eedfd2c6a21a49ca0c0d97d7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Tue, 5 May 2020 19:56:53 +0000
Subject: [PATCH] synchronize with compiler/core/Floor2_examp.thy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14176 3260e6d1-4efc-4170-b0a7-36055960796d
---
.../compiler_generic/toy_example/embedding/Core.thy | 4 +++-
.../toy_example/embedding/core/Floor2_examp.thy | 12 ++++++++++++
2 files changed, 15 insertions(+), 1 deletion(-)
diff --git a/Citadelle/src/compiler_generic/toy_example/embedding/Core.thy b/Citadelle/src/compiler_generic/toy_example/embedding/Core.thy
index 79fb2901bb0..d4f903dc4c7 100644
--- a/Citadelle/src/compiler_generic/toy_example/embedding/Core.thy
+++ b/Citadelle/src/compiler_generic/toy_example/embedding/Core.thy
@@ -115,6 +115,7 @@ local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_examp_d
local_setup \<open>embedding_fun_info_f1 @{const_name Floor1_examp.print_transition}\<close>
local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_transition_locale}\<close>
local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_transition_interp}\<close>
+local_setup \<open>embedding_fun_info_f2 @{const_name Floor2_examp.print_transition_def_state'}\<close>
local_setup \<open>embedding_fun_info_f1 @{const_name Floor1_ctxt.print_ctxt}\<close>
local_setup \<open>embedding_fun_info @{const_name print_meta_setup_def_state}\<close>
local_setup \<open>embedding_fun_info @{const_name print_meta_setup_def_transition}\<close>
@@ -189,7 +190,8 @@ definition "thy_def_transition = (\<lambda> Floor1 \<Rightarrow> Embed_theories
| Floor2 \<Rightarrow> Embed_locale
[ section' \<open>Transition (Floor 2)\<close> ]
Floor2_examp.print_transition_locale
- [ Floor2_examp.print_transition_interp ])"
+ [ Floor2_examp.print_transition_interp
+ , Floor2_examp.print_transition_def_state' ])"
definition "thy_ctxt = (\<lambda> Floor1 \<Rightarrow> Embed_theories
[ section' \<open>Context (Floor 1)\<close>
, floor1_PRINT_ctxt ]
diff --git a/Citadelle/src/compiler_generic/toy_example/embedding/core/Floor2_examp.thy b/Citadelle/src/compiler_generic/toy_example/embedding/core/Floor2_examp.thy
index 0bcac7c5a6a..347a6d04258 100644
--- a/Citadelle/src/compiler_generic/toy_example/embedding/core/Floor2_examp.thy
+++ b/Citadelle/src/compiler_generic/toy_example/embedding/core/Floor2_examp.thy
@@ -236,4 +236,16 @@ definition "print_transition_interp = get_state (\<lambda> _ _.
Interpretation n n (print_transition_locale_aux l)
(C.by [M.rule (T.thm s)])))"
+definition "print_transition_def_state' = get_state (\<lambda> pre post _.
+ (Pair o L.map O'.definition)
+ (L.map
+ (let a = \<lambda>f x. Term_app f [x]
+ ; b = \<lambda>s. Term_basic [s]
+ ; heap = \<open>heap\<close> in
+ (\<lambda>(s, _).
+ Definition (Term_rewrite (b (heap @@ \<open>_\<close> @@ s))
+ \<open>=\<close>
+ (a heap (b (print_examp_def_st_locale_name s @@ \<open>.\<close> @@ s))))))
+ [ pre, post ]))"
+
end
--
GitLab