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