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 , syntax_rules :: SyntaxRules
261 , syntax_keywords :: [String]
262 , imported :: [FilePath] -- ^ The imported modules
263 , idris_scprims :: [(Name, (Int, PrimFn))]
264 , idris_objs :: [(Codegen, FilePath)]
265 , idris_libs :: [(Codegen, String)]
266 , idris_cgflags :: [(Codegen, String)]
267 , idris_hdrs :: [(Codegen, String)]
268 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
269 , proof_list :: [(Name, (Bool, [String]))]
270 , errSpan :: Maybe FC
271 , parserWarnings :: [(FC, Err)]
272 , lastParse :: Maybe Name
273 , indent_stack :: [Int]
274 , brace_stack :: [Maybe Int]
275 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
276 , idris_parsedSpan :: Maybe FC
277 , hide_list :: Ctxt Accessibility
278 , default_access :: Accessibility
279 , default_total :: DefaultTotality
280 , ibc_write :: [IBCWrite]
281 , compiled_so :: Maybe String
282 , idris_dynamic_libs :: [DynamicLib]
283 , idris_language_extensions :: [LanguageExt]
284 , idris_outputmode :: OutputMode
285 , idris_colourRepl :: Bool
286 , idris_colourTheme :: ColourTheme
287 , idris_errorhandlers :: [Name] -- ^ Global error handlers
288 , idris_nameIdx :: (Int, Ctxt (Int, Name))
289 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
290 , module_aliases :: M.Map [T.Text] [T.Text]
291 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
292 , idris_postulates :: S.Set Name
293 , idris_externs :: S.Set (Name, Int)
294 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
296 -- | List of names that were defined in the repl, and can be re-/un-defined
297 , idris_repl_defs :: [Name]
299 -- | Stack of names currently being elaborated, Bool set if it's an
300 -- implementation (implementations appear twice; also as a function name)
301 , elab_stack :: [(Name, Bool)]
304 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
305 , idris_exports :: [Name] -- ^ Functions with ExportList
306 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
307 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
308 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
309 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
310 , idris_ttstats :: M.Map Term (Int, Term)
311 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
312 , idris_interactiveOpts :: InteractiveOpts
315-- Required for parsers library, and therefore trifecta
316instance Show IState where
317 show = const "{internal state}"
319data SizeChange = Smaller | Same | Bigger | Unknown
320 deriving (Show, Eq, Generic)
322deriving instance Binary SizeChange
325type SCGEntry = (Name, [Maybe (Int, SizeChange)])
326type UsageReason = (Name, Int) -- fn_name, its_arg_number
328data CGInfo = CGInfo {
329 calls :: [Name] -- Immediate calls
330 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
332 , usedpos :: [(Int, [UsageReason])]
333 } deriving (Show, Generic)
335deriving instance Binary CGInfo
339primDefs = [ sUN "unsafePerformPrimIO"
340 , sUN "mkLazyForeignPrim"
341 , sUN "mkForeignPrim"
343 , sUN "assert_unreachable"
347-- information that needs writing for the current module's .ibc file
348data IBCWrite = IBCFix FixDecl
353 | IBCImplementation Bool Bool Name Name
360 | IBCImport (Bool, FilePath) -- ^ True = import public
361 | IBCImportDir FilePath
362 | IBCSourceDir FilePath
363 | IBCObj Codegen FilePath
364 | IBCLib Codegen String
365 | IBCCGFlag Codegen String
367 | IBCHeader Codegen String
368 | IBCAccess Name Accessibility
369 | IBCMetaInformation Name MetaInformation
370 | IBCTotal Name Totality
371 | IBCInjective Name Injectivity
373 | IBCFnInfo Name FnInfo
374 | IBCTrans Name (Term, Term)
375 | IBCErrRev (Term, Term)
379 | IBCDef Name -- ^ The main context.
380 | IBCNameHint (Name, Name)
381 | IBCLineApp FilePath Int PTerm
382 | IBCErrorHandler Name
383 | IBCFunctionErrorHandler Name Name Name
385 | IBCExtern (Name, Int)
386 | IBCTotCheckErr FC String
388 | IBCModDocs Name -- ^ The name is the special name used to track module docs
389 | IBCUsage (Name, Int)
391 | IBCAutoHint Name Name
392 | IBCDeprecate Name String
393 | IBCFragile Name String
394 | IBCConstraint FC UConstraint
395 deriving (Show, Generic)
397initialInteractiveOpts :: InteractiveOpts
398initialInteractiveOpts = InteractiveOpts {
399 interactiveOpts_indentWith = 2
400 , interactiveOpts_indentClause = 2
403-- | The initial state for the compiler
405idrisInit = IState initContext S.empty []
406 emptyContext emptyContext emptyContext [] emptyContext
407 emptyContext emptyContext emptyContext emptyContext
408 emptyContext emptyContext emptyContext emptyContext
409 emptyContext emptyContext emptyContext emptyContext
411 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
412 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
413 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
414 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
415 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
418-- | The monad for the main REPL - reading and processing files and
419-- updating global state (hence the IO inner monad).
422-- type Idris = WriterT [Either String (IO ())] (State IState a))
425type Idris = StateT IState (ExceptT Err IO)
427catchError :: Idris a -> (Err -> Idris a) -> Idris a
428catchError = liftCatch catchE
430throwError :: Err -> Idris a
431throwError = Trans.lift . throwE
433-- Commands in the REPL
435data Codegen = Via IRFormat String
437 deriving (Show, Eq, Generic)
439data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
441data HowMuchDocs = FullDocs | OverviewDocs
443data OutputFmt = HTMLOutput | LaTeXOutput
445-- | Recognised logging categories for the Idris compiler.
447-- @TODO add in sub categories.
454 deriving (Show, Eq, Ord, Generic)
456strLogCat :: LogCat -> String
457strLogCat IParse = "parser"
458strLogCat IElab = "elab"
459strLogCat ICodeGen = "codegen"
460strLogCat IErasure = "erasure"
461strLogCat ICoverage = "coverage"
462strLogCat IIBC = "ibc"
464codegenCats :: [LogCat]
465codegenCats = [ICodeGen]
467parserCats :: [LogCat]
473loggingCatsStr :: String
474loggingCatsStr = unlines
477 , (strLogCat ICodeGen)
478 , (strLogCat IErasure)
479 , (strLogCat ICoverage)
484data ElabShellCmd = EQED
492 | EDocStr (Either Name Const)
495data Opt = Filename String
512 | NoBuiltins -- only for the really primitive stuff!
529 | Port REPLPort -- ^ REPL TCP port
538 | PkgDocBuild String -- IdrisDoc
539 | PkgDocInstall String
549 | OutputTy OutputType
550 | Extension LanguageExt
551 | InterpretScript String
553 | TargetTriple String
556 | AddOpt Optimisation
557 | RemoveOpt Optimisation
560 | AutoWidth -- ^ Automatically adjust terminal width
561 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
562 | UseConsoleWidth ConsoleWidth
565 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
566 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
567 deriving (Show, Eq, Generic)
569data REPLPort = DontListen | ListenPort PortNumber
570 deriving (Eq, Generic, Show)
572-- Parsed declarations
574data Fixity = Infixl { prec :: Int }
575 | Infixr { prec :: Int }
576 | InfixN { prec :: Int }
577 | PrefixN { prec :: Int }
578 deriving (Eq, Generic)
580deriving instance Binary Fixity
583instance Show Fixity where
584 show (Infixl i) = "infixl " ++ show i
585 show (Infixr i) = "infixr " ++ show i
586 show (InfixN i) = "infix " ++ show i
587 show (PrefixN i) = "prefix " ++ show i
589data FixDecl = Fix Fixity String
590 deriving (Eq, Generic)
592instance Show FixDecl where
593 show (Fix f s) = show f ++ " " ++ s
596deriving instance Binary FixDecl
599instance Ord FixDecl where
600 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
603data Static = Static | Dynamic
604 deriving (Show, Eq, Ord, Data, Generic, Typeable)
606deriving instance Binary Static
609-- ^ Mark bindings with their explicitness, and laziness
610data Plicity = Imp { pargopts :: [ArgOpt]
613 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
614 , pinsource :: Bool -- ^ Explicitly written in source
617 | Exp { pargopts :: [ArgOpt]
619 , pparam :: Bool -- ^ this is a param (rather than index)
622 | Constraint { pargopts :: [ArgOpt]
626 | TacImp { pargopts :: [ArgOpt]
631 deriving (Show, Eq, Ord, Data, Generic, Typeable)
634deriving instance Binary Plicity
637is_scoped :: Plicity -> Maybe ImplicitInfo
638is_scoped (Imp _ _ _ s _ _) = s
643impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
644-- Machine generated top level implicit
646impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
650forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
651forall_constraint :: Plicity
652forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
655expl = Exp [] Dynamic False RigW
657expl_param = Exp [] Dynamic True RigW
660constraint = Constraint [] Static RigW
662tacimpl :: PTerm -> Plicity
663tacimpl t = TacImp [] Dynamic t RigW
665data FnOpt = Inlinable -- ^ always evaluate when simplifying
666 | TotalFn | PartialFn | CoveringFn
667 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
670 -- | interface dictionary, eval only when a function
671 -- argument, and further evaluation results.
673 | OverlappingDictionary -- ^ Interface dictionary which may overlap
674 | Implicit -- ^ implicit coercion
675 | NoImplicit -- ^ do not apply implicit coercions
676 | CExport String -- ^ export, with a C name
677 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
678 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
679 | Reflection -- ^ a reflecting function, compile-time only
680 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
681 | UnfoldIface Name [Name]
682 -- ^ Unfold given interface name in the definition, the
683 -- top level methods, and anything which has
684 -- the interface name as an argument. This is to unfold
685 -- things for termination checking, as interfaces will otherwise
687 | Constructor -- ^ Data constructor type
688 | AutoHint -- ^ use in auto implicit search
689 | PEGenerated -- ^ generated by partial evaluator
690 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
691 deriving (Show, Eq, Generic)
693deriving instance Binary FnOpt
698inlinable :: FnOpts -> Bool
699inlinable = elem Inlinable
701dictionary :: FnOpts -> Bool
702dictionary = elem Dictionary
705-- | Type provider - what to provide
706data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
707 | ProvPostulate t -- ^ goal type must be Type, so only term
708 deriving (Show, Eq, Functor, Generic)
710type ProvideWhat = ProvideWhat' PTerm
712-- | Top-level declarations such as compiler directives, definitions,
713-- datatypes and interfaces.
715 -- | Fixity declaration
716 = PFix FC Fixity [String]
717 -- | Type declaration (last FC is precise name location)
718 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
719 -- | Postulate, second FC is precise name location
720 | PPostulate Bool -- external def if true
721 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
723 | PClauses FC FnOpts Name [PClause' t]
724 -- | Top level constant
726 -- | Data declaration.
727 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
729 | PParams FC [(Name, t)] [PDecl' t]
730 -- | Open block/declaration
731 | POpenInterfaces FC [Name] [PDecl' t]
732 -- | New namespace, where FC is accurate location of the namespace
734 | PNamespace String FC [PDecl' t]
736 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
738 FC -- Record name precise location
739 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
740 [(Name, Docstring (Either Err t))] -- Param Docs
741 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
742 (Maybe (Name, FC)) -- Optional constructor name and location
743 (Docstring (Either Err t)) -- Constructor doc
744 SyntaxInfo -- Constructor SyntaxInfo
746 -- | Interface: arguments are documentation, syntax info, source
747 -- location, constraints, interface name, interface name location,
748 -- parameters, method declarations, optional constructor name
749 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
750 [(Name, t)] -- constraints
751 Name -- interface name
752 FC -- accurate location of interface name
753 [(Name, FC, t)] -- parameters and precise locations
754 [(Name, Docstring (Either Err t))] -- parameter docstrings
755 [(Name, FC)] -- determining parameters and precise locations
756 [PDecl' t] -- declarations
757 (Maybe (Name, FC)) -- implementation constructor name and location
758 (Docstring (Either Err t)) -- implementation constructor docs
760 -- | Implementation declaration: arguments are documentation, syntax
761 -- info, source location, constraints, interface name, parameters, full
762 -- Implementation type, optional explicit name, and definitions
763 | PImplementation (Docstring (Either Err t)) -- Implementation docs
764 [(Name, Docstring (Either Err t))] -- Parameter docs
766 FC [(Name, t)] -- constraints
767 [Name] -- parent dictionaries to search for constraints
771 FC -- precise location of interface
773 [(Name, t)] -- Extra names in scope in the body
774 t -- full Implementation type
775 (Maybe Name) -- explicit name
777 | PDSL Name (DSL' t) -- ^ DSL declaration
778 | PSyntax FC Syntax -- ^ Syntax definition
779 | PMutual FC [PDecl' t] -- ^ Mutual block
780 | PDirective Directive -- ^ Compiler directive.
782 -- | Type provider. The first t is the type, the second is the
783 -- term. The second FC is precise highlighting location.
784 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
786 -- | Source-to-source transformation rule. If bool is True, lhs and
787 -- rhs must be convertible.
788 | PTransform FC Bool t t
790 -- | FC is decl-level, for errors, and Strings represent the
792 | PRunElabDecl FC t [String]
793 deriving (Functor, Generic)
795deriving instance Binary PDecl'
798-- | The set of source directives
799data Directive = DLib Codegen String
800 | DLink Codegen String
801 | DFlag Codegen String
802 | DInclude Codegen String
807 | DSetTotal Name -- assert totality after checking
808 | DAccess Accessibility
809 | DDefault DefaultTotality
811 | DDynamicLibs [String]
812 | DNameHint Name FC [(Name, FC)]
813 | DErrorHandlers Name FC Name FC [(Name, FC)]
814 | DLanguage LanguageExt
815 | DDeprecate Name String
816 | DFragile Name String
817 | DAutoImplicits Bool
821-- | A set of instructions for things that need to happen in IState
822-- after a term elaboration when there's been reflected elaboration.
823data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
824 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
825 | RAddImplementation Name Name
826 | RDatatypeDeclInstrs Name [PArg]
827 -- | Datatype, constructors
828 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
831-- | For elaborator state
832data EState = EState {
833 case_decls :: [(Name, PDecl)]
834 , delayed_elab :: [(Int, Elab' EState ())]
835 , new_tyDecls :: [RDeclInstructions]
836 , highlighting :: [(FC, OutputAnnotation)]
837 , auto_binds :: [Name] -- ^ names bound as auto implicits
838 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
842initEState = EState [] [] [] [] [] []
844type ElabD a = Elab' EState a
846highlightSource :: FC -> OutputAnnotation -> ElabD ()
847highlightSource fc annot =
848 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
850-- | One clause of a top-level definition. Term arguments to constructors are:
852-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
854-- 2. The list of extra 'with' patterns
856-- 3. The right-hand side
858-- 4. The where block (PDecl' t)
860data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
861 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
862 | PClauseR FC [t] t [PDecl' t]
863 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
864 deriving (Functor, Generic)
866deriving instance Binary PClause'
871 -- | Data declaration
872 PDatadecl { d_name :: Name -- ^ The name of the datatype
873 , d_name_fc :: FC -- ^ The precise location of the type constructor name
874 , d_tcon :: t -- ^ Type constructor
875 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
877 -- | "Placeholder" for data whose constructors are defined later
878 | PLaterdecl { d_name :: Name
881 } deriving (Functor, Generic)
883-- | Transform the FCs in a PData and its associated terms. The first
884-- function transforms the general-purpose FCs, and the second
885-- transforms those that are used for semantic source highlighting, so
886-- they can be treated specially.
887mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
888mapPDataFC f g (PDatadecl n nfc tycon ctors) =
889 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
890 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
891 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
892mapPDataFC f g (PLaterdecl n nfc tycon) =
893 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
895deriving instance Binary PData'
898-- Handy to get a free function for applying PTerm -> PTerm functions
899-- across a program, by deriving Functor
901type PDecl = PDecl' PTerm
902type PData = PData' PTerm
903type PClause = PClause' PTerm
905-- | Transform the FCs in a PTerm. The first function transforms the
906-- general-purpose FCs, and the second transforms those that are used
907-- for semantic source highlighting, so they can be treated specially.
908mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
909mapPDeclFC f g (PFix fc fixity ops) =
910 PFix (f fc) fixity ops
911mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
912 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
913mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
914 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
916mapPDeclFC f g (PClauses fc opts n clauses) =
917 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
918mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
919mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
920 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
921mapPDeclFC f g (PParams fc params decls) =
923 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
924 (map (mapPDeclFC f g) decls)
925mapPDeclFC f g (POpenInterfaces fc ifs decls) =
926 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
927mapPDeclFC f g (PNamespace ns fc decls) =
928 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
929mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
930 PRecord doc syn (f fc) opts n (g nfc)
931 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
933 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
934 plic, mapPTermFC f g ty, fdoc))
936 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
939mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
940 PInterface doc syn (f fc)
941 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
942 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
943 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
944 (map (mapPDeclFC f g) body)
945 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
947mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
948 PImplementation doc paramDocs syn (f fc)
949 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
950 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
951 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
952 (mapPTermFC f g implTy)
954 (map (mapPDeclFC f g) body)
955mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
956mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
958 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
959 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
960mapPDeclFC f g (PMutual fc decls) =
961 PMutual (f fc) (map (mapPDeclFC f g) decls)
962mapPDeclFC f g (PDirective d) =
965 DNameHint n nfc ns ->
966 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
967 DErrorHandlers n nfc n' nfc' ns ->
968 DErrorHandlers n (g nfc) n' (g nfc') $
969 map (\(an, anfc) -> (an, g anfc)) ns
970mapPDeclFC f g (PProvider doc syn fc nfc what n) =
971 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
972mapPDeclFC f g (PTransform fc safe l r) =
973 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
974mapPDeclFC f g (PRunElabDecl fc script ns) =
975 PRunElabDecl (f fc) (mapPTermFC f g script) ns
977-- | Get all the names declared in a declaration
978declared :: PDecl -> [Name]
979declared (PFix _ _ _) = []
980declared (PTy _ _ _ _ _ n fc t) = [n]
981declared (PPostulate _ _ _ _ _ _ n t) = [n]
982declared (PClauses _ _ n _) = [] -- not a declaration
983declared (PCAF _ n _) = [n]
984declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
985 where fstt (_, _, a, _, _, _, _) = a
986declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
987declared (PParams _ _ ds) = concatMap declared ds
988declared (POpenInterfaces _ _ ds) = concatMap declared ds
989declared (PNamespace _ _ ds) = concatMap declared ds
990declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
991declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
992declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
996declared (PDSL n _) = [n]
997declared (PSyntax _ _) = []
998declared (PMutual _ ds) = concatMap declared ds
999declared (PDirective _) = []
1002-- get the names declared, not counting nested parameter blocks
1003tldeclared :: PDecl -> [Name]
1004tldeclared (PFix _ _ _) = []
1005tldeclared (PTy _ _ _ _ _ n _ t) = [n]
1006tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
1007tldeclared (PClauses _ _ n _) = [] -- not a declaration
1008tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1009tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1010 where fstt (_, _, a, _, _, _, _) = a
1011tldeclared (PParams _ _ ds) = []
1012tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
1013tldeclared (PMutual _ ds) = concatMap tldeclared ds
1014tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
1015tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
1016tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1022defined :: PDecl -> [Name]
1023defined (PFix _ _ _) = []
1024defined (PTy _ _ _ _ _ n _ t) = []
1025defined (PPostulate _ _ _ _ _ _ n t) = []
1026defined (PClauses _ _ n _) = [n] -- not a declaration
1027defined (PCAF _ n _) = [n]
1028defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1029 where fstt (_, _, a, _, _, _, _) = a
1030defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1031defined (PParams _ _ ds) = concatMap defined ds
1032defined (POpenInterfaces _ _ ds) = concatMap defined ds
1033defined (PNamespace _ _ ds) = concatMap defined ds
1034defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1035defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1036defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1040defined (PDSL n _) = [n]
1041defined (PSyntax _ _) = []
1042defined (PMutual _ ds) = concatMap defined ds
1043defined (PDirective _) = []
1046updateN :: [(Name, Name)] -> Name -> Name
1047updateN ns n | Just n' <- lookup n ns = n'
1050updateNs :: [(Name, Name)] -> PTerm -> PTerm
1052updateNs ns t = mapPT updateRef t
1053 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1056-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1057-- updateDNs [] t = t
1058-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1059-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1060-- where updateCNs ns (PClause n l ts r ds)
1061-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1062-- (map (fmap (updateNs ns)) ts)
1063-- (fmap (updateNs ns) r)
1064-- (map (updateDNs ns) ds)
1065-- updateDNs ns c = c
1067data PunInfo = IsType
1070 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1072-- | High level language terms
1073data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1074 -- high-level language
1076 -- ^ A reference to a variable. The FC is its precise
1077 -- source location for highlighting. The list of FCs is a
1078 -- collection of additional highlighting locations.
1079 | PInferRef FC [FC] Name -- ^ A name to be defined later
1080 | PPatvar FC Name -- ^ A pattern variable
1081 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1082 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1083 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1084 | PTyped PTerm PTerm -- ^ Term with explicit type
1085 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1086 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1087 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1088 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1089 | PMatchApp FC Name -- ^ Make an application by type matching
1090 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1091 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1092 | PTrue FC PunInfo -- ^ Unit type..?
1093 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1094 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1095 -- ^ "rewrite" syntax, with optional rewriting function and
1096 -- optional result type
1097 | PPair FC [FC] PunInfo PTerm PTerm
1098 -- ^ A pair (a, b) and whether it's a product type or a
1099 -- pair (solved by elaboration). The list of FCs is its
1101 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1102 -- ^ A dependent pair (tm : a ** b) and whether it's a
1103 -- sigma type or a pair that inhabits one (solved by
1104 -- elaboration). The [FC] is its punctuation.
1105 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1106 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1107 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1108 | PType FC -- ^ 'Type' type
1109 | PUniverse FC Universe -- ^ Some universe
1110 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1111 | PConstant FC Const -- ^ Builtin types
1112 | Placeholder -- ^ Underscore
1113 | PDoBlock [PDo] -- ^ Do notation
1114 | PIdiom FC PTerm -- ^ Idiom brackets
1115 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1116 | PProof [PTactic] -- ^ Proof script
1117 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1118 | PElabError Err -- ^ Error to report on elaboration
1119 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1120 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1121 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1122 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1123 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1124 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1125 | PUnquote PTerm -- ^ ~Term
1126 | PQuoteName Name Bool FC
1127 -- ^ `{n} where the FC is the precise highlighting for
1128 -- the name in particular. If the Bool is False, then
1129 -- it's `{{n}} and the name won't be resolved.
1130 | PRunElab FC PTerm [String]
1131 -- ^ %runElab tm - New-style proof script. Args are
1132 -- location, script, enclosing namespace.
1133 | PConstSugar FC PTerm
1134 -- ^ A desugared constant. The FC is a precise source
1135 -- location that will be used to highlight it later.
1136 deriving (Eq, Ord, Data, Typeable, Generic)
1138data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1141 deriving (Eq, Ord, Data, Generic, Typeable)
1143-- | Transform the FCs in a PTerm. The first function transforms the
1144-- general-purpose FCs, and the second transforms those that are used
1145-- for semantic source highlighting, so they can be treated specially.
1146mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1147mapPTermFC f g (PQuote q) = PQuote q
1148mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1149mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1150mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1151mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1152mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1153mapPTermFC 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)
1154mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1155mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1156mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1157mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1158mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1159mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1160mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1161mapPTermFC 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)
1162mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1163mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1164mapPTermFC 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)
1165mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1166mapPTermFC 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)
1167mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1168mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1169mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1170mapPTermFC f g (PType fc) = PType (f fc)
1171mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1172mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1173mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1174mapPTermFC f g Placeholder = Placeholder
1175mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1176 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1177 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1178 mapPDoFC (DoBindP fc t1 t2 alts) =
1179 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1180 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1181 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1182mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1183mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1184mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1185mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1186mapPTermFC f g (PElabError err) = PElabError err
1187mapPTermFC f g PImpossible = PImpossible
1188mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1189mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1190mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1191mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1192mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1193mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1194mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1195mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1196mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1199dg instance Binary PTerm
1202mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1203mapPT f t = f (mpt t) where
1204 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1205 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1206 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1207 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1208 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1209 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1210 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1211 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1212 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1213 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1214 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1215 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1216 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1217 mpt (PHidden t) = PHidden (mapPT f t)
1218 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1219 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1220 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1221 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1222 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1223 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1224 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1228data PTactic' t = Intro [Name] | Intros | Focus Name
1229 | Refine Name [Bool] | Rewrite t | DoUnify
1236 | LetTac Name t | LetTacTy Name t t
1237 | Exact t | Compute | Trivial | TCImplementation
1238 | ProofSearch Bool Bool Int (Maybe Name)
1239 [Name] -- allowed local names
1241 -- ^ the bool is whether to search recursively
1244 | ProofState | ProofTerm | Undo
1245 | Try (PTactic' t) (PTactic' t)
1246 | TSeq (PTactic' t) (PTactic' t)
1247 | ApplyTactic t -- see Language.Reflection module
1251 | GoalType String (PTactic' t)
1254 | TDocStr (Either Name Const)
1257 | TFail [ErrorReportPart]
1260 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1262deriving instance Binary PTactic'
1264instance Sized a => Sized (PTactic' a) where
1265 size (Intro nms) = 1 + size nms
1267 size (Focus nm) = 1 + size nm
1268 size (Refine nm bs) = 1 + size nm + length bs
1269 size (Rewrite t) = 1 + size t
1270 size (Induction t) = 1 + size t
1271 size (LetTac nm t) = 1 + size nm + size t
1272 size (Exact t) = 1 + size t
1280 size (Try l r) = 1 + size l + size r
1281 size (TSeq l r) = 1 + size l + size r
1282 size (ApplyTactic t) = 1 + size t
1283 size (Reflect t) = 1 + size t
1284 size (Fill t) = 1 + size t
1288 size (TFail ts) = 1 + size ts
1291 size (CaseTac x) = 1 + size x
1292 size (Equiv t) = 1 + size t
1293 size (Claim x y) = 1 + size x + size y
1295 size (MatchRefine x) = 1 + size x
1296 size (LetTacTy x y z) = 1 + size x + size y + size z
1297 size TCImplementation = 1
1299type PTactic = PTactic' PTerm
1301data PDo' t = DoExp FC t
1302 | DoBind FC Name FC t -- ^ second FC is precise name location
1303 | DoBindP FC t t [(t,t)]
1304 | DoLet FC Name FC t t -- ^ second FC is precise name location
1306 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1308deriving instance Binary PDo'
1311instance Sized a => Sized (PDo' a) where
1312 size (DoExp fc t) = 1 + size fc + size t
1313 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1314 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1315 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1316 size (DoLetP fc l r) = 1 + size fc + size l + size r
1318type PDo = PDo' PTerm
1320-- The priority gives a hint as to elaboration order. Best to elaborate
1321-- things early which will help give a more concrete type to other
1322-- variables, e.g. a before (interpTy a).
1324data PArg' t = PImp { priority :: Int
1325 , machine_inf :: Bool -- ^ true if the machine inferred it
1326 , argopts :: [ArgOpt]
1330 | PExp { priority :: Int
1331 , argopts :: [ArgOpt]
1335 | PConstraint { priority :: Int
1336 , argopts :: [ArgOpt]
1340 | PTacImplicit { priority :: Int
1341 , argopts :: [ArgOpt]
1346 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1348data ArgOpt = AlwaysShow
1352 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1354instance Sized a => Sized (PArg' a) where
1355 size (PImp p _ l nm trm) = 1 + size nm + size trm
1356 size (PExp p l nm trm) = 1 + size nm + size trm
1357 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1358 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1361deriving instance Binary PArg'
1364pimp n t mach = PImp 1 mach [] n t
1365pexp t = PExp 1 [] (sMN 0 "arg") t
1366pconst t = PConstraint 1 [] (sMN 0 "carg") t
1367ptacimp n s t = PTacImplicit 2 [] n s t
1369type PArg = PArg' PTerm
1371-- | Get the highest FC in a term, if one exists
1372highestFC :: PTerm -> Maybe FC
1373highestFC (PQuote _) = Nothing
1374highestFC (PRef fc _ _) = Just fc
1375highestFC (PInferRef fc _ _) = Just fc
1376highestFC (PPatvar fc _) = Just fc
1377highestFC (PLam fc _ _ _ _) = Just fc
1378highestFC (PPi _ _ _ _ _) = Nothing
1379highestFC (PLet fc _ _ _ _ _) = Just fc
1380highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1381highestFC (PApp fc _ _) = Just fc
1382highestFC (PAppBind fc _ _) = Just fc
1383highestFC (PMatchApp fc _) = Just fc
1384highestFC (PCase fc _ _) = Just fc
1385highestFC (PIfThenElse fc _ _ _) = Just fc
1386highestFC (PTrue fc _) = Just fc
1387highestFC (PResolveTC fc) = Just fc
1388highestFC (PRewrite fc _ _ _ _) = Just fc
1389highestFC (PPair fc _ _ _ _) = Just fc
1390highestFC (PDPair fc _ _ _ _ _) = Just fc
1391highestFC (PAs fc _ _) = Just fc
1392highestFC (PAlternative _ _ args) =
1393 case mapMaybe highestFC args of
1396highestFC (PHidden _) = Nothing
1397highestFC (PType fc) = Just fc
1398highestFC (PUniverse _ _) = Nothing
1399highestFC (PGoal fc _ _ _) = Just fc
1400highestFC (PConstant fc _) = Just fc
1401highestFC Placeholder = Nothing
1402highestFC (PDoBlock lines) =
1403 case map getDoFC lines of
1407 getDoFC (DoExp fc t) = fc
1408 getDoFC (DoBind fc nm nfc t) = fc
1409 getDoFC (DoBindP fc l r alts) = fc
1410 getDoFC (DoLet fc nm nfc l r) = fc
1411 getDoFC (DoLetP fc l r) = fc
1413highestFC (PIdiom fc _) = Just fc
1414highestFC (PMetavar fc _) = Just fc
1415highestFC (PProof _) = Nothing
1416highestFC (PTactics _) = Nothing
1417highestFC (PElabError _) = Nothing
1418highestFC PImpossible = Nothing
1419highestFC (PCoerced tm) = highestFC tm
1420highestFC (PDisamb _ opts) = highestFC opts
1421highestFC (PUnifyLog tm) = highestFC tm
1422highestFC (PNoImplicits tm) = highestFC tm
1423highestFC (PQuasiquote _ _) = Nothing
1424highestFC (PUnquote tm) = highestFC tm
1425highestFC (PQuoteName _ _ fc) = Just fc
1426highestFC (PRunElab fc _ _) = Just fc
1427highestFC (PConstSugar fc _) = Just fc
1428highestFC (PAppImpl t _) = highestFC t
1432data InterfaceInfo = CI {
1433 implementationCtorName :: Name
1434 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1435 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1436 , interface_default_super_interfaces :: [PDecl]
1437 , interface_impparams :: [Name]
1438 , interface_params :: [Name]
1439 , interface_constraints :: [PTerm]
1440 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1441 , interface_determiners :: [Int]
1442 } deriving (Show, Generic)
1444deriving instance Binary InterfaceInfo
1448data RecordInfo = RI {
1449 record_parameters :: [(Name,PTerm)]
1450 , record_constructor :: Name
1451 , record_projections :: [Name]
1452 } deriving (Show, Generic)
1454-- Type inference data
1456data TIData = TIPartial -- ^ a function with a partially defined type
1457 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1458 deriving (Show, Generic)
1460-- | Miscellaneous information about functions
1461data FnInfo = FnInfo { fn_params :: [Int] }
1462 deriving (Show, Generic)
1464deriving instance Binary FnInfo
1467data OptInfo = Optimise {
1468 inaccessible :: [(Int,Name)] -- includes names for error reporting
1469 , detaggable :: Bool
1470 , forceable :: [Int] -- argument positions which are forced by other values
1471 } deriving (Show, Generic)
1473deriving instance Binary OptInfo
1476-- | Syntactic sugar info
1481 , dsl_var :: Maybe t
1482 , index_first :: Maybe t
1483 , index_next :: Maybe t
1484 , dsl_lambda :: Maybe t
1485 , dsl_let :: Maybe t
1487 } deriving (Show, Functor, Generic)
1489deriving instance Binary DSL'
1492type DSL = DSL' PTerm
1494data SynContext = PatternSyntax
1497 deriving (Show, Generic)
1499deriving instance Binary SynContext
1502data Syntax = Rule [SSymbol] PTerm SynContext
1503 | DeclRule [SSymbol] [PDecl]
1504 deriving (Show, Generic)
1506syntaxNames :: Syntax -> [Name]
1507syntaxNames (Rule syms _ _) = mapMaybe ename syms
1508 where ename (Keyword n) = Just n
1510syntaxNames (DeclRule syms _) = mapMaybe ename syms
1511 where ename (Keyword n) = Just n
1514syntaxSymbols :: Syntax -> [SSymbol]
1515syntaxSymbols (Rule ss _ _) = ss
1516syntaxSymbols (DeclRule ss _) = ss
1518deriving instance Binary Syntax
1521data SSymbol = Keyword Name
1526 deriving (Show, Eq, Generic)
1530deriving instance Binary SSymbol
1533newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1536emptySyntaxRules :: SyntaxRules
1537emptySyntaxRules = SyntaxRules []
1539updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1540updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1542 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1547 ruleSort (s1:ss1) (s2:ss2) =
1548 case symCompare s1 s2 of
1549 EQ -> ruleSort ss1 ss2
1552 -- Better than creating Ord implementation for SSymbol since
1553 -- in general this ordering does not really make sense.
1554 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1555 symCompare (Keyword _) _ = LT
1556 symCompare (Symbol _) (Keyword _) = GT
1557 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1558 symCompare (Symbol _) _ = LT
1559 symCompare (Binding _) (Keyword _) = GT
1560 symCompare (Binding _) (Symbol _) = GT
1561 symCompare (Binding b1) (Binding b2) = compare b1 b2
1562 symCompare (Binding _) _ = LT
1563 symCompare (Expr _) (Keyword _) = GT
1564 symCompare (Expr _) (Symbol _) = GT
1565 symCompare (Expr _) (Binding _) = GT
1566 symCompare (Expr e1) (Expr e2) = compare e1 e2
1567 symCompare (Expr _) _ = LT
1568 symCompare (SimpleExpr _) (Keyword _) = GT
1569 symCompare (SimpleExpr _) (Symbol _) = GT
1570 symCompare (SimpleExpr _) (Binding _) = GT
1571 symCompare (SimpleExpr _) (Expr _) = GT
1572 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1574initDSL = DSL (PRef f [] (sUN ">>="))
1575 (PRef f [] (sUN "<*>"))
1576 (PRef f [] (sUN "pure"))
1583 where f = fileFC "(builtin)"
1585data Using = UImplicit Name PTerm
1586 | UConstraint Name [Name]
1587 deriving (Show, Eq, Data, Generic, Typeable)
1589deriving instance Binary Using
1592data SyntaxInfo = Syn {
1594 , syn_params :: [(Name, PTerm)]
1595 , syn_namespace :: [String]
1597 , imp_methods :: [Name]
1598 -- ^ interface methods. When expanding implicits, these should be
1599 -- expanded even under binders
1600 , decoration :: Name -> Name
1602 , implicitAllowed :: Bool
1603 , constraintAllowed :: Bool
1604 , maxline :: Maybe Int
1605 , mut_nesting :: Int
1607 , syn_in_quasiquote :: Int
1608 , syn_toplevel :: Bool
1609 , withAppAllowed :: Bool
1610 } deriving (Show, Generic)
1612deriving instance Binary SyntaxInfo
1615defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1617expandNS :: SyntaxInfo -> Name -> Name
1618expandNS syn n@(NS _ _) = n
1619expandNS syn n = case syn_namespace syn of
1624-- For inferring types of things
1626bi = fileFC "builtin"
1627primfc = fileFC "(primitive)"
1629inferTy = sMN 0 "__Infer"
1630inferCon = sMN 0 "__infer"
1631inferDecl = PDatadecl inferTy primfc
1633 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1634 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1635 (PRef bi [] inferTy)), bi, [])]
1638infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1639infP = P (TCon 6 0) inferTy (TType (UVal 0))
1641getInferTerm, getInferType :: Term -> Term
1642getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1643getInferTerm (App _ (App _ _ _) tm) = tm
1644getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1646getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1647 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1648 toTy (PVar _ t) = PVTy t
1650getInferType (App _ (App _ _ ty) _) = ty
1654-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1656primNames = [inferTy, inferCon]
1659unitCon = sUN "MkUnit"
1661falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1662 "The empty type, also known as the trivially false proposition." ++
1664 "Use `void` or `absurd` to prove anything if you have a variable " ++
1665 "of type `Void` in scope."
1668pairTy = sNS (sUN "Pair") ["Builtins"]
1669pairCon = sNS (sUN "MkPair") ["Builtins"]
1671upairTy = sNS (sUN "UPair") ["Builtins"]
1672upairCon = sNS (sUN "MkUPair") ["Builtins"]
1676eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1677 "The propositional equality type. A proof that `x` = `y`." ++
1679 "To use such a proof, pattern-match on it, and the two equal things will " ++
1680 "then need to be the _same_ pattern." ++
1682 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1683 "is possible to state equalities between values of potentially different " ++
1684 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1686 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1688eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1689 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1691 [(reflDoc, reflParamDoc,
1692 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1693 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1694 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1695 pimp (n "B") Placeholder False,
1696 pexp (PRef bi [] (n "x")),
1697 pexp (PRef bi [] (n "x"))])), bi, [])]
1699 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1700 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1701 "shown that both sides are in fact equal."
1702 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1703 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1705eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1706 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1712-- | The special name to be used in the module documentation context -
1713-- not for use in the main definition context. The namespace around it
1714-- will determine the module to which the docs adhere.
1716modDocName = sMN 0 "ModuleDocs"
1718-- Defined in builtins.idr
1719sigmaTy = sNS (sUN "DPair") ["Builtins"]
1720sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1722piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1723piBind = piBindp expl
1725piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1727piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1730-- Pretty-printing declarations and terms
1732-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1733-- could interfere with interactive editing, which calls "show".
1735instance Show PTerm where
1736 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1738instance Show PDecl where
1739 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1741instance Show PClause where
1742 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1744instance Show PData where
1745 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1747instance Pretty PTerm OutputAnnotation where
1748 pretty = prettyImp defaultPPOption
1750-- | Colourise annotations according to an Idris state. It ignores the
1751-- names in the annotation, as there's no good way to show extended
1752-- information on a terminal.
1753annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1754annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1755annotationColour ist (AnnConst c) =
1756 let theme = idris_colourTheme ist
1757 in Just $ if constIsType c
1758 then typeColour theme
1759 else dataColour theme
1760annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1761annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1762annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1763annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1764annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1765annotationColour ist (AnnName n _ _ _) =
1766 let ctxt = tt_ctxt ist
1767 theme = idris_colourTheme ist
1769 _ | isDConName n ctxt -> Just $ dataColour theme
1770 _ | isFnName n ctxt -> Just $ functionColour theme
1771 _ | isTConName n ctxt -> Just $ typeColour theme
1772 _ | isPostulateName n ist -> Just $ postulateColour theme
1773 _ | otherwise -> Nothing -- don't colourise unknown names
1774annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1775 where colour BoldText = IdrisColour Nothing True False True False
1776 colour UnderlineText = IdrisColour Nothing True True False False
1777 colour ItalicText = IdrisColour Nothing True False False True
1778annotationColour ist _ = Nothing
1781-- | Colourise annotations according to an Idris state. It ignores the
1782-- names in the annotation, as there's no good way to show extended
1783-- information on a terminal. Note that strings produced this way will
1784-- not be coloured on Windows, so the use of the colour rendering
1785-- functions in Idris.Output is to be preferred.
1786consoleDecorate :: IState -> OutputAnnotation -> String -> String
1787consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1789isPostulateName :: Name -> IState -> Bool
1790isPostulateName n ist = S.member n (idris_postulates ist)
1792-- | Pretty-print a high-level closed Idris term with no information
1793-- about precedence/associativity
1794prettyImp :: PPOption -- ^ pretty printing options
1795 -> PTerm -- ^ the term to pretty-print
1796 -> Doc OutputAnnotation
1797prettyImp impl = pprintPTerm impl [] [] []
1799-- | Serialise something to base64 using its Binary implementation.
1801-- | Do the right thing for rendering a term in an IState
1802prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1803prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1805-- | Pretty-print a high-level Idris term in some bindings context
1807pprintPTerm :: PPOption -- ^ pretty printing options
1808 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1809 -> [Name] -- ^ names to always show in pi, even if not used
1810 -> [FixDecl] -- ^ Fixity declarations
1811 -> PTerm -- ^ the term to pretty-print
1812 -> Doc OutputAnnotation
1813pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1818 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1819 prettySe d p bnd (PQuote r) =
1820 text "![" <> pretty r <> text "]"
1821 prettySe d p bnd (PPatvar fc n) = pretty n
1823 | Just str <- slist d p bnd e = depth d str
1824 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1825 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1826 prettySe d p bnd (PLam fc n nfc ty sc) =
1827 let (ns, sc') = getLamNames [n] sc in
1828 depth d . bracket p startPrec . group . align . hang 2 $
1829 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1830 prettySe (decD d) startPrec ((n, False):bnd) sc'
1832 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1833 getLamNames acc sc = (reverse acc, sc)
1835 prettyBindingsOf [] t = text ""
1836 prettyBindingsOf [n] t = prettyBindingOf n t
1837 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1838 prettyBindingsOf ns t
1839 prettySe d p bnd (PLet fc n nfc ty v sc) =
1840 depth d . bracket p startPrec . group . align $
1841 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1842 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1843 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1845 depth d . bracket p startPrec . group $
1846 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1847 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1849 depth d . bracket p startPrec . group $
1850 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1851 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1852 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1853 || ppopt_pinames ppo && uname n =
1854 depth d . bracket p startPrec . group $
1855 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1856 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1858 depth d . bracket p startPrec . group $
1859 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1860 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1862 uname (UN n) = case str n of
1869 Static -> text "%static" <> space
1871 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1873 depth d . bracket p startPrec $
1874 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1875 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1876 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1878 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1879 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1880 showRig _ n = prettyBindingOf n True
1884 Static -> text "%static" <> space
1886 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1887 depth d . bracket p startPrec $
1888 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1889 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1890 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1891 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1892 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1893 depth d . bracket p startPrec $
1894 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1895 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1896 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1897 | basename neg == sUN "negate" =
1898 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1899 -- This case preserves the behavior of the former constructor PEq.
1900 -- It should be removed if feasible when the pretty-printing of infix
1901 -- operators in general is improved.
1902 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1903 | n == eqTy, ppopt_impl ppo =
1904 depth d . bracket p eqPrec $
1905 enclose lparen rparen eq <+>
1906 align (group (vsep (map (prettyArgS (decD d) bnd)
1909 depth d . bracket p eqPrec . align . group $
1910 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1911 where eq = annName eqTy (text "=")
1913 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1914 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1915 | UN nm <- basename f
1916 , not (ppopt_impl ppo) && null (getShowArgs args) =
1917 prettyName True (ppopt_impl ppo) bnd f
1918 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1919 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1920 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1921 | UN nm <- basename op
1923 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1924 case getShowArgs args of
1926 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1927 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1928 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1929 (l@(PExp{}) : r@(PExp{}) : rest) ->
1930 depth d . bracket p funcAppPrec $
1931 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1932 align (group (vsep (map (prettyArgS d bnd) rest)))
1933 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1934 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1935 f = getFixity (opStr op)
1937 Nothing -> funcAppPrec + 1
1938 Just (Infixl p') -> p'
1939 Just f' -> prec f' + 1
1941 Nothing -> funcAppPrec + 1
1942 Just (Infixr p') -> p'
1943 Just f' -> prec f' + 1
1944 inFix l r = align . group $
1945 (prettySe (decD d) left bnd l <+> opName False) <$>
1946 group (prettySe (decD d) right bnd r)
1947 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1948 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1949 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1950 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1951 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1952 let args = getShowArgs as
1953 fp = prettySe (decD d) (startPrec + 1) bnd f
1954 shownArgs = if ppopt_impl ppo then as else args
1956 depth d . bracket p funcAppPrec . group $
1959 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1960 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1961 prettySe d p bnd (PCase _ scr cases) =
1962 bracket p funcAppPrec $
1963 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1964 depth d (indent 2 (vsep (map ppcase cases)))
1966 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1967 ([(n, False) | n <- vars l] ++ bnd)
1968 in nest nestingSize $
1969 prettyCase l <+> text "=>" <+> prettyCase r
1970 -- Warning: this is a bit of a hack. At this stage, we don't have the
1971 -- global context, so we can't determine which names are constructors,
1972 -- which are types, and which are pattern variables on the LHS of the
1973 -- case pattern. We use the heuristic that names without a namespace
1974 -- are patvars, because right now case blocks in PTerms are always
1975 -- delaborated from TT before being sent to the pretty-printer. If they
1976 -- start getting printed directly, THIS WILL BREAK.
1977 -- Potential solution: add a list of known patvars to the cases in
1978 -- PCase, and have the delaborator fill it out, kind of like the pun
1979 -- disambiguation on PDPair.
1980 vars tm = filter noNS (allNamesIn tm)
1981 noNS (NS _ _) = False
1984 prettySe d p bnd (PIfThenElse _ c t f) =
1985 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1986 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1987 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1988 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1990 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1991 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1992 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1993 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1994 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1995 prettySe d p bnd (PRewrite _ by l r _) =
1996 depth d . bracket p startPrec $
1997 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
2000 Just fn -> text "using" <+>
2001 prettyName True (ppopt_impl ppo) bnd fn) <+>
2002 text "in" <+> prettySe (decD d) startPrec bnd r
2003 prettySe d p bnd (PTyped l r) =
2004 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
2005 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
2006 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
2007 align . group . vsep . punctuate (ann comma) $
2008 map (prettySe (decD d) startPrec bnd) elts
2009 where ann = case pun of
2011 IsType -> annName pairTy
2012 IsTerm -> annName pairCon
2013 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
2014 | Just elts <- dPairElts dpair
2015 = depth d . enclose (annotated lparen) (annotated rparen) .
2016 align . group . vsep . punctuate (space <> annotated (text "**")) $
2022 annotated (text "**") <+>
2023 prettySe (decD d) startPrec (addBinding bnd) r <>
2025 where annotated = case pun of
2026 IsType -> annName sigmaTy
2027 IsTerm -> annName sigmaCon
2030 (left, addBinding) = case (l, pun) of
2031 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
2032 _ -> (prettySe (decD d) startPrec bnd l, id)
2035 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
2036 ppElts ((PRef _ _ n, t):rs) bs
2038 = (bindingOf n False <+> colon <+>
2039 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2040 ppElts ((l, t):rs) bs
2041 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2042 prettySe d p bnd (PAlternative ns a as) =
2043 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2046 foldr ((\ l r -> l <+> text "," <+> r) .
2047 depth d . prettySe (decD d) startPrec bnd)
2049 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2050 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2051 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2052 -- XXX: add pretty for tactics
2053 prettySe d p bnd (PProof ts) =
2054 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2055 prettySe d p bnd (PTactics ts) =
2056 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2057 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2058 prettySe d p bnd PImpossible = kwd "impossible"
2059 prettySe d p bnd Placeholder = text "_"
2060 prettySe d p bnd (PDoBlock dos) =
2061 bracket p startPrec $
2062 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2063 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2064 ppdo bnd (DoBind _ bn _ tm : dos) =
2065 (prettyBindingOf bn False <+> text "<-" <+>
2066 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2067 ppdo ((bn, False):bnd) dos
2068 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2069 text "no pretty printer for pattern-matching do binding" :
2071 ppdo bnd (DoLet _ ln _ ty v : dos) =
2072 (kwd "let" <+> prettyBindingOf ln False <+>
2073 (if ty /= Placeholder
2074 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2076 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2077 ppdo ((ln, False):bnd) dos
2078 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2079 text "no pretty printer for pattern-matching do binding" :
2082 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2083 prettySe d p bnd (PElabError s) = pretty s
2084 -- Quasiquote pprinting ignores bound vars
2085 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2086 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2087 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2088 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2089 where start = if res then "`{" else "`{{"
2090 end = if res then "}" else "}}"
2091 prettySe d p bnd (PRunElab _ tm _) =
2092 bracket p funcAppPrec . group . align . hang 2 $
2094 prettySe (decD d) funcAppPrec bnd tm
2095 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2096 prettySe d p bnd _ = text "missing pretty-printer for term"
2098 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2099 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2100 where display (UN n) = T.unpack n
2101 display (MN _ n) = T.unpack n
2102 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2103 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2106 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2107 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2108 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2109 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2111 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2112 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2113 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2114 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2116 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2117 annName n = annotate (AnnName n Nothing Nothing Nothing)
2119 opStr :: Name -> String
2120 opStr (NS n _) = opStr n
2121 opStr (UN n) = T.unpack n
2123 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2124 slist' (Just d) _ _ _ | d <= 0 = Nothing
2126 | containsHole e = Nothing
2127 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2128 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2129 slist' d p bnd (PRef _ _ nil)
2130 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2131 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2132 | nsroot cons == sUN "::",
2133 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2135 Just tl' <- slist' (decD d) p bnd tl
2136 = Just (prettySe d startPrec bnd hd : tl')
2138 isImp (PImp {}) = True
2140 slist' _ _ _ tm = Nothing
2142 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2144 [] -> annotate (AnnData "" "") $ text "[]"
2145 [x] -> enclose left right . group $ x
2146 xs -> enclose left right .
2147 align . group . vsep .
2148 punctuate comma $ xs
2149 where left = (annotate (AnnData "" "") (text "["))
2150 right = (annotate (AnnData "" "") (text "]"))
2151 comma = (annotate (AnnData "" "") (text ","))
2152 slist _ _ _ _ = Nothing
2154 pairElts :: PTerm -> Maybe [PTerm]
2155 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2156 | otherwise = Just [x, y]
2157 pairElts _ = Nothing
2159 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2160 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2161 | otherwise = Just [(l, t), (Placeholder, r)]
2162 dPairElts _ = Nothing
2164 natns = "Prelude.Nat."
2166 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2168 | ppopt_desugarnats ppo = Nothing
2169 | otherwise = snat' d p e
2171 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2172 snat' (Just x) _ _ | x <= 0 = Nothing
2173 snat' d p (PRef _ _ z)
2174 | show z == (natns++"Z") || show z == "Z" = Just 0
2175 snat' d p (PApp _ s [PExp {getTm=n}])
2176 | show s == (natns++"S") || show s == "S",
2177 Just n' <- snat' (decD d) p n
2179 snat' _ _ _ = Nothing
2181 bracket outer inner doc
2182 | outer > inner = lparen <> doc <> rparen
2185 ellipsis = text "..."
2188 depth (Just d) = if d <= 0 then const ellipsis else id
2190 decD = fmap (\x -> x - 1)
2192 kwd = annotate AnnKeyword . text
2194 fixities :: M.Map String Fixity
2195 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2197 getFixity :: String -> Maybe Fixity
2198 getFixity = flip M.lookup fixities
2200-- | Strip away namespace information
2201basename :: Name -> Name
2202basename (NS n _) = basename n
2205-- | Determine whether a name was the one inserted for a hole or guess
2206-- by the delaborator
2207isHoleName :: Name -> Bool
2208isHoleName (UN n) = n == T.pack "[__]"
2211-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2212containsHole :: PTerm -> Bool
2213containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2215-- | Pretty-printer helper for names that attaches the correct annotations
2216prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2217 -> Bool -- ^ whether to show namespaces
2218 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2219 -> Name -- ^ the name to pprint
2220 -> Doc OutputAnnotation
2221prettyName infixParen showNS bnd n
2222 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2223 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2224 | (UN n') <- n, T.unpack n' == "_" = text "_"
2225 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2226 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2227 where fullName = text nameSpace <> parenthesise (text (baseName n))
2228 baseName (UN n) = T.unpack n
2229 baseName (NS n ns) = baseName n
2230 baseName (MN i s) = T.unpack s
2231 baseName other = show other
2232 nameSpace = case n of
2233 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2235 isInfix = case baseName n of
2237 (c : _) -> not (isAlpha c)
2238 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2241showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2242showCImp ppo (PClause _ n l ws r w)
2243 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2244 <+> text "where" <+> text (show w)
2247 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2248showCImp ppo (PWith _ n l ws r pn w)
2249 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2250 <+> braces (text (show w))
2253 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2256showDImp :: PPOption -> PData -> Doc OutputAnnotation
2257showDImp ppo (PDatadecl n nfc ty cons)
2258 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2259 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2261showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2262showDecls o ds = vsep (map (showDeclImp o) ds)
2264showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2265showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2266showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2267 indent 2 (vsep (map (showCImp o) cs))
2268showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2269showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2270showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2271showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2272showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2273showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2274 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2275showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2276 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2277showDeclImp _ _ = text "..."
2278-- showDeclImp (PImport o) = "import " ++ o
2280getImps :: [PArg] -> [(Name, PTerm)]
2282getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2283getImps (_ : xs) = getImps xs
2285getExps :: [PArg] -> [PTerm]
2287getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2288getExps (_ : xs) = getExps xs
2290getShowArgs :: [PArg] -> [PArg]
2292getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2293getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2294 | PImp _ _ _ _ tm <- e
2295 , containsHole tm = e : getShowArgs xs
2296getShowArgs (_ : xs) = getShowArgs xs
2298getConsts :: [PArg] -> [PTerm]
2300getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2301getConsts (_ : xs) = getConsts xs
2303getAll :: [PArg] -> [PTerm]
2308showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2309 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2310 -> PPOption -- ^ pretty printing options
2311 -> Bool -- ^ whether to colourise
2312 -> Name -- ^ the term to show
2314showName ist bnd ppo colour n = case ist of
2315 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2316 Nothing -> showbasic n
2317 where name = if ppopt_impl ppo then show n else showbasic n
2318 showbasic n@(UN _) = showCG n
2319 showbasic (MN i s) = str s
2320 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2321 showbasic (SN s) = show s
2323 colourise n t = let ctxt' = fmap tt_ctxt ist in
2326 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2327 else colouriseBound t name
2328 | isDConName n ctxt -> colouriseData t name
2329 | isFnName n ctxt -> colouriseFun t name
2330 | isTConName n ctxt -> colouriseType t name
2331 -- The assumption is that if a name is not bound and does not exist in the
2332 -- global context, then we're somewhere in which implicit info has been lost
2333 -- (like error messages). Thus, unknown vars are colourised as implicits.
2334 | otherwise -> colouriseImplicit t name
2336showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2337 -> PTerm -- ^ the term to show
2339showTm ist = displayDecorated (consoleDecorate ist) .
2340 renderPretty 0.8 100000 .
2341 prettyImp (ppOptionIst ist)
2343-- | Show a term with implicits, no colours
2344showTmImpls :: PTerm -> String
2345showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2347-- | Show a term with specific options
2348showTmOpts :: PPOption -> PTerm -> String
2349showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2352instance Sized PTerm where
2353 size (PQuote rawTerm) = size rawTerm
2354 size (PRef fc _ name) = size name
2355 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2356 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2357 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2358 size (PTyped trm ty) = 1 + size trm + size ty
2359 size (PApp fc name args) = 1 + size args
2360 size (PAppBind fc name args) = 1 + size args
2361 size (PCase fc trm bdy) = 1 + size trm + size bdy
2362 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2363 size (PTrue fc _) = 1
2364 size (PResolveTC fc) = 1
2365 size (PRewrite fc by left right _) = 1 + size left + size right
2366 size (PPair fc _ _ left right) = 1 + size left + size right
2367 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2368 size (PAlternative _ a alts) = 1 + size alts
2369 size (PHidden hidden) = size hidden
2370 size (PUnifyLog tm) = size tm
2371 size (PDisamb _ tm) = size tm
2372 size (PNoImplicits tm) = size tm
2374 size (PUniverse _ _) = 1
2375 size (PConstant fc const) = 1 + size fc + size const
2376 size Placeholder = 1
2377 size (PDoBlock dos) = 1 + size dos
2378 size (PIdiom fc term) = 1 + size term
2379 size (PMetavar _ name) = 1
2380 size (PProof tactics) = size tactics
2381 size (PElabError err) = size err
2382 size PImpossible = 1
2385getPArity :: PTerm -> Int
2386getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2389-- Return all names, free or globally bound, in the given term.
2391allNamesIn :: PTerm -> [Name]
2392allNamesIn tm = nub $ ni 0 [] tm
2393 where -- TODO THINK added niTacImp, but is it right?
2394 ni 0 env (PRef _ _ n)
2395 | not (n `elem` env) = [n]
2396 ni 0 env (PPatvar _ n) = [n]
2397 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2398 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2399 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2400 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2401 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2402 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2403 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2404 ni 0 env (PHidden tm) = ni 0 env tm
2405 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2406 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2407 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2408 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2409 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2410 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2411 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2412 ni 0 env (PUnifyLog tm) = ni 0 env tm
2413 ni 0 env (PDisamb _ tm) = ni 0 env tm
2414 ni 0 env (PNoImplicits tm) = ni 0 env tm
2416 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2417 ni i env (PUnquote tm) = ni (i - 1) env tm
2418 ni i env tm = concatMap (ni i env) (children tm)
2420 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2424-- Return all names defined in binders in the given term
2425boundNamesIn :: PTerm -> [Name]
2426boundNamesIn tm = S.toList (ni 0 S.empty tm)
2427 where -- TODO THINK Added niTacImp, but is it right?
2428 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2429 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2430 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2431 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2432 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2433 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2434 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2435 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2436 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2437 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2438 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2439 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2440 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2441 ni 0 set (PAlternative ns a as) = niTms 0 set as
2442 ni 0 set (PHidden tm) = ni 0 set tm
2443 ni 0 set (PUnifyLog tm) = ni 0 set tm
2444 ni 0 set (PDisamb _ tm) = ni 0 set tm
2445 ni 0 set (PNoImplicits tm) = ni 0 set tm
2447 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2448 ni i set (PUnquote tm) = ni (i - 1) set tm
2450 ni i set tm = foldr (S.union . ni i set) set (children tm)
2452 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2453 niTms i set [] = set
2454 niTms i set (x : xs) = niTms i (ni i set x) xs
2456 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2457 niTacImp i set _ = set
2459-- Return names which are valid implicits in the given term (type).
2460implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2461implicitNamesIn uvars ist tm
2462 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2465 addImp n = do (imps, fns) <- get
2467 addFn n = do (imps, fns) <- get
2471 notCAF (PExp _ _ _ _ : _) = True
2472 notCAF (_ : xs) = notCAF xs
2474 notHidden (n, _) = case getAccessibility n of
2480 = case lookupDefAccExact n False (tt_ctxt ist) of
2484 ni 0 env (PRef _ _ n@(NS _ _))
2485 | not (n `elem` env)
2486 -- Never implicitly bind if there's a namespace
2488 ni 0 env (PRef _ _ n)
2489 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2490 ni 0 env (PApp _ f@(PRef _ _ n) as)
2491 | n `elem` uvars = do ni 0 env f
2492 mapM_ (ni 0 env . getTm) as
2493 | otherwise = do case lookupTy n (tt_ctxt ist) of
2496 mapM_ (ni 0 env . getTm) as
2497 ni 0 env (PApp _ f as) = do ni 0 env f
2498 mapM_ (ni 0 env . getTm) as
2499 ni 0 env (PAppBind _ f as) = do ni 0 env f
2500 mapM_ (ni 0 env . getTm) as
2501 ni 0 env (PCase _ c os) = do ni 0 env c
2502 -- names in 'os', not counting the names bound in the cases
2503 mapM_ (ni 0 env . snd) os
2506 mapM_ (ni 0 env . fst) os
2508 put (nub imps \\ nub impsfst, fns)
2509 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2510 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2511 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2512 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2513 ni 0 env val; ni 0 (n:env) sc
2514 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2515 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2516 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2517 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2518 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2521 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2522 ni 0 env (PHidden tm) = ni 0 env tm
2523 ni 0 env (PUnifyLog tm) = ni 0 env tm
2524 ni 0 env (PDisamb _ tm) = ni 0 env tm
2525 ni 0 env (PNoImplicits tm) = ni 0 env tm
2527 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2528 maybe (return ()) (ni i env) ty
2529 ni i env (PUnquote tm) = ni (i - 1) env tm
2531 ni i env tm = mapM_ (ni i env) (children tm)
2533-- Return names which are free in the given term.
2534namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2535namesIn uvars ist tm = nub $ ni 0 [] tm
2537 ni 0 env (PRef _ _ n)
2538 | not (n `elem` env)
2539 = case lookupTy n (tt_ctxt ist) of
2541 _ -> [n | n `elem` (map fst uvars)]
2542 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2543 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2544 ni 0 env (PCase _ c os) = ni 0 env c ++
2545 -- names in 'os', not counting the names bound in the cases
2546 (nub (concatMap (ni 0 env . snd) os)
2547 \\ nub (concatMap (ni 0 env . fst) os))
2548 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2549 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2550 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2551 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2552 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2553 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2554 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2555 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2556 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2557 ni 0 env (PHidden tm) = ni 0 env tm
2558 ni 0 env (PUnifyLog tm) = ni 0 env tm
2559 ni 0 env (PDisamb _ tm) = ni 0 env tm
2560 ni 0 env (PNoImplicits tm) = ni 0 env tm
2562 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2563 ni i env (PUnquote tm) = ni (i - 1) env tm
2565 ni i env tm = concatMap (ni i env) (children tm)
2567 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2570-- Return which of the given names are used in the given term.
2572usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2573usedNamesIn vars ist tm = nub $ ni 0 [] tm
2574 where -- TODO THINK added niTacImp, but is it right?
2575 ni 0 env (PRef _ _ n)
2576 | n `elem` vars && not (n `elem` env)
2577 = case lookupDefExact n (tt_ctxt ist) of
2580 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2581 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2582 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2583 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2584 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2585 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2586 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2587 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2588 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2589 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2590 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2591 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2592 ni 0 env (PHidden tm) = ni 0 env tm
2593 ni 0 env (PUnifyLog tm) = ni 0 env tm
2594 ni 0 env (PDisamb _ tm) = ni 0 env tm
2595 ni 0 env (PNoImplicits tm) = ni 0 env tm
2597 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2598 ni i env (PUnquote tm) = ni (i - 1) env tm
2600 ni i env tm = concatMap (ni i env) (children tm)
2602 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2605-- Return the list of inaccessible (= dotted) positions for a name.
2606getErasureInfo :: IState -> Name -> [Int]
2607getErasureInfo ist n =
2608 case lookupCtxtExact n (idris_optimisation ist) of
2609 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