3264b8f · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

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

562 test/meta002/run

563 test/meta002/*.idr

564 test/meta002/expected

565+ test/meta004/run

566+ test/meta004/*.idr

567+ test/meta004/expected

565

568

566 test/primitives001/run

569 test/primitives001/run

567 test/primitives001/*.idr

570 test/primitives001/*.idr

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

3+

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 $@ --nocolour --check --consolewidth 70 meta004.idr

3+rm -f *.ibc