chalmers-lava2000 1.5 → 1.5.1

raw patch · 4 files changed

+15/−4 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Lava.Error: instance Eq Error

- Lava.Error: instance Show Error

- Lava.Generic: delaySymbol :: Ops -> Symbol -> Symbol -> Symbol

- Lava.Generic: equalSymbol :: Ops -> Symbol -> Symbol -> Signal Bool

- Lava.Generic: ifSymbol :: Ops -> Signal Bool -> (Symbol, Symbol) -> Symbol

- Lava.Generic: instance (Choice a, Choice b) => Choice (a, b)

- Lava.Generic: instance (Choice a, Choice b, Choice c) => Choice (a, b, c)

- Lava.Generic: instance (Choice a, Choice b, Choice c, Choice d) => Choice (a, b, c, d)

- Lava.Generic: instance (Choice a, Choice b, Choice c, Choice d, Choice e) => Choice (a, b, c, d, e)

- Lava.Generic: instance (Choice a, Choice b, Choice c, Choice d, Choice e, Choice f) => Choice (a, b, c, d, e, f)

- Lava.Generic: instance (Choice a, Choice b, Choice c, Choice d, Choice e, Choice f, Choice g) => Choice (a, b, c, d, e, f, g)

- Lava.Generic: instance (Constructive a, Constructive b) => Constructive (a, b)

- Lava.Generic: instance (Constructive a, Constructive b, Constructive c) => Constructive (a, b, c)

- Lava.Generic: instance (Constructive a, Constructive b, Constructive c, Constructive d) => Constructive (a, b, c, d)

- Lava.Generic: instance (Constructive a, Constructive b, Constructive c, Constructive d, Constructive e) => Constructive (a, b, c, d, e)

- Lava.Generic: instance (Constructive a, Constructive b, Constructive c, Constructive d, Constructive e, Constructive f) => Constructive (a, b, c, d, e, f)

- Lava.Generic: instance (Constructive a, Constructive b, Constructive c, Constructive d, Constructive e, Constructive f, Constructive g) => Constructive (a, b, c, d, e, f, g)

- Lava.Generic: instance (Finite a, Finite b) => Finite (a, b)

- Lava.Generic: instance (Finite a, Finite b, Finite c) => Finite (a, b, c)

- Lava.Generic: instance (Finite a, Finite b, Finite c, Finite d) => Finite (a, b, c, d)

- Lava.Generic: instance (Finite a, Finite b, Finite c, Finite d, Finite e) => Finite (a, b, c, d, e)

- Lava.Generic: instance (Finite a, Finite b, Finite c, Finite d, Finite e, Finite f) => Finite (a, b, c, d, e, f)

- Lava.Generic: instance (Finite a, Finite b, Finite c, Finite d, Finite e, Finite f, Finite g) => Finite (a, b, c, d, e, f, g)

- Lava.Generic: instance (Generic a, Generic b) => Generic (a, b)

- Lava.Generic: instance (Generic a, Generic b, Generic c) => Generic (a, b, c)

- Lava.Generic: instance (Generic a, Generic b, Generic c, Generic d) => Generic (a, b, c, d)

- Lava.Generic: instance (Generic a, Generic b, Generic c, Generic d, Generic e) => Generic (a, b, c, d, e)

- Lava.Generic: instance (Generic a, Generic b, Generic c, Generic d, Generic e, Generic f) => Generic (a, b, c, d, e, f)

- Lava.Generic: instance (Generic a, Generic b, Generic c, Generic d, Generic e, Generic f, Generic g) => Generic (a, b, c, d, e, f, g)

- Lava.Generic: instance Choice ()

- Lava.Generic: instance Choice (Signal a)

- Lava.Generic: instance Choice Symbol

- Lava.Generic: instance Choice a => Choice [a]

- Lava.Generic: instance Choice b => Choice (a -> b)

- Lava.Generic: instance Constructive ()

- Lava.Generic: instance ConstructiveSig Bool

- Lava.Generic: instance ConstructiveSig Int

- Lava.Generic: instance ConstructiveSig a => Constructive (Signal a)

- Lava.Generic: instance Eq a => Eq (Struct a)

- Lava.Generic: instance Finite ()

- Lava.Generic: instance FiniteSig Bool

- Lava.Generic: instance FiniteSig a => Finite (Signal a)

- Lava.Generic: instance Functor Struct

- Lava.Generic: instance Generic ()

- Lava.Generic: instance Generic (Signal a)

- Lava.Generic: instance Generic Symbol

- Lava.Generic: instance Generic a => Generic [a]

- Lava.Generic: instance Sequent Struct

- Lava.Generic: instance Show a => Show (Struct a)

- Lava.Generic: varSymbol :: Ops -> String -> Symbol

- Lava.Generic: zeroSymbol :: Ops -> Symbol

- Lava.Isc: instance Functor Sign

- Lava.Isc: instance Read a => Read (Sign a)

- Lava.Isc: instance Show a => Show (Sign a)

- Lava.MyST: instance Applicative (ST s)

- Lava.MyST: instance Eq (STRef s a)

- Lava.MyST: instance Functor (ST s)

- Lava.MyST: instance Monad (ST s)

- Lava.Operators: instance SignalInt Int

- Lava.Operators: instance SignalInt a => Enum (Signal a)

- Lava.Operators: instance SignalInt a => Fractional (Signal a)

- Lava.Operators: instance SignalInt a => Num (Signal a)

- Lava.Operators: instance SignalInt a => Ord (Signal a)

- Lava.Property: instance (CoFresh a, Choice b, Fresh b) => Fresh (a -> b)

- Lava.Property: instance (CoFresh a, CoFresh b) => CoFresh (a, b)

- Lava.Property: instance (CoFresh a, CoFresh b, CoFresh c) => CoFresh (a, b, c)

- Lava.Property: instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d) => CoFresh (a, b, c, d)

- Lava.Property: instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e) => CoFresh (a, b, c, d, e)

- Lava.Property: instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f) => CoFresh (a, b, c, d, e, f)

- Lava.Property: instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f, CoFresh g) => CoFresh (a, b, c, d, e, f, g)

- Lava.Property: instance (Finite a, CoFresh b) => CoFresh (a -> b)

- Lava.Property: instance (Fresh a, Fresh b) => Fresh (a, b)

- Lava.Property: instance (Fresh a, Fresh b, Fresh c) => Fresh (a, b, c)

- Lava.Property: instance (Fresh a, Fresh b, Fresh c, Fresh d) => Fresh (a, b, c, d)

- Lava.Property: instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e) => Fresh (a, b, c, d, e)

- Lava.Property: instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f) => Fresh (a, b, c, d, e, f)

- Lava.Property: instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f, Fresh g) => Fresh (a, b, c, d, e, f, g)

- Lava.Property: instance (Fresh a, ShowModel a, Checkable b) => Checkable (a -> b)

- Lava.Property: instance (ShowModel a, ShowModel b) => ShowModel (a, b)

- Lava.Property: instance (ShowModel a, ShowModel b, ShowModel c) => ShowModel (a, b, c)

- Lava.Property: instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d) => ShowModel (a, b, c, d)

- Lava.Property: instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e) => ShowModel (a, b, c, d, e)

- Lava.Property: instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f) => ShowModel (a, b, c, d, e, f)

- Lava.Property: instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f, ShowModel g) => ShowModel (a, b, c, d, e, f, g)

- Lava.Property: instance Applicative Gen

- Lava.Property: instance Checkable Bool

- Lava.Property: instance Checkable Property

- Lava.Property: instance Checkable a => Checkable (Gen a)

- Lava.Property: instance Checkable a => Checkable (Signal a)

- Lava.Property: instance Checkable a => Checkable [a]

- Lava.Property: instance ChoiceWithSig Bool

- Lava.Property: instance ChoiceWithSig a => CoFresh (Signal a)

- Lava.Property: instance CoFresh ()

- Lava.Property: instance CoFresh a => CoFresh [a]

- Lava.Property: instance ConstructiveSig a => Fresh (Signal a)

- Lava.Property: instance Fresh ()

- Lava.Property: instance Functor Gen

- Lava.Property: instance Monad Gen

- Lava.Property: instance ShowModel ()

- Lava.Property: instance ShowModel (Signal a)

- Lava.Property: instance ShowModel (a -> b)

- Lava.Property: instance ShowModel a => ShowModel [a]

- Lava.Ref: instance Eq (Ref a)

- Lava.Ref: instance Eq (TableIO a b)

- Lava.Ref: instance Eq (TableST s a b)

- Lava.Ref: instance Show a => Show (Ref a)

- Lava.Sequent: instance Sequent []

- Lava.Signal: instance Eq (Signal a)

- Lava.Signal: instance Functor S

- Lava.Signal: instance Sequent S

- Lava.Signal: instance Show (Signal a)

- Lava.Signal: instance Show Symbol

- Lava.Signal: instance Show a => Show (S a)

- Lava.Verification: instance Eq Option

- Lava.Verification: instance Eq ProofResult

- Lava.Verification: instance Show Indexed

- Lava.Verification: instance Show Option

- Lava.Verification: instance Show ProofResult

- Lava.Verification: instance Show Timed

+ Lava.Error: instance GHC.Classes.Eq Lava.Error.Error

+ Lava.Error: instance GHC.Show.Show Lava.Error.Error

+ Lava.Generic: [delaySymbol] :: Ops -> Symbol -> Symbol -> Symbol

+ Lava.Generic: [equalSymbol] :: Ops -> Symbol -> Symbol -> Signal Bool

+ Lava.Generic: [ifSymbol] :: Ops -> Signal Bool -> (Symbol, Symbol) -> Symbol

+ Lava.Generic: [varSymbol] :: Ops -> String -> Symbol

+ Lava.Generic: [zeroSymbol] :: Ops -> Symbol

+ Lava.Generic: instance (Lava.Generic.Choice a, Lava.Generic.Choice b) => Lava.Generic.Choice (a, b)

+ Lava.Generic: instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c) => Lava.Generic.Choice (a, b, c)

+ Lava.Generic: instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d) => Lava.Generic.Choice (a, b, c, d)

+ Lava.Generic: instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d, Lava.Generic.Choice e) => Lava.Generic.Choice (a, b, c, d, e)

+ Lava.Generic: instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d, Lava.Generic.Choice e, Lava.Generic.Choice f) => Lava.Generic.Choice (a, b, c, d, e, f)

+ Lava.Generic: instance (Lava.Generic.Choice a, Lava.Generic.Choice b, Lava.Generic.Choice c, Lava.Generic.Choice d, Lava.Generic.Choice e, Lava.Generic.Choice f, Lava.Generic.Choice g) => Lava.Generic.Choice (a, b, c, d, e, f, g)

+ Lava.Generic: instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b) => Lava.Generic.Constructive (a, b)

+ Lava.Generic: instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c) => Lava.Generic.Constructive (a, b, c)

+ Lava.Generic: instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c, Lava.Generic.Constructive d) => Lava.Generic.Constructive (a, b, c, d)

+ Lava.Generic: instance (Lava.Generic.Constructive a, Lava.Generic.Constructive b, Lava.Generic.Constructive c, Lava.Generic.Constructive d, Lava.Generic.Constructive e) => Lava.Generic.Constructive (a, b, c, d, e)

+ Lava.Generic: instance (Lava.Generic.Finite a, Lava.Generic.Finite b) => Lava.Generic.Finite (a, b)

+ Lava.Generic: instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c) => Lava.Generic.Finite (a, b, c)

+ Lava.Generic: instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d) => Lava.Generic.Finite (a, b, c, d)

+ Lava.Generic: instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d, Lava.Generic.Finite e) => Lava.Generic.Finite (a, b, c, d, e)

+ Lava.Generic: instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d, Lava.Generic.Finite e, Lava.Generic.Finite f) => Lava.Generic.Finite (a, b, c, d, e, f)

+ Lava.Generic: instance (Lava.Generic.Finite a, Lava.Generic.Finite b, Lava.Generic.Finite c, Lava.Generic.Finite d, Lava.Generic.Finite e, Lava.Generic.Finite f, Lava.Generic.Finite g) => Lava.Generic.Finite (a, b, c, d, e, f, g)

+ Lava.Generic: instance (Lava.Generic.Generic a, Lava.Generic.Generic b) => Lava.Generic.Generic (a, b)

+ Lava.Generic: instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c) => Lava.Generic.Generic (a, b, c)

+ Lava.Generic: instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d) => Lava.Generic.Generic (a, b, c, d)

+ Lava.Generic: instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d, Lava.Generic.Generic e) => Lava.Generic.Generic (a, b, c, d, e)

+ Lava.Generic: instance (Lava.Generic.Generic a, Lava.Generic.Generic b, Lava.Generic.Generic c, Lava.Generic.Generic d, Lava.Generic.Generic e, Lava.Generic.Generic f) => Lava.Generic.Generic (a, b, c, d, e, f)

+ Lava.Generic: instance GHC.Base.Functor Lava.Generic.Struct

+ Lava.Generic: instance GHC.Classes.Eq a => GHC.Classes.Eq (Lava.Generic.Struct a)

+ Lava.Generic: instance GHC.Show.Show a => GHC.Show.Show (Lava.Generic.Struct a)

+ Lava.Generic: instance Lava.Generic.Choice ()

+ Lava.Generic: instance Lava.Generic.Choice (Lava.Signal.Signal a)

+ Lava.Generic: instance Lava.Generic.Choice Lava.Signal.Symbol

+ Lava.Generic: instance Lava.Generic.Choice a => Lava.Generic.Choice [a]

+ Lava.Generic: instance Lava.Generic.Choice b => Lava.Generic.Choice (a -> b)

+ Lava.Generic: instance Lava.Generic.Constructive ()

+ Lava.Generic: instance Lava.Generic.ConstructiveSig GHC.Types.Bool

+ Lava.Generic: instance Lava.Generic.ConstructiveSig GHC.Types.Int

+ Lava.Generic: instance Lava.Generic.ConstructiveSig a => Lava.Generic.Constructive (Lava.Signal.Signal a)

+ Lava.Generic: instance Lava.Generic.Finite ()

+ Lava.Generic: instance Lava.Generic.FiniteSig GHC.Types.Bool

+ Lava.Generic: instance Lava.Generic.FiniteSig a => Lava.Generic.Finite (Lava.Signal.Signal a)

+ Lava.Generic: instance Lava.Generic.Generic ()

+ Lava.Generic: instance Lava.Generic.Generic (Lava.Signal.Signal a)

+ Lava.Generic: instance Lava.Generic.Generic Lava.Signal.Symbol

+ Lava.Generic: instance Lava.Generic.Generic a => Lava.Generic.Generic [a]

+ Lava.Generic: instance Lava.Sequent.Sequent Lava.Generic.Struct

+ Lava.Isc: instance GHC.Base.Functor Lava.Isc.Sign

+ Lava.Isc: instance GHC.Read.Read a => GHC.Read.Read (Lava.Isc.Sign a)

+ Lava.Isc: instance GHC.Show.Show a => GHC.Show.Show (Lava.Isc.Sign a)

+ Lava.MyST: instance GHC.Base.Applicative (Lava.MyST.ST s)

+ Lava.MyST: instance GHC.Base.Functor (Lava.MyST.ST s)

+ Lava.MyST: instance GHC.Base.Monad (Lava.MyST.ST s)

+ Lava.MyST: instance GHC.Classes.Eq (Lava.MyST.STRef s a)

+ Lava.Operators: instance Lava.Operators.SignalInt GHC.Types.Int

+ Lava.Operators: instance Lava.Operators.SignalInt a => GHC.Classes.Ord (Lava.Signal.Signal a)

+ Lava.Operators: instance Lava.Operators.SignalInt a => GHC.Enum.Enum (Lava.Signal.Signal a)

+ Lava.Operators: instance Lava.Operators.SignalInt a => GHC.Num.Num (Lava.Signal.Signal a)

+ Lava.Operators: instance Lava.Operators.SignalInt a => GHC.Real.Fractional (Lava.Signal.Signal a)

+ Lava.Property: instance (Lava.Generic.Finite a, Lava.Property.CoFresh b) => Lava.Property.CoFresh (a -> b)

+ Lava.Property: instance (Lava.Property.CoFresh a, Lava.Generic.Choice b, Lava.Property.Fresh b) => Lava.Property.Fresh (a -> b)

+ Lava.Property: instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b) => Lava.Property.CoFresh (a, b)

+ Lava.Property: instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c) => Lava.Property.CoFresh (a, b, c)

+ Lava.Property: instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d) => Lava.Property.CoFresh (a, b, c, d)

+ Lava.Property: instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d, Lava.Property.CoFresh e) => Lava.Property.CoFresh (a, b, c, d, e)

+ Lava.Property: instance (Lava.Property.CoFresh a, Lava.Property.CoFresh b, Lava.Property.CoFresh c, Lava.Property.CoFresh d, Lava.Property.CoFresh e, Lava.Property.CoFresh f) => Lava.Property.CoFresh (a, b, c, d, e, f)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.Fresh b) => Lava.Property.Fresh (a, b)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c) => Lava.Property.Fresh (a, b, c)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d) => Lava.Property.Fresh (a, b, c, d)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d, Lava.Property.Fresh e) => Lava.Property.Fresh (a, b, c, d, e)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d, Lava.Property.Fresh e, Lava.Property.Fresh f) => Lava.Property.Fresh (a, b, c, d, e, f)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.Fresh b, Lava.Property.Fresh c, Lava.Property.Fresh d, Lava.Property.Fresh e, Lava.Property.Fresh f, Lava.Property.Fresh g) => Lava.Property.Fresh (a, b, c, d, e, f, g)

+ Lava.Property: instance (Lava.Property.Fresh a, Lava.Property.ShowModel a, Lava.Property.Checkable b) => Lava.Property.Checkable (a -> b)

+ Lava.Property: instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b) => Lava.Property.ShowModel (a, b)

+ Lava.Property: instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c) => Lava.Property.ShowModel (a, b, c)

+ Lava.Property: instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d) => Lava.Property.ShowModel (a, b, c, d)

+ Lava.Property: instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d, Lava.Property.ShowModel e) => Lava.Property.ShowModel (a, b, c, d, e)

+ Lava.Property: instance (Lava.Property.ShowModel a, Lava.Property.ShowModel b, Lava.Property.ShowModel c, Lava.Property.ShowModel d, Lava.Property.ShowModel e, Lava.Property.ShowModel f) => Lava.Property.ShowModel (a, b, c, d, e, f)

+ Lava.Property: instance GHC.Base.Applicative Lava.Property.Gen

+ Lava.Property: instance GHC.Base.Functor Lava.Property.Gen

+ Lava.Property: instance GHC.Base.Monad Lava.Property.Gen

+ Lava.Property: instance Lava.Generic.ConstructiveSig a => Lava.Property.Fresh (Lava.Signal.Signal a)

+ Lava.Property: instance Lava.Property.Checkable GHC.Types.Bool

+ Lava.Property: instance Lava.Property.Checkable Lava.Property.Property

+ Lava.Property: instance Lava.Property.Checkable a => Lava.Property.Checkable (Lava.Property.Gen a)

+ Lava.Property: instance Lava.Property.Checkable a => Lava.Property.Checkable (Lava.Signal.Signal a)

+ Lava.Property: instance Lava.Property.Checkable a => Lava.Property.Checkable [a]

+ Lava.Property: instance Lava.Property.ChoiceWithSig GHC.Types.Bool

+ Lava.Property: instance Lava.Property.ChoiceWithSig a => Lava.Property.CoFresh (Lava.Signal.Signal a)

+ Lava.Property: instance Lava.Property.CoFresh ()

+ Lava.Property: instance Lava.Property.CoFresh a => Lava.Property.CoFresh [a]

+ Lava.Property: instance Lava.Property.Fresh ()

+ Lava.Property: instance Lava.Property.ShowModel ()

+ Lava.Property: instance Lava.Property.ShowModel (Lava.Signal.Signal a)

+ Lava.Property: instance Lava.Property.ShowModel (a -> b)

+ Lava.Property: instance Lava.Property.ShowModel a => Lava.Property.ShowModel [a]

+ Lava.Ref: instance GHC.Classes.Eq (Lava.Ref.Ref a)

+ Lava.Ref: instance GHC.Classes.Eq (Lava.Ref.TableIO a b)

+ Lava.Ref: instance GHC.Classes.Eq (Lava.Ref.TableST s a b)

+ Lava.Ref: instance GHC.Show.Show a => GHC.Show.Show (Lava.Ref.Ref a)

+ Lava.Sequent: instance Lava.Sequent.Sequent []

+ Lava.Signal: instance GHC.Base.Functor Lava.Signal.S

+ Lava.Signal: instance GHC.Classes.Eq (Lava.Signal.Signal a)

+ Lava.Signal: instance GHC.Show.Show (Lava.Signal.Signal a)

+ Lava.Signal: instance GHC.Show.Show Lava.Signal.Symbol

+ Lava.Signal: instance GHC.Show.Show a => GHC.Show.Show (Lava.Signal.S a)

+ Lava.Signal: instance Lava.Sequent.Sequent Lava.Signal.S

+ Lava.Verification: instance GHC.Classes.Eq Lava.Verification.Option

+ Lava.Verification: instance GHC.Classes.Eq Lava.Verification.ProofResult

+ Lava.Verification: instance GHC.Show.Show Lava.Verification.Indexed

+ Lava.Verification: instance GHC.Show.Show Lava.Verification.Option

+ Lava.Verification: instance GHC.Show.Show Lava.Verification.ProofResult

+ Lava.Verification: instance GHC.Show.Show Lava.Verification.Timed

- Lava.Arithmetic: int2bin :: (Num a, Eq a) => a -> Signal Int -> [Signal Bool]

+ Lava.Arithmetic: int2bin :: (Eq a, Num a) => a -> Signal Int -> [Signal Bool]

- Lava.Patterns: bfly :: (Num a1, Eq a1) => a1 -> ([a] -> [a]) -> [a] -> [a]

+ Lava.Patterns: bfly :: (Eq a, Num a) => a -> ([a1] -> [a1]) -> [a1] -> [a1]

- Lava.Patterns: column :: ((t2, t) -> (t, t1)) -> ([t2], t) -> (t, [t1])

+ Lava.Patterns: column :: ((t2, t1) -> (t1, t)) -> ([t2], t1) -> (t1, [t])

- Lava.Patterns: ilv :: ([t] -> [a]) -> [t] -> [a]

+ Lava.Patterns: ilv :: ([a] -> [a1]) -> [a] -> [a1]

- Lava.Patterns: ilvN :: (Num a, Eq a) => a -> ([t] -> [a1]) -> [t] -> [a1]

+ Lava.Patterns: ilvN :: (Eq a, Num a) => a -> ([a1] -> [a2]) -> [a1] -> [a2]

- Lava.Patterns: iter :: (Num a, Eq a) => a -> (t -> t) -> t -> t

+ Lava.Patterns: iter :: (Eq a, Num a) => a -> (t -> t) -> t -> t

- Lava.Patterns: mirror :: ((t, t1) -> (t3, t2)) -> (t1, t) -> (t2, t3)

+ Lava.Patterns: mirror :: ((t1, t) -> (t3, t2)) -> (t, t1) -> (t2, t3)

- Lava.Patterns: row :: ((t2, t1) -> (t, t2)) -> (t2, [t1]) -> ([t], t2)

+ Lava.Patterns: row :: ((t1, t) -> (t2, t1)) -> (t1, [t]) -> ([t2], t1)

- Lava.Patterns: twoN :: (Num a, Eq a) => a -> ([a1] -> [a2]) -> [a1] -> [a2]

+ Lava.Patterns: twoN :: (Eq a, Num a) => a -> ([a1] -> [a2]) -> [a1] -> [a2]

- Lava.Patterns: unriffle :: [t] -> [t]

+ Lava.Patterns: unriffle :: [a] -> [a]

- Lava.SequentialCircuits: delayClk :: (Generic a, Choice a) => a -> (Signal Bool, a) -> a

+ Lava.SequentialCircuits: delayClk :: (Choice t, Generic t) => t -> (Signal Bool, t) -> t

- Lava.SequentialCircuits: delayN :: (Generic a1, Num a, Eq a) => a -> a1 -> a1 -> a1

+ Lava.SequentialCircuits: delayN :: (Eq a, Num a, Generic a1) => a -> a1 -> a1 -> a1

- Lava.SequentialCircuits: outputList :: Generic b => [b] -> () -> b

+ Lava.SequentialCircuits: outputList :: (Foldable t, Generic b) => t b -> () -> b

- Lava.SequentialCircuits: puls :: (Num a, Eq a) => a -> () -> Signal Bool

+ Lava.SequentialCircuits: puls :: (Eq a, Num a) => a -> () -> Signal Bool

- Lava.SequentialCircuits: rowSeqPeriod :: (Constructive t1, Choice t1, Num a, Eq a) => a -> ((t1, t2) -> (t, t1)) -> t2 -> t

+ Lava.SequentialCircuits: rowSeqPeriod :: (Eq a, Num a, Choice t2, Constructive t2) => a -> ((t2, t) -> (t1, t2)) -> t -> t1

- Lava.SequentialCircuits: rowSeqReset :: (Constructive t1, Choice t1) => ((t1, t2) -> (t, t1)) -> (Signal Bool, t2) -> t

+ Lava.SequentialCircuits: rowSeqReset :: (Choice t2, Constructive t2) => ((t2, t) -> (t1, t2)) -> (Signal Bool, t) -> t1

- Lava.Vis: equivCheckVisInput :: (Generic b1, Generic a, Generic b) => (a -> b) -> (a -> b1) -> a -> IO ProofResult

+ Lava.Vis: equivCheckVisInput :: (Generic b, Generic a, Generic b1) => (a -> b) -> (a -> b1) -> a -> IO ProofResult

Files

INSTALL +11/−0
Scripts/satzoo.wrapper +1/−1
Scripts/smv.wrapper +1/−1
chalmers-lava2000.cabal +2/−2

INSTALL view

@@ -1,3 +1,5 @@+# Installation+ First install the [Haskell Platform](http://www.haskell.org/platform).  Then install the package by running@@ -9,3 +11,12 @@     cabal install chalmers-lava2000  to install the latest version on Hackage.++# Verification++In order to use verification, make sure that the binaries `smv` and/or `satzoo` are visible in your path.++  * SMV can be obtained from here: <http://www.cs.cmu.edu/~modelcheck/smv.html>+  * There is (as of 2015-10-23) a cached version of Satzoo available here: <http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.cs.chalmers.se/~een/Satzoo/>++If verification gives ".../smv.wrapper Permission denied" (or similarly for `satzoo`), you need to mark the problematic files as executable. (That is, not the files in the `Scripts` directory, but the copy of those files that Cabal made during installation.

Scripts/satzoo.wrapper view

@@ -40,7 +40,7 @@  satzoo_() {-  time $Lava2000_Satzoo $Args $File 2> $Time+  time satzoo $Args $File 2> $Time }  satzoo_ > $Output

Scripts/smv.wrapper view

@@ -40,7 +40,7 @@  smv_() {-  /usr/bin/time $Lava2000_SMV $File $Args 2> $Time+  time smv $File $Args 2> $Time }  smv_ > $Output

chalmers-lava2000.cabal view

@@ -1,11 +1,11 @@ name:                chalmers-lava2000-version:             1.5+version:             1.5.1 synopsis:            Hardware description EDSL description:         For more info, see the tutorial: <http://projects.haskell.org/chalmers-lava2000/Doc/tutorial.pdf> category:            Language, Hardware license:             BSD3 license-file:        LICENSE-copyright:           (c) 2008. Koen Claessen <koen@chalmers.se>+copyright:           2008 Koen Claessen, 2008-2015 Emil Axelsson author:              Koen Claessen <koen@chalmers.se> maintainer:          Emil Axelsson <emax@chalmers.se> homepage:            http://projects.haskell.org/chalmers-lava2000/Doc/tutorial.pdf