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 (*FEATURE: kind signatures in type declarations*)
  18
  19 inductive nat : Type[0] ≝ O: nat | S: nat → nat.
  20
  21 axiom test1: Type[1].
  22
  23 axiom test2: Type[1] → Type[1].
  24
  25 axiom test3: Prop → Type[1] → CProp[1] → Type[1] → Type[2].
  26
  27 axiom test4: ∀A:Type[1]. A → ∀B:Type[1]. B → ∀C:Prop. C → Type[1].
  28
  29 axiom test4': ∀C:Prop. C → C.
  30
  31 axiom test4'': ∀C:Prop. C → nat.
  32
  33 axiom test4''': ∀C:Type[1]. C.
  34
  35 axiom test4_5: (∀A:Type[0].A) → nat.
  36
  37 axiom test5: (Type[1] → Type[1]) → Type[1].
  38
  39 (* no content *)
  40 axiom test6: Type[1] → Prop.
  41
  42 definition dtest1: Type[1] ≝ nat → nat.
  43
  44 definition dtest2: Type[2] ≝ ∀A:Type[1]. A → A.
  45
  46 definition dtest3: Type[1] → Type[1] ≝ λA:Type[1]. A → A.
  47
  48 definition dtest4: Type[1] → Type[1] ≝ λA:Type[1].dtest3 A.
  49
  50 definition dtest5: Type[1] → Type[1] ≝ dtest3.
  51
  52 definition dtest6: Type[1] ≝ dtest3 nat.
  53
  54 inductive True : Prop ≝ I: True.
  55
  56 (* no content *)
  57 definition dtest7: Prop ≝ True → True.
  58
  59 (* no content *)
  60 definition dtest8: Type[1] ≝ dtest3 True.
  61
  62 (* no content *)
  63 definition dtest9: Type[1] ≝ dtest3 Prop.
  64
  65 definition dtest10: Type[1] → Type[1] → Type[1] ≝ λX,Y.X.
  66
  67 definition dtest11: Type[1] → nat → Type[1] → Type[1] ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
  68
  69
  70 definition dtest12 ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1.
  71
  72 definition dtest13 ≝ dtest3 nat → dtest3 True → dtest3 Prop → nat.
  73
  74 definition dtest14 ≝ λX:Type[2]. X → X.
  75
  76 (*FEATURE: type the forall bound variables*)
  77 definition dtest15 ≝ ∀T:Type[1] → Type[1]. T nat → T nat.
  78
  79 definition dtest16 ≝ ∀T:Type[1]. T → nat.
  80
  81 definition dtest17 ≝ ∀T:dtest14 Type[1]. T nat → dtest14 nat → dtest14 nat.
  82
  83 definition dtest18 ≝ λA,B:Type[0].λn:nat.λC:Type[0].A.
  84
  85 definition dtest19 ≝ dtest18 nat True O nat → dtest18 nat nat O nat.
  86
  87 definition dtest20 ≝ test5 test2.
  88
  89 (*BUG: lambda-lift the inner declaration;
  90   to be traced, raises NotInFOmega; why?
  91 definition dtest21 ≝ test5 (λX:Type[1].X).*)
  92
  93 definition ttest1 ≝ λx:nat.x.
  94
  95 (*BUG: clash of name due to capitalisation*)
  96 (*definition Ttest1 ≝ λx:nat.x.*)
  97
  98 (*FEATURE: print binders in the l.h.s. without using lambda abstraction*)
  99 definition ttest2 ≝ λT:Type[1].λx:T.x.
 100
 101 definition ttest3 ≝ λT:Type[1].λx:T.let y ≝ x in y.
 102
 103 definition ttest4 ≝ λT:Type[1].let y ≝ T in λx:y.x.
 104
 105 (*BUG IN HASKELL PRETTY PRINTING: all lets are let rec*)
 106 (*definition ttest5 ≝ λT:Type[1].λy:T.let y ≝ y in y.*)
 107
 108 definition ttest6 ≝ ttest4 nat.
 109
 110 definition ttest7 ≝ λf:∀X:Type[1].X. f (nat → nat) O.
 111
 112 definition ttest8 ≝ λf:∀X:Type[1].X. f (True → True) I.
 113
 114 definition ttest9 ≝ λf:∀X:Type[1].X. f (True → nat) I.
 115
 116 definition ttest10 ≝ λf:∀X:Type[1].X. f (True → nat → nat) I O.
 117
 118 definition ttest11_aux ≝ λS:Type[1]. S → nat.
 119
 120 definition ttest11 ≝ λf:ttest11_aux True. f I.
 121
 122 definition ttest12 ≝ λf:True → nat. f I.
 123
 124 (*GENERAL BUG: name clashes when binders shadow each other in CIC*)
 125
 126 (*BUG: mutual type definitions not handled correctly: the ref is computed in a
 127   wrong way *)
 128
 129 (*BUG: multiple let-reced things are given the same (wrong) name*)
 130
 131 (*BUG: for OCaml: cofixpoint not distinguished from fixpoints*)
 132
 133 let rec rtest1 (n:nat) : nat ≝
 134  match n with
 135  [ O ⇒ O
 136  | S m ⇒ rtest1 m ].
 137
 138 let rec f (n:nat) : nat ≝
 139  match n with
 140  [ O ⇒ O
 141  | S m ⇒ g m ]
 142 and g (n:nat) : nat ≝
 143  match n with
 144  [ O ⇒ O
 145  | S m ⇒ f m ].
 146
 147 (*BUG: pattern matching patterns when arguments have been deleted from
 148   the constructor are wrong *)
 149
 150 (*BUG: constructor names in pattern should be capitalised correctly;
 151   name clashes must be avoided*)
 152
 153 coinductive stream: Type[0] ≝ scons : nat → stream → stream.
 154
 155 let corec div (n:nat) : stream ≝ scons n (div (S n)).
 156
 157 axiom plus: nat → nat → nat.
 158
 159 definition rtest2 : nat → stream → nat ≝
 160  λm,s. match s with [ scons n l ⇒ plus m n ].
 161
 162 (*
 163 let rec mkterm (n:nat) : nat ≝
 164  match n with
 165  [ O ⇒ O
 166  | S m ⇒ mkterm m ]
 167 and mktyp (n:nat) : Type[0] ≝
 168  match n with
 169  [ O ⇒ nat
 170  | S m ⇒ mktyp m ].*)
 171
 172 inductive meee: Type[0] → Type[0] ≝ .
 173
 174 inductive T1 : (Type[0] → Type[0]) → ∀B:Type[0]. nat → Type[0] → Type[0] ≝ .
 175
 176 inductive T2 : (Type[0] → Type[0]) → ∀B:Type[0]. B → Type[0] → Type[0] ≝ .
 177
 178 (* no content *)
 179 (*BUG: eliminators extracted anyway???*)
 180 inductive T3 : (Type[0] → Type[0]) → CProp[2] ≝ .
 181
 182 definition erase ≝ λX:Type[0].Type[0].
 183
 184 axiom lt: nat → nat → Prop.
 185
 186 (*BUG: elimination principles not extracted *)
 187 inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
 188    myemptyv : myvect A b O
 189  | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
 190
 191 inductive False: Prop ≝ .
 192
 193 inductive Empty: Type[0] ≝ .
 194
 195 inductive bool: Type[0] ≝ true: bool | false:bool.
 196
 197 inductive eq (A:Type[1]) (a:A) : A → Prop ≝ refl: eq A a a.
 198
 199 (* BUG: requires coercion *)
 200 definition cast_bug1 ≝
 201  λH:eq Type[0] bool nat. S (match H return λA:Type[0].λ_.A with [ refl ⇒ true ]).
 202
 203 (* BUG: requires top type *)
 204 definition cast_bug2 ≝
 205  λb.
 206   match true return λb.match b with [ true ⇒ nat → nat | false ⇒ bool ] with
 207    [ true ⇒ S | false ⇒ false ]
 208   O.
 209
 210 (*BUG: try singleton elimination with constructor arguments to show bug in
 211  DeBrujin indexes *)