{-# LANGUAGE CPP             #-}
{-# LANGUAGE LambdaCase      #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE RecordWildCards #-}
module RSTT.Interpret where

import Data.Char (isSpace)
import           Data.Set             (Set)
import qualified Data.Set             as Set

import           Control.Applicative
import           Control.Monad.Logic
import           Control.Monad.Reader
import           Control.Monad.State
import           Control.Monad.Writer
#if __GLASGOW_HASKELL__ < 808
import           Control.Monad.Fail   (MonadFail)
#endif
import qualified Data.List            as List
import           Data.Maybe           (fromMaybe)

import           RSTT.Syntax.Abs
import qualified RSTT.Syntax.Layout   as RSTT
import qualified RSTT.Syntax.Par      as RSTT
import qualified RSTT.Syntax.Print    as Printer

import qualified RSTT.Cube            as RSTT
import qualified RSTT.Tope            as RSTT
import qualified RSTT.Tope.Proof      as Prover

interpretIO :: String -> IO ()
interpretIO :: String -> IO ()
interpretIO String
input = do
  case String -> Either String [String]
interpret String
input of
    Left String
err -> do
      String -> IO ()
putStrLn String
"ERROR: Syntax error:"
      String -> IO ()
putStrLn String
err
    Right [String]
outputs -> (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [String]
outputs

interpretProgramIO :: Program -> IO ()
interpretProgramIO :: Program -> IO ()
interpretProgramIO = (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn ([String] -> IO ()) -> (Program -> [String]) -> Program -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Program -> [String]
interpretProgram

interpret :: String -> Either String [String]
interpret :: String -> Either String [String]
interpret String
input = do
  let tokens :: [Token]
tokens = Bool -> [Token] -> [Token]
RSTT.resolveLayout Bool
True (String -> [Token]
RSTT.myLexer String
input)
  Program -> [String]
interpretProgram (Program -> [String])
-> Either String Program -> Either String [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Token] -> Either String Program
RSTT.pProgram [Token]
tokens

unsafeParseTope :: String -> RSTT.Tope
unsafeParseTope :: String -> Tope
unsafeParseTope String
input =
  case [Token] -> Err Tope
RSTT.pTope (String -> [Token]
RSTT.myLexer String
input) of
    Left String
err -> String -> Tope
forall a. HasCallStack => String -> a
error (String
err String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\nwhen parsing " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
input) 
    Right Tope
t -> Tope -> Tope
convertTope Tope
t

interpretProgram :: Program -> [String]
interpretProgram :: Program -> [String]
interpretProgram (Program [Decl]
decls) =
  Writer [String] () -> [String]
forall w a. Writer w a -> w
execWriter (Writer [String] () -> [String]) -> Writer [String] () -> [String]
forall a b. (a -> b) -> a -> b
$
    StateT DefinedRules (Writer [String]) ()
-> DefinedRules -> Writer [String] ()
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ((Decl -> StateT DefinedRules (Writer [String]) ())
-> [Decl] -> StateT DefinedRules (Writer [String]) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Decl -> StateT DefinedRules (Writer [String]) ()
interpretDecl [Decl]
decls) DefinedRules
Prover.rulesLJE

interpretDecl :: Decl -> StateT Prover.DefinedRules (Writer [String]) ()
interpretDecl :: Decl -> StateT DefinedRules (Writer [String]) ()
interpretDecl = \case
  DeclCube (Label String
con) [PointConDecl]
_points -> Writer [String] () -> StateT DefinedRules (Writer [String]) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Writer [String] () -> StateT DefinedRules (Writer [String]) ())
-> Writer [String] () -> StateT DefinedRules (Writer [String]) ()
forall a b. (a -> b) -> a -> b
$
    [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ String
"WARNING: cube declaration is ignored for cube " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
con ]
  DeclTopePrefix (Label String
con) [Cube]
_cubes [TopeRule]
rules -> do
    [TopeRule]
-> (TopeRule -> StateT DefinedRules (Writer [String]) ())
-> StateT DefinedRules (Writer [String]) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [TopeRule]
rules ((TopeRule -> StateT DefinedRules (Writer [String]) ())
 -> StateT DefinedRules (Writer [String]) ())
-> (TopeRule -> StateT DefinedRules (Writer [String]) ())
-> StateT DefinedRules (Writer [String]) ()
forall a b. (a -> b) -> a -> b
$ \rule :: TopeRule
rule@(TopeRule (RuleName String
name) [Sequent]
_ Line
_ Sequent
_) -> do
      [String] -> StateT DefinedRules (Writer [String]) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ String
"INFO: Adding new rule for tope " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
con String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
": " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
name ]
      (DefinedRules -> DefinedRules)
-> StateT DefinedRules (Writer [String]) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (DefinedRules -> DefinedRules -> DefinedRules
forall a. Semigroup a => a -> a -> a
<> TopeRule -> DefinedRules
convertRule TopeRule
rule)
  DeclShape (Var String
shapeName) Shape
_shape -> Writer [String] () -> StateT DefinedRules (Writer [String]) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Writer [String] () -> StateT DefinedRules (Writer [String]) ())
-> Writer [String] () -> StateT DefinedRules (Writer [String]) ()
forall a b. (a -> b) -> a -> b
$
    [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ String
"WARNING: shape definition is ignored for shape " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
shapeName ]
  DeclCommandProve Sequent
sequent -> do
    let maxDepth :: Int
maxDepth = Int
20
        k :: Int
k = Int
1
    Rules
rules <- (DefinedRules -> Rules)
-> StateT DefinedRules (Writer [String]) Rules
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets DefinedRules -> Rules
Prover.fromDefinedRules
    Writer [String] () -> StateT DefinedRules (Writer [String]) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Writer [String] () -> StateT DefinedRules (Writer [String]) ())
-> Writer [String] () -> StateT DefinedRules (Writer [String]) ()
forall a b. (a -> b) -> a -> b
$ do
      case (Int
maxDepth, Int
k) of
        (Int
_, Int
1) -> [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell
          [ String
"INFO: running BFS proofsearch up to depth " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
maxDepth Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
k) ]
        (Int
1, Int
_) -> [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell
          [ String
"INFO: running DFS proofsearch up to depth " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
maxDepth Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
k) ]
        (Int, Int)
_ -> [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell
          [ String
"INFO: running k-depth proofsearch up to depth " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show (Int
maxDepth Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
k) String -> String -> String
forall a. Semigroup a => a -> a -> a
<>
            String
" (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
maxDepth String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" iterations, k = " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")" ]
      let s :: Sequent
s = Sequent -> Sequent
convertSequent Sequent
sequent
      case Int -> Int -> Rules -> Sequent -> Maybe Proof
Prover.proveWithBFSviaDFS' Int
maxDepth Int
k Rules
rules Sequent
s of
        Maybe Proof
Nothing -> do
          [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ String
"The sequent is not provable: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Sequent -> String
Prover.ppSequent Sequent
s ]
        Just Proof
proof -> do
          [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ Proof -> String
Prover.ppProof Proof
proof ]
      [String] -> Writer [String] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [ String
"" ]
  DeclCommandRenderLatex
    shape :: Shape
shape@(Shape
      (PointPatternPair (PointPatternVar Var
"t") (PointPatternVar Var
"s"))
      (CubeProduct (CubeCon Label
"𝟚") (CubeCon Label
"𝟚"))
      Tope
tope) -> do
        Rules
rules <- (DefinedRules -> Rules)
-> StateT DefinedRules (Writer [String]) Rules
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets DefinedRules -> Rules
Prover.fromDefinedRules
        let maxDepth :: Int
maxDepth = Int
20
            k :: Int
k = Int
1
            hasShape :: String -> Sequent
hasShape String
s = CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent
              [(Var
"t", Label -> Cube
RSTT.CubeCon Label
"𝟚"), (Var
"s", Label -> Cube
RSTT.CubeCon Label
"𝟚")]
              [String -> Tope
unsafeParseTope String
s]
              (Tope -> Tope
convertTope Tope
tope)
            sub :: String -> p -> p -> p
sub String
s p
no p
yes =
              case Int -> Int -> Rules -> Sequent -> Maybe Proof
Prover.proveWithBFSviaDFS' Int
maxDepth Int
k Rules
rules (String -> Sequent
hasShape String
s) of
                Maybe Proof
Nothing -> p
no
                Just{} -> p
yes
            cornerLeftTop :: String
cornerLeftTop     = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ 𝟬 ∧ t ≡ 𝟬" String
"\\;" String
"\\bullet"
            cornerLeftBottom :: String
cornerLeftBottom  = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ 𝟭 ∧ t ≡ 𝟬" String
"\\;" String
"\\bullet"
            cornerRightTop :: String
cornerRightTop    = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ 𝟬 ∧ t ≡ 𝟭" String
"\\;" String
"\\bullet"
            cornerRightBottom :: String
cornerRightBottom = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ 𝟭 ∧ t ≡ 𝟭" String
"\\;" String
"\\bullet"
            edgeTop :: String
edgeTop     = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ 𝟬" String
"" String
"\\arrow[rr]"
            edgeBottom :: String
edgeBottom  = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ 𝟭" String
"" String
"\\arrow[rr]"
            edgeLeft :: String
edgeLeft    = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t ≡ 𝟬" String
"" String
"\\arrow[dd]"
            edgeRight :: String
edgeRight   = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t ≡ 𝟭" String
"" String
"\\arrow[dd]"
            edgeDiag :: String
edgeDiag    = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"s ≡ t" String
"" String
"\\arrow[ddrr]"
            triangleTop :: String
triangleTop = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"≤(s, t)" String
"" String
"\\fill[blue, opacity=0.2] (p00.center) -- (p10.center) -- (p11.center) -- cycle;"
            triangleBottom :: String
triangleBottom = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"≤(t, s)" String
"" String
"\\fill[blue, opacity=0.2] (p00.center) -- (p01.center) -- (p11.center) -- cycle;"
        [String] -> StateT DefinedRules (Writer [String]) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell
          [ String
"% diagram for the shape"
          , String
"% " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unwords (String -> [String]
words (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
" " (String -> [String]
lines (Shape -> String
forall a. Print a => a -> String
Printer.printTree Shape
shape))))
          , String
"\\begin{tikzcd}["
          , String
" execute at end picture={"
          , String
"   \\scoped[on background layer]"
          , String
"   " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
triangleTop
          , String
"   " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
triangleBottom
          , String
" }]"
          , String
" |[alias=p00]|"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
cornerLeftTopString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" "String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
edgeTopString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" "String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
edgeDiagString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" "String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
edgeLeftString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" & \\; & |[alias=p10]|"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
cornerRightTopString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" "String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
edgeRightString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" \\\\"
          , String
" \\; & \\; & \\; \\\\"
          , String
" |[alias=p01]|"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
cornerLeftBottomString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" "String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
edgeBottomString -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
" & \\; & |[alias=p11]|"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
cornerRightBottom
          , String
"\\end{tikzcd}" ]
  DeclCommandRenderLatex
    shape :: Shape
shape@(Shape
      (PointPatternPair (PointPatternVar Var
"t1") (PointPatternPair (PointPatternVar Var
"t2") (PointPatternVar Var
"t3")))
      (CubeProduct (CubeCon Label
"𝟚") (CubeProduct (CubeCon Label
"𝟚") (CubeCon Label
"𝟚")))
      Tope
tope) -> do
        Rules
rules <- (DefinedRules -> Rules)
-> StateT DefinedRules (Writer [String]) Rules
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets DefinedRules -> Rules
Prover.fromDefinedRules
        let maxDepth :: Int
maxDepth = Int
20
            k :: Int
k = Int
1
            hasShape :: String -> Sequent
hasShape String
s = CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent
              [ (Var
"t1", Label -> Cube
RSTT.CubeCon Label
"𝟚")
              , (Var
"t2", Label -> Cube
RSTT.CubeCon Label
"𝟚")
              , (Var
"t3", Label -> Cube
RSTT.CubeCon Label
"𝟚") ]
              [String -> Tope
unsafeParseTope String
s]
              (Tope -> Tope
convertTope Tope
tope)
            sub :: String -> p -> p -> p
sub String
s p
no p
yes =
              case Int -> Int -> Rules -> Sequent -> Maybe Proof
Prover.proveWithBFSviaDFS' Int
maxDepth Int
k Rules
rules (String -> Sequent
hasShape String
s) of
                Maybe Proof
Nothing -> p
no
                Just{} -> p
yes
            sub4 :: String -> (String, String, String, String) -> String
sub4 String
s (String
x, String
y, String
z, String
w) = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
s String
"" (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
"\n"
              [ String
"\\fill[red, opacity=0.2, transform canvas={scale around={0.3:(barycentric cs:"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p1String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
"=0.5,"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p2String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
"=0.5,"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p3String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
"=0.5,"String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p4String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
"=0.5)}}] ("String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p1String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
".center) -- ("String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p2String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
".center) -- ("String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
p3String -> String -> String
forall a. Semigroup a => a -> a -> a
<>String
".center) -- cycle;" | [String
p1, String
p2, String
p3, String
p4] <- [ [String
x, String
y, String
z, String
w], [String
x, String
y, String
w, String
z], [String
x, String
z, String
w, String
y], [String
y, String
z, String
w, String
x] ] ]

            corner000 :: String
corner000 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ 𝟬 ∧ t1 ≡ 𝟬" String
"\\;" String
"\\bullet"
            corner001 :: String
corner001 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ 𝟬 ∧ t1 ≡ 𝟭" String
"\\;" String
"\\bullet"
            corner010 :: String
corner010 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ 𝟭 ∧ t1 ≡ 𝟬" String
"\\;" String
"\\bullet"
            corner011 :: String
corner011 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ 𝟭 ∧ t1 ≡ 𝟭" String
"\\;" String
"\\bullet"
            corner100 :: String
corner100 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ 𝟬 ∧ t1 ≡ 𝟬" String
"\\;" String
"\\bullet"
            corner101 :: String
corner101 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ 𝟬 ∧ t1 ≡ 𝟭" String
"\\;" String
"\\bullet"
            corner110 :: String
corner110 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ 𝟭 ∧ t1 ≡ 𝟬" String
"\\;" String
"\\bullet"
            corner111 :: String
corner111 = String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ 𝟭 ∧ t1 ≡ 𝟭" String
"\\;" String
"\\bullet"

        [String] -> StateT DefinedRules (Writer [String]) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([String] -> StateT DefinedRules (Writer [String]) ())
-> [String] -> StateT DefinedRules (Writer [String]) ()
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> Bool) -> (String -> String) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace))
          [ String
"% diagram for the shape"
          , String
"% " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unwords (String -> [String]
words (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
" " (String -> [String]
lines (Shape -> String
forall a. Print a => a -> String
Printer.printTree Shape
shape))))
          , String
"\\begin{tikzcd}["
          , String
" execute at end picture={"
          -- , "   \\scoped[on background layer]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ ≤(t2, t1)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p001=0.5,p011=0.5)}}] (p000.center) -- (p001.center) -- (p011.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ ≤(t1, t2)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p010=0.5,p011=0.5)}}] (p000.center) -- (p010.center) -- (p011.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ ≤(t2, t1)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p100=0.5,p101=0.5,p111=0.5)}}] (p100.center) -- (p101.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ ≤(t1, t2)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p100=0.5,p110=0.5,p111=0.5)}}] (p100.center) -- (p110.center) -- (p111.center) -- cycle;"

          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟬 ∧ ≤(t3, t1)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p001=0.5,p101=0.5)}}] (p000.center) -- (p001.center) -- (p101.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟬 ∧ ≤(t1, t3)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p100=0.5,p101=0.5)}}] (p000.center) -- (p100.center) -- (p101.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟭 ∧ ≤(t3, t1)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p010=0.5,p011=0.5,p111=0.5)}}] (p010.center) -- (p011.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟭 ∧ ≤(t1, t3)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p010=0.5,p110=0.5,p111=0.5)}}] (p010.center) -- (p110.center) -- (p111.center) -- cycle;"

          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t1 ≡ 𝟬 ∧ ≤(t3, t2)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p010=0.5,p110=0.5)}}] (p000.center) -- (p010.center) -- (p110.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t1 ≡ 𝟬 ∧ ≤(t2, t3)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p100=0.5,p110=0.5)}}] (p000.center) -- (p100.center) -- (p110.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t1 ≡ 𝟭 ∧ ≤(t3, t2)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p001=0.5,p011=0.5,p111=0.5)}}] (p001.center) -- (p011.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t1 ≡ 𝟭 ∧ ≤(t2, t3)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p001=0.5,p101=0.5,p111=0.5)}}] (p001.center) -- (p101.center) -- (p111.center) -- cycle;"

          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ t2 ∧ ≤(t2, t1)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p001=0.5,p111=0.5)}}] (p000.center) -- (p001.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ t2 ∧ ≤(t1, t2)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p110=0.5,p111=0.5)}}] (p000.center) -- (p110.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ t1 ∧ ≤(t3, t1)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p011=0.5,p111=0.5)}}] (p000.center) -- (p011.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ t1 ∧ ≤(t1, t3)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p100=0.5,p111=0.5)}}] (p000.center) -- (p100.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ t1 ∧ ≤(t3, t2)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p010=0.5,p111=0.5)}}] (p000.center) -- (p010.center) -- (p111.center) -- cycle;"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ t1 ∧ ≤(t2, t3)" String
"" String
"\\fill[blue, opacity=0.2, transform canvas={scale around={0.9:(barycentric cs:p000=0.5,p101=0.5,p111=0.5)}}] (p000.center) -- (p101.center) -- (p111.center) -- cycle;"

          , String -> (String, String, String, String) -> String
sub4 String
"≤(t3, t2) ∧ ≤(t2, t1)" (String
"p000", String
"p001", String
"p011", String
"p111")
          , String -> (String, String, String, String) -> String
sub4 String
"≤(t3, t1) ∧ ≤(t1, t2)" (String
"p000", String
"p010", String
"p011", String
"p111")
          , String -> (String, String, String, String) -> String
sub4 String
"≤(t2, t3) ∧ ≤(t3, t1)" (String
"p000", String
"p001", String
"p101", String
"p111")
          , String -> (String, String, String, String) -> String
sub4 String
"≤(t1, t3) ∧ ≤(t3, t2)" (String
"p000", String
"p010", String
"p110", String
"p111")
          , String -> (String, String, String, String) -> String
sub4 String
"≤(t1, t2) ∧ ≤(t2, t3)" (String
"p000", String
"p100", String
"p110", String
"p111")
          , String -> (String, String, String, String) -> String
sub4 String
"≤(t2, t1) ∧ ≤(t1, t3)" (String
"p000", String
"p100", String
"p101", String
"p111")

          , String
" }]"

          , String
"\\;" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& |[alias=p000]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner000 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& \\; & |[alias=p001]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner001 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\\\\"
          , String
"|[alias=p100]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner100 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& \\; & |[alias=p101]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner101 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& \\; \\\\"
          , String
"\\;" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& |[alias=p010]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner010 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& \\; & |[alias=p011]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner011 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"\\\\"
          , String
"|[alias=p110]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner110 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& \\; & |[alias=p111]|" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
corner111 String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"& \\; \\\\"

          -- edges at the back, left, and bottom faces
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ 𝟬" String
"" String
"\\arrow[from=p000, to=p001]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t1 ≡ 𝟬" String
"" String
"\\arrow[from=p000, to=p010]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t1 ≡ 𝟭" String
"" String
"\\arrow[from=p001, to=p011]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ 𝟭" String
"" String
"\\arrow[from=p010, to=p011]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟬 ∧ t2 ≡ t1" String
"" String
"\\arrow[from=p000, to=p011]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟬 ∧ t1 ≡ 𝟬" String
"" String
"\\arrow[from=p000, to=p100]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t1 ≡ 𝟬 ∧ t3 ≡ t2" String
"" String
"\\arrow[from=p000, to=p110]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟭 ∧ t1 ≡ 𝟬" String
"" String
"\\arrow[from=p010, to=p110]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t1 ≡ 𝟬" String
"" String
"\\arrow[from=p100, to=p110]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟭 ∧ t3 ≡ t1" String
"" String
"\\arrow[from=p010, to=p111]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟭 ∧ t1 ≡ 𝟭" String
"" String
"\\arrow[from=p011, to=p111]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ 𝟭" String
"" String
"\\arrow[from=p110, to=p111]"

          -- edge in the middle
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ t2 ∧ t2 ≡ t1" String
"" String
"\\arrow[from=p000, to=p111, crossing over]"

          -- edges at the front, right, and top faces
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟬 ∧ t3 ≡ t1" String
"" String
"\\arrow[from=p000, to=p101]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t1 ≡ 𝟭 ∧ t3 ≡ t2" String
"" String
"\\arrow[from=p001, to=p111, crossing over]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t2 ≡ 𝟬 ∧ t1 ≡ 𝟭" String
"" String
"\\arrow[from=p001, to=p101]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ 𝟬" String
"" String
"\\arrow[from=p100, to=p101, crossing over]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t2 ≡ t1" String
"" String
"\\arrow[from=p100, to=p111, crossing over]"
          , String -> String -> String -> String
forall {p}. String -> p -> p -> p
sub String
"t3 ≡ 𝟭 ∧ t1 ≡ 𝟭" String
"" String
"\\arrow[from=p101, to=p111, crossing over]"

          , String
"\\end{tikzcd}" ]
  DeclCommandRenderLatex Shape
shape ->
    [String] -> StateT DefinedRules (Writer [String]) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [String
"WARNING: render latex unsupported for shape " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Shape -> String
forall a. Show a => a -> String
show Shape
shape]


-- ** Compiling rules

convertRule :: TopeRule -> Prover.DefinedRules
convertRule :: TopeRule -> DefinedRules
convertRule TopeRule
rule = DefinedRules :: Rules -> Rules -> Rules -> Rules -> DefinedRules
Prover.DefinedRules
  { invertibleRules :: Rules
invertibleRules    = TopeRule -> Rules
tableauRule TopeRule
rule
  , invertibleCutRules :: Rules
invertibleCutRules = TopeRule -> Rules
tableauCutRule TopeRule
rule
  , tableauxRules :: Rules
tableauxRules      = Rules
forall a. Monoid a => a
mempty -- tableauRule rule
  , tableauxCutRules :: Rules
tableauxCutRules   = Rules
forall a. Monoid a => a
mempty -- tableauCutRule rule
  }

tableauRule :: TopeRule -> Prover.Rules
tableauRule :: TopeRule -> Rules
tableauRule rule :: TopeRule
rule@(TopeRule (RuleName String
name) [Sequent]
premises Line
_line Sequent
conclusion) = do
  Sequent
currentGoal <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  let metavars :: Set Var
metavars = (Point -> Set Var) -> Set Point -> Set Var
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Point -> Set Var
collectPointVars (TopeRule -> Set Point
collectRulePoints TopeRule
rule)
  (Substs
substs, TopeContext
leftoverTopes) <- Set Var -> Sequent -> Sequent -> RulesM (Substs, TopeContext)
forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Set Var -> Sequent -> Sequent -> f (Substs, TopeContext)
matchSequent Set Var
metavars Sequent
conclusion Sequent
currentGoal
  let goals :: [Sequent]
goals = (Sequent -> Sequent) -> [Sequent] -> [Sequent]
forall a b. (a -> b) -> [a] -> [b]
map (Sequent -> Sequent
normalizeSequent (Sequent -> Sequent) -> (Sequent -> Sequent) -> Sequent -> Sequent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopeContext -> Sequent -> Sequent
addTopes TopeContext
leftoverTopes (Sequent -> Sequent) -> (Sequent -> Sequent) -> Sequent -> Sequent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substs -> Sequent -> Sequent
applySubsts Substs
substs) [Sequent]
premises
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((Sequent -> Bool) -> [Sequent] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Sequent -> Sequent -> Bool
forall a. Eq a => a -> a -> Bool
/= Sequent
currentGoal) [Sequent]
goals)
  -- trace (Prover.ppSequent currentGoal) $
  (String, [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return (String
name, [Sequent]
goals)
  where
    addTopes :: TopeContext -> Sequent -> Sequent
addTopes TopeContext
topes Prover.Sequent{CubeContext
TopeContext
Tope
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..} =
      Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent{ sequentTopeContext :: TopeContext
sequentTopeContext = TopeContext
topes TopeContext -> TopeContext -> TopeContext
forall a. Semigroup a => a -> a -> a
<> TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}

tableauCutRule :: TopeRule -> Prover.Rules
tableauCutRule :: TopeRule -> Rules
tableauCutRule rule :: TopeRule
rule@(TopeRule (RuleName String
name) [Sequent]
premises Line
_line Sequent
conclusion) = do
  -- [Heuristic] affects completeness
  -- guard (null premises)

  currentGoal :: Sequent
currentGoal@Prover.Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} <- RulesM Sequent
forall r (m :: * -> *). MonadReader r m => m r
ask
  let metavars :: Set Var
metavars = (Point -> Set Var) -> Set Point -> Set Var
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Point -> Set Var
collectPointVars (TopeRule -> Set Point
collectRulePoints TopeRule
rule)
  let Sequent CubeContext
_ TopeContext
ctx Tope
tope = Sequent
conclusion

  -- [Heuristic] TODO: check if affects completeness
  -- do not consider rules where RHS is a variable
  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Tope -> Bool
isVar Tope
tope))

  (substs :: Substs
substs@(Substs CubeContext
_ [(Var, Point)]
substPoints [(Var, Tope)]
substTopes), TopeContext
leftoverTopes) <- Substs
-> TopeContext -> TopeContext -> RulesM (Substs, TopeContext)
forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Substs -> TopeContext -> TopeContext -> f (Substs, TopeContext)
matchTopeContext (CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [] []) TopeContext
ctx TopeContext
sequentTopeContext
  subst'' :: Substs
subst''@(Substs CubeContext
_ [(Var, Point)]
substPoints' [(Var, Tope)]
_) <- Set Var -> Set Point -> RulesM Substs
forall (f :: * -> *).
Alternative f =>
Set Var -> Set Point -> f Substs
matchVars (Set Var
metavars Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList ((Var, Point) -> Var
forall a b. (a, b) -> a
fst ((Var, Point) -> Var) -> [(Var, Point)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, Point)]
substPoints))
              ((Tope -> Set Point) -> TopeContext -> Set Point
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Tope -> Set Point
collectTopePoints (Tope
sequentTope Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
sequentTopeContext))
  let substs' :: Substs
substs' = Substs
substs Substs -> Substs -> Substs
forall a. Semigroup a => a -> a -> a
<> Substs
subst''
      newTope :: Tope
newTope = [(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope
substInTope ([(Var, Point)]
substPoints [(Var, Point)] -> [(Var, Point)] -> [(Var, Point)]
forall a. Semigroup a => a -> a -> a
<> [(Var, Point)]
substPoints') [(Var, Tope)]
substTopes Tope
tope

  -- [Heuristic] TODO: check if affects completeness
  -- Make sure new goal is not a trivial consequence of existing premises via LJE
  -- (otherwise this is not useful)
  -- This should work good for rules such as excluded middle for (≤).
  RulesM (ProofTree Sequent) -> RulesM ()
forall (m :: * -> *) a. MonadLogic m => m a -> m ()
lnot (ReaderT Sequent (LogicT Identity) (ProofTree Sequent)
-> RulesM (ProofTree Sequent)
forall a. ReaderT Sequent (LogicT Identity) a -> RulesM a
Prover.RulesM (LogicT Identity (ProofTree Sequent)
-> ReaderT Sequent (LogicT Identity) (ProofTree Sequent)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Int -> Rules -> Sequent -> LogicT Identity (ProofTree Sequent)
Prover.proveWithDFS Int
1 (DefinedRules -> Rules
Prover.fromDefinedRules DefinedRules
Prover.rulesLJE) Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent{sequentTope :: Tope
sequentTope = Tope
newTope, CubeContext
TopeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
..})))

  let goals :: [Sequent]
goals = (Sequent -> Sequent) -> [Sequent] -> [Sequent]
forall a b. (a -> b) -> [a] -> [b]
map (Sequent -> Sequent
normalizeSequent (Sequent -> Sequent) -> (Sequent -> Sequent) -> Sequent -> Sequent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopeContext -> Sequent -> Sequent
addTopes TopeContext
leftoverTopes (Sequent -> Sequent) -> (Sequent -> Sequent) -> Sequent -> Sequent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substs -> Sequent -> Sequent
applySubsts Substs
substs') [Sequent]
premises
      goalR :: Sequent
goalR = Sequent -> Sequent
normalizeSequent (Sequent -> Sequent) -> Sequent -> Sequent
forall a b. (a -> b) -> a -> b
$ TopeContext -> Sequent -> Sequent
addTopes [[(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope
substInTope ([(Var, Point)]
substPoints [(Var, Point)] -> [(Var, Point)] -> [(Var, Point)]
forall a. Semigroup a => a -> a -> a
<> [(Var, Point)]
substPoints') [(Var, Tope)]
substTopes Tope
tope] Sequent
currentGoal
      newGoals :: [Sequent]
newGoals = Sequent
goalR Sequent -> [Sequent] -> [Sequent]
forall a. a -> [a] -> [a]
: [Sequent]
goals

  Bool -> RulesM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((Sequent -> Bool) -> [Sequent] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Sequent -> Sequent -> Bool
forall a. Eq a => a -> a -> Bool
/= Sequent
currentGoal) [Sequent]
newGoals)
  (String, [Sequent]) -> Rules
forall (m :: * -> *) a. Monad m => a -> m a
return (String
name String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" (left)", [Sequent]
newGoals)
  where
    addTopes :: TopeContext -> Sequent -> Sequent
addTopes TopeContext
topes Prover.Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} =
      Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent{ sequentTopeContext :: TopeContext
sequentTopeContext = TopeContext
topes TopeContext -> TopeContext -> TopeContext
forall a. Semigroup a => a -> a -> a
<> TopeContext
sequentTopeContext, CubeContext
Tope
sequentTope :: Tope
sequentCubeContext :: CubeContext
sequentTope :: Tope
sequentCubeContext :: CubeContext
..}

    isVar :: Tope -> Bool
isVar (TopeVar Var
_) = Bool
True
    isVar Tope
_           = Bool
False

collectRulePoints :: TopeRule -> Set RSTT.Point
collectRulePoints :: TopeRule -> Set Point
collectRulePoints (TopeRule RuleName
_ [Sequent]
premises Line
_ Sequent
conclusion) =
  (Sequent -> Set Point) -> [Sequent] -> Set Point
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Sequent -> Set Point
collectSequentPoints (Sequent -> Set Point)
-> (Sequent -> Sequent) -> Sequent -> Set Point
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sequent -> Sequent
convertSequent) (Sequent
conclusion Sequent -> [Sequent] -> [Sequent]
forall a. a -> [a] -> [a]
: [Sequent]
premises)

collectSequentPoints :: Prover.Sequent -> Set RSTT.Point
collectSequentPoints :: Sequent -> Set Point
collectSequentPoints (Prover.Sequent CubeContext
_cubeCtx TopeContext
ctx Tope
rhs) =
  (Tope -> Set Point) -> TopeContext -> Set Point
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Tope -> Set Point
collectTopePoints (Tope
rhs Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
ctx)

collectTopePoints :: RSTT.Tope -> Set RSTT.Point
collectTopePoints :: Tope -> Set Point
collectTopePoints = Tope -> Set Point
go
  where
    go :: Tope -> Set Point
go = \case
      Tope
RSTT.TopeTop             -> Set Point
forall a. Monoid a => a
mempty
      Tope
RSTT.TopeBottom          -> Set Point
forall a. Monoid a => a
mempty
      RSTT.TopeVar{}           -> Set Point
forall a. Monoid a => a
mempty
      RSTT.TopeCon Label
_con [Point]
points -> [Point] -> Set Point
forall a. Ord a => [a] -> Set a
Set.fromList [Point]
points
      RSTT.TopeImplies Tope
x Tope
y     -> Tope -> Set Point
go Tope
x Set Point -> Set Point -> Set Point
forall a. Semigroup a => a -> a -> a
<> Tope -> Set Point
go Tope
y
      RSTT.TopeOr Tope
x Tope
y          -> Tope -> Set Point
go Tope
x Set Point -> Set Point -> Set Point
forall a. Semigroup a => a -> a -> a
<> Tope -> Set Point
go Tope
y
      RSTT.TopeAnd Tope
x Tope
y         -> Tope -> Set Point
go Tope
x Set Point -> Set Point -> Set Point
forall a. Semigroup a => a -> a -> a
<> Tope -> Set Point
go Tope
y
      RSTT.TopeEQ Point
l Point
r          -> [Point] -> Set Point
forall a. Ord a => [a] -> Set a
Set.fromList [Point
l, Point
r]

collectPointVars :: RSTT.Point -> Set RSTT.Var
collectPointVars :: Point -> Set Var
collectPointVars = Point -> Set Var
go
  where
    go :: Point -> Set Var
go = \case
      RSTT.PointVar Var
x           -> [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList [Var
x]
      RSTT.PointCon Label
_con [Point]
points -> [Set Var] -> Set Var
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Point -> Set Var
go (Point -> Set Var) -> [Point] -> [Set Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Point]
points)
      Point
RSTT.PointUnit            -> Set Var
forall a. Monoid a => a
mempty
      RSTT.PointPair Point
x Point
y        -> Point -> Set Var
go Point
x Set Var -> Set Var -> Set Var
forall a. Semigroup a => a -> a -> a
<> Point -> Set Var
go Point
y
      RSTT.PointFirst Point
x         -> Point -> Set Var
go Point
x
      RSTT.PointSecond Point
x        -> Point -> Set Var
go Point
x

data Substs = Substs
  { Substs -> CubeContext
substCubeVars  :: [(RSTT.Var, RSTT.Cube)]
  , Substs -> [(Var, Point)]
substPointVars :: [(RSTT.Var, RSTT.Point)]
  , Substs -> [(Var, Tope)]
substTopeVars  :: [(RSTT.Var, RSTT.Tope)]
  }

instance Semigroup Substs where
  Substs CubeContext
cs [(Var, Point)]
ps [(Var, Tope)]
ts <> :: Substs -> Substs -> Substs
<> Substs CubeContext
cs' [(Var, Point)]
ps' [(Var, Tope)]
ts' =
    CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs (CubeContext
cs CubeContext -> CubeContext -> CubeContext
forall a. Semigroup a => a -> a -> a
<> CubeContext
cs') ([(Var, Point)]
ps [(Var, Point)] -> [(Var, Point)] -> [(Var, Point)]
forall a. Semigroup a => a -> a -> a
<> [(Var, Point)]
ps') ([(Var, Tope)]
ts [(Var, Tope)] -> [(Var, Tope)] -> [(Var, Tope)]
forall a. Semigroup a => a -> a -> a
<> [(Var, Tope)]
ts')

matchSequent
  :: (MonadPlus f, MonadFail f)
  => Set RSTT.Var -> Sequent -> Prover.Sequent -> f (Substs, [RSTT.Tope])
matchSequent :: forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Set Var -> Sequent -> Sequent -> f (Substs, TopeContext)
matchSequent Set Var
metavars (Sequent CubeContext
_points TopeContext
topes Tope
rhs) (Prover.Sequent CubeContext
_points' TopeContext
topes' Tope
rhs') = do
  Substs
subst <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
rhs Tope
rhs'
  (Substs
subst', TopeContext
leftover) <- Substs -> TopeContext -> TopeContext -> f (Substs, TopeContext)
forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Substs -> TopeContext -> TopeContext -> f (Substs, TopeContext)
matchTopeContext Substs
subst TopeContext
topes TopeContext
topes'
  Substs
subst'' <- Set Var -> Set Point -> f Substs
forall (f :: * -> *).
Alternative f =>
Set Var -> Set Point -> f Substs
matchVars (Set Var
metavars Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
Set.fromList ((Var, Point) -> Var
forall a b. (a, b) -> a
fst ((Var, Point) -> Var) -> [(Var, Point)] -> [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Substs -> [(Var, Point)]
substPointVars Substs
subst')))
              ((Tope -> Set Point) -> TopeContext -> Set Point
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Tope -> Set Point
collectTopePoints (Tope
rhs' Tope -> TopeContext -> TopeContext
forall a. a -> [a] -> [a]
: TopeContext
topes'))
  (Substs, TopeContext) -> f (Substs, TopeContext)
forall (m :: * -> *) a. Monad m => a -> m a
return (Substs
subst' Substs -> Substs -> Substs
forall a. Semigroup a => a -> a -> a
<> Substs
subst'', TopeContext
leftover)

matchVars :: Alternative f => Set RSTT.Var -> Set RSTT.Point -> f Substs
matchVars :: forall (f :: * -> *).
Alternative f =>
Set Var -> Set Point -> f Substs
matchVars Set Var
vars Set Point
points = CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs []
  ([(Var, Point)] -> [(Var, Tope)] -> Substs)
-> f [(Var, Point)] -> f ([(Var, Tope)] -> Substs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var -> f (Var, Point)) -> [Var] -> f [(Var, Point)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (\Var
var -> (,) Var
var (Point -> (Var, Point)) -> f Point -> f (Var, Point)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Point] -> f Point
forall (f :: * -> *) a. Alternative f => [a] -> f a
Prover.choose (Set Point -> [Point]
forall a. Set a -> [a]
Set.toList Set Point
points)) (Set Var -> [Var]
forall a. Set a -> [a]
Set.toList Set Var
vars)
  f ([(Var, Tope)] -> Substs) -> f [(Var, Tope)] -> f Substs
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Var, Tope)] -> f [(Var, Tope)]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

matchTopeContext
  :: (MonadPlus f, MonadFail f)
  => Substs -> TopeContext -> RSTT.TopeContext -> f (Substs, RSTT.TopeContext)
matchTopeContext :: forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Substs -> TopeContext -> TopeContext -> f (Substs, TopeContext)
matchTopeContext Substs
substs TopeContext
ctx TopeContext
ctx' =
  case TopeContext
ctx of
    TopeContext
TopeContextEmpty -> (Substs, TopeContext) -> f (Substs, TopeContext)
forall (m :: * -> *) a. Monad m => a -> m a
return (Substs
substs, TopeContext
ctx')
    TopeContextNonEmpty [Tope]
topes -> do
      Substs -> [Tope] -> TopeContext -> f (Substs, TopeContext)
forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Substs -> [Tope] -> TopeContext -> f (Substs, TopeContext)
matchTopes Substs
substs [Tope]
topes TopeContext
ctx'

matchTope :: MonadPlus f => Tope -> RSTT.Tope -> f Substs
matchTope :: forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope (TopeVar (Var String
x)) Tope
tope = Substs -> f Substs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Substs -> f Substs) -> Substs -> f Substs
forall a b. (a -> b) -> a -> b
$ CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [] [(String -> Var
RSTT.Var String
x, Tope
tope)]
matchTope (TopeCon (Label String
con) [Point]
points) (RSTT.TopeCon (RSTT.Label String
con') [Point]
points')
  | String
con String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
con' = f Substs
forall (f :: * -> *) a. Alternative f => f a
empty
  | [Point] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Point]
points Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Point] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Point]
points' = f Substs
forall (f :: * -> *) a. Alternative f => f a
empty
  | Bool
otherwise = (Point -> Point -> f Substs) -> [Point] -> [Point] -> f [Substs]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint [Point]
points [Point]
points' f [Substs] -> ([Substs] -> f Substs) -> f Substs
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Substs] -> f Substs
forall (f :: * -> *). MonadPlus f => [Substs] -> f Substs
mergeManySubsts
matchTope Tope
TopeTop Tope
RSTT.TopeTop = Substs -> f Substs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [] [])
matchTope Tope
TopeBottom Tope
RSTT.TopeBottom = Substs -> f Substs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [] [])
matchTope (TopeImplies Tope
x Tope
y) (RSTT.TopeImplies Tope
x' Tope
y') = do
  Substs
s1 <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
x Tope
x'
  Substs
s2 <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
y Tope
y'
  Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts Substs
s1 Substs
s2
matchTope (TopeOr Tope
x Tope
y) (RSTT.TopeOr Tope
x' Tope
y') = do
  Substs
s1 <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
x Tope
x'
  Substs
s2 <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
y Tope
y'
  Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts Substs
s1 Substs
s2
matchTope (TopeAnd Tope
x Tope
y) (RSTT.TopeAnd Tope
x' Tope
y') = do
  Substs
s1 <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
x Tope
x'
  Substs
s2 <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
y Tope
y'
  Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts Substs
s1 Substs
s2
matchTope (TopeEQ Point
t Point
s) (RSTT.TopeEQ Point
t' Point
s') = do
  Substs
s1 <- Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint Point
t Point
t'
  Substs
s2 <- Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint Point
s Point
s'
  Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts Substs
s1 Substs
s2
matchTope Tope
_ Tope
_ = f Substs
forall (f :: * -> *) a. Alternative f => f a
empty

matchPoint :: MonadPlus f => Point -> RSTT.Point -> f Substs
matchPoint :: forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint (PointVar (Var String
x)) Point
point = Substs -> f Substs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Substs -> f Substs) -> Substs -> f Substs
forall a b. (a -> b) -> a -> b
$ CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [(String -> Var
RSTT.Var String
x, Point
point)] []
matchPoint (PointCon (Label String
con) [Point]
points) (RSTT.PointCon (RSTT.Label String
con') [Point]
points')
  | String
con String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
con' = f Substs
forall (f :: * -> *) a. Alternative f => f a
empty
  | [Point] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Point]
points Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Point] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Point]
points' = f Substs
forall (f :: * -> *) a. Alternative f => f a
empty
  | Bool
otherwise = (Point -> Point -> f Substs) -> [Point] -> [Point] -> f [Substs]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint [Point]
points [Point]
points' f [Substs] -> ([Substs] -> f Substs) -> f Substs
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Substs] -> f Substs
forall (f :: * -> *). MonadPlus f => [Substs] -> f Substs
mergeManySubsts
matchPoint Point
PointUnit Point
RSTT.PointUnit = Substs -> f Substs
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [] [])
matchPoint (PointPair Point
x Point
y) (RSTT.PointPair Point
x' Point
y') = do
  Substs
s1 <- Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint Point
x Point
x'
  Substs
s2 <- Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint Point
y Point
y'
  Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts Substs
s1 Substs
s2
matchPoint (PointFirst Point
x) (RSTT.PointFirst Point
x') = Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint Point
x Point
x'
matchPoint (PointSecond Point
x) (RSTT.PointSecond Point
x') = Point -> Point -> f Substs
forall (f :: * -> *). MonadPlus f => Point -> Point -> f Substs
matchPoint Point
x Point
x'
matchPoint Point
_ Point
_ = f Substs
forall (f :: * -> *) a. Alternative f => f a
empty

matchTopes
  :: (MonadPlus f, MonadFail f)
  => Substs -> [Tope] -> [RSTT.Tope] -> f (Substs, [RSTT.Tope])
matchTopes :: forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Substs -> [Tope] -> TopeContext -> f (Substs, TopeContext)
matchTopes Substs
substs [] TopeContext
leftover = (Substs, TopeContext) -> f (Substs, TopeContext)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Substs
substs, TopeContext
leftover)
matchTopes Substs
substs (Tope
tope:[Tope]
topes) TopeContext
topes' = do
  (Tope
tope'', TopeContext
topes'') <- TopeContext -> f (Tope, TopeContext)
forall (f :: * -> *) a.
(Alternative f, MonadFail f) =>
[a] -> f (a, [a])
Prover.selectOne TopeContext
topes'
  Substs
substs' <- Tope -> Tope -> f Substs
forall (f :: * -> *). MonadPlus f => Tope -> Tope -> f Substs
matchTope Tope
tope Tope
tope''
  Substs
substs'' <- Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts Substs
substs Substs
substs'
  Substs -> [Tope] -> TopeContext -> f (Substs, TopeContext)
forall (f :: * -> *).
(MonadPlus f, MonadFail f) =>
Substs -> [Tope] -> TopeContext -> f (Substs, TopeContext)
matchTopes Substs
substs'' [Tope]
topes TopeContext
topes''

mergeSubsts :: MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts :: forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts (Substs CubeContext
cubes [(Var, Point)]
points [(Var, Tope)]
topes) (Substs CubeContext
cubes' [(Var, Point)]
points' [(Var, Tope)]
topes') = CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs
  (CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs)
-> f CubeContext -> f ([(Var, Point)] -> [(Var, Tope)] -> Substs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CubeContext -> CubeContext -> f CubeContext
forall (f :: * -> *) k v.
(MonadPlus f, Eq k, Eq v, Show k, Show v) =>
[(k, v)] -> [(k, v)] -> f [(k, v)]
merge CubeContext
cubes CubeContext
cubes'
  f ([(Var, Point)] -> [(Var, Tope)] -> Substs)
-> f [(Var, Point)] -> f ([(Var, Tope)] -> Substs)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Var, Point)] -> [(Var, Point)] -> f [(Var, Point)]
forall (f :: * -> *) k v.
(MonadPlus f, Eq k, Eq v, Show k, Show v) =>
[(k, v)] -> [(k, v)] -> f [(k, v)]
merge [(Var, Point)]
points [(Var, Point)]
points'
  f ([(Var, Tope)] -> Substs) -> f [(Var, Tope)] -> f Substs
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [(Var, Tope)] -> [(Var, Tope)] -> f [(Var, Tope)]
forall (f :: * -> *) k v.
(MonadPlus f, Eq k, Eq v, Show k, Show v) =>
[(k, v)] -> [(k, v)] -> f [(k, v)]
merge [(Var, Tope)]
topes [(Var, Tope)]
topes'

mergeManySubsts :: MonadPlus f => [Substs] -> f Substs
mergeManySubsts :: forall (f :: * -> *). MonadPlus f => [Substs] -> f Substs
mergeManySubsts = (Substs -> Substs -> f Substs) -> Substs -> [Substs] -> f Substs
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Substs -> Substs -> f Substs
forall (f :: * -> *). MonadPlus f => Substs -> Substs -> f Substs
mergeSubsts (CubeContext -> [(Var, Point)] -> [(Var, Tope)] -> Substs
Substs [] [] [])

merge
  :: (MonadPlus f, Eq k, Eq v, Show k, Show v)
  => [(k, v)] -> [(k, v)] -> f [(k, v)]
merge :: forall (f :: * -> *) k v.
(MonadPlus f, Eq k, Eq v, Show k, Show v) =>
[(k, v)] -> [(k, v)] -> f [(k, v)]
merge [(k, v)]
xs [(k, v)]
ys
  | Bool
conflicts = f [(k, v)]
forall (f :: * -> *) a. Alternative f => f a
empty
  | Bool
otherwise = [(k, v)] -> f [(k, v)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(k, v)]
xs [(k, v)] -> [(k, v)] -> [(k, v)]
forall a. [a] -> [a] -> [a]
++ [(k, v)]
ys)
  where
    conflicts :: Bool
conflicts = ((k, v) -> Bool) -> [(k, v)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (k, v) -> Bool
conflict [(k, v)]
xs
    conflict :: (k, v) -> Bool
conflict (k
k, v
v) =
      case k -> [(k, v)] -> Maybe v
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup k
k [(k, v)]
ys of
        Maybe v
Nothing -> Bool
False
        Just v
v' -> v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
/= v
v'

normalizeSequent :: Prover.Sequent -> Prover.Sequent
normalizeSequent :: Sequent -> Sequent
normalizeSequent Prover.Sequent{CubeContext
TopeContext
Tope
sequentTope :: Tope
sequentTopeContext :: TopeContext
sequentCubeContext :: CubeContext
sequentTope :: Sequent -> Tope
sequentTopeContext :: Sequent -> TopeContext
sequentCubeContext :: Sequent -> CubeContext
..} = Sequent :: CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent
  { sequentCubeContext :: CubeContext
sequentCubeContext = CubeContext -> CubeContext
forall a. Ord a => [a] -> [a]
nubSort CubeContext
sequentCubeContext
  , sequentTopeContext :: TopeContext
sequentTopeContext = TopeContext -> TopeContext
forall a. Ord a => [a] -> [a]
nubSort TopeContext
sequentTopeContext
  , Tope
sequentTope :: Tope
sequentTope :: Tope
.. }

nubSort :: Ord a => [a] -> [a]
nubSort :: forall a. Ord a => [a] -> [a]
nubSort = Set a -> [a]
forall a. Set a -> [a]
Set.toList (Set a -> [a]) -> ([a] -> Set a) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList

applySubsts :: Substs -> Sequent -> Prover.Sequent
applySubsts :: Substs -> Sequent -> Sequent
applySubsts (Substs CubeContext
cubes [(Var, Point)]
points [(Var, Tope)]
topes) (Sequent CubeContext
cubeContext TopeContext
topeContext Tope
tope) =
  CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent
    (CubeContext -> CubeContext -> CubeContext
substInCubeContext CubeContext
cubes CubeContext
cubeContext)
    ([(Var, Point)] -> [(Var, Tope)] -> TopeContext -> TopeContext
substInTopeContext [(Var, Point)]
points [(Var, Tope)]
topes TopeContext
topeContext)
    ([(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope
substInTope [(Var, Point)]
points [(Var, Tope)]
topes Tope
tope)

substInCubeContext :: [(RSTT.Var, RSTT.Cube)] -> CubeContext -> RSTT.CubeContext
substInCubeContext :: CubeContext -> CubeContext -> CubeContext
substInCubeContext CubeContext
_ = CubeContext -> CubeContext
convertCubeContext -- FIXME

substInTopeContext :: [(RSTT.Var, RSTT.Point)] -> [(RSTT.Var, RSTT.Tope)] -> TopeContext -> RSTT.TopeContext
substInTopeContext :: [(Var, Point)] -> [(Var, Tope)] -> TopeContext -> TopeContext
substInTopeContext [(Var, Point)]
points [(Var, Tope)]
topes = \case
  TopeContext
TopeContextEmpty       -> []
  TopeContextNonEmpty [Tope]
ts -> (Tope -> Tope) -> [Tope] -> TopeContext
forall a b. (a -> b) -> [a] -> [b]
map ([(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope
substInTope [(Var, Point)]
points [(Var, Tope)]
topes) [Tope]
ts

substInTope :: [(RSTT.Var, RSTT.Point)] -> [(RSTT.Var, RSTT.Tope)] -> Tope -> RSTT.Tope
substInTope :: [(Var, Point)] -> [(Var, Tope)] -> Tope -> Tope
substInTope [(Var, Point)]
points [(Var, Tope)]
topes = Tope -> Tope
go
  where
    go :: Tope -> Tope
go = \case
      Tope
TopeTop         -> Tope
RSTT.TopeTop
      Tope
TopeBottom      -> Tope
RSTT.TopeBottom
      TopeVar (Var String
x) -> String -> Tope
lookupTope String
x
      TopeCon (Label String
con) [Point]
args -> Label -> [Point] -> Tope
RSTT.TopeCon (String -> Label
RSTT.Label String
con) ([Point] -> Tope) -> [Point] -> Tope
forall a b. (a -> b) -> a -> b
$
        (Point -> Point) -> [Point] -> [Point]
forall a b. (a -> b) -> [a] -> [b]
map ([(Var, Point)] -> Point -> Point
substInPoint [(Var, Point)]
points) [Point]
args
      TopeImplies Tope
x Tope
y -> Tope -> Tope -> Tope
RSTT.TopeImplies (Tope -> Tope
go Tope
x) (Tope -> Tope
go Tope
y)
      TopeOr Tope
x Tope
y      -> Tope -> Tope -> Tope
RSTT.TopeOr (Tope -> Tope
go Tope
x) (Tope -> Tope
go Tope
y)
      TopeAnd Tope
x Tope
y     -> Tope -> Tope -> Tope
RSTT.TopeAnd (Tope -> Tope
go Tope
x) (Tope -> Tope
go Tope
y)
      TopeEQ Point
x Point
y     -> Point -> Point -> Tope
RSTT.TopeEQ ([(Var, Point)] -> Point -> Point
substInPoint [(Var, Point)]
points Point
x) ([(Var, Point)] -> Point -> Point
substInPoint [(Var, Point)]
points Point
y)

    lookupTope :: String -> Tope
lookupTope String
x = Tope -> Maybe Tope -> Tope
forall a. a -> Maybe a -> a
fromMaybe (Var -> Tope
RSTT.TopeVar (String -> Var
RSTT.Var String
x)) (Maybe Tope -> Tope) -> Maybe Tope -> Tope
forall a b. (a -> b) -> a -> b
$
      Var -> [(Var, Tope)] -> Maybe Tope
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (String -> Var
RSTT.Var String
x) [(Var, Tope)]
topes

substInPoint :: [(RSTT.Var, RSTT.Point)] -> Point -> RSTT.Point
substInPoint :: [(Var, Point)] -> Point -> Point
substInPoint [(Var, Point)]
points = Point -> Point
go
  where
    go :: Point -> Point
go = \case
      Point
PointUnit        -> Point
RSTT.PointUnit
      PointVar (Var String
x) -> String -> Point
lookupPoint String
x
      PointCon (Label String
con) [Point]
args -> Label -> [Point] -> Point
RSTT.PointCon (String -> Label
RSTT.Label String
con) ([Point] -> Point) -> [Point] -> Point
forall a b. (a -> b) -> a -> b
$
        (Point -> Point) -> [Point] -> [Point]
forall a b. (a -> b) -> [a] -> [b]
map Point -> Point
go [Point]
args
      PointPair Point
x Point
y    -> Point -> Point -> Point
RSTT.PointPair (Point -> Point
go Point
x) (Point -> Point
go Point
y)
      PointFirst Point
x     -> Point -> Point
RSTT.PointFirst (Point -> Point
go Point
x)
      PointSecond Point
x    -> Point -> Point
RSTT.PointSecond (Point -> Point
go Point
x)

    lookupPoint :: String -> Point
lookupPoint String
x = Point -> Maybe Point -> Point
forall a. a -> Maybe a -> a
fromMaybe (Var -> Point
RSTT.PointVar (String -> Var
RSTT.Var String
x)) (Maybe Point -> Point) -> Maybe Point -> Point
forall a b. (a -> b) -> a -> b
$
      Var -> [(Var, Point)] -> Maybe Point
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (String -> Var
RSTT.Var String
x) [(Var, Point)]
points

-- ** Converting syntax

convertSequent :: Sequent -> Prover.Sequent
convertSequent :: Sequent -> Sequent
convertSequent (Sequent CubeContext
points TopeContext
topes Tope
tope) = CubeContext -> TopeContext -> Tope -> Sequent
Prover.Sequent
  (CubeContext -> CubeContext
convertCubeContext CubeContext
points)
  (TopeContext -> TopeContext
convertTopeContext TopeContext
topes)
  (Tope -> Tope
convertTope Tope
tope)

convertCubeContext :: CubeContext -> RSTT.CubeContext
convertCubeContext :: CubeContext -> CubeContext
convertCubeContext CubeContext
CubeContextEmpty = []
convertCubeContext (CubeContextNonEmpty [PointDecl]
pairs) = (PointDecl -> (Var, Cube)) -> [PointDecl] -> CubeContext
forall a b. (a -> b) -> [a] -> [b]
map PointDecl -> (Var, Cube)
convert [PointDecl]
pairs
  where
    convert :: PointDecl -> (Var, Cube)
convert (PointDecl (Var String
t) Cube
cube) = (String -> Var
RSTT.Var String
t, Cube -> Cube
convertCube Cube
cube)

convertCube :: Cube -> RSTT.Cube
convertCube :: Cube -> Cube
convertCube Cube
CubeUnit              = Cube
RSTT.CubeUnit
convertCube (CubeProduct Cube
i Cube
j)     = Cube -> Cube -> Cube
RSTT.CubeProduct (Cube -> Cube
convertCube Cube
i) (Cube -> Cube
convertCube Cube
j)
convertCube (CubeCon (Label String
con)) = Label -> Cube
RSTT.CubeCon (String -> Label
RSTT.Label String
con)
convertCube (CubeVar (Var String
i))     = Var -> Cube
RSTT.CubeVar (String -> Var
RSTT.Var String
i)

convertPoint :: Point -> RSTT.Point
convertPoint :: Point -> Point
convertPoint Point
PointUnit       = Point
RSTT.PointUnit
convertPoint (PointPair Point
t Point
s) = Point -> Point -> Point
RSTT.PointPair (Point -> Point
convertPoint Point
t) (Point -> Point
convertPoint Point
s)
convertPoint (PointFirst Point
t)  = Point -> Point
RSTT.PointFirst (Point -> Point
convertPoint Point
t)
convertPoint (PointSecond Point
t) = Point -> Point
RSTT.PointSecond (Point -> Point
convertPoint Point
t)
convertPoint (PointCon (Label String
con) [Point]
points)
  = Label -> [Point] -> Point
RSTT.PointCon (String -> Label
RSTT.Label String
con) ((Point -> Point) -> [Point] -> [Point]
forall a b. (a -> b) -> [a] -> [b]
map Point -> Point
convertPoint [Point]
points)
convertPoint (PointVar (Var String
i))     = Var -> Point
RSTT.PointVar (String -> Var
RSTT.Var String
i)

convertTope :: Tope -> RSTT.Tope
convertTope :: Tope -> Tope
convertTope Tope
TopeTop           = Tope
RSTT.TopeTop
convertTope Tope
TopeBottom        = Tope
RSTT.TopeBottom
convertTope (TopeImplies Tope
x Tope
y) = Tope -> Tope -> Tope
RSTT.TopeImplies (Tope -> Tope
convertTope Tope
x) (Tope -> Tope
convertTope Tope
y)
convertTope (TopeOr Tope
x Tope
y)      = Tope -> Tope -> Tope
RSTT.TopeOr (Tope -> Tope
convertTope Tope
x) (Tope -> Tope
convertTope Tope
y)
convertTope (TopeAnd Tope
x Tope
y)     = Tope -> Tope -> Tope
RSTT.TopeAnd (Tope -> Tope
convertTope Tope
x) (Tope -> Tope
convertTope Tope
y)
convertTope (TopeEQ Point
t Point
s)      = Point -> Point -> Tope
RSTT.TopeEQ (Point -> Point
convertPoint Point
t) (Point -> Point
convertPoint Point
s)
convertTope (TopeCon (Label String
con) [Point]
points)
  = Label -> [Point] -> Tope
RSTT.TopeCon (String -> Label
RSTT.Label String
con) ((Point -> Point) -> [Point] -> [Point]
forall a b. (a -> b) -> [a] -> [b]
map Point -> Point
convertPoint [Point]
points)
convertTope (TopeVar (Var String
phi)) = Var -> Tope
RSTT.TopeVar (String -> Var
RSTT.Var String
phi)

convertTopeContext :: TopeContext -> RSTT.TopeContext
convertTopeContext :: TopeContext -> TopeContext
convertTopeContext TopeContext
TopeContextEmpty            = []
convertTopeContext (TopeContextNonEmpty [Tope]
topes) = (Tope -> Tope) -> [Tope] -> TopeContext
forall a b. (a -> b) -> [a] -> [b]
map Tope -> Tope
convertTope [Tope]
topes