2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
8{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,
9 FlexibleInstances, MultiParamTypeClasses, PatternGuards,
10 TypeSynonymInstances #-}
12module Idris.AbsSyntaxTree where
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
18import Idris.Core.Typecheck
19import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
25import Prelude hiding ((<$>))
27import Control.Applicative ((<|>))
28import qualified Control.Monad.Trans.Class as Trans (lift)
29import Control.Monad.Trans.Except
30import Control.Monad.Trans.State.Strict
32import Data.Data (Data)
34import Data.Foldable (Foldable)
35import Data.Function (on)
36import Data.Generics.Uniplate.Data (children, universe)
37import Data.List hiding (group)
38import qualified Data.Map.Strict as M
39import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
40import qualified Data.Set as S
41import qualified Data.Text as T
42import Data.Traversable (Traversable)
44import Data.Word (Word)
46import GHC.Generics (Generic)
47import Network.Socket (PortNumber)
48import System.Console.Haskeline
50import Text.PrettyPrint.Annotated.Leijen
52data ElabWhat = ETypes | EDefns | EAll
55-- | Data to pass to recursively called elaborators; e.g. for where blocks,
56-- paramaterised declarations, etc.
58-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
59-- so that we can have mutually recursive elaborators in separate modules without
60-- having to muck about with cyclic modules.
61data ElabInfo = EInfo {
62 params :: [(Name, PTerm)]
63 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
64 , liftname :: Name -> Name
65 , namespace :: [String]
67 , constraintNS :: String -- ^ filename for adding to constraint variables
70 -- | We may, recursively, collect transformations to do on the rhs,
71 -- e.g. rewriting recursive calls to functions defined by 'with'
72 , rhs_trans :: PTerm -> PTerm
73 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
77toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")
79toplevelWith :: String -> ElabInfo
80toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")
82eInfoNames :: ElabInfo -> [Name]
83eInfoNames info = map fst (params info) ++ M.keys (inblock info)
85data IOption = IOption {
87 , opt_logcats :: [LogCat] -- ^ List of logging categories.
88 , opt_typecase :: Bool
89 , opt_typeintype :: Bool
90 , opt_coverage :: Bool
91 , opt_showimp :: Bool -- ^ show implicits
92 , opt_errContext :: Bool
95 , opt_nobanner :: Bool
97 , opt_codegen :: Codegen
98 , opt_outputTy :: OutputType
99 , opt_ibcsubdir :: FilePath
100 , opt_importdirs :: [FilePath]
101 , opt_sourcedirs :: [FilePath]
102 , opt_triple :: String
104 , opt_cmdline :: [Opt] -- ^ remember whole command line
105 , opt_origerr :: Bool
106 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
107 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
108 , opt_optimise :: [Optimisation]
109 , opt_printdepth :: Maybe Int
110 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
111 , opt_desugarnats :: Bool
112 , opt_autoimpls :: Bool
113 } deriving (Show, Eq, Generic)
115defaultOpts = IOption { opt_logLevel = 0
117 , opt_typecase = False
118 , opt_typeintype = False
119 , opt_coverage = True
120 , opt_showimp = False
121 , opt_errContext = False
124 , opt_nobanner = False
126 , opt_codegen = Via IBCFormat "c"
127 , opt_outputTy = Executable
129 , opt_importdirs = []
130 , opt_sourcedirs = []
134 , opt_origerr = False
135 , opt_autoSolve = True
136 , opt_autoImport = []
137 , opt_optimise = defaultOptimise
138 , opt_printdepth = Just 5000
139 , opt_evaltypes = True
140 , opt_desugarnats = False
141 , opt_autoimpls = True
144data PPOption = PPOption {
145 ppopt_impl :: Bool -- ^ whether to show implicits
146 , ppopt_desugarnats :: Bool
147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
148 , ppopt_depth :: Maybe Int
151data Optimisation = PETransform -- ^ partial eval and associated transforms
152 deriving (Show, Eq, Generic)
154defaultOptimise = [PETransform]
156-- | Pretty printing options with default verbosity.
157defaultPPOption :: PPOption
158defaultPPOption = PPOption {
160 , ppopt_desugarnats = False
161 , ppopt_pinames = False
162 , ppopt_depth = Nothing
165-- | Pretty printing options with the most verbosity.
166verbosePPOption :: PPOption
167verbosePPOption = PPOption {
169 , ppopt_desugarnats = True
170 , ppopt_pinames = True
171 , ppopt_depth = Nothing
174-- | Get pretty printing options from the big options record.
175ppOption :: IOption -> PPOption
176ppOption opt = PPOption {
177 ppopt_impl = opt_showimp opt
178 , ppopt_pinames = False
179 , ppopt_depth = opt_printdepth opt
180 , ppopt_desugarnats = opt_desugarnats opt
183-- | Get pretty printing options from an idris state record.
184ppOptionIst :: IState -> PPOption
185ppOptionIst = ppOption . idris_options
187data LanguageExt = TypeProviders | ErrorReflection
188 deriving (Show, Eq, Read, Ord, Generic)
190-- | The output mode in use
191data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
192 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
195-- | How wide is the console?
196data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
197 | ColsWide Int -- ^ Manually specified - must be positive
198 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
199 deriving (Show, Eq, Generic)
201-- | If a function has no totality annotation, what do we assume?
202data DefaultTotality = DefaultCheckingTotal -- ^ Total
203 | DefaultCheckingPartial -- ^ Partial
204 | DefaultCheckingCovering -- ^Total coverage, but may diverge
205 deriving (Show, Eq, Generic)
207-- | The global state used in the Idris monad
208data IState = IState {
209 tt_ctxt :: Context -- ^ All the currently defined names and their terms
210 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
211 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
212 , idris_implicits :: Ctxt [PArg]
213 , idris_statics :: Ctxt [Bool]
214 , idris_interfaces :: Ctxt InterfaceInfo
215 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
216 , idris_records :: Ctxt RecordInfo
217 , idris_dsls :: Ctxt DSL
218 , idris_optimisation :: Ctxt OptInfo
219 , idris_datatypes :: Ctxt TypeInfo
220 , idris_namehints :: Ctxt [Name]
222 -- | list of lhs/rhs, and a list of missing clauses. These are not
224 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
225 , idris_flags :: Ctxt [FnOpt]
226 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
227 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
229 -- | module documentation is saved in a special MN so the context
230 -- mechanism can be used for disambiguation.
231 , idris_moduledocs :: Ctxt (Docstring DocTerm)
232 , idris_tyinfodata :: Ctxt TIData
233 , idris_fninfo :: Ctxt FnInfo
234 , idris_transforms :: Ctxt [(Term, Term)]
235 , idris_autohints :: Ctxt [Name]
236 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
237 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
238 , idris_totcheckfail :: [(FC, String)]
239 , idris_options :: IOption
241 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
243 -- | The currently defined but not proven metavariables. The Int is
244 -- the number of vars to display as a context, the Maybe Name is its
245 -- top-level function, the [Name] is the list of local variables
246 -- available for proof search and the Bools are whether :p is
247 -- allowed, and whether the variable is definable at all
248 -- (Metavariables are not definable if they are applied in a term
249 -- which still has hole bindings)
250 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
251 , idris_coercions :: [Name]
252 , idris_errRev :: [(Term, Term)]
253 , syntax_rules :: SyntaxRules
254 , syntax_keywords :: [String]
255 , imported :: [FilePath] -- ^ The imported modules
256 , idris_scprims :: [(Name, (Int, PrimFn))]
257 , idris_objs :: [(Codegen, FilePath)]
258 , idris_libs :: [(Codegen, String)]
259 , idris_cgflags :: [(Codegen, String)]
260 , idris_hdrs :: [(Codegen, String)]
261 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
262 , proof_list :: [(Name, (Bool, [String]))]
263 , errSpan :: Maybe FC
264 , parserWarnings :: [(FC, Err)]
265 , lastParse :: Maybe Name
266 , indent_stack :: [Int]
267 , brace_stack :: [Maybe Int]
268 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
269 , idris_parsedSpan :: Maybe FC
270 , hide_list :: Ctxt Accessibility
271 , default_access :: Accessibility
272 , default_total :: DefaultTotality
273 , ibc_write :: [IBCWrite]
274 , compiled_so :: Maybe String
275 , idris_dynamic_libs :: [DynamicLib]
276 , idris_language_extensions :: [LanguageExt]
277 , idris_outputmode :: OutputMode
278 , idris_colourRepl :: Bool
279 , idris_colourTheme :: ColourTheme
280 , idris_errorhandlers :: [Name] -- ^ Global error handlers
281 , idris_nameIdx :: (Int, Ctxt (Int, Name))
282 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
283 , module_aliases :: M.Map [T.Text] [T.Text]
284 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
285 , idris_postulates :: S.Set Name
286 , idris_externs :: S.Set (Name, Int)
287 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
288 , idris_whocalls :: Maybe (M.Map Name [Name])
289 , idris_callswho :: Maybe (M.Map Name [Name])
291 -- | List of names that were defined in the repl, and can be re-/un-defined
292 , idris_repl_defs :: [Name]
294 -- | Stack of names currently being elaborated, Bool set if it's an
295 -- implementation (implementations appear twice; also as a funtion name)
296 , elab_stack :: [(Name, Bool)]
299 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
300 , idris_exports :: [Name] -- ^ Functions with ExportList
301 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
302 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
303 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
304 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
305 , idris_ttstats :: M.Map Term (Int, Term)
306 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
310-- Required for parsers library, and therefore trifecta
311instance Show IState where
312 show = const "{internal state}"
314data SizeChange = Smaller | Same | Bigger | Unknown
315 deriving (Show, Eq, Generic)
317deriving instance Binary SizeChange
320type SCGEntry = (Name, [Maybe (Int, SizeChange)])
321type UsageReason = (Name, Int) -- fn_name, its_arg_number
323data CGInfo = CGInfo {
326 , usedpos :: [(Int, [UsageReason])]
327 } deriving (Show, Generic)
329deriving instance Binary CGInfo
332primDefs = [ sUN "unsafePerformPrimIO"
333 , sUN "mkLazyForeignPrim"
334 , sUN "mkForeignPrim"
336 , sUN "assert_unreachable"
339-- information that needs writing for the current module's .ibc file
340data IBCWrite = IBCFix FixDecl
345 | IBCImplementation Bool Bool Name Name
352 | IBCImport (Bool, FilePath) -- ^ True = import public
353 | IBCImportDir FilePath
354 | IBCSourceDir FilePath
355 | IBCObj Codegen FilePath
356 | IBCLib Codegen String
357 | IBCCGFlag Codegen String
359 | IBCHeader Codegen String
360 | IBCAccess Name Accessibility
361 | IBCMetaInformation Name MetaInformation
362 | IBCTotal Name Totality
363 | IBCInjective Name Injectivity
364 | IBCFlags Name [FnOpt]
365 | IBCFnInfo Name FnInfo
366 | IBCTrans Name (Term, Term)
367 | IBCErrRev (Term, Term)
371 | IBCDef Name -- ^ The main context.
372 | IBCNameHint (Name, Name)
373 | IBCLineApp FilePath Int PTerm
374 | IBCErrorHandler Name
375 | IBCFunctionErrorHandler Name Name Name
377 | IBCExtern (Name, Int)
378 | IBCTotCheckErr FC String
380 | IBCModDocs Name -- ^ The name is the special name used to track module docs
381 | IBCUsage (Name, Int)
383 | IBCAutoHint Name Name
384 | IBCDeprecate Name String
385 | IBCFragile Name String
386 | IBCConstraint FC UConstraint
387 deriving (Show, Generic)
389-- | The initial state for the compiler
391idrisInit = IState initContext S.empty []
392 emptyContext emptyContext emptyContext [] emptyContext
393 emptyContext emptyContext emptyContext emptyContext
394 emptyContext emptyContext emptyContext emptyContext
395 emptyContext emptyContext emptyContext emptyContext
397 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
398 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
399 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
400 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
401 emptyContext S.empty M.empty emptyContext
404-- | The monad for the main REPL - reading and processing files and
405-- updating global state (hence the IO inner monad).
408-- type Idris = WriterT [Either String (IO ())] (State IState a))
411type Idris = StateT IState (ExceptT Err IO)
413catchError :: Idris a -> (Err -> Idris a) -> Idris a
414catchError = liftCatch catchE
416throwError :: Err -> Idris a
417throwError = Trans.lift . throwE
419-- Commands in the REPL
421data Codegen = Via IRFormat String
423 deriving (Show, Eq, Generic)
425data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
427data HowMuchDocs = FullDocs | OverviewDocs
429data OutputFmt = HTMLOutput | LaTeXOutput
431-- | Recognised logging categories for the Idris compiler.
433-- @TODO add in sub categories.
440 deriving (Show, Eq, Ord, Generic)
442strLogCat :: LogCat -> String
443strLogCat IParse = "parser"
444strLogCat IElab = "elab"
445strLogCat ICodeGen = "codegen"
446strLogCat IErasure = "erasure"
447strLogCat ICoverage = "coverage"
448strLogCat IIBC = "ibc"
450codegenCats :: [LogCat]
451codegenCats = [ICodeGen]
453parserCats :: [LogCat]
459loggingCatsStr :: String
460loggingCatsStr = unlines
463 , (strLogCat ICodeGen)
464 , (strLogCat IErasure)
465 , (strLogCat ICoverage)
470data ElabShellCmd = EQED
478 | EDocStr (Either Name Const)
481data Opt = Filename String
496 | NoBuiltins -- only for the really primitive stuff!
513 | Port REPLPort -- ^ REPL TCP port
522 | PkgDocBuild String -- IdrisDoc
523 | PkgDocInstall String
533 | OutputTy OutputType
534 | Extension LanguageExt
535 | InterpretScript String
537 | TargetTriple String
540 | AddOpt Optimisation
541 | RemoveOpt Optimisation
544 | AutoWidth -- ^ Automatically adjust terminal width
545 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
546 | UseConsoleWidth ConsoleWidth
549 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
550 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
551 deriving (Show, Eq, Generic)
553data REPLPort = DontListen | ListenPort PortNumber
554 deriving (Eq, Generic, Show)
556-- Parsed declarations
558data Fixity = Infixl { prec :: Int }
559 | Infixr { prec :: Int }
560 | InfixN { prec :: Int }
561 | PrefixN { prec :: Int }
562 deriving (Eq, Generic)
564deriving instance Binary Fixity
567instance Show Fixity where
568 show (Infixl i) = "infixl " ++ show i
569 show (Infixr i) = "infixr " ++ show i
570 show (InfixN i) = "infix " ++ show i
571 show (PrefixN i) = "prefix " ++ show i
573data FixDecl = Fix Fixity String
574 deriving (Eq, Generic)
576instance Show FixDecl where
577 show (Fix f s) = show f ++ " " ++ s
580deriving instance Binary FixDecl
583instance Ord FixDecl where
584 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
587data Static = Static | Dynamic
588 deriving (Show, Eq, Data, Generic, Typeable)
590deriving instance Binary Static
593-- ^ Mark bindings with their explicitness, and laziness
594data Plicity = Imp { pargopts :: [ArgOpt]
597 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
598 , pinsource :: Bool -- ^ Explicitly written in source
600 | Exp { pargopts :: [ArgOpt]
602 , pparam :: Bool -- ^ this is a param (rather than index)
604 | Constraint { pargopts :: [ArgOpt]
607 | TacImp { pargopts :: [ArgOpt]
611 deriving (Show, Eq, Data, Generic, Typeable)
614deriving instance Binary Plicity
617is_scoped :: Plicity -> Maybe ImplicitInfo
618is_scoped (Imp _ _ _ s _) = s
622impl = Imp [] Dynamic False (Just (Impl False True False)) False
623-- Machine generated top level implicit
624impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False
627forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False
628forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False
630expl = Exp [] Dynamic False
631expl_param = Exp [] Dynamic True
633constraint = Constraint [] Static
635tacimpl t = TacImp [] Dynamic t
637data FnOpt = Inlinable -- ^ always evaluate when simplifying
638 | TotalFn | PartialFn | CoveringFn
639 | Coinductive | AssertTotal
641 -- | interface dictionary, eval only when a function
642 -- argument, and further evaluation results.
644 | OverlappingDictionary -- ^ Interface dictionary which may overlap
645 | Implicit -- ^ implicit coercion
646 | NoImplicit -- ^ do not apply implicit coercions
647 | CExport String -- ^ export, with a C name
648 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
649 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
650 | Reflection -- ^ a reflecting function, compile-time only
651 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
652 | Constructor -- ^ Data constructor type
653 | AutoHint -- ^ use in auto implicit search
654 | PEGenerated -- ^ generated by partial evaluator
655 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
656 deriving (Show, Eq, Generic)
658deriving instance Binary FnOpt
663inlinable :: FnOpts -> Bool
664inlinable = elem Inlinable
666dictionary :: FnOpts -> Bool
667dictionary = elem Dictionary
670-- | Type provider - what to provide
671data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
672 | ProvPostulate t -- ^ goal type must be Type, so only term
673 deriving (Show, Eq, Functor, Generic)
675type ProvideWhat = ProvideWhat' PTerm
677-- | Top-level declarations such as compiler directives, definitions,
678-- datatypes and interfaces.
680 -- | Fixity declaration
681 = PFix FC Fixity [String]
682 -- | Type declaration (last FC is precise name location)
683 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
684 -- | Postulate, second FC is precise name location
685 | PPostulate Bool -- external def if true
686 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
688 | PClauses FC FnOpts Name [PClause' t]
689 -- | Top level constant
691 -- | Data declaration.
692 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
694 | PParams FC [(Name, t)] [PDecl' t]
695 -- | Open block/declaration
696 | POpenInterfaces FC [Name] [PDecl' t]
697 -- | New namespace, where FC is accurate location of the namespace
699 | PNamespace String FC [PDecl' t]
701 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
703 FC -- Record name precise location
704 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
705 [(Name, Docstring (Either Err t))] -- Param Docs
706 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
707 (Maybe (Name, FC)) -- Optional constructor name and location
708 (Docstring (Either Err t)) -- Constructor doc
709 SyntaxInfo -- Constructor SyntaxInfo
711 -- | Interface: arguments are documentation, syntax info, source
712 -- location, constraints, interface name, interface name location,
713 -- parameters, method declarations, optional constructor name
714 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
715 [(Name, t)] -- constraints
716 Name -- interface name
717 FC -- accurate location of interface name
718 [(Name, FC, t)] -- parameters and precise locations
719 [(Name, Docstring (Either Err t))] -- parameter docstrings
720 [(Name, FC)] -- determining parameters and precise locations
721 [PDecl' t] -- declarations
722 (Maybe (Name, FC)) -- implementation constructor name and location
723 (Docstring (Either Err t)) -- implementation constructor docs
725 -- | Implementation declaration: arguments are documentation, syntax
726 -- info, source location, constraints, interface name, parameters, full
727 -- Implementation type, optional explicit name, and definitions
728 | PImplementation (Docstring (Either Err t)) -- Implementation docs
729 [(Name, Docstring (Either Err t))] -- Parameter docs
731 FC [(Name, t)] -- constraints
732 [Name] -- parent dictionaries to search for constraints
736 FC -- precise location of interface
738 [(Name, t)] -- Extra names in scope in the body
739 t -- full Implementation type
740 (Maybe Name) -- explicit name
742 | PDSL Name (DSL' t) -- ^ DSL declaration
743 | PSyntax FC Syntax -- ^ Syntax definition
744 | PMutual FC [PDecl' t] -- ^ Mutual block
745 | PDirective Directive -- ^ Compiler directive.
747 -- | Type provider. The first t is the type, the second is the
748 -- term. The second FC is precise highlighting location.
749 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
751 -- | Source-to-source transformation rule. If bool is True, lhs and
752 -- rhs must be convertible.
753 | PTransform FC Bool t t
755 -- | FC is decl-level, for errors, and Strings represent the
757 | PRunElabDecl FC t [String]
758 deriving (Functor, Generic)
760deriving instance Binary PDecl'
763-- | The set of source directives
764data Directive = DLib Codegen String
765 | DLink Codegen String
766 | DFlag Codegen String
767 | DInclude Codegen String
772 | DSetTotal Name -- assert totality after checking
773 | DAccess Accessibility
774 | DDefault DefaultTotality
776 | DDynamicLibs [String]
777 | DNameHint Name FC [(Name, FC)]
778 | DErrorHandlers Name FC Name FC [(Name, FC)]
779 | DLanguage LanguageExt
780 | DDeprecate Name String
781 | DFragile Name String
782 | DAutoImplicits Bool
786-- | A set of instructions for things that need to happen in IState
787-- after a term elaboration when there's been reflected elaboration.
788data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
789 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
790 | RAddImplementation Name Name
791 | RDatatypeDeclInstrs Name [PArg]
792 -- | Datatype, constructors
793 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
796-- | For elaborator state
797data EState = EState {
798 case_decls :: [(Name, PDecl)]
799 , delayed_elab :: [(Int, Elab' EState ())]
800 , new_tyDecls :: [RDeclInstructions]
801 , highlighting :: [(FC, OutputAnnotation)]
802 , auto_binds :: [Name] -- ^ names bound as auto implicits
803 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
807initEState = EState [] [] [] [] [] []
809type ElabD a = Elab' EState a
811highlightSource :: FC -> OutputAnnotation -> ElabD ()
812highlightSource fc annot =
813 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
815-- | One clause of a top-level definition. Term arguments to constructors are:
817-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
819-- 2. The list of extra 'with' patterns
821-- 3. The right-hand side
823-- 4. The where block (PDecl' t)
825data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
826 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
827 | PClauseR FC [t] t [PDecl' t]
828 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
829 deriving (Functor, Generic)
831deriving instance Binary PClause'
836 -- | Data declaration
837 PDatadecl { d_name :: Name -- ^ The name of the datatype
838 , d_name_fc :: FC -- ^ The precise location of the type constructor name
839 , d_tcon :: t -- ^ Type constructor
840 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
842 -- | "Placeholder" for data whose constructors are defined later
843 | PLaterdecl { d_name :: Name
846 } deriving (Functor, Generic)
848-- | Transform the FCs in a PData and its associated terms. The first
849-- function transforms the general-purpose FCs, and the second
850-- transforms those that are used for semantic source highlighting, so
851-- they can be treated specially.
852mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
853mapPDataFC f g (PDatadecl n nfc tycon ctors) =
854 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
855 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
856 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
857mapPDataFC f g (PLaterdecl n nfc tycon) =
858 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
860deriving instance Binary PData'
863-- Handy to get a free function for applying PTerm -> PTerm functions
864-- across a program, by deriving Functor
866type PDecl = PDecl' PTerm
867type PData = PData' PTerm
868type PClause = PClause' PTerm
870-- | Transform the FCs in a PTerm. The first function transforms the
871-- general-purpose FCs, and the second transforms those that are used
872-- for semantic source highlighting, so they can be treated specially.
873mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
874mapPDeclFC f g (PFix fc fixity ops) =
875 PFix (f fc) fixity ops
876mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
877 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
878mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
879 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
881mapPDeclFC f g (PClauses fc opts n clauses) =
882 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
883mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
884mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
885 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
886mapPDeclFC f g (PParams fc params decls) =
888 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
889 (map (mapPDeclFC f g) decls)
890mapPDeclFC f g (POpenInterfaces fc ifs decls) =
891 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
892mapPDeclFC f g (PNamespace ns fc decls) =
893 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
894mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
895 PRecord doc syn (f fc) opts n (g nfc)
896 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
898 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
899 plic, mapPTermFC f g ty, fdoc))
901 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
904mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
905 PInterface doc syn (f fc)
906 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
907 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
908 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
909 (map (mapPDeclFC f g) body)
910 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
912mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
913 PImplementation doc paramDocs syn (f fc)
914 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
915 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
916 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
917 (mapPTermFC f g implTy)
919 (map (mapPDeclFC f g) body)
920mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
921mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
923 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
924 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
925mapPDeclFC f g (PMutual fc decls) =
926 PMutual (f fc) (map (mapPDeclFC f g) decls)
927mapPDeclFC f g (PDirective d) =
930 DNameHint n nfc ns ->
931 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
932 DErrorHandlers n nfc n' nfc' ns ->
933 DErrorHandlers n (g nfc) n' (g nfc') $
934 map (\(an, anfc) -> (an, g anfc)) ns
935mapPDeclFC f g (PProvider doc syn fc nfc what n) =
936 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
937mapPDeclFC f g (PTransform fc safe l r) =
938 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
939mapPDeclFC f g (PRunElabDecl fc script ns) =
940 PRunElabDecl (f fc) (mapPTermFC f g script) ns
942-- | Get all the names declared in a declaration
943declared :: PDecl -> [Name]
944declared (PFix _ _ _) = []
945declared (PTy _ _ _ _ _ n fc t) = [n]
946declared (PPostulate _ _ _ _ _ _ n t) = [n]
947declared (PClauses _ _ n _) = [] -- not a declaration
948declared (PCAF _ n _) = [n]
949declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
950 where fstt (_, _, a, _, _, _, _) = a
951declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
952declared (PParams _ _ ds) = concatMap declared ds
953declared (POpenInterfaces _ _ ds) = concatMap declared ds
954declared (PNamespace _ _ ds) = concatMap declared ds
955declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
956declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
957declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
961declared (PDSL n _) = [n]
962declared (PSyntax _ _) = []
963declared (PMutual _ ds) = concatMap declared ds
964declared (PDirective _) = []
967-- get the names declared, not counting nested parameter blocks
968tldeclared :: PDecl -> [Name]
969tldeclared (PFix _ _ _) = []
970tldeclared (PTy _ _ _ _ _ n _ t) = [n]
971tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
972tldeclared (PClauses _ _ n _) = [] -- not a declaration
973tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
974tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
975 where fstt (_, _, a, _, _, _, _) = a
976tldeclared (PParams _ _ ds) = []
977tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
978tldeclared (PMutual _ ds) = concatMap tldeclared ds
979tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
980tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
981tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
987defined :: PDecl -> [Name]
988defined (PFix _ _ _) = []
989defined (PTy _ _ _ _ _ n _ t) = []
990defined (PPostulate _ _ _ _ _ _ n t) = []
991defined (PClauses _ _ n _) = [n] -- not a declaration
992defined (PCAF _ n _) = [n]
993defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
994 where fstt (_, _, a, _, _, _, _) = a
995defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
996defined (PParams _ _ ds) = concatMap defined ds
997defined (POpenInterfaces _ _ ds) = concatMap defined ds
998defined (PNamespace _ _ ds) = concatMap defined ds
999defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1000defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1001defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1005defined (PDSL n _) = [n]
1006defined (PSyntax _ _) = []
1007defined (PMutual _ ds) = concatMap defined ds
1008defined (PDirective _) = []
1011updateN :: [(Name, Name)] -> Name -> Name
1012updateN ns n | Just n' <- lookup n ns = n'
1015updateNs :: [(Name, Name)] -> PTerm -> PTerm
1017updateNs ns t = mapPT updateRef t
1018 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1021-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1022-- updateDNs [] t = t
1023-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1024-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1025-- where updateCNs ns (PClause n l ts r ds)
1026-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1027-- (map (fmap (updateNs ns)) ts)
1028-- (fmap (updateNs ns) r)
1029-- (map (updateDNs ns) ds)
1030-- updateDNs ns c = c
1032data PunInfo = IsType
1035 deriving (Eq, Show, Data, Typeable, Generic)
1037-- | High level language terms
1038data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1039 -- high-level language
1041 -- ^ A reference to a variable. The FC is its precise
1042 -- source location for highlighting. The list of FCs is a
1043 -- collection of additional highlighting locations.
1044 | PInferRef FC [FC] Name -- ^ A name to be defined later
1045 | PPatvar FC Name -- ^ A pattern variable
1046 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1047 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1048 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1049 | PTyped PTerm PTerm -- ^ Term with explicit type
1050 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1051 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1052 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1053 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1054 | PMatchApp FC Name -- ^ Make an application by type matching
1055 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1056 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1057 | PTrue FC PunInfo -- ^ Unit type..?
1058 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1059 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1060 -- ^ "rewrite" syntax, with optional rewriting function and
1061 -- optional result type
1062 | PPair FC [FC] PunInfo PTerm PTerm
1063 -- ^ A pair (a, b) and whether it's a product type or a
1064 -- pair (solved by elaboration). The list of FCs is its
1066 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1067 -- ^ A dependent pair (tm : a ** b) and whether it's a
1068 -- sigma type or a pair that inhabits one (solved by
1069 -- elaboration). The [FC] is its punctuation.
1070 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1071 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1072 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1073 | PType FC -- ^ 'Type' type
1074 | PUniverse FC Universe -- ^ Some universe
1075 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1076 | PConstant FC Const -- ^ Builtin types
1077 | Placeholder -- ^ Underscore
1078 | PDoBlock [PDo] -- ^ Do notation
1079 | PIdiom FC PTerm -- ^ Idiom brackets
1080 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1081 | PProof [PTactic] -- ^ Proof script
1082 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1083 | PElabError Err -- ^ Error to report on elaboration
1084 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1085 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1086 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1087 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1088 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1089 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1090 | PUnquote PTerm -- ^ ~Term
1091 | PQuoteName Name Bool FC
1092 -- ^ `{n} where the FC is the precise highlighting for
1093 -- the name in particular. If the Bool is False, then
1094 -- it's `{{n}} and the name won't be resolved.
1095 | PRunElab FC PTerm [String]
1096 -- ^ %runElab tm - New-style proof script. Args are
1097 -- location, script, enclosing namespace.
1098 | PConstSugar FC PTerm
1099 -- ^ A desugared constant. The FC is a precise source
1100 -- location that will be used to highlight it later.
1101 deriving (Eq, Data, Typeable, Generic)
1103data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1106 deriving (Eq, Data, Generic, Typeable)
1108-- | Transform the FCs in a PTerm. The first function transforms the
1109-- general-purpose FCs, and the second transforms those that are used
1110-- for semantic source highlighting, so they can be treated specially.
1111mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1112mapPTermFC f g (PQuote q) = PQuote q
1113mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1114mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1115mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1116mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1117mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1118mapPTermFC 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)
1119mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1120mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1121mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1122mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1123mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1124mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1125mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1126mapPTermFC 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)
1127mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1128mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1129mapPTermFC 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)
1130mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1131mapPTermFC 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)
1132mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1133mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1134mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1135mapPTermFC f g (PType fc) = PType (f fc)
1136mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1137mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1138mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1139mapPTermFC f g Placeholder = Placeholder
1140mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1141 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1142 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1143 mapPDoFC (DoBindP fc t1 t2 alts) =
1144 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1145 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1146 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1147mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1148mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1149mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1150mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1151mapPTermFC f g (PElabError err) = PElabError err
1152mapPTermFC f g PImpossible = PImpossible
1153mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1154mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1155mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1156mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1157mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1158mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1159mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1160mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1161mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1164dg instance Binary PTerm
1167mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1168mapPT f t = f (mpt t) where
1169 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1170 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1171 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1172 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1173 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1174 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1175 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1176 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1177 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1178 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1179 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1180 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1181 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1182 mpt (PHidden t) = PHidden (mapPT f t)
1183 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1184 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1185 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1186 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1187 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1188 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1189 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1193data PTactic' t = Intro [Name] | Intros | Focus Name
1194 | Refine Name [Bool] | Rewrite t | DoUnify
1201 | LetTac Name t | LetTacTy Name t t
1202 | Exact t | Compute | Trivial | TCImplementation
1203 | ProofSearch Bool Bool Int (Maybe Name)
1204 [Name] -- allowed local names
1206 -- ^ the bool is whether to search recursively
1209 | ProofState | ProofTerm | Undo
1210 | Try (PTactic' t) (PTactic' t)
1211 | TSeq (PTactic' t) (PTactic' t)
1212 | ApplyTactic t -- see Language.Reflection module
1216 | GoalType String (PTactic' t)
1219 | TDocStr (Either Name Const)
1222 | TFail [ErrorReportPart]
1225 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable)
1227deriving instance Binary PTactic'
1229instance Sized a => Sized (PTactic' a) where
1230 size (Intro nms) = 1 + size nms
1232 size (Focus nm) = 1 + size nm
1233 size (Refine nm bs) = 1 + size nm + length bs
1234 size (Rewrite t) = 1 + size t
1235 size (Induction t) = 1 + size t
1236 size (LetTac nm t) = 1 + size nm + size t
1237 size (Exact t) = 1 + size t
1245 size (Try l r) = 1 + size l + size r
1246 size (TSeq l r) = 1 + size l + size r
1247 size (ApplyTactic t) = 1 + size t
1248 size (Reflect t) = 1 + size t
1249 size (Fill t) = 1 + size t
1253 size (TFail ts) = 1 + size ts
1256 size (CaseTac x) = 1 + size x
1257 size (Equiv t) = 1 + size t
1258 size (Claim x y) = 1 + size x + size y
1260 size (MatchRefine x) = 1 + size x
1261 size (LetTacTy x y z) = 1 + size x + size y + size z
1262 size TCImplementation = 1
1264type PTactic = PTactic' PTerm
1266data PDo' t = DoExp FC t
1267 | DoBind FC Name FC t -- ^ second FC is precise name location
1268 | DoBindP FC t t [(t,t)]
1269 | DoLet FC Name FC t t -- ^ second FC is precise name location
1271 deriving (Eq, Functor, Data, Generic, Typeable)
1273deriving instance Binary PDo'
1276instance Sized a => Sized (PDo' a) where
1277 size (DoExp fc t) = 1 + size fc + size t
1278 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1279 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1280 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1281 size (DoLetP fc l r) = 1 + size fc + size l + size r
1283type PDo = PDo' PTerm
1285-- The priority gives a hint as to elaboration order. Best to elaborate
1286-- things early which will help give a more concrete type to other
1287-- variables, e.g. a before (interpTy a).
1289data PArg' t = PImp { priority :: Int
1290 , machine_inf :: Bool -- ^ true if the machine inferred it
1291 , argopts :: [ArgOpt]
1295 | PExp { priority :: Int
1296 , argopts :: [ArgOpt]
1300 | PConstraint { priority :: Int
1301 , argopts :: [ArgOpt]
1305 | PTacImplicit { priority :: Int
1306 , argopts :: [ArgOpt]
1311 deriving (Show, Eq, Functor, Data, Generic, Typeable)
1313data ArgOpt = AlwaysShow
1317 deriving (Show, Eq, Data, Generic, Typeable)
1319instance Sized a => Sized (PArg' a) where
1320 size (PImp p _ l nm trm) = 1 + size nm + size trm
1321 size (PExp p l nm trm) = 1 + size nm + size trm
1322 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1323 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1326deriving instance Binary PArg'
1329pimp n t mach = PImp 1 mach [] n t
1330pexp t = PExp 1 [] (sMN 0 "arg") t
1331pconst t = PConstraint 1 [] (sMN 0 "carg") t
1332ptacimp n s t = PTacImplicit 2 [] n s t
1334type PArg = PArg' PTerm
1336-- | Get the highest FC in a term, if one exists
1337highestFC :: PTerm -> Maybe FC
1338highestFC (PQuote _) = Nothing
1339highestFC (PRef fc _ _) = Just fc
1340highestFC (PInferRef fc _ _) = Just fc
1341highestFC (PPatvar fc _) = Just fc
1342highestFC (PLam fc _ _ _ _) = Just fc
1343highestFC (PPi _ _ _ _ _) = Nothing
1344highestFC (PLet fc _ _ _ _ _) = Just fc
1345highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1346highestFC (PApp fc _ _) = Just fc
1347highestFC (PAppBind fc _ _) = Just fc
1348highestFC (PMatchApp fc _) = Just fc
1349highestFC (PCase fc _ _) = Just fc
1350highestFC (PIfThenElse fc _ _ _) = Just fc
1351highestFC (PTrue fc _) = Just fc
1352highestFC (PResolveTC fc) = Just fc
1353highestFC (PRewrite fc _ _ _ _) = Just fc
1354highestFC (PPair fc _ _ _ _) = Just fc
1355highestFC (PDPair fc _ _ _ _ _) = Just fc
1356highestFC (PAs fc _ _) = Just fc
1357highestFC (PAlternative _ _ args) =
1358 case mapMaybe highestFC args of
1361highestFC (PHidden _) = Nothing
1362highestFC (PType fc) = Just fc
1363highestFC (PUniverse _ _) = Nothing
1364highestFC (PGoal fc _ _ _) = Just fc
1365highestFC (PConstant fc _) = Just fc
1366highestFC Placeholder = Nothing
1367highestFC (PDoBlock lines) =
1368 case map getDoFC lines of
1372 getDoFC (DoExp fc t) = fc
1373 getDoFC (DoBind fc nm nfc t) = fc
1374 getDoFC (DoBindP fc l r alts) = fc
1375 getDoFC (DoLet fc nm nfc l r) = fc
1376 getDoFC (DoLetP fc l r) = fc
1378highestFC (PIdiom fc _) = Just fc
1379highestFC (PMetavar fc _) = Just fc
1380highestFC (PProof _) = Nothing
1381highestFC (PTactics _) = Nothing
1382highestFC (PElabError _) = Nothing
1383highestFC PImpossible = Nothing
1384highestFC (PCoerced tm) = highestFC tm
1385highestFC (PDisamb _ opts) = highestFC opts
1386highestFC (PUnifyLog tm) = highestFC tm
1387highestFC (PNoImplicits tm) = highestFC tm
1388highestFC (PQuasiquote _ _) = Nothing
1389highestFC (PUnquote tm) = highestFC tm
1390highestFC (PQuoteName _ _ fc) = Just fc
1391highestFC (PRunElab fc _ _) = Just fc
1392highestFC (PConstSugar fc _) = Just fc
1393highestFC (PAppImpl t _) = highestFC t
1397data InterfaceInfo = CI {
1398 implementationCtorName :: Name
1399 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1400 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1401 , interface_default_super_interfaces :: [PDecl]
1402 , interface_impparams :: [Name]
1403 , interface_params :: [Name]
1404 , interface_constraints :: [PTerm]
1405 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1406 , interface_determiners :: [Int]
1407 } deriving (Show, Generic)
1409deriving instance Binary InterfaceInfo
1413data RecordInfo = RI {
1414 record_parameters :: [(Name,PTerm)]
1415 , record_constructor :: Name
1416 , record_projections :: [Name]
1417 } deriving (Show, Generic)
1419-- Type inference data
1421data TIData = TIPartial -- ^ a function with a partially defined type
1422 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1423 deriving (Show, Generic)
1425-- | Miscellaneous information about functions
1426data FnInfo = FnInfo { fn_params :: [Int] }
1427 deriving (Show, Generic)
1429deriving instance Binary FnInfo
1432data OptInfo = Optimise {
1433 inaccessible :: [(Int,Name)] -- includes names for error reporting
1434 , detaggable :: Bool
1435 } deriving (Show, Generic)
1437deriving instance Binary OptInfo
1440-- | Syntactic sugar info
1445 , dsl_var :: Maybe t
1446 , index_first :: Maybe t
1447 , index_next :: Maybe t
1448 , dsl_lambda :: Maybe t
1449 , dsl_let :: Maybe t
1451 } deriving (Show, Functor, Generic)
1453deriving instance Binary DSL'
1456type DSL = DSL' PTerm
1458data SynContext = PatternSyntax
1461 deriving (Show, Generic)
1463deriving instance Binary SynContext
1466data Syntax = Rule [SSymbol] PTerm SynContext
1467 | DeclRule [SSymbol] [PDecl]
1468 deriving (Show, Generic)
1470syntaxNames :: Syntax -> [Name]
1471syntaxNames (Rule syms _ _) = mapMaybe ename syms
1472 where ename (Keyword n) = Just n
1474syntaxNames (DeclRule syms _) = mapMaybe ename syms
1475 where ename (Keyword n) = Just n
1478syntaxSymbols :: Syntax -> [SSymbol]
1479syntaxSymbols (Rule ss _ _) = ss
1480syntaxSymbols (DeclRule ss _) = ss
1482deriving instance Binary Syntax
1485data SSymbol = Keyword Name
1490 deriving (Show, Eq, Generic)
1494deriving instance Binary SSymbol
1497newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1500emptySyntaxRules :: SyntaxRules
1501emptySyntaxRules = SyntaxRules []
1503updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1504updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1506 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1511 ruleSort (s1:ss1) (s2:ss2) =
1512 case symCompare s1 s2 of
1513 EQ -> ruleSort ss1 ss2
1516 -- Better than creating Ord implementation for SSymbol since
1517 -- in general this ordering does not really make sense.
1518 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1519 symCompare (Keyword _) _ = LT
1520 symCompare (Symbol _) (Keyword _) = GT
1521 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1522 symCompare (Symbol _) _ = LT
1523 symCompare (Binding _) (Keyword _) = GT
1524 symCompare (Binding _) (Symbol _) = GT
1525 symCompare (Binding b1) (Binding b2) = compare b1 b2
1526 symCompare (Binding _) _ = LT
1527 symCompare (Expr _) (Keyword _) = GT
1528 symCompare (Expr _) (Symbol _) = GT
1529 symCompare (Expr _) (Binding _) = GT
1530 symCompare (Expr e1) (Expr e2) = compare e1 e2
1531 symCompare (Expr _) _ = LT
1532 symCompare (SimpleExpr _) (Keyword _) = GT
1533 symCompare (SimpleExpr _) (Symbol _) = GT
1534 symCompare (SimpleExpr _) (Binding _) = GT
1535 symCompare (SimpleExpr _) (Expr _) = GT
1536 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1538initDSL = DSL (PRef f [] (sUN ">>="))
1539 (PRef f [] (sUN "<*>"))
1540 (PRef f [] (sUN "pure"))
1547 where f = fileFC "(builtin)"
1549data Using = UImplicit Name PTerm
1550 | UConstraint Name [Name]
1551 deriving (Show, Eq, Data, Generic, Typeable)
1553deriving instance Binary Using
1556data SyntaxInfo = Syn {
1558 , syn_params :: [(Name, PTerm)]
1559 , syn_namespace :: [String]
1561 , imp_methods :: [Name]
1562 -- ^ interface methods. When expanding implicits, these should be
1563 -- expanded even under binders
1564 , decoration :: Name -> Name
1566 , implicitAllowed :: Bool
1567 , constraintAllowed :: Bool
1568 , maxline :: Maybe Int
1569 , mut_nesting :: Int
1571 , syn_in_quasiquote :: Int
1572 , syn_toplevel :: Bool
1573 , withAppAllowed :: Bool
1574 } deriving (Show, Generic)
1576deriving instance Binary SyntaxInfo
1579defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1581expandNS :: SyntaxInfo -> Name -> Name
1582expandNS syn n@(NS _ _) = n
1583expandNS syn n = case syn_namespace syn of
1588-- For inferring types of things
1590bi = fileFC "builtin"
1591primfc = fileFC "(primitive)"
1593inferTy = sMN 0 "__Infer"
1594inferCon = sMN 0 "__infer"
1595inferDecl = PDatadecl inferTy primfc
1597 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1598 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1599 (PRef bi [] inferTy)), bi, [])]
1602infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1603infP = P (TCon 6 0) inferTy (TType (UVal 0))
1605getInferTerm, getInferType :: Term -> Term
1606getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1607getInferTerm (App _ (App _ _ _) tm) = tm
1608getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1610getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1611 where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))
1612 toTy (PVar t) = PVTy t
1614getInferType (App _ (App _ _ ty) _) = ty
1618-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1620primNames = [inferTy, inferCon]
1623unitCon = sUN "MkUnit"
1625falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1626 "The empty type, also known as the trivially false proposition." ++
1628 "Use `void` or `absurd` to prove anything if you have a variable " ++
1629 "of type `Void` in scope."
1632pairTy = sNS (sUN "Pair") ["Builtins"]
1633pairCon = sNS (sUN "MkPair") ["Builtins"]
1635upairTy = sNS (sUN "UPair") ["Builtins"]
1636upairCon = sNS (sUN "MkUPair") ["Builtins"]
1640eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1641 "The propositional equality type. A proof that `x` = `y`." ++
1643 "To use such a proof, pattern-match on it, and the two equal things will " ++
1644 "then need to be the _same_ pattern." ++
1646 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1647 "is possible to state equalities between values of potentially different " ++
1648 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1650 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1652eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1653 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1655 [(reflDoc, reflParamDoc,
1656 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1657 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1658 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1659 pimp (n "B") Placeholder False,
1660 pexp (PRef bi [] (n "x")),
1661 pexp (PRef bi [] (n "x"))])), bi, [])]
1663 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1664 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1665 "shown that both sides are in fact equal."
1666 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1667 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1669eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1670 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1676-- | The special name to be used in the module documentation context -
1677-- not for use in the main definition context. The namespace around it
1678-- will determine the module to which the docs adhere.
1680modDocName = sMN 0 "ModuleDocs"
1682-- Defined in builtins.idr
1683sigmaTy = sNS (sUN "DPair") ["Builtins"]
1684sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1686piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1687piBind = piBindp expl
1689piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1691piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1694-- Pretty-printing declarations and terms
1696-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1697-- could interfere with interactive editing, which calls "show".
1699instance Show PTerm where
1700 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1702instance Show PDecl where
1703 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1705instance Show PClause where
1706 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1708instance Show PData where
1709 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1711instance Pretty PTerm OutputAnnotation where
1712 pretty = prettyImp defaultPPOption
1714-- | Colourise annotations according to an Idris state. It ignores the
1715-- names in the annotation, as there's no good way to show extended
1716-- information on a terminal.
1717annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1718annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1719annotationColour ist (AnnConst c) =
1720 let theme = idris_colourTheme ist
1721 in Just $ if constIsType c
1722 then typeColour theme
1723 else dataColour theme
1724annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1725annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1726annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1727annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1728annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1729annotationColour ist (AnnName n _ _ _) =
1730 let ctxt = tt_ctxt ist
1731 theme = idris_colourTheme ist
1733 _ | isDConName n ctxt -> Just $ dataColour theme
1734 _ | isFnName n ctxt -> Just $ functionColour theme
1735 _ | isTConName n ctxt -> Just $ typeColour theme
1736 _ | isPostulateName n ist -> Just $ postulateColour theme
1737 _ | otherwise -> Nothing -- don't colourise unknown names
1738annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1739 where colour BoldText = IdrisColour Nothing True False True False
1740 colour UnderlineText = IdrisColour Nothing True True False False
1741 colour ItalicText = IdrisColour Nothing True False False True
1742annotationColour ist _ = Nothing
1745-- | Colourise annotations according to an Idris state. It ignores the
1746-- names in the annotation, as there's no good way to show extended
1747-- information on a terminal. Note that strings produced this way will
1748-- not be coloured on Windows, so the use of the colour rendering
1749-- functions in Idris.Output is to be preferred.
1750consoleDecorate :: IState -> OutputAnnotation -> String -> String
1751consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1753isPostulateName :: Name -> IState -> Bool
1754isPostulateName n ist = S.member n (idris_postulates ist)
1756-- | Pretty-print a high-level closed Idris term with no information
1757-- about precedence/associativity
1758prettyImp :: PPOption -- ^ pretty printing options
1759 -> PTerm -- ^ the term to pretty-print
1760 -> Doc OutputAnnotation
1761prettyImp impl = pprintPTerm impl [] [] []
1763-- | Serialise something to base64 using its Binary implementation.
1765-- | Do the right thing for rendering a term in an IState
1766prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1767prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1769-- | Pretty-print a high-level Idris term in some bindings context
1771pprintPTerm :: PPOption -- ^ pretty printing options
1772 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1773 -> [Name] -- ^ names to always show in pi, even if not used
1774 -> [FixDecl] -- ^ Fixity declarations
1775 -> PTerm -- ^ the term to pretty-print
1776 -> Doc OutputAnnotation
1777pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1782 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1783 prettySe d p bnd (PQuote r) =
1784 text "![" <> pretty r <> text "]"
1785 prettySe d p bnd (PPatvar fc n) = pretty n
1787 | Just str <- slist d p bnd e = depth d str
1788 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1789 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1790 prettySe d p bnd (PLam fc n nfc ty sc) =
1791 let (ns, sc') = getLamNames [n] sc in
1792 depth d . bracket p startPrec . group . align . hang 2 $
1793 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1794 prettySe (decD d) startPrec ((n, False):bnd) sc'
1796 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1797 getLamNames acc sc = (reverse acc, sc)
1799 prettyBindingsOf [] t = text ""
1800 prettyBindingsOf [n] t = prettyBindingOf n t
1801 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1802 prettyBindingsOf ns t
1803 prettySe d p bnd (PLet fc n nfc ty v sc) =
1804 depth d . bracket p startPrec . group . align $
1805 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1806 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1807 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1808 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1809 || ppopt_pinames ppo && uname n =
1810 depth d . bracket p startPrec . group $
1811 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1812 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1814 depth d . bracket p startPrec . group $
1815 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1816 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1818 uname (UN n) = case str n of
1825 Static -> text "%static" <> space
1827 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1829 depth d . bracket p startPrec $
1830 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1831 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1832 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1836 Static -> text "%static" <> space
1838 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1839 depth d . bracket p startPrec $
1840 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1841 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1842 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1843 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1844 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1845 depth d . bracket p startPrec $
1846 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1847 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1848 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1849 | basename neg == sUN "negate" =
1850 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1851 -- This case preserves the behavior of the former constructor PEq.
1852 -- It should be removed if feasible when the pretty-printing of infix
1853 -- operators in general is improved.
1854 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1855 | n == eqTy, ppopt_impl ppo =
1856 depth d . bracket p eqPrec $
1857 enclose lparen rparen eq <+>
1858 align (group (vsep (map (prettyArgS (decD d) bnd)
1861 depth d . bracket p eqPrec . align . group $
1862 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1863 where eq = annName eqTy (text "=")
1865 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1866 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1867 | UN nm <- basename f
1868 , not (ppopt_impl ppo) && null (getShowArgs args) =
1869 prettyName True (ppopt_impl ppo) bnd f
1870 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1871 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1872 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1873 | UN nm <- basename op
1875 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1876 case getShowArgs args of
1878 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1879 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1880 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1881 (l@(PExp{}) : r@(PExp{}) : rest) ->
1882 depth d . bracket p funcAppPrec $
1883 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1884 align (group (vsep (map (prettyArgS d bnd) rest)))
1885 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1886 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1887 f = getFixity (opStr op)
1889 Nothing -> funcAppPrec + 1
1890 Just (Infixl p') -> p'
1891 Just f' -> prec f' + 1
1893 Nothing -> funcAppPrec + 1
1894 Just (Infixr p') -> p'
1895 Just f' -> prec f' + 1
1896 inFix l r = align . group $
1897 (prettySe (decD d) left bnd l <+> opName False) <$>
1898 group (prettySe (decD d) right bnd r)
1899 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1900 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1901 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1902 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1903 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1904 let args = getShowArgs as
1905 fp = prettySe (decD d) (startPrec + 1) bnd f
1906 shownArgs = if ppopt_impl ppo then as else args
1908 depth d . bracket p funcAppPrec . group $
1911 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1912 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1913 prettySe d p bnd (PCase _ scr cases) =
1914 bracket p funcAppPrec $
1915 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1916 depth d (indent 2 (vsep (map ppcase cases)))
1918 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1919 ([(n, False) | n <- vars l] ++ bnd)
1920 in nest nestingSize $
1921 prettyCase l <+> text "=>" <+> prettyCase r
1922 -- Warning: this is a bit of a hack. At this stage, we don't have the
1923 -- global context, so we can't determine which names are constructors,
1924 -- which are types, and which are pattern variables on the LHS of the
1925 -- case pattern. We use the heuristic that names without a namespace
1926 -- are patvars, because right now case blocks in PTerms are always
1927 -- delaborated from TT before being sent to the pretty-printer. If they
1928 -- start getting printed directly, THIS WILL BREAK.
1929 -- Potential solution: add a list of known patvars to the cases in
1930 -- PCase, and have the delaborator fill it out, kind of like the pun
1931 -- disambiguation on PDPair.
1932 vars tm = filter noNS (allNamesIn tm)
1933 noNS (NS _ _) = False
1936 prettySe d p bnd (PIfThenElse _ c t f) =
1937 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1938 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1939 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1940 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1942 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1943 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1944 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1945 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1946 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1947 prettySe d p bnd (PRewrite _ by l r _) =
1948 depth d . bracket p startPrec $
1949 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1952 Just fn -> text "using" <+>
1953 prettyName True (ppopt_impl ppo) bnd fn) <+>
1954 text "in" <+> prettySe (decD d) startPrec bnd r
1955 prettySe d p bnd (PTyped l r) =
1956 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1957 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1958 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1959 align . group . vsep . punctuate (ann comma) $
1960 map (prettySe (decD d) startPrec bnd) elts
1961 where ann = case pun of
1963 IsType -> annName pairTy
1964 IsTerm -> annName pairCon
1965 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1966 | Just elts <- dPairElts dpair
1967 = depth d . enclose (annotated lparen) (annotated rparen) .
1968 align . group . vsep . punctuate (space <> annotated (text "**")) $
1974 annotated (text "**") <+>
1975 prettySe (decD d) startPrec (addBinding bnd) r <>
1977 where annotated = case pun of
1978 IsType -> annName sigmaTy
1979 IsTerm -> annName sigmaCon
1982 (left, addBinding) = case (l, pun) of
1983 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1984 _ -> (prettySe (decD d) startPrec bnd l, id)
1987 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1988 ppElts ((PRef _ _ n, t):rs) bs
1990 = (bindingOf n False <+> colon <+>
1991 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1992 ppElts ((l, t):rs) bs
1993 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1994 prettySe d p bnd (PAlternative ns a as) =
1995 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1998 foldr ((\ l r -> l <+> text "," <+> r) .
1999 depth d . prettySe (decD d) startPrec bnd)
2001 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2002 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2003 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2004 -- XXX: add pretty for tactics
2005 prettySe d p bnd (PProof ts) =
2006 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2007 prettySe d p bnd (PTactics ts) =
2008 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2009 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2010 prettySe d p bnd PImpossible = kwd "impossible"
2011 prettySe d p bnd Placeholder = text "_"
2012 prettySe d p bnd (PDoBlock dos) =
2013 bracket p startPrec $
2014 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2015 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2016 ppdo bnd (DoBind _ bn _ tm : dos) =
2017 (prettyBindingOf bn False <+> text "<-" <+>
2018 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2019 ppdo ((bn, False):bnd) dos
2020 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2021 text "no pretty printer for pattern-matching do binding" :
2023 ppdo bnd (DoLet _ ln _ ty v : dos) =
2024 (kwd "let" <+> prettyBindingOf ln False <+>
2025 (if ty /= Placeholder
2026 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2028 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2029 ppdo ((ln, False):bnd) dos
2030 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2031 text "no pretty printer for pattern-matching do binding" :
2034 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2035 prettySe d p bnd (PElabError s) = pretty s
2036 -- Quasiquote pprinting ignores bound vars
2037 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2038 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2039 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2040 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2041 where start = if res then "`{" else "`{{"
2042 end = if res then "}" else "}}"
2043 prettySe d p bnd (PRunElab _ tm _) =
2044 bracket p funcAppPrec . group . align . hang 2 $
2046 prettySe (decD d) funcAppPrec bnd tm
2047 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2048 prettySe d p bnd _ = text "missing pretty-printer for term"
2050 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2051 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2052 where display (UN n) = T.unpack n
2053 display (MN _ n) = T.unpack n
2054 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2055 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2058 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2059 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2060 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2061 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2063 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2064 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2065 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2066 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2068 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2069 annName n = annotate (AnnName n Nothing Nothing Nothing)
2071 opStr :: Name -> String
2072 opStr (NS n _) = opStr n
2073 opStr (UN n) = T.unpack n
2075 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2076 slist' (Just d) _ _ _ | d <= 0 = Nothing
2078 | containsHole e = Nothing
2079 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2080 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2081 slist' d p bnd (PRef _ _ nil)
2082 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2083 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2084 | nsroot cons == sUN "::",
2085 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2087 Just tl' <- slist' (decD d) p bnd tl
2088 = Just (prettySe d startPrec bnd hd : tl')
2090 isImp (PImp {}) = True
2092 slist' _ _ _ tm = Nothing
2094 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2096 [] -> annotate (AnnData "" "") $ text "[]"
2097 [x] -> enclose left right . group $ x
2098 xs -> enclose left right .
2099 align . group . vsep .
2100 punctuate comma $ xs
2101 where left = (annotate (AnnData "" "") (text "["))
2102 right = (annotate (AnnData "" "") (text "]"))
2103 comma = (annotate (AnnData "" "") (text ","))
2104 slist _ _ _ _ = Nothing
2106 pairElts :: PTerm -> Maybe [PTerm]
2107 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2108 | otherwise = Just [x, y]
2109 pairElts _ = Nothing
2111 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2112 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2113 | otherwise = Just [(l, t), (Placeholder, r)]
2114 dPairElts _ = Nothing
2116 natns = "Prelude.Nat."
2118 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2120 | ppopt_desugarnats ppo = Nothing
2121 | otherwise = snat' d p e
2123 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2124 snat' (Just x) _ _ | x <= 0 = Nothing
2125 snat' d p (PRef _ _ z)
2126 | show z == (natns++"Z") || show z == "Z" = Just 0
2127 snat' d p (PApp _ s [PExp {getTm=n}])
2128 | show s == (natns++"S") || show s == "S",
2129 Just n' <- snat' (decD d) p n
2131 snat' _ _ _ = Nothing
2133 bracket outer inner doc
2134 | outer > inner = lparen <> doc <> rparen
2137 ellipsis = text "..."
2140 depth (Just d) = if d <= 0 then const ellipsis else id
2142 decD = fmap (\x -> x - 1)
2144 kwd = annotate AnnKeyword . text
2146 fixities :: M.Map String Fixity
2147 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2149 getFixity :: String -> Maybe Fixity
2150 getFixity = flip M.lookup fixities
2152-- | Strip away namespace information
2153basename :: Name -> Name
2154basename (NS n _) = basename n
2157-- | Determine whether a name was the one inserted for a hole or guess
2158-- by the delaborator
2159isHoleName :: Name -> Bool
2160isHoleName (UN n) = n == T.pack "[__]"
2163-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2164containsHole :: PTerm -> Bool
2165containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2167-- | Pretty-printer helper for names that attaches the correct annotations
2168prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2169 -> Bool -- ^ whether to show namespaces
2170 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2171 -> Name -- ^ the name to pprint
2172 -> Doc OutputAnnotation
2173prettyName infixParen showNS bnd n
2174 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2175 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2176 | (UN n') <- n, T.unpack n' == "_" = text "_"
2177 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2178 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2179 where fullName = text nameSpace <> parenthesise (text (baseName n))
2180 baseName (UN n) = T.unpack n
2181 baseName (NS n ns) = baseName n
2182 baseName (MN i s) = T.unpack s
2183 baseName other = show other
2184 nameSpace = case n of
2185 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2187 isInfix = case baseName n of
2189 (c : _) -> not (isAlpha c)
2190 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2193showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2194showCImp ppo (PClause _ n l ws r w)
2195 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2196 <+> text "where" <+> text (show w)
2199 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2200showCImp ppo (PWith _ n l ws r pn w)
2201 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2202 <+> braces (text (show w))
2205 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2208showDImp :: PPOption -> PData -> Doc OutputAnnotation
2209showDImp ppo (PDatadecl n nfc ty cons)
2210 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2211 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2213showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2214showDecls o ds = vsep (map (showDeclImp o) ds)
2216showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2217showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2218showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2219 indent 2 (vsep (map (showCImp o) cs))
2220showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2221showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2222showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2223showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2224showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2225showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2226 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2227showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2228 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2229showDeclImp _ _ = text "..."
2230-- showDeclImp (PImport o) = "import " ++ o
2232getImps :: [PArg] -> [(Name, PTerm)]
2234getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2235getImps (_ : xs) = getImps xs
2237getExps :: [PArg] -> [PTerm]
2239getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2240getExps (_ : xs) = getExps xs
2242getShowArgs :: [PArg] -> [PArg]
2244getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2245getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2246 | PImp _ _ _ _ tm <- e
2247 , containsHole tm = e : getShowArgs xs
2248getShowArgs (_ : xs) = getShowArgs xs
2250getConsts :: [PArg] -> [PTerm]
2252getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2253getConsts (_ : xs) = getConsts xs
2255getAll :: [PArg] -> [PTerm]
2260showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2261 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2262 -> PPOption -- ^ pretty printing options
2263 -> Bool -- ^ whether to colourise
2264 -> Name -- ^ the term to show
2266showName ist bnd ppo colour n = case ist of
2267 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2268 Nothing -> showbasic n
2269 where name = if ppopt_impl ppo then show n else showbasic n
2270 showbasic n@(UN _) = showCG n
2271 showbasic (MN i s) = str s
2272 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2273 showbasic (SN s) = show s
2275 colourise n t = let ctxt' = fmap tt_ctxt ist in
2278 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2279 else colouriseBound t name
2280 | isDConName n ctxt -> colouriseData t name
2281 | isFnName n ctxt -> colouriseFun t name
2282 | isTConName n ctxt -> colouriseType t name
2283 -- The assumption is that if a name is not bound and does not exist in the
2284 -- global context, then we're somewhere in which implicit info has been lost
2285 -- (like error messages). Thus, unknown vars are colourised as implicits.
2286 | otherwise -> colouriseImplicit t name
2288showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2289 -> PTerm -- ^ the term to show
2291showTm ist = displayDecorated (consoleDecorate ist) .
2292 renderPretty 0.8 100000 .
2293 prettyImp (ppOptionIst ist)
2295-- | Show a term with implicits, no colours
2296showTmImpls :: PTerm -> String
2297showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2299-- | Show a term with specific options
2300showTmOpts :: PPOption -> PTerm -> String
2301showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2304instance Sized PTerm where
2305 size (PQuote rawTerm) = size rawTerm
2306 size (PRef fc _ name) = size name
2307 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2308 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2309 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2310 size (PTyped trm ty) = 1 + size trm + size ty
2311 size (PApp fc name args) = 1 + size args
2312 size (PAppBind fc name args) = 1 + size args
2313 size (PCase fc trm bdy) = 1 + size trm + size bdy
2314 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2315 size (PTrue fc _) = 1
2316 size (PResolveTC fc) = 1
2317 size (PRewrite fc by left right _) = 1 + size left + size right
2318 size (PPair fc _ _ left right) = 1 + size left + size right
2319 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2320 size (PAlternative _ a alts) = 1 + size alts
2321 size (PHidden hidden) = size hidden
2322 size (PUnifyLog tm) = size tm
2323 size (PDisamb _ tm) = size tm
2324 size (PNoImplicits tm) = size tm
2326 size (PUniverse _ _) = 1
2327 size (PConstant fc const) = 1 + size fc + size const
2328 size Placeholder = 1
2329 size (PDoBlock dos) = 1 + size dos
2330 size (PIdiom fc term) = 1 + size term
2331 size (PMetavar _ name) = 1
2332 size (PProof tactics) = size tactics
2333 size (PElabError err) = size err
2334 size PImpossible = 1
2337getPArity :: PTerm -> Int
2338getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2341-- Return all names, free or globally bound, in the given term.
2343allNamesIn :: PTerm -> [Name]
2344allNamesIn tm = nub $ ni 0 [] tm
2345 where -- TODO THINK added niTacImp, but is it right?
2346 ni 0 env (PRef _ _ n)
2347 | not (n `elem` env) = [n]
2348 ni 0 env (PPatvar _ n) = [n]
2349 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2350 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2351 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2352 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2353 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2354 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2355 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2356 ni 0 env (PHidden tm) = ni 0 env tm
2357 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2358 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2359 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2360 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2361 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2362 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2363 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2364 ni 0 env (PUnifyLog tm) = ni 0 env tm
2365 ni 0 env (PDisamb _ tm) = ni 0 env tm
2366 ni 0 env (PNoImplicits tm) = ni 0 env tm
2368 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2369 ni i env (PUnquote tm) = ni (i - 1) env tm
2370 ni i env tm = concatMap (ni i env) (children tm)
2372 niTacImp i env (TacImp _ _ scr) = ni i env scr
2376-- Return all names defined in binders in the given term
2377boundNamesIn :: PTerm -> [Name]
2378boundNamesIn tm = S.toList (ni 0 S.empty tm)
2379 where -- TODO THINK Added niTacImp, but is it right?
2380 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2381 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2382 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2383 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2384 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2385 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2386 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2387 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2388 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2389 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2390 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2391 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2392 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2393 ni 0 set (PAlternative ns a as) = niTms 0 set as
2394 ni 0 set (PHidden tm) = ni 0 set tm
2395 ni 0 set (PUnifyLog tm) = ni 0 set tm
2396 ni 0 set (PDisamb _ tm) = ni 0 set tm
2397 ni 0 set (PNoImplicits tm) = ni 0 set tm
2399 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2400 ni i set (PUnquote tm) = ni (i - 1) set tm
2402 ni i set tm = foldr (S.union . ni i set) set (children tm)
2404 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2405 niTms i set [] = set
2406 niTms i set (x : xs) = niTms i (ni i set x) xs
2408 niTacImp i set (TacImp _ _ scr) = ni i set scr
2409 niTacImp i set _ = set
2411-- Return names which are valid implicits in the given term (type).
2412implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2413implicitNamesIn uvars ist tm
2414 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2417 addImp n = do (imps, fns) <- get
2419 addFn n = do (imps, fns) <- get
2423 notCAF (PExp _ _ _ _ : _) = True
2424 notCAF (_ : xs) = notCAF xs
2426 notHidden (n, _) = case getAccessibility n of
2432 = case lookupDefAccExact n False (tt_ctxt ist) of
2436 ni 0 env (PRef _ _ n@(NS _ _))
2437 | not (n `elem` env)
2438 -- Never implicitly bind if there's a namespace
2440 ni 0 env (PRef _ _ n)
2441 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2442 ni 0 env (PApp _ f@(PRef _ _ n) as)
2443 | n `elem` uvars = do ni 0 env f
2444 mapM_ (ni 0 env . getTm) as
2445 | otherwise = do case lookupTy n (tt_ctxt ist) of
2448 mapM_ (ni 0 env . getTm) as
2449 ni 0 env (PApp _ f as) = do ni 0 env f
2450 mapM_ (ni 0 env . getTm) as
2451 ni 0 env (PAppBind _ f as) = do ni 0 env f
2452 mapM_ (ni 0 env . getTm) as
2453 ni 0 env (PCase _ c os) = do ni 0 env c
2454 -- names in 'os', not counting the names bound in the cases
2455 mapM_ (ni 0 env . snd) os
2458 mapM_ (ni 0 env . fst) os
2460 put (nub imps \\ nub impsfst, fns)
2461 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2462 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2463 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2464 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2465 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2466 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2467 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2468 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2471 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2472 ni 0 env (PHidden tm) = ni 0 env tm
2473 ni 0 env (PUnifyLog tm) = ni 0 env tm
2474 ni 0 env (PDisamb _ tm) = ni 0 env tm
2475 ni 0 env (PNoImplicits tm) = ni 0 env tm
2477 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2478 maybe (return ()) (ni i env) ty
2479 ni i env (PUnquote tm) = ni (i - 1) env tm
2481 ni i env tm = mapM_ (ni i env) (children tm)
2483-- Return names which are free in the given term.
2484namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2485namesIn uvars ist tm = nub $ ni 0 [] tm
2487 ni 0 env (PRef _ _ n)
2488 | not (n `elem` env)
2489 = case lookupTy n (tt_ctxt ist) of
2491 _ -> [n | n `elem` (map fst uvars)]
2492 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2493 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2494 ni 0 env (PCase _ c os) = ni 0 env c ++
2495 -- names in 'os', not counting the names bound in the cases
2496 (nub (concatMap (ni 0 env . snd) os)
2497 \\ nub (concatMap (ni 0 env . fst) os))
2498 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2499 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2500 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2501 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2502 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2503 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2504 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2505 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2506 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2507 ni 0 env (PHidden tm) = ni 0 env tm
2508 ni 0 env (PUnifyLog tm) = ni 0 env tm
2509 ni 0 env (PDisamb _ tm) = ni 0 env tm
2510 ni 0 env (PNoImplicits tm) = ni 0 env tm
2512 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2513 ni i env (PUnquote tm) = ni (i - 1) env tm
2515 ni i env tm = concatMap (ni i env) (children tm)
2517 niTacImp i env (TacImp _ _ scr) = ni i env scr
2520-- Return which of the given names are used in the given term.
2522usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2523usedNamesIn vars ist tm = nub $ ni 0 [] tm
2524 where -- TODO THINK added niTacImp, but is it right?
2525 ni 0 env (PRef _ _ n)
2526 | n `elem` vars && not (n `elem` env)
2527 = case lookupDefExact n (tt_ctxt ist) of
2530 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2531 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2532 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2533 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2534 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2535 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2536 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2537 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2538 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2539 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2540 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2541 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2542 ni 0 env (PHidden tm) = ni 0 env tm
2543 ni 0 env (PUnifyLog tm) = ni 0 env tm
2544 ni 0 env (PDisamb _ tm) = ni 0 env tm
2545 ni 0 env (PNoImplicits tm) = ni 0 env tm
2547 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2548 ni i env (PUnquote tm) = ni (i - 1) env tm
2550 ni i env tm = concatMap (ni i env) (children tm)
2552 niTacImp i env (TacImp _ _ scr) = ni i env scr
2555-- Return the list of inaccessible (= dotted) positions for a name.
2556getErasureInfo :: IState -> Name -> [Int]
2557getErasureInfo ist n =
2558 case lookupCtxtExact n (idris_optimisation ist) of
2559 Just (Optimise inacc detagg) -> 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