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
681deriving instance Binary PDecl'
682deriving instance NFData PDecl'
685-- | The set of source directives
686data Directive = DLib Codegen String |
687 DLink Codegen String |
688 DFlag Codegen String |
689 DInclude Codegen String |
692 DAccess Accessibility |
695 DDynamicLibs [String] |
696 DNameHint Name FC [(Name, FC)] |
697 DErrorHandlers Name FC Name FC [(Name, FC)] |
698 DLanguage LanguageExt |
701-- | A set of instructions for things that need to happen in IState
702-- after a term elaboration when there's been reflected elaboration.
703data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
704 | RClausesInstrs Name [([Name], Term, Term)]
705 | RAddInstance Name Name
707-- | For elaborator state
708data EState = EState {
709 case_decls :: [(Name, PDecl)],
710 delayed_elab :: [(Int, Elab' EState ())],
711 new_tyDecls :: [RDeclInstructions],
712 highlighting :: [(FC, OutputAnnotation)]
716initEState = EState [] [] [] []
718type ElabD a = Elab' EState a
720highlightSource :: FC -> OutputAnnotation -> ElabD ()
721highlightSource fc annot =
722 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
724-- | One clause of a top-level definition. Term arguments to constructors are:
726-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
728-- 2. The list of extra 'with' patterns
730-- 3. The right-hand side
732-- 4. The where block (PDecl' t)
734data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
735 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
736 | PClauseR FC [t] t [PDecl' t]
737 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
740deriving instance Binary PClause'
741deriving instance NFData PClause'
745data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
746 d_name_fc :: FC, -- ^ The precise location of the type constructor name
747 d_tcon :: t, -- ^ Type constructor
748 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
750 -- ^ Data declaration
751 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
752 -- ^ "Placeholder" for data whose constructors are defined later
755-- | Transform the FCs in a PData and its associated terms. The first
756-- function transforms the general-purpose FCs, and the second transforms
757-- those that are used for semantic source highlighting, so they can be
759mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
760mapPDataFC f g (PDatadecl n nfc tycon ctors) =
761 PDatadecl n (g nfc) (mapPTermFC f g tycon) (map ctorFC ctors)
762 where ctorFC (doc, argDocs, n, nfc, ty, fc, ns) =
763 (doc, argDocs, n, g nfc, mapPTermFC f g ty, f fc, ns)
764mapPDataFC f g (PLaterdecl n nfc tycon) =
765 PLaterdecl n (g nfc) (mapPTermFC f g tycon)
767deriving instance Binary PData'
768deriving instance NFData PData'
771-- Handy to get a free function for applying PTerm -> PTerm functions
772-- across a program, by deriving Functor
774type PDecl = PDecl' PTerm
775type PData = PData' PTerm
776type PClause = PClause' PTerm
778-- | Transform the FCs in a PTerm. The first function transforms the
779-- general-purpose FCs, and the second transforms those that are used
780-- for semantic source highlighting, so they can be treated specially.
781mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
782mapPDeclFC f g (PFix fc fixity ops) =
783 PFix (f fc) fixity ops
784mapPDeclFC f g (PTy doc argdocs syn fc opts n nfc ty) =
785 PTy doc argdocs syn (f fc) opts n (g nfc) (mapPTermFC f g ty)
786mapPDeclFC f g (PPostulate ext doc syn fc nfc opts n ty) =
787 PPostulate ext doc syn (f fc) (g nfc) opts n (mapPTermFC f g ty)
789mapPDeclFC f g (PClauses fc opts n clauses) =
790 PClauses (f fc) opts n (map (fmap (mapPTermFC f g)) clauses)
791mapPDeclFC f g (PCAF fc n tm) = PCAF (f fc) n (mapPTermFC f g tm)
792mapPDeclFC f g (PData doc argdocs syn fc opts dat) =
793 PData doc argdocs syn (f fc) opts (mapPDataFC f g dat)
794mapPDeclFC f g (PParams fc params decls) =
796 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)
797 (map (mapPDeclFC f g) decls)
798mapPDeclFC f g (PNamespace ns fc decls) =
799 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)
800mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =
801 PRecord doc syn (f fc) opts n (g nfc)
802 (map (\(pn, pnfc, plic, ty) -> (pn, g pnfc, plic, mapPTermFC f g ty)) params)
804 (map (\(fn, plic, ty, fdoc) -> (fmap (\(fn', fnfc) -> (fn', g fnfc)) fn,
805 plic, mapPTermFC f g ty, fdoc))
807 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)
810mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =
811 PClass doc syn (f fc)
812 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)
813 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)
814 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)
815 (map (mapPDeclFC f g) body)
816 (fmap (\(n, nfc) -> (n, g nfc)) ctor)
818mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn cnfc params instTy instN body) =
819 PInstance doc paramDocs syn (f fc)
820 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)
821 cn (g cnfc) (map (mapPTermFC f g) params)
822 (mapPTermFC f g instTy)
824 (map (mapPDeclFC f g) body)
825mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)
826mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $
828 Rule syms tm ctxt -> Rule syms (mapPTermFC f g tm) ctxt
829 DeclRule syms decls -> DeclRule syms (map (mapPDeclFC f g) decls)
830mapPDeclFC f g (PMutual fc decls) =
831 PMutual (f fc) (map (mapPDeclFC f g) decls)
832mapPDeclFC f g (PDirective d) =
835 DNameHint n nfc ns ->
836 DNameHint n (g nfc) (map (\(hn, hnfc) -> (hn, g hnfc)) ns)
837 DErrorHandlers n nfc n' nfc' ns ->
838 DErrorHandlers n (g nfc) n' (g nfc') $
839 map (\(an, anfc) -> (an, g anfc)) ns
840mapPDeclFC f g (PProvider doc syn fc nfc what n) =
841 PProvider doc syn (f fc) (g nfc) (fmap (mapPTermFC f g) what) n
842mapPDeclFC f g (PTransform fc safe l r) =
843 PTransform (f fc) safe (mapPTermFC f g l) (mapPTermFC f g r)
844mapPDeclFC f g (PRunElabDecl fc script) =
845 PRunElabDecl (f fc) (mapPTermFC f g script)
847-- | Get all the names declared in a declaration
848declared :: PDecl -> [Name]
849declared (PFix _ _ _) = []
850declared (PTy _ _ _ _ _ n fc t) = [n]
851declared (PPostulate _ _ _ _ _ _ n t) = [n]
852declared (PClauses _ _ n _) = [] -- not a declaration
853declared (PCAF _ n _) = [n]
854declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
855 where fstt (_, _, a, _, _, _, _) = a
856declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
857declared (PParams _ _ ds) = concatMap declared ds
858declared (PNamespace _ _ ds) = concatMap declared ds
859declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
860declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
861declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
862declared (PDSL n _) = [n]
863declared (PSyntax _ _) = []
864declared (PMutual _ ds) = concatMap declared ds
865declared (PDirective _) = []
868-- get the names declared, not counting nested parameter blocks
869tldeclared :: PDecl -> [Name]
870tldeclared (PFix _ _ _) = []
871tldeclared (PTy _ _ _ _ _ n _ t) = [n]
872tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
873tldeclared (PClauses _ _ n _) = [] -- not a declaration
874tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
875tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
876 where fstt (_, _, a, _, _, _, _) = a
877tldeclared (PParams _ _ ds) = []
878tldeclared (PMutual _ ds) = concatMap tldeclared ds
879tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
880tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
881tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
884defined :: PDecl -> [Name]
885defined (PFix _ _ _) = []
886defined (PTy _ _ _ _ _ n _ t) = []
887defined (PPostulate _ _ _ _ _ _ n t) = []
888defined (PClauses _ _ n _) = [n] -- not a declaration
889defined (PCAF _ n _) = [n]
890defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
891 where fstt (_, _, a, _, _, _, _) = a
892defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
893defined (PParams _ _ ds) = concatMap defined ds
894defined (PNamespace _ _ ds) = concatMap defined ds
895defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
896defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
897defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
898defined (PDSL n _) = [n]
899defined (PSyntax _ _) = []
900defined (PMutual _ ds) = concatMap defined ds
901defined (PDirective _) = []
904updateN :: [(Name, Name)] -> Name -> Name
905updateN ns n | Just n' <- lookup n ns = n'
908updateNs :: [(Name, Name)] -> PTerm -> PTerm
910updateNs ns t = mapPT updateRef t
911 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
914-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
916-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
917-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
918-- where updateCNs ns (PClause n l ts r ds)
919-- = PClause (updateN ns n) (fmap (updateNs ns) l)
920-- (map (fmap (updateNs ns)) ts)
921-- (fmap (updateNs ns) r)
922-- (map (updateDNs ns) ds)
925data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
927-- | High level language terms
928data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
929 | 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.
930 | PInferRef FC [FC] Name -- ^ A name to be defined later
931 | PPatvar FC Name -- ^ A pattern variable
932 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
933 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
934 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
935 | PTyped PTerm PTerm -- ^ Term with explicit type
936 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
937 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
938 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
939 | PMatchApp FC Name -- ^ Make an application by type matching
940 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
941 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
942 | PTrue FC PunInfo -- ^ Unit type..?
943 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
944 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
945 | 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.
946 | 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.
947 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
948 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
949 | PHidden PTerm -- ^ Irrelevant or hidden pattern
950 | PType FC -- ^ 'Type' type
951 | PUniverse Universe -- ^ Some universe
952 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
953 | PConstant FC Const -- ^ Builtin types
954 | Placeholder -- ^ Underscore
955 | PDoBlock [PDo] -- ^ Do notation
956 | PIdiom FC PTerm -- ^ Idiom brackets
958 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
959 | PProof [PTactic] -- ^ Proof script
960 | PTactics [PTactic] -- ^ As PProof, but no auto solving
961 | PElabError Err -- ^ Error to report on elaboration
962 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
963 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
964 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
965 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
966 | PNoImplicits PTerm -- ^ never run implicit converions on the term
967 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
968 | PUnquote PTerm -- ^ ~Term
969 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
970 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
971 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
972 deriving (Eq, Data, Typeable)
974data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
977 deriving (Eq, Data, Typeable)
979-- | Transform the FCs in a PTerm. The first function transforms the
980-- general-purpose FCs, and the second transforms those that are used
981-- for semantic source highlighting, so they can be treated specially.
982mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
983mapPTermFC f g (PQuote q) = PQuote q
984mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
985mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
986mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
987mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
988mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
989mapPTermFC 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)
990mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
991mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
992mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
993mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
994mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
995mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
996mapPTermFC 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)
997mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
998mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
999mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
1000mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
1001mapPTermFC 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)
1002mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
1003mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
1004mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
1005mapPTermFC f g (PType fc) = PType (f fc)
1006mapPTermFC f g (PUniverse u) = PUniverse u
1007mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
1008mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
1009mapPTermFC f g Placeholder = Placeholder
1010mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
1011 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
1012 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
1013 mapPDoFC (DoBindP fc t1 t2 alts) =
1014 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
1015 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1016 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
1017mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
1018mapPTermFC f g (PReturn fc) = PReturn (f fc)
1019mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
1020mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
1021mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
1022mapPTermFC f g (PElabError err) = PElabError err
1023mapPTermFC f g PImpossible = PImpossible
1024mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
1025mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
1026mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
1027mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
1028mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
1029mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
1030mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
1031mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
1032mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
1035dg instance Binary PTerm
1036deriving instance NFData PTerm
1039mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
1040mapPT f t = f (mpt t) where
1041 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
1042 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
1043 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
1044 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
1046 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
1047 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
1048 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
1049 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
1050 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
1051 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
1052 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
1053 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
1054 mpt (PHidden t) = PHidden (mapPT f t)
1055 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
1056 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
1057 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
1058 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
1059 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
1060 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
1061 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
1065data PTactic' t = Intro [Name] | Intros | Focus Name
1066 | Refine Name [Bool] | Rewrite t | DoUnify
1073 | LetTac Name t | LetTacTy Name t t
1074 | Exact t | Compute | Trivial | TCInstance
1075 | ProofSearch Bool Bool Int (Maybe Name)
1076 [Name] -- allowed local names
1078 -- ^ the bool is whether to search recursively
1081 | ProofState | ProofTerm | Undo
1082 | Try (PTactic' t) (PTactic' t)
1083 | TSeq (PTactic' t) (PTactic' t)
1084 | ApplyTactic t -- see Language.Reflection module
1088 | GoalType String (PTactic' t)
1091 | TDocStr (Either Name Const)
1094 | TFail [ErrorReportPart]
1097 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1099deriving instance Binary PTactic'
1100deriving instance NFData PTactic'
1102instance Sized a => Sized (PTactic' a) where
1103 size (Intro nms) = 1 + size nms
1105 size (Focus nm) = 1 + size nm
1106 size (Refine nm bs) = 1 + size nm + length bs
1107 size (Rewrite t) = 1 + size t
1108 size (Induction t) = 1 + size t
1109 size (LetTac nm t) = 1 + size nm + size t
1110 size (Exact t) = 1 + size t
1118 size (Try l r) = 1 + size l + size r
1119 size (TSeq l r) = 1 + size l + size r
1120 size (ApplyTactic t) = 1 + size t
1121 size (Reflect t) = 1 + size t
1122 size (Fill t) = 1 + size t
1126 size (TFail ts) = 1 + size ts
1129 size (CaseTac x) = 1 + size x
1130 size (Equiv t) = 1 + size t
1131 size (Claim x y) = 1 + size x + size y
1133 size (MatchRefine x) = 1 + size x
1134 size (LetTacTy x y z) = 1 + size x + size y + size z
1137type PTactic = PTactic' PTerm
1139data PDo' t = DoExp FC t
1140 | DoBind FC Name FC t -- ^ second FC is precise name location
1141 | DoBindP FC t t [(t,t)]
1142 | DoLet FC Name FC t t -- ^ second FC is precise name location
1144 deriving (Eq, Functor, Data, Typeable)
1146deriving instance Binary PDo'
1147deriving instance NFData PDo'
1150instance Sized a => Sized (PDo' a) where
1151 size (DoExp fc t) = 1 + size fc + size t
1152 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1153 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1154 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1155 size (DoLetP fc l r) = 1 + size fc + size l + size r
1157type PDo = PDo' PTerm
1159-- The priority gives a hint as to elaboration order. Best to elaborate
1160-- things early which will help give a more concrete type to other
1161-- variables, e.g. a before (interpTy a).
1163data PArg' t = PImp { priority :: Int,
1164 machine_inf :: Bool, -- true if the machine inferred it
1165 argopts :: [ArgOpt],
1168 | PExp { priority :: Int,
1169 argopts :: [ArgOpt],
1172 | PConstraint { priority :: Int,
1173 argopts :: [ArgOpt],
1176 | PTacImplicit { priority :: Int,
1177 argopts :: [ArgOpt],
1181 deriving (Show, Eq, Functor, Data, Typeable)
1183data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1184 deriving (Show, Eq, Data, Typeable)
1186instance Sized a => Sized (PArg' a) where
1187 size (PImp p _ l nm trm) = 1 + size nm + size trm
1188 size (PExp p l nm trm) = 1 + size nm + size trm
1189 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1190 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1193deriving instance Binary PArg'
1194deriving instance NFData PArg'
1197pimp n t mach = PImp 1 mach [] n t
1198pexp t = PExp 1 [] (sMN 0 "arg") t
1199pconst t = PConstraint 1 [] (sMN 0 "carg") t
1200ptacimp n s t = PTacImplicit 2 [] n s t
1202type PArg = PArg' PTerm
1204-- | Get the highest FC in a term, if one exists
1205highestFC :: PTerm -> Maybe FC
1206highestFC (PQuote _) = Nothing
1207highestFC (PRef fc _ _) = Just fc
1208highestFC (PInferRef fc _ _) = Just fc
1209highestFC (PPatvar fc _) = Just fc
1210highestFC (PLam fc _ _ _ _) = Just fc
1211highestFC (PPi _ _ _ _ _) = Nothing
1212highestFC (PLet fc _ _ _ _ _) = Just fc
1213highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1214highestFC (PApp fc _ _) = Just fc
1215highestFC (PAppBind fc _ _) = Just fc
1216highestFC (PMatchApp fc _) = Just fc
1217highestFC (PCase fc _ _) = Just fc
1218highestFC (PIfThenElse fc _ _ _) = Just fc
1219highestFC (PTrue fc _) = Just fc
1220highestFC (PResolveTC fc) = Just fc
1221highestFC (PRewrite fc _ _ _) = Just fc
1222highestFC (PPair fc _ _ _ _) = Just fc
1223highestFC (PDPair fc _ _ _ _ _) = Just fc
1224highestFC (PAs fc _ _) = Just fc
1225highestFC (PAlternative _ _ args) =
1226 case mapMaybe highestFC args of
1229highestFC (PHidden _) = Nothing
1230highestFC (PType fc) = Just fc
1231highestFC (PUniverse _) = Nothing
1232highestFC (PGoal fc _ _ _) = Just fc
1233highestFC (PConstant fc _) = Just fc
1234highestFC Placeholder = Nothing
1235highestFC (PDoBlock lines) =
1236 case map getDoFC lines of
1240 getDoFC (DoExp fc t) = fc
1241 getDoFC (DoBind fc nm nfc t) = fc
1242 getDoFC (DoBindP fc l r alts) = fc
1243 getDoFC (DoLet fc nm nfc l r) = fc
1244 getDoFC (DoLetP fc l r) = fc
1246highestFC (PIdiom fc _) = Just fc
1247highestFC (PReturn fc) = Just fc
1248highestFC (PMetavar fc _) = Just fc
1249highestFC (PProof _) = Nothing
1250highestFC (PTactics _) = Nothing
1251highestFC (PElabError _) = Nothing
1252highestFC PImpossible = Nothing
1253highestFC (PCoerced tm) = highestFC tm
1254highestFC (PDisamb _ opts) = highestFC opts
1255highestFC (PUnifyLog tm) = highestFC tm
1256highestFC (PNoImplicits tm) = highestFC tm
1257highestFC (PQuasiquote _ _) = Nothing
1258highestFC (PUnquote tm) = highestFC tm
1259highestFC (PQuoteName _ fc) = Just fc
1260highestFC (PRunElab fc _ _) = Just fc
1261highestFC (PConstSugar fc _) = Just fc
1262highestFC (PAppImpl t _) = highestFC t
1266data ClassInfo = CI { instanceCtorName :: Name,
1267 class_methods :: [(Name, (FnOpts, PTerm))],
1268 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1269 class_default_superclasses :: [PDecl],
1270 class_params :: [Name],
1271 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1272 class_determiners :: [Int] }
1275deriving instance Binary ClassInfo
1276deriving instance NFData ClassInfo
1279-- Type inference data
1281data TIData = TIPartial -- ^ a function with a partially defined type
1282 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1285-- | Miscellaneous information about functions
1286data FnInfo = FnInfo { fn_params :: [Int] }
1289deriving instance Binary FnInfo
1290deriving instance NFData FnInfo
1293data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1294 detaggable :: Bool }
1297deriving instance Binary OptInfo
1298deriving instance NFData OptInfo
1301-- | Syntactic sugar info
1302data DSL' t = DSL { dsl_bind :: t,
1307 index_first :: Maybe t,
1308 index_next :: Maybe t,
1309 dsl_lambda :: Maybe t,
1313 deriving (Show, Functor)
1315deriving instance Binary DSL'
1316deriving instance NFData DSL'
1319type DSL = DSL' PTerm
1321data SynContext = PatternSyntax | TermSyntax | AnySyntax
1324deriving instance Binary SynContext
1325deriving instance NFData SynContext
1328data Syntax = Rule [SSymbol] PTerm SynContext
1329 | DeclRule [SSymbol] [PDecl]
1332syntaxNames :: Syntax -> [Name]
1333syntaxNames (Rule syms _ _) = mapMaybe ename syms
1334 where ename (Keyword n) = Just n
1336syntaxNames (DeclRule syms _) = mapMaybe ename syms
1337 where ename (Keyword n) = Just n
1340syntaxSymbols :: Syntax -> [SSymbol]
1341syntaxSymbols (Rule ss _ _) = ss
1342syntaxSymbols (DeclRule ss _) = ss
1344deriving instance Binary Syntax
1345deriving instance NFData Syntax
1348data SSymbol = Keyword Name
1357deriving instance Binary SSymbol
1358deriving instance NFData SSymbol
1361newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1363emptySyntaxRules :: SyntaxRules
1364emptySyntaxRules = SyntaxRules []
1366updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1367updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1369 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1374 ruleSort (s1:ss1) (s2:ss2) =
1375 case symCompare s1 s2 of
1376 EQ -> ruleSort ss1 ss2
1379 -- Better than creating Ord instance for SSymbol since
1380 -- in general this ordering does not really make sense.
1381 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1382 symCompare (Keyword _) _ = LT
1383 symCompare (Symbol _) (Keyword _) = GT
1384 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1385 symCompare (Symbol _) _ = LT
1386 symCompare (Binding _) (Keyword _) = GT
1387 symCompare (Binding _) (Symbol _) = GT
1388 symCompare (Binding b1) (Binding b2) = compare b1 b2
1389 symCompare (Binding _) _ = LT
1390 symCompare (Expr _) (Keyword _) = GT
1391 symCompare (Expr _) (Symbol _) = GT
1392 symCompare (Expr _) (Binding _) = GT
1393 symCompare (Expr e1) (Expr e2) = compare e1 e2
1394 symCompare (Expr _) _ = LT
1395 symCompare (SimpleExpr _) (Keyword _) = GT
1396 symCompare (SimpleExpr _) (Symbol _) = GT
1397 symCompare (SimpleExpr _) (Binding _) = GT
1398 symCompare (SimpleExpr _) (Expr _) = GT
1399 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1401initDSL = DSL (PRef f [] (sUN ">>="))
1402 (PRef f [] (sUN "return"))
1403 (PRef f [] (sUN "<*>"))
1404 (PRef f [] (sUN "pure"))
1411 where f = fileFC "(builtin)"
1413data Using = UImplicit Name PTerm
1414 | UConstraint Name [Name]
1415 deriving (Show, Eq, Data, Typeable)
1417deriving instance Binary Using
1418deriving instance NFData Using
1421data SyntaxInfo = Syn { using :: [Using],
1422 syn_params :: [(Name, PTerm)],
1423 syn_namespace :: [String],
1425 imp_methods :: [Name], -- class methods. When expanding
1426 -- implicits, these should be expanded even under
1428 decoration :: Name -> Name,
1430 implicitAllowed :: Bool,
1431 maxline :: Maybe Int,
1434 syn_in_quasiquote :: Int }
1437deriving instance NFData SyntaxInfo
1438deriving instance Binary SyntaxInfo
1441defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1443expandNS :: SyntaxInfo -> Name -> Name
1444expandNS syn n@(NS _ _) = n
1445expandNS syn n = case syn_namespace syn of
1450-- For inferring types of things
1452bi = fileFC "builtin"
1454inferTy = sMN 0 "__Infer"
1455inferCon = sMN 0 "__infer"
1456inferDecl = PDatadecl inferTy NoFC
1458 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1459 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1460 (PRef bi [] inferTy)), bi, [])]
1463infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1464infP = P (TCon 6 0) inferTy (TType (UVal 0))
1466getInferTerm, getInferType :: Term -> Term
1467getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1468getInferTerm (App _ (App _ _ _) tm) = tm
1469getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1471getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1472 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1473 toTy (PVar t) = PVTy t
1475getInferType (App _ (App _ _ ty) _) = ty
1479-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1481primNames = [inferTy, inferCon]
1484unitCon = sUN "MkUnit"
1486falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1487 "The empty type, also known as the trivially false proposition." ++
1489 "Use `void` or `absurd` to prove anything if you have a variable " ++
1490 "of type `Void` in scope."
1493pairTy = sNS (sUN "Pair") ["Builtins"]
1494pairCon = sNS (sUN "MkPair") ["Builtins"]
1496upairTy = sNS (sUN "UPair") ["Builtins"]
1497upairCon = sNS (sUN "MkUPair") ["Builtins"]
1501eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1502 "The propositional equality type. A proof that `x` = `y`." ++
1504 "To use such a proof, pattern-match on it, and the two equal things will " ++
1505 "then need to be the _same_ pattern." ++
1507 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1508 "is possible to state equalities between values of potentially different " ++
1509 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1511 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1513eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1514 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1516 [(reflDoc, reflParamDoc,
1517 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1518 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1519 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1520 pimp (n "B") Placeholder False,
1521 pexp (PRef bi [] (n "x")),
1522 pexp (PRef bi [] (n "x"))])), bi, [])]
1524 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1525 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1526 "shown that both sides are in fact equal."
1527 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1528 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1530eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1531 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1537-- | The special name to be used in the module documentation context -
1538-- not for use in the main definition context. The namespace around it
1539-- will determine the module to which the docs adhere.
1541modDocName = sMN 0 "ModuleDocs"
1543-- Defined in builtins.idr
1544sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1545sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1547piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1548piBind = piBindp expl
1550piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1552piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1555-- Pretty-printing declarations and terms
1557-- These "show" instances render to an absurdly wide screen because inserted line breaks
1558-- could interfere with interactive editing, which calls "show".
1560instance Show PTerm where
1561 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1563instance Show PDecl where
1564 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1566instance Show PClause where
1567 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1569instance Show PData where
1570 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1572instance Pretty PTerm OutputAnnotation where
1573 pretty = prettyImp defaultPPOption
1575-- | Colourise annotations according to an Idris state. It ignores the names
1576-- in the annotation, as there's no good way to show extended information on a
1578consoleDecorate :: IState -> OutputAnnotation -> String -> String
1579consoleDecorate ist _ | not (idris_colourRepl ist) = id
1580consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1582 then colouriseType theme
1583 else colouriseData theme
1584consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1585consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1586consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1587consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1588consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1589consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1590 theme = idris_colourTheme ist
1592 _ | isDConName n ctxt -> colouriseData theme
1593 _ | isFnName n ctxt -> colouriseFun theme
1594 _ | isTConName n ctxt -> colouriseType theme
1595 _ | isPostulateName n ist -> colourisePostulate theme
1596 _ | otherwise -> id -- don't colourise unknown names
1597consoleDecorate ist (AnnFC _) = id
1598consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1599 where colour BoldText = IdrisColour Nothing True False True False
1600 colour UnderlineText = IdrisColour Nothing True True False False
1601 colour ItalicText = IdrisColour Nothing True False False True
1602consoleDecorate ist (AnnTerm _ _) = id
1603consoleDecorate ist (AnnSearchResult _) = id
1604consoleDecorate ist (AnnErr _) = id
1605consoleDecorate ist (AnnNamespace _ _) = id
1606consoleDecorate ist (AnnLink url) =
1607 \txt -> Idris.Colours.colourise (IdrisColour Nothing True True False False) txt ++ " (" ++ url ++ ")"
1609isPostulateName :: Name -> IState -> Bool
1610isPostulateName n ist = S.member n (idris_postulates ist)
1612-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1613prettyImp :: PPOption -- ^^ pretty printing options
1614 -> PTerm -- ^^ the term to pretty-print
1615 -> Doc OutputAnnotation
1616prettyImp impl = pprintPTerm impl [] [] []
1618-- | Serialise something to base64 using its Binary instance.
1620-- | Do the right thing for rendering a term in an IState
1621prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1622prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1624-- | Pretty-print a high-level Idris term in some bindings context with infix info
1625pprintPTerm :: PPOption -- ^^ pretty printing options
1626 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1627 -> [Name] -- ^^ names to always show in pi, even if not used
1628 -> [FixDecl] -- ^^ Fixity declarations
1629 -> PTerm -- ^^ the term to pretty-print
1630 -> Doc OutputAnnotation
1631pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1636 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1637 prettySe d p bnd (PQuote r) =
1638 text "![" <> pretty r <> text "]"
1639 prettySe d p bnd (PPatvar fc n) = pretty n
1641 | Just str <- slist d p bnd e = depth d $ str
1642 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1643 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1644 prettySe d p bnd (PLam fc n nfc ty sc) =
1645 depth d . bracket p startPrec . group . align . hang 2 $
1646 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1647 prettySe (decD d) startPrec ((n, False):bnd) sc
1648 prettySe d p bnd (PLet fc n nfc ty v sc) =
1649 depth d . bracket p startPrec . group . align $
1650 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1651 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1652 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1653 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs
1654 || ppopt_pinames ppo && uname n =
1655 depth d . bracket p startPrec . group $
1656 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1657 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1659 depth d . bracket p startPrec . group $
1660 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1661 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1663 uname (UN n) = case str n of
1670 Static -> text "[static]" <> space
1672 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1674 depth d . bracket p startPrec $
1675 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1676 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1677 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1681 Static -> text "[static]" <> space
1683 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1684 depth d . bracket p startPrec $
1685 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1686 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
1687 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1688 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1689 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1690 depth d . bracket p startPrec $
1691 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1692 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1693 -- This case preserves the behavior of the former constructor PEq.
1694 -- It should be removed if feasible when the pretty-printing of infix
1695 -- operators in general is improved.
1696 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1697 | n == eqTy, ppopt_impl ppo =
1698 depth d . bracket p eqPrec $
1699 enclose lparen rparen eq <+>
1700 align (group (vsep (map (prettyArgS (decD d) bnd)
1703 depth d . bracket p eqPrec . align . group $
1704 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1705 where eq = annName eqTy (text "=")
1707 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1708 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1709 | UN nm <- basename f
1710 , not (ppopt_impl ppo) && null (getShowArgs args) =
1711 prettyName True (ppopt_impl ppo) bnd f
1712 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1713 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1714 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1715 | UN nm <- basename op
1717 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1718 case getShowArgs args of
1720 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1721 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1722 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1723 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1724 depth d . bracket p funcAppPrec $
1725 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1726 align (group (vsep (map (prettyArgS d bnd) rest)))
1727 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1728 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1729 f = getFixity (opStr op)
1731 Nothing -> funcAppPrec + 1
1732 Just (Infixl p') -> p'
1733 Just f' -> prec f' + 1
1735 Nothing -> funcAppPrec + 1
1736 Just (Infixr p') -> p'
1737 Just f' -> prec f' + 1
1738 inFix l r = align . group $
1739 (prettySe (decD d) left bnd l <+> opName False) <$>
1740 group (prettySe (decD d) right bnd r)
1741 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1742 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1743 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1744 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1745 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1746 let args = getShowArgs as
1747 fp = prettySe (decD d) (startPrec + 1) bnd f
1748 shownArgs = if ppopt_impl ppo then as else args
1750 depth d . bracket p funcAppPrec . group $
1753 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1754 prettySe d p bnd (PCase _ scr cases) =
1755 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1756 depth d (indent 2 (vsep (map ppcase cases)))
1758 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1759 ([(n, False) | n <- vars l] ++ bnd)
1760 in nest nestingSize $
1761 prettyCase l <+> text "=>" <+> prettyCase r
1762 -- Warning: this is a bit of a hack. At this stage, we don't have the
1763 -- global context, so we can't determine which names are constructors,
1764 -- which are types, and which are pattern variables on the LHS of the
1765 -- case pattern. We use the heuristic that names without a namespace
1766 -- are patvars, because right now case blocks in PTerms are always
1767 -- delaborated from TT before being sent to the pretty-printer. If they
1768 -- start getting printed directly, THIS WILL BREAK.
1769 -- Potential solution: add a list of known patvars to the cases in
1770 -- PCase, and have the delaborator fill it out, kind of like the pun
1771 -- disambiguation on PDPair.
1772 vars tm = filter noNS (allNamesIn tm)
1773 noNS (NS _ _) = False
1776 prettySe d p bnd (PIfThenElse _ c t f) =
1777 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1778 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1779 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1780 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1782 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1783 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1784 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1785 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1786 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1787 prettySe d p bnd (PRewrite _ l r _) =
1788 depth d . bracket p startPrec $
1789 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1790 prettySe d p bnd (PTyped l r) =
1791 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1792 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1793 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1794 align . group . vsep . punctuate (ann comma) $
1795 map (prettySe (decD d) startPrec bnd) elts
1796 where ann = case pun of
1798 IsType -> annName pairTy
1799 IsTerm -> annName pairCon
1800 prettySe d p bnd (PDPair _ _ pun l t r) =
1804 annotated (text "**") <+>
1805 prettySe (decD d) startPrec (addBinding bnd) r <>
1807 where annotated = case pun of
1808 IsType -> annName sigmaTy
1809 IsTerm -> annName sigmaCon
1811 (left, addBinding) = case (l, pun) of
1812 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1813 _ -> (prettySe (decD d) startPrec bnd l, id)
1814 prettySe d p bnd (PAlternative ns a as) =
1815 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1818 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1819 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1820 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1821 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1822 -- XXX: add pretty for tactics
1823 prettySe d p bnd (PProof ts) =
1824 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1825 prettySe d p bnd (PTactics ts) =
1826 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1827 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1828 prettySe d p bnd (PReturn f) = kwd "return"
1829 prettySe d p bnd PImpossible = kwd "impossible"
1830 prettySe d p bnd Placeholder = text "_"
1831 prettySe d p bnd (PDoBlock dos) =
1832 bracket p startPrec $
1833 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1834 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1835 ppdo bnd (DoBind _ bn _ tm : dos) =
1836 (prettyBindingOf bn False <+> text "<-" <+>
1837 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1838 ppdo ((bn, False):bnd) dos
1839 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1840 text "no pretty printer for pattern-matching do binding" :
1842 ppdo bnd (DoLet _ ln _ ty v : dos) =
1843 (kwd "let" <+> prettyBindingOf ln False <+>
1844 (if ty /= Placeholder
1845 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1847 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1848 ppdo ((ln, False):bnd) dos
1849 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1850 text "no pretty printer for pattern-matching do binding" :
1853 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1854 prettySe d p bnd (PElabError s) = pretty s
1855 -- Quasiquote pprinting ignores bound vars
1856 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1857 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1858 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1859 prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1860 prettySe d p bnd (PRunElab _ tm _) =
1861 bracket p funcAppPrec . group . align . hang 2 $
1863 prettySe (decD d) funcAppPrec bnd tm
1864 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1866 prettySe d p bnd _ = text "missing pretty-printer for term"
1868 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1869 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1870 where display (UN n) = T.unpack n
1871 display (MN _ n) = T.unpack n
1872 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1873 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1876 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1877 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1878 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1879 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1881 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1882 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1883 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1884 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1886 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1887 annName n = annotate (AnnName n Nothing Nothing Nothing)
1889 opStr :: Name -> String
1890 opStr (NS n _) = opStr n
1891 opStr (UN n) = T.unpack n
1893 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1894 slist' (Just d) _ _ _ | d <= 0 = Nothing
1896 | containsHole e = Nothing
1897 slist' d p bnd (PApp _ (PRef _ _ nil) _)
1898 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1899 slist' d p bnd (PRef _ _ nil)
1900 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1901 slist' d p bnd (PApp _ (PRef _ _ cons) args)
1902 | nsroot cons == sUN "::",
1903 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1905 Just tl' <- slist' (decD d) p bnd tl
1906 = Just (prettySe d startPrec bnd hd : tl')
1908 isImp (PImp {}) = True
1910 slist' _ _ _ tm = Nothing
1912 slist d p bnd e | Just es <- slist' d p bnd e = Just $
1914 [] -> annotate (AnnData "" "") $ text "[]"
1915 [x] -> enclose left right . group $ x
1916 xs -> enclose left right .
1917 align . group . vsep .
1918 punctuate comma $ xs
1919 where left = (annotate (AnnData "" "") (text "["))
1920 right = (annotate (AnnData "" "") (text "]"))
1921 comma = (annotate (AnnData "" "") (text ","))
1922 slist _ _ _ _ = Nothing
1924 pairElts :: PTerm -> Maybe [PTerm]
1925 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1926 | otherwise = Just [x, y]
1927 pairElts _ = Nothing
1929 natns = "Prelude.Nat."
1931 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1932 snat (Just x) _ _ | x <= 0 = Nothing
1933 snat d p (PRef _ _ z)
1934 | show z == (natns++"Z") || show z == "Z" = Just 0
1935 snat d p (PApp _ s [PExp {getTm=n}])
1936 | show s == (natns++"S") || show s == "S",
1937 Just n' <- snat (decD d) p n
1939 snat _ _ _ = Nothing
1941 bracket outer inner doc
1942 | outer > inner = lparen <> doc <> rparen
1945 ellipsis = text "..."
1948 depth (Just d) = if d <= 0 then const (ellipsis) else id
1950 decD = fmap (\x -> x - 1)
1952 kwd = annotate AnnKeyword . text
1954 fixities :: M.Map String Fixity
1955 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1957 getFixity :: String -> Maybe Fixity
1958 getFixity = flip M.lookup fixities
1960-- | Strip away namespace information
1961basename :: Name -> Name
1962basename (NS n _) = basename n
1965-- | Determine whether a name was the one inserted for a hole or
1966-- guess by the delaborator
1967isHoleName :: Name -> Bool
1968isHoleName (UN n) = n == T.pack "[__]"
1971-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1972containsHole :: PTerm -> Bool
1973containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
1975-- | Pretty-printer helper for names that attaches the correct annotations
1977 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1978 -> Bool -- ^^ whether to show namespaces
1979 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1980 -> Name -- ^^ the name to pprint
1981 -> Doc OutputAnnotation
1982prettyName infixParen showNS bnd n
1983 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1984 | (UN n') <- n, T.unpack n' == "_" = text "_"
1985 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1986 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1987 where fullName = text nameSpace <> parenthesise (text (baseName n))
1988 baseName (UN n) = T.unpack n
1989 baseName (NS n ns) = baseName n
1990 baseName (MN i s) = T.unpack s
1991 baseName other = show other
1992 nameSpace = case n of
1993 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1995 isInfix = case baseName n of
1997 (c : _) -> not (isAlpha c)
1998 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
2001showCImp :: PPOption -> PClause -> Doc OutputAnnotation
2002showCImp ppo (PClause _ n l ws r w)
2003 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
2004 <+> text "where" <+> text (show w)
2007 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2008showCImp ppo (PWith _ n l ws r pn w)
2009 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
2010 <+> braces (text (show w))
2013 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
2016showDImp :: PPOption -> PData -> Doc OutputAnnotation
2017showDImp ppo (PDatadecl n nfc ty cons)
2018 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
2019 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
2021showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
2022showDecls o ds = vsep (map (showDeclImp o) ds)
2024showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
2025showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
2026showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
2027 indent 2 (vsep (map (showCImp o) cs))
2028showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
2029showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
2030showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
2031showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
2032showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
2033 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
2034showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
2035 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
2036showDeclImp _ _ = text "..."
2037-- showDeclImp (PImport o) = "import " ++ o
2039getImps :: [PArg] -> [(Name, PTerm)]
2041getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
2042getImps (_ : xs) = getImps xs
2044getExps :: [PArg] -> [PTerm]
2046getExps (PExp _ _ _ tm : xs) = tm : getExps xs
2047getExps (_ : xs) = getExps xs
2049getShowArgs :: [PArg] -> [PArg]
2051getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
2052getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
2053 | PImp _ _ _ _ tm <- e
2054 , containsHole tm = e : getShowArgs xs
2055getShowArgs (_ : xs) = getShowArgs xs
2057getConsts :: [PArg] -> [PTerm]
2059getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
2060getConsts (_ : xs) = getConsts xs
2062getAll :: [PArg] -> [PTerm]
2067showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
2068 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
2069 -> PPOption -- ^^ pretty printing options
2070 -> Bool -- ^^ whether to colourise
2071 -> Name -- ^^ the term to show
2073showName ist bnd ppo colour n = case ist of
2074 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
2075 Nothing -> showbasic n
2076 where name = if ppopt_impl ppo then show n else showbasic n
2077 showbasic n@(UN _) = showCG n
2078 showbasic (MN i s) = str s
2079 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
2080 showbasic (SN s) = show s
2082 colourise n t = let ctxt' = fmap tt_ctxt ist in
2085 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2086 else colouriseBound t name
2087 | isDConName n ctxt -> colouriseData t name
2088 | isFnName n ctxt -> colouriseFun t name
2089 | isTConName n ctxt -> colouriseType t name
2090 -- The assumption is that if a name is not bound and does not exist in the
2091 -- global context, then we're somewhere in which implicit info has been lost
2092 -- (like error messages). Thus, unknown vars are colourised as implicits.
2093 | otherwise -> colouriseImplicit t name
2095showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
2096 -> PTerm -- ^^ the term to show
2098showTm ist = displayDecorated (consoleDecorate ist) .
2099 renderPretty 0.8 100000 .
2100 prettyImp (ppOptionIst ist)
2102-- | Show a term with implicits, no colours
2103showTmImpls :: PTerm -> String
2104showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2106-- | Show a term with specific options
2107showTmOpts :: PPOption -> PTerm -> String
2108showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2111instance Sized PTerm where
2112 size (PQuote rawTerm) = size rawTerm
2113 size (PRef fc _ name) = size name
2114 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2115 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2116 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2117 size (PTyped trm ty) = 1 + size trm + size ty
2118 size (PApp fc name args) = 1 + size args
2119 size (PAppBind fc name args) = 1 + size args
2120 size (PCase fc trm bdy) = 1 + size trm + size bdy
2121 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2122 size (PTrue fc _) = 1
2123 size (PResolveTC fc) = 1
2124 size (PRewrite fc left right _) = 1 + size left + size right
2125 size (PPair fc _ _ left right) = 1 + size left + size right
2126 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2127 size (PAlternative _ a alts) = 1 + size alts
2128 size (PHidden hidden) = size hidden
2129 size (PUnifyLog tm) = size tm
2130 size (PDisamb _ tm) = size tm
2131 size (PNoImplicits tm) = size tm
2133 size (PUniverse _) = 1
2134 size (PConstant fc const) = 1 + size fc + size const
2135 size Placeholder = 1
2136 size (PDoBlock dos) = 1 + size dos
2137 size (PIdiom fc term) = 1 + size term
2138 size (PReturn fc) = 1
2139 size (PMetavar _ name) = 1
2140 size (PProof tactics) = size tactics
2141 size (PElabError err) = size err
2142 size PImpossible = 1
2145getPArity :: PTerm -> Int
2146getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2149-- Return all names, free or globally bound, in the given term.
2151allNamesIn :: PTerm -> [Name]
2152allNamesIn tm = nub $ ni [] tm
2153 where -- TODO THINK added niTacImp, but is it right?
2155 | not (n `elem` env) = [n]
2156 ni env (PPatvar _ n) = [n]
2157 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2158 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2159 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2160 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
2161 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2162 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2163 ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc
2164 ni env (PHidden tm) = ni env tm
2165 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2166 ni env (PTyped l r) = ni env l ++ ni env r
2167 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2168 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r
2169 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2170 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2171 ni env (PAlternative ns a ls) = concatMap (ni env) ls
2172 ni env (PUnifyLog tm) = ni env tm
2173 ni env (PDisamb _ tm) = ni env tm
2174 ni env (PNoImplicits tm) = ni env tm
2177 niTacImp env (TacImp _ _ scr) = ni env scr
2181-- Return all names defined in binders in the given term
2182boundNamesIn :: PTerm -> [Name]
2183boundNamesIn tm = S.toList (ni S.empty tm)
2184 where -- TODO THINK Added niTacImp, but is it right?
2185 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
2186 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
2187 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
2188 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
2189 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
2190 ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
2191 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
2192 ni set (PRewrite _ l r _) = ni (ni set l) r
2193 ni set (PTyped l r) = ni (ni set l) r
2194 ni set (PPair _ _ _ l r) = ni (ni set l) r
2195 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r
2196 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r
2197 ni set (PAlternative ns a as) = niTms set as
2198 ni set (PHidden tm) = ni set tm
2199 ni set (PUnifyLog tm) = ni set tm
2200 ni set (PDisamb _ tm) = ni set tm
2201 ni set (PNoImplicits tm) = ni set tm
2205 niTms set (x : xs) = niTms (ni set x) xs
2207 niTacImp set (TacImp _ _ scr) = ni set scr
2208 niTacImp set _ = set
2210-- Return names which are valid implicits in the given term (type).
2211implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2212implicitNamesIn uvars ist tm = nub $ ni [] tm
2215 | not (n `elem` env)
2216 = case lookupTy n (tt_ctxt ist) of
2218 _ -> if n `elem` uvars then [n] else []
2219 ni env (PApp _ f@(PRef _ _ n) as)
2220 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
2221 | otherwise = concatMap (ni env) (map getTm as)
2222 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2223 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2224 ni env (PCase _ c os) = ni env c ++
2225 -- names in 'os', not counting the names bound in the cases
2226 (nub (concatMap (ni env) (map snd os))
2227 \\ nub (concatMap (ni env) (map fst os)))
2228 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2229 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2230 ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
2231 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2232 ni env (PTyped l r) = ni env l ++ ni env r
2233 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2234 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2235 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2236 ni env (PAlternative ns a as) = concatMap (ni env) as
2237 ni env (PHidden tm) = ni env tm
2238 ni env (PUnifyLog tm) = ni env tm
2239 ni env (PDisamb _ tm) = ni env tm
2240 ni env (PNoImplicits tm) = ni env tm
2243-- Return names which are free in the given term.
2244namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2245namesIn uvars ist tm = nub $ ni [] tm
2248 | not (n `elem` env)
2249 = case lookupTy n (tt_ctxt ist) of
2251 _ -> if n `elem` (map fst uvars) then [n] else []
2252 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2253 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2254 ni env (PCase _ c os) = ni env c ++
2255 -- names in 'os', not counting the names bound in the cases
2256 (nub (concatMap (ni env) (map snd os))
2257 \\ nub (concatMap (ni env) (map fst os)))
2258 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2259 ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2260 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2261 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2262 ni env (PTyped l r) = ni env l ++ ni env r
2263 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2264 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2265 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2266 ni env (PAlternative ns a as) = concatMap (ni env) as
2267 ni env (PHidden tm) = ni env tm
2268 ni env (PUnifyLog tm) = ni env tm
2269 ni env (PDisamb _ tm) = ni env tm
2270 ni env (PNoImplicits tm) = ni env tm
2273 niTacImp env (TacImp _ _ scr) = ni env scr
2276-- Return which of the given names are used in the given term.
2278usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2279usedNamesIn vars ist tm = nub $ ni [] tm
2280 where -- TODO THINK added niTacImp, but is it right?
2282 | n `elem` vars && not (n `elem` env)
2283 = case lookupDefExact n (tt_ctxt ist) of
2286 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2287 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2288 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2289 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2290 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2291 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2292 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2293 ni env (PTyped l r) = ni env l ++ ni env r
2294 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2295 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2296 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2297 ni env (PAlternative ns a as) = concatMap (ni env) as
2298 ni env (PHidden tm) = ni env tm
2299 ni env (PUnifyLog tm) = ni env tm
2300 ni env (PDisamb _ tm) = ni env tm
2301 ni env (PNoImplicits tm) = ni env tm
2304 niTacImp env (TacImp _ _ scr) = ni env scr
2307-- Return the list of inaccessible (= dotted) positions for a name.
2308getErasureInfo :: IState -> Name -> [Int]
2309getErasureInfo ist n =
2310 case lookupCtxtExact n (idris_optimisation ist) of
2311 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