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