@@ -10,6 +10,8 @@ import Data.List
1010import qualified Data.Binary as B
1111import Data.Binary hiding (get, put)
1212
13+import Util.Pretty hiding (Str)
14+
1315{- The language has:
1416 * Full dependent types
1517 * A hierarchy of universes, with cumulativity: Set : Set1, Set1 : Set2, ...
@@ -197,6 +199,15 @@ data Raw = Var Name
197199 | RForce Raw
198200 | RConstant Const
199201 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+
200211{-!
201212deriving instance Binary Raw
202213!-}