idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] deriving Functor (#2568)

Browse Source
This commit is contained in:
G. Allais 2022-07-04 08:58:18 +01:00 committed by GitHub
parent ea7e43ad74
commit aeeb338e6c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
10 changed files with 878 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

491
libs/base/Deriving/Functor.idr Normal file
View File

@ -0,0 +1,491 @@
||| Deriving functor instances using reflection
||| You can for instance define:
||| ```
||| data Tree a = Leaf a | Node (Tree a) (Tree a)
||| treeFunctor : Functor Tree
||| treeFunctor = %runElab derive
||| ```
module Deriving.Functor
import public Control.Monad.Either
import public Control.Monad.State
import public Data.Maybe
import public Decidable.Equality
import public Language.Reflection
%language ElabReflection
%default total
freshName : List Name -> String -> String
freshName ns a = assert_total $ go (basicNames ns) Nothing where
basicNames : List Name -> List String
basicNames = mapMaybe $ \ nm => case dropNS nm of
UN (Basic str) => Just str
_ => Nothing
covering
go : List String -> Maybe Nat -> String
go ns mi =
let nm = a ++ maybe "" show mi in
ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
------------------------------------------------------------------------------
-- Errors
||| Possible errors for the functor-deriving machinery.
public export
data Error : Type where
NegativeOccurence : Name -> TTImp -> Error
NotAnApplication : TTImp -> Error
NotAFunctor : TTImp -> Error
NotABifunctor : TTImp -> Error
NotAFunctorInItsLastArg : TTImp -> Error
UnsupportedType : TTImp -> Error
InvalidGoal : Error
ConfusingReturnType : Error
-- Contextual information
WhenCheckingConstructor : Name -> Error -> Error
WhenCheckingArg : TTImp -> Error -> Error
export
Show Error where
show = joinBy "\n" . go [<] where
go : SnocList String -> Error -> List String
go acc (NegativeOccurence a ty) = acc <>> ["Negative occurence of \{show a} in \{show ty}"]
go acc (NotAnApplication s) = acc <>> ["The type \{show s} is not an application"]
go acc (NotAFunctor s) = acc <>> ["Couldn't find a `Functor' instance for the type constructor \{show s}"]
go acc (NotABifunctor s) = acc <>> ["Couldn't find a `Bifunctor' instance for the type constructor \{show s}"]
go acc (NotAFunctorInItsLastArg s) = acc <>> ["Not a functor in its last argument \{show s}"]
go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
go acc InvalidGoal = acc <>> ["Expected a goal of the form `Functor f`"]
go acc ConfusingReturnType = acc <>> ["Confusing telescope"]
go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
go acc (WhenCheckingArg s err) = go (acc :< "When checking argument of type \{show s}") err
------------------------------------------------------------------------------
-- Preliminaries: satisfying an interface
--
-- In order to derive Functor for `data Tree a = Node (List (Tree a))`, we need
-- to make sure that `Functor List` already exists. This is done using the following
-- convenience functions.
record IsType where
constructor MkIsType
typeConstructor : Name
parameterNames : List (Name, Nat)
dataConstructors : List (Name, TTImp)
wording : NameType -> String
wording Bound = "a bound variable"
wording Func = "a function name"
wording (DataCon tag arity) = "a data constructor"
wording (TyCon tag arity) = "a type constructor"
isTypeCon : Elaboration m => Name -> m (List (Name, TTImp))
isTypeCon ty = do
[(_, MkNameInfo (TyCon _ _))] <- getInfo ty
| [] => fail "\{show ty} out of scope"
| [(_, MkNameInfo nt)] => fail "\{show ty} is \{wording nt} rather than a type constructor"
| _ => fail "\{show ty} is ambiguous"
cs <- getCons ty
for cs $ \ n => do
[(_, ty)] <- getType n
| _ => fail "\{show n} is ambiguous"
pure (n, ty)
isType : Elaboration m => TTImp -> m IsType
isType = go Z where
go : Nat -> TTImp -> m IsType
go idx (IVar _ n) = MkIsType n [] <$> isTypeCon n
go idx (IApp _ t (IVar _ nm)) = case nm of
-- Unqualified: that's a local variable
UN (Basic _) => { parameterNames $= ((nm, idx) ::) } <$> go (S idx) t
_ => go (S idx) t
go idx t = fail "Expected a type constructor, got: \{show t}"
record Parameters where
constructor MkParameters
asFunctors : List Nat
asBifunctors : List Nat
initParameters : Parameters
initParameters = MkParameters [] []
withParams : FC -> Parameters -> List (Name, Nat) -> TTImp -> TTImp
withParams fc params nms t = go nms where
addConstraint : Bool -> Name -> Name -> TTImp -> TTImp
addConstraint False _ _ = id
addConstraint True cst nm =
let ty = IApp fc (IVar fc cst) (IVar fc nm) in
IPi fc MW AutoImplicit Nothing ty
go : List (Name, Nat) -> TTImp
go [] = t
go ((nm, pos) :: nms)
= IPi fc M0 ImplicitArg (Just nm) (Implicit fc True)
$ addConstraint (pos `elem` params.asFunctors) `{Prelude.Interfaces.Functor} nm
$ addConstraint (pos `elem` params.asBifunctors) `{Prelude.Interfaces.Bifunctor} nm
$ go nms
||| Type of proofs that a type satisfies a constraint.
||| Internally it's vacuous. We don't export the constructor so
||| that users cannot manufacture buggy proofs.
export
data HasImplementation : (intf : a -> Type) -> TTImp -> Type where
TrustMeHI : HasImplementation intf t
||| Given
||| @ intf an interface (e.g. `Functor`, or `Bifunctor`)
||| @ t a term corresponding to a (possibly partially applied) type constructor
||| check whether Idris2 can find a proof that t satisfies the interface.
export
hasImplementation : Elaboration m => (intf : a -> Type) -> (t : TTImp) ->
m (Maybe (HasImplementation intf t))
hasImplementation c t = catch $ do
prf <- isType t
intf <- quote c
ty <- check {expected = Type} $ withParams emptyFC initParameters prf.parameterNames `(~(intf) ~(t))
ignore $ check {expected = ty} `(%search)
pure TrustMeHI
------------------------------------------------------------------------------
-- Core machinery: being functorial
||| IsFunctorialIn is parametrised by
||| @ t the name of the data type whose constructors are being analysed
||| @ x the name of the type variable that the functioral action will change
||| @ ty the type being analysed
||| The inductive type delivers a proof that x occurs positively in ty,
||| assuming that t also is positive.
public export
data IsFunctorialIn : (t, x : Name) -> (ty : TTImp) -> Type
||| FreeOf is parametrised by
||| @ x the name of the type variable that the functioral action will change
||| @ ty the type that does not contain any mention of x
export
data FreeOf : (x : Name) -> (ty : TTImp) -> Type
data IsFunctorialIn : (t, x : Name) -> TTImp -> Type where
||| The type variable x occurs alone
FIVar : IsFunctorialIn t x (IVar fc x)
||| There is a recursive subtree of type (t a1 ... an u) and u is functorial in x.
||| We do not insist that u is exactly x so that we can deal with nested types
||| like the following:
||| data Full a = Leaf a | Node (Full (a, a))
||| data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))
FIRec : (0 _ : IsAppView (_, t) _ f) -> IsFunctorialIn t x arg -> IsFunctorialIn t x (IApp fc f arg)
||| The subterm is delayed (either Inf or Lazy)
FIDelayed : IsFunctorialIn t x ty -> IsFunctorialIn t x (IDelayed fc lr ty)
||| There are nested subtrees somewhere inside a 3rd party type constructor
||| which satisfies the Bifunctor interface
FIBifun : HasImplementation Bifunctor sp ->
IsFunctorialIn t x arg1 -> Either (IsFunctorialIn t x arg2) (FreeOf x arg2) ->
IsFunctorialIn t x (IApp fc1 (IApp fc2 sp arg1) arg2)
||| There are nested subtrees somewhere inside a 3rd party type constructor
||| which satisfies the Functor interface
FIFun : HasImplementation Functor sp ->
IsFunctorialIn t x arg -> IsFunctorialIn t x (IApp fc sp arg)
||| A pi type, with no negative occurence of x in its domain
FIPi : FreeOf x a -> IsFunctorialIn t x b -> IsFunctorialIn t x (IPi fc rig pinfo nm a b)
||| A type free of x is trivially Functorial in it
FIFree : FreeOf x a -> IsFunctorialIn t x a
data FreeOf : Name -> TTImp -> Type where
||| For now we do not bother keeping precise track of the proof that a type
||| is free of x
TrustMeFO : FreeOf a x
elemPos : Eq a => a -> List a -> Maybe Nat
elemPos x = go 0 where
go : Nat -> List a -> Maybe Nat
go idx [] = Nothing
go idx (y :: ys) = idx <$ guard (x == y) <|> go (S idx) ys
parameters
{0 m : Type -> Type}
{auto elab : Elaboration m}
{auto error : MonadError Error m}
{auto cs : MonadState Parameters m}
(t : Name)
(ps : List Name)
(x : Name)
||| When analysing the type of a constructor for the type family t,
||| we hope to observe
||| 1. either that it is functorial in x
||| 2. or that it is free of x
||| If if it is not the case, we will use the `MonadError Error` constraint
||| to fail with an informative message.
public export
TypeView : TTImp -> Type
TypeView ty = Either (IsFunctorialIn t x ty) (FreeOf x ty)
||| Hoping to observe that ty is functorial
export
typeView : (ty : TTImp) -> m (TypeView ty)
||| To avoid code duplication in typeView, we have an auxiliary function
||| specifically to handle the application case
typeAppView : {fc : FC} -> (f, arg : TTImp) -> m (TypeView (IApp fc f arg))
typeAppView {fc} f arg = do
chka <- typeView arg
case chka of
-- if x is present in the argument then the function better be:
-- 1. either an occurrence of t i.e. a subterm
-- 2. or a type constructor already known to be functorial
Left sp => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case decEq t hd of
Yes Refl => pure $ Left (FIRec prf sp)
No diff => case !(hasImplementation Functor f) of
Just prf => pure (Left (FIFun prf sp))
Nothing => case hd `elemPos` ps of
Just n => do
-- record that the nth parameter should be functorial
ns <- gets asFunctors
let ns = ifThenElse (n `elem` ns) ns (n :: ns)
modify { asFunctors := ns }
-- and happily succeed
logMsg "derive.functor.assumption" 10 $
"I am assuming that the parameter \{show hd} is a Functor"
pure (Left (FIFun TrustMeHI sp))
Nothing => throwError (NotAFunctor f)
-- Otherwise it better be the case that f is also free of x so that
-- we can mark the whole type as being x-free.
Right fo => do
Right _ <- typeView f
| _ => throwError (NotAFunctorInItsLastArg (IApp fc f arg))
pure (Right TrustMeFO)
typeView (IVar fc y) = pure $ case decEq x y of
Yes Refl => Left FIVar
No _ => Right TrustMeFO
typeView ty@(IPi fc rig pinfo nm a b) = do
Right p <- typeView a
| _ => throwError (NegativeOccurence x ty)
Left q <- typeView b
| _ => pure (Right TrustMeFO)
pure (Left (FIPi p q))
typeView fa@(IApp _ (IApp _ f arg1) arg2) = do
chka1 <- typeView arg1
case chka1 of
Right _ => typeAppView (assert_smaller fa (IApp _ f arg1)) arg2
Left sp => case !(hasImplementation Bifunctor f) of
Just prf => pure (Left (FIBifun prf sp !(typeView arg2)))
Nothing => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case hd `elemPos` ps of
Just n => do
-- record that the nth parameter should be bifunctorial
ns <- gets asBifunctors
let ns = ifThenElse (n `elem` ns) ns (n :: ns)
modify { asBifunctors := ns }
-- and happily succeed
logMsg "derive.functor.assumption" 10 $
"I am assuming that the parameter \{show hd} is a Bifunctor"
pure (Left (FIBifun TrustMeHI sp !(typeView arg2)))
Nothing => throwError (NotABifunctor f)
typeView fa@(IApp _ f arg) = typeAppView f arg
typeView (IDelayed _ lz f) = pure $ case !(typeView f) of
Left sp => Left (FIDelayed sp)
Right _ => Right TrustMeFO
typeView (IPrimVal _ _) = pure (Right TrustMeFO)
typeView (IType _) = pure (Right TrustMeFO)
typeView ty = throwError (UnsupportedType ty)
------------------------------------------------------------------------------
-- Core machinery: building the mapping function from an IsFunctorialIn proof
||| We often apply multiple arguments, this makes things simpler
apply : FC -> TTImp -> List TTImp -> TTImp
apply fc = foldl (IApp fc)
parameters (fc : FC) (mutualWith : List Name)
||| functorFun takes
||| @ mutualWith a list of mutually defined type constructors. Calls to their
||| respective mapping functions typically need an assert_total because the
||| termination checker is not doing enough inlining to see that things are
||| terminating
||| @ assert records whether we should mark recursive calls as total because
||| we are currently constructing the argument to a higher order function
||| which will obscure the termination argument. Starts as `Nothing`, becomes
||| `Just False` if an `assert_total` has already been inserted.
||| @ ty the type being transformed by the mapping function
||| @ rec the name of the mapping function being defined (used for recursive calls)
||| @ f the name of the function we're mapping
||| @ arg the (optional) name of the argument being mapped over. This lets us use
||| Nothing when generating arguments to higher order functions so that we generate
||| the eta contracted `map (mapTree f)` instead of `map (\ ts => mapTree f ts)`.
functorFun : (assert : Maybe Bool) -> {ty : TTImp} -> IsFunctorialIn t x ty ->
(rec, f : Name) -> (arg : Maybe TTImp) -> TTImp
functorFun assert FIVar rec f t = apply fc (IVar fc f) (toList t)
functorFun assert (FIRec y sp) rec f t
-- only add assert_total if it is declared to be needed
= ifThenElse (fromMaybe False assert) (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
$ apply fc (IVar fc rec) (functorFun (Just False) sp rec f Nothing :: toList t)
functorFun assert (FIDelayed sp) rec f Nothing
-- here we need to eta-expand to avoid "Lazy t does not unify with t" errors
= let nm = UN $ Basic "eta" in
ILam fc MW ExplicitArg (Just nm) (Implicit fc False)
$ IDelay fc
$ functorFun assert sp rec f (Just (IVar fc nm))
functorFun assert (FIDelayed sp) rec f (Just t) = functorFun assert sp rec f (Just t)
functorFun assert {ty = IApp _ ty _} (FIFun _ sp) rec f t
-- only add assert_total if we are calling a mutually defined Functor implementation.
= let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
ifThenElse isMutual (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
$ apply fc (IVar fc (UN $ Basic "map"))
(functorFun ((False <$ guard isMutual) <|> assert <|> Just True) sp rec f Nothing
:: toList t)
functorFun assert (FIBifun _ sp1 (Left sp2)) rec f t
= apply fc (IVar fc (UN $ Basic "bimap"))
(functorFun (assert <|> Just True) sp1 rec f Nothing
:: functorFun (assert <|> Just True) sp2 rec f Nothing
:: toList t)
functorFun assert (FIBifun _ sp (Right _)) rec f t
= apply fc (IVar fc (UN $ Basic "mapFst"))
(functorFun (assert <|> Just True) sp rec f Nothing
:: toList t)
functorFun assert (FIPi {rig, pinfo, nm} _ sp) rec f (Just t)
= let nm = fromMaybe (UN $ Basic "x") nm in
-- /!\ We cannot use the type stored in FIPi here because it could just
-- be a name that will happen to be different when bound on the LHS!
-- Cf. the Free test case in reflection017
ILam fc rig pinfo (Just nm) (Implicit fc False)
$ functorFun assert sp rec f (Just $ IApp fc t (IVar fc nm))
functorFun assert (FIPi {rig, pinfo, nm} _ sp) rec f Nothing
= let tnm = UN $ Basic "t" in
let nm = fromMaybe (UN $ Basic "x") nm in
ILam fc MW ExplicitArg (Just tnm) (Implicit fc False) $
-- /!\ We cannot use the type stored in FIPi here because it could just
-- be a name that will happen to be different when bound on the LHS!
-- Cf. the Free test case in reflection017
ILam fc rig pinfo (Just nm) (Implicit fc False) $
functorFun assert sp rec f (Just $ IApp fc (IVar fc tnm) (IVar fc nm))
functorFun assert (FIFree y) rec f t = fromMaybe `(id) t
------------------------------------------------------------------------------
-- User-facing: Functor deriving
record ConstructorView where
constructor MkConstructorView
params : List Name
functorPara : Name
conArgTypes : List TTImp
explicits : TTImp -> Maybe ConstructorView
explicits (IPi fc rig ExplicitArg x a b) = { conArgTypes $= (a ::) } <$> explicits b
explicits (IPi fc rig pinfo x a b) = explicits b
explicits (IApp _ f (IVar _ a)) = do
MkAppView _ ts _ <- appView f
let ps = flip mapMaybe ts $ \ t => the (Maybe Name) $ case t of
Arg _ (IVar _ nm) => Just nm
_ => Nothing
pure (MkConstructorView (ps <>> []) a [])
explicits _ = Nothing
cleanup : TTImp -> TTImp
cleanup = \case
IVar fc n => IVar fc (dropNS n)
t => t
namespace Functor
derive' : (Elaboration m, MonadError Error m) =>
{default Private vis : Visibility} ->
{default Total treq : TotalReq} ->
{default [] mutualWith : List Name} ->
m (Functor f)
derive' = do
-- expand the mutualwith names to have the internal, fully qualified, names
mutualWith <- map concat $ for mutualWith $ \ nm => do
ntys <- getType nm
pure (fst <$> ntys)
-- The goal should have the shape (Functor t)
Just (IApp _ (IVar _ functor) t) <- goal
| _ => throwError InvalidGoal
when (`{Prelude.Interfaces.Functor} /= functor) $
logMsg "derive.functor" 1 "Expected to derive Functor but got \{show functor}"
-- t should be a type constructor
logMsg "derive.functor" 1 "Deriving Functor for \{showPrec App $ mapTTImp cleanup t}"
MkIsType f params cs <- isType t
logMsg "derive.functor.constructors" 1 $
joinBy "\n" $ "" :: map (\ (n, ty) => " \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
-- Generate a clause for each data constructor
let fc = emptyFC
let un = UN . Basic
let mapName = un ("map" ++ show (dropNS f))
let funName = un "f"
let fun = IVar fc funName
(ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
withError (WhenCheckingConstructor cName) $ do
-- Grab the types of the constructor's explicit arguments
let Just (MkConstructorView paras para args) = explicits ty
| _ => throwError ConfusingReturnType
logMsg "derive.functor.clauses" 10 $
"\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup) args)})"
let vars = map (IVar fc . un . ("x" ++) . show . (`minus` 1))
$ zipWith const [1..length args] args -- fix because [1..0] is [1,0]
recs <- for (zip vars args) $ \ (v, arg) => do
res <- withError (WhenCheckingArg (mapTTImp cleanup arg)) $
typeView f paras para arg
pure $ case res of
Left sp => functorFun fc mutualWith Nothing sp mapName funName (Just v)
Right free => v
pure $ PatClause fc
(apply fc (IVar fc mapName) [ fun, apply fc (IVar fc cName) vars])
(apply fc (IVar fc cName) recs)
-- Generate the type of the mapping function
let paramNames = fst <$> params
let a = un $ freshName paramNames "a"
let b = un $ freshName paramNames "b"
let va = IVar fc a
let vb = IVar fc b
let ty = MkTy fc fc mapName $ withParams fc ns params
$ IPi fc M0 ImplicitArg (Just a) (IType fc)
$ IPi fc M0 ImplicitArg (Just b) (IType fc)
$ `((~(va) -> ~(vb)) -> ~(t) ~(va) -> ~(t) ~(vb))
logMsg "derive.functor.clauses" 1 $
joinBy "\n" ("" :: (" " ++ show (mapITy cleanup ty))
:: map ((" " ++) . showClause InDecl . mapClause cleanup) cls)
-- Define the instance
check $ ILocal fc
[ IClaim fc MW vis [Totality treq] ty
, IDef fc mapName cls
] `(MkFunctor {f = ~(t)} ~(IVar fc mapName))
||| Derive an implementation of Functor for a type constructor.
||| This can be used like so:
||| ```
||| data Tree a = Leaf a | Node (Tree a) (Tree a)
||| treeFunctor : Functor Tree
||| treeFunctor = %runElab derive
||| ```
export
derive : {default Private vis : Visibility} ->
{default Total treq : TotalReq} ->
{default [] mutualWith : List Name} ->
Elab (Functor f)
derive = do
res <- runEitherT {e = Error, m = Elab} (derive' {vis, treq, mutualWith})
case res of
Left err => fail (show err)
Right prf => pure prf

11
libs/base/Language/Reflection.idr
View File

@ -205,3 +205,14 @@ Elaboration m => MonadTrans t => Monad (t m) => Elaboration (t m) where
getLocalType = lift . getLocalType
getCons = lift . getCons
declare = lift . declare
||| Catch failures and use the `Maybe` monad instead
export
catch : Elaboration m => Elab a -> m (Maybe a)
catch elab = try (Just <$> elab) (pure Nothing)
||| Run proof search to attempt to find a value of the input type.
||| Useful to check whether a give interface constraint is satisfied.
export
search : Elaboration m => (ty : Type) -> m (Maybe ty)
search ty = catch $ check {expected = ty} `(%search)

55
libs/base/Language/Reflection/TTImp.idr
View File

@ -462,6 +462,8 @@ Eq TTImp where
_ == _ = False
public export
data Mode = InDecl | InCase
mutual
@ -507,7 +509,7 @@ mutual
= unwords [ show vis
, showTotalReq treq (show dt)
]
show (IDef fc nm xs) = joinBy "; " (map show xs)
show (IDef fc nm xs) = joinBy "; " (map (showClause InDecl) xs)
show (IParameters fc params decls)
= unwords
[ "parameters"
@ -538,16 +540,19 @@ mutual
show (ISetFieldApp path s) = "\{joinBy "->" path} $= \{show s}"
export
Show Clause where
show (PatClause fc lhs rhs) = "\{show lhs} => \{show rhs}"
show (WithClause fc lhs rig wval prf flags cls) -- TODO print flags
showClause : Mode -> Clause -> String
showClause mode (PatClause fc lhs rhs) = "\{show lhs} \{showSep mode} \{show rhs}" where
showSep : Mode -> String
showSep InDecl = "="
showSep InCase = "=>"
showClause mode (WithClause fc lhs rig wval prf flags cls) -- TODO print flags
= unwords
[ show lhs, "with"
, showCount rig $ maybe id (\ nm => (++ " proof \{show nm}")) prf
$ showParens True (show wval)
, "{", joinBy "; " (assert_total $ map show cls), "}"
, "{", joinBy "; " (assert_total $ map (showClause mode) cls), "}"
]
show (ImpossibleClause fc lhs) = "\{show lhs} impossible"
showClause mode (ImpossibleClause fc lhs) = "\{show lhs} impossible"
collectPis : Count -> PiInfo TTImp -> SnocList Name -> TTImp -> TTImp -> (List Name, TTImp)
collectPis rig pinfo xs argTy t@(IPi fc rig' pinfo' x argTy' retTy)
@ -568,6 +573,8 @@ mutual
showPrec d (IVar fc nm) = showPrefix True nm
showPrec d (IPi fc MW ExplicitArg Nothing argTy retTy)
= showParens (d > Open) $ "\{showPrec Dollar argTy} -> \{show retTy}"
showPrec d (IPi fc MW AutoImplicit Nothing argTy retTy)
= showParens (d > Open) $ "\{showPrec Dollar argTy} => \{show retTy}"
showPrec d (IPi fc rig pinfo x argTy retTy)
= showParens (d > Open) $
let (xs, retTy) = collectPis rig pinfo [<fromMaybe (UN Underscore) x] argTy retTy in
@ -582,7 +589,7 @@ mutual
showPrec d (ICase fc s ty xs)
= showParens (d > Open) $
unwords $ [ "case", show s ] ++ typeFor ty ++ [ "of", "{"
, joinBy "; " (assert_total $ map show xs)
, joinBy "; " (assert_total $ map (showClause InCase) xs)
, "}"
]
where
@ -633,6 +640,40 @@ mutual
[(_,x)] => "with \{show x} \{show s}"
_ => "with [\{joinBy ", " $ map (show . snd) ns}] \{show s}"
public export
data Argument a
= Arg FC a
| NamedArg FC Name a
| AutoArg FC a
public export
data IsAppView : (FC, Name) -> SnocList (Argument TTImp) -> TTImp -> Type where
AVVar : IsAppView (fc, t) [<] (IVar fc t)
AVApp : IsAppView x ts f -> IsAppView x (ts :< Arg fc t) (IApp fc f t)
AVNamedApp : IsAppView x ts f -> IsAppView x (ts :< NamedArg fc n t) (INamedApp fc f n t)
AVAutoApp : IsAppView x ts f -> IsAppView x (ts :< AutoArg fc t) (IAutoApp fc f a)
public export
record AppView (t : TTImp) where
constructor MkAppView
head : (FC, Name)
args : SnocList (Argument TTImp)
0 isAppView : IsAppView head args t
export
appView : (t : TTImp) -> Maybe (AppView t)
appView (IVar fc f) = Just (MkAppView (fc, f) [<] AVVar)
appView (IApp fc f t) = do
(MkAppView x ts prf) <- appView f
pure (MkAppView x (ts :< Arg fc t) (AVApp prf))
appView (INamedApp fc f n t) = do
(MkAppView x ts prf) <- appView f
pure (MkAppView x (ts :< NamedArg fc n t) (AVNamedApp prf))
appView (IAutoApp fc f t) = do
(MkAppView x ts prf) <- appView f
pure (MkAppView x (ts :< AutoArg fc t) (AVAutoApp prf))
appView _ = Nothing
parameters (f : TTImp -> TTImp)
export

2
libs/base/base.ipkg
View File

@ -85,6 +85,8 @@ modules = Control.App,
Debug.Trace,
Deriving.Functor,
Decidable.Decidable,
Decidable.Equality,
Decidable.Equality.Core,

9
src/TTImp/Elab/RunElab.idr
View File

@ -104,7 +104,13 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp
x => x
throw $ RunElabFail $ GenericMsg customFC !(reify defs msg')
elabCon defs "Try" [_, elab1, elab2]
= tryUnify (elabScript fc nest env !(evalClosure defs elab1) exp)
= tryUnify (do constart <- getNextEntry
res <- elabScript fc nest env !(evalClosure defs elab1) exp
-- We ensure that all of the constraints introduced during the elab script
-- have been solved. This guarantees that we do not mistakenly succeed even
-- though e.g. a proof search got delayed.
solveConstraintsAfter constart inTerm LastChance
pure res)
(elabScript fc nest env !(evalClosure defs elab2) exp)
elabCon defs "LogMsg" [topic, verb, str]
= do topic' <- evalClosure defs topic
@ -244,6 +250,7 @@ checkRunElab rig elabinfo nest env fc script exp
elabtt <- appCon fc defs n [expected]
(stm, sty) <- runDelays (const True) $
check rig elabinfo nest env script (Just (gnf env elabtt))
solveConstraints inTerm Normal
defs <- get Ctxt -- checking might have resolved some holes
ntm <- elabScript fc nest env
!(nfOpts withAll defs env stm) (Just (gnf env expected))

3
tests/Main.idr
View File

@ -220,7 +220,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing
["reflection001", "reflection002", "reflection003", "reflection004",
"reflection005", "reflection006", "reflection007", "reflection008",
"reflection009", "reflection010", "reflection011", "reflection012",
"reflection013", "reflection014", "reflection015", "reflection016"
"reflection013", "reflection014", "reflection015", "reflection016",
"reflection017"
]
idrisTestsWith : TestPool

222
tests/idris2/reflection017/DeriveFunctor.idr Normal file
View File

@ -0,0 +1,222 @@
module DeriveFunctor
import Deriving.Functor
%language ElabReflection
%default covering
%logging "derive.functor.clauses" 1
%logging "derive.functor.assumption" 10
list : Functor List
list = %runElab derive
maybe : Functor Maybe
maybe = %runElab derive
either : Functor (Either err)
either = %runElab derive
namespace Constant
record Constant (a, b : Type) where
constructor MkConstant
runConstant : a
constant : Functor (Constant a)
constant = %runElab derive
namespace Vect
public export
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect n a -> Vect (S n) a
export %hint
total
vect : Functor (Vect n)
vect = %runElab derive
namespace BigTree
data BigTree a
= End a
| Branch String (List a) (Bool -> BigTree a)
| Rose (List (BigTree a))
total
bigTree : Functor BigTree
bigTree = %runElab derive
namespace Matrix
record Matrix m n a where
constructor MkMatrix
runMatrix : Vect m (Vect n a)
total
matrix : Functor (Matrix m n)
matrix = %runElab derive
namespace Tm
data Op : Nat -> Type where
Neg : Op 1
Add : Op 2
data Tm : Type -> Type where
Var : a -> Tm a
Call : Op n -> Vect n (Tm a) -> Tm a
Lam : Tm (Maybe a) -> Tm a
total
tm : Functor Tm
tm = %runElab derive
namespace Forest
data Tree : Type -> Type
data Forest : Type -> Type
data Tree : Type -> Type where
Leaf : a -> Tree a
Node : Forest a -> Tree a
data Forest : Type -> Type where
Empty : Forest a
Plant : Tree a -> Forest a -> Forest a
%hint total tree : Functor Tree
%hint total forest : Functor Forest
tree = %runElab derive {mutualWith = [`{Forest}]}
forest = %runElab derive {mutualWith = [`{Tree}]}
namespace List1
data List1 : Type -> Type where
MkList1 : (a, Maybe (List1 a)) -> List1 a
total
list1 : Functor List1
list1 = %runElab derive
namespace Full
data Full a = Leaf a | Node (Full (a, a))
total
full : Functor Full
full = %runElab derive
failing "Negative occurence of a"
data NOT : Type -> Type where
MkNOT : (a -> Void) -> NOT a
total
negative : Functor NOT
negative = %runElab derive
namespace Colist
data Colist a = Nil | (::) a (Inf (Colist a))
total
colist : Functor Colist
colist = %runElab derive
namespace LAZY
record LAZY (a : Type) where
constructor MkLAZY
wrapped : Lazy a
total
lazy : Functor LAZY
lazy = %runElab derive
namespace Rose
data Rose a = Node (List (Lazy (Rose a)))
total
rose : Functor Rose
rose = %runElab derive
namespace Free
data Free : (Type -> Type) -> Type -> Type where
Pure : a -> Free f a
Bind : f a -> (a -> Free f b) -> Free f b
total
free : Functor (Free f)
free = %runElab derive
namespace MaybeT
record MaybeT (m : Type -> Type) (a : Type) where
constructor MkMaybeT
runMaybeT : m (Maybe a)
total
maybeT : Functor m => Functor (MaybeT m)
maybeT = %runElab derive
namespace TreeT
data TreeT : (Type -> Type -> Type) -> Type -> Type where
MkTreeT : layer a (TreeT layer a) -> TreeT layer a
%hint
treeT : Bifunctor layer => Functor (TreeT layer)
treeT = %runElab derive {treq = CoveringOnly}
record Tree (a : Type) where
constructor MkTree
runTree : TreeT Either a
tree : Functor Tree
tree = %runElab derive {treq = CoveringOnly}
failing "Couldn't find a `Functor' instance for the type constructor DeriveFunctor.Wrap"
record Wrap (a : Type) where
constructor MkWrap
unWrap : a
data Indirect : Type -> Type where
MkIndirect : Wrap a -> Indirect a
total
indirect : Functor Indirect
indirect = %runElab derive
namespace BifunctorFail
data Tree : (l, n : Type) -> Type where
Leaf : l -> Tree l n
Node : Tree l n -> n -> Tree l n -> Tree l n
-- this one will succeed
total
tree : Functor (Tree l)
tree = %runElab derive
failing "Couldn't find a `Bifunctor' instance for the type constructor DeriveFunctor.BifunctorFail.Tree"
record Tree' (a : Type) where
constructor MkTree'
getTree : Tree a a
-- and this one will fail
tree' : Functor Tree'
tree' = %runElab derive
failing "Expected a type constructor, got: Prelude.Basics.id {a = Type}"
total
functor : Functor Prelude.id
functor = %runElab derive

12
tests/idris2/reflection017/Search.idr Normal file
View File

@ -0,0 +1,12 @@
module Search
import Language.Reflection
import Language.Reflection.TTImp
%language ElabReflection
nothing : Maybe (Not Nat)
nothing = %runElab (search ?)
test : Search.nothing === Nothing
test = Refl

78
tests/idris2/reflection017/expected Normal file
View File

@ -0,0 +1,78 @@
1/1: Building DeriveFunctor (DeriveFunctor.idr)
LOG derive.functor.clauses:1:
mapList : {0 a, b : Type} -> (a -> b) -> List a -> List b
mapList f Nil = Nil
mapList f (x0 :: x1) = (f x0) :: (mapList f x1)
LOG derive.functor.clauses:1:
mapMaybe : {0 a, b : Type} -> (a -> b) -> Maybe a -> Maybe b
mapMaybe f Nothing = Nothing
mapMaybe f (Just x0) = Just (f x0)
LOG derive.functor.clauses:1:
mapEither : {0 err : _} -> {0 a, b : Type} -> (a -> b) -> Either err a -> Either err b
mapEither f (Left x0) = Left x0
mapEither f (Right x0) = Right (f x0)
LOG derive.functor.clauses:1:
mapConstant : {0 a : _} -> {0 a0, b : Type} -> (a0 -> b) -> Constant a a0 -> Constant a b
mapConstant f (MkConstant x0) = MkConstant x0
LOG derive.functor.clauses:1:
mapVect : {0 n : _} -> {0 a, b : Type} -> (a -> b) -> Vect n a -> Vect n b
mapVect f Nil = Nil
mapVect f (x0 :: x1) = (f x0) :: (mapVect f x1)
LOG derive.functor.clauses:1:
mapBigTree : {0 a, b : Type} -> (a -> b) -> BigTree a -> BigTree b
mapBigTree f (End x0) = End (f x0)
mapBigTree f (Branch x0 x1 x2) = Branch x0 (map f x1) (\ {arg:4047} => mapBigTree f (x2 {arg:4047}))
mapBigTree f (Rose x0) = Rose (map (assert_total (mapBigTree f)) x0)
LOG derive.functor.clauses:1:
mapMatrix : {0 n, m : _} -> {0 a, b : Type} -> (a -> b) -> Matrix m n a -> Matrix m n b
mapMatrix f (MkMatrix x0) = MkMatrix (map (map f) x0)
LOG derive.functor.clauses:1:
mapTm : {0 a, b : Type} -> (a -> b) -> Tm a -> Tm b
mapTm f (Var x0) = Var (f x0)
mapTm f (Call x0 x1) = Call x0 (map (assert_total (mapTm f)) x1)
mapTm f (Lam x0) = Lam (mapTm (map f) x0)
LOG derive.functor.clauses:1:
mapTree : {0 a, b : Type} -> (a -> b) -> Tree a -> Tree b
mapTree f (Leaf x0) = Leaf (f x0)
mapTree f (Node x0) = Node (assert_total (map f x0))
LOG derive.functor.clauses:1:
mapForest : {0 a, b : Type} -> (a -> b) -> Forest a -> Forest b
mapForest f Empty = Empty
mapForest f (Plant x0 x1) = Plant (assert_total (map f x0)) (mapForest f x1)
LOG derive.functor.clauses:1:
mapList1 : {0 a, b : Type} -> (a -> b) -> List1 a -> List1 b
mapList1 f (MkList1 x0) = MkList1 (bimap f (map (assert_total (mapList1 f))) x0)
LOG derive.functor.clauses:1:
mapFull : {0 a, b : Type} -> (a -> b) -> Full a -> Full b
mapFull f (Leaf x0) = Leaf (f x0)
mapFull f (Node x0) = Node (mapFull (bimap f f) x0)
LOG derive.functor.clauses:1:
mapColist : {0 a, b : Type} -> (a -> b) -> Colist a -> Colist b
mapColist f Nil = Nil
mapColist f (x0 :: x1) = (f x0) :: (mapColist f x1)
LOG derive.functor.clauses:1:
mapLAZY : {0 a, b : Type} -> (a -> b) -> LAZY a -> LAZY b
mapLAZY f (MkLAZY x0) = MkLAZY (f x0)
LOG derive.functor.clauses:1:
mapRose : {0 a, b : Type} -> (a -> b) -> Rose a -> Rose b
mapRose f (Node x0) = Node (map (\ eta => Delay (assert_total (mapRose f eta))) x0)
LOG derive.functor.clauses:1:
mapFree : {0 f : _} -> {0 a, b : Type} -> (a -> b) -> Free f a -> Free f b
mapFree f (Pure x0) = Pure (f x0)
mapFree f (Bind x0 x1) = Bind x0 (\ {arg:5076} => mapFree f (x1 {arg:5076}))
LOG derive.functor.assumption:10: I am assuming that the parameter m is a Functor
LOG derive.functor.clauses:1:
mapMaybeT : {0 m : _} -> Functor m => {0 a, b : Type} -> (a -> b) -> MaybeT m a -> MaybeT m b
mapMaybeT f (MkMaybeT x0) = MkMaybeT (map (map f) x0)
LOG derive.functor.assumption:10: I am assuming that the parameter layer is a Bifunctor
LOG derive.functor.clauses:1:
mapTreeT : {0 layer : _} -> Bifunctor layer => {0 a, b : Type} -> (a -> b) -> TreeT layer a -> TreeT layer b
mapTreeT f (MkTreeT x0) = MkTreeT (bimap f (assert_total (mapTreeT f)) x0)
LOG derive.functor.clauses:1:
mapTree : {0 a, b : Type} -> (a -> b) -> Tree a -> Tree b
mapTree f (MkTree x0) = MkTree (map f x0)
LOG derive.functor.clauses:1:
mapTree : {0 l : _} -> {0 a, b : Type} -> (a -> b) -> Tree l a -> Tree l b
mapTree f (Leaf x0) = Leaf x0
mapTree f (Node x0 x1 x2) = Node (mapTree f x0) (f x1) (mapTree f x2)
1/1: Building Search (Search.idr)

4
tests/idris2/reflection017/run Executable file
View File

@ -0,0 +1,4 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner -c DeriveFunctor.idr
$1 --no-color --console-width 0 --no-banner -c Search.idr