From 5637ca1371791877ac5b40ed16c4b247dcf2bb03 Mon Sep 17 00:00:00 2001 From: Kangfeng Ye Date: Tue, 21 May 2024 22:36:10 +0100 Subject: [PATCH] Update to Isabelle2023 --- RoboChart/ITree_RoboChart.thy | 4 +++- RoboChart/RoboChart_Simulation.thy | 8 +++---- .../examples/Patrol_Robot/Patrol_Robot.thy | 22 +++++++++---------- ...rt_ChemicalDetector_autonomous_general.thy | 4 +++- .../RoboChart_basic/RoboChart_basic.thy | 3 ++- 5 files changed, 23 insertions(+), 18 deletions(-) diff --git a/RoboChart/ITree_RoboChart.thy b/RoboChart/ITree_RoboChart.thy index 291e35e..f0c9bc2 100644 --- a/RoboChart/ITree_RoboChart.thy +++ b/RoboChart/ITree_RoboChart.thy @@ -1,7 +1,9 @@ section \ RoboChart semantics \ theory ITree_RoboChart - imports "Interaction_Trees.ITree_Extraction" "HOL-Library.Numeral_Type" + imports "Interaction_Trees.ITree_Extraction" + "Interaction_Trees.ITree_Deadlock" + "HOL-Library.Numeral_Type" "ITree_UTP.ITree_CSP_Biased" begin diff --git a/RoboChart/RoboChart_Simulation.thy b/RoboChart/RoboChart_Simulation.thy index 3ccff9a..7f6ac4a 100644 --- a/RoboChart/RoboChart_Simulation.thy +++ b/RoboChart/RoboChart_Simulation.thy @@ -12,9 +12,9 @@ begin generate_file \code/simulate/Simulate.hs\ = \ module Simulate (simulate) where import Interaction_Trees; -import Partial_Fun; +import Prelude; +-- import Partial_Fun; import System.IO; -import qualified Data.List.Split; import qualified Data.List; -- These library functions help us to trim the "_C" strings from pretty printed events @@ -29,7 +29,7 @@ removeSubstr w "" = ""; removeSubstr w s@(c:cs) = (if w `isPrefixOf` s then Prelude.drop (Prelude.length w) s else c : removeSubstr w cs); replace :: String -> String -> String -> String; -replace old new = Data.List.intercalate new . Data.List.Split.splitOn old; +replace old new orig = orig;-- Data.List.intercalate new . old; renameGasEvent :: String -> String; renameGasEvent gas = @@ -165,7 +165,7 @@ fun simulate model thy = let val ctx = Named_Target.theory_init thy val ctx' = (Code_Target.export_code true [Code.read_const (Local_Theory.exit_global ctx) model] [((("Haskell", ""), SOME ({physical = false}, (Path.explode "simulate", Position.none))), (Token.explode (Thy_Header.get_keywords' @{context}) Position.none "string_classes"))] ctx) - |> prep_simulation model (Context.theory_name thy) + |> prep_simulation model (Context.theory_name {long = false} thy) in run_simulation (Local_Theory.exit_global ctx'); (Local_Theory.exit_global ctx') end diff --git a/RoboChart/examples/Patrol_Robot/Patrol_Robot.thy b/RoboChart/examples/Patrol_Robot/Patrol_Robot.thy index 0709d38..0cc18f5 100644 --- a/RoboChart/examples/Patrol_Robot/Patrol_Robot.thy +++ b/RoboChart/examples/Patrol_Robot/Patrol_Robot.thy @@ -1379,14 +1379,14 @@ export_code D__PatrolMod in Haskell (* module_name RoboChart_basic *) - file_prefix RoboChart_basic_v1 + file_prefix Patrol_Robot (string_classes) text \A simulation file is generated as a pure Haskell code. \ -generate_file \code/RoboChart_basic_v1/Simulate.hs\ = +generate_file \code/Patrol_Robot/Simulate.hs\ = \module Simulate (simulate) where import qualified Interaction_Trees; -import qualified Partial_Fun; +-- import qualified Partial_Fun; isPrefixOf :: (Eq a) => [a] -> [a] -> Bool; isPrefixOf [] _ = True; @@ -1406,8 +1406,8 @@ simulate_cnt n (Interaction_Trees.Sil p) = } else simulate_cnt (n + 1) p }; -simulate_cnt n (Interaction_Trees.Vis (Partial_Fun.Pfun_of_alist [])) = Prelude.putStrLn "Deadlocked."; -simulate_cnt n t@(Interaction_Trees.Vis (Partial_Fun.Pfun_of_alist m)) = +simulate_cnt n (Interaction_Trees.Vis (Interaction_Trees.Pfun_of_alist [])) = Prelude.putStrLn "Deadlocked."; +simulate_cnt n t@(Interaction_Trees.Vis (Interaction_Trees.Pfun_of_alist m)) = do { Prelude.putStrLn ("Events:" ++ Prelude.concat (map (\(n, e) -> " (" ++ Prelude.show n ++ ") " ++ removeSubstr "_C" e ++ ";") (zip [1..] (map (Prelude.show . fst) m)))); e <- Prelude.getLine; case (Prelude.reads e) of @@ -1427,20 +1427,20 @@ text \The @{verbatim Main.hs} generated below is the main module in the ge to compile and build the generated code to an executable file by ghc. We note a compiled version has better performance than the interpreted version by ghci. \ -generate_file \code/RoboChart_basic_v1/Main.hs\ = +generate_file \code/Patrol_Robot/Main.hs\ = \import qualified Interaction_Trees; -import qualified Partial_Fun; +-- import qualified Partial_Fun; import qualified Simulate; -import qualified RoboChart_basic_v1; +import qualified Patrol_Robot; main :: IO () main = do - Simulate.simulate (RoboChart_basic_v1.d_PatrolMod 0); + Simulate.simulate (Patrol_Robot.d_PatrolMod 0); \ export_generated_files - \code/RoboChart_basic_v1/Simulate.hs\ - \code/RoboChart_basic_v1/Main.hs\ + \code/Patrol_Robot/Simulate.hs\ + \code/Patrol_Robot/Main.hs\ end diff --git a/RoboChart/examples/RoboChart_ChemicalDetector_autonomous/RoboChart_ChemicalDetector_autonomous_general.thy b/RoboChart/examples/RoboChart_ChemicalDetector_autonomous/RoboChart_ChemicalDetector_autonomous_general.thy index c23923b..16c3269 100644 --- a/RoboChart/examples/RoboChart_ChemicalDetector_autonomous/RoboChart_ChemicalDetector_autonomous_general.thy +++ b/RoboChart/examples/RoboChart_ChemicalDetector_autonomous/RoboChart_ChemicalDetector_autonomous_general.thy @@ -87,7 +87,9 @@ Sect.~\ref{sec:chem_module}. section \ General definitions \label{sec:chem_general}\ theory RoboChart_ChemicalDetector_autonomous_general - imports "ITree_RoboChart.ITree_RoboChart" "ITree_RoboChart.RoboChart_Simulation" + imports "ITree_RoboChart.ITree_RoboChart" + "ITree_Simulation.ITree_Simulation" + "ITree_RoboChart.RoboChart_Simulation" "Z_Toolkit.Bounded_List" begin diff --git a/RoboChart/examples/RoboChart_basic/RoboChart_basic.thy b/RoboChart/examples/RoboChart_basic/RoboChart_basic.thy index c3a19a9..89649bf 100644 --- a/RoboChart/examples/RoboChart_basic/RoboChart_basic.thy +++ b/RoboChart/examples/RoboChart_basic/RoboChart_basic.thy @@ -34,7 +34,8 @@ This theory, on the contrary, is built from the bottom up because the definition relies on the definitions of other processes in the top process. \ theory RoboChart_basic - imports "ITree_RoboChart.ITree_RoboChart" "ITree_Simulation.ITree_Simulation" + imports "Interaction_Trees.ITree_Deadlock" + "ITree_RoboChart.ITree_RoboChart" "ITree_Simulation.ITree_Simulation" begin text \We, therefore, structure the theory as follows. In Sect.~\ref{ssec:basic_general}, we give