2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
9{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFoldable, DeriveFunctor,
10 DeriveGeneric, DeriveTraversable, FlexibleContexts,
11 FlexibleInstances, MultiParamTypeClasses, PatternGuards,
12 TypeSynonymInstances #-}
14module Idris.AbsSyntaxTree where
16import Idris.Core.Elaborate hiding (Tactic(..))
17import Idris.Core.Evaluate
19import Idris.Docstrings
21import IRTS.CodegenCommon
23import Util.DynamicLinker
29#if (MIN_VERSION_base(4,11,0))
30import Prelude hiding (Foldable, Traversable, (<$>), (<>))
32import Prelude hiding (Foldable, Traversable, (<$>))
35import Control.Applicative ((<|>))
36import qualified Control.Monad.Trans.Class as Trans (lift)
37import Control.Monad.Trans.Except
38import Control.Monad.Trans.State.Strict
40import Data.Data (Data)
42import Data.Foldable (Foldable)
43import Data.Function (on)
44import Data.Generics.Uniplate.Data (children, universe)
45import Data.List hiding (group)
46import qualified Data.Map.Strict as M
47import Data.Maybe (mapMaybe, maybeToList)
48import qualified Data.Set as S
49import qualified Data.Text as T
50import Data.Traversable (Traversable)
52import GHC.Generics (Generic)
54data ElabWhat = ETypes | EDefns | EAll
57-- | Data to pass to recursively called elaborators; e.g. for where blocks,
58-- paramaterised declarations, etc.
60-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
61-- so that we can have mutually recursive elaborators in separate modules without
62-- having to muck about with cyclic modules.
63data ElabInfo = EInfo {
64 params :: [(Name, PTerm)]
65 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
66 , liftname :: Name -> Name
67 , namespace :: [String]
69 , constraintNS :: String -- ^ filename for adding to constraint variables
71 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
72 -- | We may, recursively, collect transformations to do on the rhs,
73 -- e.g. rewriting recursive calls to functions defined by 'with'
74 , rhs_trans :: PTerm -> PTerm
75 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
79toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
81toplevelWith :: String -> ElabInfo
82toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
84eInfoNames :: ElabInfo -> [Name]
85eInfoNames info = map fst (params info) ++ M.keys (inblock info)
87data IOption = IOption {
89 , opt_logcats :: [LogCat] -- ^ List of logging categories.
90 , opt_typecase :: Bool
91 , opt_typeintype :: Bool
92 , opt_coverage :: Bool
93 , opt_showimp :: Bool -- ^ show implicits
94 , opt_errContext :: Bool
97 , opt_nobanner :: Bool
99 , opt_codegen :: Codegen
100 , opt_outputTy :: OutputType
101 , opt_ibcsubdir :: FilePath
102 , opt_importdirs :: [FilePath]
103 , opt_sourcedirs :: [FilePath]
104 , opt_triple :: String
106 , opt_cmdline :: [Opt] -- ^ remember whole command line
107 , opt_origerr :: Bool
108 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
109 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
110 , opt_optimise :: [Optimisation]
111 , opt_printdepth :: Maybe Int
112 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
113 , opt_desugarnats :: Bool
114 , opt_autoimpls :: Bool
115 } deriving (Show, Eq, Generic)
117defaultOpts :: IOption
118defaultOpts = IOption { opt_logLevel = 0
120 , opt_typecase = False
121 , opt_typeintype = False
122 , opt_coverage = True
123 , opt_showimp = False
124 , opt_errContext = False
127 , opt_nobanner = False
129 , opt_codegen = Via IBCFormat "c"
130 , opt_outputTy = Executable
132 , opt_importdirs = []
133 , opt_sourcedirs = []
137 , opt_origerr = False
138 , opt_autoSolve = True
139 , opt_autoImport = []
140 , opt_optimise = defaultOptimise
141 , opt_printdepth = Just 5000
142 , opt_evaltypes = True
143 , opt_desugarnats = False
144 , opt_autoimpls = True
147data PPOption = PPOption {
148 ppopt_impl :: Bool -- ^ whether to show implicits
149 , ppopt_desugarnats :: Bool
150 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
151 , ppopt_depth :: Maybe Int
152 , ppopt_displayrig :: Bool -- ^ whether to display multiplicities in binders
157defaultOptimise :: [Optimisation]
160-- | Pretty printing options with default verbosity.
161defaultPPOption :: PPOption
162defaultPPOption = PPOption {
164 , ppopt_desugarnats = False
165 , ppopt_pinames = False
166 , ppopt_depth = Nothing
167 , ppopt_displayrig = False
170-- | Pretty printing options with the most verbosity.
171verbosePPOption :: PPOption
172verbosePPOption = PPOption {
174 , ppopt_desugarnats = True
175 , ppopt_pinames = True
176 , ppopt_depth = Nothing
177 , ppopt_displayrig = False
180-- | Get pretty printing options from the big options record.
181ppOption :: IOption -> PPOption
182ppOption opt = PPOption {
183 ppopt_impl = opt_showimp opt
184 , ppopt_pinames = False
185 , ppopt_depth = opt_printdepth opt
186 , ppopt_desugarnats = opt_desugarnats opt
187 , ppopt_displayrig = False
190-- | Get pretty printing options from an idris state record.
191ppOptionIst :: IState -> PPOption
192ppOptionIst = ppOption . idris_options
195-- | The output mode in use
196data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
197 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
201-- | If a function has no totality annotation, what do we assume?
202data DefaultTotality = DefaultCheckingTotal -- ^ Total
203 | DefaultCheckingPartial -- ^ Partial
204 | DefaultCheckingCovering -- ^Total coverage, but may diverge
205 deriving (Show, Eq, Generic)
207-- | Configuration options for interactive editing.
208data InteractiveOpts = InteractiveOpts {
209 interactiveOpts_indentWith :: Int
210 , interactiveOpts_indentClause :: Int
211} deriving (Show, Generic)
213-- | The global state used in the Idris monad
214data IState = IState {
215 tt_ctxt :: Context -- ^ All the currently defined names and their terms
216 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
217 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
218 , idris_implicits :: Ctxt [PArg]
219 , idris_statics :: Ctxt [Bool]
220 , idris_interfaces :: Ctxt InterfaceInfo
221 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
222 , idris_records :: Ctxt RecordInfo
223 , idris_dsls :: Ctxt DSL
224 , idris_optimisation :: Ctxt OptInfo
225 , idris_datatypes :: Ctxt TypeInfo
226 , idris_namehints :: Ctxt [Name]
228 -- | list of lhs/rhs, and a list of missing clauses. These are not
230 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
231 , idris_flags :: Ctxt [FnOpt]
232 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
233 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
235 -- | module documentation is saved in a special MN so the context
236 -- mechanism can be used for disambiguation.
237 , idris_moduledocs :: Ctxt (Docstring DocTerm)
238 , idris_tyinfodata :: Ctxt TIData
239 , idris_fninfo :: Ctxt FnInfo
240 , idris_transforms :: Ctxt [(Term, Term)]
241 , idris_autohints :: Ctxt [Name]
242 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
243 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
244 , idris_totcheckfail :: [(FC, String)]
245 , idris_options :: IOption
247 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
249 -- | The currently defined but not proven metavariables. The Int is
250 -- the number of vars to display as a context, the Maybe Name is its
251 -- top-level function, the [Name] is the list of local variables
252 -- available for proof search and the Bools are whether :p is
253 -- allowed, and whether the variable is definable at all
254 -- (Metavariables are not definable if they are applied in a term
255 -- which still has hole bindings)
256 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
257 , idris_coercions :: [Name]
258 , idris_errRev :: [(Term, Term)]
259 , idris_errReduce :: [Name]
260 , syntax_rules :: SyntaxRules
261 , syntax_keywords :: [String]
262 , imported :: [FilePath] -- ^ The imported modules
263 , idris_scprims :: [(Name, (Int, PrimFn))]
264 , idris_objs :: [(Codegen, FilePath)]
265 , idris_libs :: [(Codegen, String)]
266 , idris_cgflags :: [(Codegen, String)]
267 , idris_hdrs :: [(Codegen, String)]
268 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
269 , proof_list :: [(Name, (Bool, [String]))]
270 , errSpan :: Maybe FC
271 , parserWarnings :: [(FC, Err)]
272 , lastParse :: Maybe Name
273 , indent_stack :: [Int]
274 , brace_stack :: [Maybe Int]
275 , idris_parsedSpan :: Maybe FC
276 , hide_list :: Ctxt Accessibility
277 , default_access :: Accessibility
278 , default_total :: DefaultTotality
279 , ibc_write :: [IBCWrite]
280 , compiled_so :: Maybe String
281 , idris_dynamic_libs :: [DynamicLib]
282 , idris_language_extensions :: [LanguageExt]
283 , idris_outputmode :: OutputMode
284 , idris_colourRepl :: Bool
285 , idris_colourTheme :: ColourTheme
286 , idris_errorhandlers :: [Name] -- ^ Global error handlers
287 , idris_nameIdx :: (Int, Ctxt (Int, Name))
288 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
289 , module_aliases :: M.Map [T.Text] [T.Text]
290 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
291 , idris_postulates :: S.Set Name
292 , idris_externs :: S.Set (Name, Int)
293 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
295 -- | List of names that were defined in the repl, and can be re-/un-defined
296 , idris_repl_defs :: [Name]
298 -- | Stack of names currently being elaborated, Bool set if it's an
299 -- implementation (implementations appear twice; also as a function name)
300 , elab_stack :: [(Name, Bool)]
303 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
304 , idris_exports :: [Name] -- ^ Functions with ExportList
305 , idris_highlightedRegions :: S.Set (FC', OutputAnnotation) -- ^ Highlighting information to output
306 , idris_parserHighlights :: S.Set (FC', OutputAnnotation) -- ^ Highlighting information from the parser
307 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
308 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
309 , idris_ttstats :: M.Map Term (Int, Term)
310 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
311 , idris_interactiveOpts :: InteractiveOpts
314-- Required for parsers library, and therefore trifecta
315instance Show IState where
316 show = const "{internal state}"
318data SizeChange = Smaller | Same | Bigger | Unknown
319 deriving (Show, Eq, Generic)
321deriving instance Binary SizeChange
324type SCGEntry = (Name, [Maybe (Int, SizeChange)])
325type UsageReason = (Name, Int) -- fn_name, its_arg_number
327data CGInfo = CGInfo {
328 calls :: [Name] -- Immediate calls
329 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
331 , usedpos :: [(Int, [UsageReason])]
332 } deriving (Show, Generic)
334deriving instance Binary CGInfo
338primDefs = [ sUN "unsafePerformPrimIO"
339 , sUN "mkLazyForeignPrim"
340 , sUN "mkForeignPrim"
342 , sUN "assert_unreachable"
346-- information that needs writing for the current module's .ibc file
347data IBCWrite = IBCFix FixDecl
352 | IBCImplementation Bool Bool Name Name
359 | IBCImport (Bool, FilePath) -- ^ True = import public
360 | IBCImportDir FilePath
361 | IBCSourceDir FilePath
362 | IBCObj Codegen FilePath
363 | IBCLib Codegen String
364 | IBCCGFlag Codegen String
366 | IBCHeader Codegen String
367 | IBCAccess Name Accessibility
368 | IBCMetaInformation Name MetaInformation
369 | IBCTotal Name Totality
370 | IBCInjective Name Injectivity
372 | IBCFnInfo Name FnInfo
373 | IBCTrans Name (Term, Term)
374 | IBCErrRev (Term, Term)
379 | IBCDef Name -- ^ The main context.
380 | IBCNameHint (Name, Name)
381 | IBCLineApp FilePath Int PTerm
382 | IBCErrorHandler Name
383 | IBCFunctionErrorHandler Name Name Name
385 | IBCExtern (Name, Int)
386 | IBCTotCheckErr FC String
388 | IBCModDocs Name -- ^ The name is the special name used to track module docs
389 | IBCUsage (Name, Int)
391 | IBCAutoHint Name Name
392 | IBCDeprecate Name String
393 | IBCFragile Name String
394 | IBCConstraint FC UConstraint
395 | IBCImportHash FilePath Int
396 deriving (Show, Generic)
398initialInteractiveOpts :: InteractiveOpts
399initialInteractiveOpts = InteractiveOpts {
400 interactiveOpts_indentWith = 2
401 , interactiveOpts_indentClause = 2
404-- | The initial state for the compiler
406idrisInit = IState initContext S.empty []
407 emptyContext emptyContext emptyContext [] emptyContext
408 emptyContext emptyContext emptyContext emptyContext
409 emptyContext emptyContext emptyContext emptyContext
410 emptyContext emptyContext emptyContext emptyContext
412 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
413 [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
414 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
415 AutomaticWidth S.empty S.empty [] [] [] M.empty [] S.empty S.empty
416 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
419-- | The monad for the main REPL - reading and processing files and
420-- updating global state (hence the IO inner monad).
423-- type Idris = WriterT [Either String (IO ())] (State IState a))
426type Idris = StateT IState (ExceptT Err IO)
428catchError :: Idris a -> (Err -> Idris a) -> Idris a
429catchError = liftCatch catchE
431throwError :: Err -> Idris a
432throwError = Trans.lift . throwE
434-- Commands in the REPL
439data ElabShellCmd = EQED
447 | EDocStr (Either Name Const)
453-- Parsed declarations
455data Fixity = Infixl { prec :: Int }
456 | Infixr { prec :: Int }
457 | InfixN { prec :: Int }
458 | PrefixN { prec :: Int }
459 deriving (Eq, Generic)
461deriving instance Binary Fixity
464instance Show Fixity where
465 show (Infixl i) = "infixl " ++ show i
466 show (Infixr i) = "infixr " ++ show i
467 show (InfixN i) = "infix " ++ show i
468 show (PrefixN i) = "prefix " ++ show i
470data FixDecl = Fix Fixity String
471 deriving (Eq, Generic)
473instance Show FixDecl where
474 show (Fix f s) = show f ++ " " ++ s
477deriving instance Binary FixDecl
480instance Ord FixDecl where
481 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
484data Static = Static | Dynamic
485 deriving (Show, Eq, Ord, Data, Generic, Typeable)
487deriving instance Binary Static
490-- ^ Mark bindings with their explicitness, and laziness
491data Plicity = Imp { pargopts :: [ArgOpt]
494 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
495 , pinsource :: Bool -- ^ Explicitly written in source
498 | Exp { pargopts :: [ArgOpt]
500 , pparam :: Bool -- ^ this is a param (rather than index)
503 | Constraint { pargopts :: [ArgOpt]
507 | TacImp { pargopts :: [ArgOpt]
512 deriving (Show, Eq, Ord, Data, Generic, Typeable)
515deriving instance Binary Plicity
518is_scoped :: Plicity -> Maybe ImplicitInfo
519is_scoped (Imp _ _ _ s _ _) = s
524impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
525-- Machine generated top level implicit
527impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
531forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
532forall_constraint :: Plicity
533forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
536expl = Exp [] Dynamic False RigW
538expl_param = Exp [] Dynamic True RigW
539expl_linear :: Plicity
540expl_linear = Exp [] Dynamic False Rig1
543constraint = Constraint [] Static RigW
545tacimpl :: PTerm -> Plicity
546tacimpl t = TacImp [] Dynamic t RigW
548data FnOpt = Inlinable -- ^ always evaluate when simplifying
549 | TotalFn | PartialFn | CoveringFn
550 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
553 -- | interface dictionary, eval only when a function
554 -- argument, and further evaluation results.
556 | OverlappingDictionary -- ^ Interface dictionary which may overlap
557 | Implicit -- ^ implicit coercion
558 | NoImplicit -- ^ do not apply implicit coercions
559 | CExport String -- ^ export, with a C name
560 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
561 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
562 | ErrorReduce -- ^ unfold definition before showing an error
563 | Reflection -- ^ a reflecting function, compile-time only
564 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
565 | Constructor -- ^ Data constructor type
566 | AutoHint -- ^ use in auto implicit search
567 | PEGenerated -- ^ generated by partial evaluator
568 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
569 deriving (Show, Eq, Generic)
571deriving instance Binary FnOpt
576inlinable :: FnOpts -> Bool
577inlinable = elem Inlinable
579dictionary :: FnOpts -> Bool
580dictionary = elem Dictionary
583-- | Type provider - what to provide
584data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
585 | ProvPostulate t -- ^ goal type must be Type, so only term
586 deriving (Show, Eq, Functor, Generic)
588type ProvideWhat = ProvideWhat' PTerm
590-- | Top-level declarations such as compiler directives, definitions,
591-- datatypes and interfaces.
593 -- | Fixity declaration
594 = PFix FC Fixity [String]
595 -- | Type declaration (last FC is precise name location)
596 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
597 -- | Postulate, second FC is precise name location
598 | PPostulate Bool -- external def if true
599 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
601 | PClauses FC FnOpts Name [PClause' t]
602 -- | Top level constant
604 -- | Data declaration.
605 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
607 | PParams FC [(Name, t)] [PDecl' t]
608 -- | Open block/declaration
609 | POpenInterfaces FC [Name] [PDecl' t]
610 -- | New namespace, where FC is accurate location of the namespace
612 | PNamespace String FC [PDecl' t]
614 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
616 FC -- Record name precise location
617 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
618 [(Name, Docstring (Either Err t))] -- Param Docs
619 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
620 (Maybe (Name, FC)) -- Optional constructor name and location
621 (Docstring (Either Err t)) -- Constructor doc
622 SyntaxInfo -- Constructor SyntaxInfo
624 -- | Interface: arguments are documentation, syntax info, source
625 -- location, constraints, interface name, interface name location,
626 -- parameters, method declarations, optional constructor name
627 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
628 [(Name, t)] -- constraints
629 Name -- interface name
630 FC -- accurate location of interface name
631 [(Name, FC, t)] -- parameters and precise locations
632 [(Name, Docstring (Either Err t))] -- parameter docstrings
633 [(Name, FC)] -- determining parameters and precise locations
634 [PDecl' t] -- declarations
635 (Maybe (Name, FC)) -- implementation constructor name and location
636 (Docstring (Either Err t)) -- implementation constructor docs
638 -- | Implementation declaration: arguments are documentation, syntax
639 -- info, source location, constraints, interface name, parameters, full
640 -- Implementation type, optional explicit name, and definitions
641 | PImplementation (Docstring (Either Err t)) -- Implementation docs
642 [(Name, Docstring (Either Err t))] -- Parameter docs
644 FC [(Name, t)] -- constraints
645 [Name] -- parent dictionaries to search for constraints
649 FC -- precise location of interface
651 [(Name, t)] -- Extra names in scope in the body
652 t -- full Implementation type
653 (Maybe Name) -- explicit name
655 | PDSL Name (DSL' t) -- ^ DSL declaration
656 | PSyntax FC Syntax -- ^ Syntax definition
657 | PMutual FC [PDecl' t] -- ^ Mutual block
658 | PDirective Directive -- ^ Compiler directive.
660 -- | Type provider. The first t is the type, the second is the
661 -- term. The second FC is precise highlighting location.
662 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
664 -- | Source-to-source transformation rule. If bool is True, lhs and
665 -- rhs must be convertible.
666 | PTransform FC Bool t t
668 -- | FC is decl-level, for errors, and Strings represent the
670 | PRunElabDecl FC t [String]
671 deriving (Functor, Generic)
673deriving instance Binary PDecl'
676-- | The set of source directives
677data Directive = DLib Codegen String
678 | DLink Codegen String
679 | DFlag Codegen String
680 | DInclude Codegen String
685 | DSetTotal Name -- assert totality after checking
686 | DAccess Accessibility
687 | DDefault DefaultTotality
689 | DDynamicLibs [String]
690 | DNameHint Name FC [(Name, FC)]
691 | DErrorHandlers Name FC Name FC [(Name, FC)]
692 | DLanguage LanguageExt
693 | DDeprecate Name String
694 | DFragile Name String
695 | DAutoImplicits Bool
699-- | A set of instructions for things that need to happen in IState
700-- after a term elaboration when there's been reflected elaboration.
701data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
702 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
703 | RAddImplementation Name Name
704 | RDatatypeDeclInstrs Name [PArg]
705 -- | Datatype, constructors
706 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
709-- | For elaborator state
710data EState = EState {
711 case_decls :: [(Name, PDecl)]
712 , delayed_elab :: [(Int, Elab' EState ())]
713 , new_tyDecls :: [RDeclInstructions]
714 , highlighting :: S.Set (FC', OutputAnnotation)
715 , auto_binds :: [Name] -- ^ names bound as auto implicits
716 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
720initEState = EState [] [] [] S.empty [] []
722type ElabD a = Elab' EState a
724highlightSource :: FC -> OutputAnnotation -> ElabD ()
725highlightSource fc annot =
726 updateAux (\aux -> aux { highlighting = S.insert (FC' fc, annot) (highlighting aux) })
728-- | One clause of a top-level definition. Term arguments to constructors are:
730-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
732-- 2. The list of extra 'with' patterns
734-- 3. The right-hand side
736-- 4. The where block (PDecl' t)
738data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
739 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
740 | PClauseR FC [t] t [PDecl' t]
741 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
742 deriving (Functor, Generic)
744deriving instance Binary PClause'
749 -- | Data declaration
750 PDatadecl { d_name :: Name -- ^ The name of the datatype
751 , d_name_fc :: FC -- ^ The precise location of the type constructor name
752 , d_tcon :: t -- ^ Type constructor
753 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
755 -- | "Placeholder" for data whose constructors are defined later
756 | PLaterdecl { d_name :: Name
759 } deriving (Functor, Generic)
761-- | Transform the FCs in a PData and its associated terms. The first
762-- function transforms the general-purpose FCs, and the second
763-- transforms those that are used for semantic source highlighting, so
764-- they can be treated specially.
765mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
766mapPDataFC f g (PDatadecl n nfc tycon ctors) =
767 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
768 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
769 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
770mapPDataFC f g (PLaterdecl n nfc tycon) =
771 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
773deriving instance Binary PData'
776-- Handy to get a free function for applying PTerm -> PTerm functions
777-- across a program, by deriving Functor
779type PDecl = PDecl' PTerm
780type PData = PData' PTerm
781type PClause = PClause' PTerm
783-- | Transform the FCs in a PTerm. The first function transforms the
784-- general-purpose FCs, and the second transforms those that are used
785-- for semantic source highlighting, so they can be treated specially.
786mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
787mapPDeclFC f g (PFix fc fixity ops) =
788 PFix (f fc) fixity ops
789mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
790 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
791mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
792 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
794mapPDeclFC f g (PClauses fc opts n clauses) =
795 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
796mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
797mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
798 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
799mapPDeclFC f g (PParams fc params decls) =
801 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
802 (map (mapPDeclFC f g) decls)
803mapPDeclFC f g (POpenInterfaces fc ifs decls) =
804 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
805mapPDeclFC f g (PNamespace ns fc decls) =
806 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
807mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
808 PRecord doc syn (f fc) opts n (g nfc)
809 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
811 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
812 plic, mapPTermFC f g ty, fdoc))
814 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
817mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
818 PInterface doc syn (f fc)
819 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
820 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
821 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
822 (map (mapPDeclFC f g) body)
823 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
825mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
826 PImplementation doc paramDocs syn (f fc)
827 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
828 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
829 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
830 (mapPTermFC f g implTy)
832 (map (mapPDeclFC f g) body)
833mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
834mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
836 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
837 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
838mapPDeclFC f g (PMutual fc decls) =
839 PMutual (f fc) (map (mapPDeclFC f g) decls)
840mapPDeclFC f g (PDirective d) =
843 DNameHint n nfc ns ->
844 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
845 DErrorHandlers n nfc n' nfc' ns ->
846 DErrorHandlers n (g nfc) n' (g nfc') $
847 map (\(an, anfc) -> (an, g anfc)) ns
848mapPDeclFC f g (PProvider doc syn fc nfc what n) =
849 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
850mapPDeclFC f g (PTransform fc safe l r) =
851 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
852mapPDeclFC f g (PRunElabDecl fc script ns) =
853 PRunElabDecl (f fc) (mapPTermFC f g script) ns
855-- | Get all the names declared in a declaration
856declared :: PDecl -> [Name]
857declared (PFix _ _ _) = []
858declared (PTy _ _ _ _ _ n fc t) = [n]
859declared (PPostulate _ _ _ _ _ _ n t) = [n]
860declared (PClauses _ _ n _) = [] -- not a declaration
861declared (PCAF _ n _) = [n]
862declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
863 where fstt (_, _, a, _, _, _, _) = a
864declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
865declared (PParams _ _ ds) = concatMap declared ds
866declared (POpenInterfaces _ _ ds) = concatMap declared ds
867declared (PNamespace _ _ ds) = concatMap declared ds
868declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
869declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
870declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
874declared (PDSL n _) = [n]
875declared (PSyntax _ _) = []
876declared (PMutual _ ds) = concatMap declared ds
877declared (PDirective _) = []
880-- get the names declared, not counting nested parameter blocks
881tldeclared :: PDecl -> [Name]
882tldeclared (PFix _ _ _) = []
883tldeclared (PTy _ _ _ _ _ n _ t) = [n]
884tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
885tldeclared (PClauses _ _ n _) = [] -- not a declaration
886tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
887tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
888 where fstt (_, _, a, _, _, _, _) = a
889tldeclared (PParams _ _ ds) = []
890tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
891tldeclared (PMutual _ ds) = concatMap tldeclared ds
892tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
893tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
894tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
900defined :: PDecl -> [Name]
901defined (PFix _ _ _) = []
902defined (PTy _ _ _ _ _ n _ t) = []
903defined (PPostulate _ _ _ _ _ _ n t) = []
904defined (PClauses _ _ n _) = [n] -- not a declaration
905defined (PCAF _ n _) = [n]
906defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
907 where fstt (_, _, a, _, _, _, _) = a
908defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
909defined (PParams _ _ ds) = concatMap defined ds
910defined (POpenInterfaces _ _ ds) = concatMap defined ds
911defined (PNamespace _ _ ds) = concatMap defined ds
912defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
913defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
914defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
918defined (PDSL n _) = [n]
919defined (PSyntax _ _) = []
920defined (PMutual _ ds) = concatMap defined ds
921defined (PDirective _) = []
924updateN :: [(Name, Name)] -> Name -> Name
925updateN ns n | Just n' <- lookup n ns = n'
928updateNs :: [(Name, Name)] -> PTerm -> PTerm
930updateNs ns t = mapPT updateRef t
931 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
937 deriving (Eq, Show, Ord, Data, Typeable, Generic)
939-- | High level language terms
940data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
941 -- high-level language
943 -- ^ A reference to a variable. The FC is its precise
944 -- source location for highlighting. The list of FCs is a
945 -- collection of additional highlighting locations.
946 | PInferRef FC [FC] Name -- ^ A name to be defined later
947 | PPatvar FC Name -- ^ A pattern variable
948 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
949 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
950 | PLet FC RigCount Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
951 | PTyped PTerm PTerm -- ^ Term with explicit type
952 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
953 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
954 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
955 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
956 | PMatchApp FC Name -- ^ Make an application by type matching
957 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
958 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
959 | PTrue FC PunInfo -- ^ Unit type..?
960 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
961 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
962 -- ^ "rewrite" syntax, with optional rewriting function and
963 -- optional result type
964 | PPair FC [FC] PunInfo PTerm PTerm
965 -- ^ A pair (a, b) and whether it's a product type or a
966 -- pair (solved by elaboration). The list of FCs is its
968 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
969 -- ^ A dependent pair (tm : a ** b) and whether it's a
970 -- sigma type or a pair that inhabits one (solved by
971 -- elaboration). The [FC] is its punctuation.
972 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
973 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
974 | PHidden PTerm -- ^ Irrelevant or hidden pattern
975 | PType FC -- ^ 'Type' type
976 | PUniverse FC Universe -- ^ Some universe
977 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
978 | PConstant FC Const -- ^ Builtin types
979 | Placeholder -- ^ Underscore
980 | PDoBlock [PDo] -- ^ Do notation
981 | PIdiom FC PTerm -- ^ Idiom brackets
982 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
983 | PProof [PTactic] -- ^ Proof script
984 | PTactics [PTactic] -- ^ As PProof, but no auto solving
985 | PElabError Err -- ^ Error to report on elaboration
986 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
987 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
988 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
989 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
990 | PNoImplicits PTerm -- ^ never run implicit converions on the term
991 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
992 | PUnquote PTerm -- ^ ~Term
993 | PQuoteName Name Bool FC
994 -- ^ `{n} where the FC is the precise highlighting for
995 -- the name in particular. If the Bool is False, then
996 -- it's `{{n}} and the name won't be resolved.
997 | PRunElab FC PTerm [String]
998 -- ^ %runElab tm - New-style proof script. Args are
999 -- location, script, enclosing namespace.
1000 | PConstSugar FC PTerm
1001 -- ^ A desugared constant. The FC is a precise source
1002 -- location that will be used to highlight it later.
1003 deriving (Eq, Ord, Data, Typeable, Generic)
1005data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1008 deriving (Eq, Ord, Data, Generic, Typeable)
1010-- | Transform the FCs in a PTerm. The first function transforms the
1011-- general-purpose FCs, and the second transforms those that are used
1012-- for semantic source highlighting, so they can be treated specially.
1013mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1014mapPTermFC f g (PQuote q) = PQuote q
1015mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1016mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1017mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1018mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1019mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1020mapPTermFC f g (PLet fc rc n fc' t1 t2 t3) = PLet (f fc) rc n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1021mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1022mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1023mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1024mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1025mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1026mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1027mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1028mapPTermFC 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)
1029mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1030mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1031mapPTermFC 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)
1032mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1033mapPTermFC 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)
1034mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1035mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1036mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1037mapPTermFC f g (PType fc) = PType (f fc)
1038mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1039mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1040mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1041mapPTermFC f g Placeholder = Placeholder
1042mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1043 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1044 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1045 mapPDoFC (DoBindP fc t1 t2 alts) =
1046 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1047 mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1048 mapPDoFC (DoLetP fc t1 t2 alts) =
1049 DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1050 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1051mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1052mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1053mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1054mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1055mapPTermFC f g (PElabError err) = PElabError err
1056mapPTermFC f g PImpossible = PImpossible
1057mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1058mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1059mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1060mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1061mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1062mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1063mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1064mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1065mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1068dg instance Binary PTerm
1071mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1072mapPT f t = f (mpt t) where
1073 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1074 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1075 mpt (PLet fc rc n nfc ty v s) = PLet fc rc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1076 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1077 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1078 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1079 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1080 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1081 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1082 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1083 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1084 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1085 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1086 mpt (PHidden t) = PHidden (mapPT f t)
1087 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1088 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1089 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1090 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1091 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1092 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1093 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1097data PTactic' t = Intro [Name] | Intros | Focus Name
1098 | Refine Name [Bool] | Rewrite t | DoUnify
1103 | LetTac Name t | LetTacTy Name t t
1104 | Exact t | Compute | Trivial | TCImplementation
1105 | ProofSearch Bool Bool Int (Maybe Name)
1106 [Name] -- allowed local names
1108 -- ^ the bool is whether to search recursively
1111 | ProofState | ProofTerm | Undo
1112 | Try (PTactic' t) (PTactic' t)
1113 | TSeq (PTactic' t) (PTactic' t)
1114 | ApplyTactic t -- see Language.Reflection module
1118 | GoalType String (PTactic' t)
1121 | TDocStr (Either Name Const)
1124 | TFail [ErrorReportPart]
1127 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1129deriving instance Binary PTactic'
1131instance Sized a => Sized (PTactic' a) where
1132 size (Intro nms) = 1 + size nms
1134 size (Focus nm) = 1 + size nm
1135 size (Refine nm bs) = 1 + size nm + length bs
1136 size (Rewrite t) = 1 + size t
1137 size (LetTac nm t) = 1 + size nm + size t
1138 size (Exact t) = 1 + size t
1146 size (Try l r) = 1 + size l + size r
1147 size (TSeq l r) = 1 + size l + size r
1148 size (ApplyTactic t) = 1 + size t
1149 size (Reflect t) = 1 + size t
1150 size (Fill t) = 1 + size t
1154 size (TFail ts) = 1 + size ts
1157 size (Equiv t) = 1 + size t
1158 size (Claim x y) = 1 + size x + size y
1160 size (MatchRefine x) = 1 + size x
1161 size (LetTacTy x y z) = 1 + size x + size y + size z
1162 size TCImplementation = 1
1164type PTactic = PTactic' PTerm
1166data PDo' t = DoExp FC t
1167 | DoBind FC Name FC t -- ^ second FC is precise name location
1168 | DoBindP FC t t [(t,t)]
1169 | DoLet FC RigCount Name FC t t -- ^ second FC is precise name location
1170 | DoLetP FC t t [(t,t)]
1171 | DoRewrite FC t -- rewrite in do block
1172 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1174deriving instance Binary PDo'
1177instance Sized a => Sized (PDo' a) where
1178 size (DoExp fc t) = 1 + size fc + size t
1179 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1180 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1181 size (DoLet fc rc nm nfc l r) = 1 + size fc + size nm + size l + size r
1182 size (DoLetP fc l r alts) = 1 + size fc + size l + size r + size alts
1183 size (DoRewrite fc h) = 1 + size fc + size h
1185type PDo = PDo' PTerm
1187-- The priority gives a hint as to elaboration order. Best to elaborate
1188-- things early which will help give a more concrete type to other
1189-- variables, e.g. a before (interpTy a).
1191data PArg' t = PImp { priority :: Int
1192 , machine_inf :: Bool -- ^ true if the machine inferred it
1193 , argopts :: [ArgOpt]
1197 | PExp { priority :: Int
1198 , argopts :: [ArgOpt]
1202 | PConstraint { priority :: Int
1203 , argopts :: [ArgOpt]
1207 | PTacImplicit { priority :: Int
1208 , argopts :: [ArgOpt]
1213 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1215data ArgOpt = AlwaysShow
1219 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1221instance Sized a => Sized (PArg' a) where
1222 size (PImp p _ l nm trm) = 1 + size nm + size trm
1223 size (PExp p l nm trm) = 1 + size nm + size trm
1224 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1225 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1228deriving instance Binary PArg'
1231pimp n t mach = PImp 1 mach [] n t
1232pexp t = PExp 1 [] (sMN 0 "arg") t
1233pconst t = PConstraint 1 [] (sMN 0 "carg") t
1234ptacimp n s t = PTacImplicit 2 [] n s t
1236type PArg = PArg' PTerm
1238-- | Get the highest FC in a term, if one exists
1239highestFC :: PTerm -> Maybe FC
1240highestFC (PQuote _) = Nothing
1241highestFC (PRef fc _ _) = Just fc
1242highestFC (PInferRef fc _ _) = Just fc
1243highestFC (PPatvar fc _) = Just fc
1244highestFC (PLam fc _ _ _ _) = Just fc
1245highestFC (PPi _ _ _ _ _) = Nothing
1246highestFC (PLet fc _ _ _ _ _ _) = Just fc
1247highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1248highestFC (PApp fc _ _) = Just fc
1249highestFC (PAppBind fc _ _) = Just fc
1250highestFC (PMatchApp fc _) = Just fc
1251highestFC (PCase fc _ _) = Just fc
1252highestFC (PIfThenElse fc _ _ _) = Just fc
1253highestFC (PTrue fc _) = Just fc
1254highestFC (PResolveTC fc) = Just fc
1255highestFC (PRewrite fc _ _ _ _) = Just fc
1256highestFC (PPair fc _ _ _ _) = Just fc
1257highestFC (PDPair fc _ _ _ _ _) = Just fc
1258highestFC (PAs fc _ _) = Just fc
1259highestFC (PAlternative _ _ args) =
1260 case mapMaybe highestFC args of
1263highestFC (PHidden _) = Nothing
1264highestFC (PType fc) = Just fc
1265highestFC (PUniverse _ _) = Nothing
1266highestFC (PGoal fc _ _ _) = Just fc
1267highestFC (PConstant fc _) = Just fc
1268highestFC Placeholder = Nothing
1269highestFC (PDoBlock lines) =
1270 case map getDoFC lines of
1274 getDoFC (DoExp fc t) = fc
1275 getDoFC (DoBind fc nm nfc t) = fc
1276 getDoFC (DoBindP fc l r alts) = fc
1277 getDoFC (DoLet fc rc nm nfc l r) = fc
1278 getDoFC (DoLetP fc l r alts) = fc
1279 getDoFC (DoRewrite fc h) = fc
1281highestFC (PIdiom fc _) = Just fc
1282highestFC (PMetavar fc _) = Just fc
1283highestFC (PProof _) = Nothing
1284highestFC (PTactics _) = Nothing
1285highestFC (PElabError _) = Nothing
1286highestFC PImpossible = Nothing
1287highestFC (PCoerced tm) = highestFC tm
1288highestFC (PDisamb _ opts) = highestFC opts
1289highestFC (PUnifyLog tm) = highestFC tm
1290highestFC (PNoImplicits tm) = highestFC tm
1291highestFC (PQuasiquote _ _) = Nothing
1292highestFC (PUnquote tm) = highestFC tm
1293highestFC (PQuoteName _ _ fc) = Just fc
1294highestFC (PRunElab fc _ _) = Just fc
1295highestFC (PConstSugar fc _) = Just fc
1296highestFC (PAppImpl t _) = highestFC t
1300data InterfaceInfo = CI {
1301 implementationCtorName :: Name
1302 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1303 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1304 , interface_default_super_interfaces :: [PDecl]
1305 , interface_impparams :: [Name]
1306 , interface_params :: [Name]
1307 , interface_constraints :: [PTerm]
1308 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1309 , interface_determiners :: [Int]
1310 } deriving (Show, Generic)
1312deriving instance Binary InterfaceInfo
1316data RecordInfo = RI {
1317 record_parameters :: [(Name,PTerm)]
1318 , record_constructor :: Name
1319 , record_projections :: [Name]
1320 } deriving (Show, Generic)
1322-- Type inference data
1324data TIData = TIPartial -- ^ a function with a partially defined type
1325 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1326 deriving (Show, Generic)
1328-- | Miscellaneous information about functions
1329data FnInfo = FnInfo { fn_params :: [Int] }
1330 deriving (Show, Generic)
1332deriving instance Binary FnInfo
1335data OptInfo = Optimise {
1336 inaccessible :: [(Int,Name)] -- includes names for error reporting
1337 , detaggable :: Bool
1338 , forceable :: [Int] -- argument positions which are forced by other values
1339 } deriving (Show, Generic)
1341deriving instance Binary OptInfo
1344-- | Syntactic sugar info
1349 , dsl_var :: Maybe t
1350 , index_first :: Maybe t
1351 , index_next :: Maybe t
1352 , dsl_lambda :: Maybe t
1353 , dsl_let :: Maybe t
1355 } deriving (Show, Functor, Generic)
1357deriving instance Binary DSL'
1360type DSL = DSL' PTerm
1362data SynContext = PatternSyntax
1365 deriving (Show, Generic)
1367deriving instance Binary SynContext
1370data Syntax = Rule [SSymbol] PTerm SynContext
1371 | DeclRule [SSymbol] [PDecl]
1372 deriving (Show, Generic)
1374syntaxNames :: Syntax -> [Name]
1375syntaxNames (Rule syms _ _) = mapMaybe ename syms
1376 where ename (Keyword n) = Just n
1378syntaxNames (DeclRule syms _) = mapMaybe ename syms
1379 where ename (Keyword n) = Just n
1382syntaxSymbols :: Syntax -> [SSymbol]
1383syntaxSymbols (Rule ss _ _) = ss
1384syntaxSymbols (DeclRule ss _) = ss
1386deriving instance Binary Syntax
1389data SSymbol = Keyword Name
1394 deriving (Show, Eq, Generic)
1398deriving instance Binary SSymbol
1401newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1404emptySyntaxRules :: SyntaxRules
1405emptySyntaxRules = SyntaxRules []
1407updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1408updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1410 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1415 ruleSort (s1:ss1) (s2:ss2) =
1416 case symCompare s1 s2 of
1417 EQ -> ruleSort ss1 ss2
1420 -- Better than creating Ord implementation for SSymbol since
1421 -- in general this ordering does not really make sense.
1422 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1423 symCompare (Keyword _) _ = LT
1424 symCompare (Symbol _) (Keyword _) = GT
1425 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1426 symCompare (Symbol _) _ = LT
1427 symCompare (Binding _) (Keyword _) = GT
1428 symCompare (Binding _) (Symbol _) = GT
1429 symCompare (Binding b1) (Binding b2) = compare b1 b2
1430 symCompare (Binding _) _ = LT
1431 symCompare (Expr _) (Keyword _) = GT
1432 symCompare (Expr _) (Symbol _) = GT
1433 symCompare (Expr _) (Binding _) = GT
1434 symCompare (Expr e1) (Expr e2) = compare e1 e2
1435 symCompare (Expr _) _ = LT
1436 symCompare (SimpleExpr _) (Keyword _) = GT
1437 symCompare (SimpleExpr _) (Symbol _) = GT
1438 symCompare (SimpleExpr _) (Binding _) = GT
1439 symCompare (SimpleExpr _) (Expr _) = GT
1440 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1442initDSL = DSL (PRef f [] (sUN ">>="))
1443 (PRef f [] (sUN "<*>"))
1444 (PRef f [] (sUN "pure"))
1451 where f = fileFC "(builtin)"
1453data Using = UImplicit Name PTerm
1454 | UConstraint Name [Name]
1455 deriving (Show, Eq, Data, Generic, Typeable)
1457deriving instance Binary Using
1460data SyntaxInfo = Syn {
1462 , syn_params :: [(Name, PTerm)]
1463 , syn_namespace :: [String]
1465 , imp_methods :: [Name]
1466 -- ^ interface methods. When expanding implicits, these should be
1467 -- expanded even under binders
1468 , decoration :: Name -> Name
1470 , implicitAllowed :: Bool
1471 , constraintAllowed :: Bool
1472 , maxline :: Maybe Int
1473 , mut_nesting :: Int
1475 , syn_in_quasiquote :: Int
1476 , syn_toplevel :: Bool
1477 , withAppAllowed :: Bool
1478 } deriving (Show, Generic)
1480deriving instance Binary SyntaxInfo
1483defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1485expandNS :: SyntaxInfo -> Name -> Name
1486expandNS syn n@(NS _ _) = n
1487expandNS syn n = case syn_namespace syn of
1492-- For inferring types of things
1494bi = fileFC "builtin"
1495primfc = fileFC "(primitive)"
1497inferTy = sMN 0 "__Infer"
1498inferCon = sMN 0 "__infer"
1499inferDecl = PDatadecl inferTy primfc
1501 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1502 PPi expl_linear (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1503 (PRef bi [] inferTy)), bi, [])]
1506infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1507infP = P (TCon 6 0) inferTy (TType (UVal 0))
1509getInferTerm, getInferType :: Term -> Term
1510getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1511getInferTerm (App _ (App _ _ _) tm) = tm
1512getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1514getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1515 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1516 toTy (PVar _ t) = PVTy t
1518getInferType (App _ (App _ _ ty) _) = ty
1522-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1524primNames = [inferTy, inferCon]
1527unitCon = sUN "MkUnit"
1529falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1530 "The empty type, also known as the trivially false proposition." ++
1532 "Use `void` or `absurd` to prove anything if you have a variable " ++
1533 "of type `Void` in scope."
1536pairTy = sNS (sUN "Pair") ["Builtins"]
1537pairCon = sNS (sUN "MkPair") ["Builtins"]
1539upairTy = sNS (sUN "UPair") ["Builtins"]
1540upairCon = sNS (sUN "MkUPair") ["Builtins"]
1544eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1545 "The propositional equality type. A proof that `x` = `y`." ++
1547 "To use such a proof, pattern-match on it, and the two equal things will " ++
1548 "then need to be the _same_ pattern." ++
1550 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1551 "is possible to state equalities between values of potentially different " ++
1552 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1554 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1556eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1557 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1559 [(reflDoc, reflParamDoc,
1560 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1561 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1562 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1563 pimp (n "B") Placeholder False,
1564 pexp (PRef bi [] (n "x")),
1565 pexp (PRef bi [] (n "x"))])), bi, [])]
1567 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1568 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1569 "shown that both sides are in fact equal."
1570 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1571 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1573eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1574 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1580-- | The special name to be used in the module documentation context -
1581-- not for use in the main definition context. The namespace around it
1582-- will determine the module to which the docs adhere.
1584modDocName = sMN 0 "ModuleDocs"
1586-- Defined in builtins.idr
1587sigmaTy = sNS (sUN "DPair") ["Builtins"]
1588sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1590piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1591piBind = piBindp expl
1593piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1595piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1598-- Pretty-printing declarations and terms
1600-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1601-- could interfere with interactive editing, which calls "show".
1603instance Show PTerm where
1604 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1606instance Show PDecl where
1607 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1609instance Show PClause where
1610 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1612instance Show PData where
1613 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1615instance Pretty PTerm OutputAnnotation where
1616 pretty = prettyImp defaultPPOption
1618-- | Colourise annotations according to an Idris state. It ignores the
1619-- names in the annotation, as there's no good way to show extended
1620-- information on a terminal.
1621annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1622annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1623annotationColour ist (AnnConst c) =
1624 let theme = idris_colourTheme ist
1625 in Just $ if constIsType c
1626 then typeColour theme
1627 else dataColour theme
1628annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1629annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1630annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1631annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1632annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1633annotationColour ist (AnnName n _ _ _) =
1634 let ctxt = tt_ctxt ist
1635 theme = idris_colourTheme ist
1637 _ | isDConName n ctxt -> Just $ dataColour theme
1638 _ | isFnName n ctxt -> Just $ functionColour theme
1639 _ | isTConName n ctxt -> Just $ typeColour theme
1640 _ | isPostulateName n ist -> Just $ postulateColour theme
1641 _ | otherwise -> Nothing -- don't colourise unknown names
1642annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1643 where colour BoldText = IdrisColour Nothing True False True False
1644 colour UnderlineText = IdrisColour Nothing True True False False
1645 colour ItalicText = IdrisColour Nothing True False False True
1646annotationColour ist _ = Nothing
1649-- | Colourise annotations according to an Idris state. It ignores the
1650-- names in the annotation, as there's no good way to show extended
1651-- information on a terminal. Note that strings produced this way will
1652-- not be coloured on Windows, so the use of the colour rendering
1653-- functions in Idris.Output is to be preferred.
1654consoleDecorate :: IState -> OutputAnnotation -> String -> String
1655consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1657isPostulateName :: Name -> IState -> Bool
1658isPostulateName n ist = S.member n (idris_postulates ist)
1660-- | Pretty-print a high-level closed Idris term with no information
1661-- about precedence/associativity
1662prettyImp :: PPOption -- ^ pretty printing options
1663 -> PTerm -- ^ the term to pretty-print
1664 -> Doc OutputAnnotation
1665prettyImp impl = pprintPTerm impl [] [] []
1667-- | Serialise something to base64 using its Binary implementation.
1669-- | Do the right thing for rendering a term in an IState
1670prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1671prettyIst ist = pprintPTerm opt [] [] (idris_infixes ist)
1673 opt = if LinearTypes `elem` idris_language_extensions ist
1674 then (ppOptionIst ist) { ppopt_displayrig = True }
1675 else ppOptionIst ist
1677-- | Pretty-print a high-level Idris term in some bindings context
1679pprintPTerm :: PPOption -- ^ pretty printing options
1680 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1681 -> [Name] -- ^ names to always show in pi, even if not used
1682 -> [FixDecl] -- ^ Fixity declarations
1683 -> PTerm -- ^ the term to pretty-print
1684 -> Doc OutputAnnotation
1685pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1689 lbrace = annotate (AnnSyntax "{") (text "{")
1690 rbrace = annotate (AnnSyntax "}") (text "}")
1691 percent = annotate (AnnSyntax "%") (text "%")
1693 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1694 prettySe d p bnd (PQuote r) =
1695 text "![" <> pretty r <> text "]"
1696 prettySe d p bnd (PPatvar fc n) = pretty n
1698 | Just str <- slist d p bnd e = depth d str
1699 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1700 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1701 prettySe d p bnd (PLam fc n nfc ty sc) =
1702 let (ns, sc') = getLamNames [n] sc in
1703 depth d . bracket p startPrec . group . align . hang 2 $
1704 (annotate (AnnSyntax "\\") (text "\\"))
1705 <> prettyBindingsOf ns False <+> text "=>" <$>
1706 prettySe (decD d) startPrec ((n, False):bnd) sc'
1708 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1709 getLamNames acc sc = (reverse acc, sc)
1711 prettyBindingsOf [] t = text ""
1712 prettyBindingsOf [n] t = prettyBindingOf n t
1713 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1714 prettyBindingsOf ns t
1715 prettySe d p bnd (PLet fc rc n nfc ty v sc) =
1716 depth d . bracket p startPrec . group . align $
1717 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1718 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1719 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1720 | Rig0 <- rig, ppopt_displayrig ppo =
1721 depth d . bracket p startPrec . group $
1722 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1723 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1724 | Rig1 <- rig, ppopt_displayrig ppo =
1725 depth d . bracket p startPrec . group $
1726 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1727 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1728 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1729 || ppopt_pinames ppo && uname n =
1730 depth d . bracket p startPrec . group $
1731 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1732 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1734 depth d . bracket p startPrec . group $
1735 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1736 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1738 uname (UN n) = case str n of
1745 Static -> percent <> text "static" <> space
1747 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1749 depth d . bracket p startPrec $
1750 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1751 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1752 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1753 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1755 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1756 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1757 showRig _ n = prettyBindingOf n True
1759 isPi (PPi (Exp{}) _ _ _ _) = True
1760 isPi (PPi _ _ _ _ sc) = isPi sc
1765 Static -> percent <> text "static" <> space
1767 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1768 depth d . bracket p startPrec $
1769 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1770 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1771 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1772 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1773 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1774 depth d . bracket p startPrec $
1775 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1776 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1777 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1778 | basename neg == sUN "negate" =
1779 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1780 -- This case preserves the behavior of the former constructor PEq.
1781 -- It should be removed if feasible when the pretty-printing of infix
1782 -- operators in general is improved.
1783 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1784 | n == eqTy, ppopt_impl ppo =
1785 depth d . bracket p eqPrec $
1786 enclose lparen rparen eq <+>
1787 align (group (vsep (map (prettyArgS (decD d) bnd)
1790 depth d . bracket p eqPrec . align . group $
1791 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1792 where eq = annName eqTy (text "=")
1794 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1795 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1796 | UN nm <- basename f
1797 , not (ppopt_impl ppo) && null (getShowArgs args) =
1798 prettyName True (ppopt_impl ppo) bnd f
1799 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1800 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1801 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1802 | UN nm <- basename op
1804 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1805 case getShowArgs args of
1807 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1808 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1809 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1810 (l@(PExp{}) : r@(PExp{}) : rest) ->
1811 depth d . bracket p funcAppPrec $
1812 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1813 align (group (vsep (map (prettyArgS d bnd) rest)))
1814 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1815 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1816 f = getFixity (opStr op)
1818 Nothing -> funcAppPrec + 1
1819 Just (Infixl p') -> p'
1820 Just f' -> prec f' + 1
1822 Nothing -> funcAppPrec + 1
1823 Just (Infixr p') -> p'
1824 Just f' -> prec f' + 1
1825 inFix l r = align . group $
1826 (prettySe (decD d) left bnd l <+> opName False) <$>
1827 group (prettySe (decD d) right bnd r)
1828 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1829 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1830 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1831 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1832 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1833 let args = getShowArgs as
1834 fp = prettySe (decD d) (startPrec + 1) bnd f
1835 shownArgs = if ppopt_impl ppo then as else args
1837 depth d . bracket p funcAppPrec . group $
1840 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1841 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1842 prettySe d p bnd (PCase _ scr cases) =
1843 bracket p funcAppPrec $
1844 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1845 depth d (indent 2 (vsep (map ppcase cases)))
1847 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1848 ([(n, False) | n <- vars l] ++ bnd)
1849 in nest nestingSize $
1850 prettyCase l <+> text "=>" <+> prettyCase r
1851 -- Warning: this is a bit of a hack. At this stage, we don't have the
1852 -- global context, so we can't determine which names are constructors,
1853 -- which are types, and which are pattern variables on the LHS of the
1854 -- case pattern. We use the heuristic that names without a namespace
1855 -- are patvars, because right now case blocks in PTerms are always
1856 -- delaborated from TT before being sent to the pretty-printer. If they
1857 -- start getting printed directly, THIS WILL BREAK.
1858 -- Potential solution: add a list of known patvars to the cases in
1859 -- PCase, and have the delaborator fill it out, kind of like the pun
1860 -- disambiguation on PDPair.
1861 vars tm = filter noNS (allNamesIn tm)
1862 noNS (NS _ _) = False
1865 prettySe d p bnd (PIfThenElse _ c t f) =
1866 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1867 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1868 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1869 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1871 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1872 prettySe d p bnd (PResolveTC _) = percent <> kwd "implementation"
1873 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1874 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1875 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1876 prettySe d p bnd (PRewrite _ by l r _) =
1877 depth d . bracket p startPrec $
1878 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1881 Just fn -> text "using" <+>
1882 prettyName True (ppopt_impl ppo) bnd fn) <+>
1883 text "in" <+> prettySe (decD d) startPrec bnd r
1884 prettySe d p bnd (PTyped l r) =
1885 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1886 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1887 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1888 align . group . vsep . punctuate (ann comma) $
1889 map (prettySe (decD d) startPrec bnd) elts
1890 where ann = case pun of
1892 IsType -> annName pairTy
1893 IsTerm -> annName pairCon
1894 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1895 | Just elts <- dPairElts dpair
1896 = depth d . enclose (annotated lparen) (annotated rparen) .
1897 align . group . vsep . punctuate (space <> annotated (text "**")) $
1903 annotated (text "**") <+>
1904 prettySe (decD d) startPrec (addBinding bnd) r <>
1906 where annotated = case pun of
1907 IsType -> annName sigmaTy
1908 IsTerm -> annName sigmaCon
1911 (left, addBinding) = case (l, pun) of
1912 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1913 _ -> (prettySe (decD d) startPrec bnd l, id)
1916 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1917 ppElts ((PRef _ _ n, t):rs) bs
1919 = (bindingOf n False <+> colon <+>
1920 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1921 ppElts ((l, t):rs) bs
1922 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1923 prettySe d p bnd (PAlternative ns a as) =
1924 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1927 foldr ((\ l r -> l <+> text "," <+> r) .
1928 depth d . prettySe (decD d) startPrec bnd)
1930 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1931 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1932 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1933 -- XXX: add pretty for tactics
1934 prettySe d p bnd (PProof ts) =
1935 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1936 prettySe d p bnd (PTactics ts) =
1937 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1938 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1939 prettySe d p bnd PImpossible = kwd "impossible"
1940 prettySe d p bnd Placeholder = text "_"
1941 prettySe d p bnd (PDoBlock dos) =
1942 bracket p startPrec $
1943 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1944 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1945 ppdo bnd (DoBind _ bn _ tm : dos) =
1946 (prettyBindingOf bn False <+> text "<-" <+>
1947 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1948 ppdo ((bn, False):bnd) dos
1949 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1950 text "no pretty printer for pattern-matching do binding" :
1952 ppdo bnd (DoLet _ _ ln _ ty v : dos) =
1953 (kwd "let" <+> prettyBindingOf ln False <+>
1954 (if ty /= Placeholder
1955 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1957 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1958 ppdo ((ln, False):bnd) dos
1959 ppdo bnd (DoLetP _ _ _ _ : dos) = -- ok because never made by delab
1960 text "no pretty printer for pattern-matching do binding" :
1962 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1963 text "no pretty printer for pattern-matching do binding" :
1966 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1967 prettySe d p bnd (PElabError s) = pretty s
1968 -- Quasiquote pprinting ignores bound vars
1969 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1970 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1971 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1972 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1973 where start = if res then "`{" else "`{{"
1974 end = if res then "}" else "}}"
1975 prettySe d p bnd (PRunElab _ tm _) =
1976 bracket p funcAppPrec . group . align . hang 2 $
1977 (percent <> text "runElab") <$>
1978 prettySe (decD d) funcAppPrec bnd tm
1979 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1980 prettySe d p bnd _ = text "missing pretty-printer for term"
1982 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1983 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1984 where display (UN n) = T.unpack n
1985 display (MN _ n) = T.unpack n
1986 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1987 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1990 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1991 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1992 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1993 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1995 prettyArgSe d bnd arg = prettySe (decD d) (funcAppPrec + 1) bnd arg
1996 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1997 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1998 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2000 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2001 annName n = annotate (AnnName n Nothing Nothing Nothing)
2003 opStr :: Name -> String
2004 opStr (NS n _) = opStr n
2005 opStr (UN n) = T.unpack n
2007 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2008 slist' (Just d) _ _ _ | d <= 0 = Nothing
2010 | containsHole e = Nothing
2011 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2012 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2013 slist' d p bnd (PRef _ _ nil)
2014 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2015 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2016 | nsroot cons == sUN "::",
2017 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2019 Just tl' <- slist' (decD d) p bnd tl
2020 = Just (prettySe d startPrec bnd hd : tl')
2022 isImp (PImp {}) = True
2024 slist' _ _ _ tm = Nothing
2026 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2028 [] -> annotate (AnnData "" "") $ text "[]"
2029 [x] -> enclose left right . group $ x
2030 xs -> enclose left right .
2031 align . group . vsep .
2032 punctuate comma $ xs
2033 where left = (annotate (AnnData "" "") (text "["))
2034 right = (annotate (AnnData "" "") (text "]"))
2035 comma = (annotate (AnnData "" "") (text ","))
2036 slist _ _ _ _ = Nothing
2038 pairElts :: PTerm -> Maybe [PTerm]
2039 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2040 | otherwise = Just [x, y]
2041 pairElts _ = Nothing
2043 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2044 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2045 | otherwise = Just [(l, t), (Placeholder, r)]
2046 dPairElts _ = Nothing
2048 natns = "Prelude.Nat."
2050 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2052 | ppopt_desugarnats ppo = Nothing
2053 | otherwise = snat' d p e
2055 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2056 snat' (Just x) _ _ | x <= 0 = Nothing
2057 snat' d p (PRef _ _ z)
2058 | show z == (natns++"Z") || show z == "Z" = Just 0
2059 snat' d p (PApp _ s [PExp {getTm=n}])
2060 | show s == (natns++"S") || show s == "S",
2061 Just n' <- snat' (decD d) p n
2063 snat' _ _ _ = Nothing
2065 bracket outer inner doc
2066 | outer > inner = lparen <> doc <> rparen
2069 ellipsis = text "..."
2072 depth (Just d) = if d <= 0 then const ellipsis else id
2074 decD = fmap (\x -> x - 1)
2076 kwd = annotate AnnKeyword . text
2078 fixities :: M.Map String Fixity
2079 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2081 getFixity :: String -> Maybe Fixity
2082 getFixity = flip M.lookup fixities
2084-- | Strip away namespace information
2085basename :: Name -> Name
2086basename (NS n _) = basename n
2089-- | Determine whether a name was the one inserted for a hole or guess
2090-- by the delaborator
2091isHoleName :: Name -> Bool
2092isHoleName (UN n) = n == T.pack "[__]"
2095-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2096containsHole :: PTerm -> Bool
2097containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2099-- | Pretty-printer helper for names that attaches the correct annotations
2100prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2101 -> Bool -- ^ whether to show namespaces
2102 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2103 -> Name -- ^ the name to pprint
2104 -> Doc OutputAnnotation
2105prettyName infixParen showNS bnd n
2106 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2107 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2108 | (UN n') <- n, T.unpack n' == "_" = text "_"
2109 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2110 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2111 where fullName = text nameSpace <> parenthesise (text (baseName n))
2112 baseName (UN n) = T.unpack n
2113 baseName (NS n ns) = baseName n
2114 baseName (MN i s) = T.unpack s
2115 baseName other = show other
2116 nameSpace = case n of
2117 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2119 isInfix = case baseName n of
2121 (c : _) -> not (isAlpha c)
2122 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2125showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2126showCImp ppo (PClause _ n l ws r w)
2127 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2128 <+> text "where" <+> text (show w)
2131 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2132showCImp ppo (PWith _ n l ws r pn w)
2133 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2134 <+> braces (text (show w))
2137 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2140showDImp :: PPOption -> PData -> Doc OutputAnnotation
2141showDImp ppo (PDatadecl n nfc ty cons)
2142 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2143 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2145showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2146showDecls o ds = vsep (map (showDeclImp o) ds)
2148showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2149showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2150showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2151 indent 2 (vsep (map (showCImp o) cs))
2152showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2153showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2154showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2155showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2156showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2157showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2158 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2159showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2160 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2161showDeclImp _ _ = text "..."
2162-- showDeclImp (PImport o) = "import " ++ o
2164getImps :: [PArg] -> [(Name, PTerm)]
2166getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2167getImps (_ : xs) = getImps xs
2169getExps :: [PArg] -> [PTerm]
2171getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2172getExps (_ : xs) = getExps xs
2174getShowArgs :: [PArg] -> [PArg]
2176getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2177getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2178 | PImp _ _ _ _ tm <- e
2179 , containsHole tm = e : getShowArgs xs
2180getShowArgs (_ : xs) = getShowArgs xs
2182getConsts :: [PArg] -> [PTerm]
2184getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2185getConsts (_ : xs) = getConsts xs
2187getAll :: [PArg] -> [PTerm]
2192showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2193 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2194 -> PPOption -- ^ pretty printing options
2195 -> Bool -- ^ whether to colourise
2196 -> Name -- ^ the term to show
2198showName ist bnd ppo colour n = case ist of
2199 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2200 Nothing -> showbasic n
2201 where name = if ppopt_impl ppo then show n else showbasic n
2202 showbasic n@(UN _) = showCG n
2203 showbasic (MN i s) = str s
2204 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2205 showbasic (SN s) = show s
2206 colourise n t = let ctxt' = fmap tt_ctxt ist in
2209 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2210 else colouriseBound t name
2211 | isDConName n ctxt -> colouriseData t name
2212 | isFnName n ctxt -> colouriseFun t name
2213 | isTConName n ctxt -> colouriseType t name
2214 -- The assumption is that if a name is not bound and does not exist in the
2215 -- global context, then we're somewhere in which implicit info has been lost
2216 -- (like error messages). Thus, unknown vars are colourised as implicits.
2217 | otherwise -> colouriseImplicit t name
2219showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2220 -> PTerm -- ^ the term to show
2222showTm ist = displayDecorated (consoleDecorate ist) .
2223 renderPretty 0.8 100000 .
2224 prettyImp (ppOptionIst ist)
2226-- | Show a term with implicits, no colours
2227showTmImpls :: PTerm -> String
2228showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2230-- | Show a term with specific options
2231showTmOpts :: PPOption -> PTerm -> String
2232showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2235instance Sized PTerm where
2236 size (PQuote rawTerm) = size rawTerm
2237 size (PRef fc _ name) = size name
2238 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2239 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2240 size (PLet fc _ name nfc ty def bdy) = 1 + size ty + size def + size bdy
2241 size (PTyped trm ty) = 1 + size trm + size ty
2242 size (PApp fc name args) = 1 + size args
2243 size (PAppBind fc name args) = 1 + size args
2244 size (PCase fc trm bdy) = 1 + size trm + size bdy
2245 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2246 size (PTrue fc _) = 1
2247 size (PResolveTC fc) = 1
2248 size (PRewrite fc by left right _) = 1 + size left + size right
2249 size (PPair fc _ _ left right) = 1 + size left + size right
2250 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2251 size (PAlternative _ a alts) = 1 + size alts
2252 size (PHidden hidden) = size hidden
2253 size (PUnifyLog tm) = size tm
2254 size (PDisamb _ tm) = size tm
2255 size (PNoImplicits tm) = size tm
2257 size (PUniverse _ _) = 1
2258 size (PConstant fc const) = 1 + size fc + size const
2259 size Placeholder = 1
2260 size (PDoBlock dos) = 1 + size dos
2261 size (PIdiom fc term) = 1 + size term
2262 size (PMetavar _ name) = 1
2263 size (PProof tactics) = size tactics
2264 size (PElabError err) = size err
2265 size PImpossible = 1
2268getPArity :: PTerm -> Int
2269getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2272-- Return all names, free or globally bound, in the given term.
2274allNamesIn :: PTerm -> [Name]
2275allNamesIn tm = nub $ ni 0 [] tm
2276 where -- TODO THINK added niTacImp, but is it right?
2277 ni 0 env (PRef _ _ n)
2278 | not (n `elem` env) = [n]
2279 ni 0 env (PPatvar _ n) = [n]
2280 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2281 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2282 ni 0 env (PWithApp _ f a) = ni 0 env f ++ ni 0 env a
2283 ni 0 env (PAppImpl t _) = ni 0 env t
2284 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2285 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2286 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2287 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2288 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2289 ni 0 env (PHidden tm) = ni 0 env tm
2290 ni 0 env (PGoal _ t _ sc) = ni 0 env t ++ ni 0 env sc
2291 ni 0 env (PIdiom _ tm) = ni 0 env tm
2292 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2293 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2294 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2295 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2296 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2297 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2298 ni 0 env (PAs _ _ tm) = ni 0 env tm
2299 -- Just take the first, when disambiguating, since the shape will be
2300 -- the same and we'll get the name root
2301 ni 0 env (PAlternative ns (ExactlyOne _) (a : as))
2302 = map snd ns ++ ni 0 env a
2303 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2304 ni 0 env (PUnifyLog tm) = ni 0 env tm
2305 ni 0 env (PDisamb _ tm) = ni 0 env tm
2306 ni 0 env (PNoImplicits tm) = ni 0 env tm
2307 ni 0 env (PCoerced tm) = ni 0 env tm
2308 ni 0 env (PRunElab _ tm _) = ni 0 env tm
2309 ni 0 env (PConstSugar _ tm) = ni 0 env tm
2310 ni 0 env tm@(PDoBlock _) = concatMap (ni 0 env) (children tm)
2311 ni 0 env tm@(PProof _) = concatMap (ni 0 env) (children tm)
2312 ni 0 env tm@(PTactics _) = concatMap (ni 0 env) (children tm)
2314 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2315 ni i env (PUnquote tm) = ni (i - 1) env tm
2317 ni i env tm = concatMap (ni i env) (children tm)
2319 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2323-- Return all names defined in binders in the given term
2324boundNamesIn :: PTerm -> [Name]
2325boundNamesIn tm = S.toList (ni 0 S.empty tm)
2326 where -- TODO THINK Added niTacImp, but is it right?
2327 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2328 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2329 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2330 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2331 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2332 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2333 ni 0 set (PLet fc rc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2334 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2335 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2336 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2337 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2338 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2339 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2340 ni 0 set (PAlternative ns a as) = niTms 0 set as
2341 ni 0 set (PHidden tm) = ni 0 set tm
2342 ni 0 set (PUnifyLog tm) = ni 0 set tm
2343 ni 0 set (PDisamb _ tm) = ni 0 set tm
2344 ni 0 set (PNoImplicits tm) = ni 0 set tm
2346 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2347 ni i set (PUnquote tm) = ni (i - 1) set tm
2349 ni i set tm = foldr (S.union . ni i set) set (children tm)
2351 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2352 niTms i set [] = set
2353 niTms i set (x : xs) = niTms i (ni i set x) xs
2355 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2356 niTacImp i set _ = set
2358-- Return names which are valid implicits in the given term (type).
2359implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2360implicitNamesIn uvars ist tm
2361 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2364 addImp n = do (imps, fns) <- get
2366 addFn n = do (imps, fns) <- get
2369 ni 0 env (PRef _ _ n@(NS _ _))
2370 | not (n `elem` env)
2371 -- Never implicitly bind if there's a namespace
2373 ni 0 env (PRef _ _ n)
2374 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2375 ni 0 env (PApp _ f@(PRef _ _ n) as)
2376 | n `elem` uvars = do ni 0 env f
2377 mapM_ (ni 0 env . getTm) as
2378 | otherwise = do case lookupTy n (tt_ctxt ist) of
2381 mapM_ (ni 0 env . getTm) as
2382 ni 0 env (PApp _ f as) = do ni 0 env f
2383 mapM_ (ni 0 env . getTm) as
2384 ni 0 env (PAppBind _ f as) = do ni 0 env f
2385 mapM_ (ni 0 env . getTm) as
2386 ni 0 env (PCase _ c os) = do ni 0 env c
2387 -- names in 'os', not counting the names bound in the cases
2388 mapM_ (ni 0 env . snd) os
2391 mapM_ (ni 0 env . fst) os
2393 put (nub imps \\ nub impsfst, fns)
2394 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2395 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2396 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2397 ni 0 env (PLet fc rc n _ ty val sc) = do ni 0 env ty;
2398 ni 0 env val; ni 0 (n:env) sc
2399 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2400 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2401 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2402 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2403 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2406 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2407 ni 0 env (PHidden tm) = ni 0 env tm
2408 ni 0 env (PUnifyLog tm) = ni 0 env tm
2409 ni 0 env (PDisamb _ tm) = ni 0 env tm
2410 ni 0 env (PNoImplicits tm) = ni 0 env tm
2412 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2413 maybe (return ()) (ni i env) ty
2414 ni i env (PUnquote tm) = ni (i - 1) env tm
2416 ni i env tm = mapM_ (ni i env) (children tm)
2418-- Return names which are free in the given term.
2419namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2420namesIn uvars ist tm = nub $ ni 0 [] tm
2422 ni 0 env (PRef _ _ n)
2423 | not (n `elem` env)
2424 = case lookupTy n (tt_ctxt ist) of
2426 _ -> [n | n `elem` (map fst uvars)]
2427 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2428 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2429 ni 0 env (PCase _ c os) = ni 0 env c ++
2430 -- names in 'os', not counting the names bound in the cases
2431 (nub (concatMap (ni 0 env . snd) os)
2432 \\ nub (concatMap (ni 0 env . fst) os))
2433 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2434 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2435 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2436 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2437 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2438 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2439 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2440 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2441 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2442 ni 0 env (PHidden tm) = ni 0 env tm
2443 ni 0 env (PUnifyLog tm) = ni 0 env tm
2444 ni 0 env (PDisamb _ tm) = ni 0 env tm
2445 ni 0 env (PNoImplicits tm) = ni 0 env tm
2447 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2448 ni i env (PUnquote tm) = ni (i - 1) env tm
2450 ni i env tm = concatMap (ni i env) (children tm)
2452 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2455-- Return which of the given names are used in the given term.
2457usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2458usedNamesIn vars ist tm = nub $ ni 0 [] tm
2459 where -- TODO THINK added niTacImp, but is it right?
2460 ni 0 env (PRef _ _ n)
2461 | n `elem` vars && not (n `elem` env)
2462 = case lookupDefExact n (tt_ctxt ist) of
2465 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2466 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2467 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2468 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2469 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2470 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2471 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2472 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2473 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2474 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2475 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2476 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2477 ni 0 env (PHidden tm) = ni 0 env tm
2478 ni 0 env (PUnifyLog tm) = ni 0 env tm
2479 ni 0 env (PDisamb _ tm) = ni 0 env tm
2480 ni 0 env (PNoImplicits tm) = ni 0 env tm
2482 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2483 ni i env (PUnquote tm) = ni (i - 1) env tm
2485 ni i env tm = concatMap (ni i env) (children tm)
2487 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2490-- Return the list of inaccessible (= dotted) positions for a name.
2491getErasureInfo :: IState -> Name -> [Int]
2492getErasureInfo ist n =
2493 case lookupCtxtExact n (idris_optimisation ist) of
2494 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