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