git.iko.soy/Idris-dev
on master help sign in
Merge pull request #17 from dpmulligan/master
8d4a93bEdwin Brady
idris.cabal+1−1
compare with master
unifiedsplit
@@ -67,7 +67,7 @@ Executable idris
67
67
68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
68 Build-depends: base>=4 && <5, parsec, mtl, Cabal, haskeline,
69 containers, process, transformers, filepath, directory,
69 containers, process, transformers, filepath, directory,
70− binary, bytestring, epic>=0.9.3
70+ binary, bytestring, epic>=0.9.3, pretty
71
71
72 Extensions: MultiParamTypeClasses, FunctionalDependencies,
72 Extensions: MultiParamTypeClasses, FunctionalDependencies,
73 FlexibleInstances, TemplateHaskell
73 FlexibleInstances, TemplateHaskell
lib/prelude/heap.idr+26
@@ -30,6 +30,15 @@ total size : MaxiphobicHeap a -> Nat
30size Empty = O
30size Empty = O
31size (Node s l e r) = s
31size (Node s l e r) = s
32
32
33+isValidHeap : Ord a => MaxiphobicHeap a -> Bool
34+isValidHeap Empty = True
35+isValidHeap (Node s l e r) =
36+ dominates e l && dominates e r && s == S (size l + size r)
37+ where
38+ dominates : Ord a => a -> MaxiphobicHeap a -> Bool
39+ dominates e Empty = True
40+ dominates e (Node s l e' r) = e' <= e
41+
33--------------------------------------------------------------------------------
42--------------------------------------------------------------------------------
34-- Basic heaps
43-- Basic heaps
35--------------------------------------------------------------------------------
44--------------------------------------------------------------------------------
@@ -141,6 +150,23 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h =
141isEmptySizeZero Empty p = refl
150isEmptySizeZero Empty p = refl
142isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
151isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
143
152
153+total emptyHeapValid : Ord a => isValidHeap empty = True
154+emptyHeapValid = refl
155+
156+total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True
157+singletonHeapValid e = refl
158+
159+{-
160+total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->
161+ (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->
162+ (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True
163+mergePreservesValidHeaps Empty Empty lp rp = refl
164+mergePreservesValidHeaps Empty (Node rs rl re rr) lp rp = rp
165+mergePreservesValidHeaps (Node ls ll le lr) Empty lp rp = lp
166+mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =
167+ ?mergePreservesValidHeapsBody
168+-}
169+
144--------------------------------------------------------------------------------
170--------------------------------------------------------------------------------
145-- Proofs
171-- Proofs
146--------------------------------------------------------------------------------
172--------------------------------------------------------------------------------
src/Core/Elaborate.hs+3
@@ -21,6 +21,8 @@ import Data.Char
21import Data.List
21import Data.List
22import Debug.Trace
22import Debug.Trace
23
23
24+import Util.Pretty
25+
24-- I don't really want this here, but it's useful for the test shell
26-- I don't really want this here, but it's useful for the test shell
25data Command = Theorem Name Raw
27data Command = Theorem Name Raw
26 | Eval Raw
28 | Eval Raw
@@ -30,6 +32,7 @@ data Command = Theorem Name Raw
30
32
31data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
33data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
32 deriving Show
34 deriving Show
35+
33type Elab' aux a = StateT (ElabState aux) TC a
36type Elab' aux a = StateT (ElabState aux) TC a
34type Elab a = Elab' () a
37type Elab a = Elab' () a
35
38
src/Core/ProofShell.hs+3−1
@@ -11,6 +11,8 @@ import Core.Elaborate
11import Control.Monad.State
11import Control.Monad.State
12import System.Console.Haskeline
12import System.Console.Haskeline
13
13
14+import Util.Pretty
15+
14data ShellState = ShellState
16data ShellState = ShellState
15 { ctxt :: Context,
17 { ctxt :: Context,
16 prf :: Maybe ProofState,
18 prf :: Maybe ProofState,
@@ -56,7 +58,7 @@ processCommand (Tac e) state
56runShell :: ShellState -> InputT IO ShellState
58runShell :: ShellState -> InputT IO ShellState
57runShell st = do (prompt, parser) <-
59runShell st = do (prompt, parser) <-
58 maybe (return ("TT# ", parseCommand))
60 maybe (return ("TT# ", parseCommand))
59− (\st -> do outputStrLn (show st)
61+ (\st -> do outputStrLn . render . pretty $ st
60 return (show (thname st) ++ "# ", parseTactic))
62 return (show (thname st) ++ "# ", parseTactic))
61 (prf st)
63 (prf st)
62 x <- getInputLine prompt
64 x <- getInputLine prompt
src/Core/ProofState.hs+42−1
@@ -13,10 +13,12 @@ import Core.TT
13import Core.Unify
13import Core.Unify
14
14
15import Control.Monad.State
15import Control.Monad.State
16−import Control.Applicative
16+import Control.Applicative hiding (empty)
17import Data.List
17import Data.List
18import Debug.Trace
18import Debug.Trace
19
19
20+import Util.Pretty
21+
20data ProofState = PS { thname :: Name,
22data ProofState = PS { thname :: Name,
21 holes :: [Name], -- holes still to be solved
23 holes :: [Name], -- holes still to be solved
22 nextname :: Int, -- name supply
24 nextname :: Int, -- name supply
@@ -94,6 +96,45 @@ instance Show ProofState where
94 " =?= " ++ showEnv ps v
96 " =?= " ++ showEnv ps v
95 showG ps b = showEnv ps (binderTy b)
97 showG ps b = showEnv ps (binderTy b)
96
98
99+instance Pretty ProofState where
100+ pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =
101+ if size nm > breakingSize then
102+ pretty nm <> colon $$ nest nestingSize (text " no more goals.")
103+ else
104+ pretty nm <> colon <+> text " no more goals."
105+ pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =
106+ let OK g = goal (Just h) tm in
107+ let wkEnv = premises g in
108+ text "Other goals" <+> colon <+> pretty hs $$
109+ prettyPs wkEnv (reverse wkEnv) $$
110+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
111+ pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
112+ where
113+ prettyGoal ps (Guess t v) =
114+ if size v > breakingSize then
115+ prettyEnv ps t <+> text "=?=" $$
116+ nest nestingSize (prettyEnv ps v)
117+ else
118+ prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
119+ prettyGoal ps b = prettyEnv ps $ binderTy b
120+
121+ prettyPs env [] = empty
122+ prettyPs env ((n, Let t v):bs) =
123+ nest nestingSize (pretty n <+> colon <+>
124+ if size v > breakingSize then
125+ prettyEnv env t <+> text "=" $$
126+ nest nestingSize (prettyEnv env v) $$
127+ nest nestingSize (prettyPs env bs)
128+ else
129+ prettyEnv env t <+> text "=" <+> prettyEnv env v $$
130+ nest nestingSize (prettyPs env bs))
131+ prettyPs env ((n, b):bs) =
132+ if size (binderTy b) > breakingSize then
133+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
134+ else
135+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
136+ nest nestingSize (prettyPs env bs))
137+
97same Nothing n = True
138same Nothing n = True
98same (Just x) n = x == n
139same (Just x) n = x == n
99
140
src/Core/TT.hs+155
@@ -10,6 +10,8 @@ import Data.List
10import qualified Data.Binary as B
10import qualified Data.Binary as B
11import Data.Binary hiding (get, put)
11import Data.Binary hiding (get, put)
12
12
13+import Util.Pretty hiding (Str)
14+
13{- The language has:
15{- The language has:
14 * Full dependent types
16 * Full dependent types
15 * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
17 * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
@@ -34,6 +36,9 @@ data FC = FC { fc_fname :: String,
34deriving instance Binary FC
36deriving instance Binary FC
35!-}
37!-}
36
38
39+instance Sized FC where
40+ size (FC f l) = 1 + length f
41+
37instance Show FC where
42instance Show FC where
38 show (FC f l) = f ++ ":" ++ show l
43 show (FC f l) = f ++ ":" ++ show l
39
44
@@ -48,6 +53,17 @@ data Err = Msg String
48 | At FC Err
53 | At FC Err
49 deriving Eq
54 deriving Eq
50
55
56+instance Sized Err where
57+ size (Msg msg) = length msg
58+ size (CantUnify left right err score) = size left + size right + size err
59+ size (NoSuchVariable name) = size name
60+ size (NotInjective l c r) = size l + size c + size r
61+ size (CantResolve trm) = size trm
62+ size (IncompleteTerm trm) = size trm
63+ size UniverseError = 1
64+ size ProgramLineComment = 1
65+ size (At fc err) = size fc + size err
66+
51score :: Err -> Int
67score :: Err -> Int
52score (CantUnify _ _ m s) = s + score m
68score (CantUnify _ _ m s) = s + score m
53score (CantResolve _) = 20
69score (CantResolve _) = 20
@@ -60,10 +76,30 @@ instance Show Err where
60 ++ show e ++ " " ++ show i
76 ++ show e ++ " " ++ show i
61 show _ = "Error"
77 show _ = "Error"
62
78
79+instance Pretty Err where
80+ pretty (Msg m) = text m
81+ pretty (CantUnify l r e i) =
82+ if size l + size r > breakingSize then
83+ text "Cannot unify" <+> colon $$
84+ nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
85+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
86+ else
87+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
88+ nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
89+ pretty _ = text "Error"
90+
63data TC a = OK a
91data TC a = OK a
64 | Error Err
92 | Error Err
65 deriving (Eq, Functor)
93 deriving (Eq, Functor)
66
94
95+instance Pretty a => Pretty (TC a) where
96+ pretty (OK ok) = pretty ok
97+ pretty (Error err) =
98+ if size err > breakingSize then
99+ text "Error" <+> colon $$ (nest nestingSize $ pretty err)
100+ else
101+ text "Error" <+> colon <+> pretty err
102+
67instance Show a => Show (TC a) where
103instance Show a => Show (TC a) where
68 show (OK x) = show x
104 show (OK x) = show x
69 show (Error str) = "Error: " ++ show str
105 show (Error str) = "Error: " ++ show str
@@ -118,6 +154,16 @@ data Name = UN String
118deriving instance Binary Name
154deriving instance Binary Name
119!-}
155!-}
120
156
157+instance Sized Name where
158+ size (UN n) = 1
159+ size (NS n els) = 1 + length els
160+ size (MN i n) = 1
161+
162+instance Pretty Name where
163+ pretty (UN n) = text n
164+ pretty (NS n s) = pretty n
165+ pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace
166+
121instance Show Name where
167instance Show Name where
122 show (UN n) = n
168 show (UN n) = n
123 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n
169 show (NS n s) = showSep "." (reverse s) ++ "." ++ show n
@@ -190,6 +236,23 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
190deriving instance Binary Const
236deriving instance Binary Const
191!-}
237!-}
192
238
239+instance Sized Const where
240+ size _ = 1
241+
242+instance Pretty Const where
243+ pretty (I i) = text . show $ i
244+ pretty (BI i) = text . show $ i
245+ pretty (Fl f) = text . show $ f
246+ pretty (Ch c) = text . show $ c
247+ pretty (Str s) = text s
248+ pretty IType = text "Int"
249+ pretty BIType = text "BigInt"
250+ pretty FlType = text "Float"
251+ pretty ChType = text "Char"
252+ pretty StrType = text "String"
253+ pretty PtrType = text "Ptr"
254+ pretty Forgot = text "Forgot"
255+
193data Raw = Var Name
256data Raw = Var Name
194 | RBind Name (Binder Raw) Raw
257 | RBind Name (Binder Raw) Raw
195 | RApp Raw Raw
258 | RApp Raw Raw
@@ -197,6 +260,18 @@ data Raw = Var Name
197 | RForce Raw
260 | RForce Raw
198 | RConstant Const
261 | RConstant Const
199 deriving (Show, Eq)
262 deriving (Show, Eq)
263+
264+instance Sized Raw where
265+ size (Var name) = 1
266+ size (RBind name bind right) = 1 + size bind + size right
267+ size (RApp left right) = 1 + size left + size right
268+ size RSet = 1
269+ size (RForce raw) = 1 + size raw
270+ size (RConstant const) = size const
271+
272+instance Pretty Raw where
273+ pretty = text . show
274+
200{-!
275{-!
201deriving instance Binary Raw
276deriving instance Binary Raw
202!-}
277!-}
@@ -218,6 +293,17 @@ data Binder b = Lam { binderTy :: b }
218deriving instance Binary Binder
293deriving instance Binary Binder
219!-}
294!-}
220
295
296+instance Sized a => Sized (Binder a) where
297+ size (Lam ty) = 1 + size ty
298+ size (Pi ty) = 1 + size ty
299+ size (Let ty val) = 1 + size ty + size val
300+ size (NLet ty val) = 1 + size ty + size val
301+ size (Hole ty) = 1 + size ty
302+ size (GHole ty) = 1 + size ty
303+ size (Guess ty val) = 1 + size ty + size val
304+ size (PVar ty) = 1 + size ty
305+ size (PVTy ty) = 1 + size ty
306+
221fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
307fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
222fmapMB f (Let t v) = liftM2 Let (f t) (f v)
308fmapMB f (Let t v) = liftM2 Let (f t) (f v)
223fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
309fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
@@ -259,6 +345,9 @@ data UExp = UVar Int -- universe variable
259 | UVal Int -- explicit universe level
345 | UVal Int -- explicit universe level
260 deriving (Eq, Ord)
346 deriving (Eq, Ord)
261
347
348+instance Sized UExp where
349+ size _ = 1
350+
262-- We assume that universe levels have been checked, so anything external
351-- We assume that universe levels have been checked, so anything external
263-- can just have the same universe variable and we won't get any new
352-- can just have the same universe variable and we won't get any new
264-- cycles.
353-- cycles.
@@ -289,6 +378,12 @@ data NameType = Bound | Ref | DCon Int Int | TCon Int Int
289deriving instance Binary NameType
378deriving instance Binary NameType
290!-}
379!-}
291
380
381+instance Sized NameType where
382+ size _ = 1
383+
384+instance Pretty NameType where
385+ pretty = text . show
386+
292instance Eq NameType where
387instance Eq NameType where
293 Bound == Bound = True
388 Bound == Bound = True
294 Ref == Ref = True
389 Ref == Ref = True
@@ -308,6 +403,18 @@ data TT n = P NameType n (TT n) -- embed type
308deriving instance Binary TT
403deriving instance Binary TT
309!-}
404!-}
310
405
406+instance Sized a => Sized (TT a) where
407+ size (P name n trm) = 1 + size name + size n + size trm
408+ size (V v) = 1
409+ size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
410+ size (App l r) = 1 + size l + size r
411+ size (Constant c) = size c
412+ size Erased = 1
413+ size (Set u) = 1 + size u
414+
415+instance Pretty a => Pretty (TT a) where
416+ pretty _ = text "test"
417+
311type EnvTT n = [(n, Binder (TT n))]
418type EnvTT n = [(n, Binder (TT n))]
312
419
313data Datatype n = Data { d_typename :: n,
420data Datatype n = Data { d_typename :: n,
@@ -496,6 +603,54 @@ instance Show Const where
496showEnv env t = showEnv' env t False
603showEnv env t = showEnv' env t False
497showEnvDbg env t = showEnv' env t True
604showEnvDbg env t = showEnv' env t True
498
605
606+prettyEnv env t = prettyEnv' env t False
607+ where
608+ prettyEnv' env t dbg = prettySe 10 env t dbg
609+
610+ bracket outer inner p
611+ | inner > outer = lparen <> p <> rparen
612+ | otherwise = p
613+
614+ prettySe p env (P nt n t) debug =
615+ pretty n <+>
616+ if debug then
617+ lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
618+ else
619+ empty
620+ prettySe p env (V i) debug
621+ | i < length env =
622+ if debug then
623+ text . show . fst $ env!!i
624+ else
625+ lbrack <+> text (show i) <+> rbrack
626+ | otherwise = text "unbound" <+> text (show i) <+> text "!"
627+ prettySe p env (Bind n b@(Pi t) sc) debug
628+ | noOccurrence n sc && not debug =
629+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
630+ prettySe p env (Bind n b sc) debug =
631+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
632+ prettySe p env (App f a) debug =
633+ bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
634+ prettySe p env (Constant c) debug = pretty c
635+ prettySe p env Erased debug = text "[_]"
636+ prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)
637+
638+ prettySb env n (Lam t) = prettyB env "λ" "=>" n t
639+ prettySb env n (Hole t) = prettyB env "?defer" "." n t
640+ prettySb env n (Pi t) = prettyB env "(" ") ->" n t
641+ prettySb env n (PVar t) = prettyB env "pat" "." n t
642+ prettySb env n (PVTy t) = prettyB env "pty" "." n t
643+ prettySb env n (Let t v) = prettyBv env "let" "in" n t v
644+ prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
645+
646+ prettyB env op sc n t debug =
647+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
648+
649+ prettyBv env op sc n t v debug =
650+ text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
651+ prettySe 10 env v debug <> text sc
652+
653+
499showEnv' env t dbg = se 10 env t where
654showEnv' env t dbg = se 10 env t where
500 se p env (P nt n t) = show n
655 se p env (P nt n t) = show n
501 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
656 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
src/Idris/AbsSyntax.hs+283−1
@@ -5,18 +5,23 @@ module Idris.AbsSyntax where
5
5
6import Core.TT
6import Core.TT
7import Core.Evaluate
7import Core.Evaluate
8−import Core.Elaborate
8+import Core.Elaborate hiding (Tactic(..))
9import Core.Typecheck
9import Core.Typecheck
10
10
11import System.Console.Haskeline
11import System.Console.Haskeline
12+
12import Control.Monad.State
13import Control.Monad.State
14+
13import Data.List
15import Data.List
14import Data.Char
16import Data.Char
15import Data.Either
17import Data.Either
18+
16import Debug.Trace
19import Debug.Trace
17
20
18import qualified Epic.Epic as E
21import qualified Epic.Epic as E
19
22
23+import Util.Pretty
24+
20data IOption = IOption { opt_logLevel :: Int,
25data IOption = IOption { opt_logLevel :: Int,
21 opt_typecase :: Bool,
26 opt_typecase :: Bool,
22 opt_typeintype :: Bool,
27 opt_typeintype :: Bool,
@@ -571,6 +576,26 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
571deriving instance Binary PTactic'
576deriving instance Binary PTactic'
572!-}
577!-}
573
578
579+instance Sized a => Sized (PTactic' a) where
580+ size (Intro nms) = 1 + size nms
581+ size Intros = 1
582+ size (Focus nm) = 1 + size nm
583+ size (Refine nm bs) = 1 + size nm + length bs
584+ size (Rewrite t) = 1 + size t
585+ size (LetTac nm t) = 1 + size nm + size t
586+ size (Exact t) = 1 + size t
587+ size Compute = 1
588+ size Trivial = 1
589+ size Solve = 1
590+ size Attack = 1
591+ size ProofState = 1
592+ size ProofTerm = 1
593+ size Undo = 1
594+ size (Try l r) = 1 + size l + size r
595+ size (TSeq l r) = 1 + size l + size r
596+ size Qed = 1
597+ size Abandon = 1
598+
574type PTactic = PTactic' PTerm
599type PTactic = PTactic' PTerm
575
600
576data PDo' t = DoExp FC t
601data PDo' t = DoExp FC t
@@ -583,6 +608,13 @@ data PDo' t = DoExp FC t
583deriving instance Binary PDo'
608deriving instance Binary PDo'
584!-}
609!-}
585
610
611+instance Sized a => Sized (PDo' a) where
612+ size (DoExp fc t) = 1 + size fc + size t
613+ size (DoBind fc nm t) = 1 + size fc + size nm + size t
614+ size (DoBindP fc l r) = 1 + size fc + size l + size r
615+ size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
616+ size (DoLetP fc l r) = 1 + size fc + size l + size r
617+
586type PDo = PDo' PTerm
618type PDo = PDo' PTerm
587
619
588-- The priority gives a hint as to elaboration order. Best to elaborate
620-- The priority gives a hint as to elaboration order. Best to elaborate
@@ -600,6 +632,13 @@ data PArg' t = PImp { priority :: Int,
600 getScript :: t,
632 getScript :: t,
601 getTm :: t }
633 getTm :: t }
602 deriving (Show, Eq, Functor)
634 deriving (Show, Eq, Functor)
635+
636+instance Sized a => Sized (PArg' a) where
637+ size (PImp p l nm trm) = 1 + size nm + size trm
638+ size (PExp p l trm) = 1 + size trm
639+ size (PConstraint p l trm) = 1 + size trm
640+ size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
641+
603{-!
642{-!
604deriving instance Binary PArg'
643deriving instance Binary PArg'
605!-}
644!-}
@@ -712,6 +751,9 @@ expandNS syn n = case syn_namespace syn of
712instance Show PTerm where
751instance Show PTerm where
713 show tm = showImp False tm
752 show tm = showImp False tm
714
753
754+instance Pretty PTerm where
755+ pretty = prettyImp False
756+
715instance Show PDecl where
757instance Show PDecl where
716 show d = showDeclImp False d
758 show d = showDeclImp False d
717
759
@@ -765,6 +807,186 @@ getConsts (_ : xs) = getConsts xs
765getAll :: [PArg] -> [PTerm]
807getAll :: [PArg] -> [PTerm]
766getAll = map getTm
808getAll = map getTm
767
809
810+prettyImp :: Bool -> PTerm -> Doc
811+prettyImp impl = prettySe 10
812+ where
813+ prettySe p (PQuote r) =
814+ if size r > breakingSize then
815+ text "![" $$ pretty r <> text "]"
816+ else
817+ text "![" <> pretty r <> text "]"
818+ prettySe p (PRef fc n) =
819+ if impl then
820+ pretty n
821+ else
822+ prettyBasic n
823+ where
824+ prettyBasic n@(UN _) = pretty n
825+ prettyBasic (MN _ s) = text s
826+ prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n
827+ prettySe p (PLam n ty sc) =
828+ bracket p 2 $
829+ if size sc > breakingSize then
830+ text "λ" <> pretty n <+> text "=>" $+$ pretty sc
831+ else
832+ text "λ" <> pretty n <+> text "=>" <+> pretty sc
833+ prettySe p (PLet n ty v sc) =
834+ bracket p 2 $
835+ if size sc > breakingSize then
836+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
837+ nest nestingSize (prettySe 10 sc)
838+ else
839+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
840+ prettySe 10 sc
841+ prettySe p (PPi (Exp l s) n ty sc)
842+ | n `elem` allNamesIn sc || impl =
843+ let open = if l then text "|" <> lparen else lparen in
844+ bracket p 2 $
845+ if size sc > breakingSize then
846+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
847+ st <+> text "->" $+$ prettySe 10 sc
848+ else
849+ open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
850+ st <+> text "->" <+> prettySe 10 sc
851+ | otherwise =
852+ bracket p 2 $
853+ if size sc > breakingSize then
854+ prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
855+ else
856+ prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
857+ where
858+ st =
859+ case s of
860+ Static -> text "[static]"
861+ _ -> empty
862+ prettySe p (PPi (Imp l s) n ty sc)
863+ | impl =
864+ let open = if l then text "|" <> lbrace else lbrace in
865+ bracket p 2 $
866+ if size sc > breakingSize then
867+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
868+ st <+> text "->" <+> prettySe 10 sc
869+ else
870+ open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
871+ st <+> text "->" <+> prettySe 10 sc
872+ | otherwise = prettySe 10 sc
873+ where
874+ st =
875+ case s of
876+ Static -> text $ "[static]"
877+ _ -> empty
878+ prettySe p (PPi (Constraint _ _) n ty sc) =
879+ bracket p 2 $
880+ if size sc > breakingSize then
881+ prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
882+ else
883+ prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
884+ prettySe p (PPi (TacImp _ _ s) n ty sc) =
885+ bracket p 2 $
886+ if size sc > breakingSize then
887+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
888+ rbrace <+> text "->" $+$ prettySe 10 sc
889+ else
890+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
891+ rbrace <+> text "->" <+> prettySe 10 sc
892+ prettySe p (PApp _ (PRef _ f) [])
893+ | not impl = pretty f
894+ prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)
895+ | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =
896+ let [l, r] = getExps args in
897+ bracket p 1 $
898+ if size r > breakingSize then
899+ prettySe 1 l <+> pretty op $+$ prettySe 0 r
900+ else
901+ prettySe 1 l <+> pretty op <+> prettySe 0 r
902+ prettySe p (PApp _ f as) =
903+ let args = getExps as in
904+ bracket p 1 $
905+ prettySe 1 f <+>
906+ if impl then
907+ foldl fS empty as
908+ -- foldr (<+>) empty $ map prettyArgS as
909+ else
910+ foldl fSe empty args
911+ -- foldr (<+>) empty $ map prettyArgSe args
912+ where
913+ fS l r =
914+ if size r > breakingSize then
915+ l $+$ nest nestingSize (prettyArgS r)
916+ else
917+ l <+> prettyArgS r
918+
919+ fSe l r =
920+ if size r > breakingSize then
921+ l $+$ nest nestingSize (prettyArgSe r)
922+ else
923+ l <+> prettyArgSe r
924+ prettySe p (PCase _ scr opts) =
925+ text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
926+ where
927+ prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
928+
929+ sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
930+ prettySe p (PHidden tm) = text "." <> prettySe 0 tm
931+ prettySe p (PRefl _) = text "refl"
932+ prettySe p (PResolveTC _) = text "resolvetc"
933+ prettySe p (PTrue _) = text "()"
934+ prettySe p (PFalse _) = text "_|_"
935+ prettySe p (PEq _ l r) =
936+ bracket p 2 $
937+ if size r > breakingSize then
938+ prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
939+ else
940+ prettySe 10 l <+> text "=" <+> prettySe 10 r
941+ prettySe p (PTyped l r) =
942+ lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
943+ prettySe p (PPair _ l r) =
944+ if size r > breakingSize then
945+ lparen <> prettySe 10 l <> text "," $+$
946+ prettySe 10 r <> rparen
947+ else
948+ lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
949+ prettySe p (PDPair _ l t r) =
950+ if size r > breakingSize then
951+ lparen <> prettySe 10 l <+> text "**" $+$
952+ prettySe 10 r <> rparen
953+ else
954+ lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
955+ prettySe p (PAlternative as) =
956+ lparen <> text "|" <> prettyAs <> text "|" <> rparen
957+ where
958+ prettyAs =
959+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
960+ prettySe p PSet = text "Set"
961+ prettySe p (PConstant c) = pretty c
962+ -- XXX: add pretty for tactics
963+ prettySe p (PProof ts) =
964+ text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
965+ prettySe p (PTactics ts) =
966+ text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
967+ prettySe p (PMetavar n) = text "?" <> pretty n
968+ prettySe p (PReturn f) = text "return"
969+ prettySe p PImpossible = text "impossible"
970+ prettySe p Placeholder = text "_"
971+ prettySe p (PDoBlock _) = text "do block pretty not implemented"
972+ prettySe p (PElabError s) = pretty s
973+
974+ prettySe p _ = text "test"
975+
976+ prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)
977+ prettyArgS (PExp _ _ tm) = prettyArgSe tm
978+ prettyArgS (PConstraint _ _ tm) = prettyArgSc tm
979+ prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)
980+
981+ prettyArgSe arg = prettySe 0 arg
982+ prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
983+ prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
984+ prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
985+
986+ bracket outer inner doc
987+ | inner > outer = lparen <> doc <> rparen
988+ | otherwise = doc
989+
768showImp :: Bool -> PTerm -> String
990showImp :: Bool -> PTerm -> String
769showImp impl tm = se 10 tm where
991showImp impl tm = se 10 tm where
770 se p (PQuote r) = "![" ++ show r ++ "]"
992 se p (PQuote r) = "![" ++ show r ++ "]"
@@ -846,6 +1068,66 @@ showImp impl tm = se 10 tm where
846 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1068 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
847 | otherwise = str
1069 | otherwise = str
848
1070
1071+{-
1072+ PQuote Raw
1073+ | PRef FC Name
1074+ | PLam Name PTerm PTerm
1075+ | PPi Plicity Name PTerm PTerm
1076+ | PLet Name PTerm PTerm PTerm
1077+ | PTyped PTerm PTerm -- term with explicit type
1078+ | PApp FC PTerm [PArg]
1079+ | PCase FC PTerm [(PTerm, PTerm)]
1080+ | PTrue FC
1081+ | PFalse FC
1082+ | PRefl FC
1083+ | PResolveTC FC
1084+ | PEq FC PTerm PTerm
1085+ | PPair FC PTerm PTerm
1086+ | PDPair FC PTerm PTerm PTerm
1087+ | PAlternative [PTerm]
1088+ | PHidden PTerm -- irrelevant or hidden pattern
1089+ | PSet
1090+ | PConstant Const
1091+ | Placeholder
1092+ | PDoBlock [PDo]
1093+ | PIdiom FC PTerm
1094+ | PReturn FC
1095+ | PMetavar Name
1096+ | PProof [PTactic]
1097+ | PTactics [PTactic] -- as PProof, but no auto solving
1098+ | PElabError Err -- error to report on elaboration
1099+ | PImpossible -- special case for declaring when an LHS can't typecheck
1100+-}
1101+
1102+instance Sized PTerm where
1103+ size (PQuote rawTerm) = size rawTerm
1104+ size (PRef fc name) = size name
1105+ size (PLam name ty bdy) = 1 + size ty + size bdy
1106+ size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1107+ size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1108+ size (PTyped trm ty) = 1 + size trm + size ty
1109+ size (PApp fc name args) = 1 + size args
1110+ size (PCase fc trm bdy) = 1 + size trm + size bdy
1111+ size (PTrue fc) = 1
1112+ size (PFalse fc) = 1
1113+ size (PRefl fc) = 1
1114+ size (PResolveTC fc) = 1
1115+ size (PEq fc left right) = 1 + size left + size right
1116+ size (PPair fc left right) = 1 + size left + size right
1117+ size (PDPair fs left ty right) = 1 + size left + size ty + size right
1118+ size (PAlternative alts) = 1 + size alts
1119+ size (PHidden hidden) = size hidden
1120+ size PSet = 1
1121+ size (PConstant const) = 1 + size const
1122+ size Placeholder = 1
1123+ size (PDoBlock dos) = 1 + size dos
1124+ size (PIdiom fc term) = 1 + size term
1125+ size (PReturn fc) = 1
1126+ size (PMetavar name) = 1
1127+ size (PProof tactics) = size tactics
1128+ size (PElabError err) = size err
1129+ size PImpossible = 1
1130+
849allNamesIn :: PTerm -> [Name]
1131allNamesIn :: PTerm -> [Name]
850allNamesIn tm = nub $ ni [] tm
1132allNamesIn tm = nub $ ni [] tm
851 where
1133 where
src/Idris/Prover.hs+43−23
@@ -17,6 +17,8 @@ import Idris.DataOpts
17import System.Console.Haskeline
17import System.Console.Haskeline
18import Control.Monad.State
18import Control.Monad.State
19
19
20+import Util.Pretty
21+
20prover :: Bool -> Name -> Idris ()
22prover :: Bool -> Name -> Idris ()
21prover lit x =
23prover lit x =
22 do ctxt <- getContext
24 do ctxt <- getContext
@@ -55,31 +57,49 @@ elabStep st e = do case runStateT e st of
55 OK (a, st') -> return (a, st')
57 OK (a, st') -> return (a, st')
56 Error a -> do i <- get
58 Error a -> do i <- get
57 fail (pshow i a)
59 fail (pshow i a)
58−
60+
59dumpState :: IState -> ProofState -> IO ()
61dumpState :: IState -> ProofState -> IO ()
60−dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"
62+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =
63+ putStrLn . render $ pretty nm <> colon <+> text "No more goals."
61−dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)
64+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do
62− = do let OK ty = goalAtFocus ps
65+ let OK ty = goalAtFocus ps
63− let OK env = envAtFocus ps
66+ let OK env = envAtFocus ps
64−-- putStrLn $ "Other goals: " ++ show hs ++ "\n"
67+ putStrLn . render $
65− putStr $ "\n" ++ showPs (reverse env)
68+ prettyOtherGoals hs $$
66− putStrLn $ "---------------------------------- (" ++ show nm
69+ prettyAssumptions env $$
67− ++ ") --------"
70+ prettyGoal ty
68− putStrLn $ show h ++ " : " ++ showG ty ++ "\n"
69 where
71 where
72+ -- XXX
70− tshow t = show (delab ist t)
73+ tPretty t = pretty $ delab ist t
71−
74+
72− showPs [] = ""
75+ prettyPs [] = empty
73− showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs
76+ prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs
74− showPs ((n, Let t v) : bs)
77+ prettyPs ((n, Let t v) : bs) =
75− = " " ++ show n ++ " = " ++ tshow v ++ " : " ++
78+ nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
76− tshow t ++ "\n" ++ showPs bs
79+ tPretty t $$ prettyPs bs)
77− showPs ((n, b) : bs)
80+ prettyPs ((n, b) : bs) =
78− = " " ++ show n ++ " : " ++
81+ pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
79− tshow (binderTy b) ++ "\n" ++ showPs bs
82+
80−
83+ prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
81− showG (Guess t v) = tshow t ++ " =?= " ++ tshow v
82− showG b = tshow (binderTy b)
84+ prettyG b = tPretty $ binderTy b
85+
86+ prettyGoal ty =
87+ text "---------- Goal: ----------" $$
88+ pretty h <> colon $$ nest nestingSize (prettyG ty)
89+
90+ prettyAssumptions env =
91+ if length env == 0 then
92+ empty
93+ else
94+ text "---------- Assumptions: ----------" $$
95+ nest nestingSize (prettyPs $ reverse env)
96+
97+ prettyOtherGoals hs =
98+ if length hs == 0 then
99+ empty
100+ else
101+ text "---------- Other goals: ----------" $$
102+ pretty hs
83
103
84lifte :: ElabState [PDecl] -> ElabD a -> Idris a
104lifte :: ElabState [PDecl] -> ElabD a -> Idris a
85lifte st e = do (v, _) <- elabStep st e
105lifte st e = do (v, _) <- elabStep st e
src/Util/Pretty.hsnew file+33
@@ -0,0 +1,33 @@
1+module Util.Pretty (
2+ module Text.PrettyPrint.HughesPJ,
3+ Sized(..), breakingSize, nestingSize,
4+ Pretty(..)
5+) where
6+
7+import Text.PrettyPrint.HughesPJ
8+
9+-- A rough notion of size for pretty printing various types.
10+class Sized a where
11+ size :: a -> Int
12+
13+instance (Sized a, Sized b) => Sized (a, b) where
14+ size (left, right) = 1 + size left + size right
15+
16+instance Sized a => Sized [a] where
17+ size = sum . map size
18+
19+-- The maximum size before we break on to another line.
20+breakingSize :: Int
21+breakingSize = 15
22+
23+nestingSize :: Int
24+nestingSize = 1
25+
26+class Pretty a where
27+ pretty :: a -> Doc
28+
29+instance Pretty () where
30+ pretty () = text "()"
31+
32+instance Pretty a => Pretty [a] where
33+ pretty l = foldr ($$) empty $ map pretty l