git.iko.soy/Idris-dev
on b4dbebd help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
2043 lines 84 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 Directive -- ^ Compiler directive.
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-- | The set of source directives
642data Directive = DLib Codegen String |
643 DLink Codegen String |
644 DFlag Codegen String |
645 DInclude Codegen String |
646 DHide Name |
647 DFreeze Name |
648 DAccess Accessibility |
649 DDefault Bool |
650 DLogging Integer |
651 DDynamicLibs [String] |
652 DNameHint Name [Name] |
653 DErrorHandlers Name Name [Name] |
654 DLanguage LanguageExt |
655 DUsed FC Name Name
657-- | A set of instructions for things that need to happen in IState
658-- after a term elaboration when there's been reflected elaboration.
659data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
660 | RClausesInstrs Name [([Name], Term, Term)]
662-- | For elaborator state
663data EState = EState {
664 case_decls :: [(Name, PDecl)],
665 delayed_elab :: [Elab' EState ()],
666 new_tyDecls :: [RDeclInstructions]
667 }
669initEState :: EState
670initEState = EState [] [] []
672type ElabD a = Elab' EState a
674-- | One clause of a top-level definition. Term arguments to constructors are:
675--
676-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
677--
678-- 2. The list of extra 'with' patterns
679--
680-- 3. The right-hand side
681--
682-- 4. The where block (PDecl' t)
684data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
685 | PWith FC Name t [t] t (Maybe Name) [PDecl' t]
686 | PClauseR FC [t] t [PDecl' t]
687 | PWithR FC [t] t (Maybe Name) [PDecl' t]
688 deriving Functor
689{-!
690deriving instance Binary PClause'
691deriving instance NFData PClause'
692!-}
694-- | Data declaration
695data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
696 d_tcon :: t, -- ^ Type constructor
697 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
698 }
699 -- ^ Data declaration
700 | PLaterdecl { d_name :: Name, d_tcon :: t }
701 -- ^ "Placeholder" for data whose constructors are defined later
702 deriving Functor
703{-!
704deriving instance Binary PData'
705deriving instance NFData PData'
706!-}
708-- Handy to get a free function for applying PTerm -> PTerm functions
709-- across a program, by deriving Functor
711type PDecl = PDecl' PTerm
712type PData = PData' PTerm
713type PClause = PClause' PTerm
715-- get all the names declared in a decl
717declared :: PDecl -> [Name]
718declared (PFix _ _ _) = []
719declared (PTy _ _ _ _ _ n t) = [n]
720declared (PPostulate _ _ _ _ _ n t) = [n]
721declared (PClauses _ _ n _) = [] -- not a declaration
722declared (PCAF _ n _) = [n]
723declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
724 where fstt (_, _, a, _, _, _) = a
725declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
726declared (PParams _ _ ds) = concatMap declared ds
727declared (PNamespace _ ds) = concatMap declared ds
728declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
729declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms
730declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
731declared (PDSL n _) = [n]
732declared (PSyntax _ _) = []
733declared (PMutual _ ds) = concatMap declared ds
734declared (PDirective _) = []
736-- get the names declared, not counting nested parameter blocks
737tldeclared :: PDecl -> [Name]
738tldeclared (PFix _ _ _) = []
739tldeclared (PTy _ _ _ _ _ n t) = [n]
740tldeclared (PPostulate _ _ _ _ _ n t) = [n]
741tldeclared (PClauses _ _ n _) = [] -- not a declaration
742tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
743tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
744 where fstt (_, _, a, _, _, _) = a
745tldeclared (PParams _ _ ds) = []
746tldeclared (PMutual _ ds) = concatMap tldeclared ds
747tldeclared (PNamespace _ ds) = concatMap tldeclared ds
748tldeclared (PClass _ _ _ _ n _ _ _ ms) = concatMap tldeclared ms
749tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []
750tldeclared _ = []
752defined :: PDecl -> [Name]
753defined (PFix _ _ _) = []
754defined (PTy _ _ _ _ _ n t) = []
755defined (PPostulate _ _ _ _ _ n t) = []
756defined (PClauses _ _ n _) = [n] -- not a declaration
757defined (PCAF _ n _) = [n]
758defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
759 where fstt (_, _, a, _, _, _) = a
760defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
761defined (PParams _ _ ds) = concatMap defined ds
762defined (PNamespace _ ds) = concatMap defined ds
763defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
764defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms
765defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
766defined (PDSL n _) = [n]
767defined (PSyntax _ _) = []
768defined (PMutual _ ds) = concatMap defined ds
769defined (PDirective _) = []
770--defined _ = []
772updateN :: [(Name, Name)] -> Name -> Name
773updateN ns n | Just n' <- lookup n ns = n'
774updateN _ n = n
776updateNs :: [(Name, Name)] -> PTerm -> PTerm
777updateNs [] t = t
778updateNs ns t = mapPT updateRef t
779 where updateRef (PRef fc f) = PRef fc (updateN ns f)
780 updateRef t = t
782-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
783-- updateDNs [] t = t
784-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
785-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
786-- where updateCNs ns (PClause n l ts r ds)
787-- = PClause (updateN ns n) (fmap (updateNs ns) l)
788-- (map (fmap (updateNs ns)) ts)
789-- (fmap (updateNs ns) r)
790-- (map (updateDNs ns) ds)
791-- updateDNs ns c = c
793data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
795-- | High level language terms
796data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
797 | PRef FC Name -- ^ A reference to a variable
798 | PInferRef FC Name -- ^ A name to be defined later
799 | PPatvar FC Name -- ^ A pattern variable
800 | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
801 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
802 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
803 | PTyped PTerm PTerm -- ^ Term with explicit type
804 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
805 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
806 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
807 | PMatchApp FC Name -- ^ Make an application by type matching
808 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
809 | PTrue FC PunInfo -- ^ Unit type..?
810 | PRefl FC PTerm -- ^ The canonical proof of the equality type
811 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
812 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
813 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
814 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
815 | 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)
816 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
817 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
818 | PHidden PTerm -- ^ Irrelevant or hidden pattern
819 | PType -- ^ 'Type' type
820 | PUniverse Universe -- ^ Some universe
821 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
822 | PConstant Const -- ^ Builtin types
823 | Placeholder -- ^ Underscore
824 | PDoBlock [PDo] -- ^ Do notation
825 | PIdiom FC PTerm -- ^ Idiom brackets
826 | PReturn FC
827 | PMetavar Name -- ^ A metavariable, ?name
828 | PProof [PTactic] -- ^ Proof script
829 | PTactics [PTactic] -- ^ As PProof, but no auto solving
830 | PElabError Err -- ^ Error to report on elaboration
831 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
832 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
833 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
834 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
835 | PNoImplicits PTerm -- ^ never run implicit converions on the term
836 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
837 | PUnquote PTerm -- ^ ~Term
838 | PQuoteName Name -- ^ `{n}
839 | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script
840 deriving (Eq, Data, Typeable)
843{-!
844deriving instance Binary PTerm
845deriving instance NFData PTerm
846!-}
848mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
849mapPT f t = f (mpt t) where
850 mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
851 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
852 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
853 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
854 (fmap (mapPT f) g)
855 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
856 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
857 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
858 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
859 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
860 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
861 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
862 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
863 mpt (PHidden t) = PHidden (mapPT f t)
864 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
865 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
866 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
867 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
868 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
869 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
870 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
871 mpt x = x
874data PTactic' t = Intro [Name] | Intros | Focus Name
875 | Refine Name [Bool] | Rewrite t | DoUnify
876 | Induction t
877 | CaseTac t
878 | Equiv t
879 | Claim Name t
880 | Unfocus
881 | MatchRefine Name
882 | LetTac Name t | LetTacTy Name t t
883 | Exact t | Compute | Trivial | TCInstance
884 | ProofSearch Bool Bool Int (Maybe Name) [Name]
885 -- ^ the bool is whether to search recursively
886 | Solve
887 | Attack
888 | ProofState | ProofTerm | Undo
889 | Try (PTactic' t) (PTactic' t)
890 | TSeq (PTactic' t) (PTactic' t)
891 | ApplyTactic t -- see Language.Reflection module
892 | ByReflection t
893 | Reflect t
894 | Fill t
895 | GoalType String (PTactic' t)
896 | TCheck t
897 | TEval t
898 | TDocStr (Either Name Const)
899 | TSearch t
900 | Skip
901 | TFail [ErrorReportPart]
902 | Qed | Abandon
903 | SourceFC
904 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
905{-!
906deriving instance Binary PTactic'
907deriving instance NFData PTactic'
908!-}
909instance Sized a => Sized (PTactic' a) where
910 size (Intro nms) = 1 + size nms
911 size Intros = 1
912 size (Focus nm) = 1 + size nm
913 size (Refine nm bs) = 1 + size nm + length bs
914 size (Rewrite t) = 1 + size t
915 size (Induction t) = 1 + size t
916 size (LetTac nm t) = 1 + size nm + size t
917 size (Exact t) = 1 + size t
918 size Compute = 1
919 size Trivial = 1
920 size Solve = 1
921 size Attack = 1
922 size ProofState = 1
923 size ProofTerm = 1
924 size Undo = 1
925 size (Try l r) = 1 + size l + size r
926 size (TSeq l r) = 1 + size l + size r
927 size (ApplyTactic t) = 1 + size t
928 size (Reflect t) = 1 + size t
929 size (Fill t) = 1 + size t
930 size Qed = 1
931 size Abandon = 1
932 size Skip = 1
933 size (TFail ts) = 1 + size ts
934 size SourceFC = 1
936type PTactic = PTactic' PTerm
938data PDo' t = DoExp FC t
939 | DoBind FC Name t
940 | DoBindP FC t t [(t,t)]
941 | DoLet FC Name t t
942 | DoLetP FC t t
943 deriving (Eq, Functor, Data, Typeable)
944{-!
945deriving instance Binary PDo'
946deriving instance NFData PDo'
947!-}
949instance Sized a => Sized (PDo' a) where
950 size (DoExp fc t) = 1 + size fc + size t
951 size (DoBind fc nm t) = 1 + size fc + size nm + size t
952 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
953 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
954 size (DoLetP fc l r) = 1 + size fc + size l + size r
956type PDo = PDo' PTerm
958-- The priority gives a hint as to elaboration order. Best to elaborate
959-- things early which will help give a more concrete type to other
960-- variables, e.g. a before (interpTy a).
962data PArg' t = PImp { priority :: Int,
963 machine_inf :: Bool, -- true if the machine inferred it
964 argopts :: [ArgOpt],
965 pname :: Name, getTm :: t }
966 | PExp { priority :: Int,
967 argopts :: [ArgOpt],
968 pname :: Name,
969 getTm :: t }
970 | PConstraint { priority :: Int,
971 argopts :: [ArgOpt],
972 pname :: Name,
973 getTm :: t }
974 | PTacImplicit { priority :: Int,
975 argopts :: [ArgOpt],
976 pname :: Name,
977 getScript :: t,
978 getTm :: t }
979 deriving (Show, Eq, Functor, Data, Typeable)
981data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
982 deriving (Show, Eq, Data, Typeable)
984instance Sized a => Sized (PArg' a) where
985 size (PImp p _ l nm trm) = 1 + size nm + size trm
986 size (PExp p l nm trm) = 1 + size nm + size trm
987 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
988 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
990{-!
991deriving instance Binary PArg'
992deriving instance NFData PArg'
993!-}
995pimp n t mach = PImp 1 mach [] n t
996pexp t = PExp 1 [] (sMN 0 "arg") t
997pconst t = PConstraint 1 [] (sMN 0 "carg") t
998ptacimp n s t = PTacImplicit 2 [] n s t
1000type PArg = PArg' PTerm
1002-- | Get the highest FC in a term, if one exists
1003highestFC :: PTerm -> Maybe FC
1004highestFC (PQuote _) = Nothing
1005highestFC (PRef fc _) = Just fc
1006highestFC (PInferRef fc _) = Just fc
1007highestFC (PPatvar fc _) = Just fc
1008highestFC (PLam fc _ _ _) = Just fc
1009highestFC (PPi _ _ _ _) = Nothing
1010highestFC (PLet fc _ _ _ _) = Just fc
1011highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1012highestFC (PApp fc _ _) = Just fc
1013highestFC (PAppBind fc _ _) = Just fc
1014highestFC (PMatchApp fc _) = Just fc
1015highestFC (PCase fc _ _) = Just fc
1016highestFC (PTrue fc _) = Just fc
1017highestFC (PRefl fc _) = Just fc
1018highestFC (PResolveTC fc) = Just fc
1019highestFC (PEq fc _ _ _ _) = Just fc
1020highestFC (PRewrite fc _ _ _) = Just fc
1021highestFC (PPair fc _ _ _) = Just fc
1022highestFC (PDPair fc _ _ _ _) = Just fc
1023highestFC (PAs fc _ _) = Just fc
1024highestFC (PAlternative _ args) =
1025 case mapMaybe highestFC args of
1026 [] -> Nothing
1027 (fc:_) -> Just fc
1028highestFC (PHidden _) = Nothing
1029highestFC PType = Nothing
1030highestFC (PUniverse _) = Nothing
1031highestFC (PGoal fc _ _ _) = Just fc
1032highestFC (PConstant _) = Nothing
1033highestFC Placeholder = Nothing
1034highestFC (PDoBlock lines) =
1035 case map getDoFC lines of
1036 [] -> Nothing
1037 (fc:_) -> Just fc
1038 where
1039 getDoFC (DoExp fc t) = fc
1040 getDoFC (DoBind fc nm t) = fc
1041 getDoFC (DoBindP fc l r alts) = fc
1042 getDoFC (DoLet fc nm l r) = fc
1043 getDoFC (DoLetP fc l r) = fc
1045highestFC (PIdiom fc _) = Just fc
1046highestFC (PReturn fc) = Just fc
1047highestFC (PMetavar _) = Nothing
1048highestFC (PProof _) = Nothing
1049highestFC (PTactics _) = Nothing
1050highestFC (PElabError _) = Nothing
1051highestFC PImpossible = Nothing
1052highestFC (PCoerced tm) = highestFC tm
1053highestFC (PDisamb _ opts) = highestFC opts
1054highestFC (PUnifyLog tm) = highestFC tm
1055highestFC (PNoImplicits tm) = highestFC tm
1056highestFC (PQuasiquote _ _) = Nothing
1057highestFC (PUnquote tm) = highestFC tm
1058highestFC (PQuoteName _) = Nothing
1060-- Type class data
1062data ClassInfo = CI { instanceName :: Name,
1063 class_methods :: [(Name, (FnOpts, PTerm))],
1064 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1065 class_default_superclasses :: [PDecl],
1066 class_params :: [Name],
1067 class_instances :: [Name],
1068 class_determiners :: [Int] }
1069 deriving Show
1070{-!
1071deriving instance Binary ClassInfo
1072deriving instance NFData ClassInfo
1073!-}
1075-- Type inference data
1077data TIData = TIPartial -- ^ a function with a partially defined type
1078 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1079 deriving Show
1081-- | Miscellaneous information about functions
1082data FnInfo = FnInfo { fn_params :: [Int] }
1083 deriving Show
1084{-!
1085deriving instance Binary FnInfo
1086deriving instance NFData FnInfo
1087!-}
1089data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1090 detaggable :: Bool }
1091 deriving Show
1092{-!
1093deriving instance Binary OptInfo
1094deriving instance NFData OptInfo
1095!-}
1097-- | Syntactic sugar info
1098data DSL' t = DSL { dsl_bind :: t,
1099 dsl_return :: t,
1100 dsl_apply :: t,
1101 dsl_pure :: t,
1102 dsl_var :: Maybe t,
1103 index_first :: Maybe t,
1104 index_next :: Maybe t,
1105 dsl_lambda :: Maybe t,
1106 dsl_let :: Maybe t,
1107 dsl_pi :: Maybe t
1109 deriving (Show, Functor)
1110{-!
1111deriving instance Binary DSL'
1112deriving instance NFData DSL'
1113!-}
1115type DSL = DSL' PTerm
1117data SynContext = PatternSyntax | TermSyntax | AnySyntax
1118 deriving Show
1119{-!
1120deriving instance Binary SynContext
1121deriving instance NFData SynContext
1122!-}
1124data Syntax = Rule [SSymbol] PTerm SynContext
1125 deriving Show
1127syntaxNames :: Syntax -> [Name]
1128syntaxNames (Rule syms _ _) = mapMaybe ename syms
1129 where ename (Keyword n) = Just n
1130 ename _ = Nothing
1132syntaxSymbols :: Syntax -> [SSymbol]
1133syntaxSymbols (Rule ss _ _) = ss
1134{-!
1135deriving instance Binary Syntax
1136deriving instance NFData Syntax
1137!-}
1139data SSymbol = Keyword Name
1140 | Symbol String
1141 | Binding Name
1142 | Expr Name
1143 | SimpleExpr Name
1144 deriving (Show, Eq)
1147{-!
1148deriving instance Binary SSymbol
1149deriving instance NFData SSymbol
1150!-}
1152newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1154emptySyntaxRules :: SyntaxRules
1155emptySyntaxRules = SyntaxRules []
1157updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1158updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1159 where
1160 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1162 ruleSort [] [] = EQ
1163 ruleSort [] _ = LT
1164 ruleSort _ [] = GT
1165 ruleSort (s1:ss1) (s2:ss2) =
1166 case symCompare s1 s2 of
1167 EQ -> ruleSort ss1 ss2
1168 r -> r
1170 -- Better than creating Ord instance for SSymbol since
1171 -- in general this ordering does not really make sense.
1172 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1173 symCompare (Keyword _) _ = LT
1174 symCompare (Symbol _) (Keyword _) = GT
1175 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1176 symCompare (Symbol _) _ = LT
1177 symCompare (Binding _) (Keyword _) = GT
1178 symCompare (Binding _) (Symbol _) = GT
1179 symCompare (Binding b1) (Binding b2) = compare b1 b2
1180 symCompare (Binding _) _ = LT
1181 symCompare (Expr _) (Keyword _) = GT
1182 symCompare (Expr _) (Symbol _) = GT
1183 symCompare (Expr _) (Binding _) = GT
1184 symCompare (Expr e1) (Expr e2) = compare e1 e2
1185 symCompare (Expr _) _ = LT
1186 symCompare (SimpleExpr _) (Keyword _) = GT
1187 symCompare (SimpleExpr _) (Symbol _) = GT
1188 symCompare (SimpleExpr _) (Binding _) = GT
1189 symCompare (SimpleExpr _) (Expr _) = GT
1190 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1192initDSL = DSL (PRef f (sUN ">>="))
1193 (PRef f (sUN "return"))
1194 (PRef f (sUN "<*>"))
1195 (PRef f (sUN "pure"))
1196 Nothing
1197 Nothing
1198 Nothing
1199 Nothing
1200 Nothing
1201 Nothing
1202 where f = fileFC "(builtin)"
1204data Using = UImplicit Name PTerm
1205 | UConstraint Name [Name]
1206 deriving (Show, Eq)
1207{-!
1208deriving instance Binary Using
1209deriving instance NFData Using
1210!-}
1212data SyntaxInfo = Syn { using :: [Using],
1213 syn_params :: [(Name, PTerm)],
1214 syn_namespace :: [String],
1215 no_imp :: [Name],
1216 imp_methods :: [Name], -- class methods. When expanding
1217 -- implicits, these should be expanded even under
1218 -- binders
1219 decoration :: Name -> Name,
1220 inPattern :: Bool,
1221 implicitAllowed :: Bool,
1222 maxline :: Maybe Int,
1223 mut_nesting :: Int,
1224 dsl_info :: DSL,
1225 syn_in_quasiquote :: Int }
1226 deriving Show
1227{-!
1228deriving instance NFData SyntaxInfo
1229deriving instance Binary SyntaxInfo
1230!-}
1232defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1234expandNS :: SyntaxInfo -> Name -> Name
1235expandNS syn n@(NS _ _) = n
1236expandNS syn n = case syn_namespace syn of
1237 [] -> n
1238 xs -> sNS n xs
1241-- For inferring types of things
1243bi = fileFC "builtin"
1245inferTy = sMN 0 "__Infer"
1246inferCon = sMN 0 "__infer"
1247inferDecl = PDatadecl inferTy
1248 PType
1249 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1250 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1251 (PRef bi inferTy)), bi, [])]
1252inferOpts = []
1254infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1255infP = P (TCon 6 0) inferTy (TType (UVal 0))
1257getInferTerm, getInferType :: Term -> Term
1258getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1259getInferTerm (App _ (App _ _ _) tm) = tm
1260getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1262getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1263 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1264 toTy (PVar t) = PVTy t
1265 toTy b = b
1266getInferType (App _ (App _ _ ty) _) = ty
1270-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1272primNames = [eqTy, eqCon, inferTy, inferCon]
1274unitTy = sUN "Unit"
1275unitCon = sUN "MkUnit"
1277falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1278 "The empty type, also known as the trivially false proposition." ++
1279 "\n\n" ++
1280 "Use `void` or `absurd` to prove anything if you have a variable " ++
1281 "of type `Void` in scope."
1282falseTy = sUN "Void"
1284pairTy = sNS (sUN "Pair") ["Builtins"]
1285pairCon = sNS (sUN "MkPair") ["Builtins"]
1287upairTy = sNS (sUN "UPair") ["Builtins"]
1288upairCon = sNS (sUN "MkUPair") ["Builtins"]
1290eqTy = sUN "="
1291eqCon = sUN "Refl"
1292eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1293 "The propositional equality type. A proof that `x` = `y`." ++
1294 "\n\n" ++
1295 "To use such a proof, pattern-match on it, and the two equal things will " ++
1296 "then need to be the _same_ pattern." ++
1297 "\n\n" ++
1298 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1299 "is possible to state equalities between values of potentially different " ++
1300 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1301 "\n\n" ++
1302 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1304eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1305 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1306 PType))
1307 [(reflDoc, reflParamDoc,
1308 eqCon, PPi impl (n "A") PType (
1309 PPi impl (n "x") (PRef bi (n "A"))
1310 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1311 pimp (n "B") Placeholder False,
1312 pexp (PRef bi (n "x")),
1313 pexp (PRef bi (n "x"))])), bi, [])]
1314 where n a = sUN a
1315 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1316 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1317 "shown that both sides are in fact equal."
1318 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1319 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1321eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1322 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1324 where n a = sUN a
1326eqOpts = []
1328-- | The special name to be used in the module documentation context -
1329-- not for use in the main definition context. The namespace around it
1330-- will determine the module to which the docs adhere.
1331modDocName :: Name
1332modDocName = sMN 0 "ModuleDocs"
1334-- Defined in builtins.idr
1335sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1336existsCon = sNS (sUN "MkSigma") ["Builtins"]
1338piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1339piBind = piBindp expl
1341piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1342piBindp p [] t = t
1343piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1346-- Pretty-printing declarations and terms
1348-- These "show" instances render to an absurdly wide screen because inserted line breaks
1349-- could interfere with interactive editing, which calls "show".
1351instance Show PTerm where
1352 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1354instance Show PDecl where
1355 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1357instance Show PClause where
1358 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1360instance Show PData where
1361 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1363instance Pretty PTerm OutputAnnotation where
1364 pretty = prettyImp defaultPPOption
1366-- | Colourise annotations according to an Idris state. It ignores the names
1367-- in the annotation, as there's no good way to show extended information on a
1368-- terminal.
1369consoleDecorate :: IState -> OutputAnnotation -> String -> String
1370consoleDecorate ist _ | not (idris_colourRepl ist) = id
1371consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1372 in if constIsType c
1373 then colouriseType theme
1374 else colouriseData theme
1375consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1376consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1377consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1378consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1379consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1380consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1381 theme = idris_colourTheme ist
1382 in case () of
1383 _ | isDConName n ctxt -> colouriseData theme
1384 _ | isFnName n ctxt -> colouriseFun theme
1385 _ | isTConName n ctxt -> colouriseType theme
1386 _ | isPostulateName n ist -> colourisePostulate theme
1387 _ | otherwise -> id -- don't colourise unknown names
1388consoleDecorate ist (AnnFC _) = id
1389consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1390 where colour BoldText = IdrisColour Nothing True False True False
1391 colour UnderlineText = IdrisColour Nothing True True False False
1392 colour ItalicText = IdrisColour Nothing True False False True
1393consoleDecorate ist (AnnTerm _ _) = id
1394consoleDecorate ist (AnnSearchResult _) = id
1395consoleDecorate ist (AnnErr _) = id
1397isPostulateName :: Name -> IState -> Bool
1398isPostulateName n ist = S.member n (idris_postulates ist)
1400-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1401prettyImp :: PPOption -- ^^ pretty printing options
1402 -> PTerm -- ^^ the term to pretty-print
1403 -> Doc OutputAnnotation
1404prettyImp impl = pprintPTerm impl [] [] []
1406-- | Serialise something to base64 using its Binary instance.
1408-- | Do the right thing for rendering a term in an IState
1409prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1410prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1412-- | Pretty-print a high-level Idris term in some bindings context with infix info
1413pprintPTerm :: PPOption -- ^^ pretty printing options
1414 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1415 -> [Name] -- ^^ names to always show in pi, even if not used
1416 -> [FixDecl] -- ^^ Fixity declarations
1417 -> PTerm -- ^^ the term to pretty-print
1418 -> Doc OutputAnnotation
1419pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1420 where
1421 startPrec = 0
1422 funcAppPrec = 10
1424 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1425 prettySe p bnd (PQuote r) =
1426 text "![" <> pretty r <> text "]"
1427 prettySe p bnd (PPatvar fc n) = pretty n
1428 prettySe p bnd e
1429 | Just str <- slist p bnd e = str
1430 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1431 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1432 prettySe p bnd (PLam fc n ty sc) =
1433 bracket p startPrec . group . align . hang 2 $
1434 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1435 prettySe startPrec ((n, False):bnd) sc
1436 prettySe p bnd (PLet fc n ty v sc) =
1437 bracket p startPrec . group . align $
1438 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1439 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1440 prettySe p bnd (PPi (Exp l s _) n ty sc)
1441 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1442 bracket p startPrec . group $
1443 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1444 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1445 | otherwise =
1446 bracket p startPrec . group $
1447 group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1448 where
1449 st =
1450 case s of
1451 Static -> text "[static]" <> space
1452 _ -> empty
1453 prettySe p bnd (PPi (Imp l s _ fa) n ty sc)
1454 | ppopt_impl ppo =
1455 bracket p startPrec $
1456 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1457 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1458 | otherwise = prettySe startPrec ((n, True):bnd) sc
1459 where
1460 st =
1461 case s of
1462 Static -> text "[static]" <> space
1463 _ -> empty
1464 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1465 bracket p startPrec $
1466 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1467 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1468 bracket p startPrec $
1469 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1470 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1471 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1472 | UN nm <- basename f
1473 , not (ppopt_impl ppo) && null (getShowArgs args) =
1474 prettyName True (ppopt_impl ppo) bnd f
1475 prettySe p bnd (PAppBind _ (PRef _ f) [])
1476 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1477 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1478 | UN nm <- basename op
1479 , not (tnull nm) &&
1480 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1481 case getShowArgs args of
1482 [] -> opName True
1483 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1484 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1485 in bracket p precedence $ inFix (getTm l) (getTm r)
1486 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1487 bracket p funcAppPrec $
1488 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1489 align (group (vsep (map (prettyArgS bnd) rest)))
1490 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1491 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1492 f = getFixity (opStr op)
1493 left = case f of
1494 Nothing -> funcAppPrec + 1
1495 Just (Infixl p') -> p'
1496 Just f' -> prec f' + 1
1497 right = case f of
1498 Nothing -> funcAppPrec + 1
1499 Just (Infixr p') -> p'
1500 Just f' -> prec f' + 1
1501 inFix l r = align . group $
1502 (prettySe left bnd l <+> opName False) <$>
1503 group (prettySe right bnd r)
1504 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1505 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1506 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1507 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1508 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1509 let args = getShowArgs as
1510 fp = prettySe (startPrec + 1) bnd f
1511 shownArgs = if ppopt_impl ppo then as else args
1512 in
1513 bracket p funcAppPrec . group $
1514 if null shownArgs
1515 then fp
1516 else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1517 prettySe p bnd (PCase _ scr cases) =
1518 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1519 indent 2 (vsep (map ppcase cases))
1520 where
1521 ppcase (l, r) = let prettyCase = prettySe startPrec
1522 ([(n, False) | n <- vars l] ++ bnd)
1523 in nest nestingSize $
1524 prettyCase l <+> text "=>" <+> prettyCase r
1525 -- Warning: this is a bit of a hack. At this stage, we don't have the
1526 -- global context, so we can't determine which names are constructors,
1527 -- which are types, and which are pattern variables on the LHS of the
1528 -- case pattern. We use the heuristic that names without a namespace
1529 -- are patvars, because right now case blocks in PTerms are always
1530 -- delaborated from TT before being sent to the pretty-printer. If they
1531 -- start getting printed directly, THIS WILL BREAK.
1532 -- Potential solution: add a list of known patvars to the cases in
1533 -- PCase, and have the delaborator fill it out, kind of like the pun
1534 -- disambiguation on PDPair.
1535 vars tm = filter noNS (allNamesIn tm)
1536 noNS (NS _ _) = False
1537 noNS _ = True
1539 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1540 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1541 prettySe p bnd (PResolveTC _) = text "resolvetc"
1542 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1543 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1544 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1545 prettySe p bnd (PEq _ lt rt l r)
1546 | ppopt_impl ppo =
1547 bracket p eqPrec $
1548 enclose lparen rparen eq <+>
1549 align (group (vsep (map (prettyArgS bnd)
1550 [PImp 0 False [] (sUN "A") lt,
1551 PImp 0 False [] (sUN "B") rt,
1552 PExp 0 [] (sUN "x") l,
1553 PExp 0 [] (sUN "y") r])))
1554 | otherwise =
1555 bracket p eqPrec . align . group $
1556 prettyTerm l <+> eq <$> group (prettyTerm r)
1557 where eq = annName eqTy (text "=")
1558 eqPrec = startPrec
1559 prettyTerm = prettySe (eqPrec + 1) bnd
1560 prettySe p bnd (PRewrite _ l r _) =
1561 bracket p startPrec $
1562 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1563 prettySe p bnd (PTyped l r) =
1564 lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1565 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1566 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1567 align . group . vsep . punctuate (ann comma) $
1568 map (prettySe startPrec bnd) elts
1569 where ann = case pun of
1570 TypeOrTerm -> id
1571 IsType -> annName pairTy
1572 IsTerm -> annName pairCon
1573 prettySe p bnd (PDPair _ pun l t r) =
1574 annotated lparen <>
1575 left <+>
1576 annotated (text "**") <+>
1577 prettySe startPrec (addBinding bnd) r <>
1578 annotated rparen
1579 where annotated = case pun of
1580 IsType -> annName sigmaTy
1581 IsTerm -> annName existsCon
1582 TypeOrTerm -> id
1583 (left, addBinding) = case (l, pun) of
1584 (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1585 _ -> (prettySe startPrec bnd l, id )
1586 prettySe p bnd (PAlternative a as) =
1587 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1588 where
1589 prettyAs =
1590 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1591 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1592 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1593 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1594 -- XXX: add pretty for tactics
1595 prettySe p bnd (PProof ts) =
1596 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1597 prettySe p bnd (PTactics ts) =
1598 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1599 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1600 prettySe p bnd (PReturn f) = kwd "return"
1601 prettySe p bnd PImpossible = kwd "impossible"
1602 prettySe p bnd Placeholder = text "_"
1603 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1604 prettySe p bnd (PCoerced t) = prettySe p bnd t
1605 prettySe p bnd (PElabError s) = pretty s
1606 -- Quasiquote pprinting ignores bound vars
1607 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1608 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1609 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1610 prettySe p bnd (PQuoteName n) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1612 prettySe p bnd _ = text "missing pretty-printer for term"
1614 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1615 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1616 where display (UN n) = T.unpack n
1617 display (MN _ n) = T.unpack n
1618 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1619 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1620 display n = show n
1622 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1623 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1624 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1625 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1627 prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1628 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1629 prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1630 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1632 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1633 annName n = annotate (AnnName n Nothing Nothing Nothing)
1635 opStr :: Name -> String
1636 opStr (NS n _) = opStr n
1637 opStr (UN n) = T.unpack n
1639 basename :: Name -> Name
1640 basename (NS n _) = basename n
1641 basename n = n
1643 slist' _ _ e
1644 | containsHole e = Nothing
1645 slist' p bnd (PApp _ (PRef _ nil) _)
1646 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1647 slist' p bnd (PRef _ nil)
1648 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1649 slist' p bnd (PApp _ (PRef _ cons) args)
1650 | nsroot cons == sUN "::",
1651 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1652 all isImp imps,
1653 Just tl' <- slist' p bnd tl
1654 = Just (hd:tl')
1655 where
1656 isImp (PImp {}) = True
1657 isImp _ = False
1658 slist' _ _ tm = Nothing
1660 slist p bnd e | Just es <- slist' p bnd e = Just $
1661 case es of [] -> annotate (AnnData "" "") $ text "[]"
1662 [x] -> enclose left right . group $
1663 prettySe p bnd x
1664 xs -> (enclose left right .
1665 align . group . vsep .
1666 punctuate comma .
1667 map (prettySe p bnd)) xs
1668 where left = (annotate (AnnData "" "") (text "["))
1669 right = (annotate (AnnData "" "") (text "]"))
1670 comma = (annotate (AnnData "" "") (text ","))
1671 slist _ _ _ = Nothing
1673 pairElts :: PTerm -> Maybe [PTerm]
1674 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1675 | otherwise = Just [x, y]
1676 pairElts _ = Nothing
1678 natns = "Prelude.Nat."
1680 snat p (PRef _ z)
1681 | show z == (natns++"Z") || show z == "Z" = Just 0
1682 snat p (PApp _ s [PExp {getTm=n}])
1683 | show s == (natns++"S") || show s == "S",
1684 Just n' <- snat p n
1685 = Just $ 1 + n'
1686 snat _ _ = Nothing
1688 bracket outer inner doc
1689 | outer > inner = lparen <> doc <> rparen
1690 | otherwise = doc
1692 kwd = annotate AnnKeyword . text
1694 fixities :: M.Map String Fixity
1695 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1697 getFixity :: String -> Maybe Fixity
1698 getFixity = flip M.lookup fixities
1700-- | Determine whether a name was the one inserted for a hole or
1701-- guess by the delaborator
1702isHoleName :: Name -> Bool
1703isHoleName (UN n) = n == T.pack "[__]"
1704isHoleName _ = False
1706-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1707containsHole :: PTerm -> Bool
1708containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]
1710-- | Pretty-printer helper for names that attaches the correct annotations
1711prettyName
1712 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1713 -> Bool -- ^^ whether to show namespaces
1714 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1715 -> Name -- ^^ the name to pprint
1716 -> Doc OutputAnnotation
1717prettyName infixParen showNS bnd n
1718 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1719 | (UN n') <- n, T.unpack n' == "_" = text "_"
1720 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1721 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1722 where fullName = text nameSpace <> parenthesise (text (baseName n))
1723 baseName (UN n) = T.unpack n
1724 baseName (NS n ns) = baseName n
1725 baseName (MN i s) = T.unpack s
1726 baseName other = show other
1727 nameSpace = case n of
1728 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1729 _ -> ""
1730 isInfix = case baseName n of
1731 "" -> False
1732 (c : _) -> not (isAlpha c)
1733 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1736showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1737showCImp ppo (PClause _ n l ws r w)
1738 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1739 <+> text "where" <+> text (show w)
1740 where
1741 showWs [] = empty
1742 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1743showCImp ppo (PWith _ n l ws r pn w)
1744 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1745 <+> braces (text (show w))
1746 where
1747 showWs [] = empty
1748 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1751showDImp :: PPOption -> PData -> Doc OutputAnnotation
1752showDImp ppo (PDatadecl n ty cons)
1753 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1754 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1756showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1757showDecls o ds = vsep (map (showDeclImp o) ds)
1759showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1760showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1761showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1762 indent 2 (vsep (map (showCImp o) cs))
1763showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1764showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1765showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1766showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1767showDeclImp o (PClass _ _ _ cs n ps _ _ ds)
1768 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1769showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)
1770 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1771showDeclImp _ _ = text "..."
1772-- showDeclImp (PImport o) = "import " ++ o
1774getImps :: [PArg] -> [(Name, PTerm)]
1775getImps [] = []
1776getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1777getImps (_ : xs) = getImps xs
1779getExps :: [PArg] -> [PTerm]
1780getExps [] = []
1781getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1782getExps (_ : xs) = getExps xs
1784getShowArgs :: [PArg] -> [PArg]
1785getShowArgs [] = []
1786getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1787getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1788 | PImp _ _ _ _ tm <- e
1789 , containsHole tm = e : getShowArgs xs
1790getShowArgs (_ : xs) = getShowArgs xs
1792getConsts :: [PArg] -> [PTerm]
1793getConsts [] = []
1794getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1795getConsts (_ : xs) = getConsts xs
1797getAll :: [PArg] -> [PTerm]
1798getAll = map getTm
1801-- | Show Idris name
1802showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1803 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1804 -> PPOption -- ^^ pretty printing options
1805 -> Bool -- ^^ whether to colourise
1806 -> Name -- ^^ the term to show
1807 -> String
1808showName ist bnd ppo colour n = case ist of
1809 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1810 Nothing -> showbasic n
1811 where name = if ppopt_impl ppo then show n else showbasic n
1812 showbasic n@(UN _) = showCG n
1813 showbasic (MN i s) = str s
1814 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1815 showbasic (SN s) = show s
1816 fst3 (x, _, _) = x
1817 colourise n t = let ctxt' = fmap tt_ctxt ist in
1818 case ctxt' of
1819 Nothing -> name
1820 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1821 else colouriseBound t name
1822 | isDConName n ctxt -> colouriseData t name
1823 | isFnName n ctxt -> colouriseFun t name
1824 | isTConName n ctxt -> colouriseType t name
1825 -- The assumption is that if a name is not bound and does not exist in the
1826 -- global context, then we're somewhere in which implicit info has been lost
1827 -- (like error messages). Thus, unknown vars are colourised as implicits.
1828 | otherwise -> colouriseImplicit t name
1830showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1831 -> PTerm -- ^^ the term to show
1832 -> String
1833showTm ist = displayDecorated (consoleDecorate ist) .
1834 renderPretty 0.8 100000 .
1835 prettyImp (ppOptionIst ist)
1837-- | Show a term with implicits, no colours
1838showTmImpls :: PTerm -> String
1839showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1843instance Sized PTerm where
1844 size (PQuote rawTerm) = size rawTerm
1845 size (PRef fc name) = size name
1846 size (PLam fc name ty bdy) = 1 + size ty + size bdy
1847 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1848 size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1849 size (PTyped trm ty) = 1 + size trm + size ty
1850 size (PApp fc name args) = 1 + size args
1851 size (PAppBind fc name args) = 1 + size args
1852 size (PCase fc trm bdy) = 1 + size trm + size bdy
1853 size (PTrue fc _) = 1
1854 size (PRefl fc _) = 1
1855 size (PResolveTC fc) = 1
1856 size (PEq fc _ _ left right) = 1 + size left + size right
1857 size (PRewrite fc left right _) = 1 + size left + size right
1858 size (PPair fc _ left right) = 1 + size left + size right
1859 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1860 size (PAlternative a alts) = 1 + size alts
1861 size (PHidden hidden) = size hidden
1862 size (PUnifyLog tm) = size tm
1863 size (PDisamb _ tm) = size tm
1864 size (PNoImplicits tm) = size tm
1865 size PType = 1
1866 size (PUniverse _) = 1
1867 size (PConstant const) = 1 + size const
1868 size Placeholder = 1
1869 size (PDoBlock dos) = 1 + size dos
1870 size (PIdiom fc term) = 1 + size term
1871 size (PReturn fc) = 1
1872 size (PMetavar name) = 1
1873 size (PProof tactics) = size tactics
1874 size (PElabError err) = size err
1875 size PImpossible = 1
1876 size _ = 0
1878getPArity :: PTerm -> Int
1879getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1880getPArity _ = 0
1882-- Return all names, free or globally bound, in the given term.
1884allNamesIn :: PTerm -> [Name]
1885allNamesIn tm = nub $ ni [] tm
1886 where -- TODO THINK added niTacImp, but is it right?
1887 ni env (PRef _ n)
1888 | not (n `elem` env) = [n]
1889 ni env (PPatvar _ n) = [n]
1890 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1891 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1892 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1893 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1894 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1895 ni env (PHidden tm) = ni env tm
1896 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1897 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1898 ni env (PTyped l r) = ni env l ++ ni env r
1899 ni env (PPair _ _ l r) = ni env l ++ ni env r
1900 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1901 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1902 ni env (PAlternative a ls) = concatMap (ni env) ls
1903 ni env (PUnifyLog tm) = ni env tm
1904 ni env (PDisamb _ tm) = ni env tm
1905 ni env (PNoImplicits tm) = ni env tm
1906 ni env _ = []
1908 niTacImp env (TacImp _ _ scr) = ni env scr
1909 niTacImp _ _ = []
1912-- Return all names defined in binders in the given term
1913boundNamesIn :: PTerm -> [Name]
1914boundNamesIn tm = S.toList (ni S.empty tm)
1915 where -- TODO THINK Added niTacImp, but is it right?
1916 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
1917 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
1918 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
1919 ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc
1920 ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
1921 ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
1922 ni set (PEq _ _ _ l r) = ni (ni set l) r
1923 ni set (PRewrite _ l r _) = ni (ni set l) r
1924 ni set (PTyped l r) = ni (ni set l) r
1925 ni set (PPair _ _ l r) = ni (ni set l) r
1926 ni set (PDPair _ _ (PRef _ n) t r) = ni (ni set t) r
1927 ni set (PDPair _ _ l t r) = ni (ni (ni set l) t) r
1928 ni set (PAlternative a as) = niTms set as
1929 ni set (PHidden tm) = ni set tm
1930 ni set (PUnifyLog tm) = ni set tm
1931 ni set (PDisamb _ tm) = ni set tm
1932 ni set (PNoImplicits tm) = ni set tm
1933 ni set _ = set
1935 niTms set [] = set
1936 niTms set (x : xs) = niTms (ni set x) xs
1938 niTacImp set (TacImp _ _ scr) = ni set scr
1939 niTacImp set _ = set
1941-- Return names which are valid implicits in the given term (type).
1942implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1943implicitNamesIn uvars ist tm = nub $ ni [] tm
1944 where
1945 ni env (PRef _ n)
1946 | not (n `elem` env)
1947 = case lookupTy n (tt_ctxt ist) of
1948 [] -> [n]
1949 _ -> if n `elem` uvars then [n] else []
1950 ni env (PApp _ f@(PRef _ n) as)
1951 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1952 | otherwise = concatMap (ni env) (map getTm as)
1953 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1954 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1955 ni env (PCase _ c os) = ni env c ++
1956 -- names in 'os', not counting the names bound in the cases
1957 (nub (concatMap (ni env) (map snd os))
1958 \\ nub (concatMap (ni env) (map fst os)))
1959 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1960 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1961 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1962 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1963 ni env (PTyped l r) = ni env l ++ ni env r
1964 ni env (PPair _ _ l r) = ni env l ++ ni env r
1965 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1966 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1967 ni env (PAlternative a as) = concatMap (ni env) as
1968 ni env (PHidden tm) = ni env tm
1969 ni env (PUnifyLog tm) = ni env tm
1970 ni env (PDisamb _ tm) = ni env tm
1971 ni env (PNoImplicits tm) = ni env tm
1972 ni env _ = []
1974-- Return names which are free in the given term.
1975namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1976namesIn 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` (map fst uvars) then [n] else []
1983 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1984 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1985 ni env (PCase _ c os) = ni env c ++
1986 -- names in 'os', not counting the names bound in the cases
1987 (nub (concatMap (ni env) (map snd os))
1988 \\ nub (concatMap (ni env) (map fst os)))
1989 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1990 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1991 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1992 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1993 ni env (PTyped l r) = ni env l ++ ni env r
1994 ni env (PPair _ _ l r) = ni env l ++ ni env r
1995 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1996 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1997 ni env (PAlternative a as) = concatMap (ni env) as
1998 ni env (PHidden tm) = ni env tm
1999 ni env (PUnifyLog tm) = ni env tm
2000 ni env (PDisamb _ tm) = ni env tm
2001 ni env (PNoImplicits tm) = ni env tm
2002 ni env _ = []
2004 niTacImp env (TacImp _ _ scr) = ni env scr
2005 niTacImp _ _ = []
2007-- Return which of the given names are used in the given term.
2009usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2010usedNamesIn vars ist tm = nub $ ni [] tm
2011 where -- TODO THINK added niTacImp, but is it right?
2012 ni env (PRef _ n)
2013 | n `elem` vars && not (n `elem` env)
2014 = case lookupDefExact n (tt_ctxt ist) of
2015 Nothing -> [n]
2016 _ -> []
2017 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2018 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2019 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2020 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
2021 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2022 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
2023 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2024 ni env (PTyped l r) = ni env l ++ ni env r
2025 ni env (PPair _ _ l r) = ni env l ++ ni env r
2026 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
2027 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
2028 ni env (PAlternative a as) = concatMap (ni env) as
2029 ni env (PHidden tm) = ni env tm
2030 ni env (PUnifyLog tm) = ni env tm
2031 ni env (PDisamb _ tm) = ni env tm
2032 ni env (PNoImplicits tm) = ni env tm
2033 ni env _ = []
2035 niTacImp env (TacImp _ _ scr) = ni env scr
2036 niTacImp _ _ = []
2038-- Return the list of inaccessible (= dotted) positions for a name.
2039getErasureInfo :: IState -> Name -> [Int]
2040getErasureInfo ist n =
2041 case lookupCtxtExact n (idris_optimisation ist) of
2042 Just (Optimise inacc detagg) -> map fst inacc
2043 Nothing -> []