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
153defaultOptimise :: [Optimisation]
156-- | Pretty printing options with default verbosity.
157defaultPPOption :: PPOption
158defaultPPOption = PPOption {
160 , ppopt_desugarnats = False
161 , ppopt_pinames = False
162 , ppopt_depth = Nothing
165-- | Pretty printing options with the most verbosity.
166verbosePPOption :: PPOption
167verbosePPOption = PPOption {
169 , ppopt_desugarnats = True
170 , ppopt_pinames = True
171 , ppopt_depth = Nothing
174-- | Get pretty printing options from the big options record.
175ppOption :: IOption -> PPOption
176ppOption opt = PPOption {
177 ppopt_impl = opt_showimp opt
178 , ppopt_pinames = False
179 , ppopt_depth = opt_printdepth opt
180 , ppopt_desugarnats = opt_desugarnats opt
183-- | Get pretty printing options from an idris state record.
184ppOptionIst :: IState -> PPOption
185ppOptionIst = ppOption . idris_options
188-- | The output mode in use
189data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
190 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
194-- | If a function has no totality annotation, what do we assume?
195data DefaultTotality = DefaultCheckingTotal -- ^ Total
196 | DefaultCheckingPartial -- ^ Partial
197 | DefaultCheckingCovering -- ^Total coverage, but may diverge
198 deriving (Show, Eq, Generic)
200-- | Configuration options for interactive editing.
201data InteractiveOpts = InteractiveOpts {
202 interactiveOpts_indentWith :: Int
203 , interactiveOpts_indentClause :: Int
204} deriving (Show, Generic)
206-- | The global state used in the Idris monad
207data IState = IState {
208 tt_ctxt :: Context -- ^ All the currently defined names and their terms
209 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
210 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
211 , idris_implicits :: Ctxt [PArg]
212 , idris_statics :: Ctxt [Bool]
213 , idris_interfaces :: Ctxt InterfaceInfo
214 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
215 , idris_records :: Ctxt RecordInfo
216 , idris_dsls :: Ctxt DSL
217 , idris_optimisation :: Ctxt OptInfo
218 , idris_datatypes :: Ctxt TypeInfo
219 , idris_namehints :: Ctxt [Name]
221 -- | list of lhs/rhs, and a list of missing clauses. These are not
223 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
224 , idris_flags :: Ctxt [FnOpt]
225 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
226 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
228 -- | module documentation is saved in a special MN so the context
229 -- mechanism can be used for disambiguation.
230 , idris_moduledocs :: Ctxt (Docstring DocTerm)
231 , idris_tyinfodata :: Ctxt TIData
232 , idris_fninfo :: Ctxt FnInfo
233 , idris_transforms :: Ctxt [(Term, Term)]
234 , idris_autohints :: Ctxt [Name]
235 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
236 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
237 , idris_totcheckfail :: [(FC, String)]
238 , idris_options :: IOption
240 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
242 -- | The currently defined but not proven metavariables. The Int is
243 -- the number of vars to display as a context, the Maybe Name is its
244 -- top-level function, the [Name] is the list of local variables
245 -- available for proof search and the Bools are whether :p is
246 -- allowed, and whether the variable is definable at all
247 -- (Metavariables are not definable if they are applied in a term
248 -- which still has hole bindings)
249 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
250 , idris_coercions :: [Name]
251 , idris_errRev :: [(Term, Term)]
252 , idris_errReduce :: [Name]
253 , syntax_rules :: SyntaxRules
254 , syntax_keywords :: [String]
255 , imported :: [FilePath] -- ^ The imported modules
256 , idris_scprims :: [(Name, (Int, PrimFn))]
257 , idris_objs :: [(Codegen, FilePath)]
258 , idris_libs :: [(Codegen, String)]
259 , idris_cgflags :: [(Codegen, String)]
260 , idris_hdrs :: [(Codegen, String)]
261 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
262 , proof_list :: [(Name, (Bool, [String]))]
263 , errSpan :: Maybe FC
264 , parserWarnings :: [(FC, Err)]
265 , lastParse :: Maybe Name
266 , indent_stack :: [Int]
267 , brace_stack :: [Maybe Int]
268 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
269 , idris_parsedSpan :: Maybe FC
270 , hide_list :: Ctxt Accessibility
271 , default_access :: Accessibility
272 , default_total :: DefaultTotality
273 , ibc_write :: [IBCWrite]
274 , compiled_so :: Maybe String
275 , idris_dynamic_libs :: [DynamicLib]
276 , idris_language_extensions :: [LanguageExt]
277 , idris_outputmode :: OutputMode
278 , idris_colourRepl :: Bool
279 , idris_colourTheme :: ColourTheme
280 , idris_errorhandlers :: [Name] -- ^ Global error handlers
281 , idris_nameIdx :: (Int, Ctxt (Int, Name))
282 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
283 , module_aliases :: M.Map [T.Text] [T.Text]
284 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
285 , idris_postulates :: S.Set Name
286 , idris_externs :: S.Set (Name, Int)
287 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
289 -- | List of names that were defined in the repl, and can be re-/un-defined
290 , idris_repl_defs :: [Name]
292 -- | Stack of names currently being elaborated, Bool set if it's an
293 -- implementation (implementations appear twice; also as a function name)
294 , elab_stack :: [(Name, Bool)]
297 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
298 , idris_exports :: [Name] -- ^ Functions with ExportList
299 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
300 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
301 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
302 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
303 , idris_ttstats :: M.Map Term (Int, Term)
304 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
305 , idris_interactiveOpts :: InteractiveOpts
308-- Required for parsers library, and therefore trifecta
309instance Show IState where
310 show = const "{internal state}"
312data SizeChange = Smaller | Same | Bigger | Unknown
313 deriving (Show, Eq, Generic)
315deriving instance Binary SizeChange
318type SCGEntry = (Name, [Maybe (Int, SizeChange)])
319type UsageReason = (Name, Int) -- fn_name, its_arg_number
321data CGInfo = CGInfo {
322 calls :: [Name] -- Immediate calls
323 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
325 , usedpos :: [(Int, [UsageReason])]
326 } deriving (Show, Generic)
328deriving instance Binary CGInfo
332primDefs = [ sUN "unsafePerformPrimIO"
333 , sUN "mkLazyForeignPrim"
334 , sUN "mkForeignPrim"
336 , sUN "assert_unreachable"
340-- information that needs writing for the current module's .ibc file
341data IBCWrite = IBCFix FixDecl
346 | IBCImplementation Bool Bool Name Name
353 | IBCImport (Bool, FilePath) -- ^ True = import public
354 | IBCImportDir FilePath
355 | IBCSourceDir FilePath
356 | IBCObj Codegen FilePath
357 | IBCLib Codegen String
358 | IBCCGFlag Codegen String
360 | IBCHeader Codegen String
361 | IBCAccess Name Accessibility
362 | IBCMetaInformation Name MetaInformation
363 | IBCTotal Name Totality
364 | IBCInjective Name Injectivity
366 | IBCFnInfo Name FnInfo
367 | IBCTrans Name (Term, Term)
368 | IBCErrRev (Term, Term)
373 | IBCDef Name -- ^ The main context.
374 | IBCNameHint (Name, Name)
375 | IBCLineApp FilePath Int PTerm
376 | IBCErrorHandler Name
377 | IBCFunctionErrorHandler Name Name Name
379 | IBCExtern (Name, Int)
380 | IBCTotCheckErr FC String
382 | IBCModDocs Name -- ^ The name is the special name used to track module docs
383 | IBCUsage (Name, Int)
385 | IBCAutoHint Name Name
386 | IBCDeprecate Name String
387 | IBCFragile Name String
388 | IBCConstraint FC UConstraint
389 deriving (Show, Generic)
391initialInteractiveOpts :: InteractiveOpts
392initialInteractiveOpts = InteractiveOpts {
393 interactiveOpts_indentWith = 2
394 , interactiveOpts_indentClause = 2
397-- | The initial state for the compiler
399idrisInit = IState initContext S.empty []
400 emptyContext emptyContext emptyContext [] emptyContext
401 emptyContext emptyContext emptyContext emptyContext
402 emptyContext emptyContext emptyContext emptyContext
403 emptyContext emptyContext emptyContext emptyContext
405 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
406 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
407 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
408 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
409 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
412-- | The monad for the main REPL - reading and processing files and
413-- updating global state (hence the IO inner monad).
416-- type Idris = WriterT [Either String (IO ())] (State IState a))
419type Idris = StateT IState (ExceptT Err IO)
421catchError :: Idris a -> (Err -> Idris a) -> Idris a
422catchError = liftCatch catchE
424throwError :: Err -> Idris a
425throwError = Trans.lift . throwE
427-- Commands in the REPL
432data ElabShellCmd = EQED
440 | EDocStr (Either Name Const)
446-- Parsed declarations
448data Fixity = Infixl { prec :: Int }
449 | Infixr { prec :: Int }
450 | InfixN { prec :: Int }
451 | PrefixN { prec :: Int }
452 deriving (Eq, Generic)
454deriving instance Binary Fixity
457instance Show Fixity where
458 show (Infixl i) = "infixl " ++ show i
459 show (Infixr i) = "infixr " ++ show i
460 show (InfixN i) = "infix " ++ show i
461 show (PrefixN i) = "prefix " ++ show i
463data FixDecl = Fix Fixity String
464 deriving (Eq, Generic)
466instance Show FixDecl where
467 show (Fix f s) = show f ++ " " ++ s
470deriving instance Binary FixDecl
473instance Ord FixDecl where
474 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
477data Static = Static | Dynamic
478 deriving (Show, Eq, Ord, Data, Generic, Typeable)
480deriving instance Binary Static
483-- ^ Mark bindings with their explicitness, and laziness
484data Plicity = Imp { pargopts :: [ArgOpt]
487 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
488 , pinsource :: Bool -- ^ Explicitly written in source
491 | Exp { pargopts :: [ArgOpt]
493 , pparam :: Bool -- ^ this is a param (rather than index)
496 | Constraint { pargopts :: [ArgOpt]
500 | TacImp { pargopts :: [ArgOpt]
505 deriving (Show, Eq, Ord, Data, Generic, Typeable)
508deriving instance Binary Plicity
511is_scoped :: Plicity -> Maybe ImplicitInfo
512is_scoped (Imp _ _ _ s _ _) = s
517impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
518-- Machine generated top level implicit
520impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
524forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
525forall_constraint :: Plicity
526forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
529expl = Exp [] Dynamic False RigW
531expl_param = Exp [] Dynamic True RigW
534constraint = Constraint [] Static RigW
536tacimpl :: PTerm -> Plicity
537tacimpl t = TacImp [] Dynamic t RigW
539data FnOpt = Inlinable -- ^ always evaluate when simplifying
540 | TotalFn | PartialFn | CoveringFn
541 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
544 -- | interface dictionary, eval only when a function
545 -- argument, and further evaluation results.
547 | OverlappingDictionary -- ^ Interface dictionary which may overlap
548 | Implicit -- ^ implicit coercion
549 | NoImplicit -- ^ do not apply implicit coercions
550 | CExport String -- ^ export, with a C name
551 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
552 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
553 | ErrorReduce -- ^ unfold definition before showing an error
554 | Reflection -- ^ a reflecting function, compile-time only
555 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
556 | Constructor -- ^ Data constructor type
557 | AutoHint -- ^ use in auto implicit search
558 | PEGenerated -- ^ generated by partial evaluator
559 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
560 deriving (Show, Eq, Generic)
562deriving instance Binary FnOpt
567inlinable :: FnOpts -> Bool
568inlinable = elem Inlinable
570dictionary :: FnOpts -> Bool
571dictionary = elem Dictionary
574-- | Type provider - what to provide
575data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
576 | ProvPostulate t -- ^ goal type must be Type, so only term
577 deriving (Show, Eq, Functor, Generic)
579type ProvideWhat = ProvideWhat' PTerm
581-- | Top-level declarations such as compiler directives, definitions,
582-- datatypes and interfaces.
584 -- | Fixity declaration
585 = PFix FC Fixity [String]
586 -- | Type declaration (last FC is precise name location)
587 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
588 -- | Postulate, second FC is precise name location
589 | PPostulate Bool -- external def if true
590 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
592 | PClauses FC FnOpts Name [PClause' t]
593 -- | Top level constant
595 -- | Data declaration.
596 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
598 | PParams FC [(Name, t)] [PDecl' t]
599 -- | Open block/declaration
600 | POpenInterfaces FC [Name] [PDecl' t]
601 -- | New namespace, where FC is accurate location of the namespace
603 | PNamespace String FC [PDecl' t]
605 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
607 FC -- Record name precise location
608 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
609 [(Name, Docstring (Either Err t))] -- Param Docs
610 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
611 (Maybe (Name, FC)) -- Optional constructor name and location
612 (Docstring (Either Err t)) -- Constructor doc
613 SyntaxInfo -- Constructor SyntaxInfo
615 -- | Interface: arguments are documentation, syntax info, source
616 -- location, constraints, interface name, interface name location,
617 -- parameters, method declarations, optional constructor name
618 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
619 [(Name, t)] -- constraints
620 Name -- interface name
621 FC -- accurate location of interface name
622 [(Name, FC, t)] -- parameters and precise locations
623 [(Name, Docstring (Either Err t))] -- parameter docstrings
624 [(Name, FC)] -- determining parameters and precise locations
625 [PDecl' t] -- declarations
626 (Maybe (Name, FC)) -- implementation constructor name and location
627 (Docstring (Either Err t)) -- implementation constructor docs
629 -- | Implementation declaration: arguments are documentation, syntax
630 -- info, source location, constraints, interface name, parameters, full
631 -- Implementation type, optional explicit name, and definitions
632 | PImplementation (Docstring (Either Err t)) -- Implementation docs
633 [(Name, Docstring (Either Err t))] -- Parameter docs
635 FC [(Name, t)] -- constraints
636 [Name] -- parent dictionaries to search for constraints
640 FC -- precise location of interface
642 [(Name, t)] -- Extra names in scope in the body
643 t -- full Implementation type
644 (Maybe Name) -- explicit name
646 | PDSL Name (DSL' t) -- ^ DSL declaration
647 | PSyntax FC Syntax -- ^ Syntax definition
648 | PMutual FC [PDecl' t] -- ^ Mutual block
649 | PDirective Directive -- ^ Compiler directive.
651 -- | Type provider. The first t is the type, the second is the
652 -- term. The second FC is precise highlighting location.
653 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
655 -- | Source-to-source transformation rule. If bool is True, lhs and
656 -- rhs must be convertible.
657 | PTransform FC Bool t t
659 -- | FC is decl-level, for errors, and Strings represent the
661 | PRunElabDecl FC t [String]
662 deriving (Functor, Generic)
664deriving instance Binary PDecl'
667-- | The set of source directives
668data Directive = DLib Codegen String
669 | DLink Codegen String
670 | DFlag Codegen String
671 | DInclude Codegen String
676 | DSetTotal Name -- assert totality after checking
677 | DAccess Accessibility
678 | DDefault DefaultTotality
680 | DDynamicLibs [String]
681 | DNameHint Name FC [(Name, FC)]
682 | DErrorHandlers Name FC Name FC [(Name, FC)]
683 | DLanguage LanguageExt
684 | DDeprecate Name String
685 | DFragile Name String
686 | DAutoImplicits Bool
690-- | A set of instructions for things that need to happen in IState
691-- after a term elaboration when there's been reflected elaboration.
692data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
693 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
694 | RAddImplementation Name Name
695 | RDatatypeDeclInstrs Name [PArg]
696 -- | Datatype, constructors
697 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
700-- | For elaborator state
701data EState = EState {
702 case_decls :: [(Name, PDecl)]
703 , delayed_elab :: [(Int, Elab' EState ())]
704 , new_tyDecls :: [RDeclInstructions]
705 , highlighting :: [(FC, OutputAnnotation)]
706 , auto_binds :: [Name] -- ^ names bound as auto implicits
707 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
711initEState = EState [] [] [] [] [] []
713type ElabD a = Elab' EState a
715highlightSource :: FC -> OutputAnnotation -> ElabD ()
716highlightSource fc annot =
717 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
719-- | One clause of a top-level definition. Term arguments to constructors are:
721-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
723-- 2. The list of extra 'with' patterns
725-- 3. The right-hand side
727-- 4. The where block (PDecl' t)
729data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
730 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
731 | PClauseR FC [t] t [PDecl' t]
732 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
733 deriving (Functor, Generic)
735deriving instance Binary PClause'
740 -- | Data declaration
741 PDatadecl { d_name :: Name -- ^ The name of the datatype
742 , d_name_fc :: FC -- ^ The precise location of the type constructor name
743 , d_tcon :: t -- ^ Type constructor
744 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
746 -- | "Placeholder" for data whose constructors are defined later
747 | PLaterdecl { d_name :: Name
750 } deriving (Functor, Generic)
752-- | Transform the FCs in a PData and its associated terms. The first
753-- function transforms the general-purpose FCs, and the second
754-- transforms those that are used for semantic source highlighting, so
755-- they can be treated specially.
756mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
757mapPDataFC f g (PDatadecl n nfc tycon ctors) =
758 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
759 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
760 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
761mapPDataFC f g (PLaterdecl n nfc tycon) =
762 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
764deriving instance Binary PData'
767-- Handy to get a free function for applying PTerm -> PTerm functions
768-- across a program, by deriving Functor
770type PDecl = PDecl' PTerm
771type PData = PData' PTerm
772type PClause = PClause' PTerm
774-- | Transform the FCs in a PTerm. The first function transforms the
775-- general-purpose FCs, and the second transforms those that are used
776-- for semantic source highlighting, so they can be treated specially.
777mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
778mapPDeclFC f g (PFix fc fixity ops) =
779 PFix (f fc) fixity ops
780mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
781 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
782mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
783 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
785mapPDeclFC f g (PClauses fc opts n clauses) =
786 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
787mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
788mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
789 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
790mapPDeclFC f g (PParams fc params decls) =
792 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
793 (map (mapPDeclFC f g) decls)
794mapPDeclFC f g (POpenInterfaces fc ifs decls) =
795 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
796mapPDeclFC f g (PNamespace ns fc decls) =
797 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
798mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
799 PRecord doc syn (f fc) opts n (g nfc)
800 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
802 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
803 plic, mapPTermFC f g ty, fdoc))
805 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
808mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
809 PInterface doc syn (f fc)
810 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
811 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
812 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
813 (map (mapPDeclFC f g) body)
814 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
816mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
817 PImplementation doc paramDocs syn (f fc)
818 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
819 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
820 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
821 (mapPTermFC f g implTy)
823 (map (mapPDeclFC f g) body)
824mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
825mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
827 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
828 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
829mapPDeclFC f g (PMutual fc decls) =
830 PMutual (f fc) (map (mapPDeclFC f g) decls)
831mapPDeclFC f g (PDirective d) =
834 DNameHint n nfc ns ->
835 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
836 DErrorHandlers n nfc n' nfc' ns ->
837 DErrorHandlers n (g nfc) n' (g nfc') $
838 map (\(an, anfc) -> (an, g anfc)) ns
839mapPDeclFC f g (PProvider doc syn fc nfc what n) =
840 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
841mapPDeclFC f g (PTransform fc safe l r) =
842 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
843mapPDeclFC f g (PRunElabDecl fc script ns) =
844 PRunElabDecl (f fc) (mapPTermFC f g script) ns
846-- | Get all the names declared in a declaration
847declared :: PDecl -> [Name]
848declared (PFix _ _ _) = []
849declared (PTy _ _ _ _ _ n fc t) = [n]
850declared (PPostulate _ _ _ _ _ _ n t) = [n]
851declared (PClauses _ _ n _) = [] -- not a declaration
852declared (PCAF _ n _) = [n]
853declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
854 where fstt (_, _, a, _, _, _, _) = a
855declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
856declared (PParams _ _ ds) = concatMap declared ds
857declared (POpenInterfaces _ _ ds) = concatMap declared ds
858declared (PNamespace _ _ ds) = concatMap declared ds
859declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
860declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
861declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
865declared (PDSL n _) = [n]
866declared (PSyntax _ _) = []
867declared (PMutual _ ds) = concatMap declared ds
868declared (PDirective _) = []
871-- get the names declared, not counting nested parameter blocks
872tldeclared :: PDecl -> [Name]
873tldeclared (PFix _ _ _) = []
874tldeclared (PTy _ _ _ _ _ n _ t) = [n]
875tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
876tldeclared (PClauses _ _ n _) = [] -- not a declaration
877tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
878tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
879 where fstt (_, _, a, _, _, _, _) = a
880tldeclared (PParams _ _ ds) = []
881tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
882tldeclared (PMutual _ ds) = concatMap tldeclared ds
883tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
884tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
885tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
891defined :: PDecl -> [Name]
892defined (PFix _ _ _) = []
893defined (PTy _ _ _ _ _ n _ t) = []
894defined (PPostulate _ _ _ _ _ _ n t) = []
895defined (PClauses _ _ n _) = [n] -- not a declaration
896defined (PCAF _ n _) = [n]
897defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
898 where fstt (_, _, a, _, _, _, _) = a
899defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
900defined (PParams _ _ ds) = concatMap defined ds
901defined (POpenInterfaces _ _ ds) = concatMap defined ds
902defined (PNamespace _ _ ds) = concatMap defined ds
903defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
904defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
905defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
909defined (PDSL n _) = [n]
910defined (PSyntax _ _) = []
911defined (PMutual _ ds) = concatMap defined ds
912defined (PDirective _) = []
915updateN :: [(Name, Name)] -> Name -> Name
916updateN ns n | Just n' <- lookup n ns = n'
919updateNs :: [(Name, Name)] -> PTerm -> PTerm
921updateNs ns t = mapPT updateRef t
922 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
925-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
927-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
928-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
929-- where updateCNs ns (PClause n l ts r ds)
930-- = PClause (updateN ns n) (fmap (updateNs ns) l)
931-- (map (fmap (updateNs ns)) ts)
932-- (fmap (updateNs ns) r)
933-- (map (updateDNs ns) ds)
939 deriving (Eq, Show, Ord, Data, Typeable, Generic)
941-- | High level language terms
942data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
943 -- high-level language
945 -- ^ A reference to a variable. The FC is its precise
946 -- source location for highlighting. The list of FCs is a
947 -- collection of additional highlighting locations.
948 | PInferRef FC [FC] Name -- ^ A name to be defined later
949 | PPatvar FC Name -- ^ A pattern variable
950 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
951 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
952 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
953 | PTyped PTerm PTerm -- ^ Term with explicit type
954 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
955 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
956 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
957 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
958 | PMatchApp FC Name -- ^ Make an application by type matching
959 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
960 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
961 | PTrue FC PunInfo -- ^ Unit type..?
962 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
963 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
964 -- ^ "rewrite" syntax, with optional rewriting function and
965 -- optional result type
966 | PPair FC [FC] PunInfo PTerm PTerm
967 -- ^ A pair (a, b) and whether it's a product type or a
968 -- pair (solved by elaboration). The list of FCs is its
970 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
971 -- ^ A dependent pair (tm : a ** b) and whether it's a
972 -- sigma type or a pair that inhabits one (solved by
973 -- elaboration). The [FC] is its punctuation.
974 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
975 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
976 | PHidden PTerm -- ^ Irrelevant or hidden pattern
977 | PType FC -- ^ 'Type' type
978 | PUniverse FC Universe -- ^ Some universe
979 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
980 | PConstant FC Const -- ^ Builtin types
981 | Placeholder -- ^ Underscore
982 | PDoBlock [PDo] -- ^ Do notation
983 | PIdiom FC PTerm -- ^ Idiom brackets
984 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
985 | PProof [PTactic] -- ^ Proof script
986 | PTactics [PTactic] -- ^ As PProof, but no auto solving
987 | PElabError Err -- ^ Error to report on elaboration
988 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
989 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
990 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
991 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
992 | PNoImplicits PTerm -- ^ never run implicit converions on the term
993 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
994 | PUnquote PTerm -- ^ ~Term
995 | PQuoteName Name Bool FC
996 -- ^ `{n} where the FC is the precise highlighting for
997 -- the name in particular. If the Bool is False, then
998 -- it's `{{n}} and the name won't be resolved.
999 | PRunElab FC PTerm [String]
1000 -- ^ %runElab tm - New-style proof script. Args are
1001 -- location, script, enclosing namespace.
1002 | PConstSugar FC PTerm
1003 -- ^ A desugared constant. The FC is a precise source
1004 -- location that will be used to highlight it later.
1005 deriving (Eq, Ord, Data, Typeable, Generic)
1007data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1010 deriving (Eq, Ord, Data, Generic, Typeable)
1012-- | Transform the FCs in a PTerm. The first function transforms the
1013-- general-purpose FCs, and the second transforms those that are used
1014-- for semantic source highlighting, so they can be treated specially.
1015mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1016mapPTermFC f g (PQuote q) = PQuote q
1017mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1018mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1019mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1020mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1021mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1022mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1023mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1024mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1025mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1026mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1027mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1028mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1029mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1030mapPTermFC 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)
1031mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1032mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1033mapPTermFC 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)
1034mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1035mapPTermFC 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)
1036mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1037mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1038mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1039mapPTermFC f g (PType fc) = PType (f fc)
1040mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1041mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1042mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1043mapPTermFC f g Placeholder = Placeholder
1044mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1045 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1046 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1047 mapPDoFC (DoBindP fc t1 t2 alts) =
1048 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1049 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1050 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1051 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1052mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1053mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1054mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1055mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1056mapPTermFC f g (PElabError err) = PElabError err
1057mapPTermFC f g PImpossible = PImpossible
1058mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1059mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1060mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1061mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1062mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1063mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1064mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1065mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1066mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1069dg instance Binary PTerm
1072mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1073mapPT f t = f (mpt t) where
1074 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1075 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1076 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1077 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1078 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1079 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1080 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1081 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1082 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1083 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1084 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1085 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1086 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1087 mpt (PHidden t) = PHidden (mapPT f t)
1088 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1089 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1090 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1091 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1092 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1093 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1094 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1098data PTactic' t = Intro [Name] | Intros | Focus Name
1099 | Refine Name [Bool] | Rewrite t | DoUnify
1106 | LetTac Name t | LetTacTy Name t t
1107 | Exact t | Compute | Trivial | TCImplementation
1108 | ProofSearch Bool Bool Int (Maybe Name)
1109 [Name] -- allowed local names
1111 -- ^ the bool is whether to search recursively
1114 | ProofState | ProofTerm | Undo
1115 | Try (PTactic' t) (PTactic' t)
1116 | TSeq (PTactic' t) (PTactic' t)
1117 | ApplyTactic t -- see Language.Reflection module
1121 | GoalType String (PTactic' t)
1124 | TDocStr (Either Name Const)
1127 | TFail [ErrorReportPart]
1130 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1132deriving instance Binary PTactic'
1134instance Sized a => Sized (PTactic' a) where
1135 size (Intro nms) = 1 + size nms
1137 size (Focus nm) = 1 + size nm
1138 size (Refine nm bs) = 1 + size nm + length bs
1139 size (Rewrite t) = 1 + size t
1140 size (Induction t) = 1 + size t
1141 size (LetTac nm t) = 1 + size nm + size t
1142 size (Exact t) = 1 + size t
1150 size (Try l r) = 1 + size l + size r
1151 size (TSeq l r) = 1 + size l + size r
1152 size (ApplyTactic t) = 1 + size t
1153 size (Reflect t) = 1 + size t
1154 size (Fill t) = 1 + size t
1158 size (TFail ts) = 1 + size ts
1161 size (CaseTac x) = 1 + size x
1162 size (Equiv t) = 1 + size t
1163 size (Claim x y) = 1 + size x + size y
1165 size (MatchRefine x) = 1 + size x
1166 size (LetTacTy x y z) = 1 + size x + size y + size z
1167 size TCImplementation = 1
1169type PTactic = PTactic' PTerm
1171data PDo' t = DoExp FC t
1172 | DoBind FC Name FC t -- ^ second FC is precise name location
1173 | DoBindP FC t t [(t,t)]
1174 | DoLet FC Name FC t t -- ^ second FC is precise name location
1176 | DoRewrite FC t -- rewrite in do block
1177 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1179deriving instance Binary PDo'
1182instance Sized a => Sized (PDo' a) where
1183 size (DoExp fc t) = 1 + size fc + size t
1184 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1185 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1186 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1187 size (DoLetP fc l r) = 1 + size fc + size l + size r
1188 size (DoRewrite fc h) = 1 + size fc + size h
1190type PDo = PDo' PTerm
1192-- The priority gives a hint as to elaboration order. Best to elaborate
1193-- things early which will help give a more concrete type to other
1194-- variables, e.g. a before (interpTy a).
1196data PArg' t = PImp { priority :: Int
1197 , machine_inf :: Bool -- ^ true if the machine inferred it
1198 , argopts :: [ArgOpt]
1202 | PExp { priority :: Int
1203 , argopts :: [ArgOpt]
1207 | PConstraint { priority :: Int
1208 , argopts :: [ArgOpt]
1212 | PTacImplicit { priority :: Int
1213 , argopts :: [ArgOpt]
1218 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1220data ArgOpt = AlwaysShow
1224 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1226instance Sized a => Sized (PArg' a) where
1227 size (PImp p _ l nm trm) = 1 + size nm + size trm
1228 size (PExp p l nm trm) = 1 + size nm + size trm
1229 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1230 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1233deriving instance Binary PArg'
1236pimp n t mach = PImp 1 mach [] n t
1237pexp t = PExp 1 [] (sMN 0 "arg") t
1238pconst t = PConstraint 1 [] (sMN 0 "carg") t
1239ptacimp n s t = PTacImplicit 2 [] n s t
1241type PArg = PArg' PTerm
1243-- | Get the highest FC in a term, if one exists
1244highestFC :: PTerm -> Maybe FC
1245highestFC (PQuote _) = Nothing
1246highestFC (PRef fc _ _) = Just fc
1247highestFC (PInferRef fc _ _) = Just fc
1248highestFC (PPatvar fc _) = Just fc
1249highestFC (PLam fc _ _ _ _) = Just fc
1250highestFC (PPi _ _ _ _ _) = Nothing
1251highestFC (PLet fc _ _ _ _ _) = Just fc
1252highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1253highestFC (PApp fc _ _) = Just fc
1254highestFC (PAppBind fc _ _) = Just fc
1255highestFC (PMatchApp fc _) = Just fc
1256highestFC (PCase fc _ _) = Just fc
1257highestFC (PIfThenElse fc _ _ _) = Just fc
1258highestFC (PTrue fc _) = Just fc
1259highestFC (PResolveTC fc) = Just fc
1260highestFC (PRewrite fc _ _ _ _) = Just fc
1261highestFC (PPair fc _ _ _ _) = Just fc
1262highestFC (PDPair fc _ _ _ _ _) = Just fc
1263highestFC (PAs fc _ _) = Just fc
1264highestFC (PAlternative _ _ args) =
1265 case mapMaybe highestFC args of
1268highestFC (PHidden _) = Nothing
1269highestFC (PType fc) = Just fc
1270highestFC (PUniverse _ _) = Nothing
1271highestFC (PGoal fc _ _ _) = Just fc
1272highestFC (PConstant fc _) = Just fc
1273highestFC Placeholder = Nothing
1274highestFC (PDoBlock lines) =
1275 case map getDoFC lines of
1279 getDoFC (DoExp fc t) = fc
1280 getDoFC (DoBind fc nm nfc t) = fc
1281 getDoFC (DoBindP fc l r alts) = fc
1282 getDoFC (DoLet fc nm nfc l r) = fc
1283 getDoFC (DoLetP fc l r) = fc
1284 getDoFC (DoRewrite fc h) = fc
1286highestFC (PIdiom fc _) = Just fc
1287highestFC (PMetavar fc _) = Just fc
1288highestFC (PProof _) = Nothing
1289highestFC (PTactics _) = Nothing
1290highestFC (PElabError _) = Nothing
1291highestFC PImpossible = Nothing
1292highestFC (PCoerced tm) = highestFC tm
1293highestFC (PDisamb _ opts) = highestFC opts
1294highestFC (PUnifyLog tm) = highestFC tm
1295highestFC (PNoImplicits tm) = highestFC tm
1296highestFC (PQuasiquote _ _) = Nothing
1297highestFC (PUnquote tm) = highestFC tm
1298highestFC (PQuoteName _ _ fc) = Just fc
1299highestFC (PRunElab fc _ _) = Just fc
1300highestFC (PConstSugar fc _) = Just fc
1301highestFC (PAppImpl t _) = highestFC t
1305data InterfaceInfo = CI {
1306 implementationCtorName :: Name
1307 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1308 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1309 , interface_default_super_interfaces :: [PDecl]
1310 , interface_impparams :: [Name]
1311 , interface_params :: [Name]
1312 , interface_constraints :: [PTerm]
1313 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1314 , interface_determiners :: [Int]
1315 } deriving (Show, Generic)
1317deriving instance Binary InterfaceInfo
1321data RecordInfo = RI {
1322 record_parameters :: [(Name,PTerm)]
1323 , record_constructor :: Name
1324 , record_projections :: [Name]
1325 } deriving (Show, Generic)
1327-- Type inference data
1329data TIData = TIPartial -- ^ a function with a partially defined type
1330 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1331 deriving (Show, Generic)
1333-- | Miscellaneous information about functions
1334data FnInfo = FnInfo { fn_params :: [Int] }
1335 deriving (Show, Generic)
1337deriving instance Binary FnInfo
1340data OptInfo = Optimise {
1341 inaccessible :: [(Int,Name)] -- includes names for error reporting
1342 , detaggable :: Bool
1343 , forceable :: [Int] -- argument positions which are forced by other values
1344 } deriving (Show, Generic)
1346deriving instance Binary OptInfo
1349-- | Syntactic sugar info
1354 , dsl_var :: Maybe t
1355 , index_first :: Maybe t
1356 , index_next :: Maybe t
1357 , dsl_lambda :: Maybe t
1358 , dsl_let :: Maybe t
1360 } deriving (Show, Functor, Generic)
1362deriving instance Binary DSL'
1365type DSL = DSL' PTerm
1367data SynContext = PatternSyntax
1370 deriving (Show, Generic)
1372deriving instance Binary SynContext
1375data Syntax = Rule [SSymbol] PTerm SynContext
1376 | DeclRule [SSymbol] [PDecl]
1377 deriving (Show, Generic)
1379syntaxNames :: Syntax -> [Name]
1380syntaxNames (Rule syms _ _) = mapMaybe ename syms
1381 where ename (Keyword n) = Just n
1383syntaxNames (DeclRule syms _) = mapMaybe ename syms
1384 where ename (Keyword n) = Just n
1387syntaxSymbols :: Syntax -> [SSymbol]
1388syntaxSymbols (Rule ss _ _) = ss
1389syntaxSymbols (DeclRule ss _) = ss
1391deriving instance Binary Syntax
1394data SSymbol = Keyword Name
1399 deriving (Show, Eq, Generic)
1403deriving instance Binary SSymbol
1406newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1409emptySyntaxRules :: SyntaxRules
1410emptySyntaxRules = SyntaxRules []
1412updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1413updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1415 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1420 ruleSort (s1:ss1) (s2:ss2) =
1421 case symCompare s1 s2 of
1422 EQ -> ruleSort ss1 ss2
1425 -- Better than creating Ord implementation for SSymbol since
1426 -- in general this ordering does not really make sense.
1427 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1428 symCompare (Keyword _) _ = LT
1429 symCompare (Symbol _) (Keyword _) = GT
1430 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1431 symCompare (Symbol _) _ = LT
1432 symCompare (Binding _) (Keyword _) = GT
1433 symCompare (Binding _) (Symbol _) = GT
1434 symCompare (Binding b1) (Binding b2) = compare b1 b2
1435 symCompare (Binding _) _ = LT
1436 symCompare (Expr _) (Keyword _) = GT
1437 symCompare (Expr _) (Symbol _) = GT
1438 symCompare (Expr _) (Binding _) = GT
1439 symCompare (Expr e1) (Expr e2) = compare e1 e2
1440 symCompare (Expr _) _ = LT
1441 symCompare (SimpleExpr _) (Keyword _) = GT
1442 symCompare (SimpleExpr _) (Symbol _) = GT
1443 symCompare (SimpleExpr _) (Binding _) = GT
1444 symCompare (SimpleExpr _) (Expr _) = GT
1445 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1447initDSL = DSL (PRef f [] (sUN ">>="))
1448 (PRef f [] (sUN "<*>"))
1449 (PRef f [] (sUN "pure"))
1456 where f = fileFC "(builtin)"
1458data Using = UImplicit Name PTerm
1459 | UConstraint Name [Name]
1460 deriving (Show, Eq, Data, Generic, Typeable)
1462deriving instance Binary Using
1465data SyntaxInfo = Syn {
1467 , syn_params :: [(Name, PTerm)]
1468 , syn_namespace :: [String]
1470 , imp_methods :: [Name]
1471 -- ^ interface methods. When expanding implicits, these should be
1472 -- expanded even under binders
1473 , decoration :: Name -> Name
1475 , implicitAllowed :: Bool
1476 , constraintAllowed :: Bool
1477 , maxline :: Maybe Int
1478 , mut_nesting :: Int
1480 , syn_in_quasiquote :: Int
1481 , syn_toplevel :: Bool
1482 , withAppAllowed :: Bool
1483 } deriving (Show, Generic)
1485deriving instance Binary SyntaxInfo
1488defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1490expandNS :: SyntaxInfo -> Name -> Name
1491expandNS syn n@(NS _ _) = n
1492expandNS syn n = case syn_namespace syn of
1497-- For inferring types of things
1499bi = fileFC "builtin"
1500primfc = fileFC "(primitive)"
1502inferTy = sMN 0 "__Infer"
1503inferCon = sMN 0 "__infer"
1504inferDecl = PDatadecl inferTy primfc
1506 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1507 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1508 (PRef bi [] inferTy)), bi, [])]
1511infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1512infP = P (TCon 6 0) inferTy (TType (UVal 0))
1514getInferTerm, getInferType :: Term -> Term
1515getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1516getInferTerm (App _ (App _ _ _) tm) = tm
1517getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1519getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1520 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1521 toTy (PVar _ t) = PVTy t
1523getInferType (App _ (App _ _ ty) _) = ty
1527-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1529primNames = [inferTy, inferCon]
1532unitCon = sUN "MkUnit"
1534falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1535 "The empty type, also known as the trivially false proposition." ++
1537 "Use `void` or `absurd` to prove anything if you have a variable " ++
1538 "of type `Void` in scope."
1541pairTy = sNS (sUN "Pair") ["Builtins"]
1542pairCon = sNS (sUN "MkPair") ["Builtins"]
1544upairTy = sNS (sUN "UPair") ["Builtins"]
1545upairCon = sNS (sUN "MkUPair") ["Builtins"]
1549eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1550 "The propositional equality type. A proof that `x` = `y`." ++
1552 "To use such a proof, pattern-match on it, and the two equal things will " ++
1553 "then need to be the _same_ pattern." ++
1555 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1556 "is possible to state equalities between values of potentially different " ++
1557 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1559 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1561eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1562 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1564 [(reflDoc, reflParamDoc,
1565 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1566 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1567 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1568 pimp (n "B") Placeholder False,
1569 pexp (PRef bi [] (n "x")),
1570 pexp (PRef bi [] (n "x"))])), bi, [])]
1572 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1573 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1574 "shown that both sides are in fact equal."
1575 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1576 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1578eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1579 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1585-- | The special name to be used in the module documentation context -
1586-- not for use in the main definition context. The namespace around it
1587-- will determine the module to which the docs adhere.
1589modDocName = sMN 0 "ModuleDocs"
1591-- Defined in builtins.idr
1592sigmaTy = sNS (sUN "DPair") ["Builtins"]
1593sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1595piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1596piBind = piBindp expl
1598piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1600piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1603-- Pretty-printing declarations and terms
1605-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1606-- could interfere with interactive editing, which calls "show".
1608instance Show PTerm where
1609 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1611instance Show PDecl where
1612 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1614instance Show PClause where
1615 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1617instance Show PData where
1618 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1620instance Pretty PTerm OutputAnnotation where
1621 pretty = prettyImp defaultPPOption
1623-- | Colourise annotations according to an Idris state. It ignores the
1624-- names in the annotation, as there's no good way to show extended
1625-- information on a terminal.
1626annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1627annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1628annotationColour ist (AnnConst c) =
1629 let theme = idris_colourTheme ist
1630 in Just $ if constIsType c
1631 then typeColour theme
1632 else dataColour theme
1633annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1634annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1635annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1636annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1637annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1638annotationColour ist (AnnName n _ _ _) =
1639 let ctxt = tt_ctxt ist
1640 theme = idris_colourTheme ist
1642 _ | isDConName n ctxt -> Just $ dataColour theme
1643 _ | isFnName n ctxt -> Just $ functionColour theme
1644 _ | isTConName n ctxt -> Just $ typeColour theme
1645 _ | isPostulateName n ist -> Just $ postulateColour theme
1646 _ | otherwise -> Nothing -- don't colourise unknown names
1647annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1648 where colour BoldText = IdrisColour Nothing True False True False
1649 colour UnderlineText = IdrisColour Nothing True True False False
1650 colour ItalicText = IdrisColour Nothing True False False True
1651annotationColour ist _ = Nothing
1654-- | Colourise annotations according to an Idris state. It ignores the
1655-- names in the annotation, as there's no good way to show extended
1656-- information on a terminal. Note that strings produced this way will
1657-- not be coloured on Windows, so the use of the colour rendering
1658-- functions in Idris.Output is to be preferred.
1659consoleDecorate :: IState -> OutputAnnotation -> String -> String
1660consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1662isPostulateName :: Name -> IState -> Bool
1663isPostulateName n ist = S.member n (idris_postulates ist)
1665-- | Pretty-print a high-level closed Idris term with no information
1666-- about precedence/associativity
1667prettyImp :: PPOption -- ^ pretty printing options
1668 -> PTerm -- ^ the term to pretty-print
1669 -> Doc OutputAnnotation
1670prettyImp impl = pprintPTerm impl [] [] []
1672-- | Serialise something to base64 using its Binary implementation.
1674-- | Do the right thing for rendering a term in an IState
1675prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1676prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1678-- | Pretty-print a high-level Idris term in some bindings context
1680pprintPTerm :: PPOption -- ^ pretty printing options
1681 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1682 -> [Name] -- ^ names to always show in pi, even if not used
1683 -> [FixDecl] -- ^ Fixity declarations
1684 -> PTerm -- ^ the term to pretty-print
1685 -> Doc OutputAnnotation
1686pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1691 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1692 prettySe d p bnd (PQuote r) =
1693 text "![" <> pretty r <> text "]"
1694 prettySe d p bnd (PPatvar fc n) = pretty n
1696 | Just str <- slist d p bnd e = depth d str
1697 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1698 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1699 prettySe d p bnd (PLam fc n nfc ty sc) =
1700 let (ns, sc') = getLamNames [n] sc in
1701 depth d . bracket p startPrec . group . align . hang 2 $
1702 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1703 prettySe (decD d) startPrec ((n, False):bnd) sc'
1705 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1706 getLamNames acc sc = (reverse acc, sc)
1708 prettyBindingsOf [] t = text ""
1709 prettyBindingsOf [n] t = prettyBindingOf n t
1710 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1711 prettyBindingsOf ns t
1712 prettySe d p bnd (PLet fc n nfc ty v sc) =
1713 depth d . bracket p startPrec . group . align $
1714 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1715 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1716 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1718 depth d . bracket p startPrec . group $
1719 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1720 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1722 depth d . bracket p startPrec . group $
1723 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1724 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1725 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1726 || ppopt_pinames ppo && uname n =
1727 depth d . bracket p startPrec . group $
1728 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1729 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1731 depth d . bracket p startPrec . group $
1732 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1733 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1735 uname (UN n) = case str n of
1742 Static -> text "%static" <> space
1744 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1746 depth d . bracket p startPrec $
1747 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1748 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1749 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1750 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1752 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1753 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1754 showRig _ n = prettyBindingOf n True
1756 isPi (PPi (Exp{}) _ _ _ _) = True
1757 isPi (PPi _ _ _ _ sc) = isPi sc
1762 Static -> text "%static" <> space
1764 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1765 depth d . bracket p startPrec $
1766 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1767 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1768 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1769 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1770 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1771 depth d . bracket p startPrec $
1772 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1773 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1774 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1775 | basename neg == sUN "negate" =
1776 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1777 -- This case preserves the behavior of the former constructor PEq.
1778 -- It should be removed if feasible when the pretty-printing of infix
1779 -- operators in general is improved.
1780 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1781 | n == eqTy, ppopt_impl ppo =
1782 depth d . bracket p eqPrec $
1783 enclose lparen rparen eq <+>
1784 align (group (vsep (map (prettyArgS (decD d) bnd)
1787 depth d . bracket p eqPrec . align . group $
1788 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1789 where eq = annName eqTy (text "=")
1791 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1792 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1793 | UN nm <- basename f
1794 , not (ppopt_impl ppo) && null (getShowArgs args) =
1795 prettyName True (ppopt_impl ppo) bnd f
1796 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1797 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1798 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1799 | UN nm <- basename op
1801 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1802 case getShowArgs args of
1804 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1805 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1806 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1807 (l@(PExp{}) : r@(PExp{}) : rest) ->
1808 depth d . bracket p funcAppPrec $
1809 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1810 align (group (vsep (map (prettyArgS d bnd) rest)))
1811 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1812 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1813 f = getFixity (opStr op)
1815 Nothing -> funcAppPrec + 1
1816 Just (Infixl p') -> p'
1817 Just f' -> prec f' + 1
1819 Nothing -> funcAppPrec + 1
1820 Just (Infixr p') -> p'
1821 Just f' -> prec f' + 1
1822 inFix l r = align . group $
1823 (prettySe (decD d) left bnd l <+> opName False) <$>
1824 group (prettySe (decD d) right bnd r)
1825 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1826 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1827 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1828 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1829 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1830 let args = getShowArgs as
1831 fp = prettySe (decD d) (startPrec + 1) bnd f
1832 shownArgs = if ppopt_impl ppo then as else args
1834 depth d . bracket p funcAppPrec . group $
1837 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1838 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1839 prettySe d p bnd (PCase _ scr cases) =
1840 bracket p funcAppPrec $
1841 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1842 depth d (indent 2 (vsep (map ppcase cases)))
1844 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1845 ([(n, False) | n <- vars l] ++ bnd)
1846 in nest nestingSize $
1847 prettyCase l <+> text "=>" <+> prettyCase r
1848 -- Warning: this is a bit of a hack. At this stage, we don't have the
1849 -- global context, so we can't determine which names are constructors,
1850 -- which are types, and which are pattern variables on the LHS of the
1851 -- case pattern. We use the heuristic that names without a namespace
1852 -- are patvars, because right now case blocks in PTerms are always
1853 -- delaborated from TT before being sent to the pretty-printer. If they
1854 -- start getting printed directly, THIS WILL BREAK.
1855 -- Potential solution: add a list of known patvars to the cases in
1856 -- PCase, and have the delaborator fill it out, kind of like the pun
1857 -- disambiguation on PDPair.
1858 vars tm = filter noNS (allNamesIn tm)
1859 noNS (NS _ _) = False
1862 prettySe d p bnd (PIfThenElse _ c t f) =
1863 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1864 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1865 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1866 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1868 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1869 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1870 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1871 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1872 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1873 prettySe d p bnd (PRewrite _ by l r _) =
1874 depth d . bracket p startPrec $
1875 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1878 Just fn -> text "using" <+>
1879 prettyName True (ppopt_impl ppo) bnd fn) <+>
1880 text "in" <+> prettySe (decD d) startPrec bnd r
1881 prettySe d p bnd (PTyped l r) =
1882 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1883 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1884 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1885 align . group . vsep . punctuate (ann comma) $
1886 map (prettySe (decD d) startPrec bnd) elts
1887 where ann = case pun of
1889 IsType -> annName pairTy
1890 IsTerm -> annName pairCon
1891 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1892 | Just elts <- dPairElts dpair
1893 = depth d . enclose (annotated lparen) (annotated rparen) .
1894 align . group . vsep . punctuate (space <> annotated (text "**")) $
1900 annotated (text "**") <+>
1901 prettySe (decD d) startPrec (addBinding bnd) r <>
1903 where annotated = case pun of
1904 IsType -> annName sigmaTy
1905 IsTerm -> annName sigmaCon
1908 (left, addBinding) = case (l, pun) of
1909 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1910 _ -> (prettySe (decD d) startPrec bnd l, id)
1913 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1914 ppElts ((PRef _ _ n, t):rs) bs
1916 = (bindingOf n False <+> colon <+>
1917 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1918 ppElts ((l, t):rs) bs
1919 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1920 prettySe d p bnd (PAlternative ns a as) =
1921 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1924 foldr ((\ l r -> l <+> text "," <+> r) .
1925 depth d . prettySe (decD d) startPrec bnd)
1927 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1928 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1929 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1930 -- XXX: add pretty for tactics
1931 prettySe d p bnd (PProof ts) =
1932 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1933 prettySe d p bnd (PTactics ts) =
1934 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1935 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1936 prettySe d p bnd PImpossible = kwd "impossible"
1937 prettySe d p bnd Placeholder = text "_"
1938 prettySe d p bnd (PDoBlock dos) =
1939 bracket p startPrec $
1940 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1941 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1942 ppdo bnd (DoBind _ bn _ tm : dos) =
1943 (prettyBindingOf bn False <+> text "<-" <+>
1944 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1945 ppdo ((bn, False):bnd) dos
1946 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1947 text "no pretty printer for pattern-matching do binding" :
1949 ppdo bnd (DoLet _ ln _ ty v : dos) =
1950 (kwd "let" <+> prettyBindingOf ln False <+>
1951 (if ty /= Placeholder
1952 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1954 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1955 ppdo ((ln, False):bnd) dos
1956 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1957 text "no pretty printer for pattern-matching do binding" :
1959 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1960 text "no pretty printer for pattern-matching do binding" :
1963 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1964 prettySe d p bnd (PElabError s) = pretty s
1965 -- Quasiquote pprinting ignores bound vars
1966 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1967 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1968 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1969 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1970 where start = if res then "`{" else "`{{"
1971 end = if res then "}" else "}}"
1972 prettySe d p bnd (PRunElab _ tm _) =
1973 bracket p funcAppPrec . group . align . hang 2 $
1975 prettySe (decD d) funcAppPrec bnd tm
1976 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1977 prettySe d p bnd _ = text "missing pretty-printer for term"
1979 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1980 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1981 where display (UN n) = T.unpack n
1982 display (MN _ n) = T.unpack n
1983 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1984 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1987 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1988 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1989 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1990 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1992 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1993 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1994 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1995 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1997 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1998 annName n = annotate (AnnName n Nothing Nothing Nothing)
2000 opStr :: Name -> String
2001 opStr (NS n _) = opStr n
2002 opStr (UN n) = T.unpack n
2004 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2005 slist' (Just d) _ _ _ | d <= 0 = Nothing
2007 | containsHole e = Nothing
2008 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2009 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2010 slist' d p bnd (PRef _ _ nil)
2011 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2012 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2013 | nsroot cons == sUN "::",
2014 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2016 Just tl' <- slist' (decD d) p bnd tl
2017 = Just (prettySe d startPrec bnd hd : tl')
2019 isImp (PImp {}) = True
2021 slist' _ _ _ tm = Nothing
2023 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2025 [] -> annotate (AnnData "" "") $ text "[]"
2026 [x] -> enclose left right . group $ x
2027 xs -> enclose left right .
2028 align . group . vsep .
2029 punctuate comma $ xs
2030 where left = (annotate (AnnData "" "") (text "["))
2031 right = (annotate (AnnData "" "") (text "]"))
2032 comma = (annotate (AnnData "" "") (text ","))
2033 slist _ _ _ _ = Nothing
2035 pairElts :: PTerm -> Maybe [PTerm]
2036 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2037 | otherwise = Just [x, y]
2038 pairElts _ = Nothing
2040 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2041 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2042 | otherwise = Just [(l, t), (Placeholder, r)]
2043 dPairElts _ = Nothing
2045 natns = "Prelude.Nat."
2047 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2049 | ppopt_desugarnats ppo = Nothing
2050 | otherwise = snat' d p e
2052 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2053 snat' (Just x) _ _ | x <= 0 = Nothing
2054 snat' d p (PRef _ _ z)
2055 | show z == (natns++"Z") || show z == "Z" = Just 0
2056 snat' d p (PApp _ s [PExp {getTm=n}])
2057 | show s == (natns++"S") || show s == "S",
2058 Just n' <- snat' (decD d) p n
2060 snat' _ _ _ = Nothing
2062 bracket outer inner doc
2063 | outer > inner = lparen <> doc <> rparen
2066 ellipsis = text "..."
2069 depth (Just d) = if d <= 0 then const ellipsis else id
2071 decD = fmap (\x -> x - 1)
2073 kwd = annotate AnnKeyword . text
2075 fixities :: M.Map String Fixity
2076 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2078 getFixity :: String -> Maybe Fixity
2079 getFixity = flip M.lookup fixities
2081-- | Strip away namespace information
2082basename :: Name -> Name
2083basename (NS n _) = basename n
2086-- | Determine whether a name was the one inserted for a hole or guess
2087-- by the delaborator
2088isHoleName :: Name -> Bool
2089isHoleName (UN n) = n == T.pack "[__]"
2092-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2093containsHole :: PTerm -> Bool
2094containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2096-- | Pretty-printer helper for names that attaches the correct annotations
2097prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2098 -> Bool -- ^ whether to show namespaces
2099 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2100 -> Name -- ^ the name to pprint
2101 -> Doc OutputAnnotation
2102prettyName infixParen showNS bnd n
2103 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2104 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2105 | (UN n') <- n, T.unpack n' == "_" = text "_"
2106 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2107 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2108 where fullName = text nameSpace <> parenthesise (text (baseName n))
2109 baseName (UN n) = T.unpack n
2110 baseName (NS n ns) = baseName n
2111 baseName (MN i s) = T.unpack s
2112 baseName other = show other
2113 nameSpace = case n of
2114 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2116 isInfix = case baseName n of
2118 (c : _) -> not (isAlpha c)
2119 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2122showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2123showCImp ppo (PClause _ n l ws r w)
2124 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2125 <+> text "where" <+> text (show w)
2128 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2129showCImp ppo (PWith _ n l ws r pn w)
2130 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2131 <+> braces (text (show w))
2134 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2137showDImp :: PPOption -> PData -> Doc OutputAnnotation
2138showDImp ppo (PDatadecl n nfc ty cons)
2139 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2140 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2142showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2143showDecls o ds = vsep (map (showDeclImp o) ds)
2145showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2146showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2147showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2148 indent 2 (vsep (map (showCImp o) cs))
2149showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2150showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2151showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2152showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2153showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2154showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2155 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2156showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2157 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2158showDeclImp _ _ = text "..."
2159-- showDeclImp (PImport o) = "import " ++ o
2161getImps :: [PArg] -> [(Name, PTerm)]
2163getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2164getImps (_ : xs) = getImps xs
2166getExps :: [PArg] -> [PTerm]
2168getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2169getExps (_ : xs) = getExps xs
2171getShowArgs :: [PArg] -> [PArg]
2173getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2174getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2175 | PImp _ _ _ _ tm <- e
2176 , containsHole tm = e : getShowArgs xs
2177getShowArgs (_ : xs) = getShowArgs xs
2179getConsts :: [PArg] -> [PTerm]
2181getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2182getConsts (_ : xs) = getConsts xs
2184getAll :: [PArg] -> [PTerm]
2189showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2190 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2191 -> PPOption -- ^ pretty printing options
2192 -> Bool -- ^ whether to colourise
2193 -> Name -- ^ the term to show
2195showName ist bnd ppo colour n = case ist of
2196 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2197 Nothing -> showbasic n
2198 where name = if ppopt_impl ppo then show n else showbasic n
2199 showbasic n@(UN _) = showCG n
2200 showbasic (MN i s) = str s
2201 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2202 showbasic (SN s) = show s
2203 colourise n t = let ctxt' = fmap tt_ctxt ist in
2206 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2207 else colouriseBound t name
2208 | isDConName n ctxt -> colouriseData t name
2209 | isFnName n ctxt -> colouriseFun t name
2210 | isTConName n ctxt -> colouriseType t name
2211 -- The assumption is that if a name is not bound and does not exist in the
2212 -- global context, then we're somewhere in which implicit info has been lost
2213 -- (like error messages). Thus, unknown vars are colourised as implicits.
2214 | otherwise -> colouriseImplicit t name
2216showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2217 -> PTerm -- ^ the term to show
2219showTm ist = displayDecorated (consoleDecorate ist) .
2220 renderPretty 0.8 100000 .
2221 prettyImp (ppOptionIst ist)
2223-- | Show a term with implicits, no colours
2224showTmImpls :: PTerm -> String
2225showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2227-- | Show a term with specific options
2228showTmOpts :: PPOption -> PTerm -> String
2229showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2232instance Sized PTerm where
2233 size (PQuote rawTerm) = size rawTerm
2234 size (PRef fc _ name) = size name
2235 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2236 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2237 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2238 size (PTyped trm ty) = 1 + size trm + size ty
2239 size (PApp fc name args) = 1 + size args
2240 size (PAppBind fc name args) = 1 + size args
2241 size (PCase fc trm bdy) = 1 + size trm + size bdy
2242 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2243 size (PTrue fc _) = 1
2244 size (PResolveTC fc) = 1
2245 size (PRewrite fc by left right _) = 1 + size left + size right
2246 size (PPair fc _ _ left right) = 1 + size left + size right
2247 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2248 size (PAlternative _ a alts) = 1 + size alts
2249 size (PHidden hidden) = size hidden
2250 size (PUnifyLog tm) = size tm
2251 size (PDisamb _ tm) = size tm
2252 size (PNoImplicits tm) = size tm
2254 size (PUniverse _ _) = 1
2255 size (PConstant fc const) = 1 + size fc + size const
2256 size Placeholder = 1
2257 size (PDoBlock dos) = 1 + size dos
2258 size (PIdiom fc term) = 1 + size term
2259 size (PMetavar _ name) = 1
2260 size (PProof tactics) = size tactics
2261 size (PElabError err) = size err
2262 size PImpossible = 1
2265getPArity :: PTerm -> Int
2266getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2269-- Return all names, free or globally bound, in the given term.
2271allNamesIn :: PTerm -> [Name]
2272allNamesIn tm = nub $ ni 0 [] tm
2273 where -- TODO THINK added niTacImp, but is it right?
2274 ni 0 env (PRef _ _ n)
2275 | not (n `elem` env) = [n]
2276 ni 0 env (PPatvar _ n) = [n]
2277 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2278 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2279 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2280 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2281 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2282 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2283 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2284 ni 0 env (PHidden tm) = ni 0 env tm
2285 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2286 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2287 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2288 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2289 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2290 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2291 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2292 ni 0 env (PUnifyLog tm) = ni 0 env tm
2293 ni 0 env (PDisamb _ tm) = ni 0 env tm
2294 ni 0 env (PNoImplicits tm) = ni 0 env tm
2296 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2297 ni i env (PUnquote tm) = ni (i - 1) env tm
2298 ni i env tm = concatMap (ni i env) (children tm)
2300 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2304-- Return all names defined in binders in the given term
2305boundNamesIn :: PTerm -> [Name]
2306boundNamesIn tm = S.toList (ni 0 S.empty tm)
2307 where -- TODO THINK Added niTacImp, but is it right?
2308 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2309 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2310 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2311 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2312 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2313 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2314 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2315 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2316 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2317 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2318 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2319 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2320 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2321 ni 0 set (PAlternative ns a as) = niTms 0 set as
2322 ni 0 set (PHidden tm) = ni 0 set tm
2323 ni 0 set (PUnifyLog tm) = ni 0 set tm
2324 ni 0 set (PDisamb _ tm) = ni 0 set tm
2325 ni 0 set (PNoImplicits tm) = ni 0 set tm
2327 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2328 ni i set (PUnquote tm) = ni (i - 1) set tm
2330 ni i set tm = foldr (S.union . ni i set) set (children tm)
2332 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2333 niTms i set [] = set
2334 niTms i set (x : xs) = niTms i (ni i set x) xs
2336 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2337 niTacImp i set _ = set
2339-- Return names which are valid implicits in the given term (type).
2340implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2341implicitNamesIn uvars ist tm
2342 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2345 addImp n = do (imps, fns) <- get
2347 addFn n = do (imps, fns) <- get
2350 ni 0 env (PRef _ _ n@(NS _ _))
2351 | not (n `elem` env)
2352 -- Never implicitly bind if there's a namespace
2354 ni 0 env (PRef _ _ n)
2355 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2356 ni 0 env (PApp _ f@(PRef _ _ n) as)
2357 | n `elem` uvars = do ni 0 env f
2358 mapM_ (ni 0 env . getTm) as
2359 | otherwise = do case lookupTy n (tt_ctxt ist) of
2362 mapM_ (ni 0 env . getTm) as
2363 ni 0 env (PApp _ f as) = do ni 0 env f
2364 mapM_ (ni 0 env . getTm) as
2365 ni 0 env (PAppBind _ f as) = do ni 0 env f
2366 mapM_ (ni 0 env . getTm) as
2367 ni 0 env (PCase _ c os) = do ni 0 env c
2368 -- names in 'os', not counting the names bound in the cases
2369 mapM_ (ni 0 env . snd) os
2372 mapM_ (ni 0 env . fst) os
2374 put (nub imps \\ nub impsfst, fns)
2375 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2376 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2377 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2378 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2379 ni 0 env val; ni 0 (n:env) sc
2380 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2381 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2382 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2383 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2384 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2387 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2388 ni 0 env (PHidden tm) = ni 0 env tm
2389 ni 0 env (PUnifyLog tm) = ni 0 env tm
2390 ni 0 env (PDisamb _ tm) = ni 0 env tm
2391 ni 0 env (PNoImplicits tm) = ni 0 env tm
2393 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2394 maybe (return ()) (ni i env) ty
2395 ni i env (PUnquote tm) = ni (i - 1) env tm
2397 ni i env tm = mapM_ (ni i env) (children tm)
2399-- Return names which are free in the given term.
2400namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2401namesIn uvars ist tm = nub $ ni 0 [] tm
2403 ni 0 env (PRef _ _ n)
2404 | not (n `elem` env)
2405 = case lookupTy n (tt_ctxt ist) of
2407 _ -> [n | n `elem` (map fst uvars)]
2408 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2409 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2410 ni 0 env (PCase _ c os) = ni 0 env c ++
2411 -- names in 'os', not counting the names bound in the cases
2412 (nub (concatMap (ni 0 env . snd) os)
2413 \\ nub (concatMap (ni 0 env . fst) os))
2414 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2415 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2416 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2417 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2418 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2419 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2420 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2421 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2422 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2423 ni 0 env (PHidden tm) = ni 0 env tm
2424 ni 0 env (PUnifyLog tm) = ni 0 env tm
2425 ni 0 env (PDisamb _ tm) = ni 0 env tm
2426 ni 0 env (PNoImplicits tm) = ni 0 env tm
2428 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2429 ni i env (PUnquote tm) = ni (i - 1) env tm
2431 ni i env tm = concatMap (ni i env) (children tm)
2433 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2436-- Return which of the given names are used in the given term.
2438usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2439usedNamesIn vars ist tm = nub $ ni 0 [] tm
2440 where -- TODO THINK added niTacImp, but is it right?
2441 ni 0 env (PRef _ _ n)
2442 | n `elem` vars && not (n `elem` env)
2443 = case lookupDefExact n (tt_ctxt ist) of
2446 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2447 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2448 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2449 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2450 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2451 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2452 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2453 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2454 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2455 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2456 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2457 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2458 ni 0 env (PHidden tm) = ni 0 env tm
2459 ni 0 env (PUnifyLog tm) = ni 0 env tm
2460 ni 0 env (PDisamb _ tm) = ni 0 env tm
2461 ni 0 env (PNoImplicits tm) = ni 0 env tm
2463 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2464 ni i env (PUnquote tm) = ni (i - 1) env tm
2466 ni i env tm = concatMap (ni i env) (children tm)
2468 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2471-- Return the list of inaccessible (= dotted) positions for a name.
2472getErasureInfo :: IState -> Name -> [Int]
2473getErasureInfo ist n =
2474 case lookupCtxtExact n (idris_optimisation ist) of
2475 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