5692e48 · Idris-dev · git.iko.soy

CHANGELOG+3

@@ -3,6 +3,9 @@ New in 0.9.5:

33

44User visible changes:

55

6+* Added codata

7+ - as data declarations, but constructor arguments are evaluated lazily

8+ - functions which return a codata type do not reduce at compile time

69* Added 'parameters' blocks

710* Allow local data definitions in where blocks

811* Added '%default' directive to declare total-by-default or partial-by-default

Makefile+1−1

@@ -19,7 +19,7 @@ relib: .PHONY

1919 make -C lib IDRIS=../dist/build/idris/idris

2020

2121linecount : .PHONY

22− wc -l src/Idris/*.hs src/Core/*.hs src/IRTS/*.hs

22+ wc -l src/Idris/*.hs src/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

2323

2424.PHONY:

2525

src/Core/CoreParser.hs+1−1

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

2020 opLetter = iOpLetter,

2121 identLetter = identLetter haskellDef <|> lchar '.',

2222 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

23− reservedNames = ["let", "in", "data", "record", "Set",

23+ reservedNames = ["let", "in", "data", "codata", "record", "Set",

2424 "do", "dsl", "import", "impossible",

2525 "case", "of", "total", "partial",

2626 "infix", "infixl", "infixr",

src/Core/Evaluate.hs+4−1

@@ -691,12 +691,15 @@ addCasedef :: Name -> Bool -> Bool -> Bool ->

691691 Type -> Context -> Context

692692addCasedef n alwaysInline tcase covering ps psrt ty uctxt

693693 = let ctxt = definitions uctxt

694+ access = case lookupDefAcc Nothing n False uctxt of

695+ [(_, acc)] -> acc

696+ _ -> Public

694697 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,

695698 simpleCase tcase covering RunTime (FC "" 0) psrt) of

696699 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

697700 let inl = alwaysInline || small sc' in

698701 addDef n (CaseOp inl ty ps args sc args' sc',

699− Public, Unchecked) ctxt in

702+ access, Unchecked) ctxt in

700703 uctxt { definitions = ctxt' }

701704

702705addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

src/Idris/AbsSyntax.hs+2−2

@@ -505,7 +505,7 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)

505505 updateps yn nm (((a, t), i):as)

506506 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

507507 | otherwise = (MN i (show n ++ "_u"), t) : updateps yn nm as

508−expandParamsD ist dec ps ns (PData syn fc pd) = PData syn fc (expandPData pd)

508+expandParamsD ist dec ps ns (PData syn fc co pd) = PData syn fc co (expandPData pd)

509509 where

510510 -- just do the type decl, leave constructors alone (parameters will be

511511 -- added implicitly)

@@ -869,7 +869,7 @@ dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

869869dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

870870dumpDecl (PTy _ _ _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

871871dumpDecl (PClauses _ _ n cs) = "pat " ++ show n ++ "\t" ++ showSep "\n\t" (map (showCImp True) cs)

872−dumpDecl (PData _ _ d) = showDImp True d

872+dumpDecl (PData _ _ _ d) = showDImp True d

873873dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

874874dumpDecl (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ dumpDecls ps ++ "}\n"

875875dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

src/Idris/AbsSyntaxTree.hs+6−35

@@ -265,7 +265,8 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

265265 | PTy SyntaxInfo FC FnOpts Name t -- type declaration

266266 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

267267 | PCAF FC Name t -- top level constant

268− | PData SyntaxInfo FC (PData' t) -- data declaration

268+ | PData SyntaxInfo FC Bool -- codata

269+ (PData' t) -- data declaration

269270 | PParams FC [(Name, t)] [PDecl' t] -- params block

270271 | PNamespace String [PDecl' t] -- new namespace

271272 | PRecord SyntaxInfo FC Name t Name t -- record declaration

@@ -318,7 +319,7 @@ declared :: PDecl -> [Name]

318319declared (PFix _ _ _) = []

319320declared (PTy _ _ _ n t) = [n]

320321declared (PClauses _ _ n _) = [] -- not a declaration

321−declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

322+declared (PData _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

322323 where fstt (a, _, _) = a

323324declared (PParams _ _ ds) = concatMap declared ds

324325declared (PNamespace _ ds) = concatMap declared ds

@@ -328,7 +329,7 @@ defined :: PDecl -> [Name]

328329defined (PFix _ _ _) = []

329330defined (PTy _ _ _ n t) = []

330331defined (PClauses _ _ n _) = [n] -- not a declaration

331−defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts

332+defined (PData _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

332333 where fstt (a, _, _) = a

333334defined (PParams _ _ ds) = concatMap defined ds

334335defined (PNamespace _ ds) = concatMap defined ds

@@ -519,7 +520,7 @@ deriving instance Binary OptInfo

519520!-}

520521

521522

522−data TypeInfo = TI { con_names :: [Name] }

523+data TypeInfo = TI { con_names :: [Name], codata :: Bool }

523524 deriving Show

524525{-!

525526deriving instance Binary TypeInfo

@@ -619,7 +620,7 @@ instance Show PData where

619620showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

620621showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty

621622showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

622−showDeclImp _ (PData _ _ d) = show d

623+showDeclImp _ (PData _ _ _ d) = show d

623624showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++

624625 showSep "\n" (map show ps)

625626

@@ -930,36 +931,6 @@ showImp impl tm = se 10 tm where

930931 bracket outer inner str | inner > outer = "(" ++ str ++ ")"

931932 | otherwise = str

932933

933−{-

934− PQuote Raw

935− | PRef FC Name

936− | PLam Name PTerm PTerm

937− | PPi Plicity Name PTerm PTerm

938− | PLet Name PTerm PTerm PTerm

939− | PTyped PTerm PTerm -- term with explicit type

940− | PApp FC PTerm [PArg]

941− | PCase FC PTerm [(PTerm, PTerm)]

942− | PTrue FC

943− | PFalse FC

944− | PRefl FC

945− | PResolveTC FC

946− | PEq FC PTerm PTerm

947− | PPair FC PTerm PTerm

948− | PDPair FC PTerm PTerm PTerm

949− | PAlternative [PTerm]

950− | PHidden PTerm -- irrelevant or hidden pattern

951− | PSet

952− | PConstant Const

953− | Placeholder

954− | PDoBlock [PDo]

955− | PIdiom FC PTerm

956− | PReturn FC

957− | PMetavar Name

958− | PProof [PTactic]

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

960− | PElabError Err -- error to report on elaboration

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

962−-}

963934

964935instance Sized PTerm where

965936 size (PQuote rawTerm) = size rawTerm

src/Idris/Coverage.hs+3−3

@@ -105,8 +105,8 @@ expandAlts i all@(ConCase n _ _ _ : alts) def

105105 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef Nothing n (tt_ctxt i)

106106 = do let tyn = getTy n (tt_ctxt i)

107107 case lookupCtxt Nothing tyn (idris_datatypes i) of

108− (TI ns : _) -> do let ps = map mkPat ns

109− return $ addAlts ps (altsFor all) all

108+ (TI ns _ : _) -> do let ps = map mkPat ns

109+ return $ addAlts ps (altsFor all) all

110110 _ -> return all

111111 where

112112 altsFor [] = []

@@ -218,7 +218,7 @@ genAll i args = case filter (/=Placeholder) $ concatMap otherPats (nub args) of

218218 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)

219219 let tyn = getTy n (tt_ctxt i)

220220 case lookupCtxt Nothing tyn (idris_datatypes i) of

221− (TI ns : _) -> p : map (mkPat fc) (ns \\ [n])

221+ (TI ns _ : _) -> p : map (mkPat fc) (ns \\ [n])

222222 _ -> [p]

223223 ops fc n arg o = return Placeholder

224224

src/Idris/ElabDecls.hs+25−12

@@ -58,14 +58,24 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

5858 addStatics n cty ty'

5959 logLvl 2 $ "---> " ++ show cty

6060 let nty = cty -- normalise ctxt [] cty

61+ -- if the return type is something coinductive, freeze the definition

62+ let nty' = normalise ctxt [] nty

6163 ds <- checkDef fc [(n, nty)]

6264 addIBC (IBCDef n)

6365 addDeferred ds

6466 setFlags n opts

6567 addIBC (IBCFlags n opts)

68+ let (t, _) = unApply (getRetTy nty')

69+ case t of

70+ P _ rcty _ -> case lookupCtxt Nothing rcty (idris_datatypes i) of

71+ [TI _ True] -> do setAccessibility n Frozen

72+ addIBC (IBCAccess n Frozen)

73+ iputStrLn $ "Co " ++ show n

74+ _ -> return ()

75+ _ -> return ()

6676

67−elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

68−elabData info syn fc (PDatadecl n t_in dcons)

77+elabData :: ElabInfo -> SyntaxInfo -> FC -> Bool -> PData -> Idris ()

78+elabData info syn fc codata (PDatadecl n t_in dcons)

6979 = do iLOG (show fc)

7080 checkUndefined fc n

7181 ctxt <- getContext

@@ -80,11 +90,11 @@ elabData info syn fc (PDatadecl n t_in dcons)

8090 (cty, _) <- recheckC fc [] t'

8191 logLvl 2 $ "---> " ++ show cty

8292 updateContext (addTyDecl n cty) -- temporary, to check cons

83− cons <- mapM (elabCon info syn n) dcons

93+ cons <- mapM (elabCon info syn n codata) dcons

8494 ttag <- getName

8595 i <- get

86− put (i { idris_datatypes = addDef n (TI (map fst cons))

87− (idris_datatypes i) })

96+ put (i { idris_datatypes = addDef n (TI (map fst cons) codata)

97+ (idris_datatypes i) })

8898 addIBC (IBCDef n)

8999 addIBC (IBCData n)

90100 collapseCons n cons

@@ -94,7 +104,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

94104elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

95105 PTerm -> Name -> PTerm -> Idris ()

96106elabRecord info syn fc tyn ty cn cty

97− = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])

107+ = do elabData info syn fc False (PDatadecl tyn ty [(cn, cty, fc)])

98108 cty' <- implicit syn cn cty

99109 i <- get

100110 cty <- case lookupTy Nothing cn (tt_ctxt i) of

@@ -200,12 +210,12 @@ elabRecord info syn fc tyn ty cn cty

200210 (map pexp rhsArgs)) []

201211 return (pn, pfnTy, PClauses fc [] setname [pclause])

202212

203−elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)

204−elabCon info syn tn (n, t_in, fc)

213+elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> (Name, PTerm, FC) -> Idris (Name, Type)

214+elabCon info syn tn codata (n, t_in, fc)

205215 = do checkUndefined fc n

206216 ctxt <- getContext

207217 i <- get

208− t_in <- implicit syn n t_in

218+ t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

209219 let t = addImpl i t_in

210220 logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

211221 ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) []

@@ -229,6 +239,9 @@ elabCon info syn tn (n, t_in, fc)

229239 else return ()

230240 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

231241

242+ mkLazy (PPi pl n ty sc) = PPi (pl { plazy = True }) n ty (mkLazy sc)

243+ mkLazy t = t

244+

232245elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

233246elabClauses info fc opts n_in cs = let n = liftname info n_in in

234247 do ctxt <- getContext

@@ -605,7 +618,7 @@ elabClass info syn fc constraints tn ps ds

605618 let cons = [(cn, cty, fc)]

606619 let ddecl = PDatadecl tn tty cons

607620 logLvl 5 $ "Class data " ++ showDImp True ddecl

608− elabData info (syn { no_imp = no_imp syn ++ mnames }) fc ddecl

621+ elabData info (syn { no_imp = no_imp syn ++ mnames }) fc False ddecl

609622 -- for each constraint, build a top level function to chase it

610623 logLvl 5 $ "Building functions"

611624 let usyn = syn { using = ps ++ using syn }

@@ -899,8 +912,8 @@ elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

899912elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

900913elabDecl' info (PTy s f o n ty) = do iLOG $ "Elaborating type decl " ++ show n ++ show o

901914 elabType info s f o n ty

902−elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d)

903− elabData info s f d

915+elabDecl' info (PData s f co d) = do iLOG $ "Elaborating " ++ show (d_name d)

916+ elabData info s f co d

904917elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n

905918 i <- get -- get the type options too

906919 let o' = case lookupCtxt Nothing n (idris_flags i) of

src/Idris/IBC.hs+11−7

@@ -849,10 +849,11 @@ instance (Binary t) => Binary (PDecl' t) where

849849 put x2

850850 put x3

851851 put x4

852− PData x1 x2 x3 -> do putWord8 3

853− put x1

854− put x2

855− put x3

852+ PData x1 x2 x3 x4 -> do putWord8 3

853+ put x1

854+ put x2

855+ put x3

856+ put x4

856857 PParams x1 x2 x3 -> do putWord8 4

857858 put x1

858859 put x2

@@ -911,7 +912,8 @@ instance (Binary t) => Binary (PDecl' t) where

911912 3 -> do x1 <- get

912913 x2 <- get

913914 x3 <- get

914− return (PData x1 x2 x3)

915+ x4 <- get

916+ return (PData x1 x2 x3 x4)

915917 4 -> do x1 <- get

916918 x2 <- get

917919 x3 <- get

@@ -1389,9 +1391,11 @@ instance Binary OptInfo where

13891391 return (Optimise x1 x2 x3)

13901392

13911393instance Binary TypeInfo where

1392− put (TI x1) = put x1

1394+ put (TI x1 x2) = do put x1

1395+ put x2

13931396 get = do x1 <- get

1394− return (TI x1)

1397+ x2 <- get

1398+ return (TI x1 x2)

13951399

13961400instance Binary SynContext where

13971401 put x

src/Idris/Parser.hs+7−4

@@ -1089,9 +1089,12 @@ pRecord syn = do acc <- pAccessibility

10891089 toFreeze (Just Frozen) = Just Hidden

10901090 toFreeze x = x

10911091

1092+pDataI = do reserved "data"; return False

1093+ <|> do reserved "codata"; return True

1094+

10921095pData :: SyntaxInfo -> IParser PDecl

10931096pData syn = try (do acc <- pAccessibility

1094− reserved "data"

1097+ co <- pDataI

10951098 fc <- pfc

10961099 tyn_in <- pfName

10971100 ty <- pTSig (impOK syn)

@@ -1106,10 +1109,10 @@ pData syn = try (do acc <- pAccessibility

11061109 popIndent

11071110 closeBlock

11081111 accData acc tyn (map (\ (n, _, _) -> n) cons)

1109− return $ PData syn fc (PDatadecl tyn ty cons))

1112+ return $ PData syn fc co (PDatadecl tyn ty cons))

11101113 <|> try (do pushIndent

11111114 acc <- pAccessibility

1112− reserved "data"

1115+ co <- pDataI

11131116 fc <- pfc

11141117 tyn_in <- pfName

11151118 args <- many pName

@@ -1123,7 +1126,7 @@ pData syn = try (do acc <- pAccessibility

11231126 do let cty = bindArgs cargs conty

11241127 return (x, cty, cfc)) cons

11251128 accData acc tyn (map (\ (n, _, _) -> n) cons')

1126− return $ PData syn fc (PDatadecl tyn ty cons'))

1129+ return $ PData syn fc co (PDatadecl tyn ty cons'))

11271130 where

11281131 mkPApp fc t [] = t

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

src/Idris/Primitives.hs+1−1

@@ -281,7 +281,7 @@ elabPrim (Prim n ty i def sc tot)

281281

282282elabPrims :: Idris ()

283283elabPrims = do mapM_ (elabDecl toplevel)

284− (map (PData defaultSyntax (FC "builtin" 0))

284+ (map (PData defaultSyntax (FC "builtin" 0) False)

285285 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

286286 mapM_ elabPrim primitives

287287