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