03831d35f7499c87d51205817c93e9a8d42c4baestevel{- |

03831d35f7499c87d51205817c93e9a8d42c4baestevelModule : $Header$

03831d35f7499c87d51205817c93e9a8d42c4baestevelDescription : mixfix analysis for terms

03831d35f7499c87d51205817c93e9a8d42c4baestevelCopyright : (c) Christian Maeder and Uni Bremen 2003-2005

2983dda76a6d296fdb560c88114fe41caad1b84fMichael BergknoffLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff

03831d35f7499c87d51205817c93e9a8d42c4baestevelMaintainer : Christian.Maeder@dfki.de

03831d35f7499c87d51205817c93e9a8d42c4baestevelStability : experimental

03831d35f7499c87d51205817c93e9a8d42c4baestevelPortability : portable

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelMixfix analysis of terms and patterns, type annotations are also analysed

03831d35f7499c87d51205817c93e9a8d42c4baestevel-}

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelmodule HasCASL.MixAna where

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.GlobalAnnotations

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.Result

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.Id

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.DocUtils

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.Earley

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.Lexer

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoffimport Common.Prec

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.ConvertMixfixToken

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.Lib.State

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.AnnoState

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Common.Anno_Parser

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport qualified Data.Map as Map

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport qualified Data.Set as Set

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.As

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.AsUtils

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.PrintAs

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.Unify

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.VarDecl

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.Le

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.HToken

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.ParseTerm

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport HasCASL.TypeAna

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport qualified Text.ParserCombinators.Parsec as P

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Data.Maybe

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Data.List (partition)

03831d35f7499c87d51205817c93e9a8d42c4baestevelimport Control.Exception (assert)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baesteveladdType :: Term -> Term -> Term

03831d35f7499c87d51205817c93e9a8d42c4baesteveladdType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

03831d35f7499c87d51205817c93e9a8d42c4baesteveladdType _ _ = error "addType"

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelisCompoundList :: Set.Set [Id] -> [Term] -> Bool

03831d35f7499c87d51205817c93e9a8d42c4baestevelisCompoundList compIds l =

03831d35f7499c87d51205817c93e9a8d42c4baestevel maybe False (flip Set.member compIds) $ mapM termToId l

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelisTypeList :: Env -> [Term] -> Bool

03831d35f7499c87d51205817c93e9a8d42c4baestevelisTypeList e l = case mapM termToType l of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> False

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just ts ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel let Result ds ml =

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff mapM ( \ t -> anaTypeM (Nothing, t) e) ts

03831d35f7499c87d51205817c93e9a8d42c4baestevel in isJust ml && not (hasErrors ds)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baesteveltermToType :: Term -> Maybe Type

03831d35f7499c87d51205817c93e9a8d42c4baesteveltermToType t =

03831d35f7499c87d51205817c93e9a8d42c4baestevel case P.runParser ((case getPosList t of

03831d35f7499c87d51205817c93e9a8d42c4baestevel [] -> return ()

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

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel Right x -> Just x

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> Nothing

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baesteveltermToId :: Term -> Maybe Id

03831d35f7499c87d51205817c93e9a8d42c4baesteveltermToId t = case P.parse (uninstOpId << P.eof) "" $ showDoc t "" of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Right x -> Just x

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> Nothing

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baesteveliterateCharts :: GlobalAnnos -> Set.Set [Id] -> [Term] -> Chart Term

03831d35f7499c87d51205817c93e9a8d42c4baestevel -> State Env (Chart Term)

03831d35f7499c87d51205817c93e9a8d42c4baesteveliterateCharts ga compIds terms chart =

03831d35f7499c87d51205817c93e9a8d42c4baestevel do e <- get

03831d35f7499c87d51205817c93e9a8d42c4baestevel let self = iterateCharts ga compIds

03831d35f7499c87d51205817c93e9a8d42c4baestevel oneStep = nextChart addType (toMixTerm e) ga chart

03831d35f7499c87d51205817c93e9a8d42c4baestevel vs = localVars e

03831d35f7499c87d51205817c93e9a8d42c4baestevel tm = typeMap e

03831d35f7499c87d51205817c93e9a8d42c4baestevel case terms of

03831d35f7499c87d51205817c93e9a8d42c4baestevel [] -> return chart

03831d35f7499c87d51205817c93e9a8d42c4baestevel t:tt -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel let recurse trm = self tt $

03831d35f7499c87d51205817c93e9a8d42c4baestevel oneStep (trm, exprTok {tokPos = getRange trm})

03831d35f7499c87d51205817c93e9a8d42c4baestevel case t of

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel MixTypeTerm q typ ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel mTyp <- anaStarType typ

03831d35f7499c87d51205817c93e9a8d42c4baestevel case mTyp of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> recurse t

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just nTyp -> self tt $ oneStep

03831d35f7499c87d51205817c93e9a8d42c4baestevel (MixTypeTerm q (monoType nTyp) ps,

03831d35f7499c87d51205817c93e9a8d42c4baestevel typeTok {tokPos = ps})

03831d35f7499c87d51205817c93e9a8d42c4baestevel BracketTerm b ts ps ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel let bres = self (expandPos TermToken

03831d35f7499c87d51205817c93e9a8d42c4baestevel (getBrackets b) ts ps ++ tt) chart

03831d35f7499c87d51205817c93e9a8d42c4baestevel in case (b, ts) of

03831d35f7499c87d51205817c93e9a8d42c4baestevel (Squares, _ : _) ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel if isCompoundList compIds ts then do

03831d35f7499c87d51205817c93e9a8d42c4baestevel addDiags [mkDiag Hint "is compound list" t]

03831d35f7499c87d51205817c93e9a8d42c4baestevel bres

03831d35f7499c87d51205817c93e9a8d42c4baestevel else if isTypeList e ts then do

03831d35f7499c87d51205817c93e9a8d42c4baestevel addDiags [mkDiag Hint "is type list" t]

03831d35f7499c87d51205817c93e9a8d42c4baestevel self tt $ oneStep (t, typeInstTok {tokPos = ps})

03831d35f7499c87d51205817c93e9a8d42c4baestevel else bres

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> bres

03831d35f7499c87d51205817c93e9a8d42c4baestevel QualVar (VarDecl v typ ok ps) -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel mTyp <- anaStarType typ

03831d35f7499c87d51205817c93e9a8d42c4baestevel case mTyp of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> recurse t

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just nType -> recurse $ QualVar $

03831d35f7499c87d51205817c93e9a8d42c4baestevel VarDecl v (monoType nType) ok ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel QualOp b (InstOpId v ts qs) sc ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel mSc <- anaTypeScheme sc

03831d35f7499c87d51205817c93e9a8d42c4baestevel newTs <- anaInstTypes ts

03831d35f7499c87d51205817c93e9a8d42c4baestevel case mSc of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> recurse t

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just nSc -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel case findOpId e v nSc of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> addDiags [mkDiag Error

03831d35f7499c87d51205817c93e9a8d42c4baestevel "operation not found" v]

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> return ()

03831d35f7499c87d51205817c93e9a8d42c4baestevel recurse $ QualOp b (InstOpId v newTs qs) nSc ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel QuantifiedTerm quant decls hd ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel newDs <- mapM (anaddGenVarDecl False) decls

03831d35f7499c87d51205817c93e9a8d42c4baestevel mt <- resolve ga hd

03831d35f7499c87d51205817c93e9a8d42c4baestevel putLocalVars vs

03831d35f7499c87d51205817c93e9a8d42c4baestevel putTypeMap tm

03831d35f7499c87d51205817c93e9a8d42c4baestevel let newT = case mt of Just trm -> trm

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> hd

03831d35f7499c87d51205817c93e9a8d42c4baestevel recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel LambdaTerm decls part hd ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel mDecls <- mapM (resolvePattern ga) decls

03831d35f7499c87d51205817c93e9a8d42c4baestevel let anaDecls = catMaybes mDecls

03831d35f7499c87d51205817c93e9a8d42c4baestevel bs = concatMap extractVars anaDecls

03831d35f7499c87d51205817c93e9a8d42c4baestevel checkUniqueVars bs

03831d35f7499c87d51205817c93e9a8d42c4baestevel mapM_ (addLocalVar False) bs

03831d35f7499c87d51205817c93e9a8d42c4baestevel mt <- resolve ga hd

03831d35f7499c87d51205817c93e9a8d42c4baestevel putLocalVars vs

03831d35f7499c87d51205817c93e9a8d42c4baestevel recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel CaseTerm hd eqs ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel mt <- resolve ga hd

03831d35f7499c87d51205817c93e9a8d42c4baestevel newEs <- resolveCaseEqs ga eqs

03831d35f7499c87d51205817c93e9a8d42c4baestevel recurse $ CaseTerm (maybe hd id mt) newEs ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel LetTerm b eqs hd ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel newEs <- resolveLetEqs ga eqs

03831d35f7499c87d51205817c93e9a8d42c4baestevel mt <- resolve ga hd

03831d35f7499c87d51205817c93e9a8d42c4baestevel putLocalVars vs

03831d35f7499c87d51205817c93e9a8d42c4baestevel recurse $ LetTerm b newEs (maybe hd id mt) ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel TermToken tok -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel let (ds1, trm) = convertMixfixToken

03831d35f7499c87d51205817c93e9a8d42c4baestevel (literal_annos ga)

03831d35f7499c87d51205817c93e9a8d42c4baestevel (flip ResolvedMixTerm [])

03831d35f7499c87d51205817c93e9a8d42c4baestevel TermToken tok

03831d35f7499c87d51205817c93e9a8d42c4baestevel addDiags ds1

03831d35f7499c87d51205817c93e9a8d42c4baestevel self tt $ oneStep $

03831d35f7499c87d51205817c93e9a8d42c4baestevel case trm of

03831d35f7499c87d51205817c93e9a8d42c4baestevel TermToken _ -> (trm, tok)

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> (trm, exprTok

03831d35f7499c87d51205817c93e9a8d42c4baestevel {tokPos = tokPos tok})

03831d35f7499c87d51205817c93e9a8d42c4baestevel AsPattern vd p ps -> do

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff mp <- resolvePattern ga p

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff let newP = case mp of Just pat -> pat

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> p

03831d35f7499c87d51205817c93e9a8d42c4baestevel recurse $ AsPattern vd newP ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel TypedTerm trm k ty ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel -- assume that type is analysed

03831d35f7499c87d51205817c93e9a8d42c4baestevel mt <- resolve ga trm

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

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevel-- * equation stuff

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveCaseEq ga (ProgEq p t ps) =

03831d35f7499c87d51205817c93e9a8d42c4baestevel do mp <- resolvePattern ga p

03831d35f7499c87d51205817c93e9a8d42c4baestevel case mp of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> return Nothing

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just newP -> do

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff let bs = extractVars newP

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff checkUniqueVars bs

03831d35f7499c87d51205817c93e9a8d42c4baestevel vs <- gets localVars

03831d35f7499c87d51205817c93e9a8d42c4baestevel mapM_ (addLocalVar False) bs

03831d35f7499c87d51205817c93e9a8d42c4baestevel mtt <- resolve ga t

03831d35f7499c87d51205817c93e9a8d42c4baestevel putLocalVars vs

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ case mtt of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> Nothing

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just newT -> Just $ ProgEq newP newT ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveCaseEqs _ [] = return []

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveCaseEqs ga (eq : rt) =

03831d35f7499c87d51205817c93e9a8d42c4baestevel do mEq <- resolveCaseEq ga eq

03831d35f7499c87d51205817c93e9a8d42c4baestevel eqs <- resolveCaseEqs ga rt

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ case mEq of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> eqs

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just newEq -> newEq : eqs

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveLetEqs _ [] = return []

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolveLetEqs ga (ProgEq pat trm ps : rt) =

03831d35f7499c87d51205817c93e9a8d42c4baestevel do mPat <- resolvePattern ga pat

03831d35f7499c87d51205817c93e9a8d42c4baestevel case mPat of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> do resolve ga trm

03831d35f7499c87d51205817c93e9a8d42c4baestevel resolveLetEqs ga rt

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just newPat -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel let bs = extractVars newPat

03831d35f7499c87d51205817c93e9a8d42c4baestevel checkUniqueVars bs

03831d35f7499c87d51205817c93e9a8d42c4baestevel mapM_ (addLocalVar False) bs

03831d35f7499c87d51205817c93e9a8d42c4baestevel mTrm <- resolve ga trm

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff case mTrm of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> resolveLetEqs ga rt

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just newTrm -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel eqs <- resolveLetEqs ga rt

03831d35f7499c87d51205817c93e9a8d42c4baestevel return (ProgEq newPat newTrm ps : eqs)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelmkPatAppl :: Term -> Term -> Range -> Term

03831d35f7499c87d51205817c93e9a8d42c4baestevelmkPatAppl op arg qs =

03831d35f7499c87d51205817c93e9a8d42c4baestevel case op of

03831d35f7499c87d51205817c93e9a8d42c4baestevel QualVar (VarDecl i (MixfixType []) _ _) ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel ResolvedMixTerm i [] [arg] qs

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> ApplTerm op arg qs

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelbracketTermToTypes :: Env -> Term -> [Type]

03831d35f7499c87d51205817c93e9a8d42c4baestevelbracketTermToTypes e t = case t of

03831d35f7499c87d51205817c93e9a8d42c4baestevel BracketTerm Squares tys _ ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel map (monoType . snd) $ maybe (error "bracketTermToTypes") id $

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

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> error "bracketTermToTypes2"

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baesteveltoMixTerm :: Env -> Id -> [Term] -> Range -> Term

03831d35f7499c87d51205817c93e9a8d42c4baesteveltoMixTerm e i ar qs =

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

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

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel mkTupleTerm ar qs

03831d35f7499c87d51205817c93e9a8d42c4baestevel else case unPolyId i of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just j@(Id ts [] ps) ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel if isMixfix j && isSingle ar then

03831d35f7499c87d51205817c93e9a8d42c4baestevel ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs

03831d35f7499c87d51205817c93e9a8d42c4baestevel else assert (length ar == 1 + placeCount j) $

03831d35f7499c87d51205817c93e9a8d42c4baestevel let (toks, _) = splitMixToken ts

03831d35f7499c87d51205817c93e9a8d42c4baestevel (far, tar : sar) =

03831d35f7499c87d51205817c93e9a8d42c4baestevel splitAt (placeCount $ Id toks [] ps) ar

03831d35f7499c87d51205817c93e9a8d42c4baestevel in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> ResolvedMixTerm i [] ar qs

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetKnowns :: Id -> Set.Set Token

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetKnowns (Id ts cs _) = Set.union (Set.fromList ts) $

03831d35f7499c87d51205817c93e9a8d42c4baestevel Set.unions (map getKnowns cs)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolvePattern = resolver True

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolve = resolver False

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)

03831d35f7499c87d51205817c93e9a8d42c4baestevelresolver isPat ga trm =

03831d35f7499c87d51205817c93e9a8d42c4baestevel do e <- get

03831d35f7499c87d51205817c93e9a8d42c4baestevel let ass = assumps e

03831d35f7499c87d51205817c93e9a8d42c4baestevel vs = localVars e

03831d35f7499c87d51205817c93e9a8d42c4baestevel ps = preIds e

03831d35f7499c87d51205817c93e9a8d42c4baestevel compIds = getCompoundLists e

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

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

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel let Result ds mr = getResolved

03831d35f7499c87d51205817c93e9a8d42c4baestevel (showDoc . parenTerm) (getRange trm)

03831d35f7499c87d51205817c93e9a8d42c4baestevel (toMixTerm e) chart

03831d35f7499c87d51205817c93e9a8d42c4baestevel addDiags ds

03831d35f7499c87d51205817c93e9a8d42c4baestevel if isPat then case mr of

03831d35f7499c87d51205817c93e9a8d42c4baestevel Nothing -> return mr

03831d35f7499c87d51205817c93e9a8d42c4baestevel Just pat -> fmap Just $ anaPattern sIds pat

03831d35f7499c87d51205817c93e9a8d42c4baestevel else return mr

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetPolyIds :: Assumps -> Set.Set Id

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetPolyIds = Set.unions . map ( \ (i, OpInfos l) ->

03831d35f7499c87d51205817c93e9a8d42c4baestevel foldr ( \ oi s -> case opType oi of

03831d35f7499c87d51205817c93e9a8d42c4baestevel TypeScheme (_ : _) _ _ -> Set.insert i s

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> s) Set.empty l) . Map.toList .

03831d35f7499c87d51205817c93e9a8d42c4baestevel Map.filterWithKey ( \ (Id _ cs _) _ -> null cs)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetCompound :: Id -> [Id]

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetCompound (Id _ cs _) = cs

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetCompoundLists :: Env -> Set.Set [Id]

03831d35f7499c87d51205817c93e9a8d42c4baestevelgetCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff (Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff

03831d35f7499c87d51205817c93e9a8d42c4baesteveluTok :: Token

03831d35f7499c87d51205817c93e9a8d42c4baesteveluTok = mkSimpleId "_"

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelbuiltinIds :: [Id]

03831d35f7499c87d51205817c93e9a8d42c4baestevelbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelmakeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id

03831d35f7499c87d51205817c93e9a8d42c4baestevel -> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)

03831d35f7499c87d51205817c93e9a8d42c4baestevelmakeRules ga ps@(p, _) polyIds aIds =

03831d35f7499c87d51205817c93e9a8d42c4baestevel let (sIds, ids) = Set.partition isSimpleId aIds

03831d35f7499c87d51205817c93e9a8d42c4baestevel ks = Set.fold (Set.union . getKnowns) Set.empty ids

03831d35f7499c87d51205817c93e9a8d42c4baestevel rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks

03831d35f7499c87d51205817c93e9a8d42c4baestevel m2 = maxWeight p + 2

03831d35f7499c87d51205817c93e9a8d42c4baestevel in ( \ tok -> if isSimpleToken tok

03831d35f7499c87d51205817c93e9a8d42c4baestevel && not (Set.member tok ks)

03831d35f7499c87d51205817c93e9a8d42c4baestevel || tok == uTok then

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel , partitionRules $ listRules m2 ga ++

03831d35f7499c87d51205817c93e9a8d42c4baestevel initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)

03831d35f7499c87d51205817c93e9a8d42c4baestevel , sIds)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]

03831d35f7499c87d51205817c93e9a8d42c4baestevelinitRules (p, ps) polyIds bs is =

03831d35f7499c87d51205817c93e9a8d42c4baestevel map ( \ i -> mixRule (getIdPrec p ps i) i)

03831d35f7499c87d51205817c93e9a8d42c4baestevel (bs ++ is) ++

03831d35f7499c87d51205817c93e9a8d42c4baestevel map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))

03831d35f7499c87d51205817c93e9a8d42c4baestevel (filter isMixfix is) ++

03831d35f7499c87d51205817c93e9a8d42c4baestevel-- identifiers with a positive number of type arguments

03831d35f7499c87d51205817c93e9a8d42c4baestevel map ( \ i -> let j = polyId i in

03831d35f7499c87d51205817c93e9a8d42c4baestevel (j, getIdPrec p ps i, getTokenPlaceList j)) polyIds ++

03831d35f7499c87d51205817c93e9a8d42c4baestevel map ( \ i -> let j = polyId i in

03831d35f7499c87d51205817c93e9a8d42c4baestevel (protect j, maxWeight p + 3, getPlainTokenList j))

03831d35f7499c87d51205817c93e9a8d42c4baestevel (filter isMixfix polyIds)

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelpolyId :: Id -> Id

03831d35f7499c87d51205817c93e9a8d42c4baestevelpolyId (Id ts _ ps) = let (toks, pls) = splitMixToken ts in

03831d35f7499c87d51205817c93e9a8d42c4baestevel Id (toks ++ [typeInstTok] ++ pls) [] ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel

03831d35f7499c87d51205817c93e9a8d42c4baestevelunPolyId :: Id -> Maybe Id

03831d35f7499c87d51205817c93e9a8d42c4baestevelunPolyId (Id ts cs ps) = let (ft, rt) = partition (== typeInstTok) ts in

03831d35f7499c87d51205817c93e9a8d42c4baestevel case ft of

03831d35f7499c87d51205817c93e9a8d42c4baestevel [_] -> Just $ Id rt cs ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> Nothing

03831d35f7499c87d51205817c93e9a8d42c4baestevel

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

03831d35f7499c87d51205817c93e9a8d42c4baestevelanaPattern :: Set.Set Id -> Pattern -> State Env Pattern

03831d35f7499c87d51205817c93e9a8d42c4baestevelanaPattern s pat = case pat of

03831d35f7499c87d51205817c93e9a8d42c4baestevel QualVar vd -> do newVd <- checkVarDecl vd

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ QualVar newVd

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

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

2983dda76a6d296fdb560c88114fe41caad1b84fMichael Bergknoff not (Set.member i s) -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel (tvar, c) <- toEnvState $ freshVar $ posOfId i

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel | otherwise -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel l <- mapM (anaPattern s) pats

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ ResolvedMixTerm i tys l ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel ApplTerm p1 p2 ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel p3 <- anaPattern s p1

03831d35f7499c87d51205817c93e9a8d42c4baestevel p4 <- anaPattern s p2

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ ApplTerm p3 p4 ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel TupleTerm pats ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel l <- mapM (anaPattern s) pats

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ TupleTerm l ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel TypedTerm p q ty ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel case p of

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel let newVd = VarDecl v ty ok (qs `appRange` ps) in

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ QualVar newVd

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> do newP <- anaPattern s p

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ TypedTerm newP q ty ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel AsPattern vd p2 ps -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel newVd <- checkVarDecl vd

03831d35f7499c87d51205817c93e9a8d42c4baestevel p4 <- anaPattern s p2

03831d35f7499c87d51205817c93e9a8d42c4baestevel return $ AsPattern newVd p4 ps

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> return pat

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel MixfixType [] -> do

03831d35f7499c87d51205817c93e9a8d42c4baestevel (tvar, c) <- toEnvState $ freshVar $ posOfId v

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

03831d35f7499c87d51205817c93e9a8d42c4baestevel _ -> return vd

03831d35f7499c87d51205817c93e9a8d42c4baestevel