blob: b8eec998a958207acc23c505c56eb93520f0f4ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
module Encoded.Bool
import Term.Semantics
import Term.Syntax
-- Type ------------------------------------------------------------------------
export
B : Ty
B = N
-- Universal Properties --------------------------------------------------------
export
True : Term B ctx
True = Lit 0
export
False : Term B ctx
False = Lit 1
export
if' : Term (B ~> ty ~> ty ~> ty) ctx
if' = Abs' (\b =>
Rec b
(Abs $ Const $ Var Here)
(Const $ Const $ Abs $ Var Here))
-- Utilities -------------------------------------------------------------------
export
and : Term (B ~> B ~> B) ctx
and = Abs' (\b => App if' [<b, Id, Const False])
export
or : Term (B ~> B ~> B) ctx
or = Abs' (\b => App if' [<b, Const True, Id])
export
not : Term (B ~> B) ctx
not = Abs' (\b => App if' [<b, False, True])
export
isZero : Term (N ~> B) ctx
isZero = Id
-- Semantics -------------------------------------------------------------------
-- Conversion to Idris
export
toBool : TypeOf B -> Bool
toBool = (== 0)
export
fromBool : Bool -> TypeOf B
fromBool b = if b then 0 else 1
export
toFromId : (b : Bool) -> toBool (fromBool b) = b
toFromId False = Refl
toFromId True = Refl
-- Redefinition in Idris
namespace Sem
public export
True : TypeOf B
True = 0
public export
False : TypeOf B
False = 1
public export
if' : TypeOf B -> a -> a -> a
if' b = rec b (\t, _ => t) (\_, _, f => f)
-- Homomorphism
export
trueHomo : toBool True = True
trueHomo = Refl
export
falseHomo : toBool False = False
falseHomo = Refl
export
ifHomo : (b : Bool) -> (0 x, y : a) -> if' (fromBool b) x y = if b then x else y
ifHomo True x y = Refl
ifHomo False x y = Refl
|
