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