git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/test/basic010/Main.idr
43 lines 1.3 kB history raw
1module Main
3%default total
5-- An expensive function.
6qib : Nat -> Nat
7qib Z = 1
8qib (S Z) = 2
9qib (S (S n)) = qib n * qib (S n)
11-- An equality whose size reflects the size of numbers.
12data equals : Nat -> Nat -> Type where
13 eqZ : Z `equals` Z
14 eqS : m `equals` n -> S m `equals` S n
16eq_refl : {n : Nat} -> n `equals` n
17eq_refl {n = Z} = eqZ
18eq_refl {n = S n} = eqS eq_refl
20-- Here, the proof is very expensive to compute.
21-- We add a recursive argument to prevent Idris from inlining the function.
22f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)
23f Z n = Element n eq_refl
24f (S r) n = f r n
26-- A (contrived) relation, just to have something to show.
27data represents : Nat -> Nat -> Type where
28 axiom : (n : Nat) -> qib n `represents` n
30-- Here, the witness is very expensive to compute.
31-- We add a recursive argument to prevent Idris from inlining the function.
32g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)
33g Z n = Evidence (qib n) (axiom n)
34g (S r) n = g r n
36fmt : qib n `represents` n -> String
37fmt (axiom n) = "axiom " ++ show n
39main : IO ()
40main = do
41 n <- map (const (the Nat 10000)) (putStrLn "*oink*")
42 putStrLn . show $ getWitness (f 4 n)
43 putStrLn . fmt $ getProof (g 4 n)