8ea902d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added %hide and %freeze directives

8ea902dEdwin Brady15 years ago

impl-paper/macros.ltx+3−3

compare with master

unifiedsplit

@@ -387,7 +387,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

387

388%%%%%%%%%%%% TYPE

389

390−\newcommand{\Type}{\mbox{\texttt{\#}}} %\star}

390+\newcommand{\Type}{\mbox{\texttt{Set}}} %\star}

391

392

393%%%%%%%%%%%%% ARROWS

@@ -600,8 +600,8 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

600\newcommand{\farrow}{\Rightarrow}

601\newcommand{\lookup}{\FN{lookup}}

602

603−% \newcommand{\source}{\Lang{TT}}

603+\newcommand{\source}{\Lang{TT}}

604−\newcommand{\source}{\textbf{DT-Res}}

604+%\newcommand{\source}{\textbf{DT-Res}}

605\newcommand{\target}{\Lang{ExTT}}

606\newcommand{\runtime}{\Lang{RunTT}}

607

impl-paper/syntax.tex+10−1

@@ -1 +1,10 @@

1+\section{High Level Structures}

3+\subsection{\texttt{where} clauses}

5+\subsection{The \texttt{with} rule}

7+\subsection{Type Classes}

1−\section{Syntactic Sugar}

9+\subsection{Syntactic Sugar}

10+

impl-paper/typechecking.tex+17

@@ -1 +1,18 @@

1\section{The Core Type Theory}

3+\DM{

4+\begin{array}{rll@{\hg}|rll}

5+\vt ::= & \Type_i & (\mbox{type universes}) &

6+\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\

8+ \mid & \vx & (\mbox{variable}) &

9+ \mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\

10+

11+ \mid & \vb\SC\:\vt & (\mbox{binding}) &

12+ \mid & \all{\vx}{\vt} & (\mbox{function space}) \\

13+

14+ \mid & \vt\:\vt & (\mbox{application})

15+

16+\end{array}

17+}

18+

lib/prelude/list.idr+4

@@ -50,6 +50,10 @@ elem : Eq a => a -> List a -> Bool;

50elem x [] = False;

51elem x (y :: ys) = if (x == y) then True else (elem x ys);

53+lookup : Eq k => k -> List (k, v) -> Maybe v;

54+lookup k [] = Nothing;

55+lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs);

56+

53sort : Ord a => List a -> List a;

57sort : Ord a => List a -> List a;

54sort [] = [];

58sort [] = [];

55sort [x] = [x];

59sort [x] = [x];

lib/prelude/strings.idr+11

@@ -2,6 +2,7 @@ module prelude.strings;

3import builtins;

4import prelude.list;

5+import prelude.char;

6-- Some more complex string operations

7-- Some more complex string operations

@@ -49,3 +50,13 @@ break p = span (not . p);

50split : (Char -> Bool) -> String -> List String;

51split : (Char -> Bool) -> String -> List String;

51split p xs = map pack (split p (unpack xs));

52split p xs = map pack (split p (unpack xs));

53+

54+ltrim : String -> String;

55+ltrim xs with strM xs {

56+ ltrim "" | StrNil = "";

57+ ltrim (strCons x xs) | StrCons _ _

58+ = if (isSpace x) then (ltrim xs) else (strCons x xs);

59+}

60+

61+trim : String -> String;

62+trim xs = ltrim (rev (ltrim (rev xs)));

src/Core/Evaluate.hs+49−26

@@ -2,9 +2,9 @@

2 PatternGuards #-}

4module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

5− Def(..),

5+ Def(..), Accessibility(..),

6 Context, initContext, ctxtAlist, uconstraints, next_tvar,

7− addToCtxt, addCtxtDef, addTyDecl, addDatatype,

7+ addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

8 addCasedef, addOperator,

9 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

10 Value(..)) where

@@ -108,11 +108,11 @@ eval ctxt statics genv tm opts = ev True [] tm where

108

109 ev top env (P _ n ty)

110 | Just (Let t v) <- lookup n genv = ev top env v

111− ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of

111+ ev top env (P Ref n ty) = case lookupDefAcc Nothing n ctxt of

112− [Function _ tm] -> ev True env tm

112+ [(Function _ tm, Public)] -> trace ("Eval " ++ show n) $ ev True env tm

113− [TyDecl nt ty] -> do vty <- ev True env ty

113+ [(TyDecl nt ty, _)] -> do vty <- ev True env ty

114− return $ VP nt n vty

114+ return $ VP nt n vty

115− [CaseOp inl _ _ [] tree] ->

115+ [(CaseOp inl _ _ [] tree, Public)] ->

116 if simpl && (not inl)

117 then liftM (VP Ref n) (ev top env ty)

118 else do c <- evCase top env [] [] tree

@@ -153,7 +153,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

153 apply False env f args

154 | spec = return $ unload env f args

155 apply top env (VP Ref n ty) args

156− | [CaseOp inl _ _ ns tree] <- lookupDef Nothing n ctxt

156+ | [(CaseOp inl _ _ ns tree, Public)] <- lookupDefAcc Nothing n ctxt

157 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

158 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

159 else do c <- evCase top env ns args tree

@@ -449,32 +449,47 @@ instance Binary (a -> b) where

449

450-------

451

452+-- Frozen => doesn't reduce

453+-- Hidden => doesn't reduce and invisible to type checker

454+

455+data Accessibility = Public | Frozen | Hidden

456+ deriving (Show, Eq)

457+{-!

458+deriving instance Binary Accessibility

459+!-}

460+

452data Context = MkContext { uconstraints :: [UConstraint],

461data Context = MkContext { uconstraints :: [UConstraint],

453 next_tvar :: Int,

462 next_tvar :: Int,

454− definitions :: Ctxt Def }

463+ definitions :: Ctxt (Def, Accessibility) }

455

464

456initContext = MkContext [] 0 emptyContext

465initContext = MkContext [] 0 emptyContext

457

466

458ctxtAlist :: Context -> [(Name, Def)]

467ctxtAlist :: Context -> [(Name, Def)]

459−ctxtAlist ctxt = toAlist (definitions ctxt)

468+ctxtAlist ctxt = map (\(n, (d, a)) -> (n, d)) $ toAlist (definitions ctxt)

460

469

461veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

470veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

462

471

463addToCtxt :: Name -> Term -> Type -> Context -> Context

472addToCtxt :: Name -> Term -> Type -> Context -> Context

464addToCtxt n tm ty uctxt

473addToCtxt n tm ty uctxt

465 = let ctxt = definitions uctxt

474 = let ctxt = definitions uctxt

466− ctxt' = addDef n (Function ty tm) ctxt in

475+ ctxt' = addDef n (Function ty tm, Public) ctxt in

467 uctxt { definitions = ctxt' }

476 uctxt { definitions = ctxt' }

468

477

478+setAccess :: Name -> Accessibility -> Context -> Context

479+setAccess n a uctxt

480+ = let ctxt = definitions uctxt

481+ ctxt' = updateDef n (\ (d, _) -> (d, a)) ctxt in

482+ uctxt { definitions = ctxt' }

483+

469addCtxtDef :: Name -> Def -> Context -> Context

484addCtxtDef :: Name -> Def -> Context -> Context

470addCtxtDef n d c = let ctxt = definitions c

485addCtxtDef n d c = let ctxt = definitions c

471− ctxt' = addDef n d ctxt in

486+ ctxt' = addDef n (d, Public) ctxt in

472 c { definitions = ctxt' }

487 c { definitions = ctxt' }

473

488

474addTyDecl :: Name -> Type -> Context -> Context

489addTyDecl :: Name -> Type -> Context -> Context

475addTyDecl n ty uctxt

490addTyDecl n ty uctxt

476 = let ctxt = definitions uctxt

491 = let ctxt = definitions uctxt

477− ctxt' = addDef n (TyDecl Ref ty) ctxt in

492+ ctxt' = addDef n (TyDecl Ref ty, Public) ctxt in

478 uctxt { definitions = ctxt' }

493 uctxt { definitions = ctxt' }

479

494

480addDatatype :: Datatype Name -> Context -> Context

495addDatatype :: Datatype Name -> Context -> Context

@@ -482,14 +497,14 @@ addDatatype (Data n tag ty cons) uctxt

482 = let ctxt = definitions uctxt

497 = let ctxt = definitions uctxt

483 ty' = normalise uctxt [] ty

498 ty' = normalise uctxt [] ty

484 ctxt' = addCons 0 cons (addDef n

499 ctxt' = addCons 0 cons (addDef n

485− (TyDecl (TCon tag (arity ty')) ty) ctxt) in

500+ (TyDecl (TCon tag (arity ty')) ty, Public) ctxt) in

486 uctxt { definitions = ctxt' }

501 uctxt { definitions = ctxt' }

487 where

502 where

488 addCons tag [] ctxt = ctxt

503 addCons tag [] ctxt = ctxt

489 addCons tag ((n, ty) : cons) ctxt

504 addCons tag ((n, ty) : cons) ctxt

490 = let ty' = normalise uctxt [] ty in

505 = let ty' = normalise uctxt [] ty in

491 addCons (tag+1) cons (addDef n

506 addCons (tag+1) cons (addDef n

492− (TyDecl (DCon tag (arity ty')) ty) ctxt)

507+ (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

493

508

494addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

509addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

495addCasedef n alwaysInline tcase ps ty uctxt

510addCasedef n alwaysInline tcase ps ty uctxt

@@ -497,7 +512,8 @@ addCasedef n alwaysInline tcase ps ty uctxt

497 ps' = ps -- simpl ps in

512 ps' = ps -- simpl ps in

498 ctxt' = case simpleCase tcase ps' of

513 ctxt' = case simpleCase tcase ps' of

499 CaseDef args sc -> let inl = alwaysInline in

514 CaseDef args sc -> let inl = alwaysInline in

500− addDef n (CaseOp inl ty ps args sc) ctxt in

515+ addDef n (CaseOp inl ty ps args sc,

516+ Public) ctxt in

501 uctxt { definitions = ctxt' }

517 uctxt { definitions = ctxt' }

502 where simpl [] = []

518 where simpl [] = []

503 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

519 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

@@ -505,13 +521,13 @@ addCasedef n alwaysInline tcase ps ty uctxt

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

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

506addOperator n ty a op uctxt

522addOperator n ty a op uctxt

507 = let ctxt = definitions uctxt

523 = let ctxt = definitions uctxt

508− ctxt' = addDef n (Operator ty a op) ctxt in

524+ ctxt' = addDef n (Operator ty a op, Public) ctxt in

509 uctxt { definitions = ctxt' }

525 uctxt { definitions = ctxt' }

510

526

511lookupTy :: Maybe [String] -> Name -> Context -> [Type]

527lookupTy :: Maybe [String] -> Name -> Context -> [Type]

512lookupTy root n ctxt

528lookupTy root n ctxt

513 = do def <- lookupCtxt root n (definitions ctxt)

529 = do def <- lookupCtxt root n (definitions ctxt)

514− case def of

530+ case fst def of

515 (Function ty _) -> return ty

531 (Function ty _) -> return ty

516 (TyDecl _ ty) -> return ty

532 (TyDecl _ ty) -> return ty

517 (Operator ty _ _) -> return ty

533 (Operator ty _ _) -> return ty

@@ -520,20 +536,26 @@ lookupTy root n ctxt

520lookupP :: Maybe [String] -> Name -> Context -> [Term]

536lookupP :: Maybe [String] -> Name -> Context -> [Term]

521lookupP root n ctxt

537lookupP root n ctxt

522 = do def <- lookupCtxt root n (definitions ctxt)

538 = do def <- lookupCtxt root n (definitions ctxt)

523− case def of

539+ p <- case def of

524− (Function ty tm) -> return (P Ref n ty)

540+ (Function ty tm, a) -> return (P Ref n ty, a)

525− (TyDecl nt ty) -> return (P nt n ty)

541+ (TyDecl nt ty, a) -> return (P nt n ty, a)

526− (CaseOp _ ty _ _ _) -> return (P Ref n ty)

542+ (CaseOp _ ty _ _ _, a) -> return (P Ref n ty, a)

527− (Operator ty _ _) -> return (P Ref n ty)

543+ (Operator ty _ _, a) -> return (P Ref n ty, a)

544+ case snd p of

545+ Hidden -> []

546+ _ -> return (fst p)

528

547

529lookupDef :: Maybe [String] -> Name -> Context -> [Def]

548lookupDef :: Maybe [String] -> Name -> Context -> [Def]

549+lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)

550+

551+lookupDefAcc :: Maybe [String] -> Name -> Context -> [(Def, Accessibility)]

530−lookupDef root n ctxt = lookupCtxt root n (definitions ctxt)

552+lookupDefAcc root n ctxt = lookupCtxt root n (definitions ctxt)

531

553

532lookupVal :: Maybe [String] -> Name -> Context -> [Value]

554lookupVal :: Maybe [String] -> Name -> Context -> [Value]

533lookupVal root n ctxt

555lookupVal root n ctxt

534 = do def <- lookupCtxt root n (definitions ctxt)

556 = do def <- lookupCtxt root n (definitions ctxt)

535− case def of

557+ case fst def of

536− (Function _ htm) -> return (veval ctxt [] htm)

558+ (Function _ htm) -> return (veval ctxt [] htm)

537 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

559 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

538

560

539lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

561lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

@@ -542,3 +564,4 @@ lookupTyEnv n env = li n 0 env where

542 li n i ((x, b): xs)

564 li n i ((x, b): xs)

543 | n == x = Just (i, binderTy b)

565 | n == x = Just (i, binderTy b)

544 | otherwise = li n (i+1) xs

566 | otherwise = li n (i+1) xs

567+

src/Core/TT.hs+8−3

@@ -110,8 +110,8 @@ instance Show Name where

110 show (MN i s) = "{" ++ s ++ show i ++ "}"

111

112

113−-- Contexts allow us to map names to things

113+-- Contexts allow us to map names to things. A root name maps to a collection

114−-- TODO: Namespaces and ambiguous names

114+-- of things in different namespaces with that name.

115

116type Ctxt a = Map.Map Name (Map.Map Name a)

117emptyContext = Map.empty

@@ -119,7 +119,7 @@ emptyContext = Map.empty

119nsroot (NS n _) = n

120nsroot n = n

121

122−addDef :: Show a => Name -> a -> Ctxt a -> Ctxt a

122+addDef :: Name -> a -> Ctxt a -> Ctxt a

123addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

124 Nothing -> Map.insert (nsroot n)

125 (Map.insert n v Map.empty) ctxt

@@ -155,6 +155,11 @@ lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

155lookupCtxt :: Maybe [String] -> Name -> Ctxt a -> [a]

156lookupCtxt ns n ctxt = map snd (lookupCtxtName ns n ctxt)

157

158+updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

159+updateDef n f ctxt

160+ = let ds = lookupCtxtName Nothing n ctxt in

161+ foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds

162+

158toAlist :: Ctxt a -> [(Name, a)]

163toAlist :: Ctxt a -> [(Name, a)]

159toAlist ctxt = let allns = map snd (Map.toList ctxt) in

164toAlist ctxt = let allns = map snd (Map.toList ctxt) in

160 concat (map (Map.toList) allns)

165 concat (map (Map.toList) allns)

src/Idris/AbsSyntax.hs+13−1

@@ -64,6 +64,7 @@ data IBCWrite = IBCFix FixDecl

64 | IBCObj FilePath

65 | IBCLib String

66 | IBCHeader String

67+ | IBCAccess Name Accessibility

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

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

68 deriving Show

69 deriving Show

@@ -92,6 +93,12 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

92addHdr :: String -> Idris ()

93addHdr :: String -> Idris ()

93addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

94addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

96+setAccessibility :: Name -> Accessibility -> Idris ()

97+setAccessibility n a

98+ = do i <- get

99+ let ctxt = setAccess n a (tt_ctxt i)

100+ put (i { tt_ctxt = ctxt })

101+

95addIBC :: IBCWrite -> Idris ()

102addIBC :: IBCWrite -> Idris ()

96addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

103addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

104

@@ -298,7 +305,7 @@ inlinable :: FnOpts -> Bool

298inlinable = elem Inlinable

305inlinable = elem Inlinable

299

306

300data PDecl' t = PFix FC Fixity [String] -- fixity declaration

307data PDecl' t = PFix FC Fixity [String] -- fixity declaration

301− | PTy SyntaxInfo FC Name t -- type declaration

308+ | PTy SyntaxInfo FC Name t -- type declaration

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

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

303 | PData SyntaxInfo FC (PData' t) -- data declaration

310 | PData SyntaxInfo FC (PData' t) -- data declaration

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

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

@@ -640,7 +647,12 @@ showImp impl tm = se 10 tm where

640 se p (PProof ts) = "proof { " ++ show ts ++ "}"

647 se p (PProof ts) = "proof { " ++ show ts ++ "}"

641 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

648 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

642 se p (PMetavar n) = "?" ++ show n

649 se p (PMetavar n) = "?" ++ show n

650+ se p (PReturn f) = "return"

651+ se p PImpossible = "impossible"

643 se p Placeholder = "_"

652 se p Placeholder = "_"

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

654+ se p (PElabError s) = s

655+-- se p x = "Not implemented"

644

656

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

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

646 sArg (PExp _ _ tm) = seArg tm

658 sArg (PExp _ _ tm) = seArg tm

src/Idris/ElabTerm.hs+1−1

@@ -200,7 +200,7 @@ elab ist info pattern fn tm

200 elab' (PProof ts) = do mapM_ (runTac True ist) ts

201 elab' (PTactics ts) = do mapM_ (runTac False ist) ts

202 elab' (PElabError e) = fail e

203− elab' x = fail $ "Not implemented " ++ show x

203+ elab' x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

204

205 elabArgs failed retry [] _

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

src/Idris/IBC.hs+29−6

@@ -22,7 +22,7 @@ import System.Posix.Files

22import Paths_idris

24ibcVersion :: Word8

25−ibcVersion = 3

25+ibcVersion = 4

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

@@ -36,13 +36,14 @@ data IBCFile = IBCFile { ver :: Word8,

36 ibc_objs :: [FilePath],

37 ibc_libs :: [String],

38 ibc_hdrs :: [String],

39+ ibc_access :: [(Name, Accessibility)],

39 ibc_defs :: [(Name, Def)] }

40 ibc_defs :: [(Name, Def)] }

40{-!

41{-!

41deriving instance Binary IBCFile

42deriving instance Binary IBCFile

42!-}

43!-}

44initIBC :: IBCFile

45initIBC :: IBCFile

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

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

47loadIBC :: FilePath -> Idris ()

48loadIBC :: FilePath -> Idris ()

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

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

@@ -87,8 +88,9 @@ ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

87ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

88ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

88ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

89ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

89ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

90ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

90− [v] -> return f { ibc_defs = (n,v): ibc_defs f }

91+ [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

91 _ -> fail "IBC write failed"

92 _ -> fail "IBC write failed"

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

93process :: IBCFile -> FilePath -> Idris ()

95process :: IBCFile -> FilePath -> Idris ()

94process i fn

96process i fn

@@ -107,6 +109,7 @@ process i fn

107 pLibs (ibc_libs i)

109 pLibs (ibc_libs i)

108 pHdrs (ibc_hdrs i)

110 pHdrs (ibc_hdrs i)

109 pDefs (ibc_defs i)

111 pDefs (ibc_defs i)

112+ pAccess (ibc_access i)

110

113

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

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

112timestampOlder src ibc = do srcok <- doesFileExist src

115timestampOlder src ibc = do srcok <- doesFileExist src

@@ -180,7 +183,12 @@ pDefs ds = mapM_ (\ (n, d) ->

180 do i <- getIState

183 do i <- getIState

181 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

184 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

182 ds

185 ds

183−

186+

187+pAccess :: [(Name, Accessibility)] -> Idris ()

188+pAccess ds = mapM_ (\ (n, a) ->

189+ do i <- getIState

190+ putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

191+ ds

184

192

185----- Generated by 'derive'

193----- Generated by 'derive'

186

194

@@ -505,9 +513,22 @@ instance Binary Def where

505 return (CaseOp x1 x2 x3 x4 x5)

513 return (CaseOp x1 x2 x3 x4 x5)

506 _ -> error "Corrupted binary data for Def"

514 _ -> error "Corrupted binary data for Def"

507

515

516+instance Binary Accessibility where

517+ put x

518+ = case x of

519+ Public -> putWord8 0

520+ Frozen -> putWord8 1

521+ Hidden -> putWord8 2

522+ get

523+ = do i <- getWord8

524+ case i of

525+ 0 -> return Public

526+ 1 -> return Frozen

527+ 2 -> return Hidden

528+ _ -> error "Corrupted binary data for Accessibility"

508

529

509instance Binary IBCFile where

530instance Binary IBCFile where

510− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

531+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

511 = do put x1

532 = do put x1

512 put x2

533 put x2

513 put x3

534 put x3

@@ -521,6 +542,7 @@ instance Binary IBCFile where

521 put x11

542 put x11

522 put x12

543 put x12

523 put x13

544 put x13

545+ put x14

524 get

546 get

525 = do x1 <- get

547 = do x1 <- get

526 if x1 == ibcVersion then

548 if x1 == ibcVersion then

@@ -536,7 +558,8 @@ instance Binary IBCFile where

536 x11 <- get

558 x11 <- get

537 x12 <- get

559 x12 <- get

538 x13 <- get

560 x13 <- get

561+ x14 <- get

539− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

562+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

540 else return (initIBC { ver = x1 })

563 else return (initIBC { ver = x1 })

541

564

542instance Binary Fixity where

565instance Binary Fixity where

src/Idris/Parser.hs+6

@@ -862,6 +862,12 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

862 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

863 return [PDirective (do addHdr hdr

864 addIBC (IBCHeader hdr))])

865+ <|> try (do lchar '%'; reserved "hide"; n <- iName []

866+ return [PDirective (do setAccessibility n Hidden

867+ addIBC (IBCAccess n Hidden))])

868+ <|> try (do lchar '%'; reserved "freeze"; n <- iName []

869+ return [PDirective (do setAccessibility n Frozen

870+ addIBC (IBCAccess n Frozen))])

865 <|> do lchar '%'; reserved "logging"; i <- natural;

871 <|> do lchar '%'; reserved "logging"; i <- natural;

866 return [PDirective (setLogLevel (fromInteger i))]

872 return [PDirective (setLogLevel (fromInteger i))]

867

873

tutorial/typesfuns.tex+20−2

@@ -198,12 +198,14 @@ Ambiguous constructor names can normally be resolved from context.

198

199This declares a family of types, and so the form of the declaration is rather

200different from the simple type declarations above. We explicitly state the type

201−of the type constructor \tTC{Vect} - it takes a type and a \tTC{Nat} as an

201+of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

202argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}

203is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

204constructor targets a different part of the family of types. \tDC{Nil} can only

205be used to construct vectors with zero length, and \tDC{::} to constructor

206−vectors with non-zero length.

206+vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element

207+of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})

208+combine to make a vector of length \texttt{S k}.

207

209

208We can define functions on dependent types such as \tTC{Vect} in the same way

210We can define functions on dependent types such as \tTC{Vect} in the same way

209as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.

211as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.

@@ -295,6 +297,22 @@ since it would force \texttt{n} to be \tDC{O}.

295

297

296\subsubsection{Dependent Function Types}

298\subsubsection{Dependent Function Types}

297

299

300+The function types we have seen so far have taken the form \texttt{a -> b},

301+where \texttt{a} stands for the input type and \texttt{b} stands for the output

302+type. More generally, function types take the following form:

303+

304+\begin{SaveVerbatim}{ftype}

305+

306+(x : a) -> b

307+

308+\end{SaveVerbatim}

309+\useverb{ftype}

310+

311+\noindent

312+\ldots where the name \texttt{x} may appear in \texttt{b}. This is a \remph{dependent}

313+function type --- the output type depends on the value of \texttt{x}.

314+

315+

298\subsubsection{Implicit Arguments}

316\subsubsection{Implicit Arguments}

299

317

300\subsection{Useful Data Types}

318\subsection{Useful Data Types}