git.iko.soy/Idris-dev
on master help sign in
Started adding pretty printing capabilities for core data types to improve rendering of proof state.
9a54230Dominic Mulligan
src/Core/TT.hs+11
compare with master
unifiedsplit
@@ -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, ...
@@ -197,6 +199,15 @@ data Raw = Var Name
197 | RForce Raw
199 | RForce Raw
198 | RConstant Const
200 | RConstant Const
199 deriving (Show, Eq)
201 deriving (Show, Eq)
202+
203+instance Sized Raw where
204+ size (Var name) = 1
205+ size (RBind name bind right) = 1 + size bind + size right
206+ size (RApp left right) = 1 + size left + size right
207+ size RSet = 1
208+ size (RForce raw) = 1 + size raw
209+ size (RConstant const) = size const
210+
200{-!
211{-!
201deriving instance Binary Raw
212deriving instance Binary Raw
202!-}
213!-}