2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
9{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
10 DeriveTraversable, FlexibleContexts, FlexibleInstances,
11 MultiParamTypeClasses, PatternGuards, TypeSynonymInstances #-}
13module Idris.AbsSyntaxTree where
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
18import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
29import Prelude hiding (Foldable, Traversable, (<$>))
31import Control.Applicative ((<|>))
32import qualified Control.Monad.Trans.Class as Trans (lift)
33import Control.Monad.Trans.Except
34import Control.Monad.Trans.State.Strict
36import Data.Data (Data)
38import Data.Foldable (Foldable)
39import Data.Function (on)
40import Data.Generics.Uniplate.Data (children, universe)
41import Data.List hiding (group)
42import qualified Data.Map.Strict as M
43import Data.Maybe (mapMaybe, maybeToList)
44import qualified Data.Set as S
45import qualified Data.Text as T
46import Data.Traversable (Traversable)
48import GHC.Generics (Generic)
51data ElabWhat = ETypes | EDefns | EAll
54-- | Data to pass to recursively called elaborators; e.g. for where blocks,
55-- paramaterised declarations, etc.
57-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
58-- so that we can have mutually recursive elaborators in separate modules without
59-- having to muck about with cyclic modules.
60data ElabInfo = EInfo {
61 params :: [(Name, PTerm)]
62 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
63 , liftname :: Name -> Name
64 , namespace :: [String]
66 , constraintNS :: String -- ^ filename for adding to constraint variables
68 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
69 -- | We may, recursively, collect transformations to do on the rhs,
70 -- e.g. rewriting recursive calls to functions defined by 'with'
71 , rhs_trans :: PTerm -> PTerm
72 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
76toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
78toplevelWith :: String -> ElabInfo
79toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
81eInfoNames :: ElabInfo -> [Name]
82eInfoNames info = map fst (params info) ++ M.keys (inblock info)
84data IOption = IOption {
86 , opt_logcats :: [LogCat] -- ^ List of logging categories.
87 , opt_typecase :: Bool
88 , opt_typeintype :: Bool
89 , opt_coverage :: Bool
90 , opt_showimp :: Bool -- ^ show implicits
91 , opt_errContext :: Bool
94 , opt_nobanner :: Bool
96 , opt_codegen :: Codegen
97 , opt_outputTy :: OutputType
98 , opt_ibcsubdir :: FilePath
99 , opt_importdirs :: [FilePath]
100 , opt_sourcedirs :: [FilePath]
101 , opt_triple :: String
103 , opt_cmdline :: [Opt] -- ^ remember whole command line
104 , opt_origerr :: Bool
105 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
106 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
107 , opt_optimise :: [Optimisation]
108 , opt_printdepth :: Maybe Int
109 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
110 , opt_desugarnats :: Bool
111 , opt_autoimpls :: Bool
112 } deriving (Show, Eq, Generic)
114defaultOpts :: IOption
115defaultOpts = IOption { opt_logLevel = 0
117 , opt_typecase = False
118 , opt_typeintype = False
119 , opt_coverage = True
120 , opt_showimp = False
121 , opt_errContext = False
124 , opt_nobanner = False
126 , opt_codegen = Via IBCFormat "c"
127 , opt_outputTy = Executable
129 , opt_importdirs = []
130 , opt_sourcedirs = []
134 , opt_origerr = False
135 , opt_autoSolve = True
136 , opt_autoImport = []
137 , opt_optimise = defaultOptimise
138 , opt_printdepth = Just 5000
139 , opt_evaltypes = True
140 , opt_desugarnats = False
141 , opt_autoimpls = True
144data PPOption = PPOption {
145 ppopt_impl :: Bool -- ^ whether to show implicits
146 , ppopt_desugarnats :: Bool
147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
148 , ppopt_depth :: Maybe Int
149 , ppopt_displayrig :: Bool -- ^ whether to display multiplicities in binders
154defaultOptimise :: [Optimisation]
157-- | Pretty printing options with default verbosity.
158defaultPPOption :: PPOption
159defaultPPOption = PPOption {
161 , ppopt_desugarnats = False
162 , ppopt_pinames = False
163 , ppopt_depth = Nothing
164 , ppopt_displayrig = False
167-- | Pretty printing options with the most verbosity.
168verbosePPOption :: PPOption
169verbosePPOption = PPOption {
171 , ppopt_desugarnats = True
172 , ppopt_pinames = True
173 , ppopt_depth = Nothing
174 , ppopt_displayrig = False
177-- | Get pretty printing options from the big options record.
178ppOption :: IOption -> PPOption
179ppOption opt = PPOption {
180 ppopt_impl = opt_showimp opt
181 , ppopt_pinames = False
182 , ppopt_depth = opt_printdepth opt
183 , ppopt_desugarnats = opt_desugarnats opt
184 , ppopt_displayrig = False
187-- | Get pretty printing options from an idris state record.
188ppOptionIst :: IState -> PPOption
189ppOptionIst = ppOption . idris_options
192-- | The output mode in use
193data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
194 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
198-- | If a function has no totality annotation, what do we assume?
199data DefaultTotality = DefaultCheckingTotal -- ^ Total
200 | DefaultCheckingPartial -- ^ Partial
201 | DefaultCheckingCovering -- ^Total coverage, but may diverge
202 deriving (Show, Eq, Generic)
204-- | Configuration options for interactive editing.
205data InteractiveOpts = InteractiveOpts {
206 interactiveOpts_indentWith :: Int
207 , interactiveOpts_indentClause :: Int
208} deriving (Show, Generic)
210-- | The global state used in the Idris monad
211data IState = IState {
212 tt_ctxt :: Context -- ^ All the currently defined names and their terms
213 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
214 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
215 , idris_implicits :: Ctxt [PArg]
216 , idris_statics :: Ctxt [Bool]
217 , idris_interfaces :: Ctxt InterfaceInfo
218 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
219 , idris_records :: Ctxt RecordInfo
220 , idris_dsls :: Ctxt DSL
221 , idris_optimisation :: Ctxt OptInfo
222 , idris_datatypes :: Ctxt TypeInfo
223 , idris_namehints :: Ctxt [Name]
225 -- | list of lhs/rhs, and a list of missing clauses. These are not
227 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
228 , idris_flags :: Ctxt [FnOpt]
229 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
230 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
232 -- | module documentation is saved in a special MN so the context
233 -- mechanism can be used for disambiguation.
234 , idris_moduledocs :: Ctxt (Docstring DocTerm)
235 , idris_tyinfodata :: Ctxt TIData
236 , idris_fninfo :: Ctxt FnInfo
237 , idris_transforms :: Ctxt [(Term, Term)]
238 , idris_autohints :: Ctxt [Name]
239 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
240 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
241 , idris_totcheckfail :: [(FC, String)]
242 , idris_options :: IOption
244 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
246 -- | The currently defined but not proven metavariables. The Int is
247 -- the number of vars to display as a context, the Maybe Name is its
248 -- top-level function, the [Name] is the list of local variables
249 -- available for proof search and the Bools are whether :p is
250 -- allowed, and whether the variable is definable at all
251 -- (Metavariables are not definable if they are applied in a term
252 -- which still has hole bindings)
253 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
254 , idris_coercions :: [Name]
255 , idris_errRev :: [(Term, Term)]
256 , idris_errReduce :: [Name]
257 , syntax_rules :: SyntaxRules
258 , syntax_keywords :: [String]
259 , imported :: [FilePath] -- ^ The imported modules
260 , idris_scprims :: [(Name, (Int, PrimFn))]
261 , idris_objs :: [(Codegen, FilePath)]
262 , idris_libs :: [(Codegen, String)]
263 , idris_cgflags :: [(Codegen, String)]
264 , idris_hdrs :: [(Codegen, String)]
265 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
266 , proof_list :: [(Name, (Bool, [String]))]
267 , errSpan :: Maybe FC
268 , parserWarnings :: [(FC, Err)]
269 , lastParse :: Maybe Name
270 , indent_stack :: [Int]
271 , brace_stack :: [Maybe Int]
272 , idris_parsedSpan :: Maybe FC
273 , hide_list :: Ctxt Accessibility
274 , default_access :: Accessibility
275 , default_total :: DefaultTotality
276 , ibc_write :: [IBCWrite]
277 , compiled_so :: Maybe String
278 , idris_dynamic_libs :: [DynamicLib]
279 , idris_language_extensions :: [LanguageExt]
280 , idris_outputmode :: OutputMode
281 , idris_colourRepl :: Bool
282 , idris_colourTheme :: ColourTheme
283 , idris_errorhandlers :: [Name] -- ^ Global error handlers
284 , idris_nameIdx :: (Int, Ctxt (Int, Name))
285 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
286 , module_aliases :: M.Map [T.Text] [T.Text]
287 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
288 , idris_postulates :: S.Set Name
289 , idris_externs :: S.Set (Name, Int)
290 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
292 -- | List of names that were defined in the repl, and can be re-/un-defined
293 , idris_repl_defs :: [Name]
295 -- | Stack of names currently being elaborated, Bool set if it's an
296 -- implementation (implementations appear twice; also as a function name)
297 , elab_stack :: [(Name, Bool)]
300 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
301 , idris_exports :: [Name] -- ^ Functions with ExportList
302 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
303 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
304 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
305 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
306 , idris_ttstats :: M.Map Term (Int, Term)
307 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
308 , idris_interactiveOpts :: InteractiveOpts
311-- Required for parsers library, and therefore trifecta
312instance Show IState where
313 show = const "{internal state}"
315data SizeChange = Smaller | Same | Bigger | Unknown
316 deriving (Show, Eq, Generic)
318deriving instance Binary SizeChange
321type SCGEntry = (Name, [Maybe (Int, SizeChange)])
322type UsageReason = (Name, Int) -- fn_name, its_arg_number
324data CGInfo = CGInfo {
325 calls :: [Name] -- Immediate calls
326 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
328 , usedpos :: [(Int, [UsageReason])]
329 } deriving (Show, Generic)
331deriving instance Binary CGInfo
335primDefs = [ sUN "unsafePerformPrimIO"
336 , sUN "mkLazyForeignPrim"
337 , sUN "mkForeignPrim"
339 , sUN "assert_unreachable"
343-- information that needs writing for the current module's .ibc file
344data IBCWrite = IBCFix FixDecl
349 | IBCImplementation Bool Bool Name Name
356 | IBCImport (Bool, FilePath) -- ^ True = import public
357 | IBCImportDir FilePath
358 | IBCSourceDir FilePath
359 | IBCObj Codegen FilePath
360 | IBCLib Codegen String
361 | IBCCGFlag Codegen String
363 | IBCHeader Codegen String
364 | IBCAccess Name Accessibility
365 | IBCMetaInformation Name MetaInformation
366 | IBCTotal Name Totality
367 | IBCInjective Name Injectivity
369 | IBCFnInfo Name FnInfo
370 | IBCTrans Name (Term, Term)
371 | IBCErrRev (Term, Term)
376 | IBCDef Name -- ^ The main context.
377 | IBCNameHint (Name, Name)
378 | IBCLineApp FilePath Int PTerm
379 | IBCErrorHandler Name
380 | IBCFunctionErrorHandler Name Name Name
382 | IBCExtern (Name, Int)
383 | IBCTotCheckErr FC String
385 | IBCModDocs Name -- ^ The name is the special name used to track module docs
386 | IBCUsage (Name, Int)
388 | IBCAutoHint Name Name
389 | IBCDeprecate Name String
390 | IBCFragile Name String
391 | IBCConstraint FC UConstraint
392 deriving (Show, Generic)
394initialInteractiveOpts :: InteractiveOpts
395initialInteractiveOpts = InteractiveOpts {
396 interactiveOpts_indentWith = 2
397 , interactiveOpts_indentClause = 2
400-- | The initial state for the compiler
402idrisInit = IState initContext S.empty []
403 emptyContext emptyContext emptyContext [] emptyContext
404 emptyContext emptyContext emptyContext emptyContext
405 emptyContext emptyContext emptyContext emptyContext
406 emptyContext emptyContext emptyContext emptyContext
408 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
409 [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
410 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
411 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
412 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
415-- | The monad for the main REPL - reading and processing files and
416-- updating global state (hence the IO inner monad).
419-- type Idris = WriterT [Either String (IO ())] (State IState a))
422type Idris = StateT IState (ExceptT Err IO)
424catchError :: Idris a -> (Err -> Idris a) -> Idris a
425catchError = liftCatch catchE
427throwError :: Err -> Idris a
428throwError = Trans.lift . throwE
430-- Commands in the REPL
435data ElabShellCmd = EQED
443 | EDocStr (Either Name Const)
449-- Parsed declarations
451data Fixity = Infixl { prec :: Int }
452 | Infixr { prec :: Int }
453 | InfixN { prec :: Int }
454 | PrefixN { prec :: Int }
455 deriving (Eq, Generic)
457deriving instance Binary Fixity
460instance Show Fixity where
461 show (Infixl i) = "infixl " ++ show i
462 show (Infixr i) = "infixr " ++ show i
463 show (InfixN i) = "infix " ++ show i
464 show (PrefixN i) = "prefix " ++ show i
466data FixDecl = Fix Fixity String
467 deriving (Eq, Generic)
469instance Show FixDecl where
470 show (Fix f s) = show f ++ " " ++ s
473deriving instance Binary FixDecl
476instance Ord FixDecl where
477 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
480data Static = Static | Dynamic
481 deriving (Show, Eq, Ord, Data, Generic, Typeable)
483deriving instance Binary Static
486-- ^ Mark bindings with their explicitness, and laziness
487data Plicity = Imp { pargopts :: [ArgOpt]
490 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
491 , pinsource :: Bool -- ^ Explicitly written in source
494 | Exp { pargopts :: [ArgOpt]
496 , pparam :: Bool -- ^ this is a param (rather than index)
499 | Constraint { pargopts :: [ArgOpt]
503 | TacImp { pargopts :: [ArgOpt]
508 deriving (Show, Eq, Ord, Data, Generic, Typeable)
511deriving instance Binary Plicity
514is_scoped :: Plicity -> Maybe ImplicitInfo
515is_scoped (Imp _ _ _ s _ _) = s
520impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
521-- Machine generated top level implicit
523impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
527forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
528forall_constraint :: Plicity
529forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
532expl = Exp [] Dynamic False RigW
534expl_param = Exp [] Dynamic True RigW
535expl_linear :: Plicity
536expl_linear = Exp [] Dynamic False Rig1
539constraint = Constraint [] Static RigW
541tacimpl :: PTerm -> Plicity
542tacimpl t = TacImp [] Dynamic t RigW
544data FnOpt = Inlinable -- ^ always evaluate when simplifying
545 | TotalFn | PartialFn | CoveringFn
546 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
549 -- | interface dictionary, eval only when a function
550 -- argument, and further evaluation results.
552 | OverlappingDictionary -- ^ Interface dictionary which may overlap
553 | Implicit -- ^ implicit coercion
554 | NoImplicit -- ^ do not apply implicit coercions
555 | CExport String -- ^ export, with a C name
556 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
557 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
558 | ErrorReduce -- ^ unfold definition before showing an error
559 | Reflection -- ^ a reflecting function, compile-time only
560 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
561 | Constructor -- ^ Data constructor type
562 | AutoHint -- ^ use in auto implicit search
563 | PEGenerated -- ^ generated by partial evaluator
564 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
565 deriving (Show, Eq, Generic)
567deriving instance Binary FnOpt
572inlinable :: FnOpts -> Bool
573inlinable = elem Inlinable
575dictionary :: FnOpts -> Bool
576dictionary = elem Dictionary
579-- | Type provider - what to provide
580data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
581 | ProvPostulate t -- ^ goal type must be Type, so only term
582 deriving (Show, Eq, Functor, Generic)
584type ProvideWhat = ProvideWhat' PTerm
586-- | Top-level declarations such as compiler directives, definitions,
587-- datatypes and interfaces.
589 -- | Fixity declaration
590 = PFix FC Fixity [String]
591 -- | Type declaration (last FC is precise name location)
592 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
593 -- | Postulate, second FC is precise name location
594 | PPostulate Bool -- external def if true
595 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
597 | PClauses FC FnOpts Name [PClause' t]
598 -- | Top level constant
600 -- | Data declaration.
601 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
603 | PParams FC [(Name, t)] [PDecl' t]
604 -- | Open block/declaration
605 | POpenInterfaces FC [Name] [PDecl' t]
606 -- | New namespace, where FC is accurate location of the namespace
608 | PNamespace String FC [PDecl' t]
610 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
612 FC -- Record name precise location
613 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
614 [(Name, Docstring (Either Err t))] -- Param Docs
615 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
616 (Maybe (Name, FC)) -- Optional constructor name and location
617 (Docstring (Either Err t)) -- Constructor doc
618 SyntaxInfo -- Constructor SyntaxInfo
620 -- | Interface: arguments are documentation, syntax info, source
621 -- location, constraints, interface name, interface name location,
622 -- parameters, method declarations, optional constructor name
623 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
624 [(Name, t)] -- constraints
625 Name -- interface name
626 FC -- accurate location of interface name
627 [(Name, FC, t)] -- parameters and precise locations
628 [(Name, Docstring (Either Err t))] -- parameter docstrings
629 [(Name, FC)] -- determining parameters and precise locations
630 [PDecl' t] -- declarations
631 (Maybe (Name, FC)) -- implementation constructor name and location
632 (Docstring (Either Err t)) -- implementation constructor docs
634 -- | Implementation declaration: arguments are documentation, syntax
635 -- info, source location, constraints, interface name, parameters, full
636 -- Implementation type, optional explicit name, and definitions
637 | PImplementation (Docstring (Either Err t)) -- Implementation docs
638 [(Name, Docstring (Either Err t))] -- Parameter docs
640 FC [(Name, t)] -- constraints
641 [Name] -- parent dictionaries to search for constraints
645 FC -- precise location of interface
647 [(Name, t)] -- Extra names in scope in the body
648 t -- full Implementation type
649 (Maybe Name) -- explicit name
651 | PDSL Name (DSL' t) -- ^ DSL declaration
652 | PSyntax FC Syntax -- ^ Syntax definition
653 | PMutual FC [PDecl' t] -- ^ Mutual block
654 | PDirective Directive -- ^ Compiler directive.
656 -- | Type provider. The first t is the type, the second is the
657 -- term. The second FC is precise highlighting location.
658 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
660 -- | Source-to-source transformation rule. If bool is True, lhs and
661 -- rhs must be convertible.
662 | PTransform FC Bool t t
664 -- | FC is decl-level, for errors, and Strings represent the
666 | PRunElabDecl FC t [String]
667 deriving (Functor, Generic)
669deriving instance Binary PDecl'
672-- | The set of source directives
673data Directive = DLib Codegen String
674 | DLink Codegen String
675 | DFlag Codegen String
676 | DInclude Codegen String
681 | DSetTotal Name -- assert totality after checking
682 | DAccess Accessibility
683 | DDefault DefaultTotality
685 | DDynamicLibs [String]
686 | DNameHint Name FC [(Name, FC)]
687 | DErrorHandlers Name FC Name FC [(Name, FC)]
688 | DLanguage LanguageExt
689 | DDeprecate Name String
690 | DFragile Name String
691 | DAutoImplicits Bool
695-- | A set of instructions for things that need to happen in IState
696-- after a term elaboration when there's been reflected elaboration.
697data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
698 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
699 | RAddImplementation Name Name
700 | RDatatypeDeclInstrs Name [PArg]
701 -- | Datatype, constructors
702 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
705-- | For elaborator state
706data EState = EState {
707 case_decls :: [(Name, PDecl)]
708 , delayed_elab :: [(Int, Elab' EState ())]
709 , new_tyDecls :: [RDeclInstructions]
710 , highlighting :: [(FC, OutputAnnotation)]
711 , auto_binds :: [Name] -- ^ names bound as auto implicits
712 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
716initEState = EState [] [] [] [] [] []
718type ElabD a = Elab' EState a
720highlightSource :: FC -> OutputAnnotation -> ElabD ()
721highlightSource fc annot =
722 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
724-- | One clause of a top-level definition. Term arguments to constructors are:
726-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
728-- 2. The list of extra 'with' patterns
730-- 3. The right-hand side
732-- 4. The where block (PDecl' t)
734data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
735 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
736 | PClauseR FC [t] t [PDecl' t]
737 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
738 deriving (Functor, Generic)
740deriving instance Binary PClause'
745 -- | Data declaration
746 PDatadecl { d_name :: Name -- ^ The name of the datatype
747 , d_name_fc :: FC -- ^ The precise location of the type constructor name
748 , d_tcon :: t -- ^ Type constructor
749 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
751 -- | "Placeholder" for data whose constructors are defined later
752 | PLaterdecl { d_name :: Name
755 } deriving (Functor, Generic)
757-- | Transform the FCs in a PData and its associated terms. The first
758-- function transforms the general-purpose FCs, and the second
759-- transforms those that are used for semantic source highlighting, so
760-- they can be treated specially.
761mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
762mapPDataFC f g (PDatadecl n nfc tycon ctors) =
763 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
764 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
765 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
766mapPDataFC f g (PLaterdecl n nfc tycon) =
767 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
769deriving instance Binary PData'
772-- Handy to get a free function for applying PTerm -> PTerm functions
773-- across a program, by deriving Functor
775type PDecl = PDecl' PTerm
776type PData = PData' PTerm
777type PClause = PClause' PTerm
779-- | Transform the FCs in a PTerm. The first function transforms the
780-- general-purpose FCs, and the second transforms those that are used
781-- for semantic source highlighting, so they can be treated specially.
782mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
783mapPDeclFC f g (PFix fc fixity ops) =
784 PFix (f fc) fixity ops
785mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
786 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
787mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
788 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
790mapPDeclFC f g (PClauses fc opts n clauses) =
791 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
792mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
793mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
794 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
795mapPDeclFC f g (PParams fc params decls) =
797 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
798 (map (mapPDeclFC f g) decls)
799mapPDeclFC f g (POpenInterfaces fc ifs decls) =
800 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
801mapPDeclFC f g (PNamespace ns fc decls) =
802 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
803mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
804 PRecord doc syn (f fc) opts n (g nfc)
805 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
807 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
808 plic, mapPTermFC f g ty, fdoc))
810 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
813mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
814 PInterface doc syn (f fc)
815 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
816 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
817 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
818 (map (mapPDeclFC f g) body)
819 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
821mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
822 PImplementation doc paramDocs syn (f fc)
823 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
824 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
825 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
826 (mapPTermFC f g implTy)
828 (map (mapPDeclFC f g) body)
829mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
830mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
832 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
833 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
834mapPDeclFC f g (PMutual fc decls) =
835 PMutual (f fc) (map (mapPDeclFC f g) decls)
836mapPDeclFC f g (PDirective d) =
839 DNameHint n nfc ns ->
840 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
841 DErrorHandlers n nfc n' nfc' ns ->
842 DErrorHandlers n (g nfc) n' (g nfc') $
843 map (\(an, anfc) -> (an, g anfc)) ns
844mapPDeclFC f g (PProvider doc syn fc nfc what n) =
845 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
846mapPDeclFC f g (PTransform fc safe l r) =
847 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
848mapPDeclFC f g (PRunElabDecl fc script ns) =
849 PRunElabDecl (f fc) (mapPTermFC f g script) ns
851-- | Get all the names declared in a declaration
852declared :: PDecl -> [Name]
853declared (PFix _ _ _) = []
854declared (PTy _ _ _ _ _ n fc t) = [n]
855declared (PPostulate _ _ _ _ _ _ n t) = [n]
856declared (PClauses _ _ n _) = [] -- not a declaration
857declared (PCAF _ n _) = [n]
858declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
859 where fstt (_, _, a, _, _, _, _) = a
860declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
861declared (PParams _ _ ds) = concatMap declared ds
862declared (POpenInterfaces _ _ ds) = concatMap declared ds
863declared (PNamespace _ _ ds) = concatMap declared ds
864declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
865declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
866declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
870declared (PDSL n _) = [n]
871declared (PSyntax _ _) = []
872declared (PMutual _ ds) = concatMap declared ds
873declared (PDirective _) = []
876-- get the names declared, not counting nested parameter blocks
877tldeclared :: PDecl -> [Name]
878tldeclared (PFix _ _ _) = []
879tldeclared (PTy _ _ _ _ _ n _ t) = [n]
880tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
881tldeclared (PClauses _ _ n _) = [] -- not a declaration
882tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
883tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
884 where fstt (_, _, a, _, _, _, _) = a
885tldeclared (PParams _ _ ds) = []
886tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
887tldeclared (PMutual _ ds) = concatMap tldeclared ds
888tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
889tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
890tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
896defined :: PDecl -> [Name]
897defined (PFix _ _ _) = []
898defined (PTy _ _ _ _ _ n _ t) = []
899defined (PPostulate _ _ _ _ _ _ n t) = []
900defined (PClauses _ _ n _) = [n] -- not a declaration
901defined (PCAF _ n _) = [n]
902defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
903 where fstt (_, _, a, _, _, _, _) = a
904defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
905defined (PParams _ _ ds) = concatMap defined ds
906defined (POpenInterfaces _ _ ds) = concatMap defined ds
907defined (PNamespace _ _ ds) = concatMap defined ds
908defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
909defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
910defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
914defined (PDSL n _) = [n]
915defined (PSyntax _ _) = []
916defined (PMutual _ ds) = concatMap defined ds
917defined (PDirective _) = []
920updateN :: [(Name, Name)] -> Name -> Name
921updateN ns n | Just n' <- lookup n ns = n'
924updateNs :: [(Name, Name)] -> PTerm -> PTerm
926updateNs ns t = mapPT updateRef t
927 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
933 deriving (Eq, Show, Ord, Data, Typeable, Generic)
935-- | High level language terms
936data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
937 -- high-level language
939 -- ^ A reference to a variable. The FC is its precise
940 -- source location for highlighting. The list of FCs is a
941 -- collection of additional highlighting locations.
942 | PInferRef FC [FC] Name -- ^ A name to be defined later
943 | PPatvar FC Name -- ^ A pattern variable
944 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
945 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
946 | PLet FC RigCount Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
947 | PTyped PTerm PTerm -- ^ Term with explicit type
948 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
949 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
950 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
951 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
952 | PMatchApp FC Name -- ^ Make an application by type matching
953 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
954 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
955 | PTrue FC PunInfo -- ^ Unit type..?
956 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
957 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
958 -- ^ "rewrite" syntax, with optional rewriting function and
959 -- optional result type
960 | PPair FC [FC] PunInfo PTerm PTerm
961 -- ^ A pair (a, b) and whether it's a product type or a
962 -- pair (solved by elaboration). The list of FCs is its
964 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
965 -- ^ A dependent pair (tm : a ** b) and whether it's a
966 -- sigma type or a pair that inhabits one (solved by
967 -- elaboration). The [FC] is its punctuation.
968 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
969 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
970 | PHidden PTerm -- ^ Irrelevant or hidden pattern
971 | PType FC -- ^ 'Type' type
972 | PUniverse FC Universe -- ^ Some universe
973 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
974 | PConstant FC Const -- ^ Builtin types
975 | Placeholder -- ^ Underscore
976 | PDoBlock [PDo] -- ^ Do notation
977 | PIdiom FC PTerm -- ^ Idiom brackets
978 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
979 | PProof [PTactic] -- ^ Proof script
980 | PTactics [PTactic] -- ^ As PProof, but no auto solving
981 | PElabError Err -- ^ Error to report on elaboration
982 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
983 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
984 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
985 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
986 | PNoImplicits PTerm -- ^ never run implicit converions on the term
987 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
988 | PUnquote PTerm -- ^ ~Term
989 | PQuoteName Name Bool FC
990 -- ^ `{n} where the FC is the precise highlighting for
991 -- the name in particular. If the Bool is False, then
992 -- it's `{{n}} and the name won't be resolved.
993 | PRunElab FC PTerm [String]
994 -- ^ %runElab tm - New-style proof script. Args are
995 -- location, script, enclosing namespace.
996 | PConstSugar FC PTerm
997 -- ^ A desugared constant. The FC is a precise source
998 -- location that will be used to highlight it later.
999 deriving (Eq, Ord, Data, Typeable, Generic)
1001data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1004 deriving (Eq, Ord, Data, Generic, Typeable)
1006-- | Transform the FCs in a PTerm. The first function transforms the
1007-- general-purpose FCs, and the second transforms those that are used
1008-- for semantic source highlighting, so they can be treated specially.
1009mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1010mapPTermFC f g (PQuote q) = PQuote q
1011mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1012mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1013mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1014mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1015mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1016mapPTermFC 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)
1017mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1018mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1019mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1020mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1021mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1022mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1023mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1024mapPTermFC 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)
1025mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1026mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1027mapPTermFC 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)
1028mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1029mapPTermFC 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)
1030mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1031mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1032mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1033mapPTermFC f g (PType fc) = PType (f fc)
1034mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1035mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1036mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1037mapPTermFC f g Placeholder = Placeholder
1038mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1039 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1040 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1041 mapPDoFC (DoBindP fc t1 t2 alts) =
1042 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1043 mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1044 mapPDoFC (DoLetP fc t1 t2 alts) =
1045 DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1046 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1047mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1048mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1049mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1050mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1051mapPTermFC f g (PElabError err) = PElabError err
1052mapPTermFC f g PImpossible = PImpossible
1053mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1054mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1055mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1056mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1057mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1058mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1059mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1060mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1061mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1064dg instance Binary PTerm
1067mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1068mapPT f t = f (mpt t) where
1069 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1070 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1071 mpt (PLet fc rc n nfc ty v s) = PLet fc rc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1072 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1073 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1074 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1075 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1076 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1077 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1078 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1079 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1080 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1081 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1082 mpt (PHidden t) = PHidden (mapPT f t)
1083 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1084 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1085 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1086 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1087 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1088 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1089 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1093data PTactic' t = Intro [Name] | Intros | Focus Name
1094 | Refine Name [Bool] | Rewrite t | DoUnify
1101 | LetTac Name t | LetTacTy Name t t
1102 | Exact t | Compute | Trivial | TCImplementation
1103 | ProofSearch Bool Bool Int (Maybe Name)
1104 [Name] -- allowed local names
1106 -- ^ the bool is whether to search recursively
1109 | ProofState | ProofTerm | Undo
1110 | Try (PTactic' t) (PTactic' t)
1111 | TSeq (PTactic' t) (PTactic' t)
1112 | ApplyTactic t -- see Language.Reflection module
1116 | GoalType String (PTactic' t)
1119 | TDocStr (Either Name Const)
1122 | TFail [ErrorReportPart]
1125 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1127deriving instance Binary PTactic'
1129instance Sized a => Sized (PTactic' a) where
1130 size (Intro nms) = 1 + size nms
1132 size (Focus nm) = 1 + size nm
1133 size (Refine nm bs) = 1 + size nm + length bs
1134 size (Rewrite t) = 1 + size t
1135 size (Induction t) = 1 + size t
1136 size (LetTac nm t) = 1 + size nm + size t
1137 size (Exact t) = 1 + size t
1145 size (Try l r) = 1 + size l + size r
1146 size (TSeq l r) = 1 + size l + size r
1147 size (ApplyTactic t) = 1 + size t
1148 size (Reflect t) = 1 + size t
1149 size (Fill t) = 1 + size t
1153 size (TFail ts) = 1 + size ts
1156 size (CaseTac x) = 1 + size x
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 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 (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2283 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2284 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2285 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2286 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2287 ni 0 env (PHidden tm) = ni 0 env tm
2288 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2289 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2290 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2291 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2292 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2293 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2294 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2295 ni 0 env (PUnifyLog tm) = ni 0 env tm
2296 ni 0 env (PDisamb _ tm) = ni 0 env tm
2297 ni 0 env (PNoImplicits tm) = ni 0 env tm
2299 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2300 ni i env (PUnquote tm) = ni (i - 1) env tm
2301 ni i env tm = concatMap (ni i env) (children tm)
2303 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2307-- Return all names defined in binders in the given term
2308boundNamesIn :: PTerm -> [Name]
2309boundNamesIn tm = S.toList (ni 0 S.empty tm)
2310 where -- TODO THINK Added niTacImp, but is it right?
2311 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2312 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2313 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2314 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2315 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2316 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2317 ni 0 set (PLet fc rc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2318 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2319 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2320 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2321 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2322 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2323 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2324 ni 0 set (PAlternative ns a as) = niTms 0 set as
2325 ni 0 set (PHidden tm) = ni 0 set tm
2326 ni 0 set (PUnifyLog tm) = ni 0 set tm
2327 ni 0 set (PDisamb _ tm) = ni 0 set tm
2328 ni 0 set (PNoImplicits tm) = ni 0 set tm
2330 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2331 ni i set (PUnquote tm) = ni (i - 1) set tm
2333 ni i set tm = foldr (S.union . ni i set) set (children tm)
2335 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2336 niTms i set [] = set
2337 niTms i set (x : xs) = niTms i (ni i set x) xs
2339 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2340 niTacImp i set _ = set
2342-- Return names which are valid implicits in the given term (type).
2343implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2344implicitNamesIn uvars ist tm
2345 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2348 addImp n = do (imps, fns) <- get
2350 addFn n = do (imps, fns) <- get
2353 ni 0 env (PRef _ _ n@(NS _ _))
2354 | not (n `elem` env)
2355 -- Never implicitly bind if there's a namespace
2357 ni 0 env (PRef _ _ n)
2358 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2359 ni 0 env (PApp _ f@(PRef _ _ n) as)
2360 | n `elem` uvars = do ni 0 env f
2361 mapM_ (ni 0 env . getTm) as
2362 | otherwise = do case lookupTy n (tt_ctxt ist) of
2365 mapM_ (ni 0 env . getTm) as
2366 ni 0 env (PApp _ f as) = do ni 0 env f
2367 mapM_ (ni 0 env . getTm) as
2368 ni 0 env (PAppBind _ f as) = do ni 0 env f
2369 mapM_ (ni 0 env . getTm) as
2370 ni 0 env (PCase _ c os) = do ni 0 env c
2371 -- names in 'os', not counting the names bound in the cases
2372 mapM_ (ni 0 env . snd) os
2375 mapM_ (ni 0 env . fst) os
2377 put (nub imps \\ nub impsfst, fns)
2378 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2379 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2380 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2381 ni 0 env (PLet fc rc n _ ty val sc) = do ni 0 env ty;
2382 ni 0 env val; ni 0 (n:env) sc
2383 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2384 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2385 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2386 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2387 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2390 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2391 ni 0 env (PHidden tm) = ni 0 env tm
2392 ni 0 env (PUnifyLog tm) = ni 0 env tm
2393 ni 0 env (PDisamb _ tm) = ni 0 env tm
2394 ni 0 env (PNoImplicits tm) = ni 0 env tm
2396 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2397 maybe (return ()) (ni i env) ty
2398 ni i env (PUnquote tm) = ni (i - 1) env tm
2400 ni i env tm = mapM_ (ni i env) (children tm)
2402-- Return names which are free in the given term.
2403namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2404namesIn uvars ist tm = nub $ ni 0 [] tm
2406 ni 0 env (PRef _ _ n)
2407 | not (n `elem` env)
2408 = case lookupTy n (tt_ctxt ist) of
2410 _ -> [n | n `elem` (map fst uvars)]
2411 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2412 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2413 ni 0 env (PCase _ c os) = ni 0 env c ++
2414 -- names in 'os', not counting the names bound in the cases
2415 (nub (concatMap (ni 0 env . snd) os)
2416 \\ nub (concatMap (ni 0 env . fst) os))
2417 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2418 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2419 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2420 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2421 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2422 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2423 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2424 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2425 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2426 ni 0 env (PHidden tm) = ni 0 env tm
2427 ni 0 env (PUnifyLog tm) = ni 0 env tm
2428 ni 0 env (PDisamb _ tm) = ni 0 env tm
2429 ni 0 env (PNoImplicits tm) = ni 0 env tm
2431 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2432 ni i env (PUnquote tm) = ni (i - 1) env tm
2434 ni i env tm = concatMap (ni i env) (children tm)
2436 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2439-- Return which of the given names are used in the given term.
2441usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2442usedNamesIn vars ist tm = nub $ ni 0 [] tm
2443 where -- TODO THINK added niTacImp, but is it right?
2444 ni 0 env (PRef _ _ n)
2445 | n `elem` vars && not (n `elem` env)
2446 = case lookupDefExact n (tt_ctxt ist) of
2449 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2450 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2451 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2452 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2453 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2454 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2455 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2456 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2457 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2458 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2459 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2460 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2461 ni 0 env (PHidden tm) = ni 0 env tm
2462 ni 0 env (PUnifyLog tm) = ni 0 env tm
2463 ni 0 env (PDisamb _ tm) = ni 0 env tm
2464 ni 0 env (PNoImplicits tm) = ni 0 env tm
2466 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2467 ni i env (PUnquote tm) = ni (i - 1) env tm
2469 ni i env tm = concatMap (ni i env) (children tm)
2471 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2474-- Return the list of inaccessible (= dotted) positions for a name.
2475getErasureInfo :: IState -> Name -> [Int]
2476getErasureInfo ist n =
2477 case lookupCtxtExact n (idris_optimisation ist) of
2478 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