git.iko.soy/Idris-dev
on master help sign in
Exact name lookups in getArity.
171e45bMatus Tejiscak
src/IRTS/Compiler.hs+7−7
compare with master
unifiedsplit
@@ -304,13 +304,13 @@ irTerm vs env tm@(App f a) = case unApply tm of
304 | i >= arity || i `elem` used = x
304 | i >= arity || i `elem` used = x
305 | otherwise = Erased
305 | otherwise = Erased
306
306
307− arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
307+ arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
308− [CaseOp ci ty tys def tot cdefs] -> length tys
308+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
309− [TyDecl (DCon tag ar) _] -> ar
309+ Just (TyDecl (DCon tag ar) _) -> ar
310− [TyDecl Ref ty] -> length $ getArgTys ty
310+ Just (TyDecl Ref ty) -> length $ getArgTys ty
311− [Operator ty ar op] -> ar
311+ Just (Operator ty ar op) -> ar
312+ Just def -> error $ "unknown arity: " ++ show (n, def)
312− [] -> 0 -- no definition, probably local name => can't erase anything
313+ Nothing -> 0 -- no definition, probably local name => can't erase anything
313− def -> error $ "unknown arity: " ++ show (n, def)
314
314
315 -- name for purposes of usage info lookup
315 -- name for purposes of usage info lookup
316 uName
316 uName
src/Idris/Core/Evaluate.hs+6−2
@@ -8,12 +8,13 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
11− lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
11+ lookupNames, lookupTy, lookupP, lookupDef, lookupDefExact, lookupDefAcc, lookupVal,
12 mapDefCtxt,
12 mapDefCtxt,
13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
14 Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where
14 Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where
15
15
16import Debug.Trace
16import Debug.Trace
17+import Control.Applicative hiding (Const)
17import Control.Monad.State -- not Strict!
18import Control.Monad.State -- not Strict!
18import qualified Data.Binary as B
19import qualified Data.Binary as B
19import Data.Binary hiding (get, put)
20import Data.Binary hiding (get, put)
@@ -909,8 +910,11 @@ lookupP n ctxt
909 Hidden -> []
910 Hidden -> []
910 _ -> return (fst p)
911 _ -> return (fst p)
911
912
913+lookupDefExact :: Name -> Context -> Maybe Def
914+lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
915+
912lookupDef :: Name -> Context -> [Def]
916lookupDef :: Name -> Context -> [Def]
913−lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)
917+lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)
914
918
915lookupDefAcc :: Name -> Bool -> Context ->
919lookupDefAcc :: Name -> Bool -> Context ->
916 [(Def, Accessibility)]
920 [(Def, Accessibility)]
src/Idris/Erasure.hs+8−8
@@ -462,14 +462,14 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
462
462
463 | otherwise = error $ "unknown instance constructor: " ++ show ctorName
463 | otherwise = error $ "unknown instance constructor: " ++ show ctorName
464
464
465− getArity n = case lookupDef n ctx of
465+ getArity n = case lookupDefExact n ctx of
466− [CaseOp ci ty tys def tot cdefs] -> length tys
466+ Just (CaseOp ci ty tys def tot cdefs) -> length tys
467− [TyDecl (DCon tag arity) _] -> arity
467+ Just (TyDecl (DCon tag arity) _) -> arity
468− [TyDecl (Ref) ty] -> length $ getArgTys ty
468+ Just (TyDecl (Ref) ty) -> length $ getArgTys ty
469− [Operator ty arity op] -> arity
469+ Just (Operator ty arity op) -> arity
470− [] -> error $ "Erasure/getArity: definition not found for " ++ show n
471− df -> error $ "Erasure/getArity: unrecognised entity '"
470+ Just df -> error $ "Erasure/getArity: unrecognised entity '"
472− ++ show n ++ "' with definition: " ++ show df
471+ ++ show n ++ "' with definition: " ++ show df
472+ Nothing -> error $ "Erasure/getArity: definition not found for " ++ show n
473
473
474 -- convert applications of lambdas to lets
474 -- convert applications of lambdas to lets
475 -- Note that this transformation preserves de bruijn numbering
475 -- Note that this transformation preserves de bruijn numbering