{- |

Module : $Header$

Copyright : (c) Christian Maeder 2003

Maintainer : hets@tzi.de

Stability : experimental

Portability : non-portable

Mixfix analysis of terms, adapted from the CASL analysis

-}

module HasCASL.MixAna where

import HasCASL.As

import HasCASL.AsUtils()

import HasCASL.Le

import Common.GlobalAnnotations

import Common.GlobalAnnotationsFunctions

import Common.Result

import Common.Id

import Common.Lexer

import qualified Common.Lib.Map as Map

import Control.Monad

import Control.Monad.State

import qualified Char as C

import Data.List(intersperse)

import Data.Maybe(mapMaybe)

import HasCASL.Unify

-- Earley Algorithm

data PState = PState { ruleId :: Id -- the rule to match

, ruleScheme :: TypeScheme -- to make id unique

, ruleType :: Type -- type of Id

, posList :: [Pos] -- positions of Id tokens

, ruleArgs :: [Term] -- currently collected arguments

-- both in reverse order

, restRule :: [Token] -- part of the rule after the "dot"

, stateNo :: Int -- index into the ParseMap/input string

}

instance Eq PState where

PState r1 s1 _ _ _ t1 p1 == PState r2 s2 _ _ _ t2 p2 =

(r1, s1, t1, p1) == (r2, s2, t2, p2)

instance Show PState where

showsPrec _ (PState r _ _ _ _ d p) = showChar '{'

. showSepList (showString "") showTok first

. showChar '.'

. showSepList (showString "") showTok d

. shows p . showChar '}'

where first = take (length v - length d) v

v = getTokenList place r

termStr :: String

termStr = "(T)"

commaTok, parenTok, termTok :: Token

commaTok = mkSimpleId "," -- for list elements

termTok = mkSimpleId termStr

parenTok = mkSimpleId "(..)"

colonTok, asTok, varTok, opTok, predTok, inTok, caseTok, litTok :: Token

colonTok = mkSimpleId ":"

asTok = mkSimpleId "as"

inTok = mkSimpleId "in"

caseTok = mkSimpleId "case"

varTok = mkSimpleId "(v)"

opTok = mkSimpleId "(o)"

predTok = mkSimpleId "(p)"

litTok = mkSimpleId "\""

stripFinalPlaces :: Id -> Id

stripFinalPlaces (Id ts cs ps) =

Id (fst $ splitMixToken ts) cs ps

mkState :: Int -> (Id, OpInfo) -> State Int PState

mkState i (ide, info) =

do let sc = opType info

t <- freshInst sc

return $ PState ide sc t [] []

(getTokenList termStr $ stripFinalPlaces ide) i

mkApplState :: Int -> (Id, OpInfo) -> State Int PState

mkApplState i (ide, info) =

do let sc = opType info

t <- freshInst sc

return $ PState ide sc t [] [] (getTokenList place ide) i

listId :: Id

-- unique id (usually "[]" yields two tokens)

listId = Id [mkSimpleId "[]"] [] []

listStates :: GlobalAnnos -> Int -> State Int [PState]

-- no empty list (can be written down directly)

listStates g i =

do ty <- freshType star

let listState toks = PState listId (simpleTypeScheme $

BracketType Squares [] [])

ty [] [] toks i

(b1, b2) = listBrackets g

return $ if null b1 || null b2 then []

else [ listState (b1 ++ [termTok] ++ b2)

, listState (b1 ++ [termTok, commaTok] ++ b2)]

-- these are the possible matches for the nonterminal (T)

-- the same states are used for the predictions

initialState :: GlobalAnnos -> [(Id, OpInfo)] -> Int -> State Int [PState]

initialState g ids i =

do ls <- listStates g i

l1 <- mapM (mkState i) ids

l2 <- mapM (mkApplState i) ids

let ty = MixfixType []

sc = simpleTypeScheme ty

mkTokState toks = PState (Id toks [] []) sc ty

[] [] toks i

return (mkTokState [parenTok] :

mkTokState [termTok, colonTok] :

mkTokState [termTok, asTok] :

mkTokState [termTok, inTok] :

mkTokState [varTok] :

mkTokState [opTok] :

mkTokState [litTok] :

mkTokState [termTok, termTok] :

ls ++ l1 ++ l2)

lookUp :: (Ord a, MonadPlus m) => Map.Map a (m b) -> a -> (m b)

lookUp ce k = Map.findWithDefault mzero k ce

-- match (and shift) a token (or partially finished term)

scan :: Term -> Int -> ParseMap -> ParseMap

scan trm i cm =

let t = case trm of

TermToken x -> if isLitToken x then litTok else

x

_ -> litTok

m = parseMap cm

in

cm { parseMap = Map.insert (i+1) (

foldr (\ (PState o sc ty b a ts k) l ->

if null ts || head ts /= t then l

else let p = tokPos t : b in

if t == commaTok && o == listId then

-- list elements separator

(PState o sc ty p a

(termTok : commaTok : tail ts) k)

: (PState o sc ty p a (termTok : tail ts) k) : l

else if t == parenTok then

(PState o sc ty b (trm : a) (tail ts) k) : l

else if t == varTok || t == opTok || t == predTok then

(PState o sc ty b [trm] (tail ts) k) : l

else if t == colonTok || t == asTok then

(PState o sc ty b [mkTerm $ head a] [] k) : l

else (PState o sc ty p a (tail ts) k) : l) []

(lookUp m i)) m }

where mkTerm t1 = case trm of

_ -> t1

-- construct resulting term from PState

stateToAppl :: PState -> Term

stateToAppl p =

let vs = getTokenList place $ ruleId p

ar = reverse $ ruleArgs p

in if vs == [termTok, colonTok]

|| vs == [termTok, asTok]

|| vs == [varTok]

|| vs == [opTok]

|| vs == [predTok]

|| vs == [parenTok]

then head ar

else head ar

toAppl :: GlobalAnnos -> PState -> Term

toAppl g s =

if ruleId s == listId then

case list_lit $ literal_annos g of

Nothing -> error "toAppl"

Just (b, c, f) ->

let (b1, b2) = getListBrackets b

nb1 = length b1

nb2 = length b2

ra = reverse $ ruleArgs s

na = length ra

br = reverse $ posList s

nb = length br

mkList [] ps = asAppl c [] (head ps)

mkList (hd:tl) ps = asAppl f [hd, mkList tl (tail ps)] (head ps)

in if null ra then asAppl c []

(if null br then nullPos else head br)

else if nb + 1 == nb1 + nb2 + na then

let br1 = drop (nb1 - 1) br

in mkList ra br1

else error "toAppl"

else stateToAppl s

asAppl :: Id -> [Term] -> Pos -> Term

asAppl f args p = let pos = if null args then [] else [p]

in ApplTerm (QualOp (InstOpId f [] [])

(simpleTypeScheme $ MixfixType [])

[]) (TupleTerm args []) pos

-- precedence graph stuff

checkArg :: GlobalAnnos -> AssocEither -> Id -> Id -> Bool

checkArg g dir op arg =

if arg == op

then isAssoc dir (assoc_annos g) op || not (isInfix op)

else

case precRel (prec_annos g) op arg of

Lower -> True

Higher -> False

ExplGroup BothDirections -> False

ExplGroup NoDirection -> not $ isInfix arg

checkAnyArg :: GlobalAnnos -> Id -> Id -> Bool

checkAnyArg g op arg =

case precRel (prec_annos g) op arg of

ExplGroup BothDirections -> isInfix op && op == arg

_ -> True

isLeftArg, isRightArg :: Id -> Int -> Bool

isLeftArg (Id ts _ _) n = n + 1 == (length $ takeWhile isPlace ts)

isRightArg (Id ts _ _) n = n == (length $ filter isPlace ts) -

(length $ takeWhile isPlace (reverse ts))

filterByPrec :: GlobalAnnos -> PState -> PState -> Bool

filterByPrec _ _ (PState _ _ _ _ _ [] _) = False

filterByPrec g (PState argIde _ _ _ _ _ _)

(PState opIde _ _ _ args (hd:_) _) =

if hd == termTok then

if opIde == listId || argIde == listId then True

else let n = length args in

if isLeftArg opIde n then

if isPostfix opIde && (isPrefix argIde

|| isInfix argIde) then False

else checkArg g ALeft opIde argIde

else if isRightArg opIde n then

if isPrefix opIde && isInfix argIde then False

else checkArg g ARight opIde argIde

else checkAnyArg g opIde argIde

else False

expandType :: TypeMap -> Type -> Type

expandType tm oldT =

case oldT of

TypeName _ _ _ -> fst $ expandAlias tm oldT

KindedType t _ _ -> t

LazyType t _ -> t

_ -> oldT

filterByType :: ParseMap -> PState -> PState -> Maybe PState

filterByType cm argState opState =

let tm = typeAliases cm in

case expandType tm $ ruleType opState of

FunType t1 _ t2 _ ->

case expandType tm t1 of

argType ->

do s <- maybeResult $ unify tm argType

$ ruleType argState

return opState {ruleType = subst s t2,

ruleArgs = stateToAppl argState:

ruleArgs opState}

_ -> Nothing

-- final complete/reduction phase

-- when a grammar rule (mixfix Id) has been fully matched

collectArg :: GlobalAnnos -> ParseMap -> PState -> [PState]

-- pre: finished rule

collectArg g m s@(PState _ _ _ _ _ _ k) =

mapMaybe (filterByType m s)

$ filter (filterByPrec g s)

$ lookUp (parseMap m) k

compl :: GlobalAnnos -> ParseMap -> [PState] -> [PState]

compl g m l =

concat $ map (collectArg g m)

$ filter (\ (PState _ _ _ _ _ ts _) -> null ts) l

complRec :: GlobalAnnos -> ParseMap -> [PState] -> [PState]

complRec g m l = let l1 = compl g m l in

if null l1 then l else complRec g m l1 ++ l

complete :: GlobalAnnos -> Int -> ParseMap -> ParseMap

complete g i cm =

let m = parseMap cm in

cm { parseMap = Map.insert i (complRec g cm $ lookUp m i) m }

-- predict which rules/ids might match for (the) nonterminal(s) (termTok)

-- provided the "dot" is followed by a nonterminal

data ParseMap = ParseMap { varCount :: Int

, typeAliases :: TypeMap

, parseMap :: Map.Map Int [PState]

}

predict :: GlobalAnnos -> [(Id, OpInfo)] -> Int -> ParseMap -> ParseMap

predict g is i cm =

let m = parseMap cm in

if i /= 0 && any (\ (PState _ _ _ _ _ ts _) -> not (null ts)

&& head ts == termTok)

(lookUp m i)

then let (ps, c2) = runState (initialState g is i)

(varCount cm)

in cm { varCount = c2

, parseMap = Map.insertWith (++) i ps m }

else cm

type Chart = (Int, [Diagnosis], ParseMap)

nextState :: GlobalAnnos -> [(Id, OpInfo)] -> Term -> Chart -> Chart

nextState g is trm (i, ds, m) =

let cm1 = predict g is i m

cm2 = complete g (i+1) $

scan trm i cm1

in if null (lookUp (parseMap cm2) (i+1)) && null ds

then (i+1, mkDiag Error "unexpected mixfix token" trm

: ds, m)

else (i+1, ds, cm2)

iterateStates :: GlobalAnnos -> [(Id, OpInfo)] -> [Term] -> Chart -> Chart

iterateStates g ops terms c =

let self = iterateStates g ops

_resolveTerm = resolve g ops

in if null terms then c

else case head terms of

MixfixTerm ts -> self (ts ++ tail terms) c

BracketTerm _ ts ps ->

self (expand "[" "]" ts ps ++ tail terms) c

t -> self (tail terms) (nextState g ops t c)

where expand = expandPos TermToken

getAppls :: GlobalAnnos -> Int -> ParseMap -> [Term]

getAppls g i m =

map (toAppl g) $

filter (\ (PState _ _ _ _ _ ts k) -> null ts && k == 0) $

lookUp (parseMap m) i

resolve :: GlobalAnnos -> [(Id, OpInfo)] -> ParseMap -> Term -> Result Term

resolve g ops p trm =

let (ps, c2) = runState (initialState g ops 0) (varCount p)

(i, ds, m) = iterateStates g ops [trm]

(0, [], p { varCount = c2, parseMap =

Map.single 0 $ ps} )

ts = getAppls g i m

in if null ts then if null ds then

plain_error trm ("no resolution for term: "

++ show trm)

(nullPos)

else Result ds (Just trm)

else if null $ tail ts then Result ds (Just (head ts))

else Result (Diag Error ("ambiguous mixfix term\n\t" ++

(concat

$ intersperse "\n\t"

$ map (show)

$ take 5 ts)) (nullPos) : ds) (Just trm)

resolveTerm :: Term -> State Env (Result Term)

resolveTerm t =

do tm <- getTypeMap

as <- getAssumps

c <- getCounter

ga <- getGlobalAnnos

let ops = concatMap (\ (i, l) -> map ( \ e -> (i, e)) l)

$ Map.toList as

return $ resolve ga ops (ParseMap c tm Map.empty) t