]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/extraction.ma
- pointer structure simplified
[helm.git] / matita / matita / lib / extraction.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basics/pts.ma".
16
17 inductive nat : Type[0] ≝ O: nat | S: nat → nat.
18
19 axiom test1: Type[1].
20
21 axiom test2: Type[1] → Type[1].
22
23 axiom test3: Prop → Type[1] → CProp[1] → Type[1] → Type[2].
24
25 axiom test4: ∀A:Type[1]. A → ∀B:Type[1]. B → ∀C:Prop. C → Type[1].
26
27 axiom test4': ∀C:Prop. C → C.
28
29 axiom test4'': ∀C:Prop. C → nat.
30
31 axiom test4''': ∀C:Type[1]. C.
32
33 axiom test4_5: (∀A:Type[0].A) → nat.
34
35 axiom test5: (Type[1] → Type[1]) → Type[1].
36
37 (* no content *)
38 axiom test6: Type[1] → Prop.
39
40 definition dtest1: Type[1] ≝ nat → nat.
41
42 definition dtest2: Type[2] ≝ ∀A:Type[1]. A → A.
43
44 definition dtest3: Type[1] → Type[1] ≝ λA:Type[1]. A → A.
45
46 definition dtest4: Type[1] → Type[1] ≝ λA:Type[1].dtest3 A.
47
48 definition dtest5: Type[1] → Type[1] ≝ dtest3.
49
50 definition dtest6: Type[1] ≝ dtest3 nat.
51
52 inductive True : Prop ≝ I: True.
53
54 (* no content *)
55 definition dtest7: Prop ≝ True → True.
56
57 (* no content *)
58 definition dtest8: Type[1] ≝ dtest3 True.
59
60 (* no content *)
61 definition dtest9: Type[1] ≝ dtest3 Prop.
62
63 definition dtest10: Type[1] → Type[1] → Type[1] ≝ λX,Y.X.
64
65 definition dtest11: Type[1] → nat → Type[1] → Type[1] ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
66
67
68 definition dtest12 ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
69
70 definition dtest13 ≝ dtest3 nat → dtest3 True → dtest3 Prop → nat.
71
72 definition dtest14 ≝ λX:Type[2]. X → X.
73
74 definition dtest15 ≝ ∀T:Type[1] → Type[1]. T nat → T nat.
75
76 definition dtest16 ≝ ∀T:Type[1]. T → nat.
77
78 definition dtest17 ≝ ∀T:dtest14 Type[1]. T nat → dtest14 nat → dtest14 nat.
79
80 definition dtest18 ≝ λA,B:Type[0].λn:nat.λC:Type[0].A.
81
82 definition dtest19 ≝ dtest18 nat True O nat → dtest18 nat nat O nat.
83
84 definition dtest20 ≝ test5 test2.
85
86 (*BUG: lambda-lift the inner declaration;
87   to be traced, raises NotInFOmega; why?
88 definition dtest21 ≝ test5 (λX:Type[1].X).*)
89
90 definition ttest1 ≝ λx:nat.x.
91
92 (*BUG: clash of name due to capitalisation*)
93 (*definition Ttest1 ≝ λx:nat.x.*)
94
95 (*FEATURE: print binders in the l.h.s. without using lambda abstraction*)
96 definition ttest2 ≝ λT:Type[1].λx:T.x.
97
98 definition ttest3 ≝ λT:Type[1].λx:T.let y ≝ x in y.
99
100 definition ttest4 ≝ λT:Type[1].let y ≝ T in λx:y.x.
101
102 (*BUG IN HASKELL PRETTY PRINTING: all lets are let rec*)
103 (*definition ttest5 ≝ λT:Type[1].λy:T.let y ≝ y in y.*)
104
105 definition ttest6 ≝ ttest4 nat.
106
107 definition ttest7 ≝ λf:∀X:Type[1].X. f (nat → nat) O.
108
109 definition ttest8 ≝ λf:∀X:Type[1].X. f (True → True) I.
110
111 definition ttest9 ≝ λf:∀X:Type[1].X. f (True → nat) I.
112
113 definition ttest10 ≝ λf:∀X:Type[1].X. f (True → nat → nat) I O.
114
115 definition ttest11_aux ≝ λS:Type[1]. S → nat.
116
117 definition ttest11 ≝ λf:ttest11_aux True. f I.
118
119 definition ttest12 ≝ λf:True → nat. f I.
120
121 (*BUG: assertion failure here! difficult case for head application
122 axiom ttest13_a: ∀T:Type[1]. T → nat.
123 definition ttest13_b ≝ ttest13_a nat O.
124 definition ttest13_c ≝ ttest13_a Prop True.*)
125
126 (*GENERAL BUG: name clashes when binders shadow each other in CIC*)
127
128 (*BUG: for OCaml: cofixpoint not distinguished from fixpoints*)
129
130 let rec rtest1 (n:nat) : nat ≝
131  match n with
132  [ O ⇒ O
133  | S m ⇒ rtest1 m ].
134
135 let rec f (n:nat) : nat ≝
136  match n with
137  [ O ⇒ O
138  | S m ⇒ g m ]
139 and g (n:nat) : nat ≝
140  match n with
141  [ O ⇒ O
142  | S m ⇒ f m ].
143
144 (*BUG: pattern matching patterns when arguments have been deleted from
145   the constructor are wrong *)
146
147 coinductive stream: Type[0] ≝ scons : nat → stream → stream.
148
149 let corec div (n:nat) : stream ≝ scons n (div (S n)).
150
151 axiom plus: nat → nat → nat.
152
153 definition rtest2 : nat → stream → nat ≝
154  λm,s. match s with [ scons n l ⇒ plus m n ].
155
156 (*
157 let rec mkterm (n:nat) : nat ≝
158  match n with
159  [ O ⇒ O
160  | S m ⇒ mkterm m ]
161 and mktyp (n:nat) : Type[0] ≝
162  match n with
163  [ O ⇒ nat
164  | S m ⇒ mktyp m ].*)
165
166 inductive meee: Type[0] → Type[0] ≝ .
167
168 inductive T1 : (Type[0] → Type[0]) → ∀B:Type[0]. nat → Type[0] → Type[0] ≝ .
169
170 inductive T2 : (Type[0] → Type[0]) → ∀B:Type[0]. B → Type[0] → Type[0] ≝ .
171
172 (* no content *)
173 inductive T3 : (Type[0] → Type[0]) → CProp[2] ≝ .
174
175 definition erase ≝ λX:Type[0].Type[0].
176
177 axiom lt: nat → nat → Prop.
178
179 inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
180    myemptyv : myvect A b O
181  | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
182  
183 inductive False: Prop ≝ .
184
185 inductive Empty: Type[0] ≝ .
186
187 inductive bool: Type[0] ≝ true: bool | false:bool.
188
189 inductive eq (A:Type[1]) (a:A) : A → Prop ≝ refl: eq A a a.
190
191 (* requires coercion *)
192 definition cast_bug1 ≝
193  λH:eq Type[0] bool nat. S (match H return λA:Type[0].λ_.A with [ refl ⇒ true ]).
194
195 (*
196 (*BUG: Here we use eq_rect_Type0 in its poly-kinded form, but we only extracted
197    the one-kinded form. Require coercions *)
198 definition cast_bug1' ≝
199  λH:eq Type[0] bool nat. S (eq_rect_Type0 Type[0] bool (λA:Type[0].λ_.A) true nat H).
200 *)
201
202 (* requires coercion in all branches *)
203 definition cast_bug2 ≝
204   match true return λb.match b with [ true ⇒ nat → nat | false ⇒ bool ] with
205    [ true ⇒ S | false ⇒ false ]
206   O.
207   
208 (*BUG: try singleton elimination with constructor arguments to show bug in
209  DeBrujin indexes *)