38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski{- |

38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiModule : $Header$

38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiDescription : mixfix analysis for terms

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

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : Christian.Maeder@dfki.de

38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiStability : experimental

38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiPortability : portable

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski

38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiMixfix analysis of terms and patterns, type annotations are also analysed

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski-}

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskimodule HasCASL.MixAna

f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder ( resolve

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski , anaPolyId

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski , makeRules

7ace2968c79dc566e2c1e271663e4ff9d8e88067Till Mossakowski , getPolyIds

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski , iterateCharts

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder , toMixTerm

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder ) where

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder

aabc0d2680ea5411d5a9c82c1b2ca1f4144ca18fRainer Grabbeimport Common.GlobalAnnotations

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskiimport Common.Result

8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maederimport Common.Id

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maederimport Common.DocUtils

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maederimport Common.Earley

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maederimport Common.Lexer

7857e6ac0ed79540893dcb3e22af571ab2894932Till Mossakowskiimport Common.Prec

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskiimport Common.ConvertMixfixToken

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederimport Common.Lib.State

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederimport Common.AnnoState

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederimport Common.Anno_Parser

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maederimport qualified Data.Map as Map

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskiimport qualified Data.Set as Set

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder

f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowskiimport HasCASL.As

e194ab763147ac5df9c02fe40bdb5172013c36e8Christian Maederimport HasCASL.AsUtils

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maederimport HasCASL.PrintAs

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maederimport HasCASL.Unify

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskiimport HasCASL.VarDecl

7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowskiimport HasCASL.Le

f7fe363b4d668402d4a604727418e99a48abf533Christian Maederimport HasCASL.ParseTerm

f7fe363b4d668402d4a604727418e99a48abf533Christian Maederimport HasCASL.TypeAna

f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder

f7fe363b4d668402d4a604727418e99a48abf533Christian Maederimport qualified Text.ParserCombinators.Parsec as P

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowskiimport Data.Maybe

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maederimport Control.Exception (assert)

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder

2df21ee905717748894ce0d1b775b2a01bef4a44Christian MaederaddType :: Term -> Term -> Term

2df21ee905717748894ce0d1b775b2a01bef4a44Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

2df21ee905717748894ce0d1b775b2a01bef4a44Christian MaederaddType _ _ = error "addType"

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder-- | try to reparse terms as a compound list

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian MaederisCompoundList :: Set.Set [Id] -> [Term] -> Bool

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian MaederisCompoundList compIds =

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder maybe False (flip Set.member compIds) . mapM reparseAsId

7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder

38df2bfbe2de19e549aa812bab7c79fcf869b308Till MossakowskiisTypeList :: Env -> [Term] -> Bool

f57279093718fac174b661b128d03b5049ac467cTill MossakowskiisTypeList e l = case mapM termToType l of

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder Nothing -> False

7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder Just ts ->

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

7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian Maeder in isJust ml && not (hasErrors ds)

66c74e6bb78d2c417fd8495b5dd267c6bd0acd5aChristian Maeder

7f4e941c6b36ee1f694734bb35d82e395a2796b5Christian MaedertermToType :: Term -> Maybe Type

66c74e6bb78d2c417fd8495b5dd267c6bd0acd5aChristian MaedertermToType t = case P.runParser ((case getPosList t of

66c74e6bb78d2c417fd8495b5dd267c6bd0acd5aChristian Maeder [] -> return ()

38df2bfbe2de19e549aa812bab7c79fcf869b308Till Mossakowski p : _ -> P.setPosition $ fromPos p)

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

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder Right x -> Just x

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder _ -> Nothing

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)

33185a20196bfe66410ce6e9449005f5680a1656Christian MaederanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do

8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder mSc <- anaTypeScheme sc

33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder case mSc of

3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Nothing -> return Nothing

1e56499b4f29cca2c2a8aa47183a4fc248ed29e3Christian Maeder Just newSc@(TypeScheme tvars _ _) -> do

33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder e <- get

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder let ids = Set.unions

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder [ Map.keysSet $ classMap e

f57279093718fac174b661b128d03b5049ac467cTill Mossakowski , Map.keysSet $ typeMap e

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder , Map.keysSet $ assumps e ]

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

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder addDiags $ map (\ j -> mkDiag Warning

33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder "unexpected identifier in compound list" j) es

33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder if null cs || null tvars then return () else

7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowski addDiags [mkDiag Hint "is polymorphic compound identifier" i]

7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowski return $ Just newSc

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder

33185a20196bfe66410ce6e9449005f5680a1656Christian MaederresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme

33185a20196bfe66410ce6e9449005f5680a1656Christian MaederresolveQualOp i@(PolyId j _ _) sc = do

3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder mSc <- anaPolyId i sc

7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowski e <- get

ead4d317053c9092c59a16de66cac61f619a1293Christian Maeder case mSc of

f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowski Nothing -> return sc

1e56499b4f29cca2c2a8aa47183a4fc248ed29e3Christian Maeder Just nSc -> do

ead4d317053c9092c59a16de66cac61f619a1293Christian Maeder case findOpId e j nSc of

7857e6ac0ed79540893dcb3e22af571ab2894932Till Mossakowski Nothing -> addDiags [mkDiag Error "operation not found" j]

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder _ -> return ()

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder return nSc

ead4d317053c9092c59a16de66cac61f619a1293Christian Maeder

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian MaederiterateCharts :: GlobalAnnos -> Set.Set [Id] -> [Term] -> Chart Term

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder -> State Env (Chart Term)

f64563593a58e0e9de073c21ae69a1a877cb4692Till MossakowskiiterateCharts ga compIds terms chart = do

f64563593a58e0e9de073c21ae69a1a877cb4692Till Mossakowski e <- get

7b7ca7ef1ad99f1da0057cb8a6aa68cf6d04359bTill Mossakowski let self = iterateCharts ga compIds

33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder oneStep = nextChart addType (toMixTerm e) ga chart

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder vs = localVars e

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder tm = typeMap e

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder case terms of

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder [] -> return chart

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

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

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder MixTypeTerm q typ ps -> do

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder mTyp <- anaStarType typ

7ace2968c79dc566e2c1e271663e4ff9d8e88067Till Mossakowski case mTyp of

ecf4047143afe26a351e9fb60827671bf5e2e30dChristian Maeder Nothing -> recurse t

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder Just nTyp -> self tt $ oneStep

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

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder BracketTerm b ts ps ->

ecf4047143afe26a351e9fb60827671bf5e2e30dChristian Maeder let bres = self (expandPos TermToken

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

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder (Squares, _ : _) -> if isCompoundList compIds ts then do

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder addDiags [mkDiag Hint "is compound list" t]

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder bres

aabc0d2680ea5411d5a9c82c1b2ca1f4144ca18fRainer Grabbe else if isTypeList e ts then do

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

f7fe363b4d668402d4a604727418e99a48abf533Christian Maeder if null $ solveDiags testChart then do

aabc0d2680ea5411d5a9c82c1b2ca1f4144ca18fRainer Grabbe addDiags [mkDiag Hint "is type list" t]

4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe self tt testChart

4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe else bres

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder else bres

4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe _ -> case (b, ts, tt) of

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

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

4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe addDiags [mkDiag Hint "is type list" ts2]

4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe nSc <- resolveQualOp v sc

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder self rtt $ oneStep

33185a20196bfe66410ce6e9449005f5680a1656Christian Maeder ( QualOp b2 v nSc (bracketTermToTypes e hd) UserGiven ps2

4332f307777b02f460ab77a5dfade89628cbc215Rainer Grabbe , exprTok {tokPos = appRange ps ps3})

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder _ -> bres

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder QualVar (VarDecl v typ ok ps) -> do

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder mTyp <- anaStarType typ

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

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder ok ps) mTyp

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder QualOp b v sc [] k ps -> do

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder nSc <- resolveQualOp v sc

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder recurse $ QualOp b v nSc [] k ps

2df21ee905717748894ce0d1b775b2a01bef4a44Christian Maeder QuantifiedTerm quant decls hd ps -> do

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder newDs <- mapM (anaddGenVarDecl False) decls

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder mt <- resolve ga hd

baef5e750fbc19bad340a3293a17ba34d4fabbedChristian Maeder putLocalVars vs

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder putTypeMap tm

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) (maybe hd id mt) ps

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder LambdaTerm decls part hd ps -> do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mDecls <- mapM (resolvePattern ga) decls

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let anaDecls = catMaybes mDecls

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder bs = concatMap extractVars anaDecls

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder checkUniqueVars bs

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder mapM_ (addLocalVar False) bs

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder mt <- resolve ga hd

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder putLocalVars vs

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder CaseTerm hd eqs ps -> do

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder mt <- resolve ga hd

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder newEs <- resolveCaseEqs ga eqs

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder recurse $ CaseTerm (maybe hd id mt) newEs ps

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder LetTerm b eqs hd ps -> do

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder newEs <- resolveLetEqs ga eqs

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder mt <- resolve ga hd

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder putLocalVars vs

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder recurse $ LetTerm b newEs (maybe hd id mt) ps

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder TermToken tok -> do

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder let (ds1, trm) = convertMixfixToken (literal_annos ga)

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder (flip ResolvedMixTerm []) TermToken tok

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder addDiags ds1

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder self tt $ oneStep $ case trm of

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder TermToken _ -> (trm, tok)

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

f63170ab2ed53197f50e4575383e7981189c87dcChristian Maeder AsPattern vd p ps -> do

f63170ab2ed53197f50e4575383e7981189c87dcChristian Maeder mp <- resolvePattern ga p

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder recurse $ AsPattern vd (maybe p id mp) ps

8b0bd90bc649e740c134ad0946e0d0409c3c96e6Christian Maeder TypedTerm trm k ty ps -> do

1626d36d680e01037b6ee7ba66925a1d61eebbe9Christian Maeder -- assume that type is analysed

mt <- resolve ga trm

recurse $ TypedTerm (maybe trm id mt) k ty ps

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

-- * equation stuff

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

resolveCaseEq ga (ProgEq p t ps) = do

mp <- resolvePattern ga 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 ga t

putLocalVars vs

return $ case mtt of

Nothing -> Nothing

Just newT -> Just $ ProgEq newP newT ps

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

resolveCaseEqs ga eqs = case eqs of

[] -> return []

eq : rt -> do

mEq <- resolveCaseEq ga eq

reqs <- resolveCaseEqs ga rt

return $ case mEq of

Nothing -> reqs

Just newEq -> newEq : reqs

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

resolveLetEqs _ [] = return []

resolveLetEqs ga eqs = case eqs of

[] -> return []

ProgEq pat trm ps : rt -> do

mPat <- resolvePattern ga pat

case mPat of

Nothing -> do

resolve ga trm

resolveLetEqs ga rt

Just newPat -> do

let bs = extractVars newPat

checkUniqueVars bs

mapM_ (addLocalVar False) bs

mTrm <- resolve ga trm

case mTrm of

Nothing -> resolveLetEqs ga rt

Just newTrm -> do

reqs <- resolveLetEqs ga 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) $ maybe (error "bracketTermToTypes") id $

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

maybe (error "bracketTermToTypes1") id $ mapM termToType tys

_ -> error "bracketTermToTypes2"

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

toMixTerm e i ar qs =

if i == applId then assert (length ar == 2) $

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

else if i == tupleId || i == unitId then

mkTupleTerm ar qs

else 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

resolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)

resolvePattern = resolver True

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

resolve = resolver False

resolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)

resolver isPat ga trm = do

e <- get

let ass = assumps e

vs = localVars e

ps = preIds e

compIds = getCompoundLists e

(addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)

$ Set.union (Map.keysSet ass) $ Map.keysSet vs

chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS

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

(toMixTerm e) chart

addDiags ds

if isPat then case mr of

Nothing -> return mr

Just pat -> fmap Just $ anaPattern sIds pat

else 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 -> if isSimpleToken tok

&& not (Set.member tok ks)

|| tok == uTok then

[(simpleIdToId tok, m2, [tok])] else []

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

-- create fresh type vars for unknown ids tagged with type MixfixType [].

anaPattern :: Set.Set Id -> Term -> State Env Term

anaPattern s pat = case pat of

QualVar vd -> do

newVd <- checkVarDecl vd

return $ QualVar newVd

ResolvedMixTerm i tys pats ps | null pats && null tys &&

(isSimpleId i || i == simpleIdToId uTok) &&

not (Set.member i s) -> do

(tvar, c) <- toEnvState $ freshVar i

return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps

| otherwise -> do

l <- mapM (anaPattern s) pats

return $ ResolvedMixTerm i tys l ps

ApplTerm p1 p2 ps -> do

p3 <- anaPattern s p1

p4 <- anaPattern s p2

return $ ApplTerm p3 p4 ps

TupleTerm pats ps -> do

l <- mapM (anaPattern s) pats

return $ TupleTerm l ps

TypedTerm p q ty ps -> do

case p of

QualVar (VarDecl v (MixfixType []) ok qs) ->

return $ QualVar $ VarDecl v ty ok $ appRange qs ps

_ -> do

newP <- anaPattern s p

return $ TypedTerm newP q ty ps

AsPattern vd p2 ps -> do

newVd <- checkVarDecl vd

p4 <- anaPattern s p2

return $ AsPattern newVd p4 ps

_ -> return pat

where checkVarDecl vd@(VarDecl v t ok ps) = case t of

MixfixType [] -> do

(tvar, c) <- toEnvState $ freshVar v

return $ VarDecl v (TypeName tvar rStar c) ok ps

_ -> return vd