OpDecl.hs revision a94b530fa82bb281caac766a9c0f7b2fcfe7a584
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann{- |
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannModule : $Header$
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannCopyright : (c) Christian Maeder and Uni Bremen 2003
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMaintainer : maeder@tzi.de
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannStability : experimental
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannPortability : portable
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann analyse operation declarations
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-}
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannmodule HasCASL.OpDecl where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport Data.Maybe
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport Common.Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport Common.AS_Annotation
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport Common.Lib.State
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport Common.Result
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport Common.GlobalAnnotations
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.As
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.VarDecl
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.Le
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.Builtin
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.AsUtils
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.TypeAna
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.TypeCheck
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport HasCASL.ProgEq
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaAttr :: GlobalAnnos -> TypeScheme -> OpAttr -> State Env (Maybe OpAttr)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaAttr ga (TypeScheme tvs ty _) (UnitOpAttr trm ps) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann do let mTy = case unalias ty of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann FunType arg _ t3 _ ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann case unalias arg of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ProductType [t1, t2] _ -> Just (t1,t2,t3)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann _ -> Nothing
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann _ -> Nothing
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann tm <- gets typeMap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mapM_ (addTypeVarDecl False) tvs
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann case mTy of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Nothing -> do addDiags [mkDiag Error
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann "unexpected type of operation" ty]
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mt <- resolveTerm ga Nothing trm
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann putTypeMap tm
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann case mt of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Nothing -> return Nothing
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Just t -> return $ Just $ UnitOpAttr t ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Just (t1, t2, t3) ->
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann do if t1 == t2 && t2 == t3 then
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return ()
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann else addDiags [mkDiag Error
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann "unexpected type components of operation" ty]
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mt <- resolveTerm ga (Just t3) trm
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann putTypeMap tm
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann case mt of Nothing -> return Nothing
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Just t -> return $ Just $ UnitOpAttr t ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaAttr _ _ b = return $ Just b
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannpatternsToType :: [[VarDecl]] -> Type -> Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannpatternsToType [] t = t
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannpatternsToType (p: ps) t = FunType (tuplePatternToType p) PFunArr
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (patternsToType ps t) []
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanntuplePatternToType :: [VarDecl] -> Type
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanntuplePatternToType vds = mkProductType (map ( \ (VarDecl _ t _ _) -> t) vds) []
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanngetUninstOpId :: TypeScheme -> OpId -> (OpId, TypeScheme)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanngetUninstOpId (TypeScheme tvs q ps) (OpId i args qs) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (OpId i [] qs, TypeScheme (args ++ tvs) q ps)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaOpId :: GlobalAnnos -> OpBrand -> TypeScheme -> [OpAttr] -> OpId
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann -> State Env (Maybe OpId)
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaOpId ga br partSc attrs o =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann do let (OpId i _ _, sc) = getUninstOpId partSc o
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mSc <- anaTypeScheme sc
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann case mSc of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Nothing -> return Nothing
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Just newSc -> do
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mAttrs <- mapM (anaAttr ga newSc) attrs
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mo <- addOpId i newSc (catMaybes mAttrs) $ NoOpDefn br
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return $ fmap (const o) mo
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaOpItem :: GlobalAnnos -> OpBrand -> OpItem -> State Env OpItem
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaOpItem ga br (OpDecl is sc attr ps) = do
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann us <- mapM (anaOpId ga br sc attr) is
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann return $ OpDecl (catMaybes us) sc attr ps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannanaOpItem ga br (OpDefn o oldPats sc partial trm ps) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann do let (op@(OpId i _ _), extSc@(TypeScheme tArgs scTy qs)) =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann getUninstOpId sc o
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann checkUniqueVars $ concat oldPats
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann tm <- gets typeMap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann mArgs <- mapM anaTypeVarDecl tArgs
mPats <- mapM (mapM anaVarDecl) oldPats
let newPats = map catMaybes mPats
monoPats = map (map makeMonomorph) newPats
pats = map (\ l -> mkTupleTerm (map QualVar l) []) monoPats
as <- gets assumps
mapM (mapM addVarDecl) monoPats
let newArgs = catMaybes mArgs
checkUniqueTypevars newArgs
mty <- anaStarType scTy
case mty of
Just ty -> do
mt <- resolveTerm ga Nothing $ TypedTerm trm AsType ty ps
putAssumps as
putTypeMap tm
mSc <- fromResult $ const $ generalize $
TypeScheme tArgs
(patternsToType newPats ty) qs
case (mt, mSc) of
(Just lastTrm, Just newSc) -> do
let lamTrm = case (pats, partial) of
([], Total) -> lastTrm
_ -> LambdaTerm pats partial lastTrm ps
ot = QualOp br (InstOpId i [] []) newSc []
lhs = mkApplTerm ot pats
ef = mkEqTerm eqId ps lhs lastTrm
f = mkForall (map GenTypeVarDecl tArgs
++ (map GenVarDecl $
concatMap extractVars pats)) ef
addOpId i newSc [] $ Definition br lamTrm
appendSentences [NamedSen
("def_" ++ showId i "")
$ Formula f]
return $ OpDefn op [] newSc Total lamTrm ps
_ -> return $ OpDefn op newPats extSc partial trm ps
Nothing -> do
mt <- resolveTerm ga Nothing trm
putAssumps as
putTypeMap tm
return $ OpDefn op oldPats extSc partial
(case mt of Nothing -> trm
Just x -> x) ps
-- ----------------------------------------------------------------------------
-- ProgEq
-- ----------------------------------------------------------------------------
anaProgEq :: GlobalAnnos -> ProgEq -> State Env ProgEq
anaProgEq ga pe@(ProgEq pat trm qs) =
do as <- gets assumps
mp <- checkPattern ga pat
case mp of
Nothing -> return pe
Just newPat -> do
let exbs = extractVars newPat
checkUniqueVars exbs
mapM_ addVarDecl exbs
mt <- resolveTerm ga Nothing trm
-- guarantee that type of pattern and term are equal!
putAssumps as
case mt of
Just newTerm -> let newPrg = ProgEq newPat newTerm qs in
case getAppl newPat of
Just (i, sc, _) -> do
addOpId i sc [] $ NoOpDefn Op
appendSentences [NamedSen ("pe_" ++ showId i "")
$ ProgEqSen i sc newPrg]
e <- get
if isLHS e newPat then return ()
else addDiags [mkDiag Warning
"illegal lhs pattern"
newPat]
return newPrg
_ -> do addDiags [mkDiag Error
"illegal toplevel pattern"
newPat]
return newPrg
_ -> return $ ProgEq newPat trm qs
getApplConstr :: Pattern -> (Pattern, [Pattern])
getApplConstr pat =
case pat of
ApplTerm p1 p2 _ ->
let (tp, args) = getApplConstr p1 in (tp, p2:args)
TypedTerm tp _ _ _ -> getApplConstr tp
_ -> (pat, [])