{- |

Module : $Header$

Description : mixfix analysis for terms

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

Mixfix analysis of terms and patterns, type annotations are also analysed

-}

module HasCASL.MixAna

( resolve

, anaPolyId

, makeRules

, getPolyIds

, iterateCharts

, toMixTerm

, uTok

) where

import Common.AnnoParser

import Common.AnnoState

import Common.ConvertMixfixToken

import Common.DocUtils

import Common.Earley

import Common.GlobalAnnotations

import Common.Id

import Common.Lib.State

import Common.Parsec

import Common.Prec

import Common.Result

import qualified Data.Map as Map

import qualified Data.Set as Set

import HasCASL.As

import HasCASL.AsUtils

import HasCASL.PrintAs

import HasCASL.VarDecl

import HasCASL.Le

import HasCASL.ParseTerm

import HasCASL.TypeAna

import qualified Text.ParserCombinators.Parsec as P

import Data.Maybe

import Control.Exception (assert)

import Control.Monad

addType :: Term -> Term -> Term

addType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

addType _ _ = error "addType"

-- | try to reparse terms as a compound list

isCompoundList :: Set.Set [Id] -> [Term] -> Bool

isCompoundList compIds =

maybe False (`Set.member` compIds) . mapM reparseAsId

isTypeList :: Env -> [Term] -> Bool

isTypeList e l = case mapM termToType l of

Nothing -> False

Just ts ->

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

in isJust ml && not (hasErrors ds)

termToType :: Term -> Maybe Type

termToType t = case P.runParser ((case getPosList t of

[] -> return ()

p : _ -> P.setPosition $ fromPos p)

>> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of

Right x -> Just x

_ -> Nothing

anaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)

anaPolyId (PolyId i@(Id _ cs _) _ _) sc = do

mSc <- anaTypeScheme sc

case mSc of

Nothing -> return Nothing

Just newSc@(TypeScheme tvars _ _) -> do

e <- get

let ids = Set.unions

[ Map.keysSet $ classMap e

, Map.keysSet $ typeMap e

, Map.keysSet $ assumps e ]

es = filter (not . flip Set.member ids) cs

addDiags $ map (mkDiag (if null tvars then Hint else Warning)

"unexpected identifier in compound list") es

unless (null cs || null tvars)

$ addDiags [mkDiag Hint "is polymorphic compound identifier" i]

return $ Just newSc

resolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme

resolveQualOp i@(PolyId j _ _) sc = do

mSc <- anaPolyId i sc

e <- get

case mSc of

Nothing -> return sc -- and previous

Just nSc -> do

when (Set.null $ Set.filter ((== nSc) . opType)

$ Map.findWithDefault Set.empty j $ assumps e)

$ addDiags [mkDiag Error "operation not found" j]

return nSc

iterateCharts :: GlobalAnnos -> Set.Set Id -> Set.Set [Id] -> [Term]

-> Chart Term -> State Env (Chart Term)

iterateCharts ga sIds compIds terms chart = do

e <- get

let self = iterateCharts ga sIds compIds

oneStep = nextChart addType (toMixTerm e) ga chart

vs = localVars e

tm = typeMap e

case terms of

[] -> return chart

t : tt -> let recurse trm = self tt $ oneStep

(trm, exprTok {tokPos = getRange trm}) in case t of

MixfixTerm ts -> self (ts ++ tt) chart

MixTypeTerm q typ ps -> do

mTyp <- anaStarType typ

case mTyp of

Nothing -> recurse t

Just nTyp -> self tt $ oneStep

(MixTypeTerm q (monoType nTyp) ps, typeTok {tokPos = ps})

BracketTerm b ts ps ->

let bres = self (expandPos TermToken

(getBrackets b) ts ps ++ tt) chart in case (b, ts, tt) of

(Squares, _ : _, _)

| isCompoundList compIds ts -> do

addDiags [mkDiag Hint "is compound list" t]

bres

| isTypeList e ts -> do

let testChart = oneStep (t, typeInstTok {tokPos = ps})

if null $ solveDiags testChart then do

addDiags [mkDiag Hint "is type list" t]

self tt testChart

else bres

(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

| elem i [tupleId, 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 -> (TokRules, 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 -> if isSimpleToken tok && not (Set.member tok ks)

|| tok == uTok

then Set.singleton (simpleIdToId tok, m2, [tok])

else Set.empty

, 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)