2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
9{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
11module Idris.AbsSyntaxTree where
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.Evaluate
16import Idris.Docstrings
17import IRTS.CodegenCommon
19import Util.DynamicLinker
26import Prelude hiding (Foldable, Traversable, (<$>))
28import Control.Applicative ((<|>))
29import qualified Control.Monad.Trans.Class as Trans (lift)
30import Control.Monad.Trans.Except
31import Control.Monad.Trans.State.Strict
33import Data.Data (Data)
35import Data.Foldable (Foldable)
36import Data.Function (on)
37import Data.Generics.Uniplate.Data (children, universe)
38import Data.List hiding (group)
39import qualified Data.Map.Strict as M
40import Data.Maybe (mapMaybe, maybeToList)
41import qualified Data.Set as S
42import qualified Data.Text as T
43import Data.Traversable (Traversable)
45import GHC.Generics (Generic)
46import Network.Socket (PortNumber)
49data ElabWhat = ETypes | EDefns | EAll
52-- | Data to pass to recursively called elaborators; e.g. for where blocks,
53-- paramaterised declarations, etc.
55-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
56-- so that we can have mutually recursive elaborators in separate modules without
57-- having to muck about with cyclic modules.
58data ElabInfo = EInfo {
59 params :: [(Name, PTerm)]
60 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
61 , liftname :: Name -> Name
62 , namespace :: [String]
64 , constraintNS :: String -- ^ filename for adding to constraint variables
66 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
67 -- | We may, recursively, collect transformations to do on the rhs,
68 -- e.g. rewriting recursive calls to functions defined by 'with'
69 , rhs_trans :: PTerm -> PTerm
70 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
74toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
76toplevelWith :: String -> ElabInfo
77toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
79eInfoNames :: ElabInfo -> [Name]
80eInfoNames info = map fst (params info) ++ M.keys (inblock info)
82data IOption = IOption {
84 , opt_logcats :: [LogCat] -- ^ List of logging categories.
85 , opt_typecase :: Bool
86 , opt_typeintype :: Bool
87 , opt_coverage :: Bool
88 , opt_showimp :: Bool -- ^ show implicits
89 , opt_errContext :: Bool
92 , opt_nobanner :: Bool
94 , opt_codegen :: Codegen
95 , opt_outputTy :: OutputType
96 , opt_ibcsubdir :: FilePath
97 , opt_importdirs :: [FilePath]
98 , opt_sourcedirs :: [FilePath]
99 , opt_triple :: String
101 , opt_cmdline :: [Opt] -- ^ remember whole command line
102 , opt_origerr :: Bool
103 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
104 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
105 , opt_optimise :: [Optimisation]
106 , opt_printdepth :: Maybe Int
107 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
108 , opt_desugarnats :: Bool
109 , opt_autoimpls :: Bool
110 } deriving (Show, Eq, Generic)
112defaultOpts :: IOption
113defaultOpts = IOption { opt_logLevel = 0
115 , opt_typecase = False
116 , opt_typeintype = False
117 , opt_coverage = True
118 , opt_showimp = False
119 , opt_errContext = False
122 , opt_nobanner = False
124 , opt_codegen = Via IBCFormat "c"
125 , opt_outputTy = Executable
127 , opt_importdirs = []
128 , opt_sourcedirs = []
132 , opt_origerr = False
133 , opt_autoSolve = True
134 , opt_autoImport = []
135 , opt_optimise = defaultOptimise
136 , opt_printdepth = Just 5000
137 , opt_evaltypes = True
138 , opt_desugarnats = False
139 , opt_autoimpls = True
142data PPOption = PPOption {
143 ppopt_impl :: Bool -- ^ whether to show implicits
144 , ppopt_desugarnats :: Bool
145 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
146 , ppopt_depth :: Maybe Int
149data Optimisation = PETransform -- ^ partial eval and associated transforms
150 deriving (Show, Eq, Generic)
152defaultOptimise :: [Optimisation]
155-- | Pretty printing options with default verbosity.
156defaultPPOption :: PPOption
157defaultPPOption = PPOption {
159 , ppopt_desugarnats = False
160 , ppopt_pinames = False
161 , ppopt_depth = Nothing
164-- | Pretty printing options with the most verbosity.
165verbosePPOption :: PPOption
166verbosePPOption = PPOption {
168 , ppopt_desugarnats = True
169 , ppopt_pinames = True
170 , ppopt_depth = Nothing
173-- | Get pretty printing options from the big options record.
174ppOption :: IOption -> PPOption
175ppOption opt = PPOption {
176 ppopt_impl = opt_showimp opt
177 , ppopt_pinames = False
178 , ppopt_depth = opt_printdepth opt
179 , ppopt_desugarnats = opt_desugarnats opt
182-- | Get pretty printing options from an idris state record.
183ppOptionIst :: IState -> PPOption
184ppOptionIst = ppOption . idris_options
186data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
187 | DSLNotation | ElabReflection | FCReflection
189 deriving (Show, Eq, Read, Ord, Generic)
191-- | The output mode in use
192data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
193 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
196-- | How wide is the console?
197data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
198 | ColsWide Int -- ^ Manually specified - must be positive
199 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
200 deriving (Show, Eq, Generic)
202-- | If a function has no totality annotation, what do we assume?
203data DefaultTotality = DefaultCheckingTotal -- ^ Total
204 | DefaultCheckingPartial -- ^ Partial
205 | DefaultCheckingCovering -- ^Total coverage, but may diverge
206 deriving (Show, Eq, Generic)
208-- | Configuration options for interactive editing.
209data InteractiveOpts = InteractiveOpts {
210 interactiveOpts_indentWith :: Int
211 , interactiveOpts_indentClause :: Int
212} deriving (Show, Generic)
214-- | The global state used in the Idris monad
215data IState = IState {
216 tt_ctxt :: Context -- ^ All the currently defined names and their terms
217 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
218 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
219 , idris_implicits :: Ctxt [PArg]
220 , idris_statics :: Ctxt [Bool]
221 , idris_interfaces :: Ctxt InterfaceInfo
222 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
223 , idris_records :: Ctxt RecordInfo
224 , idris_dsls :: Ctxt DSL
225 , idris_optimisation :: Ctxt OptInfo
226 , idris_datatypes :: Ctxt TypeInfo
227 , idris_namehints :: Ctxt [Name]
229 -- | list of lhs/rhs, and a list of missing clauses. These are not
231 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
232 , idris_flags :: Ctxt [FnOpt]
233 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
234 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
236 -- | module documentation is saved in a special MN so the context
237 -- mechanism can be used for disambiguation.
238 , idris_moduledocs :: Ctxt (Docstring DocTerm)
239 , idris_tyinfodata :: Ctxt TIData
240 , idris_fninfo :: Ctxt FnInfo
241 , idris_transforms :: Ctxt [(Term, Term)]
242 , idris_autohints :: Ctxt [Name]
243 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
244 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
245 , idris_totcheckfail :: [(FC, String)]
246 , idris_options :: IOption
248 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
250 -- | The currently defined but not proven metavariables. The Int is
251 -- the number of vars to display as a context, the Maybe Name is its
252 -- top-level function, the [Name] is the list of local variables
253 -- available for proof search and the Bools are whether :p is
254 -- allowed, and whether the variable is definable at all
255 -- (Metavariables are not definable if they are applied in a term
256 -- which still has hole bindings)
257 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
258 , idris_coercions :: [Name]
259 , idris_errRev :: [(Term, Term)]
260 , idris_errReduce :: [Name]
261 , syntax_rules :: SyntaxRules
262 , syntax_keywords :: [String]
263 , imported :: [FilePath] -- ^ The imported modules
264 , idris_scprims :: [(Name, (Int, PrimFn))]
265 , idris_objs :: [(Codegen, FilePath)]
266 , idris_libs :: [(Codegen, String)]
267 , idris_cgflags :: [(Codegen, String)]
268 , idris_hdrs :: [(Codegen, String)]
269 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
270 , proof_list :: [(Name, (Bool, [String]))]
271 , errSpan :: Maybe FC
272 , parserWarnings :: [(FC, Err)]
273 , lastParse :: Maybe Name
274 , indent_stack :: [Int]
275 , brace_stack :: [Maybe Int]
276 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
277 , idris_parsedSpan :: Maybe FC
278 , hide_list :: Ctxt Accessibility
279 , default_access :: Accessibility
280 , default_total :: DefaultTotality
281 , ibc_write :: [IBCWrite]
282 , compiled_so :: Maybe String
283 , idris_dynamic_libs :: [DynamicLib]
284 , idris_language_extensions :: [LanguageExt]
285 , idris_outputmode :: OutputMode
286 , idris_colourRepl :: Bool
287 , idris_colourTheme :: ColourTheme
288 , idris_errorhandlers :: [Name] -- ^ Global error handlers
289 , idris_nameIdx :: (Int, Ctxt (Int, Name))
290 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
291 , module_aliases :: M.Map [T.Text] [T.Text]
292 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
293 , idris_postulates :: S.Set Name
294 , idris_externs :: S.Set (Name, Int)
295 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
297 -- | List of names that were defined in the repl, and can be re-/un-defined
298 , idris_repl_defs :: [Name]
300 -- | Stack of names currently being elaborated, Bool set if it's an
301 -- implementation (implementations appear twice; also as a function name)
302 , elab_stack :: [(Name, Bool)]
305 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
306 , idris_exports :: [Name] -- ^ Functions with ExportList
307 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
308 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
309 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
310 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
311 , idris_ttstats :: M.Map Term (Int, Term)
312 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
313 , idris_interactiveOpts :: InteractiveOpts
316-- Required for parsers library, and therefore trifecta
317instance Show IState where
318 show = const "{internal state}"
320data SizeChange = Smaller | Same | Bigger | Unknown
321 deriving (Show, Eq, Generic)
323deriving instance Binary SizeChange
326type SCGEntry = (Name, [Maybe (Int, SizeChange)])
327type UsageReason = (Name, Int) -- fn_name, its_arg_number
329data CGInfo = CGInfo {
330 calls :: [Name] -- Immediate calls
331 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
333 , usedpos :: [(Int, [UsageReason])]
334 } deriving (Show, Generic)
336deriving instance Binary CGInfo
340primDefs = [ sUN "unsafePerformPrimIO"
341 , sUN "mkLazyForeignPrim"
342 , sUN "mkForeignPrim"
344 , sUN "assert_unreachable"
348-- information that needs writing for the current module's .ibc file
349data IBCWrite = IBCFix FixDecl
354 | IBCImplementation Bool Bool Name Name
361 | IBCImport (Bool, FilePath) -- ^ True = import public
362 | IBCImportDir FilePath
363 | IBCSourceDir FilePath
364 | IBCObj Codegen FilePath
365 | IBCLib Codegen String
366 | IBCCGFlag Codegen String
368 | IBCHeader Codegen String
369 | IBCAccess Name Accessibility
370 | IBCMetaInformation Name MetaInformation
371 | IBCTotal Name Totality
372 | IBCInjective Name Injectivity
374 | IBCFnInfo Name FnInfo
375 | IBCTrans Name (Term, Term)
376 | IBCErrRev (Term, Term)
381 | IBCDef Name -- ^ The main context.
382 | IBCNameHint (Name, Name)
383 | IBCLineApp FilePath Int PTerm
384 | IBCErrorHandler Name
385 | IBCFunctionErrorHandler Name Name Name
387 | IBCExtern (Name, Int)
388 | IBCTotCheckErr FC String
390 | IBCModDocs Name -- ^ The name is the special name used to track module docs
391 | IBCUsage (Name, Int)
393 | IBCAutoHint Name Name
394 | IBCDeprecate Name String
395 | IBCFragile Name String
396 | IBCConstraint FC UConstraint
397 deriving (Show, Generic)
399initialInteractiveOpts :: InteractiveOpts
400initialInteractiveOpts = InteractiveOpts {
401 interactiveOpts_indentWith = 2
402 , interactiveOpts_indentClause = 2
405-- | The initial state for the compiler
407idrisInit = IState initContext S.empty []
408 emptyContext emptyContext emptyContext [] emptyContext
409 emptyContext emptyContext emptyContext emptyContext
410 emptyContext emptyContext emptyContext emptyContext
411 emptyContext emptyContext emptyContext emptyContext
413 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
414 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
415 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
416 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
417 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
420-- | The monad for the main REPL - reading and processing files and
421-- updating global state (hence the IO inner monad).
424-- type Idris = WriterT [Either String (IO ())] (State IState a))
427type Idris = StateT IState (ExceptT Err IO)
429catchError :: Idris a -> (Err -> Idris a) -> Idris a
430catchError = liftCatch catchE
432throwError :: Err -> Idris a
433throwError = Trans.lift . throwE
435-- Commands in the REPL
437data Codegen = Via IRFormat String
439 deriving (Show, Eq, Generic)
441data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
443data HowMuchDocs = FullDocs | OverviewDocs
445data OutputFmt = HTMLOutput | LaTeXOutput
447-- | Recognised logging categories for the Idris compiler.
449-- @TODO add in sub categories.
456 deriving (Show, Eq, Ord, Generic)
458strLogCat :: LogCat -> String
459strLogCat IParse = "parser"
460strLogCat IElab = "elab"
461strLogCat ICodeGen = "codegen"
462strLogCat IErasure = "erasure"
463strLogCat ICoverage = "coverage"
464strLogCat IIBC = "ibc"
466codegenCats :: [LogCat]
467codegenCats = [ICodeGen]
469parserCats :: [LogCat]
475loggingCatsStr :: String
476loggingCatsStr = unlines
479 , (strLogCat ICodeGen)
480 , (strLogCat IErasure)
481 , (strLogCat ICoverage)
486data ElabShellCmd = EQED
494 | EDocStr (Either Name Const)
497data Opt = Filename String
514 | NoBuiltins -- only for the really primitive stuff!
532 | Port REPLPort -- ^ REPL TCP port
541 | PkgDocBuild String -- IdrisDoc
542 | PkgDocInstall String
552 | OutputTy OutputType
553 | Extension LanguageExt
554 | InterpretScript String
556 | TargetTriple String
559 | AddOpt Optimisation
560 | RemoveOpt Optimisation
563 | AutoWidth -- ^ Automatically adjust terminal width
564 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
565 | UseConsoleWidth ConsoleWidth
568 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
569 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
570 deriving (Show, Eq, Generic)
572data REPLPort = DontListen | ListenPort PortNumber
573 deriving (Eq, Generic, Show)
575-- Parsed declarations
577data Fixity = Infixl { prec :: Int }
578 | Infixr { prec :: Int }
579 | InfixN { prec :: Int }
580 | PrefixN { prec :: Int }
581 deriving (Eq, Generic)
583deriving instance Binary Fixity
586instance Show Fixity where
587 show (Infixl i) = "infixl " ++ show i
588 show (Infixr i) = "infixr " ++ show i
589 show (InfixN i) = "infix " ++ show i
590 show (PrefixN i) = "prefix " ++ show i
592data FixDecl = Fix Fixity String
593 deriving (Eq, Generic)
595instance Show FixDecl where
596 show (Fix f s) = show f ++ " " ++ s
599deriving instance Binary FixDecl
602instance Ord FixDecl where
603 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
606data Static = Static | Dynamic
607 deriving (Show, Eq, Ord, Data, Generic, Typeable)
609deriving instance Binary Static
612-- ^ Mark bindings with their explicitness, and laziness
613data Plicity = Imp { pargopts :: [ArgOpt]
616 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
617 , pinsource :: Bool -- ^ Explicitly written in source
620 | Exp { pargopts :: [ArgOpt]
622 , pparam :: Bool -- ^ this is a param (rather than index)
625 | Constraint { pargopts :: [ArgOpt]
629 | TacImp { pargopts :: [ArgOpt]
634 deriving (Show, Eq, Ord, Data, Generic, Typeable)
637deriving instance Binary Plicity
640is_scoped :: Plicity -> Maybe ImplicitInfo
641is_scoped (Imp _ _ _ s _ _) = s
646impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
647-- Machine generated top level implicit
649impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
653forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
654forall_constraint :: Plicity
655forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
658expl = Exp [] Dynamic False RigW
660expl_param = Exp [] Dynamic True RigW
663constraint = Constraint [] Static RigW
665tacimpl :: PTerm -> Plicity
666tacimpl t = TacImp [] Dynamic t RigW
668data FnOpt = Inlinable -- ^ always evaluate when simplifying
669 | TotalFn | PartialFn | CoveringFn
670 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
673 -- | interface dictionary, eval only when a function
674 -- argument, and further evaluation results.
676 | OverlappingDictionary -- ^ Interface dictionary which may overlap
677 | Implicit -- ^ implicit coercion
678 | NoImplicit -- ^ do not apply implicit coercions
679 | CExport String -- ^ export, with a C name
680 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
681 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
682 | ErrorReduce -- ^ unfold definition before showing an error
683 | Reflection -- ^ a reflecting function, compile-time only
684 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
685 | Constructor -- ^ Data constructor type
686 | AutoHint -- ^ use in auto implicit search
687 | PEGenerated -- ^ generated by partial evaluator
688 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
689 deriving (Show, Eq, Generic)
691deriving instance Binary FnOpt
696inlinable :: FnOpts -> Bool
697inlinable = elem Inlinable
699dictionary :: FnOpts -> Bool
700dictionary = elem Dictionary
703-- | Type provider - what to provide
704data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
705 | ProvPostulate t -- ^ goal type must be Type, so only term
706 deriving (Show, Eq, Functor, Generic)
708type ProvideWhat = ProvideWhat' PTerm
710-- | Top-level declarations such as compiler directives, definitions,
711-- datatypes and interfaces.
713 -- | Fixity declaration
714 = PFix FC Fixity [String]
715 -- | Type declaration (last FC is precise name location)
716 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
717 -- | Postulate, second FC is precise name location
718 | PPostulate Bool -- external def if true
719 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
721 | PClauses FC FnOpts Name [PClause' t]
722 -- | Top level constant
724 -- | Data declaration.
725 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
727 | PParams FC [(Name, t)] [PDecl' t]
728 -- | Open block/declaration
729 | POpenInterfaces FC [Name] [PDecl' t]
730 -- | New namespace, where FC is accurate location of the namespace
732 | PNamespace String FC [PDecl' t]
734 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
736 FC -- Record name precise location
737 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
738 [(Name, Docstring (Either Err t))] -- Param Docs
739 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
740 (Maybe (Name, FC)) -- Optional constructor name and location
741 (Docstring (Either Err t)) -- Constructor doc
742 SyntaxInfo -- Constructor SyntaxInfo
744 -- | Interface: arguments are documentation, syntax info, source
745 -- location, constraints, interface name, interface name location,
746 -- parameters, method declarations, optional constructor name
747 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
748 [(Name, t)] -- constraints
749 Name -- interface name
750 FC -- accurate location of interface name
751 [(Name, FC, t)] -- parameters and precise locations
752 [(Name, Docstring (Either Err t))] -- parameter docstrings
753 [(Name, FC)] -- determining parameters and precise locations
754 [PDecl' t] -- declarations
755 (Maybe (Name, FC)) -- implementation constructor name and location
756 (Docstring (Either Err t)) -- implementation constructor docs
758 -- | Implementation declaration: arguments are documentation, syntax
759 -- info, source location, constraints, interface name, parameters, full
760 -- Implementation type, optional explicit name, and definitions
761 | PImplementation (Docstring (Either Err t)) -- Implementation docs
762 [(Name, Docstring (Either Err t))] -- Parameter docs
764 FC [(Name, t)] -- constraints
765 [Name] -- parent dictionaries to search for constraints
769 FC -- precise location of interface
771 [(Name, t)] -- Extra names in scope in the body
772 t -- full Implementation type
773 (Maybe Name) -- explicit name
775 | PDSL Name (DSL' t) -- ^ DSL declaration
776 | PSyntax FC Syntax -- ^ Syntax definition
777 | PMutual FC [PDecl' t] -- ^ Mutual block
778 | PDirective Directive -- ^ Compiler directive.
780 -- | Type provider. The first t is the type, the second is the
781 -- term. The second FC is precise highlighting location.
782 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
784 -- | Source-to-source transformation rule. If bool is True, lhs and
785 -- rhs must be convertible.
786 | PTransform FC Bool t t
788 -- | FC is decl-level, for errors, and Strings represent the
790 | PRunElabDecl FC t [String]
791 deriving (Functor, Generic)
793deriving instance Binary PDecl'
796-- | The set of source directives
797data Directive = DLib Codegen String
798 | DLink Codegen String
799 | DFlag Codegen String
800 | DInclude Codegen String
805 | DSetTotal Name -- assert totality after checking
806 | DAccess Accessibility
807 | DDefault DefaultTotality
809 | DDynamicLibs [String]
810 | DNameHint Name FC [(Name, FC)]
811 | DErrorHandlers Name FC Name FC [(Name, FC)]
812 | DLanguage LanguageExt
813 | DDeprecate Name String
814 | DFragile Name String
815 | DAutoImplicits Bool
819-- | A set of instructions for things that need to happen in IState
820-- after a term elaboration when there's been reflected elaboration.
821data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
822 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
823 | RAddImplementation Name Name
824 | RDatatypeDeclInstrs Name [PArg]
825 -- | Datatype, constructors
826 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
829-- | For elaborator state
830data EState = EState {
831 case_decls :: [(Name, PDecl)]
832 , delayed_elab :: [(Int, Elab' EState ())]
833 , new_tyDecls :: [RDeclInstructions]
834 , highlighting :: [(FC, OutputAnnotation)]
835 , auto_binds :: [Name] -- ^ names bound as auto implicits
836 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
840initEState = EState [] [] [] [] [] []
842type ElabD a = Elab' EState a
844highlightSource :: FC -> OutputAnnotation -> ElabD ()
845highlightSource fc annot =
846 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
848-- | One clause of a top-level definition. Term arguments to constructors are:
850-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
852-- 2. The list of extra 'with' patterns
854-- 3. The right-hand side
856-- 4. The where block (PDecl' t)
858data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
859 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
860 | PClauseR FC [t] t [PDecl' t]
861 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
862 deriving (Functor, Generic)
864deriving instance Binary PClause'
869 -- | Data declaration
870 PDatadecl { d_name :: Name -- ^ The name of the datatype
871 , d_name_fc :: FC -- ^ The precise location of the type constructor name
872 , d_tcon :: t -- ^ Type constructor
873 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
875 -- | "Placeholder" for data whose constructors are defined later
876 | PLaterdecl { d_name :: Name
879 } deriving (Functor, Generic)
881-- | Transform the FCs in a PData and its associated terms. The first
882-- function transforms the general-purpose FCs, and the second
883-- transforms those that are used for semantic source highlighting, so
884-- they can be treated specially.
885mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
886mapPDataFC f g (PDatadecl n nfc tycon ctors) =
887 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
888 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
889 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
890mapPDataFC f g (PLaterdecl n nfc tycon) =
891 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
893deriving instance Binary PData'
896-- Handy to get a free function for applying PTerm -> PTerm functions
897-- across a program, by deriving Functor
899type PDecl = PDecl' PTerm
900type PData = PData' PTerm
901type PClause = PClause' PTerm
903-- | Transform the FCs in a PTerm. The first function transforms the
904-- general-purpose FCs, and the second transforms those that are used
905-- for semantic source highlighting, so they can be treated specially.
906mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
907mapPDeclFC f g (PFix fc fixity ops) =
908 PFix (f fc) fixity ops
909mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
910 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
911mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
912 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
914mapPDeclFC f g (PClauses fc opts n clauses) =
915 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
916mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
917mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
918 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
919mapPDeclFC f g (PParams fc params decls) =
921 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
922 (map (mapPDeclFC f g) decls)
923mapPDeclFC f g (POpenInterfaces fc ifs decls) =
924 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
925mapPDeclFC f g (PNamespace ns fc decls) =
926 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
927mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
928 PRecord doc syn (f fc) opts n (g nfc)
929 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
931 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
932 plic, mapPTermFC f g ty, fdoc))
934 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
937mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
938 PInterface doc syn (f fc)
939 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
940 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
941 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
942 (map (mapPDeclFC f g) body)
943 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
945mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
946 PImplementation doc paramDocs syn (f fc)
947 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
948 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
949 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
950 (mapPTermFC f g implTy)
952 (map (mapPDeclFC f g) body)
953mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
954mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
956 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
957 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
958mapPDeclFC f g (PMutual fc decls) =
959 PMutual (f fc) (map (mapPDeclFC f g) decls)
960mapPDeclFC f g (PDirective d) =
963 DNameHint n nfc ns ->
964 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
965 DErrorHandlers n nfc n' nfc' ns ->
966 DErrorHandlers n (g nfc) n' (g nfc') $
967 map (\(an, anfc) -> (an, g anfc)) ns
968mapPDeclFC f g (PProvider doc syn fc nfc what n) =
969 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
970mapPDeclFC f g (PTransform fc safe l r) =
971 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
972mapPDeclFC f g (PRunElabDecl fc script ns) =
973 PRunElabDecl (f fc) (mapPTermFC f g script) ns
975-- | Get all the names declared in a declaration
976declared :: PDecl -> [Name]
977declared (PFix _ _ _) = []
978declared (PTy _ _ _ _ _ n fc t) = [n]
979declared (PPostulate _ _ _ _ _ _ n t) = [n]
980declared (PClauses _ _ n _) = [] -- not a declaration
981declared (PCAF _ n _) = [n]
982declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
983 where fstt (_, _, a, _, _, _, _) = a
984declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
985declared (PParams _ _ ds) = concatMap declared ds
986declared (POpenInterfaces _ _ ds) = concatMap declared ds
987declared (PNamespace _ _ ds) = concatMap declared ds
988declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
989declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
990declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
994declared (PDSL n _) = [n]
995declared (PSyntax _ _) = []
996declared (PMutual _ ds) = concatMap declared ds
997declared (PDirective _) = []
1000-- get the names declared, not counting nested parameter blocks
1001tldeclared :: PDecl -> [Name]
1002tldeclared (PFix _ _ _) = []
1003tldeclared (PTy _ _ _ _ _ n _ t) = [n]
1004tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
1005tldeclared (PClauses _ _ n _) = [] -- not a declaration
1006tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1007tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1008 where fstt (_, _, a, _, _, _, _) = a
1009tldeclared (PParams _ _ ds) = []
1010tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
1011tldeclared (PMutual _ ds) = concatMap tldeclared ds
1012tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
1013tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
1014tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1020defined :: PDecl -> [Name]
1021defined (PFix _ _ _) = []
1022defined (PTy _ _ _ _ _ n _ t) = []
1023defined (PPostulate _ _ _ _ _ _ n t) = []
1024defined (PClauses _ _ n _) = [n] -- not a declaration
1025defined (PCAF _ n _) = [n]
1026defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1027 where fstt (_, _, a, _, _, _, _) = a
1028defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1029defined (PParams _ _ ds) = concatMap defined ds
1030defined (POpenInterfaces _ _ ds) = concatMap defined ds
1031defined (PNamespace _ _ ds) = concatMap defined ds
1032defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1033defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1034defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1038defined (PDSL n _) = [n]
1039defined (PSyntax _ _) = []
1040defined (PMutual _ ds) = concatMap defined ds
1041defined (PDirective _) = []
1044updateN :: [(Name, Name)] -> Name -> Name
1045updateN ns n | Just n' <- lookup n ns = n'
1048updateNs :: [(Name, Name)] -> PTerm -> PTerm
1050updateNs ns t = mapPT updateRef t
1051 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1054-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1055-- updateDNs [] t = t
1056-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1057-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1058-- where updateCNs ns (PClause n l ts r ds)
1059-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1060-- (map (fmap (updateNs ns)) ts)
1061-- (fmap (updateNs ns) r)
1062-- (map (updateDNs ns) ds)
1063-- updateDNs ns c = c
1065data PunInfo = IsType
1068 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1070-- | High level language terms
1071data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1072 -- high-level language
1074 -- ^ A reference to a variable. The FC is its precise
1075 -- source location for highlighting. The list of FCs is a
1076 -- collection of additional highlighting locations.
1077 | PInferRef FC [FC] Name -- ^ A name to be defined later
1078 | PPatvar FC Name -- ^ A pattern variable
1079 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1080 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1081 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1082 | PTyped PTerm PTerm -- ^ Term with explicit type
1083 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1084 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1085 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1086 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1087 | PMatchApp FC Name -- ^ Make an application by type matching
1088 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1089 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1090 | PTrue FC PunInfo -- ^ Unit type..?
1091 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1092 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1093 -- ^ "rewrite" syntax, with optional rewriting function and
1094 -- optional result type
1095 | PPair FC [FC] PunInfo PTerm PTerm
1096 -- ^ A pair (a, b) and whether it's a product type or a
1097 -- pair (solved by elaboration). The list of FCs is its
1099 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1100 -- ^ A dependent pair (tm : a ** b) and whether it's a
1101 -- sigma type or a pair that inhabits one (solved by
1102 -- elaboration). The [FC] is its punctuation.
1103 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1104 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1105 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1106 | PType FC -- ^ 'Type' type
1107 | PUniverse FC Universe -- ^ Some universe
1108 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1109 | PConstant FC Const -- ^ Builtin types
1110 | Placeholder -- ^ Underscore
1111 | PDoBlock [PDo] -- ^ Do notation
1112 | PIdiom FC PTerm -- ^ Idiom brackets
1113 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1114 | PProof [PTactic] -- ^ Proof script
1115 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1116 | PElabError Err -- ^ Error to report on elaboration
1117 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1118 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1119 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1120 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1121 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1122 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1123 | PUnquote PTerm -- ^ ~Term
1124 | PQuoteName Name Bool FC
1125 -- ^ `{n} where the FC is the precise highlighting for
1126 -- the name in particular. If the Bool is False, then
1127 -- it's `{{n}} and the name won't be resolved.
1128 | PRunElab FC PTerm [String]
1129 -- ^ %runElab tm - New-style proof script. Args are
1130 -- location, script, enclosing namespace.
1131 | PConstSugar FC PTerm
1132 -- ^ A desugared constant. The FC is a precise source
1133 -- location that will be used to highlight it later.
1134 deriving (Eq, Ord, Data, Typeable, Generic)
1136data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1139 deriving (Eq, Ord, Data, Generic, Typeable)
1141-- | Transform the FCs in a PTerm. The first function transforms the
1142-- general-purpose FCs, and the second transforms those that are used
1143-- for semantic source highlighting, so they can be treated specially.
1144mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1145mapPTermFC f g (PQuote q) = PQuote q
1146mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1147mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1148mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1149mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1150mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1151mapPTermFC 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)
1152mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1153mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1154mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1155mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1156mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1157mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1158mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1159mapPTermFC 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)
1160mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1161mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1162mapPTermFC 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)
1163mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1164mapPTermFC 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)
1165mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1166mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1167mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1168mapPTermFC f g (PType fc) = PType (f fc)
1169mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1170mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1171mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1172mapPTermFC f g Placeholder = Placeholder
1173mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1174 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1175 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1176 mapPDoFC (DoBindP fc t1 t2 alts) =
1177 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1178 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1179 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1180mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1181mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1182mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1183mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1184mapPTermFC f g (PElabError err) = PElabError err
1185mapPTermFC f g PImpossible = PImpossible
1186mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1187mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1188mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1189mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1190mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1191mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1192mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1193mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1194mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1197dg instance Binary PTerm
1200mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1201mapPT f t = f (mpt t) where
1202 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1203 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1204 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1205 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1206 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1207 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1208 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1209 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1210 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1211 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1212 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1213 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1214 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1215 mpt (PHidden t) = PHidden (mapPT f t)
1216 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1217 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1218 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1219 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1220 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1221 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1222 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1226data PTactic' t = Intro [Name] | Intros | Focus Name
1227 | Refine Name [Bool] | Rewrite t | DoUnify
1234 | LetTac Name t | LetTacTy Name t t
1235 | Exact t | Compute | Trivial | TCImplementation
1236 | ProofSearch Bool Bool Int (Maybe Name)
1237 [Name] -- allowed local names
1239 -- ^ the bool is whether to search recursively
1242 | ProofState | ProofTerm | Undo
1243 | Try (PTactic' t) (PTactic' t)
1244 | TSeq (PTactic' t) (PTactic' t)
1245 | ApplyTactic t -- see Language.Reflection module
1249 | GoalType String (PTactic' t)
1252 | TDocStr (Either Name Const)
1255 | TFail [ErrorReportPart]
1258 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1260deriving instance Binary PTactic'
1262instance Sized a => Sized (PTactic' a) where
1263 size (Intro nms) = 1 + size nms
1265 size (Focus nm) = 1 + size nm
1266 size (Refine nm bs) = 1 + size nm + length bs
1267 size (Rewrite t) = 1 + size t
1268 size (Induction t) = 1 + size t
1269 size (LetTac nm t) = 1 + size nm + size t
1270 size (Exact t) = 1 + size t
1278 size (Try l r) = 1 + size l + size r
1279 size (TSeq l r) = 1 + size l + size r
1280 size (ApplyTactic t) = 1 + size t
1281 size (Reflect t) = 1 + size t
1282 size (Fill t) = 1 + size t
1286 size (TFail ts) = 1 + size ts
1289 size (CaseTac x) = 1 + size x
1290 size (Equiv t) = 1 + size t
1291 size (Claim x y) = 1 + size x + size y
1293 size (MatchRefine x) = 1 + size x
1294 size (LetTacTy x y z) = 1 + size x + size y + size z
1295 size TCImplementation = 1
1297type PTactic = PTactic' PTerm
1299data PDo' t = DoExp FC t
1300 | DoBind FC Name FC t -- ^ second FC is precise name location
1301 | DoBindP FC t t [(t,t)]
1302 | DoLet FC Name FC t t -- ^ second FC is precise name location
1304 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1306deriving instance Binary PDo'
1309instance Sized a => Sized (PDo' a) where
1310 size (DoExp fc t) = 1 + size fc + size t
1311 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1312 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1313 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1314 size (DoLetP fc l r) = 1 + size fc + size l + size r
1316type PDo = PDo' PTerm
1318-- The priority gives a hint as to elaboration order. Best to elaborate
1319-- things early which will help give a more concrete type to other
1320-- variables, e.g. a before (interpTy a).
1322data PArg' t = PImp { priority :: Int
1323 , machine_inf :: Bool -- ^ true if the machine inferred it
1324 , argopts :: [ArgOpt]
1328 | PExp { priority :: Int
1329 , argopts :: [ArgOpt]
1333 | PConstraint { priority :: Int
1334 , argopts :: [ArgOpt]
1338 | PTacImplicit { priority :: Int
1339 , argopts :: [ArgOpt]
1344 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1346data ArgOpt = AlwaysShow
1350 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1352instance Sized a => Sized (PArg' a) where
1353 size (PImp p _ l nm trm) = 1 + size nm + size trm
1354 size (PExp p l nm trm) = 1 + size nm + size trm
1355 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1356 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1359deriving instance Binary PArg'
1362pimp n t mach = PImp 1 mach [] n t
1363pexp t = PExp 1 [] (sMN 0 "arg") t
1364pconst t = PConstraint 1 [] (sMN 0 "carg") t
1365ptacimp n s t = PTacImplicit 2 [] n s t
1367type PArg = PArg' PTerm
1369-- | Get the highest FC in a term, if one exists
1370highestFC :: PTerm -> Maybe FC
1371highestFC (PQuote _) = Nothing
1372highestFC (PRef fc _ _) = Just fc
1373highestFC (PInferRef fc _ _) = Just fc
1374highestFC (PPatvar fc _) = Just fc
1375highestFC (PLam fc _ _ _ _) = Just fc
1376highestFC (PPi _ _ _ _ _) = Nothing
1377highestFC (PLet fc _ _ _ _ _) = Just fc
1378highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1379highestFC (PApp fc _ _) = Just fc
1380highestFC (PAppBind fc _ _) = Just fc
1381highestFC (PMatchApp fc _) = Just fc
1382highestFC (PCase fc _ _) = Just fc
1383highestFC (PIfThenElse fc _ _ _) = Just fc
1384highestFC (PTrue fc _) = Just fc
1385highestFC (PResolveTC fc) = Just fc
1386highestFC (PRewrite fc _ _ _ _) = Just fc
1387highestFC (PPair fc _ _ _ _) = Just fc
1388highestFC (PDPair fc _ _ _ _ _) = Just fc
1389highestFC (PAs fc _ _) = Just fc
1390highestFC (PAlternative _ _ args) =
1391 case mapMaybe highestFC args of
1394highestFC (PHidden _) = Nothing
1395highestFC (PType fc) = Just fc
1396highestFC (PUniverse _ _) = Nothing
1397highestFC (PGoal fc _ _ _) = Just fc
1398highestFC (PConstant fc _) = Just fc
1399highestFC Placeholder = Nothing
1400highestFC (PDoBlock lines) =
1401 case map getDoFC lines of
1405 getDoFC (DoExp fc t) = fc
1406 getDoFC (DoBind fc nm nfc t) = fc
1407 getDoFC (DoBindP fc l r alts) = fc
1408 getDoFC (DoLet fc nm nfc l r) = fc
1409 getDoFC (DoLetP fc l r) = fc
1411highestFC (PIdiom fc _) = Just fc
1412highestFC (PMetavar fc _) = Just fc
1413highestFC (PProof _) = Nothing
1414highestFC (PTactics _) = Nothing
1415highestFC (PElabError _) = Nothing
1416highestFC PImpossible = Nothing
1417highestFC (PCoerced tm) = highestFC tm
1418highestFC (PDisamb _ opts) = highestFC opts
1419highestFC (PUnifyLog tm) = highestFC tm
1420highestFC (PNoImplicits tm) = highestFC tm
1421highestFC (PQuasiquote _ _) = Nothing
1422highestFC (PUnquote tm) = highestFC tm
1423highestFC (PQuoteName _ _ fc) = Just fc
1424highestFC (PRunElab fc _ _) = Just fc
1425highestFC (PConstSugar fc _) = Just fc
1426highestFC (PAppImpl t _) = highestFC t
1430data InterfaceInfo = CI {
1431 implementationCtorName :: Name
1432 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1433 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1434 , interface_default_super_interfaces :: [PDecl]
1435 , interface_impparams :: [Name]
1436 , interface_params :: [Name]
1437 , interface_constraints :: [PTerm]
1438 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1439 , interface_determiners :: [Int]
1440 } deriving (Show, Generic)
1442deriving instance Binary InterfaceInfo
1446data RecordInfo = RI {
1447 record_parameters :: [(Name,PTerm)]
1448 , record_constructor :: Name
1449 , record_projections :: [Name]
1450 } deriving (Show, Generic)
1452-- Type inference data
1454data TIData = TIPartial -- ^ a function with a partially defined type
1455 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1456 deriving (Show, Generic)
1458-- | Miscellaneous information about functions
1459data FnInfo = FnInfo { fn_params :: [Int] }
1460 deriving (Show, Generic)
1462deriving instance Binary FnInfo
1465data OptInfo = Optimise {
1466 inaccessible :: [(Int,Name)] -- includes names for error reporting
1467 , detaggable :: Bool
1468 , forceable :: [Int] -- argument positions which are forced by other values
1469 } deriving (Show, Generic)
1471deriving instance Binary OptInfo
1474-- | Syntactic sugar info
1479 , dsl_var :: Maybe t
1480 , index_first :: Maybe t
1481 , index_next :: Maybe t
1482 , dsl_lambda :: Maybe t
1483 , dsl_let :: Maybe t
1485 } deriving (Show, Functor, Generic)
1487deriving instance Binary DSL'
1490type DSL = DSL' PTerm
1492data SynContext = PatternSyntax
1495 deriving (Show, Generic)
1497deriving instance Binary SynContext
1500data Syntax = Rule [SSymbol] PTerm SynContext
1501 | DeclRule [SSymbol] [PDecl]
1502 deriving (Show, Generic)
1504syntaxNames :: Syntax -> [Name]
1505syntaxNames (Rule syms _ _) = mapMaybe ename syms
1506 where ename (Keyword n) = Just n
1508syntaxNames (DeclRule syms _) = mapMaybe ename syms
1509 where ename (Keyword n) = Just n
1512syntaxSymbols :: Syntax -> [SSymbol]
1513syntaxSymbols (Rule ss _ _) = ss
1514syntaxSymbols (DeclRule ss _) = ss
1516deriving instance Binary Syntax
1519data SSymbol = Keyword Name
1524 deriving (Show, Eq, Generic)
1528deriving instance Binary SSymbol
1531newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1534emptySyntaxRules :: SyntaxRules
1535emptySyntaxRules = SyntaxRules []
1537updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1538updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1540 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1545 ruleSort (s1:ss1) (s2:ss2) =
1546 case symCompare s1 s2 of
1547 EQ -> ruleSort ss1 ss2
1550 -- Better than creating Ord implementation for SSymbol since
1551 -- in general this ordering does not really make sense.
1552 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1553 symCompare (Keyword _) _ = LT
1554 symCompare (Symbol _) (Keyword _) = GT
1555 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1556 symCompare (Symbol _) _ = LT
1557 symCompare (Binding _) (Keyword _) = GT
1558 symCompare (Binding _) (Symbol _) = GT
1559 symCompare (Binding b1) (Binding b2) = compare b1 b2
1560 symCompare (Binding _) _ = LT
1561 symCompare (Expr _) (Keyword _) = GT
1562 symCompare (Expr _) (Symbol _) = GT
1563 symCompare (Expr _) (Binding _) = GT
1564 symCompare (Expr e1) (Expr e2) = compare e1 e2
1565 symCompare (Expr _) _ = LT
1566 symCompare (SimpleExpr _) (Keyword _) = GT
1567 symCompare (SimpleExpr _) (Symbol _) = GT
1568 symCompare (SimpleExpr _) (Binding _) = GT
1569 symCompare (SimpleExpr _) (Expr _) = GT
1570 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1572initDSL = DSL (PRef f [] (sUN ">>="))
1573 (PRef f [] (sUN "<*>"))
1574 (PRef f [] (sUN "pure"))
1581 where f = fileFC "(builtin)"
1583data Using = UImplicit Name PTerm
1584 | UConstraint Name [Name]
1585 deriving (Show, Eq, Data, Generic, Typeable)
1587deriving instance Binary Using
1590data SyntaxInfo = Syn {
1592 , syn_params :: [(Name, PTerm)]
1593 , syn_namespace :: [String]
1595 , imp_methods :: [Name]
1596 -- ^ interface methods. When expanding implicits, these should be
1597 -- expanded even under binders
1598 , decoration :: Name -> Name
1600 , implicitAllowed :: Bool
1601 , constraintAllowed :: Bool
1602 , maxline :: Maybe Int
1603 , mut_nesting :: Int
1605 , syn_in_quasiquote :: Int
1606 , syn_toplevel :: Bool
1607 , withAppAllowed :: Bool
1608 } deriving (Show, Generic)
1610deriving instance Binary SyntaxInfo
1613defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1615expandNS :: SyntaxInfo -> Name -> Name
1616expandNS syn n@(NS _ _) = n
1617expandNS syn n = case syn_namespace syn of
1622-- For inferring types of things
1624bi = fileFC "builtin"
1625primfc = fileFC "(primitive)"
1627inferTy = sMN 0 "__Infer"
1628inferCon = sMN 0 "__infer"
1629inferDecl = PDatadecl inferTy primfc
1631 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1632 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1633 (PRef bi [] inferTy)), bi, [])]
1636infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1637infP = P (TCon 6 0) inferTy (TType (UVal 0))
1639getInferTerm, getInferType :: Term -> Term
1640getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1641getInferTerm (App _ (App _ _ _) tm) = tm
1642getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1644getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1645 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1646 toTy (PVar _ t) = PVTy t
1648getInferType (App _ (App _ _ ty) _) = ty
1652-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1654primNames = [inferTy, inferCon]
1657unitCon = sUN "MkUnit"
1659falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1660 "The empty type, also known as the trivially false proposition." ++
1662 "Use `void` or `absurd` to prove anything if you have a variable " ++
1663 "of type `Void` in scope."
1666pairTy = sNS (sUN "Pair") ["Builtins"]
1667pairCon = sNS (sUN "MkPair") ["Builtins"]
1669upairTy = sNS (sUN "UPair") ["Builtins"]
1670upairCon = sNS (sUN "MkUPair") ["Builtins"]
1674eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1675 "The propositional equality type. A proof that `x` = `y`." ++
1677 "To use such a proof, pattern-match on it, and the two equal things will " ++
1678 "then need to be the _same_ pattern." ++
1680 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1681 "is possible to state equalities between values of potentially different " ++
1682 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1684 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1686eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1687 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1689 [(reflDoc, reflParamDoc,
1690 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1691 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1692 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1693 pimp (n "B") Placeholder False,
1694 pexp (PRef bi [] (n "x")),
1695 pexp (PRef bi [] (n "x"))])), bi, [])]
1697 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1698 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1699 "shown that both sides are in fact equal."
1700 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1701 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1703eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1704 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1710-- | The special name to be used in the module documentation context -
1711-- not for use in the main definition context. The namespace around it
1712-- will determine the module to which the docs adhere.
1714modDocName = sMN 0 "ModuleDocs"
1716-- Defined in builtins.idr
1717sigmaTy = sNS (sUN "DPair") ["Builtins"]
1718sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1720piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1721piBind = piBindp expl
1723piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1725piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1728-- Pretty-printing declarations and terms
1730-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1731-- could interfere with interactive editing, which calls "show".
1733instance Show PTerm where
1734 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1736instance Show PDecl where
1737 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1739instance Show PClause where
1740 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1742instance Show PData where
1743 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1745instance Pretty PTerm OutputAnnotation where
1746 pretty = prettyImp defaultPPOption
1748-- | Colourise annotations according to an Idris state. It ignores the
1749-- names in the annotation, as there's no good way to show extended
1750-- information on a terminal.
1751annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1752annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1753annotationColour ist (AnnConst c) =
1754 let theme = idris_colourTheme ist
1755 in Just $ if constIsType c
1756 then typeColour theme
1757 else dataColour theme
1758annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1759annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1760annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1761annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1762annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1763annotationColour ist (AnnName n _ _ _) =
1764 let ctxt = tt_ctxt ist
1765 theme = idris_colourTheme ist
1767 _ | isDConName n ctxt -> Just $ dataColour theme
1768 _ | isFnName n ctxt -> Just $ functionColour theme
1769 _ | isTConName n ctxt -> Just $ typeColour theme
1770 _ | isPostulateName n ist -> Just $ postulateColour theme
1771 _ | otherwise -> Nothing -- don't colourise unknown names
1772annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1773 where colour BoldText = IdrisColour Nothing True False True False
1774 colour UnderlineText = IdrisColour Nothing True True False False
1775 colour ItalicText = IdrisColour Nothing True False False True
1776annotationColour ist _ = Nothing
1779-- | Colourise annotations according to an Idris state. It ignores the
1780-- names in the annotation, as there's no good way to show extended
1781-- information on a terminal. Note that strings produced this way will
1782-- not be coloured on Windows, so the use of the colour rendering
1783-- functions in Idris.Output is to be preferred.
1784consoleDecorate :: IState -> OutputAnnotation -> String -> String
1785consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1787isPostulateName :: Name -> IState -> Bool
1788isPostulateName n ist = S.member n (idris_postulates ist)
1790-- | Pretty-print a high-level closed Idris term with no information
1791-- about precedence/associativity
1792prettyImp :: PPOption -- ^ pretty printing options
1793 -> PTerm -- ^ the term to pretty-print
1794 -> Doc OutputAnnotation
1795prettyImp impl = pprintPTerm impl [] [] []
1797-- | Serialise something to base64 using its Binary implementation.
1799-- | Do the right thing for rendering a term in an IState
1800prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1801prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1803-- | Pretty-print a high-level Idris term in some bindings context
1805pprintPTerm :: PPOption -- ^ pretty printing options
1806 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1807 -> [Name] -- ^ names to always show in pi, even if not used
1808 -> [FixDecl] -- ^ Fixity declarations
1809 -> PTerm -- ^ the term to pretty-print
1810 -> Doc OutputAnnotation
1811pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1816 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1817 prettySe d p bnd (PQuote r) =
1818 text "![" <> pretty r <> text "]"
1819 prettySe d p bnd (PPatvar fc n) = pretty n
1821 | Just str <- slist d p bnd e = depth d str
1822 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1823 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1824 prettySe d p bnd (PLam fc n nfc ty sc) =
1825 let (ns, sc') = getLamNames [n] sc in
1826 depth d . bracket p startPrec . group . align . hang 2 $
1827 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1828 prettySe (decD d) startPrec ((n, False):bnd) sc'
1830 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1831 getLamNames acc sc = (reverse acc, sc)
1833 prettyBindingsOf [] t = text ""
1834 prettyBindingsOf [n] t = prettyBindingOf n t
1835 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1836 prettyBindingsOf ns t
1837 prettySe d p bnd (PLet fc n nfc ty v sc) =
1838 depth d . bracket p startPrec . group . align $
1839 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1840 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1841 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1843 depth d . bracket p startPrec . group $
1844 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1845 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1847 depth d . bracket p startPrec . group $
1848 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1849 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1850 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1851 || ppopt_pinames ppo && uname n =
1852 depth d . bracket p startPrec . group $
1853 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1854 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1856 depth d . bracket p startPrec . group $
1857 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1858 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1860 uname (UN n) = case str n of
1867 Static -> text "%static" <> space
1869 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1871 depth d . bracket p startPrec $
1872 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1873 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1874 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1875 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1877 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1878 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1879 showRig _ n = prettyBindingOf n True
1881 isPi (PPi (Exp{}) _ _ _ _) = True
1882 isPi (PPi _ _ _ _ sc) = isPi sc
1887 Static -> text "%static" <> space
1889 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1890 depth d . bracket p startPrec $
1891 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1892 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1893 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1894 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1895 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1896 depth d . bracket p startPrec $
1897 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1898 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1899 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1900 | basename neg == sUN "negate" =
1901 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1902 -- This case preserves the behavior of the former constructor PEq.
1903 -- It should be removed if feasible when the pretty-printing of infix
1904 -- operators in general is improved.
1905 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1906 | n == eqTy, ppopt_impl ppo =
1907 depth d . bracket p eqPrec $
1908 enclose lparen rparen eq <+>
1909 align (group (vsep (map (prettyArgS (decD d) bnd)
1912 depth d . bracket p eqPrec . align . group $
1913 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1914 where eq = annName eqTy (text "=")
1916 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1917 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1918 | UN nm <- basename f
1919 , not (ppopt_impl ppo) && null (getShowArgs args) =
1920 prettyName True (ppopt_impl ppo) bnd f
1921 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1922 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1923 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1924 | UN nm <- basename op
1926 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1927 case getShowArgs args of
1929 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1930 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1931 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1932 (l@(PExp{}) : r@(PExp{}) : rest) ->
1933 depth d . bracket p funcAppPrec $
1934 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1935 align (group (vsep (map (prettyArgS d bnd) rest)))
1936 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1937 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1938 f = getFixity (opStr op)
1940 Nothing -> funcAppPrec + 1
1941 Just (Infixl p') -> p'
1942 Just f' -> prec f' + 1
1944 Nothing -> funcAppPrec + 1
1945 Just (Infixr p') -> p'
1946 Just f' -> prec f' + 1
1947 inFix l r = align . group $
1948 (prettySe (decD d) left bnd l <+> opName False) <$>
1949 group (prettySe (decD d) right bnd r)
1950 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1951 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1952 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1953 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1954 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1955 let args = getShowArgs as
1956 fp = prettySe (decD d) (startPrec + 1) bnd f
1957 shownArgs = if ppopt_impl ppo then as else args
1959 depth d . bracket p funcAppPrec . group $
1962 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1963 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1964 prettySe d p bnd (PCase _ scr cases) =
1965 bracket p funcAppPrec $
1966 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1967 depth d (indent 2 (vsep (map ppcase cases)))
1969 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1970 ([(n, False) | n <- vars l] ++ bnd)
1971 in nest nestingSize $
1972 prettyCase l <+> text "=>" <+> prettyCase r
1973 -- Warning: this is a bit of a hack. At this stage, we don't have the
1974 -- global context, so we can't determine which names are constructors,
1975 -- which are types, and which are pattern variables on the LHS of the
1976 -- case pattern. We use the heuristic that names without a namespace
1977 -- are patvars, because right now case blocks in PTerms are always
1978 -- delaborated from TT before being sent to the pretty-printer. If they
1979 -- start getting printed directly, THIS WILL BREAK.
1980 -- Potential solution: add a list of known patvars to the cases in
1981 -- PCase, and have the delaborator fill it out, kind of like the pun
1982 -- disambiguation on PDPair.
1983 vars tm = filter noNS (allNamesIn tm)
1984 noNS (NS _ _) = False
1987 prettySe d p bnd (PIfThenElse _ c t f) =
1988 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1989 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1990 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1991 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1993 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1994 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1995 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1996 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1997 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1998 prettySe d p bnd (PRewrite _ by l r _) =
1999 depth d . bracket p startPrec $
2000 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
2003 Just fn -> text "using" <+>
2004 prettyName True (ppopt_impl ppo) bnd fn) <+>
2005 text "in" <+> prettySe (decD d) startPrec bnd r
2006 prettySe d p bnd (PTyped l r) =
2007 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
2008 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
2009 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
2010 align . group . vsep . punctuate (ann comma) $
2011 map (prettySe (decD d) startPrec bnd) elts
2012 where ann = case pun of
2014 IsType -> annName pairTy
2015 IsTerm -> annName pairCon
2016 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
2017 | Just elts <- dPairElts dpair
2018 = depth d . enclose (annotated lparen) (annotated rparen) .
2019 align . group . vsep . punctuate (space <> annotated (text "**")) $
2025 annotated (text "**") <+>
2026 prettySe (decD d) startPrec (addBinding bnd) r <>
2028 where annotated = case pun of
2029 IsType -> annName sigmaTy
2030 IsTerm -> annName sigmaCon
2033 (left, addBinding) = case (l, pun) of
2034 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
2035 _ -> (prettySe (decD d) startPrec bnd l, id)
2038 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
2039 ppElts ((PRef _ _ n, t):rs) bs
2041 = (bindingOf n False <+> colon <+>
2042 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2043 ppElts ((l, t):rs) bs
2044 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2045 prettySe d p bnd (PAlternative ns a as) =
2046 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2049 foldr ((\ l r -> l <+> text "," <+> r) .
2050 depth d . prettySe (decD d) startPrec bnd)
2052 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2053 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2054 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2055 -- XXX: add pretty for tactics
2056 prettySe d p bnd (PProof ts) =
2057 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2058 prettySe d p bnd (PTactics ts) =
2059 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2060 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2061 prettySe d p bnd PImpossible = kwd "impossible"
2062 prettySe d p bnd Placeholder = text "_"
2063 prettySe d p bnd (PDoBlock dos) =
2064 bracket p startPrec $
2065 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2066 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2067 ppdo bnd (DoBind _ bn _ tm : dos) =
2068 (prettyBindingOf bn False <+> text "<-" <+>
2069 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2070 ppdo ((bn, False):bnd) dos
2071 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2072 text "no pretty printer for pattern-matching do binding" :
2074 ppdo bnd (DoLet _ ln _ ty v : dos) =
2075 (kwd "let" <+> prettyBindingOf ln False <+>
2076 (if ty /= Placeholder
2077 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2079 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2080 ppdo ((ln, False):bnd) dos
2081 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2082 text "no pretty printer for pattern-matching do binding" :
2085 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2086 prettySe d p bnd (PElabError s) = pretty s
2087 -- Quasiquote pprinting ignores bound vars
2088 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2089 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2090 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2091 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2092 where start = if res then "`{" else "`{{"
2093 end = if res then "}" else "}}"
2094 prettySe d p bnd (PRunElab _ tm _) =
2095 bracket p funcAppPrec . group . align . hang 2 $
2097 prettySe (decD d) funcAppPrec bnd tm
2098 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2099 prettySe d p bnd _ = text "missing pretty-printer for term"
2101 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2102 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2103 where display (UN n) = T.unpack n
2104 display (MN _ n) = T.unpack n
2105 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2106 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2109 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2110 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2111 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2112 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2114 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2115 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2116 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2117 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2119 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2120 annName n = annotate (AnnName n Nothing Nothing Nothing)
2122 opStr :: Name -> String
2123 opStr (NS n _) = opStr n
2124 opStr (UN n) = T.unpack n
2126 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2127 slist' (Just d) _ _ _ | d <= 0 = Nothing
2129 | containsHole e = Nothing
2130 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2131 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2132 slist' d p bnd (PRef _ _ nil)
2133 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2134 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2135 | nsroot cons == sUN "::",
2136 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2138 Just tl' <- slist' (decD d) p bnd tl
2139 = Just (prettySe d startPrec bnd hd : tl')
2141 isImp (PImp {}) = True
2143 slist' _ _ _ tm = Nothing
2145 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2147 [] -> annotate (AnnData "" "") $ text "[]"
2148 [x] -> enclose left right . group $ x
2149 xs -> enclose left right .
2150 align . group . vsep .
2151 punctuate comma $ xs
2152 where left = (annotate (AnnData "" "") (text "["))
2153 right = (annotate (AnnData "" "") (text "]"))
2154 comma = (annotate (AnnData "" "") (text ","))
2155 slist _ _ _ _ = Nothing
2157 pairElts :: PTerm -> Maybe [PTerm]
2158 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2159 | otherwise = Just [x, y]
2160 pairElts _ = Nothing
2162 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2163 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2164 | otherwise = Just [(l, t), (Placeholder, r)]
2165 dPairElts _ = Nothing
2167 natns = "Prelude.Nat."
2169 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2171 | ppopt_desugarnats ppo = Nothing
2172 | otherwise = snat' d p e
2174 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2175 snat' (Just x) _ _ | x <= 0 = Nothing
2176 snat' d p (PRef _ _ z)
2177 | show z == (natns++"Z") || show z == "Z" = Just 0
2178 snat' d p (PApp _ s [PExp {getTm=n}])
2179 | show s == (natns++"S") || show s == "S",
2180 Just n' <- snat' (decD d) p n
2182 snat' _ _ _ = Nothing
2184 bracket outer inner doc
2185 | outer > inner = lparen <> doc <> rparen
2188 ellipsis = text "..."
2191 depth (Just d) = if d <= 0 then const ellipsis else id
2193 decD = fmap (\x -> x - 1)
2195 kwd = annotate AnnKeyword . text
2197 fixities :: M.Map String Fixity
2198 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2200 getFixity :: String -> Maybe Fixity
2201 getFixity = flip M.lookup fixities
2203-- | Strip away namespace information
2204basename :: Name -> Name
2205basename (NS n _) = basename n
2208-- | Determine whether a name was the one inserted for a hole or guess
2209-- by the delaborator
2210isHoleName :: Name -> Bool
2211isHoleName (UN n) = n == T.pack "[__]"
2214-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2215containsHole :: PTerm -> Bool
2216containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2218-- | Pretty-printer helper for names that attaches the correct annotations
2219prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2220 -> Bool -- ^ whether to show namespaces
2221 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2222 -> Name -- ^ the name to pprint
2223 -> Doc OutputAnnotation
2224prettyName infixParen showNS bnd n
2225 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2226 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2227 | (UN n') <- n, T.unpack n' == "_" = text "_"
2228 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2229 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2230 where fullName = text nameSpace <> parenthesise (text (baseName n))
2231 baseName (UN n) = T.unpack n
2232 baseName (NS n ns) = baseName n
2233 baseName (MN i s) = T.unpack s
2234 baseName other = show other
2235 nameSpace = case n of
2236 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2238 isInfix = case baseName n of
2240 (c : _) -> not (isAlpha c)
2241 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2244showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2245showCImp ppo (PClause _ n l ws r w)
2246 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2247 <+> text "where" <+> text (show w)
2250 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2251showCImp ppo (PWith _ n l ws r pn w)
2252 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2253 <+> braces (text (show w))
2256 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2259showDImp :: PPOption -> PData -> Doc OutputAnnotation
2260showDImp ppo (PDatadecl n nfc ty cons)
2261 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2262 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2264showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2265showDecls o ds = vsep (map (showDeclImp o) ds)
2267showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2268showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2269showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2270 indent 2 (vsep (map (showCImp o) cs))
2271showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2272showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2273showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2274showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2275showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2276showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2277 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2278showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2279 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2280showDeclImp _ _ = text "..."
2281-- showDeclImp (PImport o) = "import " ++ o
2283getImps :: [PArg] -> [(Name, PTerm)]
2285getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2286getImps (_ : xs) = getImps xs
2288getExps :: [PArg] -> [PTerm]
2290getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2291getExps (_ : xs) = getExps xs
2293getShowArgs :: [PArg] -> [PArg]
2295getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2296getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2297 | PImp _ _ _ _ tm <- e
2298 , containsHole tm = e : getShowArgs xs
2299getShowArgs (_ : xs) = getShowArgs xs
2301getConsts :: [PArg] -> [PTerm]
2303getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2304getConsts (_ : xs) = getConsts xs
2306getAll :: [PArg] -> [PTerm]
2311showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2312 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2313 -> PPOption -- ^ pretty printing options
2314 -> Bool -- ^ whether to colourise
2315 -> Name -- ^ the term to show
2317showName ist bnd ppo colour n = case ist of
2318 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2319 Nothing -> showbasic n
2320 where name = if ppopt_impl ppo then show n else showbasic n
2321 showbasic n@(UN _) = showCG n
2322 showbasic (MN i s) = str s
2323 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2324 showbasic (SN s) = show s
2326 colourise n t = let ctxt' = fmap tt_ctxt ist in
2329 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2330 else colouriseBound t name
2331 | isDConName n ctxt -> colouriseData t name
2332 | isFnName n ctxt -> colouriseFun t name
2333 | isTConName n ctxt -> colouriseType t name
2334 -- The assumption is that if a name is not bound and does not exist in the
2335 -- global context, then we're somewhere in which implicit info has been lost
2336 -- (like error messages). Thus, unknown vars are colourised as implicits.
2337 | otherwise -> colouriseImplicit t name
2339showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2340 -> PTerm -- ^ the term to show
2342showTm ist = displayDecorated (consoleDecorate ist) .
2343 renderPretty 0.8 100000 .
2344 prettyImp (ppOptionIst ist)
2346-- | Show a term with implicits, no colours
2347showTmImpls :: PTerm -> String
2348showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2350-- | Show a term with specific options
2351showTmOpts :: PPOption -> PTerm -> String
2352showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2355instance Sized PTerm where
2356 size (PQuote rawTerm) = size rawTerm
2357 size (PRef fc _ name) = size name
2358 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2359 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2360 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2361 size (PTyped trm ty) = 1 + size trm + size ty
2362 size (PApp fc name args) = 1 + size args
2363 size (PAppBind fc name args) = 1 + size args
2364 size (PCase fc trm bdy) = 1 + size trm + size bdy
2365 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2366 size (PTrue fc _) = 1
2367 size (PResolveTC fc) = 1
2368 size (PRewrite fc by left right _) = 1 + size left + size right
2369 size (PPair fc _ _ left right) = 1 + size left + size right
2370 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2371 size (PAlternative _ a alts) = 1 + size alts
2372 size (PHidden hidden) = size hidden
2373 size (PUnifyLog tm) = size tm
2374 size (PDisamb _ tm) = size tm
2375 size (PNoImplicits tm) = size tm
2377 size (PUniverse _ _) = 1
2378 size (PConstant fc const) = 1 + size fc + size const
2379 size Placeholder = 1
2380 size (PDoBlock dos) = 1 + size dos
2381 size (PIdiom fc term) = 1 + size term
2382 size (PMetavar _ name) = 1
2383 size (PProof tactics) = size tactics
2384 size (PElabError err) = size err
2385 size PImpossible = 1
2388getPArity :: PTerm -> Int
2389getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2392-- Return all names, free or globally bound, in the given term.
2394allNamesIn :: PTerm -> [Name]
2395allNamesIn tm = nub $ ni 0 [] tm
2396 where -- TODO THINK added niTacImp, but is it right?
2397 ni 0 env (PRef _ _ n)
2398 | not (n `elem` env) = [n]
2399 ni 0 env (PPatvar _ n) = [n]
2400 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2401 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2402 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2403 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2404 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2405 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2406 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2407 ni 0 env (PHidden tm) = ni 0 env tm
2408 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2409 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2410 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2411 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2412 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2413 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2414 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2415 ni 0 env (PUnifyLog tm) = ni 0 env tm
2416 ni 0 env (PDisamb _ tm) = ni 0 env tm
2417 ni 0 env (PNoImplicits tm) = ni 0 env tm
2419 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2420 ni i env (PUnquote tm) = ni (i - 1) env tm
2421 ni i env tm = concatMap (ni i env) (children tm)
2423 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2427-- Return all names defined in binders in the given term
2428boundNamesIn :: PTerm -> [Name]
2429boundNamesIn tm = S.toList (ni 0 S.empty tm)
2430 where -- TODO THINK Added niTacImp, but is it right?
2431 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2432 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2433 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2434 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2435 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2436 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2437 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2438 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2439 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2440 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2441 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2442 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2443 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2444 ni 0 set (PAlternative ns a as) = niTms 0 set as
2445 ni 0 set (PHidden tm) = ni 0 set tm
2446 ni 0 set (PUnifyLog tm) = ni 0 set tm
2447 ni 0 set (PDisamb _ tm) = ni 0 set tm
2448 ni 0 set (PNoImplicits tm) = ni 0 set tm
2450 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2451 ni i set (PUnquote tm) = ni (i - 1) set tm
2453 ni i set tm = foldr (S.union . ni i set) set (children tm)
2455 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2456 niTms i set [] = set
2457 niTms i set (x : xs) = niTms i (ni i set x) xs
2459 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2460 niTacImp i set _ = set
2462-- Return names which are valid implicits in the given term (type).
2463implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2464implicitNamesIn uvars ist tm
2465 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2468 addImp n = do (imps, fns) <- get
2470 addFn n = do (imps, fns) <- get
2474 notCAF (PExp _ _ _ _ : _) = True
2475 notCAF (_ : xs) = notCAF xs
2477 notHidden (n, _) = case getAccessibility n of
2483 = case lookupDefAccExact n False (tt_ctxt ist) of
2487 ni 0 env (PRef _ _ n@(NS _ _))
2488 | not (n `elem` env)
2489 -- Never implicitly bind if there's a namespace
2491 ni 0 env (PRef _ _ n)
2492 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2493 ni 0 env (PApp _ f@(PRef _ _ n) as)
2494 | n `elem` uvars = do ni 0 env f
2495 mapM_ (ni 0 env . getTm) as
2496 | otherwise = do case lookupTy n (tt_ctxt ist) of
2499 mapM_ (ni 0 env . getTm) as
2500 ni 0 env (PApp _ f as) = do ni 0 env f
2501 mapM_ (ni 0 env . getTm) as
2502 ni 0 env (PAppBind _ f as) = do ni 0 env f
2503 mapM_ (ni 0 env . getTm) as
2504 ni 0 env (PCase _ c os) = do ni 0 env c
2505 -- names in 'os', not counting the names bound in the cases
2506 mapM_ (ni 0 env . snd) os
2509 mapM_ (ni 0 env . fst) os
2511 put (nub imps \\ nub impsfst, fns)
2512 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2513 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2514 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2515 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2516 ni 0 env val; ni 0 (n:env) sc
2517 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2518 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2519 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2520 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2521 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2524 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2525 ni 0 env (PHidden tm) = ni 0 env tm
2526 ni 0 env (PUnifyLog tm) = ni 0 env tm
2527 ni 0 env (PDisamb _ tm) = ni 0 env tm
2528 ni 0 env (PNoImplicits tm) = ni 0 env tm
2530 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2531 maybe (return ()) (ni i env) ty
2532 ni i env (PUnquote tm) = ni (i - 1) env tm
2534 ni i env tm = mapM_ (ni i env) (children tm)
2536-- Return names which are free in the given term.
2537namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2538namesIn uvars ist tm = nub $ ni 0 [] tm
2540 ni 0 env (PRef _ _ n)
2541 | not (n `elem` env)
2542 = case lookupTy n (tt_ctxt ist) of
2544 _ -> [n | n `elem` (map fst uvars)]
2545 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2546 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2547 ni 0 env (PCase _ c os) = ni 0 env c ++
2548 -- names in 'os', not counting the names bound in the cases
2549 (nub (concatMap (ni 0 env . snd) os)
2550 \\ nub (concatMap (ni 0 env . fst) os))
2551 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2552 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2553 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2554 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2555 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2556 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2557 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2558 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2559 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2560 ni 0 env (PHidden tm) = ni 0 env tm
2561 ni 0 env (PUnifyLog tm) = ni 0 env tm
2562 ni 0 env (PDisamb _ tm) = ni 0 env tm
2563 ni 0 env (PNoImplicits tm) = ni 0 env tm
2565 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2566 ni i env (PUnquote tm) = ni (i - 1) env tm
2568 ni i env tm = concatMap (ni i env) (children tm)
2570 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2573-- Return which of the given names are used in the given term.
2575usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2576usedNamesIn vars ist tm = nub $ ni 0 [] tm
2577 where -- TODO THINK added niTacImp, but is it right?
2578 ni 0 env (PRef _ _ n)
2579 | n `elem` vars && not (n `elem` env)
2580 = case lookupDefExact n (tt_ctxt ist) of
2583 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2584 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2585 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2586 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2587 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2588 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2589 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2590 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2591 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2592 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2593 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2594 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2595 ni 0 env (PHidden tm) = ni 0 env tm
2596 ni 0 env (PUnifyLog tm) = ni 0 env tm
2597 ni 0 env (PDisamb _ tm) = ni 0 env tm
2598 ni 0 env (PNoImplicits tm) = ni 0 env tm
2600 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2601 ni i env (PUnquote tm) = ni (i - 1) env tm
2603 ni i env tm = concatMap (ni i env) (children tm)
2605 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2608-- Return the list of inaccessible (= dotted) positions for a name.
2609getErasureInfo :: IState -> Name -> [Int]
2610getErasureInfo ist n =
2611 case lookupCtxtExact n (idris_optimisation ist) of
2612 Just (Optimise inacc _ _) -> map fst inacc
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list