
   0 | module Language.Reflection.Types
   1 | 
   2 | -- inspired by https://github.com/MarcelineVQ/idris2-elab-deriving/
   3 | 
   4 | import Data.Vect
   5 | import Data.Vect.Quantifiers
   6 | import Language.Reflection
   7 | import Language.Reflection.Syntax
   8 | 
   9 | %language ElabReflection
  10 | 
  11 | %default total
  12 | 
  13 | --------------------------------------------------------------------------------
  14 | --          Utilities
  15 | --------------------------------------------------------------------------------
  16 | 
  17 | public export
  18 | Res : Type -> Type
  19 | Res = Either String
  20 | 
  21 | ||| Creates a sequence of argument names, using the given string as a prefix
  22 | ||| and appending names with their index in the sequence.
  23 | |||
  24 | ||| It is at times necessary to provide a set of fresh names to
  25 | ||| for instance pattern matching on a data constructor making sure
  26 | ||| to not shadow already existing
  27 | ||| names. This function provides a pure way to do so without having
  28 | ||| to run this in the `Elab` monad.
  29 | export
  30 | freshNames : String -> (n : Nat) -> Vect n Name
  31 | freshNames s = go 0
  32 | 
  33 |   where
  34 |     go : Nat -> (k : Nat) -> Vect k Name
  35 |     go m 0     = []
  36 |     go m (S k) = (UN $ Basic $ s ++ show m) :: go (S m) k
  37 | 
  38 | public export
  39 | implicits : Foldable t => t Name -> List Arg
  40 | implicits = map erasedImplicit . toList
  41 | 
  42 | ||| Tries to generate the given proofs for all values in the
  43 | ||| given vector over an applicative functor.
  44 | public export
  45 | tryAll :
  46 |      {0 a : Type}
  47 |   -> {0 p : a -> Type}
  48 |   -> {auto _ : Applicative f}
  49 |   -> ((v : a) -> f (p v))
  50 |   -> (vs : Vect n a)
  51 |   -> f (All p vs)
  52 | tryAll g []        = pure []
  53 | tryAll g (x :: xs) = [| g x :: tryAll g xs |]
  54 | 
  55 | --------------------------------------------------------------------------------
  56 | --          Applied Arguments
  57 | --------------------------------------------------------------------------------
  58 | 
  59 | public export
  60 | data MissingInfo : PiInfo TTImp -> Type where
  61 |   Auto     : MissingInfo AutoImplicit
  62 |   Implicit : MissingInfo ImplicitArg
  63 |   Deflt    : MissingInfo (DefImplicit t)
  64 | 
  65 | export
  66 | Uninhabited (MissingInfo ExplicitArg) where
  67 |   uninhabited Auto impossible
  68 |   uninhabited Implicit impossible
  69 |   uninhabited Deflt impossible
  70 | 
  71 | ||| An argument extracted from an applied function.
  72 | |||
  73 | ||| We use these to match result types of data constructors against the
  74 | ||| arguments of the corresponding type constructor, so they
  75 | ||| are indexed by the corresponding argument.
  76 | public export
  77 | data AppArg : Arg -> Type where
  78 |   ||| Named application: `foo {x = 12}`
  79 |   NamedApp : (n : Name) -> TTImp -> AppArg (MkArg c p (Just n) t)
  80 | 
  81 |   ||| Applying an unnamed auto implicit: `foo @{MyEq}`
  82 |   AutoApp  : TTImp -> AppArg (MkArg c AutoImplicit n t)
  83 | 
  84 |   ||| Regular function application: `foo 12`.
  85 |   Regular  : TTImp -> AppArg (MkArg c ExplicitArg n t)
  86 | 
  87 |   ||| An implicit argument not given explicitly.
  88 |   Missing  : MissingInfo p -> AppArg (MkArg c p n t)
  89 | 
  90 | public export
  91 | (.ttimp) : AppArg a -> TTImp
  92 | (.ttimp) (NamedApp nm s) = s
  93 | (.ttimp) (Regular s)     = s
  94 | (.ttimp) (AutoApp s)     = s
  95 | (.ttimp) (Missing x)     = implicitFalse
  96 | 
  97 | ||| Applies an argument to the given value.
  98 | public export
  99 | appArg : TTImp -> AppArg a -> TTImp
 100 | appArg t (NamedApp nm s) = namedApp t nm s
 101 | appArg t (AutoApp s)     = autoApp t s
 102 | appArg t (Regular s)     = app t s
 103 | appArg t (Missing _)     = t
 104 | 
 105 | ||| Sequence of applied arguments matching a list of function arguments.
 106 | public export
 107 | 0 AppArgs : Vect n Arg -> Type
 108 | AppArgs = All AppArg
 109 | 
 110 | unappVia : (TTImp -> Maybe (a, TTImp)) -> TTImp -> Maybe (a,TTImp)
 111 | unappVia f s = case f s of
 112 |   Just p  => Just p
 113 |   Nothing => case s of
 114 |     IApp fc t u         => map (\t' => IApp fc t' u) <$> unappVia f t
 115 |     INamedApp fc t nm u => map (\t' => INamedApp fc t' nm u) <$> unappVia f t
 116 |     IAutoApp fc t u     => map (\t' => IAutoApp fc t' u) <$> unappVia f t
 117 |     _                   => Nothing
 118 | 
 119 | -- tries to extract a named argument from an expression
 120 | named : (n : Name) -> TTImp -> Maybe (AppArg (MkArg c p (Just n) t), TTImp)
 121 | named n =
 122 |   unappVia $ \case
 123 |     INamedApp fc t nm u =>
 124 |       if n == nm then Just (NamedApp n u, t) else Nothing
 125 |     _                   => Nothing
 126 | 
 127 | -- tries to extract an auto-implicit argument from an expression
 128 | getAuto : TTImp -> Maybe (AppArg (MkArg c AutoImplicit n t), TTImp)
 129 | getAuto = unappVia $ \case
 130 |   IAutoApp fc t u => Just (AutoApp u, t)
 131 |   _               => Nothing
 132 | 
 133 | -- tries to extract a regular argument from an expression
 134 | regular : TTImp -> Maybe (AppArg (MkArg c ExplicitArg n t), TTImp)
 135 | regular = unappVia $ \case
 136 |   IApp fc t u => Just (Regular u, t)
 137 |   _           => Nothing
 138 | 
 139 | unnamed : (p : PiInfo TTImp) -> TTImp -> Maybe (AppArg (MkArg c p n t), TTImp)
 140 | unnamed ExplicitArg     s = regular s
 141 | unnamed ImplicitArg     s = Just (Missing Implicit, s)
 142 | unnamed (DefImplicit x) s = Just (Missing Deflt, s)
 143 | unnamed AutoImplicit    s = getAuto s <|> Just (Missing Auto, s)
 144 | 
 145 | ||| Tries to extract an applied argument from an expression,
 146 | ||| returning it together with the remainder of the expression.
 147 | export
 148 | getArg : (arg : Arg) -> TTImp -> Maybe (AppArg arg , TTImp)
 149 | getArg (MkArg _ pi Nothing _)  s = unnamed pi s
 150 | getArg (MkArg _ pi (Just n) _) s = named n s <|> unnamed pi s
 151 | 
 152 | argErr : Arg -> String
 153 | argErr (MkArg _ _ (Just n) _) = "Missing explicit argument: \{n}"
 154 | argErr (MkArg _ _ Nothing t) =
 155 |   "Missing unnamed, explicit argument of type: \{show t}"
 156 | 
 157 | ||| Tries to unapply an expression and extract all
 158 | ||| applied function arguments.
 159 | public export
 160 | getArgs : (vs : Vect n Arg) -> TTImp -> Res (AppArgs vs, TTImp)
 161 | getArgs (x :: xs) s =
 162 |   let Right (vs,s2) := getArgs xs s | Left err => Left err
 163 |       Just (v,s3)   := getArg x s2  | Nothing => Left $ argErr x
 164 |    in Right (v :: vs, s3)
 165 | getArgs []        s = Right ([], s)
 166 | 
 167 | --------------------------------------------------------------------------------
 168 | --          Constructors
 169 | --------------------------------------------------------------------------------
 170 | 
 171 | ||| Data constructor of a data type index over the list of arguments
 172 | ||| of the corresponding type constructor.
 173 | public export
 174 | record  Con (n : Nat) (vs : Vect n Arg) where
 175 |   constructor MkCon
 176 |   name     : Name
 177 |   arty     : Nat
 178 |   args     : Vect arty Arg
 179 |   typeArgs : AppArgs vs
 180 | 
 181 | public export %inline
 182 | Named (Con n vs) where
 183 |   c.getName = c.name
 184 | 
 185 | ||| True if the given constructor has only erased arguments.
 186 | public export
 187 | isConstant : Con n vs -> Bool
 188 | isConstant c = all isErased c.args
 189 | 
 190 | ||| Creates bindings for the explicit arguments of a data constructor
 191 | ||| using the given prefix plus an index for the name of each
 192 | ||| argument.
 193 | |||
 194 | ||| This is useful for implementing functions which pattern match on a
 195 | ||| data constructor.
 196 | export
 197 | bindCon : (c : Con n vs) -> Vect c.arty Name -> TTImp
 198 | bindCon c ns = go c.nameVar (map piInfo c.args) ns
 199 | 
 200 |   where
 201 |     go : TTImp -> Vect k (PiInfo TTImp) -> Vect k Name -> TTImp
 202 |     go t []                  []        = t
 203 |     go t (ExplicitArg :: xs) (n :: ns) = go (t `app` bindVar n) xs ns
 204 |     go t (_           :: xs) (n :: ns) = go t xs ns
 205 | 
 206 | ||| Applies a constructor to variables of the given name.
 207 | export
 208 | applyCon : (c : Con n vs) -> Vect c.arty Name -> TTImp
 209 | applyCon c ns = go c.nameVar (map piInfo c.args) ns
 210 | 
 211 |   where
 212 |     go : TTImp -> Vect k (PiInfo TTImp) -> Vect k Name -> TTImp
 213 |     go t []                  []        = t
 214 |     go t (ExplicitArg :: xs) (n :: ns) = go (t `app` var n) xs ns
 215 |     go t (_           :: xs) (n :: ns) = go t xs ns
 216 | 
 217 | ||| Tries to lookup a data constructor by name, based on the
 218 | ||| given list of arguments of the corresponding data constructor.
 219 | export
 220 | getCon : Elaboration m => (vs : Vect n Arg) -> Name -> m (Con n vs)
 221 | getCon vs n = do
 222 |   (n',tt)       <- lookupName n
 223 |   let (args,tpe)      := unPi tt
 224 |       (arty ** vargs) := (length args ** Vect.fromList args)
 225 |   case getArgs vs tpe of
 226 |     Right (vs, IVar _ _) => pure $ (MkCon n' arty vargs vs)
 227 |     Right (vs, _)        => fail "Unexpected type for constructor \{n}"
 228 |     Left err             => fail "Unexpected type for constructor \{n}: \{err}"
 229 | 
 230 | ||| Information about a data type
 231 | |||
 232 | ||| @name : Name of the data type
 233 | |||         Note: There is no guarantee that the name will be fully
 234 | |||         qualified
 235 | ||| @args : Type arguments of the data type
 236 | ||| @cons : List of data constructors
 237 | public export
 238 | record TypeInfo where
 239 |   constructor MkTypeInfo
 240 |   name     : Name
 241 |   arty     : Nat
 242 |   args     : Vect arty Arg
 243 |   argNames : Vect arty Name
 244 |   cons     : List (Con arty args)
 245 | 
 246 | public export %inline
 247 | Named TypeInfo where
 248 |   t.getName = t.name
 249 | 
 250 | public export
 251 | namedArg : (a : Arg) -> Maybe Name
 252 | namedArg (MkArg _ _ (Just n) _) = Just n
 253 | namedArg _                      = Nothing
 254 | 
 255 | ||| Returns the names of explicit arguments of a type constructor.
 256 | public export
 257 | (.explicitArgs) : TypeInfo -> List Name
 258 | (.explicitArgs) p = go Lin p.args p.argNames
 259 | 
 260 |   where
 261 |     go : SnocList Name -> Vect k Arg -> Vect k Name -> List Name
 262 |     go sn []        []                              = sn <>> []
 263 |     go sn (MkArg _ ExplicitArg _ _ :: xs) (n :: ns) = go (sn :< n) xs ns
 264 |     go sn (_                       :: xs) (n :: ns) = go sn xs ns
 265 | 
 266 | ||| Returns a type constructor
 267 | ||| applied to the names of its explicit arguments
 268 | public export
 269 | (.applied) : TypeInfo -> TTImp
 270 | (.applied) p = go p.nameVar p.args p.argNames
 271 | 
 272 |   where
 273 |     go : TTImp -> Vect n Arg -> Vect n Name -> TTImp
 274 |     go t []        []          = t
 275 |     go t (MkArg _ AutoImplicit _ _ :: xs) (_ :: nms) = go t xs nms
 276 |     go t (MkArg _ _ (Just no) _ :: xs) (nm :: nms) =
 277 |       go (namedApp t no (var nm)) xs nms
 278 |     go t (MkArg _ _ Nothing   _ :: xs) (nm :: nms) =
 279 |       go (t `app` var nm) xs nms
 280 | 
 281 | ||| Returns a list of implicit arguments corresponding
 282 | ||| to the data type's implicit and explicit arguments.
 283 | public export %inline
 284 | (.implicits) : TypeInfo -> List Arg
 285 | (.implicits) p = go Lin p.args
 286 | 
 287 |   where
 288 |     toArg : Maybe Name -> TTImp -> Arg
 289 |     toArg mn (IHole _ _) = MkArg M0 ImplicitArg mn implicitFalse
 290 |     toArg mn t           = MkArg M0 ImplicitArg mn t
 291 | 
 292 |     go : SnocList Arg -> Vect k Arg -> List Arg
 293 |     go sn []                               = sn <>> []
 294 |     go sn (MkArg _ ExplicitArg mn t :: xs) = go (sn :< toArg mn t) xs
 295 |     go sn (MkArg _ ImplicitArg mn t :: xs) = go (sn :< toArg mn t) xs
 296 |     go sn (_                        :: xs) = go sn xs
 297 | 
 298 | 
 299 | ||| True if the given type has only constant constructors and
 300 | ||| is therefore represented by a single unsigned integer at runtime.
 301 | public export
 302 | isEnum : TypeInfo -> Bool
 303 | isEnum ti = all isConstant $ ti.cons
 304 | 
 305 | ||| True if the given constructor has name `Nil` and no explicit arguments.
 306 | public export
 307 | isNil : Con n vs -> Bool
 308 | isNil (MkCon n _ as _) = isNil n && all (not . isExplicit) as
 309 | 
 310 | ||| True if the given constructor has name `(::)` and
 311 | ||| exactly two explicit arguments.
 312 | public export
 313 | isCons : Con n vs -> Bool
 314 | isCons (MkCon n _ as _) = isCons n && count isExplicit as == 2
 315 | 
 316 | ||| True if the given constructor has name `Lin` and no explicit arguments.
 317 | public export
 318 | isLin : Con n vs -> Bool
 319 | isLin (MkCon n _ as _) = isLin n && all (not . isExplicit) as
 320 | 
 321 | ||| True if the given constructor has name `(:<)` and
 322 | ||| exactly two explicit arguments.
 323 | public export
 324 | isSnoc : Con n vs -> Bool
 325 | isSnoc (MkCon n _ as _) = isSnoc n && count isExplicit as == 2
 326 | 
 327 | ||| True if the given type has a single constructor with a single
 328 | ||| unerased argument.
 329 | public export
 330 | isNewtype : TypeInfo -> Bool
 331 | isNewtype (MkTypeInfo _ _ _ _ [c]) = count (not . isErased) c.args == 1
 332 | isNewtype _                      = False
 333 | 
 334 | ||| True, if the given type has exactly one
 335 | ||| `Nil` constructor with no explicit
 336 | ||| argument and a `(::)` constructor with two explicit arguments.
 337 | public export
 338 | isListLike : TypeInfo -> Bool
 339 | isListLike (MkTypeInfo _ _ _ _ [x,y]) = isNil x && isCons y || isCons x && isNil y
 340 | isListLike _                        = False
 341 | 
 342 | ||| True, if the given type has exactly one
 343 | ||| `Lin` constructor with no explicit
 344 | ||| argument and a `(:<)` constructor with two explicit arguments.
 345 | public export
 346 | isSnocListLike : TypeInfo -> Bool
 347 | isSnocListLike (MkTypeInfo _ _ _ _ [x,y]) =
 348 |   isLin x && isSnoc y || isSnoc x && isLin y
 349 | isSnocListLike _                        = False
 350 | 
 351 | ||| True if the given type has a single constructor with only erased
 352 | ||| arguments. Such a value will have a trivial runtime representation.
 353 | public export
 354 | isErased : TypeInfo -> Bool
 355 | isErased (MkTypeInfo _ _ _ _ [c]) = isConstant c
 356 | isErased _                        = False
 357 | 
 358 | ||| Tries to get information about the data type specified
 359 | ||| by name. The name need not be fully qualified, but
 360 | ||| needs to be unambiguous.
 361 | export
 362 | getInfo' : Elaboration m => Name -> m TypeInfo
 363 | getInfo' n = do
 364 |   (n',tt)        <- lookupName n
 365 |   (args,IType _) <- pure $ unPi tt
 366 |     | (_,_) => fail "Type declaration does not end in IType: \{show tt}"
 367 | 
 368 |   let (arty ** vargs) := (length args ** Vect.fromList args)
 369 |   Just nargs    <- pure $ traverse name vargs
 370 |     | Nothing => fail "\{n'} has unnamed type arguments"
 371 |   conNames       <- getCons n'
 372 |   cons           <- traverse (getCon vargs) conNames
 373 |   pure (MkTypeInfo n' arty vargs nargs cons)
 374 | 
 375 | ||| macro version of `getInfo'`
 376 | export %macro
 377 | getInfo : Name -> Elab TypeInfo
 378 | getInfo = getInfo'
 379 | 
 380 | ||| Tries to get the name of the sole constructor
 381 | ||| of data type specified by name. Fails, if
 382 | ||| the name is not unambiguous, or if the data type
 383 | ||| in question has not exactly one constructor.
 384 | export %macro
 385 | singleCon : Name -> Elab Name
 386 | singleCon n = do
 387 |   (MkTypeInfo _ _ _ _ [c]) <- getInfo' n
 388 |     | _ => fail "\{n} is not a single-constructor data type"
 389 |   pure $ c.name
 390 | 
 391 | --------------------------------------------------------------------------------
 392 | --          Parameterized Types
 393 | --------------------------------------------------------------------------------
 394 | 
 395 | public export
 396 | data ParamTag : Nat -> Type where
 397 |   I : ParamTag 0
 398 |   P : ParamTag 1
 399 | 
 400 | public export
 401 | data ParamPattern : (typeArgs, params : Nat) -> Type where
 402 |   Nil  : ParamPattern 0 0
 403 |   (::) : ParamTag k -> ParamPattern m n -> ParamPattern (S m) (k + n)
 404 | 
 405 | public export
 406 | paramsOnly : (k : Nat) -> ParamPattern k k
 407 | paramsOnly 0     = []
 408 | paramsOnly (S k) = P :: paramsOnly k
 409 | 
 410 | public export
 411 | indicesOnly : (k : Nat) -> ParamPattern k 0
 412 | indicesOnly 0     = []
 413 | indicesOnly (S k) = I :: indicesOnly k
 414 | 
 415 | public export
 416 | extractParams : ParamPattern n k -> (vs : Vect n a) -> Vect k a
 417 | extractParams []        []        = []
 418 | extractParams (I :: ps) (x :: xs) = extractParams ps xs
 419 | extractParams (P :: ps) (x :: xs) = x :: extractParams ps xs
 420 | 
 421 | ||| Constructor argument type in a parameterized data type
 422 | ||| with `n` parameters.
 423 | public export
 424 | data PArg : (n : Nat) -> Type where
 425 |   PPar      : Fin n -> PArg n
 426 |   PVar      : Name -> PArg n
 427 |   PLam      : Count -> PiInfo TTImp -> Maybe Name -> PArg n -> PArg n -> PArg n
 428 |   PApp      : (x,y : PArg n) -> PArg n
 429 |   PNamedApp : PArg n -> Name -> PArg n -> PArg n
 430 |   PAutoApp  : PArg n -> PArg n -> PArg n
 431 |   PWithApp  : PArg n -> PArg n -> PArg n
 432 |   PSearch   : Nat -> PArg n
 433 |   PPrim     : Constant -> PArg n
 434 |   PDelayed  : LazyReason -> PArg n -> PArg n
 435 |   PType     : PArg n
 436 |   PHole     : String -> PArg n
 437 | 
 438 | ||| Checks if two `PArgs` are equal (ignoring the `FC`).
 439 | export
 440 | Eq (PArg n) where
 441 |   PPar x == PPar y = x == y
 442 |   PVar x == PVar y = x == y
 443 |   PApp x y == PApp v w = x == v && y == w
 444 |   PLam c p m u v == PLam d q n x y =
 445 |     c == d && p == q && m == n && u == x && v == y
 446 |   PNamedApp x m y == PNamedApp v n w = x == v && m == n && y == w
 447 |   PAutoApp x y == PAutoApp v w = x == v && y == w
 448 |   PWithApp x y == PWithApp v w = x == v && y == w
 449 |   PSearch c == PSearch d = c == d
 450 |   PPrim c == PPrim d = c == d
 451 |   PDelayed lr x == PDelayed lr2 y = lr == lr2 && x == y
 452 |   PType == PType = True
 453 |   PHole c == PHole d = c == d
 454 |   _ == _ = False
 455 | 
 456 | ||| Checks if the given name corresponds to a parameter, in
 457 | ||| which case it must be present in the given vector of names.
 458 | public export
 459 | pvar : Named a => Vect n a -> (bound : List Name) -> Name -> PArg n
 460 | pvar xs bound nm = case findIndex (\v => nm == v.getName) xs of
 461 |   Just ix => if nm `elem` bound then PVar nm else PPar ix
 462 |   Nothing => PVar nm
 463 | 
 464 | ||| Tries to convert a `TTImp` to an argument of a
 465 | ||| parameterized constructor using the given vector of parameter names.
 466 | public export
 467 | parg : Named a => Vect n a -> (bound : List Name) -> TTImp -> Res (PArg n)
 468 | parg xs b (IVar _ nm)         = Right $ pvar xs b nm
 469 | parg xs b (IApp _ s t)        = PApp <$> parg xs b s <*> parg xs b t
 470 | parg xs b (INamedApp _ s n t) = PNamedApp <$> parg xs b s <*> pure n <*> parg xs b t
 471 | parg xs b (IAutoApp _ s t)    = PAutoApp <$> parg xs b s <*> parg xs b t
 472 | parg xs b (IWithApp _ s t)    = PWithApp <$> parg xs b s <*> parg xs b t
 473 | parg xs b (IDelayed _ lr s)   = PDelayed lr <$> parg xs b s
 474 | parg xs b (IPrimVal _ c)      = Right $ PPrim c
 475 | parg xs b (IType _)           = Right PType
 476 | parg xs b (ISearch _ n)       = Right $ PSearch n
 477 | parg xs b (IHole _ n)         = Right $ PHole n
 478 | parg xs b (ILam _ c p n x y)  =
 479 |   [| PLam (pure c) (pure p) (pure n) (parg xs b x) (parg xs (toList n ++ b) y) |]
 480 | parg xs b t                 =
 481 |   Left "\{show t} is not a valid constructor argument type"
 482 | 
 483 | namespace PArg
 484 |   ||| Converts an argument of a parameterized data type to the
 485 |   ||| corresponding `TTImp` expression.
 486 |   public export
 487 |   ttimp : Vect n Name -> PArg n -> TTImp
 488 |   ttimp ns (PPar x)          = var (index x ns)
 489 |   ttimp ns (PVar nm)         = var nm
 490 |   ttimp ns (PApp x y)        = ttimp ns x `app` ttimp ns y
 491 |   ttimp ns (PNamedApp x n y) = INamedApp EmptyFC (ttimp ns x) n (ttimp ns y)
 492 |   ttimp ns (PAutoApp x y)    = IAutoApp EmptyFC (ttimp ns x) (ttimp ns y)
 493 |   ttimp ns (PWithApp x y)    = IWithApp EmptyFC (ttimp ns x) (ttimp ns y)
 494 |   ttimp ns (PPrim c)         = primVal c
 495 |   ttimp ns (PDelayed lr x)   = IDelayed EmptyFC lr (ttimp ns x)
 496 |   ttimp ns (PSearch n)       = ISearch EmptyFC n
 497 |   ttimp ns PType             = IType EmptyFC
 498 |   ttimp ns (PHole n)         = IHole EmptyFC n
 499 |   ttimp ns (PLam c p n x y)  = ILam EmptyFC c p n (ttimp ns x) (ttimp ns y)
 500 | 
 501 | ||| Extracts the sub-expressions from an argument's type
 502 | ||| where the outermost value is a parameter.
 503 | |||
 504 | ||| Example:
 505 | ||| If `f`, `a`, and `b` are parameters, this will extract
 506 | ||| `[f Int, f a, b]` from `Maybe (Pair (f Int, Pair (f a, b)))`
 507 | public export
 508 | paramArgs : PArg n -> List (PArg n)
 509 | paramArgs (PPar x)                   = [PPar x]
 510 | paramArgs (PVar nm)                  = []
 511 | paramArgs p@(PApp (PPar _) y)        = [p]
 512 | paramArgs p@(PAutoApp (PPar _) y)    = [p]
 513 | paramArgs p@(PWithApp (PPar _) y)    = [p]
 514 | paramArgs p@(PNamedApp (PPar _) n y) = [p]
 515 | paramArgs (PLam _ _ _ _ y)           = paramArgs y
 516 | paramArgs (PApp x y)                 = nub $ paramArgs x ++ paramArgs y
 517 | paramArgs (PAutoApp x y)             = nub $ paramArgs x ++ paramArgs y
 518 | paramArgs (PWithApp x y)             = nub $ paramArgs x ++ paramArgs y
 519 | paramArgs (PNamedApp x n y)          = nub $ paramArgs x ++ paramArgs y
 520 | paramArgs (PPrim c)                  = []
 521 | paramArgs (PDelayed lr x)            = paramArgs x
 522 | paramArgs  PType                     = []
 523 | paramArgs (PSearch _)                = []
 524 | paramArgs (PHole _)                  = []
 525 | 
 526 | public export
 527 | paramNames :
 528 |      {0 vs : Vect n Arg}
 529 |   -> ParamPattern n k
 530 |   -> AppArgs vs
 531 |   -> Res (Vect k Name)
 532 | paramNames []        []        = Right []
 533 | paramNames (I :: ps) (v :: vs) = paramNames ps vs
 534 | paramNames (P :: ps) (v :: vs) = case v.ttimp of
 535 |   IVar _ nm => (nm ::) <$> paramNames ps vs
 536 |   t         => Left "\{show t} is not a parameter"
 537 | 
 538 | ||| Argument of a data constructor of a parameterized data type.
 539 | public export
 540 | data ConArg : (n : Nat) -> Type where
 541 |   ParamArg : Fin n -> TTImp -> ConArg n
 542 |   CArg     : Maybe Name -> Count -> PiInfo TTImp -> PArg n -> ConArg n
 543 | 
 544 | public export
 545 | isExplicit : ConArg n -> Bool
 546 | isExplicit (CArg mnm rig ExplicitArg x) = True
 547 | isExplicit _                            = False
 548 | 
 549 | public export
 550 | conArg : Vect n Name -> Arg -> Res (ConArg n)
 551 | conArg ns (MkArg M0 ImplicitArg (Just nm) t) = case findIndex (nm ==) ns of
 552 |   Just ix => Right $ ParamArg ix t
 553 |   Nothing => CArg (Just nm) M0 ImplicitArg <$> parg ns Nil t
 554 | conArg ns (MkArg c pi nm t)                  = CArg nm c pi <$> parg ns Nil t
 555 | 
 556 | namespace ConArg
 557 |   public export
 558 |   paramArgs : ConArg n -> List (PArg n)
 559 |   paramArgs (ParamArg _ _) = []
 560 |   paramArgs (CArg _ _ _ t) = paramArgs t
 561 | 
 562 | public export
 563 | record ParamCon (n : Nat) where
 564 |   constructor MkParamCon
 565 |   name : Name
 566 |   arty : Nat
 567 |   args : Vect arty (ConArg n)
 568 | 
 569 | namespace ParamCon
 570 |   public export
 571 |   paramArgs : ParamCon n -> List (PArg n)
 572 |   paramArgs c = nub $ toList c.args >>= paramArgs
 573 | 
 574 | public export
 575 | Named (ParamCon n) where
 576 |   c.getName = c.name
 577 | 
 578 | public export
 579 | paramCon : ParamPattern n k -> Con n vs -> Res (ParamCon k)
 580 | paramCon ps (MkCon name arty args typeArgs) = do
 581 |   params  <- paramNames ps typeArgs
 582 |   conArgs <- traverse (conArg params) args
 583 |   pure $ MkParamCon name arty conArgs
 584 | 
 585 | public export
 586 | record ParamTypeInfo where
 587 |   constructor MkParamTypeInfo
 588 |   ||| Underlying type info
 589 |   info       : TypeInfo
 590 | 
 591 |   ||| Information about which type arguments are parameters and
 592 |   ||| which are indices
 593 |   pattern    : ParamPattern info.arty numParams
 594 | 
 595 |   ||| Name of parameters
 596 |   paramNames : Vect numParams Name
 597 | 
 598 |   ||| List of data constructors
 599 |   cons       : List (ParamCon numParams)
 600 | 
 601 |   ||| List of types appearing in constructor arguments, where the
 602 |   ||| the outermost applied type is one of the parameters. We use this
 603 |   ||| to generate the constraints necessary to implement interfaces such
 604 |   ||| as `Eq` or `Ord`.
 605 |   |||
 606 |   ||| For instance, in case of a constructor argument `Either (f a) (b, f Nat)`
 607 |   ||| with `f`, `a`, and `b` being parameters, this list will contain
 608 |   ||| the encoded forms of `f a`, `f Nat`, and `b`.
 609 |   pargs      : List (PArg numParams)
 610 | 
 611 | public export
 612 | Named ParamTypeInfo where
 613 |   p.getName = p.info.name
 614 | 
 615 | public export
 616 | paramType : (ti : TypeInfo) -> ParamPattern ti.arty k -> Res ParamTypeInfo
 617 | paramType ti@(MkTypeInfo nm n vs ns cs) ps = do
 618 |   cons <- traverse (paramCon ps) cs
 619 |   pure $ MkParamTypeInfo ti ps (extractParams ps ns) cons (nub $ cons >>= paramArgs)
 620 | 
 621 | ||| Returns the constraints required to implement the given interface
 622 | ||| for the given parameterized data types.
 623 | |||
 624 | ||| The interface must be of type `Type -> Type`.
 625 | export
 626 | constraints : ParamTypeInfo -> (iname : Name) -> List Arg
 627 | constraints p iname = map (toCon p.paramNames) p.pargs
 628 |   where toCon : Vect k Name ->  PArg k -> Arg
 629 |         toCon ns pa = MkArg MW AutoImplicit Nothing . (app $ var iname) $
 630 |                    ttimp ns pa
 631 | 
 632 | namespace ParamTypeInfo
 633 |   ||| Returns the type constructor of a parameterized
 634 |   ||| data type applied to its parameters
 635 |   public export
 636 |   (.applied) : ParamTypeInfo -> TTImp
 637 |   (.applied) p = p.info.applied
 638 | 
 639 |   ||| Returns a list of implicit arguments corresponding
 640 |   ||| to the data type's arguments.
 641 |   public export %inline
 642 |   (.implicits) : ParamTypeInfo -> List Arg
 643 |   (.implicits) p = p.info.implicits
 644 | 
 645 | ||| Short-hand for `p.implicits ++ constraints iname p`.
 646 | public export %inline
 647 | allImplicits : (p : ParamTypeInfo) -> (iname : Name) -> List Arg
 648 | allImplicits p iname = p.implicits ++ constraints p iname
 649 | 
 650 | ||| Returns information about a parameterized data type
 651 | ||| specified by the given (probably not fully qualified) name
 652 | ||| and a strategy for distinguishing between type parameters
 653 | ||| and indices.
 654 | export
 655 | getParamInfo' :
 656 |     {auto _ : Elaboration m}
 657 |   -> Name
 658 |   -> m ParamTypeInfo
 659 | getParamInfo' n = do
 660 |   ti <- getInfo' n
 661 |   case paramType ti (paramsOnly ti.arty) of
 662 |     Right pt => pure pt
 663 |     Left err => fail "Type \{n} is not supported: \{err}"
 664 | 
 665 | ||| macro version of `getParamInfo`.
 666 | export %macro
 667 | getParamInfo : Name -> Elab ParamTypeInfo
 668 | getParamInfo = getParamInfo'
 669 | 
 670 |