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 depth d . bracket p startPrec . group . align . hang 2 $
1792 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1793 prettySe (decD d) startPrec ((n, False):bnd) sc
1794 prettySe d p bnd (PLet fc n nfc ty v sc) =
1795 depth d . bracket p startPrec . group . align $
1796 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1797 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1798 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1799 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1800 || ppopt_pinames ppo && uname n =
1801 depth d . bracket p startPrec . group $
1802 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1803 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1805 depth d . bracket p startPrec . group $
1806 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1807 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1809 uname (UN n) = case str n of
1816 Static -> text "%static" <> space
1818 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1820 depth d . bracket p startPrec $
1821 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1822 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1823 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1827 Static -> text "%static" <> space
1829 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1830 depth d . bracket p startPrec $
1831 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1832 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1833 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1834 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1835 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1836 depth d . bracket p startPrec $
1837 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1838 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1839 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1840 | basename neg == sUN "negate" =
1841 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1842 -- This case preserves the behavior of the former constructor PEq.
1843 -- It should be removed if feasible when the pretty-printing of infix
1844 -- operators in general is improved.
1845 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1846 | n == eqTy, ppopt_impl ppo =
1847 depth d . bracket p eqPrec $
1848 enclose lparen rparen eq <+>
1849 align (group (vsep (map (prettyArgS (decD d) bnd)
1852 depth d . bracket p eqPrec . align . group $
1853 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1854 where eq = annName eqTy (text "=")
1856 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1857 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1858 | UN nm <- basename f
1859 , not (ppopt_impl ppo) && null (getShowArgs args) =
1860 prettyName True (ppopt_impl ppo) bnd f
1861 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1862 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1863 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1864 | UN nm <- basename op
1866 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1867 case getShowArgs args of
1869 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1870 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1871 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1872 (l@(PExp{}) : r@(PExp{}) : rest) ->
1873 depth d . bracket p funcAppPrec $
1874 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1875 align (group (vsep (map (prettyArgS d bnd) rest)))
1876 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1877 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1878 f = getFixity (opStr op)
1880 Nothing -> funcAppPrec + 1
1881 Just (Infixl p') -> p'
1882 Just f' -> prec f' + 1
1884 Nothing -> funcAppPrec + 1
1885 Just (Infixr p') -> p'
1886 Just f' -> prec f' + 1
1887 inFix l r = align . group $
1888 (prettySe (decD d) left bnd l <+> opName False) <$>
1889 group (prettySe (decD d) right bnd r)
1890 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1891 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1892 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1893 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1894 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1895 let args = getShowArgs as
1896 fp = prettySe (decD d) (startPrec + 1) bnd f
1897 shownArgs = if ppopt_impl ppo then as else args
1899 depth d . bracket p funcAppPrec . group $
1902 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1903 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1904 prettySe d p bnd (PCase _ scr cases) =
1905 bracket p funcAppPrec $
1906 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1907 depth d (indent 2 (vsep (map ppcase cases)))
1909 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1910 ([(n, False) | n <- vars l] ++ bnd)
1911 in nest nestingSize $
1912 prettyCase l <+> text "=>" <+> prettyCase r
1913 -- Warning: this is a bit of a hack. At this stage, we don't have the
1914 -- global context, so we can't determine which names are constructors,
1915 -- which are types, and which are pattern variables on the LHS of the
1916 -- case pattern. We use the heuristic that names without a namespace
1917 -- are patvars, because right now case blocks in PTerms are always
1918 -- delaborated from TT before being sent to the pretty-printer. If they
1919 -- start getting printed directly, THIS WILL BREAK.
1920 -- Potential solution: add a list of known patvars to the cases in
1921 -- PCase, and have the delaborator fill it out, kind of like the pun
1922 -- disambiguation on PDPair.
1923 vars tm = filter noNS (allNamesIn tm)
1924 noNS (NS _ _) = False
1927 prettySe d p bnd (PIfThenElse _ c t f) =
1928 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1929 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1930 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1931 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1933 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1934 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1935 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1936 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1937 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1938 prettySe d p bnd (PRewrite _ by l r _) =
1939 depth d . bracket p startPrec $
1940 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1943 Just fn -> text "using" <+>
1944 prettyName True (ppopt_impl ppo) bnd fn) <+>
1945 text "in" <+> prettySe (decD d) startPrec bnd r
1946 prettySe d p bnd (PTyped l r) =
1947 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1948 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1949 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1950 align . group . vsep . punctuate (ann comma) $
1951 map (prettySe (decD d) startPrec bnd) elts
1952 where ann = case pun of
1954 IsType -> annName pairTy
1955 IsTerm -> annName pairCon
1956 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1957 | Just elts <- dPairElts dpair
1958 = depth d . enclose (annotated lparen) (annotated rparen) .
1959 align . group . vsep . punctuate (space <> annotated (text "**")) $
1965 annotated (text "**") <+>
1966 prettySe (decD d) startPrec (addBinding bnd) r <>
1968 where annotated = case pun of
1969 IsType -> annName sigmaTy
1970 IsTerm -> annName sigmaCon
1973 (left, addBinding) = case (l, pun) of
1974 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1975 _ -> (prettySe (decD d) startPrec bnd l, id)
1978 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1979 ppElts ((PRef _ _ n, t):rs) bs
1981 = (bindingOf n False <+> colon <+>
1982 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1983 ppElts ((l, t):rs) bs
1984 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1985 prettySe d p bnd (PAlternative ns a as) =
1986 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1989 foldr ((\ l r -> l <+> text "," <+> r) .
1990 depth d . prettySe (decD d) startPrec bnd)
1992 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1993 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1994 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1995 -- XXX: add pretty for tactics
1996 prettySe d p bnd (PProof ts) =
1997 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1998 prettySe d p bnd (PTactics ts) =
1999 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2000 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2001 prettySe d p bnd PImpossible = kwd "impossible"
2002 prettySe d p bnd Placeholder = text "_"
2003 prettySe d p bnd (PDoBlock dos) =
2004 bracket p startPrec $
2005 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2006 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2007 ppdo bnd (DoBind _ bn _ tm : dos) =
2008 (prettyBindingOf bn False <+> text "<-" <+>
2009 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2010 ppdo ((bn, False):bnd) dos
2011 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2012 text "no pretty printer for pattern-matching do binding" :
2014 ppdo bnd (DoLet _ ln _ ty v : dos) =
2015 (kwd "let" <+> prettyBindingOf ln False <+>
2016 (if ty /= Placeholder
2017 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2019 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2020 ppdo ((ln, False):bnd) dos
2021 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2022 text "no pretty printer for pattern-matching do binding" :
2025 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2026 prettySe d p bnd (PElabError s) = pretty s
2027 -- Quasiquote pprinting ignores bound vars
2028 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2029 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2030 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2031 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2032 where start = if res then "`{" else "`{{"
2033 end = if res then "}" else "}}"
2034 prettySe d p bnd (PRunElab _ tm _) =
2035 bracket p funcAppPrec . group . align . hang 2 $
2037 prettySe (decD d) funcAppPrec bnd tm
2038 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2039 prettySe d p bnd _ = text "missing pretty-printer for term"
2041 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2042 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2043 where display (UN n) = T.unpack n
2044 display (MN _ n) = T.unpack n
2045 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2046 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2049 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2050 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2051 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2052 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2054 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2055 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2056 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2057 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2059 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2060 annName n = annotate (AnnName n Nothing Nothing Nothing)
2062 opStr :: Name -> String
2063 opStr (NS n _) = opStr n
2064 opStr (UN n) = T.unpack n
2066 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2067 slist' (Just d) _ _ _ | d <= 0 = Nothing
2069 | containsHole e = Nothing
2070 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2071 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2072 slist' d p bnd (PRef _ _ nil)
2073 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2074 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2075 | nsroot cons == sUN "::",
2076 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2078 Just tl' <- slist' (decD d) p bnd tl
2079 = Just (prettySe d startPrec bnd hd : tl')
2081 isImp (PImp {}) = True
2083 slist' _ _ _ tm = Nothing
2085 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2087 [] -> annotate (AnnData "" "") $ text "[]"
2088 [x] -> enclose left right . group $ x
2089 xs -> enclose left right .
2090 align . group . vsep .
2091 punctuate comma $ xs
2092 where left = (annotate (AnnData "" "") (text "["))
2093 right = (annotate (AnnData "" "") (text "]"))
2094 comma = (annotate (AnnData "" "") (text ","))
2095 slist _ _ _ _ = Nothing
2097 pairElts :: PTerm -> Maybe [PTerm]
2098 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2099 | otherwise = Just [x, y]
2100 pairElts _ = Nothing
2102 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2103 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2104 | otherwise = Just [(l, t), (Placeholder, r)]
2105 dPairElts _ = Nothing
2107 natns = "Prelude.Nat."
2109 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2111 | ppopt_desugarnats ppo = Nothing
2112 | otherwise = snat' d p e
2114 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2115 snat' (Just x) _ _ | x <= 0 = Nothing
2116 snat' d p (PRef _ _ z)
2117 | show z == (natns++"Z") || show z == "Z" = Just 0
2118 snat' d p (PApp _ s [PExp {getTm=n}])
2119 | show s == (natns++"S") || show s == "S",
2120 Just n' <- snat' (decD d) p n
2122 snat' _ _ _ = Nothing
2124 bracket outer inner doc
2125 | outer > inner = lparen <> doc <> rparen
2128 ellipsis = text "..."
2131 depth (Just d) = if d <= 0 then const ellipsis else id
2133 decD = fmap (\x -> x - 1)
2135 kwd = annotate AnnKeyword . text
2137 fixities :: M.Map String Fixity
2138 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2140 getFixity :: String -> Maybe Fixity
2141 getFixity = flip M.lookup fixities
2143-- | Strip away namespace information
2144basename :: Name -> Name
2145basename (NS n _) = basename n
2148-- | Determine whether a name was the one inserted for a hole or guess
2149-- by the delaborator
2150isHoleName :: Name -> Bool
2151isHoleName (UN n) = n == T.pack "[__]"
2154-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2155containsHole :: PTerm -> Bool
2156containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2158-- | Pretty-printer helper for names that attaches the correct annotations
2159prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2160 -> Bool -- ^ whether to show namespaces
2161 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2162 -> Name -- ^ the name to pprint
2163 -> Doc OutputAnnotation
2164prettyName infixParen showNS bnd n
2165 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2166 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2167 | (UN n') <- n, T.unpack n' == "_" = text "_"
2168 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2169 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2170 where fullName = text nameSpace <> parenthesise (text (baseName n))
2171 baseName (UN n) = T.unpack n
2172 baseName (NS n ns) = baseName n
2173 baseName (MN i s) = T.unpack s
2174 baseName other = show other
2175 nameSpace = case n of
2176 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2178 isInfix = case baseName n of
2180 (c : _) -> not (isAlpha c)
2181 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2184showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2185showCImp ppo (PClause _ n l ws r w)
2186 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2187 <+> text "where" <+> text (show w)
2190 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2191showCImp ppo (PWith _ n l ws r pn w)
2192 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2193 <+> braces (text (show w))
2196 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2199showDImp :: PPOption -> PData -> Doc OutputAnnotation
2200showDImp ppo (PDatadecl n nfc ty cons)
2201 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2202 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2204showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2205showDecls o ds = vsep (map (showDeclImp o) ds)
2207showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2208showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2209showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2210 indent 2 (vsep (map (showCImp o) cs))
2211showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2212showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2213showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2214showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2215showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2216showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2217 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2218showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2219 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2220showDeclImp _ _ = text "..."
2221-- showDeclImp (PImport o) = "import " ++ o
2223getImps :: [PArg] -> [(Name, PTerm)]
2225getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2226getImps (_ : xs) = getImps xs
2228getExps :: [PArg] -> [PTerm]
2230getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2231getExps (_ : xs) = getExps xs
2233getShowArgs :: [PArg] -> [PArg]
2235getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2236getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2237 | PImp _ _ _ _ tm <- e
2238 , containsHole tm = e : getShowArgs xs
2239getShowArgs (_ : xs) = getShowArgs xs
2241getConsts :: [PArg] -> [PTerm]
2243getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2244getConsts (_ : xs) = getConsts xs
2246getAll :: [PArg] -> [PTerm]
2251showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2252 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2253 -> PPOption -- ^ pretty printing options
2254 -> Bool -- ^ whether to colourise
2255 -> Name -- ^ the term to show
2257showName ist bnd ppo colour n = case ist of
2258 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2259 Nothing -> showbasic n
2260 where name = if ppopt_impl ppo then show n else showbasic n
2261 showbasic n@(UN _) = showCG n
2262 showbasic (MN i s) = str s
2263 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2264 showbasic (SN s) = show s
2266 colourise n t = let ctxt' = fmap tt_ctxt ist in
2269 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2270 else colouriseBound t name
2271 | isDConName n ctxt -> colouriseData t name
2272 | isFnName n ctxt -> colouriseFun t name
2273 | isTConName n ctxt -> colouriseType t name
2274 -- The assumption is that if a name is not bound and does not exist in the
2275 -- global context, then we're somewhere in which implicit info has been lost
2276 -- (like error messages). Thus, unknown vars are colourised as implicits.
2277 | otherwise -> colouriseImplicit t name
2279showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2280 -> PTerm -- ^ the term to show
2282showTm ist = displayDecorated (consoleDecorate ist) .
2283 renderPretty 0.8 100000 .
2284 prettyImp (ppOptionIst ist)
2286-- | Show a term with implicits, no colours
2287showTmImpls :: PTerm -> String
2288showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2290-- | Show a term with specific options
2291showTmOpts :: PPOption -> PTerm -> String
2292showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2295instance Sized PTerm where
2296 size (PQuote rawTerm) = size rawTerm
2297 size (PRef fc _ name) = size name
2298 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2299 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2300 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2301 size (PTyped trm ty) = 1 + size trm + size ty
2302 size (PApp fc name args) = 1 + size args
2303 size (PAppBind fc name args) = 1 + size args
2304 size (PCase fc trm bdy) = 1 + size trm + size bdy
2305 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2306 size (PTrue fc _) = 1
2307 size (PResolveTC fc) = 1
2308 size (PRewrite fc by left right _) = 1 + size left + size right
2309 size (PPair fc _ _ left right) = 1 + size left + size right
2310 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2311 size (PAlternative _ a alts) = 1 + size alts
2312 size (PHidden hidden) = size hidden
2313 size (PUnifyLog tm) = size tm
2314 size (PDisamb _ tm) = size tm
2315 size (PNoImplicits tm) = size tm
2317 size (PUniverse _ _) = 1
2318 size (PConstant fc const) = 1 + size fc + size const
2319 size Placeholder = 1
2320 size (PDoBlock dos) = 1 + size dos
2321 size (PIdiom fc term) = 1 + size term
2322 size (PMetavar _ name) = 1
2323 size (PProof tactics) = size tactics
2324 size (PElabError err) = size err
2325 size PImpossible = 1
2328getPArity :: PTerm -> Int
2329getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2332-- Return all names, free or globally bound, in the given term.
2334allNamesIn :: PTerm -> [Name]
2335allNamesIn tm = nub $ ni 0 [] tm
2336 where -- TODO THINK added niTacImp, but is it right?
2337 ni 0 env (PRef _ _ n)
2338 | not (n `elem` env) = [n]
2339 ni 0 env (PPatvar _ n) = [n]
2340 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2341 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2342 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2343 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2344 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2345 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2346 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2347 ni 0 env (PHidden tm) = ni 0 env tm
2348 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2349 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2350 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2351 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2352 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2353 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2354 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2355 ni 0 env (PUnifyLog tm) = ni 0 env tm
2356 ni 0 env (PDisamb _ tm) = ni 0 env tm
2357 ni 0 env (PNoImplicits tm) = ni 0 env tm
2359 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2360 ni i env (PUnquote tm) = ni (i - 1) env tm
2361 ni i env tm = concatMap (ni i env) (children tm)
2363 niTacImp i env (TacImp _ _ scr) = ni i env scr
2367-- Return all names defined in binders in the given term
2368boundNamesIn :: PTerm -> [Name]
2369boundNamesIn tm = S.toList (ni 0 S.empty tm)
2370 where -- TODO THINK Added niTacImp, but is it right?
2371 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2372 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2373 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2374 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2375 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2376 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2377 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2378 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2379 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2380 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2381 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2382 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2383 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2384 ni 0 set (PAlternative ns a as) = niTms 0 set as
2385 ni 0 set (PHidden tm) = ni 0 set tm
2386 ni 0 set (PUnifyLog tm) = ni 0 set tm
2387 ni 0 set (PDisamb _ tm) = ni 0 set tm
2388 ni 0 set (PNoImplicits tm) = ni 0 set tm
2390 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2391 ni i set (PUnquote tm) = ni (i - 1) set tm
2393 ni i set tm = foldr (S.union . ni i set) set (children tm)
2395 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2396 niTms i set [] = set
2397 niTms i set (x : xs) = niTms i (ni i set x) xs
2399 niTacImp i set (TacImp _ _ scr) = ni i set scr
2400 niTacImp i set _ = set
2402-- Return names which are valid implicits in the given term (type).
2403implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2404implicitNamesIn uvars ist tm
2405 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2408 addImp n = do (imps, fns) <- get
2410 addFn n = do (imps, fns) <- get
2414 notCAF (PExp _ _ _ _ : _) = True
2415 notCAF (_ : xs) = notCAF xs
2417 notHidden (n, _) = case getAccessibility n of
2423 = case lookupDefAccExact n False (tt_ctxt ist) of
2427 ni 0 env (PRef _ _ n@(NS _ _))
2428 | not (n `elem` env)
2429 -- Never implicitly bind if there's a namespace
2431 ni 0 env (PRef _ _ n)
2432 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2433 ni 0 env (PApp _ f@(PRef _ _ n) as)
2434 | n `elem` uvars = do ni 0 env f
2435 mapM_ (ni 0 env . getTm) as
2436 | otherwise = do case lookupTy n (tt_ctxt ist) of
2439 mapM_ (ni 0 env . getTm) as
2440 ni 0 env (PApp _ f as) = do ni 0 env f
2441 mapM_ (ni 0 env . getTm) as
2442 ni 0 env (PAppBind _ f as) = do ni 0 env f
2443 mapM_ (ni 0 env . getTm) as
2444 ni 0 env (PCase _ c os) = do ni 0 env c
2445 -- names in 'os', not counting the names bound in the cases
2446 mapM_ (ni 0 env . snd) os
2449 mapM_ (ni 0 env . fst) os
2451 put (nub imps \\ nub impsfst, fns)
2452 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2453 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2454 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2455 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2456 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2457 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2458 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2459 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2462 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2463 ni 0 env (PHidden tm) = ni 0 env tm
2464 ni 0 env (PUnifyLog tm) = ni 0 env tm
2465 ni 0 env (PDisamb _ tm) = ni 0 env tm
2466 ni 0 env (PNoImplicits tm) = ni 0 env tm
2468 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2469 maybe (return ()) (ni i env) ty
2470 ni i env (PUnquote tm) = ni (i - 1) env tm
2472 ni i env tm = mapM_ (ni i env) (children tm)
2474-- Return names which are free in the given term.
2475namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2476namesIn uvars ist tm = nub $ ni 0 [] tm
2478 ni 0 env (PRef _ _ n)
2479 | not (n `elem` env)
2480 = case lookupTy n (tt_ctxt ist) of
2482 _ -> [n | n `elem` (map fst uvars)]
2483 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2484 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2485 ni 0 env (PCase _ c os) = ni 0 env c ++
2486 -- names in 'os', not counting the names bound in the cases
2487 (nub (concatMap (ni 0 env . snd) os)
2488 \\ nub (concatMap (ni 0 env . fst) os))
2489 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2490 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2491 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2492 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2493 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2494 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2495 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2496 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2497 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2498 ni 0 env (PHidden tm) = ni 0 env tm
2499 ni 0 env (PUnifyLog tm) = ni 0 env tm
2500 ni 0 env (PDisamb _ tm) = ni 0 env tm
2501 ni 0 env (PNoImplicits tm) = ni 0 env tm
2503 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2504 ni i env (PUnquote tm) = ni (i - 1) env tm
2506 ni i env tm = concatMap (ni i env) (children tm)
2508 niTacImp i env (TacImp _ _ scr) = ni i env scr
2511-- Return which of the given names are used in the given term.
2513usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2514usedNamesIn vars ist tm = nub $ ni 0 [] tm
2515 where -- TODO THINK added niTacImp, but is it right?
2516 ni 0 env (PRef _ _ n)
2517 | n `elem` vars && not (n `elem` env)
2518 = case lookupDefExact n (tt_ctxt ist) of
2521 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2522 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2523 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2524 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2525 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2526 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2527 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2528 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2529 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2530 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2531 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2532 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2533 ni 0 env (PHidden tm) = ni 0 env tm
2534 ni 0 env (PUnifyLog tm) = ni 0 env tm
2535 ni 0 env (PDisamb _ tm) = ni 0 env tm
2536 ni 0 env (PNoImplicits tm) = ni 0 env tm
2538 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2539 ni i env (PUnquote tm) = ni (i - 1) env tm
2541 ni i env tm = concatMap (ni i env) (children tm)
2543 niTacImp i env (TacImp _ _ scr) = ni i env scr
2546-- Return the list of inaccessible (= dotted) positions for a name.
2547getErasureInfo :: IState -> Name -> [Int]
2548getErasureInfo ist n =
2549 case lookupCtxtExact n (idris_optimisation ist) of
2550 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