{- |
Module      :  ./THF/Poly.hs
Description :  Helper functions for coding out polymorphism
Copyright   :  (c) J. von Schroeder, DFKI Bremen 2012
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  non-portable

-}
module THF.Poly
where

import THF.Cons
import THF.Sign
import THF.Utils
import THF.As
import THF.PrintTHF ()
import THF.Print ()

import Common.Result
import Common.Id
import Common.AS_Annotation
import Common.DocUtils

import Control.Monad.State
import qualified Data.Map (Map, lookup, insert, empty,
                           mapAccumWithKey, foldrWithKey,
                           mapWithKey, toList)
import qualified Data.List (mapAccumL, elemIndex)
import qualified Data.Set (fromList, toList)
import Data.Maybe (catMaybes)

sh :: Pretty a => a -> String
sh :: a -> String
sh = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (a -> Doc) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty

data Constraint = NormalC (String, Range, Type)
                | WeakC (String, Range, Type) deriving Int -> Constraint -> ShowS
[Constraint] -> ShowS
Constraint -> String
(Int -> Constraint -> ShowS)
-> (Constraint -> String)
-> ([Constraint] -> ShowS)
-> Show Constraint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> Constraint -> ShowS
Show

instance GetRange Constraint where
    getRange :: Constraint -> Range
getRange (NormalC (_, r :: Range
r, _)) = Range
r
    getRange (WeakC (_, r :: Range
r, _)) = Range
r

instance GetRange Type where
    getRange :: Type -> Range
getRange _ = Range
nullRange

occursType :: Token -> Type -> Bool
occursType :: Token -> Type -> Bool
occursType t :: Token
t tp :: Type
tp = case Type
tp of
 MapType tp1 :: Type
tp1 tp2 :: Type
tp2 ->
  Token -> Type -> Bool
occursType Token
t Type
tp1 Bool -> Bool -> Bool
|| Token -> Type -> Bool
occursType Token
t Type
tp2
 ProdType tps :: [Type]
tps ->
  (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Token -> Type -> Bool
occursType Token
t) [Type]
tps
 VType t1 :: Token
t1 -> Token
t Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t1
 ParType tp2 :: Type
tp2 -> Token -> Type -> Bool
occursType Token
t Type
tp2
 _ -> Bool
False

constraintToType :: Constraint -> (Bool, (String, Range, Type))
constraintToType :: Constraint -> (Bool, (String, Range, Type))
constraintToType (WeakC d :: (String, Range, Type)
d) = (Bool
True, (String, Range, Type)
d)
constraintToType (NormalC d :: (String, Range, Type)
d) = (Bool
False, (String, Range, Type)
d)

toConstraint :: Bool -> (String, Range, Type) -> Constraint
toConstraint :: Bool -> (String, Range, Type) -> Constraint
toConstraint weak :: Bool
weak = if Bool
weak then (String, Range, Type) -> Constraint
WeakC
                    else (String, Range, Type) -> Constraint
NormalC

unifyType :: Type -> Constraint -> Result [(Token, Type)]
unifyType :: Type -> Constraint -> Result [(Token, Type)]
unifyType tp1 :: Type
tp1 tp2_ :: Constraint
tp2_ =
 let (weak :: Bool
weak, (s :: String
s, r :: Range
r, tp2 :: Type
tp2)) = Constraint -> (Bool, (String, Range, Type))
constraintToType Constraint
tp2_
     c :: Type -> Constraint
c t :: Type
t = Bool -> (String, Range, Type) -> Constraint
toConstraint Bool
weak (String
s, Range
r, Type
t)
 in case (Type
tp1, Type
tp2) of
     (ParType tp1' :: Type
tp1', _) ->
      Type -> Constraint -> Result [(Token, Type)]
unifyType Type
tp1' (Type -> Constraint
c Type
tp2)
     (_, ParType tp2' :: Type
tp2') ->
      Type -> Constraint -> Result [(Token, Type)]
unifyType Type
tp1 (Type -> Constraint
c Type
tp2')
     (VType t1 :: Token
t1, VType t2 :: Token
t2) -> [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Token, Type)] -> Result [(Token, Type)])
-> [(Token, Type)] -> Result [(Token, Type)]
forall a b. (a -> b) -> a -> b
$
      if Token
t1 Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t2 then [] else [(Token
t1, Type
tp2)]
     (VType t1 :: Token
t1, _) -> if Token -> Type -> Bool
occursType Token
t1 Type
tp2
      then String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Occurs check failed! - "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
      else [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Token
t1, Type
tp2)]
     (_, VType t2 :: Token
t2) -> if Token -> Type -> Bool
occursType Token
t2 Type
tp1
      then String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Occurs check failed! - "
       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
      else [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Token
t2, Type
tp1)]
     (MapType tp1_1 :: Type
tp1_1 tp1_2 :: Type
tp1_2,
      MapType tp2_1 :: Type
tp2_1 tp2_2 :: Type
tp2_2) -> do
      [(Token, Type)]
u1 <- Type -> Constraint -> Result [(Token, Type)]
unifyType Type
tp1_1 (Type -> Constraint
c Type
tp2_1)
      [(Token, Type)]
u2 <- Type -> Constraint -> Result [(Token, Type)]
unifyType Type
tp1_2 (Type -> Constraint
c Type
tp2_2)
      [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Token, Type)] -> Result [(Token, Type)])
-> [(Token, Type)] -> Result [(Token, Type)]
forall a b. (a -> b) -> a -> b
$ [(Token, Type)]
u1 [(Token, Type)] -> [(Token, Type)] -> [(Token, Type)]
forall a. [a] -> [a] -> [a]
++ [(Token, Type)]
u2
     (MapType _ _, _) ->
      String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Different type constructors! " String -> ShowS
forall a. [a] -> [a] -> [a]
++
       " - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (_, MapType _ _) ->
      String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Different type constructors! " String -> ShowS
forall a. [a] -> [a] -> [a]
++
       " - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (ProdType tps1 :: [Type]
tps1, ProdType tps2 :: [Type]
tps2) ->
      if [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tps2 Bool -> Bool -> Bool
||
         Bool
weak then
       ([[(Token, Type)]] -> [(Token, Type)])
-> Result [[(Token, Type)]] -> Result [(Token, Type)]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [[(Token, Type)]] -> [(Token, Type)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Result [[(Token, Type)]] -> Result [(Token, Type)])
-> Result [[(Token, Type)]] -> Result [(Token, Type)]
forall a b. (a -> b) -> a -> b
$
        ((Type, Type) -> Result [(Token, Type)])
-> [(Type, Type)] -> Result [[(Token, Type)]]
forall a b. (a -> Result b) -> [a] -> Result [b]
mapR (\ (tp1' :: Type
tp1', tp2' :: Type
tp2') -> Type -> Constraint -> Result [(Token, Type)]
unifyType Type
tp1' (Type -> Constraint
c Type
tp2'))
         ([Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
tps1 [Type]
tps2)
      else String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Products of different size! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (ProdType _, _) ->
      String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Different type constructors! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (CType c1 :: Constant
c1, CType c2 :: Constant
c2) -> if Constant
c1 Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
== Constant
c2
      then [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify different kinds!" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (CType _, _) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Unification not possible! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (_, CType _) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Unification not possible! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (_, ProdType _) ->
      String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Different type constructors! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (TType, TType) -> [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
     (OType, OType) -> [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
     (IType, IType) -> [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
     (TType, _) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify TType with "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tp2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (_, TType) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify TType with "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tp1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (OType, _) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify OType with "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tp2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (_, OType) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify OType with "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tp1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (IType, _) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify IType with "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tp2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     (_, IType) -> String -> Range -> Result [(Token, Type)]
forall a. String -> Range -> Result a
fatal_error ("Cannot unify IType with "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
tp1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) Range
r
     _ -> [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []

applyType :: [(Token, Type)] -> Token -> Maybe Type
applyType :: [(Token, Type)] -> Token -> Maybe Type
applyType us :: [(Token, Type)]
us t :: Token
t = case [(Token, Type)]
us of
 (t' :: Token
t', tp :: Type
tp) : _ | Token
t' Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
t -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
tp
 _ : us' :: [(Token, Type)]
us' -> [(Token, Type)] -> Token -> Maybe Type
applyType [(Token, Type)]
us' Token
t
 _ -> Maybe Type
forall a. Maybe a
Nothing

apply :: [(Token, Type)] -> Type -> Type
apply :: [(Token, Type)] -> Type -> Type
apply us :: [(Token, Type)]
us t :: Type
t = case Type
t of
 ParType t' :: Type
t' -> Type -> Type
ParType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [(Token, Type)] -> Type -> Type
apply [(Token, Type)]
us Type
t'
 MapType t1 :: Type
t1 t2 :: Type
t2 -> Type -> Type -> Type
MapType ([(Token, Type)] -> Type -> Type
apply [(Token, Type)]
us Type
t1)
  ([(Token, Type)] -> Type -> Type
apply [(Token, Type)]
us Type
t2)
 ProdType tps :: [Type]
tps -> [Type] -> Type
ProdType ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ([(Token, Type)] -> Type -> Type
apply [(Token, Type)]
us) [Type]
tps
 VType tok :: Token
tok -> case [(Token, Type)] -> Token -> Maybe Type
applyType [(Token, Type)]
us Token
tok of
  Just t' :: Type
t' -> [(Token, Type)] -> Type -> Type
apply [(Token, Type)]
us Type
t'
  Nothing -> Type
t
 _ -> Type
t

unify' :: [(Type, Constraint)] -> Result [(Token, Type)]
unify' :: [(Type, Constraint)] -> Result [(Token, Type)]
unify' ts :: [(Type, Constraint)]
ts = case [(Type, Constraint)]
ts of
 [] -> [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
 (t1 :: Type
t1, t2 :: Constraint
t2) : ts' :: [(Type, Constraint)]
ts' -> do
  [(Token, Type)]
r1 <- [(Type, Constraint)] -> Result [(Token, Type)]
unify' [(Type, Constraint)]
ts'
  let t1' :: Type
t1' = [(Token, Type)] -> Type -> Type
apply [(Token, Type)]
r1 Type
t1
  let (weak :: Bool
weak, (msg :: String
msg, rg :: Range
rg, t2'' :: Type
t2'')) = Constraint -> (Bool, (String, Range, Type))
constraintToType Constraint
t2
  let t2' :: Type
t2' = [(Token, Type)] -> Type -> Type
apply [(Token, Type)]
r1 Type
t2''
  [(Token, Type)]
r2 <- Type -> Constraint -> Result [(Token, Type)]
unifyType Type
t1' (Bool -> (String, Range, Type) -> Constraint
toConstraint Bool
weak (String
msg, Range
rg, Type
t2'))
  [(Token, Type)] -> Result [(Token, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Token, Type)]
r1 [(Token, Type)] -> [(Token, Type)] -> [(Token, Type)]
forall a. [a] -> [a] -> [a]
++ [(Token, Type)]
r2)

tmpV :: Token
tmpV :: Token
tmpV = String -> Token
mkSimpleId "tmpV"

type Constraints = UniqueT Result (Type, [(Type, Constraint)])

not_supported :: (Show a, GetRange a) => a -> Constraints
not_supported :: a -> Constraints
not_supported f :: a
f = Result (Type, [(Type, Constraint)]) -> Constraints
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result (Type, [(Type, Constraint)]) -> Constraints)
-> Result (Type, [(Type, Constraint)]) -> Constraints
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result (Type, [(Type, Constraint)])
forall a. String -> Range -> Result a
fatal_error
                   ("Formula " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ " not supported!")
                   (a -> Range
forall a. GetRange a => a -> Range
getRange a
f)

getTypeC :: ConstMap -> THFFormula -> Constraints
getTypeC :: ConstMap -> THFFormula -> Constraints
getTypeC cm :: ConstMap
cm f :: THFFormula
f = case THFFormula
f of
 TF_THF_Logic_Formula lf :: THFLogicFormula
lf -> ConstMap -> THFLogicFormula -> Constraints
getTypeCLF ConstMap
cm THFLogicFormula
lf
 _ -> THFFormula -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFFormula
f

getTypeCLF :: ConstMap -> THFLogicFormula -> Constraints
getTypeCLF :: ConstMap -> THFLogicFormula -> Constraints
getTypeCLF cm :: ConstMap
cm lf :: THFLogicFormula
lf = case THFLogicFormula
lf of
 TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> ConstMap -> THFBinaryFormula -> Constraints
getTypeCBF ConstMap
cm THFBinaryFormula
bf
 TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm THFUnitaryFormula
uf
 _ -> THFLogicFormula -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFLogicFormula
lf

getTypeCBF :: ConstMap -> THFBinaryFormula -> Constraints
getTypeCBF :: ConstMap -> THFBinaryFormula -> Constraints
getTypeCBF cm :: ConstMap
cm bf :: THFBinaryFormula
bf = case THFBinaryFormula
bf of
 TBF_THF_Binary_Pair uf1 :: THFUnitaryFormula
uf1 c :: THFPairConnective
c uf2 :: THFUnitaryFormula
uf2 -> if (case THFPairConnective
c of
  Infix_Equality -> Bool
True
  Infix_Inequality -> Bool
True
  _ -> Bool
False) then do
   (t1 :: Type
t1, cs1 :: [(Type, Constraint)]
cs1) <- ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm THFUnitaryFormula
uf1
   (t2 :: Type
t2, cs2 :: [(Type, Constraint)]
cs2) <- ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm THFUnitaryFormula
uf2
   let errMsg :: String
errMsg = "(In-)Equality requires (" String -> ShowS
forall a. [a] -> [a] -> [a]
++
        THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") : (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
sh Type
t1
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") and (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") : ("
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
sh Type
t2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") to have the same type"
   (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
OType,
    [(Type, Constraint)]
cs1 [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type, Constraint)]
cs2 [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type
t1, (String, Range, Type) -> Constraint
NormalC (String
errMsg, THFBinaryFormula -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFBinaryFormula
bf, Type
t2))])
  else do
   (t1 :: Type
t1, cs1 :: [(Type, Constraint)]
cs1) <- ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm THFUnitaryFormula
uf1
   (t2 :: Type
t2, cs2 :: [(Type, Constraint)]
cs2) <- ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm THFUnitaryFormula
uf2
   let errMsg1 :: String
errMsg1 = "Infix operator " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFPairConnective -> String
forall a. Pretty a => a -> String
sh THFPairConnective
c
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ " requires (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") : ("
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
sh Type
t1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")  to have type OType"
   let errMsg2 :: String
errMsg2 = "Infix operator " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFPairConnective -> String
forall a. Pretty a => a -> String
sh THFPairConnective
c
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ " requires (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") : ("
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
sh Type
t2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")  to have type OType"
   (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
OType,
    [(Type, Constraint)]
cs1 [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type, Constraint)]
cs2 [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type
t1, (String, Range, Type) -> Constraint
NormalC (String
errMsg1, THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFUnitaryFormula
uf1, Type
OType)),
                   (Type
t2, (String, Range, Type) -> Constraint
NormalC (String
errMsg2, THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFUnitaryFormula
uf2, Type
OType))])
 TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt ->
  let ufs :: [THFUnitaryFormula]
ufs = case THFBinaryTuple
bt of
       TBT_THF_Or_Formula ufs' :: [THFUnitaryFormula]
ufs' -> [THFUnitaryFormula]
ufs'
       TBT_THF_And_Formula ufs' :: [THFUnitaryFormula]
ufs' -> [THFUnitaryFormula]
ufs'
       TBT_THF_Apply_Formula ufs' :: [THFUnitaryFormula]
ufs' -> [THFUnitaryFormula]
ufs'
  in case THFBinaryTuple
bt of
      TBT_THF_Apply_Formula _ -> do
       [(Type, [(Type, Constraint)])]
ufs' <- (THFUnitaryFormula -> Constraints)
-> [THFUnitaryFormula]
-> UniqueT Result [(Type, [(Type, Constraint)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm) [THFUnitaryFormula]
ufs
       case [(Type, [(Type, Constraint)])]
ufs' of
        [] -> Result (Type, [(Type, Constraint)]) -> Constraints
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result (Type, [(Type, Constraint)]) -> Constraints)
-> Result (Type, [(Type, Constraint)]) -> Constraints
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result (Type, [(Type, Constraint)])
forall a. String -> Range -> Result a
fatal_error ("Invalid Application: "
                                  String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFBinaryTuple -> String
forall a. Show a => a -> String
show THFBinaryTuple
bt) (THFBinaryTuple -> Range
forall a. GetRange a => a -> Range
getRange THFBinaryTuple
bt)
        _ : [] -> Result (Type, [(Type, Constraint)]) -> Constraints
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result (Type, [(Type, Constraint)]) -> Constraints)
-> Result (Type, [(Type, Constraint)]) -> Constraints
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result (Type, [(Type, Constraint)])
forall a. String -> Range -> Result a
fatal_error ("Invalid Application: "
                                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFBinaryTuple -> String
forall a. Show a => a -> String
show THFBinaryTuple
bt) (THFBinaryTuple -> Range
forall a. GetRange a => a -> Range
getRange THFBinaryTuple
bt)
        u :: (Type, [(Type, Constraint)])
u : ufs'' :: [(Type, [(Type, Constraint)])]
ufs'' -> do
         let (t1 :: Type
t1, cs1 :: [(Type, Constraint)]
cs1) = (Type, [(Type, Constraint)])
u
             tps :: [Type]
tps = ((Type, [(Type, Constraint)]) -> Type)
-> [(Type, [(Type, Constraint)])] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, [(Type, Constraint)]) -> Type
forall a b. (a, b) -> a
fst [(Type, [(Type, Constraint)])]
ufs''
             cs2 :: [[(Type, Constraint)]]
cs2 = ((Type, [(Type, Constraint)]) -> [(Type, Constraint)])
-> [(Type, [(Type, Constraint)])] -> [[(Type, Constraint)]]
forall a b. (a -> b) -> [a] -> [b]
map (Type, [(Type, Constraint)]) -> [(Type, Constraint)]
forall a b. (a, b) -> b
snd [(Type, [(Type, Constraint)])]
ufs''
         {- try to do a best-effort beta-reduction
             * either t1 is a "function type" we
               can recognize
             * or we simply assign a new type variable
               and hope that further constraints
               will determine the type variable -}
         Type
t <- Int -> Type -> UniqueT Result Type
applyResult ([(Type, [(Type, Constraint)])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Type, [(Type, Constraint)])]
ufs'') Type
t1
         let errMsg :: String
errMsg = "Application is not well typed"
         (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, [(Type, Constraint)]
cs1 [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [[(Type, Constraint)]] -> [(Type, Constraint)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Constraint)]]
cs2
          [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type
t1, (String, Range, Type) -> Constraint
WeakC (String
errMsg, THFBinaryTuple -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFBinaryTuple
bt, [Type] -> Type
genFn ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ [Type]
tps [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
t]))])
      _ -> do
       [(Type, [(Type, Constraint)])]
ufs' <- (THFUnitaryFormula -> Constraints)
-> [THFUnitaryFormula]
-> UniqueT Result [(Type, [(Type, Constraint)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm) [THFUnitaryFormula]
ufs
       case [(Type, [(Type, Constraint)])]
ufs' of
        [] -> Result (Type, [(Type, Constraint)]) -> Constraints
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result (Type, [(Type, Constraint)]) -> Constraints)
-> Result (Type, [(Type, Constraint)]) -> Constraints
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result (Type, [(Type, Constraint)])
forall a. String -> Range -> Result a
fatal_error ("Empty boolean connective: "
                           String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFBinaryTuple -> String
forall a. Show a => a -> String
show THFBinaryTuple
bt) (THFBinaryTuple -> Range
forall a. GetRange a => a -> Range
getRange THFBinaryTuple
bt)
        (t :: Type
t, cs :: [(Type, Constraint)]
cs) : [] -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, [(Type, Constraint)]
cs [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type
t, (String, Range, Type) -> Constraint
NormalC (
         "Boolean connective requires all " String -> ShowS
forall a. [a] -> [a] -> [a]
++
         "arguments to be of type OType", [THFUnitaryFormula] -> Range
forall a. GetRange a => a -> Range
getRangeSpan [THFUnitaryFormula]
ufs, Type
OType))])
        _ -> do
         let (ts :: [Type]
ts, cs :: [[(Type, Constraint)]]
cs) = [(Type, [(Type, Constraint)])] -> ([Type], [[(Type, Constraint)]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, [(Type, Constraint)])]
ufs'
         let errMsg :: String
errMsg = "Boolean connective requires all " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                      "arguments to be of type OType"
         (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
OType, [[(Type, Constraint)]] -> [(Type, Constraint)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Constraint)]]
cs [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ (Type -> (Type, Constraint)) -> [Type] -> [(Type, Constraint)]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: Type
t ->
          (Type
t, (String, Range, Type) -> Constraint
NormalC (String
errMsg, THFBinaryTuple -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFBinaryTuple
bt, Type
OType))) [Type]
ts)
 _ -> THFBinaryFormula -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFBinaryFormula
bf

applyResult :: Int -> Type -> UniqueT Result Type
applyResult :: Int -> Type -> UniqueT Result Type
applyResult 0 t :: Type
t = Type -> UniqueT Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
applyResult i :: Int
i t :: Type
t = case Type
t of
 MapType _ t' :: Type
t' -> Int -> Type -> UniqueT Result Type
applyResult (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Type
t'
 _ -> do
  Token
v <- Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
  Type -> UniqueT Result Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Type
VType Token
v)

getTypeCUF :: ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF :: ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF cm :: ConstMap
cm uf :: THFUnitaryFormula
uf = case THFUnitaryFormula
uf of
 TUF_THF_Quantified_Formula qf :: THFQuantifiedFormula
qf -> case THFQuantifiedFormula
qf of
  TQF_THF_Quantified_Formula _ vs :: THFVariableList
vs uf' :: THFUnitaryFormula
uf' -> THFVariableList -> THFUnitaryFormula -> Constraints
forall (t :: * -> *).
Foldable t =>
t THFVariable -> THFUnitaryFormula -> Constraints
getTypeCQF THFVariableList
vs THFUnitaryFormula
uf'
  T0QF_THF_Quantified_Var _ vs :: THFVariableList
vs uf' :: THFUnitaryFormula
uf' -> THFVariableList -> THFUnitaryFormula -> Constraints
forall (t :: * -> *).
Foldable t =>
t THFVariable -> THFUnitaryFormula -> Constraints
getTypeCQF THFVariableList
vs THFUnitaryFormula
uf'
  _ -> THFUnitaryFormula -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFUnitaryFormula
uf
  where getTypeCQF :: t THFVariable -> THFUnitaryFormula -> Constraints
getTypeCQF vs :: t THFVariable
vs uf' :: THFUnitaryFormula
uf' = do
         ConstMap
cm' <- (ConstMap -> THFVariable -> UniqueT Result ConstMap)
-> ConstMap -> t THFVariable -> UniqueT Result ConstMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ cm' :: ConstMap
cm' 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' -> ConstMap -> UniqueT Result ConstMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstMap -> UniqueT Result ConstMap)
-> ConstMap -> UniqueT Result ConstMap
forall a b. (a -> b) -> a -> b
$ Token -> Type -> ConstMap -> ConstMap
ins Token
t Type
tp' ConstMap
cm'
             Nothing ->
              Result ConstMap -> UniqueT Result ConstMap
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result ConstMap -> UniqueT Result ConstMap)
-> Result ConstMap -> UniqueT Result ConstMap
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result ConstMap
forall a. String -> Range -> Result a
fatal_error ("Failed to analyze type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFTopLevelType -> String
forall a. Show a => a -> String
show THFTopLevelType
tp)
                                 (THFTopLevelType -> Range
forall a. GetRange a => a -> Range
getRange THFTopLevelType
tp)
           TV_Variable t :: Token
t -> do
            Token
v' <- Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
            ConstMap -> UniqueT Result ConstMap
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstMap -> UniqueT Result ConstMap)
-> ConstMap -> UniqueT Result ConstMap
forall a b. (a -> b) -> a -> b
$ Token -> Type -> ConstMap -> ConstMap
ins Token
t (Token -> Type
VType Token
v') ConstMap
cm') ConstMap
cm t THFVariable
vs
         (t :: Type
t, cs :: [(Type, Constraint)]
cs) <- ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm' THFUnitaryFormula
uf'
         let errMsg :: String
errMsg = "Quantified Formula (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf' String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") : ("
                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Pretty a => a -> String
sh Type
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") is expected to be of type OType"
         (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t, [(Type, Constraint)]
cs [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type
t, (String, Range, Type) -> Constraint
NormalC (String
errMsg, THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFUnitaryFormula
uf', Type
OType))])
        c :: Token -> Constant
c = Token -> Constant
A_Single_Quoted
        ins :: Token -> Type -> ConstMap -> ConstMap
ins t :: Token
t tp :: Type
tp = Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Data.Map.insert (Token -> Constant
c Token
t)
          ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo {
            constId :: Constant
constId = Token -> Constant
c Token
t,
            constName :: Name
constName = Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
c Token
t,
            constType :: Type
constType = Type
tp,
            constAnno :: Annotations
constAnno = Annotations
Null}
 TUF_THF_Unary_Formula q :: THFUnaryConnective
q lf :: THFLogicFormula
lf -> do
  (lf' :: Type
lf', cs :: [(Type, Constraint)]
cs) <- ConstMap -> THFLogicFormula -> Constraints
getTypeCLF ConstMap
cm THFLogicFormula
lf
  let errMsg :: String
errMsg = "Unary Formula (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") : ("
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Pretty a => a -> String
sh THFUnitaryFormula
uf String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") is expected to be of type OType"
      lf'' :: Type
lf'' = case THFUnaryConnective
q of
              Negation -> Type
lf'
              _ -> case Type
lf' of
                     MapType _ t :: Type
t -> Type
t
                     _ ->  String -> Type
forall a. HasCallStack => String -> a
error "TUF_THF_Unary_Formula"
  (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
lf'', [(Type, Constraint)]
cs [(Type, Constraint)]
-> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. [a] -> [a] -> [a]
++ [(Type
lf'', (String, Range, Type) -> Constraint
NormalC (String
errMsg, THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRangeSpan THFUnitaryFormula
uf, Type
OType))])
 TUF_THF_Atom a :: THFAtom
a -> case THFAtom
a of
  TA_THF_Conn_Term c :: THFConnTerm
c -> case THFConnTerm
c of
   TCT_THF_Unary_Connective cn :: THFUnaryConnective
cn -> case THFUnaryConnective
cn of
    Negation -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
MapType Type
OType Type
OType,[])
    _ -> do
                    Token
v <- Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
                    (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
MapType (Type -> Type -> Type
MapType (Token -> Type
VType Token
v) Type
OType) Type
OType,[])
   TCT_Assoc_Connective _ -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
MapType Type
OType (Type -> Type -> Type
MapType Type
OType Type
OType),[])
   TCT_THF_Pair_Connective _ -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
MapType Type
OType (Type -> Type -> Type
MapType Type
OType Type
OType),[])
   _ -> THFAtom -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFAtom
a
  T0A_Constant c :: Constant
c -> case Constant -> ConstMap -> Maybe ConstInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup Constant
c ConstMap
cm of
   Just ti :: ConstInfo
ti -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstInfo -> Type
constType ConstInfo
ti, [])
   Nothing -> case Token -> String
forall a. Show a => a -> String
show (Token -> String) -> Token -> String
forall a b. (a -> b) -> a -> b
$ Constant -> Token
toToken Constant
c of
     'p' : 'r' : '_' : i' :: String
i' -> do
      let i :: Int
i = String -> Int
forall a. Read a => String -> a
read String
i' :: Int
      [Type]
vs <- Int -> UniqueT Result Type -> UniqueT Result [Type]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
i (UniqueT Result Type -> UniqueT Result [Type])
-> UniqueT Result Type -> UniqueT Result [Type]
forall a b. (a -> b) -> a -> b
$ (Token -> Type) -> UniqueT Result Token -> UniqueT Result Type
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Token -> Type
VType (UniqueT Result Token -> UniqueT Result Type)
-> UniqueT Result Token -> UniqueT Result Type
forall a b. (a -> b) -> a -> b
$ Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
      (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Type -> Type
MapType ([Type] -> Type
ProdType [Type]
vs) (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Type
forall a. [a] -> a
last [Type]
vs, [])
     _ -> do
      Token
v <- Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
      (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Type
VType Token
v, [])
  -- fixme - add types for internal constants
  T0A_Defined_Constant c :: Token
c -> if (Token -> String
forall a. Show a => a -> String
show Token
c) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "true" Bool -> Bool -> Bool
|| (Token -> String
forall a. Show a => a -> String
show Token
c) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "false"
   then (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
OType, [])
   else THFAtom -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFAtom
a
  T0A_System_Constant _ -> THFAtom -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFAtom
a
  T0A_Variable v :: Token
v -> case Constant -> ConstMap -> Maybe ConstInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup (Token -> Constant
A_Single_Quoted Token
v) ConstMap
cm of
   Just ti :: ConstInfo
ti -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstInfo -> Type
constType ConstInfo
ti, [])
   Nothing -> do
    Token
v' <- Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
    (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Type
VType Token
v', [])
  _ -> THFAtom -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFAtom
a
 TUF_THF_Tuple lfs :: THFTuple
lfs -> do
  [(Type, [(Type, Constraint)])]
lfs' <- (THFLogicFormula -> Constraints)
-> THFTuple -> UniqueT Result [(Type, [(Type, Constraint)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ConstMap -> THFLogicFormula -> Constraints
getTypeCLF ConstMap
cm) THFTuple
lfs
  let (tps :: [Type]
tps, cs :: [[(Type, Constraint)]]
cs) = [(Type, [(Type, Constraint)])] -> ([Type], [[(Type, Constraint)]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Type, [(Type, Constraint)])]
lfs'
  (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type
ProdType [Type]
tps, [[(Type, Constraint)]] -> [(Type, Constraint)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Type, Constraint)]]
cs)
 TUF_THF_Logic_Formula_Par lf :: THFLogicFormula
lf -> ConstMap -> THFLogicFormula -> Constraints
getTypeCLF ConstMap
cm THFLogicFormula
lf
 T0UF_THF_Abstraction vs :: THFVariableList
vs uf' :: THFUnitaryFormula
uf' -> do
  (vst :: [Type]
vst, cm' :: ConstMap
cm') <- (([Type], ConstMap)
 -> THFVariable -> UniqueT Result ([Type], ConstMap))
-> ([Type], ConstMap)
-> THFVariableList
-> UniqueT Result ([Type], ConstMap)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ (l :: [Type]
l, cm' :: ConstMap
cm') 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' -> ([Type], ConstMap) -> UniqueT Result ([Type], ConstMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tp' Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
l, Token -> Type -> ConstMap -> ConstMap
ins Token
t Type
tp' ConstMap
cm')
             Nothing ->
              Result ([Type], ConstMap) -> UniqueT Result ([Type], ConstMap)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result ([Type], ConstMap) -> UniqueT Result ([Type], ConstMap))
-> Result ([Type], ConstMap) -> UniqueT Result ([Type], ConstMap)
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result ([Type], ConstMap)
forall a. String -> Range -> Result a
fatal_error ("Failed to analyze type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFTopLevelType -> String
forall a. Show a => a -> String
show THFTopLevelType
tp)
                                 (THFTopLevelType -> Range
forall a. GetRange a => a -> Range
getRange THFTopLevelType
tp)
           TV_Variable t :: Token
t -> do
            Token
v' <- Token -> UniqueT Result Token
forall (m :: * -> *). Monad m => Token -> UniqueT m Token
numberedTok Token
tmpV
            ([Type], ConstMap) -> UniqueT Result ([Type], ConstMap)
forall (m :: * -> *) a. Monad m => a -> m a
return (Token -> Type
VType Token
v' Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
l, Token -> Type -> ConstMap -> ConstMap
ins Token
t (Token -> Type
VType Token
v') ConstMap
cm')) ([], ConstMap
cm) (THFVariableList -> THFVariableList
forall a. [a] -> [a]
reverse THFVariableList
vs)
  (uf'' :: Type
uf'', cs :: [(Type, Constraint)]
cs) <- ConstMap -> THFUnitaryFormula -> Constraints
getTypeCUF ConstMap
cm' THFUnitaryFormula
uf'
  case [Type]
vst of
   [] -> Result (Type, [(Type, Constraint)]) -> Constraints
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Result (Type, [(Type, Constraint)]) -> Constraints)
-> Result (Type, [(Type, Constraint)]) -> Constraints
forall a b. (a -> b) -> a -> b
$ String -> Range -> Result (Type, [(Type, Constraint)])
forall a. String -> Range -> Result a
fatal_error ("Invalid Abstraction: "
                             String -> ShowS
forall a. [a] -> [a] -> [a]
++ THFUnitaryFormula -> String
forall a. Show a => a -> String
show THFUnitaryFormula
uf) (THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRange THFUnitaryFormula
uf)
   _ -> (Type, [(Type, Constraint)]) -> Constraints
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Type
genFn ([Type]
vst [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type
uf'']), [(Type, Constraint)]
cs)
  where c :: Token -> Constant
c = Token -> Constant
A_Single_Quoted
        ins :: Token -> Type -> ConstMap -> ConstMap
ins t :: Token
t tp :: Type
tp = Constant -> ConstInfo -> ConstMap -> ConstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Data.Map.insert (Token -> Constant
c Token
t)
                 ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo {
                   constId :: Constant
constId = Token -> Constant
c Token
t,
                   constName :: Name
constName = Constant -> Name
N_Atomic_Word (Constant -> Name) -> Constant -> Name
forall a b. (a -> b) -> a -> b
$ Token -> Constant
c Token
t,
                   constType :: Type
constType = Type
tp,
                   constAnno :: Annotations
constAnno = Annotations
Null }
 _ -> THFUnitaryFormula -> Constraints
forall a. (Show a, GetRange a) => a -> Constraints
not_supported THFUnitaryFormula
uf

genFn :: [Type] -> Type
genFn :: [Type] -> Type
genFn (tp :: Type
tp : []) = Type
tp
genFn (tp :: Type
tp : tps :: [Type]
tps) = Type -> Type -> Type
MapType Type
tp ([Type] -> Type
genFn [Type]
tps)
genFn _ = String -> Type
forall a. HasCallStack => String -> a
error "This shouldn't happen!"

insertAndIdx :: (Ord a, Eq b) => Data.Map.Map a [b] -> a -> b
                 -> (Data.Map.Map a [b], Maybe Int)
insertAndIdx :: Map a [b] -> a -> b -> (Map a [b], Maybe Int)
insertAndIdx m :: Map a [b]
m k :: a
k v :: b
v = case a -> Map a [b] -> Maybe [b]
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup a
k Map a [b]
m of
 Just l :: [b]
l -> case b -> [b] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
Data.List.elemIndex b
v [b]
l of
  Just i :: Int
i -> (Map a [b]
m, Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
  Nothing -> (a -> [b] -> Map a [b] -> Map a [b]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Data.Map.insert a
k ([b]
l [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [b
v]) Map a [b]
m,
   Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [b] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
l)
 Nothing -> (a -> [b] -> Map a [b] -> Map a [b]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Data.Map.insert a
k [b
v] Map a [b]
m, Int -> Maybe Int
forall a. a -> Maybe a
Just 0)

intToStr :: Int -> String
intToStr :: Int -> String
intToStr 0 = ""
intToStr i :: Int
i = '_' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i

flattenMap :: Data.Map.Map Constant [a] -> Data.Map.Map Constant a
flattenMap :: Map Constant [a] -> Map Constant a
flattenMap = (Constant -> [a] -> Map Constant a -> Map Constant a)
-> Map Constant a -> Map Constant [a] -> Map Constant a
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Data.Map.foldrWithKey
 (\ k :: Constant
k v :: [a]
v new_m :: Map Constant a
new_m ->
  let ks :: [Constant]
ks = Unique [Constant] -> [Constant]
forall a. Unique a -> a
evalUnique (Unique [Constant] -> [Constant])
-> Unique [Constant] -> [Constant]
forall a b. (a -> b) -> a -> b
$ Int -> Unique Constant -> Unique [Constant]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
v) (Unique Constant -> Unique [Constant])
-> Unique Constant -> Unique [Constant]
forall a b. (a -> b) -> a -> b
$ do
       Integer
f <- Unique Integer
forall (m :: * -> *). MonadUnique m => m Integer
fresh
       let s :: String
s = Int -> String
intToStr (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
f Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)
       Constant -> Unique Constant
forall (m :: * -> *) a. Monad m => a -> m a
return (Constant -> Unique Constant) -> Constant -> Unique Constant
forall a b. (a -> b) -> a -> b
$ String -> Constant -> Constant
addSuffix String
s Constant
k
  in (Map Constant a -> (Constant, a) -> Map Constant a)
-> Map Constant a -> [(Constant, a)] -> Map Constant a
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ new_m' :: Map Constant a
new_m' (k' :: Constant
k', v' :: a
v') -> Constant -> a -> Map Constant a -> Map Constant a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Data.Map.insert Constant
k' a
v' Map Constant a
new_m')
      Map Constant a
new_m ([Constant] -> [a] -> [(Constant, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Constant]
ks [a]
v)) Map Constant a
forall k a. Map k a
Data.Map.empty

type RewriteArg = Data.Map.Map Constant (Maybe Int)

rewriteVariableList_ :: (RewriteFuns RewriteArg, RewriteArg) ->
                        [THFVariable] -> Result [THFVariable]
rewriteVariableList_ :: (RewriteFuns RewriteArg, RewriteArg)
-> THFVariableList -> Result THFVariableList
rewriteVariableList_ (_, cm :: RewriteArg
cm) vs :: THFVariableList
vs = THFVariableList -> Result THFVariableList
forall (m :: * -> *) a. Monad m => a -> m a
return (THFVariableList -> Result THFVariableList)
-> THFVariableList -> Result THFVariableList
forall a b. (a -> b) -> a -> b
$
 (THFVariable -> THFVariable) -> THFVariableList -> THFVariableList
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: THFVariable
v -> let t :: Token
t = case THFVariable
v of
                     TV_THF_Typed_Variable t' _ -> Token
t'
                     TV_Variable t' -> Token
t'
            in case Constant -> RewriteArg -> Maybe (Maybe Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup (Token -> Constant
A_Single_Quoted Token
t) RewriteArg
cm of
                Just (Just i :: Int
i) -> Token -> THFVariable
TV_Variable (Token -> THFVariable) -> Token -> THFVariable
forall a b. (a -> b) -> a -> b
$
                 Token
t { tokStr :: String
tokStr = Token -> String
tokStr Token
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
intToStr Int
i }
                _ -> THFVariable
v) THFVariableList
vs

rewriteConst_ :: (RewriteFuns RewriteArg, RewriteArg) ->
                 Constant -> Result THFUnitaryFormula
rewriteConst_ :: (RewriteFuns RewriteArg, RewriteArg)
-> Constant -> Result THFUnitaryFormula
rewriteConst_ (_, cm :: RewriteArg
cm) c :: Constant
c = THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> (Constant -> THFUnitaryFormula)
-> Constant
-> Result THFUnitaryFormula
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 -> Result THFUnitaryFormula)
-> Constant -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$
 case Constant -> RewriteArg -> Maybe (Maybe Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup Constant
c RewriteArg
cm of
  Just (Just i :: Int
i) -> String -> Constant -> Constant
addSuffix (Int -> String
intToStr Int
i) Constant
c
  _ -> Constant
c

rewriteConst4needsConst :: (RewriteFuns Constant, Constant) ->
                           Constant -> Result THFUnitaryFormula
rewriteConst4needsConst :: (RewriteFuns Constant, Constant)
-> Constant -> Result THFUnitaryFormula
rewriteConst4needsConst (_, c1 :: Constant
c1) c2 :: Constant
c2 =
 if Constant
c1 Constant -> Constant -> Bool
forall a. Eq a => a -> a -> Bool
== Constant
c2 then String -> Range -> Result THFUnitaryFormula
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "" Range
nullRange
 else THFUnitaryFormula -> Result THFUnitaryFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (THFUnitaryFormula -> Result THFUnitaryFormula)
-> (Constant -> THFUnitaryFormula)
-> Constant
-> Result THFUnitaryFormula
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 -> Result THFUnitaryFormula)
-> Constant -> Result THFUnitaryFormula
forall a b. (a -> b) -> a -> b
$ Constant
c2

needsConst :: Constant -> Named THFFormula -> Bool
needsConst :: Constant -> Named THFFormula -> Bool
needsConst c :: Constant
c f :: Named THFFormula
f =
 let r :: RewriteFuns Constant
r = RewriteFuns Constant
forall a. RewriteFuns a
rewriteTHF0 {rewriteConst :: (RewriteFuns Constant, Constant)
-> Constant -> Result THFUnitaryFormula
rewriteConst = (RewriteFuns Constant, Constant)
-> Constant -> Result THFUnitaryFormula
rewriteConst4needsConst}
     res :: Result (Named THFFormula)
res = (RewriteFuns Constant, Constant)
-> Named THFFormula -> Result (Named THFFormula)
forall a.
(RewriteFuns a, a) -> Named THFFormula -> Result (Named THFFormula)
rewriteSenFun (RewriteFuns Constant
r, Constant
c) Named THFFormula
f
 in case Result (Named THFFormula) -> Maybe (Named THFFormula)
forall a. Result a -> Maybe a
resultToMaybe Result (Named THFFormula)
res of
     Nothing -> Bool
True
     _ -> Bool
False

infer :: ConstMap -> [Named THFFormula]
          -> Result (ConstMap, [Named THFFormula])
infer :: ConstMap
-> [Named THFFormula] -> Result (ConstMap, [Named THFFormula])
infer cm :: ConstMap
cm fs :: [Named THFFormula]
fs =
 let constraints' :: Result [(Type, [(Type, Constraint)])]
constraints' = (Named THFFormula -> Result (Type, [(Type, Constraint)]))
-> [Named THFFormula] -> Result [(Type, [(Type, Constraint)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Constraints -> Result (Type, [(Type, Constraint)])
forall (m :: * -> *) a. Monad m => UniqueT m a -> m a
evalUniqueT (Constraints -> Result (Type, [(Type, Constraint)]))
-> (Named THFFormula -> Constraints)
-> Named THFFormula
-> Result (Type, [(Type, Constraint)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstMap -> THFFormula -> Constraints
getTypeC ConstMap
cm
      (THFFormula -> Constraints)
-> (Named THFFormula -> THFFormula)
-> Named THFFormula
-> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named THFFormula -> THFFormula
forall s a. SenAttr s a -> s
sentence) [Named THFFormula]
fs
     errMsg :: String
errMsg = "Sentences have to be of type OType"
     constraints :: Result [[(Type, Constraint)]]
constraints =
      ([(Type, [(Type, Constraint)])] -> [[(Type, Constraint)]])
-> Result [(Type, [(Type, Constraint)])]
-> Result [[(Type, Constraint)]]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Type, [(Type, Constraint)]) -> [(Type, Constraint)])
-> [(Type, [(Type, Constraint)])] -> [[(Type, Constraint)]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: Type
t, cs :: [(Type, Constraint)]
cs) -> (Type
OType, (String, Range, Type) -> Constraint
NormalC
       (String
errMsg, [(Type, Constraint)] -> Range
forall a. GetRange a => a -> Range
getRangeSpan [(Type, Constraint)]
cs, Type
t)) (Type, Constraint) -> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. a -> [a] -> [a]
: [(Type, Constraint)]
cs)) Result [(Type, [(Type, Constraint)])]
constraints'
 in do
  [Result [(Token, Type)]]
unis' <- ([[(Type, Constraint)]] -> [Result [(Token, Type)]])
-> Result [[(Type, Constraint)]] -> Result [Result [(Token, Type)]]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (([(Type, Constraint)] -> Result [(Token, Type)])
-> [[(Type, Constraint)]] -> [Result [(Token, Type)]]
forall a b. (a -> b) -> [a] -> [b]
map [(Type, Constraint)] -> Result [(Token, Type)]
unify') Result [[(Type, Constraint)]]
constraints
  [Result [(Token, Type)]] -> Result [[(Token, Type)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Result [(Token, Type)]]
unis' Result [[(Token, Type)]]
-> ([[(Token, Type)]] -> Result (ConstMap, [Named THFFormula]))
-> Result (ConstMap, [Named THFFormula])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ unis :: [[(Token, Type)]]
unis ->
      let (cm' :: Map Constant [Type]
cm', instances :: [RewriteArg]
instances) = (Map Constant [Type]
 -> (Named THFFormula, [(Token, Type)])
 -> (Map Constant [Type], RewriteArg))
-> Map Constant [Type]
-> [(Named THFFormula, [(Token, Type)])]
-> (Map Constant [Type], [RewriteArg])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
Data.List.mapAccumL
           (\ cm'_ :: Map Constant [Type]
cm'_ (f :: Named THFFormula
f, u :: [(Token, Type)]
u) ->
             let (cm'' :: Map Constant [Type]
cm'', m1 :: RewriteArg
m1) = (Map Constant [Type]
 -> Constant -> ConstInfo -> (Map Constant [Type], Maybe Int))
-> Map Constant [Type]
-> ConstMap
-> (Map Constant [Type], RewriteArg)
forall a k b c.
(a -> k -> b -> (a, c)) -> a -> Map k b -> (a, Map k c)
Data.Map.mapAccumWithKey
                  (\ cm''' :: Map Constant [Type]
cm''' c :: Constant
c ci :: ConstInfo
ci -> if Constant -> Named THFFormula -> Bool
needsConst Constant
c Named THFFormula
f
                     then Map Constant [Type]
-> Constant -> Type -> (Map Constant [Type], Maybe Int)
forall a b.
(Ord a, Eq b) =>
Map a [b] -> a -> b -> (Map a [b], Maybe Int)
insertAndIdx Map Constant [Type]
cm''' Constant
c
                           ([(Token, Type)] -> Type -> Type
apply [(Token, Type)]
u (ConstInfo -> Type
constType ConstInfo
ci))
                     else (Map Constant [Type]
cm''', Maybe Int
forall a. Maybe a
Nothing)) Map Constant [Type]
cm'_ ConstMap
cm
             in (Map Constant [Type]
cm'', RewriteArg
m1))
           Map Constant [Type]
forall k a. Map k a
Data.Map.empty ([Named THFFormula]
-> [[(Token, Type)]] -> [(Named THFFormula, [(Token, Type)])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Named THFFormula]
fs [[(Token, Type)]]
unis)
          new_cm :: ConstMap
new_cm = (Constant -> Type -> ConstInfo) -> Map Constant Type -> ConstMap
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Data.Map.mapWithKey (\ k :: Constant
k v :: Type
v ->
           ConstInfo :: Constant -> Name -> Type -> Annotations -> ConstInfo
ConstInfo { constId :: Constant
constId = Constant
k,
                       constName :: Name
constName = Constant -> Name
N_Atomic_Word Constant
k,
                       constType :: Type
constType = Type
v,
                       constAnno :: Annotations
constAnno = Annotations
Null}) (Map Constant Type -> ConstMap) -> Map Constant Type -> ConstMap
forall a b. (a -> b) -> a -> b
$ Map Constant [Type] -> Map Constant Type
forall a. Map Constant [a] -> Map Constant a
flattenMap Map Constant [Type]
cm'
      in do
           let r :: RewriteFuns RewriteArg
r = RewriteFuns RewriteArg
forall a. RewriteFuns a
rewriteTHF0 {
             rewriteVariableList :: (RewriteFuns RewriteArg, RewriteArg)
-> THFVariableList -> Result THFVariableList
rewriteVariableList = (RewriteFuns RewriteArg, RewriteArg)
-> THFVariableList -> Result THFVariableList
rewriteVariableList_,
             rewriteConst :: (RewriteFuns RewriteArg, RewriteArg)
-> Constant -> Result THFUnitaryFormula
rewriteConst = (RewriteFuns RewriteArg, RewriteArg)
-> Constant -> Result THFUnitaryFormula
rewriteConst_
           }
           [Named THFFormula]
fs' <- ((Named THFFormula, RewriteArg) -> Result (Named THFFormula))
-> [(Named THFFormula, RewriteArg)] -> Result [Named THFFormula]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (f :: Named THFFormula
f, i :: RewriteArg
i) -> (RewriteFuns RewriteArg, RewriteArg)
-> Named THFFormula -> Result (Named THFFormula)
forall a.
(RewriteFuns a, a) -> Named THFFormula -> Result (Named THFFormula)
rewriteSenFun (RewriteFuns RewriteArg
r, RewriteArg
i) Named THFFormula
f)
            ([Named THFFormula]
-> [RewriteArg] -> [(Named THFFormula, RewriteArg)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Named THFFormula]
fs [RewriteArg]
instances)
           (ConstMap, [Named THFFormula])
-> Result (ConstMap, [Named THFFormula])
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstMap
new_cm, [Named THFFormula]
fs')

typeConstsOf :: Type -> [Constant]
typeConstsOf :: Type -> [Constant]
typeConstsOf (MapType tp1 :: Type
tp1 tp2 :: Type
tp2) = (Type -> [Constant]
typeConstsOf Type
tp1) [Constant] -> [Constant] -> [Constant]
forall a. [a] -> [a] -> [a]
++ (Type -> [Constant]
typeConstsOf Type
tp2)
typeConstsOf (ProdType tps :: [Type]
tps) = [[Constant]] -> [Constant]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constant]] -> [Constant]) -> [[Constant]] -> [Constant]
forall a b. (a -> b) -> a -> b
$ (Type -> [Constant]) -> [Type] -> [[Constant]]
forall a b. (a -> b) -> [a] -> [b]
map Type -> [Constant]
typeConstsOf [Type]
tps
typeConstsOf (CType c :: Constant
c) = [Constant
c]
typeConstsOf (ParType t :: Type
t) = Type -> [Constant]
typeConstsOf Type
t
typeConstsOf _ = []

collectVariableTypes :: (AnaFuns a Constant, a) -> [THFVariable] -> Result [Constant]
collectVariableTypes :: (AnaFuns a Constant, a) -> THFVariableList -> Result [Constant]
collectVariableTypes _ vs :: THFVariableList
vs =
 let tps :: [Type]
tps = [Maybe Type] -> [Type]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Type] -> [Type]) -> [Maybe Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (THFVariable -> Maybe Type) -> THFVariableList -> [Maybe Type]
forall a b. (a -> b) -> [a] -> [b]
map (\v :: THFVariable
v -> case THFVariable
v of
                                   TV_THF_Typed_Variable _ t :: THFTopLevelType
t ->
                                    THFTopLevelType -> Maybe Type
thfTopLevelTypeToType THFTopLevelType
t 
                                   _ -> Maybe Type
forall a. Maybe a
Nothing) THFVariableList
vs
 in [Constant] -> Result [Constant]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constant] -> Result [Constant])
-> ([[Constant]] -> [Constant])
-> [[Constant]]
-> Result [Constant]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Constant]] -> [Constant]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constant]] -> Result [Constant])
-> [[Constant]] -> Result [Constant]
forall a b. (a -> b) -> a -> b
$ (Type -> [Constant]) -> [Type] -> [[Constant]]
forall a b. (a -> b) -> [a] -> [b]
map Type -> [Constant]
typeConstsOf [Type]
tps

getSymbols :: SignTHF -> THFFormula -> [SymbolTHF]
getSymbols :: SignTHF -> THFFormula -> [SymbolTHF]
getSymbols s :: SignTHF
s f :: THFFormula
f =
 let f' :: Named THFFormula
f' = String -> THFFormula -> Named THFFormula
forall a s. a -> s -> SenAttr s a
makeNamed "tmp" THFFormula
f
     cs :: [(Constant, ConstInfo)]
cs = ConstMap -> [(Constant, ConstInfo)]
forall k a. Map k a -> [(k, a)]
Data.Map.toList (ConstMap -> [(Constant, ConstInfo)])
-> ConstMap -> [(Constant, ConstInfo)]
forall a b. (a -> b) -> a -> b
$ (ConstMap, [Named THFFormula]) -> ConstMap
forall a b. (a, b) -> a
fst ((ConstMap, [Named THFFormula]) -> ConstMap)
-> (ConstMap, [Named THFFormula]) -> ConstMap
forall a b. (a -> b) -> a -> b
$ String
-> Result (ConstMap, [Named THFFormula])
-> (ConstMap, [Named THFFormula])
forall a. String -> Result a -> a
propagateErrors "THF.Poly.getSymbols" (Result (ConstMap, [Named THFFormula])
 -> (ConstMap, [Named THFFormula]))
-> Result (ConstMap, [Named THFFormula])
-> (ConstMap, [Named THFFormula])
forall a b. (a -> b) -> a -> b
$
                            ConstMap
-> [Named THFFormula] -> Result (ConstMap, [Named THFFormula])
infer (SignTHF -> ConstMap
consts SignTHF
s) [Named THFFormula
f']
     r :: AnaFuns a Constant
r = AnaFuns a Constant
forall a b. AnaFuns a b
anaTHF0 { anaVariableList :: (AnaFuns a Constant, a) -> THFVariableList -> Result [Constant]
anaVariableList = (AnaFuns a Constant, a) -> THFVariableList -> Result [Constant]
forall a.
(AnaFuns a Constant, a) -> THFVariableList -> Result [Constant]
collectVariableTypes }
     ts' :: [Constant]
ts' = String -> Result [Constant] -> [Constant]
forall a. String -> Result a -> a
propagateErrors "THF.Poly.getSymbols" (Result [Constant] -> [Constant])
-> Result [Constant] -> [Constant]
forall a b. (a -> b) -> a -> b
$ (AnaFuns [Any] Constant, [Any])
-> Named THFFormula -> Result [Constant]
forall a b. (AnaFuns a b, a) -> Named THFFormula -> Result [b]
anaSenFun (AnaFuns [Any] Constant
forall a. AnaFuns a Constant
r, []) Named THFFormula
f'
     ts :: [Constant]
ts = Set Constant -> [Constant]
forall a. Set a -> [a]
Data.Set.toList (Set Constant -> [Constant])
-> ([Constant] -> Set Constant) -> [Constant] -> [Constant]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Constant] -> Set Constant
forall a. Ord a => [a] -> Set a
Data.Set.fromList ([Constant] -> [Constant]) -> [Constant] -> [Constant]
forall a b. (a -> b) -> a -> b
$ [Constant]
ts' [Constant] -> [Constant] -> [Constant]
forall a. [a] -> [a] -> [a]
++
          ([[Constant]] -> [Constant]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (((Constant, ConstInfo) -> [Constant])
-> [(Constant, ConstInfo)] -> [[Constant]]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> [Constant]
typeConstsOf (Type -> [Constant])
-> ((Constant, ConstInfo) -> Type)
-> (Constant, ConstInfo)
-> [Constant]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstInfo -> Type
constType (ConstInfo -> Type)
-> ((Constant, ConstInfo) -> ConstInfo)
-> (Constant, ConstInfo)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constant, ConstInfo) -> ConstInfo
forall a b. (a, b) -> b
snd) [(Constant, ConstInfo)]
cs))
     symsC :: [SymbolTHF]
symsC = ((Constant, ConstInfo) -> SymbolTHF)
-> [(Constant, ConstInfo)] -> [SymbolTHF]
forall a b. (a -> b) -> [a] -> [b]
map (\(_,ci :: ConstInfo
ci) -> Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
Symbol { symId :: Constant
symId = ConstInfo -> Constant
constId ConstInfo
ci,
                                      symName :: Name
symName = ConstInfo -> Name
constName ConstInfo
ci,
                                      symType :: SymbolType
symType = Type -> SymbolType
ST_Const (Type -> SymbolType) -> Type -> SymbolType
forall a b. (a -> b) -> a -> b
$ ConstInfo -> Type
constType ConstInfo
ci }) [(Constant, ConstInfo)]
cs
     symsT :: [SymbolTHF]
symsT = (Constant -> SymbolTHF) -> [Constant] -> [SymbolTHF]
forall a b. (a -> b) -> [a] -> [b]
map (\n :: Constant
n -> case Constant -> Map Constant TypeInfo -> Maybe TypeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Data.Map.lookup Constant
n (SignTHF -> Map Constant TypeInfo
types SignTHF
s) of
                         Just t :: TypeInfo
t -> Symbol :: Constant -> Name -> SymbolType -> SymbolTHF
Symbol { symId :: Constant
symId = TypeInfo -> Constant
THF.Sign.typeId TypeInfo
t,
                                            symName :: Name
symName = TypeInfo -> Name
typeName TypeInfo
t,
                                            symType :: SymbolType
symType = Kind -> SymbolType
ST_Type Kind
Kind}
                         Nothing -> String -> SymbolTHF
forall a. HasCallStack => String -> a
error (String -> SymbolTHF) -> String -> SymbolTHF
forall a b. (a -> b) -> a -> b
$ "THF.Poly.getSymbols: " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                            "Unknown type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Constant -> String
forall a. Show a => a -> String
show Constant
n)) [Constant]
ts
 in [SymbolTHF]
symsC [SymbolTHF] -> [SymbolTHF] -> [SymbolTHF]
forall a. [a] -> [a] -> [a]
++ [SymbolTHF]
symsT

type_check :: TypeMap -> ConstMap -> [Named THFFormula]
               -> Result [[(Token, Type)]]
type_check :: Map Constant TypeInfo
-> ConstMap -> [Named THFFormula] -> Result [[(Token, Type)]]
type_check _ cm :: ConstMap
cm sens :: [Named THFFormula]
sens = do
 let constraints' :: Result [(Type, [(Type, Constraint)])]
constraints' = (Named THFFormula -> Result (Type, [(Type, Constraint)]))
-> [Named THFFormula] -> Result [(Type, [(Type, Constraint)])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Constraints -> Result (Type, [(Type, Constraint)])
forall (m :: * -> *) a. Monad m => UniqueT m a -> m a
evalUniqueT (Constraints -> Result (Type, [(Type, Constraint)]))
-> (Named THFFormula -> Constraints)
-> Named THFFormula
-> Result (Type, [(Type, Constraint)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      ConstMap -> THFFormula -> Constraints
getTypeC ConstMap
cm (THFFormula -> Constraints)
-> (Named THFFormula -> THFFormula)
-> Named THFFormula
-> Constraints
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named THFFormula -> THFFormula
forall s a. SenAttr s a -> s
sentence) [Named THFFormula]
sens
 let errMsg :: String
errMsg = "Every formula is expected to be of type OType"
 let constraints :: Result [[(Type, Constraint)]]
constraints =
      ([(Type, [(Type, Constraint)])] -> [[(Type, Constraint)]])
-> Result [(Type, [(Type, Constraint)])]
-> Result [[(Type, Constraint)]]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (((Type, [(Type, Constraint)]) -> [(Type, Constraint)])
-> [(Type, [(Type, Constraint)])] -> [[(Type, Constraint)]]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: Type
t, cs :: [(Type, Constraint)]
cs) -> (Type
OType, (String, Range, Type) -> Constraint
NormalC (String
errMsg, Range
nullRange, Type
t)) (Type, Constraint) -> [(Type, Constraint)] -> [(Type, Constraint)]
forall a. a -> [a] -> [a]
: [(Type, Constraint)]
cs))
            Result [(Type, [(Type, Constraint)])]
constraints'
 [Result [(Token, Type)]]
unifications <- ([[(Type, Constraint)]] -> [Result [(Token, Type)]])
-> Result [[(Type, Constraint)]] -> Result [Result [(Token, Type)]]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (([(Type, Constraint)] -> Result [(Token, Type)])
-> [[(Type, Constraint)]] -> [Result [(Token, Type)]]
forall a b. (a -> b) -> [a] -> [b]
map [(Type, Constraint)] -> Result [(Token, Type)]
unify') Result [[(Type, Constraint)]]
constraints
 [Result [(Token, Type)]] -> Result [[(Token, Type)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [Result [(Token, Type)]]
unifications