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

git.iko.soy/Idris-dev

Annotate functions as %hint for auto search

This allows extra hints, as well as constructors, to guide proof search for auto implicit arguments. Added test proof010 which shows how this works to simulate type classes with overlapping instances (and consequently no injectivity restriction or assumption) %hint only works on functions which return an instance of a data type. Proof search exhaustively searches hints and constructors, so use with care especially when adding lots of recursive or overlapping hints.

commit13a36a3d32d1fe5f5479565b6c1c03e93340b0a9 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 29 Mar 2015, 21:24 (12 years ago) parent7befb29

13 files changed+142−32

compare with master

unifiedsplit

CHANGELOG+3 idris.cabal+3 src/Idris/AbsSyntax.hs+17 src/Idris/AbsSyntaxTree.hs+4 src/Idris/Core/Unify.hs+2 src/Idris/DeepSeq.hs+1 src/Idris/Elab/Type.hs+8−3 src/Idris/IBC.hs+15−5 src/Idris/Parser.hs+2 src/Idris/ProofSearch.hs+38−24 test/proof010/expected+6 test/proof010/proof010.idr+39 test/proof010/run+4

CHANGELOG+3

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

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

1111 purpose primitives

1212 + 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.

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

1417 need to explicitly name results in dependent effect signatures instead

1518 of using the default name "result".

idris.cabal+3

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

531531 test/proof009/*.idr

532532 test/proof009/expected

533533 test/proof009/input

534+ test/proof010/run

535+ test/proof010/*.idr

536+ test/proof010/expected

534537

535538 test/quasiquote001/run

536539 test/quasiquote001/*.idr

src/Idris/AbsSyntax.hs+17

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

385385 _ -> i

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

387387

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+

388405addIBC :: IBCWrite -> Idris ()

389406addIBC ibc@(IBCDef n)

390407 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+4

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

179179 idris_tyinfodata :: Ctxt TIData,

180180 idris_fninfo :: Ctxt FnInfo,

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

182+ idris_autohints :: Ctxt [Name],

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

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

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

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

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

308309 | IBCUsage (Name, Int)

309310 | IBCExport Name

311+ | IBCAutoHint Name Name

310312 deriving Show

311313

312314-- | The initial state for the compiler

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

316318 emptyContext emptyContext emptyContext emptyContext

317319 emptyContext emptyContext emptyContext emptyContext

318320 emptyContext emptyContext emptyContext emptyContext

321+ emptyContext

319322 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []

320323 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []

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

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

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

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

562565 | Constructor -- Data constructor type

566+ | AutoHint -- use in auto implicit search

563567 deriving (Show, Eq)

564568{-!

565569deriving instance Binary FnOpt

src/Idris/Core/Unify.hs+2

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

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

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

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

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

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

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

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

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

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

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

715717recoverable x y = True

src/Idris/DeepSeq.hs+1

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

119119 rnf Reflection = ()

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

121121 rnf Constructor = ()

122+ rnf AutoHint = ()

122123

123124instance NFData DataOpt where

124125 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

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

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

148148

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

150− let corec = case t of

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

150+ let corec = case fam of

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

152152 [TI _ True _ _ _] -> True

153153 _ -> False

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

157157 let usety = if norm then nty' else nty

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

159159 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

161161 addDeferred ds'

162162 setFlags n opts'

163163 checkDocs fc argDocs ty

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

171171 addIBC (IBCOpt n)

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

173173 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"

174179

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

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

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 103

40+ibcVersion = 104

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

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

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

8383 ibc_parsedSpan :: !(Maybe FC),

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

85− ibc_exports :: ![Name]

85+ ibc_exports :: ![Name],

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

8687 }

8788 deriving Show

8889{-!

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

9091!-}

9192

9293initIBC :: IBCFile

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

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

9495

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

9697 -> FilePath -> Idris ()

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

237238 _ -> ifail "IBC write failed"

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

239240ibc 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 }

240242

241243process :: Bool -- ^ Reexporting

242244 -> IBCFile -> FilePath -> Idris ()

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

296298 pParsedSpan $ force (ibc_parsedSpan i)

297299 pUsage $ force (ibc_usage i)

298300 pExports $ force (ibc_exports i)

301+ pAutoHints $ force (ibc_autohints i)

299302

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

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

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

326329pExports ns = do ist <- getIState

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

328331

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

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

334+

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

330336pImportDirs fs = mapM_ addImportDir fs

331337

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

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

943949

944950instance 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)

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

947953 do put x1

948954 put x2

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

988994 put x42

989995 put x43

990996 put x44

997+ put x45

991998

992999 get

9931000 = do x1 <- get

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

10351042 x42 <- get

10361043 x43 <- get

10371044 x44 <- 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)

1045+ x45 <- get

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)

10391047 else return (initIBC { ver = x1 })

10401048

10411049instance Binary DataOpt where

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

10721080 Constructor -> putWord8 13

10731081 CExport x1 -> do putWord8 14

10741082 put x1

1083+ AutoHint -> putWord8 15

10751084 get

10761085 = do i <- getWord8

10771086 case i of

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

10921101 13 -> return Constructor

10931102 14 -> do x1 <- get

10941103 return $ CExport x1

1104+ 15 -> return AutoHint

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

10961106

10971107instance Binary Fixity where

src/Idris/Parser.hs+2

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

479479 fnOpts (ErrorReverse : opts)

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

481481 fnOpts (Reflection : opts)

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

483+ fnOpts (AutoHint : opts)

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

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

484486 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

9191 if ambigok || argsok then

9292 case lookupCtxt nroot (idris_tyinfodata ist) of

9393 [TISolution ts] -> findInferredTy ts

94− _ -> psRec rec maxDepth

94+ _ -> psRec rec maxDepth []

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

9696 where

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

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

129129 toUN (App f a) = App (toUN f) (toUN a)

130130 toUN t = t

131131

132− psRec _ 0 | fromProver = cantSolveGoal

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

134− psRec False d = tryCons d hints

135− psRec True d = do compute

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

136+ psRec _ 0 locs | fromProver = cantSolveGoal

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

138+ psRec False d locs = tryCons d locs hints

139+ psRec True d locs

140+ = do compute

136141 try' (trivial elab ist)

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

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

138143 True)

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

140145 (if fromProver

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

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

146151 | otherwise = []

147152

148− resolveByCon d

153+ resolveByCon d locs

149154 = do t <- goal

150155 let (f, _) = unApply t

151156 case f of

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

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

154− getFn d fn)

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

157+ P _ n _ ->

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

159+ Nothing -> []

160+ Just hs -> hs

161+ case lookupCtxt n (idris_datatypes ist) of

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

163+ con_names t ++

164+ autohints ++

165+ getFn d fn)

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

156167 _ -> fail "Not a data type"

157168

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

159170 -- applying them too

160− resolveByLocals d

171+ resolveByLocals d locs

161172 = do env <- get_env

162− tryLocals d env

173+ tryLocals d locs env

163174

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

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

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

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

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

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

166179

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

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

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

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

169182

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

171− tryLocalArg d n a

183+ tryLocal d locs n t

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

185+ tryLocalArg d locs n a

172186

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

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

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

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

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

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

176190

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

178− tryCon d n =

192+ tryCon d locs n =

179193 do ty <- goal

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

181195 [] -> []

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

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

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

192206 aty <- goal

193− psRec True d)

207+ psRec True d locs)

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

195209 solve

196210

test/proof010/expectednew file+6

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

1+2, << function >>

2+3, << function >>

4+some bools

5+some bools

test/proof010/proof010.idrnew file+39

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

1+data MyShow : Type -> Type where

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

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

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

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