git.iko.soy/Idris-dev
on master help sign in
Tests on default args and substitution
commit9a25dfae7b547b6867581d07588ef69b37c02fb1 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateSun 6 Apr 2014, 01:22 (13 years ago) parentbfc3c3e
9 files changed+71
compare with master
unifiedsplit
test/proof005/DefaultArgSubstitutionSuccess.idr+27 test/proof005/expected test/proof005/run+3 test/proof006/DefaultArgSubstitutionSyntax.idr+30 test/proof006/expected test/proof006/run+3 test/proof007/DefaultArgUnknownName.idr+4 test/proof007/expected+1 test/proof007/run+3
test/proof005/DefaultArgSubstitutionSuccess.idrnew file+27
@@ -0,0 +1,27 @@
1+module DefaultArgSubstitutionSuccess
2+
3+DecProofType : {a:Type} -> Dec a -> Type
4+DecProofType {a} (Yes _) = a
5+DecProofType {a} (No _) = a -> _|_
6+
7+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
8+decProof (Yes x) = x
9+decProof (No x) = x
10+
11+DecType : {a:Type} -> Dec a -> Type
12+DecType {a} _ = a
13+
14+
15+argsAreSame : (n:Nat) -> (m:Nat)
16+ -> { default (decProof (decEq m n)) same : (m=n) } -> ()
17+argsAreSame _ _ = ()
18+
19+data SameNats : Type where
20+ same : (n:Nat) -> (m:Nat) ->
21+ { default (decProof (decEq m n)) same : (m=n) } -> SameNats
22+
23+zArgsAreSame : ()
24+zArgsAreSame = argsAreSame Z Z
25+
26+sameNatZs : SameNats
27+sameNatZs = same Z Z
test/proof005/expectednew file

No changes to the content.

test/proof005/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check $@ DefaultArgSubstitutionSuccess.idr
3+rm -f *.ibc
test/proof006/DefaultArgSubstitutionSyntax.idrnew file+30
@@ -0,0 +1,30 @@
1+module DefaultArgSubstitutionSyntax
2+
3+DecProofType : {a:Type} -> Dec a -> Type
4+DecProofType {a} (Yes _) = a
5+DecProofType {a} (No _) = a -> _|_
6+
7+decProof : {a:Type} -> (dec : Dec a) -> DecProofType dec
8+decProof (Yes x) = x
9+decProof (No x) = x
10+
11+DecType : {a:Type} -> Dec a -> Type
12+DecType {a} _ = a
13+
14+
15+syntax "{{" [prfname] ":" "accept" [dec] "}}" "->" [ret]
16+ = { default (decProof dec) prfname : DecType dec } -> ret
17+
18+
19+argsAreSame : (n:Nat) -> (m:Nat)
20+ -> {{ same : accept (decEq n m) }} -> ()
21+argsAreSame _ _ = ()
22+
23+data SameNats : Type where
24+ same : (n:Nat) -> (m:Nat) -> {{ same : accept (decEq m n) }} -> SameNats
25+
26+zArgsAreSame : ()
27+zArgsAreSame = argsAreSame Z Z
28+
29+sameNatZs : SameNats
30+sameNatZs = same Z Z
test/proof006/expectednew file

No changes to the content.

test/proof006/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check $@ DefaultArgSubstitutionSyntax.idr
3+rm -f *.ibc
test/proof007/DefaultArgUnknownName.idrnew file+4
@@ -0,0 +1,4 @@
1+module DefaultArgUnknownName
2+
3+funWithBadDefArg : { default sadgjhsag arg : () } -> ()
4+funWithBadDefArg : _ = ()
test/proof007/expectednew file+1
@@ -0,0 +1 @@
1+No such variable sadgjhsag
test/proof007/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris --check $@ DefaultArgUnknownName.idr
3+rm -f *.ibc