@@ -4,7 +4,7 @@ module Main
5-- An expensive function.
5-- An expensive function.
6qib : Nat -> Nat
6qib : Nat -> Nat
8qib (S Z) = 2
8qib (S Z) = 2
9qib (S (S n)) = qib n * qib (S n)
9qib (S (S n)) = qib n * qib (S n)
@@ -18,21 +18,26 @@ eq_refl {n = Z} = eqZ
18eq_refl {n = S n} = eqS eq_refl
18eq_refl {n = S n} = eqS eq_refl
20-- Here, the proof is very expensive to compute.
20-- Here, the proof is very expensive to compute.
21−-- We add a recursive argument to prevent Idris from inlining it.
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)
22f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)
23f Z n = element n eq_refl
23f Z n = element n eq_refl
24f (S r) n = f r n
24f (S r) n = f r n
26+-- A (contrived) relation, just to have something to show.
27+data represents : Nat -> Nat -> Type where
28+ axiom : (n : Nat) -> qib n `represents` n
26-- Here, the witness is very expensive to compute.
30-- Here, the witness is very expensive to compute.
27−-- We add a recursive argument to prevent Idris from inlining it.
31+-- We add a recursive argument to prevent Idris from inlining the function.
28−g : (r, n : Nat) -> Exists (\k : Nat => k = qib n)
32+g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)
29−g Z n = evidence (qib n) refl
33+g Z n = evidence (qib n) (axiom n)
30g (S r) n = g r n
34g (S r) n = g r n
32−nod : a -> IO ()
36+fmt : qib n `represents` n -> String
33−nod _ = putStrLn "*nod*"
37+fmt (axiom n) = "axiom " ++ show n
35main : IO ()
39main : IO ()
41+ n <- map (const 10000) (putStrLn "*oink*")
37− nod $ getWitness (f 4 2)
42+ putStrLn . show $ getWitness (f 4 n)
38− nod $ getProof (g 4 2)
43+ putStrLn . fmt $ getProof (g 4 n)