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