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