2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
9{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor, DeriveGeneric,
10 DeriveTraversable, FlexibleContexts, FlexibleInstances,
11 MultiParamTypeClasses, PatternGuards, TypeSynonymInstances #-}
13module Idris.AbsSyntaxTree where
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
18import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
29import Prelude hiding (Foldable, Traversable, (<$>))
31import Control.Applicative ((<|>))
32import qualified Control.Monad.Trans.Class as Trans (lift)
33import Control.Monad.Trans.Except
34import Control.Monad.Trans.State.Strict
36import Data.Data (Data)
38import Data.Foldable (Foldable)
39import Data.Function (on)
40import Data.Generics.Uniplate.Data (children, universe)
41import Data.List hiding (group)
42import qualified Data.Map.Strict as M
43import Data.Maybe (mapMaybe, maybeToList)
44import qualified Data.Set as S
45import qualified Data.Text as T
46import Data.Traversable (Traversable)
48import GHC.Generics (Generic)
51data ElabWhat = ETypes | EDefns | EAll
54-- | Data to pass to recursively called elaborators; e.g. for where blocks,
55-- paramaterised declarations, etc.
57-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
58-- so that we can have mutually recursive elaborators in separate modules without
59-- having to muck about with cyclic modules.
60data ElabInfo = EInfo {
61 params :: [(Name, PTerm)]
62 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
63 , liftname :: Name -> Name
64 , namespace :: [String]
66 , constraintNS :: String -- ^ filename for adding to constraint variables
68 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
69 -- | We may, recursively, collect transformations to do on the rhs,
70 -- e.g. rewriting recursive calls to functions defined by 'with'
71 , rhs_trans :: PTerm -> PTerm
72 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
76toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
78toplevelWith :: String -> ElabInfo
79toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
81eInfoNames :: ElabInfo -> [Name]
82eInfoNames info = map fst (params info) ++ M.keys (inblock info)
84data IOption = IOption {
86 , opt_logcats :: [LogCat] -- ^ List of logging categories.
87 , opt_typecase :: Bool
88 , opt_typeintype :: Bool
89 , opt_coverage :: Bool
90 , opt_showimp :: Bool -- ^ show implicits
91 , opt_errContext :: Bool
94 , opt_nobanner :: Bool
96 , opt_codegen :: Codegen
97 , opt_outputTy :: OutputType
98 , opt_ibcsubdir :: FilePath
99 , opt_importdirs :: [FilePath]
100 , opt_sourcedirs :: [FilePath]
101 , opt_triple :: String
103 , opt_cmdline :: [Opt] -- ^ remember whole command line
104 , opt_origerr :: Bool
105 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
106 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
107 , opt_optimise :: [Optimisation]
108 , opt_printdepth :: Maybe Int
109 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
110 , opt_desugarnats :: Bool
111 , opt_autoimpls :: Bool
112 } deriving (Show, Eq, Generic)
114defaultOpts :: IOption
115defaultOpts = IOption { opt_logLevel = 0
117 , opt_typecase = False
118 , opt_typeintype = False
119 , opt_coverage = True
120 , opt_showimp = False
121 , opt_errContext = False
124 , opt_nobanner = False
126 , opt_codegen = Via IBCFormat "c"
127 , opt_outputTy = Executable
129 , opt_importdirs = []
130 , opt_sourcedirs = []
134 , opt_origerr = False
135 , opt_autoSolve = True
136 , opt_autoImport = []
137 , opt_optimise = defaultOptimise
138 , opt_printdepth = Just 5000
139 , opt_evaltypes = True
140 , opt_desugarnats = False
141 , opt_autoimpls = True
144data PPOption = PPOption {
145 ppopt_impl :: Bool -- ^ whether to show implicits
146 , ppopt_desugarnats :: Bool
147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
148 , ppopt_depth :: Maybe Int
149 , ppopt_displayrig :: Bool -- ^ whether to display multiplicities in binders
154defaultOptimise :: [Optimisation]
157-- | Pretty printing options with default verbosity.
158defaultPPOption :: PPOption
159defaultPPOption = PPOption {
161 , ppopt_desugarnats = False
162 , ppopt_pinames = False
163 , ppopt_depth = Nothing
164 , ppopt_displayrig = False
167-- | Pretty printing options with the most verbosity.
168verbosePPOption :: PPOption
169verbosePPOption = PPOption {
171 , ppopt_desugarnats = True
172 , ppopt_pinames = True
173 , ppopt_depth = Nothing
174 , ppopt_displayrig = False
177-- | Get pretty printing options from the big options record.
178ppOption :: IOption -> PPOption
179ppOption opt = PPOption {
180 ppopt_impl = opt_showimp opt
181 , ppopt_pinames = False
182 , ppopt_depth = opt_printdepth opt
183 , ppopt_desugarnats = opt_desugarnats opt
184 , ppopt_displayrig = False
187-- | Get pretty printing options from an idris state record.
188ppOptionIst :: IState -> PPOption
189ppOptionIst = ppOption . idris_options
192-- | The output mode in use
193data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
194 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
198-- | If a function has no totality annotation, what do we assume?
199data DefaultTotality = DefaultCheckingTotal -- ^ Total
200 | DefaultCheckingPartial -- ^ Partial
201 | DefaultCheckingCovering -- ^Total coverage, but may diverge
202 deriving (Show, Eq, Generic)
204-- | Configuration options for interactive editing.
205data InteractiveOpts = InteractiveOpts {
206 interactiveOpts_indentWith :: Int
207 , interactiveOpts_indentClause :: Int
208} deriving (Show, Generic)
210-- | The global state used in the Idris monad
211data IState = IState {
212 tt_ctxt :: Context -- ^ All the currently defined names and their terms
213 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
214 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
215 , idris_implicits :: Ctxt [PArg]
216 , idris_statics :: Ctxt [Bool]
217 , idris_interfaces :: Ctxt InterfaceInfo
218 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
219 , idris_records :: Ctxt RecordInfo
220 , idris_dsls :: Ctxt DSL
221 , idris_optimisation :: Ctxt OptInfo
222 , idris_datatypes :: Ctxt TypeInfo
223 , idris_namehints :: Ctxt [Name]
225 -- | list of lhs/rhs, and a list of missing clauses. These are not
227 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
228 , idris_flags :: Ctxt [FnOpt]
229 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
230 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
232 -- | module documentation is saved in a special MN so the context
233 -- mechanism can be used for disambiguation.
234 , idris_moduledocs :: Ctxt (Docstring DocTerm)
235 , idris_tyinfodata :: Ctxt TIData
236 , idris_fninfo :: Ctxt FnInfo
237 , idris_transforms :: Ctxt [(Term, Term)]
238 , idris_autohints :: Ctxt [Name]
239 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
240 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
241 , idris_totcheckfail :: [(FC, String)]
242 , idris_options :: IOption
244 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
246 -- | The currently defined but not proven metavariables. The Int is
247 -- the number of vars to display as a context, the Maybe Name is its
248 -- top-level function, the [Name] is the list of local variables
249 -- available for proof search and the Bools are whether :p is
250 -- allowed, and whether the variable is definable at all
251 -- (Metavariables are not definable if they are applied in a term
252 -- which still has hole bindings)
253 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
254 , idris_coercions :: [Name]
255 , idris_errRev :: [(Term, Term)]
256 , idris_errReduce :: [Name]
257 , syntax_rules :: SyntaxRules
258 , syntax_keywords :: [String]
259 , imported :: [FilePath] -- ^ The imported modules
260 , idris_scprims :: [(Name, (Int, PrimFn))]
261 , idris_objs :: [(Codegen, FilePath)]
262 , idris_libs :: [(Codegen, String)]
263 , idris_cgflags :: [(Codegen, String)]
264 , idris_hdrs :: [(Codegen, String)]
265 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
266 , proof_list :: [(Name, (Bool, [String]))]
267 , errSpan :: Maybe FC
268 , parserWarnings :: [(FC, Err)]
269 , lastParse :: Maybe Name
270 , indent_stack :: [Int]
271 , brace_stack :: [Maybe Int]
272 , idris_parsedSpan :: Maybe FC
273 , hide_list :: Ctxt Accessibility
274 , default_access :: Accessibility
275 , default_total :: DefaultTotality
276 , ibc_write :: [IBCWrite]
277 , compiled_so :: Maybe String
278 , idris_dynamic_libs :: [DynamicLib]
279 , idris_language_extensions :: [LanguageExt]
280 , idris_outputmode :: OutputMode
281 , idris_colourRepl :: Bool
282 , idris_colourTheme :: ColourTheme
283 , idris_errorhandlers :: [Name] -- ^ Global error handlers
284 , idris_nameIdx :: (Int, Ctxt (Int, Name))
285 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
286 , module_aliases :: M.Map [T.Text] [T.Text]
287 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
288 , idris_postulates :: S.Set Name
289 , idris_externs :: S.Set (Name, Int)
290 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
292 -- | List of names that were defined in the repl, and can be re-/un-defined
293 , idris_repl_defs :: [Name]
295 -- | Stack of names currently being elaborated, Bool set if it's an
296 -- implementation (implementations appear twice; also as a function name)
297 , elab_stack :: [(Name, Bool)]
300 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
301 , idris_exports :: [Name] -- ^ Functions with ExportList
302 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
303 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
304 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
305 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
306 , idris_ttstats :: M.Map Term (Int, Term)
307 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
308 , idris_interactiveOpts :: InteractiveOpts
311-- Required for parsers library, and therefore trifecta
312instance Show IState where
313 show = const "{internal state}"
315data SizeChange = Smaller | Same | Bigger | Unknown
316 deriving (Show, Eq, Generic)
318deriving instance Binary SizeChange
321type SCGEntry = (Name, [Maybe (Int, SizeChange)])
322type UsageReason = (Name, Int) -- fn_name, its_arg_number
324data CGInfo = CGInfo {
325 calls :: [Name] -- Immediate calls
326 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
328 , usedpos :: [(Int, [UsageReason])]
329 } deriving (Show, Generic)
331deriving instance Binary CGInfo
335primDefs = [ sUN "unsafePerformPrimIO"
336 , sUN "mkLazyForeignPrim"
337 , sUN "mkForeignPrim"
339 , sUN "assert_unreachable"
343-- information that needs writing for the current module's .ibc file
344data IBCWrite = IBCFix FixDecl
349 | IBCImplementation Bool Bool Name Name
356 | IBCImport (Bool, FilePath) -- ^ True = import public
357 | IBCImportDir FilePath
358 | IBCSourceDir FilePath
359 | IBCObj Codegen FilePath
360 | IBCLib Codegen String
361 | IBCCGFlag Codegen String
363 | IBCHeader Codegen String
364 | IBCAccess Name Accessibility
365 | IBCMetaInformation Name MetaInformation
366 | IBCTotal Name Totality
367 | IBCInjective Name Injectivity
369 | IBCFnInfo Name FnInfo
370 | IBCTrans Name (Term, Term)
371 | IBCErrRev (Term, Term)
376 | IBCDef Name -- ^ The main context.
377 | IBCNameHint (Name, Name)
378 | IBCLineApp FilePath Int PTerm
379 | IBCErrorHandler Name
380 | IBCFunctionErrorHandler Name Name Name
382 | IBCExtern (Name, Int)
383 | IBCTotCheckErr FC String
385 | IBCModDocs Name -- ^ The name is the special name used to track module docs
386 | IBCUsage (Name, Int)
388 | IBCAutoHint Name Name
389 | IBCDeprecate Name String
390 | IBCFragile Name String
391 | IBCConstraint FC UConstraint
392 deriving (Show, Generic)
394initialInteractiveOpts :: InteractiveOpts
395initialInteractiveOpts = InteractiveOpts {
396 interactiveOpts_indentWith = 2
397 , interactiveOpts_indentClause = 2
400-- | The initial state for the compiler
402idrisInit = IState initContext S.empty []
403 emptyContext emptyContext emptyContext [] emptyContext
404 emptyContext emptyContext emptyContext emptyContext
405 emptyContext emptyContext emptyContext emptyContext
406 emptyContext emptyContext emptyContext emptyContext
408 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
409 [] [] Nothing [] Nothing [] [] Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
410 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
411 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
412 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
415-- | The monad for the main REPL - reading and processing files and
416-- updating global state (hence the IO inner monad).
419-- type Idris = WriterT [Either String (IO ())] (State IState a))
422type Idris = StateT IState (ExceptT Err IO)
424catchError :: Idris a -> (Err -> Idris a) -> Idris a
425catchError = liftCatch catchE
427throwError :: Err -> Idris a
428throwError = Trans.lift . throwE
430-- Commands in the REPL
435data ElabShellCmd = EQED
443 | EDocStr (Either Name Const)
449-- Parsed declarations
451data Fixity = Infixl { prec :: Int }
452 | Infixr { prec :: Int }
453 | InfixN { prec :: Int }
454 | PrefixN { prec :: Int }
455 deriving (Eq, Generic)
457deriving instance Binary Fixity
460instance Show Fixity where
461 show (Infixl i) = "infixl " ++ show i
462 show (Infixr i) = "infixr " ++ show i
463 show (InfixN i) = "infix " ++ show i
464 show (PrefixN i) = "prefix " ++ show i
466data FixDecl = Fix Fixity String
467 deriving (Eq, Generic)
469instance Show FixDecl where
470 show (Fix f s) = show f ++ " " ++ s
473deriving instance Binary FixDecl
476instance Ord FixDecl where
477 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
480data Static = Static | Dynamic
481 deriving (Show, Eq, Ord, Data, Generic, Typeable)
483deriving instance Binary Static
486-- ^ Mark bindings with their explicitness, and laziness
487data Plicity = Imp { pargopts :: [ArgOpt]
490 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
491 , pinsource :: Bool -- ^ Explicitly written in source
494 | Exp { pargopts :: [ArgOpt]
496 , pparam :: Bool -- ^ this is a param (rather than index)
499 | Constraint { pargopts :: [ArgOpt]
503 | TacImp { pargopts :: [ArgOpt]
508 deriving (Show, Eq, Ord, Data, Generic, Typeable)
511deriving instance Binary Plicity
514is_scoped :: Plicity -> Maybe ImplicitInfo
515is_scoped (Imp _ _ _ s _ _) = s
520impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
521-- Machine generated top level implicit
523impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
527forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
528forall_constraint :: Plicity
529forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
532expl = Exp [] Dynamic False RigW
534expl_param = Exp [] Dynamic True RigW
535expl_linear :: Plicity
536expl_linear = Exp [] Dynamic False Rig1
539constraint = Constraint [] Static RigW
541tacimpl :: PTerm -> Plicity
542tacimpl t = TacImp [] Dynamic t RigW
544data FnOpt = Inlinable -- ^ always evaluate when simplifying
545 | TotalFn | PartialFn | CoveringFn
546 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
549 -- | interface dictionary, eval only when a function
550 -- argument, and further evaluation results.
552 | OverlappingDictionary -- ^ Interface dictionary which may overlap
553 | Implicit -- ^ implicit coercion
554 | NoImplicit -- ^ do not apply implicit coercions
555 | CExport String -- ^ export, with a C name
556 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
557 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
558 | ErrorReduce -- ^ unfold definition before showing an error
559 | Reflection -- ^ a reflecting function, compile-time only
560 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
561 | Constructor -- ^ Data constructor type
562 | AutoHint -- ^ use in auto implicit search
563 | PEGenerated -- ^ generated by partial evaluator
564 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
565 deriving (Show, Eq, Generic)
567deriving instance Binary FnOpt
572inlinable :: FnOpts -> Bool
573inlinable = elem Inlinable
575dictionary :: FnOpts -> Bool
576dictionary = elem Dictionary
579-- | Type provider - what to provide
580data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
581 | ProvPostulate t -- ^ goal type must be Type, so only term
582 deriving (Show, Eq, Functor, Generic)
584type ProvideWhat = ProvideWhat' PTerm
586-- | Top-level declarations such as compiler directives, definitions,
587-- datatypes and interfaces.
589 -- | Fixity declaration
590 = PFix FC Fixity [String]
591 -- | Type declaration (last FC is precise name location)
592 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
593 -- | Postulate, second FC is precise name location
594 | PPostulate Bool -- external def if true
595 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
597 | PClauses FC FnOpts Name [PClause' t]
598 -- | Top level constant
600 -- | Data declaration.
601 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
603 | PParams FC [(Name, t)] [PDecl' t]
604 -- | Open block/declaration
605 | POpenInterfaces FC [Name] [PDecl' t]
606 -- | New namespace, where FC is accurate location of the namespace
608 | PNamespace String FC [PDecl' t]
610 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
612 FC -- Record name precise location
613 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
614 [(Name, Docstring (Either Err t))] -- Param Docs
615 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
616 (Maybe (Name, FC)) -- Optional constructor name and location
617 (Docstring (Either Err t)) -- Constructor doc
618 SyntaxInfo -- Constructor SyntaxInfo
620 -- | Interface: arguments are documentation, syntax info, source
621 -- location, constraints, interface name, interface name location,
622 -- parameters, method declarations, optional constructor name
623 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
624 [(Name, t)] -- constraints
625 Name -- interface name
626 FC -- accurate location of interface name
627 [(Name, FC, t)] -- parameters and precise locations
628 [(Name, Docstring (Either Err t))] -- parameter docstrings
629 [(Name, FC)] -- determining parameters and precise locations
630 [PDecl' t] -- declarations
631 (Maybe (Name, FC)) -- implementation constructor name and location
632 (Docstring (Either Err t)) -- implementation constructor docs
634 -- | Implementation declaration: arguments are documentation, syntax
635 -- info, source location, constraints, interface name, parameters, full
636 -- Implementation type, optional explicit name, and definitions
637 | PImplementation (Docstring (Either Err t)) -- Implementation docs
638 [(Name, Docstring (Either Err t))] -- Parameter docs
640 FC [(Name, t)] -- constraints
641 [Name] -- parent dictionaries to search for constraints
645 FC -- precise location of interface
647 [(Name, t)] -- Extra names in scope in the body
648 t -- full Implementation type
649 (Maybe Name) -- explicit name
651 | PDSL Name (DSL' t) -- ^ DSL declaration
652 | PSyntax FC Syntax -- ^ Syntax definition
653 | PMutual FC [PDecl' t] -- ^ Mutual block
654 | PDirective Directive -- ^ Compiler directive.
656 -- | Type provider. The first t is the type, the second is the
657 -- term. The second FC is precise highlighting location.
658 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
660 -- | Source-to-source transformation rule. If bool is True, lhs and
661 -- rhs must be convertible.
662 | PTransform FC Bool t t
664 -- | FC is decl-level, for errors, and Strings represent the
666 | PRunElabDecl FC t [String]
667 deriving (Functor, Generic)
669deriving instance Binary PDecl'
672-- | The set of source directives
673data Directive = DLib Codegen String
674 | DLink Codegen String
675 | DFlag Codegen String
676 | DInclude Codegen String
681 | DSetTotal Name -- assert totality after checking
682 | DAccess Accessibility
683 | DDefault DefaultTotality
685 | DDynamicLibs [String]
686 | DNameHint Name FC [(Name, FC)]
687 | DErrorHandlers Name FC Name FC [(Name, FC)]
688 | DLanguage LanguageExt
689 | DDeprecate Name String
690 | DFragile Name String
691 | DAutoImplicits Bool
695-- | A set of instructions for things that need to happen in IState
696-- after a term elaboration when there's been reflected elaboration.
697data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
698 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
699 | RAddImplementation Name Name
700 | RDatatypeDeclInstrs Name [PArg]
701 -- | Datatype, constructors
702 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
705-- | For elaborator state
706data EState = EState {
707 case_decls :: [(Name, PDecl)]
708 , delayed_elab :: [(Int, Elab' EState ())]
709 , new_tyDecls :: [RDeclInstructions]
710 , highlighting :: [(FC, OutputAnnotation)]
711 , auto_binds :: [Name] -- ^ names bound as auto implicits
712 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
716initEState = EState [] [] [] [] [] []
718type ElabD a = Elab' EState a
720highlightSource :: FC -> OutputAnnotation -> ElabD ()
721highlightSource fc annot =
722 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
724-- | One clause of a top-level definition. Term arguments to constructors are:
726-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
728-- 2. The list of extra 'with' patterns
730-- 3. The right-hand side
732-- 4. The where block (PDecl' t)
734data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
735 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
736 | PClauseR FC [t] t [PDecl' t]
737 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
738 deriving (Functor, Generic)
740deriving instance Binary PClause'
745 -- | Data declaration
746 PDatadecl { d_name :: Name -- ^ The name of the datatype
747 , d_name_fc :: FC -- ^ The precise location of the type constructor name
748 , d_tcon :: t -- ^ Type constructor
749 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
751 -- | "Placeholder" for data whose constructors are defined later
752 | PLaterdecl { d_name :: Name
755 } deriving (Functor, Generic)
757-- | Transform the FCs in a PData and its associated terms. The first
758-- function transforms the general-purpose FCs, and the second
759-- transforms those that are used for semantic source highlighting, so
760-- they can be treated specially.
761mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
762mapPDataFC f g (PDatadecl n nfc tycon ctors) =
763 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
764 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
765 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
766mapPDataFC f g (PLaterdecl n nfc tycon) =
767 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
769deriving instance Binary PData'
772-- Handy to get a free function for applying PTerm -> PTerm functions
773-- across a program, by deriving Functor
775type PDecl = PDecl' PTerm
776type PData = PData' PTerm
777type PClause = PClause' PTerm
779-- | Transform the FCs in a PTerm. The first function transforms the
780-- general-purpose FCs, and the second transforms those that are used
781-- for semantic source highlighting, so they can be treated specially.
782mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
783mapPDeclFC f g (PFix fc fixity ops) =
784 PFix (f fc) fixity ops
785mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
786 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
787mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
788 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
790mapPDeclFC f g (PClauses fc opts n clauses) =
791 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
792mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
793mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
794 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
795mapPDeclFC f g (PParams fc params decls) =
797 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
798 (map (mapPDeclFC f g) decls)
799mapPDeclFC f g (POpenInterfaces fc ifs decls) =
800 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
801mapPDeclFC f g (PNamespace ns fc decls) =
802 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
803mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
804 PRecord doc syn (f fc) opts n (g nfc)
805 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
807 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
808 plic, mapPTermFC f g ty, fdoc))
810 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
813mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
814 PInterface doc syn (f fc)
815 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
816 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
817 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
818 (map (mapPDeclFC f g) body)
819 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
821mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
822 PImplementation doc paramDocs syn (f fc)
823 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
824 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
825 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
826 (mapPTermFC f g implTy)
828 (map (mapPDeclFC f g) body)
829mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
830mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
832 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
833 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
834mapPDeclFC f g (PMutual fc decls) =
835 PMutual (f fc) (map (mapPDeclFC f g) decls)
836mapPDeclFC f g (PDirective d) =
839 DNameHint n nfc ns ->
840 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
841 DErrorHandlers n nfc n' nfc' ns ->
842 DErrorHandlers n (g nfc) n' (g nfc') $
843 map (\(an, anfc) -> (an, g anfc)) ns
844mapPDeclFC f g (PProvider doc syn fc nfc what n) =
845 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
846mapPDeclFC f g (PTransform fc safe l r) =
847 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
848mapPDeclFC f g (PRunElabDecl fc script ns) =
849 PRunElabDecl (f fc) (mapPTermFC f g script) ns
851-- | Get all the names declared in a declaration
852declared :: PDecl -> [Name]
853declared (PFix _ _ _) = []
854declared (PTy _ _ _ _ _ n fc t) = [n]
855declared (PPostulate _ _ _ _ _ _ n t) = [n]
856declared (PClauses _ _ n _) = [] -- not a declaration
857declared (PCAF _ n _) = [n]
858declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
859 where fstt (_, _, a, _, _, _, _) = a
860declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
861declared (PParams _ _ ds) = concatMap declared ds
862declared (POpenInterfaces _ _ ds) = concatMap declared ds
863declared (PNamespace _ _ ds) = concatMap declared ds
864declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
865declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
866declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
870declared (PDSL n _) = [n]
871declared (PSyntax _ _) = []
872declared (PMutual _ ds) = concatMap declared ds
873declared (PDirective _) = []
876-- get the names declared, not counting nested parameter blocks
877tldeclared :: PDecl -> [Name]
878tldeclared (PFix _ _ _) = []
879tldeclared (PTy _ _ _ _ _ n _ t) = [n]
880tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
881tldeclared (PClauses _ _ n _) = [] -- not a declaration
882tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
883tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
884 where fstt (_, _, a, _, _, _, _) = a
885tldeclared (PParams _ _ ds) = []
886tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
887tldeclared (PMutual _ ds) = concatMap tldeclared ds
888tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
889tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
890tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
896defined :: PDecl -> [Name]
897defined (PFix _ _ _) = []
898defined (PTy _ _ _ _ _ n _ t) = []
899defined (PPostulate _ _ _ _ _ _ n t) = []
900defined (PClauses _ _ n _) = [n] -- not a declaration
901defined (PCAF _ n _) = [n]
902defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
903 where fstt (_, _, a, _, _, _, _) = a
904defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
905defined (PParams _ _ ds) = concatMap defined ds
906defined (POpenInterfaces _ _ ds) = concatMap defined ds
907defined (PNamespace _ _ ds) = concatMap defined ds
908defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
909defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
910defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
914defined (PDSL n _) = [n]
915defined (PSyntax _ _) = []
916defined (PMutual _ ds) = concatMap defined ds
917defined (PDirective _) = []
920updateN :: [(Name, Name)] -> Name -> Name
921updateN ns n | Just n' <- lookup n ns = n'
924updateNs :: [(Name, Name)] -> PTerm -> PTerm
926updateNs ns t = mapPT updateRef t
927 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
933 deriving (Eq, Show, Ord, Data, Typeable, Generic)
935-- | High level language terms
936data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
937 -- high-level language
939 -- ^ A reference to a variable. The FC is its precise
940 -- source location for highlighting. The list of FCs is a
941 -- collection of additional highlighting locations.
942 | PInferRef FC [FC] Name -- ^ A name to be defined later
943 | PPatvar FC Name -- ^ A pattern variable
944 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
945 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
946 | PLet FC RigCount Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
947 | PTyped PTerm PTerm -- ^ Term with explicit type
948 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
949 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
950 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
951 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
952 | PMatchApp FC Name -- ^ Make an application by type matching
953 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
954 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
955 | PTrue FC PunInfo -- ^ Unit type..?
956 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
957 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
958 -- ^ "rewrite" syntax, with optional rewriting function and
959 -- optional result type
960 | PPair FC [FC] PunInfo PTerm PTerm
961 -- ^ A pair (a, b) and whether it's a product type or a
962 -- pair (solved by elaboration). The list of FCs is its
964 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
965 -- ^ A dependent pair (tm : a ** b) and whether it's a
966 -- sigma type or a pair that inhabits one (solved by
967 -- elaboration). The [FC] is its punctuation.
968 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
969 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
970 | PHidden PTerm -- ^ Irrelevant or hidden pattern
971 | PType FC -- ^ 'Type' type
972 | PUniverse FC Universe -- ^ Some universe
973 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
974 | PConstant FC Const -- ^ Builtin types
975 | Placeholder -- ^ Underscore
976 | PDoBlock [PDo] -- ^ Do notation
977 | PIdiom FC PTerm -- ^ Idiom brackets
978 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
979 | PProof [PTactic] -- ^ Proof script
980 | PTactics [PTactic] -- ^ As PProof, but no auto solving
981 | PElabError Err -- ^ Error to report on elaboration
982 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
983 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
984 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
985 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
986 | PNoImplicits PTerm -- ^ never run implicit converions on the term
987 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
988 | PUnquote PTerm -- ^ ~Term
989 | PQuoteName Name Bool FC
990 -- ^ `{n} where the FC is the precise highlighting for
991 -- the name in particular. If the Bool is False, then
992 -- it's `{{n}} and the name won't be resolved.
993 | PRunElab FC PTerm [String]
994 -- ^ %runElab tm - New-style proof script. Args are
995 -- location, script, enclosing namespace.
996 | PConstSugar FC PTerm
997 -- ^ A desugared constant. The FC is a precise source
998 -- location that will be used to highlight it later.
999 deriving (Eq, Ord, Data, Typeable, Generic)
1001data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1004 deriving (Eq, Ord, Data, Generic, Typeable)
1006-- | Transform the FCs in a PTerm. The first function transforms the
1007-- general-purpose FCs, and the second transforms those that are used
1008-- for semantic source highlighting, so they can be treated specially.
1009mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1010mapPTermFC f g (PQuote q) = PQuote q
1011mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1012mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1013mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1014mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1015mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1016mapPTermFC f g (PLet fc rc n fc' t1 t2 t3) = PLet (f fc) rc n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1017mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1018mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1019mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1020mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1021mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1022mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1023mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1024mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)
1025mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1026mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1027mapPTermFC f g (PRewrite fc by t1 t2 t3) = PRewrite (f fc) by (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1028mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1029mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1030mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1031mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1032mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1033mapPTermFC f g (PType fc) = PType (f fc)
1034mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1035mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1036mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1037mapPTermFC f g Placeholder = Placeholder
1038mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1039 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1040 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1041 mapPDoFC (DoBindP fc t1 t2 alts) =
1042 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1043 mapPDoFC (DoLet fc rc n nfc t1 t2) = DoLet (f fc) rc n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1044 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1045 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1046mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1047mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1048mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1049mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1050mapPTermFC f g (PElabError err) = PElabError err
1051mapPTermFC f g PImpossible = PImpossible
1052mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1053mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1054mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1055mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1056mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1057mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1058mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1059mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1060mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1063dg instance Binary PTerm
1066mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1067mapPT f t = f (mpt t) where
1068 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1069 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1070 mpt (PLet fc rc n nfc ty v s) = PLet fc rc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1071 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1072 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1073 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1074 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1075 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1076 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1077 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1078 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1079 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1080 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1081 mpt (PHidden t) = PHidden (mapPT f t)
1082 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1083 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1084 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1085 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1086 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1087 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1088 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1092data PTactic' t = Intro [Name] | Intros | Focus Name
1093 | Refine Name [Bool] | Rewrite t | DoUnify
1100 | LetTac Name t | LetTacTy Name t t
1101 | Exact t | Compute | Trivial | TCImplementation
1102 | ProofSearch Bool Bool Int (Maybe Name)
1103 [Name] -- allowed local names
1105 -- ^ the bool is whether to search recursively
1108 | ProofState | ProofTerm | Undo
1109 | Try (PTactic' t) (PTactic' t)
1110 | TSeq (PTactic' t) (PTactic' t)
1111 | ApplyTactic t -- see Language.Reflection module
1115 | GoalType String (PTactic' t)
1118 | TDocStr (Either Name Const)
1121 | TFail [ErrorReportPart]
1124 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1126deriving instance Binary PTactic'
1128instance Sized a => Sized (PTactic' a) where
1129 size (Intro nms) = 1 + size nms
1131 size (Focus nm) = 1 + size nm
1132 size (Refine nm bs) = 1 + size nm + length bs
1133 size (Rewrite t) = 1 + size t
1134 size (Induction t) = 1 + size t
1135 size (LetTac nm t) = 1 + size nm + size t
1136 size (Exact t) = 1 + size t
1144 size (Try l r) = 1 + size l + size r
1145 size (TSeq l r) = 1 + size l + size r
1146 size (ApplyTactic t) = 1 + size t
1147 size (Reflect t) = 1 + size t
1148 size (Fill t) = 1 + size t
1152 size (TFail ts) = 1 + size ts
1155 size (CaseTac x) = 1 + size x
1156 size (Equiv t) = 1 + size t
1157 size (Claim x y) = 1 + size x + size y
1159 size (MatchRefine x) = 1 + size x
1160 size (LetTacTy x y z) = 1 + size x + size y + size z
1161 size TCImplementation = 1
1163type PTactic = PTactic' PTerm
1165data PDo' t = DoExp FC t
1166 | DoBind FC Name FC t -- ^ second FC is precise name location
1167 | DoBindP FC t t [(t,t)]
1168 | DoLet FC RigCount Name FC t t -- ^ second FC is precise name location
1170 | DoRewrite FC t -- rewrite in do block
1171 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1173deriving instance Binary PDo'
1176instance Sized a => Sized (PDo' a) where
1177 size (DoExp fc t) = 1 + size fc + size t
1178 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1179 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1180 size (DoLet fc rc nm nfc l r) = 1 + size fc + size nm + size l + size r
1181 size (DoLetP fc l r) = 1 + size fc + size l + size r
1182 size (DoRewrite fc h) = 1 + size fc + size h
1184type PDo = PDo' PTerm
1186-- The priority gives a hint as to elaboration order. Best to elaborate
1187-- things early which will help give a more concrete type to other
1188-- variables, e.g. a before (interpTy a).
1190data PArg' t = PImp { priority :: Int
1191 , machine_inf :: Bool -- ^ true if the machine inferred it
1192 , argopts :: [ArgOpt]
1196 | PExp { priority :: Int
1197 , argopts :: [ArgOpt]
1201 | PConstraint { priority :: Int
1202 , argopts :: [ArgOpt]
1206 | PTacImplicit { priority :: Int
1207 , argopts :: [ArgOpt]
1212 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1214data ArgOpt = AlwaysShow
1218 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1220instance Sized a => Sized (PArg' a) where
1221 size (PImp p _ l nm trm) = 1 + size nm + size trm
1222 size (PExp p l nm trm) = 1 + size nm + size trm
1223 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1224 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1227deriving instance Binary PArg'
1230pimp n t mach = PImp 1 mach [] n t
1231pexp t = PExp 1 [] (sMN 0 "arg") t
1232pconst t = PConstraint 1 [] (sMN 0 "carg") t
1233ptacimp n s t = PTacImplicit 2 [] n s t
1235type PArg = PArg' PTerm
1237-- | Get the highest FC in a term, if one exists
1238highestFC :: PTerm -> Maybe FC
1239highestFC (PQuote _) = Nothing
1240highestFC (PRef fc _ _) = Just fc
1241highestFC (PInferRef fc _ _) = Just fc
1242highestFC (PPatvar fc _) = Just fc
1243highestFC (PLam fc _ _ _ _) = Just fc
1244highestFC (PPi _ _ _ _ _) = Nothing
1245highestFC (PLet fc _ _ _ _ _ _) = Just fc
1246highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1247highestFC (PApp fc _ _) = Just fc
1248highestFC (PAppBind fc _ _) = Just fc
1249highestFC (PMatchApp fc _) = Just fc
1250highestFC (PCase fc _ _) = Just fc
1251highestFC (PIfThenElse fc _ _ _) = Just fc
1252highestFC (PTrue fc _) = Just fc
1253highestFC (PResolveTC fc) = Just fc
1254highestFC (PRewrite fc _ _ _ _) = Just fc
1255highestFC (PPair fc _ _ _ _) = Just fc
1256highestFC (PDPair fc _ _ _ _ _) = Just fc
1257highestFC (PAs fc _ _) = Just fc
1258highestFC (PAlternative _ _ args) =
1259 case mapMaybe highestFC args of
1262highestFC (PHidden _) = Nothing
1263highestFC (PType fc) = Just fc
1264highestFC (PUniverse _ _) = Nothing
1265highestFC (PGoal fc _ _ _) = Just fc
1266highestFC (PConstant fc _) = Just fc
1267highestFC Placeholder = Nothing
1268highestFC (PDoBlock lines) =
1269 case map getDoFC lines of
1273 getDoFC (DoExp fc t) = fc
1274 getDoFC (DoBind fc nm nfc t) = fc
1275 getDoFC (DoBindP fc l r alts) = fc
1276 getDoFC (DoLet fc rc nm nfc l r) = fc
1277 getDoFC (DoLetP fc l r) = fc
1278 getDoFC (DoRewrite fc h) = fc
1280highestFC (PIdiom fc _) = Just fc
1281highestFC (PMetavar fc _) = Just fc
1282highestFC (PProof _) = Nothing
1283highestFC (PTactics _) = Nothing
1284highestFC (PElabError _) = Nothing
1285highestFC PImpossible = Nothing
1286highestFC (PCoerced tm) = highestFC tm
1287highestFC (PDisamb _ opts) = highestFC opts
1288highestFC (PUnifyLog tm) = highestFC tm
1289highestFC (PNoImplicits tm) = highestFC tm
1290highestFC (PQuasiquote _ _) = Nothing
1291highestFC (PUnquote tm) = highestFC tm
1292highestFC (PQuoteName _ _ fc) = Just fc
1293highestFC (PRunElab fc _ _) = Just fc
1294highestFC (PConstSugar fc _) = Just fc
1295highestFC (PAppImpl t _) = highestFC t
1299data InterfaceInfo = CI {
1300 implementationCtorName :: Name
1301 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1302 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1303 , interface_default_super_interfaces :: [PDecl]
1304 , interface_impparams :: [Name]
1305 , interface_params :: [Name]
1306 , interface_constraints :: [PTerm]
1307 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1308 , interface_determiners :: [Int]
1309 } deriving (Show, Generic)
1311deriving instance Binary InterfaceInfo
1315data RecordInfo = RI {
1316 record_parameters :: [(Name,PTerm)]
1317 , record_constructor :: Name
1318 , record_projections :: [Name]
1319 } deriving (Show, Generic)
1321-- Type inference data
1323data TIData = TIPartial -- ^ a function with a partially defined type
1324 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1325 deriving (Show, Generic)
1327-- | Miscellaneous information about functions
1328data FnInfo = FnInfo { fn_params :: [Int] }
1329 deriving (Show, Generic)
1331deriving instance Binary FnInfo
1334data OptInfo = Optimise {
1335 inaccessible :: [(Int,Name)] -- includes names for error reporting
1336 , detaggable :: Bool
1337 , forceable :: [Int] -- argument positions which are forced by other values
1338 } deriving (Show, Generic)
1340deriving instance Binary OptInfo
1343-- | Syntactic sugar info
1348 , dsl_var :: Maybe t
1349 , index_first :: Maybe t
1350 , index_next :: Maybe t
1351 , dsl_lambda :: Maybe t
1352 , dsl_let :: Maybe t
1354 } deriving (Show, Functor, Generic)
1356deriving instance Binary DSL'
1359type DSL = DSL' PTerm
1361data SynContext = PatternSyntax
1364 deriving (Show, Generic)
1366deriving instance Binary SynContext
1369data Syntax = Rule [SSymbol] PTerm SynContext
1370 | DeclRule [SSymbol] [PDecl]
1371 deriving (Show, Generic)
1373syntaxNames :: Syntax -> [Name]
1374syntaxNames (Rule syms _ _) = mapMaybe ename syms
1375 where ename (Keyword n) = Just n
1377syntaxNames (DeclRule syms _) = mapMaybe ename syms
1378 where ename (Keyword n) = Just n
1381syntaxSymbols :: Syntax -> [SSymbol]
1382syntaxSymbols (Rule ss _ _) = ss
1383syntaxSymbols (DeclRule ss _) = ss
1385deriving instance Binary Syntax
1388data SSymbol = Keyword Name
1393 deriving (Show, Eq, Generic)
1397deriving instance Binary SSymbol
1400newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1403emptySyntaxRules :: SyntaxRules
1404emptySyntaxRules = SyntaxRules []
1406updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1407updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1409 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1414 ruleSort (s1:ss1) (s2:ss2) =
1415 case symCompare s1 s2 of
1416 EQ -> ruleSort ss1 ss2
1419 -- Better than creating Ord implementation for SSymbol since
1420 -- in general this ordering does not really make sense.
1421 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1422 symCompare (Keyword _) _ = LT
1423 symCompare (Symbol _) (Keyword _) = GT
1424 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1425 symCompare (Symbol _) _ = LT
1426 symCompare (Binding _) (Keyword _) = GT
1427 symCompare (Binding _) (Symbol _) = GT
1428 symCompare (Binding b1) (Binding b2) = compare b1 b2
1429 symCompare (Binding _) _ = LT
1430 symCompare (Expr _) (Keyword _) = GT
1431 symCompare (Expr _) (Symbol _) = GT
1432 symCompare (Expr _) (Binding _) = GT
1433 symCompare (Expr e1) (Expr e2) = compare e1 e2
1434 symCompare (Expr _) _ = LT
1435 symCompare (SimpleExpr _) (Keyword _) = GT
1436 symCompare (SimpleExpr _) (Symbol _) = GT
1437 symCompare (SimpleExpr _) (Binding _) = GT
1438 symCompare (SimpleExpr _) (Expr _) = GT
1439 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1441initDSL = DSL (PRef f [] (sUN ">>="))
1442 (PRef f [] (sUN "<*>"))
1443 (PRef f [] (sUN "pure"))
1450 where f = fileFC "(builtin)"
1452data Using = UImplicit Name PTerm
1453 | UConstraint Name [Name]
1454 deriving (Show, Eq, Data, Generic, Typeable)
1456deriving instance Binary Using
1459data SyntaxInfo = Syn {
1461 , syn_params :: [(Name, PTerm)]
1462 , syn_namespace :: [String]
1464 , imp_methods :: [Name]
1465 -- ^ interface methods. When expanding implicits, these should be
1466 -- expanded even under binders
1467 , decoration :: Name -> Name
1469 , implicitAllowed :: Bool
1470 , constraintAllowed :: Bool
1471 , maxline :: Maybe Int
1472 , mut_nesting :: Int
1474 , syn_in_quasiquote :: Int
1475 , syn_toplevel :: Bool
1476 , withAppAllowed :: Bool
1477 } deriving (Show, Generic)
1479deriving instance Binary SyntaxInfo
1482defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1484expandNS :: SyntaxInfo -> Name -> Name
1485expandNS syn n@(NS _ _) = n
1486expandNS syn n = case syn_namespace syn of
1491-- For inferring types of things
1493bi = fileFC "builtin"
1494primfc = fileFC "(primitive)"
1496inferTy = sMN 0 "__Infer"
1497inferCon = sMN 0 "__infer"
1498inferDecl = PDatadecl inferTy primfc
1500 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1501 PPi expl_linear (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1502 (PRef bi [] inferTy)), bi, [])]
1505infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1506infP = P (TCon 6 0) inferTy (TType (UVal 0))
1508getInferTerm, getInferType :: Term -> Term
1509getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1510getInferTerm (App _ (App _ _ _) tm) = tm
1511getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1513getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1514 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1515 toTy (PVar _ t) = PVTy t
1517getInferType (App _ (App _ _ ty) _) = ty
1521-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1523primNames = [inferTy, inferCon]
1526unitCon = sUN "MkUnit"
1528falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1529 "The empty type, also known as the trivially false proposition." ++
1531 "Use `void` or `absurd` to prove anything if you have a variable " ++
1532 "of type `Void` in scope."
1535pairTy = sNS (sUN "Pair") ["Builtins"]
1536pairCon = sNS (sUN "MkPair") ["Builtins"]
1538upairTy = sNS (sUN "UPair") ["Builtins"]
1539upairCon = sNS (sUN "MkUPair") ["Builtins"]
1543eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1544 "The propositional equality type. A proof that `x` = `y`." ++
1546 "To use such a proof, pattern-match on it, and the two equal things will " ++
1547 "then need to be the _same_ pattern." ++
1549 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1550 "is possible to state equalities between values of potentially different " ++
1551 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1553 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1555eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1556 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1558 [(reflDoc, reflParamDoc,
1559 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1560 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1561 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1562 pimp (n "B") Placeholder False,
1563 pexp (PRef bi [] (n "x")),
1564 pexp (PRef bi [] (n "x"))])), bi, [])]
1566 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1567 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1568 "shown that both sides are in fact equal."
1569 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1570 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1572eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1573 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1579-- | The special name to be used in the module documentation context -
1580-- not for use in the main definition context. The namespace around it
1581-- will determine the module to which the docs adhere.
1583modDocName = sMN 0 "ModuleDocs"
1585-- Defined in builtins.idr
1586sigmaTy = sNS (sUN "DPair") ["Builtins"]
1587sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1589piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1590piBind = piBindp expl
1592piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1594piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1597-- Pretty-printing declarations and terms
1599-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1600-- could interfere with interactive editing, which calls "show".
1602instance Show PTerm where
1603 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1605instance Show PDecl where
1606 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1608instance Show PClause where
1609 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1611instance Show PData where
1612 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1614instance Pretty PTerm OutputAnnotation where
1615 pretty = prettyImp defaultPPOption
1617-- | Colourise annotations according to an Idris state. It ignores the
1618-- names in the annotation, as there's no good way to show extended
1619-- information on a terminal.
1620annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1621annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1622annotationColour ist (AnnConst c) =
1623 let theme = idris_colourTheme ist
1624 in Just $ if constIsType c
1625 then typeColour theme
1626 else dataColour theme
1627annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1628annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1629annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1630annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1631annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1632annotationColour ist (AnnName n _ _ _) =
1633 let ctxt = tt_ctxt ist
1634 theme = idris_colourTheme ist
1636 _ | isDConName n ctxt -> Just $ dataColour theme
1637 _ | isFnName n ctxt -> Just $ functionColour theme
1638 _ | isTConName n ctxt -> Just $ typeColour theme
1639 _ | isPostulateName n ist -> Just $ postulateColour theme
1640 _ | otherwise -> Nothing -- don't colourise unknown names
1641annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1642 where colour BoldText = IdrisColour Nothing True False True False
1643 colour UnderlineText = IdrisColour Nothing True True False False
1644 colour ItalicText = IdrisColour Nothing True False False True
1645annotationColour ist _ = Nothing
1648-- | Colourise annotations according to an Idris state. It ignores the
1649-- names in the annotation, as there's no good way to show extended
1650-- information on a terminal. Note that strings produced this way will
1651-- not be coloured on Windows, so the use of the colour rendering
1652-- functions in Idris.Output is to be preferred.
1653consoleDecorate :: IState -> OutputAnnotation -> String -> String
1654consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1656isPostulateName :: Name -> IState -> Bool
1657isPostulateName n ist = S.member n (idris_postulates ist)
1659-- | Pretty-print a high-level closed Idris term with no information
1660-- about precedence/associativity
1661prettyImp :: PPOption -- ^ pretty printing options
1662 -> PTerm -- ^ the term to pretty-print
1663 -> Doc OutputAnnotation
1664prettyImp impl = pprintPTerm impl [] [] []
1666-- | Serialise something to base64 using its Binary implementation.
1668-- | Do the right thing for rendering a term in an IState
1669prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1670prettyIst ist = pprintPTerm opt [] [] (idris_infixes ist)
1672 opt = if LinearTypes `elem` idris_language_extensions ist
1673 then (ppOptionIst ist) { ppopt_displayrig = True }
1674 else ppOptionIst ist
1676-- | Pretty-print a high-level Idris term in some bindings context
1678pprintPTerm :: PPOption -- ^ pretty printing options
1679 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1680 -> [Name] -- ^ names to always show in pi, even if not used
1681 -> [FixDecl] -- ^ Fixity declarations
1682 -> PTerm -- ^ the term to pretty-print
1683 -> Doc OutputAnnotation
1684pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1688 lbrace = annotate (AnnSyntax "{") (text "{")
1689 rbrace = annotate (AnnSyntax "}") (text "}")
1690 percent = annotate (AnnSyntax "%") (text "%")
1692 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1693 prettySe d p bnd (PQuote r) =
1694 text "![" <> pretty r <> text "]"
1695 prettySe d p bnd (PPatvar fc n) = pretty n
1697 | Just str <- slist d p bnd e = depth d str
1698 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1699 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1700 prettySe d p bnd (PLam fc n nfc ty sc) =
1701 let (ns, sc') = getLamNames [n] sc in
1702 depth d . bracket p startPrec . group . align . hang 2 $
1703 (annotate (AnnSyntax "\\") (text "\\"))
1704 <> prettyBindingsOf ns False <+> text "=>" <$>
1705 prettySe (decD d) startPrec ((n, False):bnd) sc'
1707 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1708 getLamNames acc sc = (reverse acc, sc)
1710 prettyBindingsOf [] t = text ""
1711 prettyBindingsOf [n] t = prettyBindingOf n t
1712 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1713 prettyBindingsOf ns t
1714 prettySe d p bnd (PLet fc rc n nfc ty v sc) =
1715 depth d . bracket p startPrec . group . align $
1716 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1717 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1718 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1719 | Rig0 <- rig, ppopt_displayrig ppo =
1720 depth d . bracket p startPrec . group $
1721 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1722 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1723 | Rig1 <- rig, ppopt_displayrig ppo =
1724 depth d . bracket p startPrec . group $
1725 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1726 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1727 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1728 || ppopt_pinames ppo && uname n =
1729 depth d . bracket p startPrec . group $
1730 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1731 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1733 depth d . bracket p startPrec . group $
1734 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1735 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1737 uname (UN n) = case str n of
1744 Static -> percent <> text "static" <> space
1746 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1748 depth d . bracket p startPrec $
1749 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1750 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1751 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1752 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1754 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1755 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1756 showRig _ n = prettyBindingOf n True
1758 isPi (PPi (Exp{}) _ _ _ _) = True
1759 isPi (PPi _ _ _ _ sc) = isPi sc
1764 Static -> percent <> text "static" <> space
1766 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1767 depth d . bracket p startPrec $
1768 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1769 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1770 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1771 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1772 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1773 depth d . bracket p startPrec $
1774 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1775 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1776 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1777 | basename neg == sUN "negate" =
1778 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1779 -- This case preserves the behavior of the former constructor PEq.
1780 -- It should be removed if feasible when the pretty-printing of infix
1781 -- operators in general is improved.
1782 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1783 | n == eqTy, ppopt_impl ppo =
1784 depth d . bracket p eqPrec $
1785 enclose lparen rparen eq <+>
1786 align (group (vsep (map (prettyArgS (decD d) bnd)
1789 depth d . bracket p eqPrec . align . group $
1790 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1791 where eq = annName eqTy (text "=")
1793 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1794 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1795 | UN nm <- basename f
1796 , not (ppopt_impl ppo) && null (getShowArgs args) =
1797 prettyName True (ppopt_impl ppo) bnd f
1798 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1799 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1800 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1801 | UN nm <- basename op
1803 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1804 case getShowArgs args of
1806 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1807 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1808 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1809 (l@(PExp{}) : r@(PExp{}) : rest) ->
1810 depth d . bracket p funcAppPrec $
1811 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1812 align (group (vsep (map (prettyArgS d bnd) rest)))
1813 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1814 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1815 f = getFixity (opStr op)
1817 Nothing -> funcAppPrec + 1
1818 Just (Infixl p') -> p'
1819 Just f' -> prec f' + 1
1821 Nothing -> funcAppPrec + 1
1822 Just (Infixr p') -> p'
1823 Just f' -> prec f' + 1
1824 inFix l r = align . group $
1825 (prettySe (decD d) left bnd l <+> opName False) <$>
1826 group (prettySe (decD d) right bnd r)
1827 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1828 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1829 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1830 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1831 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1832 let args = getShowArgs as
1833 fp = prettySe (decD d) (startPrec + 1) bnd f
1834 shownArgs = if ppopt_impl ppo then as else args
1836 depth d . bracket p funcAppPrec . group $
1839 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1840 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1841 prettySe d p bnd (PCase _ scr cases) =
1842 bracket p funcAppPrec $
1843 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1844 depth d (indent 2 (vsep (map ppcase cases)))
1846 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1847 ([(n, False) | n <- vars l] ++ bnd)
1848 in nest nestingSize $
1849 prettyCase l <+> text "=>" <+> prettyCase r
1850 -- Warning: this is a bit of a hack. At this stage, we don't have the
1851 -- global context, so we can't determine which names are constructors,
1852 -- which are types, and which are pattern variables on the LHS of the
1853 -- case pattern. We use the heuristic that names without a namespace
1854 -- are patvars, because right now case blocks in PTerms are always
1855 -- delaborated from TT before being sent to the pretty-printer. If they
1856 -- start getting printed directly, THIS WILL BREAK.
1857 -- Potential solution: add a list of known patvars to the cases in
1858 -- PCase, and have the delaborator fill it out, kind of like the pun
1859 -- disambiguation on PDPair.
1860 vars tm = filter noNS (allNamesIn tm)
1861 noNS (NS _ _) = False
1864 prettySe d p bnd (PIfThenElse _ c t f) =
1865 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1866 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1867 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1868 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1870 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1871 prettySe d p bnd (PResolveTC _) = percent <> kwd "implementation"
1872 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1873 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1874 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1875 prettySe d p bnd (PRewrite _ by l r _) =
1876 depth d . bracket p startPrec $
1877 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1880 Just fn -> text "using" <+>
1881 prettyName True (ppopt_impl ppo) bnd fn) <+>
1882 text "in" <+> prettySe (decD d) startPrec bnd r
1883 prettySe d p bnd (PTyped l r) =
1884 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1885 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1886 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1887 align . group . vsep . punctuate (ann comma) $
1888 map (prettySe (decD d) startPrec bnd) elts
1889 where ann = case pun of
1891 IsType -> annName pairTy
1892 IsTerm -> annName pairCon
1893 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1894 | Just elts <- dPairElts dpair
1895 = depth d . enclose (annotated lparen) (annotated rparen) .
1896 align . group . vsep . punctuate (space <> annotated (text "**")) $
1902 annotated (text "**") <+>
1903 prettySe (decD d) startPrec (addBinding bnd) r <>
1905 where annotated = case pun of
1906 IsType -> annName sigmaTy
1907 IsTerm -> annName sigmaCon
1910 (left, addBinding) = case (l, pun) of
1911 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1912 _ -> (prettySe (decD d) startPrec bnd l, id)
1915 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1916 ppElts ((PRef _ _ n, t):rs) bs
1918 = (bindingOf n False <+> colon <+>
1919 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1920 ppElts ((l, t):rs) bs
1921 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1922 prettySe d p bnd (PAlternative ns a as) =
1923 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1926 foldr ((\ l r -> l <+> text "," <+> r) .
1927 depth d . prettySe (decD d) startPrec bnd)
1929 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1930 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1931 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1932 -- XXX: add pretty for tactics
1933 prettySe d p bnd (PProof ts) =
1934 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1935 prettySe d p bnd (PTactics ts) =
1936 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1937 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1938 prettySe d p bnd PImpossible = kwd "impossible"
1939 prettySe d p bnd Placeholder = text "_"
1940 prettySe d p bnd (PDoBlock dos) =
1941 bracket p startPrec $
1942 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1943 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1944 ppdo bnd (DoBind _ bn _ tm : dos) =
1945 (prettyBindingOf bn False <+> text "<-" <+>
1946 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1947 ppdo ((bn, False):bnd) dos
1948 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1949 text "no pretty printer for pattern-matching do binding" :
1951 ppdo bnd (DoLet _ _ ln _ ty v : dos) =
1952 (kwd "let" <+> prettyBindingOf ln False <+>
1953 (if ty /= Placeholder
1954 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1956 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1957 ppdo ((ln, False):bnd) dos
1958 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1959 text "no pretty printer for pattern-matching do binding" :
1961 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1962 text "no pretty printer for pattern-matching do binding" :
1965 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1966 prettySe d p bnd (PElabError s) = pretty s
1967 -- Quasiquote pprinting ignores bound vars
1968 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1969 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1970 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1971 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1972 where start = if res then "`{" else "`{{"
1973 end = if res then "}" else "}}"
1974 prettySe d p bnd (PRunElab _ tm _) =
1975 bracket p funcAppPrec . group . align . hang 2 $
1976 (percent <> text "runElab") <$>
1977 prettySe (decD d) funcAppPrec bnd tm
1978 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1979 prettySe d p bnd _ = text "missing pretty-printer for term"
1981 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1982 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1983 where display (UN n) = T.unpack n
1984 display (MN _ n) = T.unpack n
1985 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1986 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1989 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1990 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1991 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1992 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1994 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1995 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1996 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1997 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1999 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2000 annName n = annotate (AnnName n Nothing Nothing Nothing)
2002 opStr :: Name -> String
2003 opStr (NS n _) = opStr n
2004 opStr (UN n) = T.unpack n
2006 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2007 slist' (Just d) _ _ _ | d <= 0 = Nothing
2009 | containsHole e = Nothing
2010 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2011 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2012 slist' d p bnd (PRef _ _ nil)
2013 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2014 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2015 | nsroot cons == sUN "::",
2016 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2018 Just tl' <- slist' (decD d) p bnd tl
2019 = Just (prettySe d startPrec bnd hd : tl')
2021 isImp (PImp {}) = True
2023 slist' _ _ _ tm = Nothing
2025 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2027 [] -> annotate (AnnData "" "") $ text "[]"
2028 [x] -> enclose left right . group $ x
2029 xs -> enclose left right .
2030 align . group . vsep .
2031 punctuate comma $ xs
2032 where left = (annotate (AnnData "" "") (text "["))
2033 right = (annotate (AnnData "" "") (text "]"))
2034 comma = (annotate (AnnData "" "") (text ","))
2035 slist _ _ _ _ = Nothing
2037 pairElts :: PTerm -> Maybe [PTerm]
2038 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2039 | otherwise = Just [x, y]
2040 pairElts _ = Nothing
2042 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2043 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2044 | otherwise = Just [(l, t), (Placeholder, r)]
2045 dPairElts _ = Nothing
2047 natns = "Prelude.Nat."
2049 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2051 | ppopt_desugarnats ppo = Nothing
2052 | otherwise = snat' d p e
2054 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2055 snat' (Just x) _ _ | x <= 0 = Nothing
2056 snat' d p (PRef _ _ z)
2057 | show z == (natns++"Z") || show z == "Z" = Just 0
2058 snat' d p (PApp _ s [PExp {getTm=n}])
2059 | show s == (natns++"S") || show s == "S",
2060 Just n' <- snat' (decD d) p n
2062 snat' _ _ _ = Nothing
2064 bracket outer inner doc
2065 | outer > inner = lparen <> doc <> rparen
2068 ellipsis = text "..."
2071 depth (Just d) = if d <= 0 then const ellipsis else id
2073 decD = fmap (\x -> x - 1)
2075 kwd = annotate AnnKeyword . text
2077 fixities :: M.Map String Fixity
2078 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2080 getFixity :: String -> Maybe Fixity
2081 getFixity = flip M.lookup fixities
2083-- | Strip away namespace information
2084basename :: Name -> Name
2085basename (NS n _) = basename n
2088-- | Determine whether a name was the one inserted for a hole or guess
2089-- by the delaborator
2090isHoleName :: Name -> Bool
2091isHoleName (UN n) = n == T.pack "[__]"
2094-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2095containsHole :: PTerm -> Bool
2096containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2098-- | Pretty-printer helper for names that attaches the correct annotations
2099prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2100 -> Bool -- ^ whether to show namespaces
2101 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2102 -> Name -- ^ the name to pprint
2103 -> Doc OutputAnnotation
2104prettyName infixParen showNS bnd n
2105 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2106 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2107 | (UN n') <- n, T.unpack n' == "_" = text "_"
2108 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2109 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2110 where fullName = text nameSpace <> parenthesise (text (baseName n))
2111 baseName (UN n) = T.unpack n
2112 baseName (NS n ns) = baseName n
2113 baseName (MN i s) = T.unpack s
2114 baseName other = show other
2115 nameSpace = case n of
2116 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2118 isInfix = case baseName n of
2120 (c : _) -> not (isAlpha c)
2121 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2124showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2125showCImp ppo (PClause _ n l ws r w)
2126 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2127 <+> text "where" <+> text (show w)
2130 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2131showCImp ppo (PWith _ n l ws r pn w)
2132 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2133 <+> braces (text (show w))
2136 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2139showDImp :: PPOption -> PData -> Doc OutputAnnotation
2140showDImp ppo (PDatadecl n nfc ty cons)
2141 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2142 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2144showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2145showDecls o ds = vsep (map (showDeclImp o) ds)
2147showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2148showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2149showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2150 indent 2 (vsep (map (showCImp o) cs))
2151showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2152showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2153showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2154showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2155showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2156showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2157 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2158showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2159 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2160showDeclImp _ _ = text "..."
2161-- showDeclImp (PImport o) = "import " ++ o
2163getImps :: [PArg] -> [(Name, PTerm)]
2165getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2166getImps (_ : xs) = getImps xs
2168getExps :: [PArg] -> [PTerm]
2170getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2171getExps (_ : xs) = getExps xs
2173getShowArgs :: [PArg] -> [PArg]
2175getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2176getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2177 | PImp _ _ _ _ tm <- e
2178 , containsHole tm = e : getShowArgs xs
2179getShowArgs (_ : xs) = getShowArgs xs
2181getConsts :: [PArg] -> [PTerm]
2183getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2184getConsts (_ : xs) = getConsts xs
2186getAll :: [PArg] -> [PTerm]
2191showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2192 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2193 -> PPOption -- ^ pretty printing options
2194 -> Bool -- ^ whether to colourise
2195 -> Name -- ^ the term to show
2197showName ist bnd ppo colour n = case ist of
2198 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2199 Nothing -> showbasic n
2200 where name = if ppopt_impl ppo then show n else showbasic n
2201 showbasic n@(UN _) = showCG n
2202 showbasic (MN i s) = str s
2203 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2204 showbasic (SN s) = show s
2205 colourise n t = let ctxt' = fmap tt_ctxt ist in
2208 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2209 else colouriseBound t name
2210 | isDConName n ctxt -> colouriseData t name
2211 | isFnName n ctxt -> colouriseFun t name
2212 | isTConName n ctxt -> colouriseType t name
2213 -- The assumption is that if a name is not bound and does not exist in the
2214 -- global context, then we're somewhere in which implicit info has been lost
2215 -- (like error messages). Thus, unknown vars are colourised as implicits.
2216 | otherwise -> colouriseImplicit t name
2218showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2219 -> PTerm -- ^ the term to show
2221showTm ist = displayDecorated (consoleDecorate ist) .
2222 renderPretty 0.8 100000 .
2223 prettyImp (ppOptionIst ist)
2225-- | Show a term with implicits, no colours
2226showTmImpls :: PTerm -> String
2227showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2229-- | Show a term with specific options
2230showTmOpts :: PPOption -> PTerm -> String
2231showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2234instance Sized PTerm where
2235 size (PQuote rawTerm) = size rawTerm
2236 size (PRef fc _ name) = size name
2237 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2238 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2239 size (PLet fc _ name nfc ty def bdy) = 1 + size ty + size def + size bdy
2240 size (PTyped trm ty) = 1 + size trm + size ty
2241 size (PApp fc name args) = 1 + size args
2242 size (PAppBind fc name args) = 1 + size args
2243 size (PCase fc trm bdy) = 1 + size trm + size bdy
2244 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2245 size (PTrue fc _) = 1
2246 size (PResolveTC fc) = 1
2247 size (PRewrite fc by left right _) = 1 + size left + size right
2248 size (PPair fc _ _ left right) = 1 + size left + size right
2249 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2250 size (PAlternative _ a alts) = 1 + size alts
2251 size (PHidden hidden) = size hidden
2252 size (PUnifyLog tm) = size tm
2253 size (PDisamb _ tm) = size tm
2254 size (PNoImplicits tm) = size tm
2256 size (PUniverse _ _) = 1
2257 size (PConstant fc const) = 1 + size fc + size const
2258 size Placeholder = 1
2259 size (PDoBlock dos) = 1 + size dos
2260 size (PIdiom fc term) = 1 + size term
2261 size (PMetavar _ name) = 1
2262 size (PProof tactics) = size tactics
2263 size (PElabError err) = size err
2264 size PImpossible = 1
2267getPArity :: PTerm -> Int
2268getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2271-- Return all names, free or globally bound, in the given term.
2273allNamesIn :: PTerm -> [Name]
2274allNamesIn tm = nub $ ni 0 [] tm
2275 where -- TODO THINK added niTacImp, but is it right?
2276 ni 0 env (PRef _ _ n)
2277 | not (n `elem` env) = [n]
2278 ni 0 env (PPatvar _ n) = [n]
2279 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2280 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2281 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2282 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2283 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2284 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2285 ni 0 env (PLet _ _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2286 ni 0 env (PHidden tm) = ni 0 env tm
2287 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2288 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2289 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2290 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2291 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2292 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2293 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2294 ni 0 env (PUnifyLog tm) = ni 0 env tm
2295 ni 0 env (PDisamb _ tm) = ni 0 env tm
2296 ni 0 env (PNoImplicits tm) = ni 0 env tm
2298 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2299 ni i env (PUnquote tm) = ni (i - 1) env tm
2300 ni i env tm = concatMap (ni i env) (children tm)
2302 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2306-- Return all names defined in binders in the given term
2307boundNamesIn :: PTerm -> [Name]
2308boundNamesIn tm = S.toList (ni 0 S.empty tm)
2309 where -- TODO THINK Added niTacImp, but is it right?
2310 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2311 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2312 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2313 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2314 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2315 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2316 ni 0 set (PLet fc rc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2317 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2318 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2319 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2320 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2321 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2322 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2323 ni 0 set (PAlternative ns a as) = niTms 0 set as
2324 ni 0 set (PHidden tm) = ni 0 set tm
2325 ni 0 set (PUnifyLog tm) = ni 0 set tm
2326 ni 0 set (PDisamb _ tm) = ni 0 set tm
2327 ni 0 set (PNoImplicits tm) = ni 0 set tm
2329 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2330 ni i set (PUnquote tm) = ni (i - 1) set tm
2332 ni i set tm = foldr (S.union . ni i set) set (children tm)
2334 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2335 niTms i set [] = set
2336 niTms i set (x : xs) = niTms i (ni i set x) xs
2338 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2339 niTacImp i set _ = set
2341-- Return names which are valid implicits in the given term (type).
2342implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2343implicitNamesIn uvars ist tm
2344 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2347 addImp n = do (imps, fns) <- get
2349 addFn n = do (imps, fns) <- get
2352 ni 0 env (PRef _ _ n@(NS _ _))
2353 | not (n `elem` env)
2354 -- Never implicitly bind if there's a namespace
2356 ni 0 env (PRef _ _ n)
2357 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2358 ni 0 env (PApp _ f@(PRef _ _ n) as)
2359 | n `elem` uvars = do ni 0 env f
2360 mapM_ (ni 0 env . getTm) as
2361 | otherwise = do case lookupTy n (tt_ctxt ist) of
2364 mapM_ (ni 0 env . getTm) as
2365 ni 0 env (PApp _ f as) = do ni 0 env f
2366 mapM_ (ni 0 env . getTm) as
2367 ni 0 env (PAppBind _ f as) = do ni 0 env f
2368 mapM_ (ni 0 env . getTm) as
2369 ni 0 env (PCase _ c os) = do ni 0 env c
2370 -- names in 'os', not counting the names bound in the cases
2371 mapM_ (ni 0 env . snd) os
2374 mapM_ (ni 0 env . fst) os
2376 put (nub imps \\ nub impsfst, fns)
2377 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2378 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2379 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2380 ni 0 env (PLet fc rc n _ ty val sc) = do ni 0 env ty;
2381 ni 0 env val; ni 0 (n:env) sc
2382 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2383 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2384 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2385 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2386 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2389 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2390 ni 0 env (PHidden tm) = ni 0 env tm
2391 ni 0 env (PUnifyLog tm) = ni 0 env tm
2392 ni 0 env (PDisamb _ tm) = ni 0 env tm
2393 ni 0 env (PNoImplicits tm) = ni 0 env tm
2395 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2396 maybe (return ()) (ni i env) ty
2397 ni i env (PUnquote tm) = ni (i - 1) env tm
2399 ni i env tm = mapM_ (ni i env) (children tm)
2401-- Return names which are free in the given term.
2402namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2403namesIn uvars ist tm = nub $ ni 0 [] tm
2405 ni 0 env (PRef _ _ n)
2406 | not (n `elem` env)
2407 = case lookupTy n (tt_ctxt ist) of
2409 _ -> [n | n `elem` (map fst uvars)]
2410 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2411 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2412 ni 0 env (PCase _ c os) = ni 0 env c ++
2413 -- names in 'os', not counting the names bound in the cases
2414 (nub (concatMap (ni 0 env . snd) os)
2415 \\ nub (concatMap (ni 0 env . fst) os))
2416 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2417 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2418 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2419 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2420 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2421 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2422 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2423 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2424 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2425 ni 0 env (PHidden tm) = ni 0 env tm
2426 ni 0 env (PUnifyLog tm) = ni 0 env tm
2427 ni 0 env (PDisamb _ tm) = ni 0 env tm
2428 ni 0 env (PNoImplicits tm) = ni 0 env tm
2430 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2431 ni i env (PUnquote tm) = ni (i - 1) env tm
2433 ni i env tm = concatMap (ni i env) (children tm)
2435 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2438-- Return which of the given names are used in the given term.
2440usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2441usedNamesIn vars ist tm = nub $ ni 0 [] tm
2442 where -- TODO THINK added niTacImp, but is it right?
2443 ni 0 env (PRef _ _ n)
2444 | n `elem` vars && not (n `elem` env)
2445 = case lookupDefExact n (tt_ctxt ist) of
2448 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2449 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2450 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2451 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2452 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2453 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2454 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2455 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2456 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2457 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2458 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2459 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2460 ni 0 env (PHidden tm) = ni 0 env tm
2461 ni 0 env (PUnifyLog tm) = ni 0 env tm
2462 ni 0 env (PDisamb _ tm) = ni 0 env tm
2463 ni 0 env (PNoImplicits tm) = ni 0 env tm
2465 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2466 ni i env (PUnquote tm) = ni (i - 1) env tm
2468 ni i env tm = concatMap (ni i env) (children tm)
2470 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2473-- Return the list of inaccessible (= dotted) positions for a name.
2474getErasureInfo :: IState -> Name -> [Int]
2475getErasureInfo ist n =
2476 case lookupCtxtExact n (idris_optimisation ist) of
2477 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