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 *)