Builtin.hs revision 9d75ab580dbf51b7ca60903fb32e7f38d939d326
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiModule : $Header$
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiDescription : builtin types and functions
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiCopyright : (c) Christian Maeder and Uni Bremen 2003
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiMaintainer : Christian.Maeder@dfki.de
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiStability : experimental
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiPortability : portable
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiHasCASL's builtin types and functions
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiimport qualified Data.Map as Map
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport qualified Data.Set as Set
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport qualified Common.Lib.Rel as Rel
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- * buitln identifiers
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaitrueId :: Id
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaitrueId = mkId [mkSimpleId trueS]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchifalseId = mkId [mkSimpleId falseS]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiifThenElse :: Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiifThenElse = mkId (map mkSimpleId [ifS, place, thenS, place, elseS, place])
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiwhenElse :: Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiwhenElse = mkId (map mkSimpleId [place, whenS, place, elseS, place])
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiinfixIf = mkInfix ifS
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiandId = mkInfix lAnd
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiorId = mkInfix lOr
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiimplId = mkInfix implS
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchieqvId = mkInfix equivS
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi make these prefix identifier to allow "not def x" to be recognized
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi as "not (def x)" by giving def__ higher precedence then not__.
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Simple identifiers usually have higher precedence then ____,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi otherwise "def x" would be rejected. But with simple identifiers
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi "not def x" would be parsed as "(not def) x" because ____ is left
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchidefId = mkId [mkSimpleId defS, placeTok]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchinotId = mkId [mkSimpleId notS, placeTok]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchinegId = mkId [mkSimpleId negS, placeTok]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibuiltinRelIds :: Set.Set Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibuiltinRelIds = Set.fromList [typeId, eqId, exEq, defId]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibuiltinLogIds :: Set.Set Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi [andId, eqvId, implId, orId, infixIf, notId]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | add builtin identifiers
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaddBuiltins :: GlobalAnnos -> GlobalAnnos
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaddBuiltins ga =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi let ass = assoc_annos ga
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi [(applId, ALeft), (andId, ALeft), (orId, ALeft),
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (implId, ARight), (infixIf, ALeft),
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (whenElse, ARight)]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi precs = prec_annos ga
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi opIds = Set.unions (Map.keysSet pMap : Map.elems pMap)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi opIs = Set.toList ((((Set.filter isInfix opIds)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Set.\\ builtinRelIds) Set.\\ builtinLogIds)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Set.\\ Set.fromList [applId, whenElse])
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi logs = [(eqvId, implId), (implId, andId), (implId, orId),
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (eqvId, infixIf), (infixIf, andId), (infixIf, orId),
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (andId, notId), (orId, notId),
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (andId, negId), (orId, negId)]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi rels1 = map ( \ i -> (notId, i)) $ Set.toList builtinRelIds
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi rels1b = map ( \ i -> (negId, i)) $ Set.toList builtinRelIds
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi rels2 = map ( \ i -> (i, whenElse)) $ Set.toList builtinRelIds
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ops1 = map ( \ i -> (whenElse, i)) (applId : opIs)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ops2 = map ( \ i -> (i, applId)) opIs
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi newPrecs = foldl (\ p (a, b) -> if Rel.path b a p then p else
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi concat [logs, rels1, rels1b, rels2, ops1, ops2]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi in case addGlobalAnnos ga { assoc_annos = newAss
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , prec_annos = Rel.transClosure newPrecs } $
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi map parseDAnno displayStrings of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Result _ (Just newGa) -> newGa
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi _ -> error "addBuiltins"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchidisplayStrings :: [String]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchidisplayStrings =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi [ "%display __\\/__ %LATEX __\\vee__"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , "%display __/\\__ %LATEX __\\wedge__"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , "%display __=>__ %LATEX __\\Rightarrow__"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , "%display __<=>__ %LATEX __\\Leftrightarrow__"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , "%display not__ %LATEX \\neg__"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiparseDAnno :: String -> Annotation
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiparseDAnno str = case parse annotationL "" str of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Left _ -> error "parseDAnno"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaVar = simpleIdToId $ mkSimpleId "a"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaTypeWithKind :: Kind -> Type
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaTypeWithKind k = TypeName aVar (toRaw k) (-1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaType = aTypeWithKind universe
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilazyAType :: Type
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilazyAType = mkLazyType aType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaBindWithKind :: Variance -> Kind -> TypeArg
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaBindWithKind v k =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi TypeArg aVar v (VarKind k) (toRaw k) (-1) Other nullRange
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibindA :: Type -> TypeScheme
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibindA t = TypeScheme [aBindWithKind InVar universe] t nullRange
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilazyLog :: Type
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilazyLog = mkLazyType unitType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaPredType :: Type
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaPredType = TypeAbs (aBindWithKind ContraVar universe)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (mkFunArrType aType PFunArr unitType) nullRange
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchieqType, logType, notType, whenType, unitTypeScheme :: TypeScheme
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchieqType = bindA $ mkFunArrType (mkProductType [lazyAType, lazyAType])
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi PFunArr unitType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilogType = simpleTypeScheme $
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi mkFunArrType (mkProductType [lazyLog, lazyLog]) PFunArr unitType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchinotType = simpleTypeScheme $ mkFunArrType lazyLog PFunArr unitType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi bindA $ mkFunArrType (mkProductType [lazyAType, lazyLog, lazyAType])
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi PFunArr aType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiunitTypeScheme = simpleTypeScheme lazyLog
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibotId = mkId [mkSimpleId "g_bottom"]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchipredTypeId :: Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchipredTypeId = mkId [mkSimpleId "Pred"]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilogId = mkId [mkSimpleId "Logical"]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibotType :: TypeScheme
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibotType = bindA $ lazyAType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchidefType :: TypeScheme
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchidefType = bindA $ mkFunArrType lazyAType PFunArr unitType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibList :: [(Id, TypeScheme)]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchibList = (botId, botType) : (defId, defType) : (notId, notType) :
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (negId, notType) : (whenElse, whenType) :
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (trueId, unitTypeScheme) : (falseId, unitTypeScheme) :
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (eqId, eqType) : (exEq, eqType) :
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi map ( \ o -> (o, logType)) [andId, orId, eqvId, implId, infixIf]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchifunSupertypes :: [(Arrow, [Arrow])]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchifunSupertypes = [(PFunArr,[]), (FunArr, [PFunArr]), (PContFunArr, [PFunArr]),
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (ContFunArr, [PContFunArr, FunArr])]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaddUnit :: TypeMap -> TypeMap
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaddUnit tm = foldr ( \ (i, k, s, d) m ->
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Map.insertWith ( \ _ old -> old) i
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (TypeInfo (toRaw k) [k] (Set.fromList s) d) m) tm $
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (unitTypeId, universe, [], NoTypeDefn)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi : (predTypeId, FunKind ContraVar universe universe nullRange, [],
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi AliasTypeDefn aPredType)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi : (lazyTypeId, coKind, [], NoTypeDefn)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi : (logId, universe, [], AliasTypeDefn $ mkLazyType unitType)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi : map ( \ n -> (productId n , prodKind n, [], NoTypeDefn))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ++ map ( \ (a, l) -> (arrowId a, funKind,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi map ( \ b -> arrowId b) l,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi funSupertypes
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaddOps :: Assumps -> Assumps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiaddOps as = foldr ( \ (i, sc) m ->
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Map.insertWith ( \ _ old -> old) i
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (OpInfos [OpInfo sc [] (NoOpDefn Fun)]) m) as bList
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkQualOp :: Id -> TypeScheme -> Range -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkQualOp i sc ps = QualOp Fun i sc [] ps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkTerm :: Id -> TypeScheme -> Range -> Term -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkTerm i sc ps t = ApplTerm (mkQualOp i sc ps) t ps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkBinTerm :: Id -> TypeScheme -> Range -> Term -> Term -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkBinTerm i sc ps t1 t2 = mkTerm i sc ps $ TupleTerm [t1, t2] ps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkLogTerm :: Id -> Range -> Term -> Term -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkLogTerm i ps = mkBinTerm i logType ps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkEqTerm :: Id -> Range -> Term -> Term -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimkEqTerm i ps = mkBinTerm i eqType ps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiunitTerm :: Id -> Range -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiunitTerm i ps = mkQualOp i unitTypeScheme ps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitoBinJunctor :: Id -> [Term] -> Range -> Term
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitoBinJunctor i ts ps = case ts of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi [] -> error "toBinJunctor"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi t:rs -> mkLogTerm i ps t
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (toBinJunctor i rs ps)