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_dsls :: Ctxt DSL,
181 idris_optimisation :: Ctxt OptInfo,
182 idris_datatypes :: Ctxt TypeInfo,
183 idris_namehints :: Ctxt [Name],
184 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
185 -- ^ list of lhs/rhs, and a list of missing clauses
186 idris_flags :: Ctxt [FnOpt],
187 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
188 idris_calledgraph :: Ctxt [Name],
189 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
190 idris_moduledocs :: Ctxt (Docstring DocTerm),
191 -- ^ module documentation is saved in a special MN so the context
192 -- mechanism can be used for disambiguation
193 idris_tyinfodata :: Ctxt TIData,
194 idris_fninfo :: Ctxt FnInfo,
195 idris_transforms :: Ctxt [(Term, Term)],
196 idris_autohints :: Ctxt [Name],
197 idris_totcheck :: [(FC, Name)], -- names to check totality on
198 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
199 idris_totcheckfail :: [(FC, String)],
200 idris_options :: IOption,
202 idris_lineapps :: [((FilePath, Int), PTerm)],
203 -- ^ Full application LHS on source line
204 idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],
205 -- ^ The currently defined but not proven metavariables. The Int
206 -- is the number of vars to display as a context, the Maybe Name
207 -- is its top-level function, the [Name] is the list of local variables
208 -- available for proof search and the Bool is whether :p is
210 idris_coercions :: [Name],
211 idris_errRev :: [(Term, Term)],
212 syntax_rules :: SyntaxRules,
213 syntax_keywords :: [String],
214 imported :: [FilePath], -- ^ The imported modules
215 idris_scprims :: [(Name, (Int, PrimFn))],
216 idris_objs :: [(Codegen, FilePath)],
217 idris_libs :: [(Codegen, String)],
218 idris_cgflags :: [(Codegen, String)],
219 idris_hdrs :: [(Codegen, String)],
220 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
221 proof_list :: [(Name, (Bool, [String]))],
223 parserWarnings :: [(FC, Err)],
224 lastParse :: Maybe Name,
225 indent_stack :: [Int],
226 brace_stack :: [Maybe Int],
227 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
228 idris_parsedSpan :: Maybe FC,
229 hide_list :: [(Name, Maybe Accessibility)],
230 default_access :: Accessibility,
231 default_total :: Bool,
232 ibc_write :: [IBCWrite],
233 compiled_so :: Maybe String,
234 idris_dynamic_libs :: [DynamicLib],
235 idris_language_extensions :: [LanguageExt],
236 idris_outputmode :: OutputMode,
237 idris_colourRepl :: Bool,
238 idris_colourTheme :: ColourTheme,
239 idris_errorhandlers :: [Name], -- ^ Global error handlers
240 idris_nameIdx :: (Int, Ctxt (Int, Name)),
241 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
242 module_aliases :: M.Map [T.Text] [T.Text],
243 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
244 idris_postulates :: S.Set Name,
245 idris_externs :: S.Set (Name, Int),
246 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
247 idris_whocalls :: Maybe (M.Map Name [Name]),
248 idris_callswho :: Maybe (M.Map Name [Name]),
249 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
250 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
251 -- (instances appear twice; also as a funtion name)
252 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
253 idris_exports :: [Name], -- ^ Functions with ExportList
254 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
255 idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
258-- Required for parsers library, and therefore trifecta
259instance Show IState where
260 show = const "{internal state}"
262data SizeChange = Smaller | Same | Bigger | Unknown
265deriving instance Binary SizeChange
266deriving instance NFData SizeChange
269type SCGEntry = (Name, [Maybe (Int, SizeChange)])
270type UsageReason = (Name, Int) -- fn_name, its_arg_number
272data CGInfo = CGInfo { argsdef :: [Name],
273 calls :: [(Name, [[Name]])],
276 usedpos :: [(Int, [UsageReason])] }
279deriving instance Binary CGInfo
280deriving instance NFData CGInfo
283primDefs = [sUN "unsafePerformPrimIO",
284 sUN "mkLazyForeignPrim",
288-- information that needs writing for the current module's .ibc file
289data IBCWrite = IBCFix FixDecl
293 | IBCInstance Bool Bool Name Name
300 | IBCImport (Bool, FilePath) -- True = import public
301 | IBCImportDir FilePath
302 | IBCObj Codegen FilePath
303 | IBCLib Codegen String
304 | IBCCGFlag Codegen String
306 | IBCHeader Codegen String
307 | IBCAccess Name Accessibility
308 | IBCMetaInformation Name MetaInformation
309 | IBCTotal Name Totality
310 | IBCFlags Name [FnOpt]
311 | IBCFnInfo Name FnInfo
312 | IBCTrans Name (Term, Term)
313 | IBCErrRev (Term, Term)
317 | IBCDef Name -- i.e. main context
318 | IBCNameHint (Name, Name)
319 | IBCLineApp FilePath Int PTerm
320 | IBCErrorHandler Name
321 | IBCFunctionErrorHandler Name Name Name
323 | IBCExtern (Name, Int)
324 | IBCTotCheckErr FC String
326 | IBCModDocs Name -- ^ The name is the special name used to track module docs
327 | IBCUsage (Name, Int)
329 | IBCAutoHint Name Name
332-- | The initial state for the compiler
334idrisInit = IState initContext S.empty []
335 emptyContext emptyContext emptyContext emptyContext
336 emptyContext emptyContext emptyContext emptyContext
337 emptyContext emptyContext emptyContext emptyContext
338 emptyContext emptyContext emptyContext emptyContext
340 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
341 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
342 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
343 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
345-- | The monad for the main REPL - reading and processing files and updating
346-- global state (hence the IO inner monad).
347--type Idris = WriterT [Either String (IO ())] (State IState a))
348type Idris = StateT IState (ExceptT Err IO)
350catchError :: Idris a -> (Err -> Idris a) -> Idris a
351catchError = liftCatch catchE
353throwError :: Err -> Idris a
354throwError = Trans.lift . throwE
356-- Commands in the REPL
358data Codegen = Via String
367deriving instance NFData Codegen
370data HowMuchDocs = FullDocs | OverviewDocs
376 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
380 | DocStr (Either Name Const) HowMuchDocs
383 | Load FilePath (Maybe Int) -- up to maximum line number
384 | ChangeDirectory FilePath
387 | Compile Codegen String
391 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
392 | AddProof (Maybe Name)
403 | DynamicLink FilePath
406 | Search [String] PTerm
407 | CaseSplitAt Bool Int Name
408 | AddClauseFrom Bool Int Name
409 | AddProofClauseFrom Bool Int Name
410 | AddMissing Bool Int Name
411 | MakeWith Bool Int Name
412 | MakeCase Bool Int Name
413 | MakeLemma Bool Int Name
414 | DoProofSearch Bool -- update file
415 Bool -- recursive search
417 Name -- top level name
422 | SetColour ColourType IdrisColour
426 | SetConsoleWidth ConsoleWidth
427 | SetPrinterDepth (Maybe Int)
428 | Apropos [String] String
432 | MakeDoc String -- IdrisDoc
435 | PPrint OutputFmt Int PTerm
437 -- Debugging commands
439 | DebugUnify PTerm PTerm
441data OutputFmt = HTMLOutput | LaTeXOutput
443data Opt = Filename String
455 | NoBuiltins -- only for the really primitive stuff!
471 | Port String -- REPL TCP port
479 | PkgMkDoc String -- IdrisDoc
489 | OutputTy OutputType
490 | Extension LanguageExt
491 | InterpretScript String
493 | TargetTriple String
496 | AddOpt Optimisation
497 | RemoveOpt Optimisation
500 | AutoWidth -- ^ Automatically adjust terminal width
501 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
502 | UseConsoleWidth ConsoleWidth
506data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
507 | EEval PTerm | ECheck PTerm | ESearch PTerm
508 | EDocStr (Either Name Const)
511-- Parsed declarations
513data Fixity = Infixl { prec :: Int }
514 | Infixr { prec :: Int }
515 | InfixN { prec :: Int }
516 | PrefixN { prec :: Int }
519deriving instance Binary Fixity
520deriving instance NFData Fixity
523instance Show Fixity where
524 show (Infixl i) = "infixl " ++ show i
525 show (Infixr i) = "infixr " ++ show i
526 show (InfixN i) = "infix " ++ show i
527 show (PrefixN i) = "prefix " ++ show i
529data FixDecl = Fix Fixity String
532instance Show FixDecl where
533 show (Fix f s) = show f ++ " " ++ s
536deriving instance Binary FixDecl
537deriving instance NFData FixDecl
540instance Ord FixDecl where
541 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
544data Static = Static | Dynamic
545 deriving (Show, Eq, Data, Typeable)
547deriving instance Binary Static
548deriving instance NFData Static
551-- Mark bindings with their explicitness, and laziness
552data Plicity = Imp { pargopts :: [ArgOpt],
555 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
557 | Exp { pargopts :: [ArgOpt],
559 pparam :: Bool } -- this is a param (rather than index)
560 | Constraint { pargopts :: [ArgOpt],
562 | TacImp { pargopts :: [ArgOpt],
565 deriving (Show, Eq, Data, Typeable)
568deriving instance Binary Plicity
569deriving instance NFData Plicity
572is_scoped :: Plicity -> Maybe ImplicitInfo
573is_scoped (Imp _ _ _ s) = s
576impl = Imp [] Dynamic False Nothing
577forall_imp = Imp [] Dynamic False (Just (Impl False))
578forall_constraint = Imp [] Dynamic False (Just (Impl True))
579expl = Exp [] Dynamic False
580expl_param = Exp [] Dynamic True
581constraint = Constraint [] Static
582tacimpl t = TacImp [] Dynamic t
584data FnOpt = Inlinable -- always evaluate when simplifying
585 | TotalFn | PartialFn | CoveringFn
586 | Coinductive | AssertTotal
587 | Dictionary -- type class dictionary, eval only when
588 -- a function argument, and further evaluation resutls
589 | Implicit -- implicit coercion
590 | NoImplicit -- do not apply implicit coercions
591 | CExport String -- export, with a C name
592 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
593 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
594 | Reflection -- a reflecting function, compile-time only
595 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
596 | Constructor -- Data constructor type
597 | AutoHint -- use in auto implicit search
598 | PEGenerated -- generated by partial evaluator
601deriving instance Binary FnOpt
602deriving instance NFData FnOpt
607inlinable :: FnOpts -> Bool
608inlinable = elem Inlinable
610dictionary :: FnOpts -> Bool
611dictionary = elem Dictionary
614-- | Type provider - what to provide
615data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
616 | ProvPostulate t -- ^ goal type must be Type, so only term
617 deriving (Show, Eq, Functor)
619type ProvideWhat = ProvideWhat' PTerm
621-- | Top-level declarations such as compiler directives, definitions,
622-- datatypes and typeclasses.
624 = PFix FC Fixity [String] -- ^ Fixity declaration
625 | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
626 | PPostulate Bool -- external def if true
627 (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
628 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
629 | PCAF FC Name t -- ^ Top level constant
630 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
631 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
632 | PNamespace String FC [PDecl' t]
633 -- ^ New namespace, where FC is accurate location of the
634 -- namespace in the file
635 | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts
637 FC -- Record name precise location
638 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
639 [(Name, Docstring (Either Err t))] -- Param Docs
640 [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err t)))] -- Fields
641 (Maybe (Name, FC)) -- Optional constructor name and location
642 (Docstring (Either Err t)) -- Constructor doc
643 SyntaxInfo -- Constructor SyntaxInfo
644 -- ^ Record declaration
645 | PClass (Docstring (Either Err t)) SyntaxInfo FC
646 [(Name, t)] -- constraints
648 FC -- accurate location of class name
649 [(Name, FC, t)] -- parameters and precise locations
650 [(Name, Docstring (Either Err t))] -- parameter docstrings
651 [(Name, FC)] -- determining parameters and precise locations
652 [PDecl' t] -- declarations
653 (Maybe (Name, FC)) -- instance constructor name and location
654 (Docstring (Either Err t)) -- instance constructor docs
655 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
656 -- class name, class name location, parameters, method declarations, optional constructor name
658 (Docstring (Either Err t)) -- Instance docs
659 [(Name, Docstring (Either Err t))] -- Parameter docs
661 FC [(Name, t)] -- constraints
663 FC -- precise location of class
665 t -- full instance type
666 (Maybe Name) -- explicit name
668 -- ^ Instance declaration: arguments are documentation, syntax info, source
669 -- location, constraints, class name, parameters, full instance
670 -- type, optional explicit name, and definitions
671 | PDSL Name (DSL' t) -- ^ DSL declaration
672 | PSyntax FC Syntax -- ^ Syntax definition
673 | PMutual FC [PDecl' t] -- ^ Mutual block
674 | PDirective Directive -- ^ Compiler directive.
675 | 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.
676 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
677 -- bool is True, lhs and rhs must be convertible
678 | PRunElabDecl FC t [String] -- ^ FC is decl-level, for errors, and
679 -- Strings represent the namespace
682deriving instance Binary PDecl'
683deriving instance NFData PDecl'
686-- | The set of source directives
687data Directive = DLib Codegen String |
688 DLink Codegen String |
689 DFlag Codegen String |
690 DInclude Codegen String |
693 DAccess Accessibility |
696 DDynamicLibs [String] |
697 DNameHint Name FC [(Name, FC)] |
698 DErrorHandlers Name FC Name FC [(Name, FC)] |
699 DLanguage LanguageExt |
702-- | A set of instructions for things that need to happen in IState
703-- after a term elaboration when there's been reflected elaboration.
704data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
705 | RClausesInstrs Name [([Name], Term, Term)]
706 | RAddInstance Name Name
708-- | For elaborator state
709data EState = EState {
710 case_decls :: [(Name, PDecl)],
711 delayed_elab :: [(Int, Elab' EState ())],
712 new_tyDecls :: [RDeclInstructions],
713 highlighting :: [(FC, OutputAnnotation)]
717initEState = EState [] [] [] []
719type ElabD a = Elab' EState a
721highlightSource :: FC -> OutputAnnotation -> ElabD ()
722highlightSource fc annot =
723 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
725-- | One clause of a top-level definition. Term arguments to constructors are:
727-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
729-- 2. The list of extra 'with' patterns
731-- 3. The right-hand side
733-- 4. The where block (PDecl' t)
735data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
736 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
737 | PClauseR FC [t] t [PDecl' t]
738 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
741deriving instance Binary PClause'
742deriving instance NFData PClause'
746data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
747 d_name_fc :: FC, -- ^ The precise location of the type constructor name
748 d_tcon :: t, -- ^ Type constructor
749 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
751 -- ^ Data declaration
752 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
753 -- ^ "Placeholder" for data whose constructors are defined later
756-- | Transform the FCs in a PData and its associated terms. The first
757-- function transforms the general-purpose FCs, and the second transforms
758-- those that are used for semantic source highlighting, so they can be
760mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
761mapPDataFC f g (PDatadecl n nfc tycon ctors) =
762 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
763 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
764 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
765mapPDataFC f g (PLaterdecl n nfc tycon) =
766 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
768deriving instance Binary PData'
769deriving instance NFData PData'
772-- Handy to get a free function for applying PTerm -> PTerm functions
773-- across a program, by deriving Functor
775type PDecl = PDecl' PTerm
776type PData = PData' PTerm
777type PClause = PClause' PTerm
779-- | Transform the FCs in a PTerm. The first function transforms the
780-- general-purpose FCs, and the second transforms those that are used
781-- for semantic source highlighting, so they can be treated specially.
782mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
783mapPDeclFC f g (PFix fc fixity ops) =
784 PFix (f fc) fixity ops
785mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
786 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
787mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
788 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
790mapPDeclFC f g (PClauses fc opts n clauses) =
791 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
792mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
793mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
794 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
795mapPDeclFC f g (PParams fc params decls) =
797 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
798 (map (mapPDeclFC f g) decls)
799mapPDeclFC f g (PNamespace ns fc decls) =
800 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
801mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
802 PRecord doc syn (f fc) opts n (g nfc)
803 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
805 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
806 plic, mapPTermFC f g ty, fdoc))
808 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
811mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
812 PClass doc syn (f fc)
813 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
814 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
815 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
816 (map (mapPDeclFC f g) body)
817 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
819mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn cnfc params instTy instN body) =
820 PInstance doc paramDocs syn (f fc)
821 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
822 cn (g cnfc) (map (mapPTermFC f g) params)
823 (mapPTermFC f g instTy)
825 (map (mapPDeclFC f g) body)
826mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
827mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
829 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
830 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
831mapPDeclFC f g (PMutual fc decls) =
832 PMutual (f fc) (map (mapPDeclFC f g) decls)
833mapPDeclFC f g (PDirective d) =
836 DNameHint n nfc ns ->
837 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
838 DErrorHandlers n nfc n' nfc' ns ->
839 DErrorHandlers n (g nfc) n' (g nfc') $
840 map (\(an, anfc) -> (an, g anfc)) ns
841mapPDeclFC f g (PProvider doc syn fc nfc what n) =
842 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
843mapPDeclFC f g (PTransform fc safe l r) =
844 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
845mapPDeclFC f g (PRunElabDecl fc script ns) =
846 PRunElabDecl (f fc) (mapPTermFC f g script) ns
848-- | Get all the names declared in a declaration
849declared :: PDecl -> [Name]
850declared (PFix _ _ _) = []
851declared (PTy _ _ _ _ _ n fc t) = [n]
852declared (PPostulate _ _ _ _ _ _ n t) = [n]
853declared (PClauses _ _ n _) = [] -- not a declaration
854declared (PCAF _ n _) = [n]
855declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
856 where fstt (_, _, a, _, _, _, _) = a
857declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
858declared (PParams _ _ ds) = concatMap declared ds
859declared (PNamespace _ _ ds) = concatMap declared ds
860declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
861declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
862declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
863declared (PDSL n _) = [n]
864declared (PSyntax _ _) = []
865declared (PMutual _ ds) = concatMap declared ds
866declared (PDirective _) = []
869-- get the names declared, not counting nested parameter blocks
870tldeclared :: PDecl -> [Name]
871tldeclared (PFix _ _ _) = []
872tldeclared (PTy _ _ _ _ _ n _ t) = [n]
873tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
874tldeclared (PClauses _ _ n _) = [] -- not a declaration
875tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
876tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
877 where fstt (_, _, a, _, _, _, _) = a
878tldeclared (PParams _ _ ds) = []
879tldeclared (PMutual _ ds) = concatMap tldeclared ds
880tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
881tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
882tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
885defined :: PDecl -> [Name]
886defined (PFix _ _ _) = []
887defined (PTy _ _ _ _ _ n _ t) = []
888defined (PPostulate _ _ _ _ _ _ n t) = []
889defined (PClauses _ _ n _) = [n] -- not a declaration
890defined (PCAF _ n _) = [n]
891defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
892 where fstt (_, _, a, _, _, _, _) = a
893defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
894defined (PParams _ _ ds) = concatMap defined ds
895defined (PNamespace _ _ ds) = concatMap defined ds
896defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
897defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
898defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
899defined (PDSL n _) = [n]
900defined (PSyntax _ _) = []
901defined (PMutual _ ds) = concatMap defined ds
902defined (PDirective _) = []
905updateN :: [(Name, Name)] -> Name -> Name
906updateN ns n | Just n' <- lookup n ns = n'
909updateNs :: [(Name, Name)] -> PTerm -> PTerm
911updateNs ns t = mapPT updateRef t
912 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
915-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
917-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
918-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
919-- where updateCNs ns (PClause n l ts r ds)
920-- = PClause (updateN ns n) (fmap (updateNs ns) l)
921-- (map (fmap (updateNs ns)) ts)
922-- (fmap (updateNs ns) r)
923-- (map (updateDNs ns) ds)
926data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
928-- | High level language terms
929data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
930 | 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.
931 | PInferRef FC [FC] Name -- ^ A name to be defined later
932 | PPatvar FC Name -- ^ A pattern variable
933 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
934 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
935 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
936 | PTyped PTerm PTerm -- ^ Term with explicit type
937 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
938 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
939 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
940 | PMatchApp FC Name -- ^ Make an application by type matching
941 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
942 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
943 | PTrue FC PunInfo -- ^ Unit type..?
944 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
945 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
946 | 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.
947 | 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.
948 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
949 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
950 | PHidden PTerm -- ^ Irrelevant or hidden pattern
951 | PType FC -- ^ 'Type' type
952 | PUniverse Universe -- ^ Some universe
953 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
954 | PConstant FC Const -- ^ Builtin types
955 | Placeholder -- ^ Underscore
956 | PDoBlock [PDo] -- ^ Do notation
957 | PIdiom FC PTerm -- ^ Idiom brackets
959 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
960 | PProof [PTactic] -- ^ Proof script
961 | PTactics [PTactic] -- ^ As PProof, but no auto solving
962 | PElabError Err -- ^ Error to report on elaboration
963 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
964 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
965 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
966 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
967 | PNoImplicits PTerm -- ^ never run implicit converions on the term
968 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
969 | PUnquote PTerm -- ^ ~Term
970 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
971 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
972 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
973 deriving (Eq, Data, Typeable)
975data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
978 deriving (Eq, Data, Typeable)
980-- | Transform the FCs in a PTerm. The first function transforms the
981-- general-purpose FCs, and the second transforms those that are used
982-- for semantic source highlighting, so they can be treated specially.
983mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
984mapPTermFC f g (PQuote q) = PQuote q
985mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
986mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
987mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
988mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
989mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
990mapPTermFC 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)
991mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
992mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
993mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
994mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
995mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
996mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
997mapPTermFC 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)
998mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
999mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
1000mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1001mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1002mapPTermFC 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)
1003mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1004mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1005mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1006mapPTermFC f g (PType fc) = PType (f fc)
1007mapPTermFC f g (PUniverse u) = PUniverse u
1008mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1009mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1010mapPTermFC f g Placeholder = Placeholder
1011mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1012 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1013 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1014 mapPDoFC (DoBindP fc t1 t2 alts) =
1015 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1016 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1017 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1018mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1019mapPTermFC f g (PReturn fc) = PReturn (f fc)
1020mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1021mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1022mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1023mapPTermFC f g (PElabError err) = PElabError err
1024mapPTermFC f g PImpossible = PImpossible
1025mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1026mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1027mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1028mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1029mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1030mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1031mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1032mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1033mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
1036dg instance Binary PTerm
1037deriving instance NFData PTerm
1040mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1041mapPT f t = f (mpt t) where
1042 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1043 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1044 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1045 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
1047 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1048 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1049 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1050 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1051 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1052 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1053 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1054 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1055 mpt (PHidden t) = PHidden (mapPT f t)
1056 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1057 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1058 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1059 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1060 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1061 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1062 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1066data PTactic' t = Intro [Name] | Intros | Focus Name
1067 | Refine Name [Bool] | Rewrite t | DoUnify
1074 | LetTac Name t | LetTacTy Name t t
1075 | Exact t | Compute | Trivial | TCInstance
1076 | ProofSearch Bool Bool Int (Maybe Name)
1077 [Name] -- allowed local names
1079 -- ^ the bool is whether to search recursively
1082 | ProofState | ProofTerm | Undo
1083 | Try (PTactic' t) (PTactic' t)
1084 | TSeq (PTactic' t) (PTactic' t)
1085 | ApplyTactic t -- see Language.Reflection module
1089 | GoalType String (PTactic' t)
1092 | TDocStr (Either Name Const)
1095 | TFail [ErrorReportPart]
1098 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1100deriving instance Binary PTactic'
1101deriving instance NFData PTactic'
1103instance Sized a => Sized (PTactic' a) where
1104 size (Intro nms) = 1 + size nms
1106 size (Focus nm) = 1 + size nm
1107 size (Refine nm bs) = 1 + size nm + length bs
1108 size (Rewrite t) = 1 + size t
1109 size (Induction t) = 1 + size t
1110 size (LetTac nm t) = 1 + size nm + size t
1111 size (Exact t) = 1 + size t
1119 size (Try l r) = 1 + size l + size r
1120 size (TSeq l r) = 1 + size l + size r
1121 size (ApplyTactic t) = 1 + size t
1122 size (Reflect t) = 1 + size t
1123 size (Fill t) = 1 + size t
1127 size (TFail ts) = 1 + size ts
1130 size (CaseTac x) = 1 + size x
1131 size (Equiv t) = 1 + size t
1132 size (Claim x y) = 1 + size x + size y
1134 size (MatchRefine x) = 1 + size x
1135 size (LetTacTy x y z) = 1 + size x + size y + size z
1138type PTactic = PTactic' PTerm
1140data PDo' t = DoExp FC t
1141 | DoBind FC Name FC t -- ^ second FC is precise name location
1142 | DoBindP FC t t [(t,t)]
1143 | DoLet FC Name FC t t -- ^ second FC is precise name location
1145 deriving (Eq, Functor, Data, Typeable)
1147deriving instance Binary PDo'
1148deriving instance NFData PDo'
1151instance Sized a => Sized (PDo' a) where
1152 size (DoExp fc t) = 1 + size fc + size t
1153 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1154 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1155 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1156 size (DoLetP fc l r) = 1 + size fc + size l + size r
1158type PDo = PDo' PTerm
1160-- The priority gives a hint as to elaboration order. Best to elaborate
1161-- things early which will help give a more concrete type to other
1162-- variables, e.g. a before (interpTy a).
1164data PArg' t = PImp { priority :: Int,
1165 machine_inf :: Bool, -- true if the machine inferred it
1166 argopts :: [ArgOpt],
1169 | PExp { priority :: Int,
1170 argopts :: [ArgOpt],
1173 | PConstraint { priority :: Int,
1174 argopts :: [ArgOpt],
1177 | PTacImplicit { priority :: Int,
1178 argopts :: [ArgOpt],
1182 deriving (Show, Eq, Functor, Data, Typeable)
1184data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1185 deriving (Show, Eq, Data, Typeable)
1187instance Sized a => Sized (PArg' a) where
1188 size (PImp p _ l nm trm) = 1 + size nm + size trm
1189 size (PExp p l nm trm) = 1 + size nm + size trm
1190 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1191 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1194deriving instance Binary PArg'
1195deriving instance NFData PArg'
1198pimp n t mach = PImp 1 mach [] n t
1199pexp t = PExp 1 [] (sMN 0 "arg") t
1200pconst t = PConstraint 1 [] (sMN 0 "carg") t
1201ptacimp n s t = PTacImplicit 2 [] n s t
1203type PArg = PArg' PTerm
1205-- | Get the highest FC in a term, if one exists
1206highestFC :: PTerm -> Maybe FC
1207highestFC (PQuote _) = Nothing
1208highestFC (PRef fc _ _) = Just fc
1209highestFC (PInferRef fc _ _) = Just fc
1210highestFC (PPatvar fc _) = Just fc
1211highestFC (PLam fc _ _ _ _) = Just fc
1212highestFC (PPi _ _ _ _ _) = Nothing
1213highestFC (PLet fc _ _ _ _ _) = Just fc
1214highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1215highestFC (PApp fc _ _) = Just fc
1216highestFC (PAppBind fc _ _) = Just fc
1217highestFC (PMatchApp fc _) = Just fc
1218highestFC (PCase fc _ _) = Just fc
1219highestFC (PIfThenElse fc _ _ _) = Just fc
1220highestFC (PTrue fc _) = Just fc
1221highestFC (PResolveTC fc) = Just fc
1222highestFC (PRewrite fc _ _ _) = Just fc
1223highestFC (PPair fc _ _ _ _) = Just fc
1224highestFC (PDPair fc _ _ _ _ _) = Just fc
1225highestFC (PAs fc _ _) = Just fc
1226highestFC (PAlternative _ _ args) =
1227 case mapMaybe highestFC args of
1230highestFC (PHidden _) = Nothing
1231highestFC (PType fc) = Just fc
1232highestFC (PUniverse _) = Nothing
1233highestFC (PGoal fc _ _ _) = Just fc
1234highestFC (PConstant fc _) = Just fc
1235highestFC Placeholder = Nothing
1236highestFC (PDoBlock lines) =
1237 case map getDoFC lines of
1241 getDoFC (DoExp fc t) = fc
1242 getDoFC (DoBind fc nm nfc t) = fc
1243 getDoFC (DoBindP fc l r alts) = fc
1244 getDoFC (DoLet fc nm nfc l r) = fc
1245 getDoFC (DoLetP fc l r) = fc
1247highestFC (PIdiom fc _) = Just fc
1248highestFC (PReturn fc) = Just fc
1249highestFC (PMetavar fc _) = Just fc
1250highestFC (PProof _) = Nothing
1251highestFC (PTactics _) = Nothing
1252highestFC (PElabError _) = Nothing
1253highestFC PImpossible = Nothing
1254highestFC (PCoerced tm) = highestFC tm
1255highestFC (PDisamb _ opts) = highestFC opts
1256highestFC (PUnifyLog tm) = highestFC tm
1257highestFC (PNoImplicits tm) = highestFC tm
1258highestFC (PQuasiquote _ _) = Nothing
1259highestFC (PUnquote tm) = highestFC tm
1260highestFC (PQuoteName _ fc) = Just fc
1261highestFC (PRunElab fc _ _) = Just fc
1262highestFC (PConstSugar fc _) = Just fc
1263highestFC (PAppImpl t _) = highestFC t
1267data ClassInfo = CI { instanceCtorName :: Name,
1268 class_methods :: [(Name, (FnOpts, PTerm))],
1269 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1270 class_default_superclasses :: [PDecl],
1271 class_params :: [Name],
1272 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1273 class_determiners :: [Int] }
1276deriving instance Binary ClassInfo
1277deriving instance NFData ClassInfo
1280-- Type inference data
1282data TIData = TIPartial -- ^ a function with a partially defined type
1283 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1286-- | Miscellaneous information about functions
1287data FnInfo = FnInfo { fn_params :: [Int] }
1290deriving instance Binary FnInfo
1291deriving instance NFData FnInfo
1294data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1295 detaggable :: Bool }
1298deriving instance Binary OptInfo
1299deriving instance NFData OptInfo
1302-- | Syntactic sugar info
1303data DSL' t = DSL { dsl_bind :: t,
1308 index_first :: Maybe t,
1309 index_next :: Maybe t,
1310 dsl_lambda :: Maybe t,
1314 deriving (Show, Functor)
1316deriving instance Binary DSL'
1317deriving instance NFData DSL'
1320type DSL = DSL' PTerm
1322data SynContext = PatternSyntax | TermSyntax | AnySyntax
1325deriving instance Binary SynContext
1326deriving instance NFData SynContext
1329data Syntax = Rule [SSymbol] PTerm SynContext
1330 | DeclRule [SSymbol] [PDecl]
1333syntaxNames :: Syntax -> [Name]
1334syntaxNames (Rule syms _ _) = mapMaybe ename syms
1335 where ename (Keyword n) = Just n
1337syntaxNames (DeclRule syms _) = mapMaybe ename syms
1338 where ename (Keyword n) = Just n
1341syntaxSymbols :: Syntax -> [SSymbol]
1342syntaxSymbols (Rule ss _ _) = ss
1343syntaxSymbols (DeclRule ss _) = ss
1345deriving instance Binary Syntax
1346deriving instance NFData Syntax
1349data SSymbol = Keyword Name
1358deriving instance Binary SSymbol
1359deriving instance NFData SSymbol
1362newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1364emptySyntaxRules :: SyntaxRules
1365emptySyntaxRules = SyntaxRules []
1367updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1368updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1370 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1375 ruleSort (s1:ss1) (s2:ss2) =
1376 case symCompare s1 s2 of
1377 EQ -> ruleSort ss1 ss2
1380 -- Better than creating Ord instance for SSymbol since
1381 -- in general this ordering does not really make sense.
1382 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1383 symCompare (Keyword _) _ = LT
1384 symCompare (Symbol _) (Keyword _) = GT
1385 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1386 symCompare (Symbol _) _ = LT
1387 symCompare (Binding _) (Keyword _) = GT
1388 symCompare (Binding _) (Symbol _) = GT
1389 symCompare (Binding b1) (Binding b2) = compare b1 b2
1390 symCompare (Binding _) _ = LT
1391 symCompare (Expr _) (Keyword _) = GT
1392 symCompare (Expr _) (Symbol _) = GT
1393 symCompare (Expr _) (Binding _) = GT
1394 symCompare (Expr e1) (Expr e2) = compare e1 e2
1395 symCompare (Expr _) _ = LT
1396 symCompare (SimpleExpr _) (Keyword _) = GT
1397 symCompare (SimpleExpr _) (Symbol _) = GT
1398 symCompare (SimpleExpr _) (Binding _) = GT
1399 symCompare (SimpleExpr _) (Expr _) = GT
1400 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1402initDSL = DSL (PRef f [] (sUN ">>="))
1403 (PRef f [] (sUN "return"))
1404 (PRef f [] (sUN "<*>"))
1405 (PRef f [] (sUN "pure"))
1412 where f = fileFC "(builtin)"
1414data Using = UImplicit Name PTerm
1415 | UConstraint Name [Name]
1416 deriving (Show, Eq, Data, Typeable)
1418deriving instance Binary Using
1419deriving instance NFData Using
1422data SyntaxInfo = Syn { using :: [Using],
1423 syn_params :: [(Name, PTerm)],
1424 syn_namespace :: [String],
1426 imp_methods :: [Name], -- class methods. When expanding
1427 -- implicits, these should be expanded even under
1429 decoration :: Name -> Name,
1431 implicitAllowed :: Bool,
1432 maxline :: Maybe Int,
1435 syn_in_quasiquote :: Int }
1438deriving instance NFData SyntaxInfo
1439deriving instance Binary SyntaxInfo
1442defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1444expandNS :: SyntaxInfo -> Name -> Name
1445expandNS syn n@(NS _ _) = n
1446expandNS syn n = case syn_namespace syn of
1451-- For inferring types of things
1453bi = fileFC "builtin"
1455inferTy = sMN 0 "__Infer"
1456inferCon = sMN 0 "__infer"
1457inferDecl = PDatadecl inferTy NoFC
1459 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1460 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1461 (PRef bi [] inferTy)), bi, [])]
1464infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1465infP = P (TCon 6 0) inferTy (TType (UVal 0))
1467getInferTerm, getInferType :: Term -> Term
1468getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1469getInferTerm (App _ (App _ _ _) tm) = tm
1470getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1472getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1473 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1474 toTy (PVar t) = PVTy t
1476getInferType (App _ (App _ _ ty) _) = ty
1480-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1482primNames = [inferTy, inferCon]
1485unitCon = sUN "MkUnit"
1487falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1488 "The empty type, also known as the trivially false proposition." ++
1490 "Use `void` or `absurd` to prove anything if you have a variable " ++
1491 "of type `Void` in scope."
1494pairTy = sNS (sUN "Pair") ["Builtins"]
1495pairCon = sNS (sUN "MkPair") ["Builtins"]
1497upairTy = sNS (sUN "UPair") ["Builtins"]
1498upairCon = sNS (sUN "MkUPair") ["Builtins"]
1502eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1503 "The propositional equality type. A proof that `x` = `y`." ++
1505 "To use such a proof, pattern-match on it, and the two equal things will " ++
1506 "then need to be the _same_ pattern." ++
1508 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1509 "is possible to state equalities between values of potentially different " ++
1510 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1512 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1514eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1515 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1517 [(reflDoc, reflParamDoc,
1518 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1519 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1520 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1521 pimp (n "B") Placeholder False,
1522 pexp (PRef bi [] (n "x")),
1523 pexp (PRef bi [] (n "x"))])), bi, [])]
1525 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1526 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1527 "shown that both sides are in fact equal."
1528 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1529 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1531eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1532 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1538-- | The special name to be used in the module documentation context -
1539-- not for use in the main definition context. The namespace around it
1540-- will determine the module to which the docs adhere.
1542modDocName = sMN 0 "ModuleDocs"
1544-- Defined in builtins.idr
1545sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1546sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1548piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1549piBind = piBindp expl
1551piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1553piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1556-- Pretty-printing declarations and terms
1558-- These "show" instances render to an absurdly wide screen because inserted line breaks
1559-- could interfere with interactive editing, which calls "show".
1561instance Show PTerm where
1562 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1564instance Show PDecl where
1565 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1567instance Show PClause where
1568 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1570instance Show PData where
1571 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1573instance Pretty PTerm OutputAnnotation where
1574 pretty = prettyImp defaultPPOption
1576-- | Colourise annotations according to an Idris state. It ignores the names
1577-- in the annotation, as there's no good way to show extended information on a
1579annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
1580annotationColour ist _ | not (idris_colourRepl ist) = Nothing
1581annotationColour ist (AnnConst c) =
1582 let theme = idris_colourTheme ist
1583 in Just $ if constIsType c
1584 then typeColour theme
1585 else dataColour theme
1586annotationColour ist (AnnData _ _) = Just $ dataColour (idris_colourTheme ist)
1587annotationColour ist (AnnType _ _) = Just $ typeColour (idris_colourTheme ist)
1588annotationColour ist (AnnBoundName _ True) = Just $ implicitColour (idris_colourTheme ist)
1589annotationColour ist (AnnBoundName _ False) = Just $ boundVarColour (idris_colourTheme ist)
1590annotationColour ist AnnKeyword = Just $ keywordColour (idris_colourTheme ist)
1591annotationColour ist (AnnName n _ _ _) =
1592 let ctxt = tt_ctxt ist
1593 theme = idris_colourTheme ist
1595 _ | isDConName n ctxt -> Just $ dataColour theme
1596 _ | isFnName n ctxt -> Just $ functionColour theme
1597 _ | isTConName n ctxt -> Just $ typeColour theme
1598 _ | isPostulateName n ist -> Just $ postulateColour theme
1599 _ | otherwise -> Nothing -- don't colourise unknown names
1600annotationColour ist (AnnTextFmt fmt) = Just (colour fmt)
1601 where colour BoldText = IdrisColour Nothing True False True False
1602 colour UnderlineText = IdrisColour Nothing True True False False
1603 colour ItalicText = IdrisColour Nothing True False False True
1604annotationColour ist _ = Nothing
1607-- | Colourise annotations according to an Idris state. It ignores the names
1608-- in the annotation, as there's no good way to show extended
1609-- information on a terminal. Note that strings produced this way will
1610-- not be coloured on Windows, so the use of the colour rendering
1611-- functions in Idris.Output is to be preferred.
1612consoleDecorate :: IState -> OutputAnnotation -> String -> String
1613consoleDecorate ist ann = maybe id colourise (annotationColour ist ann)
1615isPostulateName :: Name -> IState -> Bool
1616isPostulateName n ist = S.member n (idris_postulates ist)
1618-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1619prettyImp :: PPOption -- ^^ pretty printing options
1620 -> PTerm -- ^^ the term to pretty-print
1621 -> Doc OutputAnnotation
1622prettyImp impl = pprintPTerm impl [] [] []
1624-- | Serialise something to base64 using its Binary instance.
1626-- | Do the right thing for rendering a term in an IState
1627prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1628prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1630-- | Pretty-print a high-level Idris term in some bindings context with infix info
1631pprintPTerm :: PPOption -- ^^ pretty printing options
1632 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1633 -> [Name] -- ^^ names to always show in pi, even if not used
1634 -> [FixDecl] -- ^^ Fixity declarations
1635 -> PTerm -- ^^ the term to pretty-print
1636 -> Doc OutputAnnotation
1637pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1642 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1643 prettySe d p bnd (PQuote r) =
1644 text "![" <> pretty r <> text "]"
1645 prettySe d p bnd (PPatvar fc n) = pretty n
1647 | Just str <- slist d p bnd e = depth d $ str
1648 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1649 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1650 prettySe d p bnd (PLam fc n nfc ty sc) =
1651 depth d . bracket p startPrec . group . align . hang 2 $
1652 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1653 prettySe (decD d) startPrec ((n, False):bnd) sc
1654 prettySe d p bnd (PLet fc n nfc ty v sc) =
1655 depth d . bracket p startPrec . group . align $
1656 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1657 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1658 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1659 | n `elem` allNamesIn sc || ppopt_impl ppo && uname n || n `elem` docArgs
1660 || ppopt_pinames ppo && uname n =
1661 depth d . bracket p startPrec . group $
1662 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1663 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1665 depth d . bracket p startPrec . group $
1666 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1667 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1669 uname (UN n) = case str n of
1676 Static -> text "[static]" <> space
1678 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1680 depth d . bracket p startPrec $
1681 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1682 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1683 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1687 Static -> text "[static]" <> space
1689 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1690 depth d . bracket p startPrec $
1691 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1692 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
1693 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1694 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1695 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1696 depth d . bracket p startPrec $
1697 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1698 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1699 -- This case preserves the behavior of the former constructor PEq.
1700 -- It should be removed if feasible when the pretty-printing of infix
1701 -- operators in general is improved.
1702 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1703 | n == eqTy, ppopt_impl ppo =
1704 depth d . bracket p eqPrec $
1705 enclose lparen rparen eq <+>
1706 align (group (vsep (map (prettyArgS (decD d) bnd)
1709 depth d . bracket p eqPrec . align . group $
1710 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1711 where eq = annName eqTy (text "=")
1713 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1714 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1715 | UN nm <- basename f
1716 , not (ppopt_impl ppo) && null (getShowArgs args) =
1717 prettyName True (ppopt_impl ppo) bnd f
1718 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1719 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1720 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1721 | UN nm <- basename op
1723 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1724 case getShowArgs args of
1726 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1727 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1728 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1729 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1730 depth d . bracket p funcAppPrec $
1731 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1732 align (group (vsep (map (prettyArgS d bnd) rest)))
1733 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1734 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1735 f = getFixity (opStr op)
1737 Nothing -> funcAppPrec + 1
1738 Just (Infixl p') -> p'
1739 Just f' -> prec f' + 1
1741 Nothing -> funcAppPrec + 1
1742 Just (Infixr p') -> p'
1743 Just f' -> prec f' + 1
1744 inFix l r = align . group $
1745 (prettySe (decD d) left bnd l <+> opName False) <$>
1746 group (prettySe (decD d) right bnd r)
1747 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1748 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1749 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1750 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1751 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1752 let args = getShowArgs as
1753 fp = prettySe (decD d) (startPrec + 1) bnd f
1754 shownArgs = if ppopt_impl ppo then as else args
1756 depth d . bracket p funcAppPrec . group $
1759 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1760 prettySe d p bnd (PCase _ scr cases) =
1761 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1762 depth d (indent 2 (vsep (map ppcase cases)))
1764 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1765 ([(n, False) | n <- vars l] ++ bnd)
1766 in nest nestingSize $
1767 prettyCase l <+> text "=>" <+> prettyCase r
1768 -- Warning: this is a bit of a hack. At this stage, we don't have the
1769 -- global context, so we can't determine which names are constructors,
1770 -- which are types, and which are pattern variables on the LHS of the
1771 -- case pattern. We use the heuristic that names without a namespace
1772 -- are patvars, because right now case blocks in PTerms are always
1773 -- delaborated from TT before being sent to the pretty-printer. If they
1774 -- start getting printed directly, THIS WILL BREAK.
1775 -- Potential solution: add a list of known patvars to the cases in
1776 -- PCase, and have the delaborator fill it out, kind of like the pun
1777 -- disambiguation on PDPair.
1778 vars tm = filter noNS (allNamesIn tm)
1779 noNS (NS _ _) = False
1782 prettySe d p bnd (PIfThenElse _ c t f) =
1783 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1784 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1785 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1786 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1788 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1789 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1790 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1791 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1792 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1793 prettySe d p bnd (PRewrite _ l r _) =
1794 depth d . bracket p startPrec $
1795 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1796 prettySe d p bnd (PTyped l r) =
1797 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1798 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1799 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1800 align . group . vsep . punctuate (ann comma) $
1801 map (prettySe (decD d) startPrec bnd) elts
1802 where ann = case pun of
1804 IsType -> annName pairTy
1805 IsTerm -> annName pairCon
1806 prettySe d p bnd (PDPair _ _ pun l t r) =
1810 annotated (text "**") <+>
1811 prettySe (decD d) startPrec (addBinding bnd) r <>
1813 where annotated = case pun of
1814 IsType -> annName sigmaTy
1815 IsTerm -> annName sigmaCon
1817 (left, addBinding) = case (l, pun) of
1818 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1819 _ -> (prettySe (decD d) startPrec bnd l, id)
1820 prettySe d p bnd (PAlternative ns a as) =
1821 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1824 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1825 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1826 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1827 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1828 -- XXX: add pretty for tactics
1829 prettySe d p bnd (PProof ts) =
1830 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1831 prettySe d p bnd (PTactics ts) =
1832 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1833 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1834 prettySe d p bnd (PReturn f) = kwd "return"
1835 prettySe d p bnd PImpossible = kwd "impossible"
1836 prettySe d p bnd Placeholder = text "_"
1837 prettySe d p bnd (PDoBlock dos) =
1838 bracket p startPrec $
1839 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1840 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1841 ppdo bnd (DoBind _ bn _ tm : dos) =
1842 (prettyBindingOf bn False <+> text "<-" <+>
1843 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1844 ppdo ((bn, False):bnd) dos
1845 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1846 text "no pretty printer for pattern-matching do binding" :
1848 ppdo bnd (DoLet _ ln _ ty v : dos) =
1849 (kwd "let" <+> prettyBindingOf ln False <+>
1850 (if ty /= Placeholder
1851 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1853 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1854 ppdo ((ln, False):bnd) dos
1855 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1856 text "no pretty printer for pattern-matching do binding" :
1859 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1860 prettySe d p bnd (PElabError s) = pretty s
1861 -- Quasiquote pprinting ignores bound vars
1862 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1863 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1864 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1865 prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1866 prettySe d p bnd (PRunElab _ tm _) =
1867 bracket p funcAppPrec . group . align . hang 2 $
1869 prettySe (decD d) funcAppPrec bnd tm
1870 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1872 prettySe d p bnd _ = text "missing pretty-printer for term"
1874 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1875 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1876 where display (UN n) = T.unpack n
1877 display (MN _ n) = T.unpack n
1878 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1879 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1882 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1883 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1884 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1885 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1887 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1888 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1889 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1890 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1892 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1893 annName n = annotate (AnnName n Nothing Nothing Nothing)
1895 opStr :: Name -> String
1896 opStr (NS n _) = opStr n
1897 opStr (UN n) = T.unpack n
1899 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1900 slist' (Just d) _ _ _ | d <= 0 = Nothing
1902 | containsHole e = Nothing
1903 slist' d p bnd (PApp _ (PRef _ _ nil) _)
1904 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1905 slist' d p bnd (PRef _ _ nil)
1906 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1907 slist' d p bnd (PApp _ (PRef _ _ cons) args)
1908 | nsroot cons == sUN "::",
1909 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1911 Just tl' <- slist' (decD d) p bnd tl
1912 = Just (prettySe d startPrec bnd hd : tl')
1914 isImp (PImp {}) = True
1916 slist' _ _ _ tm = Nothing
1918 slist d p bnd e | Just es <- slist' d p bnd e = Just $
1920 [] -> annotate (AnnData "" "") $ text "[]"
1921 [x] -> enclose left right . group $ x
1922 xs -> enclose left right .
1923 align . group . vsep .
1924 punctuate comma $ xs
1925 where left = (annotate (AnnData "" "") (text "["))
1926 right = (annotate (AnnData "" "") (text "]"))
1927 comma = (annotate (AnnData "" "") (text ","))
1928 slist _ _ _ _ = Nothing
1930 pairElts :: PTerm -> Maybe [PTerm]
1931 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1932 | otherwise = Just [x, y]
1933 pairElts _ = Nothing
1935 natns = "Prelude.Nat."
1937 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1938 snat (Just x) _ _ | x <= 0 = Nothing
1939 snat d p (PRef _ _ z)
1940 | show z == (natns++"Z") || show z == "Z" = Just 0
1941 snat d p (PApp _ s [PExp {getTm=n}])
1942 | show s == (natns++"S") || show s == "S",
1943 Just n' <- snat (decD d) p n
1945 snat _ _ _ = Nothing
1947 bracket outer inner doc
1948 | outer > inner = lparen <> doc <> rparen
1951 ellipsis = text "..."
1954 depth (Just d) = if d <= 0 then const (ellipsis) else id
1956 decD = fmap (\x -> x - 1)
1958 kwd = annotate AnnKeyword . text
1960 fixities :: M.Map String Fixity
1961 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1963 getFixity :: String -> Maybe Fixity
1964 getFixity = flip M.lookup fixities
1966-- | Strip away namespace information
1967basename :: Name -> Name
1968basename (NS n _) = basename n
1971-- | Determine whether a name was the one inserted for a hole or
1972-- guess by the delaborator
1973isHoleName :: Name -> Bool
1974isHoleName (UN n) = n == T.pack "[__]"
1977-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1978containsHole :: PTerm -> Bool
1979containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
1981-- | Pretty-printer helper for names that attaches the correct annotations
1983 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1984 -> Bool -- ^^ whether to show namespaces
1985 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1986 -> Name -- ^^ the name to pprint
1987 -> Doc OutputAnnotation
1988prettyName infixParen showNS bnd n
1989 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1990 | (UN n') <- n, T.unpack n' == "_" = text "_"
1991 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1992 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1993 where fullName = text nameSpace <> parenthesise (text (baseName n))
1994 baseName (UN n) = T.unpack n
1995 baseName (NS n ns) = baseName n
1996 baseName (MN i s) = T.unpack s
1997 baseName other = show other
1998 nameSpace = case n of
1999 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
2001 isInfix = case baseName n of
2003 (c : _) -> not (isAlpha c)
2004 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2007showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2008showCImp ppo (PClause _ n l ws r w)
2009 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2010 <+> text "where" <+> text (show w)
2013 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2014showCImp ppo (PWith _ n l ws r pn w)
2015 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2016 <+> braces (text (show w))
2019 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2022showDImp :: PPOption -> PData -> Doc OutputAnnotation
2023showDImp ppo (PDatadecl n nfc ty cons)
2024 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2025 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2027showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2028showDecls o ds = vsep (map (showDeclImp o) ds)
2030showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2031showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2032showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2033 indent 2 (vsep (map (showCImp o) cs))
2034showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2035showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2036showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2037showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2038showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2039 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2040showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
2041 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2042showDeclImp _ _ = text "..."
2043-- showDeclImp (PImport o) = "import " ++ o
2045getImps :: [PArg] -> [(Name, PTerm)]
2047getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2048getImps (_ : xs) = getImps xs
2050getExps :: [PArg] -> [PTerm]
2052getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2053getExps (_ : xs) = getExps xs
2055getShowArgs :: [PArg] -> [PArg]
2057getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2058getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2059 | PImp _ _ _ _ tm <- e
2060 , containsHole tm = e : getShowArgs xs
2061getShowArgs (_ : xs) = getShowArgs xs
2063getConsts :: [PArg] -> [PTerm]
2065getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2066getConsts (_ : xs) = getConsts xs
2068getAll :: [PArg] -> [PTerm]
2073showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
2074 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
2075 -> PPOption -- ^^ pretty printing options
2076 -> Bool -- ^^ whether to colourise
2077 -> Name -- ^^ the term to show
2079showName ist bnd ppo colour n = case ist of
2080 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2081 Nothing -> showbasic n
2082 where name = if ppopt_impl ppo then show n else showbasic n
2083 showbasic n@(UN _) = showCG n
2084 showbasic (MN i s) = str s
2085 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2086 showbasic (SN s) = show s
2088 colourise n t = let ctxt' = fmap tt_ctxt ist in
2091 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2092 else colouriseBound t name
2093 | isDConName n ctxt -> colouriseData t name
2094 | isFnName n ctxt -> colouriseFun t name
2095 | isTConName n ctxt -> colouriseType t name
2096 -- The assumption is that if a name is not bound and does not exist in the
2097 -- global context, then we're somewhere in which implicit info has been lost
2098 -- (like error messages). Thus, unknown vars are colourised as implicits.
2099 | otherwise -> colouriseImplicit t name
2101showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
2102 -> PTerm -- ^^ the term to show
2104showTm ist = displayDecorated (consoleDecorate ist) .
2105 renderPretty 0.8 100000 .
2106 prettyImp (ppOptionIst ist)
2108-- | Show a term with implicits, no colours
2109showTmImpls :: PTerm -> String
2110showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2112-- | Show a term with specific options
2113showTmOpts :: PPOption -> PTerm -> String
2114showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2117instance Sized PTerm where
2118 size (PQuote rawTerm) = size rawTerm
2119 size (PRef fc _ name) = size name
2120 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2121 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2122 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2123 size (PTyped trm ty) = 1 + size trm + size ty
2124 size (PApp fc name args) = 1 + size args
2125 size (PAppBind fc name args) = 1 + size args
2126 size (PCase fc trm bdy) = 1 + size trm + size bdy
2127 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2128 size (PTrue fc _) = 1
2129 size (PResolveTC fc) = 1
2130 size (PRewrite fc left right _) = 1 + size left + size right
2131 size (PPair fc _ _ left right) = 1 + size left + size right
2132 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2133 size (PAlternative _ a alts) = 1 + size alts
2134 size (PHidden hidden) = size hidden
2135 size (PUnifyLog tm) = size tm
2136 size (PDisamb _ tm) = size tm
2137 size (PNoImplicits tm) = size tm
2139 size (PUniverse _) = 1
2140 size (PConstant fc const) = 1 + size fc + size const
2141 size Placeholder = 1
2142 size (PDoBlock dos) = 1 + size dos
2143 size (PIdiom fc term) = 1 + size term
2144 size (PReturn fc) = 1
2145 size (PMetavar _ name) = 1
2146 size (PProof tactics) = size tactics
2147 size (PElabError err) = size err
2148 size PImpossible = 1
2151getPArity :: PTerm -> Int
2152getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2155-- Return all names, free or globally bound, in the given term.
2157allNamesIn :: PTerm -> [Name]
2158allNamesIn tm = nub $ ni [] tm
2159 where -- TODO THINK added niTacImp, but is it right?
2161 | not (n `elem` env) = [n]
2162 ni env (PPatvar _ n) = [n]
2163 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2164 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2165 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2166 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
2167 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2168 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2169 ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc
2170 ni env (PHidden tm) = ni env tm
2171 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2172 ni env (PTyped l r) = ni env l ++ ni env r
2173 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2174 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r
2175 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2176 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2177 ni env (PAlternative ns a ls) = concatMap (ni env) ls
2178 ni env (PUnifyLog tm) = ni env tm
2179 ni env (PDisamb _ tm) = ni env tm
2180 ni env (PNoImplicits tm) = ni env tm
2183 niTacImp env (TacImp _ _ scr) = ni env scr
2187-- Return all names defined in binders in the given term
2188boundNamesIn :: PTerm -> [Name]
2189boundNamesIn tm = S.toList (ni S.empty tm)
2190 where -- TODO THINK Added niTacImp, but is it right?
2191 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
2192 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
2193 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
2194 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
2195 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
2196 ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
2197 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
2198 ni set (PRewrite _ l r _) = ni (ni set l) r
2199 ni set (PTyped l r) = ni (ni set l) r
2200 ni set (PPair _ _ _ l r) = ni (ni set l) r
2201 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r
2202 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r
2203 ni set (PAlternative ns a as) = niTms set as
2204 ni set (PHidden tm) = ni set tm
2205 ni set (PUnifyLog tm) = ni set tm
2206 ni set (PDisamb _ tm) = ni set tm
2207 ni set (PNoImplicits tm) = ni set tm
2211 niTms set (x : xs) = niTms (ni set x) xs
2213 niTacImp set (TacImp _ _ scr) = ni set scr
2214 niTacImp set _ = set
2216-- Return names which are valid implicits in the given term (type).
2217implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2218implicitNamesIn uvars ist tm = nub $ ni [] tm
2221 | not (n `elem` env)
2222 = case lookupTy n (tt_ctxt ist) of
2224 _ -> if n `elem` uvars then [n] else []
2225 ni env (PApp _ f@(PRef _ _ n) as)
2226 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
2227 | otherwise = concatMap (ni env) (map getTm as)
2228 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2229 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2230 ni env (PCase _ c os) = ni env c ++
2231 -- names in 'os', not counting the names bound in the cases
2232 (nub (concatMap (ni env) (map snd os))
2233 \\ nub (concatMap (ni env) (map fst os)))
2234 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2235 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2236 ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
2237 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2238 ni env (PTyped l r) = ni env l ++ ni env r
2239 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2240 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2241 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2242 ni env (PAlternative ns a as) = concatMap (ni env) as
2243 ni env (PHidden tm) = ni env tm
2244 ni env (PUnifyLog tm) = ni env tm
2245 ni env (PDisamb _ tm) = ni env tm
2246 ni env (PNoImplicits tm) = ni env tm
2249-- Return names which are free in the given term.
2250namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2251namesIn uvars ist tm = nub $ ni [] tm
2254 | not (n `elem` env)
2255 = case lookupTy n (tt_ctxt ist) of
2257 _ -> if n `elem` (map fst uvars) then [n] else []
2258 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2259 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2260 ni env (PCase _ c os) = ni env c ++
2261 -- names in 'os', not counting the names bound in the cases
2262 (nub (concatMap (ni env) (map snd os))
2263 \\ nub (concatMap (ni env) (map fst os)))
2264 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2265 ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2266 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2267 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2268 ni env (PTyped l r) = ni env l ++ ni env r
2269 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2270 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2271 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2272 ni env (PAlternative ns a as) = concatMap (ni env) as
2273 ni env (PHidden tm) = ni env tm
2274 ni env (PUnifyLog tm) = ni env tm
2275 ni env (PDisamb _ tm) = ni env tm
2276 ni env (PNoImplicits tm) = ni env tm
2279 niTacImp env (TacImp _ _ scr) = ni env scr
2282-- Return which of the given names are used in the given term.
2284usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2285usedNamesIn vars ist tm = nub $ ni [] tm
2286 where -- TODO THINK added niTacImp, but is it right?
2288 | n `elem` vars && not (n `elem` env)
2289 = case lookupDefExact n (tt_ctxt ist) of
2292 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2293 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2294 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2295 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2296 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2297 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2298 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2299 ni env (PTyped l r) = ni env l ++ ni env r
2300 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2301 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2302 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2303 ni env (PAlternative ns a as) = concatMap (ni env) as
2304 ni env (PHidden tm) = ni env tm
2305 ni env (PUnifyLog tm) = ni env tm
2306 ni env (PDisamb _ tm) = ni env tm
2307 ni env (PNoImplicits tm) = ni env tm
2310 niTacImp env (TacImp _ _ scr) = ni env scr
2313-- Return the list of inaccessible (= dotted) positions for a name.
2314getErasureInfo :: IState -> Name -> [Int]
2315getErasureInfo ist n =
2316 case lookupCtxtExact n (idris_optimisation ist) of
2317 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