OpDecl.hs revision c3f7e132e0c214b755c6c4b485f4748c4dd1595c
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder{- |
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : analyse operation declarations
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederStability : experimental
fbb66ee3e170624835b99f7aa91980753cb5b472Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederanalyse operation declarations
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder-}
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maedermodule HasCASL.OpDecl
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder ( anaOpItem
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder , anaProgEq
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder , mkEnvForall
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder ) where
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederimport Data.Maybe (catMaybes)
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederimport qualified Data.Set as Set
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport qualified Data.Map as Map
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Text.ParserCombinators.Parsec (parse, eof)
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport Control.Monad
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Id
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Lib.State as State
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Result
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.GlobalAnnotations
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederimport Common.AS_Annotation
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederimport Common.Doc
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport Common.Lexer ((<<), skip)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian Maederimport HasCASL.As
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport HasCASL.HToken
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian Maederimport HasCASL.TypeAna
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maederimport HasCASL.VarDecl
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport HasCASL.Le
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maederimport HasCASL.Builtin
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maederimport HasCASL.AsUtils
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskiimport HasCASL.MixAna
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maederimport HasCASL.TypeCheck
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport HasCASL.ProgEq
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport HasCASL.Unify
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskianaAttr :: TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederanaAttr (TypeScheme tvs ty _) b = case b of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder UnitOpAttr trm ps -> do
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder e <- get
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder let mTy = let (fty, fArgs) = getTypeAppl ty in case fArgs of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder [arg, t3] | lesserType e fty (toFunType PFunArr)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -> let (pty, ts) = getTypeAppl arg in case ts of
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder [t1, t2] | lesserType e pty (toProdType 2 ps)
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder -> Just (t1,t2,t3)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder _ -> Nothing
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder _ -> Nothing
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder let tm = typeMap e
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder mapM_ (addTypeVarDecl False) tvs
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder case mTy of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Nothing -> do addDiags [mkDiag Error
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder "unexpected type of operation" ty]
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder putTypeMap tm
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return Nothing
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder Just (t1, t2, t3) ->
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder do if t1 == t2 && t2 == t3 then return ()
c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder else addDiags [mkDiag Error
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian Maeder "unexpected type components of operation" ty]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder mt <- resolveTerm t3 trm
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder putTypeMap tm
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder case mt of Nothing -> return Nothing
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Just t -> return $ Just $ UnitOpAttr t ps
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder _ -> return $ Just b
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaedertuplePatternToType :: [VarDecl] -> Type
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedertuplePatternToType vds =
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder mkProductTypeWithRange (map ( \ (VarDecl _ t _ _) -> t) vds) $ getRange vds
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederanaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederanaOpId br sc attrs i@(PolyId j _ _) =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder do mSc <- anaPolyId i sc
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder case mSc of
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder Nothing -> return False
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Just newSc -> do
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder mAttrs <- mapM (anaAttr newSc) attrs
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder addOpId j newSc (Set.fromList $ catMaybes mAttrs) $ NoOpDefn br
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder-- | analyse an op-item
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederanaOpItem :: OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaederanaOpItem br oi = do
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder let Result ds (Just bs) = extractBinders $ l_annos oi ++ r_annos oi
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder addDiags ds
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder case item oi of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder OpDecl is sc attr ps -> do
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder case is of
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder [PolyId i _ _] -> mapM_ (addBinder i) bs
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder _ -> unless (null bs) $ addDiags
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder [mkDiag Warning "ignoring binder syntax" bs]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder ois <- mapM (anaOpId br sc attr) is
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder let us = map fst $ filter snd $ zip is ois
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder return $ replaceAnnoted (if null us then Nothing else
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Just $ OpDecl us sc attr ps) oi
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder OpDefn p@(PolyId i _ _) oldPats rsc@(TypeScheme tArgs scTy qs) trm ps
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder -> do
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder mapM_ (addBinder i) bs
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder checkUniqueVars $ concat oldPats
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder tvs <- gets localTypeVars
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder mArgs <- mapM anaddTypeVarDecl tArgs
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder mPats <- mapM (mapM anaVarDecl) oldPats
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder let newPats = map catMaybes mPats
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder monoPats = map (map makeMonomorph) newPats
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder pats = map (\ l -> mkTupleTerm (map QualVar l) nullRange) monoPats
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder vs <- gets localVars
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder mapM_ (mapM_ $ addLocalVar True) monoPats
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder let newArgs = catMaybes mArgs
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder mty <- anaStarType scTy
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder mtrm <- resolve trm
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder case (mty, mtrm) of
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder (Just rty, Just rTrm) -> do
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let (partial, ty) = case getTypeAppl rty of
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maeder (TypeName j _ _ , [lt]) | j == lazyTypeId -> (Partial, lt)
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maeder _ -> (Total, rty)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder monoty = monoType ty
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mt <- typeCheck monoty $ TypedTerm rTrm AsType monoty ps
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder e <- get
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder newSc <- generalizeS $ TypeScheme newArgs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (getFunType ty partial
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder $ map tuplePatternToType newPats) qs
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder putLocalVars vs
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder putLocalTypeVars tvs
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder case mt of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Just lastTrm0 -> do
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let lastTrm = case lastTrm0 of
d48085f765fca838c1d972d2123601997174583dChristian Maeder TypedTerm lTrm AsType rTy rs ->
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder case getTypeOf lTrm of
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder Just oTy | lesserType e oTy rTy ->
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if oTy == rTy then lTrm else
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder TypedTerm lTrm Inferred rTy rs
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder _ -> lastTrm0
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder _ -> lastTrm0
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder lamTrm = case (pats, partial) of
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder ([], Total) -> lastTrm
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder _ -> LambdaTerm pats partial lastTrm ps
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ot = QualOp br p newSc [] Infer
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder nullRange
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder lhs = mkApplTerm ot pats
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder ef = mkEqTerm eqId monoty ps lhs lastTrm
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder f = mkEnvForall e ef ps
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder addOpId i newSc Set.empty $ Definition br lamTrm
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder appendSentences
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder [(makeNamed (getRLabel oi) $ Formula f)
1738d16957389457347bee85075d3d33d002158fChristian Maeder { isDef = True }]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder return $ replaceAnnoted
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder (Just $ OpDefn p oldPats rsc rTrm ps) oi
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder Nothing -> do
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder addOpId i newSc Set.empty $ NoOpDefn br
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder return $ replaceAnnoted
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder (Just $ OpDecl [p] newSc [] ps) oi
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder _ -> do
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder putLocalVars vs
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder putLocalTypeVars tvs
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder return $ replaceAnnoted Nothing oi
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | analyse a program equation
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederanaProgEq :: Annoted ProgEq -> State Env (Maybe ProgEq)
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaederanaProgEq ape = do
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder let pe@(ProgEq _ _ q) = item ape
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian Maeder rp <- resolve (LetTerm Program [pe] (BracketTerm Parens [] q) q)
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder case rp of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Just t@(LetTerm _ (rpe@(ProgEq _ _ _) : _) _ _) -> do
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder mp <- typeCheck unitType t
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder ga <- State.gets globAnnos
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder case mp of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Just (LetTerm _ (newPrg@(ProgEq newPat _ _) : _) _ _) ->
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder case getAppl newPat of
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder Just (i, sc, _) -> do
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder addOpId i sc Set.empty $ NoOpDefn Op
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder appendSentences [(makeNamed ("pe_" ++ showId i "")
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $ ProgEqSen i sc newPrg)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder { isDef = True }]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder e <- get
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder if isLHS e newPat then return ()
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder else addDiags [mkNiceDiag ga Warning
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder "illegal lhs pattern"
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder newPat]
return $ Just rpe
Nothing -> do addDiags [mkNiceDiag ga Error
"illegal toplevel pattern"
newPat]
return Nothing
_ -> return Nothing
_ -> return Nothing
extractBinderId :: Annotation -> Result Id
extractBinderId a = case a of
Unparsed_anno (Annote_word f@"binder") s r ->
case parse (skip >> opId << eof) f $ fromAText s of
Right i -> return i
Left err -> fatal_error (showErr err ++ "\nin " ++ show (annoDoc a)) r
_ -> Result [] Nothing
extractBinders :: [Annotation] -> Result [Id]
extractBinders as =
let rs = map extractBinderId as
ds = concatMap diags rs
in if null ds then return $ catMaybes $ map maybeResult rs
else Result ds $ Just []
addBinding :: Id -> Id -> State.State Env ()
addBinding o b = do
addDiags $ getBinderDiags o b
State.modify $ \ e -> e { binders = Map.insert b o $ binders e }
e <- State.get
let ga = globAnnos e
aa = assoc_annos ga
when (isInfix b && not (Map.member b aa)) $
State.put e { globAnnos = ga { assoc_annos = Map.insert b ARight aa }}
getBinderDiags :: Id -> Id -> [Diagnosis]
getBinderDiags o b =
let c = placeCount b
d = placeCount o + 1
str = "expected " ++ show (max 2 d) ++ " places in binder"
in if c < 2 then [mkDiag Error str b]
else if d /= c then
if isMixfix o then [mkDiag Warning str b]
else [mkDiag Hint ("non-mixfix-id '" ++ show o ++ "' for binder") b]
else []
addBinder :: Id -> Id -> State.State Env ()
addBinder o b = do
bs <- State.gets binders
as <- State.gets assumps
when (Map.member b as) $ addDiags
[mkDiag Warning "binder shadows shadows global name(s)" b]
case Map.lookup b bs of
Just o2 -> if o == o2 then do
addDiags [Diag Warning
("binder conflict for: " ++ show b ++ expected o2 o)
$ posOfId b]
addBinding o b
else addDiags [mkDiag Warning "repeated binder syntax" b]
Nothing -> addBinding o b
fromAText :: Annote_text -> String
fromAText t = case t of
Line_anno s -> s
Group_anno l -> unlines l