13a36a3 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

@@ -10,6 +10,9 @@ New in 0.9.18:

10 '%extern' directive, allowing back ends to define their own special

11 purpose primitives

12 + Ptr and ManagedPtr have been removed and replaced with external primitives

13+* Add %hint function annotation, which allows functions to be used as

14+ hints in proof search for 'auto' arguments. Only functions which return

15+ an instance of a data or record type are allowed as hints.

13* Syntax rules no longer perform variable capture. Users of effects will

16* Syntax rules no longer perform variable capture. Users of effects will

14 need to explicitly name results in dependent effect signatures instead

17 need to explicitly name results in dependent effect signatures instead

15 of using the default name "result".

18 of using the default name "result".

idris.cabal+3

@@ -531,6 +531,9 @@ Extra-source-files:

531 test/proof009/*.idr

532 test/proof009/expected

533 test/proof009/input

534+ test/proof010/run

535+ test/proof010/*.idr

536+ test/proof010/expected

534

537

535 test/quasiquote001/run

538 test/quasiquote001/run

536 test/quasiquote001/*.idr

539 test/quasiquote001/*.idr

src/Idris/AbsSyntax.hs+17

@@ -385,6 +385,23 @@ addClass n i

385 _ -> i

386 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

387

388+addAutoHint :: Name -> Name -> Idris ()

389+addAutoHint n hint =

390+ do ist <- getIState

391+ case lookupCtxtExact n (idris_autohints ist) of

392+ Nothing ->

393+ do let hs = addDef n [hint] (idris_autohints ist)

394+ putIState $ ist { idris_autohints = hs }

395+ Just nhints ->

396+ do let hs = addDef n (hint : nhints) (idris_autohints ist)

397+ putIState $ ist { idris_autohints = hs }

398+

399+getAutoHints :: Name -> Idris [Name]

400+getAutoHints n = do ist <- getIState

401+ case lookupCtxtExact n (idris_autohints ist) of

402+ Nothing -> return []

403+ Just ns -> return ns

404+

388addIBC :: IBCWrite -> Idris ()

405addIBC :: IBCWrite -> Idris ()

389addIBC ibc@(IBCDef n)

406addIBC ibc@(IBCDef n)

390 = do i <- getIState

407 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+4

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

179 idris_tyinfodata :: Ctxt TIData,

180 idris_fninfo :: Ctxt FnInfo,

181 idris_transforms :: Ctxt [(Term, Term)],

182+ idris_autohints :: Ctxt [Name],

182 idris_totcheck :: [(FC, Name)], -- names to check totality on

183 idris_totcheck :: [(FC, Name)], -- names to check totality on

183 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

184 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

184 idris_totcheckfail :: [(FC, String)],

185 idris_totcheckfail :: [(FC, String)],

@@ -307,6 +308,7 @@ data IBCWrite = IBCFix FixDecl

307 | IBCModDocs Name -- ^ The name is the special name used to track module docs

308 | IBCModDocs Name -- ^ The name is the special name used to track module docs

308 | IBCUsage (Name, Int)

309 | IBCUsage (Name, Int)

309 | IBCExport Name

310 | IBCExport Name

311+ | IBCAutoHint Name Name

310 deriving Show

312 deriving Show

311

313

312-- | The initial state for the compiler

314-- | The initial state for the compiler

@@ -316,6 +318,7 @@ idrisInit = IState initContext S.empty []

316 emptyContext emptyContext emptyContext emptyContext

318 emptyContext emptyContext emptyContext emptyContext

317 emptyContext emptyContext emptyContext emptyContext

319 emptyContext emptyContext emptyContext emptyContext

318 emptyContext emptyContext emptyContext emptyContext

320 emptyContext emptyContext emptyContext emptyContext

321+ emptyContext

319 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

322 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

320 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

323 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

321 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

324 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty

@@ -560,6 +563,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

560 | Reflection -- a reflecting function, compile-time only

563 | Reflection -- a reflecting function, compile-time only

561 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

564 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names

562 | Constructor -- Data constructor type

565 | Constructor -- Data constructor type

566+ | AutoHint -- use in auto implicit search

563 deriving (Show, Eq)

567 deriving (Show, Eq)

564{-!

568{-!

565deriving instance Binary FnOpt

569deriving instance Binary FnOpt

src/Idris/Core/Unify.hs+2

@@ -707,9 +707,11 @@ recoverable (App f a) (App f' a')

707recoverable f (Bind _ (Pi _ _ _) sc)

708 | (P (DCon _ _ _) _ _, _) <- unApply f = False

709 | (P (TCon _ _) _ _, _) <- unApply f = False

710+ | (Constant _) <- f = False

710recoverable (Bind _ (Pi _ _ _) sc) f

711recoverable (Bind _ (Pi _ _ _) sc) f

711 | (P (DCon _ _ _) _ _, _) <- unApply f = False

712 | (P (DCon _ _ _) _ _, _) <- unApply f = False

712 | (P (TCon _ _) _ _, _) <- unApply f = False

713 | (P (TCon _ _) _ _, _) <- unApply f = False

714+ | (Constant _) <- f = False

713recoverable (Bind _ (Lam _) sc) f = recoverable sc f

715recoverable (Bind _ (Lam _) sc) f = recoverable sc f

714recoverable f (Bind _ (Lam _) sc) = recoverable f sc

716recoverable f (Bind _ (Lam _) sc) = recoverable f sc

715recoverable x y = True

717recoverable x y = True

src/Idris/DeepSeq.hs+1

@@ -119,6 +119,7 @@ instance NFData FnOpt where

119 rnf Reflection = ()

120 rnf (Specialise x1) = rnf x1 `seq` ()

121 rnf Constructor = ()

122+ rnf AutoHint = ()

122

123

123instance NFData DataOpt where

124instance NFData DataOpt where

124 rnf Codata = ()

125 rnf Codata = ()

src/Idris/Elab/Type.hs+8−3

@@ -146,8 +146,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

146 addInternalApp (fc_fname fc) (fst . fc_start $ fc) ty' -- (mergeTy ty' (delab i nty')) -- TODO: Should use span instead of line and filename?

147 addIBC (IBCLineApp (fc_fname fc) (fst . fc_start $ fc) ty') -- (mergeTy ty' (delab i nty')))

148

149− let (t, _) = unApply (getRetTy nty')

149+ let (fam, _) = unApply (getRetTy nty')

150− let corec = case t of

150+ let corec = case fam of

151 P _ rcty _ -> case lookupCtxt rcty (idris_datatypes i) of

152 [TI _ True _ _ _] -> True

153 _ -> False

@@ -157,7 +157,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

157 let usety = if norm then nty' else nty

158 ds <- checkDef fc iderr [(n, (-1, Nothing, usety))]

159 addIBC (IBCDef n)

160− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

160+ let ds' = map (\(n, (i, top, fam)) -> (n, (i, top, fam, True))) ds

161 addDeferred ds'

162 setFlags n opts'

163 checkDocs fc argDocs ty

@@ -171,6 +171,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

171 addIBC (IBCOpt n)

172 when (Implicit `elem` opts') $ do addCoercion n

173 addIBC (IBCCoercion n)

174+ when (AutoHint `elem` opts') $

175+ case fam of

176+ P _ tyn _ -> do addAutoHint tyn n

177+ addIBC (IBCAutoHint tyn n)

178+ t -> ifail $ "Hints must return a data or record type"

174

179

175 -- If the function is declared as an error handler and the language

180 -- If the function is declared as an error handler and the language

176 -- extension is enabled, then add it to the list of error handlers.

181 -- extension is enabled, then add it to the list of error handlers.

src/Idris/IBC.hs+15−5

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 103

40+ibcVersion = 104

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

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

82 ibc_externs :: ![(Name, Int)],

83 ibc_parsedSpan :: !(Maybe FC),

84 ibc_usage :: ![(Name, Int)],

85− ibc_exports :: ![Name]

85+ ibc_exports :: ![Name],

86+ ibc_autohints :: ![(Name, Name)]

86 }

87 }

87 deriving Show

88 deriving Show

88{-!

89{-!

@@ -90,7 +91,7 @@ deriving instance Binary IBCFile

90!-}

91!-}

91

92

92initIBC :: IBCFile

93initIBC :: IBCFile

93−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] []

94+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

94

95

95loadIBC :: Bool -- ^ True = reexport, False = make everything private

96loadIBC :: Bool -- ^ True = reexport, False = make everything private

96 -> FilePath -> Idris ()

97 -> FilePath -> Idris ()

@@ -237,6 +238,7 @@ ibc i (IBCModDocs n) f = case lookupCtxtExact n (idris_moduledocs i) of

237 _ -> ifail "IBC write failed"

238 _ -> ifail "IBC write failed"

238ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

239ibc i (IBCUsage n) f = return f { ibc_usage = n : ibc_usage f }

239ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

240ibc i (IBCExport n) f = return f { ibc_exports = n : ibc_exports f }

241+ibc i (IBCAutoHint n h) f = return f { ibc_autohints = (n, h) : ibc_autohints f }

240

242

241process :: Bool -- ^ Reexporting

243process :: Bool -- ^ Reexporting

242 -> IBCFile -> FilePath -> Idris ()

244 -> IBCFile -> FilePath -> Idris ()

@@ -296,6 +298,7 @@ process reexp i fn

296 pParsedSpan $ force (ibc_parsedSpan i)

298 pParsedSpan $ force (ibc_parsedSpan i)

297 pUsage $ force (ibc_usage i)

299 pUsage $ force (ibc_usage i)

298 pExports $ force (ibc_exports i)

300 pExports $ force (ibc_exports i)

301+ pAutoHints $ force (ibc_autohints i)

299

302

300timestampOlder :: FilePath -> FilePath -> Idris ()

303timestampOlder :: FilePath -> FilePath -> Idris ()

301timestampOlder src ibc = do srct <- runIO $ getModificationTime src

304timestampOlder src ibc = do srct <- runIO $ getModificationTime src

@@ -326,6 +329,9 @@ pExports :: [Name] -> Idris ()

326pExports ns = do ist <- getIState

329pExports ns = do ist <- getIState

327 putIState ist { idris_exports = ns ++ idris_exports ist }

330 putIState ist { idris_exports = ns ++ idris_exports ist }

328

331

332+pAutoHints :: [(Name, Name)] -> Idris ()

333+pAutoHints ns = mapM_ (\(n,h) -> addAutoHint n h) ns

334+

329pImportDirs :: [FilePath] -> Idris ()

335pImportDirs :: [FilePath] -> Idris ()

330pImportDirs fs = mapM_ addImportDir fs

336pImportDirs fs = mapM_ addImportDir fs

331

337

@@ -942,7 +948,7 @@ instance Binary MetaInformation where

942 _ -> error "Corrupted binary data for MetaInformation"

948 _ -> error "Corrupted binary data for MetaInformation"

943

949

944instance Binary IBCFile where

950instance Binary IBCFile where

945− 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 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44)

951+ 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 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45)

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

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

947 do put x1

953 do put x1

948 put x2

954 put x2

@@ -988,6 +994,7 @@ instance Binary IBCFile where

988 put x42

994 put x42

989 put x43

995 put x43

990 put x44

996 put x44

997+ put x45

991

998

992 get

999 get

993 = do x1 <- get

1000 = do x1 <- get

@@ -1035,7 +1042,8 @@ instance Binary IBCFile where

1035 x42 <- get

1042 x42 <- get

1036 x43 <- get

1043 x43 <- get

1037 x44 <- get

1044 x44 <- get

1045+ x45 <- get

1038− 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 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44)

1046+ 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 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45)

1039 else return (initIBC { ver = x1 })

1047 else return (initIBC { ver = x1 })

1040

1048

1041instance Binary DataOpt where

1049instance Binary DataOpt where

@@ -1072,6 +1080,7 @@ instance Binary FnOpt where

1072 Constructor -> putWord8 13

1080 Constructor -> putWord8 13

1073 CExport x1 -> do putWord8 14

1081 CExport x1 -> do putWord8 14

1074 put x1

1082 put x1

1083+ AutoHint -> putWord8 15

1075 get

1084 get

1076 = do i <- getWord8

1085 = do i <- getWord8

1077 case i of

1086 case i of

@@ -1092,6 +1101,7 @@ instance Binary FnOpt where

1092 13 -> return Constructor

1101 13 -> return Constructor

1093 14 -> do x1 <- get

1102 14 -> do x1 <- get

1094 return $ CExport x1

1103 return $ CExport x1

1104+ 15 -> return AutoHint

1095 _ -> error "Corrupted binary data for FnOpt"

1105 _ -> error "Corrupted binary data for FnOpt"

1096

1106

1097instance Binary Fixity where

1107instance Binary Fixity where

src/Idris/Parser.hs+2

@@ -479,6 +479,8 @@ fnOpts opts

479 fnOpts (ErrorReverse : opts)

480 <|> do try (lchar '%' *> reserved "reflection");

481 fnOpts (Reflection : opts)

482+ <|> do try (lchar '%' *> reserved "hint");

483+ fnOpts (AutoHint : opts)

482 <|> do lchar '%'; reserved "specialise";

484 <|> do lchar '%'; reserved "specialise";

483 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

485 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'

484 fnOpts (Specialise ns : opts)

486 fnOpts (Specialise ns : opts)

src/Idris/ProofSearch.hs+38−24

@@ -91,7 +91,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

91 if ambigok || argsok then

92 case lookupCtxt nroot (idris_tyinfodata ist) of

93 [TISolution ts] -> findInferredTy ts

94− _ -> psRec rec maxDepth

94+ _ -> psRec rec maxDepth []

95 else autoArg (sUN "auto") -- not enough info in the type yet

96 where

97 findInferredTy (t : _) = elab (delab ist (toUN t))

@@ -129,12 +129,17 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

129 toUN (App f a) = App (toUN f) (toUN a)

130 toUN t = t

131

132+ -- psRec counts depth and the local variable applications we're under

133+ -- (so we don't try a pointless application of something to itself,

134+ -- which obviously won't work anyway but might lead us on a wild

135+ -- goose chase...)

132− psRec _ 0 | fromProver = cantSolveGoal

136+ psRec _ 0 locs | fromProver = cantSolveGoal

133− psRec rec 0 = do attack; defer [] nroot; solve --fail "Maximum depth reached"

137+ psRec rec 0 locs = do attack; defer [] nroot; solve --fail "Maximum depth reached"

134− psRec False d = tryCons d hints

138+ psRec False d locs = tryCons d locs hints

139+ psRec True d locs

135− psRec True d = do compute

140+ = do compute

136 try' (trivial elab ist)

141 try' (trivial elab ist)

137− (try' (try' (resolveByCon (d - 1)) (resolveByLocals (d - 1))

142+ (try' (try' (resolveByCon (d - 1) locs) (resolveByLocals (d - 1) locs)

138 True)

143 True)

139 -- if all else fails, make a new metavariable

144 -- if all else fails, make a new metavariable

140 (if fromProver

145 (if fromProver

@@ -145,37 +150,46 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

145 getFn d (Just f) | d < maxDepth-1 = [f]

150 getFn d (Just f) | d < maxDepth-1 = [f]

146 | otherwise = []

151 | otherwise = []

147

152

148− resolveByCon d

153+ resolveByCon d locs

149 = do t <- goal

154 = do t <- goal

150 let (f, _) = unApply t

155 let (f, _) = unApply t

151 case f of

156 case f of

157+ P _ n _ ->

158+ do let autohints = case lookupCtxtExact n (idris_autohints ist) of

159+ Nothing -> []

160+ Just hs -> hs

152− P _ n _ -> case lookupCtxt n (idris_datatypes ist) of

161+ case lookupCtxt n (idris_datatypes ist) of

153− [t] -> tryCons d (hints ++ con_names t ++

162+ [t] -> tryCons d locs (hints ++

163+ con_names t ++

164+ autohints ++

154− getFn d fn)

165+ getFn d fn)

155− _ -> fail "Not a data type"

166+ _ -> fail "Not a data type"

156 _ -> fail "Not a data type"

167 _ -> fail "Not a data type"

157

168

158 -- if there are local variables which have a function type, try

169 -- if there are local variables which have a function type, try

159 -- applying them too

170 -- applying them too

160− resolveByLocals d

171+ resolveByLocals d locs

161 = do env <- get_env

172 = do env <- get_env

162− tryLocals d env

173+ tryLocals d locs env

163

174

164− tryLocals d [] = fail "Locals failed"

175+ tryLocals d locs [] = fail "Locals failed"

176+ tryLocals d locs ((x, t) : xs)

177+ | x `elem` locs = tryLocals d locs xs

165− tryLocals d ((x, t) : xs) = try' (tryLocal d x t) (tryLocals d xs) True

178+ | otherwise = try' (tryLocal d (x : locs) x t) (tryLocals d locs xs) True

166

179

167− tryCons d [] = fail "Constructors failed"

180+ tryCons d locs [] = fail "Constructors failed"

168− tryCons d (c : cs) = try' (tryCon d c) (tryCons d cs) True

181+ tryCons d locs (c : cs) = try' (tryCon d locs c) (tryCons d locs cs) True

169

182

183+ tryLocal d locs n t

170− tryLocal d n t = do let a = getPArity (delab ist (binderTy t))

184+ = do let a = getPArity (delab ist (binderTy t))

171− tryLocalArg d n a

185+ tryLocalArg d locs n a

172

186

173− tryLocalArg d n 0 = elab (PRef (fileFC "prf") n)

187+ tryLocalArg d locs n 0 = elab (PRef (fileFC "prf") n)

174− tryLocalArg d n i = simple_app False (tryLocalArg d n (i - 1))

188+ tryLocalArg d locs n i = simple_app False (tryLocalArg d locs n (i - 1))

175− (psRec True d) "proof search local apply"

189+ (psRec True d locs) "proof search local apply"

176

190

177 -- Like type class resolution, but searching with constructors

191 -- Like type class resolution, but searching with constructors

178− tryCon d n =

192+ tryCon d locs n =

179 do ty <- goal

193 do ty <- goal

180 let imps = case lookupCtxtName n (idris_implicits ist) of

194 let imps = case lookupCtxtName n (idris_implicits ist) of

181 [] -> []

195 [] -> []

@@ -190,7 +204,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

190 when (length ps < length ps') $ fail "Can't apply constructor"

204 when (length ps < length ps') $ fail "Can't apply constructor"

191 mapM_ (\ (_, h) -> do focus h

205 mapM_ (\ (_, h) -> do focus h

192 aty <- goal

206 aty <- goal

193− psRec True d)

207+ psRec True d locs)

194 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

208 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

195 solve

209 solve

196

210

test/proof010/expectednew file+6

@@ -0,0 +1,6 @@

1+2, << function >>

2+3, << function >>

3+

4+some bools

5+some bools

6+

test/proof010/proof010.idrnew file+39

@@ -0,0 +1,39 @@

1+data MyShow : Type -> Type where

2+ ShowInstance : (show : a -> String) -> MyShow a

3+

4+myshow : {auto inst : MyShow a} -> a -> String

5+myshow {inst = ShowInstance show} x1 = show x1

6+

7+%hint

8+showNat : MyShow Nat

9+showNat = ShowInstance show

10+

11+%hint

12+showFn : MyShow (a -> b)

13+showFn = ShowInstance (\x => "<< function >>")

14+

15+%hint

16+showBools : MyShow (Bool, Bool)

17+showBools = ShowInstance (\x => "some bools")

18+

19+%hint

20+showStuff : MyShow a -> MyShow b -> MyShow (a, b)

21+showStuff sa sb = ShowInstance showPair

22+ where

23+ showPair : (a, b) -> String

24+ showPair (x, y) = myshow x ++ ", " ++ myshow y

25+

26+testShow : List (Bool, Bool) -> String

27+testShow [] = ""

28+testShow (x :: xs) = myshow x ++ "\n" ++ testShow xs

29+

30+testShow2 : List (Nat, Int -> Int) -> String

31+testShow2 [] = ""

32+testShow2 (x :: xs) = myshow x ++ "\n" ++ testShow2 xs

33+

34+main : IO ()

35+main = do putStrLn $ testShow2 [(2, (+1)), (3, abs)]

36+ putStrLn $ testShow [(True, False), (False, True)]

37+

38+

39+

test/proof010/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ proof010.idr -o proof010

3+./proof010

4+rm -f proof010 *.ibc