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