git.iko.soy/Idris-dev
on master help sign in
Lift syntax tree, main monad and pretty printing out of AbsSyntax
848a597Edwin Brady
idris.cabal+2−1
compare with master
unifiedsplit
@@ -59,7 +59,8 @@ Executable idris
59 Core.ShellParser, Core.Unify, Core.Elaborate,
59 Core.ShellParser, Core.Unify, Core.Elaborate,
60 Core.CaseTree, Core.Constraints,
60 Core.CaseTree, Core.Constraints,
61
61
62− Idris.AbsSyntax, Idris.Parser, Idris.REPL,
62+ Idris.AbsSyntax, Idris.AbsSyntaxTree,
63+ Idris.Parser, Idris.REPL,
63 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
64 Idris.REPLParser, Idris.ElabDecls, Idris.Error,
64 Idris.Delaborate, Idris.Primitives, Idris.Imports,
65 Idris.Delaborate, Idris.Primitives, Idris.Imports,
65 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
66 Idris.Compiler, Idris.Prover, Idris.ElabTerm,
src/Idris/AbsSyntax.hs+2−952
@@ -1,12 +1,13 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
2 TypeSynonymInstances, PatternGuards #-}
3
3
4−module Idris.AbsSyntax where
4+module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
5
5
6import Core.TT
6import Core.TT
7import Core.Evaluate
7import Core.Evaluate
8import Core.Elaborate hiding (Tactic(..))
8import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
9import Core.Typecheck
10+import Idris.AbsSyntaxTree
10import RTS.SC
11import RTS.SC
11
12
12import Paths_idris
13import Paths_idris
@@ -25,96 +26,6 @@ import qualified Epic.Epic as E
25
26
26import Util.Pretty
27import Util.Pretty
27
28
28−data IOption = IOption { opt_logLevel :: Int,
29− opt_typecase :: Bool,
30− opt_typeintype :: Bool,
31− opt_coverage :: Bool,
32− opt_showimp :: Bool,
33− opt_errContext :: Bool,
34− opt_repl :: Bool,
35− opt_verbose :: Bool,
36− opt_ibcsubdir :: FilePath,
37− opt_importdirs :: [FilePath]
38− }
39− deriving (Show, Eq)
40−
41−defaultOpts = IOption 0 False False True False False True True "" []
42−
43−-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
44−-- without typechecking).
45−-- This will include all the functions and data declarations, plus fixity declarations
46−-- and syntax macros.
47−
48−data IState = IState { tt_ctxt :: Context,
49− idris_constraints :: [(UConstraint, FC)],
50− idris_infixes :: [FixDecl],
51− idris_implicits :: Ctxt [PArg],
52− idris_statics :: Ctxt [Bool],
53− idris_classes :: Ctxt ClassInfo,
54− idris_dsls :: Ctxt DSL,
55− idris_optimisation :: Ctxt OptInfo,
56− idris_datatypes :: Ctxt TypeInfo,
57− idris_patdefs :: Ctxt [([Name], Term, Term)], -- not exported
58− idris_flags :: Ctxt [FnOpt],
59− idris_callgraph :: Ctxt [Name],
60− idris_calledgraph :: Ctxt [Name],
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_prims :: [(Name, ([E.Name], E.Term))],
70− idris_scprims :: Prims,
71− idris_objs :: [FilePath],
72− idris_libs :: [String],
73− idris_hdrs :: [String],
74− last_proof :: Maybe (Name, [String]),
75− errLine :: Maybe Int,
76− lastParse :: Maybe Name,
77− indent_stack :: [Int],
78− brace_stack :: [Maybe Int],
79− hide_list :: [(Name, Maybe Accessibility)],
80− default_access :: Accessibility,
81− ibc_write :: [IBCWrite],
82− compiled_so :: Maybe String
83− }
84−
85−primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
86−
87−-- information that needs writing for the current module's .ibc file
88−data IBCWrite = IBCFix FixDecl
89− | IBCImp Name
90− | IBCStatic Name
91− | IBCClass Name
92− | IBCInstance Bool Name Name
93− | IBCDSL Name
94− | IBCData Name
95− | IBCOpt Name
96− | IBCSyntax Syntax
97− | IBCKeyword String
98− | IBCImport FilePath
99− | IBCObj FilePath
100− | IBCLib String
101− | IBCHeader String
102− | IBCAccess Name Accessibility
103− | IBCTotal Name Totality
104− | IBCFlags Name [FnOpt]
105− | IBCCG Name
106− | IBCDef Name -- i.e. main context
107− deriving Show
108−
109−idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
110− emptyContext emptyContext emptyContext emptyContext
111− emptyContext emptyContext emptyContext
112− [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
113− Nothing Nothing Nothing [] [] [] Hidden [] Nothing
114−
115−-- The monad for the main REPL - reading and processing files and updating
116−-- global state (hence the IO inner monad).
117−type Idris = StateT IState (InputT IO)
118
29
119getContext :: Idris Context
30getContext :: Idris Context
120getContext = do i <- get; return (tt_ctxt i)
31getContext = do i <- get; return (tt_ctxt i)
@@ -392,867 +303,6 @@ setTypeCase t = do i <- get
392 let opt' = opts { opt_typecase = t }
303 let opt' = opts { opt_typecase = t }
393 put (i { idris_options = opt' })
304 put (i { idris_options = opt' })
394
305
395−-- Commands in the REPL
396−
397−data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
398− | Reload | Edit
399− | Compile String | Execute | ExecVal PTerm
400− | NewCompile String
401− | Metavars | Prove Name | AddProof | Universes
402− | TTShell
403− | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
404− | Info Name | DebugInfo Name
405− | Search PTerm
406− | SetOpt Opt | UnsetOpt Opt
407− | NOP
408−
409−data Opt = Filename String
410− | Ver
411− | Usage
412− | ShowLibs
413− | ShowIncs
414− | NoPrelude
415− | NoREPL
416− | OLogging Int
417− | Output String
418− | NewOutput String
419− | TypeCase
420− | TypeInType
421− | NoCoverage
422− | ErrContext
423− | ShowImpl
424− | Verbose
425− | IBCSubDir String
426− | ImportDir String
427− | BCAsm String
428− deriving Eq
429−
430−
431−-- Parsed declarations
432−
433−data Fixity = Infixl { prec :: Int }
434− | Infixr { prec :: Int }
435− | InfixN { prec :: Int }
436− | PrefixN { prec :: Int }
437− deriving Eq
438−{-!
439−deriving instance Binary Fixity
440−!-}
441−
442−instance Show Fixity where
443− show (Infixl i) = "infixl " ++ show i
444− show (Infixr i) = "infixr " ++ show i
445− show (InfixN i) = "infix " ++ show i
446− show (PrefixN i) = "prefix " ++ show i
447−
448−data FixDecl = Fix Fixity String
449− deriving (Show, Eq)
450−{-!
451−deriving instance Binary FixDecl
452−!-}
453−
454−instance Ord FixDecl where
455− compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
456−
457−
458−data Static = Static | Dynamic
459− deriving (Show, Eq)
460−{-!
461−deriving instance Binary Static
462−!-}
463−
464−-- Mark bindings with their explicitness, and laziness
465−data Plicity = Imp { plazy :: Bool,
466− pstatic :: Static }
467− | Exp { plazy :: Bool,
468− pstatic :: Static }
469− | Constraint { plazy :: Bool,
470− pstatic :: Static }
471− | TacImp { plazy :: Bool,
472− pstatic :: Static,
473− pscript :: PTerm }
474− deriving (Show, Eq)
475−
476−{-!
477−deriving instance Binary Plicity
478−!-}
479−
480−impl = Imp False Dynamic
481−expl = Exp False Dynamic
482−constraint = Constraint False Dynamic
483−tacimpl = TacImp False Dynamic
484−
485−data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
486− | CExport String -- export, with a C name
487− | Specialise [Name] -- specialise it, freeze these names
488− deriving (Show, Eq)
489−{-!
490−deriving instance Binary FnOpt
491−!-}
492−
493−type FnOpts = [FnOpt]
494−
495−inlinable :: FnOpts -> Bool
496−inlinable = elem Inlinable
497−
498−data PDecl' t = PFix FC Fixity [String] -- fixity declaration
499− | PTy SyntaxInfo FC FnOpts Name t -- type declaration
500− | PClauses FC FnOpts Name [PClause' t] -- pattern clause
501− | PData SyntaxInfo FC (PData' t) -- data declaration
502− | PParams FC [(Name, t)] [PDecl' t] -- params block
503− | PNamespace String [PDecl' t] -- new namespace
504− | PRecord SyntaxInfo FC Name t Name t -- record declaration
505− | PClass SyntaxInfo FC
506− [t] -- constraints
507− Name
508− [(Name, t)] -- parameters
509− [PDecl' t] -- declarations
510− | PInstance SyntaxInfo FC [t] -- constraints
511− Name -- class
512− [t] -- parameters
513− t -- full instance type
514− (Maybe Name) -- explicit name
515− [PDecl' t]
516− | PDSL Name (DSL' t)
517− | PSyntax FC Syntax
518− | PDirective (Idris ())
519− deriving Functor
520−{-!
521−deriving instance Binary PDecl'
522−!-}
523−
524−data PClause' t = PClause FC Name t [t] t [PDecl' t]
525− | PWith FC Name t [t] t [PDecl' t]
526− | PClauseR FC [t] t [PDecl' t]
527− | PWithR FC [t] t [PDecl' t]
528− deriving Functor
529−{-!
530−deriving instance Binary PClause'
531−!-}
532−
533−data PData' t = PDatadecl { d_name :: Name,
534− d_tcon :: t,
535− d_cons :: [(Name, t, FC)] }
536− deriving Functor
537−{-!
538−deriving instance Binary PData'
539−!-}
540−
541−-- Handy to get a free function for applying PTerm -> PTerm functions
542−-- across a program, by deriving Functor
543−
544−type PDecl = PDecl' PTerm
545−type PData = PData' PTerm
546−type PClause = PClause' PTerm
547−
548−-- get all the names declared in a decl
549−
550−declared :: PDecl -> [Name]
551−declared (PFix _ _ _) = []
552−declared (PTy _ _ _ n t) = [n]
553−declared (PClauses _ _ n _) = [] -- not a declaration
554−declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
555− where fstt (a, _, _) = a
556−declared (PParams _ _ ds) = concatMap declared ds
557−declared (PNamespace _ ds) = concatMap declared ds
558−-- declared (PImport _) = []
559−
560−defined :: PDecl -> [Name]
561−defined (PFix _ _ _) = []
562−defined (PTy _ _ _ n t) = []
563−defined (PClauses _ _ n _) = [n] -- not a declaration
564−defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
565− where fstt (a, _, _) = a
566−defined (PParams _ _ ds) = concatMap defined ds
567−defined (PNamespace _ ds) = concatMap defined ds
568−-- declared (PImport _) = []
569−
570−updateN :: [(Name, Name)] -> Name -> Name
571−updateN ns n | Just n' <- lookup n ns = n'
572−updateN _ n = n
573−
574−updateNs :: [(Name, Name)] -> PTerm -> PTerm
575−updateNs [] t = t
576−updateNs ns t = mapPT updateRef t
577− where updateRef (PRef fc f) = PRef fc (updateN ns f)
578− updateRef t = t
579−
580−-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
581−-- updateDNs [] t = t
582−-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
583−-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
584−-- where updateCNs ns (PClause n l ts r ds)
585−-- = PClause (updateN ns n) (fmap (updateNs ns) l)
586−-- (map (fmap (updateNs ns)) ts)
587−-- (fmap (updateNs ns) r)
588−-- (map (updateDNs ns) ds)
589−-- updateDNs ns c = c
590−
591−-- High level language terms
592−
593−data PTerm = PQuote Raw
594− | PRef FC Name
595− | PLam Name PTerm PTerm
596− | PPi Plicity Name PTerm PTerm
597− | PLet Name PTerm PTerm PTerm
598− | PTyped PTerm PTerm -- term with explicit type
599− | PApp FC PTerm [PArg]
600− | PCase FC PTerm [(PTerm, PTerm)]
601− | PTrue FC
602− | PFalse FC
603− | PRefl FC
604− | PResolveTC FC
605− | PEq FC PTerm PTerm
606− | PPair FC PTerm PTerm
607− | PDPair FC PTerm PTerm PTerm
608− | PAlternative Bool [PTerm] -- True if only one may work
609− | PHidden PTerm -- irrelevant or hidden pattern
610− | PSet
611− | PConstant Const
612− | Placeholder
613− | PDoBlock [PDo]
614− | PIdiom FC PTerm
615− | PReturn FC
616− | PMetavar Name
617− | PProof [PTactic]
618− | PTactics [PTactic] -- as PProof, but no auto solving
619− | PElabError Err -- error to report on elaboration
620− | PImpossible -- special case for declaring when an LHS can't typecheck
621− deriving Eq
622−{-!
623−deriving instance Binary PTerm
624−!-}
625−
626−mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
627−mapPT f t = f (mpt t) where
628− mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
629− mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
630− mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
631− mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
632− mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
633− mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
634− mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
635− mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
636− mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
637− mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
638− mpt (PHidden t) = PHidden (mapPT f t)
639− mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
640− mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
641− mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
642− mpt x = x
643−
644−
645−data PTactic' t = Intro [Name] | Intros | Focus Name
646− | Refine Name [Bool] | Rewrite t | LetTac Name t
647− | Exact t | Compute | Trivial
648− | Solve
649− | Attack
650− | ProofState | ProofTerm | Undo
651− | Try (PTactic' t) (PTactic' t)
652− | TSeq (PTactic' t) (PTactic' t)
653− | Qed | Abandon
654− deriving (Show, Eq, Functor)
655−{-!
656−deriving instance Binary PTactic'
657−!-}
658−
659−instance Sized a => Sized (PTactic' a) where
660− size (Intro nms) = 1 + size nms
661− size Intros = 1
662− size (Focus nm) = 1 + size nm
663− size (Refine nm bs) = 1 + size nm + length bs
664− size (Rewrite t) = 1 + size t
665− size (LetTac nm t) = 1 + size nm + size t
666− size (Exact t) = 1 + size t
667− size Compute = 1
668− size Trivial = 1
669− size Solve = 1
670− size Attack = 1
671− size ProofState = 1
672− size ProofTerm = 1
673− size Undo = 1
674− size (Try l r) = 1 + size l + size r
675− size (TSeq l r) = 1 + size l + size r
676− size Qed = 1
677− size Abandon = 1
678−
679−type PTactic = PTactic' PTerm
680−
681−data PDo' t = DoExp FC t
682− | DoBind FC Name t
683− | DoBindP FC t t
684− | DoLet FC Name t t
685− | DoLetP FC t t
686− deriving (Eq, Functor)
687−{-!
688−deriving instance Binary PDo'
689−!-}
690−
691−instance Sized a => Sized (PDo' a) where
692− size (DoExp fc t) = 1 + size fc + size t
693− size (DoBind fc nm t) = 1 + size fc + size nm + size t
694− size (DoBindP fc l r) = 1 + size fc + size l + size r
695− size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
696− size (DoLetP fc l r) = 1 + size fc + size l + size r
697−
698−type PDo = PDo' PTerm
699−
700−-- The priority gives a hint as to elaboration order. Best to elaborate
701−-- things early which will help give a more concrete type to other
702−-- variables, e.g. a before (interpTy a).
703−
704−data PArg' t = PImp { priority :: Int,
705− lazyarg :: Bool, pname :: Name, getTm :: t }
706− | PExp { priority :: Int,
707− lazyarg :: Bool, getTm :: t }
708− | PConstraint { priority :: Int,
709− lazyarg :: Bool, getTm :: t }
710− | PTacImplicit { priority :: Int,
711− lazyarg :: Bool, pname :: Name,
712− getScript :: t,
713− getTm :: t }
714− deriving (Show, Eq, Functor)
715−
716−instance Sized a => Sized (PArg' a) where
717− size (PImp p l nm trm) = 1 + size nm + size trm
718− size (PExp p l trm) = 1 + size trm
719− size (PConstraint p l trm) = 1 + size trm
720− size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
721−
722−{-!
723−deriving instance Binary PArg'
724−!-}
725−
726−pimp = PImp 0 True
727−pexp = PExp 0 False
728−pconst = PConstraint 0 False
729−ptacimp = PTacImplicit 0 True
730−
731−type PArg = PArg' PTerm
732−
733−-- Type class data
734−
735−data ClassInfo = CI { instanceName :: Name,
736− class_methods :: [(Name, (FnOpts, PTerm))],
737− class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
738− class_params :: [Name],
739− class_instances :: [Name] }
740− deriving Show
741−{-!
742−deriving instance Binary ClassInfo
743−!-}
744−
745−data OptInfo = Optimise { collapsible :: Bool,
746− forceable :: [Int], -- argument positions
747− recursive :: [Int] }
748− deriving Show
749−{-!
750−deriving instance Binary OptInfo
751−!-}
752−
753−
754−data TypeInfo = TI { con_names :: [Name] }
755− deriving Show
756−{-!
757−deriving instance Binary TypeInfo
758−!-}
759−
760−-- Syntactic sugar info
761−
762−data DSL' t = DSL { dsl_bind :: t,
763− dsl_return :: t,
764− dsl_apply :: t,
765− dsl_pure :: t,
766− dsl_var :: Maybe t,
767− index_first :: Maybe t,
768− index_next :: Maybe t,
769− dsl_lambda :: Maybe t,
770− dsl_let :: Maybe t
771− }
772− deriving (Show, Functor)
773−{-!
774−deriving instance Binary DSL'
775−!-}
776−
777−type DSL = DSL' PTerm
778−
779−data SynContext = PatternSyntax | TermSyntax | AnySyntax
780− deriving Show
781−{-!
782−deriving instance Binary SynContext
783−!-}
784−
785−data Syntax = Rule [SSymbol] PTerm SynContext
786− deriving Show
787−{-!
788−deriving instance Binary Syntax
789−!-}
790−
791−data SSymbol = Keyword Name
792− | Symbol String
793− | Binding Name
794− | Expr Name
795− | SimpleExpr Name
796− deriving Show
797−{-!
798−deriving instance Binary SSymbol
799−!-}
800−
801−initDSL = DSL (PRef f (UN ">>="))
802− (PRef f (UN "return"))
803− (PRef f (UN "<$>"))
804− (PRef f (UN "pure"))
805− Nothing
806− Nothing
807− Nothing
808− Nothing
809− Nothing
810− where f = FC "(builtin)" 0
811−
812−data SyntaxInfo = Syn { using :: [(Name, PTerm)],
813− syn_params :: [(Name, PTerm)],
814− syn_namespace :: [String],
815− no_imp :: [Name],
816− decoration :: Name -> Name,
817− inPattern :: Bool,
818− implicitAllowed :: Bool,
819− dsl_info :: DSL }
820− deriving Show
821−{-!
822−deriving instance Binary SyntaxInfo
823−!-}
824−
825−defaultSyntax = Syn [] [] [] [] id False False initDSL
826−
827−expandNS :: SyntaxInfo -> Name -> Name
828−expandNS syn n@(NS _ _) = n
829−expandNS syn n = case syn_namespace syn of
830− [] -> n
831− xs -> NS n xs
832−
833−
834−--- Pretty printing declarations and terms
835−
836−instance Show PTerm where
837− show tm = showImp False tm
838−
839−instance Pretty PTerm where
840− pretty = prettyImp False
841−
842−instance Show PDecl where
843− show d = showDeclImp False d
844−
845−instance Show PClause where
846− show c = showCImp True c
847−
848−instance Show PData where
849− show d = showDImp False d
850−
851−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
852−showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
853−showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
854−showDeclImp _ (PData _ _ d) = show d
855−
856−showCImp :: Bool -> PClause -> String
857−showCImp impl (PClause _ n l ws r w)
858− = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
859− ++ " where " ++ show w
860− where
861− showWs [] = ""
862− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
863−showCImp impl (PWith _ n l ws r w)
864− = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
865− ++ " { " ++ show w ++ " } "
866− where
867− showWs [] = ""
868− showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
869−
870−
871−showDImp :: Bool -> PData -> String
872−showDImp impl (PDatadecl n ty cons)
873− = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
874− ++ showSep "\n\t| "
875− (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
876−
877−getImps :: [PArg] -> [(Name, PTerm)]
878−getImps [] = []
879−getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
880−getImps (_ : xs) = getImps xs
881−
882−getExps :: [PArg] -> [PTerm]
883−getExps [] = []
884−getExps (PExp _ _ tm : xs) = tm : getExps xs
885−getExps (_ : xs) = getExps xs
886−
887−getConsts :: [PArg] -> [PTerm]
888−getConsts [] = []
889−getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
890−getConsts (_ : xs) = getConsts xs
891−
892−getAll :: [PArg] -> [PTerm]
893−getAll = map getTm
894−
895−prettyImp :: Bool -> PTerm -> Doc
896−prettyImp impl = prettySe 10
897− where
898− prettySe p (PQuote r) =
899− if size r > breakingSize then
900− text "![" $$ pretty r <> text "]"
901− else
902− text "![" <> pretty r <> text "]"
903− prettySe p (PRef fc n) =
904− if impl then
905− pretty n
906− else
907− prettyBasic n
908− where
909− prettyBasic n@(UN _) = pretty n
910− prettyBasic (MN _ s) = text s
911− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
912− prettySe p (PLam n ty sc) =
913− bracket p 2 $
914− if size sc > breakingSize then
915− text "λ" <> pretty n <+> text "=>" $+$ pretty sc
916− else
917− text "λ" <> pretty n <+> text "=>" <+> pretty sc
918− prettySe p (PLet n ty v sc) =
919− bracket p 2 $
920− if size sc > breakingSize then
921− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
922− nest nestingSize (prettySe 10 sc)
923− else
924− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
925− prettySe 10 sc
926− prettySe p (PPi (Exp l s) n ty sc)
927− | n `elem` allNamesIn sc || impl =
928− let open = if l then text "|" <> lparen else lparen in
929− bracket p 2 $
930− if size sc > breakingSize then
931− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
932− st <+> text "->" $+$ prettySe 10 sc
933− else
934− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
935− st <+> text "->" <+> prettySe 10 sc
936− | otherwise =
937− bracket p 2 $
938− if size sc > breakingSize then
939− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
940− else
941− prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
942− where
943− st =
944− case s of
945− Static -> text "[static]"
946− _ -> empty
947− prettySe p (PPi (Imp l s) n ty sc)
948− | impl =
949− let open = if l then text "|" <> lbrace else lbrace in
950− bracket p 2 $
951− if size sc > breakingSize then
952− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
953− st <+> text "->" <+> prettySe 10 sc
954− else
955− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
956− st <+> text "->" <+> prettySe 10 sc
957− | otherwise = prettySe 10 sc
958− where
959− st =
960− case s of
961− Static -> text $ "[static]"
962− _ -> empty
963− prettySe p (PPi (Constraint _ _) n ty sc) =
964− bracket p 2 $
965− if size sc > breakingSize then
966− prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
967− else
968− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
969− prettySe p (PPi (TacImp _ _ s) n ty sc) =
970− bracket p 2 $
971− if size sc > breakingSize then
972− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
973− rbrace <+> text "->" $+$ prettySe 10 sc
974− else
975− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
976− rbrace <+> text "->" <+> prettySe 10 sc
977− prettySe p (PApp _ (PRef _ f) [])
978− | not impl = pretty f
979− prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
980− | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
981− let [l, r] = getExps args in
982− bracket p 1 $
983− if size r > breakingSize then
984− prettySe 1 l <+> pretty op $+$ prettySe 0 r
985− else
986− prettySe 1 l <+> pretty op <+> prettySe 0 r
987− prettySe p (PApp _ f as) =
988− let args = getExps as in
989− bracket p 1 $
990− prettySe 1 f <+>
991− if impl then
992− foldl fS empty as
993− -- foldr (<+>) empty $ map prettyArgS as
994− else
995− foldl fSe empty args
996− -- foldr (<+>) empty $ map prettyArgSe args
997− where
998− fS l r =
999− if size r > breakingSize then
1000− l $+$ nest nestingSize (prettyArgS r)
1001− else
1002− l <+> prettyArgS r
1003−
1004− fSe l r =
1005− if size r > breakingSize then
1006− l $+$ nest nestingSize (prettyArgSe r)
1007− else
1008− l <+> prettyArgSe r
1009− prettySe p (PCase _ scr opts) =
1010− text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
1011− where
1012− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
1013−
1014− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
1015− prettySe p (PHidden tm) = text "." <> prettySe 0 tm
1016− prettySe p (PRefl _) = text "refl"
1017− prettySe p (PResolveTC _) = text "resolvetc"
1018− prettySe p (PTrue _) = text "()"
1019− prettySe p (PFalse _) = text "_|_"
1020− prettySe p (PEq _ l r) =
1021− bracket p 2 $
1022− if size r > breakingSize then
1023− prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
1024− else
1025− prettySe 10 l <+> text "=" <+> prettySe 10 r
1026− prettySe p (PTyped l r) =
1027− lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
1028− prettySe p (PPair _ l r) =
1029− if size r > breakingSize then
1030− lparen <> prettySe 10 l <> text "," $+$
1031− prettySe 10 r <> rparen
1032− else
1033− lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
1034− prettySe p (PDPair _ l t r) =
1035− if size r > breakingSize then
1036− lparen <> prettySe 10 l <+> text "**" $+$
1037− prettySe 10 r <> rparen
1038− else
1039− lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
1040− prettySe p (PAlternative a as) =
1041− lparen <> text "|" <> prettyAs <> text "|" <> rparen
1042− where
1043− prettyAs =
1044− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
1045− prettySe p PSet = text "Set"
1046− prettySe p (PConstant c) = pretty c
1047− -- XXX: add pretty for tactics
1048− prettySe p (PProof ts) =
1049− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1050− prettySe p (PTactics ts) =
1051− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1052− prettySe p (PMetavar n) = text "?" <> pretty n
1053− prettySe p (PReturn f) = text "return"
1054− prettySe p PImpossible = text "impossible"
1055− prettySe p Placeholder = text "_"
1056− prettySe p (PDoBlock _) = text "do block pretty not implemented"
1057− prettySe p (PElabError s) = pretty s
1058−
1059− prettySe p _ = text "test"
1060−
1061− prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
1062− prettyArgS (PExp _ _ tm) = prettyArgSe tm
1063− prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
1064− prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
1065−
1066− prettyArgSe arg = prettySe 0 arg
1067− prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1068− prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1069− prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1070−
1071− bracket outer inner doc
1072− | inner > outer = lparen <> doc <> rparen
1073− | otherwise = doc
1074−
1075−showImp :: Bool -> PTerm -> String
1076−showImp impl tm = se 10 tm where
1077− se p (PQuote r) = "![" ++ show r ++ "]"
1078− se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
1079− else showbasic n
1080− where showbasic n@(UN _) = show n
1081− showbasic (MN _ s) = s
1082− showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
1083− se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
1084− (if impl then " : " ++ se 10 ty else "") ++ " => "
1085− ++ se 10 sc
1086− se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
1087− " in " ++ se 10 sc
1088− se p (PPi (Exp l s) n ty sc)
1089− | n `elem` allNamesIn sc || impl
1090− = bracket p 2 $
1091− if l then "|(" else "(" ++
1092− show n ++ " : " ++ se 10 ty ++
1093− ") " ++ st ++
1094− "-> " ++ se 10 sc
1095− | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
1096− where st = case s of
1097− Static -> "[static] "
1098− _ -> ""
1099− se p (PPi (Imp l s) n ty sc)
1100− | impl = bracket p 2 $ if l then "|{" else "{" ++
1101− show n ++ " : " ++ se 10 ty ++
1102− "} " ++ st ++ "-> " ++ se 10 sc
1103− | otherwise = se 10 sc
1104− where st = case s of
1105− Static -> "[static] "
1106− _ -> ""
1107− se p (PPi (Constraint _ _) n ty sc)
1108− = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
1109− se p (PPi (TacImp _ _ s) n ty sc)
1110− = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1111− se p (PApp _ (PRef _ f) [])
1112− | not impl = show f
1113− se p (PApp _ (PRef _ op@(UN (f:_))) args)
1114− | length (getExps args) == 2 && not impl && not (isAlpha f)
1115− = let [l, r] = getExps args in
1116− bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
1117− se p (PApp _ f as)
1118− = let args = getExps as in
1119− bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
1120− else concatMap seArg args
1121− se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
1122− where sc (l, r) = se 10 l ++ " => " ++ se 10 r
1123− se p (PHidden tm) = "." ++ se 0 tm
1124− se p (PRefl _) = "refl"
1125− se p (PResolveTC _) = "resolvetc"
1126− se p (PTrue _) = "()"
1127− se p (PFalse _) = "_|_"
1128− se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
1129− se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
1130− se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
1131− se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
1132− se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
1133− se p PSet = "Set"
1134− se p (PConstant c) = show c
1135− se p (PProof ts) = "proof { " ++ show ts ++ "}"
1136− se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
1137− se p (PMetavar n) = "?" ++ show n
1138− se p (PReturn f) = "return"
1139− se p PImpossible = "impossible"
1140− se p Placeholder = "_"
1141− se p (PDoBlock _) = "do block show not implemented"
1142− se p (PElabError s) = show s
1143−-- se p x = "Not implemented"
1144−
1145− sArg (PImp _ _ n tm) = siArg (n, tm)
1146− sArg (PExp _ _ tm) = seArg tm
1147− sArg (PConstraint _ _ tm) = scArg tm
1148− sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
1149−
1150− seArg arg = " " ++ se 0 arg
1151− siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
1152− scArg val = " {{" ++ se 10 val ++ "}}"
1153− stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
1154−
1155− bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1156− | otherwise = str
1157−
1158−{-
1159− PQuote Raw
1160− | PRef FC Name
1161− | PLam Name PTerm PTerm
1162− | PPi Plicity Name PTerm PTerm
1163− | PLet Name PTerm PTerm PTerm
1164− | PTyped PTerm PTerm -- term with explicit type
1165− | PApp FC PTerm [PArg]
1166− | PCase FC PTerm [(PTerm, PTerm)]
1167− | PTrue FC
1168− | PFalse FC
1169− | PRefl FC
1170− | PResolveTC FC
1171− | PEq FC PTerm PTerm
1172− | PPair FC PTerm PTerm
1173− | PDPair FC PTerm PTerm PTerm
1174− | PAlternative [PTerm]
1175− | PHidden PTerm -- irrelevant or hidden pattern
1176− | PSet
1177− | PConstant Const
1178− | Placeholder
1179− | PDoBlock [PDo]
1180− | PIdiom FC PTerm
1181− | PReturn FC
1182− | PMetavar Name
1183− | PProof [PTactic]
1184− | PTactics [PTactic] -- as PProof, but no auto solving
1185− | PElabError Err -- error to report on elaboration
1186− | PImpossible -- special case for declaring when an LHS can't typecheck
1187−-}
1188−
1189−instance Sized PTerm where
1190− size (PQuote rawTerm) = size rawTerm
1191− size (PRef fc name) = size name
1192− size (PLam name ty bdy) = 1 + size ty + size bdy
1193− size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1194− size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1195− size (PTyped trm ty) = 1 + size trm + size ty
1196− size (PApp fc name args) = 1 + size args
1197− size (PCase fc trm bdy) = 1 + size trm + size bdy
1198− size (PTrue fc) = 1
1199− size (PFalse fc) = 1
1200− size (PRefl fc) = 1
1201− size (PResolveTC fc) = 1
1202− size (PEq fc left right) = 1 + size left + size right
1203− size (PPair fc left right) = 1 + size left + size right
1204− size (PDPair fs left ty right) = 1 + size left + size ty + size right
1205− size (PAlternative a alts) = 1 + size alts
1206− size (PHidden hidden) = size hidden
1207− size PSet = 1
1208− size (PConstant const) = 1 + size const
1209− size Placeholder = 1
1210− size (PDoBlock dos) = 1 + size dos
1211− size (PIdiom fc term) = 1 + size term
1212− size (PReturn fc) = 1
1213− size (PMetavar name) = 1
1214− size (PProof tactics) = size tactics
1215− size (PElabError err) = size err
1216− size PImpossible = 1
1217−
1218−allNamesIn :: PTerm -> [Name]
1219−allNamesIn tm = nub $ ni [] tm
1220− where
1221− ni env (PRef _ n)
1222− | not (n `elem` env) = [n]
1223− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1224− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1225− ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1226− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1227− ni env (PHidden tm) = ni env tm
1228− ni env (PEq _ l r) = ni env l ++ ni env r
1229− ni env (PTyped l r) = ni env l ++ ni env r
1230− ni env (PPair _ l r) = ni env l ++ ni env r
1231− ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1232− ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1233− ni env (PAlternative a ls) = concatMap (ni env) ls
1234− ni env _ = []
1235−
1236−namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1237−namesIn uvars ist tm = nub $ ni [] tm
1238− where
1239− ni env (PRef _ n)
1240− | not (n `elem` env)
1241− = case lookupTy Nothing n (tt_ctxt ist) of
1242− [] -> [n]
1243− _ -> if n `elem` (map fst uvars) then [n] else []
1244− ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1245− ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1246− ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1247− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
1248− ni env (PEq _ l r) = ni env l ++ ni env r
1249− ni env (PTyped l r) = ni env l ++ ni env r
1250− ni env (PPair _ l r) = ni env l ++ ni env r
1251− ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1252− ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
1253− ni env (PAlternative a as) = concatMap (ni env) as
1254− ni env (PHidden tm) = ni env tm
1255− ni env _ = []
1256
306
1257-- For inferring types of things
307-- For inferring types of things
1258
308
src/Idris/AbsSyntaxTree.hsnew file+978
@@ -0,0 +1,978 @@
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2+ TypeSynonymInstances, PatternGuards #-}
3+
4+module Idris.AbsSyntaxTree where
5+
6+import Core.TT
7+import Core.Evaluate
8+import Core.Elaborate hiding (Tactic(..))
9+import Core.Typecheck
10+import RTS.SC
11+import Util.Pretty
12+
13+import Paths_idris
14+
15+import System.Console.Haskeline
16+
17+import Control.Monad.State
18+
19+import Data.List
20+import Data.Char
21+import Data.Either
22+
23+import Debug.Trace
24+
25+import qualified Epic.Epic as E
26+
27+data IOption = IOption { opt_logLevel :: Int,
28+ opt_typecase :: Bool,
29+ opt_typeintype :: Bool,
30+ opt_coverage :: Bool,
31+ opt_showimp :: Bool,
32+ opt_errContext :: Bool,
33+ opt_repl :: Bool,
34+ opt_verbose :: Bool,
35+ opt_ibcsubdir :: FilePath,
36+ opt_importdirs :: [FilePath]
37+ }
38+ deriving (Show, Eq)
39+
40+defaultOpts = IOption 0 False False True False False True True "" []
41+
42+-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
43+-- without typechecking).
44+-- This will include all the functions and data declarations, plus fixity declarations
45+-- and syntax macros.
46+
47+data IState = IState { 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 [Name],
59+ idris_calledgraph :: Ctxt [Name],
60+ idris_totcheck :: [(FC, Name)],
61+ idris_log :: String,
62+ idris_options :: IOption,
63+ idris_name :: Int,
64+ idris_metavars :: [Name],
65+ syntax_rules :: [Syntax],
66+ syntax_keywords :: [String],
67+ imported :: [FilePath],
68+ idris_prims :: [(Name, ([E.Name], E.Term))],
69+ idris_scprims :: Prims,
70+ idris_objs :: [FilePath],
71+ idris_libs :: [String],
72+ idris_hdrs :: [String],
73+ last_proof :: Maybe (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+ ibc_write :: [IBCWrite],
81+ compiled_so :: Maybe String
82+ }
83+
84+primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
85+
86+-- information that needs writing for the current module's .ibc file
87+data IBCWrite = IBCFix FixDecl
88+ | IBCImp Name
89+ | IBCStatic Name
90+ | IBCClass Name
91+ | IBCInstance Bool Name Name
92+ | IBCDSL Name
93+ | IBCData Name
94+ | IBCOpt Name
95+ | IBCSyntax Syntax
96+ | IBCKeyword String
97+ | IBCImport FilePath
98+ | IBCObj FilePath
99+ | IBCLib String
100+ | IBCHeader String
101+ | IBCAccess Name Accessibility
102+ | IBCTotal Name Totality
103+ | IBCFlags Name [FnOpt]
104+ | IBCCG Name
105+ | IBCDef Name -- i.e. main context
106+ deriving Show
107+
108+idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
109+ emptyContext emptyContext emptyContext emptyContext
110+ emptyContext emptyContext emptyContext
111+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []
112+ Nothing Nothing Nothing [] [] [] Hidden [] Nothing
113+
114+-- The monad for the main REPL - reading and processing files and updating
115+-- global state (hence the IO inner monad).
116+type Idris = StateT IState (InputT IO)
117+
118+-- Commands in the REPL
119+
120+data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name
121+ | Reload | Edit
122+ | Compile String | Execute | ExecVal PTerm
123+ | NewCompile String
124+ | Metavars | Prove Name | AddProof | Universes
125+ | TTShell
126+ | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name
127+ | Info Name | DebugInfo Name
128+ | Search PTerm
129+ | SetOpt Opt | UnsetOpt Opt
130+ | NOP
131+
132+data Opt = Filename String
133+ | Ver
134+ | Usage
135+ | ShowLibs
136+ | ShowIncs
137+ | NoPrelude
138+ | NoREPL
139+ | OLogging Int
140+ | Output String
141+ | NewOutput String
142+ | TypeCase
143+ | TypeInType
144+ | NoCoverage
145+ | ErrContext
146+ | ShowImpl
147+ | Verbose
148+ | IBCSubDir String
149+ | ImportDir String
150+ | BCAsm String
151+ deriving Eq
152+
153+
154+-- Parsed declarations
155+
156+data Fixity = Infixl { prec :: Int }
157+ | Infixr { prec :: Int }
158+ | InfixN { prec :: Int }
159+ | PrefixN { prec :: Int }
160+ deriving Eq
161+{-!
162+deriving instance Binary Fixity
163+!-}
164+
165+instance Show Fixity where
166+ show (Infixl i) = "infixl " ++ show i
167+ show (Infixr i) = "infixr " ++ show i
168+ show (InfixN i) = "infix " ++ show i
169+ show (PrefixN i) = "prefix " ++ show i
170+
171+data FixDecl = Fix Fixity String
172+ deriving (Show, Eq)
173+{-!
174+deriving instance Binary FixDecl
175+!-}
176+
177+instance Ord FixDecl where
178+ compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
179+
180+
181+data Static = Static | Dynamic
182+ deriving (Show, Eq)
183+{-!
184+deriving instance Binary Static
185+!-}
186+
187+-- Mark bindings with their explicitness, and laziness
188+data Plicity = Imp { plazy :: Bool,
189+ pstatic :: Static }
190+ | Exp { plazy :: Bool,
191+ pstatic :: Static }
192+ | Constraint { plazy :: Bool,
193+ pstatic :: Static }
194+ | TacImp { plazy :: Bool,
195+ pstatic :: Static,
196+ pscript :: PTerm }
197+ deriving (Show, Eq)
198+
199+{-!
200+deriving instance Binary Plicity
201+!-}
202+
203+impl = Imp False Dynamic
204+expl = Exp False Dynamic
205+constraint = Constraint False Dynamic
206+tacimpl = TacImp False Dynamic
207+
208+data FnOpt = Inlinable | TotalFn | AssertTotal | TCGen
209+ | CExport String -- export, with a C name
210+ | Specialise [Name] -- specialise it, freeze these names
211+ deriving (Show, Eq)
212+{-!
213+deriving instance Binary FnOpt
214+!-}
215+
216+type FnOpts = [FnOpt]
217+
218+inlinable :: FnOpts -> Bool
219+inlinable = elem Inlinable
220+
221+data PDecl' t = PFix FC Fixity [String] -- fixity declaration
222+ | PTy SyntaxInfo FC FnOpts Name t -- type declaration
223+ | PClauses FC FnOpts Name [PClause' t] -- pattern clause
224+ | PData SyntaxInfo FC (PData' t) -- data declaration
225+ | PParams FC [(Name, t)] [PDecl' t] -- params block
226+ | PNamespace String [PDecl' t] -- new namespace
227+ | PRecord SyntaxInfo FC Name t Name t -- record declaration
228+ | PClass SyntaxInfo FC
229+ [t] -- constraints
230+ Name
231+ [(Name, t)] -- parameters
232+ [PDecl' t] -- declarations
233+ | PInstance SyntaxInfo FC [t] -- constraints
234+ Name -- class
235+ [t] -- parameters
236+ t -- full instance type
237+ (Maybe Name) -- explicit name
238+ [PDecl' t]
239+ | PDSL Name (DSL' t)
240+ | PSyntax FC Syntax
241+ | PDirective (Idris ())
242+ deriving Functor
243+{-!
244+deriving instance Binary PDecl'
245+!-}
246+
247+data PClause' t = PClause FC Name t [t] t [PDecl' t]
248+ | PWith FC Name t [t] t [PDecl' t]
249+ | PClauseR FC [t] t [PDecl' t]
250+ | PWithR FC [t] t [PDecl' t]
251+ deriving Functor
252+{-!
253+deriving instance Binary PClause'
254+!-}
255+
256+data PData' t = PDatadecl { d_name :: Name,
257+ d_tcon :: t,
258+ d_cons :: [(Name, t, FC)] }
259+ deriving Functor
260+{-!
261+deriving instance Binary PData'
262+!-}
263+
264+-- Handy to get a free function for applying PTerm -> PTerm functions
265+-- across a program, by deriving Functor
266+
267+type PDecl = PDecl' PTerm
268+type PData = PData' PTerm
269+type PClause = PClause' PTerm
270+
271+-- get all the names declared in a decl
272+
273+declared :: PDecl -> [Name]
274+declared (PFix _ _ _) = []
275+declared (PTy _ _ _ n t) = [n]
276+declared (PClauses _ _ n _) = [] -- not a declaration
277+declared (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
278+ where fstt (a, _, _) = a
279+declared (PParams _ _ ds) = concatMap declared ds
280+declared (PNamespace _ ds) = concatMap declared ds
281+-- declared (PImport _) = []
282+
283+defined :: PDecl -> [Name]
284+defined (PFix _ _ _) = []
285+defined (PTy _ _ _ n t) = []
286+defined (PClauses _ _ n _) = [n] -- not a declaration
287+defined (PData _ _ (PDatadecl n _ ts)) = n : map fstt ts
288+ where fstt (a, _, _) = a
289+defined (PParams _ _ ds) = concatMap defined ds
290+defined (PNamespace _ ds) = concatMap defined ds
291+-- declared (PImport _) = []
292+
293+updateN :: [(Name, Name)] -> Name -> Name
294+updateN ns n | Just n' <- lookup n ns = n'
295+updateN _ n = n
296+
297+updateNs :: [(Name, Name)] -> PTerm -> PTerm
298+updateNs [] t = t
299+updateNs ns t = mapPT updateRef t
300+ where updateRef (PRef fc f) = PRef fc (updateN ns f)
301+ updateRef t = t
302+
303+-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
304+-- updateDNs [] t = t
305+-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
306+-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
307+-- where updateCNs ns (PClause n l ts r ds)
308+-- = PClause (updateN ns n) (fmap (updateNs ns) l)
309+-- (map (fmap (updateNs ns)) ts)
310+-- (fmap (updateNs ns) r)
311+-- (map (updateDNs ns) ds)
312+-- updateDNs ns c = c
313+
314+-- High level language terms
315+
316+data PTerm = PQuote Raw
317+ | PRef FC Name
318+ | PLam Name PTerm PTerm
319+ | PPi Plicity Name PTerm PTerm
320+ | PLet Name PTerm PTerm PTerm
321+ | PTyped PTerm PTerm -- term with explicit type
322+ | PApp FC PTerm [PArg]
323+ | PCase FC PTerm [(PTerm, PTerm)]
324+ | PTrue FC
325+ | PFalse FC
326+ | PRefl FC
327+ | PResolveTC FC
328+ | PEq FC PTerm PTerm
329+ | PPair FC PTerm PTerm
330+ | PDPair FC PTerm PTerm PTerm
331+ | PAlternative Bool [PTerm] -- True if only one may work
332+ | PHidden PTerm -- irrelevant or hidden pattern
333+ | PSet
334+ | PConstant Const
335+ | Placeholder
336+ | PDoBlock [PDo]
337+ | PIdiom FC PTerm
338+ | PReturn FC
339+ | PMetavar Name
340+ | PProof [PTactic]
341+ | PTactics [PTactic] -- as PProof, but no auto solving
342+ | PElabError Err -- error to report on elaboration
343+ | PImpossible -- special case for declaring when an LHS can't typecheck
344+ deriving Eq
345+{-!
346+deriving instance Binary PTerm
347+!-}
348+
349+mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
350+mapPT f t = f (mpt t) where
351+ mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
352+ mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
353+ mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
354+ mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
355+ mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
356+ mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
357+ mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
358+ mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
359+ mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
360+ mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
361+ mpt (PHidden t) = PHidden (mapPT f t)
362+ mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
363+ mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
364+ mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
365+ mpt x = x
366+
367+
368+data PTactic' t = Intro [Name] | Intros | Focus Name
369+ | Refine Name [Bool] | Rewrite t | LetTac Name t
370+ | Exact t | Compute | Trivial
371+ | Solve
372+ | Attack
373+ | ProofState | ProofTerm | Undo
374+ | Try (PTactic' t) (PTactic' t)
375+ | TSeq (PTactic' t) (PTactic' t)
376+ | Qed | Abandon
377+ deriving (Show, Eq, Functor)
378+{-!
379+deriving instance Binary PTactic'
380+!-}
381+
382+instance Sized a => Sized (PTactic' a) where
383+ size (Intro nms) = 1 + size nms
384+ size Intros = 1
385+ size (Focus nm) = 1 + size nm
386+ size (Refine nm bs) = 1 + size nm + length bs
387+ size (Rewrite t) = 1 + size t
388+ size (LetTac nm t) = 1 + size nm + size t
389+ size (Exact t) = 1 + size t
390+ size Compute = 1
391+ size Trivial = 1
392+ size Solve = 1
393+ size Attack = 1
394+ size ProofState = 1
395+ size ProofTerm = 1
396+ size Undo = 1
397+ size (Try l r) = 1 + size l + size r
398+ size (TSeq l r) = 1 + size l + size r
399+ size Qed = 1
400+ size Abandon = 1
401+
402+type PTactic = PTactic' PTerm
403+
404+data PDo' t = DoExp FC t
405+ | DoBind FC Name t
406+ | DoBindP FC t t
407+ | DoLet FC Name t t
408+ | DoLetP FC t t
409+ deriving (Eq, Functor)
410+{-!
411+deriving instance Binary PDo'
412+!-}
413+
414+instance Sized a => Sized (PDo' a) where
415+ size (DoExp fc t) = 1 + size fc + size t
416+ size (DoBind fc nm t) = 1 + size fc + size nm + size t
417+ size (DoBindP fc l r) = 1 + size fc + size l + size r
418+ size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
419+ size (DoLetP fc l r) = 1 + size fc + size l + size r
420+
421+type PDo = PDo' PTerm
422+
423+-- The priority gives a hint as to elaboration order. Best to elaborate
424+-- things early which will help give a more concrete type to other
425+-- variables, e.g. a before (interpTy a).
426+
427+data PArg' t = PImp { priority :: Int,
428+ lazyarg :: Bool, pname :: Name, getTm :: t }
429+ | PExp { priority :: Int,
430+ lazyarg :: Bool, getTm :: t }
431+ | PConstraint { priority :: Int,
432+ lazyarg :: Bool, getTm :: t }
433+ | PTacImplicit { priority :: Int,
434+ lazyarg :: Bool, pname :: Name,
435+ getScript :: t,
436+ getTm :: t }
437+ deriving (Show, Eq, Functor)
438+
439+instance Sized a => Sized (PArg' a) where
440+ size (PImp p l nm trm) = 1 + size nm + size trm
441+ size (PExp p l trm) = 1 + size trm
442+ size (PConstraint p l trm) = 1 + size trm
443+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
444+
445+{-!
446+deriving instance Binary PArg'
447+!-}
448+
449+pimp = PImp 0 True
450+pexp = PExp 0 False
451+pconst = PConstraint 0 False
452+ptacimp = PTacImplicit 0 True
453+
454+type PArg = PArg' PTerm
455+
456+-- Type class data
457+
458+data ClassInfo = CI { instanceName :: Name,
459+ class_methods :: [(Name, (FnOpts, PTerm))],
460+ class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
461+ class_params :: [Name],
462+ class_instances :: [Name] }
463+ deriving Show
464+{-!
465+deriving instance Binary ClassInfo
466+!-}
467+
468+data OptInfo = Optimise { collapsible :: Bool,
469+ forceable :: [Int], -- argument positions
470+ recursive :: [Int] }
471+ deriving Show
472+{-!
473+deriving instance Binary OptInfo
474+!-}
475+
476+
477+data TypeInfo = TI { con_names :: [Name] }
478+ deriving Show
479+{-!
480+deriving instance Binary TypeInfo
481+!-}
482+
483+-- Syntactic sugar info
484+
485+data DSL' t = DSL { dsl_bind :: t,
486+ dsl_return :: t,
487+ dsl_apply :: t,
488+ dsl_pure :: t,
489+ dsl_var :: Maybe t,
490+ index_first :: Maybe t,
491+ index_next :: Maybe t,
492+ dsl_lambda :: Maybe t,
493+ dsl_let :: Maybe t
494+ }
495+ deriving (Show, Functor)
496+{-!
497+deriving instance Binary DSL'
498+!-}
499+
500+type DSL = DSL' PTerm
501+
502+data SynContext = PatternSyntax | TermSyntax | AnySyntax
503+ deriving Show
504+{-!
505+deriving instance Binary SynContext
506+!-}
507+
508+data Syntax = Rule [SSymbol] PTerm SynContext
509+ deriving Show
510+{-!
511+deriving instance Binary Syntax
512+!-}
513+
514+data SSymbol = Keyword Name
515+ | Symbol String
516+ | Binding Name
517+ | Expr Name
518+ | SimpleExpr Name
519+ deriving Show
520+{-!
521+deriving instance Binary SSymbol
522+!-}
523+
524+initDSL = DSL (PRef f (UN ">>="))
525+ (PRef f (UN "return"))
526+ (PRef f (UN "<$>"))
527+ (PRef f (UN "pure"))
528+ Nothing
529+ Nothing
530+ Nothing
531+ Nothing
532+ Nothing
533+ where f = FC "(builtin)" 0
534+
535+data SyntaxInfo = Syn { using :: [(Name, PTerm)],
536+ syn_params :: [(Name, PTerm)],
537+ syn_namespace :: [String],
538+ no_imp :: [Name],
539+ decoration :: Name -> Name,
540+ inPattern :: Bool,
541+ implicitAllowed :: Bool,
542+ dsl_info :: DSL }
543+ deriving Show
544+{-!
545+deriving instance Binary SyntaxInfo
546+!-}
547+
548+defaultSyntax = Syn [] [] [] [] id False False initDSL
549+
550+expandNS :: SyntaxInfo -> Name -> Name
551+expandNS syn n@(NS _ _) = n
552+expandNS syn n = case syn_namespace syn of
553+ [] -> n
554+ xs -> NS n xs
555+
556+
557+--- Pretty printing declarations and terms
558+
559+instance Show PTerm where
560+ show tm = showImp False tm
561+
562+instance Pretty PTerm where
563+ pretty = prettyImp False
564+
565+instance Show PDecl where
566+ show d = showDeclImp False d
567+
568+instance Show PClause where
569+ show c = showCImp True c
570+
571+instance Show PData where
572+ show d = showDImp False d
573+
574+showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
575+showDeclImp t (PTy _ _ _ n ty) = show n ++ " : " ++ showImp t ty
576+showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)
577+showDeclImp _ (PData _ _ d) = show d
578+
579+showCImp :: Bool -> PClause -> String
580+showCImp impl (PClause _ n l ws r w)
581+ = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r
582+ ++ " where " ++ show w
583+ where
584+ showWs [] = ""
585+ showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
586+showCImp impl (PWith _ n l ws r w)
587+ = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r
588+ ++ " { " ++ show w ++ " } "
589+ where
590+ showWs [] = ""
591+ showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs
592+
593+
594+showDImp :: Bool -> PData -> String
595+showDImp impl (PDatadecl n ty cons)
596+ = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"
597+ ++ showSep "\n\t| "
598+ (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)
599+
600+getImps :: [PArg] -> [(Name, PTerm)]
601+getImps [] = []
602+getImps (PImp _ _ n tm : xs) = (n, tm) : getImps xs
603+getImps (_ : xs) = getImps xs
604+
605+getExps :: [PArg] -> [PTerm]
606+getExps [] = []
607+getExps (PExp _ _ tm : xs) = tm : getExps xs
608+getExps (_ : xs) = getExps xs
609+
610+getConsts :: [PArg] -> [PTerm]
611+getConsts [] = []
612+getConsts (PConstraint _ _ tm : xs) = tm : getConsts xs
613+getConsts (_ : xs) = getConsts xs
614+
615+getAll :: [PArg] -> [PTerm]
616+getAll = map getTm
617+
618+prettyImp :: Bool -> PTerm -> Doc
619+prettyImp impl = prettySe 10
620+ where
621+ prettySe p (PQuote r) =
622+ if size r > breakingSize then
623+ text "![" $$ pretty r <> text "]"
624+ else
625+ text "![" <> pretty r <> text "]"
626+ prettySe p (PRef fc n) =
627+ if impl then
628+ pretty n
629+ else
630+ prettyBasic n
631+ where
632+ prettyBasic n@(UN _) = pretty n
633+ prettyBasic (MN _ s) = text s
634+ prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
635+ prettySe p (PLam n ty sc) =
636+ bracket p 2 $
637+ if size sc > breakingSize then
638+ text "λ" <> pretty n <+> text "=>" $+$ pretty sc
639+ else
640+ text "λ" <> pretty n <+> text "=>" <+> pretty sc
641+ prettySe p (PLet n ty v sc) =
642+ bracket p 2 $
643+ if size sc > breakingSize then
644+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
645+ nest nestingSize (prettySe 10 sc)
646+ else
647+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
648+ prettySe 10 sc
649+ prettySe p (PPi (Exp l s) n ty sc)
650+ | n `elem` allNamesIn sc || impl =
651+ let open = if l then text "|" <> lparen else lparen in
652+ bracket p 2 $
653+ if size sc > breakingSize then
654+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
655+ st <+> text "->" $+$ prettySe 10 sc
656+ else
657+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
658+ st <+> text "->" <+> prettySe 10 sc
659+ | otherwise =
660+ bracket p 2 $
661+ if size sc > breakingSize then
662+ prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
663+ else
664+ prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
665+ where
666+ st =
667+ case s of
668+ Static -> text "[static]"
669+ _ -> empty
670+ prettySe p (PPi (Imp l s) n ty sc)
671+ | impl =
672+ let open = if l then text "|" <> lbrace else lbrace in
673+ bracket p 2 $
674+ if size sc > breakingSize then
675+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
676+ st <+> text "->" <+> prettySe 10 sc
677+ else
678+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
679+ st <+> text "->" <+> prettySe 10 sc
680+ | otherwise = prettySe 10 sc
681+ where
682+ st =
683+ case s of
684+ Static -> text $ "[static]"
685+ _ -> empty
686+ prettySe p (PPi (Constraint _ _) n ty sc) =
687+ bracket p 2 $
688+ if size sc > breakingSize then
689+ prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
690+ else
691+ prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
692+ prettySe p (PPi (TacImp _ _ s) n ty sc) =
693+ bracket p 2 $
694+ if size sc > breakingSize then
695+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
696+ rbrace <+> text "->" $+$ prettySe 10 sc
697+ else
698+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
699+ rbrace <+> text "->" <+> prettySe 10 sc
700+ prettySe p (PApp _ (PRef _ f) [])
701+ | not impl = pretty f
702+ prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
703+ | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
704+ let [l, r] = getExps args in
705+ bracket p 1 $
706+ if size r > breakingSize then
707+ prettySe 1 l <+> pretty op $+$ prettySe 0 r
708+ else
709+ prettySe 1 l <+> pretty op <+> prettySe 0 r
710+ prettySe p (PApp _ f as) =
711+ let args = getExps as in
712+ bracket p 1 $
713+ prettySe 1 f <+>
714+ if impl then
715+ foldl fS empty as
716+ -- foldr (<+>) empty $ map prettyArgS as
717+ else
718+ foldl fSe empty args
719+ -- foldr (<+>) empty $ map prettyArgSe args
720+ where
721+ fS l r =
722+ if size r > breakingSize then
723+ l $+$ nest nestingSize (prettyArgS r)
724+ else
725+ l <+> prettyArgS r
726+
727+ fSe l r =
728+ if size r > breakingSize then
729+ l $+$ nest nestingSize (prettyArgSe r)
730+ else
731+ l <+> prettyArgSe r
732+ prettySe p (PCase _ scr opts) =
733+ text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
734+ where
735+ prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
736+
737+ sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
738+ prettySe p (PHidden tm) = text "." <> prettySe 0 tm
739+ prettySe p (PRefl _) = text "refl"
740+ prettySe p (PResolveTC _) = text "resolvetc"
741+ prettySe p (PTrue _) = text "()"
742+ prettySe p (PFalse _) = text "_|_"
743+ prettySe p (PEq _ l r) =
744+ bracket p 2 $
745+ if size r > breakingSize then
746+ prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
747+ else
748+ prettySe 10 l <+> text "=" <+> prettySe 10 r
749+ prettySe p (PTyped l r) =
750+ lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
751+ prettySe p (PPair _ l r) =
752+ if size r > breakingSize then
753+ lparen <> prettySe 10 l <> text "," $+$
754+ prettySe 10 r <> rparen
755+ else
756+ lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
757+ prettySe p (PDPair _ l t r) =
758+ if size r > breakingSize then
759+ lparen <> prettySe 10 l <+> text "**" $+$
760+ prettySe 10 r <> rparen
761+ else
762+ lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
763+ prettySe p (PAlternative a as) =
764+ lparen <> text "|" <> prettyAs <> text "|" <> rparen
765+ where
766+ prettyAs =
767+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
768+ prettySe p PSet = text "Set"
769+ prettySe p (PConstant c) = pretty c
770+ -- XXX: add pretty for tactics
771+ prettySe p (PProof ts) =
772+ text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
773+ prettySe p (PTactics ts) =
774+ text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
775+ prettySe p (PMetavar n) = text "?" <> pretty n
776+ prettySe p (PReturn f) = text "return"
777+ prettySe p PImpossible = text "impossible"
778+ prettySe p Placeholder = text "_"
779+ prettySe p (PDoBlock _) = text "do block pretty not implemented"
780+ prettySe p (PElabError s) = pretty s
781+
782+ prettySe p _ = text "test"
783+
784+ prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
785+ prettyArgS (PExp _ _ tm) = prettyArgSe tm
786+ prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
787+ prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
788+
789+ prettyArgSe arg = prettySe 0 arg
790+ prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
791+ prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
792+ prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
793+
794+ bracket outer inner doc
795+ | inner > outer = lparen <> doc <> rparen
796+ | otherwise = doc
797+
798+showImp :: Bool -> PTerm -> String
799+showImp impl tm = se 10 tm where
800+ se p (PQuote r) = "![" ++ show r ++ "]"
801+ se p (PRef fc n) = if impl then show n -- ++ "[" ++ show fc ++ "]"
802+ else showbasic n
803+ where showbasic n@(UN _) = show n
804+ showbasic (MN _ s) = s
805+ showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n
806+ se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++
807+ (if impl then " : " ++ se 10 ty else "") ++ " => "
808+ ++ se 10 sc
809+ se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++
810+ " in " ++ se 10 sc
811+ se p (PPi (Exp l s) n ty sc)
812+ | n `elem` allNamesIn sc || impl
813+ = bracket p 2 $
814+ if l then "|(" else "(" ++
815+ show n ++ " : " ++ se 10 ty ++
816+ ") " ++ st ++
817+ "-> " ++ se 10 sc
818+ | otherwise = bracket p 2 $ se 0 ty ++ " " ++ st ++ "-> " ++ se 10 sc
819+ where st = case s of
820+ Static -> "[static] "
821+ _ -> ""
822+ se p (PPi (Imp l s) n ty sc)
823+ | impl = bracket p 2 $ if l then "|{" else "{" ++
824+ show n ++ " : " ++ se 10 ty ++
825+ "} " ++ st ++ "-> " ++ se 10 sc
826+ | otherwise = se 10 sc
827+ where st = case s of
828+ Static -> "[static] "
829+ _ -> ""
830+ se p (PPi (Constraint _ _) n ty sc)
831+ = bracket p 2 $ se 10 ty ++ " => " ++ se 10 sc
832+ se p (PPi (TacImp _ _ s) n ty sc)
833+ = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
834+ se p (PApp _ (PRef _ f) [])
835+ | not impl = show f
836+ se p (PApp _ (PRef _ op@(UN (f:_))) args)
837+ | length (getExps args) == 2 && not impl && not (isAlpha f)
838+ = let [l, r] = getExps args in
839+ bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r
840+ se p (PApp _ f as)
841+ = let args = getExps as in
842+ bracket p 1 $ se 1 f ++ if impl then concatMap sArg as
843+ else concatMap seArg args
844+ se p (PCase _ scr opts) = "case " ++ se 10 scr ++ " of " ++ showSep " | " (map sc opts)
845+ where sc (l, r) = se 10 l ++ " => " ++ se 10 r
846+ se p (PHidden tm) = "." ++ se 0 tm
847+ se p (PRefl _) = "refl"
848+ se p (PResolveTC _) = "resolvetc"
849+ se p (PTrue _) = "()"
850+ se p (PFalse _) = "_|_"
851+ se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r
852+ se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"
853+ se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"
854+ se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"
855+ se p (PAlternative a as) = "(|" ++ showSep " , " (map (se 10) as) ++ "|)"
856+ se p PSet = "Set"
857+ se p (PConstant c) = show c
858+ se p (PProof ts) = "proof { " ++ show ts ++ "}"
859+ se p (PTactics ts) = "tactics { " ++ show ts ++ "}"
860+ se p (PMetavar n) = "?" ++ show n
861+ se p (PReturn f) = "return"
862+ se p PImpossible = "impossible"
863+ se p Placeholder = "_"
864+ se p (PDoBlock _) = "do block show not implemented"
865+ se p (PElabError s) = show s
866+-- se p x = "Not implemented"
867+
868+ sArg (PImp _ _ n tm) = siArg (n, tm)
869+ sArg (PExp _ _ tm) = seArg tm
870+ sArg (PConstraint _ _ tm) = scArg tm
871+ sArg (PTacImplicit _ _ n _ tm) = stiArg (n, tm)
872+
873+ seArg arg = " " ++ se 0 arg
874+ siArg (n, val) = " {" ++ show n ++ " = " ++ se 10 val ++ "}"
875+ scArg val = " {{" ++ se 10 val ++ "}}"
876+ stiArg (n, val) = " {auto " ++ show n ++ " = " ++ se 10 val ++ "}"
877+
878+ bracket outer inner str | inner > outer = "(" ++ str ++ ")"
879+ | otherwise = str
880+
881+{-
882+ PQuote Raw
883+ | PRef FC Name
884+ | PLam Name PTerm PTerm
885+ | PPi Plicity Name PTerm PTerm
886+ | PLet Name PTerm PTerm PTerm
887+ | PTyped PTerm PTerm -- term with explicit type
888+ | PApp FC PTerm [PArg]
889+ | PCase FC PTerm [(PTerm, PTerm)]
890+ | PTrue FC
891+ | PFalse FC
892+ | PRefl FC
893+ | PResolveTC FC
894+ | PEq FC PTerm PTerm
895+ | PPair FC PTerm PTerm
896+ | PDPair FC PTerm PTerm PTerm
897+ | PAlternative [PTerm]
898+ | PHidden PTerm -- irrelevant or hidden pattern
899+ | PSet
900+ | PConstant Const
901+ | Placeholder
902+ | PDoBlock [PDo]
903+ | PIdiom FC PTerm
904+ | PReturn FC
905+ | PMetavar Name
906+ | PProof [PTactic]
907+ | PTactics [PTactic] -- as PProof, but no auto solving
908+ | PElabError Err -- error to report on elaboration
909+ | PImpossible -- special case for declaring when an LHS can't typecheck
910+-}
911+
912+instance Sized PTerm where
913+ size (PQuote rawTerm) = size rawTerm
914+ size (PRef fc name) = size name
915+ size (PLam name ty bdy) = 1 + size ty + size bdy
916+ size (PPi plicity name ty bdy) = 1 + size ty + size bdy
917+ size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
918+ size (PTyped trm ty) = 1 + size trm + size ty
919+ size (PApp fc name args) = 1 + size args
920+ size (PCase fc trm bdy) = 1 + size trm + size bdy
921+ size (PTrue fc) = 1
922+ size (PFalse fc) = 1
923+ size (PRefl fc) = 1
924+ size (PResolveTC fc) = 1
925+ size (PEq fc left right) = 1 + size left + size right
926+ size (PPair fc left right) = 1 + size left + size right
927+ size (PDPair fs left ty right) = 1 + size left + size ty + size right
928+ size (PAlternative a alts) = 1 + size alts
929+ size (PHidden hidden) = size hidden
930+ size PSet = 1
931+ size (PConstant const) = 1 + size const
932+ size Placeholder = 1
933+ size (PDoBlock dos) = 1 + size dos
934+ size (PIdiom fc term) = 1 + size term
935+ size (PReturn fc) = 1
936+ size (PMetavar name) = 1
937+ size (PProof tactics) = size tactics
938+ size (PElabError err) = size err
939+ size PImpossible = 1
940+
941+allNamesIn :: PTerm -> [Name]
942+allNamesIn tm = nub $ ni [] tm
943+ where
944+ ni env (PRef _ n)
945+ | not (n `elem` env) = [n]
946+ ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
947+ ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
948+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
949+ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
950+ ni env (PHidden tm) = ni env tm
951+ ni env (PEq _ l r) = ni env l ++ ni env r
952+ ni env (PTyped l r) = ni env l ++ ni env r
953+ ni env (PPair _ l r) = ni env l ++ ni env r
954+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
955+ ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
956+ ni env (PAlternative a ls) = concatMap (ni env) ls
957+ ni env _ = []
958+
959+namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
960+namesIn uvars ist tm = nub $ ni [] tm
961+ where
962+ ni env (PRef _ n)
963+ | not (n `elem` env)
964+ = case lookupTy Nothing n (tt_ctxt ist) of
965+ [] -> [n]
966+ _ -> if n `elem` (map fst uvars) then [n] else []
967+ ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
968+ ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
969+ ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
970+ ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc
971+ ni env (PEq _ l r) = ni env l ++ ni env r
972+ ni env (PTyped l r) = ni env l ++ ni env r
973+ ni env (PPair _ l r) = ni env l ++ ni env r
974+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
975+ ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
976+ ni env (PAlternative a as) = concatMap (ni env) as
977+ ni env (PHidden tm) = ni env tm
978+ ni env _ = []