From 5793653f6bb2aef9f4a7e2f3f10e59218a788b32 Mon Sep 17 00:00:00 2001
From: Joshua Moerman <lakseru@gmail.com>
Date: Mon, 9 Apr 2018 19:23:27 +0200
Subject: [PATCH] Implemented a FO-theory solver for the dense linear order

---
 app/Main.hs           | 124 +++++++++++++++++++++++++++++++++++++++++-
 ons-hs.cabal          |   1 +
 src/EquivariantSet.hs |   1 +
 3 files changed, 124 insertions(+), 2 deletions(-)

diff --git a/app/Main.hs b/app/Main.hs
index 18fc10e..9735770 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,6 +1,126 @@
 module Main where
 
-import Orbit
+import EquivariantSet
+import Support.Rat
+
+import Prelude (Show, Ord, Eq, Int, IO, print, otherwise, (.), ($))
+import qualified Prelude as P
+
+{-
+Solver for the FO theory of the dense linear order (i.e. Rationals with
+the relation <). Implemented using nominal sets. This is in contrast to
+libraries such as LOIS and nlambda, which use a solver to implement nominal
+sets.
+-}
+
+-- De Bruijn indices
+type Var = Int
+
+-- Literals for the FO formulas
+data Literal
+  = Equals Var Var   -- There is always == in the FO language
+  | LessThan Var Var -- And in our case we have 1 more relation
+  deriving (Show, Ord, Eq)
+
+-- Formulas are constructed with literals and connectives
+-- Note that we only include the necessary ones (the others can be derived)
+data Formula
+  = Lit Literal
+  | True
+  | Exists Formula
+  | Or Formula Formula
+  | Not Formula
+  deriving (Show, Ord, Eq)
+
+-- smart constructors to avoid unwieldy expressions
+infix 4 ==, /=, <, <=, >, >=
+(==), (/=), (<), (<=), (>), (>=) :: Var -> Var -> Formula
+x == y | x P.== y  = true
+       | otherwise = Lit (Equals x y)
+x /= y = not (x == y)
+x < y  | x P.== y  = false
+       | otherwise = Lit (LessThan x y)
+x <= y = or (x < y) (x == y)
+x > y  = y < x
+x >= y = or (x > y) (x == y)
+
+true, false :: Formula
+true  = True
+false = Not True
+
+not :: Formula -> Formula
+not (Not x) = x
+not x = Not x
+
+infixr 3 `and`
+infixr 2 `or`, `implies`
+and, or, implies :: Formula -> Formula -> Formula
+or True x = true
+or x True = true
+or x y    = Or x y
+and True x = x
+and x True = x
+and x y    = not (not x `or` not y)
+implies x y = not x `or` y
+
+forAll, exists :: Formula -> Formula
+forAll p = not (exists (not p))
+exists p = Exists p
+
+
+-- Here is the solver. It keeps track of a nominal set.
+-- If that sets is empty in the end, the formula does not hold.
+type Context = EquivariantSet [Rat]
+
+extend, drop :: Context -> Context
+extend ctx = map (P.uncurry (:)) (product singleVar ctx)
+  where singleVar = singleOrbit (Rat 0)
+drop ctx = map (P.tail) ctx
+
+truth0 :: Context -> Formula -> Context
+truth0 ctx (Lit (Equals i j))   = filter (\w -> w P.!! i P.== w P.!! j) ctx
+truth0 ctx (Lit (LessThan i j)) = filter (\w -> w P.!! i P.< w P.!! j) ctx
+truth0 ctx True       = ctx
+truth0 ctx (Not x)    = ctx `difference` truth0 ctx x
+truth0 ctx (Or x y)   = truth0 ctx x `union` truth0 ctx y
+truth0 ctx (Exists p) = drop (truth0 (extend ctx) p)
+
+truth :: Formula -> P.Bool
+truth f = P.not . null $ truth0 (singleOrbit []) f
+
+
+-- Some tests
+-- De Bruijn indices are not very easy to work with...
+
+-- for each element there is a strictly bigger element
+test1 = forAll {-1-} (exists {-0-} (1 > 0))
+-- there is a minimal element (= false)
+test2 = exists {-1-} (forAll {-0-} (1 <= 0))
+-- the order is dense
+test3 = forAll {-x-} (forAll {-y-} (1 {-x-} < 0 {-y-} `implies` exists {-z-} (2 < 0 `and` 0 < 1)))
+-- Formulas by Niels (= true)
+test4 = forAll (forAll (forAll (2 < 1 `and` 1 < 0 `implies`
+                           (forAll (forAll (4 < 1 `and` 1 < 3 `and` 3 < 0 `and` 0 < 2) `implies`
+                              (exists (2 < 0 `and` 0 < 1)))))))
+test5 = exists (forAll (forAll (1 < 0 `implies`
+                           exists (forAll (forAll ((1 < 0 `and` 0 < 4 `and` 3 < 1) `implies`
+                                              (forAll (6 == 0))))))))
+test6 = (forAll (0 == 0)) `implies` (exists (0 /= 0))
+test7 = (forAll (forAll (0 == 1))) `implies` (exists (0 /= 0))
 
 main :: IO ()
-main = putStrLn "Hello from App.hs"
+main = do
+  print test1
+  print (truth test1)
+  print test2
+  print (truth test2)
+  print test3
+  print (truth test3)
+  print test4
+  print (truth test4)
+  print test5
+  print (truth test5)
+  print test6
+  print (truth test6)
+  print test7
+  print (truth test7)
diff --git a/ons-hs.cabal b/ons-hs.cabal
index 3619633..aef65cd 100644
--- a/ons-hs.cabal
+++ b/ons-hs.cabal
@@ -36,6 +36,7 @@ executable ons-hs-exe
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N
   build-depends:       base
                      , ons-hs
+  ghc-options:         -threaded -rtsopts -with-rtsopts=-N -O2
   default-language:    Haskell2010
 
 benchmark ons-hs-bench
diff --git a/src/EquivariantSet.hs b/src/EquivariantSet.hs
index fcb9def..8899aec 100644
--- a/src/EquivariantSet.hs
+++ b/src/EquivariantSet.hs
@@ -88,6 +88,7 @@ delete a = EqSet . Set.delete (toOrbit a) . unEqSet
 union :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
 union a b = EqSet $ Set.union (unEqSet a) (unEqSet b)
 
+-- Not symmetric, but A \ B
 difference :: Ord (Orb a) => EquivariantSet a -> EquivariantSet a -> EquivariantSet a
 difference a b = EqSet $ Set.difference (unEqSet a) (unEqSet b)