git.iko.soy/Idris-dev
on 7e43af7 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
2023 lines 83 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, maybeToList)
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 | IdeMode 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 idris_exports :: [Name] -- ^ Functions with ExportList
230 }
232-- Required for parsers library, and therefore trifecta
233instance Show IState where
234 show = const "{internal state}"
236data SizeChange = Smaller | Same | Bigger | Unknown
237 deriving (Show, Eq)
238{-!
239deriving instance Binary SizeChange
240deriving instance NFData SizeChange
241!-}
243type SCGEntry = (Name, [Maybe (Int, SizeChange)])
244type UsageReason = (Name, Int) -- fn_name, its_arg_number
246data CGInfo = CGInfo { argsdef :: [Name],
247 calls :: [(Name, [[Name]])],
248 scg :: [SCGEntry],
249 argsused :: [Name],
250 usedpos :: [(Int, [UsageReason])] }
251 deriving Show
252{-!
253deriving instance Binary CGInfo
254deriving instance NFData CGInfo
255!-}
257primDefs = [sUN "unsafePerformPrimIO",
258 sUN "mkLazyForeignPrim",
259 sUN "mkForeignPrim",
260 sUN "void"]
262-- information that needs writing for the current module's .ibc file
263data IBCWrite = IBCFix FixDecl
264 | IBCImp Name
265 | IBCStatic Name
266 | IBCClass Name
267 | IBCInstance Bool Name Name
268 | IBCDSL Name
269 | IBCData Name
270 | IBCOpt Name
271 | IBCMetavar Name
272 | IBCSyntax Syntax
273 | IBCKeyword String
274 | IBCImport (Bool, FilePath) -- True = import public
275 | IBCImportDir FilePath
276 | IBCObj Codegen FilePath
277 | IBCLib Codegen String
278 | IBCCGFlag Codegen String
279 | IBCDyLib String
280 | IBCHeader Codegen String
281 | IBCAccess Name Accessibility
282 | IBCMetaInformation Name MetaInformation
283 | IBCTotal Name Totality
284 | IBCFlags Name [FnOpt]
285 | IBCFnInfo Name FnInfo
286 | IBCTrans Name (Term, Term)
287 | IBCErrRev (Term, Term)
288 | IBCCG Name
289 | IBCDoc Name
290 | IBCCoercion Name
291 | IBCDef Name -- i.e. main context
292 | IBCNameHint (Name, Name)
293 | IBCLineApp FilePath Int PTerm
294 | IBCErrorHandler Name
295 | IBCFunctionErrorHandler Name Name Name
296 | IBCPostulate Name
297 | IBCTotCheckErr FC String
298 | IBCParsedRegion FC
299 | IBCModDocs Name -- ^ The name is the special name used to track module docs
300 | IBCUsage (Name, Int)
301 | IBCExport Name
302 deriving Show
304-- | The initial state for the compiler
305idrisInit :: IState
306idrisInit = IState initContext [] []
307 emptyContext emptyContext emptyContext emptyContext
308 emptyContext emptyContext emptyContext emptyContext
309 emptyContext emptyContext emptyContext emptyContext
310 emptyContext emptyContext emptyContext emptyContext
311 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
312 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
313 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
314 AutomaticWidth S.empty [] Nothing Nothing [] [] M.empty []
316-- | The monad for the main REPL - reading and processing files and updating
317-- global state (hence the IO inner monad).
318--type Idris = WriterT [Either String (IO ())] (State IState a))
319type Idris = StateT IState (ExceptT Err IO)
321catchError :: Idris a -> (Err -> Idris a) -> Idris a
322catchError = liftCatch catchE
324throwError :: Err -> Idris a
325throwError = Trans.lift . throwE
327-- Commands in the REPL
329data Codegen = Via String
330-- | ViaC
331-- | ViaJava
332-- | ViaNode
333-- | ViaJavaScript
334-- | ViaLLVM
335 | Bytecode
336 deriving (Show, Eq)
337{-!
338deriving instance NFData Codegen
339!-}
341data HowMuchDocs = FullDocs | OverviewDocs
343-- | REPL commands
344data Command = Quit
345 | Help
346 | Eval PTerm
347 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
348 | Undefine [Name]
349 | Check PTerm
350 | DocStr (Either Name Const) HowMuchDocs
351 | TotCheck Name
352 | Reload
353 | Load FilePath (Maybe Int) -- up to maximum line number
354 | ChangeDirectory FilePath
355 | ModImport String
356 | Edit
357 | Compile Codegen String
358 | Execute
359 | ExecVal PTerm
360 | Metavars
361 | Prove Name
362 | AddProof (Maybe Name)
363 | RmProof Name
364 | ShowProof Name
365 | Proofs
366 | Universes
367 | LogLvl Int
368 | Spec PTerm
369 | HNF PTerm
370 | TestInline PTerm
371 | Defn Name
372 | Missing Name
373 | DynamicLink FilePath
374 | ListDynamic
375 | Pattelab PTerm
376 | Search [String] PTerm
377 | CaseSplitAt Bool Int Name
378 | AddClauseFrom Bool Int Name
379 | AddProofClauseFrom Bool Int Name
380 | AddMissing Bool Int Name
381 | MakeWith Bool Int Name
382 | MakeLemma Bool Int Name
383 | DoProofSearch Bool Bool Int Name [Name]
384 -- ^ the first bool is whether to update,
385 -- the second is whether to search recursively (i.e. for the arguments)
386 | SetOpt Opt
387 | UnsetOpt Opt
388 | NOP
389 | SetColour ColourType IdrisColour
390 | ColourOn
391 | ColourOff
392 | ListErrorHandlers
393 | SetConsoleWidth ConsoleWidth
394 | Apropos [String] String
395 | WhoCalls Name
396 | CallsWho Name
397 | MakeDoc String -- IdrisDoc
398 | Warranty
399 | PrintDef Name
400 | PPrint OutputFmt Int PTerm
401 | TransformInfo Name
402 -- Debugging commands
403 | DebugInfo Name
404 | DebugUnify PTerm PTerm
406data OutputFmt = HTMLOutput | LaTeXOutput
408data Opt = Filename String
409 | Quiet
410 | NoBanner
411 | ColourREPL Bool
412 | Idemode
413 | IdemodeSocket
414 | ShowLibs
415 | ShowLibdir
416 | ShowIncs
417 | ShowPkgs
418 | NoBasePkgs
419 | NoPrelude
420 | NoBuiltins -- only for the really primitive stuff!
421 | NoREPL
422 | OLogging Int
423 | Output String
424 | Interface
425 | TypeCase
426 | TypeInType
427 | DefaultTotal
428 | DefaultPartial
429 | WarnPartial
430 | WarnReach
431 | NoCoverage
432 | ErrContext
433 | ShowImpl
434 | Verbose
435 | Port String -- REPL TCP port
436 | IBCSubDir String
437 | ImportDir String
438 | PkgBuild String
439 | PkgInstall String
440 | PkgClean String
441 | PkgCheck String
442 | PkgREPL String
443 | PkgMkDoc String -- IdrisDoc
444 | PkgTest String
445 | PkgIndex FilePath
446 | WarnOnly
447 | Pkg String
448 | BCAsm String
449 | DumpDefun String
450 | DumpCases String
451 | UseCodegen Codegen
452 | OutputTy OutputType
453 | Extension LanguageExt
454 | InterpretScript String
455 | EvalExpr String
456 | TargetTriple String
457 | TargetCPU String
458 | OptLevel Int
459 | AddOpt Optimisation
460 | RemoveOpt Optimisation
461 | Client String
462 | ShowOrigErr
463 | AutoWidth -- ^ Automatically adjust terminal width
464 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
465 deriving (Show, Eq)
467-- Parsed declarations
469data Fixity = Infixl { prec :: Int }
470 | Infixr { prec :: Int }
471 | InfixN { prec :: Int }
472 | PrefixN { prec :: Int }
473 deriving Eq
474{-!
475deriving instance Binary Fixity
476deriving instance NFData Fixity
477!-}
479instance Show Fixity where
480 show (Infixl i) = "infixl " ++ show i
481 show (Infixr i) = "infixr " ++ show i
482 show (InfixN i) = "infix " ++ show i
483 show (PrefixN i) = "prefix " ++ show i
485data FixDecl = Fix Fixity String
486 deriving Eq
488instance Show FixDecl where
489 show (Fix f s) = show f ++ " " ++ s
491{-!
492deriving instance Binary FixDecl
493deriving instance NFData FixDecl
494!-}
496instance Ord FixDecl where
497 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
500data Static = Static | Dynamic
501 deriving (Show, Eq, Data, Typeable)
502{-!
503deriving instance Binary Static
504deriving instance NFData Static
505!-}
507-- Mark bindings with their explicitness, and laziness
508data Plicity = Imp { pargopts :: [ArgOpt],
509 pstatic :: Static,
510 pparam :: Bool,
511 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
512 }
513 | Exp { pargopts :: [ArgOpt],
514 pstatic :: Static,
515 pparam :: Bool } -- this is a param (rather than index)
516 | Constraint { pargopts :: [ArgOpt],
517 pstatic :: Static }
518 | TacImp { pargopts :: [ArgOpt],
519 pstatic :: Static,
520 pscript :: PTerm }
521 deriving (Show, Eq, Data, Typeable)
523{-!
524deriving instance Binary Plicity
525deriving instance NFData Plicity
526!-}
528is_scoped :: Plicity -> Maybe ImplicitInfo
529is_scoped (Imp _ _ _ s) = s
530is_scoped _ = Nothing
532impl = Imp [] Dynamic False Nothing
533forall_imp = Imp [] Dynamic False (Just (Impl False))
534forall_constraint = Imp [] Dynamic False (Just (Impl True))
535expl = Exp [] Dynamic False
536expl_param = Exp [] Dynamic True
537constraint = Constraint [] Static
538tacimpl t = TacImp [] Dynamic t
540data FnOpt = Inlinable -- always evaluate when simplifying
541 | TotalFn | PartialFn | CoveringFn
542 | Coinductive | AssertTotal
543 | Dictionary -- type class dictionary, eval only when
544 -- a function argument, and further evaluation resutls
545 | Implicit -- implicit coercion
546 | NoImplicit -- do not apply implicit coercions
547 | CExport String -- export, with a C name
548 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
549 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
550 | Reflection -- a reflecting function, compile-time only
551 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
552 | Constructor -- Data constructor type
553 deriving (Show, Eq)
554{-!
555deriving instance Binary FnOpt
556deriving instance NFData FnOpt
557!-}
559type FnOpts = [FnOpt]
561inlinable :: FnOpts -> Bool
562inlinable = elem Inlinable
564dictionary :: FnOpts -> Bool
565dictionary = elem Dictionary
567-- | Data declaration options
568data DataOpt = Codata -- ^ Set if the the data-type is coinductive
569 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
570 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
571 | DataErrRev
572 deriving (Show, Eq)
574type DataOpts = [DataOpt]
576-- | Type provider - what to provide
577data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
578 | ProvPostulate t -- ^ goal type must be Type, so only term
579 deriving (Show, Eq, Functor)
581type ProvideWhat = ProvideWhat' PTerm
583-- | Top-level declarations such as compiler directives, definitions,
584-- datatypes and typeclasses.
585data PDecl' t
586 = PFix FC Fixity [String] -- ^ Fixity declaration
587 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
588 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
589 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
590 | PCAF FC Name t -- ^ Top level constant
591 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
592 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
593 | PNamespace String [PDecl' t] -- ^ New namespace
594 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
595 Name -- Record name
596 [(Name, Plicity, t)] -- Params
597 [(Name, Docstring (Either Err PTerm))] -- Params doc
598 [(Name, Plicity, t)] -- Fields
599 [(Name, Docstring (Either Err PTerm))] -- Fields doc
600 (Maybe Name) -- Optional constructor name
601 (Docstring (Either Err PTerm)) -- Constructor doc
602 SyntaxInfo -- Constructor SyntaxInfo
603 -- ^ Record declaration
604 -- (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) (Maybe Name) t -- ^ Record declaration
605 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
606 [(Name, t)] -- constraints
607 Name
608 [(Name, t)] -- parameters
609 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
610 [PDecl' t] -- declarations
611 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
612 -- class name, parameters, method declarations
613 | PInstance
614 (Docstring (Either Err PTerm)) -- Instance docs
615 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
616 SyntaxInfo
617 FC [(Name, t)] -- constraints
618 Name -- class
619 [t] -- parameters
620 t -- full instance type
621 (Maybe Name) -- explicit name
622 [PDecl' t]
623 -- ^ Instance declaration: arguments are documentation, syntax info, source
624 -- location, constraints, class name, parameters, full instance
625 -- type, optional explicit name, and definitions
626 | PDSL Name (DSL' t) -- ^ DSL declaration
627 | PSyntax FC Syntax -- ^ Syntax definition
628 | PMutual FC [PDecl' t] -- ^ Mutual block
629 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
630 | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
631 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
632 -- bool is True, lhs and rhs must be convertible
633 deriving Functor
634{-!
635deriving instance Binary PDecl'
636deriving instance NFData PDecl'
637!-}
639-- For elaborator state
640data EState = EState {
641 case_decls :: [PDecl],
642 delayed_elab :: [Elab' EState ()]
643 }
645initEState = EState [] []
647type ElabD a = Elab' EState a
649-- | One clause of a top-level definition. Term arguments to constructors are:
650--
651-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
652--
653-- 2. The list of extra 'with' patterns
654--
655-- 3. The right-hand side
656--
657-- 4. The where block (PDecl' t)
659data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
660 | PWith FC Name t [t] t (Maybe Name) [PDecl' t]
661 | PClauseR FC [t] t [PDecl' t]
662 | PWithR FC [t] t (Maybe Name) [PDecl' t]
663 deriving Functor
664{-!
665deriving instance Binary PClause'
666deriving instance NFData PClause'
667!-}
669-- | Data declaration
670data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
671 d_tcon :: t, -- ^ Type constructor
672 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
673 }
674 -- ^ Data declaration
675 | PLaterdecl { d_name :: Name, d_tcon :: t }
676 -- ^ "Placeholder" for data whose constructors are defined later
677 deriving Functor
678{-!
679deriving instance Binary PData'
680deriving instance NFData PData'
681!-}
683-- Handy to get a free function for applying PTerm -> PTerm functions
684-- across a program, by deriving Functor
686type PDecl = PDecl' PTerm
687type PData = PData' PTerm
688type PClause = PClause' PTerm
690-- get all the names declared in a decl
692declared :: PDecl -> [Name]
693declared (PFix _ _ _) = []
694declared (PTy _ _ _ _ _ n t) = [n]
695declared (PPostulate _ _ _ _ n t) = [n]
696declared (PClauses _ _ n _) = [] -- not a declaration
697declared (PCAF _ n _) = [n]
698declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
699 where fstt (_, _, a, _, _, _) = a
700declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
701declared (PParams _ _ ds) = concatMap declared ds
702declared (PNamespace _ ds) = concatMap declared ds
703declared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn
704 where fstt (a, _, _) = a
705declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
706declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
707declared (PDSL n _) = [n]
708declared (PSyntax _ _) = []
709declared (PMutual _ ds) = concatMap declared ds
710declared (PDirective _) = []
711declared _ = []
713-- get the names declared, not counting nested parameter blocks
714tldeclared :: PDecl -> [Name]
715tldeclared (PFix _ _ _) = []
716tldeclared (PTy _ _ _ _ _ n t) = [n]
717tldeclared (PPostulate _ _ _ _ n t) = [n]
718tldeclared (PClauses _ _ n _) = [] -- not a declaration
719tldeclared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn
720 where fstt (a, _, _) = a
721tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
722 where fstt (_, _, a, _, _, _) = a
723tldeclared (PParams _ _ ds) = []
724tldeclared (PMutual _ ds) = concatMap tldeclared ds
725tldeclared (PNamespace _ ds) = concatMap tldeclared ds
726tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
727tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []
728tldeclared _ = []
730defined :: PDecl -> [Name]
731defined (PFix _ _ _) = []
732defined (PTy _ _ _ _ _ n t) = []
733defined (PPostulate _ _ _ _ n t) = []
734defined (PClauses _ _ n _) = [n] -- not a declaration
735defined (PCAF _ n _) = [n]
736defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
737 where fstt (_, _, a, _, _, _) = a
738defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
739defined (PParams _ _ ds) = concatMap defined ds
740defined (PNamespace _ ds) = concatMap defined ds
741defined (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn
742 where fstt (a, _, _) = a
743defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
744defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
745defined (PDSL n _) = [n]
746defined (PSyntax _ _) = []
747defined (PMutual _ ds) = concatMap defined ds
748defined (PDirective _) = []
749defined _ = []
751updateN :: [(Name, Name)] -> Name -> Name
752updateN ns n | Just n' <- lookup n ns = n'
753updateN _ n = n
755updateNs :: [(Name, Name)] -> PTerm -> PTerm
756updateNs [] t = t
757updateNs ns t = mapPT updateRef t
758 where updateRef (PRef fc f) = PRef fc (updateN ns f)
759 updateRef t = t
761-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
762-- updateDNs [] t = t
763-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
764-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
765-- where updateCNs ns (PClause n l ts r ds)
766-- = PClause (updateN ns n) (fmap (updateNs ns) l)
767-- (map (fmap (updateNs ns)) ts)
768-- (fmap (updateNs ns) r)
769-- (map (updateDNs ns) ds)
770-- updateDNs ns c = c
772data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
774-- | High level language terms
775data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
776 | PRef FC Name -- ^ A reference to a variable
777 | PInferRef FC Name -- ^ A name to be defined later
778 | PPatvar FC Name -- ^ A pattern variable
779 | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
780 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
781 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
782 | PTyped PTerm PTerm -- ^ Term with explicit type
783 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
784 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
785 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
786 | PMatchApp FC Name -- ^ Make an application by type matching
787 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
788 | PTrue FC PunInfo -- ^ Unit type..?
789 | PRefl FC PTerm -- ^ The canonical proof of the equality type
790 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
791 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
792 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
793 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
794 | 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)
795 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
796 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
797 | PHidden PTerm -- ^ Irrelevant or hidden pattern
798 | PType -- ^ 'Type' type
799 | PUniverse Universe -- ^ Some universe
800 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
801 | PConstant Const -- ^ Builtin types
802 | Placeholder -- ^ Underscore
803 | PDoBlock [PDo] -- ^ Do notation
804 | PIdiom FC PTerm -- ^ Idiom brackets
805 | PReturn FC
806 | PMetavar Name -- ^ A metavariable, ?name
807 | PProof [PTactic] -- ^ Proof script
808 | PTactics [PTactic] -- ^ As PProof, but no auto solving
809 | PElabError Err -- ^ Error to report on elaboration
810 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
811 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
812 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
813 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
814 | PNoImplicits PTerm -- ^ never run implicit converions on the term
815 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
816 | PUnquote PTerm -- ^ ~Term
817 | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script
818 deriving (Eq, Data, Typeable)
821{-!
822deriving instance Binary PTerm
823deriving instance NFData PTerm
824!-}
826mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
827mapPT f t = f (mpt t) where
828 mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
829 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
830 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
831 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
832 (fmap (mapPT f) g)
833 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
834 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
835 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
836 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
837 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
838 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
839 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
840 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
841 mpt (PHidden t) = PHidden (mapPT f t)
842 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
843 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
844 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
845 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
846 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
847 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
848 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
849 mpt x = x
852data PTactic' t = Intro [Name] | Intros | Focus Name
853 | Refine Name [Bool] | Rewrite t | DoUnify
854 | Induction t
855 | CaseTac t
856 | Equiv t
857 | Claim Name t
858 | Unfocus
859 | MatchRefine Name
860 | LetTac Name t | LetTacTy Name t t
861 | Exact t | Compute | Trivial | TCInstance
862 | ProofSearch Bool Bool Int (Maybe Name) [Name]
863 -- ^ the bool is whether to search recursively
864 | Solve
865 | Attack
866 | ProofState | ProofTerm | Undo
867 | Try (PTactic' t) (PTactic' t)
868 | TSeq (PTactic' t) (PTactic' t)
869 | ApplyTactic t -- see Language.Reflection module
870 | ByReflection t
871 | Reflect t
872 | Fill t
873 | GoalType String (PTactic' t)
874 | TCheck t
875 | TEval t
876 | TDocStr (Either Name Const)
877 | TSearch t
878 | Skip
879 | TFail [ErrorReportPart]
880 | Qed | Abandon
881 | SourceFC
882 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
883{-!
884deriving instance Binary PTactic'
885deriving instance NFData PTactic'
886!-}
887instance Sized a => Sized (PTactic' a) where
888 size (Intro nms) = 1 + size nms
889 size Intros = 1
890 size (Focus nm) = 1 + size nm
891 size (Refine nm bs) = 1 + size nm + length bs
892 size (Rewrite t) = 1 + size t
893 size (Induction t) = 1 + size t
894 size (LetTac nm t) = 1 + size nm + size t
895 size (Exact t) = 1 + size t
896 size Compute = 1
897 size Trivial = 1
898 size Solve = 1
899 size Attack = 1
900 size ProofState = 1
901 size ProofTerm = 1
902 size Undo = 1
903 size (Try l r) = 1 + size l + size r
904 size (TSeq l r) = 1 + size l + size r
905 size (ApplyTactic t) = 1 + size t
906 size (Reflect t) = 1 + size t
907 size (Fill t) = 1 + size t
908 size Qed = 1
909 size Abandon = 1
910 size Skip = 1
911 size (TFail ts) = 1 + size ts
912 size SourceFC = 1
914type PTactic = PTactic' PTerm
916data PDo' t = DoExp FC t
917 | DoBind FC Name t
918 | DoBindP FC t t [(t,t)]
919 | DoLet FC Name t t
920 | DoLetP FC t t
921 deriving (Eq, Functor, Data, Typeable)
922{-!
923deriving instance Binary PDo'
924deriving instance NFData PDo'
925!-}
927instance Sized a => Sized (PDo' a) where
928 size (DoExp fc t) = 1 + size fc + size t
929 size (DoBind fc nm t) = 1 + size fc + size nm + size t
930 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
931 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
932 size (DoLetP fc l r) = 1 + size fc + size l + size r
934type PDo = PDo' PTerm
936-- The priority gives a hint as to elaboration order. Best to elaborate
937-- things early which will help give a more concrete type to other
938-- variables, e.g. a before (interpTy a).
940data PArg' t = PImp { priority :: Int,
941 machine_inf :: Bool, -- true if the machine inferred it
942 argopts :: [ArgOpt],
943 pname :: Name, getTm :: t }
944 | PExp { priority :: Int,
945 argopts :: [ArgOpt],
946 pname :: Name,
947 getTm :: t }
948 | PConstraint { priority :: Int,
949 argopts :: [ArgOpt],
950 pname :: Name,
951 getTm :: t }
952 | PTacImplicit { priority :: Int,
953 argopts :: [ArgOpt],
954 pname :: Name,
955 getScript :: t,
956 getTm :: t }
957 deriving (Show, Eq, Functor, Data, Typeable)
959data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
960 deriving (Show, Eq, Data, Typeable)
962instance Sized a => Sized (PArg' a) where
963 size (PImp p _ l nm trm) = 1 + size nm + size trm
964 size (PExp p l nm trm) = 1 + size nm + size trm
965 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
966 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
968{-!
969deriving instance Binary PArg'
970deriving instance NFData PArg'
971!-}
973pimp n t mach = PImp 1 mach [] n t
974pexp t = PExp 1 [] (sMN 0 "arg") t
975pconst t = PConstraint 1 [] (sMN 0 "carg") t
976ptacimp n s t = PTacImplicit 2 [] n s t
978type PArg = PArg' PTerm
980-- | Get the highest FC in a term, if one exists
981highestFC :: PTerm -> Maybe FC
982highestFC (PQuote _) = Nothing
983highestFC (PRef fc _) = Just fc
984highestFC (PInferRef fc _) = Just fc
985highestFC (PPatvar fc _) = Just fc
986highestFC (PLam fc _ _ _) = Just fc
987highestFC (PPi _ _ _ _) = Nothing
988highestFC (PLet fc _ _ _ _) = Just fc
989highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
990highestFC (PApp fc _ _) = Just fc
991highestFC (PAppBind fc _ _) = Just fc
992highestFC (PMatchApp fc _) = Just fc
993highestFC (PCase fc _ _) = Just fc
994highestFC (PTrue fc _) = Just fc
995highestFC (PRefl fc _) = Just fc
996highestFC (PResolveTC fc) = Just fc
997highestFC (PEq fc _ _ _ _) = Just fc
998highestFC (PRewrite fc _ _ _) = Just fc
999highestFC (PPair fc _ _ _) = Just fc
1000highestFC (PDPair fc _ _ _ _) = Just fc
1001highestFC (PAs fc _ _) = Just fc
1002highestFC (PAlternative _ args) =
1003 case mapMaybe highestFC args of
1004 [] -> Nothing
1005 (fc:_) -> Just fc
1006highestFC (PHidden _) = Nothing
1007highestFC PType = Nothing
1008highestFC (PUniverse _) = Nothing
1009highestFC (PGoal fc _ _ _) = Just fc
1010highestFC (PConstant _) = Nothing
1011highestFC Placeholder = Nothing
1012highestFC (PDoBlock lines) =
1013 case map getDoFC lines of
1014 [] -> Nothing
1015 (fc:_) -> Just fc
1016 where
1017 getDoFC (DoExp fc t) = fc
1018 getDoFC (DoBind fc nm t) = fc
1019 getDoFC (DoBindP fc l r alts) = fc
1020 getDoFC (DoLet fc nm l r) = fc
1021 getDoFC (DoLetP fc l r) = fc
1023highestFC (PIdiom fc _) = Just fc
1024highestFC (PReturn fc) = Just fc
1025highestFC (PMetavar _) = Nothing
1026highestFC (PProof _) = Nothing
1027highestFC (PTactics _) = Nothing
1028highestFC (PElabError _) = Nothing
1029highestFC PImpossible = Nothing
1030highestFC (PCoerced tm) = highestFC tm
1031highestFC (PDisamb _ opts) = highestFC opts
1032highestFC (PUnifyLog tm) = highestFC tm
1033highestFC (PNoImplicits tm) = highestFC tm
1034highestFC (PQuasiquote _ _) = Nothing
1035highestFC (PUnquote tm) = highestFC tm
1037-- Type class data
1039data ClassInfo = CI { instanceName :: Name,
1040 class_methods :: [(Name, (FnOpts, PTerm))],
1041 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1042 class_default_superclasses :: [PDecl],
1043 class_params :: [Name],
1044 class_instances :: [Name] }
1045 deriving Show
1046{-!
1047deriving instance Binary ClassInfo
1048deriving instance NFData ClassInfo
1049!-}
1051-- Type inference data
1053data TIData = TIPartial -- ^ a function with a partially defined type
1054 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1055 deriving Show
1057-- | Miscellaneous information about functions
1058data FnInfo = FnInfo { fn_params :: [Int] }
1059 deriving Show
1060{-!
1061deriving instance Binary FnInfo
1062deriving instance NFData FnInfo
1063!-}
1065data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1066 detaggable :: Bool }
1067 deriving Show
1068{-!
1069deriving instance Binary OptInfo
1070deriving instance NFData OptInfo
1071!-}
1074data TypeInfo = TI { con_names :: [Name],
1075 codata :: Bool,
1076 data_opts :: DataOpts,
1077 param_pos :: [Int],
1078 mutual_types :: [Name] }
1079 deriving Show
1080{-!
1081deriving instance Binary TypeInfo
1082deriving instance NFData TypeInfo
1083!-}
1085-- Syntactic sugar info
1087data DSL' t = DSL { dsl_bind :: t,
1088 dsl_return :: t,
1089 dsl_apply :: t,
1090 dsl_pure :: t,
1091 dsl_var :: Maybe t,
1092 index_first :: Maybe t,
1093 index_next :: Maybe t,
1094 dsl_lambda :: Maybe t,
1095 dsl_let :: Maybe t,
1096 dsl_pi :: Maybe t
1098 deriving (Show, Functor)
1099{-!
1100deriving instance Binary DSL'
1101deriving instance NFData DSL'
1102!-}
1104type DSL = DSL' PTerm
1106data SynContext = PatternSyntax | TermSyntax | AnySyntax
1107 deriving Show
1108{-!
1109deriving instance Binary SynContext
1110deriving instance NFData SynContext
1111!-}
1113data Syntax = Rule [SSymbol] PTerm SynContext
1114 deriving Show
1116syntaxNames :: Syntax -> [Name]
1117syntaxNames (Rule syms _ _) = mapMaybe ename syms
1118 where ename (Keyword n) = Just n
1119 ename _ = Nothing
1121syntaxSymbols :: Syntax -> [SSymbol]
1122syntaxSymbols (Rule ss _ _) = ss
1123{-!
1124deriving instance Binary Syntax
1125deriving instance NFData Syntax
1126!-}
1128data SSymbol = Keyword Name
1129 | Symbol String
1130 | Binding Name
1131 | Expr Name
1132 | SimpleExpr Name
1133 deriving (Show, Eq)
1136{-!
1137deriving instance Binary SSymbol
1138deriving instance NFData SSymbol
1139!-}
1141newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1143emptySyntaxRules :: SyntaxRules
1144emptySyntaxRules = SyntaxRules []
1146updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1147updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1148 where
1149 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1151 ruleSort [] [] = EQ
1152 ruleSort [] _ = LT
1153 ruleSort _ [] = GT
1154 ruleSort (s1:ss1) (s2:ss2) =
1155 case symCompare s1 s2 of
1156 EQ -> ruleSort ss1 ss2
1157 r -> r
1159 -- Better than creating Ord instance for SSymbol since
1160 -- in general this ordering does not really make sense.
1161 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1162 symCompare (Keyword _) _ = LT
1163 symCompare (Symbol _) (Keyword _) = GT
1164 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1165 symCompare (Symbol _) _ = LT
1166 symCompare (Binding _) (Keyword _) = GT
1167 symCompare (Binding _) (Symbol _) = GT
1168 symCompare (Binding b1) (Binding b2) = compare b1 b2
1169 symCompare (Binding _) _ = LT
1170 symCompare (Expr _) (Keyword _) = GT
1171 symCompare (Expr _) (Symbol _) = GT
1172 symCompare (Expr _) (Binding _) = GT
1173 symCompare (Expr e1) (Expr e2) = compare e1 e2
1174 symCompare (Expr _) _ = LT
1175 symCompare (SimpleExpr _) (Keyword _) = GT
1176 symCompare (SimpleExpr _) (Symbol _) = GT
1177 symCompare (SimpleExpr _) (Binding _) = GT
1178 symCompare (SimpleExpr _) (Expr _) = GT
1179 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1181initDSL = DSL (PRef f (sUN ">>="))
1182 (PRef f (sUN "return"))
1183 (PRef f (sUN "<*>"))
1184 (PRef f (sUN "pure"))
1185 Nothing
1186 Nothing
1187 Nothing
1188 Nothing
1189 Nothing
1190 Nothing
1191 where f = fileFC "(builtin)"
1193data Using = UImplicit Name PTerm
1194 | UConstraint Name [Name]
1195 deriving (Show, Eq)
1196{-!
1197deriving instance Binary Using
1198deriving instance NFData Using
1199!-}
1201data SyntaxInfo = Syn { using :: [Using],
1202 syn_params :: [(Name, PTerm)],
1203 syn_namespace :: [String],
1204 no_imp :: [Name],
1205 decoration :: Name -> Name,
1206 inPattern :: Bool,
1207 implicitAllowed :: Bool,
1208 maxline :: Maybe Int,
1209 mut_nesting :: Int,
1210 dsl_info :: DSL,
1211 syn_in_quasiquote :: Int }
1212 deriving Show
1213{-!
1214deriving instance NFData SyntaxInfo
1215deriving instance Binary SyntaxInfo
1216!-}
1218defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1220expandNS :: SyntaxInfo -> Name -> Name
1221expandNS syn n@(NS _ _) = n
1222expandNS syn n = case syn_namespace syn of
1223 [] -> n
1224 xs -> sNS n xs
1227-- For inferring types of things
1229bi = fileFC "builtin"
1231inferTy = sMN 0 "__Infer"
1232inferCon = sMN 0 "__infer"
1233inferDecl = PDatadecl inferTy
1234 PType
1235 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1236 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1237 (PRef bi inferTy)), bi, [])]
1238inferOpts = []
1240infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1241infP = P (TCon 6 0) inferTy (TType (UVal 0))
1243getInferTerm, getInferType :: Term -> Term
1244getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1245getInferTerm (App (App _ _) tm) = tm
1246getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1248getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1249 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1250 toTy (PVar t) = PVTy t
1251 toTy b = b
1252getInferType (App (App _ ty) _) = ty
1256-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1258primNames = [eqTy, eqCon, inferTy, inferCon]
1260unitTy = sUN "Unit"
1261unitCon = sUN "MkUnit"
1263falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1264 "The empty type, also known as the trivially false proposition." ++
1265 "\n\n" ++
1266 "Use `void` or `absurd` to prove anything if you have a variable " ++
1267 "of type `Void` in scope."
1268falseTy = sUN "Void"
1270pairTy = sNS (sUN "Pair") ["Builtins"]
1271pairCon = sNS (sUN "MkPair") ["Builtins"]
1273upairTy = sNS (sUN "UPair") ["Builtins"]
1274upairCon = sNS (sUN "MkUPair") ["Builtins"]
1276eqTy = sUN "="
1277eqCon = sUN "Refl"
1278eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1279 "The propositional equality type. A proof that `x` = `y`." ++
1280 "\n\n" ++
1281 "To use such a proof, pattern-match on it, and the two equal things will " ++
1282 "then need to be the _same_ pattern." ++
1283 "\n\n" ++
1284 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1285 "is possible to state equalities between values of potentially different " ++
1286 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1287 "\n\n" ++
1288 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1290eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1291 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1292 PType))
1293 [(reflDoc, reflParamDoc,
1294 eqCon, PPi impl (n "A") PType (
1295 PPi impl (n "x") (PRef bi (n "A"))
1296 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1297 pimp (n "B") Placeholder False,
1298 pexp (PRef bi (n "x")),
1299 pexp (PRef bi (n "x"))])), bi, [])]
1300 where n a = sUN a
1301 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1302 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1303 "shown that both sides are in fact equal."
1304 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1305 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1307eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1308 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1310 where n a = sUN a
1312eqOpts = []
1314-- | The special name to be used in the module documentation context -
1315-- not for use in the main definition context. The namespace around it
1316-- will determine the module to which the docs adhere.
1317modDocName :: Name
1318modDocName = sMN 0 "ModuleDocs"
1320-- Defined in builtins.idr
1321sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1322existsCon = sNS (sUN "MkSigma") ["Builtins"]
1324piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1325piBind = piBindp expl
1327piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1328piBindp p [] t = t
1329piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1332-- Pretty-printing declarations and terms
1334-- These "show" instances render to an absurdly wide screen because inserted line breaks
1335-- could interfere with interactive editing, which calls "show".
1337instance Show PTerm where
1338 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1340instance Show PDecl where
1341 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1343instance Show PClause where
1344 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1346instance Show PData where
1347 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1349instance Pretty PTerm OutputAnnotation where
1350 pretty = prettyImp defaultPPOption
1352-- | Colourise annotations according to an Idris state. It ignores the names
1353-- in the annotation, as there's no good way to show extended information on a
1354-- terminal.
1355consoleDecorate :: IState -> OutputAnnotation -> String -> String
1356consoleDecorate ist _ | not (idris_colourRepl ist) = id
1357consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1358 in if constIsType c
1359 then colouriseType theme
1360 else colouriseData theme
1361consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1362consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1363consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1364consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1365consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1366consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1367 theme = idris_colourTheme ist
1368 in case () of
1369 _ | isDConName n ctxt -> colouriseData theme
1370 _ | isFnName n ctxt -> colouriseFun theme
1371 _ | isTConName n ctxt -> colouriseType theme
1372 _ | isPostulateName n ist -> colourisePostulate theme
1373 _ | otherwise -> id -- don't colourise unknown names
1374consoleDecorate ist (AnnFC _) = id
1375consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1376 where colour BoldText = IdrisColour Nothing True False True False
1377 colour UnderlineText = IdrisColour Nothing True True False False
1378 colour ItalicText = IdrisColour Nothing True False False True
1379consoleDecorate ist (AnnTerm _ _) = id
1380consoleDecorate ist (AnnSearchResult _) = id
1381consoleDecorate ist (AnnErr _) = id
1383isPostulateName :: Name -> IState -> Bool
1384isPostulateName n ist = S.member n (idris_postulates ist)
1386-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1387prettyImp :: PPOption -- ^^ pretty printing options
1388 -> PTerm -- ^^ the term to pretty-print
1389 -> Doc OutputAnnotation
1390prettyImp impl = pprintPTerm impl [] [] []
1392-- | Serialise something to base64 using its Binary instance.
1394-- | Do the right thing for rendering a term in an IState
1395prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1396prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1398-- | Pretty-print a high-level Idris term in some bindings context with infix info
1399pprintPTerm :: PPOption -- ^^ pretty printing options
1400 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1401 -> [Name] -- ^^ names to always show in pi, even if not used
1402 -> [FixDecl] -- ^^ Fixity declarations
1403 -> PTerm -- ^^ the term to pretty-print
1404 -> Doc OutputAnnotation
1405pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1406 where
1407 startPrec = 0
1408 funcAppPrec = 10
1410 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1411 prettySe p bnd (PQuote r) =
1412 text "![" <> pretty r <> text "]"
1413 prettySe p bnd (PPatvar fc n) = pretty n
1414 prettySe p bnd e
1415 | Just str <- slist p bnd e = str
1416 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1417 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1418 prettySe p bnd (PLam fc n ty sc) =
1419 bracket p startPrec . group . align . hang 2 $
1420 text "\\" <> bindingOf n False <+> text "=>" <$>
1421 prettySe startPrec ((n, False):bnd) sc
1422 prettySe p bnd (PLet fc n ty v sc) =
1423 bracket p startPrec . group . align $
1424 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1425 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1426 prettySe p bnd (PPi (Exp l s _) n ty sc)
1427 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1428 bracket p startPrec . group $
1429 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1430 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1431 | otherwise =
1432 bracket p startPrec . group $
1433 group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1434 where
1435 st =
1436 case s of
1437 Static -> text "[static]" <> space
1438 _ -> empty
1439 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1440 | ppopt_impl ppo =
1441 bracket p startPrec $
1442 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1443 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1444 | otherwise = prettySe startPrec ((n, True):bnd) sc
1445 where
1446 st =
1447 case s of
1448 Static -> text "[static]" <> space
1449 _ -> empty
1450 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1451 bracket p startPrec $
1452 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1453 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1454 bracket p startPrec $
1455 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1456 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1457 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1458 | UN nm <- basename f
1459 , not (ppopt_impl ppo) && null (getShowArgs args) =
1460 prettyName True (ppopt_impl ppo) bnd f
1461 prettySe p bnd (PAppBind _ (PRef _ f) [])
1462 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1463 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1464 | UN nm <- basename op
1465 , not (tnull nm) &&
1466 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1467 case getShowArgs args of
1468 [] -> opName True
1469 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1470 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1471 in bracket p precedence $ inFix (getTm l) (getTm r)
1472 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1473 bracket p funcAppPrec $
1474 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1475 align (group (vsep (map (prettyArgS bnd) rest)))
1476 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1477 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1478 f = getFixity (opStr op)
1479 left = case f of
1480 Nothing -> funcAppPrec + 1
1481 Just (Infixl p') -> p'
1482 Just f' -> prec f' + 1
1483 right = case f of
1484 Nothing -> funcAppPrec + 1
1485 Just (Infixr p') -> p'
1486 Just f' -> prec f' + 1
1487 inFix l r = align . group $
1488 (prettySe left bnd l <+> opName False) <$>
1489 group (prettySe right bnd r)
1490 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1491 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1492 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1493 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1494 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1495 let args = getShowArgs as
1496 fp = prettySe (startPrec + 1) bnd f
1497 shownArgs = if ppopt_impl ppo then as else args
1498 in
1499 bracket p funcAppPrec . group $
1500 if null shownArgs
1501 then fp
1502 else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1503 prettySe p bnd (PCase _ scr cases) =
1504 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1505 indent 2 (vsep (map ppcase cases))
1506 where
1507 ppcase (l, r) = let prettyCase = prettySe startPrec
1508 ([(n, False) | n <- vars l] ++ bnd)
1509 in nest nestingSize $
1510 prettyCase l <+> text "=>" <+> prettyCase r
1511 -- Warning: this is a bit of a hack. At this stage, we don't have the
1512 -- global context, so we can't determine which names are constructors,
1513 -- which are types, and which are pattern variables on the LHS of the
1514 -- case pattern. We use the heuristic that names without a namespace
1515 -- are patvars, because right now case blocks in PTerms are always
1516 -- delaborated from TT before being sent to the pretty-printer. If they
1517 -- start getting printed directly, THIS WILL BREAK.
1518 -- Potential solution: add a list of known patvars to the cases in
1519 -- PCase, and have the delaborator fill it out, kind of like the pun
1520 -- disambiguation on PDPair.
1521 vars tm = filter noNS (allNamesIn tm)
1522 noNS (NS _ _) = False
1523 noNS _ = True
1525 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1526 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1527 prettySe p bnd (PResolveTC _) = text "resolvetc"
1528 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1529 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1530 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1531 prettySe p bnd (PEq _ lt rt l r)
1532 | ppopt_impl ppo =
1533 bracket p eqPrec $
1534 enclose lparen rparen eq <+>
1535 align (group (vsep (map (prettyArgS bnd)
1536 [PImp 0 False [] (sUN "A") lt,
1537 PImp 0 False [] (sUN "B") rt,
1538 PExp 0 [] (sUN "x") l,
1539 PExp 0 [] (sUN "y") r])))
1540 | otherwise =
1541 bracket p eqPrec . align . group $
1542 prettyTerm l <+> eq <$> group (prettyTerm r)
1543 where eq = annName eqTy (text "=")
1544 eqPrec = startPrec
1545 prettyTerm = prettySe (eqPrec + 1) bnd
1546 prettySe p bnd (PRewrite _ l r _) =
1547 bracket p startPrec $
1548 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1549 prettySe p bnd (PTyped l r) =
1550 lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1551 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1552 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1553 align . group . vsep . punctuate (ann comma) $
1554 map (prettySe startPrec bnd) elts
1555 where ann = case pun of
1556 TypeOrTerm -> id
1557 IsType -> annName pairTy
1558 IsTerm -> annName pairCon
1559 prettySe p bnd (PDPair _ pun l t r) =
1560 annotated lparen <>
1561 left <+>
1562 annotated (text "**") <+>
1563 prettySe startPrec (addBinding bnd) r <>
1564 annotated rparen
1565 where annotated = case pun of
1566 IsType -> annName sigmaTy
1567 IsTerm -> annName existsCon
1568 TypeOrTerm -> id
1569 (left, addBinding) = case (l, pun) of
1570 (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1571 _ -> (prettySe startPrec bnd l, id )
1572 prettySe p bnd (PAlternative a as) =
1573 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1574 where
1575 prettyAs =
1576 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1577 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1578 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1579 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1580 -- XXX: add pretty for tactics
1581 prettySe p bnd (PProof ts) =
1582 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1583 prettySe p bnd (PTactics ts) =
1584 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1585 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1586 prettySe p bnd (PReturn f) = kwd "return"
1587 prettySe p bnd PImpossible = kwd "impossible"
1588 prettySe p bnd Placeholder = text "_"
1589 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1590 prettySe p bnd (PCoerced t) = prettySe p bnd t
1591 prettySe p bnd (PElabError s) = pretty s
1592 -- Quasiquote pprinting ignores bound vars
1593 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1594 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1595 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1597 prettySe p bnd _ = text "missing pretty-printer for term"
1599 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1600 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1601 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1602 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1604 prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1605 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1606 prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1607 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1609 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1610 annName n = annotate (AnnName n Nothing Nothing Nothing)
1612 opStr :: Name -> String
1613 opStr (NS n _) = opStr n
1614 opStr (UN n) = T.unpack n
1616 basename :: Name -> Name
1617 basename (NS n _) = basename n
1618 basename n = n
1620 slist' p bnd (PApp _ (PRef _ nil) _)
1621 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1622 slist' p bnd (PRef _ nil)
1623 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1624 slist' p bnd (PApp _ (PRef _ cons) args)
1625 | nsroot cons == sUN "::",
1626 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1627 all isImp imps,
1628 Just tl' <- slist' p bnd tl
1629 = Just (hd:tl')
1630 where
1631 isImp (PImp {}) = True
1632 isImp _ = False
1633 slist' _ _ tm = Nothing
1635 slist p bnd e | Just es <- slist' p bnd e = Just $
1636 case es of [] -> annotate (AnnData "" "") $ text "[]"
1637 [x] -> enclose left right . group $
1638 prettySe p bnd x
1639 xs -> (enclose left right .
1640 align . group . vsep .
1641 punctuate comma .
1642 map (prettySe p bnd)) xs
1643 where left = (annotate (AnnData "" "") (text "["))
1644 right = (annotate (AnnData "" "") (text "]"))
1645 comma = (annotate (AnnData "" "") (text ","))
1646 slist _ _ _ = Nothing
1648 pairElts :: PTerm -> Maybe [PTerm]
1649 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1650 | otherwise = Just [x, y]
1651 pairElts _ = Nothing
1653 natns = "Prelude.Nat."
1655 snat p (PRef _ z)
1656 | show z == (natns++"Z") || show z == "Z" = Just 0
1657 snat p (PApp _ s [PExp {getTm=n}])
1658 | show s == (natns++"S") || show s == "S",
1659 Just n' <- snat p n
1660 = Just $ 1 + n'
1661 snat _ _ = Nothing
1663 bracket outer inner doc
1664 | outer > inner = lparen <> doc <> rparen
1665 | otherwise = doc
1667 kwd = annotate AnnKeyword . text
1669 fixities :: M.Map String Fixity
1670 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1672 getFixity :: String -> Maybe Fixity
1673 getFixity = flip M.lookup fixities
1675-- | Determine whether a name was the one inserted for a hole or
1676-- guess by the delaborator
1677isHoleName :: Name -> Bool
1678isHoleName (UN n) = n == T.pack "[__]"
1679isHoleName _ = False
1681-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1682containsHole :: PTerm -> Bool
1683containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]
1685-- | Pretty-printer helper for the binding site of a name
1686bindingOf :: Name -- ^^ the bound name
1687 -> Bool -- ^^ whether the name is implicit
1688 -> Doc OutputAnnotation
1689bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1691-- | Pretty-printer helper for names that attaches the correct annotations
1692prettyName
1693 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1694 -> Bool -- ^^ whether to show namespaces
1695 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1696 -> Name -- ^^ the name to pprint
1697 -> Doc OutputAnnotation
1698prettyName infixParen showNS bnd n
1699 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1700 | (UN n') <- n, T.unpack n' == "_" = text "_"
1701 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1702 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1703 where fullName = text nameSpace <> parenthesise (text (baseName n))
1704 baseName (UN n) = T.unpack n
1705 baseName (NS n ns) = baseName n
1706 baseName (MN i s) = T.unpack s
1707 baseName other = show other
1708 nameSpace = case n of
1709 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1710 _ -> ""
1711 isInfix = case baseName n of
1712 "" -> False
1713 (c : _) -> not (isAlpha c)
1714 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1717showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1718showCImp ppo (PClause _ n l ws r w)
1719 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1720 <+> text "where" <+> text (show w)
1721 where
1722 showWs [] = empty
1723 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1724showCImp ppo (PWith _ n l ws r pn w)
1725 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1726 <+> braces (text (show w))
1727 where
1728 showWs [] = empty
1729 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1732showDImp :: PPOption -> PData -> Doc OutputAnnotation
1733showDImp ppo (PDatadecl n ty cons)
1734 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1735 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1737showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1738showDecls o ds = vsep (map (showDeclImp o) ds)
1740showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1741showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1742showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1743 indent 2 (vsep (map (showCImp o) cs))
1744showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1745showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1746showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1747showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1748showDeclImp o (PClass _ _ _ cs n ps _ ds)
1749 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1750showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)
1751 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1752showDeclImp _ _ = text "..."
1753-- showDeclImp (PImport o) = "import " ++ o
1755instance Show (Doc OutputAnnotation) where
1756 show = flip (displayS . renderCompact) ""
1758getImps :: [PArg] -> [(Name, PTerm)]
1759getImps [] = []
1760getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1761getImps (_ : xs) = getImps xs
1763getExps :: [PArg] -> [PTerm]
1764getExps [] = []
1765getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1766getExps (_ : xs) = getExps xs
1768getShowArgs :: [PArg] -> [PArg]
1769getShowArgs [] = []
1770getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1771getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1772 | PImp _ _ _ _ tm <- e
1773 , containsHole tm = e : getShowArgs xs
1774getShowArgs (_ : xs) = getShowArgs xs
1776getConsts :: [PArg] -> [PTerm]
1777getConsts [] = []
1778getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1779getConsts (_ : xs) = getConsts xs
1781getAll :: [PArg] -> [PTerm]
1782getAll = map getTm
1785-- | Show Idris name
1786showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1787 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1788 -> PPOption -- ^^ pretty printing options
1789 -> Bool -- ^^ whether to colourise
1790 -> Name -- ^^ the term to show
1791 -> String
1792showName ist bnd ppo colour n = case ist of
1793 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1794 Nothing -> showbasic n
1795 where name = if ppopt_impl ppo then show n else showbasic n
1796 showbasic n@(UN _) = showCG n
1797 showbasic (MN i s) = str s
1798 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1799 showbasic (SN s) = show s
1800 fst3 (x, _, _) = x
1801 colourise n t = let ctxt' = fmap tt_ctxt ist in
1802 case ctxt' of
1803 Nothing -> name
1804 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1805 else colouriseBound t name
1806 | isDConName n ctxt -> colouriseData t name
1807 | isFnName n ctxt -> colouriseFun t name
1808 | isTConName n ctxt -> colouriseType t name
1809 -- The assumption is that if a name is not bound and does not exist in the
1810 -- global context, then we're somewhere in which implicit info has been lost
1811 -- (like error messages). Thus, unknown vars are colourised as implicits.
1812 | otherwise -> colouriseImplicit t name
1814showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1815 -> PTerm -- ^^ the term to show
1816 -> String
1817showTm ist = displayDecorated (consoleDecorate ist) .
1818 renderPretty 0.8 100000 .
1819 prettyImp (ppOptionIst ist)
1821-- | Show a term with implicits, no colours
1822showTmImpls :: PTerm -> String
1823showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1827instance Sized PTerm where
1828 size (PQuote rawTerm) = size rawTerm
1829 size (PRef fc name) = size name
1830 size (PLam fc name ty bdy) = 1 + size ty + size bdy
1831 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1832 size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1833 size (PTyped trm ty) = 1 + size trm + size ty
1834 size (PApp fc name args) = 1 + size args
1835 size (PAppBind fc name args) = 1 + size args
1836 size (PCase fc trm bdy) = 1 + size trm + size bdy
1837 size (PTrue fc _) = 1
1838 size (PRefl fc _) = 1
1839 size (PResolveTC fc) = 1
1840 size (PEq fc _ _ left right) = 1 + size left + size right
1841 size (PRewrite fc left right _) = 1 + size left + size right
1842 size (PPair fc _ left right) = 1 + size left + size right
1843 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1844 size (PAlternative a alts) = 1 + size alts
1845 size (PHidden hidden) = size hidden
1846 size (PUnifyLog tm) = size tm
1847 size (PDisamb _ tm) = size tm
1848 size (PNoImplicits tm) = size tm
1849 size PType = 1
1850 size (PUniverse _) = 1
1851 size (PConstant const) = 1 + size const
1852 size Placeholder = 1
1853 size (PDoBlock dos) = 1 + size dos
1854 size (PIdiom fc term) = 1 + size term
1855 size (PReturn fc) = 1
1856 size (PMetavar name) = 1
1857 size (PProof tactics) = size tactics
1858 size (PElabError err) = size err
1859 size PImpossible = 1
1860 size _ = 0
1862getPArity :: PTerm -> Int
1863getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1864getPArity _ = 0
1866-- Return all names, free or globally bound, in the given term.
1868allNamesIn :: PTerm -> [Name]
1869allNamesIn tm = nub $ ni [] tm
1870 where -- TODO THINK added niTacImp, but is it right?
1871 ni env (PRef _ n)
1872 | not (n `elem` env) = [n]
1873 ni env (PPatvar _ n) = [n]
1874 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1875 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1876 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1877 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1878 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1879 ni env (PHidden tm) = ni env tm
1880 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1881 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1882 ni env (PTyped l r) = ni env l ++ ni env r
1883 ni env (PPair _ _ l r) = ni env l ++ ni env r
1884 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1885 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1886 ni env (PAlternative a ls) = concatMap (ni env) ls
1887 ni env (PUnifyLog tm) = ni env tm
1888 ni env (PDisamb _ tm) = ni env tm
1889 ni env (PNoImplicits tm) = ni env tm
1890 ni env _ = []
1892 niTacImp env (TacImp _ _ scr) = ni env scr
1893 niTacImp _ _ = []
1895-- Return all names defined in binders in the given term
1896boundNamesIn :: PTerm -> [Name]
1897boundNamesIn tm = nub $ ni tm
1898 where -- TODO THINK Added niTacImp, but is it right?
1899 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1900 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1901 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1902 ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)
1903 ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1904 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1905 ni (PEq _ _ _ l r) = ni l ++ ni r
1906 ni (PRewrite _ l r _) = ni l ++ ni r
1907 ni (PTyped l r) = ni l ++ ni r
1908 ni (PPair _ _ l r) = ni l ++ ni r
1909 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1910 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1911 ni (PAlternative a as) = concatMap (ni) as
1912 ni (PHidden tm) = ni tm
1913 ni (PUnifyLog tm) = ni tm
1914 ni (PDisamb _ tm) = ni tm
1915 ni (PNoImplicits tm) = ni tm
1916 ni _ = []
1918 niTacImp (TacImp _ _ scr) = ni scr
1919 niTacImp _ = []
1921-- Return names which are valid implicits in the given term (type).
1922implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1923implicitNamesIn uvars ist tm = nub $ ni [] tm
1924 where
1925 ni env (PRef _ n)
1926 | not (n `elem` env)
1927 = case lookupTy n (tt_ctxt ist) of
1928 [] -> [n]
1929 _ -> if n `elem` uvars then [n] else []
1930 ni env (PApp _ f@(PRef _ n) as)
1931 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1932 | otherwise = concatMap (ni env) (map getTm as)
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) = 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-- Return names which are free in the given term.
1955namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1956namesIn uvars ist tm = nub $ ni [] tm
1957 where
1958 ni env (PRef _ n)
1959 | not (n `elem` env)
1960 = case lookupTy n (tt_ctxt ist) of
1961 [] -> [n]
1962 _ -> if n `elem` (map fst uvars) then [n] else []
1963 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1964 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1965 ni env (PCase _ c os) = ni env c ++
1966 -- names in 'os', not counting the names bound in the cases
1967 (nub (concatMap (ni env) (map snd os))
1968 \\ nub (concatMap (ni env) (map fst os)))
1969 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1970 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1971 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1972 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1973 ni env (PTyped l r) = ni env l ++ ni env r
1974 ni env (PPair _ _ l r) = ni env l ++ ni env r
1975 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1976 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1977 ni env (PAlternative a as) = concatMap (ni env) as
1978 ni env (PHidden tm) = ni env tm
1979 ni env (PUnifyLog tm) = ni env tm
1980 ni env (PDisamb _ tm) = ni env tm
1981 ni env (PNoImplicits tm) = ni env tm
1982 ni env _ = []
1984 niTacImp env (TacImp _ _ scr) = ni env scr
1985 niTacImp _ _ = []
1987-- Return which of the given names are used in the given term.
1989usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1990usedNamesIn vars ist tm = nub $ ni [] tm
1991 where -- TODO THINK added niTacImp, but is it right?
1992 ni env (PRef _ n)
1993 | n `elem` vars && not (n `elem` env)
1994 = case lookupDefExact n (tt_ctxt ist) of
1995 Nothing -> [n]
1996 _ -> []
1997 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1998 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1999 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2000 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
2001 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2002 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
2003 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2004 ni env (PTyped l r) = ni env l ++ ni env r
2005 ni env (PPair _ _ l r) = ni env l ++ ni env r
2006 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
2007 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
2008 ni env (PAlternative a as) = concatMap (ni env) as
2009 ni env (PHidden tm) = ni env tm
2010 ni env (PUnifyLog tm) = ni env tm
2011 ni env (PDisamb _ tm) = ni env tm
2012 ni env (PNoImplicits tm) = ni env tm
2013 ni env _ = []
2015 niTacImp env (TacImp _ _ scr) = ni env scr
2016 niTacImp _ _ = []
2018-- Return the list of inaccessible (= dotted) positions for a name.
2019getErasureInfo :: IState -> Name -> [Int]
2020getErasureInfo ist n =
2021 case lookupCtxtExact n (idris_optimisation ist) of
2022 Just (Optimise inacc detagg) -> map fst inacc
2023 Nothing -> []