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
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"
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]
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
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]
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
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)]
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
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)