MixAna.hs revision 639732746d7c3a586790043b452a4cbdd29a3fc3
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceDescription : mixfix analysis for terms
81ec673ac5ab1493568d9ef7798b752ab8ee0e61Felix Gabriel ManceCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : experimental
5d801400993c9671010d244646936d8fd435638cChristian MaederPortability : portable
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceMixfix analysis of terms and patterns, type annotations are also analysed
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , iterateCharts
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Map as Map
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Manceimport qualified Data.Set as Set
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Manceimport qualified Text.ParserCombinators.Parsec as P
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport Control.Exception (assert)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceaddType :: Term -> Term -> Term
6033265e7b4ae660eff78e944213286863304903Mihai CodescuaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceaddType _ _ = error "addType"
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-- | try to reparse terms as a compound list
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisCompoundList :: Set.Set [Id] -> [Term] -> Bool
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceisCompoundList compIds =
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance maybe False (flip Set.member compIds) . mapM reparseAsId
68de80eb2800338cbd16512106fcadab79325d8bChristian MaederisTypeList :: Env -> [Term] -> Bool
68de80eb2800338cbd16512106fcadab79325d8bChristian MaederisTypeList e l = case mapM termToType l of
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder Nothing -> False
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder let Result ds ml = mapM ( \ t -> anaTypeM (Nothing, t) e) ts
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder in isJust ml && not (hasErrors ds)
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian MaedertermToType :: Term -> Maybe Type
68de80eb2800338cbd16512106fcadab79325d8bChristian MaedertermToType t = case P.runParser ((case getPosList t of
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder [] -> return ()
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance p : _ -> P.setPosition $ fromPos p)
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Right x -> Just x
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederanaPolyId :: Id -> TypeScheme -> State Env (Maybe (Id, TypeScheme))
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceanaPolyId i@(Id ts cs ps) sc = do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mSc <- anaTypeScheme sc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> return Nothing
407f3d9049715c5d96f014a5a1776410e034db83Christian Maeder Just newSc@(TypeScheme tvars _ _) -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let poly = cs == map getTypeVar tvars
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance es = filter (not . flip Set.member ids) cs
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance if null cs || poly then return ()
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder addDiags $ map (\ j -> mkDiag Warning
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder "unexpected identifier in compound list" j) es
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder if null tvars then return () else
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder if null es then
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder addDiags [mkDiag Hint
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder "is polymorphic compound identifier" i]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else addDiags [mkDiag Error
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder ("type scheme '" ++ showDoc sc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance "`\n must correspond to instantiation list") cs]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return $ Just (if poly then Id ts [] ps else i, newSc)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceresolveQualOp :: Id -> TypeScheme -> State Env (Id, TypeScheme)
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederresolveQualOp i sc = do
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder mSc <- anaPolyId i sc
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder Nothing -> return (i, sc)
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder Just p@(j, nSc) -> do
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance case findOpId e j nSc of
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Nothing -> addDiags [mkDiag Error "operation not found" j]
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance _ -> return ()
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceiterateCharts :: GlobalAnnos -> Set.Set [Id] -> [Term] -> Chart Term
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance -> State Env (Chart Term)
19e01e1a7e319063434bd86c8ecbc5f241ef9993Felix Gabriel ManceiterateCharts ga compIds terms chart = do
5a3ae0a9224276de25e709ef8788c1b9716cd206Christian Maeder let self = iterateCharts ga compIds
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance oneStep = nextChart addType (toMixTerm e) ga chart
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance vs = localVars e
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance tm = typeMap e
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance [] -> return chart
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance t : tt -> let recurse trm = self tt $ oneStep
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance (trm, exprTok {tokPos = getRange trm}) in case t of
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance MixfixTerm ts -> self (ts ++ tt) chart
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance MixTypeTerm q typ ps -> do
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance mTyp <- anaStarType typ
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Nothing -> recurse t
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Just nTyp -> self tt $ oneStep
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance (MixTypeTerm q (monoType nTyp) ps, typeTok {tokPos = ps})
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance BracketTerm b ts ps ->
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance let bres = self (expandPos TermToken
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (getBrackets b) ts ps ++ tt) chart in case (b, ts) of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (Squares, _ : _) -> if isCompoundList compIds ts then do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance addDiags [mkDiag Hint "is compound list" t]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance else if isTypeList e ts then do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance let testChart = oneStep (t, typeInstTok {tokPos = ps})
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance if null $ solveDiags testChart then do
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel Mance addDiags [mkDiag Hint "is type list" t]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance self tt testChart
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> case (b, ts, tt) of
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (Parens, [QualOp b2 v sc [] ps2], hd@(BracketTerm Squares
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance ts2@(_ : _) ps3) : rtt) | isTypeList e ts2 -> do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance addDiags [mkDiag Hint "is type list" ts2]
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (j, nSc) <- resolveQualOp v sc
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance self rtt $ oneStep
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance ( QualOp b2 j nSc (bracketTermToTypes e hd) ps2
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , exprTok {tokPos = appRange ps ps3})
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualVar (VarDecl v typ ok ps) -> do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mTyp <- anaStarType typ
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance recurse $ maybe t ( \ nType -> QualVar $ VarDecl v (monoType nType)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance QualOp b v sc [] ps -> do
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance (j, nSc) <- resolveQualOp v sc
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder recurse $ QualOp b j nSc [] ps
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance QuantifiedTerm quant decls hd ps -> do
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance newDs <- mapM (anaddGenVarDecl False) decls
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance mt <- resolve ga hd
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance putLocalVars vs
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance recurse $ QuantifiedTerm quant (catMaybes newDs) (maybe hd id mt) ps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance LambdaTerm decls part hd ps -> do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mDecls <- mapM (resolvePattern ga) decls
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance let anaDecls = catMaybes mDecls
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance bs = concatMap extractVars anaDecls
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance checkUniqueVars bs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mapM_ (addLocalVar False) bs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mt <- resolve ga hd
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance putLocalVars vs
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance CaseTerm hd eqs ps -> do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mt <- resolve ga hd
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance newEs <- resolveCaseEqs ga eqs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance recurse $ CaseTerm (maybe hd id mt) newEs ps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance LetTerm b eqs hd ps -> do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance newEs <- resolveLetEqs ga eqs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mt <- resolve ga hd
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance putLocalVars vs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance recurse $ LetTerm b newEs (maybe hd id mt) ps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance TermToken tok -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let (ds1, trm) = convertMixfixToken (literal_annos ga)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance (flip ResolvedMixTerm []) TermToken tok
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance self tt $ oneStep $ case trm of
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance TermToken _ -> (trm, tok)
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance _ -> (trm, exprTok {tokPos = tokPos tok})
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance AsPattern vd p ps -> do
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance mp <- resolvePattern ga p
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance recurse $ AsPattern vd (maybe p id mp) ps
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance TypedTerm trm k ty ps -> do
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance -- assume that type is analysed
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mt <- resolve ga trm
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance recurse $ TypedTerm (maybe trm id mt) k ty ps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance _ -> error ("iterCharts: " ++ show t)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance-- * equation stuff
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceresolveCaseEq ga (ProgEq p t ps) = do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mp <- resolvePattern ga p
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Nothing -> return Nothing
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Just newP -> do
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance let bs = extractVars newP
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance checkUniqueVars bs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance vs <- gets localVars
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder mapM_ (addLocalVar False) bs
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mtt <- resolve ga t
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance putLocalVars vs
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder return $ case mtt of
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance Nothing -> Nothing
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Just newT -> Just $ ProgEq newP newT ps
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel ManceresolveCaseEqs ga eqs = case eqs of
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance [] -> return []
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mance mEq <- resolveCaseEq ga eq
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance reqs <- resolveCaseEqs ga rt
083b2687afdb676237f926bdb643b24027291d05Felix Gabriel Mance return $ case mEq of
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance Nothing -> reqs
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder Just newEq -> newEq : reqs
e26bfed39ffa184453272125a4adf147206eac74Christian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel ManceresolveLetEqs _ [] = return []
e26bfed39ffa184453272125a4adf147206eac74Christian MaederresolveLetEqs ga eqs = case eqs of
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder [] -> return []
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder ProgEq pat trm ps : rt -> do
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder mPat <- resolvePattern ga pat
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder resolve ga trm
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder resolveLetEqs ga rt
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder Just newPat -> do
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder let bs = extractVars newPat
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance checkUniqueVars bs
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance mapM_ (addLocalVar False) bs
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder mTrm <- resolve ga trm
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder Nothing -> resolveLetEqs ga rt
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder Just newTrm -> do
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance reqs <- resolveLetEqs ga rt
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel Mance return $ ProgEq newPat newTrm ps : reqs
e26bfed39ffa184453272125a4adf147206eac74Christian MaedermkPatAppl :: Term -> Term -> Range -> Term
e26bfed39ffa184453272125a4adf147206eac74Christian MaedermkPatAppl op arg qs = case op of
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder QualVar (VarDecl i (MixfixType []) _ _) -> ResolvedMixTerm i [] [arg] qs
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel Mance _ -> ApplTerm op arg qs
e26bfed39ffa184453272125a4adf147206eac74Christian MaederbracketTermToTypes :: Env -> Term -> [Type]
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel MancebracketTermToTypes e t = case t of
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance BracketTerm Squares tys _ ->
d850dba73b02f345f64a3546d0f0299c292f88d6Felix Gabriel Mance map (monoType . snd) $ maybe (error "bracketTermToTypes") id $
511be329b2e8f55d0c6b18bd92571a1776b15932Felix Gabriel Mance maybeResult $ mapM ( \ ty -> anaTypeM (Nothing, ty) e) $
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance maybe (error "bracketTermToTypes1") id $ mapM termToType tys
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel Mance _ -> error "bracketTermToTypes2"
6504b297e21d071d8fada2f732cabb6d8f7d38a2Felix Gabriel MancetoMixTerm :: Env -> Id -> [Term] -> Range -> Term
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian MaedertoMixTerm e i ar qs =
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder if i == applId then assert (length ar == 2) $
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder else if i == tupleId || i == unitId then
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder mkTupleTerm ar qs
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance else case unPolyId i of
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian Maeder Just j@(Id ts _ _) -> if isMixfix j && isSingle ar then
1075744775ba70c9ef6cdd06523204751f544ed5Christian Maeder ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs
1075744775ba70c9ef6cdd06523204751f544ed5Christian Maeder else assert (length ar == 1 + placeCount j) $
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder let (far, tar : sar) =
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder splitAt (placeCount $ mkId $ fst $ splitMixToken ts) ar
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder _ -> ResolvedMixTerm i [] ar qs
e26bfed39ffa184453272125a4adf147206eac74Christian MaedergetKnowns :: Id -> Set.Set Token
e26bfed39ffa184453272125a4adf147206eac74Christian MaedergetKnowns (Id ts cs _) =
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder Set.union (Set.fromList ts) $ Set.unions $ map getKnowns cs
e26bfed39ffa184453272125a4adf147206eac74Christian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian MaederresolvePattern = resolver True
1075744775ba70c9ef6cdd06523204751f544ed5Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
e26bfed39ffa184453272125a4adf147206eac74Christian Maederresolve = resolver False
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maederresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maederresolver isPat ga trm = do
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder let ass = assumps e
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder vs = localVars e
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder ps = preIds e
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder compIds = getCompoundLists e
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder $ Set.union (Map.keysSet ass) $ Map.keysSet vs
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS
6470a08d94430381c14ed30c3a3a8e433401352bcmaeder let Result ds mr = getResolved (showDoc . parenTerm) (getRange trm)
6470a08d94430381c14ed30c3a3a8e433401352bcmaeder (toMixTerm e) chart
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder if isPat then case mr of
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder Nothing -> return mr
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder Just pat -> fmap Just $ anaPattern sIds pat
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder else return mr
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian MaedergetPolyIds :: Assumps -> Set.Set Id
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian MaedergetPolyIds = Set.unions . map ( \ (i, s) ->
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maeder Set.fold ( \ oi -> case opType oi of
6470a08d94430381c14ed30c3a3a8e433401352bcmaeder TypeScheme (_ : _) _ _ -> Set.insert i
e26bfed39ffa184453272125a4adf147206eac74Christian MaederuTok = mkSimpleId "_"
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel MancebuiltinIds :: [Id]
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
44985cbd4eb61dbc348617ebdd44a774e51dac07Christian MaedermakeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance -> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel MancemakeRules ga ps@(p, _) polyIds aIds =
1075744775ba70c9ef6cdd06523204751f544ed5Christian Maeder let (sIds, ids) = Set.partition isSimpleId aIds
1075744775ba70c9ef6cdd06523204751f544ed5Christian Maeder ks = Set.fold (Set.union . getKnowns) Set.empty ids
1075744775ba70c9ef6cdd06523204751f544ed5Christian Maeder rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance m2 = maxWeight p + 2
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance in ( \ tok -> if isSimpleToken tok
63946b0fc89de113d5bf4819f9c8cc5d6adce810cmaeder || tok == uTok then
63946b0fc89de113d5bf4819f9c8cc5d6adce810cmaeder [(simpleIdToId tok, m2, [tok])] else []
63946b0fc89de113d5bf4819f9c8cc5d6adce810cmaeder , partitionRules $ listRules m2 ga ++
63946b0fc89de113d5bf4819f9c8cc5d6adce810cmaeder initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)
63946b0fc89de113d5bf4819f9c8cc5d6adce810cmaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceinitRules (p, ps) polyIds bs is =
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance map ( \ i -> mixRule (getIdPrec p ps i) i)
4b7c9b9fec53befb553f2c9b11e30a4fe2235e03Felix Gabriel Mance map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance (filter isMixfix is) ++
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance-- identifiers with a positive number of type arguments
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance map ( \ i -> ( polyId i, getIdPrec p ps i
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance , getPolyTokenList i)) polyIds ++
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance map ( \ i -> ( protect $ polyId i, maxWeight p + 3
0c3badd7ad83eb89f64ef5ed1122c4fa856fb45dFelix Gabriel Mance , getPlainPolyTokenList i)) (filter isMixfix polyIds)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance-- create fresh type vars for unknown ids tagged with type MixfixType [].
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel ManceanaPattern :: Set.Set Id -> Pattern -> State Env Pattern
3980dee81f793b601da33adea1b55753bab868a9Felix Gabriel ManceanaPattern s pat = case pat of
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance QualVar vd -> do
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder newVd <- checkVarDecl vd
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder return $ QualVar newVd
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder ResolvedMixTerm i tys pats ps | null pats && null tys &&
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder (isSimpleId i || i == simpleIdToId uTok) &&
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder not (Set.member i s) -> do
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder (tvar, c) <- toEnvState $ freshVar i
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder | otherwise -> do
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder l <- mapM (anaPattern s) pats
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder return $ ResolvedMixTerm i tys l ps
669b3375925f7a145d287fa89f3a815708dbe7a1Christian Maeder ApplTerm p1 p2 ps -> do
92ae4d5885ea837ffe3dae9b2de742f871229b94Christian Maeder p3 <- anaPattern s p1
a03c109eabfe250e4b57bdf44f37f53751a65df4Felix Gabriel Mance p4 <- anaPattern s p2
a03c109eabfe250e4b57bdf44f37f53751a65df4Felix Gabriel Mance return $ ApplTerm p3 p4 ps
a03c109eabfe250e4b57bdf44f37f53751a65df4Felix Gabriel Mance TupleTerm pats ps -> do
a03c109eabfe250e4b57bdf44f37f53751a65df4Felix Gabriel Mance l <- mapM (anaPattern s) pats
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance return $ TupleTerm l ps
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder TypedTerm p q ty ps -> do
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance QualVar (VarDecl v (MixfixType []) ok qs) ->
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance return $ QualVar $ VarDecl v ty ok $ appRange qs ps
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder newP <- anaPattern s p
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder return $ TypedTerm newP q ty ps
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mance AsPattern vd p2 ps -> do
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder newVd <- checkVarDecl vd
fa544036407a8ec4be203ebd5e3bff225175e664Felix Gabriel Mance p4 <- anaPattern s p2
fa544036407a8ec4be203ebd5e3bff225175e664Felix Gabriel Mance return $ AsPattern newVd p4 ps
83f5f3291f9b40fa688776b4da10b5fa102a5ff8Felix Gabriel Mance _ -> return pat
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder where checkVarDecl vd@(VarDecl v t ok ps) = case t of
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder MixfixType [] -> do
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder (tvar, c) <- toEnvState $ freshVar v
e26bfed39ffa184453272125a4adf147206eac74Christian Maeder return $ VarDecl v (TypeName tvar rStar c) ok ps
6d907570443508c99867ea29ddf5e5cb0a2ef8c2Christian Maeder _ -> return vd