OpDecl.hs revision dfa74d066ea0f00a70276aedecc624c6b3c86dea
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : maeder@tzi.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : experimental
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder analyse operation declarations
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaAttr :: GlobalAnnos -> TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
d17834302eaa101395b4b806cd73670fd864445fChristian MaederanaAttr ga (TypeScheme tvs ty _) (UnitOpAttr trm ps) =
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder do let mTy = case unalias ty of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder FunType arg _ t3 _ ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case unalias arg of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ProductType [t1, t2] _ -> Just (t1,t2,t3)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder tm <- gets typeMap
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder mapM_ (addTypeVarDecl False) tvs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> do addDiags [mkDiag Error
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder "unexpected type of operation" ty]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder mt <- resolveTerm ga Nothing trm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder putTypeMap tm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> return Nothing
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Just t -> return $ Just $ UnitOpAttr t ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Just (t1, t2, t3) ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder do if t1 == t2 && t2 == t3 then
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder else addDiags [mkDiag Error
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder "unexpected type components of operation" ty]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder mt <- resolveTerm ga (Just t3) trm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder putTypeMap tm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder case mt of Nothing -> return Nothing
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Just t -> return $ Just $ UnitOpAttr t ps
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaAttr _ _ b = return $ Just b
25612a7b3ce708909298d5426406592473880a20Christian MaederpatternsToType :: [[VarDecl]] -> Type -> Type
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian MaederpatternsToType [] t = t
c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian MaederpatternsToType (p: ps) t = FunType (tuplePatternToType p) PFunArr
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (patternsToType ps t) []
25612a7b3ce708909298d5426406592473880a20Christian MaedertuplePatternToType :: [VarDecl] -> Type
25612a7b3ce708909298d5426406592473880a20Christian MaedertuplePatternToType vds = mkProductType (map ( \ (VarDecl _ t _ _) -> t) vds) []
18b709ce961d68328da768318dcc70067f066d86Christian MaedergetUninstOpId :: TypeScheme -> OpId -> (OpId, TypeScheme)
18b709ce961d68328da768318dcc70067f066d86Christian MaedergetUninstOpId (TypeScheme tvs q ps) (OpId i args qs) =
18b709ce961d68328da768318dcc70067f066d86Christian Maeder (OpId i [] qs, TypeScheme (args ++ tvs) q ps)
18b709ce961d68328da768318dcc70067f066d86Christian MaederanaOpId :: GlobalAnnos -> OpBrand -> TypeScheme -> [OpAttr] -> OpId
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -> State Env (Maybe OpId)
18b709ce961d68328da768318dcc70067f066d86Christian MaederanaOpId ga br partSc attrs o =
18b709ce961d68328da768318dcc70067f066d86Christian Maeder do let (OpId i _ _, sc) = getUninstOpId partSc o
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mSc <- anaTypeScheme sc
18b709ce961d68328da768318dcc70067f066d86Christian Maeder Nothing -> return Nothing
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Just newSc -> do
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mAttrs <- mapM (anaAttr ga newSc) attrs
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mo <- addOpId i newSc (catMaybes mAttrs) $ NoOpDefn br
18b709ce961d68328da768318dcc70067f066d86Christian Maeder return $ fmap (const o) mo
9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederanaOpItem :: GlobalAnnos -> OpBrand -> OpItem -> State Env (Maybe OpItem)
18b709ce961d68328da768318dcc70067f066d86Christian MaederanaOpItem ga br (OpDecl is sc attr ps) = do
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder mus <- mapM (anaOpId ga br sc attr) is
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder let us = catMaybes mus
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder return $ if null us then Nothing else
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder Just $ OpDecl us sc attr ps
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederanaOpItem ga br (OpDefn o oldPats sc partial trm ps) =
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder do let (op@(OpId i _ _), TypeScheme tArgs scTy qs) =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder getUninstOpId sc o
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder checkUniqueVars $ concat oldPats
18b709ce961d68328da768318dcc70067f066d86Christian Maeder tm <- gets typeMap
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder ass <- gets assumps
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mArgs <- mapM anaTypeVarDecl tArgs
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder mPats <- mapM (mapM anaVarDecl) oldPats
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putAssumps ass
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder let newPats = map catMaybes mPats
18b709ce961d68328da768318dcc70067f066d86Christian Maeder monoPats = map (map makeMonomorph) newPats
18b709ce961d68328da768318dcc70067f066d86Christian Maeder pats = map (\ l -> mkTupleTerm (map QualVar l) []) monoPats
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder vs <- gets localVars
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder mapM (mapM addLocalVar) monoPats
18b709ce961d68328da768318dcc70067f066d86Christian Maeder let newArgs = catMaybes mArgs
18b709ce961d68328da768318dcc70067f066d86Christian Maeder mty <- anaStarType scTy
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Just ty -> do
3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder mt <- resolveTerm ga Nothing $ TypedTerm trm AsType ty ps
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder putTypeMap tm
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder newSc <- generalizeS $ TypeScheme newArgs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (patternsToType newPats ty) qs
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder Just lastTrm -> do
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let lamTrm = case (pats, partial) of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ([], Total) -> lastTrm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder _ -> LambdaTerm pats partial lastTrm ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ot = QualOp br (InstOpId i [] []) newSc []
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder lhs = mkApplTerm ot pats
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ef = mkEqTerm eqId ps lhs lastTrm
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder f = mkForall (map GenTypeVarDecl newArgs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ++ (map GenVarDecl $
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder concatMap extractVars pats)) ef
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder addOpId i newSc [] $ Definition br lamTrm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder appendSentences [NamedSen
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder ("def_" ++ showId i "")
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder True $ Formula f]
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder return $ Just $ OpDefn op [] newSc Total lamTrm ps
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder Nothing -> do
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder addOpId i newSc [] $ NoOpDefn br
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder return $ Just $ OpDecl [OpId i [] ps] newSc [] ps
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> do
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder resolveTerm ga Nothing trm -- get a view more diags
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder putTypeMap tm
9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder return Nothing
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder-- ----------------------------------------------------------------------------
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maeder-- ----------------------------------------------------------------------------
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaederanaProgEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaederanaProgEq ga pe@(ProgEq _ _ q) =
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder do mp <- resolveTerm ga Nothing (LetTerm Program [pe]
c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder (BracketTerm Parens [] q) q)
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder Just (LetTerm _ (newPrg@(ProgEq newPat _ _) : _) _ _) ->
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder case getAppl newPat of
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder Just (i, sc, _) -> do
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder addOpId i sc [] $ NoOpDefn Op
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder appendSentences [NamedSen ("pe_" ++ showId i "")
dfa74d066ea0f00a70276aedecc624c6b3c86deaChristian Maeder True $ ProgEqSen i sc newPrg]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if isLHS e newPat then return ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder else addDiags [mkDiag Warning
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder "illegal lhs pattern"
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return $ Just newPrg
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder Nothing -> do addDiags [mkDiag Error
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder "illegal toplevel pattern"
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder return Nothing
fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder _ -> return Nothing
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian MaedergetApplConstr :: Pattern -> (Pattern, [Pattern])
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian MaedergetApplConstr pat =
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder ApplTerm p1 p2 _ ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let (tp, args) = getApplConstr p1 in (tp, p2:args)
f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder TypedTerm tp _ _ _ -> getApplConstr tp
2f3c4316d3979a76918f0a93206b9dc75d46a1d4Christian Maeder _ -> (pat, [])