diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,8 +1,18 @@ +2016-06-22 John D. Ramsdell + + * cpsa.cabal (Extension): Add allow ambiguous types when compiling + with GHC 8.0.0 or later. + +2016-06-21 Moses D. Liskov + + * src/CPSA/DiffieHellman/Algebra.hs: Added code to implement the + "tag" sort, which quoted string tags belong to. + 2016-06-03 Moses D. Liskov * doc/examples/IKE_variants.tar.gz: Added this compressed archive of IKEv1 and IKEv2 variant input files. - + 2016-03-30 John D. Ramsdell * src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that @@ -222,4 +232,3 @@ 2013-02-06 John D. Ramsdell * cpet.cabal (Version): Tagged as 0.0.0. - diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -2,6 +2,12 @@ June, 2016: +* New feature: tag sort. Introduced a new sort "tag" in both the basic and + diffie-hellman algebras. Quoted string constants are now considered to be + of this sort rather than of least sort mesg. This allows a user to specify + a variable that may stand for a string constant, without forcing the user to + use a variable of the mesg sort for that purpose. + * New feature: depth limit. When a depth limit is specified, analysis of skeletons will proceed as long as the skeleton's depth in the search tree is below the limit. Skeletons not analyzed are marked as "(fringe)" to diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 3.3.1 +Version: 3.3.2 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -98,9 +98,11 @@ Executable cpsa Main-Is: CPSA/Lib/Main.hs - Build-Depends: base >= 3 && < 5, containers, parallel, array + Build-Depends: base >= 3 && < 5, containers, parallel GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Vector CPSA.Lib.Utilities CPSA.Lib.Debug @@ -118,6 +120,8 @@ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr @@ -134,6 +138,8 @@ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr @@ -147,6 +153,8 @@ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr @@ -162,6 +170,8 @@ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr @@ -175,6 +185,8 @@ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr @@ -198,6 +210,8 @@ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports + if impl(ghc >= 8.0.0) + Extensions: AllowAmbiguousTypes Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr diff --git a/doc/cpsamanual.pdf b/doc/cpsamanual.pdf Binary files a/doc/cpsamanual.pdf and b/doc/cpsamanual.pdf differ diff --git a/src/CPSA/Annotations/Annotations.hs b/src/CPSA/Annotations/Annotations.hs --- a/src/CPSA/Annotations/Annotations.hs +++ b/src/CPSA/Annotations/Annotations.hs @@ -246,8 +246,7 @@ return (gen', Instance { pos = pos, role = Just r, env = env, height = height }) -lookupRole :: (Algebra t p g s e c, Monad m) => Pos -> - Prot t g -> String -> m (Role t) +lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t) lookupRole pos prot role = case L.find (\r -> role == rname r) (roles prot) of Nothing -> @@ -426,8 +425,7 @@ successors strands = [((s, p), (s, p + 1)) | (s, n) <- zip [0..] strands, p <- nats (n - 1)] -before :: (Algebra t p g s e c, Monad m) => Pos -> - Preskel t g e -> m [(Node, [Node])] +before :: Monad m => Pos -> Preskel t g e -> m [(Node, [Node])] before pos k = case isAcyclic graph nodes of False -> fail (shows pos "Cycle found") diff --git a/src/CPSA/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs --- a/src/CPSA/DiffieHellman/Algebra.hs +++ b/src/CPSA/DiffieHellman/Algebra.hs @@ -22,7 +22,7 @@ -- The Diffie-Hellman Order-Sorted Signature is --- Sorts: mesg, text, data, name, skey, akey, +-- Sorts: mesg, text, data, name, skey, akey, tag, -- string, base, expr, and expn -- -- Subsorts: text, data, name, skey, akey, @@ -339,6 +339,7 @@ | Name -- Principal atom | Skey -- Symmetric key atom | Base -- Base of an exponentiated atom + | Tag -- Tag atom | Ltk -- Long term shared symmetric key | Bltk -- Bidirectional ltk | Akey -- Asymmetric key atom @@ -426,6 +427,7 @@ forceVar (F Text y) = (F Text y) forceVar (F Data y) = (F Data y) forceVar (F Name y) = (F Name y) +forceVar (F Tag [(I x)]) = (F Tag [(I x)]) forceVar (F Skey [(I x)]) = (F Skey [(I x)]) forceVar (F Skey [(F Ltk ns@(_:_))]) = forceVar (head ns) forceVar (F Skey [(F Bltk ns@(_:_))]) = forceVar (head ns) @@ -539,7 +541,8 @@ isVar (I _) = True -- Sort: mesg isVar (F s [I _]) = -- Sorts: text, data, name, skey, and akey - s == Text || s == Data || s == Name || s == Skey || s == Akey || s == Base + s == Text || s == Data || s == Name || s == Skey || + s == Akey || s == Base || s == Tag isVar (G t) = isGroupVar t isVar _ = False @@ -557,6 +560,7 @@ varId (F Skey [I x]) = x varId (F Akey [I x]) = x varId (F Base [I x]) = x +varId (F Tag [I x]) = x varId (G t) | isGroupVar t = getGroupVar t varId (D x) = x varId _ = C.assertError "Algebra.varId: term not a variable with its sort" @@ -603,6 +607,8 @@ extendVarEnv xts x t -- Name variable termWellFormed xts t@(F Skey [I x]) = extendVarEnv xts x t -- Symmetric key variable +termWellFormed xts t@(F Tag [I x]) = + extendVarEnv xts x t -- Tag variable termWellFormed xts (F Skey [F Ltk [I x, I y]]) = -- Long term shared symmetric key doubleTermWellFormed xts (F Name [I x]) (F Name [I y]) @@ -635,7 +641,7 @@ where expnVarEnv xts (x, (be, _)) = extendVarEnv xts x (groupVar be x) -termWellFormed xts (C _) = +termWellFormed xts (F Tag [(C _)]) = Just xts -- Tags termWellFormed xts (F Cat [t0, t1]) = doubleTermWellFormed xts t0 t1 -- Concatenation @@ -661,9 +667,9 @@ -- Is the sort of the term a base sort? isAtom :: Term -> Bool isAtom (I _) = False -isAtom (C _) = False +isAtom (C _) = True isAtom (F s _) = - s == Text || s == Data || s == Name || s == Skey || s == Akey + s == Text || s == Data || s == Name || s == Skey || s == Akey || s == Tag isAtom (G x) = isBasisVar x isAtom (D _) = False isAtom (P _) = False @@ -696,6 +702,7 @@ foldVars :: (a -> Term -> a) -> a -> Term -> a foldVars f acc t@(I _) = f acc t -- Mesg variable foldVars f acc t@(F Text [I _]) = f acc t -- Text variable +foldVars f acc t@(F Tag [I _]) = f acc t -- Tag variable foldVars f acc t@(F Data [I _]) = f acc t -- Data variable foldVars f acc t@(F Name [I _]) = f acc t -- Name variable foldVars f acc t@(F Skey [I _]) = @@ -727,7 +734,7 @@ where expnAddVars acc x (be, _) = f acc (groupVar be x) -foldVars _ acc (C _) = acc -- Tags +foldVars _ acc (F Tag [(C _)]) = acc -- Tags foldVars f acc (F Cat [t0, t1]) = -- Concatenation foldVars f (foldVars f acc t0) t1 foldVars f acc (F Enc [t0, t1]) = -- Encryption @@ -783,8 +790,7 @@ ba term where ba (I _) = True -- A mesg sorted variable is always buildable --- ba (F Genr _) = True -- as is the generator - ba (C _) = True -- So is a tag +-- ba (C _) = True -- Tags are now atoms. ba (F Cat [t0, t1]) = ba t0 && ba t1 ba t@(F Enc [t0, t1]) = @@ -2075,6 +2081,8 @@ | x == y = (F Akey [I x], F Akey [t]) loop (F Base [I x] : _) (y, t) | x == y = (F Base [I x], F Base [t]) + loop (F Tag [I x] : _) (y, t) + | x == y = (F Tag [I x], F Tag [t]) loop (G x : _) (y, G t) | isGroupVar x && varId (G x) == y = (G x, G t) loop (D x : _) (y, t) @@ -2192,6 +2200,7 @@ "skey" -> return $ F Skey [t] "akey" -> return $ F Akey [t] "base" -> return $ F Base [t] + "tag" -> return $ F Tag [t] "expr" -> return $ groupVar False x "expn" -> return $ groupVar True x "node" -> return (D x) @@ -2227,7 +2236,7 @@ loadTerm vars strict (S pos s) = either fail return (loadLookup pos vars strict s) loadTerm _ _ (Q _ t) = - return (C t) + return (F Tag [(C t)]) loadTerm vars strict (L pos (S _ s : l)) = case lookup s loadDispatch of Nothing -> fail (shows pos "Keyword " ++ s ++ " unknown") @@ -2415,6 +2424,7 @@ displayVar ctx (F Skey [I x]) = displaySortId "skey" ctx x displayVar ctx (F Akey [I x]) = displaySortId "akey" ctx x displayVar ctx (F Base [I x]) = displaySortId "base" ctx x +displayVar ctx (F Tag [I x]) = displaySortId "tag" ctx x displayVar ctx t@(G x) | isBasisVar x = displaySortId "expn" ctx (varId t) | isGroupVar x = displaySortId "expr" ctx (varId t) @@ -2454,6 +2464,7 @@ F Invk [F Pubk [C c, I x]] -> L () [S () "privk", Q () c, displayId ctx x] _ -> error ("Algebra.displayAkey: Bad term " ++ show t) +displayTerm ctx (F Tag [I x]) = displayId ctx x displayTerm ctx (F Base [t]) = displayBase t where @@ -2475,6 +2486,7 @@ displayFactor (x, (_, n)) | n >= 0 = displayId ctx x | otherwise = L () [S () "rec", displayId ctx x] +displayTerm _ (F Tag [(C t)]) = Q () t displayTerm _ (C t) = Q () t displayTerm ctx (F Cat [t0, t1]) = L () (S () "cat" : displayTerm ctx t0 : displayList ctx t1) diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs --- a/src/CPSA/Lib/Cohort.hs +++ b/src/CPSA/Lib/Cohort.hs @@ -196,8 +196,7 @@ if visitOldStrandsFirst mode then (compare s0 s1) else (compare s1 s0) -compareNodeOrder :: Algebra t p g s e c => Mode -> Strand t e -> - Int -> Int -> Ordering +compareNodeOrder :: Mode -> Strand t e -> Int -> Int -> Ordering compareNodeOrder mode s i0 i1 = if (reverseNodeOrder mode == rsearch (role $ inst s)) then (compare i0 i1) else (compare i1 i0) diff --git a/src/CPSA/Lib/Declaration.hs b/src/CPSA/Lib/Declaration.hs --- a/src/CPSA/Lib/Declaration.hs +++ b/src/CPSA/Lib/Declaration.hs @@ -138,45 +138,39 @@ Declarations t l mkDecls dl = declsNub Declarations { dlist = dl } -dnon :: (Algebra t p g s e c, Loc l) => Declarations t l -> - DeclInstList t l +dnon :: Declarations t l -> DeclInstList t l dnon decls = tagDecls "non-orig" decls -dpnon :: (Algebra t p g s e c, Loc l) => Declarations t l -> - DeclInstList t l +dpnon :: Declarations t l -> DeclInstList t l dpnon decls = tagDecls "pen-non-orig" decls -dunique :: (Algebra t p g s e c, Loc l) => Declarations t l -> - DeclInstList t l +dunique :: Declarations t l -> DeclInstList t l dunique decls = tagDecls "uniq-orig" decls -duniqgen :: (Algebra t p g s e c, Loc l) => Declarations t l -> - DeclInstList t l +duniqgen :: Declarations t l -> DeclInstList t l duniqgen decls = tagDecls "uniq-gen" decls -- Exported -dknon :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t] +dknon :: Declarations t l -> [t] dknon d = map head $ map dterms (dnon d) -- Exported -dkpnon :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t] +dkpnon :: Declarations t l -> [t] dkpnon d = map head $ map dterms (dpnon d) -- Exported -dkunique :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t] +dkunique :: Declarations t l -> [t] dkunique d = map head $ map dterms (dunique d) -dkuniqgen :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t] +dkuniqgen :: Declarations t l -> [t] dkuniqgen d = map head $ map dterms (duniqgen d) -- Exported -dkuniqFull :: (Algebra t p g s e c, Loc l) => Declarations t l -> - [(t,l)] +dkuniqFull :: Declarations t l -> [(t,l)] dkuniqFull d = map (\x -> (head $ dterms x, head $ dlocs x)) (dunique d) -- Exported -dkugenFull :: (Algebra t p g s e c, Loc l) => Declarations t l -> - [(t, Maybe l)] +dkugenFull :: Declarations t l -> [(t, Maybe l)] dkugenFull d = map (\x -> foo x) (duniqgen d) where foo x @@ -247,19 +241,17 @@ -- Exported -- Classifies the declaration tags used in the given Declarations according to format. -declarationTags :: (Algebra t p g s e c, Loc l) => Declarations t l -> - [(String, (DeclOutFormat, Bool))] +declarationTags :: Declarations t l -> [(String, (DeclOutFormat, Bool))] declarationTags d = nub $ declarationTagsCore d declFormats -- Exported -declarationRoleTags :: (Algebra t p g s e c, Loc l) => Declarations t l -> - [(String, (DeclOutFormat, Bool))] +declarationRoleTags :: Declarations t l -> [(String, (DeclOutFormat, Bool))] declarationRoleTags d = nub $ declarationTagsCore d declRFormats -- Common code for declarationRoleTags and declarationTags. -- Looks up the format associated each declaration and pairs the tag with its format. -- Since subtags are subsequent words in the tag string, we look up by the first word. -declarationTagsCore :: (Algebra t p g s e c, Loc l) => Declarations t l -> +declarationTagsCore :: Declarations t l -> [(String, (Int, Int))] -> [(String, (DeclOutFormat, Bool))] declarationTagsCore d fmts = map (\ tag -> (tag, declOutputFormats !! (getOutFormat tag))) dtags @@ -270,18 +262,15 @@ Just (_,out) -> out -- Exported -tagDeclsTermsOnly :: (Algebra t p g s e c, Loc l) => String -> - Declarations t l -> [t] +tagDeclsTermsOnly :: String -> Declarations t l -> [t] tagDeclsTermsOnly tag decls = map head $ map dterms $ tagDecls tag decls -- Exported -tagDeclsLocsOnly :: (Algebra t p g s e c, Loc l) => String -> - Declarations t l -> [l] +tagDeclsLocsOnly :: String -> Declarations t l -> [l] tagDeclsLocsOnly tag decls = map head $ map dlocs $ tagDecls tag decls -- Exported -tagDecls :: (Algebra t p g s e c, Loc l) => String -> Declarations t l -> - DeclInstList t l +tagDecls :: String -> Declarations t l -> DeclInstList t l tagDecls tag decls = case lookup tag (dlist decls) of Nothing -> [] @@ -325,7 +314,7 @@ g dinst = declInstAux (map f $ dterms dinst) (dlocs dinst) (daux dinst) -- Exported -declsMapLocations :: (Algebra t p g s e c, Loc l, Loc l') => (l -> l') -> +declsMapLocations :: (Algebra t p g s e c, Loc l') => (l -> l') -> Declarations t l -> Declarations t l' declsMapLocations f decls = mkDecls (map fdecls (dlist decls)) @@ -353,7 +342,7 @@ f dinst = declInstAux (map (instantiate env) $ dterms dinst) (map locmap $ dlocs dinst) (daux dinst) -avoidTerms :: (Algebra t p g s e c, Loc l) => Declarations t l -> Set t +avoidTerms :: Algebra t p g s e c => Declarations t l -> Set t avoidTerms decls = S.unions [ns, as, uos, ugs] where @@ -363,8 +352,7 @@ ugs = S.fromList (dkuniqgen decls) -------------------------- Constraint checking, where possible -------------- -declCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> - (Bool, String) +declCheck :: Algebra t p g s e c => Declarations t l -> (Bool, String) declCheck d = case doDeclCheck d of Return _ -> (True, "") @@ -377,10 +365,10 @@ failwith "subsort requirements violated" $ subsortCheck d failwith "[ASSERT FAILED] inst limit requirements violated" $ instlimitCheck d -instlimitCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool +instlimitCheck :: Declarations t l -> Bool instlimitCheck _ = True -neqCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool +neqCheck :: Algebra t p g s e c => Declarations t l -> Bool neqCheck decls = null failures where @@ -393,7 +381,7 @@ dts = map dterms ((tagDecls "neq" decls) ++ (tagDecls "neqlist" decls)) -ltCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool +ltCheck :: Algebra t p g s e c => Declarations t l -> Bool ltCheck decls = checkAll pairs pairs ((length pairs)-1) where @@ -405,7 +393,7 @@ evlv x y = [[(ts1 !! 0),(ts2 !! 1)]| ts1 <- y, ts2 <- x, ts1 !! 1 == ts2 !! 0] pairs = map dterms (tagDecls "lt" decls) -subsortCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool +subsortCheck :: Algebra t p g s e c => Declarations t l -> Bool subsortCheck decls = null failures where diff --git a/src/CPSA/Lib/Loader.hs b/src/CPSA/Lib/Loader.hs --- a/src/CPSA/Lib/Loader.hs +++ b/src/CPSA/Lib/Loader.hs @@ -571,8 +571,7 @@ (gen', env') <- foldM (loadMaplet kvars vars) (gen, emptyEnv) env return (mkInstance gen' r env' height) -lookupRole :: (Algebra t p g s e c, Monad m) => Pos -> - Prot t g -> String -> m (Role t) +lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t) lookupRole _ p role | role == "" = return $ listenerRole p lookupRole pos p role = diff --git a/src/CPSA/Lib/Main.hs b/src/CPSA/Lib/Main.hs --- a/src/CPSA/Lib/Main.hs +++ b/src/CPSA/Lib/Main.hs @@ -105,6 +105,21 @@ | otherwise -> abort ("Bad algebra: " ++ name) +{-- +-- name the algebra and go. +select :: [String] -> Maybe (SExpr Pos) -> Options -> [SExpr Pos] -> IO () +select files herald opts sexprs = + case optAlg opts of + name | name == CPSA.Algebra.Basic.name -> + go name (CPSA.Algebra.Algebra.origin CPSA.Algebra.Basic.origin) + files herald opts sexprs + | name == CPSA.Algebra.DiffieHellman.name -> + go name (CPSA.Algebra.Algebra.origin CPSA.Algebra.DiffieHellman.origin) + files herald opts sexprs + | otherwise -> + abort ("Bad algebra: " ++ name) +--} + -- Load protocols and preskeletons and print run time information go :: Algebra t p g s e c => String -> g -> [String] -> Maybe (SExpr Pos) -> Options -> [SExpr Pos] -> IO () diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs --- a/src/CPSA/Lib/Reduction.hs +++ b/src/CPSA/Lib/Reduction.hs @@ -42,8 +42,7 @@ parent :: Maybe (LPreskel t g s e) } deriving Show -withParent :: Algebra t p g s e c => Preskel t g s e -> - Int -> LPreskel t g s e -> LPreskel t g s e +withParent :: Preskel t g s e -> Int -> LPreskel t g s e -> LPreskel t g s e withParent k label parent = LPreskel k label (1 + depth parent) (Just parent) @@ -65,26 +64,24 @@ newtype Seen t g s e = Seen [IPreskel t g s e] -- Create a singleton seen history -hist :: Algebra t p g s e c => IPreskel t g s e -> Seen t g s e +hist :: IPreskel t g s e -> Seen t g s e hist ik = Seen [ik] -- Add an element to the seen history. -remember :: Algebra t p g s e c => IPreskel t g s e -> - Seen t g s e -> Seen t g s e +remember :: IPreskel t g s e -> Seen t g s e -> Seen t g s e remember ik (Seen seen) = Seen (ik : seen) -- Find an element of the seen history that satisfies a predicate. -recall :: Algebra t p g s e c => (IPreskel t g s e -> Bool) -> +recall :: (IPreskel t g s e -> Bool) -> Seen t g s e -> Maybe (IPreskel t g s e) recall f (Seen seen) = L.find f seen -- Create an empty seen history -void :: Algebra t p g s e c => Seen t g s e +void :: Seen t g s e void = Seen [] -- Merge two seen histories. -merge :: Algebra t p g s e c => Seen t g s e -> - Seen t g s e -> Seen t g s e +merge :: Seen t g s e -> Seen t g s e -> Seen t g s e merge (Seen xs) (Seen ys) = Seen (xs ++ ys) -- Contains the result of applying the cohort reduction rule. The @@ -277,7 +274,7 @@ Nothing -> (kid : unseen, dups) -- Make a todo list for dump -mktodo :: Algebra t p g s e c => [Reduct t g s e] -> +mktodo :: [Reduct t g s e] -> [LPreskel t g s e] -> [LPreskel t g s e] -> [LPreskel t g s e] mktodo reducts todo tobig = @@ -328,8 +325,7 @@ let (n', todo') = foldl (children lk) (n, []) ks' fast p h ks m n' (todo ++ reverse todo') -children :: Algebra t p g s e c => LPreskel t g s e -> - (Int, [LPreskel t g s e]) -> +children :: LPreskel t g s e -> (Int, [LPreskel t g s e]) -> Preskel t g s e -> (Int, [LPreskel t g s e]) children p (n, todo) k = -- Label a preskeleton here (n + 1, withParent k n p : todo) diff --git a/src/CPSA/Lib/State.hs b/src/CPSA/Lib/State.hs --- a/src/CPSA/Lib/State.hs +++ b/src/CPSA/Lib/State.hs @@ -17,14 +17,14 @@ -- label :: Tran t -> Maybe t -- label (Tran (_, _, t)) = t -observer :: Eq t => Tran t -> Bool +observer :: Tran t -> Bool observer (Tran (_, Nothing, _)) = True observer _ = False -path :: Eq t => Tran t -> Bool +path :: Tran t -> Bool path x = not (observer x) -transition :: Eq t => Tran t -> Bool +transition :: Tran t -> Bool transition (Tran (Just _, Just _, _)) = True transition _ = False diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -200,7 +200,7 @@ where g s (_, t) = foldVars (flip S.insert) s t -listenerTerm :: Algebra t p g s e c => Instance t e -> Maybe t +listenerTerm :: Instance t e -> Maybe t listenerTerm inst = case rname (role inst) of "" -> recvTerm (trace inst !! 0) -- Get first term in trace @@ -495,11 +495,10 @@ -- Strand functions -strandInst :: Algebra t p g s e c => Preskel t g s e -> - Sid -> Instance t e +strandInst :: Preskel t g s e -> Sid -> Instance t e strandInst k strand = insts k !! strand -nstrands :: Algebra t p g s e c => Preskel t g s e -> Int +nstrands :: Preskel t g s e -> Int nstrands k = length (strandids k) -- Convert the preskeleton made by the loader into the first skeleton @@ -559,8 +558,7 @@ error ("Strand.checkVars: role var in skel " ++ show k) | otherwise = k -vertex :: Algebra t p g s e c => Preskel t g s e -> Node -> - Vertex t e +vertex :: Preskel t g s e -> Node -> Vertex t e vertex k (s, i) = nodes (strands k !! s) !! i @@ -579,11 +577,11 @@ p <- M.maybeToList $ generationPos u (trace (inst strand)) ]) -- Do the nodes in the orderings have the right direction? -wellOrdered :: Algebra t p g s e c => Preskel t g s e -> Bool +wellOrdered :: Preskel t g s e -> Bool wellOrdered k = all pairWellOrdered (edges k) -pairWellOrdered :: Algebra t p g s e c => Edge t e -> Bool +pairWellOrdered :: Edge t e -> Bool pairWellOrdered (n0, n1) = case (event n0, event n1) of (Out _, In _) -> True @@ -593,11 +591,11 @@ _ -> False -- Do transitively reduced orderings have the right direction? -reducedWellOrdered :: Algebra t p g s e c => Preskel t g s e -> Bool +reducedWellOrdered :: Preskel t g s e -> Bool reducedWellOrdered k = all reducedPairWellOrdered (edges k) -reducedPairWellOrdered :: Algebra t p g s e c => Edge t e -> Bool +reducedPairWellOrdered :: Edge t e -> Bool reducedPairWellOrdered (n0, n1) = case (event n0, event n1) of (Out _, In _) -> True @@ -636,7 +634,7 @@ -- Use depth first search to detect cycles. A graph with no node with -- an indegree of zero is cyclic and must not be checked with depth -- first search. -acyclicOrder :: Algebra t p g s e c => Preskel t g s e -> Bool +acyclicOrder :: Preskel t g s e -> Bool acyclicOrder k = all (not . backEdge numbering) edges where @@ -828,7 +826,7 @@ s) -- Substition part of homomorphism -- Extract the protential cohort member from a PRS. -skel :: Algebra t p g s e c => PRS t p g s e c -> Preskel t g s e +skel :: PRS t p g s e c -> Preskel t g s e skel (_, k, _, _, _) = k -- Returns the preskeletons that result from applying a substitution. @@ -945,7 +943,7 @@ map (\ (n,i) -> (nodeMap mapping n, i)) kpriority -- Provide a list of nodes with non-default priorities -kpriorities :: Algebra t p g s e c => Preskel t g s e -> [(Node,Int)] +kpriorities :: Preskel t g s e -> [(Node,Int)] kpriorities k = [((s,i),priority k (s,i)) | s <- [0..(length (insts k) - 1)], i <- [0..(height ((insts k) !! s) -1)], @@ -958,7 +956,7 @@ In _ -> True Sync _ -> False -priority :: Algebra t p g s e c => Preskel t g s e -> Node -> Int +priority :: Preskel t g s e -> Node -> Int priority k (s,i) = case lookup (s,i) (kpriority k) of Just p -> p @@ -1089,8 +1087,7 @@ -- Ensure that if (s, p) precedes (s", p"), then (s', p) precedes (s", p") -- and if (s", p") precedes (s, p), then (s", p") precedes (s', p) -precedesCheck :: Algebra t p g s e c => Preskel t g s e -> - Sid -> Sid -> Edge t e -> Bool +precedesCheck :: Preskel t g s e -> Sid -> Sid -> Edge t e -> Bool precedesCheck k s s' (gn0, gn1) | s == sid (strand gn0) = graphPrecedes (vertex k (s', pos gn0)) gn1 | s == sid (strand gn1) = graphPrecedes gn0 (vertex k (s', pos gn1)) @@ -1360,7 +1357,7 @@ -- Answers for cohorts type Ans t p g s e c = (Preskel t g s e, Node, [Sid], s) -ans :: Algebra t p g s e c => PRS t p g s e c -> [Ans t p g s e c] +ans :: PRS t p g s e c -> [Ans t p g s e c] ans (_, k, n, phi, subst) = [(k, n, phi, subst)] -- Returns the skeleton associated with a preskeleton or nothing when @@ -1568,8 +1565,7 @@ type Candidate t p g s e c = (Preskel t g s e, [Sid]) -addIdentity :: Algebra t p g s e c => Preskel t g s e -> - Candidate t p g s e c +addIdentity :: Preskel t g s e -> Candidate t p g s e c addIdentity k = (k, strandids k) separateVariablesLimit :: Int @@ -1675,7 +1671,7 @@ (declsMapStrands mapping decls0) terms = iterms insts' -nodeInSkel :: Algebra t p g s e c => Preskel t g s e -> Node -> Bool +nodeInSkel :: Preskel t g s e -> Node -> Bool nodeInSkel k (s, i) = s >= 0 && s < nstrands k && i >= 0 && i < height (strandInst k s) @@ -1997,27 +1993,27 @@ deriving Show -- Exported -knon :: Algebra t p g s e c => Preskel t g s e -> [t] +knon :: Preskel t g s e -> [t] knon = dknon . decls -- Exported -kpnon :: Algebra t p g s e c => Preskel t g s e -> [t] +kpnon :: Preskel t g s e -> [t] kpnon = dkpnon . decls -- Exported -kunique :: Algebra t p g s e c => Preskel t g s e -> [t] +kunique :: Preskel t g s e -> [t] kunique = dkunique . decls -- Exported -korig :: Algebra t p g s e c => Preskel t g s e -> [(t, [Node])] +korig :: Preskel t g s e -> [(t, [Node])] korig = dkorig . cInfo -- Exported -kugen :: Algebra t p g s e c => Preskel t g s e -> [(t, [Node])] +kugen :: Preskel t g s e -> [(t, [Node])] kugen = dkugen . cInfo -- Exported -kuniqgen :: Algebra t p g s e c => Preskel t g s e -> [t] +kuniqgen :: Preskel t g s e -> [t] kuniqgen k = map head $ filter (\ts -> not $ null ts) $ map dterms $ tagDecls "uniq-gen" $ decls k {-- Exported @@ -2026,7 +2022,7 @@ --} -- Exported -nsdecls :: (Algebra t p g s e c, Loc l) => Declarations t l -> [Int] +nsdecls :: Declarations t l -> [Int] nsdecls decls = [length (dknon decls), length (dkpnon decls), length (dkunique decls)] @@ -2133,16 +2129,14 @@ (null ts) -- Do notation friendly preskeleton well formed check. -reducedWellFormed :: (Monad m, Algebra t p g s e c) => - Preskel t g s e -> m () +reducedWellFormed :: Monad m => Preskel t g s e -> m () reducedWellFormed k | reducedWellOrdered k = return () | otherwise = fail "reduced preskeleton not well formed" -- A transition or an observer node should have at most one transition -- node immediately after it. -noStateSplit :: (Monad m, Algebra t p g s e c) => - Preskel t g s e -> m () +noStateSplit :: Monad m => Preskel t g s e -> m () noStateSplit k | loop (leadsto k) S.empty = return () | otherwise = fail "reduced preskeleton has a state split" @@ -2307,7 +2301,7 @@ -- Determine if a given PRS has a multiple origination of a -- non-numeric fresh value. -hasMultipleOrig :: Algebra t p g s e c => PRS t p g s e c -> Bool +hasMultipleOrig :: PRS t p g s e c -> Bool hasMultipleOrig prs = any (\(_, l) -> length l > 1) (korig (skel prs)) || any (\(_, l) -> length l > 1) (kugen (skel prs)) @@ -2318,7 +2312,7 @@ declCheckOrigs (declsMapLocations (permuteNode perm) $ gdecls g) (gdecls g') env -- Exported -declsOrig :: (Algebra t p g s e c, Loc l) => [Strand t e] -> +declsOrig :: Algebra t p g s e c => [Strand t e] -> Declarations t l -> ConstInfo t declsOrig strands d = ConstInfo { dkorig = map (originationNodes strands) (dkunique d), @@ -2577,7 +2571,7 @@ t' <- dkuniqgen $ decls k match t t' e -inSkel :: Algebra t p g s e c => Preskel t g s e -> (Int, Int) -> Bool +inSkel :: Preskel t g s e -> (Int, Int) -> Bool inSkel k (s, i) = s >= 0 && s < nstrands k && i >= 0 && i < height (insts k !! s) diff --git a/src/CPSA/SAS/Main.hs b/src/CPSA/SAS/Main.hs --- a/src/CPSA/SAS/Main.hs +++ b/src/CPSA/SAS/Main.hs @@ -48,7 +48,7 @@ abort ("Bad algebra: " ++ alg) -- Continue and ignore header if one was found -next :: Algebra t p g s e c => PosHandle -> Handle -> Int -> +next :: PosHandle -> Handle -> Int -> Maybe (SExpr Pos) -> (State t g c -> Maybe (SExpr Pos) -> IO (State t g c)) -> IO () next p h margin Nothing f = -- Found header @@ -103,7 +103,7 @@ Left err -> abort (show err) -after :: Algebra t p g s e c => Handle -> Int -> State t g c -> +after :: Handle -> Int -> State t g c -> Maybe (SExpr Pos) -> IO (State t g c) after output margin state (Just sexpr@(L _ (S _ "defprotocol" : _))) = do diff --git a/src/CPSA/SAS/SAS.hs b/src/CPSA/SAS/SAS.hs --- a/src/CPSA/SAS/SAS.hs +++ b/src/CPSA/SAS/SAS.hs @@ -215,8 +215,7 @@ -- Find a protocol -findProt :: (Algebra t p g s e c, Monad m) => Pos -> - [Prot t g c] -> [SExpr Pos] -> m (Prot t g c) +findProt :: Monad m => Pos -> [Prot t g c] -> [SExpr Pos] -> m (Prot t g c) findProt pos ps (S _ name : _) = case L.find (\p -> name == pname p) ps of Nothing -> fail (shows pos $ "Protocol " ++ name ++ " unknown") @@ -317,8 +316,7 @@ return (Instance { pos = pos, role = r, env = env, height = height }) -lookupRole :: (Algebra t p g s e c, Monad m) => Pos -> - Prot t g c -> String -> m (Role t c) +lookupRole :: Monad m => Pos -> Prot t g c -> String -> m (Role t c) lookupRole pos prot role = case L.find (\r -> role == rname r) (roles prot) of Nothing -> @@ -461,8 +459,7 @@ -- Applies a strand permutation to a node. -- Hope the strand map is valid, or !! will blow up. -loadNodeEq :: Algebra t p g s e c => Preskel t g c -> - [Int] -> (Node, t) -> (t, t) +loadNodeEq :: Preskel t g c -> [Int] -> (Node, t) -> (t, t) loadNodeEq k perm ((s, i), v) = (v, nlookup (perm !! s, i) (varmap k))