c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : $Header$

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederDescription : mixfix analysis for terms

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederMaintainer : Christian.Maeder@dfki.de

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability : experimental

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederPortability : portable

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule HasCASL.MixAna

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder ( resolve

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder , anaPolyId

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , makeRules

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , getPolyIds

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , iterateCharts

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder , toMixTerm

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , uTok

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder ) where

fb50920e621bfc152c19147cb52077ff06b3526bChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.AnnoParser

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.AnnoState

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.ConvertMixfixToken

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.DocUtils

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Earley

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.GlobalAnnotations

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Id

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Lib.State

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.Parsec

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.Prec

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Common.Result

b5699d97a9e2b4496f98d624f4b0a537986651c3Christian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maederimport qualified Data.Map as Map

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport qualified Data.Set as Set

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport HasCASL.As

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport HasCASL.AsUtils

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport HasCASL.PrintAs

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport HasCASL.VarDecl

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport HasCASL.Le

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport HasCASL.ParseTerm

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport HasCASL.TypeAna

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport qualified Text.ParserCombinators.Parsec as P

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maederimport Data.Maybe

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Control.Exception (assert)

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maederimport Control.Monad

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder

04dada28736b4a237745e92063d8bdd49a362debChristian MaederaddType :: Term -> Term -> Term

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederaddType _ _ = error "addType"

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder-- | try to reparse terms as a compound list

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian MaederisCompoundList :: Set.Set [Id] -> [Term] -> Bool

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederisCompoundList compIds =

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

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederisTypeList :: Env -> [Term] -> Bool

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederisTypeList e l = case mapM termToType l of

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Nothing -> False

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Just ts ->

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder in isJust ml && not (hasErrors ds)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaedertermToType :: Term -> Maybe Type

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaedertermToType t = case P.runParser ((case getPosList t of

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder [] -> return ()

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder p : _ -> P.setPosition $ fromPos p)

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Right x -> Just x

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder _ -> Nothing

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder mSc <- anaTypeScheme sc

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder case mSc of

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Nothing -> return Nothing

4c4a6faea90bdb95062434ca9b9e85f5c3b2d012Christian Maeder Just newSc@(TypeScheme tvars _ _) -> do

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder e <- get

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder let ids = Set.unions

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder [ Map.keysSet $ classMap e

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , Map.keysSet $ typeMap e

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder , Map.keysSet $ assumps e ]

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder addDiags $ map (mkDiag Warning

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder "unexpected identifier in compound list") es

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder unless (null cs || null tvars)

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

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder return $ Just newSc

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederresolveQualOp i@(PolyId j _ _) sc = do

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder mSc <- anaPolyId i sc

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder e <- get

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder case mSc of

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Nothing -> return sc -- and previous

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Just nSc -> do

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder when (Set.null $ Set.filter ((== nSc) . opType)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder $ Map.findWithDefault Set.empty j $ assumps e)

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder $ addDiags [mkDiag Error "operation not found" j]

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder return nSc

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian MaederiterateCharts :: GlobalAnnos -> Set.Set Id -> Set.Set [Id] -> [Term]

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

da245da15da78363c896e44ea97a14ab1f83eb50Christian MaederiterateCharts ga sIds compIds terms chart = do

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder e <- get

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder let self = iterateCharts ga sIds compIds

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder oneStep = nextChart addType (toMixTerm e) ga chart

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder vs = localVars e

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder tm = typeMap e

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder case terms of

462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder [] -> return chart

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

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder MixfixTerm ts -> self (ts ++ tt) chart

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder MixTypeTerm q typ ps -> do

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder mTyp <- anaStarType typ

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder case mTyp of

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder Nothing -> recurse t

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder Just nTyp -> self tt $ oneStep

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder BracketTerm b ts ps ->

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder let bres = self (expandPos TermToken

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder (Squares, _ : _) -> if isCompoundList compIds ts then do

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder addDiags [mkDiag Hint "is compound list" t]

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder bres

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder else if isTypeList e ts then do

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder if null $ solveDiags testChart then do

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder addDiags [mkDiag Hint "is type list" t]

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder self tt testChart

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder else bres

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder else bres

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

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

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder addDiags [mkDiag Hint "is type list" ts2]

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder nSc <- resolveQualOp v sc

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder self rtt $ oneStep

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder ( QualOp b2 v nSc (bracketTermToTypes e hd) UserGiven ps2

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder , exprTok {tokPos = appRange ps ps3})

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder _ -> bres

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mTyp <- anaStarType typ

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder ok ps) mTyp

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder QualOp b v sc [] k ps -> do

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder nSc <- resolveQualOp v sc

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder recurse $ QualOp b v nSc [] k ps

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder QuantifiedTerm quant decls hd ps -> do

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder newDs <- mapM (anaddGenVarDecl False) decls

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mt <- resolve hd

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder putLocalVars vs

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder putTypeMap tm

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder LambdaTerm decls part hd ps -> do

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mDecls <- mapM resolve decls

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder let anaDecls = catMaybes mDecls

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder bs = concatMap extractVars anaDecls

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder checkUniqueVars bs

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mapM_ (addLocalVar False) bs

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mt <- resolve hd

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder putLocalVars vs

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder recurse $ LambdaTerm anaDecls part (fromMaybe hd mt) ps

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder CaseTerm hd eqs ps -> do

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder mt <- resolve hd

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder newEs <- resolveCaseEqs eqs

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder recurse $ CaseTerm (fromMaybe hd mt) newEs ps

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder LetTerm b eqs hd ps -> do

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder newEs <- resolveLetEqs eqs

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder mt <- resolve hd

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder putLocalVars vs

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder recurse $ LetTerm b newEs (fromMaybe hd mt) ps

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder TermToken tok -> do

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

b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder (flip ResolvedMixTerm []) TermToken tok

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder addDiags ds1

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder self tt $ oneStep $ case trm of

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder TermToken _ -> (trm, tok)

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

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder AsPattern vd p ps -> do

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder mp <- resolve p

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder recurse $ AsPattern vd (fromMaybe p mp) ps

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder TypedTerm trm k ty ps -> do

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder -- assume that type is analysed

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder mt <- resolve trm

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder recurse $ TypedTerm (fromMaybe trm mt) k ty ps

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

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder-- * equation stuff

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederresolveCaseEq :: ProgEq -> State Env (Maybe ProgEq)

c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederresolveCaseEq (ProgEq p t ps) = do

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder mp <- resolve p

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder case mp of

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder Nothing -> return Nothing

c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder 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)