0 | module Deriving.Common
3 | import Language.Reflection
14 | data IsFreeOf : (x : Name) -> (ty : TTImp) -> Type where
17 | TrustMeFO : IsFreeOf a x
21 | assert_IsFreeOf : IsFreeOf x ty
22 | assert_IsFreeOf = TrustMeFO
27 | isFreeOf : (x : Name) -> (ty : TTImp) -> Maybe (IsFreeOf x ty)
29 | = do isOk <- flip mapMTTImp ty $
\case
30 | t@(IVar _ v) => t <$ guard (v /= x)
41 | | MkTPApp (Name, SnocList (Argument TypeParameter))
45 | Show TypeParameter where
46 | showPrec d (MkTPLocal a) = showCon d "MkTPLocal" $
show a
47 | showPrec d (MkTPPrim c) = showCon d "MkTPPrim" $
show c
48 | showPrec d (MkTPApp a) = showCon d "MkTPApp" $
assert_total $
show (map (map unArg) a)
49 | showPrec d MkTPIType = "MkTPIType"
52 | record IsFamily where
53 | constructor MkIsFamily
54 | typeConstructor : Name
55 | parameterNames : List (Argument TypeParameter, Nat)
56 | dataConstructors : List (Name, TTImp)
58 | wording : NameType -> String
59 | wording Bound = "a bound variable"
60 | wording Func = "a function name"
61 | wording (DataCon tag arity) = "a data constructor"
62 | wording (TyCon tag arity) = "a type constructor"
64 | checkAccessToDefinition : Elaboration m => (given, candidate : Name) -> m Bool
65 | checkAccessToDefinition g c = pure $
isParentOf (getNS g) (getNS c) || !(isPublic g)
67 | normaliseName : Elaboration m => FC -> Name -> m (Maybe TTImp)
68 | normaliseName fc n = do
69 | [(_, typeFun)] <- getType n
70 | | _ => failAt fc "\{show n} is ambiguous"
72 | Just typedFun <- catch $
check {expected = Type} typeFun
73 | | _ => failAt fc "\{show n} is not a Type declaration"
75 | Just checkedTy <- catch $
check {expected = typedFun} $
IVar fc n
76 | | _ => failAt fc "\{show n} has a different type than checked: \{show !(quote typedFun)}"
78 | normalisedTy <- quote checkedTy
81 | let tyq@(_, Just nn) = getHeadName normalisedTy
82 | | (broken, _) => failAt fc "Failed to extract type name from \{show n} (\{show normalisedTy}) at \{show broken}"
84 | pure $
if dropNS nn == dropNS n
86 | else Just normalisedTy
88 | getHeadName : TTImp -> (TTImp, Maybe Name)
89 | getHeadName t@(IVar _ n) = (t, pure n)
90 | getHeadName (IApp _ n _) = getHeadName n
91 | getHeadName (INamedApp _ n _ _) = getHeadName n
92 | getHeadName (IAutoApp _ n _) = getHeadName n
93 | getHeadName (IWithApp _ n _) = getHeadName n
94 | getHeadName (IPi _ _ _ _ _ retTy) = getHeadName retTy
95 | getHeadName (ILam _ _ _ _ _ retTy) = getHeadName retTy
96 | getHeadName t = (t, Nothing)
98 | isTypeCon : Elaboration m => Name -> FC -> Name -> m (Either TTImp (List (Name, TTImp)))
99 | isTypeCon currentFnName fc ty = do
100 | [(_, MkNameInfo (TyCon _ _))] <- getInfo ty
101 | | [(fullName, MkNameInfo Func)] => do
102 | unless !(checkAccessToDefinition fullName currentFnName) $
103 | failAt fc "Make sure \{show fullName} has public export visibility"
105 | Just normalised <- normaliseName fc fullName
106 | | _ => failAt fc "Unable to normalise \{show ty} to type constructor"
108 | pure $
Left normalised
109 | | [] => failAt fc "\{show ty} out of scope"
110 | | [(_, MkNameInfo nt)] => failAt fc "\{show ty} is \{wording nt} rather than a type constructor"
111 | | _ => failAt fc "\{show ty} is ambiguous"
113 | res <- for cs $
\ n => do
114 | [(_, ty)] <- getType n
115 | | _ => failAt fc "\{show n} is ambiguous"
119 | toTypeParameter : Elaboration m => TTImp -> m TypeParameter
120 | toTypeParameter (IType _) = pure MkTPIType
121 | toTypeParameter (IPrimVal _ c) = pure (MkTPPrim c)
123 | toTypeParameter (IVar _ nm@(UN (Basic _))) = pure (MkTPLocal nm)
124 | toTypeParameter arg with (appView arg)
125 | toTypeParameter t | Nothing = failAt (getFC t) "Unexpected a type parameter, got: \{show t}"
126 | toTypeParameter _ | (Just $
MkAppView (fc, h) args _) = do
127 | typedArgs <- assert_total $
traverse @{Compose} toTypeParameter args
128 | pure $
MkTPApp (h, typedArgs)
130 | isFamily' : Elaboration m => Name -> TTImp -> m IsFamily
131 | isFamily' currentFnName = go Z [] where
132 | go : Nat -> List (Argument TypeParameter, Nat) -> TTImp -> m IsFamily
133 | go idx acc (IVar fc n) = do
134 | case !(isTypeCon currentFnName fc n) of
135 | Right tcons => pure $
MkIsFamily n (map (map (minus idx . S)) acc) tcons
136 | Left normalised => assert_total $
isFamily' currentFnName normalised
137 | go idx acc (IApp fc t arg) = go (S idx) ((Arg fc !(toTypeParameter arg), idx) :: acc) t
138 | go idx acc (INamedApp fc t nm arg) = go (S idx) ((NamedArg fc nm !(toTypeParameter arg), idx) :: acc) t
139 | go idx acc (IAutoApp fc t arg) = go (S idx) ((AutoArg fc !(toTypeParameter arg), idx) :: acc) t
140 | go idx acc t = failAt (getFC t) "Expected a type constructor, got: \{show t}"
143 | isFamily : Elaboration m => TTImp -> m IsFamily
145 | let (Just currentName) = leftMost !getCurrentFn
146 | | _ => failAt (getFC t) "Deriving requires a function declaration, not a top level"
148 | isFamily' currentName t
154 | record ConstructorView where
155 | constructor MkConstructorView
156 | params : SnocList (Name, Nat)
157 | conArgTypes : List (Count, Argument TTImp)
160 | constructorView : TTImp -> Maybe ConstructorView
161 | constructorView (IPi fc rig pinfo x a b) = do
162 | let Just arg = fromPiInfo fc pinfo x a
163 | | Nothing => constructorView b
164 | let True = rig /= M1
165 | | False => constructorView b
166 | { conArgTypes $= ((rig, arg) ::) } <$> constructorView b
167 | constructorView f = do
168 | MkAppView _ ts _ <- appView f
169 | let range = [<] <>< [0..minus (length ts) 1]
170 | let ps = flip mapMaybe (zip ts range) $
\ t => the (Maybe (Name, Nat)) $
case t of
171 | (Arg _ (IVar _ nm), n) => Just (nm, n)
173 | pure (MkConstructorView ps [])
183 | withParams : FC -> (Nat -> Maybe TTImp) -> List (Argument TypeParameter, Nat) -> TTImp -> TTImp
184 | withParams fc params nms t = go nms where
186 | addConstraint : Maybe TTImp -> Name -> TTImp -> TTImp
187 | addConstraint Nothing _ = id
188 | addConstraint (Just cst) nm =
189 | let ty = IApp fc cst (IVar fc nm) in
190 | IPi fc MW AutoImplicit Nothing ty
192 | go : List (Argument TypeParameter, Nat) -> TTImp
194 | go ((arg, pos) :: nms) with (unArg arg)
195 | go ((arg, pos) :: nms) | MkTPLocal nm =
196 | IPi fc M0 ImplicitArg (Just nm) (Implicit fc True)
197 | $
addConstraint (params pos) nm
199 | go ((arg, pos) :: nms) | MkTPPrim _ = go nms
200 | go ((arg, pos) :: nms) | MkTPApp _ = go nms
201 | go ((arg, pos) :: nms) | MkTPIType = go nms
205 | data HasType : (nm : Name) -> (ty : TTImp) -> Type where
206 | TrustMeHT : HasType nm ty
209 | hasType : Elaboration m => (nm : Name) ->
210 | m (Maybe (ty : TTImp ** HasType nm ty))
211 | hasType nm = catch $
do
212 | [(_, ty)] <- getType nm
213 | | _ => fail "Ambiguous name"
214 | pure (
ty ** TrustMeHT)
218 | data IsProvable : (ty : TTImp) -> Type where
219 | TrustMeIP : IsProvable ty
222 | isProvable : Elaboration m => (ty : TTImp) ->
223 | m (Maybe (IsProvable ty))
224 | isProvable ty = catch $
do
225 | ty <- check {expected = Type} ty
226 | ignore $
check {expected = ty} `(%search)
233 | data HasImplementation : (intf : a -> Type) -> TTImp -> Type where
234 | TrustMeHI : HasImplementation intf t
238 | assert_hasImplementation : HasImplementation intf t
239 | assert_hasImplementation = TrustMeHI
246 | hasImplementation : Elaboration m => (intf : a -> Type) -> (t : TTImp) ->
247 | m (Maybe (HasImplementation intf t))
248 | hasImplementation c t = do
249 | Just prf <- catch $
isFamily t
250 | | _ => Nothing <$ logMsg "derive.common.hasImplementation" 100
251 | "\{show t} is not a Type"
252 | Just intf <- catch $
quote c
253 | | _ => Nothing <$ logMsg "derive.common.hasImplementation" 100
254 | "Could not quote constraint"
255 | Just ty <- catch $
check {expected = Type} $
256 | withParams emptyFC (const Nothing) prf.parameterNames `(~(intf) ~(t))
257 | | _ => Nothing <$ logMsg "derive.common.hasImplementation" 100
258 | "\{show (`(~(intf) ~(t)))} is not a Type"
260 | Just _ <- catch $
check {expected = ty} `(%search)
261 | | _ => Nothing <$ logMsg "derive.common.hasImplementation" 100
262 | "Could not find an implementation of \{show (`(~(intf) ~(t)))}"
263 | pure (Just TrustMeHI)
270 | optionallyEta : FC -> Maybe TTImp -> (TTImp -> TTImp) -> TTImp
271 | optionallyEta fc (Just t) f = f t
272 | optionallyEta fc Nothing f =
273 | let tnm = UN $
Basic "t" in
274 | ILam fc MW ExplicitArg (Just tnm) (Implicit fc False) $
279 | apply : FC -> TTImp -> List TTImp -> TTImp
280 | apply fc t ts = apply t (map (Arg fc) ts)
284 | cleanup : TTImp -> TTImp
286 | IVar fc n => IVar fc (dropNS n)
291 | freshName : List TypeParameter -> String -> String
292 | freshName ns a = assert_total $
go (basicNames $
concatMap typeParameterNames ns) Nothing where
293 | typeParameterNames : TypeParameter -> List Name
294 | typeParameterNames (MkTPLocal a) = [a]
295 | typeParameterNames (MkTPPrim c) = []
296 | typeParameterNames (MkTPApp (n, tp)) = assert_total
297 | $
n :: concatMap (typeParameterNames . unArg) tp
298 | typeParameterNames MkTPIType = []
300 | basicNames : List Name -> List String
301 | basicNames names = mapMaybe (toBasic . dropNS) names where
302 | toBasic : Name -> Maybe String
303 | toBasic (UN (Basic str)) = Just str
304 | toBasic _ = Nothing
307 | go : List String -> Maybe Nat -> String
309 | let name = a ++ maybe "" show counter in
310 | if name `elem` names
311 | then go names (Just $
maybe 0 S counter)