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
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 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
642 -- | interface dictionary, eval only when a function
643 -- argument, and further evaluation results.
645 | OverlappingDictionary -- ^ Interface dictionary which may overlap
646 | Implicit -- ^ implicit coercion
647 | NoImplicit -- ^ do not apply implicit coercions
648 | CExport String -- ^ export, with a C name
649 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
650 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
651 | Reflection -- ^ a reflecting function, compile-time only
652 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
653 | UnfoldIface Name [Name]
654 -- ^ Unfold given interface name in the definition, the
655 -- top level methods, and anything which has
656 -- the interface name as an argument. This is to unfold
657 -- things for termination checking, as interfaces will otherwise
659 | Constructor -- ^ Data constructor type
660 | AutoHint -- ^ use in auto implicit search
661 | PEGenerated -- ^ generated by partial evaluator
662 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
663 deriving (Show, Eq, Generic)
665deriving instance Binary FnOpt
670inlinable :: FnOpts -> Bool
671inlinable = elem Inlinable
673dictionary :: FnOpts -> Bool
674dictionary = elem Dictionary
677-- | Type provider - what to provide
678data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
679 | ProvPostulate t -- ^ goal type must be Type, so only term
680 deriving (Show, Eq, Functor, Generic)
682type ProvideWhat = ProvideWhat' PTerm
684-- | Top-level declarations such as compiler directives, definitions,
685-- datatypes and interfaces.
687 -- | Fixity declaration
688 = PFix FC Fixity [String]
689 -- | Type declaration (last FC is precise name location)
690 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
691 -- | Postulate, second FC is precise name location
692 | PPostulate Bool -- external def if true
693 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
695 | PClauses FC FnOpts Name [PClause' t]
696 -- | Top level constant
698 -- | Data declaration.
699 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
701 | PParams FC [(Name, t)] [PDecl' t]
702 -- | Open block/declaration
703 | POpenInterfaces FC [Name] [PDecl' t]
704 -- | New namespace, where FC is accurate location of the namespace
706 | PNamespace String FC [PDecl' t]
708 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
710 FC -- Record name precise location
711 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
712 [(Name, Docstring (Either Err t))] -- Param Docs
713 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
714 (Maybe (Name, FC)) -- Optional constructor name and location
715 (Docstring (Either Err t)) -- Constructor doc
716 SyntaxInfo -- Constructor SyntaxInfo
718 -- | Interface: arguments are documentation, syntax info, source
719 -- location, constraints, interface name, interface name location,
720 -- parameters, method declarations, optional constructor name
721 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
722 [(Name, t)] -- constraints
723 Name -- interface name
724 FC -- accurate location of interface name
725 [(Name, FC, t)] -- parameters and precise locations
726 [(Name, Docstring (Either Err t))] -- parameter docstrings
727 [(Name, FC)] -- determining parameters and precise locations
728 [PDecl' t] -- declarations
729 (Maybe (Name, FC)) -- implementation constructor name and location
730 (Docstring (Either Err t)) -- implementation constructor docs
732 -- | Implementation declaration: arguments are documentation, syntax
733 -- info, source location, constraints, interface name, parameters, full
734 -- Implementation type, optional explicit name, and definitions
735 | PImplementation (Docstring (Either Err t)) -- Implementation docs
736 [(Name, Docstring (Either Err t))] -- Parameter docs
738 FC [(Name, t)] -- constraints
739 [Name] -- parent dictionaries to search for constraints
743 FC -- precise location of interface
745 [(Name, t)] -- Extra names in scope in the body
746 t -- full Implementation type
747 (Maybe Name) -- explicit name
749 | PDSL Name (DSL' t) -- ^ DSL declaration
750 | PSyntax FC Syntax -- ^ Syntax definition
751 | PMutual FC [PDecl' t] -- ^ Mutual block
752 | PDirective Directive -- ^ Compiler directive.
754 -- | Type provider. The first t is the type, the second is the
755 -- term. The second FC is precise highlighting location.
756 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
758 -- | Source-to-source transformation rule. If bool is True, lhs and
759 -- rhs must be convertible.
760 | PTransform FC Bool t t
762 -- | FC is decl-level, for errors, and Strings represent the
764 | PRunElabDecl FC t [String]
765 deriving (Functor, Generic)
767deriving instance Binary PDecl'
770-- | The set of source directives
771data Directive = DLib Codegen String
772 | DLink Codegen String
773 | DFlag Codegen String
774 | DInclude Codegen String
779 | DSetTotal Name -- assert totality after checking
780 | DAccess Accessibility
781 | DDefault DefaultTotality
783 | DDynamicLibs [String]
784 | DNameHint Name FC [(Name, FC)]
785 | DErrorHandlers Name FC Name FC [(Name, FC)]
786 | DLanguage LanguageExt
787 | DDeprecate Name String
788 | DFragile Name String
789 | DAutoImplicits Bool
793-- | A set of instructions for things that need to happen in IState
794-- after a term elaboration when there's been reflected elaboration.
795data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
796 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
797 | RAddImplementation Name Name
798 | RDatatypeDeclInstrs Name [PArg]
799 -- | Datatype, constructors
800 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
803-- | For elaborator state
804data EState = EState {
805 case_decls :: [(Name, PDecl)]
806 , delayed_elab :: [(Int, Elab' EState ())]
807 , new_tyDecls :: [RDeclInstructions]
808 , highlighting :: [(FC, OutputAnnotation)]
809 , auto_binds :: [Name] -- ^ names bound as auto implicits
810 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
814initEState = EState [] [] [] [] [] []
816type ElabD a = Elab' EState a
818highlightSource :: FC -> OutputAnnotation -> ElabD ()
819highlightSource fc annot =
820 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
822-- | One clause of a top-level definition. Term arguments to constructors are:
824-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
826-- 2. The list of extra 'with' patterns
828-- 3. The right-hand side
830-- 4. The where block (PDecl' t)
832data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
833 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
834 | PClauseR FC [t] t [PDecl' t]
835 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
836 deriving (Functor, Generic)
838deriving instance Binary PClause'
843 -- | Data declaration
844 PDatadecl { d_name :: Name -- ^ The name of the datatype
845 , d_name_fc :: FC -- ^ The precise location of the type constructor name
846 , d_tcon :: t -- ^ Type constructor
847 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
849 -- | "Placeholder" for data whose constructors are defined later
850 | PLaterdecl { d_name :: Name
853 } deriving (Functor, Generic)
855-- | Transform the FCs in a PData and its associated terms. The first
856-- function transforms the general-purpose FCs, and the second
857-- transforms those that are used for semantic source highlighting, so
858-- they can be treated specially.
859mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
860mapPDataFC f g (PDatadecl n nfc tycon ctors) =
861 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
862 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
863 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
864mapPDataFC f g (PLaterdecl n nfc tycon) =
865 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
867deriving instance Binary PData'
870-- Handy to get a free function for applying PTerm -> PTerm functions
871-- across a program, by deriving Functor
873type PDecl = PDecl' PTerm
874type PData = PData' PTerm
875type PClause = PClause' PTerm
877-- | Transform the FCs in a PTerm. The first function transforms the
878-- general-purpose FCs, and the second transforms those that are used
879-- for semantic source highlighting, so they can be treated specially.
880mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
881mapPDeclFC f g (PFix fc fixity ops) =
882 PFix (f fc) fixity ops
883mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
884 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
885mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
886 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
888mapPDeclFC f g (PClauses fc opts n clauses) =
889 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
890mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
891mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
892 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
893mapPDeclFC f g (PParams fc params decls) =
895 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
896 (map (mapPDeclFC f g) decls)
897mapPDeclFC f g (POpenInterfaces fc ifs decls) =
898 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
899mapPDeclFC f g (PNamespace ns fc decls) =
900 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
901mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
902 PRecord doc syn (f fc) opts n (g nfc)
903 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
905 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
906 plic, mapPTermFC f g ty, fdoc))
908 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
911mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
912 PInterface doc syn (f fc)
913 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
914 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
915 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
916 (map (mapPDeclFC f g) body)
917 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
919mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
920 PImplementation doc paramDocs syn (f fc)
921 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
922 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
923 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
924 (mapPTermFC f g implTy)
926 (map (mapPDeclFC f g) body)
927mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
928mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
930 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
931 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
932mapPDeclFC f g (PMutual fc decls) =
933 PMutual (f fc) (map (mapPDeclFC f g) decls)
934mapPDeclFC f g (PDirective d) =
937 DNameHint n nfc ns ->
938 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
939 DErrorHandlers n nfc n' nfc' ns ->
940 DErrorHandlers n (g nfc) n' (g nfc') $
941 map (\(an, anfc) -> (an, g anfc)) ns
942mapPDeclFC f g (PProvider doc syn fc nfc what n) =
943 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
944mapPDeclFC f g (PTransform fc safe l r) =
945 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
946mapPDeclFC f g (PRunElabDecl fc script ns) =
947 PRunElabDecl (f fc) (mapPTermFC f g script) ns
949-- | Get all the names declared in a declaration
950declared :: PDecl -> [Name]
951declared (PFix _ _ _) = []
952declared (PTy _ _ _ _ _ n fc t) = [n]
953declared (PPostulate _ _ _ _ _ _ n t) = [n]
954declared (PClauses _ _ n _) = [] -- not a declaration
955declared (PCAF _ n _) = [n]
956declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
957 where fstt (_, _, a, _, _, _, _) = a
958declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
959declared (PParams _ _ ds) = concatMap declared ds
960declared (POpenInterfaces _ _ ds) = concatMap declared ds
961declared (PNamespace _ _ ds) = concatMap declared ds
962declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
963declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
964declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
968declared (PDSL n _) = [n]
969declared (PSyntax _ _) = []
970declared (PMutual _ ds) = concatMap declared ds
971declared (PDirective _) = []
974-- get the names declared, not counting nested parameter blocks
975tldeclared :: PDecl -> [Name]
976tldeclared (PFix _ _ _) = []
977tldeclared (PTy _ _ _ _ _ n _ t) = [n]
978tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
979tldeclared (PClauses _ _ n _) = [] -- not a declaration
980tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
981tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
982 where fstt (_, _, a, _, _, _, _) = a
983tldeclared (PParams _ _ ds) = []
984tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
985tldeclared (PMutual _ ds) = concatMap tldeclared ds
986tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
987tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
988tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
994defined :: PDecl -> [Name]
995defined (PFix _ _ _) = []
996defined (PTy _ _ _ _ _ n _ t) = []
997defined (PPostulate _ _ _ _ _ _ n t) = []
998defined (PClauses _ _ n _) = [n] -- not a declaration
999defined (PCAF _ n _) = [n]
1000defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1001 where fstt (_, _, a, _, _, _, _) = a
1002defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1003defined (PParams _ _ ds) = concatMap defined ds
1004defined (POpenInterfaces _ _ ds) = concatMap defined ds
1005defined (PNamespace _ _ ds) = concatMap defined ds
1006defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1007defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1008defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1012defined (PDSL n _) = [n]
1013defined (PSyntax _ _) = []
1014defined (PMutual _ ds) = concatMap defined ds
1015defined (PDirective _) = []
1018updateN :: [(Name, Name)] -> Name -> Name
1019updateN ns n | Just n' <- lookup n ns = n'
1022updateNs :: [(Name, Name)] -> PTerm -> PTerm
1024updateNs ns t = mapPT updateRef t
1025 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1028-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1029-- updateDNs [] t = t
1030-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1031-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1032-- where updateCNs ns (PClause n l ts r ds)
1033-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1034-- (map (fmap (updateNs ns)) ts)
1035-- (fmap (updateNs ns) r)
1036-- (map (updateDNs ns) ds)
1037-- updateDNs ns c = c
1039data PunInfo = IsType
1042 deriving (Eq, Show, Data, Typeable, Generic)
1044-- | High level language terms
1045data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1046 -- high-level language
1048 -- ^ A reference to a variable. The FC is its precise
1049 -- source location for highlighting. The list of FCs is a
1050 -- collection of additional highlighting locations.
1051 | PInferRef FC [FC] Name -- ^ A name to be defined later
1052 | PPatvar FC Name -- ^ A pattern variable
1053 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1054 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1055 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1056 | PTyped PTerm PTerm -- ^ Term with explicit type
1057 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1058 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1059 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1060 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1061 | PMatchApp FC Name -- ^ Make an application by type matching
1062 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1063 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1064 | PTrue FC PunInfo -- ^ Unit type..?
1065 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1066 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1067 -- ^ "rewrite" syntax, with optional rewriting function and
1068 -- optional result type
1069 | PPair FC [FC] PunInfo PTerm PTerm
1070 -- ^ A pair (a, b) and whether it's a product type or a
1071 -- pair (solved by elaboration). The list of FCs is its
1073 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1074 -- ^ A dependent pair (tm : a ** b) and whether it's a
1075 -- sigma type or a pair that inhabits one (solved by
1076 -- elaboration). The [FC] is its punctuation.
1077 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1078 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1079 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1080 | PType FC -- ^ 'Type' type
1081 | PUniverse FC Universe -- ^ Some universe
1082 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1083 | PConstant FC Const -- ^ Builtin types
1084 | Placeholder -- ^ Underscore
1085 | PDoBlock [PDo] -- ^ Do notation
1086 | PIdiom FC PTerm -- ^ Idiom brackets
1087 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1088 | PProof [PTactic] -- ^ Proof script
1089 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1090 | PElabError Err -- ^ Error to report on elaboration
1091 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1092 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1093 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1094 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1095 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1096 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1097 | PUnquote PTerm -- ^ ~Term
1098 | PQuoteName Name Bool FC
1099 -- ^ `{n} where the FC is the precise highlighting for
1100 -- the name in particular. If the Bool is False, then
1101 -- it's `{{n}} and the name won't be resolved.
1102 | PRunElab FC PTerm [String]
1103 -- ^ %runElab tm - New-style proof script. Args are
1104 -- location, script, enclosing namespace.
1105 | PConstSugar FC PTerm
1106 -- ^ A desugared constant. The FC is a precise source
1107 -- location that will be used to highlight it later.
1108 deriving (Eq, Data, Typeable, Generic)
1110data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1113 deriving (Eq, Data, Generic, Typeable)
1115-- | Transform the FCs in a PTerm. The first function transforms the
1116-- general-purpose FCs, and the second transforms those that are used
1117-- for semantic source highlighting, so they can be treated specially.
1118mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1119mapPTermFC f g (PQuote q) = PQuote q
1120mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1121mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1122mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1123mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1124mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1125mapPTermFC 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)
1126mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1127mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1128mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1129mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1130mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1131mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1132mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1133mapPTermFC 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)
1134mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1135mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1136mapPTermFC 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)
1137mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1138mapPTermFC 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)
1139mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1140mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1141mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1142mapPTermFC f g (PType fc) = PType (f fc)
1143mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1144mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1145mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1146mapPTermFC f g Placeholder = Placeholder
1147mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1148 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1149 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1150 mapPDoFC (DoBindP fc t1 t2 alts) =
1151 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1152 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1153 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1154mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1155mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1156mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1157mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1158mapPTermFC f g (PElabError err) = PElabError err
1159mapPTermFC f g PImpossible = PImpossible
1160mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1161mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1162mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1163mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1164mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1165mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1166mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1167mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1168mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1171dg instance Binary PTerm
1174mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1175mapPT f t = f (mpt t) where
1176 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1177 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1178 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1179 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1180 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1181 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1182 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1183 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1184 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1185 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1186 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1187 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1188 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1189 mpt (PHidden t) = PHidden (mapPT f t)
1190 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1191 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1192 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1193 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1194 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1195 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1196 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1200data PTactic' t = Intro [Name] | Intros | Focus Name
1201 | Refine Name [Bool] | Rewrite t | DoUnify
1208 | LetTac Name t | LetTacTy Name t t
1209 | Exact t | Compute | Trivial | TCImplementation
1210 | ProofSearch Bool Bool Int (Maybe Name)
1211 [Name] -- allowed local names
1213 -- ^ the bool is whether to search recursively
1216 | ProofState | ProofTerm | Undo
1217 | Try (PTactic' t) (PTactic' t)
1218 | TSeq (PTactic' t) (PTactic' t)
1219 | ApplyTactic t -- see Language.Reflection module
1223 | GoalType String (PTactic' t)
1226 | TDocStr (Either Name Const)
1229 | TFail [ErrorReportPart]
1232 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Generic, Typeable)
1234deriving instance Binary PTactic'
1236instance Sized a => Sized (PTactic' a) where
1237 size (Intro nms) = 1 + size nms
1239 size (Focus nm) = 1 + size nm
1240 size (Refine nm bs) = 1 + size nm + length bs
1241 size (Rewrite t) = 1 + size t
1242 size (Induction t) = 1 + size t
1243 size (LetTac nm t) = 1 + size nm + size t
1244 size (Exact t) = 1 + size t
1252 size (Try l r) = 1 + size l + size r
1253 size (TSeq l r) = 1 + size l + size r
1254 size (ApplyTactic t) = 1 + size t
1255 size (Reflect t) = 1 + size t
1256 size (Fill t) = 1 + size t
1260 size (TFail ts) = 1 + size ts
1263 size (CaseTac x) = 1 + size x
1264 size (Equiv t) = 1 + size t
1265 size (Claim x y) = 1 + size x + size y
1267 size (MatchRefine x) = 1 + size x
1268 size (LetTacTy x y z) = 1 + size x + size y + size z
1269 size TCImplementation = 1
1271type PTactic = PTactic' PTerm
1273data PDo' t = DoExp FC t
1274 | DoBind FC Name FC t -- ^ second FC is precise name location
1275 | DoBindP FC t t [(t,t)]
1276 | DoLet FC Name FC t t -- ^ second FC is precise name location
1278 deriving (Eq, Functor, Data, Generic, Typeable)
1280deriving instance Binary PDo'
1283instance Sized a => Sized (PDo' a) where
1284 size (DoExp fc t) = 1 + size fc + size t
1285 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1286 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1287 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1288 size (DoLetP fc l r) = 1 + size fc + size l + size r
1290type PDo = PDo' PTerm
1292-- The priority gives a hint as to elaboration order. Best to elaborate
1293-- things early which will help give a more concrete type to other
1294-- variables, e.g. a before (interpTy a).
1296data PArg' t = PImp { priority :: Int
1297 , machine_inf :: Bool -- ^ true if the machine inferred it
1298 , argopts :: [ArgOpt]
1302 | PExp { priority :: Int
1303 , argopts :: [ArgOpt]
1307 | PConstraint { priority :: Int
1308 , argopts :: [ArgOpt]
1312 | PTacImplicit { priority :: Int
1313 , argopts :: [ArgOpt]
1318 deriving (Show, Eq, Functor, Data, Generic, Typeable)
1320data ArgOpt = AlwaysShow
1324 deriving (Show, Eq, Data, Generic, Typeable)
1326instance Sized a => Sized (PArg' a) where
1327 size (PImp p _ l nm trm) = 1 + size nm + size trm
1328 size (PExp p l nm trm) = 1 + size nm + size trm
1329 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1330 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1333deriving instance Binary PArg'
1336pimp n t mach = PImp 1 mach [] n t
1337pexp t = PExp 1 [] (sMN 0 "arg") t
1338pconst t = PConstraint 1 [] (sMN 0 "carg") t
1339ptacimp n s t = PTacImplicit 2 [] n s t
1341type PArg = PArg' PTerm
1343-- | Get the highest FC in a term, if one exists
1344highestFC :: PTerm -> Maybe FC
1345highestFC (PQuote _) = Nothing
1346highestFC (PRef fc _ _) = Just fc
1347highestFC (PInferRef fc _ _) = Just fc
1348highestFC (PPatvar fc _) = Just fc
1349highestFC (PLam fc _ _ _ _) = Just fc
1350highestFC (PPi _ _ _ _ _) = Nothing
1351highestFC (PLet fc _ _ _ _ _) = Just fc
1352highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1353highestFC (PApp fc _ _) = Just fc
1354highestFC (PAppBind fc _ _) = Just fc
1355highestFC (PMatchApp fc _) = Just fc
1356highestFC (PCase fc _ _) = Just fc
1357highestFC (PIfThenElse fc _ _ _) = Just fc
1358highestFC (PTrue fc _) = Just fc
1359highestFC (PResolveTC fc) = Just fc
1360highestFC (PRewrite fc _ _ _ _) = Just fc
1361highestFC (PPair fc _ _ _ _) = Just fc
1362highestFC (PDPair fc _ _ _ _ _) = Just fc
1363highestFC (PAs fc _ _) = Just fc
1364highestFC (PAlternative _ _ args) =
1365 case mapMaybe highestFC args of
1368highestFC (PHidden _) = Nothing
1369highestFC (PType fc) = Just fc
1370highestFC (PUniverse _ _) = Nothing
1371highestFC (PGoal fc _ _ _) = Just fc
1372highestFC (PConstant fc _) = Just fc
1373highestFC Placeholder = Nothing
1374highestFC (PDoBlock lines) =
1375 case map getDoFC lines of
1379 getDoFC (DoExp fc t) = fc
1380 getDoFC (DoBind fc nm nfc t) = fc
1381 getDoFC (DoBindP fc l r alts) = fc
1382 getDoFC (DoLet fc nm nfc l r) = fc
1383 getDoFC (DoLetP fc l r) = fc
1385highestFC (PIdiom fc _) = Just fc
1386highestFC (PMetavar fc _) = Just fc
1387highestFC (PProof _) = Nothing
1388highestFC (PTactics _) = Nothing
1389highestFC (PElabError _) = Nothing
1390highestFC PImpossible = Nothing
1391highestFC (PCoerced tm) = highestFC tm
1392highestFC (PDisamb _ opts) = highestFC opts
1393highestFC (PUnifyLog tm) = highestFC tm
1394highestFC (PNoImplicits tm) = highestFC tm
1395highestFC (PQuasiquote _ _) = Nothing
1396highestFC (PUnquote tm) = highestFC tm
1397highestFC (PQuoteName _ _ fc) = Just fc
1398highestFC (PRunElab fc _ _) = Just fc
1399highestFC (PConstSugar fc _) = Just fc
1400highestFC (PAppImpl t _) = highestFC t
1404data InterfaceInfo = CI {
1405 implementationCtorName :: Name
1406 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1407 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1408 , interface_default_super_interfaces :: [PDecl]
1409 , interface_impparams :: [Name]
1410 , interface_params :: [Name]
1411 , interface_constraints :: [PTerm]
1412 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1413 , interface_determiners :: [Int]
1414 } deriving (Show, Generic)
1416deriving instance Binary InterfaceInfo
1420data RecordInfo = RI {
1421 record_parameters :: [(Name,PTerm)]
1422 , record_constructor :: Name
1423 , record_projections :: [Name]
1424 } deriving (Show, Generic)
1426-- Type inference data
1428data TIData = TIPartial -- ^ a function with a partially defined type
1429 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1430 deriving (Show, Generic)
1432-- | Miscellaneous information about functions
1433data FnInfo = FnInfo { fn_params :: [Int] }
1434 deriving (Show, Generic)
1436deriving instance Binary FnInfo
1439data OptInfo = Optimise {
1440 inaccessible :: [(Int,Name)] -- includes names for error reporting
1441 , detaggable :: Bool
1442 } deriving (Show, Generic)
1444deriving instance Binary OptInfo
1447-- | Syntactic sugar info
1452 , dsl_var :: Maybe t
1453 , index_first :: Maybe t
1454 , index_next :: Maybe t
1455 , dsl_lambda :: Maybe t
1456 , dsl_let :: Maybe t
1458 } deriving (Show, Functor, Generic)
1460deriving instance Binary DSL'
1463type DSL = DSL' PTerm
1465data SynContext = PatternSyntax
1468 deriving (Show, Generic)
1470deriving instance Binary SynContext
1473data Syntax = Rule [SSymbol] PTerm SynContext
1474 | DeclRule [SSymbol] [PDecl]
1475 deriving (Show, Generic)
1477syntaxNames :: Syntax -> [Name]
1478syntaxNames (Rule syms _ _) = mapMaybe ename syms
1479 where ename (Keyword n) = Just n
1481syntaxNames (DeclRule syms _) = mapMaybe ename syms
1482 where ename (Keyword n) = Just n
1485syntaxSymbols :: Syntax -> [SSymbol]
1486syntaxSymbols (Rule ss _ _) = ss
1487syntaxSymbols (DeclRule ss _) = ss
1489deriving instance Binary Syntax
1492data SSymbol = Keyword Name
1497 deriving (Show, Eq, Generic)
1501deriving instance Binary SSymbol
1504newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1507emptySyntaxRules :: SyntaxRules
1508emptySyntaxRules = SyntaxRules []
1510updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1511updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1513 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1518 ruleSort (s1:ss1) (s2:ss2) =
1519 case symCompare s1 s2 of
1520 EQ -> ruleSort ss1 ss2
1523 -- Better than creating Ord implementation for SSymbol since
1524 -- in general this ordering does not really make sense.
1525 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1526 symCompare (Keyword _) _ = LT
1527 symCompare (Symbol _) (Keyword _) = GT
1528 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1529 symCompare (Symbol _) _ = LT
1530 symCompare (Binding _) (Keyword _) = GT
1531 symCompare (Binding _) (Symbol _) = GT
1532 symCompare (Binding b1) (Binding b2) = compare b1 b2
1533 symCompare (Binding _) _ = LT
1534 symCompare (Expr _) (Keyword _) = GT
1535 symCompare (Expr _) (Symbol _) = GT
1536 symCompare (Expr _) (Binding _) = GT
1537 symCompare (Expr e1) (Expr e2) = compare e1 e2
1538 symCompare (Expr _) _ = LT
1539 symCompare (SimpleExpr _) (Keyword _) = GT
1540 symCompare (SimpleExpr _) (Symbol _) = GT
1541 symCompare (SimpleExpr _) (Binding _) = GT
1542 symCompare (SimpleExpr _) (Expr _) = GT
1543 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1545initDSL = DSL (PRef f [] (sUN ">>="))
1546 (PRef f [] (sUN "<*>"))
1547 (PRef f [] (sUN "pure"))
1554 where f = fileFC "(builtin)"
1556data Using = UImplicit Name PTerm
1557 | UConstraint Name [Name]
1558 deriving (Show, Eq, Data, Generic, Typeable)
1560deriving instance Binary Using
1563data SyntaxInfo = Syn {
1565 , syn_params :: [(Name, PTerm)]
1566 , syn_namespace :: [String]
1568 , imp_methods :: [Name]
1569 -- ^ interface methods. When expanding implicits, these should be
1570 -- expanded even under binders
1571 , decoration :: Name -> Name
1573 , implicitAllowed :: Bool
1574 , constraintAllowed :: Bool
1575 , maxline :: Maybe Int
1576 , mut_nesting :: Int
1578 , syn_in_quasiquote :: Int
1579 , syn_toplevel :: Bool
1580 , withAppAllowed :: Bool
1581 } deriving (Show, Generic)
1583deriving instance Binary SyntaxInfo
1586defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1588expandNS :: SyntaxInfo -> Name -> Name
1589expandNS syn n@(NS _ _) = n
1590expandNS syn n = case syn_namespace syn of
1595-- For inferring types of things
1597bi = fileFC "builtin"
1598primfc = fileFC "(primitive)"
1600inferTy = sMN 0 "__Infer"
1601inferCon = sMN 0 "__infer"
1602inferDecl = PDatadecl inferTy primfc
1604 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1605 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1606 (PRef bi [] inferTy)), bi, [])]
1609infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1610infP = P (TCon 6 0) inferTy (TType (UVal 0))
1612getInferTerm, getInferType :: Term -> Term
1613getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1614getInferTerm (App _ (App _ _ _) tm) = tm
1615getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1617getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1618 where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))
1619 toTy (PVar t) = PVTy t
1621getInferType (App _ (App _ _ ty) _) = ty
1625-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1627primNames = [inferTy, inferCon]
1630unitCon = sUN "MkUnit"
1632falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1633 "The empty type, also known as the trivially false proposition." ++
1635 "Use `void` or `absurd` to prove anything if you have a variable " ++
1636 "of type `Void` in scope."
1639pairTy = sNS (sUN "Pair") ["Builtins"]
1640pairCon = sNS (sUN "MkPair") ["Builtins"]
1642upairTy = sNS (sUN "UPair") ["Builtins"]
1643upairCon = sNS (sUN "MkUPair") ["Builtins"]
1647eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1648 "The propositional equality type. A proof that `x` = `y`." ++
1650 "To use such a proof, pattern-match on it, and the two equal things will " ++
1651 "then need to be the _same_ pattern." ++
1653 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1654 "is possible to state equalities between values of potentially different " ++
1655 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1657 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1659eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1660 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1662 [(reflDoc, reflParamDoc,
1663 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1664 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1665 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1666 pimp (n "B") Placeholder False,
1667 pexp (PRef bi [] (n "x")),
1668 pexp (PRef bi [] (n "x"))])), bi, [])]
1670 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1671 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1672 "shown that both sides are in fact equal."
1673 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1674 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1676eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1677 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1683-- | The special name to be used in the module documentation context -
1684-- not for use in the main definition context. The namespace around it
1685-- will determine the module to which the docs adhere.
1687modDocName = sMN 0 "ModuleDocs"
1689-- Defined in builtins.idr
1690sigmaTy = sNS (sUN "DPair") ["Builtins"]
1691sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1693piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1694piBind = piBindp expl
1696piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1698piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1701-- Pretty-printing declarations and terms
1703-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1704-- could interfere with interactive editing, which calls "show".
1706instance Show PTerm where
1707 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1709instance Show PDecl where
1710 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1712instance Show PClause where
1713 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1715instance Show PData where
1716 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1718instance Pretty PTerm OutputAnnotation where
1719 pretty = prettyImp defaultPPOption
1721-- | Colourise annotations according to an Idris state. It ignores the
1722-- names in the annotation, as there's no good way to show extended
1723-- information on a terminal.
1724annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1725annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1726annotationColour ist (AnnConst c) =
1727 let theme = idris_colourTheme ist
1728 in Just $ if constIsType c
1729 then typeColour theme
1730 else dataColour theme
1731annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1732annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1733annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1734annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1735annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1736annotationColour ist (AnnName n _ _ _) =
1737 let ctxt = tt_ctxt ist
1738 theme = idris_colourTheme ist
1740 _ | isDConName n ctxt -> Just $ dataColour theme
1741 _ | isFnName n ctxt -> Just $ functionColour theme
1742 _ | isTConName n ctxt -> Just $ typeColour theme
1743 _ | isPostulateName n ist -> Just $ postulateColour theme
1744 _ | otherwise -> Nothing -- don't colourise unknown names
1745annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1746 where colour BoldText = IdrisColour Nothing True False True False
1747 colour UnderlineText = IdrisColour Nothing True True False False
1748 colour ItalicText = IdrisColour Nothing True False False True
1749annotationColour ist _ = Nothing
1752-- | Colourise annotations according to an Idris state. It ignores the
1753-- names in the annotation, as there's no good way to show extended
1754-- information on a terminal. Note that strings produced this way will
1755-- not be coloured on Windows, so the use of the colour rendering
1756-- functions in Idris.Output is to be preferred.
1757consoleDecorate :: IState -> OutputAnnotation -> String -> String
1758consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1760isPostulateName :: Name -> IState -> Bool
1761isPostulateName n ist = S.member n (idris_postulates ist)
1763-- | Pretty-print a high-level closed Idris term with no information
1764-- about precedence/associativity
1765prettyImp :: PPOption -- ^ pretty printing options
1766 -> PTerm -- ^ the term to pretty-print
1767 -> Doc OutputAnnotation
1768prettyImp impl = pprintPTerm impl [] [] []
1770-- | Serialise something to base64 using its Binary implementation.
1772-- | Do the right thing for rendering a term in an IState
1773prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1774prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1776-- | Pretty-print a high-level Idris term in some bindings context
1778pprintPTerm :: PPOption -- ^ pretty printing options
1779 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1780 -> [Name] -- ^ names to always show in pi, even if not used
1781 -> [FixDecl] -- ^ Fixity declarations
1782 -> PTerm -- ^ the term to pretty-print
1783 -> Doc OutputAnnotation
1784pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1789 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1790 prettySe d p bnd (PQuote r) =
1791 text "![" <> pretty r <> text "]"
1792 prettySe d p bnd (PPatvar fc n) = pretty n
1794 | Just str <- slist d p bnd e = depth d str
1795 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1796 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1797 prettySe d p bnd (PLam fc n nfc ty sc) =
1798 let (ns, sc') = getLamNames [n] sc in
1799 depth d . bracket p startPrec . group . align . hang 2 $
1800 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1801 prettySe (decD d) startPrec ((n, False):bnd) sc'
1803 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1804 getLamNames acc sc = (reverse acc, sc)
1806 prettyBindingsOf [] t = text ""
1807 prettyBindingsOf [n] t = prettyBindingOf n t
1808 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1809 prettyBindingsOf ns t
1810 prettySe d p bnd (PLet fc n nfc ty v sc) =
1811 depth d . bracket p startPrec . group . align $
1812 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1813 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1814 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1815 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1816 || ppopt_pinames ppo && uname n =
1817 depth d . bracket p startPrec . group $
1818 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1819 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1821 depth d . bracket p startPrec . group $
1822 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1823 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1825 uname (UN n) = case str n of
1832 Static -> text "%static" <> space
1834 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1836 depth d . bracket p startPrec $
1837 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1838 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1839 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1843 Static -> text "%static" <> space
1845 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1846 depth d . bracket p startPrec $
1847 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1848 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1849 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1850 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1851 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1852 depth d . bracket p startPrec $
1853 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1854 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1855 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1856 | basename neg == sUN "negate" =
1857 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1858 -- This case preserves the behavior of the former constructor PEq.
1859 -- It should be removed if feasible when the pretty-printing of infix
1860 -- operators in general is improved.
1861 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1862 | n == eqTy, ppopt_impl ppo =
1863 depth d . bracket p eqPrec $
1864 enclose lparen rparen eq <+>
1865 align (group (vsep (map (prettyArgS (decD d) bnd)
1868 depth d . bracket p eqPrec . align . group $
1869 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1870 where eq = annName eqTy (text "=")
1872 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1873 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1874 | UN nm <- basename f
1875 , not (ppopt_impl ppo) && null (getShowArgs args) =
1876 prettyName True (ppopt_impl ppo) bnd f
1877 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1878 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1879 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1880 | UN nm <- basename op
1882 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1883 case getShowArgs args of
1885 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1886 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1887 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1888 (l@(PExp{}) : r@(PExp{}) : rest) ->
1889 depth d . bracket p funcAppPrec $
1890 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1891 align (group (vsep (map (prettyArgS d bnd) rest)))
1892 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1893 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1894 f = getFixity (opStr op)
1896 Nothing -> funcAppPrec + 1
1897 Just (Infixl p') -> p'
1898 Just f' -> prec f' + 1
1900 Nothing -> funcAppPrec + 1
1901 Just (Infixr p') -> p'
1902 Just f' -> prec f' + 1
1903 inFix l r = align . group $
1904 (prettySe (decD d) left bnd l <+> opName False) <$>
1905 group (prettySe (decD d) right bnd r)
1906 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1907 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1908 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1909 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1910 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1911 let args = getShowArgs as
1912 fp = prettySe (decD d) (startPrec + 1) bnd f
1913 shownArgs = if ppopt_impl ppo then as else args
1915 depth d . bracket p funcAppPrec . group $
1918 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1919 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1920 prettySe d p bnd (PCase _ scr cases) =
1921 bracket p funcAppPrec $
1922 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1923 depth d (indent 2 (vsep (map ppcase cases)))
1925 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1926 ([(n, False) | n <- vars l] ++ bnd)
1927 in nest nestingSize $
1928 prettyCase l <+> text "=>" <+> prettyCase r
1929 -- Warning: this is a bit of a hack. At this stage, we don't have the
1930 -- global context, so we can't determine which names are constructors,
1931 -- which are types, and which are pattern variables on the LHS of the
1932 -- case pattern. We use the heuristic that names without a namespace
1933 -- are patvars, because right now case blocks in PTerms are always
1934 -- delaborated from TT before being sent to the pretty-printer. If they
1935 -- start getting printed directly, THIS WILL BREAK.
1936 -- Potential solution: add a list of known patvars to the cases in
1937 -- PCase, and have the delaborator fill it out, kind of like the pun
1938 -- disambiguation on PDPair.
1939 vars tm = filter noNS (allNamesIn tm)
1940 noNS (NS _ _) = False
1943 prettySe d p bnd (PIfThenElse _ c t f) =
1944 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1945 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1946 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1947 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1949 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1950 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1951 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1952 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1953 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1954 prettySe d p bnd (PRewrite _ by l r _) =
1955 depth d . bracket p startPrec $
1956 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1959 Just fn -> text "using" <+>
1960 prettyName True (ppopt_impl ppo) bnd fn) <+>
1961 text "in" <+> prettySe (decD d) startPrec bnd r
1962 prettySe d p bnd (PTyped l r) =
1963 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1964 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1965 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1966 align . group . vsep . punctuate (ann comma) $
1967 map (prettySe (decD d) startPrec bnd) elts
1968 where ann = case pun of
1970 IsType -> annName pairTy
1971 IsTerm -> annName pairCon
1972 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1973 | Just elts <- dPairElts dpair
1974 = depth d . enclose (annotated lparen) (annotated rparen) .
1975 align . group . vsep . punctuate (space <> annotated (text "**")) $
1981 annotated (text "**") <+>
1982 prettySe (decD d) startPrec (addBinding bnd) r <>
1984 where annotated = case pun of
1985 IsType -> annName sigmaTy
1986 IsTerm -> annName sigmaCon
1989 (left, addBinding) = case (l, pun) of
1990 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1991 _ -> (prettySe (decD d) startPrec bnd l, id)
1994 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1995 ppElts ((PRef _ _ n, t):rs) bs
1997 = (bindingOf n False <+> colon <+>
1998 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1999 ppElts ((l, t):rs) bs
2000 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2001 prettySe d p bnd (PAlternative ns a as) =
2002 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2005 foldr ((\ l r -> l <+> text "," <+> r) .
2006 depth d . prettySe (decD d) startPrec bnd)
2008 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2009 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2010 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2011 -- XXX: add pretty for tactics
2012 prettySe d p bnd (PProof ts) =
2013 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2014 prettySe d p bnd (PTactics ts) =
2015 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2016 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2017 prettySe d p bnd PImpossible = kwd "impossible"
2018 prettySe d p bnd Placeholder = text "_"
2019 prettySe d p bnd (PDoBlock dos) =
2020 bracket p startPrec $
2021 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2022 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2023 ppdo bnd (DoBind _ bn _ tm : dos) =
2024 (prettyBindingOf bn False <+> text "<-" <+>
2025 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2026 ppdo ((bn, False):bnd) dos
2027 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2028 text "no pretty printer for pattern-matching do binding" :
2030 ppdo bnd (DoLet _ ln _ ty v : dos) =
2031 (kwd "let" <+> prettyBindingOf ln False <+>
2032 (if ty /= Placeholder
2033 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2035 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2036 ppdo ((ln, False):bnd) dos
2037 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2038 text "no pretty printer for pattern-matching do binding" :
2041 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2042 prettySe d p bnd (PElabError s) = pretty s
2043 -- Quasiquote pprinting ignores bound vars
2044 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2045 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2046 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2047 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2048 where start = if res then "`{" else "`{{"
2049 end = if res then "}" else "}}"
2050 prettySe d p bnd (PRunElab _ tm _) =
2051 bracket p funcAppPrec . group . align . hang 2 $
2053 prettySe (decD d) funcAppPrec bnd tm
2054 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2055 prettySe d p bnd _ = text "missing pretty-printer for term"
2057 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2058 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2059 where display (UN n) = T.unpack n
2060 display (MN _ n) = T.unpack n
2061 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2062 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2065 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2066 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2067 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2068 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2070 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2071 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2072 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2073 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2075 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2076 annName n = annotate (AnnName n Nothing Nothing Nothing)
2078 opStr :: Name -> String
2079 opStr (NS n _) = opStr n
2080 opStr (UN n) = T.unpack n
2082 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2083 slist' (Just d) _ _ _ | d <= 0 = Nothing
2085 | containsHole e = Nothing
2086 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2087 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2088 slist' d p bnd (PRef _ _ nil)
2089 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2090 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2091 | nsroot cons == sUN "::",
2092 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2094 Just tl' <- slist' (decD d) p bnd tl
2095 = Just (prettySe d startPrec bnd hd : tl')
2097 isImp (PImp {}) = True
2099 slist' _ _ _ tm = Nothing
2101 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2103 [] -> annotate (AnnData "" "") $ text "[]"
2104 [x] -> enclose left right . group $ x
2105 xs -> enclose left right .
2106 align . group . vsep .
2107 punctuate comma $ xs
2108 where left = (annotate (AnnData "" "") (text "["))
2109 right = (annotate (AnnData "" "") (text "]"))
2110 comma = (annotate (AnnData "" "") (text ","))
2111 slist _ _ _ _ = Nothing
2113 pairElts :: PTerm -> Maybe [PTerm]
2114 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2115 | otherwise = Just [x, y]
2116 pairElts _ = Nothing
2118 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2119 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2120 | otherwise = Just [(l, t), (Placeholder, r)]
2121 dPairElts _ = Nothing
2123 natns = "Prelude.Nat."
2125 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2127 | ppopt_desugarnats ppo = Nothing
2128 | otherwise = snat' d p e
2130 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2131 snat' (Just x) _ _ | x <= 0 = Nothing
2132 snat' d p (PRef _ _ z)
2133 | show z == (natns++"Z") || show z == "Z" = Just 0
2134 snat' d p (PApp _ s [PExp {getTm=n}])
2135 | show s == (natns++"S") || show s == "S",
2136 Just n' <- snat' (decD d) p n
2138 snat' _ _ _ = Nothing
2140 bracket outer inner doc
2141 | outer > inner = lparen <> doc <> rparen
2144 ellipsis = text "..."
2147 depth (Just d) = if d <= 0 then const ellipsis else id
2149 decD = fmap (\x -> x - 1)
2151 kwd = annotate AnnKeyword . text
2153 fixities :: M.Map String Fixity
2154 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2156 getFixity :: String -> Maybe Fixity
2157 getFixity = flip M.lookup fixities
2159-- | Strip away namespace information
2160basename :: Name -> Name
2161basename (NS n _) = basename n
2164-- | Determine whether a name was the one inserted for a hole or guess
2165-- by the delaborator
2166isHoleName :: Name -> Bool
2167isHoleName (UN n) = n == T.pack "[__]"
2170-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2171containsHole :: PTerm -> Bool
2172containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2174-- | Pretty-printer helper for names that attaches the correct annotations
2175prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2176 -> Bool -- ^ whether to show namespaces
2177 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2178 -> Name -- ^ the name to pprint
2179 -> Doc OutputAnnotation
2180prettyName infixParen showNS bnd n
2181 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2182 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2183 | (UN n') <- n, T.unpack n' == "_" = text "_"
2184 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2185 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2186 where fullName = text nameSpace <> parenthesise (text (baseName n))
2187 baseName (UN n) = T.unpack n
2188 baseName (NS n ns) = baseName n
2189 baseName (MN i s) = T.unpack s
2190 baseName other = show other
2191 nameSpace = case n of
2192 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2194 isInfix = case baseName n of
2196 (c : _) -> not (isAlpha c)
2197 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2200showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2201showCImp ppo (PClause _ n l ws r w)
2202 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2203 <+> text "where" <+> text (show w)
2206 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2207showCImp ppo (PWith _ n l ws r pn w)
2208 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2209 <+> braces (text (show w))
2212 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2215showDImp :: PPOption -> PData -> Doc OutputAnnotation
2216showDImp ppo (PDatadecl n nfc ty cons)
2217 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2218 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2220showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2221showDecls o ds = vsep (map (showDeclImp o) ds)
2223showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2224showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2225showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2226 indent 2 (vsep (map (showCImp o) cs))
2227showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2228showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2229showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2230showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2231showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2232showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2233 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2234showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2235 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2236showDeclImp _ _ = text "..."
2237-- showDeclImp (PImport o) = "import " ++ o
2239getImps :: [PArg] -> [(Name, PTerm)]
2241getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2242getImps (_ : xs) = getImps xs
2244getExps :: [PArg] -> [PTerm]
2246getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2247getExps (_ : xs) = getExps xs
2249getShowArgs :: [PArg] -> [PArg]
2251getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2252getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2253 | PImp _ _ _ _ tm <- e
2254 , containsHole tm = e : getShowArgs xs
2255getShowArgs (_ : xs) = getShowArgs xs
2257getConsts :: [PArg] -> [PTerm]
2259getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2260getConsts (_ : xs) = getConsts xs
2262getAll :: [PArg] -> [PTerm]
2267showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2268 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2269 -> PPOption -- ^ pretty printing options
2270 -> Bool -- ^ whether to colourise
2271 -> Name -- ^ the term to show
2273showName ist bnd ppo colour n = case ist of
2274 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2275 Nothing -> showbasic n
2276 where name = if ppopt_impl ppo then show n else showbasic n
2277 showbasic n@(UN _) = showCG n
2278 showbasic (MN i s) = str s
2279 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2280 showbasic (SN s) = show s
2282 colourise n t = let ctxt' = fmap tt_ctxt ist in
2285 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2286 else colouriseBound t name
2287 | isDConName n ctxt -> colouriseData t name
2288 | isFnName n ctxt -> colouriseFun t name
2289 | isTConName n ctxt -> colouriseType t name
2290 -- The assumption is that if a name is not bound and does not exist in the
2291 -- global context, then we're somewhere in which implicit info has been lost
2292 -- (like error messages). Thus, unknown vars are colourised as implicits.
2293 | otherwise -> colouriseImplicit t name
2295showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2296 -> PTerm -- ^ the term to show
2298showTm ist = displayDecorated (consoleDecorate ist) .
2299 renderPretty 0.8 100000 .
2300 prettyImp (ppOptionIst ist)
2302-- | Show a term with implicits, no colours
2303showTmImpls :: PTerm -> String
2304showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2306-- | Show a term with specific options
2307showTmOpts :: PPOption -> PTerm -> String
2308showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2311instance Sized PTerm where
2312 size (PQuote rawTerm) = size rawTerm
2313 size (PRef fc _ name) = size name
2314 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2315 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2316 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2317 size (PTyped trm ty) = 1 + size trm + size ty
2318 size (PApp fc name args) = 1 + size args
2319 size (PAppBind fc name args) = 1 + size args
2320 size (PCase fc trm bdy) = 1 + size trm + size bdy
2321 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2322 size (PTrue fc _) = 1
2323 size (PResolveTC fc) = 1
2324 size (PRewrite fc by left right _) = 1 + size left + size right
2325 size (PPair fc _ _ left right) = 1 + size left + size right
2326 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2327 size (PAlternative _ a alts) = 1 + size alts
2328 size (PHidden hidden) = size hidden
2329 size (PUnifyLog tm) = size tm
2330 size (PDisamb _ tm) = size tm
2331 size (PNoImplicits tm) = size tm
2333 size (PUniverse _ _) = 1
2334 size (PConstant fc const) = 1 + size fc + size const
2335 size Placeholder = 1
2336 size (PDoBlock dos) = 1 + size dos
2337 size (PIdiom fc term) = 1 + size term
2338 size (PMetavar _ name) = 1
2339 size (PProof tactics) = size tactics
2340 size (PElabError err) = size err
2341 size PImpossible = 1
2344getPArity :: PTerm -> Int
2345getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2348-- Return all names, free or globally bound, in the given term.
2350allNamesIn :: PTerm -> [Name]
2351allNamesIn tm = nub $ ni 0 [] tm
2352 where -- TODO THINK added niTacImp, but is it right?
2353 ni 0 env (PRef _ _ n)
2354 | not (n `elem` env) = [n]
2355 ni 0 env (PPatvar _ n) = [n]
2356 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2357 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2358 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2359 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2360 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2361 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2362 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2363 ni 0 env (PHidden tm) = ni 0 env tm
2364 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2365 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2366 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2367 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2368 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2369 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2370 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2371 ni 0 env (PUnifyLog tm) = ni 0 env tm
2372 ni 0 env (PDisamb _ tm) = ni 0 env tm
2373 ni 0 env (PNoImplicits tm) = ni 0 env tm
2375 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2376 ni i env (PUnquote tm) = ni (i - 1) env tm
2377 ni i env tm = concatMap (ni i env) (children tm)
2379 niTacImp i env (TacImp _ _ scr) = ni i env scr
2383-- Return all names defined in binders in the given term
2384boundNamesIn :: PTerm -> [Name]
2385boundNamesIn tm = S.toList (ni 0 S.empty tm)
2386 where -- TODO THINK Added niTacImp, but is it right?
2387 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2388 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2389 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2390 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2391 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2392 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2393 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2394 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2395 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2396 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2397 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2398 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2399 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2400 ni 0 set (PAlternative ns a as) = niTms 0 set as
2401 ni 0 set (PHidden tm) = ni 0 set tm
2402 ni 0 set (PUnifyLog tm) = ni 0 set tm
2403 ni 0 set (PDisamb _ tm) = ni 0 set tm
2404 ni 0 set (PNoImplicits tm) = ni 0 set tm
2406 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2407 ni i set (PUnquote tm) = ni (i - 1) set tm
2409 ni i set tm = foldr (S.union . ni i set) set (children tm)
2411 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2412 niTms i set [] = set
2413 niTms i set (x : xs) = niTms i (ni i set x) xs
2415 niTacImp i set (TacImp _ _ scr) = ni i set scr
2416 niTacImp i set _ = set
2418-- Return names which are valid implicits in the given term (type).
2419implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2420implicitNamesIn uvars ist tm
2421 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2424 addImp n = do (imps, fns) <- get
2426 addFn n = do (imps, fns) <- get
2430 notCAF (PExp _ _ _ _ : _) = True
2431 notCAF (_ : xs) = notCAF xs
2433 notHidden (n, _) = case getAccessibility n of
2439 = case lookupDefAccExact n False (tt_ctxt ist) of
2443 ni 0 env (PRef _ _ n@(NS _ _))
2444 | not (n `elem` env)
2445 -- Never implicitly bind if there's a namespace
2447 ni 0 env (PRef _ _ n)
2448 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2449 ni 0 env (PApp _ f@(PRef _ _ n) as)
2450 | n `elem` uvars = do ni 0 env f
2451 mapM_ (ni 0 env . getTm) as
2452 | otherwise = do case lookupTy n (tt_ctxt ist) of
2455 mapM_ (ni 0 env . getTm) as
2456 ni 0 env (PApp _ f as) = do ni 0 env f
2457 mapM_ (ni 0 env . getTm) as
2458 ni 0 env (PAppBind _ f as) = do ni 0 env f
2459 mapM_ (ni 0 env . getTm) as
2460 ni 0 env (PCase _ c os) = do ni 0 env c
2461 -- names in 'os', not counting the names bound in the cases
2462 mapM_ (ni 0 env . snd) os
2465 mapM_ (ni 0 env . fst) os
2467 put (nub imps \\ nub impsfst, fns)
2468 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2469 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2470 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2471 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2472 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2473 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2474 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2475 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2478 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2479 ni 0 env (PHidden tm) = ni 0 env tm
2480 ni 0 env (PUnifyLog tm) = ni 0 env tm
2481 ni 0 env (PDisamb _ tm) = ni 0 env tm
2482 ni 0 env (PNoImplicits tm) = ni 0 env tm
2484 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2485 maybe (return ()) (ni i env) ty
2486 ni i env (PUnquote tm) = ni (i - 1) env tm
2488 ni i env tm = mapM_ (ni i env) (children tm)
2490-- Return names which are free in the given term.
2491namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2492namesIn uvars ist tm = nub $ ni 0 [] tm
2494 ni 0 env (PRef _ _ n)
2495 | not (n `elem` env)
2496 = case lookupTy n (tt_ctxt ist) of
2498 _ -> [n | n `elem` (map fst uvars)]
2499 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2500 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2501 ni 0 env (PCase _ c os) = ni 0 env c ++
2502 -- names in 'os', not counting the names bound in the cases
2503 (nub (concatMap (ni 0 env . snd) os)
2504 \\ nub (concatMap (ni 0 env . fst) os))
2505 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2506 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2507 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2508 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2509 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2510 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2511 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2512 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2513 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2514 ni 0 env (PHidden tm) = ni 0 env tm
2515 ni 0 env (PUnifyLog tm) = ni 0 env tm
2516 ni 0 env (PDisamb _ tm) = ni 0 env tm
2517 ni 0 env (PNoImplicits tm) = ni 0 env tm
2519 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2520 ni i env (PUnquote tm) = ni (i - 1) env tm
2522 ni i env tm = concatMap (ni i env) (children tm)
2524 niTacImp i env (TacImp _ _ scr) = ni i env scr
2527-- Return which of the given names are used in the given term.
2529usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2530usedNamesIn vars ist tm = nub $ ni 0 [] tm
2531 where -- TODO THINK added niTacImp, but is it right?
2532 ni 0 env (PRef _ _ n)
2533 | n `elem` vars && not (n `elem` env)
2534 = case lookupDefExact n (tt_ctxt ist) of
2537 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2538 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2539 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2540 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2541 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2542 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2543 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2544 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2545 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2546 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2547 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2548 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2549 ni 0 env (PHidden tm) = ni 0 env tm
2550 ni 0 env (PUnifyLog tm) = ni 0 env tm
2551 ni 0 env (PDisamb _ tm) = ni 0 env tm
2552 ni 0 env (PNoImplicits tm) = ni 0 env tm
2554 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2555 ni i env (PUnquote tm) = ni (i - 1) env tm
2557 ni i env tm = concatMap (ni i env) (children tm)
2559 niTacImp i env (TacImp _ _ scr) = ni i env scr
2562-- Return the list of inaccessible (= dotted) positions for a name.
2563getErasureInfo :: IState -> Name -> [Int]
2564getErasureInfo ist n =
2565 case lookupCtxtExact n (idris_optimisation ist) of
2566 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