diff options
Diffstat (limited to 'contrib/correctness')
54 files changed, 8404 insertions, 0 deletions
diff --git a/contrib/correctness/ArrayPermut.v b/contrib/correctness/ArrayPermut.v new file mode 100644 index 00000000..b352045a --- /dev/null +++ b/contrib/correctness/ArrayPermut.v @@ -0,0 +1,175 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ArrayPermut.v,v 1.3.2.1 2004/07/16 19:29:59 herbelin Exp $ *) + +(****************************************************************************) +(* Permutations of elements in arrays *) +(* Definition and properties *) +(****************************************************************************) + +Require Import ProgInt. +Require Import Arrays. +Require Export Exchange. + +Require Import Omega. + +Set Implicit Arguments. + +(* We define "permut" as the smallest equivalence relation which contains + * transpositions i.e. exchange of two elements. + *) + +Inductive permut (n:Z) (A:Set) : array n A -> array n A -> Prop := + | exchange_is_permut : + forall (t t':array n A) (i j:Z), exchange t t' i j -> permut t t' + | permut_refl : forall t:array n A, permut t t + | permut_sym : forall t t':array n A, permut t t' -> permut t' t + | permut_trans : + forall t t' t'':array n A, permut t t' -> permut t' t'' -> permut t t''. + +Hint Resolve exchange_is_permut permut_refl permut_sym permut_trans: v62 + datatypes. + +(* We also define the permutation on a segment of an array, "sub_permut", + * the other parts of the array being unchanged + * + * One again we define it as the smallest equivalence relation containing + * transpositions on the given segment. + *) + +Inductive sub_permut (n:Z) (A:Set) (g d:Z) : +array n A -> array n A -> Prop := + | exchange_is_sub_permut : + forall (t t':array n A) (i j:Z), + (g <= i <= d)%Z -> + (g <= j <= d)%Z -> exchange t t' i j -> sub_permut g d t t' + | sub_permut_refl : forall t:array n A, sub_permut g d t t + | sub_permut_sym : + forall t t':array n A, sub_permut g d t t' -> sub_permut g d t' t + | sub_permut_trans : + forall t t' t'':array n A, + sub_permut g d t t' -> sub_permut g d t' t'' -> sub_permut g d t t''. + +Hint Resolve exchange_is_sub_permut sub_permut_refl sub_permut_sym + sub_permut_trans: v62 datatypes. + +(* To express that some parts of arrays are equal we introduce the + * property "array_id" which says that a segment is the same on two + * arrays. + *) + +Definition array_id (n:Z) (A:Set) (t t':array n A) + (g d:Z) := forall i:Z, (g <= i <= d)%Z -> #t [i] = #t' [i]. + +(* array_id is an equivalence relation *) + +Lemma array_id_refl : + forall (n:Z) (A:Set) (t:array n A) (g d:Z), array_id t t g d. +Proof. +unfold array_id in |- *. +auto with datatypes. +Qed. + +Hint Resolve array_id_refl: v62 datatypes. + +Lemma array_id_sym : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + array_id t t' g d -> array_id t' t g d. +Proof. +unfold array_id in |- *. intros. +symmetry in |- *; auto with datatypes. +Qed. + +Hint Resolve array_id_sym: v62 datatypes. + +Lemma array_id_trans : + forall (n:Z) (A:Set) (t t' t'':array n A) (g d:Z), + array_id t t' g d -> array_id t' t'' g d -> array_id t t'' g d. +Proof. +unfold array_id in |- *. intros. +apply trans_eq with (y := #t' [i]); auto with datatypes. +Qed. + +Hint Resolve array_id_trans: v62 datatypes. + +(* Outside the segment [g,d] the elements are equal *) + +Lemma sub_permut_id : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + sub_permut g d t t' -> + array_id t t' 0 (g - 1) /\ array_id t t' (d + 1) (n - 1). +Proof. +intros n A t t' g d. simple induction 1; intros. +elim H2; intros. +unfold array_id in |- *; split; intros. +apply H7; omega. +apply H7; omega. +auto with datatypes. +decompose [and] H1; auto with datatypes. +decompose [and] H1; decompose [and] H3; eauto with datatypes. +Qed. + +Hint Resolve sub_permut_id. + +Lemma sub_permut_eq : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + sub_permut g d t t' -> + forall i:Z, (0 <= i < g)%Z \/ (d < i < n)%Z -> #t [i] = #t' [i]. +Proof. +intros n A t t' g d Htt' i Hi. +elim (sub_permut_id Htt'). unfold array_id in |- *. +intros. +elim Hi; [ intro; apply H; omega | intro; apply H0; omega ]. +Qed. + +(* sub_permut is a particular case of permutation *) + +Lemma sub_permut_is_permut : + forall (n:Z) (A:Set) (t t':array n A) (g d:Z), + sub_permut g d t t' -> permut t t'. +Proof. +intros n A t t' g d. simple induction 1; intros; eauto with datatypes. +Qed. + +Hint Resolve sub_permut_is_permut. + +(* If we have a sub-permutation on an empty segment, then we have a + * sub-permutation on any segment. + *) + +Lemma sub_permut_void : + forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z), + (d < g)%Z -> sub_permut g d t t' -> sub_permut g' d' t t'. +Proof. +intros N A t t' g g' d d' Hdg. +simple induction 1; intros. +absurd (g <= d)%Z; omega. +auto with datatypes. +auto with datatypes. +eauto with datatypes. +Qed. + +(* A sub-permutation on a segment may be extended to any segment that + * contains the first one. + *) + +Lemma sub_permut_extension : + forall (N:Z) (A:Set) (t t':array N A) (g g' d d':Z), + (g' <= g)%Z -> (d <= d')%Z -> sub_permut g d t t' -> sub_permut g' d' t t'. +Proof. +intros N A t t' g g' d d' Hgg' Hdd'. +simple induction 1; intros. +apply exchange_is_sub_permut with (i := i) (j := j); + [ omega | omega | assumption ]. +auto with datatypes. +auto with datatypes. +eauto with datatypes. +Qed.
\ No newline at end of file diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v new file mode 100644 index 00000000..1659917a --- /dev/null +++ b/contrib/correctness/Arrays.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Arrays.v,v 1.9.2.1 2004/07/16 19:29:59 herbelin Exp $ *) + +(**********************************************) +(* Functional arrays, for use in Correctness. *) +(**********************************************) + +(* This is an axiomatization of arrays. + * + * The type (array N T) is the type of arrays ranging from 0 to N-1 + * which elements are of type T. + * + * Arrays are created with new, accessed with access and modified with store. + * + * Operations of accessing and storing are not guarded, but axioms are. + * So these arrays can be viewed as arrays where accessing and storing + * out of the bounds has no effect. + *) + + +Require Export ProgInt. + +Set Implicit Arguments. + + +(* The type of arrays *) + +Parameter array : Z -> Set -> Set. + + +(* Functions to create, access and modify arrays *) + +Parameter new : forall (n:Z) (T:Set), T -> array n T. + +Parameter access : forall (n:Z) (T:Set), array n T -> Z -> T. + +Parameter store : forall (n:Z) (T:Set), array n T -> Z -> T -> array n T. + + +(* Axioms *) + +Axiom + new_def : + forall (n:Z) (T:Set) (v0:T) (i:Z), + (0 <= i < n)%Z -> access (new n v0) i = v0. + +Axiom + store_def_1 : + forall (n:Z) (T:Set) (t:array n T) (v:T) (i:Z), + (0 <= i < n)%Z -> access (store t i v) i = v. + +Axiom + store_def_2 : + forall (n:Z) (T:Set) (t:array n T) (v:T) (i j:Z), + (0 <= i < n)%Z -> + (0 <= j < n)%Z -> i <> j -> access (store t i v) j = access t j. + +Hint Resolve new_def store_def_1 store_def_2: datatypes v62. + +(* A tactic to simplify access in arrays *) + +Ltac array_access i j H := + elim (Z_eq_dec i j); + [ intro H; rewrite H; rewrite store_def_1 + | intro H; rewrite store_def_2; [ idtac | idtac | idtac | exact H ] ]. + +(* Symbolic notation for access *) + +Notation "# t [ c ]" := (access t c) (at level 0, t at level 0).
\ No newline at end of file diff --git a/contrib/correctness/Arrays_stuff.v b/contrib/correctness/Arrays_stuff.v new file mode 100644 index 00000000..899d7007 --- /dev/null +++ b/contrib/correctness/Arrays_stuff.v @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Arrays_stuff.v,v 1.2.16.1 2004/07/16 19:29:59 herbelin Exp $ *) + +Require Export Exchange. +Require Export ArrayPermut. +Require Export Sorted. + diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v new file mode 100644 index 00000000..a2ad2f50 --- /dev/null +++ b/contrib/correctness/Correctness.v @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Correctness.v,v 1.6.2.1 2004/07/16 19:29:59 herbelin Exp $ *) + +(* Correctness is base on the tactic Refine (developped on purpose) *) + +Require Export Tuples. + +Require Export ProgInt. +Require Export ProgBool. +Require Export Zwf. + +Require Export Arrays. + +(* +Token "'". +*)
\ No newline at end of file diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v new file mode 100644 index 00000000..7dc5218e --- /dev/null +++ b/contrib/correctness/Exchange.v @@ -0,0 +1,95 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Exchange.v,v 1.4.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +(****************************************************************************) +(* Exchange of two elements in an array *) +(* Definition and properties *) +(****************************************************************************) + +Require Import ProgInt. +Require Import Arrays. + +Set Implicit Arguments. + +(* Definition *) + +Inductive exchange (n:Z) (A:Set) (t t':array n A) (i j:Z) : Prop := + exchange_c : + (0 <= i < n)%Z -> + (0 <= j < n)%Z -> + #t [i] = #t' [j] -> + #t [j] = #t' [i] -> + (forall k:Z, (0 <= k < n)%Z -> k <> i -> k <> j -> #t [k] = #t' [k]) -> + exchange t t' i j. + +(* Properties about exchanges *) + +Lemma exchange_1 : + forall (n:Z) (A:Set) (t:array n A) (i j:Z), + (0 <= i < n)%Z -> + (0 <= j < n)%Z -> #(store (store t i #t [j]) j #t [i]) [i] = #t [j]. +Proof. +intros n A t i j H_i H_j. +case (dec_eq j i). +intro eq_i_j. rewrite eq_i_j. +auto with datatypes. +intro not_j_i. +rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_i not_j_i). +auto with datatypes. +Qed. + +Hint Resolve exchange_1: v62 datatypes. + + +Lemma exchange_proof : + forall (n:Z) (A:Set) (t:array n A) (i j:Z), + (0 <= i < n)%Z -> + (0 <= j < n)%Z -> exchange (store (store t i #t [j]) j #t [i]) t i j. +Proof. +intros n A t i j H_i H_j. +apply exchange_c; auto with datatypes. +intros k H_k not_k_i not_k_j. +cut (j <> k); auto with datatypes. intro not_j_k. +rewrite (store_def_2 (store t i #t [j]) #t [i] H_j H_k not_j_k). +auto with datatypes. +Qed. + +Hint Resolve exchange_proof: v62 datatypes. + + +Lemma exchange_sym : + forall (n:Z) (A:Set) (t t':array n A) (i j:Z), + exchange t t' i j -> exchange t' t i j. +Proof. +intros n A t t' i j H1. +elim H1. clear H1. intros. +constructor 1; auto with datatypes. +intros. rewrite (H3 k); auto with datatypes. +Qed. + +Hint Resolve exchange_sym: v62 datatypes. + + +Lemma exchange_id : + forall (n:Z) (A:Set) (t t':array n A) (i j:Z), + exchange t t' i j -> + i = j -> forall k:Z, (0 <= k < n)%Z -> #t [k] = #t' [k]. +Proof. +intros n A t t' i j Hex Heq k Hk. +elim Hex. clear Hex. intros. +rewrite Heq in H1. rewrite Heq in H2. +case (Z_eq_dec k j). + intro Heq'. rewrite Heq'. assumption. + intro Hnoteq. apply (H3 k); auto with datatypes. rewrite Heq. assumption. +Qed. + +Hint Resolve exchange_id: v62 datatypes.
\ No newline at end of file diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v new file mode 100644 index 00000000..bce19870 --- /dev/null +++ b/contrib/correctness/ProgBool.v @@ -0,0 +1,66 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ProgBool.v,v 1.4.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +Require Import ZArith. +Require Export Bool_nat. +Require Export Sumbool. + +Definition annot_bool : + forall b:bool, {b' : bool | if b' then b = true else b = false}. +Proof. +intro b. +exists b. case b; trivial. +Qed. + + +(* Logical connectives *) + +Definition spec_and (A B C D:Prop) (b:bool) := if b then A /\ C else B \/ D. + +Definition prog_bool_and : + forall Q1 Q2:bool -> Prop, + sig Q1 -> + sig Q2 -> + {b : bool | if b then Q1 true /\ Q2 true else Q1 false \/ Q2 false}. +Proof. +intros Q1 Q2 H1 H2. +elim H1. intro b1. elim H2. intro b2. +case b1; case b2; intros. +exists true; auto. +exists false; auto. exists false; auto. exists false; auto. +Qed. + +Definition spec_or (A B C D:Prop) (b:bool) := if b then A \/ C else B /\ D. + +Definition prog_bool_or : + forall Q1 Q2:bool -> Prop, + sig Q1 -> + sig Q2 -> + {b : bool | if b then Q1 true \/ Q2 true else Q1 false /\ Q2 false}. +Proof. +intros Q1 Q2 H1 H2. +elim H1. intro b1. elim H2. intro b2. +case b1; case b2; intros. +exists true; auto. exists true; auto. exists true; auto. +exists false; auto. +Qed. + +Definition spec_not (A B:Prop) (b:bool) := if b then B else A. + +Definition prog_bool_not : + forall Q:bool -> Prop, sig Q -> {b : bool | if b then Q false else Q true}. +Proof. +intros Q H. +elim H. intro b. +case b; intro. +exists false; auto. exists true; auto. +Qed. diff --git a/contrib/correctness/ProgInt.v b/contrib/correctness/ProgInt.v new file mode 100644 index 00000000..c26e3553 --- /dev/null +++ b/contrib/correctness/ProgInt.v @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ProgInt.v,v 1.2.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +Require Export ZArith. +Require Export ZArith_dec. + +Theorem Znotzero : forall x:Z, {x <> 0%Z} + {x = 0%Z}. +Proof. +intro x. elim (Z_eq_dec x 0); auto. +Qed.
\ No newline at end of file diff --git a/contrib/correctness/ProgramsExtraction.v b/contrib/correctness/ProgramsExtraction.v new file mode 100644 index 00000000..40253f33 --- /dev/null +++ b/contrib/correctness/ProgramsExtraction.v @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ProgramsExtraction.v,v 1.2.16.1 2004/07/16 19:30:00 herbelin Exp $ *) + +Require Export Extraction. + +Extract Inductive unit => unit [ "()" ]. +Extract Inductive bool => bool [ true false ]. +Extract Inductive sumbool => bool [ true false ]. + +Require Export Correctness. + +Declare ML Module "pextract". + +Grammar vernac vernac : ast := + imperative_ocaml [ "Write" "Caml" "File" stringarg($file) + "[" ne_identarg_list($idl) "]" "." ] + -> [ (IMPERATIVEEXTRACTION $file (VERNACARGLIST ($LIST $idl))) ] + +| initialize [ "Initialize" identarg($id) "with" comarg($c) "." ] + -> [ (INITIALIZE $id $c) ] +. diff --git a/contrib/correctness/Programs_stuff.v b/contrib/correctness/Programs_stuff.v new file mode 100644 index 00000000..1ca4b63e --- /dev/null +++ b/contrib/correctness/Programs_stuff.v @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Programs_stuff.v,v 1.1.16.1 2004/07/16 19:30:00 herbelin Exp $ *) + +Require Export Arrays_stuff. diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v new file mode 100644 index 00000000..2efe54a4 --- /dev/null +++ b/contrib/correctness/Sorted.v @@ -0,0 +1,202 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Library about sorted (sub-)arrays / Nicolas Magaud, July 1998 *) + +(* $Id: Sorted.v,v 1.7.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +Require Export Arrays. +Require Import ArrayPermut. + +Require Import ZArithRing. +Require Import Omega. +Open Local Scope Z_scope. + +Set Implicit Arguments. + +(* Definition *) + +Definition sorted_array (N:Z) (A:array N Z) (deb fin:Z) := + deb <= fin -> forall x:Z, x >= deb -> x < fin -> #A [x] <= #A [x + 1]. + +(* Elements of a sorted sub-array are in increasing order *) + +(* one element and the next one *) + +Lemma sorted_elements_1 : + forall (N:Z) (A:array N Z) (n m:Z), + sorted_array A n m -> + forall k:Z, + k >= n -> forall i:Z, 0 <= i -> k + i <= m -> #A [k] <= #A [k + i]. +Proof. +intros N A n m H_sorted k H_k i H_i. +pattern i in |- *. apply natlike_ind. +intro. +replace (k + 0) with k; omega. (*** Ring `k+0` => BUG ***) + +intros. +apply Zle_trans with (m := #A [k + x]). +apply H0; omega. + +unfold Zsucc in |- *. +replace (k + (x + 1)) with (k + x + 1). +unfold sorted_array in H_sorted. +apply H_sorted; omega. + +omega. + +assumption. +Qed. + +(* one element and any of the following *) + +Lemma sorted_elements : + forall (N:Z) (A:array N Z) (n m k l:Z), + sorted_array A n m -> + k >= n -> l < N -> k <= l -> l <= m -> #A [k] <= #A [l]. +Proof. +intros. +replace l with (k + (l - k)). +apply sorted_elements_1 with (n := n) (m := m); + [ assumption | omega | omega | omega ]. +omega. +Qed. + +Hint Resolve sorted_elements: datatypes v62. + +(* A sub-array of a sorted array is sorted *) + +Lemma sub_sorted_array : + forall (N:Z) (A:array N Z) (deb fin i j:Z), + sorted_array A deb fin -> + i >= deb -> j <= fin -> i <= j -> sorted_array A i j. +Proof. +unfold sorted_array in |- *. +intros. +apply H; omega. +Qed. + +Hint Resolve sub_sorted_array: datatypes v62. + +(* Extension on the left of the property of being sorted *) + +Lemma left_extension : + forall (N:Z) (A:array N Z) (i j:Z), + i > 0 -> + j < N -> + sorted_array A i j -> #A [i - 1] <= #A [i] -> sorted_array A (i - 1) j. +Proof. +intros; unfold sorted_array in |- *; intros. +elim (Z_ge_lt_dec x i). (* (`x >= i`) + (`x < i`) *) +intro Hcut. +apply H1; omega. + +intro Hcut. +replace x with (i - 1). +replace (i - 1 + 1) with i; [ assumption | omega ]. + +omega. +Qed. + +(* Extension on the right *) + +Lemma right_extension : + forall (N:Z) (A:array N Z) (i j:Z), + i >= 0 -> + j < N - 1 -> + sorted_array A i j -> #A [j] <= #A [j + 1] -> sorted_array A i (j + 1). +Proof. +intros; unfold sorted_array in |- *; intros. +elim (Z_lt_ge_dec x j). +intro Hcut. +apply H1; omega. + +intro HCut. +replace x with j; [ assumption | omega ]. +Qed. + +(* Substitution of the leftmost value by a smaller value *) + +Lemma left_substitution : + forall (N:Z) (A:array N Z) (i j v:Z), + i >= 0 -> + j < N -> + sorted_array A i j -> v <= #A [i] -> sorted_array (store A i v) i j. +Proof. +intros N A i j v H_i H_j H_sorted H_v. +unfold sorted_array in |- *; intros. + +cut (x = i \/ x > i). +intro Hcut; elim Hcut; clear Hcut; intro. +rewrite H2. +rewrite store_def_1; try omega. +rewrite store_def_2; try omega. +apply Zle_trans with (m := #A [i]); [ assumption | apply H_sorted; omega ]. + +rewrite store_def_2; try omega. +rewrite store_def_2; try omega. +apply H_sorted; omega. +omega. +Qed. + +(* Substitution of the rightmost value by a larger value *) + +Lemma right_substitution : + forall (N:Z) (A:array N Z) (i j v:Z), + i >= 0 -> + j < N -> + sorted_array A i j -> #A [j] <= v -> sorted_array (store A j v) i j. +Proof. +intros N A i j v H_i H_j H_sorted H_v. +unfold sorted_array in |- *; intros. + +cut (x = j - 1 \/ x < j - 1). +intro Hcut; elim Hcut; clear Hcut; intro. +rewrite H2. +replace (j - 1 + 1) with j; [ idtac | omega ]. (*** Ring `j-1+1`. => BUG ***) +rewrite store_def_2; try omega. +rewrite store_def_1; try omega. +apply Zle_trans with (m := #A [j]). +apply sorted_elements with (n := i) (m := j); try omega; assumption. +assumption. + +rewrite store_def_2; try omega. +rewrite store_def_2; try omega. +apply H_sorted; omega. + +omega. +Qed. + +(* Affectation outside of the sorted region *) + +Lemma no_effect : + forall (N:Z) (A:array N Z) (i j k v:Z), + i >= 0 -> + j < N -> + sorted_array A i j -> + 0 <= k < i \/ j < k < N -> sorted_array (store A k v) i j. +Proof. +intros. +unfold sorted_array in |- *; intros. +rewrite store_def_2; try omega. +rewrite store_def_2; try omega. +apply H1; assumption. +Qed. + +Lemma sorted_array_id : + forall (N:Z) (t1 t2:array N Z) (g d:Z), + sorted_array t1 g d -> array_id t1 t2 g d -> sorted_array t2 g d. +Proof. +intros N t1 t2 g d Hsorted Hid. +unfold array_id in Hid. +unfold sorted_array in Hsorted. unfold sorted_array in |- *. +intros Hgd x H1x H2x. +rewrite <- (Hid x); [ idtac | omega ]. +rewrite <- (Hid (x + 1)); [ idtac | omega ]. +apply Hsorted; assumption. +Qed.
\ No newline at end of file diff --git a/contrib/correctness/Tuples.v b/contrib/correctness/Tuples.v new file mode 100644 index 00000000..e3fff08d --- /dev/null +++ b/contrib/correctness/Tuples.v @@ -0,0 +1,98 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Tuples.v,v 1.2.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +(* Tuples *) + +Definition tuple_1 (X:Set) := X. +Definition tuple_2 := prod. +Definition Build_tuple_2 := pair. +Definition proj_2_1 := fst. +Definition proj_2_2 := snd. + +Record tuple_3 (T1 T2 T3:Set) : Set := + {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}. + +Record tuple_4 (T1 T2 T3 T4:Set) : Set := + {proj_4_1 : T1; proj_4_2 : T2; proj_4_3 : T3; proj_4_4 : T4}. + +Record tuple_5 (T1 T2 T3 T4 T5:Set) : Set := + {proj_5_1 : T1; proj_5_2 : T2; proj_5_3 : T3; proj_5_4 : T4; proj_5_5 : T5}. + +Record tuple_6 (T1 T2 T3 T4 T5 T6:Set) : Set := + {proj_6_1 : T1; + proj_6_2 : T2; + proj_6_3 : T3; + proj_6_4 : T4; + proj_6_5 : T5; + proj_6_6 : T6}. + +Record tuple_7 (T1 T2 T3 T4 T5 T6 T7:Set) : Set := + {proj_7_1 : T1; + proj_7_2 : T2; + proj_7_3 : T3; + proj_7_4 : T4; + proj_7_5 : T5; + proj_7_6 : T6; + proj_7_7 : T7}. + + +(* Existentials *) + +Definition sig_1 := sig. +Definition exist_1 := exist. + +Inductive sig_2 (T1 T2:Set) (P:T1 -> T2 -> Prop) : Set := + exist_2 : forall (x1:T1) (x2:T2), P x1 x2 -> sig_2 T1 T2 P. + +Inductive sig_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Prop) : Set := + exist_3 : forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> sig_3 T1 T2 T3 P. + + +Inductive sig_4 (T1 T2 T3 T4:Set) (P:T1 -> T2 -> T3 -> T4 -> Prop) : Set := + exist_4 : + forall (x1:T1) (x2:T2) (x3:T3) (x4:T4), + P x1 x2 x3 x4 -> sig_4 T1 T2 T3 T4 P. + +Inductive sig_5 (T1 T2 T3 T4 T5:Set) (P:T1 -> T2 -> T3 -> T4 -> T5 -> Prop) : +Set := + exist_5 : + forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5), + P x1 x2 x3 x4 x5 -> sig_5 T1 T2 T3 T4 T5 P. + +Inductive sig_6 (T1 T2 T3 T4 T5 T6:Set) +(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> Prop) : Set := + exist_6 : + forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) + (x6:T6), P x1 x2 x3 x4 x5 x6 -> sig_6 T1 T2 T3 T4 T5 T6 P. + +Inductive sig_7 (T1 T2 T3 T4 T5 T6 T7:Set) +(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> Prop) : Set := + exist_7 : + forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) + (x6:T6) (x7:T7), + P x1 x2 x3 x4 x5 x6 x7 -> sig_7 T1 T2 T3 T4 T5 T6 T7 P. + +Inductive sig_8 (T1 T2 T3 T4 T5 T6 T7 T8:Set) +(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> T8 -> Prop) : Set := + exist_8 : + forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) + (x6:T6) (x7:T7) (x8:T8), + P x1 x2 x3 x4 x5 x6 x7 x8 -> sig_8 T1 T2 T3 T4 T5 T6 T7 T8 P. + +Inductive dep_tuple_2 (T1 T2:Set) (P:T1 -> T2 -> Set) : Set := + Build_dep_tuple_2 : + forall (x1:T1) (x2:T2), P x1 x2 -> dep_tuple_2 T1 T2 P. + +Inductive dep_tuple_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Set) : Set := + Build_dep_tuple_3 : + forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> dep_tuple_3 T1 T2 T3 P. + diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v new file mode 100644 index 00000000..8c983a72 --- /dev/null +++ b/contrib/correctness/examples/Handbook.v @@ -0,0 +1,232 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: Handbook.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) + +(* This file contains proofs of programs taken from the + * "Handbook of Theoretical Computer Science", volume B, + * chapter "Methods and Logics for Proving Programs", by P. Cousot, + * pp 841--993, Edited by J. van Leeuwen (c) Elsevier Science Publishers B.V. + * 1990. + * + * Programs are refered to by numbers and pages. + *) + +Require Correctness. + +Require Sumbool. +Require Omega. +Require Zcomplements. +Require Zpower. + +(****************************************************************************) + +(* program (2) page 853 to compute x^y (annotated version is (25) page 860) *) + +(* en attendant... *) +Parameter Zdiv2 : Z->Z. + +Parameter Zeven_odd_dec : (x:Z){`x=2*(Zdiv2 x)`}+{`x=2*(Zdiv2 x)+1`}. +Definition Zodd_dec := [z:Z](sumbool_not ? ? (Zeven_odd_dec z)). +Definition Zodd_bool := [z:Z](bool_of_sumbool ? ? (Zodd_dec z)). + +Axiom axiom1 : (x,y:Z) `y>0` -> `x*(Zpower x (Zpred y)) = (Zpower x y)`. +Axiom axiom2 : (x:Z)`x>0` -> `(Zdiv2 x)<x`. +Axiom axiom3 : (x,y:Z) `y>=0` -> `(Zpower (x*x) (Zdiv2 y)) = (Zpower x y)`. + +Global Variable X : Z ref. +Global Variable Y : Z ref. +Global Variable Z_ : Z ref. + +Correctness pgm25 + { `Y >= 0` } + begin + Z_ := 1; + while !Y <> 0 do + { invariant `Y >= 0` /\ `Z_ * (Zpower X Y) = (Zpower X@0 Y@0)` + variant Y } + if (Zodd_bool !Y) then begin + Y := (Zpred !Y); + Z_ := (Zmult !Z_ !X) + end else begin + Y := (Zdiv2 !Y); + X := (Zmult !X !X) + end + done + end + { Z_ = (Zpower X@ Y@) }. +Proof. +Split. +Unfold Zpred; Unfold Zwf; Omega. +Split. +Unfold Zpred; Omega. +Decompose [and] Pre2. +Rewrite <- H0. +Replace `Z_1*X0*(Zpower X0 (Zpred Y0))` with `Z_1*(X0*(Zpower X0 (Zpred Y0)))`. +Apply f_equal with f := (Zmult Z_1). +Apply axiom1. +Omega. + +Auto. +Symmetry. +Apply Zmult_assoc_r. + +Split. +Unfold Zwf. +Repeat (Apply conj). +Omega. + +Omega. + +Apply axiom2. Omega. + +Split. +Omega. + +Decompose [and] Pre2. +Rewrite <- H0. +Apply f_equal with f:=(Zmult Z_1). +Apply axiom3. Omega. + +Omega. + +Decompose [and] Post6. +Rewrite <- H2. +Rewrite H0. +Simpl. +Omega. + +Save. + + +(****************************************************************************) + +(* program (178) page 934 to compute the factorial using global variables + * annotated version is (185) page 939 + *) + +Parameter Zfact : Z -> Z. + +Axiom axiom4 : `(Zfact 0) = 1`. +Axiom axiom5 : (x:Z) `x>0` -> `(Zfact (x-1))*x=(Zfact x)`. + +Correctness pgm178 +let rec F (u:unit) : unit { variant X } = + { `X>=0` } + (if !X = 0 then + Y := 1 + else begin + label L; + X := (Zpred !X); + (F tt); + X := (Zs !X); + Y := (Zmult !Y !X) + end) + { `X=X@` /\ `Y=(Zfact X@)` }. +Proof. +Rewrite Test1. Rewrite axiom4. Auto. +Unfold Zwf. Unfold Zpred. Omega. +Unfold Zpred. Omega. +Unfold Zs. Unfold Zpred in Post3. Split. +Omega. +Decompose [and] Post3. +Rewrite H. +Replace `X0+(-1)+1` with X0. +Rewrite H0. +Replace `X0+(-1)` with `X0-1`. +Apply axiom5. +Omega. +Omega. +Omega. +Save. + + +(****************************************************************************) + +(* program (186) page 939 "showing the usefulness of auxiliary variables" ! *) + +Global Variable N : Z ref. +Global Variable S : Z ref. + +Correctness pgm186 +let rec F (u:unit) : unit { variant N } = + { `N>=0` } + (if !N > 0 then begin + label L; + N := (Zpred !N); + (F tt); + S := (Zs !S); + (F tt); + N := (Zs !N) + end) + { `N=N@` /\ `S=S@+(Zpower 2 N@)-1` }. +Proof. +Unfold Zwf. Unfold Zpred. Omega. +Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zwf. Unfold Zpred. Omega. +Decompose [and] Post5. Rewrite H. Unfold Zpred. Omega. +Split. +Unfold Zpred in Post5. Omega. +Decompose [and] Post4. Rewrite H0. +Decompose [and] Post5. Rewrite H2. Rewrite H1. +Replace `(Zpower 2 N0)` with `2*(Zpower 2 (Zpred N0))`. Omega. +Symmetry. +Replace `(Zpower 2 N0)` with `(Zpower 2 (1+(Zpred N0)))`. +Replace `2*(Zpower 2 (Zpred N0))` with `(Zpower 2 1)*(Zpower 2 (Zpred N0))`. +Apply Zpower_exp. +Omega. +Unfold Zpred. Omega. +Auto. +Replace `(1+(Zpred N0))` with N0; [ Auto | Unfold Zpred; Omega ]. +Split. +Auto. +Replace N0 with `0`; Simpl; Omega. +Save. + + +(****************************************************************************) + +(* program (196) page 944 (recursive factorial procedure with value-result + * parameters) + *) + +Correctness pgm196 +let rec F (U:Z) (V:Z ref) : unit { variant U } = + { `U >= 0` } + (if U = 0 then + V := 1 + else begin + (F (Zpred U) V); + V := (Zmult !V U) + end) + { `V = (Zfact U)` }. +Proof. +Symmetry. Rewrite Test1. Apply axiom4. +Unfold Zwf. Unfold Zpred. Omega. +Unfold Zpred. Omega. +Rewrite Post3. +Unfold Zpred. Replace `U0+(-1)` with `U0-1`. Apply axiom5. +Omega. +Omega. +Save. + +(****************************************************************************) + +(* program (197) page 945 (L_4 subset of Pascal) *) + +(* +procedure P(X:Z; procedure Q(Z:Z)); + procedure L(X:Z); begin Q(X-1) end; + begin if X>0 then P(X-1,L) else Q(X) end; + +procedure M(N:Z); + procedure R(X:Z); begin writeln(X) (* => RES := !X *) end; + begin P(N,R) end. +*) diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v new file mode 100644 index 00000000..dcfcec87 --- /dev/null +++ b/contrib/correctness/examples/exp.v @@ -0,0 +1,204 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(*i $Id: exp.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ i*) + +(* Efficient computation of X^n using + * + * X^(2n) = (X^n) ^ 2 + * X^(2n+1) = X . (X^n) ^ 2 + * + * Proofs of both fonctional and imperative programs. + *) + +Require Even. +Require Div2. +Require Correctness. +Require ArithRing. +Require ZArithRing. + +(* The specification uses the traditional definition of X^n *) + +Fixpoint power [x,n:nat] : nat := + Cases n of + O => (S O) + | (S n') => (mult x (power x n')) + end. + +Definition square := [n:nat](mult n n). + + +(* Three lemmas are necessary to establish the forthcoming proof obligations *) + +(* n = 2*(n/2) => (x^(n/2))^2 = x^n *) + +Lemma exp_div2_0 : (x,n:nat) + n=(double (div2 n)) + -> (square (power x (div2 n)))=(power x n). +Proof. +Unfold square. +Intros x n. Pattern n. Apply ind_0_1_SS. +Auto. + +Intro. (Absurd (1)=(double (0)); Auto). + +Intros. Simpl. +Cut n0=(double (div2 n0)). +Intro. Rewrite <- (H H1). +Ring. + +Simpl in H0. +Unfold double in H0. +Simpl in H0. +Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0. +(Injection H0; Auto). +Save. + +(* n = 2*(n/2)+1 => x*(x^(n/2))^2 = x^n *) + +Lemma exp_div2_1 : (x,n:nat) + n=(S (double (div2 n))) + -> (mult x (square (power x (div2 n))))=(power x n). +Proof. +Unfold square. +Intros x n. Pattern n. Apply ind_0_1_SS. + +Intro. (Absurd (0)=(S (double (0))); Auto). + +Auto. + +Intros. Simpl. +Cut n0=(S (double (div2 n0))). +Intro. Rewrite <- (H H1). +Ring. + +Simpl in H0. +Unfold double in H0. +Simpl in H0. +Rewrite <- (plus_n_Sm (div2 n0) (div2 n0)) in H0. +(Injection H0; Auto). +Save. + +(* x^(2*n) = (x^2)^n *) + +Lemma power_2n : (x,n:nat)(power x (double n))=(power (square x) n). +Proof. +Unfold double. Unfold square. +Induction n. +Auto. + +Intros. +Simpl. +Rewrite <- H. +Rewrite <- (plus_n_Sm n0 n0). +Simpl. +Auto with arith. +Save. + +Hints Resolve exp_div2_0 exp_div2_1. + + +(* Functional version. + * + * Here we give the functional program as an incomplete CIC term, + * using the tactic Refine. + * + * On this example, it really behaves as the tactic Program. + *) + +(* +Lemma f_exp : (x,n:nat) { y:nat | y=(power x n) }. +Proof. +Refine [x:nat] + (well_founded_induction nat lt lt_wf + [n:nat]{y:nat | y=(power x n) } + [n:nat] + [f:(p:nat)(lt p n)->{y:nat | y=(power x p) }] + Cases (zerop n) of + (left _) => (exist ? ? (S O) ?) + | (right _) => + let (y,H) = (f (div2 n) ?) in + Cases (even_odd_dec n) of + (left _) => (exist ? ? (mult y y) ?) + | (right _) => (exist ? ? (mult x (mult y y)) ?) + end + end). +Proof. +Rewrite a. Auto. +Exact (lt_div2 n a). +Change (square y)=(power x n). Rewrite H. Auto with arith. +Change (mult x (square y))=(power x n). Rewrite H. Auto with arith. +Save. +*) + +(* Imperative version. *) + +Definition even_odd_bool := [x:nat](bool_of_sumbool ? ? (even_odd_dec x)). + +Correctness i_exp + fun (x:nat)(n:nat) -> + let y = ref (S O) in + let m = ref x in + let e = ref n in + begin + while (notzerop_bool !e) do + { invariant (power x n)=(mult y (power m e)) as Inv + variant e for lt } + (if not (even_odd_bool !e) then y := (mult !y !m)) + { (power x n) = (mult y (power m (double (div2 e)))) as Q }; + m := (square !m); + e := (div2 !e) + done; + !y + end + { result=(power x n) } +. +Proof. +Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith. + +Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity. + +Split. +Exact (lt_div2 e0 Test2). + +Rewrite Q. Unfold double. Unfold square. +Simpl. +Change (mult y1 (power m0 (double (div2 e0)))) + = (mult y1 (power (square m0) (div2 e0))). +Rewrite (power_2n m0 (div2 e0)). Reflexivity. + +Auto with arith. + +Decompose [and] Inv. +Rewrite H. Rewrite H0. +Auto with arith. +Save. + + +(* Recursive version. *) + +Correctness r_exp + let rec exp (x:nat) (n:nat) : nat { variant n for lt} = + (if (zerop_bool n) then + (S O) + else + let y = (exp x (div2 n)) in + if (even_odd_bool n) then + (mult y y) + else + (mult x (mult y y)) + ) { result=(power x n) } +. +Proof. +Rewrite Test2. Auto. +Exact (lt_div2 n0 Test2). +Change (square y)=(power x0 n0). Rewrite Post7. Auto with arith. +Change (mult x0 (square y))=(power x0 n0). Rewrite Post7. Auto with arith. +Save. diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v new file mode 100644 index 00000000..accd60c2 --- /dev/null +++ b/contrib/correctness/examples/exp_int.v @@ -0,0 +1,218 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: exp_int.v,v 1.4 2001/04/11 07:56:19 filliatr Exp $ *) + +(* Efficient computation of X^n using + * + * X^(2n) = (X^n) ^ 2 + * X^(2n+1) = X . (X^n) ^ 2 + * + * Proofs of both fonctional and imperative programs. + *) + +Require Zpower. +Require Zcomplements. + +Require Correctness. +Require ZArithRing. +Require Omega. + +Definition Zdouble := [n:Z]`2*n`. + +Definition Zsquare := [n:Z](Zmult n n). + +(* Some auxiliary lemmas about Zdiv2 are necessary *) + +Lemma Zdiv2_ge_0 : (x:Z) `x >= 0` -> `(Zdiv2 x) >= 0`. +Proof. +Destruct x; Auto with zarith. +Destruct p; Auto with zarith. +Simpl. Omega. +Intros. (Absurd `(NEG p) >= 0`; Red; Auto with zarith). +Save. + +Lemma Zdiv2_lt : (x:Z) `x > 0` -> `(Zdiv2 x) < x`. +Proof. +Destruct x. +Intro. Absurd `0 > 0`; [ Omega | Assumption ]. +Destruct p; Auto with zarith. + +Simpl. +Intro p0. +Replace (POS (xI p0)) with `2*(POS p0)+1`. +Omega. +Simpl. Auto with zarith. + +Intro p0. +Simpl. +Replace (POS (xO p0)) with `2*(POS p0)`. +Omega. +Simpl. Auto with zarith. + +Simpl. Omega. + +Intros. +Absurd `(NEG p) > 0`; Red; Auto with zarith. +Elim p; Auto with zarith. +Omega. +Save. + +(* A property of Zpower: x^(2*n) = (x^2)^n *) + +Lemma Zpower_2n : + (x,n:Z)`n >= 0` -> (Zpower x (Zdouble n))=(Zpower (Zsquare x) n). +Proof. +Unfold Zdouble. +Intros x n Hn. +Replace `2*n` with `n+n`. +Rewrite Zpower_exp. +Pattern n. +Apply natlike_ind. + +Simpl. Auto with zarith. + +Intros. +Unfold Zs. +Rewrite Zpower_exp. +Rewrite Zpower_exp. +Replace (Zpower x `1`) with x. +Replace (Zpower (Zsquare x) `1`) with (Zsquare x). +Rewrite <- H0. +Unfold Zsquare. +Ring. + +Unfold Zpower; Unfold Zpower_pos; Simpl. Omega. + +Unfold Zpower; Unfold Zpower_pos; Simpl. Omega. + +Omega. +Omega. +Omega. +Omega. +Omega. +Assumption. +Assumption. +Omega. +Save. + + +(* The program *) + +Correctness i_exp + fun (x:Z)(n:Z) -> + { `n >= 0` } + (let y = ref 1 in + let m = ref x in + let e = ref n in + begin + while !e > 0 do + { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv + variant e } + (if not (Zeven_odd_bool !e) then y := (Zmult !y !m)) + { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q }; + m := (Zsquare !m); + e := (Zdiv2 !e) + done; + !y + end) + { result=(Zpower x n) } +. +Proof. +(* Zodd *) +Decompose [and] Inv. +Rewrite (Zodd_div2 e0 H0 Test1) in H. Rewrite H. +Rewrite Zpower_exp. +Unfold Zdouble. +Replace (Zpower m0 `1`) with m0. +Ring. +Unfold Zpower; Unfold Zpower_pos; Simpl; Ring. +Generalize (Zdiv2_ge_0 e0); Omega. +Omega. +(* Zeven *) +Decompose [and] Inv. +Rewrite (Zeven_div2 e0 Test1) in H. Rewrite H. +Auto with zarith. +Split. +(* Zwf *) +Unfold Zwf. +Repeat Split. +Generalize (Zdiv2_ge_0 e0); Omega. +Omega. +Exact (Zdiv2_lt e0 Test2). +(* invariant *) +Split. +Rewrite Q. Unfold Zdouble. Unfold Zsquare. +Rewrite (Zpower_2n). +Trivial. +Generalize (Zdiv2_ge_0 e0); Omega. +Generalize (Zdiv2_ge_0 e0); Omega. +Split; [ Ring | Assumption ]. +(* exit fo loop *) +Decompose [and] Inv. +Cut `e0 = 0`. Intro. +Rewrite H1. Rewrite H. +Simpl; Ring. +Omega. +Save. + + +(* Recursive version. *) + +Correctness r_exp + let rec exp (x:Z) (n:Z) : Z { variant n } = + { `n >= 0` } + (if n = 0 then + 1 + else + let y = (exp x (Zdiv2 n)) in + (if (Zeven_odd_bool n) then + (Zmult y y) + else + (Zmult x (Zmult y y))) { result=(Zpower x n) as Q } + ) + { result=(Zpower x n) } +. +Proof. +Rewrite Test2. Auto with zarith. +(* w.f. *) +Unfold Zwf. +Repeat Split. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +Generalize (Zdiv2_lt n0) ; Omega. +(* rec. call *) +Generalize (Zdiv2_ge_0 n0) ; Omega. +(* invariant: case even *) +Generalize (Zeven_div2 n0 Test1). +Intro Heq. Rewrite Heq. +Rewrite Post4. +Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`. +Rewrite Zpower_exp. +Auto with zarith. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +(* invariant: cas odd *) +Generalize (Zodd_div2 n0 Pre1 Test1). +Intro Heq. Rewrite Heq. +Rewrite Post4. +Rewrite Zpower_exp. +Replace `2*(Zdiv2 n0)` with `(Zdiv2 n0)+(Zdiv2 n0)`. +Rewrite Zpower_exp. +Replace `(Zpower x0 1)` with x0. +Ring. +Unfold Zpower; Unfold Zpower_pos; Simpl. Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +Generalize (Zdiv2_ge_0 n0) ; Omega. +Omega. +Save. diff --git a/contrib/correctness/examples/extract.v b/contrib/correctness/examples/extract.v new file mode 100644 index 00000000..e225ba18 --- /dev/null +++ b/contrib/correctness/examples/extract.v @@ -0,0 +1,43 @@ + +(* Tests d'extraction *) + +Require ProgramsExtraction. +Save State Ici "test extraction". + +(* exp *) + +Require exp. +Write Caml File "exp" [ i_exp r_exp ]. + +(* exp_int *) + +Restore State Ici. +Require exp_int. +Write Caml File "exp_int" [ i_exp r_exp ]. + +(* fact *) + +Restore State Ici. +Require fact. +Initialize x with (S (S (S O))). +Initialize y with O. +Write Caml File "fact" [ factorielle ]. + +(* fact_int *) + +Restore State Ici. +Require fact_int. +Initialize x with `3`. +Initialize y with `0`. +Write Caml File "fact_int" [ factorielle ]. + +(* Handbook *) + +Restore State Ici. +Require Handbook. +Initialize X with `3`. +Initialize Y with `3`. +Initialize Z with `3`. +Initialize N with `3`. +Initialize S with `3`. +Write Caml File "Handbook" [ pgm178 pgm186 pgm196 ]. diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v new file mode 100644 index 00000000..e480c806 --- /dev/null +++ b/contrib/correctness/examples/fact.v @@ -0,0 +1,69 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: fact.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) + +(* Proof of an imperative program computing the factorial (over type nat) *) + +Require Correctness. +Require Omega. +Require Arith. + +Fixpoint fact [n:nat] : nat := + Cases n of + O => (S O) + | (S p) => (mult n (fact p)) + end. + +(* (x * y) * (x-1)! = y * x! *) + +Lemma fact_rec : (x,y:nat)(lt O x) -> + (mult (mult x y) (fact (pred x))) = (mult y (fact x)). +Proof. +Intros x y H. +Generalize (mult_sym x y). Intro H1. Rewrite H1. +Generalize (mult_assoc_r y x (fact (pred x))). Intro H2. Rewrite H2. +Apply (f_equal nat nat [x:nat](mult y x)). +Generalize H. Elim x; Auto with arith. +Save. + + +(* we declare two variables x and y *) + +Global Variable x : nat ref. +Global Variable y : nat ref. + +(* we give the annotated program *) + +Correctness factorielle + begin + y := (S O); + while (notzerop_bool !x) do + { invariant (mult y (fact x)) = (fact x@0) as I + variant x for lt } + y := (mult !x !y); + x := (pred !x) + done + end + { y = (fact x@0) }. +Proof. +Split. +(* decreasing of the variant *) +Omega. +(* preservation of the invariant *) +Rewrite <- I. Exact (fact_rec x0 y1 Test1). +(* entrance of loop *) +Auto with arith. +(* exit of loop *) +Elim I. Intros H1 H2. +Rewrite H2 in H1. +Rewrite <- H1. +Auto with arith. +Save. diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v new file mode 100644 index 00000000..cb2b0460 --- /dev/null +++ b/contrib/correctness/examples/fact_int.v @@ -0,0 +1,195 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: fact_int.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) + +(* Proof of an imperative program computing the factorial (over type Z) *) + +Require Correctness. +Require Omega. +Require ZArithRing. + +(* We define the factorial as a relation... *) + +Inductive fact : Z -> Z -> Prop := + fact_0 : (fact `0` `1`) + | fact_S : (z,f:Z) (fact z f) -> (fact (Zs z) (Zmult (Zs z) f)). + +(* ...and then we prove that it contains a function *) + +Lemma fact_function : (z:Z) `0 <= z` -> (EX f:Z | (fact z f)). +Proof. +Intros. +Apply natlike_ind with P:=[z:Z](EX f:Z | (fact z f)). +Split with `1`. +Exact fact_0. + +Intros. +Elim H1. +Intros. +Split with `(Zs x)*x0`. +Exact (fact_S x x0 H2). + +Assumption. +Save. + +(* This lemma should belong to the ZArith library *) + +Lemma Z_mult_1 : (x,y:Z)`x>=1`->`y>=1`->`x*y>=1`. +Proof. +Intros. +Generalize H. +Apply natlike_ind with P:=[x:Z]`x >= 1`->`x*y >= 1`. +Omega. + +Intros. +Simpl. +Elim (Z_le_lt_eq_dec `0` x0 H1). +Simpl. +Unfold Zs. +Replace `(x0+1)*y` with `x0*y+y`. +Generalize H2. +Generalize `x0*y`. +Intro. +Intros. +Omega. + +Ring. + +Intros. +Rewrite <- b. +Omega. + +Omega. +Save. + +(* (fact x f) implies x>=0 and f>=1 *) + +Lemma fact_pos : (x,f:Z)(fact x f)-> `x>=0` /\ `f>=1`. +Proof. +Intros. +(Elim H; Auto). +Omega. + +Intros. +(Split; Try Omega). +(Apply Z_mult_1; Try Omega). +Save. + +(* (fact 0 x) implies x=1 *) + +Lemma fact_0_1 : (x:Z)(fact `0` x) -> `x=1`. +Proof. +Intros. +Inversion H. +Reflexivity. + +Elim (fact_pos z f H1). +Intros. +(Absurd `z >= 0`; Omega). +Save. + + +(* We define the loop invariant : y * x! = x0! *) + +Inductive invariant [y,x,x0:Z] : Prop := + c_inv : (f,f0:Z)(fact x f)->(fact x0 f0)->(Zmult y f)=f0 + -> (invariant y x x0). + +(* The following lemma is used to prove the preservation of the invariant *) + +Lemma fact_rec : (x0,x,y:Z)`0 < x` -> + (invariant y x x0) + -> (invariant `x*y` (Zpred x) x0). +Proof. +Intros x0 x y H H0. +Elim H0. +Intros. +Generalize H H0 H3. +Elim H1. +Intros. +Absurd `0 < 0`; Omega. + +Intros. +Apply c_inv with f:=f1 f0:=f0. +Cut `z+1+-1 = z`. Intro eq_z. Rewrite <- eq_z in H4. +Assumption. + +Omega. + +Assumption. + +Rewrite (Zmult_sym (Zs z) y). +Rewrite (Zmult_assoc_r y (Zs z) f1). +Auto. +Save. + + +(* This one is used to prove the proof obligation at the exit of the loop *) + +Lemma invariant_0 : (x,y:Z)(invariant y `0` x)->(fact x y). +Proof. +Intros. +Elim H. +Intros. +Generalize (fact_0_1 f H0). +Intro. +Rewrite H3 in H2. +Simpl in H2. +Replace y with `y*1`. +Rewrite H2. +Assumption. + +Omega. +Save. + + +(* At last we come to the proof itself *************************************) + +(* we declare two variable x and y *) + +Global Variable x : Z ref. +Global Variable y : Z ref. + +(* and we give the annotated program *) + +Correctness factorielle + { `0 <= x` } + begin + y := 1; + while !x <> 0 do + { invariant `0 <= x` /\ (invariant y x x@0) as Inv + variant x for (Zwf ZERO) } + y := (Zmult !x !y); + x := (Zpred !x) + done + end + { (fact x@0 y) }. +Proof. +Split. +(* decreasing *) +Unfold Zwf. Unfold Zpred. Omega. +(* preservation of the invariant *) +Split. + Unfold Zpred; Omega. + Cut `0 < x0`. Intro Hx0. + Decompose [and] Inv. + Exact (fact_rec x x0 y1 Hx0 H0). + Omega. +(* entrance of the loop *) +Split; Auto. +Elim (fact_function x Pre1). Intros. +Apply c_inv with f:=x0 f0:=x0; Auto. +Omega. +(* exit of the loop *) +Decompose [and] Inv. +Rewrite H0 in H2. +Exact (invariant_0 x y1 H2). +Save. diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli new file mode 100644 index 00000000..1cc7164e --- /dev/null +++ b/contrib/correctness/past.mli @@ -0,0 +1,97 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: past.mli,v 1.7.6.1 2004/07/16 19:30:00 herbelin Exp $ *) + +(*s Abstract syntax of imperative programs. *) + +open Names +open Ptype +open Topconstr + +type termination = + | RecArg of int + | Wf of constr_expr * constr_expr + +type variable = identifier + +type pattern = + | PatVar of identifier + | PatConstruct of identifier * ((kernel_name * int) * int) + | PatAlias of pattern * identifier + | PatPair of pattern * pattern + | PatApp of pattern list + +type epattern = + | ExnConstant of identifier + | ExnBind of identifier * identifier + +type ('a, 'b) block_st = + | Label of string + | Assert of 'b Ptype.assertion + | Statement of 'a + +type ('a, 'b) block = ('a, 'b) block_st list + +type ('a, 'b) t = { + desc : ('a, 'b) t_desc; + pre : 'b Ptype.precondition list; + post : 'b Ptype.postcondition option; + loc : Util.loc; + info : 'a +} + +and ('a, 'b) t_desc = + | Variable of variable + | Acc of variable + | Aff of variable * ('a, 'b) t + | TabAcc of bool * variable * ('a, 'b) t + | TabAff of bool * variable * ('a, 'b) t * ('a, 'b) t + | Seq of (('a, 'b) t, 'b) block + | While of ('a, 'b) t * 'b Ptype.assertion option * ('b * 'b) * + (('a, 'b) t, 'b) block + | If of ('a, 'b) t * ('a, 'b) t * ('a, 'b) t + | Lam of 'b Ptype.ml_type_v Ptype.binder list * ('a, 'b) t + | Apply of ('a, 'b) t * ('a, 'b) arg list + | SApp of ('a, 'b) t_desc list * ('a, 'b) t list + | LetRef of variable * ('a, 'b) t * ('a, 'b) t + | Let of variable * ('a, 'b) t * ('a, 'b) t + | LetRec of variable * 'b Ptype.ml_type_v Ptype.binder list * + 'b Ptype.ml_type_v * ('b * 'b) * ('a, 'b) t + | PPoint of string * ('a, 'b) t_desc + | Expression of Term.constr + | Debug of string * ('a, 'b) t + +and ('a, 'b) arg = + | Term of ('a, 'b) t + | Refarg of variable + | Type of 'b Ptype.ml_type_v + +type program = (unit, Topconstr.constr_expr) t + +(*s Intermediate type for CC terms. *) + +type cc_type = Term.constr + +type cc_bind_type = + | CC_typed_binder of cc_type + | CC_untyped_binder + +type cc_binder = variable * cc_bind_type + +type cc_term = + | CC_var of variable + | CC_letin of bool * cc_type * cc_binder list * cc_term * cc_term + | CC_lam of cc_binder list * cc_term + | CC_app of cc_term * cc_term list + | CC_tuple of bool * cc_type list * cc_term list + | CC_case of cc_type * cc_term * cc_term list + | CC_expr of Term.constr + | CC_hole of cc_type diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml new file mode 100644 index 00000000..e87ba70c --- /dev/null +++ b/contrib/correctness/pcic.ml @@ -0,0 +1,231 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pcic.ml,v 1.23.2.1 2004/07/16 19:30:00 herbelin Exp $ *) + +open Util +open Names +open Nameops +open Libnames +open Term +open Termops +open Nametab +open Declarations +open Indtypes +open Sign +open Rawterm +open Typeops +open Entries +open Topconstr + +open Pmisc +open Past + + +(* Here we translate intermediates terms (cc_term) into CCI terms (constr) *) + +let make_hole c = mkCast (isevar, c) + +(* Tuples are defined in file Tuples.v + * and their constructors are called Build_tuple_n or exists_n, + * wether they are dependant (last element only) or not. + * If necessary, tuples are generated ``on the fly''. *) + +let tuple_exists id = + try let _ = Nametab.locate (make_short_qualid id) in true + with Not_found -> false + +let ast_set = CSort (dummy_loc,RProp Pos) + +let tuple_n n = + let id = make_ident "tuple_" (Some n) in + let l1n = Util.interval 1 n in + let params = + List.map (fun i -> + (LocalRawAssum ([dummy_loc,Name (make_ident "T" (Some i))], ast_set))) + l1n in + let fields = + List.map + (fun i -> + let id = make_ident ("proj_" ^ string_of_int n ^ "_") (Some i) in + let id' = make_ident "T" (Some i) in + (false, Vernacexpr.AssumExpr ((dummy_loc,Name id), mkIdentC id'))) + l1n + in + let cons = make_ident "Build_tuple_" (Some n) in + Record.definition_structure + ((false, (dummy_loc,id)), params, fields, cons, mk_Set) + +(*s [(sig_n n)] generates the inductive + \begin{verbatim} + Inductive sig_n [T1,...,Tn:Set; P:T1->...->Tn->Prop] : Set := + exist_n : (x1:T1)...(xn:Tn)(P x1 ... xn) -> (sig_n T1 ... Tn P). + \end{verbatim} *) + +let sig_n n = + let id = make_ident "sig_" (Some n) in + let l1n = Util.interval 1 n in + let lT = List.map (fun i -> make_ident "T" (Some i)) l1n in + let lx = List.map (fun i -> make_ident "x" (Some i)) l1n in + let idp = make_ident "P" None in + let params = + let typ = List.fold_right (fun _ c -> mkArrow (mkRel n) c) lT mkProp in + (idp, LocalAssum typ) :: + (List.rev_map (fun id -> (id, LocalAssum mkSet)) lT) + in + let lc = + let app_sig = mkApp(mkRel (2*n+3), + Array.init (n+1) (fun i -> mkRel (2*n+2-i))) in + let app_p = mkApp(mkRel (n+1), + Array.init n (fun i -> mkRel (n-i))) in + let c = mkArrow app_p app_sig in + List.fold_right (fun id c -> mkProd (Name id, mkRel (n+1), c)) lx c + in + let cname = make_ident "exist_" (Some n) in + Declare.declare_mind + { mind_entry_finite = true; + mind_entry_inds = + [ { mind_entry_params = params; + mind_entry_typename = id; + mind_entry_arity = mkSet; + mind_entry_consnames = [ cname ]; + mind_entry_lc = [ lc ] } ] } + +(*s On the fly generation of needed (possibly dependent) tuples. *) + +let check_product_n n = + if n > 2 then + let s = Printf.sprintf "tuple_%d" n in + if not (tuple_exists (id_of_string s)) then tuple_n n + +let check_dep_product_n n = + if n > 1 then + let s = Printf.sprintf "sig_%d" n in + if not (tuple_exists (id_of_string s)) then ignore (sig_n n) + +(*s Constructors for the tuples. *) + +let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "prod",0),1) +let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "sig",0),1) + +let tuple_ref dep n = + if n = 2 & not dep then + pair + else + let n = n - (if dep then 1 else 0) in + if dep then + if n = 1 then + exist + else begin + let id = make_ident "exist_" (Some n) in + if not (tuple_exists id) then ignore (sig_n n); + Nametab.locate (make_short_qualid id) + end + else begin + let id = make_ident "Build_tuple_" (Some n) in + if not (tuple_exists id) then tuple_n n; + Nametab.locate (make_short_qualid id) + end + +(* Binders. *) + +let trad_binder avoid nenv id = function + | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id)) + | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty + +let rec push_vars avoid nenv = function + | [] -> ([],avoid,nenv) + | (id,b) :: bl -> + let b' = trad_binder avoid nenv id b in + let bl',avoid',nenv' = + push_vars (id :: avoid) (add_name (Name id) nenv) bl + in + ((id,b') :: bl', avoid', nenv') + +let rec raw_lambda bl v = match bl with + | [] -> + v + | (id,ty) :: bl' -> + RLambda (dummy_loc, Name id, ty, raw_lambda bl' v) + +(* The translation itself is quite easy. + letin are translated into Cases constructions *) + +let rawconstr_of_prog p = + let rec trad avoid nenv = function + | CC_var id -> + RVar (dummy_loc, id) + + (*i optimisation : let x = <constr> in e2 => e2[x<-constr] + | CC_letin (_,_,[id,_],CC_expr c,e2) -> + real_subst_in_constr [id,c] (trad e2) + | CC_letin (_,_,([_] as b),CC_expr e1,e2) -> + let (b',avoid',nenv') = push_vars avoid nenv b in + let c1 = Detyping.detype avoid nenv e1 + and c2 = trad avoid' nenv' e2 in + let id = Name (fst (List.hd b')) in + RLetIn (dummy_loc, id, c1, c2) + i*) + + | CC_letin (_,_,([_] as b),e1,e2) -> + let (b',avoid',nenv') = push_vars avoid nenv b in + let c1 = trad avoid nenv e1 + and c2 = trad avoid' nenv' e2 in + RApp (dummy_loc, raw_lambda b' c2, [c1]) + + | CC_letin (dep,ty,bl,e1,e2) -> + let (bl',avoid',nenv') = push_vars avoid nenv bl in + let c1 = trad avoid nenv e1 + and c2 = trad avoid' nenv' e2 in + ROrderedCase (dummy_loc, LetStyle, None, c1, [| raw_lambda bl' c2 |], ref None) + + | CC_lam (bl,e) -> + let bl',avoid',nenv' = push_vars avoid nenv bl in + let c = trad avoid' nenv' e in + raw_lambda bl' c + + | CC_app (f,args) -> + let c = trad avoid nenv f + and cargs = List.map (trad avoid nenv) args in + RApp (dummy_loc, c, cargs) + + | CC_tuple (_,_,[e]) -> + trad avoid nenv e + + | CC_tuple (false,_,[e1;e2]) -> + let c1 = trad avoid nenv e1 + and c2 = trad avoid nenv e2 in + RApp (dummy_loc, RRef (dummy_loc,pair), + [RHole (dummy_loc,ImplicitArg (pair,1)); + RHole (dummy_loc,ImplicitArg (pair,2));c1;c2]) + + | CC_tuple (dep,tyl,l) -> + let n = List.length l in + let cl = List.map (trad avoid nenv) l in + let tuple = tuple_ref dep n in + let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in + let args = tyl @ cl in + RApp (dummy_loc, RRef (dummy_loc, tuple), args) + + | CC_case (ty,b,el) -> + let c = trad avoid nenv b in + let cl = List.map (trad avoid nenv) el in + let ty = Detyping.detype (false,Global.env()) avoid nenv ty in + ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None) + + | CC_expr c -> + Detyping.detype (false,Global.env()) avoid nenv c + + | CC_hole c -> + RCast (dummy_loc, RHole (dummy_loc, QuestionMark), + Detyping.detype (false,Global.env()) avoid nenv c) + + in + trad [] empty_names_context p diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli new file mode 100644 index 00000000..89731472 --- /dev/null +++ b/contrib/correctness/pcic.mli @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(*i $Id: pcic.mli,v 1.3.16.1 2004/07/16 19:30:00 herbelin Exp $ i*) + +open Past +open Rawterm + +(* On-the-fly generation of needed (possibly dependent) tuples. *) + +val check_product_n : int -> unit +val check_dep_product_n : int -> unit + +(* transforms intermediate functional programs into (raw) CIC terms *) + +val rawconstr_of_prog : cc_term -> rawconstr + diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml new file mode 100644 index 00000000..cc15c8f3 --- /dev/null +++ b/contrib/correctness/pcicenv.ml @@ -0,0 +1,118 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pcicenv.ml,v 1.5.14.1 2004/07/16 19:30:00 herbelin Exp $ *) + +open Names +open Term +open Sign + +open Pmisc +open Putil +open Ptype +open Past + +(* on redéfinit add_sign pour éviter de construire des environnements + * avec des doublons (qui font planter la résolution des implicites !) *) + +(* VERY UGLY!! find some work around *) +let modify_sign id t s = + fold_named_context + (fun ((x,b,ty) as d) sign -> + if x=id then add_named_decl (x,b,t) sign else add_named_decl d sign) + s ~init:empty_named_context + +let add_sign (id,t) s = + try + let _ = lookup_named id s in + modify_sign id t s + with Not_found -> + add_named_decl (id,None,t) s + +let cast_set c = mkCast (c, mkSet) + +let set = mkCast (mkSet, mkType Univ.prop_univ) + +(* [cci_sign_of env] construit un environnement pour CIC ne comprenant que + * les objets fonctionnels de l'environnement de programes [env] + *) + +let cci_sign_of ren env = + Penv.fold_all + (fun (id,v) sign -> + match v with + | Penv.TypeV (Ref _ | Array _) -> sign + | Penv.TypeV v -> + let ty = Pmonad.trad_ml_type_v ren env v in + add_sign (id,cast_set ty) sign + | Penv.Set -> add_sign (id,set) sign) + env (Global.named_context ()) + +(* [sign_meta ren env fadd ini] + * construit un environnement pour CIC qui prend en compte les variables + * de programme. + * pour cela, cette fonction parcours tout l'envrionnement (global puis + * local [env]) et pour chaque déclaration, ajoute ce qu'il faut avec la + * fonction [fadd] s'il s'agit d'un mutable et directement sinon, + * en partant de [ini]. + *) + +let sign_meta ren env fast ini = + Penv.fold_all + (fun (id,v) sign -> + match v with + | Penv.TypeV (Ref _ | Array _ as v) -> + let ty = Pmonad.trad_imp_type ren env v in + fast sign id ty + | Penv.TypeV v -> + let ty = Pmonad.trad_ml_type_v ren env v in + add_sign (id,cast_set ty) sign + | Penv.Set -> add_sign (id,set) sign) + env ini + +let add_sign_d dates (id,c) sign = + let sign = + List.fold_left (fun sign d -> add_sign (at_id id d,c) sign) sign dates + in + add_sign (id,c) sign + +let sign_of add ren env = + sign_meta ren env + (fun sign id c -> let c = cast_set c in add (id,c) sign) + (Global.named_context ()) + +let result_of sign = function + None -> sign + | Some (id,c) -> add_sign (id, cast_set c) sign + +let before_after_result_sign_of res ren env = + let dates = "" :: Prename.all_dates ren in + result_of (sign_of (add_sign_d dates) ren env) res + +let before_after_sign_of ren = + let dates = "" :: Prename.all_dates ren in + sign_of (add_sign_d dates) ren + +let before_sign_of ren = + let dates = Prename.all_dates ren in + sign_of (add_sign_d dates) ren + +let now_sign_of = + sign_of (add_sign_d []) + + +(* environnement aprčs traduction *) + +let trad_sign_of ren = + sign_of + (fun (id,c) sign -> add_sign (Prename.current_var ren id,c) sign) + ren + + diff --git a/contrib/correctness/pcicenv.mli b/contrib/correctness/pcicenv.mli new file mode 100644 index 00000000..fc4fa0b9 --- /dev/null +++ b/contrib/correctness/pcicenv.mli @@ -0,0 +1,38 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pcicenv.mli,v 1.2.16.1 2004/07/16 19:30:00 herbelin Exp $ *) + +open Penv +open Names +open Term +open Sign + +(* Translation of local programs environments into Coq signatures. + * It is mainly used to type the pre/post conditions in the good + * environment *) + +(* cci_sign_of: uniquement les objets purement fonctionnels de l'env. *) +val cci_sign_of : Prename.t -> local_env -> named_context + +(* env. Coq avec seulement les variables X de l'env. *) +val now_sign_of : Prename.t -> local_env -> named_context + +(* + les variables X@d pour toutes les dates de l'env. *) +val before_sign_of : Prename.t -> local_env -> named_context + +(* + les variables `avant' X@ *) +val before_after_sign_of : Prename.t -> local_env -> named_context +val before_after_result_sign_of : ((identifier * constr) option) + -> Prename.t -> local_env -> named_context + +(* env. des programmes traduits, avec les variables rennomées *) +val trad_sign_of : Prename.t -> local_env -> named_context + diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml new file mode 100644 index 00000000..302db871 --- /dev/null +++ b/contrib/correctness/pdb.ml @@ -0,0 +1,165 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pdb.ml,v 1.8.2.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Names +open Term +open Termops +open Nametab +open Constrintern + +open Ptype +open Past +open Penv + +let cci_global id = + try + global_reference id + with + _ -> raise Not_found + +let lookup_var ids locop id = + if List.mem id ids then + None + else begin + try Some (cci_global id) + with Not_found -> Perror.unbound_variable id locop + end + +let check_ref idl loc id = + if (not (List.mem id idl)) & (not (Penv.is_global id)) then + Perror.unbound_reference id loc + +(* db types : only check the references for the moment *) + +let rec check_type_v refs = function + | Ref v -> + check_type_v refs v + | Array (c,v) -> + check_type_v refs v + | Arrow (bl,c) -> + check_binder refs c bl + | TypePure _ -> + () + +and check_type_c refs ((_,v),e,_,_) = + check_type_v refs v; + List.iter (check_ref refs None) (Peffect.get_reads e); + List.iter (check_ref refs None) (Peffect.get_writes e) + (* TODO: check_condition on p and q *) + +and check_binder refs c = function + | [] -> + check_type_c refs c + | (id, BindType (Ref _ | Array _ as v)) :: bl -> + check_type_v refs v; + check_binder (id :: refs) c bl + | (_, BindType v) :: bl -> + check_type_v refs v; + check_binder refs c bl + | _ :: bl -> + check_binder refs c bl + +(* db binders *) + +let rec db_binders ((tids,pids,refs) as idl) = function + | [] -> + idl, [] + | (id, BindType (Ref _ | Array _ as v)) as b :: rem -> + check_type_v refs v; + let idl',rem' = db_binders (tids,pids,id::refs) rem in + idl', b :: rem' + | (id, BindType v) as b :: rem -> + check_type_v refs v; + let idl',rem' = db_binders (tids,id::pids,refs) rem in + idl', b :: rem' + | ((id, BindSet) as t) :: rem -> + let idl',rem' = db_binders (id::tids,pids,refs) rem in + idl', t :: rem' + | a :: rem -> + let idl',rem' = db_binders idl rem in idl', a :: rem' + + +(* db programs *) + +let db_prog e = + (* tids = type identifiers, ids = variables, refs = references and arrays *) + let rec db_desc ((tids,ids,refs) as idl) = function + | (Variable x) as t -> + (match lookup_var ids (Some e.loc) x with + None -> t + | Some c -> Expression c) + | (Acc x) as t -> + check_ref refs (Some e.loc) x; + t + | Aff (x,e1) -> + check_ref refs (Some e.loc) x; + Aff (x, db idl e1) + | TabAcc (b,x,e1) -> + check_ref refs (Some e.loc) x; + TabAcc(b,x,db idl e1) + | TabAff (b,x,e1,e2) -> + check_ref refs (Some e.loc) x; + TabAff (b,x, db idl e1, db idl e2) + | Seq bl -> + Seq (List.map (function + Statement p -> Statement (db idl p) + | x -> x) bl) + | If (e1,e2,e3) -> + If (db idl e1, db idl e2, db idl e3) + | While (b,inv,var,bl) -> + let bl' = List.map (function + Statement p -> Statement (db idl p) + | x -> x) bl in + While (db idl b, inv, var, bl') + + | Lam (bl,e) -> + let idl',bl' = db_binders idl bl in Lam(bl', db idl' e) + | Apply (e1,l) -> + Apply (db idl e1, List.map (db_arg idl) l) + | SApp (dl,l) -> + SApp (dl, List.map (db idl) l) + | LetRef (x,e1,e2) -> + LetRef (x, db idl e1, db (tids,ids,x::refs) e2) + | Let (x,e1,e2) -> + Let (x, db idl e1, db (tids,x::ids,refs) e2) + + | LetRec (f,bl,v,var,e) -> + let (tids',ids',refs'),bl' = db_binders idl bl in + check_type_v refs' v; + LetRec (f, bl, v, var, db (tids',f::ids',refs') e) + + | Debug (s,e1) -> + Debug (s, db idl e1) + + | Expression _ as x -> x + | PPoint (s,d) -> PPoint (s, db_desc idl d) + + and db_arg ((tids,_,refs) as idl) = function + | Term ({ desc = Variable id } as t) -> + if List.mem id refs then Refarg id else Term (db idl t) + | Term t -> Term (db idl t) + | Type v as ty -> check_type_v refs v; ty + | Refarg _ -> assert false + + and db idl e = + { desc = db_desc idl e.desc ; + pre = e.pre; post = e.post; + loc = e.loc; info = e.info } + + in + let ids = Termops.ids_of_named_context (Global.named_context ()) in + (* TODO: separer X:Set et x:V:Set + virer le reste (axiomes, etc.) *) + let vars,refs = all_vars (), all_refs () in + db ([],vars@ids,refs) e +;; + diff --git a/contrib/correctness/pdb.mli b/contrib/correctness/pdb.mli new file mode 100644 index 00000000..a0df29bd --- /dev/null +++ b/contrib/correctness/pdb.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pdb.mli,v 1.2.16.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Ptype +open Past + + +(* Here we separate local and global variables, we check the use of + * references and arrays w.r.t the local and global environments, etc. + * These functions directly raise UserError exceptions on bad programs. + *) + +val check_type_v : Names.identifier list -> 'a ml_type_v -> unit + +val db_prog : program -> program + diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml new file mode 100644 index 00000000..08d6b002 --- /dev/null +++ b/contrib/correctness/peffect.ml @@ -0,0 +1,159 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: peffect.ml,v 1.3.14.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Names +open Nameops +open Pmisc + +(* The type of effects. + * + * An effect is composed of two lists (r,w) of variables. + * The first one is the list of read-only variables + * and the second one is the list of read-write variables. + * + * INVARIANT: 1. each list is sorted in decreasing order for Pervasives.compare + * 2. there are no duplicate elements in each list + * 3. the two lists are disjoint + *) + +type t = identifier list * identifier list + + +(* the empty effect *) + +let bottom = ([], []) + +(* basic operations *) + +let push x l = + let rec push_rec = function + [] -> [x] + | (y::rem) as l -> + if x = y then l else if x > y then x::l else y :: push_rec rem + in + push_rec l + +let basic_remove x l = + let rec rem_rec = function + [] -> [] + | y::l -> if x = y then l else y :: rem_rec l + in + rem_rec l + +let mem x (r,w) = (List.mem x r) or (List.mem x w) + +let rec basic_union = function + [], s2 -> s2 + | s1, [] -> s1 + | ((v1::l1) as s1), ((v2::l2) as s2) -> + if v1 > v2 then + v1 :: basic_union (l1,s2) + else if v1 < v2 then + v2 :: basic_union (s1,l2) + else + v1 :: basic_union (l1,l2) + +(* adds reads and writes variables *) + +let add_read id ((r,w) as e) = + (* if the variable is already a RW it is ok, otherwise adds it as a RO. *) + if List.mem id w then + e + else + push id r, w + +let add_write id (r,w) = + (* if the variable is a RO then removes it from RO. Adds it to RW. *) + if List.mem id r then + basic_remove id r, push id w + else + r, push id w + +(* access *) + +let get_reads = basic_union +let get_writes = snd +let get_repr e = (get_reads e, get_writes e) + +(* tests *) + +let is_read (r,_) id = List.mem id r +let is_write (_,w) id = List.mem id w + +(* union and disjunction *) + +let union (r1,w1) (r2,w2) = basic_union (r1,r2), basic_union (w1,w2) + +let rec diff = function + [], s2 -> [] + | s1, [] -> s1 + | ((v1::l1) as s1), ((v2::l2) as s2) -> + if v1 > v2 then + v1 :: diff (l1,s2) + else if v1 < v2 then + diff (s1,l2) + else + diff (l1,l2) + +let disj (r1,w1) (r2,w2) = + let w1_w2 = diff (w1,w2) and w2_w1 = diff (w2,w1) in + let r = basic_union (basic_union (r1,r2), basic_union (w1_w2,w2_w1)) + and w = basic_union (w1,w2) in + r,w + +(* comparison relation *) + +let le e1 e2 = failwith "effects: le: not yet implemented" + +let inf e1 e2 = failwith "effects: inf: not yet implemented" + +(* composition *) + +let compose (r1,w1) (r2,w2) = + let r = basic_union (r1, diff (r2,w1)) in + let w = basic_union (w1,w2) in + r,w + +(* remove *) + +let remove (r,w) name = basic_remove name r, basic_remove name w + +(* substitution *) + +let subst_list (x,x') l = + if List.mem x l then push x' (basic_remove x l) else l + +let subst_one (r,w) s = subst_list s r, subst_list s w + +let subst s e = List.fold_left subst_one e s + +(* pretty-print *) + +open Pp +open Util +open Himsg + +let pp (r,w) = + hov 0 (if r<>[] then + (str"reads " ++ + prlist_with_sep (fun () -> (str"," ++ spc ())) pr_id r) + else (mt ()) ++ + spc () ++ + if w<>[] then + (str"writes " ++ + prlist_with_sep (fun ()-> (str"," ++ spc ())) pr_id w) + else (mt ()) +) + +let ppr e = + Pp.pp (pp e) + diff --git a/contrib/correctness/peffect.mli b/contrib/correctness/peffect.mli new file mode 100644 index 00000000..d6d0ce22 --- /dev/null +++ b/contrib/correctness/peffect.mli @@ -0,0 +1,42 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: peffect.mli,v 1.1.16.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Names + +(* The abstract type of effects *) + +type t + +val bottom : t +val add_read : identifier -> t -> t +val add_write : identifier -> t -> t + +val get_reads : t -> identifier list +val get_writes : t -> identifier list +val get_repr : t -> (identifier list) * (identifier list) + +val is_read : t -> identifier -> bool (* read-only *) +val is_write : t -> identifier -> bool (* read-write *) + +val compose : t -> t -> t + +val union : t -> t -> t +val disj : t -> t -> t + +val remove : t -> identifier -> t + +val subst : (identifier * identifier) list -> t -> t + + +val pp : t -> Pp.std_ppcmds +val ppr : t -> unit + diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml new file mode 100644 index 00000000..820d1cf0 --- /dev/null +++ b/contrib/correctness/penv.ml @@ -0,0 +1,240 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: penv.ml,v 1.10.2.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Pmisc +open Past +open Ptype +open Names +open Nameops +open Libobject +open Library +open Term + +(* Environments for imperative programs. + * + * An environment of programs is an association tables + * from identifiers (Names.identifier) to types of values with effects + * (ProgAst.ml_type_v), together with a list of these associations, since + * the order is relevant (we have dependent types e.g. [x:nat; t:(array x T)]) + *) + +module Env = struct + type 'a t = ('a Idmap.t) + * ((identifier * 'a) list) + * ((identifier * (identifier * variant)) list) + let empty = Idmap.empty, [], [] + let add id v (m,l,r) = (Idmap.add id v m, (id,v)::l, r) + let find id (m,_,_) = Idmap.find id m + let fold f (_,l,_) x0 = List.fold_right f l x0 + let add_rec (id,var) (m,l,r) = (m,l,(id,var)::r) + let find_rec id (_,_,r) = List.assoc id r +end + +(* Local environments *) + +type type_info = Set | TypeV of type_v + +type local_env = type_info Env.t + +let empty = (Env.empty : local_env) + +let add (id,v) = Env.add id (TypeV v) + +let add_set id = Env.add id Set + +let find id env = + match Env.find id env with TypeV v -> v | Set -> raise Not_found + +let is_local env id = + try + match Env.find id env with TypeV _ -> true | Set -> false + with + Not_found -> false + +let is_local_set env id = + try + match Env.find id env with TypeV _ -> false | Set -> true + with + Not_found -> false + + +(* typed programs *) + +type typing_info = { + env : local_env; + kappa : constr ml_type_c +} + +type typed_program = (typing_info, constr) t + + +(* The global environment. + * + * We have a global typing environment env + * We also keep a table of programs for extraction purposes + * and a table of initializations (still for extraction) + *) + +let (env : type_info Env.t ref) = ref Env.empty + +let (pgm_table : (typed_program option) Idmap.t ref) = ref Idmap.empty + +let (init_table : constr Idmap.t ref) = ref Idmap.empty + +let freeze () = (!env, !pgm_table, !init_table) +let unfreeze (e,p,i) = env := e; pgm_table := p; init_table := i +let init () = + env := Env.empty; pgm_table := Idmap.empty; init_table := Idmap.empty +;; + +Summary.declare_summary "programs-environment" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init; + Summary.survive_module = false; + Summary.survive_section = false } +;; + +(* Operations on the global environment. *) + +let add_pgm id p = pgm_table := Idmap.add id p !pgm_table + +let cache_global (_,(id,v,p)) = + env := Env.add id v !env; add_pgm id p + +let type_info_app f = function Set -> Set | TypeV v -> TypeV (f v) + +let subst_global (_,s,(id,v,p)) = (id, type_info_app (type_v_knsubst s) v, p) + +let (inProg,outProg) = + declare_object { object_name = "programs-objects"; + cache_function = cache_global; + load_function = (fun _ -> cache_global); + open_function = (fun _ _ -> ()); + classify_function = (fun (_,x) -> Substitute x); + subst_function = subst_global; + export_function = (fun x -> Some x) } + +let is_mutable = function Ref _ | Array _ -> true | _ -> false + +let add_global id v p = + try + let _ = Env.find id !env in + Perror.clash id None + with + Not_found -> begin + let id' = + if is_mutable v then id + else id_of_string ("prog_" ^ (string_of_id id)) + in + Lib.add_leaf id' (inProg (id,TypeV v,p)) + end + +let add_global_set id = + try + let _ = Env.find id !env in + Perror.clash id None + with + Not_found -> Lib.add_leaf id (inProg (id,Set,None)) + +let is_global id = + try + match Env.find id !env with TypeV _ -> true | Set -> false + with + Not_found -> false + +let is_global_set id = + try + match Env.find id !env with TypeV _ -> false | Set -> true + with + Not_found -> false + + +let lookup_global id = + match Env.find id !env with TypeV v -> v | Set -> raise Not_found + +let find_pgm id = Idmap.find id !pgm_table + +let all_vars () = + Env.fold + (fun (id,v) l -> match v with TypeV (Arrow _|TypePure _) -> id::l | _ -> l) + !env [] + +let all_refs () = + Env.fold + (fun (id,v) l -> match v with TypeV (Ref _ | Array _) -> id::l | _ -> l) + !env [] + +(* initializations *) + +let cache_init (_,(id,c)) = + init_table := Idmap.add id c !init_table + +let subst_init (_,s,(id,c)) = (id, subst_mps s c) + +let (inInit,outInit) = + declare_object { object_name = "programs-objects-init"; + cache_function = cache_init; + load_function = (fun _ -> cache_init); + open_function = (fun _ _-> ()); + classify_function = (fun (_,x) -> Substitute x); + subst_function = subst_init; + export_function = (fun x -> Some x) } + +let initialize id c = Lib.add_anonymous_leaf (inInit (id,c)) + +let find_init id = Idmap.find id !init_table + + +(* access in env, local then global *) + +let type_in_env env id = + try find id env with Not_found -> lookup_global id + +let is_in_env env id = + (is_global id) or (is_local env id) + +let fold_all f lenv x0 = + let x1 = Env.fold f !env x0 in + Env.fold f lenv x1 + + +(* recursions *) + +let add_recursion = Env.add_rec + +let find_recursion = Env.find_rec + + +(* We also maintain a table of the currently edited proofs of programs + * in order to add them in the environnement when the user does Save *) + +open Pp +open Himsg + +let (edited : (type_v * typed_program) Idmap.t ref) = ref Idmap.empty + +let new_edited id v = + edited := Idmap.add id v !edited + +let is_edited id = + try let _ = Idmap.find id !edited in true with Not_found -> false + +let register id id' = + try + let (v,p) = Idmap.find id !edited in + let _ = add_global id' v (Some p) in + Options.if_verbose + msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined")); + edited := Idmap.remove id !edited + with Not_found -> () + diff --git a/contrib/correctness/penv.mli b/contrib/correctness/penv.mli new file mode 100644 index 00000000..ef2e4c6e --- /dev/null +++ b/contrib/correctness/penv.mli @@ -0,0 +1,87 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: penv.mli,v 1.3.8.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Ptype +open Past +open Names +open Libnames +open Term + +(* Environment for imperative programs. + * + * Here we manage the global environment, which is imperative, + * and we provide a functional local environment. + * + * The most important functions, is_in_env, type_in_env and fold_all + * first look in the local environment then in the global one. + *) + +(* local environments *) + +type local_env + +val empty : local_env +val add : (identifier * type_v) -> local_env -> local_env +val add_set : identifier -> local_env -> local_env +val is_local : local_env -> identifier -> bool +val is_local_set : local_env -> identifier -> bool + +(* typed programs *) + +type typing_info = { + env : local_env; + kappa : constr ml_type_c +} + +type typed_program = (typing_info, constr) t + +(* global environment *) + +val add_global : identifier -> type_v -> typed_program option -> object_name +val add_global_set : identifier -> object_name +val is_global : identifier -> bool +val is_global_set : identifier -> bool +val lookup_global : identifier -> type_v + +val all_vars : unit -> identifier list +val all_refs : unit -> identifier list + +(* a table keeps the program (for extraction) *) + +val find_pgm : identifier -> typed_program option + +(* a table keeps the initializations of mutable objects *) + +val initialize : identifier -> constr -> unit +val find_init : identifier -> constr + +(* access in env (local then global) *) + +val type_in_env : local_env -> identifier -> type_v +val is_in_env : local_env -> identifier -> bool + +type type_info = Set | TypeV of type_v +val fold_all : (identifier * type_info -> 'a -> 'a) -> local_env -> 'a -> 'a + +(* local environnements also contains a list of recursive functions + * with the associated variant *) + +val add_recursion : identifier * (identifier*variant) -> local_env -> local_env +val find_recursion : identifier -> local_env -> identifier * variant + +(* We also maintain a table of the currently edited proofs of programs + * in order to add them in the environnement when the user does Save *) + +val new_edited : identifier -> type_v * typed_program -> unit +val is_edited : identifier -> bool +val register : identifier -> identifier -> unit + diff --git a/contrib/correctness/perror.ml b/contrib/correctness/perror.ml new file mode 100644 index 00000000..40fe4c98 --- /dev/null +++ b/contrib/correctness/perror.ml @@ -0,0 +1,172 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: perror.ml,v 1.9.2.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Himsg + +open Ptype +open Past + +let is_mutable = function Ref _ | Array _ -> true | _ -> false +let is_pure = function TypePure _ -> true | _ -> false + +let raise_with_loc = function + | None -> raise + | Some loc -> Stdpp.raise_with_loc loc + +let unbound_variable id loc = + raise_with_loc loc + (UserError ("Perror.unbound_variable", + (hov 0 (str"Unbound variable" ++ spc () ++ pr_id id ++ fnl ())))) + +let unbound_reference id loc = + raise_with_loc loc + (UserError ("Perror.unbound_reference", + (hov 0 (str"Unbound reference" ++ spc () ++ pr_id id ++ fnl ())))) + +let clash id loc = + raise_with_loc loc + (UserError ("Perror.clash", + (hov 0 (str"Clash with previous constant" ++ spc () ++ + str(string_of_id id) ++ fnl ())))) + +let not_defined id = + raise + (UserError ("Perror.not_defined", + (hov 0 (str"The object" ++ spc () ++ pr_id id ++ spc () ++ + str"is not defined" ++ fnl ())))) + +let check_for_reference loc id = function + Ref _ -> () + | _ -> Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_reference", + hov 0 (pr_id id ++ spc () ++ + str"is not a reference"))) + +let check_for_array loc id = function + Array _ -> () + | _ -> Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_array", + hov 0 (pr_id id ++ spc () ++ + str"is not an array"))) + +let is_constant_type s = function + TypePure c -> + let id = id_of_string s in + let c' = Constrintern.global_reference id in + Reductionops.is_conv (Global.env()) Evd.empty c c' + | _ -> false + +let check_for_index_type loc v = + let is_index = is_constant_type "Z" v in + if not is_index then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_index", + hov 0 (str"This expression is an index" ++ spc () ++ + str"and should have type int (Z)"))) + +let check_no_effect loc ef = + if not (Peffect.get_writes ef = []) then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_no_effect", + hov 0 (str"A boolean should not have side effects" +))) + +let should_be_boolean loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.should_be_boolean", + hov 0 (str"This expression is a test:" ++ spc () ++ + str"it should have type bool"))) + +let test_should_be_annotated loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.test_should_be_annotated", + hov 0 (str"This test should be annotated"))) + +let if_branches loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.if_branches", + hov 0 (str"The two branches of an `if' expression" ++ spc () ++ + str"should have the same type"))) + +let check_for_not_mutable loc v = + if is_mutable v then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_not_mutable", + hov 0 (str"This expression cannot be a mutable"))) + +let check_for_pure_type loc v = + if not (is_pure v) then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_pure_type", + hov 0 (str"This expression must be pure" ++ spc () ++ + str"(neither a mutable nor a function)"))) + +let check_for_let_ref loc v = + if not (is_pure v) then + Stdpp.raise_with_loc loc + (UserError ("Perror.check_for_let_ref", + hov 0 (str"References can only be bound in pure terms"))) + +let informative loc s = + Stdpp.raise_with_loc loc + (UserError ("Perror.variant_informative", + hov 0 (str s ++ spc () ++ str"must be informative"))) + +let variant_informative loc = informative loc "Variant" +let should_be_informative loc = informative loc "This term" + +let app_of_non_function loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.app_of_non_function", + hov 0 (str"This term cannot be applied" ++ spc () ++ + str"(either it is not a function" ++ spc () ++ + str"or it is applied to non pure arguments)"))) + +let partial_app loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.partial_app", + hov 0 (str"This function does not have" ++ + spc () ++ str"the right number of arguments"))) + +let expected_type loc s = + Stdpp.raise_with_loc loc + (UserError ("Perror.expected_type", + hov 0 (str"Argument is expected to have type" ++ spc () ++ s))) + +let expects_a_type id loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.expects_a_type", + hov 0 (str"The argument " ++ pr_id id ++ spc () ++ + str"in this application is supposed to be a type"))) + +let expects_a_term id = + raise + (UserError ("Perror.expects_a_type", + hov 0 (str"The argument " ++ pr_id id ++ spc () ++ + str"in this application is supposed to be a term"))) + +let should_be_a_variable loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.should_be_a_variable", + hov 0 (str"Argument should be a variable"))) + +let should_be_a_reference loc = + Stdpp.raise_with_loc loc + (UserError ("Perror.should_be_a_reference", + hov 0 (str"Argument of function should be a reference"))) + + diff --git a/contrib/correctness/perror.mli b/contrib/correctness/perror.mli new file mode 100644 index 00000000..40b2d25c --- /dev/null +++ b/contrib/correctness/perror.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: perror.mli,v 1.2.6.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Pp +open Util +open Names +open Ptype +open Past + +val unbound_variable : identifier -> loc option -> 'a +val unbound_reference : identifier -> loc option -> 'a + +val clash : identifier -> loc option -> 'a +val not_defined : identifier -> 'a + +val check_for_reference : loc -> identifier -> type_v -> unit +val check_for_array : loc -> identifier -> type_v -> unit + +val check_for_index_type : loc -> type_v -> unit +val check_no_effect : loc -> Peffect.t -> unit +val should_be_boolean : loc -> 'a +val test_should_be_annotated : loc -> 'a +val if_branches : loc -> 'a + +val check_for_not_mutable : loc -> type_v -> unit +val check_for_pure_type : loc -> type_v -> unit +val check_for_let_ref : loc -> type_v -> unit + +val variant_informative : loc -> 'a +val should_be_informative : loc -> 'a + +val app_of_non_function : loc -> 'a +val partial_app : loc -> 'a +val expected_type : loc -> std_ppcmds -> 'a +val expects_a_type : identifier -> loc -> 'a +val expects_a_term : identifier -> 'a +val should_be_a_variable : loc -> 'a +val should_be_a_reference : loc -> 'a diff --git a/contrib/correctness/pextract.ml b/contrib/correctness/pextract.ml new file mode 100644 index 00000000..2a35d471 --- /dev/null +++ b/contrib/correctness/pextract.ml @@ -0,0 +1,473 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pextract.ml,v 1.5.6.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Pp_control +open Pp +open Util +open System +open Names +open Term +open Himsg +open Reduction + +open Putil +open Ptype +open Past +open Penv +open Putil + +let extraction env c = + let ren = initial_renaming env in + let sign = Pcicenv.now_sign_of ren env in + let fsign = Mach.fsign_of_sign (Evd.mt_evd()) sign in + match Mach.infexecute (Evd.mt_evd()) (sign,fsign) c with + | (_,Inf j) -> j._VAL + | (_,Logic) -> failwith "Prog_extract.pp: should be informative" + +(* les tableaux jouent un role particulier, puisqu'ils seront extraits + * vers des tableaux ML *) + +let sp_access = coq_constant ["correctness"; "Arrays"] "access" +let access = ConstRef sp_access + +let has_array = ref false + +let pp_conversions () = + (str"\ +let rec int_of_pos = function + XH -> 1 + | XI p -> 2 * (int_of_pos p) + 1 + | XO p -> 2 * (int_of_pos p) + ++ ++ + +let int_of_z = function + ZERO -> 0 + | POS p -> int_of_pos p + | NEG p -> -(int_of_pos p) + ++ ++ +") (* '"' *) + +(* collect all section-path in a CIC constant *) + +let spset_of_cci env c = + let spl = Fw_env.collect (extraction env c) in + let sps = List.fold_left (fun e x -> SpSet.add x e) SpSet.empty spl in + has_array := !has_array or (SpSet.mem sp_access sps) ++ + SpSet.remove sp_access sps + + +(* collect all Coq constants and all pgms appearing in a given program *) + +let add_id env ((sp,ids) as s) id = + if is_local env id then + s + else if is_global id then + (sp,IdSet.add id ids) + else + try (SpSet.add (Nametab.sp_of_id FW id) sp,ids) with Not_found -> s + +let collect env = + let rec collect_desc env s = function + | Var x -> add_id env s x + | Acc x -> add_id env s x + | Aff (x,e1) -> add_id env (collect_rec env s e1) x + | TabAcc (_,x,e1) -> + has_array := true ++ + add_id env (collect_rec env s e1) x + | TabAff (_,x,e1,e2) -> + has_array := true ++ + add_id env (collect_rec env (collect_rec env s e1) e2) x + | Seq bl -> + List.fold_left (fun s st -> match st with + Statement p -> collect_rec env s p + | _ -> s) s bl + | If (e1,e2,e3) -> + collect_rec env (collect_rec env (collect_rec env s e1) e2) e3 + | While (b,_,_,bl) -> + let s = List.fold_left (fun s st -> match st with + Statement p -> collect_rec env s p + | _ -> s) s bl in + collect_rec env s b + | Lam (bl,e) -> + collect_rec (traverse_binders env bl) s e + | App (e1,l) -> + let s = List.fold_left (fun s a -> match a with + Term t -> collect_rec env s t + | Type _ | Refarg _ -> s) s l in + collect_rec env s e1 + | SApp (_,l) -> + List.fold_left (fun s a -> collect_rec env s a) s l + | LetRef (x,e1,e2) -> + let (_,v),_,_,_ = e1.info.kappa in + collect_rec (add (x,Ref v) env) (collect_rec env s e1) e2 + | LetIn (x,e1,e2) -> + let (_,v),_,_,_ = e1.info.kappa in + collect_rec (add (x,v) env) (collect_rec env s e1) e2 + | LetRec (f,bl,_,_,e) -> + let env' = traverse_binders env bl in + let env'' = add (f,make_arrow bl e.info.kappa) env' in + collect_rec env'' s e + | Debug (_,e1) -> collect_rec env s e1 + | PPoint (_,d) -> collect_desc env s d + | Expression c -> + let (sp,ids) = s in + let sp' = spset_of_cci env c in + SpSet.fold + (fun s (es,ei) -> + let id = basename s in + if is_global id then (*SpSet.add s*)es,IdSet.add id ei + else SpSet.add s es,ei) + sp' (sp,ids) + + and collect_rec env s p = collect_desc env s p.desc + + in + collect_rec env (SpSet.empty,IdSet.empty) + + +(* On a besoin de faire du renommage, tout comme pour l'extraction des + * termes Coq. En ce qui concerne les globaux, on utilise la table de + * Fwtoml. Pour les objects locaux, on introduit la structure de + * renommage rename_struct + *) + +module Ocaml_ren = Ocaml.OCaml_renaming + +let rename_global id = + let id' = Ocaml_ren.rename_global_term !Fwtoml.globals (Name id) in + Fwtoml.add_global_renaming (id,id') ++ + id' + +type rename_struct = { rn_map : identifier IdMap.t; + rn_avoid : identifier list } + +let rn_empty = { rn_map = IdMap.empty; rn_avoid = [] } + +let rename_local rn id = + let id' = Ocaml_ren.rename_term (!Fwtoml.globals@rn.rn_avoid) (Name id) in + { rn_map = IdMap.add id id' rn.rn_map; rn_avoid = id' :: rn.rn_avoid }, + id' + +let get_local_name rn id = IdMap.find id rn.rn_map + +let get_name env rn id = + if is_local env id then + get_local_name rn id + else + Fwtoml.get_global_name id + +let rec rename_binders rn = function + | [] -> rn + | (id,_) :: bl -> let rn',_ = rename_local rn id in rename_binders rn' bl + +(* on a bespoin d'un pretty-printer de constr particulier, qui reconnaisse + * les acces a des references et dans des tableaux, et qui de plus n'imprime + * pas de GENTERM lorsque des identificateurs ne sont pas visibles. + * Il est simplifie dans la mesure ou l'on a ici que des constantes et + * des applications. + *) + +let putpar par s = + if par then (str"(" ++ s ++ str")") else s + +let is_ref env id = + try + (match type_in_env env id with Ref _ -> true | _ -> false) + with + Not_found -> false + +let rec pp_constr env rn = function + | VAR id -> + if is_ref env id then + (str"!" ++ pID (get_name env rn id)) + else + pID (get_name env rn id) + | DOPN((Const _|MutInd _|MutConstruct _) as oper, _) -> + pID (Fwtoml.name_of_oper oper) + | DOPN(AppL,v) -> + if Array.length v = 0 then + (mt ()) + else begin + match v.(0) with + DOPN(Const sp,_) when sp = sp_access -> + (pp_constr env rn v.(3) ++ + str".(int_of_z " ++ pp_constr env rn v.(4) ++ str")") + | _ -> + hov 2 (putpar true (prvect_with_sep (fun () -> (spc ())) + (pp_constr env rn) v)) + end + | DOP2(Cast,c,_) -> pp_constr env rn c + | _ -> failwith "Prog_extract.pp_constr: unexpected constr" + + +(* pretty-print of imperative programs *) + +let collect_lambda = + let rec collect acc p = match p.desc with + | Lam(bl,t) -> collect (bl@acc) t + | x -> acc,p + in + collect [] + +let pr_binding rn = + prlist_with_sep (fun () -> (mt ())) + (function + | (id,(Untyped | BindType _)) -> + (str" " ++ pID (get_local_name rn id)) + | (id,BindSet) -> (mt ())) + +let pp_prog id = + let rec pp_d env rn par = function + | Var x -> pID (get_name env rn x) + | Acc x -> (str"!" ++ pID (get_name env rn x)) + | Aff (x,e1) -> (pID (get_name env rn x) ++ + str" := " ++ hov 0 (pp env rn false e1)) + | TabAcc (_,x,e1) -> + (pID (get_name env rn x) ++ + str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")") + | TabAff (_,x,e1,e2) -> + (pID (get_name env rn x) ++ + str".(int_of_z " ++ hov 0 (pp env rn true e1) ++ str")" ++ + str" <-" ++ spc () ++ hov 2 (pp env rn false e2)) + | Seq bl -> + (str"begin" ++ fnl () ++ + str" " ++ hov 0 (pp_block env rn bl) ++ fnl () ++ + str"end") + | If (e1,e2,e3) -> + putpar par (str"if " ++ (pp env rn false e1) ++ + str" then" ++ fnl () ++ + str" " ++ hov 0 (pp env rn false e2) ++ fnl () ++ + str"else" ++ fnl () ++ + str" " ++ hov 0 (pp env rn false e3)) + (* optimisations : then begin .... end else begin ... end *) + | While (b,inv,_,bl) -> + (str"while " ++ (pp env rn false b) ++ str" do" ++ fnl () ++ + str" " ++ + hov 0 ((match inv with + None -> (mt ()) + | Some c -> (str"(* invariant: " ++ pTERM c.a_value ++ + str" *)" ++ fnl ())) ++ + pp_block env rn bl) ++ fnl () ++ + str"done") + | Lam (bl,e) -> + let env' = traverse_binders env bl in + let rn' = rename_binders rn bl in + putpar par + (hov 2 (str"fun" ++ pr_binding rn' bl ++ str" ->" ++ + spc () ++ pp env' rn' false e)) + | SApp ((Var id)::_, [e1; e2]) + when id = connective_and or id = connective_or -> + let conn = if id = connective_and then "&" else "or" in + putpar par + (hov 0 (pp env rn true e1 ++ spc () ++ str conn ++ spc () ++ + pp env rn true e2)) + | SApp ((Var id)::_, [e]) when id = connective_not -> + putpar par + (hov 0 (str"not" ++ spc () ++ pp env rn true e)) + | SApp _ -> + invalid_arg "Prog_extract.pp_prog (SApp)" + | App(e1,[]) -> + hov 0 (pp env rn false e1) + | App (e1,l) -> + putpar true + (hov 2 (pp env rn true e1 ++ + prlist (function + Term p -> (spc () ++ pp env rn true p) + | Refarg x -> (spc () ++ pID (get_name env rn x)) + | Type _ -> (mt ())) + l)) + | LetRef (x,e1,e2) -> + let (_,v),_,_,_ = e1.info.kappa in + let env' = add (x,Ref v) env in + let rn',x' = rename_local rn x in + putpar par + (hov 0 (str"let " ++ pID x' ++ str" = ref " ++ pp env rn false e1 ++ + str" in" ++ fnl () ++ pp env' rn' false e2)) + | LetIn (x,e1,e2) -> + let (_,v),_,_,_ = e1.info.kappa in + let env' = add (x,v) env in + let rn',x' = rename_local rn x in + putpar par + (hov 0 (str"let " ++ pID x' ++ str" = " ++ pp env rn false e1 ++ + str" in" ++ fnl () ++ pp env' rn' false e2)) + | LetRec (f,bl,_,_,e) -> + let env' = traverse_binders env bl in + let rn' = rename_binders rn bl in + let env'' = add (f,make_arrow bl e.info.kappa) env' in + let rn'',f' = rename_local rn' f in + putpar par + (hov 0 (str"let rec " ++ pID f' ++ pr_binding rn' bl ++ str" =" ++ fnl () ++ + str" " ++ hov 0 (pp env'' rn'' false e) ++ fnl () ++ + str"in " ++ pID f')) + | Debug (_,e1) -> pp env rn par e1 + | PPoint (_,d) -> pp_d env rn par d + | Expression c -> + pp_constr env rn (extraction env c) + + and pp_block env rn bl = + let bl = + map_succeed (function Statement p -> p | _ -> failwith "caught") bl + in + prlist_with_sep (fun () -> (str";" ++ fnl ())) + (fun p -> hov 0 (pp env rn false p)) bl + + and pp env rn par p = + (pp_d env rn par p.desc) + + and pp_mut v c = match v with + | Ref _ -> + (str"ref " ++ pp_constr empty rn_empty (extraction empty c)) + | Array (n,_) -> + (str"Array.create " ++ cut () ++ + putpar true + (str"int_of_z " ++ + pp_constr empty rn_empty (extraction empty n)) ++ + str" " ++ pp_constr empty rn_empty (extraction empty c)) + | _ -> invalid_arg "pp_mut" + in + let v = lookup_global id in + let id' = rename_global id in + if is_mutable v then + try + let c = find_init id in + hov 0 (str"let " ++ pID id' ++ str" = " ++ pp_mut v c) + with Not_found -> + errorlabstrm "Prog_extract.pp_prog" + (str"The variable " ++ pID id ++ + str" must be initialized first !") + else + match find_pgm id with + | None -> + errorlabstrm "Prog_extract.pp_prog" + (str"The program " ++ pID id ++ + str" must be realized first !") + | Some p -> + let bl,p = collect_lambda p in + let rn = rename_binders rn_empty bl in + let env = traverse_binders empty bl in + hov 0 (str"let " ++ pID id' ++ pr_binding rn bl ++ str" =" ++ fnl () ++ + str" " ++ hov 2 (pp env rn false p)) + +(* extraction des programmes impératifs/fonctionnels vers ocaml *) + +(* Il faut parfois importer des modules non ouverts, sinon + * Ocaml.OCaml_pp_file.pp echoue en disant "machin is not a defined + * informative object". Cela dit, ce n'est pas tres satisfaisant, vu que + * la constante existe quand meme: il vaudrait mieux contourner l'echec + * de ml_import.fwsp_of_id + *) + +let import sp = match repr_path sp with + | [m],_,_ -> + begin + try Library.import_export_module m true + with _ -> () + end + | _ -> () + +let pp_ocaml file prm = + has_array := false ++ + (* on separe objects Coq et programmes *) + let cic,pgms = + List.fold_left + (fun (sp,ids) id -> + if is_global id then (sp,IdSet.add id ids) else (IdSet.add id sp,ids)) + (IdSet.empty,IdSet.empty) prm.needed + in + (* on met les programmes dans l'ordre et pour chacun on recherche les + * objects Coq necessaires, que l'on rajoute a l'ensemble cic *) + let cic,_,pgms = + let o_pgms = fold_all (fun (id,_) l -> id::l) empty [] in + List.fold_left + (fun (cic,pgms,pl) id -> + if IdSet.mem id pgms then + let spl,pgms' = + try + (match find_pgm id with + | Some p -> collect empty p + | None -> + (try + let c = find_init id in + spset_of_cci empty c,IdSet.empty + with Not_found -> + SpSet.empty,IdSet.empty)) + with Not_found -> SpSet.empty,IdSet.empty + in + let cic' = + SpSet.fold + (fun sp cic -> import sp ++ IdSet.add (basename sp) cic) + spl cic + in + (cic',IdSet.union pgms pgms',id::pl) + else + (cic,pgms,pl)) + (cic,pgms,[]) o_pgms + in + let cic = IdSet.elements cic in + (* on pretty-print *) + let prm' = { needed = cic ++ expand = prm.expand ++ + expansion = prm.expansion ++ exact = prm.exact } + in + let strm = (Ocaml.OCaml_pp_file.pp_recursive prm' ++ + fnl () ++ fnl () ++ + if !has_array then pp_conversions() else (mt ()) ++ + prlist (fun p -> (pp_prog p ++ fnl () ++ str";;" ++ fnl () ++ fnl ())) + pgms +) + in + (* puis on ecrit dans le fichier *) + let chan = open_trapping_failure open_out file ".ml" in + let ft = with_output_to chan in + begin + try pP_with ft strm ++ pp_flush_with ft () + with e -> pp_flush_with ft () ++ close_out chan ++ raise e + end ++ + close_out chan + + +(* Initializations of mutable objects *) + +let initialize id com = + let loc = Ast.loc com in + let c = constr_of_com (Evd.mt_evd()) (initial_sign()) com in + let ty = + Reductionops.nf_betaiota (type_of (Evd.mt_evd()) (initial_sign()) c) in + try + let v = lookup_global id in + let ety = match v with + | Ref (TypePure c) -> c | Array (_,TypePure c) -> c + | _ -> raise Not_found + in + if conv (Evd.mt_evd()) ty ety then + initialize id c + else + errorlabstrm "Prog_extract.initialize" + (str"Not the expected type for the mutable " ++ pID id) + with Not_found -> + errorlabstrm "Prog_extract.initialize" + (pr_id id ++ str" is not a mutable") + +(* grammaire *) + +open Vernacinterp + +let _ = vinterp_add "IMPERATIVEEXTRACTION" + (function + | VARG_STRING file :: rem -> + let prm = parse_param rem in (fun () -> pp_ocaml file prm) + | _ -> assert false) + +let _ = vinterp_add "INITIALIZE" + (function + | [VARG_IDENTIFIER id; VARG_COMMAND com] -> + (fun () -> initialize id com) + | _ -> assert false) diff --git a/contrib/correctness/pextract.mli b/contrib/correctness/pextract.mli new file mode 100644 index 00000000..dc5b4124 --- /dev/null +++ b/contrib/correctness/pextract.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pextract.mli,v 1.2.16.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Names + +val pp_ocaml : string -> unit + + diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml new file mode 100644 index 00000000..aed8c5cb --- /dev/null +++ b/contrib/correctness/pmisc.ml @@ -0,0 +1,222 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pmisc.ml,v 1.18.2.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Pp +open Util +open Names +open Nameops +open Term +open Libnames +open Topconstr + +(* debug *) + +let deb_mess s = + if !Options.debug then begin + msgnl s; pp_flush() + end + +let deb_print f x = + if !Options.debug then begin + msgnl (f x); pp_flush() + end + +let list_of_some = function + None -> [] + | Some x -> [x] + +let difference l1 l2 = + let rec diff = function + [] -> [] + | a::rem -> if List.mem a l2 then diff rem else a::(diff rem) + in + diff l1 + +(* TODO: these functions should be moved in the code of Coq *) + +let reraise_with_loc loc f x = + try f x with Util.UserError (_,_) as e -> Stdpp.raise_with_loc loc e + + +(* functions on names *) + +let at = if !Options.v7 then "@" else "'at'" + +let at_id id d = id_of_string ((string_of_id id) ^ at ^ d) + +let is_at id = + try + let _ = string_index_from (string_of_id id) 0 at in true + with Not_found -> + false + +let un_at id = + let s = string_of_id id in + try + let n = string_index_from s 0 at in + id_of_string (String.sub s 0 n), + String.sub s (n + String.length at) + (String.length s - n - String.length at) + with Not_found -> + invalid_arg "un_at" + +let renaming_of_ids avoid ids = + let rec rename avoid = function + [] -> [], avoid + | x::rem -> + let al,avoid = rename avoid rem in + let x' = next_ident_away x avoid in + (x,x')::al, x'::avoid + in + rename avoid ids + +let result_id = id_of_string "result" + +let adr_id id = id_of_string ("adr_" ^ (string_of_id id)) + +(* hypotheses names *) + +let next s r = function + Anonymous -> incr r; id_of_string (s ^ string_of_int !r) + | Name id -> id + +let reset_names,pre_name,post_name,inv_name, + test_name,bool_name,var_name,phi_name,for_name,label_name = + let pre = ref 0 in + let post = ref 0 in + let inv = ref 0 in + let test = ref 0 in + let bool = ref 0 in + let var = ref 0 in + let phi = ref 0 in + let forr = ref 0 in + let label = ref 0 in + (fun () -> + pre := 0; post := 0; inv := 0; test := 0; + bool := 0; var := 0; phi := 0; label := 0), + (next "Pre" pre), + (next "Post" post), + (next "Inv" inv), + (next "Test" test), + (fun () -> next "Bool" bool Anonymous), + (next "Variant" var), + (fun () -> next "rphi" phi Anonymous), + (fun () -> next "for" forr Anonymous), + (fun () -> string_of_id (next "Label" label Anonymous)) + +let default = id_of_string "x_" +let id_of_name = function Name id -> id | Anonymous -> default + + +(* functions on CIC terms *) + +let isevar = Evarutil.new_evar_in_sign (Global.env ()) + +(* Substitutions of variables by others. *) +let subst_in_constr alist = + let alist' = List.map (fun (id,id') -> (id, mkVar id')) alist in + replace_vars alist' + +(* +let subst_in_ast alist ast = + let rec subst = function + Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s) + | Node(l,s,args) -> Node(l,s,List.map subst args) + | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *) + | x -> x + in + subst ast +*) +(* +let subst_ast_in_ast alist ast = + let rec subst = function + Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x) + | Node(l,s,args) -> Node(l,s,List.map subst args) + | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *) + | x -> x + in + subst ast +*) + +let rec subst_in_ast alist = function + | CRef (Ident (loc,id)) -> + CRef (Ident (loc,(try List.assoc id alist with Not_found -> id))) + | x -> map_constr_expr_with_binders subst_in_ast List.remove_assoc alist x + +let rec subst_ast_in_ast alist = function + | CRef (Ident (_,id)) as x -> (try List.assoc id alist with Not_found -> x) + | x -> + map_constr_expr_with_binders subst_ast_in_ast List.remove_assoc alist x + +(* subst. of variables by constr *) +let real_subst_in_constr = replace_vars + +(* Coq constants *) + +let coq_constant d s = + Libnames.encode_kn + (make_dirpath (List.rev (List.map id_of_string ("Coq"::d)))) + (id_of_string s) + +let bool_sp = coq_constant ["Init"; "Datatypes"] "bool" +let coq_true = mkConstruct ((bool_sp,0),1) +let coq_false = mkConstruct ((bool_sp,0),2) + +let constant s = + let id = Constrextern.id_of_v7_string s in + Constrintern.global_reference id + +let connective_and = id_of_string "prog_bool_and" +let connective_or = id_of_string "prog_bool_or" +let connective_not = id_of_string "prog_bool_not" + +let is_connective id = + id = connective_and or id = connective_or or id = connective_not + +(* [conj i s] constructs the conjunction of two constr *) + +let conj i s = Term.applist (constant "and", [i; s]) + +(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type + [(x1:t1)...(xn:tn)v] *) + +let rec n_mkNamedProd v = function + | [] -> v + | (id,ty) :: rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem + +(* [n_lambda v [xn,tn;...;x1,t1]] constructs the type [x1:t1]...[xn:tn]v *) + +let rec n_lambda v = function + | [] -> v + | (id,ty) :: rem -> n_lambda (Term.mkNamedLambda id ty v) rem + +(* [abstract env idl c] constructs [x1]...[xn]c where idl = [x1;...;xn] *) + +let abstract ids c = n_lambda c (List.rev ids) + +(* substitutivity (of kernel names, for modules management) *) + +open Ptype + +let rec type_v_knsubst s = function + | Ref v -> Ref (type_v_knsubst s v) + | Array (c, v) -> Array (subst_mps s c, type_v_knsubst s v) + | Arrow (bl, c) -> Arrow (List.map (binder_knsubst s) bl, type_c_knsubst s c) + | TypePure c -> TypePure (subst_mps s c) + +and type_c_knsubst s ((id,v),e,pl,q) = + ((id, type_v_knsubst s v), e, + List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl, + option_app (fun q -> { q with a_value = subst_mps s q.a_value }) q) + +and binder_knsubst s (id,b) = + (id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b) diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli new file mode 100644 index 00000000..ec7521cc --- /dev/null +++ b/contrib/correctness/pmisc.mli @@ -0,0 +1,81 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pmisc.mli,v 1.9.6.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Names +open Term +open Ptype +open Topconstr + +(* Some misc. functions *) + +val reraise_with_loc : Util.loc -> ('a -> 'b) -> 'a -> 'b + +val list_of_some : 'a option -> 'a list +val difference : 'a list -> 'a list -> 'a list + +val at_id : identifier -> string -> identifier +val un_at : identifier -> identifier * string +val is_at : identifier -> bool + +val result_id : identifier +val adr_id : identifier -> identifier + +val renaming_of_ids : identifier list -> identifier list + -> (identifier * identifier) list * identifier list + +val reset_names : unit -> unit +val pre_name : name -> identifier +val post_name : name -> identifier +val inv_name : name -> identifier +val test_name : name -> identifier +val bool_name : unit -> identifier +val var_name : name -> identifier +val phi_name : unit -> identifier +val for_name : unit -> identifier +val label_name : unit -> string + +val id_of_name : name -> identifier + +(* CIC terms *) + +val isevar : constr + +val subst_in_constr : (identifier * identifier) list -> constr -> constr +val subst_in_ast : (identifier * identifier) list -> constr_expr -> constr_expr +val subst_ast_in_ast : + (identifier * constr_expr) list -> constr_expr -> constr_expr +val real_subst_in_constr : (identifier * constr) list -> constr -> constr + +val constant : string -> constr +val coq_constant : string list -> string -> kernel_name +val conj : constr -> constr -> constr + +val coq_true : constr +val coq_false : constr + +val connective_and : identifier +val connective_or : identifier +val connective_not : identifier +val is_connective : identifier -> bool + +val n_mkNamedProd : constr -> (identifier * constr) list -> constr +val n_lambda : constr -> (identifier * constr) list -> constr +val abstract : (identifier * constr) list -> constr -> constr + +val type_v_knsubst : substitution -> type_v -> type_v +val type_c_knsubst : substitution -> type_c -> type_c + +(* for debugging purposes *) + +val deb_mess : Pp.std_ppcmds -> unit +val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit + diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml new file mode 100644 index 00000000..f899366d --- /dev/null +++ b/contrib/correctness/pmlize.ml @@ -0,0 +1,320 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pmlize.ml,v 1.7.2.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Names +open Term +open Termast +open Pattern +open Matching + +open Pmisc +open Ptype +open Past +open Putil +open Prename +open Penv +open Peffect +open Ptyping +open Pmonad + + +let has_proof_part ren env c = + let sign = Pcicenv.trad_sign_of ren env in + let ty = Typing.type_of (Global.env_of_context sign) Evd.empty c in + Hipattern.is_matching_sigma (Reductionops.nf_betaiota ty) + +(* main part: translation of imperative programs into functional ones. + * + * [env] is the environment + * [ren] is the current renamings of variables + * [t] is the imperative program to translate, annotated with type+effects + * + * we return the translated program in type cc_term + *) + +let rec trad ren t = + let env = t.info.env in + trad_desc ren env t.info.kappa t.desc + +and trad_desc ren env ct d = + let (_,tt),eft,pt,qt = ct in + match d with + + | Expression c -> + let ids = get_reads eft in + let al = current_vars ren ids in + let c' = subst_in_constr al c in + if has_proof_part ren env c' then + CC_expr c' + else + let ty = trad_ml_type_v ren env tt in + make_tuple [ CC_expr c',ty ] qt ren env (current_date ren) + + | Variable id -> + if is_mutable_in_env env id then + invalid_arg "Mlise.trad_desc" + else if is_local env id then + CC_var id + else + CC_expr (constant (string_of_id id)) + + | Acc _ -> + failwith "Mlise.trad: pure terms are supposed to be expressions" + + | TabAcc (check, x, e1) -> + let _,ty_elem,_ = array_info ren env x in + let te1 = trad ren e1 in + let (_,ef1,p1,q1) = e1.info.kappa in + let w = get_writes ef1 in + let ren' = next ren w in + let id = id_of_string "index" in + let access = + make_raw_access ren' env (x,current_var ren' x) (mkVar id) + in + let t,ty = result_tuple ren' (current_date ren) env + (CC_expr access, ty_elem) (eft,qt) in + let t = + if check then + let h = make_pre_access ren env x (mkVar id) in + let_in_pre ty (anonymous_pre true h) t + else + t + in + make_let_in ren env te1 p1 + (current_vars ren' w,q1) (id,constant "Z") (t,ty) + + | Aff (x, e1) -> + let tx = trad_type_in_env ren env x in + let te1 = trad ren e1 in + let (_,ef1,p1,q1) = e1.info.kappa in + let w1 = get_writes ef1 in + let ren' = next ren (x::w1) in + let t_ty = result_tuple ren' (current_date ren) env + (CC_expr (constant "tt"), constant "unit") (eft,qt) + in + make_let_in ren env te1 p1 + (current_vars ren' w1,q1) (current_var ren' x,tx) t_ty + + | TabAff (check, x, e1, e2) -> + let _,ty_elem,ty_array = array_info ren env x in + let te1 = trad ren e1 in + let (_,ef1,p1,q1) = e1.info.kappa in + let w1 = get_writes ef1 in + let ren' = next ren w1 in + let te2 = trad ren' e2 in + let (_,ef2,p2,q2) = e2.info.kappa in + let w2 = get_writes ef2 in + let ren'' = next ren' w2 in + let id1 = id_of_string "index" in + let id2 = id_of_string "v" in + let ren''' = next ren'' [x] in + let t,ty = result_tuple ren''' (current_date ren) env + (CC_expr (constant "tt"), constant "unit") (eft,qt) in + let store = make_raw_store ren'' env (x,current_var ren'' x) (mkVar id1) + (mkVar id2) in + let t = make_let_in ren'' env (CC_expr store) [] ([],None) + (current_var ren''' x,ty_array) (t,ty) in + let t = make_let_in ren' env te2 p2 + (current_vars ren'' w2,q2) (id2,ty_elem) (t,ty) in + let t = + if check then + let h = make_pre_access ren' env x (mkVar id1) in + let_in_pre ty (anonymous_pre true h) t + else + t + in + make_let_in ren env te1 p1 + (current_vars ren' w1,q1) (id1,constant "Z") (t,ty) + + | Seq bl -> + let before = current_date ren in + let finish ren = function + Some (id,ty) -> + result_tuple ren before env (CC_var id, ty) (eft,qt) + | None -> + failwith "a block should contain at least one statement" + in + let bl = trad_block ren env bl in + make_block ren env finish bl + + | If (b, e1, e2) -> + let tb = trad ren b in + let _,efb,_,_ = b.info.kappa in + let ren' = next ren (get_writes efb) in + let te1 = trad ren' e1 in + let te2 = trad ren' e2 in + make_if ren env (tb,b.info.kappa) ren' (te1,e1.info.kappa) + (te2,e2.info.kappa) ct + + (* Translation of the while. *) + + | While (b, inv, var, bl) -> + let ren' = next ren (get_writes eft) in + let tb = trad ren' b in + let tbl = trad_block ren' env bl in + let var' = typed_var ren env var in + make_while ren env var' (tb,b.info.kappa) tbl (inv,ct) + + | Lam (bl, e) -> + let bl' = trad_binders ren env bl in + let env' = traverse_binders env bl in + let ren' = initial_renaming env' in + let te = trans ren' e in + CC_lam (bl', te) + + | SApp ([Variable id; Expression q1; Expression q2], [e1; e2]) + when id = connective_and or id = connective_or -> + let c = constant (string_of_id id) in + let te1 = trad ren e1 + and te2 = trad ren e2 in + let q1' = apply_post ren env (current_date ren) (anonymous q1) + and q2' = apply_post ren env (current_date ren) (anonymous q2) in + CC_app (CC_expr c, [CC_expr q1'.a_value; CC_expr q2'.a_value; te1; te2]) + + | SApp ([Variable id; Expression q], [e]) when id = connective_not -> + let c = constant (string_of_id id) in + let te = trad ren e in + let q' = apply_post ren env (current_date ren) (anonymous q) in + CC_app (CC_expr c, [CC_expr q'.a_value; te]) + + | SApp _ -> + invalid_arg "mlise.trad (SApp)" + + | Apply (f, args) -> + let trad_arg (ren,args) = function + | Term a -> + let ((_,tya),efa,_,_) as ca = a.info.kappa in + let ta = trad ren a in + let w = get_writes efa in + let ren' = next ren w in + ren', ta::args + | Refarg _ -> + ren, args + | Type v -> + let c = trad_ml_type_v ren env v in + ren, (CC_expr c)::args + in + let ren',targs = List.fold_left trad_arg (ren,[]) args in + let tf = trad ren' f in + let cf = f.info.kappa in + let c,(s,_,_),capp = effect_app ren env f args in + let tc_args = + List.combine + (List.rev targs) + (Util.map_succeed + (function + | Term x -> x.info.kappa + | Refarg _ -> failwith "caught" + | Type _ -> + (result_id,TypePure mkSet),Peffect.bottom,[],None) + args) + in + make_app env ren tc_args ren' (tf,cf) (c,s,capp) ct + + | LetRef (x, e1, e2) -> + let (_,v1),ef1,p1,q1 = e1.info.kappa in + let te1 = trad ren e1 in + let tv1 = trad_ml_type_v ren env v1 in + let env' = add (x,Ref v1) env in + let ren' = next ren [x] in + let (_,v2),ef2,p2,q2 = e2.info.kappa in + let tv2 = trad_ml_type_v ren' env' v2 in + let te2 = trad ren' e2 in + let ren'' = next ren' (get_writes ef2) in + let t,ty = result_tuple ren'' (current_date ren) env + (CC_var result_id, tv2) (eft,qt) in + let t = make_let_in ren' env' te2 p2 + (current_vars ren'' (get_writes ef2),q2) + (result_id,tv2) (t,ty) in + let t = make_let_in ren env te1 p1 + (current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty) + in + t + + | Let (x, e1, e2) -> + let (_,v1),ef1,p1,q1 = e1.info.kappa in + let te1 = trad ren e1 in + let tv1 = trad_ml_type_v ren env v1 in + let env' = add (x,v1) env in + let ren' = next ren (get_writes ef1) in + let (_,v2),ef2,p2,q2 = e2.info.kappa in + let tv2 = trad_ml_type_v ren' env' v2 in + let te2 = trad ren' e2 in + let ren'' = next ren' (get_writes ef2) in + let t,ty = result_tuple ren'' (current_date ren) env + (CC_var result_id, tv2) (eft,qt) in + let t = make_let_in ren' env' te2 p2 + (current_vars ren'' (get_writes ef2),q2) + (result_id,tv2) (t,ty) in + let t = make_let_in ren env te1 p1 + (current_vars ren' (get_writes ef1),q1) (x,tv1) (t,ty) + in + t + + | LetRec (f,bl,v,var,e) -> + let (_,ef,_,_) as c = + match tt with Arrow(_,c) -> c | _ -> assert false in + let bl' = trad_binders ren env bl in + let env' = traverse_binders env bl in + let ren' = initial_renaming env' in + let (phi0,var') = find_recursion f e.info.env in + let te = trad ren' e in + let t = make_letrec ren' env' (phi0,var') f bl' (te,e.info.kappa) c in + CC_lam (bl', t) + + | PPoint (s,d) -> + let ren' = push_date ren s in + trad_desc ren' env ct d + + | Debug _ -> failwith "Mlise.trad: Debug: not implemented" + + +and trad_binders ren env = function + | [] -> + [] + | (_,BindType (Ref _ | Array _))::bl -> + trad_binders ren env bl + | (id,BindType v)::bl -> + let tt = trad_ml_type_v ren env v in + (id, CC_typed_binder tt) :: (trad_binders ren env bl) + | (id,BindSet)::bl -> + (id, CC_typed_binder mkSet) :: (trad_binders ren env bl) + | (_,Untyped)::_ -> invalid_arg "trad_binders" + + +and trad_block ren env = function + | [] -> + [] + | (Assert c)::block -> + (Assert c)::(trad_block ren env block) + | (Label s)::block -> + let ren' = push_date ren s in + (Label s)::(trad_block ren' env block) + | (Statement e)::block -> + let te = trad ren e in + let _,efe,_,_ = e.info.kappa in + let w = get_writes efe in + let ren' = next ren w in + (Statement (te,e.info.kappa))::(trad_block ren' env block) + + +and trans ren e = + let env = e.info.env in + let _,ef,p,_ = e.info.kappa in + let ty = trad_ml_type_c ren env e.info.kappa in + let ids = get_reads ef in + let al = current_vars ren ids in + let c = trad ren e in + let c = abs_pre ren env (c,ty) p in + let bl = binding_of_alist ren env al in + make_abs (List.rev bl) c + diff --git a/contrib/correctness/pmlize.mli b/contrib/correctness/pmlize.mli new file mode 100644 index 00000000..95f74ef9 --- /dev/null +++ b/contrib/correctness/pmlize.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pmlize.mli,v 1.2.16.1 2004/07/16 19:30:01 herbelin Exp $ *) + +open Past +open Penv +open Names + +(* translation of imperative programs into intermediate functional programs *) + +val trans : Prename.t -> typed_program -> cc_term + diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml new file mode 100644 index 00000000..b8b39353 --- /dev/null +++ b/contrib/correctness/pmonad.ml @@ -0,0 +1,665 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pmonad.ml,v 1.6.16.1 2004/07/16 19:30:02 herbelin Exp $ *) + +open Util +open Names +open Term +open Termast + +open Pmisc +open Putil +open Ptype +open Past +open Prename +open Penv +open Pcic +open Peffect + + +(* [product ren [y1,z1;...;yk,zk] q] constructs + * the (possibly dependent) tuple type + * + * z1 x ... x zk if no post-condition + * or \exists. y1:z1. ... yk:zk. (Q x1 ... xn) otherwise + * + * where the xi are given by the renaming [ren]. + *) + +let product_name = function + | 2 -> "prod" + | n -> check_product_n n; Printf.sprintf "tuple_%d" n + +let dep_product_name = function + | 1 -> "sig" + | n -> check_dep_product_n n; Printf.sprintf "sig_%d" n + +let product ren env before lo = function + | None -> (* non dependent case *) + begin match lo with + | [_,v] -> v + | _ -> + let s = product_name (List.length lo) in + Term.applist (constant s, List.map snd lo) + end + | Some q -> (* dependent case *) + let s = dep_product_name (List.length lo) in + let a' = apply_post ren env before q in + Term.applist (constant s, (List.map snd lo) @ [a'.a_value]) + +(* [arrow ren v pl] abstracts the term v over the pre-condition if any + * i.e. computes + * + * (P1 x1 ... xn) -> ... -> (Pk x1 ... xn) -> v + * + * where the xi are given by the renaming [ren]. + *) + +let arrow ren env v pl = + List.fold_left + (fun t p -> + if p.p_assert then t else Term.mkArrow (apply_pre ren env p).p_value t) + v pl + +(* [abstract_post ren env (e,q) (res,v)] abstract a post-condition q + * over the write-variables of e *) + +let rec abstract_post ren env (e,q) = + let after_id id = id_of_string ((string_of_id id) ^ "'") in + let (_,go) = Peffect.get_repr e in + let al = List.map (fun id -> (id,after_id id)) go in + let q = option_app (named_app (subst_in_constr al)) q in + let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in + option_app (named_app (abstract tgo)) q + +(* Translation of effects types in cic types. + * + * [trad_ml_type_v] and [trad_ml_type_c] translate types with effects + * into cic types. + *) + +and prod ren env g = + List.map + (fun id -> (current_var ren id, trad_type_in_env ren env id)) + g + +and input ren env e = + let i,_ = Peffect.get_repr e in + prod ren env i + +and output ren env ((id,v),e) = + let tv = trad_ml_type_v ren env v in + let _,o = Peffect.get_repr e in + (prod ren env o) @ [id,tv] + +and input_output ren env c = + let ((res,v),e,_,_) = c in + input ren env e, output ren env ((res,v),e) + +(* The function t -> \barre{t} on V and C. *) + +and trad_ml_type_c ren env c = + let ((res,v),e,p,q) = c in + let q = abstract_post ren env (e,q) in + let lo = output ren env ((res,v),e) in + let ty = product ren env (current_date ren) lo q in + let ty = arrow ren env ty p in + let li = input ren env e in + n_mkNamedProd ty li + +and trad_ml_type_v ren env = function + + | Ref _ | Array _ -> invalid_arg "Monad.trad_ml_type_v" + + | Arrow (bl, c) -> + let bl',ren',env' = + List.fold_left + (fun (bl,ren,env) b -> match b with + | (id,BindType ((Ref _ | Array _) as v)) -> + let env' = add (id,v) env in + let ren' = initial_renaming env' in + (bl,ren',env') + | (id,BindType v) -> + let tt = trad_ml_type_v ren env v in + let env' = add (id,v) env in + let ren' = initial_renaming env' in + (id,tt)::bl,ren',env' + | (id, BindSet) -> + (id,mkSet) :: bl,ren,env + | _ -> failwith "Monad: trad_ml_type_v: not yet implemented" + ) + ([],ren,env) bl + in + n_mkNamedProd (trad_ml_type_c ren' env' c) bl' + + | TypePure c -> + (apply_pre ren env (anonymous_pre false c)).p_value + +and trad_imp_type ren env = function + | Ref v -> trad_ml_type_v ren env v + | Array (c,v) -> Term.applist (constant "array", + [c; trad_ml_type_v ren env v]) + | _ -> invalid_arg "Monad.trad_imp_type" + +and trad_type_in_env ren env id = + let v = type_in_env env id in trad_imp_type ren env v + + + +(* bindings *) + +let binding_of_alist ren env al = + List.map + (fun (id,id') -> (id', CC_typed_binder (trad_type_in_env ren env id))) + al + + +(* [make_abs bl t p] abstracts t w.r.t binding list bl., that is + * [x1:t1]...[xn:tn]t. Returns t if the binding is empty. *) + +let make_abs bl t = match bl with + | [] -> t + | _ -> CC_lam (bl, t) + + +(* [result_tuple ren before env (res,v) (ef,q)] constructs the tuple + * + * (y1,...,yn,res,?::(q/ren y1 ... yn res)) + * + * where the yi are the values of the output of ef. + * if there is no yi and no post-condition, it is simplified in res itself. + *) + +let simple_constr_of_prog = function + | CC_expr c -> c + | CC_var id -> mkVar id + | _ -> assert false + +let make_tuple l q ren env before = match l with + | [e,_] when q = None -> + e + | _ -> + let tl = List.map snd l in + let dep,h,th = match q with + | None -> false,[],[] + | Some c -> + let args = List.map (fun (e,_) -> simple_constr_of_prog e) l in + let c = apply_post ren env before c in + true, + [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *) + [ c.a_value ] (* type of the hole *) + in + CC_tuple (dep, tl @ th, (List.map fst l) @ h) + +let result_tuple ren before env (res,v) (ef,q) = + let ids = get_writes ef in + let lo = + (List.map (fun id -> + let id' = current_var ren id in + CC_var id', trad_type_in_env ren env id) ids) + @ [res,v] + in + let q = abstract_post ren env (ef,q) in + make_tuple lo q ren env before, + product ren env before lo q + + +(* [make_let_in ren env fe p (vo,q) (res,v) t] constructs the term + + [ let h1 = ?:P1 in ... let hn = ?:Pm in ] + let y1,y2,...,yn, res [,q] = fe in + t + + vo=[_,y1;...;_,ym] are list of renamings. + v is the type of res + *) + +let let_in_pre ty p t = + let h = p.p_value in + CC_letin (false, ty, [pre_name p.p_name,CC_typed_binder h], CC_hole h, t) + +let multiple_let_in_pre ty hl t = + List.fold_left (fun t h -> let_in_pre ty h t) t hl + +let make_let_in ren env fe p (vo,q) (res,tyres) (t,ty) = + let b = [res, CC_typed_binder tyres] in + let b',dep = match q with + | None -> [],false + | Some q -> [post_name q.a_name, CC_untyped_binder],true + in + let bl = (binding_of_alist ren env vo) @ b @ b' in + let tyapp = + let n = succ (List.length vo) in + let name = match q with None -> product_name n | _ -> dep_product_name n in + constant name + in + let t = CC_letin (dep, ty, bl, fe, t) in + multiple_let_in_pre ty (List.map (apply_pre ren env) p) t + + +(* [abs_pre ren env (t,ty) pl] abstracts a term t with respect to the + * list of pre-conditions [pl]. Some of them are real pre-conditions + * and others are assertions, according to the boolean field p_assert, + * so we construct the term + * [h1:P1]...[hn:Pn]let h'1 = ?:P'1 in ... let H'm = ?:P'm in t + *) + +let abs_pre ren env (t,ty) pl = + List.fold_left + (fun t p -> + if p.p_assert then + let_in_pre ty (apply_pre ren env p) t + else + let h = pre_name p.p_name in + CC_lam ([h,CC_typed_binder (apply_pre ren env p).p_value],t)) + t pl + + +(* [make_block ren env finish bl] builds the translation of a block + * finish is the function that is applied to the result at the end of the + * block. *) + +let make_block ren env finish bl = + let rec rec_block ren result = function + | [] -> + finish ren result + | (Assert c) :: block -> + let t,ty = rec_block ren result block in + let c = apply_assert ren env c in + let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in + let_in_pre ty p t, ty + | (Label s) :: block -> + let ren' = push_date ren s in + rec_block ren' result block + | (Statement (te,info)) :: block -> + let (_,tye),efe,pe,qe = info in + let w = get_writes efe in + let ren' = next ren w in + let id = result_id in + let tye = trad_ml_type_v ren env tye in + let t = rec_block ren' (Some (id,tye)) block in + make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t, + snd t + in + let t,_ = rec_block ren None bl in + t + + +(* [make_app env ren args ren' (tf,cf) (cb,s,capp) c] + * constructs the application of [tf] to [args]. + * capp is the effect of application, after substitution (s) and cb before + *) + +let eq ty e1 e2 = + Term.applist (constant "eq", [ty; e1; e2]) + +let lt r e1 e2 = + Term.applist (r, [e1; e2]) + +let is_recursive env = function + | CC_var x -> + (try let _ = find_recursion x env in true with Not_found -> false) + | _ -> false + +let if_recursion env f = function + | CC_var x -> + (try let v = find_recursion x env in (f v x) with Not_found -> []) + | _ -> [] + +let dec_phi ren env s svi = + if_recursion env + (fun (phi0,(cphi,r,_)) f -> + let phi = subst_in_constr svi (subst_in_constr s cphi) in + let phi = (apply_pre ren env (anonymous_pre true phi)).p_value in + [CC_expr phi; CC_hole (lt r phi (mkVar phi0))]) + +let eq_phi ren env s svi = + if_recursion env + (fun (phi0,(cphi,_,a)) f -> + let phi = subst_in_constr svi (subst_in_constr s cphi) in + let phi = (apply_pre ren env (anonymous_pre true phi)).p_value in + [CC_hole (eq a phi phi)]) + +let is_ref_binder = function + | (_,BindType (Ref _ | Array _)) -> true + | _ -> false + +let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c = + let ((_,tvf),ef,pf,qf) = cf in + let (_,eapp,papp,qapp) = capp in + let ((_,v),e,p,q) = c in + let bl = List.filter (fun b -> not (is_ref_binder b)) bl in + let recur = is_recursive env tf in + let before = current_date ren in + let ren'' = next ren' (get_writes ef) in + let ren''' = next ren'' (get_writes eapp) in + let res = result_id in + let vi,svi = + let ids = List.map fst bl in + let s = fresh (avoid ren ids) ids in + List.map snd s, s + in + let tyres = subst_in_constr svi (trad_ml_type_v ren env v) in + let t,ty = result_tuple ren''' before env (CC_var res, tyres) (e,q) in + let res_f = id_of_string "vf" in + let inf,outf = + let i,o = let _,e,_,_ = cb in get_reads e, get_writes e in + let apply_s = List.map (fun id -> try List.assoc id s with _ -> id) in + apply_s i, apply_s o + in + let fe = + let xi = List.rev (List.map snd (current_vars ren'' inf)) in + let holes = List.map (fun x -> (apply_pre ren'' env x).p_value) + (List.map (pre_app (subst_in_constr svi)) papp) in + CC_app ((if recur then tf else CC_var res_f), + (dec_phi ren'' env s svi tf) + @(List.map (fun id -> CC_var id) (vi @ xi)) + @(eq_phi ren'' env s svi tf) + @(List.map (fun c -> CC_hole c) holes)) + in + let qapp' = option_app (named_app (subst_in_constr svi)) qapp in + let t = + make_let_in ren'' env fe [] (current_vars ren''' outf,qapp') + (res,tyres) (t,ty) + in + let t = + if recur then + t + else + make_let_in ren' env tf pf + (current_vars ren'' (get_writes ef),qf) + (res_f,trad_ml_type_v ren env tvf) (t,ty) + in + let rec eval_args ren = function + | [] -> t + | (vx,(ta,((_,tva),ea,pa,qa)))::args -> + let w = get_writes ea in + let ren' = next ren w in + let t' = eval_args ren' args in + make_let_in ren env ta pa (current_vars ren' (get_writes ea),qa) + (vx,trad_ml_type_v ren env tva) (t',ty) + in + eval_args ren (List.combine vi args) + + +(* [make_if ren env (tb,cb) ren' (t1,c1) (t2,c2)] + * constructs the term corresponding to a if expression, i.e + * + * [p] let o1, b [,q1] = m1 [?::p1] in + * Cases b of + * R => let o2, v2 [,q2] = t1 [?::p2] in + * (proj (o1,o2)), v2 [,?::q] + * | S => let o2, v2 [,q2] = t2 [?::p2] in + * (proj (o1,o2)), v2 [,?::q] + *) + +let make_if_case ren env ty (b,qb) (br1,br2) = + let id_b,ty',ty1,ty2 = match qb with + | Some q -> + let q = apply_post ren env (current_date ren) q in + let (name,t1,t2) = Term.destLambda q.a_value in + q.a_name, + Term.mkLambda (name, t1, mkArrow t2 ty), + Term.mkApp (q.a_value, [| coq_true |]), + Term.mkApp (q.a_value, [| coq_false |]) + | None -> assert false + in + let n = test_name Anonymous in + CC_app (CC_case (ty', b, [CC_lam ([n,CC_typed_binder ty1], br1); + CC_lam ([n,CC_typed_binder ty2], br2)]), + [CC_var (post_name id_b)]) + +let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c = + let ((_,tvb),eb,pb,qb) = cb in + let ((_,tv1),e1,p1,q1) = c1 in + let ((_,tv2),e2,p2,q2) = c2 in + let ((_,t),e,p,q) = c in + + let wb = get_writes eb in + let resb = id_of_string "resultb" in + let res = result_id in + let tyb = trad_ml_type_v ren' env tvb in + let tt = trad_ml_type_v ren env t in + + (* une branche de if *) + let branch (tv_br,e_br,p_br,q_br) f_br = + let w_br = get_writes e_br in + let ren'' = next ren' w_br in + let t,ty = result_tuple ren'' (current_date ren') env + (CC_var res,tt) (e,q) in + make_let_in ren' env f_br p_br (current_vars ren'' w_br,q_br) + (res,tt) (t,ty), + ty + in + let t1,ty1 = branch c1 t1 in + let t2,ty2 = branch c2 t2 in + let ty = ty1 in + let qb = force_bool_name qb in + let t = make_if_case ren env ty (CC_var resb,qb) (t1,t2) in + make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) + + +(* [make_while ren env (cphi,r,a) (tb,cb) (te,ce) c] + * constructs the term corresponding to the while, i.e. + * + * [h:(I x)](well_founded_induction + * A R ?::(well_founded A R) + * [Phi:A] (x) Phi=phi(x)->(I x)-> \exists x'.res.(I x')/\(S x') + * [Phi_0:A][w:(Phi:A)(Phi<Phi_0)-> ...] + * [x][eq:Phi_0=phi(x)][h:(I x)] + * Cases (b x) of + * (left HH) => (x,?::(IS x)) + * | (right HH) => let x1,_,_ = (e x ?) in + * (w phi(x1) ? x1 ? ?) + * phi(x) x ? ?) + *) + +let id_phi = id_of_string "phi" +let id_phi0 = id_of_string "phi0" + +let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) = + let ((_,tvb),eb,pb,qb) = cb in + let (_,ef,_,is) = c in + + let ren' = next ren (get_writes ef) in + let before = current_date ren in + + let ty = + let is = abstract_post ren' env (ef,is) in + let _,lo = input_output ren env c in + product ren env before lo is + in + let resb = id_of_string "resultb" in + let tyb = trad_ml_type_v ren' env tvb in + let wb = get_writes eb in + + (* premičre branche: le test est vrai => e;w *) + let t1 = + make_block ren' env + (fun ren'' result -> match result with + | Some (id,_) -> + let v = List.rev (current_vars ren'' (get_writes ef)) in + CC_app (CC_var id_w, + [CC_expr (phi_of ren''); + CC_hole (lt r (phi_of ren'') (mkVar id_phi0))] + @(List.map (fun (_,id) -> CC_var id) v) + @(CC_hole (eq a (phi_of ren'') (phi_of ren''))) + ::(match i with + | None -> [] + | Some c -> + [CC_hole (apply_assert ren'' env c).a_value])), + ty + | None -> failwith "a block should contain at least one statement") + tbl + in + + (* deuxičme branche: le test est faux => on sort de la boucle *) + let t2,_ = + result_tuple ren' before env + (CC_expr (constant "tt"),constant "unit") (ef,is) + in + + let b_al = current_vars ren' (get_reads eb) in + let qb = force_bool_name qb in + let t = make_if_case ren' env ty (CC_var resb,qb) (t1,t2) in + let t = + make_let_in ren' env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) + in + let t = + let pl = List.map (pre_of_assert false) (list_of_some i) in + abs_pre ren' env (t,ty) pl + in + let t = + CC_lam ([var_name Anonymous, + CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren'))],t) + in + let bl = binding_of_alist ren env (current_vars ren' (get_writes ef)) in + make_abs (List.rev bl) t + + +let make_while ren env (cphi,r,a) (tb,cb) tbl (i,c) = + let (_,ef,_,is) = c in + let phi_of ren = (apply_pre ren env (anonymous_pre true cphi)).p_value in + let wf_a_r = Term.applist (constant "well_founded", [a; r]) in + + let before = current_date ren in + let ren' = next ren (get_writes ef) in + let al = current_vars ren' (get_writes ef) in + let v = + let _,lo = input_output ren env c in + let is = abstract_post ren' env (ef,is) in + match i with + | None -> product ren' env before lo is + | Some ci -> + Term.mkArrow (apply_assert ren' env ci).a_value + (product ren' env before lo is) + in + let v = Term.mkArrow (eq a (mkVar id_phi) (phi_of ren')) v in + let v = + n_mkNamedProd v + (List.map (fun (id,id') -> (id',trad_type_in_env ren env id)) al) + in + let tw = + Term.mkNamedProd id_phi a + (Term.mkArrow (lt r (mkVar id_phi) (mkVar id_phi0)) v) + in + let id_w = id_of_string "loop" in + let vars = List.rev (current_vars ren (get_writes ef)) in + let body = + make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) + in + CC_app (CC_expr (constant "well_founded_induction"), + [CC_expr a; CC_expr r; + CC_hole wf_a_r; + CC_expr (Term.mkNamedLambda id_phi a v); + CC_lam ([id_phi0, CC_typed_binder a; + id_w, CC_typed_binder tw], + body); + CC_expr (phi_of ren)] + @(List.map (fun (_,id) -> CC_var id) vars) + @(CC_hole (eq a (phi_of ren) (phi_of ren))) + ::(match i with + | None -> [] + | Some c -> [CC_hole (apply_assert ren env c).a_value])) + + +(* [make_letrec ren env (phi0,(cphi,r,a)) bl (te,ce) c] + * constructs the term corresponding to the let rec i.e. + * + * [x][h:P(x)](well_founded_induction + * A R ?::(well_founded A R) + * [Phi:A] (bl) (x) Phi=phi(x)->(P x)-> \exists x'.res.(Q x x') + * [Phi_0:A][w:(Phi:A)(Phi<Phi_0)-> ...] + * [bl][x][eq:Phi_0=phi(x)][h:(P x)]te + * phi(x) bl x ? ?) + *) + +let make_letrec ren env (id_phi0,(cphi,r,a)) idf bl (te,ce) c = + let (_,ef,p,q) = c in + let phi_of ren = (apply_pre ren env (anonymous_pre true cphi)).p_value in + let wf_a_r = Term.applist (constant "well_founded", [a; r]) in + + let before = current_date ren in + let al = current_vars ren (get_reads ef) in + let v = + let _,lo = input_output ren env c in + let q = abstract_post ren env (ef,q) in + arrow ren env (product ren env (current_date ren) lo q) p + in + let v = Term.mkArrow (eq a (mkVar id_phi) (phi_of ren)) v in + let v = + n_mkNamedProd v + (List.map (fun (id,id') -> (id',trad_type_in_env ren env id)) al) + in + let v = + n_mkNamedProd v + (List.map (function (id,CC_typed_binder c) -> (id,c) + | _ -> assert false) (List.rev bl)) + in + let tw = + Term.mkNamedProd id_phi a + (Term.mkArrow (lt r (mkVar id_phi) (mkVar id_phi0)) v) + in + let vars = List.rev (current_vars ren (get_reads ef)) in + let body = + let al = current_vars ren (get_reads ef) in + let bod = abs_pre ren env (te,v) p in + let bod = CC_lam ([var_name Anonymous, + CC_typed_binder (eq a (mkVar id_phi0) (phi_of ren))], + bod) + in + let bl' = binding_of_alist ren env al in + make_abs (bl@(List.rev bl')) bod + in + let t = + CC_app (CC_expr (constant "well_founded_induction"), + [CC_expr a; CC_expr r; + CC_hole wf_a_r; + CC_expr (Term.mkNamedLambda id_phi a v); + CC_lam ([id_phi0, CC_typed_binder a; + idf, CC_typed_binder tw], + body); + CC_expr (phi_of ren)] + @(List.map (fun (id,_) -> CC_var id) bl) + @(List.map (fun (_,id) -> CC_var id) vars) + @[CC_hole (eq a (phi_of ren) (phi_of ren))] + ) + in + (* on abstrait juste par rapport aux variables de ef *) + let al = current_vars ren (get_reads ef) in + let bl = binding_of_alist ren env al in + make_abs (List.rev bl) t + + +(* [make_access env id c] Access in array id. + * + * Constructs [t:(array s T)](access_g s T t c ?::(lt c s)). + *) + +let array_info ren env id = + let ty = type_in_env env id in + let size,v = dearray_type ty in + let ty_elem = trad_ml_type_v ren env v in + let ty_array = trad_imp_type ren env ty in + size,ty_elem,ty_array + +let make_raw_access ren env (id,id') c = + let size,ty_elem,_ = array_info ren env id in + Term.applist (constant "access", [size; ty_elem; mkVar id'; c]) + +let make_pre_access ren env id c = + let size,_,_ = array_info ren env id in + conj (lt (constant "Zle") (constant "ZERO") c) + (lt (constant "Zlt") c size) + +let make_raw_store ren env (id,id') c1 c2 = + let size,ty_elem,_ = array_info ren env id in + Term.applist (constant "store", [size; ty_elem; mkVar id'; c1; c2]) diff --git a/contrib/correctness/pmonad.mli b/contrib/correctness/pmonad.mli new file mode 100644 index 00000000..e1400fcb --- /dev/null +++ b/contrib/correctness/pmonad.mli @@ -0,0 +1,106 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pmonad.mli,v 1.1.16.1 2004/07/16 19:30:02 herbelin Exp $ *) + +open Names +open Term + +open Ptype +open Past +open Penv + +(* Main part of the translation of imperative programs into functional ones + * (with mlise.ml) *) + +(* Here we translate the specification into a CIC specification *) + +val trad_ml_type_v : Prename.t -> local_env -> type_v -> constr +val trad_ml_type_c : Prename.t -> local_env -> type_c -> constr +val trad_imp_type : Prename.t -> local_env -> type_v -> constr +val trad_type_in_env : Prename.t -> local_env -> identifier -> constr + +val binding_of_alist : Prename.t -> local_env + -> (identifier * identifier) list + -> cc_binder list +val make_abs : cc_binder list -> cc_term -> cc_term +val abs_pre : Prename.t -> local_env -> cc_term * constr -> + constr precondition list -> cc_term + +(* The following functions translate the main constructions *) + +val make_tuple : (cc_term * cc_type) list -> predicate option + -> Prename.t -> local_env -> string + -> cc_term + +val result_tuple : Prename.t -> string -> local_env + -> (cc_term * constr) -> (Peffect.t * predicate option) + -> cc_term * constr + +val let_in_pre : constr -> constr precondition -> cc_term -> cc_term + +val make_let_in : Prename.t -> local_env -> cc_term + -> constr precondition list + -> ((identifier * identifier) list * predicate option) + -> identifier * constr + -> cc_term * constr -> cc_term + +val make_block : Prename.t -> local_env + -> (Prename.t -> (identifier * constr) option -> cc_term * constr) + -> (cc_term * type_c, constr) block + -> cc_term + +val make_app : local_env + -> Prename.t -> (cc_term * type_c) list + -> Prename.t -> cc_term * type_c + -> ((type_v binder list) * type_c) + * ((identifier*identifier) list) + * type_c + -> type_c + -> cc_term + +val make_if : Prename.t -> local_env + -> cc_term * type_c + -> Prename.t + -> cc_term * type_c + -> cc_term * type_c + -> type_c + -> cc_term + +val make_while : Prename.t -> local_env + -> (constr * constr * constr) (* typed variant *) + -> cc_term * type_c + -> (cc_term * type_c, constr) block + -> constr assertion option * type_c + -> cc_term + +val make_letrec : Prename.t -> local_env + -> (identifier * (constr * constr * constr)) (* typed variant *) + -> identifier (* the name of the function *) + -> (cc_binder list) + -> (cc_term * type_c) + -> type_c + -> cc_term + +(* Functions to translate array operations *) + +val array_info : + Prename.t -> local_env -> identifier -> constr * constr * constr + +val make_raw_access : + Prename.t -> local_env -> identifier * identifier -> constr -> constr + +val make_raw_store : + Prename.t -> local_env -> identifier * identifier + -> constr -> constr -> constr + +val make_pre_access : + Prename.t -> local_env -> identifier -> constr -> constr + diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml new file mode 100644 index 00000000..732dcf08 --- /dev/null +++ b/contrib/correctness/pred.ml @@ -0,0 +1,115 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pred.ml,v 1.6.14.1 2004/07/16 19:30:05 herbelin Exp $ *) + +open Pp +open Past +open Pmisc + +let rec cc_subst subst = function + | CC_var id as c -> + (try CC_expr (List.assoc id subst) with Not_found -> c) + | CC_letin (b,ty,bl,c1,c2) -> + CC_letin (b, real_subst_in_constr subst ty, cc_subst_binders subst bl, + cc_subst subst c1, cc_subst (cc_cross_binders subst bl) c2) + | CC_lam (bl, c) -> + CC_lam (cc_subst_binders subst bl, + cc_subst (cc_cross_binders subst bl) c) + | CC_app (c, cl) -> + CC_app (cc_subst subst c, List.map (cc_subst subst) cl) + | CC_tuple (b, tl, cl) -> + CC_tuple (b, List.map (real_subst_in_constr subst) tl, + List.map (cc_subst subst) cl) + | CC_case (ty, c, cl) -> + CC_case (real_subst_in_constr subst ty, cc_subst subst c, + List.map (cc_subst subst) cl) + | CC_expr c -> + CC_expr (real_subst_in_constr subst c) + | CC_hole ty -> + CC_hole (real_subst_in_constr subst ty) + +and cc_subst_binders subst = List.map (cc_subst_binder subst) + +and cc_subst_binder subst = function + | id,CC_typed_binder c -> id,CC_typed_binder (real_subst_in_constr subst c) + | b -> b + +and cc_cross_binders subst = function + | [] -> subst + | (id,_) :: bl -> cc_cross_binders (List.remove_assoc id subst) bl + +(* here we only perform eta-reductions on programs to eliminate + * redexes of the kind + * + * let (x1,...,xn) = e in (x1,...,xn) --> e + * + *) + +let is_eta_redex bl al = + try + List.for_all2 + (fun (id,_) t -> match t with CC_var id' -> id=id' | _ -> false) + bl al + with + Invalid_argument("List.for_all2") -> false + +let rec red = function + | CC_letin (_, _, [id,_], CC_expr c1, e2) -> + red (cc_subst [id,c1] e2) + | CC_letin (dep, ty, bl, e1, e2) -> + begin match red e2 with + | CC_tuple (false,tl,al) -> + if is_eta_redex bl al then + red e1 + else + CC_letin (dep, ty, bl, red e1, + CC_tuple (false,tl,List.map red al)) + | e -> CC_letin (dep, ty, bl, red e1, e) + end + | CC_lam (bl, e) -> + CC_lam (bl, red e) + | CC_app (e, al) -> + CC_app (red e, List.map red al) + | CC_case (ty, e1, el) -> + CC_case (ty, red e1, List.map red el) + | CC_tuple (dep, tl, al) -> + CC_tuple (dep, tl, List.map red al) + | e -> e + + +(* How to reduce uncomplete proof terms when they have become constr *) + +open Term +open Reductionops + +(* Il ne faut pas reduire de redexe (beta/iota) qui impliquerait + * la substitution d'une métavariable. + * + * On commence par rendre toutes les applications binaire (strong bin_app) + * puis on applique la reduction spéciale programmes définie dans + * typing/reduction *) + +(*i +let bin_app = function + | DOPN(AppL,v) as c -> + (match Array.length v with + | 1 -> v.(0) + | 2 -> c + | n -> + let f = DOPN(AppL,Array.sub v 0 (pred n)) in + DOPN(AppL,[|f;v.(pred n)|])) + | c -> c +i*) + +let red_cci c = + (*i let c = strong bin_app c in i*) + strong whd_programs (Global.env ()) Evd.empty c + diff --git a/contrib/correctness/pred.mli b/contrib/correctness/pred.mli new file mode 100644 index 00000000..2f43f4ad --- /dev/null +++ b/contrib/correctness/pred.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pred.mli,v 1.1.16.1 2004/07/16 19:30:05 herbelin Exp $ *) + +open Term +open Past + +(* reduction on intermediate programs + * get rid of redexes of the kind let (x1,...,xn) = e in (x1,...,xn) *) + +val red : cc_term -> cc_term + + +(* Ad-hoc reduction on partial proof terms *) + +val red_cci : constr -> constr + + diff --git a/contrib/correctness/prename.ml b/contrib/correctness/prename.ml new file mode 100644 index 00000000..864f6abd --- /dev/null +++ b/contrib/correctness/prename.ml @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: prename.ml,v 1.3.14.1 2004/07/16 19:30:05 herbelin Exp $ *) + +open Names +open Nameops +open Util +open Pp +open Himsg +open Pmisc + +(* Variables names management *) + +type date = string + +(* The following data structure keeps the successive names of the variables + * as we traverse the program. A each step a ``date'' and a + * collection of new names is (possibly) given, and updates the + * previous renaming. + * + * Then, we can ask for the name of a variable, at current date or + * at a given date. + * + * It is easily represented by a list of date x assoc list, most recent coming + * first i.e. as follows: + * + * [ date (= current), [ (x,xi); ... ]; + * date , [ (z,zk); ... ]; + * ... + * date (= initial), [ (x,xj); (y,yi); ... ] + * + * We also keep a list of all names already introduced, in order to + * quickly get fresh names. + *) + +type t = + { levels : (date * (identifier * identifier) list) list; + avoid : identifier list; + cpt : int } + + +let empty_ren = { levels = []; avoid = []; cpt = 0 } + +let update r d ids = + let al,av = renaming_of_ids r.avoid ids in + { levels = (d,al) :: r.levels; avoid = av; cpt = r.cpt } + +let push_date r d = update r d [] + +let next r ids = + let al,av = renaming_of_ids r.avoid ids in + let n = succ r.cpt in + let d = string_of_int n in + { levels = (d,al) :: r.levels; avoid = av; cpt = n } + + +let find r x = + let rec find_in_one = function + [] -> raise Not_found + | (y,v)::rem -> if y = x then v else find_in_one rem + in + let rec find_in_all = function + [] -> raise Not_found + | (_,l)::rem -> try find_in_one l with Not_found -> find_in_all rem + in + find_in_all r.levels + + +let current_var = find + +let current_vars r ids = List.map (fun id -> id,current_var r id) ids + + +let avoid r ids = { levels = r.levels; avoid = r.avoid @ ids; cpt = r.cpt } + +let fresh r ids = fst (renaming_of_ids r.avoid ids) + + +let current_date r = + match r.levels with + [] -> invalid_arg "Renamings.current_date" + | (d,_)::_ -> d + +let all_dates r = List.map fst r.levels + +let rec valid_date da r = + let rec valid = function + [] -> false + | (d,_)::rem -> (d=da) or (valid rem) + in + valid r.levels + +(* [until d r] selects the part of the renaming [r] starting from date [d] *) +let rec until da r = + let rec cut = function + [] -> invalid_arg "Renamings.until" + | (d,_)::rem as r -> if d=da then r else cut rem + in + { avoid = r.avoid; levels = cut r.levels; cpt = r.cpt } + +let var_at_date r d id = + try + find (until d r) id + with Not_found -> + raise (UserError ("Renamings.var_at_date", + hov 0 (str"Variable " ++ pr_id id ++ str" is unknown" ++ spc () ++ + str"at date " ++ str d))) + +let vars_at_date r d ids = + let r' = until d r in List.map (fun id -> id,find r' id) ids + + +(* pretty-printers *) + +open Pp +open Util +open Himsg + +let pp r = + hov 2 (prlist_with_sep (fun () -> (fnl ())) + (fun (d,l) -> + (str d ++ str": " ++ + prlist_with_sep (fun () -> (spc ())) + (fun (id,id') -> + (str"(" ++ pr_id id ++ str"," ++ pr_id id' ++ str")")) + l)) + r.levels) + +let ppr e = + Pp.pp (pp e) + diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli new file mode 100644 index 00000000..88b49d2c --- /dev/null +++ b/contrib/correctness/prename.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: prename.mli,v 1.1.16.1 2004/07/16 19:30:05 herbelin Exp $ *) + +open Names + +(* Abstract type for renamings + * + * Records the names of the mutables objets (ref, arrays) at the different + * moments of the evaluation, called dates + *) + +type t + +type date = string + + +val empty_ren : t +val update : t -> date -> identifier list -> t + (* assign new names for the given variables, associated to a new date *) +val next : t -> identifier list -> t + (* assign new names for the given variables, associated to a new + * date which is generated from an internal counter *) +val push_date : t -> date -> t + (* put a new date on top of the stack *) + +val valid_date : date -> t -> bool +val current_date : t -> date +val all_dates : t -> date list + +val current_var : t -> identifier -> identifier +val current_vars : t -> identifier list -> (identifier * identifier) list + (* gives the current names of some variables *) + +val avoid : t -> identifier list -> t +val fresh : t -> identifier list -> (identifier * identifier) list + (* introduces new names to avoid and renames some given variables *) + +val var_at_date : t -> date -> identifier -> identifier + (* gives the name of a variable at a given date *) +val vars_at_date : t -> date -> identifier list + -> (identifier * identifier) list + (* idem for a list of variables *) + +(* pretty-printers *) + +val pp : t -> Pp.std_ppcmds +val ppr : t -> unit + diff --git a/contrib/correctness/preuves.v b/contrib/correctness/preuves.v new file mode 100644 index 00000000..33659b43 --- /dev/null +++ b/contrib/correctness/preuves.v @@ -0,0 +1,128 @@ + +(* Quelques preuves sur des programmes simples, + * juste histoire d'avoir un petit bench. + *) + +Require Correctness. +Require Omega. + +Global Variable x : Z ref. +Global Variable y : Z ref. +Global Variable z : Z ref. +Global Variable i : Z ref. +Global Variable j : Z ref. +Global Variable n : Z ref. +Global Variable m : Z ref. +Variable r : Z. +Variable N : Z. +Global Variable t : array N of Z. + +(**********************************************************************) + +Require Exchange. +Require ArrayPermut. + +Correctness swap + fun (N:Z)(t:array N of Z)(i,j:Z) -> + { `0 <= i < N` /\ `0 <= j < N` } + (let v = t[i] in + begin + t[i] := t[j]; + t[j] := v + end) + { (exchange t t@ i j) }. +Proof. +Auto with datatypes. +Save. + +Correctness downheap + let rec downheap (N:Z)(t:array N of Z) : unit { variant `0` } = + (swap N t 0 0) { True } +. + +(**********************************************************************) + +Global Variable x : Z ref. +Debug on. +Correctness assign0 (x := 0) { `x=0` }. +Save. + +(**********************************************************************) + +Global Variable i : Z ref. +Debug on. +Correctness assign1 { `0 <= i` } (i := !i + 1) { `0 < i` }. +Omega. +Save. + +(**********************************************************************) + +Global Variable i : Z ref. +Debug on. +Correctness if0 { `0 <= i` } (if !i>0 then i:=!i-1 else tt) { `0 <= i` }. +Omega. +Save. + +(**********************************************************************) + +Global Variable i : Z ref. +Debug on. +Correctness assert0 { `0 <= i` } begin assert { `i=2` }; i:=!i-1 end { `i=1` }. + +(**********************************************************************) + +Correctness echange + { `0 <= i < N` /\ `0 <= j < N` } + begin + label B; + x := t[!i]; t[!i] := t[!j]; t[!j] := !x; + assert { #t[i] = #t@B[j] /\ #t[j] = #t@B[i] } + end. +Proof. +Auto with datatypes. +Save. + + +(**********************************************************************) + +(* + * while x <= y do x := x+1 done { y < x } + *) + +Correctness incrementation + while !x < !y do + { invariant True variant `(Zs y)-x` } + x := !x + 1 + done + { `y < x` }. +Proof. +Exact (Zwf_well_founded `0`). +Unfold Zwf. Omega. +Exact I. +Save. + + +(************************************************************************) + +Correctness pivot1 + begin + while (Z_lt_ge_dec !i r) do + { invariant True variant (Zminus (Zs r) i) } i := (Zs !i) + done; + while (Z_lt_ge_dec r !j) do + { invariant True variant (Zminus (Zs j) r) } j := (Zpred !j) + done + end + { `j <= r` /\ `r <= i` }. +Proof. +Exact (Zwf_well_founded `0`). +Unfold Zwf. Omega. +Exact I. +Exact (Zwf_well_founded `0`). +Unfold Zwf. Unfold Zpred. Omega. +Exact I. +Omega. +Save. + + + diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 new file mode 100644 index 00000000..c1f00a3d --- /dev/null +++ b/contrib/correctness/psyntax.ml4 @@ -0,0 +1,1058 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: psyntax.ml4,v 1.29.2.1 2004/07/16 19:30:05 herbelin Exp $ *) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +open Options +open Util +open Names +open Nameops +open Vernacentries +open Reduction +open Term +open Libnames +open Topconstr + +open Prename +open Pmisc +open Putil +open Ptype +open Past +open Penv +open Pmonad +open Vernacexpr + + +(* We define new entries for programs, with the use of this module + * Programs. These entries are named Programs.<foo> + *) + +module Gram = Pcoq.Gram +module Constr = Pcoq.Constr +module Tactic = Pcoq.Tactic + +module Programs = + struct + let gec s = Gram.Entry.create ("Programs."^s) + (* types *) + let type_v = gec "type_v" + let type_v0 = gec "type_v0" + let type_v1 = gec "type_v1" + let type_v2 = gec "type_v2" + let type_v3 = gec "type_v3" + let type_v_app = gec "type_v_app" + let type_c = gec "type_c" + let effects = gec "effects" + let reads = gec "reads" + let writes = gec "writes" + let pre_condition = gec "pre_condition" + let post_condition = gec "post_condition" + (* binders *) + let binder = gec "binder" + let binder_type = gec "binder_type" + let binders = gec "binders" + (* programs *) + let program = gec "program" + let prog1 = gec "prog1" + let prog2 = gec "prog2" + let prog3 = gec "prog3" + let prog4 = gec "prog4" + let prog5 = gec "prog5" + let prog6 = gec "prog6" + let prog7 = gec "prog7" + let ast1 = gec "ast1" + let ast2 = gec "ast2" + let ast3 = gec "ast3" + let ast4 = gec "ast4" + let ast5 = gec "ast5" + let ast6 = gec "ast6" + let ast7 = gec "ast7" + let arg = gec "arg" + let block = gec "block" + let block_statement = gec "block_statement" + let relation = gec "relation" + let variable = gec "variable" + let invariant = gec "invariant" + let variant = gec "variant" + let assertion = gec "assertion" + let precondition = gec "precondition" + let postcondition = gec "postcondition" + let predicate = gec "predicate" + let name = gec "name" + end + +open Programs + +let ast_of_int n = + CDelimiters + (dummy_loc, "Z", CNumeral (dummy_loc, Bignat.POS (Bignat.of_string n))) + +let constr_of_int n = + Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n) + +open Util +open Coqast + +let mk_id loc id = mkRefC (Ident (loc, id)) +let mk_ref loc s = mk_id loc (Constrextern.id_of_v7_string s) +let mk_appl loc1 loc2 f args = + CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args) + +let conj_assert {a_name=n;a_value=a} {a_value=b} = + let loc1 = constr_loc a in + let loc2 = constr_loc a in + { a_value = mk_appl loc1 loc2 "and" [a;b]; a_name = n } + +let conj = function + None,None -> None + | None,b -> b + | a,None -> a + | Some a,Some b -> Some (conj_assert a b) + +let without_effect loc d = + { desc = d; pre = []; post = None; loc = loc; info = () } + +let isevar = Expression isevar + +let bin_op op loc e1 e2 = + without_effect loc + (Apply (without_effect loc (Expression (constant op)), + [ Term e1; Term e2 ])) + +let un_op op loc e = + without_effect loc + (Apply (without_effect loc (Expression (constant op)), [Term e])) + +let bool_bin op loc a1 a2 = + let w = without_effect loc in + let d = SApp ( [Variable op], [a1; a2]) in + w d + +let bool_or loc = bool_bin connective_or loc +let bool_and loc = bool_bin connective_and loc + +let bool_not loc a = + let w = without_effect loc in + let d = SApp ( [Variable connective_not ], [a]) in + w d + +let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "ZERO"] + +(* program -> Coq AST *) + +let bdize c = + let env = + Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty) + in + Constrextern.extern_constr true env c + +let rec coqast_of_program loc = function + | Variable id -> mk_id loc id + | Acc id -> mk_id loc id + | Apply (f,l) -> + let f = coqast_of_program f.loc f.desc in + let args = List.map + (function Term t -> (coqast_of_program t.loc t.desc,None) + | _ -> invalid_arg "coqast_of_program") l + in + CApp (dummy_loc, (None,f), args) + | Expression c -> bdize c + | _ -> invalid_arg "coqast_of_program" + +(* The construction `for' is syntactic sugar. + * + * for i = v1 to v2 do { invariant Inv } block done + * + * ==> (let rec f i { variant v2+1-i } = + * { i <= v2+1 /\ Inv(i) } + * (if i > v2 then tt else begin block; (f (i+1)) end) + * { Inv(v2+1) } + * in (f v1)) { Inv(v2+1) } + *) + +let ast_plus_un loc ast = + let un = ast_of_int "1" in + mk_appl loc loc "Zplus" [ast;un] + +let make_ast_for loc i v1 v2 inv block = + let f = for_name() in + let id_i = id_of_string i in + let var_i = without_effect loc (Variable id_i) in + let var_f = without_effect loc (Variable f) in + let succ_v2 = + let a_v2 = coqast_of_program v2.loc v2.desc in + ast_plus_un loc a_v2 in + let post = named_app (subst_ast_in_ast [ id_i, succ_v2 ]) inv in + let e1 = + let test = bin_op "Z_gt_le_bool" loc var_i v2 in + let br_t = without_effect loc (Expression (constant "tt")) in + let br_f = + let un = without_effect loc (Expression (constr_of_int "1")) in + let succ_i = bin_op "Zplus" loc var_i un in + let f_succ_i = without_effect loc (Apply (var_f, [Term succ_i])) in + without_effect loc (Seq (block @ [Statement f_succ_i])) + in + let inv' = + let i_le_sv2 = mk_appl loc loc "Zle" [mk_ref loc i; succ_v2] in + conj_assert {a_value=i_le_sv2;a_name=inv.a_name} inv + in + { desc = If(test,br_t,br_f); loc = loc; + pre = [pre_of_assert false inv']; post = Some post; info = () } + in + let bl = + let typez = mk_ref loc "Z" in + [(id_of_string i, BindType (TypePure typez))] + in + let fv1 = without_effect loc (Apply (var_f, [Term v1])) in + let v = TypePure (mk_ref loc "unit") in + let var = + let a = mk_appl loc loc "Zminus" [succ_v2;mk_ref loc i] in + (a, ast_zwf_zero loc) + in + Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1) + +let mk_prog loc p pre post = + { desc = p.desc; + pre = p.pre @ pre; + post = conj (p.post,post); + loc = loc; + info = () } + +if !Options.v7 then +GEXTEND Gram + + (* Types ******************************************************************) + type_v: + [ [ t = type_v0 -> t ] ] + ; + type_v0: + [ [ t = type_v1 -> t ] ] + ; + type_v1: + [ [ t = type_v2 -> t ] ] + ; + type_v2: + [ LEFTA + [ v = type_v2; IDENT "ref" -> Ref v + | t = type_v3 -> t ] ] + ; + type_v3: + [ [ IDENT "array"; size = Constr.constr; "of"; v = type_v0 -> + Array (size,v) + | IDENT "fun"; bl = binders; c = type_c -> make_arrow bl c + | c = Constr.constr -> TypePure c + ] ] + ; + type_c: + [ [ IDENT "returns"; id = IDENT; ":"; v = type_v; + e = effects; p = OPT pre_condition; q = OPT post_condition; "end" -> + ((id_of_string id, v), e, list_of_some p, q) + ] ] + ; + effects: + [ [ r = OPT reads; w = OPT writes -> + let r' = match r with Some l -> l | _ -> [] in + let w' = match w with Some l -> l | _ -> [] in + List.fold_left (fun e x -> Peffect.add_write x e) + (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r') + w' + ] ] + ; + reads: + [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ] + ; + writes: + [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ] + ; + pre_condition: + [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ] + ; + post_condition: + [ [ IDENT "post"; c = predicate -> c ] ] + ; + + (* Binders (for both types and programs) **********************************) + binder: + [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" -> + List.map (fun s -> (id_of_string s, t)) sl + ] ] + ; + binder_type: + [ [ "Set" -> BindSet + | v = type_v -> BindType v + ] ] + ; + binders: + [ [ bl = LIST0 binder -> List.flatten bl ] ] + ; + + (* annotations *) + predicate: + [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ] + ; + name: + [ [ "as"; s = IDENT -> Name (id_of_string s) + | -> Anonymous + ] ] + ; + + (* Programs ***************************************************************) + variable: + [ [ s = IDENT -> id_of_string s ] ] + ; + assertion: + [ [ "{"; c = predicate; "}" -> c ] ] + ; + precondition: + [ [ "{"; c = predicate; "}" -> pre_of_assert false c ] ] + ; + postcondition: + [ [ "{"; c = predicate; "}" -> c ] ] + ; + program: + [ [ p = prog1 -> p ] ] + ; + prog1: + [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog2: + [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog3: + [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog4: + [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog5: + [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog6: + [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + + ast1: + [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y + | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y + | x = prog2 -> x + ] ] + ; + ast2: + [ [ IDENT "not"; x = prog3 -> bool_not loc x + | x = prog3 -> x + ] ] + ; + ast3: + [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y + | x = prog4 -> x + ] ] + ; + ast4: + [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y + | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y + | x = prog5 -> x + ] ] + ; + ast5: + [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y + | x = prog6 -> x + ] ] + ; + ast6: + [ [ "-"; x = prog6 -> un_op "Zopp" loc x + | x = ast7 -> without_effect loc x + ] ] + ; + ast7: + [ [ v = variable -> + Variable v + | n = INT -> + Expression (constr_of_int n) + | "!"; v = variable -> + Acc v + | "?" -> + isevar + | v = variable; ":="; p = program -> + Aff (v,p) + | v = variable; "["; e = program; "]" -> TabAcc (true,v,e) + | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e) + | v = variable; "["; e = program; "]"; ":="; p = program -> + TabAff (true,v,e,p) + | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> + TabAff (true,v,e,p) + | IDENT "if"; e1 = program; IDENT "then"; e2 = program; + IDENT "else"; e3 = program -> + If (e1,e2,e3) + | IDENT "if"; e1 = program; IDENT "then"; e2 = program -> + If (e1,e2,without_effect loc (Expression (constant "tt"))) + | IDENT "while"; b = program; IDENT "do"; + "{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}"; + bl = block; IDENT "done" -> + While (b, inv, wf, bl) + | IDENT "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program; + IDENT "do"; "{"; inv = invariant; "}"; + bl = block; IDENT "done" -> + make_ast_for loc i v1 v2 inv bl + | IDENT "let"; v = variable; "="; IDENT "ref"; p1 = program; + "in"; p2 = program -> + LetRef (v, p1, p2) + | IDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program -> + Let (v, p1, p2) + | IDENT "begin"; b = block; "end" -> + Seq b + | IDENT "fun"; bl = binders; "->"; p = program -> + Lam (bl,p) + | IDENT "let"; IDENT "rec"; f = variable; + bl = binders; ":"; v = type_v; + "{"; IDENT "variant"; var = variant; "}"; "="; p = program -> + LetRec (f,bl,v,var,p) + | IDENT "let"; IDENT "rec"; f = variable; + bl = binders; ":"; v = type_v; + "{"; IDENT "variant"; var = variant; "}"; "="; p = program; + "in"; p2 = program -> + Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2) + + | "@"; s = STRING; p = program -> + Debug (s,p) + + | "("; p = program; args = LIST0 arg; ")" -> + match args with + [] -> + if p.pre<>[] or p.post<>None then + Pp.warning "Some annotations are lost"; + p.desc + | _ -> + Apply(p,args) + ] ] + ; + arg: + [ [ "'"; t = type_v -> Type t + | p = program -> Term p + ] ] + ; + block: + [ [ s = block_statement; ";"; b = block -> s::b + | s = block_statement -> [s] ] ] + ; + block_statement: + [ [ IDENT "label"; s = IDENT -> Label s + | IDENT "assert"; c = assertion -> Assert c + | p = program -> Statement p ] ] + ; + relation: + [ [ "<" -> "Z_lt_ge_bool" + | "<=" -> "Z_le_gt_bool" + | ">" -> "Z_gt_le_bool" + | ">=" -> "Z_ge_lt_bool" + | "=" -> "Z_eq_bool" + | "<>" -> "Z_noteq_bool" ] ] + ; + + (* Other entries (invariants, etc.) ***************************************) + invariant: + [ [ IDENT "invariant"; c = predicate -> c ] ] + ; + variant: + [ [ c = Constr.constr; IDENT "for"; r = Constr.constr -> (c, r) + | c = Constr.constr -> (c, ast_zwf_zero loc) ] ] + ; + END +else +GEXTEND Gram + GLOBAL: type_v program; + + (* Types ******************************************************************) + type_v: + [ [ t = type_v0 -> t ] ] + ; + type_v0: + [ [ t = type_v1 -> t ] ] + ; + type_v1: + [ [ t = type_v2 -> t ] ] + ; + type_v2: + [ LEFTA + [ v = type_v2; IDENT "ref" -> Ref v + | t = type_v3 -> t ] ] + ; + type_v3: + [ [ IDENT "array"; size = Constr.constr; IDENT "of"; v = type_v0 -> + Array (size,v) + | "fun"; bl = binders; c = type_c -> make_arrow bl c + | c = Constr.constr -> TypePure c + ] ] + ; + type_c: + [ [ IDENT "returns"; id = IDENT; ":"; v = type_v; + e = effects; p = OPT pre_condition; q = OPT post_condition; "end" -> + ((id_of_string id, v), e, list_of_some p, q) + ] ] + ; + effects: + [ [ r = OPT reads; w = OPT writes -> + let r' = match r with Some l -> l | _ -> [] in + let w' = match w with Some l -> l | _ -> [] in + List.fold_left (fun e x -> Peffect.add_write x e) + (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r') + w' + ] ] + ; + reads: + [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ] + ; + writes: + [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ] + ; + pre_condition: + [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ] + ; + post_condition: + [ [ IDENT "post"; c = predicate -> c ] ] + ; + + (* Binders (for both types and programs) **********************************) + binder: + [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" -> + List.map (fun s -> (id_of_string s, t)) sl + ] ] + ; + binder_type: + [ [ "Set" -> BindSet + | v = type_v -> BindType v + ] ] + ; + binders: + [ [ bl = LIST0 binder -> List.flatten bl ] ] + ; + + (* annotations *) + predicate: + [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ] + ; + dpredicate: + [ [ c = Constr.lconstr; n = name -> { a_name = n; a_value = c } ] ] + ; + name: + [ [ "as"; s = IDENT -> Name (id_of_string s) + | -> Anonymous + ] ] + ; + + (* Programs ***************************************************************) + variable: + [ [ s = IDENT -> id_of_string s ] ] + ; + assertion: + [ [ "{"; c = dpredicate; "}" -> c ] ] + ; + precondition: + [ [ "{"; c = dpredicate; "}" -> pre_of_assert false c ] ] + ; + postcondition: + [ [ "{"; c = dpredicate; "}" -> c ] ] + ; + program: + [ [ p = prog1 -> p ] ] + ; + prog1: + [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog2: + [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog3: + [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog4: + [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog5: + [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + prog6: + [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition -> + mk_prog loc ast pre post ] ] + ; + + ast1: + [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y + | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y + | x = prog2 -> x + ] ] + ; + ast2: + [ [ IDENT "not"; x = prog3 -> bool_not loc x + | x = prog3 -> x + ] ] + ; + ast3: + [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y + | x = prog4 -> x + ] ] + ; + ast4: + [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y + | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y + | x = prog5 -> x + ] ] + ; + ast5: + [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y + | x = prog6 -> x + ] ] + ; + ast6: + [ [ "-"; x = prog6 -> un_op "Zopp" loc x + | x = ast7 -> without_effect loc x + ] ] + ; + ast7: + [ [ v = variable -> + Variable v + | n = INT -> + Expression (constr_of_int n) + | "!"; v = variable -> + Acc v + | "?" -> + isevar + | v = variable; ":="; p = program -> + Aff (v,p) + | v = variable; "["; e = program; "]" -> TabAcc (true,v,e) + | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e) + | v = variable; "["; e = program; "]"; ":="; p = program -> + TabAff (true,v,e,p) + | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> + TabAff (true,v,e,p) + | "if"; e1 = program; "then"; e2 = program; "else"; e3 = program -> + If (e1,e2,e3) + | "if"; e1 = program; "then"; e2 = program -> + If (e1,e2,without_effect loc (Expression (constant "tt"))) + | IDENT "while"; b = program; IDENT "do"; + "{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}"; + bl = block; IDENT "done" -> + While (b, inv, wf, bl) + | "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program; + IDENT "do"; "{"; inv = invariant; "}"; + bl = block; IDENT "done" -> + make_ast_for loc i v1 v2 inv bl + | "let"; v = variable; "="; IDENT "ref"; p1 = program; + "in"; p2 = program -> + LetRef (v, p1, p2) + | "let"; v = variable; "="; p1 = program; "in"; p2 = program -> + Let (v, p1, p2) + | IDENT "begin"; b = block; "end" -> + Seq b + | "fun"; bl = binders; "=>"; p = program -> + Lam (bl,p) + | "let"; IDENT "rec"; f = variable; + bl = binders; ":"; v = type_v; + "{"; IDENT "variant"; var = variant; "}"; "="; p = program -> + LetRec (f,bl,v,var,p) + | "let"; IDENT "rec"; f = variable; + bl = binders; ":"; v = type_v; + "{"; IDENT "variant"; var = variant; "}"; "="; p = program; + "in"; p2 = program -> + Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2) + + | "@"; s = STRING; p = program -> + Debug (s,p) + + | "("; p = program; args = LIST0 arg; ")" -> + match args with + [] -> + if p.pre<>[] or p.post<>None then + Pp.warning "Some annotations are lost"; + p.desc + | _ -> + Apply(p,args) + ] ] + ; + arg: + [ [ "'"; t = type_v -> Type t + | p = program -> Term p + ] ] + ; + block: + [ [ s = block_statement; ";"; b = block -> s::b + | s = block_statement -> [s] ] ] + ; + block_statement: + [ [ IDENT "label"; s = IDENT -> Label s + | IDENT "assert"; c = assertion -> Assert c + | p = program -> Statement p ] ] + ; + relation: + [ [ "<" -> "Z_lt_ge_bool" + | "<=" -> "Z_le_gt_bool" + | ">" -> "Z_gt_le_bool" + | ">=" -> "Z_ge_lt_bool" + | "=" -> "Z_eq_bool" + | "<>" -> "Z_noteq_bool" ] ] + ; + + (* Other entries (invariants, etc.) ***************************************) + invariant: + [ [ IDENT "invariant"; c = predicate -> c ] ] + ; + variant: + [ [ c = Constr.constr; "for"; r = Constr.constr -> (c, r) + | c = Constr.constr -> (c, ast_zwf_zero loc) ] ] + ; + END +;; + +let wit_program, globwit_program, rawwit_program = + Genarg.create_arg "program" +let wit_type_v, globwit_type_v, rawwit_type_v = + Genarg.create_arg "type_v" + +open Pp +open Util +open Himsg +open Vernacinterp +open Vernacexpr +open Declare + +let is_assumed global ids = + if List.length ids = 1 then + msgnl (str (if global then "A global variable " else "") ++ + pr_id (List.hd ids) ++ str " is assumed") + else + msgnl (str (if global then "Some global variables " else "") ++ + prlist_with_sep (fun () -> (str ", ")) pr_id ids ++ + str " are assumed") + +open Pcoq + +(* Variables *) + +let wit_variables, globwit_variables, rawwit_variables = + Genarg.create_arg "variables" + +let variables = Gram.Entry.create "Variables" + +GEXTEND Gram + variables: [ [ l = LIST1 Prim.ident SEP "," -> l ] ]; +END + +let pr_variables _prc _prtac l = spc() ++ prlist_with_sep pr_coma pr_id l + +let _ = + Pptactic.declare_extra_genarg_pprule true + (rawwit_variables, pr_variables) + (globwit_variables, pr_variables) + (wit_variables, pr_variables) + +(* then_tac *) + +open Genarg +open Tacinterp + +let pr_then_tac _ prt = function + | None -> mt () + | Some t -> pr_semicolon () ++ prt t + +ARGUMENT EXTEND then_tac + TYPED AS tactic_opt + PRINTED BY pr_then_tac + INTERPRETED BY interp_genarg + GLOBALIZED BY intern_genarg +| [ ";" tactic(t) ] -> [ Some t ] +| [ ] -> [ None ] +END + +(* Correctness *) + +VERNAC COMMAND EXTEND Correctness + [ "Correctness" preident(str) program(pgm) then_tac(tac) ] + -> [ Ptactic.correctness str pgm (option_app Tacinterp.interp tac) ] +END + +(* Show Programs *) + +let show_programs () = + fold_all + (fun (id,v) _ -> + msgnl (pr_id id ++ str " : " ++ + hov 2 (match v with TypeV v -> pp_type_v v + | Set -> (str "Set")) ++ + fnl ())) + Penv.empty () + +VERNAC COMMAND EXTEND ShowPrograms + [ "Show" "Programs" ] -> [ show_programs () ] +END + +(* Global Variable *) + +let global_variable ids v = + List.iter + (fun id -> if Penv.is_global id then + Util.errorlabstrm "PROGVARIABLE" + (str"Clash with previous constant " ++ pr_id id)) + ids; + Pdb.check_type_v (all_refs ()) v; + let env = empty in + let ren = update empty_ren "" [] in + let v = Ptyping.cic_type_v env ren v in + if not (is_mutable v) then begin + let c = + Entries.ParameterEntry (trad_ml_type_v ren env v), + Decl_kinds.IsAssumption Decl_kinds.Definitional in + List.iter + (fun id -> ignore (Declare.declare_constant id c)) ids; + if_verbose (is_assumed false) ids + end; + if not (is_pure v) then begin + List.iter (fun id -> ignore (Penv.add_global id v None)) ids; + if_verbose (is_assumed true) ids + end + +VERNAC COMMAND EXTEND ProgVariable + [ "Global" "Variable" variables(ids) ":" type_v(t) ] + -> [ global_variable ids t] +END + +let pr_id id = pr_id (Constrextern.v7_to_v8_id id) + +(* Type printer *) + +let pr_reads = function + | [] -> mt () + | l -> spc () ++ + hov 0 (str "reads" ++ spc () ++ prlist_with_sep pr_coma pr_id l) + +let pr_writes = function + | [] -> mt () + | l -> spc () ++ + hov 0 (str "writes" ++ spc () ++ prlist_with_sep pr_coma pr_id l) + +let pr_effects x = + let (ro,rw) = Peffect.get_repr x in pr_reads ro ++ pr_writes rw + +let pr_predicate delimited { a_name = n; a_value = c } = + (if delimited then Ppconstrnew.pr_lconstr else Ppconstrnew.pr_constr) c ++ + (match n with Name id -> spc () ++ str "as " ++ pr_id id | Anonymous -> mt()) + +let pr_assert b { p_name = x; p_value = v } = + pr_predicate b { a_name = x; a_value = v } + +let pr_pre_condition_list = function + | [] -> mt () + | [pre] -> spc() ++ hov 0 (str "pre" ++ spc () ++ pr_assert false pre) + | _ -> assert false + +let pr_post_condition_opt = function + | None -> mt () + | Some post -> + spc() ++ hov 0 (str "post" ++ spc () ++ pr_predicate false post) + +let rec pr_type_v_v8 = function + | Array (a,v) -> + str "array" ++ spc() ++ Ppconstrnew.pr_constr a ++ spc() ++ str "of " ++ + pr_type_v_v8 v + | v -> pr_type_v3 v + +and pr_type_v3 = function + | Ref v -> pr_type_v3 v ++ spc () ++ str "ref" + | Arrow (bl,((id,v),e,prel,postl)) -> + str "fun" ++ spc() ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ + spc () ++ str "returns" ++ spc () ++ pr_id id ++ str ":" ++ + pr_type_v_v8 v ++ pr_effects e ++ + pr_pre_condition_list prel ++ pr_post_condition_opt postl ++ + spc () ++ str "end" + | TypePure a -> Ppconstrnew.pr_constr a + | v -> str "(" ++ pr_type_v_v8 v ++ str ")" + +and pr_binder = function + | (id,BindType c) -> + str "(" ++ pr_id id ++ str ":" ++ pr_type_v_v8 c ++ str ")" + | (id,BindSet) -> + str "(" ++ pr_id id ++ str ":" ++ str "Set" ++ str ")" + | (id,Untyped) -> + str "<<<<< TODO: Untyped binder >>>>" + +let _ = + Pptactic.declare_extra_genarg_pprule true + (rawwit_type_v, fun _ _ -> pr_type_v_v8) + (globwit_type_v, fun _ -> raise Not_found) + (wit_type_v, fun _ -> raise Not_found) + +(* Program printer *) + +let pr_precondition pred = str "{" ++ pr_assert true pred ++ str "}" ++ spc () + +let pr_postcondition pred = str "{" ++ pr_predicate true pred ++ str "}" + +let pr_invariant = function + | None -> mt () + | Some c -> hov 2 (str "invariant" ++ spc () ++ pr_predicate false c) + +let pr_variant (c1,c2) = + Ppconstrnew.pr_constr c1 ++ + (try Constrextern.check_same_type c2 (ast_zwf_zero dummy_loc); mt () + with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstrnew.pr_constr c2)) + +let rec pr_desc = function + | Variable id -> + (* Unsafe: should distinguish global names and bound vars *) + let vars = (* TODO *) Idset.empty in + let id = try + snd (repr_qualid + (snd (qualid_of_reference + (Constrextern.extern_reference + dummy_loc vars (Nametab.locate (make_short_qualid id)))))) + with _ -> id in + pr_id id + | Acc id -> str "!" ++ pr_id id + | Aff (id,p) -> pr_id id ++ spc() ++ str ":=" ++ spc() ++ pr_prog p + | TabAcc (b,id,p) -> pr_id id ++ str "[" ++ pr_prog p ++ str "]" + | TabAff (b,id,p1,p2) -> + pr_id id ++ str "[" ++ pr_prog p1 ++ str "]" ++ + str ":=" ++ pr_prog p2 + | Seq bll -> + hv 0 (str "begin" ++ spc () ++ pr_block bll ++ spc () ++ str "end") + | While (p1,inv,var,bll) -> + hv 0 ( + hov 0 (str "while" ++ spc () ++ pr_prog p1 ++ spc () ++ str "do") ++ + brk (1,2) ++ + hv 2 ( + str "{ " ++ + pr_invariant inv ++ spc() ++ + hov 0 (str "variant" ++ spc () ++ pr_variant var) + ++ str " }") ++ cut () ++ + hov 0 (pr_block bll) ++ cut () ++ + str "done") + | If (p1,p2,p3) -> + hov 1 (str "if " ++ pr_prog p1) ++ spc () ++ + hov 0 (str "then" ++ spc () ++ pr_prog p2) ++ spc () ++ + hov 0 (str "else" ++ spc () ++ pr_prog p3) + | Lam (bl,p) -> + hov 0 + (str "fun" ++ spc () ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ + spc () ++ str "=>") ++ + pr_prog p + | Apply ({desc=Expression e; pre=[]; post=None} as p,args) when isConst e -> + begin match + string_of_id (snd (repr_path (Nametab.sp_of_global (ConstRef (destConst e))))), + args + with + | "Zmult", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"*" ++ pr_arg a2 ++ str ")" + | "Zplus", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"+" ++ pr_arg a2 ++ str ")" + | "Zminus", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"-" ++ pr_arg a2 ++ str ")" + | "Zopp", [a] -> + str "( -" ++ pr_arg a ++ str ")" + | "Z_lt_ge_bool", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"<" ++ pr_arg a2 ++ str ")" + | "Z_le_gt_bool", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"<=" ++ pr_arg a2 ++ str ")" + | "Z_gt_le_bool", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str">" ++ pr_arg a2 ++ str ")" + | "Z_ge_lt_bool", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str">=" ++ pr_arg a2 ++ str ")" + | "Z_eq_bool", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"=" ++ pr_arg a2 ++ str ")" + | "Z_noteq_bool", [a1;a2] -> + str "(" ++ pr_arg a1 ++ str"<> " ++ pr_arg a2 ++ str ")" + | _ -> + str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++ + str ")" + end + | Apply (p,args) -> + str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++ + str ")" + | SApp ([Variable v], args) -> + begin match string_of_id v, args with + | "prog_bool_and", [a1;a2] -> + str"(" ++ pr_prog a1 ++ spc() ++ str"and " ++ pr_prog a2 ++str")" + | "prog_bool_or", [a1;a2] -> + str"(" ++ pr_prog a1 ++ spc() ++ str"or " ++ pr_prog a2 ++ str")" + | "prog_bool_not", [a] -> + str "(not " ++ pr_prog a ++ str ")" + | _ -> failwith "Correctness printer: TODO" + end + | SApp _ -> failwith "Correctness printer: TODO" + | LetRef (v,p1,p2) -> + hov 2 ( + str "let " ++ pr_id v ++ str " =" ++ spc () ++ str "ref" ++ spc () ++ + pr_prog p1 ++ str " in") ++ + spc () ++ pr_prog p2 + | Let (id, {desc=LetRec (f,bl,v,var,p); pre=[]; post=None },p2) when f=id -> + hov 2 ( + str "let rec " ++ pr_id f ++ spc () ++ + hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ + str ":" ++ pr_type_v_v8 v ++ spc () ++ + hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ + spc() ++ str "=" ++ spc () ++ pr_prog p ++ + str " in") ++ + spc () ++ pr_prog p2 + | Let (v,p1,p2) -> + hov 2 ( + str "let " ++ pr_id v ++ str " =" ++ spc () ++ pr_prog p1 ++ str" in") + ++ spc () ++ pr_prog p2 + | LetRec (f,bl,v,var,p) -> + str "let rec " ++ pr_id f ++ spc () ++ + hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ + str ":" ++ pr_type_v_v8 v ++ spc () ++ + hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ + spc () ++ str "=" ++ spc () ++ pr_prog p + | PPoint _ -> str "TODO: Ppoint" (* Internal use only *) + | Expression c -> + (* Numeral or "tt": use a printer which doesn't globalize *) + Ppconstr.pr_constr + (Constrextern.extern_constr_in_scope false "Z_scope" (Global.env()) c) + | Debug (s,p) -> str "@" ++ Pptacticnew.qsnew s ++ pr_prog p + +and pr_block_st = function + | Label s -> hov 0 (str "label" ++ spc() ++ str s) + | Assert pred -> + hov 0 (str "assert" ++ spc() ++ hov 0 (pr_postcondition pred)) + | Statement p -> pr_prog p + +and pr_block bl = prlist_with_sep pr_semicolon pr_block_st bl + +and pr_arg = function + | Past.Term p -> pr_prog p + | Past.Type t -> str "'" ++ pr_type_v_v8 t + | Refarg _ -> str "TODO: Refarg" (* Internal use only *) + +and pr_prog0 b { desc = desc; pre = pre; post = post } = + hv 0 ( + prlist pr_precondition pre ++ + hov 0 + (if b & post<>None then str"(" ++ pr_desc desc ++ str")" + else pr_desc desc) + ++ Ppconstrnew.pr_opt pr_postcondition post) + +and pr_prog x = pr_prog0 true x + +let _ = + Pptactic.declare_extra_genarg_pprule true + (rawwit_program, fun _ _ a -> spc () ++ pr_prog0 false a) + (globwit_program, fun _ -> raise Not_found) + (wit_program, fun _ -> raise Not_found) + diff --git a/contrib/correctness/psyntax.mli b/contrib/correctness/psyntax.mli new file mode 100644 index 00000000..18912548 --- /dev/null +++ b/contrib/correctness/psyntax.mli @@ -0,0 +1,25 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: psyntax.mli,v 1.3.2.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Pcoq +open Ptype +open Past +open Topconstr + +(* Grammar for the programs and the tactic Correctness *) + +module Programs : + sig + val program : program Gram.Entry.e + val type_v : constr_expr ml_type_v Gram.Entry.e + val type_c : constr_expr ml_type_c Gram.Entry.e + end diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml new file mode 100644 index 00000000..4b22954e --- /dev/null +++ b/contrib/correctness/ptactic.ml @@ -0,0 +1,258 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ptactic.ml,v 1.30.2.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Pp +open Options +open Names +open Libnames +open Term +open Pretyping +open Pfedit +open Decl_kinds +open Vernacentries + +open Pmisc +open Putil +open Past +open Penv +open Prename +open Peffect +open Pmonad + +(* [coqast_of_prog: program -> constr * constr] + * Traduction d'un programme impératif en un but (second constr) + * et un terme de preuve partiel pour ce but (premier constr) + *) + +let coqast_of_prog p = + (* 1. db : séparation dB/var/const *) + let p = Pdb.db_prog p in + + (* 2. typage avec effets *) + deb_mess (str"Ptyping.states: Typing with effects..." ++ fnl ()); + let env = Penv.empty in + let ren = initial_renaming env in + let p = Ptyping.states ren env p in + let ((_,v),_,_,_) as c = p.info.kappa in + Perror.check_for_not_mutable p.loc v; + deb_print pp_type_c c; + + (* 3. propagation annotations *) + let p = Pwp.propagate ren p in + + (* 4a. traduction type *) + let ty = Pmonad.trad_ml_type_c ren env c in + deb_print (Printer.prterm_env (Global.env())) ty; + + (* 4b. traduction terme (terme intermédiaire de type cc_term) *) + deb_mess + (fnl () ++ str"Mlize.trad: Translation program -> cc_term..." ++ fnl ()); + let cc = Pmlize.trans ren p in + let cc = Pred.red cc in + deb_print Putil.pp_cc_term cc; + + (* 5. traduction en constr *) + deb_mess + (fnl () ++ str"Pcic.constr_of_prog: Translation cc_term -> rawconstr..." ++ + fnl ()); + let r = Pcic.rawconstr_of_prog cc in + deb_print Printer.pr_rawterm r; + + (* 6. résolution implicites *) + deb_mess (fnl () ++ str"Resolution implicits (? => Meta(n))..." ++ fnl ()); + let oc = understand_gen_tcc Evd.empty (Global.env()) [] None r in + deb_print (Printer.prterm_env (Global.env())) (snd oc); + + p,oc,ty,v + +(* [automatic : tactic] + * + * Certains buts engendrés par "correctness" (ci-dessous) + * sont réellement triviaux. On peut les résoudre aisément, sans pour autant + * tomber dans la solution trop lourde qui consiste ą faire "; Auto." + * + * Cette tactique fait les choses suivantes : + * o elle élimine les hypothčses de nom loop<i> + * o sur G |- (well_founded nat lt) ==> Exact lt_wf. + * o sur G |- (well_founded Z (Zwf c)) ==> Exact (Zwf_well_founded c) + * o sur G |- e = e' ==> Reflexivity. (arg. de decr. des boucles) + * sinon Try Assumption. + * o sur G |- P /\ Q ==> Try (Split; Assumption). (sortie de boucle) + * o sinon, Try AssumptionBis (= Assumption + décomposition /\ dans hyp.) + * (pour entrée dans corps de boucle par ex.) + *) + +open Pattern +open Tacmach +open Tactics +open Tacticals +open Equality +open Nametab + +let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0) +let lt = ConstRef (coq_constant ["Init";"Peano"] "lt") +let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded") +let z = IndRef (coq_constant ["ZArith";"BinInt"] "Z", 0) +let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0) +let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0) + +let mkmeta n = Nameops.make_ident "X" (Some n) +let mkPMeta n = PMeta (Some (mkmeta n)) + +(* ["(well_founded nat lt)"] *) +let wf_nat_pattern = + PApp (PRef well_founded, [| PRef nat; PRef lt |]) +(* ["((well_founded Z (Zwf ?1))"] *) +let wf_z_pattern = + let zwf = ConstRef (coq_constant ["ZArith";"Zwf"] "Zwf") in + PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| mkPMeta 1 |]) |]) +(* ["(and ?1 ?2)"] *) +let and_pattern = + PApp (PRef and_, [| mkPMeta 1; mkPMeta 2 |]) +(* ["(eq ?1 ?2 ?3)"] *) +let eq_pattern = + PApp (PRef eq, [| mkPMeta 1; mkPMeta 2; mkPMeta 3 |]) + +(* loop_ids: remove loop<i> hypotheses from the context, and rewrite + * using Variant<i> hypotheses when needed. *) + +let (loop_ids : tactic) = fun gl -> + let rec arec hyps gl = + let env = pf_env gl in + let concl = pf_concl gl in + match hyps with + | [] -> tclIDTAC gl + | (id,a) :: al -> + let s = string_of_id id in + let n = String.length s in + if n >= 4 & (let su = String.sub s 0 4 in su="loop" or su="Bool") + then + tclTHEN (clear [id]) (arec al) gl + else if n >= 7 & String.sub s 0 7 = "Variant" then begin + match pf_matches gl eq_pattern (body_of_type a) with + | [_; _,varphi; _] when isVar varphi -> + let phi = destVar varphi in + if Termops.occur_var env phi concl then + tclTHEN (rewriteLR (mkVar id)) (arec al) gl + else + arec al gl + | _ -> assert false end + else + arec al gl + in + arec (pf_hyps_types gl) gl + +(* assumption_bis: like assumption, but also solves ... h:A/\B ... |- A + * (resp. B) *) + +let (assumption_bis : tactic) = fun gl -> + let concl = pf_concl gl in + let rec arec = function + | [] -> Util.error "No such assumption" + | (s,a) :: al -> + let a = body_of_type a in + if pf_conv_x_leq gl a concl then + refine (mkVar s) gl + else if pf_is_matching gl and_pattern a then + match pf_matches gl and_pattern a with + | [_,c1; _,c2] -> + if pf_conv_x_leq gl c1 concl then + exact_check (applistc (constant "proj1") [c1;c2;mkVar s]) gl + else if pf_conv_x_leq gl c2 concl then + exact_check (applistc (constant "proj2") [c1;c2;mkVar s]) gl + else + arec al + | _ -> assert false + else + arec al + in + arec (pf_hyps_types gl) + +(* automatic: see above *) + +let (automatic : tactic) = + tclTHEN + loop_ids + (fun gl -> + let c = pf_concl gl in + if pf_is_matching gl wf_nat_pattern c then + exact_check (constant "lt_wf") gl + else if pf_is_matching gl wf_z_pattern c then + let (_,z) = List.hd (pf_matches gl wf_z_pattern c) in + exact_check (Term.applist (constant "Zwf_well_founded",[z])) gl + else if pf_is_matching gl and_pattern c then + (tclORELSE assumption_bis + (tclTRY (tclTHEN simplest_split assumption))) gl + else if pf_is_matching gl eq_pattern c then + (tclORELSE reflexivity (tclTRY assumption_bis)) gl + else + tclTRY assumption_bis gl) + +(* [correctness s p] : string -> program -> tactic option -> unit + * + * Vernac: Correctness <string> <program> [; <tactic>]. + *) + +let reduce_open_constr (em0,c) = + let existential_map_of_constr = + let rec collect em c = match kind_of_term c with + | Cast (c',t) -> + (match kind_of_term c' with + | Evar (ev,_) -> + if not (Evd.in_dom em ev) then + Evd.add em ev (Evd.map em0 ev) + else + em + | _ -> fold_constr collect em c) + | Evar _ -> + assert false (* all existentials should be casted *) + | _ -> + fold_constr collect em c + in + collect Evd.empty + in + let c = Pred.red_cci c in + let em = existential_map_of_constr c in + (em,c) + +let register id n = + let id' = match n with None -> id | Some id' -> id' in + Penv.register id id' + + (* On dit ą la commande "Save" d'enregistrer les nouveaux programmes *) +let correctness_hook _ ref = + let pf_id = Nametab.id_of_global ref in + register pf_id None + +let correctness s p opttac = + Library.check_required_library ["Coq";"correctness";"Correctness"]; + Pmisc.reset_names(); + let p,oc,cty,v = coqast_of_prog p in + let env = Global.env () in + let sign = Global.named_context () in + let sigma = Evd.empty in + let cty = Reduction.nf_betaiota cty in + let id = id_of_string s in + start_proof id (IsGlobal (Proof Lemma)) sign cty correctness_hook; + Penv.new_edited id (v,p); + if !debug then msg (Pfedit.pr_open_subgoals()); + deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); + let oc = reduce_open_constr oc in + deb_mess (str"AFTER REDUCTION:" ++ fnl ()); + deb_print (Printer.prterm_env (Global.env())) (snd oc); + let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in + let tac = match opttac with + | None -> tac + | Some t -> tclTHEN tac t + in + solve_nth 1 tac; + if_verbose msg (pr_open_subgoals ()) diff --git a/contrib/correctness/ptactic.mli b/contrib/correctness/ptactic.mli new file mode 100644 index 00000000..875e0780 --- /dev/null +++ b/contrib/correctness/ptactic.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ptactic.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *) + +(* The main tactic: takes a name N, a program P, creates a goal + * of name N with the functional specification of P, then apply the Refine + * tactic with the partial proof term obtained by the translation of + * P into a functional program. + * + * Then an ad-hoc automatic tactic is applied on each subgoal to solve the + * trivial proof obligations *) + +val correctness : string -> Past.program -> Tacmach.tactic option -> unit + diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli new file mode 100644 index 00000000..f2dc85e3 --- /dev/null +++ b/contrib/correctness/ptype.mli @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ptype.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Term + +(* Types des valeurs (V) et des calculs (C). + * + * On a C = r:V,E,P,Q + * + * et V = (x1:V1)...(xn:Vn)C | V ref | V array | <type pur> + * + * INVARIANT: l'effet E contient toutes les variables apparaissant dans + * le programme ET les annotations P et Q + * Si E = { x1,...,xn | y1,...,ym }, les variables x sont les + * variables en lecture seule et y1 les variables modifiées + * les xi sont libres dans P et Q, et les yi,result liées dans Q + * i.e. P = p(x) + * et Q = [y1]...[yn][res]q(x,y,res) + *) + +(* pre and post conditions *) + +type 'a precondition = { p_assert : bool; p_name : Names.name; p_value : 'a } + +type 'a assertion = { a_name : Names.name; a_value : 'a } + +type 'a postcondition = 'a assertion + +type predicate = constr assertion + +(* binders *) + +type 'a binder_type = + BindType of 'a + | BindSet + | Untyped + +type 'a binder = Names.identifier * 'a binder_type + +(* variant *) + +type variant = constr * constr * constr (* phi, R, A *) + +(* types des valeurs *) + +type 'a ml_type_v = + Ref of 'a ml_type_v + | Array of 'a * 'a ml_type_v (* size x type *) + | Arrow of 'a ml_type_v binder list * 'a ml_type_c + + | TypePure of 'a + +(* et type des calculs *) + +and 'a ml_type_c = + (Names.identifier * 'a ml_type_v) + * Peffect.t + * ('a precondition list) * ('a postcondition option) + +(* at beginning they contain Coq AST but they become constr after typing *) +type type_v = constr ml_type_v +type type_c = constr ml_type_c + + diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml new file mode 100644 index 00000000..9047a925 --- /dev/null +++ b/contrib/correctness/ptyping.ml @@ -0,0 +1,600 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ptyping.ml,v 1.7.6.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Pp +open Util +open Names +open Term +open Termops +open Environ +open Constrintern +open Himsg +open Proof_trees +open Topconstr + +open Pmisc +open Putil +open Prename +open Ptype +open Past +open Penv +open Peffect +open Pcicenv + +(* Ce module implante le jugement Gamma |-a e : kappa de la thčse. + * Les annotations passent du type CoqAst.t au type Term.constr ici. + * Les post-conditions sont abstraites par rapport au résultat. *) + +let simplify_type_of env sigma t = + Reductionops.nf_betaiota (Typing.type_of env sigma t) + +let just_reads e = + difference (get_reads e) (get_writes e) + +let type_v_sup loc t1 t2 = + if t1 = t2 then + t1 + else + Perror.if_branches loc + +let typed_var ren env (phi,r) = + let sign = Pcicenv.before_after_sign_of ren env in + let a = simplify_type_of (Global.env_of_context sign) Evd.empty phi in + (phi,r,a) + +(* Application de fonction *) + +let rec convert = function + | (TypePure c1, TypePure c2) -> + Reductionops.is_conv (Global.env ()) Evd.empty c1 c2 + | (Ref v1, Ref v2) -> + convert (v1,v2) + | (Array (s1,v1), Array (s2,v2)) -> + (Reductionops.is_conv (Global.env ()) Evd.empty s1 s2) && (convert (v1,v2)) + | (v1,v2) -> v1 = v2 + +let effect_app ren env f args = + let n = List.length args in + let tf = + let ((_,v),_,_,_) = f.info.kappa in + match v with TypePure c -> v_of_constr c | _ -> v + in + let bl,c = + match tf with + Arrow (bl, c) -> + if List.length bl <> n then Perror.partial_app f.loc; + bl,c + | _ -> Perror.app_of_non_function f.loc + in + let check_type loc v t so = + let v' = type_v_rsubst so v in + if not (convert (v',t)) then Perror.expected_type loc (pp_type_v v') + in + let s,so,ok = + (* s est la substitution des références, so celle des autres arg. + * ok nous dit si les arguments sont sans effet i.e. des expressions *) + List.fold_left + (fun (s,so,ok) (b,a) -> + match b,a with + (id,BindType (Ref _ | Array _ as v)), Refarg id' -> + let ta = type_in_env env id' in + check_type f.loc v ta so; + (id,id')::s, so, ok + | _, Refarg _ -> Perror.should_be_a_variable f.loc + | (id,BindType v), Term t -> + let ((_,ta),_,_,_) = t.info.kappa in + check_type t.loc v ta so; + (match t.desc with + Expression c -> s, (id,c)::so, ok + | _ -> s,so,false) + | (id,BindSet), Type v -> + let c = Pmonad.trad_ml_type_v ren env v in + s, (id,c)::so, ok + | (id,BindSet), Term t -> Perror.expects_a_type id t.loc + | (id,BindType _), Type _ -> Perror.expects_a_term id + | (_,Untyped), _ -> invalid_arg "effects_app") + ([],[],true) + (List.combine bl args) + in + let (id,v),ef,pre,post = type_c_subst s c in + (bl,c), (s,so,ok), ((id,type_v_rsubst so v),ef,pre,post) + +(* Execution of a Coq AST. Returns value and type. + * Also returns its variables *) + +let state_coq_ast sign a = + let env = Global.env_of_context sign in + let j = + reraise_with_loc (constr_loc a) (judgment_of_rawconstr Evd.empty env) a in + let ids = global_vars env j.uj_val in + j.uj_val, j.uj_type, ids + +(* [is_pure p] tests wether the program p is an expression or not. *) + +let type_of_expression ren env c = + let sign = now_sign_of ren env in + simplify_type_of (Global.env_of_context sign) Evd.empty c + +let rec is_pure_type_v = function + TypePure _ -> true + | Arrow (bl,c) -> List.for_all is_pure_arg bl & is_pure_type_c c + | Ref _ | Array _ -> false +and is_pure_arg = function + (_,BindType v) -> is_pure_type_v v + | (_,BindSet) -> true + | (_,Untyped) -> false +and is_pure_type_c = function + (_,v),_,[],None -> is_pure_type_v v + | _ -> false + +let rec is_pure_desc ren env = function + Variable id -> + not (is_in_env env id) or (is_pure_type_v (type_in_env env id)) + | Expression c -> + (c = isevar) or (is_pure_cci (type_of_expression ren env c)) + | Acc _ -> true + | TabAcc (_,_,p) -> is_pure ren env p + | Apply (p,args) -> + is_pure ren env p & List.for_all (is_pure_arg ren env) args + | SApp _ | Aff _ | TabAff _ | Seq _ | While _ | If _ + | Lam _ | LetRef _ | Let _ | LetRec _ -> false + | Debug (_,p) -> is_pure ren env p + | PPoint (_,d) -> is_pure_desc ren env d +and is_pure ren env p = + p.pre = [] & p.post = None & is_pure_desc ren env p.desc +and is_pure_arg ren env = function + Term p -> is_pure ren env p + | Type _ -> true + | Refarg _ -> false + +(* [state_var ren env (phi,r)] returns a tuple (e,(phi',r')) + * where e is the effect of the variant phi and phi',r' the corresponding + * constr of phi and r. + *) + +let state_var ren env (phi,r) = + let sign = Pcicenv.before_after_sign_of ren env in + let phi',_,ids = state_coq_ast sign phi in + let ef = List.fold_left + (fun e id -> + if is_mutable_in_env env id then Peffect.add_read id e else e) + Peffect.bottom ids in + let r',_,_ = state_coq_ast (Global.named_context ()) r in + ef,(phi',r') + +(* [state_pre ren env pl] returns a pair (e,c) where e is the effect of the + * pre-conditions list pl and cl the corresponding constrs not yet abstracted + * over the variables xi (i.e. c NOT [x1]...[xn]c !) + *) + +let state_pre ren env pl = + let state e p = + let sign = Pcicenv.before_sign_of ren env in + let cc,_,ids = state_coq_ast sign p.p_value in + let ef = List.fold_left + (fun e id -> + if is_mutable_in_env env id then + Peffect.add_read id e + else if is_at id then + let uid,_ = un_at id in + if is_mutable_in_env env uid then + Peffect.add_read uid e + else + e + else + e) + e ids + in + ef,{ p_assert = p.p_assert; p_name = p.p_name; p_value = cc } + in + List.fold_left + (fun (e,cl) p -> let ef,c = state e p in (ef,c::cl)) + (Peffect.bottom,[]) pl + +let state_assert ren env a = + let p = pre_of_assert true a in + let e,l = state_pre ren env [p] in + e,assert_of_pre (List.hd l) + +let state_inv ren env = function + None -> Peffect.bottom, None + | Some i -> let e,p = state_assert ren env i in e,Some p + +(* [state_post ren env (id,v,ef) q] returns a pair (e,c) + * where e is the effect of the + * post-condition q and c the corresponding constr not yet abstracted + * over the variables xi, yi and result. + * Moreover the RW variables not appearing in ef have been replaced by + * RO variables, and (id,v) is the result + *) + +let state_post ren env (id,v,ef) = function + None -> Peffect.bottom, None + | Some q -> + let v' = Pmonad.trad_ml_type_v ren env v in + let sign = Pcicenv.before_after_result_sign_of (Some (id,v')) ren env in + let cc,_,ids = state_coq_ast sign q.a_value in + let ef,c = + List.fold_left + (fun (e,c) id -> + if is_mutable_in_env env id then + if is_write ef id then + Peffect.add_write id e, c + else + Peffect.add_read id e, + subst_in_constr [id,at_id id ""] c + else if is_at id then + let uid,_ = un_at id in + if is_mutable_in_env env uid then + Peffect.add_read uid e, c + else + e,c + else + e,c) + (Peffect.bottom,cc) ids + in + let c = abstract [id,v'] c in + ef, Some { a_name = q.a_name; a_value = c } + +(* transformation of AST into constr in types V and C *) + +let rec cic_type_v env ren = function + | Ref v -> Ref (cic_type_v env ren v) + | Array (com,v) -> + let sign = Pcicenv.now_sign_of ren env in + let c = interp_constr Evd.empty (Global.env_of_context sign) com in + Array (c, cic_type_v env ren v) + | Arrow (bl,c) -> + let bl',ren',env' = + List.fold_left + (fun (bl,ren,env) b -> + let b' = cic_binder env ren b in + let env' = traverse_binders env [b'] in + let ren' = initial_renaming env' in + b'::bl,ren',env') + ([],ren,env) bl + in + let c' = cic_type_c env' ren' c in + Arrow (List.rev bl',c') + | TypePure com -> + let sign = Pcicenv.cci_sign_of ren env in + let c = interp_constr Evd.empty (Global.env_of_context sign) com in + TypePure c + +and cic_type_c env ren ((id,v),e,p,q) = + let v' = cic_type_v env ren v in + let cv = Pmonad.trad_ml_type_v ren env v' in + let efp,p' = state_pre ren env p in + let efq,q' = state_post ren env (id,v',e) q in + let ef = Peffect.union e (Peffect.union efp efq) in + ((id,v'),ef,p',q') + +and cic_binder env ren = function + | (id,BindType v) -> + let v' = cic_type_v env ren v in + let env' = add (id,v') env in + let ren' = initial_renaming env' in + (id, BindType v') + | (id,BindSet) -> (id,BindSet) + | (id,Untyped) -> (id,Untyped) + +and cic_binders env ren = function + [] -> [] + | b::bl -> + let b' = cic_binder env ren b in + let env' = traverse_binders env [b'] in + let ren' = initial_renaming env' in + b' :: (cic_binders env' ren' bl) + + +(* The case of expressions. + * + * Expressions are programs without neither effects nor pre/post conditions. + * But access to variables are allowed. + * + * Here we transform an expression into the corresponding constr, + * the variables still appearing as VAR (they will be abstracted in + * Mlise.trad) + * We collect the pre-conditions (e<N for t[e]) as we traverse the term. + * We also return the effect, which does contain only *read* variables. + *) + +let states_expression ren env expr = + let rec effect pl = function + | Variable id -> + (if is_global id then constant (string_of_id id) else mkVar id), + pl, Peffect.bottom + | Expression c -> c, pl, Peffect.bottom + | Acc id -> mkVar id, pl, Peffect.add_read id Peffect.bottom + | TabAcc (_,id,p) -> + let c,pl,ef = effect pl p.desc in + let pre = Pmonad.make_pre_access ren env id c in + Pmonad.make_raw_access ren env (id,id) c, + (anonymous_pre true pre)::pl, Peffect.add_read id ef + | Apply (p,args) -> + let a,pl,e = effect pl p.desc in + let args,pl,e = + List.fold_right + (fun arg (l,pl,e) -> + match arg with + Term p -> + let carg,pl,earg = effect pl p.desc in + carg::l,pl,Peffect.union e earg + | Type v -> + let v' = cic_type_v env ren v in + (Pmonad.trad_ml_type_v ren env v')::l,pl,e + | Refarg _ -> assert false) + args ([],pl,e) + in + Term.applist (a,args),pl,e + | _ -> invalid_arg "Ptyping.states_expression" + in + let e0,pl0 = state_pre ren env expr.pre in + let c,pl,e = effect [] expr.desc in + let sign = Pcicenv.before_sign_of ren env in + (*i WAS + let c = (Trad.ise_resolve true empty_evd [] (gLOB sign) c)._VAL in + i*) + let ty = simplify_type_of (Global.env_of_context sign) Evd.empty c in + let v = TypePure ty in + let ef = Peffect.union e0 e in + Expression c, (v,ef), pl0@pl + + +(* We infer here the type with effects. + * The type of types with effects (ml_type_c) is defined in the module ProgAst. + * + * A program of the shape {P} e {Q} has a type + * + * V, E, {None|Some P}, {None|Some Q} + * + * where - V is the type of e + * - E = (I,O) is the effect; the input I contains + * all the input variables appearing in P,e and Q; + * the output O contains variables possibly modified in e + * - P is NOT abstracted + * - Q = [y'1]...[y'k][result]Q where O = {y'j} + * i.e. Q is only abstracted over the output and the result + * the other variables now refer to value BEFORE + *) + +let verbose_fix = ref false + +let rec states_desc ren env loc = function + + Expression c -> + let ty = type_of_expression ren env c in + let v = v_of_constr ty in + Expression c, (v,Peffect.bottom) + + | Acc _ -> + failwith "Ptyping.states: term is supposed not to be pure" + + | Variable id -> + let v = type_in_env env id in + let ef = Peffect.bottom in + Variable id, (v,ef) + + | Aff (x, e1) -> + Perror.check_for_reference loc x (type_in_env env x); + let s_e1 = states ren env e1 in + let _,e,_,_ = s_e1.info.kappa in + let ef = add_write x e in + let v = constant_unit () in + Aff (x, s_e1), (v, ef) + + | TabAcc (check, x, e) -> + let s_e = states ren env e in + let _,efe,_,_ = s_e.info.kappa in + let ef = Peffect.add_read x efe in + let _,ty = dearray_type (type_in_env env x) in + TabAcc (check, x, s_e), (ty, ef) + + | TabAff (check, x, e1, e2) -> + let s_e1 = states ren env e1 in + let s_e2 = states ren env e2 in + let _,ef1,_,_ = s_e1.info.kappa in + let _,ef2,_,_ = s_e2.info.kappa in + let ef = Peffect.add_write x (Peffect.union ef1 ef2) in + let v = constant_unit () in + TabAff (check, x, s_e1, s_e2), (v,ef) + + | Seq bl -> + let bl,v,ef,_ = states_block ren env bl in + Seq bl, (v,ef) + + | While(b, invopt, var, bl) -> + let efphi,(cvar,r') = state_var ren env var in + let ren' = next ren [] in + let s_b = states ren' env b in + let s_bl,_,ef_bl,_ = states_block ren' env bl in + let cb = s_b.info.kappa in + let efinv,inv = state_inv ren env invopt in + let _,efb,_,_ = s_b.info.kappa in + let ef = + Peffect.union (Peffect.union ef_bl efb) (Peffect.union efinv efphi) + in + let v = constant_unit () in + let cvar = + let al = List.map (fun id -> (id,at_id id "")) (just_reads ef) in + subst_in_constr al cvar + in + While (s_b,inv,(cvar,r'),s_bl), (v,ef) + + | Lam ([],_) -> + failwith "Ptyping.states: abs. should have almost one binder" + + | Lam (bl, e) -> + let bl' = cic_binders env ren bl in + let env' = traverse_binders env bl' in + let ren' = initial_renaming env' in + let s_e = states ren' env' e in + let v = make_arrow bl' s_e.info.kappa in + let ef = Peffect.bottom in + Lam(bl',s_e), (v,ef) + + (* Connectives AND and OR *) + | SApp ([Variable id], [e1;e2]) -> + let s_e1 = states ren env e1 + and s_e2 = states ren env e2 in + let (_,ef1,_,_) = s_e1.info.kappa + and (_,ef2,_,_) = s_e2.info.kappa in + let ef = Peffect.union ef1 ef2 in + SApp ([Variable id], [s_e1; s_e2]), + (TypePure (constant "bool"), ef) + + (* Connective NOT *) + | SApp ([Variable id], [e]) -> + let s_e = states ren env e in + let (_,ef,_,_) = s_e.info.kappa in + SApp ([Variable id], [s_e]), + (TypePure (constant "bool"), ef) + + | SApp _ -> invalid_arg "Ptyping.states (SApp)" + + (* ATTENTION: + Si un argument réel de type ref. correspond ą une ref. globale + modifiée par la fonction alors la traduction ne sera pas correcte. + Exemple: + f=[x:ref Int]( r := !r+1 ; x := !x+1) modifie r et son argument x + donc si on l'applique ą r justement, elle ne modifiera que r + mais le séquencement ne sera pas correct. *) + + | Apply (f, args) -> + let s_f = states ren env f in + let _,eff,_,_ = s_f.info.kappa in + let s_args = List.map (states_arg ren env) args in + let ef_args = + List.map + (function Term t -> let (_,e,_,_) = t.info.kappa in e + | _ -> Peffect.bottom) + s_args + in + let _,_,((_,tapp),efapp,_,_) = effect_app ren env s_f s_args in + let ef = + Peffect.compose (List.fold_left Peffect.compose eff ef_args) efapp + in + Apply (s_f, s_args), (tapp, ef) + + | LetRef (x, e1, e2) -> + let s_e1 = states ren env e1 in + let (_,v1),ef1,_,_ = s_e1.info.kappa in + let env' = add (x,Ref v1) env in + let ren' = next ren [x] in + let s_e2 = states ren' env' e2 in + let (_,v2),ef2,_,_ = s_e2.info.kappa in + Perror.check_for_let_ref loc v2; + let ef = Peffect.compose ef1 (Peffect.remove ef2 x) in + LetRef (x, s_e1, s_e2), (v2,ef) + + | Let (x, e1, e2) -> + let s_e1 = states ren env e1 in + let (_,v1),ef1,_,_ = s_e1.info.kappa in + Perror.check_for_not_mutable e1.loc v1; + let env' = add (x,v1) env in + let s_e2 = states ren env' e2 in + let (_,v2),ef2,_,_ = s_e2.info.kappa in + let ef = Peffect.compose ef1 ef2 in + Let (x, s_e1, s_e2), (v2,ef) + + | If (b, e1, e2) -> + let s_b = states ren env b in + let s_e1 = states ren env e1 + and s_e2 = states ren env e2 in + let (_,tb),efb,_,_ = s_b.info.kappa in + let (_,t1),ef1,_,_ = s_e1.info.kappa in + let (_,t2),ef2,_,_ = s_e2.info.kappa in + let ef = Peffect.compose efb (disj ef1 ef2) in + let v = type_v_sup loc t1 t2 in + If (s_b, s_e1, s_e2), (v,ef) + + | LetRec (f,bl,v,var,e) -> + let bl' = cic_binders env ren bl in + let env' = traverse_binders env bl' in + let ren' = initial_renaming env' in + let v' = cic_type_v env' ren' v in + let efvar,var' = state_var ren' env' var in + let phi0 = phi_name () in + let tvar = typed_var ren env' var' in + (* effect for a let/rec construct is computed as a fixpoint *) + let rec state_rec c = + let tf = make_arrow bl' c in + let env'' = add_recursion (f,(phi0,tvar)) (add (f,tf) env') in + let s_e = states ren' env'' e in + if s_e.info.kappa = c then + s_e + else begin + if !verbose_fix then begin msgnl (pp_type_c s_e.info.kappa) end ; + state_rec s_e.info.kappa + end + in + let s_e = state_rec ((result_id,v'),efvar,[],None) in + let tf = make_arrow bl' s_e.info.kappa in + LetRec (f,bl',v',var',s_e), (tf,Peffect.bottom) + + | PPoint (s,d) -> + let ren' = push_date ren s in + states_desc ren' env loc d + + | Debug _ -> failwith "Ptyping.states: Debug: TODO" + + +and states_arg ren env = function + Term a -> let s_a = states ren env a in Term s_a + | Refarg id -> Refarg id + | Type v -> let v' = cic_type_v env ren v in Type v' + + +and states ren env expr = + (* Here we deal with the pre- and post- conditions: + * we add their effects to the effects of the program *) + let (d,(v,e),p1) = + if is_pure_desc ren env expr.desc then + states_expression ren env expr + else + let (d,ve) = states_desc ren env expr.loc expr.desc in (d,ve,[]) + in + let (ep,p) = state_pre ren env expr.pre in + let (eq,q) = state_post ren env (result_id,v,e) expr.post in + let e' = Peffect.union e (Peffect.union ep eq) in + let p' = p1 @ p in + let tinfo = { env = env; kappa = ((result_id,v),e',p',q) } in + { desc = d; + loc = expr.loc; + pre = p'; post = q; (* on les conserve aussi ici pour prog_wp *) + info = tinfo } + + +and states_block ren env bl = + let rec ef_block ren tyres = function + [] -> + begin match tyres with + Some ty -> [],ty,Peffect.bottom,ren + | None -> failwith "a block should contain at least one statement" + end + | (Assert p)::block -> + let ep,c = state_assert ren env p in + let bl,t,ef,ren' = ef_block ren tyres block in + (Assert c)::bl,t,Peffect.union ep ef,ren' + | (Label s)::block -> + let ren' = push_date ren s in + let bl,t,ef,ren'' = ef_block ren' tyres block in + (Label s)::bl,t,ef,ren'' + | (Statement e)::block -> + let s_e = states ren env e in + let (_,t),efe,_,_ = s_e.info.kappa in + let ren' = next ren (get_writes efe) in + let bl,t,ef,ren'' = ef_block ren' (Some t) block in + (Statement s_e)::bl,t,Peffect.compose efe ef,ren'' + in + ef_block ren None bl + diff --git a/contrib/correctness/ptyping.mli b/contrib/correctness/ptyping.mli new file mode 100644 index 00000000..0c0d5905 --- /dev/null +++ b/contrib/correctness/ptyping.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: ptyping.mli,v 1.3.6.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Names +open Term +open Topconstr + +open Ptype +open Past +open Penv + +(* This module realizes type and effect inference *) + +val cic_type_v : local_env -> Prename.t -> constr_expr ml_type_v -> type_v + +val effect_app : Prename.t -> local_env + -> (typing_info,'b) Past.t + -> (typing_info,constr) arg list + -> (type_v binder list * type_c) + * ((identifier*identifier) list * (identifier*constr) list * bool) + * type_c + +val typed_var : Prename.t -> local_env -> constr * constr -> variant + +val type_of_expression : Prename.t -> local_env -> constr -> constr + +val states : Prename.t -> local_env -> program -> typed_program diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml new file mode 100644 index 00000000..48f0781a --- /dev/null +++ b/contrib/correctness/putil.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: putil.ml,v 1.10.2.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Util +open Names +open Nameops +open Term +open Termops +open Pattern +open Matching +open Hipattern +open Environ + +open Pmisc +open Ptype +open Past +open Penv +open Prename + +let is_mutable = function Ref _ | Array _ -> true | _ -> false +let is_pure = function TypePure _ -> true | _ -> false + +let named_app f x = { a_name = x.a_name; a_value = (f x.a_value) } + +let pre_app f x = + { p_assert = x.p_assert; p_name = x.p_name; p_value = f x.p_value } + +let post_app = named_app + +let anonymous x = { a_name = Anonymous; a_value = x } + +let anonymous_pre b x = { p_assert = b; p_name = Anonymous; p_value = x } + +let force_name f x = + option_app (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x + +let force_post_name x = force_name post_name x + +let force_bool_name x = + force_name (function Name id -> id | Anonymous -> bool_name()) x + +let out_post = function + Some { a_value = x } -> x + | None -> invalid_arg "out_post" + +let pre_of_assert b x = + { p_assert = b; p_name = x.a_name; p_value = x.a_value } + +let assert_of_pre x = + { a_name = x.p_name; a_value = x.p_value } + +(* Some generic functions on programs *) + +let is_mutable_in_env env id = + (is_in_env env id) & (is_mutable (type_in_env env id)) + +let now_vars env c = + Util.map_succeed + (function id -> if is_mutable_in_env env id then id else failwith "caught") + (global_vars (Global.env()) c) + +let make_before_after c = + let ids = global_vars (Global.env()) c in + let al = + Util.map_succeed + (function id -> + if is_at id then + match un_at id with (uid,"") -> (id,uid) | _ -> failwith "caught" + else failwith "caught") + ids + in + subst_in_constr al c + +(* [apply_pre] and [apply_post] instantiate pre- and post- conditions + * according to a given renaming of variables (and a date that means + * `before' in the case of the post-condition). + *) + +let make_assoc_list ren env on_prime ids = + List.fold_left + (fun al id -> + if is_mutable_in_env env id then + (id,current_var ren id)::al + else if is_at id then + let uid,d = un_at id in + if is_mutable_in_env env uid then + (match d with + "" -> (id,on_prime ren uid) + | _ -> (id,var_at_date ren d uid))::al + else + al + else + al) + [] ids + +let apply_pre ren env c = + let ids = global_vars (Global.env()) c.p_value in + let al = make_assoc_list ren env current_var ids in + { p_assert = c.p_assert; p_name = c.p_name; + p_value = subst_in_constr al c.p_value } + +let apply_assert ren env c = + let ids = global_vars (Global.env()) c.a_value in + let al = make_assoc_list ren env current_var ids in + { a_name = c.a_name; a_value = subst_in_constr al c.a_value } + +let apply_post ren env before c = + let ids = global_vars (Global.env()) c.a_value in + let al = + make_assoc_list ren env (fun r uid -> var_at_date r before uid) ids in + { a_name = c.a_name; a_value = subst_in_constr al c.a_value } + +(* [traverse_binder ren env bl] updates renaming [ren] and environment [env] + * as we cross the binders [bl] + *) + +let rec traverse_binders env = function + [] -> env + | (id,BindType v)::rem -> + traverse_binders (add (id,v) env) rem + | (id,BindSet)::rem -> + traverse_binders (add_set id env) rem + | (_,Untyped)::_ -> + invalid_arg "traverse_binders" + +let initial_renaming env = + let ids = Penv.fold_all (fun (id,_) l -> id::l) env [] in + update empty_ren "0" ids + + +(* Substitutions *) + +let rec type_c_subst s ((id,t),e,p,q) = + let s' = s @ List.map (fun (x,x') -> (at_id x "", at_id x' "")) s in + (id, type_v_subst s t), Peffect.subst s e, + List.map (pre_app (subst_in_constr s)) p, + option_app (post_app (subst_in_constr s')) q + +and type_v_subst s = function + Ref v -> Ref (type_v_subst s v) + | Array (n,v) -> Array (n,type_v_subst s v) + | Arrow (bl,c) -> Arrow(List.map (binder_subst s) bl, type_c_subst s c) + | (TypePure _) as v -> v + +and binder_subst s = function + (n, BindType v) -> (n, BindType (type_v_subst s v)) + | b -> b + +(* substitution of constr by others *) + +let rec type_c_rsubst s ((id,t),e,p,q) = + (id, type_v_rsubst s t), e, + List.map (pre_app (real_subst_in_constr s)) p, + option_app (post_app (real_subst_in_constr s)) q + +and type_v_rsubst s = function + Ref v -> Ref (type_v_rsubst s v) + | Array (n,v) -> Array (real_subst_in_constr s n,type_v_rsubst s v) + | Arrow (bl,c) -> Arrow(List.map (binder_rsubst s) bl, type_c_rsubst s c) + | TypePure c -> TypePure (real_subst_in_constr s c) + +and binder_rsubst s = function + | (n, BindType v) -> (n, BindType (type_v_rsubst s v)) + | b -> b + +(* make_arrow bl c = (x1:V1)...(xn:Vn)c *) + +let make_arrow bl c = match bl with + | [] -> invalid_arg "make_arrow: no binder" + | _ -> Arrow (bl,c) + +(* misc. functions *) + +let deref_type = function + | Ref v -> v + | _ -> invalid_arg "deref_type" + +let dearray_type = function + | Array (size,v) -> size,v + | _ -> invalid_arg "dearray_type" + +let constant_unit () = TypePure (constant "unit") + +let id_from_name = function Name id -> id | Anonymous -> (id_of_string "X") + +(* v_of_constr : traduit un type CCI en un type ML *) + +(* TODO: faire un test plus serieux sur le type des objets Coq *) +let rec is_pure_cci c = match kind_of_term c with + | Cast (c,_) -> is_pure_cci c + | Prod(_,_,c') -> is_pure_cci c' + | Rel _ | Ind _ | Const _ -> true (* heu... *) + | App _ -> not (is_matching_sigma c) + | _ -> Util.error "CCI term not acceptable in programs" + +let rec v_of_constr c = match kind_of_term c with + | Cast (c,_) -> v_of_constr c + | Prod _ -> + let revbl,t2 = Term.decompose_prod c in + let bl = + List.map + (fun (name,t1) -> (id_from_name name, BindType (v_of_constr t1))) + (List.rev revbl) + in + let vars = List.rev (List.map (fun (id,_) -> mkVar id) bl) in + Arrow (bl, c_of_constr (substl vars t2)) + | Ind _ | Const _ | App _ -> + TypePure c + | _ -> + failwith "v_of_constr: TODO" + +and c_of_constr c = + if is_matching_sigma c then + let (a,q) = match_sigma c in + (result_id, v_of_constr a), Peffect.bottom, [], Some (anonymous q) + else + (result_id, v_of_constr c), Peffect.bottom, [], None + + +(* pretty printers (for debugging purposes) *) + +open Pp +open Util + +let prterm x = Printer.prterm_env (Global.env()) x + +let pp_pre = function + [] -> (mt ()) + | l -> + hov 0 (str"pre " ++ + prlist_with_sep (fun () -> (spc ())) + (fun x -> prterm x.p_value) l) + +let pp_post = function + None -> (mt ()) + | Some c -> hov 0 (str"post " ++ prterm c.a_value) + +let rec pp_type_v = function + Ref v -> hov 0 (pp_type_v v ++ spc () ++ str"ref") + | Array (cc,v) -> hov 0 (str"array " ++ prterm cc ++ str" of " ++ pp_type_v v) + | Arrow (b,c) -> + hov 0 (prlist_with_sep (fun () -> (mt ())) pp_binder b ++ + pp_type_c c) + | TypePure c -> prterm c + +and pp_type_c ((id,v),e,p,q) = + hov 0 (str"returns " ++ pr_id id ++ str":" ++ pp_type_v v ++ spc () ++ + Peffect.pp e ++ spc () ++ pp_pre p ++ spc () ++ pp_post q ++ + spc () ++ str"end") + +and pp_binder = function + id,BindType v -> (str"(" ++ pr_id id ++ str":" ++ pp_type_v v ++ str")") + | id,BindSet -> (str"(" ++ pr_id id ++ str":Set)") + | id,Untyped -> (str"(" ++ pr_id id ++ str")") + +(* pretty-print of cc-terms (intermediate terms) *) + +let rec pp_cc_term = function + CC_var id -> pr_id id + | CC_letin (_,_,bl,c,c1) -> + hov 0 (hov 2 (str"let " ++ + prlist_with_sep (fun () -> (str",")) + (fun (id,_) -> pr_id id) bl ++ + str" =" ++ spc () ++ + pp_cc_term c ++ + str " in") ++ + fnl () ++ + pp_cc_term c1) + | CC_lam (bl,c) -> + hov 2 (prlist (fun (id,_) -> (str"[" ++ pr_id id ++ str"]")) bl ++ + cut () ++ + pp_cc_term c) + | CC_app (f,args) -> + hov 2 (str"(" ++ + pp_cc_term f ++ spc () ++ + prlist_with_sep (fun () -> (spc ())) pp_cc_term args ++ + str")") + | CC_tuple (_,_,cl) -> + hov 2 (str"(" ++ + prlist_with_sep (fun () -> (str"," ++ cut ())) + pp_cc_term cl ++ + str")") + | CC_case (_,b,[e1;e2]) -> + hov 0 (str"if " ++ pp_cc_term b ++ str" then" ++ fnl () ++ + str" " ++ hov 0 (pp_cc_term e1) ++ fnl () ++ + str"else" ++ fnl () ++ + str" " ++ hov 0 (pp_cc_term e2)) + | CC_case _ -> + hov 0 (str"<Case: not yet implemented>") + | CC_expr c -> + hov 0 (prterm c) + | CC_hole c -> + (str"(?::" ++ prterm c ++ str")") + diff --git a/contrib/correctness/putil.mli b/contrib/correctness/putil.mli new file mode 100644 index 00000000..b44774ae --- /dev/null +++ b/contrib/correctness/putil.mli @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: putil.mli,v 1.3.2.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Pp +open Names +open Term +open Pmisc +open Ptype +open Past +open Penv + +val is_mutable : 'a ml_type_v -> bool +val is_pure : 'a ml_type_v -> bool + +val named_app : ('a -> 'b) -> 'a assertion -> 'b assertion +val pre_app : ('a -> 'b) -> 'a precondition -> 'b precondition +val post_app : ('a -> 'b) -> 'a postcondition -> 'b postcondition + +val anonymous : 'a -> 'a assertion +val anonymous_pre : bool -> 'a -> 'a precondition +val out_post : 'a postcondition option -> 'a +val pre_of_assert : bool -> 'a assertion -> 'a precondition +val assert_of_pre : 'a precondition -> 'a assertion + +val force_post_name : 'a postcondition option -> 'a postcondition option +val force_bool_name : 'a postcondition option -> 'a postcondition option + +val make_before_after : constr -> constr + +val traverse_binders : local_env -> (type_v binder) list -> local_env +val initial_renaming : local_env -> Prename.t + +val apply_pre : Prename.t -> local_env -> constr precondition -> + constr precondition +val apply_post : Prename.t -> local_env -> string -> constr postcondition -> + constr postcondition +val apply_assert : Prename.t -> local_env -> constr assertion -> + constr assertion + +val type_v_subst : (identifier * identifier) list -> type_v -> type_v +val type_c_subst : (identifier * identifier) list -> type_c -> type_c + +val type_v_rsubst : (identifier * constr) list -> type_v -> type_v +val type_c_rsubst : (identifier * constr) list -> type_c -> type_c + +val make_arrow : ('a ml_type_v binder) list -> 'a ml_type_c -> 'a ml_type_v + +val is_mutable_in_env : local_env -> identifier -> bool +val now_vars : local_env -> constr -> identifier list + +val deref_type : 'a ml_type_v -> 'a ml_type_v +val dearray_type : 'a ml_type_v -> 'a * 'a ml_type_v +val constant_unit : unit -> constr ml_type_v +val v_of_constr : constr -> constr ml_type_v +val c_of_constr : constr -> constr ml_type_c +val is_pure_cci : constr -> bool + +(* pretty printers *) + +val pp_type_v : type_v -> std_ppcmds +val pp_type_c : type_c -> std_ppcmds +val pp_cc_term : cc_term -> std_ppcmds + diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml new file mode 100644 index 00000000..58bef673 --- /dev/null +++ b/contrib/correctness/pwp.ml @@ -0,0 +1,347 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pwp.ml,v 1.8.2.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Util +open Names +open Libnames +open Term +open Termops +open Environ +open Nametab + +open Pmisc +open Ptype +open Past +open Putil +open Penv +open Peffect +open Ptyping +open Prename + +(* In this module: + * - we try to insert more annotations to achieve a greater completeness; + * - we recursively propagate annotations inside programs; + * - we normalize boolean expressions. + * + * The propagation schemas are the following: + * + * 1. (f a1 ... an) -> (f a1 ... an) {Qf} if the ai are functional + * + * 2. (if e1 then e2 else e3) {Q} -> (if e1 then e2 {Q} else e3 {Q}) {Q} + * + * 3. (let x = e1 in e2) {Q} -> (let x = e1 in e2 {Q}) {Q} + *) + +(* force a post-condition *) +let update_post env top ef c = + let i,o = Peffect.get_repr ef in + let al = + List.fold_left + (fun l id -> + if is_mutable_in_env env id then + if is_write ef id then l else (id,at_id id "")::l + else if is_at id then + let (uid,d) = un_at id in + if is_mutable_in_env env uid & d="" then + (id,at_id uid top)::l + else + l + else + l) + [] (global_vars (Global.env()) c) + in + subst_in_constr al c + +let force_post up env top q e = + let (res,ef,p,_) = e.info.kappa in + let q' = + if up then option_app (named_app (update_post env top ef)) q else q + in + let i = { env = e.info.env; kappa = (res,ef,p,q') } in + { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i } + +(* put a post-condition if none is present *) +let post_if_none_up env top q = function + | { post = None } as p -> force_post true env top q p + | p -> p + +let post_if_none env q = function + | { post = None } as p -> force_post false env "" q p + | p -> p + +(* [annotation_candidate p] determines if p is a candidate for a + * post-condition *) + +let annotation_candidate = function + | { desc = If _ | Let _ | LetRef _ ; post = None } -> true + | _ -> false + +(* [extract_pre p] erase the pre-condition of p and returns it *) +let extract_pre pr = + let (v,e,p,q) = pr.info.kappa in + { desc = pr.desc; pre = []; post = pr.post; loc = pr.loc; + info = { env = pr.info.env; kappa = (v,e,[],q) } }, + p + +(* adds some pre-conditions *) +let add_pre p1 pr = + let (v,e,p,q) = pr.info.kappa in + let p' = p1 @ p in + { desc = pr.desc; pre = p'; post = pr.post; loc = pr.loc; + info = { env = pr.info.env; kappa = (v,e,p',q) } } + +(* change the statement *) +let change_desc p d = + { desc = d; pre = p.pre; post = p.post; loc = p.loc; info = p.info } + +let create_bool_post c = + Some { a_value = c; a_name = Name (bool_name()) } + +(* [normalize_boolean b] checks if the boolean expression b (of type bool) is + * annotated, and if it is not the case tries to add the annotation + * (if result then c=true else c=false) if b is an expression c. + *) + +let is_bool = function + | TypePure c -> + (match kind_of_term (strip_outer_cast c) with + | Ind op -> + string_of_id (id_of_global (IndRef op)) = "bool" + | _ -> false) + | _ -> false + +let normalize_boolean ren env b = + let ((res,v),ef,p,q) = b.info.kappa in + Perror.check_no_effect b.loc ef; + if is_bool v then + match q with + | Some _ -> + (* il y a une annotation : on se contente de lui forcer un nom *) + let q = force_bool_name q in + { desc = b.desc; pre = b.pre; post = q; loc = b.loc; + info = { env = b.info.env; kappa = ((res,v),ef,p,q) } } + | None -> begin + (* il n'y a pas d'annotation : on cherche ą en mettre une *) + match b.desc with + Expression c -> + let c' = Term.applist (constant "annot_bool",[c]) in + let ty = type_of_expression ren env c' in + let (_,q') = Hipattern.match_sigma ty in + let q' = Some { a_value = q'; a_name = Name (bool_name()) } in + { desc = Expression c'; + pre = b.pre; post = q'; loc = b.loc; + info = { env = b.info.env; kappa = ((res, v),ef,p,q') } } + | _ -> b + end + else + Perror.should_be_boolean b.loc + +(* [decomp_boolean c] returns the specs R and S of a boolean expression *) + +let decomp_boolean = function + | Some { a_value = q } -> + Reductionops.whd_betaiota (Term.applist (q, [constant "true"])), + Reductionops.whd_betaiota (Term.applist (q, [constant "false"])) + | _ -> invalid_arg "Ptyping.decomp_boolean" + +(* top point of a program *) + +let top_point = function + | PPoint (s,_) as p -> s,p + | p -> let s = label_name() in s,PPoint(s,p) + +let top_point_block = function + | (Label s :: _) as b -> s,b + | b -> let s = label_name() in s,(Label s)::b + +let abstract_unit q = abstract [result_id,constant "unit"] q + +(* [add_decreasing env ren ren' phi r bl] adds the decreasing condition + * phi(ren') r phi(ren) + * to the last assertion of the block [bl], which is created if needed + *) + +let add_decreasing env inv (var,r) lab bl = + let ids = now_vars env var in + let al = List.map (fun id -> (id,at_id id lab)) ids in + let var_lab = subst_in_constr al var in + let dec = Term.applist (r, [var;var_lab]) in + let post = match inv with + None -> anonymous dec + | Some i -> { a_value = conj dec i.a_value; a_name = i.a_name } + in + bl @ [ Assert post ] + +(* [post_last_statement env top q bl] annotates the last statement of the + * sequence bl with q if necessary *) + +let post_last_statement env top q bl = + match List.rev bl with + | Statement e :: rem when annotation_candidate e -> + List.rev ((Statement (post_if_none_up env top q e)) :: rem) + | _ -> bl + +(* [propagate_desc] moves the annotations inside the program + * info is the typing information coming from the outside annotations *) +let rec propagate_desc ren info d = + let env = info.env in + let (_,_,p,q) = info.kappa in + match d with + | If (e1,e2,e3) -> + (* propagation number 2 *) + let e1' = normalize_boolean ren env (propagate ren e1) in + if e2.post = None or e3.post = None then + let top = label_name() in + let ren' = push_date ren top in + PPoint (top, If (e1', + propagate ren' (post_if_none_up env top q e2), + propagate ren' (post_if_none_up env top q e3))) + else + If (e1', propagate ren e2, propagate ren e3) + | Aff (x,e) -> + Aff (x, propagate ren e) + | TabAcc (ch,x,e) -> + TabAcc (ch, x, propagate ren e) + | TabAff (ch,x,({desc=Expression c} as e1),e2) -> + let p = Pmonad.make_pre_access ren env x c in + let e1' = add_pre [(anonymous_pre true p)] e1 in + TabAff (false, x, propagate ren e1', propagate ren e2) + | TabAff (ch,x,e1,e2) -> + TabAff (ch, x, propagate ren e1, propagate ren e2) + | Apply (f,l) -> + Apply (propagate ren f, List.map (propagate_arg ren) l) + | SApp (f,l) -> + let l = + List.map (fun e -> normalize_boolean ren env (propagate ren e)) l + in + SApp (f, l) + | Lam (bl,e) -> + Lam (bl, propagate ren e) + | Seq bl -> + let top,bl = top_point_block bl in + let bl = post_last_statement env top q bl in + Seq (propagate_block ren env bl) + | While (b,inv,var,bl) -> + let b = normalize_boolean ren env (propagate ren b) in + let lab,bl = top_point_block bl in + let bl = add_decreasing env inv var lab bl in + While (b,inv,var,propagate_block ren env bl) + | LetRef (x,e1,e2) -> + let top = label_name() in + let ren' = push_date ren top in + PPoint (top, LetRef (x, propagate ren' e1, + propagate ren' (post_if_none_up env top q e2))) + | Let (x,e1,e2) -> + let top = label_name() in + let ren' = push_date ren top in + PPoint (top, Let (x, propagate ren' e1, + propagate ren' (post_if_none_up env top q e2))) + | LetRec (f,bl,v,var,e) -> + LetRec (f, bl, v, var, propagate ren e) + | PPoint (s,d) -> + PPoint (s, propagate_desc ren info d) + | Debug _ | Variable _ + | Acc _ | Expression _ as d -> d + + +(* [propagate] adds new annotations if possible *) +and propagate ren p = + let env = p.info.env in + let p = match p.desc with + | Apply (f,l) -> + let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in + if ok then + let q = option_app (named_app (real_subst_in_constr so)) qapp in + post_if_none env q p + else + p + | _ -> p + in + let d = propagate_desc ren p.info p.desc in + let p = change_desc p d in + match d with + | Aff (x,e) -> + let e1,p1 = extract_pre e in + change_desc (add_pre p1 p) (Aff (x,e1)) + + | TabAff (check, x, ({ desc = Expression _ } as e1), e2) -> + let e1',p1 = extract_pre e1 in + let e2',p2 = extract_pre e2 in + change_desc (add_pre (p1@p2) p) (TabAff (check,x,e1',e2')) + + | While (b,inv,_,_) -> + let _,s = decomp_boolean b.post in + let s = make_before_after s in + let q = match inv with + None -> Some (anonymous s) + | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name } + in + let q = option_app (named_app abstract_unit) q in + post_if_none env q p + + | SApp ([Variable id], [e1;e2]) + when id = connective_and or id = connective_or -> + let (_,_,_,q1) = e1.info.kappa + and (_,_,_,q2) = e2.info.kappa in + let (r1,s1) = decomp_boolean q1 + and (r2,s2) = decomp_boolean q2 in + let q = + let conn = if id = connective_and then "spec_and" else "spec_or" in + let c = Term.applist (constant conn, [r1; s1; r2; s2]) in + let c = Reduction.whd_betadeltaiota (Global.env()) c in + create_bool_post c + in + let d = + SApp ([Variable id; + Expression (out_post q1); + Expression (out_post q2)], + [e1; e2] ) + in + post_if_none env q (change_desc p d) + + | SApp ([Variable id], [e1]) when id = connective_not -> + let (_,_,_,q1) = e1.info.kappa in + let (r1,s1) = decomp_boolean q1 in + let q = + let c = Term.applist (constant "spec_not", [r1; s1]) in + let c = Reduction.whd_betadeltaiota (Global.env ()) c in + create_bool_post c + in + let d = SApp ([Variable id; Expression (out_post q1)], [ e1 ]) in + post_if_none env q (change_desc p d) + + | _ -> p + +and propagate_arg ren = function + | Type _ | Refarg _ as a -> a + | Term e -> Term (propagate ren e) + + +and propagate_block ren env = function + | [] -> + [] + | (Statement p) :: (Assert q) :: rem when annotation_candidate p -> + (* TODO: plutot p.post = None ? *) + let q' = + let ((id,v),_,_,_) = p.info.kappa in + let tv = Pmonad.trad_ml_type_v ren env v in + named_app (abstract [id,tv]) q + in + let p' = post_if_none env (Some q') p in + (Statement (propagate ren p')) :: (Assert q) + :: (propagate_block ren env rem) + | (Statement p) :: rem -> + (Statement (propagate ren p)) :: (propagate_block ren env rem) + | (Label s as x) :: rem -> + x :: propagate_block (push_date ren s) env rem + | x :: rem -> + x :: propagate_block ren env rem diff --git a/contrib/correctness/pwp.mli b/contrib/correctness/pwp.mli new file mode 100644 index 00000000..015031a0 --- /dev/null +++ b/contrib/correctness/pwp.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Certification of Imperative Programs / Jean-Christophe Filliātre *) + +(* $Id: pwp.mli,v 1.2.16.1 2004/07/16 19:30:06 herbelin Exp $ *) + +open Term +open Penv + +val update_post : local_env -> string -> Peffect.t -> constr -> constr + +val propagate : Prename.t -> typed_program -> typed_program |