MixAna.hs revision 6e2c88c65d50b2e44f7afa165e6a5fac0724f08c
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance{- |
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
5d801400993c9671010d244646936d8fd435638cChristian MaederDescription : mixfix analysis for terms
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceCopyright : (c) Christian Maeder and Uni Bremen 2003-2005
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
5d801400993c9671010d244646936d8fd435638cChristian MaederStability : experimental
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancePortability : portable
5d801400993c9671010d244646936d8fd435638cChristian Maeder
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel ManceMixfix analysis of terms and patterns, type annotations are also analysed
5d801400993c9671010d244646936d8fd435638cChristian Maeder-}
5d801400993c9671010d244646936d8fd435638cChristian Maeder
5d801400993c9671010d244646936d8fd435638cChristian Maedermodule HasCASL.MixAna
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ( resolve
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , anaPolyId
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance , makeRules
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , getPolyIds
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , iterateCharts
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder , toMixTerm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ) where
feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Mance
feab1106bbee4f2ea2fd48bca7106dd041e4211dFelix Gabriel Manceimport Common.GlobalAnnotations
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Result
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Id
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.DocUtils
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Earley
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Lexer
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Prec
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.ConvertMixfixToken
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Lib.State
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.AnnoState
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Common.Anno_Parser
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Manceimport qualified Data.Map as Map
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Data.Set as Set
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder
968930c7674ae3b63d308bf4fa651400aa263054Christian Maederimport HasCASL.As
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.AsUtils
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.PrintAs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.Unify
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.VarDecl
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.Le
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport HasCASL.ParseTerm
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maederimport HasCASL.TypeAna
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Text.ParserCombinators.Parsec as P
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Data.Maybe
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport Control.Exception (assert)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceaddType :: Term -> Term -> Term
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederaddType (MixTypeTerm q ty ps) t = TypedTerm t q ty ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceaddType _ _ = error "addType"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder-- | try to reparse terms as a compound list
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederisCompoundList :: Set.Set [Id] -> [Term] -> Bool
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceisCompoundList compIds =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance maybe False (flip Set.member compIds) . mapM reparseAsId
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceisTypeList :: Env -> [Term] -> Bool
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaederisTypeList e l = case mapM termToType l of
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder Nothing -> False
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder Just ts ->
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder let Result ds ml = mapM ( \ t -> anaTypeM (Nothing, t) e) ts
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder in isJust ml && not (hasErrors ds)
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancetermToType :: Term -> Maybe Type
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancetermToType t = case P.runParser ((case getPosList t of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [] -> return ()
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance p : _ -> P.setPosition $ fromPos p)
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder >> parseType << P.eof) (emptyAnnos ()) "" $ showDoc t "" of
806e8e0fe1a46ce1523c0d7804f1c193321f7981Christian Maeder Right x -> Just x
806e8e0fe1a46ce1523c0d7804f1c193321f7981Christian Maeder _ -> Nothing
806e8e0fe1a46ce1523c0d7804f1c193321f7981Christian Maeder
806e8e0fe1a46ce1523c0d7804f1c193321f7981Christian MaederanaPolyId :: PolyId -> TypeScheme -> State Env (Maybe TypeScheme)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceanaPolyId (PolyId i@(Id _ cs _) _ _) sc = do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance mSc <- anaTypeScheme sc
dd3c105fcc30b5d6b750d8fbe32250207b996109Felix Gabriel Mance case mSc of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> return Nothing
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just newSc@(TypeScheme tvars _ _) -> do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance e <- get
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let ids = Set.unions
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance [ Map.keysSet $ classMap e
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance , Map.keysSet $ typeMap e
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance , Map.keysSet $ assumps e ]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance es = filter (not . flip Set.member ids) cs
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance addDiags $ map (\ j -> mkDiag Warning
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance "unexpected identifier in compound list" j) es
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance if null cs || null tvars then return () else
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance addDiags [mkDiag Hint "is polymorphic compound identifier" i]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance return $ Just newSc
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel ManceresolveQualOp :: PolyId -> TypeScheme -> State Env TypeScheme
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceresolveQualOp i@(PolyId j _ _) sc = do
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder mSc <- anaPolyId i sc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance e <- get
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance case mSc of
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder Nothing -> return sc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just nSc -> do
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance case findOpId e j nSc of
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder Nothing -> addDiags [mkDiag Error "operation not found" j]
a921ae1da1302f673204e7b63cdce01439a9bd5eFelix Gabriel Mance _ -> return ()
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return nSc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceiterateCharts :: GlobalAnnos -> Set.Set [Id] -> [Term] -> Chart Term
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder -> State Env (Chart Term)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceiterateCharts ga compIds terms chart = do
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance e <- get
097bc9f18b722812d480df0f5c634d09cbca8e21Felix Gabriel Mance let self = iterateCharts ga compIds
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder oneStep = nextChart addType (toMixTerm e) ga chart
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder vs = localVars e
5d801400993c9671010d244646936d8fd435638cChristian Maeder tm = typeMap e
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance case terms of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance [] -> return chart
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance t : tt -> let recurse trm = self tt $ oneStep
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (trm, exprTok {tokPos = getRange trm}) in case t of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance MixfixTerm ts -> self (ts ++ tt) chart
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance MixTypeTerm q typ ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mTyp <- anaStarType typ
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance case mTyp of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Nothing -> recurse t
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just nTyp -> self tt $ oneStep
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (MixTypeTerm q (monoType nTyp) ps, typeTok {tokPos = ps})
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance BracketTerm b ts ps ->
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let bres = self (expandPos TermToken
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (getBrackets b) ts ps ++ tt) chart in case (b, ts) of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (Squares, _ : _) -> if isCompoundList compIds ts then do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance addDiags [mkDiag Hint "is compound list" t]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance bres
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else if isTypeList e ts then do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let testChart = oneStep (t, typeInstTok {tokPos = ps})
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder if null $ solveDiags testChart then do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance addDiags [mkDiag Hint "is type list" t]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance self tt testChart
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else bres
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance else bres
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> case (b, ts, tt) of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (Parens, [QualOp b2 v sc [] _ ps2], hd@(BracketTerm Squares
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ts2@(_ : _) ps3) : rtt) | isTypeList e ts2 -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance addDiags [mkDiag Hint "is type list" ts2]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance nSc <- resolveQualOp v sc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance self rtt $ oneStep
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ( QualOp b2 v nSc (bracketTermToTypes e hd) UserGiven ps2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , exprTok {tokPos = appRange ps ps3})
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder _ -> bres
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance QualVar (VarDecl v typ ok ps) -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mTyp <- anaStarType typ
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance recurse $ maybe t ( \ nType -> QualVar $ VarDecl v (monoType nType)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ok ps) mTyp
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance QualOp b v sc [] k ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance nSc <- resolveQualOp v sc
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance recurse $ QualOp b v nSc [] k ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance QuantifiedTerm quant decls hd ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance newDs <- mapM (anaddGenVarDecl False) decls
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mt <- resolve ga hd
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putLocalVars vs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance putTypeMap tm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance recurse $ QuantifiedTerm quant (catMaybes newDs) (maybe hd id mt) ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance LambdaTerm decls part hd ps -> do
962c83276bc80dd04f4a83e47eb81524d5294a4fChristian Maeder mDecls <- mapM (resolvePattern ga) decls
5d801400993c9671010d244646936d8fd435638cChristian Maeder let anaDecls = catMaybes mDecls
5d801400993c9671010d244646936d8fd435638cChristian Maeder bs = concatMap extractVars anaDecls
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder checkUniqueVars bs
5d801400993c9671010d244646936d8fd435638cChristian Maeder mapM_ (addLocalVar False) bs
5d801400993c9671010d244646936d8fd435638cChristian Maeder mt <- resolve ga hd
5d801400993c9671010d244646936d8fd435638cChristian Maeder putLocalVars vs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance CaseTerm hd eqs ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mt <- resolve ga hd
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance newEs <- resolveCaseEqs ga eqs
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance recurse $ CaseTerm (maybe hd id mt) newEs ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance LetTerm b eqs hd ps -> do
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder newEs <- resolveLetEqs ga eqs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mt <- resolve ga hd
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putLocalVars vs
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance recurse $ LetTerm b newEs (maybe hd id mt) ps
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance TermToken tok -> do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance let (ds1, trm) = convertMixfixToken (literal_annos ga)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance (flip ResolvedMixTerm []) TermToken tok
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance addDiags ds1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance self tt $ oneStep $ case trm of
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance TermToken _ -> (trm, tok)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> (trm, exprTok {tokPos = tokPos tok})
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance AsPattern vd p ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mp <- resolvePattern ga p
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance recurse $ AsPattern vd (maybe p id mp) ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance TypedTerm trm k ty ps -> do
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -- assume that type is analysed
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance mt <- resolve ga trm
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance recurse $ TypedTerm (maybe trm id mt) k ty ps
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> error ("iterCharts: " ++ show t)
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance-- * equation stuff
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceresolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceresolveCaseEq ga (ProgEq p t ps) = do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance mp <- resolvePattern ga p
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance case mp of
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Nothing -> return Nothing
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Just newP -> do
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance let bs = extractVars newP
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance checkUniqueVars bs
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance vs <- gets localVars
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder mapM_ (addLocalVar False) bs
a6526952d69bccd048c954eb920493a6a83e78faFelix Gabriel Mance mtt <- resolve ga t
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance putLocalVars vs
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance return $ case mtt of
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder Nothing -> Nothing
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Just newT -> Just $ ProgEq newP newT ps
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceresolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceresolveCaseEqs ga eqs = case eqs of
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder [] -> return []
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance eq : rt -> do
962c83276bc80dd04f4a83e47eb81524d5294a4fChristian Maeder mEq <- resolveCaseEq ga eq
5d801400993c9671010d244646936d8fd435638cChristian Maeder reqs <- resolveCaseEqs ga rt
5d801400993c9671010d244646936d8fd435638cChristian Maeder return $ case mEq of
5d801400993c9671010d244646936d8fd435638cChristian Maeder Nothing -> reqs
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance Just newEq -> newEq : reqs
1435782fda52a2898ea74e99088351d4f5b450dcChristian Maeder
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel ManceresolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel ManceresolveLetEqs _ [] = return []
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel ManceresolveLetEqs ga eqs = case eqs of
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder [] -> return []
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder ProgEq pat trm ps : rt -> do
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance mPat <- resolvePattern ga pat
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance case mPat of
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance Nothing -> do
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance resolve ga trm
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance resolveLetEqs ga rt
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance Just newPat -> do
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance let bs = extractVars newPat
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance checkUniqueVars bs
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance mapM_ (addLocalVar False) bs
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance mTrm <- resolve ga trm
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance case mTrm of
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance Nothing -> resolveLetEqs ga rt
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance Just newTrm -> do
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance reqs <- resolveLetEqs ga rt
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance return $ ProgEq newPat newTrm ps : reqs
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel MancemkPatAppl :: Term -> Term -> Range -> Term
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel MancemkPatAppl op arg qs = case op of
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance QualVar (VarDecl i (MixfixType []) _ _) -> ResolvedMixTerm i [] [arg] qs
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance _ -> ApplTerm op arg qs
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel MancebracketTermToTypes :: Env -> Term -> [Type]
1435782fda52a2898ea74e99088351d4f5b450dcChristian MaederbracketTermToTypes e t = case t of
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance BracketTerm Squares tys _ ->
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance map (monoType . snd) $ maybe (error "bracketTermToTypes") id $
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance maybeResult $ mapM ( \ ty -> anaTypeM (Nothing, ty) e) $
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance maybe (error "bracketTermToTypes1") id $ mapM termToType tys
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance _ -> error "bracketTermToTypes2"
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel MancetoMixTerm :: Env -> Id -> [Term] -> Range -> Term
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel MancetoMixTerm e i ar qs =
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance if i == applId then assert (length ar == 2) $
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance let [op, arg] = ar in mkPatAppl op arg qs
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance else if i == tupleId || i == unitId then
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance mkTupleTerm ar qs
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance else case unPolyId i of
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance Just j@(Id ts _ _) -> if isMixfix j && isSingle ar then
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance else assert (length ar == 1 + placeCount j) $
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance let (far, tar : sar) =
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance splitAt (placeCount $ mkId $ fst $ splitMixToken ts) ar
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs
bf47922605c34ddeb05f77188da395945ac2a2c8Felix Gabriel Mance _ -> ResolvedMixTerm i [] ar qs
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel MancegetKnowns :: Id -> Set.Set Token
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian MaedergetKnowns (Id ts cs _) =
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder Set.union (Set.fromList ts) $ Set.unions $ map getKnowns cs
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder
f853560cb2b56c631af268adec9dd0c1f518ffd8Felix Gabriel ManceresolvePattern :: GlobalAnnos -> Term -> State Env (Maybe Term)
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel ManceresolvePattern = resolver True
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maederresolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceresolve = resolver False
aa64389ee694577d9e665cf57331129000072a79Felix Gabriel Mance
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Manceresolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Manceresolver isPat ga trm = do
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder e <- get
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder let ass = assumps e
ba2c0d8be230f0b274cf3e0013e3844a80d9afd4Christian Maeder vs = localVars e
f853560cb2b56c631af268adec9dd0c1f518ffd8Felix Gabriel Mance ps = preIds e
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance compIds = getCompoundLists e
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance $ Set.union (Map.keysSet ass) $ Map.keysSet vs
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance let Result ds mr = getResolved (showDoc . parenTerm) (getRange trm)
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance (toMixTerm e) chart
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance addDiags ds
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance if isPat then case mr of
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance Nothing -> return mr
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance Just pat -> fmap Just $ anaPattern sIds pat
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance else return mr
f07079faf4e99014e900c7c99adb5ff7fa106b61Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancegetPolyIds :: Assumps -> Set.Set Id
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel MancegetPolyIds = Set.unions . map ( \ (i, s) ->
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance Set.fold ( \ oi -> case opType oi of
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance TypeScheme (_ : _) _ _ -> Set.insert i
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance _ -> id) Set.empty s) . Map.toList
a604cbad8e2202147b5c6bb9f2e06ae61162d654Felix Gabriel Mance
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel ManceuTok :: Token
968930c7674ae3b63d308bf4fa651400aa263054Christian MaederuTok = mkSimpleId "_"
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancebuiltinIds :: [Id]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancebuiltinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancemakeRules :: GlobalAnnos -> (PrecMap, Set.Set Id) -> Set.Set Id
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -> Set.Set Id -> (Token -> [Rule], Rules, Set.Set Id)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancemakeRules ga ps@(p, _) polyIds aIds =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance let (sIds, ids) = Set.partition isSimpleId aIds
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance ks = Set.fold (Set.union . getKnowns) Set.empty ids
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance rIds = Set.union ids $ Set.intersection sIds $ Set.map simpleIdToId ks
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder m2 = maxWeight p + 2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance in ( \ tok -> if isSimpleToken tok
ae9f6ee28850f767319629d3c2e28918698dce3bChristian Maeder && not (Set.member tok ks)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance || tok == uTok then
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance [(simpleIdToId tok, m2, [tok])] else []
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , partitionRules $ listRules m2 ga ++
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance initRules ps (Set.toList polyIds) builtinIds (Set.toList rIds)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance , sIds)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceinitRules :: (PrecMap, Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]
initRules (p, ps) polyIds bs is =
map ( \ i -> mixRule (getIdPrec p ps i) i)
(bs ++ is) ++
map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))
(filter isMixfix is) ++
-- identifiers with a positive number of type arguments
map ( \ i -> ( polyId i, getIdPrec p ps i
, getPolyTokenList i)) polyIds ++
map ( \ i -> ( protect $ polyId i, maxWeight p + 3
, getPlainPolyTokenList i)) (filter isMixfix polyIds)
-- create fresh type vars for unknown ids tagged with type MixfixType [].
anaPattern :: Set.Set Id -> Term -> State Env Term
anaPattern s pat = case pat of
QualVar vd -> do
newVd <- checkVarDecl vd
return $ QualVar newVd
ResolvedMixTerm i tys pats ps | null pats && null tys &&
(isSimpleId i || i == simpleIdToId uTok) &&
not (Set.member i s) -> do
(tvar, c) <- toEnvState $ freshVar i
return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps
| otherwise -> do
l <- mapM (anaPattern s) pats
return $ ResolvedMixTerm i tys 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) ->
return $ QualVar $ VarDecl v ty ok $ appRange qs ps
_ -> 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 v
return $ VarDecl v (TypeName tvar rStar c) ok ps
_ -> return vd