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]
153defaultOptimise = [PETransform]
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!
531 | Port REPLPort -- ^ REPL TCP port
540 | PkgDocBuild String -- IdrisDoc
541 | PkgDocInstall String
551 | OutputTy OutputType
552 | Extension LanguageExt
553 | InterpretScript String
555 | TargetTriple String
558 | AddOpt Optimisation
559 | RemoveOpt Optimisation
562 | AutoWidth -- ^ Automatically adjust terminal width
563 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
564 | UseConsoleWidth ConsoleWidth
567 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
568 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
569 deriving (Show, Eq, Generic)
571data REPLPort = DontListen | ListenPort PortNumber
572 deriving (Eq, Generic, Show)
574-- Parsed declarations
576data Fixity = Infixl { prec :: Int }
577 | Infixr { prec :: Int }
578 | InfixN { prec :: Int }
579 | PrefixN { prec :: Int }
580 deriving (Eq, Generic)
582deriving instance Binary Fixity
585instance Show Fixity where
586 show (Infixl i) = "infixl " ++ show i
587 show (Infixr i) = "infixr " ++ show i
588 show (InfixN i) = "infix " ++ show i
589 show (PrefixN i) = "prefix " ++ show i
591data FixDecl = Fix Fixity String
592 deriving (Eq, Generic)
594instance Show FixDecl where
595 show (Fix f s) = show f ++ " " ++ s
598deriving instance Binary FixDecl
601instance Ord FixDecl where
602 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
605data Static = Static | Dynamic
606 deriving (Show, Eq, Ord, Data, Generic, Typeable)
608deriving instance Binary Static
611-- ^ Mark bindings with their explicitness, and laziness
612data Plicity = Imp { pargopts :: [ArgOpt]
615 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
616 , pinsource :: Bool -- ^ Explicitly written in source
619 | Exp { pargopts :: [ArgOpt]
621 , pparam :: Bool -- ^ this is a param (rather than index)
624 | Constraint { pargopts :: [ArgOpt]
628 | TacImp { pargopts :: [ArgOpt]
633 deriving (Show, Eq, Ord, Data, Generic, Typeable)
636deriving instance Binary Plicity
639is_scoped :: Plicity -> Maybe ImplicitInfo
640is_scoped (Imp _ _ _ s _ _) = s
645impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
646-- Machine generated top level implicit
648impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
652forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
653forall_constraint :: Plicity
654forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
657expl = Exp [] Dynamic False RigW
659expl_param = Exp [] Dynamic True RigW
662constraint = Constraint [] Static RigW
664tacimpl :: PTerm -> Plicity
665tacimpl t = TacImp [] Dynamic t RigW
667data FnOpt = Inlinable -- ^ always evaluate when simplifying
668 | TotalFn | PartialFn | CoveringFn
669 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
672 -- | interface dictionary, eval only when a function
673 -- argument, and further evaluation results.
675 | OverlappingDictionary -- ^ Interface dictionary which may overlap
676 | Implicit -- ^ implicit coercion
677 | NoImplicit -- ^ do not apply implicit coercions
678 | CExport String -- ^ export, with a C name
679 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
680 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
681 | ErrorReduce -- ^ unfold definition before showing an error
682 | Reflection -- ^ a reflecting function, compile-time only
683 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
684 | UnfoldIface Name [Name]
685 -- ^ Unfold given interface name in the definition, the
686 -- top level methods, and anything which has
687 -- the interface name as an argument. This is to unfold
688 -- things for termination checking, as interfaces will otherwise
690 | Constructor -- ^ Data constructor type
691 | AutoHint -- ^ use in auto implicit search
692 | PEGenerated -- ^ generated by partial evaluator
693 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
694 deriving (Show, Eq, Generic)
696deriving instance Binary FnOpt
701inlinable :: FnOpts -> Bool
702inlinable = elem Inlinable
704dictionary :: FnOpts -> Bool
705dictionary = elem Dictionary
708-- | Type provider - what to provide
709data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
710 | ProvPostulate t -- ^ goal type must be Type, so only term
711 deriving (Show, Eq, Functor, Generic)
713type ProvideWhat = ProvideWhat' PTerm
715-- | Top-level declarations such as compiler directives, definitions,
716-- datatypes and interfaces.
718 -- | Fixity declaration
719 = PFix FC Fixity [String]
720 -- | Type declaration (last FC is precise name location)
721 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
722 -- | Postulate, second FC is precise name location
723 | PPostulate Bool -- external def if true
724 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
726 | PClauses FC FnOpts Name [PClause' t]
727 -- | Top level constant
729 -- | Data declaration.
730 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
732 | PParams FC [(Name, t)] [PDecl' t]
733 -- | Open block/declaration
734 | POpenInterfaces FC [Name] [PDecl' t]
735 -- | New namespace, where FC is accurate location of the namespace
737 | PNamespace String FC [PDecl' t]
739 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
741 FC -- Record name precise location
742 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
743 [(Name, Docstring (Either Err t))] -- Param Docs
744 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
745 (Maybe (Name, FC)) -- Optional constructor name and location
746 (Docstring (Either Err t)) -- Constructor doc
747 SyntaxInfo -- Constructor SyntaxInfo
749 -- | Interface: arguments are documentation, syntax info, source
750 -- location, constraints, interface name, interface name location,
751 -- parameters, method declarations, optional constructor name
752 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
753 [(Name, t)] -- constraints
754 Name -- interface name
755 FC -- accurate location of interface name
756 [(Name, FC, t)] -- parameters and precise locations
757 [(Name, Docstring (Either Err t))] -- parameter docstrings
758 [(Name, FC)] -- determining parameters and precise locations
759 [PDecl' t] -- declarations
760 (Maybe (Name, FC)) -- implementation constructor name and location
761 (Docstring (Either Err t)) -- implementation constructor docs
763 -- | Implementation declaration: arguments are documentation, syntax
764 -- info, source location, constraints, interface name, parameters, full
765 -- Implementation type, optional explicit name, and definitions
766 | PImplementation (Docstring (Either Err t)) -- Implementation docs
767 [(Name, Docstring (Either Err t))] -- Parameter docs
769 FC [(Name, t)] -- constraints
770 [Name] -- parent dictionaries to search for constraints
774 FC -- precise location of interface
776 [(Name, t)] -- Extra names in scope in the body
777 t -- full Implementation type
778 (Maybe Name) -- explicit name
780 | PDSL Name (DSL' t) -- ^ DSL declaration
781 | PSyntax FC Syntax -- ^ Syntax definition
782 | PMutual FC [PDecl' t] -- ^ Mutual block
783 | PDirective Directive -- ^ Compiler directive.
785 -- | Type provider. The first t is the type, the second is the
786 -- term. The second FC is precise highlighting location.
787 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
789 -- | Source-to-source transformation rule. If bool is True, lhs and
790 -- rhs must be convertible.
791 | PTransform FC Bool t t
793 -- | FC is decl-level, for errors, and Strings represent the
795 | PRunElabDecl FC t [String]
796 deriving (Functor, Generic)
798deriving instance Binary PDecl'
801-- | The set of source directives
802data Directive = DLib Codegen String
803 | DLink Codegen String
804 | DFlag Codegen String
805 | DInclude Codegen String
810 | DSetTotal Name -- assert totality after checking
811 | DAccess Accessibility
812 | DDefault DefaultTotality
814 | DDynamicLibs [String]
815 | DNameHint Name FC [(Name, FC)]
816 | DErrorHandlers Name FC Name FC [(Name, FC)]
817 | DLanguage LanguageExt
818 | DDeprecate Name String
819 | DFragile Name String
820 | DAutoImplicits Bool
824-- | A set of instructions for things that need to happen in IState
825-- after a term elaboration when there's been reflected elaboration.
826data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
827 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
828 | RAddImplementation Name Name
829 | RDatatypeDeclInstrs Name [PArg]
830 -- | Datatype, constructors
831 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
834-- | For elaborator state
835data EState = EState {
836 case_decls :: [(Name, PDecl)]
837 , delayed_elab :: [(Int, Elab' EState ())]
838 , new_tyDecls :: [RDeclInstructions]
839 , highlighting :: [(FC, OutputAnnotation)]
840 , auto_binds :: [Name] -- ^ names bound as auto implicits
841 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
845initEState = EState [] [] [] [] [] []
847type ElabD a = Elab' EState a
849highlightSource :: FC -> OutputAnnotation -> ElabD ()
850highlightSource fc annot =
851 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
853-- | One clause of a top-level definition. Term arguments to constructors are:
855-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
857-- 2. The list of extra 'with' patterns
859-- 3. The right-hand side
861-- 4. The where block (PDecl' t)
863data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
864 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
865 | PClauseR FC [t] t [PDecl' t]
866 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
867 deriving (Functor, Generic)
869deriving instance Binary PClause'
874 -- | Data declaration
875 PDatadecl { d_name :: Name -- ^ The name of the datatype
876 , d_name_fc :: FC -- ^ The precise location of the type constructor name
877 , d_tcon :: t -- ^ Type constructor
878 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
880 -- | "Placeholder" for data whose constructors are defined later
881 | PLaterdecl { d_name :: Name
884 } deriving (Functor, Generic)
886-- | Transform the FCs in a PData and its associated terms. The first
887-- function transforms the general-purpose FCs, and the second
888-- transforms those that are used for semantic source highlighting, so
889-- they can be treated specially.
890mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
891mapPDataFC f g (PDatadecl n nfc tycon ctors) =
892 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
893 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
894 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
895mapPDataFC f g (PLaterdecl n nfc tycon) =
896 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
898deriving instance Binary PData'
901-- Handy to get a free function for applying PTerm -> PTerm functions
902-- across a program, by deriving Functor
904type PDecl = PDecl' PTerm
905type PData = PData' PTerm
906type PClause = PClause' PTerm
908-- | Transform the FCs in a PTerm. The first function transforms the
909-- general-purpose FCs, and the second transforms those that are used
910-- for semantic source highlighting, so they can be treated specially.
911mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
912mapPDeclFC f g (PFix fc fixity ops) =
913 PFix (f fc) fixity ops
914mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
915 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
916mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
917 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
919mapPDeclFC f g (PClauses fc opts n clauses) =
920 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
921mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
922mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
923 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
924mapPDeclFC f g (PParams fc params decls) =
926 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
927 (map (mapPDeclFC f g) decls)
928mapPDeclFC f g (POpenInterfaces fc ifs decls) =
929 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
930mapPDeclFC f g (PNamespace ns fc decls) =
931 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
932mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
933 PRecord doc syn (f fc) opts n (g nfc)
934 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
936 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
937 plic, mapPTermFC f g ty, fdoc))
939 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
942mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
943 PInterface doc syn (f fc)
944 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
945 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
946 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
947 (map (mapPDeclFC f g) body)
948 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
950mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
951 PImplementation doc paramDocs syn (f fc)
952 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
953 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
954 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
955 (mapPTermFC f g implTy)
957 (map (mapPDeclFC f g) body)
958mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
959mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
961 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
962 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
963mapPDeclFC f g (PMutual fc decls) =
964 PMutual (f fc) (map (mapPDeclFC f g) decls)
965mapPDeclFC f g (PDirective d) =
968 DNameHint n nfc ns ->
969 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
970 DErrorHandlers n nfc n' nfc' ns ->
971 DErrorHandlers n (g nfc) n' (g nfc') $
972 map (\(an, anfc) -> (an, g anfc)) ns
973mapPDeclFC f g (PProvider doc syn fc nfc what n) =
974 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
975mapPDeclFC f g (PTransform fc safe l r) =
976 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
977mapPDeclFC f g (PRunElabDecl fc script ns) =
978 PRunElabDecl (f fc) (mapPTermFC f g script) ns
980-- | Get all the names declared in a declaration
981declared :: PDecl -> [Name]
982declared (PFix _ _ _) = []
983declared (PTy _ _ _ _ _ n fc t) = [n]
984declared (PPostulate _ _ _ _ _ _ n t) = [n]
985declared (PClauses _ _ n _) = [] -- not a declaration
986declared (PCAF _ n _) = [n]
987declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
988 where fstt (_, _, a, _, _, _, _) = a
989declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
990declared (PParams _ _ ds) = concatMap declared ds
991declared (POpenInterfaces _ _ ds) = concatMap declared ds
992declared (PNamespace _ _ ds) = concatMap declared ds
993declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
994declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
995declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
999declared (PDSL n _) = [n]
1000declared (PSyntax _ _) = []
1001declared (PMutual _ ds) = concatMap declared ds
1002declared (PDirective _) = []
1005-- get the names declared, not counting nested parameter blocks
1006tldeclared :: PDecl -> [Name]
1007tldeclared (PFix _ _ _) = []
1008tldeclared (PTy _ _ _ _ _ n _ t) = [n]
1009tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
1010tldeclared (PClauses _ _ n _) = [] -- not a declaration
1011tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1012tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1013 where fstt (_, _, a, _, _, _, _) = a
1014tldeclared (PParams _ _ ds) = []
1015tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
1016tldeclared (PMutual _ ds) = concatMap tldeclared ds
1017tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
1018tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
1019tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1025defined :: PDecl -> [Name]
1026defined (PFix _ _ _) = []
1027defined (PTy _ _ _ _ _ n _ t) = []
1028defined (PPostulate _ _ _ _ _ _ n t) = []
1029defined (PClauses _ _ n _) = [n] -- not a declaration
1030defined (PCAF _ n _) = [n]
1031defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1032 where fstt (_, _, a, _, _, _, _) = a
1033defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1034defined (PParams _ _ ds) = concatMap defined ds
1035defined (POpenInterfaces _ _ ds) = concatMap defined ds
1036defined (PNamespace _ _ ds) = concatMap defined ds
1037defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1038defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1039defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1043defined (PDSL n _) = [n]
1044defined (PSyntax _ _) = []
1045defined (PMutual _ ds) = concatMap defined ds
1046defined (PDirective _) = []
1049updateN :: [(Name, Name)] -> Name -> Name
1050updateN ns n | Just n' <- lookup n ns = n'
1053updateNs :: [(Name, Name)] -> PTerm -> PTerm
1055updateNs ns t = mapPT updateRef t
1056 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1059-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1060-- updateDNs [] t = t
1061-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1062-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1063-- where updateCNs ns (PClause n l ts r ds)
1064-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1065-- (map (fmap (updateNs ns)) ts)
1066-- (fmap (updateNs ns) r)
1067-- (map (updateDNs ns) ds)
1068-- updateDNs ns c = c
1070data PunInfo = IsType
1073 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1075-- | High level language terms
1076data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1077 -- high-level language
1079 -- ^ A reference to a variable. The FC is its precise
1080 -- source location for highlighting. The list of FCs is a
1081 -- collection of additional highlighting locations.
1082 | PInferRef FC [FC] Name -- ^ A name to be defined later
1083 | PPatvar FC Name -- ^ A pattern variable
1084 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1085 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1086 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1087 | PTyped PTerm PTerm -- ^ Term with explicit type
1088 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1089 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1090 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1091 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1092 | PMatchApp FC Name -- ^ Make an application by type matching
1093 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1094 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1095 | PTrue FC PunInfo -- ^ Unit type..?
1096 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1097 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1098 -- ^ "rewrite" syntax, with optional rewriting function and
1099 -- optional result type
1100 | PPair FC [FC] PunInfo PTerm PTerm
1101 -- ^ A pair (a, b) and whether it's a product type or a
1102 -- pair (solved by elaboration). The list of FCs is its
1104 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1105 -- ^ A dependent pair (tm : a ** b) and whether it's a
1106 -- sigma type or a pair that inhabits one (solved by
1107 -- elaboration). The [FC] is its punctuation.
1108 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1109 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1110 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1111 | PType FC -- ^ 'Type' type
1112 | PUniverse FC Universe -- ^ Some universe
1113 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1114 | PConstant FC Const -- ^ Builtin types
1115 | Placeholder -- ^ Underscore
1116 | PDoBlock [PDo] -- ^ Do notation
1117 | PIdiom FC PTerm -- ^ Idiom brackets
1118 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1119 | PProof [PTactic] -- ^ Proof script
1120 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1121 | PElabError Err -- ^ Error to report on elaboration
1122 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1123 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1124 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1125 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1126 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1127 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1128 | PUnquote PTerm -- ^ ~Term
1129 | PQuoteName Name Bool FC
1130 -- ^ `{n} where the FC is the precise highlighting for
1131 -- the name in particular. If the Bool is False, then
1132 -- it's `{{n}} and the name won't be resolved.
1133 | PRunElab FC PTerm [String]
1134 -- ^ %runElab tm - New-style proof script. Args are
1135 -- location, script, enclosing namespace.
1136 | PConstSugar FC PTerm
1137 -- ^ A desugared constant. The FC is a precise source
1138 -- location that will be used to highlight it later.
1139 deriving (Eq, Ord, Data, Typeable, Generic)
1141data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1144 deriving (Eq, Ord, Data, Generic, Typeable)
1146-- | Transform the FCs in a PTerm. The first function transforms the
1147-- general-purpose FCs, and the second transforms those that are used
1148-- for semantic source highlighting, so they can be treated specially.
1149mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1150mapPTermFC f g (PQuote q) = PQuote q
1151mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1152mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1153mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1154mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1155mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1156mapPTermFC 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)
1157mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1158mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1159mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1160mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1161mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1162mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1163mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1164mapPTermFC 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)
1165mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1166mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1167mapPTermFC 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)
1168mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1169mapPTermFC 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)
1170mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1171mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1172mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1173mapPTermFC f g (PType fc) = PType (f fc)
1174mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1175mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1176mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1177mapPTermFC f g Placeholder = Placeholder
1178mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1179 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1180 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1181 mapPDoFC (DoBindP fc t1 t2 alts) =
1182 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1183 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1184 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1185mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1186mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1187mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1188mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1189mapPTermFC f g (PElabError err) = PElabError err
1190mapPTermFC f g PImpossible = PImpossible
1191mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1192mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1193mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1194mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1195mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1196mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1197mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1198mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1199mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1202dg instance Binary PTerm
1205mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1206mapPT f t = f (mpt t) where
1207 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1208 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1209 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1210 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1211 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1212 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1213 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1214 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1215 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1216 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1217 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1218 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1219 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1220 mpt (PHidden t) = PHidden (mapPT f t)
1221 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1222 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1223 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1224 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1225 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1226 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1227 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1231data PTactic' t = Intro [Name] | Intros | Focus Name
1232 | Refine Name [Bool] | Rewrite t | DoUnify
1239 | LetTac Name t | LetTacTy Name t t
1240 | Exact t | Compute | Trivial | TCImplementation
1241 | ProofSearch Bool Bool Int (Maybe Name)
1242 [Name] -- allowed local names
1244 -- ^ the bool is whether to search recursively
1247 | ProofState | ProofTerm | Undo
1248 | Try (PTactic' t) (PTactic' t)
1249 | TSeq (PTactic' t) (PTactic' t)
1250 | ApplyTactic t -- see Language.Reflection module
1254 | GoalType String (PTactic' t)
1257 | TDocStr (Either Name Const)
1260 | TFail [ErrorReportPart]
1263 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1265deriving instance Binary PTactic'
1267instance Sized a => Sized (PTactic' a) where
1268 size (Intro nms) = 1 + size nms
1270 size (Focus nm) = 1 + size nm
1271 size (Refine nm bs) = 1 + size nm + length bs
1272 size (Rewrite t) = 1 + size t
1273 size (Induction t) = 1 + size t
1274 size (LetTac nm t) = 1 + size nm + size t
1275 size (Exact t) = 1 + size t
1283 size (Try l r) = 1 + size l + size r
1284 size (TSeq l r) = 1 + size l + size r
1285 size (ApplyTactic t) = 1 + size t
1286 size (Reflect t) = 1 + size t
1287 size (Fill t) = 1 + size t
1291 size (TFail ts) = 1 + size ts
1294 size (CaseTac x) = 1 + size x
1295 size (Equiv t) = 1 + size t
1296 size (Claim x y) = 1 + size x + size y
1298 size (MatchRefine x) = 1 + size x
1299 size (LetTacTy x y z) = 1 + size x + size y + size z
1300 size TCImplementation = 1
1302type PTactic = PTactic' PTerm
1304data PDo' t = DoExp FC t
1305 | DoBind FC Name FC t -- ^ second FC is precise name location
1306 | DoBindP FC t t [(t,t)]
1307 | DoLet FC Name FC t t -- ^ second FC is precise name location
1309 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1311deriving instance Binary PDo'
1314instance Sized a => Sized (PDo' a) where
1315 size (DoExp fc t) = 1 + size fc + size t
1316 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1317 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1318 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1319 size (DoLetP fc l r) = 1 + size fc + size l + size r
1321type PDo = PDo' PTerm
1323-- The priority gives a hint as to elaboration order. Best to elaborate
1324-- things early which will help give a more concrete type to other
1325-- variables, e.g. a before (interpTy a).
1327data PArg' t = PImp { priority :: Int
1328 , machine_inf :: Bool -- ^ true if the machine inferred it
1329 , argopts :: [ArgOpt]
1333 | PExp { priority :: Int
1334 , argopts :: [ArgOpt]
1338 | PConstraint { priority :: Int
1339 , argopts :: [ArgOpt]
1343 | PTacImplicit { priority :: Int
1344 , argopts :: [ArgOpt]
1349 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1351data ArgOpt = AlwaysShow
1355 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1357instance Sized a => Sized (PArg' a) where
1358 size (PImp p _ l nm trm) = 1 + size nm + size trm
1359 size (PExp p l nm trm) = 1 + size nm + size trm
1360 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1361 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1364deriving instance Binary PArg'
1367pimp n t mach = PImp 1 mach [] n t
1368pexp t = PExp 1 [] (sMN 0 "arg") t
1369pconst t = PConstraint 1 [] (sMN 0 "carg") t
1370ptacimp n s t = PTacImplicit 2 [] n s t
1372type PArg = PArg' PTerm
1374-- | Get the highest FC in a term, if one exists
1375highestFC :: PTerm -> Maybe FC
1376highestFC (PQuote _) = Nothing
1377highestFC (PRef fc _ _) = Just fc
1378highestFC (PInferRef fc _ _) = Just fc
1379highestFC (PPatvar fc _) = Just fc
1380highestFC (PLam fc _ _ _ _) = Just fc
1381highestFC (PPi _ _ _ _ _) = Nothing
1382highestFC (PLet fc _ _ _ _ _) = Just fc
1383highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1384highestFC (PApp fc _ _) = Just fc
1385highestFC (PAppBind fc _ _) = Just fc
1386highestFC (PMatchApp fc _) = Just fc
1387highestFC (PCase fc _ _) = Just fc
1388highestFC (PIfThenElse fc _ _ _) = Just fc
1389highestFC (PTrue fc _) = Just fc
1390highestFC (PResolveTC fc) = Just fc
1391highestFC (PRewrite fc _ _ _ _) = Just fc
1392highestFC (PPair fc _ _ _ _) = Just fc
1393highestFC (PDPair fc _ _ _ _ _) = Just fc
1394highestFC (PAs fc _ _) = Just fc
1395highestFC (PAlternative _ _ args) =
1396 case mapMaybe highestFC args of
1399highestFC (PHidden _) = Nothing
1400highestFC (PType fc) = Just fc
1401highestFC (PUniverse _ _) = Nothing
1402highestFC (PGoal fc _ _ _) = Just fc
1403highestFC (PConstant fc _) = Just fc
1404highestFC Placeholder = Nothing
1405highestFC (PDoBlock lines) =
1406 case map getDoFC lines of
1410 getDoFC (DoExp fc t) = fc
1411 getDoFC (DoBind fc nm nfc t) = fc
1412 getDoFC (DoBindP fc l r alts) = fc
1413 getDoFC (DoLet fc nm nfc l r) = fc
1414 getDoFC (DoLetP fc l r) = fc
1416highestFC (PIdiom fc _) = Just fc
1417highestFC (PMetavar fc _) = Just fc
1418highestFC (PProof _) = Nothing
1419highestFC (PTactics _) = Nothing
1420highestFC (PElabError _) = Nothing
1421highestFC PImpossible = Nothing
1422highestFC (PCoerced tm) = highestFC tm
1423highestFC (PDisamb _ opts) = highestFC opts
1424highestFC (PUnifyLog tm) = highestFC tm
1425highestFC (PNoImplicits tm) = highestFC tm
1426highestFC (PQuasiquote _ _) = Nothing
1427highestFC (PUnquote tm) = highestFC tm
1428highestFC (PQuoteName _ _ fc) = Just fc
1429highestFC (PRunElab fc _ _) = Just fc
1430highestFC (PConstSugar fc _) = Just fc
1431highestFC (PAppImpl t _) = highestFC t
1435data InterfaceInfo = CI {
1436 implementationCtorName :: Name
1437 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1438 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1439 , interface_default_super_interfaces :: [PDecl]
1440 , interface_impparams :: [Name]
1441 , interface_params :: [Name]
1442 , interface_constraints :: [PTerm]
1443 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1444 , interface_determiners :: [Int]
1445 } deriving (Show, Generic)
1447deriving instance Binary InterfaceInfo
1451data RecordInfo = RI {
1452 record_parameters :: [(Name,PTerm)]
1453 , record_constructor :: Name
1454 , record_projections :: [Name]
1455 } deriving (Show, Generic)
1457-- Type inference data
1459data TIData = TIPartial -- ^ a function with a partially defined type
1460 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1461 deriving (Show, Generic)
1463-- | Miscellaneous information about functions
1464data FnInfo = FnInfo { fn_params :: [Int] }
1465 deriving (Show, Generic)
1467deriving instance Binary FnInfo
1470data OptInfo = Optimise {
1471 inaccessible :: [(Int,Name)] -- includes names for error reporting
1472 , detaggable :: Bool
1473 , forceable :: [Int] -- argument positions which are forced by other values
1474 } deriving (Show, Generic)
1476deriving instance Binary OptInfo
1479-- | Syntactic sugar info
1484 , dsl_var :: Maybe t
1485 , index_first :: Maybe t
1486 , index_next :: Maybe t
1487 , dsl_lambda :: Maybe t
1488 , dsl_let :: Maybe t
1490 } deriving (Show, Functor, Generic)
1492deriving instance Binary DSL'
1495type DSL = DSL' PTerm
1497data SynContext = PatternSyntax
1500 deriving (Show, Generic)
1502deriving instance Binary SynContext
1505data Syntax = Rule [SSymbol] PTerm SynContext
1506 | DeclRule [SSymbol] [PDecl]
1507 deriving (Show, Generic)
1509syntaxNames :: Syntax -> [Name]
1510syntaxNames (Rule syms _ _) = mapMaybe ename syms
1511 where ename (Keyword n) = Just n
1513syntaxNames (DeclRule syms _) = mapMaybe ename syms
1514 where ename (Keyword n) = Just n
1517syntaxSymbols :: Syntax -> [SSymbol]
1518syntaxSymbols (Rule ss _ _) = ss
1519syntaxSymbols (DeclRule ss _) = ss
1521deriving instance Binary Syntax
1524data SSymbol = Keyword Name
1529 deriving (Show, Eq, Generic)
1533deriving instance Binary SSymbol
1536newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1539emptySyntaxRules :: SyntaxRules
1540emptySyntaxRules = SyntaxRules []
1542updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1543updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1545 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1550 ruleSort (s1:ss1) (s2:ss2) =
1551 case symCompare s1 s2 of
1552 EQ -> ruleSort ss1 ss2
1555 -- Better than creating Ord implementation for SSymbol since
1556 -- in general this ordering does not really make sense.
1557 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1558 symCompare (Keyword _) _ = LT
1559 symCompare (Symbol _) (Keyword _) = GT
1560 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1561 symCompare (Symbol _) _ = LT
1562 symCompare (Binding _) (Keyword _) = GT
1563 symCompare (Binding _) (Symbol _) = GT
1564 symCompare (Binding b1) (Binding b2) = compare b1 b2
1565 symCompare (Binding _) _ = LT
1566 symCompare (Expr _) (Keyword _) = GT
1567 symCompare (Expr _) (Symbol _) = GT
1568 symCompare (Expr _) (Binding _) = GT
1569 symCompare (Expr e1) (Expr e2) = compare e1 e2
1570 symCompare (Expr _) _ = LT
1571 symCompare (SimpleExpr _) (Keyword _) = GT
1572 symCompare (SimpleExpr _) (Symbol _) = GT
1573 symCompare (SimpleExpr _) (Binding _) = GT
1574 symCompare (SimpleExpr _) (Expr _) = GT
1575 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1577initDSL = DSL (PRef f [] (sUN ">>="))
1578 (PRef f [] (sUN "<*>"))
1579 (PRef f [] (sUN "pure"))
1586 where f = fileFC "(builtin)"
1588data Using = UImplicit Name PTerm
1589 | UConstraint Name [Name]
1590 deriving (Show, Eq, Data, Generic, Typeable)
1592deriving instance Binary Using
1595data SyntaxInfo = Syn {
1597 , syn_params :: [(Name, PTerm)]
1598 , syn_namespace :: [String]
1600 , imp_methods :: [Name]
1601 -- ^ interface methods. When expanding implicits, these should be
1602 -- expanded even under binders
1603 , decoration :: Name -> Name
1605 , implicitAllowed :: Bool
1606 , constraintAllowed :: Bool
1607 , maxline :: Maybe Int
1608 , mut_nesting :: Int
1610 , syn_in_quasiquote :: Int
1611 , syn_toplevel :: Bool
1612 , withAppAllowed :: Bool
1613 } deriving (Show, Generic)
1615deriving instance Binary SyntaxInfo
1618defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1620expandNS :: SyntaxInfo -> Name -> Name
1621expandNS syn n@(NS _ _) = n
1622expandNS syn n = case syn_namespace syn of
1627-- For inferring types of things
1629bi = fileFC "builtin"
1630primfc = fileFC "(primitive)"
1632inferTy = sMN 0 "__Infer"
1633inferCon = sMN 0 "__infer"
1634inferDecl = PDatadecl inferTy primfc
1636 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1637 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1638 (PRef bi [] inferTy)), bi, [])]
1641infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1642infP = P (TCon 6 0) inferTy (TType (UVal 0))
1644getInferTerm, getInferType :: Term -> Term
1645getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1646getInferTerm (App _ (App _ _ _) tm) = tm
1647getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1649getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1650 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1651 toTy (PVar _ t) = PVTy t
1653getInferType (App _ (App _ _ ty) _) = ty
1657-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1659primNames = [inferTy, inferCon]
1662unitCon = sUN "MkUnit"
1664falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1665 "The empty type, also known as the trivially false proposition." ++
1667 "Use `void` or `absurd` to prove anything if you have a variable " ++
1668 "of type `Void` in scope."
1671pairTy = sNS (sUN "Pair") ["Builtins"]
1672pairCon = sNS (sUN "MkPair") ["Builtins"]
1674upairTy = sNS (sUN "UPair") ["Builtins"]
1675upairCon = sNS (sUN "MkUPair") ["Builtins"]
1679eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1680 "The propositional equality type. A proof that `x` = `y`." ++
1682 "To use such a proof, pattern-match on it, and the two equal things will " ++
1683 "then need to be the _same_ pattern." ++
1685 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1686 "is possible to state equalities between values of potentially different " ++
1687 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1689 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1691eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1692 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1694 [(reflDoc, reflParamDoc,
1695 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1696 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1697 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1698 pimp (n "B") Placeholder False,
1699 pexp (PRef bi [] (n "x")),
1700 pexp (PRef bi [] (n "x"))])), bi, [])]
1702 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1703 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1704 "shown that both sides are in fact equal."
1705 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1706 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1708eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1709 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1715-- | The special name to be used in the module documentation context -
1716-- not for use in the main definition context. The namespace around it
1717-- will determine the module to which the docs adhere.
1719modDocName = sMN 0 "ModuleDocs"
1721-- Defined in builtins.idr
1722sigmaTy = sNS (sUN "DPair") ["Builtins"]
1723sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1725piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1726piBind = piBindp expl
1728piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1730piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1733-- Pretty-printing declarations and terms
1735-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1736-- could interfere with interactive editing, which calls "show".
1738instance Show PTerm where
1739 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1741instance Show PDecl where
1742 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1744instance Show PClause where
1745 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1747instance Show PData where
1748 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1750instance Pretty PTerm OutputAnnotation where
1751 pretty = prettyImp defaultPPOption
1753-- | Colourise annotations according to an Idris state. It ignores the
1754-- names in the annotation, as there's no good way to show extended
1755-- information on a terminal.
1756annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1757annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1758annotationColour ist (AnnConst c) =
1759 let theme = idris_colourTheme ist
1760 in Just $ if constIsType c
1761 then typeColour theme
1762 else dataColour theme
1763annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1764annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1765annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1766annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1767annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1768annotationColour ist (AnnName n _ _ _) =
1769 let ctxt = tt_ctxt ist
1770 theme = idris_colourTheme ist
1772 _ | isDConName n ctxt -> Just $ dataColour theme
1773 _ | isFnName n ctxt -> Just $ functionColour theme
1774 _ | isTConName n ctxt -> Just $ typeColour theme
1775 _ | isPostulateName n ist -> Just $ postulateColour theme
1776 _ | otherwise -> Nothing -- don't colourise unknown names
1777annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1778 where colour BoldText = IdrisColour Nothing True False True False
1779 colour UnderlineText = IdrisColour Nothing True True False False
1780 colour ItalicText = IdrisColour Nothing True False False True
1781annotationColour ist _ = Nothing
1784-- | Colourise annotations according to an Idris state. It ignores the
1785-- names in the annotation, as there's no good way to show extended
1786-- information on a terminal. Note that strings produced this way will
1787-- not be coloured on Windows, so the use of the colour rendering
1788-- functions in Idris.Output is to be preferred.
1789consoleDecorate :: IState -> OutputAnnotation -> String -> String
1790consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1792isPostulateName :: Name -> IState -> Bool
1793isPostulateName n ist = S.member n (idris_postulates ist)
1795-- | Pretty-print a high-level closed Idris term with no information
1796-- about precedence/associativity
1797prettyImp :: PPOption -- ^ pretty printing options
1798 -> PTerm -- ^ the term to pretty-print
1799 -> Doc OutputAnnotation
1800prettyImp impl = pprintPTerm impl [] [] []
1802-- | Serialise something to base64 using its Binary implementation.
1804-- | Do the right thing for rendering a term in an IState
1805prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1806prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1808-- | Pretty-print a high-level Idris term in some bindings context
1810pprintPTerm :: PPOption -- ^ pretty printing options
1811 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1812 -> [Name] -- ^ names to always show in pi, even if not used
1813 -> [FixDecl] -- ^ Fixity declarations
1814 -> PTerm -- ^ the term to pretty-print
1815 -> Doc OutputAnnotation
1816pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1821 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1822 prettySe d p bnd (PQuote r) =
1823 text "![" <> pretty r <> text "]"
1824 prettySe d p bnd (PPatvar fc n) = pretty n
1826 | Just str <- slist d p bnd e = depth d str
1827 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1828 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1829 prettySe d p bnd (PLam fc n nfc ty sc) =
1830 let (ns, sc') = getLamNames [n] sc in
1831 depth d . bracket p startPrec . group . align . hang 2 $
1832 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1833 prettySe (decD d) startPrec ((n, False):bnd) sc'
1835 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1836 getLamNames acc sc = (reverse acc, sc)
1838 prettyBindingsOf [] t = text ""
1839 prettyBindingsOf [n] t = prettyBindingOf n t
1840 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1841 prettyBindingsOf ns t
1842 prettySe d p bnd (PLet fc n nfc ty v sc) =
1843 depth d . bracket p startPrec . group . align $
1844 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1845 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1846 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1848 depth d . bracket p startPrec . group $
1849 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1850 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1852 depth d . bracket p startPrec . group $
1853 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1854 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1855 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1856 || ppopt_pinames ppo && uname n =
1857 depth d . bracket p startPrec . group $
1858 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1859 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1861 depth d . bracket p startPrec . group $
1862 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1863 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1865 uname (UN n) = case str n of
1872 Static -> text "%static" <> space
1874 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1876 depth d . bracket p startPrec $
1877 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1878 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1879 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1881 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1882 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1883 showRig _ n = prettyBindingOf n True
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