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)
930-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
932-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
933-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
934-- where updateCNs ns (PClause n l ts r ds)
935-- = PClause (updateN ns n) (fmap (updateNs ns) l)
936-- (map (fmap (updateNs ns)) ts)
937-- (fmap (updateNs ns) r)
938-- (map (updateDNs ns) ds)
944 deriving (Eq, Show, Ord, Data, Typeable, Generic)
946-- | High level language terms
947data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
948 -- high-level language
950 -- ^ A reference to a variable. The FC is its precise
951 -- source location for highlighting. The list of FCs is a
952 -- collection of additional highlighting locations.
953 | PInferRef FC [FC] Name -- ^ A name to be defined later
954 | PPatvar FC Name -- ^ A pattern variable
955 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
956 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
957 | PLet FC RigCount Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
958 | PTyped PTerm PTerm -- ^ Term with explicit type
959 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
960 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
961 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
962 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
963 | PMatchApp FC Name -- ^ Make an application by type matching
964 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
965 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
966 | PTrue FC PunInfo -- ^ Unit type..?
967 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
968 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
969 -- ^ "rewrite" syntax, with optional rewriting function and
970 -- optional result type
971 | PPair FC [FC] PunInfo PTerm PTerm
972 -- ^ A pair (a, b) and whether it's a product type or a
973 -- pair (solved by elaboration). The list of FCs is its
975 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
976 -- ^ A dependent pair (tm : a ** b) and whether it's a
977 -- sigma type or a pair that inhabits one (solved by
978 -- elaboration). The [FC] is its punctuation.
979 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
980 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
981 | PHidden PTerm -- ^ Irrelevant or hidden pattern
982 | PType FC -- ^ 'Type' type
983 | PUniverse FC Universe -- ^ Some universe
984 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
985 | PConstant FC Const -- ^ Builtin types
986 | Placeholder -- ^ Underscore
987 | PDoBlock [PDo] -- ^ Do notation
988 | PIdiom FC PTerm -- ^ Idiom brackets
989 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
990 | PProof [PTactic] -- ^ Proof script
991 | PTactics [PTactic] -- ^ As PProof, but no auto solving
992 | PElabError Err -- ^ Error to report on elaboration
993 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
994 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
995 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
996 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
997 | PNoImplicits PTerm -- ^ never run implicit converions on the term
998 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
999 | PUnquote PTerm -- ^ ~Term
1000 | PQuoteName Name Bool FC
1001 -- ^ `{n} where the FC is the precise highlighting for
1002 -- the name in particular. If the Bool is False, then
1003 -- it's `{{n}} and the name won't be resolved.
1004 | PRunElab FC PTerm [String]
1005 -- ^ %runElab tm - New-style proof script. Args are
1006 -- location, script, enclosing namespace.
1007 | PConstSugar FC PTerm
1008 -- ^ A desugared constant. The FC is a precise source
1009 -- location that will be used to highlight it later.
1010 deriving (Eq, Ord, Data, Typeable, Generic)
1012data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1015 deriving (Eq, Ord, Data, Generic, Typeable)
1017-- | Transform the FCs in a PTerm. The first function transforms the
1018-- general-purpose FCs, and the second transforms those that are used
1019-- for semantic source highlighting, so they can be treated specially.
1020mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1021mapPTermFC f g (PQuote q) = PQuote q
1022mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1023mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1024mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1025mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1026mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1027mapPTermFC 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)
1028mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1029mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1030mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1031mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1032mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1033mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1034mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1035mapPTermFC 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)
1036mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1037mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1038mapPTermFC 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)
1039mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1040mapPTermFC 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)
1041mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1042mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1043mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1044mapPTermFC f g (PType fc) = PType (f fc)
1045mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1046mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1047mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1048mapPTermFC f g Placeholder = Placeholder
1049mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1050 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1051 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1052 mapPDoFC (DoBindP fc t1 t2 alts) =
1053 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1054 mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1055 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1056 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1057mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1058mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1059mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1060mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1061mapPTermFC f g (PElabError err) = PElabError err
1062mapPTermFC f g PImpossible = PImpossible
1063mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1064mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1065mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1066mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1067mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1068mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1069mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1070mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1071mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1074dg instance Binary PTerm
1077mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1078mapPT f t = f (mpt t) where
1079 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1080 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1081 mpt (PLet fc rc n nfc ty v s) = PLet fc rc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1082 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1083 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1084 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1085 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1086 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1087 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1088 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1089 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1090 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1091 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1092 mpt (PHidden t) = PHidden (mapPT f t)
1093 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1094 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1095 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1096 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1097 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1098 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1099 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1103data PTactic' t = Intro [Name] | Intros | Focus Name
1104 | Refine Name [Bool] | Rewrite t | DoUnify
1111 | LetTac Name t | LetTacTy Name t t
1112 | Exact t | Compute | Trivial | TCImplementation
1113 | ProofSearch Bool Bool Int (Maybe Name)
1114 [Name] -- allowed local names
1116 -- ^ the bool is whether to search recursively
1119 | ProofState | ProofTerm | Undo
1120 | Try (PTactic' t) (PTactic' t)
1121 | TSeq (PTactic' t) (PTactic' t)
1122 | ApplyTactic t -- see Language.Reflection module
1126 | GoalType String (PTactic' t)
1129 | TDocStr (Either Name Const)
1132 | TFail [ErrorReportPart]
1135 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1137deriving instance Binary PTactic'
1139instance Sized a => Sized (PTactic' a) where
1140 size (Intro nms) = 1 + size nms
1142 size (Focus nm) = 1 + size nm
1143 size (Refine nm bs) = 1 + size nm + length bs
1144 size (Rewrite t) = 1 + size t
1145 size (Induction t) = 1 + size t
1146 size (LetTac nm t) = 1 + size nm + size t
1147 size (Exact t) = 1 + size t
1155 size (Try l r) = 1 + size l + size r
1156 size (TSeq l r) = 1 + size l + size r
1157 size (ApplyTactic t) = 1 + size t
1158 size (Reflect t) = 1 + size t
1159 size (Fill t) = 1 + size t
1163 size (TFail ts) = 1 + size ts
1166 size (CaseTac x) = 1 + size x
1167 size (Equiv t) = 1 + size t
1168 size (Claim x y) = 1 + size x + size y
1170 size (MatchRefine x) = 1 + size x
1171 size (LetTacTy x y z) = 1 + size x + size y + size z
1172 size TCImplementation = 1
1174type PTactic = PTactic' PTerm
1176data PDo' t = DoExp FC t
1177 | DoBind FC Name FC t -- ^ second FC is precise name location
1178 | DoBindP FC t t [(t,t)]
1179 | DoLet FC RigCount Name FC t t -- ^ second FC is precise name location
1181 | DoRewrite FC t -- rewrite in do block
1182 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1184deriving instance Binary PDo'
1187instance Sized a => Sized (PDo' a) where
1188 size (DoExp fc t) = 1 + size fc + size t
1189 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1190 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1191 size (DoLet fc rc nm nfc l r) = 1 + size fc + size nm + size l + size r
1192 size (DoLetP fc l r) = 1 + size fc + size l + size r
1193 size (DoRewrite fc h) = 1 + size fc + size h
1195type PDo = PDo' PTerm
1197-- The priority gives a hint as to elaboration order. Best to elaborate
1198-- things early which will help give a more concrete type to other
1199-- variables, e.g. a before (interpTy a).
1201data PArg' t = PImp { priority :: Int
1202 , machine_inf :: Bool -- ^ true if the machine inferred it
1203 , argopts :: [ArgOpt]
1207 | PExp { priority :: Int
1208 , argopts :: [ArgOpt]
1212 | PConstraint { priority :: Int
1213 , argopts :: [ArgOpt]
1217 | PTacImplicit { priority :: Int
1218 , argopts :: [ArgOpt]
1223 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1225data ArgOpt = AlwaysShow
1229 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1231instance Sized a => Sized (PArg' a) where
1232 size (PImp p _ l nm trm) = 1 + size nm + size trm
1233 size (PExp p l nm trm) = 1 + size nm + size trm
1234 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1235 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1238deriving instance Binary PArg'
1241pimp n t mach = PImp 1 mach [] n t
1242pexp t = PExp 1 [] (sMN 0 "arg") t
1243pconst t = PConstraint 1 [] (sMN 0 "carg") t
1244ptacimp n s t = PTacImplicit 2 [] n s t
1246type PArg = PArg' PTerm
1248-- | Get the highest FC in a term, if one exists
1249highestFC :: PTerm -> Maybe FC
1250highestFC (PQuote _) = Nothing
1251highestFC (PRef fc _ _) = Just fc
1252highestFC (PInferRef fc _ _) = Just fc
1253highestFC (PPatvar fc _) = Just fc
1254highestFC (PLam fc _ _ _ _) = Just fc
1255highestFC (PPi _ _ _ _ _) = Nothing
1256highestFC (PLet fc _ _ _ _ _ _) = Just fc
1257highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1258highestFC (PApp fc _ _) = Just fc
1259highestFC (PAppBind fc _ _) = Just fc
1260highestFC (PMatchApp fc _) = Just fc
1261highestFC (PCase fc _ _) = Just fc
1262highestFC (PIfThenElse fc _ _ _) = Just fc
1263highestFC (PTrue fc _) = Just fc
1264highestFC (PResolveTC fc) = Just fc
1265highestFC (PRewrite fc _ _ _ _) = Just fc
1266highestFC (PPair fc _ _ _ _) = Just fc
1267highestFC (PDPair fc _ _ _ _ _) = Just fc
1268highestFC (PAs fc _ _) = Just fc
1269highestFC (PAlternative _ _ args) =
1270 case mapMaybe highestFC args of
1273highestFC (PHidden _) = Nothing
1274highestFC (PType fc) = Just fc
1275highestFC (PUniverse _ _) = Nothing
1276highestFC (PGoal fc _ _ _) = Just fc
1277highestFC (PConstant fc _) = Just fc
1278highestFC Placeholder = Nothing
1279highestFC (PDoBlock lines) =
1280 case map getDoFC lines of
1284 getDoFC (DoExp fc t) = fc
1285 getDoFC (DoBind fc nm nfc t) = fc
1286 getDoFC (DoBindP fc l r alts) = fc
1287 getDoFC (DoLet fc rc nm nfc l r) = fc
1288 getDoFC (DoLetP fc l r) = fc
1289 getDoFC (DoRewrite fc h) = fc
1291highestFC (PIdiom fc _) = Just fc
1292highestFC (PMetavar fc _) = Just fc
1293highestFC (PProof _) = Nothing
1294highestFC (PTactics _) = Nothing
1295highestFC (PElabError _) = Nothing
1296highestFC PImpossible = Nothing
1297highestFC (PCoerced tm) = highestFC tm
1298highestFC (PDisamb _ opts) = highestFC opts
1299highestFC (PUnifyLog tm) = highestFC tm
1300highestFC (PNoImplicits tm) = highestFC tm
1301highestFC (PQuasiquote _ _) = Nothing
1302highestFC (PUnquote tm) = highestFC tm
1303highestFC (PQuoteName _ _ fc) = Just fc
1304highestFC (PRunElab fc _ _) = Just fc
1305highestFC (PConstSugar fc _) = Just fc
1306highestFC (PAppImpl t _) = highestFC t
1310data InterfaceInfo = CI {
1311 implementationCtorName :: Name
1312 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1313 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1314 , interface_default_super_interfaces :: [PDecl]
1315 , interface_impparams :: [Name]
1316 , interface_params :: [Name]
1317 , interface_constraints :: [PTerm]
1318 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1319 , interface_determiners :: [Int]
1320 } deriving (Show, Generic)
1322deriving instance Binary InterfaceInfo
1326data RecordInfo = RI {
1327 record_parameters :: [(Name,PTerm)]
1328 , record_constructor :: Name
1329 , record_projections :: [Name]
1330 } deriving (Show, Generic)
1332-- Type inference data
1334data TIData = TIPartial -- ^ a function with a partially defined type
1335 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1336 deriving (Show, Generic)
1338-- | Miscellaneous information about functions
1339data FnInfo = FnInfo { fn_params :: [Int] }
1340 deriving (Show, Generic)
1342deriving instance Binary FnInfo
1345data OptInfo = Optimise {
1346 inaccessible :: [(Int,Name)] -- includes names for error reporting
1347 , detaggable :: Bool
1348 , forceable :: [Int] -- argument positions which are forced by other values
1349 } deriving (Show, Generic)
1351deriving instance Binary OptInfo
1354-- | Syntactic sugar info
1359 , dsl_var :: Maybe t
1360 , index_first :: Maybe t
1361 , index_next :: Maybe t
1362 , dsl_lambda :: Maybe t
1363 , dsl_let :: Maybe t
1365 } deriving (Show, Functor, Generic)
1367deriving instance Binary DSL'
1370type DSL = DSL' PTerm
1372data SynContext = PatternSyntax
1375 deriving (Show, Generic)
1377deriving instance Binary SynContext
1380data Syntax = Rule [SSymbol] PTerm SynContext
1381 | DeclRule [SSymbol] [PDecl]
1382 deriving (Show, Generic)
1384syntaxNames :: Syntax -> [Name]
1385syntaxNames (Rule syms _ _) = mapMaybe ename syms
1386 where ename (Keyword n) = Just n
1388syntaxNames (DeclRule syms _) = mapMaybe ename syms
1389 where ename (Keyword n) = Just n
1392syntaxSymbols :: Syntax -> [SSymbol]
1393syntaxSymbols (Rule ss _ _) = ss
1394syntaxSymbols (DeclRule ss _) = ss
1396deriving instance Binary Syntax
1399data SSymbol = Keyword Name
1404 deriving (Show, Eq, Generic)
1408deriving instance Binary SSymbol
1411newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1414emptySyntaxRules :: SyntaxRules
1415emptySyntaxRules = SyntaxRules []
1417updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1418updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1420 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1425 ruleSort (s1:ss1) (s2:ss2) =
1426 case symCompare s1 s2 of
1427 EQ -> ruleSort ss1 ss2
1430 -- Better than creating Ord implementation for SSymbol since
1431 -- in general this ordering does not really make sense.
1432 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1433 symCompare (Keyword _) _ = LT
1434 symCompare (Symbol _) (Keyword _) = GT
1435 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1436 symCompare (Symbol _) _ = LT
1437 symCompare (Binding _) (Keyword _) = GT
1438 symCompare (Binding _) (Symbol _) = GT
1439 symCompare (Binding b1) (Binding b2) = compare b1 b2
1440 symCompare (Binding _) _ = LT
1441 symCompare (Expr _) (Keyword _) = GT
1442 symCompare (Expr _) (Symbol _) = GT
1443 symCompare (Expr _) (Binding _) = GT
1444 symCompare (Expr e1) (Expr e2) = compare e1 e2
1445 symCompare (Expr _) _ = LT
1446 symCompare (SimpleExpr _) (Keyword _) = GT
1447 symCompare (SimpleExpr _) (Symbol _) = GT
1448 symCompare (SimpleExpr _) (Binding _) = GT
1449 symCompare (SimpleExpr _) (Expr _) = GT
1450 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1452initDSL = DSL (PRef f [] (sUN ">>="))
1453 (PRef f [] (sUN "<*>"))
1454 (PRef f [] (sUN "pure"))
1461 where f = fileFC "(builtin)"
1463data Using = UImplicit Name PTerm
1464 | UConstraint Name [Name]
1465 deriving (Show, Eq, Data, Generic, Typeable)
1467deriving instance Binary Using
1470data SyntaxInfo = Syn {
1472 , syn_params :: [(Name, PTerm)]
1473 , syn_namespace :: [String]
1475 , imp_methods :: [Name]
1476 -- ^ interface methods. When expanding implicits, these should be
1477 -- expanded even under binders
1478 , decoration :: Name -> Name
1480 , implicitAllowed :: Bool
1481 , constraintAllowed :: Bool
1482 , maxline :: Maybe Int
1483 , mut_nesting :: Int
1485 , syn_in_quasiquote :: Int
1486 , syn_toplevel :: Bool
1487 , withAppAllowed :: Bool
1488 } deriving (Show, Generic)
1490deriving instance Binary SyntaxInfo
1493defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1495expandNS :: SyntaxInfo -> Name -> Name
1496expandNS syn n@(NS _ _) = n
1497expandNS syn n = case syn_namespace syn of
1502-- For inferring types of things
1504bi = fileFC "builtin"
1505primfc = fileFC "(primitive)"
1507inferTy = sMN 0 "__Infer"
1508inferCon = sMN 0 "__infer"
1509inferDecl = PDatadecl inferTy primfc
1511 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1512 PPi expl_linear (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1513 (PRef bi [] inferTy)), bi, [])]
1516infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1517infP = P (TCon 6 0) inferTy (TType (UVal 0))
1519getInferTerm, getInferType :: Term -> Term
1520getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1521getInferTerm (App _ (App _ _ _) tm) = tm
1522getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1524getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1525 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1526 toTy (PVar _ t) = PVTy t
1528getInferType (App _ (App _ _ ty) _) = ty
1532-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1534primNames = [inferTy, inferCon]
1537unitCon = sUN "MkUnit"
1539falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1540 "The empty type, also known as the trivially false proposition." ++
1542 "Use `void` or `absurd` to prove anything if you have a variable " ++
1543 "of type `Void` in scope."
1546pairTy = sNS (sUN "Pair") ["Builtins"]
1547pairCon = sNS (sUN "MkPair") ["Builtins"]
1549upairTy = sNS (sUN "UPair") ["Builtins"]
1550upairCon = sNS (sUN "MkUPair") ["Builtins"]
1554eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1555 "The propositional equality type. A proof that `x` = `y`." ++
1557 "To use such a proof, pattern-match on it, and the two equal things will " ++
1558 "then need to be the _same_ pattern." ++
1560 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1561 "is possible to state equalities between values of potentially different " ++
1562 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1564 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1566eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1567 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1569 [(reflDoc, reflParamDoc,
1570 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1571 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1572 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1573 pimp (n "B") Placeholder False,
1574 pexp (PRef bi [] (n "x")),
1575 pexp (PRef bi [] (n "x"))])), bi, [])]
1577 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1578 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1579 "shown that both sides are in fact equal."
1580 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1581 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1583eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1584 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1590-- | The special name to be used in the module documentation context -
1591-- not for use in the main definition context. The namespace around it
1592-- will determine the module to which the docs adhere.
1594modDocName = sMN 0 "ModuleDocs"
1596-- Defined in builtins.idr
1597sigmaTy = sNS (sUN "DPair") ["Builtins"]
1598sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1600piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1601piBind = piBindp expl
1603piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1605piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1608-- Pretty-printing declarations and terms
1610-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1611-- could interfere with interactive editing, which calls "show".
1613instance Show PTerm where
1614 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1616instance Show PDecl where
1617 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1619instance Show PClause where
1620 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1622instance Show PData where
1623 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1625instance Pretty PTerm OutputAnnotation where
1626 pretty = prettyImp defaultPPOption
1628-- | Colourise annotations according to an Idris state. It ignores the
1629-- names in the annotation, as there's no good way to show extended
1630-- information on a terminal.
1631annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1632annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1633annotationColour ist (AnnConst c) =
1634 let theme = idris_colourTheme ist
1635 in Just $ if constIsType c
1636 then typeColour theme
1637 else dataColour theme
1638annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1639annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1640annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1641annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1642annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1643annotationColour ist (AnnName n _ _ _) =
1644 let ctxt = tt_ctxt ist
1645 theme = idris_colourTheme ist
1647 _ | isDConName n ctxt -> Just $ dataColour theme
1648 _ | isFnName n ctxt -> Just $ functionColour theme
1649 _ | isTConName n ctxt -> Just $ typeColour theme
1650 _ | isPostulateName n ist -> Just $ postulateColour theme
1651 _ | otherwise -> Nothing -- don't colourise unknown names
1652annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1653 where colour BoldText = IdrisColour Nothing True False True False
1654 colour UnderlineText = IdrisColour Nothing True True False False
1655 colour ItalicText = IdrisColour Nothing True False False True
1656annotationColour ist _ = Nothing
1659-- | Colourise annotations according to an Idris state. It ignores the
1660-- names in the annotation, as there's no good way to show extended
1661-- information on a terminal. Note that strings produced this way will
1662-- not be coloured on Windows, so the use of the colour rendering
1663-- functions in Idris.Output is to be preferred.
1664consoleDecorate :: IState -> OutputAnnotation -> String -> String
1665consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1667isPostulateName :: Name -> IState -> Bool
1668isPostulateName n ist = S.member n (idris_postulates ist)
1670-- | Pretty-print a high-level closed Idris term with no information
1671-- about precedence/associativity
1672prettyImp :: PPOption -- ^ pretty printing options
1673 -> PTerm -- ^ the term to pretty-print
1674 -> Doc OutputAnnotation
1675prettyImp impl = pprintPTerm impl [] [] []
1677-- | Serialise something to base64 using its Binary implementation.
1679-- | Do the right thing for rendering a term in an IState
1680prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1681prettyIst ist = pprintPTerm opt [] [] (idris_infixes ist)
1683 opt = if LinearTypes `elem` idris_language_extensions ist
1684 then (ppOptionIst ist) { ppopt_displayrig = True }
1685 else ppOptionIst ist
1687-- | Pretty-print a high-level Idris term in some bindings context
1689pprintPTerm :: PPOption -- ^ pretty printing options
1690 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1691 -> [Name] -- ^ names to always show in pi, even if not used
1692 -> [FixDecl] -- ^ Fixity declarations
1693 -> PTerm -- ^ the term to pretty-print
1694 -> Doc OutputAnnotation
1695pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1699 lbrace = annotate (AnnSyntax "{") (text "{")
1700 rbrace = annotate (AnnSyntax "}") (text "}")
1701 percent = annotate (AnnSyntax "%") (text "%")
1703 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1704 prettySe d p bnd (PQuote r) =
1705 text "![" <> pretty r <> text "]"
1706 prettySe d p bnd (PPatvar fc n) = pretty n
1708 | Just str <- slist d p bnd e = depth d str
1709 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1710 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1711 prettySe d p bnd (PLam fc n nfc ty sc) =
1712 let (ns, sc') = getLamNames [n] sc in
1713 depth d . bracket p startPrec . group . align . hang 2 $
1714 (annotate (AnnSyntax "\\") (text "\\"))
1715 <> prettyBindingsOf ns False <+> text "=>" <$>
1716 prettySe (decD d) startPrec ((n, False):bnd) sc'
1718 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1719 getLamNames acc sc = (reverse acc, sc)
1721 prettyBindingsOf [] t = text ""
1722 prettyBindingsOf [n] t = prettyBindingOf n t
1723 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1724 prettyBindingsOf ns t
1725 prettySe d p bnd (PLet fc rc n nfc ty v sc) =
1726 depth d . bracket p startPrec . group . align $
1727 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1728 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1729 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1730 | Rig0 <- rig, ppopt_displayrig ppo =
1731 depth d . bracket p startPrec . group $
1732 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1733 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1734 | Rig1 <- rig, ppopt_displayrig ppo =
1735 depth d . bracket p startPrec . group $
1736 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1737 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1738 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1739 || ppopt_pinames ppo && uname n =
1740 depth d . bracket p startPrec . group $
1741 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1742 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1744 depth d . bracket p startPrec . group $
1745 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1746 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1748 uname (UN n) = case str n of
1755 Static -> percent <> text "static" <> space
1757 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1759 depth d . bracket p startPrec $
1760 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1761 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1762 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1763 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1765 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1766 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1767 showRig _ n = prettyBindingOf n True
1769 isPi (PPi (Exp{}) _ _ _ _) = True
1770 isPi (PPi _ _ _ _ sc) = isPi sc
1775 Static -> percent <> text "static" <> space
1777 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1778 depth d . bracket p startPrec $
1779 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1780 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1781 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1782 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1783 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1784 depth d . bracket p startPrec $
1785 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1786 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1787 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1788 | basename neg == sUN "negate" =
1789 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1790 -- This case preserves the behavior of the former constructor PEq.
1791 -- It should be removed if feasible when the pretty-printing of infix
1792 -- operators in general is improved.
1793 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1794 | n == eqTy, ppopt_impl ppo =
1795 depth d . bracket p eqPrec $
1796 enclose lparen rparen eq <+>
1797 align (group (vsep (map (prettyArgS (decD d) bnd)
1800 depth d . bracket p eqPrec . align . group $
1801 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1802 where eq = annName eqTy (text "=")
1804 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1805 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1806 | UN nm <- basename f
1807 , not (ppopt_impl ppo) && null (getShowArgs args) =
1808 prettyName True (ppopt_impl ppo) bnd f
1809 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1810 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1811 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1812 | UN nm <- basename op
1814 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1815 case getShowArgs args of
1817 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1818 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1819 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1820 (l@(PExp{}) : r@(PExp{}) : rest) ->
1821 depth d . bracket p funcAppPrec $
1822 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1823 align (group (vsep (map (prettyArgS d bnd) rest)))
1824 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1825 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1826 f = getFixity (opStr op)
1828 Nothing -> funcAppPrec + 1
1829 Just (Infixl p') -> p'
1830 Just f' -> prec f' + 1
1832 Nothing -> funcAppPrec + 1
1833 Just (Infixr p') -> p'
1834 Just f' -> prec f' + 1
1835 inFix l r = align . group $
1836 (prettySe (decD d) left bnd l <+> opName False) <$>
1837 group (prettySe (decD d) right bnd r)
1838 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1839 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1840 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1841 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1842 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1843 let args = getShowArgs as
1844 fp = prettySe (decD d) (startPrec + 1) bnd f
1845 shownArgs = if ppopt_impl ppo then as else args
1847 depth d . bracket p funcAppPrec . group $
1850 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1851 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1852 prettySe d p bnd (PCase _ scr cases) =
1853 bracket p funcAppPrec $
1854 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1855 depth d (indent 2 (vsep (map ppcase cases)))
1857 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1858 ([(n, False) | n <- vars l] ++ bnd)
1859 in nest nestingSize $
1860 prettyCase l <+> text "=>" <+> prettyCase r
1861 -- Warning: this is a bit of a hack. At this stage, we don't have the
1862 -- global context, so we can't determine which names are constructors,
1863 -- which are types, and which are pattern variables on the LHS of the
1864 -- case pattern. We use the heuristic that names without a namespace
1865 -- are patvars, because right now case blocks in PTerms are always
1866 -- delaborated from TT before being sent to the pretty-printer. If they
1867 -- start getting printed directly, THIS WILL BREAK.
1868 -- Potential solution: add a list of known patvars to the cases in
1869 -- PCase, and have the delaborator fill it out, kind of like the pun
1870 -- disambiguation on PDPair.
1871 vars tm = filter noNS (allNamesIn tm)
1872 noNS (NS _ _) = False
1875 prettySe d p bnd (PIfThenElse _ c t f) =
1876 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1877 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1878 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1879 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1881 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1882 prettySe d p bnd (PResolveTC _) = percent <> kwd "implementation"
1883 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1884 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1885 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1886 prettySe d p bnd (PRewrite _ by l r _) =
1887 depth d . bracket p startPrec $
1888 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1891 Just fn -> text "using" <+>
1892 prettyName True (ppopt_impl ppo) bnd fn) <+>
1893 text "in" <+> prettySe (decD d) startPrec bnd r
1894 prettySe d p bnd (PTyped l r) =
1895 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1896 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1897 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1898 align . group . vsep . punctuate (ann comma) $
1899 map (prettySe (decD d) startPrec bnd) elts
1900 where ann = case pun of
1902 IsType -> annName pairTy
1903 IsTerm -> annName pairCon
1904 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1905 | Just elts <- dPairElts dpair
1906 = depth d . enclose (annotated lparen) (annotated rparen) .
1907 align . group . vsep . punctuate (space <> annotated (text "**")) $
1913 annotated (text "**") <+>
1914 prettySe (decD d) startPrec (addBinding bnd) r <>
1916 where annotated = case pun of
1917 IsType -> annName sigmaTy
1918 IsTerm -> annName sigmaCon
1921 (left, addBinding) = case (l, pun) of
1922 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1923 _ -> (prettySe (decD d) startPrec bnd l, id)
1926 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1927 ppElts ((PRef _ _ n, t):rs) bs
1929 = (bindingOf n False <+> colon <+>
1930 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1931 ppElts ((l, t):rs) bs
1932 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1933 prettySe d p bnd (PAlternative ns a as) =
1934 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1937 foldr ((\ l r -> l <+> text "," <+> r) .
1938 depth d . prettySe (decD d) startPrec bnd)
1940 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1941 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1942 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1943 -- XXX: add pretty for tactics
1944 prettySe d p bnd (PProof ts) =
1945 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1946 prettySe d p bnd (PTactics ts) =
1947 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1948 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1949 prettySe d p bnd PImpossible = kwd "impossible"
1950 prettySe d p bnd Placeholder = text "_"
1951 prettySe d p bnd (PDoBlock dos) =
1952 bracket p startPrec $
1953 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1954 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1955 ppdo bnd (DoBind _ bn _ tm : dos) =
1956 (prettyBindingOf bn False <+> text "<-" <+>
1957 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1958 ppdo ((bn, False):bnd) dos
1959 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1960 text "no pretty printer for pattern-matching do binding" :
1962 ppdo bnd (DoLet _ _ ln _ ty v : dos) =
1963 (kwd "let" <+> prettyBindingOf ln False <+>
1964 (if ty /= Placeholder
1965 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1967 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1968 ppdo ((ln, False):bnd) dos
1969 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1970 text "no pretty printer for pattern-matching do binding" :
1972 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1973 text "no pretty printer for pattern-matching do binding" :
1976 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1977 prettySe d p bnd (PElabError s) = pretty s
1978 -- Quasiquote pprinting ignores bound vars
1979 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1980 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1981 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1982 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1983 where start = if res then "`{" else "`{{"
1984 end = if res then "}" else "}}"
1985 prettySe d p bnd (PRunElab _ tm _) =
1986 bracket p funcAppPrec . group . align . hang 2 $
1987 (percent <> text "runElab") <$>
1988 prettySe (decD d) funcAppPrec bnd tm
1989 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1990 prettySe d p bnd _ = text "missing pretty-printer for term"
1992 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1993 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1994 where display (UN n) = T.unpack n
1995 display (MN _ n) = T.unpack n
1996 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1997 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2000 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2001 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2002 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2003 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2005 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2006 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2007 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2008 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2010 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2011 annName n = annotate (AnnName n Nothing Nothing Nothing)
2013 opStr :: Name -> String
2014 opStr (NS n _) = opStr n
2015 opStr (UN n) = T.unpack n
2017 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2018 slist' (Just d) _ _ _ | d <= 0 = Nothing
2020 | containsHole e = Nothing
2021 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2022 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2023 slist' d p bnd (PRef _ _ nil)
2024 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2025 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2026 | nsroot cons == sUN "::",
2027 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2029 Just tl' <- slist' (decD d) p bnd tl
2030 = Just (prettySe d startPrec bnd hd : tl')
2032 isImp (PImp {}) = True
2034 slist' _ _ _ tm = Nothing
2036 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2038 [] -> annotate (AnnData "" "") $ text "[]"
2039 [x] -> enclose left right . group $ x
2040 xs -> enclose left right .
2041 align . group . vsep .
2042 punctuate comma $ xs
2043 where left = (annotate (AnnData "" "") (text "["))
2044 right = (annotate (AnnData "" "") (text "]"))
2045 comma = (annotate (AnnData "" "") (text ","))
2046 slist _ _ _ _ = Nothing
2048 pairElts :: PTerm -> Maybe [PTerm]
2049 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2050 | otherwise = Just [x, y]
2051 pairElts _ = Nothing
2053 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2054 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2055 | otherwise = Just [(l, t), (Placeholder, r)]
2056 dPairElts _ = Nothing
2058 natns = "Prelude.Nat."
2060 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2062 | ppopt_desugarnats ppo = Nothing
2063 | otherwise = snat' d p e
2065 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2066 snat' (Just x) _ _ | x <= 0 = Nothing
2067 snat' d p (PRef _ _ z)
2068 | show z == (natns++"Z") || show z == "Z" = Just 0
2069 snat' d p (PApp _ s [PExp {getTm=n}])
2070 | show s == (natns++"S") || show s == "S",
2071 Just n' <- snat' (decD d) p n
2073 snat' _ _ _ = Nothing
2075 bracket outer inner doc
2076 | outer > inner = lparen <> doc <> rparen
2079 ellipsis = text "..."
2082 depth (Just d) = if d <= 0 then const ellipsis else id
2084 decD = fmap (\x -> x - 1)
2086 kwd = annotate AnnKeyword . text
2088 fixities :: M.Map String Fixity
2089 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2091 getFixity :: String -> Maybe Fixity
2092 getFixity = flip M.lookup fixities
2094-- | Strip away namespace information
2095basename :: Name -> Name
2096basename (NS n _) = basename n
2099-- | Determine whether a name was the one inserted for a hole or guess
2100-- by the delaborator
2101isHoleName :: Name -> Bool
2102isHoleName (UN n) = n == T.pack "[__]"
2105-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2106containsHole :: PTerm -> Bool
2107containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2109-- | Pretty-printer helper for names that attaches the correct annotations
2110prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2111 -> Bool -- ^ whether to show namespaces
2112 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2113 -> Name -- ^ the name to pprint
2114 -> Doc OutputAnnotation
2115prettyName infixParen showNS bnd n
2116 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2117 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2118 | (UN n') <- n, T.unpack n' == "_" = text "_"
2119 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2120 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2121 where fullName = text nameSpace <> parenthesise (text (baseName n))
2122 baseName (UN n) = T.unpack n
2123 baseName (NS n ns) = baseName n
2124 baseName (MN i s) = T.unpack s
2125 baseName other = show other
2126 nameSpace = case n of
2127 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2129 isInfix = case baseName n of
2131 (c : _) -> not (isAlpha c)
2132 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2135showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2136showCImp ppo (PClause _ n l ws r w)
2137 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2138 <+> text "where" <+> text (show w)
2141 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2142showCImp ppo (PWith _ n l ws r pn w)
2143 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2144 <+> braces (text (show w))
2147 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2150showDImp :: PPOption -> PData -> Doc OutputAnnotation
2151showDImp ppo (PDatadecl n nfc ty cons)
2152 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2153 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2155showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2156showDecls o ds = vsep (map (showDeclImp o) ds)
2158showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2159showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2160showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2161 indent 2 (vsep (map (showCImp o) cs))
2162showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2163showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2164showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2165showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2166showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2167showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2168 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2169showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2170 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2171showDeclImp _ _ = text "..."
2172-- showDeclImp (PImport o) = "import " ++ o
2174getImps :: [PArg] -> [(Name, PTerm)]
2176getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2177getImps (_ : xs) = getImps xs
2179getExps :: [PArg] -> [PTerm]
2181getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2182getExps (_ : xs) = getExps xs
2184getShowArgs :: [PArg] -> [PArg]
2186getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2187getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2188 | PImp _ _ _ _ tm <- e
2189 , containsHole tm = e : getShowArgs xs
2190getShowArgs (_ : xs) = getShowArgs xs
2192getConsts :: [PArg] -> [PTerm]
2194getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2195getConsts (_ : xs) = getConsts xs
2197getAll :: [PArg] -> [PTerm]
2202showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2203 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2204 -> PPOption -- ^ pretty printing options
2205 -> Bool -- ^ whether to colourise
2206 -> Name -- ^ the term to show
2208showName ist bnd ppo colour n = case ist of
2209 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2210 Nothing -> showbasic n
2211 where name = if ppopt_impl ppo then show n else showbasic n
2212 showbasic n@(UN _) = showCG n
2213 showbasic (MN i s) = str s
2214 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2215 showbasic (SN s) = show s
2216 colourise n t = let ctxt' = fmap tt_ctxt ist in
2219 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2220 else colouriseBound t name
2221 | isDConName n ctxt -> colouriseData t name
2222 | isFnName n ctxt -> colouriseFun t name
2223 | isTConName n ctxt -> colouriseType t name
2224 -- The assumption is that if a name is not bound and does not exist in the
2225 -- global context, then we're somewhere in which implicit info has been lost
2226 -- (like error messages). Thus, unknown vars are colourised as implicits.
2227 | otherwise -> colouriseImplicit t name
2229showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2230 -> PTerm -- ^ the term to show
2232showTm ist = displayDecorated (consoleDecorate ist) .
2233 renderPretty 0.8 100000 .
2234 prettyImp (ppOptionIst ist)
2236-- | Show a term with implicits, no colours
2237showTmImpls :: PTerm -> String
2238showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2240-- | Show a term with specific options
2241showTmOpts :: PPOption -> PTerm -> String
2242showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2245instance Sized PTerm where
2246 size (PQuote rawTerm) = size rawTerm
2247 size (PRef fc _ name) = size name
2248 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2249 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2250 size (PLet fc _ name nfc ty def bdy) = 1 + size ty + size def + size bdy
2251 size (PTyped trm ty) = 1 + size trm + size ty
2252 size (PApp fc name args) = 1 + size args
2253 size (PAppBind fc name args) = 1 + size args
2254 size (PCase fc trm bdy) = 1 + size trm + size bdy
2255 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2256 size (PTrue fc _) = 1
2257 size (PResolveTC fc) = 1
2258 size (PRewrite fc by left right _) = 1 + size left + size right
2259 size (PPair fc _ _ left right) = 1 + size left + size right
2260 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2261 size (PAlternative _ a alts) = 1 + size alts
2262 size (PHidden hidden) = size hidden
2263 size (PUnifyLog tm) = size tm
2264 size (PDisamb _ tm) = size tm
2265 size (PNoImplicits tm) = size tm
2267 size (PUniverse _ _) = 1
2268 size (PConstant fc const) = 1 + size fc + size const
2269 size Placeholder = 1
2270 size (PDoBlock dos) = 1 + size dos
2271 size (PIdiom fc term) = 1 + size term
2272 size (PMetavar _ name) = 1
2273 size (PProof tactics) = size tactics
2274 size (PElabError err) = size err
2275 size PImpossible = 1
2278getPArity :: PTerm -> Int
2279getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2282-- Return all names, free or globally bound, in the given term.
2284allNamesIn :: PTerm -> [Name]
2285allNamesIn tm = nub $ ni 0 [] tm
2286 where -- TODO THINK added niTacImp, but is it right?
2287 ni 0 env (PRef _ _ n)
2288 | not (n `elem` env) = [n]
2289 ni 0 env (PPatvar _ n) = [n]
2290 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2291 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2292 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2293 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2294 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2295 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2296 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2297 ni 0 env (PHidden tm) = ni 0 env tm
2298 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2299 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2300 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2301 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2302 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2303 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2304 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2305 ni 0 env (PUnifyLog tm) = ni 0 env tm
2306 ni 0 env (PDisamb _ tm) = ni 0 env tm
2307 ni 0 env (PNoImplicits tm) = ni 0 env tm
2309 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2310 ni i env (PUnquote tm) = ni (i - 1) env tm
2311 ni i env tm = concatMap (ni i env) (children tm)
2313 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2317-- Return all names defined in binders in the given term
2318boundNamesIn :: PTerm -> [Name]
2319boundNamesIn tm = S.toList (ni 0 S.empty tm)
2320 where -- TODO THINK Added niTacImp, but is it right?
2321 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2322 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2323 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2324 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2325 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2326 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2327 ni 0 set (PLet fc rc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2328 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2329 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2330 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2331 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2332 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2333 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2334 ni 0 set (PAlternative ns a as) = niTms 0 set as
2335 ni 0 set (PHidden tm) = ni 0 set tm
2336 ni 0 set (PUnifyLog tm) = ni 0 set tm
2337 ni 0 set (PDisamb _ tm) = ni 0 set tm
2338 ni 0 set (PNoImplicits tm) = ni 0 set tm
2340 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2341 ni i set (PUnquote tm) = ni (i - 1) set tm
2343 ni i set tm = foldr (S.union . ni i set) set (children tm)
2345 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2346 niTms i set [] = set
2347 niTms i set (x : xs) = niTms i (ni i set x) xs
2349 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2350 niTacImp i set _ = set
2352-- Return names which are valid implicits in the given term (type).
2353implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2354implicitNamesIn uvars ist tm
2355 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2358 addImp n = do (imps, fns) <- get
2360 addFn n = do (imps, fns) <- get
2363 ni 0 env (PRef _ _ n@(NS _ _))
2364 | not (n `elem` env)
2365 -- Never implicitly bind if there's a namespace
2367 ni 0 env (PRef _ _ n)
2368 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2369 ni 0 env (PApp _ f@(PRef _ _ n) as)
2370 | n `elem` uvars = do ni 0 env f
2371 mapM_ (ni 0 env . getTm) as
2372 | otherwise = do case lookupTy n (tt_ctxt ist) of
2375 mapM_ (ni 0 env . getTm) as
2376 ni 0 env (PApp _ f as) = do ni 0 env f
2377 mapM_ (ni 0 env . getTm) as
2378 ni 0 env (PAppBind _ f as) = do ni 0 env f
2379 mapM_ (ni 0 env . getTm) as
2380 ni 0 env (PCase _ c os) = do ni 0 env c
2381 -- names in 'os', not counting the names bound in the cases
2382 mapM_ (ni 0 env . snd) os
2385 mapM_ (ni 0 env . fst) os
2387 put (nub imps \\ nub impsfst, fns)
2388 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2389 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2390 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2391 ni 0 env (PLet fc rc n _ ty val sc) = do ni 0 env ty;
2392 ni 0 env val; ni 0 (n:env) sc
2393 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2394 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2395 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2396 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2397 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2400 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2401 ni 0 env (PHidden tm) = ni 0 env tm
2402 ni 0 env (PUnifyLog tm) = ni 0 env tm
2403 ni 0 env (PDisamb _ tm) = ni 0 env tm
2404 ni 0 env (PNoImplicits tm) = ni 0 env tm
2406 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2407 maybe (return ()) (ni i env) ty
2408 ni i env (PUnquote tm) = ni (i - 1) env tm
2410 ni i env tm = mapM_ (ni i env) (children tm)
2412-- Return names which are free in the given term.
2413namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2414namesIn uvars ist tm = nub $ ni 0 [] tm
2416 ni 0 env (PRef _ _ n)
2417 | not (n `elem` env)
2418 = case lookupTy n (tt_ctxt ist) of
2420 _ -> [n | n `elem` (map fst uvars)]
2421 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2422 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2423 ni 0 env (PCase _ c os) = ni 0 env c ++
2424 -- names in 'os', not counting the names bound in the cases
2425 (nub (concatMap (ni 0 env . snd) os)
2426 \\ nub (concatMap (ni 0 env . fst) os))
2427 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2428 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2429 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2430 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2431 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2432 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2433 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2434 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2435 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2436 ni 0 env (PHidden tm) = ni 0 env tm
2437 ni 0 env (PUnifyLog tm) = ni 0 env tm
2438 ni 0 env (PDisamb _ tm) = ni 0 env tm
2439 ni 0 env (PNoImplicits tm) = ni 0 env tm
2441 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2442 ni i env (PUnquote tm) = ni (i - 1) env tm
2444 ni i env tm = concatMap (ni i env) (children tm)
2446 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2449-- Return which of the given names are used in the given term.
2451usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2452usedNamesIn vars ist tm = nub $ ni 0 [] tm
2453 where -- TODO THINK added niTacImp, but is it right?
2454 ni 0 env (PRef _ _ n)
2455 | n `elem` vars && not (n `elem` env)
2456 = case lookupDefExact n (tt_ctxt ist) of
2459 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2460 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2461 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2462 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2463 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2464 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2465 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2466 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2467 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2468 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2469 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2470 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2471 ni 0 env (PHidden tm) = ni 0 env tm
2472 ni 0 env (PUnifyLog tm) = ni 0 env tm
2473 ni 0 env (PDisamb _ tm) = ni 0 env tm
2474 ni 0 env (PNoImplicits tm) = ni 0 env tm
2476 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2477 ni i env (PUnquote tm) = ni (i - 1) env tm
2479 ni i env tm = concatMap (ni i env) (children tm)
2481 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2484-- Return the list of inaccessible (= dotted) positions for a name.
2485getErasureInfo :: IState -> Name -> [Int]
2486getErasureInfo ist n =
2487 case lookupCtxtExact n (idris_optimisation ist) of
2488 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