AsToLe.hs revision b56389e736838ac2fe7b105a8a2d0963a2374e99
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder Authors: Christian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Common.Lib.Set as Set
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder----------------------------------------------------------------------------
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-----------------------------------------------------------------------------
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederlogicalType :: Type
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederlogicalType = TypeName (simpleIdToId (mkSimpleId "logical")) star 0
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedermissingAna :: PrettyPrint a => a -> [Pos] -> State Env ()
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaedermissingAna t ps = appendDiags [Diag FatalError
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder ("no analysis yet for: " ++ showPretty t "")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ if null ps then nullPos else head ps]
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaBasicSpec :: BasicSpec -> State Env ()
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaBasicSpec (BasicSpec l) = mapM_ anaBasicItem $ map item l
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederanaBasicItem :: BasicItem -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem (SigItems i) = anaSigItems Loose i
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaederanaBasicItem (ClassItems inst l _) = mapM_ (anaAnnotedClassItem inst) l
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaederanaBasicItem (GenVarItems l _) = mapM_ anaGenVarDecl l
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederanaBasicItem t@(ProgItems _ p) = missingAna t p
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem (FreeDatatype l _) = mapM_ (anaDatatype Free Plain) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem (GenItems l _) = mapM_ (anaSigItems Generated) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem (AxiomItems decls fs _) =
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder do tm <- gets typeMap -- save type map
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder as <- gets assumps -- save vars
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder mapM_ anaGenVarDecl decls
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder ds <- mapM (( \ (TermFormula t) -> resolveTermWithType
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (Just logicalType) t ) . item) fs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder appendDiags $ concatMap diags ds
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder putTypeMap tm -- restore
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder putAssumps as -- restore
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- store the formulae
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaSigItems :: GenKind -> SigItems -> State Env ()
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederanaSigItems gk (TypeItems inst l _) = mapM_ (anaTypeItem gk inst) $ map item l
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederanaSigItems _ (OpItems l _) = mapM_ anaOpItem $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaSigItems _ l@(PredItems _ p) = missingAna l p
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaGenVarDecl :: GenVarDecl -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaGenVarDecl(GenVarDecl v) = optAnaVarDecl v
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaGenVarDecl(GenTypeVarDecl t) = anaTypeVarDecl t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToClass :: Type -> ReadR ClassMap Class
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToClass (TypeToken t) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if tokStr t == "Type" then return universe else do
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let ci = simpleIdToId t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mapReadR ( \ (Result _ m) ->
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just _ -> Result [] (Just $ Intersection
998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian Maeder Nothing -> Result
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder [mkDiag Hint "not a class" ci] Nothing )
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ anaClassId ci
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToClass (BracketType Parens ts ps) =
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder do cs <- mapM convertTypeToClass ts
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder return $ Intersection (Set.unions $ map iclass cs) ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToClass t = lift $ Result [mkDiag Hint "not a class" t] Nothing
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToKind :: Type -> ReadR ClassMap Kind
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToKind (FunType t1 FunArr t2 ps) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do k1 <- convertTypeToKind t1
81d182b21020b815887e9057959228546cf61b6bChristian Maeder k2 <- convertTypeToKind t2
f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder return $ KindAppl k1 k2 ps
cce6eaa31ad53bd212fb41d71a2df6aafb463067Christian MaederconvertTypeToKind (BracketType Parens [t] _) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do k <- convertTypeToKind t
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederconvertTypeToKind (MixfixType [t1, TypeToken t]) =
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder let s = tokStr t
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder v = case s of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder "-" -> ContraVar
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder InVar -> lift $ Result [] Nothing
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder _ -> do k1 <- convertTypeToClass t1
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return $ ExtClass k1 v [tokPos t]
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederconvertTypeToKind t =
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder do c <- convertTypeToClass t
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder return $ ExtClass c InVar []
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederoptAnaVarDecl, anaVarDecl :: VarDecl -> State Env ()
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederoptAnaVarDecl vd@(VarDecl v t s q) =
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder if isSimpleId v then
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder do mc <- toMaybeState classMap $ convertTypeToKind t
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder Just c -> anaTypeVarDecl(TypeArg v c s q)
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder Nothing -> anaVarDecl vd
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else anaVarDecl vd
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaederanaVarDecl(VarDecl v oldT _ _) =
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do (k, t) <- anaTypeS (star, oldT)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder checkKindsS v star k
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder addOpId v (simpleTypeScheme t) [] VarDefn
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder-- ----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- ----------------------------------------------------------------------------
6cb518d88084543c13aa7e56db767c14ee97ab77Christian MaederanaAnnotedClassItem :: Instance -> Annoted ClassItem -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaAnnotedClassItem _ aci =
61091743da1a9ed6dfd5e077fdcc972553358962Christian Maeder let ClassItem d l _ = item aci in
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do anaClassDecls d
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder mapM_ anaBasicItem $ map item l