diff options
51 files changed, 6447 insertions, 0 deletions
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v new file mode 100644 index 000000000..6fe72671a --- /dev/null +++ b/contrib/correctness/Arrays.v @@ -0,0 +1,82 @@ +(***********************************************************************) +(* 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$ *) + +(*******************************************) +(* Functional arrays, for use in Programs. *) +(*******************************************) + +(* 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. + +Implicit Arguments On. + + +(* The type of arrays *) + +Parameter array : Z -> Set -> Set. + + +(* Functions to create, access and modify arrays *) + +Parameter new : (n:Z)(T:Set) T -> (array n T). + +Parameter access : (n:Z)(T:Set) (array n T) -> Z -> T. + +Parameter store : (n:Z)(T:Set) (array n T) -> Z -> T -> (array n T). + + +(* Axioms *) + +Axiom new_def : (n:Z)(T:Set)(v0:T) + (i:Z) `0<=i<n` -> (access (new n v0) i) = v0. + +Axiom store_def_1 : (n:Z)(T:Set)(t:(array n T))(v:T) + (i:Z) `0<=i<n` -> + (access (store t i v) i) = v. + +Axiom store_def_2 : (n:Z)(T:Set)(t:(array n T))(v:T) + (i:Z)(j:Z) `0<=i<n` -> `0<=j<n` -> + `i <> j` -> + (access (store t i v) j) = (access t j). + +Hints Resolve new_def store_def_1 store_def_2 : datatypes v62. + +(* A tactic to simplify access in arrays *) + +Tactic Definition ArrayAccess [$i $j $H] := + [<:tactic: < + 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 ] ] + >>]. + +(* Syntax and pretty-print for arrays *) + +Grammar command command0 := + array_access + [ ident($t) "#" "[" command($c) "]" ] -> [ <<(access $t $c)>> ]. + +Syntax constr level 0 : + array_access + [ (APPLIST <<access>> ($VAR $t) $c) ] -> [ $t "#[" $c:L "]" ]. diff --git a/contrib/correctness/Arrays_stuff.v b/contrib/correctness/Arrays_stuff.v new file mode 100644 index 000000000..edb3c8058 --- /dev/null +++ b/contrib/correctness/Arrays_stuff.v @@ -0,0 +1,16 @@ +(***********************************************************************) +(* 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$ *) + +Require Export Exchange. +Require Export Permut. +Require Export Sorted. + diff --git a/contrib/correctness/Exchange.v b/contrib/correctness/Exchange.v new file mode 100644 index 000000000..2a449ba25 --- /dev/null +++ b/contrib/correctness/Exchange.v @@ -0,0 +1,94 @@ +(***********************************************************************) +(* 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$ *) + +(****************************************************************************) +(* Exchange of two elements in an array *) +(* Definition and properties *) +(****************************************************************************) + +Require ProgInt. +Require Arrays. + +Implicit Arguments On. + +(* Definition *) + +Inductive exchange [n:Z; A:Set; t,t':(array n A); i,j:Z] : Prop := + exchange_c : + `0<=i<n` -> `0<=j<n` -> + (t#[i] = t'#[j]) -> + (t#[j] = t'#[i]) -> + ((k:Z)`0<=k<n` -> `k<>i` -> `k<>j` -> t#[k] = t'#[k]) -> + (exchange t t' i j). + +(* Properties about exchanges *) + +Lemma exchange_1 : (n:Z)(A:Set)(t:(array n A)) + (i,j:Z) `0<=i<n` -> `0<=j<n` -> + (access (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. +Save. + +Hints Resolve exchange_1 : v62 datatypes. + + +Lemma exchange_proof : + (n:Z)(A:Set)(t:(array n A)) + (i,j:Z) `0<=i<n` -> `0<=j<n` -> + (exchange (store (store t i (access t j)) j (access 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 (access t j)) (access t i) H_j H_k not_j_k). +Auto with datatypes. +Save. + +Hints Resolve exchange_proof : v62 datatypes. + + +Lemma exchange_sym : + (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. +Save. + +Hints Resolve exchange_sym : v62 datatypes. + + +Lemma exchange_id : + (n:Z)(A:Set)(t,t':(array n A))(i,j:Z) + (exchange t t' i j) -> + i=j -> + (k:Z) `0 <= k < n` -> (access t k)=(access 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. +Save. + +Hints Resolve exchange_id : v62 datatypes. diff --git a/contrib/correctness/MakeProgramsState.v b/contrib/correctness/MakeProgramsState.v new file mode 100644 index 000000000..fac2d8fba --- /dev/null +++ b/contrib/correctness/MakeProgramsState.v @@ -0,0 +1,2 @@ +Require Programs. +Save State Programs "etat avec la tactics Programs". diff --git a/contrib/correctness/Permut.v b/contrib/correctness/Permut.v new file mode 100644 index 000000000..0963c2b14 --- /dev/null +++ b/contrib/correctness/Permut.v @@ -0,0 +1,183 @@ +(***********************************************************************) +(* 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$ *) + +(****************************************************************************) +(* Permutations of elements in arrays *) +(* Definition and properties *) +(****************************************************************************) + +Require ProgInt. +Require Arrays. +Require Export Exchange. + +Require Omega. + +Implicit Arguments On. + +(* 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 : + (t,t':(array n A))(i,j:Z)(exchange t t' i j) -> (permut t t') + | permut_refl : + (t:(array n A))(permut t t) + | permut_sym : + (t,t':(array n A))(permut t t') -> (permut t' t) + | permut_trans : + (t,t',t'':(array n A)) + (permut t t') -> (permut t' t'') -> (permut t t''). + +Hints 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 : + (t,t':(array n A))(i,j:Z)`g <= i <= d` -> `g <= j <= d` + -> (exchange t t' i j) -> (sub_permut g d t t') + | sub_permut_refl : + (t:(array n A))(sub_permut g d t t) + | sub_permut_sym : + (t,t':(array n A))(sub_permut g d t t') -> (sub_permut g d t' t) + | sub_permut_trans : + (t,t',t'':(array n A)) + (sub_permut g d t t') -> (sub_permut g d t' t'') + -> (sub_permut g d t t''). + +Hints 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] + (i:Z) `g <= i <= d` -> t#[i] = t'#[i]. + +(* array_id is an equivalence relation *) + +Lemma array_id_refl : + (n:Z)(A:Set)(t:(array n A))(g,d:Z) + (array_id t t g d). +Proof. +Unfold array_id. +Auto with datatypes. +Save. + +Hints Resolve array_id_refl : v62 datatypes. + +Lemma array_id_sym : + (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. Intros. +Symmetry; Auto with datatypes. +Save. + +Hints Resolve array_id_sym : v62 datatypes. + +Lemma array_id_trans : + (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. Intros. +Apply trans_eq with y:=t'#[i]; Auto with datatypes. +Save. + +Hints Resolve array_id_trans: v62 datatypes. + +(* Outside the segment [g,d] the elements are equal *) + +Lemma sub_permut_id : + (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. Induction 1; Intros. +Elim H2; Intros. +Unfold array_id; 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. +Save. + +Hints Resolve sub_permut_id. + +Lemma sub_permut_eq : + (n:Z)(A:Set)(t,t':(array n A))(g,d:Z) + (sub_permut g d t t') -> + (i:Z) (`0<=i<g` \/ `d<i<n`) -> t#[i]=t'#[i]. +Proof. +Intros n A t t' g d Htt' i Hi. +Elim (sub_permut_id Htt'). Unfold array_id. +Intros. +Elim Hi; [ Intro; Apply H; Omega | Intro; Apply H0; Omega ]. +Save. + +(* sub_permut is a particular case of permutation *) + +Lemma sub_permut_is_permut : + (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. Induction 1; Intros; EAuto with datatypes. +Save. + +Hints 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 : + (N:Z)(A:Set)(t,t':(array N A)) + (g,g',d,d':Z) `d < g` + -> (sub_permut g d t t') -> (sub_permut g' d' t t'). +Proof. +Intros N A t t' g g' d d' Hdg. +(Induction 1; Intros). +(Absurd `g <= d`; Omega). +Auto with datatypes. +Auto with datatypes. +EAuto with datatypes. +Save. + +(* A sub-permutation on a segment may be extended to any segment that + * contains the first one. + *) + +Lemma sub_permut_extension : + (N:Z)(A:Set)(t,t':(array N A)) + (g,g',d,d':Z) `g' <= g` -> `d <= d'` + -> (sub_permut g d t t') -> (sub_permut g' d' t t'). +Proof. +Intros N A t t' g g' d d' Hgg' Hdd'. +(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. +Save. diff --git a/contrib/correctness/ProgBool.v b/contrib/correctness/ProgBool.v new file mode 100644 index 000000000..026390a01 --- /dev/null +++ b/contrib/correctness/ProgBool.v @@ -0,0 +1,122 @@ +(***********************************************************************) +(* 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$ *) + +Require Export Compare_dec. +Require Export Peano_dec. +Require ZArith. +Require Sumbool. + +(* Programs use the booleans of type "bool", so we tranform any decidability + * proof, in type sumbool, into a function returning a boolean with the + * correct specification, through the following function: + *) + +Definition bool_of_sumbool : + (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }. +Proof. +Intros A B H. +Elim H; [ Intro; Exists true; Assumption + | Intro; Exists false; Assumption ]. +Save. + +Definition annot_bool : + (b:bool) { b':bool | if b' then b=true else b=false }. +Proof. +Intro b. +Exists b. Case b; Trivial. +Save. + + +(* Logical connectives *) + +Definition spec_and := [A,B,C,D:Prop][b:bool]if b then A /\ C else B \/ D. + +Definition prog_bool_and : + (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool 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. +Save. + +Definition spec_or := [A,B,C,D:Prop][b:bool]if b then A \/ C else B /\ D. + +Definition prog_bool_or : + (Q1,Q2:bool->Prop) (sig bool Q1) -> (sig bool 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. +Save. + +Definition spec_not:= [A,B:Prop][b:bool]if b then B else A. + +Definition prog_bool_not : + (Q:bool->Prop) (sig bool 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. +Save. + + +(* Application: the decidability of equality and order relations over + * type Z give some boolean functions with the adequate specification. + * For instance, Z_lt_ge_bool has type: + * + * (x,y:Z){b:bool | if b then `x < y` else `x >= y`} + *) + +Definition Z_lt_ge_bool := [x,y:Z](bool_of_sumbool ? ? (Z_lt_ge_dec x y)). +Definition Z_ge_lt_bool := [x,y:Z](bool_of_sumbool ? ? (Z_ge_lt_dec x y)). + +Definition Z_le_gt_bool := [x,y:Z](bool_of_sumbool ? ? (Z_le_gt_dec x y)). +Definition Z_gt_le_bool := [x,y:Z](bool_of_sumbool ? ? (Z_gt_le_dec x y)). + +Definition Z_eq_bool := [x,y:Z](bool_of_sumbool ? ? (Z_eq_dec x y)). +Definition Z_noteq_bool := [x,y:Z](bool_of_sumbool ? ? (Z_noteq_dec x y)). + +Definition Zeven_odd_bool := [x:Z](bool_of_sumbool ? ? (Zeven_odd_dec x)). + +(* ... and similarly for type nat *) + +Definition notzerop := [n:nat] (sumbool_not ? ? (zerop n)). +Definition lt_ge_dec : (x,y:nat){(lt x y)}+{(ge x y)} := + [n,m:nat] (sumbool_not ? ? (le_lt_dec m n)). + +Definition nat_lt_ge_bool := + [x,y:nat](bool_of_sumbool ? ? (lt_ge_dec x y)). +Definition nat_ge_lt_bool := + [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (lt_ge_dec x y))). + +Definition nat_le_gt_bool := + [x,y:nat](bool_of_sumbool ? ? (le_gt_dec x y)). +Definition nat_gt_le_bool := + [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (le_gt_dec x y))). + +Definition nat_eq_bool := + [x,y:nat](bool_of_sumbool ? ? (eq_nat_dec x y)). +Definition nat_noteq_bool := + [x,y:nat](bool_of_sumbool ? ? (sumbool_not ? ? (eq_nat_dec x y))). + +Definition zerop_bool := [x:nat](bool_of_sumbool ? ? (zerop x)). +Definition notzerop_bool := [x:nat](bool_of_sumbool ? ? (notzerop x)). diff --git a/contrib/correctness/ProgInt.v b/contrib/correctness/ProgInt.v new file mode 100644 index 000000000..ec46e2de6 --- /dev/null +++ b/contrib/correctness/ProgInt.v @@ -0,0 +1,19 @@ +(***********************************************************************) +(* 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$ *) + +Require Export ZArith. +Require Export ZArith_dec. + +Theorem Znotzero : (x:Z){`x<>0`}+{`x=0`}. +Proof. +Intro x. Elim (Z_eq_dec x `0`) ; Auto. +Save. diff --git a/contrib/correctness/ProgWf.v b/contrib/correctness/ProgWf.v new file mode 100644 index 000000000..f51506d21 --- /dev/null +++ b/contrib/correctness/ProgWf.v @@ -0,0 +1,85 @@ +(***********************************************************************) +(* 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$ *) + +Require ZArith. +Require Export Wf_nat. + +(* Well-founded relations on Z. *) + +(* We define the following family of relations on ZxZ : + * + * x (Zwf c) y iff c <= x < y + *) + +Definition Zwf := [c:Z][x,y:Z] `c <= x` /\ `c <= y` /\ `x < y`. + + +(* and we prove that (Zwf c) is well founded *) + +Section wf_proof. + +Variable c : Z. + +(* The proof of well-foundness is classic : we do the proof by induction + * on a measure in nat, which is here |x-c| *) + +Local f := [z:Z](absolu (Zminus z c)). + +Lemma Zwf_well_founded : (well_founded Z (Zwf c)). +Proof. +Apply well_founded_lt_compat with f:=f. +Unfold Zwf f. +Intros. +Apply absolu_lt. +Unfold Zminus. Split. +Apply Zle_left; Intuition. +Rewrite (Zplus_sym x `-c`). Rewrite (Zplus_sym y `-c`). +Apply Zlt_reg_l; Intuition. +Save. + +End wf_proof. + +Hints Resolve Zwf_well_founded : datatypes v62. + + +(* We also define the other family of relations : + * + * x (Zwf_up c) y iff y < x <= c + *) + +Definition Zwf_up := [c:Z][x,y:Z] `y < x <= c`. + +(* and we prove that (Zwf_up c) is well founded *) + +Section wf_proof_up. + +Variable c : Z. + +(* The proof of well-foundness is classic : we do the proof by induction + * on a measure in nat, which is here |c-x| *) + +Local f := [z:Z](absolu (Zminus c z)). + +Lemma Zwf_up_well_founded : (well_founded Z (Zwf_up c)). +Proof. +Apply well_founded_lt_compat with f:=f. +Unfold Zwf_up f. +Intros. +Apply absolu_lt. +Unfold Zminus. Split. +Apply Zle_left; Intuition. +Apply Zlt_reg_l; Unfold Zlt; Rewrite <- Zcompare_Zopp; Intuition. +Save. + +End wf_proof_up. + +Hints Resolve Zwf_up_well_founded : datatypes v62. diff --git a/contrib/correctness/Programs.v b/contrib/correctness/Programs.v new file mode 100644 index 000000000..34d843908 --- /dev/null +++ b/contrib/correctness/Programs.v @@ -0,0 +1,36 @@ +(***********************************************************************) +(* 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$ *) + +(* Correctness is base on the tactic Refine (developped on purpose) *) + +Require Export Refine. + +Require Export Tuples. + +Require Export ProgInt. +Require Export ProgBool. +Require Export ProgWf. + +Require Export Arrays. + +Declare ML Module + "misc_utils" "effects" "renamings" "progTypes" "progAst" + "prog_errors" "prog_env" "prog_utils" + "prog_db" "prog_cci" "monad" "tradEnv" + "prog_red" "prog_typing" "prog_wp" "mlise" "prog_tactic" + "pprog". + +Token "'". + + + + diff --git a/contrib/correctness/ProgramsExtraction.v b/contrib/correctness/ProgramsExtraction.v new file mode 100644 index 000000000..23394dc18 --- /dev/null +++ b/contrib/correctness/ProgramsExtraction.v @@ -0,0 +1,30 @@ +(***********************************************************************) +(* 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$ *) + +Require Export Extraction. + +Extract Inductive unit => unit [ "()" ]. +Extract Inductive bool => bool [ true false ]. +Extract Inductive sumbool => bool [ true false ]. + +Require Export Programs. + +Declare ML Module "prog_extract". + +Grammar vernac vernac := + 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 000000000..0fe692167 --- /dev/null +++ b/contrib/correctness/Programs_stuff.v @@ -0,0 +1,13 @@ +(***********************************************************************) +(* 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$ *) + +Require Export Arrays_stuff. diff --git a/contrib/correctness/Sorted.v b/contrib/correctness/Sorted.v new file mode 100644 index 000000000..9c99d6ed5 --- /dev/null +++ b/contrib/correctness/Sorted.v @@ -0,0 +1,196 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* Library about sorted (sub-)arrays / Nicolas Magaud, July 1998 *) + +(* $Id$ *) + +Require Export Arrays. +Require Permut. + +Require ZArithRing. +Require Omega. + +Implicit Arguments On. + +(* Definition *) + +Definition sorted_array := + [N:Z][A:(array N Z)][deb:Z][fin:Z] + `deb<=fin` -> (x:Z) `x>=deb` -> `x<fin` -> (Zle 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 : + (N:Z)(A:(array N Z))(n:Z)(m:Z) + (sorted_array A n m) + -> (k:Z)`k>=n` + -> (i:Z) `0<=i` -> `k+i<=m` + -> (Zle (access A k) (access A `k+i`)). +Proof. +Intros N A n m H_sorted k H_k i H_i. +Pattern i. Apply natlike_ind. +Intro. +Replace `k+0` with k; Omega. (*** Ring `k+0` => BUG ***) + +Intros. +Apply Zle_trans with m:=(access A `k+x`). +Apply H0 ; Omega. + +Unfold Zs. +Replace `k+(x+1)` with `(k+x)+1`. +Unfold sorted_array in H_sorted. +Apply H_sorted ; Omega. + +Omega. + +Assumption. +Save. + +(* one element and any of the following *) + +Lemma sorted_elements : + (N:Z)(A:(array N Z))(n:Z)(m:Z)(k:Z)(l:Z) + (sorted_array A n m) + -> `k>=n` -> `l<N` -> `k<=l` -> `l<=m` + -> (Zle (access A k) (access A l)). +Proof. +Intros. +Replace l with `k+(l-k)`. +Apply sorted_elements_1 with n:=n m:=m; [Assumption | Omega | Omega | Omega]. +Omega. +Save. + +Hints Resolve sorted_elements : datatypes v62. + +(* A sub-array of a sorted array is sorted *) + +Lemma sub_sorted_array : (N:Z)(A:(array N Z))(deb:Z)(fin:Z)(i:Z)(j:Z) + (sorted_array A deb fin) -> + (`i>=deb` -> `j<=fin` -> `i<=j` -> (sorted_array A i j)). +Proof. +Unfold sorted_array. +Intros. +Apply H ; Omega. +Save. + +Hints Resolve sub_sorted_array : datatypes v62. + +(* Extension on the left of the property of being sorted *) + +Lemma left_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z) + `i>0` -> `j<N` -> (sorted_array A i j) + -> (Zle A#[`i-1`] A#[i]) -> (sorted_array A `i-1` j). +Proof. +(Intros; Unfold sorted_array ; 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. +Save. + +(* Extension on the right *) + +Lemma right_extension : (N:Z)(A:(array N Z))(i:Z)(j:Z) + `i>=0` -> `j<N-1` -> (sorted_array A i j) + -> (Zle A#[j] A#[`j+1`]) -> (sorted_array A i `j+1`). +Proof. +(Intros; Unfold sorted_array ; Intros). +Elim (Z_lt_ge_dec x j). +Intro Hcut. +Apply H1 ; Omega. + +Intro HCut. +Replace x with j ; [Assumption | Omega]. +Save. + +(* Substitution of the leftmost value by a smaller value *) + +Lemma left_substitution : + (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z) + `i>=0` -> `j<N` -> (sorted_array A i j) + -> (Zle 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 ; 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:=(access A i) ; [Assumption | Apply H_sorted ; Omega]. + +(Rewrite store_def_2; Try Omega). +(Rewrite store_def_2; Try Omega). +Apply H_sorted ; Omega. +Omega. +Save. + +(* Substitution of the rightmost value by a larger value *) + +Lemma right_substitution : + (N:Z)(A:(array N Z))(i:Z)(j:Z)(v:Z) + `i>=0` -> `j<N` -> (sorted_array A i j) + -> (Zle 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 ; 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:=(access 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. +Save. + +(* Affectation outside of the sorted region *) + +Lemma no_effect : + (N:Z)(A:(array N Z))(i:Z)(j:Z)(k:Z)(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 ; Intros. +Rewrite store_def_2 ; Try Omega. +Rewrite store_def_2 ; Try Omega. +Apply H1 ; Assumption. +Save. + +Lemma sorted_array_id : (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. +Intros Hgd x H1x H2x. +Rewrite <- (Hid x); [ Idtac | Omega ]. +Rewrite <- (Hid `x+1`); [ Idtac | Omega ]. +Apply Hsorted; Assumption. +Save. diff --git a/contrib/correctness/Tuples.v b/contrib/correctness/Tuples.v new file mode 100644 index 000000000..f9a3b56b7 --- /dev/null +++ b/contrib/correctness/Tuples.v @@ -0,0 +1,106 @@ +(***********************************************************************) +(* 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$ *) + +(* 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 : (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 : (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 : (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 : (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 : (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 : (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 : (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 : (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 : (x1:T1)(x2:T2)(x3:T3)(P x1 x2 x3) + -> (dep_tuple_3 T1 T2 T3 P). + + diff --git a/contrib/correctness/past.ml b/contrib/correctness/past.ml new file mode 100644 index 000000000..5dd0301eb --- /dev/null +++ b/contrib/correctness/past.ml @@ -0,0 +1,118 @@ +(***********************************************************************) +(* 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$ *) + +open Term +open Ptype + +(* Programmes impératifs *) + +type termination = RecArg of int + | Wf of Coqast.t * Coqast.t + +type variable = Names.identifier + +type pattern = + PatVar of Names.identifier + | PatConstruct of Names.identifier * ((Names.section_path * int) * int) + | PatAlias of pattern * Names.identifier + | PatPair of pattern * pattern + | PatApp of pattern list + +type epattern = + ExnConstant of Names.identifier + | ExnBind of Names.identifier * Names.identifier + +type ('a,'b) block_st = + Label of string + | Assert of 'b assertion + | Statement of 'a + +type ('a,'b) block = ('a,'b) block_st list + +(* type of programs with assertions of type 'b and info of type 'a *) + +type ('a,'b) t = + { desc : ('a,'b) t_desc ; + pre : 'b precondition list ; + post : 'b postcondition option ; + loc : Coqast.loc ; + info : 'a } + +and ('a,'b) t_desc = + Var 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) (* test *) + * 'b assertion option (* invariant *) + * ('b * 'b) (* variant *) + * (('a,'b) t, 'b) block (* corps *) + | If of (('a,'b) t) * (('a,'b) t) * (('a,'b) t) + | Lam of 'b ml_type_v binder list * ('a,'b) t + | App of (('a,'b) t) * (('a,'b) arg) list + | SApp of (('a,'b) t_desc) list * (('a,'b) t) list (* for connectives *) + | LetRef of variable * (('a,'b) t) * (('a,'b) t) + | LetIn of variable * (('a,'b) t) * (('a,'b) t) + | LetRec of variable (* nom *) + * 'b ml_type_v binder list * 'b ml_type_v (* types *) + * ('b * 'b) (* variant *) + * ('a,'b) t (* corps *) + | PPoint of string * ('a,'b) t_desc + | Expression of constr + + | Debug of string * (('a,'b) t) + +and ('a,'b) arg = + Term of (('a,'b) t) + | Refarg of variable + | Type of 'b ml_type_v + +type program = (unit, Coqast.t) t + + +(* AST for intermediate constructions. + * + * We define an intermediate type between typed program (above) + * and CIC terms (constr), because we need to perform some eta-reductions + * (see prog_red.ml for details) + * + * But here types are already CIC terms (constr). + *) + +type cc_type = 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 (* dep. or not *) + * cc_type (* type of result *) + * cc_binder list + * (cc_term * constr) (* the matched term and its ind. type *) + * cc_term + | CC_lam of cc_binder list * cc_term + | CC_app of cc_term * cc_term list + | CC_tuple of bool (* dep. or not *) + * cc_type list * cc_term list + | CC_case of cc_type (* type of result *) + * (cc_term * constr) (* the test and its inductive type *) + * cc_term list (* branches *) + | CC_expr of constr + | CC_hole of cc_type + + diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli new file mode 100644 index 000000000..36022f208 --- /dev/null +++ b/contrib/correctness/past.mli @@ -0,0 +1,74 @@ +(***********************************************************************) +(* 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$ *) + +(* Generated automatically by ocamlc -i *) + +type termination = | RecArg of int | Wf of Coqast.t * Coqast.t +type variable = Names.identifier +type pattern = + | PatVar of Names.identifier + | PatConstruct of Names.identifier * ((Names.section_path * int) * int) + | PatAlias of pattern * Names.identifier + | PatPair of pattern * pattern + | PatApp of pattern list +type epattern = + | ExnConstant of Names.identifier + | ExnBind of Names.identifier * Names.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: Coqast.loc; + info: 'a } +and ('a, 'b) t_desc = + | Var 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 + | App 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 + | LetIn 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, Coqast.t) t +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 * Term.constr) * + 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 * Term.constr) * 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 000000000..4c0d08732 --- /dev/null +++ b/contrib/correctness/pcic.ml @@ -0,0 +1,173 @@ +(***********************************************************************) +(* 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$ *) + +open Names +open Term + +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.sp_of_id CCI id in true with Not_found -> false + +let ast_set = Ast.ope ("PROP", [ Ast.ide "Pos" ]) + +let tuple_n n = + let name = "tuple_" ^ string_of_int n in + let id = id_of_string name in + let l1n = Util.interval 1 n in + let params = + List.map + (fun i -> let id = id_of_string ("T" ^ string_of_int i) in (id, ast_set)) + l1n + in + let fields = + List.map + (fun i -> + let id = id_of_string + ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in + (false, (id, true, Ast.nvar ("T" ^ string_of_int i)))) + l1n + in + let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in + Record.definition_structure (false, id, params, fields, cons, mk_Set) + +let sig_n n = + let name = "sig_" ^ string_of_int n in + let id = id_of_string name in + let l1n = Util.interval 1 n in + let lT = + List.map (fun i -> id_of_string ("T" ^ string_of_int i)) l1n in + let lx = + List.map (fun i -> id_of_string ("x" ^ string_of_int i)) l1n in + let ty_p = List.fold_right (fun ti c -> mkArrow (mkVar ti) c) lT mkProp in + let arity = + let ar = + List.fold_right (fun ti c -> mkNamedProd ti mkSet c) lT + (mkArrow ty_p mkSet) in + mkCast (ar, mkType Univ.prop_univ) + in + let idp = id_of_string "P" in + let lc = + let app_sig = + let l = + (mkRel (2*n+3)) :: (List.map (fun id -> (mkVar id)) lT) @ [mkVar idp] + in + mkAppA (Array.of_list l) in + let app_p = + let l = (mkVar idp) :: (List.map (fun id -> mkVar id) lx) in + mkAppA (Array.of_list l) in + let c = mkArrow app_p app_sig in + let c = List.fold_right (fun (x,tx) c -> mkNamedProd x (mkVar tx) c) + (List.combine lx lT) c in + let c = mkNamedProd idp ty_p c in + let c = List.fold_right (fun ti c -> mkNamedProd ti mkSet c) lT c in + DLAMV (Name id, [| c |]) + in + let cname = id_of_string ("exist_" ^ string_of_int n) in + Declare.machine_minductive (Termenv.initial_assumptions()) (succ n) + [| id, Anonymous, arity, lc, [| cname |] |] true + +let tuple_name 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 name = Printf.sprintf "exist_%d" n in + if not (tuple_exists (id_of_string name)) then sig_n n; + name + end + else begin + let name = Printf.sprintf "Build_tuple_%d" n in + if not (tuple_exists (id_of_string name)) then tuple_n n; + name + end + +(* Binders. *) + +let trad_binding bl = + List.map (function + (id,CC_untyped_binder) -> (id,isevar) + | (id,CC_typed_binder ty) -> (id,ty)) bl + +let lambda_of_bl bl c = + let b = trad_binding bl in n_lambda c (List.rev b) + +(* The translation itself is quite easy. + letin are translated into Cases construtions *) + +let constr_of_prog p = + let rec trad = function + CC_var id -> VAR id + + (* 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),(e1,_),e2) -> + let c = trad e1 and c2 = trad e2 in + Term.applist (lambda_of_bl b c2, [c]) + + | CC_letin (dep,ty,bl,(e,info),e1) -> + let c1 = trad e1 + and c = trad e in + let l = [ lambda_of_bl bl c1 ] in + Term.mkMutCase (Term.ci_of_mind info) ty c l + + | CC_lam (bl,e) -> + let c = trad e in lambda_of_bl bl c + + | CC_app (f,args) -> + let c = trad f + and cargs = List.map trad args in + Term.applist (c,cargs) + + | CC_tuple (_,_,[e]) -> trad e + + | CC_tuple (false,_,[e1;e2]) -> + let c1 = trad e1 + and c2 = trad e2 in + Term.applist (constant "pair", [isevar;isevar;c1;c2]) + + | CC_tuple (dep,tyl,l) -> + let n = List.length l in + let cl = List.map trad l in + let name = tuple_name dep n in + let args = tyl @ cl in + Term.applist (constant name,args) + + | CC_case (ty,(b,info),el) -> + let c = trad b in + let cl = List.map trad el in + mkMutCase (Term.ci_of_mind info) ty c cl + + | CC_expr c -> c + + | CC_hole c -> make_hole c + + in + trad p + diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli new file mode 100644 index 000000000..21c3839d9 --- /dev/null +++ b/contrib/correctness/pcic.mli @@ -0,0 +1,20 @@ +(***********************************************************************) +(* 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$ *) + +open Past +open Term + + +(* transforms intermediate functional programs into CIC terms *) + +val constr_of_prog : cc_term -> constr + diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml new file mode 100644 index 000000000..046fa7f72 --- /dev/null +++ b/contrib/correctness/pcicenv.ml @@ -0,0 +1,109 @@ +(***********************************************************************) +(* 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$ *) + +open Names +open Term + +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 !) *) + +let add_sign (id,t) s = + if mem_sign s id then + modify_sign id t s + else + add_sign (id,t) s + +let cast_set c = make_type c mk_Set + +let set = make_type Term.mkSet (Term.Type Impuniv.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 = + Prog_env.fold_all + (fun (id,v) sign -> + match v with + Prog_env.TypeV (Ref _ | Array _) -> sign + | Prog_env.TypeV v -> + let ty = Monad.trad_ml_type_v ren env v in + add_sign (id,cast_set ty) sign + | Prog_env.Set -> add_sign (id,set) sign) + env (initial_sign()) + +(* [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 = + Prog_env.fold_all + (fun (id,v) sign -> + match v with + Prog_env.TypeV (Ref _ | Array _ as v) -> + let ty = Monad.trad_imp_type ren env v in + fast sign id ty + | Prog_env.TypeV v -> + let ty = Monad.trad_ml_type_v ren env v in + add_sign (id,cast_set ty) sign + | Prog_env.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) + (initial_sign()) + +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 = "" :: Renamings.all_dates ren in + result_of (sign_of (add_sign_d dates) ren env) res + +let before_after_sign_of ren = + let dates = "" :: Renamings.all_dates ren in + sign_of (add_sign_d dates) ren + +let before_sign_of ren = + let dates = Renamings.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 (Renamings.current_var ren id,c) sign) + ren + + diff --git a/contrib/correctness/pcicenv.mli b/contrib/correctness/pcicenv.mli new file mode 100644 index 000000000..e0bfd386b --- /dev/null +++ b/contrib/correctness/pcicenv.mli @@ -0,0 +1,37 @@ +(***********************************************************************) +(* 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$ *) + +open Penv +open Names +open Term + +(* 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 : Renamings.t -> local_env -> context + +(* env. Coq avec seulement les variables X de l'env. *) +val now_sign_of : Renamings.t -> local_env -> context + +(* + les variables X@d pour toutes les dates de l'env. *) +val before_sign_of : Renamings.t -> local_env -> context + +(* + les variables `avant' X@ *) +val before_after_sign_of : Renamings.t -> local_env -> context +val before_after_result_sign_of : ((identifier * constr) option) + -> Renamings.t -> local_env -> context + +(* env. des programmes traduits, avec les variables rennomées *) +val trad_sign_of : Renamings.t -> local_env -> context + diff --git a/contrib/correctness/pdb.ml b/contrib/correctness/pdb.ml new file mode 100644 index 000000000..125924fb2 --- /dev/null +++ b/contrib/correctness/pdb.ml @@ -0,0 +1,168 @@ +(***********************************************************************) +(* 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$ *) + +open Names + +open Ptype +open Past +open Penv + + +let cci_global id = + try + Machops.global (gLOB(initial_sign())) 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 -> Prog_errors.unbound_variable id locop + end + +let check_ref idl loc id = + if (not (List.mem id idl)) & (not (Prog_env.is_global id)) then + Prog_errors.unbound_reference id (Some loc) + +(* db types : just do nothing for the moment ! *) + +let rec db_type_v ids = function + | Ref v -> Ref (db_type_v ids v) + | Array (c,v) -> Array (c,db_type_v ids v) + | Arrow (bl,c) -> Arrow (List.map (db_binder ids) bl, db_type_c ids c) + | TypePure _ as v -> v +and db_type_c ids ((id,v),e,p,q) = + (id,db_type_v ids v), e, p, q + (* TODO: db_condition ? *) +and db_binder ids = function + (n, BindType v) -> (n, BindType (db_type_v ids v)) + | b -> b + +(* db binders *) + +let rec db_binders ((tids,pids,refs) as idl) = function + [] -> idl, [] + | (id, BindType (Ref _ | Array _ as v)) :: rem -> + let idl',rem' = db_binders (tids,pids,id::refs) rem in + idl', (id, BindType (db_type_v tids v)) :: rem' + | (id, BindType v) :: rem -> + let idl',rem' = db_binders (tids,id::pids,refs) rem in + idl', (id, BindType (db_type_v tids v)) :: 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 patterns *) + +let rec db_pattern = function + (PatVar id) as t -> + (try + let sp = Nametab.fw_sp_of_id id in + (match Environ.global_operator sp id with + Term.MutConstruct (x,y),_ -> [], PatConstruct (id,(x,y)) + | _ -> [id],t) + with Not_found -> [id],t) + | PatAlias (p,id) -> + let ids,p' = db_pattern p in ids,PatAlias (p',id) + | PatPair (p1,p2) -> + let ids1,p1' = db_pattern p1 in + let ids2,p2' = db_pattern p2 in + ids1@ids2, PatPair (p1',p2') + | PatApp pl -> + let ids,pl' = + List.fold_right + (fun p (ids,pl) -> + let ids',p' = db_pattern p in ids'@ids,p'::pl) pl ([],[]) in + ids,PatApp pl' + | PatConstruct _ -> + failwith "constructor in a pattern after parsing !" + + +(* 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 + (Var 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 e.loc x; + t + | Aff (x,e1) -> + check_ref refs e.loc x; + Aff (x, db idl e1) + | TabAcc (b,x,e1) -> + check_ref refs e.loc x; + TabAcc(b,x,db idl e1) + | TabAff (b,x,e1,e2) -> + check_ref refs 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) + | App (e1,l) -> + App (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) + | LetIn (x,e1,e2) -> + LetIn (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 + LetRec (f, bl, db_type_v tids' 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 = Var id } as t) -> + if List.mem id refs then Refarg id else Term (db idl t) + | Term t -> Term (db idl t) + | Type v -> Type (db_type_v tids v) + | 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 = Names.ids_of_sign (Vartab.initial_sign()) 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 000000000..4b031be6c --- /dev/null +++ b/contrib/correctness/pdb.mli @@ -0,0 +1,25 @@ +(***********************************************************************) +(* 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$ *) + +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 db_type_v : Names.identifier list -> 'a ml_type_v -> 'a ml_type_v + +val db_prog : program -> program + diff --git a/contrib/correctness/peffect.ml b/contrib/correctness/peffect.ml new file mode 100644 index 000000000..23d4dea34 --- /dev/null +++ b/contrib/correctness/peffect.ml @@ -0,0 +1,158 @@ +(***********************************************************************) +(* 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$ *) + +open Names +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 [< >]; + 'sPC; + if w<>[] then + [< 'sTR"writes "; + prlist_with_sep (fun ()-> [< 'sTR","; 'sPC >]) pr_id w >] + else [< >] + >] + +let ppr e = + pP (pp e) + diff --git a/contrib/correctness/peffect.mli b/contrib/correctness/peffect.mli new file mode 100644 index 000000000..2412622e6 --- /dev/null +++ b/contrib/correctness/peffect.mli @@ -0,0 +1,42 @@ +(***********************************************************************) +(* 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$ *) + +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 000000000..fe37f8308 --- /dev/null +++ b/contrib/correctness/penv.ml @@ -0,0 +1,224 @@ +(***********************************************************************) +(* 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$ *) + +open Pmisc +open Past +open Ptype +open Names +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_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 (inProg,outProg) = + declare_object ("programs-objects", + { load_function = cache_global; + cache_function = cache_global; + open_function = (fun _ -> ()); + export_function = (fun x -> Some x) }) +;; + +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 + add_named_object (id',OBJ) (inProg (id,TypeV v,p)) + end + +let add_global_set id = + try + let _ = Env.find id !env in + Prog_errors.clash id None + with + Not_found -> add_named_object (id,OBJ) (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 (inInit,outInit) = + declare_object ("programs-objects-init", + { load_function = (fun _ -> ()); + cache_function = cache_init; + specification_function = fun x -> x}) + +let initialize id c = add_anonymous_object (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 + add_global id' v (Some p); + mSGNL (hOV 0 [< 'sTR"Program "; pID 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 000000000..c6962b5f4 --- /dev/null +++ b/contrib/correctness/penv.mli @@ -0,0 +1,86 @@ +(***********************************************************************) +(* 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$ *) + +open Ptype +open Past +open Names +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 -> unit +val add_global_set : identifier -> unit +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 000000000..251471082 --- /dev/null +++ b/contrib/correctness/perror.ml @@ -0,0 +1,170 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Util +open Names +open Term +open Himsg + +open Putil +open Ptype +open Past + + +let raise_with_loc = function + None -> raise + | Some loc -> Stdpp.raise_with_loc loc + +let unbound_variable id loc = + raise_with_loc loc + (UserError ("Prog_errors.unbound_variable", + (hOV 0 [<'sTR"Unbound variable"; 'sPC; pr_id id; 'fNL >]))) + +let unbound_reference id loc = + raise_with_loc loc + (UserError ("Prog_errors.unbound_reference", + (hOV 0 [<'sTR"Unbound reference"; 'sPC; pr_id id; 'fNL >]))) + +let clash id loc = + raise_with_loc loc + (UserError ("Prog_errors.clash", + (hOV 0 [< 'sTR"Clash with previous constant"; 'sPC; + 'sTR(string_of_id id); 'fNL >]))) + +let not_defined id = + raise + (UserError ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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' = Declare.global_reference CCI id in + Reduction.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 ("Prog_errors.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 ("Prog_errors.check_no_effect", + hOV 0 [< 'sTR"A boolean should not have side effects" + >])) + +let should_be_boolean loc = + Stdpp.raise_with_loc loc + (UserError ("Prog_errors.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 ("Prog_errors.test_should_be_annotated", + hOV 0 [< 'sTR"This test should be annotated" >])) + +let if_branches loc = + Stdpp.raise_with_loc loc + (UserError ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.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 ("Prog_errors.should_be_a_variable", + hOV 0 [< 'sTR"Argument should be a variable" >])) + +let should_be_a_reference loc = + Stdpp.raise_with_loc loc + (UserError ("Prog_errors.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 000000000..81bed4404 --- /dev/null +++ b/contrib/correctness/perror.mli @@ -0,0 +1,47 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Names +open Ptype +open Past +open Coqast + +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 000000000..03f9b30e1 --- /dev/null +++ b/contrib/correctness/pextract.ml @@ -0,0 +1,471 @@ +(***********************************************************************) +(* 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$ *) + +open Pp_control +open Pp +open Util +open System +open Names +open Term +open Himsg +open Termenv +open Reduction + +open Genpp + +open Mutil +open Ptypes +open Past +open Penv +open Putil + +let extraction env c = + let ren = initial_renaming env in + let sign = TradEnv.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 = path_of_string "#Arrays#access.fw" + +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 + [< >] + 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 () -> [< >]) + (function + (id,(Untyped | BindType _)) -> + [< 'sTR" "; pID (get_local_name rn id) >] + | (id,BindSet) -> [< >]) + +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 -> [< >] + | 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 _ -> [< >]) + 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 [< >]; + 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 + (try pP_with ft strm ; pp_flush_with ft () + with e -> pp_flush_with ft () ; close_out chan; raise e); + 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 = 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" + [< pID id; 'sTR" is not a mutable" >] + +(* grammaire *) + +open Vernacinterp;; + +overwriting_vinterp_add("IMPERATIVEEXTRACTION", + function VARG_STRING file :: rem -> + let prm = parse_param rem in + (fun () -> pp_ocaml file prm) + | _ -> anomaly "IMPERATIVEEXTRACTION called with bad arguments.") +;; + +overwriting_vinterp_add("INITIALIZE", + function [VARG_IDENTIFIER id ; VARG_COMMAND com] -> + fun () -> initialize id com + | _ -> anomaly "INITIALIZE called with bad arguments.") +;; diff --git a/contrib/correctness/pextract.mli b/contrib/correctness/pextract.mli new file mode 100644 index 000000000..433fc33f2 --- /dev/null +++ b/contrib/correctness/pextract.mli @@ -0,0 +1,18 @@ +(***********************************************************************) +(* 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$ *) + +open Names +open Genpp + +val pp_ocaml : string -> extraction_params -> unit + + diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml new file mode 100644 index 000000000..f25541961 --- /dev/null +++ b/contrib/correctness/pmisc.ml @@ -0,0 +1,183 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Coqast +open Names +open Term + +module SpSet = Set.Make(struct type t = section_path let compare = sp_ord end) + +(* debug *) + +let debug = ref false + +let deb_mess s = + if !debug then begin + mSGNL s; 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_id id d = id_of_string ((string_of_id id) ^ "@" ^ d) + +let is_at id = + try + let _ = String.index (string_of_id id) '@' in true + with Not_found -> + false + +let un_at id = + let s = string_of_id id in + try + let n = String.index s '@' in + id_of_string (String.sub s 0 n), + String.sub s (succ n) (pred (String.length s - n)) + 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 "_" +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 alist' = + List.map (fun (id,id') -> (string_of_id id,string_of_id id')) alist in + 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 alist' = + List.map (fun (id,a) -> (string_of_id id,a)) alist in + 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 + +(* subst. of variables by constr *) +let real_subst_in_constr = replace_vars + +(* Coq constants *) + +let constant s = + let id = id_of_string s in + Declare.global_reference CCI 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) + + diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli new file mode 100644 index 000000000..f486d0d4e --- /dev/null +++ b/contrib/correctness/pmisc.mli @@ -0,0 +1,73 @@ +(***********************************************************************) +(* 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$ *) + +open Names +open Term + +module SpSet : Set.S with type elt = section_path + +(* Some misc. functions *) + +val reraise_with_loc : Coqast.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 -> Coqast.t -> Coqast.t +val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t +val real_subst_in_constr : (identifier * constr) list -> constr -> constr + +val constant : string -> constr +val conj : constr -> constr -> 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 + +(* for debugging purposes *) + +val debug : bool ref +val deb_mess : Pp.std_ppcmds -> unit + diff --git a/contrib/correctness/pmlize.ml b/contrib/correctness/pmlize.ml new file mode 100644 index 000000000..e81432c5f --- /dev/null +++ b/contrib/correctness/pmlize.ml @@ -0,0 +1,319 @@ +(***********************************************************************) +(* 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$ *) + +open Names +open Term +open Termast +open Pattern + +open Pmisc +open Ptype +open Past +open Putil +open Prename +open Penv +open Peffect +open Ptyping +open Pmonad + + +let mmk = make_module_marker [ "#Specif.obj" ] +let sig_pattern = put_pat mmk "(sig ? ?)" + +let has_proof_part ren env c = + let sign = TradEnv.trad_sign_of ren env in + let ty = Mach.type_of (Evd.mt_evd()) sign c in + somatches ty sig_pattern + +(* 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 + let t = make_tuple [ CC_expr c',ty ] qt ren env (current_date ren) in + t + + | Var 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) (VAR 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 (VAR 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) (VAR id1) + (VAR 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 (VAR 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 ([Var 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 ([Var 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)" + + | App (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) + (Std.map_succeed + (function + Term x -> x.info.kappa + | Refarg _ -> failwith "caught" + | Type _ -> + (result_id,TypePure mkSet),Effects.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 + + | LetIn (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 (DOP0(Sort(Prop Pos)))) :: (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 000000000..964b4327c --- /dev/null +++ b/contrib/correctness/pmlize.mli @@ -0,0 +1,20 @@ +(***********************************************************************) +(* 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$ *) + +open Past +open Penv +open Names + +(* translation of imperative programs into intermediate functional programs *) + +val trans : Renamings.t -> typed_program -> cc_term + diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml new file mode 100644 index 000000000..92b904bc1 --- /dev/null +++ b/contrib/correctness/pmonad.ml @@ -0,0 +1,675 @@ +(***********************************************************************) +(* 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$ *) + +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 -> Printf.sprintf "tuple_%d" n + +let dep_product_name = function + 1 -> "sig" + | 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) = Effects.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,_ = Effects.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 = Effects.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,(DOP0(Sort(Prop Pos))))::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 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,_) -> 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,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,tyapp), 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 (VAR 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 = Std.map_succeed + (function b -> if is_ref_binder b then failwith "caught" else 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 ty',id_b = 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 + Term.mkLambda name t1 (mkArrow t2 ty), q.a_name + | None -> assert false + in + CC_app (CC_case (ty', (b, constant "bool"), [br1;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 t1,t2 = + let n = test_name Anonymous in + CC_lam ([n,CC_untyped_binder],t1), + CC_lam ([n,CC_untyped_binder],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 + let t = + make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) + in + t + + +(* [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'') (VAR 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 t1,t2 = + let n = test_name Anonymous in + CC_lam ([n,CC_untyped_binder],t1), + CC_lam ([n,CC_untyped_binder],t2) 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 (VAR 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 (VAR 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 (VAR id_phi) (VAR 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 (VAR 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 (VAR id_phi) (VAR 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 (VAR 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; VAR 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; VAR id'; c1; c2]) + + +(* $Id$ *) diff --git a/contrib/correctness/pmonad.mli b/contrib/correctness/pmonad.mli new file mode 100644 index 000000000..2906858a7 --- /dev/null +++ b/contrib/correctness/pmonad.mli @@ -0,0 +1,106 @@ +(***********************************************************************) +(* 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$ *) + +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 000000000..08a22f06f --- /dev/null +++ b/contrib/correctness/pred.ml @@ -0,0 +1,79 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Past + +(* 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 (dep, ty, bl, (e1,info), 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,info), + CC_tuple (false,tl,List.map red al)) + | e -> CC_letin (dep, ty, bl, (red e1,info), 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,info), el) -> + CC_case (ty, (red e1,info), 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 Generic +open Term +open Reduction + +(* 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 *) + +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 + +let red_cci c = + let c = strong bin_app c in strong whd_programs c + diff --git a/contrib/correctness/pred.mli b/contrib/correctness/pred.mli new file mode 100644 index 000000000..27b8e0ea0 --- /dev/null +++ b/contrib/correctness/pred.mli @@ -0,0 +1,26 @@ +(***********************************************************************) +(* 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$ *) + +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 000000000..682463238 --- /dev/null +++ b/contrib/correctness/prename.ml @@ -0,0 +1,138 @@ +(***********************************************************************) +(* 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$ *) + +open Names +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 e) + diff --git a/contrib/correctness/prename.mli b/contrib/correctness/prename.mli new file mode 100644 index 000000000..55b7f3886 --- /dev/null +++ b/contrib/correctness/prename.mli @@ -0,0 +1,57 @@ +(***********************************************************************) +(* 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$ *) + +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 000000000..757669c67 --- /dev/null +++ b/contrib/correctness/preuves.v @@ -0,0 +1,81 @@ + +(* Quelques preuves sur des programmes simples, + * juste histoire d'avoir un petit bench. + *) + +Require Programs. +Require Omega. + +Prog Variable x : Z ref. +Prog Variable y : Z ref. +Prog Variable z : Z ref. +Prog Variable i : Z ref. +Prog Variable j : Z ref. +Prog Variable n : Z ref. +Prog Variable m : Z ref. +Variable r : Z. +Variable N : Z. +Prog Variable t : array N of Z. + + +(**********************************************************************) + +Correctness echange + { `0 <= i < N` /\ `0 <= j < N` } + begin + state 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. +Assumption. +Assumption. +Elim HH_6; Auto. +Elim HH_6; Auto. +Save. + + +(**********************************************************************) + +(* + * while x <= y do x := x+1 done { y < x } + *) + +Correctness incrementation + while (Z_le_gt_dec !x !y) do + { invariant True variant (Zminus (Zs y) x) } + x := (Zs !x) + 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.mli b/contrib/correctness/psyntax.mli new file mode 100644 index 000000000..f5128fdef --- /dev/null +++ b/contrib/correctness/psyntax.mli @@ -0,0 +1,25 @@ +(***********************************************************************) +(* 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$ *) + +open Pcoq +open Ptype +open Past + +(* Grammar for the programs and the tactic Correctness *) + +module Programs : + sig + val program : program Gram.Entry.e + val type_v : Coqast.t ml_type_v Gram.Entry.e + val type_c : Coqast.t ml_type_c Gram.Entry.e + end + diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml new file mode 100644 index 000000000..620e42593 --- /dev/null +++ b/contrib/correctness/ptactic.ml @@ -0,0 +1,257 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Names +open Term +open Pfedit +open Constrtypes +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 = Prog_db.db_prog p in + + (* 2. typage avec effets *) + deb_mess [< 'sTR"Prog_typing.states: Typage avec effets..."; 'fNL >]; + let env = Prog_env.empty in + let ren = initial_renaming env in + let p = Prog_typing.states ren env p in + let ((_,v),_,_,_) as c = p.info.kappa in + Prog_errors.check_for_not_mutable p.loc v; + deb_mess (pp_type_c c); + + (* 3. propagation annotations *) + let p = Prog_wp.propagate ren p in + + (* 4a. traduction type *) + let ty = Monad.trad_ml_type_c ren env c in + deb_mess (Himsg.pTERM ty); + + (* 4b. traduction terme (terme intermédiaire de type cc_term) *) + deb_mess + [< 'fNL; 'sTR"Mlise.trad: Traduction program -> cc_term..."; 'fNL >]; + let cc = Mlise.trans ren p in + let cc = Prog_red.red cc in + deb_mess (Prog_utils.pp_cc_term cc); + + (* 5. traduction en constr *) + deb_mess + [< 'fNL; 'sTR"Prog_cci.constr_of_prog: Traduction cc_term -> constr..."; + 'fNL >]; + let c = Prog_cci.constr_of_prog cc in + deb_mess (Himsg.pTERM c); + + (* 6. résolution implicites *) + deb_mess [< 'fNL; 'sTR"Résolution implicites (? => Meta(n))..."; 'fNL >]; + let c = + (ise_resolve false (Evd.mt_evd()) [] (gLOB(initial_sign())) c)._VAL in + deb_mess (Himsg.pTERM c); + + p,c,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 + +let mmk = make_module_marker ["#Prelude.obj"; "#Wf.obj"] + +let wf_nat_pattern = put_pat mmk "(well_founded nat lt)" +let zwf_nat_pattern = put_pat mmk "(well_founded Z (Zwf ?))" +let and_pattern = put_pat mmk "(and ? ?)" +let eq_pattern = put_pat mmk "(eq ? ? ?)" + +(* 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 concl = pf_concl gl in + match hyps with + ([],[]) -> tclIDTAC gl + | (id::sl,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 (sl,al)) gl + else if n >= 7 & String.sub s 0 7 = "Variant" then begin + match dest_match gl (body_of_type a) eq_pattern with + [_; VAR phi; _] -> + if occur_var phi concl then + tclTHEN (rewriteLR (VAR id)) (arec (sl,al)) gl + else + arec (sl,al) gl + | _ -> assert false end + else + arec (sl,al) gl + | _ -> assert false + in + arec (pf_hyps 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 + ([],[]) -> Std.error "No such assumption" + | (s::sl,a::al) -> + let a = body_of_type a in + if pf_conv_x_leq gl a concl then + refine (VAR s) gl + else if matches gl a and_pattern then + match dest_match gl a and_pattern with + [c1;c2] -> + if pf_conv_x_leq gl c1 concl then + exact (applistc (constant "proj1") [c1;c2;VAR s]) gl + else if pf_conv_x_leq gl c2 concl then + exact (applistc (constant "proj2") [c1;c2;VAR s]) gl + else + arec (sl,al) + | _ -> assert false + else + arec (sl,al) + | _ -> assert false + in + arec (pf_hyps gl) + +(* automatic: see above *) + +let (automatic : tactic) = + tclTHEN + loop_ids + (fun gl -> + let c = pf_concl gl in + if matches gl c wf_nat_pattern then + exact (constant "lt_wf") gl + else if matches gl c zwf_nat_pattern then + let z = List.hd (dest_match gl c zwf_nat_pattern) in + exact (Term.applist (constant "Zwf_well_founded",[z])) gl + else if matches gl c and_pattern then + (tclORELSE assumption_bis + (tclTRY (tclTHEN simplest_split assumption))) gl + else if matches gl c eq_pattern then + (tclORELSE reflexivity (tclTRY assumption_bis)) gl + else + tclTRY assumption_bis gl) + +(* [correctness s p] : string -> program -> unit + * + * Vernac: Correctness <string> <program>. + *) + +let correctness s p opttac = + Misc_utils.reset_names(); + let p,c,cty,v = coqast_of_prog p in + let sigma = Proof_trees.empty_evd in + let sign = initial_sign() in + let cty = Reduction.nf_betaiota cty in + start_proof_constr s NeverDischarge cty; + Prog_env.new_edited (id_of_string s) (v,p); + if !debug then show_open_subgoals(); + deb_mess [< 'sTR"Prog_red.red_cci: Réduction..."; 'fNL >]; + let c = Prog_red.red_cci c in + deb_mess [< 'sTR"APRES REDUCTION :"; 'fNL >]; + deb_mess (Himsg.pTERM c); + let tac = (tclTHEN (Tcc.refine_tac c) automatic) in + let tac = match opttac with + None -> tac + | Some t -> tclTHEN tac t + in + solve_nth 1 tac; + show_open_subgoals() + + +(* On redéfinit la commande "Save" pour enregistrer les nouveaux programmes *) + +open Initial +open Vernacinterp + +let add = Vernacinterp.overwriting_vinterp_add + +let register id n = + let id' = match n with None -> id | Some id' -> id' in + Prog_env.register id id' + +let wrap_save_named b = + let pf_id = id_of_string (Pfedit.get_proof()) in + save_named b; + register pf_id None + +let wrap_save_anonymous_thm b id = + let pf_id = id_of_string (Pfedit.get_proof()) in + save_anonymous_thm b (string_of_id id); + register pf_id (Some id) + +let wrap_save_anonymous_remark b id = + let pf_id = id_of_string (Pfedit.get_proof()) in + save_anonymous_remark b (string_of_id id); + register pf_id (Some id) +;; + +add("SaveNamed", + function [] -> (fun () -> if not(is_silent()) then show_script(); + wrap_save_named true) + | _ -> assert false);; + +add("DefinedNamed", + function [] -> (fun () -> if not(is_silent()) then show_script(); + wrap_save_named false) + | _ -> assert false);; + +add("SaveAnonymousThm", + function [VARG_IDENTIFIER id] -> + (fun () -> if not(is_silent()) then show_script(); + wrap_save_anonymous_thm true id) + | _ -> assert false);; + +add("SaveAnonymousRmk", + function [VARG_IDENTIFIER id] -> + (fun () -> if not(is_silent()) then show_script(); + wrap_save_anonymous_remark true id) + | _ -> assert false);; + + diff --git a/contrib/correctness/ptactic.mli b/contrib/correctness/ptactic.mli new file mode 100644 index 000000000..f1cd81a48 --- /dev/null +++ b/contrib/correctness/ptactic.mli @@ -0,0 +1,22 @@ +(***********************************************************************) +(* 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$ *) + +(* 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 -> ProgAst.program -> Tacmach.tactic option -> unit + diff --git a/contrib/correctness/ptype.ml b/contrib/correctness/ptype.ml new file mode 100644 index 000000000..a2caa69c4 --- /dev/null +++ b/contrib/correctness/ptype.ml @@ -0,0 +1,75 @@ +(***********************************************************************) +(* 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$ *) + +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 + +let is_mutable = function Ref _ | Array _ -> true | _ -> false +let is_pure = function TypePure _ -> true | _ -> false + diff --git a/contrib/correctness/ptype.mli b/contrib/correctness/ptype.mli new file mode 100644 index 000000000..bbb517a20 --- /dev/null +++ b/contrib/correctness/ptype.mli @@ -0,0 +1,33 @@ +(***********************************************************************) +(* 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$ *) + +(* Generated automatically by ocamlc -i *) + +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 = Term.constr assertion +type 'a binder_type = | BindType of 'a | BindSet | Untyped +type 'a binder = Names.identifier * 'a binder_type +type variant = Term.constr * Term.constr * Term.constr +type 'a ml_type_v = + | Ref of 'a ml_type_v + | Array of 'a * 'a ml_type_v + | Arrow of 'a ml_type_v binder list * 'a ml_type_c + | TypePure of 'a +and 'a ml_type_c = + (Names.identifier * 'a ml_type_v) * Peffect.t * 'a precondition list * + 'a postcondition option +type type_v = Term.constr ml_type_v +type type_c = Term.constr ml_type_c +val is_mutable : 'a ml_type_v -> bool +val is_pure : 'a ml_type_v -> bool diff --git a/contrib/correctness/ptyping.ml b/contrib/correctness/ptyping.ml new file mode 100644 index 000000000..773447f9a --- /dev/null +++ b/contrib/correctness/ptyping.ml @@ -0,0 +1,590 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Util +open Names +open Term +open Termast +open Himsg +open Proof_trees + +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 just_reads e = + difference (get_reads e) (get_writes e) + +let type_v_sup loc t1 t2 = + if t1 = t2 then + t1 + else + Prog_errors.if_branches loc + +let typed_var ren env (phi,r) = + let sign = TradEnv.before_after_sign_of ren env in + let a = Mach.type_of (Evd.mt_evd()) sign phi in + (phi,r,a) + +(* Application de fonction *) + +let rec convert = function + | (TypePure c1, TypePure c2) -> + Reduction.conv_x (Evd.mt_evd()) c1 c2 + | (Ref v1, Ref v2) -> + convert (v1,v2) + | (Array (s1,v1), Array (s2,v2)) -> + (Reduction.conv_x (Evd.mt_evd()) 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 Prog_errors.partial_app f.loc; + bl,c + | _ -> Prog_errors.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 Prog_errors.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 _ -> Prog_errors.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 = Monad.trad_ml_type_v ren env v in + s, (id,c)::so, ok + | (id,BindSet), Term t -> Prog_errors.expects_a_type id t.loc + | (id,BindType _), Type _ -> Prog_errors.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 j = + reraise_with_loc (Ast.loc a) (fconstruct (Evd.mt_evd()) sign) a in + let ids = global_vars j._VAL in + j._VAL, j._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 + Mach.type_of (Evd.mt_evd()) sign 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 + Var 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 + | App (p,args) -> + is_pure ren env p & List.for_all (is_pure_arg ren env) args + | SApp _ | Aff _ | TabAff _ | Seq _ | While _ | If _ + | Lam _ | LetRef _ | LetIn _ | 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 = TradEnv.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 Effects.add_read id e else e) + Effects.bottom ids in + let r',_,_ = state_coq_ast (initial_sign()) 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 = TradEnv.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 + Effects.add_read id e + else if is_at id then + let uid,_ = un_at id in + if is_mutable_in_env env uid then + Effects.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)) + (Effects.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 -> Effects.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 -> Effects.bottom, None + | Some q -> + let v' = Monad.trad_ml_type_v ren env v in + let sign = TradEnv.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 + Effects.add_write id e, c + else + Effects.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 + Effects.add_read uid e, c + else + e,c + else + e,c) + (Effects.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 = TradEnv.now_sign_of ren env in + let c = constr_of_com (Evd.mt_evd()) 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 = TradEnv.cci_sign_of ren env in + let c = constr_of_com (Evd.mt_evd()) 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 = Monad.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 = Effects.union e (Effects.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 + Var id -> + (if is_global id then constant (string_of_id id) else VAR id), + pl, Effects.bottom + | Expression c -> c, pl, Effects.bottom + | Acc id -> VAR id, pl, Effects.add_read id Effects.bottom + | TabAcc (_,id,p) -> + let c,pl,ef = effect pl p.desc in + let pre = Monad.make_pre_access ren env id c in + Monad.make_raw_access ren env (id,id) c, + (anonymous_pre true pre)::pl, Effects.add_read id ef + | App (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,Effects.union e earg + | Type v -> + let v' = cic_type_v env ren v in + (Monad.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 "Prog_typing.states_expression" + in + let e0,pl0 = state_pre ren env expr.pre in + let c,pl,e = effect [] expr.desc in + let sign =TradEnv.before_sign_of ren env in + let c = (Trad.ise_resolve true empty_evd [] (gLOB sign) c)._VAL in + let ty = Mach.type_of empty_evd sign c in + let v = TypePure ty in + let ef = Effects.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,Effects.bottom) + + | Acc _ -> + failwith "Prog_typing.states: term is supposed not to be pure" + + | Var id -> + let v = type_in_env env id in + let ef = Effects.bottom in + Var id, (v,ef) + + | Aff (x, e1) -> + Prog_errors.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 = Effects.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 = Effects.add_write x (Effects.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 = + Effects.union (Effects.union ef_bl efb) (Effects.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 "Prog_typing.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 = Effects.bottom in + Lam(bl',s_e), (v,ef) + + (* Connectives AND and OR *) + | SApp ([Var 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 = Effects.union ef1 ef2 in + SApp ([Var id], [s_e1; s_e2]), + (TypePure (constant "bool"), ef) + + (* Connective NOT *) + | SApp ([Var id], [e]) -> + let s_e = states ren env e in + let (_,ef,_,_) = s_e.info.kappa in + SApp ([Var id], [s_e]), + (TypePure (constant "bool"), ef) + + | SApp _ -> invalid_arg "Prog_typing.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. *) + + | App (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 + | _ -> Effects.bottom) + s_args + in + let _,_,((_,tapp),efapp,_,_) = effect_app ren env s_f s_args in + let ef = + Effects.compose (List.fold_left Effects.compose eff ef_args) efapp + in + App (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 + Prog_errors.check_for_let_ref loc v2; + let ef = Effects.compose ef1 (Effects.remove ef2 x) in + LetRef (x, s_e1, s_e2), (v2,ef) + + | LetIn (x, e1, e2) -> + let s_e1 = states ren env e1 in + let (_,v1),ef1,_,_ = s_e1.info.kappa in + Prog_errors.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 = Effects.compose ef1 ef2 in + LetIn (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 = Effects.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,Effects.bottom) + + | PPoint (s,d) -> + let ren' = push_date ren s in + states_desc ren' env loc d + + | Debug _ -> failwith "Prog_typing.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' = Effects.union e (Effects.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,Effects.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,Effects.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,Effects.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 000000000..985d7b52e --- /dev/null +++ b/contrib/correctness/ptyping.mli @@ -0,0 +1,35 @@ +(***********************************************************************) +(* 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$ *) + +open Names +open Term + +open Ptype +open Past +open Penv + +(* This module realizes type and effect inference *) + +val cic_type_v : local_env -> Renamings.t -> CoqAst.t ml_type_v -> type_v + +val effect_app : Renamings.t -> local_env + -> (typing_info,'b) ProgAst.t + -> (typing_info,constr) arg list + -> (type_v binder list * type_c) + * ((identifier*identifier) list * (identifier*constr) list * bool) + * type_c + +val typed_var : Renamings.t -> local_env -> constr * constr -> variant + +val type_of_expression : Renamings.t -> local_env -> constr -> constr + +val states : Renamings.t -> local_env -> program -> typed_program diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml new file mode 100644 index 000000000..7fd8b7b4a --- /dev/null +++ b/contrib/correctness/putil.ml @@ -0,0 +1,298 @@ +(***********************************************************************) +(* 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$ *) + +open Util +open Names +open Term +open Pattern + +open Pmisc +open Ptype +open Past +open Penv +open Prename + +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 c) + +let make_before_after c = + let ids = global_vars 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 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 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 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 *) + +let dest_sig c = match matches (Coqlib.build_coq_sig_pattern ()) c with + | [_,a; _,p] -> (a,p) + | _ -> assert false + +(* TODO: faire un test plus serieux sur le type des objets Coq *) +let rec is_pure_cci c = match kind_of_term c with + | IsCast (c,_) -> is_pure_cci c + | IsProd(_,_,c') -> is_pure_cci c' + | IsRel _ | IsMutInd _ | IsConst _ -> true (* heu... *) + | IsApp _ -> not (is_matching (Coqlib.build_coq_sig_pattern ()) c) + | _ -> Util.error "CCI term not acceptable in programs" + +let rec v_of_constr c = match kind_of_term c with + | IsCast (c,_) -> v_of_constr c + | IsProd _ -> + 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)) + | IsMutInd _ | IsConst _ | IsApp _ -> + TypePure c + | _ -> + failwith "v_of_constr: TODO" + +and c_of_constr c = + if is_matching (Coqlib.build_coq_sig_pattern ()) c then + let (a,q) = dest_sig 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 +open Printer + +let pp_pre = function + [] -> [< >] + | l -> + hOV 0 [< 'sTR"pre "; + prlist_with_sep (fun () -> [< 'sPC >]) + (fun x -> prterm x.p_value) l >] + +let pp_post = function + None -> [< >] + | 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 () -> [< >]) 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 000000000..ca139f9e1 --- /dev/null +++ b/contrib/correctness/putil.mli @@ -0,0 +1,71 @@ +(***********************************************************************) +(* 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$ *) + +open Pp +open Names +open Term +open Pmisc +open Ptype +open Past +open Penv + +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 dest_sig : constr -> constr * constr + +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 000000000..af6801a1c --- /dev/null +++ b/contrib/correctness/pwp.ml @@ -0,0 +1,342 @@ +(***********************************************************************) +(* 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$ *) + +open More_util +open Names +open Generic +open Term +open Environ + +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 = Effects.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 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 _ | LetIn _ | 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 bool_id = id_of_string "bool" + +let is_bool = function + TypePure c -> + (match (strip_outer_cast c) with + DOPN(MutInd _ as op,_) -> id_of_global op = bool_id + | _ -> false) + | _ -> false + +let normalize_boolean ren env b = + let ((res,v),ef,p,q) = b.info.kappa in + Prog_errors.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') = dest_sig 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 + Prog_errors.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 } -> + Reduction.whd_betaiota (Term.applist (q, [constant "true"])), + Reduction.whd_betaiota (Term.applist (q, [constant "false"])) + | _ -> invalid_arg "Prog_typing.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 = Monad.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) + | App (f,l) -> + App (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))) + | LetIn (x,e1,e2) -> + let top = label_name() in + let ren' = push_date ren top in + PPoint (top, LetIn (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 _ | Var _ + | 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 + App (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 ([Var 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 (Evd.mt_evd()) c in + create_bool_post c + in + let d = + SApp ([Var id; Expression (out_post q1); Expression (out_post q2)], + [e1; e2] ) + in + post_if_none env q (change_desc p d) + + | SApp ([Var 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 (Evd.mt_evd()) c in + create_bool_post c + in + let d = SApp ([Var 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 -> + let q' = + let ((id,v),_,_,_) = p.info.kappa in + let tv = Monad.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 000000000..7ccc52c82 --- /dev/null +++ b/contrib/correctness/pwp.mli @@ -0,0 +1,18 @@ +(***********************************************************************) +(* 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$ *) + +open Term +open Penv + +val update_post : local_env -> string -> Effects.t -> constr -> constr + +val propagate : Renamings.t -> typed_program -> typed_program |