2Module : Idris.AbsSyntaxTree
3Description : Core data definitions used in Idris.
6Maintainer : The Idris Community.
8{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric,
9 FlexibleInstances, MultiParamTypeClasses, PatternGuards,
10 TypeSynonymInstances #-}
12module Idris.AbsSyntaxTree where
15import Idris.Core.Elaborate hiding (Tactic(..))
16import Idris.Core.Evaluate
18import Idris.Core.Typecheck
19import Idris.Docstrings
20import IRTS.CodegenCommon
22import Util.DynamicLinker
25import Prelude hiding ((<$>))
27import Control.Applicative ((<|>))
28import qualified Control.Monad.Trans.Class as Trans (lift)
29import Control.Monad.Trans.Except
30import Control.Monad.Trans.State.Strict
32import Data.Data (Data)
34import Data.Foldable (Foldable)
35import Data.Function (on)
36import Data.Generics.Uniplate.Data (children, universe)
37import Data.List hiding (group)
38import qualified Data.Map.Strict as M
39import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
40import qualified Data.Set as S
41import qualified Data.Text as T
42import Data.Traversable (Traversable)
44import Data.Word (Word)
46import GHC.Generics (Generic)
47import Network.Socket (PortNumber)
48import System.Console.Haskeline
50import Text.PrettyPrint.Annotated.Leijen
52data ElabWhat = ETypes | EDefns | EAll
55-- | Data to pass to recursively called elaborators; e.g. for where blocks,
56-- paramaterised declarations, etc.
58-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
59-- so that we can have mutually recursive elaborators in separate modules without
60-- having to muck about with cyclic modules.
61data ElabInfo = EInfo {
62 params :: [(Name, PTerm)]
63 , inblock :: Ctxt [Name] -- ^ names in the block, and their params
64 , liftname :: Name -> Name
65 , namespace :: [String]
67 , constraintNS :: String -- ^ filename for adding to constraint variables
70 -- | We may, recursively, collect transformations to do on the rhs,
71 -- e.g. rewriting recursive calls to functions defined by 'with'
72 , rhs_trans :: PTerm -> PTerm
73 , rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
77toplevel = EInfo [] emptyContext id [] Nothing "(toplevel)" 0 id (\_ _ _ -> fail "Not implemented")
79toplevelWith :: String -> ElabInfo
80toplevelWith ns = EInfo [] emptyContext id [] Nothing ns 0 id (\_ _ _ -> fail "Not implemented")
82eInfoNames :: ElabInfo -> [Name]
83eInfoNames info = map fst (params info) ++ M.keys (inblock info)
85data IOption = IOption {
87 , opt_logcats :: [LogCat] -- ^ List of logging categories.
88 , opt_typecase :: Bool
89 , opt_typeintype :: Bool
90 , opt_coverage :: Bool
91 , opt_showimp :: Bool -- ^ show implicits
92 , opt_errContext :: Bool
95 , opt_nobanner :: Bool
97 , opt_codegen :: Codegen
98 , opt_outputTy :: OutputType
99 , opt_ibcsubdir :: FilePath
100 , opt_importdirs :: [FilePath]
101 , opt_sourcedirs :: [FilePath]
102 , opt_triple :: String
104 , opt_cmdline :: [Opt] -- ^ remember whole command line
105 , opt_origerr :: Bool
106 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
107 , opt_autoImport :: [FilePath] -- ^ List of modules to auto import i.e. `Builtins+Prelude`
108 , opt_optimise :: [Optimisation]
109 , opt_printdepth :: Maybe Int
110 , opt_evaltypes :: Bool -- ^ normalise types in `:t`
111 , opt_desugarnats :: Bool
112 , opt_autoimpls :: Bool
113 } deriving (Show, Eq, Generic)
115defaultOpts = IOption { opt_logLevel = 0
117 , opt_typecase = False
118 , opt_typeintype = False
119 , opt_coverage = True
120 , opt_showimp = False
121 , opt_errContext = False
124 , opt_nobanner = False
126 , opt_codegen = Via IBCFormat "c"
127 , opt_outputTy = Executable
129 , opt_importdirs = []
130 , opt_sourcedirs = []
134 , opt_origerr = False
135 , opt_autoSolve = True
136 , opt_autoImport = []
137 , opt_optimise = defaultOptimise
138 , opt_printdepth = Just 5000
139 , opt_evaltypes = True
140 , opt_desugarnats = False
141 , opt_autoimpls = True
144data PPOption = PPOption {
145 ppopt_impl :: Bool -- ^ whether to show implicits
146 , ppopt_desugarnats :: Bool
147 , ppopt_pinames :: Bool -- ^ whether to show names in pi bindings
148 , ppopt_depth :: Maybe Int
151data Optimisation = PETransform -- ^ partial eval and associated transforms
152 deriving (Show, Eq, Generic)
154defaultOptimise = [PETransform]
156-- | Pretty printing options with default verbosity.
157defaultPPOption :: PPOption
158defaultPPOption = PPOption {
160 , ppopt_desugarnats = False
161 , ppopt_pinames = False
162 , ppopt_depth = Nothing
165-- | Pretty printing options with the most verbosity.
166verbosePPOption :: PPOption
167verbosePPOption = PPOption {
169 , ppopt_desugarnats = True
170 , ppopt_pinames = True
171 , ppopt_depth = Nothing
174-- | Get pretty printing options from the big options record.
175ppOption :: IOption -> PPOption
176ppOption opt = PPOption {
177 ppopt_impl = opt_showimp opt
178 , ppopt_pinames = False
179 , ppopt_depth = opt_printdepth opt
180 , ppopt_desugarnats = opt_desugarnats opt
183-- | Get pretty printing options from an idris state record.
184ppOptionIst :: IState -> PPOption
185ppOptionIst = ppOption . idris_options
187data LanguageExt = TypeProviders | ErrorReflection
188 deriving (Show, Eq, Read, Ord, Generic)
190-- | The output mode in use
191data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
192 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
195-- | How wide is the console?
196data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
197 | ColsWide Int -- ^ Manually specified - must be positive
198 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
199 deriving (Show, Eq, Generic)
201-- | If a function has no totality annotation, what do we assume?
202data DefaultTotality = DefaultCheckingTotal -- ^ Total
203 | DefaultCheckingPartial -- ^ Partial
204 | DefaultCheckingCovering -- ^Total coverage, but may diverge
205 deriving (Show, Eq, Generic)
207-- | The global state used in the Idris monad
208data IState = IState {
209 tt_ctxt :: Context -- ^ All the currently defined names and their terms
210 , idris_constraints :: S.Set ConstraintFC -- ^ A list of universe constraints and their corresponding source locations
211 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators
212 , idris_implicits :: Ctxt [PArg]
213 , idris_statics :: Ctxt [Bool]
214 , idris_interfaces :: Ctxt InterfaceInfo
215 , idris_openimpls :: [Name] -- ^ Privileged implementations, will resolve immediately
216 , idris_records :: Ctxt RecordInfo
217 , idris_dsls :: Ctxt DSL
218 , idris_optimisation :: Ctxt OptInfo
219 , idris_datatypes :: Ctxt TypeInfo
220 , idris_namehints :: Ctxt [Name]
222 -- | list of lhs/rhs, and a list of missing clauses. These are not
224 , idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
225 , idris_flags :: Ctxt [FnOpt]
226 , idris_callgraph :: Ctxt CGInfo -- ^ name, args used in each pos
227 , idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
229 -- | module documentation is saved in a special MN so the context
230 -- mechanism can be used for disambiguation.
231 , idris_moduledocs :: Ctxt (Docstring DocTerm)
232 , idris_tyinfodata :: Ctxt TIData
233 , idris_fninfo :: Ctxt FnInfo
234 , idris_transforms :: Ctxt [(Term, Term)]
235 , idris_autohints :: Ctxt [Name]
236 , idris_totcheck :: [(FC, Name)] -- ^ names to check totality on
237 , idris_defertotcheck :: [(FC, Name)] -- ^ names to check at the end
238 , idris_totcheckfail :: [(FC, String)]
239 , idris_options :: IOption
241 , idris_lineapps :: [((FilePath, Int), PTerm)] -- ^ Full application LHS on source line
243 -- | The currently defined but not proven metavariables. The Int is
244 -- the number of vars to display as a context, the Maybe Name is its
245 -- top-level function, the [Name] is the list of local variables
246 -- available for proof search and the Bools are whether :p is
247 -- allowed, and whether the variable is definable at all
248 -- (Metavariables are not definable if they are applied in a term
249 -- which still has hole bindings)
250 , idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
251 , idris_coercions :: [Name]
252 , idris_errRev :: [(Term, Term)]
253 , syntax_rules :: SyntaxRules
254 , syntax_keywords :: [String]
255 , imported :: [FilePath] -- ^ The imported modules
256 , idris_scprims :: [(Name, (Int, PrimFn))]
257 , idris_objs :: [(Codegen, FilePath)]
258 , idris_libs :: [(Codegen, String)]
259 , idris_cgflags :: [(Codegen, String)]
260 , idris_hdrs :: [(Codegen, String)]
261 , idris_imported :: [(FilePath, Bool)] -- ^ Imported ibc file names, whether public
262 , proof_list :: [(Name, (Bool, [String]))]
263 , errSpan :: Maybe FC
264 , parserWarnings :: [(FC, Err)]
265 , lastParse :: Maybe Name
266 , indent_stack :: [Int]
267 , brace_stack :: [Maybe Int]
268 , lastTokenSpan :: Maybe FC -- ^ What was the span of the latest token parsed?
269 , idris_parsedSpan :: Maybe FC
270 , hide_list :: Ctxt Accessibility
271 , default_access :: Accessibility
272 , default_total :: DefaultTotality
273 , ibc_write :: [IBCWrite]
274 , compiled_so :: Maybe String
275 , idris_dynamic_libs :: [DynamicLib]
276 , idris_language_extensions :: [LanguageExt]
277 , idris_outputmode :: OutputMode
278 , idris_colourRepl :: Bool
279 , idris_colourTheme :: ColourTheme
280 , idris_errorhandlers :: [Name] -- ^ Global error handlers
281 , idris_nameIdx :: (Int, Ctxt (Int, Name))
282 , idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers
283 , module_aliases :: M.Map [T.Text] [T.Text]
284 , idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
285 , idris_postulates :: S.Set Name
286 , idris_externs :: S.Set (Name, Int)
287 , idris_erasureUsed :: [(Name, Int)] -- ^ Function/constructor name, argument position is used
288 , idris_whocalls :: Maybe (M.Map Name [Name])
289 , idris_callswho :: Maybe (M.Map Name [Name])
291 -- | List of names that were defined in the repl, and can be re-/un-defined
292 , idris_repl_defs :: [Name]
294 -- | Stack of names currently being elaborated, Bool set if it's an
295 -- implementation (implementations appear twice; also as a funtion name)
296 , elab_stack :: [(Name, Bool)]
299 , idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
300 , idris_exports :: [Name] -- ^ Functions with ExportList
301 , idris_highlightedRegions :: [(FC, OutputAnnotation)] -- ^ Highlighting information to output
302 , idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
303 , idris_deprecated :: Ctxt String -- ^ Deprecated names and explanation
304 , idris_inmodule :: S.Set Name -- ^ Names defined in current module
305 , idris_ttstats :: M.Map Term (Int, Term)
306 , idris_fragile :: Ctxt String -- ^ Fragile names and explanation.
310-- Required for parsers library, and therefore trifecta
311instance Show IState where
312 show = const "{internal state}"
314data SizeChange = Smaller | Same | Bigger | Unknown
315 deriving (Show, Eq, Generic)
317deriving instance Binary SizeChange
320type SCGEntry = (Name, [Maybe (Int, SizeChange)])
321type UsageReason = (Name, Int) -- fn_name, its_arg_number
323data CGInfo = CGInfo {
324 calls :: [Name] -- Immediate calls
325 , allCalls :: Maybe [Name] -- Calls and descendents (built as required, for PE)
327 , usedpos :: [(Int, [UsageReason])]
328 } deriving (Show, Generic)
330deriving instance Binary CGInfo
333primDefs = [ sUN "unsafePerformPrimIO"
334 , sUN "mkLazyForeignPrim"
335 , sUN "mkForeignPrim"
337 , sUN "assert_unreachable"
340-- information that needs writing for the current module's .ibc file
341data IBCWrite = IBCFix FixDecl
346 | IBCImplementation Bool Bool Name Name
353 | IBCImport (Bool, FilePath) -- ^ True = import public
354 | IBCImportDir FilePath
355 | IBCSourceDir FilePath
356 | IBCObj Codegen FilePath
357 | IBCLib Codegen String
358 | IBCCGFlag Codegen String
360 | IBCHeader Codegen String
361 | IBCAccess Name Accessibility
362 | IBCMetaInformation Name MetaInformation
363 | IBCTotal Name Totality
364 | IBCInjective Name Injectivity
366 | IBCFnInfo Name FnInfo
367 | IBCTrans Name (Term, Term)
368 | 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)
390-- | The initial state for the compiler
392idrisInit = IState initContext S.empty []
393 emptyContext emptyContext emptyContext [] emptyContext
394 emptyContext emptyContext emptyContext emptyContext
395 emptyContext emptyContext emptyContext emptyContext
396 emptyContext emptyContext emptyContext emptyContext
398 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
399 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private DefaultCheckingPartial [] Nothing [] []
400 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
401 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
402 emptyContext S.empty M.empty emptyContext
405-- | The monad for the main REPL - reading and processing files and
406-- updating global state (hence the IO inner monad).
409-- type Idris = WriterT [Either String (IO ())] (State IState a))
412type Idris = StateT IState (ExceptT Err IO)
414catchError :: Idris a -> (Err -> Idris a) -> Idris a
415catchError = liftCatch catchE
417throwError :: Err -> Idris a
418throwError = Trans.lift . throwE
420-- Commands in the REPL
422data Codegen = Via IRFormat String
424 deriving (Show, Eq, Generic)
426data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)
428data HowMuchDocs = FullDocs | OverviewDocs
430data OutputFmt = HTMLOutput | LaTeXOutput
432-- | Recognised logging categories for the Idris compiler.
434-- @TODO add in sub categories.
441 deriving (Show, Eq, Ord, Generic)
443strLogCat :: LogCat -> String
444strLogCat IParse = "parser"
445strLogCat IElab = "elab"
446strLogCat ICodeGen = "codegen"
447strLogCat IErasure = "erasure"
448strLogCat ICoverage = "coverage"
449strLogCat IIBC = "ibc"
451codegenCats :: [LogCat]
452codegenCats = [ICodeGen]
454parserCats :: [LogCat]
460loggingCatsStr :: String
461loggingCatsStr = unlines
464 , (strLogCat ICodeGen)
465 , (strLogCat IErasure)
466 , (strLogCat ICoverage)
471data ElabShellCmd = EQED
479 | EDocStr (Either Name Const)
482data Opt = Filename String
497 | NoBuiltins -- only for the really primitive stuff!
514 | Port REPLPort -- ^ REPL TCP port
523 | PkgDocBuild String -- IdrisDoc
524 | PkgDocInstall String
534 | OutputTy OutputType
535 | Extension LanguageExt
536 | InterpretScript String
538 | TargetTriple String
541 | AddOpt Optimisation
542 | RemoveOpt Optimisation
545 | AutoWidth -- ^ Automatically adjust terminal width
546 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
547 | UseConsoleWidth ConsoleWidth
550 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
551 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
552 deriving (Show, Eq, Generic)
554data REPLPort = DontListen | ListenPort PortNumber
555 deriving (Eq, Generic, Show)
557-- Parsed declarations
559data Fixity = Infixl { prec :: Int }
560 | Infixr { prec :: Int }
561 | InfixN { prec :: Int }
562 | PrefixN { prec :: Int }
563 deriving (Eq, Generic)
565deriving instance Binary Fixity
568instance Show Fixity where
569 show (Infixl i) = "infixl " ++ show i
570 show (Infixr i) = "infixr " ++ show i
571 show (InfixN i) = "infix " ++ show i
572 show (PrefixN i) = "prefix " ++ show i
574data FixDecl = Fix Fixity String
575 deriving (Eq, Generic)
577instance Show FixDecl where
578 show (Fix f s) = show f ++ " " ++ s
581deriving instance Binary FixDecl
584instance Ord FixDecl where
585 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
588data Static = Static | Dynamic
589 deriving (Show, Eq, Ord, Data, Generic, Typeable)
591deriving instance Binary Static
594-- ^ Mark bindings with their explicitness, and laziness
595data Plicity = Imp { pargopts :: [ArgOpt]
598 , pscoped :: Maybe ImplicitInfo -- ^ Nothing, if top level
599 , pinsource :: Bool -- ^ Explicitly written in source
601 | Exp { pargopts :: [ArgOpt]
603 , pparam :: Bool -- ^ this is a param (rather than index)
605 | Constraint { pargopts :: [ArgOpt]
608 | TacImp { pargopts :: [ArgOpt]
612 deriving (Show, Eq, Ord, Data, Generic, Typeable)
615deriving instance Binary Plicity
618is_scoped :: Plicity -> Maybe ImplicitInfo
619is_scoped (Imp _ _ _ s _) = s
623impl = Imp [] Dynamic False (Just (Impl False True False)) False
624-- Machine generated top level implicit
625impl_gen = Imp [] Dynamic False (Just (Impl False True True)) False
628forall_imp = Imp [] Dynamic False (Just (Impl False False True)) False
629forall_constraint = Imp [] Dynamic False (Just (Impl True False True)) False
631expl = Exp [] Dynamic False
632expl_param = Exp [] Dynamic True
634constraint = Constraint [] Static
636tacimpl t = TacImp [] Dynamic t
638data FnOpt = Inlinable -- ^ always evaluate when simplifying
639 | TotalFn | PartialFn | CoveringFn
640 | AllGuarded -- ^ all delayed arguments guaranteed guarded by constructors
643 -- | interface dictionary, eval only when a function
644 -- argument, and further evaluation results.
646 | OverlappingDictionary -- ^ Interface dictionary which may overlap
647 | Implicit -- ^ implicit coercion
648 | NoImplicit -- ^ do not apply implicit coercions
649 | CExport String -- ^ export, with a C name
650 | ErrorHandler -- ^ an error handler for use with the ErrorReflection extension
651 | ErrorReverse -- ^ attempt to reverse normalise before showing in error
652 | Reflection -- ^ a reflecting function, compile-time only
653 | Specialise [(Name, Maybe Int)] -- ^ specialise it, freeze these names
654 | UnfoldIface Name [Name]
655 -- ^ Unfold given interface name in the definition, the
656 -- top level methods, and anything which has
657 -- the interface name as an argument. This is to unfold
658 -- things for termination checking, as interfaces will otherwise
660 | Constructor -- ^ Data constructor type
661 | AutoHint -- ^ use in auto implicit search
662 | PEGenerated -- ^ generated by partial evaluator
663 | StaticFn -- ^ Marked static, to be evaluated by partial evaluator
664 deriving (Show, Eq, Generic)
666deriving instance Binary FnOpt
671inlinable :: FnOpts -> Bool
672inlinable = elem Inlinable
674dictionary :: FnOpts -> Bool
675dictionary = elem Dictionary
678-- | Type provider - what to provide
679data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
680 | ProvPostulate t -- ^ goal type must be Type, so only term
681 deriving (Show, Eq, Functor, Generic)
683type ProvideWhat = ProvideWhat' PTerm
685-- | Top-level declarations such as compiler directives, definitions,
686-- datatypes and interfaces.
688 -- | Fixity declaration
689 = PFix FC Fixity [String]
690 -- | Type declaration (last FC is precise name location)
691 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
692 -- | Postulate, second FC is precise name location
693 | PPostulate Bool -- external def if true
694 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
696 | PClauses FC FnOpts Name [PClause' t]
697 -- | Top level constant
699 -- | Data declaration.
700 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
702 | PParams FC [(Name, t)] [PDecl' t]
703 -- | Open block/declaration
704 | POpenInterfaces FC [Name] [PDecl' t]
705 -- | New namespace, where FC is accurate location of the namespace
707 | PNamespace String FC [PDecl' t]
709 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
711 FC -- Record name precise location
712 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
713 [(Name, Docstring (Either Err t))] -- Param Docs
714 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
715 (Maybe (Name, FC)) -- Optional constructor name and location
716 (Docstring (Either Err t)) -- Constructor doc
717 SyntaxInfo -- Constructor SyntaxInfo
719 -- | Interface: arguments are documentation, syntax info, source
720 -- location, constraints, interface name, interface name location,
721 -- parameters, method declarations, optional constructor name
722 | PInterface (Docstring (Either Err t)) SyntaxInfo FC
723 [(Name, t)] -- constraints
724 Name -- interface name
725 FC -- accurate location of interface name
726 [(Name, FC, t)] -- parameters and precise locations
727 [(Name, Docstring (Either Err t))] -- parameter docstrings
728 [(Name, FC)] -- determining parameters and precise locations
729 [PDecl' t] -- declarations
730 (Maybe (Name, FC)) -- implementation constructor name and location
731 (Docstring (Either Err t)) -- implementation constructor docs
733 -- | Implementation declaration: arguments are documentation, syntax
734 -- info, source location, constraints, interface name, parameters, full
735 -- Implementation type, optional explicit name, and definitions
736 | PImplementation (Docstring (Either Err t)) -- Implementation docs
737 [(Name, Docstring (Either Err t))] -- Parameter docs
739 FC [(Name, t)] -- constraints
740 [Name] -- parent dictionaries to search for constraints
744 FC -- precise location of interface
746 [(Name, t)] -- Extra names in scope in the body
747 t -- full Implementation type
748 (Maybe Name) -- explicit name
750 | PDSL Name (DSL' t) -- ^ DSL declaration
751 | PSyntax FC Syntax -- ^ Syntax definition
752 | PMutual FC [PDecl' t] -- ^ Mutual block
753 | PDirective Directive -- ^ Compiler directive.
755 -- | Type provider. The first t is the type, the second is the
756 -- term. The second FC is precise highlighting location.
757 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
759 -- | Source-to-source transformation rule. If bool is True, lhs and
760 -- rhs must be convertible.
761 | PTransform FC Bool t t
763 -- | FC is decl-level, for errors, and Strings represent the
765 | PRunElabDecl FC t [String]
766 deriving (Functor, Generic)
768deriving instance Binary PDecl'
771-- | The set of source directives
772data Directive = DLib Codegen String
773 | DLink Codegen String
774 | DFlag Codegen String
775 | DInclude Codegen String
780 | DSetTotal Name -- assert totality after checking
781 | DAccess Accessibility
782 | DDefault DefaultTotality
784 | DDynamicLibs [String]
785 | DNameHint Name FC [(Name, FC)]
786 | DErrorHandlers Name FC Name FC [(Name, FC)]
787 | DLanguage LanguageExt
788 | DDeprecate Name String
789 | DFragile Name String
790 | DAutoImplicits Bool
794-- | A set of instructions for things that need to happen in IState
795-- after a term elaboration when there's been reflected elaboration.
796data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
797 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
798 | RAddImplementation Name Name
799 | RDatatypeDeclInstrs Name [PArg]
800 -- | Datatype, constructors
801 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
804-- | For elaborator state
805data EState = EState {
806 case_decls :: [(Name, PDecl)]
807 , delayed_elab :: [(Int, Elab' EState ())]
808 , new_tyDecls :: [RDeclInstructions]
809 , highlighting :: [(FC, OutputAnnotation)]
810 , auto_binds :: [Name] -- ^ names bound as auto implicits
811 , implicit_warnings :: [(FC, Name)] -- ^ Implicit warnings to report (location and global name)
815initEState = EState [] [] [] [] [] []
817type ElabD a = Elab' EState a
819highlightSource :: FC -> OutputAnnotation -> ElabD ()
820highlightSource fc annot =
821 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
823-- | One clause of a top-level definition. Term arguments to constructors are:
825-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
827-- 2. The list of extra 'with' patterns
829-- 3. The right-hand side
831-- 4. The where block (PDecl' t)
833data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
834 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
835 | PClauseR FC [t] t [PDecl' t]
836 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
837 deriving (Functor, Generic)
839deriving instance Binary PClause'
844 -- | Data declaration
845 PDatadecl { d_name :: Name -- ^ The name of the datatype
846 , d_name_fc :: FC -- ^ The precise location of the type constructor name
847 , d_tcon :: t -- ^ Type constructor
848 , d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
850 -- | "Placeholder" for data whose constructors are defined later
851 | PLaterdecl { d_name :: Name
854 } deriving (Functor, Generic)
856-- | Transform the FCs in a PData and its associated terms. The first
857-- function transforms the general-purpose FCs, and the second
858-- transforms those that are used for semantic source highlighting, so
859-- they can be treated specially.
860mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
861mapPDataFC f g (PDatadecl n nfc tycon ctors) =
862 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
863 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
864 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
865mapPDataFC f g (PLaterdecl n nfc tycon) =
866 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
868deriving instance Binary PData'
871-- Handy to get a free function for applying PTerm -> PTerm functions
872-- across a program, by deriving Functor
874type PDecl = PDecl' PTerm
875type PData = PData' PTerm
876type PClause = PClause' PTerm
878-- | Transform the FCs in a PTerm. The first function transforms the
879-- general-purpose FCs, and the second transforms those that are used
880-- for semantic source highlighting, so they can be treated specially.
881mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
882mapPDeclFC f g (PFix fc fixity ops) =
883 PFix (f fc) fixity ops
884mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
885 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
886mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
887 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
889mapPDeclFC f g (PClauses fc opts n clauses) =
890 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
891mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
892mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
893 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
894mapPDeclFC f g (PParams fc params decls) =
896 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
897 (map (mapPDeclFC f g) decls)
898mapPDeclFC f g (POpenInterfaces fc ifs decls) =
899 POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)
900mapPDeclFC f g (PNamespace ns fc decls) =
901 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
902mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
903 PRecord doc syn (f fc) opts n (g nfc)
904 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
906 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
907 plic, mapPTermFC f g ty, fdoc))
909 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
912mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
913 PInterface doc syn (f fc)
914 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
915 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
916 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
917 (map (mapPDeclFC f g) body)
918 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
920mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =
921 PImplementation doc paramDocs syn (f fc)
922 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
923 pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)
924 (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)
925 (mapPTermFC f g implTy)
927 (map (mapPDeclFC f g) body)
928mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
929mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
931 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
932 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
933mapPDeclFC f g (PMutual fc decls) =
934 PMutual (f fc) (map (mapPDeclFC f g) decls)
935mapPDeclFC f g (PDirective d) =
938 DNameHint n nfc ns ->
939 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
940 DErrorHandlers n nfc n' nfc' ns ->
941 DErrorHandlers n (g nfc) n' (g nfc') $
942 map (\(an, anfc) -> (an, g anfc)) ns
943mapPDeclFC f g (PProvider doc syn fc nfc what n) =
944 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
945mapPDeclFC f g (PTransform fc safe l r) =
946 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
947mapPDeclFC f g (PRunElabDecl fc script ns) =
948 PRunElabDecl (f fc) (mapPTermFC f g script) ns
950-- | Get all the names declared in a declaration
951declared :: PDecl -> [Name]
952declared (PFix _ _ _) = []
953declared (PTy _ _ _ _ _ n fc t) = [n]
954declared (PPostulate _ _ _ _ _ _ n t) = [n]
955declared (PClauses _ _ n _) = [] -- not a declaration
956declared (PCAF _ n _) = [n]
957declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
958 where fstt (_, _, a, _, _, _, _) = a
959declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
960declared (PParams _ _ ds) = concatMap declared ds
961declared (POpenInterfaces _ _ ds) = concatMap declared ds
962declared (PNamespace _ _ ds) = concatMap declared ds
963declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
964declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
965declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
969declared (PDSL n _) = [n]
970declared (PSyntax _ _) = []
971declared (PMutual _ ds) = concatMap declared ds
972declared (PDirective _) = []
975-- get the names declared, not counting nested parameter blocks
976tldeclared :: PDecl -> [Name]
977tldeclared (PFix _ _ _) = []
978tldeclared (PTy _ _ _ _ _ n _ t) = [n]
979tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
980tldeclared (PClauses _ _ n _) = [] -- not a declaration
981tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
982tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
983 where fstt (_, _, a, _, _, _, _) = a
984tldeclared (PParams _ _ ds) = []
985tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds
986tldeclared (PMutual _ ds) = concatMap tldeclared ds
987tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
988tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
989tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
995defined :: PDecl -> [Name]
996defined (PFix _ _ _) = []
997defined (PTy _ _ _ _ _ n _ t) = []
998defined (PPostulate _ _ _ _ _ _ n t) = []
999defined (PClauses _ _ n _) = [n] -- not a declaration
1000defined (PCAF _ n _) = [n]
1001defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
1002 where fstt (_, _, a, _, _, _, _) = a
1003defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
1004defined (PParams _ _ ds) = concatMap defined ds
1005defined (POpenInterfaces _ _ ds) = concatMap defined ds
1006defined (PNamespace _ _ ds) = concatMap defined ds
1007defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
1008defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
1009defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)
1013defined (PDSL n _) = [n]
1014defined (PSyntax _ _) = []
1015defined (PMutual _ ds) = concatMap defined ds
1016defined (PDirective _) = []
1019updateN :: [(Name, Name)] -> Name -> Name
1020updateN ns n | Just n' <- lookup n ns = n'
1023updateNs :: [(Name, Name)] -> PTerm -> PTerm
1025updateNs ns t = mapPT updateRef t
1026 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
1029-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
1030-- updateDNs [] t = t
1031-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
1032-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1033-- where updateCNs ns (PClause n l ts r ds)
1034-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1035-- (map (fmap (updateNs ns)) ts)
1036-- (fmap (updateNs ns) r)
1037-- (map (updateDNs ns) ds)
1038-- updateDNs ns c = c
1040data PunInfo = IsType
1043 deriving (Eq, Show, Ord, Data, Typeable, Generic)
1045-- | High level language terms
1046data PTerm = PQuote Raw -- ^ Inclusion of a core term into the
1047 -- high-level language
1049 -- ^ A reference to a variable. The FC is its precise
1050 -- source location for highlighting. The list of FCs is a
1051 -- collection of additional highlighting locations.
1052 | PInferRef FC [FC] Name -- ^ A name to be defined later
1053 | PPatvar FC Name -- ^ A pattern variable
1054 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1055 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1056 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1057 | PTyped PTerm PTerm -- ^ Term with explicit type
1058 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1059 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1060 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1061 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1062 | PMatchApp FC Name -- ^ Make an application by type matching
1063 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1064 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1065 | PTrue FC PunInfo -- ^ Unit type..?
1066 | PResolveTC FC -- ^ Solve this dictionary by interface resolution
1067 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1068 -- ^ "rewrite" syntax, with optional rewriting function and
1069 -- optional result type
1070 | PPair FC [FC] PunInfo PTerm PTerm
1071 -- ^ A pair (a, b) and whether it's a product type or a
1072 -- pair (solved by elaboration). The list of FCs is its
1074 | PDPair FC [FC] PunInfo PTerm PTerm PTerm
1075 -- ^ A dependent pair (tm : a ** b) and whether it's a
1076 -- sigma type or a pair that inhabits one (solved by
1077 -- elaboration). The [FC] is its punctuation.
1078 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1079 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1080 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1081 | PType FC -- ^ 'Type' type
1082 | PUniverse FC Universe -- ^ Some universe
1083 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1084 | PConstant FC Const -- ^ Builtin types
1085 | Placeholder -- ^ Underscore
1086 | PDoBlock [PDo] -- ^ Do notation
1087 | PIdiom FC PTerm -- ^ Idiom brackets
1088 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1089 | PProof [PTactic] -- ^ Proof script
1090 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1091 | PElabError Err -- ^ Error to report on elaboration
1092 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1093 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1094 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1095 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1096 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1097 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1098 | PUnquote PTerm -- ^ ~Term
1099 | PQuoteName Name Bool FC
1100 -- ^ `{n} where the FC is the precise highlighting for
1101 -- the name in particular. If the Bool is False, then
1102 -- it's `{{n}} and the name won't be resolved.
1103 | PRunElab FC PTerm [String]
1104 -- ^ %runElab tm - New-style proof script. Args are
1105 -- location, script, enclosing namespace.
1106 | PConstSugar FC PTerm
1107 -- ^ A desugared constant. The FC is a precise source
1108 -- location that will be used to highlight it later.
1109 deriving (Eq, Ord, Data, Typeable, Generic)
1111data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1114 deriving (Eq, Ord, Data, Generic, Typeable)
1116-- | Transform the FCs in a PTerm. The first function transforms the
1117-- general-purpose FCs, and the second transforms those that are used
1118-- for semantic source highlighting, so they can be treated specially.
1119mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1120mapPTermFC f g (PQuote q) = PQuote q
1121mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1122mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1123mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1124mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1125mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1126mapPTermFC 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)
1127mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1128mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1129mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1130mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1131mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1132mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1133mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1134mapPTermFC 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)
1135mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1136mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1137mapPTermFC 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)
1138mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1139mapPTermFC 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)
1140mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1141mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1142mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1143mapPTermFC f g (PType fc) = PType (f fc)
1144mapPTermFC f g (PUniverse fc u) = PUniverse (f fc) u
1145mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1146mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1147mapPTermFC f g Placeholder = Placeholder
1148mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1149 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1150 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1151 mapPDoFC (DoBindP fc t1 t2 alts) =
1152 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1153 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1154 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1155mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1156mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1157mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1158mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1159mapPTermFC f g (PElabError err) = PElabError err
1160mapPTermFC f g PImpossible = PImpossible
1161mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1162mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1163mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1164mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1165mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1166mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1167mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1168mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1169mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1172dg instance Binary PTerm
1175mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1176mapPT f t = f (mpt t) where
1177 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1178 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1179 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1180 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1181 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1182 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1183 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1184 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1185 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1186 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1187 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1188 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1189 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1190 mpt (PHidden t) = PHidden (mapPT f t)
1191 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1192 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1193 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1194 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1195 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1196 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1197 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1201data PTactic' t = Intro [Name] | Intros | Focus Name
1202 | Refine Name [Bool] | Rewrite t | DoUnify
1209 | LetTac Name t | LetTacTy Name t t
1210 | Exact t | Compute | Trivial | TCImplementation
1211 | ProofSearch Bool Bool Int (Maybe Name)
1212 [Name] -- allowed local names
1214 -- ^ the bool is whether to search recursively
1217 | ProofState | ProofTerm | Undo
1218 | Try (PTactic' t) (PTactic' t)
1219 | TSeq (PTactic' t) (PTactic' t)
1220 | ApplyTactic t -- see Language.Reflection module
1224 | GoalType String (PTactic' t)
1227 | TDocStr (Either Name Const)
1230 | TFail [ErrorReportPart]
1233 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
1235deriving instance Binary PTactic'
1237instance Sized a => Sized (PTactic' a) where
1238 size (Intro nms) = 1 + size nms
1240 size (Focus nm) = 1 + size nm
1241 size (Refine nm bs) = 1 + size nm + length bs
1242 size (Rewrite t) = 1 + size t
1243 size (Induction t) = 1 + size t
1244 size (LetTac nm t) = 1 + size nm + size t
1245 size (Exact t) = 1 + size t
1253 size (Try l r) = 1 + size l + size r
1254 size (TSeq l r) = 1 + size l + size r
1255 size (ApplyTactic t) = 1 + size t
1256 size (Reflect t) = 1 + size t
1257 size (Fill t) = 1 + size t
1261 size (TFail ts) = 1 + size ts
1264 size (CaseTac x) = 1 + size x
1265 size (Equiv t) = 1 + size t
1266 size (Claim x y) = 1 + size x + size y
1268 size (MatchRefine x) = 1 + size x
1269 size (LetTacTy x y z) = 1 + size x + size y + size z
1270 size TCImplementation = 1
1272type PTactic = PTactic' PTerm
1274data PDo' t = DoExp FC t
1275 | DoBind FC Name FC t -- ^ second FC is precise name location
1276 | DoBindP FC t t [(t,t)]
1277 | DoLet FC Name FC t t -- ^ second FC is precise name location
1279 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
1281deriving instance Binary PDo'
1284instance Sized a => Sized (PDo' a) where
1285 size (DoExp fc t) = 1 + size fc + size t
1286 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1287 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1288 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1289 size (DoLetP fc l r) = 1 + size fc + size l + size r
1291type PDo = PDo' PTerm
1293-- The priority gives a hint as to elaboration order. Best to elaborate
1294-- things early which will help give a more concrete type to other
1295-- variables, e.g. a before (interpTy a).
1297data PArg' t = PImp { priority :: Int
1298 , machine_inf :: Bool -- ^ true if the machine inferred it
1299 , argopts :: [ArgOpt]
1303 | PExp { priority :: Int
1304 , argopts :: [ArgOpt]
1308 | PConstraint { priority :: Int
1309 , argopts :: [ArgOpt]
1313 | PTacImplicit { priority :: Int
1314 , argopts :: [ArgOpt]
1319 deriving (Show, Eq, Ord, Functor, Data, Generic, Typeable)
1321data ArgOpt = AlwaysShow
1325 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1327instance Sized a => Sized (PArg' a) where
1328 size (PImp p _ l nm trm) = 1 + size nm + size trm
1329 size (PExp p l nm trm) = 1 + size nm + size trm
1330 size (PConstraint p l nm trm) = 1 + size nm + size nm + size trm
1331 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1334deriving instance Binary PArg'
1337pimp n t mach = PImp 1 mach [] n t
1338pexp t = PExp 1 [] (sMN 0 "arg") t
1339pconst t = PConstraint 1 [] (sMN 0 "carg") t
1340ptacimp n s t = PTacImplicit 2 [] n s t
1342type PArg = PArg' PTerm
1344-- | Get the highest FC in a term, if one exists
1345highestFC :: PTerm -> Maybe FC
1346highestFC (PQuote _) = Nothing
1347highestFC (PRef fc _ _) = Just fc
1348highestFC (PInferRef fc _ _) = Just fc
1349highestFC (PPatvar fc _) = Just fc
1350highestFC (PLam fc _ _ _ _) = Just fc
1351highestFC (PPi _ _ _ _ _) = Nothing
1352highestFC (PLet fc _ _ _ _ _) = Just fc
1353highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1354highestFC (PApp fc _ _) = Just fc
1355highestFC (PAppBind fc _ _) = Just fc
1356highestFC (PMatchApp fc _) = Just fc
1357highestFC (PCase fc _ _) = Just fc
1358highestFC (PIfThenElse fc _ _ _) = Just fc
1359highestFC (PTrue fc _) = Just fc
1360highestFC (PResolveTC fc) = Just fc
1361highestFC (PRewrite fc _ _ _ _) = Just fc
1362highestFC (PPair fc _ _ _ _) = Just fc
1363highestFC (PDPair fc _ _ _ _ _) = Just fc
1364highestFC (PAs fc _ _) = Just fc
1365highestFC (PAlternative _ _ args) =
1366 case mapMaybe highestFC args of
1369highestFC (PHidden _) = Nothing
1370highestFC (PType fc) = Just fc
1371highestFC (PUniverse _ _) = Nothing
1372highestFC (PGoal fc _ _ _) = Just fc
1373highestFC (PConstant fc _) = Just fc
1374highestFC Placeholder = Nothing
1375highestFC (PDoBlock lines) =
1376 case map getDoFC lines of
1380 getDoFC (DoExp fc t) = fc
1381 getDoFC (DoBind fc nm nfc t) = fc
1382 getDoFC (DoBindP fc l r alts) = fc
1383 getDoFC (DoLet fc nm nfc l r) = fc
1384 getDoFC (DoLetP fc l r) = fc
1386highestFC (PIdiom fc _) = Just fc
1387highestFC (PMetavar fc _) = Just fc
1388highestFC (PProof _) = Nothing
1389highestFC (PTactics _) = Nothing
1390highestFC (PElabError _) = Nothing
1391highestFC PImpossible = Nothing
1392highestFC (PCoerced tm) = highestFC tm
1393highestFC (PDisamb _ opts) = highestFC opts
1394highestFC (PUnifyLog tm) = highestFC tm
1395highestFC (PNoImplicits tm) = highestFC tm
1396highestFC (PQuasiquote _ _) = Nothing
1397highestFC (PUnquote tm) = highestFC tm
1398highestFC (PQuoteName _ _ fc) = Just fc
1399highestFC (PRunElab fc _ _) = Just fc
1400highestFC (PConstSugar fc _) = Just fc
1401highestFC (PAppImpl t _) = highestFC t
1405data InterfaceInfo = CI {
1406 implementationCtorName :: Name
1407 , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method
1408 , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl
1409 , interface_default_super_interfaces :: [PDecl]
1410 , interface_impparams :: [Name]
1411 , interface_params :: [Name]
1412 , interface_constraints :: [PTerm]
1413 , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded
1414 , interface_determiners :: [Int]
1415 } deriving (Show, Generic)
1417deriving instance Binary InterfaceInfo
1421data RecordInfo = RI {
1422 record_parameters :: [(Name,PTerm)]
1423 , record_constructor :: Name
1424 , record_projections :: [Name]
1425 } deriving (Show, Generic)
1427-- Type inference data
1429data TIData = TIPartial -- ^ a function with a partially defined type
1430 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1431 deriving (Show, Generic)
1433-- | Miscellaneous information about functions
1434data FnInfo = FnInfo { fn_params :: [Int] }
1435 deriving (Show, Generic)
1437deriving instance Binary FnInfo
1440data OptInfo = Optimise {
1441 inaccessible :: [(Int,Name)] -- includes names for error reporting
1442 , detaggable :: Bool
1443 , forceable :: [Int] -- argument positions which are forced by other values
1444 } deriving (Show, Generic)
1446deriving instance Binary OptInfo
1449-- | Syntactic sugar info
1454 , dsl_var :: Maybe t
1455 , index_first :: Maybe t
1456 , index_next :: Maybe t
1457 , dsl_lambda :: Maybe t
1458 , dsl_let :: Maybe t
1460 } deriving (Show, Functor, Generic)
1462deriving instance Binary DSL'
1465type DSL = DSL' PTerm
1467data SynContext = PatternSyntax
1470 deriving (Show, Generic)
1472deriving instance Binary SynContext
1475data Syntax = Rule [SSymbol] PTerm SynContext
1476 | DeclRule [SSymbol] [PDecl]
1477 deriving (Show, Generic)
1479syntaxNames :: Syntax -> [Name]
1480syntaxNames (Rule syms _ _) = mapMaybe ename syms
1481 where ename (Keyword n) = Just n
1483syntaxNames (DeclRule syms _) = mapMaybe ename syms
1484 where ename (Keyword n) = Just n
1487syntaxSymbols :: Syntax -> [SSymbol]
1488syntaxSymbols (Rule ss _ _) = ss
1489syntaxSymbols (DeclRule ss _) = ss
1491deriving instance Binary Syntax
1494data SSymbol = Keyword Name
1499 deriving (Show, Eq, Generic)
1503deriving instance Binary SSymbol
1506newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1509emptySyntaxRules :: SyntaxRules
1510emptySyntaxRules = SyntaxRules []
1512updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1513updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1515 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1520 ruleSort (s1:ss1) (s2:ss2) =
1521 case symCompare s1 s2 of
1522 EQ -> ruleSort ss1 ss2
1525 -- Better than creating Ord implementation for SSymbol since
1526 -- in general this ordering does not really make sense.
1527 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1528 symCompare (Keyword _) _ = LT
1529 symCompare (Symbol _) (Keyword _) = GT
1530 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1531 symCompare (Symbol _) _ = LT
1532 symCompare (Binding _) (Keyword _) = GT
1533 symCompare (Binding _) (Symbol _) = GT
1534 symCompare (Binding b1) (Binding b2) = compare b1 b2
1535 symCompare (Binding _) _ = LT
1536 symCompare (Expr _) (Keyword _) = GT
1537 symCompare (Expr _) (Symbol _) = GT
1538 symCompare (Expr _) (Binding _) = GT
1539 symCompare (Expr e1) (Expr e2) = compare e1 e2
1540 symCompare (Expr _) _ = LT
1541 symCompare (SimpleExpr _) (Keyword _) = GT
1542 symCompare (SimpleExpr _) (Symbol _) = GT
1543 symCompare (SimpleExpr _) (Binding _) = GT
1544 symCompare (SimpleExpr _) (Expr _) = GT
1545 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1547initDSL = DSL (PRef f [] (sUN ">>="))
1548 (PRef f [] (sUN "<*>"))
1549 (PRef f [] (sUN "pure"))
1556 where f = fileFC "(builtin)"
1558data Using = UImplicit Name PTerm
1559 | UConstraint Name [Name]
1560 deriving (Show, Eq, Data, Generic, Typeable)
1562deriving instance Binary Using
1565data SyntaxInfo = Syn {
1567 , syn_params :: [(Name, PTerm)]
1568 , syn_namespace :: [String]
1570 , imp_methods :: [Name]
1571 -- ^ interface methods. When expanding implicits, these should be
1572 -- expanded even under binders
1573 , decoration :: Name -> Name
1575 , implicitAllowed :: Bool
1576 , constraintAllowed :: Bool
1577 , maxline :: Maybe Int
1578 , mut_nesting :: Int
1580 , syn_in_quasiquote :: Int
1581 , syn_toplevel :: Bool
1582 , withAppAllowed :: Bool
1583 } deriving (Show, Generic)
1585deriving instance Binary SyntaxInfo
1588defaultSyntax = Syn [] [] [] [] [] id False False False Nothing 0 initDSL 0 True True
1590expandNS :: SyntaxInfo -> Name -> Name
1591expandNS syn n@(NS _ _) = n
1592expandNS syn n = case syn_namespace syn of
1597-- For inferring types of things
1599bi = fileFC "builtin"
1600primfc = fileFC "(primitive)"
1602inferTy = sMN 0 "__Infer"
1603inferCon = sMN 0 "__infer"
1604inferDecl = PDatadecl inferTy primfc
1606 [(emptyDocstring, [], inferCon, primfc, PPi impl (sMN 0 "iType") primfc (PType bi) (
1607 PPi expl (sMN 0 "ival") primfc (PRef bi [] (sMN 0 "iType"))
1608 (PRef bi [] inferTy)), bi, [])]
1611infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1612infP = P (TCon 6 0) inferTy (TType (UVal 0))
1614getInferTerm, getInferType :: Term -> Term
1615getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1616getInferTerm (App _ (App _ _ _) tm) = tm
1617getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1619getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1620 where toTy (Lam t) = Pi Nothing t (TType (UVar [] 0))
1621 toTy (PVar t) = PVTy t
1623getInferType (App _ (App _ _ ty) _) = ty
1627-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1629primNames = [inferTy, inferCon]
1632unitCon = sUN "MkUnit"
1634falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1635 "The empty type, also known as the trivially false proposition." ++
1637 "Use `void` or `absurd` to prove anything if you have a variable " ++
1638 "of type `Void` in scope."
1641pairTy = sNS (sUN "Pair") ["Builtins"]
1642pairCon = sNS (sUN "MkPair") ["Builtins"]
1644upairTy = sNS (sUN "UPair") ["Builtins"]
1645upairCon = sNS (sUN "MkUPair") ["Builtins"]
1649eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1650 "The propositional equality type. A proof that `x` = `y`." ++
1652 "To use such a proof, pattern-match on it, and the two equal things will " ++
1653 "then need to be the _same_ pattern." ++
1655 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1656 "is possible to state equalities between values of potentially different " ++
1657 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1659 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1661eqDecl = PDatadecl eqTy primfc (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1662 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1664 [(reflDoc, reflParamDoc,
1665 eqCon, primfc, PPi impl (n "A") primfc (PType bi) (
1666 PPi impl (n "x") primfc (PRef bi [] (n "A"))
1667 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1668 pimp (n "B") Placeholder False,
1669 pexp (PRef bi [] (n "x")),
1670 pexp (PRef bi [] (n "x"))])), bi, [])]
1672 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1673 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1674 "shown that both sides are in fact equal."
1675 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1676 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1678eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1679 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1685-- | The special name to be used in the module documentation context -
1686-- not for use in the main definition context. The namespace around it
1687-- will determine the module to which the docs adhere.
1689modDocName = sMN 0 "ModuleDocs"
1691-- Defined in builtins.idr
1692sigmaTy = sNS (sUN "DPair") ["Builtins"]
1693sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1695piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1696piBind = piBindp expl
1698piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1700piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1703-- Pretty-printing declarations and terms
1705-- These "show" implementations render to an absurdly wide screen because inserted line breaks
1706-- could interfere with interactive editing, which calls "show".
1708instance Show PTerm where
1709 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1711instance Show PDecl where
1712 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1714instance Show PClause where
1715 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1717instance Show PData where
1718 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1720instance Pretty PTerm OutputAnnotation where
1721 pretty = prettyImp defaultPPOption
1723-- | Colourise annotations according to an Idris state. It ignores the
1724-- names in the annotation, as there's no good way to show extended
1725-- information on a terminal.
1726annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1727annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1728annotationColour ist (AnnConst c) =
1729 let theme = idris_colourTheme ist
1730 in Just $ if constIsType c
1731 then typeColour theme
1732 else dataColour theme
1733annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1734annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1735annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1736annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1737annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1738annotationColour ist (AnnName n _ _ _) =
1739 let ctxt = tt_ctxt ist
1740 theme = idris_colourTheme ist
1742 _ | isDConName n ctxt -> Just $ dataColour theme
1743 _ | isFnName n ctxt -> Just $ functionColour theme
1744 _ | isTConName n ctxt -> Just $ typeColour theme
1745 _ | isPostulateName n ist -> Just $ postulateColour theme
1746 _ | otherwise -> Nothing -- don't colourise unknown names
1747annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1748 where colour BoldText = IdrisColour Nothing True False True False
1749 colour UnderlineText = IdrisColour Nothing True True False False
1750 colour ItalicText = IdrisColour Nothing True False False True
1751annotationColour ist _ = Nothing
1754-- | Colourise annotations according to an Idris state. It ignores the
1755-- names in the annotation, as there's no good way to show extended
1756-- information on a terminal. Note that strings produced this way will
1757-- not be coloured on Windows, so the use of the colour rendering
1758-- functions in Idris.Output is to be preferred.
1759consoleDecorate :: IState -> OutputAnnotation -> String -> String
1760consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1762isPostulateName :: Name -> IState -> Bool
1763isPostulateName n ist = S.member n (idris_postulates ist)
1765-- | Pretty-print a high-level closed Idris term with no information
1766-- about precedence/associativity
1767prettyImp :: PPOption -- ^ pretty printing options
1768 -> PTerm -- ^ the term to pretty-print
1769 -> Doc OutputAnnotation
1770prettyImp impl = pprintPTerm impl [] [] []
1772-- | Serialise something to base64 using its Binary implementation.
1774-- | Do the right thing for rendering a term in an IState
1775prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1776prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1778-- | Pretty-print a high-level Idris term in some bindings context
1780pprintPTerm :: PPOption -- ^ pretty printing options
1781 -> [(Name, Bool)] -- ^ the currently-bound names and whether they are implicit
1782 -> [Name] -- ^ names to always show in pi, even if not used
1783 -> [FixDecl] -- ^ Fixity declarations
1784 -> PTerm -- ^ the term to pretty-print
1785 -> Doc OutputAnnotation
1786pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1791 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1792 prettySe d p bnd (PQuote r) =
1793 text "![" <> pretty r <> text "]"
1794 prettySe d p bnd (PPatvar fc n) = pretty n
1796 | Just str <- slist d p bnd e = depth d str
1797 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1798 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1799 prettySe d p bnd (PLam fc n nfc ty sc) =
1800 let (ns, sc') = getLamNames [n] sc in
1801 depth d . bracket p startPrec . group . align . hang 2 $
1802 text "\\" <> prettyBindingsOf ns False <+> text "=>" <$>
1803 prettySe (decD d) startPrec ((n, False):bnd) sc'
1805 getLamNames acc (PLam fc n nfc ty sc) = getLamNames (n : acc) sc
1806 getLamNames acc sc = (reverse acc, sc)
1808 prettyBindingsOf [] t = text ""
1809 prettyBindingsOf [n] t = prettyBindingOf n t
1810 prettyBindingsOf (n : ns) t = prettyBindingOf n t <> text "," <+>
1811 prettyBindingsOf ns t
1812 prettySe d p bnd (PLet fc n nfc ty v sc) =
1813 depth d . bracket p startPrec . group . align $
1814 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1815 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1816 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1817 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1818 || ppopt_pinames ppo && uname n =
1819 depth d . bracket p startPrec . group $
1820 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1821 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1823 depth d . bracket p startPrec . group $
1824 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1825 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1827 uname (UN n) = case str n of
1834 Static -> text "%static" <> space
1836 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1838 depth d . bracket p startPrec $
1839 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1840 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1841 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1845 Static -> text "%static" <> space
1847 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1848 depth d . bracket p startPrec $
1849 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1850 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1851 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1852 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1853 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1854 depth d . bracket p startPrec $
1855 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1856 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1857 prettySe d p bnd (PApp _ (PRef _ _ neg) [_, _, val])
1858 | basename neg == sUN "negate" =
1859 lparen <> text "-" <> prettySe d funcAppPrec bnd (getTm val) <> rparen
1860 -- This case preserves the behavior of the former constructor PEq.
1861 -- It should be removed if feasible when the pretty-printing of infix
1862 -- operators in general is improved.
1863 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1864 | n == eqTy, ppopt_impl ppo =
1865 depth d . bracket p eqPrec $
1866 enclose lparen rparen eq <+>
1867 align (group (vsep (map (prettyArgS (decD d) bnd)
1870 depth d . bracket p eqPrec . align . group $
1871 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1872 where eq = annName eqTy (text "=")
1874 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1875 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1876 | UN nm <- basename f
1877 , not (ppopt_impl ppo) && null (getShowArgs args) =
1878 prettyName True (ppopt_impl ppo) bnd f
1879 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1880 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1881 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1882 | UN nm <- basename op
1884 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1885 case getShowArgs args of
1887 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1888 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1889 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1890 (l@(PExp{}) : r@(PExp{}) : rest) ->
1891 depth d . bracket p funcAppPrec $
1892 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1893 align (group (vsep (map (prettyArgS d bnd) rest)))
1894 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1895 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1896 f = getFixity (opStr op)
1898 Nothing -> funcAppPrec + 1
1899 Just (Infixl p') -> p'
1900 Just f' -> prec f' + 1
1902 Nothing -> funcAppPrec + 1
1903 Just (Infixr p') -> p'
1904 Just f' -> prec f' + 1
1905 inFix l r = align . group $
1906 (prettySe (decD d) left bnd l <+> opName False) <$>
1907 group (prettySe (decD d) right bnd r)
1908 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1909 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1910 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1911 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1912 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1913 let args = getShowArgs as
1914 fp = prettySe (decD d) (startPrec + 1) bnd f
1915 shownArgs = if ppopt_impl ppo then as else args
1917 depth d . bracket p funcAppPrec . group $
1920 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1921 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1922 prettySe d p bnd (PCase _ scr cases) =
1923 bracket p funcAppPrec $
1924 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1925 depth d (indent 2 (vsep (map ppcase cases)))
1927 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1928 ([(n, False) | n <- vars l] ++ bnd)
1929 in nest nestingSize $
1930 prettyCase l <+> text "=>" <+> prettyCase r
1931 -- Warning: this is a bit of a hack. At this stage, we don't have the
1932 -- global context, so we can't determine which names are constructors,
1933 -- which are types, and which are pattern variables on the LHS of the
1934 -- case pattern. We use the heuristic that names without a namespace
1935 -- are patvars, because right now case blocks in PTerms are always
1936 -- delaborated from TT before being sent to the pretty-printer. If they
1937 -- start getting printed directly, THIS WILL BREAK.
1938 -- Potential solution: add a list of known patvars to the cases in
1939 -- PCase, and have the delaborator fill it out, kind of like the pun
1940 -- disambiguation on PDPair.
1941 vars tm = filter noNS (allNamesIn tm)
1942 noNS (NS _ _) = False
1945 prettySe d p bnd (PIfThenElse _ c t f) =
1946 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1947 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1948 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1949 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1951 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1952 prettySe d p bnd (PResolveTC _) = kwd "%implementation"
1953 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1954 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1955 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1956 prettySe d p bnd (PRewrite _ by l r _) =
1957 depth d . bracket p startPrec $
1958 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1961 Just fn -> text "using" <+>
1962 prettyName True (ppopt_impl ppo) bnd fn) <+>
1963 text "in" <+> prettySe (decD d) startPrec bnd r
1964 prettySe d p bnd (PTyped l r) =
1965 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1966 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1967 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1968 align . group . vsep . punctuate (ann comma) $
1969 map (prettySe (decD d) startPrec bnd) elts
1970 where ann = case pun of
1972 IsType -> annName pairTy
1973 IsTerm -> annName pairCon
1974 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1975 | Just elts <- dPairElts dpair
1976 = depth d . enclose (annotated lparen) (annotated rparen) .
1977 align . group . vsep . punctuate (space <> annotated (text "**")) $
1983 annotated (text "**") <+>
1984 prettySe (decD d) startPrec (addBinding bnd) r <>
1986 where annotated = case pun of
1987 IsType -> annName sigmaTy
1988 IsTerm -> annName sigmaCon
1991 (left, addBinding) = case (l, pun) of
1992 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1993 _ -> (prettySe (decD d) startPrec bnd l, id)
1996 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1997 ppElts ((PRef _ _ n, t):rs) bs
1999 = (bindingOf n False <+> colon <+>
2000 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
2001 ppElts ((l, t):rs) bs
2002 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
2003 prettySe d p bnd (PAlternative ns a as) =
2004 lparen <> text "|" <> prettyAs <> text "|" <> rparen
2007 foldr ((\ l r -> l <+> text "," <+> r) .
2008 depth d . prettySe (decD d) startPrec bnd)
2010 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
2011 prettySe d p bnd (PUniverse _ u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
2012 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
2013 -- XXX: add pretty for tactics
2014 prettySe d p bnd (PProof ts) =
2015 kwd "proof" <+> lbrace <> ellipsis <> rbrace
2016 prettySe d p bnd (PTactics ts) =
2017 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
2018 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
2019 prettySe d p bnd PImpossible = kwd "impossible"
2020 prettySe d p bnd Placeholder = text "_"
2021 prettySe d p bnd (PDoBlock dos) =
2022 bracket p startPrec $
2023 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
2024 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
2025 ppdo bnd (DoBind _ bn _ tm : dos) =
2026 (prettyBindingOf bn False <+> text "<-" <+>
2027 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
2028 ppdo ((bn, False):bnd) dos
2029 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
2030 text "no pretty printer for pattern-matching do binding" :
2032 ppdo bnd (DoLet _ ln _ ty v : dos) =
2033 (kwd "let" <+> prettyBindingOf ln False <+>
2034 (if ty /= Placeholder
2035 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
2037 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
2038 ppdo ((ln, False):bnd) dos
2039 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
2040 text "no pretty printer for pattern-matching do binding" :
2043 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
2044 prettySe d p bnd (PElabError s) = pretty s
2045 -- Quasiquote pprinting ignores bound vars
2046 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
2047 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
2048 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
2049 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
2050 where start = if res then "`{" else "`{{"
2051 end = if res then "}" else "}}"
2052 prettySe d p bnd (PRunElab _ tm _) =
2053 bracket p funcAppPrec . group . align . hang 2 $
2055 prettySe (decD d) funcAppPrec bnd tm
2056 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
2057 prettySe d p bnd _ = text "missing pretty-printer for term"
2059 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
2060 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
2061 where display (UN n) = T.unpack n
2062 display (MN _ n) = T.unpack n
2063 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
2064 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
2067 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2068 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2069 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2070 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2072 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2073 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2074 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2075 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2077 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2078 annName n = annotate (AnnName n Nothing Nothing Nothing)
2080 opStr :: Name -> String
2081 opStr (NS n _) = opStr n
2082 opStr (UN n) = T.unpack n
2084 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2085 slist' (Just d) _ _ _ | d <= 0 = Nothing
2087 | containsHole e = Nothing
2088 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2089 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2090 slist' d p bnd (PRef _ _ nil)
2091 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2092 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2093 | nsroot cons == sUN "::",
2094 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2096 Just tl' <- slist' (decD d) p bnd tl
2097 = Just (prettySe d startPrec bnd hd : tl')
2099 isImp (PImp {}) = True
2101 slist' _ _ _ tm = Nothing
2103 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2105 [] -> annotate (AnnData "" "") $ text "[]"
2106 [x] -> enclose left right . group $ x
2107 xs -> enclose left right .
2108 align . group . vsep .
2109 punctuate comma $ xs
2110 where left = (annotate (AnnData "" "") (text "["))
2111 right = (annotate (AnnData "" "") (text "]"))
2112 comma = (annotate (AnnData "" "") (text ","))
2113 slist _ _ _ _ = Nothing
2115 pairElts :: PTerm -> Maybe [PTerm]
2116 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2117 | otherwise = Just [x, y]
2118 pairElts _ = Nothing
2120 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2121 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2122 | otherwise = Just [(l, t), (Placeholder, r)]
2123 dPairElts _ = Nothing
2125 natns = "Prelude.Nat."
2127 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2129 | ppopt_desugarnats ppo = Nothing
2130 | otherwise = snat' d p e
2132 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2133 snat' (Just x) _ _ | x <= 0 = Nothing
2134 snat' d p (PRef _ _ z)
2135 | show z == (natns++"Z") || show z == "Z" = Just 0
2136 snat' d p (PApp _ s [PExp {getTm=n}])
2137 | show s == (natns++"S") || show s == "S",
2138 Just n' <- snat' (decD d) p n
2140 snat' _ _ _ = Nothing
2142 bracket outer inner doc
2143 | outer > inner = lparen <> doc <> rparen
2146 ellipsis = text "..."
2149 depth (Just d) = if d <= 0 then const ellipsis else id
2151 decD = fmap (\x -> x - 1)
2153 kwd = annotate AnnKeyword . text
2155 fixities :: M.Map String Fixity
2156 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2158 getFixity :: String -> Maybe Fixity
2159 getFixity = flip M.lookup fixities
2161-- | Strip away namespace information
2162basename :: Name -> Name
2163basename (NS n _) = basename n
2166-- | Determine whether a name was the one inserted for a hole or guess
2167-- by the delaborator
2168isHoleName :: Name -> Bool
2169isHoleName (UN n) = n == T.pack "[__]"
2172-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2173containsHole :: PTerm -> Bool
2174containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2176-- | Pretty-printer helper for names that attaches the correct annotations
2177prettyName :: Bool -- ^ whether the name should be parenthesised if it is an infix operator
2178 -> Bool -- ^ whether to show namespaces
2179 -> [(Name, Bool)] -- ^ the current bound variables and whether they are implicit
2180 -> Name -- ^ the name to pprint
2181 -> Doc OutputAnnotation
2182prettyName infixParen showNS bnd n
2183 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2184 | (UN n') <- n, isPrefixOf "__" $ T.unpack n' = text "_"
2185 | (UN n') <- n, T.unpack n' == "_" = text "_"
2186 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2187 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2188 where fullName = text nameSpace <> parenthesise (text (baseName n))
2189 baseName (UN n) = T.unpack n
2190 baseName (NS n ns) = baseName n
2191 baseName (MN i s) = T.unpack s
2192 baseName other = show other
2193 nameSpace = case n of
2194 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2196 isInfix = case baseName n of
2198 (c : _) -> not (isAlpha c)
2199 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2202showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2203showCImp ppo (PClause _ n l ws r w)
2204 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2205 <+> text "where" <+> text (show w)
2208 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2209showCImp ppo (PWith _ n l ws r pn w)
2210 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2211 <+> braces (text (show w))
2214 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2217showDImp :: PPOption -> PData -> Doc OutputAnnotation
2218showDImp ppo (PDatadecl n nfc ty cons)
2219 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2220 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2222showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2223showDecls o ds = vsep (map (showDeclImp o) ds)
2225showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2226showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2227showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2228 indent 2 (vsep (map (showCImp o) cs))
2229showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2230showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2231showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2232showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2233showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2234showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)
2235 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2236showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)
2237 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2238showDeclImp _ _ = text "..."
2239-- showDeclImp (PImport o) = "import " ++ o
2241getImps :: [PArg] -> [(Name, PTerm)]
2243getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2244getImps (_ : xs) = getImps xs
2246getExps :: [PArg] -> [PTerm]
2248getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2249getExps (_ : xs) = getExps xs
2251getShowArgs :: [PArg] -> [PArg]
2253getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2254getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2255 | PImp _ _ _ _ tm <- e
2256 , containsHole tm = e : getShowArgs xs
2257getShowArgs (_ : xs) = getShowArgs xs
2259getConsts :: [PArg] -> [PTerm]
2261getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2262getConsts (_ : xs) = getConsts xs
2264getAll :: [PArg] -> [PTerm]
2269showName :: Maybe IState -- ^ the Idris state, for information about names and colours
2270 -> [(Name, Bool)] -- ^ the bound variables and whether they're implicit
2271 -> PPOption -- ^ pretty printing options
2272 -> Bool -- ^ whether to colourise
2273 -> Name -- ^ the term to show
2275showName ist bnd ppo colour n = case ist of
2276 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2277 Nothing -> showbasic n
2278 where name = if ppopt_impl ppo then show n else showbasic n
2279 showbasic n@(UN _) = showCG n
2280 showbasic (MN i s) = str s
2281 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2282 showbasic (SN s) = show s
2284 colourise n t = let ctxt' = fmap tt_ctxt ist in
2287 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2288 else colouriseBound t name
2289 | isDConName n ctxt -> colouriseData t name
2290 | isFnName n ctxt -> colouriseFun t name
2291 | isTConName n ctxt -> colouriseType t name
2292 -- The assumption is that if a name is not bound and does not exist in the
2293 -- global context, then we're somewhere in which implicit info has been lost
2294 -- (like error messages). Thus, unknown vars are colourised as implicits.
2295 | otherwise -> colouriseImplicit t name
2297showTm :: IState -- ^ the Idris state, for information about identifiers and colours
2298 -> PTerm -- ^ the term to show
2300showTm ist = displayDecorated (consoleDecorate ist) .
2301 renderPretty 0.8 100000 .
2302 prettyImp (ppOptionIst ist)
2304-- | Show a term with implicits, no colours
2305showTmImpls :: PTerm -> String
2306showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2308-- | Show a term with specific options
2309showTmOpts :: PPOption -> PTerm -> String
2310showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2313instance Sized PTerm where
2314 size (PQuote rawTerm) = size rawTerm
2315 size (PRef fc _ name) = size name
2316 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2317 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2318 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2319 size (PTyped trm ty) = 1 + size trm + size ty
2320 size (PApp fc name args) = 1 + size args
2321 size (PAppBind fc name args) = 1 + size args
2322 size (PCase fc trm bdy) = 1 + size trm + size bdy
2323 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2324 size (PTrue fc _) = 1
2325 size (PResolveTC fc) = 1
2326 size (PRewrite fc by left right _) = 1 + size left + size right
2327 size (PPair fc _ _ left right) = 1 + size left + size right
2328 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2329 size (PAlternative _ a alts) = 1 + size alts
2330 size (PHidden hidden) = size hidden
2331 size (PUnifyLog tm) = size tm
2332 size (PDisamb _ tm) = size tm
2333 size (PNoImplicits tm) = size tm
2335 size (PUniverse _ _) = 1
2336 size (PConstant fc const) = 1 + size fc + size const
2337 size Placeholder = 1
2338 size (PDoBlock dos) = 1 + size dos
2339 size (PIdiom fc term) = 1 + size term
2340 size (PMetavar _ name) = 1
2341 size (PProof tactics) = size tactics
2342 size (PElabError err) = size err
2343 size PImpossible = 1
2346getPArity :: PTerm -> Int
2347getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2350-- Return all names, free or globally bound, in the given term.
2352allNamesIn :: PTerm -> [Name]
2353allNamesIn tm = nub $ ni 0 [] tm
2354 where -- TODO THINK added niTacImp, but is it right?
2355 ni 0 env (PRef _ _ n)
2356 | not (n `elem` env) = [n]
2357 ni 0 env (PPatvar _ n) = [n]
2358 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2359 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2360 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2361 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2362 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2363 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2364 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2365 ni 0 env (PHidden tm) = ni 0 env tm
2366 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2367 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2368 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2369 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2370 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2371 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2372 ni 0 env (PAlternative ns a ls) = map snd ns ++ concatMap (ni 0 env) ls
2373 ni 0 env (PUnifyLog tm) = ni 0 env tm
2374 ni 0 env (PDisamb _ tm) = ni 0 env tm
2375 ni 0 env (PNoImplicits tm) = ni 0 env tm
2377 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2378 ni i env (PUnquote tm) = ni (i - 1) env tm
2379 ni i env tm = concatMap (ni i env) (children tm)
2381 niTacImp i env (TacImp _ _ scr) = ni i env scr
2385-- Return all names defined in binders in the given term
2386boundNamesIn :: PTerm -> [Name]
2387boundNamesIn tm = S.toList (ni 0 S.empty tm)
2388 where -- TODO THINK Added niTacImp, but is it right?
2389 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2390 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2391 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2392 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2393 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2394 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2395 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2396 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2397 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2398 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2399 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2400 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2401 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2402 ni 0 set (PAlternative ns a as) = niTms 0 set as
2403 ni 0 set (PHidden tm) = ni 0 set tm
2404 ni 0 set (PUnifyLog tm) = ni 0 set tm
2405 ni 0 set (PDisamb _ tm) = ni 0 set tm
2406 ni 0 set (PNoImplicits tm) = ni 0 set tm
2408 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2409 ni i set (PUnquote tm) = ni (i - 1) set tm
2411 ni i set tm = foldr (S.union . ni i set) set (children tm)
2413 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2414 niTms i set [] = set
2415 niTms i set (x : xs) = niTms i (ni i set x) xs
2417 niTacImp i set (TacImp _ _ scr) = ni i set scr
2418 niTacImp i set _ = set
2420-- Return names which are valid implicits in the given term (type).
2421implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2422implicitNamesIn uvars ist tm
2423 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2426 addImp n = do (imps, fns) <- get
2428 addFn n = do (imps, fns) <- get
2432 notCAF (PExp _ _ _ _ : _) = True
2433 notCAF (_ : xs) = notCAF xs
2435 notHidden (n, _) = case getAccessibility n of
2441 = case lookupDefAccExact n False (tt_ctxt ist) of
2445 ni 0 env (PRef _ _ n@(NS _ _))
2446 | not (n `elem` env)
2447 -- Never implicitly bind if there's a namespace
2449 ni 0 env (PRef _ _ n)
2450 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2451 ni 0 env (PApp _ f@(PRef _ _ n) as)
2452 | n `elem` uvars = do ni 0 env f
2453 mapM_ (ni 0 env . getTm) as
2454 | otherwise = do case lookupTy n (tt_ctxt ist) of
2457 mapM_ (ni 0 env . getTm) as
2458 ni 0 env (PApp _ f as) = do ni 0 env f
2459 mapM_ (ni 0 env . getTm) as
2460 ni 0 env (PAppBind _ f as) = do ni 0 env f
2461 mapM_ (ni 0 env . getTm) as
2462 ni 0 env (PCase _ c os) = do ni 0 env c
2463 -- names in 'os', not counting the names bound in the cases
2464 mapM_ (ni 0 env . snd) os
2467 mapM_ (ni 0 env . fst) os
2469 put (nub imps \\ nub impsfst, fns)
2470 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2471 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2472 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2473 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2474 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2475 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2476 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2477 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2480 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2481 ni 0 env (PHidden tm) = ni 0 env tm
2482 ni 0 env (PUnifyLog tm) = ni 0 env tm
2483 ni 0 env (PDisamb _ tm) = ni 0 env tm
2484 ni 0 env (PNoImplicits tm) = ni 0 env tm
2486 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2487 maybe (return ()) (ni i env) ty
2488 ni i env (PUnquote tm) = ni (i - 1) env tm
2490 ni i env tm = mapM_ (ni i env) (children tm)
2492-- Return names which are free in the given term.
2493namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2494namesIn uvars ist tm = nub $ ni 0 [] tm
2496 ni 0 env (PRef _ _ n)
2497 | not (n `elem` env)
2498 = case lookupTy n (tt_ctxt ist) of
2500 _ -> [n | n `elem` (map fst uvars)]
2501 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2502 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2503 ni 0 env (PCase _ c os) = ni 0 env c ++
2504 -- names in 'os', not counting the names bound in the cases
2505 (nub (concatMap (ni 0 env . snd) os)
2506 \\ nub (concatMap (ni 0 env . fst) os))
2507 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2508 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2509 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2510 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2511 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2512 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2513 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2514 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2515 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2516 ni 0 env (PHidden tm) = ni 0 env tm
2517 ni 0 env (PUnifyLog tm) = ni 0 env tm
2518 ni 0 env (PDisamb _ tm) = ni 0 env tm
2519 ni 0 env (PNoImplicits tm) = ni 0 env tm
2521 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2522 ni i env (PUnquote tm) = ni (i - 1) env tm
2524 ni i env tm = concatMap (ni i env) (children tm)
2526 niTacImp i env (TacImp _ _ scr) = ni i env scr
2529-- Return which of the given names are used in the given term.
2531usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2532usedNamesIn vars ist tm = nub $ ni 0 [] tm
2533 where -- TODO THINK added niTacImp, but is it right?
2534 ni 0 env (PRef _ _ n)
2535 | n `elem` vars && not (n `elem` env)
2536 = case lookupDefExact n (tt_ctxt ist) of
2539 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2540 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2541 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2542 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2543 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2544 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2545 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2546 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2547 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2548 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2549 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2550 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2551 ni 0 env (PHidden tm) = ni 0 env tm
2552 ni 0 env (PUnifyLog tm) = ni 0 env tm
2553 ni 0 env (PDisamb _ tm) = ni 0 env tm
2554 ni 0 env (PNoImplicits tm) = ni 0 env tm
2556 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2557 ni i env (PUnquote tm) = ni (i - 1) env tm
2559 ni i env tm = concatMap (ni i env) (children tm)
2561 niTacImp i env (TacImp _ _ scr) = ni i env scr
2564-- Return the list of inaccessible (= dotted) positions for a name.
2565getErasureInfo :: IState -> Name -> [Int]
2566getErasureInfo ist n =
2567 case lookupCtxtExact n (idris_optimisation ist) of
2568 Just (Optimise inacc detag force) -> 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