spectacle (empty) → 1.0.0

raw patch · 89 files changed

+6983/−0 lines, 89 filesdep +basedep +comonaddep +containers

Dependencies added: base, comonad, containers, hashable, hedgehog, logict, microlens, microlens-mtl, mtl, optparse-applicative, prettyprinter, prettyprinter-ansi-terminal, spectacle, tasty, tasty-hedgehog, text, transformers

Files

• CHANGELOG.md +34/−0
• LICENSE +201/−0
• README.md +5/−0
• spectacle.cabal +189/−0
• src/Control/Applicative/Day.hs +44/−0
• src/Control/Applicative/Phases.hs +61/−0
• src/Control/Applicative/Queue.hs +53/−0
• src/Control/Comonad/Tape.hs +119/−0
• src/Control/Hyper.hs +31/−0
• src/Control/Mealy.hs +59/−0
• src/Control/Monad/Levels.hs +34/−0
• src/Control/Monad/Levels/Internal.hs +138/−0
• src/Control/Monad/Ref.hs +67/−0
• src/Control/Natural.hs +12/−0
• src/Data/Ascript.hs +41/−0
• src/Data/Bag.hs +75/−0
• src/Data/Fingerprint.hs +72/−0
• src/Data/Functor/Loom.hs +104/−0
• src/Data/Functor/Tree.hs +83/−0
• src/Data/Name.hs +51/−0
• src/Data/Node.hs +48/−0
• src/Data/Type/List.hs +18/−0
• src/Data/Type/Rec.hs +223/−0
• src/Data/World.hs +86/−0
• src/Language/Spectacle.hs +89/−0
• src/Language/Spectacle/AST.hs +15/−0
• src/Language/Spectacle/AST/Action.hs +211/−0
• src/Language/Spectacle/AST/Temporal.hs +36/−0
• src/Language/Spectacle/Exception/RuntimeException.hs +62/−0
• src/Language/Spectacle/Fairness.hs +41/−0
• src/Language/Spectacle/Interaction.hs +59/−0
• src/Language/Spectacle/Interaction/CLI.hs +124/−0
• src/Language/Spectacle/Interaction/Diagram.hs +361/−0
• src/Language/Spectacle/Interaction/Doc.hs +163/−0
• src/Language/Spectacle/Interaction/Options.hs +158/−0
• src/Language/Spectacle/Interaction/Paths.hs +82/−0
• src/Language/Spectacle/Interaction/Point.hs +103/−0
• src/Language/Spectacle/Interaction/Pos.hs +115/−0
• src/Language/Spectacle/Lang.hs +83/−0
• src/Language/Spectacle/Lang/Internal.hs +105/−0
• src/Language/Spectacle/Lang/Member.hs +96/−0
• src/Language/Spectacle/Lang/Op.hs +37/−0
• src/Language/Spectacle/Lang/Scoped.hs +140/−0
• src/Language/Spectacle/Model.hs +314/−0
• src/Language/Spectacle/Model/ModelAction.hs +51/−0
• src/Language/Spectacle/Model/ModelEnv.hs +74/−0
• src/Language/Spectacle/Model/ModelError.hs +96/−0
• src/Language/Spectacle/Model/ModelNode.hs +81/−0
• src/Language/Spectacle/Model/ModelState.hs +57/−0
• src/Language/Spectacle/Model/ModelTemporal.hs +34/−0
• src/Language/Spectacle/Model/Monad.hs +75/−0
• src/Language/Spectacle/RTS/Registers.hs +118/−0
• src/Language/Spectacle/Specification.hs +96/−0
• src/Language/Spectacle/Specification/Action.hs +43/−0
• src/Language/Spectacle/Specification/Prop.hs +65/−0
• src/Language/Spectacle/Specification/Variable.hs +73/−0
• src/Language/Spectacle/Syntax.hs +64/−0
• src/Language/Spectacle/Syntax/Closure.hs +125/−0
• src/Language/Spectacle/Syntax/Closure/Internal.hs +27/−0
• src/Language/Spectacle/Syntax/Enabled.hs +40/−0
• src/Language/Spectacle/Syntax/Enabled/Internal.hs +19/−0
• src/Language/Spectacle/Syntax/Env.hs +50/−0
• src/Language/Spectacle/Syntax/Env/Internal.hs +21/−0
• src/Language/Spectacle/Syntax/Error.hs +55/−0
• src/Language/Spectacle/Syntax/Error/Internal.hs +17/−0
• src/Language/Spectacle/Syntax/Logic.hs +93/−0
• src/Language/Spectacle/Syntax/Logic/Internal.hs +23/−0
• src/Language/Spectacle/Syntax/NonDet.hs +80/−0
• src/Language/Spectacle/Syntax/NonDet/Internal.hs +19/−0
• src/Language/Spectacle/Syntax/Plain.hs +45/−0
• src/Language/Spectacle/Syntax/Plain/Internal.hs +24/−0
• src/Language/Spectacle/Syntax/Prime.hs +167/−0
• src/Language/Spectacle/Syntax/Prime/Internal.hs +20/−0
• src/Language/Spectacle/Syntax/Quantifier.hs +98/−0
• src/Language/Spectacle/Syntax/Quantifier/Internal.hs +34/−0
• test/integration/Main.hs +50/−0
• test/integration/Specifications/BitClock.hs +58/−0
• test/integration/Specifications/Diehard.hs +116/−0
• test/integration/Specifications/SimpleClock.hs +73/−0
• test/integration/Specifications/Status.hs +96/−0
• test/unit-tests/Main.hs +19/−0
• test/unit-tests/Test/Control/Comonad/Tape.hs +98/−0
• test/unit-tests/Test/Gen.hs +100/−0
• test/unit-tests/Test/Gen/Rec.hs +22/−0
• test/unit-tests/Test/Language/Spectacle/Interaction.hs +19/−0
• test/unit-tests/Test/Language/Spectacle/Interaction/Paths.hs +39/−0
• test/unit-tests/Test/Language/Spectacle/Interaction/Pos.hs +58/−0
• test/unit-tests/Test/Laws/Lens.hs +58/−0
• test/unit-tests/Test/Laws/Ord.hs +51/−0

@@ -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 {} = ... +  ```

@@ -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.

@@ -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`.

@@ -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

@@ -0,0 +1,44 @@+{-# LANGUAGE TupleSections #-}++-- | Cayley applicative transformer.+--+-- === Reference+--+-- 1. <https://doisinkidney.com/posts/2020-11-23-applicative-queue.html>+--+-- 2. "Notions of Computations as Monoids" <https://arxiv.org/abs/1406.4823>+--+-- @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 #-}

@@ -0,0 +1,61 @@+-- | 'Phases' applicative functor transformer.+--+-- === Reference+--+-- 1. <https://doisinkidney.com/posts/2020-11-23-applicative-queue.html>+--+-- 2. <https://github.com/rampion/tree-traversals>+--+-- @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 #-}

@@ -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)

@@ -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)

@@ -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 #-}

@@ -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 (<*>) #-}

@@ -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)

@@ -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 #-}

@@ -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 #-}

@@ -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

@@ -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

@@ -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 #-}

@@ -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)

@@ -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 #-}

@@ -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 (<>)

@@ -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 #-}

@@ -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 #-}

@@ -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)

@@ -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)

@@ -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

@@ -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,+    (.=),+    (/\),+    (<=>),+    (==>),+    (\/),+  )++-- ---------------------------------------------------------------------------------------------------------------------

@@ -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)++-- ---------------------------------------------------------------------------------------------------------------------

@@ -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

@@ -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

@@ -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)

@@ -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)

@@ -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

@@ -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 #-}

@@ -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 #-}

@@ -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 '╰'

@@ -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"+        )

@@ -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)

@@ -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 #-}

@@ -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 #-}

@@ -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)

@@ -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 #-}

@@ -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 #-}

@@ -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 #-}

@@ -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

@@ -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

@@ -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]

@@ -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, ..}

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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)

@@ -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 _) = "<<thunk>>"+  show (Evaluated x) = show x+  show Unchanged = "<<unchanged>>"

@@ -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

@@ -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

@@ -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"

@@ -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)

@@ -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 (<=>) #-}

@@ -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

@@ -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 ()

@@ -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 #-}

@@ -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

@@ -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')

@@ -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 ()

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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))

@@ -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))

@@ -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)

@@ -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

@@ -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

@@ -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

@@ -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 #-}

@@ -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 #-}

@@ -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

@@ -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+    }

@@ -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+    }

@@ -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+    }

@@ -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+    }

@@ -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+    ]

@@ -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)

@@ -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

@@ -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

@@ -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+    ]

@@ -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

@@ -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+    ]

@@ -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)

@@ -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)