{-# LANGUAGE CPP #-}
#if __GLASGOW_HASKELL__ >= 610
{-# LANGUAGE ScopedTypeVariables #-}
#else
{-# LANGUAGE PatternSignatures #-}
#endif

module Language.Haskell.FreeTheorems.Unfold (
    asTheorem
  , asCompleteTheorem
  , unfoldFormula
  , unfoldLifts
  , unfoldClasses
) where



import Control.Monad (liftM)
import Control.Monad.State (StateT, get, put, evalStateT, evalState)
import Control.Monad.Reader (Reader, ask, local, runReader, runReaderT)
import Data.Generics (everything, extQ, listify, Data, mkQ)
import Data.List (unfoldr, nub, find, (\\), nubBy)
import Data.Map as Map (fromList)
import Data.Maybe (fromJust)

import Language.Haskell.FreeTheorems.BasicSyntax
import Language.Haskell.FreeTheorems.ValidSyntax
import Language.Haskell.FreeTheorems.LanguageSubsets
import Language.Haskell.FreeTheorems.Intermediate
import Language.Haskell.FreeTheorems.Theorems
import Language.Haskell.FreeTheorems.NameStores




------- Basic structures and functions ----------------------------------------


-- | Abbreviation for the state used to unfold relations to theorems.

type Unfolded a = StateT UnfoldedState (Reader (Bool,Bool)) a



-- | The state used to unfold relations to theorems.

data UnfoldedState = UnfoldedState 
  { UnfoldedState -> [String]
newVariableNames :: [String]
        -- ^ An infinite list storing names for variables.
        --   Every element of this list is distinct to the elements of
        --   'newFunctionNames1' and 'newFunctionNames2'.
  
  , UnfoldedState -> [String]
newFunctionNames1 :: [String]
        -- ^ An infinite list storing names for functions.
        --   Every element of this list is distinct to the elements of
        --   'newVariableNames' and 'newFunctionNames2'.

  , UnfoldedState -> [String]
newFunctionNames2 :: [String]
        -- ^ Another infinite list storing names for functions.
        --   Every element of this list is distinct to the elements of
        --   'newVariableNames' and 'newFunctionNames1'.
  }
  


-- | Create the initial name store which serves for creating new variable names.

initialState :: Intermediate -> UnfoldedState
initialState :: Intermediate -> UnfoldedState
initialState Intermediate
ir = 
  let fs :: [String]
fs = Intermediate -> String
intermediateName Intermediate
ir forall a. a -> [a] -> [a]
: Intermediate -> [String]
signatureNames Intermediate
ir
   in UnfoldedState
        { newVariableNames :: [String]
newVariableNames = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
fs) [String]
variableNameStore
          -- variable names must not equal the name of the intermediate
          -- variable names don't ever collide with function names or names of
          -- fixed type expressions (see 'NameStores' module)
  
        , newFunctionNames1 :: [String]
newFunctionNames1 = Intermediate -> [String]
functionVariableNames1 Intermediate
ir
          -- take the name store of functions which was already used during
          -- generation and modification of the intermediate relations

        , newFunctionNames2 :: [String]
newFunctionNames2 = Intermediate -> [String]
functionVariableNames2 Intermediate
ir
          -- take the name store of functions which was already used during
          -- generation and modification of the intermediate relations
        }
        


-- | Creates a new term variable. The name is chosen depending on the given
--   type expression, i.e. either a function variable name or a variable name
--   is returned.

newVariableFor :: TypeExpression -> Unfolded TermVariable
newVariableFor :: TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t = do
  case TypeExpression
t of
    TypeFun TypeExpression
_ TypeExpression
_    -> do UnfoldedState
state <- forall s (m :: * -> *). MonadState s m => m s
get
                         let ([String
f], [String]
fs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
1 (UnfoldedState -> [String]
newFunctionNames2 UnfoldedState
state)
                         forall s (m :: * -> *). MonadState s m => s -> m ()
put (UnfoldedState
state { newFunctionNames2 :: [String]
newFunctionNames2 = [String]
fs })
                         forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TermVariable
TVar String
f)

    TypeFunLab TypeExpression
_ TypeExpression
_ -> do UnfoldedState
state <- forall s (m :: * -> *). MonadState s m => m s
get
                         let ([String
f], [String]
fs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
1 (UnfoldedState -> [String]
newFunctionNames2 UnfoldedState
state)
                         forall s (m :: * -> *). MonadState s m => s -> m ()
put (UnfoldedState
state { newFunctionNames2 :: [String]
newFunctionNames2 = [String]
fs })
                         forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TermVariable
TVar String
f)
    
    TypeAbs TypeVariable
_ [TypeClass]
_ TypeExpression
t' -> TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t'
    
    TypeExpression
otherwise      -> do UnfoldedState
state <- forall s (m :: * -> *). MonadState s m => m s
get
                         let ([String
x], [String]
xs) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
1 (UnfoldedState -> [String]
newVariableNames UnfoldedState
state)
                         forall s (m :: * -> *). MonadState s m => s -> m ()
put (UnfoldedState
state { newVariableNames :: [String]
newVariableNames = [String]
xs })
                         forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TermVariable
TVar String
x)



-- | Checks if simplifications are possible.

simplificationsAllowed :: Unfolded Bool
simplificationsAllowed :: Unfolded Bool
simplificationsAllowed = do
  (Bool
simplificationPossible, Bool
allowAnySimplification) <- forall r (m :: * -> *). MonadReader r m => m r
ask
  if Bool
allowAnySimplification
    then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
simplificationPossible
    else forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False




-- | Toggles the simplification state in the unfolding of the argument.

toggleSimplifications :: Unfolded a -> Unfolded a
toggleSimplifications :: forall a. Unfolded a -> Unfolded a
toggleSimplifications = forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\(Bool
p,Bool
a) -> (Bool -> Bool
not Bool
p, Bool
a))





------- Unfolding formulas ----------------------------------------------------


-- | Unfolds an intermediate structure to a theorem.

asTheorem :: Intermediate -> Theorem
asTheorem :: Intermediate -> Theorem
asTheorem Intermediate
i = 
  let v :: Term
v = TermVariable -> Term
TermVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TermVariable
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Intermediate -> String
intermediateName forall a b. (a -> b) -> a -> b
$ Intermediate
i
      r :: Relation
r = Intermediate -> Relation
intermediateRelation Intermediate
i
      s :: UnfoldedState
s = Intermediate -> UnfoldedState
initialState Intermediate
i
   in forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula Term
v Term
v Relation
r) UnfoldedState
s) (Bool
True, Bool
True)


-- | Unfolds an intermediate structure to a theorem with _all_ restrictions.

asCompleteTheorem :: Intermediate -> Theorem
asCompleteTheorem :: Intermediate -> Theorem
asCompleteTheorem Intermediate
i = 
  let v :: Term
v = TermVariable -> Term
TermVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TermVariable
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Intermediate -> String
intermediateName forall a b. (a -> b) -> a -> b
$ Intermediate
i
      r :: Relation
r = Intermediate -> Relation
intermediateRelation Intermediate
i
      s :: UnfoldedState
s = Intermediate -> UnfoldedState
initialState Intermediate
i
   in forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula Term
v Term
v Relation
r) UnfoldedState
s) (Bool
True, Bool
False)


-- | Unfolds the logical relation "R" in the expression "(x,y) in R" to a
--   theorem. It works by recursively applying unfolding operations of
--   relational actions.

unfoldFormula :: Term -> Term -> Relation -> Unfolded Formula
unfoldFormula :: Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula Term
x Term
y Relation
rel = case Relation
rel of
  RelVar RelationInfo
_ RelationVariable
_           -> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate -> Theorem
Predicate forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Relation -> Predicate
IsMember Term
x Term
y forall a b. (a -> b) -> a -> b
$ Relation
rel
  FunVar RelationInfo
ri Either Term Term
term       -> Term
-> Term -> RelationInfo -> Either Term Term -> Unfolded Theorem
unfoldTerm Term
x Term
y RelationInfo
ri Either Term Term
term
  RelBasic RelationInfo
ri          -> Term -> Term -> RelationInfo -> Unfolded Theorem
unfoldBasic Term
x Term
y RelationInfo
ri
  RelLift RelationInfo
_ TypeConstructor
_ [Relation]
_        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate -> Theorem
Predicate forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term -> Relation -> Predicate
IsMember Term
x Term
y forall a b. (a -> b) -> a -> b
$ Relation
rel
  RelFun RelationInfo
ri Relation
r1 Relation
r2      -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFun Term
x Term
y RelationInfo
ri Relation
r1 Relation
r2
  RelFunLab RelationInfo
ri Relation
r1 Relation
r2   -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLab Term
x Term
y RelationInfo
ri Relation
r1 Relation
r2
  RelAbs RelationInfo
ri RelationVariable
v (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
r -> Term
-> Term
-> RelationInfo
-> RelationVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Unfolded Theorem
unfoldAbsRel Term
x Term
y RelationInfo
ri RelationVariable
v (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
r
  FunAbs RelationInfo
ri Either TermVariable TermVariable
v (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
r -> Term
-> Term
-> RelationInfo
-> Either TermVariable TermVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Unfolded Theorem
unfoldAbsFun Term
x Term
y RelationInfo
ri Either TermVariable TermVariable
v (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
r



-- | Unfolding operation for terms, i.e. relations specialised to functions.

unfoldTerm :: 
    Term -> Term -> RelationInfo -> Either Term Term -> Unfolded Formula
unfoldTerm :: Term
-> Term -> RelationInfo -> Either Term Term -> Unfolded Theorem
unfoldTerm Term
x Term
y RelationInfo
ri Either Term Term
term = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate -> Theorem
Predicate forall a b. (a -> b) -> a -> b
$
  case Either Term Term
term of
    Left Term
t  -> case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
                 TheoremType
EquationalTheorem   -> Term -> Term -> Predicate
IsEqual (Term -> Term -> Term
TermApp Term
t Term
x) Term
y
                 TheoremType
InequationalTheorem -> Term -> Term -> Predicate
IsLessEq (Term -> Term -> Term
TermApp Term
t Term
x) Term
y
    Right Term
t -> Term -> Term -> Predicate
IsLessEq Term
x (Term -> Term -> Term
TermApp Term
t Term
y)



-- | Unfolding operation for nullary relational actions.

unfoldBasic :: Term -> Term -> RelationInfo -> Unfolded Formula
unfoldBasic :: Term -> Term -> RelationInfo -> Unfolded Theorem
unfoldBasic Term
x Term
y RelationInfo
ri = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Predicate -> Theorem
Predicate forall a b. (a -> b) -> a -> b
$
  case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
    TheoremType
EquationalTheorem   -> Term -> Term -> Predicate
IsEqual  Term
x Term
y
    TheoremType
InequationalTheorem -> Term -> Term -> Predicate
IsLessEq Term
x Term
y
  


-- | Unfolding operation for relational actions of type abstractions.

unfoldAbsRel :: 
    Term -> Term -> RelationInfo 
    -> RelationVariable -> (TypeExpression, TypeExpression)
    -> [Restriction] -> Relation -> Unfolded Formula

unfoldAbsRel :: Term
-> Term
-> RelationInfo
-> RelationVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Unfolded Theorem
unfoldAbsRel Term
x Term
y RelationInfo
ri RelationVariable
v (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Relation
rel = do
  Theorem
rightSide <- Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> TypeExpression -> Term
TermIns Term
x TypeExpression
t1) (Term -> TypeExpression -> Term
TermIns Term
y TypeExpression
t2) Relation
rel
  forall (m :: * -> *) a. Monad m => a -> m a
return (RelationVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Theorem
-> Theorem
ForallRelations RelationVariable
v (TypeExpression
t1, TypeExpression
t2) [Restriction]
res Theorem
rightSide)



-- | Unfolding operation for relational actions of type abstractions
--   (for an abstraction of a function).

unfoldAbsFun :: 
    Term -> Term -> RelationInfo 
    -> Either TermVariable TermVariable -> (TypeExpression, TypeExpression)
    -> [Restriction] -> Relation -> Unfolded Formula

unfoldAbsFun :: Term
-> Term
-> RelationInfo
-> Either TermVariable TermVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Unfolded Theorem
unfoldAbsFun Term
x Term
y RelationInfo
ri Either TermVariable TermVariable
v (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Relation
rel = do
  Theorem
rightSide <- Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> TypeExpression -> Term
TermIns Term
x TypeExpression
t1) (Term -> TypeExpression -> Term
TermIns Term
y TypeExpression
t2) Relation
rel
  forall (m :: * -> *) a. Monad m => a -> m a
return (Either TermVariable TermVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Theorem
-> Theorem
ForallFunctions Either TermVariable TermVariable
v (TypeExpression
t1, TypeExpression
t2) [Restriction]
res Theorem
rightSide)



-- | Unfolding operation for relational actions of function type constructors.

unfoldFun :: 
    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula
unfoldFun :: Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFun Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2 =
  case Relation
rel1 of
    RelVar RelationInfo
_ RelationVariable
_          -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunPairs Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    FunVar RelationInfo
_ Either Term Term
t          -> 
      let ta :: Either (Term -> Term) (Term -> Term)
ta = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Term
t -> forall a b. a -> Either a b
Left (Term -> Term -> Term
TermApp Term
t)) (\Term
t -> forall a b. b -> Either a b
Right (Term -> Term -> Term
TermApp Term
t)) Either Term Term
t
          one :: Unfolded Theorem
one = Term
-> Term
-> RelationInfo
-> Either (Term -> Term) (Term -> Term)
-> Relation
-> Relation
-> Unfolded Theorem
unfoldFunOneVar Term
x Term
y RelationInfo
ri Either (Term -> Term) (Term -> Term)
ta Relation
rel1 Relation
rel2
          two :: Unfolded Theorem
two = Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
       in case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
            TheoremType
EquationalTheorem   -> Unfolded Theorem
one
            TheoremType
InequationalTheorem -> do
              Bool
simple <- Unfolded Bool
simplificationsAllowed
              if Bool
simple then Unfolded Theorem
one else Unfolded Theorem
two
    RelBasic RelationInfo
_          -> 
      case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
        TheoremType
EquationalTheorem   -> Term
-> Term
-> RelationInfo
-> Either (Term -> Term) (Term -> Term)
-> Relation
-> Relation
-> Unfolded Theorem
unfoldFunOneVar Term
x Term
y RelationInfo
ri (forall a b. a -> Either a b
Left forall a. a -> a
id) Relation
rel1 Relation
rel2
        TheoremType
InequationalTheorem -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelLift RelationInfo
_ TypeConstructor
_ [Relation]
_       -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunPairs Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelFun RelationInfo
_ Relation
_ Relation
_        -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelFunLab RelationInfo
_ Relation
_ Relation
_     -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelAbs RelationInfo
_ RelationVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
r Relation
_    -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    FunAbs RelationInfo
_ Either TermVariable TermVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
_ Relation
_    -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2

-- | Unfolding operation for relational actions of function type constructors.

unfoldFunLab :: 
    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula
unfoldFunLab :: Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLab Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2 =
  case Relation
rel1 of
    RelVar RelationInfo
_ RelationVariable
_          -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabPairs Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    FunVar RelationInfo
_ Either Term Term
t          -> 
      let ta :: Either (Term -> Term) (Term -> Term)
ta = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Term
t -> forall a b. a -> Either a b
Left (Term -> Term -> Term
TermApp Term
t)) (\Term
t -> forall a b. b -> Either a b
Right (Term -> Term -> Term
TermApp Term
t)) Either Term Term
t
          one :: Unfolded Theorem
one = Term
-> Term
-> RelationInfo
-> Either (Term -> Term) (Term -> Term)
-> Relation
-> Relation
-> Unfolded Theorem
unfoldFunLabOneVar Term
x Term
y RelationInfo
ri Either (Term -> Term) (Term -> Term)
ta Relation
rel1 Relation
rel2
          two :: Unfolded Theorem
two = Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
       in case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
            TheoremType
EquationalTheorem   -> Unfolded Theorem
one
            TheoremType
InequationalTheorem -> do
              Bool
simple <- Unfolded Bool
simplificationsAllowed
              if Bool
simple then Unfolded Theorem
one else Unfolded Theorem
two
    RelBasic RelationInfo
_          -> 
      case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
        TheoremType
EquationalTheorem   -> Term
-> Term
-> RelationInfo
-> Either (Term -> Term) (Term -> Term)
-> Relation
-> Relation
-> Unfolded Theorem
unfoldFunLabOneVar Term
x Term
y RelationInfo
ri (forall a b. a -> Either a b
Left forall a. a -> a
id) Relation
rel1 Relation
rel2
        TheoremType
InequationalTheorem -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelLift RelationInfo
_ TypeConstructor
_ [Relation]
_       -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabPairs Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelFun RelationInfo
_ Relation
_ Relation
_        -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelFunLab RelationInfo
_ Relation
_ Relation
_     -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    RelAbs RelationInfo
_ RelationVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
r Relation
_    -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2
    FunAbs RelationInfo
_ Either TermVariable TermVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
_ Relation
_    -> Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2



unfoldFunOneVar :: 
    Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term) 
    -> Relation -> Relation -> Unfolded Formula
unfoldFunOneVar :: Term
-> Term
-> RelationInfo
-> Either (Term -> Term) (Term -> Term)
-> Relation
-> Relation
-> Unfolded Theorem
unfoldFunOneVar Term
x Term
y RelationInfo
ri Either (Term -> Term) (Term -> Term)
termapp Relation
rel1 Relation
rel2 = do
  let t :: TypeExpression
t = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const (RelationInfo -> TypeExpression
relationLeftType (Relation -> RelationInfo
relationInfo Relation
rel1))) 
                 (forall a b. a -> b -> a
const (RelationInfo -> TypeExpression
relationRightType (Relation -> RelationInfo
relationInfo Relation
rel1)))
                 Either (Term -> Term) (Term -> Term)
termapp
  
  TermVariable
x' <- TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t
  let tx' :: Term
tx' = TermVariable -> Term
TermVar TermVariable
x'

  Theorem
f <- case Either (Term -> Term) (Term -> Term)
termapp of
         Left Term -> Term
t  -> Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x Term
tx') (Term -> Term -> Term
TermApp Term
y (Term -> Term
t Term
tx')) Relation
rel2
         Right Term -> Term
t -> Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x (Term -> Term
t Term
tx')) (Term -> Term -> Term
TermApp Term
y Term
tx') Relation
rel2

  Term -> Term -> LanguageSubset -> Theorem -> Unfolded Theorem
addRestriction Term
x Term
y (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) (TermVariable -> TypeExpression -> Theorem -> Theorem
ForallVariables TermVariable
x' TypeExpression
t Theorem
f)
--  return (ForallVariables x' t f)

unfoldFunLabOneVar :: 
    Term -> Term -> RelationInfo -> Either (Term -> Term) (Term -> Term) 
    -> Relation -> Relation -> Unfolded Formula
unfoldFunLabOneVar :: Term
-> Term
-> RelationInfo
-> Either (Term -> Term) (Term -> Term)
-> Relation
-> Relation
-> Unfolded Theorem
unfoldFunLabOneVar Term
x Term
y RelationInfo
ri Either (Term -> Term) (Term -> Term)
termapp Relation
rel1 Relation
rel2 = do
  let t :: TypeExpression
t = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const (RelationInfo -> TypeExpression
relationLeftType (Relation -> RelationInfo
relationInfo Relation
rel1))) 
                 (forall a b. a -> b -> a
const (RelationInfo -> TypeExpression
relationRightType (Relation -> RelationInfo
relationInfo Relation
rel1)))
                 Either (Term -> Term) (Term -> Term)
termapp
  
  TermVariable
x' <- TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t
  let tx' :: Term
tx' = TermVariable -> Term
TermVar TermVariable
x'

  Theorem
f <- case Either (Term -> Term) (Term -> Term)
termapp of
         Left Term -> Term
t  -> Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x Term
tx') (Term -> Term -> Term
TermApp Term
y (Term -> Term
t Term
tx')) Relation
rel2
         Right Term -> Term
t -> Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x (Term -> Term
t Term
tx')) (Term -> Term -> Term
TermApp Term
y Term
tx') Relation
rel2

-- addRestriction x y (relationLanguageSubset ri) (ForallVariables x' t f)
  forall (m :: * -> *) a. Monad m => a -> m a
return (TermVariable -> TypeExpression -> Theorem -> Theorem
ForallVariables TermVariable
x' TypeExpression
t Theorem
f)


unfoldFunPairs :: 
    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula
unfoldFunPairs :: Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunPairs Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2 = do
  TermVariable
x' <- TypeExpression -> Unfolded TermVariable
newVariableFor forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelationInfo -> TypeExpression
relationLeftType  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo forall a b. (a -> b) -> a -> b
$ Relation
rel1
  TermVariable
y' <- TypeExpression -> Unfolded TermVariable
newVariableFor forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelationInfo -> TypeExpression
relationRightType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo forall a b. (a -> b) -> a -> b
$ Relation
rel1

  Theorem
f  <- Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x (TermVariable -> Term
TermVar TermVariable
x')) (Term -> Term -> Term
TermApp Term
y (TermVariable -> Term
TermVar TermVariable
y')) Relation
rel2
  
  Term -> Term -> LanguageSubset -> Theorem -> Unfolded Theorem
addRestriction Term
x Term
y (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) ((TermVariable, TermVariable) -> Relation -> Theorem -> Theorem
ForallPairs (TermVariable
x', TermVariable
y') Relation
rel1 Theorem
f)
--  return (ForallPairs (x', y') rel1 f)

unfoldFunLabPairs :: 
    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula
unfoldFunLabPairs :: Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabPairs Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2 = do
  TermVariable
x' <- TypeExpression -> Unfolded TermVariable
newVariableFor forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelationInfo -> TypeExpression
relationLeftType  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo forall a b. (a -> b) -> a -> b
$ Relation
rel1
  TermVariable
y' <- TypeExpression -> Unfolded TermVariable
newVariableFor forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelationInfo -> TypeExpression
relationRightType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo forall a b. (a -> b) -> a -> b
$ Relation
rel1

  Theorem
f  <- Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x (TermVariable -> Term
TermVar TermVariable
x')) (Term -> Term -> Term
TermApp Term
y (TermVariable -> Term
TermVar TermVariable
y')) Relation
rel2
  
-- addRestriction x y (relationLanguageSubset ri) (ForallPairs (x', y') rel1 f)
  forall (m :: * -> *) a. Monad m => a -> m a
return ((TermVariable, TermVariable) -> Relation -> Theorem -> Theorem
ForallPairs (TermVariable
x', TermVariable
y') Relation
rel1 Theorem
f)


unfoldFunVars :: 
    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula
unfoldFunVars :: Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2 = do
  let t1 :: TypeExpression
t1 = RelationInfo -> TypeExpression
relationLeftType (Relation -> RelationInfo
relationInfo Relation
rel1)
  let t2 :: TypeExpression
t2 = RelationInfo -> TypeExpression
relationRightType (Relation -> RelationInfo
relationInfo Relation
rel1)

  TermVariable
x' <- TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t1
  TermVariable
y' <- TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t2

  Theorem
l  <- forall a. Unfolded a -> Unfolded a
toggleSimplifications (Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (TermVariable -> Term
TermVar TermVariable
x') (TermVariable -> Term
TermVar TermVariable
y') Relation
rel1)
  Theorem
r  <- Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x (TermVariable -> Term
TermVar TermVariable
x')) (Term -> Term -> Term
TermApp Term
y (TermVariable -> Term
TermVar TermVariable
y')) Relation
rel2

  let f :: Theorem
f = TermVariable -> TypeExpression -> Theorem -> Theorem
ForallVariables TermVariable
x' TypeExpression
t1 (TermVariable -> TypeExpression -> Theorem -> Theorem
ForallVariables TermVariable
y' TypeExpression
t2 (Theorem -> Theorem -> Theorem
Implication Theorem
l Theorem
r))
  Term -> Term -> LanguageSubset -> Theorem -> Unfolded Theorem
addRestriction Term
x Term
y (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) Theorem
f
--  return f


unfoldFunLabVars :: 
    Term -> Term -> RelationInfo -> Relation -> Relation -> Unfolded Formula
unfoldFunLabVars :: Term
-> Term -> RelationInfo -> Relation -> Relation -> Unfolded Theorem
unfoldFunLabVars Term
x Term
y RelationInfo
ri Relation
rel1 Relation
rel2 = do
  let t1 :: TypeExpression
t1 = RelationInfo -> TypeExpression
relationLeftType (Relation -> RelationInfo
relationInfo Relation
rel1)
  let t2 :: TypeExpression
t2 = RelationInfo -> TypeExpression
relationRightType (Relation -> RelationInfo
relationInfo Relation
rel1)

  TermVariable
x' <- TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t1
  TermVariable
y' <- TypeExpression -> Unfolded TermVariable
newVariableFor TypeExpression
t2

  Theorem
l  <- forall a. Unfolded a -> Unfolded a
toggleSimplifications (Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (TermVariable -> Term
TermVar TermVariable
x') (TermVariable -> Term
TermVar TermVariable
y') Relation
rel1)
  Theorem
r  <- Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula (Term -> Term -> Term
TermApp Term
x (TermVariable -> Term
TermVar TermVariable
x')) (Term -> Term -> Term
TermApp Term
y (TermVariable -> Term
TermVar TermVariable
y')) Relation
rel2

  let f :: Theorem
f = TermVariable -> TypeExpression -> Theorem -> Theorem
ForallVariables TermVariable
x' TypeExpression
t1 (TermVariable -> TypeExpression -> Theorem -> Theorem
ForallVariables TermVariable
y' TypeExpression
t2 (Theorem -> Theorem -> Theorem
Implication Theorem
l Theorem
r))
  forall (m :: * -> *) a. Monad m => a -> m a
return Theorem
f


addRestriction :: Term -> Term -> LanguageSubset -> Formula -> Unfolded Formula
addRestriction :: Term -> Term -> LanguageSubset -> Theorem -> Unfolded Theorem
addRestriction Term
x Term
y LanguageSubset
l Theorem
f = do
  Bool
simple <- Unfolded Bool
simplificationsAllowed
  case LanguageSubset
l of
    SubsetWithSeq TheoremType
EquationalTheorem -> 
      if Bool
simple
        then forall (m :: * -> *) a. Monad m => a -> m a
return Theorem
f
        else let botrefl :: Theorem
botrefl = Theorem -> Theorem -> Theorem
Equivalence (Predicate -> Theorem
Predicate (Term -> Predicate
IsNotBot Term
x))
                                       (Predicate -> Theorem
Predicate (Term -> Predicate
IsNotBot Term
y))
              in forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Theorem -> Theorem -> Theorem
Conjunction Theorem
botrefl Theorem
f
    SubsetWithSeq TheoremType
InequationalTheorem -> 
      if Bool
simple
        then forall (m :: * -> *) a. Monad m => a -> m a
return Theorem
f
        else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Theorem -> Theorem -> Theorem
Conjunction (Theorem -> Theorem -> Theorem
Implication (Predicate -> Theorem
Predicate (Term -> Predicate
IsNotBot Term
x)) 
                                               (Predicate -> Theorem
Predicate (Term -> Predicate
IsNotBot Term
y))) Theorem
f
    LanguageSubset
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return Theorem
f





------- Unfold lifts ----------------------------------------------------------


-- | Extracts all lift relations and returns their definition.

unfoldLifts :: [ValidDeclaration] -> Intermediate -> [UnfoldedLift]  
unfoldLifts :: [ValidDeclaration] -> Intermediate -> [UnfoldedLift]
unfoldLifts [ValidDeclaration]
vds Intermediate
i =
  let decls :: [Declaration]
decls = forall a b. (a -> b) -> [a] -> [b]
map ValidDeclaration -> Declaration
rawDeclaration [ValidDeclaration]
vds
      rs :: [Relation]
rs = forall a. Data a => a -> [Relation]
collectLifts (Intermediate -> Relation
intermediateRelation Intermediate
i)

      recUnfold :: [Relation] -> [Relation] -> [UnfoldedLift]
recUnfold [Relation]
done [Relation]
rs = let ([UnfoldedLift]
us, [[Relation]]
ms) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> b) -> [a] -> [b]
map Relation -> (UnfoldedLift, [Relation])
unfold [Relation]
rs)
                              ns :: [Relation]
ns = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Relation]]
ms forall a. Eq a => [a] -> [a] -> [a]
\\ ([Relation]
done forall a. [a] -> [a] -> [a]
++ [Relation]
rs)
                           in if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Relation]
ns
                                then [UnfoldedLift]
us
                                else [UnfoldedLift]
us forall a. [a] -> [a] -> [a]
++ [Relation] -> [Relation] -> [UnfoldedLift]
recUnfold ([Relation]
done forall a. [a] -> [a] -> [a]
++ [Relation]
rs) [Relation]
ns
      
      unfold :: Relation -> (UnfoldedLift, [Relation])
unfold Relation
r = case Relation
r of 
                   RelLift RelationInfo
ri TypeConstructor
con [Relation]
rs -> let ([UnfoldedDataCon]
u,[Relation]
ms) = [Declaration]
-> RelationInfo
-> TypeConstructor
-> [Relation]
-> ([UnfoldedDataCon], [Relation])
unfoldDecl [Declaration]
decls RelationInfo
ri TypeConstructor
con [Relation]
rs
                                         in (Relation -> [UnfoldedDataCon] -> UnfoldedLift
UnfoldedLift Relation
r [UnfoldedDataCon]
u, [Relation]
ms)
      
      eqLift :: UnfoldedLift -> UnfoldedLift -> Bool
eqLift (UnfoldedLift Relation
r1 [UnfoldedDataCon]
_) (UnfoldedLift Relation
r2 [UnfoldedDataCon]
_) = Relation
r1 forall a. Eq a => a -> a -> Bool
== Relation
r2
  in forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy UnfoldedLift -> UnfoldedLift -> Bool
eqLift forall a b. (a -> b) -> a -> b
$ [Relation] -> [Relation] -> [UnfoldedLift]
recUnfold [] [Relation]
rs



collectLifts :: Data a => a -> [Relation]
collectLifts :: forall a. Data a => a -> [Relation]
collectLifts = forall a. Eq a => [a] -> [a]
nub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify Relation -> Bool
isLift
  where
    isLift :: Relation -> Bool
isLift Relation
rel = case Relation
rel of
      RelLift RelationInfo
_ TypeConstructor
_ [Relation]
_ -> Bool
True
      Relation
otherwise     -> Bool
False



unfoldDecl :: 
    [Declaration] -> RelationInfo -> TypeConstructor -> [Relation] 
    -> ([UnfoldedDataCon], [Relation])
unfoldDecl :: [Declaration]
-> RelationInfo
-> TypeConstructor
-> [Relation]
-> ([UnfoldedDataCon], [Relation])
unfoldDecl [Declaration]
decls RelationInfo
ri TypeConstructor
con [Relation]
rs = 
  let botPair :: [UnfoldedDataCon]
botPair = case RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri of
                  LanguageSubset
BasicSubset -> []
                  LanguageSubset
otherwise   -> [UnfoldedDataCon
BotPair]
      vars :: Char -> a -> [TermVariable]
vars Char
t a
n = forall a b. (a -> b) -> [a] -> [b]
map (\a
i -> String -> TermVariable
TVar (Char
t forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show a
i)) [a
1..a
n]
   in case TypeConstructor
con of
        TypeConstructor
ConList    -> ([UnfoldedDataCon]
botPair forall a. [a] -> [a] -> [a]
++ RelationInfo -> Relation -> [UnfoldedDataCon]
unfoldList RelationInfo
ri (forall a. [a] -> a
head [Relation]
rs), [])
        ConTuple Int
n -> ([UnfoldedDataCon]
botPair forall a. [a] -> [a] -> [a]
++ [Int -> [Relation] -> UnfoldedDataCon
unfoldTuple Int
n [Relation]
rs], [])
        TypeConstructor
otherwise  -> 
          let d :: Declaration
d = forall a. HasCallStack => Maybe a -> a
fromJust (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (TypeConstructor -> Declaration -> Bool
isDeclOf TypeConstructor
con) [Declaration]
decls)
           in case Declaration
d of
                DataDecl DataDeclaration
d'    -> 
                  let ucs :: [UnfoldedDataCon]
ucs = forall a b. (a -> b) -> [a] -> [b]
map ([TypeVariable]
-> [Relation] -> DataConstructorDeclaration -> UnfoldedDataCon
unfoldCon (DataDeclaration -> [TypeVariable]
dataVars DataDeclaration
d') [Relation]
rs) (DataDeclaration -> [DataConstructorDeclaration]
dataCons DataDeclaration
d')
                   in ([UnfoldedDataCon]
botPair forall a. [a] -> [a] -> [a]
++ [UnfoldedDataCon]
ucs, forall a. Data a => a -> [Relation]
collectLifts [UnfoldedDataCon]
ucs)
                NewtypeDecl NewtypeDeclaration
d' -> 
                  let uc :: UnfoldedDataCon
uc = [TypeVariable]
-> [Relation] -> DataConstructorDeclaration -> UnfoldedDataCon
unfoldCon (NewtypeDeclaration -> [TypeVariable]
newtypeVars NewtypeDeclaration
d') [Relation]
rs 
                                     (Identifier -> [BangTypeExpression] -> DataConstructorDeclaration
DataCon (NewtypeDeclaration -> Identifier
newtypeCon NewtypeDeclaration
d') 
                                              [TypeExpression -> BangTypeExpression
Unbanged (NewtypeDeclaration -> TypeExpression
newtypeRhs NewtypeDeclaration
d')])
                   in ([UnfoldedDataCon
uc], forall a. Data a => a -> [Relation]
collectLifts UnfoldedDataCon
uc)
  where
    isDeclOf :: TypeConstructor -> Declaration -> Bool
isDeclOf (Con Identifier
c) Declaration
d = case Declaration
d of
      DataDecl DataDeclaration
_    -> Declaration -> Identifier
getDeclarationName Declaration
d forall a. Eq a => a -> a -> Bool
== Identifier
c
      NewtypeDecl NewtypeDeclaration
_ -> Declaration -> Identifier
getDeclarationName Declaration
d forall a. Eq a => a -> a -> Bool
== Identifier
c
      Declaration
otherwise     -> Bool
False



unfoldList :: RelationInfo -> Relation -> [UnfoldedDataCon]
unfoldList :: RelationInfo -> Relation -> [UnfoldedDataCon]
unfoldList RelationInfo
ri Relation
rel = 
  let x :: TermVariable
x  = String -> TermVariable
TVar String
"x"
      y :: TermVariable
y  = String -> TermVariable
TVar String
"y"
      xs :: TermVariable
xs = String -> TermVariable
TVar String
"xs"
      ys :: TermVariable
ys = String -> TermVariable
TVar String
"ys"
      vs :: [TermVariable]
vs = forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (\(TermVariable
_::TermVariable) -> Bool
True) Relation
rel
      fs :: [String]
fs = forall a b. (a -> b) -> [a] -> [b]
map (\(TVar String
v) -> String
v) (TermVariable
xforall a. a -> [a] -> [a]
:TermVariable
yforall a. a -> [a] -> [a]
:TermVariable
xsforall a. a -> [a] -> [a]
:TermVariable
ysforall a. a -> [a] -> [a]
:[TermVariable]
vs) 
   in [ DataConstructor -> UnfoldedDataCon
ConPair DataConstructor
DConEmptyList
      , DataConstructor
-> [TermVariable] -> [TermVariable] -> Theorem -> UnfoldedDataCon
ConMore DataConstructor
DConConsList [TermVariable
x,TermVariable
xs] [TermVariable
y,TermVariable
ys]
            (Theorem -> Theorem -> Theorem
Conjunction ([String] -> (Term, Term, Relation) -> Theorem
unfoldFormulaEx [String]
fs (TermVariable -> Term
TermVar TermVariable
x, TermVariable -> Term
TermVar TermVariable
y, Relation
rel))
                         (Predicate -> Theorem
Predicate (Term -> Term -> Relation -> Predicate
IsMember (TermVariable -> Term
TermVar TermVariable
xs) (TermVariable -> Term
TermVar TermVariable
ys) 
                                              (RelationInfo -> TypeConstructor -> [Relation] -> Relation
RelLift RelationInfo
ri TypeConstructor
ConList [Relation
rel]))))
      ]


unfoldTuple :: Int -> [Relation] -> UnfoldedDataCon
unfoldTuple :: Int -> [Relation] -> UnfoldedDataCon
unfoldTuple Int
n [Relation]
rs = 
  let xs :: [TermVariable]
xs = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> String -> TermVariable
TVar (Char
'x' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
i)) [Int
1..Int
n]
      ys :: [TermVariable]
ys = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> String -> TermVariable
TVar (Char
'y' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
i)) [Int
1..Int
n]
      vs :: [TermVariable]
vs = forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (\(TermVariable
_::TermVariable) -> Bool
True) [Relation]
rs
      fs :: [String]
fs = forall a b. (a -> b) -> [a] -> [b]
map (\(TVar String
v) -> String
v) ([TermVariable]
xs forall a. [a] -> [a] -> [a]
++ [TermVariable]
ys forall a. [a] -> [a] -> [a]
++ [TermVariable]
vs)
      txs :: [Term]
txs = forall a b. (a -> b) -> [a] -> [b]
map TermVariable -> Term
TermVar [TermVariable]
xs
      tys :: [Term]
tys = forall a b. (a -> b) -> [a] -> [b]
map TermVariable -> Term
TermVar [TermVariable]
ys
      th :: Theorem
th = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Theorem -> Theorem -> Theorem
Conjunction (forall a b. (a -> b) -> [a] -> [b]
map ([String] -> (Term, Term, Relation) -> Theorem
unfoldFormulaEx [String]
fs) (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Term]
txs [Term]
tys [Relation]
rs))
   in DataConstructor
-> [TermVariable] -> [TermVariable] -> Theorem -> UnfoldedDataCon
ConMore (Int -> DataConstructor
DConTuple Int
n) [TermVariable]
xs [TermVariable]
ys Theorem
th



unfoldCon :: 
    [TypeVariable] -> [Relation] -> DataConstructorDeclaration 
    -> UnfoldedDataCon
unfoldCon :: [TypeVariable]
-> [Relation] -> DataConstructorDeclaration -> UnfoldedDataCon
unfoldCon [TypeVariable]
vs [Relation]
rs (DataCon Identifier
name [BangTypeExpression]
ts) =
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [BangTypeExpression]
ts
    then DataConstructor -> UnfoldedDataCon
ConPair (String -> DataConstructor
DCon (Identifier -> String
unpackIdent Identifier
name))
    else let n :: Int
n  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [BangTypeExpression]
ts
             xs :: [TermVariable]
xs = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> String -> TermVariable
TVar (Char
'x' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
i)) [Int
1..Int
n]
             ys :: [TermVariable]
ys = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> String -> TermVariable
TVar (Char
'y' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
i)) [Int
1..Int
n]
             is :: [Relation]
is = forall a b. (a -> b) -> [a] -> [b]
map (([String], [TypeExpression])
-> [TypeVariable] -> [Relation] -> TypeExpression -> Relation
interpretEx ([], []) [TypeVariable]
vs [Relation]
rs forall b c a. (b -> c) -> (a -> b) -> a -> c
. BangTypeExpression -> TypeExpression
withoutBang) [BangTypeExpression]
ts
             os :: [TermVariable]
os = forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (\(TermVariable
_::TermVariable) -> Bool
True) [Relation]
rs
             fs :: [String]
fs = forall a b. (a -> b) -> [a] -> [b]
map (\(TVar String
v) -> String
v) ([TermVariable]
xs forall a. [a] -> [a] -> [a]
++ [TermVariable]
ys forall a. [a] -> [a] -> [a]
++ [TermVariable]
os)
             txs :: [Term]
txs = forall a b. (a -> b) -> [a] -> [b]
map TermVariable -> Term
TermVar [TermVariable]
xs
             tys :: [Term]
tys = forall a b. (a -> b) -> [a] -> [b]
map TermVariable -> Term
TermVar [TermVariable]
ys
             th :: Theorem
th = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Theorem -> Theorem -> Theorem
Conjunction (forall a b. (a -> b) -> [a] -> [b]
map ([String] -> (Term, Term, Relation) -> Theorem
unfoldFormulaEx [String]
fs) 
                                          (forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Term]
txs [Term]
tys [Relation]
is))
          in DataConstructor
-> [TermVariable] -> [TermVariable] -> Theorem -> UnfoldedDataCon
ConMore (String -> DataConstructor
DCon (Identifier -> String
unpackIdent Identifier
name)) [TermVariable]
xs [TermVariable]
ys Theorem
th
                              




unfoldFormulaEx :: 
    [String] -> (Term, Term, Relation) -> Formula
unfoldFormulaEx :: [String] -> (Term, Term, Relation) -> Theorem
unfoldFormulaEx [String]
forbidden (Term
x, Term
y, Relation
rel) = 
  let s :: UnfoldedState
s = UnfoldedState
          { newVariableNames :: [String]
newVariableNames = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
forbidden) [String]
variableNameStore
          , newFunctionNames1 :: [String]
newFunctionNames1 = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
forbidden) [String]
functionNameStore1
          , newFunctionNames2 :: [String]
newFunctionNames2 = forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
forbidden) [String]
functionNameStore2
          }
   in forall r a. Reader r a -> r -> a
runReader (forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Term -> Term -> Relation -> Unfolded Theorem
unfoldFormula Term
x Term
y Relation
rel) UnfoldedState
s) (Bool
True, Bool
False)
                                                    

interpretEx :: 
    ([String], [TypeExpression]) -> [TypeVariable] -> [Relation] 
    -> TypeExpression -> Relation
interpretEx :: ([String], [TypeExpression])
-> [TypeVariable] -> [Relation] -> TypeExpression -> Relation
interpretEx ([String], [TypeExpression])
ns [TypeVariable]
vs [Relation]
rs TypeExpression
t = 
  let e :: Map TypeVariable Relation
e = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a b. [a] -> [b] -> [(a, b)]
zip [TypeVariable]
vs [Relation]
rs)
      l :: LanguageSubset
l = RelationInfo -> LanguageSubset
relationLanguageSubset forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [Relation]
rs
   in forall s a. State s a -> s -> a
evalState (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (LanguageSubset
-> TypeExpression
-> ReaderT
     (Map TypeVariable Relation)
     (State ([String], [TypeExpression]))
     Relation
interpretM LanguageSubset
l TypeExpression
t) Map TypeVariable Relation
e) ([String], [TypeExpression])
ns






------- Exported functions ----------------------------------------------------


-- | Extracts all class constraints and returns their definition.

unfoldClasses :: [ValidDeclaration] -> Intermediate -> [UnfoldedClass]
unfoldClasses :: [ValidDeclaration] -> Intermediate -> [UnfoldedClass]
unfoldClasses [ValidDeclaration]
vds Intermediate
i = 
  let ds :: [Declaration]
ds = forall a b. (a -> b) -> [a] -> [b]
map ValidDeclaration -> Declaration
rawDeclaration [ValidDeclaration]
vds
      cs :: [(Relation, TypeClass)]
cs = forall a. Data a => a -> [(Relation, TypeClass)]
collectClasses (Intermediate -> Relation
intermediateRelation Intermediate
i)
      ns :: [String]
ns = forall a b. (a -> b) -> [a] -> [b]
map (\(TVar String
n) -> String
n) (forall r. Typeable r => (r -> Bool) -> GenericQ [r]
listify (\(TermVariable
_::TermVariable) -> Bool
True) [(Relation, TypeClass)]
cs)
      fs :: [String]
fs = Intermediate -> [String]
signatureNames Intermediate
i forall a. [a] -> [a] -> [a]
++ [Intermediate -> String
intermediateName Intermediate
i] forall a. [a] -> [a] -> [a]
++ [String]
ns
      rs :: ([String], [TypeExpression])
rs = Intermediate -> ([String], [TypeExpression])
interpretNameStore Intermediate
i
      
      recUnfold :: [(Relation, TypeClass)]
-> [(Relation, TypeClass)] -> [UnfoldedClass]
recUnfold [(Relation, TypeClass)]
done [(Relation, TypeClass)]
cs =
        let ([UnfoldedClass]
us, [[(Relation, TypeClass)]]
os) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a b. (a -> b) -> [a] -> [b]
map (([String], [TypeExpression])
-> [Declaration]
-> [String]
-> (Relation, TypeClass)
-> (UnfoldedClass, [(Relation, TypeClass)])
unfoldClass ([String], [TypeExpression])
rs [Declaration]
ds [String]
fs) [(Relation, TypeClass)]
cs)
            done' :: [(Relation, TypeClass)]
done' = [(Relation, TypeClass)]
done forall a. [a] -> [a] -> [a]
++ [(Relation, TypeClass)]
cs 
            ns :: [(Relation, TypeClass)]
ns = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Relation, TypeClass)]]
os forall a. Eq a => [a] -> [a] -> [a]
\\ [(Relation, TypeClass)]
done'
         in if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Relation, TypeClass)]
ns
              then [UnfoldedClass]
us
              else [UnfoldedClass]
us forall a. [a] -> [a] -> [a]
++ [(Relation, TypeClass)]
-> [(Relation, TypeClass)] -> [UnfoldedClass]
recUnfold [(Relation, TypeClass)]
done' [(Relation, TypeClass)]
ns

   in [(Relation, TypeClass)]
-> [(Relation, TypeClass)] -> [UnfoldedClass]
recUnfold [] [(Relation, TypeClass)]
cs



collectClasses :: Data a => a -> [(Relation, TypeClass)]
collectClasses :: forall a. Data a => a -> [(Relation, TypeClass)]
collectClasses = forall a. Eq a => [a] -> [a]
nub forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything forall a. [a] -> [a] -> [a]
(++) ([] forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
`mkQ` Relation -> [(Relation, TypeClass)]
getCC)
  where
    getCC :: Relation -> [(Relation, TypeClass)]
getCC Relation
rel = case Relation
rel of
      RelAbs RelationInfo
ri RelationVariable
rv (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Relation
_ -> 
        let cs :: [TypeClass]
cs  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Restriction -> [TypeClass]
getClasses [Restriction]
res
            ri' :: RelationInfo
ri' = RelationInfo
ri { relationLeftType :: TypeExpression
relationLeftType = TypeExpression
t1
                     , relationRightType :: TypeExpression
relationRightType = TypeExpression
t2 }
            r :: Relation
r   = RelationInfo -> RelationVariable -> Relation
RelVar RelationInfo
ri' RelationVariable
rv
         in forall a b. (a -> b) -> [a] -> [b]
map (\TypeClass
c -> (Relation
r, TypeClass
c)) [TypeClass]
cs
      FunAbs RelationInfo
ri Either TermVariable TermVariable
fv (TypeExpression
t1, TypeExpression
t2) [Restriction]
res Relation
_ ->
        let cs :: [TypeClass]
cs  = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Restriction -> [TypeClass]
getClasses [Restriction]
res
            ri' :: RelationInfo
ri' = RelationInfo
ri { relationLeftType :: TypeExpression
relationLeftType = TypeExpression
t1
                     , relationRightType :: TypeExpression
relationRightType = TypeExpression
t2 }
            r :: Relation
r   = RelationInfo -> Either Term Term -> Relation
FunVar RelationInfo
ri' (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermVariable -> Term
TermVar) (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermVariable -> Term
TermVar) Either TermVariable TermVariable
fv)
         in forall a b. (a -> b) -> [a] -> [b]
map (\TypeClass
c -> (Relation
r, TypeClass
c)) [TypeClass]
cs
      Relation
otherwise           -> []

    getClasses :: Restriction -> [TypeClass]
getClasses Restriction
r = case Restriction
r of
      RespectsClasses [TypeClass]
tcs -> [TypeClass]
tcs
      Restriction
otherwise           -> []



unfoldClass :: 
    ([String], [TypeExpression]) -> [Declaration] -> [String] 
    -> (Relation, TypeClass) -> (UnfoldedClass, [(Relation, TypeClass)])
unfoldClass :: ([String], [TypeExpression])
-> [Declaration]
-> [String]
-> (Relation, TypeClass)
-> (UnfoldedClass, [(Relation, TypeClass)])
unfoldClass ([String], [TypeExpression])
istore [Declaration]
decls [String]
forbiddenNames (Relation
r, c :: TypeClass
c@(TC Identifier
name)) =
  let ClassDecl ClassDeclaration
d = forall a. HasCallStack => Maybe a -> a
fromJust (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Declaration
d -> Declaration -> Identifier
getDeclarationName Declaration
d forall a. Eq a => a -> a -> Bool
== Identifier
name) [Declaration]
decls)
      ri :: RelationInfo
ri = Relation -> RelationInfo
relationInfo Relation
r

      interpretSig :: Signature -> Relation
interpretSig Signature
s = ([String], [TypeExpression])
-> [TypeVariable] -> [Relation] -> TypeExpression -> Relation
interpretEx ([String], [TypeExpression])
istore [ClassDeclaration -> TypeVariable
classVar ClassDeclaration
d] [Relation
r] (Signature -> TypeExpression
signatureType Signature
s)
      
      methodName :: Signature -> Term
methodName = TermVariable -> Term
TermVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TermVariable
TVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> String
unpackIdent forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> Identifier
signatureName
      leftMethod :: Signature -> Term
leftMethod Signature
s = Term -> TypeExpression -> Term
TermIns (Signature -> Term
methodName Signature
s) (RelationInfo -> TypeExpression
relationLeftType RelationInfo
ri)
      rightMethod :: Signature -> Term
rightMethod Signature
s = Term -> TypeExpression -> Term
TermIns (Signature -> Term
methodName Signature
s) (RelationInfo -> TypeExpression
relationRightType RelationInfo
ri)
      
      asFormula :: Signature -> Theorem
asFormula Signature
s = [String] -> (Term, Term, Relation) -> Theorem
unfoldFormulaEx
                      [String]
forbiddenNames 
                      (Signature -> Term
leftMethod Signature
s, Signature -> Term
rightMethod Signature
s, Signature -> Relation
interpretSig Signature
s)

      fs :: [Theorem]
fs = forall a b. (a -> b) -> [a] -> [b]
map Signature -> Theorem
asFormula (ClassDeclaration -> [Signature]
classFuns ClassDeclaration
d)

      ps :: [(Relation, TypeClass)]
ps = forall a b. (a -> b) -> [a] -> [b]
map (\TypeClass
c -> (Relation
r,TypeClass
c)) (ClassDeclaration -> [TypeClass]
superClasses ClassDeclaration
d)
      ds :: [(Relation, TypeClass)]
ds = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a. Data a => a -> [(Relation, TypeClass)]
collectClasses [Theorem]
fs

      v :: Either RelationVariable TermVariable
v = case Relation
r of
            RelVar RelationInfo
_ RelationVariable
rv -> forall a b. a -> Either a b
Left RelationVariable
rv
            FunVar RelationInfo
_ Either Term Term
fv -> forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TermVariable
unterm) (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> TermVariable
unterm) Either Term Term
fv
      unterm :: Term -> TermVariable
unterm (TermVar TermVariable
v) = TermVariable
v
   
   in ([TypeClass]
-> TypeClass
-> Either RelationVariable TermVariable
-> [Theorem]
-> UnfoldedClass
UnfoldedClass (ClassDeclaration -> [TypeClass]
superClasses ClassDeclaration
d) TypeClass
c Either RelationVariable TermVariable
v [Theorem]
fs, [(Relation, TypeClass)]
ps forall a. [a] -> [a] -> [a]
++ [(Relation, TypeClass)]
ds)