Copyright : (c) Christian Maeder and Uni Bremen 2003
HasCASL's builtin types and functions
trueId = mkId [mkSimpleId trueS]
falseId = mkId [mkSimpleId falseS]
ifThenElse = mkId (map mkSimpleId [ifS, place, thenS, place, elseS, place])
whenElse = mkId (map mkSimpleId [place, whenS, place, elseS, place])
mkInfix s = mkId $ map mkSimpleId [place, s, place]
defId = mkId $ map mkSimpleId [defS, place]
notId = mkId $ map mkSimpleId [notS, place]
negId = mkId $ map mkSimpleId [negS, place]
[andId, eqvId, implId, orId, infixIf, notId]
addBuiltins :: GlobalAnnos -> GlobalAnnos
[(applId, ALeft), (andId, ALeft), (orId, ALeft),
(implId, ARight), (infixIf, ALeft),
Set.\\ builtinRelIds) Set.\\ builtinLogIds)
logs = [(eqvId, implId), (implId, andId), (implId, orId),
(eqvId, infixIf), (infixIf, andId), (infixIf, orId),
(andId, notId), (orId, notId),
(andId, negId), (orId, negId)]
rels1 = map ( \ i -> (notId, i)) $
Set.toList builtinRelIds
rels1b = map ( \ i -> (negId, i)) $
Set.toList builtinRelIds
rels2 = map ( \ i -> (i, whenElse)) $
Set.toList builtinRelIds
ops1 = map ( \ i -> (whenElse, i)) (applId : opIs)
ops2 = map ( \ i -> (i, applId)) (whenElse : opIs)
newPrecs = foldr (\ (a, b) p -> if
Rel.member b a p then p else
concat [logs, rels1, rels1b, rels2, ops1, ops2]
in ga { assoc_annos = newAss
mkPrecIntMap ::
Rel.Rel Id -> PrecMap
m = foldr ( \ (n, s) m1 ->
aVar = simpleIdToId $ mkSimpleId "a"
aType = TypeName aVar star (-1)
bindA :: Type -> TypeScheme
bindA ty = TypeScheme [TypeArg aVar star Other []] ty []
lazyLog = LazyType logicalType []
eqType, logType, defType, notType, whenType, unitType :: TypeScheme
FunType (ProductType [aType, aType] [])
logType = simpleTypeScheme $
FunType (ProductType [lazyLog, lazyLog] [])
defType = bindA $ FunType aType PFunArr logicalType []
notType = simpleTypeScheme $ FunType lazyLog PFunArr logicalType []
FunType (ProductType [aType, lazyLog, aType] [])
unitType = simpleTypeScheme logicalType
botId = mkId [mkSimpleId "bottom"]
bList :: [(Id, TypeScheme)]
bList = (botId, botType) : (defId, defType) : (notId, notType) :
(negId, notType) : (whenElse, whenType) :
(trueId, unitType) : (falseId, unitType) :
(eqId, eqType) : (exEq, eqType) :
map ( \ o -> (o, logType)) [andId, orId, eqvId, implId, infixIf]
addUnit :: TypeMap -> TypeMap
addUnit tm = foldr ( \ (i, k, s, d) m ->
(TypeInfo k [k] s d) m) tm $
(unitTypeId, star, [], NoTypeDefn)
: (simpleIdToId $ mkSimpleId "Pred",
FunKind star star [], [], AliasTypeDefn defType)
: (simpleIdToId $ mkSimpleId "Logical",
star, [], AliasTypeDefn $ simpleTypeScheme $
FunType logicalType PFunArr logicalType [])
: (productId, prodKind, [], NoTypeDefn)
: map ( \ (a, l) -> (arrowId a, funKind,
map ( \ b -> TypeName (arrowId b) funKind 0) l,
[(PFunArr,[]), (FunArr, [PFunArr]), (PContFunArr, [PFunArr]),
(ContFunArr, [PContFunArr, FunArr])]
addOps :: Assumps -> Assumps
addOps as = foldr ( \ (i, sc) m ->
(OpInfos [OpInfo sc [] (NoOpDefn Fun)]) m) as bList
mkQualOp :: Id -> TypeScheme -> [Pos] -> Term
mkQualOp i sc ps = QualOp Fun (InstOpId i [] ps) sc ps
mkTerm :: Id -> TypeScheme -> [Pos] -> Term -> Term
mkTerm i sc ps t = ApplTerm (mkQualOp i sc ps) t ps
mkBinTerm :: Id -> TypeScheme -> [Pos] -> Term -> Term -> Term
mkBinTerm i sc ps t1 t2 = mkTerm i sc ps $ TupleTerm [t1, t2] ps
mkLogTerm :: Id -> [Pos] -> Term -> Term -> Term
mkLogTerm i ps = mkBinTerm i logType ps
mkEqTerm :: Id -> [Pos] -> Term -> Term -> Term
mkEqTerm i ps = mkBinTerm i eqType ps
unitTerm :: Id -> [Pos] -> Term
unitTerm i ps = mkQualOp i unitType ps
toBinJunctor :: Id -> [Term] -> [Pos] -> Term
toBinJunctor i ts ps = case ts of
[] -> error "toBinJunctor"