83b7ae5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak linearity checker to deal with overloaded names properly

commit83b7ae5e06c37729b71712e713e8dd9a48dab606 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 22 Mar 2013, 22:10 (14 years ago) parent22001e5

2 files changed+5−2

unifiedsplit

src/Idris/AbsSyntax.hs+4−1

@@ -942,6 +942,9 @@ aiFn inpat expat ist fc f as

942942 find n (g : gs) acc = find n gs (g : acc)

943943

944944-- replace non-linear occurrences with _

945+-- ASSUMPTION: This is called before adding 'alternatives' because otherwise

946+-- it is hard to get right!

947+

945948stripLinear :: IState -> PTerm -> PTerm

946949stripLinear i tm = evalState (sl tm) [] where

947950 sl :: PTerm -> State [Name] PTerm

@@ -949,7 +952,7 @@ stripLinear i tm = evalState (sl tm) [] where

949952 | (_:_) <- lookupTy Nothing f (tt_ctxt i)

950953 = return $ PRef fc f

951954 | otherwise = do ns <- get

952− trace (show (f, ns)) $ if (f `elem` ns)

955+ if (f `elem` ns)

953956 then return Placeholder

954957 else do put (f : ns)

955958 return (PRef fc f)

src/Idris/ElabDecls.hs+1−1

@@ -576,7 +576,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

576576 [t] -> t

577577 _ -> []

578578 let params = getParamsInType i [] fn_is fn_ty

579− let lhs = stripLinear i $ addImplPat i (propagateParams params lhs_in)

579+ let lhs = addImplPat i (propagateParams params (stripLinear i lhs_in))

580580 logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)

581581 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

582582 ((lhs', dlhs, []), _) <-