{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/THFP_P2HasCASL.hs
Description :  Comorphism from THFP to HasCASL
Copyright   :  (c) Jonathan von Schroeder, DFKI Bremen 2013
License     :  GPLv2 or higher, see LICENSE.txt

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

The embedding comorphism from THFP to HasCASL.
-}

module Comorphisms.THFP_P2HasCASL where

import Logic.Logic as Logic
import Logic.Comorphism

import Common.ProofTree
import Common.Result
import Common.Id
import Common.AS_Annotation

import HasCASL.Logic_HasCASL
import HasCASL.Sublogic
import HasCASL.Le as HCLe
import HasCASL.As as HCAs
import HasCASL.AsUtils
import HasCASL.Builtin

import THF.As as THFAs
import THF.Logic_THF
import THF.Cons as THFCons
import THF.Sign as THFSign
import THF.Utils (thfTopLevelTypeToType)
import qualified THF.Sublogic as SL

import Control.Monad

import qualified Data.Map as Map
import qualified Data.Set as Set

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

instance Language THFP_P2HasCASL

instance Comorphism THFP_P2HasCASL
                THF SL.THFSl
                BasicSpecTHF THFFormula () ()
                SignTHF MorphismTHF SymbolTHF () ProofTree
                HasCASL Sublogic
                BasicSpec Sentence SymbItems SymbMapItems
                Env Morphism Symbol RawSymbol () where
    sourceLogic :: THFP_P2HasCASL -> THF
sourceLogic THFP_P2HasCASL = THF
THF
    sourceSublogic :: THFP_P2HasCASL -> THFSl
sourceSublogic THFP_P2HasCASL = THFSl
SL.tHFP_P
    targetLogic :: THFP_P2HasCASL -> HasCASL
targetLogic THFP_P2HasCASL = HasCASL
HasCASL
    mapSublogic :: THFP_P2HasCASL -> THFSl -> Maybe Sublogic
mapSublogic THFP_P2HasCASL _ = Sublogic -> Maybe Sublogic
forall a. a -> Maybe a
Just Sublogic
reqSubLogicForTHFP
    map_theory :: THFP_P2HasCASL
-> (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence])
map_theory THFP_P2HasCASL = (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence])
transTheory
    map_symbol :: THFP_P2HasCASL -> SignTHF -> SymbolTHF -> Set Symbol
map_symbol THFP_P2HasCASL _ s :: SymbolTHF
s = String -> Result (Set Symbol) -> Set Symbol
forall a. String -> Result a -> a
propagateErrors "" (Result (Set Symbol) -> Set Symbol)
-> Result (Set Symbol) -> Set Symbol
forall a b. (a -> b) -> a -> b
$ SymbolTHF -> Result (Set Symbol)
transSymbol SymbolTHF
s
    has_model_expansion :: THFP_P2HasCASL -> Bool
has_model_expansion THFP_P2HasCASL = Bool
True

reqSubLogicForTHFP :: Sublogic
reqSubLogicForTHFP :: Sublogic
reqSubLogicForTHFP = Sublogic :: Bool
-> Bool
-> Bool
-> Bool
-> Classes
-> Bool
-> Bool
-> Bool
-> Formulas
-> Sublogic
Sublogic
    { has_sub :: Bool
has_sub = Bool
False
    , has_part :: Bool
has_part = Bool
False
    , has_eq :: Bool
has_eq = Bool
True
    , has_pred :: Bool
has_pred = Bool
True
    , type_classes :: Classes
type_classes = Classes
NoClasses
    , has_polymorphism :: Bool
has_polymorphism = Bool
False
    , has_type_constructors :: Bool
has_type_constructors = Bool
False
    , has_products :: Bool
has_products = Bool
True
    , which_logic :: Formulas
which_logic = Formulas
HOL }

-- Translation of a Theory

transTheory :: (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence])
transTheory :: (SignTHF, [Named THFFormula]) -> Result (Env, [Named Sentence])
transTheory (s :: SignTHF
s@(Sign t :: TypeMap
t c :: ConstMap
c _), nfs :: [Named THFFormula]
nfs) =
 let typeMap_ :: Map Id TypeInfo
typeMap_ = [(Id, TypeInfo)] -> Map Id TypeInfo
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, TypeInfo)] -> Map Id TypeInfo)
-> [(Id, TypeInfo)] -> Map Id TypeInfo
forall a b. (a -> b) -> a -> b
$ ((Constant, TypeInfo) -> (Id, TypeInfo))
-> [(Constant, TypeInfo)] -> [(Id, TypeInfo)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, THFSign.TypeInfo i :: Constant
i _ k :: Kind
k _) ->
      let id' :: Token
id' = case Constant
i of
                A_Lower_Word tok :: Token
tok -> Token
tok
                A_Single_Quoted tok :: Token
tok -> Token
tok
      in case Kind
k of
          Kind -> ([Token] -> Id
mkId [Token
id'], TypeInfo :: RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
HCLe.TypeInfo {
           typeKind :: RawKind
HCLe.typeKind = () -> RawKind
forall a. a -> AnyKind a
ClassKind (), -- the only supported kind right now
           otherTypeKinds :: Set Kind
otherTypeKinds = Set Kind
forall a. Set a
Set.empty,
           superTypes :: Set Id
superTypes = Set Id
forall a. Set a
Set.empty,
           typeDefn :: TypeDefn
typeDefn = TypeDefn
NoTypeDefn
           })) (TypeMap -> [(Constant, TypeInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList TypeMap
t)
     assumps_ :: Map Id (Set OpInfo)
assumps_ = [(Id, Set OpInfo)] -> Map Id (Set OpInfo)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Set OpInfo)] -> Map Id (Set OpInfo))
-> [(Id, Set OpInfo)] -> Map Id (Set OpInfo)
forall a b. (a -> b) -> a -> b
$ ((Constant, ConstInfo) -> (Id, Set OpInfo))
-> [(Constant, ConstInfo)] -> [(Id, Set OpInfo)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (_, THFSign.ConstInfo i :: Constant
i _ t' :: Type
t' _) ->
      let id' :: Token
id' = case Constant
i of
                A_Lower_Word tok :: Token
tok -> Token
tok
                A_Single_Quoted tok :: Token
tok -> Token
tok
      in ([Token] -> Id
mkId [Token
id'], OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton OpInfo :: TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo {
           opType :: TypeScheme
opType = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] (Type -> Type
toHCType Type
t') (Type -> Range
forall a. GetRange a => a -> Range
getRange Type
t'),
           opAttrs :: Set OpAttr
opAttrs = Set OpAttr
forall a. Set a
Set.empty,
           opDefn :: OpDefn
opDefn = OpBrand -> OpDefn
NoOpDefn OpBrand
HCAs.Fun
          })) (ConstMap -> [(Constant, ConstInfo)]
forall k a. Map k a -> [(k, a)]
Map.toList ConstMap
c)
     env :: Env
env = Env
preEnv { typeMap :: Map Id TypeInfo
typeMap = Map Id TypeInfo
typeMap_,
                         assumps :: Map Id (Set OpInfo)
assumps = Map Id (Set OpInfo)
assumps_ }
 in do
    [Named Sentence]
nfs' <- (Named THFFormula -> Result (Named Sentence))
-> [Named THFFormula] -> Result [Named Sentence]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignTHF -> Named THFFormula -> Result (Named Sentence)
transNamedFormula SignTHF
s) [Named THFFormula]
nfs
    (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
env, [Named Sentence]
nfs')

transNamedFormula :: SignTHF -> Named THFFormula -> Result (Named Sentence)
transNamedFormula :: SignTHF -> Named THFFormula -> Result (Named Sentence)
transNamedFormula sig :: SignTHF
sig ns :: Named THFFormula
ns = do
 Term
s' <- SignTHF -> THFFormula -> Result Term
transFormula SignTHF
sig (THFFormula -> Result Term) -> THFFormula -> Result Term
forall a b. (a -> b) -> a -> b
$ Named THFFormula -> THFFormula
forall s a. SenAttr s a -> s
sentence Named THFFormula
ns
 Named Sentence -> Result (Named Sentence)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named Sentence -> Result (Named Sentence))
-> Named Sentence -> Result (Named Sentence)
forall a b. (a -> b) -> a -> b
$ Named THFFormula
ns { sentence :: Sentence
sentence = Term -> Sentence
Formula Term
s' }

transFormula :: SignTHF -> THFFormula -> Result HCAs.Term
transFormula :: SignTHF -> THFFormula -> Result Term
transFormula sig :: SignTHF
sig (TF_THF_Logic_Formula lf :: THFLogicFormula
lf) = case THFLogicFormula
lf of
 TLF_THF_Binary_Formula bf :: THFBinaryFormula
bf -> SignTHF -> THFBinaryFormula -> Result Term
transBinaryFormula SignTHF
sig THFBinaryFormula
bf
 TLF_THF_Unitary_Formula uf :: THFUnitaryFormula
uf -> SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig THFUnitaryFormula
uf
 _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
transFormula _ _ = String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange

transBinaryFormula :: SignTHF -> THFBinaryFormula -> Result HCAs.Term
transBinaryFormula :: SignTHF -> THFBinaryFormula -> Result Term
transBinaryFormula sig :: SignTHF
sig bf :: THFBinaryFormula
bf = case THFBinaryFormula
bf of
 TBF_THF_Binary_Pair uf1 :: THFUnitaryFormula
uf1 cn :: THFPairConnective
cn uf2 :: THFUnitaryFormula
uf2 -> do
  Term
uf1' <- SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig THFUnitaryFormula
uf1
  Term
uf2' <- SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig THFUnitaryFormula
uf2
  let tm :: Id -> Term
tm id' :: Id
id' = Id -> Range -> Term -> Term -> Term
mkLogTerm Id
id' (THFBinaryFormula -> Range
forall a. GetRange a => a -> Range
getRange THFBinaryFormula
bf) Term
uf1' Term
uf2'
  case THFPairConnective
cn of
   Infix_Equality -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> Term
tm Id
eqId
   Infix_Inequality -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
notId TypeScheme
notType [] (THFBinaryFormula -> Range
forall a. GetRange a => a -> Range
getRange THFBinaryFormula
bf) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Term
tm Id
eqId
   Equivalent -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> Term
tm Id
eqvId
   Implication -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> Term
tm Id
implId
   IF -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
    -- mkEqTerm implId (getRange bf) uf2' uf1'
   XOR -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
   NOR -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
   NAND -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
 TBF_THF_Binary_Tuple bt :: THFBinaryTuple
bt -> case THFBinaryTuple
bt of
   TBT_THF_Or_Formula ufs :: [THFUnitaryFormula]
ufs -> do
    (u :: Term
u : ufs' :: [Term]
ufs') <- (THFUnitaryFormula -> Result Term)
-> [THFUnitaryFormula] -> Result [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig) [THFUnitaryFormula]
ufs
    (Term -> Term -> Result Term) -> Term -> [Term] -> Result Term
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ a :: Term
a b :: Term
b -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
nullRange Term
a Term
b) Term
u [Term]
ufs'
   TBT_THF_And_Formula ufs :: [THFUnitaryFormula]
ufs -> do
    (u :: Term
u : ufs' :: [Term]
ufs') <- (THFUnitaryFormula -> Result Term)
-> [THFUnitaryFormula] -> Result [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig) [THFUnitaryFormula]
ufs
    (Term -> Term -> Result Term) -> Term -> [Term] -> Result Term
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ a :: Term
a b :: Term
b -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> Range -> Term -> Term -> Term
mkLogTerm Id
orId Range
nullRange Term
a Term
b) Term
u [Term]
ufs'
   TBT_THF_Apply_Formula (u :: THFUnitaryFormula
u : ufs :: [THFUnitaryFormula]
ufs) -> do
    Term
u' <- SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig THFUnitaryFormula
u
    [Term]
ufs' <- (THFUnitaryFormula -> Result Term)
-> [THFUnitaryFormula] -> Result [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig) [THFUnitaryFormula]
ufs
    Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
mkApplTerm Term
u' [Term]
ufs'
   _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Translation not possible!" Range
nullRange
 _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange

transUnitaryFormula :: SignTHF -> THFUnitaryFormula -> Result HCAs.Term
transUnitaryFormula :: SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula sig :: SignTHF
sig uf :: THFUnitaryFormula
uf = case THFUnitaryFormula
uf of
 TUF_THF_Quantified_Formula qf :: THFQuantifiedFormula
qf -> do
  (quantifier :: Quantifier
quantifier, vs :: THFVariableList
vs, uf' :: THFUnitaryFormula
uf') <- case THFQuantifiedFormula
qf of
    TQF_THF_Quantified_Formula qf' :: THFQuantifier
qf' vs :: THFVariableList
vs uf' :: THFUnitaryFormula
uf' -> case THFQuantifier
qf' of
     TQ_ForAll -> (Quantifier, THFVariableList, THFUnitaryFormula)
-> Result (Quantifier, THFVariableList, THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantifier
Universal, THFVariableList
vs, THFUnitaryFormula
uf')
     TQ_Exists -> (Quantifier, THFVariableList, THFUnitaryFormula)
-> Result (Quantifier, THFVariableList, THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantifier
Existential, THFVariableList
vs, THFUnitaryFormula
uf')
     _ -> String
-> Range -> Result (Quantifier, THFVariableList, THFUnitaryFormula)
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
    T0QF_THF_Quantified_Var q :: Quantifier
q vs :: THFVariableList
vs uf' :: THFUnitaryFormula
uf' -> case Quantifier
q of
     T0Q_ForAll -> (Quantifier, THFVariableList, THFUnitaryFormula)
-> Result (Quantifier, THFVariableList, THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantifier
Universal, THFVariableList
vs, THFUnitaryFormula
uf')
     T0Q_Exists -> (Quantifier, THFVariableList, THFUnitaryFormula)
-> Result (Quantifier, THFVariableList, THFUnitaryFormula)
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantifier
Existential, THFVariableList
vs, THFUnitaryFormula
uf')
    _ -> String
-> Range -> Result (Quantifier, THFVariableList, THFUnitaryFormula)
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
  Term
uf'' <- SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig THFUnitaryFormula
uf'
  let vs' :: [GenVarDecl]
vs' = (THFVariable -> GenVarDecl) -> THFVariableList -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map THFVariable -> GenVarDecl
variable2VarDecl THFVariableList
vs
  Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
quantifier [GenVarDecl]
vs' Term
uf'' (THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRange THFUnitaryFormula
uf))
 TUF_THF_Unary_Formula c :: THFUnaryConnective
c lf :: THFLogicFormula
lf -> do
  Term
lf' <- SignTHF -> THFFormula -> Result Term
transFormula SignTHF
sig (THFLogicFormula -> THFFormula
TF_THF_Logic_Formula THFLogicFormula
lf)
  case THFUnaryConnective
c of
   Negation -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
notId TypeScheme
notType [] (THFLogicFormula -> Range
forall a. GetRange a => a -> Range
getRange THFLogicFormula
lf) Term
lf'
   _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
 TUF_THF_Atom a :: THFAtom
a -> case THFAtom
a of
  TA_THF_Conn_Term _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error ("Not directly translatable! - " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                             "Maybe the term is malformed?") Range
nullRange
  T0A_Constant c :: Constant
c ->
   let id' :: Id
id' = case Constant
c of
           A_Lower_Word tok :: Token
tok -> [Token] -> Id
mkId [Token
tok]
           A_Single_Quoted tok :: Token
tok -> [Token] -> Id
mkId [Token
tok]
       t :: TypeScheme
t = case Constant -> ConstMap -> Maybe ConstInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Constant
c (SignTHF -> ConstMap
consts SignTHF
sig) of
            Just ci :: ConstInfo
ci -> [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] (Type -> Type
toHCType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ ConstInfo -> Type
constType ConstInfo
ci) Range
nullRange
            Nothing -> [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg (String -> Id
stringToId "tmp") Variance
NonVar
              (Kind -> VarKind
VarKind (Id -> Kind
forall a. a -> AnyKind a
ClassKind (String -> Id
stringToId "tmp"))) (() -> RawKind
forall a. a -> AnyKind a
ClassKind ()) 0 SeparatorKind
Comma Range
nullRange]
             (Id -> RawKind -> Int -> Type
TypeName (String -> Id
stringToId "tmp") (() -> RawKind
forall a. a -> AnyKind a
ClassKind ()) (-1)) Range
nullRange
   in Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
HCAs.Fun (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
id' [] (Constant -> Range
forall a. GetRange a => a -> Range
getRange Constant
c)) TypeScheme
t [] InstKind
Infer Range
nullRange
  T0A_Variable v :: Token
v -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
v)
                             (Id -> RawKind -> Int -> Type
TypeName (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
v)
                               (() -> RawKind
forall a. a -> AnyKind a
ClassKind ()) (-1)) SeparatorKind
Comma Range
nullRange
   -- what type should we give a (bound) variable?
  _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange
 TUF_THF_Tuple t :: THFTuple
t -> do
  [Term]
t' <- (THFLogicFormula -> Result Term) -> THFTuple -> Result [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (SignTHF -> THFFormula -> Result Term
transFormula SignTHF
sig (THFFormula -> Result Term)
-> (THFLogicFormula -> THFFormula)
-> THFLogicFormula
-> Result Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. THFLogicFormula -> THFFormula
TF_THF_Logic_Formula) THFTuple
t
  Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
TupleTerm [Term]
t' (THFTuple -> Range
forall a. GetRange a => a -> Range
getRange THFTuple
t)
 TUF_THF_Logic_Formula_Par lf :: THFLogicFormula
lf -> SignTHF -> THFFormula -> Result Term
transFormula SignTHF
sig (THFLogicFormula -> THFFormula
TF_THF_Logic_Formula THFLogicFormula
lf)
 T0UF_THF_Abstraction vs :: THFVariableList
vs uf' :: THFUnitaryFormula
uf' -> do
  [Term]
vs' <- (THFVariable -> Result Term) -> THFVariableList -> Result [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM THFVariable -> Result Term
variable2Term THFVariableList
vs
  Term
uf'' <- SignTHF -> THFUnitaryFormula -> Result Term
transUnitaryFormula SignTHF
sig THFUnitaryFormula
uf'
  Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm [Term]
vs' Partiality
Total Term
uf'' (THFUnitaryFormula -> Range
forall a. GetRange a => a -> Range
getRange THFUnitaryFormula
uf)
 _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "Not yet implemented!" Range
nullRange

variable2Term :: THFVariable -> Result HCAs.Term
variable2Term :: THFVariable -> Result Term
variable2Term v :: THFVariable
v@(TV_Variable _) = case THFVariable -> GenVarDecl
variable2VarDecl THFVariable
v of
 GenVarDecl vdecl :: VarDecl
vdecl -> Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ VarDecl -> Term
QualVar VarDecl
vdecl
 _ -> String -> Range -> Result Term
forall a. String -> Range -> Result a
fatal_error "This shouldn't happen!" Range
nullRange
variable2Term (TV_THF_Typed_Variable t :: Token
t tp :: THFTopLevelType
tp) =
 case THFTopLevelType -> Maybe Type
thfTopLevelTypeToType THFTopLevelType
tp of
   Just tp' :: Type
tp' -> do
    Term
t' <- THFVariable -> Result Term
variable2Term (Token -> THFVariable
TV_Variable Token
t)
    Term -> Result Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Result Term) -> Term -> Result Term
forall a b. (a -> b) -> a -> b
$ Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
t' TypeQual
OfType (Type -> Type
toHCType Type
tp') Range
nullRange
   Nothing -> THFVariable -> Result Term
variable2Term (Token -> THFVariable
TV_Variable Token
t)

variable2VarDecl :: THFVariable -> GenVarDecl
variable2VarDecl :: THFVariable -> GenVarDecl
variable2VarDecl (TV_Variable t :: Token
t) = TypeArg -> GenVarDecl
GenTypeVarDecl (TypeArg -> GenVarDecl) -> TypeArg -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg
 ([Token] -> Id
mkId [Token
t]) Variance
NonVar (Kind -> VarKind
VarKind (Id -> Kind
forall a. a -> AnyKind a
ClassKind ([Token] -> Id
mkId [Token
t]))) (() -> RawKind
forall a. a -> AnyKind a
ClassKind ()) 0 SeparatorKind
Comma
 (Token -> Range
forall a. GetRange a => a -> Range
getRange Token
t)
variable2VarDecl (TV_THF_Typed_Variable t :: Token
t tp :: THFTopLevelType
tp) =
 case THFTopLevelType -> Maybe Type
thfTopLevelTypeToType THFTopLevelType
tp of
  Just tp' :: Type
tp' -> VarDecl -> GenVarDecl
GenVarDecl (VarDecl -> GenVarDecl) -> VarDecl -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl ([Token] -> Id
mkId [Token
t]) (Type -> Type
toHCType Type
tp') SeparatorKind
Comma
               (Token -> Range
forall a. GetRange a => a -> Range
getRange Token
t)
  Nothing -> THFVariable -> GenVarDecl
variable2VarDecl (Token -> THFVariable
TV_Variable Token
t)

transSymbol :: SymbolTHF -> Result (Set.Set Symbol)
transSymbol :: SymbolTHF -> Result (Set Symbol)
transSymbol (THFCons.Symbol i :: Constant
i _ t :: SymbolType
t) =
 let id' :: Id
id' = case Constant
i of
           A_Lower_Word tok :: Token
tok -> [Token] -> Id
mkId [Token
tok]
           A_Single_Quoted tok :: Token
tok -> [Token] -> Id
mkId [Token
tok]
 in case SymbolType
t of
  (ST_Type Kind) -> Set Symbol -> Result (Set Symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Symbol -> Result (Set Symbol))
-> Set Symbol -> Result (Set Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbolType -> Symbol
HCLe.Symbol Id
id' (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$
   RawKind -> SymbolType
TypeAsItemType (RawKind -> SymbolType) -> RawKind -> SymbolType
forall a b. (a -> b) -> a -> b
$ () -> RawKind
forall a. a -> AnyKind a
ClassKind ()
  (ST_Const t_ :: Type
t_) -> {- currently only "simple" kinds are allowed in thf so this
                     must be the type of an operator -}
    case Type -> (Type, Maybe Type)
tailType Type
t_ of
     (t' :: Type
t', Just OType) -> Set Symbol -> Result (Set Symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Symbol -> Result (Set Symbol))
-> Set Symbol -> Result (Set Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbolType -> Symbol
HCLe.Symbol Id
id' (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$
      TypeScheme -> SymbolType
PredAsItemType (TypeScheme -> SymbolType) -> TypeScheme -> SymbolType
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] (Type -> Type
toHCType Type
t') (Type -> Range
forall a. GetRange a => a -> Range
getRange Type
t')
     _ -> Set Symbol -> Result (Set Symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set Symbol -> Result (Set Symbol))
-> Set Symbol -> Result (Set Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbolType -> Symbol
HCLe.Symbol Id
id' (SymbolType -> Symbol) -> SymbolType -> Symbol
forall a b. (a -> b) -> a -> b
$
      TypeScheme -> SymbolType
OpAsItemType (TypeScheme -> SymbolType) -> TypeScheme -> SymbolType
forall a b. (a -> b) -> a -> b
$ [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [] (Type -> Type
toHCType Type
t_) (Type -> Range
forall a. GetRange a => a -> Range
getRange Type
t_)

tailType :: THFCons.Type -> (THFCons.Type, Maybe THFCons.Type)
tailType :: Type -> (Type, Maybe Type)
tailType (MapType t1 :: Type
t1 t2 :: Type
t2) = case Type
t2 of
 MapType _ _ ->
  let (t2' :: Type
t2', tailT :: Maybe Type
tailT) = Type -> (Type, Maybe Type)
tailType Type
t2
  in (Type -> Type -> Type
MapType Type
t1 Type
t2', Maybe Type
tailT)
 _ -> (Type
t1, Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t2)
tailType t :: Type
t = (Type
t, Maybe Type
forall a. Maybe a
Nothing)

toHCType :: THFCons.Type -> HCAs.Type
toHCType :: Type -> Type
toHCType IType = Id -> Type
toType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ String -> Id
stringToId "$i"
toHCType TType = Id -> Type
toType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ String -> Id
stringToId "$t"
toHCType OType = Type
unitType
toHCType (MapType t1 :: Type
t1 t2 :: Type
t2) = Type -> Arrow -> Type -> Type
mkFunArrType (Type -> Type
toHCType Type
t1) Arrow
FunArr (Type -> Type
toHCType Type
t2)
toHCType (ProdType ts :: [Type]
ts) = [Type] -> Type
mkProductType ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
toHCType [Type]
ts
toHCType (CType c :: Constant
c) = Id -> Type
toType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ Constant -> String
forall a. Show a => a -> String
show Constant
c
toHCType (SType _) = String -> Type
forall a. HasCallStack => String -> a
error "not implemented" {- currently not in use
open issue: is the integer argument required
   to be unique for each typ var? -}
toHCType (VType t :: Token
t) = Id -> RawKind -> Int -> Type
TypeName (String -> Id
stringToId (String -> Id) -> String -> Id
forall a b. (a -> b) -> a -> b
$ Token -> String
forall a. Show a => a -> String
show Token
t) (() -> RawKind
forall a. a -> AnyKind a
ClassKind ()) (-1)
toHCType (ParType t :: Type
t) = Type -> Type
toHCType Type
t