A new approach to the skolem escape check

skolems.hs

module Main where

import Data.Maybe (fromMaybe)

import Control.Monad (liftM, liftM2)

data Term
  = TmVar Int
  | TmSkolem Int Int Int
  | TmPair Term Term
  | TmLeft Term
  | TmRight Term
  | TmUnit
  deriving (Show, Eq, Ord)

newtype Subst = Subst { runSubst :: Int -> Term } 

ext :: Int -> Term -> Subst -> Subst
ext v t s = Subst $ \i -> replace i v t (runSubst s i)

newtype Constraint = Constraint { runConstraint :: (Int, Term) } deriving (Show, Eq)

unify :: Term -> Term -> [Constraint]
unify (TmVar v1) (TmVar v2) | v1 == v2 = []
unify t@(TmSkolem lo _ hi) (TmVar v) 
  | lo <= v && v <= hi = [Constraint (v, t)]
  | otherwise = error "Escaped skolem" 
unify v@(TmVar _) t@(TmSkolem _ _ _) = unify t v
unify (TmVar v) t = [Constraint (v, t)]
unify t (TmVar v) = [Constraint (v, t)]
unify (TmPair a1 b1) (TmPair a2 b2) = 
  unify a1 a2 ++ unify b1 b2
unify (TmLeft  t1) (TmLeft  t2) = unify t1 t2
unify (TmRight t1) (TmRight t2) = unify t1 t2
unify TmUnit TmUnit = []
unify _ _ = error "Cannot unify"

replace :: Int -> Int -> Term -> Term -> Term
replace i v t = go
  where
  go :: Term -> Term
  go (TmVar v') | v == v' = t
  go (TmSkolem lo _ hi) | lo > v || v > hi = error "Escaped skolem"
  go (TmPair t1 t2) = TmPair (go t1) (go t2)
  go (TmLeft t) = TmLeft (go t)
  go (TmRight t) = TmRight (go t)
  go other = other

solve :: [Constraint] -> Subst 
solve cs = go cs (Subst TmVar) where
  go :: [Constraint] -> Subst -> Subst
  go [] s = s
  go (c@(Constraint (i, x)) : cs) s =
    go (substConstraints c cs) (ext i x s)

  substConstraints :: Constraint -> [Constraint] -> [Constraint]
  substConstraints c [] = []
  substConstraints c@(Constraint (i, x)) (Constraint (j, y) : cs) 
    | i == j = substConstraints c cs ++ unify x y
    | otherwise = Constraint (j, replace j i x y) : substConstraints c cs

data State = State 
  { stateNextVar :: Int
  , stateNextSkolem :: Int
  } deriving (Show)

type Goal = State -> Result

data Result = Result
  { resultConstraints :: [Constraint]
  , resultState :: State
  } deriving (Show) 

fresh :: (Term -> Goal) -> Goal
fresh f s =
  let 
    nm = stateNextVar s
    s' = State (nm + 1) (stateNextSkolem s)
  in 
    f (TmVar nm) s'

eigen :: (Term -> Goal) -> Goal
eigen f (State lo sk) = 
  let 
    t  = TmSkolem lo sk hi
    r  = f t (State lo (sk + 1))
    hi = stateNextVar $ resultState r
  in r

(===) :: Term -> Term -> Goal
(===) t1 t2 s = Result (unify t1 t2) s

conj :: Goal -> Goal -> Goal
conj g1 g2 s0 =
  let
    Result cs1 s1 = g1 s0
    Result cs2 s2 = g2 s1
  in
    Result (cs1 ++ cs2) s2

runGoal :: Goal -> [Term]
runGoal g =
  let 
    r = g (State 0 0)
    s = solve $ resultConstraints r
  in
    [ runSubst s v | v <- [0..] ]