{-# OPTIONS -O0 #-}
{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/THFP2THF0.hs
Description :  Comorphism from THFP to THF0
Copyright   :  (c) J. von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  J. von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The comorphism from THFP to THF0.
-}

module Comorphisms.THFP2THF0 where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.ProofTree
import Common.Result
import Common.Id (Token (..))
import Common.AS_Annotation (Named)

import THF.Logic_THF
import THF.Cons
import THF.Sign
import qualified THF.Sublogic as SL
import THF.As
import THF.Utils (RewriteFuns (..), rewriteSenFun, rewriteTHF0, recreateSymbols,
                  toToken, typeToTopLevelType, thfTopLevelTypeToType, mkNames)

import qualified Data.Map as Map
import Control.Monad (liftM)

data THFP2THF0 = THFP2THF0 deriving Int -> THFP2THF0 -> ShowS
[THFP2THF0] -> ShowS
THFP2THF0 -> String
(Int -> THFP2THF0 -> ShowS)
-> (THFP2THF0 -> String)
-> ([THFP2THF0] -> ShowS)
-> Show THFP2THF0
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [THFP2THF0] -> ShowS
$cshowList :: [THFP2THF0] -> ShowS
show :: THFP2THF0 -> String
$cshow :: THFP2THF0 -> String
showsPrec :: Int -> THFP2THF0 -> ShowS
$cshowsPrec :: Int -> THFP2THF0 -> ShowS
Show

instance Language THFP2THF0

instance Comorphism THFP2THF0
                THF SL.THFSl
                BasicSpecTHF THFFormula () ()
                SignTHF MorphismTHF SymbolTHF () ProofTree
                THF SL.THFSl
                BasicSpecTHF THFFormula () ()
                SignTHF MorphismTHF SymbolTHF () ProofTree where
    sourceLogic :: THFP2THF0 -> THF
sourceLogic THFP2THF0 = THF
THF
    sourceSublogic :: THFP2THF0 -> THFSl
sourceSublogic THFP2THF0 = THFSl
SL.tHFP
    targetLogic :: THFP2THF0 -> THF
targetLogic THFP2THF0 = THF
THF
    mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl
mapSublogic THFP2THF0 _ = THFSl -> Maybe THFSl
forall a. a -> Maybe a
Just THFSl
SL.tHF0
    map_theory :: THFP2THF0
-> (SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
map_theory THFP2THF0 = (SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
trans_theory
    has_model_expansion :: THFP2THF0 -> Bool
has_model_expansion THFP2THF0 = Bool
True

trans_theory :: (SignTHF, [Named THFFormula])
                -> Result (SignTHF, [Named THFFormula])
trans_theory :: (SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
trans_theory (sig :: SignTHF
sig, sentences1 :: [Named THFFormula]
sentences1) = do
 let (cs_trans :: TransMap
cs_trans, sig1 :: SignTHF
sig1) = [(TransMap, SignTHF)] -> (TransMap, SignTHF)
forall a. [a] -> a
head ([(TransMap, SignTHF)] -> (TransMap, SignTHF))
-> ([(TransMap, SignTHF)] -> [(TransMap, SignTHF)])
-> [(TransMap, SignTHF)]
-> (TransMap, SignTHF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TransMap, SignTHF) -> Bool)
-> [(TransMap, SignTHF)] -> [(TransMap, SignTHF)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (tp_t :: TransMap
tp_t, Sign _ cs :: ConstMap
cs _) ->
                                  Bool -> Bool
not ((ConstInfo -> Bool) -> [ConstInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TransMap -> ConstInfo -> Bool
hasProdT TransMap
tp_t) ([ConstInfo] -> Bool) -> [ConstInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ ConstMap -> [ConstInfo]
forall k a. Map k a -> [a]
Map.elems ConstMap
cs)) ([(TransMap, SignTHF)] -> (TransMap, SignTHF))
-> [(TransMap, SignTHF)] -> (TransMap, SignTHF)
forall a b. (a -> b) -> a -> b
$
                 ((TransMap, SignTHF) -> (TransMap, SignTHF))
-> (TransMap, SignTHF) -> [(TransMap, SignTHF)]
forall a. (a -> a) -> a -> [a]
iterate (TransMap, SignTHF) -> (TransMap, SignTHF)
makeExplicitProducts (TransMap
forall k a. Map k a
Map.empty, SignTHF
sig)
     sig2 :: SignTHF
sig2 = SignTHF
sig1 {consts :: ConstMap
consts =
      (ConstInfo -> ConstInfo) -> ConstMap -> ConstMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ c :: ConstInfo
c -> ConstInfo
c {constType :: Type
constType = Type -> Type
curryConstType (ConstInfo -> Type
constType ConstInfo
c)}) (ConstMap -> ConstMap) -> ConstMap -> ConstMap
forall a b. (a -> b) -> a -> b
$
                         SignTHF -> ConstMap
consts SignTHF
sig1}
 [Named THFFormula]
sentences <- TransMap -> [Named THFFormula] -> Result [Named THFFormula]
rewriteSen TransMap
cs_trans [Named THFFormula]
sentences1
 (SignTHF, [Named THFFormula])
-> Result (SignTHF, [Named THFFormula])
forall (m :: * -> *) a. Monad m => a -> m a
return (SignTHF -> SignTHF
recreateSymbols SignTHF
sig2, [Named THFFormula]
sentences)

type TransMap = Map.Map Constant [Constant]

-- note: does not do anything on non-map-types
curryConstType :: Type -> Type
curryConstType :: Type -> Type
curryConstType (MapType t1 :: Type
t1 t2 :: Type
t2) = Type -> Type -> Type
prodToMapType Type
t1 Type
t2
curryConstType (ParType t :: Type
t) = Type -> Type
ParType (Type -> Type
curryConstType Type
t)
curryConstType t :: Type
t = Type
t

prodToMapType :: Type -> Type -> Type
prodToMapType :: Type -> Type -> Type
prodToMapType t1 :: Type
t1 t2 :: Type
t2 = case Type
t1 of
 MapType _ _ -> Type -> Type -> Type
MapType (Type -> Type
curryConstType Type
t1) Type
t2
 ProdType ts :: [Type]
ts -> let ts' :: [Type]
ts' = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
curryConstType [Type]
ts
                in (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
MapType) Type
t2 ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
ts')
 ParType t :: Type
t -> Type -> Type -> Type
prodToMapType Type
t Type
t2
 _ -> Type -> Type -> Type
MapType Type
t1 Type
t2

rewriteSen :: TransMap -> [Named THFFormula]
               -> Result [Named THFFormula]
rewriteSen :: TransMap -> [Named THFFormula] -> Result [Named THFFormula]
rewriteSen cs_trans :: TransMap
cs_trans = (Named THFFormula -> Result (Named THFFormula))
-> [Named THFFormula] -> Result [Named THFFormula]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (TransMap -> Named THFFormula -> Result (Named THFFormula)
rewriteSen' TransMap
cs_trans)

rewriteFns :: RewriteFuns TransMap
rewriteFns :: RewriteFuns TransMap
rewriteFns = RewriteFuns TransMap
forall a. RewriteFuns a
rewriteTHF0 {
 rewriteLogicFormula :: (RewriteFuns TransMap, TransMap)
-> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula = (RewriteFuns TransMap, TransMap)
-> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula',
 rewriteBinaryFormula :: (RewriteFuns TransMap, TransMap)
-> THFBinaryFormula -> Result THFBinaryFormula
rewriteBinaryFormula =
  \ _ bf :: THFBinaryFormula
bf -> String -> THFBinaryFormula -> Result THFBinaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "This function shouldn't be called!" THFBinaryFormula
bf,
 rewriteBinaryTuple :: (RewriteFuns TransMap, TransMap)
-> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple =
  \ _ bt :: THFBinaryTuple
bt -> String -> THFBinaryTuple -> Result THFBinaryTuple
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "This function shouldn't be called!" THFBinaryTuple
bt,
 rewriteVariableList :: (RewriteFuns TransMap, TransMap)
-> [THFVariable] -> Result [THFVariable]
rewriteVariableList = (RewriteFuns TransMap, TransMap)
-> [THFVariable] -> Result [THFVariable]
rewriteVariableList',
 rewriteConst :: (RewriteFuns TransMap, TransMap)
-> Constant -> Result THFUnitaryFormula
rewriteConst = (RewriteFuns TransMap, TransMap)
-> Constant -> Result THFUnitaryFormula
rewriteConst'
}

rewriteSen' :: TransMap -> Named THFFormula
               -> Result (Named THFFormula)
rewriteSen' :: TransMap -> Named THFFormula -> Result (Named THFFormula)
rewriteSen' cs_trans :: TransMap
cs_trans = (RewriteFuns TransMap, TransMap)
-> Named THFFormula -> Result (Named THFFormula)
forall a.
(RewriteFuns a, a) -> Named THFFormula -> Result (Named THFFormula)
rewriteSenFun (RewriteFuns TransMap
rewriteFns, TransMap
cs_trans)

rewriteLogicFormula' :: (RewriteFuns TransMap, TransMap)
                       -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula' :: (RewriteFuns TransMap, TransMap)
-> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula' d :: (RewriteFuns TransMap, TransMap)
d lf :: THFLogicFormula
lf = case THFLogicFormula
lf of
 TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> do
  Either THFBinaryFormula THFUnitaryFormula
bf' <- (RewriteFuns TransMap, TransMap)
-> THFBinaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryFormula' (RewriteFuns TransMap, TransMap)
d THFBinaryFormula
bf
  case Either THFBinaryFormula THFUnitaryFormula
bf' of
   Left bf'' :: THFBinaryFormula
bf'' -> THFLogicFormula -> Result THFLogicFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFLogicFormula -> Result THFLogicFormula)
-> THFLogicFormula -> Result THFLogicFormula
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula THFBinaryFormula
bf''
   Right uf :: THFUnitaryFormula
uf -> THFLogicFormula -> Result THFLogicFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFLogicFormula -> Result THFLogicFormula)
-> THFLogicFormula -> Result THFLogicFormula
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula THFUnitaryFormula
uf
 _ -> RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFLogicFormula
-> Result THFLogicFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFLogicFormula -> Result THFLogicFormula
rewriteLogicFormula RewriteFuns TransMap
forall a. RewriteFuns a
rewriteTHF0 (RewriteFuns TransMap, TransMap)
d THFLogicFormula
lf

rewriteBinaryFormula' :: (RewriteFuns TransMap, TransMap)
                        -> THFBinaryFormula
                        -> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryFormula' :: (RewriteFuns TransMap, TransMap)
-> THFBinaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryFormula' d :: (RewriteFuns TransMap, TransMap)
d@(fns :: RewriteFuns TransMap
fns, _) bf :: THFBinaryFormula
bf = case THFBinaryFormula
bf of
 TBF_THF_Binary_Pair uf1 :: THFUnitaryFormula
uf1 cn :: THFPairConnective
cn uf2 :: THFUnitaryFormula
uf2 -> do
  THFUnitaryFormula
uf1' <- RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns TransMap
fns (RewriteFuns TransMap, TransMap)
d THFUnitaryFormula
uf1
  THFUnitaryFormula
uf2' <- RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns TransMap
fns (RewriteFuns TransMap, TransMap)
d THFUnitaryFormula
uf2
  case (THFUnitaryFormula -> Maybe THFUnitaryFormula
toTuple THFUnitaryFormula
uf1', THFPairConnective
cn, THFUnitaryFormula -> Maybe THFUnitaryFormula
toTuple THFUnitaryFormula
uf2') of
      (Just (TUF_THF_Tuple t1 :: THFTuple
t1), Infix_Equality,
       Just (TUF_THF_Tuple t2 :: THFTuple
t2)) -> if THFTuple -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length THFTuple
t1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== THFTuple -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length THFTuple
t2
        then Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either THFBinaryFormula THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple (THFBinaryTuple -> THFBinaryFormula)
-> THFBinaryTuple -> THFBinaryFormula
forall a b. (a -> b) -> a -> b
$ [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_And_Formula ([THFUnitaryFormula] -> THFBinaryTuple)
-> [THFUnitaryFormula] -> THFBinaryTuple
forall a b. (a -> b) -> a -> b
$
              ((THFLogicFormula, THFLogicFormula) -> THFUnitaryFormula)
-> [(THFLogicFormula, THFLogicFormula)] -> [THFUnitaryFormula]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t1' :: THFLogicFormula
t1', t2' :: THFLogicFormula
t2') ->
               THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par (THFLogicFormula -> THFUnitaryFormula)
-> THFLogicFormula -> THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula (THFBinaryFormula -> THFLogicFormula)
-> THFBinaryFormula -> THFLogicFormula
forall a b. (a -> b) -> a -> b
$
                THFUnitaryFormula
-> THFPairConnective -> THFUnitaryFormula -> THFBinaryFormula
TBF_THF_Binary_Pair (THFLogicFormula -> THFUnitaryFormula
logicFormula2UnitaryFormula THFLogicFormula
t1')
                 THFPairConnective
cn (THFLogicFormula -> THFUnitaryFormula
logicFormula2UnitaryFormula THFLogicFormula
t2')) (THFTuple -> THFTuple -> [(THFLogicFormula, THFLogicFormula)]
forall a b. [a] -> [b] -> [(a, b)]
zip THFTuple
t1 THFTuple
t2)
        else String
-> THFBinaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THFP2THF0.rewriteBinaryFormula: Equality on tuples " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      "of different size!") THFBinaryFormula
bf
      _ -> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either THFBinaryFormula THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula
-> THFPairConnective -> THFUnitaryFormula -> THFBinaryFormula
TBF_THF_Binary_Pair THFUnitaryFormula
uf1' THFPairConnective
cn THFUnitaryFormula
uf2'
 TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt -> (RewriteFuns TransMap, TransMap)
-> THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryTuple' (RewriteFuns TransMap, TransMap)
d THFBinaryTuple
bt
 _ -> (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> Result THFBinaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left (Result THFBinaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Result THFBinaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFBinaryFormula
-> Result THFBinaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFBinaryFormula
-> Result THFBinaryFormula
rewriteBinaryFormula RewriteFuns TransMap
forall a. RewriteFuns a
rewriteTHF0 (RewriteFuns TransMap, TransMap)
d THFBinaryFormula
bf

toTuple :: THFUnitaryFormula -> Maybe THFUnitaryFormula
toTuple :: THFUnitaryFormula -> Maybe THFUnitaryFormula
toTuple u :: THFUnitaryFormula
u@(TUF_THF_Tuple _) = THFUnitaryFormula -> Maybe THFUnitaryFormula
forall a. a -> Maybe a
Just THFUnitaryFormula
u
toTuple (TUF_THF_Logic_Formula_Par
  (TLF_THF_Unitary_Formula u :: THFUnitaryFormula
u)) = THFUnitaryFormula -> Maybe THFUnitaryFormula
forall a. a -> Maybe a
Just THFUnitaryFormula
u
toTuple _ = Maybe THFUnitaryFormula
forall a. Maybe a
Nothing

logicFormula2UnitaryFormula :: THFLogicFormula -> THFUnitaryFormula
logicFormula2UnitaryFormula :: THFLogicFormula -> THFUnitaryFormula
logicFormula2UnitaryFormula l :: THFLogicFormula
l = case THFLogicFormula
l of
 TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> THFUnitaryFormula
uf
 _ -> THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par THFLogicFormula
l

rewriteBinaryTuple' :: (RewriteFuns TransMap, TransMap)
                        -> THFBinaryTuple
                        -> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryTuple' :: (RewriteFuns TransMap, TransMap)
-> THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryTuple' d :: (RewriteFuns TransMap, TransMap)
d@(fns :: RewriteFuns TransMap
fns, _) bt :: THFBinaryTuple
bt = case THFBinaryTuple
bt of
 TBT_THF_Apply_Formula ufs :: [THFUnitaryFormula]
ufs -> do
  [THFUnitaryFormula]
ufs' <- (THFUnitaryFormula -> Result THFUnitaryFormula)
-> [THFUnitaryFormula] -> Result [THFUnitaryFormula]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns TransMap
fns (RewriteFuns TransMap, TransMap)
d) [THFUnitaryFormula]
ufs
  case [THFUnitaryFormula]
ufs' of
      [] -> String
-> THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THFP2THF0.rewriteBinaryTuple: Illegal Application!" THFBinaryTuple
bt
      _ : [] -> String
-> THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THFP2THF0.rewriteBinaryTuple: Illegal Application!" THFBinaryTuple
bt
      fn :: THFUnitaryFormula
fn : args :: [THFUnitaryFormula]
args -> case THFUnitaryFormula -> THFUnitaryFormula
removeParensUnitaryFormula THFUnitaryFormula
fn of
       (TUF_THF_Atom (T0A_Constant c :: Constant
c)) ->
         case Token -> String
forall a. Show a => a -> String
show (Token -> String) -> (Constant -> Token) -> Constant -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Token
toToken (Constant -> String) -> Constant -> String
forall a b. (a -> b) -> a -> b
$ Constant
c of
           'p' : 'r' : '_' : i :: String
i ->
              case [THFUnitaryFormula]
args of
               tuple :: THFUnitaryFormula
tuple : [] ->
                let i' :: Int
i' = String -> Int
forall a. Read a => String -> a
read String
i :: Int
                in THFUnitaryFormula
-> Int -> Result (Either THFBinaryFormula THFUnitaryFormula)
unpack_tuple THFUnitaryFormula
tuple Int
i'
               _ -> String
-> [THFUnitaryFormula]
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THFP2THF0.rewriteBinaryTuple: Invalid " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                            "argument for projection: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [THFUnitaryFormula] -> String
forall a. Show a => a -> String
show [THFUnitaryFormula]
args) [THFUnitaryFormula]
ufs
           _ -> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either THFBinaryFormula THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple (THFBinaryTuple -> THFBinaryFormula)
-> THFBinaryTuple -> THFBinaryFormula
forall a b. (a -> b) -> a -> b
$ [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula ([THFUnitaryFormula] -> THFBinaryTuple)
-> [THFUnitaryFormula] -> THFBinaryTuple
forall a b. (a -> b) -> a -> b
$
                 THFUnitaryFormula
fn THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula] -> [THFUnitaryFormula]
flattenTuples [THFUnitaryFormula]
args
       TUF_THF_Tuple lfs :: THFTuple
lfs ->
         (THFUnitaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> Result THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM THFUnitaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. b -> Either a b
Right (Result THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Result THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ (THFLogicFormula -> Result THFLogicFormula)
-> THFTuple -> Result THFTuple
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (\ l :: THFLogicFormula
l ->
                         do Either THFBinaryFormula THFUnitaryFormula
app' <- (RewriteFuns TransMap, TransMap)
-> THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryTuple' (RewriteFuns TransMap, TransMap)
d (THFBinaryTuple
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> ([THFUnitaryFormula] -> THFBinaryTuple)
-> [THFUnitaryFormula]
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                    [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula ([THFUnitaryFormula]
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> [THFUnitaryFormula]
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$
                                     THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par THFLogicFormula
l THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula]
args
                            THFLogicFormula -> Result THFLogicFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFLogicFormula -> Result THFLogicFormula)
-> THFLogicFormula -> Result THFLogicFormula
forall a b. (a -> b) -> a -> b
$ case Either THFBinaryFormula THFUnitaryFormula
app' of
                              Left bf :: THFBinaryFormula
bf -> THFBinaryFormula -> THFLogicFormula
TLF_THF_Binary_Formula THFBinaryFormula
bf
                              Right uf :: THFUnitaryFormula
uf -> THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula THFUnitaryFormula
uf) THFTuple
lfs
                       Result THFTuple
-> (THFTuple -> Result THFUnitaryFormula)
-> Result THFUnitaryFormula
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
forall a.
RewriteFuns a
-> (RewriteFuns a, a)
-> THFUnitaryFormula
-> Result THFUnitaryFormula
rewriteUnitaryFormula RewriteFuns TransMap
fns (RewriteFuns TransMap, TransMap)
d (THFUnitaryFormula -> Result THFUnitaryFormula)
-> (THFTuple -> THFUnitaryFormula)
-> THFTuple
-> Result THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFTuple -> THFUnitaryFormula
TUF_THF_Tuple
       _ -> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either THFBinaryFormula THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple (THFBinaryTuple -> THFBinaryFormula)
-> THFBinaryTuple -> THFBinaryFormula
forall a b. (a -> b) -> a -> b
$ [THFUnitaryFormula] -> THFBinaryTuple
TBT_THF_Apply_Formula ([THFUnitaryFormula] -> THFBinaryTuple)
-> [THFUnitaryFormula] -> THFBinaryTuple
forall a b. (a -> b) -> a -> b
$
             THFUnitaryFormula
fn THFUnitaryFormula -> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall a. a -> [a] -> [a]
: [THFUnitaryFormula] -> [THFUnitaryFormula]
flattenTuples [THFUnitaryFormula]
args
 _ -> (THFBinaryTuple -> Either THFBinaryFormula THFUnitaryFormula)
-> Result THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left (THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula)
-> (THFBinaryTuple -> THFBinaryFormula)
-> THFBinaryTuple
-> Either THFBinaryFormula THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFBinaryTuple -> THFBinaryFormula
TBF_THF_Binary_Tuple) (Result THFBinaryTuple
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Result THFBinaryTuple
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ RewriteFuns TransMap
-> (RewriteFuns TransMap, TransMap)
-> THFBinaryTuple
-> Result THFBinaryTuple
forall a.
RewriteFuns a
-> (RewriteFuns a, a) -> THFBinaryTuple -> Result THFBinaryTuple
rewriteBinaryTuple RewriteFuns TransMap
forall a. RewriteFuns a
rewriteTHF0 (RewriteFuns TransMap, TransMap)
d THFBinaryTuple
bt

flattenTuples :: [THFUnitaryFormula] -> [THFUnitaryFormula]
flattenTuples :: [THFUnitaryFormula] -> [THFUnitaryFormula]
flattenTuples = (THFUnitaryFormula -> [THFUnitaryFormula])
-> [THFUnitaryFormula] -> [THFUnitaryFormula]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap THFUnitaryFormula -> [THFUnitaryFormula]
flattenTuple

flattenTuple :: THFUnitaryFormula -> [THFUnitaryFormula]
flattenTuple :: THFUnitaryFormula -> [THFUnitaryFormula]
flattenTuple u :: THFUnitaryFormula
u = case THFUnitaryFormula -> THFUnitaryFormula
removeParensUnitaryFormula THFUnitaryFormula
u of
 TUF_THF_Tuple lfs :: THFTuple
lfs ->
  (THFLogicFormula -> [THFUnitaryFormula])
-> THFTuple -> [THFUnitaryFormula]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (THFUnitaryFormula -> [THFUnitaryFormula]
flattenTuple (THFUnitaryFormula -> [THFUnitaryFormula])
-> (THFLogicFormula -> THFUnitaryFormula)
-> THFLogicFormula
-> [THFUnitaryFormula]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFLogicFormula -> THFUnitaryFormula
TUF_THF_Logic_Formula_Par) THFTuple
lfs
 _ -> [THFUnitaryFormula
u]

unpack_tuple :: THFUnitaryFormula -> Int
                -> Result (Either THFBinaryFormula THFUnitaryFormula)
unpack_tuple :: THFUnitaryFormula
-> Int -> Result (Either THFBinaryFormula THFUnitaryFormula)
unpack_tuple uf :: THFUnitaryFormula
uf i :: Int
i = case THFUnitaryFormula -> THFUnitaryFormula
removeParensUnitaryFormula THFUnitaryFormula
uf of
 TUF_THF_Tuple lfs :: THFTuple
lfs -> if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> THFTuple -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length THFTuple
lfs
  then String
-> THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "THFP2THF0.unpack_tuple: Tuple has too few elements!" THFUnitaryFormula
uf
  else case THFTuple
lfs THFTuple -> Int -> THFLogicFormula
forall a. [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) of
        TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either THFBinaryFormula THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ THFBinaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. a -> Either a b
Left THFBinaryFormula
bf
        TLF_THF_Unitary_Formula uf' :: THFUnitaryFormula
uf' -> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either THFBinaryFormula THFUnitaryFormula
 -> Result (Either THFBinaryFormula THFUnitaryFormula))
-> Either THFBinaryFormula THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (a -> b) -> a -> b
$ THFUnitaryFormula -> Either THFBinaryFormula THFUnitaryFormula
forall a b. b -> Either a b
Right THFUnitaryFormula
uf'
        lf :: THFLogicFormula
lf -> String
-> THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THFP2THF0.unpack_tuple: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFLogicFormula -> String
forall a. Show a => a -> String
show THFLogicFormula
lf
                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is not in THF0!") THFUnitaryFormula
uf
 _ -> String
-> THFUnitaryFormula
-> Result (Either THFBinaryFormula THFUnitaryFormula)
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THFP2THF0.unpack_tuple: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Show a => a -> String
show THFUnitaryFormula
uf String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is not a tuple!") THFUnitaryFormula
uf

removeParensUnitaryFormula :: THFUnitaryFormula -> THFUnitaryFormula
removeParensUnitaryFormula :: THFUnitaryFormula -> THFUnitaryFormula
removeParensUnitaryFormula (TUF_THF_Logic_Formula_Par
 (TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf)) = THFUnitaryFormula
uf
removeParensUnitaryFormula uf :: THFUnitaryFormula
uf = THFUnitaryFormula
uf

rewriteVariableList' :: (RewriteFuns TransMap, TransMap)
                       -> [THFVariable] -> Result [THFVariable]
rewriteVariableList' :: (RewriteFuns TransMap, TransMap)
-> [THFVariable] -> Result [THFVariable]
rewriteVariableList' (_, cs_trans :: TransMap
cs_trans) vs :: [THFVariable]
vs = do
 [[THFVariable]]
vs' <- (THFVariable -> Result [THFVariable])
-> [THFVariable] -> Result [[THFVariable]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (\ v :: THFVariable
v -> case THFVariable
v of
             TV_THF_Typed_Variable t :: Token
t tp :: THFTopLevelType
tp ->
              case THFTopLevelType -> Maybe Type
thfTopLevelTypeToType THFTopLevelType
tp of
               Just tp' :: Type
tp' -> let cs :: [(Constant, Type)]
cs = Constant -> Type -> [(Constant, Type)]
constMakeExplicitProduct
                                     (Token -> Constant
A_Lower_Word Token
t) Type
tp'
                           in ((Constant, Type) -> Result THFVariable)
-> [(Constant, Type)] -> Result [THFVariable]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (c :: Constant
c, tp'' :: Type
tp'') -> (THFTopLevelType -> THFVariable)
-> Result THFTopLevelType -> Result THFVariable
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
                                 (Token -> THFTopLevelType -> THFVariable
TV_THF_Typed_Variable (Constant -> Token
toToken Constant
c))
                                 (Type -> Result THFTopLevelType
typeToTopLevelType (Type -> Type
curryConstType Type
tp''))) [(Constant, Type)]
cs
               Nothing ->
                String -> THFTopLevelType -> Result [THFVariable]
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError ("THFP2THF0.rewriteVariableList: Couldn't " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                         "type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFTopLevelType -> String
forall a. Show a => a -> String
show THFTopLevelType
tp) THFTopLevelType
tp
             TV_Variable t :: Token
t -> case TransMap -> Token -> [Token]
transToken TransMap
cs_trans Token
t of
                               [_] -> [THFVariable] -> Result [THFVariable]
forall (m :: * -> *) a. Monad m => a -> m a
return [THFVariable
v]
                               t' :: [Token]
t' -> [THFVariable] -> Result [THFVariable]
forall (m :: * -> *) a. Monad m => a -> m a
return ([THFVariable] -> Result [THFVariable])
-> [THFVariable] -> Result [THFVariable]
forall a b. (a -> b) -> a -> b
$ (Token -> THFVariable) -> [Token] -> [THFVariable]
forall a b. (a -> b) -> [a] -> [b]
map Token -> THFVariable
TV_Variable [Token]
t') [THFVariable]
vs
 [THFVariable] -> Result [THFVariable]
forall (m :: * -> *) a. Monad m => a -> m a
return ([THFVariable] -> Result [THFVariable])
-> [THFVariable] -> Result [THFVariable]
forall a b. (a -> b) -> a -> b
$ [[THFVariable]] -> [THFVariable]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[THFVariable]]
vs'

transToken :: TransMap -> Token -> [Token]
transToken :: TransMap -> Token -> [Token]
transToken m :: TransMap
m t :: Token
t = case TransMap -> [(Constant, [Constant])]
forall k a. Map k a -> [(k, a)]
Map.toList (TransMap -> [(Constant, [Constant])])
-> TransMap -> [(Constant, [Constant])]
forall a b. (a -> b) -> a -> b
$
  (Constant -> [Constant] -> Bool) -> TransMap -> TransMap
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ c :: Constant
c _ -> Constant -> Token
toToken Constant
c Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t) TransMap
m of
                   (_, cs :: [Constant]
cs) : _ -> (Constant -> [Token]) -> [Constant] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (TransMap -> Token -> [Token]
transToken TransMap
m (Token -> [Token]) -> (Constant -> Token) -> Constant -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> Token
toToken) [Constant]
cs
                   [] -> [Token
t]

rewriteConst' :: (RewriteFuns TransMap, TransMap)
                  -> Constant -> Result THFUnitaryFormula
rewriteConst' :: (RewriteFuns TransMap, TransMap)
-> Constant -> Result THFUnitaryFormula
rewriteConst' (_, m :: TransMap
m) c :: Constant
c = case TransMap -> Constant -> THFTuple
transConst' TransMap
m Constant
c of
 [] -> THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFAtom -> THFUnitaryFormula
TUF_THF_Atom (Constant -> THFAtom
T0A_Constant Constant
c)
 lfs :: THFTuple
lfs -> THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> THFUnitaryFormula -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ THFTuple -> THFUnitaryFormula
TUF_THF_Tuple THFTuple
lfs

transConst' :: TransMap -> Constant -> [THFLogicFormula]
transConst' :: TransMap -> Constant -> THFTuple
transConst' m :: TransMap
m c :: Constant
c = case TransMap -> [(Constant, [Constant])]
forall k a. Map k a -> [(k, a)]
Map.toList (TransMap -> [(Constant, [Constant])])
-> TransMap -> [(Constant, [Constant])]
forall a b. (a -> b) -> a -> b
$
  (Constant -> [Constant] -> Bool) -> TransMap -> TransMap
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ c' :: Constant
c' _ -> Constant
c Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
== Constant
c') TransMap
m of
   (_, cs :: [Constant]
cs) : _ -> (Constant -> THFLogicFormula) -> [Constant] -> THFTuple
forall a b. (a -> b) -> [a] -> [b]
map (\ c' :: Constant
c' -> case TransMap -> Constant -> THFTuple
transConst' TransMap
m Constant
c' of
                           [] -> THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (THFUnitaryFormula -> THFLogicFormula)
-> (Constant -> THFUnitaryFormula) -> Constant -> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                 THFAtom -> THFUnitaryFormula
TUF_THF_Atom (THFAtom -> THFUnitaryFormula)
-> (Constant -> THFAtom) -> Constant -> THFUnitaryFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constant -> THFAtom
T0A_Constant (Constant -> THFLogicFormula) -> Constant -> THFLogicFormula
forall a b. (a -> b) -> a -> b
$ Constant
c'
                           lfs :: THFTuple
lfs -> THFUnitaryFormula -> THFLogicFormula
TLF_THF_Unitary_Formula (THFUnitaryFormula -> THFLogicFormula)
-> (THFTuple -> THFUnitaryFormula) -> THFTuple -> THFLogicFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                                  THFTuple -> THFUnitaryFormula
TUF_THF_Tuple (THFTuple -> THFLogicFormula) -> THFTuple -> THFLogicFormula
forall a b. (a -> b) -> a -> b
$ THFTuple
lfs) [Constant]
cs
   [] -> []

constMakeExplicitProduct :: Constant -> Type -> [(Constant, Type)]
constMakeExplicitProduct :: Constant -> Type -> [(Constant, Type)]
constMakeExplicitProduct c :: Constant
c t :: Type
t =
 let (_, Sign _ cs :: ConstMap
cs _) = [(TransMap, SignTHF)] -> (TransMap, SignTHF)
forall a. [a] -> a
head ([(TransMap, SignTHF)] -> (TransMap, SignTHF))
-> ([(TransMap, SignTHF)] -> [(TransMap, SignTHF)])
-> [(TransMap, SignTHF)]
-> (TransMap, SignTHF)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TransMap, SignTHF) -> Bool)
-> [(TransMap, SignTHF)] -> [(TransMap, SignTHF)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (tp_t :: TransMap
tp_t, Sign _ cs' :: ConstMap
cs' _) ->
                          Bool -> Bool
not ((ConstInfo -> Bool) -> [ConstInfo] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TransMap -> ConstInfo -> Bool
hasProdT TransMap
tp_t) ([ConstInfo] -> Bool) -> [ConstInfo] -> Bool
forall a b. (a -> b) -> a -> b
$ ConstMap -> [ConstInfo]
forall k a. Map k a -> [a]
Map.elems ConstMap
cs')) ([(TransMap, SignTHF)] -> (TransMap, SignTHF))
-> [(TransMap, SignTHF)] -> (TransMap, SignTHF)
forall a b. (a -> b) -> a -> b
$
      ((TransMap, SignTHF) -> (TransMap, SignTHF))
-> (TransMap, SignTHF) -> [(TransMap, SignTHF)]
forall a. (a -> a) -> a -> [a]
iterate (TransMap, SignTHF) -> (TransMap, SignTHF)
makeExplicitProducts
      (TransMap
forall k a. Map k a
Map.empty, TypeMap -> ConstMap -> SymbolMap -> SignTHF
Sign TypeMap
forall k a. Map k a
Map.empty ([(Constant, ConstInfo)] -> ConstMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Constant
c,
        ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo {constId :: Constant
constId = Constant
c, constName :: Name
constName = Constant -> Name
N_Atomic_Word Constant
c,
                   constType :: Type
constType = Type
t, constAnno :: Annotations
constAnno = Annotations
Null})]) SymbolMap
forall k a. Map k a
Map.empty)
 in (ConstInfo -> (Constant, Type))
-> [ConstInfo] -> [(Constant, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: ConstInfo
i -> (ConstInfo -> Constant
constId ConstInfo
i, ConstInfo -> Type
constType ConstInfo
i)) ([ConstInfo] -> [(Constant, Type)])
-> [ConstInfo] -> [(Constant, Type)]
forall a b. (a -> b) -> a -> b
$ ConstMap -> [ConstInfo]
forall k a. Map k a -> [a]
Map.elems ConstMap
cs

-- Note: Type definitions are non-recursive
makeExplicitProducts :: (TransMap, SignTHF) ->
 (TransMap, SignTHF)
makeExplicitProducts :: (TransMap, SignTHF) -> (TransMap, SignTHF)
makeExplicitProducts (cs_trans1 :: TransMap
cs_trans1, sig :: SignTHF
sig) =
 let (cs_trans :: TransMap
cs_trans, cs :: ConstMap
cs) = TransMap -> ConstMap -> (TransMap, ConstMap)
mkExplicitProductsT TransMap
cs_trans1 (SignTHF -> ConstMap
consts SignTHF
sig)
 in (TransMap
cs_trans, SignTHF
sig {consts :: ConstMap
consts = ConstMap
cs})

mkExplicitProductsT :: TransMap -> Map.Map Constant ConstInfo
                       -> (TransMap, Map.Map Constant ConstInfo)
mkExplicitProductsT :: TransMap -> ConstMap -> (TransMap, ConstMap)
mkExplicitProductsT cs_trans1 :: TransMap
cs_trans1 cs1 :: ConstMap
cs1 = (ConstInfo -> (TransMap, ConstMap) -> (TransMap, ConstMap))
-> (TransMap, ConstMap) -> ConstMap -> (TransMap, ConstMap)
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr
 (\ c :: ConstInfo
c (trans :: TransMap
trans, cs :: ConstMap
cs) -> TransMap
-> ConstMap -> Constant -> Name -> Type -> (TransMap, ConstMap)
prodTToTuple TransMap
trans ConstMap
cs (ConstInfo -> Constant
constId ConstInfo
c) (ConstInfo -> Name
constName ConstInfo
c)
                     (ConstInfo -> Type
constType ConstInfo
c)) (TransMap
cs_trans1, ConstMap
cs1) ConstMap
cs1

prodTToTuple :: TransMap -> Map.Map Constant ConstInfo -> Constant
                -> Name -> Type -> (TransMap, Map.Map Constant ConstInfo)
prodTToTuple :: TransMap
-> ConstMap -> Constant -> Name -> Type -> (TransMap, ConstMap)
prodTToTuple trans :: TransMap
trans cs :: ConstMap
cs c :: Constant
c n :: Name
n t :: Type
t = case Type
t of
 MapType t1 :: Type
t1 t2 :: Type
t2 ->
  let (_, cs' :: ConstMap
cs') = TransMap
-> ConstMap -> Constant -> Name -> Type -> (TransMap, ConstMap)
prodTToTuple TransMap
forall k a. Map k a
Map.empty ConstMap
forall k a. Map k a
Map.empty Constant
c Name
n Type
t2
      cs'' :: ConstMap
cs'' = Constant -> ConstMap -> ConstMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Constant
c ConstMap
cs
      tuple :: [ConstInfo]
tuple = ConstMap -> [ConstInfo]
forall k a. Map k a -> [a]
Map.elems ConstMap
cs'
      names :: [(Constant, Name)]
names = Constant -> Name -> Int -> [(Constant, Name)]
mkNames Constant
c Name
n (Int -> [(Constant, Name)]) -> Int -> [(Constant, Name)]
forall a b. (a -> b) -> a -> b
$ [ConstInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ConstInfo]
tuple
  in if [ConstInfo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ConstInfo]
tuple then (TransMap
trans, ConstMap
cs) else
     (Constant -> [Constant] -> TransMap -> TransMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c (((Constant, Name) -> Constant) -> [(Constant, Name)] -> [Constant]
forall a b. (a -> b) -> [a] -> [b]
map (Constant, Name) -> Constant
forall a b. (a, b) -> a
fst [(Constant, Name)]
names) TransMap
trans,
      (((Constant, Name), ConstInfo) -> ConstMap -> ConstMap)
-> ConstMap -> [((Constant, Name), ConstInfo)] -> ConstMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ((n1 :: Constant
n1, n2 :: Name
n2), ci :: ConstInfo
ci) cs''' :: ConstMap
cs''' -> Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
n1
                ConstInfo
ci {constName :: Name
constName = Name
n2,
                    constId :: Constant
constId = Constant
n1,
                    constType :: Type
constType = Type -> Type -> Type
MapType Type
t1 (ConstInfo -> Type
constType ConstInfo
ci)} ConstMap
cs''')
            ConstMap
cs'' ([(Constant, Name)]
-> [ConstInfo] -> [((Constant, Name), ConstInfo)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Constant, Name)]
names [ConstInfo]
tuple))
 ProdType ts :: [Type]
ts -> let cs' :: ConstMap
cs' = Constant -> ConstMap -> ConstMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Constant
c ConstMap
cs
                    names :: [(Constant, Name)]
names = Constant -> Name -> Int -> [(Constant, Name)]
mkNames Constant
c Name
n (Int -> [(Constant, Name)]) -> Int -> [(Constant, Name)]
forall a b. (a -> b) -> a -> b
$ [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
                in (Constant -> [Constant] -> TransMap -> TransMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
c (((Constant, Name) -> Constant) -> [(Constant, Name)] -> [Constant]
forall a b. (a -> b) -> [a] -> [b]
map (Constant, Name) -> Constant
forall a b. (a, b) -> a
fst [(Constant, Name)]
names) TransMap
trans,
                    (((Constant, Name), Type) -> ConstMap -> ConstMap)
-> ConstMap -> [((Constant, Name), Type)] -> ConstMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ((n1 :: Constant
n1, n2 :: Name
n2), tp :: Type
tp) cs'' :: ConstMap
cs'' -> Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Constant
n1
                              ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo {constType :: Type
constType = Type
tp,
                                        constName :: Name
constName = Name
n2,
                                        constId :: Constant
constId = Constant
n1,
                                        constAnno :: Annotations
constAnno = Annotations
Null} ConstMap
cs'')
                          ConstMap
cs' ([(Constant, Name)] -> [Type] -> [((Constant, Name), Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Constant, Name)]
names [Type]
ts))
 ParType tp :: Type
tp -> TransMap
-> ConstMap -> Constant -> Name -> Type -> (TransMap, ConstMap)
prodTToTuple TransMap
trans ConstMap
cs Constant
c Name
n Type
tp
 _ -> (TransMap
trans, ConstMap
cs)

hasProdT :: TransMap -> ConstInfo -> Bool
hasProdT :: TransMap -> ConstInfo -> Bool
hasProdT t :: TransMap
t = TransMap -> Type -> Bool
isProdT TransMap
t (Type -> Bool) -> (ConstInfo -> Type) -> ConstInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstInfo -> Type
constType

isProdT :: TransMap -> Type -> Bool
isProdT :: TransMap -> Type -> Bool
isProdT _ TType = Bool
False
isProdT _ OType = Bool
False
isProdT _ IType = Bool
False
isProdT m :: TransMap
m (MapType _ t2 :: Type
t2) = TransMap -> Type -> Bool
isProdT TransMap
m Type
t2
isProdT _ (ProdType _) = Bool
True
isProdT m :: TransMap
m (CType c :: Constant
c) = case Constant -> TransMap -> Maybe [Constant]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Constant
c TransMap
m of
                            Just _ -> Bool
True
                            Nothing -> Bool
False
isProdT _ (SType _) = Bool
False
isProdT _ (VType _) = Bool
False
isProdT m :: TransMap
m (ParType t :: Type
t) = TransMap -> Type -> Bool
isProdT TransMap
m Type
t