packages feed

nom (empty) → 0.1.0.0

raw patch · 46 files changed

+6376/−0 lines, 46 filesdep +QuickCheckdep +TypeComposedep +Uniquebuild-type:Customsetup-changed

Dependencies added: QuickCheck, TypeCompose, Unique, algebra, base, base-compat, containers, data-default, doctest, extra, finite-typelits, flow, hspec, nom, syb, template-haskell

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Murdoch J. Gabbay (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Author name here nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,33 @@+{-# LANGUAGE CPP #-}+{-# OPTIONS_GHC -Wall #-}+module Main (main) where++#ifndef MIN_VERSION_cabal_doctest+#define MIN_VERSION_cabal_doctest(x,y,z) 0+#endif++#if MIN_VERSION_cabal_doctest(1,0,0)++import Distribution.Extra.Doctest ( defaultMainWithDoctests )+main :: IO ()+main = defaultMainWithDoctests "nom-doctest"++#else++#ifdef MIN_VERSION_Cabal+-- If the macro is defined, we have new cabal-install,+-- but for some reason we don't have cabal-doctest in package-db+--+-- Probably we are running cabal sdist, when otherwise using new-build+-- workflow+#warning You are configuring this package without cabal-doctest installed. \+         The doctests test-suite will not work as a result. \+         To fix this, install cabal-doctest before configuring.+#endif++import Distribution.Simple++main :: IO ()+main = defaultMain++#endif
+ doctest/DocTest.hs view
@@ -0,0 +1,14 @@+module Main where++import Build_doctests            (flags, pkgs, module_sources)+import Data.Foldable             (traverse_)+import System.Environment.Compat (unsetEnv)+import Test.DocTest              (doctest)++main :: IO ()+main = do+    traverse_ putStrLn args+    unsetEnv "GHC_ENVIRONMENT"+    doctest args+  where+    args = flags ++ pkgs ++ module_sources
+ nom.cabal view
@@ -0,0 +1,118 @@+cabal-version:  2.0+name:           nom+version:        0.1.0.0+description:    Nominal-flavoured implementation of data in a context of local names, following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).+                __The recommended landing page is "Language.Nominal", so please go there first.__ See also: a tutorial in "Language.Nominal.Examples.Tutorial"; a short development of untyped lambda-calculus in "Language.Nominal.Examples.UntypedLambda"; an example development of System F in "Language.Nominal.Examples.SystemF"; and an example development of an EUTxO-style blockchain in "Language.Nominal.Examples.IdealisedEUTxO".+homepage:       https://github.com/bellissimogiorno/nominal#readme+bug-reports:    https://github.com/bellissimogiorno/nominal/issues+author:         Murdoch J. Gabbay+maintainer:     murdoch.gabbay@gmail.com+copyright:      2020 Murdoch J. Gabbay+license:        BSD3+license-file:   LICENSE+build-type:     Custom+category:       Language, Compilers/Interpreters+synopsis:       Name-binding & alpha-equivalence+ +custom-setup+  setup-depends:+      base+    , Cabal+    , cabal-doctest >=1.0.6 && <1.1++source-repository head+  type: git+  location: https://github.com/bellissimogiorno/nominal++library+  exposed-modules:+      Language.Nominal.Utilities+      Language.Nominal.Name+      Language.Nominal.NameSet+      Language.Nominal.SMonad+      Language.Nominal.Nom+      Language.Nominal.Binder+      Language.Nominal.Abs+      Language.Nominal.Sub+      Language.Nominal.Unify+      Language.Nominal.Unique+      Language.Nominal.Equivar+      Language.Nominal.Examples.SystemF+      Language.Nominal.Examples.IdealisedEUTxO+      Language.Nominal.Examples.UntypedLambda+      Language.Nominal.Examples.Assembly1+      Language.Nominal.Examples.Assembly2+      Language.Nominal.Examples.Style+      Language.Nominal.Examples.Tutorial+      Language.Nominal+      Language.Nominal.Properties.SpecUtilities+      Language.Nominal.Properties.NameSpec+      Language.Nominal.Properties.NameSetSpec+      Language.Nominal.Properties.NomSpec+      Language.Nominal.Properties.AbsSpec+      Language.Nominal.Properties.SubSpec+      Language.Nominal.Properties.UnifySpec+      Language.Nominal.Properties.UtilitiesSpec+      Language.Nominal.Properties.EquivarSpec+      Language.Nominal.Properties.Examples.IdealisedEUTxOSpec+      Language.Nominal.Properties.Examples.SystemFSpec+      Language.Nominal.Properties.AllTests+  hs-source-dirs:+      src+  build-depends:+    QuickCheck                        >= 2.11.3 && < 2.13.3,+    containers                        >= 0.5.11 && < 0.6.3,+    Unique                            >= 0.4.7 && < 0.5,+    extra                             >= 1.6.9 && < 1.7,+    algebra                           >= 4.3.1 && < 4.4,+    data-default                      >= 0.7.1 && < 0.8,+    finite-typelits                   >= 0.1.4 && < 0.2,+    flow                              >= 1.0.20 && < 1.1,+    syb                               >= 0.7 && < 0.8,+    base                              >= 4.7 && <5,+    TypeCompose                       >= 0.9.14 && < 0.10+  default-language: Haskell2010+  ghc-options: -Wall +               -- -Werror++test-suite nom-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Language.Nominal.NameSpec+    , Language.Nominal.NameSetSpec+    , Language.Nominal.NomSpec+    , Language.Nominal.AbsSpec+    , Language.Nominal.SubSpec+    , Language.Nominal.UnifySpec+    , Language.Nominal.UtilitiesSpec+    , Language.Nominal.EquivarSpec+    , Language.Nominal.Examples.SystemFSpec+    , Language.Nominal.Examples.IdealisedEUTxOSpec+  hs-source-dirs:+      test+  ghc-options: -Wall +               -- -Werror+  build-depends:+      base >=4.7 && <5+    , data-default+    , hspec+    , nom+    , QuickCheck+  build-tool-depends:+      hspec-discover:hspec-discover+  default-language: Haskell2010++test-suite nom-doctest+  type:             exitcode-stdio-1.0+  main-is:          DocTest.hs+  hs-source-dirs:+      doctest+  build-depends:+      base+    , base-compat       >=0.10.5 && <0.12+    , doctest           >=0.15   && <0.17+    , nom+    , template-haskell+  ghc-options:      -Wall -threaded+  default-language: Haskell2010
+ src/Language/Nominal.hs view
@@ -0,0 +1,102 @@+{-|+Module      : Nominal +Description : Implementation of nominal techniques as a Haskell package+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Nominal-flavoured implementation of data in a context of local names, designed following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).++-}++{-# LANGUAGE CPP #-}++module Language.Nominal+     ( +-- * Introduction+-- $blurb++-- * Quick links+-- $quicklinks++-- * Type(class) overview +-- $quickref++       module Language.Nominal.Name+     , module Language.Nominal.NameSet+     , module Language.Nominal.Sub+     , module Language.Nominal.Nom+     , module Language.Nominal.Binder+     , module Language.Nominal.Abs+     , module Language.Nominal.Equivar+     , module Language.Nominal.Unify+     ) +    where++import Language.Nominal.Name+import Language.Nominal.NameSet+import Language.Nominal.Sub+import Language.Nominal.Nom +import Language.Nominal.Binder+import Language.Nominal.Abs +import Language.Nominal.Equivar+import Language.Nominal.Unify++#include "Nominal/Blurb.txt"++{- $quicklinks++== Worked examples ++* "Language.Nominal.Examples.Tutorial": We explore some basic concepts. +* "Language.Nominal.Examples.UntypedLambda": Untyped lambda-calculus syntax and reductions (short example). +* "Language.Nominal.Examples.Assembly1": A simple assembly language, with binding (short example). +* "Language.Nominal.Examples.Assembly2": A simple assembly language, with binding and a swap-variable primitive (short example). +* "Language.Nominal.Examples.Style": Some basic comments on recommended programming style using this package. +* "Language.Nominal.Examples.SystemF": System F syntax and reductions (longer example). +* "Language.Nominal.Examples.IdealisedEUTxO": A EUTxO-style blockchain system, following the ideas in <https://arxiv.org/abs/2003.14271 mathematical idealisation of the Extended UTxO model> (longer example). ++== Links and references++* This package's <https://github.com/bellissimogiorno/nominal GitHub page>.+* The underlying mathematical model is described in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (<http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).+* The paper on <https://arxiv.org/abs/1009.2791v1 closed nominal rewriting> (<http://www.gabbay.org.uk/papers.html#clonre author's pdfs>) is pertinent to the design of "Language.Nominal.Unify".+* The paper on the <https://arxiv.org/abs/2003.14271 mathematical idealisation of the Extended UTxO model> is pertinent "Language.Nominal.Examples.IdealisedEUTxO".+* This draft book on <https://www.mimuw.edu.pl/~bojan/upload/main-10.pdf orbit-finite sets> may be of interest.+* The <https://hackage.haskell.org/package/bound Bound package>, from which the worked examples "Language.Nominal.Examples.Assembly1" and "Language.Nominal.Examples.Assembly2" are adapted. ++== Related work +* <https://hackage.haskell.org/package/bound bound: Making de Bruijn Succ less>+* <https://hackage.haskell.org/package/unbound unbound: Generic support for programming with names and binders>+* <https://hackage.haskell.org/package/unbound-generics unbound-generics: Support for programming with names and binders using GHC Generics>+* <https://hackage.haskell.org/package/nominal nominal: Binders and alpha-equivalence made easy> +* <https://www.mimuw.edu.pl/~szynwelski/nlambda/doc/ NLambda: computations over infinite structures using logical formulas and SMT solving>++/(Something I should put on this list?  Let me know.)/+-}++{- $quickref++Here is an overview of some core typeclasses:++* 'Language.Nominal.Name.KAtom' and 'Language.Nominal.Name.Atom': +Types of atomic freshly generatable identifiers. +* 'Language.Nominal.Name.KName' and 'Language.Nominal.Name.Name': +Types of labelled atoms.+* 'Language.Nominal.Name.KSwappable' and 'Language.Nominal.Name.Swappable':  +Typeclasses of types with a /swapping action/ by atoms and names.+* 'Language.Nominal.Name.KSupport' and 'Language.Nominal.Name.Support':  +Typeclasses of types with a structural notion of /the atoms in this object/.  In the mathematics, "support" coincides with "atoms for which the object may be asymmetric under swappings", but in this package support means something much stricter: that it is possible to traverse the data and pick out the atoms in its support.+/Note:/ "having empty support" does /not/ mean "having no atoms".  It means "symmetric under swapping atoms", which is not at all the same idea. +* 'Language.Nominal.Name.Nameless': types like @Int@, @String@, and @()@ that are guaranteed atoms-free. +* 'Language.Nominal.Nom.KNom' and 'Language.Nominal.Nom.Nom': An atoms-binding monad.+* 'Language.Nominal.Nom.Binder': A typeclass for functions acting on binding types.+* 'Language.Nominal.Abs.KAbs' and 'Language.Nominal.Abs.Abs': A name-abstracting functor.+* 'Language.Nominal.Name.KRestrict' and 'Language.Nominal.Name.Restrict': A typeclass of types with an inherent notion of atoms-binding.+* 'Language.Nominal.Unify.KUnifyPerm' and 'Language.Nominal.Unify.UnifyPerm': Typeclasses of types with a notion of unification by injective partial functions on atoms.+++-}+
+ src/Language/Nominal/Abs.hs view
@@ -0,0 +1,220 @@+{-|+Module      : Abs +Description : Nominal atoms-abstraction types +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Name-abstraction, nominal style.  This captures the "a." in "λa.ab".  ++Examples of practical usage are in "Language.Nominal.Examples.SystemF", e.g. the type and term datatypes 'Language.Nominal.Examples.SystemF.Typ' and 'Language.Nominal.Examples.SystemF.Trm'.+-}++{-# LANGUAGE DataKinds             +           , FlexibleContexts      +           , FlexibleInstances     +           , InstanceSigs          +           , MultiParamTypeClasses +           , PartialTypeSignatures   +           , ScopedTypeVariables   +           , StandaloneDeriving +           , TupleSections         +           , UndecidableInstances    -- needed for Num a => Nameless a+           , DerivingStrategies    +           , DerivingVia+           , GeneralizedNewtypeDeriving   +           , DeriveAnyClass        +           , DeriveGeneric         +           , DeriveFunctor          +           , DeriveFoldable          +           , DeriveTraversable     +           , PatternSynonyms+#-}  +++module Language.Nominal.Abs +   ( -- * Name-abstraction+     KAbs -- We don't expose the internals of KAbs.  Use @abst@. +   , Abs +-- * Abstractions (basic functions)+   , abst, abst', pattern (:@>), fuse, unfuse, absLabel, conc+-- * The bijection between @'Abs'@ and @'Nom'@+   , absToNom, nomToAbs+-- * Unpacking name-contexts and abstractions+   , absFresh, absFresh', absFuncOut+-- * Tests+   -- $tests +   )+   where++import Data.Data +import Data.Default+import GHC.Generics hiding (Prefix) -- avoid clash with Data.Data.Prefix++import Language.Nominal.Utilities ((.:))+import Language.Nominal.Name +import Language.Nominal.NameSet +import Language.Nominal.Nom+import Language.Nominal.Binder++-- * Name-abstraction++-- | A datatype for name-abstractions.+--+-- * @KAbs n a@ is a type for abstractions of @a@s by @n@-names, where we intend that @n = KName s t@ for some @s@-atoms (atoms of type @s@) and @t@-labels (labels of type @t@). +-- +-- * @Abs t a@ is a type for abstractions of @a@s by @t@-labelled @'Tom'@-atoms. +--+-- Under the hood an abstraction is just an element of @(n, n -> a)@, but we do not expose this.  What makes the type interesting is its constructor, @'abst' :: KName s t -> a -> KAbs (KName s t) a@, which is the only way to build an abstraction. +--+-- It's possible to implement @'KAbs'@ using @'Nom'@ — see @'absToNom'@ and @'nomToAbs'@ — but this requires a @'KSwappable'@ typeclass constraint on @a@, which we prefer to avoid so that e.g. @'KAbs'@ can be a @'Functor'@. +--+data KAbs n a = AbsWrapper { +   absName :: n,   -- ^ We only care about the name for its label.  For reasons having to do with the Haskell type system, it's convenient to wrap this label up in a "dummy name".  We do not export 'absName' outside this file. +   absApp :: n -> a  -- ^ A function that /concretes/ an abstraction at a particular name.   +-- Unsafe if the name is not fresh. +--+-- > (abst a x) `absApp` a == x+--+-- > abst a (x `absApp` a) == x -- provided a is suitably fresh. +--+-- > new' $ \a -> abst a (x `absApp` a) == x  +   }+   deriving ( Generic+            , Functor+            , Swappable -- ^ Spelling out the generic swapping action for clarity, where we write @KA@ for the (internal) constructor for @KAbs@: @kswp n1 n2 (KA n f) = KA (kswp n1 n2 n) (kswp n1 n2 f)@+            , Typeable+            )+-- | Support of a :@> x is the support of x minus a+deriving via BinderSupp (KAbs (KName s t) a) +   instance (KSupport s a, KSupport s t) => KSupport s (KAbs (KName s t) a) +++-- | Abstraction by @'Tom'@-names. +type Abs t a = KAbs (KName Tom t) a++-- * Creating abstractions++-- | Create an abstraction by providing a name and a datum in which that name can be swapped (straight out of the paper; <https://link.springer.com/article/10.1007/s001650200016 publisher> and <http://www.gabbay.org.uk/papers.html#newaas-jv author's> pdfs).+--+-- Instance of '@>', for the case of a nominal abstraction.+abst :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a+abst = (@>) ++-- | The abstraction pattern '(:@>)' is just an instance of '(:@@!)' for 'KAbs'.  Thus, +--+-- > n :@> x -> f n x+--+-- is synonymous with +--+-- > x' -> x' @@! f +--+-- Because '(:@>)' is a concrete instance of '(:@@!)', we can declare it @COMPLETE@.+pattern (:@>) :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a+pattern n :@> a <- n :@@! a where+    (:@>) = (@>) -- Explicitly bidirectional pattern synonym.  https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms#explicitly-bidirectional-pattern-synonyms+{-# COMPLETE (:@>) #-}   -- States that this match on an abstraction is complete.+infixr 0 :@> ++-- | A 'Name' is just a pair of a label and an 'Atom'.  This version of 'abst' that takes a label and an atom, instead of a name.+abst' :: (Typeable s, Swappable t, Swappable a) => t -> KAtom s -> a -> KAbs (KName s t) a+abst' = (@>) .: Name ++-- | Fuse abstractions, taking label of abstracted name from first argument.+-- Should satisfy:+--+-- > fuse (n @> x) (n @> y) = n @> (x, y)+--+fuse :: (KAbs (KName s t) a1, KAbs (KName s t) a2) -> KAbs (KName s t) (a1, a2)+fuse (AbsWrapper n1 f1, AbsWrapper _ f2) = AbsWrapper n1 $ \n -> (f1 n, f2 n)  ++-- | Split two abstractions.+-- Should satisfy:+--+-- > unfuse (n @> (x,y)) = (n @> x, n @> y)+--+unfuse :: KAbs (KName s t) (a, b) -> (KAbs (KName s t) a, KAbs (KName s t) b) +unfuse (AbsWrapper n f) = +   (AbsWrapper n (fst . f), AbsWrapper n (snd . f)) +++-- | Return the label of an abstraction.+--+-- /Note:/ For reasons having to do with the Haskell type system it's convenient to store this label in the underlying representation of the abstraction, using a "dummy name".  However, we do not export access to this name, we only export access to its label, using 'absLabel'. +absLabel :: KAbs (KName s t) a -> t+absLabel = nameLabel . absName+++-- * Abstraction the binder++-- | Acts on an abstraction @x'@ by unpacking @x'@ as @(n,x)@ for a fresh name @n@, and calculating @f n x@.+instance (Typeable s, Swappable t, Swappable a) => Binder (KAbs (KName s t) a) (KName s t) a s where+   (@@) :: KAbs (KName s t) a -> (KName s t -> a -> b) -> KNom s b+   (@@) x' f = freshKName (absLabel x') @@ \_ n -> f n $ x' `absApp` n+   (@>) :: KName s t -> a -> KAbs (KName s t) a+   (@>) nam a = AbsWrapper nam $ \nam' -> kswpN nam' nam a++-- | Concretes an abstraction at a particular name.   +-- Unsafe if the name is not fresh. +--+-- > (abst a x) `conc` a == x+--+-- > abst a (x `conc` a) == x -- provided a is suitably fresh. +--+-- > new' $ \a -> abst a (x `conc` a) == x  +instance Binder (KAbs n a) n a s => BinderConc (KAbs n a) n a s n where +   conc = absApp+   +-- * The bijection between @'Abs'@ and @'Nom'@+++-- | Bijection between @Nom@ and @Abs@.  Just an instance of 'binderToNom'.+absToNom :: (Typeable s, Swappable t, Swappable a) => KAbs (KName s t) a -> KNom s (KName s t, a)+absToNom = binderToNom ++-- | Bijection between @Nom@ and @Abs@.  Just an instance of 'nomToBinder'.+nomToAbs :: (Typeable s, Swappable t, Swappable a) => KNom s (KName s t, a) -> KAbs (KName s t) a+nomToAbs = nomToBinder ++++-- * Unpacking name-contexts and abstractions+++-- | Abstractions are equal up to fusing their abstracted names. +instance (Typeable s, Swappable t, Eq t, Eq a) => Eq (KAbs (KName s t) a) where+   AbsWrapper n1 f1 == AbsWrapper n2 f2 = +      (nameLabel n1 == nameLabel n2) && new (nameLabel n1) (\n -> f1 n == f2 n)  -- note atom ids of @n1@ and @n2@ are discarded. +++-- | We show an abstraction by evaluating the function inside `Abs` on a fresh name (with the default `Nothing` label)+instance (Typeable s, Swappable t, Swappable a, Show t, Show a) => Show (KAbs (KName s t) a) where+   show a' = a' @@! \n a -> show n ++ ". " ++ show a   -- could also use @@. or :@>, but this would introduce a @Typeable s@ typeclass condition.+++instance Default t => Applicative (KAbs (KName s t)) where -- use typeclass constraint on t.  all usual labels have defaults+   pure  :: a -> KAbs (KName s t) a+   pure a = AbsWrapper (justALabel def) (const a) +   (<*>) :: KAbs (KName s t) (a -> b) -> KAbs (KName s t) a -> KAbs (KName s t) b+   (<*>) (AbsWrapper n g) (AbsWrapper _ a) = AbsWrapper n $ \nam -> let nam' = (nam `withLabelOf` n) in g nam' $ a nam' -- must choose one of the two labels+-- TODO: use fuse?++-- | Apply f to a fresh element with label @t@+absFresh :: (Typeable s, Swappable t, Swappable a) => t -> (KName s t -> a) -> KAbs (KName s t) a+absFresh t f = freshKName t @@! \_ m -> m @> f m  -- It's OK to use '@@!' and release the bound ID, because we know it's bound in the result.+--- absFresh t f = genUnNom . atFresh t $ \m -> m @> f m++-- | Apply f to a fresh element with default label +absFresh' :: (Typeable s, Swappable t, Swappable a, Default t) => (KName s t -> a) -> KAbs (KName s t) a+absFresh' = absFresh def +++-- | Near inverse to applicative distribution.+-- @absFuncIn . absFuncOut = id@ but not necessarily other way around +absFuncOut :: (Typeable s, Swappable t, Swappable a, Swappable b, Default t) => (KAbs (KName s t) a -> KAbs (KName s t) b) -> KAbs (KName s t) (a -> b)+absFuncOut f = AbsWrapper (justALabel def) $ \nam a -> f (nam @> a) `conc` nam+++{- $tests Property-based tests are in "Language.Nominal.Properties.AbsSpec". -}
+ src/Language/Nominal/Binder.hs view
@@ -0,0 +1,369 @@+{-|+Module      : Binder +Description : Typeclass theory of binders +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Typeclass theory of binders ++-}++{-# LANGUAGE DataKinds+           , DeriveFunctor+           , DeriveGeneric+           , DeriveTraversable+           , DerivingVia+           , FlexibleContexts+           , FlexibleInstances+           , FunctionalDependencies+           , GeneralizedNewtypeDeriving+           , InstanceSigs+           , MultiParamTypeClasses+           , PartialTypeSignatures+           , PatternSynonyms+           , ScopedTypeVariables+           , StandaloneDeriving+           , TypeApplications+           , TypeOperators+           , ViewPatterns+           , UndecidableInstances+#-}++{-# OPTIONS_GHC -fno-warn-orphans #-} -- Suppress orphan instance of Data instance of Binder ctxbody.++module Language.Nominal.Binder+   ( -- * The @'Binder'@ typeclass+     -- $binder+       Binder (..), (@@!), (@@.), pattern (:@@!), nomApp, nomAppC, genApp, genAppC, resApp, resAppC, resAppC'+     -- * @'new'@ quantifier+     , newA, new, freshForA, freshFor+     -- * Detecting trivial @'KNom'@s, that bind no atoms in their argument+     , isTrivialNomBySupp, isTrivialNomByEq+     -- * @'Nom'@ and @'supp'@+     , kfreshen, freshen, BinderSupp (..)+     -- * Binder isomorphism+     -- $binderiso+     , kbinderToNom, knomToBinder, knomToMaybeBinder, binderToNom, nomToBinder, nomToMaybeBinder+     -- * Binder with concretion+     , BinderConc (..)+     -- * Tests+     -- $tests+   )+   where++import Data.Data+import Data.Maybe+import Data.Set         as S (toList) -- , Set) -- , union)+import GHC.Generics     hiding (Prefix) -- avoid clash with Data.Data.Prefix++import Language.Nominal.Utilities+import Language.Nominal.NameSet+import Language.Nominal.Name+import Language.Nominal.Nom+++-- * Binder++{- $binder++'Binder' is a typeclass for creating and unpacking local bindings.+The current development contains three instances of 'Binder':++* 'KNom' itself: the primitive binding construct of this package.+* 'Language.Nominal.Abs.KAbs': abstraction by a single name.+* 'Language.Nominal.Examples.IdealisedEUTxO.Chunk': a (generalisation of) EUTxO-style blockchains (the binding is in essence the names of edges connecting input-output pairs).++The simplest way to make a binder is to wrap a 'KNom' in further structure:++* 'Language.Nominal.Examples.IdealisedEUTxO.Chunk' has this design.+Its internal representation is structurally just a 'KNom' (what makes it interesting is that it is wrapped in some smart contructors that validate nontrivial extra structure, involving binding and more).++However, it is possible to design a binder without explicitly mentioning 'KNom' in its underlying representation:++* 'Language.Nominal.Abs.KAbs' is an instance.  For technical reasons its underlying representation uses functions, although a bijection does exist with a 'KNom'-based structure (see 'Language.Nominal.Abs.absToNom' and 'Language.Nominal.Abs.nomToAbs').++What makes 'Binder' interesting is a rich array of destructors (e.g. '@@', '@@!', '@@.', 'nomApp', 'nomAppC', 'genApp', 'genAppC', 'resApp', 'resAppC', 'resAppC'').+These correspond to common patterns of unpacking a binder and mapping to other types, and provide a consistent interface across different binding constructs.++-}++-- | A typeclass for unpacking local binding.+--+-- Provides a function to unpack a binder, giving access to its locally bound names.  Examples of binders include 'KNom', 'Language.Nominal.Abs.KAbs', and 'Language.Nominal.Examples.IdealisedEUTxO.Chunk'.+--+-- A 'Binder' comes with a rich array of destructors, like '@@', '@@!', '@@.', 'nomApp', 'nomAppC', 'genApp', 'genAppC', 'resApp', 'resAppC', 'resAppC''.+-- These correspond to common patterns of unpacking a binder and mapping to other types.+--+-- Below:+--+-- * @ctxbody@ is the type of the datum in its name-binding context, which consists intuitively of data wrapped in a local name binding.  (Canonical example: 'KNom'.)+-- * @ctx@ is the type of a concrete name-carrying representation of the local binding (atom, names, list of atoms, etc).  (Canonical examples: 'KAtom' and @['KAtom']@.)+-- * @body@ is the type of the body of the data.+-- * @s@ is the type of atoms output.  Output will be wrapped in @'KNom' s@.+--+-- For example the 'Language.Nominal.Abs.KAbs' instance of 'Binder' has type @Binder (KAbs (KName s t) a) (KName s t) s a@; and this means that+--+-- * a datum in @ctxbody = KAbs (KName s t) a@ can be unpacked as+-- * something in @ctx = KName s t@ and something in @body = a@, and+-- * mapped by a function of type @KName s t -> a -> b@ using '@@',+-- * to obtain something in @KNom s b@.+--+-- The other destructors ('@@!', '@@.', 'nomApp', 'nomAppC', 'genApp', 'genAppC', 'resApp', 'resAppC', 'resAppC'') are variations on this basic pattern which the wider development shows are empirically useful.+--+-- See also 'kbinderToNom' and 'nomToMaybeBinder'.+class (Typeable s, Swappable ctx, Swappable body, Swappable ctxbody) => Binder ctxbody ctx body s | ctxbody -> ctx body s  where+   -- | A destructor for the binder (required)+   (@@) :: ctxbody           -- ^ the data in its local binding+       -> (ctx -> body -> b) -- ^ function that inputs an explicit name context @ctx@ and a @body@ for that context, and outputs a @b@.+       -> KNom s b           -- ^ Result is a @b@ in a binding context.+   (@>) :: ctx -> body -> ctxbody+   -- ^ A constructor for the binder (optional, since e.g. your instance may impose additional well-formedness constraints on the input).  Call this @res@.+   (@>) = fromJust .: resMay+   -- | A partial constructor for the binder, if preferred.+   resMay :: ctx -> body -> Maybe ctxbody+   resMay = Just .: (@>)+   {-# MINIMAL (@@) #-} -- Please at least provide the destructor (@@).  The constructor is optional, since e.g. your instance may impose additional well-formedness constraints on the input.+infixr 9 @@+infixr 1 @>+-- documentation doesn't appear above for (@>) unless I use -- ^+++-- | Use this to map a binder to a type @b@, generating fresh atoms for any local bindings, and allowing them to escape.+(@@!) :: Binder ctxbody ctx body s => ctxbody -> (ctx -> body -> b) -> b+(@@!) = exit .: (@@)+infixr 9 @@!++-- | This pattern is not quite as useful as it could be, because it's too polymorphic to use a COMPLETE pragma on.  You can use it, but you may get incomplete pattern match errors.+pattern (:@@!) :: Binder ctxbody ctx body s => ctx -> body -> ctxbody+pattern ctx :@@! body <- ((@@! (,)) -> (ctx, body))+   where (:@@!) = (@>)+-- {-# COMPLETE (:@@!) #-}   -- States this match is complete.+infixr 0 :@@!++-- | Acts on a 'KNom' binder by applying a function to the body and the context of locally bound names.  Local names are preserved.+instance (Typeable s, Swappable a) => Binder (KNom s a) [KAtom s] a s where+   (@@) :: KNom s a -> ([KAtom s] -> a -> b) -> KNom s b+   (@@) = pami . reRes -- the @reRes@ ensures capture-avoidance, in case the input binding was formed using 'enter' instead of 'res'.+   -- (@@) a' f = imap f $ withExit a' res   -- flip imap +   (@>) :: (Typeable s, Swappable a) => [KAtom s] -> a -> KNom s a+   (@>) = res++-- | Use this to map a binder to a type @b@ with its own notion of restriction.  Bindings do not escape.+(@@.) :: (Binder ctxbody ctx body s, KRestrict s b) => ctxbody -> (ctx -> body -> b) -> b+(@@.) x' f = unNom $ x' @@ f++infixr 9 @@.++++-- | Unpacks a binder and maps into a @'KNom'@ environment.+--+-- 'nomApp' = 'flip' '(@@)'+nomApp :: Binder ctxbody ctx body s => (ctx -> body -> b) -> ctxbody -> KNom s b+nomApp = flip (@@)+-- | Unpacks a binder and maps into a @'KNom'@ environment.+-- Local bindings are not examined, and get carried over to the @'KNom'@.+--+-- 'nomAppC' = 'nomApp' . 'const'+nomAppC :: Binder ctxbody ctx body s => (body -> b) -> ctxbody -> KNom s b+nomAppC = nomApp . const+-- | Unpacks a binder.  New names are generated and released.+--+-- 'genApp' = 'flip' '(@@!)'+genApp :: Binder ctxbody ctx body s => (ctx -> body -> b) -> ctxbody -> b+genApp = flip (@@!)+-- | Unpacks a binder.  New names are generated and released.+-- Local bindings are not examined.+--+-- 'genAppC' = 'genApp' . 'const'+genAppC :: Binder ctxbody ctx body s => (body -> b) -> ctxbody -> b+genAppC = genApp . const+-- | Unpacks a binder and maps to a type with its own @'restrict'@ operation.+--+-- 'resApp' = 'flip' '(@@.)'+resApp :: (Binder ctxbody ctx body s, KRestrict s b) => (ctx -> body -> b) -> ctxbody -> b+resApp = flip (@@.)++-- | Unpacks a binder and maps to a type with its own @'restrict'@ operation.+-- Local bindings are not examined, and get carried over and @'restrict'@ed in the target type.+--+-- A common type instance is @(a -> Bool) -> KNom s a -> Bool@, in which case 'resAppC' acts to capture-avoidingly apply a predicate under a binder, and return the relevant truth-value.  See for example the code for 'transposeNomFunc'.+--+-- 'resAppC' = 'resApp' . 'const'+resAppC :: (Binder ctxbody ctx body s, KRestrict s b) => (body -> b) -> ctxbody -> b+resAppC = resApp . const+-- | Unpacks a binder and maps to a type with its own @'restrict'@ operation.  'Flip'ped version, for convenience.+--+-- A common type instance is @KNom s a -> (a -> Bool) -> Bool @, in which case 'resAppC'' acts to apply a predicate inside a binder and return the relevant truth-value.  See for example the code for 'transposeNomMaybe'.+--+-- 'resAppC'' = 'flip' 'resApp'+resAppC' :: (Binder ctxbody ctx body s, KRestrict s b) => ctxbody -> (body -> b) -> b+resAppC' = flip resAppC+++-- * Variants on 'res'+++{-- | A version of '@>' (@res@) that accepts a proxy to explicitly specify the type of atoms.+kres :: (Typeable s, Swappable body, Binder ctxbody ctx body s) => proxy s -> ctx -> body -> ctxbody+kres _ = (@>)+--}++++-- * New quantifier++-- | Evaluate predicate on fresh atom.+newA :: KRestrict s b => (KAtom s -> b) -> b+newA = resAppC' freshKAtom++-- | Evaluate predicate on fresh name with label @t@.+new :: (KRestrict s b, Swappable t) => t -> (KName s t -> b) -> b+new = resAppC' . freshKName+++-- | @n@ is @'freshFor'@ @a@ when @swp n' n a == a@ for a @'new'@ @n'@.  Straight out of the paper (<https://link.springer.com/article/10.1007/s001650200016 publisher> and <http://www.gabbay.org.uk/papers.html#newaas-jv author's> pdfs).+--+-- /Note: In practice we mostly need this for names.  This version is for atoms.+freshForA :: (Typeable s, Swappable a, Eq a) => KAtom s -> a -> Bool+freshForA n a = newA $ \n' -> kswp n' n a == a++-- | @n@ is @'freshFor'@ @a@ when @swp n' n a == a@ for a @'new'@ @n'@.  Straight out of the paper (<https://link.springer.com/article/10.1007/s001650200016 publisher> and <http://www.gabbay.org.uk/papers.html#newaas-jv author's> pdfs).+freshFor :: (Typeable s, Swappable t, Swappable a, Eq a) => KName s t -> a -> Bool+freshFor = freshForA . nameAtom+++-- * Detecting trivial @'KNom'@s, that bind no atoms in their argument++-- | Is the @'Nom'@ binding trivial?+--+-- This is the @'KSupport'@ version, for highly structured data that we can traverse (think: lists, tuples, sums, and maps).+--+-- See also @'isTrivialNomByEq'@, for less structured data when we have equality @'Eq'@ and swapping 'KSwappable'.+isTrivialNomBySupp :: forall s a. KSupport s a => KNom s a -> Bool+isTrivialNomBySupp = resApp $ kapart (Proxy :: Proxy s)++-- | Is the @'Nom'@ binding trivial?+--+-- This is the @'Eq'@ version, using @'freshFor'@.+-- Use this when we /do/ have equality and swapping, but /can't/ (or don't want to) traverse the type (think: sets).+--+-- See also @'isTrivialNomBySupp'@, for when we have @'KSupport'@.+isTrivialNomByEq :: (Typeable s, Swappable a, Eq a) => KNom s a -> Bool+isTrivialNomByEq = resApp $ \atms a -> and $ (`freshForA` a) <$> atms+++-- * @'KNom'@ and @'KSupport'@+++-- | Freshen all @s@-atoms, if we have @'KSupport'@.  Returns result inside @'KNom'@ binding to store the freshly-generated atoms.+kfreshen :: KSupport s a => proxy s -> a -> KNom s a+kfreshen p a = S.toList (ksupp p a) @> a++-- | Freshen all atoms, if we have @'Support'@.+freshen :: Support a => a -> Nom a+freshen = kfreshen atTom++-- | Wrapper for generic method of deriving support of binder+newtype BinderSupp a = BinderSupp {getBinderSupp :: a}+   deriving (Generic, Swappable)++instance (Binder ctxbody ctx body s, KSupport s ctx, KSupport s body) => KSupport s (BinderSupp ctxbody) where+   ksupp p (BinderSupp ctxbody) = ctxbody @@. \ctx body -> ksupp p (ctx, body)  -- Use of '(@@.)' here cleans out bound atoms.++{-- | Standard method to calculate the support of a binder+ksuppBinder :: (Binder ctxbody ctx body s, KSupport s ctx, KSupport s body) => proxy s -> ctxbody -> S.Set (KAtom s)+ksuppBinder = resAppC . ksupp -- Use of 'resAppC' here cleans out the (atom of the) abstracted name.+-- | @supp (ns @> x) == supp x \\ ns@+instance KSupport s a => KSupport s (KNom s a) where+   ksupp = ksuppBinder+--}++++-- * Binder isomorphism++{- $binderiso++The 'Binder' class has two functions pointing in opposite directions.+This suggests a standard isomorphism.  We expect:++> binderToNom <$> nomToMaybeBinder x == Just x+> nomToBinder . binderToNom == id++For 'KNom' and 'KAbs' it's safe to use 'knomToBinder'.  For others, like 'Language.Nominal.Examples.IdealisedEUTxO.Chunk', you would need 'knomToMaybeBinder', because additional well-formedness conditions are imposed on the constructor.+-}++kbinderToNom :: Binder ctxbody ctx body s => proxy ctxbody -> ctxbody -> KNom s (ctx, body)+kbinderToNom _ = nomApp (,)++knomToMaybeBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => proxy ctxbody -> KNom s (ctx, body) -> Maybe ctxbody+knomToMaybeBinder _ = genAppC $ uncurry resMay++knomToBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => proxy ctxbody -> KNom s (ctx, body) -> ctxbody+knomToBinder = fromJust .: knomToMaybeBinder++binderToNom :: Binder ctxbody ctx body s => ctxbody -> KNom s (ctx, body)+binderToNom = kbinderToNom (Proxy :: Proxy ctxbody)++nomToMaybeBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => KNom s (ctx, body) -> Maybe ctxbody+nomToMaybeBinder = knomToMaybeBinder (Proxy :: Proxy ctxbody)++nomToBinder :: (Typeable s, Swappable ctx, Swappable body, Binder ctxbody ctx body s) => KNom s (ctx, body) -> ctxbody+nomToBinder = knomToBinder (Proxy :: Proxy ctxbody)++-- * Scrap your boilerplate generic support++binderD :: DataType+binderD = mkDataType "Binder" [binderC]++binderC :: Constr+binderC = mkConstr binderD "(@>)" [] Prefix++instance {-# OVERLAPPABLE #-} (Binder ctxbody ctx body s, Typeable ctxbody, Data ctx, Data body) => Data ctxbody where++    gfoldl k z ctxbody = ctxbody @@! \ctx body -> z (@>) `k` ctx `k` body+    gunfold k z _ = k $ k $ z (@>)+    toConstr   = const binderC+    dataTypeOf = const binderD++-- * Binder with concretion++-- | Sometimes we can /concrete/ a bound entity @ctxbody@ at a datum @a@ (where it need not be the case that @a == ctx@), to return a body @body@.  In the case that @a == ctx@, we expect+--+-- > (a @> x) `conc` a == x+-- > a @> (x' `conc` a) == x+class Binder ctxbody ctx body s => BinderConc ctxbody ctx body s a where+   conc :: ctxbody -> a -> body+   conc = flip cnoc+   cnoc :: a -> ctxbody -> body+   cnoc = flip conc+   {-# MINIMAL conc | cnoc #-}++-- | Suppose we have a nominal abstraction @x' :: KNom s a@ where @a@ has its own internal notion of name restriction.+-- Then @cnoc () x'@ folds the 'KNom'-bound names down into @x'@ to return a concrete element of @a@.+--+-- > cnoc () = unNom+instance (Typeable s, Swappable a, KRestrict s a) => BinderConc (KNom s a) [KAtom s] a s () where+   cnoc = const unNom++-- | Suppose we have a nominal abstraction @x' :: KNom s a@.+-- Then @x' `conc` (Proxy :: Proxy s)@ triggers an IO action to strip the 'KNom' context and concrete @x'@ at some choice of fresh atoms.  +--+-- > cnoc (Proxy :: Proxy s) = exit +instance (Typeable s, Swappable a) => BinderConc (KNom s a) [KAtom s] a s (Proxy s) where+   cnoc = const exit ++-- | Concrete a nominal abstraction at a particular list of atoms.+-- Dangerous for two reasons:+--+-- * The list needs to be long enough.+-- * There are no guarantees about the order the bound atoms come out in.+instance (Typeable s, Swappable a) => BinderConc (KNom s a) [KAtom s] a s [KAtom s] where+   conc a' st = a' @@! \atms a -> perm (zip st atms) a+++{- $tests Property-based tests are in "Language.Nominal.Properties.NomSpec". -}
+ src/Language/Nominal/Equivar.hs view
@@ -0,0 +1,347 @@+{-|+Module      : Equivar +Description : Theory of equivariant orbit-finite structures+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++This module contains functions for manipulating lists of representatives which represent orbit-finite equivariant maps, and applying them to arguments by matching representatives to arguments up to a swapping (permutation) action.+-}++{-# LANGUAGE ConstraintKinds       +           , DataKinds             +           , DeriveGeneric         +           , DeriveAnyClass        +           , FlexibleContexts      +           , FlexibleInstances     +           , GADTs                +           , InstanceSigs          +           , MultiParamTypeClasses +           , PartialTypeSignatures +           , ScopedTypeVariables   +           , TypeOperators         +#-}++module Language.Nominal.Equivar+   (+    -- * Equivariance +    -- $intro+      KEvFun (..)+    , EvFun+    -- * Equivariant lists and maps+    -- $basiclists+    , kevRep+    , evRep+    , kevNub+    , evNub+    -- * Lookup +    -- $lookup+    , kevLookup+    , evLookup+    , kevLookupList'+    , kevLookupList+    , evLookupList+    -- * Orbit-finite equivariant maps+    -- $orbitfinite+    , KEvFinMap+    , EvFinMap+    , ($$)+    , constEvFinMap+    , extEvFinMap+    , evFinMap+    , fromEvFinMap+    -- * Tests+    -- $tests+    ) where++import qualified Data.Map.Strict          as DM -- for unifyPerm +import           Data.List                as L+import           Data.Proxy               (Proxy (..))+import qualified Data.Set                 as Set (fromList,empty) +import           GHC.Generics+import           Type.Reflection+import           Data.Type.Equality       -- for testEquality++import           Language.Nominal.Name+import           Language.Nominal.NameSet+import           Language.Nominal.Unify++-- For doctest:++-- $setup+-- >>> :m +Language.Nominal.Nom+-- >>> let [a, b, c] = exit $ freshAtoms [(), (), ()]+++{- $intro++A structure is __equivariant__ when it has a trivial swapping action:++> swp _ _ a == a++/__Example:__ Every element of a @Nameless@ type is equivariant./++/__Example:__ The mapping @const True :: Atoms -> Bool@ is equivariant./  ++This second example is a particularly important example because it illustrates that "being equivariant" is /not/ the same as "being nameless".  To be equivariant, you only need to be /symmetric/.  ++A structure is __equivariant orbit-finite__ when it can be represented by ++* taking finitely many representatives and +* closing under the swapping action.  +   +/__Example:__ the graph of the identity mapping @id :: Atom -> Atom@ can be represented by closing @[(a,a)]@ under all swappings.  So @id@ is equivariant orbit-finite./+   +Two equivariant orbit-finite maps may be compared for equality even though they may be infinite as functions, because they are finite as representatives-up-to-orbits.+Opearationally for us here in Haskell, it suffices to inspect the representatives and compare them for unifiability using the functions from "Unify". ++We will build:++* An equivariant function type 'KEvFun'.+* An equivariant orbit-finite space of maps 'KEvFinMap', and +* an equivariant application operation @$$@, for applying a 'KEvFinMap' (which under the hood is just a finite list of representatives) equivariantly to an argument. ++ __Warning:__ When applying a map equivariantly using '$$', It should hold that if @(m $$ a) == b@ then @supp b `isSubsetOf` supp a@.  If not, then unexpected behaviour may result.  The general mathematical reasons for this are discussed with examples e.g. in <http://dx.doi.org/10.4204/EPTCS.34.5 closed nominal rewriting> (see also <http://www.gabbay.org.uk/papers.html#clonre author's pdfs>).  Thus in the terminology of that paper, we need @m@ to be closed.  One way to guarantee this is to ensure that @b@ be @'Nameless'@, so that @b@ is a type like 'Bool' or 'Int' and @supp b@ is guaranteed empty.  In practice for the cases we care about, @b@ will indeed always be @'Nameless'@. +-}+++-- | @'KEvFun' s a b@ is just @a -> b@ in a wrapper.  +-- But, we give this wrapped function trivial swapping and support.  (For a usage example see the source code for 'Language.Nominal.Examples.IdealisedEUTxO.Val'.) +--+-- Functions need not be finite and are not equality types in general, so we cannot computably test that the actual function wrapped by the programmer actually /does/ have a trivial swapping action (i.e. really is equivariant).  +--+-- It's the programmer's job to only insert truly equivariant functions here.  Non-equivariant elements may lead to incorrect runtime behaviour.  +--+-- On an equivariant orbit-finite type, the compiler can step in with more stringent guarantees.  See e.g. 'KEvFinMap'. +newtype KEvFun s a b = EvFun { runEvFun :: a -> b -- ^ Function in a wrapper +                             }++instance (Typeable s, Swappable a, Swappable b) => Swappable (KEvFun s a b) where+   kswp (a1 :: KAtom t) (a2 :: KAtom t) (EvFun f) = +      case testEquality (typeRep :: TypeRep t) (typeRep :: TypeRep s) of  +         Just Refl  -> EvFun f   -- s and t are the same type+         Nothing    -> EvFun $ kswp a1 a2 f++instance (Typeable s, Swappable a, Swappable b) => KSupport s (KEvFun s a b) where+   ksupp _ _ = Set.empty   +                              +-- | @'Tom'@-equivariant function-space+type EvFun = KEvFun Tom+++-- * Equivariant lists and maps++{- $basiclists++Now for some basic functions that filter an input list down to a nub of representatives.  ++-}++-- | Filter a list down to one representative from each atoms-orbit (choosing first representative of each orbit). +kevRep :: KUnifyPerm s a => proxy s -> [a] -> [a]+kevRep = L.nubBy . kunifiablePerm++-- | Instance for @'Tom'@ atom type.+evRep :: UnifyPerm a => [a] -> [a]+evRep = kevRep atTom++-- | Restrict a Map to its equivariant nub, discarding all but one of each key-orbit+kevNub :: (Ord a, KUnifyPerm s a) => proxy s -> DM.Map a b -> DM.Map a b+kevNub p m = DM.restrictKeys m ((Set.fromList . kevRep p . DM.keys) m) ++-- | Instance for unit atom type.+evNub :: (Ord a, UnifyPerm a) => DM.Map a b -> DM.Map a b+evNub = kevNub atTom++-- * Lookup ++{- $lookup++So we have a finite set of representative pairs.  +How do we unify a putative input with a representative to find a matching output?++-}++-- | Equivariantly apply a list of pairs, which we assume represents a map, to an element.+-- Also returns the source element.+kevLookupList' :: (KUnifyPerm s a, KUnifyPerm s b) => proxy s -> [(a, b)] -> a -> Maybe (a, b)+kevLookupList' _ []           _  = Nothing    -- Empty list?  Stop.+kevLookupList' p ((a, b) : t) a' =            -- Nonempty list? +   let r = kunifyPerm p a a' in               -- fetch unifier, if exists+   if isJustRen r then Just (a, ren r b)      -- if it does, Just apply unifying renaming +                  else kevLookupList' p t a'  -- otherwise, continue down list. ++-- | Equivariantly apply a list of pairs (which we assume represents a map), to an element+kevLookupList :: (KUnifyPerm s a, KUnifyPerm s b) => proxy s -> [(a,b)] -> a -> Maybe b+kevLookupList p xs a = snd <$> kevLookupList' p xs a++-- | Equivariantly apply a list of pairs (which we assume represents a map), to an element.  @'Tom'@ version.+evLookupList :: (UnifyPerm a, UnifyPerm b) => [(a,b)] -> a -> Maybe b+evLookupList = kevLookupList atTom++-- | Equivariantly apply a map @m@ to an element @a@.  +-- Also returns a unifier.+kevLookup' :: (KUnifyPerm s a, KUnifyPerm s b) => proxy s -> DM.Map a b -> a -> Maybe (a, b)+kevLookup' p m = kevLookupList' p (DM.toList m)++-- | Equivariantly apply a map @m@ to an element @a@.  +-- +-- * If @a == ren r a'@ for some @r :: Ren@ and @m a' == b'@, +--+-- * then @kevLookup m a == ren r b'@. +--+-- For this to work, we require types @a@ and @b@ to support a @'ren'@ action, meaning they should support notions of unification up to permutation.+kevLookup :: (KUnifyPerm s a, KUnifyPerm s b) => proxy s -> DM.Map a b -> a -> Maybe b+kevLookup p m = fmap snd . kevLookup' p m++-- | @'kevLookup'@ instantiated to a @'Tom'@.+evLookup :: (UnifyPerm a, UnifyPerm b) => DM.Map a b -> a -> Maybe b+evLookup = kevLookup atTom++++-- * Orbit-finite equivariant maps+{- $orbitfinite+++@'KEvFinMap'@ is a type for /orbit-finite/ equivariant maps (contrast with @'KEvFun'@, a type for equivariant functions which need not be orbit-finite).+Values of @'KEvFinMap'@ must be constructed using ++* @'constEvFinMap'@, +* @'extEvFinMap'@ and +* @'evFinMap'@.++ Under the hood, @KEvFinMap s a b@ has just one constructor: ++ > DefAndRep b [(a, b)]  ++ @DefAndRep@ stands for /Default and list of Representatives/.+ We represent an orbit-finite equivariant map from @a@ to @b@ as ++ * A default value in @b@, and++ * a list of key-value pairs, to be applied up to permuting @s@-sorted atoms in the keys. ++ @DefAndRep@ does not store the atoms it wants permuted, in its structure.  It's just a pair of an element in @b@ and a list of pairs from @[(a, b)]@.  At the point where we use @'$$'@ to equivariantly apply some @DefAndRep@ structure to some argument in @a@, we specify over which atoms we wish to be equivariant.  + + Thus: calling this @KEvFinMap@ is convenient but slighly misleading: the equivariance lies in the @'$$'@-/application/ of a @KEvFinMap@-wrapped collection of representatives, to an argument. ++-}++-- | A type for orbit-finite equivariant maps.+data KEvFinMap s a b = DefAndRep (Nameless b) [(a, Nameless b)]  +    deriving (Show, Generic, Swappable)++-- | We insist @a@ and @b@ be @k@-swappable so that the mathematical notion of support (which is based on nominal sets) makes sense.  +--+-- Operationally, we don't care: if see something of type @KEvFinMap s a b@, we return @Set.empty@.+instance (Typeable s, Swappable a, Swappable b) => KSupport s (KEvFinMap s a b) where +   ksupp _ _ = Set.empty  ++-- | @'KEvFinMap'@ at a @'Tom'@.  Thus, a type for orbit-finite @'Tom'@-equivariant maps.+type EvFinMap a b = KEvFinMap Tom a b+++-- | Equivariant application of an orbit-finite map.  +-- Given a map (expressed as finitely many representative pairs) and an argument ... +--+-- * it tries to rename atoms to match the argument to the first element of one of its pairs and +-- * if it finds a match, it maps to the second element of that pair, suitably renamed. +($$) :: forall s a b. (KUnifyPerm s a, Eq b) => KEvFinMap s a b -> a -> b+DefAndRep (Nameless b') xs $$ a = maybe b' getNameless $ kevLookupList (Proxy :: Proxy s) xs a ++infixr 0 $$++-- | A constant equivariant map. We assume the codomain is @'Nameless'@.+--+-- >>> (constEvFinMap 42 :: EvFinMap Char Int) $$ 'x'+-- 42+--+-- >>> (constEvFinMap 0 :: EvFinMap Atom Int) $$ a+-- 0 +constEvFinMap :: KUnifyPerm s a => b -> KEvFinMap s a b+constEvFinMap b = DefAndRep (Nameless b) []+++-- | Extends a map with a new orbit, by specifying a representative @a@ maps to @b@.+-- We assume codomain @b@ is @'Nameless'@, as discussed above. +--+-- >>> (extEvFinMap 'x' 7 $ (constEvFinMap 42 :: EvFinMap Char Int)) $$ 'x'+-- 7+--+-- >>> (extEvFinMap 'x' 7 $ (constEvFinMap 42 :: EvFinMap Char Int)) $$ 'y'+-- 42+--+-- >>> let [m, n, o] = exit $ freshNames [(), (), ()] +-- >>> m == n+-- False+-- >>> unifiablePerm m n+-- True+-- >>> (extEvFinMap m 7 $ (constEvFinMap 42 :: EvFinMap (Name ()) Int)) $$ n+-- 7+-- >>> (extEvFinMap o 8 (extEvFinMap m 7 $ (constEvFinMap 42 :: EvFinMap (Name ()) Int))) $$ n+-- 8+extEvFinMap :: forall s a b. (KUnifyPerm s a, Eq a, Eq b) => a -> b -> KEvFinMap s a b -> KEvFinMap s a b+extEvFinMap a b f@(DefAndRep (Nameless b') xs) = case kevLookupList' (Proxy :: Proxy s) xs a of+    Nothing+-- No mapping but sending a to the default value?  Then noop. +        | b == b'   -> f  +-- No mapping and not sending a to the default value?  Add (a,b)+        | otherwise -> DefAndRep (Nameless b') $ (a, Nameless b) : xs  +    Just (a'', Nameless b'')+-- (a,b) is already there, up to permuting atoms in a (b is nameless).  Noop.+        | b == b''  -> f+-- (a,b) is not already there up to permuting atoms in a.  Remove (a'',b'') and replace with (a'',b).  We really rely on b being nameless, here.+        | otherwise -> DefAndRep (Nameless b') [(c, if c == a'' then Nameless b else d) | (c, d) <- xs]++-- | Constructs an orbit-finite equivariant map by prescribing a default value, and+-- finitely many argument-value pairs.+-- We assume the codomain is @'Nameless'@, as discussed above. +--+-- >>> let f = evFinMap 42 [('x', 7), ('y', 5), ('x', 13)] :: EvFinMap Char Int+-- >>> map (f $$) ['x', 'y', 'z']+-- [13,5,42]+--+-- >>> let atmEq = evFinMap False [((a,a), True)] :: EvFinMap (Atom, Atom) Bool +-- >>> map (atmEq $$) [(b,b), (c,c), (a,c), (b,c)]+-- [True,True,False,False]+--+-- >>> let g = evFinMap 2 [((a,a), 0), ((b,c), 1)] :: EvFinMap (Atom, Atom) Int +-- >>> map (g $$) [(b,b), (c,c), (a,c), (b,c)]+-- [0,0,1,1]+evFinMap :: (KUnifyPerm s a, Eq a, Eq b) +         => b             -- ^ Default value.+         -> [(a, b)]      -- ^ List of exceptional argument-value pairs. In case of conflict, later pairs overwrite earlier pairs.+         -> KEvFinMap s a b+evFinMap = L.foldl' (\m (a, b) -> extEvFinMap a b m) . constEvFinMap++-- | Extracts default value und list of exceptional argument-value pairs from an @'EvFinMap'@.+--+-- >>> fromEvFinMap $ (evFinMap 42 [('x', 7), ('y', 5), ('x', 13)] :: EvFinMap Char Int)+-- (42,[('y',5),('x',13)])+--+fromEvFinMap :: KEvFinMap s a b -> (b, [(a, b)])+fromEvFinMap (DefAndRep (Nameless b') xs) = (b', [(a, b) | (a, Nameless b) <- xs])++-- | 'KEvFinMap' is compared for equality by comparing the default value and the representatives, up to permutations.  +--+-- __Edge case:__ If a codomain type is orbit-finite (e.g. @'Bool'@ and @'(Atom,Atom)'@, with two orbits, or @'Atom'@ with one), and representatives exhaust all possibilities, then the default value will never be queried, yet it will still be considered in our equality test.  +instance (KUnifyPerm s a, Eq b) => Eq (KEvFinMap s a b) where+    f1@(DefAndRep b1 xs1) == f2@(DefAndRep b2 xs2)+        =    (b1 == b2)                                    -- default values equal?+          && all (\(a, Nameless b) -> (f2 $$ a) == b) xs1  -- check equality by representatives +          && all (\(a, Nameless b) -> (f1 $$ a) == b) xs2+-- TODO: replace with extensionality test++-- This looks like 'Nameless', but 'Nameless' cannot be parameterised over s.+instance (KUnifyPerm s a, KUnifyPerm s b, Eq b) => KUnifyPerm s (KEvFinMap s a b) where+    kunifyPerm _ f g   +        | f == g    = mempty+        | otherwise = Ren Nothing+    ren = const id+++{- $tests Property-based tests are in "Language.Nominal.Properties.EquivarSpec". -}+
+ src/Language/Nominal/Examples/Assembly1.hs view
@@ -0,0 +1,79 @@+{-|+Module      : Simple Assembly Example 1 +Description : A simple assembly language, with binding +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Based on <https://github.com/ekmett/bound/blob/master/examples/Imperative.hs an example in the Bound package>.  +What makes this interesting is the binding behaviour of 'Add', which adds two numbers and binds the result to a fresh register with scope over subsequent instructions. +++-}++{-# LANGUAGE InstanceSigs          +           , DeriveGeneric         +           , MultiParamTypeClasses +           , DeriveAnyClass       -- to derive 'Swappable' +           , FlexibleInstances     +#-}+++module Language.Nominal.Examples.Assembly1+    where++import GHC.Generics++import Language.Nominal.Name +import Language.Nominal.Nom+import Language.Nominal.Binder+import Language.Nominal.Abs +import Language.Nominal.Sub ++-- | Variables are string-labelled names+type V = Name String ++-- | An operand is an integer literal or a variable+data Operand = Lit Int | Var V +  deriving (Eq, Generic, Swappable, Show)++-- | Substitution as standard on 'Operand'+instance KSub V Operand Operand where+   sub :: V -> Operand -> Operand -> Operand+   sub _ _ (Lit n)  = Lit n+   sub v o (Var v') = if v == v' then o else Var v' ++-- | Terms of our assembly language +data Prog = Ret Operand        -- ^ Return a value +          | Add Operand Operand (KAbs V Prog) -- ^ Add two operands and store the value in a fresh variable which is local to subsequent computation (the third argument) +  deriving (Eq, +            Generic, +            Swappable, +            Show, +            KSub V Operand -- ^ Substitution on 'Prog'rams is generic+           )++-- | Evaluate an operand.  +--+-- * A literal maps to its corresponding integer.  +-- * If asked to evaluate a free variable, complain. +evalOperand :: Operand -> Int+evalOperand (Lit i) = i+evalOperand (Var _) = undefined ++-- | Evaluate a program +evalProg :: Prog -> Int+evalProg (Ret o)        = evalOperand o+evalProg (Add o1 o2 x') = evalProg (x' `conc` Lit (evalOperand o1 + evalOperand o2)) -- `conc` here substitutes a value for a bound name in an abstraction++-- | Add 1 2 [v] Add v v [w] Ret w  +example1 :: Prog +example1 = freshNames ["v", "w"] @@! \_ [v, w] -> +           Add (Lit 1) (Lit 2) $ v :@> Add (Var v) (Var v) $ w :@> Ret (Var w) -- :@> is name-abstraction, also called 'abst'. ++-- | 6 +example1eval :: Int +example1eval = evalProg example1 +
+ src/Language/Nominal/Examples/Assembly2.hs view
@@ -0,0 +1,92 @@+{-|+Module      : Simple Assembly Example 2 +Description : A simple assembly language, with binding and variable-swapping +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Based on <https://github.com/ekmett/bound/blob/master/examples/Imperative.hs an example in the Bound package>.  This is interesting for the binding behaviour of 'Add' and the swapping behaviour of 'Swp'. +'Add' adds two numbers and binds the result to a fresh register with scope over subsequent instructions. +'Swp' swaps the contents of two registers with scope over subsequent instructions. ++-}++{-# LANGUAGE InstanceSigs          +           , DeriveGeneric         +           , MultiParamTypeClasses +           , DeriveAnyClass       -- to derive 'Swappable' +           , FlexibleInstances     +#-}+++module Language.Nominal.Examples.Assembly2+    where++import GHC.Generics++import Language.Nominal.Name +import Language.Nominal.Nom+import Language.Nominal.Binder+import Language.Nominal.Abs +import Language.Nominal.Sub ++-- | Variables are string-labelled names+type V = Name String ++-- | An operand is an integer literal or a variable+data Operand = Lit Int | Var V +  deriving (Eq, Generic, Swappable, Show)++-- | Substitution as standard on 'Operand'+instance KSub V Operand Operand where+   sub :: V -> Operand -> Operand -> Operand+   sub _ _ (Lit n)  = Lit n+   sub v o (Var v') = if v == v' then o else Var v' ++-- | Terms of our assembly language +data Prog = Ret Operand        -- ^ Return a value +          | Swp Operand Operand Prog -- ^ Swap the contents of two variables+          | Add Operand Operand (KAbs V Prog) -- ^ Add two operands and store the value in a fresh variable which is local to subsequent computation (the third argument) +  deriving (Eq, +            Generic, +            Swappable, +            Show, +            KSub V Operand -- ^ Substitution on 'Prog'rams is generic+           )++-- | Evaluate an operand.  +--+-- * A literal maps to its corresponding integer.  +-- * If asked to evaluate a free variable, complain. +evalOperand :: Operand -> Int+evalOperand (Lit i) = i+evalOperand (Var _) = undefined ++-- | Normalise a program by executing any embedded Swp commands. +normaliseProg :: Prog -> Prog +normaliseProg (Swp (Var v1) (Var v2) x)  +             = normaliseProg $ swpN v1 v2 x+normaliseProg (Add o1 o2 x') +             = Add o1 o2 $ normaliseProg <$> x'+normaliseProg p = p++-- | Evaluate a program +evalProg :: Prog -> Int +evalProg = go . normaliseProg+   where +      go :: Prog -> Int+      go (Ret o)        = evalOperand o+      go (Add o1 o2 x') = go $ x' `conc` Lit (evalOperand o1 + evalOperand o2) -- `conc` here substitutes a value for a bound name in an abstraction+      go _              = undefined++-- | Add 1 2 [v] Add v v [w] Swp v w Ret w  +example1 :: Prog +example1 = freshNames ["v", "w"] @@! \_ [v, w] -> +           Add (Lit 1) (Lit 2) $ v :@> Add (Var v) (Var v) $ w :@> Swp (Var v) (Var w) $ Ret (Var w)   -- :@> is name-abstraction, also called 'abst'. ++-- | 3 +example1eval :: Int +example1eval = evalProg example1 +
+ src/Language/Nominal/Examples/IdealisedEUTxO.hs view
@@ -0,0 +1,844 @@+{-|+Module      : Idealised EUTxO +Description : Haskell rendering of the mathematical idealisation of the Extended UTxO model +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Haskell rendering of the <https://arxiv.org/abs/2003.14271 mathematical idealisation of the Extended UTxO model>. +-}++{-# LANGUAGE ConstraintKinds            +           , DataKinds                  +           , DefaultSignatures          +           , DeriveAnyClass             +           , DeriveGeneric              +           , DerivingStrategies         +           , DerivingVia                +           , EmptyCase                   -- for \case {} in GHasInputPositions+           , LambdaCase                  -- for \case {} in GHasInputPositions+           , FlexibleInstances          +           , FlexibleContexts            -- so we can write `Swappable d`+           , FunctionalDependencies     +           , GeneralizedNewtypeDeriving +           , IncoherentInstances         -- monoid instance of Maybe Chunk +           , InstanceSigs               +           , MultiParamTypeClasses      +           , ScopedTypeVariables        +           , StandaloneDeriving         +           , TypeOperators              +           , UndecidableInstances       +#-}++{-# OPTIONS_GHC -fprint-explicit-foralls #-}  -- more detailed type information, along with :t +v <expr>++module Language.Nominal.Examples.IdealisedEUTxO +    ( +    -- * Types for inputs, outputs, and transaction lists+    -- $types+       Position, Input (..), Output (..), TransactionF (..), Transaction, Context,+    -- * Calculating input and output positions +    -- $calculating+       HasInputPositions (..), HasOutputPositions (..),+    -- * Validators+    -- $validator+       Validator (..), ValTriv (..), Val (..), ValFin (..),+    -- * Chunks+    -- $chunks+       Chunk (..), transactionValid, singletonChunk, unsafeSingletonChunk, txListToChunk, nomTxListToNomChunk, nomTxListToChunk, +    -- * Examples+    -- $examples+    exampleCh0, exampleCh1, exampleCh2, exampleCh12, exampleCh21, exampleCh12',+    -- * Unspent (dangling) elements: UTxO, UTxI, UTxC+    -- $unspent+    outputsOfTx, inputsOfTx, txPoint, contextsOfTx, utxosOfChunk, utxisOfChunk, contextPos, utxcsOfChunk,+    -- * Combining and extending chunks+    appendTxChunk, appendTxMaybeChunk, concatChunk, safeConcatChunk,+    -- * Splitting chunks up +    genUnNomChunk, isPrefixChunk, chunkLength, chunkTail, chunkHead, warningNotChunkTail, chunkTakeEnd, subTxListOf, reverseTxsOf, chunkToHdTl, chunkToHdHdTl,+    -- * Blockchain+    Blockchain, getBlockchain, blockchain,   +    -- * Is Chunk / Blockchain check+    chunkBindingOK, chunkValidatorsOK, isChunk, isChunk', isBlockchain, isBlockchain', +    -- * Intensional equality of 'Chunk'+    -- $intension+    IEq, equivChunk +    -- * Tests+    -- $tests+    )+    where++import           Data.List                  as L+import           Data.List.NonEmpty         (NonEmpty (..))+import           Data.List.Unique +import           Data.List.Extra            (disjoint, takeEnd)+import           Data.Maybe+import           Data.Functor               ((<&>)) +import           Control.Monad              (guard, zipWithM) +import qualified Data.Set                   as S+import           Foreign+import           GHC.Generics+import           GHC.Stack                  (HasCallStack)+import           Numeric.Partial.Monoid+import           Numeric.Partial.Semigroup++import           Language.Nominal.Utilities +import           Language.Nominal.Name +import           Language.Nominal.NameSet+import           Language.Nominal.Nom+import           Language.Nominal.Binder+import           Language.Nominal.Unify+import           Language.Nominal.Equivar++++-- * Types for inputs, outputs, and transaction lists +{- $types+These are the basic types of our development.++* A __'Position'__ is just an 'Atom' (a unique identifier).  It identifies a location on the blockchain.+* __'Input's__ point backwards towards outputs.  Inputs and outputs identify one another by position.+* __'Output's__ point wait for future inputs to point to them by naming the position they carry.  Outputs carry validators, to check whether they like any input that tries to point to them.+* A __'Transaction'__ is a list of inputs (pointing backwards) and a list of outputs (pointing forwards).+* A __'Context'__ is a transaction with a distinguished designated input, i.e. an input-in-context.  In fact, outputs validate contexts; this is what makes it EUTxO, for Extended UTxO, instead of just UTxO. +* We also introduce the notion of __'Chunk'__, which is a valid list of transactions under a name-binding, and a notion of __UTxI__, meaning an input that does not refer to a preceding output in its chunk. +* A __'Blockchain'__ is then a 'Chunk' with no UTxIs.  The benefit of working with Chunks as primitive is that valid Chunks form a monoid and are down-closed under taking sublists.  ++These are all novel observations which are original to this development and the associated paper(s).+Then mathematically, the types below solve and make operational the following equations, parameterised over types @r@ and @d@ of /redeemer/s and /data/: ++@+Input       =  Position x r +Output      =  d x Validator+Transaction =  Input-list x Output-list+Context     =  Input-nonempty-list x Output-list+Validator   <= (d x Context) -> Bool -- Val and ValFin are +                                 -- two solutions to this subset inclusion+@++More exposition follows in the code.  See also the tests in "Language.Nominal.Properties.Examples.IdealisedEUTxOSpec":+-} ++-- | Positions are atoms.  These identify locations in a 'Chunk' or 'Blockchain'.+type Position             = Atom +-- | An input has a position and a /redeemer/ @r@.  Think of the redeemer is a key which we use to unlock access to whatever output this input wants to connect to.  +--+-- Here @r@ is a type parameter, to be instantiated later.+data Input r              = Input Position r                       +   deriving stock (Show, Eq, Ord, Generic)+-- | An output has a position, a /datum/ @d@, and a /validator/ @v@.  +-- +-- * Think of the /datum/ as a fragment of state data which is attached to this output.+-- * Think of the /validator/ as a machine which, if given a suitable redeemer (along with other stuff), with authorise or forbid access to this output.+-- +-- @d@ and @v@ are type parameters, to be instantiated later.+data Output d v           = Output Position d v                    +   deriving stock (Show, Eq, Ord, Generic)+-- | A @TransactionF@ consists of an @f@ of inputs, and a list of outputs.  +-- +-- Type parameters are:+--+-- * @f@ a parameter which can be instantiated to a type-constructor (<http://dev.stephendiehl.com/fun/001_basics.html#higher-kinded-types higher-kinded types>).  In this file, @f@ will be either list or nonempty list. +-- * @r@ a parameter for the /redeemer/.+-- * @d@ a parameter for the /datum/.+-- * @v@ a parameter for the /validator/.+data TransactionF f r d v = Transaction (f (Input r)) [Output d v] +   deriving stock (Generic)+-- A @Transaction@ is a @'TransactionF'@ over lists.  +-- +-- Here @f@ is instantiated to the list type, so Transaction r d v = Transaction [Input r] [Output d v]. +type Transaction          = TransactionF []            +-- A @Context@ is a @'TransactionF'@ over nonempty lists; the first element of the list of intputs is taken to be the distinguished "point" of the context. +-- +-- Here @f@ is instantiated to the nonempty list type, so Context r d v = Transaction (NonEmpty (Input r)) [Output d v]. +type Context              = TransactionF NonEmpty++deriving stock instance (Eq r, Eq d, Eq v) => Eq (Transaction r d v)  +deriving stock instance (Eq r, Eq d, Eq v) => Eq (Context r d v)++-- With @ConstraintKinds@, the type synonym @KSupport Tom@ is allowed in the assumptions, but must be spelled out in the head.  +instance Support r => KSupport Tom (Input r) where    +instance (Support d, Support v) => KSupport Tom (Output d v) where+instance (Support d, Support r, Support v) => KSupport Tom (Context r d v)+instance (Support d, Support r, Support v) => KSupport Tom (Transaction r d v)++instance Swappable r => Swappable (Input r) +instance (Swappable d, Swappable v) => Swappable (Output d v)+instance (Swappable r, Swappable d, Swappable v) => Swappable (Transaction r d v)+instance (Swappable r, Swappable d, Swappable v) => Swappable (Context r d v)++instance UnifyPerm r => KUnifyPerm Tom (Input r)+instance (UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Output d v)+instance (UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Context r d v)+instance (UnifyPerm d, UnifyPerm r, UnifyPerm v) => KUnifyPerm Tom (Transaction r d v)++deriving instance (Show (f (Input r)), Show d, Show v) => Show (TransactionF f r d v)+++-- * Calculating input and output positions ++{- $calculating+A technical matter: we exploit the Haskell typeclass mechanisms to set up some machinery to calculate the input and output positions mentioned in a data structure.  This resembles the development of @'Support'@, but specialised to intputs and outputs.+-}+ +-- | A typeclass for types for which we can calculate __input positions__.+--+-- @'inputPositions'@ just traverses @a@'s type structure, looking for subtypes of the form @'Input' p _@, and collecting the @p@s.+-- The only interesting instance is that of @'Nom' a@, where bound @p@s get garbage-collected. +class HasInputPositions a where+    inputPositions :: a -> [Position]+    default inputPositions :: (Generic a, GHasInputPositions (Rep a)) => a -> [Position]+    inputPositions = gInputPositions . from++instance HasInputPositions (Input r) where+   inputPositions (Input p _)  = [p]++instance HasInputPositions (Output d v) where+   inputPositions Output {} = []++instance (HasInputPositions a, HasInputPositions b) => HasInputPositions (a,b)+instance HasInputPositions a => HasInputPositions [a]+instance HasInputPositions a => HasInputPositions (NonEmpty a)+instance HasInputPositions (Transaction r d v) where+   inputPositions (Transaction is _) = inputPositions is -- Not boilerplate: must not count inputs that appear in the list of outputs. ++-- | A typeclass for types for which we can calculate __output positions__. +--+-- @'outputPositions'@ just traverses @a@'s type structure, looking for subtypes of the form @'Output' p _ _@, and collecting the @p@s. +-- The only interesting instance is that of @'Nom' a@, where bound @p@s get garbage-collected. +class HasOutputPositions a where+    outputPositions :: a -> [Position]+    default outputPositions :: (Generic a, GHasOutputPositions (Rep a)) => a -> [Position]+    outputPositions = gOutputPositions . from++instance HasOutputPositions (Input r) where+   outputPositions (Input _ _) = [] ++instance HasOutputPositions (Output d v) where+   outputPositions (Output p _ _) = [p]++instance (HasOutputPositions a, HasOutputPositions b) => HasOutputPositions (a,b)+instance HasOutputPositions a => HasOutputPositions [a]+instance HasOutputPositions a => HasOutputPositions (NonEmpty a)+instance HasOutputPositions (Transaction r d v) where+   outputPositions (Transaction _ os) = outputPositions os  +++instance (Swappable a, HasOutputPositions a) => HasOutputPositions (Nom a) where+   outputPositions = resAppC outputPositions ++-- * Unspent (dangling) elements: UTxO, UTxI, UTxC+{- $unspent++We care about which inputs point to earlier outputs, and which outputs point to later inputs, and which do not.  Specifically, we introduce three functions:++* @'utxosOfChunk'@, calculating those outputs that do not point to a later input in a chunk.  This is standard (albeit for chunks, not blockchains).+* @'utxisOfChunk'@, calculating those inputs that do not point to an earlier output in a chunk.  While not complicated to define, the explicit emphasis on this as an interesting value to calculate comes from our shift from working with /'Blockchain's/ to working with /'Chunk's/.+* @'utxcsOfChunk'@, calculating those contexts (inputs-in-their-transaction) that do not point to an earlier output in a chunk.  Again, the explicit emphasis on this as an interesting value to calculate comes from our shift from working with /'Blockchain's/ to working with /'Chunk's/.+-}++-- | Return the output-list of a 'Transaction'.+outputsOfTx :: Transaction r d v -> [Output d v]+outputsOfTx (Transaction _ os) = os++-- | Return the input-list of a 'Transaction'.+inputsOfTx :: Transaction r d v -> [Input r]+inputsOfTx (Transaction is _) = is++-- | Point a transaction at @p@ +txPoint :: Support r => Transaction r d v -> Position -> Context r d v+txPoint (Transaction is os) p = Transaction (atomPoint p is) os+ +-- | Form the contexts of a 'Transaction'.+contextsOfTx :: Support r => Transaction r d v -> [Context r d v]+contextsOfTx tx = txPoint tx <$> inputPositions tx++-- | Calculate __unspent outputs__.+-- +-- We tell an output is unspent when its position isn't bound in the enclosing 'Nom' name-context.+utxosOfChunk :: Validator r d v => Chunk r d v -> [Output d v]+utxosOfChunk = resAppC $ concatMap outputsOfTx ++-- | Calculate __unspent inputs__. +--+-- Because we're dealing with transaction lists, we care about dangling /inputs/ (which we call UTxIs) as well as UTxOs.+utxisOfChunk :: Validator r d v => Chunk r d v -> [Input r]+utxisOfChunk = resAppC $ concatMap inputsOfTx -- accumulate inputs listwise.  The 'restrict' implicit in the use of 'resAppC' filters out outputs that mention bound names.++-- | What's the point of my context?   The position @p@ of the first element of the input list of a context is deemed to be the "call site" from which the context tries to find a preceding output (with position @p@) in its @'Chunk'@. +contextPos :: Context r d v -> Position+contextPos (Transaction (Input p _ :| _) _) = p ++-- | Calculate unspent __input contexts__. +--+-- Because we're dealing with transaction lists, we care about dangling /contexts/ (which we call UTxCs). +utxcsOfChunk :: Validator r d v => Chunk r d v -> Nom [Context r d v] -- the top-level Nom binding here stores the bound names of the chunk, i.e. those participating in an Input-Output binding within the chunk.+utxcsOfChunk = nomApp $ \ps txs ->  +    L.filter (\c -> contextPos c `notElem` ps) (concatMap contextsOfTx txs)+++-- * Validators++{- $validator+Our types for 'Output', 'Transaction', and 'Context' are parameterised over a type of validators.  We now build a typeclass 'Validator' to hold validators, and build two instances 'Val' and 'ValFin': ++* 'Val' is just a type of functions wrapped up in a wrapper saying "I am a validator".  If you have a function and it's a validator, you can put it here.+* 'ValFin' is an /equivariant orbit-finite map/ type, intended to be used with the machinery in "Language.Nominal.Equivar".  A significant difference from 'Val' is that 'ValFin' can support equality 'Eq'. +-}++-- | A typeclass for __validators__.  A validator is an equivariant object that takes a datum and a @'Context'@, and returns a @'Bool'@.+class (Support r, Support d, Support v) => Validator r d v | v -> r d where  +    validate :: v -> d -> Context r d v -> Bool++-- | A type for trivial validators that always return true+data ValTriv r d = ValTriv+    deriving (Eq, Ord, Show, Read)++deriving via Nameless (ValTriv r d) instance Swappable (ValTriv r d)+deriving via Nameless (ValTriv r d) instance KUnifyPerm Tom (ValTriv r d)+deriving via Nameless (ValTriv r d) instance KSupport Tom (ValTriv r d)++instance (Support r, Support d) => Validator r d (ValTriv r d) where+    validate ValTriv _ _ = True++-- | A 'Val' is an equivariant predicate on datum and context.  +-- For convenience we make it @'Nameless'@. +newtype Val r d = Val (EvFun (d, Context r d (Val r d))  Bool)+    deriving newtype IEq +    deriving (Swappable, KRestrict Tom, KSupport Tom) via Nameless (Val r d)+instance Show (Val r d) where+    show = const "Val"++-- | 'Val' is a 'Validator'+instance (Support r, Support d) => Validator r d (Val r d) where+    validate (Val f) d c = runEvFun f (d, c)++-- | A 'ValFin' is an equivariant orbit-finite predicate on datum and context.  +-- For convenience we make it @'Nameless'@. +newtype ValFin r d = ValFin (EvFinMap (d, Context r d (ValFin r d)) Bool)+    deriving newtype (Generic, Show)+    deriving (Swappable, KRestrict Tom, KSupport Tom) via Nameless (ValFin r d)++instance (UnifyPerm r, UnifyPerm d) => Eq (ValFin r d) where+    ValFin f == ValFin g = f == g  ++deriving via Nameless (ValFin r d) instance (UnifyPerm r, UnifyPerm d) => KUnifyPerm Tom (ValFin r d) -- @ValFin r d@ is assumed nameless++instance (UnifyPerm r, UnifyPerm d) => Validator r d (ValFin r d) where+    validate (ValFin f) d c = f $$ (d, c)  ++++-- * Chunks++{- $chunks+A @'Chunk'@ is a valid list of transactions in a local name-binding context. +Validity is enforced by the constructor @'appendTxChunk'@, which imposes a validity check.++@'Chunk'@, not @'Blockchain'@, is the fundamental abstraction of our development.+A blockchain is just a chunk without any UTxIs (see @'isBlockchain'@ and @'utxisOfChunk'@); conversely a chunk is "like a blockchain, but may have UTxIs as well as UTxOs". ++Chunks have properties that blockchains don't.  For instance: ++* If we slice a chunk up into pieces, we get another chunk. +* A subchunk of a chunk is still a chunk.++In contrast, if we slice up a blockchain, we get chunks, not blockchains. +Thus, blockchains are not naturally compositional and structured in the way that chunks are.++This is a benefit of making the datatype of /chunks/ our primary abstraction.+-}++-- | A @'Chunk'@ is a valid list of transactions in a local name-binding context.  Think of it as a generalisation of blockhains that allows UTxIs (unspent transaction /inputs/). +newtype Chunk r d v = Chunk {chunkToTxList :: Nom [Transaction r d v]}+    deriving (Show, Generic) ++-- equivalent formulation+-- instance (Swappable r, Swappable d, Swappable v) => Swappable (Chunk r d v) where+--   kswp n1 n2 (Chunk p) = Chunk (kswp n1 n2 p)+deriving newtype instance (Swappable r, Swappable d, Swappable v) => Swappable (Chunk r d v)+deriving newtype instance (UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Chunk r d v)+deriving newtype instance (Support r, Support d, Support v) => KSupport Tom (Chunk r d v) -- could also use deriving via BinderSupp, but since Chunk is just a newtype wrapper around a Nom, a deriving newtype seems more direct.+++-- | Acts on a @'Chunk'@ by unpacking it as a transaction-list and a list of locally bound atoms, and applying a function. +instance Validator r d v => Binder (Chunk r d v) [Atom] [Transaction r d v] Tom where +   (@@) :: Chunk r d v -> ([Atom] -> [Transaction r d v] -> b) -> Nom b -- ^ The destructor.  +   (@@) (Chunk nomtxs) = (@@) nomtxs +   resMay :: [Atom] -> [Transaction r d v] -> Maybe (Chunk r d v) -- ^ The constructor.  Because chunks are subject to validation conditions, not every list of transactions is a valid chunk.  Thus, we define 'resMay' instead of '(@>)'. +   resMay = const txListToChunk++-- | Chunk equality tests for equality, with permutative unification on the local names+--+-- @(==) = unifiablePerm@ would be wrong; we should only unify /bound/ atoms.+--+-- Note: @'Ren'@ equality compares nubs (non-identity mappings) +instance (UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Eq (Chunk r d v) where+   ch1 == ch2 = +      ch1 @@. \as1 txs1 ->  -- unpack the local bindings of both chunks+      ch2 @@. \as2 txs2 ->+         idRen == renRemoveBlock (as1 ++ as2) (unifyPerm txs1 txs2) -- unify txs1 with txs2 and make sure all renamings are only on the bound atoms ++-- | A @'transaction'@ is valid if (at least) all positions are disjoint +transactionValid :: Transaction r d v -> Bool+transactionValid (Transaction is os) = allUnique $ inputPositions is ++ outputPositions os++-- | Tries to create a valid @'Chunk'@ from a single @'Transaction'@.  If it fails, we get 'Nothing'.+singletonChunk :: Transaction r d v -> Maybe (Chunk r d v)+singletonChunk tx = toMaybe (transactionValid tx) $ Chunk (return [tx])++-- | Creates a valid @'Chunk'@ from a single @'Transaction'@.+-- If it fails (because the transaction is invalid), it raises and error.+unsafeSingletonChunk :: HasCallStack => Transaction r d v -> Chunk r d v+unsafeSingletonChunk = fromMaybe err . singletonChunk+  where+    err = error "singletonChunk: invalid transaction"++-- | Combine a list of transactions into a @'Chunk'@.  Return @'Nothing'@ if list does not represent a valid chunk.+txListToChunk :: Validator r d v => [Transaction r d v] -> Maybe (Chunk r d v)+txListToChunk = foldMap singletonChunk -- relies on Monoid action on Maybe Chunk +++-- | Combines a list of @'Transaction'@s in a @'Nom'@ binding context, into a @'Chunk'@.+--+-- * Gathers any excess positions (those not linking inputs to outputs) in the @'Nom'@ binding.+-- * Returns @'Nothing'@ if the transaction list doesn't form a valid @'Chunk'@.+nomTxListToNomChunk :: (HasCallStack, Validator r d v) +   => Nom [Transaction r d v] -> Maybe (Nom (Chunk r d v))+nomTxListToNomChunk ntxs = transposeMF $ txListToChunk <$> ntxs  ++-- | Combines a list of transactions in a binding context, into a Chunk, with a check that no excess positions are bound.  Returns Nothing if check fails.+nomTxListToChunk :: (HasCallStack, Validator r d v) +   => Nom [Transaction r d v] -> Maybe (Chunk r d v)+nomTxListToChunk ntxs = do -- Maybe monad+   n <- nomTxListToNomChunk ntxs +   guard (isTrivialNomBySupp n) +   return $ unNom n   ++-- * Examples ++{- $examples++Some example chunks for the reader's convenience and for unit tests.  ++* @exampleCh0@ is the chunk containing a trivial transaction with no inputs and no outputs (and one locally bound name, which is not used). +* @exampleCh1@ is an output with trivial validator.  Wrapped in a Nom binding to store its position.+* @exampleCh2@ is an input.  Wrapped in a Nom binding to store its position.+* @exampleCh12@ is @exampleCh1 <> exampleCh 2@.  Note their positions don't line up.  Also has overbinding! +* @exampleCh21@ is @exampleCh1 <> exampleCh 2@ with positions lined up. +* @exampleCh12'@ is @exampleCh2 <> exampleCh 1@ with positions lined up.  Name-clash: fails.++See 'isChunk' and 'isBlockchain' for unit tests.++-}++-- | Example chunk 0: "Chunk [p] [Transaction [] []]"+--+-- A chunk containing an empty transaction, with a vacuous binding by some @p@.+--+-- Is chunk.  Is blockchain.+--+-- >>> isChunk exampleCh0+-- True+--+-- >>> isBlockchain exampleCh0+-- True+exampleCh0 :: Chunk Int Int (ValTriv Int Int) +exampleCh0 = newA $ \(_p :: Atom) -> fromJust . singletonChunk $ Transaction [] [] ++-- | Example chunk 1: "Chunk [p] [Transaction [] [Output p 0 (const True)]]"+--+-- One output with datum 0 and trivial validator that always returns 'True'.  +--+-- Is chunk.  Is blockchain.+exampleCh1 :: Nom (Chunk Int Int (ValTriv Int Int)) +exampleCh1 = freshAtom <&> \p -> fromJust $ singletonChunk $ Transaction [] [Output p 0 ValTriv] ++-- | Example chunk 2: "Chunk [p] [Transaction [Input p 0] []]"+--+-- One input with redeemer 0.  +--+-- Is chunk.  Is not blockchain.+exampleCh2 :: Nom (Chunk Int Int (ValTriv Int Int)) +exampleCh2 = freshAtom <&> \p -> fromJust $ singletonChunk $ Transaction [Input p 0] [] ++-- | Example chunk obtained by concatenating chunks 1 and 2.  Concat succeeds but positions don't line up.  Is not blockchain, and also is not valid chunk because of overbinding.+--+-- "Chunk [p1, p2] [Transaction [Input p2 0] [], Transaction [] [Output p1 0 (const True)])]"+--+-- (Note: we write lists with their head to the left, so time flows from right to left above.)+--+-- >>> isChunk exampleCh12+-- False+exampleCh12 :: (Chunk Int Int (ValTriv Int Int)) +exampleCh12 = fromJust . unNom $ do -- Nom monad+   ch1 <- exampleCh1+   ch2 <- exampleCh2+   return $ concatChunk ch1 ch2 ++-- | Example chunk obtained by combining chunks 1 and 2, now on same name so input points to output.  +-- +-- "Chunk [p] [Transaction [Input p 0] [], Transaction [] [Output p 0 (const True)])]"+--+-- (Note: we write lists with their head to the left, so time flows from right to left above.)+--+-- Is chunk.  Is blockchain.+exampleCh21 :: (Chunk Int Int (ValTriv Int Int)) +exampleCh21 = fromJust . unNom $ do -- Nom monad+   ch1 <- exampleCh1+   ch2 <- exampleCh2+   let [a] = S.toList $ supp ch1 +   let [b] = S.toList $ supp ch2 +   return $ concatChunk ch2 (swp a b ch1) ++-- | Example chunk obtained by combining chunks 1 and 2, on same name.  But output comes /after/ input, not before.  Concat fails because nameclash is detected.+exampleCh12' :: Maybe (Chunk Int Int (ValTriv Int Int)) +exampleCh12' = unNom $ do -- Nom monad+   ch1 <- exampleCh1+   ch2 <- exampleCh2+   let [a] = S.toList $ supp ch1 +   let [b] = S.toList $ supp ch2 +   return $ concatChunk ch1 (swp a b ch2) ++-- * Combining and extending chunks++-- | Calculate the input and output positions+positionsOfTxs :: [Transaction r d v] -> ([Position], [Position])+positionsOfTxs txs = (inputPositions txs, outputPositions txs) + +-- | @'appendTxChunk' tx txs@ adds @tx@ to @txs@, provided that:+--+-- * @tx@ is valid+-- * there is no position name-clash and +-- * validators are happy.+--+-- This is the core of this file.  In a certain sense, everything is just different ways of wiring into this function.+appendTxChunk :: (HasCallStack, Validator r d v) => Transaction r d v -> Chunk r d v -> Maybe (Chunk r d v)  +appendTxChunk tx ch = ch @@. \_ txs -> -- use of '@@.' here ensures that any atoms bound in ch stay bound in result.  However, the extra atoms in bn below, get added to binding.+   let (txIns,  txOuts ) = positionsOfTxs [tx] +       (txsIns, txsOuts) = positionsOfTxs txs+       bn = intersect txIns txsOuts -- the inputs of @tx@ that point to outputs in @txs@ and so should get bound+   in+   toMaybe +      (   transactionValid tx     -- tx is valid +       && disjoint txOuts txsOuts -- no outputs in tx clash with outputs in txs+       && disjoint txOuts txsIns  -- no outputs in tx clash with inputs in txs+       && disjoint txIns  txsIns  -- no inputs in tx clash with inputs in txs+       && all validate' bn)       -- all validators happy with context   +      (Chunk $ bn @> tx : txs)    -- all OK?  then push tx + where+   validate' :: Position -> Bool+   validate' pos =+      let Transaction ins outs = tx+          utxos                = utxosOfChunk ch +          Output _ datum v     = iota (\(Output p _ _) -> p == pos) utxos+          context              = Transaction (atomPoint pos ins) outs+      in  validate v datum context++-- | Version of @'appendTxChunk'@ that acts directly on @Maybe (Chunk r d v)@.+appendTxMaybeChunk :: Validator r d v => Transaction r d v -> Maybe (Chunk r d v) -> Maybe (Chunk r d v)+appendTxMaybeChunk = (=<<) . appendTxChunk + +-- | Restrict atoms in a 'Chunk'.+instance (Swappable r, Swappable d, Swappable v) => KRestrict Tom (Chunk r d v) where +   restrict atms (Chunk x) = Chunk $ restrict atms x -- Relies on restrict being monadic on Maybe+++-- | Concatenate two @'Chunk'@s, merging their binding contexts in a capture-avoiding manner.+-- If concatenation is impossible (e.g. because validation fails), defaults to @Chunk Nothing@.+--+-- __Note:__ No explicit checks are made here that inputs are valid chunks.  In particular, no overbinding protection (overbinding = Nom binder in Chunk binds excess positions not involved in UTxO-UTxI linkage).  If you want such checks, look at 'isChunk' and 'isBlockchain'.+--+-- Works by unpacking first chunk as a list of transactions and appending them to 'Just' the second argument.  Local binding of first chunk gets carried over automatically; new local bindings may get generated during the append.+concatChunk :: Validator r d v => Chunk r d v -> Chunk r d v -> Maybe (Chunk r d v)+concatChunk ch1 ch2 = resAppC (foldr appendTxMaybeChunk (Just ch2)) ch1 +++-- | A version of 'concatChunk' that performs explicit validity checks on its inputs and result. +safeConcatChunk :: Validator r d v => Chunk r d v -> Chunk r d v -> Maybe (Chunk r d v)+safeConcatChunk ch1 ch2 = +   guard (isChunk ch1 && isChunk ch2 && isJust (concatChunk ch1 ch2)) +   >> (concatChunk ch1 ch2) ++-------------------------------------+----- Algebraic properties of Chunk and Maybe Chunk+++instance Validator r d v => PartialSemigroup (Chunk r d v) where+   padd = concatChunk++-- | Chunk forms a partial monoid+instance Validator r d v => PartialMonoid (Chunk r d v) where+   pzero = Chunk $ return []+++instance Validator r d v => Semigroup (Maybe (Chunk r d v)) where+   mch <> mch' = do -- Maybe monad+      ch  <- mch+      ch' <- mch'+      concatChunk ch ch'++-- | Maybe Chunk forms a monoid, with unit being the empty chunk.+instance Validator r d v => Monoid (Maybe (Chunk r d v)) where+   mempty  = Just . Chunk . return $ []+   mappend = (<>)+-- TODO: why no overlapping instance error messages with rule from Data.Monoid?++++-- * Splitting chunks up ++-- | For debugging+genUnNomChunk :: Validator r d v => Chunk r d v -> Chunk r d v+genUnNomChunk = genAppC $ Chunk . return ++-- | Check whether one chunk is a prefix of another.  See @'chunkTail'@ to understand why the @'Nom'@ binding on the first argument is required.+isPrefixChunk :: (UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Nom (Chunk r d v) -> Chunk r d v -> Bool  +isPrefixChunk ch1' ch2 =     +   ch1' @@. \as  ch1  ->   -- as = local names in putative prefix +   ch1  @@. \as1 txs1 ->  +   ch2  @@. \as2 txs2 -> +      case evPrefixRen txs1 txs2 of +         Ren Nothing -> False +         r           -> supp r `S.isSubsetOf` S.fromList (as ++ as1 ++ as2) +++-- | Calculate the length of a Chunk+chunkLength :: Validator r d v => Chunk r d v -> Int +chunkLength = resAppC L.length +++-- | Calculate the head of a chunk.  +chunkHead :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Nom (Transaction r d v))+chunkHead ch = transposeMF $ nomAppC safeHead ch +++-- | Calculate the tail of a chunk.  Two monads here:+--+-- * @'Maybe'@, because the underlying list of transactions might be empty and so have no tail.  And if it's not empty ...+--+-- * @'Nom'@ ... to bind the names of any positions in newly-exposed UTxOs.+chunkTail :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Nom (Chunk r d v))+chunkTail ch = transposeMF $ nomAppC ((=<<) txListToChunk . safeTail) ch +-- chunkTail ch = transposeMF $ nomAppC (\txs -> safeTail txs >>= txListToChunk) ch +++-- | Compare the code for this function with the code for @'chunkTail'@.  +-- It looks plausible ... but it's wrong.+--+-- It looks like it returns the tail of a chunk, and indeed it does.  However, the result is not a chunk because positions get exposed. +--+-- See the test 'Language.Nominal.Properties.Examples.IdealisedEUTxOSpec.prop_warningNotChunkTail_is_not_chunk'.+warningNotChunkTail :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v)+warningNotChunkTail = genAppC $ \txs -> (Chunk . return) <$> safeTail txs +{-- warningNotChunkTail ch = ch @@. \_ txs -> case txs of+    []         -> Nothing+    (_ : txs') -> Just $ Chunk $ return txs'  --}+++-- | @'take'@, for chunks.  The @'Nom'@ binding captures any dangling UTxOs or UTxIs that are left after truncating the chunk. +chunkTakeEnd :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Int -> Chunk r d v -> Nom (Chunk r d v)+chunkTakeEnd i ch = fromJust . nomTxListToNomChunk $ takeEnd i <$> chunkToTxList ch +++-- | List of subchunks.  @'Nom'@ binding is to capture dangling UTxOs or UTxIs.+subTxListOf :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Nom [[Transaction r d v]] +subTxListOf = nomAppC subsequences +++-- | Take a chunk and reverse its transactions.  Usually this will result in an invalid chunk, in which case we get @Nothing@.  +-- Used for testing. +reverseTxsOf :: (UnifyPerm r, UnifyPerm d, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v) +reverseTxsOf = nomTxListToChunk . nomAppC L.reverse ++-- | Split a chunk into a head and a tail.+chunkToHdTl :: Validator r d v => Chunk r d v -> Maybe (Nom (Transaction r d v, Chunk r d v))+chunkToHdTl (Chunk x') = transposeMF $ x' @@ \_ x -> case x of+   (tx:txs) -> return (tx, fromJust $ txListToChunk txs)+   []       -> Nothing++-- | Split a chunk into a head and a head and a tail.+chunkToHdHdTl :: Validator r d v => Chunk r d v -> Maybe (Nom (Transaction r d v, Transaction r d v, Chunk r d v))+chunkToHdHdTl (Chunk x') = transposeMF $ x' @@ \_ x -> case x of+   (tx1:tx2:txs) -> return (tx1, tx2, fromJust $ txListToChunk txs)+   _             -> Nothing+++-- * Blockchain ++-- | A blockchain is a /valid/ @'Chunk'@, with no unspent inputs.+newtype Blockchain r d v = Blockchain {getBlockchain :: Chunk r d v}+    deriving (Show, Generic)++instance (Swappable r, Swappable d, Swappable v) => Swappable (Blockchain r d v) +instance (Support r, Support d, Support v) => KSupport Tom (Blockchain r d v) +instance (UnifyPerm r, UnifyPerm d, UnifyPerm v) => KUnifyPerm Tom (Blockchain r d v) ++-- | Smart constructor for a @'Blockchain'@. +-- Ensures only valid blockchains are constructed, by testing for @'isBlockchain'@.+blockchain :: (HasCallStack, Validator r d v) => Chunk r d v -> Blockchain r d v  +blockchain c+    | isBlockchain c = Blockchain c+    | otherwise      = error ("blockchain: invalid chunk or dangling inputs") +++-- * Is Chunk / Blockchain check ++-- | Check that the correct atoms are bound in a 'Chunk'.+chunkBindingOK :: Validator r d v => Chunk r d v -> Bool +chunkBindingOK = resApp $ \ps txs -> let (ips, ops) = positionsOfTxs txs in +   ps `intersect` (ips ++ ops) == ips `intersect` ops ++-- | Check that validators are happy, by taking a 'Chunk' apart and putting it together again.+chunkValidatorsOK :: Validator r d v => Chunk r d v -> Bool +chunkValidatorsOK = resAppC $ isJust . txListToChunk   -- take it apart and put it together with transaction validation ++-- | Is this a valid chunk?  ('exampleCh1', 'exampleCh2', 'exampleCh12', 'exampleCh21') +--+-- >>> resAppC isChunk exampleCh1+-- True +--+-- >>> resAppC isChunk exampleCh2+-- True +--+-- >>> isChunk exampleCh12+-- False+--+-- >>> isChunk exampleCh21+-- True+isChunk :: Validator r d v => Chunk r d v -> Bool +isChunk ch = chunkBindingOK ch && chunkValidatorsOK ch ++-- | Is this a valid chunk?  Test by splitting it into a transaction list and putting it back together again. +--+isChunk' :: (Validator r d v, UnifyPerm r, UnifyPerm d, UnifyPerm v) => Chunk r d v -> Bool +isChunk' ch = Just ch == genAppC txListToChunk (chunkToTxList ch) ++-- | A blockchain is a valid 'Chunk' with no UTxI (unspent transaction /inputs/).  ('exampleCh1', 'exampleCh2', 'exampleCh12', 'exampleCh21') +--+-- >>> isBlockchain exampleCh0+-- True+--+-- >>> resAppC isBlockchain exampleCh1+-- True+--+-- >>> resAppC isBlockchain exampleCh2+-- False +--+-- >>> isBlockchain exampleCh12+-- False +--+-- >>> isBlockchain exampleCh21+-- True +isBlockchain :: Validator r d v => Chunk r d v -> Bool+isBlockchain ch = (L.null . utxisOfChunk) ch  -- no dangling inputs+               && isChunk ch                  -- is a valid chunk (e.g. no overbinding) +++-- | Blockchain check for 'Maybe' a 'Chunk'.+isBlockchain' :: Validator r d v => Maybe (Chunk r d v) -> Bool+isBlockchain' mch = (isBlockchain <$> mch) == Just True+++++-- * Intensional equality of 'Chunk' ++{- $intension+Modelled on <https://web.archive.org/web/20200405185005/https://mail.haskell.org/pipermail/haskell-cafe/2004-December/007766.html a post by Oleg Kiselyov>+An intensional equality allows us to compare 'Chunk's for equality of UTxOs, even if the type of validators does not have an 'Eq' instance.++We don't do this at the moment (we use 'ValFin' instead), but we still provide the facility in case it is useful for a user running e.g. QuickCheck tests where we care that structure gets put in the right place and assembled in the right ways, without caring too much about executing that structure for values of specific interest. +-}++class IEq a where+    iEq :: a -> a -> IO Bool  +    default iEq :: Eq a => a -> a -> IO Bool+    iEq x y = return $ x == y ++instance IEq (a -> b) where+   iEq f g = do -- IO monad     +      pf <- newStablePtr f  -- fetch pointer to f+      pg <- newStablePtr g  -- and to f'+      let result = pf == pg -- equal?+      freeStablePtr pf      -- free the pointers+      freeStablePtr pg+      return result++instance IEq a => IEq [a] where+   iEq la la' = and <$> zipWithM iEq la la'++deriving newtype instance IEq (KEvFun k a b)+deriving anyclass instance Eq r => IEq (Input r)++-- | Equality on validators is intensional; (Validator f == Validator f') when f and f' happen to point to the same bit of memory when the equality runs. +-- Thus if iEq f f' returns True this means that f and f' represent the same mathematical function, and indeed are also the same code.+-- If iEq f f' returns False this does not mean that f and f' represent distinct mathematical functions.+-- It just means they were represented by distinct code when iEq is called.  +-- This may be useful for running tests where we check that gobs of code get put in the right places and assembled in the right ways, without necessarily caring to execute them (or even without necessarily instantiating executable values). +-- instance IEq Value where+instance (Eq d, IEq v) => IEq (Output d v) where+   iEq (Output p d vd) (Output p' d' vd') = do -- IO monad+      eqvd <- iEq vd vd'  -- check everything is intensionally equal+      return $ p == p' && eqvd && d == d'++-- | Intensional equality +equivChunk :: (Eq r, Eq d, IEq v, Validator r d v) => Chunk r d v -> Chunk r d v -> IO Bool+equivChunk txlist1 txlist2 = and <$> sequence +   [ utxosOfChunk txlist1 `iEq` utxosOfChunk txlist2 +   , utxisOfChunk txlist1 `iEq` utxisOfChunk txlist2+   ]+++-- * Generics support for @'HasInputPositions'@++class GHasInputPositions f where+    gInputPositions :: f x -> [Position]++instance GHasInputPositions V1 where+    gInputPositions = \case {}  -- uses EmptyCase and LambdaCase.  Avoids hlint parse issue. + +instance GHasInputPositions U1 where+    gInputPositions U1 = []++instance HasInputPositions c => GHasInputPositions (K1 i c) where+    gInputPositions = inputPositions . unK1++instance (GHasInputPositions f, GHasInputPositions g) => GHasInputPositions (f :*: g) where+    gInputPositions (x :*: y) = gInputPositions x ++ gInputPositions y++instance (GHasInputPositions f, GHasInputPositions g) => GHasInputPositions (f :+: g) where+    gInputPositions (L1 x) = gInputPositions x+    gInputPositions (R1 y) = gInputPositions y++instance GHasInputPositions f => GHasInputPositions (M1 i c f) where+    gInputPositions = gInputPositions . unM1++-- * Generics support for @'HasOutputPositions'@++class GHasOutputPositions f where+    gOutputPositions :: f x -> [Position]++instance GHasOutputPositions V1 where+    gOutputPositions = \case {}  -- uses EmptyCase and LambdaCase.  Avoids hlint parse issue. +++instance GHasOutputPositions U1 where+    gOutputPositions U1 = []++instance HasOutputPositions c => GHasOutputPositions (K1 i c) where+    gOutputPositions = outputPositions . unK1++instance (GHasOutputPositions f, GHasOutputPositions g) => GHasOutputPositions (f :*: g) where+    gOutputPositions (x :*: y) = gOutputPositions x ++ gOutputPositions y++instance (GHasOutputPositions f, GHasOutputPositions g) => GHasOutputPositions (f :+: g) where+    gOutputPositions (L1 x) = gOutputPositions x+    gOutputPositions (R1 y) = gOutputPositions y++instance GHasOutputPositions f => GHasOutputPositions (M1 i c f) where+    gOutputPositions = gOutputPositions . unM1++{- $tests Property-based tests are in "Language.Nominal.Properties.Examples.IdealisedEUTxOSpec". -}
+ src/Language/Nominal/Examples/Style.hs view
@@ -0,0 +1,134 @@+{-|+Module      : Comments on style+Description : Examples of coding style+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Commented examples of coding style.  (Or: ways to abuse this code.) ++-}++{-# LANGUAGE InstanceSigs+           , DeriveGeneric+           , LambdaCase+           , MultiParamTypeClasses+           , DeriveAnyClass       -- to derive 'Swappable'+           , DeriveDataTypeable   -- to derive 'Data'+           , FlexibleInstances+#-}+++module Language.Nominal.Examples.Style+    ( +     -- $intro+     bad_countBinding, bad_countOrder, badRestrict, okRestrict, badEq+    )+    where++-- import Data.Function    ((&))++import Language.Nominal.Name+import Language.Nominal.Nom+import Language.Nominal.Binder++{- $intro+It's tempting to try to provide static guarantees of good behaviour with respect to name-handling.+However, this is expensive and may be impossible: sometimes what makes code good or bad depends on how the output is used.++For example: a substitution of a term for a bound name may involve generating a fresh identifier for that name.+This is reasonable, because we expect the choice of name to be destroyed by the substitution.+We can rewrite the code to avoid this name-generation, at some expense, and arguably this stilts the coding style, but either way it is not clear how a type system can provide a comprehensive answer.++Here, we give examples of programs (that may even still work, but) are arguably ugly. +So: this file is devoted to some programs that you might think twice about writing.+ +-}++-- | You probably shouldn't count the atoms bound in a 'Nom'.   +--+-- > bad_countBinding :: Swappable a => Nom a -> Int+-- > bad_countBinding x' = x' @@! \atms _ -> length atms+bad_countBinding :: Swappable a => Nom a -> Int+bad_countBinding x' = x' @@! \atms _ -> length atms++-- | You probably shouldn't look at the order of the atoms bound in a 'Nom'.+--+-- > bad_countOrder :: Swappable a => Nom a -> Bool+-- > bad_countOrder x' = x' @@! \atms _ -> isSorted atms+bad_countOrder :: Swappable a => Nom a -> Bool+bad_countOrder x' = x' @@! \atms _ -> isSorted atms++-- | It's OK to create fresh IDs for bound atoms, but doing so /unnecessarily/ is deprecated.+--+-- For example, here is code for a restrict instance of Nom (code simplified for clarity):+--+-- > restrict :: Swappable a => [Atom] -> Nom a -> Nom a+-- > restrict atms x' = x' >>= \x -> res atms x+--+-- We can simplify it down to this:+--+-- > restrict = (=<<) . res +--+-- The code for 'badRestrict' below does the same thing, but unnecessarily unpacks the local binding, generates fresh IDs for its atoms, and then rebinds.+--+-- > badRestrict :: Swappable a => [Atom] -> Nom a -> Nom a+-- > badRestrict atms' a' = a' @@! \atms a -> res (atms' ++ atms) a+badRestrict :: Swappable a => [Atom] -> Nom a -> Nom a+badRestrict atms' a' = a' @@! \atms a -> res (atms' ++ atms) a++-- | Contrast 'badRestrict' with the similar 'okRestrict'.  What separates them is the use of '(@@!)' instead of '(@@.)' (respectively).  +-- The latter '(@@.)' avoids an intermediate generation of explicit fresh IDs for the bound atoms, and so is better.+--+-- In fact 'okRestrict' is equivalent to the actual 'restrict' instance; it's just expressed using higher-level tools.+--+-- > okRestrict :: Swappable a => [Atom] -> Nom a -> Nom a+-- > okRestrict atms a' = a' @@. \_ -> res atms+--+-- Also OK:+--+-- > okRestrict' atms' = join . fmap (res atms')+okRestrict :: Swappable a => [Atom] -> Nom a -> Nom a+okRestrict atms a' = a' @@. \_ -> res atms+++-- | Still on the theme of trying to be parsimonious with generating atoms here is code for an equality instance of 'KNom':+-- +-- > instance Eq a => Eq (KNom s a) where+-- >    a1' == a2' = exit $ a1' >>= \a1 -> a2' >>= \a2 -> return $ a1 == a2+--+-- Note how we 'exit' at 'Bool'.+-- Contrast with the deprecated version, in which we exit earlier than required, and furthermore, we exit twice (code simplified for clarity):+--+-- > badEq :: Eq a => Nom a -> Nom a -> Bool+-- > badEq a1' a2' = withExit a1' $ \_ a1 -> withExit a2' $ \_ a2 -> a1 == a2+badEq :: Eq a => Nom a -> Nom a -> Bool+badEq a1' a2' = withExit a1' $ \_ a1 -> withExit a2' $ \_ a2 -> a1 == a2++++++++-- from Data.List.Ordered++-- |  The 'isSorted' predicate returns 'True' if the elements of a list occur+-- in non-descending order,  equivalent to @'isSortedBy' ('<=')@.+isSorted :: Ord a => [a] -> Bool+isSorted = isSortedBy (<=)++-- |  The 'isSortedBy' function returns 'True' iff the predicate returns true+-- for all adjacent pairs of elements in the list.+isSortedBy :: (a -> a -> Bool) -> [a] -> Bool+isSortedBy lte = loop+  where+    loop []       = True+    loop [_]      = True+    loop (x:y:zs) = (x `lte` y) && loop (y:zs)++{-- TODO: ksupp p x' = unNom $ ksupp p <$> x'+   -- ksupp p x' = withExit x' $ \atms x -> restrict atms (ksupp p x)+--}
+ src/Language/Nominal/Examples/SystemF.hs view
@@ -0,0 +1,396 @@+{-|+Module      : System F +Description : Syntax and reductions of System F using the Nominal package+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Syntax and reductions of System F using the Nominal package+-}++{-# LANGUAGE DataKinds             +           , InstanceSigs          +           , DeriveAnyClass        +           , DeriveGeneric         +           , MultiParamTypeClasses +           , FlexibleInstances     +           , LambdaCase            +           -- , PolyKinds             +           , DefaultSignatures     +           , DeriveAnyClass        +           , DeriveDataTypeable+           , DeriveGeneric         +           , EmptyCase             +           , FlexibleInstances     +           , FlexibleContexts       -- so we can write `Swappable d`+           , InstanceSigs          +           , LambdaCase            +           , MultiParamTypeClasses +           , StandaloneDeriving    +           , TypeOperators         +           , UndecidableInstances  +#-}+++module Language.Nominal.Examples.SystemF +    ( +-- * Introduction+-- $intro+    ATrm, ATyp,+-- * System F types +    NTypLabel, NTyp, Typ (..), typRecurse,+-- * System F terms+    NTrmLabel, NTrm, Trm (..), typeOf, typeOf', typeable,  +-- * Normal forms+    nf, nf', normalisable,+-- * Pretty-printer+    PP (..),  +-- * Helper functions for building terms +    tall, tlam, lam, (@.), (@:),+-- * Example terms+    idTrm, idTrm2, zero, suc, one, nat, church, transform, selfapp+-- * Tests+-- $tests+    )+    where++import Data.Generics              hiding (Generic, typeOf)+import Data.Maybe+import GHC.Generics+import Control.Monad              (guard)++import Language.Nominal.Utilities +import Language.Nominal.Name +import Language.Nominal.Binder+import Language.Nominal.Abs +import Language.Nominal.Sub ++{- $intro++System F is a classic example and has some interesting features:++* Two kinds of variable: /type variables/ and /term variables/.+* Three kinds of binding: /type forall/ binding a type variable in a type; /term lambda/ binding a term variable in a term; and /type lambda/ binding a type variable in a term.+* A static assignment of semantic information to term variables, namely: a /type assignment/.  Thus intuitively term variables carry labels (types), which themselves may contain type variables.+* And it's an expressive system of independent mathematical interest.++So implementing System F is a natural test for this package.+We start with atoms:+ +-}++-- | With @DataKinds@, we obtain:+--+-- * @ATyp@ a type of atoms to identify type variables @'NTyp'@, and+-- * @ATrm@ a type of atoms to identify term variables @'NTrm'@.+--+-- See 'Language.Nominal.Name.Tom' for more discussion of how this works.+data ATyp +   deriving (Data)+-- | With @DataKinds@, we obtain:+--+-- * @ATyp@ a type of atoms to identify type variables @'NTyp'@, and+-- * @ATrm@ a type of atoms to identify term variables @'NTrm'@.+--+-- See 'Language.Nominal.Name.Tom' for more discussion of how this works.+data ATrm +   deriving (Data)++-- * System F types ++-- | A type variable is labelled just by a display name+type NTypLabel = String +-- | A type variable name.  Internally, this consists of+--+-- * an atom of type @KAtom ATyp@, and+-- * a label of type @'NTypLabel'@, which is just a display name in @'String'@. +type NTyp = KName ATyp NTypLabel++-- | Datatype of System F types +--+-- We use @Generic@ to deduce a swapping action for atoms of sorts @'ATyp'@ and @'ATrm'@. +-- Just once, we spell out the definition implicit in the generic instance:  +--+-- > instance Swappable Typ where+-- >    swpN n1 n2 (TVar n)   = TVar $ swpN n1 n2 n+-- >    swpN n1 n2 (t' :-> t) = swpN n1 n2 t' :-> swpN n1 n2 t+-- >    swpN n1 n2 (All x)    = All $ swpN n1 n2 x+--+-- This is boring, and automated, and that's the point: swappings distribute uniformly through everything including abstractors (the @x@ under the @All@).  +--+-- (The mathematical reason for this is that swappings are invertible, whereas renamings and substitutions aren't.)+--+data Typ = +   TVar NTyp           -- ^ Type variable+ | Typ :-> Typ         -- ^ Type application+ | All (KAbs NTyp Typ) -- ^ Type forall-abstraction+ deriving (Eq, Generic, Swappable, Typeable, Data)+ +-- | Substitution acts on type variables.  Capture-avoidance is automagical.+instance KSub NTyp Typ Typ where+    sub :: NTyp -> Typ -> Typ -> Typ +    sub a t = rewrite $ \case -- 'rewrite' comes from Scrap-Your-Boilerplate generics.  +        TVar n | n == a -> Just t  -- note name-equality is atom-wise and ignores labels +        _               -> Nothing ++-- | Nominal recursion scheme.  We never use it because it's implicit in pattern-matching.  See e.g. code for 'typeOf', 'nf', and 'ppp'. +typRecurse :: (NTyp -> a) -> (Typ -> Typ -> a) -> (NTyp -> Typ -> a) -> Typ -> a +typRecurse f1 _ _ (TVar n)    = f1 n+typRecurse _ f2 _ (s1 :-> s2) = f2 s1 s2+typRecurse _ _ f3 (All x')    = x' @@! f3 +++------------------------------------+-- * System F terms+++-- | A term variable is labelled by a display name, and its type+type NTrmLabel = ( String -- Display name of term variable+                 , Typ    -- Type of the term variable+                 )+-- | A term variable name +type NTrm = KName ATrm NTrmLabel++-- | Substitute type variables with type in term variable.  +-- Non-trivial because a term variable carries a label which contains a type.  +-- Action is functorial, descending into the type label. +instance KSub NTyp Typ NTrm where+   sub a ty' (Name lab atm) = Name (sub a ty' lab) atm++-- | System F terms.  +--+-- * We get swapping actions automatically, and also substitution of type names @NTyp@ for types @Typ@.  +-- * Substitution of term variables @NTrm@ for terms @Trm@ needs defined separately. +--+data Trm =  Var NTrm             -- ^ Term variable, labelled by its display name and type +          | App Trm Trm          -- ^ Apply a term to a term  +          | Lam (KAbs NTrm Trm)  -- ^ Nominal atoms-abstraction by a term variable. +          | TApp Trm Typ         -- ^ Apply a term to a type+          | TLam (KAbs NTyp Trm) -- ^ Nominal atoms-abstraction by a type variable.   +  deriving ( Eq+           , Generic+           , Swappable          --- swappings derived automatically+           , KSub NTyp Typ      --- substitution of type names for types derived automatically+           , Typeable+           , Data+           )++-- | Substitute term variable with term in term+instance KSub NTrm Trm Trm where+   sub :: NTrm -> Trm -> Trm -> Trm +   sub a t = rewrite $ \case          -- 'rewrite' comes from Scrap-Your-Boilerplate generics.  +        Var n | n == a -> Just t  -- note name-equality is atom-wise and ignores labels +        _              -> Nothing +{--        Var n -> toMaybe (a == n) t  -- note name-equality is atom-wise and ignores labels +        _     -> Nothing --}++-- | Calculate type of term, maybe+typeOf :: Trm -> Maybe Typ +typeOf (Var n)     = let (_, t) = nameLabel n in Just t+typeOf (TLam (tp :@> tm)) = do -- Maybe monad+   typetm <- typeOf tm +   return $ All (tp :@> typetm) +typeOf (Lam (n :@> tm)) = do -- Maybe monad+   typetm <- typeOf tm+   let (_, t) = nameLabel n+   return $ t :-> typetm +typeOf (App s1 s2) = do -- Maybe monad +   t1a :-> t1b    <- typeOf s1+   t2             <- typeOf s2 +   guard (t1a == t2) +   return t1b +typeOf (TApp s t)  = do -- Maybe monad+   All x' <- typeOf s+   return $ x' `conc` t -- substitution of type name for type, in type ++-- | Calculate type of term; raise error if none exists+typeOf' :: Trm -> Typ+typeOf' s = fromMaybe (error ("Type error" ++ ppp s)) (typeOf s) ++-- | @'True'@ if term is typeable; @'False'@ if not. +typeable :: Trm -> Bool+typeable = isJust . typeOf +++-- * Normal forms++-- | Normal form, maybe +nf :: Trm -> Maybe Trm  +nf s = guard (typeable s) >> return (repeatedly nf_ s)+   where -- behaviour on untypeable terms is undefined+   nf_ :: Trm -> Trm+   nf_ = rewrite $ \case -- 'rewrite' comes from Scrap-Your-Boilerplate generics.  ++            TApp (TLam x') t2 -> return . nf_ $ x' `conc` t2+            App  (Lam x')  s2 -> return . nf_ $ x' `conc` (nf_ s2)+            _                 -> Nothing++-- | Normal form; raise error if none+nf' :: Trm -> Trm +nf' s = fromMaybe (error ("Type error: " ++ ppp s)) (nf s) ++-- | True if term is normalisable; false if not. +normalisable :: Trm -> Bool+normalisable = isJust . nf  ++++{---------------------------------------------+-- Semantics ++data Sem = SemLam Typ (Sem -> Sem) | SemTLam (Typ -> Sem) ++-- We get sub automagically+type TypeVarContext = Name NTypLabel -> Typ+type TermVarContext = Name NTrmLabel -> Sem ++sem :: TypeVarContext -> TermVarContext -> Trm -> Maybe Sem+sem tyc tmc (Var n)      = Just $ tmc n       -- ^ Look up in the var context+sem tyc tmc (App s1 s2)  = do -- Maybe monad+   SemLam t f <- sem tyc tmc s1 +   f <$> (sem tyc tmc s2)+sem tyc tmc (Lam x)      = x @@! \n s -> do -- Maybe monad+   (_, nty) <- nameLabel n+   return $ SemLam nty (\x -> sem tyc (sub n x tmc) s)+sem tyc tmc (TApp s1 t2) = do -- Maybe monad+   SemTLam f <- sem tyc tmc s1 +   return $ f t2+sem tyc tmc (TLam x)     = x @@! \n s -> SemTLam (\x -> sem (sub n x tyc) tmc s)++-- A useful property would be that sem (t t') = sem t (sem t')+--}++---------------------------------------------+-- * Pretty-printer++-- | Typeclass for things that can be pretty-printed+class PP a where+   ppp :: a -> String+   pp  :: a -> IO ()+   pp = putStrLn . ppp ++-- | Pretty-print type variable +instance PP NTyp where+   ppp n = (nameLabel n) ++ "(" ++ show (nameAtom n) ++ ")" ++-- | Pretty-print type +instance PP Typ where+  ppp (TVar n)  = ppp n+  ppp (All (n :@> t)) = '∀':(ppp n ++ "." ++ ppp t)+  ppp (t :-> u) = pppL t ++ " -> " ++ pppR u where+    pppL (All _)      = "(" ++ ppp t ++ ")"+    pppL (_ :-> _)    = "(" ++ ppp t ++ ")"+    pppL _            = ppp t+    pppR (All _)      = "(" ++ ppp u ++ ")"+    pppR _            = ppp u++-- | Pretty-print term variable +instance PP NTrm where+   ppp n = (\(s, t) -> s ++ ":" ++ ppp t) (nameLabel n) ++ "(" ++ show (nameAtom n) ++ ")" ++-- Forall ∀+-- Capital Lambda Λ = \0923+-- lambda λ = \0955+-- | Pretty-print term +instance PP Trm where+   ppp (Lam (n :@> t))      = "λ" ++ pppN n ++ pppB t where+      pppB (Lam (n' :@> t')) = "," ++ " " ++ pppN n' ++ pppB t' +      pppB expr     = '.':ppp expr+      pppN n'       = let (s', t') = nameLabel n' in (s' ++ ":" ++ ppp t')+   ppp (TLam (n :@> t))     = "Λ" ++ ppp n ++ pppB t where+      pppB (TLam (n' :@> t')) = " " ++ ppp n' ++ pppB t'+      pppB expr     = '.':ppp expr+   ppp (Var s)      = ppp s+   ppp (App x y)    = pppL x ++ pppR y where+      pppL (Lam _)  = "(" ++ ppp x ++ ")"+      pppL _        = ppp x+      pppR (Var s)  = ' ':ppp s+      pppR _        = "(" ++ ppp y ++ ")"+   ppp (TApp x y)   = pppL x ++ "[" ++ ppp y ++ "]" where+      pppL (Lam _)  = "(" ++ ppp x ++ ")"+      pppL _        = ppp x+--  ppp (Let x y z) =+--    "let " ++ x ++ " = " ++ ppp y ++ " in " ++ ppp z+++instance {-# OVERLAPS #-} Show Trm where+   show = ppp+instance {-# OVERLAPS #-} Show (Maybe Trm) where+   show = maybe "No term!" ppp++instance {-# OVERLAPS #-} Show Typ where+   show = ppp+instance {-# OVERLAPS #-} Show (Maybe Typ) where+   show = maybe "No type!" ppp++++-- * Helper functions for building terms ++-- | Build type quantification from function: f ↦ ∀ a.(f a) for fresh a+tall :: NTypLabel -> (Typ -> Typ) -> Typ +tall s f = All $ absFresh s (f . TVar)++-- | Build type lambda from function: f ↦ Λ a.(f a) for fresh a+tlam :: NTypLabel -> (Typ -> Trm) -> Trm+tlam s f = TLam $ absFresh s (f . TVar)++-- | Build term lambda from function: f ↦ λ a.(f a) for fresh a+lam :: NTrmLabel -> (Trm -> Trm) -> Trm+lam (s,ty) f = Lam $ absFresh (s, ty) (f . Var)++-- | Term-to-term application+(@.) :: Trm -> Trm -> Trm+s1 @. s2   = App s1 s2++-- | Term-to-type application+(@:) :: Trm -> Typ -> Trm+s1 @: t2  = TApp s1 t2+++-- * Example terms++-- | polymorphic identity term = λX x:X.x+idTrm :: Trm+idTrm = TLam $ absFresh "X" (\xx -> Lam $ absFresh ("x", TVar xx) (\x -> Var x))+-- | Another rendering of polymorphic identity term+idTrm2 :: Trm+idTrm2 = tlam "X" $ \xx -> lam ("x", xx) $ \x -> x -- hlint complains about \x -> x.  retained for clarity++-- | 0 = λX λs:X->X λz:X.z+zero :: Trm+zero = tlam "X" $ \xx -> lam ("s", xx :-> xx) $ \_s -> lam ("z", xx) $ \z -> z  -- hlint complains about \x -> x.  retained for clarity+++-- | suc = λx:(∀X.(X->X)->X->X) X s:X->X z:X.s(n[X] s z)+suc :: Trm+suc = lam ("n",nat) $ \n -> +      tlam "X" $ \xx -> +      lam ("s", xx :-> xx) $ \s -> +      lam ("z", xx) $ \z -> +         s @. (((n @: xx) @. s) @. z)++-- | 1+one :: Trm+one = nf' (suc @. zero)++-- | nat+nat :: Typ+nat = tall "X" $ \xx -> (xx :-> xx) :-> (xx :-> xx) ++-- | Cast an Int to the corresponding Church numeral.+church :: Int -> Trm+church 0 = zero+church i = suc @. church (i-1)++-- | Transformer type = ∀X.X->X+transform :: Typ+transform = tall "X" $ \xx -> xx :-> xx ++-- | Self-application = λx:∀X.X->X.x[∀X.X->X] x+selfapp :: Trm+selfapp = lam ("x", transform) $ \x -> (x @: transform) @. x  ++{- $tests Property-based tests are in "Language.Nominal.Properties.Examples.SystemFSpec". -}
+ src/Language/Nominal/Examples/Tutorial.hs view
@@ -0,0 +1,415 @@+{-|+Module      : Tutorial +Description : Name-binding for dummies: tutorial on use of nominal package +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++= Name-binding for dummies: tutorial on use of nominal package  ++-}++{-# LANGUAGE CPP                   +           , FlexibleInstances     +           , InstanceSigs          +           , LambdaCase            +           , MultiParamTypeClasses +#-}++{-# OPTIONS_GHC -Wno-unused-top-binds #-}+{-# OPTIONS_GHC -Wno-unused-imports   #-}++module Language.Nominal.Examples.Tutorial+    ( +      -- $blurb++      -- * Basics of names+      -- $basics+      MyNameLabel+    , MyName  +      -- * Creating fresh names+      -- $setup+      +      -- * Creating @'Nom'@ bindings with @'res'@ +      -- $res++      -- * Binding multiple names+      -- $multiple++      -- * Local scope out of global names +      -- $local++      -- * Nameless types+      -- $nameless++      -- * The monad of name-binding +      -- $bindings+      +      ++      -- * Name-abstraction +      -- $abstraction++      -- * Functorial action of binders+      -- $abs_functorial++      -- * Swapping+      -- $swapping+ +      -- * Unification up to permutation +      -- $unify++      -- * Substitution+      -- $substitution++      -- * Names and atoms+      -- $atoms+    )+    where++import Data.Default++import Language.Nominal.Name +import Language.Nominal.Nom+import Language.Nominal.Binder+import Language.Nominal.Abs +import Language.Nominal.Sub +import Language.Nominal.Unify++#include "../Blurb.txt"++{- $basics++Let's start by declaring a type @'MyNameLabel'@ of labels for names; our labels are just strings.  ++__Example:__ More complex examples of labels are in the "Language.Nominal.Examples.SystemF" example, including labels that can themselves contain names.+ +Then we create a type @'MyName'@ of @'MyNameLabel'@-labelled names. +An inhabitant of this type is a string-labelled name.  +Under the hood names are implemented a pair of a "Unique" identifier, and a label.  +So names are just unique hashable atomic objects with a label attached. +++-}++type MyNameLabel = String +type MyName = Name MyNameLabel +++{- $setup++  +   Let's create a fresh name @a'@.  Note that it's wrapped in a name-binding monad @'Nom'@; more on that shortly.+  +   >>> let a' = freshName "a" :: Nom MyName+  +   Is @a' == a'@?+   +   >>> a' == a'+   False+  +   No!+   This is because evaluation is lazy, so two copies of @a'@ are created in two distinct local name-binding contexts; +   one to the left of the @'=='@ and the other to the right.+   +   But we can unpack name-binding context in (at least) two ways: using 'exit', or using 'nomToIO':++   >>> a1 = exit a' :: MyName+   >>> a2 = exit a' :: MyName+   >>> a  <- nomToIO a' :: IO MyName+   +   Both methods trigger the computation of actual fresh identifiers for any bindings.+   We may prefer 'nomToIO' in this tutorial, just because we're at an interactive prompt, but the code has many examples of the use of 'exit' (which is also a more polymorphic method):+  +   >>> a == a+   True+   >>> a1 == a1+   True+   >>> a2 == a2+   True+   >>> a1 == a2+   False +   >>> a == a1+   False ++   @a@ is just a plain datum, whose name-identifier was generated fresh.  So if we do this again:++   >>> b <- nomToIO a' :: IO MyName+   >>> a == b+   False++   This is to be expected: the unique identifier of @b@ was generated fresh for that of @a@. +   +   __Warning__: The label of @b@ is still @"a"@ ... of course:++   >>> nameLabel b+   "a"+   >>> nameLabel a == nameLabel b+   True+-}++{- $res+   Having freed @a@ from its name-binding context, we can wrap it up again.+  +   >>> let a'' = resN [a] a :: Nom MyName+  +   This isn't equal to @a'@ because the name bound in @a''@ is bound by a separate context from that bound in @a'@: +  +   >>> a' == a''+   False+-}++{- $multiple+ +   We can bind multiple names simultaneously:+   +   >>> let x1 = resN [a,b] (a,a,b) :: Nom (MyName, MyName, MyName)++   We'll see more of @x1@ later.++-}++{- $local++   Now for a more involved example.  We show how @'resN'@ creates local scope:++   >>> :set -XScopedTypeVariables+   >>> let prop_split_scope (n :: MyName) = (resN [n] n) /= (resN [n] n)++   Note we use /one/ input name @n@ to create /two/ output local scopes.  This should return @'True'@ on @a@:++   >>> prop_split_scope a+   True+-}++{- $nameless+   Some types, like @'Bool'@ and @'String'@, are @'Nameless'@.  +   E.g. if we have a truth-value, we know it doesn't have any names in it; we might have used names to calculate the truth-value, but the truth-value itself @'True'@ or @'False'@ is nameless.+ +   On @'Nameless'@ types the @'Nom'@ context can always be removed.  We can use @'unNom'@ (a general and versatile function which happens to be useful in this instance). +   Let's illustrate this by safely extracting @a@'s nameless 'String' label: +  +   >>> unNom $ nameLabel <$> a' :: MyNameLabel+   "a"+-} ++{- $bindings+   @'Nom'@ is a monad.  We can use monad composition @'>>='@ to go under a binder: +  +   >>> unNom $ a' >>= \a -> return $ a == a+   True+ +   We can use monad composition to merge binding contexts in a capture-avoiding manner.  Compare @x1@ with @x2@ below:++   >>> let x1 = resN [a,b] (a,a,b) :: Nom (MyName, MyName, MyName)+   >>> let x2 = a' >>= \a -> a' >>= \b -> return (a,a,b) :: Nom (MyName, MyName, MyName) +   +   @x2@ is /morally equal/ to @x1@, though an equality test will return @False@ because they each have their own local binding context.  ++   >>> x1 == x2+   False++   @x1@ and @x2@ are /unifiable/.  We'll come to that later.++-}++{- $abstraction++   The package offers facilities for @'Abs'@traction.  Let's @'abst'@ract @a@ in @a@: +  +   >>> absaa = abst a a :: Abs MyNameLabel MyName+  +   Think of @absaa@ as the @a.a@ in @λa.a@.+   Unlike the @'res'@ binding @'x1'@, this abstraction is equal to itself ...+  +   >>> absaa == absaa+   True+   +   ... and to any other alpha-equivalent abstraction:++   >>> absaa == abst b b+   True+   +   Likewise:+   +   >>> c <- (nomToIO $ freshName "a") :: IO MyName+   >>> abst b [a, b]  ==  abst c [a, c] +   True++   __Warning:__ The label of the abstracted name is preserved; only its identifier gets alpha-converted.  Thus, this returns false, just because @"a" /= "d"@:+   +   >>> d <- (nomToIO $ freshName "d") :: IO MyName+   >>> abst b [a, b]  ==  abst d [a, d] +   False ++   We can concrete @absaa@ at @a@ to get @a@, or at @b@ to get @b@.+  +   >>> conc absaa a == a+   True+  +   >>> conc absaa b == b+   True++   Name labels come from the abstraction, whereas the name's identifier comes from the argument. +   Thus, we get @"a"@ below and not @"d"@ (recall the labels of @a@, @b@, and @c@ are @"a"@ and the label of @d@ is @"d"@):++   >>> nameLabel a+   "a"+   >>> nameLabel d+   "d"+   >>> nameLabel (conc absaa d) +   "a"++   __Example:__ There are many examples of using abstractions in "Language.Nominal.Examples.SystemF".  + +   __Warning__: Behaviour if we concrete an abstraction at a name that is not fresh, is undefined. ++   >>> conc (abst a (a, b)) b :: (MyName, MyName)+   ...++-}++{- $abs_functorial++   Our machinery now pays dividends.  Abstraction is functorial, and capture-avoidance is automagical: + +   >>> let aTob = (map $ \n -> if n == a then b else n) :: [MyName] -> [MyName]+   >>> c <- (nomToIO $ freshName "a") :: IO MyName+   >>> (aTob <$> abst a [a, b])  ==  abst a [a, b] +   True+   >>> (aTob <$> abst b [a, b])  ==  abst c [b, c]  +   True++   Another equally valid rendering of the second example above, because alpha-equivalence allows it:++   >>> (aTob <$> abst b [a, b])  ==  abst a [b, a]  +   True+   +   __Note__: @'resN'@ is functorial in the same way, but it unbinds its local scope differently from @'abst'@:  +   +   >>> resN [a] a == resN [a] a+   False+   +   >>> abst a a == abst a a+   True+-}  ++-- * Swapping+{- $swapping++>>> [a, b, c] <- nomToIO $ freshNames ["a", "b", "c"]++We can swap @a@ and @b@ in simple types like lists ...++>>> swpN a b [a,b,c,a,a,c] == [b,a,c,b,b,c]+True++... and in not-so-simple types, like 'Abs', 'Nom', and function-types. ++>>> :{ + f n  +   | n == a    = b+   | n == b    = c+   | n == c    = a+   | otherwise = n+:}++>>> map f [a, b, c] == [b, c, a]+True++>>> fswp = swpN a b f +>>> map fswp [a, b, c] == [c, a, b]+True++-}+++{- $unify+   Recall @x1@ and @x2@ above; let's reconstruct them here:++   >>> [a, b] <- nomToIO $ freshNames ["a", "b"] +   >>> let x1 = resN [a,b] (a,a,b) :: Nom (MyName, MyName, MyName)+   >>> let x2 = x1                 :: Nom (MyName, MyName, MyName)+   +   We noted that @x1@ and @x2@ are not equal because they have distinct local scopes:+   +   >>> x1 == x2+   False++   However, they /are/ unifiable:+   +   >>> unifiablePerm x1 x2+   True++   If a type is sufficiently structured, 'unifiablePerm' can be used as an equality predicate that tries to unify local scopes.  More on this in "Language.Nominal.Unify", with many example applications in "Language.Nominal.Examples.IdealisedEUTxO".++-}++{- $substitution++We have a theory of substitution given by a typeclass @'Sub'@ with function @'sub'@.+This works automatically on simple datatypes (like lists and name-abstractions) and can be extended using typeclasses to more complex datatypes (see "Language.Nominal.Examples.SystemF").++>>> [a, b, b', c] <- nomToIO $ freshNames [(), (), (), ()] +>>> sub a b [a,b,c] == [b,b,c]+True+>>> (sub a b $ abst b [a,b,c]) == abst b' [b, b', c]+True++__Gotcha__: The expression below might not mean what you think.  Note the bracketing!++>>> sub a b $ abst b [a,b,c] == abst b' [b, b', c]+False++-}++{- $atoms++We actually have two species of identifier:++* Names (like @'Name' 'String'@) , as discussed above, and+* atoms (like @'Atom'@).++Both names and atoms are datatypes of bindable identifiers, but names come with labels and atoms don't.+An atom is essentially identical to a @()@-labelled name, and conversely a name is essentially identical to a pair of an atom and the name's label.++So why maintain both?  ++* /If you need identifiers with no semantic information,/ then use atoms.  We do this in "Language.Nominal.Examples.IdealisedEUTxO", where atoms are used to identify locations in a blockchain.  +Because our identifiers have no semantic content aside from pointing to themselves, we use atoms.++* /If you need identifiers with associated semantic information/ (e.g. a denotation, a type, or even just a display name), then you might prefer to use names.  We do this in "Language.Nominal.Examples.SystemF", where term names 'Language.Nominal.Examples.SystemF.NTrm' are labelled with types 'Language.Nominal.Examples.SystemF.Typ'.++* Although we can emulate atoms as @()@-labelled names, these are not quite the same thing.  +Atoms are interesting because they give us swapping, and swapping gives us 'res' and 'abst'. +Names (i.e. labelled atoms) are built /on top of/ this underlying structure.  (So even if we only exposed names and not atoms, the atoms would still be there.) ++Sometimes functions come in two versions: an atoms-version and a names-version (e.g. 'swp' and 'swpN', and 'res' and 'resN'). +Where this occurs, the N (for 'Name') version just discards labels and calls the atoms-version.++/Instead of names, why not maintain a state lookup monad, associating atoms to their semantic information?/+We could, but we'd have to thread it through our computations (if they need labelled atoms), incurring overhead that defeats a purpose of the design of this package, to /not/ require everything to happen inside a 'Nom' monad (see for example @prop_split_scope@ above).+It is a principle of nominal techniques that /names are data/: pure data should not require an omnipresent top-level monad.++__Gotcha:__ Names are compared for equality on their atoms.  Labels are discarded during the equality check:++>>> a = exit $ freshName "a" +>>> b = a `withLabel` "b"+>>> a == b+True++Wait, we can explain!  ++* We get 'Eq' and 'Ord' instances of name-types (because atoms have them) even if the labels don't. ++* We get "Data.Map" on name-types, again even if the labels lack 'Eq' or 'Ord'.+ +* Have you considered why you're asking for this?  A name is an atomic ID tagged with information, and one atom occurring associated to multiple tags is like one license plate number on multiple cars; that's /not/ what /unique/ identifiers are meant for.  Or if you must do this, you can, but then it's up to you to keep track of which label (or combination of labels) is "true".  This package makes it easy to create fresh atoms, so perhaps you'd be better off creating multiple fresh atoms and giving a distinct label to each one.+++-}+++
+ src/Language/Nominal/Examples/UntypedLambda.hs view
@@ -0,0 +1,98 @@+{-|+Module      : Untyped Lambda-Calculus +Description : Syntax and reductions of the untyped lambda-calculus using the Nominal package+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Untyped lambda-calculus: syntax, substitution, nominal-style recursion, weak head normal form function, and a couple of examples.++Compare with an example in <https://hackage.haskell.org/package/bound the Bound package>. ++-}++{-# LANGUAGE InstanceSigs          +           , DeriveGeneric         +           , LambdaCase +           , MultiParamTypeClasses +           , DeriveAnyClass       -- to derive 'Swappable' +           , DeriveDataTypeable   -- to derive 'Data' +           , FlexibleInstances     +#-}+++module Language.Nominal.Examples.UntypedLambda+    ( +     Var, Exp (..), whnf, lam, example1, example1whnf, example2, example2whnf +    )+    where++import GHC.Generics+import Data.Generics     hiding (Generic, typeOf)++import Language.Nominal.Utilities+import Language.Nominal.Name +import Language.Nominal.Nom+import Language.Nominal.Binder+import Language.Nominal.Abs +import Language.Nominal.Sub ++-- | Variables are string-labelled names+type Var = Name String ++infixl 9 :@+-- | Terms of the untyped lambda-calculus +data Exp = V Var              -- ^ Variable +         | Exp :@ Exp         -- ^ Application +         | Lam (KAbs Var Exp) -- ^ Lambda, using abstraction-type + deriving (Eq, Generic, Data, Swappable, Show)++-- | helper for building lambda-abstractions +lam :: Var -> Exp -> Exp +lam x a = Lam (x @> a)++-- | Substitution.  Capture-avoidance is automatic.+instance KSub Var Exp Exp where+   sub :: Var -> Exp -> Exp -> Exp +   sub v t = rewrite $ \case -- 'rewrite' comes from Scrap-Your-Boilerplate generics.  It recurses properly under the binder. +      V v' | v' == v -> Just t   -- If @V v'@, replace with @t@ ... +      _              -> Nothing  -- ... otherwise recurse.++{- The substitution instance above is equivalent to the following:+ +-- | Explicit recursion.     +expRec :: (Var -> a) -> (Exp -> Exp -> a) -> (Var -> Exp -> a) -> Exp -> a +expRec f0 _ _ (V n)      = f1 n+expRec _ f1 _ (s1 :@ s2) = f2 s1 s2+expRec _ _ f2 (Lam x')   = f3 `genApp` x' ++instance KSub Var Exp Exp where+   sub :: Var -> Exp -> Exp -> Exp +   sub v t = expRec (\v'   -> if v' == v then t else V v') +                    (\a b  -> sub v t a :@ sub v t b) +                    (\v' a -> lam v' $ sub v t a)+-}++-- | weak head normal form of a lambda-term.+whnf :: Exp -> Exp +whnf (f :@ a) = case whnf f of+  Lam b' -> whnf $ b' `conc` a  +  f'     -> f' :@ a+whnf e = e++-- | (\x x) y+example1 :: Exp+example1 = (\[x, y] -> lam x $ V x :@ V y) `genAppC` freshNames ["x", "y"] +-- | y+example1whnf :: Exp+example1whnf = whnf example1++-- | (\x xy) x+example2 :: Exp+example2 = (\[x, y] -> lam x (V x :@ V y) :@ V x) `genAppC` freshNames ["x", "y"] +-- | xy+example2whnf :: Exp+example2whnf = whnf example2+
+ src/Language/Nominal/Name.hs view
@@ -0,0 +1,345 @@+{-|+Module      : Name+Description : Nominal theory of names and swappings+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++The basic framework: a nominal theory of names and swappings+-}++{-# LANGUAGE ConstraintKinds            +           , DataKinds                  +           , DefaultSignatures          +           , DeriveAnyClass             +           , DeriveGeneric              +           , DerivingStrategies         +           , DerivingVia                +           , DeriveDataTypeable+           , DeriveFunctor                +           , DeriveFoldable               +           , DeriveTraversable            +           , EmptyCase                  +           , EmptyDataDeriving+           , FlexibleContexts           +           , FlexibleInstances          +           , GADTs                      +           , GeneralizedNewtypeDeriving   +           , InstanceSigs               +           , MultiParamTypeClasses      +           , PartialTypeSignatures        +           , ScopedTypeVariables        +           , StandaloneDeriving           +           , TupleSections              +#-}++module Language.Nominal.Name+    ( -- $setup+      -- * Atoms+      KAtom (..)+    , Atom+    , Tom -- (..)+    , atTom+    -- * Creating atoms+    , freshKAtomsIO +    , freshAtomsIO+    , freshKAtomIO +    , freshAtomIO+    -- * Atom swapping+    , Swappable (..)+    , swp +    -- * Permutations+    , KPerm +    , Perm+    , perm+    -- * Names+    , KName (..)+    , Name+    , withLabel +    , withLabelOf+    , justALabel+    , justAnAtom+    -- * Name swapping+    , kswpN+    , swpN+    -- * Nameless types+    , Nameless (..)+    -- * Tests+    -- $tests+    ) +    where++import           Data.Data                  hiding (typeRep, TypeRep)+import           Data.List.NonEmpty         (NonEmpty)+import           Data.Type.Equality         -- for testEquality+import qualified Data.Map                   as DM +import qualified Data.Set                   as S +import           GHC.Generics               hiding (Prefix)+import           Type.Reflection++import           Language.Nominal.Unique+import           Language.Nominal.Utilities+++{- $setup+-} ++-- * Atoms++-- | An atom is a unique atomic token. +--+-- The argument @s@ of 'KAtom' is part of facilities offered by this package for declaring types of atom @s@ ranging over kinds @k@.  For usage see 'Language.Nominal.Examples.SystemF.ATyp', and 'Language.Nominal.Examples.SystemF.ATrm' in "Language.Nominal.Examples.SystemF".+-- +-- /If your development requires just a single type of atomic tokens, ignore 'KAtom' and use 'Atom'./ +newtype KAtom s = Atom Unique+   deriving (Eq, Ord, Generic, Typeable, Data)++-- | We provide a stock datatype @'Tom'@. +--+-- Using the @DataKinds@ package, this is then used to provide a stock type of atoms @'Atom'@. +data Tom +   deriving (Eq, Ord, Generic, Typeable, Data)++-- | A proxy element for sort @'Tom'@.  If we pass this, we tell the typechecker we are "at Tom".+atTom :: Proxy Tom+atTom = Proxy++-- | A distinguished type of atoms.+--+-- It is populated by @'Tom'@s (below), thus an element of @'Atom'@ is "a Tom".+--+-- We provide @'Atom'@ as primitive for convenience.  If you need more than one type of atom (e.g. term atoms and type atoms), look at 'KAtom'. +type Atom = KAtom Tom++-- | Display an atom by showing (the hash of) its unique id. +instance Show (KAtom s) where+   show (Atom a) = "_" ++ show (hashUnique a)++-- * Creating atoms++-- | Make a fresh atom for each element of some list (@a@ny list).  /If you just want one fresh atom, use e.g. @[()]@./+--+-- This is an IO action; when executed, fresh identifiers get generated.+freshKAtomsIO :: Traversable m => m a -> IO (m (KAtom s))+freshKAtomsIO = mapM (const $ Atom <$> newUnique) ++-- | Make a fresh atom at @'Tom'@ for each element of some list (@a@ny list).+freshAtomsIO :: Traversable m => m a -> IO (m Atom)+freshAtomsIO = freshKAtomsIO++-- | For convenience: generate a fresh katom+freshKAtomIO :: IO (KAtom s) +freshKAtomIO = head <$> freshKAtomsIO [()]++-- | For convenience: generate a fresh atom+--+-- >>> a <- freshAtomIO +-- >>> b <- freshAtomIO+-- >>> a == b+-- False +freshAtomIO :: IO Atom +freshAtomIO = head <$> freshAtomsIO [()]++-- * Atom swapping++-- | Types that admit a __swapping action__.  +--+-- A swapping @(a b)@ maps +--+-- * @a@ to @b@ and +-- * @b@ to @a@ and +-- * any other @c@ to @c@.+--+-- Swappings are invertible, which allows them to commute through type-formers containing negative arities, e.g. the left-hand argument of function arrow.  Swappings always distribute:+--+-- > swp a b (x, y)       == (swp a b x, swp a b y)+-- > swp a b [x1, x2, x3] == [swp a b x1, swp a b x2, swp a b x3] +-- > swp a b (f x)        == (swp a b f) (swp a b x)+-- > swp a b (abst n x)   == abst (swp a b n) (swp a b x)+-- > swp a b (res [n] x)  == res [swp a b n] (swp a b x)+-- > swp a b (Name t x)   == Name (swp a b t) (swp a b x)+--+-- __Technical note:__ The content of @Swappable a@ is that @a@ supports a swapping action by atoms of every @s@.  Everything else, e.g. 'Language.Nominal.Nameset.KSupport', just uses @s@.  So @k@ is a "world" of sorts of atoms, for a particular application.+-- This is invisible at our default world @'Tom'@ because @'Tom'@ has only one inhabitant, @''Tom'@.  See 'Language.Nominal.Examples.SystemF.ASort' and surrounding code for a more sophisticated atoms setup.+class Swappable a where  ++   kswp :: Typeable s => KAtom s -> KAtom s -> a -> a        --  swap n and n' in a+   default kswp :: (Typeable s, Generic a, GSwappable (Rep a)) => KAtom s -> KAtom s -> a -> a+   kswp n n' = to . gswp n n' . from++-- | A @'Tom'@-swapping+swp :: Swappable a => Atom -> Atom -> a -> a+swp = kswp++-- Don't need () instance because captured by @'Nameless'@ instance Swappable a => Swappable ()+instance Swappable a => Swappable (Maybe a)+instance Swappable a => Swappable [a]+instance Swappable a => Swappable (NonEmpty a)+instance (Ord a, Swappable a) => Swappable (S.Set a) where+   kswp a1 a2 s = S.fromList $ kswp a1 a2 (S.toList s)  -- Ord a so we can use fromList+instance (Swappable a, Swappable b) => Swappable (a, b)+instance (Swappable a, Swappable b, Swappable c) => Swappable (a,b,c)+instance (Swappable a, Swappable b, Swappable c,  Swappable d) => Swappable (a,b,c,d)+instance (Swappable a, Swappable b, Swappable c,  Swappable d, Swappable e) => Swappable (a,b,c,d,e)+instance (Swappable a, Swappable b) => Swappable (Either a b)+++-- | Swap distributes over function types, because functions inherit swapping action pointwise (also called the /conjugation action/)+instance (Swappable a, Swappable b) => Swappable (a -> b) where+   kswp a1 a2 f = kswp a1 a2 . f . kswp a1 a2 ++-- | Swap distributes over map types. +--+-- Note that maps store their keys ordered for quick lookup, so a swapping acting on a map is not a noop and can provoke reorderings.+instance (Swappable a, Swappable b, Ord a) => Swappable (DM.Map a b) where+    kswp n1 n2 m = DM.fromList $ kswp n1 n2 (DM.toList m)  -- This design treats a map explicitly as its graph (list of pairs).  Could also view it as a function, and consider implementing conjugation action using DM.map and/or DM.mapKeys  ++-- | Base case for swapping: atoms acting on atoms.+instance Typeable s => Swappable (KAtom s) where    -- typeable constraint gives us type representatives which allows the runtime type equality test (technically: type representation equality test) below. +    kswp (a1 :: KAtom t) (a2 :: KAtom t) (a :: KAtom s) = -- explicit type annotations for clarity here +        case testEquality (typeRep :: TypeRep t) (typeRep :: TypeRep s) of  +            Nothing         -> a   -- are s and t are different types +            Just Refl              -- are s and t the same type? +                | a == a1   -> a2  +                | a == a2   -> a1  +                | otherwise -> a+++-- * Permutations++-- | A permutation represented as a list of swappings (simple but inefficient).+type KPerm s = [(KAtom s, KAtom s)] ++-- | A permutation at @'Tom'@.+type Perm = KPerm Tom++-- | A permutation acts as a list of swappings.  Rightmost/innermost swapping acts first.+--+-- >>> a <- freshAtomIO +-- >>> b <- freshAtomIO+-- >>> c <- freshAtomIO+-- >>> perm [(c,b), (b,a)] a == c+-- True +perm :: (Typeable s, Swappable a) => KPerm s -> a -> a          +perm = chain . map (uncurry kswp)  +++-- * Names++-- | A name is a pair of +--+-- * an atom, and +-- * a label @t@. +--+-- @t@ is intended to store semantic information about the atom.  For instance, if implementing a simply-typed lambda-calculus then @t@ might be a dataype of (object-level) types.+--+-- A similar effect could be achieved by maintaining a monadic lookup context relating atoms to their semantic information; the advantage of using a name is that this information is packaged up with the atom in a local datum of type @'Name'@. +data KName s t = Name { nameLabel :: t, nameAtom :: KAtom s}+   deriving (Generic, Functor, Foldable, Traversable, Typeable, Data) ++-- | Swapping atoms in names distributes normally; so we swap in the semantic label and also in the name's atom identifier.  Operationally, it's just a tuple action:+-- +-- > swp atm1 atm2 (Name t atm)  = Name (swp atm1 atm2 t) (swp atm1 atm2 atm)+instance (Typeable s, Swappable t) => Swappable (KName s t) ++-- | A @'Tom'@ instance of @'KName'@.+type Name = KName Tom +++-- | Names are equal when they refer to the same atom.+-- +-- WARNING: Labels are not considered! +-- In particular, @t@-names always have @'Eq'@, even if the type of labels @t@ does not.+instance Eq (KName s t) where+   n1 == n2 = nameAtom n1 == nameAtom n2 ++-- | Names are leq when their atoms are leq.+--+-- WARNING: Labels are not considered! +-- In particular, @t@-names are always ordered even if /labels/ @t@ are unordered. +instance Ord (KName s t) where+   n1 `compare` n2 = nameAtom n1 `compare` nameAtom n2 ++instance Show t => Show (KName s t) where+   show nam = show (nameLabel nam) ++ show (nameAtom nam)+instance {-# OVERLAPPING #-} Show (KName s ()) where+   show nam = "n" ++ show (nameAtom nam)+++-- | As the name suggests: overwrite the name's label+withLabel :: KName s t -> t -> KName s t+n `withLabel` t = const t <$> n -- functorial action automatically derived ++-- | Overwrite the name's label.  Intended to be read infix as @n `withLabelOf n'@+withLabelOf :: KName s t -> KName s t -> KName s t+n `withLabelOf` n' = n `withLabel` (nameLabel n') ++-- | Name with @'undefined'@ atom, so really just a label.  Use with care!+justALabel :: t -> KName s t+justALabel = flip Name undefined++-- | Name with @'undefined'@ label, so really just an atom.  Use with care!+justAnAtom :: KAtom s -> KName s t+justAnAtom = Name undefined +++-- * Name swapping++-- | A name swap discards the names' labels and calls the atom-swap @'kswp'@.+kswpN :: (Typeable s, Swappable a) => KName s t -> KName s t -> a -> a+kswpN n n' = kswp (nameAtom n) (nameAtom n') ++-- | A name swap for a @'Tom'@-name.  Discards the names' labels and calls a @'Tom'@-atom swapping.+swpN :: Swappable a => Name t -> Name t -> a -> a+swpN = kswpN +++-- * Nameless types++-- | Some types, like @'Bool'@ and @'String'@, are @'Nameless'@.  E.g. if we have a truth-value, we know it doesn't have any names in it; we might have used names to calculate the truth-value, but the truth-value itself @'True'@ or @'False'@ is nameless. +newtype Nameless a = Nameless {getNameless :: a}+    deriving (Show, Read, Eq, Ord)++instance Swappable (Nameless a) where+    kswp _ _ = id+-- TODO: KEquivar s (Nameless a) where+-- KEquivar s (Nameless a) where+--    kswp _ _ = id++-- deriving via is described in:+-- Deriving Via: or, How to Turn Hand-Written Instances into an Anti-Pattern+-- https://www.kosmikus.org/DerivingVia/deriving-via-paper.pdf++deriving via Nameless Bool instance Swappable Bool+deriving via Nameless Int  instance Swappable Int+deriving via Nameless ()   instance Swappable ()+deriving via Nameless Char instance Swappable Char+++-- * Generics support for @'KSwappable'@++class GSwappable f where+    gswp :: Typeable s => KAtom s -> KAtom s -> f x -> f x++instance GSwappable V1 where   -- empty types, no instances+    gswp _ _ x = case x of++instance GSwappable U1 where   -- one constructor, no arguments+    gswp _ _ U1 = U1++instance Swappable c => GSwappable (K1 i c) where  -- base case.  wrapper for all of some type c so we escape back out to swp.  +    gswp m n x = K1 $ kswp m n $ unK1 x++instance (GSwappable f, GSwappable g) => GSwappable ((:*:) f g) where  -- products+    gswp m n (x :*: y) = gswp m n x :*: gswp m n y++instance (GSwappable f, GSwappable g) => GSwappable ((:+:) f g) where  -- sums+    gswp m n (L1 x) = L1 $ gswp m n x+    gswp m n (R1 y) = R1 $ gswp m n y++instance GSwappable f => GSwappable (M1 i c f) where -- meta-information.  e.g. constructor names (like for generic show method), fixity information; all captured by M1 type.  this is transparent for swappings+    gswp m n = M1 . gswp m n . unM1++{- $tests Property-based tests are in "Language.Nominal.Properties.NameSpec". -}
+ src/Language/Nominal/NameSet.hs view
@@ -0,0 +1,209 @@+{-|+Module      : NameSet +Description : Theory of support, apartness, and restriction +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Typeclasses and operations having to do with sets of names/atoms, namely: ++* 'Support', +* 'apart'ness, and +* 'restrict'ion.+-}++{-# LANGUAGE ConstraintKinds       +           , DataKinds             +           , DefaultSignatures     +           , DerivingVia           +           , EmptyCase             +           , FlexibleContexts      +           , FlexibleInstances     +           , GADTs                 +           , InstanceSigs          +           , MultiParamTypeClasses +           , PartialTypeSignatures   +           , ScopedTypeVariables     +           , StandaloneDeriving      +           , TupleSections         +           , TypeOperators         +#-}  ++module Language.Nominal.NameSet+    ( -- * Support and apartness+      KSupport (..)+    , Support+    , supp+    , kapart+    , apart+    -- * Identifying list elements by name or atom +    , atomPoint+    , namePoint+    -- * Restriction+    , KRestrict (..) +    , Restrict+    , restrictN+    -- * Tests+    -- $tests+    ) where++import           Data.Proxy                 (Proxy (..))+import           Data.Type.Equality+import           Type.Reflection+import           Data.List.NonEmpty         (NonEmpty)+import           Data.Set                   (Set)+import qualified Data.Set                   as S   +import           GHC.Generics          ++import           Language.Nominal.Name+import           Language.Nominal.Utilities++++-- * Support++-- | A typeclass for elements for which a supporting set of atoms can be computed in an efficient, structural, type-directed manner.  +--+-- So: /lists/, /sets/, and /name-abstractions/ yes, and /function-types/ no.  +-- See instances for full details. +--+-- /Note: This gives 'KSupport' a strictly more specific and structure-directed meaning than the motivating mathematical notion of support, which __does__ work e.g. on function-types./+--+class (Typeable s, Swappable a) => KSupport s a where   +    ksupp :: proxy s -> a -> Set (KAtom s)+    default ksupp :: (Generic a, GSupport s (Rep a)) => proxy s -> a -> Set (KAtom s)+    ksupp _ = gsupp . from++-- | A 'Tom' instance of 'KSupport'. +type Support a = KSupport Tom a++-- | A 'Tom' instance of 'ksupp'. +supp :: Support a => a -> Set Atom+supp = ksupp atTom++instance Typeable s => KSupport s (Nameless a) where+    ksupp _ _ = S.empty +deriving via Nameless ()   instance Typeable s => KSupport s ()+deriving via Nameless Bool instance Typeable s => KSupport s Bool+deriving via Nameless Char instance Typeable s => KSupport s Char+deriving via Nameless Int  instance Typeable s => KSupport s Int++-- order: nameless, tuple, list, nonempty list, maybe, sum, atom, name, nom, abs +instance (Typeable s, Typeable t) => KSupport s (KAtom t) where  +    ksupp _ a = case testEquality (typeRep :: TypeRep s) (typeRep :: TypeRep t) of+        Nothing   -> S.empty+        Just Refl -> S.singleton a+instance (Typeable s, Typeable u, KSupport s t) => KSupport s (KName u t) where+   ksupp p a = ksupp p $ (nameAtom a, nameLabel a)+-- instance {-# OVERLAPPABLE #-} (Foldable f, KSupport s a) => KSupport s (f a) where+--    supp = foldMap supp -- No good: causes Ambiguity warnings; and incorrect on pairs, which are foldable but by action on second component.+instance KSupport s a => KSupport s (Maybe a)+instance KSupport s a => KSupport s [a]+instance KSupport s a => KSupport s (NonEmpty a)+instance (Ord a, KSupport s a) => KSupport s (S.Set a) where +   ksupp p = foldMap $ ksupp p+instance (KSupport s a, KSupport s b) => KSupport s (a, b)+instance (KSupport s a, KSupport s b, KSupport s c) => KSupport s (a, b, c)+instance (KSupport s a, KSupport s b, KSupport s c, KSupport s d) => KSupport s (a, b, c, d)+instance (KSupport s a, KSupport s b, KSupport s c, KSupport s d, KSupport s e) => KSupport s (a, b, c, d, e)+instance (KSupport s a, KSupport s b) => KSupport s (Either a b)+-- TODO: map instance ++-- | @a@ and @b@ are 'kapart' when they are supported by disjoint sets of @s@-atoms.+--+-- /We use @proxy@ instead of 'Proxy' below, so the user can supply any type that mentions @s@./ +kapart :: (KSupport s a, KSupport s b) => proxy s -> a -> b -> Bool  +kapart p a b = (ksupp p a) `S.disjoint` (ksupp p b)++-- | @a@ and @b@ are 'apart' when they are supported by disjoint sets of atoms.+apart :: (Support a, Support b) => a -> b -> Bool+apart = kapart atTom+++-- * Identifying list elements by name or atom ++-- | Bring the first element of a list-like structure that an atom points to (by being mentioned in the support), and put it at the head of the nonempty list.  Raises error if no such element exists. +atomPoint :: (Foldable f, KSupport s a) => KAtom s -> f a -> NonEmpty a+atomPoint a = point $ S.member a . ksupp Proxy++-- | `atomPoint`, for names.  A name is just a labelled atom, and @namePoint@ just discards the label and calls @'atomPoint'@.+namePoint :: (Foldable f, KSupport s a) => KName s t -> f a -> NonEmpty a+namePoint = atomPoint . nameAtom+++-- * Restriction++-- | Class for types that support a /remove these atoms from my support, please/ operation. +-- Should satisfy e.g.: +--  +-- > restrict atms $ restrict atms x == restrict atms x+--+-- > atms `apart` x ==> restrict atms x == x+--+-- The canonical instance of @'KRestrict'@ is @'Language.Nominal.Nom.Nom'@.+-- The @'Swappable'@ constraint is not necessary for the code to run, but in practice wherever we use @'KRestrict'@ we expect the type to have a swapping action.+--+-- /Note for experts:/ We may want @'KRestrict'@ without @'KSupport'@, for example to work with @Nom (Atom -> Atom)@. +--+-- /Note for experts:/ Restriction is familiar in general terms (e.g. pi-calculus restriction).  In a nominal context, the original paper is <https://dl.acm.org/doi/10.1145/1069774.1069779 nominal rewriting with name-generation> (<http://gabbay.org.uk/papers.html#nomrng author's pdf>), and this has a for-us highly pertinent emphasis on unification and rewriting. +class (Typeable s, Swappable a) => KRestrict s a where+   restrict  :: [KAtom s] -> a -> a   ++-- | Instance of 'KRestrict' on a 'Tom'.+type Restrict = KRestrict Tom++-- | Form of restriction that takes names instead of atoms.  Just discards name labels and calls @'restrict'@.+restrictN :: KRestrict s a => [KName s t] -> a -> a+restrictN l = restrict (nameAtom <$> l)+++-- | Restriction is trivial on elements of nameless types +instance Typeable s => KRestrict s (Nameless a) where+   restrict _ = id++deriving via Nameless Bool instance Typeable s => KRestrict s Bool+deriving via Nameless Int  instance Typeable s => KRestrict s Int+deriving via Nameless ()   instance Typeable s => KRestrict s ()+deriving via Nameless Char instance Typeable s => KRestrict s Char++-- | Restriction is monadic on Maybe +instance KRestrict s a => KRestrict s (Maybe a) where+  restrict atms a = restrict atms <$> a+-- | On lists, Restrict traverses the list and eliminate elements for which any of the @atms@ are in the support.  +--+-- A alternative is to assume restriction on the underlying elements and restrict pointwise.  The elimination choice seems more useful in practice. +instance KSupport s a => KRestrict s [a] where+   restrict atms as = filter (kapart (Proxy :: Proxy s) atms) as+-- | Eliminate elements for which any of the @atms@ are in the support+instance (Ord a, KSupport s a) => KRestrict s (S.Set a) where+   restrict atms as = S.filter (kapart (Proxy :: Proxy s) atms) as++++-- * Generics support for @'KSupport'@+--+class GSupport s f where+    gsupp :: f x -> Set (KAtom s)++instance GSupport s V1 where+    gsupp x = case x of++instance GSupport s U1 where+    gsupp U1 = S.empty++instance GSupport s f => GSupport s (M1 i t f) where+    gsupp = gsupp . unM1++instance KSupport s c => GSupport s (K1 i c) where+    gsupp = ksupp Proxy . unK1++instance (GSupport s f, GSupport s g) => GSupport s (f :*: g) where+    gsupp (x :*: y) = gsupp x `S.union` gsupp y++instance (GSupport s f, GSupport s g) => GSupport s (f :+: g) where+    gsupp (L1 x) = gsupp x+    gsupp (R1 y) = gsupp y++{- $tests Property-based tests are in "Language.Nominal.Properties.NameSetSpec". -}
+ src/Language/Nominal/Nom.hs view
@@ -0,0 +1,272 @@+{-|+Module      : Nom+Description : Nominal-flavoured implementation of data in a context of local names+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Nominal-flavoured implementation of data in a context of local names+-}++{-# LANGUAGE ConstraintKinds+           , DataKinds+           , DeriveFunctor+           , DeriveFoldable+           , DeriveTraversable+           , DeriveGeneric+           , DerivingVia+           , FlexibleContexts+           , FlexibleInstances+           , FunctionalDependencies+           , GADTs +           , GeneralizedNewtypeDeriving+           , InstanceSigs+           , MultiParamTypeClasses+           , PartialTypeSignatures+           , PatternSynonyms+           , ScopedTypeVariables+           , StandaloneDeriving+           , TypeApplications+           , TypeFamilies+           , TypeOperators+           , ViewPatterns+           , UndecidableInstances+#-}++{-# OPTIONS_GHC -fno-warn-orphans #-} -- Suppress orphan instance of Data instance of Binder ctxbody.++module Language.Nominal.Nom+   ( -- * The Nom monad+     -- $nom+       KNom (..), Nom+     -- * Creating a @'Nom'@+     , res, kres, resN, reRes +     -- * Destroying a @'Nom'@+     , unNom, nomToIO+     -- * Creating fresh ids in a @'Nom'@+     , freshKAtom, freshAtom, freshKAtoms, freshAtoms, freshKName, freshName, freshKNames, freshNames -- , atFresh+     -- * 'KNom' and other functors+     -- $functor+     , transposeNomF +     -- * Tests+     -- $tests+     , module Language.Nominal.SMonad+   )+   where++-- import Data.Data        hiding (typeRep, TypeRep)+-- import Data.Function    ((&))+-- import Data.Proxy+import Data.Type.Equality+import Type.Reflection+import Control.Applicative  -- for Alternative+import Control.Compose -- for :.+import System.IO.Unsafe (unsafePerformIO)+import Data.Functor+import GHC.Generics     hiding (Prefix) -- avoid clash with Data.Data.Prefix+-- import Flow             ((.>))++import Language.Nominal.Name+import Language.Nominal.NameSet+import Language.Nominal.SMonad+import Language.Nominal.Utilities+++-- * The Nom monad++{- $nom++Broadly speaking there are three kinds of functions involving 'KNom':++* 'KNom'-specific functions that may involve creating fresh atoms, but do not involve swappings.+* More general functions involving the 'Language.Nominal.Binder.Binder' typeclass (defined using 'KNom', and of which 'KNom' is the canonical instance).  These functions tend to impose 'Swappable' and 'Typeable' constraints on their type parameters.+* 'KNom'-specific functions in which, for various reasons (elegance, avoiding code duplication, necessity) we make use of both classes of functions above.++This file deals with the first class above.  The second and third are in "Language.Nominal.Binder".++/Remark: 'KNom' is more basic than 'Language.Nominal.Binder.Binder', though it's the canonical instance.  This creates a design tension: is a function on 'KNom' best viewed as a function directly on Nom, or as an instance of a more general function involving Binder?/++-}++++-- | Data in local @'KAtom' s@-binding context.+newtype KNom s a = Nom { getNom :: IO (XRes s a) -- ^ Recover a name-generating IO action from a 'KNom' binding.  If you execute one of these using 'unsafePerformIO', you get the data in @a@ (the /body/ of the binding), with some actual freshly-generated atoms.  See also 'unNom'.+                       }+   deriving (Generic)+   deriving (Functor, Applicative, Monad) via ViaSMonad (KNom s) +--   deriving (KSupport s) via BinderSupp (KNom s a) -- avoid forward dependency++-- | Swap goes under name-binders.+--+-- > swp n1 n2 (ns @> x) = (swp n1 n2 ns) @> (swp n1 n2 x)+instance (Typeable s, Swappable a) => Swappable (KNom s a) where+   kswp n1 n2 (Nom x) = Nom $ kswp n1 n2 <$> x++instance SMonad [KAtom s] (KNom s) where+    (>>+)  :: KNom s a -> ([KAtom s] -> a -> KNom s b) -> KNom s b+    (Nom a') >>+ cont = Nom $ do -- IO monad+        a <- a'+        let (atms0, a0) = exitWith (,) a +        let (Nom b') = cont atms0 a0+        iact atms0 <$> b' +    -- | Enters a name-binding context. +    --+    -- /Note: This is a low-level instruction.  It does not enforce capture-avoidance.  Only use it if you know what you're doing; if in doubt use @'res'@ instead, which is higher-level but cost typeclass assumptions)./+    enter :: [KAtom s] -> a -> KNom s a+    enter = Nom . return .: enter +    -- | Exits a name-binding context, using 'unsafePerformIO'. +    --+    -- /Note: This is a low-level instruction.  Only use it if you know what you're doing; if in doubt use @'unNom'@ or destructors from "Language.Nominal.Binder" instead, which are higher-level but cost typeclass assumptions./+    --+    -- /Note: This is our only use of 'unsafePerformIO'.  If a fresh ID got generated, then it came from here./+    exit :: KNom s a -> a+    exit = exit . unsafePerformIO . getNom ++-- | Data in a local atom-binding context at @'Tom'@s.+type Nom = KNom Tom+++instance (KSupport t a, Typeable s) => KSupport t (KNom s a) where+   ksupp p x' = unNom $ ksupp p <$> x' -- use of unNom garbage-collects restricted atoms++-- | 'KRestrict' @atms@ in @a@, inside 'KNom' monad.+instance {-# OVERLAPPING #-} (Typeable s, Swappable a) => KRestrict s (KNom s a) where+   restrict = (=<<) . res +instance {-# OVERLAPPABLE #-} (Typeable s, Swappable a, KRestrict t a) => KRestrict t (KNom s a) where+   restrict atms x' = case testEquality (typeRep :: (TypeRep t)) (typeRep :: (TypeRep s)) of+-- are s and t the same type?  (this should never trigger, because it should be captured by overlapping instance)+            Just Refl   -> x' >>= res atms +-- are s and t different types?+            Nothing     -> restrict atms <$> x'++-- | Alternatives are composed in a capture-avoiding manner+instance Alternative f => Alternative ((KNom s) :. f) where+   empty = O $ return empty+   a' <|> b' = O $ do -- Nom monad+      a <- unO a'+      b <- unO b'+      return $ a <|> b++++-- * Creating a 'KNom'++-- | Constructor for @'KNom' s@. +res :: (Typeable s, Swappable a) => [KAtom s] -> a -> KNom s a+res atms a = freshKAtoms atms <&> \atms' -> perm (zip atms' atms) a ++-- | Constructor for @'KNom' s@ (proxy version). +kres :: (Typeable s, Swappable a) => proxy s -> [KAtom s] -> a -> KNom s a+kres _ = res++-- | Make sure restricted atoms will alpha-convert to avoid capture, if e.g. they were created using 'enter' and not 'res'. +reRes :: (Typeable s, Swappable a) => KNom s a -> KNom s a+reRes = exitWith res ++-- | A version of 'res' on 'Nom' that takes names, not atoms (it just strips the labels of the names and acts on their atoms).+resN :: (Typeable s, Swappable a) => [KName s t] -> a -> KNom s a+resN = res . fmap nameAtom++++-- | Use this to safely exit a @'KNom'@ monad.+-- It works by binding the @KNom@-bound @s@-atoms using @a@'s native instance of @KRestrict@.  See "Language.Nominal.Examples.Tutorial" for examples.+--+-- > unNom = resAppC id+--+-- /Note: The less versions of 'unNom' are the 'exit' and 'exitWith' instances of 'KNom' as an instance of 'SMonad'.  See also 'Language.Nominal.Binder.@@'./ +unNom :: KRestrict s a => KNom s a -> a+unNom = exitWith restrict++-- | Another way to safely exit 'KNom': convert it to an IO action (the IO may generate fresh names) +nomToIO :: KNom s a -> IO a+nomToIO (Nom a') = exit <$> a' +++-- * Creating fresh ids in a @'Nom'@++-- | Create a fresh atom-in-nominal-context+freshKAtom :: Typeable s => KNom s (KAtom s)+freshKAtom = Nom $ do -- IO monad+   [a] <- freshKAtomsIO [()]+   return $ enter [a] a++-- | Canonical version for unit atoms sort.+freshAtom :: Nom Atom+freshAtom = freshKAtom++-- | Fresh @'Traversable' m@ of atoms (e.g. @m@ is list or stream)+freshKAtoms :: (Traversable m, Typeable s) => m t -> KNom s (m (KAtom s))+freshKAtoms = mapM (const freshKAtom)++-- | Fresh @'Traversable' m@ of atoms (e.g. @m@ is list or stream).+-- | 'Tom' instance.+freshAtoms :: Traversable m => m t -> Nom (m Atom)+freshAtoms = freshKAtoms++-- | Create a fresh name-in-a-nominal-context with label @t@+freshKName :: Typeable s => t -> KNom s (KName s t)+freshKName t = freshKAtom <&> Name t++-- | Create fresh names-in-a-nominal-context+freshKNames :: (Traversable m, Typeable s) => m t -> KNom s (m (KName s t))+freshKNames = mapM freshKName++-- | Canonical version of 'freshKName' for @'Tom'@ name.+freshName :: t -> Nom (Name t)+freshName = freshKName++-- | Canonical version of 'freshKNames' for @'Tom'@ names.+freshNames :: Traversable m => m t -> Nom (m (Name t))+freshNames = freshKNames++{-- +-- | atFresh f returns the value of f at a fresh name with label @t@+atFresh :: Typeable s => t -> (KName s t -> a) -> KNom s a+atFresh t f = freshKName t <&> f+--}++-- * 'KNom' and functors++{- $functor++There are three functions that will commute 'KNom' with some other 'f':++* 'transposeNomF'+* 'transposeMF'+* 'transposeFM'++Taken together, these functions are making a point that 'KNom' is compatible with your favourite container type.  Because 'KNom' can commuted, there is no need to wonder whether (for example) a graph-with-binding should be a graph with binding on the vertices, or on the edges, or on the graph overall, or any combination.  All of these are valid design decisions and one may be more /convenient/ than the other, but in the end we can isomorphically commute to a single top-level 'KNom' binding.++In that sense, 'KNom' captures a general theory of binding.+It is also a mathematical justification for why the 'Language.Nominal.Binder.Binder' typeclass turns out to be so useful.++-}+++-- | 'KNom' commutes down through functors.+--+-- 'transposeNomF' is a version of 'transposeMF' where bindings are have added capture-avoidance (for inverse, see 'transposeFM'). +transposeNomF :: (Functor f, Typeable s, Swappable a) => KNom s (f a) -> f (KNom s a)+transposeNomF = exitWith $ fmap . res +-- transposeNomFunc = exitWith $ fmap . enter +++-- * `Nom` and `Eq`++-- | Fresh names are generated when name contexts are opened for equality test+instance Eq a => Eq (KNom s a) where+   a1' == a2' = exit $ a1' >>= \a1 -> a2' >>= \a2 -> return $ a1 == a2+-- Rendering using 'Binder' machinery is possible, but adds forward dependencies and imposes typeclass condition:+-- instance (Typeable s, Swappable a, Eq a) => Eq (KNom s a) where+--   a1' == a2' = a1' @@. \_ a1 -> a2' @@. \_ a2 -> a1 == a2++-- | Show a nom by unpacking it+instance Show a => Show (KNom s a) where+    show = exitWith $ \atms a -> show atms ++ "." ++ show a+++{- $tests Property-based tests are in "Language.Nominal.Properties.NomSpec". -}
+ src/Language/Nominal/Properties/AbsSpec.hs view
@@ -0,0 +1,54 @@+module Language.Nominal.Properties.AbsSpec+     where++import Test.QuickCheck++import Language.Nominal.Name +import Language.Nominal.Nom+import Language.Nominal.Binder+import Language.Nominal.Abs+import Language.Nominal.Unify+import Language.Nominal.Properties.SpecUtilities ()++-- | @fuse a.x a.x' = a.(x,x')@+prop_fuse :: Name () -> [Name ()] -> [Name ()] -> Bool+prop_fuse n a b = fuse (abst n a, abst n b) == abst n (a,b)++-- | @n # x => [n](x @ n) = x@+prop_Abs_Conc :: Name () -> Abs () [Name ()] -> Property +prop_Abs_Conc n x = n `freshFor` x ==> (abst n (conc x n) === x) ++-- | @n' # x => [n]x = [n'](n' n).x@+prop_Abs_alpha :: Name () -> Name () -> [Name()] -> Property+prop_Abs_alpha n n' l = n' `freshFor` l ==> (abst n l === abst n' (swpN n' n l))++-- | @(n.x) \@ n = x@+prop_Conc_Abs :: Name () -> [Name ()] -> Property +prop_Conc_Abs n x = conc (abst n x) n === x++-- | @(n.x) \@ n' = (n' n).x@+prop_Conc_Abs_swap :: Name () -> Name () -> [Name ()] -> Property +prop_Conc_Abs_swap n n' x = n' `freshFor` x ==> conc (abst n x) n' === swpN n' n x++-- | Atm.(X x Y) iso Atm.X x Atm.Y, left-to-right-to-left+prop_fuse_unfuse_Abs :: Abs () ([Name ()], [Name ()]) -> Property +prop_fuse_unfuse_Abs x = (fuse . unfuse) x === x ++-- | Atm.(X x Y) iso Atm.X x Atm.Y, right-to-left-to-right+prop_unfuse_fuse_Abs :: (Abs () [Name ()], Abs () [Name ()]) -> Property +prop_unfuse_fuse_Abs (a, b) = (unfuse . fuse) (a, b) === (a, b) ++-- | Iso fails if atoms labelled, since one label lost Atm.X x Atm.Y -> Atm.(X x Y), and one label invented if list empty +prop_unfuse_fuse_Abs' :: (Abs Int [Name Int], Abs Int [Name Int]) -> Property +prop_unfuse_fuse_Abs' (a, b) = expectFailure ( (unfuse . fuse) (a, b) === (a, b) )++-- | Atm.X iso Nom (Atm x X)+prop_abs_to_nom :: Abs Int [Name Int] -> Bool+prop_abs_to_nom x' = x' == nomToAbs (absToNom x')++-- | Nom (Atm x X) iso Atm.X.  +--+-- Note: We have to use unifiability because of local scope.+prop_nom_to_abs :: Nom (Name Int, [Name Int]) -> Bool +prop_nom_to_abs x' = unifiablePerm x' (absToNom (nomToAbs x'))+
+ src/Language/Nominal/Properties/AllTests.hs view
@@ -0,0 +1,46 @@+{-|+Module      : Tests for nominal package +Description : Implementation of nominal techniques as a Haskell package, tests +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Nominal-flavoured implementation of data in a context of local names, designed following the ideas in <https://link.springer.com/article/10.1007/s001650200016 a new approach to abstract syntax with variable binding> (see also <http://www.gabbay.org.uk/papers.html#newaas-jv author's pdfs>).++Run tests by ++- typing @stack ghci AllTests@ from the command line in the directory containing @AllTests.hs@, then typing @quickcheck prop_name@ from the Haskell prompt, or +- by typing @stack test@ from the command line (e.g. in the root directory of this package). ++-}++-- {-# LANGUAGE TemplateHaskell       #-}  -- needed for QuickCheck test generation+{-# OPTIONS_GHC -Wno-unused-imports #-}  -- suppress warnings of unused imports; intended here++module Language.Nominal.Properties.AllTests+    where++import Language.Nominal.Name +import Language.Nominal.Nom +import Language.Nominal.Sub +import Language.Nominal.Abs +import Language.Nominal.Examples.SystemF  +import Language.Nominal.Properties.SpecUtilities  +import Language.Nominal.Properties.NameSpec +import Language.Nominal.Properties.NomSpec +import Language.Nominal.Properties.AbsSpec +import Language.Nominal.Properties.Examples.SystemFSpec ++import Test.QuickCheck ++-- mjg to update++-- import Test.QuickCheck.All++{--------------------------+return []+runTests :: IO Bool+runTests = $quickCheckAll+-}
+ src/Language/Nominal/Properties/EquivarSpec.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE PolyKinds           #-}++-- {-# OPTIONS_GHC -Wno-orphans #-}+++module Language.Nominal.Properties.EquivarSpec+    where++import Language.Nominal.Name +import Language.Nominal.Equivar++-- | Only one orbit of atoms +prop_atoms_one_orbit :: [Name ()] -> Bool+prop_atoms_one_orbit [] = length (evRep ([] :: [Name Int])) == 0+prop_atoms_one_orbit l  = length (evRep l)  == 1++-- | Two orbits of atom pairs (equal, or disjoint) +prop_atomssq_orbit :: [(Name (),Name ())] -> Bool+prop_atomssq_orbit l  = length (evRep l) <= 2++-- TODO: more tests+
+ src/Language/Nominal/Properties/Examples/IdealisedEUTxOSpec.hs view
@@ -0,0 +1,386 @@+{-| +__Please read the source code to view the tests.__+-}+{-# LANGUAGE ConstraintKinds        #-}+{-# LANGUAGE DeriveGeneric          #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE GADTs                  #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+{-# LANGUAGE RankNTypes             #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeSynonymInstances   #-}+{-# LANGUAGE UndecidableInstances   #-}++{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++module Language.Nominal.Properties.Examples.IdealisedEUTxOSpec+    where++import Control.Monad                              (replicateM)+import Data.List.NonEmpty                         (NonEmpty (..))+import Data.Maybe                                 (fromJust, isJust)+import Data.Proxy                                 (Proxy (..))+import qualified Data.Set as S +import GHC.Generics+import Numeric.Partial.Semigroup+import Numeric.Partial.Monoid+import Test.QuickCheck+import Type.Reflection                           ++import Language.Nominal.Examples.IdealisedEUTxO+import Language.Nominal.NameSet+import Language.Nominal.Properties.SpecUtilities  (genEvFinMap)+import Language.Nominal.Properties.UnifySpec      ()+import Language.Nominal.Unify+import Language.Nominal.Equivar+import Language.Nominal.Nom+import Language.Nominal.Binder++instance Arbitrary r => Arbitrary (Input r) where+    arbitrary = Input <$> arbitrary <*> arbitrary+    shrink (Input p r) = Input p <$> shrink r -- only shrinking the redeemer, not the position++instance Arbitrary (ValTriv r d) where+    arbitrary = return ValTriv+    shrink = const []++instance (Eq r, UnifyPerm r, Arbitrary r, Eq d, UnifyPerm d, Arbitrary d) => Arbitrary (ValFin r d) where+    arbitrary = ValFin <$> genEvFinMap (scale (`div` 3) arbitrary) arbitrary+    shrink (ValFin f) = ValFin <$> shrink f++instance (Arbitrary d, Arbitrary v) => Arbitrary (Output d v) where+    arbitrary = Output <$> arbitrary <*> arbitrary <*> arbitrary+    shrink (Output p d v) =+           (Output p d <$> shrink v)             -- shrink the validator+        ++ ((\d' -> Output p d' v) <$> shrink d) -- shrink the datum++instance (Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (Transaction r d v) where++    arbitrary = Transaction <$> arbitrary <*> arbitrary++    shrink (Transaction is os) =+           (Transaction is <$> shrink os)+        ++ (flip Transaction os <$> shrink is)++instance (Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (Context r d v) where+    arbitrary = Transaction <$> arbitrary <*> arbitrary++newtype ValidTx r d v = ValidTx (Transaction r d v) deriving (Show, Generic)++fromValidTx :: ValidTx r d v -> Transaction r d v+fromValidTx (ValidTx tx) = tx++instance (Arbitrary r, Arbitrary d, Arbitrary v) => Arbitrary (ValidTx r d v) where++    arbitrary = do+        tx <- arbitrary+        return $ ValidTx $ go [tx]+      where+        go []                     = Transaction [] []+        go (tx : txs)+            | transactionValid tx = tx+            | otherwise           = go $ take 10 $ txs ++ shrink tx++    shrink (ValidTx tx) = ValidTx <$> shrink tx++instance ( Arbitrary r+         , Support r+         , Arbitrary d+         , Support d+         , Arbitrary v+         , Validator r d v+         ) => Arbitrary (Chunk r d v) where+    arbitrary = sized $ \size -> do+        l <- choose (0, min limit size)+        scale (min limit) $ go l+      where+        go :: Int -> Gen (Chunk r d v)+        go 0    = return pzero+        go l = do+            valids <- replicateM 5 $ scale (min limit) arbitrary+            chunk  <- go $ pred l+            go' valids chunk++        go' [] chunk = return chunk+        go' (ValidTx tx : txs) chunk = do+            let c  = unsafeSingletonChunk tx+            let c1 = padd c chunk+                c2 = padd chunk c+            case (c1, c2) of+                (Just chunk', _)           -> return chunk'+                (Nothing    , Just chunk') -> return chunk'+                (Nothing    , Nothing)     -> go' txs chunk++        limit :: Int+        limit = 15++    shrink = const [] -- TODO: We need something better here++newtype SmallChunk r d v = SmallChunk (Chunk r d v)+    deriving Show++instance Arbitrary (Chunk r d v) => Arbitrary (SmallChunk r d v) where+    arbitrary = SmallChunk <$> scale (min 7) arbitrary+    shrink (SmallChunk ch) = SmallChunk <$> shrink ch++class Validator r d v => Fixable r d v | v -> r d where+    -- | Takes a context and an output and modifies the output such that it can be consumed by the context.+    fixOutput :: Context r d v -> Output d v -> Output d v++instance (Support r, Support d) => Fixable r d (Val r d) where  ++    fixOutput (Transaction (Input p _ :| _) _) (Output _ d _) =+        Output p d $ Val $ EvFun $ const True++instance (Eq r, UnifyPerm r, Eq d, UnifyPerm d) => Fixable r d (ValFin r d) where+    fixOutput c@(Transaction (Input p _ :| _) _) (Output _ d (ValFin f)) =+          Output p d (ValFin $ extEvFinMap (d, c) True f) ++instance (Support r, Support d) => Fixable r d (ValTriv r d) where+    fixOutput (Transaction (Input p _ :| _) _) (Output _ d v) = Output p d v+++fixChunkToBlockchain :: (Arbitrary d, Arbitrary v, Fixable r d v) +   => Chunk r d v -> Gen (Blockchain r d v) +fixChunkToBlockchain chunk +   | isBlockchain chunk = return $ blockchain chunk+   | otherwise = do -- Gen monad +       -- get the utxcs of the chunk, still in a Nom binding+       let utxcsCh' = utxcsOfChunk chunk+       -- generate an arbitrary output for each utxc /first/ +       os' <- replicateM (resAppC length utxcsCh') arbitrary -- :: Gen (Output d v) +       -- and only /then/ unpack the list of utxcs.  Fresh atoms generated are for input-output bindings and should not interfere with atoms in os' +       let cs = exit $ utxcsCh' +       -- fix each output so it matches the relevant utxc.+       let os = map (uncurry fixOutput) (zip cs os')  +       -- make genesis block+       let genesis = unsafeSingletonChunk (Transaction [] os)+       -- add it to the chunk and parcel it up as a blockchain+       -- genesis block is on the right because lists grow from right-to-left in Haskell +       return . blockchain . fromJust $ chunk `padd` genesis ++instance ( Arbitrary r+         , Support r +         , Arbitrary d+         , Support d+         , Arbitrary v+         , Fixable r d v+         ) => Arbitrary (Blockchain r d v) where+    arbitrary = arbitrary >>= fixChunkToBlockchain ++    shrink = const [] -- TODO: We need something better here+++-- Tests++-- TODO: two ways to combine different validator types in one property, one lightweight, one more heavy-handed:+-- Given prop_chunkrefl below, you can either manually (or in the actual test suite) do+--+-- quickCheck $ prop_chunkrefl atVal+-- quickCheck $ prop_chunkrefl atValFin+--+-- If you want to automate this, you can use the ValProxy-machinery above, so by doing+--+-- quickCheck $ withVal (property . prop_chunkrefl)+--+-- a random validator type will be picked for each test. We could extend this to include more different validator types+-- and also to include types for redeemers and/or datum if we want.++{-- Types 1+type TR = () +type TD = () +type TV = ValTriv TR TD +--}++-- Types 2 +type TR = Int  +type TD = Int   +type TV = ValFin TR TD+--++type TC = Chunk TR TD TV+type SmallTC = SmallChunk TR TD TV+type TB = Blockchain TR TD TV+type TX = ValidTx TR TD TV++type TC' v = Chunk TR TD v++atValTriv :: Proxy (ValTriv TR TD)+atValTriv = Proxy++atValFin :: Proxy (ValFin TR TD)+atValFin = Proxy++type CVal v = (Typeable v, Show v, Arbitrary v, UnifyPerm v, Validator TR TD v)++data ValProxy where+    ValProxy :: CVal v => Proxy v -> ValProxy    ++instance Show ValProxy where+    show (ValProxy (Proxy :: Proxy v)) = "{" ++ show (typeRep :: TypeRep v) ++ "}"++instance Arbitrary ValProxy where+    arbitrary = elements [ValProxy atValTriv, ValProxy atValFin]+    shrink = const []++valTriv, valFin :: ValProxy+valTriv = ValProxy atValTriv+valFin = ValProxy atValFin++withVal :: (forall v proxy. CVal v => proxy v -> a) -> ValProxy -> a+withVal f (ValProxy p) = f p++-- | Sanity check: every arbitrary chunk is indeed a valid chunk.+prop_arbitraryChunkIsValid :: TC -> Bool+prop_arbitraryChunkIsValid = isChunk++-- | Sanity check: every arbitrary chunk is indeed a valid chunk (alternate test).+prop_arbitraryChunkIsValid' :: TC -> Bool+prop_arbitraryChunkIsValid' = isChunk'++-- | Sanity check: every arbitrary chunk is equal to itself (not trivial because 'Eq' instance is nontrivial)+prop_arbitraryChunkEqCheck :: TC -> Bool+prop_arbitraryChunkEqCheck ch = ch == ch+++-- | Sanity check: not every chunk is a blockchain (might have UTxIs)! +prop_notEveryChunkBlockchain :: TC -> Property +prop_notEveryChunkBlockchain c = expectFailure $ isBlockchain c+++-- | Sanity check: an arbitrary transaction is indeed a valid transaction.+prop_arbitraryTxIsValid :: TX -> Bool+prop_arbitraryTxIsValid = transactionValid . fromValidTx++-- | Sanity check: an arbitrary blockchain is indeed a valid blockchain.+prop_arbitraryBlockchainIsValid :: TB -> Bool+prop_arbitraryBlockchainIsValid = isBlockchain . getBlockchain+++-- | Sanity check: arbitrary instance of TB generates a blockchain, which is equal to itself.+--+-- /'unifiablePerm' must be used here, because of the local scope./ +prop_blockchainToChunkAndBack :: TB -> Bool+prop_blockchainToChunkAndBack b = (blockchain . getBlockchain $ b) `unifiablePerm` b++-- | Blockchain has no UTxIs+prop_blockchainHasNoUTxIs :: TB -> Bool +prop_blockchainHasNoUTxIs b = null . utxisOfChunk . getBlockchain $ b++-- | Chunk is equal to itself+prop_chunkrefl :: CVal v => proxy v -> TC' v -> Bool +prop_chunkrefl _ ch = ch == ch  -- chunk equality goes through @'chunkEq'@++-- | There are two different chunks+prop_chunkneq :: TC -> TC -> Property +prop_chunkneq ch ch' = expectFailure $ ch == ch'++-- | Empty chunk is prefix of any chunk+prop_emptyIsPrefix :: TC -> Bool+prop_emptyIsPrefix ch = isPrefixChunk (return pzero) ch ++-- | The tail of a chunk, is a chunk.+prop_chunkTail_is_chunk :: TC -> Property +prop_chunkTail_is_chunk ch = chunkLength ch > 0 ==> isJust $ chunkTail ch++-- | The tail of a chunk, is a prefix of the original chunk.+prop_chunkTail_is_prefix :: TC -> Property +prop_chunkTail_is_prefix ch = chunkLength ch > 0 ==> isPrefixChunk (fromJust $ chunkTail ch) ch ++-- | The tail of a chunk, generating fresh atoms if required +genChunkTail :: (UnifyPerm r, UnifyPerm d, UnifyPerm v, Validator r d v) => Chunk r d v -> Maybe (Chunk r d v)+genChunkTail = fmap exit . chunkTail ++-- | The tail of a chunk, is a prefix of the original chunk.  Gotcha version, that doesn't have the Nom bindings: expect failure here.+prop_chunkTail_is_prefix_gotcha :: TC -> Property +prop_chunkTail_is_prefix_gotcha ch = expectFailure $ chunkLength ch > 0 ==> isPrefixChunk (return . fromJust $ genChunkTail ch) ch ++-- | Plausible-but-wrong @'warningNotChunkTail'@ is wrong: expect failure here. +prop_warningNotChunkTail_is_not_chunk :: TC -> Property +prop_warningNotChunkTail_is_not_chunk ch = expectFailure $ chunkLength ch > 0 ==> fromJust $ isChunk <$> warningNotChunkTail ch+-- prop_warningNotChunkTail_is_not_chunk ch = expectFailure $ chunkLength ch > 0 ==> (isJust . nomTxListToChunk) ((chunkToTxList . fromJust . warningNotChunkTail) ch)++-- | /Underbinding/ is when not enough atoms are bound in a chunk +prop_underbinding :: TC -> Property+prop_underbinding ch = expectFailure $ isChunk $ ch @@! \_ txs -> Chunk (return txs) ++-- | /Overbinding/ is when too many atoms are bound in a chunk +prop_overbinding :: TC -> Property+prop_overbinding ch = expectFailure $ isChunk $ restrict (S.toList $ supp ch) ch ++-- | Gotcha: Fails because loss of information from two Nom bindings.+prop_chunkHead_chunkTail_recombine :: TC -> Property+prop_chunkHead_chunkTail_recombine ch = expectFailure $ chunkLength ch > 0 ==> unNom $ do -- Nom monad+   h <- fromJust $ chunkHead ch+   t <- fromJust $ chunkTail ch+   return $ Just ch == appendTxChunk h t++-- | Succeeds because one Nom binding thus no loss of information. +prop_chunkHdTl_recombine :: TC -> Property+prop_chunkHdTl_recombine ch = chunkLength ch > 0 ==> unNom $ do -- Nom monad+   (tx,ch') <- fromJust $ chunkToHdTl ch+   return $ Just ch == appendTxChunk tx ch' ++{- prop_chunkTailIsPrefix :: TC -> Property +prop_tailIsPrefix ch = +    let mt = chunkTail ch+    in isJust mt ==> isPrefixChunk (fromJust mt) ch +-}+{- prop_tailIsPrefix :: TC -> Property +prop_tailIsPrefix ch = +    let mt = chunkTail ch+    in isJust mt ==> unNom $ isPrefixChunk (fromJust mt) ch +-}++-- | If you reverse the order of transactions in a chunk, it need not be valid+prop_reverseIsNotValid :: TC -> Property +prop_reverseIsNotValid ch = expectFailure $ isJust (reverseTxsOf ch) ++prop_subchunksValid :: SmallChunk TR TD TV -> Bool +prop_subchunksValid (SmallChunk ch) = and . unNom $ map (isJust . txListToChunk) <$> (subTxListOf ch) +-- also subchunk and composition interact++-- | If two transactions are apart, they can be validly combined. +-- | Corresponds to Lemma 2.14(1) of <https://arxiv.org/pdf/2003.14271.pdf UTxO- vs account-based smart contractblockchain programming paradigms>.+prop_apart_is_valid_tx :: TX -> TX -> Bool +prop_apart_is_valid_tx vtx1 vtx2 = unNom $ do -- Nom monad+      let [tx1, tx2] = fromValidTx <$> [vtx1, vtx2]+      tx2' <- freshen tx2+      return . isJust $ txListToChunk [tx1, tx2']  ++-- | If two chunks are apart, they can be validly combined. +-- | Extends Lemma 2.14(1) of <https://arxiv.org/pdf/2003.14271.pdf UTxO- vs account-based smart contractblockchain programming paradigms>.+prop_apart_is_valid_ch :: TC -> TC -> Bool +prop_apart_is_valid_ch ch1 ch2 = unNom $ do -- Nom monad+      ch2' <- freshen ch2+      return . isJust $ (Just ch1) <> (Just ch2')+++-- A helper to observe equivalence of chunks+observe :: Maybe TC -> Maybe TC -> Maybe TC -> Bool+observe mch1 mch2 mch3 =+     isJust (mch3 <> mch1) == isJust (mch3 <> mch2) +   &&+     isJust (mch1 <> mch3) == isJust (mch2 <> mch3) ++-- | If two chunks are apart, they can be validly commuted. +-- | Extends Lemma 2.14(1) of <https://arxiv.org/pdf/2003.14271.pdf UTxO- vs account-based smart contractblockchain programming paradigms>.+-- We use smaller chunks for speed.+prop_chunk_apart_commutes :: SmallTC -> SmallTC -> SmallTC -> Bool +prop_chunk_apart_commutes (SmallChunk ch1) (SmallChunk ch2) (SmallChunk ch3) = unNom $ do -- Nom monad+      ch2' <- freshen ch2+      return $ observe ((Just ch1) <> (Just ch2'))+                       ((Just ch2') <> (Just ch1)) +                       (Just ch3) ++-- | This corresponds to a key result, Lemma 2.14(2) of <https://arxiv.org/pdf/2003.14271.pdf UTxO- vs account-based smart contractblockchain programming paradigms>.+prop_validity_fresh :: TC -> Property+prop_validity_fresh ch = chunkLength ch > 1 ==> unNom $ do -- Nom monad+   (tx1, tx2, ch') <- fromJust $ chunkToHdHdTl ch+   let mch2 = appendTxChunk tx1 ch' +   return $ (isBlockchain ch && isBlockchain' mch2) <= (tx1 `apart` tx2) + +
+ src/Language/Nominal/Properties/Examples/SystemFSpec.hs view
@@ -0,0 +1,110 @@+{-| +__Please read the source code to view the tests.__+-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE FlexibleContexts #-}++module Language.Nominal.Properties.Examples.SystemFSpec+    where++import Data.Maybe+import Test.QuickCheck+import Type.Reflection                   (Typeable)++import Language.Nominal.Name +import Language.Nominal.Binder+import Language.Nominal.Sub+import Language.Nominal.Examples.SystemF++-- * Substitution++-- | y[n-> var n] = y+iprop_sub_id :: (KSub ntyp x y, Eq y) => (ntyp -> x) -> ntyp -> y -> Bool +iprop_sub_id f n y = y == sub n (f n) y+prop_sub_id_typevar' :: NTyp -> Typ -> Bool +prop_sub_id_typevar' = iprop_sub_id TVar +prop_sub_id_termvar :: NTrm -> Trm -> Bool +prop_sub_id_termvar = iprop_sub_id Var+prop_sub_id_typevar :: NTyp -> Trm -> Bool +prop_sub_id_typevar = iprop_sub_id TVar+++-- | n # y => y[n->x] = y+iprop_sub_fresh :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => KName s n -> x -> y -> Property +iprop_sub_fresh n x y = n `freshFor` y ==> (y === sub n x y)+prop_sub_fresh_typevar' :: NTyp -> Typ -> Typ -> Property +prop_sub_fresh_typevar' = iprop_sub_fresh +prop_sub_fresh_typevar :: NTyp -> Typ -> Trm -> Property +prop_sub_fresh_typevar = iprop_sub_fresh +prop_sub_fresh_termvar :: NTrm -> Trm -> Trm -> Property +prop_sub_fresh_termvar = iprop_sub_fresh ++-- | n' # y => y[n->n'] = (n' n).y+iprop_sub_perm :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => (KName s n -> x) -> KName s n -> KName s n -> y -> Property +iprop_sub_perm f n n' y = +   n' `freshFor` y ==> sub n (f n') y === kswpN n' n y+prop_sub_perm_typevar' :: NTyp -> NTyp -> Typ -> Property +prop_sub_perm_typevar' = iprop_sub_perm TVar +-- this one trapped an error+prop_sub_perm_typevar'' :: NTyp -> NTyp -> Trm -> Property +prop_sub_perm_typevar'' = iprop_sub_perm TVar +prop_sub_perm_termvar :: NTrm -> NTrm -> Trm -> Property +prop_sub_perm_termvar = iprop_sub_perm Var +++-- * Typing and reduction++-- | (id id) has no type (it needs a type argument)+prop_untypeable :: Bool +prop_untypeable = isNothing $ typeOf (App idTrm idTrm) ++-- | Not all terms are typeable+prop_all_typeable :: Trm -> Property +prop_all_typeable t = expectFailure $ typeable t +++prop_typeable_nf :: Trm -> Property+prop_typeable_nf t = typeable t ==> normalisable t++prop_nf_typeable :: Trm -> Property+prop_nf_typeable t = normalisable t ==> typeable t++-- | Type soundness+-- If a term is typeable and normalisable then its normal form has the same type as it does. +prop_type_soundness :: Trm -> Property +prop_type_soundness t = typeable t ==> normalisable t ==> (typeOf t === (typeOf =<< nf t))++-- | typeof(id t) = typeof(t)+prop_id_type_unchanged :: Trm -> Property +prop_id_type_unchanged t = typeable t ==> typeOf t === typeOf (App (TApp idTrm (typeOf' t)) t)++-- | If x : t then (id t x) --> x+prop_app_id :: Trm -> Property +prop_app_id t = typeable t ==> nf' t === nf' (App (TApp idTrm (typeOf' t)) t)++{-- prop_typeable_sub :: Name NTrmLabel -> Trm -> Trm -> Property+prop_typeable_sub n t1 t2 = typeable t1 ==> typeable t2 ==> typeable $ sub n t1 t2 --}++{-- prop_typeable_sub' :: Name NTrmLabel -> Trm -> Trm -> Property+prop_typeable_sub' n t1 t2 = typeable t1 ==> typeable t2 ==> ((typeOf' t2) === (typeOf' (sub n' t1 t2))) where +   n' = nameOverwriteLabel (Just ("",typeOf' t1)) n --}++-- * Church numerals++-- | 0 : nat+prop_typeof_zero :: Bool+prop_typeof_zero = typeOf zero == Just nat++-- | i+1 /= 0 +prop_church_numerals0 :: NonNegative Int -> Bool+prop_church_numerals0 (NonNegative i) = church (i + 1) /= zero++-- | i+1 /= i +prop_church_numerals1 :: NonNegative Int -> Bool+prop_church_numerals1 (NonNegative i) = church (i + 1) /= church i ++-- | i : nat+prop_church_numerals_type :: NonNegative Int -> Bool+prop_church_numerals_type (NonNegative i) = typeOf (church i) == Just nat+
+ src/Language/Nominal/Properties/NameSetSpec.hs view
@@ -0,0 +1,21 @@+module Language.Nominal.Properties.NameSetSpec+    where++import qualified Data.List.Extra as L+import           Test.QuickCheck++import           Language.Nominal.Name +import           Language.Nominal.NameSet+-- import           Language.Nominal.Properties.SpecUtilities++-- ns disjoint ns', if apart +prop_supp_apart :: [Name Bool] -> [Name Bool] -> Property +prop_supp_apart ns ns' = (take 4 ns `apart` take 4 ns') ==> take 4 ns `L.disjoint` take 4 ns'  -- restrict length so tests don't give up++-- ns disjoint ns' iff apart, if triv labels +prop_supp_apart_atom :: [Name ()] -> [Name ()] -> Bool +prop_supp_apart_atom ns ns' = (ns `apart` ns') == ns `L.disjoint` ns'++{-- supp([[a]]) = supp(unions [a])+prop_supp_unions :: [[Name Int]] -> Bool +prop_supp_unions l = supp (S.unions --}
+ src/Language/Nominal/Properties/NameSpec.hs view
@@ -0,0 +1,58 @@+module Language.Nominal.Properties.NameSpec+     where++import Test.QuickCheck++import Language.Nominal.Name+-- import Language.Nominal.Nom+import Language.Nominal.Binder++-- $setup+-- >>> :set -XScopedTypeVariables+-- >>> import Test.QuickCheck+-- >>> import Language.Nominal.Properties.SpecUtilities++-- | @'withLabel'@ does indeed overwrite the label.+--+-- prop> \(n :: Name String) t -> nameLabel (n `withLabel` t) == t+--+prop_namelabel :: Name String -> String -> Bool+prop_namelabel n t = t == nameLabel (n `withLabel` t) ++-- | Not all names are equal (even with trivial labels)+prop_twonames :: Name () -> Name () -> Property +prop_twonames n1 n2 = +   expectFailure $ n1 == n2++-- | (n' n).x = x  (we expect this to fail)+prop_singleswap :: Name String -> Name String -> [Name String] -> Property +prop_singleswap n1 n2 l = +   expectFailure $ swpN n1 n2 l == l++-- | n',n#x => (n' n).x = x.  Test on x a tuple.+prop_freshswap :: Name String -> Name String -> (Name String, Name String, Name String) -> Property+prop_freshswap n1 n2 l = +   n1 `freshFor` l ==> n2 `freshFor` l ==> +      swpN n1 n2 l == l++-- | (n' n).(n' n).x = x  +prop_doubleswap :: Name String -> Name String -> [Name String] -> Bool+prop_doubleswap n1 n2 l = +   swpN n1 n2 (swpN n1 n2 l) == l++-- | n'',n'#x => (n'' n').(n' n).m = (n'' n).m  +prop_doubleswap_fresh' :: Name String -> Name String -> Name String -> Name String -> Property +prop_doubleswap_fresh' n n' n'' m = +   n' `freshFor` m ==> n'' `freshFor` m ==> +      swpN n'' n' (swpN n' n m) === swpN n'' n m++-- | n'#x => (n'' n').(n' n).x = (n'' n).x  +prop_doubleswap_fresh :: Name String -> Name String -> Name String -> [Name String] -> Property +prop_doubleswap_fresh n n' n'' l = +   n' `freshFor` l ==> n'' `freshFor` l ==> +      swpN n'' n' (swpN n' n l) === swpN n'' n l++-- | (n' n).x = (n n').x+prop_swap_symm :: Name String -> Name String -> [Name String] -> Bool+prop_swap_symm n' n x = swpN n' n x == swpN n n' x+
+ src/Language/Nominal/Properties/NomSpec.hs view
@@ -0,0 +1,162 @@+{-# LANGUAGE FlexibleContexts      #-}  -- for non-type variable argument in constraint, namely Support and Swappable+{-# LANGUAGE DataKinds             #-}  -- for Tom+{-# LANGUAGE ScopedTypeVariables   #-}++module Language.Nominal.Properties.NomSpec+    where++import Data.Function   (on, (&))+import Data.Set        as S+import Data.Default+import Data.List.Extra as LE+import Test.QuickCheck++import Language.Nominal.Name+import Language.Nominal.NameSet+import Language.Nominal.Nom+import Language.Nominal.Binder+-- import Language.Nominal.Unify+import Language.Nominal.Properties.SpecUtilities ()++-- | Nom creates local binding, which is unpacked separately by equality.  Cf. `UnifySpec` to see how this can be addressed.+prop_x_neq_x :: Nom [Name Int] -> Property+prop_x_neq_x x = expectFailure $ x == x++-- | Check restriction creates local scope.+-- Should return False.+prop_split_scope :: Name String -> Bool+prop_split_scope n = unNom $ do -- Nom monad+   let (x1,x2) = (resN [n] n, resN [n] n) -- create two scopes+   y1 <- x1                             -- unpack them+   y2 <- x2+   return $ y1 /= y2                    -- check for equality++-- | n' # n if n' is chosen fresh, after n+prop_fresh_neq :: Name () -> Bool+prop_fresh_neq n = unNom $ do -- Nom monad+   n' <- freshName ()+   return $ n /= n'++-- | @freshName () /= freshName ()@  Lazy evaluation means distinct fresh names generated.+prop_fresh_neq' :: Bool+prop_fresh_neq' = let x = freshName () in x /= x++-- | Same thing using @let@.+prop_fresh_neq'' :: Bool+prop_fresh_neq'' = let x = exit (freshName ()) in x == x++-- | But if we unpack a single fresh name monadically, we can compare it for equality.+prop_fresh_eq :: Bool+prop_fresh_eq =+   let x' = freshName () in+   unNom $ do -- Nom monad+      x <- x'+      return $ x == x+++-- | @~ (n # (n,n'))@+prop_freshFor1 :: Name () -> Name () -> Bool+prop_freshFor1 n n' = not $ n `freshFor` (n,n')++-- | @n # n'@+prop_freshFor2 :: Name () -> Bool+prop_freshFor2 n = unNom $ do -- Nom monad+   n' <- freshName ()+   return $ n `freshFor` n'++-- | Nom Maybe -> Maybe Nom -> Nom Maybe = id+prop_transposeNomMaybe :: Nom (Maybe [Name Int]) -> Bool+prop_transposeNomMaybe x' = unNom $ do -- Nom monad+    l1' <- x'  -- Maybe get a list of names+    l2' <- transposeFM (transposeMF x') -- Maybe get another list of names (freshening means the atoms will be different)+    -- l2' <- transposeTraversableNom (transposeNomFunc x') -- Maybe get another list of names (freshening means the atoms will be different)+    return $ ((==) `on` fmap (fmap nameLabel)) l1' l2' -- first fmap for Maybe, second for list++-- | Maybe Nom -> Nom Maybe -> Nom Maybe = id+prop_transposeMaybeNom :: Maybe (Nom [Name Int]) -> Bool+prop_transposeMaybeNom x' =+    let y' = transposeMF (transposeFM x')+    -- let y' = transposeNomFunc (transposeTraversableNom x')+    in  case (x', y') of+            (Nothing,  Nothing)  -> True+            (Just l1', Just l2') -> unNom $ ((==) `on` fmap nameLabel) <$> l1' <*> l2' -- fmap is for list, <$> <*> is for Nom+            _                    -> False+++-- a,b#x |- (a b).x = x+prop_new' :: [Name Int] -> Bool+prop_new' l = (new :: Int -> (Name Int -> Bool) -> Bool) def $ \a -> new def $ \b -> (swpN a b l) == l++-- a#x |/- (a b).x = x (cf. 'Language.Nominal.Properties.NameSpec.prop_singleswap')+prop_not_new' :: [Name Int] -> Name Int -> Property+prop_not_new' l b = expectFailure $ new def $ \a -> (swpN a b l) == l++-- a,b#x |- (a b).x = x+prop_new :: Int -> Int -> [Name Int] -> Bool+prop_new ta tb l = (new :: Int -> (Name Int -> Bool) -> Bool) ta $ \a -> new tb $ \b -> (swpN a b l) == l++-- n#l iff n not in l, for n a name and l a list of names+prop_freshFor_notElem :: Name () -> [Name ()] -> Bool+prop_freshFor_notElem n ns = not (n `elem` ns) == (n `freshFor` ns)++-- atoms-restriction precisely removes atoms from support+iprop_support_nom :: forall a. (Support a, Swappable a) => [Atom] -> a -> Bool+iprop_support_nom atms a = supp ((atms @> a) :: Nom a) == (supp a) S.\\ (S.fromList atms)++prop_support_nom_atmlist :: [Atom] -> [Atom] -> Bool+prop_support_nom_atmlist = iprop_support_nom++prop_support_nom_nomatmlist :: [Atom] -> Nom [Atom] -> Bool+prop_support_nom_nomatmlist = iprop_support_nom++-- if we freshen all atoms in an element, its support is apart from the original+iprop_freshen_apart :: (Support a, Swappable a) => a -> Bool+iprop_freshen_apart a = unNom $ (kfreshen atTom a) >>= \a' -> return $ a' `apart` a++prop_freshen_apart_atmlist :: [Atom] -> Bool+prop_freshen_apart_atmlist = iprop_freshen_apart++prop_freshen_apart_nom_atmlist :: Nom [Atom] -> Bool+prop_freshen_apart_nom_atmlist = iprop_freshen_apart++-- a freshened list of atoms is disjoint from its original+prop_freshen_apart_disjoint :: [Atom] -> Bool+prop_freshen_apart_disjoint as = unNom $ (freshen as) >>= \as' -> return $ as' `LE.disjoint` as++-- two notions of trivial Nom binding are equal, on a type with both Support and Swappable+Eq+prop_isTrivial_equal :: Nom [Atom] -> Bool+prop_isTrivial_equal x = isTrivialNomBySupp x == isTrivialNomByEq x++-- isTrivial sanity check (supp version)+prop_isTrivial_sane :: Nom [Atom] -> Property+prop_isTrivial_sane x = expectFailure $ isTrivialNomBySupp x++-- isTrivial sanity check (freshFor version)+prop_isTrivial_sane' :: Nom [Atom] -> Property+prop_isTrivial_sane' x = expectFailure $ isTrivialNomByEq x+++deBruijnAcc :: KNom s a -> (KAtom s -> b) -> b -> (a, KAtom s -> b)+deBruijnAcc a' f b = exitWith (\atms a -> (a, \atm -> if (atm `elem` atms) then b else f atm)) a'  +-- deBruijnAcc a' f b = (exitWith (,) a') & \(atms, a) -> (a, \atm -> if (atm `elem` atms) then b else f atm)++deBruijn1 :: Functor f => KNom s (f (KAtom s)) -> f Int+deBruijn1 a' = (deBruijnAcc a' (\_ -> 0) 1) & \(a, f) -> f <$> a++deBruijn2 :: Functor f => KNom s (KNom s (f (KAtom s)))-> f Int+deBruijn2 a'' = (deBruijnAcc a'' (\_ -> 0) 1) & \(a', f') -> (deBruijnAcc a' f' 2) & \(a, f) -> f <$> a++-- | Commute Nom and List+prop_transposeNomList :: Nom [Atom] -> Property+prop_transposeNomList x' = deBruijn1 x' === deBruijn1 (transposeFM (transposeMF x'))+-- prop_transposeNomList x' = deBruijn1 x' === deBruijn1 (transposeTraversableNom (transposeNomFunc x'))++-- | Commute Nom and Nom (one way)+prop_transposeNomNom :: Nom (Nom [Atom]) -> Property+prop_transposeNomNom x'' = deBruijn2 x'' === deBruijn2 (transposeMF $ transposeMF x'')+-- prop_transposeNomNom x'' = deBruijn2 x'' === deBruijn2 (transposeNomFunc $ transposeNomFunc x'')++{-- | Commute List and Nom+prop_transposeListNom :: [Nom Atom] -> Bool+prop_transposeListNom x' = (deBruijn1 <$> x') == (deBruijn1 (transposeNomFunc (transposeTraversableNom x')))+--}
+ src/Language/Nominal/Properties/SpecUtilities.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE FlexibleInstances   #-}+{-# LANGUAGE PolyKinds           #-}+{-# LANGUAGE ScopedTypeVariables #-}++{-# OPTIONS_GHC -Wno-orphans #-}++module Language.Nominal.Properties.SpecUtilities+    where++import qualified Data.List.NonEmpty                as NE+import           Data.Proxy                        (Proxy (..))+import           System.IO.Unsafe                  (unsafePerformIO)+import           Type.Reflection                   (Typeable)++import           Test.QuickCheck++import           Language.Nominal.Abs+import           Language.Nominal.Examples.SystemF+import           Language.Nominal.Name+import           Language.Nominal.Nom+import           Language.Nominal.Binder+import           Language.Nominal.Unify+import           Language.Nominal.Unique+import           Language.Nominal.Equivar++myatomnames :: [String]+myatomnames = map show [0 :: Int .. 25]++{-# NOINLINE myUniques #-}  -- play safe because of unsafePerformIO+myUniques :: [Unique]+myUniques = unsafePerformIO $ mapM (\_x -> newUnique) myatomnames ++myAtoms :: proxy s -> [KAtom s]+myAtoms _ = Atom <$> myUniques++-- | We only care about short and simple strings+instance {-# OVERLAPPING #-} Arbitrary String where+    arbitrary = elements $ map return (['a'..'z']++['A'..'Z'])++-- | Pick an atom+instance Arbitrary (KAtom s) where+    arbitrary = elements $ myAtoms (Proxy :: Proxy s)++instance Arbitrary a => Arbitrary (KName s a) where+   arbitrary = Name <$> arbitrary <*> arbitrary+instance {-# OVERLAPPING #-} Arbitrary (Name String) where+   arbitrary = do -- Gen monad+      atm <- arbitrary  +      return $ Name (show atm) atm++instance (Typeable s, Swappable t, Swappable a, Arbitrary (KName s t), Arbitrary a) => Arbitrary (KAbs (KName s t) a) where+   arbitrary = do -- Gen monad+      nam <- arbitrary+      a   <- arbitrary+      return $ nam @> a  -- hlint suggestion ignored++instance (Typeable s, Swappable a, Arbitrary a) => Arbitrary (KNom s a) where+   arbitrary = do -- Gen monad+      nams <- arbitrary+      a    <- arbitrary+      return $ nams @> a   -- hlint suggestion ignored++-- | For QuickCheck tests: pick a type+instance Arbitrary Typ where+  arbitrary =+    sized arbitrarySizedTyp++arbitrarySizedTyp :: Int -> Gen Typ +arbitrarySizedTyp m = +  if m < 2 then +     TVar <$> arbitrary +  else +     oneof [TVar <$> arbitrary+           ,do -- Gen monad+               t1 <- arbitrarySizedTyp (m `div` 2) +               t2 <- arbitrarySizedTyp (m `div` 2)+               return $ t1 :-> t2+           ,do -- Gen monad+               t <- arbitrarySizedTyp (m-1)+               n <- arbitrary+               return $ All (n @> t)+           ]++-- | For QuickCheck tests: pick a term +instance Arbitrary Trm where+  arbitrary =+    sized arbitrarySizedTrm++arbitrarySizedTrm :: Int -> Gen Trm +arbitrarySizedTrm m = +  if m < 2 then +     Var <$> arbitrary +  else +     oneof [Var <$> arbitrary+           ,do -- Gen monad+               t1 <- arbitrarySizedTrm (m `div` 2) +               t2 <- arbitrarySizedTrm (m `div` 2)+               return $ App t1 t2+           ,do -- Gen monad+               t <- arbitrarySizedTrm (m-1)+               n <- arbitrary+               return $ Lam (n @> t)+           ,do -- Gen monad+               t1 <- arbitrarySizedTrm (m `div` 2) +               t2 <- arbitrarySizedTyp (m `div` 2)+               return $ TApp t1 t2+           ,do -- Gen monad+               t <- arbitrarySizedTrm (m-1)+               n <- arbitrary+               return $ TLam (n @> t)+           ]++instance Arbitrary a => Arbitrary (NE.NonEmpty a) where+    arbitrary = (NE.:|) <$> arbitrary <*> arbitrary++genEvFinMap :: (UnifyPerm a, Eq a, Eq b) => Gen a -> Gen b -> Gen (EvFinMap a b)+genEvFinMap genA genB = evFinMap <$> genB <*> listOf ((,) <$> genA <*> genB)++instance forall a b. +         ( Arbitrary a+         , UnifyPerm a+         , Eq a+         , Arbitrary b+         , Eq b+         ) => Arbitrary (EvFinMap a b) where+    arbitrary = genEvFinMap arbitrary arbitrary+    shrink f = [evFinMap b xs | (b, xs) <- shrink $ fromEvFinMap f]
+ src/Language/Nominal/Properties/SubSpec.hs view
@@ -0,0 +1,82 @@+{-|+Module      : SubSpect +Description : Substitution properties +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Duplicating some tests from "Language.Nominal.Properties.Examples.SystemFSpec", which has good inductive datatypes to substitute on. +-}++{-# LANGUAGE DataKinds        #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PolyKinds        #-}++module Language.Nominal.Properties.SubSpec+    where++import Test.QuickCheck+import Type.Reflection                   (Typeable)++import Language.Nominal.Name +import Language.Nominal.Binder+import Language.Nominal.Sub+import Language.Nominal.Abs+import Language.Nominal.Examples.SystemF+++-- | y[n-> var n] = y+iprop_sub_id :: (KSub ntyp x y, Eq y) => (ntyp -> x) -> ntyp -> y -> Bool +iprop_sub_id f n y = y == sub n (f n) y+prop_sub_id_typevar' :: NTyp -> Typ -> Bool +prop_sub_id_typevar' = iprop_sub_id TVar +prop_sub_id_termvar :: NTrm -> Trm -> Bool +prop_sub_id_termvar = iprop_sub_id Var+prop_sub_id_typevar :: NTyp -> Trm -> Bool +prop_sub_id_typevar = iprop_sub_id TVar++-- | n # y => y[n->x] = y+iprop_sub_fresh :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => KName s n -> x -> y -> Property +iprop_sub_fresh n x y = n `freshFor` y ==> (y === sub n x y)+prop_sub_fresh_typevar' :: NTyp -> Typ -> Typ -> Property +prop_sub_fresh_typevar' = iprop_sub_fresh +prop_sub_fresh_typevar :: NTyp -> Typ -> Trm -> Property +prop_sub_fresh_typevar = iprop_sub_fresh +prop_sub_fresh_termvar :: NTrm -> Trm -> Trm -> Property +prop_sub_fresh_termvar = iprop_sub_fresh ++-- | n' # y => y[n->n'] = (n' n).y+iprop_sub_perm :: (Typeable s, Swappable y, Swappable n, KSub (KName s n) x y, Eq y, Show y) => (KName s n -> x) -> KName s n -> KName s n -> y -> Property +iprop_sub_perm f n n' y = n' `freshFor` y ==> sub n (f n') y === kswpN n' n y+prop_sub_perm_typevar' :: NTyp -> NTyp -> Typ -> Property +prop_sub_perm_typevar' = iprop_sub_perm TVar +-- this one trapped an error+prop_sub_perm_typevar'' :: NTyp -> NTyp -> Trm -> Property +prop_sub_perm_typevar'' = iprop_sub_perm TVar +prop_sub_perm_termvar :: NTrm -> NTrm -> Trm -> Property +prop_sub_perm_termvar = iprop_sub_perm Var ++-- Test capture-avoidance++-- [n1][n1 -> n2] = n2+prop_sub_singleton1 :: Name Int -> Name Int -> Bool+prop_sub_singleton1 n1 n2 = sub n1 n2 [n1] == [n2]++-- [n2][n1 -> n2] = n2+prop_sub_singleton2 :: Name Int -> Name Int -> Bool+prop_sub_singleton2 n1 n2 = (sub n1 n2 [n2]) == [n2]++ +-- n#n1,n2 ==> (n.x)[n1 -> n2] = n.(x[n1 -> n2])+prop_sub_abs_1 :: Name () -> Name () -> Name () -> [Name ()] -> Property +prop_sub_abs_1 n n1 n2 x = n /= n1 && n /= n2 ==> (sub n1 n2 (abst n x)) == abst n (sub n1 n2 x)++-- (n.x)[n1 -> n2] = n.(x[n1 -> n2]) fails in general+prop_sub_abs_1' :: Name () -> Name () -> Name () -> [Name ()] -> Property +prop_sub_abs_1' n n1 n2 x = expectFailure $ (sub n1 n2 (abst n (n:n1:n2:x))) == abst n (sub n1 n2 (n:n1:n2:x))++-- (n.x)[n -> n2] = n.x +prop_sub_abs_3 :: Name () -> Name () -> [Name ()] -> Bool+prop_sub_abs_3 n n2 x = (sub n n2 (abst n x)) == abst n x
+ src/Language/Nominal/Properties/UnifySpec.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE DataKinds              #-}+{-# LANGUAGE DeriveGeneric          #-}+{-# LANGUAGE FlexibleContexts       #-}+{-# LANGUAGE FlexibleInstances      #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses  #-}+-- {-# LANGUAGE PolyKinds              #-}+{-# LANGUAGE ScopedTypeVariables    #-}+{-# LANGUAGE TypeSynonymInstances   #-}+{-# LANGUAGE TypeApplications       #-}++{-# OPTIONS_GHC -Wno-orphans #-}++module Language.Nominal.Properties.UnifySpec+    where++import Data.Set                      as S+import Test.QuickCheck++import Language.Nominal.Name +import Language.Nominal.NameSet +import Language.Nominal.Nom+import Language.Nominal.Binder+import Language.Nominal.Abs+import Language.Nominal.Unify++-- | l is unifiable with  l' for any l and l'+-- Should fail, taking e.g. l = [] and l' nonempty+prop_l_l' :: [Name Int] -> [Name Int] -> Property +prop_l_l' ns' ns = expectFailure $ unifiablePerm ns ns' ++-- | ns @> ns' @> x  is unifiable with  ns' @> ns @> x  +prop_res_res :: [Atom] -> [Atom] -> [Atom] -> Bool+prop_res_res ns' ns x = kunifiablePerm atTom (restrict ns' ((ns @> x) :: Nom [Atom])) (restrict ns (ns' @> x))++-- | x' -> ns x -> res ns x unifies with x'+prop_res_unres :: Nom [Name Int] -> Bool+prop_res_unres x' = x' @@! \atms x -> unifiablePerm x' $ atms @> x++-- | Unifiers correctly calculated +prop_unify_ren :: [Name ()] -> [Name ()] -> Property +prop_unify_ren a b = let a' = Prelude.take 5 a -- control size so decent chance are unifiable+                         b' = Prelude.take 5 b+                     in unifiablePerm a' b' ==> ren (unifyPerm a' b') a' === b'++-- | 'idRen' equals 'idRen' extended with an identity mapping (since equality is on nub).+prop_renId :: Atom -> Bool+prop_renId a = renExtend a a idRen == idRen +++-- | Permutations and freshening renamings coincide+iprop_fresh_ren :: (UnifyPerm a, Support a, Swappable a, Eq a) => a -> Bool+iprop_fresh_ren a = let (atms :: [Atom]) = S.toList $ supp a in unNom $ do -- Nom monad+   atms' <- freshKAtoms atms+   let p = zip atms atms'+   return $ perm p a == ren (renFromList p) a ++prop_fresh_ren_atmlistlist :: [[Atom]] -> Bool+prop_fresh_ren_atmlistlist = iprop_fresh_ren ++prop_fresh_ren_absatmlist :: Abs () [Atom] -> Bool+prop_fresh_ren_absatmlist = iprop_fresh_ren ++-- TODO: arbitrary instance for Ren?
+ src/Language/Nominal/Properties/UtilitiesSpec.hs view
@@ -0,0 +1,22 @@+module Language.Nominal.Properties.UtilitiesSpec+    where++import Data.Data ++import Language.Nominal.Utilities+import Language.Nominal.Name+import Language.Nominal.Properties.SpecUtilities ()+++-- | Find integers and increment them+superSucc :: Data x => x -> x+superSucc = rewrite $ Just . (succ :: Int -> Int) ++-- | Rewrite rewrites inside a @[Int]@ +prop_test_rewrite1 :: [Int] -> Bool +prop_test_rewrite1 x = superSucc x == fmap succ x++-- | Rewrite rewrites inside a list of 'Int'-labelled names+prop_test_rewrite2 :: [Name Int] -> Bool +prop_test_rewrite2 x = superSucc x == fmap (fmap succ) x+
+ src/Language/Nominal/SMonad.hs view
@@ -0,0 +1,167 @@+{-|+Module      : A theory of suspended monoid actions+Description : A theory of suspended monoid actions+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Typeclass and instances for a "suspended" monoid action.  Three examples will be of particular interest:++* Suspend a permutation (@'XSwp' s@).  (This is familiar from the theory of /nominal rewriting/, where swappings suspend on unknowns.)  +* Suspend a binding (@'XRes' s@; we use this to define @'Language.Nominal.Nom.KNom'@).   +* Suspend a capture-avoiding binding (@'Language.Nominal.Nom.KNom' s@).  ++Intuitively, 'Language.Nominal.Nom.KNom' is just 'XRes' plus 'Swappable' plus 'IO' (for fresh IDs). +-}++{-# LANGUAGE ConstraintKinds       +           , DataKinds             +           , DefaultSignatures     +           , DeriveAnyClass+           , DerivingVia           +           , DeriveFunctor+           , DeriveGeneric+           , EmptyCase             +           , FlexibleContexts      +           , FlexibleInstances     +           , FunctionalDependencies +           , GADTs                 +           , InstanceSigs          +           , KindSignatures +           , MultiParamTypeClasses +           , PartialTypeSignatures   +           , ScopedTypeVariables     +           , StandaloneDeriving      +           , TupleSections         +           , TypeOperators         +           , UndecidableInstances +#-}  ++module Language.Nominal.SMonad+    where++import           Control.Monad+import           GHC.Generics     hiding (Prefix) -- avoid clash with Data.Data.Prefix+import           Type.Reflection++import           Language.Nominal.Name+import           Language.Nominal.NameSet+import           Language.Nominal.Utilities++-- | A typeclass for computing under a monoid action.  +--+-- RULES: +--+-- > exit . enter mempty ==  id+-- > flip >>+ . const    ==  >==     i.e.   a' >>= f = a' >>+ const f+-- > enter mempty        ==  return+--+-- In other words:+--+-- * @+<< . const@ and @enter mempty@ form a monad.+-- * @enter mempty@ followed by @exit@ is a noop. +class Monoid i => SMonad i m | m -> i where+   (>>+) :: m a -> (i -> a -> m b) -> m b+   -- ^ Move from one suspended environment to another via a function @i -> a -> m b@.+   enter :: i -> a -> m a+   -- ^ Enter the suspended environment, by suspending @i@ on @a@.+   exit  :: m a -> a+   -- ^ Exit the suspended environment, discarding any suspended actions. +   -- Use 'exitWith' to exit while folding actions into the computation. ++{-- instance SMonad i m => Functor m where+    fmap = liftM+instance SMonad i m => Applicative m where+    pure  = return+    (<*>) = ap+instance SMonad i m => Monad m where+    (>>=) a' cont = a' >>+ const cont+    return = enter mempty +--}+   +(+<<) :: SMonad i m => (i -> a -> m b) -> m a -> m b+(+<<) = flip (>>+)++-- | An equivalent to 'fmap', with access to the monoid.+imap :: SMonad i m => (i -> a -> b) -> m a -> m b+imap f a' = a' >>+ \i a -> enter mempty $ f i a -- mempty -> i?++-- | An equivalent to '<&>', with access to the monoid.+pami :: SMonad i m => m a -> (i -> a -> b) -> m b+pami = flip imap++-- | Exit the 'SMonad', with a function to fold the monoid into the computation.  So:+--+-- > exit = exitWith (,)+exitWith :: SMonad i m => (i -> a -> b) -> m a -> b+exitWith = exit .: imap  ++-- | @flip 'exitWith'@+withExit :: SMonad i m => m a -> (i -> a -> b) -> b+withExit = flip exitWith++-- | An 'SMonad' has an @i@-monoid action+iact :: (Monad m, SMonad i m) => i -> m a -> m a+-- iact i a' = a' >>+ \i' a -> enter (i <> i') a +iact = join .: enter +++----------------------+-- Deriving via machinery for SMonad+--+-- Usage:+--    deriving (Functor, Applicative, Monad) via ViaSMonad <instance-name>++newtype ViaSMonad m a = ViaSMonad {runViaSMonad :: m a}+instance SMonad i m => Functor (ViaSMonad m) where+    fmap = liftM+instance SMonad i m => Applicative (ViaSMonad m) where+    pure = return+    (<*>) = ap+instance SMonad i m => Monad (ViaSMonad m) where+    return = ViaSMonad . enter mempty+    ViaSMonad fa >>= cont = ViaSMonad $ fa >>+ const (runViaSMonad . cont)+----------------------+++-- | A generic type for suspended monoid operations +data XSuspend i a = Suspend i a +   deriving (Functor, Applicative, Monad) via ViaSMonad (XSuspend i)+   deriving (Generic, Swappable, Eq, Show)++instance Monoid i => SMonad i (XSuspend i) where+   (>>+)  :: XSuspend i a -> (i -> a -> XSuspend i a') -> XSuspend i a' +   Suspend i a >>+ g = let (Suspend i' a') = g i a in Suspend (i <> i') a'+   enter :: i -> a -> XSuspend i a+   enter = Suspend +   exit :: XSuspend i a -> a+   exit (Suspend _ a) = a+++-- | A type for suspended swappings+type XSwp s a = XSuspend (KPerm s) a++-- | Exit with a swapping action, if available+getSwp :: (Typeable s, Swappable a) => XSwp s a -> a+getSwp = exitWith perm++-- | A type for suspended restrictions +type XRes s a = XSuspend [KAtom s] a++-- | Exit with a restriction action, if available+getRes :: KRestrict s a => XRes s a -> a+getRes = exitWith restrict++-- * Transpose an 'SMonad' with other constructors.++-- | Transpose an 'SMonad' with a 'Functor'+-- +-- /Note: if @m@ is instantiated to @'Language.Nominal.Nom.KNom' s@ then note there is no capture-avoidance here; local bindings are just moved around.  A stronger version (with correspondingly stronger typeclass assumptions) is in 'Language.Nominal.Nom.transposeNomF'./ +transposeMF :: (Functor f, SMonad i m) => m (f a) -> f (m a)+transposeMF = exitWith $ fmap . enter ++-- | This is just an instance of a more general principle, since @f@ is 'Traversable' and we assume @m@ applicative.+transposeFM :: (Traversable f, Applicative m, SMonad i m) => f (m a) -> m (f a)+transposeFM = sequenceA
+ src/Language/Nominal/Sub.hs view
@@ -0,0 +1,138 @@+{-|+Module      : Sub +Description : Nominal treatment of substitution+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Typeclass for types that support a substitution action.  Capture-avoidance is automatic, provided you used @'Nom'@ or @'Abs'@ types for binding, of course.  ++See "Language.Nominal.Examples.SystemF" for usage examples. +-}++{-# LANGUAGE ConstraintKinds       +           , DataKinds             +           , DefaultSignatures     +           , DerivingVia           +           , EmptyCase             +           , FlexibleContexts      +           , FlexibleInstances     +           , InstanceSigs          +           , MultiParamTypeClasses +           , PartialTypeSignatures   +           , StandaloneDeriving      +           , TupleSections         +           , TypeOperators         +#-}++{-# OPTIONS_GHC -fno-warn-orphans #-} -- Suppress orphan instance of BinderConc instance of KAbs.++module Language.Nominal.Sub+   ( -- * Substitution+     KSub (..)+   , Sub+   -- * Test+   -- $test+   ) +    where++import GHC.Generics         +import Type.Reflection +import Data.List.NonEmpty (NonEmpty)++import Language.Nominal.Name +import Language.Nominal.Binder+import Language.Nominal.Abs++-- * Substitution++-- | Substitution.  @sub n x y@ corresponds to "substitute the name n for the datum x in y".+--+-- We intend that @n@ should be a type of names @KName k n@. +class KSub n x y where+    sub :: n -> x -> y -> y+    -- We could reasonably insert a MINIMAL condition here, but in this case we don't because there's a default instance. +    default sub :: (Generic y, GSub n x (Rep y)) => n -> x -> y -> y+    sub n x = to . gsub n x . from++-- | Canonical instance for the unit atom sort+type Sub n x y = KSub (KName Tom n) x y+++-- order: nameless, tuple, list, nonempty list, maybe, sum, nom ++-- | sub on nameless type is trivial+instance KSub n x (Nameless a) where+   sub _ _ = id++deriving via Nameless Bool instance KSub n x Bool+deriving via Nameless Int  instance KSub n x Int+deriving via Nameless ()   instance KSub n x ()+deriving via Nameless Char instance KSub n x Char++instance (KSub n x a, KSub n x b) => KSub n x (a, b)+instance (KSub n x a, KSub n x b, KSub n x c) => KSub n x (a, b, c)+instance (KSub n x a, KSub n x b, KSub n x c, KSub n x d) => KSub n x (a, b, c, d)+instance (KSub n x a, KSub n x b, KSub n x c, KSub n x d, KSub n x e) => KSub n x (a, b, c, d, e)+instance KSub n x a => KSub n x [a]+instance KSub n x a => KSub n x (NonEmpty a)+instance KSub n x a => KSub n x (Maybe a)+instance (KSub n x a, KSub n x b) => KSub n x (Either a b)+++-- | sub on names+instance KSub (KName s n) (KName s n) (KName s n) where -- We could legitimately insist on Typeable s, Swappable n, Eq n here, but we do not because names are compared for equality by atom.+   sub n n' a = if a == n then n' else a ++-- | Nameless form of substitution, where the name for which we substitute is packaged in a @'KAbs'@ abstraction. +instance {-# INCOHERENT #-} (Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => BinderConc (KAbs (KName s n) y) (KName s n) y s x where  -- may be overlapped by the native `conc` name instance of KAbs.  If in doubt, favour the native version.  This may change.+   conc y' x = y' @@! \n -> sub n x  + ++{-- | Nameless form of substitution, where the name for which we substitute is packaged in a @'KAbs'@ abstraction. +subApp :: (Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => KAbs (KName s n) y -> x -> y+subApp y' x = y' @@! \n -> sub n x -- flip sub x +-- | Nameless form of substitution, where the name for which we substitute is packaged in a @'KAbs'@ abstraction ('flip'ped version). +appSub :: (Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => x -> KAbs (KName s n) y -> y+appSub = flip subApp --}+++-- | sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body+instance (Typeable s, Typeable u, KSub (KName s n) x t, KSub (KName s n) x y, Swappable t, Swappable y) => +            KSub (KName s n) x (KAbs (KName u t) y) where+  sub n x = genApp $ \n' y -> (sub n x <$> n') @> sub n x y ++-- | Placeholder for future development.  A general maths behind this definition is given in Section 8.1 of <https://dl.acm.org/doi/10.1145/2700819 Semantics Out Of Context> (<http://gabbay.org.uk/papers.html#semooc author's pdf>).+instance Eq n => KSub n ((n -> a) -> a) (n -> a) where+   sub n x ctx n' = if n' == n then x ctx else ctx n'+-- | Placeholder for future development.  A general maths behind this definition is given in Section 8.1 of <https://dl.acm.org/doi/10.1145/2700819 Definition 8.12 of Semantics Out Of Context> (<http://gabbay.org.uk/papers.html#semooc author's pdf>).+instance Eq n => KSub n ((n -> a) -> a) ((n -> a) -> a) where+   sub n x x' ctx = x' (sub n x ctx)++-- * Generics support for @'KSub'@++class GSub n x f where+    gsub :: n -> x -> f w -> f w ++instance GSub n x V1 where+    gsub _ _ y = case y of++instance GSub n x U1 where+    gsub _ _ = id++instance GSub n x f => GSub n x (M1 i t f) where+    gsub n x = M1 . gsub n x . unM1++instance KSub n x c => GSub n x (K1 i c) where+    gsub n x = K1 . sub n x . unK1++instance (GSub n x f, GSub n x g) => GSub n x (f :*: g) where+    gsub n x (y :*: z) = gsub n x y :*: gsub n x z++instance (GSub n x f, GSub n x g) => GSub n x (f :+: g) where+    gsub n x (L1 y) = L1 $ gsub n x y+    gsub n x (R1 z) = R1 $ gsub n x z++{- $tests Property-based tests are in "Language.Nominal.Properties.SubSpec". -}
+ src/Language/Nominal/Unify.hs view
@@ -0,0 +1,363 @@+{-|+Module      : Unify +Description : Unification by permutation+Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Unification by permutation+-}++{-# LANGUAGE ConstraintKinds            +           , DataKinds                  +           , DefaultSignatures          +           , DeriveGeneric              +           , DerivingStrategies         +           , DerivingVia                +           , EmptyCase                  +           , FlexibleContexts           +           , FlexibleInstances          +           , GADTs                      +           , GeneralizedNewtypeDeriving   +           , InstanceSigs               +           , MultiParamTypeClasses      +           , PartialTypeSignatures        +           , ScopedTypeVariables        +           , StandaloneDeriving         +           , TupleSections              +           , TypeOperators              +#-}++module Language.Nominal.Unify+    ( -- $setup+      -- * Introduction+      -- -- $intro+      -- * @'Ren'@+      KRen (..)+    , Ren +    , idRen+    , nothingRen+    , isJustRen +    , isNothingRen +      -- Manipulating renamings+    , renNub +    , renExtend+    , renToList+    , renFromList+    , renRemoveBlock+      -- * Unification up to a @'KRen'@+    , KUnifyPerm (..)+    , UnifyPerm+    , unifyPerm+    , kunifiablePerm+    , unifiablePerm+      -- * Special case: unifying prefixes of lists+    , kevPrefixRen+    , evPrefixRen+    , kevIsPrefix+    , evIsPrefix+      -- * Tests+      -- $tests+    ) where++import           Data.Function            (on)+import qualified Data.Map.Strict          as DM -- for unifyPerm +import           Data.Maybe               -- (isJust)+import           Data.List.Extra          (takeEnd)+import           Data.List.NonEmpty       (NonEmpty)+import           Data.Proxy               (Proxy (..))+import qualified Data.Set                 as S -- (fromList) +import           Data.Type.Equality+import           GHC.Generics+import           Type.Reflection++import           Language.Nominal.Name+import           Language.Nominal.NameSet+import           Language.Nominal.Nom+import           Language.Nominal.Binder+import           Language.Nominal.Abs++-- $setup+-- >>> import Data.Set as S++{- $intro++-}+++-- * @'Ren'@++-- | An element of `Ren` is either+-- +-- 1. `Just` an injective finite map from `Atom` to `Atom` (for this file, call this a __renaming__), or+--+-- 2. A "nomap" value (`Nothing`).+-- +-- A `Ren` represents a solution to the problem +--+-- /does there exist a permutation that makes @x@ equal to @y@?/+--+-- A type in the @'KUnifyPerm'@ typeclass is structurally guaranteed to give /at most one/ solution to such a unification problem, up to renaming irrelevant atoms. +-- So in a nutshell: names, lists, and tuples are good here, and functions (not an equality type) and sets (may have multiple solutions) are not good.+--+--  A 'Just' value represents a solution to this unification problem; a 'Nothing' value represents that no such solution can be found.  @'unifyPerm'@ calculates these solutions. +newtype KRen s = Ren {unRen :: Maybe (DM.Map (KAtom s) (KAtom s))}+   deriving (Show, Generic)++instance Typeable s => Swappable (KRen s) where + +-- | Renaming on a @'Tom'@ instance+type Ren = KRen Tom++-- | The identity renaming.  +idRen :: KRen s +idRen = Ren . Just $ DM.empty++-- | The Nothing renaming.  If we think of @'KRen' s@ as type of solutions to permutation unification problems, then @'nothingRen'@ indicates no solution could be found. +nothingRen :: KRen s +nothingRen = Ren Nothing +++-- | Is it Just a renaming?  (My unification problem can be solved, and here's the solution.) +isJustRen :: KRen s -> Bool+isJustRen (Ren x) = isJust x++-- | Is it Nothing?  (Nope; no solution exists.) +isNothingRen :: KRen s -> Bool+isNothingRen = not . isJustRen++-- | Elements of @'KRen'@ are compared for equality on their __nub__ @'renNub'@, meaning just that identity mappings are ignored.+--+-- >>> a = exit $ freshAtom+-- >>> idRen == renExtend a a idRen+-- True +instance Eq (KRen s) where+    (==) = (==) `on` (unRen . renNub)++-- | Elements of @'KRen'@ are compared on their __nub__ @'renNub'@, meaning just that identity mappings are ignored.+instance Ord (KRen s) where+    compare = compare `on` unRen . renNub++-- | Support of a renaming is the set of nontrivially mapped atoms +--+-- >>> (supp (idRen :: Ren)) == S.empty+-- True+-- >>> (supp (nothingRen :: Ren)) == S.empty+-- True+instance Typeable s => KSupport s (KRen s) where+   ksupp _ (Ren m') = +      fromMaybe S.empty $ +         DM.foldrWithKey (\a b s -> if a == b then s else s `S.union` (S.fromList [a,b])) S.empty <$> m' +++-- | The parts of the map that are not identity+renNub :: KRen s -> KRen s+renNub (Ren m') = Ren $ DM.filterWithKey (/=) <$> m' +++-- | Extend a renaming m with a new pair a -> b, maintaining the property of being a partial injection.+-- If adding a->b would destroy partial injectivity, then return @Nothing@. +renExtend :: KAtom s -> KAtom s -> KRen s -> KRen s+renExtend a b (Ren m') = Ren $ do -- Maybe monad +   m <- m'+   case DM.lookup a m of+      Nothing | not $ elem b $ DM.elems m -> DM.insert a b <$> m' -- if a doesn't map and b isn't already mapped to, then add (a,b)+      Just b' | b' == b                   -> m' -- if a maps to b already, then do nothing +      _                                   -> Nothing -- otherwise, complain++-- | Extract the graph of a 'Ren', Maybe.+renToList :: KRen s -> Maybe [(KAtom s, KAtom s)]+renToList (Ren Nothing)  = Nothing+renToList (Ren (Just m)) = Just $ DM.toList m++-- | Convert a graph to a 'Ren'. +renFromList :: [(KAtom s, KAtom s)] -> KRen s+renFromList = foldr (\(a,b) r -> renExtend a b r) idRen ++-- | Given a block of atoms, remove them from the map /provided/ that the atoms in that block only map to other atoms within it; if an atom gets mapped across the block boundary, return @Nothing@. +--+-- Needed for equality instance of 'Language.Nominal.Examples.IdealisedEUTxO.Chunk'.+renRemoveBlock :: [KAtom s] -> KRen s -> KRen s+renRemoveBlock _    (Ren Nothing)  = Ren Nothing+renRemoveBlock atms (Ren (Just m)) =+   DM.foldrWithKey (\a b r -> case (a `elem` atms, b `elem` atms) of  +                                 (True,  True)  -> r                 -- both elements in block; discard+                                 (False, False) -> renExtend a b r   -- both elements out of block; append (some inefficiency here, no doubt)+                                 _              -> nothingRen        -- otherwise stop+                   ) idRen m+              ++instance Semigroup (KRen s) where+    (Ren (Just m)) <> r = DM.foldrWithKey renExtend r m +    (Ren Nothing)  <> _ = Ren Nothing ++instance Monoid (KRen s) where+   mempty = Ren $ Just DM.empty++-- | There are two reasonable notions of restriction; filter, or default to Nothing.  We choose the option that discards minimal information, i.e. the filter.+instance Typeable s => KRestrict s (KRen s) where+   restrict :: [KAtom s] -> KRen s -> KRen s+   restrict as (Ren m') = Ren $ do -- Maybe monad+      m <- m'+      return $ DM.filterWithKey (\a b -> not (elem a as) && not (elem b as)) m++-- * Unification up to a @'KRen'@++-- | Equal-up-to-permutation.  The algorithm works very simply by traversing the element looking for atoms and when it finds them, trying to match them up.  If it can do so injectively then it succeeds with @'Just'@ a renaming; if it fails it returns @'Nothing'@. +--+-- /Question: Granted that 'KUnifyPerm' is a subset of 'KSupport', why are they not equal?/+-- Because for simplicity we only consider types for which at most one unifier can be found, by an efficient structural traversal.+-- This avoids backtracking, and makes a 'kunifyPerm' a function to 'KRen'.+-- So, a key difference is that 'KSupport' can easily calculate the support of a set (unordered list without multiplicities) whereas 'KUnifyPerm' does not even attempt to calculate unifiers of sets; not because this would be impossible, but because it would require a significant leap in complexity that we do not seem to need (so far).+class KSupport s a => KUnifyPerm s a where+    +    -- | This calculates a solution to a unification problem+    kunifyPerm :: proxy s -> a -> a -> KRen s+    default kunifyPerm :: (Generic a, GUnifyPerm s (Rep a)) => proxy s -> a -> a -> KRen s+    kunifyPerm _ x y = gunifyPerm (from x) (from y)+   +    -- | This applies a solution to a unification problem (represented as a renaming) to an element.  +    --+    -- __Note:__ @'ren'@ is not just swapping.  It traverses the structure of its argument performing an atom-for-atom renaming.  In the case that its argument solves a unification problem, its /effect/ is the same as if a permuatation were applied.+    --+    -- This is checked in 'Language.Nominal.Properties.UnifySpec.iprop_fresh_ren' and 'Language.Nominal.Properties.UnifySpec.prop_unify_ren'.+    ren :: KRen s -> a -> a +    default ren :: (Generic a, GUnifyPerm s (Rep a)) => KRen s -> a -> a+    ren r = to . gren r . from++-- | 'Tom'-instance of typeclass 'KUnifyPerm'.+type UnifyPerm = KUnifyPerm Tom++-- | Unify on 'Atom's, thus 'Tom'-instance of 'kunifyPerm'.+unifyPerm :: UnifyPerm a => a -> a -> Ren+unifyPerm = kunifyPerm atTom++-- | Does an s-unifier exist?+--+-- We write @proxy@ instead of 'Proxy' for the user's convenience, so the user can take advantage of any type that mentions @s@.+kunifiablePerm :: KUnifyPerm s a => proxy s -> a -> a -> Bool +kunifiablePerm p a a' = isJustRen $ kunifyPerm p a a' ++-- | Does a 'Tom'-unifier exist?+unifiablePerm :: UnifyPerm a => a -> a -> Bool+unifiablePerm = kunifiablePerm atTom+++----------------------------------------------+-- KUnifyPerm instances+-- instance order: nameless, tuple, list, nonempty list, maybe, sum, atom, name, nom, abs ++instance (Typeable s, Eq a) => KUnifyPerm s (Nameless a) where+    kunifyPerm _ a b+        | a == b    = mempty+        | otherwise = Ren Nothing+    ren _ = id++deriving via Nameless Bool instance Typeable s => KUnifyPerm s Bool+deriving via Nameless Int  instance Typeable s => KUnifyPerm s Int+deriving via Nameless ()   instance Typeable s => KUnifyPerm s ()+deriving via Nameless Char instance Typeable s => KUnifyPerm s Char++instance (KUnifyPerm s a, KUnifyPerm s b) => KUnifyPerm s (a, b)+instance (KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c) => KUnifyPerm s (a, b, c)+instance (KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c, KUnifyPerm s d) => KUnifyPerm s (a, b, c, d)+instance (KUnifyPerm s a, KUnifyPerm s b, KUnifyPerm s c, KUnifyPerm s d, KUnifyPerm s e) => KUnifyPerm s (a, b, c, d, e)+instance KUnifyPerm s a => KUnifyPerm s [a]+instance KUnifyPerm s a => KUnifyPerm s (NonEmpty a)+instance KUnifyPerm s a => KUnifyPerm s (Maybe a)+instance (KUnifyPerm s a, KUnifyPerm s b) => KUnifyPerm s (Either a b)++-- | Unify atoms+instance (Typeable s, Typeable t) => KUnifyPerm s (KAtom t) where++    kunifyPerm :: proxy s -> KAtom t -> KAtom t -> KRen s+    kunifyPerm _ a b = case testEquality (typeRep :: TypeRep s) (typeRep :: TypeRep t) of+        Nothing+            | a == b    -> mempty+            | otherwise -> Ren Nothing+        Just Refl       -> renExtend a b mempty++    ren :: KRen s -> KAtom t -> KAtom t+    ren (Ren (Just m)) a =+        case testEquality (typeRep :: TypeRep s) (typeRep :: TypeRep t) of+            Nothing   -> a+            Just Refl -> DM.findWithDefault a a m+    ren (Ren Nothing)  a = a++-- | Unify names: they behave just an atom-label tuple  +instance (Typeable s, Typeable u, KUnifyPerm s t) => KUnifyPerm s (KName u t)++-- | Unify 'Nom' abstractions.+-- Unpack, unify, clean out fresh names+instance (Typeable s, KUnifyPerm s a) => KUnifyPerm s (KNom s a) where+   -- kunifyPerm p noma nomb = resAppC (\a -> resAppC (kunifyPerm p a) nomb) noma  +   kunifyPerm p noma nomb = resAppC' noma $ \a -> resAppC' nomb $ \b -> kunifyPerm p a b+   ren r m = ren r <$> m+++-- | Unify 'Abs' name-abstraction+instance (Typeable s, KUnifyPerm s t, KUnifyPerm s a) => KUnifyPerm s (KAbs (KName s t) a) where+   kunifyPerm p absa absb = +      (fuse (absa, absb)) @@. \na (a,b) -> kunifyPerm p (na, a) (na, b) -- use of '@@.' here cleans out the (na, na) binding. +   ren r m = ren r <$> m+++-- * Special case: unifying prefixes of lists++-- | Unify a list with a prefix of the other +kevPrefixRen :: KUnifyPerm s a => proxy s -> [a] -> [a] -> KRen s+kevPrefixRen p l1 l2 = kunifyPerm p l1 (takeEnd (length l1) l2)++-- | Unify a list with a prefix of the other (at @'Tom'@ version). +evPrefixRen :: UnifyPerm a => [a] -> [a] -> Ren+evPrefixRen = kevPrefixRen atTom+++-- | One list unifies with a prefix of the other +kevIsPrefix :: forall s proxy a. KUnifyPerm s a => proxy s -> [a] -> [a] -> Bool +kevIsPrefix p l1 l2 = isJustRen $ kevPrefixRen p l1 l2++-- | One list unifies with a prefix of the other (at @'Tom'@ version). +evIsPrefix :: UnifyPerm a => [a] -> [a] -> Bool  +evIsPrefix = kevIsPrefix atTom+++-- * Generics support for @'KUnifyPerm'@++class GUnifyPerm s f where+    gunifyPerm :: f x -> f x -> KRen s+    gren       :: KRen s -> f x -> f x++instance GUnifyPerm s V1 where+    gunifyPerm x = case x of+    gren _ x = case x of++instance GUnifyPerm s U1 where+    gunifyPerm U1 U1 = mempty+    gren _ U1 = U1++instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :*: g) where+    gunifyPerm (x1 :*: y1) (x2 :*: y2) = gunifyPerm x1 x2 <> gunifyPerm y1 y2+    gren r (x :*: y) = gren r x :*: gren r y++instance (GUnifyPerm s f, GUnifyPerm s g) => GUnifyPerm s (f :+: g) where++    gunifyPerm (L1 x) (L1 y) = gunifyPerm x y+    gunifyPerm (R1 x) (R1 y) = gunifyPerm x y+    gunifyPerm _      _      = Ren Nothing++    gren r (L1 x) = L1 $ gren r x+    gren r (R1 x) = R1 $ gren r x++instance KUnifyPerm s c => GUnifyPerm s (K1 i c) where+    gunifyPerm (K1 x) (K1 y) = kunifyPerm Proxy x y    +    gren r (K1 x) = K1 $ ren r x++instance GUnifyPerm s f => GUnifyPerm s (M1 i t f) where+    gunifyPerm (M1 x) (M1 y) = gunifyPerm x y+    gren r (M1 x) = M1 $ gren r x++{- $tests Property-based tests are in "Language.Nominal.Properties.UnifySpec". -}+
+ src/Language/Nominal/Unique.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE Trustworthy        #-}+{-# LANGUAGE MagicHash          #-}++module Language.Nominal.Unique+    ( Unique+    , newUnique+    , hashUnique+    ) where++import Data.Data        (Typeable, Data)+import Data.IORef+import GHC.Base+import GHC.Num+import System.IO.Unsafe (unsafePerformIO)++-- | An abstract unique object.  Objects of type 'Unique' may be+-- compared for equality and ordering and hashed into 'Int'.+--+-- >>> :{+-- do x <- newUnique+--    print (x == x)+--    y <- newUnique+--    print (x == y)+-- :}+-- True+-- False+newtype Unique = Unique Integer deriving (Eq,Ord,Typeable,Data)++uniqSource :: IORef Integer+uniqSource = unsafePerformIO (newIORef 0)+{-# NOINLINE uniqSource #-}++-- | Creates a new object of type 'Unique'.  The value returned will+-- not compare equal to any other value of type 'Unique' returned by+-- previous calls to 'newUnique'.  There is no limit on the number of+-- times 'newUnique' may be called.+newUnique :: IO Unique+newUnique = do+  r <- atomicModifyIORef' uniqSource $ \x -> let z = x+1 in (z,z)+  return (Unique r)++-- SDM (18/3/2010): changed from MVar to STM.  This fixes+--  1. there was no async exception protection+--  2. there was a space leak (now new value is strict)+--  3. using atomicModifyIORef would be slightly quicker, but can+--     suffer from adverse scheduling issues (see #3838)+--  4. also, the STM version is faster.++-- SDM (30/4/2012): changed to IORef using atomicModifyIORef.  Reasons:+--  1. STM version could not be used inside unsafePerformIO, if it+--     happened to be poked inside an STM transaction.+--  2. IORef version can be used with unsafeIOToSTM inside STM,+--     because if the transaction retries then we just get a new+--     Unique.+--  3. IORef version is very slightly faster.++-- IGL (08/06/2013): changed to using atomicModifyIORef' instead.+--  This feels a little safer, from the point of view of not leaking+--  memory, but the resulting core is identical.++-- | Hashes a 'Unique' into an 'Int'.  Two 'Unique's may hash to the+-- same value, although in practice this is unlikely.  The 'Int'+-- returned makes a good hash key.+hashUnique :: Unique -> Int+hashUnique (Unique i) = I# (hashInteger i)
+ src/Language/Nominal/Utilities.hs view
@@ -0,0 +1,114 @@+{-|+Module      : Utilities +Description : Helper functions +Copyright   : (c) Murdoch J. Gabbay, 2020+License     : GPL-3+Maintainer  : murdoch.gabbay@gmail.com+Stability   : experimental+Portability : POSIX++Helper functions +-}++{-# LANGUAGE FlexibleInstances     +           , InstanceSigs          +           , MultiParamTypeClasses +           , FlexibleContexts      +           , TupleSections         +           , PartialTypeSignatures+#-}  ++module Language.Nominal.Utilities +    where++import           Data.Foldable      (Foldable (..)) -- for toList+import           Data.Generics+import           Data.List+import           Data.List.NonEmpty (NonEmpty (..))+import           GHC.Stack          (HasCallStack)+import           Control.Monad      (guard) +++rewrite :: (Typeable a, Data b) => (a -> Maybe a) -> b -> b+rewrite f b = case cast b of+    Just a+        | Just (Just a') <- cast $ f a -> a'+    _                                  -> gmapT (rewrite f) b++-- | Apply f repeatedly until we reach a fixedpoint+repeatedly :: Eq a => (a -> a) -> a -> a+repeatedly f x = let fx = f x in if fx == x then x else repeatedly f fx++-- | Apply a list of functions in succession.+chain :: [a -> a] -> a -> a+chain = foldr (.) id+-- https://hackage.haskell.org/package/speculate-0.4.1/docs/src/Test.Speculate.Utils.List.html#chain++-- | Standard function, returns @Just a@ provided @True@, and @Nothing@ otherwise +toMaybe :: Bool -> a -> Maybe a+toMaybe b a = guard b >> return a++-- | List subset.  Surely this must be in a library somewhere.+isSubsetOf :: Eq a => [a] -> [a] -> Bool +isSubsetOf l1 l2 = all (`elem` l2) l1++-- | Interleave a list of lists to a list+interleave :: [[a]] -> [a]+interleave = concat . transpose++-- | Returns 'Just' the tail of a list if it can, and 'Nothing' otherwise.+safeTail :: [a] -> Maybe [a]+safeTail (_ : xs) = Just xs+safeTail _        = Nothing++-- | Returns 'Just' the head of a list if it can, and 'Nothing' otherwise.+safeHead :: [a] -> Maybe a+safeHead (h : _) = Just h +safeHead _       = Nothing++-- https://hackage.haskell.org/package/intro-0.7.0.0/docs/Intro.html#v:.:+-- | Compose functions with one argument with function with two arguments.+--+--   @f .: g = \\x y -> f (g x y)@.+(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d+(.:) = (.) . (.)+infixr 8 .:+{-# INLINE (.:) #-}++-- | Finds the unique element in a collection satisfying a predicate. +-- Results in an error if there is no such element or if there are more than one.+--+-- >>> iota (== 1) [1, 2, 3]+-- 1+--+-- >>> iota (> 1) [1, 2, 3]+-- *** Exception: iota: expected exactly one element to satisfy the predicate, but found at least two+-- ...+--+-- >>> iota (> 3) [1, 2, 3]+-- *** Exception: iota: expected exactly one element to satisfy the predicate, but found none+-- ...+--+iota :: (HasCallStack, Foldable f) => (a -> Bool) -> f a -> a+iota p xs = case filter p $ toList xs of+    [x]     -> x+    []      -> error "iota: expected exactly one element to satisfy the predicate, but found none"+    (_ : _) -> error "iota: expected exactly one element to satisfy the predicate, but found at least two"++-- | point moves the (first) element satisfying the predicate to the head of the list.+-- Error raised if no such element found.+--+-- >>> point even [1,2,3]+-- 2 :| [1,3]+--+-- >>> point even [1,3,5]+-- *** Exception: point: no such element+-- ...+--+point :: Foldable f => (a -> Bool) -> f a -> NonEmpty a+point p = go . toList+  where+    go (x : xs)+        | p x       = x :| xs+        | otherwise = let (y :| ys) = go xs in y :| x : ys+    go []           = error "point: no such element"
+ test/Language/Nominal/AbsSpec.hs view
@@ -0,0 +1,24 @@+module Language.Nominal.AbsSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities () ++import Language.Nominal.Properties.AbsSpec++spec :: Spec+spec = do+    it "fuse a.x a.x' = a.(x,x')" $ property prop_fuse+    it "n # x => [n](x @ n) = x" $ property prop_Abs_Conc+    it "n' # x => [n]x = [n'](n' n).x" $ property prop_Abs_alpha+    it "(n.x) \\@ n = x" $ property prop_Conc_Abs+    it "(n.x) \\@ n = x" $ property prop_Conc_Abs_swap+    it "Atm.(X x Y) iso Atm.X x Atm.Y, left-to-right-to-left" $ property prop_fuse_unfuse_Abs+    it "Atm.(X x Y) iso Atm.X x Atm.Y, right-to-left-to-right" $ property prop_unfuse_fuse_Abs+    it "Iso fails if atoms labelled, since one label lost Atm.X x Atm.Y -> Atm.(X x Y)" $ property prop_unfuse_fuse_Abs'+    it "Atm.X iso Nom (Atm x X)" $ property prop_abs_to_nom+    it "Nom (Atm x X) iso Atm.X" $ property prop_nom_to_abs+
+ test/Language/Nominal/EquivarSpec.hs view
@@ -0,0 +1,17 @@+module Language.Nominal.EquivarSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.EquivarSpec++spec :: Spec+spec = do+    it "Atoms one orbit" $ property prop_atoms_one_orbit+    it "Two orbits of atoms pairs (equal, or distinct)" $ property prop_atomssq_orbit++
+ test/Language/Nominal/Examples/IdealisedEUTxOSpec.hs view
@@ -0,0 +1,40 @@+module Language.Nominal.Examples.IdealisedEUTxOSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.Examples.IdealisedEUTxOSpec++spec :: Spec+spec = do+    it "Sanity check: every arbitrary chunk is valid" $ property prop_arbitraryChunkIsValid +    it "Sanity check: every arbitrary chunk is valid (alternate test)" $ property prop_arbitraryChunkIsValid' +    it "Sanity check: not every chunk is a blockchain (might have UTxIs)" $ property prop_notEveryChunkBlockchain +    it "Sanity check: an arbitary transaction is indeed a transaction" $ property prop_arbitraryTxIsValid+    it "Sanity check: an arbitary blockchain is indeed a valid blockchain" $ property prop_arbitraryBlockchainIsValid+    it "Sanity check: arbitrary instance of TB generates a blockchain, which is equal to itself" $ property prop_blockchainToChunkAndBack +    it "Blockchain has no UTxIs" $ property prop_blockchainHasNoUTxIs +    describe "Chunk is equal to itself" $ do+        it "atValFin"  $ property $ prop_chunkrefl atValFin+        it "atValTriv" $ property $ prop_chunkrefl atValTriv+    it "There are two different chunks" $ property prop_chunkneq +    it "Empty chunk is prefix of any chunk" $ property prop_emptyIsPrefix +    it "The tail of a chunk, is a chunk" $ property prop_chunkTail_is_chunk +    it "The tail of a chunk, is a prefix of the original chunk" $ property prop_chunkTail_is_prefix+    it "The tail of a chunk, is a prefix of the original chunk.  Gotcha version, that doesn't have the Nom bindings: expect failure here" $ property prop_chunkTail_is_prefix_gotcha +    it "Plausible-but-wrong @'warningNotChunkTail'@ is wrong: expect failure here" $ property prop_warningNotChunkTail_is_not_chunk +    it "Underbinding check (not enough atoms bound)" $ property prop_underbinding+    it "Overbinding check (too many atoms bound)" $ property prop_overbinding+    it "Gotcha: Fails because loss of information from two Nom bindings" $ property prop_chunkHead_chunkTail_recombine +    it "Succeeds because one Nom binding thus no loss of information" $ property prop_chunkHdTl_recombine +    it "If you reverse the order of transactions in a chunk, it need not be valid" $ property prop_reverseIsNotValid +-- slow to run+--  it "Subchunks of a valid chunk, are valid chunks" $ property prop_subchunksValid +    it "If two transactions are apart, they can be validly combined" $ property prop_apart_is_valid_tx +    it "If two chunks are apart, they can be validly combined" $ property prop_apart_is_valid_ch +    it "If two chunks are apart, they can be validly commuted" $ property prop_chunk_apart_commutes+    it "Lemma 2.14(2)" $ property prop_validity_fresh
+ test/Language/Nominal/Examples/SystemFSpec.hs view
@@ -0,0 +1,38 @@+module Language.Nominal.Examples.SystemFSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.Examples.SystemFSpec++spec :: Spec+spec = do+    it "(id id) has no type (it needs a type argument)" $ property prop_untypeable+    describe "y[n-> var n] = y" $ do+        it "typevar'" $ property prop_sub_id_typevar'+        it "termvar" $ property prop_sub_id_termvar+        it "typevar" $ property prop_sub_id_typevar+    describe "n # y => y[n->x] = y" $ do+        it "typevar'" $ property prop_sub_fresh_typevar'+        it "typevar" $ property prop_sub_fresh_typevar+        it "termvar" $ property prop_sub_fresh_termvar+    describe "n' # y => y[n->n'] = (n' n).y" $ do+        it "typevar'" $ property prop_sub_perm_typevar'+        it "typevar''" $ property prop_sub_perm_typevar''+        it "termvar" $ property prop_sub_perm_termvar+    it "normal forms are typeable" $ property prop_typeable_nf+    it "typeable terms are normalisable" $ property prop_nf_typeable+    it "Type soundness: if a term is typeable and normalisable then its normal form has the same type as it does." $+        property prop_type_soundness+    it "Not all terms are typeable" $ property prop_all_typeable+    it "typeof(id t) = typeof(t)" $ property prop_id_type_unchanged+    it "If x : t then (id t x) --> x" $ property prop_app_id+    it "0 : nat" $ property prop_typeof_zero+    it "i+1 /= 0" $ property prop_church_numerals0+    it "i+1 /= i" $ property prop_church_numerals1+    it "i : nat" $ property prop_church_numerals_type+
+ test/Language/Nominal/NameSetSpec.hs view
@@ -0,0 +1,15 @@+module Language.Nominal.NameSetSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.NameSetSpec++spec :: Spec+spec = do+    it "ns disjoint ns', if apart" $ property prop_supp_apart+    it "ns disjoint ns' iff apart, if triv labels" $ property prop_supp_apart_atom
+ test/Language/Nominal/NameSpec.hs view
@@ -0,0 +1,22 @@+module Language.Nominal.NameSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.NameSpec++spec :: Spec+spec = do+    it "nameLabel (nameOverwriteLabel t n) == t" $ property prop_namelabel+    it "Not all names are equal (even with trivial labels)" $ property prop_twonames+    it "(n' n).x = x  (we expect this to fail)" $ property prop_singleswap+    it "n',n#x => (n' n).x = x.  Test on x a tuple" $ property prop_freshswap+    it "(n' n).(n' n).x = x" $ property prop_doubleswap+    it "n'',n'#x => (n'' n').(n' n).m = (n'' n).m" $ property prop_doubleswap_fresh'+    it "n'#x => (n'' n').(n' n).x = (n'' n).x" $ property prop_doubleswap_fresh+    it "(n' n).x = (n n').x" $ property prop_swap_symm+
+ test/Language/Nominal/NomSpec.hs view
@@ -0,0 +1,40 @@+module Language.Nominal.NomSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.NomSpec++spec :: Spec+spec = do+    it "Nom creates local binding, which is unpacked separately by equality." $ property prop_x_neq_x+    it "Check restriction creates local scope. Should return False." $ property prop_split_scope+    it "n' # n if n' is chosen fresh, after n" $ property prop_fresh_neq+    it "freshName () /= freshName (). Lazy evaluation means distinct fresh names generated." $ property prop_fresh_neq'+    it "Same thing using let." $ property prop_fresh_neq''+    it "But if we unpack a single fresh name monadically, we can compare it for equality." $ property prop_fresh_eq+    it "~ (n # (n,n'))" $ property prop_freshFor1+    it "n # n'" $ property prop_freshFor2+    it "Nom Maybe -> Maybe Nom -> Nom Maybe = id" $ property prop_transposeNomMaybe+    it "Maybe Nom -> Nom Maybe -> Maybe Nom = id" $ property prop_transposeMaybeNom+    it "a,b#x |- (a b).x = x" $ property prop_new'+    it "a#x |/- (a b).x = x" $ property prop_not_new'+    it "a,b#x |- (a b).x = x" $ property prop_new+    it "n#l iff n not in l, for n a name and l a list of names" $ property prop_freshFor_notElem+    it "atoms-restriction precisely removes atoms from support (atom list)" $ property prop_support_nom_atmlist +    it "atoms-restriction precisely removes atoms from support (nom of atom list)" $ property prop_support_nom_nomatmlist +    it "if we freshen all atoms in an element, its support is apart from the original (atom list)" $ property prop_freshen_apart_atmlist +    it "if we freshen all atoms in an element, its support is apart from the original (nom atom list)" $ property prop_freshen_apart_nom_atmlist +    it  "a freshened list of atoms is disjoint from its original" $ property prop_freshen_apart_disjoint +    it  "two notions of trivial Nom binding are equal" $ property prop_isTrivial_equal +    it  "isTrivial sanity check (supp version)" $ property prop_isTrivial_sane +    it  "isTrivial sanity check (freshFor version)" $ property prop_isTrivial_sane' +    it "Commute Nom and List" $ property prop_transposeNomList +    it "Commute Nom and Nom (one way)" $ property prop_transposeNomNom +--    it "Commute List and Nom" $ property prop_transposeListNom +--    it "Commute Nom and Nom (the other way)" $ property prop_transposeNomNom' +--    it "Commute Nom and Nom (two types of atom)" $ property prop_transposeNomNom''
+ test/Language/Nominal/SubSpec.hs view
@@ -0,0 +1,18 @@+module Language.Nominal.SubSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.SubSpec++spec :: Spec+spec = do+    it "[n1][n1 -> n2] = [n2]" $ property prop_sub_singleton1 +    it "[n2][n1 -> n2] = [n2]" $ property prop_sub_singleton2 +    it "n#n1,n2 ==> (n.x)[n1 -> n2] = n.(x[n1 -> n2])" $ property prop_sub_abs_1+    it "(n.x)[n1 -> n2] = n.(x[n1 -> n2]) fails in general" $ property prop_sub_abs_1' +    it "(n.x)[n -> n2] = n.x" $ property prop_sub_abs_3
+ test/Language/Nominal/UnifySpec.hs view
@@ -0,0 +1,22 @@+module Language.Nominal.UnifySpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.UnifySpec++spec :: Spec+spec = do+    it "l is not always unifiable with l', e.g. l = [] and l' nonempty" $ property prop_l_l'+    it "res ns' (res ns x)  unifiable with  res ns (res ns' x)" $ property prop_res_res+    it "x' -> ns x -> res ns x  unifies with x'" $ property prop_res_unres+    it "Unifiers correctly calculated" $ property prop_unify_ren+    it "idRen == idRen [a -> a] (equality is on nub)" $ property prop_renId+    it "Permutations and freshening renamings coincide (lists of lists of atoms)" $ property prop_fresh_ren_atmlistlist+    it "Permutations and freshening renamings coincide (abstractions of lists of atoms)" $ property prop_fresh_ren_absatmlist++
+ test/Language/Nominal/UtilitiesSpec.hs view
@@ -0,0 +1,16 @@+module Language.Nominal.UtilitiesSpec+    ( spec+    ) where++import Test.Hspec+import Test.QuickCheck++import Language.Nominal.Properties.SpecUtilities ()++import Language.Nominal.Properties.UtilitiesSpec++spec :: Spec+spec = do+    it "superSucc on [Int]" $ property prop_test_rewrite1+    it "superSucc on [Name Int]" $ property prop_test_rewrite2+
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}