0 | module Derive.BarbieInfo
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | ||| Proof that a `TTImp` corresponds to `k -> Type` for some `k`.
 7 | public export
 8 | data ToType : TTImp -> Type where
 9 |   IsToType : {k : TTImp} -> ToType  (IPi f1 MW ExplicitArg n2 k (IType f3))
10 |
11 | public export
12 | toType : (t : TTImp) -> Maybe (ToType t)
13 | toType (IPi _ MW ExplicitArg _ k (IType _)) = Just IsToType
14 | toType _ = Nothing
15 |
16 | ||| Proof that the last in a list of arguments is of type `Type -> Type`
17 | public export
18 | data BarbieArgs : Vect n Arg -> Type where
19 |   BAHere  :
20 |        {0 t : TTImp}
21 |     -> {n : Name}
22 |     -> {auto prf : ToType t}
23 |     -> BarbieArgs [MkArg c ExplicitArg (Just n) t]
24 |   BAThere : BarbieArgs vs -> BarbieArgs (v :: vs)
25 |
26 | public export
27 | barbieArgs : (vs : Vect n Arg) -> Maybe (BarbieArgs vs)
28 | barbieArgs [MkArg c ExplicitArg (Just n) t] =
29 |   let Just _ := toType t | Nothing => Nothing
30 |    in Just BAHere
31 | barbieArgs (x :: xs) = BAThere <$> barbieArgs xs
32 | barbieArgs [] = Nothing
33 |
34 | ||| Name of the last argument of a `Barbie` type constructor.
35 | public export
36 | barbieArg : BarbieArgs vs -> Name
37 | barbieArg (BAHere {n}) = n
38 | barbieArg (BAThere x)  = barbieArg x
39 |
40 | ||| Name of the last argument of a `Barbie` type constructor.
41 | public export
42 | barbieKind : BarbieArgs vs -> TTImp
43 | barbieKind (BAHere @{IsToType {k}}) = k
44 | barbieKind (BAThere x)  = barbieKind x
45 |
46 | ||| Proof that a parameterized type is actually a `Barbie`.
47 | public export
48 | record BarbieInfo where
49 |   constructor BI
50 |   info : ParamTypeInfo
51 |   prf  : BarbieArgs info.info.args
52 |
53 | public export
54 | Named BarbieInfo where
55 |   b.getName = b.info.getName
56 |
57 | public export
58 | hasFArg : (farg : Name) -> TTImp -> Bool
59 | hasFArg farg (IApp _ (IVar _ n) _) = farg == n
60 | hasFArg _    _                     = False
61 |
62 | ||| Names of all type arguments of a barbie, except the last one
63 | public export
64 | (.explicitArgs) : BarbieInfo -> List Name
65 | (.explicitArgs) p = go Lin p.info.info.args p.prf p.info.info.argNames
66 |   where
67 |     go :
68 |          SnocList Name
69 |       -> (vs : Vect k Arg)
70 |       -> BarbieArgs vs
71 |       -> Vect k Name
72 |       -> List Name
73 |     go snm [_] BAHere [_] = snm <>> []
74 |     go snm (MkArg _ ExplicitArg _ _:: vs) (BAThere x) (n :: ns) =
75 |       go (snm :< n) vs x ns
76 |     go snm (v :: vs) (BAThere x) (n :: ns) = go snm vs x ns
77 |
78 | ||| Returns a type constructor
79 | ||| applied to the names of its explicit arguments except the last one
80 | public export
81 | (.applied) : BarbieInfo -> TTImp
82 | (.applied) p = appNames p.getName p.explicitArgs
83 |
84 | ||| Returns a list of implicit arguments corresponding
85 | ||| to the data type's explicit arguments (except the last one)
86 | public export %inline
87 | (.implicits) : BarbieInfo -> List Arg
88 | (.implicits) p = implicits p.explicitArgs
89 |
90 | ||| Returns the kind of the first argument of the last parameter of
91 | ||| a barbie.
92 | public export %inline
93 | (.kind) : BarbieInfo -> TTImp
94 | (.kind) p = barbieKind p.prf
95 |