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

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maedermodule HasCASL.MixAna 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.HToken

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 Data.List (partition)

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

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

da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederisCompoundList compIds l =

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder maybe False (flip Set.member compIds) $ mapM termToId l

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

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

962036a37b92afb04ac0725cde9f20e599c04c5fChristian MaederisTypeList e l = case mapM termToType l of

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Nothing -> False

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Just ts ->

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let Result ds ml =

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder mapM ( \ t -> anaTypeM (Nothing, t) e) ts

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in isJust ml && not (hasErrors ds)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToType :: Term -> Maybe Type

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToType t =

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder case P.runParser ((case getPosList t of

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder [] -> return ()

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder p : _ -> P.setPosition $ fromPos p)

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Right x -> Just x

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> Nothing

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToId :: Term -> Maybe Id

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedertermToId t = case P.parse (uninstOpId << P.eof) "" $ showDoc t "" of

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Right x -> Just x

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> Nothing

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -> State Env (Chart Term)

da2b959c50c95309d8eb8b24174249c2847e74b5Christian MaederiterateCharts ga compIds terms chart =

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do e <- get

da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder let self = iterateCharts ga compIds

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder oneStep = nextChart addType (toMixTerm e) ga chart

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder vs = localVars e

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder tm = typeMap e

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case terms of

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder [] -> return chart

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder t:tt -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let recurse trm = self tt $

d48085f765fca838c1d972d2123601997174583dChristian Maeder oneStep (trm, exprTok {tokPos = getRange trm})

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder case t of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder MixTypeTerm q typ ps -> do

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTyp <- anaStarType typ

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case mTyp of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> recurse t

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just nTyp -> self tt $ oneStep

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (MixTypeTerm q (monoType nTyp) ps,

b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maeder typeTok {tokPos = ps})

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder BracketTerm b ts ps ->

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let bres = self (expandPos TermToken

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (getBrackets b) ts ps ++ tt) chart

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder in case (b, ts) of

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (Squares, _ : _) ->

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder if isCompoundList compIds ts then do

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder addDiags [mkDiag Hint "is compound list" t]

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder bres

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder else if isTypeList e ts then do

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder addDiags [mkDiag Hint "is type list" t]

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder self tt $ oneStep (t, typeInstTok {tokPos = ps})

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder else bres

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> bres

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

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTyp <- anaStarType typ

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case mTyp of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> recurse t

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just nType -> recurse $ QualVar $

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder VarDecl v (monoType nType) ok ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualOp b (InstOpId v ts qs) sc ps -> do

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mSc <- anaTypeScheme sc

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder newTs <- anaInstTypes ts

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case mSc of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> recurse t

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just nSc -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case findOpId e v nSc of

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Nothing -> addDiags [mkDiag Error

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder "operation not found" v]

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> return ()

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder recurse $ QualOp b (InstOpId v newTs qs) nSc ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QuantifiedTerm quant decls hd ps -> do

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder newDs <- mapM (anaddGenVarDecl False) decls

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mt <- resolve ga hd

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder putLocalVars vs

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder putTypeMap tm

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let newT = case mt of Just trm -> trm

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> hd

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder LambdaTerm decls part hd ps -> do

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mDecls <- mapM (resolvePattern ga) decls

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let anaDecls = catMaybes mDecls

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder bs = concatMap extractVars anaDecls

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder checkUniqueVars bs

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mapM_ (addLocalVar False) bs

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mt <- resolve ga hd

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder CaseTerm hd eqs ps -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder mt <- resolve ga hd

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder newEs <- resolveCaseEqs ga eqs

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ CaseTerm (maybe hd id mt) newEs ps

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder LetTerm b eqs hd ps -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder newEs <- resolveLetEqs ga eqs

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder mt <- resolve ga hd

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder recurse $ LetTerm b newEs (maybe hd id mt) ps

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TermToken tok -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let (ds1, trm) = convertMixfixToken

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (literal_annos ga)

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder (flip ResolvedMixTerm [])

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder TermToken tok

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder addDiags ds1

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder self tt $ oneStep $

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case trm of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TermToken _ -> (trm, tok)

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder _ -> (trm, exprTok

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder {tokPos = tokPos tok})

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder AsPattern vd p ps -> do

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mp <- resolvePattern ga p

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let newP = case mp of Just pat -> pat

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> p

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder recurse $ AsPattern vd newP ps

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder TypedTerm trm k ty ps -> do

3f7009c892b16d172314abbba83d663fa0d87a65Christian Maeder -- assume that type is analysed

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mt <- resolve ga trm

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

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

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- * equation stuff

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

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEq ga (ProgEq p t ps) =

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mp <- resolvePattern ga p

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case mp of

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder Nothing -> return Nothing

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just newP -> do

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let bs = extractVars newP

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder checkUniqueVars bs

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder vs <- gets localVars

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mapM_ (addLocalVar False) bs

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mtt <- resolve ga t

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder putLocalVars vs

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder return $ case mtt of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> Nothing

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Just newT -> Just $ ProgEq newP newT ps

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder

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

53301de22afd7190981b363b57c48df86fcb50f7Christian MaederresolveCaseEqs _ [] = return []

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveCaseEqs ga (eq : rt) =

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do mEq <- resolveCaseEq ga eq

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder eqs <- resolveCaseEqs ga rt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder return $ case mEq of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> eqs

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Just newEq -> newEq : eqs

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder

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

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =

13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mPat <- resolvePattern ga pat

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder case mPat of

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder Nothing -> do resolve ga trm

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder resolveLetEqs ga rt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just newPat -> do

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder let bs = extractVars newPat

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder checkUniqueVars bs

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder mapM_ (addLocalVar False) bs

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTrm <- resolve ga trm

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder case mTrm of

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Nothing -> resolveLetEqs ga rt

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Just newTrm -> do

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder eqs <- resolveLetEqs ga rt

2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder return (ProgEq newPat newTrm ps : eqs)

669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian Maeder

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

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedermkPatAppl op arg qs =

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder case op of

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder ResolvedMixTerm i [] [arg] qs

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Just j@(Id ts [] ps) ->

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder if isMixfix j && isSingle ar then

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder else assert (length ar == 1 + placeCount j) $

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let (toks, _) = splitMixToken ts

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder (far, tar : sar) =

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder splitAt (placeCount $ Id toks [] ps) ar

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs

09249711700a6acbc40a2e337688b434d7aafa28Christian Maeder _ -> ResolvedMixTerm i [] ar qs

fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns :: Id -> Set.Set Token

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList ts) $

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Set.unions (map getKnowns cs)

46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder

975642b989852fc24119c59cf40bc1af653608ffChristian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)

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)

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver isPat ga trm =

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder do e <- get

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder let ass = assumps e

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder vs = localVars e

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder ps = preIds e

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder compIds = getCompoundLists e

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder let (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)

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

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

49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let Result ds mr = getResolved

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder (showDoc . parenTerm) (getRange trm)

962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder (toMixTerm e) chart

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder addDiags ds

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder if isPat then case mr of

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Nothing -> return mr

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder Just pat -> fmap Just $ anaPattern sIds pat

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder else return mr

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetPolyIds = Set.unions . map ( \ (i, OpInfos l) ->

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder foldr ( \ oi s -> case opType oi of

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder TypeScheme (_ : _) _ _ -> Set.insert i s

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> s) Set.empty l) . Map.toList .

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Map.filterWithKey ( \ (Id _ cs _) _ -> null cs)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompound :: Id -> [Id]

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompound (Id _ cs _) = cs

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompoundLists :: Env -> Set.Set [Id]

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaedergetCompoundLists e = Set.delete [] $ Set.map getCompound $ Set.union

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (Map.keysSet $ assumps e) $ Map.keysSet $ typeMap e

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

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder map ( \ i -> let j = polyId i in

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (j, getIdPrec p ps i, getTokenPlaceList j)) polyIds ++

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder map ( \ i -> let j = polyId i in

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (protect j, maxWeight p + 3, getPlainTokenList j))

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder (filter isMixfix polyIds)

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederpolyId :: Id -> Id

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederpolyId (Id ts _ ps) = let (toks, pls) = splitMixToken ts in

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder Id (toks ++ [typeInstTok] ++ pls) [] ps

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederunPolyId :: Id -> Maybe Id

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederunPolyId (Id ts cs ps) = let (ft, rt) = partition (== typeInstTok) ts in

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder case ft of

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder [_] -> Just $ Id rt cs ps

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder _ -> Nothing

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederanaPattern :: Set.Set Id -> Pattern -> State Env Pattern

59a2f25e7d71b91b4eda6fa4da753473ad629619Christian MaederanaPattern s pat = case pat of

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualVar vd -> do newVd <- checkVarDecl vd

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

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder (tvar, c) <- toEnvState $ freshVar $ posOfId 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

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder let newVd = VarDecl v ty ok (qs `appRange` ps) in

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ QualVar newVd

dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder _ -> do newP <- anaPattern s p

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder (tvar, c) <- toEnvState $ freshVar $ posOfId v

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

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> return vd