resin (empty) → 0.1.0.0

raw patch · 5 files changed

+234/−0 lines, 5 filesdep +basedep +faildep +ghc-primsetup-changed

Dependencies added: base, fail, ghc-prim, semigroupoids, semigroups

Files

LICENSE +26/−0
Setup.hs +2/−0
readme.md +9/−0
resin.cabal +96/−0
src/Resin/Binders/Tree.hs +101/−0

+ LICENSE view

@@ -0,0 +1,26 @@+Copyright (c) 2016, Carter Tazio Schonwald+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the+   distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ readme.md view

@@ -0,0 +1,9 @@+# Resin : High performance Planar (2D) Variable binders++Resin is an experiment in variable binder design inspired by binder libraries+such as Bound and UnBound (no relation), with the goal being to provide+high performance and excellent abstraction on as large a space of syntaxes as+is feasible.+++

+ resin.cabal view

@@ -0,0 +1,96 @@+-- Initial resin.cabal generated by cabal init.  For further documentation,+--  see http://haskell.org/cabal/users-guide/++-- The name of the package.+name:                resin++-- The package version.  See the Haskell package versioning policy (PVP)+-- for standards guiding when and how versions should be incremented.+-- http://www.haskell.org/haskellwiki/Package_versioning_policy+-- PVP summary:      +-+------- breaking API changes+--                   | | +----- non-breaking API additions+--                   | | | +--- code changes with no API change+version:             0.1.0.0++-- A short (one-line) description of the package.+synopsis:            High performance variable binders++-- A longer description of the package.+description: High Performance Variable Binders library++-- URL for the project homepage or repository.+homepage:            http://github.com/cartazio/resin+++-- The license under which the package is released.+license:             BSD2++-- The file containing the license text.+license-file:        LICENSE++-- The package author(s).+author:              Carter Tazio Schonwald++-- An email address to which users can send suggestions, bug reports, and+-- patches.+maintainer:          carter at wellposed dot com++-- A copyright notice.+-- copyright:++category:            Language++build-type:          Simple++++-- Extra files to be distributed with the package, such as examples or a+-- README.+extra-source-files:  readme.md++++-- Constraint on the version of Cabal needed to build this package.+cabal-version:       >=1.10++source-repository head+  type: git+  location: https://github.com/cartazio/ralist.git++library+  -- Modules exported by the library.+  exposed-modules:+                      -- Resin++                      -- ,+                      Resin.Binders.Tree++                   --   ,Resin.Calculus.Derivatives++                    --  ,Resin.Environment.Class++  -- Modules included in this library but not exported.+  -- other-modules:++  -- LANGUAGE extensions used by modules in this package.+  -- other-extensions:++  -- Other library packages from which modules are imported.+  build-depends:      base >=4.8 && <4.11+                      ,ghc-prim >= 0.4 && < 0.6+                      ,semigroupoids >= 5.0 && <  5.3+++  -- Directories containing source files.+  hs-source-dirs:      src+  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+  else+    -- provide/emulate `Control.Monad.Fail` and `Data.Semigroups` API for pre-GHC8+    build-depends: fail == 4.9.*, semigroups == 0.18.*+  ghc-options: -Wall+  -- Base language which the package is written in.+  default-language:    Haskell2010+

+ src/Resin/Binders/Tree.hs view

@@ -0,0 +1,101 @@+{-# 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))+