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)
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 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
66toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not implemented")
68eInfoNames :: ElabInfo -> [Name]
69eInfoNames info = map fst (params info) ++ M.keys (inblock info)
71data IOption = IOption { opt_logLevel :: Int,
73 opt_typeintype :: Bool,
75 opt_showimp :: Bool, -- ^^ show implicits
76 opt_errContext :: Bool,
81 opt_codegen :: Codegen,
82 opt_outputTy :: OutputType,
83 opt_ibcsubdir :: FilePath,
84 opt_importdirs :: [FilePath],
87 opt_cmdline :: [Opt], -- remember whole command line
89 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
90 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
91 opt_optimise :: [Optimisation],
92 opt_printdepth :: Maybe Int,
93 opt_evaltypes :: Bool -- ^ normalise types in :t
97defaultOpts = IOption { opt_logLevel = 0
98 , opt_typecase = False
99 , opt_typeintype = False
100 , opt_coverage = True
101 , opt_showimp = False
102 , opt_errContext = False
105 , opt_nobanner = False
107 , opt_codegen = Via "c"
108 , opt_outputTy = Executable
110 , opt_importdirs = []
114 , opt_origerr = False
115 , opt_autoSolve = True
116 , opt_autoImport = []
117 , opt_optimise = defaultOptimise
118 , opt_printdepth = Just 5000
119 , opt_evaltypes = True
122data PPOption = PPOption {
123 ppopt_impl :: Bool -- ^^ whether to show implicits
124 , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings
125 , ppopt_depth :: Maybe Int
128data Optimisation = PETransform -- partial eval and associated transforms
131defaultOptimise = [PETransform]
133-- | Pretty printing options with default verbosity.
134defaultPPOption :: PPOption
135defaultPPOption = PPOption { ppopt_impl = False,
136 ppopt_pinames = False,
137 ppopt_depth = Just 200 }
139-- | Pretty printing options with the most verbosity.
140verbosePPOption :: PPOption
141verbosePPOption = PPOption { ppopt_impl = True,
142 ppopt_pinames = True,
143 ppopt_depth = Just 200 }
145-- | Get pretty printing options from the big options record.
146ppOption :: IOption -> PPOption
147ppOption opt = PPOption {
148 ppopt_impl = opt_showimp opt,
149 ppopt_pinames = False,
150 ppopt_depth = opt_printdepth opt
153-- | Get pretty printing options from an idris state record.
154ppOptionIst :: IState -> PPOption
155ppOptionIst = ppOption . idris_options
157data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
159-- | The output mode in use
160data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
161 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
164-- | How wide is the console?
165data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
166 | ColsWide Int -- ^ Manually specified - must be positive
167 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
171-- | The global state used in the Idris monad
172data IState = IState {
173 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
174 idris_constraints :: S.Set ConstraintFC,
175 -- ^ A list of universe constraints and their corresponding source locations
176 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
177 idris_implicits :: Ctxt [PArg],
178 idris_statics :: Ctxt [Bool],
179 idris_classes :: Ctxt ClassInfo,
180 idris_records :: Ctxt RecordInfo,
181 idris_dsls :: Ctxt DSL,
182 idris_optimisation :: Ctxt OptInfo,
183 idris_datatypes :: Ctxt TypeInfo,
184 idris_namehints :: Ctxt [Name],
185 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
186 -- ^ list of lhs/rhs, and a list of missing clauses
187 idris_flags :: Ctxt [FnOpt],
188 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
189 idris_calledgraph :: Ctxt [Name],
190 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
191 idris_moduledocs :: Ctxt (Docstring DocTerm),
192 -- ^ module documentation is saved in a special MN so the context
193 -- mechanism can be used for disambiguation
194 idris_tyinfodata :: Ctxt TIData,
195 idris_fninfo :: Ctxt FnInfo,
196 idris_transforms :: Ctxt [(Term, Term)],
197 idris_autohints :: Ctxt [Name],
198 idris_totcheck :: [(FC, Name)], -- names to check totality on
199 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
200 idris_totcheckfail :: [(FC, String)],
201 idris_options :: IOption,
203 idris_lineapps :: [((FilePath, Int), PTerm)],
204 -- ^ Full application LHS on source line
205 idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],
206 -- ^ The currently defined but not proven metavariables. The Int
207 -- is the number of vars to display as a context, the Maybe Name
208 -- is its top-level function, the [Name] is the list of local variables
209 -- available for proof search and the Bool is whether :p is
211 idris_coercions :: [Name],
212 idris_errRev :: [(Term, Term)],
213 syntax_rules :: SyntaxRules,
214 syntax_keywords :: [String],
215 imported :: [FilePath], -- ^ The imported modules
216 idris_scprims :: [(Name, (Int, PrimFn))],
217 idris_objs :: [(Codegen, FilePath)],
218 idris_libs :: [(Codegen, String)],
219 idris_cgflags :: [(Codegen, String)],
220 idris_hdrs :: [(Codegen, String)],
221 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
222 proof_list :: [(Name, (Bool, [String]))],
224 parserWarnings :: [(FC, Err)],
225 lastParse :: Maybe Name,
226 indent_stack :: [Int],
227 brace_stack :: [Maybe Int],
228 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
229 idris_parsedSpan :: Maybe FC,
230 hide_list :: [(Name, Maybe Accessibility)],
231 default_access :: Accessibility,
232 default_total :: Bool,
233 ibc_write :: [IBCWrite],
234 compiled_so :: Maybe String,
235 idris_dynamic_libs :: [DynamicLib],
236 idris_language_extensions :: [LanguageExt],
237 idris_outputmode :: OutputMode,
238 idris_colourRepl :: Bool,
239 idris_colourTheme :: ColourTheme,
240 idris_errorhandlers :: [Name], -- ^ Global error handlers
241 idris_nameIdx :: (Int, Ctxt (Int, Name)),
242 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
243 module_aliases :: M.Map [T.Text] [T.Text],
244 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
245 idris_postulates :: S.Set Name,
246 idris_externs :: S.Set (Name, Int),
247 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
248 idris_whocalls :: Maybe (M.Map Name [Name]),
249 idris_callswho :: Maybe (M.Map Name [Name]),
250 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
251 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
252 -- (instances appear twice; also as a funtion name)
253 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
254 idris_exports :: [Name], -- ^ Functions with ExportList
255 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
256 idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
259-- Required for parsers library, and therefore trifecta
260instance Show IState where
261 show = const "{internal state}"
263data SizeChange = Smaller | Same | Bigger | Unknown
266deriving instance Binary SizeChange
267deriving instance NFData SizeChange
270type SCGEntry = (Name, [Maybe (Int, SizeChange)])
271type UsageReason = (Name, Int) -- fn_name, its_arg_number
273data CGInfo = CGInfo { argsdef :: [Name],
274 calls :: [(Name, [[Name]])],
277 usedpos :: [(Int, [UsageReason])] }
280deriving instance Binary CGInfo
281deriving instance NFData CGInfo
284primDefs = [sUN "unsafePerformPrimIO",
285 sUN "mkLazyForeignPrim",
289-- information that needs writing for the current module's .ibc file
290data IBCWrite = IBCFix FixDecl
295 | IBCInstance Bool Bool Name Name
302 | IBCImport (Bool, FilePath) -- True = import public
303 | IBCImportDir FilePath
304 | IBCObj Codegen FilePath
305 | IBCLib Codegen String
306 | IBCCGFlag Codegen String
308 | IBCHeader Codegen String
309 | IBCAccess Name Accessibility
310 | IBCMetaInformation Name MetaInformation
311 | IBCTotal Name Totality
312 | IBCFlags Name [FnOpt]
313 | IBCFnInfo Name FnInfo
314 | IBCTrans Name (Term, Term)
315 | IBCErrRev (Term, Term)
319 | IBCDef Name -- i.e. main context
320 | IBCNameHint (Name, Name)
321 | IBCLineApp FilePath Int PTerm
322 | IBCErrorHandler Name
323 | IBCFunctionErrorHandler Name Name Name
325 | IBCExtern (Name, Int)
326 | IBCTotCheckErr FC String
328 | IBCModDocs Name -- ^ The name is the special name used to track module docs
329 | IBCUsage (Name, Int)
331 | IBCAutoHint Name Name
334-- | The initial state for the compiler
336idrisInit = IState initContext S.empty []
337 emptyContext emptyContext emptyContext emptyContext
338 emptyContext emptyContext emptyContext emptyContext
339 emptyContext emptyContext emptyContext emptyContext
340 emptyContext emptyContext emptyContext emptyContext
341 emptyContext emptyContext
342 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
343 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
344 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
345 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
347-- | The monad for the main REPL - reading and processing files and updating
348-- global state (hence the IO inner monad).
349--type Idris = WriterT [Either String (IO ())] (State IState a))
350type Idris = StateT IState (ExceptT Err IO)
352catchError :: Idris a -> (Err -> Idris a) -> Idris a
353catchError = liftCatch catchE
355throwError :: Err -> Idris a
356throwError = Trans.lift . throwE
358-- Commands in the REPL
360data Codegen = Via String
369deriving instance NFData Codegen
372data HowMuchDocs = FullDocs | OverviewDocs
378 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
382 | DocStr (Either Name Const) HowMuchDocs
385 | Load FilePath (Maybe Int) -- up to maximum line number
386 | ChangeDirectory FilePath
389 | Compile Codegen String
393 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
394 | AddProof (Maybe Name)
405 | DynamicLink FilePath
408 | Search [String] PTerm
409 | CaseSplitAt Bool Int Name
410 | AddClauseFrom Bool Int Name
411 | AddProofClauseFrom Bool Int Name
412 | AddMissing Bool Int Name
413 | MakeWith Bool Int Name
414 | MakeCase Bool Int Name
415 | MakeLemma Bool Int Name
416 | DoProofSearch Bool -- update file
417 Bool -- recursive search
419 Name -- top level name
424 | SetColour ColourType IdrisColour
428 | SetConsoleWidth ConsoleWidth
429 | SetPrinterDepth (Maybe Int)
430 | Apropos [String] String
434 | MakeDoc String -- IdrisDoc
437 | PPrint OutputFmt Int PTerm
439 -- Debugging commands
441 | DebugUnify PTerm PTerm
443data OutputFmt = HTMLOutput | LaTeXOutput
445data Opt = Filename String
457 | NoBuiltins -- only for the really primitive stuff!
473 | Port String -- REPL TCP port
481 | PkgMkDoc String -- IdrisDoc
491 | OutputTy OutputType
492 | Extension LanguageExt
493 | InterpretScript String
495 | TargetTriple String
498 | AddOpt Optimisation
499 | RemoveOpt Optimisation
502 | AutoWidth -- ^ Automatically adjust terminal width
503 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
504 | UseConsoleWidth ConsoleWidth
508data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
509 | EEval PTerm | ECheck PTerm | ESearch PTerm
510 | EDocStr (Either Name Const)
513-- Parsed declarations
515data Fixity = Infixl { prec :: Int }
516 | Infixr { prec :: Int }
517 | InfixN { prec :: Int }
518 | PrefixN { prec :: Int }
521deriving instance Binary Fixity
522deriving instance NFData Fixity
525instance Show Fixity where
526 show (Infixl i) = "infixl " ++ show i
527 show (Infixr i) = "infixr " ++ show i
528 show (InfixN i) = "infix " ++ show i
529 show (PrefixN i) = "prefix " ++ show i
531data FixDecl = Fix Fixity String
534instance Show FixDecl where
535 show (Fix f s) = show f ++ " " ++ s
538deriving instance Binary FixDecl
539deriving instance NFData FixDecl
542instance Ord FixDecl where
543 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
546data Static = Static | Dynamic
547 deriving (Show, Eq, Data, Typeable)
549deriving instance Binary Static
550deriving instance NFData Static
553-- Mark bindings with their explicitness, and laziness
554data Plicity = Imp { pargopts :: [ArgOpt],
557 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
559 | Exp { pargopts :: [ArgOpt],
561 pparam :: Bool } -- this is a param (rather than index)
562 | Constraint { pargopts :: [ArgOpt],
564 | TacImp { pargopts :: [ArgOpt],
567 deriving (Show, Eq, Data, Typeable)
570deriving instance Binary Plicity
571deriving instance NFData Plicity
574is_scoped :: Plicity -> Maybe ImplicitInfo
575is_scoped (Imp _ _ _ s) = s
578impl = Imp [] Dynamic False Nothing
579forall_imp = Imp [] Dynamic False (Just (Impl False))
580forall_constraint = Imp [] Dynamic False (Just (Impl True))
581expl = Exp [] Dynamic False
582expl_param = Exp [] Dynamic True
583constraint = Constraint [] Static
584tacimpl t = TacImp [] Dynamic t
586data FnOpt = Inlinable -- always evaluate when simplifying
587 | TotalFn | PartialFn | CoveringFn
588 | Coinductive | AssertTotal
589 | Dictionary -- type class dictionary, eval only when
590 -- a function argument, and further evaluation resutls
591 | Implicit -- implicit coercion
592 | NoImplicit -- do not apply implicit coercions
593 | CExport String -- export, with a C name
594 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
595 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
596 | Reflection -- a reflecting function, compile-time only
597 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
598 | Constructor -- Data constructor type
599 | AutoHint -- use in auto implicit search
600 | PEGenerated -- generated by partial evaluator
603deriving instance Binary FnOpt
604deriving instance NFData FnOpt
609inlinable :: FnOpts -> Bool
610inlinable = elem Inlinable
612dictionary :: FnOpts -> Bool
613dictionary = elem Dictionary
616-- | Type provider - what to provide
617data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
618 | ProvPostulate t -- ^ goal type must be Type, so only term
619 deriving (Show, Eq, Functor)
621type ProvideWhat = ProvideWhat' PTerm
623-- | Top-level declarations such as compiler directives, definitions,
624-- datatypes and typeclasses.
626 = PFix FC Fixity [String] -- ^ Fixity declaration
627 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
628 | PPostulate Bool -- external def if true
629 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
630 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
631 | PCAF FC Name t -- ^ Top level constant
632 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
633 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
634 | PNamespace String FC [PDecl' t]
635 -- ^ New namespace, where FC is accurate location of the
636 -- namespace in the file
637 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
639 FC -- Record name precise location
640 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
641 [(Name, Docstring (Either Err t))] -- Param Docs
642 [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
643 (Maybe (Name, FC)) -- Optional constructor name and location
644 (Docstring (Either Err t)) -- Constructor doc
645 SyntaxInfo -- Constructor SyntaxInfo
646 -- ^ Record declaration
647 | PClass (Docstring (Either Err t)) SyntaxInfo FC
648 [(Name, t)] -- constraints
650 FC -- accurate location of class name
651 [(Name, FC, t)] -- parameters and precise locations
652 [(Name, Docstring (Either Err t))] -- parameter docstrings
653 [(Name, FC)] -- determining parameters and precise locations
654 [PDecl' t] -- declarations
655 (Maybe (Name, FC)) -- instance constructor name and location
656 (Docstring (Either Err t)) -- instance constructor docs
657 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
658 -- class name, class name location, parameters, method declarations, optional constructor name
660 (Docstring (Either Err t)) -- Instance docs
661 [(Name, Docstring (Either Err t))] -- Parameter docs
663 FC [(Name, t)] -- constraints
665 FC -- precise location of class
667 t -- full instance type
668 (Maybe Name) -- explicit name
670 -- ^ Instance declaration: arguments are documentation, syntax info, source
671 -- location, constraints, class name, parameters, full instance
672 -- type, optional explicit name, and definitions
673 | PDSL Name (DSL' t) -- ^ DSL declaration
674 | PSyntax FC Syntax -- ^ Syntax definition
675 | PMutual FC [PDecl' t] -- ^ Mutual block
676 | PDirective Directive -- ^ Compiler directive.
677 | 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.
678 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
679 -- bool is True, lhs and rhs must be convertible
680 | PRunElabDecl FC t [String] -- ^ FC is decl-level, for errors, and
681 -- Strings represent the namespace
684deriving instance Binary PDecl'
685deriving instance NFData PDecl'
688-- | The set of source directives
689data Directive = DLib Codegen String |
690 DLink Codegen String |
691 DFlag Codegen String |
692 DInclude Codegen String |
695 DAccess Accessibility |
698 DDynamicLibs [String] |
699 DNameHint Name FC [(Name, FC)] |
700 DErrorHandlers Name FC Name FC [(Name, FC)] |
701 DLanguage LanguageExt |
704-- | A set of instructions for things that need to happen in IState
705-- after a term elaboration when there's been reflected elaboration.
706data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
707 | RClausesInstrs Name [([Name], Term, Term)]
708 | RAddInstance Name Name
710-- | For elaborator state
711data EState = EState {
712 case_decls :: [(Name, PDecl)],
713 delayed_elab :: [(Int, Elab' EState ())],
714 new_tyDecls :: [RDeclInstructions],
715 highlighting :: [(FC, OutputAnnotation)]
719initEState = EState [] [] [] []
721type ElabD a = Elab' EState a
723highlightSource :: FC -> OutputAnnotation -> ElabD ()
724highlightSource fc annot =
725 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
727-- | One clause of a top-level definition. Term arguments to constructors are:
729-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
731-- 2. The list of extra 'with' patterns
733-- 3. The right-hand side
735-- 4. The where block (PDecl' t)
737data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
738 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
739 | PClauseR FC [t] t [PDecl' t]
740 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
743deriving instance Binary PClause'
744deriving instance NFData PClause'
748data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
749 d_name_fc :: FC, -- ^ The precise location of the type constructor name
750 d_tcon :: t, -- ^ Type constructor
751 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
753 -- ^ Data declaration
754 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
755 -- ^ "Placeholder" for data whose constructors are defined later
758-- | Transform the FCs in a PData and its associated terms. The first
759-- function transforms the general-purpose FCs, and the second transforms
760-- those that are used for semantic source highlighting, so they can be
762mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
763mapPDataFC f g (PDatadecl n nfc tycon ctors) =
764 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
765 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
766 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
767mapPDataFC f g (PLaterdecl n nfc tycon) =
768 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
770deriving instance Binary PData'
771deriving instance NFData PData'
774-- Handy to get a free function for applying PTerm -> PTerm functions
775-- across a program, by deriving Functor
777type PDecl = PDecl' PTerm
778type PData = PData' PTerm
779type PClause = PClause' PTerm
781-- | Transform the FCs in a PTerm. The first function transforms the
782-- general-purpose FCs, and the second transforms those that are used
783-- for semantic source highlighting, so they can be treated specially.
784mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
785mapPDeclFC f g (PFix fc fixity ops) =
786 PFix (f fc) fixity ops
787mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
788 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
789mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
790 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
792mapPDeclFC f g (PClauses fc opts n clauses) =
793 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
794mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
795mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
796 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
797mapPDeclFC f g (PParams fc params decls) =
799 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
800 (map (mapPDeclFC f g) decls)
801mapPDeclFC f g (PNamespace ns fc decls) =
802 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
803mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
804 PRecord doc syn (f fc) opts n (g nfc)
805 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
807 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
808 plic, mapPTermFC f g ty, fdoc))
810 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
813mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
814 PClass doc syn (f fc)
815 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
816 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
817 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
818 (map (mapPDeclFC f g) body)
819 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
821mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn cnfc params instTy instN body) =
822 PInstance doc paramDocs syn (f fc)
823 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
824 cn (g cnfc) (map (mapPTermFC f g) params)
825 (mapPTermFC f g instTy)
827 (map (mapPDeclFC f g) body)
828mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
829mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
831 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
832 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
833mapPDeclFC f g (PMutual fc decls) =
834 PMutual (f fc) (map (mapPDeclFC f g) decls)
835mapPDeclFC f g (PDirective d) =
838 DNameHint n nfc ns ->
839 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
840 DErrorHandlers n nfc n' nfc' ns ->
841 DErrorHandlers n (g nfc) n' (g nfc') $
842 map (\(an, anfc) -> (an, g anfc)) ns
843mapPDeclFC f g (PProvider doc syn fc nfc what n) =
844 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
845mapPDeclFC f g (PTransform fc safe l r) =
846 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
847mapPDeclFC f g (PRunElabDecl fc script ns) =
848 PRunElabDecl (f fc) (mapPTermFC f g script) ns
850-- | Get all the names declared in a declaration
851declared :: PDecl -> [Name]
852declared (PFix _ _ _) = []
853declared (PTy _ _ _ _ _ n fc t) = [n]
854declared (PPostulate _ _ _ _ _ _ n t) = [n]
855declared (PClauses _ _ n _) = [] -- not a declaration
856declared (PCAF _ n _) = [n]
857declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
858 where fstt (_, _, a, _, _, _, _) = a
859declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
860declared (PParams _ _ ds) = concatMap declared ds
861declared (PNamespace _ _ ds) = concatMap declared ds
862declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
863declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
864declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
865declared (PDSL n _) = [n]
866declared (PSyntax _ _) = []
867declared (PMutual _ ds) = concatMap declared ds
868declared (PDirective _) = []
871-- get the names declared, not counting nested parameter blocks
872tldeclared :: PDecl -> [Name]
873tldeclared (PFix _ _ _) = []
874tldeclared (PTy _ _ _ _ _ n _ t) = [n]
875tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
876tldeclared (PClauses _ _ n _) = [] -- not a declaration
877tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
878tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
879 where fstt (_, _, a, _, _, _, _) = a
880tldeclared (PParams _ _ ds) = []
881tldeclared (PMutual _ ds) = concatMap tldeclared ds
882tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
883tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
884tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
887defined :: PDecl -> [Name]
888defined (PFix _ _ _) = []
889defined (PTy _ _ _ _ _ n _ t) = []
890defined (PPostulate _ _ _ _ _ _ n t) = []
891defined (PClauses _ _ n _) = [n] -- not a declaration
892defined (PCAF _ n _) = [n]
893defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
894 where fstt (_, _, a, _, _, _, _) = a
895defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
896defined (PParams _ _ ds) = concatMap defined ds
897defined (PNamespace _ _ ds) = concatMap defined ds
898defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
899defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
900defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
901defined (PDSL n _) = [n]
902defined (PSyntax _ _) = []
903defined (PMutual _ ds) = concatMap defined ds
904defined (PDirective _) = []
907updateN :: [(Name, Name)] -> Name -> Name
908updateN ns n | Just n' <- lookup n ns = n'
911updateNs :: [(Name, Name)] -> PTerm -> PTerm
913updateNs ns t = mapPT updateRef t
914 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
917-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
919-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
920-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
921-- where updateCNs ns (PClause n l ts r ds)
922-- = PClause (updateN ns n) (fmap (updateNs ns) l)
923-- (map (fmap (updateNs ns)) ts)
924-- (fmap (updateNs ns) r)
925-- (map (updateDNs ns) ds)
928data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
930-- | High level language terms
931data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
932 | 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.
933 | PInferRef FC [FC] Name -- ^ A name to be defined later
934 | PPatvar FC Name -- ^ A pattern variable
935 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
936 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
937 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
938 | PTyped PTerm PTerm -- ^ Term with explicit type
939 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
940 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
941 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
942 | PMatchApp FC Name -- ^ Make an application by type matching
943 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
944 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
945 | PTrue FC PunInfo -- ^ Unit type..?
946 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
947 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
948 | 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.
949 | 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.
950 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
951 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
952 | PHidden PTerm -- ^ Irrelevant or hidden pattern
953 | PType FC -- ^ 'Type' type
954 | PUniverse Universe -- ^ Some universe
955 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
956 | PConstant FC Const -- ^ Builtin types
957 | Placeholder -- ^ Underscore
958 | PDoBlock [PDo] -- ^ Do notation
959 | PIdiom FC PTerm -- ^ Idiom brackets
961 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
962 | PProof [PTactic] -- ^ Proof script
963 | PTactics [PTactic] -- ^ As PProof, but no auto solving
964 | PElabError Err -- ^ Error to report on elaboration
965 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
966 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
967 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
968 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
969 | PNoImplicits PTerm -- ^ never run implicit converions on the term
970 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
971 | PUnquote PTerm -- ^ ~Term
972 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
973 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
974 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
975 deriving (Eq, Data, Typeable)
977data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
980 deriving (Eq, Data, Typeable)
982-- | Transform the FCs in a PTerm. The first function transforms the
983-- general-purpose FCs, and the second transforms those that are used
984-- for semantic source highlighting, so they can be treated specially.
985mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
986mapPTermFC f g (PQuote q) = PQuote q
987mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
988mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
989mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
990mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
991mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
992mapPTermFC 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)
993mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
994mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
995mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
996mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
997mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
998mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
999mapPTermFC 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)
1000mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
1001mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1002mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1003mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1004mapPTermFC 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)
1005mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1006mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1007mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1008mapPTermFC f g (PType fc) = PType (f fc)
1009mapPTermFC f g (PUniverse u) = PUniverse u
1010mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1011mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1012mapPTermFC f g Placeholder = Placeholder
1013mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1014 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1015 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1016 mapPDoFC (DoBindP fc t1 t2 alts) =
1017 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1018 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1019 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1020mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1021mapPTermFC f g (PReturn fc) = PReturn (f fc)
1022mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1023mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1024mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1025mapPTermFC f g (PElabError err) = PElabError err
1026mapPTermFC f g PImpossible = PImpossible
1027mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1028mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1029mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1030mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1031mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1032mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1033mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1034mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1035mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
1038dg instance Binary PTerm
1039deriving instance NFData PTerm
1042mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1043mapPT f t = f (mpt t) where
1044 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1045 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1046 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1047 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
1049 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1050 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1051 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1052 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1053 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1054 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1055 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1056 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1057 mpt (PHidden t) = PHidden (mapPT f t)
1058 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1059 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1060 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1061 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1062 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1063 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1064 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1068data PTactic' t = Intro [Name] | Intros | Focus Name
1069 | Refine Name [Bool] | Rewrite t | DoUnify
1076 | LetTac Name t | LetTacTy Name t t
1077 | Exact t | Compute | Trivial | TCInstance
1078 | ProofSearch Bool Bool Int (Maybe Name)
1079 [Name] -- allowed local names
1081 -- ^ the bool is whether to search recursively
1084 | ProofState | ProofTerm | Undo
1085 | Try (PTactic' t) (PTactic' t)
1086 | TSeq (PTactic' t) (PTactic' t)
1087 | ApplyTactic t -- see Language.Reflection module
1091 | GoalType String (PTactic' t)
1094 | TDocStr (Either Name Const)
1097 | TFail [ErrorReportPart]
1100 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1102deriving instance Binary PTactic'
1103deriving instance NFData PTactic'
1105instance Sized a => Sized (PTactic' a) where
1106 size (Intro nms) = 1 + size nms
1108 size (Focus nm) = 1 + size nm
1109 size (Refine nm bs) = 1 + size nm + length bs
1110 size (Rewrite t) = 1 + size t
1111 size (Induction t) = 1 + size t
1112 size (LetTac nm t) = 1 + size nm + size t
1113 size (Exact t) = 1 + size t
1121 size (Try l r) = 1 + size l + size r
1122 size (TSeq l r) = 1 + size l + size r
1123 size (ApplyTactic t) = 1 + size t
1124 size (Reflect t) = 1 + size t
1125 size (Fill t) = 1 + size t
1129 size (TFail ts) = 1 + size ts
1132 size (CaseTac x) = 1 + size x
1133 size (Equiv t) = 1 + size t
1134 size (Claim x y) = 1 + size x + size y
1136 size (MatchRefine x) = 1 + size x
1137 size (LetTacTy x y z) = 1 + size x + size y + size z
1140type PTactic = PTactic' PTerm
1142data PDo' t = DoExp FC t
1143 | DoBind FC Name FC t -- ^ second FC is precise name location
1144 | DoBindP FC t t [(t,t)]
1145 | DoLet FC Name FC t t -- ^ second FC is precise name location
1147 deriving (Eq, Functor, Data, Typeable)
1149deriving instance Binary PDo'
1150deriving instance NFData PDo'
1153instance Sized a => Sized (PDo' a) where
1154 size (DoExp fc t) = 1 + size fc + size t
1155 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1156 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1157 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1158 size (DoLetP fc l r) = 1 + size fc + size l + size r
1160type PDo = PDo' PTerm
1162-- The priority gives a hint as to elaboration order. Best to elaborate
1163-- things early which will help give a more concrete type to other
1164-- variables, e.g. a before (interpTy a).
1166data PArg' t = PImp { priority :: Int,
1167 machine_inf :: Bool, -- true if the machine inferred it
1168 argopts :: [ArgOpt],
1171 | PExp { priority :: Int,
1172 argopts :: [ArgOpt],
1175 | PConstraint { priority :: Int,
1176 argopts :: [ArgOpt],
1179 | PTacImplicit { priority :: Int,
1180 argopts :: [ArgOpt],
1184 deriving (Show, Eq, Functor, Data, Typeable)
1186data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1187 deriving (Show, Eq, Data, Typeable)
1189instance Sized a => Sized (PArg' a) where
1190 size (PImp p _ l nm trm) = 1 + size nm + size trm
1191 size (PExp p l nm trm) = 1 + size nm + size trm
1192 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1193 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1196deriving instance Binary PArg'
1197deriving instance NFData PArg'
1200pimp n t mach = PImp 1 mach [] n t
1201pexp t = PExp 1 [] (sMN 0 "arg") t
1202pconst t = PConstraint 1 [] (sMN 0 "carg") t
1203ptacimp n s t = PTacImplicit 2 [] n s t
1205type PArg = PArg' PTerm
1207-- | Get the highest FC in a term, if one exists
1208highestFC :: PTerm -> Maybe FC
1209highestFC (PQuote _) = Nothing
1210highestFC (PRef fc _ _) = Just fc
1211highestFC (PInferRef fc _ _) = Just fc
1212highestFC (PPatvar fc _) = Just fc
1213highestFC (PLam fc _ _ _ _) = Just fc
1214highestFC (PPi _ _ _ _ _) = Nothing
1215highestFC (PLet fc _ _ _ _ _) = Just fc
1216highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1217highestFC (PApp fc _ _) = Just fc
1218highestFC (PAppBind fc _ _) = Just fc
1219highestFC (PMatchApp fc _) = Just fc
1220highestFC (PCase fc _ _) = Just fc
1221highestFC (PIfThenElse fc _ _ _) = Just fc
1222highestFC (PTrue fc _) = Just fc
1223highestFC (PResolveTC fc) = Just fc
1224highestFC (PRewrite fc _ _ _) = Just fc
1225highestFC (PPair fc _ _ _ _) = Just fc
1226highestFC (PDPair fc _ _ _ _ _) = Just fc
1227highestFC (PAs fc _ _) = Just fc
1228highestFC (PAlternative _ _ args) =
1229 case mapMaybe highestFC args of
1232highestFC (PHidden _) = Nothing
1233highestFC (PType fc) = Just fc
1234highestFC (PUniverse _) = Nothing
1235highestFC (PGoal fc _ _ _) = Just fc
1236highestFC (PConstant fc _) = Just fc
1237highestFC Placeholder = Nothing
1238highestFC (PDoBlock lines) =
1239 case map getDoFC lines of
1243 getDoFC (DoExp fc t) = fc
1244 getDoFC (DoBind fc nm nfc t) = fc
1245 getDoFC (DoBindP fc l r alts) = fc
1246 getDoFC (DoLet fc nm nfc l r) = fc
1247 getDoFC (DoLetP fc l r) = fc
1249highestFC (PIdiom fc _) = Just fc
1250highestFC (PReturn fc) = Just fc
1251highestFC (PMetavar fc _) = Just fc
1252highestFC (PProof _) = Nothing
1253highestFC (PTactics _) = Nothing
1254highestFC (PElabError _) = Nothing
1255highestFC PImpossible = Nothing
1256highestFC (PCoerced tm) = highestFC tm
1257highestFC (PDisamb _ opts) = highestFC opts
1258highestFC (PUnifyLog tm) = highestFC tm
1259highestFC (PNoImplicits tm) = highestFC tm
1260highestFC (PQuasiquote _ _) = Nothing
1261highestFC (PUnquote tm) = highestFC tm
1262highestFC (PQuoteName _ fc) = Just fc
1263highestFC (PRunElab fc _ _) = Just fc
1264highestFC (PConstSugar fc _) = Just fc
1265highestFC (PAppImpl t _) = highestFC t
1269data ClassInfo = CI { instanceCtorName :: Name,
1270 class_methods :: [(Name, (FnOpts, PTerm))],
1271 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1272 class_default_superclasses :: [PDecl],
1273 class_params :: [Name],
1274 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1275 class_determiners :: [Int] }
1278deriving instance Binary ClassInfo
1279deriving instance NFData ClassInfo
1283data RecordInfo = RI { record_parameters :: [(Name,PTerm)],
1284 record_constructor :: Name,
1285 record_projections :: [Name] }
1288-- Type inference data
1290data TIData = TIPartial -- ^ a function with a partially defined type
1291 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1294-- | Miscellaneous information about functions
1295data FnInfo = FnInfo { fn_params :: [Int] }
1298deriving instance Binary FnInfo
1299deriving instance NFData FnInfo
1302data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1303 detaggable :: Bool }
1306deriving instance Binary OptInfo
1307deriving instance NFData OptInfo
1310-- | Syntactic sugar info
1311data DSL' t = DSL { dsl_bind :: t,
1316 index_first :: Maybe t,
1317 index_next :: Maybe t,
1318 dsl_lambda :: Maybe t,
1322 deriving (Show, Functor)
1324deriving instance Binary DSL'
1325deriving instance NFData DSL'
1328type DSL = DSL' PTerm
1330data SynContext = PatternSyntax | TermSyntax | AnySyntax
1333deriving instance Binary SynContext
1334deriving instance NFData SynContext
1337data Syntax = Rule [SSymbol] PTerm SynContext
1338 | DeclRule [SSymbol] [PDecl]
1341syntaxNames :: Syntax -> [Name]
1342syntaxNames (Rule syms _ _) = mapMaybe ename syms
1343 where ename (Keyword n) = Just n
1345syntaxNames (DeclRule syms _) = mapMaybe ename syms
1346 where ename (Keyword n) = Just n
1349syntaxSymbols :: Syntax -> [SSymbol]
1350syntaxSymbols (Rule ss _ _) = ss
1351syntaxSymbols (DeclRule ss _) = ss
1353deriving instance Binary Syntax
1354deriving instance NFData Syntax
1357data SSymbol = Keyword Name
1366deriving instance Binary SSymbol
1367deriving instance NFData SSymbol
1370newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1372emptySyntaxRules :: SyntaxRules
1373emptySyntaxRules = SyntaxRules []
1375updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1376updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1378 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1383 ruleSort (s1:ss1) (s2:ss2) =
1384 case symCompare s1 s2 of
1385 EQ -> ruleSort ss1 ss2
1388 -- Better than creating Ord instance for SSymbol since
1389 -- in general this ordering does not really make sense.
1390 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1391 symCompare (Keyword _) _ = LT
1392 symCompare (Symbol _) (Keyword _) = GT
1393 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1394 symCompare (Symbol _) _ = LT
1395 symCompare (Binding _) (Keyword _) = GT
1396 symCompare (Binding _) (Symbol _) = GT
1397 symCompare (Binding b1) (Binding b2) = compare b1 b2
1398 symCompare (Binding _) _ = LT
1399 symCompare (Expr _) (Keyword _) = GT
1400 symCompare (Expr _) (Symbol _) = GT
1401 symCompare (Expr _) (Binding _) = GT
1402 symCompare (Expr e1) (Expr e2) = compare e1 e2
1403 symCompare (Expr _) _ = LT
1404 symCompare (SimpleExpr _) (Keyword _) = GT
1405 symCompare (SimpleExpr _) (Symbol _) = GT
1406 symCompare (SimpleExpr _) (Binding _) = GT
1407 symCompare (SimpleExpr _) (Expr _) = GT
1408 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1410initDSL = DSL (PRef f [] (sUN ">>="))
1411 (PRef f [] (sUN "return"))
1412 (PRef f [] (sUN "<*>"))
1413 (PRef f [] (sUN "pure"))
1420 where f = fileFC "(builtin)"
1422data Using = UImplicit Name PTerm
1423 | UConstraint Name [Name]
1424 deriving (Show, Eq, Data, Typeable)
1426deriving instance Binary Using
1427deriving instance NFData Using
1430data SyntaxInfo = Syn { using :: [Using],
1431 syn_params :: [(Name, PTerm)],
1432 syn_namespace :: [String],
1434 imp_methods :: [Name], -- class methods. When expanding
1435 -- implicits, these should be expanded even under
1437 decoration :: Name -> Name,
1439 implicitAllowed :: Bool,
1440 maxline :: Maybe Int,
1443 syn_in_quasiquote :: Int }
1446deriving instance NFData SyntaxInfo
1447deriving instance Binary SyntaxInfo
1450defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1452expandNS :: SyntaxInfo -> Name -> Name
1453expandNS syn n@(NS _ _) = n
1454expandNS syn n = case syn_namespace syn of
1459-- For inferring types of things
1461bi = fileFC "builtin"
1463inferTy = sMN 0 "__Infer"
1464inferCon = sMN 0 "__infer"
1465inferDecl = PDatadecl inferTy NoFC
1467 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1468 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1469 (PRef bi [] inferTy)), bi, [])]
1472infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1473infP = P (TCon 6 0) inferTy (TType (UVal 0))
1475getInferTerm, getInferType :: Term -> Term
1476getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1477getInferTerm (App _ (App _ _ _) tm) = tm
1478getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1480getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1481 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1482 toTy (PVar t) = PVTy t
1484getInferType (App _ (App _ _ ty) _) = ty
1488-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1490primNames = [inferTy, inferCon]
1493unitCon = sUN "MkUnit"
1495falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1496 "The empty type, also known as the trivially false proposition." ++
1498 "Use `void` or `absurd` to prove anything if you have a variable " ++
1499 "of type `Void` in scope."
1502pairTy = sNS (sUN "Pair") ["Builtins"]
1503pairCon = sNS (sUN "MkPair") ["Builtins"]
1505upairTy = sNS (sUN "UPair") ["Builtins"]
1506upairCon = sNS (sUN "MkUPair") ["Builtins"]
1510eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1511 "The propositional equality type. A proof that `x` = `y`." ++
1513 "To use such a proof, pattern-match on it, and the two equal things will " ++
1514 "then need to be the _same_ pattern." ++
1516 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1517 "is possible to state equalities between values of potentially different " ++
1518 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1520 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1522eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1523 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1525 [(reflDoc, reflParamDoc,
1526 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1527 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1528 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1529 pimp (n "B") Placeholder False,
1530 pexp (PRef bi [] (n "x")),
1531 pexp (PRef bi [] (n "x"))])), bi, [])]
1533 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1534 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1535 "shown that both sides are in fact equal."
1536 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1537 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1539eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1540 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1546-- | The special name to be used in the module documentation context -
1547-- not for use in the main definition context. The namespace around it
1548-- will determine the module to which the docs adhere.
1550modDocName = sMN 0 "ModuleDocs"
1552-- Defined in builtins.idr
1553sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1554sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1556piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1557piBind = piBindp expl
1559piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1561piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1564-- Pretty-printing declarations and terms
1566-- These "show" instances render to an absurdly wide screen because inserted line breaks
1567-- could interfere with interactive editing, which calls "show".
1569instance Show PTerm where
1570 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1572instance Show PDecl where
1573 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1575instance Show PClause where
1576 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1578instance Show PData where
1579 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1581instance Pretty PTerm OutputAnnotation where
1582 pretty = prettyImp defaultPPOption
1584-- | Colourise annotations according to an Idris state. It ignores the names
1585-- in the annotation, as there's no good way to show extended information on a
1587annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1588annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1589annotationColour ist (AnnConst c) =
1590 let theme = idris_colourTheme ist
1591 in Just $ if constIsType c
1592 then typeColour theme
1593 else dataColour theme
1594annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1595annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1596annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1597annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1598annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1599annotationColour ist (AnnName n _ _ _) =
1600 let ctxt = tt_ctxt ist
1601 theme = idris_colourTheme ist
1603 _ | isDConName n ctxt -> Just $ dataColour theme
1604 _ | isFnName n ctxt -> Just $ functionColour theme
1605 _ | isTConName n ctxt -> Just $ typeColour theme
1606 _ | isPostulateName n ist -> Just $ postulateColour theme
1607 _ | otherwise -> Nothing -- don't colourise unknown names
1608annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1609 where colour BoldText = IdrisColour Nothing True False True False
1610 colour UnderlineText = IdrisColour Nothing True True False False
1611 colour ItalicText = IdrisColour Nothing True False False True
1612annotationColour ist _ = Nothing
1615-- | Colourise annotations according to an Idris state. It ignores the names
1616-- in the annotation, as there's no good way to show extended
1617-- information on a terminal. Note that strings produced this way will
1618-- not be coloured on Windows, so the use of the colour rendering
1619-- functions in Idris.Output is to be preferred.
1620consoleDecorate :: IState -> OutputAnnotation -> String -> String
1621consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1623isPostulateName :: Name -> IState -> Bool
1624isPostulateName n ist = S.member n (idris_postulates ist)
1626-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1627prettyImp :: PPOption -- ^^ pretty printing options
1628 -> PTerm -- ^^ the term to pretty-print
1629 -> Doc OutputAnnotation
1630prettyImp impl = pprintPTerm impl [] [] []
1632-- | Serialise something to base64 using its Binary instance.
1634-- | Do the right thing for rendering a term in an IState
1635prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1636prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1638-- | Pretty-print a high-level Idris term in some bindings context with infix info
1639pprintPTerm :: PPOption -- ^^ pretty printing options
1640 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1641 -> [Name] -- ^^ names to always show in pi, even if not used
1642 -> [FixDecl] -- ^^ Fixity declarations
1643 -> PTerm -- ^^ the term to pretty-print
1644 -> Doc OutputAnnotation
1645pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1650 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1651 prettySe d p bnd (PQuote r) =
1652 text "![" <> pretty r <> text "]"
1653 prettySe d p bnd (PPatvar fc n) = pretty n
1655 | Just str <- slist d p bnd e = depth d $ str
1656 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1657 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1658 prettySe d p bnd (PLam fc n nfc ty sc) =
1659 depth d . bracket p startPrec . group . align . hang 2 $
1660 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1661 prettySe (decD d) startPrec ((n, False):bnd) sc
1662 prettySe d p bnd (PLet fc n nfc ty v sc) =
1663 depth d . bracket p startPrec . group . align $
1664 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1665 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1666 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1667 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1668 || ppopt_pinames ppo && uname n =
1669 depth d . bracket p startPrec . group $
1670 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1671 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1673 depth d . bracket p startPrec . group $
1674 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1675 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1677 uname (UN n) = case str n of
1684 Static -> text "[static]" <> space
1686 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1688 depth d . bracket p startPrec $
1689 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1690 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1691 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1695 Static -> text "[static]" <> space
1697 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1698 depth d . bracket p startPrec $
1699 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1700 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
1701 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1702 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1703 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1704 depth d . bracket p startPrec $
1705 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1706 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1707 -- This case preserves the behavior of the former constructor PEq.
1708 -- It should be removed if feasible when the pretty-printing of infix
1709 -- operators in general is improved.
1710 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1711 | n == eqTy, ppopt_impl ppo =
1712 depth d . bracket p eqPrec $
1713 enclose lparen rparen eq <+>
1714 align (group (vsep (map (prettyArgS (decD d) bnd)
1717 depth d . bracket p eqPrec . align . group $
1718 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1719 where eq = annName eqTy (text "=")
1721 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1722 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1723 | UN nm <- basename f
1724 , not (ppopt_impl ppo) && null (getShowArgs args) =
1725 prettyName True (ppopt_impl ppo) bnd f
1726 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1727 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1728 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1729 | UN nm <- basename op
1731 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1732 case getShowArgs args of
1734 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1735 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1736 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1737 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1738 depth d . bracket p funcAppPrec $
1739 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1740 align (group (vsep (map (prettyArgS d bnd) rest)))
1741 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1742 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1743 f = getFixity (opStr op)
1745 Nothing -> funcAppPrec + 1
1746 Just (Infixl p') -> p'
1747 Just f' -> prec f' + 1
1749 Nothing -> funcAppPrec + 1
1750 Just (Infixr p') -> p'
1751 Just f' -> prec f' + 1
1752 inFix l r = align . group $
1753 (prettySe (decD d) left bnd l <+> opName False) <$>
1754 group (prettySe (decD d) right bnd r)
1755 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1756 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1757 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1758 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1759 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1760 let args = getShowArgs as
1761 fp = prettySe (decD d) (startPrec + 1) bnd f
1762 shownArgs = if ppopt_impl ppo then as else args
1764 depth d . bracket p funcAppPrec . group $
1767 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1768 prettySe d p bnd (PCase _ scr cases) =
1769 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1770 depth d (indent 2 (vsep (map ppcase cases)))
1772 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1773 ([(n, False) | n <- vars l] ++ bnd)
1774 in nest nestingSize $
1775 prettyCase l <+> text "=>" <+> prettyCase r
1776 -- Warning: this is a bit of a hack. At this stage, we don't have the
1777 -- global context, so we can't determine which names are constructors,
1778 -- which are types, and which are pattern variables on the LHS of the
1779 -- case pattern. We use the heuristic that names without a namespace
1780 -- are patvars, because right now case blocks in PTerms are always
1781 -- delaborated from TT before being sent to the pretty-printer. If they
1782 -- start getting printed directly, THIS WILL BREAK.
1783 -- Potential solution: add a list of known patvars to the cases in
1784 -- PCase, and have the delaborator fill it out, kind of like the pun
1785 -- disambiguation on PDPair.
1786 vars tm = filter noNS (allNamesIn tm)
1787 noNS (NS _ _) = False
1790 prettySe d p bnd (PIfThenElse _ c t f) =
1791 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1792 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1793 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1794 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1796 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1797 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1798 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1799 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1800 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1801 prettySe d p bnd (PRewrite _ l r _) =
1802 depth d . bracket p startPrec $
1803 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1804 prettySe d p bnd (PTyped l r) =
1805 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1806 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1807 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1808 align . group . vsep . punctuate (ann comma) $
1809 map (prettySe (decD d) startPrec bnd) elts
1810 where ann = case pun of
1812 IsType -> annName pairTy
1813 IsTerm -> annName pairCon
1814 prettySe d p bnd (PDPair _ _ pun l t r) =
1818 annotated (text "**") <+>
1819 prettySe (decD d) startPrec (addBinding bnd) r <>
1821 where annotated = case pun of
1822 IsType -> annName sigmaTy
1823 IsTerm -> annName sigmaCon
1825 (left, addBinding) = case (l, pun) of
1826 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1827 _ -> (prettySe (decD d) startPrec bnd l, id)
1828 prettySe d p bnd (PAlternative ns a as) =
1829 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1832 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1833 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1834 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1835 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1836 -- XXX: add pretty for tactics
1837 prettySe d p bnd (PProof ts) =
1838 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1839 prettySe d p bnd (PTactics ts) =
1840 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1841 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1842 prettySe d p bnd (PReturn f) = kwd "return"
1843 prettySe d p bnd PImpossible = kwd "impossible"
1844 prettySe d p bnd Placeholder = text "_"
1845 prettySe d p bnd (PDoBlock dos) =
1846 bracket p startPrec $
1847 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1848 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1849 ppdo bnd (DoBind _ bn _ tm : dos) =
1850 (prettyBindingOf bn False <+> text "<-" <+>
1851 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1852 ppdo ((bn, False):bnd) dos
1853 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1854 text "no pretty printer for pattern-matching do binding" :
1856 ppdo bnd (DoLet _ ln _ ty v : dos) =
1857 (kwd "let" <+> prettyBindingOf ln False <+>
1858 (if ty /= Placeholder
1859 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1861 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1862 ppdo ((ln, False):bnd) dos
1863 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1864 text "no pretty printer for pattern-matching do binding" :
1867 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1868 prettySe d p bnd (PElabError s) = pretty s
1869 -- Quasiquote pprinting ignores bound vars
1870 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1871 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1872 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1873 prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1874 prettySe d p bnd (PRunElab _ tm _) =
1875 bracket p funcAppPrec . group . align . hang 2 $
1877 prettySe (decD d) funcAppPrec bnd tm
1878 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1880 prettySe d p bnd _ = text "missing pretty-printer for term"
1882 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1883 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1884 where display (UN n) = T.unpack n
1885 display (MN _ n) = T.unpack n
1886 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1887 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1890 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1891 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1892 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1893 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1895 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1896 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1897 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1898 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1900 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1901 annName n = annotate (AnnName n Nothing Nothing Nothing)
1903 opStr :: Name -> String
1904 opStr (NS n _) = opStr n
1905 opStr (UN n) = T.unpack n
1907 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1908 slist' (Just d) _ _ _ | d <= 0 = Nothing
1910 | containsHole e = Nothing
1911 slist' d p bnd (PApp _ (PRef _ _ nil) _)
1912 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1913 slist' d p bnd (PRef _ _ nil)
1914 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1915 slist' d p bnd (PApp _ (PRef _ _ cons) args)
1916 | nsroot cons == sUN "::",
1917 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1919 Just tl' <- slist' (decD d) p bnd tl
1920 = Just (prettySe d startPrec bnd hd : tl')
1922 isImp (PImp {}) = True
1924 slist' _ _ _ tm = Nothing
1926 slist d p bnd e | Just es <- slist' d p bnd e = Just $
1928 [] -> annotate (AnnData "" "") $ text "[]"
1929 [x] -> enclose left right . group $ x
1930 xs -> enclose left right .
1931 align . group . vsep .
1932 punctuate comma $ xs
1933 where left = (annotate (AnnData "" "") (text "["))
1934 right = (annotate (AnnData "" "") (text "]"))
1935 comma = (annotate (AnnData "" "") (text ","))
1936 slist _ _ _ _ = Nothing
1938 pairElts :: PTerm -> Maybe [PTerm]
1939 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1940 | otherwise = Just [x, y]
1941 pairElts _ = Nothing
1943 natns = "Prelude.Nat."
1945 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1946 snat (Just x) _ _ | x <= 0 = Nothing
1947 snat d p (PRef _ _ z)
1948 | show z == (natns++"Z") || show z == "Z" = Just 0
1949 snat d p (PApp _ s [PExp {getTm=n}])
1950 | show s == (natns++"S") || show s == "S",
1951 Just n' <- snat (decD d) p n
1953 snat _ _ _ = Nothing
1955 bracket outer inner doc
1956 | outer > inner = lparen <> doc <> rparen
1959 ellipsis = text "..."
1962 depth (Just d) = if d <= 0 then const (ellipsis) else id
1964 decD = fmap (\x -> x - 1)
1966 kwd = annotate AnnKeyword . text
1968 fixities :: M.Map String Fixity
1969 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1971 getFixity :: String -> Maybe Fixity
1972 getFixity = flip M.lookup fixities
1974-- | Strip away namespace information
1975basename :: Name -> Name
1976basename (NS n _) = basename n
1979-- | Determine whether a name was the one inserted for a hole or
1980-- guess by the delaborator
1981isHoleName :: Name -> Bool
1982isHoleName (UN n) = n == T.pack "[__]"
1985-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1986containsHole :: PTerm -> Bool
1987containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
1989-- | Pretty-printer helper for names that attaches the correct annotations
1991 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1992 -> Bool -- ^^ whether to show namespaces
1993 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1994 -> Name -- ^^ the name to pprint
1995 -> Doc OutputAnnotation
1996prettyName infixParen showNS bnd n
1997 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1998 | (UN n') <- n, T.unpack n' == "_" = text "_"
1999 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
2000 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
2001 where fullName = text nameSpace <> parenthesise (text (baseName n))
2002 baseName (UN n) = T.unpack n
2003 baseName (NS n ns) = baseName n
2004 baseName (MN i s) = T.unpack s
2005 baseName other = show other
2006 nameSpace = case n of
2007 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2009 isInfix = case baseName n of
2011 (c : _) -> not (isAlpha c)
2012 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2015showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2016showCImp ppo (PClause _ n l ws r w)
2017 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2018 <+> text "where" <+> text (show w)
2021 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2022showCImp ppo (PWith _ n l ws r pn w)
2023 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2024 <+> braces (text (show w))
2027 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2030showDImp :: PPOption -> PData -> Doc OutputAnnotation
2031showDImp ppo (PDatadecl n nfc ty cons)
2032 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2033 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2035showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2036showDecls o ds = vsep (map (showDeclImp o) ds)
2038showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2039showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2040showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2041 indent 2 (vsep (map (showCImp o) cs))
2042showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2043showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2044showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2045showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2046showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2047 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2048showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
2049 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2050showDeclImp _ _ = text "..."
2051-- showDeclImp (PImport o) = "import " ++ o
2053getImps :: [PArg] -> [(Name, PTerm)]
2055getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2056getImps (_ : xs) = getImps xs
2058getExps :: [PArg] -> [PTerm]
2060getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2061getExps (_ : xs) = getExps xs
2063getShowArgs :: [PArg] -> [PArg]
2065getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2066getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2067 | PImp _ _ _ _ tm <- e
2068 , containsHole tm = e : getShowArgs xs
2069getShowArgs (_ : xs) = getShowArgs xs
2071getConsts :: [PArg] -> [PTerm]
2073getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2074getConsts (_ : xs) = getConsts xs
2076getAll :: [PArg] -> [PTerm]
2081showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
2082 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
2083 -> PPOption -- ^^ pretty printing options
2084 -> Bool -- ^^ whether to colourise
2085 -> Name -- ^^ the term to show
2087showName ist bnd ppo colour n = case ist of
2088 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2089 Nothing -> showbasic n
2090 where name = if ppopt_impl ppo then show n else showbasic n
2091 showbasic n@(UN _) = showCG n
2092 showbasic (MN i s) = str s
2093 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2094 showbasic (SN s) = show s
2096 colourise n t = let ctxt' = fmap tt_ctxt ist in
2099 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2100 else colouriseBound t name
2101 | isDConName n ctxt -> colouriseData t name
2102 | isFnName n ctxt -> colouriseFun t name
2103 | isTConName n ctxt -> colouriseType t name
2104 -- The assumption is that if a name is not bound and does not exist in the
2105 -- global context, then we're somewhere in which implicit info has been lost
2106 -- (like error messages). Thus, unknown vars are colourised as implicits.
2107 | otherwise -> colouriseImplicit t name
2109showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
2110 -> PTerm -- ^^ the term to show
2112showTm ist = displayDecorated (consoleDecorate ist) .
2113 renderPretty 0.8 100000 .
2114 prettyImp (ppOptionIst ist)
2116-- | Show a term with implicits, no colours
2117showTmImpls :: PTerm -> String
2118showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2120-- | Show a term with specific options
2121showTmOpts :: PPOption -> PTerm -> String
2122showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2125instance Sized PTerm where
2126 size (PQuote rawTerm) = size rawTerm
2127 size (PRef fc _ name) = size name
2128 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2129 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2130 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2131 size (PTyped trm ty) = 1 + size trm + size ty
2132 size (PApp fc name args) = 1 + size args
2133 size (PAppBind fc name args) = 1 + size args
2134 size (PCase fc trm bdy) = 1 + size trm + size bdy
2135 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2136 size (PTrue fc _) = 1
2137 size (PResolveTC fc) = 1
2138 size (PRewrite fc left right _) = 1 + size left + size right
2139 size (PPair fc _ _ left right) = 1 + size left + size right
2140 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2141 size (PAlternative _ a alts) = 1 + size alts
2142 size (PHidden hidden) = size hidden
2143 size (PUnifyLog tm) = size tm
2144 size (PDisamb _ tm) = size tm
2145 size (PNoImplicits tm) = size tm
2147 size (PUniverse _) = 1
2148 size (PConstant fc const) = 1 + size fc + size const
2149 size Placeholder = 1
2150 size (PDoBlock dos) = 1 + size dos
2151 size (PIdiom fc term) = 1 + size term
2152 size (PReturn fc) = 1
2153 size (PMetavar _ name) = 1
2154 size (PProof tactics) = size tactics
2155 size (PElabError err) = size err
2156 size PImpossible = 1
2159getPArity :: PTerm -> Int
2160getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2163-- Return all names, free or globally bound, in the given term.
2165allNamesIn :: PTerm -> [Name]
2166allNamesIn tm = nub $ ni [] tm
2167 where -- TODO THINK added niTacImp, but is it right?
2169 | not (n `elem` env) = [n]
2170 ni env (PPatvar _ n) = [n]
2171 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2172 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2173 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2174 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
2175 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2176 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2177 ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc
2178 ni env (PHidden tm) = ni env tm
2179 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2180 ni env (PTyped l r) = ni env l ++ ni env r
2181 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2182 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r
2183 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2184 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2185 ni env (PAlternative ns a ls) = concatMap (ni env) ls
2186 ni env (PUnifyLog tm) = ni env tm
2187 ni env (PDisamb _ tm) = ni env tm
2188 ni env (PNoImplicits tm) = ni env tm
2191 niTacImp env (TacImp _ _ scr) = ni env scr
2195-- Return all names defined in binders in the given term
2196boundNamesIn :: PTerm -> [Name]
2197boundNamesIn tm = S.toList (ni S.empty tm)
2198 where -- TODO THINK Added niTacImp, but is it right?
2199 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
2200 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
2201 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
2202 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
2203 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
2204 ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
2205 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
2206 ni set (PRewrite _ l r _) = ni (ni set l) r
2207 ni set (PTyped l r) = ni (ni set l) r
2208 ni set (PPair _ _ _ l r) = ni (ni set l) r
2209 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r
2210 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r
2211 ni set (PAlternative ns a as) = niTms set as
2212 ni set (PHidden tm) = ni set tm
2213 ni set (PUnifyLog tm) = ni set tm
2214 ni set (PDisamb _ tm) = ni set tm
2215 ni set (PNoImplicits tm) = ni set tm
2219 niTms set (x : xs) = niTms (ni set x) xs
2221 niTacImp set (TacImp _ _ scr) = ni set scr
2222 niTacImp set _ = set
2224-- Return names which are valid implicits in the given term (type).
2225implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2226implicitNamesIn uvars ist tm = nub $ ni [] tm
2229 | not (n `elem` env)
2230 = case lookupTy n (tt_ctxt ist) of
2232 _ -> if n `elem` uvars then [n] else []
2233 ni env (PApp _ f@(PRef _ _ n) as)
2234 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
2235 | otherwise = concatMap (ni env) (map getTm as)
2236 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2237 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2238 ni env (PCase _ c os) = ni env c ++
2239 -- names in 'os', not counting the names bound in the cases
2240 (nub (concatMap (ni env) (map snd os))
2241 \\ nub (concatMap (ni env) (map fst os)))
2242 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2243 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2244 ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
2245 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2246 ni env (PTyped l r) = ni env l ++ ni env r
2247 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2248 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2249 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2250 ni env (PAlternative ns a as) = concatMap (ni env) as
2251 ni env (PHidden tm) = ni env tm
2252 ni env (PUnifyLog tm) = ni env tm
2253 ni env (PDisamb _ tm) = ni env tm
2254 ni env (PNoImplicits tm) = ni env tm
2257-- Return names which are free in the given term.
2258namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2259namesIn uvars ist tm = nub $ ni [] tm
2262 | not (n `elem` env)
2263 = case lookupTy n (tt_ctxt ist) of
2265 _ -> if n `elem` (map fst uvars) then [n] else []
2266 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2267 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2268 ni env (PCase _ c os) = ni env c ++
2269 -- names in 'os', not counting the names bound in the cases
2270 (nub (concatMap (ni env) (map snd os))
2271 \\ nub (concatMap (ni env) (map fst os)))
2272 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2273 ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2274 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2275 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2276 ni env (PTyped l r) = ni env l ++ ni env r
2277 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2278 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2279 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2280 ni env (PAlternative ns a as) = concatMap (ni env) as
2281 ni env (PHidden tm) = ni env tm
2282 ni env (PUnifyLog tm) = ni env tm
2283 ni env (PDisamb _ tm) = ni env tm
2284 ni env (PNoImplicits tm) = ni env tm
2287 niTacImp env (TacImp _ _ scr) = ni env scr
2290-- Return which of the given names are used in the given term.
2292usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2293usedNamesIn vars ist tm = nub $ ni [] tm
2294 where -- TODO THINK added niTacImp, but is it right?
2296 | n `elem` vars && not (n `elem` env)
2297 = case lookupDefExact n (tt_ctxt ist) of
2300 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2301 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2302 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2303 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2304 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2305 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2306 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2307 ni env (PTyped l r) = ni env l ++ ni env r
2308 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2309 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2310 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2311 ni env (PAlternative ns a as) = concatMap (ni env) as
2312 ni env (PHidden tm) = ni env tm
2313 ni env (PUnifyLog tm) = ni env tm
2314 ni env (PDisamb _ tm) = ni env tm
2315 ni env (PNoImplicits tm) = ni env tm
2318 niTacImp env (TacImp _ _ scr) = ni env scr
2321-- Return the list of inaccessible (= dotted) positions for a name.
2322getErasureInfo :: IState -> Name -> [Int]
2323getErasureInfo ist n =
2324 case lookupCtxtExact n (idris_optimisation ist) of
2325 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