{- |

Module : $Header$

Description : analyse operation declarations

Copyright : (c) Christian Maeder and Uni Bremen 2003-2005

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : experimental

Portability : portable

analyse operation declarations

-}

module HasCASL.OpDecl

( anaOpItem

, anaProgEq

, mkEnvForall

) where

import Data.Maybe

import qualified Data.Set as Set

import qualified Data.Map as Map

import Text.ParserCombinators.Parsec (parse, eof)

import Control.Monad

import Common.Id

import Common.Lib.State as State

import Common.Result

import Common.GlobalAnnotations

import Common.AS_Annotation

import Common.Doc

import Common.Lexer (skip)

import Common.Parsec

import HasCASL.As

import HasCASL.HToken

import HasCASL.TypeAna

import HasCASL.VarDecl

import HasCASL.Le

import HasCASL.Builtin

import HasCASL.AsUtils

import HasCASL.MixAna

import HasCASL.TypeCheck

import HasCASL.ProgEq

import HasCASL.Unify

anaAttr :: TypeScheme -> OpAttr -> State Env (Maybe OpAttr)

anaAttr (TypeScheme tvs ty _) b = case b of

UnitOpAttr trm ps -> do

e <- get

let mTy = let (fty, fArgs) = getTypeAppl ty in case fArgs of

[arg, t3] | lesserType e fty (toFunType PFunArr)

-> let (pty, ts) = getTypeAppl arg in case ts of

[t1, t2] | lesserType e pty (toProdType 2 ps)

-> Just (t1, t2, t3)

_ -> Nothing

_ -> Nothing

let tm = typeMap e

mapM_ (addTypeVarDecl False) tvs

case mTy of

Nothing -> do addDiags [mkDiag Error

"unexpected type of operation" ty]

putTypeMap tm

return Nothing

Just (t1, t2, t3) ->

do unless (t1 == t2 && t2 == t3)

$ addDiags [mkDiag Error

"unexpected type components of operation" ty]

mt <- resolveTerm t3 trm

putTypeMap tm

return $ case mt of

Nothing -> Nothing

Just t -> Just $ UnitOpAttr t ps

_ -> return $ Just b

tuplePatternToType :: [VarDecl] -> Type

tuplePatternToType vds =

mkProductTypeWithRange (map ( \ (VarDecl _ t _ _) -> t) vds) $ getRange vds

anaOpId :: OpBrand -> TypeScheme -> [OpAttr] -> PolyId -> State Env Bool

anaOpId br sc attrs i@(PolyId j _ _) =

do mSc <- anaPolyId i sc

case mSc of

Nothing -> return False

Just newSc -> do

mAttrs <- mapM (anaAttr newSc) attrs

addOpId j newSc (Set.fromList $ catMaybes mAttrs) $ NoOpDefn br

-- | analyse an op-item

anaOpItem :: OpBrand -> Annoted OpItem -> State Env (Annoted (Maybe OpItem))

anaOpItem br oi = do

let Result ds (Just bs) = extractBinders $ l_annos oi ++ r_annos oi

addDiags ds

case item oi of

OpDecl is sc attr ps -> do

case is of

[PolyId i _ _] -> mapM_ (addBinder i) bs

_ -> unless (null bs) $ addDiags

[mkDiag Warning "ignoring binder syntax" bs]

ois <- mapM (anaOpId br sc attr) is

let us = map fst $ filter snd $ zip is ois

return $ replaceAnnoted (if null us then Nothing else

Just $ OpDecl us sc attr ps) oi

OpDefn p@(PolyId i _ _) oldPats rsc@(TypeScheme tArgs scTy qs) trm ps

-> do

mapM_ (addBinder i) bs

checkUniqueVars $ concat oldPats

tvs <- gets localTypeVars

mArgs <- mapM anaddTypeVarDecl tArgs

mPats <- mapM (mapM anaVarDecl) oldPats

let newPats = map catMaybes mPats

monoPats = map (map makeMonomorph) newPats

pats = map (\ l -> mkTupleTerm (map QualVar l) nullRange) monoPats

vs <- gets localVars

mapM_ (mapM_ $ addLocalVar True) monoPats

let newArgs = catMaybes mArgs

mty <- anaStarType scTy

mtrm <- resolve trm

case (mty, mtrm) of

(Just rty, Just rTrm) -> do

let (partial, ty) = case getTypeAppl rty of

(TypeName j _ _ , [lt]) | j == lazyTypeId -> (Partial, lt)

_ -> (Total, rty)

monoty = monoType ty

mt <- typeCheck monoty $ TypedTerm rTrm AsType monoty ps

e <- get

newSc <- generalizeS $ TypeScheme newArgs

(getFunType ty partial

$ map tuplePatternToType newPats) qs

putLocalVars vs

putLocalTypeVars tvs

case mt of

Just lastTrm0 -> do

let lastTrm = case lastTrm0 of

TypedTerm lTrm AsType rTy rs ->

case getTypeOf lTrm of

Just oTy | lesserType e oTy rTy ->

if oTy == rTy then lTrm else

TypedTerm lTrm Inferred rTy rs

_ -> lastTrm0

_ -> lastTrm0

lamTrm = case (pats, partial) of

([], Total) -> lastTrm

_ -> LambdaTerm pats partial lastTrm ps

ot = QualOp br p newSc [] Infer

nullRange

lhs = mkApplTerm ot pats

ef = if isPred br then

mkLogTerm eqvId ps lhs lastTrm

else mkEqTerm eqId monoty ps lhs lastTrm

f = mkEnvForall e ef ps

addOpId i newSc Set.empty $ Definition br lamTrm

appendSentences

[(makeNamed (getRLabel oi) $ Formula f)

{ isDef = True }]

return $ replaceAnnoted

(Just $ OpDefn p oldPats rsc rTrm ps) oi

Nothing -> do

addOpId i newSc Set.empty $ NoOpDefn br

return $ replaceAnnoted

(Just $ OpDecl [p] newSc [] ps) oi

_ -> do

putLocalVars vs

putLocalTypeVars tvs

return $ replaceAnnoted Nothing oi

-- | analyse a program equation

anaProgEq :: Annoted ProgEq -> State Env (Maybe ProgEq)

anaProgEq ape = do

let pe@(ProgEq _ _ q) = item ape

rp <- resolve (LetTerm Program [pe] (BracketTerm Parens [] q) q)

case rp of

Just t@(LetTerm _ (rpe@(ProgEq {}) : _) _ _) -> do

mp <- typeCheck unitType t

ga <- State.gets globAnnos

case mp of

Just (LetTerm _ (newPrg@(ProgEq newPat _ _) : _) _ _) ->

case getAppl newPat of

Just (i, sc, _) -> do

addOpId i sc Set.empty $ NoOpDefn Op

appendSentences [(makeNamed ("pe_" ++ showId i "")

$ ProgEqSen i sc newPrg)

{ isDef = True }]

e <- get

unless (isLHS e newPat)

$ addDiags [mkNiceDiag ga Warning

"illegal lhs pattern" 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 $ annoArg 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 $ mapMaybe 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