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
190 deriving (Show, Eq, Read, Ord, Generic)
192-- | The output mode in use
193data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
194 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
197-- | How wide is the console?
198data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
199 | ColsWide Int -- ^ Manually specified - must be positive
200 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
201 deriving (Show, Eq, Generic)
203-- | If a function has no totality annotation, what do we assume?
204data DefaultTotality = DefaultCheckingTotal -- ^ Total
205 | DefaultCheckingPartial -- ^ Partial
206 | DefaultCheckingCovering -- ^Total coverage, but may diverge
207 deriving (Show, Eq, Generic)
209-- | The global state used in the Idris monad
210data IState = IState {
211 tt_ctxt :: Context -- ^ All the currently defined names and their terms
212 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
213 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
214 , idris_implicits :: Ctxt [PArg]
215 , idris_statics :: Ctxt [Bool]
216 , idris_interfaces :: Ctxt InterfaceInfo
217 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
218 , idris_records :: Ctxt RecordInfo
219 , idris_dsls :: Ctxt DSL
220 , idris_optimisation :: Ctxt OptInfo
221 , idris_datatypes :: Ctxt TypeInfo
222 , idris_namehints :: Ctxt [Name]
224 -- | list of lhs/rhs, and a list of missing clauses. These are not
226 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
227 , idris_flags :: Ctxt [FnOpt]
228 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
229 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
231 -- | module documentation is saved in a special MN so the context
232 -- mechanism can be used for disambiguation.
233 , idris_moduledocs :: Ctxt (Docstring DocTerm)
234 , idris_tyinfodata :: Ctxt TIData
235 , idris_fninfo :: Ctxt FnInfo
236 , idris_transforms :: Ctxt [(Term, Term)]
237 , idris_autohints :: Ctxt [Name]
238 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
239 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
240 , idris_totcheckfail :: [(FC, String)]
241 , idris_options :: IOption
243 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
245 -- | The currently defined but not proven metavariables. The Int is
246 -- the number of vars to display as a context, the Maybe Name is its
247 -- top-level function, the [Name] is the list of local variables
248 -- available for proof search and the Bools are whether :p is
249 -- allowed, and whether the variable is definable at all
250 -- (Metavariables are not definable if they are applied in a term
251 -- which still has hole bindings)
252 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
253 , idris_coercions :: [Name]
254 , idris_errRev :: [(Term, Term)]
255 , syntax_rules :: SyntaxRules
256 , syntax_keywords :: [String]
257 , imported :: [FilePath] -- ^ The imported modules
258 , idris_scprims :: [(Name, (Int, PrimFn))]
259 , idris_objs :: [(Codegen, FilePath)]
260 , idris_libs :: [(Codegen, String)]
261 , idris_cgflags :: [(Codegen, String)]
262 , idris_hdrs :: [(Codegen, String)]
263 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
264 , proof_list :: [(Name, (Bool, [String]))]
265 , errSpan :: Maybe FC
266 , parserWarnings :: [(FC, Err)]
267 , lastParse :: Maybe Name
268 , indent_stack :: [Int]
269 , brace_stack :: [Maybe Int]
270 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
271 , idris_parsedSpan :: Maybe FC
272 , hide_list :: Ctxt Accessibility
273 , default_access :: Accessibility
274 , default_total :: DefaultTotality
275 , ibc_write :: [IBCWrite]
276 , compiled_so :: Maybe String
277 , idris_dynamic_libs :: [DynamicLib]
278 , idris_language_extensions :: [LanguageExt]
279 , idris_outputmode :: OutputMode
280 , idris_colourRepl :: Bool
281 , idris_colourTheme :: ColourTheme
282 , idris_errorhandlers :: [Name] -- ^ Global error handlers
283 , idris_nameIdx :: (Int, Ctxt (Int, Name))
284 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
285 , module_aliases :: M.Map [T.Text] [T.Text]
286 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
287 , idris_postulates :: S.Set Name
288 , idris_externs :: S.Set (Name, Int)
289 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
290 , idris_whocalls :: Maybe (M.Map Name [Name])
291 , idris_callswho :: Maybe (M.Map Name [Name])
293 -- | List of names that were defined in the repl, and can be re-/un-defined
294 , idris_repl_defs :: [Name]
296 -- | Stack of names currently being elaborated, Bool set if it's an
297 -- implementation (implementations appear twice; also as a funtion name)
298 , elab_stack :: [(Name, Bool)]
301 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
302 , idris_exports :: [Name] -- ^ Functions with ExportList
303 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
304 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
305 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
306 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
307 , idris_ttstats :: M.Map Term (Int, Term)
308 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
312-- Required for parsers library, and therefore trifecta
313instance Show IState where
314 show = const "{internal state}"
316data SizeChange = Smaller | Same | Bigger | Unknown
317 deriving (Show, Eq, Generic)
319deriving instance Binary SizeChange
322type SCGEntry = (Name, [Maybe (Int, SizeChange)])
323type UsageReason = (Name, Int) -- fn_name, its_arg_number
325data CGInfo = CGInfo {
326 calls :: [Name] -- Immediate calls
327 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
329 , usedpos :: [(Int, [UsageReason])]
330 } deriving (Show, Generic)
332deriving instance Binary CGInfo
335primDefs = [ sUN "unsafePerformPrimIO"
336 , sUN "mkLazyForeignPrim"
337 , sUN "mkForeignPrim"
339 , sUN "assert_unreachable"
343-- information that needs writing for the current module's .ibc file
344data IBCWrite = IBCFix FixDecl
349 | IBCImplementation Bool Bool Name Name
356 | IBCImport (Bool, FilePath) -- ^ True = import public
357 | IBCImportDir FilePath
358 | IBCSourceDir FilePath
359 | IBCObj Codegen FilePath
360 | IBCLib Codegen String
361 | IBCCGFlag Codegen String
363 | IBCHeader Codegen String
364 | IBCAccess Name Accessibility
365 | IBCMetaInformation Name MetaInformation
366 | IBCTotal Name Totality
367 | IBCInjective Name Injectivity
369 | IBCFnInfo Name FnInfo
370 | IBCTrans Name (Term, Term)
371 | IBCErrRev (Term, Term)
375 | IBCDef Name -- ^ The main context.
376 | IBCNameHint (Name, Name)
377 | IBCLineApp FilePath Int PTerm
378 | IBCErrorHandler Name
379 | IBCFunctionErrorHandler Name Name Name
381 | IBCExtern (Name, Int)
382 | IBCTotCheckErr FC String
384 | IBCModDocs Name -- ^ The name is the special name used to track module docs
385 | IBCUsage (Name, Int)
387 | IBCAutoHint Name Name
388 | IBCDeprecate Name String
389 | IBCFragile Name String
390 | IBCConstraint FC UConstraint
391 deriving (Show, Generic)
393-- | The initial state for the compiler
395idrisInit = IState initContext S.empty []
396 emptyContext emptyContext emptyContext [] emptyContext
397 emptyContext emptyContext emptyContext emptyContext
398 emptyContext emptyContext emptyContext emptyContext
399 emptyContext emptyContext emptyContext emptyContext
401 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
402 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
403 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
404 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
405 emptyContext S.empty M.empty emptyContext
408-- | The monad for the main REPL - reading and processing files and
409-- updating global state (hence the IO inner monad).
412-- type Idris = WriterT [Either String (IO ())] (State IState a))
415type Idris = StateT IState (ExceptT Err IO)
417catchError :: Idris a -> (Err -> Idris a) -> Idris a
418catchError = liftCatch catchE
420throwError :: Err -> Idris a
421throwError = Trans.lift . throwE
423-- Commands in the REPL
425data Codegen = Via IRFormat String
427 deriving (Show, Eq, Generic)
429data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
431data HowMuchDocs = FullDocs | OverviewDocs
433data OutputFmt = HTMLOutput | LaTeXOutput
435-- | Recognised logging categories for the Idris compiler.
437-- @TODO add in sub categories.
444 deriving (Show, Eq, Ord, Generic)
446strLogCat :: LogCat -> String
447strLogCat IParse = "parser"
448strLogCat IElab = "elab"
449strLogCat ICodeGen = "codegen"
450strLogCat IErasure = "erasure"
451strLogCat ICoverage = "coverage"
452strLogCat IIBC = "ibc"
454codegenCats :: [LogCat]
455codegenCats = [ICodeGen]
457parserCats :: [LogCat]
463loggingCatsStr :: String
464loggingCatsStr = unlines
467 , (strLogCat ICodeGen)
468 , (strLogCat IErasure)
469 , (strLogCat ICoverage)
474data ElabShellCmd = EQED
482 | EDocStr (Either Name Const)
485data Opt = Filename String
500 | NoBuiltins -- only for the really primitive stuff!
517 | Port REPLPort -- ^ REPL TCP port
526 | PkgDocBuild String -- IdrisDoc
527 | PkgDocInstall String
537 | OutputTy OutputType
538 | Extension LanguageExt
539 | InterpretScript String
541 | TargetTriple String
544 | AddOpt Optimisation
545 | RemoveOpt Optimisation
548 | AutoWidth -- ^ Automatically adjust terminal width
549 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
550 | UseConsoleWidth ConsoleWidth
553 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
554 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
555 deriving (Show, Eq, Generic)
557data REPLPort = DontListen | ListenPort PortNumber
558 deriving (Eq, Generic, Show)
560-- Parsed declarations
562data Fixity = Infixl { prec :: Int }
563 | Infixr { prec :: Int }
564 | InfixN { prec :: Int }
565 | PrefixN { prec :: Int }
566 deriving (Eq, Generic)
568deriving instance Binary Fixity
571instance Show Fixity where
572 show (Infixl i) = "infixl " ++ show i
573 show (Infixr i) = "infixr " ++ show i
574 show (InfixN i) = "infix " ++ show i
575 show (PrefixN i) = "prefix " ++ show i
577data FixDecl = Fix Fixity String
578 deriving (Eq, Generic)
580instance Show FixDecl where
581 show (Fix f s) = show f ++ " " ++ s
584deriving instance Binary FixDecl
587instance Ord FixDecl where
588 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
591data Static = Static | Dynamic
592 deriving (Show, Eq, Ord, Data, Generic, Typeable)
594deriving instance Binary Static
597-- ^ Mark bindings with their explicitness, and laziness
598data Plicity = Imp { pargopts :: [ArgOpt]
601 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
602 , pinsource :: Bool -- ^ Explicitly written in source
605 | Exp { pargopts :: [ArgOpt]
607 , pparam :: Bool -- ^ this is a param (rather than index)
610 | Constraint { pargopts :: [ArgOpt]
614 | TacImp { pargopts :: [ArgOpt]
619 deriving (Show, Eq, Ord, Data, Generic, Typeable)
622deriving instance Binary Plicity
625is_scoped :: Plicity -> Maybe ImplicitInfo
626is_scoped (Imp _ _ _ s _ _) = s
630impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
631-- Machine generated top level implicit
632impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
635forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
636forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
638expl = Exp [] Dynamic False RigW
639expl_param = Exp [] Dynamic True RigW
641constraint = Constraint [] Static RigW
643tacimpl t = TacImp [] Dynamic t RigW
645data FnOpt = Inlinable -- ^ always evaluate when simplifying
646 | TotalFn | PartialFn | CoveringFn
647 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
650 -- | interface dictionary, eval only when a function
651 -- argument, and further evaluation results.
653 | OverlappingDictionary -- ^ Interface dictionary which may overlap
654 | Implicit -- ^ implicit coercion
655 | NoImplicit -- ^ do not apply implicit coercions
656 | CExport String -- ^ export, with a C name
657 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
658 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
659 | Reflection -- ^ a reflecting function, compile-time only
660 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
661 | UnfoldIface Name [Name]
662 -- ^ Unfold given interface name in the definition, the
663 -- top level methods, and anything which has
664 -- the interface name as an argument. This is to unfold
665 -- things for termination checking, as interfaces will otherwise
667 | Constructor -- ^ Data constructor type
668 | AutoHint -- ^ use in auto implicit search
669 | PEGenerated -- ^ generated by partial evaluator
670 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
671 deriving (Show, Eq, Generic)
673deriving instance Binary FnOpt
678inlinable :: FnOpts -> Bool
679inlinable = elem Inlinable
681dictionary :: FnOpts -> Bool
682dictionary = elem Dictionary
685-- | Type provider - what to provide
686data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
687 | ProvPostulate t -- ^ goal type must be Type, so only term
688 deriving (Show, Eq, Functor, Generic)
690type ProvideWhat = ProvideWhat' PTerm
692-- | Top-level declarations such as compiler directives, definitions,
693-- datatypes and interfaces.
695 -- | Fixity declaration
696 = PFix FC Fixity [String]
697 -- | Type declaration (last FC is precise name location)
698 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
699 -- | Postulate, second FC is precise name location
700 | PPostulate Bool -- external def if true
701 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
703 | PClauses FC FnOpts Name [PClause' t]
704 -- | Top level constant
706 -- | Data declaration.
707 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
709 | PParams FC [(Name, t)] [PDecl' t]
710 -- | Open block/declaration
711 | POpenInterfaces FC [Name] [PDecl' t]
712 -- | New namespace, where FC is accurate location of the namespace
714 | PNamespace String FC [PDecl' t]
716 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
718 FC -- Record name precise location
719 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
720 [(Name, Docstring (Either Err t))] -- Param Docs
721 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
722 (Maybe (Name, FC)) -- Optional constructor name and location
723 (Docstring (Either Err t)) -- Constructor doc
724 SyntaxInfo -- Constructor SyntaxInfo
726 -- | Interface: arguments are documentation, syntax info, source
727 -- location, constraints, interface name, interface name location,
728 -- parameters, method declarations, optional constructor name
729 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
730 [(Name, t)] -- constraints
731 Name -- interface name
732 FC -- accurate location of interface name
733 [(Name, FC, t)] -- parameters and precise locations
734 [(Name, Docstring (Either Err t))] -- parameter docstrings
735 [(Name, FC)] -- determining parameters and precise locations
736 [PDecl' t] -- declarations
737 (Maybe (Name, FC)) -- implementation constructor name and location
738 (Docstring (Either Err t)) -- implementation constructor docs
740 -- | Implementation declaration: arguments are documentation, syntax
741 -- info, source location, constraints, interface name, parameters, full
742 -- Implementation type, optional explicit name, and definitions
743 | PImplementation (Docstring (Either Err t)) -- Implementation docs
744 [(Name, Docstring (Either Err t))] -- Parameter docs
746 FC [(Name, t)] -- constraints
747 [Name] -- parent dictionaries to search for constraints
751 FC -- precise location of interface
753 [(Name, t)] -- Extra names in scope in the body
754 t -- full Implementation type
755 (Maybe Name) -- explicit name
757 | PDSL Name (DSL' t) -- ^ DSL declaration
758 | PSyntax FC Syntax -- ^ Syntax definition
759 | PMutual FC [PDecl' t] -- ^ Mutual block
760 | PDirective Directive -- ^ Compiler directive.
762 -- | Type provider. The first t is the type, the second is the
763 -- term. The second FC is precise highlighting location.
764 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
766 -- | Source-to-source transformation rule. If bool is True, lhs and
767 -- rhs must be convertible.
768 | PTransform FC Bool t t
770 -- | FC is decl-level, for errors, and Strings represent the
772 | PRunElabDecl FC t [String]
773 deriving (Functor, Generic)
775deriving instance Binary PDecl'
778-- | The set of source directives
779data Directive = DLib Codegen String
780 | DLink Codegen String
781 | DFlag Codegen String
782 | DInclude Codegen String
787 | DSetTotal Name -- assert totality after checking
788 | DAccess Accessibility
789 | DDefault DefaultTotality
791 | DDynamicLibs [String]
792 | DNameHint Name FC [(Name, FC)]
793 | DErrorHandlers Name FC Name FC [(Name, FC)]
794 | DLanguage LanguageExt
795 | DDeprecate Name String
796 | DFragile Name String
797 | DAutoImplicits Bool
801-- | A set of instructions for things that need to happen in IState
802-- after a term elaboration when there's been reflected elaboration.
803data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
804 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
805 | RAddImplementation Name Name
806 | RDatatypeDeclInstrs Name [PArg]
807 -- | Datatype, constructors
808 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
811-- | For elaborator state
812data EState = EState {
813 case_decls :: [(Name, PDecl)]
814 , delayed_elab :: [(Int, Elab' EState ())]
815 , new_tyDecls :: [RDeclInstructions]
816 , highlighting :: [(FC, OutputAnnotation)]
817 , auto_binds :: [Name] -- ^ names bound as auto implicits
818 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
822initEState = EState [] [] [] [] [] []
824type ElabD a = Elab' EState a
826highlightSource :: FC -> OutputAnnotation -> ElabD ()
827highlightSource fc annot =
828 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
830-- | One clause of a top-level definition. Term arguments to constructors are:
832-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
834-- 2. The list of extra 'with' patterns
836-- 3. The right-hand side
838-- 4. The where block (PDecl' t)
840data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
841 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
842 | PClauseR FC [t] t [PDecl' t]
843 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
844 deriving (Functor, Generic)
846deriving instance Binary PClause'
851 -- | Data declaration
852 PDatadecl { d_name :: Name -- ^ The name of the datatype
853 , d_name_fc :: FC -- ^ The precise location of the type constructor name
854 , d_tcon :: t -- ^ Type constructor
855 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
857 -- | "Placeholder" for data whose constructors are defined later
858 | PLaterdecl { d_name :: Name
861 } deriving (Functor, Generic)
863-- | Transform the FCs in a PData and its associated terms. The first
864-- function transforms the general-purpose FCs, and the second
865-- transforms those that are used for semantic source highlighting, so
866-- they can be treated specially.
867mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
868mapPDataFC f g (PDatadecl n nfc tycon ctors) =
869 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
870 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
871 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
872mapPDataFC f g (PLaterdecl n nfc tycon) =
873 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
875deriving instance Binary PData'
878-- Handy to get a free function for applying PTerm -> PTerm functions
879-- across a program, by deriving Functor
881type PDecl = PDecl' PTerm
882type PData = PData' PTerm
883type PClause = PClause' PTerm
885-- | Transform the FCs in a PTerm. The first function transforms the
886-- general-purpose FCs, and the second transforms those that are used
887-- for semantic source highlighting, so they can be treated specially.
888mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
889mapPDeclFC f g (PFix fc fixity ops) =
890 PFix (f fc) fixity ops
891mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
892 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
893mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
894 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
896mapPDeclFC f g (PClauses fc opts n clauses) =
897 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
898mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
899mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
900 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
901mapPDeclFC f g (PParams fc params decls) =
903 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
904 (map (mapPDeclFC f g) decls)
905mapPDeclFC f g (POpenInterfaces fc ifs decls) =
906 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
907mapPDeclFC f g (PNamespace ns fc decls) =
908 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
909mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
910 PRecord doc syn (f fc) opts n (g nfc)
911 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
913 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
914 plic, mapPTermFC f g ty, fdoc))
916 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
919mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
920 PInterface doc syn (f fc)
921 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
922 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
923 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
924 (map (mapPDeclFC f g) body)
925 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
927mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
928 PImplementation doc paramDocs syn (f fc)
929 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
930 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
931 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
932 (mapPTermFC f g implTy)
934 (map (mapPDeclFC f g) body)
935mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
936mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
938 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
939 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
940mapPDeclFC f g (PMutual fc decls) =
941 PMutual (f fc) (map (mapPDeclFC f g) decls)
942mapPDeclFC f g (PDirective d) =
945 DNameHint n nfc ns ->
946 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
947 DErrorHandlers n nfc n' nfc' ns ->
948 DErrorHandlers n (g nfc) n' (g nfc') $
949 map (\(an, anfc) -> (an, g anfc)) ns
950mapPDeclFC f g (PProvider doc syn fc nfc what n) =
951 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
952mapPDeclFC f g (PTransform fc safe l r) =
953 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
954mapPDeclFC f g (PRunElabDecl fc script ns) =
955 PRunElabDecl (f fc) (mapPTermFC f g script) ns
957-- | Get all the names declared in a declaration
958declared :: PDecl -> [Name]
959declared (PFix _ _ _) = []
960declared (PTy _ _ _ _ _ n fc t) = [n]
961declared (PPostulate _ _ _ _ _ _ n t) = [n]
962declared (PClauses _ _ n _) = [] -- not a declaration
963declared (PCAF _ n _) = [n]
964declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
965 where fstt (_, _, a, _, _, _, _) = a
966declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
967declared (PParams _ _ ds) = concatMap declared ds
968declared (POpenInterfaces _ _ ds) = concatMap declared ds
969declared (PNamespace _ _ ds) = concatMap declared ds
970declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
971declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
972declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
976declared (PDSL n _) = [n]
977declared (PSyntax _ _) = []
978declared (PMutual _ ds) = concatMap declared ds
979declared (PDirective _) = []
982-- get the names declared, not counting nested parameter blocks
983tldeclared :: PDecl -> [Name]
984tldeclared (PFix _ _ _) = []
985tldeclared (PTy _ _ _ _ _ n _ t) = [n]
986tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
987tldeclared (PClauses _ _ n _) = [] -- not a declaration
988tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
989tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
990 where fstt (_, _, a, _, _, _, _) = a
991tldeclared (PParams _ _ ds) = []
992tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
993tldeclared (PMutual _ ds) = concatMap tldeclared ds
994tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
995tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
996tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1002defined :: PDecl -> [Name]
1003defined (PFix _ _ _) = []
1004defined (PTy _ _ _ _ _ n _ t) = []
1005defined (PPostulate _ _ _ _ _ _ n t) = []
1006defined (PClauses _ _ n _) = [n] -- not a declaration
1007defined (PCAF _ n _) = [n]
1008defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1009 where fstt (_, _, a, _, _, _, _) = a
1010defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1011defined (PParams _ _ ds) = concatMap defined ds
1012defined (POpenInterfaces _ _ ds) = concatMap defined ds
1013defined (PNamespace _ _ ds) = concatMap defined ds
1014defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1015defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1016defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1020defined (PDSL n _) = [n]
1021defined (PSyntax _ _) = []
1022defined (PMutual _ ds) = concatMap defined ds
1023defined (PDirective _) = []
1026updateN :: [(Name, Name)] -> Name -> Name
1027updateN ns n | Just n' <- lookup n ns = n'
1030updateNs :: [(Name, Name)] -> PTerm -> PTerm
1032updateNs ns t = mapPT updateRef t
1033 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1036-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1037-- updateDNs [] t = t
1038-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1039-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1040-- where updateCNs ns (PClause n l ts r ds)
1041-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1042-- (map (fmap (updateNs ns)) ts)
1043-- (fmap (updateNs ns) r)
1044-- (map (updateDNs ns) ds)
1045-- updateDNs ns c = c
1047data PunInfo = IsType
1050 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1052-- | High level language terms
1053data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1054 -- high-level language
1056 -- ^ A reference to a variable. The FC is its precise
1057 -- source location for highlighting. The list of FCs is a
1058 -- collection of additional highlighting locations.
1059 | PInferRef FC [FC] Name -- ^ A name to be defined later
1060 | PPatvar FC Name -- ^ A pattern variable
1061 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1062 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1063 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1064 | PTyped PTerm PTerm -- ^ Term with explicit type
1065 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1066 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1067 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1068 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1069 | PMatchApp FC Name -- ^ Make an application by type matching
1070 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1071 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1072 | PTrue FC PunInfo -- ^ Unit type..?
1073 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1074 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1075 -- ^ "rewrite" syntax, with optional rewriting function and
1076 -- optional result type
1077 | PPair FC [FC] PunInfo PTerm PTerm
1078 -- ^ A pair (a, b) and whether it's a product type or a
1079 -- pair (solved by elaboration). The list of FCs is its
1081 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1082 -- ^ A dependent pair (tm : a ** b) and whether it's a
1083 -- sigma type or a pair that inhabits one (solved by
1084 -- elaboration). The [FC] is its punctuation.
1085 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1086 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1087 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1088 | PType FC -- ^ 'Type' type
1089 | PUniverse FC Universe -- ^ Some universe
1090 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1091 | PConstant FC Const -- ^ Builtin types
1092 | Placeholder -- ^ Underscore
1093 | PDoBlock [PDo] -- ^ Do notation
1094 | PIdiom FC PTerm -- ^ Idiom brackets
1095 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1096 | PProof [PTactic] -- ^ Proof script
1097 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1098 | PElabError Err -- ^ Error to report on elaboration
1099 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1100 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1101 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1102 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1103 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1104 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1105 | PUnquote PTerm -- ^ ~Term
1106 | PQuoteName Name Bool FC
1107 -- ^ `{n} where the FC is the precise highlighting for
1108 -- the name in particular. If the Bool is False, then
1109 -- it's `{{n}} and the name won't be resolved.
1110 | PRunElab FC PTerm [String]
1111 -- ^ %runElab tm - New-style proof script. Args are
1112 -- location, script, enclosing namespace.
1113 | PConstSugar FC PTerm
1114 -- ^ A desugared constant. The FC is a precise source
1115 -- location that will be used to highlight it later.
1116 deriving (Eq, Ord, Data, Typeable, Generic)
1118data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1121 deriving (Eq, Ord, Data, Generic, Typeable)
1123-- | Transform the FCs in a PTerm. The first function transforms the
1124-- general-purpose FCs, and the second transforms those that are used
1125-- for semantic source highlighting, so they can be treated specially.
1126mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1127mapPTermFC f g (PQuote q) = PQuote q
1128mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1129mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1130mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1131mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1132mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1133mapPTermFC 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)
1134mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1135mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1136mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1137mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1138mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1139mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1140mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1141mapPTermFC 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)
1142mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1143mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1144mapPTermFC 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)
1145mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1146mapPTermFC 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)
1147mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1148mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1149mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1150mapPTermFC f g (PType fc) = PType (f fc)
1151mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1152mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1153mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1154mapPTermFC f g Placeholder = Placeholder
1155mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1156 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1157 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1158 mapPDoFC (DoBindP fc t1 t2 alts) =
1159 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1160 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1161 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1162mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1163mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1164mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1165mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1166mapPTermFC f g (PElabError err) = PElabError err
1167mapPTermFC f g PImpossible = PImpossible
1168mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1169mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1170mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1171mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1172mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1173mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1174mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1175mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1176mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1179dg instance Binary PTerm
1182mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1183mapPT f t = f (mpt t) where
1184 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1185 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1186 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1187 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1188 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1189 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1190 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1191 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1192 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1193 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1194 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1195 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1196 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1197 mpt (PHidden t) = PHidden (mapPT f t)
1198 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1199 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1200 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1201 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1202 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1203 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1204 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1208data PTactic' t = Intro [Name] | Intros | Focus Name
1209 | Refine Name [Bool] | Rewrite t | DoUnify
1216 | LetTac Name t | LetTacTy Name t t
1217 | Exact t | Compute | Trivial | TCImplementation
1218 | ProofSearch Bool Bool Int (Maybe Name)
1219 [Name] -- allowed local names
1221 -- ^ the bool is whether to search recursively
1224 | ProofState | ProofTerm | Undo
1225 | Try (PTactic' t) (PTactic' t)
1226 | TSeq (PTactic' t) (PTactic' t)
1227 | ApplyTactic t -- see Language.Reflection module
1231 | GoalType String (PTactic' t)
1234 | TDocStr (Either Name Const)
1237 | TFail [ErrorReportPart]
1240 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1242deriving instance Binary PTactic'
1244instance Sized a => Sized (PTactic' a) where
1245 size (Intro nms) = 1 + size nms
1247 size (Focus nm) = 1 + size nm
1248 size (Refine nm bs) = 1 + size nm + length bs
1249 size (Rewrite t) = 1 + size t
1250 size (Induction t) = 1 + size t
1251 size (LetTac nm t) = 1 + size nm + size t
1252 size (Exact t) = 1 + size t
1260 size (Try l r) = 1 + size l + size r
1261 size (TSeq l r) = 1 + size l + size r
1262 size (ApplyTactic t) = 1 + size t
1263 size (Reflect t) = 1 + size t
1264 size (Fill t) = 1 + size t
1268 size (TFail ts) = 1 + size ts
1271 size (CaseTac x) = 1 + size x
1272 size (Equiv t) = 1 + size t
1273 size (Claim x y) = 1 + size x + size y
1275 size (MatchRefine x) = 1 + size x
1276 size (LetTacTy x y z) = 1 + size x + size y + size z
1277 size TCImplementation = 1
1279type PTactic = PTactic' PTerm
1281data PDo' t = DoExp FC t
1282 | DoBind FC Name FC t -- ^ second FC is precise name location
1283 | DoBindP FC t t [(t,t)]
1284 | DoLet FC Name FC t t -- ^ second FC is precise name location
1286 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1288deriving instance Binary PDo'
1291instance Sized a => Sized (PDo' a) where
1292 size (DoExp fc t) = 1 + size fc + size t
1293 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1294 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1295 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1296 size (DoLetP fc l r) = 1 + size fc + size l + size r
1298type PDo = PDo' PTerm
1300-- The priority gives a hint as to elaboration order. Best to elaborate
1301-- things early which will help give a more concrete type to other
1302-- variables, e.g. a before (interpTy a).
1304data PArg' t = PImp { priority :: Int
1305 , machine_inf :: Bool -- ^ true if the machine inferred it
1306 , argopts :: [ArgOpt]
1310 | PExp { priority :: Int
1311 , argopts :: [ArgOpt]
1315 | PConstraint { priority :: Int
1316 , argopts :: [ArgOpt]
1320 | PTacImplicit { priority :: Int
1321 , argopts :: [ArgOpt]
1326 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1328data ArgOpt = AlwaysShow
1332 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1334instance Sized a => Sized (PArg' a) where
1335 size (PImp p _ l nm trm) = 1 + size nm + size trm
1336 size (PExp p l nm trm) = 1 + size nm + size trm
1337 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1338 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1341deriving instance Binary PArg'
1344pimp n t mach = PImp 1 mach [] n t
1345pexp t = PExp 1 [] (sMN 0 "arg") t
1346pconst t = PConstraint 1 [] (sMN 0 "carg") t
1347ptacimp n s t = PTacImplicit 2 [] n s t
1349type PArg = PArg' PTerm
1351-- | Get the highest FC in a term, if one exists
1352highestFC :: PTerm -> Maybe FC
1353highestFC (PQuote _) = Nothing
1354highestFC (PRef fc _ _) = Just fc
1355highestFC (PInferRef fc _ _) = Just fc
1356highestFC (PPatvar fc _) = Just fc
1357highestFC (PLam fc _ _ _ _) = Just fc
1358highestFC (PPi _ _ _ _ _) = Nothing
1359highestFC (PLet fc _ _ _ _ _) = Just fc
1360highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1361highestFC (PApp fc _ _) = Just fc
1362highestFC (PAppBind fc _ _) = Just fc
1363highestFC (PMatchApp fc _) = Just fc
1364highestFC (PCase fc _ _) = Just fc
1365highestFC (PIfThenElse fc _ _ _) = Just fc
1366highestFC (PTrue fc _) = Just fc
1367highestFC (PResolveTC fc) = Just fc
1368highestFC (PRewrite fc _ _ _ _) = Just fc
1369highestFC (PPair fc _ _ _ _) = Just fc
1370highestFC (PDPair fc _ _ _ _ _) = Just fc
1371highestFC (PAs fc _ _) = Just fc
1372highestFC (PAlternative _ _ args) =
1373 case mapMaybe highestFC args of
1376highestFC (PHidden _) = Nothing
1377highestFC (PType fc) = Just fc
1378highestFC (PUniverse _ _) = Nothing
1379highestFC (PGoal fc _ _ _) = Just fc
1380highestFC (PConstant fc _) = Just fc
1381highestFC Placeholder = Nothing
1382highestFC (PDoBlock lines) =
1383 case map getDoFC lines of
1387 getDoFC (DoExp fc t) = fc
1388 getDoFC (DoBind fc nm nfc t) = fc
1389 getDoFC (DoBindP fc l r alts) = fc
1390 getDoFC (DoLet fc nm nfc l r) = fc
1391 getDoFC (DoLetP fc l r) = fc
1393highestFC (PIdiom fc _) = Just fc
1394highestFC (PMetavar fc _) = Just fc
1395highestFC (PProof _) = Nothing
1396highestFC (PTactics _) = Nothing
1397highestFC (PElabError _) = Nothing
1398highestFC PImpossible = Nothing
1399highestFC (PCoerced tm) = highestFC tm
1400highestFC (PDisamb _ opts) = highestFC opts
1401highestFC (PUnifyLog tm) = highestFC tm
1402highestFC (PNoImplicits tm) = highestFC tm
1403highestFC (PQuasiquote _ _) = Nothing
1404highestFC (PUnquote tm) = highestFC tm
1405highestFC (PQuoteName _ _ fc) = Just fc
1406highestFC (PRunElab fc _ _) = Just fc
1407highestFC (PConstSugar fc _) = Just fc
1408highestFC (PAppImpl t _) = highestFC t
1412data InterfaceInfo = CI {
1413 implementationCtorName :: Name
1414 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1415 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1416 , interface_default_super_interfaces :: [PDecl]
1417 , interface_impparams :: [Name]
1418 , interface_params :: [Name]
1419 , interface_constraints :: [PTerm]
1420 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1421 , interface_determiners :: [Int]
1422 } deriving (Show, Generic)
1424deriving instance Binary InterfaceInfo
1428data RecordInfo = RI {
1429 record_parameters :: [(Name,PTerm)]
1430 , record_constructor :: Name
1431 , record_projections :: [Name]
1432 } deriving (Show, Generic)
1434-- Type inference data
1436data TIData = TIPartial -- ^ a function with a partially defined type
1437 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1438 deriving (Show, Generic)
1440-- | Miscellaneous information about functions
1441data FnInfo = FnInfo { fn_params :: [Int] }
1442 deriving (Show, Generic)
1444deriving instance Binary FnInfo
1447data OptInfo = Optimise {
1448 inaccessible :: [(Int,Name)] -- includes names for error reporting
1449 , detaggable :: Bool
1450 , forceable :: [Int] -- argument positions which are forced by other values
1451 } deriving (Show, Generic)
1453deriving instance Binary OptInfo
1456-- | Syntactic sugar info
1461 , dsl_var :: Maybe t
1462 , index_first :: Maybe t
1463 , index_next :: Maybe t
1464 , dsl_lambda :: Maybe t
1465 , dsl_let :: Maybe t
1467 } deriving (Show, Functor, Generic)
1469deriving instance Binary DSL'
1472type DSL = DSL' PTerm
1474data SynContext = PatternSyntax
1477 deriving (Show, Generic)
1479deriving instance Binary SynContext
1482data Syntax = Rule [SSymbol] PTerm SynContext
1483 | DeclRule [SSymbol] [PDecl]
1484 deriving (Show, Generic)
1486syntaxNames :: Syntax -> [Name]
1487syntaxNames (Rule syms _ _) = mapMaybe ename syms
1488 where ename (Keyword n) = Just n
1490syntaxNames (DeclRule syms _) = mapMaybe ename syms
1491 where ename (Keyword n) = Just n
1494syntaxSymbols :: Syntax -> [SSymbol]
1495syntaxSymbols (Rule ss _ _) = ss
1496syntaxSymbols (DeclRule ss _) = ss
1498deriving instance Binary Syntax
1501data SSymbol = Keyword Name
1506 deriving (Show, Eq, Generic)
1510deriving instance Binary SSymbol
1513newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1516emptySyntaxRules :: SyntaxRules
1517emptySyntaxRules = SyntaxRules []
1519updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1520updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1522 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1527 ruleSort (s1:ss1) (s2:ss2) =
1528 case symCompare s1 s2 of
1529 EQ -> ruleSort ss1 ss2
1532 -- Better than creating Ord implementation for SSymbol since
1533 -- in general this ordering does not really make sense.
1534 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1535 symCompare (Keyword _) _ = LT
1536 symCompare (Symbol _) (Keyword _) = GT
1537 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1538 symCompare (Symbol _) _ = LT
1539 symCompare (Binding _) (Keyword _) = GT
1540 symCompare (Binding _) (Symbol _) = GT
1541 symCompare (Binding b1) (Binding b2) = compare b1 b2
1542 symCompare (Binding _) _ = LT
1543 symCompare (Expr _) (Keyword _) = GT
1544 symCompare (Expr _) (Symbol _) = GT
1545 symCompare (Expr _) (Binding _) = GT
1546 symCompare (Expr e1) (Expr e2) = compare e1 e2
1547 symCompare (Expr _) _ = LT
1548 symCompare (SimpleExpr _) (Keyword _) = GT
1549 symCompare (SimpleExpr _) (Symbol _) = GT
1550 symCompare (SimpleExpr _) (Binding _) = GT
1551 symCompare (SimpleExpr _) (Expr _) = GT
1552 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1554initDSL = DSL (PRef f [] (sUN ">>="))
1555 (PRef f [] (sUN "<*>"))
1556 (PRef f [] (sUN "pure"))
1563 where f = fileFC "(builtin)"
1565data Using = UImplicit Name PTerm
1566 | UConstraint Name [Name]
1567 deriving (Show, Eq, Data, Generic, Typeable)
1569deriving instance Binary Using
1572data SyntaxInfo = Syn {
1574 , syn_params :: [(Name, PTerm)]
1575 , syn_namespace :: [String]
1577 , imp_methods :: [Name]
1578 -- ^ interface methods. When expanding implicits, these should be
1579 -- expanded even under binders
1580 , decoration :: Name -> Name
1582 , implicitAllowed :: Bool
1583 , constraintAllowed :: Bool
1584 , maxline :: Maybe Int
1585 , mut_nesting :: Int
1587 , syn_in_quasiquote :: Int
1588 , syn_toplevel :: Bool
1589 , withAppAllowed :: Bool
1590 } deriving (Show, Generic)
1592deriving instance Binary SyntaxInfo
1595defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1597expandNS :: SyntaxInfo -> Name -> Name
1598expandNS syn n@(NS _ _) = n
1599expandNS syn n = case syn_namespace syn of
1604-- For inferring types of things
1606bi = fileFC "builtin"
1607primfc = fileFC "(primitive)"
1609inferTy = sMN 0 "__Infer"
1610inferCon = sMN 0 "__infer"
1611inferDecl = PDatadecl inferTy primfc
1613 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1614 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1615 (PRef bi [] inferTy)), bi, [])]
1618infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1619infP = P (TCon 6 0) inferTy (TType (UVal 0))
1621getInferTerm, getInferType :: Term -> Term
1622getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1623getInferTerm (App _ (App _ _ _) tm) = tm
1624getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1626getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1627 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1628 toTy (PVar _ t) = PVTy t
1630getInferType (App _ (App _ _ ty) _) = ty
1634-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1636primNames = [inferTy, inferCon]
1639unitCon = sUN "MkUnit"
1641falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1642 "The empty type, also known as the trivially false proposition." ++
1644 "Use `void` or `absurd` to prove anything if you have a variable " ++
1645 "of type `Void` in scope."
1648pairTy = sNS (sUN "Pair") ["Builtins"]
1649pairCon = sNS (sUN "MkPair") ["Builtins"]
1651upairTy = sNS (sUN "UPair") ["Builtins"]
1652upairCon = sNS (sUN "MkUPair") ["Builtins"]
1656eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1657 "The propositional equality type. A proof that `x` = `y`." ++
1659 "To use such a proof, pattern-match on it, and the two equal things will " ++
1660 "then need to be the _same_ pattern." ++
1662 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1663 "is possible to state equalities between values of potentially different " ++
1664 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1666 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1668eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1669 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1671 [(reflDoc, reflParamDoc,
1672 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1673 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1674 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1675 pimp (n "B") Placeholder False,
1676 pexp (PRef bi [] (n "x")),
1677 pexp (PRef bi [] (n "x"))])), bi, [])]
1679 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1680 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1681 "shown that both sides are in fact equal."
1682 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1683 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1685eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1686 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1692-- | The special name to be used in the module documentation context -
1693-- not for use in the main definition context. The namespace around it
1694-- will determine the module to which the docs adhere.
1696modDocName = sMN 0 "ModuleDocs"
1698-- Defined in builtins.idr
1699sigmaTy = sNS (sUN "DPair") ["Builtins"]
1700sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1702piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1703piBind = piBindp expl
1705piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1707piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1710-- Pretty-printing declarations and terms
1712-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1713-- could interfere with interactive editing, which calls "show".
1715instance Show PTerm where
1716 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1718instance Show PDecl where
1719 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1721instance Show PClause where
1722 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1724instance Show PData where
1725 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1727instance Pretty PTerm OutputAnnotation where
1728 pretty = prettyImp defaultPPOption
1730-- | Colourise annotations according to an Idris state. It ignores the
1731-- names in the annotation, as there's no good way to show extended
1732-- information on a terminal.
1733annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1734annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1735annotationColour ist (AnnConst c) =
1736 let theme = idris_colourTheme ist
1737 in Just $ if constIsType c
1738 then typeColour theme
1739 else dataColour theme
1740annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1741annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1742annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1743annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1744annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1745annotationColour ist (AnnName n _ _ _) =
1746 let ctxt = tt_ctxt ist
1747 theme = idris_colourTheme ist
1749 _ | isDConName n ctxt -> Just $ dataColour theme
1750 _ | isFnName n ctxt -> Just $ functionColour theme
1751 _ | isTConName n ctxt -> Just $ typeColour theme
1752 _ | isPostulateName n ist -> Just $ postulateColour theme
1753 _ | otherwise -> Nothing -- don't colourise unknown names
1754annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1755 where colour BoldText = IdrisColour Nothing True False True False
1756 colour UnderlineText = IdrisColour Nothing True True False False
1757 colour ItalicText = IdrisColour Nothing True False False True
1758annotationColour ist _ = Nothing
1761-- | Colourise annotations according to an Idris state. It ignores the
1762-- names in the annotation, as there's no good way to show extended
1763-- information on a terminal. Note that strings produced this way will
1764-- not be coloured on Windows, so the use of the colour rendering
1765-- functions in Idris.Output is to be preferred.
1766consoleDecorate :: IState -> OutputAnnotation -> String -> String
1767consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1769isPostulateName :: Name -> IState -> Bool
1770isPostulateName n ist = S.member n (idris_postulates ist)
1772-- | Pretty-print a high-level closed Idris term with no information
1773-- about precedence/associativity
1774prettyImp :: PPOption -- ^ pretty printing options
1775 -> PTerm -- ^ the term to pretty-print
1776 -> Doc OutputAnnotation
1777prettyImp impl = pprintPTerm impl [] [] []
1779-- | Serialise something to base64 using its Binary implementation.
1781-- | Do the right thing for rendering a term in an IState
1782prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1783prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1785-- | Pretty-print a high-level Idris term in some bindings context
1787pprintPTerm :: PPOption -- ^ pretty printing options
1788 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1789 -> [Name] -- ^ names to always show in pi, even if not used
1790 -> [FixDecl] -- ^ Fixity declarations
1791 -> PTerm -- ^ the term to pretty-print
1792 -> Doc OutputAnnotation
1793pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1798 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1799 prettySe d p bnd (PQuote r) =
1800 text "![" <> pretty r <> text "]"
1801 prettySe d p bnd (PPatvar fc n) = pretty n
1803 | Just str <- slist d p bnd e = depth d str
1804 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1805 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1806 prettySe d p bnd (PLam fc n nfc ty sc) =
1807 let (ns, sc') = getLamNames [n] sc in
1808 depth d . bracket p startPrec . group . align . hang 2 $
1809 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1810 prettySe (decD d) startPrec ((n, False):bnd) sc'
1812 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1813 getLamNames acc sc = (reverse acc, sc)
1815 prettyBindingsOf [] t = text ""
1816 prettyBindingsOf [n] t = prettyBindingOf n t
1817 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1818 prettyBindingsOf ns t
1819 prettySe d p bnd (PLet fc n nfc ty v sc) =
1820 depth d . bracket p startPrec . group . align $
1821 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1822 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1823 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1825 depth d . bracket p startPrec . group $
1826 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1827 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1829 depth d . bracket p startPrec . group $
1830 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1831 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1832 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1833 || ppopt_pinames ppo && uname n =
1834 depth d . bracket p startPrec . group $
1835 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1836 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1838 depth d . bracket p startPrec . group $
1839 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1840 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1842 uname (UN n) = case str n of
1849 Static -> text "%static" <> space
1851 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1853 depth d . bracket p startPrec $
1854 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1855 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1856 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1858 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1859 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1860 showRig _ n = prettyBindingOf n True
1864 Static -> text "%static" <> space
1866 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1867 depth d . bracket p startPrec $
1868 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1869 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1870 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1871 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1872 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1873 depth d . bracket p startPrec $
1874 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1875 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1876 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1877 | basename neg == sUN "negate" =
1878 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1879 -- This case preserves the behavior of the former constructor PEq.
1880 -- It should be removed if feasible when the pretty-printing of infix
1881 -- operators in general is improved.
1882 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1883 | n == eqTy, ppopt_impl ppo =
1884 depth d . bracket p eqPrec $
1885 enclose lparen rparen eq <+>
1886 align (group (vsep (map (prettyArgS (decD d) bnd)
1889 depth d . bracket p eqPrec . align . group $
1890 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1891 where eq = annName eqTy (text "=")
1893 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1894 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1895 | UN nm <- basename f
1896 , not (ppopt_impl ppo) && null (getShowArgs args) =
1897 prettyName True (ppopt_impl ppo) bnd f
1898 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1899 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1900 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1901 | UN nm <- basename op
1903 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1904 case getShowArgs args of
1906 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1907 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1908 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1909 (l@(PExp{}) : r@(PExp{}) : rest) ->
1910 depth d . bracket p funcAppPrec $
1911 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1912 align (group (vsep (map (prettyArgS d bnd) rest)))
1913 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1914 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1915 f = getFixity (opStr op)
1917 Nothing -> funcAppPrec + 1
1918 Just (Infixl p') -> p'
1919 Just f' -> prec f' + 1
1921 Nothing -> funcAppPrec + 1
1922 Just (Infixr p') -> p'
1923 Just f' -> prec f' + 1
1924 inFix l r = align . group $
1925 (prettySe (decD d) left bnd l <+> opName False) <$>
1926 group (prettySe (decD d) right bnd r)
1927 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1928 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1929 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1930 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1931 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1932 let args = getShowArgs as
1933 fp = prettySe (decD d) (startPrec + 1) bnd f
1934 shownArgs = if ppopt_impl ppo then as else args
1936 depth d . bracket p funcAppPrec . group $
1939 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1940 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1941 prettySe d p bnd (PCase _ scr cases) =
1942 bracket p funcAppPrec $
1943 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1944 depth d (indent 2 (vsep (map ppcase cases)))
1946 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1947 ([(n, False) | n <- vars l] ++ bnd)
1948 in nest nestingSize $
1949 prettyCase l <+> text "=>" <+> prettyCase r
1950 -- Warning: this is a bit of a hack. At this stage, we don't have the
1951 -- global context, so we can't determine which names are constructors,
1952 -- which are types, and which are pattern variables on the LHS of the
1953 -- case pattern. We use the heuristic that names without a namespace
1954 -- are patvars, because right now case blocks in PTerms are always
1955 -- delaborated from TT before being sent to the pretty-printer. If they
1956 -- start getting printed directly, THIS WILL BREAK.
1957 -- Potential solution: add a list of known patvars to the cases in
1958 -- PCase, and have the delaborator fill it out, kind of like the pun
1959 -- disambiguation on PDPair.
1960 vars tm = filter noNS (allNamesIn tm)
1961 noNS (NS _ _) = False
1964 prettySe d p bnd (PIfThenElse _ c t f) =
1965 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1966 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1967 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1968 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1970 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1971 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1972 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1973 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1974 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1975 prettySe d p bnd (PRewrite _ by l r _) =
1976 depth d . bracket p startPrec $
1977 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1980 Just fn -> text "using" <+>
1981 prettyName True (ppopt_impl ppo) bnd fn) <+>
1982 text "in" <+> prettySe (decD d) startPrec bnd r
1983 prettySe d p bnd (PTyped l r) =
1984 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1985 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1986 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1987 align . group . vsep . punctuate (ann comma) $
1988 map (prettySe (decD d) startPrec bnd) elts
1989 where ann = case pun of
1991 IsType -> annName pairTy
1992 IsTerm -> annName pairCon
1993 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1994 | Just elts <- dPairElts dpair
1995 = depth d . enclose (annotated lparen) (annotated rparen) .
1996 align . group . vsep . punctuate (space <> annotated (text "**")) $
2002 annotated (text "**") <+>
2003 prettySe (decD d) startPrec (addBinding bnd) r <>
2005 where annotated = case pun of
2006 IsType -> annName sigmaTy
2007 IsTerm -> annName sigmaCon
2010 (left, addBinding) = case (l, pun) of
2011 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
2012 _ -> (prettySe (decD d) startPrec bnd l, id)
2015 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
2016 ppElts ((PRef _ _ n, t):rs) bs
2018 = (bindingOf n False <+> colon <+>
2019 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2020 ppElts ((l, t):rs) bs
2021 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2022 prettySe d p bnd (PAlternative ns a as) =
2023 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2026 foldr ((\ l r -> l <+> text "," <+> r) .
2027 depth d . prettySe (decD d) startPrec bnd)
2029 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2030 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2031 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2032 -- XXX: add pretty for tactics
2033 prettySe d p bnd (PProof ts) =
2034 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2035 prettySe d p bnd (PTactics ts) =
2036 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2037 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2038 prettySe d p bnd PImpossible = kwd "impossible"
2039 prettySe d p bnd Placeholder = text "_"
2040 prettySe d p bnd (PDoBlock dos) =
2041 bracket p startPrec $
2042 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2043 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2044 ppdo bnd (DoBind _ bn _ tm : dos) =
2045 (prettyBindingOf bn False <+> text "<-" <+>
2046 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2047 ppdo ((bn, False):bnd) dos
2048 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2049 text "no pretty printer for pattern-matching do binding" :
2051 ppdo bnd (DoLet _ ln _ ty v : dos) =
2052 (kwd "let" <+> prettyBindingOf ln False <+>
2053 (if ty /= Placeholder
2054 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2056 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2057 ppdo ((ln, False):bnd) dos
2058 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2059 text "no pretty printer for pattern-matching do binding" :
2062 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2063 prettySe d p bnd (PElabError s) = pretty s
2064 -- Quasiquote pprinting ignores bound vars
2065 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2066 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2067 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2068 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2069 where start = if res then "`{" else "`{{"
2070 end = if res then "}" else "}}"
2071 prettySe d p bnd (PRunElab _ tm _) =
2072 bracket p funcAppPrec . group . align . hang 2 $
2074 prettySe (decD d) funcAppPrec bnd tm
2075 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2076 prettySe d p bnd _ = text "missing pretty-printer for term"
2078 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2079 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2080 where display (UN n) = T.unpack n
2081 display (MN _ n) = T.unpack n
2082 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2083 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2086 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2087 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2088 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2089 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2091 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2092 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2093 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2094 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2096 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2097 annName n = annotate (AnnName n Nothing Nothing Nothing)
2099 opStr :: Name -> String
2100 opStr (NS n _) = opStr n
2101 opStr (UN n) = T.unpack n
2103 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2104 slist' (Just d) _ _ _ | d <= 0 = Nothing
2106 | containsHole e = Nothing
2107 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2108 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2109 slist' d p bnd (PRef _ _ nil)
2110 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2111 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2112 | nsroot cons == sUN "::",
2113 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2115 Just tl' <- slist' (decD d) p bnd tl
2116 = Just (prettySe d startPrec bnd hd : tl')
2118 isImp (PImp {}) = True
2120 slist' _ _ _ tm = Nothing
2122 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2124 [] -> annotate (AnnData "" "") $ text "[]"
2125 [x] -> enclose left right . group $ x
2126 xs -> enclose left right .
2127 align . group . vsep .
2128 punctuate comma $ xs
2129 where left = (annotate (AnnData "" "") (text "["))
2130 right = (annotate (AnnData "" "") (text "]"))
2131 comma = (annotate (AnnData "" "") (text ","))
2132 slist _ _ _ _ = Nothing
2134 pairElts :: PTerm -> Maybe [PTerm]
2135 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2136 | otherwise = Just [x, y]
2137 pairElts _ = Nothing
2139 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2140 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2141 | otherwise = Just [(l, t), (Placeholder, r)]
2142 dPairElts _ = Nothing
2144 natns = "Prelude.Nat."
2146 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2148 | ppopt_desugarnats ppo = Nothing
2149 | otherwise = snat' d p e
2151 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2152 snat' (Just x) _ _ | x <= 0 = Nothing
2153 snat' d p (PRef _ _ z)
2154 | show z == (natns++"Z") || show z == "Z" = Just 0
2155 snat' d p (PApp _ s [PExp {getTm=n}])
2156 | show s == (natns++"S") || show s == "S",
2157 Just n' <- snat' (decD d) p n
2159 snat' _ _ _ = Nothing
2161 bracket outer inner doc
2162 | outer > inner = lparen <> doc <> rparen
2165 ellipsis = text "..."
2168 depth (Just d) = if d <= 0 then const ellipsis else id
2170 decD = fmap (\x -> x - 1)
2172 kwd = annotate AnnKeyword . text
2174 fixities :: M.Map String Fixity
2175 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2177 getFixity :: String -> Maybe Fixity
2178 getFixity = flip M.lookup fixities
2180-- | Strip away namespace information
2181basename :: Name -> Name
2182basename (NS n _) = basename n
2185-- | Determine whether a name was the one inserted for a hole or guess
2186-- by the delaborator
2187isHoleName :: Name -> Bool
2188isHoleName (UN n) = n == T.pack "[__]"
2191-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2192containsHole :: PTerm -> Bool
2193containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2195-- | Pretty-printer helper for names that attaches the correct annotations
2196prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2197 -> Bool -- ^ whether to show namespaces
2198 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2199 -> Name -- ^ the name to pprint
2200 -> Doc OutputAnnotation
2201prettyName infixParen showNS bnd n
2202 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2203 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2204 | (UN n') <- n, T.unpack n' == "_" = text "_"
2205 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2206 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2207 where fullName = text nameSpace <> parenthesise (text (baseName n))
2208 baseName (UN n) = T.unpack n
2209 baseName (NS n ns) = baseName n
2210 baseName (MN i s) = T.unpack s
2211 baseName other = show other
2212 nameSpace = case n of
2213 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2215 isInfix = case baseName n of
2217 (c : _) -> not (isAlpha c)
2218 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2221showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2222showCImp ppo (PClause _ n l ws r w)
2223 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2224 <+> text "where" <+> text (show w)
2227 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2228showCImp ppo (PWith _ n l ws r pn w)
2229 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2230 <+> braces (text (show w))
2233 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2236showDImp :: PPOption -> PData -> Doc OutputAnnotation
2237showDImp ppo (PDatadecl n nfc ty cons)
2238 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2239 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2241showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2242showDecls o ds = vsep (map (showDeclImp o) ds)
2244showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2245showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2246showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2247 indent 2 (vsep (map (showCImp o) cs))
2248showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2249showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2250showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2251showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2252showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2253showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2254 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2255showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2256 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2257showDeclImp _ _ = text "..."
2258-- showDeclImp (PImport o) = "import " ++ o
2260getImps :: [PArg] -> [(Name, PTerm)]
2262getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2263getImps (_ : xs) = getImps xs
2265getExps :: [PArg] -> [PTerm]
2267getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2268getExps (_ : xs) = getExps xs
2270getShowArgs :: [PArg] -> [PArg]
2272getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2273getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2274 | PImp _ _ _ _ tm <- e
2275 , containsHole tm = e : getShowArgs xs
2276getShowArgs (_ : xs) = getShowArgs xs
2278getConsts :: [PArg] -> [PTerm]
2280getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2281getConsts (_ : xs) = getConsts xs
2283getAll :: [PArg] -> [PTerm]
2288showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2289 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2290 -> PPOption -- ^ pretty printing options
2291 -> Bool -- ^ whether to colourise
2292 -> Name -- ^ the term to show
2294showName ist bnd ppo colour n = case ist of
2295 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2296 Nothing -> showbasic n
2297 where name = if ppopt_impl ppo then show n else showbasic n
2298 showbasic n@(UN _) = showCG n
2299 showbasic (MN i s) = str s
2300 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2301 showbasic (SN s) = show s
2303 colourise n t = let ctxt' = fmap tt_ctxt ist in
2306 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2307 else colouriseBound t name
2308 | isDConName n ctxt -> colouriseData t name
2309 | isFnName n ctxt -> colouriseFun t name
2310 | isTConName n ctxt -> colouriseType t name
2311 -- The assumption is that if a name is not bound and does not exist in the
2312 -- global context, then we're somewhere in which implicit info has been lost
2313 -- (like error messages). Thus, unknown vars are colourised as implicits.
2314 | otherwise -> colouriseImplicit t name
2316showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2317 -> PTerm -- ^ the term to show
2319showTm ist = displayDecorated (consoleDecorate ist) .
2320 renderPretty 0.8 100000 .
2321 prettyImp (ppOptionIst ist)
2323-- | Show a term with implicits, no colours
2324showTmImpls :: PTerm -> String
2325showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2327-- | Show a term with specific options
2328showTmOpts :: PPOption -> PTerm -> String
2329showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2332instance Sized PTerm where
2333 size (PQuote rawTerm) = size rawTerm
2334 size (PRef fc _ name) = size name
2335 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2336 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2337 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2338 size (PTyped trm ty) = 1 + size trm + size ty
2339 size (PApp fc name args) = 1 + size args
2340 size (PAppBind fc name args) = 1 + size args
2341 size (PCase fc trm bdy) = 1 + size trm + size bdy
2342 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2343 size (PTrue fc _) = 1
2344 size (PResolveTC fc) = 1
2345 size (PRewrite fc by left right _) = 1 + size left + size right
2346 size (PPair fc _ _ left right) = 1 + size left + size right
2347 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2348 size (PAlternative _ a alts) = 1 + size alts
2349 size (PHidden hidden) = size hidden
2350 size (PUnifyLog tm) = size tm
2351 size (PDisamb _ tm) = size tm
2352 size (PNoImplicits tm) = size tm
2354 size (PUniverse _ _) = 1
2355 size (PConstant fc const) = 1 + size fc + size const
2356 size Placeholder = 1
2357 size (PDoBlock dos) = 1 + size dos
2358 size (PIdiom fc term) = 1 + size term
2359 size (PMetavar _ name) = 1
2360 size (PProof tactics) = size tactics
2361 size (PElabError err) = size err
2362 size PImpossible = 1
2365getPArity :: PTerm -> Int
2366getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2369-- Return all names, free or globally bound, in the given term.
2371allNamesIn :: PTerm -> [Name]
2372allNamesIn tm = nub $ ni 0 [] tm
2373 where -- TODO THINK added niTacImp, but is it right?
2374 ni 0 env (PRef _ _ n)
2375 | not (n `elem` env) = [n]
2376 ni 0 env (PPatvar _ n) = [n]
2377 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2378 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2379 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2380 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2381 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2382 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2383 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2384 ni 0 env (PHidden tm) = ni 0 env tm
2385 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2386 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2387 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2388 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2389 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2390 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2391 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2392 ni 0 env (PUnifyLog tm) = ni 0 env tm
2393 ni 0 env (PDisamb _ tm) = ni 0 env tm
2394 ni 0 env (PNoImplicits tm) = ni 0 env tm
2396 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2397 ni i env (PUnquote tm) = ni (i - 1) env tm
2398 ni i env tm = concatMap (ni i env) (children tm)
2400 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2404-- Return all names defined in binders in the given term
2405boundNamesIn :: PTerm -> [Name]
2406boundNamesIn tm = S.toList (ni 0 S.empty tm)
2407 where -- TODO THINK Added niTacImp, but is it right?
2408 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2409 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2410 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2411 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2412 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2413 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2414 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2415 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2416 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2417 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2418 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2419 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2420 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2421 ni 0 set (PAlternative ns a as) = niTms 0 set as
2422 ni 0 set (PHidden tm) = ni 0 set tm
2423 ni 0 set (PUnifyLog tm) = ni 0 set tm
2424 ni 0 set (PDisamb _ tm) = ni 0 set tm
2425 ni 0 set (PNoImplicits tm) = ni 0 set tm
2427 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2428 ni i set (PUnquote tm) = ni (i - 1) set tm
2430 ni i set tm = foldr (S.union . ni i set) set (children tm)
2432 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2433 niTms i set [] = set
2434 niTms i set (x : xs) = niTms i (ni i set x) xs
2436 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2437 niTacImp i set _ = set
2439-- Return names which are valid implicits in the given term (type).
2440implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2441implicitNamesIn uvars ist tm
2442 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2445 addImp n = do (imps, fns) <- get
2447 addFn n = do (imps, fns) <- get
2451 notCAF (PExp _ _ _ _ : _) = True
2452 notCAF (_ : xs) = notCAF xs
2454 notHidden (n, _) = case getAccessibility n of
2460 = case lookupDefAccExact n False (tt_ctxt ist) of
2464 ni 0 env (PRef _ _ n@(NS _ _))
2465 | not (n `elem` env)
2466 -- Never implicitly bind if there's a namespace
2468 ni 0 env (PRef _ _ n)
2469 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2470 ni 0 env (PApp _ f@(PRef _ _ n) as)
2471 | n `elem` uvars = do ni 0 env f
2472 mapM_ (ni 0 env . getTm) as
2473 | otherwise = do case lookupTy n (tt_ctxt ist) of
2476 mapM_ (ni 0 env . getTm) as
2477 ni 0 env (PApp _ f as) = do ni 0 env f
2478 mapM_ (ni 0 env . getTm) as
2479 ni 0 env (PAppBind _ f as) = do ni 0 env f
2480 mapM_ (ni 0 env . getTm) as
2481 ni 0 env (PCase _ c os) = do ni 0 env c
2482 -- names in 'os', not counting the names bound in the cases
2483 mapM_ (ni 0 env . snd) os
2486 mapM_ (ni 0 env . fst) os
2488 put (nub imps \\ nub impsfst, fns)
2489 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2490 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2491 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2492 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2493 ni 0 env val; ni 0 (n:env) sc
2494 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2495 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2496 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2497 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2498 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2501 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2502 ni 0 env (PHidden tm) = ni 0 env tm
2503 ni 0 env (PUnifyLog tm) = ni 0 env tm
2504 ni 0 env (PDisamb _ tm) = ni 0 env tm
2505 ni 0 env (PNoImplicits tm) = ni 0 env tm
2507 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2508 maybe (return ()) (ni i env) ty
2509 ni i env (PUnquote tm) = ni (i - 1) env tm
2511 ni i env tm = mapM_ (ni i env) (children tm)
2513-- Return names which are free in the given term.
2514namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2515namesIn uvars ist tm = nub $ ni 0 [] tm
2517 ni 0 env (PRef _ _ n)
2518 | not (n `elem` env)
2519 = case lookupTy n (tt_ctxt ist) of
2521 _ -> [n | n `elem` (map fst uvars)]
2522 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2523 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2524 ni 0 env (PCase _ c os) = ni 0 env c ++
2525 -- names in 'os', not counting the names bound in the cases
2526 (nub (concatMap (ni 0 env . snd) os)
2527 \\ nub (concatMap (ni 0 env . fst) os))
2528 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2529 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2530 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2531 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2532 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2533 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2534 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2535 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2536 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2537 ni 0 env (PHidden tm) = ni 0 env tm
2538 ni 0 env (PUnifyLog tm) = ni 0 env tm
2539 ni 0 env (PDisamb _ tm) = ni 0 env tm
2540 ni 0 env (PNoImplicits tm) = ni 0 env tm
2542 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2543 ni i env (PUnquote tm) = ni (i - 1) env tm
2545 ni i env tm = concatMap (ni i env) (children tm)
2547 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2550-- Return which of the given names are used in the given term.
2552usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2553usedNamesIn vars ist tm = nub $ ni 0 [] tm
2554 where -- TODO THINK added niTacImp, but is it right?
2555 ni 0 env (PRef _ _ n)
2556 | n `elem` vars && not (n `elem` env)
2557 = case lookupDefExact n (tt_ctxt ist) of
2560 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2561 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2562 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2563 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2564 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2565 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2566 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2567 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2568 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2569 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2570 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2571 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2572 ni 0 env (PHidden tm) = ni 0 env tm
2573 ni 0 env (PUnifyLog tm) = ni 0 env tm
2574 ni 0 env (PDisamb _ tm) = ni 0 env tm
2575 ni 0 env (PNoImplicits tm) = ni 0 env tm
2577 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2578 ni i env (PUnquote tm) = ni (i - 1) env tm
2580 ni i env tm = concatMap (ni i env) (children tm)
2582 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2585-- Return the list of inaccessible (= dotted) positions for a name.
2586getErasureInfo :: IState -> Name -> [Int]
2587getErasureInfo ist n =
2588 case lookupCtxtExact n (idris_optimisation ist) of
2589 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