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