@@ -1,12 +1,13 @@
11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
22 TypeSynonymInstances, PatternGuards #-}
33
4−module Idris.AbsSyntax where
4+module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
55
66import Core.TT
77import Core.Evaluate
88import Core.Elaborate hiding (Tactic(..))
99import Core.Typecheck
10+import Idris.AbsSyntaxTree
1011import RTS.SC
1112
1213import Paths_idris
@@ -25,96 +26,6 @@ import qualified Epic.Epic as E
2526
2627import Util.Pretty
2728
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)
11829
11930getContext :: Idris Context
12031getContext = do i <- get; return (tt_ctxt i)
@@ -392,867 +303,6 @@ setTypeCase t = do i <- get
392303 let opt' = opts { opt_typecase = t }
393304 put (i { idris_options = opt' })
394305
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 _ = []
1256306
1257307-- For inferring types of things
1258308