From 4b076eaf2b73fae27f1ae58d3dfc95a385909f8b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 2 Aug 2012 15:42:20 +0000 Subject: [PATCH] Temporary stuff to test code extraction. Running make produces extraction.hs which is checked by "ghci extraction.hs" --- matita/matita/lib/Makefile | 8 ++++ matita/matita/lib/extraction.ma | 70 +++++++++++++++++++++++++-------- matita/matita/lib/preamble.hs | 5 +++ 3 files changed, 67 insertions(+), 16 deletions(-) create mode 100644 matita/matita/lib/Makefile create mode 100644 matita/matita/lib/preamble.hs diff --git a/matita/matita/lib/Makefile b/matita/matita/lib/Makefile new file mode 100644 index 000000000..f463d32e9 --- /dev/null +++ b/matita/matita/lib/Makefile @@ -0,0 +1,8 @@ +all: + touch extraction.ma + EXTRACT_HASKELL=1 ~/unison_homes/mowgli/matita1.0-reallyfresh/matita/matitac extraction.ma 2> /tmp/foo.hs + cat preamble.hs /tmp/foo.hs > extraction.hs + +.PHONY: all + +# ghci extraction.hs diff --git a/matita/matita/lib/extraction.ma b/matita/matita/lib/extraction.ma index 7791d8922..35a9a5788 100644 --- a/matita/matita/lib/extraction.ma +++ b/matita/matita/lib/extraction.ma @@ -14,7 +14,11 @@ include "arithmetics/nat.ma". -(*BUG: kind signatures in type declarations*) +(*FEATURE: kind signatures in type declarations*) + +axiom Nat: Type[0]. +axiom S: Nat → Nat. +axiom O: Nat. axiom test1: Type[1]. @@ -25,12 +29,20 @@ axiom test3: Prop → Type[1] → CProp[1] → Type[1] → Type[2]. (* not in F_omega ? *) axiom test4: ∀A:Type[1]. A → ∀B:Type[1]. B → ∀C:Prop. C → Type[1]. +axiom test4': ∀C:Prop. C → C. + +axiom test4'': ∀C:Prop. C → Nat. + +axiom test4''': ∀C:Type[1]. C. + +axiom test4_5: (∀A:Type[0].A) → Nat. + axiom test5: (Type[1] → Type[1]) → Type[1]. (* no content *) axiom test6: Type[1] → Prop. -definition dtest1: Type[1] ≝ nat → nat. +definition dtest1: Type[1] ≝ Nat → Nat. definition dtest2: Type[2] ≝ ∀A:Type[1]. A → A. @@ -40,7 +52,7 @@ definition dtest4: Type[1] → Type[1] ≝ λA:Type[1].dtest3 A. definition dtest5: Type[1] → Type[1] ≝ dtest3. -definition dtest6: Type[1] ≝ dtest3 nat. +definition dtest6: Type[1] ≝ dtest3 Nat. (* no content *) definition dtest7: Prop ≝ True → True. @@ -53,25 +65,25 @@ definition dtest9: Type[1] ≝ dtest3 Prop. definition dtest10: Type[1] → Type[1] → Type[1] ≝ λX,Y.X. -(*BUG: a' vs a''*) -definition dtest11: Type[1] → nat → Type[1] → Type[1] ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1. +definition dtest11: Type[1] → Nat → Type[1] → Type[1] ≝ λ_:Type[1].λ_:Nat.λX:Type[1]. X → Nat → test1. -definition dtest12 ≝ λ_:Type[1].λ_:nat.λX:Type[1]. X → nat → test1. -definition dtest13 ≝ dtest3 nat → dtest3 True → dtest3 Prop → nat. +definition dtest12 ≝ λ_:Type[1].λ_:Nat.λX:Type[1]. X → Nat → test1. + +definition dtest13 ≝ dtest3 Nat → dtest3 True → dtest3 Prop → Nat. definition dtest14 ≝ λX:Type[2]. X → X. (*FEATURE: type the forall bound variables*) -definition dtest15 ≝ ∀T:Type[1] → Type[1]. T nat → T nat. +definition dtest15 ≝ ∀T:Type[1] → Type[1]. T Nat → T Nat. -definition dtest16 ≝ ∀T:Type[1]. T → nat. +definition dtest16 ≝ ∀T:Type[1]. T → Nat. -definition dtest17 ≝ ∀T:dtest14 Type[1]. T nat → dtest14 nat → dtest14 nat. +definition dtest17 ≝ ∀T:dtest14 Type[1]. T Nat → dtest14 Nat → dtest14 Nat. -definition dtest18 ≝ λA,B:Type[0].λn:nat.λC:Type[0].A. +definition dtest18 ≝ λA,B:Type[0].λn:Nat.λC:Type[0].A. -definition dtest19 ≝ dtest18 nat True O nat → dtest18 nat nat O nat. +definition dtest19 ≝ dtest18 Nat True O Nat → dtest18 Nat Nat O Nat. definition dtest20 ≝ test5 test2. @@ -79,10 +91,36 @@ definition dtest20 ≝ test5 test2. to be traced, raises NotInFOmega; why? *) definition dtest21 ≝ test5 (λX:Type[1].X). -definition ttest1 ≝ λx:nat.x. +definition ttest1 ≝ λx:Nat.x. (*BUG: clash of name due to capitalisation*) -definition Ttest1 ≝ λx:nat.x. +(*definition Ttest1 ≝ λx:Nat.x.*) + +(*FEATURE: print binders in the l.h.s. without using lambda abstraction*) +definition ttest2 ≝ λT:Type[1].λx:T.x. + +definition ttest3 ≝ λT:Type[1].λx:T.let y ≝ x in y. + +definition ttest4 ≝ λT:Type[1].let y ≝ T in λx:y.x. + +(*BUG IN HASKELL PRETTY PRINTING: all lets are let rec*) +(*definition ttest5 ≝ λT:Type[1].λy:T.let y ≝ y in y.*) + +definition ttest6 ≝ ttest4 Nat. + +definition ttest7 ≝ λf:∀X:Type[1].X. f (Nat → Nat) O. + +definition ttest8 ≝ λf:∀X:Type[1].X. f (True → True) I. + +definition ttest9 ≝ λf:∀X:Type[1].X. f (True → Nat) I. + +definition ttest10 ≝ λf:∀X:Type[1].X. f (True → Nat → Nat) I O. + +definition ttest11_aux ≝ λS:Type[1]. S → Nat. + +definition ttest11 ≝ λf:ttest11_aux True. f I. + +(*BUG here: requires F_omega eat_args*) +definition ttest12 ≝ λf:True → Nat. f I. -(*BUG: Failure nth*) -definition ttest2 ≝ λT:Type[1].λx:T.x. \ No newline at end of file +(*GENERAL BUG: name clashes when binders shadow each other in CIC*) diff --git a/matita/matita/lib/preamble.hs b/matita/matita/lib/preamble.hs new file mode 100644 index 000000000..2aea1bb44 --- /dev/null +++ b/matita/matita/lib/preamble.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE RankNTypes, KindSignatures #-} + +module Main where + + -- 2.39.2