22c355a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Documentation comment additions

22c355aDavid Christiansen14 years ago

src/Core/Constraints.hs+2

compare with master

unifiedsplit

@@ -1,3 +1,4 @@

1+-- | Check universe constraints.

1module Core.Constraints(ucheck) where

2module Core.Constraints(ucheck) where

3import Core.TT

4import Core.TT

@@ -13,6 +14,7 @@ import qualified Data.Map as M

14import Debug.Trace

15import Debug.Trace

17+-- | Check that a list of universe constraints can be satisfied.

16ucheck :: [(UConstraint, FC)] -> TC ()

18ucheck :: [(UConstraint, FC)] -> TC ()

17ucheck cs = acyclic rels (map fst (M.toList rels))

19ucheck cs = acyclic rels (map fst (M.toList rels))

18 where lhs (ULT l _) = l

20 where lhs (ULT l _) = l

src/Core/Evaluate.hs+10−9

@@ -29,7 +29,7 @@ data EvalOpt = Spec | HNF | Simplify Bool | AtREPL

29initEval = ES []

31-- VALUES (as HOAS) ---------------------------------------------------------

32−

32+-- | A HOAS representation of values

33data Value = VP NameType Name Value

34 | VV Int

35 | VBind Name (Binder Value) (Value -> Eval Value)

@@ -62,7 +62,7 @@ instance Show (a -> b) where

62-- i.e. it's an intermediate environment that we have while type checking or

63-- while building a proof.

65−-- Normalise fully type checked terms (so, assume all names/let bindings resolved)

65+-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)

66normaliseC :: Context -> Env -> TT Name -> TT Name

67normaliseC ctxt env t

68 = evalState (do val <- eval False ctxt [] env t []

@@ -86,9 +86,8 @@ specialise ctxt env limits t

86 = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []

87 quote 0 val) (initEval { limited = limits })

89−-- Like normalise, but we only reduce functions that are marked as okay to

89+-- | Like normalise, but we only reduce functions that are marked as okay to

90-- inline (and probably shouldn't reduce lets?)

91−

92simplify :: Context -> Bool -> Env -> TT Name -> TT Name

91simplify :: Context -> Bool -> Env -> TT Name -> TT Name

93simplify ctxt runtime env t

92simplify ctxt runtime env t

94 = evalState (do val <- eval False ctxt [(UN "lazy", 0),

93 = evalState (do val <- eval False ctxt [(UN "lazy", 0),

@@ -98,6 +97,7 @@ simplify ctxt runtime env t

98 [Simplify runtime]

97 [Simplify runtime]

99 quote 0 val) initEval

98 quote 0 val) initEval

100

100+-- | Reduce a term to head normal form

101hnf :: Context -> Env -> TT Name -> TT Name

102hnf ctxt env t

103 = evalState (do val <- eval False ctxt []

@@ -130,9 +130,8 @@ usable s n ns = case lookup n ns of

130 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)

131 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)

132

133−-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

133+-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,

134-- such as we might have during construction of a proof)

135−

136eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

135eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->

137 [EvalOpt] -> Eval Value

136 [EvalOpt] -> Eval Value

138eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

137eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

@@ -576,7 +575,7 @@ spec ctxt statics genv tm = error "spec undefined"

576

575

577-- CONTEXTS -----------------------------------------------------------------

576-- CONTEXTS -----------------------------------------------------------------

578

577

579−{- A definition is either a simple function (just an expression with a type),

578+{-| A definition is either a simple function (just an expression with a type),

580 a constant, which could be a data or type constructor, an axiom or as an

579 a constant, which could be a data or type constructor, an axiom or as an

581 yet undefined function, or an Operator.

580 yet undefined function, or an Operator.

582 An Operator is a function which explains how to reduce.

581 An Operator is a function which explains how to reduce.

@@ -620,12 +619,14 @@ instance Binary (a -> b) where

620data Accessibility = Public | Frozen | Hidden

619data Accessibility = Public | Frozen | Hidden

621 deriving (Show, Eq)

620 deriving (Show, Eq)

622

621

622+-- | The result of totality checking

623−data Totality = Total [Int] -- well-founded arguments

623+data Totality = Total [Int] -- ^ well-founded arguments

624− | Productive

624+ | Productive -- ^ productive

625 | Partial PReason

626 | Unchecked

627 deriving Eq

628

629+-- | Reasons why a function may not be total

629data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

630data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

630 | BelieveMe | Mutual [Name] | NotProductive

631 | BelieveMe | Mutual [Name] | NotProductive

631 deriving (Show, Eq)

632 deriving (Show, Eq)

src/Core/TT.hs+34−24

@@ -1,5 +1,23 @@

1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

3+{-| TT is the core language of Idris. The language has:

5+ * Full dependent types

7+ * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...

9+ * Pattern matching letrec binding

10+

11+ * (primitive types defined externally)

12+

13+ Some technical stuff:

14+

15+ * Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.

16+

17+ * We have a simple collection of tactics which we use to elaborate source

18+ programs with implicit syntax into fully explicit terms.

19+-}

20+

3module Core.TT where

21module Core.TT where

5import Control.Monad.State

23import Control.Monad.State

@@ -12,19 +30,6 @@ import Data.Binary hiding (get, put)

13import Util.Pretty hiding (Str)

31import Util.Pretty hiding (Str)

15−{- The language has:

16− * Full dependent types

17− * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...

18− * Pattern matching letrec binding

19− * (primitive types defined externally)

20−

21− Some technical stuff:

22− * Typechecker is kept as simple as possible

23− - no unification, just a checker for incomplete terms.

24− * We have a simple collection of tactics which we use to elaborate source

25− programs with implicit syntax into fully explicit terms.

26−-}

27−

28data Option = TTypeInTType

33data Option = TTypeInTType

29 | CheckConv

34 | CheckConv

30 deriving Eq

35 deriving Eq

@@ -318,10 +323,11 @@ instance Pretty Raw where

318deriving instance Binary Raw

323deriving instance Binary Raw

319!-}

324!-}

320

325

326+-- | All binding forms are represented in a unform fashion.

321−data Binder b = Lam { binderTy :: b }

327+data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}

322 | Pi { binderTy :: b }

328 | Pi { binderTy :: b }

323 | Let { binderTy :: b,

329 | Let { binderTy :: b,

324− binderVal :: b }

330+ binderVal :: b {-^ value for bound variable-}}

325 | NLet { binderTy :: b,

331 | NLet { binderTy :: b,

326 binderVal :: b }

332 binderVal :: b }

327 | Hole { binderTy :: b}

333 | Hole { binderTy :: b}

@@ -435,15 +441,16 @@ instance Eq NameType where

435 TCon _ a == TCon _ b = (a == b) -- ignore tag

441 TCon _ a == TCon _ b = (a == b) -- ignore tag

436 _ == _ = False

442 _ == _ = False

437

443

444+-- | Terms in the core language

438−data TT n = P NameType n (TT n) -- embed type

445+data TT n = P NameType n (TT n) -- ^ named references

439− | V Int

446+ | V Int -- ^ a resolved de Bruijn-indexed variable

440− | Bind n (Binder (TT n)) (TT n)

447+ | Bind n (Binder (TT n)) (TT n) -- ^ a binding

441− | App (TT n) (TT n) -- function, function type, arg

448+ | App (TT n) (TT n) -- ^ function, function type, arg

442− | Constant Const

449+ | Constant Const -- ^ constant

443− | Proj (TT n) Int -- argument projection; runtime only

450+ | Proj (TT n) Int -- ^ argument projection; runtime only

444− | Erased

451+ | Erased -- ^ an erased term

445− | Impossible -- special case for totality checking

452+ | Impossible -- ^ special case for totality checking

446− | TType UExp

453+ | TType UExp -- ^ the type of types at some level

447 deriving (Ord, Functor)

454 deriving (Ord, Functor)

448{-!

455{-!

449deriving instance Binary TT

456deriving instance Binary TT

@@ -501,6 +508,9 @@ instance Eq n => Eq (TT n) where

501

508

502-- * A few handy operations on well typed terms:

509-- * A few handy operations on well typed terms:

503

510

511+-- | A term is injective iff it is a data constructor, type constructor,

512+-- constant, the type Type, pi-binding, or an application of an injective

513+-- term.

504isInjective :: TT n -> Bool

514isInjective :: TT n -> Bool

505isInjective (P (DCon _ _) _ _) = True

515isInjective (P (DCon _ _) _ _) = True

506isInjective (P (TCon _ _) _ _) = True

516isInjective (P (TCon _ _) _ _) = True

src/Idris/Parser.hs+7−7

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−

2+-- | Parse the full Idris language.

3module Idris.Parser where

5import Idris.AbsSyntax

@@ -259,6 +259,7 @@ notEndBlock = do ist <- getState

259 when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"

260 _ -> return ()

261

262+-- | Use Parsec's internal state to construct a source code position

262pfc :: IParser FC

263pfc :: IParser FC

263pfc = do s <- getPosition

264pfc = do s <- getPosition

264 let (dir, file) = splitFileName (sourceName s)

265 let (dir, file) = splitFileName (sourceName s)

@@ -270,9 +271,8 @@ pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

270 return (toPath f)

271 return (toPath f)

271 where toPath n = foldl1 (</>) $ splitOn "." n

272 where toPath n = foldl1 (</>) $ splitOn "." n

272

273

273−-- a program is a list of declarations, possibly with associated

274+-- | A program is a list of declarations, possibly with associated

274−-- documentation strings

275+-- documentation strings.

275−

276parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos ->

277 Idris [PDecl]

278parseProg syn fname input pos

@@ -288,8 +288,7 @@ parseProg syn fname input pos

288 Right (x, i) -> do putIState i

289 return (collect x)

290

291−-- Collect PClauses with the same function name

291+-- | Collect 'PClauses' with the same function name

292−

293collect :: [PDecl] -> [PDecl]

292collect :: [PDecl] -> [PDecl]

294collect (c@(PClauses _ o _ _) : ds)

293collect (c@(PClauses _ o _ _) : ds)

295 = clauses (cname c) [] (c : ds)

294 = clauses (cname c) [] (c : ds)

@@ -323,6 +322,7 @@ pFullExpr syn

323 i <- getState

322 i <- getState

324 return $ desugar syn i x

323 return $ desugar syn i x

325

324

325+-- | Parse a top-level declaration

326pDecl :: SyntaxInfo -> IParser [PDecl]

327pDecl syn = do notEndBlock

328 pDeclBody where

@@ -672,7 +672,7 @@ pName = do i <- getState

672 UN n <- iName (syntax_keywords i)

673 return (UN ('@':n))

674

675−-- Parser for an operator in function position, i.e. enclosed by `()', with an

675+-- | Parser for an operator in function position, i.e. enclosed by `()', with an

676-- optional namespace.

677pOpFront = maybeWithNS pOpFrontNoNS False []

678 where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o