022d4df · Idris-dev · git.iko.soy

CHANGELOG+1

@@ -3,6 +3,7 @@ New in 0.9.7:

33

44User visible changes:

55

6+* 'implicit' keyword, for implicit type conversion

67* Primitives for 8,16,32 and 64 bit integers

78

89Internal changes:

src/Core/CoreParser.hs+1−1

@@ -34,7 +34,7 @@ idrisDef = haskellDef {

3434 "infix", "infixl", "infixr",

3535 "where", "with", "syntax", "proof", "postulate",

3636 "using", "namespace", "class", "instance",

37− "public", "private", "abstract",

37+ "public", "private", "abstract", "implicit",

3838 "Int", "Integer", "Float", "Char", "String", "Ptr",

3939 "Bits8", "Bits16", "Bits32", "Bits64"]

4040 }

src/Core/Elaborate.hs+15−2

@@ -40,6 +40,16 @@ type Elab a = Elab' () a

4040proof :: ElabState aux -> ProofState

4141proof (ES (p, _) _ _) = p

4242

43+-- Insert a 'proofSearchFail' error if necessary to shortcut any further

44+-- fruitless searching

45+proofFail :: Elab' aux a -> Elab' aux a

46+proofFail e = do s <- get

47+ case runStateT e s of

48+ OK (a, s') -> trace ("OK ACTUALLY") $

49+ do put s'

50+ return a

51+ Error err -> trace "BAD" $ lift $ Error (ProofSearchFail err)

52+

4353saveState :: Elab' aux ()

4454saveState = do e@(ES p s _) <- get

4555 put (ES p s (Just e))

@@ -508,14 +518,17 @@ try' t1 t2 proofSearch

508518 case prunStateT ps t1 s of

509519 OK (v, s') -> do put s'

510520 return v

511− Error e1 -> if proofSearch || recoverableErr e1 then

521+ Error e1 -> if recoverableErr e1 then

512522 do case runStateT t2 s of

513523 OK (v, s') -> do put s'; return v

514524 Error e2 -> if score e1 >= score e2

515525 then lift (tfail e1)

516526 else lift (tfail e2)

517527 else lift (tfail e1)

518− where recoverableErr (CantUnify r _ _ _ _ _) = r

528+ where recoverableErr err@(CantUnify r _ _ _ _ _)

529+ = -- traceWhen r (show err) $

530+ r || proofSearch

531+ recoverableErr (ProofSearchFail _) = trace "FAILED" $ False

519532 recoverableErr _ = True

520533

521534tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

src/Core/TT.hs+2

@@ -61,6 +61,7 @@ data Err = Msg String

6161 | Inaccessible Name

6262 | NonCollapsiblePostulate Name

6363 | AlreadyDefined Name

64+ | ProofSearchFail Err

6465 | At FC Err

6566 deriving Eq

6667

@@ -85,6 +86,7 @@ score :: Err -> Int

8586score (CantUnify _ _ _ m _ s) = s + score m

8687score (CantResolve _) = 20

8788score (NoSuchVariable _) = 1000

89+score (ProofSearchFail _) = 10000

8890score _ = 0

8991

9092instance Show Err where

src/Idris/AbsSyntax.hs+19

@@ -68,11 +68,30 @@ getTotality n

6868 [t] -> return t

6969 _ -> return (Total [])

7070

71+-- Get coercions which might return the required type

72+getCoercionsTo :: IState -> Type -> [Name]

73+getCoercionsTo i ty =

74+ let cs = idris_coercions i

75+ (fn,_) = unApply (getRetTy ty) in

76+ findCoercions fn cs

77+ where findCoercions t [] = []

78+ findCoercions t (n : ns) =

79+ let ps = case lookupTy Nothing n (tt_ctxt i) of

80+ [ty] -> case unApply (getRetTy ty) of

81+ (t', _) ->

82+ if t == t' then [n] else []

83+ _ -> [] in

84+ ps ++ findCoercions t ns

85+

7186addToCG :: Name -> CGInfo -> Idris ()

7287addToCG n cg

7388 = do i <- getIState

7489 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

7590

91+addCoercion :: Name -> Idris ()

92+addCoercion n = do i <- getIState

93+ putIState $ i { idris_coercions = n : idris_coercions i }

94+

7695addDocStr :: Name -> String -> Idris ()

7796addDocStr n doc

7897 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+6−1

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

6666 idris_options :: IOption,

6767 idris_name :: Int,

6868 idris_metavars :: [Name],

69+ idris_coercions :: [Name],

6970 syntax_rules :: [Syntax],

7071 syntax_keywords :: [String],

7172 imported :: [FilePath],

@@ -125,13 +126,14 @@ data IBCWrite = IBCFix FixDecl

125126 | IBCFlags Name [FnOpt]

126127 | IBCCG Name

127128 | IBCDoc Name

129+ | IBCCoercion Name

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

129131 deriving Show

130132

131133idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

132134 emptyContext emptyContext emptyContext emptyContext

133135 emptyContext emptyContext emptyContext emptyContext

134− [] "" defaultOpts 6 [] [] [] [] [] [] [] []

136+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

135137 [] Nothing Nothing [] [] [] Hidden False [] Nothing

136138

137139-- The monad for the main REPL - reading and processing files and updating

@@ -281,6 +283,7 @@ tacimpl t = TacImp False Dynamic t ""

281283

282284data FnOpt = Inlinable | TotalFn | PartialFn

283285 | Coinductive | AssertTotal | TCGen

286+ | Implicit -- implicit coercion

284287 | CExport String -- export, with a C name

285288 | Specialise [Name] -- specialise it, freeze these names

286289 deriving (Show, Eq)

@@ -443,6 +446,7 @@ data PTerm = PQuote Raw

443446 | PTactics [PTactic] -- as PProof, but no auto solving

444447 | PElabError Err -- error to report on elaboration

445448 | PImpossible -- special case for declaring when an LHS can't typecheck

449+ | PCoerced PTerm -- to mark a coerced argument, so as not to coerce twice

446450 deriving Eq

447451{-!

448452deriving instance Binary PTerm

@@ -984,6 +988,7 @@ showImp impl tm = se 10 tm where

984988 se p Placeholder = "_"

985989 se p (PDoBlock _) = "do block show not implemented"

986990 se p (PElabError s) = show s

991+ se p (PCoerced t) = se p t

987992-- se p x = "Not implemented"

988993

989994 sArg (PImp _ _ n tm _) = siArg (n, tm)

src/Idris/Delaborate.hs+1

@@ -108,6 +108,7 @@ pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

108108pshow i (NonCollapsiblePostulate n)

109109 = "The return type of postulate " ++ show n ++ " is not collapsible"

110110pshow i (AlreadyDefined n) = show n ++ " is already defined"

111+pshow i (ProofSearchFail e) = pshow i e

111112pshow i (At f e) = show f ++ ":" ++ pshow i e

112113

113114showSc i [] = ""

src/Idris/ElabDecls.hs+6−4

@@ -78,6 +78,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

7878 addDocStr n doc

7979 addIBC (IBCDoc n)

8080 addIBC (IBCFlags n opts')

81+ when (Implicit `elem` opts) $ do addCoercion n

82+ addIBC (IBCCoercion n)

8183 when corec $ do setAccessibility n Frozen

8284 addIBC (IBCAccess n Frozen)

8385

@@ -1281,10 +1283,10 @@ checkInferred fc inf user =

12811283 logLvl 10 $ "Checking match"

12821284 i <- getIState

12831285 tclift $ case matchClause' True i user inf of

1284− Right vs -> return ()

1285− Left (x, y) -> tfail $ At fc

1286− (Msg $ "The type-checked term and given term do not match: "

1287− ++ show x ++ " and " ++ show y)

1286+ _ -> return ()

1287+-- Left (x, y) -> tfail $ At fc

1288+-- (Msg $ "The type-checked term and given term do not match: "

1289+-- ++ show x ++ " and " ++ show y)

12881290 logLvl 10 $ "Checked match"

12891291-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

12901292

src/Idris/ElabTerm.hs+32−12

@@ -120,7 +120,9 @@ elab ist info pattern tcgen fn tm

120120 elabE ina t = {- do g <- goal

121121 tm <- get_term

122122 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

123− $ -} elab' ina t

123+ $ -}

124+ do t' <- insertCoerce ina t

125+ elab' ina t'

124126

125127 local f = do e <- get_env

126128 return (f `elem` map fst e)

@@ -191,9 +193,10 @@ elab ist info pattern tcgen fn tm

191193 = trySeq as

192194 where -- if none work, take the error from the first

193195 trySeq (x : xs) = let e1 = elab' ina x in

194− try e1 (trySeq' e1 xs)

195− trySeq' deferr [] = deferr

196− trySeq' deferr (x : xs) = try (elab' ina x) (trySeq' deferr xs)

196+ try' e1 (trySeq' e1 xs) True

197+ trySeq' deferr [] = proofFail deferr

198+ trySeq' deferr (x : xs)

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

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

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

199202 = do ctxt <- get_context

@@ -348,7 +351,7 @@ elab ist info pattern tcgen fn tm

348351 compare (priority x) (priority y))

349352 (zip ns args)

350353 elabArgs (ina || not isinf, guarded)

351− [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

354+ [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

352355 mkSpecialised ist fc f (map getTm args') tm

353356 solve

354357 ptm <- get_term

@@ -442,14 +445,29 @@ elab ist info pattern tcgen fn tm

442445 shadowed new (PRef _ n) | n `elem` new = Placeholder

443446 shadowed new t = t

444447

445− elabArgs ina failed retry [] _

448+ insertCoerce ina t =

449+ do ty <- goal

450+ -- Check for possible coercions to get to the goal

451+ -- and add them as 'alternatives'

452+ let cs = getCoercionsTo ist ty

453+ let t' = case (t, cs) of

454+ (PCoerced tm, _) -> tm

455+ (_, []) -> t

456+ (_, cs) -> PAlternative False

457+ (t : map (mkCoerce t) cs)

458+ return t'

459+ where

460+ mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!

461+ addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

462+

463+ elabArgs ina failed fc retry [] _

446464-- | retry = let (ns, ts) = unzip (reverse failed) in

447465-- elabArgs ina [] False ns ts

448466 | otherwise = return ()

449− elabArgs ina failed r (n:ns) ((_, Placeholder) : args)

450− = elabArgs ina failed r ns args

451− elabArgs ina failed r (n:ns) ((lazy, t) : args)

452− | lazy && not pattern

467+ elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args)

468+ = elabArgs ina failed fc r ns args

469+ elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

470+ | lazy && not pattern

453471 = do elabArg n (PApp bi (PRef bi (UN "lazy"))

454472 [pimp (UN "a") Placeholder,

455473 pexp t]);

@@ -457,15 +475,17 @@ elab ist info pattern tcgen fn tm

457475 where elabArg n t

458476 = do hs <- get_holes

459477 tm <- get_term

478+ t' <- insertCoerce ina t

460479 failed' <- -- trace (show (n, t, hs, tm)) $

480+ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

461481 case n `elem` hs of

462482 True ->

463483-- if r

464484-- then try (do focus n; elabE ina t; return failed)

465485-- (return ((n,(lazy, t)):failed))

466− do focus n; elabE ina t; return failed

486+ do focus n; elabE ina t'; return failed

467487 False -> return failed

468− elabArgs ina failed r ns args

488+ elabArgs ina failed fc r ns args

469489

470490-- For every alternative, look at the function at the head. Automatically resolve

471491-- any nested alternatives where that function is also at the head

src/Idris/IBC.hs+15−5

@@ -21,7 +21,7 @@ import System.Directory

2121import Paths_idris

2222

2323ibcVersion :: Word8

24−ibcVersion = 26

24+ibcVersion = 27

2525

2626data IBCFile = IBCFile { ver :: Word8,

2727 sourcefile :: FilePath,

@@ -44,14 +44,15 @@ data IBCFile = IBCFile { ver :: Word8,

4444 ibc_flags :: [(Name, [FnOpt])],

4545 ibc_cg :: [(Name, CGInfo)],

4646 ibc_defs :: [(Name, Def)],

47− ibc_docstrings :: [(Name, String)]

47+ ibc_docstrings :: [(Name, String)],

48+ ibc_coercions :: [Name]

4849 }

4950{-!

5051deriving instance Binary IBCFile

5152!-}

5253

5354initIBC :: IBCFile

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

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

5556

5657loadIBC :: FilePath -> Idris ()

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

@@ -119,6 +120,7 @@ ibc i (IBCDoc n) f = case lookupCtxt Nothing n (idris_docstrings i) of

119120ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of

120121 [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

121122 _ -> fail "IBC write failed"

123+ibc i (IBCCoercion n) f = return f { ibc_coercions = n : ibc_coercions f }

122124ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

123125ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

124126ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

@@ -151,6 +153,7 @@ process i fn

151153 pTotal (ibc_total i)

152154 pCG (ibc_cg i)

153155 pDocs (ibc_docstrings i)

156+ pCoercions (ibc_coercions i)

154157

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

156159timestampOlder src ibc = do srct <- getModificationTime src

@@ -270,6 +273,9 @@ pTotal ds = mapM_ (\ (n, a) ->

270273pCG :: [(Name, CGInfo)] -> Idris ()

271274pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

272275

276+pCoercions :: [Name] -> Idris ()

277+pCoercions ns = mapM_ (\ n -> addCoercion n) ns

278+

273279----- Generated by 'derive'

274280

275281instance Binary SizeChange where

@@ -738,7 +744,7 @@ instance Binary Totality where

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

739745

740746instance Binary IBCFile where

741− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22)

747+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23)

742748 = do put x1

743749 put x2

744750 put x3

@@ -761,6 +767,7 @@ instance Binary IBCFile where

761767 put x20

762768 put x21

763769 put x22

770+ put x23

764771 get

765772 = do x1 <- get

766773 if x1 == ibcVersion then

@@ -785,7 +792,8 @@ instance Binary IBCFile where

785792 x20 <- get

786793 x21 <- get

787794 x22 <- get

788− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22)

795+ x23 <- get

796+ 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)

789797 else return (initIBC { ver = x1 })

790798

791799instance Binary FnOpt where

@@ -799,6 +807,7 @@ instance Binary FnOpt where

799807 put x

800808 Coinductive -> putWord8 5

801809 PartialFn -> putWord8 6

810+ Implicit -> putWord8 7

802811 get

803812 = do i <- getWord8

804813 case i of

@@ -810,6 +819,7 @@ instance Binary FnOpt where

810819 return (Specialise x)

811820 5 -> return Coinductive

812821 6 -> return PartialFn

822+ 7 -> return Implicit

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

814824

815825instance Binary Fixity where

src/Idris/Parser.hs+1

@@ -706,6 +706,7 @@ pFnOpts opts

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

707707 lchar '['; ns <- sepBy pfName (lchar ','); lchar ']'

708708 pFnOpts (Specialise ns : opts)

709+ <|> do reserved "implicit"; pFnOpts (Implicit : opts)

709710 <|> return opts

710711

711712addAcc :: Name -> Maybe Accessibility -> IParser ()