resin 0.1.0.2 → 0.2.0.0
raw patch · 4 files changed
+155/−107 lines, 4 filesdep +ralistdep ~basedep ~ghc-prim
Dependencies added: ralist
Dependency ranges changed: base, ghc-prim
Files
- changelog.md +3/−0
- resin.cabal +8/−7
- src/Resin/Binders/Tree.hs +15/−100
- src/Resin/Binders/Tree/Internal.hs +129/−0
+ changelog.md view
@@ -0,0 +1,3 @@++# Versions 0.1.0.0 - 0.1.0.2+initial release(s) with only the private proof rep for tree paths
resin.cabal view
@@ -10,7 +10,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change-version: 0.1.0.2+version: 0.2.0.0 -- A short (one-line) description of the package. synopsis: High performance variable binders@@ -46,7 +46,8 @@ -- Extra files to be distributed with the package, such as examples or a -- README.-extra-source-files: readme.md+extra-source-files: readme.md+ changelog.md @@ -62,8 +63,8 @@ exposed-modules: -- Resin - -- , Resin.Binders.Tree+ ,Resin.Binders.Tree.Internal -- ,Resin.Calculus.Derivatives @@ -76,9 +77,11 @@ -- other-extensions: -- Other library packages from which modules are imported.- build-depends: base >=4.8 && <4.11- ,ghc-prim >= 0.4 && < 0.6+ build-depends: base >= 4.8 && < 4.12+ ,ghc-prim+ -- >= 0.4 && < 0.6 ,semigroupoids >= 5.0 && < 5.3+ ,ralist == 0.2.* -- Directories containing source files.@@ -86,8 +89,6 @@ ghc-options: -Wall - if impl(ghc >= 8.0) && impl(ghc < 8.2)- ghc-options: -Wcompat -Wnoncanonical-monad-instances -Wnoncanonical-monadfail-instances if impl(ghc >= 8.0) && impl(ghc < 8.2) ghc-options: -Wno-redundant-constraints
src/Resin/Binders/Tree.hs view
@@ -1,101 +1,16 @@-{-# LANGUAGE FlexibleContexts,FlexibleInstances,GADTs,DataKinds, PolyKinds, KindSignatures #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE TypeInType #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE TypeOperators #-}--module Resin.Binders.Tree where-import Data.Kind-import Numeric.Natural-import Data.Semigroupoid---import Data.Coerce-import Unsafe.Coerce (unsafeCoerce)-import Data.Type.Equality---import qualified Data.Semigroupoid.Dual as DL---{--This module models binders which respect scope having a tree shaped topology-or at least it models some ideas about (finite?) paths on (finite??!) trees---}---data IxEq :: (k -> Type ) -> k -> k -> Type where- PolyRefl :: IxEq f i i- MonoRefl :: forall f i . f i -> IxEq f i i----testIxEquality :: TestEquality f => IxEq f a b -> IxEq f b c ->--instance TestEquality f => TestEquality (IxEq f i) where- testEquality (MonoRefl f1) (MonoRefl f2) = testEquality f1 f2- testEquality (PolyRefl )(MonoRefl _f2) = Just Refl- testEquality (MonoRefl _f1) (PolyRefl ) = Just Refl- testEquality (PolyRefl ) (PolyRefl ) = Just Refl--{- | `Inject` is about---}-data Inject :: (k -> Type ) -> k -> k -> Type where- InjectRefl :: forall f a b . IxEq f a b-> Inject f a b- --MonoId :: forall f i . (f i) -> Inject f i i- -- should MonoId be strict in its argument?- CompactCompose :: forall f i j . (IxEq f i i) -> (IxEq f j j ) -> Natural -> Inject f i j- -- i is origin/root- -- j is leaf- -- compact compose is unsafe for users, but should be exposed in a .Internal- -- module----instance Semigroupoid (Inject f) where- --PolyId `o` PolyId = PolyId- (InjectRefl (MonoRefl _p)) `o` (!f) = f- (InjectRefl (PolyRefl)) `o` (!f) = f- (CompactCompose in1 out1 size) `o` (InjectRefl (PolyRefl)) = CompactCompose in1 out1 size- (CompactCompose in1 out1 size) `o` (InjectRefl (MonoRefl !_p)) = CompactCompose in1 out1 size- (CompactCompose _cmiddle2 cout sizeleft)- `o` (CompactCompose cin _cmiddle1 sizeright) = CompactCompose cin cout (sizeright + sizeleft)- --- TODO is this case to lazy?---- extract is the dual of Inject--- aka Data.Semigroupoid.Dual is nearly the exact same type :)-newtype Extract :: (k -> Type ) -> k -> k -> Type where- Dual :: ((Inject f) b a ) -> Extract f a b--- not sure if this is the right design vs- -- :: Inject f b a -> Extract f a b --- (which has more explicit duality and less newtypery)---instance Semigroupoid (Extract f) where- o = \ (Dual l) (Dual r) -> Dual $ r `o` l---data TreeEq :: (k -> Type ) -> k -> k -> Type where- TreeInject :: Inject f a b -> TreeEq f a b- TreeExtract :: Extract f a b -> TreeEq f a b- TreeRefl :: TreeEq f c c------ this might limit a,c to being kind (or sort?) * / Type for now, but thats OK ??-treeElimination :: TestEquality f => Inject f a b -> Extract f b c-> (TreeEq f a c)-treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl PolyRefl)) = TreeRefl-treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl PolyRefl)) = TreeRefl-treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl (MonoRefl _p2))) = TreeRefl-treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl(MonoRefl _p2))) = TreeRefl-treeElimination (CompactCompose fa _fb1 n1) (Dual (CompactCompose fc _fb2 n2)) =- case (compare n1 n2, max n1 n2 - min n1 n2) of- (EQ, _ )-> (unsafeCoerce TreeRefl) :: TreeEq f a c- --- if the path is zero length they must be equal!- --- AUDIT MEEEE- (GT, m )-> TreeInject (CompactCompose fa fc m)- (LT, m ) -> TreeExtract (Dual (CompactCompose fc fa m))-treeElimination (InjectRefl p@(PolyRefl))- d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d-treeElimination (InjectRefl p@(MonoRefl _))- d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d-treeElimination d@( CompactCompose _fc _fb _n)- (Dual (InjectRefl p@(PolyRefl))) = treeElimination d (Dual (CompactCompose p p 0))-treeElimination d@(CompactCompose _fc _fb _n)- (Dual (InjectRefl p@(MonoRefl _))) = treeElimination d (Dual (CompactCompose p p 0))+{-# LANGUAGE Trustworthy #-}+module Resin.Binders.Tree(+ -- | the safe subset of the api... I think+ IxEq(..)+ ,Inject(InjectRefl)+ ,Extract -- Extract is just a newtype wrapper .. for now+ ,TreeEq(..)+ ,treeElimination+ ,rightExtendInject+ ,leftExtendExtract+ ,jumpDepthInject -- not sure if this operation is safe+ ,jumpDepthExtract -- not sure if thats safe too+ )+ where+import Resin.Binders.Tree.Internal
+ src/Resin/Binders/Tree/Internal.hs view
@@ -0,0 +1,129 @@+{-# LANGUAGE FlexibleContexts,FlexibleInstances,GADTs,DataKinds, PolyKinds, KindSignatures #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeInType #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE TypeOperators #-}++module Resin.Binders.Tree.Internal(+ -- | the safe subset of the api... I think+ IxEq(..)+ ,Inject(..)+ ,Extract(..) -- Extract is just a newtype wrapper .. for now+ ,TreeEq(..)+ ,treeElimination+ ,rightExtendInject+ ,leftExtendExtract+ ,jumpDepthInject -- not sure if this operation is safe+ ,jumpDepthExtract -- not sure if thats safe too+ ) where+import Data.Kind+import Numeric.Natural+import Data.Semigroupoid+--import Data.Coerce+import Unsafe.Coerce (unsafeCoerce)+import Data.Type.Equality+--import qualified Data.Semigroupoid.Dual as DL+++++{-+This module models binders which respect scope having a tree shaped topology+or at least it models some ideas about (finite?) paths on (finite??!) trees++-}+++data IxEq :: (k -> Type ) -> k -> k -> Type where+ PolyRefl :: IxEq f i i+ MonoRefl :: forall f i . f i -> IxEq f i i++--testIxEquality :: TestEquality f => IxEq f a b -> IxEq f b c ->++instance TestEquality f => TestEquality (IxEq f i) where+ testEquality (MonoRefl f1) (MonoRefl f2) = testEquality f1 f2+ testEquality (PolyRefl )(MonoRefl _f2) = Just Refl+ testEquality (MonoRefl _f1) (PolyRefl ) = Just Refl+ testEquality (PolyRefl ) (PolyRefl ) = Just Refl++{- | `Inject` is about++-}+data Inject :: (k -> Type ) -> k -> k -> Type where+ InjectRefl :: forall f a b . IxEq f a b-> Inject f a b+ --MonoId :: forall f i . (f i) -> Inject f i i+ -- should MonoId be strict in its argument?+ CompactCompose :: forall f i j . (IxEq f i i) -> (IxEq f j j ) -> Natural -> Inject f i j+ -- i is origin/root+ -- j is leaf+ -- compact compose is unsafe for users, but should be exposed in a .Internal+ -- module++rightExtendInject :: Inject p a b -> p c -> Inject p a c+rightExtendInject (InjectRefl PolyRefl) rP = CompactCompose PolyRefl (MonoRefl rP) 1+rightExtendInject (InjectRefl (MonoRefl f)) rP = CompactCompose (MonoRefl f) (MonoRefl rP) 1+rightExtendInject (CompactCompose pa _pb n) rP = CompactCompose pa (MonoRefl rP) (n+1 )++leftExtendExtract :: p a -> Extract p b c -> Extract p a c+leftExtendExtract p (Dual inj) = Dual (rightExtendInject inj p)+++jumpDepthInject :: Natural -> p c -> Inject p a b -> Inject p a c+jumpDepthInject plus pc (InjectRefl PolyRefl) = CompactCompose PolyRefl (MonoRefl pc) (1 + plus)+jumpDepthInject plus pc (InjectRefl (MonoRefl pa)) = CompactCompose (MonoRefl pa) (MonoRefl pc) (1 + plus)+jumpDepthInject plus pc (CompactCompose pa _pb n) = CompactCompose pa (MonoRefl pc) (n + plus + 1 )++jumpDepthExtract :: Natural -> Extract p b c -> p a -> Extract p a c+jumpDepthExtract plus (Dual cc) pc = Dual (jumpDepthInject plus pc cc)++instance Semigroupoid (Inject f) where+ --PolyId `o` PolyId = PolyId+ (InjectRefl (MonoRefl _p)) `o` (!f) = f+ (InjectRefl (PolyRefl)) `o` (!f) = f+ (CompactCompose in1 out1 size) `o` (InjectRefl (PolyRefl)) = CompactCompose in1 out1 size+ (CompactCompose in1 out1 size) `o` (InjectRefl (MonoRefl !_p)) = CompactCompose in1 out1 size+ (CompactCompose _cmiddle2 cout sizeleft)+ `o` (CompactCompose cin _cmiddle1 sizeright) = CompactCompose cin cout (sizeright + sizeleft)+ --- TODO is this case too lazy?++-- extract is the dual of Inject+-- aka Data.Semigroupoid.Dual is nearly the exact same type :)+newtype Extract :: (k -> Type ) -> k -> k -> Type where+ Dual :: ((Inject f) b a ) -> Extract f a b+-- not sure if this is the right design vs+ -- :: Inject f b a -> Extract f a b --- (which has more explicit duality and less newtypery)+++instance Semigroupoid (Extract f) where+ o = \ (Dual l) (Dual r) -> Dual $ r `o` l+++data TreeEq :: (k -> Type ) -> k -> k -> Type where+ TreeInject :: Inject f a b -> TreeEq f a b+ TreeExtract :: Extract f a b -> TreeEq f a b+ TreeRefl :: TreeEq f c c+++--- this might limit a,c to being kind (or sort?) * / Type for now, but thats OK ??+treeElimination :: TestEquality f => Inject f a b -> Extract f b c-> (TreeEq f a c)+treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl PolyRefl)) = TreeRefl+treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl PolyRefl)) = TreeRefl+treeElimination (InjectRefl PolyRefl) (Dual (InjectRefl (MonoRefl _p2))) = TreeRefl+treeElimination (InjectRefl (MonoRefl _p1)) (Dual (InjectRefl(MonoRefl _p2))) = TreeRefl+treeElimination (CompactCompose fa _fb1 n1) (Dual (CompactCompose fc _fb2 n2)) =+ case (compare n1 n2, max n1 n2 - min n1 n2) of+ (EQ, _ )-> (unsafeCoerce TreeRefl) :: TreeEq f a c+ --- if the path is zero length they must be equal!+ --- AUDIT MEEEE+ (GT, m )-> TreeInject (CompactCompose fa fc m)+ (LT, m ) -> TreeExtract (Dual (CompactCompose fc fa m))+treeElimination (InjectRefl p@(PolyRefl))+ d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d+treeElimination (InjectRefl p@(MonoRefl _))+ d@(Dual (CompactCompose _fc _fb _n)) = treeElimination (CompactCompose p p 0) d+treeElimination d@( CompactCompose _fc _fb _n)+ (Dual (InjectRefl p@(PolyRefl))) = treeElimination d (Dual (CompactCompose p p 0))+treeElimination d@(CompactCompose _fc _fb _n)+ (Dual (InjectRefl p@(MonoRefl _))) = treeElimination d (Dual (CompactCompose p p 0))+