@@ -48,23 +48,24 @@ import Text.PrettyPrint.Annotated.Leijen
4848data ElabWhat = ETypes | EDefns | EAll
4949 deriving (Show, Eq)
5050
51−-- Data to pass to recursively called elaborators; e.g. for where blocks,
51+-- | Data to pass to recursively called elaborators; e.g. for where blocks,
5252-- paramaterised declarations, etc.
53−
53+--
5454-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
5555-- so that we can have mutually recursive elaborators in separate modules without
5656-- having to muck about with cyclic modules.
57−data ElabInfo = EInfo { params :: [(Name, PTerm)],
58− inblock :: Ctxt [Name], -- names in the block, and their params
59− liftname :: Name -> Name,
60− namespace :: Maybe [String],
61− elabFC :: Maybe FC,
62− -- We may, recursively, collect transformations to
63− -- do on the rhs, e.g. rewriting recursive calls to
64− -- functions defined by 'with'
65− rhs_trans :: PTerm -> PTerm,
66− rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
67− Idris () }
57+data ElabInfo = EInfo {
58+ params :: [(Name, PTerm)]
59+ , inblock :: Ctxt [Name] -- ^ names in the block, and their params
60+ , liftname :: Name -> Name
61+ , namespace :: Maybe [String]
62+ , elabFC :: Maybe FC
63+
64+ -- | We may, recursively, collect transformations to do on the rhs,
65+ -- e.g. rewriting recursive calls to functions defined by 'with'
66+ , rhs_trans :: PTerm -> PTerm
67+ , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
68+ }
6869
6970toplevel :: ElabInfo
7071toplevel = EInfo [] emptyContext id Nothing Nothing id (\_ _ _ -> fail "Not implemented")
@@ -90,13 +91,13 @@ data IOption = IOption {
9091 , opt_importdirs :: [FilePath]
9192 , opt_triple :: String
9293 , opt_cpu :: String
93− , opt_cmdline :: [Opt] -- remember whole command line
94+ , opt_cmdline :: [Opt] -- ^ remember whole command line
9495 , opt_origerr :: Bool
9596 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
96− , opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude
97+ , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
9798 , opt_optimise :: [Optimisation]
9899 , opt_printdepth :: Maybe Int
99− , opt_evaltypes :: Bool -- ^ normalise types in :t
100+ , opt_evaltypes :: Bool -- ^ normalise types in `:t`
100101 , opt_desugarnats :: Bool
101102 , opt_autoimpls :: Bool
102103 } deriving (Show, Eq)
@@ -130,39 +131,43 @@ defaultOpts = IOption { opt_logLevel = 0
130131 }
131132
132133data PPOption = PPOption {
133− ppopt_impl :: Bool -- ^^ whether to show implicits
134+ ppopt_impl :: Bool -- ^ whether to show implicits
134135 , ppopt_desugarnats :: Bool
135− , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings
136− , ppopt_depth :: Maybe Int
137−} deriving (Show)
136+ , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
137+ , ppopt_depth :: Maybe Int
138+ } deriving (Show)
138139
139−data Optimisation = PETransform -- partial eval and associated transforms
140+data Optimisation = PETransform -- ^ partial eval and associated transforms
140141 deriving (Show, Eq)
141142
142143defaultOptimise = [PETransform]
143144
144145-- | Pretty printing options with default verbosity.
145146defaultPPOption :: PPOption
146−defaultPPOption = PPOption { ppopt_impl = False,
147− ppopt_desugarnats = False,
148− ppopt_pinames = False,
149− ppopt_depth = Just 200 }
147+defaultPPOption = PPOption {
148+ ppopt_impl = False
149+ , ppopt_desugarnats = False
150+ , ppopt_pinames = False
151+ , ppopt_depth = Just 200
152+ }
150153
151154-- | Pretty printing options with the most verbosity.
152155verbosePPOption :: PPOption
153−verbosePPOption = PPOption { ppopt_impl = True,
154− ppopt_desugarnats = True,
155− ppopt_pinames = True,
156− ppopt_depth = Just 200 }
156+verbosePPOption = PPOption {
157+ ppopt_impl = True
158+ , ppopt_desugarnats = True
159+ , ppopt_pinames = True
160+ , ppopt_depth = Just 200
161+ }
157162
158163-- | Get pretty printing options from the big options record.
159164ppOption :: IOption -> PPOption
160165ppOption opt = PPOption {
161− ppopt_impl = opt_showimp opt,
162− ppopt_pinames = False,
163− ppopt_depth = opt_printdepth opt,
164− ppopt_desugarnats = opt_desugarnats opt
165−}
166+ ppopt_impl = opt_showimp opt
167+ , ppopt_pinames = False
168+ , ppopt_depth = opt_printdepth opt
169+ , ppopt_desugarnats = opt_desugarnats opt
170+ }
166171
167172-- | Get pretty printing options from an idris state record.
168173ppOptionIst :: IState -> PPOption
@@ -171,13 +176,13 @@ ppOptionIst = ppOption . idris_options
171176data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
172177
173178-- | The output mode in use
174−data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
179+data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
175180 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
176181 deriving Show
177182
178183-- | How wide is the console?
179184data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
180− | ColsWide Int -- ^ Manually specified - must be positive
185+ | ColsWide Int -- ^ Manually specified - must be positive
181186 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
182187 deriving (Show, Eq)
183188
@@ -189,97 +194,105 @@ data DefaultTotality = DefaultCheckingTotal -- ^ Total
189194
190195-- | The global state used in the Idris monad
191196data IState = IState {
192− tt_ctxt :: Context, -- ^ All the currently defined names and their terms
193− idris_constraints :: S.Set ConstraintFC,
194− -- ^ A list of universe constraints and their corresponding source locations
195− idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
196− idris_implicits :: Ctxt [PArg],
197− idris_statics :: Ctxt [Bool],
198− idris_classes :: Ctxt ClassInfo,
199− idris_openimpls :: [Name], -- ^ Privileged implementations, will resolve immediately
200− idris_records :: Ctxt RecordInfo,
201− idris_dsls :: Ctxt DSL,
202− idris_optimisation :: Ctxt OptInfo,
203− idris_datatypes :: Ctxt TypeInfo,
204− idris_namehints :: Ctxt [Name],
205− idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported
206− -- ^ list of lhs/rhs, and a list of missing clauses
207− idris_flags :: Ctxt [FnOpt],
208− idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
209− idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
210− idris_moduledocs :: Ctxt (Docstring DocTerm),
211− -- ^ module documentation is saved in a special MN so the context
212− -- mechanism can be used for disambiguation
213− idris_tyinfodata :: Ctxt TIData,
214− idris_fninfo :: Ctxt FnInfo,
215− idris_transforms :: Ctxt [(Term, Term)],
216− idris_autohints :: Ctxt [Name],
217− idris_totcheck :: [(FC, Name)], -- names to check totality on
218− idris_defertotcheck :: [(FC, Name)], -- names to check at the end
219− idris_totcheckfail :: [(FC, String)],
220− idris_options :: IOption,
221− idris_name :: Int,
222− idris_lineapps :: [((FilePath, Int), PTerm)],
223− -- ^ Full application LHS on source line
224− idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))],
225− -- ^ The currently defined but not proven metavariables. The Int
226− -- is the number of vars to display as a context, the Maybe Name
227− -- is its top-level function, the [Name] is the list of local variables
228− -- available for proof search and the Bools are whether :p is
229− -- allowed, and whether the variable is definable at all
230− -- (Metavariables are not definable if they are applied in a term which
231− -- still has hole bindings)
232− idris_coercions :: [Name],
233− idris_errRev :: [(Term, Term)],
234− syntax_rules :: SyntaxRules,
235− syntax_keywords :: [String],
236− imported :: [FilePath], -- ^ The imported modules
237− idris_scprims :: [(Name, (Int, PrimFn))],
238− idris_objs :: [(Codegen, FilePath)],
239− idris_libs :: [(Codegen, String)],
240− idris_cgflags :: [(Codegen, String)],
241− idris_hdrs :: [(Codegen, String)],
242− idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
243− proof_list :: [(Name, (Bool, [String]))],
244− errSpan :: Maybe FC,
245− parserWarnings :: [(FC, Err)],
246− lastParse :: Maybe Name,
247− indent_stack :: [Int],
248− brace_stack :: [Maybe Int],
249− lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
250− idris_parsedSpan :: Maybe FC,
251− hide_list :: Ctxt Accessibility,
252− default_access :: Accessibility,
253− default_total :: DefaultTotality,
254− ibc_write :: [IBCWrite],
255− compiled_so :: Maybe String,
256− idris_dynamic_libs :: [DynamicLib],
257− idris_language_extensions :: [LanguageExt],
258− idris_outputmode :: OutputMode,
259− idris_colourRepl :: Bool,
260− idris_colourTheme :: ColourTheme,
261− idris_errorhandlers :: [Name], -- ^ Global error handlers
262− idris_nameIdx :: (Int, Ctxt (Int, Name)),
263− idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
264− module_aliases :: M.Map [T.Text] [T.Text],
265− idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
266− idris_postulates :: S.Set Name,
267− idris_externs :: S.Set (Name, Int),
268− idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
269− idris_whocalls :: Maybe (M.Map Name [Name]),
270− idris_callswho :: Maybe (M.Map Name [Name]),
271− idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
272− elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
273− -- (instances appear twice; also as a funtion name)
274− idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
275− idris_exports :: [Name], -- ^ Functions with ExportList
276− idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
277− idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser
278− idris_deprecated :: Ctxt String, -- ^ Deprecated names and explanation
279− idris_inmodule :: S.Set Name, -- ^ Names defined in current module
280− idris_ttstats :: M.Map Term (Int, Term),
281− idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
282− }
197+ tt_ctxt :: Context -- ^ All the currently defined names and their terms
198+ , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
199+ , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
200+ , idris_implicits :: Ctxt [PArg]
201+ , idris_statics :: Ctxt [Bool]
202+ , idris_classes :: Ctxt ClassInfo
203+ , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
204+ , idris_records :: Ctxt RecordInfo
205+ , idris_dsls :: Ctxt DSL
206+ , idris_optimisation :: Ctxt OptInfo
207+ , idris_datatypes :: Ctxt TypeInfo
208+ , idris_namehints :: Ctxt [Name]
209+
210+ -- | list of lhs/rhs, and a list of missing clauses. These are not
211+ -- exported.
212+ , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
213+ , idris_flags :: Ctxt [FnOpt]
214+ , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
215+ , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
216+
217+ -- | module documentation is saved in a special MN so the context
218+ -- mechanism can be used for disambiguation.
219+ , idris_moduledocs :: Ctxt (Docstring DocTerm)
220+ , idris_tyinfodata :: Ctxt TIData
221+ , idris_fninfo :: Ctxt FnInfo
222+ , idris_transforms :: Ctxt [(Term, Term)]
223+ , idris_autohints :: Ctxt [Name]
224+ , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
225+ , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
226+ , idris_totcheckfail :: [(FC, String)]
227+ , idris_options :: IOption
228+ , idris_name :: Int
229+ , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
230+
231+ -- | The currently defined but not proven metavariables. The Int is
232+ -- the number of vars to display as a context, the Maybe Name is its
233+ -- top-level function, the [Name] is the list of local variables
234+ -- available for proof search and the Bools are whether :p is
235+ -- allowed, and whether the variable is definable at all
236+ -- (Metavariables are not definable if they are applied in a term
237+ -- which still has hole bindings)
238+ , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
239+ , idris_coercions :: [Name]
240+ , idris_errRev :: [(Term, Term)]
241+ , syntax_rules :: SyntaxRules
242+ , syntax_keywords :: [String]
243+ , imported :: [FilePath] -- ^ The imported modules
244+ , idris_scprims :: [(Name, (Int, PrimFn))]
245+ , idris_objs :: [(Codegen, FilePath)]
246+ , idris_libs :: [(Codegen, String)]
247+ , idris_cgflags :: [(Codegen, String)]
248+ , idris_hdrs :: [(Codegen, String)]
249+ , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
250+ , proof_list :: [(Name, (Bool, [String]))]
251+ , errSpan :: Maybe FC
252+ , parserWarnings :: [(FC, Err)]
253+ , lastParse :: Maybe Name
254+ , indent_stack :: [Int]
255+ , brace_stack :: [Maybe Int]
256+ , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
257+ , idris_parsedSpan :: Maybe FC
258+ , hide_list :: Ctxt Accessibility
259+ , default_access :: Accessibility
260+ , default_total :: DefaultTotality
261+ , ibc_write :: [IBCWrite]
262+ , compiled_so :: Maybe String
263+ , idris_dynamic_libs :: [DynamicLib]
264+ , idris_language_extensions :: [LanguageExt]
265+ , idris_outputmode :: OutputMode
266+ , idris_colourRepl :: Bool
267+ , idris_colourTheme :: ColourTheme
268+ , idris_errorhandlers :: [Name] -- ^ Global error handlers
269+ , idris_nameIdx :: (Int, Ctxt (Int, Name))
270+ , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
271+ , module_aliases :: M.Map [T.Text] [T.Text]
272+ , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
273+ , idris_postulates :: S.Set Name
274+ , idris_externs :: S.Set (Name, Int)
275+ , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
276+ , idris_whocalls :: Maybe (M.Map Name [Name])
277+ , idris_callswho :: Maybe (M.Map Name [Name])
278+
279+ -- | List of names that were defined in the repl, and can be re-/un-defined
280+ , idris_repl_defs :: [Name]
281+
282+ -- | Stack of names currently being elaborated, Bool set if it's an
283+ -- instance (instances appear twice; also as a funtion name)
284+ , elab_stack :: [(Name, Bool)]
285+
286+
287+ , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
288+ , idris_exports :: [Name] -- ^ Functions with ExportList
289+ , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
290+ , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
291+ , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
292+ , idris_inmodule :: S.Set Name -- ^ Names defined in current module
293+ , idris_ttstats :: M.Map Term (Int, Term)
294+ , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
295+ }
283296
284297-- Required for parsers library, and therefore trifecta
285298instance Show IState where
@@ -295,20 +308,21 @@ deriving instance NFData SizeChange
295308type SCGEntry = (Name, [Maybe (Int, SizeChange)])
296309type UsageReason = (Name, Int) -- fn_name, its_arg_number
297310
298−data CGInfo = CGInfo { calls :: [Name],
299− scg :: [SCGEntry],
300− usedpos :: [(Int, [UsageReason])]
301− }
302− deriving Show
311+data CGInfo = CGInfo {
312+ calls :: [Name]
313+ , scg :: [SCGEntry]
314+ , usedpos :: [(Int, [UsageReason])]
315+ } deriving Show
303316{-!
304317deriving instance Binary CGInfo
305318deriving instance NFData CGInfo
306319!-}
307320
308−primDefs = [sUN "unsafePerformPrimIO",
309− sUN "mkLazyForeignPrim",
310− sUN "mkForeignPrim",
311− sUN "void"]
321+primDefs = [ sUN "unsafePerformPrimIO"
322+ , sUN "mkLazyForeignPrim"
323+ , sUN "mkForeignPrim"
324+ , sUN "void"
325+ ]
312326
313327-- information that needs writing for the current module's .ibc file
314328data IBCWrite = IBCFix FixDecl
@@ -323,7 +337,7 @@ data IBCWrite = IBCFix FixDecl
323337 | IBCMetavar Name
324338 | IBCSyntax Syntax
325339 | IBCKeyword String
326− | IBCImport (Bool, FilePath) -- True = import public
340+ | IBCImport (Bool, FilePath) -- ^ True = import public
327341 | IBCImportDir FilePath
328342 | IBCObj Codegen FilePath
329343 | IBCLib Codegen String
@@ -341,7 +355,7 @@ data IBCWrite = IBCFix FixDecl
341355 | IBCCG Name
342356 | IBCDoc Name
343357 | IBCCoercion Name
344− | IBCDef Name -- i.e. main context
358+ | IBCDef Name -- ^ The main context.
345359 | IBCNameHint (Name, Name)
346360 | IBCLineApp FilePath Int PTerm
347361 | IBCErrorHandler Name
@@ -373,9 +387,13 @@ idrisInit = IState initContext S.empty []
373387 emptyContext S.empty M.empty emptyContext
374388
375389
376−-- | The monad for the main REPL - reading and processing files and updating
377−-- global state (hence the IO inner monad).
378−--type Idris = WriterT [Either String (IO ())] (State IState a))
390+-- | The monad for the main REPL - reading and processing files and
391+-- updating global state (hence the IO inner monad).
392+--
393+-- @
394+-- type Idris = WriterT [Either String (IO ())] (State IState a))
395+-- @
396+--
379397type Idris = StateT IState (ExceptT Err IO)
380398
381399catchError :: Idris a -> (Err -> Idris a) -> Idris a
@@ -441,10 +459,10 @@ data Command = Quit
441459 | MakeWith Bool Int Name
442460 | MakeCase Bool Int Name
443461 | MakeLemma Bool Int Name
444− | DoProofSearch Bool -- update file
445− Bool -- recursive search
446− Int -- depth
447− Name -- top level name
462+ | DoProofSearch Bool -- update file
463+ Bool -- recursive search
464+ Int -- depth
465+ Name -- top level name
448466 [Name] -- hints
449467 | SetOpt Opt
450468 | UnsetOpt Opt
@@ -459,7 +477,7 @@ data Command = Quit
459477 | WhoCalls Name
460478 | CallsWho Name
461479 | Browse [String]
462− | MakeDoc String -- IdrisDoc
480+ | MakeDoc String -- IdrisDoc
463481 | Warranty
464482 | PrintDef Name
465483 | PPrint OutputFmt Int PTerm
@@ -538,7 +556,7 @@ data Opt = Filename String
538556 | ErrContext
539557 | ShowImpl
540558 | Verbose
541− | Port String -- REPL TCP port
559+ | Port String -- ^ REPL TCP port
542560 | IBCSubDir String
543561 | ImportDir String
544562 | PkgBuild String
@@ -546,7 +564,7 @@ data Opt = Filename String
546564 | PkgClean String
547565 | PkgCheck String
548566 | PkgREPL String
549− | PkgMkDoc String -- IdrisDoc
567+ | PkgMkDoc String -- IdrisDoc
550568 | PkgTest String
551569 | PkgIndex FilePath
552570 | WarnOnly
@@ -572,20 +590,26 @@ data Opt = Filename String
572590 | UseConsoleWidth ConsoleWidth
573591 | DumpHighlights
574592 | DesugarNats
575− | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
593+ | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
576594 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
577595 deriving (Show, Eq)
578596
579−data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
580− | EEval PTerm | ECheck PTerm | ESearch PTerm
597+data ElabShellCmd = EQED
598+ | EAbandon
599+ | EUndo
600+ | EProofState
601+ | EProofTerm
602+ | EEval PTerm
603+ | ECheck PTerm
604+ | ESearch PTerm
581605 | EDocStr (Either Name Const)
582606 deriving (Show, Eq)
583607
584608-- Parsed declarations
585609
586−data Fixity = Infixl { prec :: Int }
587− | Infixr { prec :: Int }
588− | InfixN { prec :: Int }
610+data Fixity = Infixl { prec :: Int }
611+ | Infixr { prec :: Int }
612+ | InfixN { prec :: Int }
589613 | PrefixN { prec :: Int }
590614 deriving Eq
591615{-!
@@ -594,9 +618,9 @@ deriving instance NFData Fixity
594618!-}
595619
596620instance Show Fixity where
597− show (Infixl i) = "infixl " ++ show i
598− show (Infixr i) = "infixr " ++ show i
599− show (InfixN i) = "infix " ++ show i
621+ show (Infixl i) = "infixl " ++ show i
622+ show (Infixr i) = "infixr " ++ show i
623+ show (InfixN i) = "infix " ++ show i
600624 show (PrefixN i) = "prefix " ++ show i
601625
602626data FixDecl = Fix Fixity String
@@ -621,22 +645,25 @@ deriving instance Binary Static
621645deriving instance NFData Static
622646!-}
623647
624−-- Mark bindings with their explicitness, and laziness
625−data Plicity = Imp { pargopts :: [ArgOpt],
626− pstatic :: Static,
627− pparam :: Bool,
628− pscoped :: Maybe ImplicitInfo, -- Nothing, if top level
629− pinsource :: Bool -- Explicitly written in source
648+-- ^ Mark bindings with their explicitness, and laziness
649+data Plicity = Imp { pargopts :: [ArgOpt]
650+ , pstatic :: Static
651+ , pparam :: Bool
652+ , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
653+ , pinsource :: Bool -- ^ Explicitly written in source
630654 }
631− | Exp { pargopts :: [ArgOpt],
632− pstatic :: Static,
633− pparam :: Bool } -- this is a param (rather than index)
634− | Constraint { pargopts :: [ArgOpt],
635− pstatic :: Static }
636− | TacImp { pargopts :: [ArgOpt],
637− pstatic :: Static,
638− pscript :: PTerm }
639− deriving (Show, Eq, Data, Typeable)
655+ | Exp { pargopts :: [ArgOpt]
656+ , pstatic :: Static
657+ , pparam :: Bool -- ^ this is a param (rather than index)
658+ }
659+ | Constraint { pargopts :: [ArgOpt]
660+ , pstatic :: Static
661+ }
662+ | TacImp { pargopts :: [ArgOpt]
663+ , pstatic :: Static
664+ , pscript :: PTerm
665+ }
666+ deriving (Show, Eq, Data, Typeable)
640667
641668{-!
642669deriving instance Binary Plicity
@@ -645,7 +672,7 @@ deriving instance NFData Plicity
645672
646673is_scoped :: Plicity -> Maybe ImplicitInfo
647674is_scoped (Imp _ _ _ s _) = s
648−is_scoped _ = Nothing
675+is_scoped _ = Nothing
649676
650677impl = Imp [] Dynamic False (Just (Impl False True)) False
651678
@@ -659,21 +686,23 @@ constraint = Constraint [] Static
659686
660687tacimpl t = TacImp [] Dynamic t
661688
662−data FnOpt = Inlinable -- always evaluate when simplifying
689+data FnOpt = Inlinable -- ^ always evaluate when simplifying
663690 | TotalFn | PartialFn | CoveringFn
664691 | Coinductive | AssertTotal
665− | Dictionary -- type class dictionary, eval only when
666− -- a function argument, and further evaluation resutls
667− | Implicit -- implicit coercion
668− | NoImplicit -- do not apply implicit coercions
669− | CExport String -- export, with a C name
670− | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
671− | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
672− | Reflection -- a reflecting function, compile-time only
673− | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
674− | Constructor -- Data constructor type
675− | AutoHint -- use in auto implicit search
676− | PEGenerated -- generated by partial evaluator
692+
693+ -- | type class dictionary, eval only when a function
694+ -- argument, and further evaluation results.
695+ | Dictionary
696+ | Implicit -- ^ implicit coercion
697+ | NoImplicit -- ^ do not apply implicit coercions
698+ | CExport String -- ^ export, with a C name
699+ | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
700+ | ErrorReverse -- ^ attempt to reverse normalise before showing in error
701+ | Reflection -- ^ a reflecting function, compile-time only
702+ | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
703+ | Constructor -- ^ Data constructor type
704+ | AutoHint -- ^ use in auto implicit search
705+ | PEGenerated -- ^ generated by partial evaluator
677706 deriving (Show, Eq)
678707{-!
679708deriving instance Binary FnOpt
@@ -699,67 +728,84 @@ type ProvideWhat = ProvideWhat' PTerm
699728-- | Top-level declarations such as compiler directives, definitions,
700729-- datatypes and typeclasses.
701730data PDecl' t
702− = PFix FC Fixity [String] -- ^ Fixity declaration
703− | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
731+ -- | Fixity declaration
732+ = PFix FC Fixity [String]
733+ -- | Type declaration (last FC is precise name location)
734+ | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
735+ -- | Postulate, second FC is precise name location
704736 | PPostulate Bool -- external def if true
705− (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
706− | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
707− | PCAF FC Name t -- ^ Top level constant
708− | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
709− | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
710− | POpenInterfaces FC [Name] [PDecl' t] -- ^ Open block/declaration
737+ (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
738+ -- | Pattern clause
739+ | PClauses FC FnOpts Name [PClause' t]
740+ -- | Top level constant
741+ | PCAF FC Name t
742+ -- | Data declaration.
743+ | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
744+ -- | Params block
745+ | PParams FC [(Name, t)] [PDecl' t]
746+ -- | Open block/declaration
747+ | POpenInterfaces FC [Name] [PDecl' t]
748+ -- | New namespace, where FC is accurate location of the namespace
749+ -- in the file
711750 | PNamespace String FC [PDecl' t]
712− -- ^ New namespace, where FC is accurate location of the
713− -- namespace in the file
714− | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
715− Name -- Record name
716− FC -- Record name precise location
717− [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
718− [(Name, Docstring (Either Err t))] -- Param Docs
719− [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
720− (Maybe (Name, FC)) -- Optional constructor name and location
721− (Docstring (Either Err t)) -- Constructor doc
722− SyntaxInfo -- Constructor SyntaxInfo
723− -- ^ Record declaration
724− | PClass (Docstring (Either Err t)) SyntaxInfo FC
725− [(Name, t)] -- constraints
726− Name -- class name
727− FC -- accurate location of class name
728− [(Name, FC, t)] -- parameters and precise locations
729− [(Name, Docstring (Either Err t))] -- parameter docstrings
730− [(Name, FC)] -- determining parameters and precise locations
731− [PDecl' t] -- declarations
732− (Maybe (Name, FC)) -- instance constructor name and location
733− (Docstring (Either Err t)) -- instance constructor docs
734− -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
735− -- class name, class name location, parameters, method declarations, optional constructor name
736− | PInstance
737− (Docstring (Either Err t)) -- Instance docs
738− [(Name, Docstring (Either Err t))] -- Parameter docs
739− SyntaxInfo
740− FC [(Name, t)] -- constraints
741− [Name] -- parent dictionaries to search for constraints
742− Accessibility
743− FnOpts
744− Name -- class
745− FC -- precise location of class
746− [t] -- parameters
747− [(Name, t)] -- Extra names in scope in the body
748− t -- full instance type
749− (Maybe Name) -- explicit name
750− [PDecl' t]
751− -- ^ Instance declaration: arguments are documentation, syntax info, source
752− -- location, constraints, class name, parameters, full instance
753− -- type, optional explicit name, and definitions
751+ -- | Record name.
752+ | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
753+ Name -- Record name
754+ FC -- Record name precise location
755+ [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
756+ [(Name, Docstring (Either Err t))] -- Param Docs
757+ [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
758+ (Maybe (Name, FC)) -- Optional constructor name and location
759+ (Docstring (Either Err t)) -- Constructor doc
760+ SyntaxInfo -- Constructor SyntaxInfo
761+
762+ -- | Type class: arguments are documentation, syntax info, source
763+ -- location, constraints, class name, class name location,
764+ -- parameters, method declarations, optional constructor name
765+ | PClass (Docstring (Either Err t)) SyntaxInfo FC
766+ [(Name, t)] -- constraints
767+ Name -- class name
768+ FC -- accurate location of class name
769+ [(Name, FC, t)] -- parameters and precise locations
770+ [(Name, Docstring (Either Err t))] -- parameter docstrings
771+ [(Name, FC)] -- determining parameters and precise locations
772+ [PDecl' t] -- declarations
773+ (Maybe (Name, FC)) -- instance constructor name and location
774+ (Docstring (Either Err t)) -- instance constructor docs
775+
776+ -- | Instance declaration: arguments are documentation, syntax
777+ -- info, source location, constraints, class name, parameters, full
778+ -- instance type, optional explicit name, and definitions
779+ | PInstance (Docstring (Either Err t)) -- Instance docs
780+ [(Name, Docstring (Either Err t))] -- Parameter docs
781+ SyntaxInfo
782+ FC [(Name, t)] -- constraints
783+ [Name] -- parent dictionaries to search for constraints
784+ Accessibility
785+ FnOpts
786+ Name -- class
787+ FC -- precise location of class
788+ [t] -- parameters
789+ [(Name, t)] -- Extra names in scope in the body
790+ t -- full instance type
791+ (Maybe Name) -- explicit name
792+ [PDecl' t]
754793 | PDSL Name (DSL' t) -- ^ DSL declaration
755− | PSyntax FC Syntax -- ^ Syntax definition
794+ | PSyntax FC Syntax -- ^ Syntax definition
756795 | PMutual FC [PDecl' t] -- ^ Mutual block
757− | PDirective Directive -- ^ Compiler directive.
758− | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.
759− | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
760− -- bool is True, lhs and rhs must be convertible
761− | PRunElabDecl FC t [String] -- ^ FC is decl-level, for errors, and
762− -- Strings represent the namespace
796+ | PDirective Directive -- ^ Compiler directive.
797+
798+ -- | Type provider. The first t is the type, the second is the
799+ -- term. The second FC is precise highlighting location.
800+ | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
801+
802+ -- | Source-to-source transformation rule. If bool is True, lhs and
803+ -- rhs must be convertible.
804+ | PTransform FC Bool t t
805+
806+ -- | FC is decl-level, for errors, and Strings represent the
807+ -- namespace
808+ | PRunElabDecl FC t [String]
763809 deriving Functor
764810{-!
765811deriving instance Binary PDecl'
@@ -792,18 +838,19 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
792838 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
793839 | RAddInstance Name Name
794840 | RDatatypeDeclInstrs Name [PArg]
841+ -- | Datatype, constructors
795842 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
796− -- ^ Datatype, constructors
843+
797844
798845-- | For elaborator state
799846data EState = EState {
800− case_decls :: [(Name, PDecl)],
801− delayed_elab :: [(Int, Elab' EState ())],
802− new_tyDecls :: [RDeclInstructions],
803− highlighting :: [(FC, OutputAnnotation)],
804− auto_binds :: [Name], -- names bound as auto implicits
805− implicit_warnings :: [(FC, Name)] -- Implicit warnings to report (location and global name)
806− }
847+ case_decls :: [(Name, PDecl)]
848+ , delayed_elab :: [(Int, Elab' EState ())]
849+ , new_tyDecls :: [RDeclInstructions]
850+ , highlighting :: [(FC, OutputAnnotation)]
851+ , auto_binds :: [Name] -- ^ names bound as auto implicits
852+ , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
853+ }
807854
808855initEState :: EState
809856initEState = EState [] [] [] [] [] []
@@ -835,20 +882,23 @@ deriving instance NFData PClause'
835882!-}
836883
837884-- | Data declaration
838−data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
839− d_name_fc :: FC, -- ^ The precise location of the type constructor name
840− d_tcon :: t, -- ^ Type constructor
841− d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
842− }
843− -- ^ Data declaration
844− | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
845− -- ^ "Placeholder" for data whose constructors are defined later
846− deriving Functor
885+data PData' t =
886+ -- | Data declaration
887+ PDatadecl { d_name :: Name -- ^ The name of the datatype
888+ , d_name_fc :: FC -- ^ The precise location of the type constructor name
889+ , d_tcon :: t -- ^ Type constructor
890+ , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
891+ }
892+ -- | "Placeholder" for data whose constructors are defined later
893+ | PLaterdecl { d_name :: Name
894+ , d_name_fc :: FC
895+ , d_tcon :: t
896+ } deriving Functor
847897
848898-- | Transform the FCs in a PData and its associated terms. The first
849−-- function transforms the general-purpose FCs, and the second transforms
850−-- those that are used for semantic source highlighting, so they can be
851−-- treated specially.
899+-- function transforms the general-purpose FCs, and the second
900+-- transforms those that are used for semantic source highlighting, so
901+-- they can be treated specially.
852902mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
853903mapPDataFC f g (PDatadecl n nfc tycon ctors) =
854904 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
@@ -1030,56 +1080,76 @@ updateNs ns t = mapPT updateRef t
10301080-- (map (updateDNs ns) ds)
10311081-- updateDNs ns c = c
10321082
1033−data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
1083+data PunInfo = IsType
1084+ | IsTerm
1085+ | TypeOrTerm
1086+ deriving (Eq, Show, Data, Typeable)
10341087
10351088-- | High level language terms
1036−data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
1037− | PRef FC [FC] Name -- ^ A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.
1038− | PInferRef FC [FC] Name -- ^ A name to be defined later
1039− | PPatvar FC Name -- ^ A pattern variable
1040− | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1041− | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1042− | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1043− | PTyped PTerm PTerm -- ^ Term with explicit type
1044− | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1045− | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1046− | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1047− | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1048− | PMatchApp FC Name -- ^ Make an application by type matching
1049− | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1050− | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1051− | PTrue FC PunInfo -- ^ Unit type..?
1052− | PResolveTC FC -- ^ Solve this dictionary by type class resolution
1089+data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1090+ -- high-level language
1091+ | PRef FC [FC] Name
1092+ -- ^ A reference to a variable. The FC is its precise
1093+ -- source location for highlighting. The list of FCs is a
1094+ -- collection of additional highlighting locations.
1095+ | PInferRef FC [FC] Name -- ^ A name to be defined later
1096+ | PPatvar FC Name -- ^ A pattern variable
1097+ | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1098+ | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1099+ | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1100+ | PTyped PTerm PTerm -- ^ Term with explicit type
1101+ | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1102+ | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1103+ | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1104+ | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1105+ | PMatchApp FC Name -- ^ Make an application by type matching
1106+ | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1107+ | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1108+ | PTrue FC PunInfo -- ^ Unit type..?
1109+ | PResolveTC FC -- ^ Solve this dictionary by type class resolution
10531110 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1054− -- ^ "rewrite" syntax, with optional rewriting function
1055− -- and optional result type
1056− | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.
1057− | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.
1058− | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1111+ -- ^ "rewrite" syntax, with optional rewriting function and
1112+ -- optional result type
1113+ | PPair FC [FC] PunInfo PTerm PTerm
1114+ -- ^ A pair (a, b) and whether it's a product type or a
1115+ -- pair (solved by elaboration). The list of FCs is its
1116+ -- punctuation.
1117+ | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1118+ -- ^ A dependent pair (tm : a ** b) and whether it's a
1119+ -- sigma type or a pair that inhabits one (solved by
1120+ -- elaboration). The [FC] is its punctuation.
1121+ | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
10591122 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1060− | PHidden PTerm -- ^ Irrelevant or hidden pattern
1061− | PType FC -- ^ 'Type' type
1062− | PUniverse Universe -- ^ Some universe
1063− | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1064− | PConstant FC Const -- ^ Builtin types
1065− | Placeholder -- ^ Underscore
1066− | PDoBlock [PDo] -- ^ Do notation
1067− | PIdiom FC PTerm -- ^ Idiom brackets
1123+ | PHidden PTerm -- ^ Irrelevant or hidden pattern
1124+ | PType FC -- ^ 'Type' type
1125+ | PUniverse Universe -- ^ Some universe
1126+ | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1127+ | PConstant FC Const -- ^ Builtin types
1128+ | Placeholder -- ^ Underscore
1129+ | PDoBlock [PDo] -- ^ Do notation
1130+ | PIdiom FC PTerm -- ^ Idiom brackets
10681131 | PReturn FC
1069− | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1070− | PProof [PTactic] -- ^ Proof script
1071− | PTactics [PTactic] -- ^ As PProof, but no auto solving
1072− | PElabError Err -- ^ Error to report on elaboration
1073− | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1074− | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1075− | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1076− | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1077− | PNoImplicits PTerm -- ^ never run implicit converions on the term
1078− | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1079− | PUnquote PTerm -- ^ ~Term
1080− | PQuoteName Name Bool FC -- ^ `{n} where the FC is the precise highlighting for the name in particular. If the Bool is False, then it's `{{n}} and the name won't be resolved.
1081− | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
1082− | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
1132+ | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1133+ | PProof [PTactic] -- ^ Proof script
1134+ | PTactics [PTactic] -- ^ As PProof, but no auto solving
1135+ | PElabError Err -- ^ Error to report on elaboration
1136+ | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1137+ | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1138+ | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1139+ | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1140+ | PNoImplicits PTerm -- ^ never run implicit converions on the term
1141+ | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1142+ | PUnquote PTerm -- ^ ~Term
1143+ | PQuoteName Name Bool FC
1144+ -- ^ `{n} where the FC is the precise highlighting for
1145+ -- the name in particular. If the Bool is False, then
1146+ -- it's `{{n}} and the name won't be resolved.
1147+ | PRunElab FC PTerm [String]
1148+ -- ^ %runElab tm - New-style proof script. Args are
1149+ -- location, script, enclosing namespace.
1150+ | PConstSugar FC PTerm
1151+ -- ^ A desugared constant. The FC is a precise source
1152+ -- location that will be used to highlight it later.
10831153 deriving (Eq, Data, Typeable)
10841154
10851155data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
@@ -1249,9 +1319,9 @@ instance Sized a => Sized (PTactic' a) where
12491319type PTactic = PTactic' PTerm
12501320
12511321data PDo' t = DoExp FC t
1252− | DoBind FC Name FC t -- ^ second FC is precise name location
1322+ | DoBind FC Name FC t -- ^ second FC is precise name location
12531323 | DoBindP FC t t [(t,t)]
1254− | DoLet FC Name FC t t -- ^ second FC is precise name location
1324+ | DoLet FC Name FC t t -- ^ second FC is precise name location
12551325 | DoLetP FC t t
12561326 deriving (Eq, Functor, Data, Typeable)
12571327{-!
@@ -1262,9 +1332,9 @@ deriving instance NFData PDo'
12621332instance Sized a => Sized (PDo' a) where
12631333 size (DoExp fc t) = 1 + size fc + size t
12641334 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1265− size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1266− size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1267− size (DoLetP fc l r) = 1 + size fc + size l + size r
1335+ size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1336+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1337+ size (DoLetP fc l r) = 1 + size fc + size l + size r
12681338
12691339type PDo = PDo' PTerm
12701340
@@ -1272,33 +1342,40 @@ type PDo = PDo' PTerm
12721342-- things early which will help give a more concrete type to other
12731343-- variables, e.g. a before (interpTy a).
12741344
1275−data PArg' t = PImp { priority :: Int,
1276− machine_inf :: Bool, -- true if the machine inferred it
1277− argopts :: [ArgOpt],
1278− pname :: Name,
1279− getTm :: t }
1280− | PExp { priority :: Int,
1281− argopts :: [ArgOpt],
1282− pname :: Name,
1283− getTm :: t }
1284− | PConstraint { priority :: Int,
1285− argopts :: [ArgOpt],
1286− pname :: Name,
1287− getTm :: t }
1288− | PTacImplicit { priority :: Int,
1289− argopts :: [ArgOpt],
1290− pname :: Name,
1291− getScript :: t,
1292− getTm :: t }
1293− deriving (Show, Eq, Functor, Data, Typeable)
1294−
1295−data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1296− deriving (Show, Eq, Data, Typeable)
1345+data PArg' t = PImp { priority :: Int
1346+ , machine_inf :: Bool -- ^ true if the machine inferred it
1347+ , argopts :: [ArgOpt]
1348+ , pname :: Name
1349+ , getTm :: t
1350+ }
1351+ | PExp { priority :: Int
1352+ , argopts :: [ArgOpt]
1353+ , pname :: Name
1354+ , getTm :: t
1355+ }
1356+ | PConstraint { priority :: Int
1357+ , argopts :: [ArgOpt]
1358+ , pname :: Name
1359+ , getTm :: t
1360+ }
1361+ | PTacImplicit { priority :: Int
1362+ , argopts :: [ArgOpt]
1363+ , pname :: Name
1364+ , getScript :: t
1365+ , getTm :: t
1366+ }
1367+ deriving (Show, Eq, Functor, Data, Typeable)
1368+
1369+data ArgOpt = AlwaysShow
1370+ | HideDisplay
1371+ | InaccessibleArg
1372+ | UnknownImp
1373+ deriving (Show, Eq, Data, Typeable)
12971374
12981375instance Sized a => Sized (PArg' a) where
12991376 size (PImp p _ l nm trm) = 1 + size nm + size trm
13001377 size (PExp p l nm trm) = 1 + size nm + size trm
1301− size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1378+ size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
13021379 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
13031380
13041381{-!
@@ -1375,28 +1452,30 @@ highestFC (PAppImpl t _) = highestFC t
13751452
13761453-- Type class data
13771454
1378−data ClassInfo = CI { instanceCtorName :: Name,
1379− class_methods :: [(Name, (Bool, FnOpts, PTerm))], -- flag whether it's a "data" method
1380− class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1381− class_default_superclasses :: [PDecl],
1382− class_params :: [Name],
1383− class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1384− class_determiners :: [Int] }
1385− deriving Show
1455+data ClassInfo = CI {
1456+ instanceCtorName :: Name
1457+ , class_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1458+ , class_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1459+ , class_default_superclasses :: [PDecl]
1460+ , class_params :: [Name]
1461+ , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded
1462+ , class_determiners :: [Int]
1463+ } deriving Show
13861464{-!
13871465deriving instance Binary ClassInfo
13881466deriving instance NFData ClassInfo
13891467!-}
13901468
13911469-- Record data
1392−data RecordInfo = RI { record_parameters :: [(Name,PTerm)],
1393− record_constructor :: Name,
1394− record_projections :: [Name] }
1395− deriving Show
1470+data RecordInfo = RI {
1471+ record_parameters :: [(Name,PTerm)]
1472+ , record_constructor :: Name
1473+ , record_projections :: [Name]
1474+ } deriving Show
13961475
13971476-- Type inference data
13981477
1399−data TIData = TIPartial -- ^ a function with a partially defined type
1478+data TIData = TIPartial -- ^ a function with a partially defined type
14001479 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
14011480 deriving Show
14021481
@@ -1408,27 +1487,28 @@ deriving instance Binary FnInfo
14081487deriving instance NFData FnInfo
14091488!-}
14101489
1411−data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1412− detaggable :: Bool }
1413− deriving Show
1490+data OptInfo = Optimise {
1491+ inaccessible :: [(Int,Name)] -- includes names for error reporting
1492+ , detaggable :: Bool
1493+ } deriving Show
14141494{-!
14151495deriving instance Binary OptInfo
14161496deriving instance NFData OptInfo
14171497!-}
14181498
14191499-- | Syntactic sugar info
1420−data DSL' t = DSL { dsl_bind :: t,
1421− dsl_return :: t,
1422− dsl_apply :: t,
1423− dsl_pure :: t,
1424− dsl_var :: Maybe t,
1425− index_first :: Maybe t,
1426− index_next :: Maybe t,
1427− dsl_lambda :: Maybe t,
1428− dsl_let :: Maybe t,
1429− dsl_pi :: Maybe t
1430− }
1431− deriving (Show, Functor)
1500+data DSL' t = DSL {
1501+ dsl_bind :: t
1502+ , dsl_return :: t
1503+ , dsl_apply :: t
1504+ , dsl_pure :: t
1505+ , dsl_var :: Maybe t
1506+ , index_first :: Maybe t
1507+ , index_next :: Maybe t
1508+ , dsl_lambda :: Maybe t
1509+ , dsl_let :: Maybe t
1510+ , dsl_pi :: Maybe t
1511+ } deriving (Show, Functor)
14321512{-!
14331513deriving instance Binary DSL'
14341514deriving instance NFData DSL'
@@ -1436,7 +1516,9 @@ deriving instance NFData DSL'
14361516
14371517type DSL = DSL' PTerm
14381518
1439−data SynContext = PatternSyntax | TermSyntax | AnySyntax
1519+data SynContext = PatternSyntax
1520+ | TermSyntax
1521+ | AnySyntax
14401522 deriving Show
14411523{-!
14421524deriving instance Binary SynContext
@@ -1536,24 +1618,25 @@ deriving instance Binary Using
15361618deriving instance NFData Using
15371619!-}
15381620
1539−data SyntaxInfo = Syn { using :: [Using],
1540− syn_params :: [(Name, PTerm)],
1541− syn_namespace :: [String],
1542− no_imp :: [Name],
1543− imp_methods :: [Name], -- class methods. When expanding
1544− -- implicits, these should be expanded even under
1545− -- binders
1546− decoration :: Name -> Name,
1547− inPattern :: Bool,
1548− implicitAllowed :: Bool,
1549− constraintAllowed :: Bool,
1550− maxline :: Maybe Int,
1551− mut_nesting :: Int,
1552− dsl_info :: DSL,
1553− syn_in_quasiquote :: Int,
1554− syn_toplevel :: Bool,
1555− withAppAllowed :: Bool }
1556− deriving Show
1621+data SyntaxInfo = Syn {
1622+ using :: [Using]
1623+ , syn_params :: [(Name, PTerm)]
1624+ , syn_namespace :: [String]
1625+ , no_imp :: [Name]
1626+ , imp_methods :: [Name]
1627+ -- ^ class methods. When expanding implicits, these should be
1628+ -- expanded even under binders
1629+ , decoration :: Name -> Name
1630+ , inPattern :: Bool
1631+ , implicitAllowed :: Bool
1632+ , constraintAllowed :: Bool
1633+ , maxline :: Maybe Int
1634+ , mut_nesting :: Int
1635+ , dsl_info :: DSL
1636+ , syn_in_quasiquote :: Int
1637+ , syn_toplevel :: Bool
1638+ , withAppAllowed :: Bool
1639+ } deriving Show
15571640{-!
15581641deriving instance NFData SyntaxInfo
15591642deriving instance Binary SyntaxInfo
@@ -1693,9 +1776,9 @@ instance Show PData where
16931776instance Pretty PTerm OutputAnnotation where
16941777 pretty = prettyImp defaultPPOption
16951778
1696−-- | Colourise annotations according to an Idris state. It ignores the names
1697−-- in the annotation, as there's no good way to show extended information on a
1698−-- terminal.
1779+-- | Colourise annotations according to an Idris state. It ignores the
1780+-- names in the annotation, as there's no good way to show extended
1781+-- information on a terminal.
16991782annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
17001783annotationColour ist _ | not (idris_colourRepl ist) = Nothing
17011784annotationColour ist (AnnConst c) =
@@ -1724,8 +1807,8 @@ annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
17241807annotationColour ist _ = Nothing
17251808
17261809
1727−-- | Colourise annotations according to an Idris state. It ignores the names
1728−-- in the annotation, as there's no good way to show extended
1810+-- | Colourise annotations according to an Idris state. It ignores the
1811+-- names in the annotation, as there's no good way to show extended
17291812-- information on a terminal. Note that strings produced this way will
17301813-- not be coloured on Windows, so the use of the colour rendering
17311814-- functions in Idris.Output is to be preferred.
@@ -1735,9 +1818,10 @@ consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
17351818isPostulateName :: Name -> IState -> Bool
17361819isPostulateName n ist = S.member n (idris_postulates ist)
17371820
1738−-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1739−prettyImp :: PPOption -- ^^ pretty printing options
1740− -> PTerm -- ^^ the term to pretty-print
1821+-- | Pretty-print a high-level closed Idris term with no information
1822+-- about precedence/associativity
1823+prettyImp :: PPOption -- ^ pretty printing options
1824+ -> PTerm -- ^ the term to pretty-print
17411825 -> Doc OutputAnnotation
17421826prettyImp impl = pprintPTerm impl [] [] []
17431827
@@ -1747,12 +1831,13 @@ prettyImp impl = pprintPTerm impl [] [] []
17471831prettyIst :: IState -> PTerm -> Doc OutputAnnotation
17481832prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
17491833
1750−-- | Pretty-print a high-level Idris term in some bindings context with infix info
1751−pprintPTerm :: PPOption -- ^^ pretty printing options
1752− -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1753− -> [Name] -- ^^ names to always show in pi, even if not used
1754− -> [FixDecl] -- ^^ Fixity declarations
1755− -> PTerm -- ^^ the term to pretty-print
1834+-- | Pretty-print a high-level Idris term in some bindings context
1835+-- with infix info.
1836+pprintPTerm :: PPOption -- ^ pretty printing options
1837+ -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1838+ -> [Name] -- ^ names to always show in pi, even if not used
1839+ -> [FixDecl] -- ^ Fixity declarations
1840+ -> PTerm -- ^ the term to pretty-print
17561841 -> Doc OutputAnnotation
17571842pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
17581843 where
@@ -2125,8 +2210,8 @@ basename :: Name -> Name
21252210basename (NS n _) = basename n
21262211basename n = n
21272212
2128−-- | Determine whether a name was the one inserted for a hole or
2129−-- guess by the delaborator
2213+-- | Determine whether a name was the one inserted for a hole or guess
2214+-- by the delaborator
21302215isHoleName :: Name -> Bool
21312216isHoleName (UN n) = n == T.pack "[__]"
21322217isHoleName _ = False
@@ -2136,12 +2221,11 @@ containsHole :: PTerm -> Bool
21362221containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
21372222
21382223-- | Pretty-printer helper for names that attaches the correct annotations
2139−prettyName
2140− :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
2141− -> Bool -- ^^ whether to show namespaces
2142− -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
2143− -> Name -- ^^ the name to pprint
2144− -> Doc OutputAnnotation
2224+prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2225+ -> Bool -- ^ whether to show namespaces
2226+ -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2227+ -> Name -- ^ the name to pprint
2228+ -> Doc OutputAnnotation
21452229prettyName infixParen showNS bnd n
21462230 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
21472231 | (UN n') <- n, T.unpack n' == "_" = text "_"
@@ -2228,11 +2312,11 @@ getAll = map getTm
22282312
22292313
22302314-- | Show Idris name
2231−showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
2232− -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
2233− -> PPOption -- ^^ pretty printing options
2234− -> Bool -- ^^ whether to colourise
2235− -> Name -- ^^ the term to show
2315+showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2316+ -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2317+ -> PPOption -- ^ pretty printing options
2318+ -> Bool -- ^ whether to colourise
2319+ -> Name -- ^ the term to show
22362320 -> String
22372321showName ist bnd ppo colour n = case ist of
22382322 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
@@ -2256,8 +2340,8 @@ showName ist bnd ppo colour n = case ist of
22562340 -- (like error messages). Thus, unknown vars are colourised as implicits.
22572341 | otherwise -> colouriseImplicit t name
22582342
2259−showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
2260− -> PTerm -- ^^ the term to show
2343+showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2344+ -> PTerm -- ^ the term to show
22612345 -> String
22622346showTm ist = displayDecorated (consoleDecorate ist) .
22632347 renderPretty 0.8 100000 .