git.iko.soy/Idris-dev
on 8935fed help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
2027 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 | Browse [String]
412 | MakeDoc String -- IdrisDoc
413 | Warranty
414 | PrintDef Name
415 | PPrint OutputFmt Int PTerm
416 | TransformInfo Name
417 -- Debugging commands
418 | DebugInfo Name
419 | DebugUnify PTerm PTerm
421data OutputFmt = HTMLOutput | LaTeXOutput
423data Opt = Filename String
424 | Quiet
425 | NoBanner
426 | ColourREPL Bool
427 | Idemode
428 | IdemodeSocket
429 | ShowLibs
430 | ShowLibdir
431 | ShowIncs
432 | ShowPkgs
433 | NoBasePkgs
434 | NoPrelude
435 | NoBuiltins -- only for the really primitive stuff!
436 | NoREPL
437 | OLogging Int
438 | Output String
439 | Interface
440 | TypeCase
441 | TypeInType
442 | DefaultTotal
443 | DefaultPartial
444 | WarnPartial
445 | WarnReach
446 | NoCoverage
447 | ErrContext
448 | ShowImpl
449 | Verbose
450 | Port String -- REPL TCP port
451 | IBCSubDir String
452 | ImportDir String
453 | PkgBuild String
454 | PkgInstall String
455 | PkgClean String
456 | PkgCheck String
457 | PkgREPL String
458 | PkgMkDoc String -- IdrisDoc
459 | PkgTest String
460 | PkgIndex FilePath
461 | WarnOnly
462 | Pkg String
463 | BCAsm String
464 | DumpDefun String
465 | DumpCases String
466 | UseCodegen Codegen
467 | OutputTy OutputType
468 | Extension LanguageExt
469 | InterpretScript String
470 | EvalExpr String
471 | TargetTriple String
472 | TargetCPU String
473 | OptLevel Int
474 | AddOpt Optimisation
475 | RemoveOpt Optimisation
476 | Client String
477 | ShowOrigErr
478 | AutoWidth -- ^ Automatically adjust terminal width
479 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
480 | UseConsoleWidth ConsoleWidth
481 deriving (Show, Eq)
483-- Parsed declarations
485data Fixity = Infixl { prec :: Int }
486 | Infixr { prec :: Int }
487 | InfixN { prec :: Int }
488 | PrefixN { prec :: Int }
489 deriving Eq
490{-!
491deriving instance Binary Fixity
492deriving instance NFData Fixity
493!-}
495instance Show Fixity where
496 show (Infixl i) = "infixl " ++ show i
497 show (Infixr i) = "infixr " ++ show i
498 show (InfixN i) = "infix " ++ show i
499 show (PrefixN i) = "prefix " ++ show i
501data FixDecl = Fix Fixity String
502 deriving Eq
504instance Show FixDecl where
505 show (Fix f s) = show f ++ " " ++ s
507{-!
508deriving instance Binary FixDecl
509deriving instance NFData FixDecl
510!-}
512instance Ord FixDecl where
513 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
516data Static = Static | Dynamic
517 deriving (Show, Eq, Data, Typeable)
518{-!
519deriving instance Binary Static
520deriving instance NFData Static
521!-}
523-- Mark bindings with their explicitness, and laziness
524data Plicity = Imp { pargopts :: [ArgOpt],
525 pstatic :: Static,
526 pparam :: Bool,
527 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
528 }
529 | Exp { pargopts :: [ArgOpt],
530 pstatic :: Static,
531 pparam :: Bool } -- this is a param (rather than index)
532 | Constraint { pargopts :: [ArgOpt],
533 pstatic :: Static }
534 | TacImp { pargopts :: [ArgOpt],
535 pstatic :: Static,
536 pscript :: PTerm }
537 deriving (Show, Eq, Data, Typeable)
539{-!
540deriving instance Binary Plicity
541deriving instance NFData Plicity
542!-}
544is_scoped :: Plicity -> Maybe ImplicitInfo
545is_scoped (Imp _ _ _ s) = s
546is_scoped _ = Nothing
548impl = Imp [] Dynamic False Nothing
549forall_imp = Imp [] Dynamic False (Just (Impl False))
550forall_constraint = Imp [] Dynamic False (Just (Impl True))
551expl = Exp [] Dynamic False
552expl_param = Exp [] Dynamic True
553constraint = Constraint [] Static
554tacimpl t = TacImp [] Dynamic t
556data FnOpt = Inlinable -- always evaluate when simplifying
557 | TotalFn | PartialFn | CoveringFn
558 | Coinductive | AssertTotal
559 | Dictionary -- type class dictionary, eval only when
560 -- a function argument, and further evaluation resutls
561 | Implicit -- implicit coercion
562 | NoImplicit -- do not apply implicit coercions
563 | CExport String -- export, with a C name
564 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
565 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
566 | Reflection -- a reflecting function, compile-time only
567 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
568 | Constructor -- Data constructor type
569 | AutoHint -- use in auto implicit search
570 deriving (Show, Eq)
571{-!
572deriving instance Binary FnOpt
573deriving instance NFData FnOpt
574!-}
576type FnOpts = [FnOpt]
578inlinable :: FnOpts -> Bool
579inlinable = elem Inlinable
581dictionary :: FnOpts -> Bool
582dictionary = elem Dictionary
586-- | Type provider - what to provide
587data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
588 | ProvPostulate t -- ^ goal type must be Type, so only term
589 deriving (Show, Eq, Functor)
591type ProvideWhat = ProvideWhat' PTerm
593-- | Top-level declarations such as compiler directives, definitions,
594-- datatypes and typeclasses.
595data PDecl' t
596 = PFix FC Fixity [String] -- ^ Fixity declaration
597 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
598 | PPostulate Bool -- external def if true
599 (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
600 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
601 | PCAF FC Name t -- ^ Top level constant
602 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
603 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
604 | PNamespace String [PDecl' t] -- ^ New namespace
605 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
606 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
607 [(Name, t)] -- constraints
608 Name
609 [(Name, t)] -- parameters
610 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
611 [Name] -- determining parameters
612 [PDecl' t] -- declarations
613 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
614 -- class name, parameters, method declarations
615 | PInstance
616 (Docstring (Either Err PTerm)) -- Instance docs
617 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
618 SyntaxInfo
619 FC [(Name, t)] -- constraints
620 Name -- class
621 [t] -- parameters
622 t -- full instance type
623 (Maybe Name) -- explicit name
624 [PDecl' t]
625 -- ^ Instance declaration: arguments are documentation, syntax info, source
626 -- location, constraints, class name, parameters, full instance
627 -- type, optional explicit name, and definitions
628 | PDSL Name (DSL' t) -- ^ DSL declaration
629 | PSyntax FC Syntax -- ^ Syntax definition
630 | PMutual FC [PDecl' t] -- ^ Mutual block
631 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
632 | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
633 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
634 -- bool is True, lhs and rhs must be convertible
635 deriving Functor
636{-!
637deriving instance Binary PDecl'
638deriving instance NFData PDecl'
639!-}
641-- | A set of instructions for things that need to happen in IState
642-- after a term elaboration when there's been reflected elaboration.
643data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
644 | RClausesInstrs Name [([Name], Term, Term)]
646-- | For elaborator state
647data EState = EState {
648 case_decls :: [(Name, PDecl)],
649 delayed_elab :: [Elab' EState ()],
650 new_tyDecls :: [RDeclInstructions]
651 }
653initEState :: EState
654initEState = EState [] [] []
656type ElabD a = Elab' EState a
658-- | One clause of a top-level definition. Term arguments to constructors are:
659--
660-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
661--
662-- 2. The list of extra 'with' patterns
663--
664-- 3. The right-hand side
665--
666-- 4. The where block (PDecl' t)
668data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
669 | PWith FC Name t [t] t (Maybe Name) [PDecl' t]
670 | PClauseR FC [t] t [PDecl' t]
671 | PWithR FC [t] t (Maybe Name) [PDecl' t]
672 deriving Functor
673{-!
674deriving instance Binary PClause'
675deriving instance NFData PClause'
676!-}
678-- | Data declaration
679data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
680 d_tcon :: t, -- ^ Type constructor
681 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
682 }
683 -- ^ Data declaration
684 | PLaterdecl { d_name :: Name, d_tcon :: t }
685 -- ^ "Placeholder" for data whose constructors are defined later
686 deriving Functor
687{-!
688deriving instance Binary PData'
689deriving instance NFData PData'
690!-}
692-- Handy to get a free function for applying PTerm -> PTerm functions
693-- across a program, by deriving Functor
695type PDecl = PDecl' PTerm
696type PData = PData' PTerm
697type PClause = PClause' PTerm
699-- get all the names declared in a decl
701declared :: PDecl -> [Name]
702declared (PFix _ _ _) = []
703declared (PTy _ _ _ _ _ n t) = [n]
704declared (PPostulate _ _ _ _ _ n t) = [n]
705declared (PClauses _ _ n _) = [] -- not a declaration
706declared (PCAF _ n _) = [n]
707declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
708 where fstt (_, _, a, _, _, _) = a
709declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
710declared (PParams _ _ ds) = concatMap declared ds
711declared (PNamespace _ ds) = concatMap declared ds
712declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
713declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms
714declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
715declared (PDSL n _) = [n]
716declared (PSyntax _ _) = []
717declared (PMutual _ ds) = concatMap declared ds
718declared (PDirective _) = []
720-- get the names declared, not counting nested parameter blocks
721tldeclared :: PDecl -> [Name]
722tldeclared (PFix _ _ _) = []
723tldeclared (PTy _ _ _ _ _ n t) = [n]
724tldeclared (PPostulate _ _ _ _ _ n t) = [n]
725tldeclared (PClauses _ _ n _) = [] -- not a declaration
726tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
727tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
728 where fstt (_, _, a, _, _, _) = a
729tldeclared (PParams _ _ ds) = []
730tldeclared (PMutual _ ds) = concatMap tldeclared ds
731tldeclared (PNamespace _ ds) = concatMap tldeclared ds
732tldeclared (PClass _ _ _ _ n _ _ _ ms) = concatMap tldeclared ms
733tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []
734tldeclared _ = []
736defined :: PDecl -> [Name]
737defined (PFix _ _ _) = []
738defined (PTy _ _ _ _ _ n t) = []
739defined (PPostulate _ _ _ _ _ n t) = []
740defined (PClauses _ _ n _) = [n] -- not a declaration
741defined (PCAF _ n _) = [n]
742defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
743 where fstt (_, _, a, _, _, _) = a
744defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
745defined (PParams _ _ ds) = concatMap defined ds
746defined (PNamespace _ ds) = concatMap defined ds
747defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
748defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms
749defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
750defined (PDSL n _) = [n]
751defined (PSyntax _ _) = []
752defined (PMutual _ ds) = concatMap defined ds
753defined (PDirective _) = []
754--defined _ = []
756updateN :: [(Name, Name)] -> Name -> Name
757updateN ns n | Just n' <- lookup n ns = n'
758updateN _ n = n
760updateNs :: [(Name, Name)] -> PTerm -> PTerm
761updateNs [] t = t
762updateNs ns t = mapPT updateRef t
763 where updateRef (PRef fc f) = PRef fc (updateN ns f)
764 updateRef t = t
766-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
767-- updateDNs [] t = t
768-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
769-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
770-- where updateCNs ns (PClause n l ts r ds)
771-- = PClause (updateN ns n) (fmap (updateNs ns) l)
772-- (map (fmap (updateNs ns)) ts)
773-- (fmap (updateNs ns) r)
774-- (map (updateDNs ns) ds)
775-- updateDNs ns c = c
777data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
779-- | High level language terms
780data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
781 | PRef FC Name -- ^ A reference to a variable
782 | PInferRef FC Name -- ^ A name to be defined later
783 | PPatvar FC Name -- ^ A pattern variable
784 | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
785 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
786 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
787 | PTyped PTerm PTerm -- ^ Term with explicit type
788 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
789 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
790 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
791 | PMatchApp FC Name -- ^ Make an application by type matching
792 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
793 | PTrue FC PunInfo -- ^ Unit type..?
794 | PRefl FC PTerm -- ^ The canonical proof of the equality type
795 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
796 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
797 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
798 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
799 | 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)
800 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
801 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
802 | PHidden PTerm -- ^ Irrelevant or hidden pattern
803 | PType -- ^ 'Type' type
804 | PUniverse Universe -- ^ Some universe
805 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
806 | PConstant Const -- ^ Builtin types
807 | Placeholder -- ^ Underscore
808 | PDoBlock [PDo] -- ^ Do notation
809 | PIdiom FC PTerm -- ^ Idiom brackets
810 | PReturn FC
811 | PMetavar Name -- ^ A metavariable, ?name
812 | PProof [PTactic] -- ^ Proof script
813 | PTactics [PTactic] -- ^ As PProof, but no auto solving
814 | PElabError Err -- ^ Error to report on elaboration
815 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
816 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
817 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
818 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
819 | PNoImplicits PTerm -- ^ never run implicit converions on the term
820 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
821 | PUnquote PTerm -- ^ ~Term
822 | PQuoteName Name -- ^ `{n}
823 | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script
824 deriving (Eq, Data, Typeable)
827{-!
828deriving instance Binary PTerm
829deriving instance NFData PTerm
830!-}
832mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
833mapPT f t = f (mpt t) where
834 mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
835 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
836 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
837 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
838 (fmap (mapPT f) g)
839 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
840 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
841 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
842 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
843 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
844 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
845 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
846 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
847 mpt (PHidden t) = PHidden (mapPT f t)
848 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
849 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
850 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
851 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
852 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
853 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
854 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
855 mpt x = x
858data PTactic' t = Intro [Name] | Intros | Focus Name
859 | Refine Name [Bool] | Rewrite t | DoUnify
860 | Induction t
861 | CaseTac t
862 | Equiv t
863 | Claim Name t
864 | Unfocus
865 | MatchRefine Name
866 | LetTac Name t | LetTacTy Name t t
867 | Exact t | Compute | Trivial | TCInstance
868 | ProofSearch Bool Bool Int (Maybe Name) [Name]
869 -- ^ the bool is whether to search recursively
870 | Solve
871 | Attack
872 | ProofState | ProofTerm | Undo
873 | Try (PTactic' t) (PTactic' t)
874 | TSeq (PTactic' t) (PTactic' t)
875 | ApplyTactic t -- see Language.Reflection module
876 | ByReflection t
877 | Reflect t
878 | Fill t
879 | GoalType String (PTactic' t)
880 | TCheck t
881 | TEval t
882 | TDocStr (Either Name Const)
883 | TSearch t
884 | Skip
885 | TFail [ErrorReportPart]
886 | Qed | Abandon
887 | SourceFC
888 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
889{-!
890deriving instance Binary PTactic'
891deriving instance NFData PTactic'
892!-}
893instance Sized a => Sized (PTactic' a) where
894 size (Intro nms) = 1 + size nms
895 size Intros = 1
896 size (Focus nm) = 1 + size nm
897 size (Refine nm bs) = 1 + size nm + length bs
898 size (Rewrite t) = 1 + size t
899 size (Induction t) = 1 + size t
900 size (LetTac nm t) = 1 + size nm + size t
901 size (Exact t) = 1 + size t
902 size Compute = 1
903 size Trivial = 1
904 size Solve = 1
905 size Attack = 1
906 size ProofState = 1
907 size ProofTerm = 1
908 size Undo = 1
909 size (Try l r) = 1 + size l + size r
910 size (TSeq l r) = 1 + size l + size r
911 size (ApplyTactic t) = 1 + size t
912 size (Reflect t) = 1 + size t
913 size (Fill t) = 1 + size t
914 size Qed = 1
915 size Abandon = 1
916 size Skip = 1
917 size (TFail ts) = 1 + size ts
918 size SourceFC = 1
920type PTactic = PTactic' PTerm
922data PDo' t = DoExp FC t
923 | DoBind FC Name t
924 | DoBindP FC t t [(t,t)]
925 | DoLet FC Name t t
926 | DoLetP FC t t
927 deriving (Eq, Functor, Data, Typeable)
928{-!
929deriving instance Binary PDo'
930deriving instance NFData PDo'
931!-}
933instance Sized a => Sized (PDo' a) where
934 size (DoExp fc t) = 1 + size fc + size t
935 size (DoBind fc nm t) = 1 + size fc + size nm + size t
936 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
937 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
938 size (DoLetP fc l r) = 1 + size fc + size l + size r
940type PDo = PDo' PTerm
942-- The priority gives a hint as to elaboration order. Best to elaborate
943-- things early which will help give a more concrete type to other
944-- variables, e.g. a before (interpTy a).
946data PArg' t = PImp { priority :: Int,
947 machine_inf :: Bool, -- true if the machine inferred it
948 argopts :: [ArgOpt],
949 pname :: Name, getTm :: t }
950 | PExp { priority :: Int,
951 argopts :: [ArgOpt],
952 pname :: Name,
953 getTm :: t }
954 | PConstraint { priority :: Int,
955 argopts :: [ArgOpt],
956 pname :: Name,
957 getTm :: t }
958 | PTacImplicit { priority :: Int,
959 argopts :: [ArgOpt],
960 pname :: Name,
961 getScript :: t,
962 getTm :: t }
963 deriving (Show, Eq, Functor, Data, Typeable)
965data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
966 deriving (Show, Eq, Data, Typeable)
968instance Sized a => Sized (PArg' a) where
969 size (PImp p _ l nm trm) = 1 + size nm + size trm
970 size (PExp p l nm trm) = 1 + size nm + size trm
971 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
972 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
974{-!
975deriving instance Binary PArg'
976deriving instance NFData PArg'
977!-}
979pimp n t mach = PImp 1 mach [] n t
980pexp t = PExp 1 [] (sMN 0 "arg") t
981pconst t = PConstraint 1 [] (sMN 0 "carg") t
982ptacimp n s t = PTacImplicit 2 [] n s t
984type PArg = PArg' PTerm
986-- | Get the highest FC in a term, if one exists
987highestFC :: PTerm -> Maybe FC
988highestFC (PQuote _) = Nothing
989highestFC (PRef fc _) = Just fc
990highestFC (PInferRef fc _) = Just fc
991highestFC (PPatvar fc _) = Just fc
992highestFC (PLam fc _ _ _) = Just fc
993highestFC (PPi _ _ _ _) = Nothing
994highestFC (PLet fc _ _ _ _) = Just fc
995highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
996highestFC (PApp fc _ _) = Just fc
997highestFC (PAppBind fc _ _) = Just fc
998highestFC (PMatchApp fc _) = Just fc
999highestFC (PCase fc _ _) = Just fc
1000highestFC (PTrue fc _) = Just fc
1001highestFC (PRefl fc _) = Just fc
1002highestFC (PResolveTC fc) = Just fc
1003highestFC (PEq fc _ _ _ _) = Just fc
1004highestFC (PRewrite fc _ _ _) = Just fc
1005highestFC (PPair fc _ _ _) = Just fc
1006highestFC (PDPair fc _ _ _ _) = Just fc
1007highestFC (PAs fc _ _) = Just fc
1008highestFC (PAlternative _ args) =
1009 case mapMaybe highestFC args of
1010 [] -> Nothing
1011 (fc:_) -> Just fc
1012highestFC (PHidden _) = Nothing
1013highestFC PType = Nothing
1014highestFC (PUniverse _) = Nothing
1015highestFC (PGoal fc _ _ _) = Just fc
1016highestFC (PConstant _) = Nothing
1017highestFC Placeholder = Nothing
1018highestFC (PDoBlock lines) =
1019 case map getDoFC lines of
1020 [] -> Nothing
1021 (fc:_) -> Just fc
1022 where
1023 getDoFC (DoExp fc t) = fc
1024 getDoFC (DoBind fc nm t) = fc
1025 getDoFC (DoBindP fc l r alts) = fc
1026 getDoFC (DoLet fc nm l r) = fc
1027 getDoFC (DoLetP fc l r) = fc
1029highestFC (PIdiom fc _) = Just fc
1030highestFC (PReturn fc) = Just fc
1031highestFC (PMetavar _) = Nothing
1032highestFC (PProof _) = Nothing
1033highestFC (PTactics _) = Nothing
1034highestFC (PElabError _) = Nothing
1035highestFC PImpossible = Nothing
1036highestFC (PCoerced tm) = highestFC tm
1037highestFC (PDisamb _ opts) = highestFC opts
1038highestFC (PUnifyLog tm) = highestFC tm
1039highestFC (PNoImplicits tm) = highestFC tm
1040highestFC (PQuasiquote _ _) = Nothing
1041highestFC (PUnquote tm) = highestFC tm
1042highestFC (PQuoteName _) = Nothing
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!-}
1081-- | Syntactic sugar info
1082data DSL' t = DSL { dsl_bind :: t,
1083 dsl_return :: t,
1084 dsl_apply :: t,
1085 dsl_pure :: t,
1086 dsl_var :: Maybe t,
1087 index_first :: Maybe t,
1088 index_next :: Maybe t,
1089 dsl_lambda :: Maybe t,
1090 dsl_let :: Maybe t,
1091 dsl_pi :: Maybe t
1093 deriving (Show, Functor)
1094{-!
1095deriving instance Binary DSL'
1096deriving instance NFData DSL'
1097!-}
1099type DSL = DSL' PTerm
1101data SynContext = PatternSyntax | TermSyntax | AnySyntax
1102 deriving Show
1103{-!
1104deriving instance Binary SynContext
1105deriving instance NFData SynContext
1106!-}
1108data Syntax = Rule [SSymbol] PTerm SynContext
1109 deriving Show
1111syntaxNames :: Syntax -> [Name]
1112syntaxNames (Rule syms _ _) = mapMaybe ename syms
1113 where ename (Keyword n) = Just n
1114 ename _ = Nothing
1116syntaxSymbols :: Syntax -> [SSymbol]
1117syntaxSymbols (Rule ss _ _) = ss
1118{-!
1119deriving instance Binary Syntax
1120deriving instance NFData Syntax
1121!-}
1123data SSymbol = Keyword Name
1124 | Symbol String
1125 | Binding Name
1126 | Expr Name
1127 | SimpleExpr Name
1128 deriving (Show, Eq)
1131{-!
1132deriving instance Binary SSymbol
1133deriving instance NFData SSymbol
1134!-}
1136newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1138emptySyntaxRules :: SyntaxRules
1139emptySyntaxRules = SyntaxRules []
1141updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1142updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1143 where
1144 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1146 ruleSort [] [] = EQ
1147 ruleSort [] _ = LT
1148 ruleSort _ [] = GT
1149 ruleSort (s1:ss1) (s2:ss2) =
1150 case symCompare s1 s2 of
1151 EQ -> ruleSort ss1 ss2
1152 r -> r
1154 -- Better than creating Ord instance for SSymbol since
1155 -- in general this ordering does not really make sense.
1156 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1157 symCompare (Keyword _) _ = LT
1158 symCompare (Symbol _) (Keyword _) = GT
1159 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1160 symCompare (Symbol _) _ = LT
1161 symCompare (Binding _) (Keyword _) = GT
1162 symCompare (Binding _) (Symbol _) = GT
1163 symCompare (Binding b1) (Binding b2) = compare b1 b2
1164 symCompare (Binding _) _ = LT
1165 symCompare (Expr _) (Keyword _) = GT
1166 symCompare (Expr _) (Symbol _) = GT
1167 symCompare (Expr _) (Binding _) = GT
1168 symCompare (Expr e1) (Expr e2) = compare e1 e2
1169 symCompare (Expr _) _ = LT
1170 symCompare (SimpleExpr _) (Keyword _) = GT
1171 symCompare (SimpleExpr _) (Symbol _) = GT
1172 symCompare (SimpleExpr _) (Binding _) = GT
1173 symCompare (SimpleExpr _) (Expr _) = GT
1174 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1176initDSL = DSL (PRef f (sUN ">>="))
1177 (PRef f (sUN "return"))
1178 (PRef f (sUN "<*>"))
1179 (PRef f (sUN "pure"))
1180 Nothing
1181 Nothing
1182 Nothing
1183 Nothing
1184 Nothing
1185 Nothing
1186 where f = fileFC "(builtin)"
1188data Using = UImplicit Name PTerm
1189 | UConstraint Name [Name]
1190 deriving (Show, Eq)
1191{-!
1192deriving instance Binary Using
1193deriving instance NFData Using
1194!-}
1196data SyntaxInfo = Syn { using :: [Using],
1197 syn_params :: [(Name, PTerm)],
1198 syn_namespace :: [String],
1199 no_imp :: [Name],
1200 imp_methods :: [Name], -- class methods. When expanding
1201 -- implicits, these should be expanded even under
1202 -- binders
1203 decoration :: Name -> Name,
1204 inPattern :: Bool,
1205 implicitAllowed :: Bool,
1206 maxline :: Maybe Int,
1207 mut_nesting :: Int,
1208 dsl_info :: DSL,
1209 syn_in_quasiquote :: Int }
1210 deriving Show
1211{-!
1212deriving instance NFData SyntaxInfo
1213deriving instance Binary SyntaxInfo
1214!-}
1216defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1218expandNS :: SyntaxInfo -> Name -> Name
1219expandNS syn n@(NS _ _) = n
1220expandNS syn n = case syn_namespace syn of
1221 [] -> n
1222 xs -> sNS n xs
1225-- For inferring types of things
1227bi = fileFC "builtin"
1229inferTy = sMN 0 "__Infer"
1230inferCon = sMN 0 "__infer"
1231inferDecl = PDatadecl inferTy
1232 PType
1233 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1234 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1235 (PRef bi inferTy)), bi, [])]
1236inferOpts = []
1238infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1239infP = P (TCon 6 0) inferTy (TType (UVal 0))
1241getInferTerm, getInferType :: Term -> Term
1242getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1243getInferTerm (App _ (App _ _ _) tm) = tm
1244getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1246getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1247 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1248 toTy (PVar t) = PVTy t
1249 toTy b = b
1250getInferType (App _ (App _ _ ty) _) = ty
1254-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1256primNames = [eqTy, eqCon, inferTy, inferCon]
1258unitTy = sUN "Unit"
1259unitCon = sUN "MkUnit"
1261falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1262 "The empty type, also known as the trivially false proposition." ++
1263 "\n\n" ++
1264 "Use `void` or `absurd` to prove anything if you have a variable " ++
1265 "of type `Void` in scope."
1266falseTy = sUN "Void"
1268pairTy = sNS (sUN "Pair") ["Builtins"]
1269pairCon = sNS (sUN "MkPair") ["Builtins"]
1271upairTy = sNS (sUN "UPair") ["Builtins"]
1272upairCon = sNS (sUN "MkUPair") ["Builtins"]
1274eqTy = sUN "="
1275eqCon = sUN "Refl"
1276eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1277 "The propositional equality type. A proof that `x` = `y`." ++
1278 "\n\n" ++
1279 "To use such a proof, pattern-match on it, and the two equal things will " ++
1280 "then need to be the _same_ pattern." ++
1281 "\n\n" ++
1282 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1283 "is possible to state equalities between values of potentially different " ++
1284 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1285 "\n\n" ++
1286 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1288eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1289 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1290 PType))
1291 [(reflDoc, reflParamDoc,
1292 eqCon, PPi impl (n "A") PType (
1293 PPi impl (n "x") (PRef bi (n "A"))
1294 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1295 pimp (n "B") Placeholder False,
1296 pexp (PRef bi (n "x")),
1297 pexp (PRef bi (n "x"))])), bi, [])]
1298 where n a = sUN a
1299 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1300 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1301 "shown that both sides are in fact equal."
1302 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1303 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1305eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1306 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1308 where n a = sUN a
1310eqOpts = []
1312-- | The special name to be used in the module documentation context -
1313-- not for use in the main definition context. The namespace around it
1314-- will determine the module to which the docs adhere.
1315modDocName :: Name
1316modDocName = sMN 0 "ModuleDocs"
1318-- Defined in builtins.idr
1319sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1320existsCon = sNS (sUN "MkSigma") ["Builtins"]
1322piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1323piBind = piBindp expl
1325piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1326piBindp p [] t = t
1327piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1330-- Pretty-printing declarations and terms
1332-- These "show" instances render to an absurdly wide screen because inserted line breaks
1333-- could interfere with interactive editing, which calls "show".
1335instance Show PTerm where
1336 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1338instance Show PDecl where
1339 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1341instance Show PClause where
1342 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1344instance Show PData where
1345 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1347instance Pretty PTerm OutputAnnotation where
1348 pretty = prettyImp defaultPPOption
1350-- | Colourise annotations according to an Idris state. It ignores the names
1351-- in the annotation, as there's no good way to show extended information on a
1352-- terminal.
1353consoleDecorate :: IState -> OutputAnnotation -> String -> String
1354consoleDecorate ist _ | not (idris_colourRepl ist) = id
1355consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1356 in if constIsType c
1357 then colouriseType theme
1358 else colouriseData theme
1359consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1360consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1361consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1362consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1363consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1364consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1365 theme = idris_colourTheme ist
1366 in case () of
1367 _ | isDConName n ctxt -> colouriseData theme
1368 _ | isFnName n ctxt -> colouriseFun theme
1369 _ | isTConName n ctxt -> colouriseType theme
1370 _ | isPostulateName n ist -> colourisePostulate theme
1371 _ | otherwise -> id -- don't colourise unknown names
1372consoleDecorate ist (AnnFC _) = id
1373consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1374 where colour BoldText = IdrisColour Nothing True False True False
1375 colour UnderlineText = IdrisColour Nothing True True False False
1376 colour ItalicText = IdrisColour Nothing True False False True
1377consoleDecorate ist (AnnTerm _ _) = id
1378consoleDecorate ist (AnnSearchResult _) = id
1379consoleDecorate ist (AnnErr _) = id
1381isPostulateName :: Name -> IState -> Bool
1382isPostulateName n ist = S.member n (idris_postulates ist)
1384-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1385prettyImp :: PPOption -- ^^ pretty printing options
1386 -> PTerm -- ^^ the term to pretty-print
1387 -> Doc OutputAnnotation
1388prettyImp impl = pprintPTerm impl [] [] []
1390-- | Serialise something to base64 using its Binary instance.
1392-- | Do the right thing for rendering a term in an IState
1393prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1394prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1396-- | Pretty-print a high-level Idris term in some bindings context with infix info
1397pprintPTerm :: PPOption -- ^^ pretty printing options
1398 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1399 -> [Name] -- ^^ names to always show in pi, even if not used
1400 -> [FixDecl] -- ^^ Fixity declarations
1401 -> PTerm -- ^^ the term to pretty-print
1402 -> Doc OutputAnnotation
1403pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1404 where
1405 startPrec = 0
1406 funcAppPrec = 10
1408 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1409 prettySe p bnd (PQuote r) =
1410 text "![" <> pretty r <> text "]"
1411 prettySe p bnd (PPatvar fc n) = pretty n
1412 prettySe p bnd e
1413 | Just str <- slist p bnd e = str
1414 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1415 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1416 prettySe p bnd (PLam fc n ty sc) =
1417 bracket p startPrec . group . align . hang 2 $
1418 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1419 prettySe startPrec ((n, False):bnd) sc
1420 prettySe p bnd (PLet fc n ty v sc) =
1421 bracket p startPrec . group . align $
1422 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1423 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1424 prettySe p bnd (PPi (Exp l s _) n ty sc)
1425 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1426 bracket p startPrec . group $
1427 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1428 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1429 | otherwise =
1430 bracket p startPrec . group $
1431 group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1432 where
1433 st =
1434 case s of
1435 Static -> text "[static]" <> space
1436 _ -> empty
1437 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1438 | ppopt_impl ppo =
1439 bracket p startPrec $
1440 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1441 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1442 | otherwise = prettySe startPrec ((n, True):bnd) sc
1443 where
1444 st =
1445 case s of
1446 Static -> text "[static]" <> space
1447 _ -> empty
1448 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1449 bracket p startPrec $
1450 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1451 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1452 bracket p startPrec $
1453 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1454 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1455 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1456 | UN nm <- basename f
1457 , not (ppopt_impl ppo) && null (getShowArgs args) =
1458 prettyName True (ppopt_impl ppo) bnd f
1459 prettySe p bnd (PAppBind _ (PRef _ f) [])
1460 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1461 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1462 | UN nm <- basename op
1463 , not (tnull nm) &&
1464 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1465 case getShowArgs args of
1466 [] -> opName True
1467 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1468 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1469 in bracket p precedence $ inFix (getTm l) (getTm r)
1470 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1471 bracket p funcAppPrec $
1472 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1473 align (group (vsep (map (prettyArgS bnd) rest)))
1474 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1475 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1476 f = getFixity (opStr op)
1477 left = case f of
1478 Nothing -> funcAppPrec + 1
1479 Just (Infixl p') -> p'
1480 Just f' -> prec f' + 1
1481 right = case f of
1482 Nothing -> funcAppPrec + 1
1483 Just (Infixr p') -> p'
1484 Just f' -> prec f' + 1
1485 inFix l r = align . group $
1486 (prettySe left bnd l <+> opName False) <$>
1487 group (prettySe right bnd r)
1488 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1489 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1490 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1491 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1492 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1493 let args = getShowArgs as
1494 fp = prettySe (startPrec + 1) bnd f
1495 shownArgs = if ppopt_impl ppo then as else args
1496 in
1497 bracket p funcAppPrec . group $
1498 if null shownArgs
1499 then fp
1500 else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1501 prettySe p bnd (PCase _ scr cases) =
1502 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1503 indent 2 (vsep (map ppcase cases))
1504 where
1505 ppcase (l, r) = let prettyCase = prettySe startPrec
1506 ([(n, False) | n <- vars l] ++ bnd)
1507 in nest nestingSize $
1508 prettyCase l <+> text "=>" <+> prettyCase r
1509 -- Warning: this is a bit of a hack. At this stage, we don't have the
1510 -- global context, so we can't determine which names are constructors,
1511 -- which are types, and which are pattern variables on the LHS of the
1512 -- case pattern. We use the heuristic that names without a namespace
1513 -- are patvars, because right now case blocks in PTerms are always
1514 -- delaborated from TT before being sent to the pretty-printer. If they
1515 -- start getting printed directly, THIS WILL BREAK.
1516 -- Potential solution: add a list of known patvars to the cases in
1517 -- PCase, and have the delaborator fill it out, kind of like the pun
1518 -- disambiguation on PDPair.
1519 vars tm = filter noNS (allNamesIn tm)
1520 noNS (NS _ _) = False
1521 noNS _ = True
1523 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1524 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1525 prettySe p bnd (PResolveTC _) = text "resolvetc"
1526 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1527 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1528 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1529 prettySe p bnd (PEq _ lt rt l r)
1530 | ppopt_impl ppo =
1531 bracket p eqPrec $
1532 enclose lparen rparen eq <+>
1533 align (group (vsep (map (prettyArgS bnd)
1534 [PImp 0 False [] (sUN "A") lt,
1535 PImp 0 False [] (sUN "B") rt,
1536 PExp 0 [] (sUN "x") l,
1537 PExp 0 [] (sUN "y") r])))
1538 | otherwise =
1539 bracket p eqPrec . align . group $
1540 prettyTerm l <+> eq <$> group (prettyTerm r)
1541 where eq = annName eqTy (text "=")
1542 eqPrec = startPrec
1543 prettyTerm = prettySe (eqPrec + 1) bnd
1544 prettySe p bnd (PRewrite _ l r _) =
1545 bracket p startPrec $
1546 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1547 prettySe p bnd (PTyped l r) =
1548 lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1549 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1550 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1551 align . group . vsep . punctuate (ann comma) $
1552 map (prettySe startPrec bnd) elts
1553 where ann = case pun of
1554 TypeOrTerm -> id
1555 IsType -> annName pairTy
1556 IsTerm -> annName pairCon
1557 prettySe p bnd (PDPair _ pun l t r) =
1558 annotated lparen <>
1559 left <+>
1560 annotated (text "**") <+>
1561 prettySe startPrec (addBinding bnd) r <>
1562 annotated rparen
1563 where annotated = case pun of
1564 IsType -> annName sigmaTy
1565 IsTerm -> annName existsCon
1566 TypeOrTerm -> id
1567 (left, addBinding) = case (l, pun) of
1568 (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1569 _ -> (prettySe startPrec bnd l, id )
1570 prettySe p bnd (PAlternative a as) =
1571 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1572 where
1573 prettyAs =
1574 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1575 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1576 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1577 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1578 -- XXX: add pretty for tactics
1579 prettySe p bnd (PProof ts) =
1580 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1581 prettySe p bnd (PTactics ts) =
1582 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1583 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1584 prettySe p bnd (PReturn f) = kwd "return"
1585 prettySe p bnd PImpossible = kwd "impossible"
1586 prettySe p bnd Placeholder = text "_"
1587 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1588 prettySe p bnd (PCoerced t) = prettySe p bnd t
1589 prettySe p bnd (PElabError s) = pretty s
1590 -- Quasiquote pprinting ignores bound vars
1591 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1592 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1593 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1594 prettySe p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1596 prettySe p bnd _ = text "missing pretty-printer for term"
1598 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1599 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1600 where display (UN n) = T.unpack n
1601 display (MN _ n) = T.unpack n
1602 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1603 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1604 display n = show n
1606 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1607 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1608 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1609 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1611 prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1612 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1613 prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1614 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1616 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1617 annName n = annotate (AnnName n Nothing Nothing Nothing)
1619 opStr :: Name -> String
1620 opStr (NS n _) = opStr n
1621 opStr (UN n) = T.unpack n
1623 basename :: Name -> Name
1624 basename (NS n _) = basename n
1625 basename n = n
1627 slist' _ _ e
1628 | containsHole e = Nothing
1629 slist' p bnd (PApp _ (PRef _ nil) _)
1630 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1631 slist' p bnd (PRef _ nil)
1632 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1633 slist' p bnd (PApp _ (PRef _ cons) args)
1634 | nsroot cons == sUN "::",
1635 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1636 all isImp imps,
1637 Just tl' <- slist' p bnd tl
1638 = Just (hd:tl')
1639 where
1640 isImp (PImp {}) = True
1641 isImp _ = False
1642 slist' _ _ tm = Nothing
1644 slist p bnd e | Just es <- slist' p bnd e = Just $
1645 case es of [] -> annotate (AnnData "" "") $ text "[]"
1646 [x] -> enclose left right . group $
1647 prettySe p bnd x
1648 xs -> (enclose left right .
1649 align . group . vsep .
1650 punctuate comma .
1651 map (prettySe p bnd)) xs
1652 where left = (annotate (AnnData "" "") (text "["))
1653 right = (annotate (AnnData "" "") (text "]"))
1654 comma = (annotate (AnnData "" "") (text ","))
1655 slist _ _ _ = Nothing
1657 pairElts :: PTerm -> Maybe [PTerm]
1658 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1659 | otherwise = Just [x, y]
1660 pairElts _ = Nothing
1662 natns = "Prelude.Nat."
1664 snat p (PRef _ z)
1665 | show z == (natns++"Z") || show z == "Z" = Just 0
1666 snat p (PApp _ s [PExp {getTm=n}])
1667 | show s == (natns++"S") || show s == "S",
1668 Just n' <- snat p n
1669 = Just $ 1 + n'
1670 snat _ _ = Nothing
1672 bracket outer inner doc
1673 | outer > inner = lparen <> doc <> rparen
1674 | otherwise = doc
1676 kwd = annotate AnnKeyword . text
1678 fixities :: M.Map String Fixity
1679 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1681 getFixity :: String -> Maybe Fixity
1682 getFixity = flip M.lookup fixities
1684-- | Determine whether a name was the one inserted for a hole or
1685-- guess by the delaborator
1686isHoleName :: Name -> Bool
1687isHoleName (UN n) = n == T.pack "[__]"
1688isHoleName _ = False
1690-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1691containsHole :: PTerm -> Bool
1692containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]
1694-- | Pretty-printer helper for names that attaches the correct annotations
1695prettyName
1696 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1697 -> Bool -- ^^ whether to show namespaces
1698 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1699 -> Name -- ^^ the name to pprint
1700 -> Doc OutputAnnotation
1701prettyName infixParen showNS bnd n
1702 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1703 | (UN n') <- n, T.unpack n' == "_" = text "_"
1704 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1705 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1706 where fullName = text nameSpace <> parenthesise (text (baseName n))
1707 baseName (UN n) = T.unpack n
1708 baseName (NS n ns) = baseName n
1709 baseName (MN i s) = T.unpack s
1710 baseName other = show other
1711 nameSpace = case n of
1712 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1713 _ -> ""
1714 isInfix = case baseName n of
1715 "" -> False
1716 (c : _) -> not (isAlpha c)
1717 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1720showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1721showCImp ppo (PClause _ n l ws r w)
1722 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1723 <+> text "where" <+> text (show w)
1724 where
1725 showWs [] = empty
1726 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1727showCImp ppo (PWith _ n l ws r pn w)
1728 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1729 <+> braces (text (show w))
1730 where
1731 showWs [] = empty
1732 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1735showDImp :: PPOption -> PData -> Doc OutputAnnotation
1736showDImp ppo (PDatadecl n ty cons)
1737 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1738 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1740showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1741showDecls o ds = vsep (map (showDeclImp o) ds)
1743showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1744showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1745showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1746 indent 2 (vsep (map (showCImp o) cs))
1747showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1748showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1749showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1750showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1751showDeclImp o (PClass _ _ _ cs n ps _ _ ds)
1752 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1753showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)
1754 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1755showDeclImp _ _ = text "..."
1756-- showDeclImp (PImport o) = "import " ++ o
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 _ _ = []
1896-- Return all names defined in binders in the given term
1897boundNamesIn :: PTerm -> [Name]
1898boundNamesIn tm = S.toList (ni S.empty tm)
1899 where -- TODO THINK Added niTacImp, but is it right?
1900 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
1901 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
1902 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
1903 ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc
1904 ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
1905 ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
1906 ni set (PEq _ _ _ l r) = ni (ni set l) r
1907 ni set (PRewrite _ l r _) = ni (ni set l) r
1908 ni set (PTyped l r) = ni (ni set l) r
1909 ni set (PPair _ _ l r) = ni (ni set l) r
1910 ni set (PDPair _ _ (PRef _ n) t r) = ni (ni set t) r
1911 ni set (PDPair _ _ l t r) = ni (ni (ni set l) t) r
1912 ni set (PAlternative a as) = niTms set as
1913 ni set (PHidden tm) = ni set tm
1914 ni set (PUnifyLog tm) = ni set tm
1915 ni set (PDisamb _ tm) = ni set tm
1916 ni set (PNoImplicits tm) = ni set tm
1917 ni set _ = set
1919 niTms set [] = set
1920 niTms set (x : xs) = niTms (ni set x) xs
1922 niTacImp set (TacImp _ _ scr) = ni set scr
1923 niTacImp set _ = set
1925-- Return names which are valid implicits in the given term (type).
1926implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1927implicitNamesIn uvars ist tm = nub $ ni [] tm
1928 where
1929 ni env (PRef _ n)
1930 | not (n `elem` env)
1931 = case lookupTy n (tt_ctxt ist) of
1932 [] -> [n]
1933 _ -> if n `elem` uvars then [n] else []
1934 ni env (PApp _ f@(PRef _ n) as)
1935 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1936 | otherwise = concatMap (ni env) (map getTm as)
1937 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1938 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1939 ni env (PCase _ c os) = ni env c ++
1940 -- names in 'os', not counting the names bound in the cases
1941 (nub (concatMap (ni env) (map snd os))
1942 \\ nub (concatMap (ni env) (map fst os)))
1943 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1944 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1945 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1946 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1947 ni env (PTyped l r) = ni env l ++ ni env r
1948 ni env (PPair _ _ l r) = ni env l ++ ni env r
1949 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1950 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1951 ni env (PAlternative a as) = concatMap (ni env) as
1952 ni env (PHidden tm) = ni env tm
1953 ni env (PUnifyLog tm) = ni env tm
1954 ni env (PDisamb _ tm) = ni env tm
1955 ni env (PNoImplicits tm) = ni env tm
1956 ni env _ = []
1958-- Return names which are free in the given term.
1959namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1960namesIn uvars ist tm = nub $ ni [] tm
1961 where
1962 ni env (PRef _ n)
1963 | not (n `elem` env)
1964 = case lookupTy n (tt_ctxt ist) of
1965 [] -> [n]
1966 _ -> if n `elem` (map fst uvars) then [n] else []
1967 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1968 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1969 ni env (PCase _ c os) = ni env c ++
1970 -- names in 'os', not counting the names bound in the cases
1971 (nub (concatMap (ni env) (map snd os))
1972 \\ nub (concatMap (ni env) (map fst os)))
1973 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1974 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1975 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1976 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1977 ni env (PTyped l r) = ni env l ++ ni env r
1978 ni env (PPair _ _ l r) = ni env l ++ ni env r
1979 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1980 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1981 ni env (PAlternative a as) = concatMap (ni env) as
1982 ni env (PHidden tm) = ni env tm
1983 ni env (PUnifyLog tm) = ni env tm
1984 ni env (PDisamb _ tm) = ni env tm
1985 ni env (PNoImplicits tm) = ni env tm
1986 ni env _ = []
1988 niTacImp env (TacImp _ _ scr) = ni env scr
1989 niTacImp _ _ = []
1991-- Return which of the given names are used in the given term.
1993usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1994usedNamesIn vars ist tm = nub $ ni [] tm
1995 where -- TODO THINK added niTacImp, but is it right?
1996 ni env (PRef _ n)
1997 | n `elem` vars && not (n `elem` env)
1998 = case lookupDefExact n (tt_ctxt ist) of
1999 Nothing -> [n]
2000 _ -> []
2001 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2002 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2003 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2004 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
2005 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2006 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
2007 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2008 ni env (PTyped l r) = ni env l ++ ni env r
2009 ni env (PPair _ _ l r) = ni env l ++ ni env r
2010 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
2011 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
2012 ni env (PAlternative a as) = concatMap (ni env) as
2013 ni env (PHidden tm) = ni env tm
2014 ni env (PUnifyLog tm) = ni env tm
2015 ni env (PDisamb _ tm) = ni env tm
2016 ni env (PNoImplicits tm) = ni env tm
2017 ni env _ = []
2019 niTacImp env (TacImp _ _ scr) = ni env scr
2020 niTacImp _ _ = []
2022-- Return the list of inaccessible (= dotted) positions for a name.
2023getErasureInfo :: IState -> Name -> [Int]
2024getErasureInfo ist n =
2025 case lookupCtxtExact n (idris_optimisation ist) of
2026 Just (Optimise inacc detagg) -> map fst inacc
2027 Nothing -> []