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