git.iko.soy/Idris-dev
on ff7ea9d 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)