1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.Docstrings
12import IRTS.CodegenCommon
14import Util.DynamicLinker
18import System.Console.Haskeline
21import Prelude hiding ((<$>))
23import Control.Applicative ((<|>))
25import Control.Monad.Trans.State.Strict
26import Control.Monad.Trans.Except
27import qualified Control.Monad.Trans.Class as Trans (lift)
29import Data.Data (Data)
30import Data.Function (on)
31import Data.Generics.Uniplate.Data (universe, children)
32import Data.List hiding (group)
34import qualified Data.Map.Strict as M
35import qualified Data.Text as T
37import qualified Data.Set as S
38import Data.Word (Word)
39import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
40import Data.Traversable (Traversable)
42import Data.Foldable (Foldable)
46import Text.PrettyPrint.Annotated.Leijen
48data ElabWhat = ETypes | EDefns | EAll
51-- Data to pass to recursively called elaborators; e.g. for where blocks,
52-- paramaterised declarations, etc.
54-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
55-- so that we can have mutually recursive elaborators in separate modules without
56-- having to muck about with cyclic modules.
57data ElabInfo = EInfo { params :: [(Name, PTerm)],
58 inblock :: Ctxt [Name], -- names in the block, and their params
59 liftname :: Name -> Name,
60 namespace :: Maybe [String],
62 -- We may, recursively, collect transformations to
63 -- do on the rhs, e.g. rewriting recursive calls to
64 -- functions defined by 'with'
65 rhs_trans :: PTerm -> PTerm,
66 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
70toplevel = EInfo [] emptyContext id Nothing Nothing id (\_ _ _ -> fail "Not implemented")
72eInfoNames :: ElabInfo -> [Name]
73eInfoNames info = map fst (params info) ++ M.keys (inblock info)
75data IOption = IOption {
77 , opt_logcats :: [LogCat] -- ^ List of logging categories.
78 , opt_typecase :: Bool
79 , opt_typeintype :: Bool
80 , opt_coverage :: Bool
81 , opt_showimp :: Bool -- ^ show implicits
82 , opt_errContext :: Bool
85 , opt_nobanner :: Bool
87 , opt_codegen :: Codegen
88 , opt_outputTy :: OutputType
89 , opt_ibcsubdir :: FilePath
90 , opt_importdirs :: [FilePath]
91 , opt_triple :: String
93 , opt_cmdline :: [Opt] -- remember whole command line
95 , opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
96 , opt_autoImport :: [FilePath] -- ^ e.g. Builtins+Prelude
97 , opt_optimise :: [Optimisation]
98 , opt_printdepth :: Maybe Int
99 , opt_evaltypes :: Bool -- ^ normalise types in :t
100 , opt_desugarnats :: Bool
101 , opt_autoimpls :: Bool
102 } deriving (Show, Eq)
104defaultOpts = IOption { opt_logLevel = 0
106 , opt_typecase = False
107 , opt_typeintype = False
108 , opt_coverage = True
109 , opt_showimp = False
110 , opt_errContext = False
113 , opt_nobanner = False
115 , opt_codegen = Via "c"
116 , opt_outputTy = Executable
118 , opt_importdirs = []
122 , opt_origerr = False
123 , opt_autoSolve = True
124 , opt_autoImport = []
125 , opt_optimise = defaultOptimise
126 , opt_printdepth = Just 5000
127 , opt_evaltypes = True
128 , opt_desugarnats = False
129 , opt_autoimpls = True
132data PPOption = PPOption {
133 ppopt_impl :: Bool -- ^^ whether to show implicits
134 , ppopt_desugarnats :: Bool
135 , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings
136 , ppopt_depth :: Maybe Int
139data Optimisation = PETransform -- partial eval and associated transforms
142defaultOptimise = [PETransform]
144-- | Pretty printing options with default verbosity.
145defaultPPOption :: PPOption
146defaultPPOption = PPOption { ppopt_impl = False,
147 ppopt_desugarnats = False,
148 ppopt_pinames = False,
149 ppopt_depth = Just 200 }
151-- | Pretty printing options with the most verbosity.
152verbosePPOption :: PPOption
153verbosePPOption = PPOption { ppopt_impl = True,
154 ppopt_desugarnats = True,
155 ppopt_pinames = True,
156 ppopt_depth = Just 200 }
158-- | Get pretty printing options from the big options record.
159ppOption :: IOption -> PPOption
160ppOption opt = PPOption {
161 ppopt_impl = opt_showimp opt,
162 ppopt_pinames = False,
163 ppopt_depth = opt_printdepth opt,
164 ppopt_desugarnats = opt_desugarnats opt
167-- | Get pretty printing options from an idris state record.
168ppOptionIst :: IState -> PPOption
169ppOptionIst = ppOption . idris_options
171data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
173-- | The output mode in use
174data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
175 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
178-- | How wide is the console?
179data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
180 | ColsWide Int -- ^ Manually specified - must be positive
181 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
185-- | The global state used in the Idris monad
186data IState = IState {
187 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
188 idris_constraints :: S.Set ConstraintFC,
189 -- ^ A list of universe constraints and their corresponding source locations
190 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
191 idris_implicits :: Ctxt [PArg],
192 idris_statics :: Ctxt [Bool],
193 idris_classes :: Ctxt ClassInfo,
194 idris_records :: Ctxt RecordInfo,
195 idris_dsls :: Ctxt DSL,
196 idris_optimisation :: Ctxt OptInfo,
197 idris_datatypes :: Ctxt TypeInfo,
198 idris_namehints :: Ctxt [Name],
199 idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm]), -- not exported
200 -- ^ list of lhs/rhs, and a list of missing clauses
201 idris_flags :: Ctxt [FnOpt],
202 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
203 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
204 idris_moduledocs :: Ctxt (Docstring DocTerm),
205 -- ^ module documentation is saved in a special MN so the context
206 -- mechanism can be used for disambiguation
207 idris_tyinfodata :: Ctxt TIData,
208 idris_fninfo :: Ctxt FnInfo,
209 idris_transforms :: Ctxt [(Term, Term)],
210 idris_autohints :: Ctxt [Name],
211 idris_totcheck :: [(FC, Name)], -- names to check totality on
212 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
213 idris_totcheckfail :: [(FC, String)],
214 idris_options :: IOption,
216 idris_lineapps :: [((FilePath, Int), PTerm)],
217 -- ^ Full application LHS on source line
218 idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))],
219 -- ^ The currently defined but not proven metavariables. The Int
220 -- is the number of vars to display as a context, the Maybe Name
221 -- is its top-level function, the [Name] is the list of local variables
222 -- available for proof search and the Bools are whether :p is
223 -- allowed, and whether the variable is definable at all
224 -- (Metavariables are not definable if they are applied in a term which
225 -- still has hole bindings)
226 idris_coercions :: [Name],
227 idris_errRev :: [(Term, Term)],
228 syntax_rules :: SyntaxRules,
229 syntax_keywords :: [String],
230 imported :: [FilePath], -- ^ The imported modules
231 idris_scprims :: [(Name, (Int, PrimFn))],
232 idris_objs :: [(Codegen, FilePath)],
233 idris_libs :: [(Codegen, String)],
234 idris_cgflags :: [(Codegen, String)],
235 idris_hdrs :: [(Codegen, String)],
236 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
237 proof_list :: [(Name, (Bool, [String]))],
239 parserWarnings :: [(FC, Err)],
240 lastParse :: Maybe Name,
241 indent_stack :: [Int],
242 brace_stack :: [Maybe Int],
243 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
244 idris_parsedSpan :: Maybe FC,
245 hide_list :: Ctxt Accessibility,
246 default_access :: Accessibility,
247 default_total :: Bool,
248 ibc_write :: [IBCWrite],
249 compiled_so :: Maybe String,
250 idris_dynamic_libs :: [DynamicLib],
251 idris_language_extensions :: [LanguageExt],
252 idris_outputmode :: OutputMode,
253 idris_colourRepl :: Bool,
254 idris_colourTheme :: ColourTheme,
255 idris_errorhandlers :: [Name], -- ^ Global error handlers
256 idris_nameIdx :: (Int, Ctxt (Int, Name)),
257 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
258 module_aliases :: M.Map [T.Text] [T.Text],
259 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
260 idris_postulates :: S.Set Name,
261 idris_externs :: S.Set (Name, Int),
262 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
263 idris_whocalls :: Maybe (M.Map Name [Name]),
264 idris_callswho :: Maybe (M.Map Name [Name]),
265 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
266 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
267 -- (instances appear twice; also as a funtion name)
268 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
269 idris_exports :: [Name], -- ^ Functions with ExportList
270 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
271 idris_parserHighlights :: [(FC, OutputAnnotation)], -- ^ Highlighting information from the parser
272 idris_deprecated :: Ctxt String, -- ^ Deprecated names and explanation
273 idris_inmodule :: S.Set Name, -- ^ Names defined in current module
274 idris_ttstats :: M.Map Term (Int, Term)
277-- Required for parsers library, and therefore trifecta
278instance Show IState where
279 show = const "{internal state}"
281data SizeChange = Smaller | Same | Bigger | Unknown
284deriving instance Binary SizeChange
285deriving instance NFData SizeChange
288type SCGEntry = (Name, [Maybe (Int, SizeChange)])
289type UsageReason = (Name, Int) -- fn_name, its_arg_number
291data CGInfo = CGInfo { calls :: [Name],
293 usedpos :: [(Int, [UsageReason])]
297deriving instance Binary CGInfo
298deriving instance NFData CGInfo
301primDefs = [sUN "unsafePerformPrimIO",
302 sUN "mkLazyForeignPrim",
306-- information that needs writing for the current module's .ibc file
307data IBCWrite = IBCFix FixDecl
312 | IBCInstance Bool Bool Name Name
319 | IBCImport (Bool, FilePath) -- True = import public
320 | IBCImportDir FilePath
321 | IBCObj Codegen FilePath
322 | IBCLib Codegen String
323 | IBCCGFlag Codegen String
325 | IBCHeader Codegen String
326 | IBCAccess Name Accessibility
327 | IBCMetaInformation Name MetaInformation
328 | IBCTotal Name Totality
329 | IBCFlags Name [FnOpt]
330 | IBCFnInfo Name FnInfo
331 | IBCTrans Name (Term, Term)
332 | IBCErrRev (Term, Term)
336 | IBCDef Name -- i.e. main context
337 | IBCNameHint (Name, Name)
338 | IBCLineApp FilePath Int PTerm
339 | IBCErrorHandler Name
340 | IBCFunctionErrorHandler Name Name Name
342 | IBCExtern (Name, Int)
343 | IBCTotCheckErr FC String
345 | IBCModDocs Name -- ^ The name is the special name used to track module docs
346 | IBCUsage (Name, Int)
348 | IBCAutoHint Name Name
349 | IBCDeprecate Name String
352-- | The initial state for the compiler
354idrisInit = IState initContext S.empty []
355 emptyContext emptyContext emptyContext emptyContext
356 emptyContext emptyContext emptyContext emptyContext
357 emptyContext emptyContext emptyContext emptyContext
358 emptyContext emptyContext emptyContext emptyContext
360 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
361 [] [] Nothing [] Nothing [] [] Nothing Nothing emptyContext Private False [] Nothing [] []
362 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
363 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
364 emptyContext S.empty M.empty
367-- | The monad for the main REPL - reading and processing files and updating
368-- global state (hence the IO inner monad).
369--type Idris = WriterT [Either String (IO ())] (State IState a))
370type Idris = StateT IState (ExceptT Err IO)
372catchError :: Idris a -> (Err -> Idris a) -> Idris a
373catchError = liftCatch catchE
375throwError :: Err -> Idris a
376throwError = Trans.lift . throwE
378-- Commands in the REPL
380data Codegen = Via String
389deriving instance NFData Codegen
392data HowMuchDocs = FullDocs | OverviewDocs
398 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
402 | DocStr (Either Name Const) HowMuchDocs
406 | Load FilePath (Maybe Int) -- up to maximum line number
407 | ChangeDirectory FilePath
410 | Compile Codegen String
414 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
415 | AddProof (Maybe Name)
421 | LogCategory [LogCat]
427 | DynamicLink FilePath
430 | Search [String] PTerm
431 | CaseSplitAt Bool Int Name
432 | AddClauseFrom Bool Int Name
433 | AddProofClauseFrom Bool Int Name
434 | AddMissing Bool Int Name
435 | MakeWith Bool Int Name
436 | MakeCase Bool Int Name
437 | MakeLemma Bool Int Name
438 | DoProofSearch Bool -- update file
439 Bool -- recursive search
441 Name -- top level name
446 | SetColour ColourType IdrisColour
450 | SetConsoleWidth ConsoleWidth
451 | SetPrinterDepth (Maybe Int)
452 | Apropos [String] String
456 | MakeDoc String -- IdrisDoc
459 | PPrint OutputFmt Int PTerm
461 -- Debugging commands
463 | DebugUnify PTerm PTerm
465data OutputFmt = HTMLOutput | LaTeXOutput
467-- | Recognised logging categories for the Idris compiler.
469-- @TODO add in sub categories.
476 deriving (Show, Eq, Ord)
478strLogCat :: LogCat -> String
479strLogCat IParse = "parser"
480strLogCat IElab = "elab"
481strLogCat ICodeGen = "codegen"
482strLogCat IErasure = "erasure"
483strLogCat ICoverage = "coverage"
484strLogCat IIBC = "ibc"
486codegenCats :: [LogCat]
487codegenCats = [ICodeGen]
489parserCats :: [LogCat]
495loggingCatsStr :: String
496loggingCatsStr = unlines
499 , (strLogCat ICodeGen)
500 , (strLogCat IErasure)
501 , (strLogCat ICoverage)
505data Opt = Filename String
518 | NoBuiltins -- only for the really primitive stuff!
535 | Port String -- REPL TCP port
543 | PkgMkDoc String -- IdrisDoc
553 | OutputTy OutputType
554 | Extension LanguageExt
555 | InterpretScript String
557 | TargetTriple String
560 | AddOpt Optimisation
561 | RemoveOpt Optimisation
564 | AutoWidth -- ^ Automatically adjust terminal width
565 | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
566 | UseConsoleWidth ConsoleWidth
569 | NoElimDeprecationWarnings -- ^ Don't show deprecation warnings for %elim
570 | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
573data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
574 | EEval PTerm | ECheck PTerm | ESearch PTerm
575 | EDocStr (Either Name Const)
578-- Parsed declarations
580data Fixity = Infixl { prec :: Int }
581 | Infixr { prec :: Int }
582 | InfixN { prec :: Int }
583 | PrefixN { prec :: Int }
586deriving instance Binary Fixity
587deriving instance NFData Fixity
590instance Show Fixity where
591 show (Infixl i) = "infixl " ++ show i
592 show (Infixr i) = "infixr " ++ show i
593 show (InfixN i) = "infix " ++ show i
594 show (PrefixN i) = "prefix " ++ show i
596data FixDecl = Fix Fixity String
599instance Show FixDecl where
600 show (Fix f s) = show f ++ " " ++ s
603deriving instance Binary FixDecl
604deriving instance NFData FixDecl
607instance Ord FixDecl where
608 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
611data Static = Static | Dynamic
612 deriving (Show, Eq, Data, Typeable)
614deriving instance Binary Static
615deriving instance NFData Static
618-- Mark bindings with their explicitness, and laziness
619data Plicity = Imp { pargopts :: [ArgOpt],
622 pscoped :: Maybe ImplicitInfo, -- Nothing, if top level
623 pinsource :: Bool -- Explicitly written in source
625 | Exp { pargopts :: [ArgOpt],
627 pparam :: Bool } -- this is a param (rather than index)
628 | Constraint { pargopts :: [ArgOpt],
630 | TacImp { pargopts :: [ArgOpt],
633 deriving (Show, Eq, Data, Typeable)
636deriving instance Binary Plicity
637deriving instance NFData Plicity
640is_scoped :: Plicity -> Maybe ImplicitInfo
641is_scoped (Imp _ _ _ s _) = s
644impl = Imp [] Dynamic False (Just (Impl False True)) False
646forall_imp = Imp [] Dynamic False (Just (Impl False False)) False
647forall_constraint = Imp [] Dynamic False (Just (Impl True False)) False
649expl = Exp [] Dynamic False
650expl_param = Exp [] Dynamic True
652constraint = Constraint [] Static
654tacimpl t = TacImp [] Dynamic t
656data FnOpt = Inlinable -- always evaluate when simplifying
657 | TotalFn | PartialFn | CoveringFn
658 | Coinductive | AssertTotal
659 | Dictionary -- type class dictionary, eval only when
660 -- a function argument, and further evaluation resutls
661 | Implicit -- implicit coercion
662 | NoImplicit -- do not apply implicit coercions
663 | CExport String -- export, with a C name
664 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
665 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
666 | Reflection -- a reflecting function, compile-time only
667 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
668 | Constructor -- Data constructor type
669 | AutoHint -- use in auto implicit search
670 | PEGenerated -- generated by partial evaluator
673deriving instance Binary FnOpt
674deriving instance NFData FnOpt
679inlinable :: FnOpts -> Bool
680inlinable = elem Inlinable
682dictionary :: FnOpts -> Bool
683dictionary = elem Dictionary
686-- | Type provider - what to provide
687data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
688 | ProvPostulate t -- ^ goal type must be Type, so only term
689 deriving (Show, Eq, Functor)
691type ProvideWhat = ProvideWhat' PTerm
693-- | Top-level declarations such as compiler directives, definitions,
694-- datatypes and typeclasses.
696 = PFix FC Fixity [String] -- ^ Fixity declaration
697 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
698 | PPostulate Bool -- external def if true
699 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
700 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
701 | PCAF FC Name t -- ^ Top level constant
702 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
703 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
704 | PNamespace String FC [PDecl' t]
705 -- ^ New namespace, where FC is accurate location of the
706 -- namespace in the file
707 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
709 FC -- Record name precise location
710 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
711 [(Name, Docstring (Either Err t))] -- Param Docs
712 [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
713 (Maybe (Name, FC)) -- Optional constructor name and location
714 (Docstring (Either Err t)) -- Constructor doc
715 SyntaxInfo -- Constructor SyntaxInfo
716 -- ^ Record declaration
717 | PClass (Docstring (Either Err t)) SyntaxInfo FC
718 [(Name, t)] -- constraints
720 FC -- accurate location of class name
721 [(Name, FC, t)] -- parameters and precise locations
722 [(Name, Docstring (Either Err t))] -- parameter docstrings
723 [(Name, FC)] -- determining parameters and precise locations
724 [PDecl' t] -- declarations
725 (Maybe (Name, FC)) -- instance constructor name and location
726 (Docstring (Either Err t)) -- instance constructor docs
727 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
728 -- class name, class name location, parameters, method declarations, optional constructor name
730 (Docstring (Either Err t)) -- Instance docs
731 [(Name, Docstring (Either Err t))] -- Parameter docs
733 FC [(Name, t)] -- constraints
737 FC -- precise location of class
739 t -- full instance type
740 (Maybe Name) -- explicit name
742 -- ^ Instance declaration: arguments are documentation, syntax info, source
743 -- location, constraints, class name, parameters, full instance
744 -- type, optional explicit name, and definitions
745 | PDSL Name (DSL' t) -- ^ DSL declaration
746 | PSyntax FC Syntax -- ^ Syntax definition
747 | PMutual FC [PDecl' t] -- ^ Mutual block
748 | PDirective Directive -- ^ Compiler directive.
749 | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.
750 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
751 -- bool is True, lhs and rhs must be convertible
752 | PRunElabDecl FC t [String] -- ^ FC is decl-level, for errors, and
753 -- Strings represent the namespace
756deriving instance Binary PDecl'
757deriving instance NFData PDecl'
760-- | The set of source directives
761data Directive = DLib Codegen String |
762 DLink Codegen String |
763 DFlag Codegen String |
764 DInclude Codegen String |
767 DAccess Accessibility |
770 DDynamicLibs [String] |
771 DNameHint Name FC [(Name, FC)] |
772 DErrorHandlers Name FC Name FC [(Name, FC)] |
773 DLanguage LanguageExt |
774 DDeprecate Name String |
775 DAutoImplicits Bool |
778-- | A set of instructions for things that need to happen in IState
779-- after a term elaboration when there's been reflected elaboration.
780data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
781 | RClausesInstrs Name [([(Name, Term)], Term, Term)]
782 | RAddInstance Name Name
783 | RDatatypeDeclInstrs Name [PArg]
784 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
785 -- ^ Datatype, constructors
787-- | For elaborator state
788data EState = EState {
789 case_decls :: [(Name, PDecl)],
790 delayed_elab :: [(Int, Elab' EState ())],
791 new_tyDecls :: [RDeclInstructions],
792 highlighting :: [(FC, OutputAnnotation)],
793 auto_binds :: [Name], -- names bound as auto implicits
794 implicit_warnings :: [(FC, Name)] -- Implicit warnings to report (location and global name)
798initEState = EState [] [] [] [] [] []
800type ElabD a = Elab' EState a
802highlightSource :: FC -> OutputAnnotation -> ElabD ()
803highlightSource fc annot =
804 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
806-- | One clause of a top-level definition. Term arguments to constructors are:
808-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
810-- 2. The list of extra 'with' patterns
812-- 3. The right-hand side
814-- 4. The where block (PDecl' t)
816data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
817 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
818 | PClauseR FC [t] t [PDecl' t]
819 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
822deriving instance Binary PClause'
823deriving instance NFData PClause'
827data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
828 d_name_fc :: FC, -- ^ The precise location of the type constructor name
829 d_tcon :: t, -- ^ Type constructor
830 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
832 -- ^ Data declaration
833 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
834 -- ^ "Placeholder" for data whose constructors are defined later
837-- | Transform the FCs in a PData and its associated terms. The first
838-- function transforms the general-purpose FCs, and the second transforms
839-- those that are used for semantic source highlighting, so they can be
841mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
842mapPDataFC f g (PDatadecl n nfc tycon ctors) =
843 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
844 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
845 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
846mapPDataFC f g (PLaterdecl n nfc tycon) =
847 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
849deriving instance Binary PData'
850deriving instance NFData PData'
853-- Handy to get a free function for applying PTerm -> PTerm functions
854-- across a program, by deriving Functor
856type PDecl = PDecl' PTerm
857type PData = PData' PTerm
858type PClause = PClause' PTerm
860-- | Transform the FCs in a PTerm. The first function transforms the
861-- general-purpose FCs, and the second transforms those that are used
862-- for semantic source highlighting, so they can be treated specially.
863mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
864mapPDeclFC f g (PFix fc fixity ops) =
865 PFix (f fc) fixity ops
866mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
867 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
868mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
869 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
871mapPDeclFC f g (PClauses fc opts n clauses) =
872 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
873mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
874mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
875 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
876mapPDeclFC f g (PParams fc params decls) =
878 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
879 (map (mapPDeclFC f g) decls)
880mapPDeclFC f g (PNamespace ns fc decls) =
881 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
882mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
883 PRecord doc syn (f fc) opts n (g nfc)
884 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
886 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
887 plic, mapPTermFC f g ty, fdoc))
889 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
892mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
893 PClass doc syn (f fc)
894 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
895 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
896 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
897 (map (mapPDeclFC f g) body)
898 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
900mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc opts cnfc params instTy instN body) =
901 PInstance doc paramDocs syn (f fc)
902 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
903 cn acc opts (g cnfc) (map (mapPTermFC f g) params)
904 (mapPTermFC f g instTy)
906 (map (mapPDeclFC f g) body)
907mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
908mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
910 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
911 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
912mapPDeclFC f g (PMutual fc decls) =
913 PMutual (f fc) (map (mapPDeclFC f g) decls)
914mapPDeclFC f g (PDirective d) =
917 DNameHint n nfc ns ->
918 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
919 DErrorHandlers n nfc n' nfc' ns ->
920 DErrorHandlers n (g nfc) n' (g nfc') $
921 map (\(an, anfc) -> (an, g anfc)) ns
922mapPDeclFC f g (PProvider doc syn fc nfc what n) =
923 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
924mapPDeclFC f g (PTransform fc safe l r) =
925 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
926mapPDeclFC f g (PRunElabDecl fc script ns) =
927 PRunElabDecl (f fc) (mapPTermFC f g script) ns
929-- | Get all the names declared in a declaration
930declared :: PDecl -> [Name]
931declared (PFix _ _ _) = []
932declared (PTy _ _ _ _ _ n fc t) = [n]
933declared (PPostulate _ _ _ _ _ _ n t) = [n]
934declared (PClauses _ _ n _) = [] -- not a declaration
935declared (PCAF _ n _) = [n]
936declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
937 where fstt (_, _, a, _, _, _, _) = a
938declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
939declared (PParams _ _ ds) = concatMap declared ds
940declared (PNamespace _ _ ds) = concatMap declared ds
941declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
942declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
943declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
944declared (PDSL n _) = [n]
945declared (PSyntax _ _) = []
946declared (PMutual _ ds) = concatMap declared ds
947declared (PDirective _) = []
950-- get the names declared, not counting nested parameter blocks
951tldeclared :: PDecl -> [Name]
952tldeclared (PFix _ _ _) = []
953tldeclared (PTy _ _ _ _ _ n _ t) = [n]
954tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
955tldeclared (PClauses _ _ n _) = [] -- not a declaration
956tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
957tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
958 where fstt (_, _, a, _, _, _, _) = a
959tldeclared (PParams _ _ ds) = []
960tldeclared (PMutual _ ds) = concatMap tldeclared ds
961tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
962tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
963tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
966defined :: PDecl -> [Name]
967defined (PFix _ _ _) = []
968defined (PTy _ _ _ _ _ n _ t) = []
969defined (PPostulate _ _ _ _ _ _ n t) = []
970defined (PClauses _ _ n _) = [n] -- not a declaration
971defined (PCAF _ n _) = [n]
972defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
973 where fstt (_, _, a, _, _, _, _) = a
974defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
975defined (PParams _ _ ds) = concatMap defined ds
976defined (PNamespace _ _ ds) = concatMap defined ds
977defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
978defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
979defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []
980defined (PDSL n _) = [n]
981defined (PSyntax _ _) = []
982defined (PMutual _ ds) = concatMap defined ds
983defined (PDirective _) = []
986updateN :: [(Name, Name)] -> Name -> Name
987updateN ns n | Just n' <- lookup n ns = n'
990updateNs :: [(Name, Name)] -> PTerm -> PTerm
992updateNs ns t = mapPT updateRef t
993 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
996-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
998-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
999-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
1000-- where updateCNs ns (PClause n l ts r ds)
1001-- = PClause (updateN ns n) (fmap (updateNs ns) l)
1002-- (map (fmap (updateNs ns)) ts)
1003-- (fmap (updateNs ns) r)
1004-- (map (updateDNs ns) ds)
1005-- updateDNs ns c = c
1007data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
1009-- | High level language terms
1010data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
1011 | PRef FC [FC] Name -- ^ A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.
1012 | PInferRef FC [FC] Name -- ^ A name to be defined later
1013 | PPatvar FC Name -- ^ A pattern variable
1014 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
1015 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
1016 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
1017 | PTyped PTerm PTerm -- ^ Term with explicit type
1018 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
1019 | PWithApp FC PTerm PTerm -- ^ Application plus a 'with' argument
1020 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
1021 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
1022 | PMatchApp FC Name -- ^ Make an application by type matching
1023 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
1024 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
1025 | PTrue FC PunInfo -- ^ Unit type..?
1026 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
1027 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
1028 -- ^ "rewrite" syntax, with optional rewriting function
1029 -- and optional result type
1030 | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.
1031 | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.
1032 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
1033 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
1034 | PHidden PTerm -- ^ Irrelevant or hidden pattern
1035 | PType FC -- ^ 'Type' type
1036 | PUniverse Universe -- ^ Some universe
1037 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
1038 | PConstant FC Const -- ^ Builtin types
1039 | Placeholder -- ^ Underscore
1040 | PDoBlock [PDo] -- ^ Do notation
1041 | PIdiom FC PTerm -- ^ Idiom brackets
1043 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
1044 | PProof [PTactic] -- ^ Proof script
1045 | PTactics [PTactic] -- ^ As PProof, but no auto solving
1046 | PElabError Err -- ^ Error to report on elaboration
1047 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
1048 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
1049 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
1050 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
1051 | PNoImplicits PTerm -- ^ never run implicit converions on the term
1052 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
1053 | PUnquote PTerm -- ^ ~Term
1054 | PQuoteName Name Bool FC -- ^ `{n} where the FC is the precise highlighting for the name in particular. If the Bool is False, then it's `{{n}} and the name won't be resolved.
1055 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
1056 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
1057 deriving (Eq, Data, Typeable)
1059data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
1062 deriving (Eq, Data, Typeable)
1064-- | Transform the FCs in a PTerm. The first function transforms the
1065-- general-purpose FCs, and the second transforms those that are used
1066-- for semantic source highlighting, so they can be treated specially.
1067mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
1068mapPTermFC f g (PQuote q) = PQuote q
1069mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
1070mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
1071mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
1072mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
1073mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1074mapPTermFC 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)
1075mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
1076mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1077mapPTermFC f g (PWithApp fc t arg) = PWithApp (f fc) (mapPTermFC f g t) (mapPTermFC f g arg)
1078mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
1079mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
1080mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
1081mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
1082mapPTermFC 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)
1083mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1084mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1085mapPTermFC 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)
1086mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1087mapPTermFC 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)
1088mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1089mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1090mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1091mapPTermFC f g (PType fc) = PType (f fc)
1092mapPTermFC f g (PUniverse u) = PUniverse u
1093mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1094mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1095mapPTermFC f g Placeholder = Placeholder
1096mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1097 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1098 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1099 mapPDoFC (DoBindP fc t1 t2 alts) =
1100 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1101 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1102 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1103mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1104mapPTermFC f g (PReturn fc) = PReturn (f fc)
1105mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1106mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1107mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1108mapPTermFC f g (PElabError err) = PElabError err
1109mapPTermFC f g PImpossible = PImpossible
1110mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1111mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1112mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1113mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1114mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1115mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1116mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1117mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1118mapPTermFC f g (PQuoteName n x fc) = PQuoteName n x (g fc)
1121dg instance Binary PTerm
1122deriving instance NFData PTerm
1125mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1126mapPT f t = f (mpt t) where
1127 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1128 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1129 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1130 mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)
1131 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1132 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)
1133 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1134 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1135 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1136 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1137 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1138 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1139 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1140 mpt (PHidden t) = PHidden (mapPT f t)
1141 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1142 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1143 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1144 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1145 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1146 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1147 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1151data PTactic' t = Intro [Name] | Intros | Focus Name
1152 | Refine Name [Bool] | Rewrite t | DoUnify
1159 | LetTac Name t | LetTacTy Name t t
1160 | Exact t | Compute | Trivial | TCInstance
1161 | ProofSearch Bool Bool Int (Maybe Name)
1162 [Name] -- allowed local names
1164 -- ^ the bool is whether to search recursively
1167 | ProofState | ProofTerm | Undo
1168 | Try (PTactic' t) (PTactic' t)
1169 | TSeq (PTactic' t) (PTactic' t)
1170 | ApplyTactic t -- see Language.Reflection module
1174 | GoalType String (PTactic' t)
1177 | TDocStr (Either Name Const)
1180 | TFail [ErrorReportPart]
1183 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1185deriving instance Binary PTactic'
1186deriving instance NFData PTactic'
1188instance Sized a => Sized (PTactic' a) where
1189 size (Intro nms) = 1 + size nms
1191 size (Focus nm) = 1 + size nm
1192 size (Refine nm bs) = 1 + size nm + length bs
1193 size (Rewrite t) = 1 + size t
1194 size (Induction t) = 1 + size t
1195 size (LetTac nm t) = 1 + size nm + size t
1196 size (Exact t) = 1 + size t
1204 size (Try l r) = 1 + size l + size r
1205 size (TSeq l r) = 1 + size l + size r
1206 size (ApplyTactic t) = 1 + size t
1207 size (Reflect t) = 1 + size t
1208 size (Fill t) = 1 + size t
1212 size (TFail ts) = 1 + size ts
1215 size (CaseTac x) = 1 + size x
1216 size (Equiv t) = 1 + size t
1217 size (Claim x y) = 1 + size x + size y
1219 size (MatchRefine x) = 1 + size x
1220 size (LetTacTy x y z) = 1 + size x + size y + size z
1223type PTactic = PTactic' PTerm
1225data PDo' t = DoExp FC t
1226 | DoBind FC Name FC t -- ^ second FC is precise name location
1227 | DoBindP FC t t [(t,t)]
1228 | DoLet FC Name FC t t -- ^ second FC is precise name location
1230 deriving (Eq, Functor, Data, Typeable)
1232deriving instance Binary PDo'
1233deriving instance NFData PDo'
1236instance Sized a => Sized (PDo' a) where
1237 size (DoExp fc t) = 1 + size fc + size t
1238 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1239 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1240 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1241 size (DoLetP fc l r) = 1 + size fc + size l + size r
1243type PDo = PDo' PTerm
1245-- The priority gives a hint as to elaboration order. Best to elaborate
1246-- things early which will help give a more concrete type to other
1247-- variables, e.g. a before (interpTy a).
1249data PArg' t = PImp { priority :: Int,
1250 machine_inf :: Bool, -- true if the machine inferred it
1251 argopts :: [ArgOpt],
1254 | PExp { priority :: Int,
1255 argopts :: [ArgOpt],
1258 | PConstraint { priority :: Int,
1259 argopts :: [ArgOpt],
1262 | PTacImplicit { priority :: Int,
1263 argopts :: [ArgOpt],
1267 deriving (Show, Eq, Functor, Data, Typeable)
1269data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1270 deriving (Show, Eq, Data, Typeable)
1272instance Sized a => Sized (PArg' a) where
1273 size (PImp p _ l nm trm) = 1 + size nm + size trm
1274 size (PExp p l nm trm) = 1 + size nm + size trm
1275 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1276 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1279deriving instance Binary PArg'
1280deriving instance NFData PArg'
1283pimp n t mach = PImp 1 mach [] n t
1284pexp t = PExp 1 [] (sMN 0 "arg") t
1285pconst t = PConstraint 1 [] (sMN 0 "carg") t
1286ptacimp n s t = PTacImplicit 2 [] n s t
1288type PArg = PArg' PTerm
1290-- | Get the highest FC in a term, if one exists
1291highestFC :: PTerm -> Maybe FC
1292highestFC (PQuote _) = Nothing
1293highestFC (PRef fc _ _) = Just fc
1294highestFC (PInferRef fc _ _) = Just fc
1295highestFC (PPatvar fc _) = Just fc
1296highestFC (PLam fc _ _ _ _) = Just fc
1297highestFC (PPi _ _ _ _ _) = Nothing
1298highestFC (PLet fc _ _ _ _ _) = Just fc
1299highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1300highestFC (PApp fc _ _) = Just fc
1301highestFC (PAppBind fc _ _) = Just fc
1302highestFC (PMatchApp fc _) = Just fc
1303highestFC (PCase fc _ _) = Just fc
1304highestFC (PIfThenElse fc _ _ _) = Just fc
1305highestFC (PTrue fc _) = Just fc
1306highestFC (PResolveTC fc) = Just fc
1307highestFC (PRewrite fc _ _ _ _) = Just fc
1308highestFC (PPair fc _ _ _ _) = Just fc
1309highestFC (PDPair fc _ _ _ _ _) = Just fc
1310highestFC (PAs fc _ _) = Just fc
1311highestFC (PAlternative _ _ args) =
1312 case mapMaybe highestFC args of
1315highestFC (PHidden _) = Nothing
1316highestFC (PType fc) = Just fc
1317highestFC (PUniverse _) = Nothing
1318highestFC (PGoal fc _ _ _) = Just fc
1319highestFC (PConstant fc _) = Just fc
1320highestFC Placeholder = Nothing
1321highestFC (PDoBlock lines) =
1322 case map getDoFC lines of
1326 getDoFC (DoExp fc t) = fc
1327 getDoFC (DoBind fc nm nfc t) = fc
1328 getDoFC (DoBindP fc l r alts) = fc
1329 getDoFC (DoLet fc nm nfc l r) = fc
1330 getDoFC (DoLetP fc l r) = fc
1332highestFC (PIdiom fc _) = Just fc
1333highestFC (PReturn fc) = Just fc
1334highestFC (PMetavar fc _) = Just fc
1335highestFC (PProof _) = Nothing
1336highestFC (PTactics _) = Nothing
1337highestFC (PElabError _) = Nothing
1338highestFC PImpossible = Nothing
1339highestFC (PCoerced tm) = highestFC tm
1340highestFC (PDisamb _ opts) = highestFC opts
1341highestFC (PUnifyLog tm) = highestFC tm
1342highestFC (PNoImplicits tm) = highestFC tm
1343highestFC (PQuasiquote _ _) = Nothing
1344highestFC (PUnquote tm) = highestFC tm
1345highestFC (PQuoteName _ _ fc) = Just fc
1346highestFC (PRunElab fc _ _) = Just fc
1347highestFC (PConstSugar fc _) = Just fc
1348highestFC (PAppImpl t _) = highestFC t
1352data ClassInfo = CI { instanceCtorName :: Name,
1353 class_methods :: [(Name, (FnOpts, PTerm))],
1354 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1355 class_default_superclasses :: [PDecl],
1356 class_params :: [Name],
1357 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1358 class_determiners :: [Int] }
1361deriving instance Binary ClassInfo
1362deriving instance NFData ClassInfo
1366data RecordInfo = RI { record_parameters :: [(Name,PTerm)],
1367 record_constructor :: Name,
1368 record_projections :: [Name] }
1371-- Type inference data
1373data TIData = TIPartial -- ^ a function with a partially defined type
1374 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1377-- | Miscellaneous information about functions
1378data FnInfo = FnInfo { fn_params :: [Int] }
1381deriving instance Binary FnInfo
1382deriving instance NFData FnInfo
1385data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1386 detaggable :: Bool }
1389deriving instance Binary OptInfo
1390deriving instance NFData OptInfo
1393-- | Syntactic sugar info
1394data DSL' t = DSL { dsl_bind :: t,
1399 index_first :: Maybe t,
1400 index_next :: Maybe t,
1401 dsl_lambda :: Maybe t,
1405 deriving (Show, Functor)
1407deriving instance Binary DSL'
1408deriving instance NFData DSL'
1411type DSL = DSL' PTerm
1413data SynContext = PatternSyntax | TermSyntax | AnySyntax
1416deriving instance Binary SynContext
1417deriving instance NFData SynContext
1420data Syntax = Rule [SSymbol] PTerm SynContext
1421 | DeclRule [SSymbol] [PDecl]
1424syntaxNames :: Syntax -> [Name]
1425syntaxNames (Rule syms _ _) = mapMaybe ename syms
1426 where ename (Keyword n) = Just n
1428syntaxNames (DeclRule syms _) = mapMaybe ename syms
1429 where ename (Keyword n) = Just n
1432syntaxSymbols :: Syntax -> [SSymbol]
1433syntaxSymbols (Rule ss _ _) = ss
1434syntaxSymbols (DeclRule ss _) = ss
1436deriving instance Binary Syntax
1437deriving instance NFData Syntax
1440data SSymbol = Keyword Name
1449deriving instance Binary SSymbol
1450deriving instance NFData SSymbol
1453newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1455emptySyntaxRules :: SyntaxRules
1456emptySyntaxRules = SyntaxRules []
1458updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1459updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1461 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1466 ruleSort (s1:ss1) (s2:ss2) =
1467 case symCompare s1 s2 of
1468 EQ -> ruleSort ss1 ss2
1471 -- Better than creating Ord instance for SSymbol since
1472 -- in general this ordering does not really make sense.
1473 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1474 symCompare (Keyword _) _ = LT
1475 symCompare (Symbol _) (Keyword _) = GT
1476 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1477 symCompare (Symbol _) _ = LT
1478 symCompare (Binding _) (Keyword _) = GT
1479 symCompare (Binding _) (Symbol _) = GT
1480 symCompare (Binding b1) (Binding b2) = compare b1 b2
1481 symCompare (Binding _) _ = LT
1482 symCompare (Expr _) (Keyword _) = GT
1483 symCompare (Expr _) (Symbol _) = GT
1484 symCompare (Expr _) (Binding _) = GT
1485 symCompare (Expr e1) (Expr e2) = compare e1 e2
1486 symCompare (Expr _) _ = LT
1487 symCompare (SimpleExpr _) (Keyword _) = GT
1488 symCompare (SimpleExpr _) (Symbol _) = GT
1489 symCompare (SimpleExpr _) (Binding _) = GT
1490 symCompare (SimpleExpr _) (Expr _) = GT
1491 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1493initDSL = DSL (PRef f [] (sUN ">>="))
1494 (PRef f [] (sUN "return"))
1495 (PRef f [] (sUN "<*>"))
1496 (PRef f [] (sUN "pure"))
1503 where f = fileFC "(builtin)"
1505data Using = UImplicit Name PTerm
1506 | UConstraint Name [Name]
1507 deriving (Show, Eq, Data, Typeable)
1509deriving instance Binary Using
1510deriving instance NFData Using
1513data SyntaxInfo = Syn { using :: [Using],
1514 syn_params :: [(Name, PTerm)],
1515 syn_namespace :: [String],
1517 imp_methods :: [Name], -- class methods. When expanding
1518 -- implicits, these should be expanded even under
1520 decoration :: Name -> Name,
1522 implicitAllowed :: Bool,
1523 maxline :: Maybe Int,
1526 syn_in_quasiquote :: Int,
1527 syn_toplevel :: Bool,
1528 withAppAllowed :: Bool }
1531deriving instance NFData SyntaxInfo
1532deriving instance Binary SyntaxInfo
1535defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0 True True
1537expandNS :: SyntaxInfo -> Name -> Name
1538expandNS syn n@(NS _ _) = n
1539expandNS syn n = case syn_namespace syn of
1544-- For inferring types of things
1546bi = fileFC "builtin"
1548inferTy = sMN 0 "__Infer"
1549inferCon = sMN 0 "__infer"
1550inferDecl = PDatadecl inferTy NoFC
1552 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1553 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1554 (PRef bi [] inferTy)), bi, [])]
1557infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1558infP = P (TCon 6 0) inferTy (TType (UVal 0))
1560getInferTerm, getInferType :: Term -> Term
1561getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1562getInferTerm (App _ (App _ _ _) tm) = tm
1563getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1565getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1566 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1567 toTy (PVar t) = PVTy t
1569getInferType (App _ (App _ _ ty) _) = ty
1573-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1575primNames = [inferTy, inferCon]
1578unitCon = sUN "MkUnit"
1580falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1581 "The empty type, also known as the trivially false proposition." ++
1583 "Use `void` or `absurd` to prove anything if you have a variable " ++
1584 "of type `Void` in scope."
1587pairTy = sNS (sUN "Pair") ["Builtins"]
1588pairCon = sNS (sUN "MkPair") ["Builtins"]
1590upairTy = sNS (sUN "UPair") ["Builtins"]
1591upairCon = sNS (sUN "MkUPair") ["Builtins"]
1595eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1596 "The propositional equality type. A proof that `x` = `y`." ++
1598 "To use such a proof, pattern-match on it, and the two equal things will " ++
1599 "then need to be the _same_ pattern." ++
1601 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1602 "is possible to state equalities between values of potentially different " ++
1603 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1605 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1607eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1608 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1610 [(reflDoc, reflParamDoc,
1611 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1612 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1613 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1614 pimp (n "B") Placeholder False,
1615 pexp (PRef bi [] (n "x")),
1616 pexp (PRef bi [] (n "x"))])), bi, [])]
1618 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1619 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1620 "shown that both sides are in fact equal."
1621 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1622 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1624eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1625 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1631-- | The special name to be used in the module documentation context -
1632-- not for use in the main definition context. The namespace around it
1633-- will determine the module to which the docs adhere.
1635modDocName = sMN 0 "ModuleDocs"
1637-- Defined in builtins.idr
1638sigmaTy = sNS (sUN "DPair") ["Builtins"]
1639sigmaCon = sNS (sUN "MkDPair") ["Builtins"]
1641piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1642piBind = piBindp expl
1644piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1646piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1649-- Pretty-printing declarations and terms
1651-- These "show" instances render to an absurdly wide screen because inserted line breaks
1652-- could interfere with interactive editing, which calls "show".
1654instance Show PTerm where
1655 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1657instance Show PDecl where
1658 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1660instance Show PClause where
1661 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1663instance Show PData where
1664 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1666instance Pretty PTerm OutputAnnotation where
1667 pretty = prettyImp defaultPPOption
1669-- | Colourise annotations according to an Idris state. It ignores the names
1670-- in the annotation, as there's no good way to show extended information on a
1672annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1673annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1674annotationColour ist (AnnConst c) =
1675 let theme = idris_colourTheme ist
1676 in Just $ if constIsType c
1677 then typeColour theme
1678 else dataColour theme
1679annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1680annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1681annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1682annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1683annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1684annotationColour ist (AnnName n _ _ _) =
1685 let ctxt = tt_ctxt ist
1686 theme = idris_colourTheme ist
1688 _ | isDConName n ctxt -> Just $ dataColour theme
1689 _ | isFnName n ctxt -> Just $ functionColour theme
1690 _ | isTConName n ctxt -> Just $ typeColour theme
1691 _ | isPostulateName n ist -> Just $ postulateColour theme
1692 _ | otherwise -> Nothing -- don't colourise unknown names
1693annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1694 where colour BoldText = IdrisColour Nothing True False True False
1695 colour UnderlineText = IdrisColour Nothing True True False False
1696 colour ItalicText = IdrisColour Nothing True False False True
1697annotationColour ist _ = Nothing
1700-- | Colourise annotations according to an Idris state. It ignores the names
1701-- in the annotation, as there's no good way to show extended
1702-- information on a terminal. Note that strings produced this way will
1703-- not be coloured on Windows, so the use of the colour rendering
1704-- functions in Idris.Output is to be preferred.
1705consoleDecorate :: IState -> OutputAnnotation -> String -> String
1706consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1708isPostulateName :: Name -> IState -> Bool
1709isPostulateName n ist = S.member n (idris_postulates ist)
1711-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1712prettyImp :: PPOption -- ^^ pretty printing options
1713 -> PTerm -- ^^ the term to pretty-print
1714 -> Doc OutputAnnotation
1715prettyImp impl = pprintPTerm impl [] [] []
1717-- | Serialise something to base64 using its Binary instance.
1719-- | Do the right thing for rendering a term in an IState
1720prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1721prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1723-- | Pretty-print a high-level Idris term in some bindings context with infix info
1724pprintPTerm :: PPOption -- ^^ pretty printing options
1725 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1726 -> [Name] -- ^^ names to always show in pi, even if not used
1727 -> [FixDecl] -- ^^ Fixity declarations
1728 -> PTerm -- ^^ the term to pretty-print
1729 -> Doc OutputAnnotation
1730pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1735 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1736 prettySe d p bnd (PQuote r) =
1737 text "![" <> pretty r <> text "]"
1738 prettySe d p bnd (PPatvar fc n) = pretty n
1740 | Just str <- slist d p bnd e = depth d $ str
1741 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1742 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1743 prettySe d p bnd (PLam fc n nfc ty sc) =
1744 depth d . bracket p startPrec . group . align . hang 2 $
1745 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1746 prettySe (decD d) startPrec ((n, False):bnd) sc
1747 prettySe d p bnd (PLet fc n nfc ty v sc) =
1748 depth d . bracket p startPrec . group . align $
1749 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1750 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1751 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1752 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1753 || ppopt_pinames ppo && uname n =
1754 depth d . bracket p startPrec . group $
1755 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1756 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1758 depth d . bracket p startPrec . group $
1759 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1760 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1762 uname (UN n) = case str n of
1769 Static -> text "%static" <> space
1771 prettySe d p bnd (PPi (Imp l s _ fa _) n _ ty sc)
1773 depth d . bracket p startPrec $
1774 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1775 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1776 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1780 Static -> text "%static" <> space
1782 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1783 depth d . bracket p startPrec $
1784 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1785 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch{}])) n _ ty sc) =
1786 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1787 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1788 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1789 depth d . bracket p startPrec $
1790 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1791 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1792 -- This case preserves the behavior of the former constructor PEq.
1793 -- It should be removed if feasible when the pretty-printing of infix
1794 -- operators in general is improved.
1795 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1796 | n == eqTy, ppopt_impl ppo =
1797 depth d . bracket p eqPrec $
1798 enclose lparen rparen eq <+>
1799 align (group (vsep (map (prettyArgS (decD d) bnd)
1802 depth d . bracket p eqPrec . align . group $
1803 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1804 where eq = annName eqTy (text "=")
1806 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1807 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1808 | UN nm <- basename f
1809 , not (ppopt_impl ppo) && null (getShowArgs args) =
1810 prettyName True (ppopt_impl ppo) bnd f
1811 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1812 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1813 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1814 | UN nm <- basename op
1816 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1817 case getShowArgs args of
1819 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1820 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1821 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1822 (l@(PExp{}) : r@(PExp{}) : rest) ->
1823 depth d . bracket p funcAppPrec $
1824 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1825 align (group (vsep (map (prettyArgS d bnd) rest)))
1826 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1827 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1828 f = getFixity (opStr op)
1830 Nothing -> funcAppPrec + 1
1831 Just (Infixl p') -> p'
1832 Just f' -> prec f' + 1
1834 Nothing -> funcAppPrec + 1
1835 Just (Infixr p') -> p'
1836 Just f' -> prec f' + 1
1837 inFix l r = align . group $
1838 (prettySe (decD d) left bnd l <+> opName False) <$>
1839 group (prettySe (decD d) right bnd r)
1840 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1841 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1842 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1843 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1844 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1845 let args = getShowArgs as
1846 fp = prettySe (decD d) (startPrec + 1) bnd f
1847 shownArgs = if ppopt_impl ppo then as else args
1849 depth d . bracket p funcAppPrec . group $
1852 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1853 prettySe d p bnd (PWithApp _ f a) = prettySe d p bnd f <+> text "|" <+> prettySe d p bnd a
1854 prettySe d p bnd (PCase _ scr cases) =
1855 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1856 depth d (indent 2 (vsep (map ppcase cases)))
1858 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1859 ([(n, False) | n <- vars l] ++ bnd)
1860 in nest nestingSize $
1861 prettyCase l <+> text "=>" <+> prettyCase r
1862 -- Warning: this is a bit of a hack. At this stage, we don't have the
1863 -- global context, so we can't determine which names are constructors,
1864 -- which are types, and which are pattern variables on the LHS of the
1865 -- case pattern. We use the heuristic that names without a namespace
1866 -- are patvars, because right now case blocks in PTerms are always
1867 -- delaborated from TT before being sent to the pretty-printer. If they
1868 -- start getting printed directly, THIS WILL BREAK.
1869 -- Potential solution: add a list of known patvars to the cases in
1870 -- PCase, and have the delaborator fill it out, kind of like the pun
1871 -- disambiguation on PDPair.
1872 vars tm = filter noNS (allNamesIn tm)
1873 noNS (NS _ _) = False
1876 prettySe d p bnd (PIfThenElse _ c t f) =
1877 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1878 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1879 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1880 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1882 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1883 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1884 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1885 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1886 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1887 prettySe d p bnd (PRewrite _ by l r _) =
1888 depth d . bracket p startPrec $
1889 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l
1892 Just fn -> text "using" <+>
1893 prettyName True (ppopt_impl ppo) bnd fn) <+>
1894 text "in" <+> prettySe (decD d) startPrec bnd r
1895 prettySe d p bnd (PTyped l r) =
1896 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1897 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1898 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1899 align . group . vsep . punctuate (ann comma) $
1900 map (prettySe (decD d) startPrec bnd) elts
1901 where ann = case pun of
1903 IsType -> annName pairTy
1904 IsTerm -> annName pairCon
1905 prettySe d p bnd dpair@(PDPair _ _ pun l t r)
1906 | Just elts <- dPairElts dpair
1907 = depth d . enclose (annotated lparen) (annotated rparen) .
1908 align . group . vsep . punctuate (space <> annotated (text "**")) $
1914 annotated (text "**") <+>
1915 prettySe (decD d) startPrec (addBinding bnd) r <>
1917 where annotated = case pun of
1918 IsType -> annName sigmaTy
1919 IsTerm -> annName sigmaCon
1922 (left, addBinding) = case (l, pun) of
1923 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1924 _ -> (prettySe (decD d) startPrec bnd l, id)
1927 ppElts [(_, v)] bs = [prettySe (decD d) startPrec bs v]
1928 ppElts ((PRef _ _ n, t):rs) bs
1930 = (bindingOf n False <+> colon <+>
1931 prettySe (decD d) startPrec bs t) : ppElts rs ((n, False):bs)
1932 ppElts ((l, t):rs) bs
1933 = (prettySe (decD d) startPrec bs l) : ppElts rs bs
1934 prettySe d p bnd (PAlternative ns a as) =
1935 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1938 foldr ((\ l r -> l <+> text "," <+> r) .
1939 depth d . prettySe (decD d) startPrec bnd)
1941 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1942 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1943 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1944 -- XXX: add pretty for tactics
1945 prettySe d p bnd (PProof ts) =
1946 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1947 prettySe d p bnd (PTactics ts) =
1948 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1949 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1950 prettySe d p bnd (PReturn f) = kwd "return"
1951 prettySe d p bnd PImpossible = kwd "impossible"
1952 prettySe d p bnd Placeholder = text "_"
1953 prettySe d p bnd (PDoBlock dos) =
1954 bracket p startPrec $
1955 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1956 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1957 ppdo bnd (DoBind _ bn _ tm : dos) =
1958 (prettyBindingOf bn False <+> text "<-" <+>
1959 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1960 ppdo ((bn, False):bnd) dos
1961 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1962 text "no pretty printer for pattern-matching do binding" :
1964 ppdo bnd (DoLet _ ln _ ty v : dos) =
1965 (kwd "let" <+> prettyBindingOf ln False <+>
1966 (if ty /= Placeholder
1967 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1969 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1970 ppdo ((ln, False):bnd) dos
1971 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1972 text "no pretty printer for pattern-matching do binding" :
1975 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1976 prettySe d p bnd (PElabError s) = pretty s
1977 -- Quasiquote pprinting ignores bound vars
1978 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1979 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1980 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1981 prettySe d p bnd (PQuoteName n res _) = text start <> prettyName True (ppopt_impl ppo) bnd n <> text end
1982 where start = if res then "`{" else "`{{"
1983 end = if res then "}" else "}}"
1984 prettySe d p bnd (PRunElab _ tm _) =
1985 bracket p funcAppPrec . group . align . hang 2 $
1987 prettySe (decD d) funcAppPrec bnd tm
1988 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1989 prettySe d p bnd _ = text "missing pretty-printer for term"
1991 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1992 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1993 where display (UN n) = T.unpack n
1994 display (MN _ n) = T.unpack n
1995 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1996 display (NS n ns) = (intercalate "." . map T.unpack . reverse) ns ++ "." ++ display n
1999 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
2000 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
2001 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
2002 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
2004 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
2005 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2006 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
2007 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
2009 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
2010 annName n = annotate (AnnName n Nothing Nothing Nothing)
2012 opStr :: Name -> String
2013 opStr (NS n _) = opStr n
2014 opStr (UN n) = T.unpack n
2016 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
2017 slist' (Just d) _ _ _ | d <= 0 = Nothing
2019 | containsHole e = Nothing
2020 slist' d p bnd (PApp _ (PRef _ _ nil) _)
2021 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2022 slist' d p bnd (PRef _ _ nil)
2023 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
2024 slist' d p bnd (PApp _ (PRef _ _ cons) args)
2025 | nsroot cons == sUN "::",
2026 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
2028 Just tl' <- slist' (decD d) p bnd tl
2029 = Just (prettySe d startPrec bnd hd : tl')
2031 isImp (PImp {}) = True
2033 slist' _ _ _ tm = Nothing
2035 slist d p bnd e | Just es <- slist' d p bnd e = Just $
2037 [] -> annotate (AnnData "" "") $ text "[]"
2038 [x] -> enclose left right . group $ x
2039 xs -> enclose left right .
2040 align . group . vsep .
2041 punctuate comma $ xs
2042 where left = (annotate (AnnData "" "") (text "["))
2043 right = (annotate (AnnData "" "") (text "]"))
2044 comma = (annotate (AnnData "" "") (text ","))
2045 slist _ _ _ _ = Nothing
2047 pairElts :: PTerm -> Maybe [PTerm]
2048 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
2049 | otherwise = Just [x, y]
2050 pairElts _ = Nothing
2052 dPairElts :: PTerm -> Maybe [(PTerm, PTerm)]
2053 dPairElts (PDPair _ _ _ l t r) | Just elts <- dPairElts r = Just ((l, t):elts)
2054 | otherwise = Just [(l, t), (Placeholder, r)]
2055 dPairElts _ = Nothing
2057 natns = "Prelude.Nat."
2059 snat :: PPOption -> Maybe Int -> Int -> PTerm -> Maybe Integer
2061 | ppopt_desugarnats ppo = Nothing
2062 | otherwise = snat' d p e
2064 snat' :: Maybe Int -> Int -> PTerm -> Maybe Integer
2065 snat' (Just x) _ _ | x <= 0 = Nothing
2066 snat' d p (PRef _ _ z)
2067 | show z == (natns++"Z") || show z == "Z" = Just 0
2068 snat' d p (PApp _ s [PExp {getTm=n}])
2069 | show s == (natns++"S") || show s == "S",
2070 Just n' <- snat' (decD d) p n
2072 snat' _ _ _ = Nothing
2074 bracket outer inner doc
2075 | outer > inner = lparen <> doc <> rparen
2078 ellipsis = text "..."
2081 depth (Just d) = if d <= 0 then const ellipsis else id
2083 decD = fmap (\x -> x - 1)
2085 kwd = annotate AnnKeyword . text
2087 fixities :: M.Map String Fixity
2088 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
2090 getFixity :: String -> Maybe Fixity
2091 getFixity = flip M.lookup fixities
2093-- | Strip away namespace information
2094basename :: Name -> Name
2095basename (NS n _) = basename n
2098-- | Determine whether a name was the one inserted for a hole or
2099-- guess by the delaborator
2100isHoleName :: Name -> Bool
2101isHoleName (UN n) = n == T.pack "[__]"
2104-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
2105containsHole :: PTerm -> Bool
2106containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
2108-- | Pretty-printer helper for names that attaches the correct annotations
2110 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
2111 -> Bool -- ^^ whether to show namespaces
2112 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
2113 -> Name -- ^^ the name to pprint
2114 -> Doc OutputAnnotation
2115prettyName infixParen showNS bnd n
2116 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
2117 | (UN n') <- n, T.unpack n' == "_" = text "_"
2118 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2119 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2120 where fullName = text nameSpace <> parenthesise (text (baseName n))
2121 baseName (UN n) = T.unpack n
2122 baseName (NS n ns) = baseName n
2123 baseName (MN i s) = T.unpack s
2124 baseName other = show other
2125 nameSpace = case n of
2126 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2128 isInfix = case baseName n of
2130 (c : _) -> not (isAlpha c)
2131 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2134showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2135showCImp ppo (PClause _ n l ws r w)
2136 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2137 <+> text "where" <+> text (show w)
2140 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2141showCImp ppo (PWith _ n l ws r pn w)
2142 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2143 <+> braces (text (show w))
2146 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2149showDImp :: PPOption -> PData -> Doc OutputAnnotation
2150showDImp ppo (PDatadecl n nfc ty cons)
2151 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2152 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2154showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2155showDecls o ds = vsep (map (showDeclImp o) ds)
2157showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2158showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2159showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2160 indent 2 (vsep (map (showCImp o) cs))
2161showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2162showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2163showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2164showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2165showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2166 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2167showDeclImp o (PInstance _ _ _ _ cs acc _ n _ _ t _ ds)
2168 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2169showDeclImp _ _ = text "..."
2170-- showDeclImp (PImport o) = "import " ++ o
2172getImps :: [PArg] -> [(Name, PTerm)]
2174getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2175getImps (_ : xs) = getImps xs
2177getExps :: [PArg] -> [PTerm]
2179getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2180getExps (_ : xs) = getExps xs
2182getShowArgs :: [PArg] -> [PArg]
2184getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2185getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2186 | PImp _ _ _ _ tm <- e
2187 , containsHole tm = e : getShowArgs xs
2188getShowArgs (_ : xs) = getShowArgs xs
2190getConsts :: [PArg] -> [PTerm]
2192getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2193getConsts (_ : xs) = getConsts xs
2195getAll :: [PArg] -> [PTerm]
2200showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
2201 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
2202 -> PPOption -- ^^ pretty printing options
2203 -> Bool -- ^^ whether to colourise
2204 -> Name -- ^^ the term to show
2206showName ist bnd ppo colour n = case ist of
2207 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2208 Nothing -> showbasic n
2209 where name = if ppopt_impl ppo then show n else showbasic n
2210 showbasic n@(UN _) = showCG n
2211 showbasic (MN i s) = str s
2212 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2213 showbasic (SN s) = show s
2215 colourise n t = let ctxt' = fmap tt_ctxt ist in
2218 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2219 else colouriseBound t name
2220 | isDConName n ctxt -> colouriseData t name
2221 | isFnName n ctxt -> colouriseFun t name
2222 | isTConName n ctxt -> colouriseType t name
2223 -- The assumption is that if a name is not bound and does not exist in the
2224 -- global context, then we're somewhere in which implicit info has been lost
2225 -- (like error messages). Thus, unknown vars are colourised as implicits.
2226 | otherwise -> colouriseImplicit t name
2228showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
2229 -> PTerm -- ^^ the term to show
2231showTm ist = displayDecorated (consoleDecorate ist) .
2232 renderPretty 0.8 100000 .
2233 prettyImp (ppOptionIst ist)
2235-- | Show a term with implicits, no colours
2236showTmImpls :: PTerm -> String
2237showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2239-- | Show a term with specific options
2240showTmOpts :: PPOption -> PTerm -> String
2241showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2244instance Sized PTerm where
2245 size (PQuote rawTerm) = size rawTerm
2246 size (PRef fc _ name) = size name
2247 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2248 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2249 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2250 size (PTyped trm ty) = 1 + size trm + size ty
2251 size (PApp fc name args) = 1 + size args
2252 size (PAppBind fc name args) = 1 + size args
2253 size (PCase fc trm bdy) = 1 + size trm + size bdy
2254 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2255 size (PTrue fc _) = 1
2256 size (PResolveTC fc) = 1
2257 size (PRewrite fc by left right _) = 1 + size left + size right
2258 size (PPair fc _ _ left right) = 1 + size left + size right
2259 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2260 size (PAlternative _ a alts) = 1 + size alts
2261 size (PHidden hidden) = size hidden
2262 size (PUnifyLog tm) = size tm
2263 size (PDisamb _ tm) = size tm
2264 size (PNoImplicits tm) = size tm
2266 size (PUniverse _) = 1
2267 size (PConstant fc const) = 1 + size fc + size const
2268 size Placeholder = 1
2269 size (PDoBlock dos) = 1 + size dos
2270 size (PIdiom fc term) = 1 + size term
2271 size (PReturn fc) = 1
2272 size (PMetavar _ name) = 1
2273 size (PProof tactics) = size tactics
2274 size (PElabError err) = size err
2275 size PImpossible = 1
2278getPArity :: PTerm -> Int
2279getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2282-- Return all names, free or globally bound, in the given term.
2284allNamesIn :: PTerm -> [Name]
2285allNamesIn tm = nub $ ni 0 [] tm
2286 where -- TODO THINK added niTacImp, but is it right?
2287 ni 0 env (PRef _ _ n)
2288 | not (n `elem` env) = [n]
2289 ni 0 env (PPatvar _ n) = [n]
2290 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2291 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2292 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2293 ni 0 env (PIfThenElse _ c t f) = ni 0 env c ++ ni 0 env t ++ ni 0 env f
2294 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2295 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2296 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc
2297 ni 0 env (PHidden tm) = ni 0 env tm
2298 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2299 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2300 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2301 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r
2302 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2303 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2304 ni 0 env (PAlternative ns a ls) = concatMap (ni 0 env) ls
2305 ni 0 env (PUnifyLog tm) = ni 0 env tm
2306 ni 0 env (PDisamb _ tm) = ni 0 env tm
2307 ni 0 env (PNoImplicits tm) = ni 0 env tm
2309 ni i env (PQuasiquote tm ty) = ni (i+1) env tm ++ maybe [] (ni i env) ty
2310 ni i env (PUnquote tm) = ni (i - 1) env tm
2311 ni i env tm = concatMap (ni i env) (children tm)
2313 niTacImp i env (TacImp _ _ scr) = ni i env scr
2317-- Return all names defined in binders in the given term
2318boundNamesIn :: PTerm -> [Name]
2319boundNamesIn tm = S.toList (ni 0 S.empty tm)
2320 where -- TODO THINK Added niTacImp, but is it right?
2321 ni :: Int -> S.Set Name -> PTerm -> S.Set Name
2322 ni 0 set (PApp _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2323 ni 0 set (PAppBind _ f as) = niTms 0 (ni 0 set f) (map getTm as)
2324 ni 0 set (PCase _ c os) = niTms 0 (ni 0 set c) (map snd os)
2325 ni 0 set (PIfThenElse _ c t f) = niTms 0 set [c, t, f]
2326 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc
2327 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc
2328 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p
2329 ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r
2330 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r
2331 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r
2332 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r
2333 ni 0 set (PDPair _ _ _ l t r) = ni 0 (ni 0 (ni 0 set l) t) r
2334 ni 0 set (PAlternative ns a as) = niTms 0 set as
2335 ni 0 set (PHidden tm) = ni 0 set tm
2336 ni 0 set (PUnifyLog tm) = ni 0 set tm
2337 ni 0 set (PDisamb _ tm) = ni 0 set tm
2338 ni 0 set (PNoImplicits tm) = ni 0 set tm
2340 ni i set (PQuasiquote tm ty) = ni (i + 1) set tm `S.union` maybe S.empty (ni i set) ty
2341 ni i set (PUnquote tm) = ni (i - 1) set tm
2343 ni i set tm = foldr (S.union . ni i set) set (children tm)
2345 niTms :: Int -> S.Set Name -> [PTerm] -> S.Set Name
2346 niTms i set [] = set
2347 niTms i set (x : xs) = niTms i (ni i set x) xs
2349 niTacImp i set (TacImp _ _ scr) = ni i set scr
2350 niTacImp i set _ = set
2352-- Return names which are valid implicits in the given term (type).
2353implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2354implicitNamesIn uvars ist tm
2355 = let (imps, fns) = execState (ni 0 [] tm) ([], []) in
2358 addImp n = do (imps, fns) <- get
2360 addFn n = do (imps, fns) <- get
2364 notCAF (PExp _ _ _ _ : _) = True
2365 notCAF (_ : xs) = notCAF xs
2367 notHidden (n, _) = case getAccessibility n of
2373 = case lookupDefAccExact n False (tt_ctxt ist) of
2377 ni 0 env (PRef _ _ n@(NS _ _))
2378 | not (n `elem` env)
2379 -- Never implicitly bind if there's a namespace
2381 ni 0 env (PRef _ _ n)
2382 | not (n `elem` env) && implicitable n || n `elem` uvars = addImp n
2383 ni 0 env (PApp _ f@(PRef _ _ n) as)
2384 | n `elem` uvars = do ni 0 env f
2385 mapM_ (ni 0 env . getTm) as
2386 | otherwise = do case lookupTy n (tt_ctxt ist) of
2389 mapM_ (ni 0 env . getTm) as
2390 ni 0 env (PApp _ f as) = do ni 0 env f
2391 mapM_ (ni 0 env . getTm) as
2392 ni 0 env (PAppBind _ f as) = do ni 0 env f
2393 mapM_ (ni 0 env . getTm) as
2394 ni 0 env (PCase _ c os) = do ni 0 env c
2395 -- names in 'os', not counting the names bound in the cases
2396 mapM_ (ni 0 env . snd) os
2399 mapM_ (ni 0 env . fst) os
2401 put (nub imps \\ nub impsfst, fns)
2402 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]
2403 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2404 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc
2405 ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r
2406 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r
2407 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r
2408 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r
2409 ni 0 env (PDPair _ _ _ l t r) = do ni 0 env l
2412 ni 0 env (PAlternative ns a as) = mapM_ (ni 0 env) as
2413 ni 0 env (PHidden tm) = ni 0 env tm
2414 ni 0 env (PUnifyLog tm) = ni 0 env tm
2415 ni 0 env (PDisamb _ tm) = ni 0 env tm
2416 ni 0 env (PNoImplicits tm) = ni 0 env tm
2418 ni i env (PQuasiquote tm ty) = do ni (i + 1) env tm
2419 maybe (return ()) (ni i env) ty
2420 ni i env (PUnquote tm) = ni (i - 1) env tm
2422 ni i env tm = mapM_ (ni i env) (children tm)
2424-- Return names which are free in the given term.
2425namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2426namesIn uvars ist tm = nub $ ni 0 [] tm
2428 ni 0 env (PRef _ _ n)
2429 | not (n `elem` env)
2430 = case lookupTy n (tt_ctxt ist) of
2432 _ -> [n | n `elem` (map fst uvars)]
2433 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2434 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2435 ni 0 env (PCase _ c os) = ni 0 env c ++
2436 -- names in 'os', not counting the names bound in the cases
2437 (nub (concatMap (ni 0 env . snd) os)
2438 \\ nub (concatMap (ni 0 env . fst) os))
2439 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2440 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2441 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2442 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2443 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2444 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2445 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2446 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2447 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2448 ni 0 env (PHidden tm) = ni 0 env tm
2449 ni 0 env (PUnifyLog tm) = ni 0 env tm
2450 ni 0 env (PDisamb _ tm) = ni 0 env tm
2451 ni 0 env (PNoImplicits tm) = ni 0 env tm
2453 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2454 ni i env (PUnquote tm) = ni (i - 1) env tm
2456 ni i env tm = concatMap (ni i env) (children tm)
2458 niTacImp i env (TacImp _ _ scr) = ni i env scr
2461-- Return which of the given names are used in the given term.
2463usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2464usedNamesIn vars ist tm = nub $ ni 0 [] tm
2465 where -- TODO THINK added niTacImp, but is it right?
2466 ni 0 env (PRef _ _ n)
2467 | n `elem` vars && not (n `elem` env)
2468 = case lookupDefExact n (tt_ctxt ist) of
2471 ni 0 env (PApp _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2472 ni 0 env (PAppBind _ f as) = ni 0 env f ++ concatMap (ni 0 env . getTm) as
2473 ni 0 env (PCase _ c os) = ni 0 env c ++ concatMap (ni 0 env . snd) os
2474 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]
2475 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc
2476 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc
2477 ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r
2478 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r
2479 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r
2480 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r
2481 ni 0 env (PDPair _ _ _ l t r) = ni 0 env l ++ ni 0 env t ++ ni 0 env r
2482 ni 0 env (PAlternative ns a as) = concatMap (ni 0 env) as
2483 ni 0 env (PHidden tm) = ni 0 env tm
2484 ni 0 env (PUnifyLog tm) = ni 0 env tm
2485 ni 0 env (PDisamb _ tm) = ni 0 env tm
2486 ni 0 env (PNoImplicits tm) = ni 0 env tm
2488 ni i env (PQuasiquote tm ty) = ni (i + 1) env tm ++ maybe [] (ni i env) ty
2489 ni i env (PUnquote tm) = ni (i - 1) env tm
2491 ni i env tm = concatMap (ni i env) (children tm)
2493 niTacImp i env (TacImp _ _ scr) = ni i env scr
2496-- Return the list of inaccessible (= dotted) positions for a name.
2497getErasureInfo :: IState -> Name -> [Int]
2498getErasureInfo ist n =
2499 case lookupCtxtExact n (idris_optimisation ist) of
2500 Just (Optimise inacc detagg) -> map fst inacc
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list