ラムゼーの有名なやつ in Idris, Egison

ramsey-N.egi

;; > egison -N
;; > loadFile("ramsey-N.egi")


in0 = matchAll 4..6 as multiset(integer)
  | $xs <++> $ys -> [xs, ys]

inputRed = map2(
  append,
  map(($xs -> [append(nth(1, xs), 1..3), nth(2, xs)]), in0),
  map(($x -> [[x]]), 100..107)
               )
inputBlue = map2(
  append,
  map(($xs -> [nth(1, xs), append(nth(2, xs), 1..3)]), in0),
  map(($x -> [[x]]), 100..107)
                )

;; 100~107が出力されたらOK!
output(input) = matchAll input as multiset(multiset(multiset(integer)))
  | ( ( ((4 <:> 5 <:> 6 <:> _)
      or (4 <:> 1 <:> 2 <:> _)
      or (5 <:> 2 <:> 3 <:> _)
      or (6 <:> 3 <:> 1 <:> _)) and $xs)
      <:> ((((100 <:> <nil>)
          or (101 <:> <nil>)
          or (102 <:> <nil>)
          or (103 <:> <nil>)
          or (104 <:> <nil>)
          or (105 <:> <nil>)
          or (106 <:> <nil>)
          or (107 <:> <nil>)) and $y) <:> _))
    <:> _ -> (xs, y)


;; C:\me\Egison\ramsey>egison -N
;; Egison Version 3.7.14 (C) 2011-2018 Satoshi Egi
;; https://www.egison.org
;; Welcome to Egison Interpreter!
;; > loadFile("ramsey-N.egi")
;; > output(inputRed)
;; {[{4 5 6} {100}] [{4 5 6 1 2 3} {107}] [{4 1 2 3} {101}] [{6 1 2 3} {103}] [{5 1 2 3} {102}] [{4 5 1 2 3} {104}] [{4 6 1 2 3} {105}] [{4 6 1 2 3} {105}] [{5 6 1 2
;; 3} {106}] [{5 6 1 2 3} {106}] [{4 5 1 2 3} {104}] [{4 5 6 1 2 3} {107}] [{4 5 6 1 2 3} {107}] [{4 5 6 1 2 3} {107}]}
;; > output(inputBlue)
;; {[{4 5 6 1 2 3} {100}] [{4 5 6} {107}] [{6 1 2 3} {104}] [{4 1 2 3} {106}] [{5 1 2 3} {105}] [{4 5 6 1 2 3} {100}] [{4 6 1 2 3} {102}] [{4 5 1 2 3} {103}] [{5 6 1
;; 2 3} {101}] [{5 6 1 2 3} {101}] [{4 6 1 2 3} {102}] [{4 5 6 1 2 3} {100}] [{4 5 6 1 2 3} {100}] [{4 5 1 2 3} {103}]}
;; >

Ramsey05.idr

-- module Ramsey05
module Main

%default total


comb : Nat -> List a -> List (List a)
comb Z     _         = [[]]
comb (S n) []        = []
comb (S n) (x :: xs) = [x :: y | y <- comb n xs] ++ comb (S n) xs

ramsey' : (e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15 : Bool) -> Bool
ramsey' e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 e11 e12 e13 e14 e15
  = any (==True) $ map (all (==True)) $ comb 3 [e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15]

partial
ramsey : List Bool -> Bool
ramsey [e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15]
  = ramsey' e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 e11 e12 e13 e14 e15
    || ramsey' (not e1) (not e2) (not e3) (not e4) (not e5) (not e6) (not e7) (not e8) (not e9) (not e10) (not e11) (not e12) (not e13) (not e14) (not e15)

partial
main : IO ()
main = traverse_ (putStr . show) $
  map ramsey [[e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15] | e1 <- [True, False], e2 <- [True, False], e3 <- [True, False], e4 <- [True, False], e5 <- [True, False],
                                                                                   e6 <- [True, False], e7 <- [True, False], e8 <- [True, False], e9 <- [True, False], e10 <- [True, False],
                                                                                   e11 <- [True, False], e12 <- [True, False], e13 <- [True, False], e14 <- [True, False], e15 <- [True, False]]

{--
> idris Ramsey05.idr -o run
> run > output.txt
でTrueの海
--}

Ramsey06.idr

-- $ idris
-- > :l Ramsey06
module Ramsey06

%default total


namespace Ram
  data Vertex = A | B | C | D
  E : Type
  E = (Vertex, Vertex) -> Bool

  data Edge : (e : E) -> Vertex -> Vertex -> Type where
    IsFalse : e (a, b) = False -> Edge e a b
    IsTrue  : e (a, b) = True  -> Edge e a b

  Premise : (e : E) -> Type
  Premise e = (e (D, A) = True, e (D, B) = True, e (D, C) = True)

  data SameColorTriangle : (e : E) -> Vertex -> Vertex -> Vertex -> Type where
    IsTri1 : (e (a, b) = bo, e (b, c) = bo, e (c, a) = bo) -> SameColorTriangle e a b c
    IsTri2 : (e (d, a) = bo, e (d, b) = bo, e (a, b) = bo) -> SameColorTriangle e d a b
    IsTri3 : (e (d, a) = bo, e (d, c) = bo, e (c, a) = bo) -> SameColorTriangle e d c a

  ramsey : (e : E) -> Premise e -> (Edge e A B, Edge e B C, Edge e C A)
    -> (a : Vertex ** (b : Vertex ** (c : Vertex ** SameColorTriangle e a b c)))
  ramsey _ _                  (IsFalse eq1, IsFalse eq2, IsFalse eq3) = (A ** (B ** (C ** IsTri1 (eq1 , eq2 , eq3))))
  ramsey _ (eqp1, eqp2, _   ) (IsTrue  eq1, _          , _          ) = (D ** (A ** (B ** IsTri2 (eqp1, eqp2, eq1))))
  ramsey _ (_,    eqp2, eqp3) (_          , IsTrue  eq2, _          ) = (D ** (B ** (C ** IsTri2 (eqp2, eqp3, eq2))))
  ramsey _ (eqp1, _,    eqp3) (_          , _          , IsTrue  eq3) = (D ** (C ** (A ** IsTri3 (eqp1, eqp3, eq3))))