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

CHANGELOG+1

compare with master

unifiedsplit

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

3

4User visible changes:

5

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

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

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

7

8

8Internal changes:

9Internal changes:

src/Core/CoreParser.hs+1−1

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

34 "infix", "infixl", "infixr",

35 "where", "with", "syntax", "proof", "postulate",

36 "using", "namespace", "class", "instance",

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

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

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

39 "Bits8", "Bits16", "Bits32", "Bits64"]

40 }

src/Core/Elaborate.hs+15−2

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

40proof :: ElabState aux -> ProofState

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

42

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+

43saveState :: Elab' aux ()

53saveState :: Elab' aux ()

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

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

45 put (ES p s (Just e))

55 put (ES p s (Just e))

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

508 case prunStateT ps t1 s of

518 case prunStateT ps t1 s of

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

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

510 return v

520 return v

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

521+ Error e1 -> if recoverableErr e1 then

512 do case runStateT t2 s of

522 do case runStateT t2 s of

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

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

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

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

515 then lift (tfail e1)

525 then lift (tfail e1)

516 else lift (tfail e2)

526 else lift (tfail e2)

517 else lift (tfail e1)

527 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

519 recoverableErr _ = True

532 recoverableErr _ = True

520

533

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

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

src/Core/TT.hs+2

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

61 | Inaccessible Name

62 | NonCollapsiblePostulate Name

63 | AlreadyDefined Name

64+ | ProofSearchFail Err

64 | At FC Err

65 | At FC Err

65 deriving Eq

66 deriving Eq

66

67

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

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

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

86score (CantResolve _) = 20

87score (CantResolve _) = 20

87score (NoSuchVariable _) = 1000

88score (NoSuchVariable _) = 1000

89+score (ProofSearchFail _) = 10000

88score _ = 0

90score _ = 0

89

91

90instance Show Err where

92instance Show Err where

src/Idris/AbsSyntax.hs+19

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

68 [t] -> return t

69 _ -> return (Total [])

70

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+

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

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

72addToCG n cg

87addToCG n cg

73 = do i <- getIState

88 = do i <- getIState

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

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

75

90

91+addCoercion :: Name -> Idris ()

92+addCoercion n = do i <- getIState

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

94+

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

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

77addDocStr n doc

96addDocStr n doc

78 = do i <- getIState

97 = do i <- getIState

src/Idris/AbsSyntaxTree.hs+6−1

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

66 idris_options :: IOption,

67 idris_name :: Int,

68 idris_metavars :: [Name],

69+ idris_coercions :: [Name],

69 syntax_rules :: [Syntax],

70 syntax_rules :: [Syntax],

70 syntax_keywords :: [String],

71 syntax_keywords :: [String],

71 imported :: [FilePath],

72 imported :: [FilePath],

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

125 | IBCFlags Name [FnOpt]

126 | IBCFlags Name [FnOpt]

126 | IBCCG Name

127 | IBCCG Name

127 | IBCDoc Name

128 | IBCDoc Name

129+ | IBCCoercion Name

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

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

129 deriving Show

131 deriving Show

130

132

131idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

133idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

132 emptyContext emptyContext emptyContext emptyContext

134 emptyContext emptyContext emptyContext emptyContext

133 emptyContext emptyContext emptyContext emptyContext

135 emptyContext emptyContext emptyContext emptyContext

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

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

135 [] Nothing Nothing [] [] [] Hidden False [] Nothing

137 [] Nothing Nothing [] [] [] Hidden False [] Nothing

136

138

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

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

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

281

283

282data FnOpt = Inlinable | TotalFn | PartialFn

284data FnOpt = Inlinable | TotalFn | PartialFn

283 | Coinductive | AssertTotal | TCGen

285 | Coinductive | AssertTotal | TCGen

286+ | Implicit -- implicit coercion

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

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

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

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

286 deriving (Show, Eq)

289 deriving (Show, Eq)

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

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

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

444 | PElabError Err -- error to report on elaboration

447 | PElabError Err -- error to report on elaboration

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

448 | 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

446 deriving Eq

450 deriving Eq

447{-!

451{-!

448deriving instance Binary PTerm

452deriving instance Binary PTerm

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

984 se p Placeholder = "_"

988 se p Placeholder = "_"

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

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

986 se p (PElabError s) = show s

990 se p (PElabError s) = show s

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

987-- se p x = "Not implemented"

992-- se p x = "Not implemented"

988

993

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

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

108pshow i (NonCollapsiblePostulate n)

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

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

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

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

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

112

113

113showSc i [] = ""

114showSc 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

78 addDocStr n doc

79 addIBC (IBCDoc n)

80 addIBC (IBCFlags n opts')

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

82+ addIBC (IBCCoercion n)

81 when corec $ do setAccessibility n Frozen

83 when corec $ do setAccessibility n Frozen

82 addIBC (IBCAccess n Frozen)

84 addIBC (IBCAccess n Frozen)

83

85

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

1281 logLvl 10 $ "Checking match"

1283 logLvl 10 $ "Checking match"

1282 i <- getIState

1284 i <- getIState

1283 tclift $ case matchClause' True i user inf of

1285 tclift $ case matchClause' True i user inf of

1284− Right vs -> return ()

1286+ _ -> return ()

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

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

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

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

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

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

1288 logLvl 10 $ "Checked match"

1290 logLvl 10 $ "Checked match"

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

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

1290

1292

src/Idris/ElabTerm.hs+32−12

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

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

121 tm <- get_term

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

123+ $ -}

124+ do t' <- insertCoerce ina t

123− $ -} elab' ina t

125+ elab' ina t'

124

126

125 local f = do e <- get_env

127 local f = do e <- get_env

126 return (f `elem` map fst e)

128 return (f `elem` map fst e)

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

191 = trySeq as

193 = trySeq as

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

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

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

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

194− try e1 (trySeq' e1 xs)

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

195− trySeq' deferr [] = deferr

197+ trySeq' deferr [] = proofFail deferr

198+ trySeq' deferr (x : xs)

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

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

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

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

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

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

199 = do ctxt <- get_context

202 = do ctxt <- get_context

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

348 compare (priority x) (priority y))

351 compare (priority x) (priority y))

349 (zip ns args)

352 (zip ns args)

350 elabArgs (ina || not isinf, guarded)

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

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

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

353 solve

356 solve

354 ptm <- get_term

357 ptm <- get_term

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

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

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

443 shadowed new t = t

446 shadowed new t = t

444

447

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+

445− elabArgs ina failed retry [] _

463+ elabArgs ina failed fc retry [] _

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

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

447-- elabArgs ina [] False ns ts

465-- elabArgs ina [] False ns ts

448 | otherwise = return ()

466 | otherwise = return ()

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

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

450− = elabArgs ina failed r ns args

468+ = elabArgs ina failed fc r ns args

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

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

452− | lazy && not pattern

470+ | lazy && not pattern

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

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

454 [pimp (UN "a") Placeholder,

472 [pimp (UN "a") Placeholder,

455 pexp t]);

473 pexp t]);

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

457 where elabArg n t

475 where elabArg n t

458 = do hs <- get_holes

476 = do hs <- get_holes

459 tm <- get_term

477 tm <- get_term

478+ t' <- insertCoerce ina t

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

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

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

461 case n `elem` hs of

481 case n `elem` hs of

462 True ->

482 True ->

463-- if r

483-- if r

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

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

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

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

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

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

467 False -> return failed

487 False -> return failed

468− elabArgs ina failed r ns args

488+ elabArgs ina failed fc r ns args

469

489

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

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

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

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

src/Idris/IBC.hs+15−5

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

21import Paths_idris

22

23ibcVersion :: Word8

24−ibcVersion = 26

24+ibcVersion = 27

25

26data IBCFile = IBCFile { ver :: Word8,

27 sourcefile :: FilePath,

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

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

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

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

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

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

48+ ibc_coercions :: [Name]

48 }

49 }

49{-!

50{-!

50deriving instance Binary IBCFile

51deriving instance Binary IBCFile

51!-}

52!-}

52

53

53initIBC :: IBCFile

54initIBC :: IBCFile

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

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

55

56

56loadIBC :: FilePath -> Idris ()

57loadIBC :: FilePath -> Idris ()

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

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

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

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

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

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

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

121 _ -> fail "IBC write failed"

122 _ -> fail "IBC write failed"

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

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

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

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

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

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

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

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

151 pTotal (ibc_total i)

153 pTotal (ibc_total i)

152 pCG (ibc_cg i)

154 pCG (ibc_cg i)

153 pDocs (ibc_docstrings i)

155 pDocs (ibc_docstrings i)

156+ pCoercions (ibc_coercions i)

154

157

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

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

156timestampOlder src ibc = do srct <- getModificationTime src

159timestampOlder src ibc = do srct <- getModificationTime src

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

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

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

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

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

272

275

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

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

278+

273----- Generated by 'derive'

279----- Generated by 'derive'

274

280

275instance Binary SizeChange where

281instance Binary SizeChange where

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

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

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

739

745

740instance Binary IBCFile where

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

742 = do put x1

748 = do put x1

743 put x2

749 put x2

744 put x3

750 put x3

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

761 put x20

767 put x20

762 put x21

768 put x21

763 put x22

769 put x22

770+ put x23

764 get

771 get

765 = do x1 <- get

772 = do x1 <- get

766 if x1 == ibcVersion then

773 if x1 == ibcVersion then

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

785 x20 <- get

792 x20 <- get

786 x21 <- get

793 x21 <- get

787 x22 <- get

794 x22 <- get

795+ x23 <- 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)

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)

789 else return (initIBC { ver = x1 })

797 else return (initIBC { ver = x1 })

790

798

791instance Binary FnOpt where

799instance Binary FnOpt where

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

799 put x

807 put x

800 Coinductive -> putWord8 5

808 Coinductive -> putWord8 5

801 PartialFn -> putWord8 6

809 PartialFn -> putWord8 6

810+ Implicit -> putWord8 7

802 get

811 get

803 = do i <- getWord8

812 = do i <- getWord8

804 case i of

813 case i of

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

810 return (Specialise x)

819 return (Specialise x)

811 5 -> return Coinductive

820 5 -> return Coinductive

812 6 -> return PartialFn

821 6 -> return PartialFn

822+ 7 -> return Implicit

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

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

814

824

815instance Binary Fixity where

825instance Binary Fixity where

src/Idris/Parser.hs+1

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

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

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

708 pFnOpts (Specialise ns : opts)

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

709 <|> return opts

710 <|> return opts

710

711

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

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