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