git.iko.soy/Idris-dev
on aef8dc1 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1912 lines 78 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.Docstrings
11import IRTS.Lang
12import IRTS.CodegenCommon
13import Util.Pretty
14import Util.DynamicLinker
16import Idris.Colours
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.Trans.State.Strict
22import Control.Monad.Trans.Except
24import Data.Data (Data)
25import Data.Function (on)
26import Data.List hiding (group)
27import Data.Char
28import qualified Data.Map.Strict as M
29import qualified Data.Text as T
30import Data.Either
31import qualified Data.Set as S
32import Data.Word (Word)
33import Data.Maybe (fromMaybe, mapMaybe)
34import Data.Traversable (Traversable)
35import Data.Typeable
36import Data.Foldable (Foldable)
38import Debug.Trace
40import Text.PrettyPrint.Annotated.Leijen
42data ElabWhat = ETypes | EDefns | EAll
43 deriving (Show, Eq)
45-- Data to pass to recursively called elaborators; e.g. for where blocks,
46-- paramaterised declarations, etc.
48-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
49-- so that we can have mutually recursive elaborators in separate modules without
50-- having to muck about with cyclic modules.
51data ElabInfo = EInfo { params :: [(Name, PTerm)],
52 inblock :: Ctxt [Name], -- names in the block, and their params
53 liftname :: Name -> Name,
54 namespace :: Maybe [String],
55 elabFC :: Maybe FC,
56 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
57 Idris () }
59toplevel :: ElabInfo
60toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not implemented")
62eInfoNames :: ElabInfo -> [Name]
63eInfoNames info = map fst (params info) ++ M.keys (inblock info)
65data IOption = IOption { opt_logLevel :: Int,
66 opt_typecase :: Bool,
67 opt_typeintype :: Bool,
68 opt_coverage :: Bool,
69 opt_showimp :: Bool, -- ^^ show implicits
70 opt_errContext :: Bool,
71 opt_repl :: Bool,
72 opt_verbose :: Bool,
73 opt_nobanner :: Bool,
74 opt_quiet :: Bool,
75 opt_codegen :: Codegen,
76 opt_outputTy :: OutputType,
77 opt_ibcsubdir :: FilePath,
78 opt_importdirs :: [FilePath],
79 opt_triple :: String,
80 opt_cpu :: String,
81 opt_cmdline :: [Opt], -- remember whole command line
82 opt_origerr :: Bool,
83 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
84 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
85 opt_optimise :: [Optimisation]
86 }
87 deriving (Show, Eq)
89defaultOpts = IOption { opt_logLevel = 0
90 , opt_typecase = False
91 , opt_typeintype = False
92 , opt_coverage = True
93 , opt_showimp = False
94 , opt_errContext = False
95 , opt_repl = True
96 , opt_verbose = True
97 , opt_nobanner = False
98 , opt_quiet = False
99 , opt_codegen = Via "c"
100 , opt_outputTy = Executable
101 , opt_ibcsubdir = ""
102 , opt_importdirs = []
103 , opt_triple = ""
104 , opt_cpu = ""
105 , opt_cmdline = []
106 , opt_origerr = False
107 , opt_autoSolve = True
108 , opt_autoImport = []
109 , opt_optimise = defaultOptimise
110 }
112data PPOption = PPOption {
113 ppopt_impl :: Bool -- ^^ whether to show implicits
114} deriving (Show)
116data Optimisation = PETransform -- partial eval and associated transforms
117 deriving (Show, Eq)
119defaultOptimise = [PETransform]
121-- | Pretty printing options with default verbosity.
122defaultPPOption :: PPOption
123defaultPPOption = PPOption { ppopt_impl = False }
125-- | Pretty printing options with the most verbosity.
126verbosePPOption :: PPOption
127verbosePPOption = PPOption { ppopt_impl = True }
129-- | Get pretty printing options from the big options record.
130ppOption :: IOption -> PPOption
131ppOption opt = PPOption {
132 ppopt_impl = opt_showimp opt
135-- | Get pretty printing options from an idris state record.
136ppOptionIst :: IState -> PPOption
137ppOptionIst = ppOption . idris_options
139data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
141-- | The output mode in use
142data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
143 | IdeSlave Integer Handle -- ^ Send IDE output for some request ID to the handle
144 deriving Show
146-- | How wide is the console?
147data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
148 | ColsWide Int -- ^ Manually specified - must be positive
149 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
151-- | The global state used in the Idris monad
152data IState = IState {
153 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
154 idris_constraints :: [(UConstraint, FC)],
155 -- ^ A list of universe constraints and their corresponding source locations
156 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
157 idris_implicits :: Ctxt [PArg],
158 idris_statics :: Ctxt [Bool],
159 idris_classes :: Ctxt ClassInfo,
160 idris_dsls :: Ctxt DSL,
161 idris_optimisation :: Ctxt OptInfo,
162 idris_datatypes :: Ctxt TypeInfo,
163 idris_namehints :: Ctxt [Name],
164 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
165 -- ^ list of lhs/rhs, and a list of missing clauses
166 idris_flags :: Ctxt [FnOpt],
167 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
168 idris_calledgraph :: Ctxt [Name],
169 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
170 idris_moduledocs :: Ctxt (Docstring DocTerm),
171 -- ^ module documentation is saved in a special MN so the context
172 -- mechanism can be used for disambiguation
173 idris_tyinfodata :: Ctxt TIData,
174 idris_fninfo :: Ctxt FnInfo,
175 idris_transforms :: Ctxt [(Term, Term)],
176 idris_totcheck :: [(FC, Name)], -- names to check totality on
177 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
178 idris_totcheckfail :: [(FC, String)],
179 idris_options :: IOption,
180 idris_name :: Int,
181 idris_lineapps :: [((FilePath, Int), PTerm)],
182 -- ^ Full application LHS on source line
183 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
184 idris_coercions :: [Name],
185 idris_errRev :: [(Term, Term)],
186 syntax_rules :: SyntaxRules,
187 syntax_keywords :: [String],
188 imported :: [FilePath], -- ^ The imported modules
189 idris_scprims :: [(Name, (Int, PrimFn))],
190 idris_objs :: [(Codegen, FilePath)],
191 idris_libs :: [(Codegen, String)],
192 idris_cgflags :: [(Codegen, String)],
193 idris_hdrs :: [(Codegen, String)],
194 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
195 proof_list :: [(Name, [String])],
196 errSpan :: Maybe FC,
197 parserWarnings :: [(FC, Err)],
198 lastParse :: Maybe Name,
199 indent_stack :: [Int],
200 brace_stack :: [Maybe Int],
201 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
202 idris_parsedSpan :: Maybe FC,
203 hide_list :: [(Name, Maybe Accessibility)],
204 default_access :: Accessibility,
205 default_total :: Bool,
206 ibc_write :: [IBCWrite],
207 compiled_so :: Maybe String,
208 idris_dynamic_libs :: [DynamicLib],
209 idris_language_extensions :: [LanguageExt],
210 idris_outputmode :: OutputMode,
211 idris_colourRepl :: Bool,
212 idris_colourTheme :: ColourTheme,
213 idris_errorhandlers :: [Name], -- ^ Global error handlers
214 idris_nameIdx :: (Int, Ctxt (Int, Name)),
215 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
216 module_aliases :: M.Map [T.Text] [T.Text],
217 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
218 idris_postulates :: S.Set Name,
219 idris_whocalls :: Maybe (M.Map Name [Name]),
220 idris_callswho :: Maybe (M.Map Name [Name]),
221 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
222 elab_stack :: [Name], -- ^ Stack of names currently being elaborated
223 idris_symbols :: M.Map Name Name -- ^ Symbol table (preserves sharing of names)
224 }
226-- Required for parsers library, and therefore trifecta
227instance Show IState where
228 show = const "{internal state}"
230data SizeChange = Smaller | Same | Bigger | Unknown
231 deriving (Show, Eq)
232{-!
233deriving instance Binary SizeChange
234deriving instance NFData SizeChange
235!-}
237type SCGEntry = (Name, [Maybe (Int, SizeChange)])
238type UsageReason = (Name, Int) -- fn_name, its_arg_number
240data CGInfo = CGInfo { argsdef :: [Name],
241 calls :: [(Name, [[Name]])],
242 scg :: [SCGEntry],
243 argsused :: [Name],
244 usedpos :: [(Int, [UsageReason])] }
245 deriving Show
246{-!
247deriving instance Binary CGInfo
248deriving instance NFData CGInfo
249!-}
251primDefs = [sUN "unsafePerformPrimIO",
252 sUN "mkLazyForeignPrim",
253 sUN "mkForeignPrim",
254 sUN "void"]
256-- information that needs writing for the current module's .ibc file
257data IBCWrite = IBCFix FixDecl
258 | IBCImp Name
259 | IBCStatic Name
260 | IBCClass Name
261 | IBCInstance Bool Name Name
262 | IBCDSL Name
263 | IBCData Name
264 | IBCOpt Name
265 | IBCMetavar Name
266 | IBCSyntax Syntax
267 | IBCKeyword String
268 | IBCImport (Bool, FilePath) -- True = import public
269 | IBCImportDir FilePath
270 | IBCObj Codegen FilePath
271 | IBCLib Codegen String
272 | IBCCGFlag Codegen String
273 | IBCDyLib String
274 | IBCHeader Codegen String
275 | IBCAccess Name Accessibility
276 | IBCMetaInformation Name MetaInformation
277 | IBCTotal Name Totality
278 | IBCFlags Name [FnOpt]
279 | IBCFnInfo Name FnInfo
280 | IBCTrans Name (Term, Term)
281 | IBCErrRev (Term, Term)
282 | IBCCG Name
283 | IBCDoc Name
284 | IBCCoercion Name
285 | IBCDef Name -- i.e. main context
286 | IBCNameHint (Name, Name)
287 | IBCLineApp FilePath Int PTerm
288 | IBCErrorHandler Name
289 | IBCFunctionErrorHandler Name Name Name
290 | IBCPostulate Name
291 | IBCTotCheckErr FC String
292 | IBCParsedRegion FC
293 | IBCModDocs Name -- ^ The name is the special name used to track module docs
294 deriving Show
296-- | The initial state for the compiler
297idrisInit :: IState
298idrisInit = IState initContext [] []
299 emptyContext emptyContext emptyContext emptyContext
300 emptyContext emptyContext emptyContext emptyContext
301 emptyContext emptyContext emptyContext emptyContext
302 emptyContext emptyContext emptyContext emptyContext
303 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
304 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
305 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
306 AutomaticWidth S.empty Nothing Nothing [] [] M.empty
308-- | The monad for the main REPL - reading and processing files and updating
309-- global state (hence the IO inner monad).
310--type Idris = WriterT [Either String (IO ())] (State IState a))
311type Idris = StateT IState (ExceptT Err IO)
313-- Commands in the REPL
315data Codegen = Via String
316-- | ViaC
317-- | ViaJava
318-- | ViaNode
319-- | ViaJavaScript
320-- | ViaLLVM
321 | Bytecode
322 deriving (Show, Eq)
323{-!
324deriving instance NFData Codegen
325!-}
327-- | REPL commands
328data Command = Quit
329 | Help
330 | Eval PTerm
331 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
332 | Undefine [Name]
333 | Check PTerm
334 | DocStr (Either Name Const)
335 | TotCheck Name
336 | Reload
337 | Load FilePath (Maybe Int) -- up to maximum line number
338 | ChangeDirectory FilePath
339 | ModImport String
340 | Edit
341 | Compile Codegen String
342 | Execute
343 | ExecVal PTerm
344 | Metavars
345 | Prove Name
346 | AddProof (Maybe Name)
347 | RmProof Name
348 | ShowProof Name
349 | Proofs
350 | Universes
351 | LogLvl Int
352 | Spec PTerm
353 | HNF PTerm
354 | TestInline PTerm
355 | Defn Name
356 | Missing Name
357 | DynamicLink FilePath
358 | ListDynamic
359 | Pattelab PTerm
360 | Search [String] PTerm
361 | CaseSplitAt Bool Int Name
362 | AddClauseFrom Bool Int Name
363 | AddProofClauseFrom Bool Int Name
364 | AddMissing Bool Int Name
365 | MakeWith Bool Int Name
366 | MakeLemma Bool Int Name
367 | DoProofSearch Bool Bool Int Name [Name]
368 -- ^ the first bool is whether to update,
369 -- the second is whether to search recursively (i.e. for the arguments)
370 | SetOpt Opt
371 | UnsetOpt Opt
372 | NOP
373 | SetColour ColourType IdrisColour
374 | ColourOn
375 | ColourOff
376 | ListErrorHandlers
377 | SetConsoleWidth ConsoleWidth
378 | Apropos [String] String
379 | WhoCalls Name
380 | CallsWho Name
381 | MakeDoc String -- IdrisDoc
382 | Warranty
383 | PrintDef Name
384 | PPrint OutputFmt Int PTerm
385 | TransformInfo Name
386 -- Debugging commands
387 | DebugInfo Name
388 | DebugUnify PTerm PTerm
390data OutputFmt = HTMLOutput | LaTeXOutput
392data Opt = Filename String
393 | Quiet
394 | NoBanner
395 | ColourREPL Bool
396 | Ideslave
397 | IdeslaveSocket
398 | ShowLibs
399 | ShowLibdir
400 | ShowIncs
401 | ShowPkgs
402 | NoBasePkgs
403 | NoPrelude
404 | NoBuiltins -- only for the really primitive stuff!
405 | NoREPL
406 | OLogging Int
407 | Output String
408 | TypeCase
409 | TypeInType
410 | DefaultTotal
411 | DefaultPartial
412 | WarnPartial
413 | WarnReach
414 | NoCoverage
415 | ErrContext
416 | ShowImpl
417 | Verbose
418 | Port String -- REPL TCP port
419 | IBCSubDir String
420 | ImportDir String
421 | PkgBuild String
422 | PkgInstall String
423 | PkgClean String
424 | PkgCheck String
425 | PkgREPL String
426 | PkgMkDoc String -- IdrisDoc
427 | PkgTest String
428 | PkgIndex FilePath
429 | WarnOnly
430 | Pkg String
431 | BCAsm String
432 | DumpDefun String
433 | DumpCases String
434 | UseCodegen Codegen
435 | OutputTy OutputType
436 | Extension LanguageExt
437 | InterpretScript String
438 | EvalExpr String
439 | TargetTriple String
440 | TargetCPU String
441 | OptLevel Int
442 | AddOpt Optimisation
443 | RemoveOpt Optimisation
444 | Client String
445 | ShowOrigErr
446 | AutoWidth -- ^ Automatically adjust terminal width
447 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
448 deriving (Show, Eq)
450-- Parsed declarations
452data Fixity = Infixl { prec :: Int }
453 | Infixr { prec :: Int }
454 | InfixN { prec :: Int }
455 | PrefixN { prec :: Int }
456 deriving Eq
457{-!
458deriving instance Binary Fixity
459deriving instance NFData Fixity
460!-}
462instance Show Fixity where
463 show (Infixl i) = "infixl " ++ show i
464 show (Infixr i) = "infixr " ++ show i
465 show (InfixN i) = "infix " ++ show i
466 show (PrefixN i) = "prefix " ++ show i
468data FixDecl = Fix Fixity String
469 deriving Eq
471instance Show FixDecl where
472 show (Fix f s) = show f ++ " " ++ s
474{-!
475deriving instance Binary FixDecl
476deriving instance NFData FixDecl
477!-}
479instance Ord FixDecl where
480 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
483data Static = Static | Dynamic
484 deriving (Show, Eq, Data, Typeable)
485{-!
486deriving instance Binary Static
487deriving instance NFData Static
488!-}
490-- Mark bindings with their explicitness, and laziness
491data Plicity = Imp { pargopts :: [ArgOpt],
492 pstatic :: Static,
493 pparam :: Bool,
494 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
495 }
496 | Exp { pargopts :: [ArgOpt],
497 pstatic :: Static,
498 pparam :: Bool } -- this is a param (rather than index)
499 | Constraint { pargopts :: [ArgOpt],
500 pstatic :: Static }
501 | TacImp { pargopts :: [ArgOpt],
502 pstatic :: Static,
503 pscript :: PTerm }
504 deriving (Show, Eq, Data, Typeable)
506{-!
507deriving instance Binary Plicity
508deriving instance NFData Plicity
509!-}
511is_scoped :: Plicity -> Maybe ImplicitInfo
512is_scoped (Imp _ _ _ s) = s
513is_scoped _ = Nothing
515impl = Imp [] Dynamic False Nothing
516forall_imp = Imp [] Dynamic False (Just (Impl False))
517forall_constraint = Imp [] Dynamic False (Just (Impl True))
518expl = Exp [] Dynamic False
519expl_param = Exp [] Dynamic True
520constraint = Constraint [] Static
521tacimpl t = TacImp [] Dynamic t
523data FnOpt = Inlinable -- always evaluate when simplifying
524 | TotalFn | PartialFn | CoveringFn
525 | Coinductive | AssertTotal
526 | Dictionary -- type class dictionary, eval only when
527 -- a function argument, and further evaluation resutls
528 | Implicit -- implicit coercion
529 | NoImplicit -- do not apply implicit coercions
530 | CExport String -- export, with a C name
531 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
532 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
533 | Reflection -- a reflecting function, compile-time only
534 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
535 | Constructor -- Data constructor type
536 deriving (Show, Eq)
537{-!
538deriving instance Binary FnOpt
539deriving instance NFData FnOpt
540!-}
542type FnOpts = [FnOpt]
544inlinable :: FnOpts -> Bool
545inlinable = elem Inlinable
547dictionary :: FnOpts -> Bool
548dictionary = elem Dictionary
551-- | Data declaration options
552data DataOpt = Codata -- ^ Set if the the data-type is coinductive
553 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
554 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
555 | DataErrRev
556 deriving (Show, Eq)
558type DataOpts = [DataOpt]
560-- | Type provider - what to provide
561data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
562 | ProvPostulate t -- ^ goal type must be Type, so only term
563 deriving (Show, Eq, Functor)
565type ProvideWhat = ProvideWhat' PTerm
567-- | Top-level declarations such as compiler directives, definitions,
568-- datatypes and typeclasses.
569data PDecl' t
570 = PFix FC Fixity [String] -- ^ Fixity declaration
571 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
572 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
573 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
574 | PCAF FC Name t -- ^ Top level constant
575 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
576 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
577 | PNamespace String [PDecl' t] -- ^ New namespace
578 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
579 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
580 [(Name, t)] -- constraints
581 Name
582 [(Name, t)] -- parameters
583 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
584 [PDecl' t] -- declarations
585 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
586 -- class name, parameters, method declarations
587 | PInstance SyntaxInfo FC [(Name, t)] -- constraints
588 Name -- class
589 [t] -- parameters
590 t -- full instance type
591 (Maybe Name) -- explicit name
592 [PDecl' t]
593 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
594 -- class name, parameters, full instance type, optional explicit name, and definitions
595 | PDSL Name (DSL' t) -- ^ DSL declaration
596 | PSyntax FC Syntax -- ^ Syntax definition
597 | PMutual FC [PDecl' t] -- ^ Mutual block
598 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
599 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
600 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
601 -- bool is True, lhs and rhs must be convertible
602 deriving Functor
603{-!
604deriving instance Binary PDecl'
605deriving instance NFData PDecl'
606!-}
608-- For elaborator state
609data EState = EState {
610 case_decls :: [PDecl],
611 delayed_elab :: [Elab' EState ()]
612 }
614initEState = EState [] []
616type ElabD a = Elab' EState a
618-- | One clause of a top-level definition. Term arguments to constructors are:
619--
620-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
621--
622-- 2. The list of extra 'with' patterns
623--
624-- 3. The right-hand side
625--
626-- 4. The where block (PDecl' t)
628data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
629 | PWith FC Name t [t] t [PDecl' t]
630 | PClauseR FC [t] t [PDecl' t]
631 | PWithR FC [t] t [PDecl' t]
632 deriving Functor
633{-!
634deriving instance Binary PClause'
635deriving instance NFData PClause'
636!-}
638-- | Data declaration
639data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
640 d_tcon :: t, -- ^ Type constructor
641 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
642 }
643 -- ^ Data declaration
644 | PLaterdecl { d_name :: Name, d_tcon :: t }
645 -- ^ "Placeholder" for data whose constructors are defined later
646 deriving Functor
647{-!
648deriving instance Binary PData'
649deriving instance NFData PData'
650!-}
652-- Handy to get a free function for applying PTerm -> PTerm functions
653-- across a program, by deriving Functor
655type PDecl = PDecl' PTerm
656type PData = PData' PTerm
657type PClause = PClause' PTerm
659-- get all the names declared in a decl
661declared :: PDecl -> [Name]
662declared (PFix _ _ _) = []
663declared (PTy _ _ _ _ _ n t) = [n]
664declared (PPostulate _ _ _ _ n t) = [n]
665declared (PClauses _ _ n _) = [] -- not a declaration
666declared (PCAF _ n _) = [n]
667declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
668 where fstt (_, _, a, _, _, _) = a
669declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
670declared (PParams _ _ ds) = concatMap declared ds
671declared (PNamespace _ ds) = concatMap declared ds
672declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
673declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
674declared (PInstance _ _ _ _ _ _ _ _) = []
675declared (PDSL n _) = [n]
676declared (PSyntax _ _) = []
677declared (PMutual _ ds) = concatMap declared ds
678declared (PDirective _) = []
680-- get the names declared, not counting nested parameter blocks
681tldeclared :: PDecl -> [Name]
682tldeclared (PFix _ _ _) = []
683tldeclared (PTy _ _ _ _ _ n t) = [n]
684tldeclared (PPostulate _ _ _ _ n t) = [n]
685tldeclared (PClauses _ _ n _) = [] -- not a declaration
686tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
687tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
688 where fstt (_, _, a, _, _, _) = a
689tldeclared (PParams _ _ ds) = []
690tldeclared (PMutual _ ds) = concatMap tldeclared ds
691tldeclared (PNamespace _ ds) = concatMap tldeclared ds
692tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
693tldeclared (PInstance _ _ _ _ _ _ _ _) = []
694tldeclared _ = []
696defined :: PDecl -> [Name]
697defined (PFix _ _ _) = []
698defined (PTy _ _ _ _ _ n t) = []
699defined (PPostulate _ _ _ _ n t) = []
700defined (PClauses _ _ n _) = [n] -- not a declaration
701defined (PCAF _ n _) = [n]
702defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
703 where fstt (_, _, a, _, _, _) = a
704defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
705defined (PParams _ _ ds) = concatMap defined ds
706defined (PNamespace _ ds) = concatMap defined ds
707defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
708defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
709defined (PInstance _ _ _ _ _ _ _ _) = []
710defined (PDSL n _) = [n]
711defined (PSyntax _ _) = []
712defined (PMutual _ ds) = concatMap defined ds
713defined (PDirective _) = []
714--defined _ = []
716updateN :: [(Name, Name)] -> Name -> Name
717updateN ns n | Just n' <- lookup n ns = n'
718updateN _ n = n
720updateNs :: [(Name, Name)] -> PTerm -> PTerm
721updateNs [] t = t
722updateNs ns t = mapPT updateRef t
723 where updateRef (PRef fc f) = PRef fc (updateN ns f)
724 updateRef t = t
726-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
727-- updateDNs [] t = t
728-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
729-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
730-- where updateCNs ns (PClause n l ts r ds)
731-- = PClause (updateN ns n) (fmap (updateNs ns) l)
732-- (map (fmap (updateNs ns)) ts)
733-- (fmap (updateNs ns) r)
734-- (map (updateDNs ns) ds)
735-- updateDNs ns c = c
737data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
739-- | High level language terms
740data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
741 | PRef FC Name -- ^ A reference to a variable
742 | PInferRef FC Name -- ^ A name to be defined later
743 | PPatvar FC Name -- ^ A pattern variable
744 | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
745 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
746 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
747 | PTyped PTerm PTerm -- ^ Term with explicit type
748 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
749 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
750 | PMatchApp FC Name -- ^ Make an application by type matching
751 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
752 | PTrue FC PunInfo -- ^ Unit type..?
753 | PRefl FC PTerm -- ^ The canonical proof of the equality type
754 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
755 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
756 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
757 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
758 | PDPair 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)
759 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
760 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
761 | PHidden PTerm -- ^ Irrelevant or hidden pattern
762 | PType -- ^ 'Type' type
763 | PUniverse Universe -- ^ Some universe
764 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
765 | PConstant Const -- ^ Builtin types
766 | Placeholder -- ^ Underscore
767 | PDoBlock [PDo] -- ^ Do notation
768 | PIdiom FC PTerm -- ^ Idiom brackets
769 | PReturn FC
770 | PMetavar Name -- ^ A metavariable, ?name
771 | PProof [PTactic] -- ^ Proof script
772 | PTactics [PTactic] -- ^ As PProof, but no auto solving
773 | PElabError Err -- ^ Error to report on elaboration
774 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
775 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
776 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
777 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
778 | PNoImplicits PTerm -- ^ never run implicit converions on the term
779 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
780 | PUnquote PTerm -- ^ ,Term
781 deriving (Eq, Data, Typeable)
784{-!
785deriving instance Binary PTerm
786deriving instance NFData PTerm
787!-}
789mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
790mapPT f t = f (mpt t) where
791 mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
792 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
793 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
794 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
795 (fmap (mapPT f) g)
796 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
797 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
798 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
799 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
800 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
801 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
802 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
803 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
804 mpt (PHidden t) = PHidden (mapPT f t)
805 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
806 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
807 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
808 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
809 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
810 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
811 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
812 mpt x = x
815data PTactic' t = Intro [Name] | Intros | Focus Name
816 | Refine Name [Bool] | Rewrite t | DoUnify
817 | Induction t
818 | CaseTac t
819 | Equiv t
820 | MatchRefine Name
821 | LetTac Name t | LetTacTy Name t t
822 | Exact t | Compute | Trivial | TCInstance
823 | ProofSearch Bool Bool Int (Maybe Name) [Name]
824 -- ^ the bool is whether to search recursively
825 | Solve
826 | Attack
827 | ProofState | ProofTerm | Undo
828 | Try (PTactic' t) (PTactic' t)
829 | TSeq (PTactic' t) (PTactic' t)
830 | ApplyTactic t -- see Language.Reflection module
831 | ByReflection t
832 | Reflect t
833 | Fill t
834 | GoalType String (PTactic' t)
835 | TCheck t
836 | TEval t
837 | TDocStr (Either Name Const)
838 | TSearch t
839 | Skip
840 | TFail [ErrorReportPart]
841 | Qed | Abandon
842 | SourceFC
843 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
844{-!
845deriving instance Binary PTactic'
846deriving instance NFData PTactic'
847!-}
848instance Sized a => Sized (PTactic' a) where
849 size (Intro nms) = 1 + size nms
850 size Intros = 1
851 size (Focus nm) = 1 + size nm
852 size (Refine nm bs) = 1 + size nm + length bs
853 size (Rewrite t) = 1 + size t
854 size (Induction t) = 1 + size t
855 size (LetTac nm t) = 1 + size nm + size t
856 size (Exact t) = 1 + size t
857 size Compute = 1
858 size Trivial = 1
859 size Solve = 1
860 size Attack = 1
861 size ProofState = 1
862 size ProofTerm = 1
863 size Undo = 1
864 size (Try l r) = 1 + size l + size r
865 size (TSeq l r) = 1 + size l + size r
866 size (ApplyTactic t) = 1 + size t
867 size (Reflect t) = 1 + size t
868 size (Fill t) = 1 + size t
869 size Qed = 1
870 size Abandon = 1
871 size Skip = 1
872 size (TFail ts) = 1 + size ts
873 size SourceFC = 1
875type PTactic = PTactic' PTerm
877data PDo' t = DoExp FC t
878 | DoBind FC Name t
879 | DoBindP FC t t [(t,t)]
880 | DoLet FC Name t t
881 | DoLetP FC t t
882 deriving (Eq, Functor, Data, Typeable)
883{-!
884deriving instance Binary PDo'
885deriving instance NFData PDo'
886!-}
888instance Sized a => Sized (PDo' a) where
889 size (DoExp fc t) = 1 + size fc + size t
890 size (DoBind fc nm t) = 1 + size fc + size nm + size t
891 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
892 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
893 size (DoLetP fc l r) = 1 + size fc + size l + size r
895type PDo = PDo' PTerm
897-- The priority gives a hint as to elaboration order. Best to elaborate
898-- things early which will help give a more concrete type to other
899-- variables, e.g. a before (interpTy a).
901data PArg' t = PImp { priority :: Int,
902 machine_inf :: Bool, -- true if the machine inferred it
903 argopts :: [ArgOpt],
904 pname :: Name, getTm :: t }
905 | PExp { priority :: Int,
906 argopts :: [ArgOpt],
907 pname :: Name,
908 getTm :: t }
909 | PConstraint { priority :: Int,
910 argopts :: [ArgOpt],
911 pname :: Name,
912 getTm :: t }
913 | PTacImplicit { priority :: Int,
914 argopts :: [ArgOpt],
915 pname :: Name,
916 getScript :: t,
917 getTm :: t }
918 deriving (Show, Eq, Functor, Data, Typeable)
920data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
921 deriving (Show, Eq, Data, Typeable)
923instance Sized a => Sized (PArg' a) where
924 size (PImp p _ l nm trm) = 1 + size nm + size trm
925 size (PExp p l nm trm) = 1 + size nm + size trm
926 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
927 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
929{-!
930deriving instance Binary PArg'
931deriving instance NFData PArg'
932!-}
934pimp n t mach = PImp 1 mach [] n t
935pexp t = PExp 1 [] (sMN 0 "arg") t
936pconst t = PConstraint 1 [] (sMN 0 "carg") t
937ptacimp n s t = PTacImplicit 2 [] n s t
939type PArg = PArg' PTerm
941-- Type class data
943data ClassInfo = CI { instanceName :: Name,
944 class_methods :: [(Name, (FnOpts, PTerm))],
945 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
946 class_default_superclasses :: [PDecl],
947 class_params :: [Name],
948 class_instances :: [Name] }
949 deriving Show
950{-!
951deriving instance Binary ClassInfo
952deriving instance NFData ClassInfo
953!-}
955-- Type inference data
957data TIData = TIPartial -- ^ a function with a partially defined type
958 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
959 deriving Show
961-- | Miscellaneous information about functions
962data FnInfo = FnInfo { fn_params :: [Int] }
963 deriving Show
964{-!
965deriving instance Binary FnInfo
966deriving instance NFData FnInfo
967!-}
969data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
970 detaggable :: Bool }
971 deriving Show
972{-!
973deriving instance Binary OptInfo
974deriving instance NFData OptInfo
975!-}
978data TypeInfo = TI { con_names :: [Name],
979 codata :: Bool,
980 data_opts :: DataOpts,
981 param_pos :: [Int],
982 mutual_types :: [Name] }
983 deriving Show
984{-!
985deriving instance Binary TypeInfo
986deriving instance NFData TypeInfo
987!-}
989-- Syntactic sugar info
991data DSL' t = DSL { dsl_bind :: t,
992 dsl_return :: t,
993 dsl_apply :: t,
994 dsl_pure :: t,
995 dsl_var :: Maybe t,
996 index_first :: Maybe t,
997 index_next :: Maybe t,
998 dsl_lambda :: Maybe t,
999 dsl_let :: Maybe t,
1000 dsl_pi :: Maybe t
1002 deriving (Show, Functor)
1003{-!
1004deriving instance Binary DSL'
1005deriving instance NFData DSL'
1006!-}
1008type DSL = DSL' PTerm
1010data SynContext = PatternSyntax | TermSyntax | AnySyntax
1011 deriving Show
1012{-!
1013deriving instance Binary SynContext
1014deriving instance NFData SynContext
1015!-}
1017data Syntax = Rule [SSymbol] PTerm SynContext
1018 deriving Show
1020syntaxNames :: Syntax -> [Name]
1021syntaxNames (Rule syms _ _) = mapMaybe ename syms
1022 where ename (Keyword n) = Just n
1023 ename _ = Nothing
1025syntaxSymbols :: Syntax -> [SSymbol]
1026syntaxSymbols (Rule ss _ _) = ss
1027{-!
1028deriving instance Binary Syntax
1029deriving instance NFData Syntax
1030!-}
1032data SSymbol = Keyword Name
1033 | Symbol String
1034 | Binding Name
1035 | Expr Name
1036 | SimpleExpr Name
1037 deriving (Show, Eq)
1040{-!
1041deriving instance Binary SSymbol
1042deriving instance NFData SSymbol
1043!-}
1045newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1047emptySyntaxRules :: SyntaxRules
1048emptySyntaxRules = SyntaxRules []
1050updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1051updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1052 where
1053 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1055 ruleSort [] [] = EQ
1056 ruleSort [] _ = LT
1057 ruleSort _ [] = GT
1058 ruleSort (s1:ss1) (s2:ss2) =
1059 case symCompare s1 s2 of
1060 EQ -> ruleSort ss1 ss2
1061 r -> r
1063 -- Better than creating Ord instance for SSymbol since
1064 -- in general this ordering does not really make sense.
1065 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1066 symCompare (Keyword _) _ = LT
1067 symCompare (Symbol _) (Keyword _) = GT
1068 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1069 symCompare (Symbol _) _ = LT
1070 symCompare (Binding _) (Keyword _) = GT
1071 symCompare (Binding _) (Symbol _) = GT
1072 symCompare (Binding b1) (Binding b2) = compare b1 b2
1073 symCompare (Binding _) _ = LT
1074 symCompare (Expr _) (Keyword _) = GT
1075 symCompare (Expr _) (Symbol _) = GT
1076 symCompare (Expr _) (Binding _) = GT
1077 symCompare (Expr e1) (Expr e2) = compare e1 e2
1078 symCompare (Expr _) _ = LT
1079 symCompare (SimpleExpr _) (Keyword _) = GT
1080 symCompare (SimpleExpr _) (Symbol _) = GT
1081 symCompare (SimpleExpr _) (Binding _) = GT
1082 symCompare (SimpleExpr _) (Expr _) = GT
1083 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1085initDSL = DSL (PRef f (sUN ">>="))
1086 (PRef f (sUN "return"))
1087 (PRef f (sUN "<$>"))
1088 (PRef f (sUN "pure"))
1089 Nothing
1090 Nothing
1091 Nothing
1092 Nothing
1093 Nothing
1094 Nothing
1095 where f = fileFC "(builtin)"
1097data Using = UImplicit Name PTerm
1098 | UConstraint Name [Name]
1099 deriving (Show, Eq)
1100{-!
1101deriving instance Binary Using
1102deriving instance NFData Using
1103!-}
1105data SyntaxInfo = Syn { using :: [Using],
1106 syn_params :: [(Name, PTerm)],
1107 syn_namespace :: [String],
1108 no_imp :: [Name],
1109 decoration :: Name -> Name,
1110 inPattern :: Bool,
1111 implicitAllowed :: Bool,
1112 maxline :: Maybe Int,
1113 mut_nesting :: Int,
1114 dsl_info :: DSL,
1115 syn_in_quasiquote :: Int }
1116 deriving Show
1117{-!
1118deriving instance NFData SyntaxInfo
1119deriving instance Binary SyntaxInfo
1120!-}
1122defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1124expandNS :: SyntaxInfo -> Name -> Name
1125expandNS syn n@(NS _ _) = n
1126expandNS syn n = case syn_namespace syn of
1127 [] -> n
1128 xs -> sNS n xs
1131-- For inferring types of things
1133bi = fileFC "builtin"
1135inferTy = sMN 0 "__Infer"
1136inferCon = sMN 0 "__infer"
1137inferDecl = PDatadecl inferTy
1138 PType
1139 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1140 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1141 (PRef bi inferTy)), bi, [])]
1142inferOpts = []
1144infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1145infP = P (TCon 6 0) inferTy (TType (UVal 0))
1147getInferTerm, getInferType :: Term -> Term
1148getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1149getInferTerm (App (App _ _) tm) = tm
1150getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1152getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1153 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1154 toTy (PVar t) = PVTy t
1155 toTy b = b
1156getInferType (App (App _ ty) _) = ty
1160-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1162primNames = [eqTy, eqCon, inferTy, inferCon]
1164unitTy = sUN "Unit"
1165unitCon = sUN "MkUnit"
1167falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1168 "The empty type, also known as the trivially false proposition." ++
1169 "\n\n" ++
1170 "Use `void` or `absurd` to prove anything if you have a variable " ++
1171 "of type `Void` in scope."
1172falseTy = sUN "Void"
1174pairTy = sNS (sUN "Pair") ["Builtins"]
1175pairCon = sNS (sUN "MkPair") ["Builtins"]
1177eqTy = sUN "="
1178eqCon = sUN "Refl"
1179eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1180 "The propositional equality type. A proof that `x` = `y`." ++
1181 "\n\n" ++
1182 "To use such a proof, pattern-match on it, and the two equal things will " ++
1183 "then need to be the _same_ pattern." ++
1184 "\n\n" ++
1185 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1186 "is possible to state equalities between values of potentially different " ++
1187 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1188 "\n\n" ++
1189 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1191eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1192 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1193 PType))
1194 [(reflDoc, reflParamDoc,
1195 eqCon, PPi impl (n "A") PType (
1196 PPi impl (n "x") (PRef bi (n "A"))
1197 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1198 pimp (n "B") Placeholder False,
1199 pexp (PRef bi (n "x")),
1200 pexp (PRef bi (n "x"))])), bi, [])]
1201 where n a = sUN a
1202 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1203 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1204 "shown that both sides are in fact equal."
1205 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1206 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1208eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1209 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1211 where n a = sUN a
1213eqOpts = []
1215-- | The special name to be used in the module documentation context -
1216-- not for use in the main definition context. The namespace around it
1217-- will determine the module to which the docs adhere.
1218modDocName :: Name
1219modDocName = sMN 0 "ModuleDocs"
1221-- Defined in builtins.idr
1222sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1223existsCon = sNS (sUN "MkSigma") ["Builtins"]
1225piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1226piBind = piBindp expl
1228piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1229piBindp p [] t = t
1230piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1233-- Pretty-printing declarations and terms
1235-- These "show" instances render to an absurdly wide screen because inserted line breaks
1236-- could interfere with interactive editing, which calls "show".
1238instance Show PTerm where
1239 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1241instance Show PDecl where
1242 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1244instance Show PClause where
1245 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1247instance Show PData where
1248 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1250instance Pretty PTerm OutputAnnotation where
1251 pretty = prettyImp defaultPPOption
1253-- | Colourise annotations according to an Idris state. It ignores the names
1254-- in the annotation, as there's no good way to show extended information on a
1255-- terminal.
1256consoleDecorate :: IState -> OutputAnnotation -> String -> String
1257consoleDecorate ist _ | not (idris_colourRepl ist) = id
1258consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1259 in if constIsType c
1260 then colouriseType theme
1261 else colouriseData theme
1262consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1263consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1264consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1265consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1266consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1267consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1268 theme = idris_colourTheme ist
1269 in case () of
1270 _ | isDConName n ctxt -> colouriseData theme
1271 _ | isFnName n ctxt -> colouriseFun theme
1272 _ | isTConName n ctxt -> colouriseType theme
1273 _ | isPostulateName n ist -> colourisePostulate theme
1274 _ | otherwise -> id -- don't colourise unknown names
1275consoleDecorate ist (AnnFC _) = id
1276consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1277 where colour BoldText = IdrisColour Nothing True False True False
1278 colour UnderlineText = IdrisColour Nothing True True False False
1279 colour ItalicText = IdrisColour Nothing True False False True
1280consoleDecorate ist (AnnTerm _ _) = id
1281consoleDecorate ist (AnnSearchResult _) = id
1282consoleDecorate ist (AnnErr _) = id
1284isPostulateName :: Name -> IState -> Bool
1285isPostulateName n ist = S.member n (idris_postulates ist)
1287-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1288prettyImp :: PPOption -- ^^ pretty printing options
1289 -> PTerm -- ^^ the term to pretty-print
1290 -> Doc OutputAnnotation
1291prettyImp impl = pprintPTerm impl [] [] []
1293-- | Serialise something to base64 using its Binary instance.
1295-- | Do the right thing for rendering a term in an IState
1296prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1297prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1299-- | Pretty-print a high-level Idris term in some bindings context with infix info
1300pprintPTerm :: PPOption -- ^^ pretty printing options
1301 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1302 -> [Name] -- ^^ names to always show in pi, even if not used
1303 -> [FixDecl] -- ^^ Fixity declarations
1304 -> PTerm -- ^^ the term to pretty-print
1305 -> Doc OutputAnnotation
1306pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1307 where
1308 startPrec = 0
1309 funcAppPrec = 10
1310 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1311 prettySe p bnd (PQuote r) =
1312 text "![" <> pretty r <> text "]"
1313 prettySe p bnd (PPatvar fc n) = pretty n
1314 prettySe p bnd e
1315 | Just str <- slist p bnd e = str
1316 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1317 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1318 prettySe p bnd (PLam fc n ty sc) =
1319 bracket p startPrec . group . align . hang 2 $
1320 text "\\" <> bindingOf n False <+> text "=>" <$>
1321 prettySe startPrec ((n, False):bnd) sc
1322 prettySe p bnd (PLet fc n ty v sc) =
1323 bracket p startPrec . group . align $
1324 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1325 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1326 prettySe p bnd (PPi (Exp l s _) n ty sc)
1327 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1328 bracket p startPrec . group $
1329 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1330 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1331 | otherwise =
1332 bracket p startPrec . group $
1333 group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1334 where
1335 st =
1336 case s of
1337 Static -> text "[static]" <> space
1338 _ -> empty
1339 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1340 | ppopt_impl ppo =
1341 bracket p startPrec $
1342 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1343 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1344 | otherwise = prettySe startPrec ((n, True):bnd) sc
1345 where
1346 st =
1347 case s of
1348 Static -> text "[static]" <> space
1349 _ -> empty
1350 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1351 bracket p startPrec $
1352 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1353 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1354 bracket p startPrec $
1355 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1356 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1357 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1358 | UN nm <- basename f
1359 , not (ppopt_impl ppo) && null (getShowArgs args) =
1360 prettyName True (ppopt_impl ppo) bnd f
1361 prettySe p bnd (PAppBind _ (PRef _ f) [])
1362 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1363 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1364 | UN nm <- basename op
1365 , not (tnull nm) &&
1366 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1367 case getShowArgs args of
1368 [] -> opName True
1369 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1370 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1371 in bracket p precedence $ inFix (getTm l) (getTm r)
1372 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1373 bracket p funcAppPrec $
1374 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1375 align (group (vsep (map (prettyArgS bnd) rest)))
1376 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1377 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1378 f = getFixity (opStr op)
1379 left = case f of
1380 Nothing -> funcAppPrec + 1
1381 Just (Infixl p') -> p'
1382 Just f' -> prec f' + 1
1383 right = case f of
1384 Nothing -> funcAppPrec + 1
1385 Just (Infixr p') -> p'
1386 Just f' -> prec f' + 1
1387 inFix l r = align . group $
1388 (prettySe left bnd l <+> opName False) <$>
1389 group (prettySe right bnd r)
1390 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1391 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1392 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1393 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1394 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1395 let args = getShowArgs as
1396 fp = prettySe (startPrec + 1) bnd f
1397 shownArgs = if ppopt_impl ppo then as else args
1398 in
1399 bracket p funcAppPrec . group $
1400 if null shownArgs
1401 then fp
1402 else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1403 prettySe p bnd (PCase _ scr cases) =
1404 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1405 indent 2 (vsep (map ppcase cases))
1406 where
1407 ppcase (l, r) = let prettyCase = prettySe startPrec
1408 ([(n, False) | n <- vars l] ++ bnd)
1409 in nest nestingSize $
1410 prettyCase l <+> text "=>" <+> prettyCase r
1411 -- Warning: this is a bit of a hack. At this stage, we don't have the
1412 -- global context, so we can't determine which names are constructors,
1413 -- which are types, and which are pattern variables on the LHS of the
1414 -- case pattern. We use the heuristic that names without a namespace
1415 -- are patvars, because right now case blocks in PTerms are always
1416 -- delaborated from TT before being sent to the pretty-printer. If they
1417 -- start getting printed directly, THIS WILL BREAK.
1418 -- Potential solution: add a list of known patvars to the cases in
1419 -- PCase, and have the delaborator fill it out, kind of like the pun
1420 -- disambiguation on PDPair.
1421 vars tm = filter noNS (allNamesIn tm)
1422 noNS (NS _ _) = False
1423 noNS _ = True
1425 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1426 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1427 prettySe p bnd (PResolveTC _) = text "resolvetc"
1428 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1429 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1430 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1431 prettySe p bnd (PEq _ lt rt l r)
1432 | ppopt_impl ppo =
1433 bracket p eqPrec $
1434 enclose lparen rparen eq <+>
1435 align (group (vsep (map (prettyArgS bnd)
1436 [PImp 0 False [] (sUN "A") lt,
1437 PImp 0 False [] (sUN "B") rt,
1438 PExp 0 [] (sUN "x") l,
1439 PExp 0 [] (sUN "y") r])))
1440 | otherwise =
1441 bracket p eqPrec . align . group $
1442 prettyTerm l <+> eq <$> group (prettyTerm r)
1443 where eq = annName eqTy (text "=")
1444 eqPrec = startPrec
1445 prettyTerm = prettySe (eqPrec + 1) bnd
1446 prettySe p bnd (PRewrite _ l r _) =
1447 bracket p startPrec $
1448 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1449 prettySe p bnd (PTyped l r) =
1450 lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1451 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1452 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1453 align . group . vsep . punctuate (ann comma) $
1454 map (prettySe startPrec bnd) elts
1455 where ann = case pun of
1456 TypeOrTerm -> id
1457 IsType -> annName pairTy
1458 IsTerm -> annName pairCon
1459 prettySe p bnd (PDPair _ pun l t r) =
1460 annotated lparen <>
1461 left <+>
1462 annotated (text "**") <+>
1463 prettySe startPrec (addBinding bnd) r <>
1464 annotated rparen
1465 where annotated = case pun of
1466 IsType -> annName sigmaTy
1467 IsTerm -> annName existsCon
1468 TypeOrTerm -> id
1469 (left, addBinding) = case (l, pun) of
1470 (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1471 _ -> (prettySe startPrec bnd l, id )
1472 prettySe p bnd (PAlternative a as) =
1473 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1474 where
1475 prettyAs =
1476 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1477 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1478 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1479 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1480 -- XXX: add pretty for tactics
1481 prettySe p bnd (PProof ts) =
1482 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1483 prettySe p bnd (PTactics ts) =
1484 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1485 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1486 prettySe p bnd (PReturn f) = kwd "return"
1487 prettySe p bnd PImpossible = kwd "impossible"
1488 prettySe p bnd Placeholder = text "_"
1489 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1490 prettySe p bnd (PCoerced t) = prettySe p bnd t
1491 prettySe p bnd (PElabError s) = pretty s
1492 -- Quasiquote pprinting ignores bound vars
1493 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1494 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1495 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1497 prettySe p bnd _ = text "missing pretty-printer for term"
1499 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1500 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1501 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1502 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1504 prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1505 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1506 prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1507 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1509 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1510 annName n = annotate (AnnName n Nothing Nothing Nothing)
1512 opStr :: Name -> String
1513 opStr (NS n _) = opStr n
1514 opStr (UN n) = T.unpack n
1516 basename :: Name -> Name
1517 basename (NS n _) = basename n
1518 basename n = n
1520 slist' p bnd (PApp _ (PRef _ nil) _)
1521 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1522 slist' p bnd (PRef _ nil)
1523 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1524 slist' p bnd (PApp _ (PRef _ cons) args)
1525 | nsroot cons == sUN "::",
1526 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1527 all isImp imps,
1528 Just tl' <- slist' p bnd tl
1529 = Just (hd:tl')
1530 where
1531 isImp (PImp {}) = True
1532 isImp _ = False
1533 slist' _ _ tm = Nothing
1535 slist p bnd e | Just es <- slist' p bnd e = Just $
1536 case es of [] -> annotate (AnnData "" "") $ text "[]"
1537 [x] -> enclose left right . group $
1538 prettySe p bnd x
1539 xs -> (enclose left right .
1540 align . group . vsep .
1541 punctuate comma .
1542 map (prettySe p bnd)) xs
1543 where left = (annotate (AnnData "" "") (text "["))
1544 right = (annotate (AnnData "" "") (text "]"))
1545 comma = (annotate (AnnData "" "") (text ","))
1546 slist _ _ _ = Nothing
1548 pairElts :: PTerm -> Maybe [PTerm]
1549 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1550 | otherwise = Just [x, y]
1551 pairElts _ = Nothing
1553 natns = "Prelude.Nat."
1555 snat p (PRef _ z)
1556 | show z == (natns++"Z") || show z == "Z" = Just 0
1557 snat p (PApp _ s [PExp {getTm=n}])
1558 | show s == (natns++"S") || show s == "S",
1559 Just n' <- snat p n
1560 = Just $ 1 + n'
1561 snat _ _ = Nothing
1563 bracket outer inner doc
1564 | outer > inner = lparen <> doc <> rparen
1565 | otherwise = doc
1567 kwd = annotate AnnKeyword . text
1569 fixities :: M.Map String Fixity
1570 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1572 getFixity :: String -> Maybe Fixity
1573 getFixity = flip M.lookup fixities
1575-- | Pretty-printer helper for the binding site of a name
1576bindingOf :: Name -- ^^ the bound name
1577 -> Bool -- ^^ whether the name is implicit
1578 -> Doc OutputAnnotation
1579bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1581-- | Pretty-printer helper for names that attaches the correct annotations
1582prettyName
1583 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1584 -> Bool -- ^^ whether to show namespaces
1585 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1586 -> Name -- ^^ the name to pprint
1587 -> Doc OutputAnnotation
1588prettyName infixParen showNS bnd n
1589 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1590 | (UN n') <- n, isPrefixOf "_" $ T.unpack n' = text "_"
1591 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1592 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1593 where fullName = text nameSpace <> parenthesise (text (baseName n))
1594 baseName (UN n) = T.unpack n
1595 baseName (NS n ns) = baseName n
1596 baseName (MN i s) = T.unpack s
1597 baseName other = show other
1598 nameSpace = case n of
1599 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1600 _ -> ""
1601 isInfix = case baseName n of
1602 "" -> False
1603 (c : _) -> not (isAlpha c)
1604 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1607showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1608showCImp ppo (PClause _ n l ws r w)
1609 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1610 <+> text "where" <+> text (show w)
1611 where
1612 showWs [] = empty
1613 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1614showCImp ppo (PWith _ n l ws r w)
1615 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1616 <+> braces (text (show w))
1617 where
1618 showWs [] = empty
1619 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1622showDImp :: PPOption -> PData -> Doc OutputAnnotation
1623showDImp ppo (PDatadecl n ty cons)
1624 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1625 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1627showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1628showDecls o ds = vsep (map (showDeclImp o) ds)
1630showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1631showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1632showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1633 indent 2 (vsep (map (showCImp o) cs))
1634showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1635showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1636showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1637showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1638showDeclImp o (PClass _ _ _ cs n ps _ ds)
1639 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1640showDeclImp o (PInstance _ _ cs n _ t _ ds)
1641 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1642showDeclImp _ _ = text "..."
1643-- showDeclImp (PImport o) = "import " ++ o
1645instance Show (Doc OutputAnnotation) where
1646 show = flip (displayS . renderCompact) ""
1648getImps :: [PArg] -> [(Name, PTerm)]
1649getImps [] = []
1650getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1651getImps (_ : xs) = getImps xs
1653getExps :: [PArg] -> [PTerm]
1654getExps [] = []
1655getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1656getExps (_ : xs) = getExps xs
1658getShowArgs :: [PArg] -> [PArg]
1659getShowArgs [] = []
1660getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1661getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1662getShowArgs (_ : xs) = getShowArgs xs
1664getConsts :: [PArg] -> [PTerm]
1665getConsts [] = []
1666getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1667getConsts (_ : xs) = getConsts xs
1669getAll :: [PArg] -> [PTerm]
1670getAll = map getTm
1673-- | Show Idris name
1674showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1675 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1676 -> PPOption -- ^^ pretty printing options
1677 -> Bool -- ^^ whether to colourise
1678 -> Name -- ^^ the term to show
1679 -> String
1680showName ist bnd ppo colour n = case ist of
1681 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1682 Nothing -> showbasic n
1683 where name = if ppopt_impl ppo then show n else showbasic n
1684 showbasic n@(UN _) = showCG n
1685 showbasic (MN i s) = str s
1686 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1687 showbasic (SN s) = show s
1688 fst3 (x, _, _) = x
1689 colourise n t = let ctxt' = fmap tt_ctxt ist in
1690 case ctxt' of
1691 Nothing -> name
1692 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1693 else colouriseBound t name
1694 | isDConName n ctxt -> colouriseData t name
1695 | isFnName n ctxt -> colouriseFun t name
1696 | isTConName n ctxt -> colouriseType t name
1697 -- The assumption is that if a name is not bound and does not exist in the
1698 -- global context, then we're somewhere in which implicit info has been lost
1699 -- (like error messages). Thus, unknown vars are colourised as implicits.
1700 | otherwise -> colouriseImplicit t name
1702showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1703 -> PTerm -- ^^ the term to show
1704 -> String
1705showTm ist = displayDecorated (consoleDecorate ist) .
1706 renderPretty 0.8 100000 .
1707 prettyImp (ppOptionIst ist)
1709-- | Show a term with implicits, no colours
1710showTmImpls :: PTerm -> String
1711showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1715instance Sized PTerm where
1716 size (PQuote rawTerm) = size rawTerm
1717 size (PRef fc name) = size name
1718 size (PLam fc name ty bdy) = 1 + size ty + size bdy
1719 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1720 size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1721 size (PTyped trm ty) = 1 + size trm + size ty
1722 size (PApp fc name args) = 1 + size args
1723 size (PAppBind fc name args) = 1 + size args
1724 size (PCase fc trm bdy) = 1 + size trm + size bdy
1725 size (PTrue fc _) = 1
1726 size (PRefl fc _) = 1
1727 size (PResolveTC fc) = 1
1728 size (PEq fc _ _ left right) = 1 + size left + size right
1729 size (PRewrite fc left right _) = 1 + size left + size right
1730 size (PPair fc _ left right) = 1 + size left + size right
1731 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1732 size (PAlternative a alts) = 1 + size alts
1733 size (PHidden hidden) = size hidden
1734 size (PUnifyLog tm) = size tm
1735 size (PDisamb _ tm) = size tm
1736 size (PNoImplicits tm) = size tm
1737 size PType = 1
1738 size (PUniverse _) = 1
1739 size (PConstant const) = 1 + size const
1740 size Placeholder = 1
1741 size (PDoBlock dos) = 1 + size dos
1742 size (PIdiom fc term) = 1 + size term
1743 size (PReturn fc) = 1
1744 size (PMetavar name) = 1
1745 size (PProof tactics) = size tactics
1746 size (PElabError err) = size err
1747 size PImpossible = 1
1748 size _ = 0
1750getPArity :: PTerm -> Int
1751getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1752getPArity _ = 0
1754-- Return all names, free or globally bound, in the given term.
1756allNamesIn :: PTerm -> [Name]
1757allNamesIn tm = nub $ ni [] tm
1758 where -- TODO THINK added niTacImp, but is it right?
1759 ni env (PRef _ n)
1760 | not (n `elem` env) = [n]
1761 ni env (PPatvar _ n) = [n]
1762 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1763 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1764 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1765 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1766 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1767 ni env (PHidden tm) = ni env tm
1768 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1769 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1770 ni env (PTyped l r) = ni env l ++ ni env r
1771 ni env (PPair _ _ l r) = ni env l ++ ni env r
1772 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1773 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1774 ni env (PAlternative a ls) = concatMap (ni env) ls
1775 ni env (PUnifyLog tm) = ni env tm
1776 ni env (PDisamb _ tm) = ni env tm
1777 ni env (PNoImplicits tm) = ni env tm
1778 ni env _ = []
1780 niTacImp env (TacImp _ _ scr) = ni env scr
1781 niTacImp _ _ = []
1783-- Return all names defined in binders in the given term
1784boundNamesIn :: PTerm -> [Name]
1785boundNamesIn tm = nub $ ni tm
1786 where -- TODO THINK Added niTacImp, but is it right?
1787 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1788 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1789 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1790 ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)
1791 ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1792 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1793 ni (PEq _ _ _ l r) = ni l ++ ni r
1794 ni (PRewrite _ l r _) = ni l ++ ni r
1795 ni (PTyped l r) = ni l ++ ni r
1796 ni (PPair _ _ l r) = ni l ++ ni r
1797 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1798 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1799 ni (PAlternative a as) = concatMap (ni) as
1800 ni (PHidden tm) = ni tm
1801 ni (PUnifyLog tm) = ni tm
1802 ni (PDisamb _ tm) = ni tm
1803 ni (PNoImplicits tm) = ni tm
1804 ni _ = []
1806 niTacImp (TacImp _ _ scr) = ni scr
1807 niTacImp _ = []
1809-- Return names which are valid implicits in the given term (type).
1810implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1811implicitNamesIn uvars ist tm = nub $ ni [] tm
1812 where
1813 ni env (PRef _ n)
1814 | not (n `elem` env)
1815 = case lookupTy n (tt_ctxt ist) of
1816 [] -> [n]
1817 _ -> if n `elem` uvars then [n] else []
1818 ni env (PApp _ f@(PRef _ n) as)
1819 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1820 | otherwise = concatMap (ni env) (map getTm as)
1821 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1822 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1823 ni env (PCase _ c os) = ni env c ++
1824 -- names in 'os', not counting the names bound in the cases
1825 (nub (concatMap (ni env) (map snd os))
1826 \\ nub (concatMap (ni env) (map fst os)))
1827 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1828 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1829 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1830 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1831 ni env (PTyped l r) = ni env l ++ ni env r
1832 ni env (PPair _ _ l r) = ni env l ++ ni env r
1833 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1834 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1835 ni env (PAlternative a as) = concatMap (ni env) as
1836 ni env (PHidden tm) = ni env tm
1837 ni env (PUnifyLog tm) = ni env tm
1838 ni env (PDisamb _ tm) = ni env tm
1839 ni env (PNoImplicits tm) = ni env tm
1840 ni env _ = []
1842-- Return names which are free in the given term.
1843namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1844namesIn uvars ist tm = nub $ ni [] tm
1845 where
1846 ni env (PRef _ n)
1847 | not (n `elem` env)
1848 = case lookupTy n (tt_ctxt ist) of
1849 [] -> [n]
1850 _ -> if n `elem` (map fst uvars) then [n] else []
1851 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1852 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1853 ni env (PCase _ c os) = ni env c ++
1854 -- names in 'os', not counting the names bound in the cases
1855 (nub (concatMap (ni env) (map snd os))
1856 \\ nub (concatMap (ni env) (map fst os)))
1857 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1858 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1859 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1860 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1861 ni env (PTyped l r) = ni env l ++ ni env r
1862 ni env (PPair _ _ l r) = ni env l ++ ni env r
1863 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1864 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1865 ni env (PAlternative a as) = concatMap (ni env) as
1866 ni env (PHidden tm) = ni env tm
1867 ni env (PUnifyLog tm) = ni env tm
1868 ni env (PDisamb _ tm) = ni env tm
1869 ni env (PNoImplicits tm) = ni env tm
1870 ni env _ = []
1872 niTacImp env (TacImp _ _ scr) = ni env scr
1873 niTacImp _ _ = []
1875-- Return which of the given names are used in the given term.
1877usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1878usedNamesIn vars ist tm = nub $ ni [] tm
1879 where -- TODO THINK added niTacImp, but is it right?
1880 ni env (PRef _ n)
1881 | n `elem` vars && not (n `elem` env)
1882 = case lookupDefExact n (tt_ctxt ist) of
1883 Nothing -> [n]
1884 _ -> []
1885 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1886 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1887 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1888 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1889 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1890 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1891 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1892 ni env (PTyped l r) = ni env l ++ ni env r
1893 ni env (PPair _ _ l r) = ni env l ++ ni env r
1894 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1895 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1896 ni env (PAlternative a as) = concatMap (ni env) as
1897 ni env (PHidden tm) = ni env tm
1898 ni env (PUnifyLog tm) = ni env tm
1899 ni env (PDisamb _ tm) = ni env tm
1900 ni env (PNoImplicits tm) = ni env tm
1901 ni env _ = []
1903 niTacImp env (TacImp _ _ scr) = ni env scr
1904 niTacImp _ _ = []
1906-- Return the list of inaccessible (= dotted) positions for a name.
1907getErasureInfo :: IState -> Name -> [Int]
1908getErasureInfo ist n =
1909 case lookupCtxtExact n (idris_optimisation ist) of
1910 Just (Optimise inacc detagg) -> map fst inacc
1911 Nothing -> []