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

git.iko.soy/Idris-dev

on master help sign in

Tweak linearity checker to deal with overloaded names properly

83b7ae5Edwin Brady14 years ago

src/Idris/AbsSyntax.hs+4−1

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

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

943

944-- replace non-linear occurrences with _

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

946+-- it is hard to get right!

947+

945stripLinear :: IState -> PTerm -> PTerm

948stripLinear :: IState -> PTerm -> PTerm

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

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

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

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

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

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

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

950 = return $ PRef fc f

953 = return $ PRef fc f

951 | otherwise = do ns <- get

954 | otherwise = do ns <- get

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

955+ if (f `elem` ns)

953 then return Placeholder

956 then return Placeholder

954 else do put (f : ns)

957 else do put (f : ns)

955 return (PRef fc f)

958 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)

576 [t] -> t

577 _ -> []

578 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))

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

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

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