Get (empty) → 0.2018.1.10

raw patch · 7 files changed

+257/−0 lines, 7 filesdep +Getdep +basedep +constraintssetup-changed

Dependencies added: Get, base, constraints, singletons

Files

ChangeLog.md +3/−0
Get.cabal +56/−0
LICENSE +30/−0
README.md +1/−0
Setup.hs +2/−0
src/Control/Get.hs +163/−0
test/Spec.hs +2/−0

+ ChangeLog.md view

@@ -0,0 +1,3 @@+# Changelog for Get++## Unreleased changes

+ Get.cabal view

@@ -0,0 +1,56 @@+-- This file has been generated from package.yaml by hpack version 0.20.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 30432a52fec2c47773bbe8af90d352f609f0b7cfc926436a2db1549755332d46++name:           Get+version:        0.2018.1.10+synopsis:       get stuff out of stuff+description:    Please see the README on Github at <https://github.com/MarisaKirisame/Get#readme>+category:       control+homepage:       https://github.com/MarisaKirisame/Get#readme+bug-reports:    https://github.com/MarisaKirisame/Get/issues+author:         Marisa Kirisame+maintainer:     lolisa@marisa.moe+copyright:      2018 Marisa Kirisame+license:        BSD3+license-file:   LICENSE+build-type:     Simple+cabal-version:  >= 1.10++extra-source-files:+    ChangeLog.md+    README.md++source-repository head+  type: git+  location: https://github.com/MarisaKirisame/Get++library+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , constraints ==0.9.1+    , singletons ==2.3.1+  exposed-modules:+      Control.Get+  other-modules:+      Paths_Get+  default-language: Haskell2010++test-suite Get-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      Get+    , base >=4.7 && <5+    , constraints ==0.9.1+    , singletons ==2.3.1+  other-modules:+      Paths_Get+  default-language: Haskell2010

+ LICENSE view

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

+ README.md view

@@ -0,0 +1,1 @@+# Get

+ Setup.hs view

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

+ src/Control/Get.hs view

@@ -0,0 +1,163 @@+{-# LANGUAGE+  MultiParamTypeClasses,+  FlexibleInstances,+  EmptyCase,+  FlexibleContexts,+  UndecidableInstances,+  DataKinds,+  KindSignatures,+  FunctionalDependencies,+  TypeFamilies,+  ConstraintKinds,+  UndecidableSuperClasses+#-}++module Control.Get where++import Data.Singletons.Prelude.Bool+import Data.Proxy+import Data.Constraint (Dict(..), withDict)++data And x y = And x y+data Or x y = OrLeft x | OrRight y++data Bottom+fromBot :: Bottom -> a+fromBot bot = case bot of++data Top = Top++fromVal :: a -> Proxy a+fromVal _ = Proxy++-- Lattice Specific Operation so they need to be resolved first. Write your instance at TryGetAux.+class TryGet as from self ok | as from self -> ok where+  tryGetSing :: Proxy self -> Proxy from -> Proxy as -> Sing ok+  tryGetVal :: self -> from -> Proxy as -> If ok as ()+  tryGet :: self -> from -> Proxy as -> (If ok as (), Sing ok)+  tryGet self from p = (tryGetVal self from p, tryGetSing (fromVal self) (fromVal from) p)++class TryGet as from from True => Get as from where+  get :: from -> as+  get f = res where+    res = tryGetVal f f (fromVal res)++instance TryGet as from from True => Get as from++instance TryGet Top from self True where+  tryGetVal _ _ _ = Top+  tryGetSing _ _ _ = STrue++instance ok ~ False => TryGet as Top self ok where+  tryGetVal _ _ _ = ()+  tryGetSing _ _ _ = SFalse++instance TryGet as Bottom self True where+  tryGetVal _ bot _ = fromBot bot+  tryGetSing _ _ _ = STrue++andLeftP :: Proxy (And l r) -> Proxy l+andLeftP _ = Proxy+andRightP :: Proxy (And l r) -> Proxy r+andRightP _ = Proxy++class TryGetAndL a b from self (aOK :: Bool) (andOK :: Bool) | b from self aOK -> andOK where+  tryGetAndLVal :: self -> from -> (If aOK a (), Sing aOK) -> Proxy (And a b) -> If andOK (And a b) ()+  tryGetAndLSing :: Proxy self -> Proxy from -> Sing aOK -> Proxy (And a b) -> Sing andOK++instance TryGetAndL a b from self False False where+  tryGetAndLVal _ _ _ _ = ()+  tryGetAndLSing _ _ _ _ = SFalse++instance TryGet b from self andOK => TryGetAndL a b from self True andOK where+  tryGetAndLVal self from (a, _) p = let (b, s) = tryGet self from (andRightP p) in+    case s of+      STrue -> And a b+      SFalse -> ()+  tryGetAndLSing self from _ p = tryGetSing self from (andRightP p)++instance (TryGet a from self aOK, TryGetAndL a b from self aOK andOK) => TryGet (And a b) from self andOK where+  tryGetVal self from p = tryGetAndLVal self from (tryGet self from (andLeftP p)) p+  tryGetSing self from p = tryGetAndLSing self from (tryGetSing self from (andLeftP p)) p++class TryGetAndR as b self (aOK :: Bool) (andOK :: Bool) | as b self aOK -> andOK where+  tryGetAndRVal :: self -> (If aOK as (), Sing aOK) -> b -> Proxy as -> If andOK as ()+  tryGetAndRSing :: Proxy self -> Sing aOK -> Proxy b -> Proxy as -> Sing andOK++instance TryGetAndR as b self True True where+  tryGetAndRVal _ (a, _) _ _ = a+  tryGetAndRSing _ _ _ _ = STrue++instance TryGet as b self andOK => TryGetAndR as b self False andOK where+  tryGetAndRVal self _ b p = tryGetVal self b p+  tryGetAndRSing self _ from p = tryGetSing self from p++instance (TryGet as a self aOK, TryGetAndR as b self aOK andOK) => TryGet as (And a b) self andOK where+  tryGetVal self (And a b) p = tryGetAndRVal self (tryGet self a p) b p+  tryGetSing self from p = tryGetAndRSing self (tryGetSing self (andLeftP from) p) (andRightP from) p++orLeftP :: Proxy (Or l r) -> Proxy l+orLeftP _ = Proxy+orRightP :: Proxy (Or l r) -> Proxy r+orRightP _ = Proxy++class TryGetOrL a b from self (aOK :: Bool) (orOK :: Bool) | b from self aOK -> orOK where+  tryGetOrLVal :: self -> from -> (If aOK a (), Sing aOK) -> Proxy (Or a b) -> If orOK (Or a b) ()+  tryGetOrLSing :: Proxy self -> Proxy from -> Sing aOK -> Proxy (Or a b) -> Sing orOK++instance TryGetOrL a b from self True True where+  tryGetOrLVal _ _ (a, _) _ = OrLeft a+  tryGetOrLSing _ _ _ _ = STrue++instance TryGet b from self orOK => TryGetOrL a b from self False orOK where+  tryGetOrLVal self from _ p = let (b, s) = tryGet self from (orRightP p) in+    case s of+      STrue -> OrRight b+      SFalse -> ()+  tryGetOrLSing self from _ p = tryGetSing self from (orRightP p)++instance (TryGet a from self aOK, TryGetOrL a b from self aOK orOK) => TryGet (Or a b) from self orOK where+  tryGetVal self from p = tryGetOrLVal self from (tryGet self from (orLeftP p)) p+  tryGetSing self from p = tryGetOrLSing self from (tryGetSing self from (orLeftP p)) p++class TryGetOrR as b self (aOK :: Bool) orOK | as b self aOK -> orOK where+  tryGetOrRVal :: self -> b -> Sing aOK -> Proxy as -> If orOK as ()+  tryGetOrRSing :: Proxy self -> Proxy b -> Sing aOK -> Proxy as -> Sing orOK+  tryGetOrRUnify :: Proxy self -> Proxy b -> Sing aOK -> Proxy as -> Dict (orOK ~ True) -> Dict (aOK ~ True)++instance TryGetOrR as b self False False where+  tryGetOrRVal _ _ _ _ = ()+  tryGetOrRSing _ _ _ _ = SFalse+  tryGetOrRUnify _ _ _ _ x = x++instance TryGet as b self orOK => TryGetOrR as b self True orOK where+  tryGetOrRVal self b _ p = tryGetVal self b p+  tryGetOrRSing self b _ p = tryGetSing self b p+  tryGetOrRUnify _ _ _ _ _ = Dict++instance (TryGet as a self aOK, TryGetOrR as b self aOK orOK) => TryGet as (Or a b) self orOK where+  tryGetVal self o@(OrLeft a) p =+    let+      oP = fromVal o+      orP = orRightP oP+      selfP = fromVal self+      singL = tryGetSing selfP (fromVal a) p+    in+      case tryGetOrRSing (fromVal self) orP singL p of+        STrue -> tryGetOrRUnify selfP orP singL p Dict `withDict` tryGetVal self a p+        SFalse -> ()+  tryGetVal self o@(OrRight b) p = tryGetOrRVal self b (tryGetSing (fromVal self) (orLeftP $ fromVal o) p) p+  tryGetSing self from p = tryGetOrRSing self (orRightP from) (tryGetSing self (orLeftP from) p) p++instance ok ~ True => TryGet a a self ok where+  tryGetVal _ a _ = a+  tryGetSing _ _ _ = STrue++newtype Protected x = Protected { runProtected :: x }++unProtectedP :: Proxy (Protected x) -> Proxy x+unProtectedP _ = Proxy++instance TryGet as from from ok => TryGet as (Protected from) self ok where+  tryGetVal self (Protected from) p = tryGetVal from from p+  tryGetSing _ pFrom p = let from = unProtectedP pFrom in tryGetSing from from p

+ test/Spec.hs view

@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"