packages feed

ds-kanren (empty) → 0.2.0.0

raw patch · 8 files changed

+503/−0 lines, 8 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, ds-kanren, logict, tasty, tasty-quickcheck

Files

+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2014 Danny Gratzer++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ds-kanren.cabal view
@@ -0,0 +1,101 @@+name:                ds-kanren+version:             0.2.0.0+synopsis:            A subset of the miniKanren language+description:+  ds-kanren is an implementation of the <http://minikanren.org miniKanren> language.+  .+  == What's in ds-kanren?+  .+  ['disconj']+    Try the left and the right and gather solutions that satisfy+    either one.+  ['fresh']+    Create a fresh logical variable+  ['===']+    Equate two terms. This will backtrack if we can't unify+    them in this branch.+  ['run']+    Actually run a logical computation and return results and+    the constraints on them.+  .+  In addition to these core combinators, we also export a few+  supplimentary tools.+  .+  ['=/=']+    The opposite of '===', ensure that the left and right+    never unify.+  .+  == The Classic Example+  .+  We can define the classic @appendo@ relationship by encoding+  lists in the Lisp "bunch-o-pairs" method.+  .+  > appendo :: Term -> Term -> Term -> Predicate+  > appendo l r o =+  >   conde [ program [l === "nil",  o === r]+  >         , manyFresh $ \h t o ->+  >             program [ Pair h t === l+  >                     , appendo t r o+  >                     , Pair h o === o ]]+  .+  Once we have a relationship, we can run it backwards and forwards+  as we can with most logic programs.+  .+  >>> let l = list ["foo", "bar"]+  .+  >>> map fst . runN 1 $ \t -> appendo t l l+  [nil]+  >>> map fst . runN 1 $ \t -> appendo l t l+  [nil]+  >>> map fst . runN 1 $ \t -> appendo l l t+  [(foo, (bar, (foo, (bar, nil))))]+  .+  == Related Links+  .+  Some good places to start learning about miniKanren would be+  .+     * <http://www.amazon.com/The-Reasoned-Schemer-Daniel-Friedman/DP/0262562146 The Reasoned Schemer>+     * <http://www.infoq.com/presentations/miniKanren A presentation at StrangeLoop>+     * <https://github.com/miniKanren/miniKanren The canonical implementation>+license:             MIT+license-file:        LICENSE+author:              Danny Gratzer+maintainer:          jozefg@cmu.edu+category:            Language+build-type:          Simple+cabal-version:       >=1.10+source-repository head+  type:     hg+  location: http://bitbucket.org/jozefg/ds-kanren++library+  exposed-modules:     Language.DSKanren+                     , Language.DSKanren.Core+                     , Language.DSKanren.Sugar+  build-depends:       base >=4 && <5+                     , containers >=0.4+                     , logict+  hs-source-dirs:      src+  default-language:    Haskell2010+Test-Suite test-unify:+  hs-source-dirs: test+  type:               exitcode-stdio-1.0+  main-is:            Unify.hs+  hs-source-dirs:     test+  build-depends:      ds-kanren+                    , tasty+                    , tasty-quickcheck+                    , QuickCheck+                    , base >=4 && <5+  default-language:    Haskell2010+Test-Suite test-list-ops:+  hs-source-dirs: test+  type:               exitcode-stdio-1.0+  main-is:            List.hs+  hs-source-dirs:     test+  build-depends:      ds-kanren+                    , tasty+                    , tasty-quickcheck+                    , QuickCheck+                    , base >=4 && <5+  default-language:    Haskell2010
+ src/Language/DSKanren.hs view
@@ -0,0 +1,7 @@+-- | The toplevel module exports the core language, in+-- 'Language.DSKanren.Core' and some simple combinators from+-- 'Language.DSKanren.Sugar'.+module Language.DSKanren ( module Language.DSKanren.Core+                         , module Language.DSKanren.Sugar ) where+import Language.DSKanren.Core+import Language.DSKanren.Sugar
+ src/Language/DSKanren/Core.hs view
@@ -0,0 +1,157 @@+{-# LANGUAGE RecordWildCards #-}+module Language.DSKanren.Core ( Term(..)+                              , Var+                              , Neq+                              , (===)+                              , (=/=)+                              , fresh+                              , conj+                              , disconj+                              , Predicate+                              , failure+                              , success+                              , currentGoal+                              , run ) where+import           Control.Monad.Logic+import           Data.String+import qualified Data.Map            as M++-- | The abstract type of variables. As a consumer you should never+-- feel the urge to manipulate these directly.+newtype Var = V Integer deriving (Eq, Ord)++instance Show Var where+  show (V i) = '_' : show i++suc :: Var -> Var+suc (V i) = V (i + 1)++-- | The terms of our logical language.+data Term = Var Var        -- ^ Logical variables that can unify with other terms+          | Atom String    -- ^ The equivalent of Scheme's symbols or keywords+          | Pair Term Term -- ^ Pairs of terms+          deriving Eq++instance Show Term where+  show t = case t of+    Var v -> show v+    Atom a -> '\'' : a+    Pair l r -> "(" ++ show l ++ ", " ++ show r ++ ")"++instance IsString Term where+  fromString = Atom++type Sol = M.Map Var Term++-- | Substitute all bound variables in a term giving the canonical+-- term in an environment. Sometimes the solution isn't canonical,+-- so some ugly recursion happens. Happily we don't have to prove+-- normalization.+canonize :: Sol -> Term -> Term+canonize sol t = case t of+  Atom a -> Atom a+  Pair l r -> canonize sol l `Pair` canonize sol r+  Var i -> maybe (Var i) (canonize $ M.delete i sol) $ M.lookup i sol++-- | Ensures that a variable doesn't occur in some other term. This+-- prevents us from getting some crazy infinite term. None of that+-- nonsense.+notIn :: Var -> Term -> Bool+notIn v t = case t of+  Var v' -> v /= v'+  Atom _ -> True+  Pair l r -> notIn v l && notIn v r++-- | Extend an environment with a given term. Note that+-- that we don't even bother to canonize things here, that+-- can wait until we extact a solution.+extend :: Var -> Term -> Sol -> Sol+extend = M.insert++-- | Unification cannot need not backtrack so this will either+-- universally succeed or failure. Tricksy bit, we don't want to allow+-- infinite terms since that can be narly. To preserve reflexivity, we+-- have a special check for when we compare a var to itself. This+-- doesn't extend the enviroment. With this special case we can add a+-- check to make sure we never unify a var with a term containing it.+unify :: Term -> Term -> Sol -> Maybe Sol+unify l r sol= case (l, r) of+  (Atom a, Atom a') | a == a' -> Just sol+  (Pair h t, Pair h' t') -> unify h h' sol >>= unify t t'+  (Var i, Var j) | i == j -> Just sol+  (Var i, t) | i `notIn` t -> Just (extend i t sol)+  (t, Var i) | i `notIn` t -> Just (extend i t sol)+  _ -> Nothing++type Neq = (Term, Term)+data State = State { sol :: Sol+                   , var :: Var+                   , neq :: [Neq] }+newtype Predicate = Predicate {unPred :: State -> Logic State}++-- | Validate the inqualities still hold.+-- To do this we try to unify each pair under the current+-- solution, if this fails we're okay. If they *don't* then+-- make sure that the solution under which they unify is an+-- extension of the solution set, ie we must add more facts+-- to get a contradiction.+checkNeqs :: State -> Logic State+checkNeqs s@State{..} = foldr go (return s) neq+  where go (l, r) m =+          case unify (canonize sol l) (canonize sol r) sol of+           Nothing -> m+           Just badSol -> if domain badSol == domain sol then mzero else m+        domain = M.keys++-- | Equating two terms will attempt to unify them and backtrack if+-- this is impossible.+(===) :: Term -> Term -> Predicate+(===) l r = Predicate $ \s@State {..} ->+  case unify (canonize sol l) (canonize sol r) sol of+   Just sol' -> checkNeqs s{sol = sol'}+   Nothing   -> mzero++-- | The opposite of unification. If any future unification would+-- cause these two terms to become equal we'll backtrack.+(=/=) :: Term -> Term -> Predicate+(=/=) l r = Predicate $ \s@State{..} -> checkNeqs s{neq = (l, r) : neq}++-- | Generate a fresh (not rigid) term to use for our program.+fresh :: (Term -> Predicate) -> Predicate+fresh withTerm =+  Predicate $ \State{..} ->+               unPred (withTerm $ Var var) $ State sol (suc var) neq++-- | Conjunction. This will return solutions that satsify both the+-- first and second predicate.+conj :: Predicate -> Predicate -> Predicate+conj p1 p2 = Predicate $ \s -> unPred p1 s >>- unPred p2++-- | Disjunction. This will return solutions that satisfy either the+-- first predicate or the second.+disconj :: Predicate -> Predicate -> Predicate+disconj p1 p2 = Predicate $ \s -> unPred p1 s `interleave` unPred p2 s++-- | The Eeyore of predicates, always fails. This is mostly useful as+-- a way of pruning out various conditions, as in+-- @'conj' (a '===' b) 'failure'@. This is also an identity for+-- 'disconj'.+failure :: Predicate+failure = Predicate $ const mzero++-- | The Tigger of predicates! always passes. This isn't very useful+-- on it's own, but is helpful when building up new combinators. This+-- is also an identity for 'conj'.+success :: Predicate+success = Predicate return++-- | The goal that this logic program is trying to create. This is+-- occasionally useful when we're doing generating programs.+currentGoal :: Term+currentGoal = Var (V 0)++-- | Run a program and find all solutions for the parametrized term.+run :: (Term -> Predicate) -> [(Term, [Neq])]+run mkProg = map answer . observeAll $ prog+  where prog = unPred (fresh mkProg) (State M.empty (V 0) [])+        answer State{..} = (canonize sol . Var $ V 0, neq)
+ src/Language/DSKanren/Sugar.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE FlexibleInstances #-}+module Language.DSKanren.Sugar where+import Language.DSKanren.Core++-- | Disjunction of many clauses. This can be thought as a logical+-- switch.+conde :: [Predicate] -> Predicate+conde = foldr disconj failure++-- | Conjuction of many clauses. Think of this as a sort of logical+-- semicolon.+program :: [Predicate] -> Predicate+program = foldr conj success++-- | Only grab n solutions. Useful for when the full logic program+-- might not terminate. Or takes its sweet time to do so.+runN :: Int -> (Term -> Predicate) -> [(Term, [Neq])]+runN n = take n . run++-- | We often want to introduce many fresh variables at once. We've+-- encoded this in DSKanren with the usual type class hackery for+-- variadic functions.+class MkFresh a where+  -- | Instantiate @a@ with as many fresh terms as needed to produce a+  -- predicate.+  manyFresh :: a -> Predicate+instance MkFresh a => MkFresh (Term -> a) where+  manyFresh = fresh . fmap manyFresh+instance MkFresh Predicate where+  manyFresh = id++-- | Build a lispish list out of terms. The atom @"nil"@ will serve as+-- the empty list and 'Pair' will be ':'.+list :: [Term] -> Term+list = foldr Pair (Atom "nil")
+ test/List.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE OverloadedStrings #-}+module Main where+import Language.DSKanren+import Test.Tasty.QuickCheck hiding ((===))+import Test.Tasty+import QuickCheckHelper++appendo :: Term -> Term -> Term -> Predicate+appendo l r o =+  conde [ program [l === "nil", o === r]+        , manyFresh $ \h t o' ->+            program [ Pair h t === l+                    , appendo t r o'+                    , Pair h o' === o ]]++heado :: Term -> Term -> Predicate+heado l h = fresh $ \t -> Pair h t === l++tailo :: Term -> Term -> Predicate+tailo l t = fresh $ \h -> Pair h t === l++isAppend :: TestTree+isAppend = testProperty "Head Works"+           . mapSize (const 3)+           . forAll (two . listOf1 $ mkTerm [])+           $ \(l, r) -> case runN 1 $ appendo (list l) (list r) of+                         (t, _) : _ -> t == list (l ++ r)+                         _ -> False++isHead :: TestTree+isHead = testProperty "Head Works"+         . mapSize (const 3)+         . forAll (listOf1 $ mkTerm [])+         $ \terms -> case runN 1 $ heado (list terms) of+                      (t, _) : _ -> t == head terms+                      _ -> False++isTail :: TestTree+isTail = testProperty "Tail Works"+         . mapSize (const 3)+         . forAll (listOf1 $ mkTerm [])+         $ \terms -> case runN 1 $ tailo (list terms) of+                      (t, _) : _ -> t == list (tail terms)+                      _ -> False++main :: IO ()+main = defaultMain (testGroup "List Tests" [isHead, isTail])
+ test/Unify.hs view
@@ -0,0 +1,134 @@+-- | Test to ensure that unification function as intended.+module Main where+import Language.DSKanren+import Test.Tasty+import Test.Tasty.QuickCheck hiding ((===))+import QuickCheckHelper++--------------------------- Equal -------------------------------------+eqrefl :: TestTree+eqrefl = testProperty "Reflexivity"+            . forTerm+            $ \t -> hasSolution (t === t)++eqcomm :: TestTree+eqcomm = testProperty "Commutative"+         . forTerm2+         $ \ l r ->+            hasSolution (l === r)+            ==> hasSolution (r === l)++eqtrans :: TestTree+eqtrans = testProperty "Transitive"+          . forTerm3+          $ \l m r ->+             hasSolution (conj (l === m) (m === r))+             ==> hasSolution (r === l)++eqTests :: TestTree+eqTests = testGroup "Equality" [eqrefl, eqcomm, eqtrans]++------------------------ Not Equal -----------------------------------+neqarefl :: TestTree+neqarefl = testProperty "Antireflexive"+           . forTerm+           $ \t -> not $ hasSolution (t =/= t)++neqcomm :: TestTree+neqcomm = testProperty "Commutative"+          . forTerm2+          $ \ l r ->+             hasSolution (l =/= r)+             ==> hasSolution (r =/= l)++neqTests :: TestTree+neqTests = testGroup "Inequality" [neqarefl, neqcomm]+++--------------------------- Fresh ------------------------------------+freshClosed :: TestTree+freshClosed = testProperty "Closed Under Fresh"+              . forPred+              $ \p -> hasSolution p ==> hasSolution (fresh $ const p)+freshUnify :: TestTree+freshUnify = testProperty "Unification Under Fresh"+             . forTerm+             $ \t -> forPred $ \p ->+             hasSolution p+             ==> hasSolution . fresh $ \v -> conj (t === v) p++freshTests :: TestTree+freshTests = testGroup "Fresh" [freshClosed, freshUnify]++--------------------------- Conj -------------------------------------+conjid :: TestTree+conjid = testProperty "Commutative"+              . forPred+              $ \p -> hasSolution p ==> hasSolution (conj success p)++conjcomm :: TestTree+conjcomm = testProperty "Commutative"+              . forPred2+              $ \p o ->+                 hasSolution (conj p o) ==> hasSolution (conj o p)++conjassoc :: TestTree+conjassoc = testProperty "Associative"+            . forPred3+            $ \l m r ->+               hasSolution (conj (conj l m) r)+               ==> hasSolution (conj l (conj m r))++conjTests :: TestTree+conjTests = testGroup "Conj" [conjid, conjcomm, conjassoc]++------------------------- Disconj ------------------------------------+disconjid :: TestTree+disconjid = testProperty "Commutative"+            . forPred+            $ \p -> hasSolution p ==> hasSolution (disconj failure p)++disconjcomm :: TestTree+disconjcomm = testProperty "Commutative"+              . forPred2+              $ \p o ->+                 hasSolution (disconj p o) ==> hasSolution (disconj o p)++disconjassoc :: TestTree+disconjassoc = testProperty "Associative"+               . forPred3+               $ \l m r ->+                  hasSolution (disconj (disconj l m) r)+                  ==> hasSolution (disconj l (disconj m r))++disconjTests :: TestTree+disconjTests = testGroup "Disconj" [disconjid, disconjcomm, disconjassoc]++------------------------- Success --------------------------------------+annihilatorDisconj :: TestTree+annihilatorDisconj = testProperty "Annihilates Disconj"+                     . forPred+                     $ \p -> hasSolution (disconj success p)++successTests :: TestTree+successTests = testGroup "Success" [annihilatorDisconj]++------------------------ Failure ---------------------------------------+annihilatorConj :: TestTree+annihilatorConj = testProperty "Annihilates Disconj"+                     . forPred+                     $ \p -> not $ hasSolution (conj failure p)++failureTests :: TestTree+failureTests = testGroup "Success" [annihilatorConj]++------------------------- Main -----------------------------------------+main :: IO ()+main = defaultMain . testGroup "List Tests" $+       [ eqTests+       , neqTests+       , freshTests+       , conjTests+       , disconjTests+       , successTests+       , failureTests ]