mini-egison 0.1.1 → 0.1.2

raw patch · 7 files changed

+414/−64 lines, 7 filesdep +sortnew-component:exe:cdclPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: sort

API changes (from Hackage documentation)

Files

• README.md +75/−6
• mini-egison.cabal +14/−3
• sample/cdcl.hs +202/−0
• src/Control/Egison/Core.hs +45/−14
• src/Control/Egison/Match.hs +22/−11
• src/Control/Egison/Matcher.hs +40/−29
• test/Spec.hs +16/−1

@@ -19,7 +19,7 @@   | matchDFS e e [C, ...]      -- match expression   | Something                  -- Something built-in matcher -C = [mc| p => e]               -- match clause+C = [mc| p => e |]             -- match clause  p = _                          -- wildcard   | $x                         -- pattern variable@@ -38,7 +38,7 @@ This expression returns a list of a single element because there is only one decomposition.  ```-matchAll [1,2,3] (List Integer) [[mc| cons $x $xs => (x, xs)]]+matchAll [1,2,3] (List Integer) [[mc| cons $x $xs => (x, xs)|]] -- [(1,[2,3])] ``` @@ -50,7 +50,7 @@ For example, by changing the matcher of the above `matchAll` from `List Integer` to `Multiset Integer`, the evaluation result changes as follows:  ```-matchAll [1,2,3] (Multiset Integer) [[mc| cons $x $xs => (x, xs)]]+matchAll [1,2,3] (Multiset Integer) [[mc| cons $x $xs => (x, xs)|]] -- [(1,[2,3]),(2,[1,3]),(3,[1,2])] ``` @@ -71,17 +71,86 @@ A non-linear pattern is effectively used for expressing the pattern.  ```-matchAll [1,2,5,9,4] (Multiset Integer) [[mc| cons $x (cons #(x+1) _) => x]]+matchAll [1,2,5,9,4] (Multiset Integer) [[mc| cons $x (cons #(x+1) _) => x|]] -- [1,4] ```  ### The `match` expression -preparing...+The `match` expression takes a target, a matcher, and match-clauses as the `matchAll` expression.+The `match` expression returns only the evaluation result of the first pattern-matching result. +```+match [1,2,5,9,4] (Multiset Integer) [[mc| cons $x (cons #(x+1) _) => x|]]+-- 1+```++The `match` expression is simply implemented using `matchAll` as follows:++```+match tgt m cs = head $ matchAll tgt m cs+```+ ### `matchAllDFS` and `matchDFS` -preparing...+The `matchAll` and `match` expressions traverse a search tree for pattern matching in breadth-first order.+The reason of the default breadth-first traversal is because to enumerate all the successful pattern-matching results even when they are infinitely many.+For example, all the pairs of natural numbers can be enumerated by the following `matchAll` expression:++```+take 10 (matchAll [1..] (Set Integer)+           [[mc| cons $x (cons $y _) => (x, y) |]])+-- [(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(1,4),(2,3),(3,2),(4,1)]+```++If we change the above `matchAll` to `matchAllDFS`, the order of the pattern-matching results changes as follows:++```+take 10 (matchAllDFS [1..] (Set Integer)+           [[mc| cons $x (cons $y _) => (x, y) |]])+-- [(1,1),(1,2),(1,3),(1,4),(1,5),(1,6),(1,7),(1,8),(1,9),(1,10)]+```++There are cases where depth-first traversal is suitable because the depth-first order of pattern-matching results is preferable.+Furthermore, `matchAllDFS` is more efficient than `matchAll`.+It would be better to use `matchAllDFS` instead of `matchAll` when the both expressions can be used.++### Matcher definitions++preparing++```+matchAll (1,2) UnorderedEqlPair [[mc| uepair #2 $x => x |]]+-- [1]+matchAll (1,2) (UnorderedPair Eql) [[mc| upair #2 $x => x |]]+-- [1]+```++```+data UnorderedEqlPair = UnorderedEqlPair+instance (Eq a) => Matcher UnorderedEqlPair (a, a)++uepair :: (Eq a)+       => Pattern a Eql ctx xs+       -> Pattern a Eql (ctx :++: xs) ys+       -> Pattern (a, a) UnorderedEqlPair ctx (xs :++: ys)+uepair p1 p2 = Pattern (\_ UnorderedEqlPair (t1, t2) ->+                          [twoMAtoms (MAtom p1 Eql t1) (MAtom p2 Eql t2)+                          ,twoMAtoms (MAtom p1 Eql t2) (MAtom p2 Eql t1)])+```++```+data UnorderedPair m = UnorderedPair m+instance Matcher m a => Matcher (UnorderedPair m) (a, a)++upair :: (Matcher m a , a ~ (b, b), m ~ (UnorderedPair m'), Matcher m' b)+      => Pattern b m' ctx xs+      -> Pattern b m' (ctx :++: xs) ys+      -> Pattern a m ctx (xs :++: ys)+upair p1 p2 = Pattern (\_ (UnorderedPair m') (t1, t2) ->+                         [twoMAtoms (MAtom p1 m' t1) (MAtom p2 m' t2)+                         ,twoMAtoms (MAtom p1 m' t2) (MAtom p2 m' t1)])+```  ## Samples 

@@ -1,7 +1,7 @@ cabal-version: 1.12  name:           mini-egison-version:        0.1.1+version:        0.1.2 synopsis:    Template Haskell Implementation of Egison Pattern Matching description: This package provides the pattern-matching facility that fulfills the following three criteria for practical pattern matching for non-free data types\: (i) non-linear pattern matching with backtracking; (ii) extensibility of pattern-matching algorithms; (iii) ad-hoc polymorphism of patterns.   Non-free data types are data types whose data have no standard forms.@@ -44,7 +44,8 @@     , regex-compat     , template-haskell   default-language: Haskell2010-+  ghc-options:  -O3+   test-suite mini-egison-test   type: exitcode-stdio-1.0   main-is: Test.hs@@ -53,10 +54,20 @@       Paths_mini_egison   hs-source-dirs:       test-  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  ghc-options: -O3   build-depends:       base >=4.7 && <5     , mini-egison     , hspec     , primes   default-language: Haskell2010++Executable cdcl+  Main-is:             cdcl.hs+  Build-depends:+      base >=4.7 && <5+    , mini-egison+    , sort+  Hs-Source-Dirs:      sample+  default-language: Haskell2010+  ghc-options:  -O3

@@ -0,0 +1,202 @@+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE QuasiQuotes           #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE TypeOperators         #-}++import           Data.List+import           Data.Sort+import           Control.Egison hiding (Integer)+import qualified Control.Egison as M+import           Debug.Trace++++-- Literal matcher = Integer matcher+data Literal = Literal+instance Integral a => Matcher Literal a++instance Integral a => ValuePat Literal a where+  valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])++-- Stage matcher = Integer matcher+data Stage = Stage+instance Integral a => Matcher Stage a++instance Integral a => ValuePat Stage a where+  valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])++-- Matchers for assignments+type TaggedLiteral = (Integer, Integer) -- a tuple of a variable and a stage++data Assign = Deduced TaggedLiteral [TaggedLiteral]+            | Guessed TaggedLiteral+  deriving (Show)++data Assignment = Assignment+instance Matcher Assignment Assign++deduced :: Pattern TaggedLiteral (Pair Literal Stage) ctx xs+        -> Pattern [TaggedLiteral] (Multiset (Pair Literal Stage)) (ctx :++: xs) ys+        -> Pattern Assign Assignment ctx (xs :++: ys)+deduced p1 p2 = Pattern (\_ _ tgt -> case tgt of+                                       Deduced l ls -> [twoMAtoms (MAtom p1 (Pair Literal Stage) l)+                                                                  (MAtom p2 (Multiset (Pair Literal Stage)) ls)]+                                       _ -> [])++guessed :: Pattern TaggedLiteral (Pair Literal Stage) ctx xs+        -> Pattern Assign Assignment ctx xs+guessed p1 = Pattern (\_ _ tgt -> case tgt of+                                    Guessed l -> [oneMAtom (MAtom p1 (Pair Literal Stage) l)]+                                    _ -> [])++whichever :: Pattern TaggedLiteral (Pair Literal Stage) ctx xs+          -> Pattern Assign Assignment ctx xs+whichever p1 = Pattern (\_ _ tgt -> case tgt of+                                      Deduced l _ -> [oneMAtom (MAtom p1 (Pair Literal Stage) l)]+                                      Guessed l -> [oneMAtom (MAtom p1 (Pair Literal Stage) l)])++--+-- VSIDS+--+toCNF :: [[Integer]] -> [([Integer], [Integer])]+toCNF cs = map (\c -> (c, c)) cs++fromCNF ::  [([Integer], [Integer])] -> [[Integer]]+fromCNF cnf = map (\(c1, _) -> c1) cnf++initVars :: [Integer] -> [(Integer, Integer)]+initVars vs = map (\v -> (negate v, 0)) vs ++ map (\v -> (v, 0)) vs++addVars :: [Integer] -> [(Integer, Integer)] -> [(Integer, Integer)]+addVars vs vars =+  matchDFS (vs, vars) (Pair (List Literal) (List (Pair Literal M.Integer)))+    [[mc| pair nil _ => sortBy (\(_, c1) (_, c2) -> opposite (compare c1 c2)) vars |],+     [mc| pair (cons $v $vs2) (join $hs (cons (pair #v $c) $ts)) =>+          addVars vs2 (hs ++ (v, c + 1) : ts) |]]+ where+   opposite LT = GT+   opposite GT = LT+   opposite EQ = EQ++deleteVar :: Integer -> [(Integer, Integer)] -> [(Integer, Integer)]+deleteVar v vars =+  matchDFS vars (Multiset (Pair Literal M.Integer))+    [[mc| cons (pair #v _) (cons (pair #(negate v) _) $vars2) => vars2 |]]++--+-- Utility functions for literals and cnfs+--+getStage :: Integer -> [Assign] -> Integer+getStage l trail =+  matchDFS trail (List Assignment)+    [[mc| join _ (cons (whichever (pair #(negate l) $s)) _) => s |]]++deleteLiteral :: Integer -> [([Integer], [Integer])] -> [([Integer], [Integer])]+deleteLiteral l cnf =+  map (\(c1, c2) -> (matchAll c1 (Multiset Literal)+                       [[mc| cons (& (not #l) $m) _ => m |]],+                     c2))+      cnf++deleteClausesWith :: Integer -> [([Integer], [Integer])] -> [([Integer], [Integer])]+deleteClausesWith l cnf =+  matchAll cnf (Multiset (Pair (Multiset Literal) (Multiset Literal)))+    [[mc| cons (& (pair (not (cons #l _)) _) $c) _ => c |]]++assignTrue :: Integer -> [([Integer], [Integer])] -> [([Integer], [Integer])]+assignTrue l cnf =+  deleteLiteral (negate l) (deleteClausesWith l cnf)++--+-- Unit propagation+--+unitPropagate :: Integer -> [([Integer], [Integer])] -> [Assign] -> ([([Integer], [Integer])], [Assign])+unitPropagate stage cnf trail = unitPropagate' stage cnf trail trail++unitPropagate' :: Integer -> [([Integer], [Integer])] -> [Assign] -> [Assign] -> ([([Integer], [Integer])], [Assign])+unitPropagate' stage cnf trail otrail =+  matchDFS trail (List Assignment)+    [[mc| cons (whichever (pair $l _)) $trail2 => unitPropagate' stage (assignTrue l cnf) trail2 otrail |],+     [mc| _ => unitPropagate'' stage cnf otrail |]]+   +unitPropagate'' :: Integer -> [([Integer], [Integer])] -> [Assign] -> ([([Integer], [Integer])], [Assign])+unitPropagate'' stage cnf trail =+  matchDFS cnf (Multiset (Pair (Multiset Literal) (Multiset Literal)))+    [[mc| cons (pair nil _) _ => (cnf, trail) |],+     [mc| cons (pair (cons $l nil) (cons #l $rs)) _ =>+          unitPropagate'' stage (assignTrue l cnf) +                          ([(Deduced (l, stage) (map (\r -> (r, (getStage r trail))) rs))] ++ trail) |],+     [mc| _ => (cnf, trail) |]]++--+-- Learning+--++learn :: Integer -> [(Integer, Integer)] -> [Assign] -> (Integer, [Integer])+learn stage cl trail =+  matchDFS (trail, cl) (Pair (List Assignment) (Multiset (Pair Literal M.Integer))) -- must be matchDFS+    [[mc| pair _ (not (cons (pair _ #stage) (cons (pair _ #stage) _))) =>+          (minimum (map (\(_, c) -> c) cl), map (\(l, _) -> l) cl) |],+     [mc| pair (join _ (cons (deduced (pair $l #stage) $ds) $trail2))+               (cons (pair #(negate l) #stage) $rs) =>+          learn stage (union rs ds) trail2 |]]++--+-- Backjumping+--++backjump :: Integer -> [Assign] -> [Assign]+backjump stage trail =+  matchDFS trail (List Assignment)+    [[mc| join _ (& (cons (guessed (pair _ #stage)) _) $trail2) => trail2 |],+     [mc| _ => [] |]]++--+-- Guess+--++guess vars trail =+  matchDFS (vars, trail) (Pair (List (Pair Literal M.Integer)) (List Assignment)) -- must be matchDFS+    [[mc| pair (join _ (cons (pair $l _) _))+               (not (join _ (cons (whichever (pair (| #l #(negate l)) _)) _))) =>+          negate l |]]++--+-- CDCL main+--++cdcl :: [Integer] -> [[Integer]] -> Bool+cdcl vars cnf = cdcl' 0 0 (initVars vars) (toCNF cnf) []++cdcl' :: Integer -> Integer -> [(Integer, Integer)] -> [([Integer], [Integer])] -> [Assign] -> Bool+cdcl' count stage vars cnf trail =+  let (cnf2, trail2) = unitPropagate stage cnf trail in+--  let (cnf2, trail2) = unitPropagate stage cnf (trace (show trail) trail) in -- debug+    matchDFS (cnf2, trail2) (Pair (Multiset (Pair (Multiset Literal) (Multiset Literal))) (List Assignment))+      [[mc| pair nil _ => True |],+       [mc| pair (cons (pair nil $cc) _) (join _ (cons (guessed (pair $l #stage)) $trail3)) =>+            let (s, lc) = learn stage (map (\l -> (l, (getStage l trail2))) cc) trail2 in+            let trail4 = backjump s trail3 in+              cdcl' (count + 1) s (addVars lc vars) ((lc, lc):cnf) trail4 |],+       [mc| pair (cons (pair nil $cc) _) _ => False |],+       [mc| _ =>+            let g = guess vars trail2 in+              cdcl' (count + 1) (stage + 1) vars cnf (Guessed (g, stage + 1):trail2) |]]++main = do+--  putStrLn $ show $ cdcl [] []+--  putStrLn $ show $ cdcl [] [[]]+--  putStrLn $ show $ cdcl [1] [[1]]+--  putStrLn $ show $ cdcl [1,2] [[1],[1,2]]+--  putStrLn $ "Problem 20"+--  putStrLn $ show $ cdcl [1..20] problem20 -- 0.293 sec+  putStrLn $ "Problem 50"+  putStrLn $ show $ cdcl [1..50] problem50 -- 2.570 sec++problem20 =+  [[4,-18,19],[3,18,-5],[-5,-8,-15],[-20,7,-16],[10,-13,-7],[-12,-9,17],[17,19,5],[-16,9,15],[11,-5,-14],[18,-10,13],[-3,11,12],[-6,-17,-8],[-18,14,1],[-19,-15,10],[12,18,-19],[-8,4,7],[-8,-9,4],[7,17,-15],[12,-7,-14],[-10,-11,8],[2,-15,-11],[9,6,1],[-11,20,-17],[9,-15,13],[12,-7,-17],[-18,-2,20],[20,12,4],[19,11,14],[-16,18,-4],[-1,-17,-19],[-13,15,10],[-12,-14,-13],[12,-14,-7],[-7,16,10],[6,10,7],[20,14,-16],[-19,17,11],[-7,1,-20],[-5,12,15],[-4,-9,-13],[12,-11,-7],[-5,19,-8],[1,16,17],[20,-14,-15],[13,-4,10],[14,7,10],[-5,9,20],[10,1,-19],[-16,-15,-1],[16,3,-11],[-15,-10,4],[4,-15,-3],[-10,-16,11],[-8,12,-5],[14,-6,12],[1,6,11],[-13,-5,-1],[-7,-2,12],[1,-20,19],[-2,-13,-8],[15,18,4],[-11,14,9],[-6,-15,-2],[5,-12,-15],[-6,17,5],[-13,5,-19],[20,-1,14],[9,-17,15],[-5,19,-18],[-12,8,-10],[-18,14,-4],[15,-9,13],[9,-5,-1],[10,-19,-14],[20,9,4],[-9,-2,19],[-5,13,-17],[2,-10,-18],[-18,3,11],[7,-9,17],[-15,-6,-3],[-2,3,-13],[12,3,-2],[-2,-3,17],[20,-15,-16],[-5,-17,-19],[-20,-18,11],[-9,1,-5],[-19,9,17],[12,-2,17],[4,-16,-5]]++problem50 =+  [[18,-8,29],[-16,3,18],[-36,-11,-30],[-50,20,32],[-6,9,35],[42,-38,29],[43,-15,10],[-48,-47,1],[-45,-16,33],[38,42,22],[-49,41,-34],[12,17,35],[22,-49,7],[-10,-11,-39],[-28,-36,-37],[-13,-46,-41],[21,-4,9],[12,48,10],[24,23,15],[-8,-41,-43],[-44,-2,-35],[-27,18,31],[47,35,6],[-11,-27,41],[-33,-47,-45],[-16,36,-37],[27,-46,2],[15,-28,10],[-38,46,-39],[-33,-4,24],[-12,-45,50],[-32,-21,-15],[8,42,24],[30,-49,4],[45,-9,28],[-33,-47,-1],[1,27,-16],[-11,-17,-35],[-42,-15,45],[-19,-27,30],[3,28,12],[48,-11,-33],[-6,37,-9],[-37,13,-7],[-2,26,16],[46,-24,-38],[-13,-24,-8],[-36,-42,-21],[-37,-19,3],[-31,-50,35],[-7,-26,29],[-42,-45,29],[33,25,-6],[-45,-5,7],[-7,28,-6],[-48,31,-11],[32,16,-37],[-24,48,1],[18,-46,23],[-30,-50,48],[-21,39,-2],[24,47,42],[-36,30,4],[-5,28,-1],[-47,32,-42],[16,37,-22],[-43,42,-34],[-40,39,-20],[-49,29,6],[-41,-3,39],[-16,-12,43],[24,22,3],[47,-45,43],[45,-37,46],[-9,26,5],[-3,23,-13],[5,-34,13],[12,39,13],[22,50,37],[19,9,46],[-24,8,-27],[-28,7,21],[8,-25,50],[20,50,4],[27,36,13],[26,31,-25],[39,-44,-32],[-20,41,-10],[49,-28,35],[1,44,34],[39,35,-11],[-50,-42,-7],[-24,7,47],[-13,5,-48],[-9,-20,-23],[2,17,-19],[11,23,21],[-45,30,15],[11,26,-24],[38,33,-13],[44,-27,-7],[41,49,2],[-18,12,-37],[-2,12,-26],[-19,7,32],[-22,11,33],[8,12,-20],[16,40,-48],[-2,-24,-11],[26,-17,37],[-14,-19,46],[5,47,36],[-29,-9,19],[32,4,28],[-34,20,-46],[-4,-36,-13],[-15,-37,45],[-21,29,23],[-6,-40,7],[-42,31,-29],[-36,24,31],[-45,-37,-1],[3,-6,-29],[-28,-50,27],[44,26,5],[-17,-48,49],[12,-40,-7],[-12,31,-48],[27,32,-42],[-27,-10,1],[6,-49,10],[-24,8,43],[23,31,1],[11,-47,38],[-28,26,-13],[-40,12,-42],[-3,39,46],[17,41,46],[23,21,13],[-14,-1,-38],[20,18,6],[-50,20,-9],[10,-32,-18],[-21,49,-34],[44,23,-35],[40,-19,34],[-1,6,-12],[6,-2,-7],[32,-20,34],[-12,43,-29],[24,2,-49],[10,-4,40],[11,5,12],[-3,47,-31],[43,-23,21],[-41,-36,-50],[-8,-42,-24],[39,45,7],[7,37,-45],[41,40,8],[-50,-10,-8],[-5,-39,-14],[-22,-24,-43],[-36,40,35],[17,49,41],[-32,7,24],[-30,-8,-9],[-41,-13,-10],[31,26,-33],[17,-22,-39],[-21,28,3],[-14,46,23],[29,16,19],[42,-32,-44],[-24,10,23],[-1,-32,-21],[-8,-44,-39],[39,11,9],[19,14,-46],[46,44,-42],[37,23,-29],[32,25,20],[14,-43,-12],[-36,-18,46],[14,-26,-10],[-2,-30,5],[6,-18,46],[-26,2,-44],[20,-8,-11],[-31,3,16],[-22,-9,39],[-49,44,-42],[-45,-44,31],[-31,50,-11],[-32,-46,2],[-6,-7,17],[19,-32,48],[39,20,-10],[-22,-37,38],[-31,9,-48],[40,12,7],[-24,-4,9],[-22,49,33],[-12,43,10],[25,-30,-10],[46,47,31],[13,27,-7],[-45,32,-35],[-50,34,9],[2,34,30],[3,16,2],[-18,45,-12],[33,37,10],[43,7,-18],[-22,44,-19],[-31,-27,-42],[-3,-40,8],[-23,-31,38]]

@@ -14,13 +14,20 @@   MState(..),   MAtom(..),   MList(..),+  mappend,+  oneMAtom,+  twoMAtoms,+  threeMAtoms,   -- Heterogeneous list   HList(..),   happend,   (:++:),   ) where +import           Prelude hiding (mappend) import           Data.Maybe+import           Data.Type.Equality+import           Unsafe.Coerce  --- --- Pattern@@ -38,11 +45,11 @@   NotPat :: Pattern a m ctx '[] -> Pattern a m ctx '[]   PredicatePat :: (HList ctx -> a -> Bool) -> Pattern a m ctx '[]   -- User-defined pattern; pattern is a function that takes a target, an intermediate pattern-matching result, and a matcher and returns a list of lists of matching atoms.-  Pattern :: Matcher m => (HList ctx -> m -> a -> [MList ctx vs]) -> Pattern a m ctx vs+  Pattern :: Matcher m a => (HList ctx -> m -> a -> [MList ctx vs]) -> Pattern a m ctx vs -class Matcher a+class Matcher m a -data MatchClause a m b = forall vs. (Matcher m) => MatchClause (Pattern a m '[] vs) (HList vs -> b)+data MatchClause a m b = forall vs. (Matcher m a) => MatchClause (Pattern a m '[] vs) (HList vs -> b)  --- --- Matching state@@ -54,7 +61,7 @@ -- matching atom -- ctx: intermediate pattern-matching results -- vs: list of types bound to the pattern variables in the pattern.-data MAtom ctx vs = forall a m. (Matcher m) => MAtom (Pattern a m ctx vs) m a+data MAtom ctx vs = forall a m. (Matcher m a) => MAtom (Pattern a m ctx vs) m a  -- stack of matching atoms data MList ctx vs where@@ -62,6 +69,24 @@   MCons :: MAtom ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys)   MJoin :: MList ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys) +mappend :: MList ctx xs -> MList (ctx :++: xs) ys -> MList ctx (xs :++: ys)+mappend MNil atoms = atoms+mappend (MCons atom atoms1) atoms2 =+  case mconsAssocProof atom atoms1 of+    Refl -> case mappendAssocProof atom atoms1 atoms2 of+      Refl -> MCons atom (mappend atoms1 atoms2)++oneMAtom :: MAtom ctx xs -> MList ctx xs+oneMAtom atom1 = MCons atom1 MNil++twoMAtoms :: MAtom ctx xs -> MAtom (ctx :++: xs) ys -> MList ctx (xs :++: ys)+twoMAtoms atom1 atom2 = MCons atom1 (MCons atom2 MNil)++threeMAtoms :: MAtom ctx xs -> MAtom (ctx :++: xs) ys -> MAtom (ctx :++: xs :++: ys) zs -> MList ctx (xs :++: ys :++: zs)+threeMAtoms atom1 atom2 atom3 =+  case threeMConsAssocProof atom1 atom2 atom3 of+    Refl -> MCons atom1 (MCons atom2 (MCons atom3 MNil))+ --- --- Heterogeneous list ---@@ -70,19 +95,25 @@   HNil :: HList '[]   HCons :: a -> HList as -> HList (a ': as) +type family (as ::[*]) :++: (bs :: [*]) :: [*] where+  as :++: '[] = as+  '[] :++: bs = bs+  (a ': as) :++: bs = a ': (as :++: bs)+ happend :: HList as -> HList bs -> HList (as :++: bs)-happend (HCons x xs) ys = case proof x xs ys of Refl -> HCons x $ happend xs ys happend HNil ys         = ys+happend xs@(HCons x xs') ys = case hconsAssocProof x xs' ys of+                                Refl -> HCons x $ happend xs' ys -type family as :++: bs :: [*] where-  bs :++: '[] = bs-  '[] :++: bs = bs-  (a ': as) :++: bs = a ': (as :++: bs)+hconsAssocProof :: a -> HList as -> HList bs -> ((a ': as) :++: bs) :~: (a ': (as :++: bs))+hconsAssocProof _ _ HNil = Refl+hconsAssocProof x xs (HCons y ys) = Refl -data (a :: [*]) :~: (b :: [*]) where-  Refl :: a :~: a+mconsAssocProof :: MAtom ctx vs -> MList (ctx :++: vs) vs' -> (ctx :++: (vs :++: vs')) :~: ((ctx :++: vs) :++: vs')+mconsAssocProof _ _ = unsafeCoerce Refl -- Todo: Write proof. -proof :: a -> HList as -> HList bs -> ((a ': as) :++: bs) :~: (a ': (as :++: bs))-proof _ _ HNil = Refl-proof x xs (HCons y ys) = Refl+mappendAssocProof :: MAtom ctx xs -> MList (ctx :++: xs) ys ->  MList (ctx :++: xs :++: ys) zs -> (xs :++: (ys :++: zs)) :~: ((xs :++: ys) :++: zs)+mappendAssocProof _ _ _ = unsafeCoerce Refl -- Todo: Write proof. +threeMConsAssocProof :: MAtom ctx xs -> MAtom (ctx :++: xs) ys -> MAtom (ctx :++: xs :++: ys) zs -> (xs :++: ys :++: zs) :~: (xs :++: (ys :++: zs))+threeMConsAssocProof _ _ _ = unsafeCoerce Refl -- Todo: Write proof.

@@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs     #-}+{-# LANGUAGE TypeOperators             #-}  module Control.Egison.Match (   matchAll,@@ -8,25 +9,27 @@   matchDFS,   ) where +import           Prelude hiding (mappend) import           Control.Egison.Core import           Unsafe.Coerce+import           Data.Type.Equality -matchAll :: (Matcher m) => a -> m -> [MatchClause a m b] -> [b]+matchAll :: (Matcher m a) => a -> m -> [MatchClause a m b] -> [b] matchAll tgt m [] = [] matchAll tgt m ((MatchClause pat f):cs) =   let results = processMStatesAll [[MState HNil (MCons (MAtom pat m tgt) MNil)]] in   map f results ++ matchAll tgt m cs -match :: (Matcher m) => a -> m -> [MatchClause a m b] -> b+match :: (Matcher m a) => a -> m -> [MatchClause a m b] -> b match tgt m cs = head $ matchAll tgt m cs -matchAllDFS :: (Matcher m) => a -> m -> [MatchClause a m b] -> [b]+matchAllDFS :: (Matcher m a) => a -> m -> [MatchClause a m b] -> [b] matchAllDFS tgt m [] = [] matchAllDFS tgt m ((MatchClause pat f):cs) =   let results = processMStatesAllDFS [MState HNil (MCons (MAtom pat m tgt) MNil)] in   map f results ++ matchAllDFS tgt m cs -matchDFS :: (Matcher m) => a -> m -> [MatchClause a m b] -> b+matchDFS :: (Matcher m a) => a -> m -> [MatchClause a m b] -> b matchDFS tgt m cs = head $ matchAllDFS tgt m cs  --@@ -62,19 +65,27 @@   case pat of     Pattern f ->       let matomss = f rs m tgt in-      map (\newAtoms -> MState rs (MJoin newAtoms atoms)) matomss+      map (\newAtoms -> MState rs (mappend newAtoms atoms)) matomss     Wildcard -> [MState rs atoms]-    PatVar _ -> [unsafeCoerce $ MState (happend rs (HCons tgt HNil)) atoms]+    PatVar _ -> case patVarProof rs (HCons tgt HNil) atoms of+                  Refl -> [MState (happend rs (HCons tgt HNil)) atoms]     AndPat p1 p2 ->-      [unsafeCoerce $ MState rs (MCons (MAtom p1 m tgt) (MCons (MAtom p2 m tgt) $ unsafeCoerce atoms))]+      case (assocProof (MAtom p1 m tgt) (MAtom p2 m tgt)) of+        Refl -> case (andPatProof (MAtom p1 m tgt) (MAtom p2 m tgt) atoms) of+          Refl -> [MState rs (MCons (MAtom p1 m tgt) (MCons (MAtom p2 m tgt) $ atoms))]     OrPat p1 p2 ->       [MState rs (MCons (MAtom p1 m tgt) atoms), MState rs (MCons (MAtom p2 m tgt) atoms)]     NotPat p ->       [MState rs atoms | null $ processMStatesAll [[MState rs $ MCons (MAtom p m tgt) MNil]]]     PredicatePat f -> [MState rs atoms | f rs tgt]-processMState (MState rs (MJoin MNil matoms2)) = processMState (MState rs matoms2)-processMState (MState rs (MJoin matoms1 matoms2)) =-  let mstates = processMState (MState rs matoms1) in-  map (\(MState rs' ms) -> unsafeCoerce $ MState rs' $ MJoin ms matoms2) mstates processMState (MState rs MNil) = [MState rs MNil] -- TODO: shold not reach here but reaches here. +patVarProof :: HList xs -> HList '[a] -> MList (xs :++: '[a]) ys -> ((xs :++: '[a]) :++: ys) :~: (xs :++: ('[a] :++: ys))+patVarProof HNil _ _ = Refl+patVarProof (HCons _ xs) ys zs = unsafeCoerce Refl -- Todo: Write proof.++andPatProof :: MAtom ctx vs -> MAtom (ctx :++: vs) vs' -> MList (ctx :++: vs :++: vs') ys -> (ctx :++: ((vs :++: vs') :++: ys)) :~: (ctx :++: (vs :++: (vs' :++: ys)))+andPatProof _ _ _ = unsafeCoerce Refl -- Todo: Write proof.++assocProof :: MAtom ctx vs -> MAtom (ctx :++: vs) vs' -> (ctx :++: (vs :++: vs')) :~: ((ctx :++: vs) :++: vs')+assocProof _ _ = unsafeCoerce Refl -- Todo: Write proof.

@@ -23,6 +23,7 @@   ) where  import           Prelude hiding (Integer)+import           Data.List (tails) import           Control.Egison.Core import           Control.Egison.Match import           Control.Egison.QQ@@ -32,25 +33,25 @@ --  data Something = Something-instance Matcher Something+instance Matcher Something a  -- -- Eql and Integer matchers --  class ValuePat m a where-  valuePat :: (Matcher m, Eq a) => (HList ctx -> a) -> Pattern a m ctx '[]+  valuePat :: (Matcher m a, Eq a) => (HList ctx -> a) -> Pattern a m ctx '[]  -- Eql matcher data Eql = Eql-instance Matcher Eql+instance Matcher Eql a  instance Eq a => ValuePat Eql a where   valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])  -- Integer matcher data Integer = Integer-instance Matcher Integer+instance Integral a => Matcher Integer a  instance Integral a => ValuePat Integer a where   valuePat f = Pattern (\ctx _ tgt -> [MNil | f ctx == tgt])@@ -59,75 +60,85 @@ --- Pair matcher --- -data Pair a b = Pair a b-instance (Matcher a, Matcher b) => Matcher (Pair a b)+data Pair m1 m2 = Pair m1 m2+instance (Matcher m1 a1, Matcher m2 a2) => Matcher (Pair m1 m2) (a1, a2)  class PairPat m a where-  pair :: (Matcher m, a ~ (b1, b2), m ~ (Pair m1 m2)) => Pattern b1 m1 ctx xs -> Pattern b2 m2 (ctx :++: xs) ys -> Pattern a m ctx (xs :++: ys)+  pair :: (Matcher m a , a ~ (b1, b2), m ~ (Pair m1 m2))+       => Pattern b1 m1 ctx xs+       -> Pattern b2 m2 (ctx :++: xs) ys+       -> Pattern a m ctx (xs :++: ys) -instance (Matcher m1, Matcher m2) => PairPat (Pair m1 m2) (a1, a2) where-  pair p1 p2 = Pattern (\_ (Pair m1 m2) (t1, t2) -> [MCons (MAtom p1 m1 t1) $ MCons (MAtom p2 m2 t2) MNil])+instance (Matcher m1 a1, Matcher m2 a2) => PairPat (Pair m1 m2) (a1, a2) where+  pair p1 p2 = Pattern (\_ (Pair m1 m2) (t1, t2) -> [twoMAtoms (MAtom p1 m1 t1) (MAtom p2 m2 t2)])  --- --- Matchers for collections ---  class CollectionPat m a where-  nil  :: (Matcher m, a ~ [a']) => Pattern a m ctx '[]-  cons :: (Matcher m, a ~ [a'], m ~ (f m')) => Pattern a' m' ctx xs -> Pattern a m (ctx :++: xs) ys -> Pattern a m ctx (xs :++: ys)-  join :: (Matcher m, a ~ [a']) => Pattern a m ctx xs -> Pattern a m (ctx :++: xs) ys -> Pattern a m ctx (xs :++: ys)+  nil  :: (Matcher m a) => Pattern a m ctx '[]+  cons :: (Matcher m a, a ~ [a'], m ~ (f m'))+       => Pattern a' m' ctx xs+       -> Pattern a m (ctx :++: xs) ys+       -> Pattern a m ctx (xs :++: ys)+  join :: (Matcher m a)+       => Pattern a m ctx xs+       -> Pattern a m (ctx :++: xs) ys+       -> Pattern a m ctx (xs :++: ys)  -- List matcher-newtype List a = List a-instance (Matcher a) => Matcher (List a)+newtype List m = List m+instance (Matcher m a) => Matcher (List m) [a] -instance (Matcher m, Eq a, ValuePat m a) => ValuePat (List m) [a] where+instance (Matcher m a, Eq a, ValuePat m a) => ValuePat (List m) [a] where   valuePat f = Pattern (\ctx (List m) tgt ->                             match (f ctx, tgt) (Pair (List m) (List m)) $                               [[mc| pair nil nil => [MNil] |],                                [mc| pair (cons $x $xs) (cons #x #xs) => [MNil] |],                                [mc| Wildcard => [] |]]) -instance Matcher m => CollectionPat (List m) [a] where+instance Matcher m a => CollectionPat (List m) [a] where   nil = Pattern (\_ _ t -> [MNil | null t])   cons p1 p2 = Pattern (\_ (List m) tgt ->                               case tgt of                                 [] -> []-                                x:xs -> [MCons (MAtom p1 m x) $ MCons (MAtom p2 (List m) xs) MNil])-  join p1 p2 = Pattern (\_ m tgt -> map (\(hs, ts) -> MCons (MAtom p1 m hs) $ MCons (MAtom p2 m ts) MNil) (splits tgt))+                                x:xs -> [twoMAtoms (MAtom p1 m x) (MAtom p2 (List m) xs)])+  join Wildcard p2 = Pattern (\_ m tgt -> map (\ts -> oneMAtom (MAtom p2 m ts)) (tails tgt))+  join p1 p2 = Pattern (\_ m tgt -> map (\(hs, ts) -> twoMAtoms (MAtom p1 m hs) (MAtom p2 m ts)) (splits tgt))  splits :: [a] -> [([a], [a])] splits []     = [([], [])] splits (x:xs) = ([], x:xs) : [(x:ys, zs) | (ys, zs) <- splits xs]  -- Multiset matcher-newtype Multiset a = Multiset a-instance (Matcher a) => Matcher (Multiset a)+newtype Multiset m = Multiset m+instance (Matcher m a) => Matcher (Multiset m) [a] -instance (Matcher m, Eq a, ValuePat m a) => ValuePat (Multiset m) [a] where+instance (Matcher m a, Eq a, ValuePat m a) => ValuePat (Multiset m) [a] where   valuePat f = Pattern (\ctx (Multiset m) tgt ->                             match (f ctx, tgt) (Pair (List m) (Multiset m)) $                               [[mc| pair nil nil => [MNil] |],                                [mc| pair (cons $x $xs) (cons #x #xs) => [MNil] |],                                [mc| Wildcard => [] |]]) -instance (Matcher m) => CollectionPat (Multiset m) [a] where+instance (Matcher m a) => CollectionPat (Multiset m) [a] where   nil = Pattern (\_ _ tgt -> [MNil | null tgt])-  cons p Wildcard = Pattern (\_ (Multiset m) tgt -> map (\x -> MCons (MAtom p m x) MNil) tgt)-  cons p1 p2 = Pattern (\_ (Multiset m) tgt -> map (\(x, xs) -> MCons (MAtom p1 m x) $ MCons (MAtom p2 (Multiset m) xs) MNil)+  cons p Wildcard = Pattern (\_ (Multiset m) tgt -> map (\x -> oneMAtom (MAtom p m x)) tgt)+  cons p1 p2 = Pattern (\_ (Multiset m) tgt -> map (\(x, xs) -> twoMAtoms (MAtom p1 m x) (MAtom p2 (Multiset m) xs))                                                    (matchAll tgt (List m) [[mc| join $hs (cons $x $ts) => (x, hs ++ ts) |]]))   join p1 p2 = undefined  -- Set matcher-newtype Set a = Set a-instance (Matcher a) => Matcher (Set a)+newtype Set m = Set m+instance (Matcher m a) => Matcher (Set m) [a] -instance (Matcher m, Eq a,  Ord a, ValuePat m a) => ValuePat (Set m) [a] where+instance (Matcher m a, Eq a,  Ord a, ValuePat m a) => ValuePat (Set m) [a] where   valuePat f = undefined -instance Matcher m => CollectionPat (Set m) [a] where+instance Matcher m a => CollectionPat (Set m) [a] where   nil = Pattern (\_ _ tgt -> [MNil | null tgt])   cons p1 p2 = Pattern (\_ (Set m) tgt ->-                  map (\x -> MCons (MAtom p1 m x) $ MCons (MAtom p2 (Set m) tgt) MNil)+                  map (\x -> twoMAtoms (MAtom p1 m x) (MAtom p2 (Set m) tgt))                       (matchAll tgt (List m) [[mc| join Wildcard (cons $x Wildcard) => x |]]))   join p1 p2 = undefined

@@ -53,11 +53,26 @@          [mc| _ => "Not matched" |]]       `shouldBe` "Matched" +--    it "test" $+--      match 1 (List Integer)+--        [[mc| $x => "Matched" |]]+--      `shouldBe` "Matched"+   describe "match-all with infinitely many results" $ do-    it "Check the order of pattern-matching results" $+    it "Check the order of pattern-matching results (multiset bfs) " $       take 10 (matchAll [1..] (Multiset Integer)                  [[mc| cons $x (cons $y _) => (x, y) |]])       `shouldBe` [(1,2),(1,3),(2,1),(1,4),(2,3),(3,1),(1,5),(2,4),(3,2),(4,1)]++    it "Check the order of pattern-matching results (set bfs)" $+      take 10 (matchAll [1..] (Set Integer)+                 [[mc| cons $x (cons $y _) => (x, y) |]])+      `shouldBe` [(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(1,4),(2,3),(3,2),(4,1)]++    it "Check the order of pattern-matching results (set dfs)" $+      take 10 (matchAllDFS [1..] (Set Integer)+                 [[mc| cons $x (cons $y _) => (x, y) |]])+      `shouldBe` [(1,1),(1,2),(1,3),(1,4),(1,5),(1,6),(1,7),(1,8),(1,9),(1,10)]    describe "built-in pattern constructs" $ do     it "Predicate patterns" $