git.iko.soy/Idris-dev
on d90165e help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1031 lines 36 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
6import Core.TT
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
10import IRTS.Lang
11import Util.Pretty
13import Paths_idris
15import System.Console.Haskeline
17import Control.Monad.Trans.State.Strict
19import Data.List
20import Data.Char
21import Data.Either
23import Debug.Trace
25data IOption = IOption { opt_logLevel :: Int,
26 opt_typecase :: Bool,
27 opt_typeintype :: Bool,
28 opt_coverage :: Bool,
29 opt_showimp :: Bool,
30 opt_errContext :: Bool,
31 opt_repl :: Bool,
32 opt_verbose :: Bool,
33 opt_ibcsubdir :: FilePath,
34 opt_importdirs :: [FilePath],
35 opt_cmdline :: [Opt] -- remember whole command line
36 }
37 deriving (Show, Eq)
39defaultOpts = IOption 0 False False True False False True True "" [] []
41-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
42-- without typechecking).
43-- This will include all the functions and data declarations, plus fixity declarations
44-- and syntax macros.
46data IState = IState {
47 tt_ctxt :: Context,
48 idris_constraints :: [(UConstraint, FC)],
49 idris_infixes :: [FixDecl],
50 idris_implicits :: Ctxt [PArg],
51 idris_statics :: Ctxt [Bool],
52 idris_classes :: Ctxt ClassInfo,
53 idris_dsls :: Ctxt DSL,
54 idris_optimisation :: Ctxt OptInfo,
55 idris_datatypes :: Ctxt TypeInfo,
56 idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
57 idris_flags :: Ctxt [FnOpt],
58 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
59 idris_calledgraph :: Ctxt [Name],
60 idris_docstrings :: Ctxt String,
61 idris_totcheck :: [(FC, Name)],
62 idris_log :: String,
63 idris_options :: IOption,
64 idris_name :: Int,
65 idris_metavars :: [Name],
66 syntax_rules :: [Syntax],
67 syntax_keywords :: [String],
68 imported :: [FilePath],
69 idris_scprims :: [(Name, (Int, PrimFn))],
70 idris_objs :: [FilePath],
71 idris_libs :: [String],
72 idris_hdrs :: [String],
73 proof_list :: [(Name, [String])],
74 errLine :: Maybe Int,
75 lastParse :: Maybe Name,
76 indent_stack :: [Int],
77 brace_stack :: [Maybe Int],
78 hide_list :: [(Name, Maybe Accessibility)],
79 default_access :: Accessibility,
80 default_total :: Bool,
81 ibc_write :: [IBCWrite],
82 compiled_so :: Maybe String
83 }
85data SizeChange = Smaller | Same | Bigger | Unknown
86 deriving (Show, Eq)
87{-!
88deriving instance Binary SizeChange
89!-}
91type SCGEntry = (Name, [Maybe (Int, SizeChange)])
93data CGInfo = CGInfo { argsdef :: [Name],
94 calls :: [(Name, [[Name]])],
95 scg :: [SCGEntry],
96 argsused :: [Name],
97 unusedpos :: [Int] }
98 deriving Show
99{-!
100deriving instance Binary CGInfo
101!-}
103primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
105-- information that needs writing for the current module's .ibc file
106data IBCWrite = IBCFix FixDecl
107 | IBCImp Name
108 | IBCStatic Name
109 | IBCClass Name
110 | IBCInstance Bool Name Name
111 | IBCDSL Name
112 | IBCData Name
113 | IBCOpt Name
114 | IBCSyntax Syntax
115 | IBCKeyword String
116 | IBCImport FilePath
117 | IBCObj FilePath
118 | IBCLib String
119 | IBCHeader String
120 | IBCAccess Name Accessibility
121 | IBCTotal Name Totality
122 | IBCFlags Name [FnOpt]
123 | IBCCG Name
124 | IBCDoc Name
125 | IBCDef Name -- i.e. main context
126 deriving Show
128idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
129 emptyContext emptyContext emptyContext emptyContext
130 emptyContext emptyContext emptyContext emptyContext
131 [] "" defaultOpts 6 [] [] [] [] [] [] [] []
132 [] Nothing Nothing [] [] [] Hidden False [] Nothing
134-- The monad for the main REPL - reading and processing files and updating
135-- global state (hence the IO inner monad).
136type Idris = StateT IState (InputT IO)
138-- Commands in the REPL
140data Target = ViaC | ViaJava
142data Command = Quit
143 | Help
144 | Eval PTerm
145 | Check PTerm
146 | DocStr Name
147 | TotCheck Name
148 | Reload
149 | Load FilePath
150 | ModImport String
151 | Edit
152 | Compile Target String
153 | Execute
154 | ExecVal PTerm
155 | NewCompile String
156 | Metavars
157 | Prove Name
158 | AddProof (Maybe Name)
159 | RmProof Name
160 | ShowProof Name
161 | Proofs
162 | Universes
163 | TTShell
164 | LogLvl Int
165 | Spec PTerm
166 | HNF PTerm
167 | Defn Name
168 | Info Name
169 | Missing Name
170 | Pattelab PTerm
171 | DebugInfo Name
172 | Search PTerm
173 | SetOpt Opt
174 | UnsetOpt Opt
175 | NOP
177data Opt = Filename String
178 | Ver
179 | Usage
180 | ShowLibs
181 | ShowLibdir
182 | ShowIncs
183 | NoPrelude
184 | NoREPL
185 | OLogging Int
186 | Output String
187 | NewOutput String
188 | TypeCase
189 | TypeInType
190 | DefaultTotal
191 | DefaultPartial
192 | WarnPartial
193 | NoCoverage
194 | ErrContext
195 | ShowImpl
196 | Verbose
197 | IBCSubDir String
198 | ImportDir String
199 | PkgBuild String
200 | PkgInstall String
201 | PkgClean String
202 | WarnOnly
203 | Pkg String
204 | BCAsm String
205 | DumpC String
206 | DumpDefun String
207 | DumpCases String
208 | FOVM String
209 deriving (Show, Eq)
212-- Parsed declarations
214data Fixity = Infixl { prec :: Int }
215 | Infixr { prec :: Int }
216 | InfixN { prec :: Int }
217 | PrefixN { prec :: Int }
218 deriving Eq
219{-!
220deriving instance Binary Fixity
221!-}
223instance Show Fixity where
224 show (Infixl i) = "infixl " ++ show i
225 show (Infixr i) = "infixr " ++ show i
226 show (InfixN i) = "infix " ++ show i
227 show (PrefixN i) = "prefix " ++ show i
229data FixDecl = Fix Fixity String
230 deriving (Show, Eq)
231{-!
232deriving instance Binary FixDecl
233!-}
235instance Ord FixDecl where
236 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
239data Static = Static | Dynamic
240 deriving (Show, Eq)
241{-!
242deriving instance Binary Static
243!-}
245-- Mark bindings with their explicitness, and laziness
246data Plicity = Imp { plazy :: Bool,
247 pstatic :: Static,
248 pdocstr :: String }
249 | Exp { plazy :: Bool,
250 pstatic :: Static,
251 pdocstr :: String }
252 | Constraint { plazy :: Bool,
253 pstatic :: Static,
254 pdocstr :: String }
255 | TacImp { plazy :: Bool,
256 pstatic :: Static,
257 pscript :: PTerm,
258 pdocstr :: String }
259 deriving (Show, Eq)
261{-!
262deriving instance Binary Plicity
263!-}
265impl = Imp False Dynamic ""
266expl = Exp False Dynamic ""
267constraint = Constraint False Dynamic ""
268tacimpl t = TacImp False Dynamic t ""
270data FnOpt = Inlinable | TotalFn | PartialFn
271 | Coinductive | AssertTotal | TCGen
272 | CExport String -- export, with a C name
273 | Specialise [Name] -- specialise it, freeze these names
274 deriving (Show, Eq)
275{-!
276deriving instance Binary FnOpt
277!-}
279type FnOpts = [FnOpt]
281inlinable :: FnOpts -> Bool
282inlinable = elem Inlinable
284data PDecl' t = PFix FC Fixity [String] -- fixity declaration
285 | PTy String SyntaxInfo FC FnOpts Name t -- type declaration
286 | PClauses FC FnOpts Name [PClause' t] -- pattern clause
287 | PCAF FC Name t -- top level constant
288 | PData String SyntaxInfo FC Bool -- codata
289 (PData' t) -- data declaration
290 | PParams FC [(Name, t)] [PDecl' t] -- params block
291 | PNamespace String [PDecl' t] -- new namespace
292 | PRecord String SyntaxInfo FC Name t String Name t -- record declaration
293 | PClass String SyntaxInfo FC
294 [t] -- constraints
295 Name
296 [(Name, t)] -- parameters
297 [PDecl' t] -- declarations
298 | PInstance SyntaxInfo FC [t] -- constraints
299 Name -- class
300 [t] -- parameters
301 t -- full instance type
302 (Maybe Name) -- explicit name
303 [PDecl' t]
304 | PDSL Name (DSL' t)
305 | PSyntax FC Syntax
306 | PMutual FC [PDecl' t]
307 | PDirective (Idris ())
308 deriving Functor
309{-!
310deriving instance Binary PDecl'
311!-}
313data PClause' t = PClause FC Name t [t] t [PDecl' t]
314 | PWith FC Name t [t] t [PDecl' t]
315 | PClauseR FC [t] t [PDecl' t]
316 | PWithR FC [t] t [PDecl' t]
317 deriving Functor
318{-!
319deriving instance Binary PClause'
320!-}
322data PData' t = PDatadecl { d_name :: Name,
323 d_tcon :: t,
324 d_cons :: [(String, Name, t, FC)] }
325 | PLaterdecl { d_name :: Name, d_tcon :: t }
326 deriving Functor
327{-!
328deriving instance Binary PData'
329!-}
331-- Handy to get a free function for applying PTerm -> PTerm functions
332-- across a program, by deriving Functor
334type PDecl = PDecl' PTerm
335type PData = PData' PTerm
336type PClause = PClause' PTerm
338-- get all the names declared in a decl
340declared :: PDecl -> [Name]
341declared (PFix _ _ _) = []
342declared (PTy _ _ _ _ n t) = [n]
343declared (PClauses _ _ n _) = [] -- not a declaration
344declared (PRecord _ _ _ n _ _ c _) = [n, c]
345declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
346 where fstt (_, a, _, _) = a
347declared (PParams _ _ ds) = concatMap declared ds
348declared (PMutual _ ds) = concatMap declared ds
349declared (PNamespace _ ds) = concatMap declared ds
350-- declared (PImport _) = []
352defined :: PDecl -> [Name]
353defined (PFix _ _ _) = []
354defined (PTy _ _ _ _ n t) = []
355defined (PClauses _ _ n _) = [n] -- not a declaration
356defined (PRecord _ _ _ n _ _ c _) = [n, c]
357defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
358 where fstt (_, a, _, _) = a
359defined (PParams _ _ ds) = concatMap defined ds
360defined (PMutual _ ds) = concatMap defined ds
361defined (PNamespace _ ds) = concatMap defined ds
362-- declared (PImport _) = []
364updateN :: [(Name, Name)] -> Name -> Name
365updateN ns n | Just n' <- lookup n ns = n'
366updateN _ n = n
368updateNs :: [(Name, Name)] -> PTerm -> PTerm
369updateNs [] t = t
370updateNs ns t = mapPT updateRef t
371 where updateRef (PRef fc f) = PRef fc (updateN ns f)
372 updateRef t = t
374-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
375-- updateDNs [] t = t
376-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
377-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
378-- where updateCNs ns (PClause n l ts r ds)
379-- = PClause (updateN ns n) (fmap (updateNs ns) l)
380-- (map (fmap (updateNs ns)) ts)
381-- (fmap (updateNs ns) r)
382-- (map (updateDNs ns) ds)
383-- updateDNs ns c = c
385-- High level language terms
387data PTerm = PQuote Raw
388 | PRef FC Name
389 | PPatvar FC Name
390 | PLam Name PTerm PTerm
391 | PPi Plicity Name PTerm PTerm
392 | PLet Name PTerm PTerm PTerm
393 | PTyped PTerm PTerm -- term with explicit type
394 | PApp FC PTerm [PArg]
395 | PCase FC PTerm [(PTerm, PTerm)]
396 | PTrue FC
397 | PFalse FC
398 | PRefl FC PTerm
399 | PResolveTC FC
400 | PEq FC PTerm PTerm
401 | PPair FC PTerm PTerm
402 | PDPair FC PTerm PTerm PTerm
403 | PAlternative Bool [PTerm] -- True if only one may work
404 | PHidden PTerm -- irrelevant or hidden pattern
405 | PSet
406 | PConstant Const
407 | Placeholder
408 | PDoBlock [PDo]
409 | PIdiom FC PTerm
410 | PReturn FC
411 | PMetavar Name
412 | PProof [PTactic]
413 | PTactics [PTactic] -- as PProof, but no auto solving
414 | PElabError Err -- error to report on elaboration
415 | PImpossible -- special case for declaring when an LHS can't typecheck
416 deriving Eq
417{-!
418deriving instance Binary PTerm
419!-}
421mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
422mapPT f t = f (mpt t) where
423 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
424 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
425 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
426 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
427 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
428 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
429 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
430 mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
431 mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
432 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
433 mpt (PHidden t) = PHidden (mapPT f t)
434 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
435 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
436 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
437 mpt x = x
440data PTactic' t = Intro [Name] | Intros | Focus Name
441 | Refine Name [Bool] | Rewrite t | LetTac Name t
442 | Exact t | Compute | Trivial
443 | Solve
444 | Attack
445 | ProofState | ProofTerm | Undo
446 | Try (PTactic' t) (PTactic' t)
447 | TSeq (PTactic' t) (PTactic' t)
448 | Qed | Abandon
449 deriving (Show, Eq, Functor)
450{-!
451deriving instance Binary PTactic'
452!-}
454instance Sized a => Sized (PTactic' a) where
455 size (Intro nms) = 1 + size nms
456 size Intros = 1
457 size (Focus nm) = 1 + size nm
458 size (Refine nm bs) = 1 + size nm + length bs
459 size (Rewrite t) = 1 + size t
460 size (LetTac nm t) = 1 + size nm + size t
461 size (Exact t) = 1 + size t
462 size Compute = 1
463 size Trivial = 1
464 size Solve = 1
465 size Attack = 1
466 size ProofState = 1
467 size ProofTerm = 1
468 size Undo = 1
469 size (Try l r) = 1 + size l + size r
470 size (TSeq l r) = 1 + size l + size r
471 size Qed = 1
472 size Abandon = 1
474type PTactic = PTactic' PTerm
476data PDo' t = DoExp FC t
477 | DoBind FC Name t
478 | DoBindP FC t t
479 | DoLet FC Name t t
480 | DoLetP FC t t
481 deriving (Eq, Functor)
482{-!
483deriving instance Binary PDo'
484!-}
486instance Sized a => Sized (PDo' a) where
487 size (DoExp fc t) = 1 + size fc + size t
488 size (DoBind fc nm t) = 1 + size fc + size nm + size t
489 size (DoBindP fc l r) = 1 + size fc + size l + size r
490 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
491 size (DoLetP fc l r) = 1 + size fc + size l + size r
493type PDo = PDo' PTerm
495-- The priority gives a hint as to elaboration order. Best to elaborate
496-- things early which will help give a more concrete type to other
497-- variables, e.g. a before (interpTy a).
499data PArg' t = PImp { priority :: Int,
500 lazyarg :: Bool, pname :: Name, getTm :: t,
501 pargdoc :: String }
502 | PExp { priority :: Int,
503 lazyarg :: Bool, getTm :: t,
504 pargdoc :: String }
505 | PConstraint { priority :: Int,
506 lazyarg :: Bool, getTm :: t,
507 pargdoc :: String }
508 | PTacImplicit { priority :: Int,
509 lazyarg :: Bool, pname :: Name,
510 getScript :: t,
511 getTm :: t,
512 pargdoc :: String }
513 deriving (Show, Eq, Functor)
515instance Sized a => Sized (PArg' a) where
516 size (PImp p l nm trm _) = 1 + size nm + size trm
517 size (PExp p l trm _) = 1 + size trm
518 size (PConstraint p l trm _) = 1 + size trm
519 size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm
521{-!
522deriving instance Binary PArg'
523!-}
525pimp n t = PImp 0 True n t ""
526pexp t = PExp 0 False t ""
527pconst t = PConstraint 0 False t ""
528ptacimp n s t = PTacImplicit 0 True n s t ""
530type PArg = PArg' PTerm
532-- Type class data
534data ClassInfo = CI { instanceName :: Name,
535 class_methods :: [(Name, (FnOpts, PTerm))],
536 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
537 class_params :: [Name],
538 class_instances :: [Name] }
539 deriving Show
540{-!
541deriving instance Binary ClassInfo
542!-}
544data OptInfo = Optimise { collapsible :: Bool,
545 forceable :: [Int], -- argument positions
546 recursive :: [Int] }
547 deriving Show
548{-!
549deriving instance Binary OptInfo
550!-}
553data TypeInfo = TI { con_names :: [Name], codata :: Bool }
554 deriving Show
555{-!
556deriving instance Binary TypeInfo
557!-}
559-- Syntactic sugar info
561data DSL' t = DSL { dsl_bind :: t,
562 dsl_return :: t,
563 dsl_apply :: t,
564 dsl_pure :: t,
565 dsl_var :: Maybe t,
566 index_first :: Maybe t,
567 index_next :: Maybe t,
568 dsl_lambda :: Maybe t,
569 dsl_let :: Maybe t
570 }
571 deriving (Show, Functor)
572{-!
573deriving instance Binary DSL'
574!-}
576type DSL = DSL' PTerm
578data SynContext = PatternSyntax | TermSyntax | AnySyntax
579 deriving Show
580{-!
581deriving instance Binary SynContext
582!-}
584data Syntax = Rule [SSymbol] PTerm SynContext
585 deriving Show
586{-!
587deriving instance Binary Syntax
588!-}
590data SSymbol = Keyword Name
591 | Symbol String
592 | Binding Name
593 | Expr Name
594 | SimpleExpr Name
595 deriving Show
596{-!
597deriving instance Binary SSymbol
598!-}
600initDSL = DSL (PRef f (UN ">>="))
601 (PRef f (UN "return"))
602 (PRef f (UN "<$>"))
603 (PRef f (UN "pure"))
604 Nothing
605 Nothing
606 Nothing
607 Nothing
608 Nothing
609 where f = FC "(builtin)" 0
611data SyntaxInfo = Syn { using :: [(Name, PTerm)],
612 syn_params :: [(Name, PTerm)],
613 syn_namespace :: [String],
614 no_imp :: [Name],
615 decoration :: Name -> Name,
616 inPattern :: Bool,
617 implicitAllowed :: Bool,
618 dsl_info :: DSL }
619 deriving Show
620{-!
621deriving instance Binary SyntaxInfo
622!-}
624defaultSyntax = Syn [] [] [] [] id False False initDSL
626expandNS :: SyntaxInfo -> Name -> Name
627expandNS syn n@(NS _ _) = n
628expandNS syn n = case syn_namespace syn of
629 [] -> n
630 xs -> NS n xs
633--- Pretty printing declarations and terms
635instance Show PTerm where
636 show tm = showImp False tm
638instance Pretty PTerm where
639 pretty = prettyImp False
641instance Show PDecl where
642 show d = showDeclImp False d
644instance Show PClause where
645 show c = showCImp True c
647instance Show PData where
648 show d = showDImp False d
650showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
651showDeclImp t (PTy _ _ _ _ n ty) = show n ++ " : " ++ showImp t ty
652showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
653showDeclImp _ (PData _ _ _ _ d) = show d
654showDeclImp _ (PParams f ns ps) = "parameters " ++ show ns ++ "\n" ++
655 showSep "\n" (map show ps)
658showCImp :: Bool -> PClause -> String
659showCImp impl (PClause _ n l ws r w)
660 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
661 ++ " where " ++ show w
662 where
663 showWs [] = ""
664 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
665showCImp impl (PWith _ n l ws r w)
666 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
667 ++ " { " ++ show w ++ " } "
668 where
669 showWs [] = ""
670 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
673showDImp :: Bool -> PData -> String
674showDImp impl (PDatadecl n ty cons)
675 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
676 ++ showSep "\n\t| "
677 (map (\ (_, n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
679getImps :: [PArg] -> [(Name, PTerm)]
680getImps [] = []
681getImps (PImp _ _ n tm _ : xs) = (n, tm) : getImps xs
682getImps (_ : xs) = getImps xs
684getExps :: [PArg] -> [PTerm]
685getExps [] = []
686getExps (PExp _ _ tm _ : xs) = tm : getExps xs
687getExps (_ : xs) = getExps xs
689getConsts :: [PArg] -> [PTerm]
690getConsts [] = []
691getConsts (PConstraint _ _ tm _ : xs) = tm : getConsts xs
692getConsts (_ : xs) = getConsts xs
694getAll :: [PArg] -> [PTerm]
695getAll = map getTm
697prettyImp :: Bool -> PTerm -> Doc
698prettyImp impl = prettySe 10
699 where
700 prettySe p (PQuote r) =
701 if size r > breakingSize then
702 text "![" $$ pretty r <> text "]"
703 else
704 text "![" <> pretty r <> text "]"
705 prettySe p (PPatvar fc n) = pretty n
706 prettySe p (PRef fc n) =
707 if impl then
708 pretty n
709 else
710 prettyBasic n
711 where
712 prettyBasic n@(UN _) = pretty n
713 prettyBasic (MN _ s) = text s
714 prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
715 prettySe p (PLam n ty sc) =
716 bracket p 2 $
717 if size sc > breakingSize then
718 text "λ" <> pretty n <+> text "=>" $+$ pretty sc
719 else
720 text "λ" <> pretty n <+> text "=>" <+> pretty sc
721 prettySe p (PLet n ty v sc) =
722 bracket p 2 $
723 if size sc > breakingSize then
724 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
725 nest nestingSize (prettySe 10 sc)
726 else
727 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
728 prettySe 10 sc
729 prettySe p (PPi (Exp l s _) n ty sc)
730 | n `elem` allNamesIn sc || impl =
731 let open = if l then text "|" <> lparen else lparen in
732 bracket p 2 $
733 if size sc > breakingSize then
734 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
735 st <+> text "->" $+$ prettySe 10 sc
736 else
737 open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
738 st <+> text "->" <+> prettySe 10 sc
739 | otherwise =
740 bracket p 2 $
741 if size sc > breakingSize then
742 prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
743 else
744 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
745 where
746 st =
747 case s of
748 Static -> text "[static]"
749 _ -> empty
750 prettySe p (PPi (Imp l s _) n ty sc)
751 | impl =
752 let open = if l then text "|" <> lbrace else lbrace in
753 bracket p 2 $
754 if size sc > breakingSize then
755 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
756 st <+> text "->" <+> prettySe 10 sc
757 else
758 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
759 st <+> text "->" <+> prettySe 10 sc
760 | otherwise = prettySe 10 sc
761 where
762 st =
763 case s of
764 Static -> text $ "[static]"
765 _ -> empty
766 prettySe p (PPi (Constraint _ _ _) n ty sc) =
767 bracket p 2 $
768 if size sc > breakingSize then
769 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
770 else
771 prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
772 prettySe p (PPi (TacImp _ _ s _) n ty sc) =
773 bracket p 2 $
774 if size sc > breakingSize then
775 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
776 rbrace <+> text "->" $+$ prettySe 10 sc
777 else
778 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
779 rbrace <+> text "->" <+> prettySe 10 sc
780 prettySe p (PApp _ (PRef _ f) [])
781 | not impl = pretty f
782 prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
783 | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
784 let [l, r] = getExps args in
785 bracket p 1 $
786 if size r > breakingSize then
787 prettySe 1 l <+> pretty op $+$ prettySe 0 r
788 else
789 prettySe 1 l <+> pretty op <+> prettySe 0 r
790 prettySe p (PApp _ f as) =
791 let args = getExps as in
792 bracket p 1 $
793 prettySe 1 f <+>
794 if impl then
795 foldl fS empty as
796 -- foldr (<+>) empty $ map prettyArgS as
797 else
798 foldl fSe empty args
799 -- foldr (<+>) empty $ map prettyArgSe args
800 where
801 fS l r =
802 if size r > breakingSize then
803 l $+$ nest nestingSize (prettyArgS r)
804 else
805 l <+> prettyArgS r
807 fSe l r =
808 if size r > breakingSize then
809 l $+$ nest nestingSize (prettyArgSe r)
810 else
811 l <+> prettyArgSe r
812 prettySe p (PCase _ scr opts) =
813 text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
814 where
815 prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
817 sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
818 prettySe p (PHidden tm) = text "." <> prettySe 0 tm
819 prettySe p (PRefl _ _) = text "refl"
820 prettySe p (PResolveTC _) = text "resolvetc"
821 prettySe p (PTrue _) = text "()"
822 prettySe p (PFalse _) = text "_|_"
823 prettySe p (PEq _ l r) =
824 bracket p 2 $
825 if size r > breakingSize then
826 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
827 else
828 prettySe 10 l <+> text "=" <+> prettySe 10 r
829 prettySe p (PTyped l r) =
830 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
831 prettySe p (PPair _ l r) =
832 if size r > breakingSize then
833 lparen <> prettySe 10 l <> text "," $+$
834 prettySe 10 r <> rparen
835 else
836 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
837 prettySe p (PDPair _ l t r) =
838 if size r > breakingSize then
839 lparen <> prettySe 10 l <+> text "**" $+$
840 prettySe 10 r <> rparen
841 else
842 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
843 prettySe p (PAlternative a as) =
844 lparen <> text "|" <> prettyAs <> text "|" <> rparen
845 where
846 prettyAs =
847 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
848 prettySe p PSet = text "Set"
849 prettySe p (PConstant c) = pretty c
850 -- XXX: add pretty for tactics
851 prettySe p (PProof ts) =
852 text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
853 prettySe p (PTactics ts) =
854 text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
855 prettySe p (PMetavar n) = text "?" <> pretty n
856 prettySe p (PReturn f) = text "return"
857 prettySe p PImpossible = text "impossible"
858 prettySe p Placeholder = text "_"
859 prettySe p (PDoBlock _) = text "do block pretty not implemented"
860 prettySe p (PElabError s) = pretty s
862 prettySe p _ = text "test"
864 prettyArgS (PImp _ _ n tm _) = prettyArgSi (n, tm)
865 prettyArgS (PExp _ _ tm _) = prettyArgSe tm
866 prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
867 prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
869 prettyArgSe arg = prettySe 0 arg
870 prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
871 prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
872 prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
874 bracket outer inner doc
875 | inner > outer = lparen <> doc <> rparen
876 | otherwise = doc
878showImp :: Bool -> PTerm -> String
879showImp impl tm = se 10 tm where
880 se p (PQuote r) = "![" ++ show r ++ "]"
881 se p (PPatvar fc n) = show n
882 se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
883 else showbasic n
884 where showbasic n@(UN _) = show n
885 showbasic (MN _ s) = s
886 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
887 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
888 (if impl then " : " ++ se 10 ty else "") ++ " => "
889 ++ se 10 sc
890 se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
891 " in " ++ se 10 sc
892 se p (PPi (Exp l s _) n ty sc)
893 | n `elem` allNamesIn sc || impl
894 = bracket p 2 $
895 if l then "|(" else "(" ++
896 show n ++ " : " ++ se 10 ty ++
897 ") " ++ st ++
898 "-> " ++ se 10 sc
899 | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
900 where st = case s of
901 Static -> "[static] "
902 _ -> ""
903 se p (PPi (Imp l s _) n ty sc)
904 | impl = bracket p 2 $ if l then "|{" else "{" ++
905 show n ++ " : " ++ se 10 ty ++
906 "} " ++ st ++ "-> " ++ se 10 sc
907 | otherwise = se 10 sc
908 where st = case s of
909 Static -> "[static] "
910 _ -> ""
911 se p (PPi (Constraint _ _ _) n ty sc)
912 = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
913 se p (PPi (TacImp _ _ s _) n ty sc)
914 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
915 se p (PApp _ (PRef _ f) [])
916 | not impl = show f
917 se p (PApp _ (PRef _ op@(UN (f:_))) args)
918 | length (getExps args) == 2 && not impl && not (isAlpha f)
919 = let [l, r] = getExps args in
920 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
921 se p (PApp _ f as)
922 = let args = getExps as in
923 bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
924 else concatMap seArg args
925 se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
926 where sc (l, r) = se 10 l ++ " => " ++ se 10 r
927 se p (PHidden tm) = "." ++ se 0 tm
928 se p (PRefl _ t)
929 | not impl = "refl"
930 | otherwise = "refl {" ++ se 10 t ++ "}"
931 se p (PResolveTC _) = "resolvetc"
932 se p (PTrue _) = "()"
933 se p (PFalse _) = "_|_"
934 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
935 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
936 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
937 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
938 se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
939 se p PSet = "Set"
940 se p (PConstant c) = show c
941 se p (PProof ts) = "proof { " ++ show ts ++ "}"
942 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
943 se p (PMetavar n) = "?" ++ show n
944 se p (PReturn f) = "return"
945 se p PImpossible = "impossible"
946 se p Placeholder = "_"
947 se p (PDoBlock _) = "do block show not implemented"
948 se p (PElabError s) = show s
949-- se p x = "Not implemented"
951 sArg (PImp _ _ n tm _) = siArg (n, tm)
952 sArg (PExp _ _ tm _) = seArg tm
953 sArg (PConstraint _ _ tm _) = scArg tm
954 sArg (PTacImplicit _ _ n _ tm _) = stiArg (n, tm)
956 seArg arg = " " ++ se 0 arg
957 siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
958 scArg val = " {{" ++ se 10 val ++ "}}"
959 stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
961 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
962 | otherwise = str
965instance Sized PTerm where
966 size (PQuote rawTerm) = size rawTerm
967 size (PRef fc name) = size name
968 size (PLam name ty bdy) = 1 + size ty + size bdy
969 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
970 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
971 size (PTyped trm ty) = 1 + size trm + size ty
972 size (PApp fc name args) = 1 + size args
973 size (PCase fc trm bdy) = 1 + size trm + size bdy
974 size (PTrue fc) = 1
975 size (PFalse fc) = 1
976 size (PRefl fc _) = 1
977 size (PResolveTC fc) = 1
978 size (PEq fc left right) = 1 + size left + size right
979 size (PPair fc left right) = 1 + size left + size right
980 size (PDPair fs left ty right) = 1 + size left + size ty + size right
981 size (PAlternative a alts) = 1 + size alts
982 size (PHidden hidden) = size hidden
983 size PSet = 1
984 size (PConstant const) = 1 + size const
985 size Placeholder = 1
986 size (PDoBlock dos) = 1 + size dos
987 size (PIdiom fc term) = 1 + size term
988 size (PReturn fc) = 1
989 size (PMetavar name) = 1
990 size (PProof tactics) = size tactics
991 size (PElabError err) = size err
992 size PImpossible = 1
994allNamesIn :: PTerm -> [Name]
995allNamesIn tm = nub $ ni [] tm
996 where
997 ni env (PRef _ n)
998 | not (n `elem` env) = [n]
999 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1000 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1001 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1002 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1003 ni env (PHidden tm) = ni env tm
1004 ni env (PEq _ l r) = ni env l ++ ni env r
1005 ni env (PTyped l r) = ni env l ++ ni env r
1006 ni env (PPair _ l r) = ni env l ++ ni env r
1007 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1008 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1009 ni env (PAlternative a ls) = concatMap (ni env) ls
1010 ni env _ = []
1012namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1013namesIn uvars ist tm = nub $ ni [] tm
1014 where
1015 ni env (PRef _ n)
1016 | not (n `elem` env)
1017 = case lookupTy Nothing n (tt_ctxt ist) of
1018 [] -> [n]
1019 _ -> if n `elem` (map fst uvars) then [n] else []
1020 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1021 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1022 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1023 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1024 ni env (PEq _ l r) = ni env l ++ ni env r
1025 ni env (PTyped l r) = ni env l ++ ni env r
1026 ni env (PPair _ l r) = ni env l ++ ni env r
1027 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1028 ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1029 ni env (PAlternative a as) = concatMap (ni env) as
1030 ni env (PHidden tm) = ni env tm
1031 ni env _ = []