2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
9{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}
11module Idris.AbsSyntaxTree where
13import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.Evaluate
16import Idris.Docstrings
17import IRTS.CodegenCommon
19import Util.DynamicLinker
26import Prelude hiding (Foldable, Traversable, (<$>))
28import Control.Applicative ((<|>))
29import qualified Control.Monad.Trans.Class as Trans (lift)
30import Control.Monad.Trans.Except
31import Control.Monad.Trans.State.Strict
33import Data.Data (Data)
35import Data.Foldable (Foldable)
36import Data.Function (on)
37import Data.Generics.Uniplate.Data (children, universe)
38import Data.List hiding (group)
39import qualified Data.Map.Strict as M
40import Data.Maybe (mapMaybe, maybeToList)
41import qualified Data.Set as S
42import qualified Data.Text as T
43import Data.Traversable (Traversable)
45import GHC.Generics (Generic)
46import Network.Socket (PortNumber)
49data ElabWhat = ETypes | EDefns | EAll
52-- | Data to pass to recursively called elaborators; e.g. for where blocks,
53-- paramaterised declarations, etc.
55-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
56-- so that we can have mutually recursive elaborators in separate modules without
57-- having to muck about with cyclic modules.
58data ElabInfo = EInfo {
59 params :: [(Name, PTerm)]
60 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
61 , liftname :: Name -> Name
62 , namespace :: [String]
64 , constraintNS :: String -- ^ filename for adding to constraint variables
66 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
67 -- | We may, recursively, collect transformations to do on the rhs,
68 -- e.g. rewriting recursive calls to functions defined by 'with'
69 , rhs_trans :: PTerm -> PTerm
70 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
74toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
76toplevelWith :: String -> ElabInfo
77toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
79eInfoNames :: ElabInfo -> [Name]
80eInfoNames info = map fst (params info) ++ M.keys (inblock info)
82data IOption = IOption {
84 , opt_logcats :: [LogCat] -- ^ List of logging categories.
85 , opt_typecase :: Bool
86 , opt_typeintype :: Bool
87 , opt_coverage :: Bool
88 , opt_showimp :: Bool -- ^ show implicits
89 , opt_errContext :: Bool
92 , opt_nobanner :: Bool
94 , opt_codegen :: Codegen
95 , opt_outputTy :: OutputType
96 , opt_ibcsubdir :: FilePath
97 , opt_importdirs :: [FilePath]
98 , opt_sourcedirs :: [FilePath]
99 , opt_triple :: String
101 , opt_cmdline :: [Opt] -- ^ remember whole command line
102 , opt_origerr :: Bool
103 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
104 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
105 , opt_optimise :: [Optimisation]
106 , opt_printdepth :: Maybe Int
107 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
108 , opt_desugarnats :: Bool
109 , opt_autoimpls :: Bool
110 } deriving (Show, Eq, Generic)
112defaultOpts :: IOption
113defaultOpts = IOption { opt_logLevel = 0
115 , opt_typecase = False
116 , opt_typeintype = False
117 , opt_coverage = True
118 , opt_showimp = False
119 , opt_errContext = False
122 , opt_nobanner = False
124 , opt_codegen = Via IBCFormat "c"
125 , opt_outputTy = Executable
127 , opt_importdirs = []
128 , opt_sourcedirs = []
132 , opt_origerr = False
133 , opt_autoSolve = True
134 , opt_autoImport = []
135 , opt_optimise = defaultOptimise
136 , opt_printdepth = Just 5000
137 , opt_evaltypes = True
138 , opt_desugarnats = False
139 , opt_autoimpls = True
142data PPOption = PPOption {
143 ppopt_impl :: Bool -- ^ whether to show implicits
144 , ppopt_desugarnats :: Bool
145 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
146 , ppopt_depth :: Maybe Int
149data Optimisation = PETransform -- ^ partial eval and associated transforms
150 deriving (Show, Eq, Generic)
152defaultOptimise :: [Optimisation]
155-- | Pretty printing options with default verbosity.
156defaultPPOption :: PPOption
157defaultPPOption = PPOption {
159 , ppopt_desugarnats = False
160 , ppopt_pinames = False
161 , ppopt_depth = Nothing
164-- | Pretty printing options with the most verbosity.
165verbosePPOption :: PPOption
166verbosePPOption = PPOption {
168 , ppopt_desugarnats = True
169 , ppopt_pinames = True
170 , ppopt_depth = Nothing
173-- | Get pretty printing options from the big options record.
174ppOption :: IOption -> PPOption
175ppOption opt = PPOption {
176 ppopt_impl = opt_showimp opt
177 , ppopt_pinames = False
178 , ppopt_depth = opt_printdepth opt
179 , ppopt_desugarnats = opt_desugarnats opt
182-- | Get pretty printing options from an idris state record.
183ppOptionIst :: IState -> PPOption
184ppOptionIst = ppOption . idris_options
186data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
187 | DSLNotation | ElabReflection | FCReflection
189 deriving (Show, Eq, Read, Ord, Generic)
191-- | The output mode in use
192data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
193 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
196-- | How wide is the console?
197data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
198 | ColsWide Int -- ^ Manually specified - must be positive
199 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
200 deriving (Show, Eq, Generic)
202-- | If a function has no totality annotation, what do we assume?
203data DefaultTotality = DefaultCheckingTotal -- ^ Total
204 | DefaultCheckingPartial -- ^ Partial
205 | DefaultCheckingCovering -- ^Total coverage, but may diverge
206 deriving (Show, Eq, Generic)
208-- | Configuration options for interactive editing.
209data InteractiveOpts = InteractiveOpts {
210 interactiveOpts_indentWith :: Int
211 , interactiveOpts_indentClause :: Int
212} deriving (Show, Generic)
214-- | The global state used in the Idris monad
215data IState = IState {
216 tt_ctxt :: Context -- ^ All the currently defined names and their terms
217 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
218 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
219 , idris_implicits :: Ctxt [PArg]
220 , idris_statics :: Ctxt [Bool]
221 , idris_interfaces :: Ctxt InterfaceInfo
222 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
223 , idris_records :: Ctxt RecordInfo
224 , idris_dsls :: Ctxt DSL
225 , idris_optimisation :: Ctxt OptInfo
226 , idris_datatypes :: Ctxt TypeInfo
227 , idris_namehints :: Ctxt [Name]
229 -- | list of lhs/rhs, and a list of missing clauses. These are not
231 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
232 , idris_flags :: Ctxt [FnOpt]
233 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
234 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
236 -- | module documentation is saved in a special MN so the context
237 -- mechanism can be used for disambiguation.
238 , idris_moduledocs :: Ctxt (Docstring DocTerm)
239 , idris_tyinfodata :: Ctxt TIData
240 , idris_fninfo :: Ctxt FnInfo
241 , idris_transforms :: Ctxt [(Term, Term)]
242 , idris_autohints :: Ctxt [Name]
243 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
244 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
245 , idris_totcheckfail :: [(FC, String)]
246 , idris_options :: IOption
248 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
250 -- | The currently defined but not proven metavariables. The Int is
251 -- the number of vars to display as a context, the Maybe Name is its
252 -- top-level function, the [Name] is the list of local variables
253 -- available for proof search and the Bools are whether :p is
254 -- allowed, and whether the variable is definable at all
255 -- (Metavariables are not definable if they are applied in a term
256 -- which still has hole bindings)
257 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
258 , idris_coercions :: [Name]
259 , idris_errRev :: [(Term, Term)]
260 , idris_errReduce :: [Name]
261 , syntax_rules :: SyntaxRules
262 , syntax_keywords :: [String]
263 , imported :: [FilePath] -- ^ The imported modules
264 , idris_scprims :: [(Name, (Int, PrimFn))]
265 , idris_objs :: [(Codegen, FilePath)]
266 , idris_libs :: [(Codegen, String)]
267 , idris_cgflags :: [(Codegen, String)]
268 , idris_hdrs :: [(Codegen, String)]
269 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
270 , proof_list :: [(Name, (Bool, [String]))]
271 , errSpan :: Maybe FC
272 , parserWarnings :: [(FC, Err)]
273 , lastParse :: Maybe Name
274 , indent_stack :: [Int]
275 , brace_stack :: [Maybe Int]
276 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
277 , idris_parsedSpan :: Maybe FC
278 , hide_list :: Ctxt Accessibility
279 , default_access :: Accessibility
280 , default_total :: DefaultTotality
281 , ibc_write :: [IBCWrite]
282 , compiled_so :: Maybe String
283 , idris_dynamic_libs :: [DynamicLib]
284 , idris_language_extensions :: [LanguageExt]
285 , idris_outputmode :: OutputMode
286 , idris_colourRepl :: Bool
287 , idris_colourTheme :: ColourTheme
288 , idris_errorhandlers :: [Name] -- ^ Global error handlers
289 , idris_nameIdx :: (Int, Ctxt (Int, Name))
290 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
291 , module_aliases :: M.Map [T.Text] [T.Text]
292 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
293 , idris_postulates :: S.Set Name
294 , idris_externs :: S.Set (Name, Int)
295 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
297 -- | List of names that were defined in the repl, and can be re-/un-defined
298 , idris_repl_defs :: [Name]
300 -- | Stack of names currently being elaborated, Bool set if it's an
301 -- implementation (implementations appear twice; also as a function name)
302 , elab_stack :: [(Name, Bool)]
305 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
306 , idris_exports :: [Name] -- ^ Functions with ExportList
307 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
308 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
309 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
310 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
311 , idris_ttstats :: M.Map Term (Int, Term)
312 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
313 , idris_interactiveOpts :: InteractiveOpts
316-- Required for parsers library, and therefore trifecta
317instance Show IState where
318 show = const "{internal state}"
320data SizeChange = Smaller | Same | Bigger | Unknown
321 deriving (Show, Eq, Generic)
323deriving instance Binary SizeChange
326type SCGEntry = (Name, [Maybe (Int, SizeChange)])
327type UsageReason = (Name, Int) -- fn_name, its_arg_number
329data CGInfo = CGInfo {
330 calls :: [Name] -- Immediate calls
331 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
333 , usedpos :: [(Int, [UsageReason])]
334 } deriving (Show, Generic)
336deriving instance Binary CGInfo
340primDefs = [ sUN "unsafePerformPrimIO"
341 , sUN "mkLazyForeignPrim"
342 , sUN "mkForeignPrim"
344 , sUN "assert_unreachable"
348-- information that needs writing for the current module's .ibc file
349data IBCWrite = IBCFix FixDecl
354 | IBCImplementation Bool Bool Name Name
361 | IBCImport (Bool, FilePath) -- ^ True = import public
362 | IBCImportDir FilePath
363 | IBCSourceDir FilePath
364 | IBCObj Codegen FilePath
365 | IBCLib Codegen String
366 | IBCCGFlag Codegen String
368 | IBCHeader Codegen String
369 | IBCAccess Name Accessibility
370 | IBCMetaInformation Name MetaInformation
371 | IBCTotal Name Totality
372 | IBCInjective Name Injectivity
374 | IBCFnInfo Name FnInfo
375 | IBCTrans Name (Term, Term)
376 | IBCErrRev (Term, Term)
381 | IBCDef Name -- ^ The main context.
382 | IBCNameHint (Name, Name)
383 | IBCLineApp FilePath Int PTerm
384 | IBCErrorHandler Name
385 | IBCFunctionErrorHandler Name Name Name
387 | IBCExtern (Name, Int)
388 | IBCTotCheckErr FC String
390 | IBCModDocs Name -- ^ The name is the special name used to track module docs
391 | IBCUsage (Name, Int)
393 | IBCAutoHint Name Name
394 | IBCDeprecate Name String
395 | IBCFragile Name String
396 | IBCConstraint FC UConstraint
397 deriving (Show, Generic)
399initialInteractiveOpts :: InteractiveOpts
400initialInteractiveOpts = InteractiveOpts {
401 interactiveOpts_indentWith = 2
402 , interactiveOpts_indentClause = 2
405-- | The initial state for the compiler
407idrisInit = IState initContext S.empty []
408 emptyContext emptyContext emptyContext [] emptyContext
409 emptyContext emptyContext emptyContext emptyContext
410 emptyContext emptyContext emptyContext emptyContext
411 emptyContext emptyContext emptyContext emptyContext
413 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
414 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
415 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
416 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
417 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
420-- | The monad for the main REPL - reading and processing files and
421-- updating global state (hence the IO inner monad).
424-- type Idris = WriterT [Either String (IO ())] (State IState a))
427type Idris = StateT IState (ExceptT Err IO)
429catchError :: Idris a -> (Err -> Idris a) -> Idris a
430catchError = liftCatch catchE
432throwError :: Err -> Idris a
433throwError = Trans.lift . throwE
435-- Commands in the REPL
437data Codegen = Via IRFormat String
439 deriving (Show, Eq, Generic)
441data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
443data HowMuchDocs = FullDocs | OverviewDocs
445data OutputFmt = HTMLOutput | LaTeXOutput
447-- | Recognised logging categories for the Idris compiler.
449-- @TODO add in sub categories.
456 deriving (Show, Eq, Ord, Generic)
458strLogCat :: LogCat -> String
459strLogCat IParse = "parser"
460strLogCat IElab = "elab"
461strLogCat ICodeGen = "codegen"
462strLogCat IErasure = "erasure"
463strLogCat ICoverage = "coverage"
464strLogCat IIBC = "ibc"
466codegenCats :: [LogCat]
467codegenCats = [ICodeGen]
469parserCats :: [LogCat]
475loggingCatsStr :: String
476loggingCatsStr = unlines
479 , (strLogCat ICodeGen)
480 , (strLogCat IErasure)
481 , (strLogCat ICoverage)
486data ElabShellCmd = EQED
494 | EDocStr (Either Name Const)
497data Opt = Filename String
514 | NoBuiltins -- only for the really primitive stuff!
531 | Port REPLPort -- ^ REPL TCP port
540 | PkgDocBuild String -- IdrisDoc
541 | PkgDocInstall String
551 | OutputTy OutputType
552 | Extension LanguageExt
553 | InterpretScript String
555 | TargetTriple String
558 | AddOpt Optimisation
559 | RemoveOpt Optimisation
562 | AutoWidth -- ^ Automatically adjust terminal width
563 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
564 | UseConsoleWidth ConsoleWidth
567 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
568 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
569 deriving (Show, Eq, Generic)
571data REPLPort = DontListen | ListenPort PortNumber
572 deriving (Eq, Generic, Show)
574-- Parsed declarations
576data Fixity = Infixl { prec :: Int }
577 | Infixr { prec :: Int }
578 | InfixN { prec :: Int }
579 | PrefixN { prec :: Int }
580 deriving (Eq, Generic)
582deriving instance Binary Fixity
585instance Show Fixity where
586 show (Infixl i) = "infixl " ++ show i
587 show (Infixr i) = "infixr " ++ show i
588 show (InfixN i) = "infix " ++ show i
589 show (PrefixN i) = "prefix " ++ show i
591data FixDecl = Fix Fixity String
592 deriving (Eq, Generic)
594instance Show FixDecl where
595 show (Fix f s) = show f ++ " " ++ s
598deriving instance Binary FixDecl
601instance Ord FixDecl where
602 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
605data Static = Static | Dynamic
606 deriving (Show, Eq, Ord, Data, Generic, Typeable)
608deriving instance Binary Static
611-- ^ Mark bindings with their explicitness, and laziness
612data Plicity = Imp { pargopts :: [ArgOpt]
615 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
616 , pinsource :: Bool -- ^ Explicitly written in source
619 | Exp { pargopts :: [ArgOpt]
621 , pparam :: Bool -- ^ this is a param (rather than index)
624 | Constraint { pargopts :: [ArgOpt]
628 | TacImp { pargopts :: [ArgOpt]
633 deriving (Show, Eq, Ord, Data, Generic, Typeable)
636deriving instance Binary Plicity
639is_scoped :: Plicity -> Maybe ImplicitInfo
640is_scoped (Imp _ _ _ s _ _) = s
645impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
646-- Machine generated top level implicit
648impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
652forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
653forall_constraint :: Plicity
654forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
657expl = Exp [] Dynamic False RigW
659expl_param = Exp [] Dynamic True RigW
662constraint = Constraint [] Static RigW
664tacimpl :: PTerm -> Plicity
665tacimpl t = TacImp [] Dynamic t RigW
667data FnOpt = Inlinable -- ^ always evaluate when simplifying
668 | TotalFn | PartialFn | CoveringFn
669 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
672 -- | interface dictionary, eval only when a function
673 -- argument, and further evaluation results.
675 | OverlappingDictionary -- ^ Interface dictionary which may overlap
676 | Implicit -- ^ implicit coercion
677 | NoImplicit -- ^ do not apply implicit coercions
678 | CExport String -- ^ export, with a C name
679 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
680 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
681 | ErrorReduce -- ^ unfold definition before showing an error
682 | Reflection -- ^ a reflecting function, compile-time only
683 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
684 | Constructor -- ^ Data constructor type
685 | AutoHint -- ^ use in auto implicit search
686 | PEGenerated -- ^ generated by partial evaluator
687 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
688 deriving (Show, Eq, Generic)
690deriving instance Binary FnOpt
695inlinable :: FnOpts -> Bool
696inlinable = elem Inlinable
698dictionary :: FnOpts -> Bool
699dictionary = elem Dictionary
702-- | Type provider - what to provide
703data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
704 | ProvPostulate t -- ^ goal type must be Type, so only term
705 deriving (Show, Eq, Functor, Generic)
707type ProvideWhat = ProvideWhat' PTerm
709-- | Top-level declarations such as compiler directives, definitions,
710-- datatypes and interfaces.
712 -- | Fixity declaration
713 = PFix FC Fixity [String]
714 -- | Type declaration (last FC is precise name location)
715 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
716 -- | Postulate, second FC is precise name location
717 | PPostulate Bool -- external def if true
718 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
720 | PClauses FC FnOpts Name [PClause' t]
721 -- | Top level constant
723 -- | Data declaration.
724 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
726 | PParams FC [(Name, t)] [PDecl' t]
727 -- | Open block/declaration
728 | POpenInterfaces FC [Name] [PDecl' t]
729 -- | New namespace, where FC is accurate location of the namespace
731 | PNamespace String FC [PDecl' t]
733 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
735 FC -- Record name precise location
736 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
737 [(Name, Docstring (Either Err t))] -- Param Docs
738 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
739 (Maybe (Name, FC)) -- Optional constructor name and location
740 (Docstring (Either Err t)) -- Constructor doc
741 SyntaxInfo -- Constructor SyntaxInfo
743 -- | Interface: arguments are documentation, syntax info, source
744 -- location, constraints, interface name, interface name location,
745 -- parameters, method declarations, optional constructor name
746 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
747 [(Name, t)] -- constraints
748 Name -- interface name
749 FC -- accurate location of interface name
750 [(Name, FC, t)] -- parameters and precise locations
751 [(Name, Docstring (Either Err t))] -- parameter docstrings
752 [(Name, FC)] -- determining parameters and precise locations
753 [PDecl' t] -- declarations
754 (Maybe (Name, FC)) -- implementation constructor name and location
755 (Docstring (Either Err t)) -- implementation constructor docs
757 -- | Implementation declaration: arguments are documentation, syntax
758 -- info, source location, constraints, interface name, parameters, full
759 -- Implementation type, optional explicit name, and definitions
760 | PImplementation (Docstring (Either Err t)) -- Implementation docs
761 [(Name, Docstring (Either Err t))] -- Parameter docs
763 FC [(Name, t)] -- constraints
764 [Name] -- parent dictionaries to search for constraints
768 FC -- precise location of interface
770 [(Name, t)] -- Extra names in scope in the body
771 t -- full Implementation type
772 (Maybe Name) -- explicit name
774 | PDSL Name (DSL' t) -- ^ DSL declaration
775 | PSyntax FC Syntax -- ^ Syntax definition
776 | PMutual FC [PDecl' t] -- ^ Mutual block
777 | PDirective Directive -- ^ Compiler directive.
779 -- | Type provider. The first t is the type, the second is the
780 -- term. The second FC is precise highlighting location.
781 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
783 -- | Source-to-source transformation rule. If bool is True, lhs and
784 -- rhs must be convertible.
785 | PTransform FC Bool t t
787 -- | FC is decl-level, for errors, and Strings represent the
789 | PRunElabDecl FC t [String]
790 deriving (Functor, Generic)
792deriving instance Binary PDecl'
795-- | The set of source directives
796data Directive = DLib Codegen String
797 | DLink Codegen String
798 | DFlag Codegen String
799 | DInclude Codegen String
804 | DSetTotal Name -- assert totality after checking
805 | DAccess Accessibility
806 | DDefault DefaultTotality
808 | DDynamicLibs [String]
809 | DNameHint Name FC [(Name, FC)]
810 | DErrorHandlers Name FC Name FC [(Name, FC)]
811 | DLanguage LanguageExt
812 | DDeprecate Name String
813 | DFragile Name String
814 | DAutoImplicits Bool
818-- | A set of instructions for things that need to happen in IState
819-- after a term elaboration when there's been reflected elaboration.
820data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
821 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
822 | RAddImplementation Name Name
823 | RDatatypeDeclInstrs Name [PArg]
824 -- | Datatype, constructors
825 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
828-- | For elaborator state
829data EState = EState {
830 case_decls :: [(Name, PDecl)]
831 , delayed_elab :: [(Int, Elab' EState ())]
832 , new_tyDecls :: [RDeclInstructions]
833 , highlighting :: [(FC, OutputAnnotation)]
834 , auto_binds :: [Name] -- ^ names bound as auto implicits
835 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
839initEState = EState [] [] [] [] [] []
841type ElabD a = Elab' EState a
843highlightSource :: FC -> OutputAnnotation -> ElabD ()
844highlightSource fc annot =
845 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
847-- | One clause of a top-level definition. Term arguments to constructors are:
849-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
851-- 2. The list of extra 'with' patterns
853-- 3. The right-hand side
855-- 4. The where block (PDecl' t)
857data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
858 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
859 | PClauseR FC [t] t [PDecl' t]
860 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
861 deriving (Functor, Generic)
863deriving instance Binary PClause'
868 -- | Data declaration
869 PDatadecl { d_name :: Name -- ^ The name of the datatype
870 , d_name_fc :: FC -- ^ The precise location of the type constructor name
871 , d_tcon :: t -- ^ Type constructor
872 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
874 -- | "Placeholder" for data whose constructors are defined later
875 | PLaterdecl { d_name :: Name
878 } deriving (Functor, Generic)
880-- | Transform the FCs in a PData and its associated terms. The first
881-- function transforms the general-purpose FCs, and the second
882-- transforms those that are used for semantic source highlighting, so
883-- they can be treated specially.
884mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
885mapPDataFC f g (PDatadecl n nfc tycon ctors) =
886 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
887 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
888 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
889mapPDataFC f g (PLaterdecl n nfc tycon) =
890 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
892deriving instance Binary PData'
895-- Handy to get a free function for applying PTerm -> PTerm functions
896-- across a program, by deriving Functor
898type PDecl = PDecl' PTerm
899type PData = PData' PTerm
900type PClause = PClause' PTerm
902-- | Transform the FCs in a PTerm. The first function transforms the
903-- general-purpose FCs, and the second transforms those that are used
904-- for semantic source highlighting, so they can be treated specially.
905mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
906mapPDeclFC f g (PFix fc fixity ops) =
907 PFix (f fc) fixity ops
908mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
909 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
910mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
911 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
913mapPDeclFC f g (PClauses fc opts n clauses) =
914 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
915mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
916mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
917 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
918mapPDeclFC f g (PParams fc params decls) =
920 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
921 (map (mapPDeclFC f g) decls)
922mapPDeclFC f g (POpenInterfaces fc ifs decls) =
923 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
924mapPDeclFC f g (PNamespace ns fc decls) =
925 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
926mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
927 PRecord doc syn (f fc) opts n (g nfc)
928 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
930 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
931 plic, mapPTermFC f g ty, fdoc))
933 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
936mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
937 PInterface doc syn (f fc)
938 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
939 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
940 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
941 (map (mapPDeclFC f g) body)
942 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
944mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
945 PImplementation doc paramDocs syn (f fc)
946 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
947 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
948 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
949 (mapPTermFC f g implTy)
951 (map (mapPDeclFC f g) body)
952mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
953mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
955 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
956 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
957mapPDeclFC f g (PMutual fc decls) =
958 PMutual (f fc) (map (mapPDeclFC f g) decls)
959mapPDeclFC f g (PDirective d) =
962 DNameHint n nfc ns ->
963 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
964 DErrorHandlers n nfc n' nfc' ns ->
965 DErrorHandlers n (g nfc) n' (g nfc') $
966 map (\(an, anfc) -> (an, g anfc)) ns
967mapPDeclFC f g (PProvider doc syn fc nfc what n) =
968 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
969mapPDeclFC f g (PTransform fc safe l r) =
970 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
971mapPDeclFC f g (PRunElabDecl fc script ns) =
972 PRunElabDecl (f fc) (mapPTermFC f g script) ns
974-- | Get all the names declared in a declaration
975declared :: PDecl -> [Name]
976declared (PFix _ _ _) = []
977declared (PTy _ _ _ _ _ n fc t) = [n]
978declared (PPostulate _ _ _ _ _ _ n t) = [n]
979declared (PClauses _ _ n _) = [] -- not a declaration
980declared (PCAF _ n _) = [n]
981declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
982 where fstt (_, _, a, _, _, _, _) = a
983declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
984declared (PParams _ _ ds) = concatMap declared ds
985declared (POpenInterfaces _ _ ds) = concatMap declared ds
986declared (PNamespace _ _ ds) = concatMap declared ds
987declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
988declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
989declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
993declared (PDSL n _) = [n]
994declared (PSyntax _ _) = []
995declared (PMutual _ ds) = concatMap declared ds
996declared (PDirective _) = []
999-- get the names declared, not counting nested parameter blocks
1000tldeclared :: PDecl -> [Name]
1001tldeclared (PFix _ _ _) = []
1002tldeclared (PTy _ _ _ _ _ n _ t) = [n]
1003tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
1004tldeclared (PClauses _ _ n _) = [] -- not a declaration
1005tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1006tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1007 where fstt (_, _, a, _, _, _, _) = a
1008tldeclared (PParams _ _ ds) = []
1009tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
1010tldeclared (PMutual _ ds) = concatMap tldeclared ds
1011tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
1012tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
1013tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1019defined :: PDecl -> [Name]
1020defined (PFix _ _ _) = []
1021defined (PTy _ _ _ _ _ n _ t) = []
1022defined (PPostulate _ _ _ _ _ _ n t) = []
1023defined (PClauses _ _ n _) = [n] -- not a declaration
1024defined (PCAF _ n _) = [n]
1025defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1026 where fstt (_, _, a, _, _, _, _) = a
1027defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1028defined (PParams _ _ ds) = concatMap defined ds
1029defined (POpenInterfaces _ _ ds) = concatMap defined ds
1030defined (PNamespace _ _ ds) = concatMap defined ds
1031defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1032defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1033defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1037defined (PDSL n _) = [n]
1038defined (PSyntax _ _) = []
1039defined (PMutual _ ds) = concatMap defined ds
1040defined (PDirective _) = []
1043updateN :: [(Name, Name)] -> Name -> Name
1044updateN ns n | Just n' <- lookup n ns = n'
1047updateNs :: [(Name, Name)] -> PTerm -> PTerm
1049updateNs ns t = mapPT updateRef t
1050 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1053-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1054-- updateDNs [] t = t
1055-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1056-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1057-- where updateCNs ns (PClause n l ts r ds)
1058-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1059-- (map (fmap (updateNs ns)) ts)
1060-- (fmap (updateNs ns) r)
1061-- (map (updateDNs ns) ds)
1062-- updateDNs ns c = c
1064data PunInfo = IsType
1067 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1069-- | High level language terms
1070data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1071 -- high-level language
1073 -- ^ A reference to a variable. The FC is its precise
1074 -- source location for highlighting. The list of FCs is a
1075 -- collection of additional highlighting locations.
1076 | PInferRef FC [FC] Name -- ^ A name to be defined later
1077 | PPatvar FC Name -- ^ A pattern variable
1078 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1079 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1080 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1081 | PTyped PTerm PTerm -- ^ Term with explicit type
1082 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1083 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1084 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1085 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1086 | PMatchApp FC Name -- ^ Make an application by type matching
1087 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1088 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1089 | PTrue FC PunInfo -- ^ Unit type..?
1090 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1091 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1092 -- ^ "rewrite" syntax, with optional rewriting function and
1093 -- optional result type
1094 | PPair FC [FC] PunInfo PTerm PTerm
1095 -- ^ A pair (a, b) and whether it's a product type or a
1096 -- pair (solved by elaboration). The list of FCs is its
1098 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1099 -- ^ A dependent pair (tm : a ** b) and whether it's a
1100 -- sigma type or a pair that inhabits one (solved by
1101 -- elaboration). The [FC] is its punctuation.
1102 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1103 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1104 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1105 | PType FC -- ^ 'Type' type
1106 | PUniverse FC Universe -- ^ Some universe
1107 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1108 | PConstant FC Const -- ^ Builtin types
1109 | Placeholder -- ^ Underscore
1110 | PDoBlock [PDo] -- ^ Do notation
1111 | PIdiom FC PTerm -- ^ Idiom brackets
1112 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1113 | PProof [PTactic] -- ^ Proof script
1114 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1115 | PElabError Err -- ^ Error to report on elaboration
1116 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1117 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1118 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1119 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1120 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1121 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1122 | PUnquote PTerm -- ^ ~Term
1123 | PQuoteName Name Bool FC
1124 -- ^ `{n} where the FC is the precise highlighting for
1125 -- the name in particular. If the Bool is False, then
1126 -- it's `{{n}} and the name won't be resolved.
1127 | PRunElab FC PTerm [String]
1128 -- ^ %runElab tm - New-style proof script. Args are
1129 -- location, script, enclosing namespace.
1130 | PConstSugar FC PTerm
1131 -- ^ A desugared constant. The FC is a precise source
1132 -- location that will be used to highlight it later.
1133 deriving (Eq, Ord, Data, Typeable, Generic)
1135data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1138 deriving (Eq, Ord, Data, Generic, Typeable)
1140-- | Transform the FCs in a PTerm. The first function transforms the
1141-- general-purpose FCs, and the second transforms those that are used
1142-- for semantic source highlighting, so they can be treated specially.
1143mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1144mapPTermFC f g (PQuote q) = PQuote q
1145mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1146mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1147mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1148mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1149mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1150mapPTermFC 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)
1151mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1152mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1153mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1154mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1155mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1156mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1157mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1158mapPTermFC 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)
1159mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1160mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1161mapPTermFC 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)
1162mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1163mapPTermFC 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)
1164mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1165mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1166mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1167mapPTermFC f g (PType fc) = PType (f fc)
1168mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1169mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1170mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1171mapPTermFC f g Placeholder = Placeholder
1172mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1173 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1174 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1175 mapPDoFC (DoBindP fc t1 t2 alts) =
1176 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1177 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1178 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1179mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1180mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1181mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1182mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1183mapPTermFC f g (PElabError err) = PElabError err
1184mapPTermFC f g PImpossible = PImpossible
1185mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1186mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1187mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1188mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1189mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1190mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1191mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1192mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1193mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1196dg instance Binary PTerm
1199mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1200mapPT f t = f (mpt t) where
1201 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1202 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1203 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1204 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1205 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1206 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1207 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1208 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1209 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1210 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1211 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1212 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1213 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1214 mpt (PHidden t) = PHidden (mapPT f t)
1215 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1216 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1217 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1218 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1219 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1220 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1221 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1225data PTactic' t = Intro [Name] | Intros | Focus Name
1226 | Refine Name [Bool] | Rewrite t | DoUnify
1233 | LetTac Name t | LetTacTy Name t t
1234 | Exact t | Compute | Trivial | TCImplementation
1235 | ProofSearch Bool Bool Int (Maybe Name)
1236 [Name] -- allowed local names
1238 -- ^ the bool is whether to search recursively
1241 | ProofState | ProofTerm | Undo
1242 | Try (PTactic' t) (PTactic' t)
1243 | TSeq (PTactic' t) (PTactic' t)
1244 | ApplyTactic t -- see Language.Reflection module
1248 | GoalType String (PTactic' t)
1251 | TDocStr (Either Name Const)
1254 | TFail [ErrorReportPart]
1257 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1259deriving instance Binary PTactic'
1261instance Sized a => Sized (PTactic' a) where
1262 size (Intro nms) = 1 + size nms
1264 size (Focus nm) = 1 + size nm
1265 size (Refine nm bs) = 1 + size nm + length bs
1266 size (Rewrite t) = 1 + size t
1267 size (Induction t) = 1 + size t
1268 size (LetTac nm t) = 1 + size nm + size t
1269 size (Exact t) = 1 + size t
1277 size (Try l r) = 1 + size l + size r
1278 size (TSeq l r) = 1 + size l + size r
1279 size (ApplyTactic t) = 1 + size t
1280 size (Reflect t) = 1 + size t
1281 size (Fill t) = 1 + size t
1285 size (TFail ts) = 1 + size ts
1288 size (CaseTac x) = 1 + size x
1289 size (Equiv t) = 1 + size t
1290 size (Claim x y) = 1 + size x + size y
1292 size (MatchRefine x) = 1 + size x
1293 size (LetTacTy x y z) = 1 + size x + size y + size z
1294 size TCImplementation = 1
1296type PTactic = PTactic' PTerm
1298data PDo' t = DoExp FC t
1299 | DoBind FC Name FC t -- ^ second FC is precise name location
1300 | DoBindP FC t t [(t,t)]
1301 | DoLet FC Name FC t t -- ^ second FC is precise name location
1303 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1305deriving instance Binary PDo'
1308instance Sized a => Sized (PDo' a) where
1309 size (DoExp fc t) = 1 + size fc + size t
1310 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1311 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1312 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1313 size (DoLetP fc l r) = 1 + size fc + size l + size r
1315type PDo = PDo' PTerm
1317-- The priority gives a hint as to elaboration order. Best to elaborate
1318-- things early which will help give a more concrete type to other
1319-- variables, e.g. a before (interpTy a).
1321data PArg' t = PImp { priority :: Int
1322 , machine_inf :: Bool -- ^ true if the machine inferred it
1323 , argopts :: [ArgOpt]
1327 | PExp { priority :: Int
1328 , argopts :: [ArgOpt]
1332 | PConstraint { priority :: Int
1333 , argopts :: [ArgOpt]
1337 | PTacImplicit { priority :: Int
1338 , argopts :: [ArgOpt]
1343 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1345data ArgOpt = AlwaysShow
1349 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1351instance Sized a => Sized (PArg' a) where
1352 size (PImp p _ l nm trm) = 1 + size nm + size trm
1353 size (PExp p l nm trm) = 1 + size nm + size trm
1354 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1355 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1358deriving instance Binary PArg'
1361pimp n t mach = PImp 1 mach [] n t
1362pexp t = PExp 1 [] (sMN 0 "arg") t
1363pconst t = PConstraint 1 [] (sMN 0 "carg") t
1364ptacimp n s t = PTacImplicit 2 [] n s t
1366type PArg = PArg' PTerm
1368-- | Get the highest FC in a term, if one exists
1369highestFC :: PTerm -> Maybe FC
1370highestFC (PQuote _) = Nothing
1371highestFC (PRef fc _ _) = Just fc
1372highestFC (PInferRef fc _ _) = Just fc
1373highestFC (PPatvar fc _) = Just fc
1374highestFC (PLam fc _ _ _ _) = Just fc
1375highestFC (PPi _ _ _ _ _) = Nothing
1376highestFC (PLet fc _ _ _ _ _) = Just fc
1377highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1378highestFC (PApp fc _ _) = Just fc
1379highestFC (PAppBind fc _ _) = Just fc
1380highestFC (PMatchApp fc _) = Just fc
1381highestFC (PCase fc _ _) = Just fc
1382highestFC (PIfThenElse fc _ _ _) = Just fc
1383highestFC (PTrue fc _) = Just fc
1384highestFC (PResolveTC fc) = Just fc
1385highestFC (PRewrite fc _ _ _ _) = Just fc
1386highestFC (PPair fc _ _ _ _) = Just fc
1387highestFC (PDPair fc _ _ _ _ _) = Just fc
1388highestFC (PAs fc _ _) = Just fc
1389highestFC (PAlternative _ _ args) =
1390 case mapMaybe highestFC args of
1393highestFC (PHidden _) = Nothing
1394highestFC (PType fc) = Just fc
1395highestFC (PUniverse _ _) = Nothing
1396highestFC (PGoal fc _ _ _) = Just fc
1397highestFC (PConstant fc _) = Just fc
1398highestFC Placeholder = Nothing
1399highestFC (PDoBlock lines) =
1400 case map getDoFC lines of
1404 getDoFC (DoExp fc t) = fc
1405 getDoFC (DoBind fc nm nfc t) = fc
1406 getDoFC (DoBindP fc l r alts) = fc
1407 getDoFC (DoLet fc nm nfc l r) = fc
1408 getDoFC (DoLetP fc l r) = fc
1410highestFC (PIdiom fc _) = Just fc
1411highestFC (PMetavar fc _) = Just fc
1412highestFC (PProof _) = Nothing
1413highestFC (PTactics _) = Nothing
1414highestFC (PElabError _) = Nothing
1415highestFC PImpossible = Nothing
1416highestFC (PCoerced tm) = highestFC tm
1417highestFC (PDisamb _ opts) = highestFC opts
1418highestFC (PUnifyLog tm) = highestFC tm
1419highestFC (PNoImplicits tm) = highestFC tm
1420highestFC (PQuasiquote _ _) = Nothing
1421highestFC (PUnquote tm) = highestFC tm
1422highestFC (PQuoteName _ _ fc) = Just fc
1423highestFC (PRunElab fc _ _) = Just fc
1424highestFC (PConstSugar fc _) = Just fc
1425highestFC (PAppImpl t _) = highestFC t
1429data InterfaceInfo = CI {
1430 implementationCtorName :: Name
1431 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1432 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1433 , interface_default_super_interfaces :: [PDecl]
1434 , interface_impparams :: [Name]
1435 , interface_params :: [Name]
1436 , interface_constraints :: [PTerm]
1437 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1438 , interface_determiners :: [Int]
1439 } deriving (Show, Generic)
1441deriving instance Binary InterfaceInfo
1445data RecordInfo = RI {
1446 record_parameters :: [(Name,PTerm)]
1447 , record_constructor :: Name
1448 , record_projections :: [Name]
1449 } deriving (Show, Generic)
1451-- Type inference data
1453data TIData = TIPartial -- ^ a function with a partially defined type
1454 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1455 deriving (Show, Generic)
1457-- | Miscellaneous information about functions
1458data FnInfo = FnInfo { fn_params :: [Int] }
1459 deriving (Show, Generic)
1461deriving instance Binary FnInfo
1464data OptInfo = Optimise {
1465 inaccessible :: [(Int,Name)] -- includes names for error reporting
1466 , detaggable :: Bool
1467 , forceable :: [Int] -- argument positions which are forced by other values
1468 } deriving (Show, Generic)
1470deriving instance Binary OptInfo
1473-- | Syntactic sugar info
1478 , dsl_var :: Maybe t
1479 , index_first :: Maybe t
1480 , index_next :: Maybe t
1481 , dsl_lambda :: Maybe t
1482 , dsl_let :: Maybe t
1484 } deriving (Show, Functor, Generic)
1486deriving instance Binary DSL'
1489type DSL = DSL' PTerm
1491data SynContext = PatternSyntax
1494 deriving (Show, Generic)
1496deriving instance Binary SynContext
1499data Syntax = Rule [SSymbol] PTerm SynContext
1500 | DeclRule [SSymbol] [PDecl]
1501 deriving (Show, Generic)
1503syntaxNames :: Syntax -> [Name]
1504syntaxNames (Rule syms _ _) = mapMaybe ename syms
1505 where ename (Keyword n) = Just n
1507syntaxNames (DeclRule syms _) = mapMaybe ename syms
1508 where ename (Keyword n) = Just n
1511syntaxSymbols :: Syntax -> [SSymbol]
1512syntaxSymbols (Rule ss _ _) = ss
1513syntaxSymbols (DeclRule ss _) = ss
1515deriving instance Binary Syntax
1518data SSymbol = Keyword Name
1523 deriving (Show, Eq, Generic)
1527deriving instance Binary SSymbol
1530newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1533emptySyntaxRules :: SyntaxRules
1534emptySyntaxRules = SyntaxRules []
1536updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1537updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1539 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1544 ruleSort (s1:ss1) (s2:ss2) =
1545 case symCompare s1 s2 of
1546 EQ -> ruleSort ss1 ss2
1549 -- Better than creating Ord implementation for SSymbol since
1550 -- in general this ordering does not really make sense.
1551 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1552 symCompare (Keyword _) _ = LT
1553 symCompare (Symbol _) (Keyword _) = GT
1554 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1555 symCompare (Symbol _) _ = LT
1556 symCompare (Binding _) (Keyword _) = GT
1557 symCompare (Binding _) (Symbol _) = GT
1558 symCompare (Binding b1) (Binding b2) = compare b1 b2
1559 symCompare (Binding _) _ = LT
1560 symCompare (Expr _) (Keyword _) = GT
1561 symCompare (Expr _) (Symbol _) = GT
1562 symCompare (Expr _) (Binding _) = GT
1563 symCompare (Expr e1) (Expr e2) = compare e1 e2
1564 symCompare (Expr _) _ = LT
1565 symCompare (SimpleExpr _) (Keyword _) = GT
1566 symCompare (SimpleExpr _) (Symbol _) = GT
1567 symCompare (SimpleExpr _) (Binding _) = GT
1568 symCompare (SimpleExpr _) (Expr _) = GT
1569 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1571initDSL = DSL (PRef f [] (sUN ">>="))
1572 (PRef f [] (sUN "<*>"))
1573 (PRef f [] (sUN "pure"))
1580 where f = fileFC "(builtin)"
1582data Using = UImplicit Name PTerm
1583 | UConstraint Name [Name]
1584 deriving (Show, Eq, Data, Generic, Typeable)
1586deriving instance Binary Using
1589data SyntaxInfo = Syn {
1591 , syn_params :: [(Name, PTerm)]
1592 , syn_namespace :: [String]
1594 , imp_methods :: [Name]
1595 -- ^ interface methods. When expanding implicits, these should be
1596 -- expanded even under binders
1597 , decoration :: Name -> Name
1599 , implicitAllowed :: Bool
1600 , constraintAllowed :: Bool
1601 , maxline :: Maybe Int
1602 , mut_nesting :: Int
1604 , syn_in_quasiquote :: Int
1605 , syn_toplevel :: Bool
1606 , withAppAllowed :: Bool
1607 } deriving (Show, Generic)
1609deriving instance Binary SyntaxInfo
1612defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1614expandNS :: SyntaxInfo -> Name -> Name
1615expandNS syn n@(NS _ _) = n
1616expandNS syn n = case syn_namespace syn of
1621-- For inferring types of things
1623bi = fileFC "builtin"
1624primfc = fileFC "(primitive)"
1626inferTy = sMN 0 "__Infer"
1627inferCon = sMN 0 "__infer"
1628inferDecl = PDatadecl inferTy primfc
1630 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1631 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1632 (PRef bi [] inferTy)), bi, [])]
1635infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1636infP = P (TCon 6 0) inferTy (TType (UVal 0))
1638getInferTerm, getInferType :: Term -> Term
1639getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1640getInferTerm (App _ (App _ _ _) tm) = tm
1641getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1643getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1644 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1645 toTy (PVar _ t) = PVTy t
1647getInferType (App _ (App _ _ ty) _) = ty
1651-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1653primNames = [inferTy, inferCon]
1656unitCon = sUN "MkUnit"
1658falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1659 "The empty type, also known as the trivially false proposition." ++
1661 "Use `void` or `absurd` to prove anything if you have a variable " ++
1662 "of type `Void` in scope."
1665pairTy = sNS (sUN "Pair") ["Builtins"]
1666pairCon = sNS (sUN "MkPair") ["Builtins"]
1668upairTy = sNS (sUN "UPair") ["Builtins"]
1669upairCon = sNS (sUN "MkUPair") ["Builtins"]
1673eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1674 "The propositional equality type. A proof that `x` = `y`." ++
1676 "To use such a proof, pattern-match on it, and the two equal things will " ++
1677 "then need to be the _same_ pattern." ++
1679 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1680 "is possible to state equalities between values of potentially different " ++
1681 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1683 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1685eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1686 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1688 [(reflDoc, reflParamDoc,
1689 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1690 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1691 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1692 pimp (n "B") Placeholder False,
1693 pexp (PRef bi [] (n "x")),
1694 pexp (PRef bi [] (n "x"))])), bi, [])]
1696 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1697 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1698 "shown that both sides are in fact equal."
1699 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1700 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1702eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1703 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1709-- | The special name to be used in the module documentation context -
1710-- not for use in the main definition context. The namespace around it
1711-- will determine the module to which the docs adhere.
1713modDocName = sMN 0 "ModuleDocs"
1715-- Defined in builtins.idr
1716sigmaTy = sNS (sUN "DPair") ["Builtins"]
1717sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1719piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1720piBind = piBindp expl
1722piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1724piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1727-- Pretty-printing declarations and terms
1729-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1730-- could interfere with interactive editing, which calls "show".
1732instance Show PTerm where
1733 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1735instance Show PDecl where
1736 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1738instance Show PClause where
1739 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1741instance Show PData where
1742 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1744instance Pretty PTerm OutputAnnotation where
1745 pretty = prettyImp defaultPPOption
1747-- | Colourise annotations according to an Idris state. It ignores the
1748-- names in the annotation, as there's no good way to show extended
1749-- information on a terminal.
1750annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1751annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1752annotationColour ist (AnnConst c) =
1753 let theme = idris_colourTheme ist
1754 in Just $ if constIsType c
1755 then typeColour theme
1756 else dataColour theme
1757annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1758annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1759annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1760annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1761annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1762annotationColour ist (AnnName n _ _ _) =
1763 let ctxt = tt_ctxt ist
1764 theme = idris_colourTheme ist
1766 _ | isDConName n ctxt -> Just $ dataColour theme
1767 _ | isFnName n ctxt -> Just $ functionColour theme
1768 _ | isTConName n ctxt -> Just $ typeColour theme
1769 _ | isPostulateName n ist -> Just $ postulateColour theme
1770 _ | otherwise -> Nothing -- don't colourise unknown names
1771annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1772 where colour BoldText = IdrisColour Nothing True False True False
1773 colour UnderlineText = IdrisColour Nothing True True False False
1774 colour ItalicText = IdrisColour Nothing True False False True
1775annotationColour ist _ = Nothing
1778-- | Colourise annotations according to an Idris state. It ignores the
1779-- names in the annotation, as there's no good way to show extended
1780-- information on a terminal. Note that strings produced this way will
1781-- not be coloured on Windows, so the use of the colour rendering
1782-- functions in Idris.Output is to be preferred.
1783consoleDecorate :: IState -> OutputAnnotation -> String -> String
1784consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1786isPostulateName :: Name -> IState -> Bool
1787isPostulateName n ist = S.member n (idris_postulates ist)
1789-- | Pretty-print a high-level closed Idris term with no information
1790-- about precedence/associativity
1791prettyImp :: PPOption -- ^ pretty printing options
1792 -> PTerm -- ^ the term to pretty-print
1793 -> Doc OutputAnnotation
1794prettyImp impl = pprintPTerm impl [] [] []
1796-- | Serialise something to base64 using its Binary implementation.
1798-- | Do the right thing for rendering a term in an IState
1799prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1800prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1802-- | Pretty-print a high-level Idris term in some bindings context
1804pprintPTerm :: PPOption -- ^ pretty printing options
1805 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1806 -> [Name] -- ^ names to always show in pi, even if not used
1807 -> [FixDecl] -- ^ Fixity declarations
1808 -> PTerm -- ^ the term to pretty-print
1809 -> Doc OutputAnnotation
1810pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1815 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1816 prettySe d p bnd (PQuote r) =
1817 text "![" <> pretty r <> text "]"
1818 prettySe d p bnd (PPatvar fc n) = pretty n
1820 | Just str <- slist d p bnd e = depth d str
1821 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1822 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1823 prettySe d p bnd (PLam fc n nfc ty sc) =
1824 let (ns, sc') = getLamNames [n] sc in
1825 depth d . bracket p startPrec . group . align . hang 2 $
1826 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1827 prettySe (decD d) startPrec ((n, False):bnd) sc'
1829 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1830 getLamNames acc sc = (reverse acc, sc)
1832 prettyBindingsOf [] t = text ""
1833 prettyBindingsOf [n] t = prettyBindingOf n t
1834 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1835 prettyBindingsOf ns t
1836 prettySe d p bnd (PLet fc n nfc ty v sc) =
1837 depth d . bracket p startPrec . group . align $
1838 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1839 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1840 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1842 depth d . bracket p startPrec . group $
1843 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1844 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1846 depth d . bracket p startPrec . group $
1847 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1848 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1849 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1850 || ppopt_pinames ppo && uname n =
1851 depth d . bracket p startPrec . group $
1852 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1853 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1855 depth d . bracket p startPrec . group $
1856 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1857 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1859 uname (UN n) = case str n of
1866 Static -> text "%static" <> space
1868 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1870 depth d . bracket p startPrec $
1871 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1872 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1873 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1875 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1876 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1877 showRig _ n = prettyBindingOf n True
1881 Static -> text "%static" <> space
1883 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1884 depth d . bracket p startPrec $
1885 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1886 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1887 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1888 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1889 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1890 depth d . bracket p startPrec $
1891 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1892 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1893 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1894 | basename neg == sUN "negate" =
1895 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1896 -- This case preserves the behavior of the former constructor PEq.
1897 -- It should be removed if feasible when the pretty-printing of infix
1898 -- operators in general is improved.
1899 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1900 | n == eqTy, ppopt_impl ppo =
1901 depth d . bracket p eqPrec $
1902 enclose lparen rparen eq <+>
1903 align (group (vsep (map (prettyArgS (decD d) bnd)
1906 depth d . bracket p eqPrec . align . group $
1907 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1908 where eq = annName eqTy (text "=")
1910 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1911 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1912 | UN nm <- basename f
1913 , not (ppopt_impl ppo) && null (getShowArgs args) =
1914 prettyName True (ppopt_impl ppo) bnd f
1915 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1916 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1917 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1918 | UN nm <- basename op
1920 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1921 case getShowArgs args of
1923 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1924 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1925 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1926 (l@(PExp{}) : r@(PExp{}) : rest) ->
1927 depth d . bracket p funcAppPrec $
1928 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1929 align (group (vsep (map (prettyArgS d bnd) rest)))
1930 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1931 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1932 f = getFixity (opStr op)
1934 Nothing -> funcAppPrec + 1
1935 Just (Infixl p') -> p'
1936 Just f' -> prec f' + 1
1938 Nothing -> funcAppPrec + 1
1939 Just (Infixr p') -> p'
1940 Just f' -> prec f' + 1
1941 inFix l r = align . group $
1942 (prettySe (decD d) left bnd l <+> opName False) <$>
1943 group (prettySe (decD d) right bnd r)
1944 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1945 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1946 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1947 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1948 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1949 let args = getShowArgs as
1950 fp = prettySe (decD d) (startPrec + 1) bnd f
1951 shownArgs = if ppopt_impl ppo then as else args
1953 depth d . bracket p funcAppPrec . group $
1956 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1957 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1958 prettySe d p bnd (PCase _ scr cases) =
1959 bracket p funcAppPrec $
1960 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1961 depth d (indent 2 (vsep (map ppcase cases)))
1963 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1964 ([(n, False) | n <- vars l] ++ bnd)
1965 in nest nestingSize $
1966 prettyCase l <+> text "=>" <+> prettyCase r
1967 -- Warning: this is a bit of a hack. At this stage, we don't have the
1968 -- global context, so we can't determine which names are constructors,
1969 -- which are types, and which are pattern variables on the LHS of the
1970 -- case pattern. We use the heuristic that names without a namespace
1971 -- are patvars, because right now case blocks in PTerms are always
1972 -- delaborated from TT before being sent to the pretty-printer. If they
1973 -- start getting printed directly, THIS WILL BREAK.
1974 -- Potential solution: add a list of known patvars to the cases in
1975 -- PCase, and have the delaborator fill it out, kind of like the pun
1976 -- disambiguation on PDPair.
1977 vars tm = filter noNS (allNamesIn tm)
1978 noNS (NS _ _) = False
1981 prettySe d p bnd (PIfThenElse _ c t f) =
1982 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1983 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1984 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1985 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1987 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1988 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1989 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1990 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1991 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1992 prettySe d p bnd (PRewrite _ by l r _) =
1993 depth d . bracket p startPrec $
1994 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1997 Just fn -> text "using" <+>
1998 prettyName True (ppopt_impl ppo) bnd fn) <+>
1999 text "in" <+> prettySe (decD d) startPrec bnd r
2000 prettySe d p bnd (PTyped l r) =
2001 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
2002 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
2003 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
2004 align . group . vsep . punctuate (ann comma) $
2005 map (prettySe (decD d) startPrec bnd) elts
2006 where ann = case pun of
2008 IsType -> annName pairTy
2009 IsTerm -> annName pairCon
2010 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
2011 | Just elts <- dPairElts dpair
2012 = depth d . enclose (annotated lparen) (annotated rparen) .
2013 align . group . vsep . punctuate (space <> annotated (text "**")) $
2019 annotated (text "**") <+>
2020 prettySe (decD d) startPrec (addBinding bnd) r <>
2022 where annotated = case pun of
2023 IsType -> annName sigmaTy
2024 IsTerm -> annName sigmaCon
2027 (left, addBinding) = case (l, pun) of
2028 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
2029 _ -> (prettySe (decD d) startPrec bnd l, id)
2032 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
2033 ppElts ((PRef _ _ n, t):rs) bs
2035 = (bindingOf n False <+> colon <+>
2036 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2037 ppElts ((l, t):rs) bs
2038 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2039 prettySe d p bnd (PAlternative ns a as) =
2040 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2043 foldr ((\ l r -> l <+> text "," <+> r) .
2044 depth d . prettySe (decD d) startPrec bnd)
2046 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2047 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2048 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2049 -- XXX: add pretty for tactics
2050 prettySe d p bnd (PProof ts) =
2051 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2052 prettySe d p bnd (PTactics ts) =
2053 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2054 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2055 prettySe d p bnd PImpossible = kwd "impossible"
2056 prettySe d p bnd Placeholder = text "_"
2057 prettySe d p bnd (PDoBlock dos) =
2058 bracket p startPrec $
2059 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2060 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2061 ppdo bnd (DoBind _ bn _ tm : dos) =
2062 (prettyBindingOf bn False <+> text "<-" <+>
2063 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2064 ppdo ((bn, False):bnd) dos
2065 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2066 text "no pretty printer for pattern-matching do binding" :
2068 ppdo bnd (DoLet _ ln _ ty v : dos) =
2069 (kwd "let" <+> prettyBindingOf ln False <+>
2070 (if ty /= Placeholder
2071 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2073 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2074 ppdo ((ln, False):bnd) dos
2075 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2076 text "no pretty printer for pattern-matching do binding" :
2079 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2080 prettySe d p bnd (PElabError s) = pretty s
2081 -- Quasiquote pprinting ignores bound vars
2082 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2083 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2084 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2085 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2086 where start = if res then "`{" else "`{{"
2087 end = if res then "}" else "}}"
2088 prettySe d p bnd (PRunElab _ tm _) =
2089 bracket p funcAppPrec . group . align . hang 2 $
2091 prettySe (decD d) funcAppPrec bnd tm
2092 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2093 prettySe d p bnd _ = text "missing pretty-printer for term"
2095 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2096 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2097 where display (UN n) = T.unpack n
2098 display (MN _ n) = T.unpack n
2099 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2100 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2103 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2104 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2105 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2106 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2108 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2109 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2110 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2111 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2113 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2114 annName n = annotate (AnnName n Nothing Nothing Nothing)
2116 opStr :: Name -> String
2117 opStr (NS n _) = opStr n
2118 opStr (UN n) = T.unpack n
2120 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2121 slist' (Just d) _ _ _ | d <= 0 = Nothing
2123 | containsHole e = Nothing
2124 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2125 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2126 slist' d p bnd (PRef _ _ nil)
2127 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2128 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2129 | nsroot cons == sUN "::",
2130 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2132 Just tl' <- slist' (decD d) p bnd tl
2133 = Just (prettySe d startPrec bnd hd : tl')
2135 isImp (PImp {}) = True
2137 slist' _ _ _ tm = Nothing
2139 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2141 [] -> annotate (AnnData "" "") $ text "[]"
2142 [x] -> enclose left right . group $ x
2143 xs -> enclose left right .
2144 align . group . vsep .
2145 punctuate comma $ xs
2146 where left = (annotate (AnnData "" "") (text "["))
2147 right = (annotate (AnnData "" "") (text "]"))
2148 comma = (annotate (AnnData "" "") (text ","))
2149 slist _ _ _ _ = Nothing
2151 pairElts :: PTerm -> Maybe [PTerm]
2152 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2153 | otherwise = Just [x, y]
2154 pairElts _ = Nothing
2156 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2157 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2158 | otherwise = Just [(l, t), (Placeholder, r)]
2159 dPairElts _ = Nothing
2161 natns = "Prelude.Nat."
2163 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2165 | ppopt_desugarnats ppo = Nothing
2166 | otherwise = snat' d p e
2168 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2169 snat' (Just x) _ _ | x <= 0 = Nothing
2170 snat' d p (PRef _ _ z)
2171 | show z == (natns++"Z") || show z == "Z" = Just 0
2172 snat' d p (PApp _ s [PExp {getTm=n}])
2173 | show s == (natns++"S") || show s == "S",
2174 Just n' <- snat' (decD d) p n
2176 snat' _ _ _ = Nothing
2178 bracket outer inner doc
2179 | outer > inner = lparen <> doc <> rparen
2182 ellipsis = text "..."
2185 depth (Just d) = if d <= 0 then const ellipsis else id
2187 decD = fmap (\x -> x - 1)
2189 kwd = annotate AnnKeyword . text
2191 fixities :: M.Map String Fixity
2192 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2194 getFixity :: String -> Maybe Fixity
2195 getFixity = flip M.lookup fixities
2197-- | Strip away namespace information
2198basename :: Name -> Name
2199basename (NS n _) = basename n
2202-- | Determine whether a name was the one inserted for a hole or guess
2203-- by the delaborator
2204isHoleName :: Name -> Bool
2205isHoleName (UN n) = n == T.pack "[__]"
2208-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2209containsHole :: PTerm -> Bool
2210containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2212-- | Pretty-printer helper for names that attaches the correct annotations
2213prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2214 -> Bool -- ^ whether to show namespaces
2215 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2216 -> Name -- ^ the name to pprint
2217 -> Doc OutputAnnotation
2218prettyName infixParen showNS bnd n
2219 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2220 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2221 | (UN n') <- n, T.unpack n' == "_" = text "_"
2222 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2223 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2224 where fullName = text nameSpace <> parenthesise (text (baseName n))
2225 baseName (UN n) = T.unpack n
2226 baseName (NS n ns) = baseName n
2227 baseName (MN i s) = T.unpack s
2228 baseName other = show other
2229 nameSpace = case n of
2230 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2232 isInfix = case baseName n of
2234 (c : _) -> not (isAlpha c)
2235 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2238showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2239showCImp ppo (PClause _ n l ws r w)
2240 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2241 <+> text "where" <+> text (show w)
2244 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2245showCImp ppo (PWith _ n l ws r pn w)
2246 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2247 <+> braces (text (show w))
2250 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2253showDImp :: PPOption -> PData -> Doc OutputAnnotation
2254showDImp ppo (PDatadecl n nfc ty cons)
2255 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2256 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2258showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2259showDecls o ds = vsep (map (showDeclImp o) ds)
2261showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2262showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2263showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2264 indent 2 (vsep (map (showCImp o) cs))
2265showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2266showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2267showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2268showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2269showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2270showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2271 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2272showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2273 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2274showDeclImp _ _ = text "..."
2275-- showDeclImp (PImport o) = "import " ++ o
2277getImps :: [PArg] -> [(Name, PTerm)]
2279getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2280getImps (_ : xs) = getImps xs
2282getExps :: [PArg] -> [PTerm]
2284getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2285getExps (_ : xs) = getExps xs
2287getShowArgs :: [PArg] -> [PArg]
2289getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2290getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2291 | PImp _ _ _ _ tm <- e
2292 , containsHole tm = e : getShowArgs xs
2293getShowArgs (_ : xs) = getShowArgs xs
2295getConsts :: [PArg] -> [PTerm]
2297getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2298getConsts (_ : xs) = getConsts xs
2300getAll :: [PArg] -> [PTerm]
2305showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2306 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2307 -> PPOption -- ^ pretty printing options
2308 -> Bool -- ^ whether to colourise
2309 -> Name -- ^ the term to show
2311showName ist bnd ppo colour n = case ist of
2312 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2313 Nothing -> showbasic n
2314 where name = if ppopt_impl ppo then show n else showbasic n
2315 showbasic n@(UN _) = showCG n
2316 showbasic (MN i s) = str s
2317 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2318 showbasic (SN s) = show s
2320 colourise n t = let ctxt' = fmap tt_ctxt ist in
2323 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2324 else colouriseBound t name
2325 | isDConName n ctxt -> colouriseData t name
2326 | isFnName n ctxt -> colouriseFun t name
2327 | isTConName n ctxt -> colouriseType t name
2328 -- The assumption is that if a name is not bound and does not exist in the
2329 -- global context, then we're somewhere in which implicit info has been lost
2330 -- (like error messages). Thus, unknown vars are colourised as implicits.
2331 | otherwise -> colouriseImplicit t name
2333showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2334 -> PTerm -- ^ the term to show
2336showTm ist = displayDecorated (consoleDecorate ist) .
2337 renderPretty 0.8 100000 .
2338 prettyImp (ppOptionIst ist)
2340-- | Show a term with implicits, no colours
2341showTmImpls :: PTerm -> String
2342showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2344-- | Show a term with specific options
2345showTmOpts :: PPOption -> PTerm -> String
2346showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2349instance Sized PTerm where
2350 size (PQuote rawTerm) = size rawTerm
2351 size (PRef fc _ name) = size name
2352 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2353 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2354 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2355 size (PTyped trm ty) = 1 + size trm + size ty
2356 size (PApp fc name args) = 1 + size args
2357 size (PAppBind fc name args) = 1 + size args
2358 size (PCase fc trm bdy) = 1 + size trm + size bdy
2359 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2360 size (PTrue fc _) = 1
2361 size (PResolveTC fc) = 1
2362 size (PRewrite fc by left right _) = 1 + size left + size right
2363 size (PPair fc _ _ left right) = 1 + size left + size right
2364 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2365 size (PAlternative _ a alts) = 1 + size alts
2366 size (PHidden hidden) = size hidden
2367 size (PUnifyLog tm) = size tm
2368 size (PDisamb _ tm) = size tm
2369 size (PNoImplicits tm) = size tm
2371 size (PUniverse _ _) = 1
2372 size (PConstant fc const) = 1 + size fc + size const
2373 size Placeholder = 1
2374 size (PDoBlock dos) = 1 + size dos
2375 size (PIdiom fc term) = 1 + size term
2376 size (PMetavar _ name) = 1
2377 size (PProof tactics) = size tactics
2378 size (PElabError err) = size err
2379 size PImpossible = 1
2382getPArity :: PTerm -> Int
2383getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2386-- Return all names, free or globally bound, in the given term.
2388allNamesIn :: PTerm -> [Name]
2389allNamesIn tm = nub $ ni 0 [] tm
2390 where -- TODO THINK added niTacImp, but is it right?
2391 ni 0 env (PRef _ _ n)
2392 | not (n `elem` env) = [n]
2393 ni 0 env (PPatvar _ n) = [n]
2394 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2395 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2396 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2397 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2398 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2399 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2400 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2401 ni 0 env (PHidden tm) = ni 0 env tm
2402 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2403 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2404 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2405 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2406 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2407 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2408 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2409 ni 0 env (PUnifyLog tm) = ni 0 env tm
2410 ni 0 env (PDisamb _ tm) = ni 0 env tm
2411 ni 0 env (PNoImplicits tm) = ni 0 env tm
2413 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2414 ni i env (PUnquote tm) = ni (i - 1) env tm
2415 ni i env tm = concatMap (ni i env) (children tm)
2417 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2421-- Return all names defined in binders in the given term
2422boundNamesIn :: PTerm -> [Name]
2423boundNamesIn tm = S.toList (ni 0 S.empty tm)
2424 where -- TODO THINK Added niTacImp, but is it right?
2425 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2426 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2427 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2428 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2429 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2430 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2431 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2432 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2433 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2434 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2435 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2436 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2437 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2438 ni 0 set (PAlternative ns a as) = niTms 0 set as
2439 ni 0 set (PHidden tm) = ni 0 set tm
2440 ni 0 set (PUnifyLog tm) = ni 0 set tm
2441 ni 0 set (PDisamb _ tm) = ni 0 set tm
2442 ni 0 set (PNoImplicits tm) = ni 0 set tm
2444 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2445 ni i set (PUnquote tm) = ni (i - 1) set tm
2447 ni i set tm = foldr (S.union . ni i set) set (children tm)
2449 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2450 niTms i set [] = set
2451 niTms i set (x : xs) = niTms i (ni i set x) xs
2453 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2454 niTacImp i set _ = set
2456-- Return names which are valid implicits in the given term (type).
2457implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2458implicitNamesIn uvars ist tm
2459 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2462 addImp n = do (imps, fns) <- get
2464 addFn n = do (imps, fns) <- get
2468 notCAF (PExp _ _ _ _ : _) = True
2469 notCAF (_ : xs) = notCAF xs
2471 notHidden (n, _) = case getAccessibility n of
2477 = case lookupDefAccExact n False (tt_ctxt ist) of
2481 ni 0 env (PRef _ _ n@(NS _ _))
2482 | not (n `elem` env)
2483 -- Never implicitly bind if there's a namespace
2485 ni 0 env (PRef _ _ n)
2486 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2487 ni 0 env (PApp _ f@(PRef _ _ n) as)
2488 | n `elem` uvars = do ni 0 env f
2489 mapM_ (ni 0 env . getTm) as
2490 | otherwise = do case lookupTy n (tt_ctxt ist) of
2493 mapM_ (ni 0 env . getTm) as
2494 ni 0 env (PApp _ f as) = do ni 0 env f
2495 mapM_ (ni 0 env . getTm) as
2496 ni 0 env (PAppBind _ f as) = do ni 0 env f
2497 mapM_ (ni 0 env . getTm) as
2498 ni 0 env (PCase _ c os) = do ni 0 env c
2499 -- names in 'os', not counting the names bound in the cases
2500 mapM_ (ni 0 env . snd) os
2503 mapM_ (ni 0 env . fst) os
2505 put (nub imps \\ nub impsfst, fns)
2506 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2507 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2508 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2509 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2510 ni 0 env val; ni 0 (n:env) sc
2511 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2512 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2513 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2514 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2515 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2518 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2519 ni 0 env (PHidden tm) = ni 0 env tm
2520 ni 0 env (PUnifyLog tm) = ni 0 env tm
2521 ni 0 env (PDisamb _ tm) = ni 0 env tm
2522 ni 0 env (PNoImplicits tm) = ni 0 env tm
2524 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2525 maybe (return ()) (ni i env) ty
2526 ni i env (PUnquote tm) = ni (i - 1) env tm
2528 ni i env tm = mapM_ (ni i env) (children tm)
2530-- Return names which are free in the given term.
2531namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2532namesIn uvars ist tm = nub $ ni 0 [] tm
2534 ni 0 env (PRef _ _ n)
2535 | not (n `elem` env)
2536 = case lookupTy n (tt_ctxt ist) of
2538 _ -> [n | n `elem` (map fst uvars)]
2539 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2540 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2541 ni 0 env (PCase _ c os) = ni 0 env c ++
2542 -- names in 'os', not counting the names bound in the cases
2543 (nub (concatMap (ni 0 env . snd) os)
2544 \\ nub (concatMap (ni 0 env . fst) os))
2545 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2546 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2547 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2548 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2549 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2550 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2551 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2552 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2553 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2554 ni 0 env (PHidden tm) = ni 0 env tm
2555 ni 0 env (PUnifyLog tm) = ni 0 env tm
2556 ni 0 env (PDisamb _ tm) = ni 0 env tm
2557 ni 0 env (PNoImplicits tm) = ni 0 env tm
2559 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2560 ni i env (PUnquote tm) = ni (i - 1) env tm
2562 ni i env tm = concatMap (ni i env) (children tm)
2564 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2567-- Return which of the given names are used in the given term.
2569usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2570usedNamesIn vars ist tm = nub $ ni 0 [] tm
2571 where -- TODO THINK added niTacImp, but is it right?
2572 ni 0 env (PRef _ _ n)
2573 | n `elem` vars && not (n `elem` env)
2574 = case lookupDefExact n (tt_ctxt ist) of
2577 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2578 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2579 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2580 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2581 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2582 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2583 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2584 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2585 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2586 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2587 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2588 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2589 ni 0 env (PHidden tm) = ni 0 env tm
2590 ni 0 env (PUnifyLog tm) = ni 0 env tm
2591 ni 0 env (PDisamb _ tm) = ni 0 env tm
2592 ni 0 env (PNoImplicits tm) = ni 0 env tm
2594 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2595 ni i env (PUnquote tm) = ni (i - 1) env tm
2597 ni i env tm = concatMap (ni i env) (children tm)
2599 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2602-- Return the list of inaccessible (= dotted) positions for a name.
2603getErasureInfo :: IState -> Name -> [Int]
2604getErasureInfo ist n =
2605 case lookupCtxtExact n (idris_optimisation ist) of
2606 Just (Optimise inacc _ _) -> map fst inacc
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list