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