diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,34 @@ +Version 0.1.0.0 +=============== + +#### Extensible Records + +* 'RecT' renamed to 'RecF' to avoid colliding with the naming scheme generally reserved for monad transformers. Record constructor names reflect this change. + +* The "rec" suffix removed from the functions 'setRecF', 'getRecF', 'getRec', and 'setRec' renamed to prefer the less noise 'setF', getF', 'set', and 'get'. + +* The selector constraint (.|) and (#) type synonym replaced with 'Has' constraint for readiblity. + ```haskell + -- previously + type HasFooInt ctx = "foo" # Int .| ctx + + -- ... is now + type HasFootInt ctx = Has "foo" Int ctx + ``` + +* A new type 'Evident' and class 'HasDict' now give a uniform way for capturing typeclass evidence of extensible records. + +* 'Rec' and 'RecT' instance declaration are no longer defined for the base case and inductive case. Instead, extensible record instances pass the responsibility witnessing a dictionary to a 'HasDict' superclass. + ```haskell + -- old version + instance Show (Rec '[]) where + show RNil = ... + + instance (Show x, Show xs) => Show (Rec (x ': xs)) where + show RNil = ... + + -- new version + instance HasDict Show ctx => Show (Rec ctx) where + show Nil = ... + show Con {} = ... + ``` diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "{}" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright 2021 Arista Networks + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,5 @@ +# spectacle + +[![ci](https://github.com/awakesecurity/spectacle/actions/workflows/ci.yml/badge.svg)](https://github.com/awakesecurity/spectacle/actions/workflows/ci.yml) + +`Language.Spectacle` defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under `test/integration`. diff --git a/spectacle.cabal b/spectacle.cabal new file mode 100644 --- /dev/null +++ b/spectacle.cabal @@ -0,0 +1,189 @@ +cabal-version: 2.4 + +name: spectacle +version: 1.0.0 +category: Testing, Concurrency +synopsis: Embedded specification language & model checker in Haskell. +description: + Spectacle is an embedded domain-specific language that provides a family + of type-level combinators for authoring specifications of program behavior + along with a model checker for verifying that user implementations of a + program satisfy written specifications. + +author: Arista Networks +maintainer: opensource@awakesecurity.com +homepage: https://github.com/awakesecurity/spectacle +bug-reports: https://github.com/awakesecurity/spectacle/issues +license: Apache-2.0 +license-file: LICENSE +copyright: 2021 Arista Networks +build-type: Simple +tested-with: + GHC == 8.10.3 + +extra-source-files: + README.md + CHANGELOG.md + +common common + default-language: Haskell2010 + + ghc-options: + -Wall + -Wcompat + -Wincomplete-record-updates + -Wincomplete-uni-patterns + -Wmissing-fields + -Wpartial-fields + -Widentities + -Wmissing-home-modules + -Wredundant-constraints + -fshow-warning-groups + -Wmissing-import-lists + -Wunused-packages + + build-depends: + base >=4.14 && <4.15 + + default-extensions: + BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures + DeriveFunctor DeriveGeneric DerivingVia FlexibleContexts FlexibleInstances + GADTs LambdaCase MagicHash MultiParamTypeClasses PatternSynonyms PolyKinds + RankNTypes RoleAnnotations ScopedTypeVariables StandaloneDeriving + StandaloneKindSignatures TypeApplications TypeOperators UnicodeSyntax + ViewPatterns + +library + import: common + hs-source-dirs: src + + build-depends: + comonad + , containers >= 0.6 + , hashable >= 1.3.0.0 + , microlens + , microlens-mtl + , mtl >= 2.2 + , optparse-applicative + , logict + , prettyprinter + , prettyprinter-ansi-terminal + , text + , transformers >= 0.5 + + exposed-modules: + Control.Applicative.Day + , Control.Applicative.Phases + , Control.Applicative.Queue + , Control.Comonad.Tape + , Control.Hyper + , Control.Mealy + , Control.Monad.Levels + , Control.Monad.Levels.Internal + , Control.Monad.Ref + , Control.Natural + , Data.Ascript + , Data.Bag + , Data.Fingerprint + , Data.Functor.Loom + , Data.Functor.Tree + , Data.Name + , Data.Node + , Data.Type.List + , Data.Type.Rec + , Data.World + , Language.Spectacle + , Language.Spectacle.AST + , Language.Spectacle.AST.Action + , Language.Spectacle.AST.Temporal + , Language.Spectacle.Exception.RuntimeException + , Language.Spectacle.Fairness + , Language.Spectacle.Interaction + , Language.Spectacle.Interaction.CLI + , Language.Spectacle.Interaction.Diagram + , Language.Spectacle.Interaction.Doc + , Language.Spectacle.Interaction.Options + , Language.Spectacle.Interaction.Paths + , Language.Spectacle.Interaction.Point + , Language.Spectacle.Interaction.Pos + , Language.Spectacle.Model + , Language.Spectacle.Model.ModelAction + , Language.Spectacle.Model.ModelEnv + , Language.Spectacle.Model.ModelError + , Language.Spectacle.Model.ModelNode + , Language.Spectacle.Model.ModelState + , Language.Spectacle.Model.ModelTemporal + , Language.Spectacle.Model.Monad + , Language.Spectacle.Lang + , Language.Spectacle.Lang.Internal + , Language.Spectacle.Lang.Member + , Language.Spectacle.Lang.Op + , Language.Spectacle.Lang.Scoped + , Language.Spectacle.RTS.Registers + , Language.Spectacle.Specification + , Language.Spectacle.Specification.Action + , Language.Spectacle.Specification.Prop + , Language.Spectacle.Specification.Variable + , Language.Spectacle.Syntax + , Language.Spectacle.Syntax.Closure + , Language.Spectacle.Syntax.Closure.Internal + , Language.Spectacle.Syntax.Enabled + , Language.Spectacle.Syntax.Enabled.Internal + , Language.Spectacle.Syntax.Env + , Language.Spectacle.Syntax.Env.Internal + , Language.Spectacle.Syntax.Error + , Language.Spectacle.Syntax.Error.Internal + , Language.Spectacle.Syntax.NonDet + , Language.Spectacle.Syntax.NonDet.Internal + , Language.Spectacle.Syntax.Plain + , Language.Spectacle.Syntax.Plain.Internal + , Language.Spectacle.Syntax.Prime + , Language.Spectacle.Syntax.Prime.Internal + , Language.Spectacle.Syntax.Quantifier + , Language.Spectacle.Syntax.Quantifier.Internal + , Language.Spectacle.Syntax.Logic + , Language.Spectacle.Syntax.Logic.Internal + +test-suite unit-tests + import: common + type: exitcode-stdio-1.0 + hs-source-dirs: test/unit-tests + main-is: Main.hs + + other-modules: + Test.Control.Comonad.Tape + Test.Gen + Test.Gen.Rec + Test.Language.Spectacle.Interaction + Test.Language.Spectacle.Interaction.Paths + Test.Language.Spectacle.Interaction.Pos + Test.Laws.Lens + Test.Laws.Ord + + build-depends: + comonad + , containers + , spectacle + , hedgehog + , microlens + , tasty + , tasty-hedgehog + +test-suite integration-tests + import: common + type: exitcode-stdio-1.0 + hs-source-dirs: test/integration + main-is: Main.hs + + other-modules: + Specifications.BitClock + Specifications.Diehard + Specifications.SimpleClock + Specifications.Status + + build-depends: + spectacle + , hashable + , hedgehog + , tasty + , tasty-hedgehog diff --git a/src/Control/Applicative/Day.hs b/src/Control/Applicative/Day.hs new file mode 100644 --- /dev/null +++ b/src/Control/Applicative/Day.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE TupleSections #-} + +-- | Cayley applicative transformer. +-- +-- === Reference +-- +-- 1. +-- +-- 2. "Notions of Computations as Monoids" +-- +-- @since 1.0.0 +module Control.Applicative.Day + ( Day (Day), + getDay, + wrapDay, + ) +where + +import Control.Applicative (liftA2) +import Data.Bifunctor (first) +import Data.Kind (Type) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype Day :: (Type -> Type) -> Type -> Type where + Day :: {getDay :: forall x. f x -> f (a, x)} -> Day f a + +wrapDay :: Monad m => m (Day m a) -> Day m a +wrapDay ma = Day \mx -> + ma >>= \case + Day k -> k mx + +-- | @since 1.0.0 +instance Functor f => Functor (Day f) where + fmap f (Day xs) = Day (fmap (first f) . xs) + {-# INLINE fmap #-} + +-- | @since 1.0.0 +instance Functor f => Applicative (Day f) where + pure x = Day (fmap (x,)) + {-# INLINE pure #-} + + liftA2 c xs ys = Day (fmap (\(x, (y, z)) -> (c x y, z)) . getDay xs . getDay ys) + {-# INLINE liftA2 #-} diff --git a/src/Control/Applicative/Phases.hs b/src/Control/Applicative/Phases.hs new file mode 100644 --- /dev/null +++ b/src/Control/Applicative/Phases.hs @@ -0,0 +1,61 @@ +-- | 'Phases' applicative functor transformer. +-- +-- === Reference +-- +-- 1. +-- +-- 2. +-- +-- @since 1.0.0 +module Control.Applicative.Phases + ( Phases (Here, There), + lowerPhases, + wrapPhases, + liftPhases, + ) +where + +import Control.Applicative (Applicative (liftA2)) +import Data.Kind (Type) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'Phases' is similar to a free applicative functor with the primary differences being it is based on 'liftA2' rather +-- than '(<*>)' and its 'Applicative' instance. +-- +-- The instance 'Applicative' of 'Phases' is not definitionally applicative, and is instead used to reorder and zip +-- effects of the underlying @f@. The 'Here' constructor apply effects immediately and 'There' constructors +-- incrementally delay effects. +-- +-- @since 1.0.0 +data Phases :: (Type -> Type) -> Type -> Type where + Here :: a -> Phases f a + There :: (a -> b -> c) -> f a -> Phases f b -> Phases f c + +lowerPhases :: Applicative f => Phases f a -> f a +lowerPhases (Here x) = pure x +lowerPhases (There op x xs) = liftA2 op x (lowerPhases xs) + +wrapPhases :: Monad f => f (Phases f a) -> Phases f a +wrapPhases f = There const (f >>= lowerPhases) (pure ()) + +liftPhases :: Monad f => Phases f (f a) -> Phases f a +liftPhases (Here x) = There const x (pure ()) +liftPhases (There f x xs) = There const (x >>= \x' -> lowerPhases xs >>= f x') xs + +-- | @since 1.0.0 +instance Functor (Phases f) where + fmap f (Here x) = Here (f x) + fmap f (There op x xs) = There (\y ys -> f (y `op` ys)) x xs + {-# INLINE fmap #-} + +-- | @since 1.0.0 +instance Applicative f => Applicative (Phases f) where + pure = Here + {-# INLINE pure #-} + + liftA2 c (Here x) ys = fmap (c x) ys + liftA2 c xs (Here y) = fmap (`c` y) xs + liftA2 c (There f x xs) (There g y ys) = + There (\(x', y') (xs', ys') -> c (f x' xs') (g y' ys')) (liftA2 (,) x y) (liftA2 (,) xs ys) + {-# INLINE liftA2 #-} diff --git a/src/Control/Applicative/Queue.hs b/src/Control/Applicative/Queue.hs new file mode 100644 --- /dev/null +++ b/src/Control/Applicative/Queue.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE TupleSections #-} + +-- | Effect queues. +-- +-- @since 1.0.0 +module Control.Applicative.Queue + ( Queue, + runQueue, + liftQueue, + wrapQueue, + joinQueue, + now, + later, + ) +where + +import Control.Applicative (Applicative (liftA2)) + +import Control.Applicative.Day (Day (Day), getDay) +import Control.Applicative.Phases (Phases (Here, There), liftPhases, lowerPhases, wrapPhases) + +-- --------------------------------------------------------------------------------------------------------------------- + +type Queue f = Day (Phases f) + +runQueue :: Applicative f => Queue f a -> f a +runQueue = fmap fst . lowerPhases . flip getDay (Here ()) + +liftQueue :: Monad f => Queue f (f a) -> Queue f a +liftQueue (Day f) = Day \x -> + let fx = fmap fst (f x) + fy = fmap snd (f (fmap snd (f x))) + in liftA2 (,) (liftPhases fx) fy + +wrapQueue :: Monad f => f (Queue f a) -> Queue f a +wrapQueue f = Day \x -> wrapPhases (fmap (($ x) . getDay) f) + +joinQueue :: Monad f => Queue f (Queue f a) -> Queue f a +joinQueue (Day f) = Day \x -> + let x' = lowerPhases (fmap fst (f x)) + in getDay (wrapQueue x') x + +now :: Applicative f => f a -> Queue f a +now xs = Day \case + Here x -> There (,) xs (Here x) + There f y ys -> There (\(a, b) c -> (a, f b c)) (liftA2 (,) xs y) ys + +later :: Applicative f => Queue f a -> Queue f a +later q = Day (go q) + where + go :: Applicative f => Queue f a -> Phases f b -> Phases f (a, b) + go (Day f) (Here y) = There (const id) (pure ()) (f (Here y)) + go (Day f) (There g y ys) = There (fmap . g) y (f ys) diff --git a/src/Control/Comonad/Tape.hs b/src/Control/Comonad/Tape.hs new file mode 100644 --- /dev/null +++ b/src/Control/Comonad/Tape.hs @@ -0,0 +1,119 @@ +module Control.Comonad.Tape + ( -- * Tape Comonad + Tape (Tape, before, focus, after), + + -- ** Construction + viewl, + viewr, + viewAt, + + -- ** Destruction + toSeq, + + -- ** Operations + shiftl, + shiftr, + tabulater, + tabulatel, + ) +where + +import Control.Comonad (Comonad, duplicate, extend, extract) +import Control.Comonad.Store (ComonadStore, peek, pos, seek) +import Data.Sequence (Seq (Empty, (:<|), (:|>)), (<|), (|>)) +import qualified Data.Sequence as Seq + +-- --------------------------------------------------------------------------------------------------------------------- + +data Tape a = Tape {before :: Seq a, focus :: a, after :: Seq a} + deriving (Eq, Functor, Show) + +-- | @since 1.0.0 +instance Foldable Tape where + foldr cons nil = foldr cons nil . toSeq + {-# INLINE foldr #-} + +-- | @since 1.0.0 +instance Traversable Tape where + traverse f (Tape lower x upper) = Tape <$> traverse f lower <*> f x <*> traverse f upper + {-# INLINE traverse #-} + +-- | @since 1.0.0 +instance Comonad Tape where + extract (Tape _ x _) = x + {-# INLINE extract #-} + + duplicate tp = Tape (tabulatel tp) tp (tabulater tp) + {-# INLINE duplicate #-} + + extend f tp = case duplicate tp of + Tape ls x us -> Tape (f <$> ls) (f x) (f <$> us) + +-- | @since 1.0.0 +instance ComonadStore Int Tape where + pos (Tape lw _ _) = length lw + {-# INLINE pos #-} + + peek n + | n < 0 = extract . shiftl n + | n > 0 = extract . shiftr n + | otherwise = extract + {-# INLINE peek #-} + + seek n + | n < 0 = shiftl n + | n > 0 = shiftr n + | otherwise = id + {-# INLINE seek #-} + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | /O(1)/, @'viewl' xs@ constructs a 'Tape' by viewing @xs@ from the left, if it is nonempty. +-- +-- @since 1.0.0 +viewl :: Seq a -> Maybe (Tape a) +viewl Empty = Nothing +viewl (x :<| upper) = Just (Tape mempty x upper) + +-- | /O(1)/, @'viewl' xs@ constructs a 'Tape' by viewing @xs@ from the left, if it is nonempty. +-- +-- @since 1.0.0 +viewr :: Seq a -> Maybe (Tape a) +viewr Empty = Nothing +viewr (lower :|> x) = Just (Tape lower x mempty) + +-- | /O(log n)/, @'viewAt' i xs@ constructs a 'Tape' focusing the ith element of @xs@, if it is nonempty. @i@ is +-- clamped to the interval [0, i). +-- +-- @since 1.0.0 +viewAt :: Int -> Seq a -> Maybe (Tape a) +viewAt i xs = + case Seq.splitAt i xs of + (Empty, Empty) -> Nothing + (lower :|> x, Empty) -> Just (Tape lower x Empty) + (lower, x :<| upper) -> Just (Tape lower x upper) + +toSeq :: Tape a -> Seq a +toSeq (Tape lower x upper) = lower <> (x <| upper) + +shiftl :: Int -> Tape a -> Tape a +shiftl i (Tape lw0 x0 up0) = + case Seq.splitAt (length lw0 - abs i) lw0 of + (_, Empty) -> Tape lw0 x0 up0 + (lw, x :<| up) -> Tape lw x (up <> (x0 <| up0)) + +shiftr :: Int -> Tape a -> Tape a +shiftr i (Tape lw0 x0 up0) = + case Seq.splitAt (abs i) up0 of + (Empty, _) -> Tape lw0 x0 up0 + (lw :|> x, up) -> Tape (lw0 <> (x0 <| lw)) x up + +tabulatel :: Tape a -> Seq (Tape a) +tabulatel sp@(Tape lower _ _) + | Seq.null lower = Seq.empty + | otherwise = tabulatel (shiftl 1 sp) |> shiftl 1 sp + +tabulater :: Tape a -> Seq (Tape a) +tabulater sp@(Tape _ _ up) + | Seq.null up = Seq.empty + | otherwise = shiftr 1 sp <| tabulater (shiftr 1 sp) diff --git a/src/Control/Hyper.hs b/src/Control/Hyper.hs new file mode 100644 --- /dev/null +++ b/src/Control/Hyper.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE PartialTypeSignatures #-} +-- Needed for MonadZip (LogicT m) +{-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_GHC -Wno-unused-matches #-} + +-- | Hyperfunction transformer. +-- +-- @since 1.0.0 +module Control.Hyper + ( HyperM (HyperM, invokeM), + ) +where + +import Control.Monad (join) +import Control.Monad.Logic (LogicT (LogicT)) +import Control.Monad.Zip (MonadZip, mzipWith) +import Data.Kind (Type) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype HyperM :: (Type -> Type) -> Type -> Type -> Type where + HyperM :: {invokeM :: m ((HyperM m a b -> a) -> b)} -> HyperM m a b + +-- | @since 1.0.0 +instance Monad m => MonadZip (LogicT m) where + mzipWith op (LogicT f) (LogicT g) = LogicT \cons nil -> + let fs x xs = pure (\k -> k (HyperM xs) x) + + gs y ys = pure (\k x -> cons (op x y) (join (invokeM k <*> ys))) + in join (f fs (pure (const nil)) <*> g gs (pure \_ _ -> nil)) + {-# INLINE mzipWith #-} diff --git a/src/Control/Mealy.hs b/src/Control/Mealy.hs new file mode 100644 --- /dev/null +++ b/src/Control/Mealy.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE TupleSections #-} + +-- | +-- +-- @since 1.0.0 +module Control.Mealy + ( -- * Mealy Machines + Mealy, + runMealy, + + -- ** Applicative Transformer + MealyM (MealyM), + runMealyM, + arrM, + refold, + ) +where + +import Control.Applicative (liftA2) +import Data.Functor.Identity (Identity (runIdentity)) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype MealyM m a b = MealyM + {runMealyM :: a -> m (b, MealyM m a b)} + deriving (Functor) + +arrM :: Functor m => (a -> m b) -> MealyM m a b +arrM f = let k = MealyM (fmap (,k) . f) in k + +refold :: Monad m => (a -> b -> MealyM m a c -> m (c, MealyM m a c)) -> MealyM m a b -> MealyM m a c +refold f (MealyM k) = + MealyM \s -> do + (x, k') <- k s + f s x (refold f k') + +type Mealy = MealyM Identity + +runMealy :: Mealy a b -> a -> (b, Mealy a b) +runMealy (MealyM k) x = runIdentity (k x) + +-- | @since 1.0.0 +instance (Applicative m, Semigroup b) => Semigroup (MealyM m a b) where + MealyM f <> MealyM g = MealyM \x -> liftA2 (<>) (f x) (g x) + {-# INLINE (<>) #-} + +-- | @since 1.0.0 +instance (Applicative m, Monoid b) => Monoid (MealyM m a b) where + mempty = MealyM \_ -> pure mempty + {-# INLINE mempty #-} + +-- | @since 1.0.0 +instance Applicative m => Applicative (MealyM m a) where + pure x = MealyM \_ -> pure (x, pure x) + {-# INLINE pure #-} + + MealyM m <*> MealyM n = MealyM \x -> + liftA2 (\(f, m') (c, n') -> (f c, m' <*> n')) (m x) (n x) + {-# INLINE (<*>) #-} diff --git a/src/Control/Monad/Levels.hs b/src/Control/Monad/Levels.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Levels.hs @@ -0,0 +1,34 @@ +-- | +-- +-- @since 1.0.0 +module Control.Monad.Levels + ( -- * Levels + Levels, + runLevels, + + -- * LevelsT + LevelsT (LevelsT), + runLevelsT, + observeLevelsT, + execLevelsT, + runLevelsA, + liftLevelsT, + wrapLevelsT, + ) +where + +import Control.Applicative (Alternative, (<|>)) + +import Control.Monad.Levels.Internal (Levels, LevelsT (LevelsT), liftLevelsT, runLevels, runLevelsT, wrapLevelsT) +import Data.Bag (Bag (None)) + +-- --------------------------------------------------------------------------------------------------------------------- + +observeLevelsT :: Applicative m => LevelsT m a -> m [a] +observeLevelsT (LevelsT m) = m (fmap . (++) . foldMap pure) (pure []) + +execLevelsT :: Applicative m => LevelsT m a -> m () +execLevelsT (LevelsT m) = m (const id) (pure ()) + +runLevelsA :: Alternative m => LevelsT m a -> m (Bag a) +runLevelsA (LevelsT m) = m ((<|>) . pure) (pure None) diff --git a/src/Control/Monad/Levels/Internal.hs b/src/Control/Monad/Levels/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Levels/Internal.hs @@ -0,0 +1,138 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | The "Levels" search monad. +-- +-- === Reference +-- +-- 1. Donnacha Oisín Kidney, Nicolas Wu. 2021. Algebras for Weighted Search. +-- +-- @since 1.0.0 +module Control.Monad.Levels.Internal + ( -- * Levels + Levels, + runLevels, + + -- * Levels Transformer + LevelsT (LevelsT, runLevelsT), + foldAlt, + liftLevelsT, + wrapLevelsT, + ) +where + +import Control.Applicative (Alternative (empty, (<|>)), Applicative (liftA2)) +import Control.Monad (ap) +import Control.Monad.Except (MonadError (catchError, throwError)) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Reader (MonadReader (local, reader)) +import Control.Monad.State (MonadState (state)) +import Control.Monad.Trans.Class (MonadTrans, lift) +import Data.Functor.Identity (Identity, runIdentity) +import Data.Kind (Type) + +import Control.Hyper (HyperM (HyperM, invokeM)) +import Data.Bag (Bag (None)) +import qualified Data.Bag as Bag + +-- --------------------------------------------------------------------------------------------------------------------- + +type Levels = LevelsT Identity + +runLevels :: Levels a -> (Bag a -> b -> b) -> b -> b +runLevels (LevelsT k) cons nil = runIdentity (k (fmap . cons) (pure nil)) + +-- | @since 1.0.0 +instance Foldable Levels where + foldMap f m = runLevels m (mappend . foldMap f) mempty + {-# INLINE foldMap #-} + +-- | @since 1.0.0 +instance Traversable Levels where + traverse f m = runLevels m (liftA2 (<|>) . fmap foldAlt . traverse f) (pure empty) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype LevelsT :: (Type -> Type) -> Type -> Type where + LevelsT :: {runLevelsT :: forall x. (Bag a -> m x -> m x) -> m x -> m x} -> LevelsT m a + +-- | Constructs a 'LevelsT' with a single level, the monoid provided. +-- +-- @since 1.0.0 +foldAlt :: Foldable m => m a -> LevelsT f a +foldAlt xs = LevelsT \cons nil -> cons (foldr Bag.cons Bag.empty xs) nil + +liftLevelsT :: Monad m => m (LevelsT m a) -> LevelsT m a +liftLevelsT xs = LevelsT (\cons nil -> xs >>= \xs' -> runLevelsT xs' cons nil) + +wrapLevelsT :: Monad m => m (LevelsT m a) -> LevelsT m a +wrapLevelsT xs = LevelsT (\cons nil -> cons None (xs >>= \xs' -> runLevelsT xs' cons nil)) + +-- | @since 1.0.0 +instance Functor (LevelsT m) where + fmap f (LevelsT g) = LevelsT \cons nil -> g (cons . fmap f) nil + {-# INLINE fmap #-} + +-- | @since 1.0.0 +instance Monad m => Applicative (LevelsT m) where + pure x = LevelsT \cons nil -> cons (Bag.singleton x) nil + {-# INLINE pure #-} + + -- TODO: Lower the definition of (<*>) from 'ap'. + (<*>) = ap + {-# INLINE (<*>) #-} + +-- | @since 1.0.0 +instance Monad m => Monad (LevelsT m) where + LevelsT m >>= k = liftLevelsT (m (\x xs -> pure (foldr ((<|>) . k) (wrapLevelsT xs) x)) (pure empty)) + {-# INLINE (>>=) #-} + +-- | @since 1.0.0 +instance Monad m => Alternative (LevelsT m) where + empty = LevelsT \_ nil -> nil + {-# INLINE empty #-} + + LevelsT f <|> LevelsT g = LevelsT \cons nil -> + -- NOTE: The instance given here yields O(n) complexity for (<|>) and is outlined in "Algebras for weighted search." + let fcons x xs = pure (\k -> k (HyperM xs) x) + fnil = pure \k -> k (HyperM fnil) None + + gcon y yk = pure \xk x -> cons (x <> y) (invokeM xk >>= (yk >>=)) + + gnil _ None = nil + gnil xk x = cons x (invokeM xk >>= ($ gnil)) + in f fcons fnil >>= (g gcon (pure gnil) >>=) + {-# INLINE (<|>) #-} + +-- | @since 1.0.0 +instance MonadTrans LevelsT where + lift m = LevelsT \cons nil -> m >>= (`cons` nil) . Bag.singleton + {-# INLINE lift #-} + +-- | @since 1.0.0 +instance MonadState s m => MonadState s (LevelsT m) where + state = lift . state + {-# INLINE state #-} + +-- | @since 1.0.0 +instance MonadReader r m => MonadReader r (LevelsT m) where + reader = lift . reader + {-# INLINE reader #-} + + local f (LevelsT g) = LevelsT \cons nil -> + local f (g cons nil) + {-# INLINE local #-} + +-- | @since 1.0.0 +instance MonadError e m => MonadError e (LevelsT m) where + throwError = lift . throwError + {-# INLINE throwError #-} + + catchError (LevelsT f) g = LevelsT \cons nil -> + catchError (f cons nil) (\e -> runLevelsT (g e) cons nil) + {-# INLINE catchError #-} + +-- | @since 1.0.0 +instance MonadIO m => MonadIO (LevelsT m) where + liftIO m = LevelsT \cons nil -> liftIO m >>= (`cons` nil) . Bag.singleton + {-# INLINE liftIO #-} diff --git a/src/Control/Monad/Ref.hs b/src/Control/Monad/Ref.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Ref.hs @@ -0,0 +1,67 @@ +-- | State implemented over 'IORef'. +-- +-- @since 1.0.0 +module Control.Monad.Ref + ( -- * RefM Transformer + RefM (RefM), + unRefM, + + -- ** Lowering + runRefM, + execRefM, + ) +where + +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.State (MonadState, get, put) +import Data.IORef (IORef, newIORef, readIORef, writeIORef) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'RefM' is an impure state monad transformer built around IORef. +-- +-- In situations where the state @s@ is a large structure which undergoes frequent alteration, 'RefM' can be used as a +-- more preformant alternative to state (assuming its impurity is not a concern). +-- +-- @since 1.0.0 +newtype RefM s m a = RefM + {unRefM :: IORef s -> m a} + deriving (Functor) + +runRefM :: MonadIO m => RefM s m a -> s -> m (s, a) +runRefM (RefM k) st = do + ref <- liftIO (newIORef st) + ret <- k ref + st' <- liftIO (readIORef ref) + return (st', ret) + +execRefM :: MonadIO m => RefM s m a -> s -> m s +execRefM refM st = fst <$> runRefM refM st + +-- | @since 1.0.0 +instance Applicative m => Applicative (RefM s m) where + pure x = RefM \_ -> pure x + {-# INLINE pure #-} + + RefM f <*> RefM m = RefM \ref -> + f ref <*> m ref + {-# INLINE (<*>) #-} + +-- | @since 1.0.0 +instance Monad m => Monad (RefM s m) where + RefM f >>= m = RefM \ref -> + f ref >>= \x -> unRefM (m x) ref + {-# INLINE (>>=) #-} + +-- | @since 1.0.0 +instance MonadIO m => MonadIO (RefM s m) where + liftIO m = RefM \_ -> liftIO m + {-# INLINE liftIO #-} + +-- | @since 1.0.0 +instance MonadIO m => MonadState s (RefM s m) where + get = RefM (liftIO . readIORef) + {-# INLINE get #-} + + put x = RefM \ref -> liftIO (writeIORef ref x) + {-# INLINE put #-} diff --git a/src/Control/Natural.hs b/src/Control/Natural.hs new file mode 100644 --- /dev/null +++ b/src/Control/Natural.hs @@ -0,0 +1,12 @@ +module Control.Natural + ( type (~>), + ) +where + +import Data.Kind (Type) + +-- ------------------------------------------------------------------------------------------------- + +infix 0 ~> +type (~>) :: (Type -> Type) -> (Type -> Type) -> Type +type f ~> g = forall x. f x -> g x diff --git a/src/Data/Ascript.hs b/src/Data/Ascript.hs new file mode 100644 --- /dev/null +++ b/src/Data/Ascript.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE TypeFamilies #-} + +module Data.Ascript + ( Ascribe (..), + type (#), + type AscriptName, + type AscriptType, + ) +where + +import Data.Kind (Type) +import GHC.TypeLits (Symbol) + +-- ------------------------------------------------------------------------------------------------- + +-- | Type ascriptions. +-- +-- @since 0.1.0.0 +data Ascribe s a = Ascribe s a + +-- | The kind of type ascribed variables in the type row of a 'Data.Type.Rec'. +-- +-- @since 0.1.0.0 +infix 6 # + +type (#) :: Symbol -> k -> Ascribe Symbol k +type s # a = 'Ascribe s a + +-- | Project the type of a 'Data.Type.Rec' ascription. +-- +-- @since 0.1.0.0 +type AscriptType :: Ascribe Symbol Type -> Type +type family AscriptType a where + AscriptType (_ # a) = a + +-- | Project the symbol of a 'Data.Type.Rec' ascription. +-- +-- @since 0.1.0.0 +type AscriptName :: Ascribe Symbol Type -> Symbol +type family AscriptName a where + AscriptName (s # _) = s diff --git a/src/Data/Bag.hs b/src/Data/Bag.hs new file mode 100644 --- /dev/null +++ b/src/Data/Bag.hs @@ -0,0 +1,75 @@ +-- | +-- +-- @since 0.1.0.0 +module Data.Bag + ( Bag (None, Some), + empty, + cons, + singleton, + ) +where + +import Data.Kind (Type) + +import Data.Node (Node (Leaf, (:*:))) + +-- --------------------------------------------------------------------------------------------------------------------- + +data Bag :: Type -> Type where + None :: Bag a + Some :: Node a -> Bag a + deriving (Show) + +empty :: Bag a +empty = None + +cons :: a -> Bag a -> Bag a +cons x None = Some (Leaf x) +cons x (Some xs) = Some (Leaf x :*: xs) + +singleton :: a -> Bag a +singleton = Some . Leaf + +-- | @since 0.1.0.0 +instance Functor Bag where + fmap _ None = None + fmap f (Some xs) = Some (fmap f xs) + {-# INLINE fmap #-} + +-- | @since 0.1.0.0 +instance Applicative Bag where + pure = Some . Leaf + {-# INLINE pure #-} + + None <*> _ = None + _ <*> None = None + Some fs <*> Some xs = Some (fs <*> xs) + {-# INLINE (<*>) #-} + +-- | @since 0.1.0.0 +instance Semigroup (Bag a) where + None <> ys = ys + xs <> None = xs + Some xs <> Some ys = Some (xs <> ys) + {-# INLINE (<>) #-} + +-- | @since 0.1.0.0 +instance Monoid (Bag a) where + mempty = None + {-# INLINE CONLIKE mempty #-} + +-- | @since 0.1.0.0 +instance Foldable Bag where + foldMap _ None = mempty + foldMap f (Some xs) = foldMap f xs + {-# INLINE foldMap #-} + + foldr _ nil None = nil + foldr c nil (Some xs) = foldr c nil xs + {-# INLINE foldr #-} + +-- | @since 0.1.0.0 +instance Traversable Bag where + traverse _ None = pure None + traverse f (Some xs) = fmap Some (traverse f xs) + {-# INLINE traverse #-} diff --git a/src/Data/Fingerprint.hs b/src/Data/Fingerprint.hs new file mode 100644 --- /dev/null +++ b/src/Data/Fingerprint.hs @@ -0,0 +1,72 @@ +-- | The 'Fingerprint' data type. +-- +-- @since 0.1.0.0 +module Data.Fingerprint + ( -- * Fingerprints + Fingerprint (Fingerprint), + getFingerprint, + + -- ** Construction + fingerprintRec, + + -- ** Conversions + showAsHex, + ) +where + +import Data.Bits (Bits (rotateR, (.&.))) +import Data.Hashable (Hashable, hash) +import Prettyprinter (Pretty, pretty) + +import Data.Type.Rec (Rec) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'Fingerprint' is a 32-bit hash used for uniquely identifying worlds while model checking. +-- +-- @since 0.1.0.0 +newtype Fingerprint = Fingerprint {getFingerprint :: Int} + deriving stock (Eq, Ord) + deriving (Enum, Hashable, Integral, Num, Real) via Int + +-- | @since 0.1.0.0 +instance Show Fingerprint where + show (Fingerprint fp) = "0x" ++ showAsHex fp + {-# INLINE show #-} + +-- | @since 0.1.0.0 +instance Pretty Fingerprint where + pretty = pretty . show + {-# INLINE pretty #-} + +-- | Constructs a probabilistically unique 'Fingerprint' from the given world. +-- +-- @since 0.1.0.0 +fingerprintRec :: Hashable (Rec ctx) => Rec ctx -> Fingerprint +fingerprintRec world = Fingerprint (hash world) + +-- | Converts an 'Int' to a hexdecimal string without a strictly positive constraint and without the preformance hit of +-- the analogous prelude function 'showHex'. +-- +-- @since 0.1.0.0 +showAsHex :: Int -> String +showAsHex = go 0 + where + go :: Int -> Int -> String + go i n + | i < 8 = fastToHexEnum (rotateR n (4 * i) .&. 0xF) : go (i + 1) n + | otherwise = [] + +-- | Converts an 'n :: Int' in the interval [0, 15] to @['0' .. '9']@ if @n <= 9@, otherwise @n@ is mapped to +-- @['a' .. 'f']@. Used to quickly convert 'Int' to a hexdecimal string. +-- +-- Note 'fastToHexEnum' is implemented via 'toEnum' so it is as fast as it is unsafe. +-- +-- @since 0.1.0.0 +fastToHexEnum :: Int -> Char +fastToHexEnum n + -- The integer range for the enums @['0' .. '9'] :: 'String'@ is @[48 .. 56] :: ['Int']@. + | n <= 9 = toEnum (n + 48) + -- The integer range for the enums @['a' .. 'f'] :: 'String'@ is @[97 .. 102] :: ['Int']@, so to construct the map + -- [10 .. 15] -> [97 .. 102] we subtract have to subtract 10 on both sides, hence adding 87. + | otherwise = toEnum (n + 87) diff --git a/src/Data/Functor/Loom.hs b/src/Data/Functor/Loom.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Loom.hs @@ -0,0 +1,104 @@ +-- | The 'Loom' functor. The mnemonic for 'Loom' is from it accumulating a continuation of /weaving/ +-- functions. +-- +-- @since 0.1.0.0 +module Data.Functor.Loom + ( -- * Loom + Loom (Loom), + runLoom, + (~>~), + identity, + + -- * Loom Combinators + weave, + bind, + lift, + hoist, + ) +where + +import Control.Monad ((>=>)) +import Data.Functor.Compose (Compose (Compose, getCompose)) +import Data.Functor.Identity (Identity (Identity, runIdentity)) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'Loom' is very similar to Coyoneda but accumulates weaving functions rather than ordinary functions. 'Loom' is used +-- to build up a continuation of higher-order effect handlers. +-- +-- @since 0.1.0.0 +data Loom m n a b where + Loom :: Functor f => f () -> (f (m a) -> n b) -> Loom m n a b + +-- | @since 0.1.0.0 +instance Functor n => Functor (Loom m n a) where + fmap f (Loom ctx eta) = Loom ctx (fmap f . eta) + {-# INLINE fmap #-} + +-- | Unwraps a 'Loom' into a natural transformation. +-- +-- @since 0.1.0.0 +runLoom :: Loom m n a b -> (m a -> n b) +runLoom (Loom ctx eta) m = eta (m <$ ctx) +{-# INLINE runLoom #-} + +-- | 'Loom' composition, 'Loom's can be constructed with the 'bind', 'lift', 'run', and 'hoist' combinators +-- and subsequently composed to produce complex weaves in a straightforward way: +-- +-- @ +-- -- weaving a state +-- let loom :: Loom (Lang ctx effs') (Lang ctx effs) a b +-- let weaveF :: s -> Lang ctx (eff ': effs) a -> Lang ctx effs (s, a) +-- weaveF = uncurry (loom ~>~ weave (st :: s, ()) (f :: s -> a -> Lang ctx effs (s a))) +-- @ +-- +-- @since 0.1.0.0 +infixr 9 ~>~ + +(~>~) :: Loom m n a b -> Loom n o b c -> Loom m o a c +Loom ctx eta ~>~ Loom ctx' eta' = Loom (Compose (ctx <$ ctx')) (eta' . fmap eta . getCompose) +{-# INLINE (~>~) #-} + +-- | Constructs the identity 'Loom'. +-- +-- @ +-- id == Loom (Identity ()) runIdentity +-- @ +-- +-- @since 0.1.0.0 +identity :: Loom m m a a +identity = Loom (Identity ()) runIdentity +{-# INLINE identity #-} + +-- | Constructs an "Effect Handlers in Scope"-style weaving function from the functor context and the distribution +-- function. This is a synonym for the 'Loom' constructor. +-- +-- @since 0.1.0.0 +weave :: Functor f => f () -> (f (m a) -> n (f b)) -> Loom m n a (f b) +weave = Loom +{-# INLINE weave #-} + +-- | Constructs a 'Loom' from a bind function. +-- +-- @since 0.1.0.0 +bind :: Monad n => (a -> n b) -> Loom n n a b +bind k = Loom (Identity ()) (runIdentity >=> k) +{-# INLINE bind #-} + +-- | Lifts a function to a 'Loom'. This is equivalent to: +-- +-- @ +-- 'hoist' ('fmap' f) +-- @ +-- +-- @since 0.1.0.0 +lift :: Functor m => (a -> b) -> Loom m m a b +lift f = Loom (Identity ()) (fmap f . runIdentity) +{-# INLINE lift #-} + +-- | Constructs a 'Loom' from a natural transformation. +-- +-- @since 0.1.0.0 +hoist :: (f a -> g b) -> Loom f g a b +hoist eta = Loom (Identity ()) (eta . runIdentity) +{-# INLINE hoist #-} diff --git a/src/Data/Functor/Tree.hs b/src/Data/Functor/Tree.hs new file mode 100644 --- /dev/null +++ b/src/Data/Functor/Tree.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} + +-- | +-- +-- @since 0.1.0.0 +module Data.Functor.Tree + ( -- * Rose Trees + Tree (Node), + rootOf, + leavesOf, + + -- ** Construction + pattern (:-), + pattern Leaf, + + -- ** Destruction + flatten, + + -- ** Maps + mapWithRoot, + + -- ** Folds + breadth, + mergeWith, + mergeS, + levels, + ) +where + +import Control.Applicative (Applicative (liftA2)) + +import Control.Applicative.Queue (later, now, runQueue) +import Data.Tree (Tree (Node), flatten) + +infixr 5 :- + +-- --------------------------------------------------------------------------------------------------------------------- + +pattern (:-) :: a -> [Tree a] -> Tree a +pattern x :- xs = Node x xs + +pattern Leaf :: a -> Tree a +pattern Leaf x = x :- [] + +{-# COMPLETE (:-) #-} + +rootOf :: Tree a -> a +rootOf (x :- _) = x + +leavesOf :: Tree a -> [Tree a] +leavesOf (_ :- xs) = xs + +-- | @'mapWithRoot' f g ts@ maps each element with @g@ given the immediate root above the current element and that +-- element. @f@ is used for the root of the tree since it has no element above itself. +-- +-- @since 0.1.0.0 +mapWithRoot :: (a -> b) -> (a -> a -> b) -> Tree a -> Tree b +mapWithRoot f g (t0 :- ts0) = f t0 :- map (go t0) ts0 + where + go root (t :- ts) = g root t :- map (go t) ts + +breadth :: Applicative f => (a -> f b) -> Tree a -> f (Tree b) +breadth f = runQueue . go + where + go (t :- ts) = liftA2 (:-) (now (f t)) (later (traverse go ts)) + +levels :: Tree a -> [[a]] +levels ts = go ts [] + where + go (x :- xs) (q : qs) = (x : q) : foldr go qs xs + go (x :- xs) [] = [x] : foldr go [] xs + +-- | 'mergeWith' is a zip over trees that does not truncate larger subtrees. +-- +-- @since 0.1.0.0 +mergeWith :: (a -> a -> a) -> Tree a -> Tree a -> Tree a +mergeWith f (Leaf x) (y :- ys) = f x y :- ys +mergeWith f (x :- xs) (Leaf y) = f x y :- xs +mergeWith f (x :- xs) (y :- ys) = f x y :- zipWith (mergeWith f) xs ys + +mergeS :: Semigroup a => Tree a -> Tree a -> Tree a +mergeS = mergeWith (<>) diff --git a/src/Data/Name.hs b/src/Data/Name.hs new file mode 100644 --- /dev/null +++ b/src/Data/Name.hs @@ -0,0 +1,51 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Data.Name + ( Name (Name), + inferName, + ) +where + +import Data.Kind (Type) +import Data.Proxy (Proxy (Proxy)) +import GHC.OverloadedLabels (IsLabel (fromLabel)) +import GHC.TypeLits (KnownSymbol, Symbol, symbolVal) +import Prettyprinter (Pretty, pretty) + +-- ------------------------------------------------------------------------------------------------- + +-- | 'Name' is the type of spectacle names. Using the OverloadedLabels syntax should be used to +-- construct 'Name's. +-- +-- @ +-- >>> :set -XOverloadedLabels -XPartialTypeSignatures +-- >>> :t #myVar :: 'Name' _ +-- >>> #myVar :: Name _ :: Name "myVar" +-- @ +-- +-- @since 0.1.0.0 +data Name :: Symbol -> Type where + Name :: KnownSymbol s => Proxy s -> Name s + +-- | @since 0.1.0.0 +instance (KnownSymbol s, l ~ s) => IsLabel l (Name s) where + -- The @l ~ s@ unification immediately solves @nm@ so that 'IsLabel' doesn't leave it ambiguous + -- with a wanted constraint. + fromLabel = Name Proxy + +-- | @since 0.1.0.0 +instance Show (Name s) where + show (Name p) = symbolVal p + +-- | @since 0.1.0.0 +instance Pretty (Name s) where + pretty name = "#" <> pretty (show name) + +-- | @since 0.1.0.0 +instance Eq (Name s) where + -- Nominal equality + _ == _ = True + +inferName :: KnownSymbol s => Name s +inferName = Name Proxy +{-# INLINE CONLIKE inferName #-} diff --git a/src/Data/Node.hs b/src/Data/Node.hs new file mode 100644 --- /dev/null +++ b/src/Data/Node.hs @@ -0,0 +1,48 @@ +module Data.Node + ( Node (Leaf, (:*:)), + ) +where + +import Data.Kind (Type) +import GHC.Base (Applicative (liftA2)) + +-- --------------------------------------------------------------------------------------------------------------------- + +infixr 5 :*: + +data Node :: Type -> Type where + Leaf :: !a -> Node a + (:*:) :: Node a -> Node a -> Node a + deriving (Show) + +-- | @since 0.1.0.0 +instance Functor Node where + fmap f (Leaf x) = Leaf (f x) + fmap f (xs :*: ys) = fmap f xs :*: fmap f ys + {-# INLINE fmap #-} + +-- | @since 0.1.0.0 +instance Applicative Node where + pure = Leaf + {-# INLINE CONLIKE pure #-} + + Leaf f <*> xs = fmap f xs + fs :*: gs <*> xs = (fs <*> xs) :*: (gs <*> xs) + {-# INLINE (<*>) #-} + +-- | @since 0.1.0.0 +instance Semigroup (Node a) where + (<>) = (:*:) + {-# INLINE CONLIKE (<>) #-} + +-- | @since 0.1.0.0 +instance Foldable Node where + foldMap f (Leaf x) = f x + foldMap f (xs :*: ys) = foldMap f xs <> foldMap f ys + {-# INLINE foldMap #-} + +-- | @since 0.1.0.0 +instance Traversable Node where + traverse f (Leaf x) = fmap Leaf (f x) + traverse f (xs :*: ys) = liftA2 (:*:) (traverse f xs) (traverse f ys) + {-# INLINE traverse #-} diff --git a/src/Data/Type/List.hs b/src/Data/Type/List.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/List.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | +-- +-- @since 0.1.0.0 +module Data.Type.List + ( type (++), + ) +where + +infix 5 ++ + +-- --------------------------------------------------------------------------------------------------------------------- + +type (++) :: [k] -> [k] -> [k] +type family xs ++ ys where + '[] ++ ys = ys + (x ': xs) ++ ys = x ': (xs ++ ys) diff --git a/src/Data/Type/Rec.hs b/src/Data/Type/Rec.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Rec.hs @@ -0,0 +1,223 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Type.Rec + ( -- * Extensible Records Transformer + RecF (NilF, ConF), + getF, + setF, + + -- ** Construction + concatF, + + -- ** Maps + mapF, + sequenceF, + + -- ** Destruction + foldMapF, + + -- ** Pretty Printing + ppRecListed, + + -- * Extensible Records + Rec, + pattern Nil, + pattern Con, + get, + set, + + -- * Record Dictionaries + Evident (Evident, Trivial), + pattern NilE, + pattern ConE, + + -- * HasDict + HasDict, + evident, + + -- * Has + Has, + + -- * Re-export + module Data.Ascript, + module Data.Name, + ) +where + +import Control.Applicative (liftA2) +import Data.Functor.Identity (Identity (Identity, runIdentity)) +import Data.Hashable (Hashable (hashWithSalt), hashWithSalt) +import Data.Kind (Constraint, Type) +import Data.List (intercalate) +import GHC.TypeLits (KnownSymbol, Symbol) +import Prettyprinter (Doc, pretty, viaShow, (<+>)) +import Prettyprinter.Render.Terminal (AnsiStyle) + +import Data.Ascript (Ascribe, type (#)) +import Data.Name (Name, inferName) +import Data.Type.List (type (++)) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Extensible record transformer. +-- +-- @since 0.1.0.0 +data RecF :: (k -> Type) -> [Ascribe Symbol k] -> Type where + NilF :: RecF f '[] + ConF :: Name s -> f a -> RecF f ctx -> RecF f (s # a ': ctx) + +sequenceF :: Applicative f => RecF f ctx -> f (Rec ctx) +sequenceF NilF = pure Nil +sequenceF (ConF name field xs) = liftA2 (Con name) field (sequenceF xs) + +mapF :: (forall s a. Name s -> f a -> g a) -> RecF f ctx -> RecF g ctx +mapF _ NilF = NilF +mapF f (ConF name field xs) = ConF name (f name field) (mapF f xs) + +foldMapF :: Monoid m => (forall s a. Name s -> f a -> m) -> RecF f ctx -> m +foldMapF _ NilF = mempty +foldMapF k (ConF name field xs) = k name field <> foldMapF k xs + +concatF :: RecF f ctx -> RecF f ctx' -> RecF f (ctx ++ ctx') +concatF NilF ys = ys +concatF (ConF name x xs) ys = ConF name x (concatF xs ys) + +ppRecListed :: HasDict Show ctx => Rec ctx -> [Doc AnsiStyle] +ppRecListed rs = + case evident @Show rs of + ConE n x xs -> pretty n <+> "=" <+> viaShow x : ppRecListed xs + NilE -> [] + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'Rec' is an extensible record. +-- +-- @since 0.1.0.0 +type Rec ctx = RecF Identity ctx + +-- | A synonym of 'NilT' specialize to 'Rec'. +-- +-- @since 0.1.0.0 +pattern Nil :: () => '[] ~ ctx => Rec ctx +pattern Nil = NilF + +-- | A synonym of 'ConT' specialize to 'Rec'. +-- +-- @since 0.1.0.0 +pattern Con :: () => (s # a ': xs) ~ ctx => Name s -> a -> Rec xs -> Rec ctx +pattern Con name field xs = ConF name (Identity field) xs + +{-# COMPLETE Nil, Con #-} + +-- | @since 0.1.0.0 +instance HasDict Eq ctx => Eq (Rec ctx) where + -- Nominal equality + Nil == Nil = True + (evident @Eq -> ConE _ x xs) == (evident @Eq -> ConE _ y ys) + | x == y = xs == ys + | otherwise = False + +-- | @since 0.1.0.0 +instance HasDict Show ctx => Show (Rec ctx) where + show Nil = "Rec {}" + show rs@Con {} = "Rec {" ++ intercalate "; " (go $ evident rs) ++ "}" + where + go :: forall x. Evident Show x -> [String] + go NilE = [] + go (ConE name field xs) = (show name ++ " = " ++ show field) : go (evident @Show xs) + +-- | @since 0.1.0.0 +instance HasDict Hashable ctx => Hashable (Rec ctx) where + hashWithSalt salt rs = case evident @Hashable rs of + NilE -> salt + ConE _ x xs -> hashWithSalt (hashWithSalt salt x) xs + +set :: Has s a ctx => Name s -> a -> Rec ctx -> Rec ctx +set name x = setF name (Identity x) + +get :: Has s a ctx => Name s -> Rec ctx -> a +get n r = runIdentity (getF n r) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | @'Evident' c ctx@ captures dictionary evidence of @Rec ctx@ for the typeclass @c@. +-- +-- @since 0.1.0.0 +data Evident :: (Type -> Constraint) -> [Ascribe Symbol Type] -> Type where + Trivial :: Evident c '[] + Evident :: (c a, HasDict c ctx) => Rec (s # a ': ctx) -> Evident c (s # a ': ctx) + +-- | A synonym of 'Nil' specialize to 'Evident'. +-- +-- @since 0.1.0.0 +pattern NilE :: () => '[] ~ ctx => Evident c ctx +pattern NilE = Trivial + +-- | A synonym of 'Con' specialize to 'Evident'. +-- +-- @since 0.1.0.0 +pattern ConE :: () => (c a, HasDict c xs, (s # a ': xs) ~ ctx) => Name s -> a -> Rec xs -> Evident c ctx +pattern ConE name field xs = Evident (Con name field xs) + +{-# COMPLETE NilE, ConE #-} + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | @'HasDict' c ctx@ is what it means for a @Rec ctx@ to be an instance of @c@. +-- +-- * @Rec CNil@ trivially fulfills any constraint. +-- +-- * @Rec (x :< ctx)@ fulfills @c@ iff. @c a@ and @HasDict c (Rec ctx)@ are fulfilled. +-- +-- @since 0.1.0.0 +class HasDict c ctx where + evident :: Rec ctx -> Evident c ctx + +-- | @since 0.1.0.0 +instance HasDict c '[] where + evident = const Trivial + {-# INLINE CONLIKE evident #-} + +-- | @since 0.1.0.0 +instance (c a, HasDict c ctx) => HasDict c (s # a ': ctx) where + evident = Evident + {-# INLINE CONLIKE evident #-} + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | @'Has' s a ctx@ is the constraint that a @'Rec' ctx@ have a field @s@ of type @a@. +-- +-- @since 0.1.0.0 +class Has s a ctx | ctx s -> a where + getF :: Name s -> RecF f ctx -> f a + + setF :: Name s -> f a -> RecF f ctx -> RecF f ctx + +-- | @since 0.1.0.0 +instance {-# OVERLAPS #-} Has s a (s # a ': ctx) where + getF _ (ConF _ x _) = x + + setF _ x (ConF name _ r) = ConF name x r + +-- | @since 0.1.0.0 +instance Has s a ctx => Has s a (s' # a' ': ctx) where + getF name (ConF _ _ r) = getF name r + + setF name x (ConF name' y r) = ConF name' y (setF name x r) + +-- | +-- +-- @since 0.1.0.0 +class ReflectRow ctx where + repeatRow :: (forall a. f a) -> RecF f ctx + +-- | @since 0.1.0.0 +instance ReflectRow '[] where + repeatRow _ = NilF + +-- | @since 0.1.0.0 +instance (KnownSymbol s, ReflectRow xs) => ReflectRow (s # x ': xs) where + repeatRow x = ConF inferName x (repeatRow x) diff --git a/src/Data/World.hs b/src/Data/World.hs new file mode 100644 --- /dev/null +++ b/src/Data/World.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.World + ( -- * Worlds + World (World), + + -- ** Construction + makeWorld, + + -- ** Lenses + fingerprint, + worldValues, + + -- ** Pretty Printing + ppWorldListed, + ) +where + +import Data.Hashable (Hashable (hashWithSalt)) +import Lens.Micro (Lens', SimpleGetter, lens, to) +import Prettyprinter (Doc, annotate, indent, pretty) +import Prettyprinter.Render.Terminal (AnsiStyle, Color (White, Yellow), color, colorDull) + +import Data.Fingerprint (Fingerprint (Fingerprint), fingerprintRec) +import Data.Type.Rec (HasDict, Rec, ppRecListed) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | The 'World' data type is a 'Rec', which is used to represent the concrete values of a model's state, paired with +-- it's 'Fingerprint' which has much faster preformance charateristics for comparison. +-- +-- @since 1.0.0 +data World ctx = World + { _worldFingerprint :: {-# UNPACK #-} !Fingerprint + , _worldValues :: Rec ctx + } + +-- | @since 1.0.0 +instance Eq (World ctx) where + World fp1 _ == World fp2 _ = fp1 == fp2 + {-# INLINE (==) #-} + +-- | @since 1.0.0 +instance Ord (World ctx) where + World fp1 _ `compare` World fp2 _ = fp1 `compare` fp2 + {-# INLINE compare #-} + +-- | @since 1.0.0 +instance Show (Rec ctx) => Show (World ctx) where + show (World fp w) = "<<" ++ show fp ++ ":" ++ show w ++ ">>" + {-# INLINE show #-} + +-- | @since 1.0.0 +instance Hashable (World ctx) where + hashWithSalt salt (World (Fingerprint fp) _) = hashWithSalt salt fp + {-# INLINE hashWithSalt #-} + +-- | Constructs a 'World' type from the given 'Rec'. +-- +-- @since 1.0.0 +makeWorld :: Hashable (Rec ctx) => Rec ctx -> World ctx +makeWorld w = World (fingerprintRec w) w + +-- | Lens focusing on a 'World's fingerprint. +-- +-- @since 1.0.0 +fingerprint :: Lens' (World ctx) Fingerprint +fingerprint = lens _worldFingerprint \World {..} x -> World {_worldFingerprint = x, ..} + +-- | Lens focusing on the 'Rec' holding the concrete values of a 'World'. +-- +-- @since 1.0.0 +worldValues :: SimpleGetter (World ctx) (Rec ctx) +worldValues = to _worldValues + +-- | @'ppWorldListed' world@ lays out a list of documents for each state variable in @world@ using the world fingerprint +-- as a header. +-- +-- @since 1.0.0 +ppWorldListed :: HasDict Show ctx => World ctx -> [Doc AnsiStyle] +ppWorldListed (World hash values) = + let hashDoc = annotate (colorDull Yellow) (pretty hash) + fieldDocs = annotate (color White) <$> ppRecListed values + in hashDoc : map (indent 2) fieldDocs diff --git a/src/Language/Spectacle.hs b/src/Language/Spectacle.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle.hs @@ -0,0 +1,89 @@ +module Language.Spectacle + ( -- * CLI Interaction + interaction, + + -- * Model Checking + modelcheck, + modeltrace, + + -- * Specification + Specification (Specification), + specInit, + specNext, + specProp, + ActionType (ActionSF, ActionWF, ActionUF), + TemporalType (PropF, PropG, PropGF, PropFG), + Fairness (StrongFair, WeakFair, Unfair), + Modality (Always, Eventually, Infinitely, Stays), + + -- * Syntax + type Action, + type Temporal, + + -- ** Variables + plain, + prime, + type (#), + + -- ** Operators + (.=), + enabled, + throwE, + catchE, + + -- ** Logic + forall, + exists, + oneOf, + conjunct, + (/\), + disjunct, + (\/), + complement, + (==>), + implies, + (<=>), + iff, + + -- * Records + pattern ConF, + pattern NilF, + ) +where + +import Data.Type.Rec (RecF (ConF, NilF), type (#)) +import Language.Spectacle.AST (Action, Temporal) +import Language.Spectacle.Fairness (Fairness (StrongFair, Unfair, WeakFair)) +import Language.Spectacle.Interaction (interaction) +import Language.Spectacle.Model (modelcheck, modeltrace) +import Language.Spectacle.Specification + ( ActionType (ActionSF, ActionUF, ActionWF), + Modality (Always, Eventually, Infinitely, Stays), + Specification (Specification), + TemporalType (PropF, PropFG, PropG, PropGF), + specInit, + specNext, + specProp, + ) +import Language.Spectacle.Syntax + ( catchE, + complement, + conjunct, + disjunct, + enabled, + exists, + forall, + iff, + implies, + oneOf, + plain, + prime, + throwE, + (.=), + (/\), + (<=>), + (==>), + (\/), + ) + +-- --------------------------------------------------------------------------------------------------------------------- diff --git a/src/Language/Spectacle/AST.hs b/src/Language/Spectacle/AST.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/AST.hs @@ -0,0 +1,15 @@ +module Language.Spectacle.AST + ( -- * Actions + type Action, + runAction, + + -- * Relations + type Temporal, + runTemporal, + ) +where + +import Language.Spectacle.AST.Action (Action, runAction) +import Language.Spectacle.AST.Temporal (Temporal, runTemporal) + +-- --------------------------------------------------------------------------------------------------------------------- diff --git a/src/Language/Spectacle/AST/Action.hs b/src/Language/Spectacle/AST/Action.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/AST/Action.hs @@ -0,0 +1,211 @@ +module Language.Spectacle.AST.Action + ( -- * Temporal Actions + type Action, + type ActionSyntax, + + -- ** Interpreters + runAction, + runExceptionalAction, + rewriteLogic, + applyComplement, + introduceEnv, + ) +where + +import Data.Either (fromRight) +import Data.Function ((&)) +import Data.Hashable (Hashable) +import Data.Kind (Type) +import Data.Set (Set) +import qualified Data.Set as Set +import GHC.TypeLits (Symbol) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Data.Type.Rec (Ascribe, Rec) +import Data.World (World, makeWorld) +import Language.Spectacle.Exception.RuntimeException + ( RuntimeException, + ) +import Language.Spectacle.Lang + ( EffectK, + Lang (Op, Pure, Scoped), + Member (projectS), + Members, + Op (OHere, OThere), + Scoped (SHere, SThere), + runLang, + ) +import Language.Spectacle.RTS.Registers (RuntimeState, emptyRuntimeState, newValues) +import Language.Spectacle.Syntax.Closure + ( Closure, + runActionClosure, + ) +import Language.Spectacle.Syntax.Env (Env, runEnv) +import Language.Spectacle.Syntax.Error (Error, runError) +import Language.Spectacle.Syntax.Logic + ( Effect (Complement, Conjunct, Disjunct), + Logic, + complement, + conjunct, + disjunct, + runLogic, + ) +import Language.Spectacle.Syntax.NonDet (NonDet, runNonDetA) +import Language.Spectacle.Syntax.Plain (Plain, runPlain) +import Language.Spectacle.Syntax.Quantifier + ( Effect (Exists, Forall), + Quantifier, + exists, + forall, + runExceptionalQuantifier, + runQuantifier, + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +type Action :: [Ascribe Symbol Type] -> Type -> Type +type Action ctx = Lang ctx ActionSyntax + +type ActionSyntax :: [EffectK] +type ActionSyntax = + -- NOTE: 'Closure' must be handled before 'Quantifier'. If 'Quantifier' discharged before 'Closure', erroneous values + -- are produced from any 'Closure' nested within a forall/exists. + '[ Logic + , Closure + , Quantifier + , Plain + , NonDet + , Error RuntimeException + ] + +-- | Completely evaluate a temporal action yielding either a 'RuntimeException' or a collection of new worlds accessible +-- by the action given. +-- +-- @since 1.0.0 +runExceptionalAction :: + forall ctxt. + Hashable (Rec ctxt) => + Rec ctxt -> + Action ctxt Bool -> + Either RuntimeException (Set (World ctxt)) +runExceptionalAction knowns action = do + states <- + action + & introduceEnv + & rewriteLogic + & runLogic + & runActionClosure + & runExceptionalQuantifier + & runEnv (emptyRuntimeState knowns) + & runPlain knowns + & runNonDetA + & runError + & runLang + + return (takeRelatedSet states) + where + takeRelatedSet :: [(RuntimeState ctxt, Bool)] -> Set (World ctxt) + takeRelatedSet = foldMap \(rst, rel) -> + if rel + then Set.singleton (makeWorld (newValues rst)) + else Set.empty +{-# INLINE runExceptionalAction #-} + +runAction :: + forall ctxt. + Hashable (Rec ctxt) => + Rec ctxt -> + Action ctxt Bool -> + Set (World ctxt) +runAction knowns action = + let states = + action + & introduceEnv + & rewriteLogic + & runLogic + & runActionClosure + & runQuantifier + & runEnv (emptyRuntimeState knowns) + & runPlain knowns + & runNonDetA + & runError + & runLang + & fromRight [] + in takeRelatedSet states + where + takeRelatedSet :: [(RuntimeState ctxt, Bool)] -> Set (World ctxt) + takeRelatedSet = foldMap \(rst, rel) -> + if rel + then Set.singleton (makeWorld (newValues rst)) + else Set.empty +{-# INLINE runAction #-} + +-- | Traverses the effects in an action, rewriting all logical operators and quantifiers scoped within a negation. +-- +-- @since 1.0.0 +rewriteLogic :: Members '[Logic, Quantifier, NonDet] effs => Lang ctx effs Bool -> Lang ctx effs Bool +rewriteLogic = \case + Pure x -> pure x + Op op k -> Op op (rewriteLogic . k) + Scoped scoped loom -> case projectS scoped of + Nothing -> Scoped scoped loom' + Just eff + | Complement m <- eff -> runLoom (loom ~>~ hoist applyComplement ~>~ hoist rewriteLogic) m + | otherwise -> Scoped scoped loom' + where + loom' = loom ~>~ hoist rewriteLogic +{-# INLINE rewriteLogic #-} + +-- | Reduces logical negation by applying the usual rewrite rules to quantifiers and other logical operators scoped +-- within the negation. +-- +-- @since 1.0.0 +applyComplement :: Members '[Logic, Quantifier, NonDet] effs => Lang ctx effs Bool -> Lang ctx effs Bool +applyComplement = \case + Pure x -> pure x + Op op k -> Op op (applyComplement . k) + Scoped scoped loom -> case projectS scoped of + Nothing -> case projectS scoped of + Nothing -> Scoped scoped loom' + -- ¬ (∀ x : A → p x) ≡ ∃ x : A → ¬ (p x) + Just (Forall xs p) -> exists xs (fmap not . runLoom loom' . p) + -- ¬ (∃ x : A → p x) ≡ ∀ x : A → ¬ (p x) + Just (Exists xs p) -> forall xs (fmap not . runLoom loom' . p) + -- ¬ ¬ p ≡ p + Just (Complement m) -> runLoom loom' (fmap not m) + -- ¬ (p ∧ q) ≡ ¬ p ∨ ¬ q + Just (Conjunct lhs rhs) -> + let lhs' = runLoom loom' lhs + rhs' = runLoom loom' rhs + in disjunct (complement lhs') (complement rhs') + -- ¬ (p ∨ q) ≡ ¬ p ∧ ¬ q + Just (Disjunct lhs rhs) -> + let lhs' = runLoom loom' lhs + rhs' = runLoom loom' rhs + in conjunct (complement lhs') (complement rhs') + where + loom' = loom ~>~ hoist applyComplement +{-# INLINE applyComplement #-} + +-- | Introduces the variable environment to an 'Action' "underneath" the 'Closure' effect. +-- +-- @since 1.0.0 +introduceEnv :: + Lang ctx (Logic ': Closure ': Quantifier ': effs) a -> + Lang ctx (Logic ': Closure ': Quantifier ': Env ': effs) a +introduceEnv = \case + Pure x -> pure x + Op op k + | OHere op' <- op -> Op (OHere op') k' + | OThere (OHere op') <- op -> Op (OThere (OHere op')) k' + | OThere (OThere (OHere op')) <- op -> Op (OThere (OThere (OHere op'))) k' + | OThere (OThere (OThere op')) <- op -> Op (OThere (OThere (OThere (OThere op')))) k' + where + k' = introduceEnv . k + Scoped scoped loom + | SHere scoped' <- scoped -> Scoped (SHere scoped') loom' + | SThere (SHere scoped') <- scoped -> Scoped (SThere (SHere scoped')) loom' + | SThere (SThere (SHere scoped')) <- scoped -> Scoped (SThere (SThere (SHere scoped'))) loom' + | SThere (SThere (SThere scoped')) <- scoped -> Scoped (SThere (SThere (SThere (SThere scoped')))) loom' + where + loom' = loom ~>~ hoist introduceEnv diff --git a/src/Language/Spectacle/AST/Temporal.hs b/src/Language/Spectacle/AST/Temporal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/AST/Temporal.hs @@ -0,0 +1,36 @@ +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.AST.Temporal + ( -- * Temporal Formula Monad + Temporal, + runTemporal, + + -- ** Effect Signature + TemporalSyntax, + ) +where + +import Data.Function ((&)) +import Data.Kind (Type) +import GHC.TypeLits (Symbol) + +import Data.Type.Rec (Ascribe, Rec) +import Language.Spectacle.Lang (EffectK, Lang, runLang) +import Language.Spectacle.Syntax.Plain (Plain, runPlain) +import Language.Spectacle.Syntax.Prime (Prime, substPrime) + +-- --------------------------------------------------------------------------------------------------------------------- + +type Temporal :: [Ascribe Symbol Type] -> Type -> Type +type Temporal ctx = Lang ctx TemporalSyntax + +type TemporalSyntax :: [EffectK] +type TemporalSyntax = '[Prime, Plain] + +runTemporal :: Rec ctx -> Rec ctx -> Temporal ctx Bool -> Bool +runTemporal unprimed primed temporal = + temporal + & substPrime primed + & runPlain unprimed + & runLang diff --git a/src/Language/Spectacle/Exception/RuntimeException.hs b/src/Language/Spectacle/Exception/RuntimeException.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Exception/RuntimeException.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE DeriveAnyClass #-} + +module Language.Spectacle.Exception.RuntimeException + ( RuntimeException (VariableException, QuantifierException, UserException), + VariableException (CyclicReference, Uninitialized), + QuantifierException (ForallViolated, ExistsViolated), + ) +where + +import Control.Exception (Exception) +import Type.Reflection (Typeable) + +-- --------------------------------------------------------------------------------------------------------------------- + +data RuntimeException where + VariableException :: + VariableException -> + RuntimeException + QuantifierException :: + QuantifierException -> + RuntimeException + UserException :: + String -> + RuntimeException + deriving stock (Show, Typeable) + deriving anyclass (Exception) + +data VariableException where + CyclicReference :: [String] -> VariableException + Uninitialized :: String -> VariableException + deriving stock (Show, Typeable) + deriving anyclass (Exception) + +data QuantifierException where + -- | 'ForallViolated' is thrown when a universally quantified set has one or more values that do not satisfy the + -- predicate given to 'forall'. + -- + -- @ + -- myAct :: Action '[] Bool + -- myAct = forall [2] odd + -- @ + -- + -- would throw 'ForallViolated' since 2 is not 'odd'. + -- + -- @since 1.0.0 + ForallViolated :: + QuantifierException + -- | 'ExistsViolated' is thrown when an existentially quantified set has no values that satisfy its predicate, + -- e.g. the expression + -- + -- @ + -- myAct :: Action '[] Bool + -- myAct = exists [2, 4] odd + -- @ + -- + -- would throw 'ExistsViolated' since there is no number @n in {2, 4}@ such that @'odd' n ≡ 'True'@ + -- + -- @since 1.0.0 + ExistsViolated :: + QuantifierException + deriving stock (Show, Typeable) + deriving anyclass (Exception) diff --git a/src/Language/Spectacle/Fairness.hs b/src/Language/Spectacle/Fairness.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Fairness.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeFamilyDependencies #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Fairness + ( -- * Fairness + Fairness (Unfair, WeakFair, StrongFair), + + -- ** Reification + reifyFairness, + ) +where + +import Data.Proxy (Proxy (Proxy)) +import Type.Reflection (Typeable, someTypeRep) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Enumerated fairness constraints. +-- +-- @since 1.0.0 +data Fairness + = Unfair + | WeakFair + | StrongFair + deriving (Enum, Eq, Ord, Show, Typeable) + +-- | Reifies a promoted 'Fairness' constructor. +-- +-- @since 1.0.0 +reifyFairness :: forall (x :: Fairness). Typeable x => Fairness +reifyFairness + | actualTyCon == strongTyCon = StrongFair + | actualTyCon == weakTyCon = WeakFair + | otherwise = Unfair + where + actualTyCon = someTypeRep (Proxy @x) + strongTyCon = someTypeRep (Proxy @ 'StrongFair) + weakTyCon = someTypeRep (Proxy @ 'WeakFair) diff --git a/src/Language/Spectacle/Interaction.hs b/src/Language/Spectacle/Interaction.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction.hs @@ -0,0 +1,59 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | CLI interaction. +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction + ( -- * CLI + interaction, + handleInteraction, + ) +where + +import Control.Monad (when) +import Control.Monad.IO.Class (liftIO) +import Control.Monad.Reader (asks) +import Data.Either (isRight) +import Data.Hashable (Hashable) +import Data.Text.Prettyprint.Doc (line) + +import Data.Functor.Tree (Tree) +import Data.Type.Rec (HasDict) +import Data.World (World) +import Language.Spectacle.Interaction.CLI (CLI, ContextCLI (ctxOpts), cliPutDoc, cliResultDoc, runCLI) +import Language.Spectacle.Interaction.Diagram (diagramFull, runDiagram) +import Language.Spectacle.Interaction.Options (OptsCLI (optsLogGraph, optsOnlyTrace)) +import qualified Language.Spectacle.Interaction.Options as Opts +import Language.Spectacle.Interaction.Paths (toPointSet) +import Language.Spectacle.Model (modelcheck, modeltrace) +import Language.Spectacle.Model.ModelError (ModelError, ppModelError) +import Language.Spectacle.Specification (Specification) + +-- --------------------------------------------------------------------------------------------------------------------- + +interaction :: (HasDict Hashable ctx, HasDict Show ctx) => Specification ctx acts form -> IO () +interaction spec = do + opts <- Opts.execOptsCLI + result <- + if optsOnlyTrace opts + then modeltrace spec + else modelcheck spec + + runCLI (handleInteraction result) opts + +handleInteraction :: HasDict Show ctx => Either (ModelError ctx) [Tree (World ctx)] -> CLI () +handleInteraction result = + let status = isRight result + in case result of + Left err -> do + cliPutDoc =<< cliResultDoc status + cliPutDoc (ppModelError err) + cliPutDoc line + Right trees -> do + isLogging <- asks (optsLogGraph . ctxOpts) + when isLogging do + let pointSet = foldMap toPointSet trees + diagramDoc <- liftIO (runDiagram $ diagramFull pointSet) + cliPutDoc (diagramDoc <> line) + cliPutDoc =<< cliResultDoc status diff --git a/src/Language/Spectacle/Interaction/CLI.hs b/src/Language/Spectacle/Interaction/CLI.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/CLI.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE OverloadedStrings #-} + +-- | This module exports the 'CLI' monad, an abstraction over command-line interactions such as emitting logs and +-- messages from the model checker per options declared by a user. +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction.CLI + ( -- * The CLI Monad + CLI (CLI), + unCLI, + + -- ** Running CLI + runCLI, + + -- ** CLI Operations + cliPutDoc, + + -- ** CLI Documents + cliResultDoc, + + -- * CLI Context + ContextCLI (ContextCLI), + ctxOpts, + ctxHandle, + + -- ** Construction + newContextCLI, + ) +where + +import Control.Monad (unless) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Reader (MonadReader, ReaderT, asks, runReaderT) +import Prettyprinter (Doc, annotate, line, unAnnotate, (<+>)) +import Prettyprinter.Render.Terminal (AnsiStyle, Color (Green, Red), bold, color, hPutDoc) +import System.IO (Handle, hClose) + +import Language.Spectacle.Interaction.Options (OptsCLI, isStdout, optsLogOutput, optsOnlyTrace) +import qualified Language.Spectacle.Interaction.Options as Opts + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | The 'CLI' monad is a @'ReaderT' 'IO'@ carrying context of command-line options. +-- +-- @since 1.0.0 +newtype CLI a = CLI + {unCLI :: ReaderT ContextCLI IO a} + deriving stock (Functor) + deriving + (Applicative, Monad, MonadIO, MonadReader ContextCLI) + via ReaderT ContextCLI IO + +-- | Lower 'CLI' into 'IO' given command-line options. +-- +-- @since 1.0.0 +runCLI :: CLI a -> OptsCLI -> IO a +runCLI cli opts = do + ctx <- newContextCLI opts + ret <- runReaderT (unCLI cli) ctx + + unless (Opts.isStdout $ optsLogOutput opts) do + -- Close the handle to the log-output buffer created by + -- 'newContextCLI'/'handleFrom' after the command-line + -- interaction has been completed, if the handle was not + -- to System.IO.stdout + hClose (ctxHandle ctx) + + pure ret + +-- | @'cliPutDoc' doc@ emits the given @doc@ using CLI context's buffer handle. +-- +-- @since 1.0.0 +cliPutDoc :: Doc AnsiStyle -> CLI () +cliPutDoc doc = do + handle <- asks ctxHandle + output <- asks (optsLogOutput . ctxOpts) + if isStdout output + then liftIO do + hPutDoc handle doc + else liftIO do + -- Clear 'AnsiStyle' annotations from the 'Doc' for + -- buffers other than stdout, since they can not be + -- rendered by the terminal. + hPutDoc handle (unAnnotate doc) + +-- | @'cliResultDoc' succeeded@ for a boolean flag @succeeded@ indicating if the model checker encountered an error or +-- not, lays out the document containing: +-- +-- * The type of run the model checker took (either "model check" or "trace"). +-- * The result of the run (either "success" or "failure") +-- +-- @since 1.0.0 +cliResultDoc :: Bool -> CLI (Doc AnsiStyle) +cliResultDoc succeeded = do + runType <- asks (mkRunTypeDoc . ctxOpts) + pure ("specification:" <+> runType <> ":" <+> resultDoc <> line) + where + mkRunTypeDoc opts + | optsOnlyTrace opts = "trace" + | otherwise = "model check" + + resultDoc + | succeeded = annotate (bold <> color Green) "success" + | otherwise = annotate (bold <> color Red) "failure" + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'ContextCLI' is the collection frequently needed information for command-line interaction. +-- +-- Note: the preferred method of construction for 'ContextCLI' is via 'newContextCLI'. +-- +-- @since 1.0.0 +data ContextCLI = ContextCLI + { ctxOpts :: OptsCLI + , ctxHandle :: Handle + } + deriving stock (Show) + +-- | Constructs a 'ContextCLI' from a set of command-line options 'OptsCLI'. +-- +-- @since 1.0.0 +newContextCLI :: OptsCLI -> IO ContextCLI +newContextCLI opts = ContextCLI opts <$> Opts.handleFrom (optsLogOutput opts) +{-# INLINE newContextCLI #-} diff --git a/src/Language/Spectacle/Interaction/Diagram.hs b/src/Language/Spectacle/Interaction/Diagram.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/Diagram.hs @@ -0,0 +1,361 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +module Language.Spectacle.Interaction.Diagram where + +import Control.Applicative (liftA2) +import Control.Arrow (Kleisli (Kleisli)) +import Control.Comonad (Comonad (duplicate)) +import Control.Comonad.Store (extract) +import Data.Foldable (Foldable (fold)) +import Data.IORef (IORef, newIORef, readIORef, writeIORef) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap +import Data.Maybe () +import qualified Data.Sequence as Seq +import Data.Set (Set) +import qualified Data.Set as Set +import Lens.Micro ((^.)) +import Lens.Micro.Extras (view) +import Prettyprinter (Doc, pretty) +import qualified Prettyprinter as Doc +import qualified Prettyprinter.Internal as Doc.Internal +import Prettyprinter.Render.Terminal (AnsiStyle, Color (Blue, Cyan, Green, Magenta, Red, Yellow)) +import qualified Prettyprinter.Render.Terminal as Doc + +import Control.Comonad.Tape (Tape (Tape), after, before, focus, tabulatel, tabulater, viewl) +import Data.Fingerprint (Fingerprint) +import Data.Traversable (for) +import Language.Spectacle.Interaction.Doc + ( Cardinal (CLeft, CRight), + cline, + hline, + tab, + tack, + turnLeftUp, + turnRightUp, + turnUpLeft, + turnUpRight, + ) +import qualified Language.Spectacle.Interaction.Doc as Doc +import Language.Spectacle.Interaction.Paths (takeMinRow) +import Language.Spectacle.Interaction.Point (Point, column, extent, fields, label, parent) + +-- --------------------------------------------------------------------------------------------------------------------- + +data LogNode = LogNode + { nodeColor :: Color + , nodeLabel :: Fingerprint + } + +-- | @'traverseRowsOf' f ps@ is a traversal of @f@ on rows of @ps@, collecting the results in a list. +-- +-- @since 1.0.0 +traverseRowsOf :: (Set Point -> DiagramM a) -> Set Point -> DiagramM [a] +traverseRowsOf f ps = + case takeMinRow ps of + (next, paths') + | Set.null paths' -> pure @[] <$> f next + | otherwise -> liftA2 (:) (f next) (traverseRowsOf f paths') + +diagramFull :: Set Point -> DiagramM (Doc AnsiStyle) +diagramFull points = do + rowDocs <- traverseRowsOf diagramRow points + pure (Doc.concatWith (flip mappend) rowDocs) + +diagramRow :: Set Point -> DiagramM (Doc AnsiStyle) +diagramRow rows = + case viewl (foldMap Seq.singleton rows) of + Nothing -> pure mempty + Just points -> do + branchDoc <- branchSection points + subtreeDoc <- subtreeDiagram points + curveDocs <- curveSection points + return (branchDoc <> Doc.line <> curveDocs <> subtreeDoc) + +subtreeDiagram :: Tape Point -> DiagramM (Doc AnsiStyle) +subtreeDiagram = fmap (foldMap (`mappend` Doc.line)) . traverse pointSection . duplicate + +pointSection :: Tape Point -> DiagramM (Doc AnsiStyle) +pointSection ps = do + lx <- labelSection ps + fs <- fieldSection ps + pure (lx <> Doc.vsep fs) + +-- | @'labelSection' points@ documents the label of the focused points as well as neighboring paths, for example: +-- +-- @ +-- | * | 0x8f46a202 +-- @ +-- +-- @since 1.0.0 +labelSection :: Tape Point -> DiagramM (Doc AnsiStyle) +labelSection ps = do + paths <- labelPaths ps + let lx = Doc.annotate (Doc.colorDull Yellow) (pretty (focus ps ^. label)) + pure (paths <> lx <> Doc.line) + +-- | @'fieldSection' points@ documents each of the fields in the focused point as well a neighboring paths, for example: +-- +-- @ +-- | | | #field1 = "foo" +-- | | | #field2 = 12345 +-- @ +-- +-- @since 1.0.0 +fieldSection :: Tape Point -> DiagramM [Doc AnsiStyle] +fieldSection points = do + paths <- fieldPaths points + let fs = extract points ^. fields + pure (map (mappend paths . Doc.indent 2) fs) + +branchSection :: Tape Point -> DiagramM (Doc AnsiStyle) +branchSection = foldr cons (pure mempty) . duplicate + where + cons points + | focus points ^. extent == 0 = id + | otherwise = liftA2 (<>) (go points) + + go points@Tape {..} = do + doc <- branchSegment points lcol ucol + withColor doc (focus ^. label) + where + lcol = sum (view extent <$> before) + ucol = lcol + focus ^. extent + +curveSection :: Tape Point -> DiagramM (Doc AnsiStyle) +curveSection = foldr cons (pure mempty) . duplicate + where + cons points + | focus points ^. extent == 0 = id + | otherwise = liftA2 (mappend) (go points) + + go points@Tape {..} + | lcol <= col && col < ucol = pure mempty + | otherwise = do + curve <- curveSegment points lcol ucol + withColor (curve <> Doc.line) (focus ^. label) + where + lcol = sum (view extent <$> before) + ucol = lcol + focus ^. extent + col = focus ^. column + +curveSegment :: Tape Point -> Int -> Int -> DiagramM (Doc AnsiStyle) +curveSegment points lcol ucol + | col < lcol = do + let curve = rightTurnSegment (lcol - col) <> turnRightUp + ls <- for (tabulatel points) \ps -> do + if focus ps ^. extent == 0 + then pure tab + else withColor (verticalSegment 1) (focus ps ^. label) + + withColor (fold ls <> curve) lx + | ucol < 1 + col = do + let curve = turnLeftUp <> Doc.copies (2 * (col - ucol) + 1) hline <> turnUpLeft + rs <- for (tabulater points) \ps -> do + if focus ps ^. extent == 0 + then pure tab + else withColor (verticalSegment 1) (focus ps ^. label) + ls <- for (tabulatel points) \ps -> do + if focus ps ^. extent == 0 + then pure mempty + else do + let spc = Doc.tabs (focus ps ^. extent - 1) + doc <- withColor (verticalSegment 1) (focus ps ^. label) + pure (spc <> doc) + + let spc = Doc.tabs (focus points ^. extent - 1) + withColor (fold ls <> spc <> curve <> Doc.space <> fold rs) lx + | otherwise = pure mempty + where + col = focus points ^. column + lx = focus points ^. label + +-- | @'labelPaths' points@ inserts a line segment for each point in @points@, and a asterrisk for the point under +-- focus. +-- +-- @since 1.0.0 +labelPaths :: Tape Point -> DiagramM (Doc AnsiStyle) +labelPaths = iteratePaths (const (pure "* ")) + +-- | @'labelPaths' points@ inserts a line segment for each point in @points@. +-- +-- @since 1.0.0 +fieldPaths :: Tape Point -> DiagramM (Doc AnsiStyle) +fieldPaths = iteratePaths foci + where + foci point = case point ^. parent of + Nothing -> pure tab + Just lx -> withColor (verticalSegment 1) lx + +branchSegment :: Tape Point -> Int -> Int -> DiagramM (Doc AnsiStyle) +branchSegment points lcol ucol + | col <= lcol = pure $ rightFanoutSegment len + | ucol <= 1 + col = pure $ leftFanoutSegment len + | otherwise = do + let ls = leavesSegment (col - lcol - 1) + let rs = leavesSegment (ucol - col - 2) + let fans = Doc.cat [turnLeftUp, hline, ls, cline, Doc.hline, rs, turnRightUp] + pure (fans <> Doc.space) + where + col = focus points ^. column + len = focus points ^. extent + +iteratePaths :: (Point -> DiagramM (Doc AnsiStyle)) -> Tape Point -> DiagramM (Doc AnsiStyle) +iteratePaths f = iterateLine groupBefore f groupAfter + +groupAfter :: Point -> DiagramM (Doc AnsiStyle) +groupAfter point = do + let len = min (point ^. extent) 1 + let lx = point ^. label + withColor (verticalSegment len) lx + +groupBefore :: Point -> DiagramM (Doc AnsiStyle) +groupBefore point = + case point ^. parent of + Nothing -> pure Doc.tab + Just lx -> withColor (verticalSegment 1) lx + +iterateLine :: + (Point -> DiagramM (Doc AnsiStyle)) -> + (Point -> DiagramM (Doc AnsiStyle)) -> + (Point -> DiagramM (Doc AnsiStyle)) -> + Tape Point -> + DiagramM (Doc AnsiStyle) +iterateLine handleLT handleEQ handleGT points = do + lt <- foldr (liftA2 (<>) . handleLT) (pure mempty) (before points) + gt <- foldr (liftA2 (<>) . handleGT) (pure mempty) (after points) + eq <- handleEQ (focus points) + pure (lt <> eq <> gt) + +-- | @'verticalSegment' len@ fills a line of length @len@ comprised of segments "│ ". +-- +-- @since 1.0.0 +verticalSegment :: Int -> Doc AnsiStyle +verticalSegment len + | len <= 0 = Doc.tab + | len == 1 = Doc.Internal.Text 2 "│ " + | otherwise = Doc.copies len (Doc.Internal.Text 2 "│ ") + +leftFanoutSegment :: Int -> Doc AnsiStyle +leftFanoutSegment len + | len <= 0 = mempty + | len == 1 = Doc.Internal.Text 2 "│ " + | otherwise = + let begin = Doc.Internal.Text 2 "╰─" + end = tack CLeft <> Doc.space + in begin <> leavesSegment (len - 2) <> end + +rightFanoutSegment :: Int -> Doc AnsiStyle +rightFanoutSegment len + | len <= 0 = mempty + | len == 1 = Doc.Internal.Text 2 "│ " + | otherwise = + let begin = tack CRight <> Doc.hline + end = Doc.Internal.Text 2 "╯ " + in begin <> leavesSegment (len - 2) <> end + +rightTurnSegment :: Int -> Doc AnsiStyle +rightTurnSegment len + | len <= 0 = mempty + | len == 1 = Doc.Internal.Text 2 "╭─" + | otherwise = turnUpRight <> Doc.copies (2 * len - 1) (Doc.Internal.Char '─') + +-- | @'leavesPaths' len@ fills a line of length @len@ comprised of segments "┴─". +-- +-- @since 1.0.0 +leavesSegment :: Int -> Doc AnsiStyle +leavesSegment len + | len <= 0 = mempty + | len == 1 = Doc.Internal.Text 2 "┴─" + | otherwise = Doc.copies len (Doc.Internal.Text 2 "┴─") + +withColor :: Doc AnsiStyle -> Fingerprint -> DiagramM (Doc AnsiStyle) +withColor doc hash = fmap (\c -> Doc.annotate (Doc.color c) doc) (colorOf hash) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype DiagramM a = DiagramM + {runDiagramM :: IORef DiagramCtx -> IO a} + deriving + (Functor, Applicative, Monad) + via Kleisli IO (IORef DiagramCtx) + +runDiagram :: DiagramM a -> IO a +runDiagram (DiagramM io) = newIORef (DiagramCtx (ColorSrc mempty mempty)) >>= io + +newtype DiagramCtx = DiagramCtx {ctxColorSource :: ColorSrc} + +colorOf :: Fingerprint -> DiagramM Color +colorOf hash = + DiagramM \ref -> do + ctx <- readIORef ref + case lookupColor hash (ctxColorSource ctx) of + Nothing -> do + let (c, cs') = takeColor hash (ctxColorSource ctx) + writeIORef ref ctx {ctxColorSource = cs'} + pure c + Just c -> pure c + +-- --------------------------------------------------------------------------------------------------------------------- + +data ColorSrc = ColorSrc + { srcColorCtx :: {-# UNPACK #-} !ColorCtx + , srcColorMap :: !(IntMap Color) + } + +lookupColor :: Fingerprint -> ColorSrc -> Maybe Color +lookupColor hash (ColorSrc _ cs) = IntMap.lookup (fromIntegral hash) cs + +takeColor :: Fingerprint -> ColorSrc -> (Color, ColorSrc) +takeColor hash (ColorSrc !cctx cmap) = + let c = getColorCtx cctx + cctx' = succ cctx + cmap' = IntMap.insert (fromIntegral hash) c cmap + in (c, ColorSrc cctx' cmap') + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype ColorCtx = ColorCtx Int + deriving (Eq, Ord) + +getColorCtx :: ColorCtx -> Color +getColorCtx (ColorCtx i) = + case mod i 6 of + 0 -> Cyan + 1 -> Red + 2 -> Green + 3 -> Yellow + 4 -> Blue + _ -> Magenta +{-# INLINE getColorCtx #-} + +-- | @since 1.0.0 +instance Semigroup ColorCtx where + -- Note: We use addition in Z mod 6 as the semigroup for 'ColorCtx' since the 'Enum' instance is cycles through 6 + -- colors. + + ColorCtx x <> ColorCtx y = ColorCtx (mod (x + y) 6) + {-# INLINE (<>) #-} + +-- | @since 1.0.0 +instance Monoid ColorCtx where + mempty = ColorCtx 0 + {-# INLINE mempty #-} + +-- | @since 1.0.0 +instance Enum ColorCtx where + -- Note: AnsiStyle have six unique colors that are not black or white (cyan, red, green, yellow, blue and magenta). + -- 'DiagramM' uses this 'Enum' instance and 'succ' to cycle through these six colors since the 'Color' datatype + -- exported does not provide one out of the box. + + toEnum i = ColorCtx (mod i 6) + {-# INLINE toEnum #-} + + fromEnum (ColorCtx i) = mod i 6 + {-# INLINE fromEnum #-} + + succ (ColorCtx i) = ColorCtx (mod (succ i) 6) + {-# INLINE succ #-} diff --git a/src/Language/Spectacle/Interaction/Doc.hs b/src/Language/Spectacle/Interaction/Doc.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/Doc.hs @@ -0,0 +1,163 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction.Doc + ( -- * Direction + Cardinal (CUp, CDown, CLeft, CRight), + + -- * Doc Combinations + sepBy, + hcopies, + copies, + tab, + tabs, + marginr, + marginl, + spaces, + segment, + segmentWith, + hruler, + + -- * Line Characters + vline, + hline, + cline, + + -- * Tack Characters + tack, + + -- * Turn Characters + turnLeftUp, + turnRightUp, + turnUpLeft, + turnUpRight, + ) +where + +import qualified Data.Text as Text +import Prettyprinter (Doc, FusionDepth (Deep)) +import qualified Prettyprinter as Doc +import qualified Prettyprinter.Internal as Doc.Internal + +-- --------------------------------------------------------------------------------------------------------------------- + +data Cardinal + = CUp + | CDown + | CLeft + | CRight + deriving (Enum, Eq, Ord, Show) + +-- | Concat a foldable collection with a seperator interspersed. +-- +-- @since 1.0.0 +sepBy :: Foldable t => Doc ann -> t (Doc ann) -> Doc ann +sepBy s = Doc.concatWith (Doc.surround s) + +-- | Like 'copies', but intersperses space between each copy. +-- +-- @since 1.0.0 +hcopies :: Int -> Doc ann -> Doc ann +hcopies len doc + | len <= 0 = Doc.Internal.Empty + | otherwise = Doc.hsep (replicate len doc) + +-- | @'copies' n doc@ is a more optimal combinator for @Doc.sep . replicate n doc@ +-- +-- @since 1.0.0 +copies :: Int -> Doc ann -> Doc ann +copies len doc + | len <= 0 = Doc.Internal.Empty + | otherwise = Doc.cat (replicate len doc) + +-- | @'tab'@ inserts a two-space tab. +-- +-- @since 1.0.0 +tab :: Doc ann +tab = Doc.Internal.Text 2 " " + +-- | @'tabs' n@ inserts n-many tabs. +-- +-- @since 1.0.0 +tabs :: Int -> Doc ann +tabs len = spaces (2 * len) + +-- | @'spaces' n@ inserts n-many spaces. +-- +-- @since 1.0.0 +spaces :: Int -> Doc ann +spaces len + | len <= 0 = Doc.Internal.Empty + | len == 1 = Doc.Internal.Char ' ' + | otherwise = Doc.Internal.Text len (Text.replicate len $ Text.singleton ' ') + +-- | @'marginr' x n@ inserts @x@ and n-many spaces after. +-- +-- @since 1.0.0 +marginr :: Int -> Doc ann -> Doc ann +marginr len doc = Doc.fuse Deep (doc <> spaces len) + +-- | @'marginr' x n@ inserts @x@ and n-many spaces after. +-- +-- @since 1.0.0 +marginl :: Int -> Doc ann -> Doc ann +marginl len doc = Doc.fuse Deep (spaces len <> doc) + +-- | @'segment' n a b@ is a line segment of length @n@ with @a@, @b@ the left and right endpoints. +-- +-- @since 1.0.0 +segment :: Int -> Doc ann -> Doc ann -> Doc ann +segment len endl endr + | len == 0 = Doc.Internal.Empty + | len <= 2 = Doc.fuse Deep (endl <> endr) + | otherwise = Doc.fuse Deep (endl <> hruler (len - 2) <> endr) + +-- | Like 'segment', but with an extra argument to specify a 'Doc' used for the line segment. +-- +-- @since 1.0.0 +segmentWith :: Int -> Doc ann -> Doc ann -> Doc ann -> Doc ann +segmentWith len doc endl endr + | len <= 2 = endl <> endr + | otherwise = endl <> hcopies len doc <> endr + +-- | @'spaces' n@ inserts horizontal ruler of length n. +-- +-- @since 1.0.0 +hruler :: Int -> Doc ann +hruler len + | len <= 0 = Doc.Internal.Empty + | len == 1 = Doc.Internal.Char '─' + | otherwise = Doc.Internal.Text len (Text.replicate len $ Text.singleton '─') + +-- --------------------------------------------------------------------------------------------------------------------- + +vline :: Doc ann +vline = Doc.Internal.Char '│' + +hline :: Doc ann +hline = Doc.Internal.Char '─' + +cline :: Doc ann +cline = Doc.Internal.Char '┼' + +tack :: Cardinal -> Doc ann +tack = \case + CUp -> Doc.Internal.Char '┴' + CDown -> Doc.Internal.Char '┬' + CLeft -> Doc.Internal.Char '┤' + CRight -> Doc.Internal.Char '├' + +turnUpRight :: Doc ann +turnUpRight = Doc.Internal.Char '╭' + +turnRightUp :: Doc ann +turnRightUp = Doc.Internal.Char '╯' + +turnUpLeft :: Doc ann +turnUpLeft = Doc.Internal.Char '╮' + +turnLeftUp :: Doc ann +turnLeftUp = Doc.Internal.Char '╰' diff --git a/src/Language/Spectacle/Interaction/Options.hs b/src/Language/Spectacle/Interaction/Options.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/Options.hs @@ -0,0 +1,158 @@ +-- | Command-line interface options. +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction.Options + ( -- * CLI Options + OptsCLI (OptsCLI), + optsLogGraph, + optsOnlyTrace, + optsLogOutput, + + -- * CLI Parser + execOptsCLI, + parseOptsCLI, + + -- ** "only-trace" option + pOnlyTrace, + + -- ** "log" option + pLogGraph, + + -- ** "output" Option + OutputOpt (OptStdout, OptPath), + isStdout, + handleFrom, + pOutputOpt, + pOutputPath, + ) +where + +import Control.Applicative (Alternative ((<|>)), (<**>)) +import Options.Applicative + ( Parser, + customExecParser, + help, + helper, + idm, + info, + long, + metavar, + prefs, + short, + showHelpOnEmpty, + strOption, + switch, + ) +import System.IO (BufferMode (LineBuffering), Handle, IOMode (ReadWriteMode), hSetBuffering, openFile, stdout) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'OptsCLI' is a record command-line options for configuring the model checker. +-- +-- @since 1.0.0 +data OptsCLI = OptsCLI + { -- | Should the state diagram be drawn? + optsLogGraph :: Bool + , -- | Should the model checker only trace the states of a specification, without checking temporal properties? + optsOnlyTrace :: Bool + , -- | The output path for logs produced by CLI. + optsLogOutput :: OutputOpt + } + deriving (Eq, Show) + +-- | 'execOptsCLI' runs the command-line options parser. +-- +-- @since 1.0.0 +execOptsCLI :: IO OptsCLI +execOptsCLI = + let option = info (parseOptsCLI <**> helper) idm + config = prefs showHelpOnEmpty + in customExecParser config option + +-- | 'parseOptsCLI' is the parses command-line options into an 'OptsCLI'. +-- +-- @since 1.0.0 +parseOptsCLI :: Parser OptsCLI +parseOptsCLI = + OptsCLI + <$> pLogGraph + <*> pOnlyTrace + <*> pOutputOpt + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | CLI parser that consumes the "only-trace" flag. +-- +-- @since 1.0.0 +pOnlyTrace :: Parser Bool +pOnlyTrace = + switch + ( long "only-trace" + <> short 't' + <> help "Disable property checking and only trace a specification" + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | CLI parser that consumes the "log" flag. +-- +-- @since 1.0.0 +pLogGraph :: Parser Bool +pLogGraph = + switch + ( long "log" + <> short 'l' + <> help "Graph the model checker trace" + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | CLI option datatype holding either a filepath to emit model checker logs to. +-- +-- * @'OutputPath' str@ is a filepath to write logs to. +-- * 'OutputStdout' represents stdout as the chosen output location. +-- +-- @since 1.0.0 +data OutputOpt + = OptStdout + | OptPath FilePath + deriving (Eq, Show) + +-- | Is the output buffer stdout? +-- +-- @since 1.0.0 +isStdout :: OutputOpt -> Bool +isStdout opt = opt == OptStdout + +-- | @'handleFrom' opt@ will extract the file hand from the given 'OutputOpt' @opt@. +-- +-- @since 1.0.0 +handleFrom :: OutputOpt -> IO Handle +handleFrom opt = do + handle <- case opt of + OptStdout -> pure stdout + OptPath fp -> openFile fp ReadWriteMode + + hSetBuffering handle LineBuffering + pure handle + +-- | CLI parser that consumes the result of 'pOutputPath' if an output path is provided, otherwise 'OutputStd' is +-- returned by default and logs will be written to stdout. +-- +-- @since 1.0.0 +pOutputOpt :: Parser OutputOpt +pOutputOpt = pOutputPath <|> pure OptStdout + +-- | CLI parser that consumes a filepath to emit logs to. +-- +-- @since 1.0.0 +pOutputPath :: Parser OutputOpt +pOutputPath = OptPath <$> parser + where + parser = + strOption + ( long "output" + <> short 'o' + <> metavar "OUTPUT" + <> help "The log output path" + ) diff --git a/src/Language/Spectacle/Interaction/Paths.hs b/src/Language/Spectacle/Interaction/Paths.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/Paths.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE RecordWildCards #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction.Paths + ( -- * Construction + toPointSet, + takeMinRow, + ) +where + +import qualified Data.Set as Set +import Data.Set.Internal (Set (Bin, Tip)) +import Lens.Micro ((.~), (?~), (^.)) + +import Control.Monad.State (execState, gets, modify) +import Data.Foldable (traverse_) +import Data.Function ((&)) +import Data.Functor.Tree (Tree, pattern (:-)) +import Data.Type.Rec (HasDict) +import Data.World (World, fingerprint) +import Language.Spectacle.Interaction.Point (Point, column, extent, fromWorld, parent, row) + +-- --------------------------------------------------------------------------------------------------------------------- + +toPointSet :: HasDict Show ctx => Tree (World ctx) -> Set Point +toPointSet = flip execState Set.empty . start + where + start (w :- ws) = do + c <- gets (columnsOn 0) + let point = + fromWorld w + & column .~ c + & extent .~ length ws + + modify (Set.insert point) + traverse_ (go 1 (w ^. fingerprint)) ws + + go row0 par (w :- ws) = do + col <- gets (columnsOn row0) + let point = + fromWorld w + & parent ?~ par + & extent .~ length ws + & column .~ col + & row .~ row0 + modify (Set.insert point) + traverse_ (go (1 + row0) (w ^. fingerprint)) ws + +-- | Like 'splitRow', but always splits on the least row in the set. +-- +-- @since 1.0.0 +takeMinRow :: Set Point -> (Set Point, Set Point) +takeMinRow ps = + case Set.minView ps of + Nothing -> (Set.empty, Set.empty) + Just (p, _) -> splitRow (p ^. row) ps + +-- | @'splitRow' i ps@ returns a subset of @ps@ containing all elements located on row @i@ and a new set stripped of +-- this row. +-- +-- @since 1.0.0 +splitRow :: Int -> Set Point -> (Set Point, Set Point) +splitRow i = seek Set.empty + where + seek acc Tip = (acc, Tip) + seek acc (Bin _ !p ls rs) = + case compare (p ^. row) i of + LT -> + let (acc', rs') = seek acc rs + in (acc', Set.union (Set.insert p rs') ls) + GT -> + let (acc', ls') = seek acc ls + in (acc', Set.union (Set.insert p ls') rs) + EQ -> + let (acc0, ls') = seek acc ls + (acc1, rs') = seek acc0 rs + in (Set.insert p acc1, Set.union ls' rs') + +columnsOn :: Int -> Set Point -> Int +columnsOn i = Set.size . Set.filter (\pt -> pt ^. row == i) diff --git a/src/Language/Spectacle/Interaction/Point.hs b/src/Language/Spectacle/Interaction/Point.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/Point.hs @@ -0,0 +1,103 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction.Point + ( -- * Points + Point (Point), + pointLabel, + pointFields, + pointPos, + pointPar, + pointLen, + + -- ** Construction + fromWorld, + + -- ** Lenses + label, + parent, + fields, + column, + row, + extent, + ) +where + +import Data.Function (on) +import Lens.Micro (Lens', SimpleGetter, lens, to, (^.)) +import Prettyprinter (Doc, pretty, viaShow, (<+>)) +import Prettyprinter.Render.Terminal (AnsiStyle) + +import Data.Fingerprint (Fingerprint) +import Data.Type.Rec (HasDict, Rec, evident, pattern ConE, pattern NilE) +import Data.World (World (World)) +import Language.Spectacle.Interaction.Pos (Pos, pcol, prow, pattern Pos) + +-- --------------------------------------------------------------------------------------------------------------------- + +data Point = Point + { pointLabel :: {-# UNPACK #-} !Fingerprint + , pointFields :: [Doc AnsiStyle] + , pointPar :: !(Maybe Fingerprint) + , pointLen :: {-# UNPACK #-} !Int + , pointPos :: {-# UNPACK #-} !Pos + } + deriving (Show) + +fromWorld :: HasDict Show ctx => World ctx -> Point +fromWorld (World hash fs0) = Point hash (docFields fs0) Nothing 0 (Pos 0 0) + where + docFields :: HasDict Show ctx => Rec ctx -> [Doc AnsiStyle] + docFields rs = + case evident @Show rs of + ConE n x xs -> pretty n <+> "=" <+> viaShow x : docFields xs + NilE -> [] + +-- | @since 1.0.0 +instance Eq Point where + pt0 == pt1 = + let lblEq = pt0 ^. label == pt1 ^. label + posEq = pt0 ^. position == pt1 ^. position + in lblEq && posEq + {-# INLINE (==) #-} + +-- | @since 1.0.0 +instance Ord Point where + compare x y = case (compare `on` pointPos) x y of + EQ -> (compare `on` pointLabel) x y + ordering -> ordering + {-# INLINE compare #-} + +-- --------------------------------------------------------------------------------------------------------------------- + +label :: SimpleGetter Point Fingerprint +label = to pointLabel +{-# INLINE label #-} + +fields :: SimpleGetter Point [Doc AnsiStyle] +fields = to pointFields +{-# INLINE fields #-} + +parent :: Lens' Point (Maybe Fingerprint) +parent = lens pointPar \pt par -> pt {pointPar = par} +{-# INLINE parent #-} + +position :: Lens' Point Pos +position = lens pointPos \pt p -> pt {pointPos = p} +{-# INLINE position #-} + +column :: Lens' Point Int +column = position . pcol +{-# INLINE column #-} + +row :: Lens' Point Int +row = position . prow +{-# INLINE row #-} + +extent :: Lens' Point Int +extent = lens pointLen \pt i -> pt {pointLen = i} +{-# INLINE extent #-} diff --git a/src/Language/Spectacle/Interaction/Pos.hs b/src/Language/Spectacle/Interaction/Pos.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Interaction/Pos.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE RecordWildCards #-} + +-- | 'Pos' is pair of integers representing a position in grid. The implementation for 'compare' on 'Pos' is biased to +-- the row-value of the position, i.e. +-- +-- @ +-- ∀ (x y u v :: Int) -> x ≢ u -> Pos x y `compare` Pos u v ≡ compare x u +-- @ +-- +-- This definition of 'compare' enables collections of 'Pos' to preserve most of the structural information in a rose +-- tree when kept in ordered-containers who manage their internal structure with 'compare' such as 'Set'. To motivate +-- why this is useful, it is worth noting that the model checker works exclusively with nested structures like rose +-- trees. Rendering output from trees is difficult since it is not always clear how to traverse a tree to extract a +-- flattened presentation of information in a tree that can be easily rendered as output. +-- +-- Traversing a ('Set' 'Pos') is trivial, though, since 'Set' is (for all intent and purposes) a flat collection of +-- elements, and more specifically one which manages its structure with 'compare' internally. As a result of the way in +-- which 'compare' is defined, column and row values of 'Pos' can simultaneously be viewed as file locations and +-- node positions in a tree. Sets of Pos are flat organizations of information that can be rendered to output +-- straightforward way while still being able to store/recover the shape information of the original tree we're +-- interested in logging: +-- +-- @ +-- 1 2 3 4 5 6 7 8 9 +-- ┌╌🮻╌╌🮻╌╌🮻╌ ○ ╌🮻╌╌🮻╌╌🮻╌╌🮻╌╌🮻╌┐ +-- ┆ ┆ ┆ ╱ ┃ ╲ ┆ ┆ ┆ ┆ ┆ +-- ├╌🮻╌╌🮻╌ ○ ○ ○ ╌╌🮻╌╌🮻╌╌🮻╌┤ 1 +-- ┆ ┆ ┆ ┃ ┃ ┃ ╲ ┆ ┆ ┆ ┆ +-- ├╌🮻╌╌🮻╌ ○ ○ ○ ○ ╌🮻╌╌🮻╌╌🮻╌┤ 2 +-- ┆ ┆ ┆ ╲ ┃ ┃ ╱ ┆ ┆ ┆ ┆ +-- ├╌🮻╌╌🮻╌ ○ ○ ╌╌🮻╌╌🮻╌╌🮻╌┤ 3 +-- ┆ ┆ ┆ ┆ ┃ ┃ ┆ ┆ ┆ ┆ ┆ +-- ├╌🮻╌╌🮻╌╌🮻╌ ○ ○ ╌🮻╌╌🮻╌╌🮻╌╌🮻╌┤ 4 +-- ┆ ┆ ┆ ┆ ┃ ╱ ┆ ┆ ┆ ┆ ┆ +-- ├╌🮻╌╌🮻╌╌🮻╌ ○ ╌🮻╌╌🮻╌╌🮻╌╌🮻╌╌🮻╌┤ 5 +-- ┆ ┆ ┆ ┆ ┃ ┆ ┆ ┆ ┆ ┆ ┆ +-- └╌🮻╌╌🮻╌╌🮻╌ ○ ╌🮻╌╌🮻╌╌🮻╌╌🮻╌╌🮻╌┘ +-- @ +-- +-- This example would be the set with elements ordered according to their depth, and then to their span: +-- +-- @ +-- fromList [(0,4), (1,3), (1,4), (1,5), (2,3), (2,4), (2,5), ..., (5,4), (6,4)] +-- @ +-- +-- @since 1.0.0 +module Language.Spectacle.Interaction.Pos + ( -- * Locations + Loc (Loc), + locPos, + locExt, + + -- * Positions + Pos (MkPos), + pattern Pos, + getPos, + posRow, + posCol, + + -- ** Lenses + prow, + pcol, + ) +where + +import Data.Function (on) +import Data.Semigroup (Sum (Sum)) +import Lens.Micro (Lens', lens, set, _1, _2) +import Lens.Micro.Extras (view) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | A 'Loc' is a position annotated with an length/span. +-- +-- @since 1.0.0 +data Loc = Loc + { locPos :: {-# UNPACK #-} !Pos + , locExt :: {-# UNPACK #-} !Int + } + deriving (Eq) + +-- | @since 1.0.0 +instance Ord Loc where + compare = compare `on` locPos + +-- | Buffer row/column positions. +-- +-- @since 1.0.0 +newtype Pos = MkPos {getPos :: (Int, Int)} + deriving (Eq, Semigroup, Monoid) via (Sum Int, Sum Int) + +pattern Pos :: Int -> Int -> Pos +pattern Pos {posRow, posCol} = MkPos (posRow, posCol) + +{-# COMPLETE Pos #-} + +-- | @since 1.0.0 +instance Ord Pos where + -- The derived implementation of 'Ord' is equivalent to what is given here, but its defined explicitly anyway + -- to emphasize the row value superseding the order of the column value in this trichotomy. + Pos x y `compare` Pos u v = case compare x u of + EQ -> compare y v + ordering -> ordering + +-- | @since 1.0.0 +instance Show Pos where + show (Pos r c) = "Pos(" ++ show r ++ ":" ++ show c ++ ")" + +prow :: Lens' Pos Int +prow = lens (view _1 . getPos) \ ~(MkPos p) x -> MkPos (set _1 x p) +{-# INLINE prow #-} + +pcol :: Lens' Pos Int +pcol = lens (view _2 . getPos) \ ~(MkPos p) x -> MkPos (set _2 x p) +{-# INLINE pcol #-} diff --git a/src/Language/Spectacle/Lang.hs b/src/Language/Spectacle/Lang.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Lang.hs @@ -0,0 +1,83 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeFamilies #-} + +-- | The 'Lang' monad and functions for defining Spectacles syntax as effects. +-- +-- @since 1.0.0 +module Language.Spectacle.Lang + ( -- * Lang + Lang (Pure, Op, Scoped), + runLang, + send, + scope, + weaken, + + -- * Effects + type EffectK, + type ScopeK, + FirstOrder, + Effect, + + -- ** Membership + type Members, + Member (inject, project, injectS, projectS), + + -- ** Unions + Op (OHere, OThere), + Scoped (SHere, SThere), + decomposeOp, + extractOp, + decomposeS, + extractS, + ) +where + +import Data.Functor.Loom (hoist, (~>~)) +import Language.Spectacle.Lang.Internal (Lang (Op, Pure, Scoped), scope, send) +import Language.Spectacle.Lang.Member (Member (inject, injectS, project, projectS), type Members) +import Language.Spectacle.Lang.Op (Op (OHere, OThere), decomposeOp, extractOp) +import Language.Spectacle.Lang.Scoped + ( Effect, + EffectK, + FirstOrder, + ScopeK, + Scoped (SHere, SThere), + decomposeS, + extractS, + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Used to unwrap the pure value in 'Lang' after all of its effects have been discharged. +-- +-- @since 1.0.0 +runLang :: Lang ctx '[] a -> a +runLang (Pure x) = x +runLang _ = + -- @Lang ctx '[] a@ can only be constructed with 'Pure' or obtained by discharging all its + -- effects, which would result in 'Pure'. Cases where @Lang ctx '[] a@ holds impure values mean + -- that: + -- + -- 1. An effect escaped the scope of 'Lang' and therefore was not discharged when the handler for + -- that effect was run on 'Lang'. This not impossible but is /very/ difficult to do since the + -- escaped effect would have to be hidden from 'Loom'. 'Lang' in a first-order operation, + -- FO effects with resumptions to Lang, or intentionally weakening/coercing a @Lang ctx effs' a@ + -- into some other 'Lang' are all ways which basically guarantee that effects will be left + -- unhandled. + -- + -- 2. Operations like 'unsafeCoerce' were used to change the effect signature of 'Lang'. + error + "internal error: Lang match against Yield, this means that an effect escaped the scope of Lang \ + \and was left unhandled. This should be impossible." + +-- | Appends an effect label @eff@ to the head of a 'Lang's effect signature by the weakening rule +-- for sum types. +-- +-- @since 1.0.0 +weaken :: forall eff effs ctx a. Lang ctx effs a -> Lang ctx (eff ': effs) a +weaken = \case + Pure x -> pure x + Op op k -> Op (OThere op) (weaken . k) + Scoped scoped loom -> Scoped (SThere scoped) (loom ~>~ hoist weaken) diff --git a/src/Language/Spectacle/Lang/Internal.hs b/src/Language/Spectacle/Lang/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Lang/Internal.hs @@ -0,0 +1,105 @@ +{-# LANGUAGE UndecidableInstances #-} + +-- | The 'Lang' monad. +-- +-- @since 1.0.0 +module Language.Spectacle.Lang.Internal + ( Lang (Pure, Op, Scoped), + send, + scope, + ) +where + +import Control.Applicative (Alternative (empty, (<|>))) +import Control.Monad (MonadPlus (mplus, mzero), (>=>)) +import Data.Bool (bool) +import Data.Kind (Type) +import GHC.TypeLits (Symbol) + +import Data.Ascript (Ascribe) +import Data.Functor.Loom (Loom (Loom), bind, (~>~)) +import qualified Data.Functor.Loom as Loom +import Language.Spectacle.Lang.Member (Member (inject, injectS)) +import Language.Spectacle.Lang.Op (Op) +import Language.Spectacle.Lang.Scoped (Effect, EffectK, Scoped) +import Language.Spectacle.Syntax.NonDet.Internal (NonDet (Choose, Empty)) + +-- ------------------------------------------------------------------------------------------------- + +-- | 'Lang' is a CEK-style interpreter for the set of effects behind Spectacles syntax and is based +-- on Oleg's Eff monad. 'Lang' differs from Eff in it's @ctx@ parameter and its ability to support +-- higher-order effects. +-- +-- * The type parameter @ctx@ is a type row associating variable names to their respective types. +-- This includes plain values from the previous frame as well as primed variables in the next frame. +-- +-- * The type parameter @effs@ is the set of effects a 'Lang' is capable of performing. +-- +-- @since 1.0.0 +type Lang :: [Ascribe Symbol Type] -> [EffectK] -> Type -> Type +data Lang ctxt effs a where + Pure :: + a -> + Lang ctxt effs a + Op :: + Op effs a -> + (a -> Lang ctxt effs b) -> + Lang ctxt effs b + Scoped :: + Scoped effs (Lang ctxt effs') a -> + Loom (Lang ctxt effs') (Lang ctxt effs) a b -> + Lang ctxt effs b + +-- | Sends a constructor for the effect @eff@ for 'Lang' to handle. +-- +-- @since 1.0.0 +send :: Member eff effs => eff a -> Lang ctx effs a +send eff = Op (inject eff) pure +{-# INLINE send #-} + +-- | Like 'send', but sends a constructor for the 'Effect' instance of @eff@. +-- +-- @since 1.0.0 +scope :: Member eff effs => Effect eff (Lang ctx effs) a -> Lang ctx effs a +scope eff = Scoped (injectS eff) Loom.identity +{-# INLINE scope #-} + +-- | @since 1.0.0 +instance Functor (Lang ctx effs) where + fmap f (Pure x) = Pure (f x) + fmap f (Op u k) = Op u (fmap f . k) + fmap f (Scoped u loom) = Scoped u (fmap f loom) + {-# INLINE fmap #-} + +-- | @since 1.0.0 +instance Applicative (Lang ctx effs) where + pure = Pure + {-# INLINE CONLIKE pure #-} + + Pure f <*> m = fmap f m + Op u k <*> m = Op u ((<*> m) . k) + Scoped u (Loom ctx eta) <*> m = Scoped u (Loom ctx ((<*> m) . eta)) + {-# INLINE (<*>) #-} + +-- | @since 1.0.0 +instance Monad (Lang ctx effs) where + Pure x >>= f = f x + Op u k >>= f = Op u (k >=> f) + Scoped u loom >>= f = Scoped u (loom ~>~ bind f) + {-# INLINE (>>=) #-} + +-- | @since 1.0.0 +instance Member NonDet effs => Alternative (Lang ctx effs) where + empty = send Empty + {-# INLINE empty #-} + + a <|> b = send Choose >>= bool b a + {-# INLINE (<|>) #-} + +-- | @since 1.0.0 +instance Member NonDet effs => MonadPlus (Lang ctx effs) where + mzero = empty + {-# INLINE mzero #-} + + mplus = (<|>) + {-# INLINE mplus #-} diff --git a/src/Language/Spectacle/Lang/Member.hs b/src/Language/Spectacle/Lang/Member.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Lang/Member.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE TypeFamilies #-} + +-- | Effect membership. +-- +-- @since 1.0.0 +module Language.Spectacle.Lang.Member + ( Members, + Member (inject, project, injectS, projectS), + ) +where + +import Data.Kind (Constraint) + +import Language.Spectacle.Lang.Op (Op (OHere, OThere)) +import Language.Spectacle.Lang.Scoped (Effect, EffectK, Scoped (SHere, SThere)) + +-- ------------------------------------------------------------------------------------------------- + +-- | N-ary, infix operator for 'Member'. +-- +-- * @Members '[A, B, C] effs = (Member A effs, Member B effs, Member C effs)@ +-- * @Members A effs = Members '[A] effs = Member A effs@ +-- +-- @since 1.0.0 +type Members :: forall k. k -> [EffectK] -> Constraint +type family Members eff effs where +-- Type ascription is used here rather than a type application to the LHS of the equations since +-- fourmolu does not know how to parse type applications at the type level yet. +-- +-- https://github.com/tweag/ormolu/issues/698 + Members (eff :: EffectK) effs = Member eff effs + Members (eff ': effs' :: [EffectK]) effs = (Member eff effs, Members effs' effs) + Members ('[] :: [EffectK]) effs = () + +-- | An effect @eff@ is a member of the effect signature @effs@ if @eff@ occurs in @effs@. +-- +-- @since 1.0.0 +type Member :: EffectK -> [EffectK] -> Constraint +class Member eff effs where + -- | Inject a first order effect @eff a@ into a sum of first-order effects 'Op'. Higher-order + -- operations must be injected with 'injectS'. + -- + -- @since 1.0.0 + inject :: eff a -> Op effs a + + -- | Projects the effect @eff@ from the given 'Op' if it is the inhabitant, otherwise 'Nothing'. + -- + -- @since 1.0.0 + project :: Op effs a -> Maybe (eff a) + + -- | Like 'inject', but specifically for scoped operations. + -- + -- @since 1.0.0 + injectS :: Effect eff m a -> Scoped effs m a + + -- | Like 'project', but specifically for scoped operations. + -- + -- @since 1.0.0 + projectS :: Scoped effs m a -> Maybe (Effect eff m a) + +-- | @since 1.0.0 +instance {-# OVERLAPS #-} Member eff (eff ': effs) where + inject = OHere + {-# INLINE CONLIKE inject #-} + + project (OHere op) = Just op + -- We only have to scrutinize this case because there is technically nothing preventing an effect + -- signature from having two of the same effect in the list; however, the only way to make that + -- happen is to instantiate Lang with a monomorphic list containing duplicates. Nubbing effect + -- signatures isn't worth it in any case since running handlers is idempotent so this case can + -- just be thrown out. + project (OThere _) = Nothing + {-# INLINE CONLIKE project #-} + + injectS = SHere + {-# INLINE CONLIKE injectS #-} + + projectS (SHere s) = Just s + projectS (SThere _) = Nothing + {-# INLINE CONLIKE projectS #-} + +-- | @since 1.0.0 +instance Member eff effs => Member eff (eff' ': effs) where + inject = OThere . inject + {-# INLINE CONLIKE inject #-} + + project (OThere op) = project op + project _ = Nothing + {-# INLINE CONLIKE project #-} + + injectS = SThere . injectS + {-# INLINE CONLIKE injectS #-} + + projectS (SThere scoped) = projectS scoped + projectS _ = Nothing + {-# INLINE CONLIKE projectS #-} diff --git a/src/Language/Spectacle/Lang/Op.hs b/src/Language/Spectacle/Lang/Op.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Lang/Op.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE EmptyCase #-} + +-- | First-order effect operations. +-- +-- @since 1.0.0 +module Language.Spectacle.Lang.Op + ( Op (OHere, OThere), + decomposeOp, + extractOp, + ) +where + +-- ------------------------------------------------------------------------------------------------- + +-- | 'Op' is an extensible sum inhabited by a first-order effect @eff a@ in @effs@. +-- +-- @since 1.0.0 +data Op effs a where + OHere :: eff a -> Op (eff ': effs) a + OThere :: Op effs a -> Op (eff ': effs) a + +-- | Orthogonal decomposition for 'Op'. Yields either a proof that the effect @eff@ is not +-- inhabiting the given 'Op' or a constructor for @eff@. +-- +-- @since 1.0.0 +decomposeOp :: Op (eff ': effs) a -> Either (Op effs a) (eff a) +decomposeOp (OHere eff) = Right eff +decomposeOp (OThere op) = Left op +{-# INLINE decomposeOp #-} + +-- | A special case of 'decomposeOp'. A singleton sum of @eff@ must be inhabited by @eff@. +-- +-- @since 1.0.0 +extractOp :: Op '[eff] a -> eff a +extractOp (OHere eff) = eff +extractOp (OThere op) = case op of +{-# INLINE extractOp #-} diff --git a/src/Language/Spectacle/Lang/Scoped.hs b/src/Language/Spectacle/Lang/Scoped.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Lang/Scoped.hs @@ -0,0 +1,140 @@ +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TypeFamilies #-} + +-- | Defining and handling higher-order effects in the 'Effect' data family. +-- +-- === Example usage of the Effect family +-- +-- The ask operation for the Reader effect is given by GADT: +-- +-- @ +-- data Reader r :: 'EffectK' where +-- Ask :: Reader r r +-- @ +-- +-- 'EffectK' intentionally precludes the ability for accessing the 'Language.Spectacle.Lang.Lang' in +-- its continuation which is needed to define a "local" operation for Reader. If this was allowed, +-- it becomes very easy for effects to escape the scope of the free monad and continue without being +-- handled, examples of which are in [1. Effect Handlers in Haskell, Evidently.]("Language.Spectacle.Lang.Scoped#references"). +-- Instead, scoped operations like local are defined in a corresponding instance of 'Effect' +-- like so: +-- +-- @ +-- data instance 'Effect' (Reader r) m a where +-- Local :: m a -> (r -> r) -> 'Effect' (Reader r) m a +-- @ +-- +-- Where @m@ is some 'Langauge.Spectacle.Lang.Lang'. This approach lets us define scoped operations +-- which may have: +-- +-- * Dependencies on other effects. +-- * Constraints on types in the effect. +-- * Monomorphic types in the continuation. +-- +-- Effects which only have first-order operations must still give a newtype instance for 'Effect' +-- wrapping 'Data.Void.Void' and handled with 'Data.Void.absurd'. +-- +-- === Reasoning behind the 'Effect' family +-- +-- The typical approach to handling higher-order effects is done by "weaving" which is described in +-- [2. Effect Handler in Scope]("Language.Spectacle.Lang.Scoped#references"). It requires that every +-- effect have an instance of @(forall x. f (m x) -> n (f x))@. This forces all effects to be +-- polymorphic in their continuation due to the rigidity of @x@. Effects like the quantifier syntax +-- can't be defined this way since there is no way to weave @(a -> m Bool)@. +-- +-- An alternative would be to change the continuation of the Freer monad to accumulate weaves rather +-- than monadic actions, thus pushing the weaving responsibility to the handler site. This allows +-- monomorphic effects and constrained data contexts, but struggles with handling effects like NonDet +-- since it's not possible to distribute functors over the freer monad. The way to work around this is +-- to use a concrete functorial state like ListT to distribute and then fold back into the resulting +-- alternative. This works at the consequence of having different semantics for NonDet in first- +-- order vs higher-order operations. +-- +-- The 'Effect' family solves boths problems since: +-- +-- 1. Weaving 'Effect' instances is done in the handler for the effect. +-- +-- 2. An 'Effect' instance is a seperate case from its corresponding first-order effect so effects +-- like NonDet can weave in terms of its own interpreter rather than choosing a concrete functor as +-- an intermediate carrier. +-- +-- #references# +-- +-- === Reference +-- +-- 1. [Effect Handlers in Haskell, Evidently](https://xnning.github.io/papers/haskell-evidently.pdf) +-- 2. [Effect Handlers in Scope](https://www.cs.ox.ac.uk/people/nicolas.wu/papers/Scope.pdf) +-- +-- @since 1.0.0 +module Language.Spectacle.Lang.Scoped + ( -- * Effect Kinds + EffectK, + ScopeK, + + -- * Effect family + FirstOrder, + Effect, + + -- * Higher-order union + Scoped (SHere, SThere), + decomposeS, + extractS, + ) +where + +import Data.Coerce (Coercible) +import Data.Kind (Constraint, Type) +import Data.Void (Void) + +-- ------------------------------------------------------------------------------------------------- + +-- | The kind of first-order effects. +-- +-- @since 1.0.0 +type EffectK = Type -> Type + +-- | The kind of higher-order effects. +-- +-- @since 1.0.0 +type ScopeK = (Type -> Type) -> Type -> Type + +-- | Constraint for first-order effects. +-- +-- @since 1.0.0 +type FirstOrder :: EffectK -> Constraint + +type FirstOrder eff = forall m a. Coercible (Effect eff m a) Void + +-- | 'Effect' is a family of higher-order operations for the effect @eff@. +-- +-- @since 1.0.0 +type Effect :: EffectK -> ScopeK +data family Effect eff m a + +-- ------------------------------------------------------------------------------------------------- + +-- | 'Scoped' is an extensible sum inhabited by the higher-order operations of some effect in +-- @effs@. +-- +-- @since 1.0.0 +data Scoped effs m a where + SHere :: Effect eff m a -> Scoped (eff ': effs) m a + SThere :: Scoped effs m a -> Scoped (eff ': effs) m a + +-- | Orthogonal decomposition of a 'Scoped'. Decomposing a 'Scoped' can yield either the 'Effect' +-- instance for @eff@ or witness a proof that @Eff eff m a@ does not inhabit this sum and remove +-- it from the effect signature. +-- +-- @since 1.0.0 +decomposeS :: Scoped (eff ': effs) m a -> Either (Scoped effs m a) (Effect eff m a) +decomposeS (SHere eff) = Right eff +decomposeS (SThere s) = Left s +{-# INLINE decomposeS #-} + +-- | A special case of 'decomposeS'. A singleton sum of @eff@ must be inhabited by @eff@. +-- +-- @since 1.0.0 +extractS :: Scoped '[eff] m a -> Effect eff m a +extractS (SHere eff) = eff +extractS (SThere s) = case s of diff --git a/src/Language/Spectacle/Model.hs b/src/Language/Spectacle/Model.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model.hs @@ -0,0 +1,314 @@ +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model where + +import Control.Monad (unless) +import Control.Monad.Except (MonadError (throwError)) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Reader (local) +import Control.Monad.State (gets) +import Data.Foldable (for_, traverse_) +import Data.Function (on) +import Data.Hashable (Hashable) +import Data.List (nubBy) +import qualified Data.Map as Map +import Data.Set (Set) +import qualified Data.Set as Set +import Data.Traversable (for) +import Lens.Micro (over, (&), (^.)) +import Lens.Micro.Mtl (use, view, (%=), (.=)) + +import Data.Fingerprint (Fingerprint) +import Data.Functor.Tree (Tree, rootOf, pattern (:-)) +import Data.Type.Rec (HasDict) +import Data.World (World (World), fingerprint, worldValues) +import Language.Spectacle.Model.ModelAction + ( ModelAction (modelActionName), + fromActionSpec, + runModelAction, + ) +import Language.Spectacle.Model.ModelError + ( ModelError (InitialError, RefutedError), + TemporalError (TemporalError), + ) +import Language.Spectacle.Model.ModelNode as ModelNode + ( ModelNode (ModelNode), + nextEntries, + valuation, + ) +import Language.Spectacle.Model.ModelState as ModelState + ( enabledActionsAt, + indexNode, + member, + queuedActionsAt, + ) +import Language.Spectacle.Model.ModelTemporal + ( ModelTemporal (getModelTemporal, modelTemporalName), + fromTemporalSpec, + ) +import Language.Spectacle.Model.Monad + ( ModelM, + modalityOf, + newModelEnv, + runModelM, + strongFairActions, + weakFairActions, + ) +import Language.Spectacle.Specification + ( Modality (Always, Eventually, Infinitely, Stays), + Specification, + getActionFormulae, + getFairnessSpec, + getModalitySpec, + getTemporalFormulae, + runInitialSpec, + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +modelcheck :: + HasDict Hashable ctx => + Specification ctx acts form -> + IO (Either (ModelError ctx) [Tree (World ctx)]) +modelcheck spec = do + let initials = runInitialSpec spec + let formulae = fromTemporalSpec (getTemporalFormulae spec) + let actions = fromActionSpec (getActionFormulae spec) + + let env = newModelEnv (getFairnessSpec spec) (getModalitySpec spec) + result <- snd <$> runModelM (checkModelSpec initials actions formulae) env mempty + + case result of + Left err -> pure (Left err) + Right modelTrees -> pure (Right modelTrees) + +modeltrace :: + HasDict Hashable ctx => + Specification ctx acts form -> + IO (Either (ModelError ctx) [Tree (World ctx)]) +modeltrace spec = do + let initials = runInitialSpec spec + let actions = fromActionSpec (getActionFormulae spec) + + let env = newModelEnv (getFairnessSpec spec) (getModalitySpec spec) + snd <$> runModelM (traceModelSpec initials actions) env mempty + +traceModelSpec :: + MonadIO m => + Set (World ctx) -> + [ModelAction ctx] -> + ModelM ctx m [Tree (World ctx)] +traceModelSpec initials actions + | Set.null initials = do + throwError InitialError + | otherwise = do + _ <- unfoldModelState actions initials + + for (Set.toList initials) \initial -> + expandAction (initial ^. fingerprint) + +checkModelSpec :: + MonadIO m => + Set (World ctx) -> + [ModelAction ctx] -> + [ModelTemporal ctx] -> + ModelM ctx m [Tree (World ctx)] +checkModelSpec initials actions formulae + | Set.null initials = do + throwError InitialError + | otherwise = do + _ <- unfoldModelState actions initials + + for (Set.toList initials) \initial -> do + let hash = initial ^. fingerprint + modelTree <- expandAction hash + + for_ formulae \formula -> do + let name = modelTemporalName formula + modality <- view (modalityOf name) + case modality of + Always -> checkAlways formula modelTree + Eventually -> checkFuture formula modelTree + Infinitely -> checkInfinitely formula modelTree + Stays -> checkStays formula modelTree + + pure modelTree + +checkAlways :: Monad m => ModelTemporal ctx -> Tree (World ctx) -> ModelM ctx m () +checkAlways formula (initial :- subtrees) = traverse_ (go initial) subtrees + where + go here (there :- nexts) = do + let satisfied = getModelTemporal formula here there + unless satisfied do + let name = modelTemporalName formula + throwRefuteAlways name (Just here) (Just there) + traverse_ (go there) nexts + +checkFuture :: MonadIO m => ModelTemporal ctx -> Tree (World ctx) -> ModelM ctx m () +checkFuture formula (root :- subtrees) = traverse_ (go root) subtrees + where + go here (there :- nexts) + | null nexts = do + let name = modelTemporalName formula + let satisfied = getModelTemporal formula here there + unless satisfied do + throwRefuteEventually name (Just here) (Just there) + | otherwise = do + let satisfied = getModelTemporal formula here there + unless satisfied do + traverse_ (go there) nexts + +checkInfinitely :: Monad m => ModelTemporal ctx -> Tree (World ctx) -> ModelM ctx m () +checkInfinitely formula (root :- subtrees) = traverse_ (go root) subtrees + where + go here (there :- nexts) + | null nexts = do + let name = modelTemporalName formula + throwRefuteInfinitely name (Just here) (Just there) + | otherwise = do + let satisfied = getModelTemporal formula here there + if satisfied + then do + isCyclicallySatisfied <- and <$> traverse (cyclically here) nexts + unless isCyclicallySatisfied do + let name = modelTemporalName formula + throwRefuteInfinitely name (Just here) (Just there) + else do + traverse_ (go there) nexts + + cyclically match (here :- []) = pure (match == here) + cyclically match (here :- there) + | match == here = pure True + | otherwise = do + and <$> traverse (cyclically match) there + +checkStays :: Monad m => ModelTemporal ctx -> Tree (World ctx) -> ModelM ctx m () +checkStays formula (root :- subtrees) = do + results <- traverse (go root) subtrees + let satisfied = and results + unless satisfied do + let name = modelTemporalName formula + throwRefuteStays name (Just root) Nothing + where + go here (there :- nexts) + | null nexts = do + pure (getModelTemporal formula here there) + | otherwise = do + results <- traverse (go there) nexts + pure (and results) + +expandAction :: MonadIO m => Fingerprint -> ModelM ctx m (Tree (World ctx)) +expandAction = run + where + run hash = do + world <- World hash <$> use (indexNode hash . valuation) + + enabled <- gets (enabledActionsAt hash) + actionsTodo <- do + queued <- use (queuedActionsAt hash) + pure (filter (`Set.member` queued) enabled) + + if null actionsTodo + then do + actionsSF <- Set.toList <$> view strongFairActions + let todoSF = filter (`elem` enabled) actionsSF + + if null todoSF + then do + actionsWF <- Set.toList <$> view weakFairActions + let todoWF = filter (`elem` enabled) actionsWF + + if null todoWF + then do + -- No actions left todo, no fairness constraints to solve, so stutter and terminate. + pure (world :- [world :- []]) + else do + subtrees <- for todoWF \actionWF -> + local (over weakFairActions (Set.delete actionWF)) do + entries <- use (indexNode hash . nextEntries actionWF) + traverse run (filter (/= hash) entries) + pure (world :- nubBy ((==) `on` rootOf) (concat subtrees)) + else do + subtrees <- for todoSF \actionSF -> do + local (over strongFairActions (Set.delete actionSF)) do + entries <- use (indexNode hash . nextEntries actionSF) + traverse run (filter (/= hash) entries) + pure (world :- nubBy ((==) `on` rootOf) (concat subtrees)) + else do + subtrees <- for actionsTodo \todo -> do + entries <- use (indexNode hash . nextEntries todo) + queuedActionsAt hash %= Set.delete todo + -- Take only changing steps + traverse run (filter (/= hash) entries) + + pure (world :- concat subtrees) + +unfoldModelState :: + MonadIO m => + [ModelAction ctx] -> + Set (World ctx) -> + ModelM ctx m [Tree Fingerprint] +unfoldModelState actions = traverse go . Set.toList + where + go world = do + let hash = world ^. fingerprint + isSeen <- gets (ModelState.member hash) + + if isSeen + then do + pure (hash :- []) + else do + nexts <- Map.fromList <$> traverse (runAction world) actions + + let entries = map (view fingerprint) <$> nexts + let values = world ^. worldValues + let queued = + nexts & Map.foldMapWithKey \action worlds -> + if null worlds + then Set.empty + else Set.singleton action + + indexNode hash .= ModelNode entries queued values + + subtrees <- traverse go (concat (Map.elems nexts)) + pure (hash :- subtrees) + + runAction world action = do + let name = modelActionName action + worlds <- runModelAction world action + pure (name, Set.toList worlds) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'throwRefute' is a helper combination for constructing an error refuting a temporal property and throwing it. +-- +-- @since 1.0.0 +throwRefute :: Monad m => Modality -> String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a +throwRefute modality name here there = do + let err = TemporalError modality name here there + throwError (RefutedError err) + +-- | Convinence function for constructing an "always" error and throwing it. +-- +-- @since 1.0.0 +throwRefuteAlways :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a +throwRefuteAlways = throwRefute Always + +-- | Convinence function for constructing an "eventually" error and throwing it. +-- +-- @since 1.0.0 +throwRefuteEventually :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a +throwRefuteEventually = throwRefute Eventually + +-- | Convinence function for constructing an "infinitely often" error and throwing it. +-- +-- @since 1.0.0 +throwRefuteInfinitely :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a +throwRefuteInfinitely = throwRefute Infinitely + +-- | Convinence function for constructing an "stays as" error and throwing it. +-- +-- @since 1.0.0 +throwRefuteStays :: Monad m => String -> Maybe (World ctx) -> Maybe (World ctx) -> ModelM ctx m a +throwRefuteStays = throwRefute Stays diff --git a/src/Language/Spectacle/Model/ModelAction.hs b/src/Language/Spectacle/Model/ModelAction.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/ModelAction.hs @@ -0,0 +1,51 @@ +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model.ModelAction + ( -- * Model Action + ModelAction (ModelAction), + modelActionName, + getModelAction, + + -- ** Construction + fromActionSpec, + + -- ** Deconstruction + runModelAction, + ) +where + +import Control.Monad.Except (MonadError, throwError) +import Data.Hashable (Hashable) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Set (Set) +import Lens.Micro ((^.)) + +import Data.Type.Rec (HasDict) +import Data.World (World, worldValues) +import Language.Spectacle.AST (Action) +import Language.Spectacle.AST.Action (runExceptionalAction) +import Language.Spectacle.Exception.RuntimeException (RuntimeException) +import Language.Spectacle.Model.ModelError + ( ModelError (RuntimeError), + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +data ModelAction ctx = ModelAction + { modelActionName :: String + , getModelAction :: World ctx -> Either RuntimeException (Set (World ctx)) + } + +runModelAction :: MonadError (ModelError ctx) m => World ctx -> ModelAction ctx -> m (Set (World ctx)) +runModelAction world action = + case getModelAction action world of + Left err -> throwError (RuntimeError err) + Right worlds -> pure worlds + +fromActionSpec :: HasDict Hashable ctx => Map String (Action ctx Bool) -> [ModelAction ctx] +fromActionSpec = + Map.foldMapWithKey \name action -> + let runner world = runExceptionalAction (world ^. worldValues) action + in [ModelAction name runner] diff --git a/src/Language/Spectacle/Model/ModelEnv.hs b/src/Language/Spectacle/Model/ModelEnv.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/ModelEnv.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE RecordWildCards #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model.ModelEnv + ( -- * Model Environments + ModelEnv (ModelEnv), + mcEnvActionFairness, + mcEnvFormulaModality, + mcEnvUnfairActions, + mcEnvWeakFairActions, + mcEnvStrongFairActions, + + -- ** Construction + newModelEnv, + + -- ** Lenses + actionInfo, + modalityOf, + fairnessOf, + unfairActions, + weakFairActions, + strongFairActions, + ) +where + +import Data.Map.Strict (Map) +import qualified Data.Map.Strict as Map +import Data.Set (Set) +import qualified Data.Set as Set +import Lens.Micro (Lens', SimpleGetter, lens, to) + +import Language.Spectacle.Fairness (Fairness (StrongFair, Unfair, WeakFair)) +import Language.Spectacle.Specification (Modality) + +-- --------------------------------------------------------------------------------------------------------------------- + +data ModelEnv = ModelEnv + { mcEnvActionFairness :: Map String Fairness + , mcEnvFormulaModality :: Map String Modality + , mcEnvUnfairActions :: Set String + , mcEnvWeakFairActions :: Set String + , mcEnvStrongFairActions :: Set String + } + +newModelEnv :: Map String Fairness -> Map String Modality -> ModelEnv +newModelEnv fairInfo modalInfo = + let unfair = Set.fromList . Map.keys $ Map.filter (Unfair ==) fairInfo + weakfair = Set.fromList . Map.keys $ Map.filter (WeakFair ==) fairInfo + strongfair = Set.fromList . Map.keys $ Map.filter (StrongFair ==) fairInfo + in ModelEnv fairInfo modalInfo unfair weakfair strongfair + +modalityOf :: String -> SimpleGetter ModelEnv Modality +modalityOf name = to \env -> + mcEnvFormulaModality env Map.! name + +fairnessOf :: String -> SimpleGetter ModelEnv Fairness +fairnessOf name = to \env -> + mcEnvActionFairness env Map.! name + +actionInfo :: SimpleGetter ModelEnv (Map String Fairness) +actionInfo = to mcEnvActionFairness + +unfairActions :: SimpleGetter ModelEnv (Set String) +unfairActions = to mcEnvUnfairActions + +weakFairActions :: Lens' ModelEnv (Set String) +weakFairActions = lens mcEnvWeakFairActions \ModelEnv {..} actions -> + ModelEnv {mcEnvWeakFairActions = actions, ..} + +strongFairActions :: Lens' ModelEnv (Set String) +strongFairActions = lens mcEnvStrongFairActions \ModelEnv {..} actions -> + ModelEnv {mcEnvStrongFairActions = actions, ..} diff --git a/src/Language/Spectacle/Model/ModelError.hs b/src/Language/Spectacle/Model/ModelError.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/ModelError.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | Model checker errors. +-- +-- @since 1.0.0 +module Language.Spectacle.Model.ModelError + ( -- * Model Errors + ModelError (InitialError, RuntimeError, RefutedError), + + -- ** Pretty Printing + ppModelError, + ppInitialError, + ppRuntimeError, + + -- * Property Errors + TemporalError (TemporalError), + errorModality, + errorPropName, + errorPrimes, + errorPlains, + + -- ** Pretty Printing + ppTemporalError, + ) +where + +import Data.Kind (Type) +import GHC.TypeLits (Symbol) +import Prettyprinter (Doc, align, indent, line, viaShow, vsep, (<+>)) +import Prettyprinter.Render.Terminal (AnsiStyle) + +import Data.Type.Rec (Ascribe, HasDict) +import Data.World (World, ppWorldListed) +import Language.Spectacle.Exception.RuntimeException (RuntimeException) +import Language.Spectacle.Specification.Prop (Modality, ppModality) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'TemporalError' captures information about a temporal property refutation. +-- +-- @since 1.0.0 +data ModelError :: [Ascribe Symbol Type] -> Type where + InitialError :: + ModelError ctx + RuntimeError :: + RuntimeException -> + ModelError ctx + RefutedError :: + TemporalError ctx -> + ModelError ctx + +-- | @since 1.0.0 +deriving instance HasDict Show ctx => Show (ModelError ctx) + +ppModelError :: HasDict Show ctx => ModelError ctx -> Doc AnsiStyle +ppModelError = \case + InitialError -> ppInitialError + RuntimeError exc -> ppRuntimeError exc + RefutedError err -> ppTemporalError err + +ppInitialError :: Doc AnsiStyle +ppInitialError = "no initial states resulted from evaluating the initial actions" + +ppRuntimeError :: RuntimeException -> Doc AnsiStyle +ppRuntimeError exc = "runtime error:" <+> viaShow exc + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | 'TemporalError' captures information about a temporal property refutation. +-- +-- @since 1.0.0 +data TemporalError ctx = TemporalError + { errorModality :: Modality + , errorPropName :: String + , errorPrimes :: Maybe (World ctx) + , errorPlains :: Maybe (World ctx) + } + +-- | @since 1.0.0 +deriving instance HasDict Show ctx => Show (TemporalError ctx) + +ppTemporalError :: HasDict Show ctx => TemporalError ctx -> Doc AnsiStyle +ppTemporalError TemporalError {..} = + "refuted property:" + <+> ppModality errorModality + <+> viaShow errorPropName + <> line + <> stateList + where + stateList = + let plains = align . mappend "from: " . vsep . ppWorldListed <$> errorPlains + primes = align . mappend "to: " . vsep . ppWorldListed <$> errorPrimes + states = foldMap (maybe [] pure) [plains, primes] + in vsep (map (indent 2 . mappend "* ") states) diff --git a/src/Language/Spectacle/Model/ModelNode.hs b/src/Language/Spectacle/Model/ModelNode.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/ModelNode.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model.ModelNode + ( -- * Model State Nodes + ModelNode (ModelNode), + nodeNextEntries, + nodeValuation, + + -- ** Lenses + nextEntries, + queuedOf, + isEnabled, + isDisabled, + actionsOf, + valuation, + ) +where + +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Set (Set) +import Lens.Micro (Lens', SimpleGetter, lens, to) + +import Data.Fingerprint (Fingerprint) +import Data.Type.Rec (HasDict, Rec) + +-- --------------------------------------------------------------------------------------------------------------------- + +data ModelNode ctx = ModelNode + { nodeNextEntries :: Map String [Fingerprint] + , nodeActionQueue :: Set String + , nodeValuation :: Rec ctx + } + +-- | @since 1.0.0 +deriving instance HasDict Show ctx => Show (ModelNode ctx) + +-- | @'nextEntries' name@ produces a list of 'Fingerprint's following the action named @name@ for the node's +-- valuation. +-- +-- @since 1.0.0 +nextEntries :: String -> Lens' (ModelNode ctx) [Fingerprint] +nextEntries name = + let getter ModelNode {..} = nodeNextEntries Map.! name + setter ModelNode {..} xs = + ModelNode {nodeNextEntries = Map.insert name xs nodeNextEntries, ..} + in lens getter setter + +queuedOf :: Lens' (ModelNode ctx) (Set String) +queuedOf = + let getter ModelNode {..} = nodeActionQueue + setter ModelNode {..} q = ModelNode {nodeActionQueue = q, ..} + in lens getter setter + +-- | Is the action with given name enabled? +-- +-- @since 1.0.0 +isEnabled :: String -> SimpleGetter (ModelNode ctx) Bool +isEnabled name = nextEntries name . to (not . null) + +-- | Is the action with given name disabled? +-- +-- @since 1.0.0 +isDisabled :: String -> SimpleGetter (ModelNode ctx) Bool +isDisabled name = nextEntries name . to null + +-- | 'actionsOf' is a lens focusing on the set of actions taken at a 'ModelNode'. +-- +-- @since 1.0.0 +actionsOf :: SimpleGetter (ModelNode ctx) [String] +actionsOf = to (Map.keys . nodeNextEntries) + +-- | 'nodeValuation' is a lens focusing on the valuation of variables this node represents. +-- +-- @since 1.0.0 +valuation :: SimpleGetter (ModelNode ctx) (Rec ctx) +valuation = to nodeValuation diff --git a/src/Language/Spectacle/Model/ModelState.hs b/src/Language/Spectacle/Model/ModelState.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/ModelState.hs @@ -0,0 +1,57 @@ +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model.ModelState + ( -- * ModelState + ModelState (ModelState), + getModelState, + + -- ** Query + member, + enabledActionsAt, + + -- ** Lenses + indexNode, + queuedActionsAt, + ) +where + +import Data.Coerce (coerce) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap +import Data.Set (Set) +import Lens.Micro (Lens', lens, (^.)) + +import Data.Fingerprint (Fingerprint (Fingerprint)) +import Data.Type.Rec (HasDict) +import Language.Spectacle.Model.ModelNode (ModelNode, actionsOf, isEnabled, queuedOf) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype ModelState ctx = ModelState + {getModelState :: IntMap (ModelNode ctx)} + deriving (Semigroup, Monoid) via IntMap (ModelNode ctx) + +-- | @since 1.0.0 +deriving instance HasDict Show ctx => Show (ModelState ctx) + +indexNode :: Fingerprint -> Lens' (ModelState ctx) (ModelNode ctx) +indexNode ~(Fingerprint hash) = + let getter (ModelState nodes) = nodes IntMap.! hash + setter (ModelState nodes) ns = ModelState (IntMap.insert hash ns nodes) + in lens getter setter + +queuedActionsAt :: Fingerprint -> Lens' (ModelState ctx) (Set String) +queuedActionsAt hash = indexNode hash . queuedOf + +enabledActionsAt :: Fingerprint -> ModelState ctx -> [String] +enabledActionsAt hash st = + let node = st ^. indexNode hash + actions = node ^. actionsOf + in filter (\action -> node ^. isEnabled action) actions + +member :: Fingerprint -> ModelState ctx -> Bool +member hash = IntMap.member (coerce hash) . getModelState diff --git a/src/Language/Spectacle/Model/ModelTemporal.hs b/src/Language/Spectacle/Model/ModelTemporal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/ModelTemporal.hs @@ -0,0 +1,34 @@ +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model.ModelTemporal + ( -- * Model Temporal Formulae + ModelTemporal (ModelTemporal), + modelTemporalName, + getModelTemporal, + + -- ** Construction + fromTemporalSpec, + ) +where + +import Data.Map (Map) +import qualified Data.Map as Map +import Lens.Micro ((^.)) + +import Data.World (World, worldValues) +import Language.Spectacle.AST.Temporal (Temporal, runTemporal) + +-- --------------------------------------------------------------------------------------------------------------------- + +data ModelTemporal ctx = ModelTemporal + { modelTemporalName :: String + , getModelTemporal :: World ctx -> World ctx -> Bool + } + +fromTemporalSpec :: Map String (Temporal ctx Bool) -> [ModelTemporal ctx] +fromTemporalSpec = Map.foldrWithKey (\k v xs -> go k v : xs) [] + where + go name formula = + let runner w0 w1 = runTemporal (w0 ^. worldValues) (w1 ^. worldValues) formula + in ModelTemporal name runner diff --git a/src/Language/Spectacle/Model/Monad.hs b/src/Language/Spectacle/Model/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Model/Monad.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Model.Monad + ( -- * Model Monad + ModelIO, + + -- * Model Transformer + ModelM (ModelM), + unModelM, + runModelM, + + -- * Re-exports + module Language.Spectacle.Model.ModelEnv, + module Language.Spectacle.Model.ModelError, + module Language.Spectacle.Model.ModelState, + ) +where + +import Control.Monad.Except (ExceptT (ExceptT), MonadError, runExceptT) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Reader (MonadReader, ReaderT (ReaderT), runReaderT) +import Control.Monad.Ref (RefM, runRefM) +import Control.Monad.State (MonadState) +import Data.Function ((&)) + +import Language.Spectacle.Model.ModelEnv + ( ModelEnv, + actionInfo, + fairnessOf, + modalityOf, + newModelEnv, + strongFairActions, + unfairActions, + weakFairActions, + ) +import Language.Spectacle.Model.ModelError (ModelError) +import Language.Spectacle.Model.ModelState + ( ModelState, + enabledActionsAt, + indexNode, + member, + queuedActionsAt, + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +type ModelIO ctx = ModelM ctx IO + +newtype ModelM ctx m a = ModelM + {unModelM :: ExceptT (ModelError ctx) (ReaderT ModelEnv (RefM (ModelState ctx) m)) a} + deriving (Functor, Applicative, Monad, MonadIO) + +runModelM :: + MonadIO m => + ModelM ctx m a -> + ModelEnv -> + ModelState ctx -> + m (ModelState ctx, Either (ModelError ctx) a) +runModelM model env st = + unModelM model + & runExceptT + & flip runReaderT env + & flip runRefM st + +-- | @since 1.0.0 +deriving instance MonadIO m => MonadState (ModelState ctx) (ModelM ctx m) + +-- | @since 1.0.0 +deriving instance Monad m => MonadReader ModelEnv (ModelM ctx m) + +-- | @since 1.0.0 +deriving instance Monad m => MonadError (ModelError ctx) (ModelM ctx m) diff --git a/src/Language/Spectacle/RTS/Registers.hs b/src/Language/Spectacle/RTS/Registers.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/RTS/Registers.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | Runtime state used to implement call-by-need evaluation of closures and variable substitution. +-- +-- @since 1.0.0 +module Language.Spectacle.RTS.Registers + ( RuntimeState (RuntimeState, plains, primes, callStack, newValues), + emptyRuntimeState, + Registers (Registers, unRegisters), + emptyRegisters, + getRegister, + setRegister, + setThunk, + StateFun, + type StateFunSyntax, + Thunk (Thunk, Evaluated, Unchanged), + ) +where + +import Data.Functor.Identity (Identity (Identity)) +import Data.Kind (Type) +import GHC.TypeLits (Symbol) + +import Data.Ascript (type (#)) +import Data.Type.Rec (Ascribe, Has, Name, Rec, RecF) +import qualified Data.Type.Rec as Rec +import Language.Spectacle.Exception.RuntimeException (RuntimeException) +import Language.Spectacle.Lang (EffectK, Lang) +import Language.Spectacle.Syntax.Error.Internal (Error) +import Language.Spectacle.Syntax.NonDet.Internal (NonDet) +import Language.Spectacle.Syntax.Plain.Internal (Plain) +import Language.Spectacle.Syntax.Prime.Internal (Prime) + +-- --------------------------------------------------------------------------------------------------------------------- + +type StateFun :: [Ascribe Symbol Type] -> Type -> Type +type StateFun ctx = Lang ctx StateFunSyntax + +type StateFunSyntax :: [EffectK] +type StateFunSyntax = '[Prime, Plain, NonDet, Error RuntimeException] + +-- | Internal state used by variable substitution and variable relations. +-- +-- * 'plains' is a record relating plain variables in @ctx@ to values in the previous frame of time. +-- * 'primes' is a record relating primed or "time" variables in @ctx@ to their values in the next +-- frame of time. +-- * 'callStack' tracks the substitution of primed variables which is used guard against a cyclic +-- variable relations. +-- +-- @since 1.0.0 +data RuntimeState ctx = RuntimeState + { plains :: Rec ctx + , primes :: Registers ctx + , callStack :: [String] + , newValues :: Rec ctx + } + +deriving instance (Show (Rec ctx), Show (Registers ctx)) => Show (RuntimeState ctx) + +emptyRuntimeState :: Rec ctx -> RuntimeState ctx +emptyRuntimeState r = + RuntimeState + { plains = r + , primes = emptyRegisters r + , callStack = mempty + , newValues = r + } + +-- | A record of 'Thunk's. +-- +-- @since 1.0.0 +newtype Registers ctxt = Registers + {unRegisters :: RecF (Thunk ctxt) ctxt} + +deriving instance Show (RecF (Thunk ctxt) ctxt) => Show (Registers ctxt) + +-- | Construct a 'Registers' of unrelated primed variables. +-- +-- @since 1.0.0 +emptyRegisters :: Rec ctx -> Registers ctx +emptyRegisters = Registers . Rec.mapF \_ (Identity _) -> Unchanged + +-- | Retrieves the value of the variable named @s@ in 'Registers' as a 'Thunk'. +-- +-- @since 1.0.0 +getRegister :: Has s a ctx => Name s -> Registers ctx -> Thunk ctx a +getRegister n (Registers rs) = Rec.getF n rs + +-- | Sets the value of the variable named @s@ to the result given by evaluating a 'Thunk'. +-- +-- @since 1.0.0 +setRegister :: Has s a ctx => Name s -> a -> Registers ctx -> Registers ctx +setRegister n x (Registers rs) = Registers (Rec.setF n (Evaluated x) rs) + +-- | Sets the value of the variable named @s@ in 'Registers' to an unevaluated expression. +-- +-- @since 1.0.0 +setThunk :: Has s a ctx => Name s -> StateFun ctx a -> Registers ctx -> Registers ctx +setThunk n m (Registers rs) = Registers (Rec.setF n (Thunk m) rs) + +-- | A 'Thunk' is the state of a primed variable in @ctx@. +-- +-- * 'Thunk' is an unevaluated expression on the right-hand side of a closure. +-- * 'Evaluated' result of evaluating a thunk in current world. +-- * Any primed variable is implicitly 'Unchanged' if it has not been related in the current world. +-- +-- @since 1.0.0 +data Thunk ctxt a + = Thunk (StateFun ctxt a) + | Evaluated a + | Unchanged + +-- | @since 1.0.0 +instance Show a => Show (Thunk (s # a ': ctx) a) where + show (Thunk _) = "<>" + show (Evaluated x) = show x + show Unchanged = "<>" diff --git a/src/Language/Spectacle/Specification.hs b/src/Language/Spectacle/Specification.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Specification.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Language.Spectacle.Specification + ( -- * Specification Constraint + Specification (Specification), + specInit, + specNext, + specProp, + + -- ** Lowering + runInitialSpec, + getActionFormulae, + getTemporalFormulae, + getFairnessSpec, + getModalitySpec, + + -- * Re-export + module Language.Spectacle.Specification.Action, + module Language.Spectacle.Specification.Prop, + module Language.Spectacle.Specification.Variable, + ) +where + +import Data.Function ((&)) +import Data.Hashable (Hashable) +import Data.Kind (Type) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Set (Set) +import qualified Data.Set as Set +import GHC.TypeLits (Symbol) + +import Data.Type.Rec as Rec + ( Ascribe, + HasDict, + RecF, + foldMapF, + mapF, + sequenceF, + ) +import Data.World (World, makeWorld) +import Language.Spectacle.AST.Action (Action) +import Language.Spectacle.AST.Temporal (Temporal) +import Language.Spectacle.Fairness (Fairness) +import Language.Spectacle.Lang (Lang, runLang) +import Language.Spectacle.Specification.Action + ( ActionType (ActionSF, ActionUF, ActionWF), + toAction, + toFairness, + ) +import Language.Spectacle.Specification.Prop + ( Modality (Always, Eventually, Infinitely, Stays), + TemporalType (PropF, PropFG, PropG, PropGF), + toFormula, + toModality, + ) +import Language.Spectacle.Specification.Variable + ( HasVars (runInitActions), + runInitStates, + ) +import Language.Spectacle.Syntax.NonDet (NonDet, runNonDetA) + +-- --------------------------------------------------------------------------------------------------------------------- + +type Specification :: + [Ascribe Symbol Type] -> + [Ascribe Symbol Fairness] -> + [Ascribe Symbol Modality] -> + Type +data Specification ctx acts form where + Specification :: + { specInit :: RecF (Lang '[] '[NonDet]) ctx + , specNext :: RecF (ActionType ctx) acts + , specProp :: RecF (TemporalType ctx) form + } -> + Specification ctx acts form + +runInitialSpec :: HasDict Hashable ctx => Specification ctx acts form -> Set (World ctx) +runInitialSpec spec = + specInit spec + & Rec.mapF (\_ -> runLang . runNonDetA @[]) + & Rec.sequenceF + & foldMap (Set.singleton . makeWorld) + +getActionFormulae :: Specification ctx acts form -> Map String (Action ctx Bool) +getActionFormulae = Rec.foldMapF (\nm act -> Map.singleton (show nm) (toAction act)) . specNext + +getTemporalFormulae :: Specification ctx acts form -> Map String (Temporal ctx Bool) +getTemporalFormulae = Rec.foldMapF (\nm form -> Map.singleton (show nm) (toFormula form)) . specProp + +getFairnessSpec :: Specification ctx acts form -> Map String Fairness +getFairnessSpec = Rec.foldMapF (\nm act -> Map.singleton (show nm) (toFairness act)) . specNext + +getModalitySpec :: Specification ctx acts form -> Map String Modality +getModalitySpec = Rec.foldMapF (\nm form -> Map.singleton (show nm) (toModality form)) . specProp diff --git a/src/Language/Spectacle/Specification/Action.hs b/src/Language/Spectacle/Specification/Action.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Specification/Action.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Specification.Action + ( -- * ActionType + ActionType (ActionUF, ActionWF, ActionSF), + + -- ** Projection + toAction, + toFairness, + ) +where + +import Data.Kind (Type) +import GHC.TypeLits (Symbol) + +import Data.Type.Rec (Ascribe) +import Language.Spectacle.AST.Action (Action) +import Language.Spectacle.Fairness (Fairness (StrongFair, Unfair, WeakFair), reifyFairness) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Action declarations. +-- +-- @since 1.0.0 +data ActionType :: [Ascribe Symbol Type] -> Fairness -> Type where + ActionUF :: Action ctx Bool -> ActionType ctx 'Unfair + ActionWF :: Action ctx Bool -> ActionType ctx 'WeakFair + ActionSF :: Action ctx Bool -> ActionType ctx 'StrongFair + +toAction :: ActionType ctx fair -> Action ctx Bool +toAction (ActionUF act) = act +toAction (ActionWF act) = act +toAction (ActionSF act) = act + +toFairness :: forall ctx fair. ActionType ctx fair -> Fairness +toFairness ActionUF {} = reifyFairness @fair +toFairness ActionWF {} = reifyFairness @fair +toFairness ActionSF {} = reifyFairness @fair diff --git a/src/Language/Spectacle/Specification/Prop.hs b/src/Language/Spectacle/Specification/Prop.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Specification/Prop.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Specification.Prop + ( -- * Temporal Formula + TemporalType (PropG, PropF, PropGF, PropFG), + + -- ** Projection + toFormula, + toModality, + + -- * Temporal Operators + Modality (Always, Infinitely, Eventually, Stays), + + -- ** Pretty Printing + ppModality, + ) +where + +import Data.Kind (Type) +import GHC.TypeLits (Symbol) +import Prettyprinter (Doc) +import Prettyprinter.Render.Terminal (AnsiStyle) + +import Data.Ascript (Ascribe) +import Language.Spectacle.AST.Temporal (Temporal) + +-- --------------------------------------------------------------------------------------------------------------------- + +data TemporalType :: [Ascribe Symbol Type] -> Modality -> Type where + PropG :: Temporal ctx Bool -> TemporalType ctx 'Always + PropF :: Temporal ctx Bool -> TemporalType ctx 'Eventually + PropGF :: Temporal ctx Bool -> TemporalType ctx 'Infinitely + PropFG :: Temporal ctx Bool -> TemporalType ctx 'Stays + +toFormula :: TemporalType ctx op -> Temporal ctx Bool +toFormula = \case + PropG form -> form + PropF form -> form + PropGF form -> form + PropFG form -> form + +toModality :: TemporalType ctx op -> Modality +toModality = \case + PropG {} -> Always + PropF {} -> Eventually + PropGF {} -> Infinitely + PropFG {} -> Stays + +data Modality + = Always + | Eventually + | Infinitely + | Stays + deriving stock (Eq, Enum, Ord, Show) + +ppModality :: Modality -> Doc AnsiStyle +ppModality = \case + Always -> "always" + Eventually -> "eventually" + Infinitely -> "infinitely" + Stays -> "stays-as" diff --git a/src/Language/Spectacle/Specification/Variable.hs b/src/Language/Spectacle/Specification/Variable.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Specification/Variable.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | +-- +-- @since 1.0.0 +module Language.Spectacle.Specification.Variable + ( -- * Syntax + Var ((:=)), + type (:.) ((:.)), + + -- * Variable Constraints + HasVars, + type VarCtxt, + runInitActions, + runInitStates, + ) +where + +import Control.Applicative (Applicative (liftA2)) +import Data.Hashable (Hashable) +import Data.Kind (Type) +import GHC.TypeLits (Symbol) + +import Data.Type.List (type (++)) +import Data.Type.Rec (Ascribe, HasDict, Name, Rec, RecF (ConF, NilF), pattern Con, pattern Nil, type (#)) +import qualified Data.Type.Rec as Rec +import Data.World (World, makeWorld) +import Language.Spectacle.Lang (Lang, runLang) +import Language.Spectacle.Syntax.NonDet (NonDet, runNonDetA) + +infixr 5 :. + +-- --------------------------------------------------------------------------------------------------------------------- + +data Var :: Symbol -> Type -> Type where + (:=) :: Name s -> Lang '[] '[NonDet] a -> Var s a + +data (:.) :: Type -> Type -> Type where + (:.) :: a -> b -> a :. b + +class HasVars a where + type VarCtxt a :: [Ascribe Symbol Type] + + runInitActions :: VarCtxt a ~ ctxt => a -> RecF (Lang '[] '[NonDet]) ctxt + +-- | @since 1.0.0 +instance (HasVars a, HasVars b) => HasVars (a :. b) where + type VarCtxt (a :. b) = VarCtxt a ++ VarCtxt b + + runInitActions (xs :. ys) = Rec.concatF (runInitActions xs) (runInitActions ys) + {-# INLINE runInitActions #-} + +-- | @since 1.0.0 +instance HasVars (Var var ty) where + type VarCtxt (Var var ty) = (var # ty) ': '[] + + runInitActions (name := act) = ConF name act NilF + {-# INLINE runInitActions #-} + +runInitStates :: forall vars ctx. (HasVars vars, HasDict Hashable ctx, VarCtxt vars ~ ctx) => vars -> [World ctx] +runInitStates vs = map makeWorld (go acts) + where + go :: RecF [] ctx' -> [Rec ctx'] + go NilF = [Nil] + go (ConF nm xs rs) = liftA2 (Con nm) xs (go rs) + + runner :: Name s -> Lang ctx' '[NonDet] a -> [a] + runner _ = runLang . runNonDetA @[] + + acts :: RecF [] ctx + acts = Rec.mapF runner (runInitActions vs) diff --git a/src/Language/Spectacle/Syntax.hs b/src/Language/Spectacle/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax.hs @@ -0,0 +1,64 @@ +module Language.Spectacle.Syntax + ( -- * Closures + (.=), + + -- * Errors + catchE, + throwE, + + -- * Logic + conjunct, + (/\), + disjunct, + (\/), + complement, + (==>), + implies, + (<=>), + iff, + + -- * Nondeterminism + oneOf, + + -- * Variables + plain, + prime, + + -- * Quantifiers + forall, + exists, + + -- * Enabled + enabled, + ) +where + +import Language.Spectacle.Lang (Lang, Member) +import Language.Spectacle.Syntax.Closure ((.=)) +import Language.Spectacle.Syntax.Enabled (enabled) +import Language.Spectacle.Syntax.Error (catchE, throwE) +import Language.Spectacle.Syntax.Logic (Logic, complement, conjunct, disjunct, iff, implies) +import Language.Spectacle.Syntax.NonDet (oneOf) +import Language.Spectacle.Syntax.Plain (plain) +import Language.Spectacle.Syntax.Prime (prime) +import Language.Spectacle.Syntax.Quantifier (exists, forall) + +-- --------------------------------------------------------------------------------------------------------------------- + +infixl 5 /\ +(/\) :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +(/\) = conjunct +{-# INLINE (/\) #-} + +infixl 5 \/ +(\/) :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +(\/) = disjunct +{-# INLINE (\/) #-} + +(==>) :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +(==>) = implies +{-# INLINE (==>) #-} + +(<=>) :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +(<=>) = iff +{-# INLINE (<=>) #-} diff --git a/src/Language/Spectacle/Syntax/Closure.hs b/src/Language/Spectacle/Syntax/Closure.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Closure.hs @@ -0,0 +1,125 @@ +-- | Closures and variable relations. +-- +-- @since 1.0.0 +module Language.Spectacle.Syntax.Closure + ( Closure (Closure), + Effect (Close), + (.=), + runActionClosure, + ) +where + +import Data.Coerce (coerce) +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Data.Type.Rec (Has, Name) +import qualified Data.Type.Rec as Rec +import Language.Spectacle.Exception.RuntimeException (RuntimeException) +import Language.Spectacle.Lang + ( Effect, + Lang (Op, Pure, Scoped), + Member (project, projectS), + Members, + decomposeOp, + decomposeS, + scope, + ) +import Language.Spectacle.RTS.Registers + ( RuntimeState (newValues), + StateFun, + Thunk (Evaluated, Thunk, Unchanged), + getRegister, + setThunk, + ) +import Language.Spectacle.Syntax.Closure.Internal (Closure (Closure), Effect (Close)) +import Language.Spectacle.Syntax.Env (Env, gets, modify) +import Language.Spectacle.Syntax.Error (Error) +import Language.Spectacle.Syntax.NonDet (NonDet) +import Language.Spectacle.Syntax.Prime (RuntimeState (primes), substitute) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | The ('.=') operator relates the variable @s@ to the primed values it can access in the next temporal frame. For +-- example, a relation which increments a variable named "x" with any number 1 through 5 each frame of time would be +-- written as: +-- +-- @ +-- increment :: Action IncrementSpec Bool +-- increment = do +-- x <- plain #x -- retrieve the value of "x" from the previous frame +-- exists [1 .. 5] \n -> do +-- #x .= return (x + n) -- set the value of "x" in the next value to x + n for some number 1 <= n <= 5 +-- return True -- relate the value to the next frame, @return (odd n)@ could be written to exclude even n. +-- @ +-- +-- @since 1.0.0 +infix 4 .= + +(.=) :: (Member Closure effs, Has s a ctx) => Name s -> StateFun ctx a -> Lang ctx effs () +name .= expr = scope (Close name expr) +{-# INLINE (.=) #-} + +-- | Discharges a 'Closure' effect, returning a 'Rec' new values for each variable in @ctx@. +-- +-- @since 1.0.0 +runActionClosure :: + Members '[NonDet, Env, Error RuntimeException] effs => + Lang ctx (Closure ': effs) a -> + Lang ctx effs a +runActionClosure m = evaluateThunks (makeThunks m) +{-# INLINE runActionClosure #-} + +-- | Evaluates all unevaluated closures in a specification. +-- +-- @since 1.0.0 +evaluateThunks :: + Members '[NonDet, Env, Error RuntimeException] effs => + Lang ctx (Closure ': effs) a -> + Lang ctx effs a +evaluateThunks = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other k' + Right bottom -> absurd (coerce bottom) + where + k' = evaluateThunks . k + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loom' + Right (Close name _) -> + gets (getRegister name . primes) >>= \case + Thunk expr -> do + x <- substitute name expr + modify \rtst -> rtst {newValues = Rec.set name x (newValues rtst)} + runLoom loom' (pure ()) + Evaluated x -> do + modify \rtst -> rtst {newValues = Rec.set name x (newValues rtst)} + runLoom loom' (pure ()) + Unchanged -> runLoom loom' (pure ()) + where + loom' = loom ~>~ hoist evaluateThunks + +-- | Traverses 'Lang' collecting all closures as 'Thunks' which will subsequently be evaluated +-- by 'evaluateThunks'. An extra pass is needed to register all closures before substitution of +-- primed variables takes place. +-- +-- @since 1.0.0 +makeThunks :: + Members '[Closure, Env, Error RuntimeException] effs => + Lang ctx effs a -> + Lang ctx effs a +makeThunks = \case + Pure x -> pure x + Op op k -> case project op of + Nothing -> Op op k' + Just (Closure bottom :: Closure x) -> absurd bottom + where + k' = makeThunks . k + Scoped scoped loom -> case projectS scoped of + Nothing -> Scoped scoped loom' + Just (Close name expr) -> do + modify \rtst -> rtst {primes = setThunk name expr (primes rtst)} + scope (Close name expr) + runLoom loom' (pure ()) + where + loom' = loom ~>~ hoist makeThunks diff --git a/src/Language/Spectacle/Syntax/Closure/Internal.hs b/src/Language/Spectacle/Syntax/Closure/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Closure/Internal.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Closure.Internal + ( Closure (Closure), + Effect (Close), + ) +where + +import Data.Void (Void) + +import Data.Name (Name) +import Data.Type.Rec (Has) +import Language.Spectacle.Lang (Effect, EffectK, Lang, ScopeK) +import Language.Spectacle.RTS.Registers (StateFun) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype Closure :: EffectK where + Closure :: Void -> Closure a + +data instance Effect Closure :: ScopeK where + Close :: + (Has s a ctx, m ~ Lang ctx effs) => + Name s -> + StateFun ctx a -> + Effect Closure m () diff --git a/src/Language/Spectacle/Syntax/Enabled.hs b/src/Language/Spectacle/Syntax/Enabled.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Enabled.hs @@ -0,0 +1,40 @@ +module Language.Spectacle.Syntax.Enabled + ( -- * Labels + Enabled (Enabled), + Effect (EnabledS), + enabled, + + -- ** Interpreters + runEnabled, + ) +where + +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, (~>~)) +import Language.Spectacle.Lang + ( Effect, + Lang (Op, Pure, Scoped), + Member, + decomposeOp, + decomposeS, + send, + ) +import Language.Spectacle.Syntax.Enabled.Internal (Effect (EnabledS), Enabled (Enabled)) + +-- --------------------------------------------------------------------------------------------------------------------- + +enabled :: Member Enabled effs => Lang ctx effs Bool +enabled = send Enabled +{-# INLINE enabled #-} + +runEnabled :: Bool -> Lang ctx (Enabled : effs) a -> Lang ctx effs a +runEnabled isEnabled = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (runEnabled isEnabled . k) + Right Enabled -> runEnabled isEnabled (k isEnabled) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other (loom ~>~ hoist (runEnabled isEnabled)) + Right (EnabledS bottom) -> absurd bottom +{-# INLINE runEnabled #-} diff --git a/src/Language/Spectacle/Syntax/Enabled/Internal.hs b/src/Language/Spectacle/Syntax/Enabled/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Enabled/Internal.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Enabled.Internal + ( Enabled (Enabled), + Effect (EnabledS), + ) +where + +import Data.Void (Void) + +import Language.Spectacle.Lang (Effect, EffectK, ScopeK) + +-- --------------------------------------------------------------------------------------------------------------------- + +data Enabled :: EffectK where + Enabled :: Enabled Bool + +newtype instance Effect Enabled :: ScopeK where + EnabledS :: Void -> Effect Enabled m a diff --git a/src/Language/Spectacle/Syntax/Env.hs b/src/Language/Spectacle/Syntax/Env.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Env.hs @@ -0,0 +1,50 @@ +module Language.Spectacle.Syntax.Env + ( Env (Env), + Effect (Get, Put), + get, + gets, + put, + modify, + runEnv, + ) +where + +import Data.Coerce (coerce) +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Language.Spectacle.Lang (Effect, Lang (Op, Pure, Scoped), Member, decomposeOp, decomposeS, scope) +import Language.Spectacle.RTS.Registers (RuntimeState) +import Language.Spectacle.Syntax.Env.Internal (Effect (Get, Put), Env (Env)) + +-- --------------------------------------------------------------------------------------------------------------------- + +get :: Member Env effs => Lang ctx effs (RuntimeState ctx) +get = scope Get +{-# INLINE get #-} + +gets :: Member Env effs => (RuntimeState ctx -> s) -> Lang ctx effs s +gets f = fmap f get +{-# INLINE gets #-} + +put :: Member Env effs => RuntimeState ctx -> Lang ctx effs () +put x = scope (Put x) +{-# INLINE put #-} + +modify :: Member Env effs => (RuntimeState ctx -> RuntimeState ctx) -> Lang ctx effs () +modify f = get >>= put . f +{-# INLINE modify #-} + +runEnv :: RuntimeState ctx -> Lang ctx (Env ': effs) a -> Lang ctx effs (RuntimeState ctx, a) +runEnv st = \case + Pure x -> pure (st, x) + Op op k -> case decomposeOp op of + Left other -> Op other (runEnv st . k) + Right (Env b) -> absurd (coerce b) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other (loom' st) + Right eff + | Get <- eff -> runLoom (loom' st) (pure st) + | Put st' <- eff -> runLoom (loom' st') (pure ()) + where + loom' st' = loom ~>~ hoist (runEnv st') diff --git a/src/Language/Spectacle/Syntax/Env/Internal.hs b/src/Language/Spectacle/Syntax/Env/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Env/Internal.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Env.Internal + ( Env (Env), + Effect (Get, Put), + ) +where + +import Data.Void (Void) + +import Language.Spectacle.Lang (Effect, EffectK) +import Language.Spectacle.RTS.Registers (RuntimeState) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype Env :: EffectK where + Env :: Void -> Env a + +data instance Effect Env m a where + Get :: m ~ f ctx effs => Effect Env m (RuntimeState ctx) + Put :: m ~ f ctx effs => RuntimeState ctx -> Effect Env m () diff --git a/src/Language/Spectacle/Syntax/Error.hs b/src/Language/Spectacle/Syntax/Error.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Error.hs @@ -0,0 +1,55 @@ +-- | The 'Error' effect for throwing exceptions which can be caught. +-- +-- @since 1.0.0 +module Language.Spectacle.Syntax.Error + ( Error (ThrowE), + Effect (CatchE), + throwE, + catchE, + runError, + ) +where + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Language.Spectacle.Lang + ( Effect, + Lang (Op, Pure, Scoped), + Member, + decomposeOp, + decomposeS, + scope, + send, + ) +import Language.Spectacle.Syntax.Error.Internal (Effect (CatchE), Error (ThrowE)) + +-- ------------------------------------------------------------------------------------------------- + +-- | Throw an error of type @e@, escaping the current continuation up to the nearest enclosing +-- 'catchE'. +-- +-- @since 1.0.0 +throwE :: Member (Error e) effs => e -> Lang ctx effs a +throwE e = send (ThrowE e) + +-- | Catch an error of type @e@ continuting from the provided function if an error was thrown. +-- +-- @since 1.0.0 +catchE :: Member (Error e) effs => Lang ctx effs a -> (e -> Lang ctx effs a) -> Lang ctx effs a +catchE m f = scope (CatchE m f) + +-- | Discharge an 'Error' effect into either an error or the result of a successful computation. +-- +-- @since 1.0.0 +runError :: Lang ctx (Error e ': effs) a -> Lang ctx effs (Either e a) +runError = \case + Pure x -> pure (Right x) + Op op k -> case decomposeOp op of + Left other -> Op other (runError . k) + Right (ThrowE exc) -> pure (Left exc) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loom' + Right (CatchE m catch) -> do + x <- runLoom loom' m + either (runLoom loom' . catch) (pure . pure) x + where + loom' = loom ~>~ hoist runError diff --git a/src/Language/Spectacle/Syntax/Error/Internal.hs b/src/Language/Spectacle/Syntax/Error/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Error/Internal.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Error.Internal + ( Error (ThrowE), + Effect (CatchE), + ) +where + +import Language.Spectacle.Lang (Effect, EffectK, ScopeK) + +-- ------------------------------------------------------------------------------------------------- + +newtype Error e :: EffectK where + ThrowE :: e -> Error e a + +data instance Effect (Error e) :: ScopeK where + CatchE :: m a -> (e -> m a) -> Effect (Error e) m a diff --git a/src/Language/Spectacle/Syntax/Logic.hs b/src/Language/Spectacle/Syntax/Logic.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Logic.hs @@ -0,0 +1,93 @@ +-- | Quantifiers and logic. +-- +-- @since 1.0.0 +module Language.Spectacle.Syntax.Logic + ( Logic (Logic), + Effect (Complement, Conjunct, Disjunct), + complement, + conjunct, + disjunct, + implies, + iff, + runLogic, + ) +where + +import Control.Applicative (Alternative ((<|>)), Applicative (liftA2), empty) +import Data.Coerce (coerce) +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Language.Spectacle.Exception.RuntimeException (RuntimeException) +import Language.Spectacle.Lang + ( Lang (Op, Pure, Scoped), + Member, + Members, + decomposeOp, + decomposeS, + scope, + ) +import Language.Spectacle.Syntax.Error (Error, catchE) +import Language.Spectacle.Syntax.Logic.Internal (Effect (Complement, Conjunct, Disjunct), Logic (Logic)) +import Language.Spectacle.Syntax.NonDet (NonDet) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Logical negation. The 'complement' operator is equivalent to 'not' for simple expressions, but +-- can be used to negate quantifiers and the other logical operators in spectacle. +-- +-- @since 1.0.0 +complement :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool +complement m = scope (Complement m) +{-# INLINE complement #-} + +-- | Boolean conjunction. +-- +-- @since 1.0.0 +conjunct :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +conjunct m n = scope (Conjunct m n) +{-# INLINE conjunct #-} + +-- | Boolean disjunction. +-- +-- @since 1.0.0 +disjunct :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +disjunct m n = scope (Disjunct m n) +{-# INLINE disjunct #-} + +-- | Logical implication. +-- +-- @since 1.0.0 +implies :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +implies m n = disjunct (complement m) n +{-# INLINE implies #-} + +-- | If and only if. +-- +-- @since 1.0.0 +iff :: Member Logic effs => Lang ctx effs Bool -> Lang ctx effs Bool -> Lang ctx effs Bool +iff m n = conjunct (implies m n) (implies n m) +{-# INLINE iff #-} + +-- | Discharge a 'Logic' effect. +-- +-- @since 1.0.0 +runLogic :: + forall ctx effs. + Members '[Error RuntimeException, NonDet] effs => + Lang ctx (Logic ': effs) Bool -> + Lang ctx effs Bool +runLogic = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (runLogic . k) + Right bottom -> absurd (coerce bottom) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loom' + Right (Complement m) -> runLoom loom' (fmap not m) + Right (Conjunct m n) -> liftA2 (&&) (runLoom loom' m) (runLoom loom' n) + Right (Disjunct m n) -> + (runLoom loom' m `catchE` \(_ :: RuntimeException) -> empty) + <|> (runLoom loom' n `catchE` \(_ :: RuntimeException) -> empty) + where + loom' = loom ~>~ hoist runLogic diff --git a/src/Language/Spectacle/Syntax/Logic/Internal.hs b/src/Language/Spectacle/Syntax/Logic/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Logic/Internal.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Logic.Internal + ( Logic (Logic), + Effect (Complement, Conjunct, Disjunct), + ) +where + +import Data.Void (Void) + +import Language.Spectacle.Lang (Effect, EffectK, ScopeK) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype Logic :: EffectK where + Logic :: Void -> Logic a + +data instance Effect Logic :: ScopeK where + Complement :: m Bool -> Effect Logic m Bool + Conjunct :: m Bool -> m Bool -> Effect Logic m Bool + Disjunct :: m Bool -> m Bool -> Effect Logic m Bool diff --git a/src/Language/Spectacle/Syntax/NonDet.hs b/src/Language/Spectacle/Syntax/NonDet.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/NonDet.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE TupleSections #-} + +-- | The 'NonDet' effect models nondeterminism. +-- +-- @since 1.0.0 +module Language.Spectacle.Syntax.NonDet + ( NonDet (Choose, Empty), + Effect (MSplit), + oneOf, + foldMapA, + msplit, + runNonDetA, + ) +where + +import Control.Applicative (Alternative (empty, (<|>)), Applicative (liftA2)) +import Data.Foldable (msum) +import Data.Monoid (Alt (Alt, getAlt)) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Language.Spectacle.Lang + ( Effect, + Lang (Op, Pure, Scoped), + Member (project), + decomposeOp, + decomposeS, + scope, + ) +import Language.Spectacle.Syntax.NonDet.Internal (Effect (MSplit), NonDet (Choose, Empty)) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Nondeterministically choose an element from a foldable container. +-- +-- @since 1.0.0 +oneOf :: (Foldable t, Alternative m) => t a -> m a +oneOf = foldMapA pure +{-# INLINE oneOf #-} + +-- | Like `foldMap`, but folds under 'Alternative' rather than 'Monoid'. +-- +-- @since 1.0.0 +foldMapA :: (Foldable t, Alternative m) => (a -> m b) -> t a -> m b +foldMapA f = getAlt . foldMap (Alt . f) +{-# INLINE foldMapA #-} + +-- | Splits a 'Lang' into its 'Alternative' branches, if it has any. +-- +-- @since 1.0.0 +msplit :: Member NonDet effs => Lang ctx effs a -> Lang ctx effs (Maybe (Lang ctx effs a, Lang ctx effs a)) +msplit m = scope (MSplit m) +{-# INLINE msplit #-} + +-- | Discharge a 'NonDet' effect into some 'Alternative' functor @f@. +-- +-- @since 1.0.0 +runNonDetA :: Alternative f => Lang ctx (NonDet ': effs) a -> Lang ctx effs (f a) +runNonDetA = \case + Pure x -> pure (pure x) + Op op k -> case decomposeOp op of + Left other -> Op other k' + Right Empty -> pure empty + Right Choose -> liftA2 (<|>) (k' True) (k' False) + where + k' = runNonDetA . k + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other (loom ~>~ hoist runNonDetA) + Right (MSplit m) -> runLoom (loom ~>~ hoist runNonDetA) (handleMSplit m) + where + handleMSplit :: Member NonDet effs => Lang ctx effs a -> Lang ctx effs (Maybe (Lang ctx effs a, Lang ctx effs a)) + handleMSplit = loop [] + where + loop xs (Pure x) = pure (Just (pure x, msum xs)) + loop xs (Op op k) = case project op of + Nothing -> Op op (loop xs . k) + Just Empty -> case xs of + [] -> pure Nothing + (x : xs') -> loop xs' x + Just Choose -> loop (k False : xs) (k True) + loop xs (Scoped scoped loom) = Scoped scoped (loom ~>~ hoist (loop xs)) diff --git a/src/Language/Spectacle/Syntax/NonDet/Internal.hs b/src/Language/Spectacle/Syntax/NonDet/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/NonDet/Internal.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.NonDet.Internal + ( NonDet (Empty, Choose), + Effect (MSplit), + ) +where + +import Language.Spectacle.Lang.Member (Member) +import Language.Spectacle.Lang.Scoped (Effect) + +-- --------------------------------------------------------------------------------------------------------------------- + +data NonDet a where + Empty :: NonDet a + Choose :: NonDet Bool + +data instance Effect NonDet m a where + MSplit :: (m ~ f ctx effs, Member NonDet effs) => m a -> Effect NonDet m (Maybe (m a, m a)) diff --git a/src/Language/Spectacle/Syntax/Plain.hs b/src/Language/Spectacle/Syntax/Plain.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Plain.hs @@ -0,0 +1,45 @@ +-- | Plain or known variable usage and substitution. +-- +-- @since 1.0.0 +module Language.Spectacle.Syntax.Plain + ( Plain (Plain), + Effect (PlainVar), + plain, + runPlain, + ) +where + +import Data.Coerce (coerce) +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Data.Type.Rec (Has, Name, Rec) +import qualified Data.Type.Rec as Rec +import Language.Spectacle.Lang (Lang (Op, Pure, Scoped), Member, decomposeOp, decomposeS, scope) +import Language.Spectacle.Syntax.Plain.Internal (Effect (PlainVar), Plain (Plain)) + +-- ------------------------------------------------------------------------------------------------- + +-- | 'plain' for a variable named @s@ is the value of @s@ from the previous frame of time. +-- +-- @since 1.0.0 +plain :: (Member Plain effs, Has s a ctx) => Name s -> Lang ctx effs a +plain nm = scope (PlainVar nm) +{-# INLINE plain #-} + +-- | Discharge a 'Plain' effect, substituting instances of 'PlainVar' for the values in the given +-- 'Data.Type.Rec'. +-- +-- @since 1.0.0 +runPlain :: Rec ctx -> Lang ctx (Plain ': effs) a -> Lang ctx effs a +runPlain vars = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (runPlain vars . k) + Right bottom -> absurd (coerce bottom) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loom' + Right (PlainVar name) -> do + runLoom loom' (pure $ Rec.get name vars) + where + loom' = loom ~>~ hoist (runPlain vars) diff --git a/src/Language/Spectacle/Syntax/Plain/Internal.hs b/src/Language/Spectacle/Syntax/Plain/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Plain/Internal.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Language.Spectacle.Syntax.Plain.Internal + ( Plain (Plain), + Effect (PlainVar), + ) +where + +import Data.Void (Void) + +import Data.Type.Rec (Has, Name) +import Language.Spectacle.Lang (Effect, EffectK, Lang) + +-- ------------------------------------------------------------------------------------------------- + +newtype Plain :: EffectK where + Plain :: Void -> Plain a + +data instance Effect Plain m a where + PlainVar :: (Has s a ctx, m ~ Lang ctx effs) => Name s -> Effect Plain m a diff --git a/src/Language/Spectacle/Syntax/Prime.hs b/src/Language/Spectacle/Syntax/Prime.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Prime.hs @@ -0,0 +1,167 @@ +-- | Prime (or time) variable usage and substitution. +-- +-- @since 1.0.0 +module Language.Spectacle.Syntax.Prime + ( -- * Labels + Prime (Prime), + Effect (PrimeVar), + + -- * Syntax + prime, + + -- * Interpreters + runPrime, + substPrime, + RuntimeState (RuntimeState, plains, primes, callStack), + substitute, + ) +where + +import Data.Coerce (coerce) +import Data.Function ((&)) +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Data.Type.Rec (Has, Name, Rec) +import qualified Data.Type.Rec as Rec +import Language.Spectacle.Exception.RuntimeException + ( RuntimeException (VariableException), + VariableException (CyclicReference), + ) +import Language.Spectacle.Lang + ( Effect, + Lang (Op, Pure, Scoped), + Member, + Members, + Op (OHere, OThere), + Scoped (SHere, SThere), + decomposeOp, + decomposeS, + runLang, + scope, + ) +import Language.Spectacle.RTS.Registers + ( RuntimeState (RuntimeState, callStack, plains, primes), + StateFun, + Thunk (Evaluated, Thunk, Unchanged), + getRegister, + setRegister, + ) +import Language.Spectacle.Syntax.Env + ( Env, + get, + gets, + modify, + put, + runEnv, + ) +import Language.Spectacle.Syntax.Error (Error, runError, throwE) +import Language.Spectacle.Syntax.NonDet (NonDet, oneOf, runNonDetA) +import Language.Spectacle.Syntax.Plain (runPlain) +import Language.Spectacle.Syntax.Prime.Internal + ( Effect (PrimeVar), + Prime (Prime), + ) + +-- ------------------------------------------------------------------------------------------------- + +-- | 'prime' for a variable named @s@ is the value of @s@ in the next time frame. +-- +-- @since 1.0.0 +prime :: (Member Prime effs, Has s a ctx) => Name s -> Lang ctx effs a +prime nm = scope (PrimeVar nm) +{-# INLINE prime #-} + +-- | Discharges a 'Prime' effect. This interpreter carries out the substitution of primed variables +-- using a call-by-need evaluation strategy. +-- +-- @since 1.0.0 +runPrime :: + forall ctx effs a. + Members '[Env, Error RuntimeException, NonDet] effs => + Lang ctx (Prime ': effs) a -> + Lang ctx effs a +runPrime = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (runPrime . k) + Right bottom -> absurd (coerce bottom) + Scoped scoped loom -> do + case decomposeS scoped of + Left other -> Scoped other loomPrime + Right (PrimeVar name) -> do + rst <- get + case getRegister name (primes rst) of + Thunk expr -> + if show name `elem` callStack rst + then throwE (VariableException (CyclicReference (callStack rst))) + else do + x <- substitute name expr + modify \rst' -> + rst' {primes = setRegister name x (primes rst')} + runLoom loomPrime (pure x) + Evaluated x -> runLoom loomPrime (pure x) + Unchanged -> do + rst' <- gets (Rec.get name . plains) + runLoom loomPrime (pure rst') + where + loomPrime = loom ~>~ hoist runPrime + +-- | Alternative interpreter for 'Prime' that substitutes with a 'Rec' rather than a record of +-- thunks. +-- +-- @since 1.0.0 +substPrime :: Rec ctx -> Lang ctx (Prime ': effs) a -> Lang ctx effs a +substPrime vars = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (substPrime vars . k) + Right bottom -> absurd (coerce bottom) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loomSubstPrime + Right (PrimeVar name) -> do + runLoom loomSubstPrime (pure $ Rec.get name vars) + where + loomSubstPrime = loom ~>~ hoist (substPrime vars) + +-- | Evaluates the thunk for a primed variable. +-- +-- @since 1.0.0 +substitute :: + (Members '[Env, NonDet, Error RuntimeException] effs, Has s a ctx) => + Name s -> + StateFun ctx a -> + Lang ctx effs a +substitute name expr = do + rst <- get + let result = + expr + & introduceState + & runPrime + & runEnv rst + & runPlain (plains rst) + & runNonDetA @[] + & runError + & runLang + case result of + Left e -> throwE e + Right results -> do + (rst', x) <- oneOf results + put (rst' {primes = setRegister name x (primes rst')}) + pure x + where + introduceState :: + Lang ctx (Prime : effs) a -> + Lang ctx (Prime ': Env ': effs) a + introduceState = \case + Pure x -> pure x + Op op k + | OHere op' <- op -> Op (OHere op') k' + | OThere op' <- op -> Op (OThere (OThere op')) k' + where + k' = introduceState . k + Scoped scoped loom + | SHere scoped' <- scoped -> Scoped (SHere scoped') loom' + | SThere scoped' <- scoped -> Scoped (SThere (SThere scoped')) loom' + where + loom' = loom ~>~ hoist introduceState diff --git a/src/Language/Spectacle/Syntax/Prime/Internal.hs b/src/Language/Spectacle/Syntax/Prime/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Prime/Internal.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Prime.Internal + ( Prime (Prime), + Effect (PrimeVar), + ) +where + +import Data.Void (Void) + +import Data.Type.Rec (Has, Name) +import Language.Spectacle.Lang (Effect, EffectK, Lang) + +-- ------------------------------------------------------------------------------------------------- + +newtype Prime :: EffectK where + Prime :: Void -> Prime a + +data instance Effect Prime m a where + PrimeVar :: (Has s a ctx, m ~ Lang ctx eff) => Name s -> Effect Prime m a diff --git a/src/Language/Spectacle/Syntax/Quantifier.hs b/src/Language/Spectacle/Syntax/Quantifier.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Quantifier.hs @@ -0,0 +1,98 @@ +module Language.Spectacle.Syntax.Quantifier + ( Quantifier (Quantifier), + Effect (Forall, Exists), + forall, + exists, + runExceptionalQuantifier, + runQuantifier, + ) +where + +import Control.Applicative (Alternative (empty), Applicative (liftA2)) +import Control.Monad (unless) +import Data.Bool (bool) +import Data.Coerce (coerce) +import Data.Foldable (Foldable (toList)) +import Data.Void (absurd) + +import Data.Functor.Loom (hoist, runLoom, (~>~)) +import Language.Spectacle.Exception.RuntimeException + ( QuantifierException (ExistsViolated, ForallViolated), + RuntimeException (QuantifierException), + ) +import Language.Spectacle.Lang + ( Effect, + Lang (Op, Pure, Scoped), + Members, + decomposeOp, + decomposeS, + ) +import Language.Spectacle.Syntax.Error (Error, catchE, throwE) +import Language.Spectacle.Syntax.NonDet (NonDet, foldMapA, msplit, oneOf) +import Language.Spectacle.Syntax.Quantifier.Internal + ( Effect (Exists, Forall), + Quantifier (Quantifier), + QuantifierIntro (forallIntro), + existsIntro, + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Universally quantify over some foldable container @f a@. A nondeterministically chosen element in @f a@ will be +-- returned so long as the given predicate is 'True' for all elements in the container, otherwise a spectacle exception +-- is raised. +-- +-- @since 1.0.0 +forall :: (Foldable f, QuantifierIntro m) => f a -> (a -> m Bool) -> m Bool +forall xs = forallIntro (toList xs) +{-# INLINE forall #-} + +-- | Existential quantification over some foldable constainer @f a@. A nondeterministically chosen element in @f a@ +-- which satisfies the given predicate will be returned. If there exists no element in the container that satisfies the +-- predicate then an exception is raised. +-- +-- @since 1.0.0 +exists :: (Foldable f, QuantifierIntro m) => f a -> (a -> m Bool) -> m Bool +exists xs = existsIntro (toList xs) +{-# INLINE exists #-} + +runExceptionalQuantifier :: + Members '[Error RuntimeException, NonDet] effs => + Lang ctx (Quantifier ': effs) Bool -> + Lang ctx effs Bool +runExceptionalQuantifier = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (runQuantifier . k) + Right bottom -> absurd (coerce bottom) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loom' + Right (Forall xs p) -> do + b <- oneOf xs >>= runLoom loom' . p + unless b (throwE (QuantifierException ForallViolated)) + return b + Right (Exists [] _) -> throwE (QuantifierException ExistsViolated) + Right (Exists dom p) -> do + let m' = flip foldMapA dom \x -> do + b <- runLoom loom' (p x) `catchE` (\(_ :: RuntimeException) -> empty) + bool empty (pure b) b + msplit m' >>= \case + Just _ -> m' + Nothing -> throwE (QuantifierException ExistsViolated) + where + loom' = loom ~>~ hoist runQuantifier +{-# INLINE runExceptionalQuantifier #-} + +runQuantifier :: Members '[NonDet] effs => Lang ctx (Quantifier ': effs) Bool -> Lang ctx effs Bool +runQuantifier = \case + Pure x -> pure x + Op op k -> case decomposeOp op of + Left other -> Op other (runQuantifier . k) + Right bottom -> absurd (coerce bottom) + Scoped scoped loom -> case decomposeS scoped of + Left other -> Scoped other loom' + Right (Forall xs p) -> foldr (liftA2 (&&) . runLoom loom' . p) (pure True) xs + Right (Exists xs p) -> foldr (liftA2 (||) . runLoom loom' . p) (pure False) xs + where + loom' = loom ~>~ hoist runQuantifier +{-# INLINE runQuantifier #-} diff --git a/src/Language/Spectacle/Syntax/Quantifier/Internal.hs b/src/Language/Spectacle/Syntax/Quantifier/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Language/Spectacle/Syntax/Quantifier/Internal.hs @@ -0,0 +1,34 @@ +{-# LANGUAGE TypeFamilies #-} + +module Language.Spectacle.Syntax.Quantifier.Internal + ( Quantifier (Quantifier), + Effect (Forall, Exists), + QuantifierIntro (existsIntro, forallIntro), + ) +where + +import Data.Void (Void) + +import Language.Spectacle.Lang (Effect, EffectK, Lang, Member, ScopeK, scope) + +-- --------------------------------------------------------------------------------------------------------------------- + +newtype Quantifier :: EffectK where + Quantifier :: Void -> Quantifier a + +data instance Effect Quantifier :: ScopeK where + Forall :: [a] -> (a -> m Bool) -> Effect Quantifier m Bool + Exists :: [a] -> (a -> m Bool) -> Effect Quantifier m Bool + +class QuantifierIntro m where + existsIntro :: [a] -> (a -> m Bool) -> m Bool + + forallIntro :: [a] -> (a -> m Bool) -> m Bool + +-- | @since 1.0.0 +instance Member Quantifier effs => QuantifierIntro (Lang ctxt effs) where + forallIntro xs p = scope (Forall xs p) + {-# INLINE forallIntro #-} + + existsIntro xs p = scope (Exists xs p) + {-# INLINE existsIntro #-} diff --git a/test/integration/Main.hs b/test/integration/Main.hs new file mode 100644 --- /dev/null +++ b/test/integration/Main.hs @@ -0,0 +1,50 @@ +import Control.Monad.IO.Class (liftIO) +import Data.Hashable (Hashable) + +import Hedgehog (Property, annotateShow, failure, property, success, withTests) +import Test.Tasty (defaultMain, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +import Data.Type.Rec (HasDict) +import Language.Spectacle.Model (modelcheck) +import Language.Spectacle.Specification (Specification) + +import qualified Specifications.BitClock as BitClock +import qualified Specifications.Diehard as Diehard +import qualified Specifications.SimpleClock as SimpleClock +import qualified Specifications.Status as Status + +-- --------------------------------------------------------------------------------------------------------------------- + +main :: IO () +main = + defaultMain $ + testGroup + "integration tests" + [ testProperty "Specifications.BitClock" (testCheckVerify BitClock.bitClockSpec) + , testProperty "Specifications.Diehard" (testCheckRefute Diehard.diehardSpec) + , testProperty "Specifications.SimpleClock" (testCheckVerify SimpleClock.clockSpec) + , testProperty "Specifications.Status" (testCheckVerify Status.statusSpec) + ] + +testCheckVerify :: + (HasDict Hashable ctx, HasDict Show ctx) => + Specification ctx acts form -> + Property +testCheckVerify spec = + withTests 1 $ property do + checkResult <- liftIO (modelcheck spec) + case checkResult of + Left err -> annotateShow err >> failure + Right {} -> success + +testCheckRefute :: + HasDict Hashable ctx => + Specification ctx acts form -> + Property +testCheckRefute spec = + withTests 1 $ property do + checkResult <- liftIO (modelcheck spec) + case checkResult of + Left {} -> success + Right {} -> failure diff --git a/test/integration/Specifications/BitClock.hs b/test/integration/Specifications/BitClock.hs new file mode 100644 --- /dev/null +++ b/test/integration/Specifications/BitClock.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE OverloadedLabels #-} + +module Specifications.BitClock where + +import Data.Word (Word8) + +import Language.Spectacle + ( Action, + ActionType (ActionWF), + Fairness (WeakFair), + Modality (Always), + Specification (Specification), + Temporal, + TemporalType (PropG), + interaction, + plain, + specInit, + specNext, + specProp, + (.=), + pattern ConF, + pattern NilF, + type (#), + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +check :: IO () +check = interaction bitClockSpec + +-- --------------------------------------------------------------------------------------------------------------------- + +type BitClockSpec = + Specification + '["clock" # Word8] + '["tick" # 'WeakFair] + '["times" # 'Always] + +bitClockNext :: Action '["clock" # Word8] Bool +bitClockNext = do + clock <- plain #clock + if clock == 0 + then #clock .= pure 1 + else #clock .= pure 0 + return True + +bitClockTimes :: Temporal '["clock" # Word8] Bool +bitClockTimes = do + clock <- plain #clock + pure (clock == 0 || clock == 1) + +bitClockSpec :: BitClockSpec +bitClockSpec = + Specification + { specInit = ConF #clock (pure 0) NilF + , specNext = ConF #tick (ActionWF bitClockNext) NilF + , specProp = ConF #times (PropG bitClockTimes) NilF + } diff --git a/test/integration/Specifications/Diehard.hs b/test/integration/Specifications/Diehard.hs new file mode 100644 --- /dev/null +++ b/test/integration/Specifications/Diehard.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE OverloadedLabels #-} + +module Specifications.Diehard where + +import Language.Spectacle + ( Action, + ActionType (ActionUF), + Fairness (Unfair), + Modality (Always), + Specification (Specification), + Temporal, + TemporalType (PropG), + interaction, + plain, + prime, + specInit, + specNext, + specProp, + (.=), + pattern ConF, + pattern NilF, + type (#), + ) + +-- ------------------------------------------------------------------------------------------------- + +interactDiehardSpec :: IO () +interactDiehardSpec = interaction diehardSpec + +-- ------------------------------------------------------------------------------------------------- + +type DiehardSpec = + Specification + DiehardVars + '[ "emptySmall" # 'Unfair + , "emptyBig" # 'Unfair + , "fillSmall" # 'Unfair + , "fillBig" # 'Unfair + , "smallToBig" # 'Unfair + , "bigToSmall" # 'Unfair + ] + '[ "isSolved" # 'Always + ] + +type DiehardVars = + '[ "smallJug" # Int + , "bigJug" # Int + ] + +emptySmall :: Action DiehardVars Bool +emptySmall = do + #smallJug .= pure 0 + return True + +emptyBig :: Action DiehardVars Bool +emptyBig = do + #bigJug .= pure 0 + pure True + +fillSmall :: Action DiehardVars Bool +fillSmall = do + #smallJug .= pure 3 + return True + +fillBig :: Action DiehardVars Bool +fillBig = do + #bigJug .= pure 5 + pure True + +bigToSmall :: Action DiehardVars Bool +bigToSmall = do + bigJug <- plain #bigJug + smallJug <- plain #smallJug + + #smallJug .= pure (min (bigJug + smallJug) 3) + #bigJug .= do + smallJug' <- prime #smallJug + pure (bigJug - (smallJug' - smallJug)) + + pure True + +smallToBig :: Action DiehardVars Bool +smallToBig = do + bigJug <- plain #bigJug + smallJug <- plain #smallJug + + #bigJug .= pure (min (bigJug + smallJug) 5) + #smallJug .= do + bigJug' <- prime #bigJug + pure (smallJug - (bigJug' - bigJug)) + + pure True + +isSolved :: Temporal DiehardVars Bool +isSolved = do + bigJug <- plain #bigJug + pure (bigJug /= 4) + +diehardSpec :: DiehardSpec +diehardSpec = + Specification + { specInit = + ConF #smallJug (pure 0) + . ConF #bigJug (pure 0) + $ NilF + , specNext = + ConF #emptySmall (ActionUF emptySmall) + . ConF #emptyBig (ActionUF emptyBig) + . ConF #fillSmall (ActionUF fillSmall) + . ConF #fillBig (ActionUF fillBig) + . ConF #smallToBig (ActionUF smallToBig) + . ConF #bigToSmall (ActionUF bigToSmall) + $ NilF + , specProp = + ConF #isSolved (PropG isSolved) NilF + } diff --git a/test/integration/Specifications/SimpleClock.hs b/test/integration/Specifications/SimpleClock.hs new file mode 100644 --- /dev/null +++ b/test/integration/Specifications/SimpleClock.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE OverloadedLabels #-} + +module Specifications.SimpleClock where + +import Language.Spectacle + ( Action, + ActionType (ActionWF), + Fairness (WeakFair), + Modality (Always, Infinitely), + Specification (Specification), + Temporal, + TemporalType (PropG, PropGF), + interaction, + modelcheck, + plain, + prime, + specInit, + specNext, + specProp, + (.=), + pattern ConF, + pattern NilF, + type (#), + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +interactClockSpec :: IO () +interactClockSpec = interaction clockSpec + +clockSpecCheck :: IO () +clockSpecCheck = do + modelcheck clockSpec >>= \case + Left err -> print err + Right xs -> print xs + +-- --------------------------------------------------------------------------------------------------------------------- + +type ClockSpec = + Specification + '["hour" # Int] + '["next" # 'WeakFair] + '["ticks" # 'Infinitely, "times" # 'Always] + +clockNext :: Action '["hour" # Int] Bool +clockNext = do + hour <- plain #hour + if hour == 12 + then #hour .= pure 1 + else #hour .= pure (1 + hour) + pure True + +clockTicks :: Temporal '["hour" # Int] Bool +clockTicks = do + hour <- plain #hour + hour' <- prime #hour + pure (1 + hour == hour') + +clockTimes :: Temporal '["hour" # Int] Bool +clockTimes = do + hour <- plain #hour + pure (1 <= hour && hour <= 12) + +clockSpec :: ClockSpec +clockSpec = + Specification + { specInit = ConF #hour (pure 1) NilF + , specNext = ConF #next (ActionWF clockNext) NilF + , specProp = + ConF #ticks (PropGF clockTicks) + . ConF #times (PropG clockTimes) + $ NilF + } diff --git a/test/integration/Specifications/Status.hs b/test/integration/Specifications/Status.hs new file mode 100644 --- /dev/null +++ b/test/integration/Specifications/Status.hs @@ -0,0 +1,96 @@ +{-# LANGUAGE OverloadedLabels #-} + +-- | +-- +-- @since 0.1.0.0 +module Specifications.Status where + +import Data.Hashable (Hashable) +import GHC.Generics (Generic) + +import Language.Spectacle + ( Action, + ActionType (ActionSF, ActionUF, ActionWF), + Fairness (StrongFair, Unfair, WeakFair), + Modality (Eventually), + Specification (Specification), + Temporal, + TemporalType (PropF), + interaction, + modelcheck, + plain, + specInit, + specNext, + specProp, + (.=), + pattern ConF, + pattern NilF, + type (#), + ) + +-- --------------------------------------------------------------------------------------------------------------------- + +statusSpecInteract :: IO () +statusSpecInteract = do + interaction statusSpec + +statusSpecCheck :: IO () +statusSpecCheck = do + modelcheck statusSpec >>= \case + Left err -> print err + Right xs -> print xs + +-- --------------------------------------------------------------------------------------------------------------------- + +type StatusSpec = + Specification + '[ "status" # Status + ] + '[ "statusRetry" # 'StrongFair + , "statusDone" # 'WeakFair + , "statusFail" # 'Unfair + ] + '[ "isStatusDone" # 'Eventually + ] + +data Status = Start | Done | Fail + deriving stock (Eq, Enum, Generic, Show) + +instance Hashable Status + +statusRetry :: Action '["status" # Status] Bool +statusRetry = do + status <- plain #status + #status .= pure Start + pure (status == Fail) + +statusDone :: Action '["status" # Status] Bool +statusDone = do + status <- plain #status + #status .= pure Done + pure (status == Start) + +statusFail :: Action '["status" # Status] Bool +statusFail = do + status <- plain #status + #status .= pure Fail + pure (status == Start) + +isStatusDone :: Temporal '["status" # Status] Bool +isStatusDone = do + status <- plain #status + pure (status == Done) + +statusSpec :: StatusSpec +statusSpec = + Specification + { specInit = + ConF #status (pure Start) NilF + , specNext = + ConF #statusRetry (ActionSF statusRetry) + . ConF #statusDone (ActionWF statusDone) + . ConF #statusFail (ActionUF statusFail) + $ NilF + , specProp = + ConF #isStatusDone (PropF isStatusDone) NilF + } diff --git a/test/unit-tests/Main.hs b/test/unit-tests/Main.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Main.hs @@ -0,0 +1,19 @@ +module Main (main) where + +import Test.Tasty (TestTree, defaultMain, testGroup) + +import qualified Test.Control.Comonad.Tape +import qualified Test.Language.Spectacle.Interaction + +-- --------------------------------------------------------------------------------------------------------------------- + +main :: IO () +main = defaultMain unitTestTree + +unitTestTree :: TestTree +unitTestTree = + testGroup + "Unit Tests" + [ Test.Control.Comonad.Tape.tests + , Test.Language.Spectacle.Interaction.tests + ] diff --git a/test/unit-tests/Test/Control/Comonad/Tape.hs b/test/unit-tests/Test/Control/Comonad/Tape.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Control/Comonad/Tape.hs @@ -0,0 +1,98 @@ +-- | +-- +-- @since 0.1.0.0 +module Test.Control.Comonad.Tape + ( tests, + ) +where + +import Control.Comonad (duplicate, extract) +import Data.Sequence (Seq) + +import Hedgehog (MonadGen, Property, diff, discard, footnote, forAll, property, withTests) +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +import Control.Comonad.Tape (Tape, shiftl, shiftr, toSeq, viewAt, viewl, viewr) + +-- --------------------------------------------------------------------------------------------------------------------- + +tests :: TestTree +tests = + testGroup + "Tape" + [ testProperty "Tape.viewl == Tape.viewAt 0" viewlIsAt0 + , testProperty "Tape.viewr == Tape.viewAt . length" viewrIsAtN + , testProperty "Tape/Seq isomorphism" isoTapeSeq + , testProperty "extract . duplicate == id" idDuplicateExtract + , testProperty "move n . viewAt i == viewAt (n + i)" idViewMove + , testProperty "shiftl . mover . shiftl == shiftl" invShiftl + , testProperty "mover . shiftl . mover == shiftr" invShiftr + ] + +linearIntSeq :: MonadGen m => Int -> Int -> m (Seq Int) +linearIntSeq lb ub = Gen.seq (Range.linear lb ub) (Gen.int Range.linearBounded) + +viewlIsAt0 :: Property +viewlIsAt0 = withTests 10 $ property do + xs <- forAll (linearIntSeq 0 5) + diff (viewl xs) (==) (viewAt 0 xs) + +viewrIsAtN :: Property +viewrIsAtN = withTests 10 $ property do + xs <- forAll (linearIntSeq 0 5) + diff (viewr xs) (==) (viewAt (length xs - 1) xs) + +isoTapeSeq :: Property +isoTapeSeq = withTests 10 $ property do + xs <- forAll (linearIntSeq 0 5) + i <- forAll (Gen.int $ Range.constant 0 (length xs)) + + if null xs + then diff (toSeq <$> viewAt i xs) (==) Nothing + else diff (toSeq <$> viewAt i xs) (==) (Just xs) + +idDuplicateExtract :: Property +idDuplicateExtract = withTests 10 $ property do + xs <- forAll (linearIntSeq 0 5) + i <- forAll (Gen.int $ Range.constant 0 (length xs - 1)) + + case viewAt i xs of + Nothing -> discard + Just tape -> do + diff (extract (duplicate tape)) (==) tape + +-- Testing that viewing the tape at some @i@ and moving it @n@ is the same as viewing it at @i - n@. +idViewMove :: Property +idViewMove = property do + xs <- forAll (linearIntSeq 0 10) + + let ub = length xs - 1 + i <- forAll (Gen.int $ Range.constant 0 ub) + n <- forAll (Gen.int $ Range.constant 0 ub) + + footnote ("viewed at: " ++ show i) + footnote ("moved by: " ++ show n) + + diff (shiftl n <$> viewAt i xs) (==) (viewAt (i - n) xs) + diff (shiftr n <$> viewAt i xs) (==) (viewAt (i + n) xs) + +invShiftl :: Property +invShiftl = isInverse shiftl shiftr + +invShiftr :: Property +invShiftr = isInverse shiftr shiftl + +isInverse :: (forall a. Int -> Tape a -> Tape a) -> (forall a. Int -> Tape a -> Tape a) -> Property +isInverse to from = property do + xs <- forAll (linearIntSeq 0 10) + let ub = length xs - 1 + i <- forAll (Gen.int $ Range.constant 0 ub) + + case viewAt i xs of + Nothing -> discard + Just tape -> do + n <- forAll (Gen.int $ Range.constant 0 ub) + diff (to n . from n . to n $ tape) (==) (to n tape) diff --git a/test/unit-tests/Test/Gen.hs b/test/unit-tests/Test/Gen.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Gen.hs @@ -0,0 +1,100 @@ +module Test.Gen + ( -- * Tree Generators + tree, + cataTree, + subtrees, + leaves, + + -- * Fingerprint + fingerprint, + + -- * World + emptyWorld, + + -- * Pos + pos, + + -- * Re-exports + Fingerprint, + Pos, + Tree, + World, + module Hedgehog.Gen, + ) +where + +import Control.Applicative (liftA2) +import Control.Monad (replicateM) + +import Hedgehog (MonadGen) +import Hedgehog.Gen (choice, int, resize, sized) +import Hedgehog.Internal.Gen (golden) +import Hedgehog.Range (Size, constantBounded, linear, linearBounded) + +import Data.Fingerprint (Fingerprint (Fingerprint)) +import Data.Functor.Tree (Tree (Node), pattern Leaf) +import Data.World (World (World)) +import Language.Spectacle.Interaction.Pos (Pos, pattern Pos) + +import qualified Test.Gen.Rec as Gen.Rec + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | @'tree' x@ recursive generates a tree of @x@ using both 'subtrees' and 'leaves'. +tree :: MonadGen m => m a -> m (Tree a) +tree gen = sized (liftA2 Node gen . fmap pure . generator) + where + generator !size + | size <= 1 = Leaf <$> gen + | otherwise = do + len <- int (linear 0 $ fromIntegral size) + liftA2 Node gen $ choice [subtrees len gen, leaves len gen] + +-- | @'cataTree' x k@ is a recursive 'Tree' generator for an element generator @x@, subtree generator @k@. The subtree +-- generator passes a suggested a subtree length (scaled by the size parameter) along with the generator for @x@. +-- +-- 'cataTree' replaces 'tree' in instances where a custom generator (such as 'subtrees' or 'leaves') is needed. +cataTree :: MonadGen m => m a -> (Int -> m a -> m [Tree a]) -> m (Tree a) +cataTree gen k = sized (liftA2 Node gen . fmap pure . generator) + where + generator !size + | size <= 1 = Leaf <$> gen + | otherwise = do + len <- int (linear 0 $ fromIntegral size) + liftA2 Node gen $ k len gen + +-- | @'subtrees' n x@ generates @n@ subtrees of @x@ dividing the size parameter among them evenly. +subtrees :: MonadGen m => Int -> m a -> m [Tree a] +subtrees len gen = + sized \size -> + if 1 < size + then resize (smallN len size) do + replicateM len (cataTree gen subtrees) + else pure [] + +-- | @'leaves' n x@ is constant to n-many leaves of @x@. +leaves :: MonadGen m => Int -> m a -> m [Tree a] +leaves len gen = replicateM len (fmap Leaf gen) + +-- --------------------------------------------------------------------------------------------------------------------- + +fingerprint :: MonadGen m => m Fingerprint +fingerprint = Fingerprint <$> int constantBounded + +-- --------------------------------------------------------------------------------------------------------------------- + +emptyWorld :: MonadGen m => m (World '[]) +emptyWorld = liftA2 World fingerprint Gen.Rec.empty + +-- --------------------------------------------------------------------------------------------------------------------- + +pos :: MonadGen m => m Pos +pos = liftA2 Pos (int linearBounded) (int linearBounded) + +-- --------------------------------------------------------------------------------------------------------------------- + +-- | Like 'small', but scales the size parameter by a factor of @n@. +smallN :: Int -> Size -> Size +smallN n size + | 1 < n = golden (size `quot` fromIntegral n) + | otherwise = 0 diff --git a/test/unit-tests/Test/Gen/Rec.hs b/test/unit-tests/Test/Gen/Rec.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Gen/Rec.hs @@ -0,0 +1,22 @@ +module Test.Gen.Rec + ( -- * Record Generators + empty, + singleton, + + -- * Re-exports + Rec, + ) +where + +import Hedgehog (MonadGen) + +import Data.Type.Rec (Name, Rec, type (#)) +import qualified Data.Type.Rec as Rec + +-- --------------------------------------------------------------------------------------------------------------------- + +empty :: MonadGen m => m (Rec '[]) +empty = pure Rec.Nil + +singleton :: MonadGen m => Name c -> m a -> m (Rec '[c # a]) +singleton n = fmap \x -> Rec.Con n x Rec.Nil diff --git a/test/unit-tests/Test/Language/Spectacle/Interaction.hs b/test/unit-tests/Test/Language/Spectacle/Interaction.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Language/Spectacle/Interaction.hs @@ -0,0 +1,19 @@ +module Test.Language.Spectacle.Interaction + ( tests, + ) +where + +import Test.Tasty (TestTree, testGroup) + +import qualified Test.Language.Spectacle.Interaction.Paths +import qualified Test.Language.Spectacle.Interaction.Pos + +-- --------------------------------------------------------------------------------------------------------------------- + +tests :: TestTree +tests = + testGroup + "Interaction" + [ Test.Language.Spectacle.Interaction.Paths.tests + , Test.Language.Spectacle.Interaction.Pos.tests + ] diff --git a/test/unit-tests/Test/Language/Spectacle/Interaction/Paths.hs b/test/unit-tests/Test/Language/Spectacle/Interaction/Paths.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Language/Spectacle/Interaction/Paths.hs @@ -0,0 +1,39 @@ +module Test.Language.Spectacle.Interaction.Paths + ( tests, + ) +where + +import Data.Foldable (find, for_) +import Lens.Micro.Extras (view) + +import Hedgehog (Property, evalMaybe, forAll, property) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +import Data.World (World (World)) +import Language.Spectacle.Interaction.Paths as Paths (toPointSet) +import Language.Spectacle.Interaction.Point (label) + +import qualified Test.Gen as Gen + +-- --------------------------------------------------------------------------------------------------------------------- + +tests :: TestTree +tests = + testGroup + "Paths" + [ testProperty "Paths.toPointSet is nondestructive" flattenNondestruct + ] + +-- | Paths.flatten does not destroy or add information. +flattenNondestruct :: Property +flattenNondestruct = property do + -- tree size is adjusted by hedgehog's size parameter. + tree <- forAll (Gen.tree Gen.emptyWorld) + let set = Paths.toPointSet tree + + for_ tree \(World hash _) -> + evalMaybe $ find (look hash) set + where + -- ensure membership for each element of the original tree and the flattened as 'Paths' by it's hash. + look hash1 world = hash1 == view label world diff --git a/test/unit-tests/Test/Language/Spectacle/Interaction/Pos.hs b/test/unit-tests/Test/Language/Spectacle/Interaction/Pos.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Language/Spectacle/Interaction/Pos.hs @@ -0,0 +1,58 @@ +module Test.Language.Spectacle.Interaction.Pos + ( -- * Pos/Interval tests + tests, + ) +where + +import Control.Monad (when) +import Lens.Micro.Extras (view) + +import Hedgehog (Property, diff, forAll, property) +import Hedgehog.Range (linearBounded) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +import Language.Spectacle.Interaction.Pos (pcol, prow) + +import qualified Test.Gen as Gen +import qualified Test.Laws.Lens +import qualified Test.Laws.Ord + +-- --------------------------------------------------------------------------------------------------------------------- + +tests :: TestTree +tests = + testGroup + "Pos" + [ testsPos + , testsInterval + ] + +-- --------------------------------------------------------------------------------------------------------------------- + +testsPos :: TestTree +testsPos = + testGroup + "Pos.Pos" + [ testProperty "row ordering" propRowOrder + , Test.Laws.Ord.laws "pos" Gen.pos + , Test.Laws.Lens.laws pcol "pcol" Gen.pos (Gen.int linearBounded) + , Test.Laws.Lens.laws prow "prow" Gen.pos (Gen.int linearBounded) + ] + +-- | This property characterizes the order on 'Pos'. +propRowOrder :: Property +propRowOrder = property do + p <- forAll Gen.pos + q <- forAll Gen.pos + when (view prow p < view prow q) do + diff p (<) q + +-- --------------------------------------------------------------------------------------------------------------------- + +testsInterval :: TestTree +testsInterval = + testGroup + "Pos.Interval" + [ Test.Laws.Ord.laws "interval" Gen.pos + ] diff --git a/test/unit-tests/Test/Laws/Lens.hs b/test/unit-tests/Test/Laws/Lens.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Laws/Lens.hs @@ -0,0 +1,58 @@ +module Test.Laws.Lens + ( -- * Lens Laws + laws, + injective, + surjective, + idempotent, + ) +where + +import Lens.Micro (Lens', set) +import Lens.Micro.Extras (view) + +import Hedgehog (Gen, PropertyT, diff, forAll, property) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +-- --------------------------------------------------------------------------------------------------------------------- + +laws :: (Show a, Eq a, Show b, Eq b) => Lens' a b -> String -> Gen a -> Gen b -> TestTree +laws p desc gen1 gen0 = + testGroup + (if null desc then "lens laws" else desc ++ " - lens laws") + [ testProperty "1. injectivity" $ property (injective p gen1 gen0) + , testProperty "2. surjectivity" $ property (surjective p gen1) + , testProperty "3. idempotency" $ property (idempotent p gen1 gen0) + ] + +-- | Setters are injective. You get back what you put in: +-- +-- @ +-- 'view' p ('set' p x fx) == 'set' p x fx +-- @ +injective :: (Monad m, Show a, Eq b, Show b) => Lens' a b -> Gen a -> Gen b -> PropertyT m () +injective p gen1 gen0 = do + fx <- forAll gen1 + x <- forAll gen0 + diff (view p (set p x fx)) (==) x + +-- | Setters are surjective. Putting back what you got doesn't change anything: +-- +-- @ +-- 'set' p ('view' p fx) fx == fx +-- @ +surjective :: (Monad m, Eq a, Show a) => Lens' a b -> Gen a -> PropertyT m () +surjective p gen1 = do + fx <- forAll gen1 + diff (set p (view p fx) fx) (==) fx + +-- | Setters are idempotent. Setting twice is the same as setting once: +-- +-- @ +-- 'set' p x ('set' p x fx) == 'set' p x fx +-- @ +idempotent :: (Monad m, Eq a, Show a, Show b) => Lens' a b -> Gen a -> Gen b -> PropertyT m () +idempotent p gen1 gen0 = do + fx <- forAll gen1 + x <- forAll gen0 + diff (set p x (set p x fx)) (==) (set p x fx) diff --git a/test/unit-tests/Test/Laws/Ord.hs b/test/unit-tests/Test/Laws/Ord.hs new file mode 100644 --- /dev/null +++ b/test/unit-tests/Test/Laws/Ord.hs @@ -0,0 +1,51 @@ +-- | Laws for total orders. +-- +-- @since 0.1.0.0 +module Test.Laws.Ord + ( -- * Ord Laws + laws, + irreflexive, + antisymmetry, + ) +where + +import Hedgehog (Gen, PropertyT, assert, failure, footnote, forAll, property, success, withTests) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +-- --------------------------------------------------------------------------------------------------------------------- + +laws :: (Show a, Ord a) => String -> Gen a -> TestTree +laws desc gen = + testGroup + (if null desc then "ord laws" else desc ++ " - ord laws") + [ testProperty "1. antisymmetry" $ property (antisymmetry gen) + , testProperty "2. irreflexive" . withTests 1 $ property (irreflexive gen) + ] + +-- | Strict order is irreflexive +-- +-- @ +-- a < b <=> a /= b +-- @ +irreflexive :: (Monad m, Show a, Ord a) => Gen a -> PropertyT m () +irreflexive gen = do + a <- forAll gen + footnote (show a ++ " < " ++ show a) + if a < a + then failure + else success + +-- | Strict order is antisymmetric +-- +-- @ +-- a < b <=> not (b < a) +-- @ +antisymmetry :: (Monad m, Show a, Ord a) => Gen a -> PropertyT m () +antisymmetry gen = do + a <- forAll gen + b <- forAll gen + footnote (show a ++ " < " ++ show b) + if a < b + then assert (b >= a) + else assert (a >= b)