{-# LANGUAGE FlexibleContexts #-}

-- | Declares an intermediate data structure along with a function to transform
--   type signatures into the intermediate structure. There are also other
--   functions working on intermediate structures, namely to retrieve relation
--   variables and to instantiate them to functions.

module Language.Haskell.FreeTheorems.Intermediate (
    Intermediate (..)
  , interpret
  , interpretM
  , relationVariables
  , specialise
  , specialiseInverse
) where



import Control.Monad (liftM, liftM2, mapM)
import Control.Monad.Reader (ReaderT, ask, runReaderT, local)
import Control.Monad.State (State, get, put, runState)
import Control.Monad.Trans (lift)
import Data.Generics ( Typeable, Data, everywhere, everything, listify, mkT
                     , mkQ, extQ)
import qualified Data.Map as Map (Map, empty, lookup, insert, map)
import Data.Maybe (fromMaybe)

import Language.Haskell.FreeTheorems.LanguageSubsets
import Language.Haskell.FreeTheorems.Syntax 
import Language.Haskell.FreeTheorems.ValidSyntax
import Language.Haskell.FreeTheorems.Theorems
import Language.Haskell.FreeTheorems.Frontend.TypeExpressions
    ( substituteTypeVariables )
import Language.Haskell.FreeTheorems.NameStores 
    ( relationNameStore, typeExpressionNameStore, functionNameStore1, functionNameStore2 )

------- Intermediate data structure -------------------------------------------


-- | A structure describing the intermediate result of interpreting a type
--   expression as a relation.

data Intermediate = Intermediate 
  { Intermediate -> String
intermediateName      :: String 
        -- ^ The name of the symbol for which the theorem is to be generated.
  
  , Intermediate -> LanguageSubset
intermediateSubset    :: LanguageSubset
        -- ^ The language subset in which the theorem is to be generated.
  
  , Intermediate -> Relation
intermediateRelation :: Relation
        -- ^ The relation obtained from the type.
  
  , Intermediate -> [String]
functionVariableNames1 :: [String]
        -- ^ A name store for new, fresh function names.
        --   This is needed because functions can be specialised step-by-step
        --   after having generated the first relation from a type.

  , Intermediate -> [String]
functionVariableNames2 :: [String]
        -- ^ Another name store for new, fresh function names, disjoint from
        --   the one above.

  , Intermediate -> [String]
signatureNames :: [String]
        -- ^ The names of all known signatures. These names must not be used to
        --   generate names of functions and variables.
  
  , Intermediate -> NameStore
interpretNameStore :: NameStore 
        -- ^ A name store to generate new relation variables and type
        --   expressions.
  
  }





------- Interpret types as relations ------------------------------------------



-- | Interprets a valid signature as a relation. This is the key point for
--   generating free theorems.

interpret :: 
    [ValidDeclaration] -> LanguageSubset -> ValidSignature -> Maybe Intermediate
interpret :: [ValidDeclaration]
-> LanguageSubset -> ValidSignature -> Maybe Intermediate
interpret [ValidDeclaration]
vds LanguageSubset
l ValidSignature
s =
  let n :: String
n  = Identifier -> String
unpackIdent forall b c a. (b -> c) -> (a -> b) -> a -> c
. Signature -> Identifier
signatureName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidSignature -> Signature
rawSignature forall a b. (a -> b) -> a -> b
$ ValidSignature
s
      ss :: [String]
ss = [Declaration] -> [String]
getSignatureNames (forall a b. (a -> b) -> [a] -> [b]
map ValidDeclaration -> Declaration
rawDeclaration [ValidDeclaration]
vds)
      fs :: [String]
fs = String
n forall a. a -> [a] -> [a]
: [String]
ss
      t :: TypeExpression
t  = Signature -> TypeExpression
signatureType forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidSignature -> Signature
rawSignature forall a b. (a -> b) -> a -> b
$ ValidSignature
s
      (Relation
i, NameStore
rs) = forall s a. State s a -> s -> (a, s)
runState (forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT (LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t) forall k a. Map k a
Map.empty) ([String] -> NameStore
initialState [String]
fs)
      r :: Intermediate
r = String
-> LanguageSubset
-> Relation
-> [String]
-> [String]
-> [String]
-> NameStore
-> Intermediate
Intermediate String
n LanguageSubset
l Relation
i (forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
fs) [String]
functionNameStore1) (forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
fs) [String]
functionNameStore2) [String]
ss NameStore
rs
   in case LanguageSubset
l of
        SubsetWithSeq TheoremType
_ -> forall a. a -> Maybe a
Just Intermediate
r
        LanguageSubset
otherwise       -> if [ValidDeclaration] -> ValidSignature -> Bool
containsStrictTypes [ValidDeclaration]
vds ValidSignature
s 
                             then forall a. Maybe a
Nothing
                             else forall a. a -> Maybe a
Just Intermediate
r
  where
    getSignatureNames :: [Declaration] -> [String]
getSignatureNames = 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` Signature -> [String]
getSigName)
    getSigName :: Signature -> [String]
getSigName (Signature Identifier
i TypeExpression
_) = [Identifier -> String
unpackIdent Identifier
i]

    containsStrictTypes :: [ValidDeclaration] -> ValidSignature -> Bool
containsStrictTypes [ValidDeclaration]
vds ValidSignature
s = 
      let rs :: Signature
rs = ValidSignature -> Signature
rawSignature ValidSignature
s
          ns :: [Identifier]
ns = 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` TypeConstructor -> [Identifier]
getCons forall a b q.
(Typeable a, Typeable b) =>
(a -> q) -> (b -> q) -> a -> q
`extQ` TypeClass -> [Identifier]
getClasses) Signature
rs
          ds :: [Identifier]
ds = forall a b. (a -> b) -> [a] -> [b]
map (Declaration -> Identifier
getDeclarationName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValidDeclaration -> Declaration
rawDeclaration) 
                   (forall a. (a -> Bool) -> [a] -> [a]
filter ValidDeclaration -> Bool
isStrictDeclaration [ValidDeclaration]
vds)
          isStrict :: Identifier -> Bool
isStrict Identifier
n = Identifier
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Identifier]
ds
       in forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Identifier -> Bool
isStrict [Identifier]
ns

    getCons :: TypeConstructor -> [Identifier]
getCons TypeConstructor
c = case TypeConstructor
c of { Con Identifier
n -> [Identifier
n] ; TypeConstructor
otherwise -> [] }
    getClasses :: TypeClass -> [Identifier]
getClasses (TC Identifier
n) = [Identifier
n]



-- | Transforms a type expression into a relation. The environment is used to
--   map seen type variables to newly created relation variables. The state
--   serves for creating relation variables.

interpretM :: 
    LanguageSubset 
    -> TypeExpression 
    -> ReaderT Environment (State NameStore) Relation

interpretM :: LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t = case TypeExpression
t of

    -- get the environment from the reader, lookup the relation variable for
    -- the given type variable (this operation will never fail because
    -- in the initial type expression, all occurring type variables are bound
    -- by type abstraction which are resolved by updating the environment, see
    -- below) and create a relation consisting solely of the relation variable
  TypeVar TypeVariable
v -> forall a. a -> Maybe a -> a
fromMaybe (forall a. HasCallStack => String -> a
error String
"Data.Map.lookup: Key not found") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TypeVariable
v forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *). MonadReader r m => m r
ask

    -- either create a basic relation or a lift relation, depending on the
    -- subtypes
  TypeCon TypeConstructor
c [TypeExpression]
ts -> do
    [Relation]
rs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l) [TypeExpression]
ts   -- interpret the subtypes
    RelationInfo
ri <- forall {m :: * -> *}.
MonadReader Environment m =>
LanguageSubset -> TypeExpression -> m RelationInfo
mkRelationInfo LanguageSubset
l TypeExpression
t       -- create the relation info

        -- checks if an intermediate relation is a basic case
    let basic :: Relation -> Bool
basic Relation
rel = case Relation
rel of { RelBasic RelationInfo
_ -> Bool
True ; Relation
otherwise -> Bool
False }

        -- create a basic intermediate relation if all subrelations are basic
        -- (or if there is no subrelation), otherwise create a lifted relation
    if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Relation -> Bool
basic [Relation]
rs
      then forall (m :: * -> *) a. Monad m => a -> m a
return (RelationInfo -> Relation
RelBasic (LanguageSubset -> TypeExpression -> TypeExpression -> RelationInfo
RelationInfo LanguageSubset
l TypeExpression
t TypeExpression
t))
      else forall (m :: * -> *) a. Monad m => a -> m a
return (RelationInfo -> TypeConstructor -> [Relation] -> Relation
RelLift RelationInfo
ri TypeConstructor
c [Relation]
rs)

    -- create a relation for function types
  TypeFun TypeExpression
t1 TypeExpression
t2 -> do
    RelationInfo
ri <- forall {m :: * -> *}.
MonadReader Environment m =>
LanguageSubset -> TypeExpression -> m RelationInfo
mkRelationInfo LanguageSubset
l TypeExpression
t       -- create the relation info
    forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (RelationInfo -> Relation -> Relation -> Relation
RelFun RelationInfo
ri) (LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t1) (LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t2)

    -- create a second relation for function types (used only for language
    -- subset with seq and the equational setting
  TypeFunLab TypeExpression
t1 TypeExpression
t2 -> do
    RelationInfo
ri <- forall {m :: * -> *}.
MonadReader Environment m =>
LanguageSubset -> TypeExpression -> m RelationInfo
mkRelationInfo LanguageSubset
l TypeExpression
t       -- create the relation info
    forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (RelationInfo -> Relation -> Relation -> Relation
RelFunLab RelationInfo
ri) (LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t1) (LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t2)

    -- create a relation for type abstractions
  TypeAbs TypeVariable
v [TypeClass]
cs TypeExpression
t' -> do
    RelationInfo
ri <- forall {m :: * -> *}.
MonadReader Environment m =>
LanguageSubset -> TypeExpression -> m RelationInfo
mkRelationInfo LanguageSubset
l TypeExpression
t                    -- create the relation info
    (RelationVariable
rv, TypeExpression
t1, TypeExpression
t2) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State NameStore (RelationVariable, TypeExpression, TypeExpression)
newRelationVariable    -- create a new variable
    let rvar :: Relation
rvar = RelationInfo -> RelationVariable -> Relation
RelVar (LanguageSubset -> TypeExpression -> TypeExpression -> RelationInfo
RelationInfo LanguageSubset
l TypeExpression
t1 TypeExpression
t2) RelationVariable
rv
    Relation
r  <- forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TypeVariable
v Relation
rvar) forall a b. (a -> b) -> a -> b
$ LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t'  -- subrelations
    let res :: [Restriction]
res = LanguageSubset -> [Restriction]
relRes LanguageSubset
l forall a. [a] -> [a] -> [a]
++ (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
cs then [] else [[TypeClass] -> Restriction
RespectsClasses [TypeClass]
cs])
    forall (m :: * -> *) a. Monad m => a -> m a
return (RelationInfo
-> RelationVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Relation
RelAbs RelationInfo
ri RelationVariable
rv (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Relation
r)

    -- create a second relation for type abstractions (used only for language
    -- subset with seq and the equational setting
  TypeAbsLab TypeVariable
v [TypeClass]
cs TypeExpression
t' -> do
    RelationInfo
ri <- forall {m :: * -> *}.
MonadReader Environment m =>
LanguageSubset -> TypeExpression -> m RelationInfo
mkRelationInfo LanguageSubset
l TypeExpression
t                    -- create the relation info
    (RelationVariable
rv, TypeExpression
t1, TypeExpression
t2) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift State NameStore (RelationVariable, TypeExpression, TypeExpression)
newRelationVariable    -- create a new variable
    let rvar :: Relation
rvar = RelationInfo -> RelationVariable -> Relation
RelVar (LanguageSubset -> TypeExpression -> TypeExpression -> RelationInfo
RelationInfo LanguageSubset
l TypeExpression
t1 TypeExpression
t2) RelationVariable
rv
    Relation
r  <- forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TypeVariable
v Relation
rvar) forall a b. (a -> b) -> a -> b
$ LanguageSubset
-> TypeExpression
-> ReaderT Environment (StateT NameStore Identity) Relation
interpretM LanguageSubset
l TypeExpression
t'  -- subrelations
    let res :: [Restriction]
res = (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Restriction
BottomReflecting) (LanguageSubset -> [Restriction]
relRes LanguageSubset
l)) forall a. [a] -> [a] -> [a]
++ (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeClass]
cs then [] else [[TypeClass] -> Restriction
RespectsClasses [TypeClass]
cs])
    forall (m :: * -> *) a. Monad m => a -> m a
return (RelationInfo
-> RelationVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Relation
RelAbs RelationInfo
ri RelationVariable
rv (TypeExpression
t1,TypeExpression
t2) [Restriction]
res Relation
r)

  where
    mkRelationInfo :: LanguageSubset -> TypeExpression -> m RelationInfo
mkRelationInfo LanguageSubset
l TypeExpression
t = do
      Environment
env <- forall r (m :: * -> *). MonadReader r m => m r
ask
        -- create the 'left' and 'right' type expression of 't',
        -- i.e. replace all free variables by the left or right type
        -- expressions of the corresponding relation variable
      let getLt :: Relation -> TypeExpression
getLt = RelationInfo -> TypeExpression
relationLeftType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo
      let getRt :: Relation -> TypeExpression
getRt = RelationInfo -> TypeExpression
relationRightType forall b c a. (b -> c) -> (a -> b) -> a -> c
. Relation -> RelationInfo
relationInfo
      let lt :: TypeExpression
lt = Map TypeVariable TypeExpression -> TypeExpression -> TypeExpression
substituteTypeVariables (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Relation -> TypeExpression
getLt Environment
env) TypeExpression
t
      let rt :: TypeExpression
rt = Map TypeVariable TypeExpression -> TypeExpression -> TypeExpression
substituteTypeVariables (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Relation -> TypeExpression
getRt Environment
env) TypeExpression
t
      forall (m :: * -> *) a. Monad m => a -> m a
return (LanguageSubset -> TypeExpression -> TypeExpression -> RelationInfo
RelationInfo LanguageSubset
l TypeExpression
lt TypeExpression
rt)


    -- Returns the restrictions for relations, depending on the current
    -- language subset and theorem type.
    relRes :: LanguageSubset -> [Restriction]
relRes LanguageSubset
l = case LanguageSubset
l of
      LanguageSubset
BasicSubset                       -> [ ]
      SubsetWithFix TheoremType
EquationalTheorem   -> [ Restriction
Strict, Restriction
Continuous ]
      SubsetWithFix TheoremType
InequationalTheorem -> [ Restriction
Strict, Restriction
Continuous
                                           , Restriction
LeftClosed ]
      SubsetWithSeq TheoremType
EquationalTheorem   -> [ Restriction
Strict, Restriction
Continuous
                                           , Restriction
BottomReflecting ]
      SubsetWithSeq TheoremType
InequationalTheorem -> [ Restriction
Strict, Restriction
Continuous, Restriction
Total
                                           , Restriction
LeftClosed ]
   




------- Helper definitions for the interpretation -----------------------------


-- | An environment mapping type variables to intermediate relation variables
--   (stored as relations).

type Environment = Map.Map TypeVariable Relation 



-- | Represents the names of future variable names. The first component provides
--   names for relations, while the second component provides names for type
--   expressions.

type NameStore = ([String], [TypeExpression])



-- | Initialises the name store. Both components of the name store are infinite
--   list.
--   For more information, see 'Language.Haskell.FreeTheorems.NameStore'.

initialState :: [String] -> NameStore
initialState :: [String] -> NameStore
initialState [String]
ns = 
   ( [String]
relationNameStore
   , forall a b. (a -> b) -> [a] -> [b]
map (FixedTypeExpression -> TypeExpression
TypeExp forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identifier -> FixedTypeExpression
TF forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Identifier
Ident) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
ns)
         forall a b. (a -> b) -> a -> b
$ [String]
typeExpressionNameStore )



-- | Creates a new relation variable using the name store.

newRelationVariable :: 
    State NameStore (RelationVariable, TypeExpression, TypeExpression)
newRelationVariable :: State NameStore (RelationVariable, TypeExpression, TypeExpression)
newRelationVariable = do
  ([String]
rvs, [TypeExpression]
ts) <- forall s (m :: * -> *). MonadState s m => m s
get
  let ([String
rv], [String]
rvs') = forall a. Int -> [a] -> ([a], [a])
splitAt Int
1 [String]
rvs
  let ([TypeExpression
t1, TypeExpression
t2], [TypeExpression]
ts') = forall a. Int -> [a] -> ([a], [a])
splitAt Int
2 [TypeExpression]
ts
  forall s (m :: * -> *). MonadState s m => s -> m ()
put ([String]
rvs', [TypeExpression]
ts') 
  forall (m :: * -> *) a. Monad m => a -> m a
return (String -> RelationVariable
RVar String
rv, TypeExpression
t1, TypeExpression
t2)





------- Instantiation of relation variables -----------------------------------


-- | Creates a list of all bound relation variables in an intermediate
--   structure, which can be specialised to a function. 

relationVariables :: Intermediate -> [RelationVariable]
relationVariables :: Intermediate -> [RelationVariable]
relationVariables (Intermediate String
_ LanguageSubset
_ Relation
rel [String]
_ [String]
_ [String]
_ NameStore
_) = Bool -> Relation -> [RelationVariable]
getRVar Bool
True Relation
rel
  where
    getRVar :: Bool -> Relation -> [RelationVariable]
getRVar Bool
ok Relation
rel = case Relation
rel of
      RelLift RelationInfo
_ TypeConstructor
_ [Relation]
rs    -> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> Relation -> [RelationVariable]
getRVar Bool
ok) [Relation]
rs
      RelFun RelationInfo
_ Relation
r1 Relation
r2    -> Bool -> Relation -> [RelationVariable]
getRVar (Bool -> Bool
not Bool
ok) Relation
r1 forall a. [a] -> [a] -> [a]
++ Bool -> Relation -> [RelationVariable]
getRVar Bool
ok Relation
r2
      RelFunLab RelationInfo
_ Relation
r1 Relation
r2 -> Bool -> Relation -> [RelationVariable]
getRVar (Bool -> Bool
not Bool
ok) Relation
r1 forall a. [a] -> [a] -> [a]
++ Bool -> Relation -> [RelationVariable]
getRVar Bool
ok Relation
r2
      RelAbs RelationInfo
_ RelationVariable
rv (TypeExpression, TypeExpression)
_ [Restriction]
_ Relation
r -> (if Bool
ok then [RelationVariable
rv] else []) forall a. [a] -> [a] -> [a]
++ Bool -> Relation -> [RelationVariable]
getRVar Bool
ok Relation
r
      FunAbs RelationInfo
_ Either TermVariable TermVariable
_ (TypeExpression, TypeExpression)
_ [Restriction]
_ Relation
r  -> Bool -> Relation -> [RelationVariable]
getRVar Bool
ok Relation
r 
      Relation
otherwise         -> []



-- | Specialises a relation variable to a function variable in an intermediate
--   structure.

specialise :: Intermediate -> RelationVariable -> Intermediate
specialise :: Intermediate -> RelationVariable -> Intermediate
specialise Intermediate
ir RelationVariable
rv = Intermediate -> Intermediate
reduceLifts (Intermediate
-> RelationVariable
-> (TermVariable -> Either TermVariable TermVariable)
-> Intermediate
replaceRelVar Intermediate
ir RelationVariable
rv forall a b. a -> Either a b
Left)



-- | Specialises a relation variable to an inverse function variable.
--   This function does not modify intermediate structures in subsets with
--   equational theorems.

specialiseInverse :: Intermediate -> RelationVariable -> Intermediate
specialiseInverse :: Intermediate -> RelationVariable -> Intermediate
specialiseInverse Intermediate
ir RelationVariable
rv = 
  case LanguageSubset -> TheoremType
theoremType (Intermediate -> LanguageSubset
intermediateSubset Intermediate
ir) of
    TheoremType
EquationalTheorem   -> Intermediate
ir
    TheoremType
InequationalTheorem -> Intermediate -> Intermediate
reduceLifts  (Intermediate
-> RelationVariable
-> (TermVariable -> Either TermVariable TermVariable)
-> Intermediate
replaceRelVar Intermediate
ir RelationVariable
rv forall a b. b -> Either a b
Right)



-- | Replaces a relation variable with a function variable.

replaceRelVar :: 
    Intermediate -> RelationVariable 
    -> (TermVariable -> Either TermVariable TermVariable) -> Intermediate
replaceRelVar :: Intermediate
-> RelationVariable
-> (TermVariable -> Either TermVariable TermVariable)
-> Intermediate
replaceRelVar Intermediate
ir (RVar String
rv) TermVariable -> Either TermVariable TermVariable
leftOrRight =
  let ([String
funName], [String]
fns) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
1 (Intermediate -> [String]
functionVariableNames1 Intermediate
ir)
      fv :: Either TermVariable TermVariable
fv = TermVariable -> Either TermVariable TermVariable
leftOrRight forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TermVariable
TVar forall a b. (a -> b) -> a -> b
$ String
funName
      relation :: Relation
relation = Intermediate -> Relation
intermediateRelation Intermediate
ir
   in Intermediate
ir { intermediateRelation :: Relation
intermediateRelation  = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT forall a b. (a -> b) -> a -> b
$ String -> Either TermVariable TermVariable -> Relation -> Relation
replace String
rv Either TermVariable TermVariable
fv) Relation
relation
         , functionVariableNames1 :: [String]
functionVariableNames1 = forall a. Int -> [a] -> [a]
drop Int
1 (Intermediate -> [String]
functionVariableNames1 Intermediate
ir)
         }
  where
    -- perform the actual replacement
    -- when replacing a relation by a 'right' function in a relation
    -- abstraction, the types have to be flipped
    replace :: String -> Either TermVariable TermVariable -> Relation -> Relation
replace String
rv Either TermVariable TermVariable
fv Relation
rel = case Relation
rel of
      RelVar RelationInfo
ri (RVar String
r) -> 
        let tv :: Either Term Term
tv = 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 if String
rv forall a. Eq a => a -> a -> Bool
== String
r then RelationInfo -> Either Term Term -> Relation
FunVar RelationInfo
ri Either Term Term
tv else Relation
rel
      RelAbs RelationInfo
ri (RVar String
r) (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
rel' ->
        let res'' :: [Restriction]
res'' = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const [Restriction]
funResL) (forall a b. a -> b -> a
const [Restriction]
funResR) Either TermVariable TermVariable
fv
            -- hack! should be somehow better implemented
	    -- if BottomReflecting is not present, we had
            -- TypeAbsLab quantification in (SubsetWithSeq Equational)
            res' :: [Restriction]
res'  = if forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Restriction
BottomReflecting [Restriction]
res Bool -> Bool -> Bool
|| forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Restriction
Total [Restriction]
res then [Restriction]
res'' else forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Restriction
Total) [Restriction]
res''
         in if String
rv forall a. Eq a => a -> a -> Bool
== String
r
              then RelationInfo
-> Either TermVariable TermVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Relation
FunAbs RelationInfo
ri Either TermVariable TermVariable
fv (TypeExpression, TypeExpression)
ts ([Restriction]
res' forall a. [a] -> [a] -> [a]
++ ([Restriction] -> [Restriction]
classConstraints [Restriction]
res)) Relation
rel'
              else Relation
rel
      Relation
otherwise -> Relation
rel

    -- the restrictions for functions in the equational setting and for
    -- 'left' functions in inequational settings
    funResL :: [Restriction]
funResL = case Intermediate -> LanguageSubset
intermediateSubset Intermediate
ir of
      LanguageSubset
BasicSubset     -> [ ]
      SubsetWithFix TheoremType
_ -> [ Restriction
Strict ]
      SubsetWithSeq TheoremType
_ -> [ Restriction
Strict, Restriction
Total ]
    
    -- the restrictions for 'right' functions in the inequational settings
    funResR :: [Restriction]
funResR = case Intermediate -> LanguageSubset
intermediateSubset Intermediate
ir of
      LanguageSubset
BasicSubset     -> [ ]
      SubsetWithFix TheoremType
_ -> [ ]
      SubsetWithSeq TheoremType
_ -> [ Restriction
Strict ]

    -- returns the class constraints
    classConstraints :: [Restriction] -> [Restriction]
classConstraints [Restriction]
res = forall a. (a -> Bool) -> [a] -> [a]
filter Restriction -> Bool
isCC [Restriction]
res
      where 
        isCC :: Restriction -> Bool
isCC Restriction
r = case Restriction
r of { RespectsClasses [TypeClass]
_ -> Bool
True ; Restriction
otherwise -> Bool
False }



-- | Applies simplifications on lifted constructors. 
--   If the argument is a function then lifted lists are replaced by map and
--   lifted Maybes are replaced by fmap.

reduceLifts :: Intermediate -> Intermediate
reduceLifts :: Intermediate -> Intermediate
reduceLifts Intermediate
ir = 
--  ir { intermediateRelation = reduceEverywhere (intermediateRelation ir) }
  Intermediate
ir { intermediateRelation :: Relation
intermediateRelation = Bool -> Relation -> Relation
re Bool
True (Intermediate -> Relation
intermediateRelation Intermediate
ir) }
  where
--    reduceEverywhere = everywhere (mkT reduce)

    re :: Bool -> Relation -> Relation
re Bool
ok Relation
rel = case Relation
rel of
      RelLift RelationInfo
ri TypeConstructor
con [Relation]
rs     -> if Bool
ok 
                                 then Relation -> Relation
reduce (RelationInfo -> TypeConstructor -> [Relation] -> Relation
RelLift RelationInfo
ri TypeConstructor
con (forall a b. (a -> b) -> [a] -> [b]
map (Bool -> Relation -> Relation
re Bool
ok) [Relation]
rs))
                                 else Relation
rel
      RelFun RelationInfo
ri Relation
r1 Relation
r2       -> RelationInfo -> Relation -> Relation -> Relation
RelFun RelationInfo
ri (Bool -> Relation -> Relation
re (Bool -> RelationInfo -> Relation -> Bool
mk' (Bool -> Bool
not Bool
ok) RelationInfo
ri Relation
r1) Relation
r1) 
                                         (Bool -> Relation -> Relation
re (forall {p}. Bool -> RelationInfo -> p -> Bool
mk Bool
ok RelationInfo
ri Relation
r2) Relation
r2)
      -- second logical relation for functions. Only used for the language
      -- subset with Seq in the equational setting
      RelFunLab RelationInfo
ri Relation
r1 Relation
r2    -> RelationInfo -> Relation -> Relation -> Relation
RelFunLab RelationInfo
ri (Bool -> Relation -> Relation
re (Bool -> RelationInfo -> Relation -> Bool
mk' (Bool -> Bool
not Bool
ok) RelationInfo
ri Relation
r1) Relation
r1) 
                                            (Bool -> Relation -> Relation
re (forall {p}. Bool -> RelationInfo -> p -> Bool
mk Bool
ok RelationInfo
ri Relation
r2) Relation
r2)
      RelAbs RelationInfo
ri RelationVariable
rv (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
r -> RelationInfo
-> RelationVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Relation
RelAbs RelationInfo
ri RelationVariable
rv (TypeExpression, TypeExpression)
ts [Restriction]
res (Bool -> Relation -> Relation
re Bool
ok Relation
r)
      FunAbs RelationInfo
ri Either TermVariable TermVariable
fv (TypeExpression, TypeExpression)
ts [Restriction]
res Relation
r -> RelationInfo
-> Either TermVariable TermVariable
-> (TypeExpression, TypeExpression)
-> [Restriction]
-> Relation
-> Relation
FunAbs RelationInfo
ri Either TermVariable TermVariable
fv (TypeExpression, TypeExpression)
ts [Restriction]
res (Bool -> Relation -> Relation
re Bool
ok Relation
r)
      Relation
otherwise             -> Relation
rel

    mk' :: Bool -> RelationInfo -> Relation -> Bool
mk' Bool
ok RelationInfo
ri Relation
r = case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
                    TheoremType
EquationalTheorem   -> Bool
True
                    TheoremType
InequationalTheorem -> 
                      case Relation
r of
                        RelLift RelationInfo
_ TypeConstructor
ConList [Relation]
_ -> Bool
True
                        Relation
otherwise           -> Bool
ok


    mk :: Bool -> RelationInfo -> p -> Bool
mk Bool
ok RelationInfo
ri p
r = case LanguageSubset -> TheoremType
theoremType (RelationInfo -> LanguageSubset
relationLanguageSubset RelationInfo
ri) of
                   TheoremType
EquationalTheorem   -> Bool
True
                   TheoremType
InequationalTheorem -> Bool
ok


    -- Transforms a lifted constructor to a function, if possible.
    -- This function is applied in a bottom-up manner, therefore the
    -- arguments of the lifted constructor are already reduced.
    reduce :: Relation -> Relation
reduce Relation
rel = case Relation
rel of
      RelLift RelationInfo
ri TypeConstructor
con [Relation]
rs -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Relation
rel forall a. a -> a
id (RelationInfo -> TypeConstructor -> [Relation] -> Maybe Relation
toTerm RelationInfo
ri TypeConstructor
con [Relation]
rs)
      Relation
otherwise         -> Relation
rel

    -- Tries to transform a lifted relation. If not succesful, Nothing is
    -- returned.
    toTerm :: RelationInfo -> TypeConstructor -> [Relation] -> Maybe Relation
toTerm RelationInfo
ri TypeConstructor
con [Relation]
rs = do
      TermVariable
f <- TypeConstructor -> Maybe TermVariable
funSymbol TypeConstructor
con
      -- first check if all arguments are 'left' functions
      case forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Relation -> Maybe (Term, (TypeExpression, TypeExpression))
leftFun [Relation]
rs of
        Just [(Term, (TypeExpression, TypeExpression))]
fts -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelationInfo -> Either Term Term -> Relation
FunVar RelationInfo
ri forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ TermVariable -> [(Term, (TypeExpression, TypeExpression))] -> Term
term TermVariable
f [(Term, (TypeExpression, TypeExpression))]
fts
        Maybe [(Term, (TypeExpression, TypeExpression))]
Nothing  -> -- then check if all arguments are 'right' functions
                    case forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Relation -> Maybe (Term, (TypeExpression, TypeExpression))
rightFun [Relation]
rs of
                      Just [(Term, (TypeExpression, TypeExpression))]
fts -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelationInfo -> Either Term Term -> Relation
FunVar RelationInfo
ri forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ TermVariable -> [(Term, (TypeExpression, TypeExpression))] -> Term
term TermVariable
f [(Term, (TypeExpression, TypeExpression))]
fts
                      Maybe [(Term, (TypeExpression, TypeExpression))]
Nothing  -> forall a. Maybe a
Nothing

    -- Returns the function symbol associated with a lifted constructor.
    funSymbol :: TypeConstructor -> Maybe TermVariable
funSymbol TypeConstructor
con = case TypeConstructor
con of
      TypeConstructor
ConList             -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TermVariable
TVar forall a b. (a -> b) -> a -> b
$ String
"map"
      Con (Ident String
"Maybe") -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> TermVariable
TVar forall a b. (a -> b) -> a -> b
$ String
"fmap"
      TypeConstructor
otherwise           -> forall a. Maybe a
Nothing

    -- Checks if 'rel' is a 'left' function. If so, its term and type is
    -- returned, otherwise Nothing.
    leftFun :: Relation -> Maybe (Term, (TypeExpression, TypeExpression))
leftFun Relation
rel = case Relation
rel of
      FunVar RelationInfo
ri (Left Term
f) -> forall a. a -> Maybe a
Just (Term
f, ( RelationInfo -> TypeExpression
relationLeftType RelationInfo
ri
                                     , RelationInfo -> TypeExpression
relationRightType RelationInfo
ri))
      Relation
otherwise          -> forall a. Maybe a
Nothing

    -- Checks if 'rel' is a 'right' function. If so, its term and type is
    -- returned, otherwise Nothing.
    -- The returned type is flipped mirroring the fact that right functions are
    -- actually inverse functions.
    rightFun :: Relation -> Maybe (Term, (TypeExpression, TypeExpression))
rightFun Relation
rel = case Relation
rel of
      FunVar RelationInfo
ri (Right Term
f) -> forall a. a -> Maybe a
Just (Term
f, ( RelationInfo -> TypeExpression
relationRightType RelationInfo
ri
                                      , RelationInfo -> TypeExpression
relationLeftType RelationInfo
ri))
      Relation
otherwise           -> forall a. Maybe a
Nothing

    -- Creates a term by instantiating 'f' and applying the arguments of 'fts'.
    term :: TermVariable -> [(Term, (TypeExpression, TypeExpression))] -> Term
term TermVariable
f [(Term, (TypeExpression, TypeExpression))]
fts = 
        let ([Term]
fs, [(TypeExpression, TypeExpression)]
ts) = forall a b. [(a, b)] -> ([a], [b])
unzip [(Term, (TypeExpression, TypeExpression))]
fts
            termins :: Term -> (TypeExpression, TypeExpression) -> Term
termins Term
t (TypeExpression
t1, TypeExpression
t2) = Term -> TypeExpression -> Term
TermIns (Term -> TypeExpression -> Term
TermIns Term
t TypeExpression
t1) TypeExpression
t2
         in forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
TermApp (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> (TypeExpression, TypeExpression) -> Term
termins (TermVariable -> Term
TermVar TermVariable
f) [(TypeExpression, TypeExpression)]
ts) [Term]
fs