{- |

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.Le

import Common.GlobalAnnotations

import Common.GlobalAnnotationsFunctions

import CASL.MixfixParser

import Common.Result

import Common.Id

import qualified Common.Lib.Map as Map

import Control.Monad

import Control.Monad.State

import qualified Char as C

import Data.List(intersperse)

import HasCASL.Unify

-- Earley Algorithm

data GrSym = Terminal Token

| NonTerminal Type -- a term of type Type

deriving (Show, Eq)

type Rule = [GrSym]

data PState = PState Id -- the rule to match

Type -- type of Id

[Pos] -- positions of Id tokens

[Term] -- currently collected arguments

-- both in reverse order

[Token] -- part of the rule after the "dot"

Int -- index into the ParseMap/input string

instance Eq PState where

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

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

instance Ord PState where

PState r1 _ _ _ t1 p1 <= PState r2 _ _ _ t2 p2 =

(r1, t1, p1) <= (r2, 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 t <- freshInst $ opType info

return $ PState ide t [] []

(getTokenList termStr $ stripFinalPlaces ide) i

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

mkApplState i (ide, info) =

do t <- freshInst $ opType info

return $ PState ide 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 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 mkTokState toks = PState (Id toks [] []) (MixfixType [])

[] [] 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)

type ParseMap = Map.Map Int [PState]

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 m =

let t = case trm of

TermToken x -> if isLitToken x then litTok else

x

in

Map.insert (i+1) (

foldr (\ (PState o 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 ty p a

(termTok : commaTok : tail ts) k)

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

else if t == parenTok then

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

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

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

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

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

else (PState o 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 (PState ide _ rs a _ _) =

let vs = getTokenList place ide

ar = reverse a

_qs = reverse rs

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@(PState i _ bs a _ _) =

if i == listId then

case list_lit $ literal_annos g of

Nothing -> error "toAppl"

Just (_, c, f) ->

let (b1, b2) = listBrackets g

nb1 = length b1

nb2 = length b2

ra = reverse a

na = length ra

nb = length bs

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

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

in if null a then asAppl c [] (if null bs then nullPos else last bs)

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

let br = reverse bs

br1 = drop (nb1 - 1) br

in mkList (reverse a) br1

else error "toAppl"

else stateToAppl s

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

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

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

PState o ty b (toAppl g s : a)

(tail ts) k1 : l) []

$ filter (filterByPrec g s)

$ lookUp 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 m = Map.insert i (complRec g m $ lookUp m i) m

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

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

data CountMap = CountMap { counter :: Int

, parseMap :: Map.Map Int [PState]

}

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

predict g is i cm@(CountMap c m) =

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

&& head ts == termTok)

(lookUp m i)

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

in CountMap c2 $ Map.insertWith (++) i ps m

else cm

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

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

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

let CountMap c2 pm = predict g is i m

m1 = complete g (i+1) $

scan trm i pm

in if null (lookUp m1 (i+1)) && null ds

then (i+1, Diag Error ("unexpected mixfix token: "

++ show trm)

(nullPos) : ds, m)

else (i+1, ds, CountMap c2 m1)

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 m i

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

resolve g ops c trm =

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

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

(0, [], CountMap c2 $ Map.single 0 $ ps)

ts = getAppls g i $ parseMap 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)

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