git.iko.soy/Idris-dev
on 419b35c help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1571 lines 61 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 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 IRTS.Lang
11import IRTS.CodegenCommon
12import Util.Pretty
13import Util.DynamicLinker
15import Idris.Colours
17import Paths_idris
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.Trans.State.Strict
23import Control.Monad.Trans.Error
25import Data.List hiding (group)
26import Data.Char
27import qualified Data.Map as M
28import qualified Data.Text as T
29import qualified Data.Map as M
30import Data.Either
31import qualified Data.Set as S
32import Data.Word (Word)
34import Debug.Trace
36import Text.PrettyPrint.Annotated.Leijen
38data IOption = IOption { opt_logLevel :: Int,
39 opt_typecase :: Bool,
40 opt_typeintype :: Bool,
41 opt_coverage :: Bool,
42 opt_showimp :: Bool, -- ^^ show implicits
43 opt_errContext :: Bool,
44 opt_repl :: Bool,
45 opt_verbose :: Bool,
46 opt_nobanner :: Bool,
47 opt_quiet :: Bool,
48 opt_codegen :: Codegen,
49 opt_outputTy :: OutputType,
50 opt_ibcsubdir :: FilePath,
51 opt_importdirs :: [FilePath],
52 opt_triple :: String,
53 opt_cpu :: String,
54 opt_optLevel :: Word,
55 opt_cmdline :: [Opt], -- remember whole command line
56 opt_origerr :: Bool
57 }
58 deriving (Show, Eq)
60defaultOpts = IOption { opt_logLevel = 0
61 , opt_typecase = False
62 , opt_typeintype = False
63 , opt_coverage = True
64 , opt_showimp = False
65 , opt_errContext = False
66 , opt_repl = True
67 , opt_verbose = True
68 , opt_nobanner = False
69 , opt_quiet = False
70 , opt_codegen = ViaC
71 , opt_outputTy = Executable
72 , opt_ibcsubdir = ""
73 , opt_importdirs = []
74 , opt_triple = ""
75 , opt_cpu = ""
76 , opt_optLevel = 2
77 , opt_cmdline = []
78 , opt_origerr = False
79 }
81data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
83-- | The output mode in use
84data OutputMode = RawOutput | IdeSlave Integer deriving Show
86-- | How wide is the console?
87data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
88 | ColsWide Int -- ^ Manually specified - must be positive
89 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
91-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
92-- without typechecking).
93-- This will include all the functions and data declarations, plus fixity declarations
94-- and syntax macros.
96-- | The global state used in the Idris monad
97data IState = IState {
98 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
99 idris_constraints :: [(UConstraint, FC)],
100 -- ^ A list of universe constraints and their corresponding source locations
101 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
102 idris_implicits :: Ctxt [PArg],
103 idris_statics :: Ctxt [Bool],
104 idris_classes :: Ctxt ClassInfo,
105 idris_dsls :: Ctxt DSL,
106 idris_optimisation :: Ctxt OptInfo,
107 idris_datatypes :: Ctxt TypeInfo,
108 idris_namehints :: Ctxt [Name],
109 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
110 -- ^ list of lhs/rhs, and a list of missing clauses
111 idris_flags :: Ctxt [FnOpt],
112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
113 idris_calledgraph :: Ctxt [Name],
114 idris_docstrings :: Ctxt (String, [(Name, String)]),
115 idris_tyinfodata :: Ctxt TIData,
116 idris_totcheck :: [(FC, Name)], -- names to check totality on
117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
118 idris_options :: IOption,
119 idris_name :: Int,
120 idris_lineapps :: [((FilePath, Int), PTerm)],
121 -- ^ Full application LHS on source line
122 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
123 idris_coercions :: [Name],
124 idris_transforms :: [(Term, Term)],
125 idris_errRev :: [(Term, Term)],
126 syntax_rules :: [Syntax],
127 syntax_keywords :: [String],
128 imported :: [FilePath], -- ^ The imported modules
129 idris_scprims :: [(Name, (Int, PrimFn))],
130 idris_objs :: [(Codegen, FilePath)],
131 idris_libs :: [(Codegen, String)],
132 idris_cgflags :: [(Codegen, String)],
133 idris_hdrs :: [(Codegen, String)],
134 proof_list :: [(Name, [String])],
135 errLine :: Maybe Int,
136 parserWarnings :: [(FC, Err)],
137 lastParse :: Maybe Name,
138 indent_stack :: [Int],
139 brace_stack :: [Maybe Int],
140 lastTokenSpan :: Maybe (FC, FC), -- ^ What was the span of the latest token parsed?
141 hide_list :: [(Name, Maybe Accessibility)],
142 default_access :: Accessibility,
143 default_total :: Bool,
144 ibc_write :: [IBCWrite],
145 compiled_so :: Maybe String,
146 idris_dynamic_libs :: [DynamicLib],
147 idris_language_extensions :: [LanguageExt],
148 idris_outputmode :: OutputMode,
149 idris_colourRepl :: Bool,
150 idris_colourTheme :: ColourTheme,
151 idris_outh :: Handle,
152 idris_errorhandlers :: [Name], -- ^ Global error handlers
153 idris_nameIdx :: (Int, Ctxt (Int, Name)),
154 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
155 module_aliases :: M.Map [T.Text] [T.Text],
156 idris_consolewidth :: ConsoleWidth -- ^ How many chars wide is the console?
157 }
159data SizeChange = Smaller | Same | Bigger | Unknown
160 deriving (Show, Eq)
161{-!
162deriving instance Binary SizeChange
163deriving instance NFData SizeChange
164!-}
166type SCGEntry = (Name, [Maybe (Int, SizeChange)])
168data CGInfo = CGInfo { argsdef :: [Name],
169 calls :: [(Name, [[Name]])],
170 scg :: [SCGEntry],
171 argsused :: [Name],
172 unusedpos :: [Int] }
173 deriving Show
174{-!
175deriving instance Binary CGInfo
176deriving instance NFData CGInfo
177!-}
179primDefs = [sUN "unsafePerformPrimIO",
180 sUN "mkLazyForeignPrim",
181 sUN "mkForeignPrim",
182 sUN "FalseElim"]
184-- information that needs writing for the current module's .ibc file
185data IBCWrite = IBCFix FixDecl
186 | IBCImp Name
187 | IBCStatic Name
188 | IBCClass Name
189 | IBCInstance Bool Name Name
190 | IBCDSL Name
191 | IBCData Name
192 | IBCOpt Name
193 | IBCMetavar Name
194 | IBCSyntax Syntax
195 | IBCKeyword String
196 | IBCImport FilePath
197 | IBCObj Codegen FilePath
198 | IBCLib Codegen String
199 | IBCCGFlag Codegen String
200 | IBCDyLib String
201 | IBCHeader Codegen String
202 | IBCAccess Name Accessibility
203 | IBCMetaInformation Name MetaInformation
204 | IBCTotal Name Totality
205 | IBCFlags Name [FnOpt]
206 | IBCTrans (Term, Term)
207 | IBCErrRev (Term, Term)
208 | IBCCG Name
209 | IBCDoc Name
210 | IBCCoercion Name
211 | IBCDef Name -- i.e. main context
212 | IBCNameHint (Name, Name)
213 | IBCLineApp FilePath Int PTerm
214 | IBCErrorHandler Name
215 | IBCFunctionErrorHandler Name Name Name
216 deriving Show
218-- | The initial state for the compiler
219idrisInit :: IState
220idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
221 emptyContext emptyContext emptyContext emptyContext
222 emptyContext emptyContext emptyContext emptyContext
223 emptyContext emptyContext
224 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
225 [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput
226 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
227 AutomaticWidth
229-- | The monad for the main REPL - reading and processing files and updating
230-- global state (hence the IO inner monad).
231--type Idris = WriterT [Either String (IO ())] (State IState a))
232type Idris = StateT IState (ErrorT Err IO)
234-- Commands in the REPL
236data Codegen = ViaC
237 | ViaJava
238 | ViaNode
239 | ViaJavaScript
240 | ViaLLVM
241 | Bytecode
242 deriving (Show, Eq)
244-- | REPL commands
245data Command = Quit
246 | Help
247 | Eval PTerm
248 | Check PTerm
249 | DocStr Name
250 | TotCheck Name
251 | Reload
252 | Load FilePath
253 | ChangeDirectory FilePath
254 | ModImport String
255 | Edit
256 | Compile Codegen String
257 | Execute
258 | ExecVal PTerm
259 | Metavars
260 | Prove Name
261 | AddProof (Maybe Name)
262 | RmProof Name
263 | ShowProof Name
264 | Proofs
265 | Universes
266 | LogLvl Int
267 | Spec PTerm
268 | HNF PTerm
269 | TestInline PTerm
270 | Defn Name
271 | Info Name
272 | Missing Name
273 | DynamicLink FilePath
274 | ListDynamic
275 | Pattelab PTerm
276 | DebugInfo Name
277 | Search PTerm
278 | CaseSplitAt Bool Int Name
279 | AddClauseFrom Bool Int Name
280 | AddProofClauseFrom Bool Int Name
281 | AddMissing Bool Int Name
282 | MakeWith Bool Int Name
283 | DoProofSearch Bool Int Name [Name]
284 | SetOpt Opt
285 | UnsetOpt Opt
286 | NOP
287 | SetColour ColourType IdrisColour
288 | ColourOn
289 | ColourOff
290 | ListErrorHandlers
291 | SetConsoleWidth ConsoleWidth
293data Opt = Filename String
294 | Ver
295 | Usage
296 | Quiet
297 | NoBanner
298 | ColourREPL Bool
299 | Ideslave
300 | ShowLibs
301 | ShowLibdir
302 | ShowIncs
303 | NoBasePkgs
304 | NoPrelude
305 | NoBuiltins -- only for the really primitive stuff!
306 | NoREPL
307 | OLogging Int
308 | Output String
309 | TypeCase
310 | TypeInType
311 | DefaultTotal
312 | DefaultPartial
313 | WarnPartial
314 | NoCoverage
315 | ErrContext
316 | ShowImpl
317 | Verbose
318 | IBCSubDir String
319 | ImportDir String
320 | PkgBuild String
321 | PkgInstall String
322 | PkgClean String
323 | PkgCheck String
324 | PkgREPL String
325 | WarnOnly
326 | Pkg String
327 | BCAsm String
328 | DumpDefun String
329 | DumpCases String
330 | UseCodegen Codegen
331 | OutputTy OutputType
332 | Extension LanguageExt
333 | InterpretScript String
334 | TargetTriple String
335 | TargetCPU String
336 | OptLevel Word
337 | Client String
338 | ShowOrigErr
339 | AutoWidth -- ^ Automatically adjust terminal width
340 deriving (Show, Eq)
342-- Parsed declarations
344data Fixity = Infixl { prec :: Int }
345 | Infixr { prec :: Int }
346 | InfixN { prec :: Int }
347 | PrefixN { prec :: Int }
348 deriving Eq
349{-!
350deriving instance Binary Fixity
351deriving instance NFData Fixity
352!-}
354instance Show Fixity where
355 show (Infixl i) = "infixl " ++ show i
356 show (Infixr i) = "infixr " ++ show i
357 show (InfixN i) = "infix " ++ show i
358 show (PrefixN i) = "prefix " ++ show i
360data FixDecl = Fix Fixity String
361 deriving Eq
363instance Show FixDecl where
364 show (Fix f s) = show f ++ " " ++ s
366{-!
367deriving instance Binary FixDecl
368deriving instance NFData FixDecl
369!-}
371instance Ord FixDecl where
372 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
375data Static = Static | Dynamic
376 deriving (Show, Eq)
377{-!
378deriving instance Binary Static
379deriving instance NFData Static
380!-}
382-- Mark bindings with their explicitness, and laziness
383data Plicity = Imp { pargopts :: [ArgOpt],
384 pstatic :: Static,
385 pparam :: Bool }
386 | Exp { pargopts :: [ArgOpt],
387 pstatic :: Static,
388 pparam :: Bool }
389 | Constraint { pargopts :: [ArgOpt],
390 pstatic :: Static }
391 | TacImp { pargopts :: [ArgOpt],
392 pstatic :: Static,
393 pscript :: PTerm }
394 deriving (Show, Eq)
396plazy :: Plicity -> Bool
397plazy tm = Lazy `elem` pargopts tm
399{-!
400deriving instance Binary Plicity
401deriving instance NFData Plicity
402!-}
404impl = Imp [Lazy] Dynamic False
405expl = Exp [] Dynamic False
406expl_param = Exp [] Dynamic True
407constraint = Constraint [] Dynamic
408tacimpl t = TacImp [] Dynamic t
410data FnOpt = Inlinable -- always evaluate when simplifying
411 | TotalFn | PartialFn
412 | Coinductive | AssertTotal
413 | Dictionary -- type class dictionary, eval only when
414 -- a function argument, and further evaluation resutls
415 | Implicit -- implicit coercion
416 | CExport String -- export, with a C name
417 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
418 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
419 | Reflection -- a reflecting function, compile-time only
420 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
421 deriving (Show, Eq)
422{-!
423deriving instance Binary FnOpt
424deriving instance NFData FnOpt
425!-}
427type FnOpts = [FnOpt]
429inlinable :: FnOpts -> Bool
430inlinable = elem Inlinable
432dictionary :: FnOpts -> Bool
433dictionary = elem Dictionary
436-- | Data declaration options
437data DataOpt = Codata -- Set if the the data-type is coinductive
438 | DefaultEliminator -- Set if an eliminator should be generated for data type
439 | DataErrRev
440 deriving (Show, Eq)
442type DataOpts = [DataOpt]
444-- | Type provider - what to provide
445data ProvideWhat = ProvTerm -- ^ only allow providing terms
446 | ProvPostulate -- ^ only allow postulates
447 | ProvAny -- ^ either is ok
448 deriving (Show, Eq)
450-- | Top-level declarations such as compiler directives, definitions,
451-- datatypes and typeclasses.
452data PDecl' t
453 = PFix FC Fixity [String] -- ^ Fixity declaration
454 | PTy String [(Name, String)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
455 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate
456 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
457 | PCAF FC Name t -- ^ Top level constant
458 | PData String [(Name, String)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
459 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
460 | PNamespace String [PDecl' t] -- ^ New namespace
461 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration
462 | PClass String SyntaxInfo FC
463 [t] -- constraints
464 Name
465 [(Name, t)] -- parameters
466 [PDecl' t] -- declarations
467 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
468 -- class name, parameters, method declarations
469 | PInstance SyntaxInfo FC [t] -- constraints
470 Name -- class
471 [t] -- parameters
472 t -- full instance type
473 (Maybe Name) -- explicit name
474 [PDecl' t]
475 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
476 -- class name, parameters, full instance type, optional explicit name, and definitions
477 | PDSL Name (DSL' t) -- ^ DSL declaration
478 | PSyntax FC Syntax -- ^ Syntax definition
479 | PMutual FC [PDecl' t] -- ^ Mutual block
480 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
481 | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term
482 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
483 -- bool is True, lhs and rhs must be convertible
484 deriving Functor
485{-!
486deriving instance Binary PDecl'
487deriving instance NFData PDecl'
488!-}
490-- For elaborator state
491type ElabD a = Elab' [PDecl] a
493-- | One clause of a top-level definition. Term arguments to constructors are:
494--
495-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
496--
497-- 2. The list of extra 'with' patterns
498--
499-- 3. The right-hand side
500--
501-- 4. The where block (PDecl' t)
503data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
504 | PWith FC Name t [t] t [PDecl' t]
505 | PClauseR FC [t] t [PDecl' t]
506 | PWithR FC [t] t [PDecl' t]
507 deriving Functor
508{-!
509deriving instance Binary PClause'
510deriving instance NFData PClause'
511!-}
513-- | Data declaration
514data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
515 d_tcon :: t, -- ^ Type constructor
516 d_cons :: [(String, [(Name, String)], Name, t, FC, [Name])] -- ^ Constructors
517 }
518 -- ^ Data declaration
519 | PLaterdecl { d_name :: Name, d_tcon :: t }
520 -- ^ "Placeholder" for data whose constructors are defined later
521 deriving Functor
522{-!
523deriving instance Binary PData'
524deriving instance NFData PData'
525!-}
527-- Handy to get a free function for applying PTerm -> PTerm functions
528-- across a program, by deriving Functor
530type PDecl = PDecl' PTerm
531type PData = PData' PTerm
532type PClause = PClause' PTerm
534-- get all the names declared in a decl
536declared :: PDecl -> [Name]
537declared (PFix _ _ _) = []
538declared (PTy _ _ _ _ _ n t) = [n]
539declared (PPostulate _ _ _ _ n t) = [n]
540declared (PClauses _ _ n _) = [] -- not a declaration
541declared (PCAF _ n _) = [n]
542declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
543 where fstt (_, _, a, _, _, _) = a
544declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
545declared (PParams _ _ ds) = concatMap declared ds
546declared (PNamespace _ ds) = concatMap declared ds
547declared (PRecord _ _ _ n _ _ c _) = [n, c]
548declared (PClass _ _ _ _ n _ ms) = n : concatMap declared ms
549declared (PInstance _ _ _ _ _ _ _ _) = []
550declared (PDSL n _) = [n]
551declared (PSyntax _ _) = []
552declared (PMutual _ ds) = concatMap declared ds
553declared (PDirective _) = []
555-- get the names declared, not counting nested parameter blocks
556tldeclared :: PDecl -> [Name]
557tldeclared (PFix _ _ _) = []
558tldeclared (PTy _ _ _ _ _ n t) = [n]
559tldeclared (PPostulate _ _ _ _ n t) = [n]
560tldeclared (PClauses _ _ n _) = [] -- not a declaration
561tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]
562tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
563 where fstt (_, _, a, _, _, _) = a
564tldeclared (PParams _ _ ds) = []
565tldeclared (PMutual _ ds) = concatMap tldeclared ds
566tldeclared (PNamespace _ ds) = concatMap tldeclared ds
567tldeclared (PClass _ _ _ _ n _ ms) = concatMap tldeclared ms
568tldeclared (PInstance _ _ _ _ _ _ _ _) = []
569tldeclared _ = []
571defined :: PDecl -> [Name]
572defined (PFix _ _ _) = []
573defined (PTy _ _ _ _ _ n t) = []
574defined (PPostulate _ _ _ _ n t) = []
575defined (PClauses _ _ n _) = [n] -- not a declaration
576defined (PCAF _ n _) = [n]
577defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
578 where fstt (_, _, a, _, _, _) = a
579defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
580defined (PParams _ _ ds) = concatMap defined ds
581defined (PNamespace _ ds) = concatMap defined ds
582defined (PRecord _ _ _ n _ _ c _) = [n, c]
583defined (PClass _ _ _ _ n _ ms) = n : concatMap defined ms
584defined (PInstance _ _ _ _ _ _ _ _) = []
585defined (PDSL n _) = [n]
586defined (PSyntax _ _) = []
587defined (PMutual _ ds) = concatMap defined ds
588defined (PDirective _) = []
589--defined _ = []
591updateN :: [(Name, Name)] -> Name -> Name
592updateN ns n | Just n' <- lookup n ns = n'
593updateN _ n = n
595updateNs :: [(Name, Name)] -> PTerm -> PTerm
596updateNs [] t = t
597updateNs ns t = mapPT updateRef t
598 where updateRef (PRef fc f) = PRef fc (updateN ns f)
599 updateRef t = t
601-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
602-- updateDNs [] t = t
603-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
604-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
605-- where updateCNs ns (PClause n l ts r ds)
606-- = PClause (updateN ns n) (fmap (updateNs ns) l)
607-- (map (fmap (updateNs ns)) ts)
608-- (fmap (updateNs ns) r)
609-- (map (updateDNs ns) ds)
610-- updateDNs ns c = c
612data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
614-- | High level language terms
615data PTerm = PQuote Raw
616 | PRef FC Name
617 | PInferRef FC Name -- ^ A name to be defined later
618 | PPatvar FC Name
619 | PLam Name PTerm PTerm
620 | PPi Plicity Name PTerm PTerm
621 | PLet Name PTerm PTerm PTerm
622 | PTyped PTerm PTerm -- ^ Term with explicit type
623 | PApp FC PTerm [PArg]
624 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
625 | PMatchApp FC Name -- ^ Make an application by type matching
626 | PCase FC PTerm [(PTerm, PTerm)]
627 | PTrue FC PunInfo
628 | PFalse FC
629 | PRefl FC PTerm
630 | PResolveTC FC
631 | PEq FC PTerm PTerm
632 | PRewrite FC PTerm PTerm (Maybe PTerm)
633 | PPair FC PunInfo PTerm PTerm
634 | PDPair FC PunInfo PTerm PTerm PTerm
635 | PAlternative Bool [PTerm] -- True if only one may work
636 | PHidden PTerm -- ^ Irrelevant or hidden pattern
637 | PType
638 | PGoal FC PTerm Name PTerm
639 | PConstant Const
640 | Placeholder
641 | PDoBlock [PDo]
642 | PIdiom FC PTerm
643 | PReturn FC
644 | PMetavar Name
645 | PProof [PTactic] -- ^ Proof script
646 | PTactics [PTactic] -- ^ As PProof, but no auto solving
647 | PElabError Err -- ^ Error to report on elaboration
648 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
649 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
650 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
651 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
652 | PNoImplicits PTerm -- ^ never run implicit converions on the term
653 deriving Eq
656{-!
657deriving instance Binary PTerm
658deriving instance NFData PTerm
659!-}
661mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
662mapPT f t = f (mpt t) where
663 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
664 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
665 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
666 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
667 (fmap (mapPT f) g)
668 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
669 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
670 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
671 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
672 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
673 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
674 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
675 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
676 mpt (PHidden t) = PHidden (mapPT f t)
677 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
678 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
679 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
680 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
681 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
682 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
683 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
684 mpt x = x
687data PTactic' t = Intro [Name] | Intros | Focus Name
688 | Refine Name [Bool] | Rewrite t
689 | Induction Name
690 | Equiv t
691 | MatchRefine Name
692 | LetTac Name t | LetTacTy Name t t
693 | Exact t | Compute | Trivial | TCInstance
694 | ProofSearch (Maybe Name) [Name]
695 | Solve
696 | Attack
697 | ProofState | ProofTerm | Undo
698 | Try (PTactic' t) (PTactic' t)
699 | TSeq (PTactic' t) (PTactic' t)
700 | ApplyTactic t -- see Language.Reflection module
701 | ByReflection t
702 | Reflect t
703 | Fill t
704 | GoalType String (PTactic' t)
705 | TCheck t
706 | TEval t
707 | Qed | Abandon
708 deriving (Show, Eq, Functor)
709{-!
710deriving instance Binary PTactic'
711deriving instance NFData PTactic'
712!-}
713instance Sized a => Sized (PTactic' a) where
714 size (Intro nms) = 1 + size nms
715 size Intros = 1
716 size (Focus nm) = 1 + size nm
717 size (Refine nm bs) = 1 + size nm + length bs
718 size (Rewrite t) = 1 + size t
719 size (Induction t) = 1 + size t
720 size (LetTac nm t) = 1 + size nm + size t
721 size (Exact t) = 1 + size t
722 size Compute = 1
723 size Trivial = 1
724 size Solve = 1
725 size Attack = 1
726 size ProofState = 1
727 size ProofTerm = 1
728 size Undo = 1
729 size (Try l r) = 1 + size l + size r
730 size (TSeq l r) = 1 + size l + size r
731 size (ApplyTactic t) = 1 + size t
732 size (Reflect t) = 1 + size t
733 size (Fill t) = 1 + size t
734 size Qed = 1
735 size Abandon = 1
737type PTactic = PTactic' PTerm
739data PDo' t = DoExp FC t
740 | DoBind FC Name t
741 | DoBindP FC t t
742 | DoLet FC Name t t
743 | DoLetP FC t t
744 deriving (Eq, Functor)
745{-!
746deriving instance Binary PDo'
747deriving instance NFData PDo'
748!-}
750instance Sized a => Sized (PDo' a) where
751 size (DoExp fc t) = 1 + size fc + size t
752 size (DoBind fc nm t) = 1 + size fc + size nm + size t
753 size (DoBindP fc l r) = 1 + size fc + size l + size r
754 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
755 size (DoLetP fc l r) = 1 + size fc + size l + size r
757type PDo = PDo' PTerm
759-- The priority gives a hint as to elaboration order. Best to elaborate
760-- things early which will help give a more concrete type to other
761-- variables, e.g. a before (interpTy a).
763data PArg' t = PImp { priority :: Int,
764 machine_inf :: Bool, -- true if the machine inferred it
765 argopts :: [ArgOpt],
766 pname :: Name, getTm :: t }
767 | PExp { priority :: Int,
768 argopts :: [ArgOpt],
769 getTm :: t }
770 | PConstraint { priority :: Int,
771 argopts :: [ArgOpt],
772 getTm :: t }
773 | PTacImplicit { priority :: Int,
774 argopts :: [ArgOpt],
775 pname :: Name,
776 getScript :: t,
777 getTm :: t }
778 deriving (Show, Eq, Functor)
780data ArgOpt = Lazy | HideDisplay
781 deriving (Show, Eq)
783lazyarg :: PArg' t -> Bool
784lazyarg tm = Lazy `elem` argopts tm
786instance Sized a => Sized (PArg' a) where
787 size (PImp p _ l nm trm) = 1 + size nm + size trm
788 size (PExp p l trm) = 1 + size trm
789 size (PConstraint p l trm) = 1 + size trm
790 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
792{-!
793deriving instance Binary PArg'
794deriving instance NFData PArg'
795!-}
797pimp n t mach = PImp 1 mach [Lazy] n t
798pexp t = PExp 1 [] t
799pconst t = PConstraint 1 [] t
800ptacimp n s t = PTacImplicit 2 [Lazy] n s t
802type PArg = PArg' PTerm
804-- Type class data
806data ClassInfo = CI { instanceName :: Name,
807 class_methods :: [(Name, (FnOpts, PTerm))],
808 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
809 class_default_superclasses :: [PDecl],
810 class_params :: [Name],
811 class_instances :: [Name] }
812 deriving Show
813{-!
814deriving instance Binary ClassInfo
815deriving instance NFData ClassInfo
816!-}
818-- Type inference data
820data TIData = TIPartial -- ^ a function with a partially defined type
821 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
822 deriving Show
824-- An argument is conditionally forceable iff its forceability
825-- depends on the collapsibility of the whole type.
826data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)
828{-!
829deriving instance Binary Forceability
830deriving instance NFData Forceability
831!-}
833data OptInfo = Optimise { collapsible :: Bool,
834 isnewtype :: Bool,
835 -- The following should actually be (IntMap Forceability)
836 -- but the corresponding Binary instance seems to be broken.
837 -- Let's store a list and convert it to IntMap whenever needed.
838 forceable :: [(Int, Forceability)],
839 recursive :: [Int] }
840 deriving Show
841{-!
842deriving instance Binary OptInfo
843deriving instance NFData OptInfo
844!-}
847data TypeInfo = TI { con_names :: [Name],
848 codata :: Bool,
849 data_opts :: DataOpts,
850 param_pos :: [Int] }
851 deriving Show
852{-!
853deriving instance Binary TypeInfo
854deriving instance NFData TypeInfo
855!-}
857-- Syntactic sugar info
859data DSL' t = DSL { dsl_bind :: t,
860 dsl_return :: t,
861 dsl_apply :: t,
862 dsl_pure :: t,
863 dsl_var :: Maybe t,
864 index_first :: Maybe t,
865 index_next :: Maybe t,
866 dsl_lambda :: Maybe t,
867 dsl_let :: Maybe t
868 }
869 deriving (Show, Functor)
870{-!
871deriving instance Binary DSL'
872deriving instance NFData DSL'
873!-}
875type DSL = DSL' PTerm
877data SynContext = PatternSyntax | TermSyntax | AnySyntax
878 deriving Show
879{-!
880deriving instance Binary SynContext
881deriving instance NFData SynContext
882!-}
884data Syntax = Rule [SSymbol] PTerm SynContext
885 deriving Show
886{-!
887deriving instance Binary Syntax
888deriving instance NFData Syntax
889!-}
891data SSymbol = Keyword Name
892 | Symbol String
893 | Binding Name
894 | Expr Name
895 | SimpleExpr Name
896 deriving Show
897{-!
898deriving instance Binary SSymbol
899deriving instance NFData SSymbol
900!-}
902initDSL = DSL (PRef f (sUN ">>="))
903 (PRef f (sUN "return"))
904 (PRef f (sUN "<$>"))
905 (PRef f (sUN "pure"))
906 Nothing
907 Nothing
908 Nothing
909 Nothing
910 Nothing
911 where f = fileFC "(builtin)"
913data Using = UImplicit Name PTerm
914 | UConstraint Name [Name]
915 deriving (Show, Eq)
916{-!
917deriving instance Binary Using
918deriving instance NFData Using
919!-}
921data SyntaxInfo = Syn { using :: [Using],
922 syn_params :: [(Name, PTerm)],
923 syn_namespace :: [String],
924 no_imp :: [Name],
925 decoration :: Name -> Name,
926 inPattern :: Bool,
927 implicitAllowed :: Bool,
928 dsl_info :: DSL }
929 deriving Show
930{-!
931deriving instance NFData SyntaxInfo
932deriving instance Binary SyntaxInfo
933!-}
935defaultSyntax = Syn [] [] [] [] id False False initDSL
937expandNS :: SyntaxInfo -> Name -> Name
938expandNS syn n@(NS _ _) = n
939expandNS syn n = case syn_namespace syn of
940 [] -> n
941 xs -> sNS n xs
944-- For inferring types of things
946bi = fileFC "builtin"
948inferTy = sMN 0 "__Infer"
949inferCon = sMN 0 "__infer"
950inferDecl = PDatadecl inferTy
951 PType
952 [("", [], inferCon, PPi impl (sMN 0 "iType") PType (
953 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
954 (PRef bi inferTy)), bi, [])]
955inferOpts = []
957infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
958infP = P (TCon 6 0) inferTy (TType (UVal 0))
960getInferTerm, getInferType :: Term -> Term
961getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
962getInferTerm (App (App _ _) tm) = tm
963getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
965getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
966 where toTy (Lam t) = Pi t
967 toTy (PVar t) = PVTy t
968 toTy b = b
969getInferType (App (App _ ty) _) = ty
973-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
975primNames = [unitTy, unitCon,
976 falseTy, pairTy, pairCon,
977 eqTy, eqCon, inferTy, inferCon]
979unitTy = sMN 0 "__Unit"
980unitCon = sMN 0 "__II"
981unitDecl = PDatadecl unitTy PType
982 [("", [], unitCon, PRef bi unitTy, bi, [])]
983unitOpts = [DefaultEliminator]
985falseTy = sMN 0 "__False"
986falseDecl = PDatadecl falseTy PType []
987falseOpts = []
989pairTy = sMN 0 "__Pair"
990pairCon = sMN 0 "__MkPair"
991pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
992 [("", [], pairCon, PPi impl (n "A") PType (
993 PPi impl (n "B") PType (
994 PPi expl (n "a") (PRef bi (n "A")) (
995 PPi expl (n "b") (PRef bi (n "B"))
996 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
997 pexp (PRef bi (n "B"))])))), bi, [])]
998 where n a = sMN 0 a
999pairOpts = []
1001eqTy = sUN "="
1002eqCon = sUN "refl"
1003eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1004 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1005 PType)
1006 [("", [], eqCon, PPi impl (n "A") PType (
1007 PPi impl (n "x") (PRef bi (n "A"))
1008 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1009 pimp (n "B") Placeholder False,
1010 pexp (PRef bi (n "x")),
1011 pexp (PRef bi (n "x"))])), bi, [])]
1012 where n a = sMN 0 a
1013eqOpts = []
1015elimName = sUN "__Elim"
1016elimMethElimTy = sUN "__elimTy"
1017elimMethElim = sUN "elim"
1018elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
1019 [PTy "" [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1020 PTy "" [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1022-- Defined in builtins.idr
1023sigmaTy = sUN "Exists"
1024existsCon = sUN "Ex_intro"
1026piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1027piBind = piBindp expl
1029piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1030piBindp p [] t = t
1031piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1034-- Pretty-printing declarations and terms
1036-- These "show" instances render to an absurdly wide screen because inserted line breaks
1037-- could interfere with interactive editing, which calls "show".
1039instance Show PTerm where
1040 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm
1042instance Show PDecl where
1043 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d
1045instance Show PClause where
1046 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c
1048instance Show PData where
1049 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d
1051instance Pretty PTerm OutputAnnotation where
1052 pretty = prettyImp False
1054-- | Colourise annotations according to an Idris state. It ignores the names
1055-- in the annotation, as there's no good way to show extended information on a
1056-- terminal.
1057consoleDecorate :: IState -> OutputAnnotation -> String -> String
1058consoleDecorate ist _ | not (idris_colourRepl ist) = id
1059consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist
1060 in colouriseData theme
1061consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
1062 in colouriseType theme
1063consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1064consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1065consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist
1066 theme = idris_colourTheme ist
1067 in case () of
1068 _ | isDConName n ctxt -> colouriseData theme
1069 _ | isFnName n ctxt -> colouriseFun theme
1070 _ | isTConName n ctxt -> colouriseType theme
1071 _ | otherwise -> id -- don't colourise unknown names
1072consoleDecorate ist (AnnFC _) = id
1074-- | Pretty-print a high-level closed Idris term
1075prettyImp :: Bool -- ^^ whether to show implicits
1076 -> PTerm -- ^^ the term to pretty-print
1077 -> Doc OutputAnnotation
1078prettyImp impl = pprintPTerm impl []
1080-- | Pretty-print a high-level Idris term in some bindings context
1081pprintPTerm :: Bool -- ^^ whether to show implicits
1082 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1083 -> PTerm -- ^^ the term to pretty-print
1084 -> Doc OutputAnnotation
1085pprintPTerm impl bnd = prettySe 10 bnd
1086 where
1087 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1088 prettySe p bnd (PQuote r) =
1089 text "![" <> pretty r <> text "]"
1090 prettySe p bnd (PPatvar fc n) = pretty n
1091 prettySe p bnd e
1092 | Just str <- slist p bnd e = str
1093 | Just n <- snat p e = annotate AnnConstData (text (show n))
1094 prettySe p bnd (PRef fc n) = prettyName impl bnd n
1095 prettySe p bnd (PLam n ty sc) =
1096 bracket p 2 . group . align . hang 2 $
1097 text "\\" <> bindingOf n False <+> text "=>" <$>
1098 prettySe 10 ((n, False):bnd) sc
1099 prettySe p bnd (PLet n ty v sc) =
1100 bracket p 2 $
1101 text "let" <+> bindingOf n False <+> text "=" </>
1102 prettySe 10 bnd v <+> text "in" </>
1103 prettySe 10 ((n, False):bnd) sc
1104 prettySe p bnd (PPi (Exp l s _) n ty sc)
1105 | n `elem` allNamesIn sc || impl =
1106 let open = if Lazy `elem` l then text "|" <> lparen else lparen in
1107 bracket p 2 . group $
1108 enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1109 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1110 | otherwise =
1111 bracket p 2 . group $
1112 group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1113 where
1114 st =
1115 case s of
1116 Static -> text "[static]" <> space
1117 _ -> empty
1118 prettySe p bnd (PPi (Imp l s _) n ty sc)
1119 | impl =
1120 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in
1121 bracket p 2 $
1122 open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1123 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1124 | otherwise = prettySe 10 ((n, True):bnd) sc
1125 where
1126 st =
1127 case s of
1128 Static -> text "[static]" <> space
1129 _ -> empty
1130 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1131 bracket p 2 $
1132 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1133 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1134 bracket p 2 $
1135 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1136 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1137 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1138 | UN nm <- basename f
1139 , not impl && null (getExps args) = if isAlpha (thead nm)
1140 then prettyName impl bnd f
1141 else enclose lparen rparen $
1142 prettyName impl bnd f
1143 prettySe p bnd (PAppBind _ (PRef _ f) [])
1144 | not impl = text "!" <> prettyName impl bnd f
1145 prettySe p bnd (PApp _ (PRef _ op) args)
1146 | UN nm <- basename op
1147 , not (tnull nm) &&
1148 (not impl) && (not $ isAlpha (thead nm)) =
1149 case getExps args of
1150 [] -> enclose lparen rparen opName
1151 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))
1152 [l,r] -> bracket p 1 $ inFix l r
1153 (l:r:rest) -> bracket p 1 $
1154 enclose lparen rparen (inFix l r) <+>
1155 align (group (vsep (map (prettyArgSe bnd) rest)))
1156 where opName = prettyName impl bnd op
1157 inFix l r = align . group $
1158 (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)
1159 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1160 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1161 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1162 prettySe p bnd (PApp _ f as) =
1163 let args = getExps as
1164 fp = prettySe 1 bnd f
1165 in
1166 bracket p 1 . group $
1167 if impl
1168 then if null as
1169 then fp
1170 else fp <+> align (vsep (map (prettyArgS bnd) as))
1171 else if null args
1172 then fp
1173 else fp <+> align (vsep (map (prettyArgSe bnd) args))
1174 prettySe p bnd (PCase _ scr opts) =
1175 text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
1176 where
1177 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1179 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1180 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1181 prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
1182 prettySe p bnd (PResolveTC _) = text "resolvetc"
1183 prettySe p bnd (PTrue _ IsType) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
1184 prettySe p bnd (PTrue _ IsTerm) = annotate (AnnName unitCon Nothing Nothing) $ text "()"
1185 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1186 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
1187 prettySe p bnd (PEq _ l r) =
1188 bracket p 2 . align . group $
1189 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1190 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
1191 prettySe p bnd (PRewrite _ l r _) =
1192 bracket p 2 $
1193 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1194 prettySe p bnd (PTyped l r) =
1195 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1196 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1197 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1198 align . group . vsep . punctuate (ann comma) $
1199 map (prettySe 10 bnd) elts
1200 where ann = case pun of
1201 TypeOrTerm -> id
1202 IsType -> annotate (AnnName pairTy Nothing Nothing)
1203 IsTerm -> annotate (AnnName pairCon Nothing Nothing)
1204 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1205 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1206 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1207 annotate (AnnName sigmaTy Nothing Nothing) lparen <>
1208 bindingOf n False <+>
1209 annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>
1210 prettySe 10 ((n, False):bnd) r <>
1211 annotate (AnnName sigmaTy Nothing Nothing) rparen
1212 prettySe p bnd (PDPair _ IsType l t r) =
1213 annotate (AnnName sigmaTy Nothing Nothing) lparen <>
1214 prettySe 10 bnd l <+>
1215 annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>
1216 prettySe 10 bnd r <>
1217 annotate (AnnName sigmaTy Nothing Nothing) rparen
1218 prettySe p bnd (PDPair _ IsTerm l t r) =
1219 annotate (AnnName existsCon Nothing Nothing) lparen <>
1220 prettySe 10 bnd l <+>
1221 annotate (AnnName existsCon Nothing Nothing) (text "**") <+>
1222 prettySe 10 bnd r <>
1223 annotate (AnnName existsCon Nothing Nothing) rparen
1224 prettySe p bnd (PAlternative a as) =
1225 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1226 where
1227 prettyAs =
1228 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1229 prettySe p bnd PType = annotate AnnConstType $ text "Type"
1230 prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))
1231 where annot (AType _) = AnnConstType
1232 annot StrType = AnnConstType
1233 annot PtrType = AnnConstType
1234 annot VoidType = AnnConstType
1235 annot _ = AnnConstData
1236 -- XXX: add pretty for tactics
1237 prettySe p bnd (PProof ts) =
1238 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1239 prettySe p bnd (PTactics ts) =
1240 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1241 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1242 prettySe p bnd (PReturn f) = text "return"
1243 prettySe p bnd PImpossible = text "impossible"
1244 prettySe p bnd Placeholder = text "_"
1245 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1246 prettySe p bnd (PElabError s) = pretty s
1248 prettySe p bnd _ = text "test"
1250 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1251 prettyArgS bnd (PExp _ _ tm) = prettyArgSe bnd tm
1252 prettyArgS bnd (PConstraint _ _ tm) = prettyArgSc bnd tm
1253 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1255 prettyArgSe bnd arg = prettySe 0 bnd arg
1256 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1257 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1258 prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1260 basename :: Name -> Name
1261 basename (NS n _) = basename n
1262 basename n = n
1264 slist' p bnd (PApp _ (PRef _ nil) _)
1265 | not impl && nsroot nil == sUN "Nil" = Just []
1266 slist' p bnd (PRef _ nil)
1267 | not impl && nsroot nil == sUN "Nil" = Just []
1268 slist' p bnd (PApp _ (PRef _ cons) args)
1269 | nsroot cons == sUN "::",
1270 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1271 all isImp imps,
1272 Just tl' <- slist' p bnd tl
1273 = Just (hd:tl')
1274 where
1275 isImp (PImp {}) = True
1276 isImp _ = False
1277 slist' _ _ tm = Nothing
1279 slist p bnd e | Just es <- slist' p bnd e = Just $
1280 case es of [] -> annotate AnnConstData $ text "[]"
1281 [x] -> enclose left right . group $
1282 prettySe p bnd x
1283 xs -> (enclose left right .
1284 align . group . vsep .
1285 punctuate comma .
1286 map (prettySe p bnd)) xs
1287 where left = (annotate AnnConstData (text "["))
1288 right = (annotate AnnConstData (text "]"))
1289 comma = (annotate AnnConstData (text ","))
1290 slist _ _ _ = Nothing
1292 pairElts :: PTerm -> Maybe [PTerm]
1293 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1294 | otherwise = Just [x, y]
1295 pairElts _ = Nothing
1297 natns = "Prelude.Nat."
1299 snat p (PRef _ z)
1300 | show z == (natns++"Z") || show z == "Z" = Just 0
1301 snat p (PApp _ s [PExp {getTm=n}])
1302 | show s == (natns++"S") || show s == "S",
1303 Just n' <- snat p n
1304 = Just $ 1 + n'
1305 snat _ _ = Nothing
1307 bracket outer inner doc
1308 | inner > outer = lparen <> doc <> rparen
1309 | otherwise = doc
1311-- | Pretty-printer helper for the binding site of a name
1312bindingOf :: Name -- ^^ the bound name
1313 -> Bool -- ^^ whether the name is implicit
1314 -> Doc OutputAnnotation
1315bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1317-- | Pretty-printer helper for names that attaches the correct annotations
1318prettyName :: Bool -- ^^ whether to show namespaces
1319 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1320 -> Name -- ^^ the name to pprint
1321 -> Doc OutputAnnotation
1322prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
1323 | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))
1324 where strName (UN n) = T.unpack n
1325 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1326 | otherwise = strName n
1327 strName (MN i s) = T.unpack s
1328 strName other = show other
1331showCImp :: Bool -> PClause -> Doc OutputAnnotation
1332showCImp impl (PClause _ n l ws r w)
1333 = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r
1334 <+> text "where" <+> text (show w)
1335 where
1336 showWs [] = empty
1337 showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1338showCImp impl (PWith _ n l ws r w)
1339 = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r
1340 <+> braces (text (show w))
1341 where
1342 showWs [] = empty
1343 showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
1346showDImp :: Bool -> PData -> Doc OutputAnnotation
1347showDImp impl (PDatadecl n ty cons)
1348 = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>
1349 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))
1351showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
1352showDecls i ds = vsep (map (showDeclImp i) ds)
1354showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1355showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t
1356showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1357 indent 2 (vsep (map (showCImp i) cs))
1358showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d
1359showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)
1360showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)
1361showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1362showDeclImp i (PClass _ _ _ cs n ps ds)
1363 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds
1364showDeclImp i (PInstance _ _ cs n _ t _ ds)
1365 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds
1366showDeclImp _ _ = text "..."
1367-- showDeclImp (PImport i) = "import " ++ i
1369instance Show (Doc OutputAnnotation) where
1370 show = flip (displayS . renderCompact) ""
1372getImps :: [PArg] -> [(Name, PTerm)]
1373getImps [] = []
1374getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1375getImps (_ : xs) = getImps xs
1377getExps :: [PArg] -> [PTerm]
1378getExps [] = []
1379getExps (PExp _ _ tm : xs) = tm : getExps xs
1380getExps (_ : xs) = getExps xs
1382getConsts :: [PArg] -> [PTerm]
1383getConsts [] = []
1384getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
1385getConsts (_ : xs) = getConsts xs
1387getAll :: [PArg] -> [PTerm]
1388getAll = map getTm
1391-- | Show Idris name
1392showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1393 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1394 -> Bool -- ^^ whether to show implicits
1395 -> Bool -- ^^ whether to colourise
1396 -> Name -- ^^ the term to show
1397 -> String
1398showName ist bnd impl colour n = case ist of
1399 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1400 Nothing -> showbasic n
1401 where name = if impl then show n else showbasic n
1402 showbasic n@(UN _) = showCG n
1403 showbasic (MN _ s) = str s
1404 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1405 showbasic (SN s) = show s
1406 fst3 (x, _, _) = x
1407 colourise n t = let ctxt' = fmap tt_ctxt ist in
1408 case ctxt' of
1409 Nothing -> name
1410 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1411 else colouriseBound t name
1412 | isDConName n ctxt -> colouriseData t name
1413 | isFnName n ctxt -> colouriseFun t name
1414 | isTConName n ctxt -> colouriseType t name
1415 -- The assumption is that if a name is not bound and does not exist in the
1416 -- global context, then we're somewhere in which implicit info has been lost
1417 -- (like error messages). Thus, unknown vars are colourised as implicits.
1418 | otherwise -> colouriseImplicit t name
1420showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1421 -> PTerm -- ^^ the term to show
1422 -> String
1423showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))
1425-- | Show a term with implicits, no colours
1426showTmImpls :: PTerm -> String
1427showTmImpls = flip (displayS . renderCompact . prettyImp True) ""
1430instance Sized PTerm where
1431 size (PQuote rawTerm) = size rawTerm
1432 size (PRef fc name) = size name
1433 size (PLam name ty bdy) = 1 + size ty + size bdy
1434 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1435 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1436 size (PTyped trm ty) = 1 + size trm + size ty
1437 size (PApp fc name args) = 1 + size args
1438 size (PAppBind fc name args) = 1 + size args
1439 size (PCase fc trm bdy) = 1 + size trm + size bdy
1440 size (PTrue fc _) = 1
1441 size (PFalse fc) = 1
1442 size (PRefl fc _) = 1
1443 size (PResolveTC fc) = 1
1444 size (PEq fc left right) = 1 + size left + size right
1445 size (PRewrite fc left right _) = 1 + size left + size right
1446 size (PPair fc _ left right) = 1 + size left + size right
1447 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1448 size (PAlternative a alts) = 1 + size alts
1449 size (PHidden hidden) = size hidden
1450 size (PUnifyLog tm) = size tm
1451 size (PDisamb _ tm) = size tm
1452 size (PNoImplicits tm) = size tm
1453 size PType = 1
1454 size (PConstant const) = 1 + size const
1455 size Placeholder = 1
1456 size (PDoBlock dos) = 1 + size dos
1457 size (PIdiom fc term) = 1 + size term
1458 size (PReturn fc) = 1
1459 size (PMetavar name) = 1
1460 size (PProof tactics) = size tactics
1461 size (PElabError err) = size err
1462 size PImpossible = 1
1464getPArity :: PTerm -> Int
1465getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1466getPArity _ = 0
1468-- Return all names, free or globally bound, in the given term.
1470allNamesIn :: PTerm -> [Name]
1471allNamesIn tm = nub $ ni [] tm
1472 where
1473 ni env (PRef _ n)
1474 | not (n `elem` env) = [n]
1475 ni env (PPatvar _ n) = [n]
1476 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1477 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1478 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1479 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1480 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1481 ni env (PHidden tm) = ni env tm
1482 ni env (PEq _ l r) = ni env l ++ ni env r
1483 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1484 ni env (PTyped l r) = ni env l ++ ni env r
1485 ni env (PPair _ _ l r) = ni env l ++ ni env r
1486 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1487 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1488 ni env (PAlternative a ls) = concatMap (ni env) ls
1489 ni env (PUnifyLog tm) = ni env tm
1490 ni env (PDisamb _ tm) = ni env tm
1491 ni env (PNoImplicits tm) = ni env tm
1492 ni env _ = []
1494-- Return all names defined in binders in the given term
1495boundNamesIn :: PTerm -> [Name]
1496boundNamesIn tm = nub $ ni tm
1497 where
1498 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1499 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1500 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1501 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1502 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1503 ni (PPi _ n ty sc) = n : (ni ty ++ ni sc)
1504 ni (PEq _ l r) = ni l ++ ni r
1505 ni (PRewrite _ l r _) = ni l ++ ni r
1506 ni (PTyped l r) = ni l ++ ni r
1507 ni (PPair _ _ l r) = ni l ++ ni r
1508 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1509 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1510 ni (PAlternative a as) = concatMap (ni) as
1511 ni (PHidden tm) = ni tm
1512 ni (PUnifyLog tm) = ni tm
1513 ni (PDisamb _ tm) = ni tm
1514 ni (PNoImplicits tm) = ni tm
1515 ni _ = []
1517-- Return names which are free in the given term.
1518namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1519namesIn uvars ist tm = nub $ ni [] tm
1520 where
1521 ni env (PRef _ n)
1522 | not (n `elem` env)
1523 = case lookupTy n (tt_ctxt ist) of
1524 [] -> [n]
1525 _ -> if n `elem` (map fst uvars) then [n] else []
1526 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1527 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1528 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1529 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1530 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1531 ni env (PEq _ l r) = ni env l ++ ni env r
1532 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1533 ni env (PTyped l r) = ni env l ++ ni env r
1534 ni env (PPair _ _ l r) = ni env l ++ ni env r
1535 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1536 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1537 ni env (PAlternative a as) = concatMap (ni env) as
1538 ni env (PHidden tm) = ni env tm
1539 ni env (PUnifyLog tm) = ni env tm
1540 ni env (PDisamb _ tm) = ni env tm
1541 ni env (PNoImplicits tm) = ni env tm
1542 ni env _ = []
1544-- Return which of the given names are used in the given term.
1546usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1547usedNamesIn vars ist tm = nub $ ni [] tm
1548 where
1549 ni env (PRef _ n)
1550 | n `elem` vars && not (n `elem` env)
1551 = case lookupTy n (tt_ctxt ist) of
1552 [] -> [n]
1553 _ -> []
1554 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1555 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1556 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1557 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1558 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1559 ni env (PEq _ l r) = ni env l ++ ni env r
1560 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1561 ni env (PTyped l r) = ni env l ++ ni env r
1562 ni env (PPair _ _ l r) = ni env l ++ ni env r
1563 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1564 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1565 ni env (PAlternative a as) = concatMap (ni env) as
1566 ni env (PHidden tm) = ni env tm
1567 ni env (PUnifyLog tm) = ni env tm
1568 ni env (PDisamb _ tm) = ni env tm
1569 ni env (PNoImplicits tm) = ni env tm
1570 ni env _ = []