2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
8{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
9 DeriveDataTypeable, DeriveGeneric, TypeSynonymInstances,
12module Idris.AbsSyntaxTree where
15import Idris.Core.Evaluate
16import Idris.Core.Elaborate hiding (Tactic(..))
17import Idris.Core.Typecheck
18import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
26import System.Console.Haskeline
29import Prelude hiding ((<$>))
31import Control.Applicative ((<|>))
33import Control.Monad.Trans.State.Strict
34import Control.Monad.Trans.Except
35import qualified Control.Monad.Trans.Class as Trans (lift)
37import Data.Data (Data)
38import Data.Function (on)
39import Data.Generics.Uniplate.Data (universe, children)
40import Data.List hiding (group)
42import qualified Data.Map.Strict as M
43import qualified Data.Text as T
45import qualified Data.Set as S
46import Data.Word (Word)
47import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
48import Data.Traversable (Traversable)
50import Data.Foldable (Foldable)
51import GHC.Generics (Generic)
55import Text.PrettyPrint.Annotated.Leijen
57data ElabWhat = ETypes | EDefns | EAll
60-- | Data to pass to recursively called elaborators; e.g. for where blocks,
61-- paramaterised declarations, etc.
63-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
64-- so that we can have mutually recursive elaborators in separate modules without
65-- having to muck about with cyclic modules.
66data ElabInfo = EInfo {
67 params :: [(Name, PTerm)]
68 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
69 , liftname :: Name -> Name
70 , namespace :: [String]
72 , constraintNS :: String -- ^ filename for adding to constraint variables
75 -- | We may, recursively, collect transformations to do on the rhs,
76 -- e.g. rewriting recursive calls to functions defined by 'with'
77 , rhs_trans :: PTerm -> PTerm
78 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
82toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")
84toplevelWith :: String -> ElabInfo
85toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")
87eInfoNames :: ElabInfo -> [Name]
88eInfoNames info = map fst (params info) ++ M.keys (inblock info)
90data IOption = IOption {
92 , opt_logcats :: [LogCat] -- ^ List of logging categories.
93 , opt_typecase :: Bool
94 , opt_typeintype :: Bool
95 , opt_coverage :: Bool
96 , opt_showimp :: Bool -- ^ show implicits
97 , opt_errContext :: Bool
100 , opt_nobanner :: Bool
102 , opt_codegen :: Codegen
103 , opt_outputTy :: OutputType
104 , opt_ibcsubdir :: FilePath
105 , opt_importdirs :: [FilePath]
106 , opt_triple :: String
108 , opt_cmdline :: [Opt] -- ^ remember whole command line
109 , opt_origerr :: Bool
110 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
111 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
112 , opt_optimise :: [Optimisation]
113 , opt_printdepth :: Maybe Int
114 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
115 , opt_desugarnats :: Bool
116 , opt_autoimpls :: Bool
117 } deriving (Show, Eq, Generic)
119defaultOpts = IOption { opt_logLevel = 0
121 , opt_typecase = False
122 , opt_typeintype = False
123 , opt_coverage = True
124 , opt_showimp = False
125 , opt_errContext = False
128 , opt_nobanner = False
130 , opt_codegen = Via IBCFormat "c"
131 , opt_outputTy = Executable
133 , opt_importdirs = []
137 , opt_origerr = False
138 , opt_autoSolve = True
139 , opt_autoImport = []
140 , opt_optimise = defaultOptimise
141 , opt_printdepth = Just 5000
142 , opt_evaltypes = True
143 , opt_desugarnats = False
144 , opt_autoimpls = True
147data PPOption = PPOption {
148 ppopt_impl :: Bool -- ^ whether to show implicits
149 , ppopt_desugarnats :: Bool
150 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
151 , ppopt_depth :: Maybe Int
154data Optimisation = PETransform -- ^ partial eval and associated transforms
155 deriving (Show, Eq, Generic)
157defaultOptimise = [PETransform]
159-- | Pretty printing options with default verbosity.
160defaultPPOption :: PPOption
161defaultPPOption = PPOption {
163 , ppopt_desugarnats = False
164 , ppopt_pinames = False
165 , ppopt_depth = Nothing
168-- | Pretty printing options with the most verbosity.
169verbosePPOption :: PPOption
170verbosePPOption = PPOption {
172 , ppopt_desugarnats = True
173 , ppopt_pinames = True
174 , ppopt_depth = Nothing
177-- | Get pretty printing options from the big options record.
178ppOption :: IOption -> PPOption
179ppOption opt = PPOption {
180 ppopt_impl = opt_showimp opt
181 , ppopt_pinames = False
182 , ppopt_depth = opt_printdepth opt
183 , ppopt_desugarnats = opt_desugarnats opt
186-- | Get pretty printing options from an idris state record.
187ppOptionIst :: IState -> PPOption
188ppOptionIst = ppOption . idris_options
190data LanguageExt = TypeProviders | ErrorReflection
191 deriving (Show, Eq, Read, Ord, Generic)
193-- | The output mode in use
194data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
195 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
198-- | How wide is the console?
199data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
200 | ColsWide Int -- ^ Manually specified - must be positive
201 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
202 deriving (Show, Eq, Generic)
204-- | If a function has no totality annotation, what do we assume?
205data DefaultTotality = DefaultCheckingTotal -- ^ Total
206 | DefaultCheckingPartial -- ^ Partial
207 | DefaultCheckingCovering -- ^Total coverage, but may diverge
208 deriving (Show, Eq, Generic)
210-- | The global state used in the Idris monad
211data IState = IState {
212 tt_ctxt :: Context -- ^ All the currently defined names and their terms
213 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
214 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
215 , idris_implicits :: Ctxt [PArg]
216 , idris_statics :: Ctxt [Bool]
217 , idris_classes :: Ctxt ClassInfo
218 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
219 , idris_records :: Ctxt RecordInfo
220 , idris_dsls :: Ctxt DSL
221 , idris_optimisation :: Ctxt OptInfo
222 , idris_datatypes :: Ctxt TypeInfo
223 , idris_namehints :: Ctxt [Name]
225 -- | list of lhs/rhs, and a list of missing clauses. These are not
227 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
228 , idris_flags :: Ctxt [FnOpt]
229 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
230 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
232 -- | module documentation is saved in a special MN so the context
233 -- mechanism can be used for disambiguation.
234 , idris_moduledocs :: Ctxt (Docstring DocTerm)
235 , idris_tyinfodata :: Ctxt TIData
236 , idris_fninfo :: Ctxt FnInfo
237 , idris_transforms :: Ctxt [(Term, Term)]
238 , idris_autohints :: Ctxt [Name]
239 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
240 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
241 , idris_totcheckfail :: [(FC, String)]
242 , idris_options :: IOption
244 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
246 -- | The currently defined but not proven metavariables. The Int is
247 -- the number of vars to display as a context, the Maybe Name is its
248 -- top-level function, the [Name] is the list of local variables
249 -- available for proof search and the Bools are whether :p is
250 -- allowed, and whether the variable is definable at all
251 -- (Metavariables are not definable if they are applied in a term
252 -- which still has hole bindings)
253 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
254 , idris_coercions :: [Name]
255 , idris_errRev :: [(Term, Term)]
256 , syntax_rules :: SyntaxRules
257 , syntax_keywords :: [String]
258 , imported :: [FilePath] -- ^ The imported modules
259 , idris_scprims :: [(Name, (Int, PrimFn))]
260 , idris_objs :: [(Codegen, FilePath)]
261 , idris_libs :: [(Codegen, String)]
262 , idris_cgflags :: [(Codegen, String)]
263 , idris_hdrs :: [(Codegen, String)]
264 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
265 , proof_list :: [(Name, (Bool, [String]))]
266 , errSpan :: Maybe FC
267 , parserWarnings :: [(FC, Err)]
268 , lastParse :: Maybe Name
269 , indent_stack :: [Int]
270 , brace_stack :: [Maybe Int]
271 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
272 , idris_parsedSpan :: Maybe FC
273 , hide_list :: Ctxt Accessibility
274 , default_access :: Accessibility
275 , default_total :: DefaultTotality
276 , ibc_write :: [IBCWrite]
277 , compiled_so :: Maybe String
278 , idris_dynamic_libs :: [DynamicLib]
279 , idris_language_extensions :: [LanguageExt]
280 , idris_outputmode :: OutputMode
281 , idris_colourRepl :: Bool
282 , idris_colourTheme :: ColourTheme
283 , idris_errorhandlers :: [Name] -- ^ Global error handlers
284 , idris_nameIdx :: (Int, Ctxt (Int, Name))
285 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
286 , module_aliases :: M.Map [T.Text] [T.Text]
287 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
288 , idris_postulates :: S.Set Name
289 , idris_externs :: S.Set (Name, Int)
290 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
291 , idris_whocalls :: Maybe (M.Map Name [Name])
292 , idris_callswho :: Maybe (M.Map Name [Name])
294 -- | List of names that were defined in the repl, and can be re-/un-defined
295 , idris_repl_defs :: [Name]
297 -- | Stack of names currently being elaborated, Bool set if it's an
298 -- instance (instances appear twice; also as a funtion name)
299 , elab_stack :: [(Name, Bool)]
302 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
303 , idris_exports :: [Name] -- ^ Functions with ExportList
304 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
305 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
306 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
307 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
308 , idris_ttstats :: M.Map Term (Int, Term)
309 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
313-- Required for parsers library, and therefore trifecta
314instance Show IState where
315 show = const "{internal state}"
317data SizeChange = Smaller | Same | Bigger | Unknown
318 deriving (Show, Eq, Generic)
320deriving instance Binary SizeChange
321deriving instance NFData SizeChange
324type SCGEntry = (Name, [Maybe (Int, SizeChange)])
325type UsageReason = (Name, Int) -- fn_name, its_arg_number
327data CGInfo = CGInfo {
330 , usedpos :: [(Int, [UsageReason])]
331 } deriving (Show, Generic)
333deriving instance Binary CGInfo
334deriving instance NFData CGInfo
337primDefs = [ sUN "unsafePerformPrimIO"
338 , sUN "mkLazyForeignPrim"
339 , sUN "mkForeignPrim"
341 , sUN "assert_unreachable"
344-- information that needs writing for the current module's .ibc file
345data IBCWrite = IBCFix FixDecl
350 | IBCInstance Bool Bool Name Name
357 | IBCImport (Bool, FilePath) -- ^ True = import public
358 | IBCImportDir FilePath
359 | IBCObj Codegen FilePath
360 | IBCLib Codegen String
361 | IBCCGFlag Codegen String
363 | IBCHeader Codegen String
364 | IBCAccess Name Accessibility
365 | IBCMetaInformation Name MetaInformation
366 | IBCTotal Name Totality
367 | IBCInjective Name Injectivity
368 | IBCFlags Name [FnOpt]
369 | IBCFnInfo Name FnInfo
370 | IBCTrans Name (Term, Term)
371 | IBCErrRev (Term, Term)
375 | IBCDef Name -- ^ The main context.
376 | IBCNameHint (Name, Name)
377 | IBCLineApp FilePath Int PTerm
378 | IBCErrorHandler Name
379 | IBCFunctionErrorHandler Name Name Name
381 | IBCExtern (Name, Int)
382 | IBCTotCheckErr FC String
384 | IBCModDocs Name -- ^ The name is the special name used to track module docs
385 | IBCUsage (Name, Int)
387 | IBCAutoHint Name Name
388 | IBCDeprecate Name String
389 | IBCFragile Name String
390 | IBCConstraint FC UConstraint
391 deriving (Show, Generic)
393-- | The initial state for the compiler
395idrisInit = IState initContext S.empty []
396 emptyContext emptyContext emptyContext [] emptyContext
397 emptyContext emptyContext emptyContext emptyContext
398 emptyContext emptyContext emptyContext emptyContext
399 emptyContext emptyContext emptyContext emptyContext
401 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
402 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
403 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
404 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
405 emptyContext S.empty M.empty emptyContext
408-- | The monad for the main REPL - reading and processing files and
409-- updating global state (hence the IO inner monad).
412-- type Idris = WriterT [Either String (IO ())] (State IState a))
415type Idris = StateT IState (ExceptT Err IO)
417catchError :: Idris a -> (Err -> Idris a) -> Idris a
418catchError = liftCatch catchE
420throwError :: Err -> Idris a
421throwError = Trans.lift . throwE
423-- Commands in the REPL
425data Codegen = Via IRFormat String
427 deriving (Show, Eq, Generic)
429deriving instance NFData Codegen
432data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
434data HowMuchDocs = FullDocs | OverviewDocs
440 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
444 | DocStr (Either Name Const) HowMuchDocs
448 | Load FilePath (Maybe Int) -- up to maximum line number
449 | ChangeDirectory FilePath
452 | Compile Codegen String
456 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
457 | AddProof (Maybe Name)
463 | LogCategory [LogCat]
469 | DynamicLink FilePath
472 | Search [String] PTerm
473 | CaseSplitAt Bool Int Name
474 | AddClauseFrom Bool Int Name
475 | AddProofClauseFrom Bool Int Name
476 | AddMissing Bool Int Name
477 | MakeWith Bool Int Name
478 | MakeCase Bool Int Name
479 | MakeLemma Bool Int Name
480 | DoProofSearch Bool -- update file
481 Bool -- recursive search
483 Name -- top level name
488 | SetColour ColourType IdrisColour
492 | SetConsoleWidth ConsoleWidth
493 | SetPrinterDepth (Maybe Int)
494 | Apropos [String] String
498 | MakeDoc String -- IdrisDoc
501 | PPrint OutputFmt Int PTerm
503 -- Debugging commands
505 | DebugUnify PTerm PTerm
507data OutputFmt = HTMLOutput | LaTeXOutput
509-- | Recognised logging categories for the Idris compiler.
511-- @TODO add in sub categories.
518 deriving (Show, Eq, Ord, Generic)
520strLogCat :: LogCat -> String
521strLogCat IParse = "parser"
522strLogCat IElab = "elab"
523strLogCat ICodeGen = "codegen"
524strLogCat IErasure = "erasure"
525strLogCat ICoverage = "coverage"
526strLogCat IIBC = "ibc"
528codegenCats :: [LogCat]
529codegenCats = [ICodeGen]
531parserCats :: [LogCat]
537loggingCatsStr :: String
538loggingCatsStr = unlines
541 , (strLogCat ICodeGen)
542 , (strLogCat IErasure)
543 , (strLogCat ICoverage)
547data Opt = Filename String
561 | NoBuiltins -- only for the really primitive stuff!
578 | Port String -- ^ REPL TCP port
586 | PkgMkDoc String -- IdrisDoc
596 | OutputTy OutputType
597 | Extension LanguageExt
598 | InterpretScript String
600 | TargetTriple String
603 | AddOpt Optimisation
604 | RemoveOpt Optimisation
607 | AutoWidth -- ^ Automatically adjust terminal width
608 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
609 | UseConsoleWidth ConsoleWidth
612 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
613 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
614 deriving (Show, Eq, Generic)
616data ElabShellCmd = EQED
624 | EDocStr (Either Name Const)
627-- Parsed declarations
629data Fixity = Infixl { prec :: Int }
630 | Infixr { prec :: Int }
631 | InfixN { prec :: Int }
632 | PrefixN { prec :: Int }
633 deriving (Eq, Generic)
635deriving instance Binary Fixity
636deriving instance NFData Fixity
639instance Show Fixity where
640 show (Infixl i) = "infixl " ++ show i
641 show (Infixr i) = "infixr " ++ show i
642 show (InfixN i) = "infix " ++ show i
643 show (PrefixN i) = "prefix " ++ show i
645data FixDecl = Fix Fixity String
646 deriving (Eq, Generic)
648instance Show FixDecl where
649 show (Fix f s) = show f ++ " " ++ s
652deriving instance Binary FixDecl
653deriving instance NFData FixDecl
656instance Ord FixDecl where
657 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
660data Static = Static | Dynamic
661 deriving (Show, Eq, Data, Generic, Typeable)
663deriving instance Binary Static
664deriving instance NFData Static
667-- ^ Mark bindings with their explicitness, and laziness
668data Plicity = Imp { pargopts :: [ArgOpt]
671 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
672 , pinsource :: Bool -- ^ Explicitly written in source
674 | Exp { pargopts :: [ArgOpt]
676 , pparam :: Bool -- ^ this is a param (rather than index)
678 | Constraint { pargopts :: [ArgOpt]
681 | TacImp { pargopts :: [ArgOpt]
685 deriving (Show, Eq, Data, Generic, Typeable)
688deriving instance Binary Plicity
689deriving instance NFData Plicity
692is_scoped :: Plicity -> Maybe ImplicitInfo
693is_scoped (Imp _ _ _ s _) = s
697impl = Imp [] Dynamic False (Just (Impl False True False)) False
698-- Machine generated top level implicit
699impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False
702forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False
703forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False
705expl = Exp [] Dynamic False
706expl_param = Exp [] Dynamic True
708constraint = Constraint [] Static
710tacimpl t = TacImp [] Dynamic t
712data FnOpt = Inlinable -- ^ always evaluate when simplifying
713 | TotalFn | PartialFn | CoveringFn
714 | Coinductive | AssertTotal
716 -- | type class dictionary, eval only when a function
717 -- argument, and further evaluation results.
719 | Implicit -- ^ implicit coercion
720 | NoImplicit -- ^ do not apply implicit coercions
721 | CExport String -- ^ export, with a C name
722 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
723 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
724 | Reflection -- ^ a reflecting function, compile-time only
725 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
726 | Constructor -- ^ Data constructor type
727 | AutoHint -- ^ use in auto implicit search
728 | PEGenerated -- ^ generated by partial evaluator
729 deriving (Show, Eq, Generic)
731deriving instance Binary FnOpt
732deriving instance NFData FnOpt
737inlinable :: FnOpts -> Bool
738inlinable = elem Inlinable
740dictionary :: FnOpts -> Bool
741dictionary = elem Dictionary
744-- | Type provider - what to provide
745data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
746 | ProvPostulate t -- ^ goal type must be Type, so only term
747 deriving (Show, Eq, Functor, Generic)
749type ProvideWhat = ProvideWhat' PTerm
751-- | Top-level declarations such as compiler directives, definitions,
752-- datatypes and typeclasses.
754 -- | Fixity declaration
755 = PFix FC Fixity [String]
756 -- | Type declaration (last FC is precise name location)
757 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
758 -- | Postulate, second FC is precise name location
759 | PPostulate Bool -- external def if true
760 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
762 | PClauses FC FnOpts Name [PClause' t]
763 -- | Top level constant
765 -- | Data declaration.
766 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
768 | PParams FC [(Name, t)] [PDecl' t]
769 -- | Open block/declaration
770 | POpenInterfaces FC [Name] [PDecl' t]
771 -- | New namespace, where FC is accurate location of the namespace
773 | PNamespace String FC [PDecl' t]
775 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
777 FC -- Record name precise location
778 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
779 [(Name, Docstring (Either Err t))] -- Param Docs
780 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
781 (Maybe (Name, FC)) -- Optional constructor name and location
782 (Docstring (Either Err t)) -- Constructor doc
783 SyntaxInfo -- Constructor SyntaxInfo
785 -- | Type class: arguments are documentation, syntax info, source
786 -- location, constraints, class name, class name location,
787 -- parameters, method declarations, optional constructor name
788 | PClass (Docstring (Either Err t)) SyntaxInfo FC
789 [(Name, t)] -- constraints
791 FC -- accurate location of class name
792 [(Name, FC, t)] -- parameters and precise locations
793 [(Name, Docstring (Either Err t))] -- parameter docstrings
794 [(Name, FC)] -- determining parameters and precise locations
795 [PDecl' t] -- declarations
796 (Maybe (Name, FC)) -- instance constructor name and location
797 (Docstring (Either Err t)) -- instance constructor docs
799 -- | Instance declaration: arguments are documentation, syntax
800 -- info, source location, constraints, class name, parameters, full
801 -- instance type, optional explicit name, and definitions
802 | PInstance (Docstring (Either Err t)) -- Instance docs
803 [(Name, Docstring (Either Err t))] -- Parameter docs
805 FC [(Name, t)] -- constraints
806 [Name] -- parent dictionaries to search for constraints
810 FC -- precise location of class
812 [(Name, t)] -- Extra names in scope in the body
813 t -- full instance type
814 (Maybe Name) -- explicit name
816 | PDSL Name (DSL' t) -- ^ DSL declaration
817 | PSyntax FC Syntax -- ^ Syntax definition
818 | PMutual FC [PDecl' t] -- ^ Mutual block
819 | PDirective Directive -- ^ Compiler directive.
821 -- | Type provider. The first t is the type, the second is the
822 -- term. The second FC is precise highlighting location.
823 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
825 -- | Source-to-source transformation rule. If bool is True, lhs and
826 -- rhs must be convertible.
827 | PTransform FC Bool t t
829 -- | FC is decl-level, for errors, and Strings represent the
831 | PRunElabDecl FC t [String]
832 deriving (Functor, Generic)
834deriving instance Binary PDecl'
835deriving instance NFData PDecl'
838-- | The set of source directives
839data Directive = DLib Codegen String
840 | DLink Codegen String
841 | DFlag Codegen String
842 | DInclude Codegen String
847 | DSetTotal Name -- assert totality after checking
848 | DAccess Accessibility
849 | DDefault DefaultTotality
851 | DDynamicLibs [String]
852 | DNameHint Name FC [(Name, FC)]
853 | DErrorHandlers Name FC Name FC [(Name, FC)]
854 | DLanguage LanguageExt
855 | DDeprecate Name String
856 | DFragile Name String
857 | DAutoImplicits Bool
861-- | A set of instructions for things that need to happen in IState
862-- after a term elaboration when there's been reflected elaboration.
863data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
864 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
865 | RAddInstance Name Name
866 | RDatatypeDeclInstrs Name [PArg]
867 -- | Datatype, constructors
868 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
871-- | For elaborator state
872data EState = EState {
873 case_decls :: [(Name, PDecl)]
874 , delayed_elab :: [(Int, Elab' EState ())]
875 , new_tyDecls :: [RDeclInstructions]
876 , highlighting :: [(FC, OutputAnnotation)]
877 , auto_binds :: [Name] -- ^ names bound as auto implicits
878 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
882initEState = EState [] [] [] [] [] []
884type ElabD a = Elab' EState a
886highlightSource :: FC -> OutputAnnotation -> ElabD ()
887highlightSource fc annot =
888 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
890-- | One clause of a top-level definition. Term arguments to constructors are:
892-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
894-- 2. The list of extra 'with' patterns
896-- 3. The right-hand side
898-- 4. The where block (PDecl' t)
900data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
901 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
902 | PClauseR FC [t] t [PDecl' t]
903 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
904 deriving (Functor, Generic)
906deriving instance Binary PClause'
907deriving instance NFData PClause'
912 -- | Data declaration
913 PDatadecl { d_name :: Name -- ^ The name of the datatype
914 , d_name_fc :: FC -- ^ The precise location of the type constructor name
915 , d_tcon :: t -- ^ Type constructor
916 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
918 -- | "Placeholder" for data whose constructors are defined later
919 | PLaterdecl { d_name :: Name
922 } deriving (Functor, Generic)
924-- | Transform the FCs in a PData and its associated terms. The first
925-- function transforms the general-purpose FCs, and the second
926-- transforms those that are used for semantic source highlighting, so
927-- they can be treated specially.
928mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
929mapPDataFC f g (PDatadecl n nfc tycon ctors) =
930 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
931 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
932 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
933mapPDataFC f g (PLaterdecl n nfc tycon) =
934 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
936deriving instance Binary PData'
937deriving instance NFData PData'
940-- Handy to get a free function for applying PTerm -> PTerm functions
941-- across a program, by deriving Functor
943type PDecl = PDecl' PTerm
944type PData = PData' PTerm
945type PClause = PClause' PTerm
947-- | Transform the FCs in a PTerm. The first function transforms the
948-- general-purpose FCs, and the second transforms those that are used
949-- for semantic source highlighting, so they can be treated specially.
950mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
951mapPDeclFC f g (PFix fc fixity ops) =
952 PFix (f fc) fixity ops
953mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
954 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
955mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
956 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
958mapPDeclFC f g (PClauses fc opts n clauses) =
959 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
960mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
961mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
962 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
963mapPDeclFC f g (PParams fc params decls) =
965 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
966 (map (mapPDeclFC f g) decls)
967mapPDeclFC f g (POpenInterfaces fc ifs decls) =
968 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
969mapPDeclFC f g (PNamespace ns fc decls) =
970 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
971mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
972 PRecord doc syn (f fc) opts n (g nfc)
973 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
975 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
976 plic, mapPTermFC f g ty, fdoc))
978 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
981mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
982 PClass doc syn (f fc)
983 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
984 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
985 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
986 (map (mapPDeclFC f g) body)
987 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
989mapPDeclFC f g (PInstance doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra instTy instN body) =
990 PInstance doc paramDocs syn (f fc)
991 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
992 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
993 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
994 (mapPTermFC f g instTy)
996 (map (mapPDeclFC f g) body)
997mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
998mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
1000 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
1001 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
1002mapPDeclFC f g (PMutual fc decls) =
1003 PMutual (f fc) (map (mapPDeclFC f g) decls)
1004mapPDeclFC f g (PDirective d) =
1007 DNameHint n nfc ns ->
1008 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
1009 DErrorHandlers n nfc n' nfc' ns ->
1010 DErrorHandlers n (g nfc) n' (g nfc') $
1011 map (\(an, anfc) -> (an, g anfc)) ns
1012mapPDeclFC f g (PProvider doc syn fc nfc what n) =
1013 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
1014mapPDeclFC f g (PTransform fc safe l r) =
1015 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
1016mapPDeclFC f g (PRunElabDecl fc script ns) =
1017 PRunElabDecl (f fc) (mapPTermFC f g script) ns
1019-- | Get all the names declared in a declaration
1020declared :: PDecl -> [Name]
1021declared (PFix _ _ _) = []
1022declared (PTy _ _ _ _ _ n fc t) = [n]
1023declared (PPostulate _ _ _ _ _ _ n t) = [n]
1024declared (PClauses _ _ n _) = [] -- not a declaration
1025declared (PCAF _ n _) = [n]
1026declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1027 where fstt (_, _, a, _, _, _, _) = a
1028declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
1029declared (PParams _ _ ds) = concatMap declared ds
1030declared (POpenInterfaces _ _ ds) = concatMap declared ds
1031declared (PNamespace _ _ ds) = concatMap declared ds
1032declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1033declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
1034declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1038declared (PDSL n _) = [n]
1039declared (PSyntax _ _) = []
1040declared (PMutual _ ds) = concatMap declared ds
1041declared (PDirective _) = []
1044-- get the names declared, not counting nested parameter blocks
1045tldeclared :: PDecl -> [Name]
1046tldeclared (PFix _ _ _) = []
1047tldeclared (PTy _ _ _ _ _ n _ t) = [n]
1048tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
1049tldeclared (PClauses _ _ n _) = [] -- not a declaration
1050tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1051tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1052 where fstt (_, _, a, _, _, _, _) = a
1053tldeclared (PParams _ _ ds) = []
1054tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
1055tldeclared (PMutual _ ds) = concatMap tldeclared ds
1056tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
1057tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
1058tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1064defined :: PDecl -> [Name]
1065defined (PFix _ _ _) = []
1066defined (PTy _ _ _ _ _ n _ t) = []
1067defined (PPostulate _ _ _ _ _ _ n t) = []
1068defined (PClauses _ _ n _) = [n] -- not a declaration
1069defined (PCAF _ n _) = [n]
1070defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1071 where fstt (_, _, a, _, _, _, _) = a
1072defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1073defined (PParams _ _ ds) = concatMap defined ds
1074defined (POpenInterfaces _ _ ds) = concatMap defined ds
1075defined (PNamespace _ _ ds) = concatMap defined ds
1076defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1077defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1078defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1082defined (PDSL n _) = [n]
1083defined (PSyntax _ _) = []
1084defined (PMutual _ ds) = concatMap defined ds
1085defined (PDirective _) = []
1088updateN :: [(Name, Name)] -> Name -> Name
1089updateN ns n | Just n' <- lookup n ns = n'
1092updateNs :: [(Name, Name)] -> PTerm -> PTerm
1094updateNs ns t = mapPT updateRef t
1095 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1098-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1099-- updateDNs [] t = t
1100-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1101-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1102-- where updateCNs ns (PClause n l ts r ds)
1103-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1104-- (map (fmap (updateNs ns)) ts)
1105-- (fmap (updateNs ns) r)
1106-- (map (updateDNs ns) ds)
1107-- updateDNs ns c = c
1109data PunInfo = IsType
1112 deriving (Eq, Show, Data, Typeable, Generic)
1114-- | High level language terms
1115data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1116 -- high-level language
1118 -- ^ A reference to a variable. The FC is its precise
1119 -- source location for highlighting. The list of FCs is a
1120 -- collection of additional highlighting locations.
1121 | PInferRef FC [FC] Name -- ^ A name to be defined later
1122 | PPatvar FC Name -- ^ A pattern variable
1123 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1124 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1125 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1126 | PTyped PTerm PTerm -- ^ Term with explicit type
1127 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1128 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1129 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1130 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1131 | PMatchApp FC Name -- ^ Make an application by type matching
1132 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1133 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1134 | PTrue FC PunInfo -- ^ Unit type..?
1135 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
1136 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1137 -- ^ "rewrite" syntax, with optional rewriting function and
1138 -- optional result type
1139 | PPair FC [FC] PunInfo PTerm PTerm
1140 -- ^ A pair (a, b) and whether it's a product type or a
1141 -- pair (solved by elaboration). The list of FCs is its
1143 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1144 -- ^ A dependent pair (tm : a ** b) and whether it's a
1145 -- sigma type or a pair that inhabits one (solved by
1146 -- elaboration). The [FC] is its punctuation.
1147 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1148 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1149 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1150 | PType FC -- ^ 'Type' type
1151 | PUniverse FC Universe -- ^ Some universe
1152 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1153 | PConstant FC Const -- ^ Builtin types
1154 | Placeholder -- ^ Underscore
1155 | PDoBlock [PDo] -- ^ Do notation
1156 | PIdiom FC PTerm -- ^ Idiom brackets
1158 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1159 | PProof [PTactic] -- ^ Proof script
1160 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1161 | PElabError Err -- ^ Error to report on elaboration
1162 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1163 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1164 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1165 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1166 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1167 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1168 | PUnquote PTerm -- ^ ~Term
1169 | PQuoteName Name Bool FC
1170 -- ^ `{n} where the FC is the precise highlighting for
1171 -- the name in particular. If the Bool is False, then
1172 -- it's `{{n}} and the name won't be resolved.
1173 | PRunElab FC PTerm [String]
1174 -- ^ %runElab tm - New-style proof script. Args are
1175 -- location, script, enclosing namespace.
1176 | PConstSugar FC PTerm
1177 -- ^ A desugared constant. The FC is a precise source
1178 -- location that will be used to highlight it later.
1179 deriving (Eq, Data, Typeable, Generic)
1181data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1184 deriving (Eq, Data, Generic, Typeable)
1186-- | Transform the FCs in a PTerm. The first function transforms the
1187-- general-purpose FCs, and the second transforms those that are used
1188-- for semantic source highlighting, so they can be treated specially.
1189mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1190mapPTermFC f g (PQuote q) = PQuote q
1191mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1192mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1193mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1194mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1195mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1196mapPTermFC 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)
1197mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1198mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1199mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1200mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1201mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1202mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1203mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1204mapPTermFC 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)
1205mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1206mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1207mapPTermFC 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)
1208mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1209mapPTermFC 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)
1210mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1211mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1212mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1213mapPTermFC f g (PType fc) = PType (f fc)
1214mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1215mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1216mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1217mapPTermFC f g Placeholder = Placeholder
1218mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1219 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1220 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1221 mapPDoFC (DoBindP fc t1 t2 alts) =
1222 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1223 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1224 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1225mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1226mapPTermFC f g (PReturn fc) = PReturn (f fc)
1227mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1228mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1229mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1230mapPTermFC f g (PElabError err) = PElabError err
1231mapPTermFC f g PImpossible = PImpossible
1232mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1233mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1234mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1235mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1236mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1237mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1238mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1239mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1240mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1243dg instance Binary PTerm
1244deriving instance NFData PTerm
1247mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1248mapPT f t = f (mpt t) where
1249 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1250 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1251 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1252 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1253 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1254 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1255 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1256 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1257 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1258 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1259 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1260 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1261 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1262 mpt (PHidden t) = PHidden (mapPT f t)
1263 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1264 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1265 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1266 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1267 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1268 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1269 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1273data PTactic' t = Intro [Name] | Intros | Focus Name
1274 | Refine Name [Bool] | Rewrite t | DoUnify
1281 | LetTac Name t | LetTacTy Name t t
1282 | Exact t | Compute | Trivial | TCInstance
1283 | ProofSearch Bool Bool Int (Maybe Name)
1284 [Name] -- allowed local names
1286 -- ^ the bool is whether to search recursively
1289 | ProofState | ProofTerm | Undo
1290 | Try (PTactic' t) (PTactic' t)
1291 | TSeq (PTactic' t) (PTactic' t)
1292 | ApplyTactic t -- see Language.Reflection module
1296 | GoalType String (PTactic' t)
1299 | TDocStr (Either Name Const)
1302 | TFail [ErrorReportPart]
1305 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable)
1307deriving instance Binary PTactic'
1308deriving instance NFData PTactic'
1310instance Sized a => Sized (PTactic' a) where
1311 size (Intro nms) = 1 + size nms
1313 size (Focus nm) = 1 + size nm
1314 size (Refine nm bs) = 1 + size nm + length bs
1315 size (Rewrite t) = 1 + size t
1316 size (Induction t) = 1 + size t
1317 size (LetTac nm t) = 1 + size nm + size t
1318 size (Exact t) = 1 + size t
1326 size (Try l r) = 1 + size l + size r
1327 size (TSeq l r) = 1 + size l + size r
1328 size (ApplyTactic t) = 1 + size t
1329 size (Reflect t) = 1 + size t
1330 size (Fill t) = 1 + size t
1334 size (TFail ts) = 1 + size ts
1337 size (CaseTac x) = 1 + size x
1338 size (Equiv t) = 1 + size t
1339 size (Claim x y) = 1 + size x + size y
1341 size (MatchRefine x) = 1 + size x
1342 size (LetTacTy x y z) = 1 + size x + size y + size z
1345type PTactic = PTactic' PTerm
1347data PDo' t = DoExp FC t
1348 | DoBind FC Name FC t -- ^ second FC is precise name location
1349 | DoBindP FC t t [(t,t)]
1350 | DoLet FC Name FC t t -- ^ second FC is precise name location
1352 deriving (Eq, Functor, Data, Generic, Typeable)
1354deriving instance Binary PDo'
1355deriving instance NFData PDo'
1358instance Sized a => Sized (PDo' a) where
1359 size (DoExp fc t) = 1 + size fc + size t
1360 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1361 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1362 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1363 size (DoLetP fc l r) = 1 + size fc + size l + size r
1365type PDo = PDo' PTerm
1367-- The priority gives a hint as to elaboration order. Best to elaborate
1368-- things early which will help give a more concrete type to other
1369-- variables, e.g. a before (interpTy a).
1371data PArg' t = PImp { priority :: Int
1372 , machine_inf :: Bool -- ^ true if the machine inferred it
1373 , argopts :: [ArgOpt]
1377 | PExp { priority :: Int
1378 , argopts :: [ArgOpt]
1382 | PConstraint { priority :: Int
1383 , argopts :: [ArgOpt]
1387 | PTacImplicit { priority :: Int
1388 , argopts :: [ArgOpt]
1393 deriving (Show, Eq, Functor, Data, Generic, Typeable)
1395data ArgOpt = AlwaysShow
1399 deriving (Show, Eq, Data, Generic, Typeable)
1401instance Sized a => Sized (PArg' a) where
1402 size (PImp p _ l nm trm) = 1 + size nm + size trm
1403 size (PExp p l nm trm) = 1 + size nm + size trm
1404 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1405 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1408deriving instance Binary PArg'
1409deriving instance NFData PArg'
1412pimp n t mach = PImp 1 mach [] n t
1413pexp t = PExp 1 [] (sMN 0 "arg") t
1414pconst t = PConstraint 1 [] (sMN 0 "carg") t
1415ptacimp n s t = PTacImplicit 2 [] n s t
1417type PArg = PArg' PTerm
1419-- | Get the highest FC in a term, if one exists
1420highestFC :: PTerm -> Maybe FC
1421highestFC (PQuote _) = Nothing
1422highestFC (PRef fc _ _) = Just fc
1423highestFC (PInferRef fc _ _) = Just fc
1424highestFC (PPatvar fc _) = Just fc
1425highestFC (PLam fc _ _ _ _) = Just fc
1426highestFC (PPi _ _ _ _ _) = Nothing
1427highestFC (PLet fc _ _ _ _ _) = Just fc
1428highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1429highestFC (PApp fc _ _) = Just fc
1430highestFC (PAppBind fc _ _) = Just fc
1431highestFC (PMatchApp fc _) = Just fc
1432highestFC (PCase fc _ _) = Just fc
1433highestFC (PIfThenElse fc _ _ _) = Just fc
1434highestFC (PTrue fc _) = Just fc
1435highestFC (PResolveTC fc) = Just fc
1436highestFC (PRewrite fc _ _ _ _) = Just fc
1437highestFC (PPair fc _ _ _ _) = Just fc
1438highestFC (PDPair fc _ _ _ _ _) = Just fc
1439highestFC (PAs fc _ _) = Just fc
1440highestFC (PAlternative _ _ args) =
1441 case mapMaybe highestFC args of
1444highestFC (PHidden _) = Nothing
1445highestFC (PType fc) = Just fc
1446highestFC (PUniverse _ _) = Nothing
1447highestFC (PGoal fc _ _ _) = Just fc
1448highestFC (PConstant fc _) = Just fc
1449highestFC Placeholder = Nothing
1450highestFC (PDoBlock lines) =
1451 case map getDoFC lines of
1455 getDoFC (DoExp fc t) = fc
1456 getDoFC (DoBind fc nm nfc t) = fc
1457 getDoFC (DoBindP fc l r alts) = fc
1458 getDoFC (DoLet fc nm nfc l r) = fc
1459 getDoFC (DoLetP fc l r) = fc
1461highestFC (PIdiom fc _) = Just fc
1462highestFC (PReturn fc) = Just fc
1463highestFC (PMetavar fc _) = Just fc
1464highestFC (PProof _) = Nothing
1465highestFC (PTactics _) = Nothing
1466highestFC (PElabError _) = Nothing
1467highestFC PImpossible = Nothing
1468highestFC (PCoerced tm) = highestFC tm
1469highestFC (PDisamb _ opts) = highestFC opts
1470highestFC (PUnifyLog tm) = highestFC tm
1471highestFC (PNoImplicits tm) = highestFC tm
1472highestFC (PQuasiquote _ _) = Nothing
1473highestFC (PUnquote tm) = highestFC tm
1474highestFC (PQuoteName _ _ fc) = Just fc
1475highestFC (PRunElab fc _ _) = Just fc
1476highestFC (PConstSugar fc _) = Just fc
1477highestFC (PAppImpl t _) = highestFC t
1481data ClassInfo = CI {
1482 instanceCtorName :: Name
1483 , class_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1484 , class_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1485 , class_default_superclasses :: [PDecl]
1486 , class_params :: [Name]
1487 , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded
1488 , class_determiners :: [Int]
1489 } deriving (Show, Generic)
1491deriving instance Binary ClassInfo
1492deriving instance NFData ClassInfo
1496data RecordInfo = RI {
1497 record_parameters :: [(Name,PTerm)]
1498 , record_constructor :: Name
1499 , record_projections :: [Name]
1500 } deriving (Show, Generic)
1502-- Type inference data
1504data TIData = TIPartial -- ^ a function with a partially defined type
1505 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1506 deriving (Show, Generic)
1508-- | Miscellaneous information about functions
1509data FnInfo = FnInfo { fn_params :: [Int] }
1510 deriving (Show, Generic)
1512deriving instance Binary FnInfo
1513deriving instance NFData FnInfo
1516data OptInfo = Optimise {
1517 inaccessible :: [(Int,Name)] -- includes names for error reporting
1518 , detaggable :: Bool
1519 } deriving (Show, Generic)
1521deriving instance Binary OptInfo
1522deriving instance NFData OptInfo
1525-- | Syntactic sugar info
1531 , dsl_var :: Maybe t
1532 , index_first :: Maybe t
1533 , index_next :: Maybe t
1534 , dsl_lambda :: Maybe t
1535 , dsl_let :: Maybe t
1537 } deriving (Show, Functor, Generic)
1539deriving instance Binary DSL'
1540deriving instance NFData DSL'
1543type DSL = DSL' PTerm
1545data SynContext = PatternSyntax
1548 deriving (Show, Generic)
1550deriving instance Binary SynContext
1551deriving instance NFData SynContext
1554data Syntax = Rule [SSymbol] PTerm SynContext
1555 | DeclRule [SSymbol] [PDecl]
1556 deriving (Show, Generic)
1558syntaxNames :: Syntax -> [Name]
1559syntaxNames (Rule syms _ _) = mapMaybe ename syms
1560 where ename (Keyword n) = Just n
1562syntaxNames (DeclRule syms _) = mapMaybe ename syms
1563 where ename (Keyword n) = Just n
1566syntaxSymbols :: Syntax -> [SSymbol]
1567syntaxSymbols (Rule ss _ _) = ss
1568syntaxSymbols (DeclRule ss _) = ss
1570deriving instance Binary Syntax
1571deriving instance NFData Syntax
1574data SSymbol = Keyword Name
1579 deriving (Show, Eq, Generic)
1583deriving instance Binary SSymbol
1584deriving instance NFData SSymbol
1587newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1590emptySyntaxRules :: SyntaxRules
1591emptySyntaxRules = SyntaxRules []
1593updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1594updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1596 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1601 ruleSort (s1:ss1) (s2:ss2) =
1602 case symCompare s1 s2 of
1603 EQ -> ruleSort ss1 ss2
1606 -- Better than creating Ord instance for SSymbol since
1607 -- in general this ordering does not really make sense.
1608 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1609 symCompare (Keyword _) _ = LT
1610 symCompare (Symbol _) (Keyword _) = GT
1611 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1612 symCompare (Symbol _) _ = LT
1613 symCompare (Binding _) (Keyword _) = GT
1614 symCompare (Binding _) (Symbol _) = GT
1615 symCompare (Binding b1) (Binding b2) = compare b1 b2
1616 symCompare (Binding _) _ = LT
1617 symCompare (Expr _) (Keyword _) = GT
1618 symCompare (Expr _) (Symbol _) = GT
1619 symCompare (Expr _) (Binding _) = GT
1620 symCompare (Expr e1) (Expr e2) = compare e1 e2
1621 symCompare (Expr _) _ = LT
1622 symCompare (SimpleExpr _) (Keyword _) = GT
1623 symCompare (SimpleExpr _) (Symbol _) = GT
1624 symCompare (SimpleExpr _) (Binding _) = GT
1625 symCompare (SimpleExpr _) (Expr _) = GT
1626 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1628initDSL = DSL (PRef f [] (sUN ">>="))
1629 (PRef f [] (sUN "return"))
1630 (PRef f [] (sUN "<*>"))
1631 (PRef f [] (sUN "pure"))
1638 where f = fileFC "(builtin)"
1640data Using = UImplicit Name PTerm
1641 | UConstraint Name [Name]
1642 deriving (Show, Eq, Data, Generic, Typeable)
1644deriving instance Binary Using
1645deriving instance NFData Using
1648data SyntaxInfo = Syn {
1650 , syn_params :: [(Name, PTerm)]
1651 , syn_namespace :: [String]
1653 , imp_methods :: [Name]
1654 -- ^ class methods. When expanding implicits, these should be
1655 -- expanded even under binders
1656 , decoration :: Name -> Name
1658 , implicitAllowed :: Bool
1659 , constraintAllowed :: Bool
1660 , maxline :: Maybe Int
1661 , mut_nesting :: Int
1663 , syn_in_quasiquote :: Int
1664 , syn_toplevel :: Bool
1665 , withAppAllowed :: Bool
1666 } deriving (Show, Generic)
1668deriving instance NFData SyntaxInfo
1669deriving instance Binary SyntaxInfo
1672defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1674expandNS :: SyntaxInfo -> Name -> Name
1675expandNS syn n@(NS _ _) = n
1676expandNS syn n = case syn_namespace syn of
1681-- For inferring types of things
1683bi = fileFC "builtin"
1684primfc = fileFC "(primitive)"
1686inferTy = sMN 0 "__Infer"
1687inferCon = sMN 0 "__infer"
1688inferDecl = PDatadecl inferTy primfc
1690 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1691 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1692 (PRef bi [] inferTy)), bi, [])]
1695infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1696infP = P (TCon 6 0) inferTy (TType (UVal 0))
1698getInferTerm, getInferType :: Term -> Term
1699getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1700getInferTerm (App _ (App _ _ _) tm) = tm
1701getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1703getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1704 where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))
1705 toTy (PVar t) = PVTy t
1707getInferType (App _ (App _ _ ty) _) = ty
1711-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1713primNames = [inferTy, inferCon]
1716unitCon = sUN "MkUnit"
1718falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1719 "The empty type, also known as the trivially false proposition." ++
1721 "Use `void` or `absurd` to prove anything if you have a variable " ++
1722 "of type `Void` in scope."
1725pairTy = sNS (sUN "Pair") ["Builtins"]
1726pairCon = sNS (sUN "MkPair") ["Builtins"]
1728upairTy = sNS (sUN "UPair") ["Builtins"]
1729upairCon = sNS (sUN "MkUPair") ["Builtins"]
1733eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1734 "The propositional equality type. A proof that `x` = `y`." ++
1736 "To use such a proof, pattern-match on it, and the two equal things will " ++
1737 "then need to be the _same_ pattern." ++
1739 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1740 "is possible to state equalities between values of potentially different " ++
1741 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1743 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1745eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1746 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1748 [(reflDoc, reflParamDoc,
1749 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1750 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1751 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1752 pimp (n "B") Placeholder False,
1753 pexp (PRef bi [] (n "x")),
1754 pexp (PRef bi [] (n "x"))])), bi, [])]
1756 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1757 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1758 "shown that both sides are in fact equal."
1759 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1760 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1762eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1763 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1769-- | The special name to be used in the module documentation context -
1770-- not for use in the main definition context. The namespace around it
1771-- will determine the module to which the docs adhere.
1773modDocName = sMN 0 "ModuleDocs"
1775-- Defined in builtins.idr
1776sigmaTy = sNS (sUN "DPair") ["Builtins"]
1777sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1779piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1780piBind = piBindp expl
1782piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1784piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1787-- Pretty-printing declarations and terms
1789-- These "show" instances render to an absurdly wide screen because inserted line breaks
1790-- could interfere with interactive editing, which calls "show".
1792instance Show PTerm where
1793 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1795instance Show PDecl where
1796 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1798instance Show PClause where
1799 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1801instance Show PData where
1802 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1804instance Pretty PTerm OutputAnnotation where
1805 pretty = prettyImp defaultPPOption
1807-- | Colourise annotations according to an Idris state. It ignores the
1808-- names in the annotation, as there's no good way to show extended
1809-- information on a terminal.
1810annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1811annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1812annotationColour ist (AnnConst c) =
1813 let theme = idris_colourTheme ist
1814 in Just $ if constIsType c
1815 then typeColour theme
1816 else dataColour theme
1817annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1818annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1819annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1820annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1821annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1822annotationColour ist (AnnName n _ _ _) =
1823 let ctxt = tt_ctxt ist
1824 theme = idris_colourTheme ist
1826 _ | isDConName n ctxt -> Just $ dataColour theme
1827 _ | isFnName n ctxt -> Just $ functionColour theme
1828 _ | isTConName n ctxt -> Just $ typeColour theme
1829 _ | isPostulateName n ist -> Just $ postulateColour theme
1830 _ | otherwise -> Nothing -- don't colourise unknown names
1831annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1832 where colour BoldText = IdrisColour Nothing True False True False
1833 colour UnderlineText = IdrisColour Nothing True True False False
1834 colour ItalicText = IdrisColour Nothing True False False True
1835annotationColour ist _ = Nothing
1838-- | Colourise annotations according to an Idris state. It ignores the
1839-- names in the annotation, as there's no good way to show extended
1840-- information on a terminal. Note that strings produced this way will
1841-- not be coloured on Windows, so the use of the colour rendering
1842-- functions in Idris.Output is to be preferred.
1843consoleDecorate :: IState -> OutputAnnotation -> String -> String
1844consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1846isPostulateName :: Name -> IState -> Bool
1847isPostulateName n ist = S.member n (idris_postulates ist)
1849-- | Pretty-print a high-level closed Idris term with no information
1850-- about precedence/associativity
1851prettyImp :: PPOption -- ^ pretty printing options
1852 -> PTerm -- ^ the term to pretty-print
1853 -> Doc OutputAnnotation
1854prettyImp impl = pprintPTerm impl [] [] []
1856-- | Serialise something to base64 using its Binary instance.
1858-- | Do the right thing for rendering a term in an IState
1859prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1860prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1862-- | Pretty-print a high-level Idris term in some bindings context
1864pprintPTerm :: PPOption -- ^ pretty printing options
1865 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1866 -> [Name] -- ^ names to always show in pi, even if not used
1867 -> [FixDecl] -- ^ Fixity declarations
1868 -> PTerm -- ^ the term to pretty-print
1869 -> Doc OutputAnnotation
1870pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1875 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1876 prettySe d p bnd (PQuote r) =
1877 text "![" <> pretty r <> text "]"
1878 prettySe d p bnd (PPatvar fc n) = pretty n
1880 | Just str <- slist d p bnd e = depth d str
1881 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1882 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1883 prettySe d p bnd (PLam fc n nfc ty sc) =
1884 depth d . bracket p startPrec . group . align . hang 2 $
1885 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1886 prettySe (decD d) startPrec ((n, False):bnd) sc
1887 prettySe d p bnd (PLet fc n nfc ty v sc) =
1888 depth d . bracket p startPrec . group . align $
1889 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1890 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1891 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1892 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1893 || ppopt_pinames ppo && uname n =
1894 depth d . bracket p startPrec . group $
1895 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1896 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1898 depth d . bracket p startPrec . group $
1899 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1900 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1902 uname (UN n) = case str n of
1909 Static -> text "%static" <> space
1911 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1913 depth d . bracket p startPrec $
1914 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1915 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1916 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1920 Static -> text "%static" <> space
1922 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1923 depth d . bracket p startPrec $
1924 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1925 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1926 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1927 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1928 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1929 depth d . bracket p startPrec $
1930 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1931 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1932 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1933 | basename neg == sUN "negate" =
1934 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1935 -- This case preserves the behavior of the former constructor PEq.
1936 -- It should be removed if feasible when the pretty-printing of infix
1937 -- operators in general is improved.
1938 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1939 | n == eqTy, ppopt_impl ppo =
1940 depth d . bracket p eqPrec $
1941 enclose lparen rparen eq <+>
1942 align (group (vsep (map (prettyArgS (decD d) bnd)
1945 depth d . bracket p eqPrec . align . group $
1946 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1947 where eq = annName eqTy (text "=")
1949 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1950 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1951 | UN nm <- basename f
1952 , not (ppopt_impl ppo) && null (getShowArgs args) =
1953 prettyName True (ppopt_impl ppo) bnd f
1954 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1955 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1956 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1957 | UN nm <- basename op
1959 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1960 case getShowArgs args of
1962 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1963 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1964 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1965 (l@(PExp{}) : r@(PExp{}) : rest) ->
1966 depth d . bracket p funcAppPrec $
1967 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1968 align (group (vsep (map (prettyArgS d bnd) rest)))
1969 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1970 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1971 f = getFixity (opStr op)
1973 Nothing -> funcAppPrec + 1
1974 Just (Infixl p') -> p'
1975 Just f' -> prec f' + 1
1977 Nothing -> funcAppPrec + 1
1978 Just (Infixr p') -> p'
1979 Just f' -> prec f' + 1
1980 inFix l r = align . group $
1981 (prettySe (decD d) left bnd l <+> opName False) <$>
1982 group (prettySe (decD d) right bnd r)
1983 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1984 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1985 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1986 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1987 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1988 let args = getShowArgs as
1989 fp = prettySe (decD d) (startPrec + 1) bnd f
1990 shownArgs = if ppopt_impl ppo then as else args
1992 depth d . bracket p funcAppPrec . group $
1995 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1996 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1997 prettySe d p bnd (PCase _ scr cases) =
1998 bracket p funcAppPrec $
1999 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
2000 depth d (indent 2 (vsep (map ppcase cases)))
2002 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
2003 ([(n, False) | n <- vars l] ++ bnd)
2004 in nest nestingSize $
2005 prettyCase l <+> text "=>" <+> prettyCase r
2006 -- Warning: this is a bit of a hack. At this stage, we don't have the
2007 -- global context, so we can't determine which names are constructors,
2008 -- which are types, and which are pattern variables on the LHS of the
2009 -- case pattern. We use the heuristic that names without a namespace
2010 -- are patvars, because right now case blocks in PTerms are always
2011 -- delaborated from TT before being sent to the pretty-printer. If they
2012 -- start getting printed directly, THIS WILL BREAK.
2013 -- Potential solution: add a list of known patvars to the cases in
2014 -- PCase, and have the delaborator fill it out, kind of like the pun
2015 -- disambiguation on PDPair.
2016 vars tm = filter noNS (allNamesIn tm)
2017 noNS (NS _ _) = False
2020 prettySe d p bnd (PIfThenElse _ c t f) =
2021 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
2022 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
2023 , kwd "then" <+> prettySe (decD d) startPrec bnd t
2024 , kwd "else" <+> prettySe (decD d) startPrec bnd f
2026 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
2027 prettySe d p bnd (PResolveTC _) = kwd "%instance"
2028 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
2029 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
2030 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
2031 prettySe d p bnd (PRewrite _ by l r _) =
2032 depth d . bracket p startPrec $
2033 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
2036 Just fn -> text "using" <+>
2037 prettyName True (ppopt_impl ppo) bnd fn) <+>
2038 text "in" <+> prettySe (decD d) startPrec bnd r
2039 prettySe d p bnd (PTyped l r) =
2040 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
2041 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
2042 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
2043 align . group . vsep . punctuate (ann comma) $
2044 map (prettySe (decD d) startPrec bnd) elts
2045 where ann = case pun of
2047 IsType -> annName pairTy
2048 IsTerm -> annName pairCon
2049 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
2050 | Just elts <- dPairElts dpair
2051 = depth d . enclose (annotated lparen) (annotated rparen) .
2052 align . group . vsep . punctuate (space <> annotated (text "**")) $
2058 annotated (text "**") <+>
2059 prettySe (decD d) startPrec (addBinding bnd) r <>
2061 where annotated = case pun of
2062 IsType -> annName sigmaTy
2063 IsTerm -> annName sigmaCon
2066 (left, addBinding) = case (l, pun) of
2067 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
2068 _ -> (prettySe (decD d) startPrec bnd l, id)
2071 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
2072 ppElts ((PRef _ _ n, t):rs) bs
2074 = (bindingOf n False <+> colon <+>
2075 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2076 ppElts ((l, t):rs) bs
2077 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2078 prettySe d p bnd (PAlternative ns a as) =
2079 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2082 foldr ((\ l r -> l <+> text "," <+> r) .
2083 depth d . prettySe (decD d) startPrec bnd)
2085 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2086 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2087 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2088 -- XXX: add pretty for tactics
2089 prettySe d p bnd (PProof ts) =
2090 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2091 prettySe d p bnd (PTactics ts) =
2092 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2093 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2094 prettySe d p bnd (PReturn f) = kwd "return"
2095 prettySe d p bnd PImpossible = kwd "impossible"
2096 prettySe d p bnd Placeholder = text "_"
2097 prettySe d p bnd (PDoBlock dos) =
2098 bracket p startPrec $
2099 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2100 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2101 ppdo bnd (DoBind _ bn _ tm : dos) =
2102 (prettyBindingOf bn False <+> text "<-" <+>
2103 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2104 ppdo ((bn, False):bnd) dos
2105 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2106 text "no pretty printer for pattern-matching do binding" :
2108 ppdo bnd (DoLet _ ln _ ty v : dos) =
2109 (kwd "let" <+> prettyBindingOf ln False <+>
2110 (if ty /= Placeholder
2111 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2113 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2114 ppdo ((ln, False):bnd) dos
2115 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2116 text "no pretty printer for pattern-matching do binding" :
2119 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2120 prettySe d p bnd (PElabError s) = pretty s
2121 -- Quasiquote pprinting ignores bound vars
2122 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2123 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2124 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2125 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2126 where start = if res then "`{" else "`{{"
2127 end = if res then "}" else "}}"
2128 prettySe d p bnd (PRunElab _ tm _) =
2129 bracket p funcAppPrec . group . align . hang 2 $
2131 prettySe (decD d) funcAppPrec bnd tm
2132 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2133 prettySe d p bnd _ = text "missing pretty-printer for term"
2135 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2136 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2137 where display (UN n) = T.unpack n
2138 display (MN _ n) = T.unpack n
2139 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2140 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2143 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2144 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2145 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2146 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2148 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2149 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2150 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2151 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2153 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2154 annName n = annotate (AnnName n Nothing Nothing Nothing)
2156 opStr :: Name -> String
2157 opStr (NS n _) = opStr n
2158 opStr (UN n) = T.unpack n
2160 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2161 slist' (Just d) _ _ _ | d <= 0 = Nothing
2163 | containsHole e = Nothing
2164 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2165 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2166 slist' d p bnd (PRef _ _ nil)
2167 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2168 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2169 | nsroot cons == sUN "::",
2170 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2172 Just tl' <- slist' (decD d) p bnd tl
2173 = Just (prettySe d startPrec bnd hd : tl')
2175 isImp (PImp {}) = True
2177 slist' _ _ _ tm = Nothing
2179 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2181 [] -> annotate (AnnData "" "") $ text "[]"
2182 [x] -> enclose left right . group $ x
2183 xs -> enclose left right .
2184 align . group . vsep .
2185 punctuate comma $ xs
2186 where left = (annotate (AnnData "" "") (text "["))
2187 right = (annotate (AnnData "" "") (text "]"))
2188 comma = (annotate (AnnData "" "") (text ","))
2189 slist _ _ _ _ = Nothing
2191 pairElts :: PTerm -> Maybe [PTerm]
2192 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2193 | otherwise = Just [x, y]
2194 pairElts _ = Nothing
2196 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2197 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2198 | otherwise = Just [(l, t), (Placeholder, r)]
2199 dPairElts _ = Nothing
2201 natns = "Prelude.Nat."
2203 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2205 | ppopt_desugarnats ppo = Nothing
2206 | otherwise = snat' d p e
2208 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2209 snat' (Just x) _ _ | x <= 0 = Nothing
2210 snat' d p (PRef _ _ z)
2211 | show z == (natns++"Z") || show z == "Z" = Just 0
2212 snat' d p (PApp _ s [PExp {getTm=n}])
2213 | show s == (natns++"S") || show s == "S",
2214 Just n' <- snat' (decD d) p n
2216 snat' _ _ _ = Nothing
2218 bracket outer inner doc
2219 | outer > inner = lparen <> doc <> rparen
2222 ellipsis = text "..."
2225 depth (Just d) = if d <= 0 then const ellipsis else id
2227 decD = fmap (\x -> x - 1)
2229 kwd = annotate AnnKeyword . text
2231 fixities :: M.Map String Fixity
2232 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2234 getFixity :: String -> Maybe Fixity
2235 getFixity = flip M.lookup fixities
2237-- | Strip away namespace information
2238basename :: Name -> Name
2239basename (NS n _) = basename n
2242-- | Determine whether a name was the one inserted for a hole or guess
2243-- by the delaborator
2244isHoleName :: Name -> Bool
2245isHoleName (UN n) = n == T.pack "[__]"
2248-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2249containsHole :: PTerm -> Bool
2250containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2252-- | Pretty-printer helper for names that attaches the correct annotations
2253prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2254 -> Bool -- ^ whether to show namespaces
2255 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2256 -> Name -- ^ the name to pprint
2257 -> Doc OutputAnnotation
2258prettyName infixParen showNS bnd n
2259 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2260 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2261 | (UN n') <- n, T.unpack n' == "_" = text "_"
2262 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2263 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2264 where fullName = text nameSpace <> parenthesise (text (baseName n))
2265 baseName (UN n) = T.unpack n
2266 baseName (NS n ns) = baseName n
2267 baseName (MN i s) = T.unpack s
2268 baseName other = show other
2269 nameSpace = case n of
2270 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2272 isInfix = case baseName n of
2274 (c : _) -> not (isAlpha c)
2275 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2278showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2279showCImp ppo (PClause _ n l ws r w)
2280 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2281 <+> text "where" <+> text (show w)
2284 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2285showCImp ppo (PWith _ n l ws r pn w)
2286 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2287 <+> braces (text (show w))
2290 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2293showDImp :: PPOption -> PData -> Doc OutputAnnotation
2294showDImp ppo (PDatadecl n nfc ty cons)
2295 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2296 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2298showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2299showDecls o ds = vsep (map (showDeclImp o) ds)
2301showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2302showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2303showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2304 indent 2 (vsep (map (showCImp o) cs))
2305showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2306showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2307showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2308showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2309showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2310showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2311 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2312showDeclImp o (PInstance _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2313 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2314showDeclImp _ _ = text "..."
2315-- showDeclImp (PImport o) = "import " ++ o
2317getImps :: [PArg] -> [(Name, PTerm)]
2319getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2320getImps (_ : xs) = getImps xs
2322getExps :: [PArg] -> [PTerm]
2324getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2325getExps (_ : xs) = getExps xs
2327getShowArgs :: [PArg] -> [PArg]
2329getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2330getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2331 | PImp _ _ _ _ tm <- e
2332 , containsHole tm = e : getShowArgs xs
2333getShowArgs (_ : xs) = getShowArgs xs
2335getConsts :: [PArg] -> [PTerm]
2337getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2338getConsts (_ : xs) = getConsts xs
2340getAll :: [PArg] -> [PTerm]
2345showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2346 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2347 -> PPOption -- ^ pretty printing options
2348 -> Bool -- ^ whether to colourise
2349 -> Name -- ^ the term to show
2351showName ist bnd ppo colour n = case ist of
2352 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2353 Nothing -> showbasic n
2354 where name = if ppopt_impl ppo then show n else showbasic n
2355 showbasic n@(UN _) = showCG n
2356 showbasic (MN i s) = str s
2357 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2358 showbasic (SN s) = show s
2360 colourise n t = let ctxt' = fmap tt_ctxt ist in
2363 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2364 else colouriseBound t name
2365 | isDConName n ctxt -> colouriseData t name
2366 | isFnName n ctxt -> colouriseFun t name
2367 | isTConName n ctxt -> colouriseType t name
2368 -- The assumption is that if a name is not bound and does not exist in the
2369 -- global context, then we're somewhere in which implicit info has been lost
2370 -- (like error messages). Thus, unknown vars are colourised as implicits.
2371 | otherwise -> colouriseImplicit t name
2373showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2374 -> PTerm -- ^ the term to show
2376showTm ist = displayDecorated (consoleDecorate ist) .
2377 renderPretty 0.8 100000 .
2378 prettyImp (ppOptionIst ist)
2380-- | Show a term with implicits, no colours
2381showTmImpls :: PTerm -> String
2382showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2384-- | Show a term with specific options
2385showTmOpts :: PPOption -> PTerm -> String
2386showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2389instance Sized PTerm where
2390 size (PQuote rawTerm) = size rawTerm
2391 size (PRef fc _ name) = size name
2392 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2393 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2394 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2395 size (PTyped trm ty) = 1 + size trm + size ty
2396 size (PApp fc name args) = 1 + size args
2397 size (PAppBind fc name args) = 1 + size args
2398 size (PCase fc trm bdy) = 1 + size trm + size bdy
2399 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2400 size (PTrue fc _) = 1
2401 size (PResolveTC fc) = 1
2402 size (PRewrite fc by left right _) = 1 + size left + size right
2403 size (PPair fc _ _ left right) = 1 + size left + size right
2404 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2405 size (PAlternative _ a alts) = 1 + size alts
2406 size (PHidden hidden) = size hidden
2407 size (PUnifyLog tm) = size tm
2408 size (PDisamb _ tm) = size tm
2409 size (PNoImplicits tm) = size tm
2411 size (PUniverse _ _) = 1
2412 size (PConstant fc const) = 1 + size fc + size const
2413 size Placeholder = 1
2414 size (PDoBlock dos) = 1 + size dos
2415 size (PIdiom fc term) = 1 + size term
2416 size (PReturn fc) = 1
2417 size (PMetavar _ name) = 1
2418 size (PProof tactics) = size tactics
2419 size (PElabError err) = size err
2420 size PImpossible = 1
2423getPArity :: PTerm -> Int
2424getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2427-- Return all names, free or globally bound, in the given term.
2429allNamesIn :: PTerm -> [Name]
2430allNamesIn tm = nub $ ni 0 [] tm
2431 where -- TODO THINK added niTacImp, but is it right?
2432 ni 0 env (PRef _ _ n)
2433 | not (n `elem` env) = [n]
2434 ni 0 env (PPatvar _ n) = [n]
2435 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2436 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2437 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2438 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2439 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2440 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2441 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2442 ni 0 env (PHidden tm) = ni 0 env tm
2443 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2444 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2445 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2446 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2447 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2448 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2449 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2450 ni 0 env (PUnifyLog tm) = ni 0 env tm
2451 ni 0 env (PDisamb _ tm) = ni 0 env tm
2452 ni 0 env (PNoImplicits tm) = ni 0 env tm
2454 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2455 ni i env (PUnquote tm) = ni (i - 1) env tm
2456 ni i env tm = concatMap (ni i env) (children tm)
2458 niTacImp i env (TacImp _ _ scr) = ni i env scr
2462-- Return all names defined in binders in the given term
2463boundNamesIn :: PTerm -> [Name]
2464boundNamesIn tm = S.toList (ni 0 S.empty tm)
2465 where -- TODO THINK Added niTacImp, but is it right?
2466 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2467 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2468 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2469 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2470 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2471 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2472 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2473 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2474 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2475 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2476 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2477 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2478 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2479 ni 0 set (PAlternative ns a as) = niTms 0 set as
2480 ni 0 set (PHidden tm) = ni 0 set tm
2481 ni 0 set (PUnifyLog tm) = ni 0 set tm
2482 ni 0 set (PDisamb _ tm) = ni 0 set tm
2483 ni 0 set (PNoImplicits tm) = ni 0 set tm
2485 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2486 ni i set (PUnquote tm) = ni (i - 1) set tm
2488 ni i set tm = foldr (S.union . ni i set) set (children tm)
2490 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2491 niTms i set [] = set
2492 niTms i set (x : xs) = niTms i (ni i set x) xs
2494 niTacImp i set (TacImp _ _ scr) = ni i set scr
2495 niTacImp i set _ = set
2497-- Return names which are valid implicits in the given term (type).
2498implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2499implicitNamesIn uvars ist tm
2500 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2503 addImp n = do (imps, fns) <- get
2505 addFn n = do (imps, fns) <- get
2509 notCAF (PExp _ _ _ _ : _) = True
2510 notCAF (_ : xs) = notCAF xs
2512 notHidden (n, _) = case getAccessibility n of
2518 = case lookupDefAccExact n False (tt_ctxt ist) of
2522 ni 0 env (PRef _ _ n@(NS _ _))
2523 | not (n `elem` env)
2524 -- Never implicitly bind if there's a namespace
2526 ni 0 env (PRef _ _ n)
2527 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2528 ni 0 env (PApp _ f@(PRef _ _ n) as)
2529 | n `elem` uvars = do ni 0 env f
2530 mapM_ (ni 0 env . getTm) as
2531 | otherwise = do case lookupTy n (tt_ctxt ist) of
2534 mapM_ (ni 0 env . getTm) as
2535 ni 0 env (PApp _ f as) = do ni 0 env f
2536 mapM_ (ni 0 env . getTm) as
2537 ni 0 env (PAppBind _ f as) = do ni 0 env f
2538 mapM_ (ni 0 env . getTm) as
2539 ni 0 env (PCase _ c os) = do ni 0 env c
2540 -- names in 'os', not counting the names bound in the cases
2541 mapM_ (ni 0 env . snd) os
2544 mapM_ (ni 0 env . fst) os
2546 put (nub imps \\ nub impsfst, fns)
2547 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2548 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2549 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2550 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2551 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2552 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2553 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2554 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2557 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2558 ni 0 env (PHidden tm) = ni 0 env tm
2559 ni 0 env (PUnifyLog tm) = ni 0 env tm
2560 ni 0 env (PDisamb _ tm) = ni 0 env tm
2561 ni 0 env (PNoImplicits tm) = ni 0 env tm
2563 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2564 maybe (return ()) (ni i env) ty
2565 ni i env (PUnquote tm) = ni (i - 1) env tm
2567 ni i env tm = mapM_ (ni i env) (children tm)
2569-- Return names which are free in the given term.
2570namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2571namesIn uvars ist tm = nub $ ni 0 [] tm
2573 ni 0 env (PRef _ _ n)
2574 | not (n `elem` env)
2575 = case lookupTy n (tt_ctxt ist) of
2577 _ -> [n | n `elem` (map fst uvars)]
2578 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2579 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2580 ni 0 env (PCase _ c os) = ni 0 env c ++
2581 -- names in 'os', not counting the names bound in the cases
2582 (nub (concatMap (ni 0 env . snd) os)
2583 \\ nub (concatMap (ni 0 env . fst) os))
2584 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2585 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2586 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2587 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2588 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2589 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2590 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2591 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2592 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2593 ni 0 env (PHidden tm) = ni 0 env tm
2594 ni 0 env (PUnifyLog tm) = ni 0 env tm
2595 ni 0 env (PDisamb _ tm) = ni 0 env tm
2596 ni 0 env (PNoImplicits tm) = ni 0 env tm
2598 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2599 ni i env (PUnquote tm) = ni (i - 1) env tm
2601 ni i env tm = concatMap (ni i env) (children tm)
2603 niTacImp i env (TacImp _ _ scr) = ni i env scr
2606-- Return which of the given names are used in the given term.
2608usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2609usedNamesIn vars ist tm = nub $ ni 0 [] tm
2610 where -- TODO THINK added niTacImp, but is it right?
2611 ni 0 env (PRef _ _ n)
2612 | n `elem` vars && not (n `elem` env)
2613 = case lookupDefExact n (tt_ctxt ist) of
2616 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2617 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2618 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2619 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2620 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2621 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2622 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2623 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2624 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2625 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2626 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2627 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2628 ni 0 env (PHidden tm) = ni 0 env tm
2629 ni 0 env (PUnifyLog tm) = ni 0 env tm
2630 ni 0 env (PDisamb _ tm) = ni 0 env tm
2631 ni 0 env (PNoImplicits tm) = ni 0 env tm
2633 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2634 ni i env (PUnquote tm) = ni (i - 1) env tm
2636 ni i env tm = concatMap (ni i env) (children tm)
2638 niTacImp i env (TacImp _ _ scr) = ni i env scr
2641-- Return the list of inaccessible (= dotted) positions for a name.
2642getErasureInfo :: IState -> Name -> [Int]
2643getErasureInfo ist n =
2644 case lookupCtxtExact n (idris_optimisation ist) of
2645 Just (Optimise inacc detagg) -> 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