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