git.iko.soy/Idris-dev
on master help sign in
Exact name lookups in getArity.
commit171e45bf55ec6a2171f3615e14fd619ede0f570b authorMatus Tejiscak <ziman@functor.sk> dateThu 3 Apr 2014, 11:46 (13 years ago) parent7c9b73b
3 files changed+21−17
compare with master
unifiedsplit
src/IRTS/Compiler.hs+7−7 src/Idris/Core/Evaluate.hs+6−2 src/Idris/Erasure.hs+8−8
src/IRTS/Compiler.hs+7−7
@@ -304,13 +304,13 @@ irTerm vs env tm@(App f a) = case unApply tm of
304304 | i >= arity || i `elem` used = x
305305 | otherwise = Erased
306306
307− arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
308− [CaseOp ci ty tys def tot cdefs] -> length tys
309− [TyDecl (DCon tag ar) _] -> ar
310− [TyDecl Ref ty] -> length $ getArgTys ty
311− [Operator ty ar op] -> ar
312− [] -> 0 -- no definition, probably local name => can't erase anything
313− def -> error $ "unknown arity: " ++ show (n, def)
307+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
308+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
309+ Just (TyDecl (DCon tag ar) _) -> ar
310+ Just (TyDecl Ref ty) -> length $ getArgTys ty
311+ Just (Operator ty ar op) -> ar
312+ Just def -> error $ "unknown arity: " ++ show (n, def)
313+ Nothing -> 0 -- no definition, probably local name => can't erase anything
314314
315315 -- name for purposes of usage info lookup
316316 uName
src/Idris/Core/Evaluate.hs+6−2
@@ -8,12 +8,13 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
88 Context, initContext, ctxtAlist, uconstraints, next_tvar,
99 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
1010 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
11+ lookupNames, lookupTy, lookupP, lookupDef, lookupDefExact, lookupDefAcc, lookupVal,
1212 mapDefCtxt,
1313 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
1414 Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where
1515
1616import Debug.Trace
17+import Control.Applicative hiding (Const)
1718import Control.Monad.State -- not Strict!
1819import qualified Data.Binary as B
1920import Data.Binary hiding (get, put)
@@ -909,8 +910,11 @@ lookupP n ctxt
909910 Hidden -> []
910911 _ -> return (fst p)
911912
913+lookupDefExact :: Name -> Context -> Maybe Def
914+lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
915+
912916lookupDef :: Name -> Context -> [Def]
913−lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)
917+lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)
914918
915919lookupDefAcc :: Name -> Bool -> Context ->
916920 [(Def, Accessibility)]
src/Idris/Erasure.hs+8−8
@@ -462,14 +462,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
462462
463463 | otherwise = error $ "unknown instance constructor: " ++ show ctorName
464464
465− getArity n = case lookupDef n ctx of
466− [CaseOp ci ty tys def tot cdefs] -> length tys
467− [TyDecl (DCon tag arity) _] -> arity
468− [TyDecl (Ref) ty] -> length $ getArgTys ty
469− [Operator ty arity op] -> arity
470− [] -> error $ "Erasure/getArity: definition not found for " ++ show n
471− df -> error $ "Erasure/getArity: unrecognised entity '"
472− ++ show n ++ "' with definition: " ++ show df
465+ getArity n = case lookupDefExact n ctx of
466+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
467+ Just (TyDecl (DCon tag arity) _) -> arity
468+ Just (TyDecl (Ref) ty) -> length $ getArgTys ty
469+ Just (Operator ty arity op) -> arity
470+ Just df -> error $ "Erasure/getArity: unrecognised entity '"
471+ ++ show n ++ "' with definition: " ++ show df
472+ Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n
473473
474474 -- convert applications of lambdas to lets
475475 -- Note that this transformation preserves de bruijn numbering