2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
9{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
10 DeriveTraversable, FlexibleContexts, FlexibleInstances,
11 MultiParamTypeClasses, PatternGuards, TypeSynonymInstances #-}
13module Idris.AbsSyntaxTree where
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
18import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
29import Prelude hiding (Foldable, Traversable, (<$>))
31import Control.Applicative ((<|>))
32import qualified Control.Monad.Trans.Class as Trans (lift)
33import Control.Monad.Trans.Except
34import Control.Monad.Trans.State.Strict
36import Data.Data (Data)
38import Data.Foldable (Foldable)
39import Data.Function (on)
40import Data.Generics.Uniplate.Data (children, universe)
41import Data.List hiding (group)
42import qualified Data.Map.Strict as M
43import Data.Maybe (mapMaybe, maybeToList)
44import qualified Data.Set as S
45import qualified Data.Text as T
46import Data.Traversable (Traversable)
48import GHC.Generics (Generic)
51data ElabWhat = ETypes | EDefns | EAll
54-- | Data to pass to recursively called elaborators; e.g. for where blocks,
55-- paramaterised declarations, etc.
57-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
58-- so that we can have mutually recursive elaborators in separate modules without
59-- having to muck about with cyclic modules.
60data ElabInfo = EInfo {
61 params :: [(Name, PTerm)]
62 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
63 , liftname :: Name -> Name
64 , namespace :: [String]
66 , constraintNS :: String -- ^ filename for adding to constraint variables
68 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
69 -- | We may, recursively, collect transformations to do on the rhs,
70 -- e.g. rewriting recursive calls to functions defined by 'with'
71 , rhs_trans :: PTerm -> PTerm
72 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
76toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
78toplevelWith :: String -> ElabInfo
79toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
81eInfoNames :: ElabInfo -> [Name]
82eInfoNames info = map fst (params info) ++ M.keys (inblock info)
84data IOption = IOption {
86 , opt_logcats :: [LogCat] -- ^ List of logging categories.
87 , opt_typecase :: Bool
88 , opt_typeintype :: Bool
89 , opt_coverage :: Bool
90 , opt_showimp :: Bool -- ^ show implicits
91 , opt_errContext :: Bool
94 , opt_nobanner :: Bool
96 , opt_codegen :: Codegen
97 , opt_outputTy :: OutputType
98 , opt_ibcsubdir :: FilePath
99 , opt_importdirs :: [FilePath]
100 , opt_sourcedirs :: [FilePath]
101 , opt_triple :: String
103 , opt_cmdline :: [Opt] -- ^ remember whole command line
104 , opt_origerr :: Bool
105 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
106 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
107 , opt_optimise :: [Optimisation]
108 , opt_printdepth :: Maybe Int
109 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
110 , opt_desugarnats :: Bool
111 , opt_autoimpls :: Bool
112 } deriving (Show, Eq, Generic)
114defaultOpts :: IOption
115defaultOpts = IOption { opt_logLevel = 0
117 , opt_typecase = False
118 , opt_typeintype = False
119 , opt_coverage = True
120 , opt_showimp = False
121 , opt_errContext = False
124 , opt_nobanner = False
126 , opt_codegen = Via IBCFormat "c"
127 , opt_outputTy = Executable
129 , opt_importdirs = []
130 , opt_sourcedirs = []
134 , opt_origerr = False
135 , opt_autoSolve = True
136 , opt_autoImport = []
137 , opt_optimise = defaultOptimise
138 , opt_printdepth = Just 5000
139 , opt_evaltypes = True
140 , opt_desugarnats = False
141 , opt_autoimpls = True
144data PPOption = PPOption {
145 ppopt_impl :: Bool -- ^ whether to show implicits
146 , ppopt_desugarnats :: Bool
147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
148 , ppopt_depth :: Maybe Int
149 , ppopt_displayrig :: Bool -- ^ whether to display multiplicities in binders
154defaultOptimise :: [Optimisation]
157-- | Pretty printing options with default verbosity.
158defaultPPOption :: PPOption
159defaultPPOption = PPOption {
161 , ppopt_desugarnats = False
162 , ppopt_pinames = False
163 , ppopt_depth = Nothing
164 , ppopt_displayrig = False
167-- | Pretty printing options with the most verbosity.
168verbosePPOption :: PPOption
169verbosePPOption = PPOption {
171 , ppopt_desugarnats = True
172 , ppopt_pinames = True
173 , ppopt_depth = Nothing
174 , ppopt_displayrig = False
177-- | Get pretty printing options from the big options record.
178ppOption :: IOption -> PPOption
179ppOption opt = PPOption {
180 ppopt_impl = opt_showimp opt
181 , ppopt_pinames = False
182 , ppopt_depth = opt_printdepth opt
183 , ppopt_desugarnats = opt_desugarnats opt
184 , ppopt_displayrig = False
187-- | Get pretty printing options from an idris state record.
188ppOptionIst :: IState -> PPOption
189ppOptionIst = ppOption . idris_options
192-- | The output mode in use
193data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
194 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
198-- | If a function has no totality annotation, what do we assume?
199data DefaultTotality = DefaultCheckingTotal -- ^ Total
200 | DefaultCheckingPartial -- ^ Partial
201 | DefaultCheckingCovering -- ^Total coverage, but may diverge
202 deriving (Show, Eq, Generic)
204-- | Configuration options for interactive editing.
205data InteractiveOpts = InteractiveOpts {
206 interactiveOpts_indentWith :: Int
207 , interactiveOpts_indentClause :: Int
208} deriving (Show, Generic)
210-- | The global state used in the Idris monad
211data IState = IState {
212 tt_ctxt :: Context -- ^ All the currently defined names and their terms
213 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
214 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
215 , idris_implicits :: Ctxt [PArg]
216 , idris_statics :: Ctxt [Bool]
217 , idris_interfaces :: Ctxt InterfaceInfo
218 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
219 , idris_records :: Ctxt RecordInfo
220 , idris_dsls :: Ctxt DSL
221 , idris_optimisation :: Ctxt OptInfo
222 , idris_datatypes :: Ctxt TypeInfo
223 , idris_namehints :: Ctxt [Name]
225 -- | list of lhs/rhs, and a list of missing clauses. These are not
227 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
228 , idris_flags :: Ctxt [FnOpt]
229 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
230 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
232 -- | module documentation is saved in a special MN so the context
233 -- mechanism can be used for disambiguation.
234 , idris_moduledocs :: Ctxt (Docstring DocTerm)
235 , idris_tyinfodata :: Ctxt TIData
236 , idris_fninfo :: Ctxt FnInfo
237 , idris_transforms :: Ctxt [(Term, Term)]
238 , idris_autohints :: Ctxt [Name]
239 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
240 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
241 , idris_totcheckfail :: [(FC, String)]
242 , idris_options :: IOption
244 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
246 -- | The currently defined but not proven metavariables. The Int is
247 -- the number of vars to display as a context, the Maybe Name is its
248 -- top-level function, the [Name] is the list of local variables
249 -- available for proof search and the Bools are whether :p is
250 -- allowed, and whether the variable is definable at all
251 -- (Metavariables are not definable if they are applied in a term
252 -- which still has hole bindings)
253 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
254 , idris_coercions :: [Name]
255 , idris_errRev :: [(Term, Term)]
256 , idris_errReduce :: [Name]
257 , syntax_rules :: SyntaxRules
258 , syntax_keywords :: [String]
259 , imported :: [FilePath] -- ^ The imported modules
260 , idris_scprims :: [(Name, (Int, PrimFn))]
261 , idris_objs :: [(Codegen, FilePath)]
262 , idris_libs :: [(Codegen, String)]
263 , idris_cgflags :: [(Codegen, String)]
264 , idris_hdrs :: [(Codegen, String)]
265 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
266 , proof_list :: [(Name, (Bool, [String]))]
267 , errSpan :: Maybe FC
268 , parserWarnings :: [(FC, Err)]
269 , lastParse :: Maybe Name
270 , indent_stack :: [Int]
271 , brace_stack :: [Maybe Int]
272 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
273 , idris_parsedSpan :: Maybe FC
274 , hide_list :: Ctxt Accessibility
275 , default_access :: Accessibility
276 , default_total :: DefaultTotality
277 , ibc_write :: [IBCWrite]
278 , compiled_so :: Maybe String
279 , idris_dynamic_libs :: [DynamicLib]
280 , idris_language_extensions :: [LanguageExt]
281 , idris_outputmode :: OutputMode
282 , idris_colourRepl :: Bool
283 , idris_colourTheme :: ColourTheme
284 , idris_errorhandlers :: [Name] -- ^ Global error handlers
285 , idris_nameIdx :: (Int, Ctxt (Int, Name))
286 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
287 , module_aliases :: M.Map [T.Text] [T.Text]
288 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
289 , idris_postulates :: S.Set Name
290 , idris_externs :: S.Set (Name, Int)
291 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
293 -- | List of names that were defined in the repl, and can be re-/un-defined
294 , idris_repl_defs :: [Name]
296 -- | Stack of names currently being elaborated, Bool set if it's an
297 -- implementation (implementations appear twice; also as a function name)
298 , elab_stack :: [(Name, Bool)]
301 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
302 , idris_exports :: [Name] -- ^ Functions with ExportList
303 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
304 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
305 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
306 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
307 , idris_ttstats :: M.Map Term (Int, Term)
308 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
309 , idris_interactiveOpts :: InteractiveOpts
312-- Required for parsers library, and therefore trifecta
313instance Show IState where
314 show = const "{internal state}"
316data SizeChange = Smaller | Same | Bigger | Unknown
317 deriving (Show, Eq, Generic)
319deriving instance Binary SizeChange
322type SCGEntry = (Name, [Maybe (Int, SizeChange)])
323type UsageReason = (Name, Int) -- fn_name, its_arg_number
325data CGInfo = CGInfo {
326 calls :: [Name] -- Immediate calls
327 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
329 , usedpos :: [(Int, [UsageReason])]
330 } deriving (Show, Generic)
332deriving instance Binary CGInfo
336primDefs = [ sUN "unsafePerformPrimIO"
337 , sUN "mkLazyForeignPrim"
338 , sUN "mkForeignPrim"
340 , sUN "assert_unreachable"
344-- information that needs writing for the current module's .ibc file
345data IBCWrite = IBCFix FixDecl
350 | IBCImplementation Bool Bool Name Name
357 | IBCImport (Bool, FilePath) -- ^ True = import public
358 | IBCImportDir FilePath
359 | IBCSourceDir FilePath
360 | IBCObj Codegen FilePath
361 | IBCLib Codegen String
362 | IBCCGFlag Codegen String
364 | IBCHeader Codegen String
365 | IBCAccess Name Accessibility
366 | IBCMetaInformation Name MetaInformation
367 | IBCTotal Name Totality
368 | IBCInjective Name Injectivity
370 | IBCFnInfo Name FnInfo
371 | IBCTrans Name (Term, Term)
372 | IBCErrRev (Term, Term)
377 | IBCDef Name -- ^ The main context.
378 | IBCNameHint (Name, Name)
379 | IBCLineApp FilePath Int PTerm
380 | IBCErrorHandler Name
381 | IBCFunctionErrorHandler Name Name Name
383 | IBCExtern (Name, Int)
384 | IBCTotCheckErr FC String
386 | IBCModDocs Name -- ^ The name is the special name used to track module docs
387 | IBCUsage (Name, Int)
389 | IBCAutoHint Name Name
390 | IBCDeprecate Name String
391 | IBCFragile Name String
392 | IBCConstraint FC UConstraint
393 deriving (Show, Generic)
395initialInteractiveOpts :: InteractiveOpts
396initialInteractiveOpts = InteractiveOpts {
397 interactiveOpts_indentWith = 2
398 , interactiveOpts_indentClause = 2
401-- | The initial state for the compiler
403idrisInit = IState initContext S.empty []
404 emptyContext emptyContext emptyContext [] emptyContext
405 emptyContext emptyContext emptyContext emptyContext
406 emptyContext emptyContext emptyContext emptyContext
407 emptyContext emptyContext emptyContext emptyContext
409 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
410 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
411 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
412 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
413 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
416-- | The monad for the main REPL - reading and processing files and
417-- updating global state (hence the IO inner monad).
420-- type Idris = WriterT [Either String (IO ())] (State IState a))
423type Idris = StateT IState (ExceptT Err IO)
425catchError :: Idris a -> (Err -> Idris a) -> Idris a
426catchError = liftCatch catchE
428throwError :: Err -> Idris a
429throwError = Trans.lift . throwE
431-- Commands in the REPL
436data ElabShellCmd = EQED
444 | EDocStr (Either Name Const)
450-- Parsed declarations
452data Fixity = Infixl { prec :: Int }
453 | Infixr { prec :: Int }
454 | InfixN { prec :: Int }
455 | PrefixN { prec :: Int }
456 deriving (Eq, Generic)
458deriving instance Binary Fixity
461instance Show Fixity where
462 show (Infixl i) = "infixl " ++ show i
463 show (Infixr i) = "infixr " ++ show i
464 show (InfixN i) = "infix " ++ show i
465 show (PrefixN i) = "prefix " ++ show i
467data FixDecl = Fix Fixity String
468 deriving (Eq, Generic)
470instance Show FixDecl where
471 show (Fix f s) = show f ++ " " ++ s
474deriving instance Binary FixDecl
477instance Ord FixDecl where
478 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
481data Static = Static | Dynamic
482 deriving (Show, Eq, Ord, Data, Generic, Typeable)
484deriving instance Binary Static
487-- ^ Mark bindings with their explicitness, and laziness
488data Plicity = Imp { pargopts :: [ArgOpt]
491 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
492 , pinsource :: Bool -- ^ Explicitly written in source
495 | Exp { pargopts :: [ArgOpt]
497 , pparam :: Bool -- ^ this is a param (rather than index)
500 | Constraint { pargopts :: [ArgOpt]
504 | TacImp { pargopts :: [ArgOpt]
509 deriving (Show, Eq, Ord, Data, Generic, Typeable)
512deriving instance Binary Plicity
515is_scoped :: Plicity -> Maybe ImplicitInfo
516is_scoped (Imp _ _ _ s _ _) = s
521impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
522-- Machine generated top level implicit
524impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
528forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
529forall_constraint :: Plicity
530forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
533expl = Exp [] Dynamic False RigW
535expl_param = Exp [] Dynamic True RigW
536expl_linear :: Plicity
537expl_linear = Exp [] Dynamic False Rig1
540constraint = Constraint [] Static RigW
542tacimpl :: PTerm -> Plicity
543tacimpl t = TacImp [] Dynamic t RigW
545data FnOpt = Inlinable -- ^ always evaluate when simplifying
546 | TotalFn | PartialFn | CoveringFn
547 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
550 -- | interface dictionary, eval only when a function
551 -- argument, and further evaluation results.
553 | OverlappingDictionary -- ^ Interface dictionary which may overlap
554 | Implicit -- ^ implicit coercion
555 | NoImplicit -- ^ do not apply implicit coercions
556 | CExport String -- ^ export, with a C name
557 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
558 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
559 | ErrorReduce -- ^ unfold definition before showing an error
560 | Reflection -- ^ a reflecting function, compile-time only
561 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
562 | Constructor -- ^ Data constructor type
563 | AutoHint -- ^ use in auto implicit search
564 | PEGenerated -- ^ generated by partial evaluator
565 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
566 deriving (Show, Eq, Generic)
568deriving instance Binary FnOpt
573inlinable :: FnOpts -> Bool
574inlinable = elem Inlinable
576dictionary :: FnOpts -> Bool
577dictionary = elem Dictionary
580-- | Type provider - what to provide
581data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
582 | ProvPostulate t -- ^ goal type must be Type, so only term
583 deriving (Show, Eq, Functor, Generic)
585type ProvideWhat = ProvideWhat' PTerm
587-- | Top-level declarations such as compiler directives, definitions,
588-- datatypes and interfaces.
590 -- | Fixity declaration
591 = PFix FC Fixity [String]
592 -- | Type declaration (last FC is precise name location)
593 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
594 -- | Postulate, second FC is precise name location
595 | PPostulate Bool -- external def if true
596 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
598 | PClauses FC FnOpts Name [PClause' t]
599 -- | Top level constant
601 -- | Data declaration.
602 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
604 | PParams FC [(Name, t)] [PDecl' t]
605 -- | Open block/declaration
606 | POpenInterfaces FC [Name] [PDecl' t]
607 -- | New namespace, where FC is accurate location of the namespace
609 | PNamespace String FC [PDecl' t]
611 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
613 FC -- Record name precise location
614 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
615 [(Name, Docstring (Either Err t))] -- Param Docs
616 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
617 (Maybe (Name, FC)) -- Optional constructor name and location
618 (Docstring (Either Err t)) -- Constructor doc
619 SyntaxInfo -- Constructor SyntaxInfo
621 -- | Interface: arguments are documentation, syntax info, source
622 -- location, constraints, interface name, interface name location,
623 -- parameters, method declarations, optional constructor name
624 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
625 [(Name, t)] -- constraints
626 Name -- interface name
627 FC -- accurate location of interface name
628 [(Name, FC, t)] -- parameters and precise locations
629 [(Name, Docstring (Either Err t))] -- parameter docstrings
630 [(Name, FC)] -- determining parameters and precise locations
631 [PDecl' t] -- declarations
632 (Maybe (Name, FC)) -- implementation constructor name and location
633 (Docstring (Either Err t)) -- implementation constructor docs
635 -- | Implementation declaration: arguments are documentation, syntax
636 -- info, source location, constraints, interface name, parameters, full
637 -- Implementation type, optional explicit name, and definitions
638 | PImplementation (Docstring (Either Err t)) -- Implementation docs
639 [(Name, Docstring (Either Err t))] -- Parameter docs
641 FC [(Name, t)] -- constraints
642 [Name] -- parent dictionaries to search for constraints
646 FC -- precise location of interface
648 [(Name, t)] -- Extra names in scope in the body
649 t -- full Implementation type
650 (Maybe Name) -- explicit name
652 | PDSL Name (DSL' t) -- ^ DSL declaration
653 | PSyntax FC Syntax -- ^ Syntax definition
654 | PMutual FC [PDecl' t] -- ^ Mutual block
655 | PDirective Directive -- ^ Compiler directive.
657 -- | Type provider. The first t is the type, the second is the
658 -- term. The second FC is precise highlighting location.
659 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
661 -- | Source-to-source transformation rule. If bool is True, lhs and
662 -- rhs must be convertible.
663 | PTransform FC Bool t t
665 -- | FC is decl-level, for errors, and Strings represent the
667 | PRunElabDecl FC t [String]
668 deriving (Functor, Generic)
670deriving instance Binary PDecl'
673-- | The set of source directives
674data Directive = DLib Codegen String
675 | DLink Codegen String
676 | DFlag Codegen String
677 | DInclude Codegen String
682 | DSetTotal Name -- assert totality after checking
683 | DAccess Accessibility
684 | DDefault DefaultTotality
686 | DDynamicLibs [String]
687 | DNameHint Name FC [(Name, FC)]
688 | DErrorHandlers Name FC Name FC [(Name, FC)]
689 | DLanguage LanguageExt
690 | DDeprecate Name String
691 | DFragile Name String
692 | DAutoImplicits Bool
696-- | A set of instructions for things that need to happen in IState
697-- after a term elaboration when there's been reflected elaboration.
698data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
699 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
700 | RAddImplementation Name Name
701 | RDatatypeDeclInstrs Name [PArg]
702 -- | Datatype, constructors
703 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
706-- | For elaborator state
707data EState = EState {
708 case_decls :: [(Name, PDecl)]
709 , delayed_elab :: [(Int, Elab' EState ())]
710 , new_tyDecls :: [RDeclInstructions]
711 , highlighting :: [(FC, OutputAnnotation)]
712 , auto_binds :: [Name] -- ^ names bound as auto implicits
713 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
717initEState = EState [] [] [] [] [] []
719type ElabD a = Elab' EState a
721highlightSource :: FC -> OutputAnnotation -> ElabD ()
722highlightSource fc annot =
723 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
725-- | One clause of a top-level definition. Term arguments to constructors are:
727-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
729-- 2. The list of extra 'with' patterns
731-- 3. The right-hand side
733-- 4. The where block (PDecl' t)
735data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
736 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
737 | PClauseR FC [t] t [PDecl' t]
738 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
739 deriving (Functor, Generic)
741deriving instance Binary PClause'
746 -- | Data declaration
747 PDatadecl { d_name :: Name -- ^ The name of the datatype
748 , d_name_fc :: FC -- ^ The precise location of the type constructor name
749 , d_tcon :: t -- ^ Type constructor
750 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
752 -- | "Placeholder" for data whose constructors are defined later
753 | PLaterdecl { d_name :: Name
756 } deriving (Functor, Generic)
758-- | Transform the FCs in a PData and its associated terms. The first
759-- function transforms the general-purpose FCs, and the second
760-- transforms those that are used for semantic source highlighting, so
761-- they can be treated specially.
762mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
763mapPDataFC f g (PDatadecl n nfc tycon ctors) =
764 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
765 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
766 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
767mapPDataFC f g (PLaterdecl n nfc tycon) =
768 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
770deriving instance Binary PData'
773-- Handy to get a free function for applying PTerm -> PTerm functions
774-- across a program, by deriving Functor
776type PDecl = PDecl' PTerm
777type PData = PData' PTerm
778type PClause = PClause' PTerm
780-- | Transform the FCs in a PTerm. The first function transforms the
781-- general-purpose FCs, and the second transforms those that are used
782-- for semantic source highlighting, so they can be treated specially.
783mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
784mapPDeclFC f g (PFix fc fixity ops) =
785 PFix (f fc) fixity ops
786mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
787 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
788mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
789 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
791mapPDeclFC f g (PClauses fc opts n clauses) =
792 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
793mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
794mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
795 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
796mapPDeclFC f g (PParams fc params decls) =
798 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
799 (map (mapPDeclFC f g) decls)
800mapPDeclFC f g (POpenInterfaces fc ifs decls) =
801 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
802mapPDeclFC f g (PNamespace ns fc decls) =
803 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
804mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
805 PRecord doc syn (f fc) opts n (g nfc)
806 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
808 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
809 plic, mapPTermFC f g ty, fdoc))
811 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
814mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
815 PInterface doc syn (f fc)
816 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
817 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
818 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
819 (map (mapPDeclFC f g) body)
820 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
822mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
823 PImplementation doc paramDocs syn (f fc)
824 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
825 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
826 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
827 (mapPTermFC f g implTy)
829 (map (mapPDeclFC f g) body)
830mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
831mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
833 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
834 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
835mapPDeclFC f g (PMutual fc decls) =
836 PMutual (f fc) (map (mapPDeclFC f g) decls)
837mapPDeclFC f g (PDirective d) =
840 DNameHint n nfc ns ->
841 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
842 DErrorHandlers n nfc n' nfc' ns ->
843 DErrorHandlers n (g nfc) n' (g nfc') $
844 map (\(an, anfc) -> (an, g anfc)) ns
845mapPDeclFC f g (PProvider doc syn fc nfc what n) =
846 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
847mapPDeclFC f g (PTransform fc safe l r) =
848 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
849mapPDeclFC f g (PRunElabDecl fc script ns) =
850 PRunElabDecl (f fc) (mapPTermFC f g script) ns
852-- | Get all the names declared in a declaration
853declared :: PDecl -> [Name]
854declared (PFix _ _ _) = []
855declared (PTy _ _ _ _ _ n fc t) = [n]
856declared (PPostulate _ _ _ _ _ _ n t) = [n]
857declared (PClauses _ _ n _) = [] -- not a declaration
858declared (PCAF _ n _) = [n]
859declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
860 where fstt (_, _, a, _, _, _, _) = a
861declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
862declared (PParams _ _ ds) = concatMap declared ds
863declared (POpenInterfaces _ _ ds) = concatMap declared ds
864declared (PNamespace _ _ ds) = concatMap declared ds
865declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
866declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
867declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
871declared (PDSL n _) = [n]
872declared (PSyntax _ _) = []
873declared (PMutual _ ds) = concatMap declared ds
874declared (PDirective _) = []
877-- get the names declared, not counting nested parameter blocks
878tldeclared :: PDecl -> [Name]
879tldeclared (PFix _ _ _) = []
880tldeclared (PTy _ _ _ _ _ n _ t) = [n]
881tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
882tldeclared (PClauses _ _ n _) = [] -- not a declaration
883tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
884tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
885 where fstt (_, _, a, _, _, _, _) = a
886tldeclared (PParams _ _ ds) = []
887tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
888tldeclared (PMutual _ ds) = concatMap tldeclared ds
889tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
890tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
891tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
897defined :: PDecl -> [Name]
898defined (PFix _ _ _) = []
899defined (PTy _ _ _ _ _ n _ t) = []
900defined (PPostulate _ _ _ _ _ _ n t) = []
901defined (PClauses _ _ n _) = [n] -- not a declaration
902defined (PCAF _ n _) = [n]
903defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
904 where fstt (_, _, a, _, _, _, _) = a
905defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
906defined (PParams _ _ ds) = concatMap defined ds
907defined (POpenInterfaces _ _ ds) = concatMap defined ds
908defined (PNamespace _ _ ds) = concatMap defined ds
909defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
910defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
911defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
915defined (PDSL n _) = [n]
916defined (PSyntax _ _) = []
917defined (PMutual _ ds) = concatMap defined ds
918defined (PDirective _) = []
921updateN :: [(Name, Name)] -> Name -> Name
922updateN ns n | Just n' <- lookup n ns = n'
925updateNs :: [(Name, Name)] -> PTerm -> PTerm
927updateNs ns t = mapPT updateRef t
928 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
931-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
933-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
934-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
935-- where updateCNs ns (PClause n l ts r ds)
936-- = PClause (updateN ns n) (fmap (updateNs ns) l)
937-- (map (fmap (updateNs ns)) ts)
938-- (fmap (updateNs ns) r)
939-- (map (updateDNs ns) ds)
945 deriving (Eq, Show, Ord, Data, Typeable, Generic)
947-- | High level language terms
948data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
949 -- high-level language
951 -- ^ A reference to a variable. The FC is its precise
952 -- source location for highlighting. The list of FCs is a
953 -- collection of additional highlighting locations.
954 | PInferRef FC [FC] Name -- ^ A name to be defined later
955 | PPatvar FC Name -- ^ A pattern variable
956 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
957 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
958 | PLet FC RigCount Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
959 | PTyped PTerm PTerm -- ^ Term with explicit type
960 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
961 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
962 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
963 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
964 | PMatchApp FC Name -- ^ Make an application by type matching
965 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
966 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
967 | PTrue FC PunInfo -- ^ Unit type..?
968 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
969 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
970 -- ^ "rewrite" syntax, with optional rewriting function and
971 -- optional result type
972 | PPair FC [FC] PunInfo PTerm PTerm
973 -- ^ A pair (a, b) and whether it's a product type or a
974 -- pair (solved by elaboration). The list of FCs is its
976 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
977 -- ^ A dependent pair (tm : a ** b) and whether it's a
978 -- sigma type or a pair that inhabits one (solved by
979 -- elaboration). The [FC] is its punctuation.
980 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
981 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
982 | PHidden PTerm -- ^ Irrelevant or hidden pattern
983 | PType FC -- ^ 'Type' type
984 | PUniverse FC Universe -- ^ Some universe
985 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
986 | PConstant FC Const -- ^ Builtin types
987 | Placeholder -- ^ Underscore
988 | PDoBlock [PDo] -- ^ Do notation
989 | PIdiom FC PTerm -- ^ Idiom brackets
990 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
991 | PProof [PTactic] -- ^ Proof script
992 | PTactics [PTactic] -- ^ As PProof, but no auto solving
993 | PElabError Err -- ^ Error to report on elaboration
994 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
995 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
996 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
997 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
998 | PNoImplicits PTerm -- ^ never run implicit converions on the term
999 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1000 | PUnquote PTerm -- ^ ~Term
1001 | PQuoteName Name Bool FC
1002 -- ^ `{n} where the FC is the precise highlighting for
1003 -- the name in particular. If the Bool is False, then
1004 -- it's `{{n}} and the name won't be resolved.
1005 | PRunElab FC PTerm [String]
1006 -- ^ %runElab tm - New-style proof script. Args are
1007 -- location, script, enclosing namespace.
1008 | PConstSugar FC PTerm
1009 -- ^ A desugared constant. The FC is a precise source
1010 -- location that will be used to highlight it later.
1011 deriving (Eq, Ord, Data, Typeable, Generic)
1013data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1016 deriving (Eq, Ord, Data, Generic, Typeable)
1018-- | Transform the FCs in a PTerm. The first function transforms the
1019-- general-purpose FCs, and the second transforms those that are used
1020-- for semantic source highlighting, so they can be treated specially.
1021mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1022mapPTermFC f g (PQuote q) = PQuote q
1023mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1024mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1025mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1026mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1027mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1028mapPTermFC f g (PLet fc rc n fc' t1 t2 t3) = PLet (f fc) rc n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1029mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1030mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1031mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1032mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1033mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1034mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1035mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1036mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)
1037mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1038mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1039mapPTermFC f g (PRewrite fc by t1 t2 t3) = PRewrite (f fc) by (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1040mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1041mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1042mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1043mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1044mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1045mapPTermFC f g (PType fc) = PType (f fc)
1046mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1047mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1048mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1049mapPTermFC f g Placeholder = Placeholder
1050mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1051 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1052 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1053 mapPDoFC (DoBindP fc t1 t2 alts) =
1054 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1055 mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1056 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1057 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1058mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1059mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1060mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1061mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1062mapPTermFC f g (PElabError err) = PElabError err
1063mapPTermFC f g PImpossible = PImpossible
1064mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1065mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1066mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1067mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1068mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1069mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1070mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1071mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1072mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1075dg instance Binary PTerm
1078mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1079mapPT f t = f (mpt t) where
1080 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1081 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1082 mpt (PLet fc rc n nfc ty v s) = PLet fc rc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1083 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1084 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1085 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1086 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1087 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1088 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1089 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1090 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1091 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1092 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1093 mpt (PHidden t) = PHidden (mapPT f t)
1094 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1095 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1096 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1097 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1098 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1099 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1100 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1104data PTactic' t = Intro [Name] | Intros | Focus Name
1105 | Refine Name [Bool] | Rewrite t | DoUnify
1112 | LetTac Name t | LetTacTy Name t t
1113 | Exact t | Compute | Trivial | TCImplementation
1114 | ProofSearch Bool Bool Int (Maybe Name)
1115 [Name] -- allowed local names
1117 -- ^ the bool is whether to search recursively
1120 | ProofState | ProofTerm | Undo
1121 | Try (PTactic' t) (PTactic' t)
1122 | TSeq (PTactic' t) (PTactic' t)
1123 | ApplyTactic t -- see Language.Reflection module
1127 | GoalType String (PTactic' t)
1130 | TDocStr (Either Name Const)
1133 | TFail [ErrorReportPart]
1136 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1138deriving instance Binary PTactic'
1140instance Sized a => Sized (PTactic' a) where
1141 size (Intro nms) = 1 + size nms
1143 size (Focus nm) = 1 + size nm
1144 size (Refine nm bs) = 1 + size nm + length bs
1145 size (Rewrite t) = 1 + size t
1146 size (Induction t) = 1 + size t
1147 size (LetTac nm t) = 1 + size nm + size t
1148 size (Exact t) = 1 + size t
1156 size (Try l r) = 1 + size l + size r
1157 size (TSeq l r) = 1 + size l + size r
1158 size (ApplyTactic t) = 1 + size t
1159 size (Reflect t) = 1 + size t
1160 size (Fill t) = 1 + size t
1164 size (TFail ts) = 1 + size ts
1167 size (CaseTac x) = 1 + size x
1168 size (Equiv t) = 1 + size t
1169 size (Claim x y) = 1 + size x + size y
1171 size (MatchRefine x) = 1 + size x
1172 size (LetTacTy x y z) = 1 + size x + size y + size z
1173 size TCImplementation = 1
1175type PTactic = PTactic' PTerm
1177data PDo' t = DoExp FC t
1178 | DoBind FC Name FC t -- ^ second FC is precise name location
1179 | DoBindP FC t t [(t,t)]
1180 | DoLet FC RigCount Name FC t t -- ^ second FC is precise name location
1182 | DoRewrite FC t -- rewrite in do block
1183 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1185deriving instance Binary PDo'
1188instance Sized a => Sized (PDo' a) where
1189 size (DoExp fc t) = 1 + size fc + size t
1190 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1191 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1192 size (DoLet fc rc nm nfc l r) = 1 + size fc + size nm + size l + size r
1193 size (DoLetP fc l r) = 1 + size fc + size l + size r
1194 size (DoRewrite fc h) = 1 + size fc + size h
1196type PDo = PDo' PTerm
1198-- The priority gives a hint as to elaboration order. Best to elaborate
1199-- things early which will help give a more concrete type to other
1200-- variables, e.g. a before (interpTy a).
1202data PArg' t = PImp { priority :: Int
1203 , machine_inf :: Bool -- ^ true if the machine inferred it
1204 , argopts :: [ArgOpt]
1208 | PExp { priority :: Int
1209 , argopts :: [ArgOpt]
1213 | PConstraint { priority :: Int
1214 , argopts :: [ArgOpt]
1218 | PTacImplicit { priority :: Int
1219 , argopts :: [ArgOpt]
1224 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1226data ArgOpt = AlwaysShow
1230 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1232instance Sized a => Sized (PArg' a) where
1233 size (PImp p _ l nm trm) = 1 + size nm + size trm
1234 size (PExp p l nm trm) = 1 + size nm + size trm
1235 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1236 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1239deriving instance Binary PArg'
1242pimp n t mach = PImp 1 mach [] n t
1243pexp t = PExp 1 [] (sMN 0 "arg") t
1244pconst t = PConstraint 1 [] (sMN 0 "carg") t
1245ptacimp n s t = PTacImplicit 2 [] n s t
1247type PArg = PArg' PTerm
1249-- | Get the highest FC in a term, if one exists
1250highestFC :: PTerm -> Maybe FC
1251highestFC (PQuote _) = Nothing
1252highestFC (PRef fc _ _) = Just fc
1253highestFC (PInferRef fc _ _) = Just fc
1254highestFC (PPatvar fc _) = Just fc
1255highestFC (PLam fc _ _ _ _) = Just fc
1256highestFC (PPi _ _ _ _ _) = Nothing
1257highestFC (PLet fc _ _ _ _ _ _) = Just fc
1258highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1259highestFC (PApp fc _ _) = Just fc
1260highestFC (PAppBind fc _ _) = Just fc
1261highestFC (PMatchApp fc _) = Just fc
1262highestFC (PCase fc _ _) = Just fc
1263highestFC (PIfThenElse fc _ _ _) = Just fc
1264highestFC (PTrue fc _) = Just fc
1265highestFC (PResolveTC fc) = Just fc
1266highestFC (PRewrite fc _ _ _ _) = Just fc
1267highestFC (PPair fc _ _ _ _) = Just fc
1268highestFC (PDPair fc _ _ _ _ _) = Just fc
1269highestFC (PAs fc _ _) = Just fc
1270highestFC (PAlternative _ _ args) =
1271 case mapMaybe highestFC args of
1274highestFC (PHidden _) = Nothing
1275highestFC (PType fc) = Just fc
1276highestFC (PUniverse _ _) = Nothing
1277highestFC (PGoal fc _ _ _) = Just fc
1278highestFC (PConstant fc _) = Just fc
1279highestFC Placeholder = Nothing
1280highestFC (PDoBlock lines) =
1281 case map getDoFC lines of
1285 getDoFC (DoExp fc t) = fc
1286 getDoFC (DoBind fc nm nfc t) = fc
1287 getDoFC (DoBindP fc l r alts) = fc
1288 getDoFC (DoLet fc rc nm nfc l r) = fc
1289 getDoFC (DoLetP fc l r) = fc
1290 getDoFC (DoRewrite fc h) = fc
1292highestFC (PIdiom fc _) = Just fc
1293highestFC (PMetavar fc _) = Just fc
1294highestFC (PProof _) = Nothing
1295highestFC (PTactics _) = Nothing
1296highestFC (PElabError _) = Nothing
1297highestFC PImpossible = Nothing
1298highestFC (PCoerced tm) = highestFC tm
1299highestFC (PDisamb _ opts) = highestFC opts
1300highestFC (PUnifyLog tm) = highestFC tm
1301highestFC (PNoImplicits tm) = highestFC tm
1302highestFC (PQuasiquote _ _) = Nothing
1303highestFC (PUnquote tm) = highestFC tm
1304highestFC (PQuoteName _ _ fc) = Just fc
1305highestFC (PRunElab fc _ _) = Just fc
1306highestFC (PConstSugar fc _) = Just fc
1307highestFC (PAppImpl t _) = highestFC t
1311data InterfaceInfo = CI {
1312 implementationCtorName :: Name
1313 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1314 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1315 , interface_default_super_interfaces :: [PDecl]
1316 , interface_impparams :: [Name]
1317 , interface_params :: [Name]
1318 , interface_constraints :: [PTerm]
1319 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1320 , interface_determiners :: [Int]
1321 } deriving (Show, Generic)
1323deriving instance Binary InterfaceInfo
1327data RecordInfo = RI {
1328 record_parameters :: [(Name,PTerm)]
1329 , record_constructor :: Name
1330 , record_projections :: [Name]
1331 } deriving (Show, Generic)
1333-- Type inference data
1335data TIData = TIPartial -- ^ a function with a partially defined type
1336 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1337 deriving (Show, Generic)
1339-- | Miscellaneous information about functions
1340data FnInfo = FnInfo { fn_params :: [Int] }
1341 deriving (Show, Generic)
1343deriving instance Binary FnInfo
1346data OptInfo = Optimise {
1347 inaccessible :: [(Int,Name)] -- includes names for error reporting
1348 , detaggable :: Bool
1349 , forceable :: [Int] -- argument positions which are forced by other values
1350 } deriving (Show, Generic)
1352deriving instance Binary OptInfo
1355-- | Syntactic sugar info
1360 , dsl_var :: Maybe t
1361 , index_first :: Maybe t
1362 , index_next :: Maybe t
1363 , dsl_lambda :: Maybe t
1364 , dsl_let :: Maybe t
1366 } deriving (Show, Functor, Generic)
1368deriving instance Binary DSL'
1371type DSL = DSL' PTerm
1373data SynContext = PatternSyntax
1376 deriving (Show, Generic)
1378deriving instance Binary SynContext
1381data Syntax = Rule [SSymbol] PTerm SynContext
1382 | DeclRule [SSymbol] [PDecl]
1383 deriving (Show, Generic)
1385syntaxNames :: Syntax -> [Name]
1386syntaxNames (Rule syms _ _) = mapMaybe ename syms
1387 where ename (Keyword n) = Just n
1389syntaxNames (DeclRule syms _) = mapMaybe ename syms
1390 where ename (Keyword n) = Just n
1393syntaxSymbols :: Syntax -> [SSymbol]
1394syntaxSymbols (Rule ss _ _) = ss
1395syntaxSymbols (DeclRule ss _) = ss
1397deriving instance Binary Syntax
1400data SSymbol = Keyword Name
1405 deriving (Show, Eq, Generic)
1409deriving instance Binary SSymbol
1412newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1415emptySyntaxRules :: SyntaxRules
1416emptySyntaxRules = SyntaxRules []
1418updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1419updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1421 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1426 ruleSort (s1:ss1) (s2:ss2) =
1427 case symCompare s1 s2 of
1428 EQ -> ruleSort ss1 ss2
1431 -- Better than creating Ord implementation for SSymbol since
1432 -- in general this ordering does not really make sense.
1433 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1434 symCompare (Keyword _) _ = LT
1435 symCompare (Symbol _) (Keyword _) = GT
1436 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1437 symCompare (Symbol _) _ = LT
1438 symCompare (Binding _) (Keyword _) = GT
1439 symCompare (Binding _) (Symbol _) = GT
1440 symCompare (Binding b1) (Binding b2) = compare b1 b2
1441 symCompare (Binding _) _ = LT
1442 symCompare (Expr _) (Keyword _) = GT
1443 symCompare (Expr _) (Symbol _) = GT
1444 symCompare (Expr _) (Binding _) = GT
1445 symCompare (Expr e1) (Expr e2) = compare e1 e2
1446 symCompare (Expr _) _ = LT
1447 symCompare (SimpleExpr _) (Keyword _) = GT
1448 symCompare (SimpleExpr _) (Symbol _) = GT
1449 symCompare (SimpleExpr _) (Binding _) = GT
1450 symCompare (SimpleExpr _) (Expr _) = GT
1451 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1453initDSL = DSL (PRef f [] (sUN ">>="))
1454 (PRef f [] (sUN "<*>"))
1455 (PRef f [] (sUN "pure"))
1462 where f = fileFC "(builtin)"
1464data Using = UImplicit Name PTerm
1465 | UConstraint Name [Name]
1466 deriving (Show, Eq, Data, Generic, Typeable)
1468deriving instance Binary Using
1471data SyntaxInfo = Syn {
1473 , syn_params :: [(Name, PTerm)]
1474 , syn_namespace :: [String]
1476 , imp_methods :: [Name]
1477 -- ^ interface methods. When expanding implicits, these should be
1478 -- expanded even under binders
1479 , decoration :: Name -> Name
1481 , implicitAllowed :: Bool
1482 , constraintAllowed :: Bool
1483 , maxline :: Maybe Int
1484 , mut_nesting :: Int
1486 , syn_in_quasiquote :: Int
1487 , syn_toplevel :: Bool
1488 , withAppAllowed :: Bool
1489 } deriving (Show, Generic)
1491deriving instance Binary SyntaxInfo
1494defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1496expandNS :: SyntaxInfo -> Name -> Name
1497expandNS syn n@(NS _ _) = n
1498expandNS syn n = case syn_namespace syn of
1503-- For inferring types of things
1505bi = fileFC "builtin"
1506primfc = fileFC "(primitive)"
1508inferTy = sMN 0 "__Infer"
1509inferCon = sMN 0 "__infer"
1510inferDecl = PDatadecl inferTy primfc
1512 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1513 PPi expl_linear (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1514 (PRef bi [] inferTy)), bi, [])]
1517infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1518infP = P (TCon 6 0) inferTy (TType (UVal 0))
1520getInferTerm, getInferType :: Term -> Term
1521getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1522getInferTerm (App _ (App _ _ _) tm) = tm
1523getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1525getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1526 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1527 toTy (PVar _ t) = PVTy t
1529getInferType (App _ (App _ _ ty) _) = ty
1533-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1535primNames = [inferTy, inferCon]
1538unitCon = sUN "MkUnit"
1540falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1541 "The empty type, also known as the trivially false proposition." ++
1543 "Use `void` or `absurd` to prove anything if you have a variable " ++
1544 "of type `Void` in scope."
1547pairTy = sNS (sUN "Pair") ["Builtins"]
1548pairCon = sNS (sUN "MkPair") ["Builtins"]
1550upairTy = sNS (sUN "UPair") ["Builtins"]
1551upairCon = sNS (sUN "MkUPair") ["Builtins"]
1555eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1556 "The propositional equality type. A proof that `x` = `y`." ++
1558 "To use such a proof, pattern-match on it, and the two equal things will " ++
1559 "then need to be the _same_ pattern." ++
1561 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1562 "is possible to state equalities between values of potentially different " ++
1563 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1565 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1567eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1568 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1570 [(reflDoc, reflParamDoc,
1571 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1572 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1573 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1574 pimp (n "B") Placeholder False,
1575 pexp (PRef bi [] (n "x")),
1576 pexp (PRef bi [] (n "x"))])), bi, [])]
1578 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1579 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1580 "shown that both sides are in fact equal."
1581 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1582 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1584eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1585 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1591-- | The special name to be used in the module documentation context -
1592-- not for use in the main definition context. The namespace around it
1593-- will determine the module to which the docs adhere.
1595modDocName = sMN 0 "ModuleDocs"
1597-- Defined in builtins.idr
1598sigmaTy = sNS (sUN "DPair") ["Builtins"]
1599sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1601piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1602piBind = piBindp expl
1604piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1606piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1609-- Pretty-printing declarations and terms
1611-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1612-- could interfere with interactive editing, which calls "show".
1614instance Show PTerm where
1615 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1617instance Show PDecl where
1618 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1620instance Show PClause where
1621 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1623instance Show PData where
1624 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1626instance Pretty PTerm OutputAnnotation where
1627 pretty = prettyImp defaultPPOption
1629-- | Colourise annotations according to an Idris state. It ignores the
1630-- names in the annotation, as there's no good way to show extended
1631-- information on a terminal.
1632annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1633annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1634annotationColour ist (AnnConst c) =
1635 let theme = idris_colourTheme ist
1636 in Just $ if constIsType c
1637 then typeColour theme
1638 else dataColour theme
1639annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1640annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1641annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1642annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1643annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1644annotationColour ist (AnnName n _ _ _) =
1645 let ctxt = tt_ctxt ist
1646 theme = idris_colourTheme ist
1648 _ | isDConName n ctxt -> Just $ dataColour theme
1649 _ | isFnName n ctxt -> Just $ functionColour theme
1650 _ | isTConName n ctxt -> Just $ typeColour theme
1651 _ | isPostulateName n ist -> Just $ postulateColour theme
1652 _ | otherwise -> Nothing -- don't colourise unknown names
1653annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1654 where colour BoldText = IdrisColour Nothing True False True False
1655 colour UnderlineText = IdrisColour Nothing True True False False
1656 colour ItalicText = IdrisColour Nothing True False False True
1657annotationColour ist _ = Nothing
1660-- | Colourise annotations according to an Idris state. It ignores the
1661-- names in the annotation, as there's no good way to show extended
1662-- information on a terminal. Note that strings produced this way will
1663-- not be coloured on Windows, so the use of the colour rendering
1664-- functions in Idris.Output is to be preferred.
1665consoleDecorate :: IState -> OutputAnnotation -> String -> String
1666consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1668isPostulateName :: Name -> IState -> Bool
1669isPostulateName n ist = S.member n (idris_postulates ist)
1671-- | Pretty-print a high-level closed Idris term with no information
1672-- about precedence/associativity
1673prettyImp :: PPOption -- ^ pretty printing options
1674 -> PTerm -- ^ the term to pretty-print
1675 -> Doc OutputAnnotation
1676prettyImp impl = pprintPTerm impl [] [] []
1678-- | Serialise something to base64 using its Binary implementation.
1680-- | Do the right thing for rendering a term in an IState
1681prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1682prettyIst ist = pprintPTerm opt [] [] (idris_infixes ist)
1684 opt = if LinearTypes `elem` idris_language_extensions ist
1685 then (ppOptionIst ist) { ppopt_displayrig = True }
1686 else ppOptionIst ist
1688-- | Pretty-print a high-level Idris term in some bindings context
1690pprintPTerm :: PPOption -- ^ pretty printing options
1691 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1692 -> [Name] -- ^ names to always show in pi, even if not used
1693 -> [FixDecl] -- ^ Fixity declarations
1694 -> PTerm -- ^ the term to pretty-print
1695 -> Doc OutputAnnotation
1696pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1700 lbrace = annotate (AnnSyntax "{") (text "{")
1701 rbrace = annotate (AnnSyntax "}") (text "}")
1702 percent = annotate (AnnSyntax "%") (text "%")
1704 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1705 prettySe d p bnd (PQuote r) =
1706 text "![" <> pretty r <> text "]"
1707 prettySe d p bnd (PPatvar fc n) = pretty n
1709 | Just str <- slist d p bnd e = depth d str
1710 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1711 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1712 prettySe d p bnd (PLam fc n nfc ty sc) =
1713 let (ns, sc') = getLamNames [n] sc in
1714 depth d . bracket p startPrec . group . align . hang 2 $
1715 (annotate (AnnSyntax "\\") (text "\\"))
1716 <> prettyBindingsOf ns False <+> text "=>" <$>
1717 prettySe (decD d) startPrec ((n, False):bnd) sc'
1719 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1720 getLamNames acc sc = (reverse acc, sc)
1722 prettyBindingsOf [] t = text ""
1723 prettyBindingsOf [n] t = prettyBindingOf n t
1724 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1725 prettyBindingsOf ns t
1726 prettySe d p bnd (PLet fc rc n nfc ty v sc) =
1727 depth d . bracket p startPrec . group . align $
1728 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1729 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1730 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1731 | Rig0 <- rig, ppopt_displayrig ppo =
1732 depth d . bracket p startPrec . group $
1733 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1734 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1735 | Rig1 <- rig, ppopt_displayrig ppo =
1736 depth d . bracket p startPrec . group $
1737 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1738 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1739 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1740 || ppopt_pinames ppo && uname n =
1741 depth d . bracket p startPrec . group $
1742 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1743 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1745 depth d . bracket p startPrec . group $
1746 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1747 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1749 uname (UN n) = case str n of
1756 Static -> percent <> text "static" <> space
1758 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1760 depth d . bracket p startPrec $
1761 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1762 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1763 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1764 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1766 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1767 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1768 showRig _ n = prettyBindingOf n True
1770 isPi (PPi (Exp{}) _ _ _ _) = True
1771 isPi (PPi _ _ _ _ sc) = isPi sc
1776 Static -> percent <> text "static" <> space
1778 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1779 depth d . bracket p startPrec $
1780 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1781 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1782 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1783 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1784 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1785 depth d . bracket p startPrec $
1786 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1787 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1788 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1789 | basename neg == sUN "negate" =
1790 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1791 -- This case preserves the behavior of the former constructor PEq.
1792 -- It should be removed if feasible when the pretty-printing of infix
1793 -- operators in general is improved.
1794 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1795 | n == eqTy, ppopt_impl ppo =
1796 depth d . bracket p eqPrec $
1797 enclose lparen rparen eq <+>
1798 align (group (vsep (map (prettyArgS (decD d) bnd)
1801 depth d . bracket p eqPrec . align . group $
1802 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1803 where eq = annName eqTy (text "=")
1805 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1806 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1807 | UN nm <- basename f
1808 , not (ppopt_impl ppo) && null (getShowArgs args) =
1809 prettyName True (ppopt_impl ppo) bnd f
1810 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1811 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1812 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1813 | UN nm <- basename op
1815 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1816 case getShowArgs args of
1818 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1819 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1820 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1821 (l@(PExp{}) : r@(PExp{}) : rest) ->
1822 depth d . bracket p funcAppPrec $
1823 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1824 align (group (vsep (map (prettyArgS d bnd) rest)))
1825 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1826 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1827 f = getFixity (opStr op)
1829 Nothing -> funcAppPrec + 1
1830 Just (Infixl p') -> p'
1831 Just f' -> prec f' + 1
1833 Nothing -> funcAppPrec + 1
1834 Just (Infixr p') -> p'
1835 Just f' -> prec f' + 1
1836 inFix l r = align . group $
1837 (prettySe (decD d) left bnd l <+> opName False) <$>
1838 group (prettySe (decD d) right bnd r)
1839 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1840 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1841 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1842 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1843 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1844 let args = getShowArgs as
1845 fp = prettySe (decD d) (startPrec + 1) bnd f
1846 shownArgs = if ppopt_impl ppo then as else args
1848 depth d . bracket p funcAppPrec . group $
1851 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1852 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1853 prettySe d p bnd (PCase _ scr cases) =
1854 bracket p funcAppPrec $
1855 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1856 depth d (indent 2 (vsep (map ppcase cases)))
1858 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1859 ([(n, False) | n <- vars l] ++ bnd)
1860 in nest nestingSize $
1861 prettyCase l <+> text "=>" <+> prettyCase r
1862 -- Warning: this is a bit of a hack. At this stage, we don't have the
1863 -- global context, so we can't determine which names are constructors,
1864 -- which are types, and which are pattern variables on the LHS of the
1865 -- case pattern. We use the heuristic that names without a namespace
1866 -- are patvars, because right now case blocks in PTerms are always
1867 -- delaborated from TT before being sent to the pretty-printer. If they
1868 -- start getting printed directly, THIS WILL BREAK.
1869 -- Potential solution: add a list of known patvars to the cases in
1870 -- PCase, and have the delaborator fill it out, kind of like the pun
1871 -- disambiguation on PDPair.
1872 vars tm = filter noNS (allNamesIn tm)
1873 noNS (NS _ _) = False
1876 prettySe d p bnd (PIfThenElse _ c t f) =
1877 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1878 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1879 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1880 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1882 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1883 prettySe d p bnd (PResolveTC _) = percent <> kwd "implementation"
1884 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1885 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1886 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1887 prettySe d p bnd (PRewrite _ by l r _) =
1888 depth d . bracket p startPrec $
1889 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1892 Just fn -> text "using" <+>
1893 prettyName True (ppopt_impl ppo) bnd fn) <+>
1894 text "in" <+> prettySe (decD d) startPrec bnd r
1895 prettySe d p bnd (PTyped l r) =
1896 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1897 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1898 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1899 align . group . vsep . punctuate (ann comma) $
1900 map (prettySe (decD d) startPrec bnd) elts
1901 where ann = case pun of
1903 IsType -> annName pairTy
1904 IsTerm -> annName pairCon
1905 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1906 | Just elts <- dPairElts dpair
1907 = depth d . enclose (annotated lparen) (annotated rparen) .
1908 align . group . vsep . punctuate (space <> annotated (text "**")) $
1914 annotated (text "**") <+>
1915 prettySe (decD d) startPrec (addBinding bnd) r <>
1917 where annotated = case pun of
1918 IsType -> annName sigmaTy
1919 IsTerm -> annName sigmaCon
1922 (left, addBinding) = case (l, pun) of
1923 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1924 _ -> (prettySe (decD d) startPrec bnd l, id)
1927 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1928 ppElts ((PRef _ _ n, t):rs) bs
1930 = (bindingOf n False <+> colon <+>
1931 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1932 ppElts ((l, t):rs) bs
1933 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1934 prettySe d p bnd (PAlternative ns a as) =
1935 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1938 foldr ((\ l r -> l <+> text "," <+> r) .
1939 depth d . prettySe (decD d) startPrec bnd)
1941 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1942 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1943 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1944 -- XXX: add pretty for tactics
1945 prettySe d p bnd (PProof ts) =
1946 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1947 prettySe d p bnd (PTactics ts) =
1948 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1949 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1950 prettySe d p bnd PImpossible = kwd "impossible"
1951 prettySe d p bnd Placeholder = text "_"
1952 prettySe d p bnd (PDoBlock dos) =
1953 bracket p startPrec $
1954 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1955 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1956 ppdo bnd (DoBind _ bn _ tm : dos) =
1957 (prettyBindingOf bn False <+> text "<-" <+>
1958 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1959 ppdo ((bn, False):bnd) dos
1960 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1961 text "no pretty printer for pattern-matching do binding" :
1963 ppdo bnd (DoLet _ _ ln _ ty v : dos) =
1964 (kwd "let" <+> prettyBindingOf ln False <+>
1965 (if ty /= Placeholder
1966 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1968 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1969 ppdo ((ln, False):bnd) dos
1970 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1971 text "no pretty printer for pattern-matching do binding" :
1973 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1974 text "no pretty printer for pattern-matching do binding" :
1977 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1978 prettySe d p bnd (PElabError s) = pretty s
1979 -- Quasiquote pprinting ignores bound vars
1980 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1981 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1982 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1983 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1984 where start = if res then "`{" else "`{{"
1985 end = if res then "}" else "}}"
1986 prettySe d p bnd (PRunElab _ tm _) =
1987 bracket p funcAppPrec . group . align . hang 2 $
1988 (percent <> text "runElab") <$>
1989 prettySe (decD d) funcAppPrec bnd tm
1990 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1991 prettySe d p bnd _ = text "missing pretty-printer for term"
1993 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1994 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1995 where display (UN n) = T.unpack n
1996 display (MN _ n) = T.unpack n
1997 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1998 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2001 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2002 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2003 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2004 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2006 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2007 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2008 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2009 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2011 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2012 annName n = annotate (AnnName n Nothing Nothing Nothing)
2014 opStr :: Name -> String
2015 opStr (NS n _) = opStr n
2016 opStr (UN n) = T.unpack n
2018 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2019 slist' (Just d) _ _ _ | d <= 0 = Nothing
2021 | containsHole e = Nothing
2022 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2023 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2024 slist' d p bnd (PRef _ _ nil)
2025 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2026 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2027 | nsroot cons == sUN "::",
2028 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2030 Just tl' <- slist' (decD d) p bnd tl
2031 = Just (prettySe d startPrec bnd hd : tl')
2033 isImp (PImp {}) = True
2035 slist' _ _ _ tm = Nothing
2037 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2039 [] -> annotate (AnnData "" "") $ text "[]"
2040 [x] -> enclose left right . group $ x
2041 xs -> enclose left right .
2042 align . group . vsep .
2043 punctuate comma $ xs
2044 where left = (annotate (AnnData "" "") (text "["))
2045 right = (annotate (AnnData "" "") (text "]"))
2046 comma = (annotate (AnnData "" "") (text ","))
2047 slist _ _ _ _ = Nothing
2049 pairElts :: PTerm -> Maybe [PTerm]
2050 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2051 | otherwise = Just [x, y]
2052 pairElts _ = Nothing
2054 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2055 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2056 | otherwise = Just [(l, t), (Placeholder, r)]
2057 dPairElts _ = Nothing
2059 natns = "Prelude.Nat."
2061 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2063 | ppopt_desugarnats ppo = Nothing
2064 | otherwise = snat' d p e
2066 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2067 snat' (Just x) _ _ | x <= 0 = Nothing
2068 snat' d p (PRef _ _ z)
2069 | show z == (natns++"Z") || show z == "Z" = Just 0
2070 snat' d p (PApp _ s [PExp {getTm=n}])
2071 | show s == (natns++"S") || show s == "S",
2072 Just n' <- snat' (decD d) p n
2074 snat' _ _ _ = Nothing
2076 bracket outer inner doc
2077 | outer > inner = lparen <> doc <> rparen
2080 ellipsis = text "..."
2083 depth (Just d) = if d <= 0 then const ellipsis else id
2085 decD = fmap (\x -> x - 1)
2087 kwd = annotate AnnKeyword . text
2089 fixities :: M.Map String Fixity
2090 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2092 getFixity :: String -> Maybe Fixity
2093 getFixity = flip M.lookup fixities
2095-- | Strip away namespace information
2096basename :: Name -> Name
2097basename (NS n _) = basename n
2100-- | Determine whether a name was the one inserted for a hole or guess
2101-- by the delaborator
2102isHoleName :: Name -> Bool
2103isHoleName (UN n) = n == T.pack "[__]"
2106-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2107containsHole :: PTerm -> Bool
2108containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2110-- | Pretty-printer helper for names that attaches the correct annotations
2111prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2112 -> Bool -- ^ whether to show namespaces
2113 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2114 -> Name -- ^ the name to pprint
2115 -> Doc OutputAnnotation
2116prettyName infixParen showNS bnd n
2117 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2118 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2119 | (UN n') <- n, T.unpack n' == "_" = text "_"
2120 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2121 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2122 where fullName = text nameSpace <> parenthesise (text (baseName n))
2123 baseName (UN n) = T.unpack n
2124 baseName (NS n ns) = baseName n
2125 baseName (MN i s) = T.unpack s
2126 baseName other = show other
2127 nameSpace = case n of
2128 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2130 isInfix = case baseName n of
2132 (c : _) -> not (isAlpha c)
2133 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2136showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2137showCImp ppo (PClause _ n l ws r w)
2138 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2139 <+> text "where" <+> text (show w)
2142 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2143showCImp ppo (PWith _ n l ws r pn w)
2144 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2145 <+> braces (text (show w))
2148 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2151showDImp :: PPOption -> PData -> Doc OutputAnnotation
2152showDImp ppo (PDatadecl n nfc ty cons)
2153 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2154 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2156showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2157showDecls o ds = vsep (map (showDeclImp o) ds)
2159showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2160showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2161showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2162 indent 2 (vsep (map (showCImp o) cs))
2163showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2164showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2165showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2166showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2167showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2168showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2169 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2170showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2171 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2172showDeclImp _ _ = text "..."
2173-- showDeclImp (PImport o) = "import " ++ o
2175getImps :: [PArg] -> [(Name, PTerm)]
2177getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2178getImps (_ : xs) = getImps xs
2180getExps :: [PArg] -> [PTerm]
2182getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2183getExps (_ : xs) = getExps xs
2185getShowArgs :: [PArg] -> [PArg]
2187getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2188getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2189 | PImp _ _ _ _ tm <- e
2190 , containsHole tm = e : getShowArgs xs
2191getShowArgs (_ : xs) = getShowArgs xs
2193getConsts :: [PArg] -> [PTerm]
2195getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2196getConsts (_ : xs) = getConsts xs
2198getAll :: [PArg] -> [PTerm]
2203showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2204 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2205 -> PPOption -- ^ pretty printing options
2206 -> Bool -- ^ whether to colourise
2207 -> Name -- ^ the term to show
2209showName ist bnd ppo colour n = case ist of
2210 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2211 Nothing -> showbasic n
2212 where name = if ppopt_impl ppo then show n else showbasic n
2213 showbasic n@(UN _) = showCG n
2214 showbasic (MN i s) = str s
2215 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2216 showbasic (SN s) = show s
2217 colourise n t = let ctxt' = fmap tt_ctxt ist in
2220 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2221 else colouriseBound t name
2222 | isDConName n ctxt -> colouriseData t name
2223 | isFnName n ctxt -> colouriseFun t name
2224 | isTConName n ctxt -> colouriseType t name
2225 -- The assumption is that if a name is not bound and does not exist in the
2226 -- global context, then we're somewhere in which implicit info has been lost
2227 -- (like error messages). Thus, unknown vars are colourised as implicits.
2228 | otherwise -> colouriseImplicit t name
2230showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2231 -> PTerm -- ^ the term to show
2233showTm ist = displayDecorated (consoleDecorate ist) .
2234 renderPretty 0.8 100000 .
2235 prettyImp (ppOptionIst ist)
2237-- | Show a term with implicits, no colours
2238showTmImpls :: PTerm -> String
2239showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2241-- | Show a term with specific options
2242showTmOpts :: PPOption -> PTerm -> String
2243showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2246instance Sized PTerm where
2247 size (PQuote rawTerm) = size rawTerm
2248 size (PRef fc _ name) = size name
2249 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2250 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2251 size (PLet fc _ name nfc ty def bdy) = 1 + size ty + size def + size bdy
2252 size (PTyped trm ty) = 1 + size trm + size ty
2253 size (PApp fc name args) = 1 + size args
2254 size (PAppBind fc name args) = 1 + size args
2255 size (PCase fc trm bdy) = 1 + size trm + size bdy
2256 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2257 size (PTrue fc _) = 1
2258 size (PResolveTC fc) = 1
2259 size (PRewrite fc by left right _) = 1 + size left + size right
2260 size (PPair fc _ _ left right) = 1 + size left + size right
2261 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2262 size (PAlternative _ a alts) = 1 + size alts
2263 size (PHidden hidden) = size hidden
2264 size (PUnifyLog tm) = size tm
2265 size (PDisamb _ tm) = size tm
2266 size (PNoImplicits tm) = size tm
2268 size (PUniverse _ _) = 1
2269 size (PConstant fc const) = 1 + size fc + size const
2270 size Placeholder = 1
2271 size (PDoBlock dos) = 1 + size dos
2272 size (PIdiom fc term) = 1 + size term
2273 size (PMetavar _ name) = 1
2274 size (PProof tactics) = size tactics
2275 size (PElabError err) = size err
2276 size PImpossible = 1
2279getPArity :: PTerm -> Int
2280getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2283-- Return all names, free or globally bound, in the given term.
2285allNamesIn :: PTerm -> [Name]
2286allNamesIn tm = nub $ ni 0 [] tm
2287 where -- TODO THINK added niTacImp, but is it right?
2288 ni 0 env (PRef _ _ n)
2289 | not (n `elem` env) = [n]
2290 ni 0 env (PPatvar _ n) = [n]
2291 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2292 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2293 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2294 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2295 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2296 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2297 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2298 ni 0 env (PHidden tm) = ni 0 env tm
2299 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2300 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2301 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2302 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2303 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2304 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2305 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2306 ni 0 env (PUnifyLog tm) = ni 0 env tm
2307 ni 0 env (PDisamb _ tm) = ni 0 env tm
2308 ni 0 env (PNoImplicits tm) = ni 0 env tm
2310 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2311 ni i env (PUnquote tm) = ni (i - 1) env tm
2312 ni i env tm = concatMap (ni i env) (children tm)
2314 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2318-- Return all names defined in binders in the given term
2319boundNamesIn :: PTerm -> [Name]
2320boundNamesIn tm = S.toList (ni 0 S.empty tm)
2321 where -- TODO THINK Added niTacImp, but is it right?
2322 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2323 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2324 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2325 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2326 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2327 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2328 ni 0 set (PLet fc rc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2329 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2330 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2331 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2332 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2333 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2334 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2335 ni 0 set (PAlternative ns a as) = niTms 0 set as
2336 ni 0 set (PHidden tm) = ni 0 set tm
2337 ni 0 set (PUnifyLog tm) = ni 0 set tm
2338 ni 0 set (PDisamb _ tm) = ni 0 set tm
2339 ni 0 set (PNoImplicits tm) = ni 0 set tm
2341 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2342 ni i set (PUnquote tm) = ni (i - 1) set tm
2344 ni i set tm = foldr (S.union . ni i set) set (children tm)
2346 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2347 niTms i set [] = set
2348 niTms i set (x : xs) = niTms i (ni i set x) xs
2350 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2351 niTacImp i set _ = set
2353-- Return names which are valid implicits in the given term (type).
2354implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2355implicitNamesIn uvars ist tm
2356 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2359 addImp n = do (imps, fns) <- get
2361 addFn n = do (imps, fns) <- get
2364 ni 0 env (PRef _ _ n@(NS _ _))
2365 | not (n `elem` env)
2366 -- Never implicitly bind if there's a namespace
2368 ni 0 env (PRef _ _ n)
2369 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2370 ni 0 env (PApp _ f@(PRef _ _ n) as)
2371 | n `elem` uvars = do ni 0 env f
2372 mapM_ (ni 0 env . getTm) as
2373 | otherwise = do case lookupTy n (tt_ctxt ist) of
2376 mapM_ (ni 0 env . getTm) as
2377 ni 0 env (PApp _ f as) = do ni 0 env f
2378 mapM_ (ni 0 env . getTm) as
2379 ni 0 env (PAppBind _ f as) = do ni 0 env f
2380 mapM_ (ni 0 env . getTm) as
2381 ni 0 env (PCase _ c os) = do ni 0 env c
2382 -- names in 'os', not counting the names bound in the cases
2383 mapM_ (ni 0 env . snd) os
2386 mapM_ (ni 0 env . fst) os
2388 put (nub imps \\ nub impsfst, fns)
2389 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2390 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2391 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2392 ni 0 env (PLet fc rc n _ ty val sc) = do ni 0 env ty;
2393 ni 0 env val; ni 0 (n:env) sc
2394 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2395 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2396 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2397 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2398 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2401 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2402 ni 0 env (PHidden tm) = ni 0 env tm
2403 ni 0 env (PUnifyLog tm) = ni 0 env tm
2404 ni 0 env (PDisamb _ tm) = ni 0 env tm
2405 ni 0 env (PNoImplicits tm) = ni 0 env tm
2407 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2408 maybe (return ()) (ni i env) ty
2409 ni i env (PUnquote tm) = ni (i - 1) env tm
2411 ni i env tm = mapM_ (ni i env) (children tm)
2413-- Return names which are free in the given term.
2414namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2415namesIn uvars ist tm = nub $ ni 0 [] tm
2417 ni 0 env (PRef _ _ n)
2418 | not (n `elem` env)
2419 = case lookupTy n (tt_ctxt ist) of
2421 _ -> [n | n `elem` (map fst uvars)]
2422 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2423 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2424 ni 0 env (PCase _ c os) = ni 0 env c ++
2425 -- names in 'os', not counting the names bound in the cases
2426 (nub (concatMap (ni 0 env . snd) os)
2427 \\ nub (concatMap (ni 0 env . fst) os))
2428 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2429 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2430 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2431 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2432 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2433 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2434 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2435 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2436 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2437 ni 0 env (PHidden tm) = ni 0 env tm
2438 ni 0 env (PUnifyLog tm) = ni 0 env tm
2439 ni 0 env (PDisamb _ tm) = ni 0 env tm
2440 ni 0 env (PNoImplicits tm) = ni 0 env tm
2442 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2443 ni i env (PUnquote tm) = ni (i - 1) env tm
2445 ni i env tm = concatMap (ni i env) (children tm)
2447 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2450-- Return which of the given names are used in the given term.
2452usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2453usedNamesIn vars ist tm = nub $ ni 0 [] tm
2454 where -- TODO THINK added niTacImp, but is it right?
2455 ni 0 env (PRef _ _ n)
2456 | n `elem` vars && not (n `elem` env)
2457 = case lookupDefExact n (tt_ctxt ist) of
2460 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2461 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2462 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2463 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2464 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2465 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2466 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2467 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2468 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2469 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2470 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2471 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2472 ni 0 env (PHidden tm) = ni 0 env tm
2473 ni 0 env (PUnifyLog tm) = ni 0 env tm
2474 ni 0 env (PDisamb _ tm) = ni 0 env tm
2475 ni 0 env (PNoImplicits tm) = ni 0 env tm
2477 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2478 ni i env (PUnquote tm) = ni (i - 1) env tm
2480 ni i env tm = concatMap (ni i env) (children tm)
2482 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2485-- Return the list of inaccessible (= dotted) positions for a name.
2486getErasureInfo :: IState -> Name -> [Int]
2487getErasureInfo ist n =
2488 case lookupCtxtExact n (idris_optimisation ist) of
2489 Just (Optimise inacc _ _) -> map fst inacc
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list