MixAna.hs revision dcb9ff0e2c2379735acce7073196508d455e0b01
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder{- |
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederModule : $Header$
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : maeder@tzi.de
c797f343be2f3619bb1f5569753166ec49d27bdbChristian MaederStability : experimental
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder-}
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maedermodule HasCASL.MixAna where
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.GlobalAnnotations
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport Common.Result
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Id
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Common.Earley
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.ConvertLiteral
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport Common.Lib.State
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport qualified Common.Lib.Rel as Rel
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport qualified Common.Lib.Map as Map
b645cf3dc1e449038ed291bbd11fcc6e02b2fc7fChristian Maederimport qualified Common.Lib.Set as Set
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maederimport HasCASL.As
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.AsUtils
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maederimport HasCASL.PrintAs
975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport HasCASL.Unify
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HasCASL.VarDecl
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport HasCASL.Le
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport Data.Maybe
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Control.Exception(assert)
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedergetIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian MaedergetIdPrec (pm, r, m) ps i = if i == applId then m + 1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder else Map.findWithDefault
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder (if begPlace i || endPlace i then if Set.member i ps then r else m
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder else m + 2) i pm
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederaddType :: Term -> Term -> Term
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian MaederaddType _ _ = error "addType"
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederiterateCharts :: GlobalAnnos -> [Term] -> Chart Term
b190f5c7cf3ddda73724efe5ce82b9585ed76be1Christian Maeder -> State Env (Chart Term)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederiterateCharts ga terms chart =
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder do e <- get
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder let self = iterateCharts ga
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder oneStep = nextChart addType toMixTerm ga chart
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder vs = localVars e
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder tm = typeMap e
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case terms of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder [] -> return chart
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder t:tt -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let recurse trm = self tt $
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder oneStep (trm, exprTok {tokPos = getRange trm})
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder case t of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder MixTypeTerm q typ ps -> do
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder mTyp <- anaStarType typ
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case mTyp of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder Nothing -> recurse t
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Just nTyp -> self tt $ oneStep
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder (MixTypeTerm q (monoType nTyp) ps,
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder typeTok {tokPos = ps})
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder BracketTerm b ts ps -> self
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder (expandPos TermToken (getBrackets b) ts ps ++ tt) chart
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder QualVar (VarDecl v typ ok ps) -> do
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder mTyp <- anaStarType typ
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder case mTyp of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> recurse t
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Just nType -> recurse $ QualVar $
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder VarDecl v (monoType nType) ok ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder QualOp b (InstOpId v ts qs) sc ps -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mSc <- anaTypeScheme sc
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder newTs <- anaInstTypes ts
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case mSc of
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> recurse t
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just nSc -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case findOpId e v nSc of
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder Nothing -> addDiags [mkDiag Error
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder "operation not found" v]
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> return ()
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder recurse $ QualOp b (InstOpId v newTs qs) nSc ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder QuantifiedTerm quant decls hd ps -> do
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder newDs <- mapM (anaddGenVarDecl False) decls
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder mt <- resolve ga hd
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder putLocalVars vs
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder putTypeMap tm
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let newT = case mt of Just trm -> trm
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder _ -> hd
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder LambdaTerm decls part hd ps -> do
462ec4b2fa3e0e788eb60dcb4aebc518298f342cChristian Maeder mDecls <- mapM (resolvePattern ga) decls
f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder let anaDecls = catMaybes mDecls
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder bs = concatMap extractVars anaDecls
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder checkUniqueVars bs
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder mapM_ (addLocalVar False) bs
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder mt <- resolve ga hd
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder putLocalVars vs
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder CaseTerm hd eqs ps -> do
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder mt <- resolve ga hd
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder newEs <- resolveCaseEqs ga eqs
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder recurse $ CaseTerm (maybe hd id mt) newEs ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder LetTerm b eqs hd ps -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder newEs <- resolveLetEqs ga eqs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mt <- resolve ga hd
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder putLocalVars vs
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder recurse $ LetTerm b newEs (maybe hd id mt) ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder TermToken tok -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let (ds1, trm) = convertMixfixToken
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (literal_annos ga)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ResolvedMixTerm TermToken tok
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder addDiags ds1
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder self tt $ oneStep $
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder case trm of
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski TermToken _ -> (trm, tok)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> (trm, exprTok
04dada28736b4a237745e92063d8bdd49a362debChristian Maeder {tokPos = tokPos tok})
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder AsPattern vd p ps -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mp <- resolvePattern ga p
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let newP = case mp of Just pat -> pat
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Nothing -> p
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder recurse $ AsPattern vd newP ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder TypedTerm trm k ty ps -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder -- assume that type is analysed
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mt <- resolve ga trm
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder recurse $ TypedTerm (maybe trm id mt) k ty ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder _ -> error ("iterCharts: " ++ show t)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder-- * equation stuff
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveCaseEq ga (ProgEq p t ps) =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder do mp <- resolvePattern ga p
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder case mp of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Nothing -> return Nothing
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Just newP -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let bs = extractVars newP
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder checkUniqueVars bs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder vs <- gets localVars
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mapM_ (addLocalVar False) bs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mtt <- resolve ga t
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder putLocalVars vs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ case mtt of
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Nothing -> Nothing
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder Just newT -> Just $ ProgEq newP newT ps
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveCaseEqs _ [] = return []
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveCaseEqs ga (eq : rt) =
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder do mEq <- resolveCaseEq ga eq
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder eqs <- resolveCaseEqs ga rt
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder return $ case mEq of
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> eqs
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just newEq -> newEq : eqs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveLetEqs _ [] = return []
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder do mPat <- resolvePattern ga pat
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder case mPat of
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Nothing -> do resolve ga trm
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder resolveLetEqs ga rt
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Just newPat -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let bs = extractVars newPat
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder checkUniqueVars bs
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder mapM_ (addLocalVar False) bs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder mTrm <- resolve ga trm
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder case mTrm of
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder Nothing -> resolveLetEqs ga rt
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder Just newTrm -> do
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder eqs <- resolveLetEqs ga rt
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder return (ProgEq newPat newTrm ps : eqs)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedermkPatAppl :: Term -> Term -> Range -> Term
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedermkPatAppl op arg qs =
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder case op of
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian Maeder ResolvedMixTerm i [arg] qs
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder _ -> ApplTerm op arg qs
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaedertoMixTerm :: Id -> [Term] -> Range -> Term
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian MaedertoMixTerm i ar qs =
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder if i == applId then assert (length ar == 2) $
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder else if i == tupleId || i == unitId then
962d5c684e2b86d1f9c556c096b426e10cc74026Christian Maeder mkTupleTerm ar qs
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder else ResolvedMixTerm i ar qs
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
b984ff0ba75221f64451c1e69b3977967d4e99a1Christian MaedergetKnowns :: Id -> Set.Set Token
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList ts) $
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder Set.unions (map getKnowns cs)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian MaederresolvePattern = resolver True
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederresolve = resolver False
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maederresolver isPat ga trm =
6cca02cb6a5ae882d887a879f8b7a71941c3715cChristian Maeder do ass <- gets assumps
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder vs <- gets localVars
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ps <- gets preIds
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder let (addRule, ruleS, sIds) = makeRules ga ps
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder $ Set.union (Rel.keysSet ass) $ Rel.keysSet vs
c797f343be2f3619bb1f5569753166ec49d27bdbChristian Maeder chart <- iterateCharts ga [trm] $ initChart addRule ruleS
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder let Result ds mr = getResolved
15bb922b665fcd44c6230a1202785d0c7890e90cChristian Maeder (shows . printTerm emptyGlobalAnnos . parenTerm) (getRange trm)
e95bbf384f5cbcb7eb23286d5f15dffbd471db17Christian Maeder toMixTerm chart
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski addDiags ds
if isPat then case mr of
Nothing -> return mr
Just pat -> fmap Just $ anaPattern sIds pat
else return mr
uTok :: Token
uTok = mkSimpleId "_"
builtinIds :: [Id]
builtinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
makeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
-> (Token -> [Rule], Rules, Set.Set Id)
makeRules ga ps@((_, _, m), _) aIds =
let (sIds, ids) = Set.partition isSimpleId aIds
ks = Set.fold (Set.union . getKnowns) Set.empty ids
rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks
m2 = m + 2
in ( \ tok -> if isSimpleToken tok
&& not (Set.member tok ks)
|| tok == uTok then
[(simpleIdToId tok, m2, [tok])] else []
, partitionRules $ listRules m2 ga ++
initRules ps builtinIds (Set.toList rIds)
, sIds)
initRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
initRules (pm@(_, _, m), ps) bs is =
map ( \ i -> mixRule (getIdPrec pm ps i) i)
(bs ++ is) ++
map ( \ i -> (protect i, m + 3, getPlainTokenList i))
(filter isMixfix is)
-- create fresh type vars for unknown ids tagged with type MixfixType [].
anaPattern :: Set.Set Id -> Pattern -> State Env Pattern
anaPattern s pat =
case pat of
QualVar vd -> do newVd <- checkVarDecl vd
return $ QualVar newVd
ResolvedMixTerm i pats ps | null pats &&
(isSimpleId i || i == simpleIdToId uTok) &&
not (Set.member i s) -> do
(tvar, c) <- toEnvState $ freshVar $ posOfId i
return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps
| otherwise -> do
l <- mapM (anaPattern s) pats
return $ ResolvedMixTerm i l ps
ApplTerm p1 p2 ps -> do
p3 <- anaPattern s p1
p4 <- anaPattern s p2
return $ ApplTerm p3 p4 ps
TupleTerm pats ps -> do
l <- mapM (anaPattern s) pats
return $ TupleTerm l ps
TypedTerm p q ty ps -> do
case p of
QualVar (VarDecl v (MixfixType []) ok qs) ->
let newVd = VarDecl v ty ok (qs `appRange` ps) in
return $ QualVar newVd
_ -> do newP <- anaPattern s p
return $ TypedTerm newP q ty ps
AsPattern vd p2 ps -> do
newVd <- checkVarDecl vd
p4 <- anaPattern s p2
return $ AsPattern newVd p4 ps
_ -> return pat
where checkVarDecl vd@(VarDecl v t ok ps) = case t of
MixfixType [] -> do
(tvar, c) <- toEnvState $ freshVar $ posOfId v
return $ VarDecl v (TypeName tvar rStar c) ok ps
_ -> return vd
-- | put parenthesis around applications
parenTerm :: Term -> Term
parenTerm trm = case trm of
ResolvedMixTerm n ts ps ->
ResolvedMixTerm n (map parenTerm ts) ps
ApplTerm t1 t2' ps -> let t2 = parenTerm t2' in
ApplTerm (addParAppl t1) (case t2 of
ResolvedMixTerm _ [] _ -> t2
QualVar _ -> t2
QualOp _ _ _ _ -> t2
TermToken _ -> t1
BracketTerm _ _ _ -> t2
TupleTerm _ _ -> t2
_ -> addPar t2) ps
TupleTerm ts ps -> TupleTerm (map parenTerm ts) ps
TypedTerm t q typ ps ->
TypedTerm (addParAppl t) q typ ps
QuantifiedTerm q vs t ps -> QuantifiedTerm q vs (parenTerm t) ps
LambdaTerm ps q t qs ->
LambdaTerm (map parenTerm ps) q (parenTerm t) qs
CaseTerm t es ps -> CaseTerm (parenTerm t) (map parenProgEq es) ps
LetTerm br es t ps ->
LetTerm br (map parenProgEq es) (parenTerm t) ps
MixfixTerm ts -> MixfixTerm $ map addParAppl ts
BracketTerm k ts ps -> BracketTerm k (map parenTerm ts) ps
AsPattern v p ps -> AsPattern v (addParAppl p) ps
TermToken _ -> trm
MixTypeTerm _ _ _ -> trm
QualVar _ -> trm
QualOp _ _ _ _ -> trm
where addPar t = TupleTerm [t] nullRange
addParAppl t' = let t = parenTerm t' in case t of
ApplTerm _ _ _ -> t
ResolvedMixTerm _ _ _ -> t
QualVar _ -> t
QualOp _ _ _ _ -> t
TermToken _ -> t
BracketTerm _ _ _ -> t
TupleTerm _ _ -> t
_ -> addPar t
-- | put parenthesis around applications in equations
parenProgEq :: ProgEq -> ProgEq
parenProgEq (ProgEq p t q) = ProgEq (parenTerm p) (parenTerm t) q