diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,11 @@ +# Changelog for `covenant` + +All notable changes to this project will be documented in this file. + +The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). + +## UNRELEASED + +## 1.0.0 -- 08-05-2025 + +Initial version diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,35 @@ +# Covenant + +# What is this? + +Covenant is a standalone IR, designed as a target for front-end DSLs for writing +Cardano scripts. It uses [call-by-push-value][cbpv] and is +[Turner-total][turner-total], which gives it a high degree of analyzability. +Furthermore, it uses a fully hash-consed structure. + +# How do I use this? + +This is currently a work-in-progress. Begin with the documentation in +`Covenant.ASG` and `Covenant.Type`. + +# What do I need? + +Our policy is to support the latest three GHC versions; see the Cabal file's +`tested-with` field to see which exact versions are supported. This is enforced +using `get-tested` in our CI. + +We support only [Tier 1 platforms](https://gitlab.haskell.org/ghc/ghc/-/wikis/platforms#tier-1-platforms). +Covenant is developed using the lowest supported version. + +# License + +Covenant is licensed under Apache 2.0. Please see the `LICENSE` file for more +information. + +# References + +* [Catalyst proposal for + Covenant](https://projectcatalyst.io/funds/13/f13-cardano-open-developers/mlabs-static-analysis-with-covenant) + +[cbpv]: https://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf +[turner-total]: https://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf diff --git a/covenant.cabal b/covenant.cabal new file mode 100644 --- /dev/null +++ b/covenant.cabal @@ -0,0 +1,162 @@ +cabal-version: 3.0 +name: covenant +version: 1.0.0 +synopsis: Standalone IR for Cardano scripts. +description: + A library describing a call-by-push-value, Turner-total IR. Includes the ability to build up the IR programmatically. + +homepage: https://github.com/mlabs-haskell/covenant +license: Apache-2.0 +license-file: LICENSE +author: Koz Ross, Sean Hunter +maintainer: koz@mlabs.city, sean@mlabs.city +bug-reports: https://github.com/mlabs-haskell/covenant/issues +copyright: (C) MLabs 2024 +category: Covenant +tested-with: ghc ==9.8.4 || ==9.10.1 || ==9.12.1 +build-type: Simple +extra-source-files: + CHANGELOG.md + README.md + +-- Common sections +common lang + ghc-options: + -Wall + -Wcompat + -Wredundant-bang-patterns + -Wredundant-strictness-flags + -Wmissing-deriving-strategies + -Woperator-whitespace + -Wambiguous-fields + -Wmisplaced-pragmas + -Wmissing-export-lists + -Wmissing-import-lists + + default-extensions: + BangPatterns + BinaryLiterals + DataKinds + DeriveTraversable + DerivingVia + DuplicateRecordFields + EmptyCase + FlexibleContexts + FlexibleInstances + GeneralizedNewtypeDeriving + HexFloatLiterals + ImportQualifiedPost + InstanceSigs + KindSignatures + LambdaCase + MultiParamTypeClasses + NoFieldSelectors + NoStarIsType + NumericUnderscores + OverloadedLabels + OverloadedStrings + PackageImports + ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeApplications + TypeFamilies + TypeOperators + UndecidableInstances + + build-depends: base >=4.19.0.0 && <5 + default-language: Haskell2010 + +common test-lang + import: lang + ghc-options: + -O2 + -threaded + -rtsopts + -with-rtsopts=-N + + build-depends: + QuickCheck ==2.15.0.1, + covenant, + tasty ==1.5.3, + tasty-hunit ==0.10.2, + tasty-quickcheck ==0.11.1, + +common bench-lang + import: lang + ghc-options: -O2 + +-- Primary library +library + import: lang + exposed-modules: + Control.Monad.Action + Control.Monad.HashCons + Covenant.ASG + Covenant.Constant + Covenant.DeBruijn + Covenant.Index + Covenant.Prim + Covenant.Test + Covenant.Type + Covenant.Util + + other-modules: + Covenant.Internal.Rename + Covenant.Internal.Term + Covenant.Internal.Type + Covenant.Internal.Unification + + build-depends: + QuickCheck ==2.15.0.1, + acc ==0.2.0.3, + bimap ==0.5.0, + bytestring >=0.12.1.0 && <0.13, + containers >=0.6.8 && <0.8, + enummapset ==0.7.3.0, + mtl >=2.3.1 && <3, + nonempty-vector ==0.2.4, + optics-core ==0.4.1.1, + optics-extra ==0.4.2.1, + optics-th ==0.4.1, + prettyprinter ==1.7.1, + quickcheck-instances ==0.3.32, + quickcheck-transformer ==0.3.1.2, + text >=2.1.1 && <2.2, + transformers >=0.6.1.0 && <0.7.0.0, + vector ==0.13.2.0, + + hs-source-dirs: src + +-- Tests +test-suite renaming + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test/renaming + +test-suite type-applications + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + build-depends: vector + hs-source-dirs: test/type-applications + +test-suite primops + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + build-depends: nonempty-vector + hs-source-dirs: test/primops + +test-suite asg + import: test-lang + type: exitcode-stdio-1.0 + main-is: Main.hs + build-depends: + optics-core, + vector, + + hs-source-dirs: test/asg + +-- Benchmarks diff --git a/src/Control/Monad/Action.hs b/src/Control/Monad/Action.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Action.hs @@ -0,0 +1,287 @@ +{-# LANGUAGE FunctionalDependencies #-} + +-- | Module: Control.Monad.Action +-- +-- Monoid actions, and the update monad, as well as an @mtl@-style capability +-- type class. +-- +-- = A note on functional dependencies +-- +-- To ensure easy inference, we make use of functional dependencies (either +-- directly or by an equivalent mechanism on associated type families) on both +-- the 'Action' and 'MonadUpdate' type classes. Specifically, we insist that: +-- +-- 1. Any monoidal action determines the state it acts on; and +-- 2. Any particular stack that implements 'MonadUpdate' determines what its +-- action is. +-- +-- This means that any given action can act on _exactly_ one state, and that any +-- given stack has at most one state we can act upon. The second restriction +-- above is in line with the other similar @mtl@-style capability type classes +-- (such as @MonadReader@, @MonadState@ etc), while the first is a reasonable +-- choice given that we want to have both good inference and also the ability +-- for different actions to act on the same state. Given that actions are likely +-- to be fairly application-specific, we don't see this as a significant +-- limitation. +module Control.Monad.Action + ( -- * Monoid actions + + -- ** Class + Action (..), + + -- ** Wrapper + Actionable, + actionable, + + -- * Action monad + + -- ** Transformer + UpdateT (..), + runUpdateT, + + -- ** Capability type class + MonadUpdate (..), + ) +where + +import Acc (Acc) +import Control.Monad.Trans (MonadTrans (lift)) +import Control.Monad.Trans.Except (ExceptT) +import Control.Monad.Trans.Maybe (MaybeT) +import Control.Monad.Trans.RWS.CPS (RWST) +import Control.Monad.Trans.Reader (ReaderT) +import Control.Monad.Trans.State.Strict (StateT) +import Control.Monad.Trans.Writer.CPS (WriterT) +import Data.Functor (void) +import Data.Kind (Type) +import Data.Monoid (Endo, appEndo) + +-- | Describes (left) [monoidal actions on a +-- set](https://en.wikipedia.org/wiki/Semigroup_action). In this case, the type +-- @StateOf a@ is \'the state being acted on\' (or \'the state\'), while @a@ is +-- \'the thing doing the acting\' (or \'the action\'). +-- +-- = Laws +-- +-- Briefly, any instance of @'Action' a@ defines a [monoid +-- homomorphism](https://en.wikipedia.org/wiki/Monoid#Monoid_homomorphisms) +-- between @a@ and @'Endo' (StateOf a)@ (which is essentially @StateOf a -> +-- StateOf a)@. In Haskell terms, this means the following laws must hold: +-- +-- 1. @'act' 'mempty'@ @=@ @'mempty'@ +-- 2. @'act' x '<>' 'act' y@ @=@ @'act' (x '<>' y)@ +-- +-- @since 1.0.0 +class (Monoid a) => Action (a :: Type) where + type StateOf a :: Type + act :: a -> Endo (StateOf a) + +-- | Often, we want to take a type that doesn't (naturally) form a 'Monoid' and +-- use it as an action. This can be done using a range of \'free monoid +-- constructions\', including lists. However, these aren't optimal due to the +-- append-heavy (and concatenation-heavy) workloads we typically need from +-- actions. +-- +-- 'Actionable' is such a \'free monoid construction\' which \'promotes\' any +-- @a@ into a 'Semigroup' and a 'Monoid'. It is fairly opaque, providing only +-- the instances we really need, but it's designed for efficient appending and +-- concatenation. +-- +-- To use 'Actionable', you want to do something like this: +-- +-- @ +-- data MyState = ... +-- +-- data MyType = ... +-- +-- newtype MyAction = MyAction (Actionable MyType) +-- deriving (Semigroup, Monoid) via (Actionable MyType) +-- +-- instance Action MyAction where +-- type StateOf MyAction = MyState +-- act (MyAction acts) = foldMap go acts +-- where +-- go :: MyType -> Endo MyState +-- go x = Endo $ \oldState -> ... +-- @ +-- +-- To \'inject\' your type into an 'Actionable', use 'actionable'. +-- +-- @since 1.0.0 +newtype Actionable a = Actionable (Acc a) + deriving + ( -- | @since 1.0.0 + Semigroup, + -- | @since 1.0.0 + Monoid + ) + via Acc a + deriving + ( -- | @since 1.0.0 + Foldable + ) + via Acc + +-- | Wrap a value into an 'Actionable'. +-- +-- @since 1.0.0 +actionable :: a -> Actionable a +actionable = Actionable . pure + +-- | A transformer implementing the \'update monad\' pattern, as described +-- [here](https://www.schoolofhaskell.com/user/edwardk/heap-of-successes). +-- +-- We leave the state implicit, as it is uniquely determined by the @act@ type, +-- together with the 'Action' type class requirement. +-- +-- = Important note +-- +-- This implementation is not suitable for any @m@ that throws exceptions. This +-- includes @IO@, @ST@ and anything stacked atop them. For the reasons why, see +-- [here](https://github.com/haskell-effectful/effectful/blob/master/transformers.md#statet). +-- +-- @since 1.0.0 +newtype UpdateT (act :: Type) (m :: Type -> Type) (a :: Type) + = UpdateT (StateOf act -> m (act, a)) + deriving stock + ( -- | @since 1.0.0 + Functor + ) + +-- | @since 1.0.0 +instance (Action act, Monad m) => Applicative (UpdateT act m) where + {-# INLINEABLE pure #-} + pure x = UpdateT $ \_ -> pure (mempty, x) + {-# INLINEABLE (<*>) #-} + UpdateT fs <*> UpdateT xs = UpdateT $ \s -> do + (act1, f) <- fs s + let s' = appEndo (act act1) s + (act2, x) <- xs s' + pure (act1 <> act2, f x) + +-- | @since 1.0.0 +instance (Action act, Monad m) => Monad (UpdateT act m) where + {-# INLINEABLE (>>=) #-} + UpdateT xs >>= f = UpdateT $ \s -> do + (act1, x) <- xs s + let s' = appEndo (act act1) s + let (UpdateT applied) = f x + (act2, y) <- applied s' + pure (act1 <> act2, y) + +-- | @since 1.0.0 +instance (Action act) => MonadTrans (UpdateT act) where + {-# INLINEABLE lift #-} + lift comp = UpdateT $ \_ -> (mempty,) <$> comp + +-- | As 'runUpdate', except that it produces the results in the \'inner monad\' +-- of 'UpdateT'. +-- +-- @since 1.0.0 +runUpdateT :: + forall (act :: Type) (m :: Type -> Type) (a :: Type). + (Functor m, Action act) => + UpdateT act m a -> + StateOf act -> + m (StateOf act, act, a) +runUpdateT (UpdateT comp) s = + (\(act1, res) -> (appEndo (act act1) s, act1, res)) <$> comp s + +-- | An @mtl@-style capability type class describing update monads in general, +-- irrespective of their states and/or actions. +-- +-- = Laws +-- +-- 1. @'send' x 'Control.Applicative.*>' 'send' y@ @=@ @'send' (x '<>' y)@ +-- +-- If you define 'update' or 'request', ensure the following also hold: +-- +-- 2. @'update' 'mempty'@ @=@ @'pure' ()@ +-- 3. @'request' 'Control.Applicative.*>' 'request'@ @=@ @'request'@ +-- 4. @'update'@ @=@ @'void' '.' 'send'@ +-- 5. @'request'@ @=@ @'send' 'mempty'@ +-- +-- Laws 4 and 5 form the default definitions of 'update' and 'request' +-- respectively, which obey all these laws. +-- +-- @since 1.0.0 +class (Action act, Monad m) => MonadUpdate act m | m -> act where + -- | Performs the given action on the state, returning the result. + -- + -- @since 1.0.0 + send :: act -> m (StateOf act) + + -- | Performs the given action, returning nothing. + -- + -- @since 1.0.0 + {-# INLINEABLE update #-} + update :: act -> m () + update = void . send + + -- | Retrieves the state without doing anything to it. + -- + -- @since 1.0.0 + {-# INLINEABLE request #-} + request :: m (StateOf act) + request = send (mempty :: act) + + {-# MINIMAL send #-} + +-- | @since 1.0.0 +instance (Action act, Monad m) => MonadUpdate act (UpdateT act m) where + {-# INLINEABLE send #-} + send x = UpdateT $ \s -> pure (x, appEndo (act x) s) + +-- | @since 1.0.0 +instance (MonadUpdate act m) => MonadUpdate act (ReaderT r m) where + {-# INLINEABLE send #-} + send = lift . send + {-# INLINEABLE update #-} + update = lift . update + {-# INLINEABLE request #-} + request = lift request + +-- | @since 1.0.0 +instance (MonadUpdate act m) => MonadUpdate act (MaybeT m) where + {-# INLINEABLE send #-} + send = lift . send + {-# INLINEABLE update #-} + update = lift . update + {-# INLINEABLE request #-} + request = lift request + +-- | @since 1.0.0 +instance (MonadUpdate act m) => MonadUpdate act (StateT s m) where + {-# INLINEABLE send #-} + send = lift . send + {-# INLINEABLE update #-} + update = lift . update + {-# INLINEABLE request #-} + request = lift request + +-- | @since 1.0.0 +instance (MonadUpdate act m) => MonadUpdate act (WriterT w m) where + {-# INLINEABLE send #-} + send = lift . send + {-# INLINEABLE update #-} + update = lift . update + {-# INLINEABLE request #-} + request = lift request + +-- | @since 1.0.0 +instance (MonadUpdate act m) => MonadUpdate act (RWST r w s m) where + {-# INLINEABLE send #-} + send = lift . send + {-# INLINEABLE update #-} + update = lift . update + {-# INLINEABLE request #-} + request = lift request + +-- | @since 1.0.0 +instance (MonadUpdate act m) => MonadUpdate act (ExceptT e m) where + {-# INLINEABLE send #-} + send = lift . send + {-# INLINEABLE update #-} + update = lift . update + {-# INLINEABLE request #-} + request = lift request diff --git a/src/Control/Monad/HashCons.hs b/src/Control/Monad/HashCons.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/HashCons.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE FunctionalDependencies #-} + +-- | Module: Control.Monad.HashCons +-- +-- Provides a transformer, and a capability type class in the style of @mtl@, +-- for hash consing. See the Covenant wiki for how this works. +module Control.Monad.HashCons + ( -- * Transformer + HashConsT, + runHashConsT, + hashCons, + lookupRef_, + + -- * Capability type class + MonadHashCons (..), + ) +where + +import Control.Monad.State.Strict + ( StateT, + get, + modify, + runStateT, + ) +import Control.Monad.Trans (MonadTrans (lift)) +import Control.Monad.Trans.Except (ExceptT) +import Control.Monad.Trans.Maybe (MaybeT) +import Control.Monad.Trans.RWS.CPS (RWST) +import Control.Monad.Trans.Reader (ReaderT) +import Control.Monad.Trans.Writer.CPS (WriterT) +import Data.Bimap (Bimap) +import Data.Bimap qualified as Bimap +import Data.Kind (Type) + +-- | A transformer implementing hash consing capabilities, with references of +-- type @r@ and referents of type @e@. It is assumed that values of type @e@ +-- contain values of type @r@ in their capacity as references, though this is +-- not a requirement of this transformer. +-- +-- = Important note +-- +-- This implementation is not suitable for any @m@ that throws exceptions. This +-- includes @IO@, @ST@ and anything stacked atop them. For the reasons why, see +-- [here](https://github.com/haskell-effectful/effectful/blob/master/transformers.md#statet). +-- +-- @since 1.0.0 +newtype HashConsT (r :: Type) (e :: Type) (m :: Type -> Type) (a :: Type) + = HashConsT (StateT (Bimap r e) m a) + deriving + ( -- | @since 1.0.0 + Functor, + -- | @since 1.0.0 + Applicative, + -- | @since 1.0.0 + Monad + ) + via (StateT (Bimap r e) m) + deriving + ( -- | @since 1.0.0 + MonadTrans + ) + via StateT (Bimap r e) + +-- | Execute the computation described, returning both the result and the unique +-- pairings of @r@ and @e@ produced as part of it. +-- +-- @since 1.0.0 +runHashConsT :: + forall (r :: Type) (e :: Type) (m :: Type -> Type) (a :: Type). + HashConsT r e m a -> + m (a, Bimap r e) +runHashConsT (HashConsT comp) = runStateT comp Bimap.empty + +-- | Given a value of type @e@, produce the unique value of type @r@ acting as a +-- reference to it. This @r@ will be cached, ensuring any future requests for +-- the reference for this value of type @e@ will be the same. +-- +-- @since 1.0.0 +hashCons :: + forall (r :: Type) (e :: Type) (m :: Type -> Type). + (Ord r, Ord e, Bounded r, Enum r, Monad m) => + e -> + HashConsT r e m r +hashCons x = HashConsT $ do + binds <- get + case Bimap.lookupR x binds of + Nothing -> + if Bimap.null binds + then minBound <$ modify (Bimap.insert minBound x) + else do + let largestOldRef = fst . Bimap.findMax $ binds + let newRef = succ largestOldRef + newRef <$ modify (Bimap.insert newRef x) + Just ref -> pure ref + +-- | Given a value of type @r@, fetch the cached @e@ value, if it exists. +-- +-- @since 1.0.0 +lookupRef_ :: + forall (r :: Type) (e :: Type) (m :: Type -> Type). + (Monad m, Ord e, Ord r) => + r -> + HashConsT r e m (Maybe e) +lookupRef_ r = HashConsT (Bimap.lookup r <$> get) + +-- | An @mtl@-style capability type class for hash consing capability, using +-- references of type @r@ and values of type @e@. +-- +-- = Laws +-- +-- 1. @'refTo' x '>>' 'refTo' x@ @=@ @'refTo' x@ +-- 2. @'liftA2' ('/=') ('refTo' x) ('refTo' y)@ @=@ @'refTo' x '*>' 'refTo' y '*>' 'pure' (x '/=' y)@ +-- 3. @'refTo' x '>>=' (\\r -> 'lookupRef' r '>>=' (\\y -> 'pure' (y, r)))@ @=@ @('Just' x, ) '<$>' 'refTo' x@ +-- +-- @since 1.0.0 +class + (Eq e, Eq r, Monad m) => + MonadHashCons (r :: Type) (e :: Type) (m :: Type -> Type) + | m -> e r + where + -- | Produce the unique value of type @r@ that acts as a reference for the + -- given value of type @e@. + -- + -- @since 1.0.0 + refTo :: e -> m r + + -- | Given a value of type @r@, fetch the cached value of type @e@. + -- + -- @since 1.0.0 + lookupRef :: r -> m (Maybe e) + +-- | @since 1.0.0 +instance (Ord r, Ord e, Bounded r, Enum r, Monad m) => MonadHashCons r e (HashConsT r e m) where + {-# INLINEABLE refTo #-} + refTo = hashCons + {-# INLINEABLE lookupRef #-} + lookupRef = lookupRef_ + +-- | @since 1.0.0 +instance (Ord r, Ord e, MonadHashCons r e m) => MonadHashCons r e (MaybeT m) where + {-# INLINEABLE refTo #-} + refTo e = lift (refTo e) + {-# INLINEABLE lookupRef #-} + lookupRef r = lift (lookupRef r) + +-- | @since 1.0.0 +instance (MonadHashCons r e m) => MonadHashCons r e (ReaderT r' m) where + {-# INLINEABLE refTo #-} + refTo e = lift (refTo e) + {-# INLINEABLE lookupRef #-} + lookupRef r = lift (lookupRef r) + +-- | @since 1.0.0 +instance (MonadHashCons r e m) => MonadHashCons r e (StateT s m) where + {-# INLINEABLE refTo #-} + refTo e = lift (refTo e) + {-# INLINEABLE lookupRef #-} + lookupRef r = lift (lookupRef r) + +-- | @since 1.0.0 +instance (MonadHashCons r e m) => MonadHashCons r e (WriterT w m) where + {-# INLINEABLE refTo #-} + refTo e = lift (refTo e) + {-# INLINEABLE lookupRef #-} + lookupRef r = lift (lookupRef r) + +-- | @since 1.0.0 +instance (MonadHashCons r e m) => MonadHashCons r e (RWST r' w s m) where + {-# INLINEABLE refTo #-} + refTo e = lift (refTo e) + {-# INLINEABLE lookupRef #-} + lookupRef r = lift (lookupRef r) + +-- | @since 1.0.0 +instance (MonadHashCons r e m) => MonadHashCons r e (ExceptT e' m) where + {-# INLINEABLE refTo #-} + refTo e = lift (refTo e) + {-# INLINEABLE lookupRef #-} + lookupRef r = lift (lookupRef r) diff --git a/src/Covenant/ASG.hs b/src/Covenant/ASG.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/ASG.hs @@ -0,0 +1,621 @@ +{-# LANGUAGE PatternSynonyms #-} + +-- | +-- Module: Covenant.ASG +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- The Covenant ASG, and ways to programmatically build it. +-- +-- = Note +-- +-- We use the term \'ASG\' to refer to \'abstract syntax graph\'. This is +-- because Covenant uses hash consing to ensure duplicate nodes do not exist, +-- thus producing a DAG structure, rather than a tree. +-- +-- @since 1.0.0 +module Covenant.ASG + ( -- * The ASG itself + + -- ** Types + ASG, + + -- ** Functions + topLevelNode, + nodeAt, + + -- * ASG components + + -- ** Types + Id, + Ref (..), + Arg, + CompNodeInfo + ( Builtin1, + Builtin2, + Builtin3, + Lam, + Force, + Return + ), + ValNodeInfo (Lit, App, Thunk), + ASGNode (..), + + -- ** Functions + typeASGNode, + + -- * ASG builder + + -- ** Types + CovenantError (..), + ScopeInfo, + ASGBuilder, + CovenantTypeError + ( BrokenIdReference, + ForceCompType, + ForceNonThunk, + ForceError, + ThunkValType, + ThunkError, + ApplyToValType, + ApplyToError, + ApplyCompType, + RenameFunctionFailed, + RenameArgumentFailed, + NoSuchArgument, + ReturnCompType, + LambdaResultsInValType, + LambdaResultsInNonReturn, + ReturnWrapsError, + ReturnWrapsCompType, + WrongReturnType, + UnificationError + ), + RenameError + ( InvalidAbstractionReference, + IrrelevantAbstraction, + UndeterminedAbstraction + ), + + -- ** Introducers + arg, + builtin1, + builtin2, + builtin3, + force, + ret, + lam, + err, + lit, + thunk, + app, + + -- ** Elimination + runASGBuilder, + ) +where + +import Control.Monad.Except + ( ExceptT, + MonadError (throwError), + runExceptT, + ) +import Control.Monad.HashCons + ( HashConsT, + MonadHashCons (lookupRef, refTo), + runHashConsT, + ) +import Control.Monad.Reader + ( MonadReader (local), + ReaderT, + asks, + runReaderT, + ) +import Covenant.Constant (AConstant, typeConstant) +import Covenant.DeBruijn (DeBruijn, asInt) +import Covenant.Index (Index, count0, intIndex) +import Covenant.Internal.Rename + ( RenameError + ( InvalidAbstractionReference, + IrrelevantAbstraction, + UndeterminedAbstraction + ), + renameCompT, + renameValT, + runRenameM, + undoRename, + ) +import Covenant.Internal.Term + ( ASGNode (ACompNode, AValNode, AnError), + ASGNodeType (CompNodeType, ErrorNodeType, ValNodeType), + Arg (Arg), + CompNodeInfo + ( Builtin1Internal, + Builtin2Internal, + Builtin3Internal, + ForceInternal, + LamInternal, + ReturnInternal + ), + CovenantTypeError + ( ApplyCompType, + ApplyToError, + ApplyToValType, + BrokenIdReference, + ForceCompType, + ForceError, + ForceNonThunk, + LambdaResultsInNonReturn, + LambdaResultsInValType, + NoSuchArgument, + RenameArgumentFailed, + RenameFunctionFailed, + ReturnCompType, + ReturnWrapsCompType, + ReturnWrapsError, + ThunkError, + ThunkValType, + UnificationError, + WrongReturnType + ), + Id, + Ref (AnArg, AnId), + ValNodeInfo (AppInternal, LitInternal, ThunkInternal), + typeASGNode, + typeId, + typeRef, + ) +import Covenant.Internal.Type + ( AbstractTy, + CompT (CompT), + CompTBody (CompTBody), + Renamed, + ValT (ThunkT), + ) +import Covenant.Internal.Unification (checkApp) +import Covenant.Prim + ( OneArgFunc, + ThreeArgFunc, + TwoArgFunc, + typeOneArgFunc, + typeThreeArgFunc, + typeTwoArgFunc, + ) +import Data.Bimap (Bimap) +import Data.Bimap qualified as Bimap +import Data.Coerce (coerce) +import Data.Functor.Identity (Identity, runIdentity) +import Data.Kind (Type) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Maybe (fromJust) +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Data.Vector.NonEmpty qualified as NonEmpty +import Optics.Core + ( A_Lens, + LabelOptic (labelOptic), + ix, + lens, + over, + preview, + review, + (%), + ) + +-- | A fully-assembled Covenant ASG. +-- +-- @since 1.0.0 +newtype ASG = ASG (Id, Map Id ASGNode) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Show + ) + +-- Note (Koz, 24/04/25): The `topLevelNode` and `nodeAt` functions use `fromJust`, +-- because we can guarantee it's impossible to miss. For an end user, the only +-- way to get hold of an `Id` is by inspecting a node, and since we control how +-- these are built and assigned, and users can't change them, it's safe. +-- +-- It is technically possible to escape this safety regime by having two +-- different `ASG`s and mixing up their `Id`s. However, this is both vanishingly +-- unlikely and probably not worth trying to protect against, given the nuisance +-- of having to work in `Maybe` all the time. + +-- | Retrieves the top-level node of an ASG. +-- +-- @since 1.0.0 +topLevelNode :: ASG -> ASGNode +topLevelNode asg@(ASG (rootId, _)) = nodeAt rootId asg + +-- | Given an 'Id' and an ASG, produces the node corresponding to that 'Id'. +-- +-- = Important note +-- +-- This is only safe to use if the 'Id' comes from a node in the argument 'ASG'. +-- 'Id's valid in one ASG are not likely to be valid in another. \'Mixing +-- and matching\' 'Id's from different ASGs will at best produce unexpected +-- results, and at worst will crash. You have been warned. +-- +-- @since 1.0.0 +nodeAt :: Id -> ASG -> ASGNode +nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings + +-- | A tracker for scope-related information while building an ASG +-- programmatically. Currently only tracks available arguments. +-- +-- = Important note +-- +-- This is a fairly low-level type, designed specifically for ASG construction. +-- While you can do arbitrary things with it, changing things in it outside of +-- the functionality provided by this module is not recommended, unless you know +-- /exactly/ what you're doing. +-- +-- @since 1.0.0 +newtype ScopeInfo = ScopeInfo (Vector (Vector (ValT AbstractTy))) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Show + ) + +-- | Gives access to the argument information for the current, and all +-- enclosing, scopes. The \'outer\' 'Vector' is a stack of scopes, with lower +-- indexes corresponding to closer scopes: index 0 is our scope, 1 is our +-- enclosing scope, 2 is the enclosing scope of our enclosing scope, etc. The +-- \'inner\' 'Vector's are positional lists of argument types. +-- +-- @since 1.0.0 +instance + (k ~ A_Lens, a ~ Vector (Vector (ValT AbstractTy)), b ~ Vector (Vector (ValT AbstractTy))) => + LabelOptic "argumentInfo" k ScopeInfo ScopeInfo a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = lens coerce (\_ v -> ScopeInfo v) + +-- | A Plutus primop with one argument. +-- +-- @since 1.0.0 +pattern Builtin1 :: OneArgFunc -> CompNodeInfo +pattern Builtin1 f <- Builtin1Internal f + +-- | A Plutus primop with two arguments. +-- +-- @since 1.0.0 +pattern Builtin2 :: TwoArgFunc -> CompNodeInfo +pattern Builtin2 f <- Builtin2Internal f + +-- | A Plutus primop with three arguments. +-- +-- @since 1.0.0 +pattern Builtin3 :: ThreeArgFunc -> CompNodeInfo +pattern Builtin3 f <- Builtin3Internal f + +-- | Force a thunk back into the computation it wraps. +-- +-- @since 1.0.0 +pattern Force :: Ref -> CompNodeInfo +pattern Force r <- ForceInternal r + +-- | Produce the result of a computation. +-- +-- @since 1.0.0 +pattern Return :: Ref -> CompNodeInfo +pattern Return r <- ReturnInternal r + +-- | A lambda. +-- +-- @since 1.0.0 +pattern Lam :: Id -> CompNodeInfo +pattern Lam i <- LamInternal i + +{-# COMPLETE Builtin1, Builtin2, Builtin3, Force, Return, Lam #-} + +-- | A compile-time literal of a flat builtin type. +-- +-- @since 1.0.0 +pattern Lit :: AConstant -> ValNodeInfo +pattern Lit c <- LitInternal c + +-- | An application of a computation (the 'Id' field) to some arguments (the +-- 'Vector' field). +-- +-- @since 1.0.0 +pattern App :: Id -> Vector Ref -> ValNodeInfo +pattern App f args <- AppInternal f args + +-- | Wrap a computation into a value (essentially delaying it). +-- +-- @since 1.0.0 +pattern Thunk :: Id -> ValNodeInfo +pattern Thunk i <- ThunkInternal i + +{-# COMPLETE Lit, App, Thunk #-} + +-- | Any problem that might arise when building an ASG programmatically. +-- +-- @since 1.0.0 +data CovenantError + = -- | There was a type error when assembling the ASG. This provides the + -- hash-consed state up to the point of the error. + -- + -- @since 1.0.0 + TypeError (Bimap Id ASGNode) CovenantTypeError + | -- | We tried to generate an ASG with no nodes in it. + -- + -- @since 1.0.0 + EmptyASG + | -- | We tried to generate as ASG whose top-level node is an error. + -- + -- @since 1.0.0 + TopLevelError + | -- | We tried to generate an ASG whose top-level node is a value. + -- + -- @since 1.0.0 + TopLevelValue (Bimap Id ASGNode) (ValT AbstractTy) ValNodeInfo + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Show + ) + +-- | A concrete monadic stack, providing the minimum amount of functionality +-- needed to build an ASG using the combinators given in this module. +-- +-- @since 1.0.0 +newtype ASGBuilder (a :: Type) + = ASGBuilder (ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a) + deriving + ( -- | @since 1.0.0 + Functor, + -- | @since 1.0.0 + Applicative, + -- | @since 1.0.0 + Monad, + -- | @since 1.0.0 + MonadReader ScopeInfo, + -- | @since 1.0.0 + MonadError CovenantTypeError, + -- | @since 1.0.0 + MonadHashCons Id ASGNode + ) + via ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) + +-- | Executes an 'ASGBuilder' to make a \'finished\' ASG. +-- +-- @since 1.0.0 +runASGBuilder :: + forall (a :: Type). + ASGBuilder a -> + Either CovenantError ASG +runASGBuilder (ASGBuilder comp) = + case runIdentity . runHashConsT . runExceptT . runReaderT comp . ScopeInfo $ Vector.empty of + (result, bm) -> case result of + Left err' -> Left . TypeError bm $ err' + Right _ -> case Bimap.size bm of + 0 -> Left EmptyASG + _ -> do + let (i, rootNode') = Bimap.findMax bm + case rootNode' of + AnError -> Left TopLevelError + ACompNode _ _ -> pure . ASG $ (i, Bimap.toMap bm) + AValNode t info -> Left . TopLevelValue bm t $ info + +-- | Given a scope and a positional argument index, construct that argument. +-- Will fail if that argument doesn't exist in the specified scope, or if the +-- specified scope doesn't exist. +-- +-- @since 1.0.0 +arg :: + forall (m :: Type -> Type). + (MonadError CovenantTypeError m, MonadReader ScopeInfo m) => + DeBruijn -> + Index "arg" -> + m Arg +arg scope index = do + let scopeAsInt = asInt scope + let indexAsInt = review intIndex index + lookedUp <- asks (preview (#argumentInfo % ix scopeAsInt % ix indexAsInt)) + case lookedUp of + Nothing -> throwError . NoSuchArgument scope $ index + Just t -> pure . Arg scope index $ t + +-- | Construct a node corresponding to the given Plutus primop. +-- +-- @since 1.0.0 +builtin1 :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m) => + OneArgFunc -> + m Id +builtin1 bi = do + let node = ACompNode (typeOneArgFunc bi) . Builtin1Internal $ bi + refTo node + +-- | As 'builtin1', but for two-argument primops. +-- +-- @since 1.0.0 +builtin2 :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m) => + TwoArgFunc -> + m Id +builtin2 bi = do + let node = ACompNode (typeTwoArgFunc bi) . Builtin2Internal $ bi + refTo node + +-- | As 'builtin1', but for three-argument primops. +-- +-- @since 1.0.0 +builtin3 :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m) => + ThreeArgFunc -> + m Id +builtin3 bi = do + let node = ACompNode (typeThreeArgFunc bi) . Builtin3Internal $ bi + refTo node + +-- | Given a reference to a thunk, turn it back into a computation. Will fail if +-- the reference isn't a thunk. +-- +-- @since 1.0.0 +force :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Ref -> + m Id +force r = do + refT <- typeRef r + case refT of + ValNodeType t -> case t of + ThunkT compT -> refTo . ACompNode compT . ForceInternal $ r + _ -> throwError . ForceNonThunk $ t + CompNodeType t -> throwError . ForceCompType $ t + ErrorNodeType -> throwError ForceError + +-- | Given the result of a function body (either a value or an error), construct +-- the return for it. Will fail if that reference aims at a computation node. +-- +-- @since 1.0.0 +ret :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Ref -> + m Id +ret r = do + refT <- typeRef r + case refT of + ValNodeType t -> do + let t' = CompT count0 . CompTBody . NonEmpty.singleton $ t + refTo . ACompNode t' . ReturnInternal $ r + CompNodeType t -> throwError . ReturnCompType $ t + ErrorNodeType -> err + +-- | Given a desired type, and a computation which will construct a lambda body +-- when executed (with the scope extended with the arguments the functions can +-- expect), construct a lambda. +-- +-- = Important note +-- +-- This combinator works slightly differently to the others in this module. This +-- is required because, due to hash consing, an ASG is typically built +-- \'bottom-up\', whereas function arguments (and their scopes) are necessarily +-- top-down. Thus, we need to \'delay\' the construction of a lambda's body to +-- ensure that proper scoped argument information can be given to it, hence why +-- the argument being passed is an @m Id@. +-- +-- @since 1.0.0 +lam :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ScopeInfo m) => + CompT AbstractTy -> + m Id -> + m Id +lam expectedT@(CompT _ (CompTBody xs)) bodyComp = do + let (args, resultT) = NonEmpty.unsnoc xs + bodyId <- local (over #argumentInfo (Vector.cons args)) bodyComp + bodyNode <- lookupRef bodyId + case bodyNode of + Nothing -> throwError . BrokenIdReference $ bodyId + -- This unifies with anything, so we're fine + Just AnError -> refTo . ACompNode expectedT . LamInternal $ bodyId + Just (ACompNode t specs) -> case specs of + ReturnInternal r -> do + rT <- typeRef r + case rT of + -- Note (Koz, 17/04/2025): I am not 100% sure about this, but I can't + -- see how anything else would make sense. + ValNodeType actualT -> + if resultT == actualT + then refTo . ACompNode expectedT . LamInternal $ bodyId + else throwError . WrongReturnType resultT $ actualT + ErrorNodeType -> throwError ReturnWrapsError -- Should be impossible + CompNodeType t' -> throwError . ReturnWrapsCompType $ t' + _ -> throwError . LambdaResultsInNonReturn $ t + Just (AValNode t _) -> throwError . LambdaResultsInValType $ t + +-- | Construct the error node. +-- +-- @since 1.0.0 +err :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m) => + m Id +err = refTo AnError + +-- | Given an 'Id' referring to a computation, and a 'Vector' of 'Ref's to the +-- desired arguments, construct the application of the arguments to that +-- computation. This can fail for a range of reasons: +-- +-- * Type mismatch between what the computation expects and what it's given +-- * Too many or too few arguments +-- * Not a computation type for 'Id' argument +-- * Not value types for 'Ref's +-- +-- @since 1.0.0 +app :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Id -> + Vector Ref -> + m Id +app fId argRefs = do + lookedUp <- typeId fId + case lookedUp of + CompNodeType fT -> case runRenameM . renameCompT $ fT of + Left err' -> throwError . RenameFunctionFailed fT $ err' + Right renamedFT -> do + renamedArgs <- traverse renameArg argRefs + case checkApp renamedFT . Vector.toList $ renamedArgs of + Left err' -> throwError . UnificationError $ err' + Right result -> do + let restored = undoRename result + refTo . AValNode restored . AppInternal fId $ argRefs + ValNodeType t -> throwError . ApplyToValType $ t + ErrorNodeType -> throwError ApplyToError + +-- | Construct a node corresponding to the given constant. +-- +-- @since 1.0.0 +lit :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m) => + AConstant -> + m Id +lit c = refTo . AValNode (typeConstant c) . LitInternal $ c + +-- | Given an 'Id' referring to a computation, build a thunk wrapping it. Will +-- fail if the 'Id' does not refer to a computation node. +-- +-- @since 1.0.0 +thunk :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Id -> + m Id +thunk i = do + idT <- typeId i + case idT of + CompNodeType t -> refTo . AValNode (ThunkT t) . ThunkInternal $ i + ValNodeType t -> throwError . ThunkValType $ t + ErrorNodeType -> throwError ThunkError + +-- Helpers + +renameArg :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Ref -> m (Maybe (ValT Renamed)) +renameArg r = + typeRef r >>= \case + CompNodeType t -> throwError . ApplyCompType $ t + ValNodeType t -> case runRenameM . renameValT $ t of + Left err' -> throwError . RenameArgumentFailed t $ err' + Right renamed -> pure . Just $ renamed + ErrorNodeType -> pure Nothing diff --git a/src/Covenant/Constant.hs b/src/Covenant/Constant.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Constant.hs @@ -0,0 +1,83 @@ +-- | +-- Module: Covenant.Constant +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- Representation of Plutus constants in Covenant. +-- +-- @since 1.0.0 +module Covenant.Constant + ( -- * Types + AConstant (..), + + -- * Functions + typeConstant, + ) +where + +import Covenant.Internal.Type + ( BuiltinFlatT (BoolT, ByteStringT, IntegerT, StringT, UnitT), + ValT (BuiltinFlat), + ) +import Data.ByteString (ByteString) +import Data.Kind (Type) +import Data.Text (Text) +import Test.QuickCheck + ( Arbitrary (arbitrary, shrink), + oneof, + ) +import Test.QuickCheck.Instances.ByteString () +import Test.QuickCheck.Instances.Text () +import Test.QuickCheck.Instances.Vector () + +-- | A Plutus constant term. +-- +-- @since 1.0.0 +data AConstant + = AUnit + | ABoolean Bool + | AnInteger Integer + | AByteString ByteString + | AString Text + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | @since 1.0.0 +instance Arbitrary AConstant where + {-# INLINEABLE arbitrary #-} + arbitrary = + oneof + [ pure AUnit, + ABoolean <$> arbitrary, + AnInteger <$> arbitrary, + AByteString <$> arbitrary, + AString <$> arbitrary + ] + {-# INLINEABLE shrink #-} + shrink = \case + AUnit -> [] + ABoolean b -> ABoolean <$> shrink b + AnInteger i -> AnInteger <$> shrink i + AByteString bs -> AByteString <$> shrink bs + AString t -> AString <$> shrink t + +-- | Produce the type of a given constant. +-- +-- @since 1.0.0 +typeConstant :: + forall (a :: Type). + AConstant -> ValT a +typeConstant = + BuiltinFlat . \case + AUnit -> UnitT + ABoolean _ -> BoolT + AnInteger _ -> IntegerT + AByteString _ -> ByteStringT + AString _ -> StringT diff --git a/src/Covenant/DeBruijn.hs b/src/Covenant/DeBruijn.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/DeBruijn.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} + +-- | +-- Module: Covenant.DeBruijn +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- DeBruijn indexing type and helpers. These are mainly used for scope tracking. +module Covenant.DeBruijn + ( DeBruijn (Z, S), + asInt, + ) +where + +import Control.Monad (guard) +import Data.Coerce (coerce) +import Data.List.NonEmpty (NonEmpty) +import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum)) +import Data.Word (Word32) +import Test.QuickCheck (Arbitrary) + +-- | A DeBruijn index. +-- +-- @since 1.0.0 +newtype DeBruijn = DeBruijn Word32 + deriving + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Arbitrary + ) + via Word32 + deriving stock + ( -- | @since 1.0.0 + Show + ) + +-- | Enables some manner of arithmetic with 'DeBruijn's. In this case, '<>' is +-- analogous to '+', while @'stimes' b@ is analogous to scalar multiplication by +-- @b@. Note that 'DeBruijn's cannot be scaled by negative numbers. +-- +-- @since 1.0.0 +instance Semigroup DeBruijn where + {-# INLINEABLE (<>) #-} + DeBruijn x <> DeBruijn y = DeBruijn (x + y) + {-# INLINEABLE sconcat #-} + sconcat = DeBruijn . sum . coerce @(NonEmpty DeBruijn) @(NonEmpty Word32) + {-# INLINEABLE stimes #-} + stimes b = DeBruijn . coerce . stimes b . coerce @_ @(Sum Word32) + +-- | @since 1.0.0 +instance Monoid DeBruijn where + {-# INLINEABLE mempty #-} + mempty = Z + +-- | The zero index. +-- +-- @since 1.0.0 +pattern Z :: DeBruijn +pattern Z <- DeBruijn 0 + where + Z = DeBruijn 0 + +-- | Successor to an index. +-- +-- @since 1.0.0 +pattern S :: DeBruijn -> DeBruijn +pattern S x <- (reduce -> Just x) + where + S (DeBruijn x) = DeBruijn (x + 1) + +{-# COMPLETE Z, S #-} + +-- | Convert a DeBruijn index into a (non-negative) 'Int'. +-- +-- @since 1.0.0 +asInt :: DeBruijn -> Int +asInt (DeBruijn i) = fromIntegral i + +-- Helpers + +reduce :: DeBruijn -> Maybe DeBruijn +reduce (DeBruijn x) = DeBruijn (x - 1) <$ guard (x > 0) diff --git a/src/Covenant/Index.hs b/src/Covenant/Index.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Index.hs @@ -0,0 +1,172 @@ +{-# LANGUAGE RoleAnnotations #-} + +-- | +-- Module: Covenant.Index +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- Positional indexes, starting from 0, and cardinality indicators. +-- +-- @since 1.0.0 +module Covenant.Index + ( Index, + Count, + intIndex, + intCount, + ix0, + count0, + ix1, + count1, + ix2, + count2, + ix3, + count3, + ) +where + +import Data.Bits (toIntegralSized) +import Data.Coerce (coerce) +import Data.List.NonEmpty (NonEmpty) +import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum)) +import Data.Word (Word32) +import GHC.TypeLits (Symbol) +import Optics.Prism (Prism', prism) +import Test.QuickCheck (Arbitrary) + +-- | A positional index, starting from zero. The label allows distinguishing +-- different flavours of indices. +-- +-- @since 1.0.0 +newtype Index (ofWhat :: Symbol) = Index Word32 + deriving + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Arbitrary + ) + via Word32 + deriving stock + ( -- | @since 1.0.0 + Show + ) + +type role Index nominal + +-- | Enables some manner of arithmetic with 'Index'ess. In this case, '<>' is +-- analogous to '+', while @'stimes' b@ is analogous to scalar multiplication by +-- @b@. Note that 'Index'es cannot be scaled by negative numbers. +-- +-- @since 1.0.0 +instance Semigroup (Index ofWhat) where + {-# INLINEABLE (<>) #-} + Index x <> Index y = Index (x + y) + {-# INLINEABLE sconcat #-} + sconcat = Index . sum . coerce @(NonEmpty (Index ofWhat)) @(NonEmpty Word32) + {-# INLINEABLE stimes #-} + stimes b = Index . coerce . stimes b . coerce @_ @(Sum Word32) + +-- | @since 1.0.0 +instance Monoid (Index ofWhat) where + {-# INLINEABLE mempty #-} + mempty = Index 0 + +-- | Helper to construct, and convert, 'Index'es and 'Int's. This is needed +-- because unfortunately, the standard Haskell practice is to use 'Int' for +-- indexes. +-- +-- To use this, do one of the following: +-- +-- * Construct with @'preview'@: for example, @'preview' intIndex 1@. +-- * Destruct with @'review'@. +-- +-- @since 1.0.0 +intIndex :: forall (ofWhat :: Symbol). Prism' Int (Index ofWhat) +intIndex = + prism + (fromIntegral . coerce @_ @Word32) + (\i -> maybe (Left i) (Right . Index) . toIntegralSized $ i) + +-- | Helper for the first index. +-- +-- @since 1.0.0 +ix0 :: forall (ofWhat :: Symbol). Index ofWhat +ix0 = Index 0 + +-- | Helper for the second index. +-- +-- @since 1.0.0 +ix1 :: forall (ofWhat :: Symbol). Index ofWhat +ix1 = Index 1 + +-- | Helper for the third index. +-- +-- @since 1.0.0 +ix2 :: forall (ofWhat :: Symbol). Index ofWhat +ix2 = Index 2 + +-- | Helper for the fourth index. +-- +-- @since 1.0.0 +ix3 :: forall (ofWhat :: Symbol). Index ofWhat +ix3 = Index 3 + +-- | An indicator of the cardinality of something. Meant to be paired with +-- 'Index' to specify which unique something you mean. +-- +-- @since 1.0.0 +newtype Count (ofWhat :: Symbol) = Count Word32 + deriving + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord + ) + via Word32 + deriving stock + ( -- | @since 1.0.0 + Show + ) + +type role Count nominal + +-- | Helper to construct, and convert, 'Count's and 'Int's. This is needed +-- because unfortunately, sizes of things are usually 'Int's in Haskell. +-- +-- To use this, do one of the following: +-- +-- * Construct with @'preview'@: for example, @'preview' intCount 1@. +-- * Destruct with @'review'@. +-- +-- @since 1.0.0 +intCount :: forall (ofWhat :: Symbol). Prism' Int (Count ofWhat) +intCount = + prism + (fromIntegral . coerce @_ @Word32) + (\i -> maybe (Left i) (Right . Count) . toIntegralSized $ i) + +-- | Helper for a count of zero items. +-- +-- @since 1.0.0 +count0 :: forall (ofWhat :: Symbol). Count ofWhat +count0 = Count 0 + +-- | Helper for a count of one item. +-- +-- @since 1.0.0 +count1 :: forall (ofWhat :: Symbol). Count ofWhat +count1 = Count 1 + +-- | Helper for a count of two items. +-- +-- @since 1.0.0 +count2 :: forall (ofWhat :: Symbol). Count ofWhat +count2 = Count 2 + +-- | Helper for a count of three items. +-- +-- @since 1.0.0 +count3 :: forall (ofWhat :: Symbol). Count ofWhat +count3 = Count 3 diff --git a/src/Covenant/Internal/Rename.hs b/src/Covenant/Internal/Rename.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/Rename.hs @@ -0,0 +1,277 @@ +module Covenant.Internal.Rename + ( RenameM, + RenameError (..), + runRenameM, + renameValT, + renameCompT, + undoRename, + ) +where + +import Control.Monad (unless) +import Control.Monad.Except + ( ExceptT, + runExceptT, + throwError, + ) +import Control.Monad.Reader + ( Reader, + asks, + local, + runReader, + ) +import Control.Monad.State.Strict + ( State, + evalState, + gets, + modify, + ) +import Covenant.DeBruijn (DeBruijn (S, Z), asInt) +import Covenant.Index (Count, Index, intCount, intIndex) +import Covenant.Internal.Type + ( AbstractTy (BoundAt), + CompT (CompT), + CompTBody (CompTBody), + Renamed (Rigid, Unifiable, Wildcard), + ValT (Abstraction, BuiltinFlat, ThunkT), + ) +import Data.Coerce (coerce) +import Data.Kind (Type) +import Data.Tuple.Optics (_1) +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Data.Vector.NonEmpty qualified as NonEmpty +import Data.Word (Word64) +import Optics.Core + ( A_Lens, + LabelOptic (labelOptic), + ix, + lens, + over, + review, + set, + to, + view, + (%), + ) + +-- Used during renaming. Contains a source of fresh indices for wildcards, as +-- well as tracking: +-- +-- 1. How many variables are bound by each scope; +-- 2. Which of these variables have been noted as used; and +-- 3. A unique identifier for each scope (for wildcards). +data RenameState = RenameState Word64 (Vector (Vector Bool, Word64)) + deriving stock (Eq, Show) + +-- Note (Koz, 11/04/2025): We need this field as a source of unique identifiers +-- when renaming wildcards. Wildcards are special in that they can unify with +-- anything (possibly _several_ anythings) except different wildcards in the +-- same scope as each other. For example, consider the computation type below: +-- +-- (forall a b . a -> b -> !Int) -> (forall c . c -> !Int) -> String -> !Int +-- +-- In particular, `a` and `c` would be defined the same way: `BoundAt Z ix0`. +-- However, while `c` and `b` could unify just fine, `a` and `b` could not. +-- Furthermore, they are identically scoped (in the sense that they're both +-- enclosed the same way), which means that, unlike rigid variables, we cannot +-- uniquely identify them just by their scoping. +-- +-- Thus, we have to have to have a way to uniquely label any wildcard in such a +-- way that wildcards in the same scope, at the same level, are tagged +-- separately from wildcards in a _different_ scope at the same level. See the +-- functions `stepUpScope` and `dropDownScope` to see how we achieve this. +instance + (k ~ A_Lens, a ~ Word64, b ~ Word64) => + LabelOptic "idSource" k RenameState RenameState a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(RenameState x _) -> x) + (\(RenameState _ y) x' -> RenameState x' y) + +-- The 'outer' vector represents a stack of scopes. Each entry is a combination +-- of a vector of used variables (length is equal to the number of variables +-- bound by that scope), together with a unique identifier not only for that +-- scope, but also the `step` into that scope, as required by wildcard renaming. +instance + (k ~ A_Lens, a ~ Vector (Vector Bool, Word64), b ~ Vector (Vector Bool, Word64)) => + LabelOptic "tracker" k RenameState RenameState a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(RenameState _ y) -> y) + (\(RenameState x _) y' -> RenameState x y') + +-- | Ways in which the renamer can fail. +-- +-- @since 1.0.0 +data RenameError + = -- | An attempt to reference an abstraction in a scope where this + -- abstraction doesn't exist. First field is the true level, second is + -- the index that was requested. + -- + -- @since 1.0.0 + InvalidAbstractionReference Int (Index "tyvar") + | -- | A value type specifies an abstraction that never gets used + -- anywhere. For example, the type @forall a b . [a]@ has @b@ + -- irrelevant. + -- + -- @since 1.0.0 + IrrelevantAbstraction + | -- | A computation type specifies an abstraction which is not used + -- by any argument. For example, the type @forall a b . a -> !(b -> !a)@ + -- has @b@ undetermined. + -- + -- @since 1.0.0 + UndeterminedAbstraction + deriving stock (Eq, Show) + +-- | A \'renaming monad\' which allows us to convert type representations from +-- ones that use /relative/ abstraction labelling to /absolute/ abstraction +-- labelling. +-- +-- = Why this is necessary +-- +-- Consider the following 'AbstractTy': @'BoundAtScope' 1 0@. The meaning of +-- this is relative to where in a type it is positioned: it could be bound by a +-- scope higher than our own, or something we can unify with. Because its +-- meaning (namely, what it refers to) is situational, type checking becomes +-- more difficult, although it has other advantages. +-- +-- This monad allows us to convert this relative form into an absolute one. More +-- specifically, the renamer does two things: +-- +-- * Ensures that any given abstraction refers to one, and /only/ one, thing; +-- and +-- * Indicates which abstractions are unifiable, and which are (effectively) +-- constant or fixed. +-- +-- @since 1.0.0 +newtype RenameM (a :: Type) + = RenameM (ExceptT RenameError (State RenameState) a) + deriving + ( -- | @since 1.0.0 + Functor, + -- | @since 1.0.0 + Applicative, + -- | @since 1.0.0 + Monad + ) + via (ExceptT RenameError (State RenameState)) + +-- | Execute a renaming computation. +-- +-- @since 1.0.0 +runRenameM :: + forall (a :: Type). + RenameM a -> + Either RenameError a +runRenameM (RenameM comp) = evalState (runExceptT comp) . RenameState 0 $ Vector.empty + +-- | Rename a computation type. +-- +-- @since 1.0.0 +renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed) +renameCompT (CompT abses (CompTBody xs)) = RenameM $ do + -- Step up a scope + modify (stepUpScope abses) + -- Rename, but only the arguments + renamedArgs <- + Vector.generateM + (NonEmpty.length xs - 1) + (\i -> coerce . renameValT $ xs NonEmpty.! i) + -- Check that we don't overdetermine anything + ourAbstractions <- gets (view (#tracker % to Vector.head % _1)) + unless (Vector.and ourAbstractions) (throwError UndeterminedAbstraction) + -- Check result type + renamedResult <- coerce . renameValT . NonEmpty.last $ xs + -- Roll back state + modify dropDownScope + -- Rebuild and return + pure . CompT abses . CompTBody . NonEmpty.snocV renamedArgs $ renamedResult + +-- | Rename a value type. +-- +-- @since 1.0.0 +renameValT :: ValT AbstractTy -> RenameM (ValT Renamed) +renameValT = \case + Abstraction t -> Abstraction <$> renameAbstraction t + ThunkT t -> ThunkT <$> renameCompT t + BuiltinFlat t -> pure . BuiltinFlat $ t + +-- A way of 'undoing' the renaming process. This is meant to be used only after +-- applications, and assumes that what is being un-renamed is the result of a +-- computation. +undoRename :: ValT Renamed -> ValT AbstractTy +undoRename t = runReader (go t) 1 + where + go :: ValT Renamed -> Reader Int (ValT AbstractTy) + go = \case + Abstraction t' -> + Abstraction <$> case t' of + Unifiable index -> BoundAt <$> trueLevelToDB 1 <*> pure index + Rigid trueLevel index -> BoundAt <$> trueLevelToDB trueLevel <*> pure index + Wildcard _ trueLevel index -> BoundAt <$> trueLevelToDB trueLevel <*> pure index + ThunkT (CompT abses (CompTBody xs)) -> + ThunkT . CompT abses . CompTBody <$> local (+ 1) (traverse go xs) + BuiltinFlat t' -> pure . BuiltinFlat $ t' + +-- Helpers + +trueLevelToDB :: Int -> Reader Int DeBruijn +trueLevelToDB trueLevel = asks (go . subtract trueLevel) + where + go :: Int -> DeBruijn + go = \case + 0 -> Z + n -> S . go $ n - 1 + +renameAbstraction :: AbstractTy -> RenameM Renamed +renameAbstraction (BoundAt scope index) = RenameM $ do + trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - asInt scope) + scopeInfo <- gets (\x -> view #tracker x Vector.!? asInt scope) + let asIntIx = review intIndex index + case scopeInfo of + -- This variable is bound in a scope that encloses the renaming scope. Thus, + -- the variable is rigid. + Nothing -> pure . Rigid trueLevel $ index + Just (occursTracker, uniqueScopeId) -> case occursTracker Vector.!? asIntIx of + Nothing -> throwError . InvalidAbstractionReference trueLevel $ index + Just beenUsed -> do + -- Note that this variable has occurred + unless beenUsed (modify (noteUsed scope index)) + pure $ + if trueLevel == 1 + -- This is a unifiable variable + then Unifiable index + -- This is a wildcard variable + else Wildcard uniqueScopeId trueLevel index + +-- Given a number of abstractions bound by a scope, modify the state to track +-- that scope. +stepUpScope :: Count "tyvar" -> RenameState -> RenameState +stepUpScope abses x = + let fresh = view #idSource x + absesI = review intCount abses + -- Label (speculatively) the current scope 'step' with a unique value. + entry = (Vector.replicate absesI False, fresh) + in -- Ensure that our source of fresh identifiers is incremented + over #tracker (Vector.cons entry) . set #idSource (fresh + 1) $ x + +-- Stop tracking the last scope we added. +-- +-- Note that, while we 'throw away' the information about (used) variables in +-- the scope, we do _not_ roll back the `idSource`. This is in fact why we have +-- to be in `State` rather than `Reader`: that change has to be persistent to +-- achieve our goal of renaming wildcards. +dropDownScope :: RenameState -> RenameState +dropDownScope = over #tracker Vector.tail + +-- Given a pair of DeBruijn index and positional index for a variable, note that +-- we've seen this variable. +noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState +noteUsed scope index = + set (#tracker % ix (asInt scope) % _1 % ix (review intIndex index)) True diff --git a/src/Covenant/Internal/Term.hs b/src/Covenant/Internal/Term.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/Term.hs @@ -0,0 +1,291 @@ +module Covenant.Internal.Term + ( CovenantTypeError (..), + Id (..), + typeId, + Arg (..), + typeArg, + Ref (..), + typeRef, + CompNodeInfo (..), + ValNodeInfo (..), + ASGNode (..), + typeASGNode, + ASGNodeType (..), + ) +where + +import Control.Monad.Except (MonadError (throwError)) +import Control.Monad.HashCons (MonadHashCons (lookupRef)) +import Covenant.Constant (AConstant) +import Covenant.DeBruijn (DeBruijn) +import Covenant.Index (Index) +import Covenant.Internal.Rename (RenameError) +import Covenant.Internal.Type (AbstractTy, CompT, ValT) +import Covenant.Internal.Unification (TypeAppError) +import Covenant.Prim (OneArgFunc, ThreeArgFunc, TwoArgFunc) +import Data.Kind (Type) +import Data.Vector (Vector) +import Data.Word (Word64) + +-- | An error that can arise during the construction of an ASG by programmatic +-- means. +-- +-- @since 1.0.0 +data CovenantTypeError + = -- | An 'Id' has no corresponding node. This error should not arise under + -- normal circumstances: the most likely explanation is that you're using an + -- 'Id' that was made by a different ASG builder computation. + -- + -- @since 1.0.0 + BrokenIdReference Id + | -- | Computation-typed nodes can't be forced, but we tried anyway. + -- + -- @since 1.0.0 + ForceCompType (CompT AbstractTy) + | -- | Value-typed nodes that aren't thunks can't be forced, but we tried anyway. + -- + -- @since 1.0.0 + ForceNonThunk (ValT AbstractTy) + | -- | Error nodes can't be forced, but we tried anyway. + -- + -- @since 1.0.0 + ForceError + | -- | Value-typed nodes can't be thunked, but we tried anyway. + -- + -- @since 1.0.0 + ThunkValType (ValT AbstractTy) + | -- | Error nodes can't be thunked, but we tried anyway. + -- + -- @since 1.0.0 + ThunkError + | -- | Arguments can't be applied to a value-typed node, but we tried anyway. + -- + -- @since 1.0.0 + ApplyToValType (ValT AbstractTy) + | -- | Arguments can't be applied to error nodes, but we tried anyway. + -- + -- @since 1.0.0 + ApplyToError + | -- | Computation-typed nodes can't be applied as arguments, but we tried anyway. + -- + -- @since 1.0.0 + ApplyCompType (CompT AbstractTy) + | -- | Renaming the function in an application failed. + -- + -- @since 1.0.0 + RenameFunctionFailed (CompT AbstractTy) RenameError + | -- | Renaming an argument in an application failed. + -- + -- @since 1.0.0 + RenameArgumentFailed (ValT AbstractTy) RenameError + | -- | We failed to unify an expected argument type with the type of the + -- argument we were actually given. + -- + -- @since 1.0.0 + UnificationError TypeAppError + | -- | An argument was requested that doesn't exist. + -- + -- @since 1.0.0 + NoSuchArgument DeBruijn (Index "arg") + | -- | Can't return a computation-typed node, but we tried anyway. + -- + -- @since 1.0.0 + ReturnCompType (CompT AbstractTy) + | -- | The body of a lambda results in a value-typed node, which isn't allowed. + -- + -- @since 1.0.0 + LambdaResultsInValType (ValT AbstractTy) + | -- | The body of a lambda results in a computation-typed node which isn't + -- a return, which isn't allowed. + -- + -- @since 1.0.0 + LambdaResultsInNonReturn (CompT AbstractTy) + | -- | A lambda body's return is wrapping an error, instead of being directly + -- an error. This should not happen under normal circumstances and is most + -- certainly a bug. + -- + -- @since 1.0.0 + ReturnWrapsError + | -- | We tried to return a computation-typed node, but this isn't allowed. + -- + -- @since 1.0.0 + ReturnWrapsCompType (CompT AbstractTy) + | -- | The result of an application is not what the computation being + -- applied expected. + -- + -- First field is the expected type, the second is what we actually got. + -- + -- @since 1.0.0 + WrongReturnType (ValT AbstractTy) (ValT AbstractTy) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Show + ) + +-- | A unique identifier for a node in a Covenant program. +-- +-- @since 1.0.0 +newtype Id = Id Word64 + deriving + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Bounded, + -- | Needed for internal reasons, even though this type class is terrible. + -- + -- @since 1.0.0 + Enum + ) + via Word64 + deriving stock + ( -- | @since 1.0.0 + Show + ) + +-- Get the type of an `Id`, or fail. +typeId :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Id -> m ASGNodeType +typeId i = do + lookedUp <- lookupRef i + case lookedUp of + Nothing -> throwError . BrokenIdReference $ i + Just node -> pure . typeASGNode $ node + +-- | An argument passed to a function in a Covenant program. +-- +-- @since 1.0.0 +data Arg = Arg DeBruijn (Index "arg") (ValT AbstractTy) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- Helper to get the type of an argument. +typeArg :: Arg -> ValT AbstractTy +typeArg (Arg _ _ t) = t + +-- | A general reference in a Covenant program. +-- +-- @since 1.0.0 +data Ref + = -- | A function argument. + -- + -- @since 1.0.0 + AnArg Arg + | -- | A link to an ASG node. + -- + -- @since 1.0.0 + AnId Id + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- Helper for getting a type for any reference. +typeRef :: + forall (m :: Type -> Type). + (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) => + Ref -> m ASGNodeType +typeRef = \case + AnArg arg -> pure . ValNodeType . typeArg $ arg + AnId i -> typeId i + +-- | Computation-term-specific node information. +-- +-- @since 1.0.0 +data CompNodeInfo + = Builtin1Internal OneArgFunc + | Builtin2Internal TwoArgFunc + | Builtin3Internal ThreeArgFunc + | LamInternal Id + | ForceInternal Ref + | ReturnInternal Ref + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | Value-term-specific node information. +-- +-- @since 1.0.0 +data ValNodeInfo + = LitInternal AConstant + | AppInternal Id (Vector Ref) + | ThunkInternal Id + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | A single node in a Covenant ASG. Where appropriate, these carry their +-- types. +-- +-- @since 1.0.0 +data ASGNode + = -- | A computation-typed node. + -- + -- @since 1.0.0 + ACompNode (CompT AbstractTy) CompNodeInfo + | -- | A value-typed node + -- + -- @since 1.0.0 + AValNode (ValT AbstractTy) ValNodeInfo + | -- | An error node. + -- + -- @since 1.0.0 + AnError + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | Produces the type of any ASG node. +-- +-- @since 1.0.0 +typeASGNode :: ASGNode -> ASGNodeType +typeASGNode = \case + ACompNode t _ -> CompNodeType t + AValNode t _ -> ValNodeType t + AnError -> ErrorNodeType + +-- | Helper data type representing the type of any ASG node whatsoever. +-- +-- @since 1.0.0 +data ASGNodeType + = CompNodeType (CompT AbstractTy) + | ValNodeType (ValT AbstractTy) + | ErrorNodeType + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) diff --git a/src/Covenant/Internal/Type.hs b/src/Covenant/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/Type.hs @@ -0,0 +1,375 @@ +module Covenant.Internal.Type + ( AbstractTy (..), + Renamed (..), + CompT (..), + CompTBody (..), + ValT (..), + BuiltinFlatT (..), + ) +where + +import Control.Monad.Reader + ( MonadReader (local), + Reader, + asks, + runReader, + ) +import Covenant.DeBruijn (DeBruijn) +import Covenant.Index + ( Count, + Index, + intCount, + intIndex, + ) +import Data.Functor.Classes (Eq1 (liftEq)) +import Data.Kind (Type) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Data.Vector.NonEmpty (NonEmptyVector) +import Data.Vector.NonEmpty qualified as NonEmpty +import Data.Word (Word64) +import GHC.Exts (fromListN) +import Optics.At () +import Optics.Core + ( A_Lens, + LabelOptic (labelOptic), + ix, + lens, + over, + preview, + review, + set, + view, + (%), + ) +import Prettyprinter + ( Doc, + Pretty (pretty), + hsep, + parens, + viaShow, + (<+>), + ) + +-- | A type abstraction, using a combination of a DeBruijn index (to indicate +-- which scope it refers to) and a positional index (to indicate which bound +-- variable in that scope it refers to). +-- +-- = Important note +-- +-- This is a /relative/ representation: any given 'AbstractTy' could refer to +-- different things when placed in different positions in the ASG. This stems +-- from how DeBruijn indices behave: 'Z' refers to \'our immediate enclosing +-- scope\', @'S' 'Z'@ to \'one scope outside our immediate enclosing scope\', +-- etc. This can mean different things depending on what these scope(s) are. +-- +-- @since 1.0.0 +data AbstractTy = BoundAt DeBruijn (Index "tyvar") + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | A type abstraction that has undergone renaming from a specific context. +-- +-- @since 1.0.0 +data Renamed + = -- | Set by an enclosing scope, and thus is essentially a + -- concrete type, we just don't know which. First field is its \'true + -- level\', second field is the positional index in that scope. + Rigid Int (Index "tyvar") + | -- | Can be unified with something, but must be consistent: that is, only one + -- unification for every instance. Field is this variable's positional index; + -- we don't need to track the scope, as only one scope contains unifiable + -- bindings. + Unifiable (Index "tyvar") + | -- | /Must/ unify with everything, except with other distinct wildcards in the + -- same scope. First field is a unique /scope/ identifier; second is its + -- \'true level\' simialr to @'Rigid'@; third is the positional index within + -- its scope. We must have unique identifiers for wildcard scopes, as + -- wildcards unify with everything /except/ other wildcards in the /same/ + -- scope, and child scopes aren't unique. + Wildcard Word64 Int (Index "tyvar") + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | The \'body\' of a computation type, consisting of the types of its +-- arguments and the type of its result. +-- +-- @since 1.0.0 +newtype CompTBody (a :: Type) = CompTBody (NonEmptyVector (ValT a)) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | @since 1.0.0 +instance Eq1 CompTBody where + {-# INLINEABLE liftEq #-} + liftEq f (CompTBody xs) (CompTBody ys) = + liftEq (liftEq f) xs ys + +-- | A computation type, with abstractions indicated by the type argument. In +-- pretty much any case imaginable, this would be either 'AbstractTy' (in the +-- ASG), or 'Renamed' (after renaming). +-- +-- @since 1.0.0 +data CompT (a :: Type) = CompT (Count "tyvar") (CompTBody a) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | @since 1.0.0 +instance Eq1 CompT where + {-# INLINEABLE liftEq #-} + liftEq f (CompT abses1 xs) (CompT abses2 ys) = + abses1 == abses2 && liftEq f xs ys + +-- | @since 1.0.0 +instance Pretty (CompT Renamed) where + pretty = runPrettyM . prettyCompTWithContext + +-- | A value type, with abstractions indicated by the type argument. In pretty +-- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or +-- 'Renamed' (after renaming). +-- +-- @since 1.0.0 +data ValT (a :: Type) + = -- | An abstract type. + Abstraction a + | -- | A suspended computation. + ThunkT (CompT a) + | -- | A builtin type without any nesting. + BuiltinFlat BuiltinFlatT + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | @since 1.0.0 +instance Eq1 ValT where + {-# INLINEABLE liftEq #-} + liftEq f = \case + Abstraction abs1 -> \case + Abstraction abs2 -> f abs1 abs2 + _ -> False + ThunkT t1 -> \case + ThunkT t2 -> liftEq f t1 t2 + _ -> False + BuiltinFlat t1 -> \case + BuiltinFlat t2 -> t1 == t2 + _ -> False + +-- | All builtin types that are \'flat\': that is, do not have other types +-- \'nested inside them\'. +data BuiltinFlatT + = UnitT + | BoolT + | IntegerT + | StringT + | ByteStringT + | BLS12_381_G1_ElementT + | BLS12_381_G2_ElementT + | BLS12_381_MlResultT + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- Helpers + +newtype ScopeBoundary = ScopeBoundary Int + deriving (Show, Eq, Ord, Num) via Int + +-- Keeping the field names for clarity even if we don't use them +data PrettyContext (ann :: Type) + = PrettyContext + { _boundIdents :: Map ScopeBoundary (Vector (Doc ann)), + _currentScope :: ScopeBoundary, + _varStream :: [Doc ann] + } + +instance + (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) => + LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(PrettyContext x _ _) -> x) + (\(PrettyContext _ y z) x -> PrettyContext x y z) + +instance + (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) => + LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(PrettyContext _ x _) -> x) + (\(PrettyContext x _ z) y -> PrettyContext x y z) + +instance + (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) => + LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b + where + {-# INLINEABLE labelOptic #-} + labelOptic = + lens + (\(PrettyContext _ _ x) -> x) + (\(PrettyContext x y _) z -> PrettyContext x y z) + +-- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail +newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a) + deriving + ( Functor, + Applicative, + Monad, + MonadReader (PrettyContext ann) + ) + via (Reader (PrettyContext ann)) + +runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a +runPrettyM (PrettyM ma) = runReader ma (PrettyContext mempty 0 infiniteVars) + where + -- Lazily generated infinite list of variables. Will start with a, b, c... + -- and cycle around to a1, b2, c3 etc. + -- We could do something more sophisticated but this should work. + infiniteVars :: [Doc ann] + infiniteVars = + let aToZ = ['a' .. 'z'] + intStrings = ("" <$ aToZ) <> map (show @Integer) [0 ..] + in zipWith (\x xs -> pretty (x : xs)) aToZ intStrings + +prettyCompTWithContext :: forall (ann :: Type). CompT Renamed -> PrettyM ann (Doc ann) +prettyCompTWithContext (CompT count (CompTBody funArgs)) + | review intCount count == 0 = prettyFunTy funArgs + | otherwise = bindVars count $ \newVars -> do + funTy <- prettyFunTy funArgs + pure $ mkForall newVars funTy + +prettyFunTy :: + forall (ann :: Type). + NonEmptyVector (ValT Renamed) -> + PrettyM ann (Doc ann) +prettyFunTy args = case NonEmpty.uncons args of + (arg, rest) -> Vector.foldl' go (("!" <>) <$> prettyArg arg) rest + where + go :: + PrettyM ann (Doc ann) -> + ValT Renamed -> + PrettyM ann (Doc ann) + go acc t = (\x y -> x <+> "->" <+> y) <$> prettyArg t <*> acc + prettyArg :: ValT Renamed -> PrettyM ann (Doc ann) + prettyArg vt = + let prettyVT = prettyValTWithContext vt + in if isSimpleValT vt + then prettyVT + else parens <$> prettyVT + +bindVars :: + forall (ann :: Type) (a :: Type). + Count "tyvar" -> + (Vector (Doc ann) -> PrettyM ann a) -> + PrettyM ann a +bindVars count' act + | count == 0 = crossBoundary (act Vector.empty) + | otherwise = crossBoundary $ do + here <- asks (view #currentScope) + withFreshVarNames count $ \newBoundVars -> + local (over #boundIdents (Map.insert here newBoundVars)) (act newBoundVars) + where + -- Increment the current scope + crossBoundary :: PrettyM ann a -> PrettyM ann a + crossBoundary = local (over #currentScope (+ 1)) + count :: Int + count = review intCount count' + +mkForall :: + forall (ann :: Type). + Vector (Doc ann) -> + Doc ann -> + Doc ann +mkForall tvars funTyBody = + if Vector.null tvars + then funTyBody + else "forall" <+> hsep (Vector.toList tvars) <> "." <+> funTyBody + +-- I.e. can we omit parens and get something unambiguous? This might be overly aggressive w/ parens but that's OK +isSimpleValT :: forall (a :: Type). ValT a -> Bool +isSimpleValT = \case + ThunkT thunk -> isSimpleCompT thunk + _ -> True + where + isSimpleCompT :: CompT a -> Bool + isSimpleCompT (CompT count (CompTBody args)) = + review intCount count == 0 && NonEmpty.length args == 1 + +prettyValTWithContext :: forall (ann :: Type). ValT Renamed -> PrettyM ann (Doc ann) +prettyValTWithContext = \case + Abstraction abstr -> prettyRenamedWithContext abstr + ThunkT compT -> prettyCompTWithContext compT + BuiltinFlat biFlat -> pure $ viaShow biFlat + +-- Generate N fresh var names and use the supplied monadic function to do something with them. +withFreshVarNames :: + forall (ann :: Type) (a :: Type). + Int -> + (Vector (Doc ann) -> PrettyM ann a) -> + PrettyM ann a +withFreshVarNames n act = do + stream <- asks (view #varStream) + let (used, rest) = splitAt n stream + local (set #varStream rest) . act . fromListN n $ used + +prettyRenamedWithContext :: forall (ann :: Type). Renamed -> PrettyM ann (Doc ann) +prettyRenamedWithContext = \case + Rigid offset index -> lookupAbstraction offset index + Unifiable i -> lookupAbstraction 0 i + Wildcard w64 offset i -> pure $ pretty offset <> "_" <> viaShow w64 <> "#" <> pretty (review intIndex i) + +lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann) +lookupAbstraction offset argIndex = do + let scopeOffset = ScopeBoundary offset + let argIndex' = review intIndex argIndex + here <- asks (view #currentScope) + asks (preview (#boundIdents % ix (here + scopeOffset) % ix argIndex')) >>= \case + Nothing -> + -- TODO: actual error reporting + error $ + "Internal error: The encountered a variable at arg index " + <> show argIndex' + <> " with true level " + <> show scopeOffset + <> " but could not locate the corresponding pretty form at scope level " + <> show here + Just res' -> pure res' diff --git a/src/Covenant/Internal/Unification.hs b/src/Covenant/Internal/Unification.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Internal/Unification.hs @@ -0,0 +1,251 @@ +{-# LANGUAGE CPP #-} + +module Covenant.Internal.Unification + ( TypeAppError (..), + checkApp, + ) +where + +import Control.Monad (foldM, unless) +import Data.Ord (comparing) +#if __GLASGOW_HASKELL__==908 +import Data.Foldable (foldl') +#endif +import Control.Monad.Except (catchError, throwError) +import Covenant.Index (Index, intCount, intIndex) +import Covenant.Internal.Type + ( BuiltinFlatT, + CompT (CompT), + CompTBody (CompTBody), + Renamed (Rigid, Unifiable, Wildcard), + ValT (Abstraction, BuiltinFlat, ThunkT), + ) +import Data.Kind (Type) +import Data.Map (Map) +import Data.Map.Merge.Strict qualified as Merge +import Data.Map.Strict qualified as Map +import Data.Maybe (fromJust, mapMaybe) +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Data.Vector.NonEmpty qualified as NonEmpty +import Data.Word (Word64) +import Optics.Core (preview) + +-- | @since 1.0.0 +data TypeAppError + = -- | The final type after all arguments are applied is @forall a . a@. + LeakingUnifiable (Index "tyvar") + | -- | A wildcard (thus, a skolem) escaped its scope. + LeakingWildcard Word64 Int (Index "tyvar") + | -- | We were given too many arguments. + ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed))) + | -- | We weren't given enough arguments. + InsufficientArgs (CompT Renamed) + | -- | The expected type (first field) and actual type (second field) do not + -- unify. + DoesNotUnify (ValT Renamed) (ValT Renamed) + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Show + ) + +-- | @since 1.0.0 +checkApp :: CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed) +checkApp f@(CompT _ (CompTBody xs)) = + let (curr, rest) = NonEmpty.uncons xs + in go curr (Vector.toList rest) + where + go :: + ValT Renamed -> + [ValT Renamed] -> + [Maybe (ValT Renamed)] -> + Either TypeAppError (ValT Renamed) + go currParam restParams args = case restParams of + [] -> case args of + -- If we got here, currParam is the resulting type after all + -- substitutions have been applied. + [] -> fixUp currParam + _ -> throwError . ExcessArgs f . Vector.fromList $ args + _ -> case args of + [] -> throwError . InsufficientArgs $ f + (currArg : restArgs) -> do + newRestParams <- case currArg of + -- An error argument unifies with anything, as it's effectively + -- `forall a . a`. Furthermore, it requires no substitutional + -- changes. Thus, we can just skip it. + Nothing -> pure restParams + Just currArg' -> do + subs <- catchError (unify currParam currArg') (promoteUnificationError currParam currArg') + pure . Map.foldlWithKey' applySub restParams $ subs + case newRestParams of + [] -> throwError . InsufficientArgs $ f + (currParam' : restParams') -> go currParam' restParams' restArgs + +-- Helpers + +applySub :: + [ValT Renamed] -> + Index "tyvar" -> + ValT Renamed -> + [ValT Renamed] +applySub acc index sub = fmap (substitute index sub) acc + +substitute :: + Index "tyvar" -> + ValT Renamed -> + ValT Renamed -> + ValT Renamed +substitute index toSub = \case + Abstraction t -> case t of + Unifiable ourIndex -> + if ourIndex == index + then toSub + else Abstraction t + _ -> Abstraction t + ThunkT (CompT abstractions (CompTBody xs)) -> + ThunkT . CompT abstractions . CompTBody . fmap (substitute index toSub) $ xs + BuiltinFlat t -> BuiltinFlat t + +-- Because unification is inherently recursive, if we find an error deep within +-- a type, the message will signify only the _part_ that fails to unify, not the +-- entire type. While potentially useful, this can be quite confusing, +-- especially with generated types. Thus, we use `catchError` with this +-- function, which effectively allows us to rename the types reported in +-- unification errors to whatever types 'wrap' them. +promoteUnificationError :: + forall (a :: Type). + ValT Renamed -> + ValT Renamed -> + TypeAppError -> + Either TypeAppError a +promoteUnificationError topLevelExpected topLevelActual = + Left . \case + DoesNotUnify _ _ -> DoesNotUnify topLevelExpected topLevelActual + err -> err + +fixUp :: ValT Renamed -> Either TypeAppError (ValT Renamed) +fixUp = \case + -- We have a result that's effectively `forall a . a` but not an error + Abstraction (Unifiable index) -> throwError . LeakingUnifiable $ index + -- We're doing the equivalent of failing the `ST` trick + Abstraction (Wildcard scopeId trueLevel index) -> throwError . LeakingWildcard scopeId trueLevel $ index + -- We may have a result with fewer unifiables than we started with + -- This can be a problem, as we might be referring to unifiables that don't + -- exist anymore + ThunkT (CompT _ (CompTBody xs)) -> do + -- Figure out how many variables the thunk has to introduce now + let remainingUnifiables = NonEmpty.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty xs + let requiredIntroductions = Set.size remainingUnifiables + -- We know that the size of a set can't be negative, but GHC doesn't. + let asCount = fromJust . preview intCount $ requiredIntroductions + -- Make enough indexes for us to use in one go + let indexesToUse = mapMaybe (preview intIndex) [0, 1 .. requiredIntroductions - 1] + -- Construct a mapping between old, possibly non-contiguous, unifiables and + -- our new ones + let renames = + zipWith + (\i replacement -> (i, Abstraction . Unifiable $ replacement)) + (Set.toList remainingUnifiables) + indexesToUse + let fixed = fmap (\t -> foldl' (\acc (i, r) -> substitute i r acc) t renames) xs + pure . ThunkT . CompT asCount . CompTBody $ fixed + t -> pure t + +collectUnifiables :: ValT Renamed -> Set (Index "tyvar") +collectUnifiables = \case + Abstraction t -> case t of + Unifiable index -> Set.singleton index + _ -> Set.empty + BuiltinFlat _ -> Set.empty + ThunkT (CompT _ (CompTBody xs)) -> NonEmpty.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty xs + +unify :: + ValT Renamed -> + ValT Renamed -> + Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) +unify expected actual = + catchError + ( case expected of + Abstraction t1 -> case t1 of + -- Unifiables unify with everything, and require a substitutional rewrite. + Unifiable index1 -> pure . Map.singleton index1 $ actual + Rigid level1 index1 -> expectRigid level1 index1 + Wildcard scopeId1 _ index1 -> expectWildcard scopeId1 index1 + ThunkT t1 -> expectThunk t1 + BuiltinFlat t1 -> expectFlatBuiltin t1 + ) + (promoteUnificationError expected actual) + where + unificationError :: forall (a :: Type). Either TypeAppError a + unificationError = Left . DoesNotUnify expected $ actual + noSubUnify :: forall (k :: Type) (a :: Type). Either TypeAppError (Map k a) + noSubUnify = pure Map.empty + expectRigid :: + Int -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + -- Rigids behave identically to concrete types: they can unify with + -- themselves, or any other abstraction, but nothing else. No substitutional + -- rewrites are needed. + expectRigid level1 index1 = case actual of + Abstraction (Rigid level2 index2) -> + if level1 == level2 && index1 == index2 + then noSubUnify + else unificationError + Abstraction _ -> noSubUnify + _ -> unificationError + expectWildcard :: + Word64 -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + -- Wildcards can unify with unifiables, as well as themselves, but nothing + -- else. No substitutional rewrites are needed. + expectWildcard scopeId1 index1 = case actual of + Abstraction (Unifiable _) -> noSubUnify + Abstraction (Wildcard scopeId2 _ index2) -> + if scopeId1 /= scopeId2 || index1 == index2 + then noSubUnify + else unificationError + _ -> unificationError + expectThunk :: CompT Renamed -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + -- Thunks unify unconditionally with wildcards or unifiables. They unify + -- conditionally with other thunks, provided that we can unify each argument + -- with its counterpart in the same position, as well as their result types, + -- without conflicts. + expectThunk (CompT _ (CompTBody t1)) = case actual of + Abstraction (Rigid _ _) -> unificationError + Abstraction _ -> noSubUnify + ThunkT (CompT _ (CompTBody t2)) -> do + unless (comparing NonEmpty.length t1 t2 == EQ) unificationError + catchError + (foldM (\acc (l, r) -> unify l r >>= reconcile acc) Map.empty . NonEmpty.zip t1 $ t2) + (promoteUnificationError expected actual) + _ -> unificationError + expectFlatBuiltin :: BuiltinFlatT -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + -- 'Flat' builtins are always concrete. They can unify with themselves, + -- unifiables or wildcards, but nothing else. No substitutional rewrites are + -- needed. + expectFlatBuiltin t1 = case actual of + Abstraction (Rigid _ _) -> unificationError + Abstraction _ -> noSubUnify + BuiltinFlat t2 -> + if t1 == t2 + then noSubUnify + else unificationError + _ -> unificationError + reconcile :: + Map (Index "tyvar") (ValT Renamed) -> + Map (Index "tyvar") (ValT Renamed) -> + Either TypeAppError (Map (Index "tyvar") (ValT Renamed)) + -- Note (Koz, 14/04/2025): This utter soup means the following: + -- + -- - If the old map and the new map don't have any overlapping assignments, + -- just union them. + -- - Otherwise, for any assignment to a unifiable that is present in both + -- maps, ensure they assign to the same thing; if they do, it's fine, + -- otherwise we have a problem. + reconcile = + Merge.mergeA + Merge.preserveMissing + Merge.preserveMissing + (Merge.zipWithAMatched $ \_ l r -> l <$ unless (l == r) unificationError) diff --git a/src/Covenant/Prim.hs b/src/Covenant/Prim.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Prim.hs @@ -0,0 +1,437 @@ +-- | +-- Module: Covenant.Prim +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- Contains definitions relating to Plutus primitive functions in Covenant +-- programs. +-- +-- = Note +-- +-- In the 1.0.0 release, we didn't include non-flat builtin types, specifically +-- pairs, lists and @Data@. Thus, the primops that operate on, or produce, these +-- are not currently included. +-- +-- @since 1.0.0 +module Covenant.Prim + ( OneArgFunc (..), + typeOneArgFunc, + TwoArgFunc (..), + typeTwoArgFunc, + ThreeArgFunc (..), + typeThreeArgFunc, + -- SixArgFunc (..), + -- typeSixArgFunc, + ) +where + +import Covenant.DeBruijn (DeBruijn (Z)) +import Covenant.Index (ix0) +import Covenant.Type + ( AbstractTy, + CompT (Comp0, Comp1), + CompTBody (ReturnT, (:--:>)), + ValT, + boolT, + byteStringT, + g1T, + g2T, + integerT, + mlResultT, + stringT, + tyvar, + unitT, + ) +import Test.QuickCheck (Arbitrary (arbitrary), elements) + +-- | All one-argument primitives provided by Plutus. +-- +-- = Note +-- +-- We exclude the @MkNilData@ and @MkNilPairData@ primitives from this list for +-- several reasons. For clarity, we list these below. Firstly, the reason why +-- these primitives still exist at all is historical: Plutus now has the ability +-- to directly \'lift\' empty list constants into itself. Secondly, while these +-- primitives /could/ still be used instead of direct lifts, there is never a +-- reason to prefer them, as they are less efficient than embedding a constant +-- directly. Thirdly, their naive typings would end up with overdetermined type +-- variables - consider the typing of @MkNilData@: +-- +-- @forall a . () -> ![a]@ +-- +-- For all of these reasons, we do not represent these primitives in the ASG. +-- +-- @since 1.0.0 +data OneArgFunc + = LengthOfByteString + | Sha2_256 + | Sha3_256 + | Blake2b_256 + | EncodeUtf8 + | DecodeUtf8 + | -- | FstPair + -- | SndPair + -- | HeadList + -- | TailList + -- | NullList + -- | MapData + -- | ListData + -- | IData + -- | BData + -- | UnConstrData + -- | UnMapData + -- | UnListData + -- | UnIData + -- | UnBData + -- | SerialiseData + BLS12_381_G1_neg + | BLS12_381_G1_compress + | BLS12_381_G1_uncompress + | BLS12_381_G2_neg + | BLS12_381_G2_compress + | BLS12_381_G2_uncompress + | Keccak_256 + | Blake2b_224 + | ComplementByteString + | CountSetBits + | FindFirstSetBit + | Ripemd_160 + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | Does not shrink. +-- +-- @since 1.0.0 +instance Arbitrary OneArgFunc where + {-# INLINEABLE arbitrary #-} + arbitrary = + elements + [ LengthOfByteString, + Sha2_256, + Sha3_256, + Blake2b_256, + EncodeUtf8, + DecodeUtf8, + -- FstPair, + -- SndPair, + -- HeadList, + -- TailList, + -- NullList, + -- MapData, + -- ListData, + -- IData, + -- BData, + -- UnConstrData, + -- UnMapData, + -- UnListData, + -- UnIData, + -- UnBData, + -- SerialiseData, + BLS12_381_G1_neg, + BLS12_381_G1_compress, + BLS12_381_G1_uncompress, + BLS12_381_G2_neg, + BLS12_381_G2_compress, + BLS12_381_G2_uncompress, + Keccak_256, + Blake2b_224, + ComplementByteString, + CountSetBits, + FindFirstSetBit, + Ripemd_160 + ] + +-- | Produce the type of a single-argument primop. +-- +-- @since 1.0.0 +typeOneArgFunc :: OneArgFunc -> CompT AbstractTy +typeOneArgFunc = \case + LengthOfByteString -> Comp0 $ byteStringT :--:> ReturnT integerT + Sha2_256 -> hashingT + Sha3_256 -> hashingT + Blake2b_256 -> hashingT + EncodeUtf8 -> Comp0 $ stringT :--:> ReturnT byteStringT + DecodeUtf8 -> Comp0 $ byteStringT :--:> ReturnT stringT + BLS12_381_G1_neg -> Comp0 $ g1T :--:> ReturnT g1T + BLS12_381_G1_compress -> Comp0 $ g1T :--:> ReturnT byteStringT + BLS12_381_G1_uncompress -> Comp0 $ byteStringT :--:> ReturnT g1T + BLS12_381_G2_neg -> Comp0 $ g2T :--:> ReturnT g2T + BLS12_381_G2_compress -> Comp0 $ g2T :--:> ReturnT byteStringT + BLS12_381_G2_uncompress -> Comp0 $ byteStringT :--:> ReturnT g2T + Keccak_256 -> hashingT + Blake2b_224 -> hashingT + ComplementByteString -> Comp0 $ byteStringT :--:> ReturnT byteStringT + CountSetBits -> Comp0 $ byteStringT :--:> ReturnT integerT + FindFirstSetBit -> Comp0 $ byteStringT :--:> ReturnT integerT + Ripemd_160 -> hashingT + where + hashingT :: CompT AbstractTy + hashingT = Comp0 $ byteStringT :--:> ReturnT byteStringT + +-- | All two-argument primitives provided by Plutus. +-- +-- @since 1.0.0 +data TwoArgFunc + = AddInteger + | SubtractInteger + | MultiplyInteger + | DivideInteger + | QuotientInteger + | RemainderInteger + | ModInteger + | EqualsInteger + | LessThanInteger + | LessThanEqualsInteger + | AppendByteString + | ConsByteString + | IndexByteString + | EqualsByteString + | LessThanByteString + | LessThanEqualsByteString + | AppendString + | EqualsString + | ChooseUnit + | Trace + | -- | MkCons + -- | ConstrData + -- | EqualsData + -- | MkPairData + BLS12_381_G1_add + | BLS12_381_G1_scalarMul + | BLS12_381_G1_equal + | BLS12_381_G1_hashToGroup + | BLS12_381_G2_add + | BLS12_381_G2_scalarMul + | BLS12_381_G2_equal + | BLS12_381_G2_hashToGroup + | BLS12_381_millerLoop + | BLS12_381_mulMlResult + | BLS12_381_finalVerify + | ByteStringToInteger + | ReadBit + | ReplicateByte + | ShiftByteString + | RotateByteString + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | Does not shrink. +-- +-- @since 1.0.0 +instance Arbitrary TwoArgFunc where + {-# INLINEABLE arbitrary #-} + arbitrary = + elements + [ AddInteger, + SubtractInteger, + MultiplyInteger, + DivideInteger, + QuotientInteger, + RemainderInteger, + ModInteger, + EqualsInteger, + LessThanInteger, + LessThanEqualsInteger, + AppendByteString, + ConsByteString, + IndexByteString, + EqualsByteString, + LessThanByteString, + LessThanEqualsByteString, + AppendString, + EqualsString, + ChooseUnit, + Trace, + -- MkCons, + -- ConstrData, + -- EqualsData, + -- MkPairData, + BLS12_381_G1_add, + BLS12_381_G1_scalarMul, + BLS12_381_G1_equal, + BLS12_381_G1_hashToGroup, + BLS12_381_G2_add, + BLS12_381_G2_scalarMul, + BLS12_381_G2_equal, + BLS12_381_G2_hashToGroup, + BLS12_381_millerLoop, + BLS12_381_mulMlResult, + BLS12_381_finalVerify, + ByteStringToInteger, + ReadBit, + ReplicateByte, + ShiftByteString, + RotateByteString + ] + +-- | Produce the type of a two-argument primop. +-- +-- @since 1.0.0 +typeTwoArgFunc :: TwoArgFunc -> CompT AbstractTy +typeTwoArgFunc = \case + AddInteger -> combineT integerT + SubtractInteger -> combineT integerT + MultiplyInteger -> combineT integerT + DivideInteger -> combineT integerT + QuotientInteger -> combineT integerT + RemainderInteger -> combineT integerT + ModInteger -> combineT integerT + EqualsInteger -> compareT integerT + LessThanInteger -> compareT integerT + LessThanEqualsInteger -> compareT integerT + AppendByteString -> combineT byteStringT + ConsByteString -> Comp0 $ integerT :--:> byteStringT :--:> ReturnT byteStringT + IndexByteString -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT integerT + EqualsByteString -> compareT byteStringT + LessThanByteString -> compareT byteStringT + LessThanEqualsByteString -> compareT byteStringT + AppendString -> combineT stringT + EqualsString -> compareT stringT + ChooseUnit -> Comp1 $ unitT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) + Trace -> Comp1 $ stringT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) + BLS12_381_G1_add -> combineT g1T + BLS12_381_G1_scalarMul -> Comp0 $ integerT :--:> g1T :--:> ReturnT g1T + BLS12_381_G1_equal -> compareT g1T + BLS12_381_G1_hashToGroup -> Comp0 $ byteStringT :--:> byteStringT :--:> ReturnT g1T + BLS12_381_G2_add -> combineT g2T + BLS12_381_G2_scalarMul -> Comp0 $ integerT :--:> g2T :--:> ReturnT g2T + BLS12_381_G2_equal -> compareT g2T + BLS12_381_G2_hashToGroup -> Comp0 $ byteStringT :--:> byteStringT :--:> ReturnT g2T + BLS12_381_millerLoop -> Comp0 $ g1T :--:> g2T :--:> ReturnT mlResultT + BLS12_381_mulMlResult -> combineT mlResultT + BLS12_381_finalVerify -> Comp0 $ mlResultT :--:> mlResultT :--:> ReturnT boolT + ByteStringToInteger -> Comp0 $ boolT :--:> byteStringT :--:> ReturnT integerT + ReadBit -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT boolT + ReplicateByte -> Comp0 $ integerT :--:> integerT :--:> ReturnT byteStringT + ShiftByteString -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT byteStringT + RotateByteString -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT byteStringT + where + combineT :: ValT AbstractTy -> CompT AbstractTy + combineT t = Comp0 $ t :--:> t :--:> ReturnT t + compareT :: ValT AbstractTy -> CompT AbstractTy + compareT t = Comp0 $ t :--:> t :--:> ReturnT boolT + +-- | All three-argument primitives provided by Plutus. +-- +-- @since 1.0.0 +data ThreeArgFunc + = VerifyEd25519Signature + | VerifyEcdsaSecp256k1Signature + | VerifySchnorrSecp256k1Signature + | IfThenElse + | -- | ChooseList + -- | CaseList + IntegerToByteString + | AndByteString + | OrByteString + | XorByteString + | -- | WriteBits + ExpModInteger + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | Does not shrink. +-- +-- @since 1.0.0 +instance Arbitrary ThreeArgFunc where + {-# INLINEABLE arbitrary #-} + arbitrary = + elements + [ VerifyEd25519Signature, + VerifyEcdsaSecp256k1Signature, + VerifySchnorrSecp256k1Signature, + IfThenElse, + -- ChooseList, + -- CaseList, + IntegerToByteString, + AndByteString, + OrByteString, + XorByteString, + -- WriteBits, + ExpModInteger + ] + +-- | Produce the type of a three-argument primop. +-- +-- @since 1.0.0 +typeThreeArgFunc :: ThreeArgFunc -> CompT AbstractTy +typeThreeArgFunc = \case + VerifyEd25519Signature -> signatureT + VerifyEcdsaSecp256k1Signature -> signatureT + VerifySchnorrSecp256k1Signature -> signatureT + IfThenElse -> + Comp1 $ + boolT + :--:> tyvar Z ix0 + :--:> tyvar Z ix0 + :--:> ReturnT (tyvar Z ix0) + IntegerToByteString -> + Comp0 $ + boolT :--:> integerT :--:> integerT :--:> ReturnT byteStringT + AndByteString -> bitwiseT + OrByteString -> bitwiseT + XorByteString -> bitwiseT + ExpModInteger -> + Comp0 $ + integerT + :--:> integerT + :--:> integerT + :--:> ReturnT integerT + where + signatureT :: CompT AbstractTy + signatureT = + Comp0 $ + byteStringT + :--:> byteStringT + :--:> byteStringT + :--:> ReturnT boolT + bitwiseT :: CompT AbstractTy + bitwiseT = + Comp0 $ + boolT + :--:> byteStringT + :--:> byteStringT + :--:> ReturnT byteStringT + +{- +-- | All six-argument primitives provided by Plutus. +-- +-- @since 1.0.0 +data SixArgFunc + = ChooseData + | CaseData + deriving stock + ( -- | @since 1.0.0 + Eq, + -- | @since 1.0.0 + Ord, + -- | @since 1.0.0 + Show + ) + +-- | Does not shrink. +-- +-- @since 1.0.0 +instance Arbitrary SixArgFunc where + {-# INLINEABLE arbitrary #-} + arbitrary = elements [ChooseData, CaseData] +-} diff --git a/src/Covenant/Test.hs b/src/Covenant/Test.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Test.hs @@ -0,0 +1,104 @@ +-- | +-- Module: Covenant.Test +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- Utilities designed to help test Covenant itself. +-- +-- @since 1.0.0 +module Covenant.Test + ( Concrete (Concrete), + ) +where + +import Control.Applicative ((<|>)) +import Covenant.Index (count0) +import Covenant.Type + ( AbstractTy, + BuiltinFlatT + ( BLS12_381_G1_ElementT, + BLS12_381_G2_ElementT, + BLS12_381_MlResultT, + BoolT, + ByteStringT, + IntegerT, + StringT, + UnitT + ), + CompT (Comp0, CompN), + CompTBody (ArgsAndResult), + ValT (Abstraction, BuiltinFlat, ThunkT), + ) +import Data.Coerce (coerce) +import Data.Vector qualified as Vector +import Test.QuickCheck + ( Arbitrary (arbitrary, shrink), + Gen, + elements, + liftArbitrary, + oneof, + sized, + ) +import Test.QuickCheck.Instances.Vector () + +-- | Wrapper for 'ValT' to provide an 'Arbitrary' instance to generate only +-- value types without any type variables. +-- +-- @since 1.0.0 +newtype Concrete = Concrete (ValT AbstractTy) + deriving + ( -- | @since 1.0.0 + Eq + ) + via (ValT AbstractTy) + deriving stock + ( -- | @since 1.0.0 + Show + ) + +-- | @since 1.0.0 +instance Arbitrary Concrete where + {-# INLINEABLE arbitrary #-} + arbitrary = Concrete <$> sized go + where + go :: Int -> Gen (ValT AbstractTy) + go size + | size <= 0 = + BuiltinFlat + <$> elements + [ UnitT, + BoolT, + IntegerT, + StringT, + ByteStringT, + BLS12_381_G1_ElementT, + BLS12_381_G2_ElementT, + BLS12_381_MlResultT + ] + | otherwise = + oneof + [ pure . BuiltinFlat $ UnitT, + pure . BuiltinFlat $ BoolT, + pure . BuiltinFlat $ IntegerT, + pure . BuiltinFlat $ StringT, + pure . BuiltinFlat $ ByteStringT, + pure . BuiltinFlat $ BLS12_381_G1_ElementT, + pure . BuiltinFlat $ BLS12_381_G2_ElementT, + pure . BuiltinFlat $ BLS12_381_MlResultT, + ThunkT . Comp0 <$> (ArgsAndResult <$> liftArbitrary (go (size `quot` 4)) <*> go (size `quot` 4)) + ] + {-# INLINEABLE shrink #-} + shrink (Concrete v) = + Concrete <$> case v of + -- impossible + Abstraction _ -> [] + ThunkT (CompN _ (ArgsAndResult args result)) -> + ThunkT . CompN count0 <$> do + let argsList = Vector.toList args + argsList' <- fmap coerce . shrink . fmap Concrete $ argsList + result' <- fmap coerce . shrink . Concrete $ result + let args' = Vector.fromList argsList' + pure (ArgsAndResult args' result) <|> pure (ArgsAndResult args result') + -- Can't shrink this + BuiltinFlat _ -> [] diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Type.hs @@ -0,0 +1,334 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} + +-- | +-- Module: Covenant.Type +-- Copyright: (C) MLabs 2025 +-- License: Apache 2.0 +-- Maintainer: koz@mlabs.city, sean@mlabs.city +-- +-- Covenant's type system and various ways to construct types. +-- +-- @since 1.0.0 +module Covenant.Type + ( -- * Type abstractions + AbstractTy (..), + Renamed (..), + + -- * Computation types + CompT (Comp0, Comp1, Comp2, Comp3, CompN), + CompTBody (ReturnT, (:--:>), ArgsAndResult), + arity, + + -- * Value types + ValT (..), + BuiltinFlatT (..), + byteStringT, + integerT, + stringT, + tyvar, + boolT, + g1T, + g2T, + mlResultT, + unitT, + + -- * Renaming + + -- ** Types + RenameError (..), + RenameM, + + -- ** Introduction + renameValT, + renameCompT, + + -- ** Elimination + runRenameM, + + -- * Type application + TypeAppError (..), + checkApp, + ) +where + +import Control.Monad (guard) +import Covenant.DeBruijn (DeBruijn) +import Covenant.Index + ( Count, + Index, + count0, + count1, + count2, + count3, + intCount, + ) +import Covenant.Internal.Rename + ( RenameError + ( InvalidAbstractionReference, + IrrelevantAbstraction, + UndeterminedAbstraction + ), + RenameM, + renameCompT, + renameValT, + runRenameM, + ) +import Covenant.Internal.Type + ( AbstractTy (BoundAt), + BuiltinFlatT + ( BLS12_381_G1_ElementT, + BLS12_381_G2_ElementT, + BLS12_381_MlResultT, + BoolT, + ByteStringT, + IntegerT, + StringT, + UnitT + ), + CompT (CompT), + CompTBody (CompTBody), + Renamed (Rigid, Unifiable, Wildcard), + ValT (Abstraction, BuiltinFlat, ThunkT), + ) +import Covenant.Internal.Unification + ( TypeAppError + ( DoesNotUnify, + ExcessArgs, + InsufficientArgs, + LeakingUnifiable, + LeakingWildcard + ), + checkApp, + ) +import Data.Coerce (coerce) +import Data.Kind (Type) +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Data.Vector.NonEmpty (NonEmptyVector) +import Data.Vector.NonEmpty qualified as NonEmpty +import Optics.Core (preview) + +-- | The body of a computation type that doesn't take any arguments and produces +-- the a result of the given value type. Use this just as you would a +-- data constructor. +-- +-- = Example +-- +-- * @'ReturnT' 'integerT'@ is @!Integer@ +-- +-- @since 1.0.0 +pattern ReturnT :: forall (a :: Type). ValT a -> CompTBody a +pattern ReturnT x <- CompTBody (returnHelper -> Just x) + where + ReturnT x = CompTBody (NonEmpty.singleton x) + +-- | Given a type of argument, and the body of another computation type, +-- construct a copy of the body, adding an extra argument of the argument type. +-- Use this just as you would a data constructor. +-- +-- = Note +-- +-- Together with 'ReturnT', these two patterns provide an exhaustive pattern +-- match. +-- +-- = Example +-- +-- * @'integerT' :--:> ReturnT 'byteStringT'@ is @Integer -> !ByteString@ +-- +-- @since 1.0.0 +pattern (:--:>) :: + forall (a :: Type). + ValT a -> + CompTBody a -> + CompTBody a +pattern x :--:> xs <- CompTBody (arrowHelper -> Just (x, xs)) + where + x :--:> xs = CompTBody (NonEmpty.cons x (coerce xs)) + +infixr 1 :--:> + +-- | A view of a computation type as a 'Vector' of its argument types, together +-- with its result type. Can be used as a data constructor, and is an exhaustive +-- match. +-- +-- = Example +-- +-- * @'ArgsAndResult' ('Vector.fromList' ['integerT', 'integerT']) 'integerT'@ +-- is @Integer -> Integer -> !Integer@ +-- +-- @since 1.0.0 +pattern ArgsAndResult :: + forall (a :: Type). + Vector (ValT a) -> + ValT a -> + CompTBody a +pattern ArgsAndResult args result <- (argsAndResultHelper -> (args, result)) + where + ArgsAndResult args result = CompTBody (NonEmpty.snocV args result) + +{-# COMPLETE ArgsAndResult #-} + +{-# COMPLETE ReturnT, (:--:>) #-} + +-- | Determine the arity of a computation type: that is, how many arguments a +-- function of this type must be given. +-- +-- @since 1.0.0 +arity :: forall (a :: Type). CompT a -> Int +arity (CompT _ (CompTBody xs)) = NonEmpty.length xs - 1 + +-- | A computation type that does not bind any type variables. Use this like a +-- data constructor. +-- +-- @since 1.0.0 +pattern Comp0 :: + forall (a :: Type). + CompTBody a -> + CompT a +pattern Comp0 xs <- (countHelper 0 -> Just xs) + where + Comp0 xs = CompT count0 xs + +-- | A computation type that binds one type variable (that +-- is, something whose type is @forall a . ... -> ...)@. Use this like a data +-- constructor. +-- +-- @since 1.0.0 +pattern Comp1 :: + forall (a :: Type). + CompTBody a -> + CompT a +pattern Comp1 xs <- (countHelper 1 -> Just xs) + where + Comp1 xs = CompT count1 xs + +-- | A computation type that binds two type variables (that +-- is, something whose type is @forall a b . ... -> ...)@. Use this like a data +-- constructor. +-- +-- @since 1.0.0 +pattern Comp2 :: + forall (a :: Type). + CompTBody a -> + CompT a +pattern Comp2 xs <- (countHelper 2 -> Just xs) + where + Comp2 xs = CompT count2 xs + +-- | A computation type that binds three type variables +-- (that is, something whose type is @forall a b c . ... -> ...)@. Use this like +-- a data constructor. +-- +-- @since 1.0.0 +pattern Comp3 :: + forall (a :: Type). + CompTBody a -> + CompT a +pattern Comp3 xs <- (countHelper 3 -> Just xs) + where + Comp3 xs = CompT count3 xs + +-- | A general way to construct and deconstruct computations which bind an +-- arbitrary number of type variables. Use this like a data constructor. Unlike +-- the other @Comp@ patterns, 'CompN' is exhaustive if matched on. +-- +-- @since 1.0.0 +pattern CompN :: + Count "tyvar" -> + CompTBody AbstractTy -> + CompT AbstractTy +pattern CompN count xs <- CompT count xs + where + CompN count xs = CompT count xs + +{-# COMPLETE CompN #-} + +-- | Helper for defining type variables. +-- +-- @since 1.0.0 +tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy +tyvar db = Abstraction . BoundAt db + +-- | Helper for defining the value type of builtin bytestrings. +-- +-- @since 1.0.0 +byteStringT :: forall (a :: Type). ValT a +byteStringT = BuiltinFlat ByteStringT + +-- | Helper for defining the value type of builtin integers. +-- +-- @since 1.0.0 +integerT :: forall (a :: Type). ValT a +integerT = BuiltinFlat IntegerT + +-- | Helper for defining the value type of builtin strings. +-- +-- @since 1.0.0 +stringT :: forall (a :: Type). ValT a +stringT = BuiltinFlat StringT + +-- | Helper for defining the value type of builtin booleans. +-- +-- @since 1.0.0 +boolT :: forall (a :: Type). ValT a +boolT = BuiltinFlat BoolT + +-- | Helper for defining the value type of BLS12-381 G1 curve points. +-- +-- @since 1.0.0 +g1T :: forall (a :: Type). ValT a +g1T = BuiltinFlat BLS12_381_G1_ElementT + +-- | Helper for defining the value type of BLS12-381 G2 curve points. +-- +-- @since 1.0.0 +g2T :: forall (a :: Type). ValT a +g2T = BuiltinFlat BLS12_381_G2_ElementT + +-- | Helper for defining the value type of BLS12-381 multiplication results. +-- +-- @since 1.0.0 +mlResultT :: forall (a :: Type). ValT a +mlResultT = BuiltinFlat BLS12_381_MlResultT + +-- | Helper for defining the value type of the builtin unit type. +-- +-- @since 1.0.0 +unitT :: forall (a :: Type). ValT a +unitT = BuiltinFlat UnitT + +-- Helpers + +returnHelper :: + forall (a :: Type). + NonEmptyVector (ValT a) -> + Maybe (ValT a) +returnHelper xs = case NonEmpty.uncons xs of + (y, ys) -> + if Vector.length ys == 0 + then pure y + else Nothing + +arrowHelper :: + forall (a :: Type). + NonEmptyVector (ValT a) -> + Maybe (ValT a, CompTBody a) +arrowHelper xs = case NonEmpty.uncons xs of + (y, ys) -> (y,) . CompTBody <$> NonEmpty.fromVector ys + +argsAndResultHelper :: + forall (a :: Type). + CompTBody a -> + (Vector (ValT a), ValT a) +argsAndResultHelper (CompTBody xs) = NonEmpty.unsnoc xs + +countHelper :: + forall (a :: Type). + Int -> + CompT a -> + Maybe (CompTBody a) +countHelper expected (CompT actual xs) = do + expectedCount <- preview intCount expected + guard (expectedCount == actual) + pure xs diff --git a/src/Covenant/Util.hs b/src/Covenant/Util.hs new file mode 100644 --- /dev/null +++ b/src/Covenant/Util.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} + +-- | Module: Covenant.Util +-- +-- Various helpers that don't fit anywhere else. +-- +-- @since 1.0.0 +module Covenant.Util + ( pattern NilV, + pattern ConsV, + ) +where + +import Data.Kind (Type) +import Data.Vector.Generic (Vector) +import Data.Vector.Generic qualified as Vector + +-- | A pattern matching helper for vectors (of all types), corresponding to @[]@ +-- for lists. This pattern is bidirectional, which means it can be used just +-- like a data constructor. +-- +-- @since 1.0.0 +pattern NilV :: forall (a :: Type) (v :: Type -> Type). (Vector v a) => v a +pattern NilV <- (Vector.uncons -> Nothing) + where + NilV = Vector.empty + +-- | A pattern matching helper for vectors (of all types), corresponding to @x : +-- xs@-style matches. This is a read-only pattern, which means you can match +-- with it, but not construct; this is done because @cons@ for vectors is +-- inefficient and should thus be used consciously, using appropriate functions. +-- +-- Together with 'NilV', 'ConsV' provides an exhaustive match. +-- +-- @since 1.0.0 +pattern ConsV :: + forall (a :: Type) (v :: Type -> Type). + (Vector v a) => + a -> + v a -> + v a +pattern ConsV x xs <- (Vector.uncons -> Just (x, xs)) + +{-# COMPLETE NilV, ConsV #-} diff --git a/test/asg/Main.hs b/test/asg/Main.hs new file mode 100644 --- /dev/null +++ b/test/asg/Main.hs @@ -0,0 +1,467 @@ +{-# LANGUAGE PatternSynonyms #-} + +module Main (main) where + +import Control.Applicative ((<|>)) +import Control.Monad (guard) +import Covenant.ASG + ( ASG, + ASGBuilder, + ASGNode (ACompNode, AValNode), + CompNodeInfo + ( Builtin1, + Builtin2, + Builtin3, + Return + ), + CovenantError (EmptyASG, TopLevelError, TopLevelValue, TypeError), + CovenantTypeError + ( ApplyCompType, + ApplyToError, + ApplyToValType, + ForceCompType, + ForceError, + ForceNonThunk, + LambdaResultsInValType, + NoSuchArgument, + ReturnCompType, + ThunkError, + ThunkValType + ), + Id, + Ref (AnArg, AnId), + ValNodeInfo (Lit), + app, + arg, + builtin1, + builtin2, + builtin3, + err, + force, + lam, + lit, + nodeAt, + ret, + runASGBuilder, + thunk, + topLevelNode, + ) +import Covenant.Constant (typeConstant) +import Covenant.DeBruijn (DeBruijn (Z)) +import Covenant.Index (Index, intIndex, ix0) +import Covenant.Prim + ( typeOneArgFunc, + typeThreeArgFunc, + typeTwoArgFunc, + ) +import Covenant.Test (Concrete (Concrete)) +import Covenant.Type + ( AbstractTy, + CompT (Comp0, CompN), + CompTBody (ArgsAndResult, ReturnT), + ValT, + arity, + ) +import Covenant.Util (pattern ConsV, pattern NilV) +import Data.Coerce (coerce) +import Data.Kind (Type) +import Data.Maybe (fromJust) +import Data.Vector qualified as Vector +import Optics.Core (preview, review) +import Test.QuickCheck + ( Gen, + Property, + arbitrary, + conjoin, + counterexample, + forAllShrinkShow, + liftShrink, + listOf, + property, + shrink, + (===), + ) +import Test.Tasty (adjustOption, defaultMain, testGroup) +import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) +import Test.Tasty.QuickCheck (QuickCheckTests, testProperty) + +main :: IO () +main = + defaultMain . adjustOption moreTests . testGroup "ASG" $ + [ testCase "empty ASG does not compile" unitEmptyASG, + testCase "single error does not compile" unitSingleError, + testCase "forcing an error does not compile" unitForceError, + testCase "thunking an error does not compile" unitThunkError, + testProperty "toplevel constant does not compile" propTopLevelConstant, + testProperty "toplevel one-arg builtin compiles and has the right type" propTopLevelBuiltin1, + testProperty "toplevel two-arg builtin compiles and has the right type" propTopLevelBuiltin2, + testProperty "toplevel three-arg builtin compiles and has the right type" propTopLevelBuiltin3, + testProperty "toplevel return compiles and has the right type" propTopLevelReturn, + testProperty "forcing a thunk has the same type as what the thunk wraps" propForceThunk, + testProperty "applying zero arguments to a return has the same type as what the return wraps" propApplyReturn, + testProperty "forcing a computation type does not compile" propForceComp, + testProperty "forcing a non-thunk value type does not compile" propForceNonThunk, + testProperty "thunking a value type does not compile" propThunkValType, + testProperty "applying arguments to a value does not compile" propApplyToVal, + testProperty "applying arguments to an error does not compile" propApplyToError, + testProperty "passing computations as arguments does not compile" propApplyComp, + testProperty "requesting a non-existent argument does not compile" propNonExistentArg, + testProperty "requesting an argument that exists compiles" propExistingArg, + testProperty "returning a computation from a lambda does not compile" propReturnComp, + testProperty "a lambda body having a value type does not compile" propLambdaValBody + ] + where + moreTests :: QuickCheckTests -> QuickCheckTests + moreTests = max 10_000 + +-- Units + +unitEmptyASG :: IO () +unitEmptyASG = do + let builtUp = pure () + let expected = Left EmptyASG + let actual = runASGBuilder builtUp + assertEqual "" expected actual + +unitSingleError :: IO () +unitSingleError = do + let builtUp = err + let expected = Left TopLevelError + let actual = runASGBuilder builtUp + assertEqual "" expected actual + +unitForceError :: IO () +unitForceError = do + let builtUp = err >>= \i -> force (AnId i) + let result = runASGBuilder builtUp + case result of + Left (TypeError _ ForceError) -> pure () + _ -> assertFailure $ "Unexpected result: " <> show result + +unitThunkError :: IO () +unitThunkError = do + let builtUp = err >>= thunk + let result = runASGBuilder builtUp + case result of + Left (TypeError _ ThunkError) -> pure () + _ -> assertFailure $ "Unexpected result: " <> show result + +-- Properties + +propTopLevelConstant :: Property +propTopLevelConstant = forAllShrinkShow arbitrary shrink show $ \c -> + let builtUp = lit c + in withCompilationFailure builtUp $ \case + TopLevelValue _ t info -> case info of + Lit c' -> + conjoin + [ typeConstant c === t, + c' === c + ] + _ -> failUnexpectedValNodeInfo info + err' -> failWithCounterExample ("Unexpected failure type: " <> show err') + +propTopLevelBuiltin1 :: Property +propTopLevelBuiltin1 = forAllShrinkShow arbitrary shrink show $ \bi1 -> + let builtUp = builtin1 bi1 + in withCompilationSuccess builtUp $ \asg -> + withToplevelCompNode asg $ \t info -> + case info of + Builtin1 bi -> + conjoin + [ t === typeOneArgFunc bi1, + bi === bi1 + ] + _ -> failUnexpectedCompNodeInfo info + +propTopLevelBuiltin2 :: Property +propTopLevelBuiltin2 = forAllShrinkShow arbitrary shrink show $ \bi2 -> + let builtUp = builtin2 bi2 + in withCompilationSuccess builtUp $ \asg -> + withToplevelCompNode asg $ \t info -> + case info of + Builtin2 bi -> + conjoin + [ t === typeTwoArgFunc bi2, + bi === bi2 + ] + _ -> failUnexpectedCompNodeInfo info + +propTopLevelBuiltin3 :: Property +propTopLevelBuiltin3 = forAllShrinkShow arbitrary shrink show $ \bi3 -> + let builtUp = builtin3 bi3 + in withCompilationSuccess builtUp $ \asg -> + withToplevelCompNode asg $ \t info -> + case info of + Builtin3 bi -> + conjoin + [ t === typeThreeArgFunc bi3, + bi === bi3 + ] + _ -> failUnexpectedCompNodeInfo info + +propTopLevelReturn :: Property +propTopLevelReturn = forAllShrinkShow arbitrary shrink show $ \c -> + let builtUp = lit c >>= \i -> ret (AnId i) + in withCompilationSuccess builtUp $ \asg -> + withToplevelCompNode asg $ \t info -> + case info of + Return r -> withExpectedId r $ \i -> + withExpectedValNode i asg $ \t' info' -> + case info' of + Lit c' -> + let cT = typeConstant c + in conjoin + [ c' === c, + cT === t', + t === Comp0 (ReturnT cT) + ] + _ -> failUnexpectedValNodeInfo info' + _ -> failUnexpectedCompNodeInfo info + +-- We use builtins only for this test, but this should demonstrate the +-- properties well enough +propForceThunk :: Property +propForceThunk = forAllShrinkShow arbitrary shrink show $ \x -> + let (comp, forceThunkComp) = case x of + Left bi1 -> mkComps builtin1 bi1 + Right (Left bi2) -> mkComps builtin2 bi2 + Right (Right bi3) -> mkComps builtin3 bi3 + in withCompilationSuccess comp $ \expectedASG -> + withCompilationSuccess forceThunkComp $ \forceThunkASG -> + withToplevelCompNode expectedASG $ \expectedT _ -> + withToplevelCompNode forceThunkASG $ \actualT _ -> + expectedT === actualT + where + mkComps :: + forall (a :: Type). + (a -> ASGBuilder Id) -> a -> (ASGBuilder Id, ASGBuilder Id) + mkComps f x = + let comp = f x + forceThunkComp = do + i <- comp + thunkI <- thunk i + force (AnId thunkI) + in (comp, forceThunkComp) + +-- As we can't build toplevel value ASGs, this has to be a bit roundabout +propApplyReturn :: Property +propApplyReturn = forAllShrinkShow arbitrary shrink show $ \c -> + let comp = do + i <- lit c + ret (AnId i) + applyReturnComp = do + i <- comp + applied <- app i Vector.empty + ret (AnId applied) + in withCompilationSuccess comp $ \expectedASG -> + withCompilationSuccess applyReturnComp $ \applyReturnASG -> + withToplevelCompNode expectedASG $ \expectedT _ -> + withToplevelCompNode applyReturnASG $ \actualT _ -> + expectedT === actualT + +propForceComp :: Property +propForceComp = forAllShrinkShow arbitrary shrink show $ \x -> + let comp = do + i <- case x of + Left bi1 -> builtin1 bi1 + Right (Left bi2) -> builtin2 bi2 + Right (Right bi3) -> builtin3 bi3 + force (AnId i) + expectedT = case x of + Left bi1 -> typeOneArgFunc bi1 + Right (Left bi2) -> typeTwoArgFunc bi2 + Right (Right bi3) -> typeThreeArgFunc bi3 + in withCompilationFailure comp $ \case + TypeError _ (ForceCompType actualT) -> expectedT === actualT + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +propForceNonThunk :: Property +propForceNonThunk = forAllShrinkShow arbitrary shrink show $ \c -> + let comp = do + i <- lit c + force (AnId i) + in withCompilationFailure comp $ \case + TypeError _ (ForceNonThunk actualT) -> typeConstant c === actualT + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +propThunkValType :: Property +propThunkValType = forAllShrinkShow arbitrary shrink show $ \c -> + let comp = do + i <- lit c + thunk i + in withCompilationFailure comp $ \case + TypeError _ (ThunkValType actualT) -> typeConstant c === actualT + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +propApplyToVal :: Property +propApplyToVal = forAllShrinkShow arbitrary shrink show $ \c args -> + let comp = do + args' <- traverse (fmap AnId . lit) args + i <- lit c + app i args' + in withCompilationFailure comp $ \case + TypeError _ (ApplyToValType t) -> typeConstant c === t + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +propApplyToError :: Property +propApplyToError = forAllShrinkShow arbitrary shrink show $ \args -> + let comp = do + args' <- traverse (fmap AnId . lit) args + i <- err + app i args' + in withCompilationFailure comp $ \case + TypeError _ ApplyToError -> property True + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +-- We use only builtins for this test, and specifically a one-argument builtin +-- for the thing being applied to, but this should still demonstrate the +-- behaviour as we expect +propApplyComp :: Property +propApplyComp = forAllShrinkShow arbitrary shrink show $ \f arg1 -> + let t = case arg1 of + Left bi1 -> typeOneArgFunc bi1 + Right (Left bi2) -> typeTwoArgFunc bi2 + Right (Right bi3) -> typeThreeArgFunc bi3 + + comp = do + i <- builtin1 f + arg' <- case arg1 of + Left bi1 -> builtin1 bi1 + Right (Left bi2) -> builtin2 bi2 + Right (Right bi3) -> builtin3 bi3 + app i (Vector.singleton . AnId $ arg') + in withCompilationFailure comp $ \case + TypeError _ (ApplyCompType actualT) -> t === actualT + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +propNonExistentArg :: Property +propNonExistentArg = forAllShrinkShow arbitrary shrink show $ \(db, index) -> + let comp = arg db index >>= \i -> ret (AnArg i) + in withCompilationFailure comp $ \case + TypeError _ (NoSuchArgument db' index') -> conjoin [db === db', index === index'] + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +-- Generate a lambda taking an arbitrary (positive) number of arguments, plus a +-- positional index, then return that argument in the body. The type of the +-- lambda we get back should match. +propExistingArg :: Property +propExistingArg = forAllShrinkShow gen shr show $ \(t, index) -> + let comp = lam t $ do + arg1 <- arg Z index + ret (AnArg arg1) + in withCompilationSuccess comp $ \asg -> + withToplevelCompNode asg $ \t' _ -> + t' === t + where + gen :: Gen (CompT AbstractTy, Index "arg") + gen = do + Concrete argT <- arbitrary + prefixArgs <- listOf (arbitrary @Concrete) + suffixArgs <- listOf (arbitrary @Concrete) + -- We know that lengths can't be negative, but GHC doesn't + let index = fromJust . preview intIndex $ length prefixArgs + let args = Vector.fromList $ coerce prefixArgs <> [argT] <> coerce suffixArgs + pure (Comp0 $ ArgsAndResult args argT, index) + -- We shrink only in the index and the number of arguments, as shrinking the + -- argument types themselves doesn't change anything + shr :: (CompT AbstractTy, Index "arg") -> [(CompT AbstractTy, Index "arg")] + shr (t@(CompN _ (ArgsAndResult args _)), index) + | arity t <= 1 = [] + | index == ix0 = do + args' <- liftShrink (const []) . fmap Concrete $ args + case args' of + NilV -> [] -- no arguments left to use + ConsV (Concrete res') _ -> pure (Comp0 (ArgsAndResult (coerce args') res'), index) + | otherwise = + let shrinkOnIndex = do + index' <- shrink index + let indexAsInt = review intIndex index + case args Vector.!? indexAsInt of + Nothing -> [] -- Should be impossible + Just res' -> pure (Comp0 (ArgsAndResult args res'), index') + shrinkOnArgs = do + args' <- liftShrink (const []) . fmap Concrete $ args + let indexAsInt = review intIndex index + guard (indexAsInt < Vector.length args') + case args' Vector.!? indexAsInt of + Nothing -> [] -- Should be impossible + Just (Concrete res') -> pure (Comp0 (ArgsAndResult (coerce args') res'), index) + in shrinkOnIndex <|> shrinkOnArgs + +propReturnComp :: Property +propReturnComp = forAllShrinkShow arbitrary shrink show $ \x -> + let t = case x of + Left bi1 -> typeOneArgFunc bi1 + Right (Left bi2) -> typeTwoArgFunc bi2 + Right (Right bi3) -> typeThreeArgFunc bi3 + comp = do + i <- case x of + Left bi1 -> builtin1 bi1 + Right (Left bi2) -> builtin2 bi2 + Right (Right bi3) -> builtin3 bi3 + ret (AnId i) + in withCompilationFailure comp $ \case + TypeError _ (ReturnCompType actualT) -> t === actualT + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +propLambdaValBody :: Property +propLambdaValBody = forAllShrinkShow arbitrary shrink show $ \(Concrete t, c) -> + let resultT = typeConstant c + comp = lam (Comp0 (ArgsAndResult (Vector.singleton t) resultT)) $ lit c + in withCompilationFailure comp $ \case + TypeError _ (LambdaResultsInValType actualT) -> resultT === actualT + TypeError _ err' -> failWrongTypeError err' + err' -> failWrongError err' + +-- Helpers + +failWrongTypeError :: CovenantTypeError -> Property +failWrongTypeError err' = failWithCounterExample ("Unexpected type error: " <> show err') + +failWrongError :: CovenantError -> Property +failWrongError err' = failWithCounterExample ("Unexpected error: " <> show err') + +withCompilationFailure :: ASGBuilder Id -> (CovenantError -> Property) -> Property +withCompilationFailure comp cb = case runASGBuilder comp of + Left err' -> cb err' + Right asg -> failWithCounterExample ("Unexpected success: " <> show asg) + +withCompilationSuccess :: ASGBuilder Id -> (ASG -> Property) -> Property +withCompilationSuccess comp cb = case runASGBuilder comp of + Left err' -> failWithCounterExample ("Unexpected failure: " <> show err') + Right asg -> cb asg + +withToplevelCompNode :: ASG -> (CompT AbstractTy -> CompNodeInfo -> Property) -> Property +withToplevelCompNode asg cb = case topLevelNode asg of + ACompNode t info -> cb t info + node -> failWithCounterExample ("Unexpected toplevel node: " <> show node) + +failWithCounterExample :: String -> Property +failWithCounterExample msg = counterexample msg . property $ False + +failUnexpectedCompNodeInfo :: CompNodeInfo -> Property +failUnexpectedCompNodeInfo info = + failWithCounterExample ("Unexpected CompNodeInfo: " <> show info) + +failUnexpectedValNodeInfo :: ValNodeInfo -> Property +failUnexpectedValNodeInfo info = + failWithCounterExample ("Unexpected ValNodeInfo: " <> show info) + +withExpectedId :: Ref -> (Id -> Property) -> Property +withExpectedId r cb = case r of + AnId i -> cb i + AnArg arg' -> failWithCounterExample ("Unexpected argument: " <> show arg') + +withExpectedValNode :: Id -> ASG -> (ValT AbstractTy -> ValNodeInfo -> Property) -> Property +withExpectedValNode i asg cb = case nodeAt i asg of + AValNode t info -> cb t info + node -> failWithCounterExample ("Unexpected node: " <> show node) diff --git a/test/primops/Main.hs b/test/primops/Main.hs new file mode 100644 --- /dev/null +++ b/test/primops/Main.hs @@ -0,0 +1,108 @@ +module Main (main) where + +import Covenant.Prim + ( typeOneArgFunc, + typeThreeArgFunc, + typeTwoArgFunc, + ) +import Covenant.Type + ( AbstractTy (BoundAt), + CompT, + Renamed (Unifiable), + arity, + renameCompT, + runRenameM, + ) +import Data.Functor.Classes (liftEq) +import Data.Kind (Type) +import Test.QuickCheck + ( Arbitrary (arbitrary), + Property, + counterexample, + forAll, + property, + (===), + ) +import Test.Tasty (defaultMain, testGroup) +import Test.Tasty.QuickCheck (testProperty) + +main :: IO () +main = + defaultMain . testGroup "Primops" $ + [ -- Since there are so few primops, we don't increase the test count + -- beyond the default 100, as it would just be redundant. + testGroup + "Arity" + [ testProperty "One-argument primops take one argument" prop1Arg, + testProperty "Two-argument primops take two arguments" prop2Args, + testProperty "Three-argument primops take three arguments" prop3Args + -- testProperty "Six-argument primops take six arguments" prop6Args + ], + testGroup + "Renaming" + [ testProperty "One-argument primops rename correctly" prop1Rename, + testProperty "Two-argument primops rename correctly" prop2Rename, + testProperty "Three-argument primops rename correctly" prop3Rename + -- testProperty "Six-argument primops rename correctly" prop6Rename + ] + ] + +-- Test cases and properties + +prop1Arg :: Property +prop1Arg = mkArgProp typeOneArgFunc 1 + +prop1Rename :: Property +prop1Rename = mkRenameProp typeOneArgFunc + +prop2Args :: Property +prop2Args = mkArgProp typeTwoArgFunc 2 + +prop2Rename :: Property +prop2Rename = mkRenameProp typeTwoArgFunc + +prop3Args :: Property +prop3Args = mkArgProp typeThreeArgFunc 3 + +prop3Rename :: Property +prop3Rename = mkRenameProp typeThreeArgFunc + +{- +prop6Args :: Property +prop6Args = mkArgProp typeSixArgFunc 6 + +prop6Rename :: Property +prop6Rename = mkRenameProp typeSixArgFunc +-} + +-- Helpers + +mkArgProp :: + forall (a :: Type). + (Show a, Arbitrary a) => + (a -> CompT AbstractTy) -> + Int -> + Property +mkArgProp typingFun targetArity = forAll arbitrary $ \f -> + let t = typingFun f + in arity t === targetArity + +mkRenameProp :: + forall (a :: Type). + (Show a, Arbitrary a) => + (a -> CompT AbstractTy) -> + Property +mkRenameProp typingFun = forAll arbitrary $ \f -> + let t = typingFun f + result = runRenameM . renameCompT $ t + in case result of + Left err -> counterexample (show err) False + Right renamed -> property $ liftEq eqRenamedVar t renamed + +-- In our context, the _only_ variables we have are unifiable. If we see +-- anything else, we know we've messed up somewhere. Furthermore, the indexes +-- should 'line up'. +eqRenamedVar :: AbstractTy -> Renamed -> Bool +eqRenamedVar (BoundAt _ ix) = \case + Unifiable ix' -> ix == ix' + _ -> False diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs new file mode 100644 --- /dev/null +++ b/test/renaming/Main.hs @@ -0,0 +1,185 @@ +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE PatternSynonyms #-} + +module Main (main) where + +import Covenant.DeBruijn (DeBruijn (S, Z)) +import Covenant.Index + ( ix0, + ix1, + ) +import Covenant.Test (Concrete (Concrete)) +import Covenant.Type + ( BuiltinFlatT + ( BLS12_381_G1_ElementT, + BLS12_381_G2_ElementT, + BLS12_381_MlResultT, + BoolT, + ByteStringT, + IntegerT, + StringT, + UnitT + ), + CompT (Comp0, Comp1, Comp2), + RenameError + ( InvalidAbstractionReference, + UndeterminedAbstraction + ), + Renamed (Unifiable, Wildcard), + ValT (Abstraction, BuiltinFlat, ThunkT), + renameCompT, + renameValT, + runRenameM, + tyvar, + pattern ReturnT, + pattern (:--:>), + ) +import Data.Functor.Classes (liftEq) +import Data.Kind (Type) +import Test.QuickCheck + ( Arbitrary (arbitrary, shrink), + Property, + forAllShrinkShow, + ) +import Test.Tasty (adjustOption, defaultMain, testGroup) +import Test.Tasty.HUnit (assertBool, assertEqual, testCase) +import Test.Tasty.QuickCheck (QuickCheckTests, testProperty) + +main :: IO () +main = + defaultMain . adjustOption moreTests . testGroup "Renaming" $ + [ testGroup + "Builtin flat types" + [ testCase "UnitT" $ testFlat UnitT, + testCase "BoolT" $ testFlat BoolT, + testCase "IntegerT" $ testFlat IntegerT, + testCase "StringT" $ testFlat StringT, + testCase "ByteStringT" $ testFlat ByteStringT, + testCase "G1ElementT" $ testFlat BLS12_381_G1_ElementT, + testCase "G2ElementT" $ testFlat BLS12_381_G2_ElementT, + testCase "MlResultT" $ testFlat BLS12_381_MlResultT + ], + testProperty "Nested concrete types" propNestedConcrete, + testCase "forall a . a -> !a" testIdT, + testCase "forall a b . a -> b -> !a" testConstT, + testCase "forall a . a -> !(forall b . b -> !a)" testConstT2, + testGroup + "Overdeterminance" + [ testCase "forall a b . a -> !(b -> !a)" testDodgyConstT, + testCase "forall a b . a -> !a" testDodgyIdT + ], + testGroup + "Non-existent abstractions" + [ testCase "forall a . b -> !a" testIndexingIdT + ] + ] + where + -- Note (Koz, 26/02/2025): By default, QuickCheck runs only 100 tests per + -- property, which is far to few. Using the method below, we can ensure that + -- we run a decent number of tests, while also permitting more than this to + -- be set via the CLI if we want. + moreTests :: QuickCheckTests -> QuickCheckTests + moreTests = max 10_000 + +-- Tests and properties + +-- Checks that the given 'flat' type renames to itself. +testFlat :: BuiltinFlatT -> IO () +testFlat t = do + let input = BuiltinFlat t + let result = runRenameM . renameValT $ input + assertRight (assertBool "" . liftEq (\_ _ -> False) input) result + +-- Checks that for any 'fully concretified' type (nested or not), renaming +-- changes nothing. +propNestedConcrete :: Property +propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) -> + let result = runRenameM . renameValT $ t + in case result of + Left _ -> False + Right actual -> liftEq (\_ _ -> False) t actual + +-- Checks that `forall a . a -> !a` correctly renames. +testIdT :: IO () +testIdT = do + let idT = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) + let expected = + Comp1 $ + Abstraction (Unifiable ix0) + :--:> ReturnT (Abstraction (Unifiable ix0)) + let result = runRenameM . renameCompT $ idT + assertRight (assertEqual "" expected) result + +-- Checks that `forall a b . a -> b -> !a` correctly renames. +testConstT :: IO () +testConstT = do + let constT = Comp2 $ tyvar Z ix0 :--:> tyvar Z ix1 :--:> ReturnT (tyvar Z ix0) + let expected = + Comp2 $ + Abstraction (Unifiable ix0) + :--:> Abstraction (Unifiable ix1) + :--:> ReturnT (Abstraction (Unifiable ix0)) + let result = runRenameM . renameCompT $ constT + assertRight (assertEqual "" expected) result + +-- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames. +testConstT2 :: IO () +testConstT2 = do + let constT = + Comp1 $ tyvar Z ix0 :--:> ReturnT (ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar (S Z) ix0)) + let expected = + Comp1 $ + Abstraction (Unifiable ix0) + :--:> ReturnT + ( ThunkT . Comp1 $ + Abstraction (Wildcard 1 2 ix0) + :--:> ReturnT (Abstraction (Unifiable ix0)) + ) + let result = runRenameM . renameCompT $ constT + assertRight (assertEqual "" expected) result + +-- Checks that `forall a b . a -> !a` triggers the undetermined variable checker. +testDodgyIdT :: IO () +testDodgyIdT = do + let idT = Comp2 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) + let result = runRenameM . renameCompT $ idT + case result of + Left UndeterminedAbstraction -> assertBool "" True + Left _ -> assertBool "wrong renaming error" False + _ -> assertBool "renaming succeeded when it should have failed" False + +-- Checks that `forall a b. a -> !(b -> !a)` triggers the undetermined variable checker. +testDodgyConstT :: IO () +testDodgyConstT = do + let constT = + Comp2 $ + tyvar Z ix0 + :--:> ReturnT (ThunkT . Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix0)) + let result = runRenameM . renameCompT $ constT + case result of + Left UndeterminedAbstraction -> assertBool "" True + Left _ -> assertBool "wrong renaming error" False + _ -> assertBool "renaming succeeded when it should have failed" False + +-- Checks that `forall a . b -> !a` triggers the variable indexing checker. +testIndexingIdT :: IO () +testIndexingIdT = do + let t = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix1) + let result = runRenameM . renameCompT $ t + case result of + Left (InvalidAbstractionReference trueLevel ix) -> do + assertEqual "" trueLevel 1 + assertEqual "" ix ix1 + Left _ -> assertBool "wrong renaming error" False + _ -> assertBool "renaming succeeded when it should have failed" False + +-- Helpers + +assertRight :: + forall (a :: Type) (b :: Type). + (b -> IO ()) -> + Either a b -> + IO () +assertRight f = \case + Left _ -> assertBool "renamer errored" False + Right actual -> f actual diff --git a/test/type-applications/Main.hs b/test/type-applications/Main.hs new file mode 100644 --- /dev/null +++ b/test/type-applications/Main.hs @@ -0,0 +1,369 @@ +{-# LANGUAGE PatternSynonyms #-} + +module Main (main) where + +import Control.Applicative ((<|>)) +import Control.Monad (guard) +import Covenant.DeBruijn (DeBruijn (S, Z), asInt) +import Covenant.Index + ( Index, + ix0, + ix1, + ) +import Covenant.Test (Concrete (Concrete)) +import Covenant.Type + ( AbstractTy, + CompT (Comp0, Comp1, Comp2), + Renamed (Rigid, Wildcard), + TypeAppError + ( DoesNotUnify, + ExcessArgs, + InsufficientArgs + ), + ValT + ( Abstraction, + ThunkT + ), + checkApp, + integerT, + renameCompT, + renameValT, + runRenameM, + tyvar, + pattern ReturnT, + pattern (:--:>), + ) +import Data.Coerce (coerce) +import Data.Functor.Identity (Identity (Identity)) +import Data.Kind (Type) +import Data.Vector qualified as Vector +import Test.QuickCheck + ( Gen, + Property, + arbitrary, + counterexample, + discard, + elements, + forAllShrink, + getSize, + liftShrink, + oneof, + shrink, + suchThat, + vectorOf, + (===), + ) +import Test.Tasty (adjustOption, defaultMain, testGroup) +import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) +import Test.Tasty.QuickCheck (QuickCheckTests, testProperty) + +main :: IO () +main = + defaultMain . adjustOption moreTests . testGroup "Type application" $ + [ testProperty "Too many arguments to id" propTooManyArgs, + testCase "id on no arguments" unitInsufficientArgs, + testGroup + "Substitution" + [ testProperty "id applied to concrete" propIdConcrete, + testProperty "two-arg const to same concretes" propConst2Same, + testProperty "two-arg const to different concretes" propConst2Different + ], + testGroup + "Unification" + [ testProperty "concrete expected, concrete actual" propUnifyConcrete, + testProperty "rigid expected, concrete actual" propUnifyRigidConcrete, + testProperty "wildcard expected, concrete actual" propUnifyWildcardConcrete, + testProperty "wildcard expected, unifiable actual" propUnifyWildcardUnifiable, + testProperty "concrete expected, rigid actual" propUnifyConcreteRigid, + testProperty "unifiable expected, rigid actual" propUnifyUnifiableRigid, + testProperty "rigid expected, rigid actual" propUnifyRigid, + testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid + ] + ] + where + -- Note (Koz, 26/02/2025): By default, QuickCheck runs only 100 tests per + -- property, which is far too few. Using the method below, we can ensure that + -- we run a decent number of tests, while also permitting more than this to + -- be set via the CLI if we want. + moreTests :: QuickCheckTests -> QuickCheckTests + moreTests = max 10_000 + +-- Units and properties + +-- Try to apply more than one argument to `forall a . a -> !a`. +-- Result should indicate excess arguments. +propTooManyArgs :: Property +propTooManyArgs = forAllShrink gen shr $ \excessArgs -> + withRenamedComp idT $ \renamedIdT -> + withRenamedVals excessArgs $ \renamedExcessArgs -> + case renamedExcessArgs of + [] -> discard -- should be impossible + _ : extraArgs -> + let expected = Left . ExcessArgs renamedIdT . Vector.fromList . fmap Just $ extraArgs + actual = checkApp renamedIdT (fmap Just renamedExcessArgs) + in expected === actual + where + -- Note (Koz, 14/04/2025): The default size of 100 makes it rather painful + -- to generate excess arguments, as the generator used for concrete types + -- is recursive. Furthermore, we need to ensure the list has at least two + -- elements, which forces too many restarts. Thus, we roll our own. + gen :: Gen [ValT AbstractTy] + gen = do + size <- getSize + lenIncrease <- elements [0, 1 .. size `quot` 4] + Concrete firstTy <- arbitrary + Concrete secondTy <- arbitrary + ([firstTy, secondTy] <>) <$> vectorOf lenIncrease (coerce @Concrete <$> arbitrary) + shr :: [ValT AbstractTy] -> [[ValT AbstractTy]] + shr = \case + [] -> [] + [_] -> [] + [_, _] -> [] + xs -> liftShrink (coerce . shrink . Concrete) xs + +-- Try to apply `forall a . a -> !a` to zero arguments. Result should indicate +-- insufficient arguments. +unitInsufficientArgs :: IO () +unitInsufficientArgs = do + renamedIdT <- failLeft . runRenameM . renameCompT $ idT + let expected = Left . InsufficientArgs $ renamedIdT + let actual = checkApp renamedIdT [] + assertEqual "" expected actual + +-- Try to apply `forall a . a -> !a` to a random concrete type. Result should be +-- that type. +propIdConcrete :: Property +propIdConcrete = forAllShrink arbitrary shrink $ \(Concrete t) -> + withRenamedComp idT $ \renamedIdT -> + withRenamedVals (Identity t) $ \(Identity t') -> + let expected = Right t' + actual = checkApp renamedIdT [Just t'] + in expected === actual + +-- Try to apply `forall a b . a -> b -> !a` to two identical concrete types. +-- Result should be that type. +propConst2Same :: Property +propConst2Same = forAllShrink arbitrary shrink $ \(Concrete t) -> + withRenamedComp const2T $ \renamedConst2T -> + withRenamedVals (Identity t) $ \(Identity t') -> + let expected = Right t' + actual = checkApp renamedConst2T [Just t', Just t'] + in expected === actual + +-- Try to apply `forall a b . a -> b -> !a` to two random _different_ concrete +-- types. Result should be the choice for `a`. +propConst2Different :: Property +propConst2Different = forAllShrink arbitrary shrink $ \(Concrete t1, Concrete t2) -> + if t1 == t2 + then discard + else withRenamedComp const2T $ \renamedConst2T -> + withRenamedVals (Identity t1) $ \(Identity t1') -> + withRenamedVals (Identity t2) $ \(Identity t2') -> + let expected = Right t1' + actual = checkApp renamedConst2T [Just t1', Just t2'] + in expected === actual + +-- Randomly pick a concrete type `A`, then pick a type `b` which is either `A` +-- or a type different from `A` (50% of the time each way). Then try to apply `A +-- -> !Integer` to `b`. Result should unify be `Integer` if `b ~ A`, and a +-- unification error otherwise. +propUnifyConcrete :: Property +propUnifyConcrete = forAllShrink gen shr $ \(tA, mtB) -> + withRenamedComp (Comp0 $ tA :--:> ReturnT integerT) $ \f -> + withRenamedVals (Identity tA) $ \(Identity tA') -> + case mtB of + Nothing -> + let expected = Right integerT + actual = checkApp f [Just tA'] + in expected === actual + Just tB -> + if tA == tB + then discard + else withRenamedVals (Identity tB) $ \(Identity arg) -> + let expected = Left . DoesNotUnify tA' $ arg + actual = checkApp f [Just arg] + in expected === actual + where + -- This ensures that our cases occur with equal frequency. + gen :: Gen (ValT AbstractTy, Maybe (ValT AbstractTy)) + gen = do + Concrete x <- arbitrary + (x,) <$> oneof [pure Nothing, Just . coerce <$> arbitrary @Concrete] + -- We don't want to 'shrink out of case'; if we have a `Just`, we want to + -- keep it a `Just`. + shr :: (ValT AbstractTy, Maybe (ValT AbstractTy)) -> [(ValT AbstractTy, Maybe (ValT AbstractTy))] + shr (x, my) = do + Concrete x' <- shrink (Concrete x) + case my of + Nothing -> pure (x', Nothing) + Just y -> do + Concrete y' <- shrink (Concrete y) + pure (x', my) <|> pure (x, Just y') + +-- Randomly pick a rigid type A and concrete type B, then try to apply `A -> +-- !Integer` to `b`. Result should fail to unify. +propUnifyRigidConcrete :: Property +propUnifyRigidConcrete = forAllShrink arbitrary shrink $ \(Concrete t, scope, ix) -> + withRenamedComp (Comp0 $ tyvar (S scope) ix :--:> ReturnT integerT) $ \f -> + withRenamedVals (Identity t) $ \(Identity t') -> + -- This is a little confusing, as we would expect that the true level will + -- be based on `S scope`, since that's what's in the computation type. + -- However, we actually have to reduce it by 1, as we have a 'scope + -- stepdown' for `f` even though we bind no variables. + let trueLevel = negate . asInt $ scope + expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t' + actual = checkApp f [Just t'] + in expected === actual + +-- Randomly pick a concrete type A, then try to apply `(forall a . a -> +-- !Integer) -> !Integer` to `(A -> !Integer)`. Result should fail to unify. +propUnifyWildcardConcrete :: Property +propUnifyWildcardConcrete = forAllShrink arbitrary shrink $ \(Concrete t) -> + let thunk = ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT integerT + in withRenamedComp (Comp0 $ thunk :--:> ReturnT integerT) $ \f -> + let argT = ThunkT . Comp0 $ t :--:> ReturnT integerT + in withRenamedVals (Identity argT) $ \(Identity argT') -> + let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT + expected = Left . DoesNotUnify lhs $ argT' + actual = checkApp f [Just argT'] + in expected === actual + +-- Randomly generate a concrete type A, then try to apply +-- `(forall a . a -> !A) -> !A` to `forall a . (a -> !A)`. Result should unify +-- to `A`. +propUnifyWildcardUnifiable :: Property +propUnifyWildcardUnifiable = forAllShrink arbitrary shrink $ \(Concrete t) -> + withRenamedComp (Comp0 $ ThunkT (Comp1 $ tyvar Z ix0 :--:> ReturnT t) :--:> ReturnT t) $ \f -> + withRenamedVals (Identity t) $ \(Identity t') -> + withRenamedVals (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) -> + let expected = Right t' + actual = checkApp f [Just arg] + in expected === actual + +-- Randomly generate a concrete type A, and a rigid type B, then try to apply `A +-- -> !Integer` to `B`. Result should fail to unify. +propUnifyConcreteRigid :: Property +propUnifyConcreteRigid = forAllShrink arbitrary shrink $ \(Concrete aT, scope, index) -> + withRenamedComp (Comp0 $ aT :--:> ReturnT integerT) $ \f -> + withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) -> + withRenamedVals (Identity aT) $ \(Identity aT') -> + let level = negate . asInt $ scope + expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index + actual = checkApp f [Just arg] + in expected === actual + +-- Randomly generate a rigid type A, then try to apply `forall a . a -> !a` to +-- `A`. Result should unify to `A`. +propUnifyUnifiableRigid :: Property +propUnifyUnifiableRigid = forAllShrink arbitrary shrink $ \(scope, index) -> + withRenamedComp idT $ \f -> + withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) -> + let expected = Right arg + actual = checkApp f [Just arg] + in expected === actual + +-- Randomly generate a scope S and an index I, then another scope S' and another +-- index I', that may or may not be different to S and/or I respectively. Let +-- `T` be the rigid type that results from `S` and `I`, and `U` be the rigid +-- type that results from `S'` and `I'`. Attempt to unify `T -> !Integer` with +-- `U`. This should unify to `Integer` if, and only if, `T == U`; otherwise, it +-- should fail to unify. +propUnifyRigid :: Property +propUnifyRigid = forAllShrink gen shr $ \testData -> + withTestData testData $ \(f, arg, expected) -> + let actual = checkApp f [Just arg] + in expected === actual + where + gen :: Gen (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) + gen = do + db <- arbitrary + index <- arbitrary + (db,index,) + <$> oneof + [ pure Nothing, + Just . Left <$> suchThat arbitrary (db /=), + Just . Right <$> suchThat arbitrary (index /=) + ] + shr :: + (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) -> + [(DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))] + shr (db, index, mrest) = do + db' <- shrink db + index' <- shrink index + case mrest of + Nothing -> pure (db', index, Nothing) <|> pure (db, index', Nothing) + Just (Left db2) -> do + db2' <- shrink db2 + (db', index, Just (Left db2)) <$ guard (db' /= db2) + <|> pure (db, index', Just (Left db2)) + <|> (db, index, Just (Left db2')) <$ guard (db /= db2') + Just (Right index2) -> do + index2' <- shrink index2 + pure (db', index, Just (Right index2)) + <|> (db, index', Just (Right index2)) <$ guard (index' /= index2) + <|> (db, index, Just (Right index2')) <$ guard (index /= index2') + withTestData :: + (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) -> + ((CompT Renamed, ValT Renamed, Either TypeAppError (ValT Renamed)) -> Property) -> + Property + withTestData (db, index, mrest) f = + withRenamedComp (Comp0 $ tyvar (S db) index :--:> ReturnT integerT) $ \fun -> + case mrest of + Nothing -> withRenamedVals (Identity . tyvar db $ index) $ \(Identity arg) -> + f (fun, arg, Right integerT) + Just rest -> + let level = negate . asInt $ db + lhs = Abstraction . Rigid level $ index + in case rest of + Left db2 -> withRenamedVals (Identity . tyvar db2 $ index) $ \(Identity arg) -> + f (fun, arg, Left . DoesNotUnify lhs $ arg) + Right index2 -> withRenamedVals (Identity . tyvar db $ index2) $ \(Identity arg) -> + f (fun, arg, Left . DoesNotUnify lhs $ arg) + +-- Randomly pick a rigid type A, then try to apply `(forall a . a -> !Integer) +-- -> !Integer` to `(A -> !Integer)`. Result should fail to unify. +propUnifyWildcardRigid :: Property +propUnifyWildcardRigid = forAllShrink arbitrary shrink $ \(scope, index) -> + let thunk = ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT integerT + in withRenamedComp (Comp0 $ thunk :--:> ReturnT integerT) $ \f -> + let argT = ThunkT . Comp0 $ tyvar (S scope) index :--:> ReturnT integerT + in withRenamedVals (Identity argT) $ \(Identity argT') -> + let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT + expected = Left . DoesNotUnify lhs $ argT' + actual = checkApp f [Just argT'] + in expected === actual + +-- Helpers + +-- `forall a. a -> !a` +idT :: CompT AbstractTy +idT = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) + +-- `forall a b . a -> b -> !a +const2T :: CompT AbstractTy +const2T = Comp2 $ tyvar Z ix0 :--:> tyvar Z ix1 :--:> ReturnT (tyvar Z ix0) + +failLeft :: + forall (a :: Type) (b :: Type). + (Show a) => + Either a b -> + IO b +failLeft = either (assertFailure . show) pure + +withRenamedComp :: + CompT AbstractTy -> + (CompT Renamed -> Property) -> + Property +withRenamedComp t f = case runRenameM . renameCompT $ t of + Left err -> counterexample (show err) False + Right t' -> f t' + +withRenamedVals :: + forall (t :: Type -> Type). + (Traversable t) => + t (ValT AbstractTy) -> + (t (ValT Renamed) -> Property) -> + Property +withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of + Left err -> counterexample (show err) False + Right vals' -> f vals'