git.iko.soy/Idris-dev
on master help sign in
Started adding pretty-printing capabilities for core datatypes to improve rendering of proof state.
d254ce1Dominic Mulligan
src/Idris/AbsSyntax.hs+65
compare with master
unifiedsplit
@@ -9,14 +9,19 @@ import Core.Elaborate
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,
@@ -846,6 +851,66 @@ showImp impl tm = se 10 tm where
846 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
851 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
847 | otherwise = str
852 | otherwise = str
848
853
854+{-
855+ PQuote Raw
856+ | PRef FC Name
857+ | PLam Name PTerm PTerm
858+ | PPi Plicity Name PTerm PTerm
859+ | PLet Name PTerm PTerm PTerm
860+ | PTyped PTerm PTerm -- term with explicit type
861+ | PApp FC PTerm [PArg]
862+ | PCase FC PTerm [(PTerm, PTerm)]
863+ | PTrue FC
864+ | PFalse FC
865+ | PRefl FC
866+ | PResolveTC FC
867+ | PEq FC PTerm PTerm
868+ | PPair FC PTerm PTerm
869+ | PDPair FC PTerm PTerm PTerm
870+ | PAlternative [PTerm]
871+ | PHidden PTerm -- irrelevant or hidden pattern
872+ | PSet
873+ | PConstant Const
874+ | Placeholder
875+ | PDoBlock [PDo]
876+ | PIdiom FC PTerm
877+ | PReturn FC
878+ | PMetavar Name
879+ | PProof [PTactic]
880+ | PTactics [PTactic] -- as PProof, but no auto solving
881+ | PElabError Err -- error to report on elaboration
882+ | PImpossible -- special case for declaring when an LHS can't typecheck
883+-}
884+
885+instance Sized PTerm where
886+ size (PQuote rawTerm) = size rawTerm
887+ size (PRef fc name) = size name
888+ size (PLam name ty bdy) = 1 + size ty + size bdy
889+ size (PPi name ty bdy) = 1 + size ty + size bdy
890+ size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
891+ size (PTyped trm ty) = 1 + size trm + size ty
892+ size (PApp fc name args) = 1 + size args
893+ size (PCase fc trm bdy) = 1 + size trm + size bdy
894+ size (PTrue fc) = 1
895+ size (PFalse fc) = 1
896+ size (PRefl fc) = 1
897+ size (PResolveTC fc) = 1
898+ size (PEq fc left right) = 1 + size left + size right
899+ size (PPair fc left right) = 1 + size left + size right
900+ size (PDPair fs left right) = 1 + size left + size right
901+ size (PAlternative alts) = 1 + size alts
902+ size (PHidden hidden) = size hidden
903+ size PSet = 1
904+ size (PConstant const) = 1 + size const
905+ size Placeholder = 1
906+ size (PDoBlock dos) = 1 + size dos
907+ size (PIdiom fc term) = 1 + size term
908+ size (PReturn fc) = 1
909+ size (PMetavar name) = 1
910+ size (PProof tactics) = size tactics
911+ size (PElabError err) = size err
912+ size PImpossible = 1
913+
849allNamesIn :: PTerm -> [Name]
914allNamesIn :: PTerm -> [Name]
850allNamesIn tm = nub $ ni [] tm
915allNamesIn tm = nub $ ni [] tm
851 where
916 where