4752N/A{- |

4752N/AModule : $Header$

4752N/ADescription : mixfix analysis for terms

4752N/ACopyright : (c) Christian Maeder and Uni Bremen 2003-2005

4752N/ALicense : GPLv2 or higher, see LICENSE.txt

4752N/A

4752N/AMaintainer : Christian.Maeder@dfki.de

4752N/AStability : experimental

4752N/APortability : portable

4752N/A

4752N/AMixfix analysis of terms and patterns, type annotations are also analysed

4752N/A-}

4752N/A

4752N/Amodule HasCASL.MixAna

4752N/A ( resolve

4752N/A , anaPolyId

4752N/A , makeRules

4752N/A , getPolyIds

4752N/A , iterateCharts

4752N/A , toMixTerm

4752N/A , uTok

4752N/A ) where

4752N/A

4752N/Aimport Common.AnnoParser

4752N/Aimport Common.AnnoState

4752N/Aimport Common.ConvertMixfixToken

5821N/Aimport Common.DocUtils

4752N/Aimport Common.Earley

4752N/Aimport Common.GlobalAnnotations

4752N/Aimport Common.Id

4752N/Aimport Common.Lib.State

4752N/Aimport Common.Parsec

4752N/Aimport Common.Prec

4752N/Aimport Common.Result

4752N/A

4752N/Aimport qualified Data.Map as Map

4752N/Aimport qualified Data.Set as Set

4752N/A

4752N/Aimport HasCASL.As

4752N/Aimport HasCASL.AsUtils

4752N/Aimport HasCASL.PrintAs

4752N/Aimport HasCASL.VarDecl

4752N/Aimport HasCASL.Le

4752N/Aimport HasCASL.ParseTerm

4752N/Aimport HasCASL.TypeAna

4752N/A

4752N/Aimport qualified Text.ParserCombinators.Parsec as P

4752N/A

4752N/Aimport Data.Maybe

4752N/Aimport Control.Exception (assert)

4752N/Aimport Control.Monad

4752N/A

4752N/AaddType :: Term -> Term -> Term

4752N/AaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

4752N/AaddType _ _ = error "addType"

4752N/A

4752N/A-- | try to reparse terms as a compound list

4752N/AisCompoundList :: Set.Set [Id] -> [Term] -> Bool

4752N/AisCompoundList compIds =

4752N/A maybe False (flip Set.member compIds) . mapM reparseAsId

4752N/A

4752N/AisTypeList :: Env -> [Term] -> Bool

4752N/AisTypeList e l = case mapM termToType l of

4752N/A Nothing -> False

4752N/A Just ts ->

4752N/A let Result ds ml = mapM ( \ t -> anaTypeM (Nothing, t) e) ts

4752N/A in isJust ml && not (hasErrors ds)

4752N/A

4752N/AtermToType :: Term -> Maybe Type

4752N/AtermToType t = case P.runParser ((case getPosList t of

4752N/A [] -> return ()

4752N/A p : _ -> P.setPosition $ fromPos p)

4752N/A >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of

4752N/A Right x -> Just x

4752N/A _ -> Nothing

4752N/A

4752N/AanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)

4752N/AanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do

4752N/A mSc <- anaTypeScheme sc

4752N/A case mSc of

4752N/A Nothing -> return Nothing

4752N/A Just newSc@(TypeScheme tvars _ _) -> do

4752N/A e <- get

4752N/A let ids = Set.unions

4752N/A [ Map.keysSet $ classMap e

4752N/A , Map.keysSet $ typeMap e

4752N/A , Map.keysSet $ assumps e ]

4752N/A es = filter (not . flip Set.member ids) cs

4752N/A addDiags $ map (mkDiag Warning

4752N/A "unexpected identifier in compound list") es

4752N/A unless (null cs || null tvars)

4752N/A $ addDiags [mkDiag Hint "is polymorphic compound identifier" i]

4752N/A return $ Just newSc

4752N/A

4752N/AresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme

4752N/AresolveQualOp i@(PolyId j _ _) sc = do

4752N/A mSc <- anaPolyId i sc

4752N/A e <- get

4752N/A case mSc of

4752N/A Nothing -> return sc -- and previous

4752N/A Just nSc -> do

4752N/A when (Set.null $ Set.filter ((== nSc) . opType)

4752N/A $ Map.findWithDefault Set.empty j $ assumps e)

4752N/A $ addDiags [mkDiag Error "operation not found" j]

4752N/A return nSc

4752N/A

4752N/AiterateCharts :: GlobalAnnos -> Set.Set Id -> Set.Set [Id] -> [Term]

4752N/A -> Chart Term -> State Env (Chart Term)

4752N/AiterateCharts ga sIds compIds terms chart = do

4752N/A e <- get

4752N/A let self = iterateCharts ga sIds compIds

4752N/A oneStep = nextChart addType (toMixTerm e) ga chart

4752N/A vs = localVars e

4752N/A tm = typeMap e

4752N/A case terms of

5821N/A [] -> return chart

4752N/A t : tt -> let recurse trm = self tt $ oneStep

4752N/A (trm, exprTok {tokPos = getRange trm}) in case t of

4752N/A MixfixTerm ts -> self (ts ++ tt) chart

4752N/A MixTypeTerm q typ ps -> do

4752N/A mTyp <- anaStarType typ

4752N/A case mTyp of

4752N/A Nothing -> recurse t

4752N/A Just nTyp -> self tt $ oneStep

4752N/A (MixTypeTerm q (monoType nTyp) ps, typeTok {tokPos = ps})

4752N/A BracketTerm b ts ps ->

4752N/A let bres = self (expandPos TermToken

4752N/A (getBrackets b) ts ps ++ tt) chart in case (b, ts) of

4752N/A (Squares, _ : _) -> if isCompoundList compIds ts then do

4752N/A addDiags [mkDiag Hint "is compound list" t]

4752N/A bres

4752N/A else if isTypeList e ts then do

4752N/A let testChart = oneStep (t, typeInstTok {tokPos = ps})

4752N/A if null $ solveDiags testChart then do

4752N/A addDiags [mkDiag Hint "is type list" t]

self tt testChart

else bres

else bres

_ -> case (b, ts, tt) of

(Parens, [QualOp b2 v sc [] _ ps2], hd@(BracketTerm Squares

ts2@(_ : _) ps3) : rtt) | isTypeList e ts2 -> do

addDiags [mkDiag Hint "is type list" ts2]

nSc <- resolveQualOp v sc

self rtt $ oneStep

( QualOp b2 v nSc (bracketTermToTypes e hd) UserGiven ps2

, exprTok {tokPos = appRange ps ps3})

_ -> bres

QualVar (VarDecl v typ ok ps) -> do

mTyp <- anaStarType typ

recurse $ maybe t ( \ nType -> QualVar $ VarDecl v (monoType nType)

ok ps) mTyp

QualOp b v sc [] k ps -> do

nSc <- resolveQualOp v sc

recurse $ QualOp b v nSc [] k ps

QuantifiedTerm quant decls hd ps -> do

newDs <- mapM (anaddGenVarDecl False) decls

mt <- resolve hd

putLocalVars vs

putTypeMap tm

recurse $ QuantifiedTerm quant (catMaybes newDs) (fromMaybe hd mt) ps

LambdaTerm decls part hd ps -> do

mDecls <- mapM resolve decls

let anaDecls = catMaybes mDecls

bs = concatMap extractVars anaDecls

checkUniqueVars bs

mapM_ (addLocalVar False) bs

mt <- resolve hd

putLocalVars vs

recurse $ LambdaTerm anaDecls part (fromMaybe hd mt) ps

CaseTerm hd eqs ps -> do

mt <- resolve hd

newEs <- resolveCaseEqs eqs

recurse $ CaseTerm (fromMaybe hd mt) newEs ps

LetTerm b eqs hd ps -> do

newEs <- resolveLetEqs eqs

mt <- resolve hd

putLocalVars vs

recurse $ LetTerm b newEs (fromMaybe hd mt) ps

TermToken tok -> do

let (ds1, trm) = convertMixfixToken (literal_annos ga)

(flip ResolvedMixTerm []) TermToken tok

addDiags ds1

self tt $ oneStep $ case trm of

TermToken _ -> (trm, tok)

_ -> (trm, exprTok {tokPos = tokPos tok})

AsPattern vd p ps -> do

mp <- resolve p

recurse $ AsPattern vd (fromMaybe p mp) ps

TypedTerm trm k ty ps -> do

-- assume that type is analysed

mt <- resolve trm

recurse $ TypedTerm (fromMaybe trm mt) k ty ps

_ -> error ("iterCharts: " ++ show t)

-- * equation stuff

resolveCaseEq :: ProgEq -> State Env (Maybe ProgEq)

resolveCaseEq (ProgEq p t ps) = do

mp <- resolve p

case mp of

Nothing -> return Nothing

Just newP -> do

let bs = extractVars newP

checkUniqueVars bs

vs <- gets localVars

mapM_ (addLocalVar False) bs

mtt <- resolve t

putLocalVars vs

return $ case mtt of

Nothing -> Nothing

Just newT -> Just $ ProgEq newP newT ps

resolveCaseEqs :: [ProgEq] -> State Env [ProgEq]

resolveCaseEqs eqs = case eqs of

[] -> return []

eq : rt -> do

mEq <- resolveCaseEq eq

reqs <- resolveCaseEqs rt

return $ case mEq of

Nothing -> reqs

Just newEq -> newEq : reqs

resolveLetEqs :: [ProgEq] -> State Env [ProgEq]

resolveLetEqs eqs = case eqs of

[] -> return []

ProgEq pat trm ps : rt -> do

mPat <- resolve pat

case mPat of

Nothing -> do

resolve trm

resolveLetEqs rt

Just newPat -> do

let bs = extractVars newPat

checkUniqueVars bs

mapM_ (addLocalVar False) bs

mTrm <- resolve trm

case mTrm of

Nothing -> resolveLetEqs rt

Just newTrm -> do

reqs <- resolveLetEqs rt

return $ ProgEq newPat newTrm ps : reqs

mkPatAppl :: Term -> Term -> Range -> Term

mkPatAppl op arg qs = case op of

QualVar (VarDecl i (MixfixType []) _ _) -> ResolvedMixTerm i [] [arg] qs

_ -> ApplTerm op arg qs

bracketTermToTypes :: Env -> Term -> [Type]

bracketTermToTypes e t = case t of

BracketTerm Squares tys _ ->

map (monoType . snd) $ fromMaybe (error "bracketTermToTypes")

$ maybeResult $ mapM ( \ ty -> anaTypeM (Nothing, ty) e)

$ fromMaybe (error "bracketTermToTypes1") $ mapM termToType tys

_ -> error "bracketTermToTypes2"

toMixTerm :: Env -> Id -> [Term] -> Range -> Term

toMixTerm e i ar qs

| i == applId = assert (length ar == 2) $

let [op, arg] = ar in mkPatAppl op arg qs

| i == tupleId || i == unitId = mkTupleTerm ar qs

| otherwise = case unPolyId i of

Just j@(Id ts _ _) -> if isMixfix j && isSingle ar then

ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs

else assert (length ar == 1 + placeCount j) $

let (far, tar : sar) =

splitAt (placeCount $ mkId $ fst $ splitMixToken ts) ar

in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs

_ -> ResolvedMixTerm i [] ar qs

getKnowns :: Id -> Set.Set Token

getKnowns (Id ts cs _) =

Set.union (Set.fromList ts) $ Set.unions $ map getKnowns cs

resolve :: Term -> State Env (Maybe Term)

resolve trm = do

e <- get

let ass = assumps e

ga = globAnnos e

(addRule, ruleS, sIds) = makeRules ga (preIds e) (getPolyIds ass)

$ Set.union (Map.keysSet $ binders e)

$ Set.union (Map.keysSet ass)

$ Map.keysSet $ localVars e

chart <- iterateCharts ga sIds (getCompoundLists e) [trm]

$ initChart addRule ruleS

let Result ds mr = getResolved (showDoc . parenTerm) (getRange trm)

(toMixTerm e) chart

addDiags ds

return mr

getPolyIds :: Assumps -> Set.Set Id

getPolyIds = Set.unions . map ( \ (i, s) ->

Set.fold ( \ oi -> case opType oi of

TypeScheme (_ : _) _ _ -> Set.insert i

_ -> id) Set.empty s) . Map.toList

uTok :: Token

uTok = mkSimpleId "_"

builtinIds :: [Id]

builtinIds = [unitId, parenId, tupleId, exprId, typeId, applId]

makeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id

-> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)

makeRules ga ps@(p, _) polyIds aIds =

let (sIds, ids) = Set.partition isSimpleId aIds

ks = Set.fold (Set.union . getKnowns) Set.empty ids

rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks

m2 = maxWeight p + 2

in ( \ tok -> [(simpleIdToId tok, m2, [tok])

| isSimpleToken tok && not (Set.member tok ks)

|| tok == uTok ]

, partitionRules $ listRules m2 ga ++

initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)

, sIds)

initRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]

initRules (p, ps) polyIds bs is =

map ( \ i -> mixRule (getIdPrec p ps i) i)

(bs ++ is) ++

map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))

(filter isMixfix is) ++

-- identifiers with a positive number of type arguments

map ( \ i -> ( polyId i, getIdPrec p ps i

, getPolyTokenList i)) polyIds ++

map ( \ i -> ( protect $ polyId i, maxWeight p + 3

, getPlainPolyTokenList i)) (filter isMixfix polyIds)