From f5ce1c8f89a83185c372e97e49ba6d71c1678f31 Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Fri, 20 Mar 2009 11:26:54 +0000 Subject: [PATCH] Added the code to mobilise arrays inside protocols --- transformations/ImplicitMobility.hs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/transformations/ImplicitMobility.hs b/transformations/ImplicitMobility.hs index 88ad029..02f9cb5 100644 --- a/transformations/ImplicitMobility.hs +++ b/transformations/ImplicitMobility.hs @@ -247,6 +247,25 @@ mobiliseArrays = pass "Make all arrays mobile" [] [] recurse let A.Proc _ _ _ stub = A.ndSpecType nd in newSpecF stub}) return $ A.Spec m (A.Specification m' n (newSpecF body')) scope' + doStructured (A.Spec m (A.Specification m' n (A.Protocol m'' ts)) scope) + = do let ts' = [case t of + A.Array {} -> A.Mobile t + _ -> t + | t <- ts] + newSpec = A.Protocol m'' ts' + modifyName n (\nd -> nd {A.ndSpecType = newSpec}) + scope' <- recurse scope + return $ A.Spec m (A.Specification m' n newSpec) scope' + + doStructured (A.Spec m (A.Specification m' n (A.ProtocolCase m'' nts)) scope) + = do let nts' = [(n, [case t of + A.Array {} -> A.Mobile t + _ -> t + | t <- ts]) | (n, ts) <- nts] + newSpec = A.ProtocolCase m'' nts' + modifyName n (\nd -> nd {A.ndSpecType = newSpec}) + scope' <- recurse scope + return $ A.Spec m (A.Specification m' n newSpec) scope' -- Must also mobilise channels of arrays, and arrays of channels of arrays: doStructured s@(A.Spec m (A.Specification m' n st) scope)