c1d71ac637c449feb0a25369f029397e6a1f241cChristian Maeder

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder{- |

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederModule : $Header$

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederStability : experimental

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaederMixfix analysis of terms and patterns, type annotations are also analysed

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-}

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maedermodule HasCASL.MixAna where

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.GlobalAnnotations

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.Result

5c602504f85bbac7ddf0226064452bdc7d4a8cd8Till Mossakowskiimport Common.Id

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.Keywords

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport qualified Common.Lib.Map as Map

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport qualified Common.Lib.Set as Set

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskiimport Common.Earley

ae7058143db9e9993b5eff70bd6b7aede7cec658Till Mossakowskiimport Common.ConvertLiteral

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport Common.Lib.State

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.As

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.AsUtils

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.VarDecl

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.Le

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maederimport HasCASL.Unify

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maederimport HasCASL.TypeAna

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederimport Data.Maybe

53310804002cd9e3c9c5844db3b984abcf001788Christian Maederimport Control.Exception(assert)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maedertype Rule = (Id, Int, [Token])

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiopKindFilter :: Int -> Int -> Maybe Bool

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian MaederopKindFilter arg op =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if op < arg then Just True

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski else if arg < op then Just False

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski else Nothing

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedergetIdPrec :: PrecMap -> Set.Set Id -> Id -> Int

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskigetIdPrec (pm, r, m) ps i = Map.findWithDefault

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (if begPlace i || endPlace i then if Set.member i ps then r else m - 1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski else m + 1) i pm

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiaddType :: Term -> Term -> Term

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederaddType (TypedTerm _ q ty ps) p = TypedTerm p q ty ps

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiaddType _ _ = error "addType"

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowskitype TermChart = Chart Term Int

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski-- | find information for qualified operation

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskifindOpId :: Assumps -> TypeMap -> Int -> UninstOpId -> Type -> Maybe OpInfo

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till MossakowskifindOpId as tm c i ty = listToMaybe $ fst $

2ecf6cfb90e84d40f224cda5d92c191182c976d2Till Mossakowski partitionOpId as tm c i $ TypeScheme [] ([] :=> ty) []

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiiterateCharts :: GlobalAnnos -> [Term] -> TermChart

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder -> State Env TermChart

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiiterateCharts ga terms chart =

5d6e7ea3bd14fc987436cff0f542393ea9ba34bbTill Mossakowski do e <- get

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder let self = iterateCharts ga

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder oneStep = nextChart addType opKindFilter

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder toMixTerm ga chart

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski as = assumps e

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tm = typeMap e

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if null terms then return chart else

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder do let t:tt = terms

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski recurse trm = self tt $

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski oneStep (trm, exprTok {tokPos = posOfTerm trm})

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski case t of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski MixfixTerm ts -> self (ts ++ tt) chart

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder TypedTerm hd q typ ps -> do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder mp <- resolvePattern ga hd

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let np = case mp of Just pt -> pt

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ -> t

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder recurse $ TypedTerm np q typ ps

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder MixTypeTerm q typ ps -> do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder mTyp <- anaStarType typ

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case mTyp of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder Nothing -> recurse t

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder Just nTyp -> self tt $ oneStep

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (MixTypeTerm q nTyp ps,

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder typeTok {tokPos = headPos ps})

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder BracketTerm b ts ps -> self

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (expandPos TermToken (getBrackets b) ts ps ++ tt) chart

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder QualVar v typ ps -> do

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder mTyp <- anaStarType typ

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder case mTyp of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Nothing -> recurse t

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Just nTyp -> do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let mi = findOpId as tm (counter e) v nTyp

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case mi of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Nothing -> addDiags [mkDiag Error

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder "value not found" v]

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ -> return ()

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder recurse $ QualVar v nTyp ps

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder QualOp b io@(InstOpId v _ _)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (TypeScheme rs (qs :=> typ) ss) ps -> do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder mTyp <- anaStarType typ

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case mTyp of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Nothing -> recurse t

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Just nTyp -> do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let mi = findOpId as tm (counter e) v nTyp

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder case mi of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder Nothing -> addDiags [mkDiag Error

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder "value not found" v]

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ -> return ()

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder recurse $ QualOp b io

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (TypeScheme rs (qs :=> nTyp) ss) ps

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder QuantifiedTerm quant decls hd ps -> do

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder newDs <- mapM anaGenVarDecl decls

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder mt <- resolve ga hd

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder putAssumps as

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder putTypeMap tm

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let newT = case mt of Just trm -> trm

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ -> hd

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder LambdaTerm decls part hd ps -> do

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder mDecls <- mapM (resolvePattern ga) decls

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder let newDecls = catMaybes mDecls

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder l <- mapM extractBindings newDecls

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder let bs = concatMap snd l

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder checkUniqueVars bs

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder mapM_ addVarDecl bs

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder mt <- resolve ga hd

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder putAssumps as

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder let newT = case mt of Just trm -> trm

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder _ -> hd

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder recurse $ LambdaTerm (map fst l) part newT ps

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder CaseTerm hd eqs ps -> do

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder mt <- resolve ga hd

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder let newT = case mt of Just trm -> trm

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder _ -> hd

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder newEs <- resolveCaseEqs ga eqs

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder recurse $ CaseTerm newT newEs ps

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder LetTerm b eqs hd ps -> do

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder newEs <- resolveLetEqs ga eqs

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder mt <- resolve ga hd

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder let newT = case mt of Just trm -> trm

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder _ -> hd

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder putAssumps as

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder recurse $ LetTerm b newEs newT ps

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder TermToken tok -> do

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder let (ds1, trm) = convertMixfixToken

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (literal_annos ga)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder ResolvedMixTerm TermToken tok

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder addDiags ds1

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder self tt $ oneStep $

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder case trm of

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder TermToken _ -> (trm, tok)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder _ -> (trm, exprTok

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder {tokPos = tokPos tok})

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder _ -> error ("iterCharts: " ++ show t)

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder-- * equation stuff

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederresolveCaseEq ga (ProgEq p t ps) =

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder do mp <- resolvePattern ga p

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case mp of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Nothing -> return Nothing

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski Just np -> do

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski as <- gets assumps

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski (newP, bs) <- extractBindings np

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski checkUniqueVars bs

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski mapM_ addVarDecl bs

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mtt <- resolve ga t

797595aad6dfd626bc1c9df52616f1ac4235c669Till Mossakowski putAssumps as

933baca0720dae81434de384b32a93b47e754d09Christian Maeder return $ case mtt of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Nothing -> Nothing

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just newT -> Just $ ProgEq newP newT ps

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

586af0e9490a14dd3075095692b584c652584875Till MossakowskiresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederresolveCaseEqs _ [] = return []

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian MaederresolveCaseEqs ga (eq:rt) =

933baca0720dae81434de384b32a93b47e754d09Christian Maeder do mEq <- resolveCaseEq ga eq

933baca0720dae81434de384b32a93b47e754d09Christian Maeder eqs <- resolveCaseEqs ga rt

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return $ case mEq of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Nothing -> eqs

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just newEq -> newEq : eqs

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

586af0e9490a14dd3075095692b584c652584875Till MossakowskiresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiresolveLetEqs _ [] = return []

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskiresolveLetEqs ga (ProgEq pat trm ps : rt) =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do mPat <- resolvePattern ga pat

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski case mPat of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Nothing -> do resolve ga trm

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder resolveLetEqs ga rt

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just nPat -> do

933baca0720dae81434de384b32a93b47e754d09Christian Maeder (newPat, bs) <- extractBindings nPat

933baca0720dae81434de384b32a93b47e754d09Christian Maeder checkUniqueVars bs

933baca0720dae81434de384b32a93b47e754d09Christian Maeder mapM addVarDecl bs

f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski mTrm <- resolve ga trm

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder case mTrm of

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder Nothing -> resolveLetEqs ga rt

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder Just newTrm -> do

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder eqs <- resolveLetEqs ga rt

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski return (ProgEq newPat newTrm ps : eqs)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder-- * pattern stuff

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder-- | extract bindings from a pattern

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian MaederextractBindings :: Pattern -> State Env (Pattern, [VarDecl])

53310804002cd9e3c9c5844db3b984abcf001788Christian MaederextractBindings pat =

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder case pat of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski QualVar v t ps -> case t of

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder MixfixType [] ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski do tvar <- toEnvState freshVar

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let ty = TypeName tvar star 1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski return (QualVar v ty ps, [VarDecl v ty Other ps])

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski _ -> do mt <- anaStarType t

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case mt of

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Just ty ->

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder return (QualVar v ty ps, [VarDecl v ty Other ps])

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder _ -> return (pat, [])

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ResolvedMixTerm i pats ps -> do

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski l <- mapM extractBindings pats

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder return (ResolvedMixTerm i (map fst l) ps, concatMap snd l)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ApplTerm p1 p2 ps -> do

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (p3, l1) <- extractBindings p1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (p4, l2) <- extractBindings p2

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder return (ApplTerm p3 p4 ps, l1 ++ l2)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder TupleTerm pats ps -> do

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski l <- mapM extractBindings pats

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder return (TupleTerm (map fst l) ps, concatMap snd l)

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski TypedTerm p q ty ps -> do

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder mt <- anaStarType ty

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill Mossakowski let newT = case mt of Just t -> t

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder _ -> ty

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case p of

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder QualVar v (MixfixType []) _ ->

f2a87c712ea3cd13f86a95cae738f861f6c4a908Till Mossakowski return (QualVar v newT ps, [VarDecl v newT Other ps])

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder _ -> do (newP, bs) <- extractBindings p

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder return (TypedTerm newP q newT ps, bs)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski AsPattern p1 p2 ps -> do

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (p3, l1) <- extractBindings p1

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (p4, l2) <- extractBindings p2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder return (AsPattern p3 p4 ps, l1 ++ l2)

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder _ -> return (pat, [])

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian MaedermkPatAppl :: Pattern -> Pattern -> [Pos] -> Pattern

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimkPatAppl op arg qs =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder case op of

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder QualVar i (MixfixType []) _ ->

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian Maeder ResolvedMixTerm i [arg] qs

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder _ -> ApplTerm op arg qs

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaedertoMixTerm :: Id -> Int -> [Pattern] -> [Pos] -> Pattern

5bb3727ef464d9f08ab0decb2d4a59c1352a389eChristian MaedertoMixTerm i _ ar qs =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder if i == applId then assert (length ar == 2) $

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder let [op, arg] = ar in mkPatAppl op arg qs

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder else if i == tupleId || i == unitId then

9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski mkTupleTerm ar qs

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder else if isUnknownId i then

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski QualVar (simpleIdToId $ unToken i)

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder (MixfixType []) qs

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder else ResolvedMixTerm i ar qs

0647a6c86b231e391826c7715338ba29cb4934c0Christian Maeder

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedergetKnowns :: Id -> Knowns

0647a6c86b231e391826c7715338ba29cb4934c0Christian MaedergetKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Set.unions (map getKnowns cs)

933baca0720dae81434de384b32a93b47e754d09Christian Maeder

resolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)

resolvePattern ga = resolver ga (unknownId : builtinIds)

resolve :: GlobalAnnos -> Term -> State Env (Maybe Term)

resolve ga = resolver ga builtinIds

resolver :: GlobalAnnos -> [Id] -> Term

-> State Env (Maybe Term)

resolver ga bs trm =

do as <- gets assumps

ps@((_, _, m), _) <- gets preIds

let ids = Map.keys as

ks = Set.union (Set.fromList (tokStr exprTok: inS :

map (:[]) "{}[](),"))

$ Set.unions $ map getKnowns ids

chart<- iterateCharts ga [trm] $

initChart (listRules (m+2) ga ++

(initRules ps bs

ids)) (if unknownId `elem` bs then ks else Set.empty)

let Result ds mr = getResolved showPretty (posOfTerm trm)

toMixTerm chart

addDiags ds

return mr

builtinIds :: [Id]

builtinIds = [unitId, parenId, tupleId, exprId, typeId, applId]

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 + 2, getPlainTokenList i))

(filter isMixfix is)