MixAna.hs revision 4561227a776bdf0ab679b19fb92f1eaaed8786f7
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
eca29a7be76eb73944ec19b06eda3d6a9e6e543dChristian MaederMaintainer : maeder@tzi.de
ca010363454de207082dfaa4b753531ce2a34551Christian MaederStability : experimental
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederPortability : portable
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maederimport qualified Common.Lib.Rel as Rel
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Common.Lib.Set as Set
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType :: Term -> Term -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederaddType _ _ = error "addType"
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederiterateCharts :: GlobalAnnos -> [Term] -> Chart Term
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -> State Env (Chart Term)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederiterateCharts ga terms chart =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let self = iterateCharts ga
5e605dc61ff9ec5724c319603905dc9b0dccc05fChristian 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 let recurse trm = self tt $
d48085f765fca838c1d972d2123601997174583dChristian Maeder oneStep (trm, exprTok {tokPos = getRange trm})
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder MixfixTerm ts -> self (ts ++ tt) chart
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder MixTypeTerm q typ ps -> do
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder mTyp <- anaStarType typ
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
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
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 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 self tt $ oneStep $
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 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)
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
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 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 MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
669e21946b6f90785fc3cb44e7cf4f38c3f6493dChristian MaederresolveLetEqs _ [] = return []
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =
13b24998210d193b38cae06485da6f06c61d7f62Christian Maeder do mPat <- resolvePattern ga pat
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
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)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimkPatAppl :: Term -> Term -> Range -> Term
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian MaedermkPatAppl op arg qs =
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder ResolvedMixTerm i [arg] qs
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder _ -> ApplTerm op arg qs
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
909ce57d58a9cec1d214f0ecbdb1dadddad2e6d9Christian Maeder else ResolvedMixTerm i ar qs
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns :: Id -> Set.Set Token
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList ts) $
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder Set.unions (map getKnowns cs)
975642b989852fc24119c59cf40bc1af653608ffChristian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederresolvePattern = resolver True
13b24998210d193b38cae06485da6f06c61d7f62Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolve = resolver False
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maederresolver isPat ga trm =
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder do ass <- gets assumps
369454f9b2dbea113cbb40544a9b0f31425b2c69Christian Maeder vs <- gets localVars
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder ps <- gets preIds
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let (addRule, ruleS, sIds) = makeRules ga ps
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder $ Set.union (Rel.keysSet ass) $ Rel.keysSet vs
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder chart <- iterateCharts ga [trm] $ initChart addRule ruleS
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder let Result ds mr = getResolved
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder (shows . printTerm emptyGlobalAnnos . parenTerm) (getRange trm)
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder toMixTerm chart
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 MaederuTok = mkSimpleId "_"
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds :: [Id]
13b24998210d193b38cae06485da6f06c61d7f62Christian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermakeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder -> (Token -> [Rule], Rules, Set.Set Id)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermakeRules ga ps@(p, _) 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 ++
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder initRules ps builtinIds (Set.toList rIds)
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederinitRules (p, ps) 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))
2fc11b362b9242202bda207e7c7ecc7771f1a5e3Christian Maeder (filter isMixfix is)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder-- create fresh type vars for unknown ids tagged with type MixfixType [].
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederanaPattern :: Set.Set Id -> Pattern -> State Env Pattern
dcb9ff0e2c2379735acce7073196508d455e0b01Christian MaederanaPattern s pat =
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder QualVar vd -> do newVd <- checkVarDecl vd
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder return $ QualVar newVd
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder ResolvedMixTerm i pats ps | null pats &&
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
dcb9ff0e2c2379735acce7073196508d455e0b01Christian Maeder return $ ResolvedMixTerm i 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
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
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-- | put parenthesis around applications in equations
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian MaederparenProgEq :: ProgEq -> ProgEq
7e0b79aa73910981e12d1e237074c4e9b0b991dcChristian MaederparenProgEq (ProgEq p t q) = ProgEq (parenTerm p) (parenTerm t) q