new test suite

test-suite/Makefile

@@ -1,21 +1,12 @@
 COQBIN := ../../coq/bin/
 .PHONY: coq clean
 
-all: Parametricity.vo Theories_R.vo Ring_polynom_R.vo bug.vo
-
-Theories_R.vo: Theories_R.v Parametricity.vo
-	$(COQBIN)coqc -I ../src $<
-
-Ring_polynom_R.vo: Ring_polynom_R.v Theories_R.vo Theories_R.vo 
-	$(COQBIN)coqc -I ../src $<
+all: Parametricity.vo 
 
 Parametricity.vo: Parametricity.v
 	$(COQBIN)coqc -I ../src $<
 
-bug.vo: bug.v 
-	$(COQBIN)coqc -I ../src bug.v 
-
-ide:: 
+ide:: Parametricity.vo
 	$(COQBIN)coqide -I ../src *.v 
 
 clean:: 

test-suite/Parametricity.v

@@ -4,35 +4,21 @@ Declare ML Module "declare_translation".
 Declare ML Module "abstraction".
 
 
-Require Import ProofIrrelevance.
-Require CRelationClasses.
-Require Relation_Definitions Relation_Operators.
-Require Bool Basics Init Tactics Relation_Definitions RelationClasses Morphisms CRelationClasses.
+Require Import ProofIrrelevance. (* for opaque terms *)
 
 Translate Module Logic.
+
+(* Realizer of proof_admitted. *)
 Next Obligation.
 admit.
 Defined.
 
 Translate Module Datatypes.
-
-
-Translate Module Relation_Definitions.
 Translate Module Logic_Type.
 Translate Module Specif.
-Translate Module Relation_Operators.
-
-
 Translate Module Nat.
 Translate Module Peano.
-
 Translate Module Wf.
-
-
-
-Translate Module Bool.
-Translate Module Basics.
-Translate Module Init.
 Translate Module Tactics.
 
-Export Logic_R Datatypes_R Relation_Definitions_R Logic_Type_R Specif_R Relation_Operators_R Nat_R Peano_R Wf_R Bool_R Basics_R Init_R Tactics_R.
+Export Logic_R Datatypes_R Logic_Type_R Specif_R Nat_R Peano_R Wf_R Tactics_R.

test-suite/example.v

@@ -0,0 +1,165 @@
+Require Import Parametricity.
+
+(** Base Types. **)
+
+Inductive bool := true | false.
+
+Translate Inductive bool.
+
+Print bool_R.
+(* Prints:  
+Inductive bool_R : bool -> bool -> Set :=  
+  true_R : bool_R true true 
+| false_R : bool_R false false *)
+
+Lemma bool_R_eq:
+  forall x y, bool_R x y -> x = y.
+intros x y H.
+destruct H.
+* reflexivity.
+* reflexivity.
+Defined.
+
+Lemma bool_R_refl:
+   forall x, bool_R x x.
+induction x.
+constructor.
+constructor.
+Defined.
+
+(** Boolean functions **)
+
+Definition boolfun := bool -> bool.
+Translate boolfun.
+Print boolfun_R.
+(* Prints:
+boolfun_R = fun f1 f2 : bool -> bool => 
+   forall x1 x2 : bool, bool_R x1 x2 -> 
+                        bool_R (f1 x1) (f2 x2)
+*)
+
+Print Module Bool.
+
+Definition negb (x : bool) := 
+  match x with 
+   | true => false
+   | fale => true
+  end. 
+Translate negb.
+Check negb_R.
+Print negb_R.
+
+(** Universes **)
+
+Translate Type as Type_R.
+Print Type_R.
+(* Prints : 
+  Type_R = fun A1 A2 : Type => A1 -> A2 -> Type
+*)
+Check (bool_R : Type_R bool bool).
+Check (boolfun_R : Type_R boolfun boolfun).
+
+Polymorphic Definition pType := Type.
+Translate pType.
+Check (pType_R : pType_R pType pType).
+
+(** Simple arrows **)
+
+Definition arrow (A : Type) (B  : Type) := 
+  A -> B.
+
+Translate arrow.
+Print arrow_R.
+(* Prints: 
+arrow_R = 
+  fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
+      (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) 
+      (f₁ : A₁ -> B₁) (f₂ : A₂ -> B₂) =>
+  forall (x₁ : A₁) (x₂ : A₂), 
+    A_R x₁ x₂ -> B_R (f₁ x₁) (f₂ x₂)
+*)
+
+(** Lambdas **)
+Definition lambda (A : Type) (B : Type)
+  (f : arrow A B) := fun x => f x.
+Translate lambda.
+Print lambda_R.
+(* lambda_R = 
+fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type)
+    (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) 
+  (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂) 
+     (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) 
+  (x₁ : A₁) (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R *)
+
+(** Applications of functions *)
+Definition application A B (f : arrow A B) (x : A) : B :=
+  f x.
+Translate application.
+Print application_R.
+(* Prints : 
+fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
+    (B₁ B₂ : Type) (B_R : B₁ -> B₂ -> Type) 
+    (f₁ : arrow A₁ B₁) (f₂ : arrow A₂ B₂) 
+          (f_R : arrow_R A₁ A₂ A_R B₁ B₂ B_R f₁ f₂) 
+    (x₁ : A₁) (x₂ : A₂) (x_R : A_R x₁ x₂) => f_R x₁ x₂ x_R. *)
+
+(** Dependent product **)
+Definition for_all (A : Type) (B : A -> Type) := forall x, B x.
+Translate for_all.
+Print for_all_R.
+(* Prints: 
+for_all_R =
+fun (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) 
+    (B₁ : A₁ -> Type) (B₂ : A₂ -> Type) 
+    (B_R : forall (x₁ : A₁) (x₂ : A₂), A_R x₁ x₂ -> B₁ x₁ -> B₂ x₂ -> Type) 
+    (f₁ : forall x : A₁, B₁ x) (f₂ : forall x : A₂, B₂ x) => 
+for all (x₁ : A₁) (x₂ : A₂) (x_R : A_R x₁ x₂), B_R x₁ x₂ x_R (f₁ x₁) (f₂ x₂)
+*)
+
+(** Inductive types. *)
+Inductive nat := 
+  | O : nat 
+  | S : nat -> nat.
+Translate Inductive nat.
+Print nat_R.
+(* Prints:
+Inductive nat_R : nat -> nat -> Set :=  
+  O_R : nat_R 0 0 
+| S_R : forall n₁ n₂ : nat, nat_R n₁ n₂ -> nat_R (S n₁) (S n₂) *)
+
+Inductive list (A : Type) : Type :=  nil : list A | cons : A -> list A -> list A.
+Translate Inductive list.
+Print list_R.
+(* Prints : 
+Inductive list_R (A₁ A₂ : Type) (A_R : A₁ -> A₂ -> Type) : 
+                                         list A₁ -> list A₂ -> Type :=
+    nil_R : list_R A₁ A₂ A_R (nil A₁) (nil A₂)
+  | cons_R : forall (x₁ : A₁) (x₂ : A₂), A_R x₁ x₂ -> 
+    forall (l₁ : list A₁) (l₂ : list A₂),
+    list_R A₁ A₂ A_R l₁ l₂ -> list_R A₁ A₂ A_R (cons A₁ x₁ l₁) (cons A₂ x₂ l₂)
+*)
+
+Fixpoint length A (l : list A) : nat := 
+  match l with nil _ => O | cons _ _ tl => S (length A tl) end.
+Translate length.
+Check length_R.
+Print length_R.
+(* Prints : ... something that looks complicated. *)
+
+Translate list_rec.
+Print list_rec_R.
+Definition length2 (A : Type) (l : list A) : nat :=
+  list_rec A (fun _ => nat) O (fun _ _ => S) l.
+Translate length2.
+Check length2_R.
+Print length2_R.
+
+Print sum_rect.
+
+Translate sum_rect.
+Check sum_rect.
+Check sum_rect_R.
+Print Datatypes_R.sum_rect_R.
+
+
+

test-suite/features.v

@@ -0,0 +1,80 @@
+Require Import Parametricity.
+
+
+(** Separate compilation: *)
+Translate nat as test.
+Require List.
+Translate List.rev.
+Check rev_R.
+
+(** Module translation *)
+Module A.
+  Definition t := nat.
+  Module B.
+   Definition t := nat -> nat.
+  End B.
+End A.
+
+Translate Module A.
+Print Module A_R.
+Print Module A_R.B_R.
+
+Translate Module Bool.
+Print Module Bool_R.
+
+(** Unary parametricity *)
+Translate (forall X, X -> X) as ID_R arity 1.
+
+Lemma ID_unique: 
+  forall f, ID_R f -> forall A x, f A x = x.
+intros f f_R A x.
+specialize (f_R A (fun y => y = x) x).
+apply f_R.
+reflexivity.
+Defined.
+
+Translate Inductive nat arity 10.
+Print nat_R_10.
+
+(** Realizing axioms and section variables. *)
+Section Test.
+Variable A : Set.
+Variable R : A -> A -> Set.
+Realizer A as A_R := R.
+Definition id : A -> A := fun x => x.
+Translate id.
+End Test.
+
+Realizer proof_admitted as proof_admitted_R := _.
+Next Obligation.
+admit.
+Defined.
+
+Lemma test_admit: 2+2 = 5.
+admit.
+Defined.
+Translate test_admit.
+Print test_admit_R.
+
+(** Opaque terms. **)
+
+Require ProofIrrelevance.
+
+Lemma opaque : True.
+trivial.
+Qed.
+Translate opaque.
+Eval compute in opaque.
+Eval compute in opaque_R.
+
+
+Lemma opaquenat : nat.
+exact 41.
+Qed.
+Translate opaquenat.
+Next Obligation.
+admit.
+Defined.
+
+
+