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 (*GENERAL BUG: name clashes when binders shadow each other in CIC*)
 122
 123 (*BUG: for OCaml: cofixpoint not distinguished from fixpoints*)
 124
 125 let rec rtest1 (n:nat) : nat ≝
 126  match n with
 127  [ O ⇒ O
 128  | S m ⇒ rtest1 m ].
 129
 130 let rec f (n:nat) : nat ≝
 131  match n with
 132  [ O ⇒ O
 133  | S m ⇒ g m ]
 134 and g (n:nat) : nat ≝
 135  match n with
 136  [ O ⇒ O
 137  | S m ⇒ f m ].
 138
 139 (*BUG: pattern matching patterns when arguments have been deleted from
 140   the constructor are wrong *)
 141
 142 coinductive stream: Type[0] ≝ scons : nat → stream → stream.
 143
 144 let corec div (n:nat) : stream ≝ scons n (div (S n)).
 145
 146 axiom plus: nat → nat → nat.
 147
 148 definition rtest2 : nat → stream → nat ≝
 149  λm,s. match s with [ scons n l ⇒ plus m n ].
 150
 151 (*
 152 let rec mkterm (n:nat) : nat ≝
 153  match n with
 154  [ O ⇒ O
 155  | S m ⇒ mkterm m ]
 156 and mktyp (n:nat) : Type[0] ≝
 157  match n with
 158  [ O ⇒ nat
 159  | S m ⇒ mktyp m ].*)
 160
 161 inductive meee: Type[0] → Type[0] ≝ .
 162
 163 inductive T1 : (Type[0] → Type[0]) → ∀B:Type[0]. nat → Type[0] → Type[0] ≝ .
 164
 165 inductive T2 : (Type[0] → Type[0]) → ∀B:Type[0]. B → Type[0] → Type[0] ≝ .
 166
 167 (* no content *)
 168 inductive T3 : (Type[0] → Type[0]) → CProp[2] ≝ .
 169
 170 definition erase ≝ λX:Type[0].Type[0].
 171
 172 axiom lt: nat → nat → Prop.
 173
 174 inductive myvect (A: Type[0]) (b:nat) : nat → Type[0] ≝
 175    myemptyv : myvect A b O
 176  | mycons: ∀n. lt n b → A → myvect A b n → myvect A b (S n).
 177
 178 inductive False: Prop ≝ .
 179
 180 inductive Empty: Type[0] ≝ .
 181
 182 inductive bool: Type[0] ≝ true: bool | false:bool.
 183
 184 inductive eq (A:Type[1]) (a:A) : A → Prop ≝ refl: eq A a a.
 185
 186 (* requires coercion *)
 187 definition cast_bug1 ≝
 188  λH:eq Type[0] bool nat. S (match H return λA:Type[0].λ_.A with [ refl ⇒ true ]).
 189
 190 (* requires coercion in all branches *)
 191 definition cast_bug2 ≝
 192  λb.
 193   match true return λb.match b with [ true ⇒ nat → nat | false ⇒ bool ] with
 194    [ true ⇒ S | false ⇒ false ]
 195   O.
 196
 197 (*BUG: try singleton elimination with constructor arguments to show bug in
 198  DeBrujin indexes *)