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