AsToLe.hs revision 4b0a4c7dea0f67a233dcc42ce9bb18d36de109ae
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederLicence : All rights reserved.
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederMaintainer : hets@tzi.de
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederStability : experimental
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederPortability : portable
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder conversion from As to Le
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport qualified Common.Lib.Set as Set
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder----------------------------------------------------------------------------
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermissingAna :: PrettyPrint a => a -> [Pos] -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian 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 :: GlobalAnnos -> BasicSpec -> State Env ()
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederanaBasicSpec ga (BasicSpec l) = mapM_ (anaBasicItem ga) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem :: GlobalAnnos -> BasicItem -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem ga (SigItems i) = anaSigItems ga Loose i
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem ga (ClassItems inst l _) = mapM_ (anaAnnotedClassItem ga inst) l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem _ (GenVarItems l _) = mapM_ anaGenVarDecl l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem ga (ProgItems l _) = mapM_ (anaProgEq ga) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem _ (FreeDatatype l _) = mapM_ (anaDatatype Free Plain) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaBasicItem ga (GenItems l _) = mapM_ (anaSigItems ga Generated) $ map item l
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian MaederanaBasicItem ga (AxiomItems decls fs _) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do tm <- gets typeMap -- save type map
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder as <- gets assumps -- save vars
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mapM_ anaGenVarDecl decls
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder ds <- mapM (( \ (TermFormula t) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder resolveTerm ga logicalType t ) . item) fs
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder putTypeMap tm -- restore
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder putAssumps as -- restore
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder appendDiags $ concatMap diags ds
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let sens = concat $ zipWith ( \ r f ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case maybeResult r of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just t -> [NamedSen (getRLabel f) $ TermFormula t]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> [] ) ds fs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder appendSentences sens
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederappendSentences :: [Named Formula] -> State Env ()
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederappendSentences fs =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null fs then return () else
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder put $ e {sentences = sentences e ++ fs}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaSigItems :: GlobalAnnos -> GenKind -> SigItems -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaSigItems _ gk (TypeItems inst l _) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mapM_ (anaTypeItem gk inst) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaSigItems ga _ (OpItems l _) = mapM_ (anaOpItem ga) $ map item l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaGenVarDecl :: GenVarDecl -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaGenVarDecl(GenVarDecl v) = optAnaVarDecl v
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaGenVarDecl(GenTypeVarDecl t) = anaTypeVarDecl t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederconvertTypeToClass :: Type -> ReadR ClassMap Class
36c6cc568751e4235502cfee00ba7b597dae78dcChristian 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) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just _ -> Result [] (Just $ Intersection
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> Result
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [mkDiag Hint "not a class" ci] Nothing )
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ anaClassId ci
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToClass (BracketType Parens ts ps) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do cs <- mapM convertTypeToClass ts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian 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
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederconvertTypeToKind (FunType t1 FunArr t2 ps) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do k1 <- convertTypeToKind t1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder k2 <- convertTypeToKind t2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ KindAppl k1 k2 ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToKind (BracketType Parens [t] _) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do k <- convertTypeToKind t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederconvertTypeToKind (MixfixType [t1, TypeToken t]) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let s = tokStr t
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder v = case s of
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder "-" -> ContraVar
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder InVar -> lift $ Result [] Nothing
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder _ -> do k1 <- convertTypeToClass t1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ ExtClass k1 v [tokPos t]
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederconvertTypeToKind t =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do c <- convertTypeToClass t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return $ ExtClass c InVar []
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederoptAnaVarDecl, anaVarDecl :: VarDecl -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederoptAnaVarDecl vd@(VarDecl v t s q) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if isSimpleId v then
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do mc <- toMaybeState classMap $ convertTypeToKind t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just c -> anaTypeVarDecl(TypeArg v c s q)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> anaVarDecl vd
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder else anaVarDecl vd
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian MaederanaVarDecl(VarDecl v oldT _ _) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do (k, t) <- anaTypeS (star, oldT)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder checkKindsS v star k
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder addOpId v (simpleTypeScheme t) [] VarDefn
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder-- ----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- ----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaAnnotedClassItem :: GlobalAnnos -> Instance -> Annoted ClassItem
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder -> State Env ()
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederanaAnnotedClassItem ga _ aci =
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder let ClassItem d l _ = item aci in
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do anaClassDecls d
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mapM_ (anaBasicItem ga) $ map item l
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- ----------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- ----------------------------------------------------------------------------
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian MaederanaProgEq :: GlobalAnnos -> ProgEq -> State Env ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederanaProgEq ga (ProgEq pat trm _) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do Result es mp <- resolvePattern ga pat
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder appendDiags es
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> return ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just (ty, newPat) -> do
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let bs = extractBindings newPat
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mapM_ anaVarDecl bs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Result ts mt <- resolveTerm ga ty trm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder appendDiags ts
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder Nothing -> return ()
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Just newTerm ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case removeResultType newPat of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder PatternConstr (InstOpId i _tys _) sc args ps ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder addOpId i sc [] $ Definition $
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null args then newTerm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else LambdaTerm args Partial newTerm ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> appendDiags $ [mkDiag Error
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder "no toplevel pattern" newPat]
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder where removeResultType p =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder TypedPattern tp _ _ ->