ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |

ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederDescription : mixfix analysis for terms

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

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder-}

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedermodule HasCASL.MixAna

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder ( resolve

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , anaPolyId

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , makeRules

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , getPolyIds

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , iterateCharts

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder , toMixTerm

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder ) where

ca010363454de207082dfaa4b753531ce2a34551Christian Maeder

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.GlobalAnnotations

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.Result

ca010363454de207082dfaa4b753531ce2a34551Christian Maederimport Common.Id

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport Common.DocUtils

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Earley

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Common.Lexer

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Prec

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.ConvertMixfixToken

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.Lib.State

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Common.AnnoState

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maederimport Common.Anno_Parser

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maederimport qualified Data.Map as Map

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport HasCASL.As

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport HasCASL.AsUtils

028f19cdb09d52bb2fd207399b6fa874540d1670Christian Maederimport HasCASL.PrintAs

975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport HasCASL.Unify

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport HasCASL.VarDecl

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport HasCASL.Le

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport HasCASL.ParseTerm

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport HasCASL.TypeAna

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport qualified Text.ParserCombinators.Parsec as P

fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder

83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport Data.Maybe

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederimport Control.Exception (assert)

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder-- | try to reparse terms as a compound list

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

0a39036fa485579a7b7c81cdd44a412392571927Christian MaederisCompoundList compIds =

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederisTypeList :: Env -> [Term] -> Bool

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisTypeList e l = case mapM termToType l of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> False

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just ts ->

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

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in isJust ml && not (hasErrors ds)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToType :: Term -> Maybe Type

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedertermToType t = case P.runParser ((case getPosList t of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return ()

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder p : _ -> P.setPosition $ fromPos p)

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Right x -> Just x

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> Nothing

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder mSc <- anaTypeScheme sc

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder case mSc of

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder Nothing -> return Nothing

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

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder e <- get

c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder let ids = Set.unions

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder [ Map.keysSet $ classMap e

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Map.keysSet $ typeMap e

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder , Map.keysSet $ assumps e ]

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

c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder addDiags $ map (\ j -> mkDiag Warning

c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder "unexpected identifier in compound list" j) es

c2c1ca07d7f3c2228b66599a7fb37b90fe6fb3bcChristian Maeder if null cs || null tvars then return () else

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

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder return $ Just newSc

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaederresolveQualOp i@(PolyId j _ _) sc = do

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder mSc <- anaPolyId i sc

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder e <- get

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder case mSc of

c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder Nothing -> return sc -- and previous

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder Just nSc -> do

c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder if Set.null $ Set.filter ((== nSc) . opType)

c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder $ Map.findWithDefault Set.empty j $ assumps e

c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder then addDiags [mkDiag Error "operation not found" j]

c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder else return ()

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder return nSc

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -> State Env (Chart Term)

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederiterateCharts ga compIds terms chart = do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder e <- get

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let self = iterateCharts ga compIds

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder oneStep = nextChart addType (toMixTerm e) ga chart

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder vs = localVars e

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder tm = typeMap e

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case terms of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return chart

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder t : tt -> let recurse trm = self tt $ oneStep

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (trm, exprTok {tokPos = getRange trm}) in case t of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder MixTypeTerm q typ ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mTyp <- anaStarType typ

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mTyp of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> recurse t

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just nTyp -> self tt $ oneStep

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (MixTypeTerm q (monoType nTyp) ps, typeTok {tokPos = ps})

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder BracketTerm b ts ps ->

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bres = self (expandPos TermToken

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (getBrackets b) ts ps ++ tt) chart in case (b, ts) of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (Squares, _ : _) -> if isCompoundList compIds ts then do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags [mkDiag Hint "is compound list" t]

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder bres

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else if isTypeList e ts then do

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

639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder if null $ solveDiags testChart then do

639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder addDiags [mkDiag Hint "is type list" t]

639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder self tt testChart

639732746d7c3a586790043b452a4cbdd29a3fc3Christian Maeder else bres

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else bres

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

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

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

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder addDiags [mkDiag Hint "is type list" ts2]

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder nSc <- resolveQualOp v sc

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder self rtt $ oneStep

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder ( QualOp b2 v nSc (bracketTermToTypes e hd) UserGiven ps2

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

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder _ -> bres

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

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mTyp <- anaStarType typ

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder recurse $ maybe t ( \ nType -> QualVar $ VarDecl v (monoType nType)

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ok ps) mTyp

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

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder nSc <- resolveQualOp v sc

6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder recurse $ QualOp b v nSc [] k ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QuantifiedTerm quant decls hd ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newDs <- mapM (anaddGenVarDecl False) decls

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga hd

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putTypeMap tm

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) (maybe hd id mt) ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LambdaTerm decls part hd ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mDecls <- mapM (resolvePattern ga) decls

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let anaDecls = catMaybes mDecls

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder bs = concatMap extractVars anaDecls

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga hd

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder CaseTerm hd eqs ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga hd

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newEs <- resolveCaseEqs ga eqs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ CaseTerm (maybe hd id mt) newEs ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder LetTerm b eqs hd ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newEs <- resolveLetEqs ga eqs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga hd

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ LetTerm b newEs (maybe hd id mt) ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermToken tok -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let (ds1, trm) = convertMixfixToken (literal_annos ga)

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (flip ResolvedMixTerm []) TermToken tok

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags ds1

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder self tt $ oneStep $ case trm of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TermToken _ -> (trm, tok)

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

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder AsPattern vd p ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mp <- resolvePattern ga p

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder recurse $ AsPattern vd (maybe p id mp) ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TypedTerm trm k ty ps -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder -- assume that type is analysed

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mt <- resolve ga trm

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

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

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- * equation stuff

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederresolveCaseEq ga (ProgEq p t ps) = do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mp <- resolvePattern ga p

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mp of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> return Nothing

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newP -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bs = extractVars newP

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder vs <- gets localVars

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mtt <- resolve ga t

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder putLocalVars vs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ case mtt of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> Nothing

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newT -> Just $ ProgEq newP newT ps

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederresolveCaseEqs ga eqs = case eqs of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder eq : rt -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mEq <- resolveCaseEq ga eq

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder reqs <- resolveCaseEqs ga rt

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ case mEq of

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Nothing -> reqs

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder Just newEq -> newEq : reqs

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederresolveLetEqs ga eqs = case eqs of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder [] -> return []

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ProgEq pat trm ps : rt -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mPat <- resolvePattern ga pat

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mPat of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder resolve ga trm

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder resolveLetEqs ga rt

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newPat -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let bs = extractVars newPat

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder checkUniqueVars bs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mapM_ (addLocalVar False) bs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder mTrm <- resolve ga trm

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder case mTrm of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> resolveLetEqs ga rt

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just newTrm -> do

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder reqs <- resolveLetEqs ga rt

d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder return $ ProgEq newPat newTrm ps : reqs

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkPatAppl :: Term -> Term -> Range -> Term

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedermkPatAppl op arg qs = case op of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar (VarDecl i (MixfixType []) _ _) -> ResolvedMixTerm i [] [arg] qs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> ApplTerm op arg qs

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederbracketTermToTypes :: Env -> Term -> [Type]

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederbracketTermToTypes e t = case t of

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder BracketTerm Squares tys _ ->

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder map (monoType . snd) $ maybe (error "bracketTermToTypes") id $

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

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder maybe (error "bracketTermToTypes1") id $ mapM termToType tys

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder _ -> error "bracketTermToTypes2"

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaedertoMixTerm :: Env -> Id -> [Term] -> Range -> Term

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaedertoMixTerm e i ar qs =

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

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs

909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else if i == tupleId || i == unitId then

f8a03685d9184046e88e1d76aabdab4f714db440Christian Maeder mkTupleTerm ar qs

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else case unPolyId i of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just j@(Id ts _ _) -> if isMixfix j && isSingle ar then

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else assert (length ar == 1 + placeCount j) $

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let (far, tar : sar) =

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder splitAt (placeCount $ mkId $ fst $ splitMixToken ts) ar

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> ResolvedMixTerm i [] ar qs

fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns :: Id -> Set.Set Token

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaedergetKnowns (Id ts cs _) =

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Set.union (Set.fromList ts) $ Set.unions $ map getKnowns cs

46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder

d1012ae182d765c4e6986029d210b9e7b48de205Christian MaederresolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederresolvePattern = resolver True

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder

13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolve = resolver False

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maederresolver isPat _ga trm = do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder e <- get

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder let ass = assumps e

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder ga = globAnnos e

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder (addRule, ruleS, sIds) = makeRules ga (preIds e) (getPolyIds ass)

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ Set.union (Map.keysSet $ binders e)

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ Set.union (Map.keysSet ass)

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ Map.keysSet $ localVars e

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder chart <- iterateCharts ga (getCompoundLists e) [trm]

b734b51e16ca659814c11205dfb0e97d13bf7ef6Christian Maeder $ initChart addRule ruleS

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

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder (toMixTerm e) chart

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder addDiags ds

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder if isPat then case mr of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Nothing -> return mr

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Just pat -> fmap Just $ anaPattern sIds pat

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else return mr

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetPolyIds :: Assumps -> Set.Set Id

ad187062b0009820118c1b773a232e29b879a2faChristian MaedergetPolyIds = Set.unions . map ( \ (i, s) ->

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder Set.fold ( \ oi -> case opType oi of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder TypeScheme (_ : _) _ _ -> Set.insert i

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> id) Set.empty s) . Map.toList

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederuTok :: Token

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederuTok = mkSimpleId "_"

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder

13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]

13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermakeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder -> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedermakeRules ga ps@(p, _) polyIds aIds =

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder let (sIds, ids) = Set.partition isSimpleId aIds

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ks = Set.fold (Set.union . getKnowns) Set.empty ids

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder m2 = maxWeight p + 2

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder in ( \ tok -> if isSimpleToken tok

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder && not (Set.member tok ks)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder || tok == uTok then

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , partitionRules $ listRules m2 ga ++

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder , sIds)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederinitRules (p, ps) polyIds bs is =

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder map ( \ i -> mixRule (getIdPrec p ps i) i)

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (bs ++ is) ++

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (filter isMixfix is) ++

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder-- identifiers with a positive number of type arguments

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder map ( \ i -> ( polyId i, getIdPrec p ps i

f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder , getPolyTokenList i)) polyIds ++

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder map ( \ i -> ( protect $ polyId i, maxWeight p + 3

f1ef1c750f805c1732b01001f2b157c0077b808eChristian Maeder , getPlainPolyTokenList i)) (filter isMixfix polyIds)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

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

d1012ae182d765c4e6986029d210b9e7b48de205Christian MaederanaPattern :: Set.Set Id -> Term -> State Env Term

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederanaPattern s pat = case pat of

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder QualVar vd -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newVd <- checkVarDecl vd

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ QualVar newVd

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm i tys pats ps | null pats && null tys &&

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (isSimpleId i || i == simpleIdToId uTok) &&

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder not (Set.member i s) -> do

ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder (tvar, c) <- toEnvState $ freshVar i

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder | otherwise -> do

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder l <- mapM (anaPattern s) pats

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder return $ ResolvedMixTerm i tys l ps

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ApplTerm p1 p2 ps -> do

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder p3 <- anaPattern s p1

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder p4 <- anaPattern s p2

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ ApplTerm p3 p4 ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TupleTerm pats ps -> do

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder l <- mapM (anaPattern s) pats

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ TupleTerm l ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TypedTerm p q ty ps -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case p of

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

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ QualVar $ VarDecl v ty ok $ appRange qs ps

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> do

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder newP <- anaPattern s p

4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder return $ TypedTerm newP q ty ps

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder AsPattern vd p2 ps -> do

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder newVd <- checkVarDecl vd

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder p4 <- anaPattern s p2

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ AsPattern newVd p4 ps

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return pat

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder MixfixType [] -> do

ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder (tvar, c) <- toEnvState $ freshVar v

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return vd