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

git.iko.soy/Idris-dev

on master help sign in

Added "codata"

5692e48Edwin Brady14 years ago

CHANGELOG+3

compare with master

unifiedsplit

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

4User visible changes:

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

6* Added 'parameters' blocks

9* Added 'parameters' blocks

7* Allow local data definitions in where blocks

10* Allow local data definitions in where blocks

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

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

Makefile+1−1

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

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

21linecount : .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

24.PHONY:

src/Core/CoreParser.hs+1−1

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

20 opLetter = iOpLetter,

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

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

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

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

24 "do", "dsl", "import", "impossible",

25 "case", "of", "total", "partial",

26 "infix", "infixl", "infixr",

src/Core/Evaluate.hs+4−1

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

691 Type -> Context -> Context

692addCasedef n alwaysInline tcase covering ps psrt ty uctxt

693 = let ctxt = definitions uctxt

694+ access = case lookupDefAcc Nothing n False uctxt of

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

696+ _ -> Public

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

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

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

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

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

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

697 let inl = alwaysInline || small sc' in

700 let inl = alwaysInline || small sc' in

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

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

699− Public, Unchecked) ctxt in

702+ access, Unchecked) ctxt in

700 uctxt { definitions = ctxt' }

703 uctxt { definitions = ctxt' }

701

704

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

705addOperator :: 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)

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

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

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

509 where

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

511 -- added implicitly)

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

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

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

871dumpDecl (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

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

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

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

src/Idris/AbsSyntaxTree.hs+6−35

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

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

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

267 | PCAF FC Name t -- top level constant

268+ | PData SyntaxInfo FC Bool -- codata

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

269+ (PData' t) -- data declaration

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

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

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

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

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

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

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

318declared (PFix _ _ _) = []

319declared (PFix _ _ _) = []

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

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

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

321declared (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

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

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

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

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

324declared (PNamespace _ ds) = concatMap declared ds

325declared (PNamespace _ ds) = concatMap declared ds

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

328defined (PFix _ _ _) = []

329defined (PFix _ _ _) = []

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

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

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

331defined (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

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

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

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

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

334defined (PNamespace _ ds) = concatMap defined ds

335defined (PNamespace _ ds) = concatMap defined ds

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

519!-}

520!-}

520

521

522

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

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

523 deriving Show

524 deriving Show

524{-!

525{-!

525deriving instance Binary TypeInfo

526deriving instance Binary TypeInfo

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

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

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

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

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

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

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

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

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

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

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

624 showSep "\n" (map show ps)

625 showSep "\n" (map show ps)

625

626

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

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

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

931 | otherwise = str

932 | otherwise = str

932

933

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−-}

963

934

964instance Sized PTerm where

935instance Sized PTerm where

965 size (PQuote rawTerm) = size rawTerm

936 size (PQuote rawTerm) = size rawTerm

src/Idris/Coverage.hs+3−3

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

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

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

107 case lookupCtxt Nothing tyn (idris_datatypes i) of

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

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

109− return $ addAlts ps (altsFor all) all

109+ return $ addAlts ps (altsFor all) all

110 _ -> return all

111 where

112 altsFor [] = []

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

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

219 let tyn = getTy n (tt_ctxt i)

220 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])

222 _ -> [p]

223 ops fc n arg o = return Placeholder

224

src/Idris/ElabDecls.hs+25−12

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

58 addStatics n cty ty'

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

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

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

62+ let nty' = normalise ctxt [] nty

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

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

62 addIBC (IBCDef n)

64 addIBC (IBCDef n)

63 addDeferred ds

65 addDeferred ds

64 setFlags n opts

66 setFlags n opts

65 addIBC (IBCFlags n opts)

67 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 ()

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

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

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

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

69 = do iLOG (show fc)

79 = do iLOG (show fc)

70 checkUndefined fc n

80 checkUndefined fc n

71 ctxt <- getContext

81 ctxt <- getContext

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

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

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

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

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

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

92 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

84 ttag <- getName

94 ttag <- getName

85 i <- get

95 i <- get

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

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

87− (idris_datatypes i) })

97+ (idris_datatypes i) })

88 addIBC (IBCDef n)

98 addIBC (IBCDef n)

89 addIBC (IBCData n)

99 addIBC (IBCData n)

90 collapseCons n cons

100 collapseCons n cons

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

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

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

95 PTerm -> Name -> PTerm -> Idris ()

105 PTerm -> Name -> PTerm -> Idris ()

96elabRecord info syn fc tyn ty cn cty

106elabRecord 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)])

98 cty' <- implicit syn cn cty

108 cty' <- implicit syn cn cty

99 i <- get

109 i <- get

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

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

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

200 (map pexp rhsArgs)) []

210 (map pexp rhsArgs)) []

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

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

202

212

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

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

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

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

205 = do checkUndefined fc n

215 = do checkUndefined fc n

206 ctxt <- getContext

216 ctxt <- getContext

207 i <- get

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

209 let t = addImpl i t_in

219 let t = addImpl i t_in

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

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

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

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

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

229 else return ()

239 else return ()

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

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

231

241

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

243+ mkLazy t = t

244+

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

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

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

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

234 do ctxt <- getContext

247 do ctxt <- getContext

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

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

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

606 let ddecl = PDatadecl tn tty cons

619 let ddecl = PDatadecl tn tty cons

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

620 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

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

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

610 logLvl 5 $ "Building functions"

623 logLvl 5 $ "Building functions"

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

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

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

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

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

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

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

901 elabType info s f o n ty

914 elabType info s f o n ty

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

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

903− elabData info s f d

916+ elabData info s f co d

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

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

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

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

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

919 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

849 put x2

850 put x3

851 put x4

852− PData x1 x2 x3 -> do putWord8 3

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

853− put x1

853+ put x1

854− put x2

854+ put x2

855− put x3

855+ put x3

856+ put x4

856 PParams x1 x2 x3 -> do putWord8 4

857 PParams x1 x2 x3 -> do putWord8 4

857 put x1

858 put x1

858 put x2

859 put x2

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

911 3 -> do x1 <- get

912 3 -> do x1 <- get

912 x2 <- get

913 x2 <- get

913 x3 <- get

914 x3 <- get

915+ x4 <- get

914− return (PData x1 x2 x3)

916+ return (PData x1 x2 x3 x4)

915 4 -> do x1 <- get

917 4 -> do x1 <- get

916 x2 <- get

918 x2 <- get

917 x3 <- get

919 x3 <- get

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

1389 return (Optimise x1 x2 x3)

1391 return (Optimise x1 x2 x3)

1390

1392

1391instance Binary TypeInfo where

1393instance Binary TypeInfo where

1392− put (TI x1) = put x1

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

1395+ put x2

1393 get = do x1 <- get

1396 get = do x1 <- get

1397+ x2 <- get

1394− return (TI x1)

1398+ return (TI x1 x2)

1395

1399

1396instance Binary SynContext where

1400instance Binary SynContext where

1397 put x

1401 put x

src/Idris/Parser.hs+7−4

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

1089 toFreeze (Just Frozen) = Just Hidden

1090 toFreeze x = x

1091

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

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

1094+

1092pData :: SyntaxInfo -> IParser PDecl

1095pData :: SyntaxInfo -> IParser PDecl

1093pData syn = try (do acc <- pAccessibility

1096pData syn = try (do acc <- pAccessibility

1094− reserved "data"

1097+ co <- pDataI

1095 fc <- pfc

1098 fc <- pfc

1096 tyn_in <- pfName

1099 tyn_in <- pfName

1097 ty <- pTSig (impOK syn)

1100 ty <- pTSig (impOK syn)

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

1106 popIndent

1109 popIndent

1107 closeBlock

1110 closeBlock

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

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

1110 <|> try (do pushIndent

1113 <|> try (do pushIndent

1111 acc <- pAccessibility

1114 acc <- pAccessibility

1112− reserved "data"

1115+ co <- pDataI

1113 fc <- pfc

1116 fc <- pfc

1114 tyn_in <- pfName

1117 tyn_in <- pfName

1115 args <- many pName

1118 args <- many pName

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

1123 do let cty = bindArgs cargs conty

1126 do let cty = bindArgs cargs conty

1124 return (x, cty, cfc)) cons

1127 return (x, cty, cfc)) cons

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

1128 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'))

1127 where

1130 where

1128 mkPApp fc t [] = t

1131 mkPApp fc t [] = t

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

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

281

282elabPrims :: Idris ()

283elabPrims = do mapM_ (elabDecl toplevel)

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

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

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

286 mapM_ elabPrim primitives

287