4a0eba1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add %name directive for naming hints in editing.

4a0eba1Edwin Brady13 years ago

libs/prelude/Prelude/List.idr+3

compare with master

unifiedsplit

@@ -19,6 +19,9 @@ infixl 8 ++

19 = Nil

20 | (::) a (List a)

22+-- Name hints for interactive editing

23+%name List xs, ys, zs, ws

24+

22--------------------------------------------------------------------------------

25--------------------------------------------------------------------------------

23-- Syntactic tests

26-- Syntactic tests

24--------------------------------------------------------------------------------

27--------------------------------------------------------------------------------

libs/prelude/Prelude/Nat.idr+3

@@ -14,6 +14,9 @@ import Prelude.Classes

14 = Z

15 | S Nat

17+-- name hints for interactive editing

18+%name Nat k,j,i,n,m

19+

17--------------------------------------------------------------------------------

20--------------------------------------------------------------------------------

18-- Syntactic tests

21-- Syntactic tests

19--------------------------------------------------------------------------------

22--------------------------------------------------------------------------------

libs/prelude/Prelude/Vect.idr+3

@@ -15,6 +15,9 @@ infixr 7 ::

15 Nil : Vect Z a

16 (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a

18+-- Hints for interactive editing

19+%name Vect xs,ys,zs,ws

20+

18--------------------------------------------------------------------------------

21--------------------------------------------------------------------------------

19-- Indexing into vectors

22-- Indexing into vectors

20--------------------------------------------------------------------------------

23--------------------------------------------------------------------------------

src/Core/TT.hs+5

@@ -834,6 +834,11 @@ getRetTy (Bind n (PVTy _) sc) = getRetTy sc

834getRetTy (Bind n (Pi _) sc) = getRetTy sc

835getRetTy sc = sc

836

837+uniqueNameFrom :: [Name] -> [Name] -> Name

838+uniqueNameFrom (s : supply) hs

839+ | s `elem` hs = uniqueNameFrom supply hs

840+ | otherwise = s

841+

837uniqueName :: Name -> [Name] -> Name

842uniqueName :: Name -> [Name] -> Name

838uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

843uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs

839 | otherwise = n

844 | otherwise = n

src/Idris/AbsSyntax.hs+19

@@ -167,6 +167,25 @@ addDocStr n doc

167 = do i <- getIState

168 putIState $ i { idris_docstrings = addDef n doc (idris_docstrings i) }

169

170+addNameHint :: Name -> Name -> Idris ()

171+addNameHint ty n

172+ = do i <- getIState

173+ ty' <- case lookupCtxtName ty (idris_implicits i) of

174+ [(tyn, _)] -> return tyn

175+ [] -> throwError (NoSuchVariable ty)

176+ tyns -> throwError (CantResolveAlts (map show (map fst tyns)))

177+ let ns' = case lookupCtxt ty' (idris_namehints i) of

178+ [ns] -> ns ++ [n]

179+ _ -> [n]

180+ putIState $ i { idris_namehints = addDef ty' ns' (idris_namehints i) }

181+

182+getNameHints :: IState -> Name -> [Name]

183+getNameHints i (UN "->") = [UN "f",UN "g"]

184+getNameHints i n =

185+ case lookupCtxt n (idris_namehints i) of

186+ [ns] -> ns

187+ _ -> []

188+

170addToCalledG :: Name -> [Name] -> Idris ()

189addToCalledG :: Name -> [Name] -> Idris ()

171addToCalledG n ns = return () -- TODO

190addToCalledG n ns = return () -- TODO

172

191

src/Idris/AbsSyntaxTree.hs+3

@@ -92,6 +92,7 @@ data IState = IState {

92 idris_dsls :: Ctxt DSL,

93 idris_optimisation :: Ctxt OptInfo,

94 idris_datatypes :: Ctxt TypeInfo,

95+ idris_namehints :: Ctxt [Name],

95 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported

96 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported

96 -- ^ list of lhs/rhs, and a list of missing clauses

97 -- ^ list of lhs/rhs, and a list of missing clauses

97 idris_flags :: Ctxt [FnOpt],

98 idris_flags :: Ctxt [FnOpt],

@@ -183,12 +184,14 @@ data IBCWrite = IBCFix FixDecl

183 | IBCDoc Name

184 | IBCDoc Name

184 | IBCCoercion Name

185 | IBCCoercion Name

185 | IBCDef Name -- i.e. main context

186 | IBCDef Name -- i.e. main context

187+ | IBCNameHint (Name, Name)

186 | IBCLineApp FilePath Int PTerm

188 | IBCLineApp FilePath Int PTerm

187 deriving Show

189 deriving Show

188

190

189idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

191idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

190 emptyContext emptyContext emptyContext emptyContext

192 emptyContext emptyContext emptyContext emptyContext

191 emptyContext emptyContext emptyContext emptyContext

193 emptyContext emptyContext emptyContext emptyContext

194+ emptyContext

192 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

195 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []

193 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

196 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

194 True defaultTheme stdout

197 True defaultTheme stdout

src/Idris/CaseSplit.hs+78−48

@@ -71,7 +71,7 @@ split n t'

71 logLvl 3 ("Split:\n" ++

72 (showSep "\n" (map show (mapMaybe id newPats))))

73 logLvl 3 "----"

74− let newPats' = mergeAllPats ctxt t (mapMaybe id newPats)

74+ let newPats' = mergeAllPats ist n t (mapMaybe id newPats)

75 iLOG ("Name updates " ++ showSep "\n"

76 (map (\ (p, u) -> show u ++ " " ++ show p) newPats'))

77 return (map snd newPats')

@@ -84,47 +84,55 @@ data MergeState = MS { namemap :: [(Name, Name)],

84addUpdate n tm = do ms <- get

85 put (ms { updates = ((n, stripNS tm) : updates ms) } )

87−inventName n =

87+inventName ist ty n =

88 do ms <- get

89+ let supp = case ty of

90+ Nothing -> []

91+ Just t -> getNameHints ist t

92+ let nsupp = case n of

93+ MN i ('_':_) -> mkSupply (supp ++ varlist)

94+ MN i n -> mkSupply (UN n : supp ++ varlist)

95+ x -> mkSupply (x : supp)

89 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++

96 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++

90 explicit ms

97 explicit ms

91 case lookup n (invented ms) of

98 case lookup n (invented ms) of

92 Just n' -> return n'

99 Just n' -> return n'

93 Nothing ->

100 Nothing ->

94− do let n' = case n of

101+ do let n' = uniqueNameFrom nsupp badnames

95− MN i ('_':_) ->

96− uniqueName (UN "var") badnames

97− MN i n -> uniqueName (UN n) badnames

98− x -> x

99 put (ms { invented = (n, n') : invented ms })

102 put (ms { invented = (n, n') : invented ms })

100 return n'

103 return n'

104+

105+mkSupply ns = mkSupply' ns (map nextName ns)

106+ where mkSupply' xs ns' = xs ++ mkSupply ns'

107+

108+varlist = map (UN . (:[])) "xyzwstuv" -- EB's personal preference :)

101

109

102stripNS tm = mapPT dens tm where

110stripNS tm = mapPT dens tm where

103 dens (PRef fc n) = PRef fc (nsroot n)

111 dens (PRef fc n) = PRef fc (nsroot n)

104 dens t = t

112 dens t = t

105

113

106−mergeAllPats :: Context -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]

114+mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]

107−mergeAllPats ctxt t [] = []

115+mergeAllPats ist cv t [] = []

108−mergeAllPats ctxt t (p : ps)

116+mergeAllPats ist cv t (p : ps)

109− = let (p', MS _ _ _ u) = runState (mergePat ctxt t p)

117+ = let (p', MS _ _ _ u) = runState (mergePat ist t p Nothing)

110− (MS [] [] (patvars t) [])

118+ (MS [] [] (filter (/=cv) (patvars t)) [])

111− ps' = mergeAllPats ctxt t ps in

119+ ps' = mergeAllPats ist cv t ps in

112 ((p, u) : ps')

120 ((p, u) : ps')

113 where patvars (PRef _ n) = [n]

121 where patvars (PRef _ n) = [n]

114 patvars (PApp _ _ as) = concatMap (patvars . getTm) as

122 patvars (PApp _ _ as) = concatMap (patvars . getTm) as

115 patvars (PPatvar _ n) = [n]

123 patvars (PPatvar _ n) = [n]

116 patvars _ = []

124 patvars _ = []

117

125

118−mergePat :: Context -> PTerm -> PTerm -> State MergeState PTerm

126+mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm

119-- If any names are unified, make sure they stay unified. Always prefer

127-- If any names are unified, make sure they stay unified. Always prefer

120-- user provided name (first pattern)

128-- user provided name (first pattern)

121−mergePat ctxt (PPatvar fc n) new

129+mergePat ist (PPatvar fc n) new t

122− = mergePat ctxt (PRef fc n) new

130+ = mergePat ist (PRef fc n) new t

123−mergePat ctxt old (PPatvar fc n)

131+mergePat ist old (PPatvar fc n) t

124− = mergePat ctxt old (PRef fc n)

132+ = mergePat ist old (PRef fc n) t

125−mergePat ctxt orig@(PRef fc n) new@(PRef _ n')

133+mergePat ist orig@(PRef fc n) new@(PRef _ n') t

126− | isDConName n' ctxt = do addUpdate n new;

134+ | isDConName n' (tt_ctxt ist) = do addUpdate n new

127− return new

135+ return new

128 | otherwise

136 | otherwise

129 = do ms <- get

137 = do ms <- get

130 case lookup n' (namemap ms) of

138 case lookup n' (namemap ms) of

@@ -132,37 +140,49 @@ mergePat ctxt orig@(PRef fc n) new@(PRef _ n')

132 return (PRef fc x)

140 return (PRef fc x)

133 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })

141 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })

134 return (PRef fc n)

142 return (PRef fc n)

135−mergePat ctxt (PApp _ _ args) (PApp fc f args')

143+mergePat ist (PApp _ _ args) (PApp fc f args') t

136− = do newArgs <- zipWithM mergeArg args args'

144+ = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))

137 return (PApp fc f newArgs)

145 return (PApp fc f newArgs)

146+ where mergeArg x (y, t)

138− where mergeArg x y = do tm' <- mergePat ctxt (getTm x) (getTm y)

147+ = do tm' <- mergePat ist (getTm x) (getTm y) t

139− case x of

148+ case x of

140− (PImp _ _ _ _ _ _) ->

149+ (PImp _ _ _ _ _ _) ->

141− return (y { machine_inf = machine_inf x,

150+ return (y { machine_inf = machine_inf x,

142− getTm = tm' })

151+ getTm = tm' })

143− _ -> return (y { getTm = tm' })

152+ _ -> return (y { getTm = tm' })

144−mergePat ctxt (PRef fc n) t = do tm <- tidy t

153+mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty

145− addUpdate n tm

154+ addUpdate n tm

146− return tm

155+ return tm

147−mergePat ctxt x y = return y

156+mergePat ist x y t = return y

148

157

149mergeUserImpl :: PTerm -> PTerm -> PTerm

158mergeUserImpl :: PTerm -> PTerm -> PTerm

150mergeUserImpl x y = x

159mergeUserImpl x y = x

151

160

161+argTys :: IState -> PTerm -> [Maybe Name]

162+argTys ist (PRef fc n)

163+ = case lookupTy n (tt_ctxt ist) of

164+ [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing

165+ _ -> repeat Nothing

166+ where tyName (Bind _ (Pi _) _) = Just (UN "->")

167+ tyName t | (P _ n _, _) <- unApply t = Just n

168+ | otherwise = Nothing

169+argTys _ _ = repeat Nothing

170+

171+tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm

152−tidy orig@(PRef fc n)

172+tidy ist orig@(PRef fc n) ty

153 = do ms <- get

173 = do ms <- get

154 case lookup n (namemap ms) of

174 case lookup n (namemap ms) of

155 Just x -> return (PRef fc x)

175 Just x -> return (PRef fc x)

156 Nothing -> case n of

176 Nothing -> case n of

157 (UN _) -> return orig

177 (UN _) -> return orig

158− _ -> do n' <- inventName n

178+ _ -> do n' <- inventName ist ty n

159 return (PRef fc n')

179 return (PRef fc n')

160−tidy (PApp fc f args)

180+tidy ist (PApp fc f args) ty

161− = do args' <- mapM tidyArg args

181+ = do args' <- zipWithM tidyArg args (argTys ist f)

162 return (PApp fc f args')

182 return (PApp fc f args')

163− where tidyArg x = do tm' <- tidy (getTm x)

183+ where tidyArg x ty' = do tm' <- tidy ist (getTm x) ty'

164− return (x { getTm = tm' })

184+ return (x { getTm = tm' })

165−tidy tm = return tm

185+tidy ist tm ty = return tm

166

186

167

187

168-- mapPT tidyVar tm

188-- mapPT tidyVar tm

@@ -291,15 +311,26 @@ getClause :: Int -- ^ line number that the type is declared on

291 -> FilePath -- ^ Source file name

311 -> FilePath -- ^ Source file name

292 -> Idris String

312 -> Idris String

293getClause l fn fp = do ty <- getInternalApp fp l

313getClause l fn fp = do ty <- getInternalApp fp l

314+ ist <- get

294− let ap = mkApp ty [1..]

315+ let ap = mkApp ist ty []

295 return (show fn ++ " " ++ ap ++

316 return (show fn ++ " " ++ ap ++

296 "= ?" ++ show fn ++ "_rhs")

317 "= ?" ++ show fn ++ "_rhs")

297− where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)

318+ where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used

319+ = let n = getNameFrom i used ty in

298− = "x" ++ show n ++ " " ++ mkApp sc ns

320+ show n ++ " " ++ mkApp i sc (n : used)

299− mkApp (PPi (Exp _ _ _ False) n _ sc) ns

321+ mkApp i (PPi (Exp _ _ _ False) n _ sc) used

300− = show n ++ " " ++ mkApp sc ns

322+ = show n ++ " " ++ mkApp i sc (n : used)

301− mkApp (PPi _ _ _ sc) ns = mkApp sc ns

323+ mkApp i (PPi _ _ _ sc) used = mkApp i sc used

302− mkApp _ _ = ""

324+ mkApp i _ _ = ""

325+

326+ getNameFrom i used (PPi _ _ _ _)

327+ = uniqueNameFrom (mkSupply [UN "f", UN "g"]) used

328+ getNameFrom i used (PApp fc f as) = getNameFrom i used f

329+ getNameFrom i used (PRef fc f)

330+ = case getNameHints i f of

331+ [] -> uniqueName (UN "x") used

332+ ns -> uniqueNameFrom (mkSupply ns) used

333+ getNameFrom i used _ = uniqueName (UN "x") used

303

334

304getProofClause :: Int -- ^ line number that the type is declared

335getProofClause :: Int -- ^ line number that the type is declared

305 -> Name -- ^ Function name

336 -> Name -- ^ Function name

@@ -326,4 +357,3 @@ mkWith str n = let str' = replaceRHS str "with (_)"

326 | not ('=' `elem` rest) = str

357 | not ('=' `elem` rest) = str

327 replaceRHS (x : rest) str = x : replaceRHS rest str

358 replaceRHS (x : rest) str = x : replaceRHS rest str

328

359

329−

src/Idris/IBC.hs+14−5

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 45

26+ibcVersion = 46

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -51,7 +51,8 @@ data IBCFile = IBCFile { ver :: Word8,

51 ibc_docstrings :: [(Name, String)],

52 ibc_transforms :: [(Term, Term)],

53 ibc_coercions :: [Name],

54− ibc_lineapps :: [(FilePath, Int, PTerm)]

54+ ibc_lineapps :: [(FilePath, Int, PTerm)],

55+ ibc_namehints :: [(Name, Name)]

55 }

56 }

56 deriving Show

57 deriving Show

57{-!

58{-!

@@ -59,7 +60,7 @@ deriving instance Binary IBCFile

59!-}

60!-}

61initIBC :: IBCFile

62initIBC :: IBCFile

62−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

63+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

64loadIBC :: FilePath -> Idris ()

65loadIBC :: FilePath -> Idris ()

65loadIBC fp = do iLOG $ "Loading ibc " ++ fp

66loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -137,6 +138,8 @@ ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

137ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

138ibc i (IBCTrans t) f = return f { ibc_transforms = t : ibc_transforms f }

138ibc i (IBCLineApp fp l t) f

139ibc i (IBCLineApp fp l t) f

139 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

140 = return f { ibc_lineapps = (fp,l,t) : ibc_lineapps f }

141+ibc i (IBCNameHint (n, ty)) f

142+ = return f { ibc_namehints = (n, ty) : ibc_namehints f }

140

143

141process :: IBCFile -> FilePath -> Idris ()

144process :: IBCFile -> FilePath -> Idris ()

142process i fn

145process i fn

@@ -172,6 +175,7 @@ process i fn

172 pCoercions (ibc_coercions i)

175 pCoercions (ibc_coercions i)

173 pTrans (ibc_transforms i)

176 pTrans (ibc_transforms i)

174 pLineApps (ibc_lineapps i)

177 pLineApps (ibc_lineapps i)

178+ pNameHints (ibc_namehints i)

175

179

176timestampOlder :: FilePath -> FilePath -> IO ()

180timestampOlder :: FilePath -> FilePath -> IO ()

177timestampOlder src ibc = do srct <- getModificationTime src

181timestampOlder src ibc = do srct <- getModificationTime src

@@ -319,6 +323,9 @@ pTrans ts = mapM_ addTrans ts

319pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

323pLineApps :: [(FilePath, Int, PTerm)] -> Idris ()

320pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

324pLineApps ls = mapM_ (\ (f, i, t) -> addInternalApp f i t) ls

321

325

326+pNameHints :: [(Name, Name)] -> Idris ()

327+pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

328+

322----- Generated by 'derive'

329----- Generated by 'derive'

323

330

324instance Binary SizeChange where

331instance Binary SizeChange where

@@ -873,7 +880,7 @@ instance Binary Totality where

873 _ -> error "Corrupted binary data for Totality"

880 _ -> error "Corrupted binary data for Totality"

874

881

875instance Binary IBCFile where

882instance Binary IBCFile where

876− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)

883+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)

877 = {-# SCC "putIBCFile" #-}

884 = {-# SCC "putIBCFile" #-}

878 do put x1

885 do put x1

879 put x2

886 put x2

@@ -902,6 +909,7 @@ instance Binary IBCFile where

902 put x25

909 put x25

903 put x26

910 put x26

904 put x27

911 put x27

912+ put x28

905 get

913 get

906 = do x1 <- get

914 = do x1 <- get

907 if x1 == ibcVersion then

915 if x1 == ibcVersion then

@@ -931,7 +939,8 @@ instance Binary IBCFile where

931 x25 <- get

939 x25 <- get

932 x26 <- get

940 x26 <- get

933 x27 <- get

941 x27 <- get

942+ x28 <- get

934− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)

943+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28)

935 else return (initIBC { ver = x1 })

944 else return (initIBC { ver = x1 })

936

945

937instance Binary DataOpt where

946instance Binary DataOpt where

src/Idris/ParseData.hs+1−1

@@ -144,7 +144,7 @@ data_ syn = do (doc, acc, dataOpts) <- try (do

144 mkPApp fc t [] = t

145 mkPApp fc t xs = PApp fc t (map pexp xs)

146 bindArgs :: [PTerm] -> PTerm -> PTerm

147− bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

147+ bindArgs xs t = foldr (PPi expl (MN 0 "_t")) t xs

148 combineDataOpts :: DataOpts -> DataOpts

149 combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts

150

src/Idris/Parser.hs+7

@@ -797,6 +797,7 @@ Directive' ::= 'lib' CodeGen String_t

797 | 'default' Totality

798 | 'logging' Natural

799 | 'dynamic' StringList

800+ | 'name' Name NameList

800 | 'language' 'TypeProviders'

801 | 'language' 'TypeProviders'

801 | 'language' 'ErrorReflection'

802 | 'language' 'ErrorReflection'

802 ;

803 ;

@@ -839,6 +840,12 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

839 Left lib -> addIBC (IBCDyLib (lib_name lib))

840 Left lib -> addIBC (IBCDyLib (lib_name lib))

840 Right msg ->

841 Right msg ->

841 fail $ msg)]

842 fail $ msg)]

843+ <|> do try (lchar '%' *> reserved "name")

844+ ty <- iName []

845+ ns <- sepBy1 name (lchar ',')

846+ return [PDirective

847+ (do mapM_ (addNameHint ty) ns

848+ mapM_ (\n -> addIBC (IBCNameHint (ty, n))) ns)]

842 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

849 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

843 return [PDirective (addLangExt ext)]

850 return [PDirective (addLangExt ext)]

844 <?> "directive"

851 <?> "directive"

test/test032/expected+3−3

@@ -1,8 +1,8 @@

1Type checking ./test032.idr

2isElem x [] = ?isElem_rhs_1

3−isElem x (t :: t1) = ?isElem_rhs_3

3+isElem x (y :: xs) = ?isElem_rhs_3

5− localZipWith f (_ :: _) (x :: xs1) = ?localZipWith_rhs_1

5+ localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1

7f x :: (map f xs)

8isElem2 x (y :: ys) with (_)

@@ -10,5 +10,5 @@ isElem2 x (y :: ys) with (_)

10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3

12 [] => ?bar_1

13− (t :: t1) => ?bar_2

13+ (x :: ys) => ?bar_2