packages feed

idris 0.9.2 → 0.9.2.1

raw patch · 18 files changed

+621/−45 lines, 18 filesdep +pretty

Dependencies added: pretty

Files

idris.cabal view
@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.2+Version:        0.9.2.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -63,11 +63,13 @@                               Idris.Coverage, Idris.IBC, Idris.Unlit,                               Idris.DataOpts, Idris.Transforms, Idris.DSL,  +                              Util.Pretty,+                               Paths_idris                 Build-depends:   base>=4 && <5, parsec, mtl, Cabal, haskeline,                                 containers, process, transformers, filepath, directory,-                                binary, bytestring, epic>=0.9.3+                                binary, bytestring, epic>=0.9.3, pretty                                                 Extensions:      MultiParamTypeClasses, FunctionalDependencies,                                 FlexibleInstances, TemplateHaskell
lib/builtins.idr view
@@ -192,7 +192,7 @@       else compare xr yr  -class Eq a => Num a where +class Num a where      (+) : a -> a -> a     (-) : a -> a -> a     (*) : a -> a -> a
lib/prelude/heap.idr view
@@ -30,6 +30,15 @@ size Empty          = O size (Node s l e r) = s +isValidHeap : Ord a => MaxiphobicHeap a -> Bool+isValidHeap Empty          = True+isValidHeap (Node s l e r) =+  dominates e l && dominates e r && s == S (size l + size r)+  where+    dominates : Ord a => a -> MaxiphobicHeap a -> Bool+    dominates e Empty           = True+    dominates e (Node s l e' r) = e' <= e+ -------------------------------------------------------------------------------- -- Basic heaps --------------------------------------------------------------------------------@@ -140,6 +149,23 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O isEmptySizeZero Empty          p = refl isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd++total emptyHeapValid : Ord a => isValidHeap empty = True+emptyHeapValid = refl++total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True+singletonHeapValid e = refl++{-+total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->+  (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->+  (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True+mergePreservesValidHeaps Empty              Empty              lp rp = refl+mergePreservesValidHeaps Empty              (Node rs rl re rr) lp rp = rp+mergePreservesValidHeaps (Node ls ll le lr) Empty              lp rp = lp+mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =+  ?mergePreservesValidHeapsBody+-}  -------------------------------------------------------------------------------- -- Proofs
lib/prelude/list.idr view
@@ -8,7 +8,7 @@  %access public -infixr 10 :: +infixr 7 ::   data List a   = Nil
lib/prelude/vect.idr view
@@ -6,7 +6,7 @@  %access public -infixr 10 :: +infixr 7 ::   data Vect : Set -> Nat -> Set where   Nil  : Vect a O@@ -67,6 +67,7 @@ -- Building bigger vectors -------------------------------------------------------------------------------- +total (++) : Vect a m -> Vect a n -> Vect a (m + n) (++) []      ys = ys (++) (x::xs) ys = x :: xs ++ ys
src/Core/Elaborate.hs view
@@ -21,6 +21,8 @@ import Data.List import Debug.Trace +import Util.Pretty+ -- I don't really want this here, but it's useful for the test shell data Command = Theorem Name Raw              | Eval Raw@@ -30,6 +32,7 @@  data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))   deriving Show+ type Elab' aux a = StateT (ElabState aux) TC a type Elab a = Elab' () a
src/Core/Evaluate.hs view
@@ -80,6 +80,7 @@ threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking                  -- in fact it's a maximum recursion depth +-- Normalise fully type checked terms (so, assume all names/let bindings resolved) normaliseC :: Context -> Env -> TT Name -> TT Name normaliseC ctxt env t     = evalState (do val <- eval ctxt threshold [] env t []
src/Core/ProofShell.hs view
@@ -11,6 +11,8 @@ import Control.Monad.State import System.Console.Haskeline +import Util.Pretty+ data ShellState = ShellState                          { ctxt     :: Context,                           prf      :: Maybe ProofState,@@ -56,7 +58,7 @@ runShell :: ShellState -> InputT IO ShellState runShell st = do (prompt, parser) <-                             maybe (return ("TT# ", parseCommand)) -                                 (\st -> do outputStrLn (show st)+                                 (\st -> do outputStrLn . render . pretty $ st                                             return (show (thname st) ++ "# ", parseTactic))                                   (prf st)                  x <- getInputLine prompt
src/Core/ProofState.hs view
@@ -13,10 +13,12 @@ import Core.Unify  import Control.Monad.State-import Control.Applicative+import Control.Applicative hiding (empty) import Data.List import Debug.Trace +import Util.Pretty+ data ProofState = PS { thname   :: Name,                        holes    :: [Name], -- holes still to be solved                        nextname :: Int,    -- name supply@@ -93,6 +95,45 @@                showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++                                           " =?= " ++ showEnv ps v                showG ps b = showEnv ps (binderTy b)++instance Pretty ProofState where+  pretty (PS nm [] _ trm _ _ _ _ _ _ _ _ _ _ _) =+    if size nm > breakingSize then+      pretty nm <> colon $$ nest nestingSize (text " no more goals.")+    else+      pretty nm <> colon <+> text " no more goals."+  pretty p@(PS nm (h:hs) _ tm _ _ _ _ _ i _ _ ctxt _ _) =+    let OK g  = goal (Just h) tm in+    let wkEnv = premises g in+      text "Other goals" <+> colon <+> pretty hs $$+      prettyPs wkEnv (reverse wkEnv) $$+      text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$+      pretty h <+> colon <+> prettyGoal wkEnv (goalType g)+    where+      prettyGoal ps (Guess t v) =+        if size v > breakingSize then+          prettyEnv ps t <+> text "=?=" $$+            nest nestingSize (prettyEnv ps v)+        else +          prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v+      prettyGoal ps b = prettyEnv ps $ binderTy b++      prettyPs env [] = empty+      prettyPs env ((n, Let t v):bs) =+        nest nestingSize (pretty n <+> colon <+>+          if size v > breakingSize then+            prettyEnv env t <+> text "=" $$+              nest nestingSize (prettyEnv env v) $$+                nest nestingSize (prettyPs env bs)+          else+            prettyEnv env t <+> text "=" <+> prettyEnv env v $$+              nest nestingSize (prettyPs env bs))+      prettyPs env ((n, b):bs) =+        if size (binderTy b) > breakingSize then+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)+        else+          nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$+            nest nestingSize (prettyPs env bs))  same Nothing n  = True same (Just x) n = x == n
src/Core/TT.hs view
@@ -10,6 +10,8 @@ import qualified Data.Binary as B import Data.Binary hiding (get, put) +import Util.Pretty hiding (Str)+ {- The language has:    * Full dependent types    * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...@@ -34,6 +36,9 @@ deriving instance Binary FC  !-} +instance Sized FC where+  size (FC f l) = 1 + length f+ instance Show FC where     show (FC f l) = f ++ ":" ++ show l @@ -48,6 +53,17 @@          | At FC Err   deriving Eq +instance Sized Err where+  size (Msg msg) = length msg+  size (CantUnify left right err score) = size left + size right + size err+  size (NoSuchVariable name) = size name+  size (NotInjective l c r) = size l + size c + size r+  size (CantResolve trm) = size trm+  size (IncompleteTerm trm) = size trm+  size UniverseError = 1+  size ProgramLineComment = 1+  size (At fc err) = size fc + size err+ score :: Err -> Int score (CantUnify _ _ m s) = s + score m score (CantResolve _) = 20@@ -60,10 +76,30 @@                                ++ show e ++ " " ++ show i     show _ = "Error" +instance Pretty Err where+  pretty (Msg m) = text m+  pretty (CantUnify l r e i) =+    if size l + size r > breakingSize then+      text "Cannot unify" <+> colon $$+        nest nestingSize (pretty l <+> text "and" <+> pretty r) $$+        nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))+    else+      text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$+        nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))+  pretty _ = text "Error"+ data TC a = OK a           | Error Err   deriving (Eq, Functor) +instance Pretty a => Pretty (TC a) where+  pretty (OK ok) = pretty ok+  pretty (Error err) =+    if size err > breakingSize then+      text "Error" <+> colon $$ (nest nestingSize $ pretty err)+    else+      text "Error" <+> colon <+> pretty err+ instance Show a => Show (TC a) where     show (OK x) = show x     show (Error str) = "Error: " ++ show str@@ -118,6 +154,16 @@ deriving instance Binary Name  !-} +instance Sized Name where+  size (UN n)     = 1+  size (NS n els) = 1 + length els+  size (MN i n) = 1++instance Pretty Name where+  pretty (UN n) = text n+  pretty (NS n s) = pretty n+  pretty (MN i s) = lbrace <+> text s <+> (text . show $ i) <+> rbrace+ instance Show Name where     show (UN n) = n     show (NS n s) = showSep "." (reverse s) ++ "." ++ show n@@ -190,6 +236,23 @@ deriving instance Binary Const  !-} +instance Sized Const where+  size _ = 1++instance Pretty Const where+  pretty (I i) = text . show $ i+  pretty (BI i) = text . show $ i+  pretty (Fl f) = text . show $ f+  pretty (Ch c) = text . show $ c+  pretty (Str s) = text s+  pretty IType = text "Int"+  pretty BIType = text "BigInt"+  pretty FlType = text "Float"+  pretty ChType = text "Char"+  pretty StrType = text "String"+  pretty PtrType = text "Ptr"+  pretty Forgot = text "Forgot"+ data Raw = Var Name          | RBind Name (Binder Raw) Raw          | RApp Raw Raw@@ -197,6 +260,18 @@          | RForce Raw          | RConstant Const   deriving (Show, Eq)++instance Sized Raw where+  size (Var name) = 1+  size (RBind name bind right) = 1 + size bind + size right+  size (RApp left right) = 1 + size left + size right+  size RSet = 1+  size (RForce raw) = 1 + size raw+  size (RConstant const) = size const++instance Pretty Raw where+  pretty = text . show+ {-!  deriving instance Binary Raw  !-}@@ -218,6 +293,17 @@ deriving instance Binary Binder  !-} +instance Sized a => Sized (Binder a) where+  size (Lam ty) = 1 + size ty+  size (Pi ty) = 1 + size ty+  size (Let ty val) = 1 + size ty + size val+  size (NLet ty val) = 1 + size ty + size val+  size (Hole ty) = 1 + size ty+  size (GHole ty) = 1 + size ty+  size (Guess ty val) = 1 + size ty + size val+  size (PVar ty) = 1 + size ty+  size (PVTy ty) = 1 + size ty+ fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b) fmapMB f (Let t v)   = liftM2 Let (f t) (f v) fmapMB f (NLet t v)  = liftM2 NLet (f t) (f v)@@ -259,6 +345,9 @@           | UVal Int -- explicit universe level   deriving (Eq, Ord) +instance Sized UExp where+  size _ = 1+ -- We assume that universe levels have been checked, so anything external -- can just have the same universe variable and we won't get any new -- cycles.@@ -289,6 +378,12 @@ deriving instance Binary NameType  !-} +instance Sized NameType where+  size _ = 1++instance Pretty NameType where+  pretty = text . show+ instance Eq NameType where     Bound    == Bound    = True     Ref      == Ref      = True@@ -308,6 +403,18 @@ deriving instance Binary TT  !-} +instance Sized a => Sized (TT a) where+  size (P name n trm) = 1 + size name + size n + size trm+  size (V v) = 1+  size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy+  size (App l r) = 1 + size l + size r+  size (Constant c) = size c+  size Erased = 1+  size (Set u) = 1 + size u++instance Pretty a => Pretty (TT a) where+  pretty _ = text "test"+ type EnvTT n = [(n, Binder (TT n))]  data Datatype n = Data { d_typename :: n,@@ -495,6 +602,54 @@  showEnv env t = showEnv' env t False showEnvDbg env t = showEnv' env t True++prettyEnv env t = prettyEnv' env t False+  where+    prettyEnv' env t dbg = prettySe 10 env t dbg++    bracket outer inner p+      | inner > outer = lparen <> p <> rparen+      | otherwise     = p++    prettySe p env (P nt n t) debug =+      pretty n <+> +        if debug then+          lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack+        else+          empty+    prettySe p env (V i) debug+      | i < length env =+        if debug then+          text . show . fst $ env!!i+        else+          lbrack <+> text (show i) <+> rbrack+      | otherwise      = text "unbound" <+> text (show i) <+> text "!"+    prettySe p env (Bind n b@(Pi t) sc) debug+      | noOccurrence n sc && not debug =+          bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug+    prettySe p env (Bind n b sc) debug =+      bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug+    prettySe p env (App f a) debug =+      bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug+    prettySe p env (Constant c) debug = pretty c+    prettySe p env Erased debug = text "[_]"+    prettySe p env (Set i) debug = text "Set" <+> (text . show $ i)++    prettySb env n (Lam t) = prettyB env "λ" "=>" n t+    prettySb env n (Hole t) = prettyB env "?defer" "." n t+    prettySb env n (Pi t) = prettyB env "(" ") ->" n t+    prettySb env n (PVar t) = prettyB env "pat" "." n t+    prettySb env n (PVTy t) = prettyB env "pty" "." n t+    prettySb env n (Let t v) = prettyBv env "let" "in" n t v+    prettySb env n (Guess t v) = prettyBv env "??" "in" n t v++    prettyB env op sc n t debug =+      text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc++    prettyBv env op sc n t v debug =+      text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>+        prettySe 10 env v debug <> text sc+            showEnv' env t dbg = se 10 env t where     se p env (P nt n t) = show n
src/Idris/AbsSyntax.hs view
@@ -5,18 +5,23 @@  import Core.TT import Core.Evaluate-import Core.Elaborate+import Core.Elaborate hiding (Tactic(..)) import Core.Typecheck  import System.Console.Haskeline+ import Control.Monad.State+ import Data.List import Data.Char import Data.Either+ import Debug.Trace  import qualified Epic.Epic as E +import Util.Pretty+ data IOption = IOption { opt_logLevel :: Int,                          opt_typecase :: Bool,                          opt_typeintype :: Bool,@@ -571,6 +576,26 @@ deriving instance Binary PTactic'  !-} +instance Sized a => Sized (PTactic' a) where+  size (Intro nms) = 1 + size nms+  size Intros = 1+  size (Focus nm) = 1 + size nm+  size (Refine nm bs) = 1 + size nm + length bs+  size (Rewrite t) = 1 + size t+  size (LetTac nm t) = 1 + size nm + size t+  size (Exact t) = 1 + size t+  size Compute = 1+  size Trivial = 1+  size Solve = 1+  size Attack = 1+  size ProofState = 1+  size ProofTerm = 1+  size Undo = 1+  size (Try l r) = 1 + size l + size r+  size (TSeq l r) = 1 + size l + size r+  size Qed = 1+  size Abandon = 1+ type PTactic = PTactic' PTerm  data PDo' t = DoExp  FC t@@ -583,6 +608,13 @@ deriving instance Binary PDo'  !-} +instance Sized a => Sized (PDo' a) where+  size (DoExp fc t) = 1 + size fc + size t+  size (DoBind fc nm t) = 1 + size fc + size nm + size t+  size (DoBindP fc l r) = 1 + size fc + size l + size r+  size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r+  size (DoLetP fc l r) = 1 + size fc + size l + size r+ type PDo = PDo' PTerm  -- The priority gives a hint as to elaboration order. Best to elaborate@@ -600,6 +632,13 @@                               getScript :: t,                               getTm :: t }     deriving (Show, Eq, Functor)++instance Sized a => Sized (PArg' a) where+  size (PImp p l nm trm) = 1 + size nm + size trm+  size (PExp p l trm) = 1 + size trm+  size (PConstraint p l trm) = 1 + size trm+  size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm+ {-!  deriving instance Binary PArg'  !-}@@ -712,6 +751,9 @@ instance Show PTerm where     show tm = showImp False tm +instance Pretty PTerm where+  pretty = prettyImp False+ instance Show PDecl where     show d = showDeclImp False d @@ -765,6 +807,186 @@ getAll :: [PArg] -> [PTerm] getAll = map getTm  +prettyImp :: Bool -> PTerm -> Doc+prettyImp impl = prettySe 10+  where+    prettySe p (PQuote r) =+      if size r > breakingSize then+        text "![" $$ pretty r <> text "]"+      else+        text "![" <> pretty r <> text "]"+    prettySe p (PRef fc n) =+      if impl then+        pretty n+      else+        prettyBasic n+      where+        prettyBasic n@(UN _) = pretty n+        prettyBasic (MN _ s) = text s+        prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map text $ reverse s))) <> prettyBasic n+    prettySe p (PLam n ty sc) =+      bracket p 2 $+        if size sc > breakingSize then+          text "λ" <> pretty n <+> text "=>" $+$ pretty sc+        else+          text "λ" <> pretty n <+> text "=>" <+> pretty sc+    prettySe p (PLet n ty v sc) =+      bracket p 2 $+        if size sc > breakingSize then+          text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$+            nest nestingSize (prettySe 10 sc)+        else+          text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>+            prettySe 10 sc+    prettySe p (PPi (Exp l s) n ty sc)+      | n `elem` allNamesIn sc || impl =+          let open = if l then text "|" <> lparen else lparen in+            bracket p 2 $+              if size sc > breakingSize then+                open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>+                  st <+> text "->" $+$ prettySe 10 sc+              else+                open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>+                  st <+> text "->" <+> prettySe 10 sc+      | otherwise                      =+          bracket p 2 $+            if size sc > breakingSize then+              prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc+            else+              prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc+      where+        st =+          case s of+            Static -> text "[static]"+            _      -> empty+    prettySe p (PPi (Imp l s) n ty sc)+      | impl =+          let open = if l then text "|" <> lbrace else lbrace in+            bracket p 2 $+              if size sc > breakingSize then+                open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>+                  st <+> text "->" <+> prettySe 10 sc+              else+                open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>+                  st <+> text "->" <+> prettySe 10 sc+      | otherwise = prettySe 10 sc+      where+        st =+          case s of+            Static -> text $ "[static]"+            _      -> empty+    prettySe p (PPi (Constraint _ _) n ty sc) =+      bracket p 2 $+        if size sc > breakingSize then+          prettySe 10 ty <+> text "=>" <+> prettySe 10 sc+        else+          prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc+    prettySe p (PPi (TacImp _ _ s) n ty sc) =+      bracket p 2 $+        if size sc > breakingSize then+          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>+            rbrace <+> text "->" $+$ prettySe 10 sc+        else+          lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>+            rbrace <+> text "->" <+> prettySe 10 sc+    prettySe p (PApp _ (PRef _ f) [])+      | not impl = pretty f+    prettySe p (PApp _ (PRef _ op@(UN (f:_))) args)+      | length (getExps args) == 2 && (not impl) && (not $ isAlpha f) =+          let [l, r] = getExps args in+            bracket p 1 $+              if size r > breakingSize then+                prettySe 1 l <+> pretty op $+$ prettySe 0 r+              else+                prettySe 1 l <+> pretty op <+> prettySe 0 r+    prettySe p (PApp _ f as) =+      let args = getExps as in+        bracket p 1 $+          prettySe 1 f <+>+            if impl then+              foldl fS empty as+              -- foldr (<+>) empty $ map prettyArgS as+            else+              foldl fSe empty args+              -- foldr (<+>) empty $ map prettyArgSe args+      where+        fS l r =+          if size r > breakingSize then+            l $+$ nest nestingSize (prettyArgS r)+          else+            l <+> prettyArgS r++        fSe l r =+          if size r > breakingSize then+            l $+$ nest nestingSize (prettyArgSe r)+          else+            l <+> prettyArgSe r+    prettySe p (PCase _ scr opts) =+      text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody+      where+        prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts++        sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r+    prettySe p (PHidden tm) = text "." <> prettySe 0 tm+    prettySe p (PRefl _) = text "refl"+    prettySe p (PResolveTC _) = text "resolvetc"+    prettySe p (PTrue _) = text "()"+    prettySe p (PFalse _) = text "_|_"+    prettySe p (PEq _ l r) =+      bracket p 2 $+        if size r > breakingSize then+          prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)+        else+          prettySe 10 l <+> text "=" <+> prettySe 10 r+    prettySe p (PTyped l r) =+      lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen+    prettySe p (PPair _ l r) =+      if size r > breakingSize then+        lparen <> prettySe 10 l <> text "," $+$+          prettySe 10 r <> rparen+      else+        lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen+    prettySe p (PDPair _ l t r) =+      if size r > breakingSize then+        lparen <> prettySe 10 l <+> text "**" $+$+          prettySe 10 r <> rparen+      else+        lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen+    prettySe p (PAlternative as) =+      lparen <> text "|" <> prettyAs <> text "|" <> rparen+        where+          prettyAs =+            foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as+    prettySe p PSet = text "Set"+    prettySe p (PConstant c) = pretty c+    -- XXX: add pretty for tactics+    prettySe p (PProof ts) =+      text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace+    prettySe p (PTactics ts) =+      text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace+    prettySe p (PMetavar n) = text "?" <> pretty n+    prettySe p (PReturn f) = text "return"+    prettySe p PImpossible = text "impossible"+    prettySe p Placeholder = text "_"+    prettySe p (PDoBlock _) = text "do block pretty not implemented"+    prettySe p (PElabError s) = pretty s++    prettySe p _ = text "test"++    prettyArgS (PImp _ _ n tm) = prettyArgSi (n, tm)+    prettyArgS (PExp _ _ tm)   = prettyArgSe tm+    prettyArgS (PConstraint _ _ tm) = prettyArgSc tm+    prettyArgS (PTacImplicit _ _ n _ tm) = prettyArgSti (n, tm)++    prettyArgSe arg = prettySe 0 arg+    prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace+    prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace+    prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace++    bracket outer inner doc+      | inner > outer = lparen <> doc <> rparen+      | otherwise     = doc+         showImp :: Bool -> PTerm -> String showImp impl tm = se 10 tm where     se p (PQuote r) = "![" ++ show r ++ "]"@@ -773,7 +995,9 @@       where showbasic n@(UN _) = show n             showbasic (MN _ s) = s             showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n-    se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc+    se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ +                            (if impl then " : " ++ se 10 ty else "") ++ " => " +                            ++ se 10 sc     se p (PLet n ty v sc) = bracket p 2 $ "let " ++ show n ++ " = " ++ se 10 v ++                             " in " ++ se 10 sc      se p (PPi (Exp l s) n ty sc)@@ -845,6 +1069,66 @@      bracket outer inner str | inner > outer = "(" ++ str ++ ")"                             | otherwise = str++{-+ PQuote Raw+           | PRef FC Name+           | PLam Name PTerm PTerm+           | PPi  Plicity Name PTerm PTerm+           | PLet Name PTerm PTerm PTerm +           | PTyped PTerm PTerm -- term with explicit type+           | PApp FC PTerm [PArg]+           | PCase FC PTerm [(PTerm, PTerm)]+           | PTrue FC+           | PFalse FC+           | PRefl FC+           | PResolveTC FC+           | PEq FC PTerm PTerm+           | PPair FC PTerm PTerm+           | PDPair FC PTerm PTerm PTerm+           | PAlternative [PTerm]+           | PHidden PTerm -- irrelevant or hidden pattern+           | PSet+           | PConstant Const+           | Placeholder+           | PDoBlock [PDo]+           | PIdiom FC PTerm+           | PReturn FC+           | PMetavar Name+           | PProof [PTactic]+           | PTactics [PTactic] -- as PProof, but no auto solving+           | PElabError Err -- error to report on elaboration+           | PImpossible -- special case for declaring when an LHS can't typecheck+-}++instance Sized PTerm where+  size (PQuote rawTerm) = size rawTerm+  size (PRef fc name) = size name+  size (PLam name ty bdy) = 1 + size ty + size bdy+  size (PPi plicity name ty bdy) = 1 + size ty + size bdy+  size (PLet name ty def bdy) = 1 + size ty + size def + size bdy+  size (PTyped trm ty) = 1 + size trm + size ty+  size (PApp fc name args) = 1 + size args+  size (PCase fc trm bdy) = 1 + size trm + size bdy+  size (PTrue fc) = 1+  size (PFalse fc) = 1+  size (PRefl fc) = 1+  size (PResolveTC fc) = 1+  size (PEq fc left right) = 1 + size left + size right+  size (PPair fc left right) = 1 + size left + size right+  size (PDPair fs left ty right) = 1 + size left + size ty + size right+  size (PAlternative alts) = 1 + size alts+  size (PHidden hidden) = size hidden+  size PSet = 1+  size (PConstant const) = 1 + size const+  size Placeholder = 1+  size (PDoBlock dos) = 1 + size dos+  size (PIdiom fc term) = 1 + size term+  size (PReturn fc) = 1+  size (PMetavar name) = 1+  size (PProof tactics) = size tactics+  size (PElabError err) = size err+  size PImpossible = 1  allNamesIn :: PTerm -> [Name] allNamesIn tm = nub $ ni [] tm
src/Idris/Delaborate.hs view
@@ -47,8 +47,10 @@     deFn env (P _ n _) [l,r]     | n == pairTy  = PPair un (de env l) (de env r)                                  | n == eqCon   = PRefl un                                  | n == UN "lazy" = de env r-                                 | n == UN "Exists" = PDPair un (de env l) Placeholder-                                                                (de env r)+    deFn env (P _ n _) [ty, Bind x (Lam _) r]+                                 | n == UN "Exists" +                                       = PDPair un (PRef un x) (de env ty)+                                                   (de env (instantiate (P Bound x ty) r))     deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)                                  | n == eqTy    = PEq un (de env l) (de env r)                                  | n == UN "Ex_intro" = PDPair un (de env l) Placeholder@@ -71,6 +73,7 @@ pshow i (CantUnify x y e s)      = "Can't unify " ++ show (delab i x)         ++ " with " ++ show (delab i y) +++--         " (" ++ show x ++ " and " ++ show y ++ ") " ++         case e of             Msg "" -> ""             _ -> "\n\nSpecifically:\n\t " ++ pshow i e
src/Idris/ElabDecls.hs view
@@ -207,11 +207,12 @@          mapM_ (elabCaseBlock info) is          ctxt <- getContext          (cty, _)  <- recheckC fc [] t'-         tyIs cty-         logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty+         let cty' = normaliseC ctxt [] cty+         tyIs cty'+         logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'          addIBC (IBCDef n)-         forceArgs n cty-         return (n, cty)+         forceArgs n cty'+         return (n, cty')   where     tyIs (Bind n b sc) = tyIs sc     tyIs t | (P _ n' _, _) <- unApply t @@ -801,6 +802,7 @@           dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as           dappname t = t + pbinds (Bind n (PVar t) sc) = do attack; patbind n                                   pbinds sc pbinds tm = return ()@@ -862,7 +864,6 @@     = do i <- get          put (i { idris_dsls = addDef n dsl (idris_dsls i) })           addIBC (IBCDSL n)- elabDecl' info (PDirective i) = i  elabCaseBlock info d@(PClauses f o n ps)
src/Idris/ElabTerm.hs view
@@ -102,8 +102,12 @@     elab' ina (PFalse fc)    = elab' ina (PRef fc falseTy)     elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes        = resolveTC 5 fn ist-    elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")-                                   instanceArg c+    elab' ina (PResolveTC fc) +        | pattern = do c <- unique_hole (MN 0 "c")+                       instanceArg c+        | otherwise = try (resolveTC 2 fn ist)+                          (do c <- unique_hole (MN 0 "c")+                              instanceArg c)     elab' ina (PRefl fc)     = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,                                                            pimp (MN 0 "x") Placeholder])     elab' ina (PEq fc l r)   = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
src/Idris/Parser.hs view
@@ -1261,8 +1261,8 @@          <|> try (do lchar '%'; reserved "access"; acc <- pAccessibility'                      return [PDirective (do i <- getIState                                             putIState (i { default_access = acc }))])-         <|> do lchar '%'; reserved "logging"; i <- natural;-                return [PDirective (setLogLevel (fromInteger i))] +         <|> try (do lchar '%'; reserved "logging"; i <- natural;+                     return [PDirective (setLogLevel (fromInteger i))])  pTactic :: SyntaxInfo -> IParser PTactic pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
src/Idris/Prover.hs view
@@ -17,6 +17,8 @@ import System.Console.Haskeline import Control.Monad.State +import Util.Pretty+ prover :: Bool -> Name -> Idris () prover lit x =            do ctxt <- getContext@@ -55,31 +57,49 @@                      OK (a, st') -> return (a, st')                      Error a -> do i <- get                                    fail (pshow i a)-                  + dumpState :: IState -> ProofState -> IO ()-dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) = putStrLn $ (show nm) ++ ": no more goals"-dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _)-   = do let OK ty = goalAtFocus ps-        let OK env = envAtFocus ps---         putStrLn $ "Other goals: " ++ show hs ++ "\n"-        putStr $ "\n" ++ showPs (reverse env)-        putStrLn $ "---------------------------------- (" ++ show nm-                     ++ ") --------"-        putStrLn $ show h ++ " : " ++ showG ty ++ "\n"+dumpState ist (PS nm [] _ tm _ _ _ _ _ _ _ _ _ _ _) =+  putStrLn . render $ pretty nm <> colon <+> text "No more goals."+dumpState ist ps@(PS nm (h:hs) _ tm _ _ _ _ problems i _ _ ctxy _ _) = do+  let OK ty  = goalAtFocus ps+  let OK env = envAtFocus ps+  putStrLn . render $+    prettyOtherGoals hs $$+    prettyAssumptions env $$+    prettyGoal ty   where-    tshow t = show (delab ist t)+    -- XXX+    tPretty t = pretty $ delab ist t -    showPs [] = ""-    showPs ((MN _ "rewrite_rule", _) : bs) = showPs bs-    showPs ((n, Let t v) : bs)-        = "  " ++ show n ++ " = " ++ tshow v ++ " : " ++-            tshow t ++ "\n" ++ showPs bs-    showPs ((n, b) : bs)-        = "  " ++ show n ++ " : " ++-            tshow (binderTy b) ++ "\n" ++ showPs bs+    prettyPs [] = empty+    prettyPs ((MN _ "rewrite_rule", _) : bs) = prettyPs bs+    prettyPs ((n, Let t v) : bs) =+      nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>+        tPretty t $$ prettyPs bs)+    prettyPs ((n, b) : bs) = +      pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs -    showG (Guess t v) = tshow t ++ " =?= " ++ tshow v-    showG b = tshow (binderTy b)+    prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v+    prettyG b = tPretty $ binderTy b++    prettyGoal ty =+      text "----------                 Goal:                  ----------" $$+      pretty h <> colon $$ nest nestingSize (prettyG ty)++    prettyAssumptions env =+      if length env == 0 then+        empty+      else+        text "----------              Assumptions:              ----------" $$+        nest nestingSize (prettyPs $ reverse env)++    prettyOtherGoals hs =+      if length hs == 0 then+        empty+      else+        text "----------              Other goals:              ----------" $$+        pretty hs  lifte :: ElabState [PDecl] -> ElabD a -> Idris a lifte st e = do (v, _) <- elabStep st e
src/Idris/REPL.hs view
@@ -151,9 +151,9 @@                        ist <- get                        imp <- impShow                        case lookupTy Nothing n ctxt of-                        [t] -> iputStrLn $ show n ++ " : " ++-                                  showImp imp (delab ist t)-                        _ -> iputStrLn $ "No such variable " ++ show n+                        ts@(_:_) -> mapM_ (\t -> iputStrLn $ show n ++ " : " +++                                                       showImp imp (delab ist t)) ts+                        [] -> iputStrLn $ "No such variable " ++ show n process fn (Check t) = do (tm, ty) <- elabVal toplevel False t                           ctxt <- getContext                           ist <- get @@ -188,7 +188,7 @@                                 [t] -> iputStrLn (showTotal t i)                                 _ -> return () process fn (Info n) = do i <- get-                         let oi = lookupCtxt Nothing n (idris_optimisation i)+                         let oi = lookupCtxtName Nothing n (idris_optimisation i)                          when (not (null oi)) $ iputStrLn (show oi)                          let si = lookupCtxt Nothing n (idris_statics i)                          when (not (null si)) $ iputStrLn (show si)
+ src/Util/Pretty.hs view
@@ -0,0 +1,33 @@+module Util.Pretty (+  module Text.PrettyPrint.HughesPJ,+  Sized(..), breakingSize, nestingSize,+  Pretty(..)+) where++import Text.PrettyPrint.HughesPJ++-- A rough notion of size for pretty printing various types.+class Sized a where+  size :: a -> Int++instance (Sized a, Sized b) => Sized (a, b) where+  size (left, right) = 1 + size left + size right++instance Sized a => Sized [a] where+  size = sum . map size++-- The maximum size before we break on to another line.+breakingSize :: Int+breakingSize = 15++nestingSize :: Int+nestingSize = 1++class Pretty a where+  pretty :: a -> Doc++instance Pretty () where+  pretty () = text "()"++instance Pretty a => Pretty [a] where+  pretty l = foldr ($$) empty $ map pretty l