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