chp-spec-1.0.0: A mirror implementation of chp that generates a specification of the program



A module with support for things that are enrollable.

Enrollment is currently pretty much ignored during model generation, but these operations are provided so that you don't have to change your program.


data Enrolled b a Source


Eq (b a) => Eq (Enrolled b a) 
Typeable (b a) => Typeable (Enrolled b a) 

class Enrollable b z whereSource


enroll :: b z -> (Enrolled b z -> CHP a) -> CHP aSource

resign :: Enrolled b z -> CHP a -> CHP aSource


furtherEnroll :: Enrollable b z => Enrolled b z -> (Enrolled b z -> CHP a) -> CHP aSource

enrollPair :: (Enrollable b p, Enrollable b' p') => (b p, b' p') -> ((Enrolled b p, Enrolled b' p') -> CHP a) -> CHP aSource

enrollList :: Enrollable b p => [b p] -> ([Enrolled b p] -> CHP a) -> CHP aSource

enrollAll :: Enrollable b p => CHP (b p) -> [Enrolled b p -> CHP a] -> CHP [a]Source

enrollAll_ :: Enrollable b p => CHP (b p) -> [Enrolled b p -> CHP a] -> CHP ()Source

enrollAllT :: Enrollable b p => ([a] -> CHP c) -> CHP (b p) -> [Enrolled b p -> a] -> CHP cSource

enrollOneMany :: Enrollable b p => ([Enrolled b p] -> CHP a) -> [(CHP (b p), Enrolled b p -> CHP c)] -> CHP (a, [c])Source