@@ -46,10 +46,12 @@ defaultOpts = IOption 0 False False True False False True True ViaC Executable "
4646-- This will include all the functions and data declarations, plus fixity declarations
4747-- and syntax macros.
4848
49+-- | The global state used in the Idris monad
4950data IState = IState {
50− tt_ctxt :: Context,
51+ tt_ctxt :: Context, -- ^ All the currently defined names and their terms
5152 idris_constraints :: [(UConstraint, FC)],
52− idris_infixes :: [FixDecl],
53+ -- ^ A list of universe constraints and their corresponding source locations
54+ idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
5355 idris_implicits :: Ctxt [PArg],
5456 idris_statics :: Ctxt [Bool],
5557 idris_classes :: Ctxt ClassInfo,
@@ -65,11 +67,11 @@ data IState = IState {
6567 idris_log :: String,
6668 idris_options :: IOption,
6769 idris_name :: Int,
68− idris_metavars :: [Name],
70+ idris_metavars :: [Name], -- ^ The currently defined but not proven metavariables
6971 idris_coercions :: [Name],
7072 syntax_rules :: [Syntax],
7173 syntax_keywords :: [String],
72− imported :: [FilePath],
74+ imported :: [FilePath], -- ^ The imported modules
7375 idris_scprims :: [(Name, (Int, PrimFn))],
7476 idris_objs :: [FilePath],
7577 idris_libs :: [String],
@@ -136,7 +138,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
136138 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
137139 [] Nothing Nothing [] [] [] Hidden False [] Nothing
138140
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
140142-- global state (hence the IO inner monad).
141143type Idris = StateT IState IO
142144
@@ -149,6 +151,7 @@ data Target = ViaC
149151 | Bytecode
150152 deriving (Show, Eq)
151153
154+-- | REPL commands
152155data Command = Quit
153156 | Help
154157 | Eval PTerm
@@ -296,32 +299,37 @@ type FnOpts = [FnOpt]
296299inlinable :: FnOpts -> Bool
297300inlinable = elem Inlinable
298301
299−data PDecl' t
300− = PFix FC Fixity [String] -- fixity declaration
301− | PTy String SyntaxInfo FC FnOpts Name t -- type declaration
302− | PPostulate String SyntaxInfo FC FnOpts Name t
303− | PClauses FC FnOpts Name [PClause' t] -- pattern clause
304− | PCAF FC Name t -- top level constant
305− | PData String SyntaxInfo FC Bool -- codata
306− (PData' t) -- data declaration
307− | PParams FC [(Name, t)] [PDecl' t] -- params block
308− | PNamespace String [PDecl' t] -- new namespace
309− | PRecord String SyntaxInfo FC Name t String Name t -- record declaration
302+-- | Top-level declarations such as compiler directives, definitions,
303+-- datatypes and typeclasses.
304+data PDecl' t
305+ = PFix FC Fixity [String] -- ^ Fixity declaration
306+ | PTy String SyntaxInfo FC FnOpts Name t -- ^ Type declaration
307+ | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
308+ | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
309+ | PCAF FC Name t -- ^ Top level constant
310+ | PData String SyntaxInfo FC Bool (PData' t) -- ^ Data declaration. The Bool argument is True for codata.
311+ | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
312+ | PNamespace String [PDecl' t] -- ^ New namespace
313+ | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
310314 | PClass String SyntaxInfo FC
311315 [t] -- constraints
312316 Name
313317 [(Name, t)] -- parameters
314318 [PDecl' t] -- declarations
319+ -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
320+ -- class name, parameters, method declarations
315321 | PInstance SyntaxInfo FC [t] -- constraints
316322 Name -- class
317323 [t] -- parameters
318324 t -- full instance type
319325 (Maybe Name) -- explicit name
320326 [PDecl' t]
321− | PDSL Name (DSL' t)
322− | PSyntax FC Syntax
323− | PMutual FC [PDecl' t]
324− | PDirective (Idris ())
327+ -- ^ Instance declaration: arguments are syntax info, source location, constraints,
328+ -- class name, parameters, full instance type, optional explicit name, and definitions
329+ | PDSL Name (DSL' t) -- ^ DSL declaration
330+ | PSyntax FC Syntax -- ^ Syntax definition
331+ | PMutual FC [PDecl' t] -- ^ Mutual block
332+ | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
325333 deriving Functor
326334{-!
327335deriving instance Binary PDecl'
@@ -336,10 +344,14 @@ data PClause' t = PClause FC Name t [t] t [PDecl' t]
336344deriving instance Binary PClause'
337345!-}
338346
339−data PData' t = PDatadecl { d_name :: Name,
340− d_tcon :: t,
341− d_cons :: [(String, Name, t, FC)] }
347+-- | Data declaration
348+data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
349+ d_tcon :: t, -- ^ Type constructor
350+ d_cons :: [(String, Name, t, FC)] -- ^ Constructors
351+ }
352+ -- ^ Data declaration
342353 | PLaterdecl { d_name :: Name, d_tcon :: t }
354+ -- ^ "Placeholder" for data whose constructors are defined later
343355 deriving Functor
344356{-!
345357deriving instance Binary PData'
@@ -414,16 +426,15 @@ updateNs ns t = mapPT updateRef t
414426-- (map (updateDNs ns) ds)
415427-- updateDNs ns c = c
416428
417−-- High level language terms
418−
429+-- | High level language terms
419430data PTerm = PQuote Raw
420431 | PRef FC Name
421− | PInferRef FC Name -- a name to be defined later
432+ | PInferRef FC Name -- ^ A name to be defined later
422433 | PPatvar FC Name
423434 | PLam Name PTerm PTerm
424435 | PPi Plicity Name PTerm PTerm
425− | PLet Name PTerm PTerm PTerm
426− | PTyped PTerm PTerm -- term with explicit type
436+ | PLet Name PTerm PTerm PTerm
437+ | PTyped PTerm PTerm -- ^ Term with explicit type
427438 | PApp FC PTerm [PArg]
428439 | PCase FC PTerm [(PTerm, PTerm)]
429440 | PTrue FC
@@ -434,7 +445,7 @@ data PTerm = PQuote Raw
434445 | PPair FC PTerm PTerm
435446 | PDPair FC PTerm PTerm PTerm
436447 | PAlternative Bool [PTerm] -- True if only one may work
437− | PHidden PTerm -- irrelevant or hidden pattern
448+ | PHidden PTerm -- ^ Irrelevant or hidden pattern
438449 | PType
439450 | PConstant Const
440451 | Placeholder
@@ -442,11 +453,11 @@ data PTerm = PQuote Raw
442453 | PIdiom FC PTerm
443454 | PReturn FC
444455 | PMetavar Name
445− | PProof [PTactic]
446− | PTactics [PTactic] -- as PProof, but no auto solving
447− | PElabError Err -- error to report on elaboration
448− | 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
456+ | PProof [PTactic] -- ^ Proof script
457+ | PTactics [PTactic] -- ^ As PProof, but no auto solving
458+ | PElabError Err -- ^ Error to report on elaboration
459+ | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
460+ | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
450461 deriving Eq
451462{-!
452463deriving instance Binary PTerm