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