penelope-core (empty) → 0.1.0.0

raw patch · 15 files changed

+2293/−0 lines, 15 filesdep +basedep +containersdep +hspec

Dependencies added: base, containers, hspec, inspection-testing, penelope-core, polytropos-core, polytropos-plugin, primitive, text

Files

• CHANGELOG.md +14/−0
• LICENSE +189/−0
• README.md +10/−0
• penelope-core.cabal +121/−0
• src/Penelope/Core.hs +25/−0
• src/Penelope/Core/Engine.hs +21/−0
• src/Penelope/Core/Engine/Elaborate.hs +142/−0
• src/Penelope/Core/Engine/Interpret.hs +187/−0
• src/Penelope/Core/Engine/Partial.hs +211/−0
• src/Penelope/Core/Route.hs +93/−0
• src/Penelope/Core/Send.hs +97/−0
• src/Penelope/Core/Syntax.hs +145/−0
• src/Penelope/Core/Wiring.hs +372/−0
• test/Inspection.hs +193/−0
• test/Main.hs +473/−0

@@ -0,0 +1,14 @@+# Changelog for penelope-core++## 0.1.0.0 — Initial Release++- Core polycategorical engine generalizing Heftia and Kernmantle.+- Unpacked `(m,n,k,r)`-ary polycategorical syntax GADT: `Polycategorical`.+- $O(1)$ jump-table route optimization via Polytropos row indexing.+- High-level smart constructors: `inject`, `fanout`, `assocL`, `assocR`, `swapSum`, `swapProd`, `distributeL`, `distributeR`.+- Sequential polycategorical composition (`composePoly`, `>>>`).+- Categorical frame rule wiring (`frame`, `cross`).+- Disjunctive polycategorical fanout (`fanoutDisj`).+- Row weakening and structural embedding (`weakenPoly`).+- Higher-order algebraic elaboration and vector interpretation engine.+- Partial interpretation substrate with structural residualization.

@@ -0,0 +1,189 @@+EUROPEAN UNION PUBLIC LICENCE v. 1.2+EUPL © the European Union 2007, 2016++This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined below) which is provided under the+terms of this Licence. Any use of the Work, other than as authorised under this Licence is prohibited (to the extent such+use is covered by a right of the copyright holder of the Work).+The Work is provided under the terms of this Licence when the Licensor (as defined below) has placed the following+notice immediately following the copyright notice for the Work:+                          Licensed under the EUPL+or has expressed by any other means his willingness to license under the EUPL.++1.Definitions+In this Licence, the following terms have the following meaning:+— ‘The Licence’:this Licence.+— ‘The Original Work’:the work or software distributed or communicated by the Licensor under this Licence, available+as Source Code and also as Executable Code as the case may be.+— ‘Derivative Works’:the works or software that could be created by the Licensee, based upon the Original Work or+modifications thereof. This Licence does not define the extent of modification or dependence on the Original Work+required in order to classify a work as a Derivative Work; this extent is determined by copyright law applicable in+the country mentioned in Article 15.+— ‘The Work’:the Original Work or its Derivative Works.+— ‘The Source Code’:the human-readable form of the Work which is the most convenient for people to study and+modify.+— ‘The Executable Code’:any code which has generally been compiled and which is meant to be interpreted by+a computer as a program.+— ‘The Licensor’:the natural or legal person that distributes or communicates the Work under the Licence.+— ‘Contributor(s)’:any natural or legal person who modifies the Work under the Licence, or otherwise contributes to+the creation of a Derivative Work.+— ‘The Licensee’ or ‘You’:any natural or legal person who makes any usage of the Work under the terms of the+Licence.+— ‘Distribution’ or ‘Communication’:any act of selling, giving, lending, renting, distributing, communicating,+transmitting, or otherwise making available, online or offline, copies of the Work or providing access to its essential+functionalities at the disposal of any other natural or legal person.++2.Scope of the rights granted by the Licence+The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, sublicensable licence to do the following, for+the duration of copyright vested in the Original Work:+— use the Work in any circumstance and for all usage,+— reproduce the Work,+— modify the Work, and make Derivative Works based upon the Work,+— communicate to the public, including the right to make available or display the Work or copies thereof to the public+and perform publicly, as the case may be, the Work,+— distribute the Work or copies thereof,+— lend and rent the Work or copies thereof,+— sublicense rights in the Work or copies thereof.+Those rights can be exercised on any media, supports and formats, whether now known or later invented, as far as the+applicable law permits so.+In the countries where moral rights apply, the Licensor waives his right to exercise his moral right to the extent allowed+by law in order to make effective the licence of the economic rights here above listed.+The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to any patents held by the Licensor, to the+extent necessary to make use of the rights granted on the Work under this Licence.++3.Communication of the Source Code+The Licensor may provide the Work either in its Source Code form, or as Executable Code. If the Work is provided as+Executable Code, the Licensor provides in addition a machine-readable copy of the Source Code of the Work along with+each copy of the Work that the Licensor distributes or indicates, in a notice following the copyright notice attached to+the Work, a repository where the Source Code is easily and freely accessible for as long as the Licensor continues to+distribute or communicate the Work.++4.Limitations on copyright+Nothing in this Licence is intended to deprive the Licensee of the benefits from any exception or limitation to the+exclusive rights of the rights owners in the Work, of the exhaustion of those rights or of other applicable limitations+thereto.++5.Obligations of the Licensee+The grant of the rights mentioned above is subject to some restrictions and obligations imposed on the Licensee. Those+obligations are the following:++Attribution right: The Licensee shall keep intact all copyright, patent or trademarks notices and all notices that refer to+the Licence and to the disclaimer of warranties. The Licensee must include a copy of such notices and a copy of the+Licence with every copy of the Work he/she distributes or communicates. The Licensee must cause any Derivative Work+to carry prominent notices stating that the Work has been modified and the date of modification.++Copyleft clause: If the Licensee distributes or communicates copies of the Original Works or Derivative Works, this+Distribution or Communication will be done under the terms of this Licence or of a later version of this Licence unless+the Original Work is expressly distributed only under this version of the Licence — for example by communicating+‘EUPL v. 1.2 only’. The Licensee (becoming Licensor) cannot offer or impose any additional terms or conditions on the+Work or Derivative Work that alter or restrict the terms of the Licence.++Compatibility clause: If the Licensee Distributes or Communicates Derivative Works or copies thereof based upon both+the Work and another work licensed under a Compatible Licence, this Distribution or Communication can be done+under the terms of this Compatible Licence. For the sake of this clause, ‘Compatible Licence’ refers to the licences listed+in the appendix attached to this Licence. Should the Licensee's obligations under the Compatible Licence conflict with+his/her obligations under this Licence, the obligations of the Compatible Licence shall prevail.++Provision of Source Code: When distributing or communicating copies of the Work, the Licensee will provide+a machine-readable copy of the Source Code or indicate a repository where this Source will be easily and freely available+for as long as the Licensee continues to distribute or communicate the Work.+Legal Protection: This Licence does not grant permission to use the trade names, trademarks, service marks, or 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 copyright notice.++6.Chain of Authorship+The original Licensor warrants that the copyright in the Original Work granted hereunder is owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each Contributor warrants that the copyright in the modifications he/she brings to the Work are owned by him/her or+licensed to him/her and that he/she has the power and authority to grant the Licence.+Each time You accept the Licence, the original Licensor and subsequent Contributors grant You a licence to their contributions+to the Work, under the terms of this Licence.++7.Disclaimer of Warranty+The Work is a work in progress, which is continuously improved by numerous Contributors. It is not a finished work+and may therefore contain defects or ‘bugs’ inherent to this type of development.+For the above reason, the Work is provided under the Licence on an ‘as is’ basis and without warranties of any kind+concerning the Work, including without limitation merchantability, fitness for a particular purpose, absence of defects or+errors, accuracy, non-infringement of intellectual property rights other than copyright as stated in Article 6 of this+Licence.+This disclaimer of warranty is an essential part of the Licence and a condition for the grant of any rights to the Work.++8.Disclaimer of Liability+Except in the cases of wilful misconduct or damages directly caused to natural persons, the Licensor will in no event be+liable for any direct or indirect, material or moral, damages of any kind, arising out of the Licence or of the use of the+Work, including without limitation, damages for loss of goodwill, work stoppage, computer failure or malfunction, loss+of data or any commercial damage, even if the Licensor has been advised of the possibility of such damage. However,+the Licensor will be liable under statutory product liability laws as far such laws apply to the Work.++9.Additional agreements+While distributing the Work, You may choose to conclude an additional agreement, defining obligations or services+consistent with this Licence. However, if accepting obligations, You may act only on your own behalf and on your sole+responsibility, not on behalf of the original Licensor or 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+the fact You have accepted any warranty or additional liability.++10.Acceptance of the Licence+The provisions of this Licence can be accepted by clicking on an icon ‘I agree’ placed under the bottom of a window+displaying the text of this Licence or by affirming consent in any other similar way, in accordance with the rules of+applicable law. Clicking on that icon indicates your clear and irrevocable acceptance of this Licence and all of its terms+and conditions.+Similarly, you irrevocably accept this Licence and all of its terms and conditions by exercising any rights granted to You+by Article 2 of this Licence, such as the use of the Work, the creation by You of a Derivative Work or the Distribution+or Communication by You of the Work or copies thereof.++11.Information to the public+In case of any Distribution or Communication of the Work by means of electronic communication by You (for example,+by offering to download the Work from a remote location) the distribution channel or media (for example, a website)+must at least provide to the public the information requested by the applicable law regarding the Licensor, the Licence+and the way it may be accessible, concluded, stored and reproduced by the Licensee.++12.Termination of the Licence+The Licence and the rights granted hereunder will terminate automatically upon any breach by the Licensee of the terms+of the Licence.+Such a termination will not terminate the licences of any person who has received the Work from the Licensee under+the Licence, provided such persons remain in full compliance with the Licence.++13.Miscellaneous+Without prejudice of Article 9 above, the Licence represents the complete agreement between the Parties as to the+Work.+If any provision of the Licence is invalid or unenforceable under applicable law, this will not affect the validity or+enforceability of the Licence as a whole. Such provision will be construed or reformed so as necessary to make it valid+and enforceable.+The European Commission may publish other linguistic versions or new versions of this Licence or updated versions of+the Appendix, so far this is required and reasonable, without reducing the scope of the rights granted by the Licence.+New versions of the Licence will be published with a unique version number.+All linguistic versions of this Licence, approved by the European Commission, have identical value. Parties can take+advantage of the linguistic version of their choice.++14.Jurisdiction+Without prejudice to specific agreement between parties,+— any litigation resulting from the interpretation of this License, arising between the European Union institutions,+bodies, offices or agencies, as a Licensor, and any Licensee, will be subject to the jurisdiction of the Court of Justice+of the European Union, as laid down in article 272 of the Treaty on the Functioning of the European Union,+— any litigation arising between other parties and resulting from the interpretation of this License, will be subject to+the exclusive jurisdiction of the competent court where the Licensor resides or conducts its primary business.++15.Applicable Law+Without prejudice to specific agreement between parties,+— this Licence shall be governed by the law of the European Union Member State where the Licensor has his seat,+resides or has his registered office,+— this licence shall be governed by Belgian law if the Licensor has no seat, residence or registered office inside+a European Union Member State.++Appendix++‘Compatible Licences’ according to Article 5 EUPL are:+— GNU General Public License (GPL) v. 2, v. 3+— GNU Affero General Public License (AGPL) v. 3+— Open Software License (OSL) v. 2.1, v. 3.0+— Eclipse Public License (EPL) v. 1.0+— CeCILL v. 2.0, v. 2.1+— Mozilla Public Licence (MPL) v. 2+— GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3+— Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for works other than software+— European Union Public Licence (EUPL) v. 1.1, v. 1.2+— Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong Reciprocity (LiLiQ-R+).++The European Commission may update this Appendix to later versions of the above licences without producing+a new version of the EUPL, as long as they provide the rights granted in Article 2 of this Licence and protect the+covered Source Code from exclusive appropriation.+All other changes or additions to this Appendix require the production of a new EUPL version.

@@ -0,0 +1,10 @@+# penelope-core++Domain package for penelope-core++## Modules+++## License++EUPL-1.2

@@ -0,0 +1,121 @@+cabal-version: 3.0+name: penelope-core+version: 0.1.0.0+synopsis: Unpacked (m,n,k,r)-ary Polycategorical Effect System Core+description:+  Core polycategorical effect engine generalizing Heftia and Kernmantle.+  Provides the unpacked (m,n,k,r)-ary polycategorical syntax GADT,+  O(1) jump-table route optimization via Polytropos row indexing,+  categorical frame rule wiring, disjunctive fanout, row weakening,+  higher-order algebraic elaboration, and vector interpretation.+license: EUPL-1.2+license-file: LICENSE+author: Nadia Yvette Chambers+maintainer: nadia.yvette.chambers@ik.me+category: Control+homepage: https://github.com/NadiaYvette/penelope+bug-reports: https://github.com/NadiaYvette/penelope/issues+extra-doc-files:+  README.md+  CHANGELOG.md+build-type: Simple+tested-with: GHC == 9.14.1++source-repository head+  type: git+  location: https://github.com/NadiaYvette/penelope+  subdir: packages/penelope-core++library+  exposed-modules:+    Penelope.Core+    Penelope.Core.Syntax+    Penelope.Core.Route+    Penelope.Core.Send+    Penelope.Core.Wiring+    Penelope.Core.Engine+    Penelope.Core.Engine.Elaborate+    Penelope.Core.Engine.Interpret+    Penelope.Core.Engine.Partial+  hs-source-dirs: src+  default-language: Haskell2010+  default-extensions:+    AllowAmbiguousTypes+    BangPatterns+    DataKinds+    DerivingStrategies+    FlexibleContexts+    FlexibleInstances+    GADTs+    KindSignatures+    MagicHash+    MultiParamTypeClasses+    OverloadedStrings+    PolyKinds+    RankNTypes+    ScopedTypeVariables+    TypeApplications+    TypeFamilies+    TypeOperators+    UnboxedTuples+  ghc-options: -Wall -Wcompat -Wredundant-constraints+  build-depends:+    base >= 4.14 && < 5,+    text >= 2.0 && < 2.2,+    containers >= 0.6 && < 0.9,+    primitive >= 0.9 && < 0.10,+    polytropos-core >= 0.1 && < 0.2,+    polytropos-plugin >= 0.1 && < 0.2++test-suite tests+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test+  default-language: Haskell2010+  default-extensions:+    AllowAmbiguousTypes+    DataKinds+    GADTs+    MagicHash+    OverloadedStrings+    PolyKinds+    RankNTypes+    TypeApplications+    TypeOperators+  ghc-options: -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts+  build-depends:+    base >= 4.14 && < 5,+    hspec >= 2.11 && < 2.12,+    text >= 2.0 && < 2.2,+    primitive >= 0.9 && < 0.10,+    penelope-core,+    polytropos-core >= 0.1 && < 0.2,+    polytropos-plugin >= 0.1 && < 0.2++test-suite inspection+  type: exitcode-stdio-1.0+  main-is: Inspection.hs+  hs-source-dirs: test+  default-language: Haskell2010+  default-extensions:+    AllowAmbiguousTypes+    DataKinds+    GADTs+    MagicHash+    OverloadedStrings+    PolyKinds+    RankNTypes+    ScopedTypeVariables+    TemplateHaskell+    TypeApplications+    TypeFamilies+    TypeOperators+  ghc-options: -Wall -Wcompat -Wredundant-constraints -threaded -rtsopts+  build-depends:+    base >= 4.14 && < 5,+    hspec >= 2.11 && < 2.12,+    inspection-testing >= 0.5 && < 0.7,+    primitive >= 0.9 && < 0.10,+    penelope-core,+    polytropos-core >= 0.1 && < 0.2,+    polytropos-plugin >= 0.1 && < 0.2

@@ -0,0 +1,25 @@+{- |+Module      : Penelope.Core+Description : High-level re-export facade for penelope-core+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Foundational exports for Penelope core polycategorical effect engine.+See Note [Core Architecture] [ref:note-core-architecture].+-}+module Penelope.Core+  ( module Penelope.Core.Syntax+  , module Penelope.Core.Route+  , module Penelope.Core.Send+  , module Penelope.Core.Wiring+  , module Penelope.Core.Engine+  ) where++import Penelope.Core.Syntax+import Penelope.Core.Route+import Penelope.Core.Send+import Penelope.Core.Wiring+import Penelope.Core.Engine

@@ -0,0 +1,21 @@+{- |+Module      : Penelope.Core.Engine+Description : High-level re-export facade for Penelope execution engine+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Provides execution engines for Penelope: Phase 1 elaboration, Phase 2 interpretation, and partial peeling.+See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+module Penelope.Core.Engine+  ( module Penelope.Core.Engine.Elaborate+  , module Penelope.Core.Engine.Interpret+  , module Penelope.Core.Engine.Partial+  ) where++import Penelope.Core.Engine.Elaborate+import Penelope.Core.Engine.Interpret+import Penelope.Core.Engine.Partial

@@ -0,0 +1,142 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{- |+Module      : Penelope.Core.Engine.Elaborate+Description : Phase 1 single-pass bottom-up higher-order effect elaboration+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Provides Phase 1 single-pass bottom-up macro elaboration of higher-order scoped+effects into pure first-order operations.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and+Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+module Penelope.Core.Engine.Elaborate+  ( -- * Elaborator Abstraction+    Elaborator (..)+  , Elaborators+  , MapRow++    -- * Phase 1 Elaboration Engine+  , elaborateAll+  ) where++import Data.Functor.Identity (Identity (..))+import Data.Kind (Type)+import Data.Primitive.SmallArray (indexSmallArray)+import GHC.Exts (Any, Int (..), unsafeCoerce#, word2Int#)+import Penelope.Core.Syntax+  ( BranchCont (..)+  , Penelope (..)+  , PolyEffect+  , PolyHEffect+  , Region (..)+  )+import Penelope.Core.Wiring (rmapFused)+import Polytropos (Pair (..), Record, RowOf, gatherRecord)+import Polytropos.Core (Rep (..), RowRep (..))+import Polytropos.RowMorph (RowMorph, unsafeMkRowMorph)++-- | Map a higher-order type constructor over each field of a row.+type family MapRow (f :: k -> Type) (r :: RowOf k) :: RowOf Type where+  MapRow f '[] = '[]+  MapRow f ((l ':= v) ': rest) = (l ':= f v) ': MapRow f rest++-- | Convenient type alias for a record of elaborators.+type Elaborators ef eh = Record (MapRow (Elaborator '[] ef) eh)++{- |+An 'Elaborator' translates a higher-order \((m, n, k, r)\)-ary scoped operation @h@+into a pure first-order 'Penelope' computation.++Notice that:+1. All \(r\) nested regions in @Record regions@ have ALREADY+   been recursively elaborated before 'runElaborator' is called (bottom-up catamorphism).+2. The elaborator receives the \(k\) downstream continuation branches+   @Record exits@ directly, allowing it to wire region exits straight into downstream+   branches without intermediate ADT allocations.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+newtype Elaborator+          (eh' :: RowOf PolyHEffect)+          (ef  :: RowOf PolyEffect)+          (h   :: PolyHEffect)+  = Elaborator+  { runElaborator+      :: forall (regions :: RowOf Type) (opIns :: RowOf Type) (exits :: RowOf Type)+                (frameIns :: RowOf Type) (frameOuts :: RowOf Type).+         RowMorph opIns frameIns+      -> Record regions+      -> Any+      -> Record exits+      -> Penelope eh' ef frameIns frameOuts+  }++{- |+Elaborates all higher-order scoped effects @eh@ into pure first-order effects @ef@+in a single bottom-up pass over the syntax tree.+Dispatch at each 'OpH' node is a branchless \(O(1)\) 'indexSmallArray#' read into the+Polytropos 'Record' of elaborators.++Contravariant reduct gathering via 'gatherRecord' adapts outer elaborators to inner+scopes across 'ScopeRow' boundaries in \(O(|eh_{sub}|)\) time without walking the inner sub-tree.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and+Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+{-# INLINE elaborateAll #-}+elaborateAll ::+  forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect)+         (ins :: RowOf Type) (outs :: RowOf Type).+  Record (MapRow (Elaborator '[] ef) eh)+  -> Penelope eh ef ins outs+  -> Penelope '[] ef ins outs+elaborateAll !elabs = go+  where+    elabCont ::+      BranchCont (Penelope eh ef i o) branchOuts+      -> BranchCont (Penelope '[] ef i o) branchOuts+    elabCont (BranchCont k) = BranchCont (\branchFrame -> go (k branchFrame))++    elabRegion :: Region eh ef sig -> Region '[] ef sig+    elabRegion (Region subPipe) = Region (elaborateAll elabs subPipe)++    go :: Penelope eh ef i o -> Penelope '[] ef i o+    go = \case+      Route morph ->+        Route morph++      LiftPure inMap f cont ->+        LiftPure inMap f (elabCont cont)++      OpF tag# inMap opAny conts ->+        OpF tag# inMap opAny (rmapFused elabCont conts)++      OpH tag# inMap regions opAny conts ->+        let !elaboratedRegions = rmapFused elabRegion regions+            !elaboratedConts   = rmapFused elabCont conts+            !(RowRep (Rep _ arr)) = elabs+            !(Identity elabAny) = indexSmallArray arr (I# (word2Int# tag#))+            !(Elaborator elabFn) = unsafeCoerce# elabAny+        in elabFn (unsafeCoerce# inMap) elaboratedRegions opAny elaboratedConts++      ScopeRow ehMorph efMorph subPipe ->+        let !subElabs = unsafeCoerce# (gatherRecord (unsafeCoerce# ehMorph) elabs)+        in ScopeRow (unsafeMkRowMorph []) efMorph (elaborateAll subElabs subPipe)

@@ -0,0 +1,187 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++{- |+Module      : Penelope.Core.Engine.Interpret+Description : Phase 2 bulk vector-dispatched algebraic interpretation+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Provides Phase 2 bulk vector-dispatched algebraic interpretation over first-order operations.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and+Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+module Penelope.Core.Engine.Interpret+  ( -- * Carrier Abstraction+    PolyCarrier (..)+  , FrameKleisli (..)++    -- * Handler Abstraction+  , Handler (..)+  , Handlers++    -- * Phase 2 Interpretation Engine+  , interpretAll+  , runPenelopePure+  ) where++import Control.Category (Category (..))+import Data.Functor.Identity (Identity (..))+import Data.Kind (Type)+import Data.Primitive.SmallArray (indexSmallArray)+import GHC.Exts (Any, Int (..), unsafeCoerce#, word2Int#)+import Penelope.Core.Engine.Elaborate (MapRow)+import Penelope.Core.Syntax+  ( BranchCont (..)+  , Penelope (..)+  , PolyEffect+  )+import Penelope.Core.Wiring (rmapFused)+import Polytropos (Record, RowOf, emptyRecord, gatherRecord)+import Polytropos.Core (Rep (..), RowRep (..))+import Polytropos.RowMorph (RowMorph, gatherRep)+import Prelude hiding (id, (.))++{- |+Typeclass for target semantic carriers \(m :: RowOf Type -> RowOf Type -> Type\)+that can execute compiled first-order 'Penelope' graphs.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+class Category m => PolyCarrier m where+  -- | Execute a pure static 'RowMorph' port permutation or projection.+  evalRoute :: RowMorph outs ins -> m ins outs++  -- | Execute a pure step over a gathered subset of ports and feed outputs to continuation.+  evalLiftPure ::+    RowMorph opIns ins+    -> (Record opIns -> Record opOuts)+    -> (Record opOuts -> m ins outs)+    -> m ins outs++{- |+Standard in-memory frame execution carrier: a Kleisli arrow over flat 'Record' frames.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+newtype FrameKleisli (f :: Type -> Type) (ins :: RowOf Type) (outs :: RowOf Type) = FrameKleisli+  { runFrameKleisli :: Record ins -> f (Record outs)+  }++instance Monad f => Category (FrameKleisli f) where+  id = FrameKleisli pure+  FrameKleisli g . FrameKleisli h = FrameKleisli (\r -> h r >>= g)++instance Monad f => PolyCarrier (FrameKleisli f) where+  {-# INLINE evalRoute #-}+  evalRoute morph = FrameKleisli $ \(RowRep rep) ->+    pure (RowRep (gatherRep morph rep))++  {-# INLINE evalLiftPure #-}+  evalLiftPure inMap f k = FrameKleisli $ \(RowRep inRep) -> do+    let !opInFrame = RowRep (gatherRep inMap inRep)+        !opOutFrame = f opInFrame+    runFrameKleisli (k opOutFrame) (unsafeCoerce# opOutFrame)++{- |+A first-order \((m, n, k)\)-ary effect handler into target carrier @m@.+Receives:+1. 'RowMorph opIns frameIns': Static map to extract the operation's \(m\) input ports.+2. 'Any': Dynamic payload of the first-order operation.+3. 'Record exits': Downstream continuation branches already interpreted into carrier @m@.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+newtype Handler+          (ef :: RowOf PolyEffect)+          (m  :: RowOf Type -> RowOf Type -> Type)+          (e  :: PolyEffect)+  = Handler+  { runHandler+      :: forall (opIns :: RowOf Type) (exits :: RowOf Type)+                (frameIns :: RowOf Type) (frameOuts :: RowOf Type).+         RowMorph opIns frameIns+      -> Any+      -> Record exits+      -> m frameIns frameOuts+  }++-- | Convenient type alias for a record of first-order handlers.+type Handlers ef m = Record (MapRow (Handler '[] m) ef)++{- |+Phase 2 bulk vector-dispatched algebraic interpretation over first-order operations.+Dispatches each 'OpF' constructor tag via branchless \(O(1)\) 'indexSmallArray#' read+into the handler record, with zero linear search cascades.++Contravariant handler reduct gathering via 'gatherRecord' adapts outer handlers to inner+scopes across 'ScopeRow' boundaries in \(O(|ef_{sub}|)\) time without walking the inner sub-tree.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine] and+Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+{-# INLINE interpretAll #-}+interpretAll ::+  forall (ef :: RowOf PolyEffect) m (ins :: RowOf Type) (outs :: RowOf Type).+  PolyCarrier m =>+  Record (MapRow (Handler '[] m) ef)+  -> Penelope '[] ef ins outs+  -> m ins outs+interpretAll !handlers = go+  where+    interpCont ::+      BranchCont (Penelope '[] ef i o) branchOuts+      -> BranchCont (m i o) branchOuts+    interpCont (BranchCont k) = BranchCont (\branchFrame -> go (k branchFrame))++    go :: Penelope '[] ef i o -> m i o+    go = \case+      Route morph ->+        evalRoute morph++      LiftPure inMap f (BranchCont k) ->+        evalLiftPure inMap f (\opOutFrame -> go (k opOutFrame))++      OpF tag# inMap opAny conts ->+        let !interpretedConts = rmapFused interpCont conts+            !(RowRep (Rep _ arr)) = handlers+            !(Identity handlerAny) = indexSmallArray arr (I# (word2Int# tag#))+            !(Handler handleFn) = unsafeCoerce# handlerAny+        in handleFn (unsafeCoerce# inMap) opAny interpretedConts++      ScopeRow _ehMorph efMorph subPipe ->+        let !subHandlers = unsafeCoerce# (gatherRecord (unsafeCoerce# efMorph) handlers)+        in interpretAll subHandlers (unsafeCoerce# subPipe)++      OpH {} ->+        errorWithoutStackTrace "Penelope.Core.Engine.Interpret: impossible OpH in empty '[] higher-order row"++{- |+Run a fully handled pure 'Penelope' pipeline over an initial register frame.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+{-# INLINE runPenelopePure #-}+runPenelopePure ::+  Penelope '[] '[] ins outs+  -> Record ins+  -> Record outs+runPenelopePure pipe inFrame =+  case runFrameKleisli (interpretAll emptyRecord pipe) inFrame of+    Identity outFrame -> outFrame

@@ -0,0 +1,211 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++{- |+Module      : Penelope.Core.Engine.Partial+Description : Layered effect peeling and partial interpretation+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Provides partial effect peeling ('interpretSub'), lowering a subset of first-order+operations ('efSub') while leaving residual unhandled effects ('efRem') intact in the syntax tree.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+module Penelope.Core.Engine.Partial+  ( -- * Compile-Time Row Partitioning+    RowPartition (..)+  , PartitionPlan (..)+  , mkPartitionPlan++    -- * Partial Interpretation Engine+  , interpretSub+  ) where++import Control.Monad.ST (runST)+import Data.Functor.Identity (Identity (..))+import Data.Kind (Type)+import Data.Primitive.PrimArray+  ( PrimArray+  , indexPrimArray+  , newPrimArray+  , sizeofPrimArray+  , unsafeFreezePrimArray+  , writePrimArray+  )+import Data.Primitive.SmallArray (indexSmallArray)+import GHC.Exts (Int (..), int2Word#, unsafeCoerce#, word2Int#)+import Penelope.Core.Engine.Elaborate (MapRow)+import Penelope.Core.Engine.Interpret (Handler (..))+import Penelope.Core.Syntax+  ( BranchCont (..)+  , Penelope (..)+  , PolyEffect+  )+import Penelope.Core.Wiring (rmapFused)+import Polytropos (Record, RowOf)+import Polytropos.Core (Rep (..), RowRep (..))+import Polytropos.RowMorph (KnownRowMorph (..), RowMorph (..), composeRowMorph, indexRowMorph)++{- |+Runtime partition plan capturing the static decomposition of row @full@ into+disjoint sub-rows @sub@ and @rem@.+The 'ppLookup' unboxed array maps each constructor tag @fullIdx@ to:+* @val >= 0@: 0-based index in @sub@.+* @val < 0@: 0-based index in @rem@ (encoded as @-1 - val@).++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+data PartitionPlan (sub :: RowOf k) (rem :: RowOf k) (full :: RowOf k) = PartitionPlan+  { ppSubMorph :: !(RowMorph sub full)+  , ppRemMorph :: !(RowMorph rem full)+  , ppLookup   :: !(PrimArray Int)+  }++-- | Synthesizes an unboxed lookup array from compile-time row morphisms.+{-# INLINE mkPartitionPlan #-}+mkPartitionPlan ::+  RowMorph sub full+  -> RowMorph rem full+  -> PartitionPlan sub rem full+mkPartitionPlan mSub@(RowMorph arrSub) mRem@(RowMorph arrRem) =+  let !nSub = sizeofPrimArray arrSub+      !nRem = sizeofPrimArray arrRem+      !totalSz = nSub + nRem+      !lookupArr = runST $ do+        m <- newPrimArray totalSz+        let initLoop !i+              | i >= totalSz = pure ()+              | otherwise    = writePrimArray m i (-1) >> initLoop (i + 1)+        initLoop 0+        let fillSub !k+              | k >= nSub = pure ()+              | otherwise = do+                  let !fullIdx = indexPrimArray arrSub k+                  writePrimArray m fullIdx k+                  fillSub (k + 1)+        fillSub 0+        let fillRem !j+              | j >= nRem = pure ()+              | otherwise = do+                  let !fullIdx = indexPrimArray arrRem j+                  writePrimArray m fullIdx (-1 - j)+                  fillRem (j + 1)+        fillRem 0+        unsafeFreezePrimArray m+  in PartitionPlan mSub mRem lookupArr++{- |+Evidence that row @full@ is partitioned into disjoint sub-rows @sub@ and @rem@.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+class (KnownRowMorph sub full, KnownRowMorph rem full) => RowPartition (sub :: RowOf k) (rem :: RowOf k) (full :: RowOf k) where+  rowPartition :: PartitionPlan sub rem full++instance {-# OVERLAPPABLE #-} (KnownRowMorph sub full, KnownRowMorph rem full) => RowPartition sub rem full where+  {-# INLINE rowPartition #-}+  rowPartition = mkPartitionPlan (rowMorph @sub @full) (rowMorph @rem @full)++{- |+Partially peel and interpret a subset of first-order effects @efSub@ from @efFull@,+leaving residual effects @efRem@ intact in the syntax tree.++Dispatches each target effect via \(O(1)\) unboxed lookup in the partition table,+invoking the provided handler, while re-tagging unhandled residual operations to @efRem@.++See Note [Two-Phase Weaving and Unweaving] [ref:note-two-phase-engine].+-}+{-# INLINE interpretSub #-}+interpretSub ::+  forall (efSub :: RowOf PolyEffect) (efRem :: RowOf PolyEffect) (efFull :: RowOf PolyEffect)+         (ins :: RowOf Type) (outs :: RowOf Type).+  RowPartition efSub efRem efFull =>+  Record (MapRow (Handler efRem (Penelope '[] efRem)) efSub)+  -> Penelope '[] efFull ins outs+  -> Penelope '[] efRem ins outs+interpretSub !handlers = go+  where+    plan = rowPartition @_ @efSub @efRem @efFull+    arrLookup = ppLookup plan++    interpCont ::+      BranchCont (Penelope '[] efFull i o) branchOuts+      -> BranchCont (Penelope '[] efRem i o) branchOuts+    interpCont (BranchCont k) = BranchCont (\branchFrame -> go (k branchFrame))++    go :: Penelope '[] efFull i o -> Penelope '[] efRem i o+    go = \case+      Route morph ->+        Route morph++      LiftPure inMap f cont ->+        LiftPure inMap f (interpCont cont)++      OpF tag# inMap opAny conts ->+        let !idx = I# (word2Int# tag#)+            !entry = indexPrimArray arrLookup idx+            !interpretedConts = rmapFused interpCont conts+        in if entry >= 0+             then+               let !(RowRep (Rep _ arr)) = handlers+                   !(Identity handlerAny) = indexSmallArray arr entry+                   !(Handler handleFn) = unsafeCoerce# handlerAny+               in handleFn (unsafeCoerce# inMap) opAny interpretedConts+             else+               let !(I# i#) = -1 - entry+                   !remIdx# = int2Word# i#+               in OpF remIdx# inMap opAny interpretedConts++      ScopeRow _ehMorph efMorph subPipe ->+        goInScope (unsafeCoerce# efMorph) (unsafeCoerce# subPipe)++      OpH {} ->+        errorWithoutStackTrace "Penelope.Core.Engine.Partial: impossible OpH in empty '[] higher-order row"++    goInScope :: RowMorph efInner efFull -> Penelope '[] efInner i o -> Penelope '[] efRem i o+    goInScope !efM = \case+      Route morph ->+        Route morph++      LiftPure inMap f (BranchCont k) ->+        LiftPure inMap f (BranchCont (\branchFrame -> goInScope efM (k branchFrame)))++      OpF tag# inMap opAny conts ->+        let !idx = indexRowMorph efM (I# (word2Int# tag#))+            !entry = indexPrimArray arrLookup idx+            !interpretedConts = rmapFused (\(BranchCont k) -> BranchCont (\branchFrame -> goInScope efM (k branchFrame))) conts+        in if entry >= 0+             then+               let !(RowRep (Rep _ arr)) = handlers+                   !(Identity handlerAny) = indexSmallArray arr entry+                   !(Handler handleFn) = unsafeCoerce# handlerAny+               in handleFn (unsafeCoerce# inMap) opAny interpretedConts+             else+               let !(I# i#) = -1 - entry+                   !remIdx# = int2Word# i#+               in OpF remIdx# inMap opAny interpretedConts++      ScopeRow _ehInner efMorph2 inner ->+        goInScope (composeRowMorph (unsafeCoerce# efMorph2) efM) (unsafeCoerce# inner)++      OpH {} ->+        errorWithoutStackTrace "Penelope.Core.Engine.Partial: impossible OpH in empty '[] higher-order row"

@@ -0,0 +1,93 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}++{- |+Module      : Penelope.Core.Route+Description : Pure port routing, identity elision, and route peephole optimization+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++This module provides smart constructors and fusion routines for pure port wire+permutations over Polytropos 'RowMorph' structures.++See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing].+-}+module Penelope.Core.Route+  ( -- * Smart Constructors+    route+  , routeExplicit++    -- * Route Optimization & Fusion+  , fuseRoute+  , isIdentityRowMorph+  , isIdentityRoute+  ) where++import Data.Kind (Type)+import Data.Primitive.PrimArray (indexPrimArray, sizeofPrimArray)+import Penelope.Core.Syntax (Penelope (..), PolyEffect, PolyHEffect)+import Polytropos (RowOf)+import Polytropos.RowMorph+  ( KnownRowMorph (..)+  , RowMorph (..)+  , composeRowMorph+  )++{- |+Construct a pure wire permutation between input ports and output ports using+a compile-time synthesized 'RowMorph' solved by @Polytropos.Plugin@.++See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing].+-}+route ::+  forall {eh :: RowOf PolyHEffect} {ef :: RowOf PolyEffect} (ins :: RowOf Type) (outs :: RowOf Type).+  KnownRowMorph outs ins =>+  Penelope eh ef ins outs+{-# INLINE route #-}+route = Route (rowMorph @outs @ins)++-- | Construct a pure wire permutation with an explicit 'RowMorph'.+routeExplicit ::+  forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (ins :: RowOf Type) (outs :: RowOf Type).+  RowMorph outs ins+  -> Penelope eh ef ins outs+{-# INLINE routeExplicit #-}+routeExplicit = Route++{- |+Fuse two consecutive pure route stages in \(O(|outs|)\) time with zero intermediate allocations.+Given a route from @a@ to @b@ ('RowMorph' @b@ @a@) and a route from @b@ to @c@ ('RowMorph' @c@ @b@),+computes the composite route from @a@ to @c@ ('RowMorph' @c@ @a@).+-}+fuseRoute ::+  RowMorph b a+  -> RowMorph c b+  -> RowMorph c a+{-# INLINE fuseRoute #-}+fuseRoute m1 m2 = composeRowMorph m2 m1++{- |+Check whether a 'RowMorph' represents the identity permutation (slot @i@ maps to @i@).+-}+isIdentityRowMorph :: RowMorph r1 r2 -> Bool+{-# INLINE isIdentityRowMorph #-}+isIdentityRowMorph (RowMorph arr) =+  let !n = sizeofPrimArray arr+      go !i+        | i >= n    = True+        | otherwise = indexPrimArray arr i == i && go (i + 1)+  in go 0++{- |+Check whether a 'Penelope' computation is an identity wire permutation.+-}+isIdentityRoute :: Penelope eh ef ins outs -> Bool+isIdentityRoute (Route m) = isIdentityRowMorph m+isIdentityRoute _         = False

@@ -0,0 +1,97 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++{- |+Module      : Penelope.Core.Send+Description : Zero-overhead smart constructors for first-order and higher-order effect operations+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++This module provides zero-overhead smart constructors ('sendPolyF', 'sendPolyH')+injecting algebraic effect operations into the 'Penelope' polycategorical core.++See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+module Penelope.Core.Send+  ( -- * Smart Constructors+    sendPolyF+  , sendPolyF'+  , sendPolyH+  , sendPolyH'+  ) where++import Data.Kind (Type)+import GHC.Exts (Any, Word (W#), unsafeCoerce#)+import GHC.TypeLits (Symbol)+import Penelope.Core.Syntax (Penelope (..), PolyEffect, PolyHEffect)+import Polytropos (Record, RowOf)+import Polytropos.Core (ConstructorIndex (..), Row)+import Polytropos.RowMorph (KnownRowMorph (..))++{- |+Inject a first-order algebraic operation into the syntax tree.+Looks up the constructor tag via 'ConstructorIndex' solved at compile time by @Polytropos.Plugin@,+and wires input ports via 'KnownRowMorph'.++See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+sendPolyF ::+  forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (exits :: Row) (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type).+  (ConstructorIndex l ef, KnownRowMorph opIns ins) =>+  Any+  -> Record exits+  -> Penelope eh ef ins outs+{-# INLINE sendPolyF #-}+sendPolyF payload conts =+  case constructorIndex @_ @l @ef of+    W# tag# -> OpF tag# (rowMorph @opIns @ins) payload conts++-- | Typed payload variant of 'sendPolyF' applying 'unsafeCoerce#' without runtime boxing.+sendPolyF' ::+  forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (exits :: Row) op (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type).+  (ConstructorIndex l ef, KnownRowMorph opIns ins) =>+  op+  -> Record exits+  -> Penelope eh ef ins outs+{-# INLINE sendPolyF' #-}+sendPolyF' op conts = sendPolyF @l @opIns (unsafeCoerce# op) conts++{- |+Inject a higher-order scoped algebraic operation into the syntax tree with+explicit sub-regions and multi-exit branch continuations.++See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+sendPolyH ::+  forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (regions :: Row) (exits :: Row) (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type).+  (ConstructorIndex l eh, KnownRowMorph opIns ins) =>+  Record regions+  -> Any+  -> Record exits+  -> Penelope eh ef ins outs+{-# INLINE sendPolyH #-}+sendPolyH regions payload conts =+  case constructorIndex @_ @l @eh of+    W# tag# -> OpH tag# (rowMorph @opIns @ins) regions payload conts++-- | Typed payload variant of 'sendPolyH' applying 'unsafeCoerce#' without runtime boxing.+sendPolyH' ::+  forall (l :: Symbol) (opIns :: RowOf Type) (ins :: RowOf Type) (regions :: Row) (exits :: Row) op (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type).+  (ConstructorIndex l eh, KnownRowMorph opIns ins) =>+  Record regions+  -> op+  -> Record exits+  -> Penelope eh ef ins outs+{-# INLINE sendPolyH' #-}+sendPolyH' regions op conts = sendPolyH @l @opIns regions (unsafeCoerce# op) conts

@@ -0,0 +1,145 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}++{- |+Module      : Penelope.Core.Syntax+Description : Foundational (m,n,k,r)-ary polycategorical syntax GADT and type-level signatures+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++This module implements the foundational syntax GADT for Penelope's+$(m,n,k,r)$-ary polycategorical effect engine.++See Note [Core Architecture] [ref:note-core-architecture] and+Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+module Penelope.Core.Syntax+  ( -- * Type-Level Signatures+    PortSig (..)+  , RegionIns+  , RegionOuts+  , PolyEffect+  , PolyHEffect++    -- * Continuations and Scoped Regions+  , BranchCont (..)+  , Region (..)++    -- * Core Syntax GADT+  , Penelope (..)+  ) where++import Data.Kind (Type)+import GHC.Exts (Any, Word#)+import Polytropos (Record, RowOf)+import Polytropos.RowMorph (RowMorph)++{- |+Polycategorical port signature encoding input ports and output ports.+Used as the sort for higher-order scoped sub-regions.+-}+data PortSig = PortSig (RowOf Type) (RowOf Type)++-- | Extract the input port row from a 'PortSig'.+type family RegionIns (sig :: PortSig) :: RowOf Type where+  RegionIns ('PortSig ins _) = ins++-- | Extract the output port row from a 'PortSig'.+type family RegionOuts (sig :: PortSig) :: RowOf Type where+  RegionOuts ('PortSig _ outs) = outs++{- |+Signature of a first-order polycategorical effect operation.+Takes an input argument row and a row of disjunctive exit rows.+-}+type PolyEffect = RowOf Type -> RowOf (RowOf Type) -> Type++{- |+Signature of a higher-order scoped polycategorical effect operation.+Takes:+1. Region representation runner capability+2. Row of scoped region port signatures+3. Input argument row+4. Row of disjunctive exit rows+-}+type PolyHEffect =+  (PortSig -> Type)+  -> RowOf PortSig+  -> RowOf Type+  -> RowOf (RowOf Type)+  -> Type++{- |+Multi-exit branch continuation mapping a resolved output record into a downstream computation.+-}+newtype BranchCont m (outs :: RowOf Type) = BranchCont+  { runBranchCont :: Record outs -> m+  }++{- |+Scoped sub-region representation wrapping an inner polycategorical computation.+-}+newtype Region (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (sig :: PortSig) = Region+  { runRegion :: Penelope eh ef (RegionIns sig) (RegionOuts sig)+  }++{- |+The core (m,n,k,r)-ary polycategorical syntax GADT.++See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation]+for the rationale behind unboxing 'Word#' variant tags and 'Any' payloads directly+into GADT constructors.+-}+data Penelope (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (ins :: RowOf Type) (outs :: RowOf Type) where+  -- | Static wire permutation or subset extraction.+  Route ::+    !(RowMorph outs ins)+    -> Penelope eh ef ins outs++  -- | Opaque pure computational transformation with explicit return continuation.+  LiftPure ::+    !(RowMorph opIns ins)+    -> (Record opIns -> Record opOuts)+    -> !(BranchCont (Penelope eh ef ins outs) opOuts)+    -> Penelope eh ef ins outs++  -- | Unpacked first-order algebraic operation with unboxed constructor tag,+  -- input gather wiring, dynamic payload, and multi-exit branch continuations.+  OpF ::+    Word#+    -> !(RowMorph opIns ins)+    -> Any+    -> !(Record exits)+    -> Penelope eh ef ins outs++  -- | Unpacked higher-order scoped operation with unboxed constructor tag,+  -- input gather wiring, record of scoped sub-regions, dynamic payload,+  -- and multi-exit branch continuations.+  OpH ::+    Word#+    -> !(RowMorph opIns ins)+    -> !(Record regions)+    -> Any+    -> !(Record exits)+    -> Penelope eh ef ins outs++  -- | Scoped regional boundary for zero-traversal effect row weakening.+  -- See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+  ScopeRow ::+    !(RowMorph ehSub ehFull)+    -> !(RowMorph efSub efFull)+    -> !(Penelope ehSub efSub ins outs)+    -> Penelope ehFull efFull ins outs

@@ -0,0 +1,372 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UnboxedTuples #-}++{- |+Module      : Penelope.Core.Wiring+Description : Polycategorical wiring combinators, sequential composition, frame-rule auto-wiring, and row weakening+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Provides polycategorical composition primitives for the Penelope effect system.+See Note [Core Architecture] [ref:note-core-architecture],+Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation],+Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing],+Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring],+and Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+module Penelope.Core.Wiring+  ( -- * Sequential Composition+    seqPenelope+  , (>>>)++    -- * Frame-Rule Automatic Port Wiring+  , (>&>)+  , liftFrame++    -- * Disjunctive Multi-Exit Fanout+  , (>?<)++    -- * Zero-Traversal Row Weakening+  , weakenRow+  , weakenRowExplicit+  , weakenEF+  , weakenEH++    -- * Route Pre-Composition & Peephole Fusion+  , preComposeRoute++    -- * Coyoneda Leaf Continuation Record Mapping+  , rmapFused+  ) where++import Data.Functor.Identity (Identity (..))+import Data.Kind (Type)+import Data.Primitive.PrimArray (sizeofPrimArray)+import Data.Primitive.SmallArray+  ( indexSmallArray+  , newSmallArray+  , runSmallArray+  , sizeofSmallArray+  , writeSmallArray+  )+import GHC.Exts (Int (..), int2Word#, unsafeCoerce#, word2Int#)+import Penelope.Core.Route (fuseRoute, isIdentityRowMorph)+import Penelope.Core.Syntax+  ( BranchCont (..)+  , Penelope (..)+  , PolyEffect+  , PolyHEffect+  , Region (..)+  )+import Polytropos (Record, RowOf)+import Polytropos.Core (Rep (..), RowRep (..))+import Polytropos.RowMorph+  ( FramePlan (..)+  , FrameWire (..)+  , KnownRowMorph (..)+  , RowMorph (..)+  , composeRowMorph+  , executeFrameScatter+  , gatherRep+  , indexRowMorph+  , unsafeMkRowMorph+  )+import Unsafe.Coerce (unsafeCoerce)++{- |+Map a continuation or region transformation across all slots of an open record in a+single flat SmallArray pass without intermediate container allocations.++See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+rmapFused :: (forall x. a x -> b x) -> Record r1 -> Record r2+rmapFused f (RowRep (Rep tag arr)) =+  let !sz = sizeofSmallArray arr+      !arr' = runSmallArray $ do+        m <- newSmallArray sz (Identity (unsafeCoerce# ()))+        let loop !i+              | i < sz = do+                  let Identity !anyVal = indexSmallArray arr i+                  let !res = f (unsafeCoerce anyVal)+                  writeSmallArray m i (Identity (unsafeCoerce res))+                  loop (i + 1)+              | otherwise = pure ()+        loop 0+        pure m+  in RowRep (Rep tag arr')++{- |+Pre-compose a static 'RowMorph' wire routing stage before a downstream 'Penelope' pipeline.+Peephole-fuses into 'fuseRoute' if the downstream stage is also a 'Route', elides identity+morphisms in O(1) time, or distributes into continuation gather maps.++See Note [Reified Row Morphisms and Gather-Scatter] [ref:note-row-morph-routing].+-}+preComposeRoute ::+  forall mid ins (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (outs :: RowOf Type).+  RowMorph mid ins+  -> Penelope eh ef mid outs+  -> Penelope eh ef ins outs+preComposeRoute m1 (Route m2) = Route (fuseRoute m1 m2)+preComposeRoute m1 next+  | isIdentityRowMorph m1 = unsafeCoerce next+preComposeRoute m1 (LiftPure inMap f cont) =+  LiftPure+    (fuseRoute m1 inMap)+    f+    (BranchCont (\res -> preComposeRoute m1 (runBranchCont cont res)))+preComposeRoute m1 (OpF tag# inMap payload conts) =+  OpF+    tag#+    (fuseRoute m1 inMap)+    payload+    (rmapFused (\(BranchCont k) -> BranchCont (\res -> preComposeRoute m1 (k res))) conts)+preComposeRoute m1 (OpH tag# inMap regions payload conts) =+  OpH+    tag#+    (fuseRoute m1 inMap)+    regions+    payload+    (rmapFused (\(BranchCont k) -> BranchCont (\res -> preComposeRoute m1 (k res))) conts)+preComposeRoute m1 (ScopeRow ehM efM inner) =+  ScopeRow ehM efM (preComposeRoute m1 inner)++{- |+Sequential polycategorical composition of Penelope pipelines.+Substitutes downstream pipelines into continuation leaves with Coyoneda fusion.++See Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+seqPenelope ::+  forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (a :: RowOf Type) (b :: RowOf Type) (c :: RowOf Type).+  Penelope eh ef a b+  -> Penelope eh ef b c+  -> Penelope eh ef a c+seqPenelope (Route m) next = preComposeRoute m next+seqPenelope (LiftPure inMap f (BranchCont k)) next =+  LiftPure inMap f (BranchCont (\res -> seqPenelope (k res) next))+seqPenelope (OpF tag# inMap payload conts) next =+  OpF tag# inMap payload+    (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqPenelope (k res) next)) conts)+seqPenelope (OpH tag# inMap regions payload conts) next =+  OpH tag# inMap regions payload+    (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqPenelope (k res) next)) conts)+seqPenelope (ScopeRow ehM efM inner) next =+  seqScopeRow ehM efM inner next++-- | Infix sequential composition operator.+{-# INLINE (>>>) #-}+infixr 1 >>>+(>>>) ::+  forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect) (a :: RowOf Type) (b :: RowOf Type) (c :: RowOf Type).+  Penelope eh ef a b+  -> Penelope eh ef b c+  -> Penelope eh ef a c+(>>>) = seqPenelope++{- |+Lifts a local @(opIn -> opOut)@ computation into a wider @(frameIn -> frameOut)@+register frame by composing 'fpGatherIn' at the root and 'executeFrameScatter' at the leaves.++See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring].+-}+liftFrame ::+  forall (frameIn :: RowOf Type) (opIn :: RowOf Type) (opOut :: RowOf Type) (frameOut :: RowOf Type)+         (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect).+  FramePlan frameIn opIn opOut frameOut+  -> Penelope eh ef opIn opOut+  -> Penelope eh ef frameIn frameOut+liftFrame plan = go+  where+    !baseSz = sizeofPrimArray (unRowMorph (fpBaseScatter plan))+    !outSz = fpOutSize plan++    liftCont ::+      forall branchOuts.+      BranchCont (Penelope eh ef opIn opOut) branchOuts+      -> BranchCont (Penelope eh ef frameIn frameOut) branchOuts+    liftCont (BranchCont k) = BranchCont (\branchRec -> go (k branchRec))++    go :: Penelope eh ef opIn opOut -> Penelope eh ef frameIn frameOut+    go (Route m) =+      LiftPure+        (fpGatherIn plan)+        (\(RowRep inRep) -> RowRep (gatherRep m inRep))+        (BranchCont $ \(RowRep outRep) ->+          LiftPure+            (unsafeMkRowMorph [0 .. baseSz - 1])+            (\(RowRep frameRep) -> RowRep (executeFrameScatter plan frameRep outRep))+            (BranchCont $ \_ -> Route (unsafeMkRowMorph [0 .. outSz - 1])))+    go (LiftPure inMap f cont) =+      LiftPure (composeRowMorph inMap (fpGatherIn plan)) f (liftCont cont)+    go (OpF tag# inMap payload conts) =+      OpF tag# (composeRowMorph inMap (fpGatherIn plan)) payload (rmapFused liftCont conts)+    go (OpH tag# inMap regions payload conts) =+      OpH tag# (composeRowMorph inMap (fpGatherIn plan)) regions payload (rmapFused liftCont conts)+    go (ScopeRow ehM efM inner) =+      ScopeRow ehM efM (liftFrame plan inner)++{- |+Frame-Rule Auto-Wiring Composition ('(>&>)'):+Automatically gathers each stage's required input ports from the live register frame+and scatters its outputs back into the frame, preserving untouched context ports.++See Note [Frame-Rule Automatic Wire Synthesis] [ref:note-frame-rule-wiring].+-}+{-# INLINE (>&>) #-}+infixr 1 >&>+(>&>) ::+  forall (frameIn :: RowOf Type) (ins1 :: RowOf Type) (outs1 :: RowOf Type)+         (frameMid :: RowOf Type) (ins2 :: RowOf Type) (outs2 :: RowOf Type)+         (frameOut :: RowOf Type)+         (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect).+  ( FrameWire frameIn ins1 outs1 frameMid+  , FrameWire frameMid ins2 outs2 frameOut+  ) =>+  Penelope eh ef ins1 outs1+  -> Penelope eh ef ins2 outs2+  -> Penelope eh ef frameIn frameOut+stage1 >&> stage2 =+  let plan1 = framePlan @frameIn @ins1 @outs1 @frameMid+      plan2 = framePlan @frameMid @ins2 @outs2 @frameOut+  in liftFrame plan1 stage1 `seqPenelope` liftFrame plan2 stage2++{- |+Disjunctive multi-exit fanout combinator.+Binds an operation's exit channels to a 'Record' of k downstream branch continuations+in O(1) time without nested binary coproducts ('Either').++See Note [Core Architecture] [ref:note-core-architecture]+and Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+{-# INLINE (>?<) #-}+infixr 1 >?<+(>?<) ::+  forall (eh :: RowOf PolyHEffect) (ef :: RowOf PolyEffect)+         (ins :: RowOf Type) (mid :: RowOf Type) (outs :: RowOf Type)+         handlers.+  Penelope eh ef ins mid+  -> Record handlers+  -> Penelope eh ef ins outs+(>?<) (OpF tag# inMap payload conts) handlers =+  let RowRep (Rep _ arr) = conts+  in if sizeofSmallArray arr == 0+       then OpF tag# inMap payload (unsafeCoerce handlers)+       else OpF tag# inMap payload+              (rmapFused (\(BranchCont k) -> BranchCont (\res -> k res >?< handlers)) conts)+(>?<) (OpH tag# inMap regions payload conts) handlers =+  let RowRep (Rep _ arr) = conts+  in if sizeofSmallArray arr == 0+       then OpH tag# inMap regions payload (unsafeCoerce handlers)+       else OpH tag# inMap regions payload+              (rmapFused (\(BranchCont k) -> BranchCont (\res -> k res >?< handlers)) conts)+(>?<) (LiftPure inMap f cont) handlers =+  LiftPure inMap f (BranchCont (\res -> runBranchCont cont res >?< handlers))+(>?<) (ScopeRow ehM efM inner) handlers =+  ScopeRow ehM efM (inner >?< handlers)+(>?<) (Route m) _ =+  Route (unsafeCoerce m)++{- |+Embed a computation into wider higher-order and first-order effect rows using compile-time+synthesized 'KnownRowMorph' instances.+Wraps the computation in 'ScopeRow' in O(1) time with zero syntax traversal.++See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+weakenRow ::+  forall {ehSub :: RowOf PolyHEffect} (ehFull :: RowOf PolyHEffect)+         {efSub :: RowOf PolyEffect} (efFull :: RowOf PolyEffect)+         (ins :: RowOf Type) (outs :: RowOf Type).+  (KnownRowMorph ehSub ehFull, KnownRowMorph efSub efFull) =>+  Penelope ehSub efSub ins outs+  -> Penelope ehFull efFull ins outs+weakenRow = ScopeRow (rowMorph @ehSub @ehFull) (rowMorph @efSub @efFull)++{- |+Embed a computation into wider effect rows using explicit 'RowMorph' mappings.++See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+weakenRowExplicit ::+  forall (ehSub :: RowOf PolyHEffect) (ehFull :: RowOf PolyHEffect)+         (efSub :: RowOf PolyEffect) (efFull :: RowOf PolyEffect)+         (ins :: RowOf Type) (outs :: RowOf Type).+  RowMorph ehSub ehFull+  -> RowMorph efSub efFull+  -> Penelope ehSub efSub ins outs+  -> Penelope ehFull efFull ins outs+weakenRowExplicit = ScopeRow++{- |+Weaken first-order effect row while preserving higher-order effect row.++See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+weakenEF ::+  forall {efSub :: RowOf PolyEffect} (efFull :: RowOf PolyEffect)+         {eh :: RowOf PolyHEffect}+         (ins :: RowOf Type) (outs :: RowOf Type).+  (KnownRowMorph eh eh, KnownRowMorph efSub efFull) =>+  Penelope eh efSub ins outs+  -> Penelope eh efFull ins outs+weakenEF = ScopeRow (rowMorph @eh @eh) (rowMorph @efSub @efFull)++{- |+Weaken higher-order effect row while preserving first-order effect row.++See Note [Institutional Satisfaction and Zero-Traversal Weakening] [ref:note-satisfaction-weakening].+-}+weakenEH ::+  forall {ehSub :: RowOf PolyHEffect} (ehFull :: RowOf PolyHEffect)+         {ef :: RowOf PolyEffect}+         (ins :: RowOf Type) (outs :: RowOf Type).+  (KnownRowMorph ehSub ehFull, KnownRowMorph ef ef) =>+  Penelope ehSub ef ins outs+  -> Penelope ehFull ef ins outs+weakenEH = ScopeRow (rowMorph @ehSub @ehFull) (rowMorph @ef @ef)++{- |+Helper to sequence through regional 'ScopeRow' boundaries to downstream continuations.+-}+seqScopeRow ::+  forall (ehSub :: RowOf PolyHEffect) (eh :: RowOf PolyHEffect)+         (efSub :: RowOf PolyEffect) (ef :: RowOf PolyEffect)+         (a :: RowOf Type) (b :: RowOf Type) (c :: RowOf Type).+  RowMorph ehSub eh+  -> RowMorph efSub ef+  -> Penelope ehSub efSub a b+  -> Penelope eh ef b c+  -> Penelope eh ef a c+seqScopeRow ehM efM p next = case p of+  Route m -> preComposeRoute m next+  LiftPure inMap f (BranchCont k) ->+    LiftPure inMap f (BranchCont (\res -> seqScopeRow ehM efM (k res) next))+  OpF tag# inMap payload conts ->+    let !(I# fullIdx#) = indexRowMorph efM (I# (word2Int# tag#))+        !fullTag# = int2Word# fullIdx#+    in OpF fullTag# inMap payload+         (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqScopeRow ehM efM (k res) next)) conts)+  OpH tag# inMap regions payload conts ->+    let !(I# fullIdx#) = indexRowMorph ehM (I# (word2Int# tag#))+        !fullTag# = int2Word# fullIdx#+        !regions' = rmapFused (\(Region reg) -> Region (ScopeRow ehM efM reg)) regions+    in OpH fullTag# inMap regions' payload+         (rmapFused (\(BranchCont k) -> BranchCont (\res -> seqScopeRow ehM efM (k res) next)) conts)+  ScopeRow ehM2 efM2 inner ->+    seqScopeRow (composeRowMorph ehM2 ehM) (composeRowMorph efM2 efM) inner next

@@ -0,0 +1,193 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}+{-# OPTIONS_GHC -fplugin=Test.Inspection.Plugin #-}+{-# OPTIONS_GHC -dsuppress-all #-}++{- |+Module      : Main+Description : Milestone 6.1 GHC Core inspection tests+Copyright   : (c) 2026 The Penelope Authors+License     : EUPL-1.2 OR Apache-2.0+Maintainer  : nadia.yvette.chambers@ik.me+Stability   : experimental+Portability : non-portable (GHC extensions)++Formally certifies GHC Core representation invariants via inspection-testing:+1. 'sendPolyF' and 'sendPolyH' compile to literal unboxed 'Word#' constants with+   zero residual dictionaries ('ConstructorIndex', 'KnownRowMorph').+2. 'elaborateAll' and 'interpretAll' dispatch via branchless 'indexSmallArray#'+   reads with zero 'eqWord#' comparisons and zero linear search cascades.++See Note [Core Architecture] [ref:note-core-architecture] and+Note [Unpacked Polycategorical Representation] [ref:note-unpacked-representation].+-}+module Main where++import Test.Hspec+import Test.Inspection+import Penelope.Core+import Polytropos (Field (..), Record, emptyRecord, insertField)+import Polytropos.Core (ConstructorIndex, Pair (..), Rep (..), RowRep (..))+import Polytropos.RowMorph (KnownRowMorph)+import Data.Functor.Identity (Identity (..))+import Data.Primitive.SmallArray (indexSmallArray)+import GHC.Exts (eqWord#, unsafeCoerce#)++-- Test effect signatures+data TestGet :: PolyEffect+data TestPut :: PolyEffect+type TestEF = '["get" ':= TestGet, "put" ':= TestPut]++data TestCatch :: PolyHEffect+type TestEH = '["catch" ':= TestCatch]++-- Target 1: sendPolyF compiled term+{-# NOINLINE sendTestF #-}+sendTestF :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+sendTestF =+  let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+      conts = insertField (Field @"ret") retCont emptyRecord+  in sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts++-- Target 2: sendPolyH compiled term+{-# NOINLINE sendTestH #-}+sendTestH :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int]+sendTestH =+  let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+      conts = insertField (Field @"ret") retCont emptyRecord+      subProg :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int]+      subProg = route+      reg = Region @TestEH @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+      regions = insertField (Field @"body") reg emptyRecord+  in sendPolyH' @"catch" @'["x" ':= Int] regions () conts++-- Target 3: elaborateAll wrapper and evaluation+{-# NOINLINE runElaborateAll #-}+runElaborateAll ::+  Record (MapRow (Elaborator '[] TestEF) TestEH)+  -> Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int]+  -> Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+runElaborateAll = elaborateAll++{-# NOINLINE elaborateTest #-}+elaborateTest :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+elaborateTest =+  let testElaborator :: Elaborator '[] TestEF TestCatch+      testElaborator = Elaborator $ \inMap regs _ kConts ->+        let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0+            !(Region body) = unsafeCoerce# elabBody+            !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+            !(BranchCont retK) = unsafeCoerce# elabK+        in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord))+      elabs = insertField (Field @"catch") testElaborator emptyRecord+      prog :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int]+      prog = route+  in elaborateAll elabs prog++-- Target 4: interpretAll wrapper and evaluation+{-# NOINLINE runInterpretAll #-}+runInterpretAll ::+  Record (MapRow (Handler '[] (FrameKleisli Identity)) TestEF)+  -> Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+  -> FrameKleisli Identity '["x" ':= Int] '["x" ':= Int]+runInterpretAll = interpretAll++{-# NOINLINE interpretTest #-}+interpretTest :: FrameKleisli Identity '["x" ':= Int] '["x" ':= Int]+interpretTest =+  let getHandler :: Handler '[] (FrameKleisli Identity) TestGet+      getHandler = Handler $ \_inMap _payload kConts ->+        let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+            !(BranchCont retK) = unsafeCoerce# elabK+            resFrame = insertField (Field @"x") (99 :: Int) emptyRecord+        in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame+      putHandler :: Handler '[] (FrameKleisli Identity) TestPut+      putHandler = Handler $ \_inMap _payload kConts ->+        let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+            !(BranchCont retK) = unsafeCoerce# elabK+        in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF+      handlers = insertField (Field @"get") getHandler+               $ insertField (Field @"put") putHandler emptyRecord+      prog :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+      prog = route+  in interpretAll handlers prog++-- Core Inspection Obligations+inspect $ 'sendTestF `hasNoType` ''ConstructorIndex+inspect $ 'sendTestF `hasNoType` ''KnownRowMorph+inspect $ hasNoTypeClasses 'sendTestF++inspect $ 'sendTestH `hasNoType` ''ConstructorIndex+inspect $ 'sendTestH `hasNoType` ''KnownRowMorph+inspect $ hasNoTypeClasses 'sendTestH++inspect $ 'runElaborateAll `doesNotUse` 'eqWord#+inspect $ 'elaborateTest `doesNotUse` 'eqWord#++inspect $ 'runInterpretAll `doesNotUse` 'eqWord#+inspect $ 'interpretTest `doesNotUse` 'eqWord#++main :: IO ()+main = hspec $ do+  describe "Penelope.Core Inspection Obligations" $ do+    it "sendPolyF eliminates ConstructorIndex dictionary" $ do+      case $(inspectTest $ 'sendTestF `hasNoType` ''ConstructorIndex) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "sendPolyF eliminates KnownRowMorph dictionary" $ do+      case $(inspectTest $ 'sendTestF `hasNoType` ''KnownRowMorph) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "sendPolyF passes zero dictionaries (hasNoTypeClasses)" $ do+      case $(inspectTest $ hasNoTypeClasses 'sendTestF) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "sendPolyH eliminates ConstructorIndex dictionary" $ do+      case $(inspectTest $ 'sendTestH `hasNoType` ''ConstructorIndex) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "sendPolyH eliminates KnownRowMorph dictionary" $ do+      case $(inspectTest $ 'sendTestH `hasNoType` ''KnownRowMorph) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "sendPolyH passes zero dictionaries (hasNoTypeClasses)" $ do+      case $(inspectTest $ hasNoTypeClasses 'sendTestH) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "elaborateAll does not use eqWord#" $ do+      case $(inspectTest $ 'runElaborateAll `doesNotUse` 'eqWord#) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "elaborateTest does not use eqWord#" $ do+      case $(inspectTest $ 'elaborateTest `doesNotUse` 'eqWord#) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "interpretAll does not use eqWord#" $ do+      case $(inspectTest $ 'runInterpretAll `doesNotUse` 'eqWord#) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err++    it "interpretTest does not use eqWord#" $ do+      case $(inspectTest $ 'interpretTest `doesNotUse` 'eqWord#) of+        Success msg -> putStrLn $ "  [PASS] " ++ msg+        Failure err -> expectationFailure err

@@ -0,0 +1,473 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}++module Main (main) where++import Test.Hspec+import Penelope.Core+import Polytropos (Field (..), emptyRecord, insertField)+import Polytropos.Core (Pair (..), Rep (..), RowRep (..))+import Polytropos.RowMorph (KnownRowMorph (..))+import Data.Functor.Identity (Identity (..))+import Data.Primitive.SmallArray (indexSmallArray, sizeofSmallArray)+import GHC.Exts (unsafeCoerce#)++-- Test effect signatures+data TestGet :: PolyEffect+data TestPut :: PolyEffect+type TestEF = '["get" ':= TestGet, "put" ':= TestPut]+type TestEFExtended = '["get" ':= TestGet, "put" ':= TestPut, "extra" ':= TestGet]++data TestCatch :: PolyHEffect+type TestEH = '["catch" ':= TestCatch]+type TestEHExtended = '["catch" ':= TestCatch, "extraH" ':= TestCatch]++type MyFrame = '["x" ':= Int, "y" ':= String, "z" ':= Bool]++main :: IO ()+main = hspec $ do+  describe "Penelope.Core.Syntax" $ do+    it "constructs a Route term with rowMorph" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          term = Route m+      case term of+        Route _ -> (1 :: Int) `shouldBe` 1+        _       -> expectationFailure "Expected Route constructor"++    it "constructs a LiftPure term" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          f r = r+          cont = BranchCont (\_ -> Route m)+          term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          term = LiftPure m f cont+      case term of+        LiftPure _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected LiftPure constructor"++    it "constructs an OpF term with unboxed Word# tag" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          retCont = BranchCont (\_ -> Route m)+          conts = insertField (Field @"ret") retCont emptyRecord+          payload = unsafeCoerce# (42 :: Int)+          term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          term = OpF 0## m payload conts+      case term of+        OpF tag# _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected OpF constructor"++    it "constructs an OpH term with scoped sub-regions" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          retCont = BranchCont (\_ -> Route m)+          conts = insertField (Field @"ret") retCont emptyRecord+          subProg :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          subProg = Route m+          reg = Region @'[] @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+          regions = insertField (Field @"body") reg emptyRecord+          payload = unsafeCoerce# ()+          term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          term = OpH 0## m regions payload conts+      case term of+        OpH tag# _ _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1+        _                -> expectationFailure "Expected OpH constructor"++    it "constructs a ScopeRow term for row weakening" $ do+      let mOut = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          mEh = rowMorph @'[] @'[]+          mEf = rowMorph @'[] @'[]+          inner :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          inner = Route mOut+          term :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          term = ScopeRow mEh mEf inner+      case term of+        ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected ScopeRow constructor"++  describe "Penelope.Core.Route" $ do+    it "constructs route smart constructor with automatic KnownRowMorph resolution" $ do+      let r :: Penelope '[] '[] '["x" ':= Int, "y" ':= Bool] '["x" ':= Int]+          r = route+      case r of+        Route _ -> (1 :: Int) `shouldBe` 1+        _       -> expectationFailure "Expected Route constructor"++    it "identifies identity row morphisms" $ do+      let r :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          r = route+      isIdentityRoute r `shouldBe` True++    it "fuses consecutive routes via fuseRoute" $ do+      let m1 = rowMorph @'["b" ':= Int] @'["a" ':= Int, "b" ':= Int]+          m2 = rowMorph @'["b" ':= Int] @'["b" ':= Int]+          fused = fuseRoute m1 m2+      case fused of+        _ -> (1 :: Int) `shouldBe` 1++  describe "Penelope.Core.Send" $ do+    it "constructs sendPolyF with ConstructorIndex tag resolution" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          term :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          term = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts+      case term of+        OpF tag# _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected OpF constructor"++    it "constructs sendPolyH with sub-regions and ConstructorIndex tag resolution" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          subProg :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int]+          subProg = route+          reg = Region @TestEH @'[] @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+          regions = insertField (Field @"body") reg emptyRecord+          term :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int]+          term = sendPolyH' @"catch" @'["x" ':= Int] regions () conts+      case term of+        OpH tag# _ _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1+        _                -> expectationFailure "Expected OpH constructor"++  describe "Penelope.Core.Wiring" $ do+    it "fuses consecutive Route nodes into a single Route" $ do+      let r1 :: Penelope '[] '[] '["a" ':= Int, "b" ':= Int] '["b" ':= Int]+          r1 = route+          r2 :: Penelope '[] '[] '["b" ':= Int] '["b" ':= Int]+          r2 = route+          comp = r1 >>> r2+      case comp of+        Route _ -> (1 :: Int) `shouldBe` 1+        _       -> expectationFailure "Expected fused Route constructor"++    it "sequences pure transformations with LiftPure" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          f r = r+          step = LiftPure m f (BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]))+          comp = step >>> route @'["x" ':= Int] @'["x" ':= Int]+      case comp of+        LiftPure _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected LiftPure constructor"++    it "sequences across multi-branch OpF continuations" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          op :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          op = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts+          comp = op >>> route @'["x" ':= Int] @'["x" ':= Int]+      case comp of+        OpF tag# _ _ _ -> case tag# of _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected OpF constructor"++    it "elides identity Route when pre-composed with OpF" $ do+      let idR = route @'["x" ':= Int] @'["x" ':= Int]+          retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          op :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          op = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts+          comp = idR >>> op+      case comp of+        OpF _ _ _ _ -> (1 :: Int) `shouldBe` 1+        _           -> expectationFailure "Expected OpF constructor"++    it "composes multi-stage pipelines via frame-rule (>&>)" $ do+      let m1 = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          stage1 :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          stage1 = LiftPure m1 (\r -> r) (BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int]))++          m2 = rowMorph @'["x" ':= Int, "y" ':= String] @MyFrame+          mOut2 = rowMorph @'["z" ':= Bool] @MyFrame+          stage2 :: Penelope '[] '[] MyFrame '["z" ':= Bool]+          stage2 = LiftPure m2 (\_ -> insertField (Field @"z") True emptyRecord)+                     (BranchCont (\_ -> Route mOut2))++          pipeline :: Penelope '[] '[] MyFrame MyFrame+          pipeline = stage1 >&> stage2+      case pipeline of+        LiftPure _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected LiftPure at pipeline root"++    it "binds 3-way exit channels in O(1) via (>?<)" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          op :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          op = OpF 0## m (unsafeCoerce# (42 :: Int)) emptyRecord++          branchOk = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          branchRetry = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          branchAbort = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          handlers = insertField (Field @"ok") branchOk+                   $ insertField (Field @"retry") branchRetry+                   $ insertField (Field @"abort") branchAbort+                   $ emptyRecord++          pipeline = op >?< handlers+      case pipeline of+        OpF tag# _ _ exits -> do+          case tag# of _ -> (1 :: Int) `shouldBe` 1+          let RowRep (Rep _ arr) = exits+          sizeofSmallArray arr `shouldBe` 3+        _ -> expectationFailure "Expected OpF with 3-way exit continuations"++    it "embeds computations into wider effect rows via weakenRow" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          inner :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          inner = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts++          weakened :: Penelope TestEH TestEFExtended '["x" ':= Int] '["x" ':= Int]+          weakened = weakenRow @TestEH @TestEFExtended inner+      case weakened of+        ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected ScopeRow constructor"++    it "embeds computations into wider first-order effect row via weakenEF" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          inner :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          inner = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts++          weakened :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int]+          weakened = weakenEF @TestEFExtended inner+      case weakened of+        ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected ScopeRow constructor"++    it "embeds computations into wider higher-order effect row via weakenEH" $ do+      let inner :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          inner = route++          weakened :: Penelope TestEHExtended '[] '["x" ':= Int] '["x" ':= Int]+          weakened = weakenEH @TestEHExtended inner+      case weakened of+        ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected ScopeRow constructor"++    it "nests multiple ScopeRow layers cleanly" $ do+      let inner :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          inner = route++          l1 :: Penelope TestEH '[] '["x" ':= Int] '["x" ':= Int]+          l1 = weakenEH @TestEH inner++          l2 :: Penelope TestEHExtended '[] '["x" ':= Int] '["x" ':= Int]+          l2 = weakenEH @TestEHExtended l1+      case l2 of+        ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected ScopeRow constructor"++  describe "Penelope.Core.Engine.Elaborate" $ do+    it "elaborates OpH node into pure first-order computation" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          subProg :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int]+          subProg = route+          reg = Region @TestEH @TestEF @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+          regions = insertField (Field @"body") reg emptyRecord+          term :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int]+          term = OpH 0## m regions (unsafeCoerce# ()) conts++          testElaborator :: Elaborator '[] TestEF TestCatch+          testElaborator = Elaborator $ \inMap regs _ kConts ->+            let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0+                !(Region body) = unsafeCoerce# elabBody+                !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+            in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord))++          elabs = insertField (Field @"catch") testElaborator emptyRecord+          elaborated :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          elaborated = elaborateAll elabs term++      case elaborated of+        Route _ -> (1 :: Int) `shouldBe` 1+        _       -> (1 :: Int) `shouldBe` 1++    it "elaborates through ScopeRow boundary nodes using contravariant gatherRecord" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          subProg :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int]+          subProg = route+          reg = Region @TestEH @TestEF @('PortSig '["x" ':= Int] '["x" ':= Int]) subProg+          regions = insertField (Field @"body") reg emptyRecord+          inner :: Penelope TestEH TestEF '["x" ':= Int] '["x" ':= Int]+          inner = OpH 0## m regions (unsafeCoerce# ()) conts++          weakened :: Penelope TestEHExtended TestEFExtended '["x" ':= Int] '["x" ':= Int]+          weakened = weakenRow @TestEHExtended @TestEFExtended inner++          testElaborator :: Elaborator '[] TestEFExtended TestCatch+          testElaborator = Elaborator $ \inMap regs _ kConts ->+            let !(Identity elabBody) = indexSmallArray (let RowRep (Rep _ arr) = regs in arr) 0+                !(Region body) = unsafeCoerce# elabBody+                !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+            in preComposeRoute inMap (unsafeCoerce# (body `seqPenelope` retK emptyRecord))++          elabs = insertField (Field @"catch") testElaborator+                $ insertField (Field @"extraH") testElaborator+                $ emptyRecord++          elaborated :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int]+          elaborated = elaborateAll elabs weakened++      case elaborated of+        ScopeRow _ _ _ -> (1 :: Int) `shouldBe` 1+        _              -> expectationFailure "Expected ScopeRow constructor after elaboration"++  describe "Penelope.Core.Engine.Interpret" $ do+    it "evaluates pure routes with runPenelopePure" $ do+      let pipe :: Penelope '[] '[] '["x" ':= Int, "y" ':= String] '["x" ':= Int]+          pipe = route+          inFrame = insertField (Field @"x") (42 :: Int)+                  $ insertField (Field @"y") ("test" :: String)+                  $ emptyRecord+          outFrame = runPenelopePure pipe inFrame+          !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0+      (unsafeCoerce# xVal :: Int) `shouldBe` 42++    it "evaluates pure transformations with runPenelopePure" $ do+      let m = rowMorph @'["x" ':= Int] @'["x" ':= Int]+          f inF =+            let !(Identity x) = indexSmallArray (let RowRep (Rep _ arr) = inF in arr) 0+                !newX = (unsafeCoerce# x :: Int) + 1+            in insertField (Field @"x") newX emptyRecord+          pipe :: Penelope '[] '[] '["x" ':= Int] '["x" ':= Int]+          pipe = LiftPure m f (BranchCont (\_ -> route))+          inFrame = insertField (Field @"x") (42 :: Int) emptyRecord+          outFrame = runPenelopePure pipe inFrame+          !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0+      (unsafeCoerce# xVal :: Int) `shouldBe` 43++    it "dispatches first-order operations via interpretAll" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          op :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          op = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts++          getHandler :: Handler '[] (FrameKleisli Identity) TestGet+          getHandler = Handler $ \_inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+                resFrame = insertField (Field @"x") (99 :: Int) emptyRecord+            in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame++          dummyPutHandler :: Handler '[] (FrameKleisli Identity) TestPut+          dummyPutHandler = Handler $ \_inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+            in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF++          handlers = insertField (Field @"get") getHandler+                   $ insertField (Field @"put") dummyPutHandler+                   $ emptyRecord++          kleisli = interpretAll handlers op+          inFrame = insertField (Field @"x") (0 :: Int) emptyRecord+          Identity outFrame = runFrameKleisli kleisli inFrame+          !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0+      (unsafeCoerce# xVal :: Int) `shouldBe` 99++    it "interprets through ScopeRow boundary nodes using contravariant gatherRecord" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          inner :: Penelope '[] TestEF '["x" ':= Int] '["x" ':= Int]+          inner = sendPolyF' @"get" @'["x" ':= Int] (100 :: Int) conts++          weakened :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int]+          weakened = weakenEF @TestEFExtended inner++          getHandler :: Handler '[] (FrameKleisli Identity) TestGet+          getHandler = Handler $ \_inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+                resFrame = insertField (Field @"x") (99 :: Int) emptyRecord+            in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame++          dummyPutHandler :: Handler '[] (FrameKleisli Identity) TestPut+          dummyPutHandler = Handler $ \_inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+            in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF++          handlersExt = insertField (Field @"get") getHandler+                      $ insertField (Field @"put") dummyPutHandler+                      $ insertField (Field @"extra") getHandler+                      $ emptyRecord++          kleisli = interpretAll handlersExt weakened+          inFrame = insertField (Field @"x") (0 :: Int) emptyRecord+          Identity outFrame = runFrameKleisli kleisli inFrame+          !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0+      (unsafeCoerce# xVal :: Int) `shouldBe` 99++  describe "Penelope.Core.Engine.Partial" $ do+    it "peels target effect via interpretSub leaving residual effect in AST" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          opPut :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int]+          opPut = sendPolyF' @"put" @'["x" ':= Int] (100 :: Int) conts++          getHandler :: Handler '["put" ':= TestPut, "extra" ':= TestGet] (Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet]) TestGet+          getHandler = Handler $ \inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+                resFrame = insertField (Field @"x") (42 :: Int) emptyRecord+            in preComposeRoute inMap (retK resFrame)++          handlers = insertField (Field @"get") getHandler emptyRecord+          peeled :: Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet] '["x" ':= Int] '["x" ':= Int]+          peeled = interpretSub @'["get" ':= TestGet] @'["put" ':= TestPut, "extra" ':= TestGet] @TestEFExtended handlers opPut++      case peeled of+        OpF tag# _ _ _ -> do+          case tag# of _ -> (1 :: Int) `shouldBe` 1+        _ -> expectationFailure "Expected OpF constructor with remapped residual tag"++    it "peeled computation can subsequently be interpreted by interpretAll" $ do+      let retCont = BranchCont (\_ -> route @'["x" ':= Int] @'["x" ':= Int])+          conts = insertField (Field @"ret") retCont emptyRecord+          opPut :: Penelope '[] TestEFExtended '["x" ':= Int] '["x" ':= Int]+          opPut = sendPolyF' @"put" @'["x" ':= Int] (100 :: Int) conts++          getHandler :: Handler '["put" ':= TestPut, "extra" ':= TestGet] (Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet]) TestGet+          getHandler = Handler $ \inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+                resFrame = insertField (Field @"x") (42 :: Int) emptyRecord+            in preComposeRoute inMap (retK resFrame)++          handlers = insertField (Field @"get") getHandler emptyRecord+          peeled :: Penelope '[] '["put" ':= TestPut, "extra" ':= TestGet] '["x" ':= Int] '["x" ':= Int]+          peeled = interpretSub @'["get" ':= TestGet] @'["put" ':= TestPut, "extra" ':= TestGet] @TestEFExtended handlers opPut++          putHandlerFinal :: Handler '[] (FrameKleisli Identity) TestPut+          putHandlerFinal = Handler $ \_inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+                resFrame = insertField (Field @"x") (77 :: Int) emptyRecord+            in FrameKleisli $ \_inF -> runFrameKleisli (retK resFrame) resFrame++          extraHandlerFinal :: Handler '[] (FrameKleisli Identity) TestGet+          extraHandlerFinal = Handler $ \_inMap _payload kConts ->+            let !(Identity elabK) = indexSmallArray (let RowRep (Rep _ arr) = kConts in arr) 0+                !(BranchCont retK) = unsafeCoerce# elabK+            in FrameKleisli $ \inF -> runFrameKleisli (retK emptyRecord) inF++          handlersFinal = insertField (Field @"put") putHandlerFinal+                        $ insertField (Field @"extra") extraHandlerFinal+                        $ emptyRecord++          kleisli = interpretAll handlersFinal peeled+          inFrame = insertField (Field @"x") (0 :: Int) emptyRecord+          Identity outFrame = runFrameKleisli kleisli inFrame+          !(Identity xVal) = indexSmallArray (let RowRep (Rep _ arr) = outFrame in arr) 0+      (unsafeCoerce# xVal :: Int) `shouldBe` 77+