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

git.iko.soy/Idris-dev

Documentation comment additions

commit22c355a191b3bb71e65de3733ef6a706daed623b authorDavid Christiansen <david@davidchristiansen.dk> dateTue 26 Feb 2013, 11:17 (14 years ago) parentc0bc353

4 files changed+53−40

compare with master

unifiedsplit

src/Core/Constraints.hs+2 src/Core/Evaluate.hs+10−9 src/Core/TT.hs+34−24 src/Idris/Parser.hs+7−7

src/Core/Constraints.hs+2

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

1+-- | Check universe constraints.

12module Core.Constraints(ucheck) where

34import Core.TT

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

1314

1415import Debug.Trace

1516

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

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

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

1820 where lhs (ULT l _) = l

src/Core/Evaluate.hs+10−9

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

2929initEval = ES []

3030

3131-- VALUES (as HOAS) ---------------------------------------------------------

32−

32+-- | A HOAS representation of values

3333data Value = VP NameType Name Value

3434 | VV Int

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

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

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

6363-- while building a proof.

6464

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)

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

6767normaliseC ctxt env t

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

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

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

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

8888

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

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

91−

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

9392simplify ctxt runtime env t

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

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

9897 [Simplify runtime]

9998 quote 0 val) initEval

10099

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

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

102102hnf ctxt env t

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

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

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

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

132132

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,

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

135−

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

137136 [EvalOpt] -> Eval Value

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

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

576575

577576-- CONTEXTS -----------------------------------------------------------------

578577

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

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

581580 yet undefined function, or an Operator.

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

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

620619data Accessibility = Public | Frozen | Hidden

621620 deriving (Show, Eq)

622621

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

624− | Productive

622+-- | The result of totality checking

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

624+ | Productive -- ^ productive

625625 | Partial PReason

626626 | Unchecked

627627 deriving Eq

628628

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

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

630631 | BelieveMe | Mutual [Name] | NotProductive

631632 deriving (Show, Eq)

src/Core/TT.hs+34−24

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

11{-# 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+

321module Core.TT where

422

523import Control.Monad.State

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

1230

1331import Util.Pretty hiding (Str)

1432

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−

2833data Option = TTypeInTType

2934 | CheckConv

3035 deriving Eq

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

318323deriving instance Binary Raw

319324!-}

320325

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

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

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

322328 | Pi { binderTy :: b }

323329 | Let { binderTy :: b,

324− binderVal :: b }

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

325331 | NLet { binderTy :: b,

326332 binderVal :: b }

327333 | Hole { binderTy :: b}

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

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

436442 _ == _ = False

437443

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

439− | V Int

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

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

442− | Constant Const

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

444− | Erased

445− | Impossible -- special case for totality checking

446− | TType UExp

444+-- | Terms in the core language

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

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

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

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

449+ | Constant Const -- ^ constant

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

451+ | Erased -- ^ an erased term

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

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

447454 deriving (Ord, Functor)

448455{-!

449456deriving instance Binary TT

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

501508

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

503510

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.

504514isInjective :: TT n -> Bool

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

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

src/Idris/Parser.hs+7−7

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

11{-# LANGUAGE PatternGuards #-}

2−

2+-- | Parse the full Idris language.

33module Idris.Parser where

55import Idris.AbsSyntax

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

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

260260 _ -> return ()

261261

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

262263pfc :: IParser FC

263264pfc = do s <- getPosition

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

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

270271 return (toPath f)

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

272273

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

274−-- documentation strings

275−

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

275+-- documentation strings.

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

277277 Idris [PDecl]

278278parseProg syn fname input pos

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

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

289289 return (collect x)

290290

291−-- Collect PClauses with the same function name

292−

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

293292collect :: [PDecl] -> [PDecl]

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

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

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

323322 i <- getState

324323 return $ desugar syn i x

325324

325+-- | Parse a top-level declaration

326326pDecl :: SyntaxInfo -> IParser [PDecl]

327327pDecl syn = do notEndBlock

328328 pDeclBody where

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

672672 UN n <- iName (syntax_keywords i)

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

674674

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

676676-- optional namespace.

677677pOpFront = maybeWithNS pOpFrontNoNS False []

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