algo.hs

module UseInterpolation (useInterpolation) where
import Data.Maybe

data Formula = Not Formula | And [Formula] | Or [Formula] | T [Var] deriving Eq
data Binder = Binder Var Type [(Var,Var)] deriving Eq
data Var = V | S String deriving Eq
type Constraint = ([Binder], Type, Type)
data Type = Type { reft :: Formula } deriving Eq

interpolate :: Formula -> Formula -> IO Formula
interpolate = undefined

useInterpolation :: [Constraint] -> Constraint -> IO Formula
useInterpolation cons failCon = interpolate (And lhs) rhs
  where (gamma,l,r) = failCon
        rhs         = Not $ reft r
        lhs         = reft l:unwrap [] cons gamma

--only unwrap to 0th level
unwrap :: [Constraint] -> [Constraint] -> [Binder] -> [Formula]
unwrap visited cons bs = map unwrap1 bs
  where
    vs = map (\(Binder v _ _) -> v) bs
    unwrap1 (Binder var ĸ subs) = applySubs ((var,V):subs) $ rename vs formula
      where formula        = Or $ map recur cons'
            cons'          = filter undeep $ filter hasĸ cons
            undeep       x = x `notElem` visited
            recur  (g,l,_) = And (reft l:unwrap (visited++cons') cons g)
            hasĸ (_,_,rhs) = ĸ == rhs

applySubs :: [(Var,Var)] -> Formula -> Formula
applySubs subs = liftF sub
  where sub v  = fromMaybe v $ lookup v subs

rename :: [Var] -> Formula -> Formula
rename free f = applySubs subs f
  where bound = filterF (`notElem` free) f
        subs  = map ((,) fresh) bound
        fresh = undefined

liftF :: (Var -> Var) -> Formula -> Formula
liftF sub (Not  f) = Not (liftF sub f)
liftF sub (And fs) = And (map (liftF sub) fs)
liftF sub (Or  fs) = Or (map (liftF sub) fs)
liftF sub (T   vs) = T (map sub vs)

filterF :: (Var -> Bool) -> Formula -> [Var]
filterF sub (Not  f) = filterF sub f
filterF sub (And fs) = fs >>= filterF sub
filterF sub (Or  fs) = fs >>= filterF sub
filterF sub (T   vs) = filter sub vs