39d643b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'elab-lookup-function-def' of https://github.com/shlevy/Idris-dev into shlevy-elab-lookup-function-def

39d643bDavid Raymond Christiansen11 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -571,6 +571,9 @@ Extra-source-files:

571 test/meta002/run

572 test/meta002/*.idr

573 test/meta002/expected

574+ test/meta004/run

575+ test/meta004/*.idr

576+ test/meta004/expected

574

577

575 test/primitives001/run

578 test/primitives001/run

576 test/primitives001/*.idr

579 test/primitives001/*.idr

libs/prelude/Language/Reflection/Elab.idr+21−8

@@ -69,17 +69,16 @@ record TyDecl where

69 returnType : Raw

72−-- Note: FunClause is not a record because impossible clauses may be

73−-- added at some point.

74||| A single pattern-matching clause

72||| A single pattern-matching clause

75−data FunClause : Type where

73+data FunClause : Type -> Type where

76− MkFunClause : (lhs, rhs : Raw) -> FunClause

74+ MkFunClause : (lhs, rhs : a) -> FunClause a

75+ MkImpossibleClause : (lhs : a) -> FunClause a

78||| A reflected function definition.

77||| A reflected function definition.

79−record FunDefn where

78+record FunDefn a where

80 constructor DefineFun

79 constructor DefineFun

81 name : TTName

80 name : TTName

82− clauses : List FunClause

81+ clauses : List (FunClause a)

85data CtorArg = CtorParameter FunArg | CtorField FunArg

84data CtorArg = CtorParameter FunArg | CtorField FunArg

@@ -116,6 +115,7 @@ data Elab : Type -> Type where

116 Prim__Guess : Elab TT

115 Prim__Guess : Elab TT

117 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

116 Prim__LookupTy : TTName -> Elab (List (TTName, NameType, TT))

118 Prim__LookupDatatype : TTName -> Elab (List Datatype)

117 Prim__LookupDatatype : TTName -> Elab (List Datatype)

118+ Prim__LookupFunDefn : TTName -> Elab (List (FunDefn TT))

119 Prim__LookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

120

121 Prim__Check : List (TTName, Binder TT) -> Raw -> Elab (TT, TT)

@@ -148,7 +148,7 @@ data Elab : Type -> Type where

148 Prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()

149

150 Prim__DeclareType : TyDecl -> Elab ()

151− Prim__DefineFunction : FunDefn -> Elab ()

151+ Prim__DefineFunction : FunDefn Raw -> Elab ()

152 Prim__AddInstance : TTName -> TTName -> Elab ()

153 Prim__IsTCName : TTName -> Elab Bool

154

@@ -231,6 +231,19 @@ namespace Tactics

231 [] => fail [TextPart "No datatype named", NamePart n]

232 xs => fail [TextPart "More than one datatype named", NamePart n]

233

234+ ||| Find the reflected function definition of all functions whose names

235+ ||| are overloadings of some name.

236+ lookupFunDefn : TTName -> Elab (List (FunDefn TT))

237+ lookupFunDefn n = Prim__LookupFunDefn n

238+

239+ ||| Find the reflected function definition of a function, given its

240+ ||| fully-qualified name. Fail if the name does not uniquely resolve

241+ ||| to a function.

242+ lookupFunDefnExact : TTName -> Elab (FunDefn TT)

243+ lookupFunDefnExact n = case !(lookupFunDefn n) of

244+ [res] => return res

245+ [] => fail [TextPart "No function named", NamePart n]

246+ xs => fail [TextPart "More than one function named", NamePart n]

234

247

235 ||| Get the argument specification for each overloading of a name.

248 ||| Get the argument specification for each overloading of a name.

236 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

249 lookupArgs : TTName -> Elab (List (TTName, List FunArg, Raw))

@@ -452,7 +465,7 @@ namespace Tactics

452 ||| Define a function in the global context. The function must have

465 ||| Define a function in the global context. The function must have

453 ||| already been declared, either in ordinary Idris code or using

466 ||| already been declared, either in ordinary Idris code or using

454 ||| `declareType`.

467 ||| `declareType`.

455− defineFunction : FunDefn -> Elab ()

468+ defineFunction : FunDefn Raw -> Elab ()

456 defineFunction defun = Prim__DefineFunction defun

469 defineFunction defun = Prim__DefineFunction defun

457

470

458 ||| Register a new instance for type class resolution.

471 ||| Register a new instance for type class resolution.

libs/pruviloj/Pruviloj/Derive/DecEq.idr+1−1

@@ -181,7 +181,7 @@ deriveDecEq fn =

181 Nothing => return False

182

183 partial -- mkRhs

184− mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)

184+ mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe (FunClause Raw))

185 mkCase k fam (cn1, args1, _) (cn2, args2, _) =

186 perhaps $ elabPatternClause

187 (do (h2 :: h1 :: _) <- reverse <$>

libs/pruviloj/Pruviloj/Derive/Eliminators.idr+3−3

@@ -134,7 +134,7 @@ instance Show ElimArg where

134 show (NormalArgument x) = "NormalArgument " ++ show x

135

136getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->

137− (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause

137+ (TTName, List CtorArg, Raw) -> Nat -> Elab (FunClause Raw)

138getElimClause info elimn methCount (cn, args, resTy) whichCon =

139 elabPatternClause

140 (do -- Establish a hole for each parameter

@@ -242,13 +242,13 @@ getElimClause info elimn methCount (cn, args, resTy) whichCon =

242 bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x

243

244getElimClauses : TyConInfo -> (elimn : TTName) ->

245− List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

245+ List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

246getElimClauses info elimn ctors =

247 let methodCount = length ctors

248 in traverse (\(i, con) => getElimClause info elimn methodCount con i)

249 (enumerate ctors)

250

251−instance Show FunClause where

251+instance (Show a) => Show (FunClause a) where

252 show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"

253

254abstract

libs/pruviloj/Pruviloj/Internals.idr+1−1

@@ -101,7 +101,7 @@ bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res

101||| It will be run in a context where the pattern variables are

102||| already bound, and should leave behind no holes.

103partial

104−elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause

104+elabPatternClause : (lhs, rhs : Elab ()) -> Elab (FunClause Raw)

105elabPatternClause lhs rhs =

106 do -- Elaborate the LHS in a context where its type will be solved via unification

107 (pat, _) <- runElab `(Infer) $

src/Idris/Elab/Term.hs+6−1

@@ -1782,7 +1782,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1782 pullVars :: (Term, Term) -> ([Name], Term, Term)

1783 pullVars (lhs, rhs) = (fst (patvars [] lhs), snd (patvars [] lhs), snd (patvars [] rhs)) -- TODO alpha-convert rhs

1784

1785− defineFunction :: RFunDefn -> ElabD ()

1785+ defineFunction :: RFunDefn Raw -> ElabD ()

1786 defineFunction (RDefineFun n clauses) =

1787 do ctxt <- get_context

1788 ty <- maybe (fail "no type decl") return $ lookupTyExact n ctxt

@@ -1874,6 +1874,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1874 fmap fst . checkClosed $

1875 rawList (Var (tacN "Datatype"))

1876 (map reflectDatatype (buildDatatypes ist n'))

1877+ | n == tacN "Prim__LookupFunDefn", [name] <- args

1878+ = do n' <- reifyTTName name

1879+ fmap fst . checkClosed $

1880+ rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))

1881+ (map reflectFunDefn (buildFunDefns ist n'))

1877 | n == tacN "Prim__LookupArgs", [name] <- args

1882 | n == tacN "Prim__LookupArgs", [name] <- args

1878 = do n' <- reifyTTName name

1883 = do n' <- reifyTTName name

1879 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

1884 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])

src/Idris/Reflection.hs+41−13

@@ -7,6 +7,8 @@ module Idris.Reflection where

8#if __GLASGOW_HASKELL__ < 710

9import Control.Applicative ((<$>), (<*>), pure)

10+import Prelude hiding (mapM)

11+import Data.Traversable (mapM)

10#endif

12#endif

11import Control.Monad (liftM, liftM2, liftM4)

13import Control.Monad (liftM, liftM2, liftM4)

12import Control.Monad.State.Strict (lift)

14import Control.Monad.State.Strict (lift)

@@ -19,7 +21,7 @@ import Idris.Core.Elaborate (claim, fill, focus, getNameFrom, initElaborator,

19import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

21import Idris.Core.Evaluate (Def(TyDecl), initContext, lookupDefExact, lookupTyExact)

20import Idris.Core.TT

22import Idris.Core.TT

22−import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes),

24+import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,idris_datatypes, idris_patdefs),

23 PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

25 PArg'(..), PArg, PTactic, PTactic'(..), PTerm(..), Fixity (..),

24 initEState, pairCon, pairTy)

26 initEState, pairCon, pairTy)

25import Idris.Delaborate (delab)

27import Idris.Delaborate (delab)

@@ -55,11 +57,11 @@ rFunArgToPArg (RFunArg n _ RExplicit e) = PExp 0 (rArgOpts e) n Placeholder

55rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder

57rFunArgToPArg (RFunArg n _ RImplicit e) = PImp 0 False (rArgOpts e) n Placeholder

56rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder

58rFunArgToPArg (RFunArg n _ RConstraint e) = PConstraint 0 (rArgOpts e) n Placeholder

58−data RFunClause = RMkFunClause Raw Raw

60+data RFunClause a = RMkFunClause a a

59− | RMkImpossibleClause Raw

61+ | RMkImpossibleClause a

60− deriving Show

62+ deriving Show

62−data RFunDefn = RDefineFun Name [RFunClause] deriving Show

64+data RFunDefn a = RDefineFun Name [RFunClause a] deriving Show

64-- | Prefix a name with the "Language.Reflection" namespace

66-- | Prefix a name with the "Language.Reflection" namespace

65reflm :: String -> Name

67reflm :: String -> Name

@@ -1023,21 +1025,21 @@ reifyTyDecl (App _ (App _ (App _ (P (DCon _ _ _) n _) tyN) args) ret)

1023 return $ RDeclare tyN' args' ret'

1025 return $ RDeclare tyN' args' ret'

1024reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

1026reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

1025

1027

1026−reifyFunDefn :: Term -> ElabD RFunDefn

1028+reifyFunDefn :: Term -> ElabD (RFunDefn Raw)

1027−reifyFunDefn (App _ (App _ (P _ n _) fnN) clauses)

1029+reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)

1028− | n == tacN "DefineFun" =

1030+ | n == tacN "DefineFun" && t == reflm "Raw" =

1029 do fnN' <- reifyTTName fnN

1031 do fnN' <- reifyTTName fnN

1030 clauses' <- case unList clauses of

1032 clauses' <- case unList clauses of

1031 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"

1033 Nothing -> fail $ "Couldn't reify " ++ show clauses ++ " as a clause list"

1032 Just cs -> mapM reifyC cs

1034 Just cs -> mapM reifyC cs

1033 return $ RDefineFun fnN' clauses'

1035 return $ RDefineFun fnN' clauses'

1034− where reifyC :: Term -> ElabD RFunClause

1036+ where reifyC :: Term -> ElabD (RFunClause Raw)

1035− reifyC (App _ (App _ (P (DCon _ _ _) n _) lhs) rhs)

1037+ reifyC (App _ (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs) rhs)

1036− | n == tacN "MkFunClause" = liftM2 RMkFunClause

1038+ | n == tacN "MkFunClause" && t == reflm "Raw" = liftM2 RMkFunClause

1037 (reifyRaw lhs)

1039 (reifyRaw lhs)

1038 (reifyRaw rhs)

1040 (reifyRaw rhs)

1039− reifyC (App _ (P (DCon _ _ _) n _) lhs)

1041+ reifyC (App _ (App _ (P (DCon _ _ _) n _) (P _ t _)) lhs)

1040− | n == tacN "MkImpossibleClause" = fmap RMkImpossibleClause $ reifyRaw lhs

1042+ | n == tacN "MkImpossibleClause" && t == reflm "Raw" = fmap RMkImpossibleClause $ reifyRaw lhs

1041 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

1043 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

1042reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

1044reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

1043

1045

@@ -1074,6 +1076,22 @@ unApplyRaw tm = ua [] tm

1074 ua args (RApp f a) = ua (a:args) f

1076 ua args (RApp f a) = ua (a:args) f

1075 ua args t = (t, args)

1077 ua args t = (t, args)

1076

1078

1079+-- | Build the reflected function definition(s) that correspond(s) to

1080+-- a provided unqualifed name

1081+buildFunDefns :: IState -> Name -> [RFunDefn Term]

1082+buildFunDefns ist n =

1083+ [ mkFunDefn name clauses

1084+ | (name, (clauses, _)) <- lookupCtxtName n $ idris_patdefs ist

1085+ ]

1086+

1087+ where mkFunDefn name clauses = RDefineFun name (map mkFunClause clauses)

1088+

1089+ mkFunClause ([], lhs, Impossible) = RMkImpossibleClause lhs

1090+ mkFunClause ([], lhs, rhs) = RMkFunClause lhs rhs

1091+ mkFunClause ((n : ns), lhs, rhs) = mkFunClause (ns, bind lhs, bind rhs) where

1092+ bind Impossible = Impossible

1093+ bind tm = Bind n (PVar Erased) tm

1094+

1077-- | Build the reflected datatype definition(s) that correspond(s) to

1095-- | Build the reflected datatype definition(s) that correspond(s) to

1078-- a provided unqualified name

1096-- a provided unqualified name

1079buildDatatypes :: IState -> Name -> [RDatatype]

1097buildDatatypes :: IState -> Name -> [RDatatype]

@@ -1163,3 +1181,13 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

1163 RApp (Var $ tacN "TyConParameter") (reflectArg a)

1181 RApp (Var $ tacN "TyConParameter") (reflectArg a)

1164 reflectConArg (RIndex a) =

1182 reflectConArg (RIndex a) =

1165 RApp (Var $ tacN "TyConIndex") (reflectArg a)

1183 RApp (Var $ tacN "TyConIndex") (reflectArg a)

1184+

1185+reflectFunClause :: RFunClause Term -> Raw

1186+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]

1187+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]

1188+

1189+reflectFunDefn :: RFunDefn Term -> Raw

1190+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"

1191+ , reflectName name

1192+ , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)

1193+ ]

test/meta001/Finite.idr+13−13

@@ -29,7 +29,7 @@ mkFin (S k) (S j) = do i <- mkFin k j

30mkToClause : TTName -> (size, i : Nat) ->

31 (constr : (TTName, List CtorArg, Raw)) ->

32− Elab FunClause

32+ Elab (FunClause Raw)

33mkToClause fn size i (n, [], Var ty) =

34 MkFunClause (RApp (Var fn) (Var n)) <$> mkFin size i

35mkToClause fn size i (n, _, ty) =

@@ -38,14 +38,14 @@ mkToClause fn size i (n, _, ty) =

39mkFromClause : TTName -> (size, i : Nat) ->

40 (constr : (TTName, List CtorArg, Raw)) ->

41− Elab FunClause

41+ Elab (FunClause Raw)

42mkFromClause fn size i (n, [], Var ty) =

43 return $ MkFunClause (RApp (Var fn) !(mkFin size i)) (Var n)

44mkFromClause fn size i (n, _, ty) =

45 fail [TextPart "unsupported constructor", NamePart n]

48−mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause

48+mkOk1Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

49mkOk1Clause fn size i (n, [], Var ty) =

50 return $ MkFunClause (RApp (Var fn) (Var n))

51 [| (Var (UN "Refl")) (Var ty) (Var n) |]

@@ -53,7 +53,7 @@ mkOk1Clause fn size i (n, _, ty) =

53 fail [TextPart "unsupported constructor", NamePart n]

56−mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab FunClause

56+mkOk2Clause : TTName -> (size, i : Nat) -> (constr : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)

57mkOk2Clause fn size i (n, [], Var ty) =

58 return $ MkFunClause (RApp (Var fn) !(mkFin size i))

59 [| (Var "Refl") `(Fin ~(quote size))

@@ -62,9 +62,9 @@ mkOk2Clause fn size i (n, _, ty) =

62 fail [TextPart "unsupported constructor", NamePart n]

65−mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

65+mkToClauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

66mkToClauses fn size xs = mkToClauses' Z xs

67− where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

67+ where mkToClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

68 mkToClauses' k [] = return []

69 mkToClauses' k (x :: xs) = do rest <- mkToClauses' (S k) xs

70 clause <- mkToClause fn size k x

@@ -76,7 +76,7 @@ mkToClauses fn size xs = mkToClauses' Z xs

76||| This is to satisfy the totality checker, because `impossible`

77||| clauses are still

78mkAbsurdFinClause : (fn : TTName) -> (goal : Raw -> Raw) -> (size : Nat) ->

79− Elab FunClause

79+ Elab (FunClause Raw)

80mkAbsurdFinClause fn goal size =

81 do pv <- gensym "badfin"

82 lhsArg <- lhsBody pv size

@@ -92,26 +92,26 @@ mkAbsurdFinClause fn goal size =

94mkFromClauses : TTName -> TTName -> Nat ->

95− List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

95+ List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

96mkFromClauses fn ty size xs = mkFromClauses' Z xs

97− where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

97+ where mkFromClauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

98 mkFromClauses' k [] =

99 return [!(mkAbsurdFinClause fn (const (Var ty)) size)]

100 mkFromClauses' k (x :: xs) = do rest <- mkFromClauses' (S k) xs

101 clause <- mkFromClause fn size k x

102 return $ clause :: rest

103

104−mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

104+mkOk1Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

105mkOk1Clauses fn size xs = mkOk1Clauses' Z xs

106− where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

106+ where mkOk1Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

107 mkOk1Clauses' k [] = return []

108 mkOk1Clauses' k (x :: xs) = do rest <- mkOk1Clauses' (S k) xs

109 clause <- mkOk1Clause fn size k x

110 return $ clause :: rest

111

112−mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List FunClause)

112+mkOk2Clauses : TTName -> Nat -> List (TTName, List CtorArg, Raw) -> (Raw -> Raw) -> Elab (List (FunClause Raw))

113mkOk2Clauses fn size xs resTy = mkOk2Clauses' Z xs

114− where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List FunClause)

114+ where mkOk2Clauses' : Nat -> List (TTName, List CtorArg, Raw) -> Elab (List (FunClause Raw))

115 mkOk2Clauses' k [] = return [!(mkAbsurdFinClause fn resTy size)]

116 mkOk2Clauses' k (x :: xs) = do rest <- mkOk2Clauses' (S k) xs

117 clause <- mkOk2Clause fn size k x

test/meta004/expectednew file

No changes to the content.

test/meta004/meta004.idrnew file+26

@@ -0,0 +1,26 @@

1+import Language.Reflection.Utils

2+import Pruviloj.Core

4+forgotToNatAndRename : TTName -> TTName -> Raw -> Raw

5+forgotToNatAndRename old new (RBind name b body) = RBind name (map (forgotToNatAndRename old new) b) (forgotToNatAndRename old new body)

6+forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename old new arg)

7+forgotToNatAndRename old new (RConstant Forgot) = Var `{Nat}

8+forgotToNatAndRename old new (Var n) = if n == old then Var new else Var n

9+forgotToNatAndRename old new tm = tm

10+

11+roundtrip : TTName -> TTName -> Elab ()

12+roundtrip old new = do

13+ DefineFun _ clauses <- lookupFunDefnExact old

14+ clauses' <- for clauses (\(MkFunClause lhs rhs) => do

15+ lhs' <- forgotToNatAndRename old new <$> forget lhs

16+ rhs' <- forgotToNatAndRename old new <$> forget rhs

17+ pure $ MkFunClause lhs' rhs')

18+ defineFunction (DefineFun new clauses')

19+

20+plus' : Nat -> Nat -> Nat

21+%runElab (roundtrip `{plus} `{plus'})

22+

23+total

24+p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b

25+p Z right = Refl

26+p (S left) right = Refl

test/meta004/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ -p pruviloj --nocolour --check --consolewidth 70 meta004.idr

3+rm -f *.ibc