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)
49import Network.Socket (PortNumber)
52data ElabWhat = ETypes | EDefns | EAll
55-- | Data to pass to recursively called elaborators; e.g. for where blocks,
56-- paramaterised declarations, etc.
58-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
59-- so that we can have mutually recursive elaborators in separate modules without
60-- having to muck about with cyclic modules.
61data ElabInfo = EInfo {
62 params :: [(Name, PTerm)]
63 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
64 , liftname :: Name -> Name
65 , namespace :: [String]
67 , constraintNS :: String -- ^ filename for adding to constraint variables
69 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
70 -- | We may, recursively, collect transformations to do on the rhs,
71 -- e.g. rewriting recursive calls to functions defined by 'with'
72 , rhs_trans :: PTerm -> PTerm
73 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
77toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
79toplevelWith :: String -> ElabInfo
80toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
82eInfoNames :: ElabInfo -> [Name]
83eInfoNames info = map fst (params info) ++ M.keys (inblock info)
85data IOption = IOption {
87 , opt_logcats :: [LogCat] -- ^ List of logging categories.
88 , opt_typecase :: Bool
89 , opt_typeintype :: Bool
90 , opt_coverage :: Bool
91 , opt_showimp :: Bool -- ^ show implicits
92 , opt_errContext :: Bool
95 , opt_nobanner :: Bool
97 , opt_codegen :: Codegen
98 , opt_outputTy :: OutputType
99 , opt_ibcsubdir :: FilePath
100 , opt_importdirs :: [FilePath]
101 , opt_sourcedirs :: [FilePath]
102 , opt_triple :: String
104 , opt_cmdline :: [Opt] -- ^ remember whole command line
105 , opt_origerr :: Bool
106 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
107 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
108 , opt_optimise :: [Optimisation]
109 , opt_printdepth :: Maybe Int
110 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
111 , opt_desugarnats :: Bool
112 , opt_autoimpls :: Bool
113 } deriving (Show, Eq, Generic)
115defaultOpts :: IOption
116defaultOpts = IOption { opt_logLevel = 0
118 , opt_typecase = False
119 , opt_typeintype = False
120 , opt_coverage = True
121 , opt_showimp = False
122 , opt_errContext = False
125 , opt_nobanner = False
127 , opt_codegen = Via IBCFormat "c"
128 , opt_outputTy = Executable
130 , opt_importdirs = []
131 , opt_sourcedirs = []
135 , opt_origerr = False
136 , opt_autoSolve = True
137 , opt_autoImport = []
138 , opt_optimise = defaultOptimise
139 , opt_printdepth = Just 5000
140 , opt_evaltypes = True
141 , opt_desugarnats = False
142 , opt_autoimpls = True
145data PPOption = PPOption {
146 ppopt_impl :: Bool -- ^ whether to show implicits
147 , ppopt_desugarnats :: Bool
148 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
149 , ppopt_depth :: Maybe Int
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
166-- | Pretty printing options with the most verbosity.
167verbosePPOption :: PPOption
168verbosePPOption = PPOption {
170 , ppopt_desugarnats = True
171 , ppopt_pinames = True
172 , ppopt_depth = Nothing
175-- | Get pretty printing options from the big options record.
176ppOption :: IOption -> PPOption
177ppOption opt = PPOption {
178 ppopt_impl = opt_showimp opt
179 , ppopt_pinames = False
180 , ppopt_depth = opt_printdepth opt
181 , ppopt_desugarnats = opt_desugarnats opt
184-- | Get pretty printing options from an idris state record.
185ppOptionIst :: IState -> PPOption
186ppOptionIst = ppOption . idris_options
189-- | The output mode in use
190data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
191 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
195-- | If a function has no totality annotation, what do we assume?
196data DefaultTotality = DefaultCheckingTotal -- ^ Total
197 | DefaultCheckingPartial -- ^ Partial
198 | DefaultCheckingCovering -- ^Total coverage, but may diverge
199 deriving (Show, Eq, Generic)
201-- | Configuration options for interactive editing.
202data InteractiveOpts = InteractiveOpts {
203 interactiveOpts_indentWith :: Int
204 , interactiveOpts_indentClause :: Int
205} deriving (Show, Generic)
207-- | The global state used in the Idris monad
208data IState = IState {
209 tt_ctxt :: Context -- ^ All the currently defined names and their terms
210 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
211 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
212 , idris_implicits :: Ctxt [PArg]
213 , idris_statics :: Ctxt [Bool]
214 , idris_interfaces :: Ctxt InterfaceInfo
215 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
216 , idris_records :: Ctxt RecordInfo
217 , idris_dsls :: Ctxt DSL
218 , idris_optimisation :: Ctxt OptInfo
219 , idris_datatypes :: Ctxt TypeInfo
220 , idris_namehints :: Ctxt [Name]
222 -- | list of lhs/rhs, and a list of missing clauses. These are not
224 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
225 , idris_flags :: Ctxt [FnOpt]
226 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
227 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
229 -- | module documentation is saved in a special MN so the context
230 -- mechanism can be used for disambiguation.
231 , idris_moduledocs :: Ctxt (Docstring DocTerm)
232 , idris_tyinfodata :: Ctxt TIData
233 , idris_fninfo :: Ctxt FnInfo
234 , idris_transforms :: Ctxt [(Term, Term)]
235 , idris_autohints :: Ctxt [Name]
236 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
237 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
238 , idris_totcheckfail :: [(FC, String)]
239 , idris_options :: IOption
241 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
243 -- | The currently defined but not proven metavariables. The Int is
244 -- the number of vars to display as a context, the Maybe Name is its
245 -- top-level function, the [Name] is the list of local variables
246 -- available for proof search and the Bools are whether :p is
247 -- allowed, and whether the variable is definable at all
248 -- (Metavariables are not definable if they are applied in a term
249 -- which still has hole bindings)
250 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
251 , idris_coercions :: [Name]
252 , idris_errRev :: [(Term, Term)]
253 , idris_errReduce :: [Name]
254 , syntax_rules :: SyntaxRules
255 , syntax_keywords :: [String]
256 , imported :: [FilePath] -- ^ The imported modules
257 , idris_scprims :: [(Name, (Int, PrimFn))]
258 , idris_objs :: [(Codegen, FilePath)]
259 , idris_libs :: [(Codegen, String)]
260 , idris_cgflags :: [(Codegen, String)]
261 , idris_hdrs :: [(Codegen, String)]
262 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
263 , proof_list :: [(Name, (Bool, [String]))]
264 , errSpan :: Maybe FC
265 , parserWarnings :: [(FC, Err)]
266 , lastParse :: Maybe Name
267 , indent_stack :: [Int]
268 , brace_stack :: [Maybe Int]
269 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
270 , idris_parsedSpan :: Maybe FC
271 , hide_list :: Ctxt Accessibility
272 , default_access :: Accessibility
273 , default_total :: DefaultTotality
274 , ibc_write :: [IBCWrite]
275 , compiled_so :: Maybe String
276 , idris_dynamic_libs :: [DynamicLib]
277 , idris_language_extensions :: [LanguageExt]
278 , idris_outputmode :: OutputMode
279 , idris_colourRepl :: Bool
280 , idris_colourTheme :: ColourTheme
281 , idris_errorhandlers :: [Name] -- ^ Global error handlers
282 , idris_nameIdx :: (Int, Ctxt (Int, Name))
283 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
284 , module_aliases :: M.Map [T.Text] [T.Text]
285 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
286 , idris_postulates :: S.Set Name
287 , idris_externs :: S.Set (Name, Int)
288 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
290 -- | List of names that were defined in the repl, and can be re-/un-defined
291 , idris_repl_defs :: [Name]
293 -- | Stack of names currently being elaborated, Bool set if it's an
294 -- implementation (implementations appear twice; also as a function name)
295 , elab_stack :: [(Name, Bool)]
298 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
299 , idris_exports :: [Name] -- ^ Functions with ExportList
300 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
301 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
302 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
303 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
304 , idris_ttstats :: M.Map Term (Int, Term)
305 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
306 , idris_interactiveOpts :: InteractiveOpts
309-- Required for parsers library, and therefore trifecta
310instance Show IState where
311 show = const "{internal state}"
313data SizeChange = Smaller | Same | Bigger | Unknown
314 deriving (Show, Eq, Generic)
316deriving instance Binary SizeChange
319type SCGEntry = (Name, [Maybe (Int, SizeChange)])
320type UsageReason = (Name, Int) -- fn_name, its_arg_number
322data CGInfo = CGInfo {
323 calls :: [Name] -- Immediate calls
324 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
326 , usedpos :: [(Int, [UsageReason])]
327 } deriving (Show, Generic)
329deriving instance Binary CGInfo
333primDefs = [ sUN "unsafePerformPrimIO"
334 , sUN "mkLazyForeignPrim"
335 , sUN "mkForeignPrim"
337 , sUN "assert_unreachable"
341-- information that needs writing for the current module's .ibc file
342data IBCWrite = IBCFix FixDecl
347 | IBCImplementation Bool Bool Name Name
354 | IBCImport (Bool, FilePath) -- ^ True = import public
355 | IBCImportDir FilePath
356 | IBCSourceDir FilePath
357 | IBCObj Codegen FilePath
358 | IBCLib Codegen String
359 | IBCCGFlag Codegen String
361 | IBCHeader Codegen String
362 | IBCAccess Name Accessibility
363 | IBCMetaInformation Name MetaInformation
364 | IBCTotal Name Totality
365 | IBCInjective Name Injectivity
367 | IBCFnInfo Name FnInfo
368 | IBCTrans Name (Term, Term)
369 | IBCErrRev (Term, Term)
374 | IBCDef Name -- ^ The main context.
375 | IBCNameHint (Name, Name)
376 | IBCLineApp FilePath Int PTerm
377 | IBCErrorHandler Name
378 | IBCFunctionErrorHandler Name Name Name
380 | IBCExtern (Name, Int)
381 | IBCTotCheckErr FC String
383 | IBCModDocs Name -- ^ The name is the special name used to track module docs
384 | IBCUsage (Name, Int)
386 | IBCAutoHint Name Name
387 | IBCDeprecate Name String
388 | IBCFragile Name String
389 | IBCConstraint FC UConstraint
390 deriving (Show, Generic)
392initialInteractiveOpts :: InteractiveOpts
393initialInteractiveOpts = InteractiveOpts {
394 interactiveOpts_indentWith = 2
395 , interactiveOpts_indentClause = 2
398-- | The initial state for the compiler
400idrisInit = IState initContext S.empty []
401 emptyContext emptyContext emptyContext [] emptyContext
402 emptyContext emptyContext emptyContext emptyContext
403 emptyContext emptyContext emptyContext emptyContext
404 emptyContext emptyContext emptyContext emptyContext
406 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
407 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
408 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
409 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
410 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
413-- | The monad for the main REPL - reading and processing files and
414-- updating global state (hence the IO inner monad).
417-- type Idris = WriterT [Either String (IO ())] (State IState a))
420type Idris = StateT IState (ExceptT Err IO)
422catchError :: Idris a -> (Err -> Idris a) -> Idris a
423catchError = liftCatch catchE
425throwError :: Err -> Idris a
426throwError = Trans.lift . throwE
428-- Commands in the REPL
433data ElabShellCmd = EQED
441 | EDocStr (Either Name Const)
447-- Parsed declarations
449data Fixity = Infixl { prec :: Int }
450 | Infixr { prec :: Int }
451 | InfixN { prec :: Int }
452 | PrefixN { prec :: Int }
453 deriving (Eq, Generic)
455deriving instance Binary Fixity
458instance Show Fixity where
459 show (Infixl i) = "infixl " ++ show i
460 show (Infixr i) = "infixr " ++ show i
461 show (InfixN i) = "infix " ++ show i
462 show (PrefixN i) = "prefix " ++ show i
464data FixDecl = Fix Fixity String
465 deriving (Eq, Generic)
467instance Show FixDecl where
468 show (Fix f s) = show f ++ " " ++ s
471deriving instance Binary FixDecl
474instance Ord FixDecl where
475 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
478data Static = Static | Dynamic
479 deriving (Show, Eq, Ord, Data, Generic, Typeable)
481deriving instance Binary Static
484-- ^ Mark bindings with their explicitness, and laziness
485data Plicity = Imp { pargopts :: [ArgOpt]
488 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
489 , pinsource :: Bool -- ^ Explicitly written in source
492 | Exp { pargopts :: [ArgOpt]
494 , pparam :: Bool -- ^ this is a param (rather than index)
497 | Constraint { pargopts :: [ArgOpt]
501 | TacImp { pargopts :: [ArgOpt]
506 deriving (Show, Eq, Ord, Data, Generic, Typeable)
509deriving instance Binary Plicity
512is_scoped :: Plicity -> Maybe ImplicitInfo
513is_scoped (Imp _ _ _ s _ _) = s
518impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
519-- Machine generated top level implicit
521impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
525forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
526forall_constraint :: Plicity
527forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
530expl = Exp [] Dynamic False RigW
532expl_param = Exp [] Dynamic True RigW
535constraint = Constraint [] Static RigW
537tacimpl :: PTerm -> Plicity
538tacimpl t = TacImp [] Dynamic t RigW
540data FnOpt = Inlinable -- ^ always evaluate when simplifying
541 | TotalFn | PartialFn | CoveringFn
542 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
545 -- | interface dictionary, eval only when a function
546 -- argument, and further evaluation results.
548 | OverlappingDictionary -- ^ Interface dictionary which may overlap
549 | Implicit -- ^ implicit coercion
550 | NoImplicit -- ^ do not apply implicit coercions
551 | CExport String -- ^ export, with a C name
552 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
553 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
554 | ErrorReduce -- ^ unfold definition before showing an error
555 | Reflection -- ^ a reflecting function, compile-time only
556 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
557 | Constructor -- ^ Data constructor type
558 | AutoHint -- ^ use in auto implicit search
559 | PEGenerated -- ^ generated by partial evaluator
560 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
561 deriving (Show, Eq, Generic)
563deriving instance Binary FnOpt
568inlinable :: FnOpts -> Bool
569inlinable = elem Inlinable
571dictionary :: FnOpts -> Bool
572dictionary = elem Dictionary
575-- | Type provider - what to provide
576data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
577 | ProvPostulate t -- ^ goal type must be Type, so only term
578 deriving (Show, Eq, Functor, Generic)
580type ProvideWhat = ProvideWhat' PTerm
582-- | Top-level declarations such as compiler directives, definitions,
583-- datatypes and interfaces.
585 -- | Fixity declaration
586 = PFix FC Fixity [String]
587 -- | Type declaration (last FC is precise name location)
588 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
589 -- | Postulate, second FC is precise name location
590 | PPostulate Bool -- external def if true
591 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
593 | PClauses FC FnOpts Name [PClause' t]
594 -- | Top level constant
596 -- | Data declaration.
597 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
599 | PParams FC [(Name, t)] [PDecl' t]
600 -- | Open block/declaration
601 | POpenInterfaces FC [Name] [PDecl' t]
602 -- | New namespace, where FC is accurate location of the namespace
604 | PNamespace String FC [PDecl' t]
606 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
608 FC -- Record name precise location
609 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
610 [(Name, Docstring (Either Err t))] -- Param Docs
611 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
612 (Maybe (Name, FC)) -- Optional constructor name and location
613 (Docstring (Either Err t)) -- Constructor doc
614 SyntaxInfo -- Constructor SyntaxInfo
616 -- | Interface: arguments are documentation, syntax info, source
617 -- location, constraints, interface name, interface name location,
618 -- parameters, method declarations, optional constructor name
619 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
620 [(Name, t)] -- constraints
621 Name -- interface name
622 FC -- accurate location of interface name
623 [(Name, FC, t)] -- parameters and precise locations
624 [(Name, Docstring (Either Err t))] -- parameter docstrings
625 [(Name, FC)] -- determining parameters and precise locations
626 [PDecl' t] -- declarations
627 (Maybe (Name, FC)) -- implementation constructor name and location
628 (Docstring (Either Err t)) -- implementation constructor docs
630 -- | Implementation declaration: arguments are documentation, syntax
631 -- info, source location, constraints, interface name, parameters, full
632 -- Implementation type, optional explicit name, and definitions
633 | PImplementation (Docstring (Either Err t)) -- Implementation docs
634 [(Name, Docstring (Either Err t))] -- Parameter docs
636 FC [(Name, t)] -- constraints
637 [Name] -- parent dictionaries to search for constraints
641 FC -- precise location of interface
643 [(Name, t)] -- Extra names in scope in the body
644 t -- full Implementation type
645 (Maybe Name) -- explicit name
647 | PDSL Name (DSL' t) -- ^ DSL declaration
648 | PSyntax FC Syntax -- ^ Syntax definition
649 | PMutual FC [PDecl' t] -- ^ Mutual block
650 | PDirective Directive -- ^ Compiler directive.
652 -- | Type provider. The first t is the type, the second is the
653 -- term. The second FC is precise highlighting location.
654 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
656 -- | Source-to-source transformation rule. If bool is True, lhs and
657 -- rhs must be convertible.
658 | PTransform FC Bool t t
660 -- | FC is decl-level, for errors, and Strings represent the
662 | PRunElabDecl FC t [String]
663 deriving (Functor, Generic)
665deriving instance Binary PDecl'
668-- | The set of source directives
669data Directive = DLib Codegen String
670 | DLink Codegen String
671 | DFlag Codegen String
672 | DInclude Codegen String
677 | DSetTotal Name -- assert totality after checking
678 | DAccess Accessibility
679 | DDefault DefaultTotality
681 | DDynamicLibs [String]
682 | DNameHint Name FC [(Name, FC)]
683 | DErrorHandlers Name FC Name FC [(Name, FC)]
684 | DLanguage LanguageExt
685 | DDeprecate Name String
686 | DFragile Name String
687 | DAutoImplicits Bool
691-- | A set of instructions for things that need to happen in IState
692-- after a term elaboration when there's been reflected elaboration.
693data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
694 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
695 | RAddImplementation Name Name
696 | RDatatypeDeclInstrs Name [PArg]
697 -- | Datatype, constructors
698 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
701-- | For elaborator state
702data EState = EState {
703 case_decls :: [(Name, PDecl)]
704 , delayed_elab :: [(Int, Elab' EState ())]
705 , new_tyDecls :: [RDeclInstructions]
706 , highlighting :: [(FC, OutputAnnotation)]
707 , auto_binds :: [Name] -- ^ names bound as auto implicits
708 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
712initEState = EState [] [] [] [] [] []
714type ElabD a = Elab' EState a
716highlightSource :: FC -> OutputAnnotation -> ElabD ()
717highlightSource fc annot =
718 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
720-- | One clause of a top-level definition. Term arguments to constructors are:
722-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
724-- 2. The list of extra 'with' patterns
726-- 3. The right-hand side
728-- 4. The where block (PDecl' t)
730data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
731 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
732 | PClauseR FC [t] t [PDecl' t]
733 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
734 deriving (Functor, Generic)
736deriving instance Binary PClause'
741 -- | Data declaration
742 PDatadecl { d_name :: Name -- ^ The name of the datatype
743 , d_name_fc :: FC -- ^ The precise location of the type constructor name
744 , d_tcon :: t -- ^ Type constructor
745 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
747 -- | "Placeholder" for data whose constructors are defined later
748 | PLaterdecl { d_name :: Name
751 } deriving (Functor, Generic)
753-- | Transform the FCs in a PData and its associated terms. The first
754-- function transforms the general-purpose FCs, and the second
755-- transforms those that are used for semantic source highlighting, so
756-- they can be treated specially.
757mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
758mapPDataFC f g (PDatadecl n nfc tycon ctors) =
759 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
760 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
761 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
762mapPDataFC f g (PLaterdecl n nfc tycon) =
763 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
765deriving instance Binary PData'
768-- Handy to get a free function for applying PTerm -> PTerm functions
769-- across a program, by deriving Functor
771type PDecl = PDecl' PTerm
772type PData = PData' PTerm
773type PClause = PClause' PTerm
775-- | Transform the FCs in a PTerm. The first function transforms the
776-- general-purpose FCs, and the second transforms those that are used
777-- for semantic source highlighting, so they can be treated specially.
778mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
779mapPDeclFC f g (PFix fc fixity ops) =
780 PFix (f fc) fixity ops
781mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
782 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
783mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
784 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
786mapPDeclFC f g (PClauses fc opts n clauses) =
787 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
788mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
789mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
790 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
791mapPDeclFC f g (PParams fc params decls) =
793 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
794 (map (mapPDeclFC f g) decls)
795mapPDeclFC f g (POpenInterfaces fc ifs decls) =
796 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
797mapPDeclFC f g (PNamespace ns fc decls) =
798 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
799mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
800 PRecord doc syn (f fc) opts n (g nfc)
801 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
803 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
804 plic, mapPTermFC f g ty, fdoc))
806 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
809mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
810 PInterface doc syn (f fc)
811 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
812 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
813 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
814 (map (mapPDeclFC f g) body)
815 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
817mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
818 PImplementation doc paramDocs syn (f fc)
819 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
820 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
821 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
822 (mapPTermFC f g implTy)
824 (map (mapPDeclFC f g) body)
825mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
826mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
828 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
829 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
830mapPDeclFC f g (PMutual fc decls) =
831 PMutual (f fc) (map (mapPDeclFC f g) decls)
832mapPDeclFC f g (PDirective d) =
835 DNameHint n nfc ns ->
836 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
837 DErrorHandlers n nfc n' nfc' ns ->
838 DErrorHandlers n (g nfc) n' (g nfc') $
839 map (\(an, anfc) -> (an, g anfc)) ns
840mapPDeclFC f g (PProvider doc syn fc nfc what n) =
841 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
842mapPDeclFC f g (PTransform fc safe l r) =
843 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
844mapPDeclFC f g (PRunElabDecl fc script ns) =
845 PRunElabDecl (f fc) (mapPTermFC f g script) ns
847-- | Get all the names declared in a declaration
848declared :: PDecl -> [Name]
849declared (PFix _ _ _) = []
850declared (PTy _ _ _ _ _ n fc t) = [n]
851declared (PPostulate _ _ _ _ _ _ n t) = [n]
852declared (PClauses _ _ n _) = [] -- not a declaration
853declared (PCAF _ n _) = [n]
854declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
855 where fstt (_, _, a, _, _, _, _) = a
856declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
857declared (PParams _ _ ds) = concatMap declared ds
858declared (POpenInterfaces _ _ ds) = concatMap declared ds
859declared (PNamespace _ _ ds) = concatMap declared ds
860declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
861declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
862declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
866declared (PDSL n _) = [n]
867declared (PSyntax _ _) = []
868declared (PMutual _ ds) = concatMap declared ds
869declared (PDirective _) = []
872-- get the names declared, not counting nested parameter blocks
873tldeclared :: PDecl -> [Name]
874tldeclared (PFix _ _ _) = []
875tldeclared (PTy _ _ _ _ _ n _ t) = [n]
876tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
877tldeclared (PClauses _ _ n _) = [] -- not a declaration
878tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
879tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
880 where fstt (_, _, a, _, _, _, _) = a
881tldeclared (PParams _ _ ds) = []
882tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
883tldeclared (PMutual _ ds) = concatMap tldeclared ds
884tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
885tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
886tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
892defined :: PDecl -> [Name]
893defined (PFix _ _ _) = []
894defined (PTy _ _ _ _ _ n _ t) = []
895defined (PPostulate _ _ _ _ _ _ n t) = []
896defined (PClauses _ _ n _) = [n] -- not a declaration
897defined (PCAF _ n _) = [n]
898defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
899 where fstt (_, _, a, _, _, _, _) = a
900defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
901defined (PParams _ _ ds) = concatMap defined ds
902defined (POpenInterfaces _ _ ds) = concatMap defined ds
903defined (PNamespace _ _ ds) = concatMap defined ds
904defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
905defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
906defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
910defined (PDSL n _) = [n]
911defined (PSyntax _ _) = []
912defined (PMutual _ ds) = concatMap defined ds
913defined (PDirective _) = []
916updateN :: [(Name, Name)] -> Name -> Name
917updateN ns n | Just n' <- lookup n ns = n'
920updateNs :: [(Name, Name)] -> PTerm -> PTerm
922updateNs ns t = mapPT updateRef t
923 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
926-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
928-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
929-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
930-- where updateCNs ns (PClause n l ts r ds)
931-- = PClause (updateN ns n) (fmap (updateNs ns) l)
932-- (map (fmap (updateNs ns)) ts)
933-- (fmap (updateNs ns) r)
934-- (map (updateDNs ns) ds)
940 deriving (Eq, Show, Ord, Data, Typeable, Generic)
942-- | High level language terms
943data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
944 -- high-level language
946 -- ^ A reference to a variable. The FC is its precise
947 -- source location for highlighting. The list of FCs is a
948 -- collection of additional highlighting locations.
949 | PInferRef FC [FC] Name -- ^ A name to be defined later
950 | PPatvar FC Name -- ^ A pattern variable
951 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
952 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
953 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
954 | PTyped PTerm PTerm -- ^ Term with explicit type
955 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
956 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
957 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
958 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
959 | PMatchApp FC Name -- ^ Make an application by type matching
960 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
961 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
962 | PTrue FC PunInfo -- ^ Unit type..?
963 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
964 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
965 -- ^ "rewrite" syntax, with optional rewriting function and
966 -- optional result type
967 | PPair FC [FC] PunInfo PTerm PTerm
968 -- ^ A pair (a, b) and whether it's a product type or a
969 -- pair (solved by elaboration). The list of FCs is its
971 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
972 -- ^ A dependent pair (tm : a ** b) and whether it's a
973 -- sigma type or a pair that inhabits one (solved by
974 -- elaboration). The [FC] is its punctuation.
975 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
976 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
977 | PHidden PTerm -- ^ Irrelevant or hidden pattern
978 | PType FC -- ^ 'Type' type
979 | PUniverse FC Universe -- ^ Some universe
980 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
981 | PConstant FC Const -- ^ Builtin types
982 | Placeholder -- ^ Underscore
983 | PDoBlock [PDo] -- ^ Do notation
984 | PIdiom FC PTerm -- ^ Idiom brackets
985 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
986 | PProof [PTactic] -- ^ Proof script
987 | PTactics [PTactic] -- ^ As PProof, but no auto solving
988 | PElabError Err -- ^ Error to report on elaboration
989 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
990 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
991 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
992 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
993 | PNoImplicits PTerm -- ^ never run implicit converions on the term
994 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
995 | PUnquote PTerm -- ^ ~Term
996 | PQuoteName Name Bool FC
997 -- ^ `{n} where the FC is the precise highlighting for
998 -- the name in particular. If the Bool is False, then
999 -- it's `{{n}} and the name won't be resolved.
1000 | PRunElab FC PTerm [String]
1001 -- ^ %runElab tm - New-style proof script. Args are
1002 -- location, script, enclosing namespace.
1003 | PConstSugar FC PTerm
1004 -- ^ A desugared constant. The FC is a precise source
1005 -- location that will be used to highlight it later.
1006 deriving (Eq, Ord, Data, Typeable, Generic)
1008data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1011 deriving (Eq, Ord, Data, Generic, Typeable)
1013-- | Transform the FCs in a PTerm. The first function transforms the
1014-- general-purpose FCs, and the second transforms those that are used
1015-- for semantic source highlighting, so they can be treated specially.
1016mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1017mapPTermFC f g (PQuote q) = PQuote q
1018mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1019mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1020mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1021mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1022mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1023mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1024mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1025mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1026mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1027mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1028mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1029mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1030mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1031mapPTermFC 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)
1032mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1033mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1034mapPTermFC 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)
1035mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1036mapPTermFC 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)
1037mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1038mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1039mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1040mapPTermFC f g (PType fc) = PType (f fc)
1041mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1042mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1043mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1044mapPTermFC f g Placeholder = Placeholder
1045mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1046 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1047 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1048 mapPDoFC (DoBindP fc t1 t2 alts) =
1049 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1050 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1051 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1052 mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)
1053mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1054mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1055mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1056mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1057mapPTermFC f g (PElabError err) = PElabError err
1058mapPTermFC f g PImpossible = PImpossible
1059mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1060mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1061mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1062mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1063mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1064mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1065mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1066mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1067mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1070dg instance Binary PTerm
1073mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1074mapPT f t = f (mpt t) where
1075 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1076 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1077 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1078 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1079 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1080 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1081 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1082 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1083 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1084 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1085 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1086 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1087 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1088 mpt (PHidden t) = PHidden (mapPT f t)
1089 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1090 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1091 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1092 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1093 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1094 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1095 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1099data PTactic' t = Intro [Name] | Intros | Focus Name
1100 | Refine Name [Bool] | Rewrite t | DoUnify
1107 | LetTac Name t | LetTacTy Name t t
1108 | Exact t | Compute | Trivial | TCImplementation
1109 | ProofSearch Bool Bool Int (Maybe Name)
1110 [Name] -- allowed local names
1112 -- ^ the bool is whether to search recursively
1115 | ProofState | ProofTerm | Undo
1116 | Try (PTactic' t) (PTactic' t)
1117 | TSeq (PTactic' t) (PTactic' t)
1118 | ApplyTactic t -- see Language.Reflection module
1122 | GoalType String (PTactic' t)
1125 | TDocStr (Either Name Const)
1128 | TFail [ErrorReportPart]
1131 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1133deriving instance Binary PTactic'
1135instance Sized a => Sized (PTactic' a) where
1136 size (Intro nms) = 1 + size nms
1138 size (Focus nm) = 1 + size nm
1139 size (Refine nm bs) = 1 + size nm + length bs
1140 size (Rewrite t) = 1 + size t
1141 size (Induction t) = 1 + size t
1142 size (LetTac nm t) = 1 + size nm + size t
1143 size (Exact t) = 1 + size t
1151 size (Try l r) = 1 + size l + size r
1152 size (TSeq l r) = 1 + size l + size r
1153 size (ApplyTactic t) = 1 + size t
1154 size (Reflect t) = 1 + size t
1155 size (Fill t) = 1 + size t
1159 size (TFail ts) = 1 + size ts
1162 size (CaseTac x) = 1 + size x
1163 size (Equiv t) = 1 + size t
1164 size (Claim x y) = 1 + size x + size y
1166 size (MatchRefine x) = 1 + size x
1167 size (LetTacTy x y z) = 1 + size x + size y + size z
1168 size TCImplementation = 1
1170type PTactic = PTactic' PTerm
1172data PDo' t = DoExp FC t
1173 | DoBind FC Name FC t -- ^ second FC is precise name location
1174 | DoBindP FC t t [(t,t)]
1175 | DoLet FC Name FC t t -- ^ second FC is precise name location
1177 | DoRewrite FC t -- rewrite in do block
1178 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1180deriving instance Binary PDo'
1183instance Sized a => Sized (PDo' a) where
1184 size (DoExp fc t) = 1 + size fc + size t
1185 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1186 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1187 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1188 size (DoLetP fc l r) = 1 + size fc + size l + size r
1189 size (DoRewrite fc h) = 1 + size fc + size h
1191type PDo = PDo' PTerm
1193-- The priority gives a hint as to elaboration order. Best to elaborate
1194-- things early which will help give a more concrete type to other
1195-- variables, e.g. a before (interpTy a).
1197data PArg' t = PImp { priority :: Int
1198 , machine_inf :: Bool -- ^ true if the machine inferred it
1199 , argopts :: [ArgOpt]
1203 | PExp { priority :: Int
1204 , argopts :: [ArgOpt]
1208 | PConstraint { priority :: Int
1209 , argopts :: [ArgOpt]
1213 | PTacImplicit { priority :: Int
1214 , argopts :: [ArgOpt]
1219 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1221data ArgOpt = AlwaysShow
1225 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1227instance Sized a => Sized (PArg' a) where
1228 size (PImp p _ l nm trm) = 1 + size nm + size trm
1229 size (PExp p l nm trm) = 1 + size nm + size trm
1230 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1231 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1234deriving instance Binary PArg'
1237pimp n t mach = PImp 1 mach [] n t
1238pexp t = PExp 1 [] (sMN 0 "arg") t
1239pconst t = PConstraint 1 [] (sMN 0 "carg") t
1240ptacimp n s t = PTacImplicit 2 [] n s t
1242type PArg = PArg' PTerm
1244-- | Get the highest FC in a term, if one exists
1245highestFC :: PTerm -> Maybe FC
1246highestFC (PQuote _) = Nothing
1247highestFC (PRef fc _ _) = Just fc
1248highestFC (PInferRef fc _ _) = Just fc
1249highestFC (PPatvar fc _) = Just fc
1250highestFC (PLam fc _ _ _ _) = Just fc
1251highestFC (PPi _ _ _ _ _) = Nothing
1252highestFC (PLet fc _ _ _ _ _) = Just fc
1253highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1254highestFC (PApp fc _ _) = Just fc
1255highestFC (PAppBind fc _ _) = Just fc
1256highestFC (PMatchApp fc _) = Just fc
1257highestFC (PCase fc _ _) = Just fc
1258highestFC (PIfThenElse fc _ _ _) = Just fc
1259highestFC (PTrue fc _) = Just fc
1260highestFC (PResolveTC fc) = Just fc
1261highestFC (PRewrite fc _ _ _ _) = Just fc
1262highestFC (PPair fc _ _ _ _) = Just fc
1263highestFC (PDPair fc _ _ _ _ _) = Just fc
1264highestFC (PAs fc _ _) = Just fc
1265highestFC (PAlternative _ _ args) =
1266 case mapMaybe highestFC args of
1269highestFC (PHidden _) = Nothing
1270highestFC (PType fc) = Just fc
1271highestFC (PUniverse _ _) = Nothing
1272highestFC (PGoal fc _ _ _) = Just fc
1273highestFC (PConstant fc _) = Just fc
1274highestFC Placeholder = Nothing
1275highestFC (PDoBlock lines) =
1276 case map getDoFC lines of
1280 getDoFC (DoExp fc t) = fc
1281 getDoFC (DoBind fc nm nfc t) = fc
1282 getDoFC (DoBindP fc l r alts) = fc
1283 getDoFC (DoLet fc nm nfc l r) = fc
1284 getDoFC (DoLetP fc l r) = fc
1285 getDoFC (DoRewrite fc h) = fc
1287highestFC (PIdiom fc _) = Just fc
1288highestFC (PMetavar fc _) = Just fc
1289highestFC (PProof _) = Nothing
1290highestFC (PTactics _) = Nothing
1291highestFC (PElabError _) = Nothing
1292highestFC PImpossible = Nothing
1293highestFC (PCoerced tm) = highestFC tm
1294highestFC (PDisamb _ opts) = highestFC opts
1295highestFC (PUnifyLog tm) = highestFC tm
1296highestFC (PNoImplicits tm) = highestFC tm
1297highestFC (PQuasiquote _ _) = Nothing
1298highestFC (PUnquote tm) = highestFC tm
1299highestFC (PQuoteName _ _ fc) = Just fc
1300highestFC (PRunElab fc _ _) = Just fc
1301highestFC (PConstSugar fc _) = Just fc
1302highestFC (PAppImpl t _) = highestFC t
1306data InterfaceInfo = CI {
1307 implementationCtorName :: Name
1308 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1309 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1310 , interface_default_super_interfaces :: [PDecl]
1311 , interface_impparams :: [Name]
1312 , interface_params :: [Name]
1313 , interface_constraints :: [PTerm]
1314 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1315 , interface_determiners :: [Int]
1316 } deriving (Show, Generic)
1318deriving instance Binary InterfaceInfo
1322data RecordInfo = RI {
1323 record_parameters :: [(Name,PTerm)]
1324 , record_constructor :: Name
1325 , record_projections :: [Name]
1326 } deriving (Show, Generic)
1328-- Type inference data
1330data TIData = TIPartial -- ^ a function with a partially defined type
1331 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1332 deriving (Show, Generic)
1334-- | Miscellaneous information about functions
1335data FnInfo = FnInfo { fn_params :: [Int] }
1336 deriving (Show, Generic)
1338deriving instance Binary FnInfo
1341data OptInfo = Optimise {
1342 inaccessible :: [(Int,Name)] -- includes names for error reporting
1343 , detaggable :: Bool
1344 , forceable :: [Int] -- argument positions which are forced by other values
1345 } deriving (Show, Generic)
1347deriving instance Binary OptInfo
1350-- | Syntactic sugar info
1355 , dsl_var :: Maybe t
1356 , index_first :: Maybe t
1357 , index_next :: Maybe t
1358 , dsl_lambda :: Maybe t
1359 , dsl_let :: Maybe t
1361 } deriving (Show, Functor, Generic)
1363deriving instance Binary DSL'
1366type DSL = DSL' PTerm
1368data SynContext = PatternSyntax
1371 deriving (Show, Generic)
1373deriving instance Binary SynContext
1376data Syntax = Rule [SSymbol] PTerm SynContext
1377 | DeclRule [SSymbol] [PDecl]
1378 deriving (Show, Generic)
1380syntaxNames :: Syntax -> [Name]
1381syntaxNames (Rule syms _ _) = mapMaybe ename syms
1382 where ename (Keyword n) = Just n
1384syntaxNames (DeclRule syms _) = mapMaybe ename syms
1385 where ename (Keyword n) = Just n
1388syntaxSymbols :: Syntax -> [SSymbol]
1389syntaxSymbols (Rule ss _ _) = ss
1390syntaxSymbols (DeclRule ss _) = ss
1392deriving instance Binary Syntax
1395data SSymbol = Keyword Name
1400 deriving (Show, Eq, Generic)
1404deriving instance Binary SSymbol
1407newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1410emptySyntaxRules :: SyntaxRules
1411emptySyntaxRules = SyntaxRules []
1413updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1414updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1416 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1421 ruleSort (s1:ss1) (s2:ss2) =
1422 case symCompare s1 s2 of
1423 EQ -> ruleSort ss1 ss2
1426 -- Better than creating Ord implementation for SSymbol since
1427 -- in general this ordering does not really make sense.
1428 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1429 symCompare (Keyword _) _ = LT
1430 symCompare (Symbol _) (Keyword _) = GT
1431 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1432 symCompare (Symbol _) _ = LT
1433 symCompare (Binding _) (Keyword _) = GT
1434 symCompare (Binding _) (Symbol _) = GT
1435 symCompare (Binding b1) (Binding b2) = compare b1 b2
1436 symCompare (Binding _) _ = LT
1437 symCompare (Expr _) (Keyword _) = GT
1438 symCompare (Expr _) (Symbol _) = GT
1439 symCompare (Expr _) (Binding _) = GT
1440 symCompare (Expr e1) (Expr e2) = compare e1 e2
1441 symCompare (Expr _) _ = LT
1442 symCompare (SimpleExpr _) (Keyword _) = GT
1443 symCompare (SimpleExpr _) (Symbol _) = GT
1444 symCompare (SimpleExpr _) (Binding _) = GT
1445 symCompare (SimpleExpr _) (Expr _) = GT
1446 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1448initDSL = DSL (PRef f [] (sUN ">>="))
1449 (PRef f [] (sUN "<*>"))
1450 (PRef f [] (sUN "pure"))
1457 where f = fileFC "(builtin)"
1459data Using = UImplicit Name PTerm
1460 | UConstraint Name [Name]
1461 deriving (Show, Eq, Data, Generic, Typeable)
1463deriving instance Binary Using
1466data SyntaxInfo = Syn {
1468 , syn_params :: [(Name, PTerm)]
1469 , syn_namespace :: [String]
1471 , imp_methods :: [Name]
1472 -- ^ interface methods. When expanding implicits, these should be
1473 -- expanded even under binders
1474 , decoration :: Name -> Name
1476 , implicitAllowed :: Bool
1477 , constraintAllowed :: Bool
1478 , maxline :: Maybe Int
1479 , mut_nesting :: Int
1481 , syn_in_quasiquote :: Int
1482 , syn_toplevel :: Bool
1483 , withAppAllowed :: Bool
1484 } deriving (Show, Generic)
1486deriving instance Binary SyntaxInfo
1489defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1491expandNS :: SyntaxInfo -> Name -> Name
1492expandNS syn n@(NS _ _) = n
1493expandNS syn n = case syn_namespace syn of
1498-- For inferring types of things
1500bi = fileFC "builtin"
1501primfc = fileFC "(primitive)"
1503inferTy = sMN 0 "__Infer"
1504inferCon = sMN 0 "__infer"
1505inferDecl = PDatadecl inferTy primfc
1507 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1508 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1509 (PRef bi [] inferTy)), bi, [])]
1512infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1513infP = P (TCon 6 0) inferTy (TType (UVal 0))
1515getInferTerm, getInferType :: Term -> Term
1516getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1517getInferTerm (App _ (App _ _ _) tm) = tm
1518getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1520getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1521 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1522 toTy (PVar _ t) = PVTy t
1524getInferType (App _ (App _ _ ty) _) = ty
1528-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1530primNames = [inferTy, inferCon]
1533unitCon = sUN "MkUnit"
1535falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1536 "The empty type, also known as the trivially false proposition." ++
1538 "Use `void` or `absurd` to prove anything if you have a variable " ++
1539 "of type `Void` in scope."
1542pairTy = sNS (sUN "Pair") ["Builtins"]
1543pairCon = sNS (sUN "MkPair") ["Builtins"]
1545upairTy = sNS (sUN "UPair") ["Builtins"]
1546upairCon = sNS (sUN "MkUPair") ["Builtins"]
1550eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1551 "The propositional equality type. A proof that `x` = `y`." ++
1553 "To use such a proof, pattern-match on it, and the two equal things will " ++
1554 "then need to be the _same_ pattern." ++
1556 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1557 "is possible to state equalities between values of potentially different " ++
1558 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1560 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1562eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1563 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1565 [(reflDoc, reflParamDoc,
1566 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1567 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1568 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1569 pimp (n "B") Placeholder False,
1570 pexp (PRef bi [] (n "x")),
1571 pexp (PRef bi [] (n "x"))])), bi, [])]
1573 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1574 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1575 "shown that both sides are in fact equal."
1576 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1577 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1579eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1580 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1586-- | The special name to be used in the module documentation context -
1587-- not for use in the main definition context. The namespace around it
1588-- will determine the module to which the docs adhere.
1590modDocName = sMN 0 "ModuleDocs"
1592-- Defined in builtins.idr
1593sigmaTy = sNS (sUN "DPair") ["Builtins"]
1594sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1596piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1597piBind = piBindp expl
1599piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1601piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1604-- Pretty-printing declarations and terms
1606-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1607-- could interfere with interactive editing, which calls "show".
1609instance Show PTerm where
1610 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1612instance Show PDecl where
1613 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1615instance Show PClause where
1616 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1618instance Show PData where
1619 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1621instance Pretty PTerm OutputAnnotation where
1622 pretty = prettyImp defaultPPOption
1624-- | Colourise annotations according to an Idris state. It ignores the
1625-- names in the annotation, as there's no good way to show extended
1626-- information on a terminal.
1627annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1628annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1629annotationColour ist (AnnConst c) =
1630 let theme = idris_colourTheme ist
1631 in Just $ if constIsType c
1632 then typeColour theme
1633 else dataColour theme
1634annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1635annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1636annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1637annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1638annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1639annotationColour ist (AnnName n _ _ _) =
1640 let ctxt = tt_ctxt ist
1641 theme = idris_colourTheme ist
1643 _ | isDConName n ctxt -> Just $ dataColour theme
1644 _ | isFnName n ctxt -> Just $ functionColour theme
1645 _ | isTConName n ctxt -> Just $ typeColour theme
1646 _ | isPostulateName n ist -> Just $ postulateColour theme
1647 _ | otherwise -> Nothing -- don't colourise unknown names
1648annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1649 where colour BoldText = IdrisColour Nothing True False True False
1650 colour UnderlineText = IdrisColour Nothing True True False False
1651 colour ItalicText = IdrisColour Nothing True False False True
1652annotationColour ist _ = Nothing
1655-- | Colourise annotations according to an Idris state. It ignores the
1656-- names in the annotation, as there's no good way to show extended
1657-- information on a terminal. Note that strings produced this way will
1658-- not be coloured on Windows, so the use of the colour rendering
1659-- functions in Idris.Output is to be preferred.
1660consoleDecorate :: IState -> OutputAnnotation -> String -> String
1661consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1663isPostulateName :: Name -> IState -> Bool
1664isPostulateName n ist = S.member n (idris_postulates ist)
1666-- | Pretty-print a high-level closed Idris term with no information
1667-- about precedence/associativity
1668prettyImp :: PPOption -- ^ pretty printing options
1669 -> PTerm -- ^ the term to pretty-print
1670 -> Doc OutputAnnotation
1671prettyImp impl = pprintPTerm impl [] [] []
1673-- | Serialise something to base64 using its Binary implementation.
1675-- | Do the right thing for rendering a term in an IState
1676prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1677prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1679-- | Pretty-print a high-level Idris term in some bindings context
1681pprintPTerm :: PPOption -- ^ pretty printing options
1682 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1683 -> [Name] -- ^ names to always show in pi, even if not used
1684 -> [FixDecl] -- ^ Fixity declarations
1685 -> PTerm -- ^ the term to pretty-print
1686 -> Doc OutputAnnotation
1687pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
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 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1704 prettySe (decD d) startPrec ((n, False):bnd) sc'
1706 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1707 getLamNames acc sc = (reverse acc, sc)
1709 prettyBindingsOf [] t = text ""
1710 prettyBindingsOf [n] t = prettyBindingOf n t
1711 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1712 prettyBindingsOf ns t
1713 prettySe d p bnd (PLet fc n nfc ty v sc) =
1714 depth d . bracket p startPrec . group . align $
1715 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1716 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1717 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1719 depth d . bracket p startPrec . group $
1720 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1721 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1723 depth d . bracket p startPrec . group $
1724 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1725 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1726 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1727 || ppopt_pinames ppo && uname n =
1728 depth d . bracket p startPrec . group $
1729 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1730 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1732 depth d . bracket p startPrec . group $
1733 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1734 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1736 uname (UN n) = case str n of
1743 Static -> text "%static" <> space
1745 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1747 depth d . bracket p startPrec $
1748 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1749 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1750 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1751 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1753 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1754 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1755 showRig _ n = prettyBindingOf n True
1757 isPi (PPi (Exp{}) _ _ _ _) = True
1758 isPi (PPi _ _ _ _ sc) = isPi sc
1763 Static -> text "%static" <> space
1765 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1766 depth d . bracket p startPrec $
1767 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1768 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1769 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1770 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1771 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1772 depth d . bracket p startPrec $
1773 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1774 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1775 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1776 | basename neg == sUN "negate" =
1777 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1778 -- This case preserves the behavior of the former constructor PEq.
1779 -- It should be removed if feasible when the pretty-printing of infix
1780 -- operators in general is improved.
1781 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1782 | n == eqTy, ppopt_impl ppo =
1783 depth d . bracket p eqPrec $
1784 enclose lparen rparen eq <+>
1785 align (group (vsep (map (prettyArgS (decD d) bnd)
1788 depth d . bracket p eqPrec . align . group $
1789 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1790 where eq = annName eqTy (text "=")
1792 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1793 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1794 | UN nm <- basename f
1795 , not (ppopt_impl ppo) && null (getShowArgs args) =
1796 prettyName True (ppopt_impl ppo) bnd f
1797 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1798 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1799 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1800 | UN nm <- basename op
1802 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1803 case getShowArgs args of
1805 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1806 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1807 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1808 (l@(PExp{}) : r@(PExp{}) : rest) ->
1809 depth d . bracket p funcAppPrec $
1810 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1811 align (group (vsep (map (prettyArgS d bnd) rest)))
1812 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1813 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1814 f = getFixity (opStr op)
1816 Nothing -> funcAppPrec + 1
1817 Just (Infixl p') -> p'
1818 Just f' -> prec f' + 1
1820 Nothing -> funcAppPrec + 1
1821 Just (Infixr p') -> p'
1822 Just f' -> prec f' + 1
1823 inFix l r = align . group $
1824 (prettySe (decD d) left bnd l <+> opName False) <$>
1825 group (prettySe (decD d) right bnd r)
1826 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1827 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1828 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1829 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1830 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1831 let args = getShowArgs as
1832 fp = prettySe (decD d) (startPrec + 1) bnd f
1833 shownArgs = if ppopt_impl ppo then as else args
1835 depth d . bracket p funcAppPrec . group $
1838 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1839 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1840 prettySe d p bnd (PCase _ scr cases) =
1841 bracket p funcAppPrec $
1842 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1843 depth d (indent 2 (vsep (map ppcase cases)))
1845 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1846 ([(n, False) | n <- vars l] ++ bnd)
1847 in nest nestingSize $
1848 prettyCase l <+> text "=>" <+> prettyCase r
1849 -- Warning: this is a bit of a hack. At this stage, we don't have the
1850 -- global context, so we can't determine which names are constructors,
1851 -- which are types, and which are pattern variables on the LHS of the
1852 -- case pattern. We use the heuristic that names without a namespace
1853 -- are patvars, because right now case blocks in PTerms are always
1854 -- delaborated from TT before being sent to the pretty-printer. If they
1855 -- start getting printed directly, THIS WILL BREAK.
1856 -- Potential solution: add a list of known patvars to the cases in
1857 -- PCase, and have the delaborator fill it out, kind of like the pun
1858 -- disambiguation on PDPair.
1859 vars tm = filter noNS (allNamesIn tm)
1860 noNS (NS _ _) = False
1863 prettySe d p bnd (PIfThenElse _ c t f) =
1864 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1865 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1866 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1867 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1869 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1870 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1871 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1872 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1873 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1874 prettySe d p bnd (PRewrite _ by l r _) =
1875 depth d . bracket p startPrec $
1876 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1879 Just fn -> text "using" <+>
1880 prettyName True (ppopt_impl ppo) bnd fn) <+>
1881 text "in" <+> prettySe (decD d) startPrec bnd r
1882 prettySe d p bnd (PTyped l r) =
1883 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1884 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1885 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1886 align . group . vsep . punctuate (ann comma) $
1887 map (prettySe (decD d) startPrec bnd) elts
1888 where ann = case pun of
1890 IsType -> annName pairTy
1891 IsTerm -> annName pairCon
1892 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1893 | Just elts <- dPairElts dpair
1894 = depth d . enclose (annotated lparen) (annotated rparen) .
1895 align . group . vsep . punctuate (space <> annotated (text "**")) $
1901 annotated (text "**") <+>
1902 prettySe (decD d) startPrec (addBinding bnd) r <>
1904 where annotated = case pun of
1905 IsType -> annName sigmaTy
1906 IsTerm -> annName sigmaCon
1909 (left, addBinding) = case (l, pun) of
1910 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1911 _ -> (prettySe (decD d) startPrec bnd l, id)
1914 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1915 ppElts ((PRef _ _ n, t):rs) bs
1917 = (bindingOf n False <+> colon <+>
1918 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1919 ppElts ((l, t):rs) bs
1920 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1921 prettySe d p bnd (PAlternative ns a as) =
1922 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1925 foldr ((\ l r -> l <+> text "," <+> r) .
1926 depth d . prettySe (decD d) startPrec bnd)
1928 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1929 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1930 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1931 -- XXX: add pretty for tactics
1932 prettySe d p bnd (PProof ts) =
1933 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1934 prettySe d p bnd (PTactics ts) =
1935 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1936 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1937 prettySe d p bnd PImpossible = kwd "impossible"
1938 prettySe d p bnd Placeholder = text "_"
1939 prettySe d p bnd (PDoBlock dos) =
1940 bracket p startPrec $
1941 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1942 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1943 ppdo bnd (DoBind _ bn _ tm : dos) =
1944 (prettyBindingOf bn False <+> text "<-" <+>
1945 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1946 ppdo ((bn, False):bnd) dos
1947 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1948 text "no pretty printer for pattern-matching do binding" :
1950 ppdo bnd (DoLet _ ln _ ty v : dos) =
1951 (kwd "let" <+> prettyBindingOf ln False <+>
1952 (if ty /= Placeholder
1953 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1955 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1956 ppdo ((ln, False):bnd) dos
1957 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1958 text "no pretty printer for pattern-matching do binding" :
1960 ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab
1961 text "no pretty printer for pattern-matching do binding" :
1964 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1965 prettySe d p bnd (PElabError s) = pretty s
1966 -- Quasiquote pprinting ignores bound vars
1967 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1968 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1969 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1970 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1971 where start = if res then "`{" else "`{{"
1972 end = if res then "}" else "}}"
1973 prettySe d p bnd (PRunElab _ tm _) =
1974 bracket p funcAppPrec . group . align . hang 2 $
1976 prettySe (decD d) funcAppPrec bnd tm
1977 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1978 prettySe d p bnd _ = text "missing pretty-printer for term"
1980 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1981 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1982 where display (UN n) = T.unpack n
1983 display (MN _ n) = T.unpack n
1984 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1985 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1988 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1989 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1990 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1991 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1993 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1994 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1995 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1996 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1998 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1999 annName n = annotate (AnnName n Nothing Nothing Nothing)
2001 opStr :: Name -> String
2002 opStr (NS n _) = opStr n
2003 opStr (UN n) = T.unpack n
2005 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2006 slist' (Just d) _ _ _ | d <= 0 = Nothing
2008 | containsHole e = Nothing
2009 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2010 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2011 slist' d p bnd (PRef _ _ nil)
2012 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2013 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2014 | nsroot cons == sUN "::",
2015 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2017 Just tl' <- slist' (decD d) p bnd tl
2018 = Just (prettySe d startPrec bnd hd : tl')
2020 isImp (PImp {}) = True
2022 slist' _ _ _ tm = Nothing
2024 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2026 [] -> annotate (AnnData "" "") $ text "[]"
2027 [x] -> enclose left right . group $ x
2028 xs -> enclose left right .
2029 align . group . vsep .
2030 punctuate comma $ xs
2031 where left = (annotate (AnnData "" "") (text "["))
2032 right = (annotate (AnnData "" "") (text "]"))
2033 comma = (annotate (AnnData "" "") (text ","))
2034 slist _ _ _ _ = Nothing
2036 pairElts :: PTerm -> Maybe [PTerm]
2037 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2038 | otherwise = Just [x, y]
2039 pairElts _ = Nothing
2041 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2042 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2043 | otherwise = Just [(l, t), (Placeholder, r)]
2044 dPairElts _ = Nothing
2046 natns = "Prelude.Nat."
2048 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2050 | ppopt_desugarnats ppo = Nothing
2051 | otherwise = snat' d p e
2053 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2054 snat' (Just x) _ _ | x <= 0 = Nothing
2055 snat' d p (PRef _ _ z)
2056 | show z == (natns++"Z") || show z == "Z" = Just 0
2057 snat' d p (PApp _ s [PExp {getTm=n}])
2058 | show s == (natns++"S") || show s == "S",
2059 Just n' <- snat' (decD d) p n
2061 snat' _ _ _ = Nothing
2063 bracket outer inner doc
2064 | outer > inner = lparen <> doc <> rparen
2067 ellipsis = text "..."
2070 depth (Just d) = if d <= 0 then const ellipsis else id
2072 decD = fmap (\x -> x - 1)
2074 kwd = annotate AnnKeyword . text
2076 fixities :: M.Map String Fixity
2077 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2079 getFixity :: String -> Maybe Fixity
2080 getFixity = flip M.lookup fixities
2082-- | Strip away namespace information
2083basename :: Name -> Name
2084basename (NS n _) = basename n
2087-- | Determine whether a name was the one inserted for a hole or guess
2088-- by the delaborator
2089isHoleName :: Name -> Bool
2090isHoleName (UN n) = n == T.pack "[__]"
2093-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2094containsHole :: PTerm -> Bool
2095containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2097-- | Pretty-printer helper for names that attaches the correct annotations
2098prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2099 -> Bool -- ^ whether to show namespaces
2100 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2101 -> Name -- ^ the name to pprint
2102 -> Doc OutputAnnotation
2103prettyName infixParen showNS bnd n
2104 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2105 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2106 | (UN n') <- n, T.unpack n' == "_" = text "_"
2107 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2108 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2109 where fullName = text nameSpace <> parenthesise (text (baseName n))
2110 baseName (UN n) = T.unpack n
2111 baseName (NS n ns) = baseName n
2112 baseName (MN i s) = T.unpack s
2113 baseName other = show other
2114 nameSpace = case n of
2115 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2117 isInfix = case baseName n of
2119 (c : _) -> not (isAlpha c)
2120 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2123showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2124showCImp ppo (PClause _ n l ws r w)
2125 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2126 <+> text "where" <+> text (show w)
2129 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2130showCImp ppo (PWith _ n l ws r pn w)
2131 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2132 <+> braces (text (show w))
2135 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2138showDImp :: PPOption -> PData -> Doc OutputAnnotation
2139showDImp ppo (PDatadecl n nfc ty cons)
2140 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2141 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2143showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2144showDecls o ds = vsep (map (showDeclImp o) ds)
2146showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2147showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2148showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2149 indent 2 (vsep (map (showCImp o) cs))
2150showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2151showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2152showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2153showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2154showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2155showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2156 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2157showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2158 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2159showDeclImp _ _ = text "..."
2160-- showDeclImp (PImport o) = "import " ++ o
2162getImps :: [PArg] -> [(Name, PTerm)]
2164getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2165getImps (_ : xs) = getImps xs
2167getExps :: [PArg] -> [PTerm]
2169getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2170getExps (_ : xs) = getExps xs
2172getShowArgs :: [PArg] -> [PArg]
2174getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2175getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2176 | PImp _ _ _ _ tm <- e
2177 , containsHole tm = e : getShowArgs xs
2178getShowArgs (_ : xs) = getShowArgs xs
2180getConsts :: [PArg] -> [PTerm]
2182getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2183getConsts (_ : xs) = getConsts xs
2185getAll :: [PArg] -> [PTerm]
2190showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2191 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2192 -> PPOption -- ^ pretty printing options
2193 -> Bool -- ^ whether to colourise
2194 -> Name -- ^ the term to show
2196showName ist bnd ppo colour n = case ist of
2197 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2198 Nothing -> showbasic n
2199 where name = if ppopt_impl ppo then show n else showbasic n
2200 showbasic n@(UN _) = showCG n
2201 showbasic (MN i s) = str s
2202 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2203 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 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
2353 notCAF (PExp _ _ _ _ : _) = True
2354 notCAF (_ : xs) = notCAF xs
2356 notHidden (n, _) = case getAccessibility n of
2362 = case lookupDefAccExact n False (tt_ctxt ist) of
2366 ni 0 env (PRef _ _ n@(NS _ _))
2367 | not (n `elem` env)
2368 -- Never implicitly bind if there's a namespace
2370 ni 0 env (PRef _ _ n)
2371 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2372 ni 0 env (PApp _ f@(PRef _ _ n) as)
2373 | n `elem` uvars = do ni 0 env f
2374 mapM_ (ni 0 env . getTm) as
2375 | otherwise = do case lookupTy n (tt_ctxt ist) of
2378 mapM_ (ni 0 env . getTm) as
2379 ni 0 env (PApp _ f as) = do ni 0 env f
2380 mapM_ (ni 0 env . getTm) as
2381 ni 0 env (PAppBind _ f as) = do ni 0 env f
2382 mapM_ (ni 0 env . getTm) as
2383 ni 0 env (PCase _ c os) = do ni 0 env c
2384 -- names in 'os', not counting the names bound in the cases
2385 mapM_ (ni 0 env . snd) os
2388 mapM_ (ni 0 env . fst) os
2390 put (nub imps \\ nub impsfst, fns)
2391 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2392 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2393 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2394 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2395 ni 0 env val; ni 0 (n:env) sc
2396 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2397 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2398 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2399 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2400 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2403 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2404 ni 0 env (PHidden tm) = ni 0 env tm
2405 ni 0 env (PUnifyLog tm) = ni 0 env tm
2406 ni 0 env (PDisamb _ tm) = ni 0 env tm
2407 ni 0 env (PNoImplicits tm) = ni 0 env tm
2409 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2410 maybe (return ()) (ni i env) ty
2411 ni i env (PUnquote tm) = ni (i - 1) env tm
2413 ni i env tm = mapM_ (ni i env) (children tm)
2415-- Return names which are free in the given term.
2416namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2417namesIn uvars ist tm = nub $ ni 0 [] tm
2419 ni 0 env (PRef _ _ n)
2420 | not (n `elem` env)
2421 = case lookupTy n (tt_ctxt ist) of
2423 _ -> [n | n `elem` (map fst uvars)]
2424 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2425 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2426 ni 0 env (PCase _ c os) = ni 0 env c ++
2427 -- names in 'os', not counting the names bound in the cases
2428 (nub (concatMap (ni 0 env . snd) os)
2429 \\ nub (concatMap (ni 0 env . fst) os))
2430 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2431 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2432 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2433 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2434 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2435 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2436 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2437 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2438 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2439 ni 0 env (PHidden tm) = ni 0 env tm
2440 ni 0 env (PUnifyLog tm) = ni 0 env tm
2441 ni 0 env (PDisamb _ tm) = ni 0 env tm
2442 ni 0 env (PNoImplicits tm) = ni 0 env tm
2444 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2445 ni i env (PUnquote tm) = ni (i - 1) env tm
2447 ni i env tm = concatMap (ni i env) (children tm)
2449 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2452-- Return which of the given names are used in the given term.
2454usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2455usedNamesIn vars ist tm = nub $ ni 0 [] tm
2456 where -- TODO THINK added niTacImp, but is it right?
2457 ni 0 env (PRef _ _ n)
2458 | n `elem` vars && not (n `elem` env)
2459 = case lookupDefExact n (tt_ctxt ist) of
2462 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2463 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2464 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2465 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2466 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2467 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2468 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2469 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2470 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2471 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2472 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2473 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2474 ni 0 env (PHidden tm) = ni 0 env tm
2475 ni 0 env (PUnifyLog tm) = ni 0 env tm
2476 ni 0 env (PDisamb _ tm) = ni 0 env tm
2477 ni 0 env (PNoImplicits tm) = ni 0 env tm
2479 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2480 ni i env (PUnquote tm) = ni (i - 1) env tm
2482 ni i env tm = concatMap (ni i env) (children tm)
2484 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2487-- Return the list of inaccessible (= dotted) positions for a name.
2488getErasureInfo :: IState -> Name -> [Int]
2489getErasureInfo ist n =
2490 case lookupCtxtExact n (idris_optimisation ist) of
2491 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