2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
8{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,
9 FlexibleInstances, MultiParamTypeClasses, PatternGuards,
10 TypeSynonymInstances #-}
12module Idris.AbsSyntaxTree where
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
18import Idris.Core.Typecheck
19import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
25import Prelude hiding ((<$>))
27import Control.Applicative ((<|>))
28import qualified Control.Monad.Trans.Class as Trans (lift)
29import Control.Monad.Trans.Except
30import Control.Monad.Trans.State.Strict
32import Data.Data (Data)
34import Data.Foldable (Foldable)
35import Data.Function (on)
36import Data.Generics.Uniplate.Data (children, universe)
37import Data.List hiding (group)
38import qualified Data.Map.Strict as M
39import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
40import qualified Data.Set as S
41import qualified Data.Text as T
42import Data.Traversable (Traversable)
44import Data.Word (Word)
46import GHC.Generics (Generic)
47import Network.Socket (PortNumber)
48import System.Console.Haskeline
50import Text.PrettyPrint.Annotated.Leijen
52data ElabWhat = ETypes | EDefns | EAll
55-- | Data to pass to recursively called elaborators; e.g. for where blocks,
56-- paramaterised declarations, etc.
58-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
59-- so that we can have mutually recursive elaborators in separate modules without
60-- having to muck about with cyclic modules.
61data ElabInfo = EInfo {
62 params :: [(Name, PTerm)]
63 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
64 , liftname :: Name -> Name
65 , namespace :: [String]
67 , constraintNS :: String -- ^ filename for adding to constraint variables
70 -- | We may, recursively, collect transformations to do on the rhs,
71 -- e.g. rewriting recursive calls to functions defined by 'with'
72 , rhs_trans :: PTerm -> PTerm
73 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
77toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")
79toplevelWith :: String -> ElabInfo
80toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")
82eInfoNames :: ElabInfo -> [Name]
83eInfoNames info = map fst (params info) ++ M.keys (inblock info)
85data IOption = IOption {
87 , opt_logcats :: [LogCat] -- ^ List of logging categories.
88 , opt_typecase :: Bool
89 , opt_typeintype :: Bool
90 , opt_coverage :: Bool
91 , opt_showimp :: Bool -- ^ show implicits
92 , opt_errContext :: Bool
95 , opt_nobanner :: Bool
97 , opt_codegen :: Codegen
98 , opt_outputTy :: OutputType
99 , opt_ibcsubdir :: FilePath
100 , opt_importdirs :: [FilePath]
101 , opt_sourcedirs :: [FilePath]
102 , opt_triple :: String
104 , opt_cmdline :: [Opt] -- ^ remember whole command line
105 , opt_origerr :: Bool
106 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
107 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
108 , opt_optimise :: [Optimisation]
109 , opt_printdepth :: Maybe Int
110 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
111 , opt_desugarnats :: Bool
112 , opt_autoimpls :: Bool
113 } deriving (Show, Eq, Generic)
115defaultOpts = IOption { opt_logLevel = 0
117 , opt_typecase = False
118 , opt_typeintype = False
119 , opt_coverage = True
120 , opt_showimp = False
121 , opt_errContext = False
124 , opt_nobanner = False
126 , opt_codegen = Via IBCFormat "c"
127 , opt_outputTy = Executable
129 , opt_importdirs = []
130 , opt_sourcedirs = []
134 , opt_origerr = False
135 , opt_autoSolve = True
136 , opt_autoImport = []
137 , opt_optimise = defaultOptimise
138 , opt_printdepth = Just 5000
139 , opt_evaltypes = True
140 , opt_desugarnats = False
141 , opt_autoimpls = True
144data PPOption = PPOption {
145 ppopt_impl :: Bool -- ^ whether to show implicits
146 , ppopt_desugarnats :: Bool
147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
148 , ppopt_depth :: Maybe Int
151data Optimisation = PETransform -- ^ partial eval and associated transforms
152 deriving (Show, Eq, Generic)
154defaultOptimise = [PETransform]
156-- | Pretty printing options with default verbosity.
157defaultPPOption :: PPOption
158defaultPPOption = PPOption {
160 , ppopt_desugarnats = False
161 , ppopt_pinames = False
162 , ppopt_depth = Nothing
165-- | Pretty printing options with the most verbosity.
166verbosePPOption :: PPOption
167verbosePPOption = PPOption {
169 , ppopt_desugarnats = True
170 , ppopt_pinames = True
171 , ppopt_depth = Nothing
174-- | Get pretty printing options from the big options record.
175ppOption :: IOption -> PPOption
176ppOption opt = PPOption {
177 ppopt_impl = opt_showimp opt
178 , ppopt_pinames = False
179 , ppopt_depth = opt_printdepth opt
180 , ppopt_desugarnats = opt_desugarnats opt
183-- | Get pretty printing options from an idris state record.
184ppOptionIst :: IState -> PPOption
185ppOptionIst = ppOption . idris_options
187data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
188 | DSLNotation | ElabReflection | FCReflection
189 deriving (Show, Eq, Read, Ord, Generic)
191-- | The output mode in use
192data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
193 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
196-- | How wide is the console?
197data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
198 | ColsWide Int -- ^ Manually specified - must be positive
199 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
200 deriving (Show, Eq, Generic)
202-- | If a function has no totality annotation, what do we assume?
203data DefaultTotality = DefaultCheckingTotal -- ^ Total
204 | DefaultCheckingPartial -- ^ Partial
205 | DefaultCheckingCovering -- ^Total coverage, but may diverge
206 deriving (Show, Eq, Generic)
208-- | The global state used in the Idris monad
209data IState = IState {
210 tt_ctxt :: Context -- ^ All the currently defined names and their terms
211 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
212 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
213 , idris_implicits :: Ctxt [PArg]
214 , idris_statics :: Ctxt [Bool]
215 , idris_interfaces :: Ctxt InterfaceInfo
216 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
217 , idris_records :: Ctxt RecordInfo
218 , idris_dsls :: Ctxt DSL
219 , idris_optimisation :: Ctxt OptInfo
220 , idris_datatypes :: Ctxt TypeInfo
221 , idris_namehints :: Ctxt [Name]
223 -- | list of lhs/rhs, and a list of missing clauses. These are not
225 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
226 , idris_flags :: Ctxt [FnOpt]
227 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
228 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
230 -- | module documentation is saved in a special MN so the context
231 -- mechanism can be used for disambiguation.
232 , idris_moduledocs :: Ctxt (Docstring DocTerm)
233 , idris_tyinfodata :: Ctxt TIData
234 , idris_fninfo :: Ctxt FnInfo
235 , idris_transforms :: Ctxt [(Term, Term)]
236 , idris_autohints :: Ctxt [Name]
237 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
238 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
239 , idris_totcheckfail :: [(FC, String)]
240 , idris_options :: IOption
242 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
244 -- | The currently defined but not proven metavariables. The Int is
245 -- the number of vars to display as a context, the Maybe Name is its
246 -- top-level function, the [Name] is the list of local variables
247 -- available for proof search and the Bools are whether :p is
248 -- allowed, and whether the variable is definable at all
249 -- (Metavariables are not definable if they are applied in a term
250 -- which still has hole bindings)
251 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
252 , idris_coercions :: [Name]
253 , idris_errRev :: [(Term, Term)]
254 , syntax_rules :: SyntaxRules
255 , syntax_keywords :: [String]
256 , imported :: [FilePath] -- ^ The imported modules
257 , idris_scprims :: [(Name, (Int, PrimFn))]
258 , idris_objs :: [(Codegen, FilePath)]
259 , idris_libs :: [(Codegen, String)]
260 , idris_cgflags :: [(Codegen, String)]
261 , idris_hdrs :: [(Codegen, String)]
262 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
263 , proof_list :: [(Name, (Bool, [String]))]
264 , errSpan :: Maybe FC
265 , parserWarnings :: [(FC, Err)]
266 , lastParse :: Maybe Name
267 , indent_stack :: [Int]
268 , brace_stack :: [Maybe Int]
269 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
270 , idris_parsedSpan :: Maybe FC
271 , hide_list :: Ctxt Accessibility
272 , default_access :: Accessibility
273 , default_total :: DefaultTotality
274 , ibc_write :: [IBCWrite]
275 , compiled_so :: Maybe String
276 , idris_dynamic_libs :: [DynamicLib]
277 , idris_language_extensions :: [LanguageExt]
278 , idris_outputmode :: OutputMode
279 , idris_colourRepl :: Bool
280 , idris_colourTheme :: ColourTheme
281 , idris_errorhandlers :: [Name] -- ^ Global error handlers
282 , idris_nameIdx :: (Int, Ctxt (Int, Name))
283 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
284 , module_aliases :: M.Map [T.Text] [T.Text]
285 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
286 , idris_postulates :: S.Set Name
287 , idris_externs :: S.Set (Name, Int)
288 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
289 , idris_whocalls :: Maybe (M.Map Name [Name])
290 , idris_callswho :: Maybe (M.Map Name [Name])
292 -- | List of names that were defined in the repl, and can be re-/un-defined
293 , idris_repl_defs :: [Name]
295 -- | Stack of names currently being elaborated, Bool set if it's an
296 -- implementation (implementations appear twice; also as a funtion name)
297 , elab_stack :: [(Name, Bool)]
300 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
301 , idris_exports :: [Name] -- ^ Functions with ExportList
302 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
303 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
304 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
305 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
306 , idris_ttstats :: M.Map Term (Int, Term)
307 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
311-- Required for parsers library, and therefore trifecta
312instance Show IState where
313 show = const "{internal state}"
315data SizeChange = Smaller | Same | Bigger | Unknown
316 deriving (Show, Eq, Generic)
318deriving instance Binary SizeChange
321type SCGEntry = (Name, [Maybe (Int, SizeChange)])
322type UsageReason = (Name, Int) -- fn_name, its_arg_number
324data CGInfo = CGInfo {
325 calls :: [Name] -- Immediate calls
326 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
328 , usedpos :: [(Int, [UsageReason])]
329 } deriving (Show, Generic)
331deriving instance Binary CGInfo
334primDefs = [ sUN "unsafePerformPrimIO"
335 , sUN "mkLazyForeignPrim"
336 , sUN "mkForeignPrim"
338 , sUN "assert_unreachable"
342-- information that needs writing for the current module's .ibc file
343data IBCWrite = IBCFix FixDecl
348 | IBCImplementation Bool Bool Name Name
355 | IBCImport (Bool, FilePath) -- ^ True = import public
356 | IBCImportDir FilePath
357 | IBCSourceDir FilePath
358 | IBCObj Codegen FilePath
359 | IBCLib Codegen String
360 | IBCCGFlag Codegen String
362 | IBCHeader Codegen String
363 | IBCAccess Name Accessibility
364 | IBCMetaInformation Name MetaInformation
365 | IBCTotal Name Totality
366 | IBCInjective Name Injectivity
368 | IBCFnInfo Name FnInfo
369 | IBCTrans Name (Term, Term)
370 | IBCErrRev (Term, Term)
374 | IBCDef Name -- ^ The main context.
375 | IBCNameHint (Name, Name)
376 | IBCLineApp FilePath Int PTerm
377 | IBCErrorHandler Name
378 | IBCFunctionErrorHandler Name Name Name
380 | IBCExtern (Name, Int)
381 | IBCTotCheckErr FC String
383 | IBCModDocs Name -- ^ The name is the special name used to track module docs
384 | IBCUsage (Name, Int)
386 | IBCAutoHint Name Name
387 | IBCDeprecate Name String
388 | IBCFragile Name String
389 | IBCConstraint FC UConstraint
390 deriving (Show, Generic)
392-- | The initial state for the compiler
394idrisInit = IState initContext S.empty []
395 emptyContext emptyContext emptyContext [] emptyContext
396 emptyContext emptyContext emptyContext emptyContext
397 emptyContext emptyContext emptyContext emptyContext
398 emptyContext emptyContext emptyContext emptyContext
400 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
401 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
402 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
403 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
404 emptyContext S.empty M.empty emptyContext
407-- | The monad for the main REPL - reading and processing files and
408-- updating global state (hence the IO inner monad).
411-- type Idris = WriterT [Either String (IO ())] (State IState a))
414type Idris = StateT IState (ExceptT Err IO)
416catchError :: Idris a -> (Err -> Idris a) -> Idris a
417catchError = liftCatch catchE
419throwError :: Err -> Idris a
420throwError = Trans.lift . throwE
422-- Commands in the REPL
424data Codegen = Via IRFormat String
426 deriving (Show, Eq, Generic)
428data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
430data HowMuchDocs = FullDocs | OverviewDocs
432data OutputFmt = HTMLOutput | LaTeXOutput
434-- | Recognised logging categories for the Idris compiler.
436-- @TODO add in sub categories.
443 deriving (Show, Eq, Ord, Generic)
445strLogCat :: LogCat -> String
446strLogCat IParse = "parser"
447strLogCat IElab = "elab"
448strLogCat ICodeGen = "codegen"
449strLogCat IErasure = "erasure"
450strLogCat ICoverage = "coverage"
451strLogCat IIBC = "ibc"
453codegenCats :: [LogCat]
454codegenCats = [ICodeGen]
456parserCats :: [LogCat]
462loggingCatsStr :: String
463loggingCatsStr = unlines
466 , (strLogCat ICodeGen)
467 , (strLogCat IErasure)
468 , (strLogCat ICoverage)
473data ElabShellCmd = EQED
481 | EDocStr (Either Name Const)
484data Opt = Filename String
499 | NoBuiltins -- only for the really primitive stuff!
516 | Port REPLPort -- ^ REPL TCP port
525 | PkgDocBuild String -- IdrisDoc
526 | PkgDocInstall String
536 | OutputTy OutputType
537 | Extension LanguageExt
538 | InterpretScript String
540 | TargetTriple String
543 | AddOpt Optimisation
544 | RemoveOpt Optimisation
547 | AutoWidth -- ^ Automatically adjust terminal width
548 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
549 | UseConsoleWidth ConsoleWidth
552 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
553 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
554 deriving (Show, Eq, Generic)
556data REPLPort = DontListen | ListenPort PortNumber
557 deriving (Eq, Generic, Show)
559-- Parsed declarations
561data Fixity = Infixl { prec :: Int }
562 | Infixr { prec :: Int }
563 | InfixN { prec :: Int }
564 | PrefixN { prec :: Int }
565 deriving (Eq, Generic)
567deriving instance Binary Fixity
570instance Show Fixity where
571 show (Infixl i) = "infixl " ++ show i
572 show (Infixr i) = "infixr " ++ show i
573 show (InfixN i) = "infix " ++ show i
574 show (PrefixN i) = "prefix " ++ show i
576data FixDecl = Fix Fixity String
577 deriving (Eq, Generic)
579instance Show FixDecl where
580 show (Fix f s) = show f ++ " " ++ s
583deriving instance Binary FixDecl
586instance Ord FixDecl where
587 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
590data Static = Static | Dynamic
591 deriving (Show, Eq, Ord, Data, Generic, Typeable)
593deriving instance Binary Static
596-- ^ Mark bindings with their explicitness, and laziness
597data Plicity = Imp { pargopts :: [ArgOpt]
600 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
601 , pinsource :: Bool -- ^ Explicitly written in source
603 | Exp { pargopts :: [ArgOpt]
605 , pparam :: Bool -- ^ this is a param (rather than index)
607 | Constraint { pargopts :: [ArgOpt]
610 | TacImp { pargopts :: [ArgOpt]
614 deriving (Show, Eq, Ord, Data, Generic, Typeable)
617deriving instance Binary Plicity
620is_scoped :: Plicity -> Maybe ImplicitInfo
621is_scoped (Imp _ _ _ s _) = s
625impl = Imp [] Dynamic False (Just (Impl False True False)) False
626-- Machine generated top level implicit
627impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False
630forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False
631forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False
633expl = Exp [] Dynamic False
634expl_param = Exp [] Dynamic True
636constraint = Constraint [] Static
638tacimpl t = TacImp [] Dynamic t
640data FnOpt = Inlinable -- ^ always evaluate when simplifying
641 | TotalFn | PartialFn | CoveringFn
642 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
645 -- | interface dictionary, eval only when a function
646 -- argument, and further evaluation results.
648 | OverlappingDictionary -- ^ Interface dictionary which may overlap
649 | Implicit -- ^ implicit coercion
650 | NoImplicit -- ^ do not apply implicit coercions
651 | CExport String -- ^ export, with a C name
652 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
653 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
654 | Reflection -- ^ a reflecting function, compile-time only
655 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
656 | UnfoldIface Name [Name]
657 -- ^ Unfold given interface name in the definition, the
658 -- top level methods, and anything which has
659 -- the interface name as an argument. This is to unfold
660 -- things for termination checking, as interfaces will otherwise
662 | Constructor -- ^ Data constructor type
663 | AutoHint -- ^ use in auto implicit search
664 | PEGenerated -- ^ generated by partial evaluator
665 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
666 deriving (Show, Eq, Generic)
668deriving instance Binary FnOpt
673inlinable :: FnOpts -> Bool
674inlinable = elem Inlinable
676dictionary :: FnOpts -> Bool
677dictionary = elem Dictionary
680-- | Type provider - what to provide
681data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
682 | ProvPostulate t -- ^ goal type must be Type, so only term
683 deriving (Show, Eq, Functor, Generic)
685type ProvideWhat = ProvideWhat' PTerm
687-- | Top-level declarations such as compiler directives, definitions,
688-- datatypes and interfaces.
690 -- | Fixity declaration
691 = PFix FC Fixity [String]
692 -- | Type declaration (last FC is precise name location)
693 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
694 -- | Postulate, second FC is precise name location
695 | PPostulate Bool -- external def if true
696 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
698 | PClauses FC FnOpts Name [PClause' t]
699 -- | Top level constant
701 -- | Data declaration.
702 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
704 | PParams FC [(Name, t)] [PDecl' t]
705 -- | Open block/declaration
706 | POpenInterfaces FC [Name] [PDecl' t]
707 -- | New namespace, where FC is accurate location of the namespace
709 | PNamespace String FC [PDecl' t]
711 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
713 FC -- Record name precise location
714 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
715 [(Name, Docstring (Either Err t))] -- Param Docs
716 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
717 (Maybe (Name, FC)) -- Optional constructor name and location
718 (Docstring (Either Err t)) -- Constructor doc
719 SyntaxInfo -- Constructor SyntaxInfo
721 -- | Interface: arguments are documentation, syntax info, source
722 -- location, constraints, interface name, interface name location,
723 -- parameters, method declarations, optional constructor name
724 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
725 [(Name, t)] -- constraints
726 Name -- interface name
727 FC -- accurate location of interface name
728 [(Name, FC, t)] -- parameters and precise locations
729 [(Name, Docstring (Either Err t))] -- parameter docstrings
730 [(Name, FC)] -- determining parameters and precise locations
731 [PDecl' t] -- declarations
732 (Maybe (Name, FC)) -- implementation constructor name and location
733 (Docstring (Either Err t)) -- implementation constructor docs
735 -- | Implementation declaration: arguments are documentation, syntax
736 -- info, source location, constraints, interface name, parameters, full
737 -- Implementation type, optional explicit name, and definitions
738 | PImplementation (Docstring (Either Err t)) -- Implementation docs
739 [(Name, Docstring (Either Err t))] -- Parameter docs
741 FC [(Name, t)] -- constraints
742 [Name] -- parent dictionaries to search for constraints
746 FC -- precise location of interface
748 [(Name, t)] -- Extra names in scope in the body
749 t -- full Implementation type
750 (Maybe Name) -- explicit name
752 | PDSL Name (DSL' t) -- ^ DSL declaration
753 | PSyntax FC Syntax -- ^ Syntax definition
754 | PMutual FC [PDecl' t] -- ^ Mutual block
755 | PDirective Directive -- ^ Compiler directive.
757 -- | Type provider. The first t is the type, the second is the
758 -- term. The second FC is precise highlighting location.
759 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
761 -- | Source-to-source transformation rule. If bool is True, lhs and
762 -- rhs must be convertible.
763 | PTransform FC Bool t t
765 -- | FC is decl-level, for errors, and Strings represent the
767 | PRunElabDecl FC t [String]
768 deriving (Functor, Generic)
770deriving instance Binary PDecl'
773-- | The set of source directives
774data Directive = DLib Codegen String
775 | DLink Codegen String
776 | DFlag Codegen String
777 | DInclude Codegen String
782 | DSetTotal Name -- assert totality after checking
783 | DAccess Accessibility
784 | DDefault DefaultTotality
786 | DDynamicLibs [String]
787 | DNameHint Name FC [(Name, FC)]
788 | DErrorHandlers Name FC Name FC [(Name, FC)]
789 | DLanguage LanguageExt
790 | DDeprecate Name String
791 | DFragile Name String
792 | DAutoImplicits Bool
796-- | A set of instructions for things that need to happen in IState
797-- after a term elaboration when there's been reflected elaboration.
798data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
799 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
800 | RAddImplementation Name Name
801 | RDatatypeDeclInstrs Name [PArg]
802 -- | Datatype, constructors
803 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
806-- | For elaborator state
807data EState = EState {
808 case_decls :: [(Name, PDecl)]
809 , delayed_elab :: [(Int, Elab' EState ())]
810 , new_tyDecls :: [RDeclInstructions]
811 , highlighting :: [(FC, OutputAnnotation)]
812 , auto_binds :: [Name] -- ^ names bound as auto implicits
813 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
817initEState = EState [] [] [] [] [] []
819type ElabD a = Elab' EState a
821highlightSource :: FC -> OutputAnnotation -> ElabD ()
822highlightSource fc annot =
823 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
825-- | One clause of a top-level definition. Term arguments to constructors are:
827-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
829-- 2. The list of extra 'with' patterns
831-- 3. The right-hand side
833-- 4. The where block (PDecl' t)
835data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
836 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
837 | PClauseR FC [t] t [PDecl' t]
838 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
839 deriving (Functor, Generic)
841deriving instance Binary PClause'
846 -- | Data declaration
847 PDatadecl { d_name :: Name -- ^ The name of the datatype
848 , d_name_fc :: FC -- ^ The precise location of the type constructor name
849 , d_tcon :: t -- ^ Type constructor
850 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
852 -- | "Placeholder" for data whose constructors are defined later
853 | PLaterdecl { d_name :: Name
856 } deriving (Functor, Generic)
858-- | Transform the FCs in a PData and its associated terms. The first
859-- function transforms the general-purpose FCs, and the second
860-- transforms those that are used for semantic source highlighting, so
861-- they can be treated specially.
862mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
863mapPDataFC f g (PDatadecl n nfc tycon ctors) =
864 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
865 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
866 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
867mapPDataFC f g (PLaterdecl n nfc tycon) =
868 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
870deriving instance Binary PData'
873-- Handy to get a free function for applying PTerm -> PTerm functions
874-- across a program, by deriving Functor
876type PDecl = PDecl' PTerm
877type PData = PData' PTerm
878type PClause = PClause' PTerm
880-- | Transform the FCs in a PTerm. The first function transforms the
881-- general-purpose FCs, and the second transforms those that are used
882-- for semantic source highlighting, so they can be treated specially.
883mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
884mapPDeclFC f g (PFix fc fixity ops) =
885 PFix (f fc) fixity ops
886mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
887 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
888mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
889 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
891mapPDeclFC f g (PClauses fc opts n clauses) =
892 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
893mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
894mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
895 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
896mapPDeclFC f g (PParams fc params decls) =
898 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
899 (map (mapPDeclFC f g) decls)
900mapPDeclFC f g (POpenInterfaces fc ifs decls) =
901 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
902mapPDeclFC f g (PNamespace ns fc decls) =
903 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
904mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
905 PRecord doc syn (f fc) opts n (g nfc)
906 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
908 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
909 plic, mapPTermFC f g ty, fdoc))
911 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
914mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
915 PInterface doc syn (f fc)
916 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
917 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
918 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
919 (map (mapPDeclFC f g) body)
920 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
922mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
923 PImplementation doc paramDocs syn (f fc)
924 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
925 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
926 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
927 (mapPTermFC f g implTy)
929 (map (mapPDeclFC f g) body)
930mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
931mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
933 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
934 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
935mapPDeclFC f g (PMutual fc decls) =
936 PMutual (f fc) (map (mapPDeclFC f g) decls)
937mapPDeclFC f g (PDirective d) =
940 DNameHint n nfc ns ->
941 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
942 DErrorHandlers n nfc n' nfc' ns ->
943 DErrorHandlers n (g nfc) n' (g nfc') $
944 map (\(an, anfc) -> (an, g anfc)) ns
945mapPDeclFC f g (PProvider doc syn fc nfc what n) =
946 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
947mapPDeclFC f g (PTransform fc safe l r) =
948 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
949mapPDeclFC f g (PRunElabDecl fc script ns) =
950 PRunElabDecl (f fc) (mapPTermFC f g script) ns
952-- | Get all the names declared in a declaration
953declared :: PDecl -> [Name]
954declared (PFix _ _ _) = []
955declared (PTy _ _ _ _ _ n fc t) = [n]
956declared (PPostulate _ _ _ _ _ _ n t) = [n]
957declared (PClauses _ _ n _) = [] -- not a declaration
958declared (PCAF _ n _) = [n]
959declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
960 where fstt (_, _, a, _, _, _, _) = a
961declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
962declared (PParams _ _ ds) = concatMap declared ds
963declared (POpenInterfaces _ _ ds) = concatMap declared ds
964declared (PNamespace _ _ ds) = concatMap declared ds
965declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
966declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
967declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
971declared (PDSL n _) = [n]
972declared (PSyntax _ _) = []
973declared (PMutual _ ds) = concatMap declared ds
974declared (PDirective _) = []
977-- get the names declared, not counting nested parameter blocks
978tldeclared :: PDecl -> [Name]
979tldeclared (PFix _ _ _) = []
980tldeclared (PTy _ _ _ _ _ n _ t) = [n]
981tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
982tldeclared (PClauses _ _ n _) = [] -- not a declaration
983tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
984tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
985 where fstt (_, _, a, _, _, _, _) = a
986tldeclared (PParams _ _ ds) = []
987tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
988tldeclared (PMutual _ ds) = concatMap tldeclared ds
989tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
990tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
991tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
997defined :: PDecl -> [Name]
998defined (PFix _ _ _) = []
999defined (PTy _ _ _ _ _ n _ t) = []
1000defined (PPostulate _ _ _ _ _ _ n t) = []
1001defined (PClauses _ _ n _) = [n] -- not a declaration
1002defined (PCAF _ n _) = [n]
1003defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1004 where fstt (_, _, a, _, _, _, _) = a
1005defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1006defined (PParams _ _ ds) = concatMap defined ds
1007defined (POpenInterfaces _ _ ds) = concatMap defined ds
1008defined (PNamespace _ _ ds) = concatMap defined ds
1009defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1010defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1011defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1015defined (PDSL n _) = [n]
1016defined (PSyntax _ _) = []
1017defined (PMutual _ ds) = concatMap defined ds
1018defined (PDirective _) = []
1021updateN :: [(Name, Name)] -> Name -> Name
1022updateN ns n | Just n' <- lookup n ns = n'
1025updateNs :: [(Name, Name)] -> PTerm -> PTerm
1027updateNs ns t = mapPT updateRef t
1028 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1031-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1032-- updateDNs [] t = t
1033-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1034-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1035-- where updateCNs ns (PClause n l ts r ds)
1036-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1037-- (map (fmap (updateNs ns)) ts)
1038-- (fmap (updateNs ns) r)
1039-- (map (updateDNs ns) ds)
1040-- updateDNs ns c = c
1042data PunInfo = IsType
1045 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1047-- | High level language terms
1048data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1049 -- high-level language
1051 -- ^ A reference to a variable. The FC is its precise
1052 -- source location for highlighting. The list of FCs is a
1053 -- collection of additional highlighting locations.
1054 | PInferRef FC [FC] Name -- ^ A name to be defined later
1055 | PPatvar FC Name -- ^ A pattern variable
1056 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1057 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1058 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1059 | PTyped PTerm PTerm -- ^ Term with explicit type
1060 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1061 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1062 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1063 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1064 | PMatchApp FC Name -- ^ Make an application by type matching
1065 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1066 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1067 | PTrue FC PunInfo -- ^ Unit type..?
1068 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1069 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1070 -- ^ "rewrite" syntax, with optional rewriting function and
1071 -- optional result type
1072 | PPair FC [FC] PunInfo PTerm PTerm
1073 -- ^ A pair (a, b) and whether it's a product type or a
1074 -- pair (solved by elaboration). The list of FCs is its
1076 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1077 -- ^ A dependent pair (tm : a ** b) and whether it's a
1078 -- sigma type or a pair that inhabits one (solved by
1079 -- elaboration). The [FC] is its punctuation.
1080 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1081 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1082 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1083 | PType FC -- ^ 'Type' type
1084 | PUniverse FC Universe -- ^ Some universe
1085 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1086 | PConstant FC Const -- ^ Builtin types
1087 | Placeholder -- ^ Underscore
1088 | PDoBlock [PDo] -- ^ Do notation
1089 | PIdiom FC PTerm -- ^ Idiom brackets
1090 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1091 | PProof [PTactic] -- ^ Proof script
1092 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1093 | PElabError Err -- ^ Error to report on elaboration
1094 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1095 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1096 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1097 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1098 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1099 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1100 | PUnquote PTerm -- ^ ~Term
1101 | PQuoteName Name Bool FC
1102 -- ^ `{n} where the FC is the precise highlighting for
1103 -- the name in particular. If the Bool is False, then
1104 -- it's `{{n}} and the name won't be resolved.
1105 | PRunElab FC PTerm [String]
1106 -- ^ %runElab tm - New-style proof script. Args are
1107 -- location, script, enclosing namespace.
1108 | PConstSugar FC PTerm
1109 -- ^ A desugared constant. The FC is a precise source
1110 -- location that will be used to highlight it later.
1111 deriving (Eq, Ord, Data, Typeable, Generic)
1113data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1116 deriving (Eq, Ord, Data, Generic, Typeable)
1118-- | Transform the FCs in a PTerm. The first function transforms the
1119-- general-purpose FCs, and the second transforms those that are used
1120-- for semantic source highlighting, so they can be treated specially.
1121mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1122mapPTermFC f g (PQuote q) = PQuote q
1123mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1124mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1125mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1126mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1127mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1128mapPTermFC 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)
1129mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1130mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1131mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1132mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1133mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1134mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1135mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1136mapPTermFC 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)
1137mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1138mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1139mapPTermFC 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)
1140mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1141mapPTermFC 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)
1142mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1143mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1144mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1145mapPTermFC f g (PType fc) = PType (f fc)
1146mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1147mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1148mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1149mapPTermFC f g Placeholder = Placeholder
1150mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1151 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1152 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1153 mapPDoFC (DoBindP fc t1 t2 alts) =
1154 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1155 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1156 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1157mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1158mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1159mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1160mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1161mapPTermFC f g (PElabError err) = PElabError err
1162mapPTermFC f g PImpossible = PImpossible
1163mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1164mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1165mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1166mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1167mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1168mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1169mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1170mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1171mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1174dg instance Binary PTerm
1177mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1178mapPT f t = f (mpt t) where
1179 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1180 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1181 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1182 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1183 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1184 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1185 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1186 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1187 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1188 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1189 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1190 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1191 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1192 mpt (PHidden t) = PHidden (mapPT f t)
1193 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1194 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1195 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1196 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1197 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1198 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1199 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1203data PTactic' t = Intro [Name] | Intros | Focus Name
1204 | Refine Name [Bool] | Rewrite t | DoUnify
1211 | LetTac Name t | LetTacTy Name t t
1212 | Exact t | Compute | Trivial | TCImplementation
1213 | ProofSearch Bool Bool Int (Maybe Name)
1214 [Name] -- allowed local names
1216 -- ^ the bool is whether to search recursively
1219 | ProofState | ProofTerm | Undo
1220 | Try (PTactic' t) (PTactic' t)
1221 | TSeq (PTactic' t) (PTactic' t)
1222 | ApplyTactic t -- see Language.Reflection module
1226 | GoalType String (PTactic' t)
1229 | TDocStr (Either Name Const)
1232 | TFail [ErrorReportPart]
1235 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1237deriving instance Binary PTactic'
1239instance Sized a => Sized (PTactic' a) where
1240 size (Intro nms) = 1 + size nms
1242 size (Focus nm) = 1 + size nm
1243 size (Refine nm bs) = 1 + size nm + length bs
1244 size (Rewrite t) = 1 + size t
1245 size (Induction t) = 1 + size t
1246 size (LetTac nm t) = 1 + size nm + size t
1247 size (Exact t) = 1 + size t
1255 size (Try l r) = 1 + size l + size r
1256 size (TSeq l r) = 1 + size l + size r
1257 size (ApplyTactic t) = 1 + size t
1258 size (Reflect t) = 1 + size t
1259 size (Fill t) = 1 + size t
1263 size (TFail ts) = 1 + size ts
1266 size (CaseTac x) = 1 + size x
1267 size (Equiv t) = 1 + size t
1268 size (Claim x y) = 1 + size x + size y
1270 size (MatchRefine x) = 1 + size x
1271 size (LetTacTy x y z) = 1 + size x + size y + size z
1272 size TCImplementation = 1
1274type PTactic = PTactic' PTerm
1276data PDo' t = DoExp FC t
1277 | DoBind FC Name FC t -- ^ second FC is precise name location
1278 | DoBindP FC t t [(t,t)]
1279 | DoLet FC Name FC t t -- ^ second FC is precise name location
1281 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1283deriving instance Binary PDo'
1286instance Sized a => Sized (PDo' a) where
1287 size (DoExp fc t) = 1 + size fc + size t
1288 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1289 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1290 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1291 size (DoLetP fc l r) = 1 + size fc + size l + size r
1293type PDo = PDo' PTerm
1295-- The priority gives a hint as to elaboration order. Best to elaborate
1296-- things early which will help give a more concrete type to other
1297-- variables, e.g. a before (interpTy a).
1299data PArg' t = PImp { priority :: Int
1300 , machine_inf :: Bool -- ^ true if the machine inferred it
1301 , argopts :: [ArgOpt]
1305 | PExp { priority :: Int
1306 , argopts :: [ArgOpt]
1310 | PConstraint { priority :: Int
1311 , argopts :: [ArgOpt]
1315 | PTacImplicit { priority :: Int
1316 , argopts :: [ArgOpt]
1321 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1323data ArgOpt = AlwaysShow
1327 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1329instance Sized a => Sized (PArg' a) where
1330 size (PImp p _ l nm trm) = 1 + size nm + size trm
1331 size (PExp p l nm trm) = 1 + size nm + size trm
1332 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1333 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1336deriving instance Binary PArg'
1339pimp n t mach = PImp 1 mach [] n t
1340pexp t = PExp 1 [] (sMN 0 "arg") t
1341pconst t = PConstraint 1 [] (sMN 0 "carg") t
1342ptacimp n s t = PTacImplicit 2 [] n s t
1344type PArg = PArg' PTerm
1346-- | Get the highest FC in a term, if one exists
1347highestFC :: PTerm -> Maybe FC
1348highestFC (PQuote _) = Nothing
1349highestFC (PRef fc _ _) = Just fc
1350highestFC (PInferRef fc _ _) = Just fc
1351highestFC (PPatvar fc _) = Just fc
1352highestFC (PLam fc _ _ _ _) = Just fc
1353highestFC (PPi _ _ _ _ _) = Nothing
1354highestFC (PLet fc _ _ _ _ _) = Just fc
1355highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1356highestFC (PApp fc _ _) = Just fc
1357highestFC (PAppBind fc _ _) = Just fc
1358highestFC (PMatchApp fc _) = Just fc
1359highestFC (PCase fc _ _) = Just fc
1360highestFC (PIfThenElse fc _ _ _) = Just fc
1361highestFC (PTrue fc _) = Just fc
1362highestFC (PResolveTC fc) = Just fc
1363highestFC (PRewrite fc _ _ _ _) = Just fc
1364highestFC (PPair fc _ _ _ _) = Just fc
1365highestFC (PDPair fc _ _ _ _ _) = Just fc
1366highestFC (PAs fc _ _) = Just fc
1367highestFC (PAlternative _ _ args) =
1368 case mapMaybe highestFC args of
1371highestFC (PHidden _) = Nothing
1372highestFC (PType fc) = Just fc
1373highestFC (PUniverse _ _) = Nothing
1374highestFC (PGoal fc _ _ _) = Just fc
1375highestFC (PConstant fc _) = Just fc
1376highestFC Placeholder = Nothing
1377highestFC (PDoBlock lines) =
1378 case map getDoFC lines of
1382 getDoFC (DoExp fc t) = fc
1383 getDoFC (DoBind fc nm nfc t) = fc
1384 getDoFC (DoBindP fc l r alts) = fc
1385 getDoFC (DoLet fc nm nfc l r) = fc
1386 getDoFC (DoLetP fc l r) = fc
1388highestFC (PIdiom fc _) = Just fc
1389highestFC (PMetavar fc _) = Just fc
1390highestFC (PProof _) = Nothing
1391highestFC (PTactics _) = Nothing
1392highestFC (PElabError _) = Nothing
1393highestFC PImpossible = Nothing
1394highestFC (PCoerced tm) = highestFC tm
1395highestFC (PDisamb _ opts) = highestFC opts
1396highestFC (PUnifyLog tm) = highestFC tm
1397highestFC (PNoImplicits tm) = highestFC tm
1398highestFC (PQuasiquote _ _) = Nothing
1399highestFC (PUnquote tm) = highestFC tm
1400highestFC (PQuoteName _ _ fc) = Just fc
1401highestFC (PRunElab fc _ _) = Just fc
1402highestFC (PConstSugar fc _) = Just fc
1403highestFC (PAppImpl t _) = highestFC t
1407data InterfaceInfo = CI {
1408 implementationCtorName :: Name
1409 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1410 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1411 , interface_default_super_interfaces :: [PDecl]
1412 , interface_impparams :: [Name]
1413 , interface_params :: [Name]
1414 , interface_constraints :: [PTerm]
1415 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1416 , interface_determiners :: [Int]
1417 } deriving (Show, Generic)
1419deriving instance Binary InterfaceInfo
1423data RecordInfo = RI {
1424 record_parameters :: [(Name,PTerm)]
1425 , record_constructor :: Name
1426 , record_projections :: [Name]
1427 } deriving (Show, Generic)
1429-- Type inference data
1431data TIData = TIPartial -- ^ a function with a partially defined type
1432 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1433 deriving (Show, Generic)
1435-- | Miscellaneous information about functions
1436data FnInfo = FnInfo { fn_params :: [Int] }
1437 deriving (Show, Generic)
1439deriving instance Binary FnInfo
1442data OptInfo = Optimise {
1443 inaccessible :: [(Int,Name)] -- includes names for error reporting
1444 , detaggable :: Bool
1445 , forceable :: [Int] -- argument positions which are forced by other values
1446 } deriving (Show, Generic)
1448deriving instance Binary OptInfo
1451-- | Syntactic sugar info
1456 , dsl_var :: Maybe t
1457 , index_first :: Maybe t
1458 , index_next :: Maybe t
1459 , dsl_lambda :: Maybe t
1460 , dsl_let :: Maybe t
1462 } deriving (Show, Functor, Generic)
1464deriving instance Binary DSL'
1467type DSL = DSL' PTerm
1469data SynContext = PatternSyntax
1472 deriving (Show, Generic)
1474deriving instance Binary SynContext
1477data Syntax = Rule [SSymbol] PTerm SynContext
1478 | DeclRule [SSymbol] [PDecl]
1479 deriving (Show, Generic)
1481syntaxNames :: Syntax -> [Name]
1482syntaxNames (Rule syms _ _) = mapMaybe ename syms
1483 where ename (Keyword n) = Just n
1485syntaxNames (DeclRule syms _) = mapMaybe ename syms
1486 where ename (Keyword n) = Just n
1489syntaxSymbols :: Syntax -> [SSymbol]
1490syntaxSymbols (Rule ss _ _) = ss
1491syntaxSymbols (DeclRule ss _) = ss
1493deriving instance Binary Syntax
1496data SSymbol = Keyword Name
1501 deriving (Show, Eq, Generic)
1505deriving instance Binary SSymbol
1508newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1511emptySyntaxRules :: SyntaxRules
1512emptySyntaxRules = SyntaxRules []
1514updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1515updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1517 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1522 ruleSort (s1:ss1) (s2:ss2) =
1523 case symCompare s1 s2 of
1524 EQ -> ruleSort ss1 ss2
1527 -- Better than creating Ord implementation for SSymbol since
1528 -- in general this ordering does not really make sense.
1529 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1530 symCompare (Keyword _) _ = LT
1531 symCompare (Symbol _) (Keyword _) = GT
1532 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1533 symCompare (Symbol _) _ = LT
1534 symCompare (Binding _) (Keyword _) = GT
1535 symCompare (Binding _) (Symbol _) = GT
1536 symCompare (Binding b1) (Binding b2) = compare b1 b2
1537 symCompare (Binding _) _ = LT
1538 symCompare (Expr _) (Keyword _) = GT
1539 symCompare (Expr _) (Symbol _) = GT
1540 symCompare (Expr _) (Binding _) = GT
1541 symCompare (Expr e1) (Expr e2) = compare e1 e2
1542 symCompare (Expr _) _ = LT
1543 symCompare (SimpleExpr _) (Keyword _) = GT
1544 symCompare (SimpleExpr _) (Symbol _) = GT
1545 symCompare (SimpleExpr _) (Binding _) = GT
1546 symCompare (SimpleExpr _) (Expr _) = GT
1547 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1549initDSL = DSL (PRef f [] (sUN ">>="))
1550 (PRef f [] (sUN "<*>"))
1551 (PRef f [] (sUN "pure"))
1558 where f = fileFC "(builtin)"
1560data Using = UImplicit Name PTerm
1561 | UConstraint Name [Name]
1562 deriving (Show, Eq, Data, Generic, Typeable)
1564deriving instance Binary Using
1567data SyntaxInfo = Syn {
1569 , syn_params :: [(Name, PTerm)]
1570 , syn_namespace :: [String]
1572 , imp_methods :: [Name]
1573 -- ^ interface methods. When expanding implicits, these should be
1574 -- expanded even under binders
1575 , decoration :: Name -> Name
1577 , implicitAllowed :: Bool
1578 , constraintAllowed :: Bool
1579 , maxline :: Maybe Int
1580 , mut_nesting :: Int
1582 , syn_in_quasiquote :: Int
1583 , syn_toplevel :: Bool
1584 , withAppAllowed :: Bool
1585 } deriving (Show, Generic)
1587deriving instance Binary SyntaxInfo
1590defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1592expandNS :: SyntaxInfo -> Name -> Name
1593expandNS syn n@(NS _ _) = n
1594expandNS syn n = case syn_namespace syn of
1599-- For inferring types of things
1601bi = fileFC "builtin"
1602primfc = fileFC "(primitive)"
1604inferTy = sMN 0 "__Infer"
1605inferCon = sMN 0 "__infer"
1606inferDecl = PDatadecl inferTy primfc
1608 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1609 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1610 (PRef bi [] inferTy)), bi, [])]
1613infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1614infP = P (TCon 6 0) inferTy (TType (UVal 0))
1616getInferTerm, getInferType :: Term -> Term
1617getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1618getInferTerm (App _ (App _ _ _) tm) = tm
1619getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1621getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1622 where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))
1623 toTy (PVar t) = PVTy t
1625getInferType (App _ (App _ _ ty) _) = ty
1629-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1631primNames = [inferTy, inferCon]
1634unitCon = sUN "MkUnit"
1636falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1637 "The empty type, also known as the trivially false proposition." ++
1639 "Use `void` or `absurd` to prove anything if you have a variable " ++
1640 "of type `Void` in scope."
1643pairTy = sNS (sUN "Pair") ["Builtins"]
1644pairCon = sNS (sUN "MkPair") ["Builtins"]
1646upairTy = sNS (sUN "UPair") ["Builtins"]
1647upairCon = sNS (sUN "MkUPair") ["Builtins"]
1651eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1652 "The propositional equality type. A proof that `x` = `y`." ++
1654 "To use such a proof, pattern-match on it, and the two equal things will " ++
1655 "then need to be the _same_ pattern." ++
1657 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1658 "is possible to state equalities between values of potentially different " ++
1659 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1661 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1663eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1664 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1666 [(reflDoc, reflParamDoc,
1667 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1668 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1669 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1670 pimp (n "B") Placeholder False,
1671 pexp (PRef bi [] (n "x")),
1672 pexp (PRef bi [] (n "x"))])), bi, [])]
1674 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1675 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1676 "shown that both sides are in fact equal."
1677 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1678 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1680eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1681 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1687-- | The special name to be used in the module documentation context -
1688-- not for use in the main definition context. The namespace around it
1689-- will determine the module to which the docs adhere.
1691modDocName = sMN 0 "ModuleDocs"
1693-- Defined in builtins.idr
1694sigmaTy = sNS (sUN "DPair") ["Builtins"]
1695sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1697piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1698piBind = piBindp expl
1700piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1702piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1705-- Pretty-printing declarations and terms
1707-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1708-- could interfere with interactive editing, which calls "show".
1710instance Show PTerm where
1711 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1713instance Show PDecl where
1714 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1716instance Show PClause where
1717 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1719instance Show PData where
1720 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1722instance Pretty PTerm OutputAnnotation where
1723 pretty = prettyImp defaultPPOption
1725-- | Colourise annotations according to an Idris state. It ignores the
1726-- names in the annotation, as there's no good way to show extended
1727-- information on a terminal.
1728annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1729annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1730annotationColour ist (AnnConst c) =
1731 let theme = idris_colourTheme ist
1732 in Just $ if constIsType c
1733 then typeColour theme
1734 else dataColour theme
1735annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1736annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1737annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1738annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1739annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1740annotationColour ist (AnnName n _ _ _) =
1741 let ctxt = tt_ctxt ist
1742 theme = idris_colourTheme ist
1744 _ | isDConName n ctxt -> Just $ dataColour theme
1745 _ | isFnName n ctxt -> Just $ functionColour theme
1746 _ | isTConName n ctxt -> Just $ typeColour theme
1747 _ | isPostulateName n ist -> Just $ postulateColour theme
1748 _ | otherwise -> Nothing -- don't colourise unknown names
1749annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1750 where colour BoldText = IdrisColour Nothing True False True False
1751 colour UnderlineText = IdrisColour Nothing True True False False
1752 colour ItalicText = IdrisColour Nothing True False False True
1753annotationColour ist _ = Nothing
1756-- | Colourise annotations according to an Idris state. It ignores the
1757-- names in the annotation, as there's no good way to show extended
1758-- information on a terminal. Note that strings produced this way will
1759-- not be coloured on Windows, so the use of the colour rendering
1760-- functions in Idris.Output is to be preferred.
1761consoleDecorate :: IState -> OutputAnnotation -> String -> String
1762consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1764isPostulateName :: Name -> IState -> Bool
1765isPostulateName n ist = S.member n (idris_postulates ist)
1767-- | Pretty-print a high-level closed Idris term with no information
1768-- about precedence/associativity
1769prettyImp :: PPOption -- ^ pretty printing options
1770 -> PTerm -- ^ the term to pretty-print
1771 -> Doc OutputAnnotation
1772prettyImp impl = pprintPTerm impl [] [] []
1774-- | Serialise something to base64 using its Binary implementation.
1776-- | Do the right thing for rendering a term in an IState
1777prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1778prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1780-- | Pretty-print a high-level Idris term in some bindings context
1782pprintPTerm :: PPOption -- ^ pretty printing options
1783 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1784 -> [Name] -- ^ names to always show in pi, even if not used
1785 -> [FixDecl] -- ^ Fixity declarations
1786 -> PTerm -- ^ the term to pretty-print
1787 -> Doc OutputAnnotation
1788pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1793 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1794 prettySe d p bnd (PQuote r) =
1795 text "![" <> pretty r <> text "]"
1796 prettySe d p bnd (PPatvar fc n) = pretty n
1798 | Just str <- slist d p bnd e = depth d str
1799 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1800 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1801 prettySe d p bnd (PLam fc n nfc ty sc) =
1802 let (ns, sc') = getLamNames [n] sc in
1803 depth d . bracket p startPrec . group . align . hang 2 $
1804 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1805 prettySe (decD d) startPrec ((n, False):bnd) sc'
1807 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1808 getLamNames acc sc = (reverse acc, sc)
1810 prettyBindingsOf [] t = text ""
1811 prettyBindingsOf [n] t = prettyBindingOf n t
1812 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1813 prettyBindingsOf ns t
1814 prettySe d p bnd (PLet fc n nfc ty v sc) =
1815 depth d . bracket p startPrec . group . align $
1816 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1817 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1818 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1819 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1820 || ppopt_pinames ppo && uname n =
1821 depth d . bracket p startPrec . group $
1822 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1823 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1825 depth d . bracket p startPrec . group $
1826 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1827 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1829 uname (UN n) = case str n of
1836 Static -> text "%static" <> space
1838 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1840 depth d . bracket p startPrec $
1841 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1842 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1843 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1847 Static -> text "%static" <> space
1849 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1850 depth d . bracket p startPrec $
1851 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1852 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1853 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1854 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1855 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1856 depth d . bracket p startPrec $
1857 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1858 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1859 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1860 | basename neg == sUN "negate" =
1861 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1862 -- This case preserves the behavior of the former constructor PEq.
1863 -- It should be removed if feasible when the pretty-printing of infix
1864 -- operators in general is improved.
1865 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1866 | n == eqTy, ppopt_impl ppo =
1867 depth d . bracket p eqPrec $
1868 enclose lparen rparen eq <+>
1869 align (group (vsep (map (prettyArgS (decD d) bnd)
1872 depth d . bracket p eqPrec . align . group $
1873 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1874 where eq = annName eqTy (text "=")
1876 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1877 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1878 | UN nm <- basename f
1879 , not (ppopt_impl ppo) && null (getShowArgs args) =
1880 prettyName True (ppopt_impl ppo) bnd f
1881 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1882 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1883 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1884 | UN nm <- basename op
1886 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1887 case getShowArgs args of
1889 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1890 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1891 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1892 (l@(PExp{}) : r@(PExp{}) : rest) ->
1893 depth d . bracket p funcAppPrec $
1894 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1895 align (group (vsep (map (prettyArgS d bnd) rest)))
1896 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1897 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1898 f = getFixity (opStr op)
1900 Nothing -> funcAppPrec + 1
1901 Just (Infixl p') -> p'
1902 Just f' -> prec f' + 1
1904 Nothing -> funcAppPrec + 1
1905 Just (Infixr p') -> p'
1906 Just f' -> prec f' + 1
1907 inFix l r = align . group $
1908 (prettySe (decD d) left bnd l <+> opName False) <$>
1909 group (prettySe (decD d) right bnd r)
1910 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1911 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1912 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1913 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1914 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1915 let args = getShowArgs as
1916 fp = prettySe (decD d) (startPrec + 1) bnd f
1917 shownArgs = if ppopt_impl ppo then as else args
1919 depth d . bracket p funcAppPrec . group $
1922 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1923 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1924 prettySe d p bnd (PCase _ scr cases) =
1925 bracket p funcAppPrec $
1926 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1927 depth d (indent 2 (vsep (map ppcase cases)))
1929 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1930 ([(n, False) | n <- vars l] ++ bnd)
1931 in nest nestingSize $
1932 prettyCase l <+> text "=>" <+> prettyCase r
1933 -- Warning: this is a bit of a hack. At this stage, we don't have the
1934 -- global context, so we can't determine which names are constructors,
1935 -- which are types, and which are pattern variables on the LHS of the
1936 -- case pattern. We use the heuristic that names without a namespace
1937 -- are patvars, because right now case blocks in PTerms are always
1938 -- delaborated from TT before being sent to the pretty-printer. If they
1939 -- start getting printed directly, THIS WILL BREAK.
1940 -- Potential solution: add a list of known patvars to the cases in
1941 -- PCase, and have the delaborator fill it out, kind of like the pun
1942 -- disambiguation on PDPair.
1943 vars tm = filter noNS (allNamesIn tm)
1944 noNS (NS _ _) = False
1947 prettySe d p bnd (PIfThenElse _ c t f) =
1948 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1949 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1950 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1951 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1953 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1954 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1955 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1956 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1957 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1958 prettySe d p bnd (PRewrite _ by l r _) =
1959 depth d . bracket p startPrec $
1960 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1963 Just fn -> text "using" <+>
1964 prettyName True (ppopt_impl ppo) bnd fn) <+>
1965 text "in" <+> prettySe (decD d) startPrec bnd r
1966 prettySe d p bnd (PTyped l r) =
1967 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1968 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1969 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1970 align . group . vsep . punctuate (ann comma) $
1971 map (prettySe (decD d) startPrec bnd) elts
1972 where ann = case pun of
1974 IsType -> annName pairTy
1975 IsTerm -> annName pairCon
1976 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1977 | Just elts <- dPairElts dpair
1978 = depth d . enclose (annotated lparen) (annotated rparen) .
1979 align . group . vsep . punctuate (space <> annotated (text "**")) $
1985 annotated (text "**") <+>
1986 prettySe (decD d) startPrec (addBinding bnd) r <>
1988 where annotated = case pun of
1989 IsType -> annName sigmaTy
1990 IsTerm -> annName sigmaCon
1993 (left, addBinding) = case (l, pun) of
1994 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1995 _ -> (prettySe (decD d) startPrec bnd l, id)
1998 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1999 ppElts ((PRef _ _ n, t):rs) bs
2001 = (bindingOf n False <+> colon <+>
2002 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2003 ppElts ((l, t):rs) bs
2004 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2005 prettySe d p bnd (PAlternative ns a as) =
2006 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2009 foldr ((\ l r -> l <+> text "," <+> r) .
2010 depth d . prettySe (decD d) startPrec bnd)
2012 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2013 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2014 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2015 -- XXX: add pretty for tactics
2016 prettySe d p bnd (PProof ts) =
2017 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2018 prettySe d p bnd (PTactics ts) =
2019 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2020 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2021 prettySe d p bnd PImpossible = kwd "impossible"
2022 prettySe d p bnd Placeholder = text "_"
2023 prettySe d p bnd (PDoBlock dos) =
2024 bracket p startPrec $
2025 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2026 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2027 ppdo bnd (DoBind _ bn _ tm : dos) =
2028 (prettyBindingOf bn False <+> text "<-" <+>
2029 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2030 ppdo ((bn, False):bnd) dos
2031 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2032 text "no pretty printer for pattern-matching do binding" :
2034 ppdo bnd (DoLet _ ln _ ty v : dos) =
2035 (kwd "let" <+> prettyBindingOf ln False <+>
2036 (if ty /= Placeholder
2037 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2039 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2040 ppdo ((ln, False):bnd) dos
2041 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2042 text "no pretty printer for pattern-matching do binding" :
2045 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2046 prettySe d p bnd (PElabError s) = pretty s
2047 -- Quasiquote pprinting ignores bound vars
2048 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2049 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2050 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2051 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2052 where start = if res then "`{" else "`{{"
2053 end = if res then "}" else "}}"
2054 prettySe d p bnd (PRunElab _ tm _) =
2055 bracket p funcAppPrec . group . align . hang 2 $
2057 prettySe (decD d) funcAppPrec bnd tm
2058 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2059 prettySe d p bnd _ = text "missing pretty-printer for term"
2061 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2062 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2063 where display (UN n) = T.unpack n
2064 display (MN _ n) = T.unpack n
2065 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2066 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2069 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2070 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2071 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2072 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2074 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2075 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2076 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2077 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2079 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2080 annName n = annotate (AnnName n Nothing Nothing Nothing)
2082 opStr :: Name -> String
2083 opStr (NS n _) = opStr n
2084 opStr (UN n) = T.unpack n
2086 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2087 slist' (Just d) _ _ _ | d <= 0 = Nothing
2089 | containsHole e = Nothing
2090 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2091 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2092 slist' d p bnd (PRef _ _ nil)
2093 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2094 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2095 | nsroot cons == sUN "::",
2096 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2098 Just tl' <- slist' (decD d) p bnd tl
2099 = Just (prettySe d startPrec bnd hd : tl')
2101 isImp (PImp {}) = True
2103 slist' _ _ _ tm = Nothing
2105 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2107 [] -> annotate (AnnData "" "") $ text "[]"
2108 [x] -> enclose left right . group $ x
2109 xs -> enclose left right .
2110 align . group . vsep .
2111 punctuate comma $ xs
2112 where left = (annotate (AnnData "" "") (text "["))
2113 right = (annotate (AnnData "" "") (text "]"))
2114 comma = (annotate (AnnData "" "") (text ","))
2115 slist _ _ _ _ = Nothing
2117 pairElts :: PTerm -> Maybe [PTerm]
2118 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2119 | otherwise = Just [x, y]
2120 pairElts _ = Nothing
2122 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2123 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2124 | otherwise = Just [(l, t), (Placeholder, r)]
2125 dPairElts _ = Nothing
2127 natns = "Prelude.Nat."
2129 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2131 | ppopt_desugarnats ppo = Nothing
2132 | otherwise = snat' d p e
2134 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2135 snat' (Just x) _ _ | x <= 0 = Nothing
2136 snat' d p (PRef _ _ z)
2137 | show z == (natns++"Z") || show z == "Z" = Just 0
2138 snat' d p (PApp _ s [PExp {getTm=n}])
2139 | show s == (natns++"S") || show s == "S",
2140 Just n' <- snat' (decD d) p n
2142 snat' _ _ _ = Nothing
2144 bracket outer inner doc
2145 | outer > inner = lparen <> doc <> rparen
2148 ellipsis = text "..."
2151 depth (Just d) = if d <= 0 then const ellipsis else id
2153 decD = fmap (\x -> x - 1)
2155 kwd = annotate AnnKeyword . text
2157 fixities :: M.Map String Fixity
2158 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2160 getFixity :: String -> Maybe Fixity
2161 getFixity = flip M.lookup fixities
2163-- | Strip away namespace information
2164basename :: Name -> Name
2165basename (NS n _) = basename n
2168-- | Determine whether a name was the one inserted for a hole or guess
2169-- by the delaborator
2170isHoleName :: Name -> Bool
2171isHoleName (UN n) = n == T.pack "[__]"
2174-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2175containsHole :: PTerm -> Bool
2176containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2178-- | Pretty-printer helper for names that attaches the correct annotations
2179prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2180 -> Bool -- ^ whether to show namespaces
2181 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2182 -> Name -- ^ the name to pprint
2183 -> Doc OutputAnnotation
2184prettyName infixParen showNS bnd n
2185 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2186 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2187 | (UN n') <- n, T.unpack n' == "_" = text "_"
2188 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2189 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2190 where fullName = text nameSpace <> parenthesise (text (baseName n))
2191 baseName (UN n) = T.unpack n
2192 baseName (NS n ns) = baseName n
2193 baseName (MN i s) = T.unpack s
2194 baseName other = show other
2195 nameSpace = case n of
2196 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2198 isInfix = case baseName n of
2200 (c : _) -> not (isAlpha c)
2201 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2204showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2205showCImp ppo (PClause _ n l ws r w)
2206 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2207 <+> text "where" <+> text (show w)
2210 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2211showCImp ppo (PWith _ n l ws r pn w)
2212 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2213 <+> braces (text (show w))
2216 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2219showDImp :: PPOption -> PData -> Doc OutputAnnotation
2220showDImp ppo (PDatadecl n nfc ty cons)
2221 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2222 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2224showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2225showDecls o ds = vsep (map (showDeclImp o) ds)
2227showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2228showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2229showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2230 indent 2 (vsep (map (showCImp o) cs))
2231showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2232showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2233showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2234showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2235showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2236showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2237 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2238showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2239 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2240showDeclImp _ _ = text "..."
2241-- showDeclImp (PImport o) = "import " ++ o
2243getImps :: [PArg] -> [(Name, PTerm)]
2245getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2246getImps (_ : xs) = getImps xs
2248getExps :: [PArg] -> [PTerm]
2250getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2251getExps (_ : xs) = getExps xs
2253getShowArgs :: [PArg] -> [PArg]
2255getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2256getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2257 | PImp _ _ _ _ tm <- e
2258 , containsHole tm = e : getShowArgs xs
2259getShowArgs (_ : xs) = getShowArgs xs
2261getConsts :: [PArg] -> [PTerm]
2263getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2264getConsts (_ : xs) = getConsts xs
2266getAll :: [PArg] -> [PTerm]
2271showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2272 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2273 -> PPOption -- ^ pretty printing options
2274 -> Bool -- ^ whether to colourise
2275 -> Name -- ^ the term to show
2277showName ist bnd ppo colour n = case ist of
2278 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2279 Nothing -> showbasic n
2280 where name = if ppopt_impl ppo then show n else showbasic n
2281 showbasic n@(UN _) = showCG n
2282 showbasic (MN i s) = str s
2283 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2284 showbasic (SN s) = show s
2286 colourise n t = let ctxt' = fmap tt_ctxt ist in
2289 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2290 else colouriseBound t name
2291 | isDConName n ctxt -> colouriseData t name
2292 | isFnName n ctxt -> colouriseFun t name
2293 | isTConName n ctxt -> colouriseType t name
2294 -- The assumption is that if a name is not bound and does not exist in the
2295 -- global context, then we're somewhere in which implicit info has been lost
2296 -- (like error messages). Thus, unknown vars are colourised as implicits.
2297 | otherwise -> colouriseImplicit t name
2299showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2300 -> PTerm -- ^ the term to show
2302showTm ist = displayDecorated (consoleDecorate ist) .
2303 renderPretty 0.8 100000 .
2304 prettyImp (ppOptionIst ist)
2306-- | Show a term with implicits, no colours
2307showTmImpls :: PTerm -> String
2308showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2310-- | Show a term with specific options
2311showTmOpts :: PPOption -> PTerm -> String
2312showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2315instance Sized PTerm where
2316 size (PQuote rawTerm) = size rawTerm
2317 size (PRef fc _ name) = size name
2318 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2319 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2320 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2321 size (PTyped trm ty) = 1 + size trm + size ty
2322 size (PApp fc name args) = 1 + size args
2323 size (PAppBind fc name args) = 1 + size args
2324 size (PCase fc trm bdy) = 1 + size trm + size bdy
2325 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2326 size (PTrue fc _) = 1
2327 size (PResolveTC fc) = 1
2328 size (PRewrite fc by left right _) = 1 + size left + size right
2329 size (PPair fc _ _ left right) = 1 + size left + size right
2330 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2331 size (PAlternative _ a alts) = 1 + size alts
2332 size (PHidden hidden) = size hidden
2333 size (PUnifyLog tm) = size tm
2334 size (PDisamb _ tm) = size tm
2335 size (PNoImplicits tm) = size tm
2337 size (PUniverse _ _) = 1
2338 size (PConstant fc const) = 1 + size fc + size const
2339 size Placeholder = 1
2340 size (PDoBlock dos) = 1 + size dos
2341 size (PIdiom fc term) = 1 + size term
2342 size (PMetavar _ name) = 1
2343 size (PProof tactics) = size tactics
2344 size (PElabError err) = size err
2345 size PImpossible = 1
2348getPArity :: PTerm -> Int
2349getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2352-- Return all names, free or globally bound, in the given term.
2354allNamesIn :: PTerm -> [Name]
2355allNamesIn tm = nub $ ni 0 [] tm
2356 where -- TODO THINK added niTacImp, but is it right?
2357 ni 0 env (PRef _ _ n)
2358 | not (n `elem` env) = [n]
2359 ni 0 env (PPatvar _ n) = [n]
2360 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2361 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2362 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2363 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2364 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2365 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2366 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2367 ni 0 env (PHidden tm) = ni 0 env tm
2368 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2369 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2370 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2371 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2372 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2373 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2374 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2375 ni 0 env (PUnifyLog tm) = ni 0 env tm
2376 ni 0 env (PDisamb _ tm) = ni 0 env tm
2377 ni 0 env (PNoImplicits tm) = ni 0 env tm
2379 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2380 ni i env (PUnquote tm) = ni (i - 1) env tm
2381 ni i env tm = concatMap (ni i env) (children tm)
2383 niTacImp i env (TacImp _ _ scr) = ni i env scr
2387-- Return all names defined in binders in the given term
2388boundNamesIn :: PTerm -> [Name]
2389boundNamesIn tm = S.toList (ni 0 S.empty tm)
2390 where -- TODO THINK Added niTacImp, but is it right?
2391 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2392 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2393 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2394 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2395 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2396 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2397 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2398 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2399 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2400 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2401 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2402 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2403 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2404 ni 0 set (PAlternative ns a as) = niTms 0 set as
2405 ni 0 set (PHidden tm) = ni 0 set tm
2406 ni 0 set (PUnifyLog tm) = ni 0 set tm
2407 ni 0 set (PDisamb _ tm) = ni 0 set tm
2408 ni 0 set (PNoImplicits tm) = ni 0 set tm
2410 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2411 ni i set (PUnquote tm) = ni (i - 1) set tm
2413 ni i set tm = foldr (S.union . ni i set) set (children tm)
2415 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2416 niTms i set [] = set
2417 niTms i set (x : xs) = niTms i (ni i set x) xs
2419 niTacImp i set (TacImp _ _ scr) = ni i set scr
2420 niTacImp i set _ = set
2422-- Return names which are valid implicits in the given term (type).
2423implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2424implicitNamesIn uvars ist tm
2425 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2428 addImp n = do (imps, fns) <- get
2430 addFn n = do (imps, fns) <- get
2434 notCAF (PExp _ _ _ _ : _) = True
2435 notCAF (_ : xs) = notCAF xs
2437 notHidden (n, _) = case getAccessibility n of
2443 = case lookupDefAccExact n False (tt_ctxt ist) of
2447 ni 0 env (PRef _ _ n@(NS _ _))
2448 | not (n `elem` env)
2449 -- Never implicitly bind if there's a namespace
2451 ni 0 env (PRef _ _ n)
2452 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2453 ni 0 env (PApp _ f@(PRef _ _ n) as)
2454 | n `elem` uvars = do ni 0 env f
2455 mapM_ (ni 0 env . getTm) as
2456 | otherwise = do case lookupTy n (tt_ctxt ist) of
2459 mapM_ (ni 0 env . getTm) as
2460 ni 0 env (PApp _ f as) = do ni 0 env f
2461 mapM_ (ni 0 env . getTm) as
2462 ni 0 env (PAppBind _ f as) = do ni 0 env f
2463 mapM_ (ni 0 env . getTm) as
2464 ni 0 env (PCase _ c os) = do ni 0 env c
2465 -- names in 'os', not counting the names bound in the cases
2466 mapM_ (ni 0 env . snd) os
2469 mapM_ (ni 0 env . fst) os
2471 put (nub imps \\ nub impsfst, fns)
2472 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2473 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2474 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2475 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2476 ni 0 env val; ni 0 (n:env) sc
2477 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2478 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2479 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2480 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2481 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2484 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2485 ni 0 env (PHidden tm) = ni 0 env tm
2486 ni 0 env (PUnifyLog tm) = ni 0 env tm
2487 ni 0 env (PDisamb _ tm) = ni 0 env tm
2488 ni 0 env (PNoImplicits tm) = ni 0 env tm
2490 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2491 maybe (return ()) (ni i env) ty
2492 ni i env (PUnquote tm) = ni (i - 1) env tm
2494 ni i env tm = mapM_ (ni i env) (children tm)
2496-- Return names which are free in the given term.
2497namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2498namesIn uvars ist tm = nub $ ni 0 [] tm
2500 ni 0 env (PRef _ _ n)
2501 | not (n `elem` env)
2502 = case lookupTy n (tt_ctxt ist) of
2504 _ -> [n | n `elem` (map fst uvars)]
2505 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2506 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2507 ni 0 env (PCase _ c os) = ni 0 env c ++
2508 -- names in 'os', not counting the names bound in the cases
2509 (nub (concatMap (ni 0 env . snd) os)
2510 \\ nub (concatMap (ni 0 env . fst) os))
2511 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2512 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2513 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2514 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2515 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2516 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2517 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2518 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2519 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2520 ni 0 env (PHidden tm) = ni 0 env tm
2521 ni 0 env (PUnifyLog tm) = ni 0 env tm
2522 ni 0 env (PDisamb _ tm) = ni 0 env tm
2523 ni 0 env (PNoImplicits tm) = ni 0 env tm
2525 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2526 ni i env (PUnquote tm) = ni (i - 1) env tm
2528 ni i env tm = concatMap (ni i env) (children tm)
2530 niTacImp i env (TacImp _ _ scr) = ni i env scr
2533-- Return which of the given names are used in the given term.
2535usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2536usedNamesIn vars ist tm = nub $ ni 0 [] tm
2537 where -- TODO THINK added niTacImp, but is it right?
2538 ni 0 env (PRef _ _ n)
2539 | n `elem` vars && not (n `elem` env)
2540 = case lookupDefExact n (tt_ctxt ist) of
2543 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2544 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2545 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2546 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2547 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2548 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2549 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2550 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2551 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2552 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2553 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2554 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2555 ni 0 env (PHidden tm) = ni 0 env tm
2556 ni 0 env (PUnifyLog tm) = ni 0 env tm
2557 ni 0 env (PDisamb _ tm) = ni 0 env tm
2558 ni 0 env (PNoImplicits tm) = ni 0 env tm
2560 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2561 ni i env (PUnquote tm) = ni (i - 1) env tm
2563 ni i env tm = concatMap (ni i env) (children tm)
2565 niTacImp i env (TacImp _ _ scr) = ni i env scr
2568-- Return the list of inaccessible (= dotted) positions for a name.
2569getErasureInfo :: IState -> Name -> [Int]
2570getErasureInfo ist n =
2571 case lookupCtxtExact n (idris_optimisation ist) of
2572 Just (Optimise inacc detag force) -> 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