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