MixAna.hs revision 49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- |
ca010363454de207082dfaa4b753531ce2a34551Christian MaederModule : $Header$
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : maeder@tzi.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
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Keywords
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Common.Earley
9e36526b3e4a01ba4c0e63d263261653628eaa0fChristian Maederimport Common.ConvertLiteral
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Common.Lib.State
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maederimport qualified Common.Lib.Rel as Rel
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Map as Map
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Set as Set
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport HasCASL.As
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport HasCASL.AsUtils
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maederimport HasCASL.PrintAs
975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport HasCASL.Unify
53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport HasCASL.VarDecl
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport HasCASL.Le
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maeder
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maederimport Data.Maybe
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maederimport Control.Exception(assert)
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
1bc3627bdb66ecc1efe23eeaeca0ee1f3151ab14Christian MaedergetIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetIdPrec (pm, r, m) ps i = if i == applId then m + 1
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder else Map.findWithDefault
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder (if begPlace i || endPlace i then if Set.member i ps then r else m
454b2a26b6ea95206df2f82768a8e12765f182bfChristian Maeder else m + 2) i pm
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maedertype TermChart = Chart Term
08f8731b34de5dc1ced274594978ad8879c831bdChristian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederiterateCharts :: GlobalAnnos -> [Term] -> TermChart
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -> State Env TermChart
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederiterateCharts ga terms chart =
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder do e <- get
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let self = iterateCharts ga
eed6203a39f88e398d86431a66d367036a3d17baChristian Maeder oneStep = nextChart addType toMixTerm 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})
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder BracketTerm b ts ps -> self
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (expandPos TermToken (getBrackets b) ts ps ++ tt) chart
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)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ResolvedMixTerm 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 []) _ _) ->
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ResolvedMixTerm i [arg] qs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> ApplTerm op arg qs
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskitoMixTerm :: Id -> [Term] -> Range -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedertoMixTerm 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
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder else if isUnknownId i then
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualVar $ VarDecl (simpleIdToId $ unToken i)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (MixfixType []) Other qs
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else ResolvedMixTerm i ar qs
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian Maeder
fcfed328fae6266214ee61ee7a16fd263fd3cb70Christian MaedergetKnowns :: Id -> Knowns
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Set.unions (map getKnowns cs)
46d766efdf8beaaadf3f34d99c305738064e9216Christian Maeder
975642b989852fc24119c59cf40bc1af653608ffChristian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolvePattern ga p = do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder mp <- resolver ga (unknownId : builtinIds) p
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder case mp of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Nothing -> return Nothing
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Just np -> fmap Just $ anaPattern np
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve ga = resolver ga builtinIds
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maederresolver :: GlobalAnnos -> [Id] -> Term
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder -> State Env (Maybe Term)
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolver ga bs trm =
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder do ass <- gets assumps
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder vs <- gets localVars
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder ps@((_, _, m), _) <- gets preIds
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder let ids = Set.toList $ Set.union (Rel.keysSet ass) $ Rel.keysSet vs
a1d523aa255a291c0154af764fbdb8597c445918Christian Maeder ks = Set.union (Set.fromList (tokStr exprTok: inS :
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder map (:[]) ":{}[](),"))
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder $ Set.unions $ map getKnowns ids
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder chart<- iterateCharts ga [trm] $
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder initChart (listRules (m + 3) ga ++
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (initRules ps bs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ids)) (if unknownId `elem` bs then ks else Set.empty)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let Result ds mr = getResolved
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (shows . printTerm emptyGlobalAnnos . parenTerm) (getRange trm)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder toMixTerm chart
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder addDiags ds
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder return mr
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederinitRules (pm@(_, _, m), ps) bs is =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map ( \ i -> mixRule (getIdPrec pm ps i) i)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (bs ++ is) ++
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder map ( \ i -> (protect i, m + 3, getPlainTokenList i))
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (filter isMixfix is)
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- create fresh type vars for unknown ids tagged with type MixfixType [].
975642b989852fc24119c59cf40bc1af653608ffChristian MaederanaPattern :: Pattern -> State Env Pattern
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederanaPattern pat =
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder case pat of
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualVar vd -> do newVd <- checkVarDecl vd
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ QualVar newVd
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder ResolvedMixTerm i pats ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder l <- mapM anaPattern pats
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ ResolvedMixTerm i l ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ApplTerm p1 p2 ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder p3 <- anaPattern p1
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder p4 <- anaPattern p2
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ ApplTerm p3 p4 ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TupleTerm pats ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder l <- mapM anaPattern 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
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder _ -> do newP <- anaPattern p
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ TypedTerm newP q ty ps
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder AsPattern vd p2 ps -> do
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder newVd <- checkVarDecl vd
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder p4 <- anaPattern 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
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- | put parenthesis around applications
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian MaederparenTerm :: Term -> Term
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian MaederparenTerm trm = case trm of
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder ResolvedMixTerm n ts ps ->
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder ResolvedMixTerm n (map parenTerm ts) ps
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder ApplTerm t1 t2' ps -> let t2 = parenTerm t2' in
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder ApplTerm (addParAppl t1) (case t2 of
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder ResolvedMixTerm _ [] _ -> t2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QualVar _ -> t2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QualOp _ _ _ _ -> t2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TermToken _ -> t1
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder BracketTerm _ _ _ -> t2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TupleTerm _ _ -> t2
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder _ -> addPar t2) ps
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TupleTerm ts ps -> TupleTerm (map parenTerm ts) ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder TypedTerm t q typ ps ->
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TypedTerm (addParAppl t) q typ ps
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QuantifiedTerm q vs t ps -> QuantifiedTerm q vs (parenTerm t) ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder LambdaTerm ps q t qs ->
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder LambdaTerm (map parenTerm ps) q (parenTerm t) qs
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder CaseTerm t es ps -> CaseTerm (parenTerm t) (map parenProgEq es) ps
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder LetTerm br es t ps ->
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder LetTerm br (map parenProgEq es) (parenTerm t) ps
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder MixfixTerm ts -> MixfixTerm $ map addParAppl ts
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder BracketTerm k ts ps -> BracketTerm k (map parenTerm ts) ps
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder AsPattern v p ps -> AsPattern v (addParAppl p) ps
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TermToken _ -> trm
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder MixTypeTerm _ _ _ -> trm
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QualVar _ -> trm
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QualOp _ _ _ _ -> trm
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder where addPar t = TupleTerm [t] nullRange
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder addParAppl t' = let t = parenTerm t' in case t of
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder ApplTerm _ _ _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder ResolvedMixTerm _ _ _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QualVar _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder QualOp _ _ _ _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TermToken _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder BracketTerm _ _ _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder TupleTerm _ _ -> t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder _ -> addPar t
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian Maeder-- | put parenthesis around applications in equations
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian MaederparenProgEq :: ProgEq -> ProgEq
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian MaederparenProgEq (ProgEq p t q) = ProgEq (parenTerm p) (parenTerm t) q