Show
Ignore:
Timestamp:
05.01.2009 15:46:06 (11 months ago)
Author:
csliam
Message:

Large commit - improved static analysis of cspcasl and translation of cspcasl to isabelle

Files:
1 modified

Legend:

Unmodified
Added
Removed

  • trunk/CspCASL/StatAnaCSP.hs

    r11201 r11215  
    2121import qualified Data.Maybe as Maybe 
    2222import qualified Data.Set as S 
    23  
     23-- liam added the following, they should be deleted from imports when 
     24-- liams temp code is removed: Op_name mkSimpleId mkInfix OP_SYMB(..), 
     25-- OP_TYPE(..) 
    2426import CASL.AS_Basic_CASL (FORMULA(..), OpKind(..), SORT, TERM(..), VAR, 
    2527                           VAR_DECL(..)) 
    … …  
    3436import Common.ConvertGlobalAnnos 
    3537import qualified Common.Lib.Rel as Rel 
    36 import Common.Id (getRange, Id, simpleIdToId, nullRange, mkSimpleId) 
     38import Common.Id (getRange, Id, simpleIdToId, nullRange) 
    3739import Common.Lib.State 
    3840import Common.ExtSign 
    … …  
    4446import CspCASL.SignCSP 
    4547 
     48import qualified Data.Set as Set 
     49 
    4650basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) 
    4751        -> Result (CspBasicSpec, ExtSign CspCASLSign (), 
    48                    [Named CspCASLSentence]) 
    49 basicAnalysisCspCASL (cc, sigma, ga) = do 
     52                   [Named CspCASLSen]) 
     53basicAnalysisCspCASL (cc, sigma, ga) = 
    5054    let Result es mga = mergeGlobalAnnos ga $ globAnnos sigma 
    5155        (_, accSig) = runState (ana_BASIC_CSP cc) $ case mga of 
    … …  
    5357              Just nga -> sigma { globAnnos = nga } 
    5458        ds = reverse $ envDiags accSig 
    55     Result (es ++ ds) (Just ()) -- insert diagnostics 
    56     return (cc, mkExtSign accSig, [makeNamed "empty_sentence" emptyCCSentence, 
    57                                    makeNamed "StopProcSen"  stopProc, 
    58                                    makeNamed "GParProcSen"  gParProc, 
    59                                    makeNamed "AParProcSen"  aParProc, 
    60                                    makeNamed "StopProcSen"  seqProc]) 
    61     where 
    62       stopProc = CspCASLSentence (mkSimpleId "stopProc") [] (Stop nullRange) 
    63       seqProc = CspCASLSentence (mkSimpleId "seqProc") [] 
    64                                        (Sequential (Stop nullRange) 
    65                                         (Stop nullRange) nullRange) 
    66       gParProc = CspCASLSentence (mkSimpleId "gParProc") [] 
    67                                        (GeneralisedParallel (Stop nullRange) 
    68                                         (EventSet [mkSimpleId "S"] nullRange) 
    69                                         (Skip nullRange) nullRange) 
    70       aParProc = CspCASLSentence (mkSimpleId "gParProc") [] 
    71                                      (AlphabetisedParallel (Stop nullRange) 
    72                                       (EventSet [mkSimpleId "T"] nullRange) 
    73                                       (EventSet [mkSimpleId "U"] nullRange) 
    74                                       (Skip nullRange) nullRange) 
     59        -- Extract process equations only. 
     60        ext = extendedInfo accSig 
     61        ccsents = reverse $ ccSentences ext 
     62        -- Clean signature here 
     63        cleanSig = accSig 
     64                   { extendedInfo = ext { ccSentences = []}} 
     65    in Result (es ++ ds) $ 
     66      Just (cc, mkExtSign cleanSig, ccsents) 
    7567 
    7668ana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign () 
    … …  
    10294 
    10395-- | Statically analyse a CspCASL channel declaration. 
    104 anaChanDecl :: CHANNEL_DECL -> State CspCASLSign CHANNEL_DECL 
     96anaChanDecl :: CHANNEL_DECL -> State CspCASLSign () 
    10597anaChanDecl (ChannelDecl chanNames chanSort) = do 
    10698    checkSorts [chanSort] -- check channel sort is known 
    … …  
    113105            , envDiags = vds 
    114106            } 
    115     return (ChannelDecl chanNames chanSort) 
     107    return () 
    116108 
    117109-- | Statically analyse a CspCASL channel name. 
    … …  
    178170    sig <- get 
    179171    let ext = extendedInfo sig 
     172        ccsens = ccSentences ext 
    180173        procDecls = procSet ext 
    181174        prof = pn `Map.lookup` procDecls 
    182175    case prof of 
    183       -- Only analyse a process if its name (and thus profile) is known 
    184       Just (ProcProfile procArgs procAlpha) -> 
    185         do gVars <- anaProcVars pn procArgs vs -- compute global vars 
    186            termAlpha <- anaProcTerm proc gVars Map.empty 
    187            checkCommAlphaSub termAlpha procAlpha proc "process equation" 
    188            return () 
    189       Nothing -> 
    190         do addDiags [mkDiag Error "process equation for unknown process" pn] 
    191            return () 
    192     vds <- gets envDiags 
    193     put sig { envDiags = vds } 
     176         -- Only analyse a process if its name (and thus profile) is known 
     177         Just (ProcProfile procArgs procAlpha) -> 
     178             do  gVars <- anaProcVars pn procArgs vs -- compute global vars 
     179                 (termAlpha, fqProc) <- anaProcTerm proc (Map.fromList gVars) Map.empty 
     180                 checkCommAlphaSub termAlpha procAlpha proc "process equation" 
     181                 -- Save the diags from the checkCommAlphaSub 
     182                 vds <- gets envDiags 
     183                 -- put CspCASL Sentences back in to the state with new sentence 
     184                 put sig {envDiags = vds, extendedInfo = 
     185                          ext { ccSentences = 
     186                                -- BUG - What should the constituent 
     187                                -- alphabet be for this process? 
     188                                -- probably the same as the inner one! 
     189                                (makeNamed ("ProcHugo") 
     190                                               (ProcessEq pn gVars 
     191                                                          Set.empty 
     192                                                          fqProc)):ccsens 
     193                              } 
     194                         } 
     195                 return () 
     196         Nothing -> 
     197             do addDiags [mkDiag Error "process equation for unknown process" pn] 
     198                return () 
    194199    return () 
    195200 
    196201-- | Statically analyse a CspCASL process equation's global variable 
    197202-- names. 
    198 anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarMap 
     203anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList 
    199204anaProcVars pn ss vs = do 
    200205    case (compare (length ss) (length vs)) of 
    201206       LT -> do addDiags [mkDiag Error "too many process arguments" pn] 
    202                 return Map.empty 
     207                return [] 
    203208       GT -> do addDiags [mkDiag Error "not enough process arguments" pn] 
    204                 return Map.empty 
    205        EQ -> Monad.foldM anaProcVar Map.empty (zip vs ss) 
     209                return [] 
     210       EQ -> Monad.foldM anaProcVar [] (zip vs ss) 
    206211 
    207212-- | Statically analyse a CspCASL process-global variable name. 
    208 anaProcVar :: ProcVarMap -> (VAR, SORT) -> State CspCASLSign ProcVarMap 
     213anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList 
    209214anaProcVar old (v, s) = do 
    210     if v `Map.member` old 
    211        then do addDiags [mkDiag Error "process arg declared more than once" v] 
     215    if v `elem` (map fst old) 
     216       then do addDiags [mkDiag Error "process argument declared more than once" v] 
    212217               return old 
    213        else return (Map.insert v s old) 
     218       else return (old ++ [(v, s)]) 
    214219 
    215220-- Static analysis of process terms 
    216221 
     222-- BUG in fucntion below 
     223-- not returing FQProcesses 
    217224-- | Statically analyse a CspCASL process term. 
     225--   The process that is returned is a fully qualified process. 
    218226anaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap -> 
    219                State CspCASLSign CommAlpha 
     227               State CspCASLSign (CommAlpha, PROCESS) 
    220228anaProcTerm proc gVars lVars = case proc of 
    221     NamedProcess name args _ -> 
     229    NamedProcess name args range -> 
    222230        do addDiags [mkDiag Debug "Named process" proc] 
    223231           al <- anaNamedProc proc name args (lVars `Map.union` gVars) 
    224            return al 
    225     Skip _ -> 
     232           return (al, 
     233                   FQProcess (NamedProcess name args range) al range) 
     234    Skip range -> 
    226235        do addDiags [mkDiag Debug "Skip" proc] 
    227            return S.empty 
    228     Stop _ -> 
     236           return (S.empty, 
     237                   FQProcess (Skip range) S.empty range) 
     238    Stop range -> 
    229239        do addDiags [mkDiag Debug "Stop" proc] 
    230            return S.empty 
    231     Div _ -> 
     240           return (S.empty, 
     241                   FQProcess (Stop range) S.empty range) 
     242    Div range -> 
    232243        do addDiags [mkDiag Debug "Div" proc] 
    233            return S.empty 
    234     Run es _ -> 
     244           return (S.empty, 
     245                   FQProcess (Div range) S.empty range) 
     246    Run es range -> 
    235247        do addDiags [mkDiag Debug "Run" proc] 
    236248           comms <- anaEventSet es 
    237            return comms 
    238     Chaos es _ -> 
     249           return (comms, 
     250                   FQProcess (Run es range) comms range) 
     251    Chaos es range -> 
    239252        do addDiags [mkDiag Debug "Chaos" proc] 
    240253           comms <- anaEventSet es 
    241            return comms 
    242     PrefixProcess e p _ -> 
     254           return (comms, 
     255                   FQProcess (Chaos es range) comms range) 
     256    PrefixProcess e p range -> 
    243257        do addDiags [mkDiag Debug "Prefix" proc] 
    244258           (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars) 
    245            comms <- anaProcTerm p gVars (rcvMap `Map.union` lVars) 
    246            return (comms `S.union` evComms) 
    247     InternalPrefixProcess v s p _ -> 
     259           (comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `Map.union` lVars) 
     260           return (comms `S.union` evComms, 
     261                   FQProcess (PrefixProcess e pFQTerm range) (comms `S.union` evComms) range) 
     262    InternalPrefixProcess v s p range -> 
    248263        do addDiags [mkDiag Debug "Internal prefix" proc] 
    249264           checkSorts [s] -- check sort is known 
    250            comms <- anaProcTerm p gVars (Map.insert v s lVars) 
    251            return (S.insert (CommTypeSort s) comms) 
    252     ExternalPrefixProcess v s p _ -> 
     265           (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) 
     266           return (S.insert (CommTypeSort s) comms, 
     267                   FQProcess (InternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) 
     268    ExternalPrefixProcess v s p range -> 
    253269        do addDiags [mkDiag Debug "External prefix" proc] 
    254270           checkSorts [s] -- check sort is known 
    255            comms <- anaProcTerm p gVars (Map.insert v s lVars) 
    256            return (S.insert (CommTypeSort s) comms) 
    257     Sequential p q _ -> 
     271           (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) 
     272           return (S.insert (CommTypeSort s) comms, 
     273                   FQProcess (ExternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) 
     274    Sequential p q range -> 
    258275        do addDiags [mkDiag Debug "Sequential" proc] 
    259            pComms <- anaProcTerm p gVars lVars 
    260            qComms <- anaProcTerm q gVars Map.empty 
    261            return (pComms `S.union` qComms) 
    262     InternalChoice p q _ -> 
     276           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
     277           (qComms, qFQTerm) <- anaProcTerm q gVars Map.empty 
     278           return (pComms `S.union` qComms, 
     279                   FQProcess (Sequential pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 
     280    InternalChoice p q range -> 
    263281        do addDiags [mkDiag Debug "InternalChoice" proc] 
    264            pComms <- anaProcTerm p gVars lVars 
    265            qComms <- anaProcTerm q gVars lVars 
    266            return (pComms `S.union` qComms) 
    267     ExternalChoice p q _ -> 
     282           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
     283           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
     284           return (pComms `S.union` qComms, 
     285                   FQProcess (InternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 
     286    ExternalChoice p q range -> 
    268287        do addDiags [mkDiag Debug "ExternalChoice" proc] 
    269            pComms <- anaProcTerm p gVars lVars 
    270            qComms <- anaProcTerm q gVars lVars 
    271            return (pComms `S.union` qComms) 
    272     Interleaving p q _ -> 
     288           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
     289           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
     290           return (pComms `S.union` qComms, 
     291                   FQProcess (ExternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 
     292    Interleaving p q range -> 
    273293        do addDiags [mkDiag Debug "Interleaving" proc] 
    274            pComms <- anaProcTerm p gVars lVars 
    275            qComms <- anaProcTerm q gVars lVars 
    276            return (pComms `S.union` qComms) 
    277     SynchronousParallel p q _ -> 
     294           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
     295           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
     296           return (pComms `S.union` qComms, 
     297                   FQProcess (Interleaving pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 
     298    SynchronousParallel p q range -> 
    278299        do addDiags [mkDiag Debug "Synchronous" proc] 
    279            pComms <- anaProcTerm p gVars lVars 
    280            qComms <- anaProcTerm q gVars lVars 
    281            return (pComms `S.union` qComms) 
    282     GeneralisedParallel p es q _ -> 
     300           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
     301           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
     302           return (pComms `S.union` qComms, 
     303                   FQProcess (SynchronousParallel pFQTerm qFQTerm range) (pComms `S.union` qComms) range) 
     304    GeneralisedParallel p es q range -> 
    283305        do addDiags [mkDiag Debug "Generalised parallel" proc] 
    284            pComms <- anaProcTerm p gVars lVars 
     306           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
    285307           synComms <- anaEventSet es 
    286            qComms <- anaProcTerm q gVars lVars 
    287            return (S.unions [pComms, qComms, synComms]) 
    288     AlphabetisedParallel p esp esq q _ -> 
     308           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
     309           return (S.unions [pComms, qComms, synComms], 
     310                   FQProcess (GeneralisedParallel pFQTerm es qFQTerm range) (S.unions [pComms, qComms, synComms]) range) 
     311    AlphabetisedParallel p esp esq q range -> 
    289312        do addDiags [mkDiag Debug "Alphabetised parallel" proc] 
    290            pComms <- anaProcTerm p gVars lVars 
     313           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
    291314           pSynComms <- anaEventSet esp 
    292315           checkCommAlphaSub pSynComms pComms proc 
    293316                                 "alphabetised parallel, left" 
    294317           qSynComms <- anaEventSet esq 
    295            qComms <- anaProcTerm q gVars lVars 
     318           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
    296319           checkCommAlphaSub qSynComms qComms proc 
    297320                                 "alphabetised parallel, right" 
    298            return (pComms `S.union` qComms) 
    299     Hiding p es _ -> 
     321           return (pComms `S.union` qComms, 
     322                   FQProcess (AlphabetisedParallel pFQTerm esp esq qFQTerm range) (pComms `S.union` qComms) range) 
     323    Hiding p es range -> 
    300324        do addDiags [mkDiag Debug "Hiding" proc] 
    301            pComms <- anaProcTerm p gVars lVars 
     325           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
    302326           hidComms <- anaEventSet es 
    303            return (pComms `S.union` hidComms) 
    304     RenamingProcess p r _ -> 
     327           return (pComms `S.union` hidComms, 
     328                   FQProcess (Hiding pFQTerm es range) (pComms `S.union` hidComms) range) 
     329    RenamingProcess p r range -> 
    305330        do addDiags [mkDiag Debug "Renaming" proc] 
    306            pComms <- anaProcTerm p gVars lVars 
     331           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
    307332           renAlpha <- anaRenaming r 
    308            return (pComms `S.union` renAlpha) 
    309     ConditionalProcess f p q _ -> 
     333           return (pComms `S.union` renAlpha, 
     334                   FQProcess (RenamingProcess pFQTerm r range) (pComms `S.union` renAlpha) range) 
     335    ConditionalProcess f p q range -> 
    310336        do addDiags [mkDiag Debug "Conditional" proc] 
    311            pComms <- anaProcTerm p gVars lVars 
    312            qComms <- anaProcTerm q gVars lVars 
     337           (pComms, pFQTerm) <- anaProcTerm p gVars lVars 
     338           (qComms, qFQTerm) <- anaProcTerm q gVars lVars 
     339           -- mfs is the fully qualified formula version of f 
    313340           mfs <- anaFormulaCspCASL (gVars `Map.union` lVars) f 
     341           addDiags [mkDiag Debug "Formula" f] 
     342           addDiags [mkDiag Debug "FQFormula" (Maybe.fromJust mfs)] 
    314343           let fComms = case mfs of 
    315344                          Nothing -> S.empty 
    316345                          Just fs -> formulaComms fs 
    317            return (S.unions [pComms, qComms, fComms]) 
     346           return (S.unions [pComms, qComms, fComms], 
     347                   FQProcess (ConditionalProcess (Maybe.fromJust mfs) pFQTerm qFQTerm range) 
     348                                 (S.unions [pComms, qComms, fComms]) range) 
    318349 
    319350-- | Statically analyse a CspCASL "named process" term. 
    … …  
    582613        ga = globAnnos sig 
    583614        mix = emptyMix { mixRules = makeRules ga allIds } 
    584     resF <- resolveFormula (putParen mix) (mixResolve mix) 
    585                  ga (mixRules mix) frm 
     615    resF <- resolveFormula (putParen mix) (mixResolve mix) ga (mixRules mix) frm 
    586616    minExpFORMULA (const return) sig resF 
    587617