{- |
Module      :  ./HasCASL/Builtin.hs
Description :  builtin types and functions
Copyright   :  (c) Christian Maeder and Uni Bremen 2003
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  portable

HasCASL's builtin types and functions
-}

module HasCASL.Builtin
    ( cpoMap
    , bList
    , bTypes
    , bOps
    , preEnv
    , addBuiltins
    , aTypeArg
    , bTypeArg
    , cTypeArg
    , aType
    , bType
    , cType
    , botId
    , whenElse
    , ifThenElse
    , defId
    , eqId
    , exEq
    , falseId
    , trueId
    , notId
    , negId
    , andId
    , orId
    , logId
    , predTypeId
    , implId
    , infixIf
    , eqvId
    , resId
    , resType
    , botType
    , whenType
    , defType
    , eqType
    , notType
    , logType
    , mkQualOp
    , mkEqTerm
    , mkLogTerm
    , toBinJunctor
    , mkTerm
    , mkTermInst
    , unitTerm
    , unitTypeScheme
    ) where

import Common.Id
import Common.Keywords
import Common.GlobalAnnotations
import Common.AS_Annotation
import Common.AnnoParser
import Common.AnalyseAnnos
import Common.Result
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.Rel as Rel

import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Le

import Text.ParserCombinators.Parsec

-- * buitln identifiers

trueId :: Id
trueId :: Id
trueId = [Token] -> Id
mkId [String -> Token
mkSimpleId String
trueS]

falseId :: Id
falseId :: Id
falseId = [Token] -> Id
mkId [String -> Token
mkSimpleId String
falseS]

ifThenElse :: Id
ifThenElse :: Id
ifThenElse = [Token] -> Id
mkId ((String -> Token) -> [String] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map String -> Token
mkSimpleId [String
ifS, String
place, String
thenS, String
place, String
elseS, String
place])

whenElse :: Id
whenElse :: Id
whenElse = [Token] -> Id
mkId ((String -> Token) -> [String] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map String -> Token
mkSimpleId [String
place, String
whenS, String
place, String
elseS, String
place])

infixIf :: Id
infixIf :: Id
infixIf = String -> Id
mkInfix String
ifS

andId :: Id
andId :: Id
andId = String -> Id
mkInfix String
lAnd

orId :: Id
orId :: Id
orId = String -> Id
mkInfix String
lOr

implId :: Id
implId :: Id
implId = String -> Id
mkInfix String
implS

eqvId :: Id
eqvId :: Id
eqvId = String -> Id
mkInfix String
equivS

resId :: Id
resId :: Id
resId = String -> Id
mkInfix "res"

{-
    make these prefix identifier to allow "not def x" to be recognized
    as "not (def x)" by giving def__ higher precedence then not__.
    Simple identifiers usually have higher precedence then ____,
    otherwise "def x" would be rejected. But with simple identifiers
    "not def x" would be parsed as "(not def) x" because ____ is left
    associative.
-}

defId :: Id
defId :: Id
defId = [Token] -> Id
mkId [String -> Token
mkSimpleId String
defS, Token
placeTok]

notId :: Id
notId :: Id
notId = [Token] -> Id
mkId [String -> Token
mkSimpleId String
notS, Token
placeTok]

negId :: Id
negId :: Id
negId = [Token] -> Id
mkId [String -> Token
mkSimpleId String
negS, Token
placeTok]

builtinRelIds :: Set.Set Id
builtinRelIds :: Set Id
builtinRelIds = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id
typeId, Id
eqId, Id
exEq, Id
defId]

builtinLogIds :: Set.Set Id
builtinLogIds :: Set Id
builtinLogIds = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id
andId, Id
eqvId, Id
implId, Id
orId, Id
infixIf, Id
notId]

-- | add builtin identifiers
addBuiltins :: GlobalAnnos -> GlobalAnnos
addBuiltins :: GlobalAnnos -> GlobalAnnos
addBuiltins ga :: GlobalAnnos
ga =
    let ass :: AssocMap
ass = GlobalAnnos -> AssocMap
assoc_annos GlobalAnnos
ga
        newAss :: AssocMap
newAss = AssocMap -> AssocMap -> AssocMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union AssocMap
ass (AssocMap -> AssocMap) -> AssocMap -> AssocMap
forall a b. (a -> b) -> a -> b
$ [(Id, AssocEither)] -> AssocMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                 [(Id
applId, AssocEither
ALeft), (Id
andId, AssocEither
ALeft), (Id
orId, AssocEither
ALeft),
                  (Id
implId, AssocEither
ARight), (Id
infixIf, AssocEither
ALeft),
                  (Id
whenElse, AssocEither
ARight)]
        precs :: PrecedenceGraph
precs = GlobalAnnos -> PrecedenceGraph
prec_annos GlobalAnnos
ga
        pMap :: Map Id (Set Id)
pMap = PrecedenceGraph -> Map Id (Set Id)
forall a. Rel a -> Map a (Set a)
Rel.toMap PrecedenceGraph
precs
        opIds :: Set Id
opIds = [Set Id] -> Set Id
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (Map Id (Set Id) -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Map Id (Set Id)
pMap Set Id -> [Set Id] -> [Set Id]
forall a. a -> [a] -> [a]
: Map Id (Set Id) -> [Set Id]
forall k a. Map k a -> [a]
Map.elems Map Id (Set Id)
pMap)
        opIs :: [Id]
opIs = Set Id -> [Id]
forall a. Set a -> [a]
Set.toList
               ((((Id -> Bool) -> Set Id -> Set Id
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ i :: Id
i -> Id -> Bool
begPlace Id
i Bool -> Bool -> Bool
|| Id -> Bool
endPlace Id
i) Set Id
opIds
                Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Id
builtinRelIds) Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Id
builtinLogIds)
                Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id
applId, Id
whenElse])
        logs :: [(Id, Id)]
logs = [(Id
eqvId, Id
implId), (Id
implId, Id
andId), (Id
implId, Id
orId),
                (Id
eqvId, Id
infixIf), (Id
infixIf, Id
andId), (Id
infixIf, Id
orId),
                 (Id
andId, Id
notId), (Id
orId, Id
notId),
                (Id
andId, Id
negId), (Id
orId, Id
negId)]
        rels1 :: [(Id, Id)]
rels1 = (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> (Id
notId, Id
i)) ([Id] -> [(Id, Id)]) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
builtinRelIds
        rels1b :: [(Id, Id)]
rels1b = (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> (Id
negId, Id
i)) ([Id] -> [(Id, Id)]) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
builtinRelIds
        rels2 :: [(Id, Id)]
rels2 = (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> (Id
i, Id
whenElse)) ([Id] -> [(Id, Id)]) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList Set Id
builtinRelIds
        ops1 :: [(Id, Id)]
ops1 = (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> (Id
whenElse, Id
i)) (Id
applId Id -> [Id] -> [Id]
forall a. a -> [a] -> [a]
: [Id]
opIs)
        ops2 :: [(Id, Id)]
ops2 = (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: Id
i -> (Id
i, Id
applId)) [Id]
opIs
        newPrecs :: PrecedenceGraph
newPrecs = (PrecedenceGraph -> (Id, Id) -> PrecedenceGraph)
-> PrecedenceGraph -> [(Id, Id)] -> PrecedenceGraph
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ p :: PrecedenceGraph
p (a :: Id
a, b :: Id
b) -> if Id -> Id -> PrecedenceGraph -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.path Id
b Id
a PrecedenceGraph
p then PrecedenceGraph
p else
                         Id -> Id -> PrecedenceGraph -> PrecedenceGraph
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertDiffPair Id
a Id
b PrecedenceGraph
p) PrecedenceGraph
precs ([(Id, Id)] -> PrecedenceGraph) -> [(Id, Id)] -> PrecedenceGraph
forall a b. (a -> b) -> a -> b
$
                   [[(Id, Id)]] -> [(Id, Id)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Id, Id)]
logs, [(Id, Id)]
rels1, [(Id, Id)]
rels1b, [(Id, Id)]
rels2, [(Id, Id)]
ops1, [(Id, Id)]
ops2]
    in case GlobalAnnos -> [Annotation] -> Result GlobalAnnos
addGlobalAnnos GlobalAnnos
ga { assoc_annos :: AssocMap
assoc_annos = AssocMap
newAss
          , prec_annos :: PrecedenceGraph
prec_annos = PrecedenceGraph -> PrecedenceGraph
forall a. Ord a => Rel a -> Rel a
Rel.transClosure PrecedenceGraph
newPrecs } ([Annotation] -> Result GlobalAnnos)
-> [Annotation] -> Result GlobalAnnos
forall a b. (a -> b) -> a -> b
$
            (String -> Annotation) -> [String] -> [Annotation]
forall a b. (a -> b) -> [a] -> [b]
map String -> Annotation
parseDAnno [String]
displayStrings of
         Result _ (Just newGa :: GlobalAnnos
newGa) -> GlobalAnnos
newGa
         _ -> String -> GlobalAnnos
forall a. HasCallStack => String -> a
error "addBuiltins"

displayStrings :: [String]
displayStrings :: [String]
displayStrings =
  [ "%display __\\/__ %LATEX __\\vee__"
  , "%display __/\\__ %LATEX __\\wedge__"
  , "%display __=>__ %LATEX __\\Rightarrow__"
  , "%display __<=>__ %LATEX __\\Leftrightarrow__"
  , "%display not__ %LATEX \\neg__"
  ]

parseDAnno :: String -> Annotation
parseDAnno :: String -> Annotation
parseDAnno str :: String
str = case Parsec String () Annotation
-> String -> String -> Either ParseError Annotation
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () Annotation
forall st. GenParser Char st Annotation
annotationL "" String
str of
    Left _ -> String -> Annotation
forall a. HasCallStack => String -> a
error "parseDAnno"
    Right a :: Annotation
a -> Annotation
a

aVar :: Id
aVar :: Id
aVar = String -> Id
stringToId "a"

bVar :: Id
bVar :: Id
bVar = String -> Id
stringToId "b"

cVar :: Id
cVar :: Id
cVar = String -> Id
stringToId "c"

aType :: Type
aType :: Type
aType = TypeArg -> Type
typeArgToType TypeArg
aTypeArg

bType :: Type
bType :: Type
bType = TypeArg -> Type
typeArgToType TypeArg
bTypeArg

cType :: Type
cType :: Type
cType = TypeArg -> Type
typeArgToType TypeArg
cTypeArg

lazyAType :: Type
lazyAType :: Type
lazyAType = Type -> Type
mkLazyType Type
aType

varToTypeArgK :: Id -> Int -> Variance -> Kind -> TypeArg
varToTypeArgK :: Id -> Int -> Variance -> Kind -> TypeArg
varToTypeArgK i :: Id
i n :: Int
n v :: Variance
v k :: Kind
k = Id
-> Variance
-> VarKind
-> RawKind
-> Int
-> SeparatorKind
-> Range
-> TypeArg
TypeArg Id
i Variance
v (Kind -> VarKind
VarKind Kind
k) (Kind -> RawKind
toRaw Kind
k) Int
n SeparatorKind
Other Range
nullRange

varToTypeArg :: Id -> Int -> Variance -> TypeArg
varToTypeArg :: Id -> Int -> Variance -> TypeArg
varToTypeArg i :: Id
i n :: Int
n v :: Variance
v = Id -> Int -> Variance -> Kind -> TypeArg
varToTypeArgK Id
i Int
n Variance
v Kind
universe

mkATypeArg :: Variance -> TypeArg
mkATypeArg :: Variance -> TypeArg
mkATypeArg = Id -> Int -> Variance -> TypeArg
varToTypeArg Id
aVar (-1)

aTypeArg :: TypeArg
aTypeArg :: TypeArg
aTypeArg = Variance -> TypeArg
mkATypeArg Variance
NonVar

aTypeArgK :: Kind -> TypeArg
aTypeArgK :: Kind -> TypeArg
aTypeArgK = Id -> Int -> Variance -> Kind -> TypeArg
varToTypeArgK Id
aVar (-1) Variance
NonVar

bTypeArg :: TypeArg
bTypeArg :: TypeArg
bTypeArg = Id -> Int -> Variance -> TypeArg
varToTypeArg Id
bVar (-2) Variance
NonVar

cTypeArg :: TypeArg
cTypeArg :: TypeArg
cTypeArg = Id -> Int -> Variance -> TypeArg
varToTypeArg Id
cVar (-3) Variance
NonVar

bindVarA :: TypeArg -> Type -> TypeScheme
bindVarA :: TypeArg -> Type -> TypeScheme
bindVarA a :: TypeArg
a t :: Type
t = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg
a] Type
t Range
nullRange

bindA :: Type -> TypeScheme
bindA :: Type -> TypeScheme
bindA = TypeArg -> Type -> TypeScheme
bindVarA TypeArg
aTypeArg

resType :: TypeScheme
resType :: TypeScheme
resType = [TypeArg] -> Type -> Range -> TypeScheme
TypeScheme [TypeArg
aTypeArg, TypeArg
bTypeArg]
    (Type -> Arrow -> Type -> Type
mkFunArrType ([Type] -> Type
mkProductType [Type
lazyAType, Type -> Type
mkLazyType Type
bType]) Arrow
FunArr Type
aType)
    Range
nullRange

lazyLog :: Type
lazyLog :: Type
lazyLog = Type -> Type
mkLazyType Type
unitType

aPredType :: Type
aPredType :: Type
aPredType = TypeArg -> Type -> Range -> Type
TypeAbs (Variance -> TypeArg
mkATypeArg Variance
ContraVar)
    (Type -> Arrow -> Type -> Type
mkFunArrType Type
aType Arrow
PFunArr Type
unitType) Range
nullRange

eqType :: TypeScheme
eqType :: TypeScheme
eqType = Type -> TypeScheme
bindA (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Arrow -> Type -> Type
mkFunArrType ([Type] -> Type
mkProductType [Type
lazyAType, Type
lazyAType])
    Arrow
PFunArr Type
unitType

logType :: TypeScheme
logType :: TypeScheme
logType = Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Arrow -> Type -> Type
mkFunArrType
    ([Type] -> Type
mkProductType [Type
lazyLog, Type
lazyLog]) Arrow
PFunArr Type
unitType

notType :: TypeScheme
notType :: TypeScheme
notType = Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Arrow -> Type -> Type
mkFunArrType Type
lazyLog Arrow
PFunArr Type
unitType

whenType :: TypeScheme
whenType :: TypeScheme
whenType = Type -> TypeScheme
bindA (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Arrow -> Type -> Type
mkFunArrType
    ([Type] -> Type
mkProductType [Type
lazyAType, Type
lazyLog, Type
lazyAType]) Arrow
PFunArr Type
aType

unitTypeScheme :: TypeScheme
unitTypeScheme :: TypeScheme
unitTypeScheme = Type -> TypeScheme
simpleTypeScheme Type
lazyLog

botId :: Id
botId :: Id
botId = [Token] -> Id
mkId [String -> Token
mkSimpleId "bottom"]

predTypeId :: Id
predTypeId :: Id
predTypeId = [Token] -> Id
mkId [String -> Token
mkSimpleId "Pred"]

logId :: Id
logId :: Id
logId = [Token] -> Id
mkId [String -> Token
mkSimpleId "Logical"]

botType :: TypeScheme
botType :: TypeScheme
botType = let a :: TypeArg
a = Kind -> TypeArg
aTypeArgK Kind
cppoCl in TypeArg -> Type -> TypeScheme
bindVarA TypeArg
a (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkLazyType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TypeArg -> Type
typeArgToType TypeArg
a

defType :: TypeScheme
defType :: TypeScheme
defType = Type -> TypeScheme
bindA (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Type -> Arrow -> Type -> Type
mkFunArrType Type
lazyAType Arrow
PFunArr Type
unitType

-- | builtin functions
bList :: [(Id, TypeScheme)]
bList :: [(Id, TypeScheme)]
bList = (Id
botId, TypeScheme
botType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
: (Id
defId, TypeScheme
defType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
: (Id
notId, TypeScheme
notType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
:
        (Id
negId, TypeScheme
notType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
: (Id
whenElse, TypeScheme
whenType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
:
        (Id
trueId, TypeScheme
unitTypeScheme) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
: (Id
falseId, TypeScheme
unitTypeScheme) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
:
        (Id
eqId, TypeScheme
eqType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
: (Id
exEq, TypeScheme
eqType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
: (Id
resId, TypeScheme
resType) (Id, TypeScheme) -> [(Id, TypeScheme)] -> [(Id, TypeScheme)]
forall a. a -> [a] -> [a]
:
        (Id -> (Id, TypeScheme)) -> [Id] -> [(Id, TypeScheme)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: Id
o -> (Id
o, TypeScheme
logType)) [Id
andId, Id
orId, Id
eqvId, Id
implId, Id
infixIf]

mkTypesEntry :: Id -> Kind -> [Kind] -> [Id] -> TypeDefn -> (Id, TypeInfo)
mkTypesEntry :: Id -> Kind -> [Kind] -> [Id] -> TypeDefn -> (Id, TypeInfo)
mkTypesEntry i :: Id
i k :: Kind
k cs :: [Kind]
cs s :: [Id]
s d :: TypeDefn
d =
  (Id
i, RawKind -> Set Kind -> Set Id -> TypeDefn -> TypeInfo
TypeInfo (Kind -> RawKind
toRaw Kind
k) ([Kind] -> Set Kind
forall a. Ord a => [a] -> Set a
Set.fromList [Kind]
cs) ([Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id]
s) TypeDefn
d)

funEntry :: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry :: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry a :: Arrow
a s :: [Arrow]
s cs :: [Kind]
cs =
  Id -> Kind -> [Kind] -> [Id] -> TypeDefn -> (Id, TypeInfo)
mkTypesEntry (Arrow -> Id
arrowId Arrow
a) Kind
funKind (Kind
funKind Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: [Kind]
cs) ((Arrow -> Id) -> [Arrow] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Arrow -> Id
arrowId [Arrow]
s) TypeDefn
NoTypeDefn

mkEntry :: Id -> Kind -> [Kind] -> TypeDefn -> (Id, TypeInfo)
mkEntry :: Id -> Kind -> [Kind] -> TypeDefn -> (Id, TypeInfo)
mkEntry i :: Id
i k :: Kind
k cs :: [Kind]
cs = Id -> Kind -> [Kind] -> [Id] -> TypeDefn -> (Id, TypeInfo)
mkTypesEntry Id
i Kind
k [Kind]
cs []

pEntry :: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry :: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry i :: Id
i k :: Kind
k = Id -> Kind -> [Kind] -> TypeDefn -> (Id, TypeInfo)
mkEntry Id
i Kind
k [Kind
k]

-- | builtin data type map
bTypes :: TypeMap
bTypes :: TypeMap
bTypes = [(Id, TypeInfo)] -> TypeMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, TypeInfo)] -> TypeMap) -> [(Id, TypeInfo)] -> TypeMap
forall a b. (a -> b) -> a -> b
$ Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry Arrow
PFunArr [] []
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry Arrow
FunArr [Arrow
PFunArr] []
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry Arrow
PContFunArr [Arrow
PFunArr] [Kind -> Kind -> Kind -> Kind
funKind3 Kind
cpoCl Kind
cpoCl Kind
cppoCl]
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Arrow -> [Arrow] -> [Kind] -> (Id, TypeInfo)
funEntry Arrow
ContFunArr [Arrow
PContFunArr, Arrow
FunArr]
        [Kind -> Kind -> Kind -> Kind
funKind3 Kind
cpoCl Kind
cpoCl Kind
cpoCl, Kind -> Kind -> Kind -> Kind
funKind3 Kind
cpoCl Kind
cppoCl Kind
cppoCl]
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry Id
unitTypeId Kind
cppoCl TypeDefn
NoTypeDefn
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry Id
predTypeId (Variance -> Kind -> Kind -> Range -> Kind
forall a. Variance -> AnyKind a -> AnyKind a -> Range -> AnyKind a
FunKind Variance
ContraVar Kind
universe Kind
universe Range
nullRange)
        (Type -> TypeDefn
AliasTypeDefn Type
aPredType)
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry Id
lazyTypeId Kind
coKind TypeDefn
NoTypeDefn
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: Id -> Kind -> TypeDefn -> (Id, TypeInfo)
pEntry Id
logId Kind
universe (Type -> TypeDefn
AliasTypeDefn (Type -> TypeDefn) -> Type -> TypeDefn
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkLazyType Type
unitType)
    (Id, TypeInfo) -> [(Id, TypeInfo)] -> [(Id, TypeInfo)]
forall a. a -> [a] -> [a]
: (Int -> (Id, TypeInfo)) -> [Int] -> [(Id, TypeInfo)]
forall a b. (a -> b) -> [a] -> [b]
map (\ n :: Int
n -> let k :: Kind
k = Int -> Range -> Kind
prodKind Int
n Range
nullRange in
            Id -> Kind -> [Kind] -> TypeDefn -> (Id, TypeInfo)
mkEntry (Int -> Range -> Id
productId Int
n Range
nullRange) Kind
k
              (Kind
k Kind -> [Kind] -> [Kind]
forall a. a -> [a] -> [a]
: (Kind -> Kind) -> [Kind] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Range -> Kind -> Kind
prodKind1 Int
n Range
nullRange) [Kind
cpoCl, Kind
cppoCl]) TypeDefn
NoTypeDefn)
          [2 .. 5]

cpoId :: Id
cpoId :: Id
cpoId = String -> Id
stringToId "Cpo"

cpoCl :: Kind
cpoCl :: Kind
cpoCl = Id -> Kind
forall a. a -> AnyKind a
ClassKind Id
cpoId

cppoId :: Id
cppoId :: Id
cppoId = String -> Id
stringToId "Cppo"

cppoCl :: Kind
cppoCl :: Kind
cppoCl = Id -> Kind
forall a. a -> AnyKind a
ClassKind Id
cppoId

-- | builtin class map
cpoMap :: ClassMap
cpoMap :: ClassMap
cpoMap = [(Id, ClassInfo)] -> ClassMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [ (Id
cpoId, RawKind -> Set Kind -> ClassInfo
ClassInfo RawKind
rStar (Set Kind -> ClassInfo) -> Set Kind -> ClassInfo
forall a b. (a -> b) -> a -> b
$ Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
universe)
  , (Id
cppoId, RawKind -> Set Kind -> ClassInfo
ClassInfo RawKind
rStar (Set Kind -> ClassInfo) -> Set Kind -> ClassInfo
forall a b. (a -> b) -> a -> b
$ Kind -> Set Kind
forall a. a -> Set a
Set.singleton Kind
cpoCl)]

-- | builtin function map
bOps :: Assumps
bOps :: Assumps
bOps = [(Id, Set OpInfo)] -> Assumps
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Set OpInfo)] -> Assumps) -> [(Id, Set OpInfo)] -> Assumps
forall a b. (a -> b) -> a -> b
$ ((Id, TypeScheme) -> (Id, Set OpInfo))
-> [(Id, TypeScheme)] -> [(Id, Set OpInfo)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: Id
i, sc :: TypeScheme
sc) ->
    (Id
i, OpInfo -> Set OpInfo
forall a. a -> Set a
Set.singleton (OpInfo -> Set OpInfo) -> OpInfo -> Set OpInfo
forall a b. (a -> b) -> a -> b
$ TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo TypeScheme
sc Set OpAttr
forall a. Set a
Set.empty (OpDefn -> OpInfo) -> OpDefn -> OpInfo
forall a b. (a -> b) -> a -> b
$ OpBrand -> OpDefn
NoOpDefn OpBrand
Fun)) [(Id, TypeScheme)]
bList

-- | environment with predefined names
preEnv :: Env
preEnv :: Env
preEnv = Env
initialEnv { classMap :: ClassMap
classMap = ClassMap
cpoMap, typeMap :: TypeMap
typeMap = TypeMap
bTypes, assumps :: Assumps
assumps = Assumps
bOps }

mkQualOpInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOpInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOpInst k :: InstKind
k i :: Id
i sc :: TypeScheme
sc tys :: [Type]
tys ps :: Range
ps = OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Fun (Id -> [TypeArg] -> Range -> PolyId
PolyId Id
i [] Range
ps) TypeScheme
sc [Type]
tys InstKind
k Range
ps

mkQualOp :: Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp :: Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp = InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOpInst InstKind
Infer

mkTermInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTermInst :: InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTermInst k :: InstKind
k i :: Id
i sc :: TypeScheme
sc tys :: [Type]
tys ps :: Range
ps t :: Term
t = Term -> Term -> Range -> Term
ApplTerm (InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOpInst InstKind
k Id
i TypeScheme
sc [Type]
tys Range
ps) Term
t Range
ps

mkTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm = InstKind -> Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTermInst InstKind
Infer

mkBinTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term -> Term
mkBinTerm :: Id -> TypeScheme -> [Type] -> Range -> Term -> Term -> Term
mkBinTerm i :: Id
i sc :: TypeScheme
sc tys :: [Type]
tys ps :: Range
ps t1 :: Term
t1 t2 :: Term
t2 = Id -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm Id
i TypeScheme
sc [Type]
tys Range
ps (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
TupleTerm [Term
t1, Term
t2] Range
ps

mkLogTerm :: Id -> Range -> Term -> Term -> Term
mkLogTerm :: Id -> Range -> Term -> Term -> Term
mkLogTerm i :: Id
i = Id -> TypeScheme -> [Type] -> Range -> Term -> Term -> Term
mkBinTerm Id
i TypeScheme
logType []

mkEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm :: Id -> Type -> Range -> Term -> Term -> Term
mkEqTerm i :: Id
i ty :: Type
ty = Id -> TypeScheme -> [Type] -> Range -> Term -> Term -> Term
mkBinTerm Id
i TypeScheme
eqType [Type
ty]

unitTerm :: Id -> Range -> Term
unitTerm :: Id -> Range -> Term
unitTerm i :: Id
i = Id -> TypeScheme -> [Type] -> Range -> Term
mkQualOp Id
i TypeScheme
unitTypeScheme []

toBinJunctor :: Id -> [Term] -> Range -> Term
toBinJunctor :: Id -> [Term] -> Range -> Term
toBinJunctor i :: Id
i ts :: [Term]
ts ps :: Range
ps = case [Term]
ts of
    [] -> String -> Term
forall a. HasCallStack => String -> a
error "toBinJunctor"
    [t :: Term
t] -> Term
t
    t :: Term
t : rs :: [Term]
rs -> Id -> Range -> Term -> Term -> Term
mkLogTerm Id
i Range
ps Term
t (Id -> [Term] -> Range -> Term
toBinJunctor Id
i [Term]
rs Range
ps)