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

lib/Prelude.idr−1

compare with master

unifiedsplit

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

268partial

269openFile : String -> Mode -> IO File

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

271− modeStr : Mode -> String

272 modeStr Read = "r"

271 modeStr Read = "r"

273 modeStr Write = "w"

272 modeStr Write = "w"

274 modeStr ReadWrite = "r+"

273 modeStr ReadWrite = "r+"

lib/Prelude/Strings.idr+1−1

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

36unpack : String -> List Char

37unpack s with (strM s)

38 unpack "" | StrNil = []

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

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

40

41pack : List Char -> String

42pack [] = ""

src/Idris/AbsSyntax.hs+33

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

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

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

916

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+

917mkPApp fc a f [] = f

950mkPApp fc a f [] = f

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

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

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

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

548 [t] -> t

549 _ -> []

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

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

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

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

src/Idris/ElabTerm.hs+16−12

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

198 trySeq' deferr (x : xs)

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

200 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

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

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

202− = do ctxt <- get_context

206+ = do ctxt <- get_context

203− let iscon = isConName Nothing n ctxt

207+ env <- get_env

204− let defined = case lookupTy Nothing n ctxt of

208+ let defined = case lookupTy Nothing n ctxt of

205− [] -> False

209+ [] -> False

206− _ -> True

210+ _ -> True

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

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

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

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

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

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

210− else if (defined && not guarded)

214+ else if (defined && not guarded)

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

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

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

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

213− (patvar n)

217+ (patvar n)

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

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

215 [] -> False

219 [] -> False

216 _ -> True

220 _ -> True

src/Idris/Prover.hs+2

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

20import Control.Monad.State

21

22import Util.Pretty

23+import Debug.Trace

23

24

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

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

25prover lit x =

26prover lit x =

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

159 return (False, e, True, prf)

160 return (False, e, True, prf)

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

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

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

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

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

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

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

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

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

164 return (False, e, False, prf))

166 return (False, e, False, prf))

test/reg005/reg005.idr+2−2

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

20rle (x :: xs) with (rle xs)

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

22 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

24 = RChar (S n) x rs

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

26 = RChar O x (RChar n y rs)

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

28compress : Vect Char n -> String

29compress xs with (rle xs)

30 compress Nil | REnd = ""

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

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

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

33 show ni ++ show x ++ compress xs

34

test/reg010/expectednew file+4

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

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

2+

3+Specifically:

4+ Can't unify x with y

test/reg010/reg010.idrnew file+5

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

1+module usubst

2+

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