0 | module Deriving.Common
  1 |
  2 | import Data.SnocList
  3 | import Language.Reflection
  4 |
  5 | %default total
  6 |
  7 | ------------------------------------------------------------------------------
  8 | -- Being free of a variable
  9 |
 10 | ||| IsFreeOf is parametrised by
 11 | ||| @ x  the name of the type variable that the functorial action will change
 12 | ||| @ ty the type that does not contain any mention of x
 13 | export
 14 | data IsFreeOf : (x : Name) -> (ty : TTImp) -> Type where
 15 |   ||| For now we do not bother keeping precise track of the proof that a type
 16 |   ||| is free of x
 17 |   TrustMeFO : IsFreeOf a x
 18 |
 19 | ||| We may need to manufacture proofs and so we provide the `assert` escape hatch.
 20 | export %unsafe
 21 | assert_IsFreeOf : IsFreeOf x ty
 22 | assert_IsFreeOf = TrustMeFO
 23 |
 24 | ||| Testing function deciding whether the given term is free of a particular
 25 | ||| variable.
 26 | export
 27 | isFreeOf : (x : Name) -> (ty : TTImp) -> Maybe (IsFreeOf x ty)
 28 | isFreeOf x ty
 29 |   = do isOk <- flip mapMTTImp ty $ \case
 30 |          t@(IVar _ v) => t <$ guard (v /= x)
 31 |          t => pure t
 32 |        pure TrustMeFO
 33 |
 34 | ------------------------------------------------------------------------------
 35 | -- Being a (data) type
 36 |
 37 | public export
 38 | record IsType where
 39 |   constructor MkIsType
 40 |   typeConstructor  : Name
 41 |   parameterNames   : List (Argument Name, Nat)
 42 |   dataConstructors : List (Name, TTImp)
 43 |
 44 | wording : NameType -> String
 45 | wording Bound = "a bound variable"
 46 | wording Func = "a function name"
 47 | wording (DataCon tag arity) = "a data constructor"
 48 | wording (TyCon tag arity) = "a type constructor"
 49 |
 50 | isTypeCon : Elaboration m => FC -> Name -> m (List (Name, TTImp))
 51 | isTypeCon fc ty = do
 52 |     [(_, MkNameInfo (TyCon _ _))] <- getInfo ty
 53 |       | [] => failAt fc "\{show ty} out of scope"
 54 |       | [(_, MkNameInfo nt)] => failAt fc "\{show ty} is \{wording nt} rather than a type constructor"
 55 |       | _ => failAt fc "\{show ty} is ambiguous"
 56 |     cs <- getCons ty
 57 |     for cs $ \ n => do
 58 |       [(_, ty)] <- getType n
 59 |          | _ => failAt fc "\{show n} is ambiguous"
 60 |       pure (n, ty)
 61 |
 62 | export
 63 | isType : Elaboration m => TTImp -> m IsType
 64 | isType = go Z [] where
 65 |
 66 |   go : Nat -> List (Argument Name, Nat) -> TTImp -> m IsType
 67 |   go idx acc (IVar fc n) = MkIsType n (map (map (minus idx . S)) acc) <$> isTypeCon fc n
 68 |   go idx acc (IApp _ t (IVar _ nm)) = case nm of
 69 |     -- Unqualified: that's a local variable
 70 |     UN (Basic _) => go (S idx) ((Arg emptyFC nm, idx) :: acc) t
 71 |     _ => go (S idx) acc t
 72 |   go idx acc (INamedApp _ t nm (IVar _ nm')) = case nm' of
 73 |     -- Unqualified: that's a local variable
 74 |     UN (Basic _) => go (S idx) ((NamedArg emptyFC nm nm', idx) :: acc) t
 75 |     _ => go (S idx) acc t
 76 |   go idx acc (IAutoApp _ t (IVar _ nm)) = case nm of
 77 |     -- Unqualified: that's a local variable
 78 |     UN (Basic _) => go (S idx) ((AutoArg emptyFC nm, idx) :: acc) t
 79 |     _ => go (S idx) acc t
 80 |   go idx acc t = failAt (getFC t) "Expected a type constructor, got: \{show t}"
 81 |
 82 | ------------------------------------------------------------------------------
 83 | -- Being a (data) constructor with a parameter
 84 | -- TODO: generalise?
 85 |
 86 | public export
 87 | record ConstructorView where
 88 |   constructor MkConstructorView
 89 |   params      : SnocList (Name, Nat)
 90 |   conArgTypes : List (Count, Argument TTImp)
 91 |
 92 | export
 93 | constructorView : TTImp -> Maybe ConstructorView
 94 | constructorView (IPi fc rig pinfo x a b) = do
 95 |   let Just arg = fromPiInfo fc pinfo x a
 96 |     | Nothing => constructorView b -- this better be a boring argument...
 97 |   let True = rig /= M1
 98 |     | False => constructorView b -- this better be another boring argument...
 99 |   { conArgTypes $= ((rig, arg) ::) } <$> constructorView b
100 | constructorView f = do
101 |   MkAppView _ ts _ <- appView f
102 |   let range = [<] <>< [0..minus (length ts) 1]
103 |   let ps = flip mapMaybe (zip ts range) $ \ t => the (Maybe (Name, Nat)) $ case t of
104 |              (Arg _ (IVar _ nm), n) => Just (nm, n)
105 |              _ => Nothing
106 |   pure (MkConstructorView ps [])
107 |
108 | ------------------------------------------------------------------------------
109 | -- Satisfying an interface
110 | --
111 | -- In order to derive Functor for `data Tree a = Node (List (Tree a))`, we need
112 | -- to make sure that `Functor List` already exists. This is done using the following
113 | -- convenience functions.
114 |
115 | export
116 | withParams : FC -> (Nat -> Maybe TTImp) -> List (Argument Name, Nat) -> TTImp -> TTImp
117 | withParams fc params nms t = go nms where
118 |
119 |   addConstraint : Maybe TTImp -> Name -> TTImp -> TTImp
120 |   addConstraint Nothing _ = id
121 |   addConstraint (Just cst) nm =
122 |      let ty = IApp fc cst (IVar fc nm) in
123 |      IPi fc MW AutoImplicit Nothing ty
124 |
125 |   go : List (Argument Name, Nat) -> TTImp
126 |   go [] = t
127 |   go ((arg, pos) :: nms)
128 |     = let nm = unArg arg in
129 |       IPi fc M0 ImplicitArg (Just nm) (Implicit fc True)
130 |     $ addConstraint (params pos) nm
131 |     $ go nms
132 |
133 | ||| Type of proofs that something has a given type
134 | export
135 | data HasType : (nm : Name) -> (ty : TTImp) -> Type where
136 |   TrustMeHT : HasType nm ty
137 |
138 | export
139 | hasType : Elaboration m => (nm : Name) ->
140 |           m (Maybe (ty : TTImp ** HasType nm ty))
141 | hasType nm = catch $ do
142 |   [(_, ty)] <- getType nm
143 |     | _ => fail "Ambiguous name"
144 |   pure (ty ** TrustMeHT)
145 |
146 | ||| Type of proofs that a type is inhabited
147 | export
148 | data IsProvable : (ty : TTImp) -> Type where
149 |   TrustMeIP : IsProvable ty
150 |
151 | export
152 | isProvable : Elaboration m => (ty : TTImp) ->
153 |              m (Maybe (IsProvable ty))
154 | isProvable ty = catch $ do
155 |   ty <- check {expected = Type} ty
156 |   ignore $ check {expected = ty} `(%search)
157 |   pure TrustMeIP
158 |
159 | ||| Type of proofs that a type satisfies a constraint.
160 | ||| Internally it's vacuous. We don't export the constructor so
161 | ||| that users cannot manufacture buggy proofs.
162 | export
163 | data HasImplementation : (intf : a -> Type) -> TTImp -> Type where
164 |   TrustMeHI : HasImplementation intf t
165 |
166 | ||| We may need to manufacture proofs and so we provide the `assert` escape hatch.
167 | export %unsafe
168 | assert_hasImplementation : HasImplementation intf t
169 | assert_hasImplementation = TrustMeHI
170 |
171 | ||| Given
172 | ||| @ intf an interface (e.g. `Functor`, or `Bifunctor`)
173 | ||| @ t    a term corresponding to a (possibly partially applied) type constructor
174 | ||| check whether Idris2 can find a proof that t satisfies the interface.
175 | export
176 | hasImplementation : Elaboration m => (intf : a -> Type) -> (t : TTImp) ->
177 |                     m (Maybe (HasImplementation intf t))
178 | hasImplementation c t = catch $ do
179 |   prf <- isType t
180 |   intf <- quote c
181 |   ty <- check {expected = Type} $ withParams emptyFC (const Nothing) prf.parameterNames `(~(intf) ~(t))
182 |   ignore $ check {expected = ty} `(%search)
183 |   pure TrustMeHI
184 |
185 | ------------------------------------------------------------------------------
186 | -- Utils
187 |
188 | ||| Optionally eta-expand if there is no argument available
189 | export
190 | optionallyEta : FC -> Maybe TTImp -> (TTImp -> TTImp) -> TTImp
191 | optionallyEta fc (Just t) f = f t
192 | optionallyEta fc Nothing f =
193 |   let tnm = UN $ Basic "t" in
194 |   ILam fc MW ExplicitArg (Just tnm) (Implicit fc False) $
195 |   f (IVar fc tnm)
196 |
197 | ||| We often apply multiple arguments, this makes things simpler
198 | export
199 | apply : FC -> TTImp -> List TTImp -> TTImp
200 | apply fc t ts = apply t (map (Arg fc) ts)
201 |
202 | ||| Use unqualified names (useful for more compact printing)
203 | export
204 | cleanup : TTImp -> TTImp
205 | cleanup = \case
206 |   IVar fc n => IVar fc (dropNS n)
207 |   t => t
208 |
209 | ||| Create fresh names
210 | export
211 | freshName : List Name -> String -> String
212 | freshName ns a = assert_total $ go (basicNames ns) Nothing where
213 |
214 |   basicNames : List Name -> List String
215 |   basicNames = mapMaybe $ \ nm => case dropNS nm of
216 |     UN (Basic str) => Just str
217 |     _ => Nothing
218 |
219 |   covering
220 |   go : List String -> Maybe Nat -> String
221 |   go ns mi =
222 |     let nm = a ++ maybe "" show mi in
223 |     ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
224 |