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
18import IRTS.CodegenCommon
20import Util.DynamicLinker
27import Prelude hiding (Foldable, Traversable, (<$>))
29import Control.Applicative ((<|>))
30import qualified Control.Monad.Trans.Class as Trans (lift)
31import Control.Monad.Trans.Except
32import Control.Monad.Trans.State.Strict
34import Data.Data (Data)
36import Data.Foldable (Foldable)
37import Data.Function (on)
38import Data.Generics.Uniplate.Data (children, universe)
39import Data.List hiding (group)
40import qualified Data.Map.Strict as M
41import Data.Maybe (mapMaybe, maybeToList)
42import qualified Data.Set as S
43import qualified Data.Text as T
44import Data.Traversable (Traversable)
46import GHC.Generics (Generic)
47import Network.Socket (PortNumber)
50data ElabWhat = ETypes | EDefns | EAll
53-- | Data to pass to recursively called elaborators; e.g. for where blocks,
54-- paramaterised declarations, etc.
56-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
57-- so that we can have mutually recursive elaborators in separate modules without
58-- having to muck about with cyclic modules.
59data ElabInfo = EInfo {
60 params :: [(Name, PTerm)]
61 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
62 , liftname :: Name -> Name
63 , namespace :: [String]
65 , constraintNS :: String -- ^ filename for adding to constraint variables
67 , noCaseLift :: [Name] -- ^ types which shouldn't be made arguments to case
68 -- | We may, recursively, collect transformations to do on the rhs,
69 -- e.g. rewriting recursive calls to functions defined by 'with'
70 , rhs_trans :: PTerm -> PTerm
71 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
75toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 [] id (\_ _ _ -> fail "Not implemented")
77toplevelWith :: String -> ElabInfo
78toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 [] id (\_ _ _ -> fail "Not implemented")
80eInfoNames :: ElabInfo -> [Name]
81eInfoNames info = map fst (params info) ++ M.keys (inblock info)
83data IOption = IOption {
85 , opt_logcats :: [LogCat] -- ^ List of logging categories.
86 , opt_typecase :: Bool
87 , opt_typeintype :: Bool
88 , opt_coverage :: Bool
89 , opt_showimp :: Bool -- ^ show implicits
90 , opt_errContext :: Bool
93 , opt_nobanner :: Bool
95 , opt_codegen :: Codegen
96 , opt_outputTy :: OutputType
97 , opt_ibcsubdir :: FilePath
98 , opt_importdirs :: [FilePath]
99 , opt_sourcedirs :: [FilePath]
100 , opt_triple :: String
102 , opt_cmdline :: [Opt] -- ^ remember whole command line
103 , opt_origerr :: Bool
104 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
105 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
106 , opt_optimise :: [Optimisation]
107 , opt_printdepth :: Maybe Int
108 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
109 , opt_desugarnats :: Bool
110 , opt_autoimpls :: Bool
111 } deriving (Show, Eq, Generic)
113defaultOpts :: IOption
114defaultOpts = IOption { opt_logLevel = 0
116 , opt_typecase = False
117 , opt_typeintype = False
118 , opt_coverage = True
119 , opt_showimp = False
120 , opt_errContext = False
123 , opt_nobanner = False
125 , opt_codegen = Via IBCFormat "c"
126 , opt_outputTy = Executable
128 , opt_importdirs = []
129 , opt_sourcedirs = []
133 , opt_origerr = False
134 , opt_autoSolve = True
135 , opt_autoImport = []
136 , opt_optimise = defaultOptimise
137 , opt_printdepth = Just 5000
138 , opt_evaltypes = True
139 , opt_desugarnats = False
140 , opt_autoimpls = True
143data PPOption = PPOption {
144 ppopt_impl :: Bool -- ^ whether to show implicits
145 , ppopt_desugarnats :: Bool
146 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
147 , ppopt_depth :: Maybe Int
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
187-- | The output mode in use
188data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
189 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
193-- | If a function has no totality annotation, what do we assume?
194data DefaultTotality = DefaultCheckingTotal -- ^ Total
195 | DefaultCheckingPartial -- ^ Partial
196 | DefaultCheckingCovering -- ^Total coverage, but may diverge
197 deriving (Show, Eq, Generic)
199-- | Configuration options for interactive editing.
200data InteractiveOpts = InteractiveOpts {
201 interactiveOpts_indentWith :: Int
202 , interactiveOpts_indentClause :: Int
203} deriving (Show, Generic)
205-- | The global state used in the Idris monad
206data IState = IState {
207 tt_ctxt :: Context -- ^ All the currently defined names and their terms
208 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
209 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
210 , idris_implicits :: Ctxt [PArg]
211 , idris_statics :: Ctxt [Bool]
212 , idris_interfaces :: Ctxt InterfaceInfo
213 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
214 , idris_records :: Ctxt RecordInfo
215 , idris_dsls :: Ctxt DSL
216 , idris_optimisation :: Ctxt OptInfo
217 , idris_datatypes :: Ctxt TypeInfo
218 , idris_namehints :: Ctxt [Name]
220 -- | list of lhs/rhs, and a list of missing clauses. These are not
222 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
223 , idris_flags :: Ctxt [FnOpt]
224 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
225 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
227 -- | module documentation is saved in a special MN so the context
228 -- mechanism can be used for disambiguation.
229 , idris_moduledocs :: Ctxt (Docstring DocTerm)
230 , idris_tyinfodata :: Ctxt TIData
231 , idris_fninfo :: Ctxt FnInfo
232 , idris_transforms :: Ctxt [(Term, Term)]
233 , idris_autohints :: Ctxt [Name]
234 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
235 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
236 , idris_totcheckfail :: [(FC, String)]
237 , idris_options :: IOption
239 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
241 -- | The currently defined but not proven metavariables. The Int is
242 -- the number of vars to display as a context, the Maybe Name is its
243 -- top-level function, the [Name] is the list of local variables
244 -- available for proof search and the Bools are whether :p is
245 -- allowed, and whether the variable is definable at all
246 -- (Metavariables are not definable if they are applied in a term
247 -- which still has hole bindings)
248 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
249 , idris_coercions :: [Name]
250 , idris_errRev :: [(Term, Term)]
251 , idris_errReduce :: [Name]
252 , syntax_rules :: SyntaxRules
253 , syntax_keywords :: [String]
254 , imported :: [FilePath] -- ^ The imported modules
255 , idris_scprims :: [(Name, (Int, PrimFn))]
256 , idris_objs :: [(Codegen, FilePath)]
257 , idris_libs :: [(Codegen, String)]
258 , idris_cgflags :: [(Codegen, String)]
259 , idris_hdrs :: [(Codegen, String)]
260 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
261 , proof_list :: [(Name, (Bool, [String]))]
262 , errSpan :: Maybe FC
263 , parserWarnings :: [(FC, Err)]
264 , lastParse :: Maybe Name
265 , indent_stack :: [Int]
266 , brace_stack :: [Maybe Int]
267 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
268 , idris_parsedSpan :: Maybe FC
269 , hide_list :: Ctxt Accessibility
270 , default_access :: Accessibility
271 , default_total :: DefaultTotality
272 , ibc_write :: [IBCWrite]
273 , compiled_so :: Maybe String
274 , idris_dynamic_libs :: [DynamicLib]
275 , idris_language_extensions :: [LanguageExt]
276 , idris_outputmode :: OutputMode
277 , idris_colourRepl :: Bool
278 , idris_colourTheme :: ColourTheme
279 , idris_errorhandlers :: [Name] -- ^ Global error handlers
280 , idris_nameIdx :: (Int, Ctxt (Int, Name))
281 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
282 , module_aliases :: M.Map [T.Text] [T.Text]
283 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
284 , idris_postulates :: S.Set Name
285 , idris_externs :: S.Set (Name, Int)
286 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
288 -- | List of names that were defined in the repl, and can be re-/un-defined
289 , idris_repl_defs :: [Name]
291 -- | Stack of names currently being elaborated, Bool set if it's an
292 -- implementation (implementations appear twice; also as a function name)
293 , elab_stack :: [(Name, Bool)]
296 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
297 , idris_exports :: [Name] -- ^ Functions with ExportList
298 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
299 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
300 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
301 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
302 , idris_ttstats :: M.Map Term (Int, Term)
303 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
304 , idris_interactiveOpts :: InteractiveOpts
307-- Required for parsers library, and therefore trifecta
308instance Show IState where
309 show = const "{internal state}"
311data SizeChange = Smaller | Same | Bigger | Unknown
312 deriving (Show, Eq, Generic)
314deriving instance Binary SizeChange
317type SCGEntry = (Name, [Maybe (Int, SizeChange)])
318type UsageReason = (Name, Int) -- fn_name, its_arg_number
320data CGInfo = CGInfo {
321 calls :: [Name] -- Immediate calls
322 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
324 , usedpos :: [(Int, [UsageReason])]
325 } deriving (Show, Generic)
327deriving instance Binary CGInfo
331primDefs = [ sUN "unsafePerformPrimIO"
332 , sUN "mkLazyForeignPrim"
333 , sUN "mkForeignPrim"
335 , sUN "assert_unreachable"
339-- information that needs writing for the current module's .ibc file
340data IBCWrite = IBCFix FixDecl
345 | IBCImplementation Bool Bool Name Name
352 | IBCImport (Bool, FilePath) -- ^ True = import public
353 | IBCImportDir FilePath
354 | IBCSourceDir FilePath
355 | IBCObj Codegen FilePath
356 | IBCLib Codegen String
357 | IBCCGFlag Codegen String
359 | IBCHeader Codegen String
360 | IBCAccess Name Accessibility
361 | IBCMetaInformation Name MetaInformation
362 | IBCTotal Name Totality
363 | IBCInjective Name Injectivity
365 | IBCFnInfo Name FnInfo
366 | IBCTrans Name (Term, Term)
367 | IBCErrRev (Term, Term)
372 | IBCDef Name -- ^ The main context.
373 | IBCNameHint (Name, Name)
374 | IBCLineApp FilePath Int PTerm
375 | IBCErrorHandler Name
376 | IBCFunctionErrorHandler Name Name Name
378 | IBCExtern (Name, Int)
379 | IBCTotCheckErr FC String
381 | IBCModDocs Name -- ^ The name is the special name used to track module docs
382 | IBCUsage (Name, Int)
384 | IBCAutoHint Name Name
385 | IBCDeprecate Name String
386 | IBCFragile Name String
387 | IBCConstraint FC UConstraint
388 deriving (Show, Generic)
390initialInteractiveOpts :: InteractiveOpts
391initialInteractiveOpts = InteractiveOpts {
392 interactiveOpts_indentWith = 2
393 , interactiveOpts_indentClause = 2
396-- | The initial state for the compiler
398idrisInit = IState initContext S.empty []
399 emptyContext emptyContext emptyContext [] emptyContext
400 emptyContext emptyContext emptyContext emptyContext
401 emptyContext emptyContext emptyContext emptyContext
402 emptyContext emptyContext emptyContext emptyContext
404 [] [] [] defaultOpts 6 [] [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
405 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
406 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
407 AutomaticWidth S.empty S.empty [] [] [] M.empty [] [] []
408 emptyContext S.empty M.empty emptyContext initialInteractiveOpts
411-- | The monad for the main REPL - reading and processing files and
412-- updating global state (hence the IO inner monad).
415-- type Idris = WriterT [Either String (IO ())] (State IState a))
418type Idris = StateT IState (ExceptT Err IO)
420catchError :: Idris a -> (Err -> Idris a) -> Idris a
421catchError = liftCatch catchE
423throwError :: Err -> Idris a
424throwError = Trans.lift . throwE
426-- Commands in the REPL
431data ElabShellCmd = EQED
439 | EDocStr (Either Name Const)
445-- Parsed declarations
447data Fixity = Infixl { prec :: Int }
448 | Infixr { prec :: Int }
449 | InfixN { prec :: Int }
450 | PrefixN { prec :: Int }
451 deriving (Eq, Generic)
453deriving instance Binary Fixity
456instance Show Fixity where
457 show (Infixl i) = "infixl " ++ show i
458 show (Infixr i) = "infixr " ++ show i
459 show (InfixN i) = "infix " ++ show i
460 show (PrefixN i) = "prefix " ++ show i
462data FixDecl = Fix Fixity String
463 deriving (Eq, Generic)
465instance Show FixDecl where
466 show (Fix f s) = show f ++ " " ++ s
469deriving instance Binary FixDecl
472instance Ord FixDecl where
473 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
476data Static = Static | Dynamic
477 deriving (Show, Eq, Ord, Data, Generic, Typeable)
479deriving instance Binary Static
482-- ^ Mark bindings with their explicitness, and laziness
483data Plicity = Imp { pargopts :: [ArgOpt]
486 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
487 , pinsource :: Bool -- ^ Explicitly written in source
490 | Exp { pargopts :: [ArgOpt]
492 , pparam :: Bool -- ^ this is a param (rather than index)
495 | Constraint { pargopts :: [ArgOpt]
499 | TacImp { pargopts :: [ArgOpt]
504 deriving (Show, Eq, Ord, Data, Generic, Typeable)
507deriving instance Binary Plicity
510is_scoped :: Plicity -> Maybe ImplicitInfo
511is_scoped (Imp _ _ _ s _ _) = s
516impl = Imp [] Dynamic False (Just (Impl False True False)) False RigW
517-- Machine generated top level implicit
519impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False RigW
523forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False RigW
524forall_constraint :: Plicity
525forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False RigW
528expl = Exp [] Dynamic False RigW
530expl_param = Exp [] Dynamic True RigW
533constraint = Constraint [] Static RigW
535tacimpl :: PTerm -> Plicity
536tacimpl t = TacImp [] Dynamic t RigW
538data FnOpt = Inlinable -- ^ always evaluate when simplifying
539 | TotalFn | PartialFn | CoveringFn
540 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
543 -- | interface dictionary, eval only when a function
544 -- argument, and further evaluation results.
546 | OverlappingDictionary -- ^ Interface dictionary which may overlap
547 | Implicit -- ^ implicit coercion
548 | NoImplicit -- ^ do not apply implicit coercions
549 | CExport String -- ^ export, with a C name
550 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
551 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
552 | ErrorReduce -- ^ unfold definition before showing an error
553 | Reflection -- ^ a reflecting function, compile-time only
554 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
555 | Constructor -- ^ Data constructor type
556 | AutoHint -- ^ use in auto implicit search
557 | PEGenerated -- ^ generated by partial evaluator
558 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
559 deriving (Show, Eq, Generic)
561deriving instance Binary FnOpt
566inlinable :: FnOpts -> Bool
567inlinable = elem Inlinable
569dictionary :: FnOpts -> Bool
570dictionary = elem Dictionary
573-- | Type provider - what to provide
574data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
575 | ProvPostulate t -- ^ goal type must be Type, so only term
576 deriving (Show, Eq, Functor, Generic)
578type ProvideWhat = ProvideWhat' PTerm
580-- | Top-level declarations such as compiler directives, definitions,
581-- datatypes and interfaces.
583 -- | Fixity declaration
584 = PFix FC Fixity [String]
585 -- | Type declaration (last FC is precise name location)
586 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
587 -- | Postulate, second FC is precise name location
588 | PPostulate Bool -- external def if true
589 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
591 | PClauses FC FnOpts Name [PClause' t]
592 -- | Top level constant
594 -- | Data declaration.
595 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
597 | PParams FC [(Name, t)] [PDecl' t]
598 -- | Open block/declaration
599 | POpenInterfaces FC [Name] [PDecl' t]
600 -- | New namespace, where FC is accurate location of the namespace
602 | PNamespace String FC [PDecl' t]
604 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
606 FC -- Record name precise location
607 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
608 [(Name, Docstring (Either Err t))] -- Param Docs
609 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
610 (Maybe (Name, FC)) -- Optional constructor name and location
611 (Docstring (Either Err t)) -- Constructor doc
612 SyntaxInfo -- Constructor SyntaxInfo
614 -- | Interface: arguments are documentation, syntax info, source
615 -- location, constraints, interface name, interface name location,
616 -- parameters, method declarations, optional constructor name
617 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
618 [(Name, t)] -- constraints
619 Name -- interface name
620 FC -- accurate location of interface name
621 [(Name, FC, t)] -- parameters and precise locations
622 [(Name, Docstring (Either Err t))] -- parameter docstrings
623 [(Name, FC)] -- determining parameters and precise locations
624 [PDecl' t] -- declarations
625 (Maybe (Name, FC)) -- implementation constructor name and location
626 (Docstring (Either Err t)) -- implementation constructor docs
628 -- | Implementation declaration: arguments are documentation, syntax
629 -- info, source location, constraints, interface name, parameters, full
630 -- Implementation type, optional explicit name, and definitions
631 | PImplementation (Docstring (Either Err t)) -- Implementation docs
632 [(Name, Docstring (Either Err t))] -- Parameter docs
634 FC [(Name, t)] -- constraints
635 [Name] -- parent dictionaries to search for constraints
639 FC -- precise location of interface
641 [(Name, t)] -- Extra names in scope in the body
642 t -- full Implementation type
643 (Maybe Name) -- explicit name
645 | PDSL Name (DSL' t) -- ^ DSL declaration
646 | PSyntax FC Syntax -- ^ Syntax definition
647 | PMutual FC [PDecl' t] -- ^ Mutual block
648 | PDirective Directive -- ^ Compiler directive.
650 -- | Type provider. The first t is the type, the second is the
651 -- term. The second FC is precise highlighting location.
652 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
654 -- | Source-to-source transformation rule. If bool is True, lhs and
655 -- rhs must be convertible.
656 | PTransform FC Bool t t
658 -- | FC is decl-level, for errors, and Strings represent the
660 | PRunElabDecl FC t [String]
661 deriving (Functor, Generic)
663deriving instance Binary PDecl'
666-- | The set of source directives
667data Directive = DLib Codegen String
668 | DLink Codegen String
669 | DFlag Codegen String
670 | DInclude Codegen String
675 | DSetTotal Name -- assert totality after checking
676 | DAccess Accessibility
677 | DDefault DefaultTotality
679 | DDynamicLibs [String]
680 | DNameHint Name FC [(Name, FC)]
681 | DErrorHandlers Name FC Name FC [(Name, FC)]
682 | DLanguage LanguageExt
683 | DDeprecate Name String
684 | DFragile Name String
685 | DAutoImplicits Bool
689-- | A set of instructions for things that need to happen in IState
690-- after a term elaboration when there's been reflected elaboration.
691data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
692 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
693 | RAddImplementation Name Name
694 | RDatatypeDeclInstrs Name [PArg]
695 -- | Datatype, constructors
696 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
699-- | For elaborator state
700data EState = EState {
701 case_decls :: [(Name, PDecl)]
702 , delayed_elab :: [(Int, Elab' EState ())]
703 , new_tyDecls :: [RDeclInstructions]
704 , highlighting :: [(FC, OutputAnnotation)]
705 , auto_binds :: [Name] -- ^ names bound as auto implicits
706 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
710initEState = EState [] [] [] [] [] []
712type ElabD a = Elab' EState a
714highlightSource :: FC -> OutputAnnotation -> ElabD ()
715highlightSource fc annot =
716 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
718-- | One clause of a top-level definition. Term arguments to constructors are:
720-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
722-- 2. The list of extra 'with' patterns
724-- 3. The right-hand side
726-- 4. The where block (PDecl' t)
728data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
729 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
730 | PClauseR FC [t] t [PDecl' t]
731 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
732 deriving (Functor, Generic)
734deriving instance Binary PClause'
739 -- | Data declaration
740 PDatadecl { d_name :: Name -- ^ The name of the datatype
741 , d_name_fc :: FC -- ^ The precise location of the type constructor name
742 , d_tcon :: t -- ^ Type constructor
743 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
745 -- | "Placeholder" for data whose constructors are defined later
746 | PLaterdecl { d_name :: Name
749 } deriving (Functor, Generic)
751-- | Transform the FCs in a PData and its associated terms. The first
752-- function transforms the general-purpose FCs, and the second
753-- transforms those that are used for semantic source highlighting, so
754-- they can be treated specially.
755mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
756mapPDataFC f g (PDatadecl n nfc tycon ctors) =
757 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
758 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
759 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
760mapPDataFC f g (PLaterdecl n nfc tycon) =
761 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
763deriving instance Binary PData'
766-- Handy to get a free function for applying PTerm -> PTerm functions
767-- across a program, by deriving Functor
769type PDecl = PDecl' PTerm
770type PData = PData' PTerm
771type PClause = PClause' PTerm
773-- | Transform the FCs in a PTerm. The first function transforms the
774-- general-purpose FCs, and the second transforms those that are used
775-- for semantic source highlighting, so they can be treated specially.
776mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
777mapPDeclFC f g (PFix fc fixity ops) =
778 PFix (f fc) fixity ops
779mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
780 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
781mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
782 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
784mapPDeclFC f g (PClauses fc opts n clauses) =
785 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
786mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
787mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
788 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
789mapPDeclFC f g (PParams fc params decls) =
791 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
792 (map (mapPDeclFC f g) decls)
793mapPDeclFC f g (POpenInterfaces fc ifs decls) =
794 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
795mapPDeclFC f g (PNamespace ns fc decls) =
796 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
797mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
798 PRecord doc syn (f fc) opts n (g nfc)
799 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
801 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
802 plic, mapPTermFC f g ty, fdoc))
804 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
807mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
808 PInterface doc syn (f fc)
809 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
810 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
811 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
812 (map (mapPDeclFC f g) body)
813 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
815mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
816 PImplementation doc paramDocs syn (f fc)
817 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
818 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
819 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
820 (mapPTermFC f g implTy)
822 (map (mapPDeclFC f g) body)
823mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
824mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
826 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
827 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
828mapPDeclFC f g (PMutual fc decls) =
829 PMutual (f fc) (map (mapPDeclFC f g) decls)
830mapPDeclFC f g (PDirective d) =
833 DNameHint n nfc ns ->
834 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
835 DErrorHandlers n nfc n' nfc' ns ->
836 DErrorHandlers n (g nfc) n' (g nfc') $
837 map (\(an, anfc) -> (an, g anfc)) ns
838mapPDeclFC f g (PProvider doc syn fc nfc what n) =
839 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
840mapPDeclFC f g (PTransform fc safe l r) =
841 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
842mapPDeclFC f g (PRunElabDecl fc script ns) =
843 PRunElabDecl (f fc) (mapPTermFC f g script) ns
845-- | Get all the names declared in a declaration
846declared :: PDecl -> [Name]
847declared (PFix _ _ _) = []
848declared (PTy _ _ _ _ _ n fc t) = [n]
849declared (PPostulate _ _ _ _ _ _ n t) = [n]
850declared (PClauses _ _ n _) = [] -- not a declaration
851declared (PCAF _ n _) = [n]
852declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
853 where fstt (_, _, a, _, _, _, _) = a
854declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
855declared (PParams _ _ ds) = concatMap declared ds
856declared (POpenInterfaces _ _ ds) = concatMap declared ds
857declared (PNamespace _ _ ds) = concatMap declared ds
858declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
859declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
860declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
864declared (PDSL n _) = [n]
865declared (PSyntax _ _) = []
866declared (PMutual _ ds) = concatMap declared ds
867declared (PDirective _) = []
870-- get the names declared, not counting nested parameter blocks
871tldeclared :: PDecl -> [Name]
872tldeclared (PFix _ _ _) = []
873tldeclared (PTy _ _ _ _ _ n _ t) = [n]
874tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
875tldeclared (PClauses _ _ n _) = [] -- not a declaration
876tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
877tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
878 where fstt (_, _, a, _, _, _, _) = a
879tldeclared (PParams _ _ ds) = []
880tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
881tldeclared (PMutual _ ds) = concatMap tldeclared ds
882tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
883tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
884tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
890defined :: PDecl -> [Name]
891defined (PFix _ _ _) = []
892defined (PTy _ _ _ _ _ n _ t) = []
893defined (PPostulate _ _ _ _ _ _ n t) = []
894defined (PClauses _ _ n _) = [n] -- not a declaration
895defined (PCAF _ n _) = [n]
896defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
897 where fstt (_, _, a, _, _, _, _) = a
898defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
899defined (PParams _ _ ds) = concatMap defined ds
900defined (POpenInterfaces _ _ ds) = concatMap defined ds
901defined (PNamespace _ _ ds) = concatMap defined ds
902defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
903defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
904defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
908defined (PDSL n _) = [n]
909defined (PSyntax _ _) = []
910defined (PMutual _ ds) = concatMap defined ds
911defined (PDirective _) = []
914updateN :: [(Name, Name)] -> Name -> Name
915updateN ns n | Just n' <- lookup n ns = n'
918updateNs :: [(Name, Name)] -> PTerm -> PTerm
920updateNs ns t = mapPT updateRef t
921 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
924-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
926-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
927-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
928-- where updateCNs ns (PClause n l ts r ds)
929-- = PClause (updateN ns n) (fmap (updateNs ns) l)
930-- (map (fmap (updateNs ns)) ts)
931-- (fmap (updateNs ns) r)
932-- (map (updateDNs ns) ds)
938 deriving (Eq, Show, Ord, Data, Typeable, Generic)
940-- | High level language terms
941data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
942 -- high-level language
944 -- ^ A reference to a variable. The FC is its precise
945 -- source location for highlighting. The list of FCs is a
946 -- collection of additional highlighting locations.
947 | PInferRef FC [FC] Name -- ^ A name to be defined later
948 | PPatvar FC Name -- ^ A pattern variable
949 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
950 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
951 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
952 | PTyped PTerm PTerm -- ^ Term with explicit type
953 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
954 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
955 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
956 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
957 | PMatchApp FC Name -- ^ Make an application by type matching
958 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
959 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
960 | PTrue FC PunInfo -- ^ Unit type..?
961 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
962 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
963 -- ^ "rewrite" syntax, with optional rewriting function and
964 -- optional result type
965 | PPair FC [FC] PunInfo PTerm PTerm
966 -- ^ A pair (a, b) and whether it's a product type or a
967 -- pair (solved by elaboration). The list of FCs is its
969 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
970 -- ^ A dependent pair (tm : a ** b) and whether it's a
971 -- sigma type or a pair that inhabits one (solved by
972 -- elaboration). The [FC] is its punctuation.
973 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
974 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
975 | PHidden PTerm -- ^ Irrelevant or hidden pattern
976 | PType FC -- ^ 'Type' type
977 | PUniverse FC Universe -- ^ Some universe
978 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
979 | PConstant FC Const -- ^ Builtin types
980 | Placeholder -- ^ Underscore
981 | PDoBlock [PDo] -- ^ Do notation
982 | PIdiom FC PTerm -- ^ Idiom brackets
983 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
984 | PProof [PTactic] -- ^ Proof script
985 | PTactics [PTactic] -- ^ As PProof, but no auto solving
986 | PElabError Err -- ^ Error to report on elaboration
987 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
988 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
989 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
990 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
991 | PNoImplicits PTerm -- ^ never run implicit converions on the term
992 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
993 | PUnquote PTerm -- ^ ~Term
994 | PQuoteName Name Bool FC
995 -- ^ `{n} where the FC is the precise highlighting for
996 -- the name in particular. If the Bool is False, then
997 -- it's `{{n}} and the name won't be resolved.
998 | PRunElab FC PTerm [String]
999 -- ^ %runElab tm - New-style proof script. Args are
1000 -- location, script, enclosing namespace.
1001 | PConstSugar FC PTerm
1002 -- ^ A desugared constant. The FC is a precise source
1003 -- location that will be used to highlight it later.
1004 deriving (Eq, Ord, Data, Typeable, Generic)
1006data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1009 deriving (Eq, Ord, Data, Generic, Typeable)
1011-- | Transform the FCs in a PTerm. The first function transforms the
1012-- general-purpose FCs, and the second transforms those that are used
1013-- for semantic source highlighting, so they can be treated specially.
1014mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1015mapPTermFC f g (PQuote q) = PQuote q
1016mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1017mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1018mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1019mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1020mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1021mapPTermFC 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)
1022mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1023mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1024mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1025mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1026mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1027mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1028mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1029mapPTermFC 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)
1030mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1031mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1032mapPTermFC 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)
1033mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1034mapPTermFC 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)
1035mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1036mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1037mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1038mapPTermFC f g (PType fc) = PType (f fc)
1039mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1040mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1041mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1042mapPTermFC f g Placeholder = Placeholder
1043mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1044 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1045 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1046 mapPDoFC (DoBindP fc t1 t2 alts) =
1047 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1048 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1049 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1050mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1051mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1052mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1053mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1054mapPTermFC f g (PElabError err) = PElabError err
1055mapPTermFC f g PImpossible = PImpossible
1056mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1057mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1058mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1059mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1060mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1061mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1062mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1063mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1064mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1067dg instance Binary PTerm
1070mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1071mapPT f t = f (mpt t) where
1072 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1073 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1074 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1075 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1076 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1077 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1078 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1079 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1080 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1081 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1082 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1083 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1084 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1085 mpt (PHidden t) = PHidden (mapPT f t)
1086 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1087 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1088 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1089 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1090 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1091 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1092 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1096data PTactic' t = Intro [Name] | Intros | Focus Name
1097 | Refine Name [Bool] | Rewrite t | DoUnify
1104 | LetTac Name t | LetTacTy Name t t
1105 | Exact t | Compute | Trivial | TCImplementation
1106 | ProofSearch Bool Bool Int (Maybe Name)
1107 [Name] -- allowed local names
1109 -- ^ the bool is whether to search recursively
1112 | ProofState | ProofTerm | Undo
1113 | Try (PTactic' t) (PTactic' t)
1114 | TSeq (PTactic' t) (PTactic' t)
1115 | ApplyTactic t -- see Language.Reflection module
1119 | GoalType String (PTactic' t)
1122 | TDocStr (Either Name Const)
1125 | TFail [ErrorReportPart]
1128 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1130deriving instance Binary PTactic'
1132instance Sized a => Sized (PTactic' a) where
1133 size (Intro nms) = 1 + size nms
1135 size (Focus nm) = 1 + size nm
1136 size (Refine nm bs) = 1 + size nm + length bs
1137 size (Rewrite t) = 1 + size t
1138 size (Induction t) = 1 + size t
1139 size (LetTac nm t) = 1 + size nm + size t
1140 size (Exact t) = 1 + size t
1148 size (Try l r) = 1 + size l + size r
1149 size (TSeq l r) = 1 + size l + size r
1150 size (ApplyTactic t) = 1 + size t
1151 size (Reflect t) = 1 + size t
1152 size (Fill t) = 1 + size t
1156 size (TFail ts) = 1 + size ts
1159 size (CaseTac x) = 1 + size x
1160 size (Equiv t) = 1 + size t
1161 size (Claim x y) = 1 + size x + size y
1163 size (MatchRefine x) = 1 + size x
1164 size (LetTacTy x y z) = 1 + size x + size y + size z
1165 size TCImplementation = 1
1167type PTactic = PTactic' PTerm
1169data PDo' t = DoExp FC t
1170 | DoBind FC Name FC t -- ^ second FC is precise name location
1171 | DoBindP FC t t [(t,t)]
1172 | DoLet FC Name FC t t -- ^ second FC is precise name location
1174 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1176deriving instance Binary PDo'
1179instance Sized a => Sized (PDo' a) where
1180 size (DoExp fc t) = 1 + size fc + size t
1181 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1182 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1183 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1184 size (DoLetP fc l r) = 1 + size fc + size l + size r
1186type PDo = PDo' PTerm
1188-- The priority gives a hint as to elaboration order. Best to elaborate
1189-- things early which will help give a more concrete type to other
1190-- variables, e.g. a before (interpTy a).
1192data PArg' t = PImp { priority :: Int
1193 , machine_inf :: Bool -- ^ true if the machine inferred it
1194 , argopts :: [ArgOpt]
1198 | PExp { priority :: Int
1199 , argopts :: [ArgOpt]
1203 | PConstraint { priority :: Int
1204 , argopts :: [ArgOpt]
1208 | PTacImplicit { priority :: Int
1209 , argopts :: [ArgOpt]
1214 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1216data ArgOpt = AlwaysShow
1220 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1222instance Sized a => Sized (PArg' a) where
1223 size (PImp p _ l nm trm) = 1 + size nm + size trm
1224 size (PExp p l nm trm) = 1 + size nm + size trm
1225 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1226 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1229deriving instance Binary PArg'
1232pimp n t mach = PImp 1 mach [] n t
1233pexp t = PExp 1 [] (sMN 0 "arg") t
1234pconst t = PConstraint 1 [] (sMN 0 "carg") t
1235ptacimp n s t = PTacImplicit 2 [] n s t
1237type PArg = PArg' PTerm
1239-- | Get the highest FC in a term, if one exists
1240highestFC :: PTerm -> Maybe FC
1241highestFC (PQuote _) = Nothing
1242highestFC (PRef fc _ _) = Just fc
1243highestFC (PInferRef fc _ _) = Just fc
1244highestFC (PPatvar fc _) = Just fc
1245highestFC (PLam fc _ _ _ _) = Just fc
1246highestFC (PPi _ _ _ _ _) = Nothing
1247highestFC (PLet fc _ _ _ _ _) = Just fc
1248highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1249highestFC (PApp fc _ _) = Just fc
1250highestFC (PAppBind fc _ _) = Just fc
1251highestFC (PMatchApp fc _) = Just fc
1252highestFC (PCase fc _ _) = Just fc
1253highestFC (PIfThenElse fc _ _ _) = Just fc
1254highestFC (PTrue fc _) = Just fc
1255highestFC (PResolveTC fc) = Just fc
1256highestFC (PRewrite fc _ _ _ _) = Just fc
1257highestFC (PPair fc _ _ _ _) = Just fc
1258highestFC (PDPair fc _ _ _ _ _) = Just fc
1259highestFC (PAs fc _ _) = Just fc
1260highestFC (PAlternative _ _ args) =
1261 case mapMaybe highestFC args of
1264highestFC (PHidden _) = Nothing
1265highestFC (PType fc) = Just fc
1266highestFC (PUniverse _ _) = Nothing
1267highestFC (PGoal fc _ _ _) = Just fc
1268highestFC (PConstant fc _) = Just fc
1269highestFC Placeholder = Nothing
1270highestFC (PDoBlock lines) =
1271 case map getDoFC lines of
1275 getDoFC (DoExp fc t) = fc
1276 getDoFC (DoBind fc nm nfc t) = fc
1277 getDoFC (DoBindP fc l r alts) = fc
1278 getDoFC (DoLet fc nm nfc l r) = fc
1279 getDoFC (DoLetP fc l r) = fc
1281highestFC (PIdiom fc _) = Just fc
1282highestFC (PMetavar fc _) = Just fc
1283highestFC (PProof _) = Nothing
1284highestFC (PTactics _) = Nothing
1285highestFC (PElabError _) = Nothing
1286highestFC PImpossible = Nothing
1287highestFC (PCoerced tm) = highestFC tm
1288highestFC (PDisamb _ opts) = highestFC opts
1289highestFC (PUnifyLog tm) = highestFC tm
1290highestFC (PNoImplicits tm) = highestFC tm
1291highestFC (PQuasiquote _ _) = Nothing
1292highestFC (PUnquote tm) = highestFC tm
1293highestFC (PQuoteName _ _ fc) = Just fc
1294highestFC (PRunElab fc _ _) = Just fc
1295highestFC (PConstSugar fc _) = Just fc
1296highestFC (PAppImpl t _) = highestFC t
1300data InterfaceInfo = CI {
1301 implementationCtorName :: Name
1302 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1303 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1304 , interface_default_super_interfaces :: [PDecl]
1305 , interface_impparams :: [Name]
1306 , interface_params :: [Name]
1307 , interface_constraints :: [PTerm]
1308 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1309 , interface_determiners :: [Int]
1310 } deriving (Show, Generic)
1312deriving instance Binary InterfaceInfo
1316data RecordInfo = RI {
1317 record_parameters :: [(Name,PTerm)]
1318 , record_constructor :: Name
1319 , record_projections :: [Name]
1320 } deriving (Show, Generic)
1322-- Type inference data
1324data TIData = TIPartial -- ^ a function with a partially defined type
1325 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1326 deriving (Show, Generic)
1328-- | Miscellaneous information about functions
1329data FnInfo = FnInfo { fn_params :: [Int] }
1330 deriving (Show, Generic)
1332deriving instance Binary FnInfo
1335data OptInfo = Optimise {
1336 inaccessible :: [(Int,Name)] -- includes names for error reporting
1337 , detaggable :: Bool
1338 , forceable :: [Int] -- argument positions which are forced by other values
1339 } deriving (Show, Generic)
1341deriving instance Binary OptInfo
1344-- | Syntactic sugar info
1349 , dsl_var :: Maybe t
1350 , index_first :: Maybe t
1351 , index_next :: Maybe t
1352 , dsl_lambda :: Maybe t
1353 , dsl_let :: Maybe t
1355 } deriving (Show, Functor, Generic)
1357deriving instance Binary DSL'
1360type DSL = DSL' PTerm
1362data SynContext = PatternSyntax
1365 deriving (Show, Generic)
1367deriving instance Binary SynContext
1370data Syntax = Rule [SSymbol] PTerm SynContext
1371 | DeclRule [SSymbol] [PDecl]
1372 deriving (Show, Generic)
1374syntaxNames :: Syntax -> [Name]
1375syntaxNames (Rule syms _ _) = mapMaybe ename syms
1376 where ename (Keyword n) = Just n
1378syntaxNames (DeclRule syms _) = mapMaybe ename syms
1379 where ename (Keyword n) = Just n
1382syntaxSymbols :: Syntax -> [SSymbol]
1383syntaxSymbols (Rule ss _ _) = ss
1384syntaxSymbols (DeclRule ss _) = ss
1386deriving instance Binary Syntax
1389data SSymbol = Keyword Name
1394 deriving (Show, Eq, Generic)
1398deriving instance Binary SSymbol
1401newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1404emptySyntaxRules :: SyntaxRules
1405emptySyntaxRules = SyntaxRules []
1407updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1408updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1410 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1415 ruleSort (s1:ss1) (s2:ss2) =
1416 case symCompare s1 s2 of
1417 EQ -> ruleSort ss1 ss2
1420 -- Better than creating Ord implementation for SSymbol since
1421 -- in general this ordering does not really make sense.
1422 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1423 symCompare (Keyword _) _ = LT
1424 symCompare (Symbol _) (Keyword _) = GT
1425 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1426 symCompare (Symbol _) _ = LT
1427 symCompare (Binding _) (Keyword _) = GT
1428 symCompare (Binding _) (Symbol _) = GT
1429 symCompare (Binding b1) (Binding b2) = compare b1 b2
1430 symCompare (Binding _) _ = LT
1431 symCompare (Expr _) (Keyword _) = GT
1432 symCompare (Expr _) (Symbol _) = GT
1433 symCompare (Expr _) (Binding _) = GT
1434 symCompare (Expr e1) (Expr e2) = compare e1 e2
1435 symCompare (Expr _) _ = LT
1436 symCompare (SimpleExpr _) (Keyword _) = GT
1437 symCompare (SimpleExpr _) (Symbol _) = GT
1438 symCompare (SimpleExpr _) (Binding _) = GT
1439 symCompare (SimpleExpr _) (Expr _) = GT
1440 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1442initDSL = DSL (PRef f [] (sUN ">>="))
1443 (PRef f [] (sUN "<*>"))
1444 (PRef f [] (sUN "pure"))
1451 where f = fileFC "(builtin)"
1453data Using = UImplicit Name PTerm
1454 | UConstraint Name [Name]
1455 deriving (Show, Eq, Data, Generic, Typeable)
1457deriving instance Binary Using
1460data SyntaxInfo = Syn {
1462 , syn_params :: [(Name, PTerm)]
1463 , syn_namespace :: [String]
1465 , imp_methods :: [Name]
1466 -- ^ interface methods. When expanding implicits, these should be
1467 -- expanded even under binders
1468 , decoration :: Name -> Name
1470 , implicitAllowed :: Bool
1471 , constraintAllowed :: Bool
1472 , maxline :: Maybe Int
1473 , mut_nesting :: Int
1475 , syn_in_quasiquote :: Int
1476 , syn_toplevel :: Bool
1477 , withAppAllowed :: Bool
1478 } deriving (Show, Generic)
1480deriving instance Binary SyntaxInfo
1483defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1485expandNS :: SyntaxInfo -> Name -> Name
1486expandNS syn n@(NS _ _) = n
1487expandNS syn n = case syn_namespace syn of
1492-- For inferring types of things
1494bi = fileFC "builtin"
1495primfc = fileFC "(primitive)"
1497inferTy = sMN 0 "__Infer"
1498inferCon = sMN 0 "__infer"
1499inferDecl = PDatadecl inferTy primfc
1501 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1502 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1503 (PRef bi [] inferTy)), bi, [])]
1506infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1507infP = P (TCon 6 0) inferTy (TType (UVal 0))
1509getInferTerm, getInferType :: Term -> Term
1510getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1511getInferTerm (App _ (App _ _ _) tm) = tm
1512getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1514getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1515 where toTy (Lam r t) = Pi r Nothing t (TType (UVar [] 0))
1516 toTy (PVar _ t) = PVTy t
1518getInferType (App _ (App _ _ ty) _) = ty
1522-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1524primNames = [inferTy, inferCon]
1527unitCon = sUN "MkUnit"
1529falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1530 "The empty type, also known as the trivially false proposition." ++
1532 "Use `void` or `absurd` to prove anything if you have a variable " ++
1533 "of type `Void` in scope."
1536pairTy = sNS (sUN "Pair") ["Builtins"]
1537pairCon = sNS (sUN "MkPair") ["Builtins"]
1539upairTy = sNS (sUN "UPair") ["Builtins"]
1540upairCon = sNS (sUN "MkUPair") ["Builtins"]
1544eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1545 "The propositional equality type. A proof that `x` = `y`." ++
1547 "To use such a proof, pattern-match on it, and the two equal things will " ++
1548 "then need to be the _same_ pattern." ++
1550 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1551 "is possible to state equalities between values of potentially different " ++
1552 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1554 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1556eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1557 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1559 [(reflDoc, reflParamDoc,
1560 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1561 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1562 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1563 pimp (n "B") Placeholder False,
1564 pexp (PRef bi [] (n "x")),
1565 pexp (PRef bi [] (n "x"))])), bi, [])]
1567 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1568 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1569 "shown that both sides are in fact equal."
1570 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1571 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1573eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1574 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1580-- | The special name to be used in the module documentation context -
1581-- not for use in the main definition context. The namespace around it
1582-- will determine the module to which the docs adhere.
1584modDocName = sMN 0 "ModuleDocs"
1586-- Defined in builtins.idr
1587sigmaTy = sNS (sUN "DPair") ["Builtins"]
1588sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1590piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1591piBind = piBindp expl
1593piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1595piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1598-- Pretty-printing declarations and terms
1600-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1601-- could interfere with interactive editing, which calls "show".
1603instance Show PTerm where
1604 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1606instance Show PDecl where
1607 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1609instance Show PClause where
1610 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1612instance Show PData where
1613 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1615instance Pretty PTerm OutputAnnotation where
1616 pretty = prettyImp defaultPPOption
1618-- | Colourise annotations according to an Idris state. It ignores the
1619-- names in the annotation, as there's no good way to show extended
1620-- information on a terminal.
1621annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1622annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1623annotationColour ist (AnnConst c) =
1624 let theme = idris_colourTheme ist
1625 in Just $ if constIsType c
1626 then typeColour theme
1627 else dataColour theme
1628annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1629annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1630annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1631annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1632annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1633annotationColour ist (AnnName n _ _ _) =
1634 let ctxt = tt_ctxt ist
1635 theme = idris_colourTheme ist
1637 _ | isDConName n ctxt -> Just $ dataColour theme
1638 _ | isFnName n ctxt -> Just $ functionColour theme
1639 _ | isTConName n ctxt -> Just $ typeColour theme
1640 _ | isPostulateName n ist -> Just $ postulateColour theme
1641 _ | otherwise -> Nothing -- don't colourise unknown names
1642annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1643 where colour BoldText = IdrisColour Nothing True False True False
1644 colour UnderlineText = IdrisColour Nothing True True False False
1645 colour ItalicText = IdrisColour Nothing True False False True
1646annotationColour ist _ = Nothing
1649-- | Colourise annotations according to an Idris state. It ignores the
1650-- names in the annotation, as there's no good way to show extended
1651-- information on a terminal. Note that strings produced this way will
1652-- not be coloured on Windows, so the use of the colour rendering
1653-- functions in Idris.Output is to be preferred.
1654consoleDecorate :: IState -> OutputAnnotation -> String -> String
1655consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1657isPostulateName :: Name -> IState -> Bool
1658isPostulateName n ist = S.member n (idris_postulates ist)
1660-- | Pretty-print a high-level closed Idris term with no information
1661-- about precedence/associativity
1662prettyImp :: PPOption -- ^ pretty printing options
1663 -> PTerm -- ^ the term to pretty-print
1664 -> Doc OutputAnnotation
1665prettyImp impl = pprintPTerm impl [] [] []
1667-- | Serialise something to base64 using its Binary implementation.
1669-- | Do the right thing for rendering a term in an IState
1670prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1671prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1673-- | Pretty-print a high-level Idris term in some bindings context
1675pprintPTerm :: PPOption -- ^ pretty printing options
1676 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1677 -> [Name] -- ^ names to always show in pi, even if not used
1678 -> [FixDecl] -- ^ Fixity declarations
1679 -> PTerm -- ^ the term to pretty-print
1680 -> Doc OutputAnnotation
1681pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1686 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1687 prettySe d p bnd (PQuote r) =
1688 text "![" <> pretty r <> text "]"
1689 prettySe d p bnd (PPatvar fc n) = pretty n
1691 | Just str <- slist d p bnd e = depth d str
1692 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1693 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1694 prettySe d p bnd (PLam fc n nfc ty sc) =
1695 let (ns, sc') = getLamNames [n] sc in
1696 depth d . bracket p startPrec . group . align . hang 2 $
1697 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1698 prettySe (decD d) startPrec ((n, False):bnd) sc'
1700 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1701 getLamNames acc sc = (reverse acc, sc)
1703 prettyBindingsOf [] t = text ""
1704 prettyBindingsOf [n] t = prettyBindingOf n t
1705 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1706 prettyBindingsOf ns t
1707 prettySe d p bnd (PLet fc n nfc ty v sc) =
1708 depth d . bracket p startPrec . group . align $
1709 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1710 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1711 prettySe d p bnd (PPi (Exp l s _ rig) n _ ty sc)
1713 depth d . bracket p startPrec . group $
1714 enclose lparen rparen (group . align $ text "0" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1715 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1717 depth d . bracket p startPrec . group $
1718 enclose lparen rparen (group . align $ text "1" <+> prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1719 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1720 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1721 || ppopt_pinames ppo && uname n =
1722 depth d . bracket p startPrec . group $
1723 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1724 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1726 depth d . bracket p startPrec . group $
1727 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1728 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1730 uname (UN n) = case str n of
1737 Static -> text "%static" <> space
1739 prettySe d p bnd (PPi (Imp l s _ fa _ rig) n _ ty sc)
1741 depth d . bracket p startPrec $
1742 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1743 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1744 | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc
1745 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1747 showRig Rig0 n = text "0" <+> prettyBindingOf n True
1748 showRig Rig1 n = text "1" <+> prettyBindingOf n True
1749 showRig _ n = prettyBindingOf n True
1751 isPi (PPi (Exp{}) _ _ _ _) = True
1752 isPi (PPi _ _ _ _ sc) = isPi sc
1757 Static -> text "%static" <> space
1759 prettySe d p bnd (PPi (Constraint _ _ rig) n _ ty sc) =
1760 depth d . bracket p startPrec $
1761 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1762 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}]) rig) n _ ty sc) =
1763 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1764 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1765 prettySe d p bnd (PPi (TacImp _ _ s rig) n _ ty sc) =
1766 depth d . bracket p startPrec $
1767 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1768 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1769 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1770 | basename neg == sUN "negate" =
1771 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1772 -- This case preserves the behavior of the former constructor PEq.
1773 -- It should be removed if feasible when the pretty-printing of infix
1774 -- operators in general is improved.
1775 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1776 | n == eqTy, ppopt_impl ppo =
1777 depth d . bracket p eqPrec $
1778 enclose lparen rparen eq <+>
1779 align (group (vsep (map (prettyArgS (decD d) bnd)
1782 depth d . bracket p eqPrec . align . group $
1783 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1784 where eq = annName eqTy (text "=")
1786 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1787 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1788 | UN nm <- basename f
1789 , not (ppopt_impl ppo) && null (getShowArgs args) =
1790 prettyName True (ppopt_impl ppo) bnd f
1791 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1792 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1793 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1794 | UN nm <- basename op
1796 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1797 case getShowArgs args of
1799 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1800 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1801 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1802 (l@(PExp{}) : r@(PExp{}) : rest) ->
1803 depth d . bracket p funcAppPrec $
1804 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1805 align (group (vsep (map (prettyArgS d bnd) rest)))
1806 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1807 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1808 f = getFixity (opStr op)
1810 Nothing -> funcAppPrec + 1
1811 Just (Infixl p') -> p'
1812 Just f' -> prec f' + 1
1814 Nothing -> funcAppPrec + 1
1815 Just (Infixr p') -> p'
1816 Just f' -> prec f' + 1
1817 inFix l r = align . group $
1818 (prettySe (decD d) left bnd l <+> opName False) <$>
1819 group (prettySe (decD d) right bnd r)
1820 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1821 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1822 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1823 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1824 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1825 let args = getShowArgs as
1826 fp = prettySe (decD d) (startPrec + 1) bnd f
1827 shownArgs = if ppopt_impl ppo then as else args
1829 depth d . bracket p funcAppPrec . group $
1832 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1833 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1834 prettySe d p bnd (PCase _ scr cases) =
1835 bracket p funcAppPrec $
1836 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1837 depth d (indent 2 (vsep (map ppcase cases)))
1839 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1840 ([(n, False) | n <- vars l] ++ bnd)
1841 in nest nestingSize $
1842 prettyCase l <+> text "=>" <+> prettyCase r
1843 -- Warning: this is a bit of a hack. At this stage, we don't have the
1844 -- global context, so we can't determine which names are constructors,
1845 -- which are types, and which are pattern variables on the LHS of the
1846 -- case pattern. We use the heuristic that names without a namespace
1847 -- are patvars, because right now case blocks in PTerms are always
1848 -- delaborated from TT before being sent to the pretty-printer. If they
1849 -- start getting printed directly, THIS WILL BREAK.
1850 -- Potential solution: add a list of known patvars to the cases in
1851 -- PCase, and have the delaborator fill it out, kind of like the pun
1852 -- disambiguation on PDPair.
1853 vars tm = filter noNS (allNamesIn tm)
1854 noNS (NS _ _) = False
1857 prettySe d p bnd (PIfThenElse _ c t f) =
1858 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1859 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1860 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1861 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1863 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1864 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1865 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1866 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1867 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1868 prettySe d p bnd (PRewrite _ by l r _) =
1869 depth d . bracket p startPrec $
1870 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1873 Just fn -> text "using" <+>
1874 prettyName True (ppopt_impl ppo) bnd fn) <+>
1875 text "in" <+> prettySe (decD d) startPrec bnd r
1876 prettySe d p bnd (PTyped l r) =
1877 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1878 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1879 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1880 align . group . vsep . punctuate (ann comma) $
1881 map (prettySe (decD d) startPrec bnd) elts
1882 where ann = case pun of
1884 IsType -> annName pairTy
1885 IsTerm -> annName pairCon
1886 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1887 | Just elts <- dPairElts dpair
1888 = depth d . enclose (annotated lparen) (annotated rparen) .
1889 align . group . vsep . punctuate (space <> annotated (text "**")) $
1895 annotated (text "**") <+>
1896 prettySe (decD d) startPrec (addBinding bnd) r <>
1898 where annotated = case pun of
1899 IsType -> annName sigmaTy
1900 IsTerm -> annName sigmaCon
1903 (left, addBinding) = case (l, pun) of
1904 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1905 _ -> (prettySe (decD d) startPrec bnd l, id)
1908 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1909 ppElts ((PRef _ _ n, t):rs) bs
1911 = (bindingOf n False <+> colon <+>
1912 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1913 ppElts ((l, t):rs) bs
1914 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1915 prettySe d p bnd (PAlternative ns a as) =
1916 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1919 foldr ((\ l r -> l <+> text "," <+> r) .
1920 depth d . prettySe (decD d) startPrec bnd)
1922 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1923 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1924 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1925 -- XXX: add pretty for tactics
1926 prettySe d p bnd (PProof ts) =
1927 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1928 prettySe d p bnd (PTactics ts) =
1929 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1930 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1931 prettySe d p bnd PImpossible = kwd "impossible"
1932 prettySe d p bnd Placeholder = text "_"
1933 prettySe d p bnd (PDoBlock dos) =
1934 bracket p startPrec $
1935 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1936 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1937 ppdo bnd (DoBind _ bn _ tm : dos) =
1938 (prettyBindingOf bn False <+> text "<-" <+>
1939 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1940 ppdo ((bn, False):bnd) dos
1941 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1942 text "no pretty printer for pattern-matching do binding" :
1944 ppdo bnd (DoLet _ ln _ ty v : dos) =
1945 (kwd "let" <+> prettyBindingOf ln False <+>
1946 (if ty /= Placeholder
1947 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1949 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1950 ppdo ((ln, False):bnd) dos
1951 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1952 text "no pretty printer for pattern-matching do binding" :
1955 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1956 prettySe d p bnd (PElabError s) = pretty s
1957 -- Quasiquote pprinting ignores bound vars
1958 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1959 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1960 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1961 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1962 where start = if res then "`{" else "`{{"
1963 end = if res then "}" else "}}"
1964 prettySe d p bnd (PRunElab _ tm _) =
1965 bracket p funcAppPrec . group . align . hang 2 $
1967 prettySe (decD d) funcAppPrec bnd tm
1968 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1969 prettySe d p bnd _ = text "missing pretty-printer for term"
1971 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1972 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1973 where display (UN n) = T.unpack n
1974 display (MN _ n) = T.unpack n
1975 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1976 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1979 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1980 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1981 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1982 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1984 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1985 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1986 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1987 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1989 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1990 annName n = annotate (AnnName n Nothing Nothing Nothing)
1992 opStr :: Name -> String
1993 opStr (NS n _) = opStr n
1994 opStr (UN n) = T.unpack n
1996 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1997 slist' (Just d) _ _ _ | d <= 0 = Nothing
1999 | containsHole e = Nothing
2000 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2001 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2002 slist' d p bnd (PRef _ _ nil)
2003 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2004 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2005 | nsroot cons == sUN "::",
2006 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2008 Just tl' <- slist' (decD d) p bnd tl
2009 = Just (prettySe d startPrec bnd hd : tl')
2011 isImp (PImp {}) = True
2013 slist' _ _ _ tm = Nothing
2015 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2017 [] -> annotate (AnnData "" "") $ text "[]"
2018 [x] -> enclose left right . group $ x
2019 xs -> enclose left right .
2020 align . group . vsep .
2021 punctuate comma $ xs
2022 where left = (annotate (AnnData "" "") (text "["))
2023 right = (annotate (AnnData "" "") (text "]"))
2024 comma = (annotate (AnnData "" "") (text ","))
2025 slist _ _ _ _ = Nothing
2027 pairElts :: PTerm -> Maybe [PTerm]
2028 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2029 | otherwise = Just [x, y]
2030 pairElts _ = Nothing
2032 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2033 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2034 | otherwise = Just [(l, t), (Placeholder, r)]
2035 dPairElts _ = Nothing
2037 natns = "Prelude.Nat."
2039 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2041 | ppopt_desugarnats ppo = Nothing
2042 | otherwise = snat' d p e
2044 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2045 snat' (Just x) _ _ | x <= 0 = Nothing
2046 snat' d p (PRef _ _ z)
2047 | show z == (natns++"Z") || show z == "Z" = Just 0
2048 snat' d p (PApp _ s [PExp {getTm=n}])
2049 | show s == (natns++"S") || show s == "S",
2050 Just n' <- snat' (decD d) p n
2052 snat' _ _ _ = Nothing
2054 bracket outer inner doc
2055 | outer > inner = lparen <> doc <> rparen
2058 ellipsis = text "..."
2061 depth (Just d) = if d <= 0 then const ellipsis else id
2063 decD = fmap (\x -> x - 1)
2065 kwd = annotate AnnKeyword . text
2067 fixities :: M.Map String Fixity
2068 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2070 getFixity :: String -> Maybe Fixity
2071 getFixity = flip M.lookup fixities
2073-- | Strip away namespace information
2074basename :: Name -> Name
2075basename (NS n _) = basename n
2078-- | Determine whether a name was the one inserted for a hole or guess
2079-- by the delaborator
2080isHoleName :: Name -> Bool
2081isHoleName (UN n) = n == T.pack "[__]"
2084-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2085containsHole :: PTerm -> Bool
2086containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2088-- | Pretty-printer helper for names that attaches the correct annotations
2089prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2090 -> Bool -- ^ whether to show namespaces
2091 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2092 -> Name -- ^ the name to pprint
2093 -> Doc OutputAnnotation
2094prettyName infixParen showNS bnd n
2095 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2096 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2097 | (UN n') <- n, T.unpack n' == "_" = text "_"
2098 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2099 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2100 where fullName = text nameSpace <> parenthesise (text (baseName n))
2101 baseName (UN n) = T.unpack n
2102 baseName (NS n ns) = baseName n
2103 baseName (MN i s) = T.unpack s
2104 baseName other = show other
2105 nameSpace = case n of
2106 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2108 isInfix = case baseName n of
2110 (c : _) -> not (isAlpha c)
2111 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2114showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2115showCImp ppo (PClause _ n l ws r w)
2116 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2117 <+> text "where" <+> text (show w)
2120 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2121showCImp ppo (PWith _ n l ws r pn w)
2122 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2123 <+> braces (text (show w))
2126 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2129showDImp :: PPOption -> PData -> Doc OutputAnnotation
2130showDImp ppo (PDatadecl n nfc ty cons)
2131 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2132 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2134showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2135showDecls o ds = vsep (map (showDeclImp o) ds)
2137showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2138showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2139showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2140 indent 2 (vsep (map (showCImp o) cs))
2141showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2142showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2143showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2144showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2145showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2146showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2147 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2148showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2149 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2150showDeclImp _ _ = text "..."
2151-- showDeclImp (PImport o) = "import " ++ o
2153getImps :: [PArg] -> [(Name, PTerm)]
2155getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2156getImps (_ : xs) = getImps xs
2158getExps :: [PArg] -> [PTerm]
2160getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2161getExps (_ : xs) = getExps xs
2163getShowArgs :: [PArg] -> [PArg]
2165getShowArgs (e@(PExp _ _ _ _) : xs) = e : getShowArgs xs
2166getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2167 | PImp _ _ _ _ tm <- e
2168 , containsHole tm = e : getShowArgs xs
2169getShowArgs (_ : xs) = getShowArgs xs
2171getConsts :: [PArg] -> [PTerm]
2173getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2174getConsts (_ : xs) = getConsts xs
2176getAll :: [PArg] -> [PTerm]
2181showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2182 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2183 -> PPOption -- ^ pretty printing options
2184 -> Bool -- ^ whether to colourise
2185 -> Name -- ^ the term to show
2187showName ist bnd ppo colour n = case ist of
2188 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2189 Nothing -> showbasic n
2190 where name = if ppopt_impl ppo then show n else showbasic n
2191 showbasic n@(UN _) = showCG n
2192 showbasic (MN i s) = str s
2193 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2194 showbasic (SN s) = show s
2196 colourise n t = let ctxt' = fmap tt_ctxt ist in
2199 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2200 else colouriseBound t name
2201 | isDConName n ctxt -> colouriseData t name
2202 | isFnName n ctxt -> colouriseFun t name
2203 | isTConName n ctxt -> colouriseType t name
2204 -- The assumption is that if a name is not bound and does not exist in the
2205 -- global context, then we're somewhere in which implicit info has been lost
2206 -- (like error messages). Thus, unknown vars are colourised as implicits.
2207 | otherwise -> colouriseImplicit t name
2209showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2210 -> PTerm -- ^ the term to show
2212showTm ist = displayDecorated (consoleDecorate ist) .
2213 renderPretty 0.8 100000 .
2214 prettyImp (ppOptionIst ist)
2216-- | Show a term with implicits, no colours
2217showTmImpls :: PTerm -> String
2218showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2220-- | Show a term with specific options
2221showTmOpts :: PPOption -> PTerm -> String
2222showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2225instance Sized PTerm where
2226 size (PQuote rawTerm) = size rawTerm
2227 size (PRef fc _ name) = size name
2228 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2229 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2230 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2231 size (PTyped trm ty) = 1 + size trm + size ty
2232 size (PApp fc name args) = 1 + size args
2233 size (PAppBind fc name args) = 1 + size args
2234 size (PCase fc trm bdy) = 1 + size trm + size bdy
2235 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2236 size (PTrue fc _) = 1
2237 size (PResolveTC fc) = 1
2238 size (PRewrite fc by left right _) = 1 + size left + size right
2239 size (PPair fc _ _ left right) = 1 + size left + size right
2240 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2241 size (PAlternative _ a alts) = 1 + size alts
2242 size (PHidden hidden) = size hidden
2243 size (PUnifyLog tm) = size tm
2244 size (PDisamb _ tm) = size tm
2245 size (PNoImplicits tm) = size tm
2247 size (PUniverse _ _) = 1
2248 size (PConstant fc const) = 1 + size fc + size const
2249 size Placeholder = 1
2250 size (PDoBlock dos) = 1 + size dos
2251 size (PIdiom fc term) = 1 + size term
2252 size (PMetavar _ name) = 1
2253 size (PProof tactics) = size tactics
2254 size (PElabError err) = size err
2255 size PImpossible = 1
2258getPArity :: PTerm -> Int
2259getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2262-- Return all names, free or globally bound, in the given term.
2264allNamesIn :: PTerm -> [Name]
2265allNamesIn tm = nub $ ni 0 [] tm
2266 where -- TODO THINK added niTacImp, but is it right?
2267 ni 0 env (PRef _ _ n)
2268 | not (n `elem` env) = [n]
2269 ni 0 env (PPatvar _ n) = [n]
2270 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2271 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2272 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2273 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2274 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2275 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2276 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2277 ni 0 env (PHidden tm) = ni 0 env tm
2278 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2279 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2280 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2281 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2282 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2283 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2284 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2285 ni 0 env (PUnifyLog tm) = ni 0 env tm
2286 ni 0 env (PDisamb _ tm) = ni 0 env tm
2287 ni 0 env (PNoImplicits tm) = ni 0 env tm
2289 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2290 ni i env (PUnquote tm) = ni (i - 1) env tm
2291 ni i env tm = concatMap (ni i env) (children tm)
2293 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2297-- Return all names defined in binders in the given term
2298boundNamesIn :: PTerm -> [Name]
2299boundNamesIn tm = S.toList (ni 0 S.empty tm)
2300 where -- TODO THINK Added niTacImp, but is it right?
2301 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2302 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2303 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2304 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2305 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2306 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2307 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2308 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2309 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2310 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2311 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2312 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2313 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2314 ni 0 set (PAlternative ns a as) = niTms 0 set as
2315 ni 0 set (PHidden tm) = ni 0 set tm
2316 ni 0 set (PUnifyLog tm) = ni 0 set tm
2317 ni 0 set (PDisamb _ tm) = ni 0 set tm
2318 ni 0 set (PNoImplicits tm) = ni 0 set tm
2320 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2321 ni i set (PUnquote tm) = ni (i - 1) set tm
2323 ni i set tm = foldr (S.union . ni i set) set (children tm)
2325 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2326 niTms i set [] = set
2327 niTms i set (x : xs) = niTms i (ni i set x) xs
2329 niTacImp i set (TacImp _ _ scr _) = ni i set scr
2330 niTacImp i set _ = set
2332-- Return names which are valid implicits in the given term (type).
2333implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2334implicitNamesIn uvars ist tm
2335 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2338 addImp n = do (imps, fns) <- get
2340 addFn n = do (imps, fns) <- get
2344 notCAF (PExp _ _ _ _ : _) = True
2345 notCAF (_ : xs) = notCAF xs
2347 notHidden (n, _) = case getAccessibility n of
2353 = case lookupDefAccExact n False (tt_ctxt ist) of
2357 ni 0 env (PRef _ _ n@(NS _ _))
2358 | not (n `elem` env)
2359 -- Never implicitly bind if there's a namespace
2361 ni 0 env (PRef _ _ n)
2362 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2363 ni 0 env (PApp _ f@(PRef _ _ n) as)
2364 | n `elem` uvars = do ni 0 env f
2365 mapM_ (ni 0 env . getTm) as
2366 | otherwise = do case lookupTy n (tt_ctxt ist) of
2369 mapM_ (ni 0 env . getTm) as
2370 ni 0 env (PApp _ f as) = do ni 0 env f
2371 mapM_ (ni 0 env . getTm) as
2372 ni 0 env (PAppBind _ f as) = do ni 0 env f
2373 mapM_ (ni 0 env . getTm) as
2374 ni 0 env (PCase _ c os) = do ni 0 env c
2375 -- names in 'os', not counting the names bound in the cases
2376 mapM_ (ni 0 env . snd) os
2379 mapM_ (ni 0 env . fst) os
2381 put (nub imps \\ nub impsfst, fns)
2382 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2383 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2384 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2385 ni 0 env (PLet fc n _ ty val sc) = do ni 0 env ty;
2386 ni 0 env val; ni 0 (n:env) sc
2387 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2388 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2389 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2390 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2391 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2394 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2395 ni 0 env (PHidden tm) = ni 0 env tm
2396 ni 0 env (PUnifyLog tm) = ni 0 env tm
2397 ni 0 env (PDisamb _ tm) = ni 0 env tm
2398 ni 0 env (PNoImplicits tm) = ni 0 env tm
2400 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2401 maybe (return ()) (ni i env) ty
2402 ni i env (PUnquote tm) = ni (i - 1) env tm
2404 ni i env tm = mapM_ (ni i env) (children tm)
2406-- Return names which are free in the given term.
2407namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2408namesIn uvars ist tm = nub $ ni 0 [] tm
2410 ni 0 env (PRef _ _ n)
2411 | not (n `elem` env)
2412 = case lookupTy n (tt_ctxt ist) of
2414 _ -> [n | n `elem` (map fst uvars)]
2415 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2416 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2417 ni 0 env (PCase _ c os) = ni 0 env c ++
2418 -- names in 'os', not counting the names bound in the cases
2419 (nub (concatMap (ni 0 env . snd) os)
2420 \\ nub (concatMap (ni 0 env . fst) os))
2421 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2422 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2423 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2424 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2425 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2426 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2427 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2428 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2429 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2430 ni 0 env (PHidden tm) = ni 0 env tm
2431 ni 0 env (PUnifyLog tm) = ni 0 env tm
2432 ni 0 env (PDisamb _ tm) = ni 0 env tm
2433 ni 0 env (PNoImplicits tm) = ni 0 env tm
2435 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2436 ni i env (PUnquote tm) = ni (i - 1) env tm
2438 ni i env tm = concatMap (ni i env) (children tm)
2440 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2443-- Return which of the given names are used in the given term.
2445usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2446usedNamesIn vars ist tm = nub $ ni 0 [] tm
2447 where -- TODO THINK added niTacImp, but is it right?
2448 ni 0 env (PRef _ _ n)
2449 | n `elem` vars && not (n `elem` env)
2450 = case lookupDefExact n (tt_ctxt ist) of
2453 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2454 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2455 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2456 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2457 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2458 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2459 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2460 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2461 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2462 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2463 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2464 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2465 ni 0 env (PHidden tm) = ni 0 env tm
2466 ni 0 env (PUnifyLog tm) = ni 0 env tm
2467 ni 0 env (PDisamb _ tm) = ni 0 env tm
2468 ni 0 env (PNoImplicits tm) = ni 0 env tm
2470 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2471 ni i env (PUnquote tm) = ni (i - 1) env tm
2473 ni i env tm = concatMap (ni i env) (children tm)
2475 niTacImp i env (TacImp _ _ scr _) = ni i env scr
2478-- Return the list of inaccessible (= dotted) positions for a name.
2479getErasureInfo :: IState -> Name -> [Int]
2480getErasureInfo ist n =
2481 case lookupCtxtExact n (idris_optimisation ist) of
2482 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