NaturalDeductionContext: more permutation proofs
[coq-hetmet.git] / examples / Demo.hs
1 {-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-}
2 module Demo (demo) where
3
4 {-
5 demo const mult =
6   <[ \y ->
7      ~~mult
8        (~~mult y y)
9        (~~mult y y)
10    ]>
11 -}
12
13
14
15
16
17
18 {-
19 demo const mult =
20   <[ \y ->
21      ~~mult
22        (~~mult (~~mult y y) (~~mult y y))
23        (~~mult (~~mult y y) (~~mult y y))
24    ]>
25 -}
26
27
28
29 {-
30 demo const mult =
31     <[ \y -> ~~(foo 4) ]>
32         where
33           foo 0 = const (12::Int)
34           foo n = <[ let bar = ~~(foo (n-1))
35                      in ~~mult bar bar
36                    ]>
37
38 -}
39
40
41
42 {-
43 demo const mult =
44     <[ \y -> ~~(foo 3) ]>
45         where
46           foo 0 = const (12::Int)
47           foo n = <[ let recurs = ~~(foo (n-1))
48                      in  ~~mult recurs recurs
49                    ]>
50
51 -}
52
53
54
55
56
57 demo const mult =
58  <[ \y ->
59     let   foo  = ~~mult (~~mult foo (~~mult y foo)) y
60     in    foo ]>
61
62
63
64
65
66
67
68
69
70
71
72
73 {-
74 demo const mult =
75     <[ \y -> ~~(foo 2 <[y]>) ]>
76         where
77           foo 0 y = const (12::Int)
78           foo n y = <[ let recurs = ~~(foo (n-1) y)
79                        in  ~~mult recurs recurs
80                      ]>
81 -}
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123 -- demo const mult = <[ \(y::Int) -> ~~mult y ~~(const 12) ]>
124 -- demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) ]>
125 -- golden
126 {-
127 demo const mult =
128  <[ \y ->
129     let   twelve  = ~~mult twelve y
130     in    twelve ]>
131 -}
132
133 {-
134 demo const mult =
135    <[ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) ]>
136 -}
137
138 {-
139 demo const mult =
140    <[ \(y::Int) ->
141       let four   = ~~mult four ~~(const  4)
142 --          twelve = {- {- ~~mult four -}  ~~(const 12) -} four
143       in  four
144     ]>
145 -}
146 demo ::
147     forall c . 
148          (Int -> <[Int]>@c) -> 
149         <[Int -> Int -> Int]>@c ->
150         <[Int -> Int]>@c
151
152 {-
153 demo const mult =
154  <[ let     twelve = ~~(const (12::Int))
155     in let  four    = ~~(const (4::Int))
156          in  ~~mult four twelve  ]>
157 -}
158
159 {-
160 demo const mult = demo' 3
161  where
162   demo' 0 = const 12
163   demo' 1 = const 12
164   demo' n = <[ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) ]>
165 -}
166
167 -- BUG
168 --demo const mult = <[ \y -> ~~(demo' 0) ]>
169 --  where
170 --   demo' 0 = const 4
171 --   demo' n = const 4