MixAna.hs revision eed6203a39f88e398d86431a66d367036a3d17ba
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : maeder@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederMixfix analysis of terms and patterns, type annotations are also analysed
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Rel as Rel
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Set as Set
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaedergetIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaedergetIdPrec (pm, r, m) ps i = if i == applId then m + 1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (if begPlace i || endPlace i then if Set.member i ps then r else m
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else m + 2) i pm
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederaddType :: Term -> Term -> Term
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichaddType _ _ = error "addType"
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichtype TermChart = Chart Term
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichiterateCharts :: GlobalAnnos -> [Term] -> TermChart
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich -> State Env TermChart
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus LuettichiterateCharts ga terms chart =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let self = iterateCharts ga
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski oneStep = nextChart addType toMixTerm ga chart
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder vs = localVars e
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder tm = typeMap e
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if null terms then return chart else
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu do let t:tt = terms
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski recurse trm = self tt $
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski oneStep (trm, exprTok {tokPos = posOfTerm trm})
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder MixfixTerm ts -> self (ts ++ tt) chart
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder MixTypeTerm q typ ps -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mTyp <- anaStarType typ
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> recurse t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just nTyp -> self tt $ oneStep
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (MixTypeTerm q (monoType nTyp) ps,
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder typeTok {tokPos = ps})
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder BracketTerm b ts ps -> self
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (expandPos TermToken (getBrackets b) ts ps ++ tt) chart
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder QualVar (VarDecl v typ ok ps) -> do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder mTyp <- anaStarType typ
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Nothing -> recurse t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just nType -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let nTyp = monoType nType
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder mi = findOpId e v $ simpleTypeScheme nTyp
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Nothing -> addDiags [mkDiag Error
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski "value not found" v]
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder _ -> return ()
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder recurse $ QualVar $ VarDecl v nTyp ok ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder QualOp b (InstOpId v ts qs) sc ps -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mSc <- anaTypeScheme sc
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder newTs <- anaInstTypes ts
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> recurse t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just nSc -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let mi = findOpId e v nSc
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> addDiags [mkDiag Error
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder "value not found" v]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> return ()
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski recurse $ QualOp b (InstOpId v newTs qs) nSc ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski QuantifiedTerm quant decls hd ps -> do
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder newDs <- mapM (anaddGenVarDecl False) decls
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mt <- resolve ga hd
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putLocalVars vs
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder putTypeMap tm
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let newT = case mt of Just trm -> trm
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder LambdaTerm decls part hd ps -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mDecls <- mapM (resolvePattern ga) decls
26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder let anaDecls = catMaybes mDecls
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder bs = concatMap extractVars anaDecls
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder checkUniqueVars bs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapM_ (addLocalVar False) bs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mt <- resolve ga hd
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putLocalVars vs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let newT = case mt of Just trm -> trm
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder recurse $ LambdaTerm anaDecls part newT ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder CaseTerm hd eqs ps -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mt <- resolve ga hd
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let newT = case mt of Just trm -> trm
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newEs <- resolveCaseEqs ga eqs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder recurse $ CaseTerm newT newEs ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski LetTerm b eqs hd ps -> do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder newEs <- resolveLetEqs ga eqs
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mt <- resolve ga hd
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let newT = case mt of Just trm -> trm
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder putLocalVars vs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder recurse $ LetTerm b newEs newT ps
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder TermToken tok -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let (ds1, trm) = convertMixfixToken
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (literal_annos ga)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski ResolvedMixTerm TermToken tok
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder self tt $ oneStep $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder TermToken _ -> (trm, tok)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> (trm, exprTok
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder {tokPos = tokPos tok})
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder AsPattern vd p ps -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mp <- resolvePattern ga p
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let newP = case mp of Just pat -> pat
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder recurse $ AsPattern vd newP ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski TypedTerm trm k ty ps -> do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- assume that type is analysed
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mt <- resolve ga trm
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let newT = case mt of Just tr -> tr
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> trm
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski recurse $ TypedTerm newT k ty ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> error ("iterCharts: " ++ show t)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- * equation stuff
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederresolveCaseEq ga (ProgEq p t ps) =
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder do mp <- resolvePattern ga p
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> return Nothing
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just newP -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let bs = extractVars newP
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder checkUniqueVars bs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder vs <- gets localVars
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapM_ (addLocalVar False) bs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mtt <- resolve ga t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder putLocalVars vs
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ case mtt of
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Nothing -> Nothing
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Just newT -> Just $ ProgEq newP newT ps
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiresolveCaseEqs _ [] = return []
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederresolveCaseEqs ga (eq:rt) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski do mEq <- resolveCaseEq ga eq
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder eqs <- resolveCaseEqs ga rt
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ case mEq of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> eqs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just newEq -> newEq : eqs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederresolveLetEqs _ [] = return []
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederresolveLetEqs ga (ProgEq pat trm ps : rt) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do mPat <- resolvePattern ga pat
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> do resolve ga trm
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski resolveLetEqs ga rt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just newPat -> do
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let bs = extractVars newPat
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder checkUniqueVars bs
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder mapM_ (addLocalVar False) bs
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder mTrm <- resolve ga trm
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> resolveLetEqs ga rt
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Just newTrm -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder eqs <- resolveLetEqs ga rt
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (ProgEq newPat newTrm ps : eqs)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermkPatAppl :: Term -> Term -> Range -> Term
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermkPatAppl op arg qs =
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian Maeder QualVar (VarDecl i (MixfixType []) _ _) ->
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ResolvedMixTerm i [arg] qs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder _ -> ApplTerm op arg qs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertoMixTerm :: Id -> [Term] -> Range -> Term
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertoMixTerm i ar qs =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder if i == applId then assert (length ar == 2) $
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let [op, arg] = ar in mkPatAppl op arg qs
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else if i == tupleId || i == unitId then
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mkTupleTerm ar qs
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else if isUnknownId i then
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder QualVar $ VarDecl (simpleIdToId $ unToken i)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (MixfixType []) Other qs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else ResolvedMixTerm i ar qs
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedergetKnowns :: Id -> Knowns
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Set.unions (map getKnowns cs)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederresolvePattern ga p = do
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mp <- resolver ga (unknownId : builtinIds) p
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Nothing -> return Nothing
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Just np -> fmap Just $ anaPattern np
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederresolve ga = resolver ga builtinIds
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederresolver :: GlobalAnnos -> [Id] -> Term
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -> State Env (Maybe Term)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maederresolver ga bs trm =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do ass <- gets assumps
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder vs <- gets localVars
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder ps@((_, _, m), _) <- gets preIds
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder let ids = Set.toList $ Set.union (Rel.keysSet ass) $ Rel.keysSet vs
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder ks = Set.union (Set.fromList (tokStr exprTok: inS :
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder map (:[]) ":{}[](),"))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ Set.unions $ map getKnowns ids
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder chart<- iterateCharts ga [trm] $
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder initChart (listRules (m + 3) ga ++
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (initRules ps bs
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ids)) (if unknownId `elem` bs then ks else Set.empty)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder let Result ds mr = getResolved showPretty (posOfTerm trm)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder toMixTerm chart
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederbuiltinIds :: [Id]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederbuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Rule]
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederinitRules (pm@(_, _, m), ps) bs is =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder map ( \ i -> mixRule (getIdPrec pm ps i) i)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (bs ++ is) ++
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder map ( \ i -> (protect i, m + 3, getPlainTokenList i))
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (filter isMixfix is)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- create fresh type vars for unknown ids tagged with type MixfixType [].
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederanaPattern :: Pattern -> State Env Pattern
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederanaPattern pat =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder QualVar vd -> do newVd <- checkVarDecl vd
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ QualVar newVd
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ResolvedMixTerm i pats ps -> do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder l <- mapM anaPattern pats
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ ResolvedMixTerm i l ps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ApplTerm p1 p2 ps -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder p3 <- anaPattern p1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder p4 <- anaPattern p2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ ApplTerm p3 p4 ps
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder TupleTerm pats ps -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder l <- mapM anaPattern pats
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return $ TupleTerm l ps
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski TypedTerm p q ty ps -> do
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder QualVar (VarDecl v (MixfixType []) ok qs) ->
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski let newVd = VarDecl v ty ok (qs `appRange` ps) in
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder return $ QualVar newVd
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder _ -> do newP <- anaPattern p
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ TypedTerm newP q ty ps
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder AsPattern vd p2 ps -> do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder newVd <- checkVarDecl vd
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder p4 <- anaPattern p2
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder return $ AsPattern newVd p4 ps
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder _ -> return pat
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder where checkVarDecl vd@(VarDecl v t ok ps) = case t of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder MixfixType [] -> do
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (tvar, c) <- toEnvState $ freshVar $ posOfId v
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return $ VarDecl v (TypeName tvar rStar c) ok ps
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder _ -> return vd