318e20d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #197 from david-christiansen/haddock

318e20dEdwin Brady14 years ago

src/Core/CaseTree.hs+2−2

compare with master

unifiedsplit

@@ -418,8 +418,8 @@ depatt ns tm = dp [] tm

418 applyMaps ms (App f a) = App (applyMaps ms f) (applyMaps ms a)

419 applyMaps ms t = t

420

421−prune :: Bool -> -- ^ Convert single branches to projections (only useful at runtime)

421+prune :: Bool -- ^ Convert single branches to projections (only useful at runtime)

422− SC -> SC

422+ -> SC -> SC

423prune proj (Case n alts)

424 = let alts' = filter notErased (map pruneAlt alts) in

425 case alts' of

src/Core/Elaborate.hs+1−1

@@ -379,7 +379,7 @@ apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

379apply fn imps =

380 do args <- prepare_apply fn (map fst imps)

381 fill (raw_apply fn (map Var args))

382− -- *Don't* solve the arguments we're specifying by hand.

382+ -- _Don't_ solve the arguments we're specifying by hand.

383 -- (remove from unified list before calling end_unify)

384 -- HMMM: Actually, if we get it wrong, the typechecker will complain!

385 -- so do nothing

src/Core/Evaluate.hs+4

@@ -655,14 +655,18 @@ deriving instance Binary Totality

655deriving instance Binary PReason

656!-}

657

658+-- | Contexts used for global definitions and for proof state. They contain

659+-- universe constraints and existing definitions.

658data Context = MkContext {

660data Context = MkContext {

659 uconstraints :: [UConstraint],

661 uconstraints :: [UConstraint],

660 next_tvar :: Int,

662 next_tvar :: Int,

661 definitions :: Ctxt (Def, Accessibility, Totality)

663 definitions :: Ctxt (Def, Accessibility, Totality)

662 }

664 }

663

665

666+-- | The initial empty context

664initContext = MkContext [] 0 emptyContext

667initContext = MkContext [] 0 emptyContext

665

668

669+-- | Get the definitions from a context

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

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

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

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

668

672

src/Core/TT.hs+29−30

@@ -29,8 +29,10 @@ data Option = TTypeInTType

29 | CheckConv

30 deriving Eq

32+-- | Source location. These are typically produced by the parser 'Idris.Parser.pfc'

32−data FC = FC { fc_fname :: String,

33+data FC = FC { fc_fname :: String, -- ^ Filename

33− fc_line :: Int }

34+ fc_line :: Int -- ^ Line number

35+ }

34 deriving Eq

36 deriving Eq

35{-!

37{-!

36deriving instance Binary FC

38deriving instance Binary FC

@@ -163,14 +165,12 @@ traceWhen False _ a = a

163

165

164-- RAW TERMS ----------------------------------------------------------------

166-- RAW TERMS ----------------------------------------------------------------

165

167

166−-- Names are hierarchies of strings, describing scope (so no danger of

168+-- | Names are hierarchies of strings, describing scope (so no danger of

167-- duplicate names, but need to be careful on lookup).

169-- duplicate names, but need to be careful on lookup).

168−-- Also MN for machine chosen names

169−

170−data Name = UN String

170+data Name = UN String -- ^ User-provided name

171− | NS Name [String] -- root, namespaces

171+ | NS Name [String] -- ^ Root, namespaces

172− | MN Int String

172+ | MN Int String -- ^ Machine chosen names

173− | NErased -- name of somethng which is never used in scope

173+ | NErased -- ^ Name of somethng which is never used in scope

174 deriving (Eq, Ord)

175{-!

176deriving instance Binary Name

@@ -193,9 +193,8 @@ instance Show Name where

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

194 show NErased = "_"

195

196−-- Contexts allow us to map names to things. A root name maps to a collection

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

197-- of things in different namespaces with that name.

198−

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

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

200emptyContext = Map.empty

199emptyContext = Map.empty

201

200

@@ -217,14 +216,17 @@ addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

217 Just xs -> Map.insert (nsroot n)

216 Just xs -> Map.insert (nsroot n)

218 (Map.insert n v xs) ctxt

217 (Map.insert n v xs) ctxt

219

218

220−{- lookup a name in the context, given an optional namespace.

219+{-| Look up a name in the context, given an optional namespace.

221 The name (n) may itself have a (partial) namespace given.

220 The name (n) may itself have a (partial) namespace given.

222

221

223 Rules for resolution:

222 Rules for resolution:

223+

224 - if an explicit namespace is given, return the names which match it. If none

225 match, return all names.

226+

226 - if the name has has explicit namespace given, return the names which match it

227 - if the name has has explicit namespace given, return the names which match it

227 and ignore the given namespace.

228 and ignore the given namespace.

229+

228 - otherwise, return all names.

230 - otherwise, return all names.

229

231

230-}

232-}

@@ -381,8 +383,9 @@ type RProgram = [(Name, RDef)]

381

383

382-- WELL TYPED TERMS ---------------------------------------------------------

384-- WELL TYPED TERMS ---------------------------------------------------------

383

385

386+-- | Universe expressions for universe checking

384−data UExp = UVar Int -- universe variable

387+data UExp = UVar Int -- ^ universe variable

385− | UVal Int -- explicit universe level

388+ | UVal Int -- ^ explicit universe level

386 deriving (Eq, Ord)

389 deriving (Eq, Ord)

387

390

388instance Sized UExp where

391instance Sized UExp where

@@ -402,8 +405,9 @@ instance Show UExp where

402 show (UVal x) = show x

405 show (UVal x) = show x

403-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"

406-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"

404

407

408+-- | Universe constraints

405−data UConstraint = ULT UExp UExp

409+data UConstraint = ULT UExp UExp -- ^ Strictly less than

406− | ULE UExp UExp

410+ | ULE UExp UExp -- ^ Less than or equal to

407 deriving Eq

411 deriving Eq

408

412

409instance Show UConstraint where

413instance Show UConstraint where

@@ -495,7 +499,7 @@ instance Eq n => Eq (TT n) where

495 (==) _ Erased = True

499 (==) _ Erased = True

496 (==) _ _ = False

500 (==) _ _ = False

497

501

498−-- A few handy operations on well typed terms:

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

499

503

500isInjective :: TT n -> Bool

504isInjective :: TT n -> Bool

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

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

@@ -506,7 +510,7 @@ isInjective (Bind _ (Pi _) sc) = True

506isInjective (App f a) = isInjective f

510isInjective (App f a) = isInjective f

507isInjective _ = False

511isInjective _ = False

508

512

509−-- Count the number of instances of a de Bruijn index in a term

513+-- | Count the number of instances of a de Bruijn index in a term

510vinstances :: Int -> TT n -> Int

514vinstances :: Int -> TT n -> Int

511vinstances i (V x) | i == x = 1

515vinstances i (V x) | i == x = 1

512vinstances i (App f a) = vinstances i f + vinstances i a

516vinstances i (App f a) = vinstances i f + vinstances i a

@@ -544,7 +548,7 @@ pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

544pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

548pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

545pToV' n i t = t

549pToV' n i t = t

546

550

547−-- Convert several names. First in the list comes out as V 0

551+-- | Convert several names. First in the list comes out as V 0

548pToVs :: Eq n => [n] -> TT n -> TT n

552pToVs :: Eq n => [n] -> TT n -> TT n

549pToVs ns tm = pToVs' ns tm 0 where

553pToVs ns tm = pToVs' ns tm 0 where

550 pToVs' [] tm i = tm

554 pToVs' [] tm i = tm

@@ -593,8 +597,7 @@ noOccurrence n t = no' 0 t

593 no' i (Proj x _) = no' i x

597 no' i (Proj x _) = no' i x

594 no' i _ = True

598 no' i _ = True

595

599

596−-- Returns all names used free in the term

600+-- | Returns all names used free in the term

597−

598freeNames :: Eq n => TT n -> [n]

601freeNames :: Eq n => TT n -> [n]

599freeNames (P _ n _) = [n]

602freeNames (P _ n _) = [n]

600freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])

603freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])

@@ -604,14 +607,12 @@ freeNames (App f a) = nub $ freeNames f ++ freeNames a

604freeNames (Proj x i) = nub $ freeNames x

607freeNames (Proj x i) = nub $ freeNames x

605freeNames _ = []

608freeNames _ = []

606

609

607−-- Return the arity of a (normalised) type

610+-- | Return the arity of a (normalised) type

608−

609arity :: TT n -> Int

611arity :: TT n -> Int

610arity (Bind n (Pi t) sc) = 1 + arity sc

612arity (Bind n (Pi t) sc) = 1 + arity sc

611arity _ = 0

613arity _ = 0

612

614

613−-- deconstruct an application; returns the function and a list of arguments

615+-- | Deconstruct an application; returns the function and a list of arguments

614−

615unApply :: TT n -> (TT n, [TT n])

616unApply :: TT n -> (TT n, [TT n])

616unApply t = ua [] t where

617unApply t = ua [] t where

617 ua args (App f a) = ua (a:args) f

618 ua args (App f a) = ua (a:args) f

@@ -794,8 +795,7 @@ showEnv' env t dbg = se 10 env t where

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

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

795 | otherwise = str

796 | otherwise = str

796

797

797−-- Check whether a term has any holes in it - impure if so

798+-- | Check whether a term has any holes in it - impure if so

798−

799pureTerm :: TT Name -> Bool

800pureTerm (App f a) = pureTerm f && pureTerm a

801pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

@@ -809,8 +809,7 @@ pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where

809

810pureTerm _ = True

811

812−-- weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)

812+-- | Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)

813−

814weakenTm :: Int -> TT n -> TT n

813weakenTm :: Int -> TT n -> TT n

815weakenTm i t = wk i 0 t

814weakenTm i t = wk i 0 t

816 where wk i min (V x) | x >= min = V (i + x)

815 where wk i min (V x) | x >= min = V (i + x)

@@ -819,7 +818,7 @@ weakenTm i t = wk i 0 t

819 wk i m t = t

818 wk i m t = t

820 wkb i m t = fmap (wk i m) t

819 wkb i m t = fmap (wk i m) t

821

820

822−-- weaken an environment so that all the de Bruijn indices are correct according

821+-- | Weaken an environment so that all the de Bruijn indices are correct according

823-- to the latest bound variable

822-- to the latest bound variable

824

823

825weakenEnv :: EnvTT n -> EnvTT n

824weakenEnv :: EnvTT n -> EnvTT n

src/Idris/AbsSyntaxTree.hs+45−34

@@ -46,10 +46,12 @@ defaultOpts = IOption 0 False False True False False True True ViaC Executable "

46-- This will include all the functions and data declarations, plus fixity declarations

47-- and syntax macros.

49+-- | The global state used in the Idris monad

49data IState = IState {

50data IState = IState {

50− tt_ctxt :: Context,

51+ tt_ctxt :: Context, -- ^ All the currently defined names and their terms

51 idris_constraints :: [(UConstraint, FC)],

52 idris_constraints :: [(UConstraint, FC)],

53+ -- ^ A list of universe constraints and their corresponding source locations

52− idris_infixes :: [FixDecl],

54+ idris_infixes :: [FixDecl], -- ^ Currently defined infix operators

53 idris_implicits :: Ctxt [PArg],

55 idris_implicits :: Ctxt [PArg],

54 idris_statics :: Ctxt [Bool],

56 idris_statics :: Ctxt [Bool],

55 idris_classes :: Ctxt ClassInfo,

57 idris_classes :: Ctxt ClassInfo,

@@ -65,11 +67,11 @@ data IState = IState {

65 idris_log :: String,

67 idris_log :: String,

66 idris_options :: IOption,

68 idris_options :: IOption,

67 idris_name :: Int,

69 idris_name :: Int,

68− idris_metavars :: [Name],

70+ idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables

69 idris_coercions :: [Name],

71 idris_coercions :: [Name],

70 syntax_rules :: [Syntax],

72 syntax_rules :: [Syntax],

71 syntax_keywords :: [String],

73 syntax_keywords :: [String],

72− imported :: [FilePath],

74+ imported :: [FilePath], -- ^ The imported modules

73 idris_scprims :: [(Name, (Int, PrimFn))],

75 idris_scprims :: [(Name, (Int, PrimFn))],

74 idris_objs :: [FilePath],

76 idris_objs :: [FilePath],

75 idris_libs :: [String],

77 idris_libs :: [String],

@@ -136,7 +138,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

136 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

138 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

137 [] Nothing Nothing [] [] [] Hidden False [] Nothing

139 [] Nothing Nothing [] [] [] Hidden False [] Nothing

138

140

139−-- The monad for the main REPL - reading and processing files and updating

141+-- | The monad for the main REPL - reading and processing files and updating

140-- global state (hence the IO inner monad).

142-- global state (hence the IO inner monad).

141type Idris = StateT IState IO

143type Idris = StateT IState IO

142

144

@@ -149,6 +151,7 @@ data Target = ViaC

149 | Bytecode

151 | Bytecode

150 deriving (Show, Eq)

152 deriving (Show, Eq)

151

153

154+-- | REPL commands

152data Command = Quit

155data Command = Quit

153 | Help

156 | Help

154 | Eval PTerm

157 | Eval PTerm

@@ -296,32 +299,37 @@ type FnOpts = [FnOpt]

296inlinable :: FnOpts -> Bool

299inlinable :: FnOpts -> Bool

297inlinable = elem Inlinable

300inlinable = elem Inlinable

298

301

302+-- | Top-level declarations such as compiler directives, definitions,

303+-- datatypes and typeclasses.

299−data PDecl' t

304+data PDecl' t

300− = PFix FC Fixity [String] -- fixity declaration

305+ = PFix FC Fixity [String] -- ^ Fixity declaration

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

306+ | PTy String SyntaxInfo FC FnOpts Name t -- ^ Type declaration

302− | PPostulate String SyntaxInfo FC FnOpts Name t

307+ | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

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

308+ | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

304− | PCAF FC Name t -- top level constant

309+ | PCAF FC Name t -- ^ Top level constant

305− | PData String SyntaxInfo FC Bool -- codata

310+ | PData String SyntaxInfo FC Bool (PData' t) -- ^ Data declaration. The Bool argument is True for codata.

306− (PData' t) -- data declaration

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

311+ | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

308− | PNamespace String [PDecl' t] -- new namespace

312+ | PNamespace String [PDecl' t] -- ^ New namespace

309− | PRecord String SyntaxInfo FC Name t String Name t -- record declaration

313+ | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

310 | PClass String SyntaxInfo FC

314 | PClass String SyntaxInfo FC

311 [t] -- constraints

315 [t] -- constraints

312 Name

316 Name

313 [(Name, t)] -- parameters

317 [(Name, t)] -- parameters

314 [PDecl' t] -- declarations

318 [PDecl' t] -- declarations

319+ -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

320+ -- class name, parameters, method declarations

315 | PInstance SyntaxInfo FC [t] -- constraints

321 | PInstance SyntaxInfo FC [t] -- constraints

316 Name -- class

322 Name -- class

317 [t] -- parameters

323 [t] -- parameters

318 t -- full instance type

324 t -- full instance type

319 (Maybe Name) -- explicit name

325 (Maybe Name) -- explicit name

320 [PDecl' t]

326 [PDecl' t]

327+ -- ^ Instance declaration: arguments are syntax info, source location, constraints,

328+ -- class name, parameters, full instance type, optional explicit name, and definitions

321− | PDSL Name (DSL' t)

329+ | PDSL Name (DSL' t) -- ^ DSL declaration

322− | PSyntax FC Syntax

330+ | PSyntax FC Syntax -- ^ Syntax definition

323− | PMutual FC [PDecl' t]

331+ | PMutual FC [PDecl' t] -- ^ Mutual block

324− | PDirective (Idris ())

332+ | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

325 deriving Functor

333 deriving Functor

326{-!

334{-!

327deriving instance Binary PDecl'

335deriving instance Binary PDecl'

@@ -336,10 +344,14 @@ data PClause' t = PClause FC Name t [t] t [PDecl' t]

336deriving instance Binary PClause'

344deriving instance Binary PClause'

337!-}

345!-}

338

346

347+-- | Data declaration

339−data PData' t = PDatadecl { d_name :: Name,

348+data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

340− d_tcon :: t,

349+ d_tcon :: t, -- ^ Type constructor

341− d_cons :: [(String, Name, t, FC)] }

350+ d_cons :: [(String, Name, t, FC)] -- ^ Constructors

351+ }

352+ -- ^ Data declaration

342 | PLaterdecl { d_name :: Name, d_tcon :: t }

353 | PLaterdecl { d_name :: Name, d_tcon :: t }

354+ -- ^ "Placeholder" for data whose constructors are defined later

343 deriving Functor

355 deriving Functor

344{-!

356{-!

345deriving instance Binary PData'

357deriving instance Binary PData'

@@ -414,16 +426,15 @@ updateNs ns t = mapPT updateRef t

414-- (map (updateDNs ns) ds)

426-- (map (updateDNs ns) ds)

415-- updateDNs ns c = c

427-- updateDNs ns c = c

416

428

417−-- High level language terms

429+-- | High level language terms

418−

419data PTerm = PQuote Raw

430data PTerm = PQuote Raw

420 | PRef FC Name

431 | PRef FC Name

421− | PInferRef FC Name -- a name to be defined later

432+ | PInferRef FC Name -- ^ A name to be defined later

422 | PPatvar FC Name

433 | PPatvar FC Name

423 | PLam Name PTerm PTerm

434 | PLam Name PTerm PTerm

424 | PPi Plicity Name PTerm PTerm

435 | PPi Plicity Name PTerm PTerm

425− | PLet Name PTerm PTerm PTerm

436+ | PLet Name PTerm PTerm PTerm

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

437+ | PTyped PTerm PTerm -- ^ Term with explicit type

427 | PApp FC PTerm [PArg]

438 | PApp FC PTerm [PArg]

428 | PCase FC PTerm [(PTerm, PTerm)]

439 | PCase FC PTerm [(PTerm, PTerm)]

429 | PTrue FC

440 | PTrue FC

@@ -434,7 +445,7 @@ data PTerm = PQuote Raw

434 | PPair FC PTerm PTerm

445 | PPair FC PTerm PTerm

435 | PDPair FC PTerm PTerm PTerm

446 | PDPair FC PTerm PTerm PTerm

436 | PAlternative Bool [PTerm] -- True if only one may work

447 | PAlternative Bool [PTerm] -- True if only one may work

437− | PHidden PTerm -- irrelevant or hidden pattern

448+ | PHidden PTerm -- ^ Irrelevant or hidden pattern

438 | PType

449 | PType

439 | PConstant Const

450 | PConstant Const

440 | Placeholder

451 | Placeholder

@@ -442,11 +453,11 @@ data PTerm = PQuote Raw

442 | PIdiom FC PTerm

453 | PIdiom FC PTerm

443 | PReturn FC

454 | PReturn FC

444 | PMetavar Name

455 | PMetavar Name

445− | PProof [PTactic]

456+ | PProof [PTactic] -- ^ Proof script

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

457+ | PTactics [PTactic] -- ^ As PProof, but no auto solving

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

458+ | PElabError Err -- ^ Error to report on elaboration

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

459+ | PImpossible -- ^ Special case for declaring when an LHS can't typecheck

449− | PCoerced PTerm -- to mark a coerced argument, so as not to coerce twice

460+ | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

450 deriving Eq

461 deriving Eq

451{-!

462{-!

452deriving instance Binary PTerm

463deriving instance Binary PTerm

src/Idris/Completion.hs+5−2

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

1+-- | Support for command-line completion at the REPL and in the prover

1module Idris.Completion (replCompletion, proverCompletion) where

2module Idris.Completion (replCompletion, proverCompletion) where

3import Core.Evaluate (ctxtAlist)

4import Core.Evaluate (ctxtAlist)

@@ -122,6 +123,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo

122 completeArg ExprArg = completeExpr [] (prev, next)

123 completeArg ExprArg = completeExpr [] (prev, next)

123 completeCmdName = return $ ("", completeWith commands cmd)

124 completeCmdName = return $ ("", completeWith commands cmd)

124

125

126+-- | Complete REPL commands and defined identifiers

125replCompletion :: CompletionFunc Idris

127replCompletion :: CompletionFunc Idris

126replCompletion (prev, next) = case firstWord of

128replCompletion (prev, next) = case firstWord of

127 ':':cmdName -> completeCmd (':':cmdName) (prev, next)

129 ':':cmdName -> completeCmd (':':cmdName) (prev, next)

@@ -137,7 +139,8 @@ completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeAr

137 completeArg (Just ExprTArg) = completeExpr as (prev, next)

139 completeArg (Just ExprTArg) = completeExpr as (prev, next)

138 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO

140 completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO

139

141

140−

142+-- | Complete tactics and their arguments

143+proverCompletion :: [String] -- ^ The names of current local assumptions

141−proverCompletion :: [String] -> CompletionFunc Idris

144+ -> CompletionFunc Idris

142proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)

145proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)

143 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev

146 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev

src/Idris/REPL.hs+6−1

@@ -50,7 +50,10 @@ import Data.List

50import Data.Char

51import Data.Version

53+-- | Run the REPL

54+repl :: IState -- ^ The initial state

55+ -> [FilePath] -- ^ The loaded modules

53−repl :: IState -> [FilePath] -> InputT Idris ()

56+ -> InputT Idris ()

54repl orig mods

57repl orig mods

55 = H.catch

58 = H.catch

56 (do let prompt = mkPrompt mods

59 (do let prompt = mkPrompt mods

@@ -69,10 +72,12 @@ repl orig mods

69 ctrlC e = do lift $ iputStrLn (show e)

72 ctrlC e = do lift $ iputStrLn (show e)

70 repl orig mods

73 repl orig mods

75+-- | The prompt consists of the currently loaded modules, or "Idris" if there are none

72mkPrompt [] = "Idris"

76mkPrompt [] = "Idris"

73mkPrompt [x] = "*" ++ dropExtension x

77mkPrompt [x] = "*" ++ dropExtension x

74mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

78mkPrompt (x:xs) = "*" ++ dropExtension x ++ " " ++ mkPrompt xs

80+-- | Determine whether a file uses literate syntax

76lit f = case splitExtension f of

81lit f = case splitExtension f of

77 (_, ".lidr") -> True

82 (_, ".lidr") -> True

78 _ -> False

83 _ -> False