Add test for lookupFunDefn

idris.cabal

@@ -562,6 +562,9 @@ Extra-source-files:
                        test/meta002/run
                        test/meta002/*.idr
                        test/meta002/expected
+                       test/meta004/run
+                       test/meta004/*.idr
+                       test/meta004/expected
 
                        test/primitives001/run
                        test/primitives001/*.idr

test/meta004/meta004.idr

@@ -0,0 +1,26 @@
+import Language.Reflection.Utils
+import Pruviloj.Core
+
+forgotToNatAndRename : TTName -> TTName -> Raw -> Raw
+forgotToNatAndRename old new (RBind name b body) = RBind name (map (forgotToNatAndRename old new) b) (forgotToNatAndRename old new body)
+forgotToNatAndRename old new (RApp f arg) = RApp (forgotToNatAndRename old new f) (forgotToNatAndRename old new arg)
+forgotToNatAndRename old new (RConstant Forgot) = Var `{Nat}
+forgotToNatAndRename old new (Var n) = if n == old then Var new else Var n
+forgotToNatAndRename old new tm = tm
+
+roundtrip : TTName -> TTName -> Elab ()
+roundtrip old new = do
+  DefineFun _ clauses <- lookupFunDefnExact old
+  clauses' <- for clauses (\(MkFunClause lhs rhs) => do
+    lhs' <- forgotToNatAndRename old new <$> forget lhs
+    rhs' <- forgotToNatAndRename old new <$> forget rhs
+    pure $ MkFunClause lhs' rhs')
+  defineFunction (DefineFun new clauses')
+
+plus' : Nat -> Nat -> Nat
+%runElab (roundtrip `{plus} `{plus'})
+
+total
+p : (a : Nat) -> (b : Nat) -> plus a b = plus' a b
+p Z right = Refl
+p (S left) right = Refl

test/meta004/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ --nocolour --check --consolewidth 70 meta004.idr
+rm -f *.ibc