3fc67a2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix error with linearity checking in patterns

commit3fc67a2f0e83384c99e453e0ed133d6a4049adea authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 13 Mar 2013, 12:16 (14 years ago) parent9841e2a

10 files changed+66−17

compare with master

unifiedsplit

lib/Prelude.idr−1 lib/Prelude/Strings.idr+1−1 src/Idris/AbsSyntax.hs+33 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+16−12 src/Idris/Prover.hs+2 test/reg005/reg005.idr+2−2 test/reg010/expected+4 test/reg010/reg010.idr+5 test/reg010/run+2

lib/Prelude.idr−1

@@ -268,7 +268,6 @@ data Mode = Read | Write | ReadWrite

268268partial

269269openFile : String -> Mode -> IO File

270270openFile f m = fopen f (modeStr m) where

271− modeStr : Mode -> String

272271 modeStr Read = "r"

273272 modeStr Write = "w"

274273 modeStr ReadWrite = "r+"

lib/Prelude/Strings.idr+1−1

@@ -36,7 +36,7 @@ strM x with (choose (not (x == "")))

3636unpack : String -> List Char

3737unpack s with (strM s)

3838 unpack "" | StrNil = []

39− unpack (strCons x xs) | (StrCons _ xs) = x :: unpack xs

39+ unpack (strCons x xs) | (StrCons x xs) = x :: unpack xs

4040

4141pack : List Char -> String

4242pack [] = ""

src/Idris/AbsSyntax.hs+33

@@ -914,6 +914,39 @@ aiFn inpat expat ist fc f as

914914 | n == n' = Just (t, reverse acc ++ gs)

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

916916

917+-- replace non-linear occurrences with _

918+stripLinear :: IState -> PTerm -> PTerm

919+stripLinear i tm = evalState (sl tm) [] where

920+ sl :: PTerm -> State [Name] PTerm

921+ sl (PRef fc f)

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

923+ = return $ PRef fc f

924+ | otherwise = do ns <- get

925+ trace (show (f, ns)) $ if (f `elem` ns)

926+ then return Placeholder

927+ else do put (f : ns)

928+ return (PRef fc f)

929+ sl (PPatvar fc f)

930+ = do ns <- get

931+ if (f `elem` ns)

932+ then return Placeholder

933+ else do put (f : ns)

934+ return (PRef fc f)

935+ sl (PApp fc fn args) = do fn' <- sl fn

936+ args' <- mapM slA args

937+ return $ PApp fc fn' args'

938+ where slA (PImp p l n t d) = do t' <- sl t

939+ return $ PImp p l n t' d

940+ slA (PExp p l t d) = do t' <- sl t

941+ return $ PExp p l t' d

942+ slA (PConstraint p l t d)

943+ = do t' <- sl t

944+ return $ PConstraint p l t' d

945+ slA (PTacImplicit p l n sc t d)

946+ = do t' <- sl t

947+ return $ PTacImplicit p l n sc t' d

948+ sl x = return x

949+

917950mkPApp fc a f [] = f

918951mkPApp fc a f as = let rest = drop a as in

919952 appRest fc (PApp fc f (take a as)) rest

src/Idris/ElabDecls.hs+1−1

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

548548 [t] -> t

549549 _ -> []

550550 let params = getParamsInType i [] fn_is fn_ty

551− let lhs = addImplPat i (propagateParams params lhs_in)

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

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

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

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

src/Idris/ElabTerm.hs+16−12

@@ -198,19 +198,23 @@ elab ist info pattern tcgen fn tm

198198 trySeq' deferr (x : xs)

199199 = try' (elab' ina x) (trySeq' deferr xs) True

200200 elab' ina (PPatvar fc n) | pattern = patvar n

201+-- = do env <- get_env

202+-- case lookup n env of

203+-- Just (PVar _) -> elab' ina Placeholder

204+-- _ -> patvar n

201205 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

202− = do ctxt <- get_context

203− let iscon = isConName Nothing n ctxt

204− let defined = case lookupTy Nothing n ctxt of

205− [] -> False

206− _ -> True

207− -- this is to stop us resolve type classes recursively

208− -- trace (show (n, guarded)) $

209− if (tcname n && ina) then erun fc $ patvar n

210− else if (defined && not guarded)

211− then do apply (Var n) []; solve

212− else try (do apply (Var n) []; solve)

213− (patvar n)

206+ = do ctxt <- get_context

207+ env <- get_env

208+ let defined = case lookupTy Nothing n ctxt of

209+ [] -> False

210+ _ -> True

211+ -- this is to stop us resolve type classes recursively

212+ -- trace (show (n, guarded)) $

213+ if (tcname n && ina) then erun fc $ patvar n

214+ else if (defined && not guarded)

215+ then do apply (Var n) []; solve

216+ else try (do apply (Var n) []; solve)

217+ (patvar n)

214218 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

215219 [] -> False

216220 _ -> True

src/Idris/Prover.hs+2

@@ -20,6 +20,7 @@ import System.Console.Haskeline.History

2020import Control.Monad.State

2121

2222import Util.Pretty

23+import Debug.Trace

2324

2425prover :: Bool -> Name -> Idris ()

2526prover lit x =

@@ -159,6 +160,7 @@ ploop d prompt prf e h

159160 return (False, e, True, prf)

160161 Right tac -> do (_, e) <- elabStep e saveState

161162 (_, st) <- elabStep e (runTac True i tac)

163+-- trace (show (problems (proof st))) $

162164 return (True, st, False, prf ++ [step]))

163165 (\err -> do iputStrLn (show err)

164166 return (False, e, False, prf))

test/reg005/reg005.idr+2−2

@@ -20,7 +20,7 @@ rle [] = REnd

2020rle (x :: xs) with (rle xs)

2121 rle (x :: Vect.Nil) | REnd = RChar O x REnd

2222 rle (x :: rep (S n) yvar ++ ys) | RChar n yvar rs with (eq x yvar)

23− rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just p

23+ rle (x :: rep (S n) x ++ ys) | RChar n x rs | Just refl

2424 = RChar (S n) x rs

2525 rle (x :: rep (S n) y ++ ys) | RChar n y rs | Nothing

2626 = RChar O x (RChar n y rs)

@@ -28,7 +28,7 @@ rle (x :: xs) with (rle xs)

2828compress : Vect Char n -> String

2929compress xs with (rle xs)

3030 compress Nil | REnd = ""

31− compress (rep (S n) x ++ xs) | RChar n x rs

31+ compress (rep (S n) x ++ xs) | RChar _ _ rs

3232 = let ni : Int = cast (S n) in

3333 show ni ++ show x ++ compress xs

3434

test/reg010/expectednew file+4

@@ -0,0 +1,4 @@

1+reg010.idr:5:Can't unify P x with P y

3+Specifically:

4+ Can't unify x with y

test/reg010/reg010.idrnew file+5

@@ -0,0 +1,5 @@

1+module usubst

3+total unsafeSubst : (P : a -> Type) -> (x : a) -> (y : a) -> P x -> P y

4+unsafeSubst P x y px with (O)

5+ unsafeSubst P x x px | _ = px

test/reg010/runnew file+2

@@ -0,0 +1,2 @@

1+#!/bin/bash

2+idris $@ reg010.idr --check