
   0 | module Core.TT.Binder
   1 | 
   2 | import Algebra
   3 | 
   4 | import Core.FC
   5 | 
   6 | %default total
   7 | 
   8 | ------------------------------------------------------------------------
   9 | -- Pi information classifies the kind of pi type this is
  10 | 
  11 | public export
  12 | data PiInfo t =
  13 |   ||| Implicit Pi types (e.g. {0 a : Type} -> ...)
  14 |   ||| The argument is to be solved by unification
  15 |   Implicit |
  16 |   ||| Explicit Pi types (e.g. (x : a) -> ...)
  17 |   ||| The argument is to be passed explicitly
  18 |   Explicit |
  19 |   ||| Auto Pi types (e.g. (fun : Functor f) => ...)
  20 |   ||| The argument is to be solved by proof search
  21 |   AutoImplicit |
  22 |   ||| Default Pi types (e.g. {default True flag : Bool} -> ...)
  23 |   ||| The argument is set to the default value if nothing is
  24 |   ||| passed explicitly
  25 |   DefImplicit t
  26 | 
  27 | %name PiInfo pinfo
  28 | 
  29 | namespace PiInfo
  30 | 
  31 |   export
  32 |   isImplicit : PiInfo t -> Bool
  33 |   isImplicit Explicit = False
  34 |   isImplicit _ = True
  35 | 
  36 | ||| Heterogeneous equality, provided an heterogeneous equality
  37 | ||| of default values
  38 | export
  39 | eqPiInfoBy : (t -> u -> Bool) -> PiInfo t -> PiInfo u -> Bool
  40 | eqPiInfoBy eqT = go where
  41 | 
  42 |   go : PiInfo t -> PiInfo u -> Bool
  43 |   go Implicit Implicit = True
  44 |   go Explicit Explicit = True
  45 |   go AutoImplicit AutoImplicit = True
  46 |   go (DefImplicit t) (DefImplicit t') = eqT t t'
  47 |   go _ _ = False
  48 | 
  49 | -- There's few places where we need the default - it's just when checking if
  50 | -- there's a default during elaboration - so often it's easier just to erase it
  51 | -- to a normal implicit
  52 | export
  53 | forgetDef : PiInfo t -> PiInfo t'
  54 | forgetDef Explicit = Explicit
  55 | forgetDef Implicit = Implicit
  56 | forgetDef AutoImplicit = AutoImplicit
  57 | forgetDef (DefImplicit t) = Implicit
  58 | 
  59 | export
  60 | Show t => Show (PiInfo t) where
  61 |   show Implicit = "Implicit"
  62 |   show Explicit = "Explicit"
  63 |   show AutoImplicit = "AutoImplicit"
  64 |   show (DefImplicit t) = "DefImplicit " ++ show t
  65 | 
  66 | export
  67 | Eq t => Eq (PiInfo t) where
  68 |   (==) = eqPiInfoBy (==)
  69 | ------------------------------------------------------------------------
  70 | -- A bound value
  71 | 
  72 | ||| A bound value along with its `PiInfo`.
  73 | ||| We cannot use `PiInfo` as metadata for `WithData` because the record is functorial in both
  74 | ||| `t` and `PiInfo`.
  75 | public export
  76 | record PiBindData (t : Type) where
  77 |   constructor MkPiBindData
  78 |   info : PiInfo t
  79 |   boundType : t
  80 | 
  81 | public export
  82 | mapType : (t -> t) -> PiBindData t -> PiBindData t
  83 | mapType f = {boundType $= f}
  84 | 
  85 | export
  86 | Show t => Show (PiBindData t) where
  87 |   show bind = show bind.info ++ ", " ++ show bind.boundType
  88 | ------------------------------------------------------------------------
  89 | -- Different types of binders we may encounter
  90 | 
  91 | public export
  92 | data Binder : Type -> Type where
  93 |      -- Lambda bound variables with their implicitness
  94 |      Lam : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
  95 |      -- Let bound variables with their value
  96 |      Let : FC -> RigCount -> (val : type) -> (ty : type) -> Binder type
  97 |      -- Forall/pi bound variables with their implicitness
  98 |      Pi : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
  99 |      -- pattern bound variables. The PiInfo gives the implicitness at the
 100 |      -- point it was bound (Explicit if it was explicitly named in the
 101 |      -- program)
 102 |      PVar : FC -> RigCount -> PiInfo type -> (ty : type) -> Binder type
 103 |      -- variable bound for an as pattern (Like a let, but no computational
 104 |      -- force, and only used on the lhs. Converted to a let on the rhs because
 105 |      -- we want the computational behaviour.)
 106 |      PLet : FC -> RigCount -> (val : type) -> (ty : type) -> Binder type
 107 |      -- the type of pattern bound variables
 108 |      PVTy : FC -> RigCount -> (ty : type) -> Binder type
 109 | 
 110 | %name Binder bd
 111 | 
 112 | export
 113 | isLet : Binder t -> Bool
 114 | isLet (Let {}) = True
 115 | isLet _ = False
 116 | 
 117 | export
 118 | binderLoc : Binder tm -> FC
 119 | binderLoc (Lam fc _ x ty) = fc
 120 | binderLoc (Let fc _ val ty) = fc
 121 | binderLoc (Pi fc _ x ty) = fc
 122 | binderLoc (PVar fc _ p ty) = fc
 123 | binderLoc (PLet fc _ val ty) = fc
 124 | binderLoc (PVTy fc _ ty) = fc
 125 | 
 126 | export
 127 | binderType : Binder tm -> tm
 128 | binderType (Lam _ _ x ty) = ty
 129 | binderType (Let _ _ val ty) = ty
 130 | binderType (Pi _ _ x ty) = ty
 131 | binderType (PVar _ _ _ ty) = ty
 132 | binderType (PLet _ _ val ty) = ty
 133 | binderType (PVTy _ _ ty) = ty
 134 | 
 135 | export
 136 | multiplicity : Binder tm -> RigCount
 137 | multiplicity (Lam _ c x ty) = c
 138 | multiplicity (Let _ c val ty) = c
 139 | multiplicity (Pi _ c x ty) = c
 140 | multiplicity (PVar _ c p ty) = c
 141 | multiplicity (PLet _ c val ty) = c
 142 | multiplicity (PVTy _ c ty) = c
 143 | 
 144 | export
 145 | piInfo : Binder tm -> PiInfo tm
 146 | piInfo (Lam _ c x ty) = x
 147 | piInfo (Let _ c val ty) = Explicit
 148 | piInfo (Pi _ c x ty) = x
 149 | piInfo (PVar _ c p ty) = p
 150 | piInfo (PLet _ c val ty) = Explicit
 151 | piInfo (PVTy _ c ty) = Explicit
 152 | 
 153 | export
 154 | isImplicit : Binder tm -> Bool
 155 | isImplicit = PiInfo.isImplicit . piInfo
 156 | 
 157 | export
 158 | setMultiplicity : Binder tm -> RigCount -> Binder tm
 159 | setMultiplicity (Lam fc _ x ty) c = Lam fc c x ty
 160 | setMultiplicity (Let fc _ val ty) c = Let fc c val ty
 161 | setMultiplicity (Pi fc _ x ty) c = Pi fc c x ty
 162 | setMultiplicity (PVar fc _ p ty) c = PVar fc c p ty
 163 | setMultiplicity (PLet fc _ val ty) c = PLet fc c val ty
 164 | setMultiplicity (PVTy fc _ ty) c = PVTy fc c ty
 165 | 
 166 | Show ty => Show (Binder ty) where
 167 |   show (Lam _ c _ t) = "\\" ++ showCount c ++ show t
 168 |   show (Pi _ c _ t) = "Pi " ++ showCount c ++ show t
 169 |   show (Let _ c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t
 170 |   show (PVar _ c _ t) = "pat " ++ showCount c ++ show t
 171 |   show (PLet _ c v t) = "plet " ++ showCount c ++ show v ++ " : " ++ show t
 172 |   show (PVTy _ c t) = "pty " ++ showCount c ++ show t
 173 | 
 174 | export
 175 | setType : Binder tm -> tm -> Binder tm
 176 | setType (Lam fc c x _) ty = Lam fc c x ty
 177 | setType (Let fc c val _) ty = Let fc c val ty
 178 | setType (Pi fc c x _) ty = Pi fc c x ty
 179 | setType (PVar fc c p _) ty = PVar fc c p ty
 180 | setType (PLet fc c val _) ty = PLet fc c val ty
 181 | setType (PVTy fc c _) ty = PVTy fc c ty
 182 | 
 183 | export
 184 | Functor PiInfo where
 185 |   map func Explicit = Explicit
 186 |   map func Implicit = Implicit
 187 |   map func AutoImplicit = AutoImplicit
 188 |   map func (DefImplicit t) = (DefImplicit (func t))
 189 | 
 190 | export
 191 | Foldable PiInfo where
 192 |   foldr f acc Implicit = acc
 193 |   foldr f acc Explicit = acc
 194 |   foldr f acc AutoImplicit = acc
 195 |   foldr f acc (DefImplicit x) = f x acc
 196 | 
 197 | export
 198 | Traversable PiInfo where
 199 |   traverse f Implicit = pure Implicit
 200 |   traverse f Explicit = pure Explicit
 201 |   traverse f AutoImplicit = pure AutoImplicit
 202 |   traverse f (DefImplicit x) = map DefImplicit (f x)
 203 | 
 204 | export
 205 | Functor PiBindData where
 206 |   map f (MkPiBindData info type) = MkPiBindData (map f info) (f type)
 207 | 
 208 | export
 209 | Foldable PiBindData where
 210 |   foldr f acc (MkPiBindData info type) = f type (foldr f acc info)
 211 | 
 212 | export
 213 | Traversable PiBindData where
 214 |   traverse f (MkPiBindData info type) = MkPiBindData <$> traverse f info <*> f type
 215 | 
 216 | export
 217 | Functor Binder where
 218 |   map func (Lam fc c x ty) = Lam fc c (map func x) (func ty)
 219 |   map func (Let fc c val ty) = Let fc c (func val) (func ty)
 220 |   map func (Pi fc c x ty) = Pi fc c (map func x) (func ty)
 221 |   map func (PVar fc c p ty) = PVar fc c (map func p) (func ty)
 222 |   map func (PLet fc c val ty) = PLet fc c (func val) (func ty)
 223 |   map func (PVTy fc c ty) = PVTy fc c (func ty)
 224 | 
 225 | export
 226 | Foldable Binder where
 227 |   foldr f acc (Lam fc c x ty) = foldr f (f ty acc) x
 228 |   foldr f acc (Let fc c val ty) = f val (f ty acc)
 229 |   foldr f acc (Pi fc c x ty) = foldr f (f ty acc) x
 230 |   foldr f acc (PVar fc c p ty) = foldr f (f ty acc) p
 231 |   foldr f acc (PLet fc c val ty) = f val (f ty acc)
 232 |   foldr f acc (PVTy fc c ty) = f ty acc
 233 | 
 234 | export
 235 | Traversable Binder where
 236 |   traverse f (Lam fc c x ty) = Lam fc c <$> traverse f x <*> f ty
 237 |   traverse f (Let fc c val ty) = Let fc c <$> f val <*> f ty
 238 |   traverse f (Pi fc c x ty) = Pi fc c <$> traverse f x <*> f ty
 239 |   traverse f (PVar fc c p ty) = PVar fc c <$> traverse f p <*> f ty
 240 |   traverse f (PLet fc c val ty) = PLet fc c <$> f val <*> f ty
 241 |   traverse f (PVTy fc c ty) = PVTy fc c <$> f ty
 242 | 
 243 | 
 244 | export
 245 | eqBinderBy : (t -> u -> Bool) -> (Binder t -> Binder u -> Bool)
 246 | eqBinderBy eqTU = go where
 247 | 
 248 |   go : Binder t -> Binder u -> Bool
 249 |   go (Lam _ c p ty) (Lam _ c' p' ty') = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
 250 |   go (Let _ c v ty) (Let _ c' v' ty') = c == c' && eqTU v v' && eqTU ty ty'
 251 |   go (Pi _ c p ty) (Pi _ c' p' ty')   = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
 252 |   go (PVar _ c p ty) (PVar _ c' p' ty') = c == c' && eqPiInfoBy eqTU p p' && eqTU ty ty'
 253 |   go (PLet _ c v ty) (PLet _ c' v' ty') = c == c' && eqTU v v' && eqTU ty ty'
 254 |   go (PVTy _ c ty) (PVTy _ c' ty') = c == c' && eqTU ty ty'
 255 |   go _ _ = False
 256 | 
 257 | export
 258 | Eq a => Eq (Binder a) where
 259 |   (==) = eqBinderBy (==)
 260 |