diff options
| author | ckeller <ckeller@users.noreply.github.com> | 2019-03-11 20:25:35 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-11 20:25:35 +0100 |
| commit | a88e3b3b6ad01a9b85c828b9a1225732275affee (patch) | |
| tree | acc3768695698a80867b4ce941ab4cb7b4b99d7a | |
| parent | 33010bfa6345549d8b9b0c06f44150b60d0c86e5 (diff) | |
| download | smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.tar.gz smtcoq-a88e3b3b6ad01a9b85c828b9a1225732275affee.zip | |
V8.8 (#42)
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Towards 8.8
* Organization structures
* 8.8 ok with standard coq
34 files changed, 1146 insertions, 1063 deletions
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index 37a39b5..4a791e6 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -102,7 +102,7 @@ Ltac converting := repeat match goal with (* On capture chaque sous-terme x avec son contexte, i.e. le but est C[x] *) - | |- appcontext C[?x] => + | |- context C[?x] => (* Si x est de type T *) let U := type of x in lazymatch eval fold T in U with @@ -116,7 +116,7 @@ Ltac converting := pose proof x as var; (* Sinon, on analyse la formule obtenue en remplaçant x par notre variable fraîche dans le but *) lazymatch context C[var] with - | appcontext [?h var] => + | context [?h var] => let h := get_head h in lazymatch h with (* x est déjà réécrit *) @@ -201,7 +201,7 @@ Ltac renaming := repeat match goal with (* S'il y a un terme de la forme (T2Z (f t1 ... tn)) *) - | |- appcontext [T2Z ?X] => + | |- context [T2Z ?X] => (* On récupère le symbole de tête *) let f := get_head X in (* S'il s'agit d'un constructeur on ne fait rien *) @@ -214,7 +214,7 @@ Ltac renaming := repeat match goal with (* Pour chaque terme de la forme (T2Z (f' t'1 ... t'n)) *) - | |- appcontext [T2Z ?X'] => + | |- context [T2Z ?X'] => (* On récupère le symbole de tête *) let f' := get_head X' in (* Si f' = f *) @@ -269,7 +269,7 @@ Ltac renaming' := repeat match goal with (* S'il y a un terme de la forme (f t1 ... (Z2T tn)) *) - | |- appcontext [?X (Z2T ?Y)] => + | |- context [?X (Z2T ?Y)] => (* On récupère le symbole de tête *) let f := get_head X in (* S'il s'agit d'un constructeur on ne fait rien *) @@ -280,7 +280,7 @@ Ltac renaming' := repeat match goal with (* Pour chaque terme de la forme (f' t'1 ... (Z2T t'n)) *) - | |- appcontext [?X' (Z2T ?Y')] => + | |- context [?X' (Z2T ?Y')] => (* On récupère le symbole de tête *) let f' := get_head X' in (* Si f' = f *) @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool List PArray Int63 ZArith. +Require Import Bool List PArray Int63 ZArith Psatz. Local Open Scope int63_scope. Local Open Scope array_scope. @@ -30,12 +30,12 @@ Proof. rewrite <- leb_spec in H; rewrite H; discriminate. intros H1 _; apply to_Z_inj; rewrite add_spec, to_Z_1 in H. assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB). - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. destruct H2 as [H2|H2]. rewrite Zmod_small in H. - omega. + lia. split. - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. assumption. rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption. Qed. @@ -48,14 +48,14 @@ Proof. rewrite <- ltb_spec in H; rewrite H; discriminate. intros H1 _; apply to_Z_inj. rewrite add_spec in H1. rewrite to_Z_1 in H1. assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB). - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. destruct H2 as [H2|H2]. rewrite Zmod_small in H1. - omega. + lia. split. - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. assumption. - rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. omega. + rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia. Qed. @@ -74,19 +74,19 @@ Proof. min (fun a0 : A => a0))). apply foldi_down_cont_ZInd;intros;red. assert (H20: (z+1 < [|min|]+1)%Z). - omega. + lia. rewrite Zlt_is_lt_bool in H20; rewrite H20;trivial. case_eq (Zlt_bool ([|i|]+1) ([|min|]+1));intros. - rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;omega. + rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;lia. clear H4;revert H3;unfold P'. case_eq (Zlt_bool ([|i|] - 1 + 1) ([|min|]+1));intros;auto. - rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;omega). + rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;lia). rewrite H4, <- H6. apply H0;trivial. - apply H4. replace ([|i|] - 1 + 1)%Z with [|i|] by omega. auto. + apply H4. replace ([|i|] - 1 + 1)%Z with [|i|] by lia. auto. revert H1;unfold P'. case_eq (Zlt_bool ([|max|]+1)%Z ([|min|]+1)%Z);auto. rewrite <- Zlt_is_lt_bool. - intro H22; assert (H21: ([|max|] < [|min|])%Z). omega. + intro H22; assert (H21: ([|max|] < [|min|])%Z). lia. rewrite <- ltb_spec in H21. intros;rewrite foldi_down_cont_lt;auto. Qed. @@ -120,26 +120,26 @@ Lemma to_list_In : forall {A} (t: array A) i, i < length t = true -> In (t.[i]) (to_list t). Proof. intros A t i H; unfold to_list; case_eq (0 == length t); intro Heq. - unfold is_true in H; rewrite ltb_spec in H; rewrite eqb_spec in Heq; rewrite <- Heq in H; rewrite to_Z_0 in H; pose (H1 := to_Z_bounded i); elimtype False; omega. + unfold is_true in H; rewrite ltb_spec in H; rewrite eqb_spec in Heq; rewrite <- Heq in H; rewrite to_Z_0 in H; pose (H1 := to_Z_bounded i); elimtype False; lia. pose (P := fun j a => i < j = true \/ In (t .[ i]) a). pose (H1:= foldi_down_Ind2 _ P); unfold P in H1. assert (H2: i < 0 = true \/ In (t .[ i]) (foldi_down (fun (i0 : int) (l : list A) => t .[ i0] :: l) (length t - 1) 0 nil)). apply H1. rewrite ltb_spec; erewrite to_Z_sub_1; try eassumption. - pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; omega. - intro H2; elimtype False; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded (length t - 1)); omega. + pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; lia. + intro H2; elimtype False; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded (length t - 1)); lia. left; unfold is_true; rewrite ltb_spec; rewrite (to_Z_add_1 _ max_int). erewrite to_Z_sub_1; try eassumption. - unfold is_true in H; rewrite ltb_spec in H; omega. + unfold is_true in H; rewrite ltb_spec in H; lia. rewrite ltb_spec; erewrite to_Z_sub_1; try eassumption. - pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; omega. + pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; lia. intros j a H2 H3 [H4|H4]. case_eq (i < j); intro Heq2. left; reflexivity. right; rewrite (lt_eq _ _ H4 Heq2); constructor; reflexivity. right; constructor 2; assumption. destruct H2 as [H2|H2]; try assumption. - unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; omega. + unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia. Qed. Lemma In_to_list : forall {A} (t: array A) x, @@ -151,11 +151,11 @@ Proof. pose (P (_:int) l := In x l -> exists i : int, (i < length t) = true /\ x = t .[ i]). pose (H1 := foldi_down_Ind2 _ P (fun (i : int) (l : list A) => t .[ i] :: l) (length t - 1) 0); unfold P in H1; apply H1. - rewrite ltb_spec, to_Z_sub_1_diff; auto; change [|max_int|] with (wB-1)%Z; pose (H2 := to_Z_bounded (length t)); omega. + rewrite ltb_spec, to_Z_sub_1_diff; auto; change [|max_int|] with (wB-1)%Z; pose (H2 := to_Z_bounded (length t)); lia. intros _ H; inversion H. intro H; inversion H. simpl; intros i a _ H2 IH [H3|H3]. - exists i; split; auto; rewrite ltb_spec; rewrite leb_spec, to_Z_sub_1_diff in H2; auto; omega. + exists i; split; auto; rewrite ltb_spec; rewrite leb_spec, to_Z_sub_1_diff in H2; auto; lia. destruct (IH H3) as [j [H4 H5]]; exists j; auto. Qed. @@ -190,17 +190,17 @@ Proof. rewrite Int63Properties.eqb_spec; intro Heq; rewrite Heq in Hi; eelim ltb_0; eassumption. rewrite eqb_false_spec; intro Heq; pose (Hi':=Hi); replace (length t) with ((length t - 1) + 1) in Hi'. generalize Hi'; apply (foldi_Ind _ (fun j a => (i < j) = true -> length a = length t -> a.[i] = f i (t.[i]))). - rewrite ltb_spec, (to_Z_sub_1 _ i); auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; omega. + rewrite ltb_spec, (to_Z_sub_1 _ i); auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; lia. intros H _; eelim ltb_0; eassumption. intros H; eelim ltb_0; eassumption. intros j a _ H1 IH H2 H3; rewrite length_set in H3; case_eq (j == i). rewrite Int63Properties.eqb_spec; intro Heq2; subst i; rewrite get_set_same; auto; rewrite H3; auto. rewrite eqb_false_spec; intro Heq2; rewrite get_set_other; auto; apply IH; auto; rewrite ltb_spec; rewrite ltb_spec, (to_Z_add_1 _ (length t)) in H2. - assert (H4: [|i|] <> [|j|]) by (intro H4; apply Heq2, to_Z_inj; auto); omega. - rewrite ltb_spec; rewrite leb_spec, (to_Z_sub_1 _ _ Hi) in H1; omega. + assert (H4: [|i|] <> [|j|]) by (intro H4; apply Heq2, to_Z_inj; auto); lia. + rewrite ltb_spec; rewrite leb_spec, (to_Z_sub_1 _ _ Hi) in H1; lia. apply to_Z_inj; rewrite (to_Z_add_1 _ max_int). - rewrite to_Z_sub_1_diff; auto; omega. - rewrite ltb_spec, to_Z_sub_1_diff; auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; omega. + rewrite to_Z_sub_1_diff; auto; lia. + rewrite ltb_spec, to_Z_sub_1_diff; auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; lia. Qed. @@ -268,7 +268,7 @@ Proof. rewrite ltb_spec, to_Z_sub_1_diff; auto with zarith. intro H3; rewrite H3 in Heq; discriminate. intro Hlt; assert (H3: length t - 1 = 0). - rewrite ltb_spec, to_Z_1 in Hlt; apply to_Z_inj; rewrite to_Z_0; pose (H3 := to_Z_bounded (length t - 1)); omega. + rewrite ltb_spec, to_Z_1 in Hlt; apply to_Z_inj; rewrite to_Z_0; pose (H3 := to_Z_bounded (length t - 1)); lia. rewrite H3; assumption. intros i a H3 H4; apply H1; trivial. rewrite ltb_leb_sub1; auto. @@ -321,7 +321,7 @@ Lemma afold_left_spec : forall A B (f:B -> A) args op e, assert (H1: length args = 1). generalize (to_Z_bounded (length args)). rewrite <- not_true_iff_false, ltb_spec, to_Z_0, to_Z_sub_1_diff in H;auto. - intros;apply to_Z_inj;rewrite to_Z_1;omega. + intros;apply to_Z_inj;rewrite to_Z_1;lia. rewrite H1; change (1 - 1) with 0; rewrite (foldi_eq _ _ 0 0); auto. Qed. @@ -347,7 +347,7 @@ Proof. apply ltb_leb_sub1;trivial. revert n0 H3;rewrite ltb_spec, leb_spec, to_Z_1, sub_spec. change [|2|] with 2%Z. - intros HH;assert (W:= to_Z_bounded (length V1));rewrite Zmod_small;omega. + intros HH;assert (W:= to_Z_bounded (length V1));rewrite Zmod_small;lia. Qed. @@ -379,10 +379,10 @@ Proof. rewrite to_Z_sub_1_diff. ring_simplify ([|length t - 1|] - 1 + 1)%Z;rewrite of_to_Z;trivial. assert (H10: (1 < length t) = true) by (rewrite ltb_negb_geb, Heq; auto). - intro H11. rewrite ltb_spec in H10. assert (H12: [|length t - 1|] = 0%Z) by (rewrite H11; auto). change [|1|] with (1%Z) in H10. rewrite to_Z_sub_1_diff in H12; [omega| ]. intro H13. assert (H14: [|length t|] = 0%Z) by (rewrite H13; auto). omega. + intro H11. rewrite ltb_spec in H10. assert (H12: [|length t - 1|] = 0%Z) by (rewrite H11; auto). change [|1|] with (1%Z) in H10. rewrite to_Z_sub_1_diff in H12; [lia| ]. intro H13. assert (H14: [|length t|] = 0%Z) by (rewrite H13; auto). lia. intros;ring_simplify ([|i|] - 1 + 1)%Z;rewrite of_to_Z;auto. assert (i < length t - 1 = true). - rewrite ltb_spec. rewrite leb_spec in H0. replace (length t - 2) with (length t - 1 - 1) in H0 by ring. rewrite to_Z_sub_1_diff in H0; [omega| ]. intro H4. assert (H5: [|length t - 1|] = 0%Z) by (rewrite H4; auto). assert (H6: 1 < length t = true) by (rewrite ltb_negb_geb, Heq; auto). rewrite ltb_spec in H6. change ([|1|]) with (1%Z) in H6. rewrite to_Z_sub_1_diff in H5; [omega| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). omega. + rewrite ltb_spec. rewrite leb_spec in H0. replace (length t - 2) with (length t - 1 - 1) in H0 by ring. rewrite to_Z_sub_1_diff in H0; [lia| ]. intro H4. assert (H5: [|length t - 1|] = 0%Z) by (rewrite H4; auto). assert (H6: 1 < length t = true) by (rewrite ltb_negb_geb, Heq; auto). rewrite ltb_spec in H6. change ([|1|]) with (1%Z) in H6. rewrite to_Z_sub_1_diff in H5; [lia| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). lia. apply H1; [trivial| ]. rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto. symmetry. rewrite eqb_false_spec. intro H. rewrite H in Heq. discriminate. @@ -412,7 +412,7 @@ Proof. intros A B P default OP F t H1 H2 H4. pose (H3 := afold_right_Ind A B (fun _ => P) default OP F t). unfold afold_right. case_eq (length t == 0); auto. intro H10. assert (H := H10). rewrite eqb_false_spec in H. case_eq (length t <= 1); intro Heq. - replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). omega. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto. + replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). lia. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto. Qed. @@ -425,7 +425,7 @@ Proof. intros A B P default OP F t H1 H2 H4. pose (H3 := afold_right_Ind A B (fun _ => P) default OP F t). unfold afold_right. assert (H10 : length t == 0 = false) by (rewrite eqb_false_spec; intro H; rewrite H in H2; discriminate). rewrite H10. assert (H := H10). rewrite eqb_false_spec in H. case_eq (length t <= 1); intro Heq. - replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). omega. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto. + replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). lia. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto. Qed. @@ -440,11 +440,11 @@ Lemma afold_right_spec : forall A B (f:B -> A) args op e, apply not_eq_sym in n;rewrite (eqb_false_complete _ _ n). case_eq (length args <= 1); intro Heq. assert (H11: length args = 1). - apply to_Z_inj. rewrite leb_spec in Heq. assert (H11: 0%Z <> [|length args|]) by (intro H; elim n; apply to_Z_inj; auto). change [|1|] with (1%Z) in *. assert (H12 := leb_0 (length args)). rewrite leb_spec in H12. change [|0|] with 0%Z in H12. omega. + apply to_Z_inj. rewrite leb_spec in Heq. assert (H11: 0%Z <> [|length args|]) by (intro H; elim n; apply to_Z_inj; auto). change [|1|] with (1%Z) in *. assert (H12 := leb_0 (length args)). rewrite leb_spec in H12. change [|0|] with 0%Z in H12. lia. rewrite H11, foldi_down_eq; auto. assert (H11: 1 < length args = true) by (rewrite ltb_negb_geb, Heq; auto). replace (foldi_down (fun (i : int) (b : A) => op (f (args .[ i])) b) (length args - 1) 0 neu) with (foldi_down (fun (i : int) (b : A) => op (f (args .[ i])) b) (length args - 1 - 1) 0 (op (f (args .[ length args - 1])) neu)). replace (length args - 1 - 1) with (length args - 2) by ring. rewrite H10. auto. - symmetry. apply foldi_down_gt. rewrite ltb_spec. change [|0|] with 0%Z. rewrite to_Z_sub_1_diff; auto. rewrite ltb_spec in H11. change [|1|] with 1%Z in H11. omega. + symmetry. apply foldi_down_gt. rewrite ltb_spec. change [|0|] with 0%Z. rewrite to_Z_sub_1_diff; auto. rewrite ltb_spec in H11. change [|1|] with 1%Z in H11. lia. Qed. @@ -459,7 +459,7 @@ Proof. intros A i a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => (i < j) = true -> f (a .[ i]) = false -> t = false)). intros b j H1 H2 H3 H4; case_eq (i == j). rewrite Int63Properties.eqb_spec; intro; subst i; rewrite H4, andb_false_r; auto. - rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); omega. + rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); lia. intro H; eelim ltb_0; eassumption. Qed. @@ -490,7 +490,7 @@ Proof. intros A a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => t = true -> forall i, (i < j) = true -> f (a .[ i]) = true)). intros b i H1; case b; simpl; try discriminate; intros H2 H3 j Hj; case_eq (j == i); intro Heq. rewrite Int63Properties.eqb_spec in Heq; subst j; auto. - apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; omega. + apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; lia. intros _ i H; eelim ltb_0; eassumption. Qed. @@ -505,7 +505,7 @@ Proof. intros A i a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => (i < j) = true -> f (a .[ i]) = true -> t = true)). intros b j H1 H2 H3 H4; case_eq (i == j). rewrite Int63Properties.eqb_spec; intro; subst i; rewrite H4, orb_true_r; auto. - rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); omega. + rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); lia. intro H; eelim ltb_0; eassumption. Qed. @@ -536,7 +536,7 @@ Proof. intros A a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => t = false -> forall i, (i < j) = true -> f (a .[ i]) = false)). intros b i H1; case b; simpl; try discriminate; intros H2 H3 j Hj; case_eq (j == i); intro Heq. rewrite Int63Properties.eqb_spec in Heq; subst j; auto. - apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; omega. + apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; lia. intros _ i H; eelim ltb_0; eassumption. Qed. @@ -566,15 +566,15 @@ Proof. generalize H; clear H; case_eq (length a <= 1); intro Heq2. unfold afold_right; rewrite Heq1, Heq2; intro H; replace (length a - 1) with 0. split; auto; intros i Hi; elim (ltb_0 i); auto. - rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; assert ([|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; omega. + rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; assert ([|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; lia. pose (P j k := k = false -> (forall i : int, (j <= i) = true -> (i < length a - 1) = true -> f (a .[ i]) = true) /\ f (a .[ length a - 1]) = false); assert (H: P 0 (afold_right bool A true implb f a)). generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P. intros b i H1 H2 H3; case_eq b; intro Heq3. rewrite Heq3 in H3; generalize H3; case (f (a .[ i])); discriminate. destruct (H2 Heq3) as [H4 H5]; split; auto; intros j H6 H7; case_eq (i == j); intro Heq4. rewrite eqb_spec in Heq4; subst j b; generalize H3; case (f (a .[ i])); auto; discriminate. - apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq4; assert ([|i|] <> [|j|]) by (intro H; apply Heq4, to_Z_inj; auto); omega. - intro H; split; auto; intros i H1 H2; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; omega. + apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq4; assert ([|i|] <> [|j|]) by (intro H; apply Heq4, to_Z_inj; auto); lia. + intro H; split; auto; intros i H1 H2; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; lia. unfold P in H; intro H1; destruct (H H1) as [H2 H3]; split; auto; intro i; apply H2, leb_0. Qed. @@ -586,7 +586,7 @@ Proof. intros A a f; case_eq (length a == 0); intro Heq1. intros _; unfold afold_right; rewrite Heq1; auto. case_eq (length a <= 1); intro Heq2. - intros [i [Hi _]]; elim (ltb_0 i); replace 0 with (length a - 1); auto; rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; assert (H1: [|length a|] <> 0%Z) by (intro H; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; change [|1|] with 1%Z in Heq2; omega. + intros [i [Hi _]]; elim (ltb_0 i); replace 0 with (length a - 1); auto; rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; assert (H1: [|length a|] <> 0%Z) by (intro H; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; change [|1|] with 1%Z in Heq2; lia. pose (P j k := (exists i : int, (j <= i) = true /\ (i < length a - 1) = true /\ f (a .[ i]) = false) -> k = true); assert (H: P 0 (afold_right bool A true implb f a)). generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P. intros b i H1 H2 [j [H3 [H4 H5]]]; case_eq (i == j); intro Heq3. @@ -594,9 +594,9 @@ Proof. rewrite H2. case (f (a .[ i])); auto. exists j; repeat split; auto; assert (H: i < j = true). - rewrite ltb_spec; rewrite leb_spec in H3; rewrite eqb_false_spec in Heq3; assert (H: [|i|] <> [|j|]) by (intro H; apply Heq3, to_Z_inj; auto); omega. - rewrite leb_spec, (to_Z_add_1 _ _ H); rewrite ltb_spec in H; omega. - intros [i [H1 [H2 _]]]; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; omega. + rewrite ltb_spec; rewrite leb_spec in H3; rewrite eqb_false_spec in Heq3; assert (H: [|i|] <> [|j|]) by (intro H; apply Heq3, to_Z_inj; auto); lia. + rewrite leb_spec, (to_Z_add_1 _ _ H); rewrite ltb_spec in H; lia. + intros [i [H1 [H2 _]]]; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; lia. unfold P in H; intros [i Hi]; apply H; exists i; split; auto; apply leb_0. Qed. @@ -614,7 +614,7 @@ Proof. apply afold_right_ind_nonempty. intros b i H2 H3; subst b; case (f (a .[ i])); auto. apply not_0_ltb; intro H; rewrite H in Heq; discriminate. - apply H1; rewrite ltb_spec, to_Z_sub_1_diff; [omega| ]; intro H; rewrite H in Heq; discriminate. + apply H1; rewrite ltb_spec, to_Z_sub_1_diff; [lia| ]; intro H; rewrite H in Heq; discriminate. Qed. @@ -626,19 +626,19 @@ Proof. intros A a f; case_eq (length a == 0); intro Heq1. intros _; left; rewrite eqb_spec in Heq1; auto. case_eq (length a <= 1); intro Heq2. - unfold afold_right; rewrite Heq1, Heq2; intro H; right; right; intros i Hi; replace i with 0; auto; apply to_Z_inj; rewrite ltb_spec in Hi; rewrite eqb_false_spec in Heq1; assert (H1: [|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; generalize (leb_0 (length a)) (leb_0 i); rewrite !leb_spec; change [|0|] with 0%Z; omega. + unfold afold_right; rewrite Heq1, Heq2; intro H; right; right; intros i Hi; replace i with 0; auto; apply to_Z_inj; rewrite ltb_spec in Hi; rewrite eqb_false_spec in Heq1; assert (H1: [|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; generalize (leb_0 (length a)) (leb_0 i); rewrite !leb_spec; change [|0|] with 0%Z; lia. pose (P j k := k = true -> (exists i : int, (j <= i) = true /\ (i < length a - 1) = true /\ f (a .[ i]) = false) \/ (forall i : int, (j <= i) = true -> (i < length a) = true -> f (a .[ i]) = true)); assert (H: P 0 (afold_right bool A true implb f a)). generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P. intros b i H1 H2 H3; case_eq b; intro Heq3. destruct (H2 Heq3) as [[j [H4 [H5 H6]]]|H4]. - left; exists j; repeat split; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1) in H4; omega. + left; exists j; repeat split; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1) in H4; lia. case_eq (f (a.[i])); intro Heq4. right; intros j H5 H6; case_eq (i == j); intro Heq5. rewrite eqb_spec in Heq5; subst j; auto. - apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq5; assert ([|i|] <> [|j|]) by (intro H; apply Heq5, to_Z_inj; auto); omega. + apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq5; assert ([|i|] <> [|j|]) by (intro H; apply Heq5, to_Z_inj; auto); lia. left; exists i; repeat split; auto; apply leb_refl. rewrite Heq3 in H3; case_eq (f (a .[ i])); intro Heq4; rewrite Heq4 in H3; try discriminate; left; exists i; repeat split; auto; apply leb_refl. - intros H1; right; intros i H2 H3; replace i with (length a - 1); auto; apply to_Z_inj; rewrite leb_spec in H2; rewrite (to_Z_sub_1 _ _ H3) in *; rewrite ltb_spec in H3; omega. + intros H1; right; intros i H2 H3; replace i with (length a - 1); auto; apply to_Z_inj; rewrite leb_spec in H2; rewrite (to_Z_sub_1 _ _ H3) in *; rewrite ltb_spec in H3; lia. unfold P in H; intro H1; right; destruct (H H1) as [[i [_ H2]]|H2]. left; exists i; auto. right; intro i; apply H2, leb_0. @@ -946,14 +946,14 @@ Lemma existsb_false_spec : forall f from to, forall i, ((from <= i) = true /\ (i <= to) = true) -> f i = false. Proof. unfold existsb;intros; setoid_rewrite leb_spec; apply foldi_cont_ZInd. - intros z Hz; split; auto; intros _ i [H1 H2]; assert (H3 := Z.le_trans _ _ _ H1 H2); elimtype False; omega. + intros z Hz; split; auto; intros _ i [H1 H2]; assert (H3 := Z.le_trans _ _ _ H1 H2); elimtype False; lia. intros i cont H1 H2 H3; case_eq (f i); intro Heq. - split; try discriminate; intro H; rewrite <- Heq; apply H; split; try omega; rewrite leb_spec in H2; auto. + split; try discriminate; intro H; rewrite <- Heq; apply H; split; try lia; rewrite leb_spec in H2; auto. rewrite H3; split; intros H j [Hj1 Hj2]. case_eq (i == j); intro Heq2. rewrite eqb_spec in Heq2; subst j; auto. - apply H; split; auto; rewrite eqb_false_spec in Heq2; assert ([|i|] <> [|j|]) by (intro; apply Heq2, to_Z_inj; auto); omega. - apply H; omega. + apply H; split; auto; rewrite eqb_false_spec in Heq2; assert ([|i|] <> [|j|]) by (intro; apply Heq2, to_Z_inj; auto); lia. + apply H; lia. Qed. @@ -964,8 +964,8 @@ Proof. unfold existsbi;intros A f t; destruct (reflect_eqb 0 (length t)). split; auto. intros _ i Hi. elim (ltb_0 i). rewrite e. auto. rewrite existsb_false_spec. split. - intros H i Hi. apply H. split; [apply leb_0| ]. rewrite leb_spec. rewrite (to_Z_sub_1 _ _ Hi). rewrite ltb_spec in Hi. omega. - intros H i [_ Hi]. apply H. rewrite ltb_spec. rewrite leb_spec in Hi. rewrite to_Z_sub_1_diff in Hi; auto; omega. + intros H i Hi. apply H. split; [apply leb_0| ]. rewrite leb_spec. rewrite (to_Z_sub_1 _ _ Hi). rewrite ltb_spec in Hi. lia. + intros H i [_ Hi]. apply H. rewrite ltb_spec. rewrite leb_spec in Hi. rewrite to_Z_sub_1_diff in Hi; auto; lia. Qed. @@ -976,8 +976,8 @@ Proof. intros A f t; unfold PArray.existsb; case_eq (0 == length t). rewrite eqb_spec; intro H; split; auto; intros _ i Hi; elim (ltb_0 i); rewrite H; auto. intro H; rewrite existsb_false_spec; split. - intros H1 i Hi; apply H1; split; [apply leb_0| ]; rewrite leb_spec, (to_Z_sub_1 _ _ Hi); rewrite ltb_spec in Hi; omega. - intros H1 i [_ H2]; apply H1; rewrite ltb_spec; rewrite leb_spec in H2; rewrite to_Z_sub_1_diff in H2; [omega| ]; intro H3; rewrite H3 in H; discriminate. + intros H1 i Hi; apply H1; split; [apply leb_0| ]; rewrite leb_spec, (to_Z_sub_1 _ _ Hi); rewrite ltb_spec in Hi; lia. + intros H1 i [_ H2]; apply H1; rewrite ltb_spec; rewrite leb_spec in H2; rewrite to_Z_sub_1_diff in H2; [lia| ]; intro H3; rewrite H3 in H; discriminate. Qed. diff --git a/src/SMT_terms.v b/src/SMT_terms.v index c627bc2..169c761 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -416,7 +416,7 @@ Module Typ. | Tindex i => eqb_of_compdec (t_i.[i]).(te_compdec) | TZ => Z.eqb (* Zeq_bool *) | Tbool => Bool.eqb - | Tpositive => Peqb + | Tpositive => Pos.eqb | TBV n => (@BITVECTOR_LIST.bv_eq n) | TFArray ti te => i_eqb (TFArray ti te) end. @@ -1513,7 +1513,7 @@ Qed. | UO_xI => apply_unop Typ.Tpositive Typ.Tpositive xI | UO_Zpos => apply_unop Typ.Tpositive Typ.TZ Zpos | UO_Zneg => apply_unop Typ.Tpositive Typ.TZ Zneg - | UO_Zopp => apply_unop Typ.TZ Typ.TZ Zopp + | UO_Zopp => apply_unop Typ.TZ Typ.TZ Z.opp | UO_BVbitOf s n => apply_unop (Typ.TBV s) Typ.Tbool (BITVECTOR_LIST.bitOf n) | UO_BVnot s => apply_unop (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_not s) | UO_BVneg s => apply_unop (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_neg s) diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index dd1a65f..3a982b2 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -10,8 +10,8 @@ (**************************************************************************) -Require Import Bool List Int63 PArray SMT_classes. -Require Import Misc State SMT_terms FArray. +Require Import Bool List Int63 PArray Psatz. +Require Import Misc State SMT_terms FArray SMT_classes. Import Form. Import Atom. @@ -897,8 +897,6 @@ Section certif. afold_left bool int false orb (Lit.interp rho) a = C.interp rho (to_list a). - Require Import Psatz. - Lemma valid_check_ext lres : C.valid rho (check_ext lres). unfold check_ext, eq_sel_sym. case_eq (Lit.is_pos lres); intro Heq; simpl; try now apply C.interp_true. diff --git a/src/array/FArray.v b/src/array/FArray.v index 1f8c6b4..a17817f 100644 --- a/src/array/FArray.v +++ b/src/array/FArray.v @@ -11,7 +11,8 @@ Require Import Bool OrderedType SMT_classes. -Require Import ProofIrrelevance. (* TODO: REMOVE THIS AXIOM *) +Require Import ProofIrrelevance Classical_Pred_Type ClassicalEpsilon. (* TODO: REMOVE ALL THESE AXIOMS *) + (** This file formalizes functional arrays with extensionality as specified in SMT-LIB 2. It gives realization to axioms that define the SMT-LIB theory of @@ -1777,8 +1778,6 @@ Section FArray. Section Classical_extensionnality. - Require Import Classical_Pred_Type ClassicalEpsilon. - Lemma extensionnality2 : forall a b, a <> b -> (exists i, select a i <> select b i). Proof. intros. diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index d6180a0..55e689d 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -10,9 +10,9 @@ (**************************************************************************) -Require Import Bool OrderedType BinPos ZArith. +Require Import Bool OrderedType BinPos ZArith OrderedTypeEx. Require Import Int63. -Require Import State BVList. +Require Import State BVList FArray. Require Structures. Require Export SMT_classes. @@ -119,8 +119,6 @@ End Bool. Section Z. - Require Import OrderedTypeEx. - Instance Z_ord : OrdType Z. Proof. exists Z_as_OT.lt. @@ -252,8 +250,6 @@ End Z. Section Nat. - Require Import OrderedTypeEx. - Instance Nat_ord : OrdType nat. Proof. @@ -291,9 +287,6 @@ End Nat. Section Positive. - - Require Import OrderedTypeEx. - Instance Positive_ord : OrdType positive. Proof. exists Positive_as_OT.lt. @@ -412,8 +405,6 @@ End BV. Section FArray. - Require Import FArray. - Instance FArray_ord key elt `{key_ord: OrdType key} `{elt_ord: OrdType elt} diff --git a/src/lia/Lia.v b/src/lia/Lia.v index 8c5a597..c214c3b 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -74,7 +74,7 @@ Section certif. match l with | nil => None | h' :: l => - let p := Ppred p in + let p := Pos.pred p in if Atom.eqb h h' then Some p else find_var_aux h p l end. @@ -82,7 +82,7 @@ Section certif. let (count,map) := vm in match find_var_aux h count map with | Some p => (vm, p) - | None => ((Psucc count,h::map), count) + | None => ((Pos.succ count,h::map), count) end. Definition empty_vmap : vmap := (1%positive, nil). @@ -508,7 +508,7 @@ Section certif. intros pvm Heq1 Heq. assert (1 < pvm)%positive. rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega. - assert (Datatypes.length lvm = nat_of_P (Ppred pvm) - 1)%nat. + assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat. rewrite Ppred_minus, Pminus_minus;trivial. change (nat_of_P 1) with 1%nat ;try omega. revert Heq1. @@ -554,7 +554,7 @@ Section certif. intros pvm p Heq1 Heq. assert (1 < pvm)%positive. rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega. - assert (Datatypes.length lvm = nat_of_P (Ppred pvm) - 1)%nat. + assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat. rewrite Ppred_minus, Pminus_minus;trivial. change (nat_of_P 1) with 1%nat ;try omega. revert Heq1. @@ -562,8 +562,8 @@ Section certif. intros Heq1;inversion Heq1;clear Heq1;subst. unfold is_true;rewrite andb_true_iff;intros (H1,H2). assert (1 < nat_of_P pvm)%nat by (rewrite Plt_lt in H;trivial). - assert (W:=nat_of_P_pos (Ppred pvm)). - assert (nat_of_P (pvm - Ppred pvm) - 1 = 0)%nat. + assert (W:=nat_of_P_pos (Pos.pred pvm)). + assert (nat_of_P (pvm - Pos.pred pvm) - 1 = 0)%nat. rewrite Pminus_minus;try omega. apply Plt_lt;omega. rewrite H4;simpl. @@ -571,10 +571,10 @@ Section certif. rewrite Hz;trivial. unfold is_true;rewrite andb_true_iff;intros Heq1 (H1,H2). assert (W:= find_var_aux_lt _ _ _ _ Heq1 H0). - assert (nat_of_P (pvm - p) - 1 = S (nat_of_P (Ppred pvm - p) - 1))%nat. + assert (nat_of_P (pvm - p) - 1 = S (nat_of_P (Pos.pred pvm - p) - 1))%nat. assert (W1:= W);rewrite <- Plt_lt in W. rewrite !Pminus_minus;trivial. - assert (W2:=nat_of_P_pos (Ppred pvm)). + assert (W2:=nat_of_P_pos (Pos.pred pvm)). omega. rewrite Plt_lt. apply lt_trans with (1:= W1);omega. @@ -585,7 +585,7 @@ Section certif. rewrite Hh;trivial. rewrite Psucc_S;omega. intros p Hlt; - assert (nat_of_P (Psucc pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat. + assert (nat_of_P (Pos.succ pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat. assert (W1:= Hlt);rewrite <- Plt_lt in W1. rewrite !Pminus_minus;trivial. rewrite Psucc_S;omega. @@ -595,7 +595,7 @@ Section certif. rewrite Zpos_succ_morphism;omega. destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ Hh) as (z,Hz). rewrite Hz;unfold interp_vmap;simpl. - assert (nat_of_P (Psucc pvm - pvm) = 1%nat). + assert (nat_of_P (Pos.succ pvm - pvm) = 1%nat). rewrite Pplus_one_succ_l, Pminus_minus, Pplus_plus. change (nat_of_P 1) with 1%nat;omega. rewrite Plt_lt, Pplus_plus. @@ -611,7 +611,7 @@ Section certif. Proof. unfold is_true;induction pe;simpl;trivial. rewrite <- !Zlt_is_lt_bool; rewrite <- Ple_le in H. - intros H1;apply Zlt_le_trans with (1:= H1);trivial. + intros H1;apply Z.lt_le_trans with (1:= H1);trivial. rewrite !andb_true_iff;intros (H1,H2);auto. rewrite !andb_true_iff;intros (H1,H2);auto. rewrite !andb_true_iff;intros (H1,H2);auto. diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml index 203077b..64f0b20 100644 --- a/src/smtlib2/smtlib2_genConstr.ml +++ b/src/smtlib2/smtlib2_genConstr.ml @@ -98,10 +98,10 @@ let rec sort_of_sort = function let declare_sort rt sym = let s = string_of_symbol sym in - let cons_t = declare_new_type (Names.id_of_string ("Smt_sort_"^s)) in + let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in let compdec_type = mklApp cCompDec [| cons_t |] in let compdec_var = - declare_new_variable (Names.id_of_string ("CompDec_"^s)) compdec_type in + Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in let ce = mklApp cTyp_compdec [|cons_t; compdec_var|] in let res = SmtBtype.declare rt cons_t ce in VeritSyntax.add_btype s res; @@ -115,7 +115,7 @@ let declare_fun rt ro sym arg cod = let coqTy = List.fold_right (fun typ c -> Term.mkArrow (interp_to_coq rt typ) c) tyl (interp_to_coq rt ty) in - let cons_v = declare_new_variable (Names.id_of_string ("Smt_var_"^s)) coqTy in + let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in let op = Op.declare ro cons_v (Array.of_list tyl) ty None in VeritSyntax.add_fun s op; op diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 895d217..ad5ec1d 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -11,6 +11,7 @@ open Coqlib +open SmtMisc let gen_constant = Structures.gen_constant @@ -274,7 +275,7 @@ let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "i let make_certif_ops modules args = let gen_constant c = match args with - | Some args -> lazy (SmtMisc.mklApp (gen_constant modules c) args) + | Some args -> lazy (mklApp (gen_constant modules c) args) | None -> gen_constant modules c in (gen_constant "step", gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten", @@ -300,14 +301,14 @@ let make_certif_ops modules args = (** Useful constructions *) let ceq_refl_true = - lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|]) + lazy (mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|]) let eq_refl_true () = Lazy.force ceq_refl_true let vm_cast_true_no_check t = - Term.mkCast(eq_refl_true (), - Term.VMcast, - SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]) + Structures.mkCast(eq_refl_true (), + Structures.vmcast, + mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]) (* This version checks convertibility right away instead of delaying it at Qed. This allows to report issues to the user as soon as he/she runs one of @@ -315,9 +316,9 @@ let vm_cast_true_no_check t = let vm_cast_true env t = try Structures.vm_conv Reduction.CUMUL env - (SmtMisc.mklApp ceq + (mklApp ceq [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|]) - (SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]); + (mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]); vm_cast_true_no_check t with Reduction.NotConvertible -> Structures.error ("SMTCoq was not able to check the proof certificate.") @@ -326,19 +327,19 @@ let vm_cast_true env t = (* Compute a nat *) let rec mkNat = function | 0 -> Lazy.force cO - | i -> SmtMisc.mklApp cS [|mkNat (i-1)|] + | i -> mklApp cS [|mkNat (i-1)|] (* Compute a positive *) let rec mkPositive = function | 1 -> Lazy.force cxH | i -> let c = if (i mod 2) = 0 then cxO else cxI in - SmtMisc.mklApp c [|mkPositive (i / 2)|] + mklApp c [|mkPositive (i / 2)|] (* Compute a N *) let mkN = function | 0 -> Lazy.force cN0 - | i -> SmtMisc.mklApp cNpos [|mkPositive i|] + | i -> mklApp cNpos [|mkPositive i|] (* Compute a Boolean *) let mkBool = function @@ -347,47 +348,47 @@ let mkBool = function (* Compute a Boolean list *) let rec mk_bv_list = function - | [] -> SmtMisc.mklApp cnil [|Lazy.force cbool|] + | [] -> mklApp cnil [|Lazy.force cbool|] | b :: bv -> - SmtMisc.mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|] + mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|] (* Reification *) let mk_bool b = - let c, args = Term.decompose_app b in - if Term.eq_constr c (Lazy.force ctrue) then true - else if Term.eq_constr c (Lazy.force cfalse) then false + let c, args = Structures.decompose_app b in + if Structures.eq_constr c (Lazy.force ctrue) then true + else if Structures.eq_constr c (Lazy.force cfalse) then false else assert false let rec mk_bool_list bs = - let c, args = Term.decompose_app bs in - if Term.eq_constr c (Lazy.force cnil) then [] - else if Term.eq_constr c (Lazy.force ccons) then + let c, args = Structures.decompose_app bs in + if Structures.eq_constr c (Lazy.force cnil) then [] + else if Structures.eq_constr c (Lazy.force ccons) then match args with | [_; b; bs] -> mk_bool b :: mk_bool_list bs | _ -> assert false else assert false let rec mk_nat n = - let c, args = Term.decompose_app n in - if Term.eq_constr c (Lazy.force cO) then + let c, args = Structures.decompose_app n in + if Structures.eq_constr c (Lazy.force cO) then 0 - else if Term.eq_constr c (Lazy.force cS) then + else if Structures.eq_constr c (Lazy.force cS) then match args with | [n] -> (mk_nat n) + 1 | _ -> assert false else assert false let rec mk_positive n = - let c, args = Term.decompose_app n in - if Term.eq_constr c (Lazy.force cxH) then + let c, args = Structures.decompose_app n in + if Structures.eq_constr c (Lazy.force cxH) then 1 - else if Term.eq_constr c (Lazy.force cxO) then + else if Structures.eq_constr c (Lazy.force cxO) then match args with | [n] -> 2 * (mk_positive n) | _ -> assert false - else if Term.eq_constr c (Lazy.force cxI) then + else if Structures.eq_constr c (Lazy.force cxI) then match args with | [n] -> 2 * (mk_positive n) + 1 | _ -> assert false @@ -395,10 +396,10 @@ let rec mk_positive n = let mk_N n = - let c, args = Term.decompose_app n in - if Term.eq_constr c (Lazy.force cN0) then + let c, args = Structures.decompose_app n in + if Structures.eq_constr c (Lazy.force cN0) then 0 - else if Term.eq_constr c (Lazy.force cNpos) then + else if Structures.eq_constr c (Lazy.force cNpos) then match args with | [n] -> mk_positive n | _ -> assert false @@ -406,13 +407,13 @@ let mk_N n = let mk_Z n = - let c, args = Term.decompose_app n in - if Term.eq_constr c (Lazy.force cZ0) then 0 - else if Term.eq_constr c (Lazy.force cZpos) then + let c, args = Structures.decompose_app n in + if Structures.eq_constr c (Lazy.force cZ0) then 0 + else if Structures.eq_constr c (Lazy.force cZpos) then match args with | [n] -> mk_positive n | _ -> assert false - else if Term.eq_constr c (Lazy.force cZneg) then + else if Structures.eq_constr c (Lazy.force cZneg) then match args with | [n] -> - mk_positive n | _ -> assert false @@ -421,12 +422,12 @@ let mk_Z n = (* size of bivectors are either N.of_nat (length l) or an N *) let mk_bvsize n = - let c, args = Term.decompose_app n in - if Term.eq_constr c (Lazy.force cof_nat) then + let c, args = Structures.decompose_app n in + if Structures.eq_constr c (Lazy.force cof_nat) then match args with | [nl] -> - let c, args = Term.decompose_app nl in - if Term.eq_constr c (Lazy.force clength) then + let c, args = Structures.decompose_app nl in + if Structures.eq_constr c (Lazy.force clength) then match args with | [_; l] -> List.length (mk_bool_list l) | _ -> assert false diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index 9aeddac..bf626b3 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -10,254 +10,254 @@ (**************************************************************************) -val gen_constant : string list list -> string -> Term.constr lazy_t +val gen_constant : string list list -> string -> Structures.constr lazy_t (* Int63 *) -val cint : Term.constr lazy_t -val ceq63 : Term.constr lazy_t +val cint : Structures.constr lazy_t +val ceq63 : Structures.constr lazy_t (* PArray *) -val carray : Term.constr lazy_t +val carray : Structures.constr lazy_t (* nat *) -val cnat : Term.constr lazy_t -val cO : Term.constr lazy_t -val cS : Term.constr lazy_t +val cnat : Structures.constr lazy_t +val cO : Structures.constr lazy_t +val cS : Structures.constr lazy_t (* Positive *) -val cpositive : Term.constr lazy_t -val cxI : Term.constr lazy_t -val cxO : Term.constr lazy_t -val cxH : Term.constr lazy_t -val ceqbP : Term.constr lazy_t +val cpositive : Structures.constr lazy_t +val cxI : Structures.constr lazy_t +val cxO : Structures.constr lazy_t +val cxH : Structures.constr lazy_t +val ceqbP : Structures.constr lazy_t (* N *) -val cN : Term.constr lazy_t -val cN0 : Term.constr lazy_t -val cNpos : Term.constr lazy_t -val cof_nat : Term.constr lazy_t +val cN : Structures.constr lazy_t +val cN0 : Structures.constr lazy_t +val cNpos : Structures.constr lazy_t +val cof_nat : Structures.constr lazy_t (* Z *) -val cZ : Term.constr lazy_t -val cZ0 : Term.constr lazy_t -val cZpos : Term.constr lazy_t -val cZneg : Term.constr lazy_t -val copp : Term.constr lazy_t -val cadd : Term.constr lazy_t -val csub : Term.constr lazy_t -val cmul : Term.constr lazy_t -val cltb : Term.constr lazy_t -val cleb : Term.constr lazy_t -val cgeb : Term.constr lazy_t -val cgtb : Term.constr lazy_t -val ceqbZ : Term.constr lazy_t +val cZ : Structures.constr lazy_t +val cZ0 : Structures.constr lazy_t +val cZpos : Structures.constr lazy_t +val cZneg : Structures.constr lazy_t +val copp : Structures.constr lazy_t +val cadd : Structures.constr lazy_t +val csub : Structures.constr lazy_t +val cmul : Structures.constr lazy_t +val cltb : Structures.constr lazy_t +val cleb : Structures.constr lazy_t +val cgeb : Structures.constr lazy_t +val cgtb : Structures.constr lazy_t +val ceqbZ : Structures.constr lazy_t (* Booleans *) -val cbool : Term.constr lazy_t -val ctrue : Term.constr lazy_t -val cfalse : Term.constr lazy_t -val candb : Term.constr lazy_t -val corb : Term.constr lazy_t -val cxorb : Term.constr lazy_t -val cnegb : Term.constr lazy_t -val cimplb : Term.constr lazy_t -val ceqb : Term.constr lazy_t -val cifb : Term.constr lazy_t -val ciff : Term.constr lazy_t -val creflect : Term.constr lazy_t +val cbool : Structures.constr lazy_t +val ctrue : Structures.constr lazy_t +val cfalse : Structures.constr lazy_t +val candb : Structures.constr lazy_t +val corb : Structures.constr lazy_t +val cxorb : Structures.constr lazy_t +val cnegb : Structures.constr lazy_t +val cimplb : Structures.constr lazy_t +val ceqb : Structures.constr lazy_t +val cifb : Structures.constr lazy_t +val ciff : Structures.constr lazy_t +val creflect : Structures.constr lazy_t (* Lists *) -val clist : Term.constr lazy_t -val cnil : Term.constr lazy_t -val ccons : Term.constr lazy_t -val clength : Term.constr lazy_t +val clist : Structures.constr lazy_t +val cnil : Structures.constr lazy_t +val ccons : Structures.constr lazy_t +val clength : Structures.constr lazy_t (* Option *) -val coption : Term.constr lazy_t -val cSome : Term.constr lazy_t -val cNone : Term.constr lazy_t +val coption : Structures.constr lazy_t +val cSome : Structures.constr lazy_t +val cNone : Structures.constr lazy_t (* Pairs *) -val cpair : Term.constr lazy_t -val cprod : Term.constr lazy_t +val cpair : Structures.constr lazy_t +val cprod : Structures.constr lazy_t (* Dependent pairs *) -val csigT : Term.constr lazy_t +val csigT : Structures.constr lazy_t (* Logical Operators *) -val cnot : Term.constr lazy_t -val ceq : Term.constr lazy_t -val crefl_equal : Term.constr lazy_t -val cconj : Term.constr lazy_t -val cand : Term.constr lazy_t +val cnot : Structures.constr lazy_t +val ceq : Structures.constr lazy_t +val crefl_equal : Structures.constr lazy_t +val cconj : Structures.constr lazy_t +val cand : Structures.constr lazy_t (* Bit vectors *) -val cbitvector : Term.constr lazy_t -val cof_bits : Term.constr lazy_t -val cbitOf : Term.constr lazy_t -val cbv_eq : Term.constr lazy_t -val cbv_not : Term.constr lazy_t -val cbv_neg : Term.constr lazy_t -val cbv_and : Term.constr lazy_t -val cbv_or : Term.constr lazy_t -val cbv_xor : Term.constr lazy_t -val cbv_add : Term.constr lazy_t -val cbv_mult : Term.constr lazy_t -val cbv_ult : Term.constr lazy_t -val cbv_slt : Term.constr lazy_t -val cbv_concat : Term.constr lazy_t -val cbv_extr : Term.constr lazy_t -val cbv_zextn : Term.constr lazy_t -val cbv_sextn : Term.constr lazy_t -val cbv_shl : Term.constr lazy_t -val cbv_shr : Term.constr lazy_t +val cbitvector : Structures.constr lazy_t +val cof_bits : Structures.constr lazy_t +val cbitOf : Structures.constr lazy_t +val cbv_eq : Structures.constr lazy_t +val cbv_not : Structures.constr lazy_t +val cbv_neg : Structures.constr lazy_t +val cbv_and : Structures.constr lazy_t +val cbv_or : Structures.constr lazy_t +val cbv_xor : Structures.constr lazy_t +val cbv_add : Structures.constr lazy_t +val cbv_mult : Structures.constr lazy_t +val cbv_ult : Structures.constr lazy_t +val cbv_slt : Structures.constr lazy_t +val cbv_concat : Structures.constr lazy_t +val cbv_extr : Structures.constr lazy_t +val cbv_zextn : Structures.constr lazy_t +val cbv_sextn : Structures.constr lazy_t +val cbv_shl : Structures.constr lazy_t +val cbv_shr : Structures.constr lazy_t (* Arrays *) -val cfarray : Term.constr lazy_t -val cselect : Term.constr lazy_t -val cstore : Term.constr lazy_t -val cdiff : Term.constr lazy_t -val cequalarray : Term.constr lazy_t +val cfarray : Structures.constr lazy_t +val cselect : Structures.constr lazy_t +val cstore : Structures.constr lazy_t +val cdiff : Structures.constr lazy_t +val cequalarray : Structures.constr lazy_t (* OrderedType *) (* SMT_terms *) -val cState_C_t : Term.constr lazy_t -val cState_S_t : Term.constr lazy_t - -val cdistinct : Term.constr lazy_t - -val ctype : Term.constr lazy_t -val cTZ : Term.constr lazy_t -val cTbool : Term.constr lazy_t -val cTpositive : Term.constr lazy_t -val cTBV : Term.constr lazy_t -val cTFArray : Term.constr lazy_t -val cTindex : Term.constr lazy_t - -val cinterp_t : Term.constr lazy_t -val cdec_interp : Term.constr lazy_t -val cord_interp : Term.constr lazy_t -val ccomp_interp : Term.constr lazy_t -val cinh_interp : Term.constr lazy_t - -val cinterp_eqb : Term.constr lazy_t - -val ctyp_compdec : Term.constr lazy_t -val cTyp_compdec : Term.constr lazy_t -val cunit_typ_compdec : Term.constr lazy_t -val cte_carrier : Term.constr lazy_t -val cte_compdec : Term.constr lazy_t -val ceqb_of_compdec : Term.constr lazy_t -val cCompDec : Term.constr lazy_t - -val cbool_compdec : Term.constr lazy_t -val cZ_compdec : Term.constr lazy_t -val cPositive_compdec : Term.constr lazy_t -val cBV_compdec : Term.constr lazy_t -val cFArray_compdec : Term.constr lazy_t - -val ctval : Term.constr lazy_t -val cTval : Term.constr lazy_t - -val cCO_xH : Term.constr lazy_t -val cCO_Z0 : Term.constr lazy_t -val cCO_BV : Term.constr lazy_t - -val cUO_xO : Term.constr lazy_t -val cUO_xI : Term.constr lazy_t -val cUO_Zpos : Term.constr lazy_t -val cUO_Zneg : Term.constr lazy_t -val cUO_Zopp : Term.constr lazy_t -val cUO_BVbitOf : Term.constr lazy_t -val cUO_BVnot : Term.constr lazy_t -val cUO_BVneg : Term.constr lazy_t -val cUO_BVextr : Term.constr lazy_t -val cUO_BVzextn : Term.constr lazy_t -val cUO_BVsextn : Term.constr lazy_t - -val cBO_Zplus : Term.constr lazy_t -val cBO_Zminus : Term.constr lazy_t -val cBO_Zmult : Term.constr lazy_t -val cBO_Zlt : Term.constr lazy_t -val cBO_Zle : Term.constr lazy_t -val cBO_Zge : Term.constr lazy_t -val cBO_Zgt : Term.constr lazy_t -val cBO_eq : Term.constr lazy_t -val cBO_BVand : Term.constr lazy_t -val cBO_BVor : Term.constr lazy_t -val cBO_BVxor : Term.constr lazy_t -val cBO_BVadd : Term.constr lazy_t -val cBO_BVmult : Term.constr lazy_t -val cBO_BVult : Term.constr lazy_t -val cBO_BVslt : Term.constr lazy_t -val cBO_BVconcat : Term.constr lazy_t -val cBO_BVshl : Term.constr lazy_t -val cBO_BVshr : Term.constr lazy_t -val cBO_select : Term.constr lazy_t -val cBO_diffarray : Term.constr lazy_t - -val cTO_store : Term.constr lazy_t - -val cNO_distinct : Term.constr lazy_t - -val catom : Term.constr lazy_t -val cAcop : Term.constr lazy_t -val cAuop : Term.constr lazy_t -val cAbop : Term.constr lazy_t -val cAtop : Term.constr lazy_t -val cAnop : Term.constr lazy_t -val cAapp : Term.constr lazy_t - -val cform : Term.constr lazy_t -val cFatom : Term.constr lazy_t -val cFtrue : Term.constr lazy_t -val cFfalse : Term.constr lazy_t -val cFnot2 : Term.constr lazy_t -val cFand : Term.constr lazy_t -val cFor : Term.constr lazy_t -val cFxor : Term.constr lazy_t -val cFimp : Term.constr lazy_t -val cFiff : Term.constr lazy_t -val cFite : Term.constr lazy_t -val cFbbT : Term.constr lazy_t - -val cis_true : Term.constr lazy_t - -val cvalid_sat_checker : Term.constr lazy_t -val cinterp_var_sat_checker : Term.constr lazy_t +val cState_C_t : Structures.constr lazy_t +val cState_S_t : Structures.constr lazy_t + +val cdistinct : Structures.constr lazy_t + +val ctype : Structures.constr lazy_t +val cTZ : Structures.constr lazy_t +val cTbool : Structures.constr lazy_t +val cTpositive : Structures.constr lazy_t +val cTBV : Structures.constr lazy_t +val cTFArray : Structures.constr lazy_t +val cTindex : Structures.constr lazy_t + +val cinterp_t : Structures.constr lazy_t +val cdec_interp : Structures.constr lazy_t +val cord_interp : Structures.constr lazy_t +val ccomp_interp : Structures.constr lazy_t +val cinh_interp : Structures.constr lazy_t + +val cinterp_eqb : Structures.constr lazy_t + +val ctyp_compdec : Structures.constr lazy_t +val cTyp_compdec : Structures.constr lazy_t +val cunit_typ_compdec : Structures.constr lazy_t +val cte_carrier : Structures.constr lazy_t +val cte_compdec : Structures.constr lazy_t +val ceqb_of_compdec : Structures.constr lazy_t +val cCompDec : Structures.constr lazy_t + +val cbool_compdec : Structures.constr lazy_t +val cZ_compdec : Structures.constr lazy_t +val cPositive_compdec : Structures.constr lazy_t +val cBV_compdec : Structures.constr lazy_t +val cFArray_compdec : Structures.constr lazy_t + +val ctval : Structures.constr lazy_t +val cTval : Structures.constr lazy_t + +val cCO_xH : Structures.constr lazy_t +val cCO_Z0 : Structures.constr lazy_t +val cCO_BV : Structures.constr lazy_t + +val cUO_xO : Structures.constr lazy_t +val cUO_xI : Structures.constr lazy_t +val cUO_Zpos : Structures.constr lazy_t +val cUO_Zneg : Structures.constr lazy_t +val cUO_Zopp : Structures.constr lazy_t +val cUO_BVbitOf : Structures.constr lazy_t +val cUO_BVnot : Structures.constr lazy_t +val cUO_BVneg : Structures.constr lazy_t +val cUO_BVextr : Structures.constr lazy_t +val cUO_BVzextn : Structures.constr lazy_t +val cUO_BVsextn : Structures.constr lazy_t + +val cBO_Zplus : Structures.constr lazy_t +val cBO_Zminus : Structures.constr lazy_t +val cBO_Zmult : Structures.constr lazy_t +val cBO_Zlt : Structures.constr lazy_t +val cBO_Zle : Structures.constr lazy_t +val cBO_Zge : Structures.constr lazy_t +val cBO_Zgt : Structures.constr lazy_t +val cBO_eq : Structures.constr lazy_t +val cBO_BVand : Structures.constr lazy_t +val cBO_BVor : Structures.constr lazy_t +val cBO_BVxor : Structures.constr lazy_t +val cBO_BVadd : Structures.constr lazy_t +val cBO_BVmult : Structures.constr lazy_t +val cBO_BVult : Structures.constr lazy_t +val cBO_BVslt : Structures.constr lazy_t +val cBO_BVconcat : Structures.constr lazy_t +val cBO_BVshl : Structures.constr lazy_t +val cBO_BVshr : Structures.constr lazy_t +val cBO_select : Structures.constr lazy_t +val cBO_diffarray : Structures.constr lazy_t + +val cTO_store : Structures.constr lazy_t + +val cNO_distinct : Structures.constr lazy_t + +val catom : Structures.constr lazy_t +val cAcop : Structures.constr lazy_t +val cAuop : Structures.constr lazy_t +val cAbop : Structures.constr lazy_t +val cAtop : Structures.constr lazy_t +val cAnop : Structures.constr lazy_t +val cAapp : Structures.constr lazy_t + +val cform : Structures.constr lazy_t +val cFatom : Structures.constr lazy_t +val cFtrue : Structures.constr lazy_t +val cFfalse : Structures.constr lazy_t +val cFnot2 : Structures.constr lazy_t +val cFand : Structures.constr lazy_t +val cFor : Structures.constr lazy_t +val cFxor : Structures.constr lazy_t +val cFimp : Structures.constr lazy_t +val cFiff : Structures.constr lazy_t +val cFite : Structures.constr lazy_t +val cFbbT : Structures.constr lazy_t + +val cis_true : Structures.constr lazy_t + +val cvalid_sat_checker : Structures.constr lazy_t +val cinterp_var_sat_checker : Structures.constr lazy_t val make_certif_ops : string list list -> - Term.constr array option -> - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t * - Term.constr lazy_t * Term.constr lazy_t + Structures.constr array option -> + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t * + Structures.constr lazy_t * Structures.constr lazy_t (* Some constructions *) -val ceq_refl_true : Term.constr lazy_t -val eq_refl_true : unit -> Term.constr -val vm_cast_true_no_check : Term.constr -> Term.constr -val vm_cast_true : Environ.env -> Term.constr -> Term.constr -val mkNat : int -> Term.constr -val mkN : int -> Term.constr -val mk_bv_list : bool list -> Term.constr +val ceq_refl_true : Structures.constr lazy_t +val eq_refl_true : unit -> Structures.constr +val vm_cast_true_no_check : Structures.constr -> Structures.constr +val vm_cast_true : Environ.env -> Structures.constr -> Structures.constr +val mkNat : int -> Structures.constr +val mkN : int -> Structures.constr +val mk_bv_list : bool list -> Structures.constr (* Reification *) -val mk_bool : Term.constr -> bool -val mk_bool_list : Term.constr -> bool list -val mk_nat : Term.constr -> int -val mk_N : Term.constr -> int -val mk_Z : Term.constr -> int -val mk_bvsize : Term.constr -> int +val mk_bool : Structures.constr -> bool +val mk_bool_list : Structures.constr -> bool list +val mk_nat : Structures.constr -> int +val mk_N : Structures.constr -> int +val mk_Z : Structures.constr -> int +val mk_bvsize : Structures.constr -> int diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml index 549462c..c91cee1 100644 --- a/src/trace/satAtom.ml +++ b/src/trace/satAtom.ml @@ -27,7 +27,7 @@ module Atom = type reify_tbl = { mutable count : int; - tbl : (Term.constr, int) Hashtbl.t + tbl : (Structures.constr, int) Hashtbl.t } let create () = diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli index 4ecfae3..49bc590 100644 --- a/src/trace/satAtom.mli +++ b/src/trace/satAtom.mli @@ -23,13 +23,13 @@ module Atom : sig type reify_tbl = { mutable count : int; - tbl : (Term.constr, t) Hashtbl.t; + tbl : (Structures.constr, t) Hashtbl.t; } val create : unit -> reify_tbl - val declare : reify_tbl -> Term.constr -> t - val get : reify_tbl -> Term.constr -> t - val atom_tbl : reify_tbl -> Term.constr array - val interp_tbl : reify_tbl -> Term.constr + val declare : reify_tbl -> Structures.constr -> t + val get : reify_tbl -> Structures.constr -> t + val atom_tbl : reify_tbl -> Structures.constr array + val interp_tbl : reify_tbl -> Structures.constr end diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 330884b..16d9bdb 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -68,7 +68,7 @@ type nop = type op_def = { tparams : btype array; tres : btype; - op_val : Term.constr } + op_val : Structures.constr } type index = Index of int | Rel_name of string @@ -80,14 +80,14 @@ let destruct s (i, hval) = match i with | Rel_name _ -> failwith s let dummy_indexed_op i dom codom = - (i, {tparams = dom; tres = codom; op_val = Term.mkProp}) + (i, {tparams = dom; tres = codom; op_val = Structures.mkProp}) let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in index let debruijn_indexed_op i ty = - (Index i, {tparams = [||]; tres = ty; op_val = Term.mkRel i}) + (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i}) module Op = struct @@ -339,7 +339,7 @@ module Op = (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Term.constr, indexed_op) Hashtbl.t + tbl : (Structures.constr, indexed_op) Hashtbl.t } let create () = @@ -692,7 +692,7 @@ module Atom = Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta; Format.fprintf fmt ") ( "; SmtBtype.to_smt fmt bt; - Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Printer.pr_constr t)) + Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t)) and to_smt_bop op h1 h2 = let s = match op with @@ -1019,8 +1019,8 @@ module Atom = else CCunknown_deps (gobble_of_coq_cst cc) with Not_found -> CCunknown in - let rec mk_hatom (h : Term.constr) = - let c, args = Term.decompose_app h in + let rec mk_hatom (h : Structures.constr) = + let c, args = Structures.decompose_app h in match get_cst c with | CCxH -> mk_cop CCxH args | CCZ0 -> mk_cop CCZ0 args @@ -1248,10 +1248,10 @@ module Atom = with | Not_found -> let targs = Array.map type_of hargs in let tres = SmtBtype.of_coq rt known_logic ty in - let os = if Term.isRel c then - let i = Term.destRel c in + let os = if Structures.isRel c then + let i = Structures.destRel c in let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in - Some (string_of_name n) + Some (Structures.string_of_name n) else None in @@ -1267,7 +1267,7 @@ module Atom = [gobble] *) and mk_unknown_deps c args ty gobble = let deps, args = split_list_at gobble args in - let c = Term.mkApp (c, Array.of_list deps) in + let c = Structures.mkApp (c, Array.of_list deps) in mk_unknown c args ty in @@ -1320,12 +1320,12 @@ module Atom = let pc = match atom a with | Acop c -> Op.interp_cop c - | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|]) + | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|]) | Abop (op,h1,h2) -> - Term.mkApp (Op.interp_bop t_i op, + Structures.mkApp (Op.interp_bop t_i op, [|interp_atom h1; interp_atom h2|]) | Atop (op,h1,h2,h3) -> - Term.mkApp (Op.interp_top t_i op, + Structures.mkApp (Op.interp_top t_i op, [|interp_atom h1; interp_atom h2; interp_atom h3|]) | Anop (NO_distinct ty as op,ha) -> let cop = Op.interp_nop t_i op in @@ -1333,9 +1333,9 @@ module Atom = let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in - Term.mkApp (cop,[|cargs|]) + Structures.mkApp (cop,[|cargs|]) | Aapp (op,t) -> - Term.mkApp ((snd op).op_val, Array.map interp_atom t) in + Structures.mkApp ((snd op).op_val, Array.map interp_atom t) in Hashtbl.add atom_tbl l pc; pc in interp_atom a diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index a542ad6..a6a1761 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -76,14 +76,14 @@ module Op : val create : unit -> reify_tbl - val declare : reify_tbl -> Term.constr -> btype array -> + val declare : reify_tbl -> Structures.constr -> btype array -> btype -> string option -> indexed_op - val of_coq : reify_tbl -> Term.constr -> indexed_op + val of_coq : reify_tbl -> Structures.constr -> indexed_op - val interp_tbl : Term.constr -> - (btype array -> btype -> Term.constr -> Term.constr) -> - reify_tbl -> Term.constr + val interp_tbl : Structures.constr -> + (btype array -> btype -> Structures.constr -> Structures.constr) -> + reify_tbl -> Structures.constr val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list @@ -143,18 +143,18 @@ module Atom : (** Given a coq term, build the corresponding atom *) val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl -> - reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Term.constr -> t + reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t - val get_coq_term_op : int -> Term.constr + val get_coq_term_op : int -> Structures.constr - val to_coq : t -> Term.constr + val to_coq : t -> Structures.constr val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array - val interp_tbl : reify_tbl -> Term.constr + val interp_tbl : reify_tbl -> Structures.constr - val interp_to_coq : Term.constr -> (int, Term.constr) Hashtbl.t -> - t -> Term.constr + val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t -> + t -> Structures.constr val logic : t -> SmtMisc.logic @@ -202,5 +202,5 @@ module Trace : sig end -val make_t_i : SmtBtype.reify_tbl -> Term.constr -val make_t_func : Op.reify_tbl -> Term.constr -> Term.constr +val make_t_i : SmtBtype.reify_tbl -> Structures.constr +val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml index 119c046..948acaa 100644 --- a/src/trace/smtBtype.ml +++ b/src/trace/smtBtype.ml @@ -15,9 +15,9 @@ open CoqTerms (** Syntaxified version of Coq type *) -type indexed_type = Term.constr gen_hashed +type indexed_type = Structures.constr gen_hashed -let dummy_indexed_type i = {index = i; hval = Term.mkProp} +let dummy_indexed_type i = {index = i; hval = Structures.mkProp} let indexed_type_index i = i.index let indexed_type_hval i = i.hval @@ -76,8 +76,8 @@ let rec logic = function (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Term.constr, btype) Hashtbl.t; - mutable cuts : (Structures.names_id * Term.types) list; + tbl : (Structures.constr, btype) Hashtbl.t; + mutable cuts : (Structures.id * Structures.types) list; unsup_tbl : (btype, btype) Hashtbl.t; } @@ -175,8 +175,8 @@ let rec compdec_btype reify = function [|interp_to_coq reify ti; interp_to_coq reify te; compdec_btype reify ti; compdec_btype reify te|] | Tindex i -> - let c, args = Term.decompose_app i.hval in - if Term.eq_constr c (Lazy.force cTyp_compdec) then + let c, args = Structures.decompose_app i.hval in + if Structures.eq_constr c (Lazy.force cTyp_compdec) then match args with | [_; tic] -> tic | _ -> assert false @@ -195,22 +195,22 @@ let declare_and_compdec reify t ty = let rec of_coq reify known_logic t = try - let c, args = Term.decompose_app t in - if Term.eq_constr c (Lazy.force cbool) || - Term.eq_constr c (Lazy.force cTbool) then Tbool - else if Term.eq_constr c (Lazy.force cZ) || - Term.eq_constr c (Lazy.force cTZ) then + let c, args = Structures.decompose_app t in + if Structures.eq_constr c (Lazy.force cbool) || + Structures.eq_constr c (Lazy.force cTbool) then Tbool + else if Structures.eq_constr c (Lazy.force cZ) || + Structures.eq_constr c (Lazy.force cTZ) then check_known TZ known_logic - else if Term.eq_constr c (Lazy.force cpositive) || - Term.eq_constr c (Lazy.force cTpositive) then + else if Structures.eq_constr c (Lazy.force cpositive) || + Structures.eq_constr c (Lazy.force cTpositive) then check_known Tpositive known_logic - else if Term.eq_constr c (Lazy.force cbitvector) || - Term.eq_constr c (Lazy.force cTBV) then + else if Structures.eq_constr c (Lazy.force cbitvector) || + Structures.eq_constr c (Lazy.force cTBV) then match args with | [s] -> check_known (TBV (mk_bvsize s)) known_logic | _ -> assert false - else if Term.eq_constr c (Lazy.force cfarray) || - Term.eq_constr c (Lazy.force cTFArray) then + else if Structures.eq_constr c (Lazy.force cfarray) || + Structures.eq_constr c (Lazy.force cTFArray) then match args with | ti :: te :: _ -> let ty = TFArray (of_coq reify known_logic ti, @@ -221,8 +221,8 @@ let rec of_coq reify known_logic t = try Hashtbl.find reify.tbl t with Not_found -> let n = string_of_int (List.length reify.cuts) in - let compdec_name = Names.id_of_string ("CompDec"^n) in - let compdec_var = Term.mkVar compdec_name in + let compdec_name = Structures.mkId ("CompDec"^n) in + let compdec_var = Structures.mkVar compdec_name in let compdec_type = mklApp cCompDec [| t |]in reify.cuts <- (compdec_name, compdec_type) :: reify.cuts; let ce = mklApp cTyp_compdec [|t; compdec_var|] in diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli index 4f8d4ad..5d45ca4 100644 --- a/src/trace/smtBtype.mli +++ b/src/trace/smtBtype.mli @@ -13,11 +13,11 @@ open SmtMisc -type indexed_type = Term.constr gen_hashed +type indexed_type = Structures.constr gen_hashed val dummy_indexed_type: int -> indexed_type val indexed_type_index : indexed_type -> int -val indexed_type_hval : indexed_type -> Term.constr +val indexed_type_hval : indexed_type -> Structures.constr type btype = | TZ @@ -27,11 +27,11 @@ type btype = | TFArray of btype * btype | Tindex of indexed_type -val indexed_type_of_int : int -> Term.constr SmtMisc.gen_hashed +val indexed_type_of_int : int -> Structures.constr SmtMisc.gen_hashed val equal : btype -> btype -> bool -val to_coq : btype -> Term.constr +val to_coq : btype -> Structures.constr val to_smt : Format.formatter -> btype -> unit @@ -39,26 +39,26 @@ type reify_tbl val create : unit -> reify_tbl -val declare : reify_tbl -> Term.constr -> Term.constr -> btype +val declare : reify_tbl -> Structures.constr -> Structures.constr -> btype -val of_coq : reify_tbl -> logic -> Term.constr -> btype +val of_coq : reify_tbl -> logic -> Structures.constr -> btype -val get_coq_type_op : int -> Term.constr +val get_coq_type_op : int -> Structures.constr -val interp_tbl : reify_tbl -> Term.constr +val interp_tbl : reify_tbl -> Structures.constr val to_list : reify_tbl -> (int * indexed_type) list -val make_t_i : reify_tbl -> Term.constr +val make_t_i : reify_tbl -> Structures.constr -val dec_interp : Term.constr -> btype -> Term.constr -val ord_interp : Term.constr -> btype -> Term.constr -val comp_interp : Term.constr -> btype -> Term.constr -val inh_interp : Term.constr -> btype -> Term.constr -val interp : Term.constr -> btype -> Term.constr +val dec_interp : Structures.constr -> btype -> Structures.constr +val ord_interp : Structures.constr -> btype -> Structures.constr +val comp_interp : Structures.constr -> btype -> Structures.constr +val inh_interp : Structures.constr -> btype -> Structures.constr +val interp : Structures.constr -> btype -> Structures.constr -val interp_to_coq : reify_tbl -> btype -> Term.constr +val interp_to_coq : reify_tbl -> btype -> Structures.constr -val get_cuts : reify_tbl -> (Structures.names_id * Term.types) list +val get_cuts : reify_tbl -> (Structures.id * Structures.types) list val logic : btype -> logic diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 1a990f1..78c07b9 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -10,10 +10,6 @@ (**************************************************************************) -open Entries -open Declare -open Decl_kinds - open SmtMisc open CoqTerms open SmtForm @@ -132,19 +128,19 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, let t_i' = make_t_i rt in let ce5 = Structures.mkUConst t_i' in - let ct_i = Term.mkConst (declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition)) in + let ct_i = Structures.mkConst (Structures.declare_constant t_i ce5) in let t_func' = make_t_func ro ct_i in let ce6 = Structures.mkUConst t_func' in - let ct_func = Term.mkConst (declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition)) in + let ct_func = Structures.mkConst (Structures.declare_constant t_func ce6) in let t_atom' = Atom.interp_tbl ra in let ce1 = Structures.mkUConst t_atom' in - let ct_atom = Term.mkConst (declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition)) in + let ct_atom = Structures.mkConst (Structures.declare_constant t_atom ce1) in let t_form' = snd (Form.interp_tbl rf) in let ce2 = Structures.mkUConst t_form' in - let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in + let ct_form = Structures.mkConst (Structures.declare_constant t_form ce2) in (* EMPTY LEMMA LIST *) let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) @@ -167,14 +163,14 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in let ce3 = Structures.mkUConst roots in - let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in + let _ = Structures.declare_constant root ce3 in let ce3' = Structures.mkUConst used_roots in - let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in + let _ = Structures.declare_constant used_root ce3' in let certif = mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let ce4 = Structures.mkUConst certif in - let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in + let _ = Structures.declare_constant trace ce4 in () @@ -188,15 +184,15 @@ let interp_roots t_i roots = | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots let theorem name (rt, ro, ra, rf, roots, max_id, confl) = - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in - let nused_roots = mkName "used_roots" in - let nd = mkName "d" in + let nti = Structures.mkName "t_i" in + let ntfunc = Structures.mkName "t_func" in + let ntatom = Structures.mkName "t_atom" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in + let nused_roots = Structures.mkName "used_roots" in + let nd = Structures.mkName "d" in - let v = Term.mkRel in + let v = Structures.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -230,50 +226,50 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) = let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in let theorem_proof_cast = - Term.mkCast ( - Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + Structures.mkCast ( + Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_correct [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*); vm_cast_true_no_check (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))), - Term.VMcast, + Structures.vmcast, theorem_concl) in let theorem_proof_nocast = - Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_correct [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in - let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in + let _ = Structures.declare_constant name ce in () (* Given an SMT-LIB2 file and a certif, call the checker *) let checker (rt, ro, ra, rf, roots, max_id, confl) = - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in - let nused_roots = mkName "used_roots" in - let nd = mkName "d" in + let nti = Structures.mkName "t_i" in + let ntfunc = Structures.mkName "t_func" in + let ntatom = Structures.mkName "t_atom" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in + let nused_roots = Structures.mkName "used_roots" in + let nd = Structures.mkName "d" in - let v = Term.mkRel in + let v = Structures.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -306,18 +302,18 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) = Structures.mkArray (Lazy.force cint, res) in let tm = - Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Term.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], + Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], + Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], + Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in Format.eprintf " = %s\n : bool@." - (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then + (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then "true" else "false") let count_used confl = @@ -333,15 +329,15 @@ let count_used confl = let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in - let nused_roots = mkName "used_roots" in - let nd = mkName "d" in + let nti = Structures.mkName "t_i" in + let ntfunc = Structures.mkName "t_func" in + let ntatom = Structures.mkName "t_atom" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in + let nused_roots = Structures.mkName "used_roots" in + let nd = Structures.mkName "d" in - let v = Term.mkRel in + let v = Structures.mkRel in let t_i = make_t_i rt in let t_func = make_t_func ro (v 1 (*t_i*)) in @@ -376,16 +372,16 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = Structures.mkArray (Lazy.force cint, res) in let tm = - Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Term.mkLetIn (ntfunc, t_func, + Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|], - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); + Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], - Term.mkLetIn (nused_roots, used_rootsCstr, + Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], - Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], + Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|], mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in @@ -394,54 +390,54 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = [|mklApp cprod [|Lazy.force cnat; Lazy.force cname_step|]|]) in - match Term.decompose_app res with - | c, _ when Term.eq_constr c (Lazy.force cNone) -> + match Structures.decompose_app res with + | c, _ when Structures.eq_constr c (Lazy.force cNone) -> Structures.error ("Debug checker is only meant to be used for certificates \ that fail to be checked by SMTCoq.") - | c, [_; n] when Term.eq_constr c (Lazy.force cSome) -> - (match Term.decompose_app n with - | c, [_; _; cnb; cn] when Term.eq_constr c (Lazy.force cpair) -> - let n = fst (Term.decompose_app cn) in + | c, [_; n] when Structures.eq_constr c (Lazy.force cSome) -> + (match Structures.decompose_app n with + | c, [_; _; cnb; cn] when Structures.eq_constr c (Lazy.force cpair) -> + let n = fst (Structures.decompose_app cn) in let name = - if Term.eq_constr n (Lazy.force cName_Res ) then "Res" - else if Term.eq_constr n (Lazy.force cName_Weaken) then "Weaken" - else if Term.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten" - else if Term.eq_constr n (Lazy.force cName_CTrue) then "CTrue" - else if Term.eq_constr n (Lazy.force cName_CFalse ) then "CFalse" - else if Term.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef" - else if Term.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2" - else if Term.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj" - else if Term.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef" - else if Term.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2" - else if Term.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj" - else if Term.eq_constr n (Lazy.force cName_EqTr ) then "EqTr" - else if Term.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr" - else if Term.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP" - else if Term.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega" - else if Term.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq" - else if Term.eq_constr n (Lazy.force cName_SplArith) then "SplArith" - else if Term.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim" - else if Term.eq_constr n (Lazy.force cName_BBVar) then "BBVar" - else if Term.eq_constr n (Lazy.force cName_BBConst) then "BBConst" - else if Term.eq_constr n (Lazy.force cName_BBOp) then "BBOp" - else if Term.eq_constr n (Lazy.force cName_BBNot) then "BBNot" - else if Term.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg" - else if Term.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd" - else if Term.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat" - else if Term.eq_constr n (Lazy.force cName_BBMul) then "BBMul" - else if Term.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt" - else if Term.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt" - else if Term.eq_constr n (Lazy.force cName_BBEq) then "BBEq" - else if Term.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq" - else if Term.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract" - else if Term.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend" - else if Term.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend" - else if Term.eq_constr n (Lazy.force cName_BBShl) then "BBShl" - else if Term.eq_constr n (Lazy.force cName_BBShr) then "BBShr" - else if Term.eq_constr n (Lazy.force cName_RowEq) then "RowEq" - else if Term.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq" - else if Term.eq_constr n (Lazy.force cName_Ext) then "Ext" - else if Term.eq_constr n (Lazy.force cName_Hole) then "Hole" + if Structures.eq_constr n (Lazy.force cName_Res ) then "Res" + else if Structures.eq_constr n (Lazy.force cName_Weaken) then "Weaken" + else if Structures.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten" + else if Structures.eq_constr n (Lazy.force cName_CTrue) then "CTrue" + else if Structures.eq_constr n (Lazy.force cName_CFalse ) then "CFalse" + else if Structures.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef" + else if Structures.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2" + else if Structures.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj" + else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef" + else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2" + else if Structures.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj" + else if Structures.eq_constr n (Lazy.force cName_EqTr ) then "EqTr" + else if Structures.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr" + else if Structures.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP" + else if Structures.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega" + else if Structures.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq" + else if Structures.eq_constr n (Lazy.force cName_SplArith) then "SplArith" + else if Structures.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim" + else if Structures.eq_constr n (Lazy.force cName_BBVar) then "BBVar" + else if Structures.eq_constr n (Lazy.force cName_BBConst) then "BBConst" + else if Structures.eq_constr n (Lazy.force cName_BBOp) then "BBOp" + else if Structures.eq_constr n (Lazy.force cName_BBNot) then "BBNot" + else if Structures.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg" + else if Structures.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd" + else if Structures.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat" + else if Structures.eq_constr n (Lazy.force cName_BBMul) then "BBMul" + else if Structures.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt" + else if Structures.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt" + else if Structures.eq_constr n (Lazy.force cName_BBEq) then "BBEq" + else if Structures.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq" + else if Structures.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract" + else if Structures.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend" + else if Structures.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend" + else if Structures.eq_constr n (Lazy.force cName_BBShl) then "BBShl" + else if Structures.eq_constr n (Lazy.force cName_BBShr) then "BBShr" + else if Structures.eq_constr n (Lazy.force cName_RowEq) then "RowEq" + else if Structures.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq" + else if Structures.eq_constr n (Lazy.force cName_Ext) then "Ext" + else if Structures.eq_constr n (Lazy.force cName_Hole) then "Hole" else string_coq_constr n in let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in @@ -454,9 +450,9 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (* let rec of_coq_list cl = - * match Term.decompose_app cl with - * | c, _ when Term.eq_constr c (Lazy.force cnil) -> [] - * | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) -> + * match Structures.decompose_app cl with + * | c, _ when Structures.eq_constr c (Lazy.force cnil) -> [] + * | c, [_; x; cr] when Structures.eq_constr c (Lazy.force ccons) -> * x :: of_coq_list cr * | _ -> assert false *) @@ -466,26 +462,22 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * * let t_i' = make_t_i rt in * let ce5 = Structures.mkUConst t_i' in - * let ct_i = Term.mkConst (declare_constant t_i - * (DefinitionEntry ce5, IsDefinition Definition)) in + * let ct_i = Structures.mkConst (Structures.declare_constant t_i ce5) in * * let t_func' = make_t_func ro ct_i in * let ce6 = Structures.mkUConst t_func' in * let ct_func = - * Term.mkConst (declare_constant t_func - * (DefinitionEntry ce6, IsDefinition Definition)) in + * Structures.mkConst (Structures.declare_constant t_func ce6) in * * let t_atom' = Atom.interp_tbl ra in * let ce1 = Structures.mkUConst t_atom' in * let ct_atom = - * Term.mkConst (declare_constant t_atom - * (DefinitionEntry ce1, IsDefinition Definition)) in + * Structures.mkConst (Structures.declare_constant t_atom ce1) in * * let t_form' = snd (Form.interp_tbl rf) in * let ce2 = Structures.mkUConst t_form' in * let ct_form = - * Term.mkConst (declare_constant t_form - * (DefinitionEntry ce2, IsDefinition Definition)) in + * Structures.mkConst (Structures.declare_constant t_form ce2) in * * let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) * (interp_conseq_uf ct_i) @@ -509,18 +501,15 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * mklApp cSome [|mklApp carray [|Lazy.force cint|]; * Structures.mkArray (Lazy.force cint, res)|] in * let ce3 = Structures.mkUConst croots in - * let _ = declare_constant root - * (DefinitionEntry ce3, IsDefinition Definition) in + * let _ = Structures.declare_constant root ce3 in * let ce3' = Structures.mkUConst cused_roots in - * let _ = declare_constant used_root - * (DefinitionEntry ce3', IsDefinition Definition) in + * let _ = Structures.declare_constant used_root ce3' in * * let certif = * mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); * tres;mkInt (get_pos confl)|] in * let ce4 = Structures.mkUConst certif in - * let _ = declare_constant trace - * (DefinitionEntry ce4, IsDefinition Definition) in + * let _ = Structures.declare_constant trace ce4 in * * let setup = * mklApp csetup_checker_step_debug @@ -532,8 +521,8 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * mklApp clist [|mklApp cstep * [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in * - * let s, steps = match Term.decompose_app setup with - * | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) -> + * let s, steps = match Structures.decompose_app setup with + * | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) -> * s, of_coq_list csteps * | _ -> assert false * in @@ -550,12 +539,12 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = * Structures.cbv_vm (Global.env ()) tm * (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in * - * match Term.decompose_app res with - * | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) -> + * match Structures.decompose_app res with + * | c, [_; _; s; cbad] when Structures.eq_constr c (Lazy.force cpair) -> * if not (mk_bool cbad) then s * else Structures.error ("Step number " ^ string_of_int !cpt ^ * " (" ^ string_coq_constr - * (fst (Term.decompose_app step)) ^ ")" ^ + * (fst (Structures.decompose_app step)) ^ ")" ^ * " of the certificate likely failed." ) * | _ -> assert false * in @@ -570,13 +559,13 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) = (* Tactic *) let build_body rt ro ra rf l b (max_id, confl) vm_cast find = - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in + let nti = Structures.mkName "t_i" in + let ntfunc = Structures.mkName "t_func" in + let ntatom = Structures.mkName "t_atom" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in - let v = Term.mkRel in + let v = Structures.mkRel in let t_i = make_t_i rt in let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in @@ -594,11 +583,11 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find = mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let add_lets t = - Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, mklApp ccertif + Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], + Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], t))))) in @@ -625,13 +614,13 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find = let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = - let nti = mkName "t_i" in - let ntfunc = mkName "t_func" in - let ntatom = mkName "t_atom" in - let ntform = mkName "t_form" in - let nc = mkName "c" in + let nti = Structures.mkName "t_i" in + let ntfunc = Structures.mkName "t_func" in + let ntatom = Structures.mkName "t_atom" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in - let v = Term.mkRel in + let v = Structures.mkRel in let t_i = make_t_i rt in let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in @@ -644,11 +633,11 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let add_lets t = - Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], - Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], - Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], - Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, mklApp ccertif + Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|], + Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|], + Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], + Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|], t))))) in @@ -676,10 +665,10 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find = let get_arguments concl = - let f, args = Term.decompose_app concl in + let f, args = Structures.decompose_app concl in match args with - | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b - | [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue + | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b + | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue | _ -> failwith ("Verit.tactic: can only deal with equality over bool") @@ -699,18 +688,18 @@ let of_coq_lemma rt ro ra' rf' env sigma solver_logic clemma = let env_lemma = List.fold_right Environ.push_rel rel_context env in let forall_args = let fmap r = let n, t = Structures.destruct_rel_decl r in - string_of_name n, SmtBtype.of_coq rt solver_logic t in + Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in List.map fmap rel_context in - let f, args = Term.decompose_app qf_lemma in + let f, args = Structures.decompose_app qf_lemma in let core_f = - if Term.eq_constr f (Lazy.force cis_true) then + if Structures.eq_constr f (Lazy.force cis_true) then match args with | [a] -> a | _ -> raise Axiom_form_unsupported - else if Term.eq_constr f (Lazy.force ceq) then + else if Structures.eq_constr f (Lazy.force ceq) then match args with - | [ty; arg1; arg2] when Term.eq_constr ty (Lazy.force cbool) && - Term.eq_constr arg2 (Lazy.force ctrue) -> + | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) && + Structures.eq_constr arg2 (Lazy.force ctrue) -> arg1 | _ -> raise Axiom_form_unsupported else raise Axiom_form_unsupported in @@ -730,7 +719,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl let lsmt = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in - let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t = + let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t = Hashtbl.create 100 in let new_ref ((l, pl), ls) = Hashtbl.add lem_tbl (Form.index ls) (l, pl) in @@ -752,10 +741,10 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl | _ -> failwith "unexpected form of root" in let (body_cast, body_nocast, cuts) = - if ((Term.eq_constr b (Lazy.force ctrue)) || - (Term.eq_constr b (Lazy.force cfalse))) then + if ((Structures.eq_constr b (Lazy.force ctrue)) || + (Structures.eq_constr b (Lazy.force cfalse))) then let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in - let nl = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in + let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in let _ = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in let lsmt = Form.flatten rf nl :: lsmt in let max_id_confl = make_proof call_solver env rt ro ra' rf' nl lsmt in @@ -776,7 +765,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl List.fold_right (fun (eqn, eqt) tac -> Structures.tclTHENLAST - (Structures.assert_before (Names.Name eqn) eqt) + (Structures.assert_before (Structures.name_of_id eqn) eqt) tac ) cuts (Structures.tclTHEN @@ -804,7 +793,7 @@ let string_index_of_constr env i cf = try let s = string_coq_constr cf in let nc = Environ.named_context env in - let nd = Environ.lookup_named (Names.id_of_string s) env in + let nd = Environ.lookup_named (Structures.mkId s) env in let cpt = ref 0 in (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc with Exit -> ()); @@ -814,14 +803,13 @@ let string_index_of_constr env i cf = let vstring_i env i = let cf = SmtAtom.Atom.get_coq_term_op i in - if Term.isRel cf then - let dbi = Term.destRel cf in + if Structures.isRel cf then + let dbi = Structures.destRel cf in let s = Environ.lookup_rel dbi env |> Structures.get_rel_dec_name - |> function - | Names.Name id -> Names.string_of_id id - | Names.Anonymous -> "?" in + |> SmtMisc.string_of_name_def "?" + in s, dbi else string_index_of_constr env i cf diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli index d7b6ae6..9a1b681 100644 --- a/src/trace/smtCommands.mli +++ b/src/trace/smtCommands.mli @@ -11,13 +11,13 @@ val parse_certif : - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> + Structures.id -> + Structures.id -> + Structures.id -> + Structures.id -> + Structures.id -> + Structures.id -> + Structures.id -> SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> @@ -29,7 +29,7 @@ val checker_debug : SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a val theorem : - Structures.names_id -> + Structures.id -> SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify * SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> @@ -56,8 +56,8 @@ val tactic : SmtAtom.Form.reify -> SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> - (Environ.env -> Term.constr -> Term.constr) -> - Term.constr list -> + (Environ.env -> Structures.constr -> Structures.constr) -> + Structures.constr list -> Structures.constr_expr list -> Structures.tactic val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index ad6a5a4..20b99ac 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -82,7 +82,7 @@ module type FORM = val get : ?declare:bool -> reify -> pform -> t (** Give a coq term, build the corresponding formula *) - val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t (** Flattening of [Fand] and [For], removing of [Fnot2] *) @@ -94,20 +94,20 @@ module type FORM = (** Producing Coq terms *) - val to_coq : t -> Term.constr + val to_coq : t -> Structures.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Term.constr * Term.constr + val interp_tbl : reify -> Structures.constr * Structures.constr val nvars : reify -> int (** Producing a Coq term corresponding to the interpretation of a formula *) (** [interp_atom] map [hatom] to coq term, it is better if it produce shared terms. *) val interp_to_coq : - (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> - t -> Term.constr + (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> + t -> Structures.constr end module Make (Atom:ATOM) = @@ -361,9 +361,9 @@ module Make (Atom:ATOM) = | CCunknown module ConstrHash = struct - type t = Term.constr - let equal = Term.eq_constr - let hash = Term.hash_constr + type t = Structures.constr + let equal = Structures.eq_constr + let hash = Structures.hash_constr end module ConstrHashtbl = Hashtbl.Make(ConstrHash) @@ -386,7 +386,7 @@ module Make (Atom:ATOM) = let get_cst c = try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in let rec mk_hform h = - let c, args = Term.decompose_app h in + let c, args = Structures.decompose_app h in match get_cst c with | CCtrue -> get reify (Fapp(Ftrue,empty_args)) | CCfalse -> get reify (Fapp(Ffalse,empty_args)) @@ -427,8 +427,8 @@ module Make (Atom:ATOM) = and mk_fnot i args = match args with | [t] -> - let c,args = Term.decompose_app t in - if Term.eq_constr c (Lazy.force cnegb) then + let c,args = Structures.decompose_app t in + if Structures.eq_constr c (Lazy.force cnegb) then mk_fnot (i+1) args else let q,r = i lsr 1 , i land 1 in @@ -442,8 +442,8 @@ module Make (Atom:ATOM) = match args with | [t1;t2] -> let l2 = mk_hform t2 in - let c, args = Term.decompose_app t1 in - if Term.eq_constr c (Lazy.force candb) then + let c, args = Structures.decompose_app t1 in + if Structures.eq_constr c (Lazy.force candb) then mk_fand (l2::acc) args else let l1 = mk_hform t1 in @@ -454,8 +454,8 @@ module Make (Atom:ATOM) = match args with | [t1;t2] -> let l2 = mk_hform t2 in - let c, args = Term.decompose_app t1 in - if Term.eq_constr c (Lazy.force corb) then + let c, args = Structures.decompose_app t1 in + if Structures.eq_constr c (Lazy.force corb) then mk_for (l2::acc) args else let l1 = mk_hform t1 in diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index c26e279..ba8c066 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -12,10 +12,10 @@ open SmtMisc -module type ATOM = - sig +module type ATOM = + sig - type t + type t val index : t -> int val equal : t -> t -> bool @@ -25,7 +25,7 @@ module type ATOM = val to_smt : Format.formatter -> t -> unit val logic : t -> logic - end + end type fop = @@ -38,16 +38,16 @@ type fop = | Fiff | Fite | Fnot2 of int - | Fforall of (string * SmtBtype.btype) list - -type ('a,'f) gen_pform = + | Fforall of (string * SmtBtype.btype) list + +type ('a,'f) gen_pform = | Fatom of 'a | Fapp of fop * 'f array | FbbT of 'a * 'f list module type FORM = - sig - type hatom + sig + type hatom type t type pform = (hatom, t) gen_pform @@ -72,16 +72,16 @@ module type FORM = (* Building formula from positive formula *) exception NotWellTyped of pform - type reify + type reify val create : unit -> reify val clear : reify -> unit val get : ?declare:bool -> reify -> pform -> t - - (** Given a coq term, build the corresponding formula *) - val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t + + (** Given a coq term, build the corresponding formula *) + val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t - + (** Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t @@ -89,24 +89,22 @@ module type FORM = counter-parts *) val right_assoc : reify -> t -> t - (** Producing Coq terms *) + (** Producing Coq terms *) - val to_coq : t -> Term.constr + val to_coq : t -> Structures.constr val pform_tbl : reify -> pform array val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array - val interp_tbl : reify -> Term.constr * Term.constr - val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation + val interp_tbl : reify -> Structures.constr * Structures.constr + val nvars : reify -> int + (** Producing a Coq term corresponding to the interpretation of a formula *) (** [interp_atom] map [hatom] to coq term, it is better if it produce shared terms. *) - val interp_to_coq : - (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> - t -> Term.constr + val interp_to_coq : + (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> + t -> Structures.constr end module Make (Atom:ATOM) : FORM with type hatom = Atom.t - - diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index f839869..92f0f09 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -25,16 +25,9 @@ type 'a gen_hashed = { index : int; hval : 'a } (** Functions over constr *) -let mklApp f args = Term.mkApp (Lazy.force f, args) - -(* TODO : Set -> Type *) -let declare_new_type = Structures.declare_new_type -let declare_new_variable = Structures.declare_new_variable - -let mkName s = - let id = Names.id_of_string s in - Names.Name id +let mklApp f args = Structures.mkApp (Lazy.force f, args) +let string_of_name_def d n = try Structures.string_of_name n with | _ -> d let string_coq_constr t = let rec fix rf x = rf (fix rf) x in @@ -43,11 +36,6 @@ let string_coq_constr t = Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t)) -let string_of_name = function - Names.Name id -> Names.string_of_id id - | _ -> failwith "unnamed rel" - - (** Logics *) type logic_item = diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli index a9de935..f3bcf60 100644 --- a/src/trace/smtMisc.mli +++ b/src/trace/smtMisc.mli @@ -10,15 +10,12 @@ (**************************************************************************) -val cInt_tbl : (int, Term.constr) Hashtbl.t -val mkInt : int -> Term.constr +val cInt_tbl : (int, Structures.constr) Hashtbl.t +val mkInt : int -> Structures.constr type 'a gen_hashed = { index : int; hval : 'a; } -val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr -val declare_new_type : Names.variable -> Term.constr -val declare_new_variable : Names.variable -> Term.types -> Term.constr -val mkName : string -> Names.name -val string_coq_constr : Term.constr -> string -val string_of_name : Names.name -> string +val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr +val string_of_name_def : string -> Structures.name -> string +val string_coq_constr : Structures.constr -> string type logic_item = LUF | LLia | LBitvectors | LArrays module SL : Set.S with type elt = logic_item type logic = SL.t diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml index a9855a2..5d9d82d 100644 --- a/src/trace/smtTrace.ml +++ b/src/trace/smtTrace.ml @@ -458,10 +458,10 @@ let to_coq to_lit interp (cstep, | Ext (res) -> mklApp cExt [|out_c c; out_f res|] | Hole (prem_id, concl) -> let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in - let ass_name = Names.id_of_string ("ass"^(string_of_int (Hashtbl.hash concl))) in + let ass_name = Structures.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in let ass_ty = interp (prem, concl) in cuts := (ass_name, ass_ty)::!cuts; - let ass_var = Term.mkVar ass_name in + let ass_var = Structures.mkVar ass_name in let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in let concl' = out_cl concl in @@ -471,8 +471,8 @@ let to_coq to_lit interp (cstep, | Some find -> find cl | None -> assert false in let concl' = out_cl [concl] in - let app_name = Names.id_of_string ("app" ^ (string_of_int (Hashtbl.hash concl))) in - let app_var = Term.mkVar app_name in + let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in + let app_var = Structures.mkVar app_name in let app_ty = Term.mkArrow clemma (interp ([], [concl])) in cuts := (app_name, app_ty)::!cuts; mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|] diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli index f06ade4..5ded32a 100644 --- a/src/trace/smtTrace.mli +++ b/src/trace/smtTrace.mli @@ -47,26 +47,26 @@ val alloc : 'a SmtCertif.clause -> int val naive_alloc : 'a SmtCertif.clause -> int val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int val to_coq : - ('a -> Term.constr) -> - ('a list list * 'a list -> Term.types) -> - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t * - Term.constr Lazy.t * Term.constr Lazy.t -> + ('a -> Structures.constr) -> + ('a list list * 'a list -> Structures.types) -> + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t * + Structures.constr Lazy.t * Structures.constr Lazy.t -> 'a SmtCertif.clause -> - ('a SmtCertif.clause -> Term.types * Term.constr) option -> - Term.constr * 'a SmtCertif.clause * - (Names.identifier * Term.types) list + ('a SmtCertif.clause -> Structures.types * Structures.constr) option -> + Structures.constr * 'a SmtCertif.clause * + (Structures.id * Structures.types) list module MakeOpt : functor (Form : SmtForm.FORM) -> sig diff --git a/src/verit/verit.mli b/src/verit/verit.mli index 468aa1e..6fa62d8 100644 --- a/src/verit/verit.mli +++ b/src/verit/verit.mli @@ -11,13 +11,13 @@ val parse_certif : - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> - Structures.names_id -> Structures.names_id -> Structures.names_id -> string -> string -> unit + Structures.id -> + Structures.id -> + Structures.id -> + Structures.id -> + Structures.id -> Structures.id -> Structures.id -> string -> string -> unit val checker : string -> string -> unit val checker_debug : string -> string -> unit -val theorem : Structures.names_id -> string -> string -> unit -val tactic : Term.constr list -> Structures.constr_expr list -> Structures.tactic -val tactic_no_check : Term.constr list -> Structures.constr_expr list -> Structures.tactic +val theorem : Structures.id -> string -> string -> unit +val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic +val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index dbf3d62..13beb9d 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -14,9 +14,80 @@ open Entries open Coqlib +(* Constr generation and manipulation *) +type id = Names.id +let mkId = Names.id_of_string + + +type name = Names.name +let name_of_id i = Names.Name i +let mkName s = + let id = mkId s in + name_of_id id +let string_of_name = function + Names.Name id -> Names.string_of_id id + | _ -> failwith "unnamed rel" + + +type constr = Term.constr +type types = Term.types +let eq_constr = Term.eq_constr +let hash_constr = Term.hash_constr +let mkProp = Term.mkProp +let mkConst = Constr.mkConst +let mkVar = Term.mkVar +let mkRel = Term.mkRel +let isRel = Term.isRel +let destRel = Term.destRel +let lift = Term.lift +let mkApp = Term.mkApp +let decompose_app = Term.decompose_app +let mkLambda = Term.mkLambda +let mkProd = Term.mkProd +let mkLetIn = Term.mkLetIn + +let pr_constr_env = Printer.pr_constr_env +let pr_constr = Printer.pr_constr + +let mkUConst c = + { const_entry_body = c; + const_entry_type = None; + const_entry_secctx = None; + const_entry_opaque = false; + const_entry_inline_code = false} + +let mkTConst c _ ty = + { const_entry_body = c; + const_entry_type = Some ty; + const_entry_secctx = None; + const_entry_opaque = false; + const_entry_inline_code = false} + +(* TODO : Set -> Type *) +let declare_new_type t = + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force Term.mkSet) [] false None (dummy_loc, t); + Term.mkVar t + +let declare_new_variable v constr_t = + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v); + Term.mkVar v + +let declare_constant n c = + Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition) -let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) +type cast_kind = Term.cast_kind +let vmcast = Term.VMcast +let mkCast = Term.mkCast + + +(* EConstr *) +type econstr = Term.constr +let econstr_of_constr e = e + + +(* Modules *) +let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) (* Int63 *) @@ -64,58 +135,24 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r = mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace) -(* Differences between the two versions of Coq *) -type names_id_t = Names.identifier - -let dummy_loc = Pp.dummy_loc - -let mkUConst c = - { const_entry_body = c; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} - -let mkTConst c _ ty = - { const_entry_body = c; - const_entry_type = Some ty; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} - -let error = Errors.error - -let coqtype = lazy Term.mkSet - -let declare_new_type t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (dummy_loc, t); - Term.mkVar t - -let declare_new_variable v constr_t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v); - Term.mkVar v - -let extern_constr = Constrextern.extern_constr true Environ.empty_env - -let vernacentries_interp expr = - Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some (Glob_term.CbvVm None), None, expr)) - -let pr_constr_env = Printer.pr_constr_env +(* Micromega *) +module Micromega_plugin_Certificate = Certificate +module Micromega_plugin_Coq_micromega = Coq_micromega +module Micromega_plugin_Micromega = Micromega +module Micromega_plugin_Mutils = Mutils -let lift = Term.lift +let micromega_coq_proofTerm = + Coq_micromega.M.coq_proofTerm -let destruct_rel_decl (n, _, t) = n, t +let micromega_dump_proof_term p = + Coq_micromega.dump_proof_term p -let interp_constr env sigma = Constrintern.interp_constr sigma env +(* Tactics *) let tclTHEN = Tacticals.tclTHEN let tclTHENLAST = Tacticals.tclTHENLAST let assert_before = Tactics.assert_tac - -let vm_conv = Reduction.vm_conv let vm_cast_no_check = Tactics.vm_cast_no_check -let cbv_vm = Vnorm.cbv_vm - let mk_tactic tac gl = let env = Tacmach.pf_env gl in let sigma = Tacmach.project gl in @@ -123,6 +160,12 @@ let mk_tactic tac gl = tac env sigma t gl let set_evars_tac _ = Tacticals.tclIDTAC + +(* Other differences between the two versions of Coq *) +let error = Errors.error +let extern_constr = Constrextern.extern_constr true Environ.empty_env +let destruct_rel_decl (n, _, t) = n, t +let interp_constr env sigma = Constrintern.interp_constr sigma env let ppconstr_lsimpleconstr = Ppconstr.lsimple let constrextern_extern_constr = let env = Global.env () in @@ -133,25 +176,7 @@ let get_rel_dec_name = fun _ -> Names.Anonymous (* Eta-expanded to get rid of optional arguments *) let retyping_get_type_of env = Retyping.get_type_of env +let vm_conv = Reduction.vm_conv +let cbv_vm = Vnorm.cbv_vm -(* Micromega *) -module Micromega_plugin_Certificate = Certificate -module Micromega_plugin_Coq_micromega = Coq_micromega -module Micromega_plugin_Micromega = Micromega -module Micromega_plugin_Mutils = Mutils - -let micromega_coq_proofTerm = - Coq_micromega.M.coq_proofTerm - -let micromega_dump_proof_term p = - Coq_micromega.dump_proof_term p - - -(* Types in the Coq source code *) -type tactic = Proof_type.tactic -type names_id = Names.identifier -type constr_expr = Topconstr.constr_expr -(* EConstr *) -type econstr = Term.constr -let econstr_of_constr e = e diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index 9ec21d2..abedc17 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -10,49 +10,74 @@ (**************************************************************************) -val gen_constant : string list list -> string -> Term.constr lazy_t +(* Constr generation and manipulation *) +type id +val mkId : string -> id + +type name +val name_of_id : id -> name +val mkName : string -> name +val string_of_name : name -> string + +type constr = Term.constr +type types = constr +val eq_constr : constr -> constr -> bool +val hash_constr : constr -> int +val mkProp : types +val mkConst : Names.Constant.t -> constr +val mkVar : id -> constr +val mkRel : int -> constr +val isRel : constr -> bool +val destRel : constr -> int +val lift : int -> constr -> constr +val mkApp : constr -> constr array -> constr +val decompose_app : constr -> constr * constr list +val mkLambda : name * types * constr -> constr +val mkProd : name * types * types -> types +val mkLetIn : name * constr * types * constr -> constr + +val pr_constr_env : Environ.env -> constr -> Pp.t +val pr_constr : constr -> Pp.t + +val mkUConst : constr -> Entries.definition_entry +val mkTConst : constr -> 'a -> types -> Entries.definition_entry +val declare_new_type : id -> types +val declare_new_variable : id -> types -> constr +val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t + +type cast_kind +val vmcast : cast_kind +val mkCast : constr * cast_kind * constr -> constr + + +(* EConstr *) +type econstr = constr +val econstr_of_constr : constr -> econstr + + +(* Modules *) +val gen_constant : string list list -> string -> constr lazy_t + + +(* Int63 *) val int63_modules : string list list -val mkInt : int -> Term.constr -val cint : Term.constr lazy_t +val mkInt : int -> constr +val cint : constr lazy_t + + +(* PArray *) val parray_modules : string list list val max_array_size : int -val mkArray : Term.types * Term.constr array -> Term.constr +val mkArray : types * constr array -> constr + + +(* Traces *) val mkTrace : - ('a -> Term.constr) -> + ('a -> constr) -> ('a -> 'a) -> - Term.constr Lazy.t -> + constr Lazy.t -> 'b -> - 'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr -type names_id_t = Names.identifier -val mkUConst : Term.constr -> Entries.definition_entry -val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry -val error : string -> 'a -val coqtype : Term.types lazy_t -val declare_new_type : Names.variable -> Term.constr -val declare_new_variable : Names.variable -> Term.types -> Term.constr -val extern_constr : Term.constr -> Topconstr.constr_expr -val vernacentries_interp : Topconstr.constr_expr -> unit -val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds -val lift : int -> Term.constr -> Term.constr -val destruct_rel_decl : Term.rel_declaration -> Names.name * Term.constr -val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term.constr -val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic -val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic -val assert_before : Names.name -> Term.types -> Proof_type.tactic - -val vm_conv : Reduction.conv_pb -> Term.types Reduction.conversion_function -val vm_cast_no_check : Term.constr -> Proof_type.tactic -val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr - -val mk_tactic : - (Environ.env -> - Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) -> - Proof_type.goal Tacmach.sigma -> 'a -val set_evars_tac : 'a -> Proof_type.tactic -val ppconstr_lsimpleconstr : Ppconstr.precedence -val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr -val get_rel_dec_name : 'a -> Names.name -val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr + 'c -> 'd -> 'e -> int -> types -> constr -> 'a ref -> constr (* Micromega *) @@ -61,15 +86,33 @@ module Micromega_plugin_Coq_micromega = Coq_micromega module Micromega_plugin_Micromega = Micromega module Micromega_plugin_Mutils = Mutils -val micromega_coq_proofTerm : Term.constr lazy_t -val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr +val micromega_coq_proofTerm : constr lazy_t +val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr -(* Types in the Coq source code *) +(* Tactics *) type tactic = Proof_type.tactic -type names_id = Names.identifier +val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic +val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic +val assert_before : name -> types -> Proof_type.tactic +val vm_cast_no_check : constr -> Proof_type.tactic +val mk_tactic : + (Environ.env -> + Evd.evar_map -> types -> Proof_type.goal Tacmach.sigma -> 'a) -> + Proof_type.goal Tacmach.sigma -> 'a +val set_evars_tac : 'a -> Proof_type.tactic + + +(* Other differences between the two versions of Coq *) type constr_expr = Topconstr.constr_expr +val error : string -> 'a +val extern_constr : constr -> Topconstr.constr_expr +val destruct_rel_decl : Term.rel_declaration -> name * constr +val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr +val ppconstr_lsimpleconstr : Ppconstr.precedence +val constrextern_extern_constr : constr -> Topconstr.constr_expr +val get_rel_dec_name : 'a -> name +val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr -(* EConstr *) -type econstr = Term.constr -val econstr_of_constr : Term.constr -> econstr +val vm_conv : Reduction.conv_pb -> types Reduction.conversion_function +val cbv_vm : Environ.env -> constr -> types -> constr diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v index 9a90d39..9a79f04 100644 --- a/src/versions/standard/Int63/Int63Axioms_standard.v +++ b/src/versions/standard/Int63/Int63Axioms_standard.v @@ -300,7 +300,7 @@ Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y. Axiom diveucl_21_spec : forall a1 a2 b, let (q,r) := diveucl_21 a1 a2 b in - ([|q|],[|r|]) = Zdiv_eucl ([|a1|] * wB + [|a2|]) [|b|]. + ([|q|],[|r|]) = Z.div_eucl ([|a1|] * wB + [|a2|]) [|b|]. Axiom addmuldiv_def_spec : forall p x y, addmuldiv p x y = addmuldiv_def p x y. diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v index 9f24c54..726bffd 100644 --- a/src/versions/standard/Int63/Int63Properties_standard.v +++ b/src/versions/standard/Int63/Int63Properties_standard.v @@ -131,7 +131,7 @@ Admitted. (** translation with Z *) Require Import Ndigits. -Lemma Z_of_N_double : forall n, Z_of_N (Ndouble n) = Zdouble (Z_of_N n). +Lemma Z_of_N_double : forall n, Z_of_N (N.double n) = Z.double (Z_of_N n). Proof. destruct n;simpl;trivial. Qed. @@ -148,7 +148,7 @@ Proof. apply phi_bounded. Qed. (* rewrite inj_S;simpl;assert (W:= IHn (x >> 1)%int). *) (* rewrite Zpower_Zsucc;auto with zarith. *) (* destruct (is_even x). *) -(* rewrite Zdouble_mult;auto with zarith. *) +(* rewrite Z.double_mult;auto with zarith. *) (* rewrite Zdouble_plus_one_mult;auto with zarith. *) (* Qed. *) @@ -183,7 +183,7 @@ Proof. red in Heq;rewrite Heq;trivial. rewrite <- not_true_iff_false, ltb_spec in Heq. case_eq (x == y)%int;intros Heq1. - rewrite eqb_spec in Heq1;rewrite Heq1, Zcompare_refl;trivial. + rewrite eqb_spec in Heq1;rewrite Heq1, Z.compare_refl;trivial. rewrite <- not_true_iff_false, eqb_spec in Heq1. symmetry;change ([|x|] > [|y|]);rewrite <- to_Z_eq in Heq1;omega. Qed. @@ -331,11 +331,11 @@ Proof. intros; unfold pred; apply sub_spec. Qed. Lemma diveucl_spec : forall x y, let (q,r) := diveucl x y in - ([|q|],[|r|]) = Zdiv_eucl [|x|] [|y|]. + ([|q|],[|r|]) = Z.div_eucl [|x|] [|y|]. Proof. intros;rewrite diveucl_def_spec. unfold diveucl_def;rewrite div_spec, mod_spec. - unfold Zdiv, Zmod;destruct (Zdiv_eucl [|x|] [|y|]);trivial. + unfold Z.div, Zmod;destruct (Z.div_eucl [|x|] [|y|]);trivial. Qed. (* Sqrt *) @@ -358,26 +358,26 @@ Proof. apply Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith. intros j Hj Hrec _ k Hk; pattern k; apply natlike_ind; auto; clear k Hk. rewrite Zmult_0_r, Zplus_0_r, Zplus_0_l. - generalize (sqr_pos (Zsucc j / 2)) (quotient_by_2 (Zsucc j)); - unfold Zsucc. + generalize (sqr_pos (Z.succ j / 2)) (quotient_by_2 (Z.succ j)); + unfold Z.succ. rewrite Zpower_2, Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. auto with zarith. intros k Hk _. - replace ((Zsucc j + Zsucc k) / 2) with ((j + k)/2 + 1). + replace ((Z.succ j + Z.succ k) / 2) with ((j + k)/2 + 1). generalize (Hrec Hj k Hk) (quotient_by_2 (j + k)). - unfold Zsucc; repeat rewrite Zpower_2; + unfold Z.succ; repeat rewrite Zpower_2; repeat rewrite Zmult_plus_distr_l; repeat rewrite Zmult_plus_distr_r. repeat rewrite Zmult_1_l; repeat rewrite Zmult_1_r. auto with zarith. rewrite Zplus_comm, <- Z_div_plus_full_l; auto with zarith. - apply f_equal2 with (f := Zdiv); auto with zarith. + apply f_equal2 with (f := Z.div); auto with zarith. Qed. Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2. Proof. intros Hi Hj. assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith). - apply Zlt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij). + apply Z.lt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij). pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith. Qed. @@ -402,7 +402,7 @@ Qed. Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i. Proof. intros Hi Hj Hd; rewrite Zpower_2. - apply Zle_trans with (j * (i/j)); auto with zarith. + apply Z.le_trans with (j * (i/j)); auto with zarith. apply Z_mult_div_ge; auto with zarith. Qed. @@ -411,7 +411,7 @@ Proof. intros Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto. intros H1; contradict H; apply Zle_not_lt. assert (2 * j <= j + (i/j)); auto with zarith. - apply Zle_trans with (2 * ((j + (i/j))/2)); auto with zarith. + apply Z.le_trans with (2 * ((j + (i/j))/2)); auto with zarith. apply Z_mult_div_ge; auto with zarith. Qed. @@ -488,7 +488,7 @@ Proof. intros j3 Hj3 Hpj3. apply HHrec; auto. rewrite inj_S, Zpower_Zsucc. - apply Zle_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith. + apply Z.le_trans with (2 ^Z_of_nat n + [|j2|]); auto with zarith. apply Zle_0_nat. Qed. @@ -496,7 +496,7 @@ Lemma sqrt_spec : forall x, [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2. Proof. intros i; unfold sqrt. - rewrite compare_spec. case Zcompare_spec; rewrite to_Z_1; + rewrite compare_spec. case Z.compare_spec; rewrite to_Z_1; intros Hi; auto with zarith. repeat rewrite Zpower_2; auto with zarith. apply iter_sqrt_correct; auto with zarith; @@ -508,9 +508,9 @@ Proof. assert (W:= Z_mult_div_ge [|i|] 2);assert (W':= to_Z_bounded i);auto with zarith. intros j2 H1 H2; contradict H2; apply Zlt_not_le. fold wB;assert (W:=to_Z_bounded i). - apply Zle_lt_trans with ([|i|]); auto with zarith. + apply Z.le_lt_trans with ([|i|]); auto with zarith. assert (0 <= [|i|]/2)%Z by (apply Z_div_pos; auto with zarith). - apply Zle_trans with (2 * ([|i|]/2)); auto with zarith. + apply Z.le_trans with (2 * ([|i|]/2)); auto with zarith. apply Z_mult_div_ge; auto with zarith. case (to_Z_bounded i); repeat rewrite Zpower_2; auto with zarith. Qed. @@ -543,8 +543,8 @@ Proof. assert (([|ih|] < [|j|] + 1)%Z); auto with zarith. apply Zlt_square_simpl; auto with zarith. simpl zn2z_to_Z in H1. - repeat rewrite <-Zpower_2; apply Zle_lt_trans with (2 := H1). - apply Zle_trans with ([|ih|] * wB)%Z;try rewrite Zpower_2; auto with zarith. + repeat rewrite <-Zpower_2; apply Z.le_lt_trans with (2 := H1). + apply Z.le_trans with ([|ih|] * wB)%Z;try rewrite Zpower_2; auto with zarith. Qed. @@ -553,7 +553,7 @@ Lemma div2_phi ih il j: Proof. generalize (diveucl_21_spec ih il j). case diveucl_21; intros q r Heq. - simpl zn2z_to_Z;unfold Zdiv;rewrite <- Heq;trivial. + simpl zn2z_to_Z;unfold Z.div;rewrite <- Heq;trivial. Qed. Lemma zn2z_to_Z_pos ih il : 0 <= [||WW ih il||]. @@ -577,9 +577,9 @@ Proof. case (to_Z_bounded il); intros Hil1 _. case (to_Z_bounded j); intros _ Hj1. assert (Hp3: (0 < [||WW ih il||])). - simpl zn2z_to_Z;apply Zlt_le_trans with ([|ih|] * wB)%Z; auto with zarith. + simpl zn2z_to_Z;apply Z.lt_le_trans with ([|ih|] * wB)%Z; auto with zarith. apply Zmult_lt_0_compat; auto with zarith. - apply Zlt_le_trans with (2:= Hih); auto with zarith. + apply Z.lt_le_trans with (2:= Hih); auto with zarith. cbv zeta. case_eq (ih < j)%int;intros Heq. rewrite ltb_spec in Heq. @@ -642,11 +642,11 @@ Proof. apply sqrt_main; auto with zarith. contradict Hij; apply Zle_not_lt. assert ((1 + [|j|]) <= 2 ^ (Z_of_nat size - 1)); auto with zarith. - apply Zle_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith. + apply Z.le_trans with ((2 ^ (Z_of_nat size - 1)) ^2); auto with zarith. assert (0 <= 1 + [|j|]); auto with zarith. apply Zmult_le_compat; auto with zarith. change ((2 ^ (Z_of_nat size - 1))^2) with (2 ^ (Z_of_nat size - 2) * wB). - apply Zle_trans with ([|ih|] * wB); auto with zarith. + apply Z.le_trans with ([|ih|] * wB); auto with zarith. unfold zn2z_to_Z, wB; auto with zarith. Qed. @@ -671,7 +671,7 @@ Proof. intros j3 Hj3 Hpj3. apply HHrec; auto. rewrite inj_S, Zpower_Zsucc. - apply Zle_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith. + apply Z.le_trans with (2 ^Z_of_nat n + [|j2|])%Z; auto with zarith. apply Zle_0_nat. Qed. @@ -688,7 +688,7 @@ Lemma sqrt2_spec : forall x y, (intros s; ring). assert (Hb: 0 <= wB) by (red; intros HH; discriminate). assert (Hi2: [||WW ih il ||] < ([|max_int|] + 1) ^ 2). - apply Zle_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith. + apply Z.le_lt_trans with ((wB - 1) * wB + (wB - 1)); auto with zarith. 2: apply refl_equal. case (to_Z_bounded ih); case (to_Z_bounded il); intros H1 H2 H3 H4. unfold zn2z_to_Z; auto with zarith. @@ -719,7 +719,7 @@ Lemma sqrt2_spec : forall x y, assert ([|ih1|] * wB + 2 * [|s|] + 1 <= [|ih|] * wB); auto with zarith. case (to_Z_bounded s); intros _ Hps. case (to_Z_bounded ih1); intros Hpih1 _; auto with zarith. - apply Zle_trans with (([|ih1|] + 2) * wB); auto with zarith. + apply Z.le_trans with (([|ih1|] + 2) * wB); auto with zarith. rewrite Zmult_plus_distr_l. assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. @@ -734,7 +734,7 @@ Lemma sqrt2_spec : forall x y, apply Zlt_not_le; rewrite Zpower_2, Hihl1. unfold zn2z_to_Z. case (to_Z_bounded il); intros _ H2. - apply Zlt_le_trans with (([|ih|] + 1) * wB + 0). + apply Z.lt_le_trans with (([|ih|] + 1) * wB + 0). rewrite Zmult_plus_distr_l, Zplus_0_r; auto with zarith. case (to_Z_bounded il1); intros H3 _. apply Zplus_le_compat; auto with zarith. @@ -750,7 +750,7 @@ Lemma sqrt2_spec : forall x y, rewrite sub_spec, Zmod_small; auto; replace [|1|] with 1; auto. case (to_Z_bounded ih); intros H1 H2. split; auto with zarith. - apply Zle_trans with (wB/4 - 1); auto with zarith. + apply Z.le_trans with (wB/4 - 1); auto with zarith. case_eq (ih1 < ih - 1)%int; [idtac | rewrite <- not_true_iff_false]; rewrite ltb_spec, Hsih; intros Heq. rewrite Zpower_2, Hihl1. @@ -762,10 +762,10 @@ Lemma sqrt2_spec : forall x y, auto with zarith. rewrite <-Hil2. case (to_Z_bounded il2); intros Hpil2 _. - apply Zle_trans with ([|ih|] * wB + - wB); auto with zarith. + apply Z.le_trans with ([|ih|] * wB + - wB); auto with zarith. case (to_Z_bounded s); intros _ Hps. assert (2 * [|s|] + 1 <= 2 * wB); auto with zarith. - apply Zle_trans with ([|ih1|] * wB + 2 * wB); auto with zarith. + apply Z.le_trans with ([|ih1|] * wB + 2 * wB); auto with zarith. assert (Hi: ([|ih1|] + 3) * wB <= [|ih|] * wB); auto with zarith. rewrite Zmult_plus_distr_l in Hi; auto with zarith. unfold zn2z_to_Z; rewrite <-Hihl1, Hbin; auto. @@ -786,10 +786,10 @@ Lemma sqrt2_spec : forall x y, contradict Hs1; apply Zlt_not_le; rewrite Zpower_2, Hihl1. unfold zn2z_to_Z. case (to_Z_bounded il); intros _ Hpil1. - apply Zlt_le_trans with (([|ih|] + 1) * wB). + apply Z.lt_le_trans with (([|ih|] + 1) * wB). rewrite Zmult_plus_distr_l, Zmult_1_l; auto with zarith. case (to_Z_bounded il1); intros Hpil2 _. - apply Zle_trans with (([|ih1|]) * wB); auto with zarith. + apply Z.le_trans with (([|ih1|]) * wB); auto with zarith. contradict Hs1; apply Zlt_not_le; rewrite Zpower_2, Hihl1. unfold zn2z_to_Z; rewrite He. assert ([|il|] - [|il1|] < 0); auto with zarith. @@ -880,7 +880,7 @@ Proof. unfold wB; change (Z_of_nat size) with [|digits|]. replace ([|i|]) with (([|i|] - [|digits|]) + [|digits|])%Z; try ring. rewrite Zpower_exp, Zmult_assoc, Z_mod_mult; auto with arith. - apply Zle_ge; auto with zarith. + apply Z.le_ge; auto with zarith. case (to_Z_bounded digits); auto with zarith. Qed. @@ -905,7 +905,7 @@ Proof. case (to_Z_bounded digits); intros H1d H2d. rewrite leb_spec in H. apply Zdiv_small; split; auto. - apply Zlt_le_trans with (1 := H2x). + apply Z.lt_le_trans with (1 := H2x). unfold wB; change (Z_of_nat size) with [|digits|]. apply Zpower_le_monotone; auto with zarith. Qed. @@ -940,8 +940,8 @@ Proof. rewrite add_spec, Zmod_small; auto with zarith. apply to_Z_inj; rewrite !lsr_spec, Zdiv_Zdiv, <- Zpower_exp; auto with zarith. apply Zdiv_small; split; auto with zarith. - apply Zlt_le_trans with (1 := H2i). - apply Zle_trans with (1 := H). + apply Z.lt_le_trans with (1 := H2i). + apply Z.le_trans with (1 := H). apply Zpower2_le_lin; auto with zarith. Qed. @@ -1082,10 +1082,10 @@ Admitted. (* Too slow *) (* replace (2^[|1|]) with 2%Z; auto with zarith. *) (* apply Zdiv_lt_upper_bound; auto with zarith. *) (* generalize H2i1; rewrite inj_S. *) -(* unfold Zsucc; rewrite Zpower_exp; auto with zarith. *) +(* unfold Z.succ; rewrite Zpower_exp; auto with zarith. *) (* apply Zdiv_lt_upper_bound; auto with zarith. *) (* generalize H2i2; rewrite inj_S. *) -(* unfold Zsucc; rewrite Zpower_exp; auto with zarith. *) +(* unfold Z.succ; rewrite Zpower_exp; auto with zarith. *) (* intros i. *) (* case (Zle_or_lt [|digits|] [|i|]); intros Hi. *) (* rewrite !bit_M; auto; rewrite leb_spec; auto. *) @@ -1157,17 +1157,14 @@ Proof. rewrite Zpower_exp; auto with zarith. rewrite Zdiv_mult_cancel_r. 2: (apply Zlt0_not_eq; apply Z.pow_pos_nonneg; [apply Pos2Z.is_pos|assumption]). - 2: unfold d2; auto with zarith. rewrite (Z_div_mod_eq [|x|] (2^d1)) at 2; auto with zarith. - 2: apply Zlt_gt; apply Zpower_gt_0; unfold d1; lia. + 2: apply Z.lt_gt; apply Zpower_gt_0; unfold d1; lia. pattern d1 at 2; replace d1 with (d2 + (1+ (d - [|j|] - 1)))%Z. 2: unfold d1, d2; ring. rewrite Zpower_exp; auto with zarith. - 2: unfold d2; auto with zarith. rewrite <-Zmult_assoc, Zmult_comm. rewrite Z_div_plus_l; auto with zarith. - 2: unfold d2; auto with zarith. rewrite Zpower_exp, Zpower_1_r; auto with zarith. rewrite <-Zplus_mod_idemp_l. rewrite <-!Zmult_assoc, Zmult_comm, Z_mod_mult, Zplus_0_l; auto. @@ -1452,11 +1449,11 @@ Proof. apply Zle_antisym. apply Zdiv_le_lower_bound; auto with zarith. assert (F2: [|x|] + [|z|] < 2 * wB); auto with zarith. - generalize (Zdiv_lt_upper_bound _ _ _ (Zgt_lt _ _ F1) F2); auto with zarith. + generalize (Zdiv_lt_upper_bound _ _ _ (Z.gt_lt _ _ F1) F2); auto with zarith. apply Zle_antisym. apply Zdiv_le_lower_bound; auto with zarith. assert (F2: [|x|] + [|y|] < 2 * wB); auto with zarith. - generalize (Zdiv_lt_upper_bound _ _ _ (Zgt_lt _ _ F1) F2); auto with zarith. + generalize (Zdiv_lt_upper_bound _ _ _ (Z.gt_lt _ _ F1) F2); auto with zarith. Qed. Lemma add_cancel_r x y z : (y + x = z + x)%int -> y = z. @@ -1499,7 +1496,7 @@ Proof. apply to_Z_inj; rewrite to_Z_0; auto with zarith. apply to_Z_inj; rewrite to_Z_0; auto with zarith. intros n IH x y; rewrite inj_S. - unfold Zsucc; rewrite Zpower_exp, Zpower_1_r; auto with zarith. + unfold Z.succ; rewrite Zpower_exp, Zpower_1_r; auto with zarith. intros Hx Hy. rewrite leb_spec. rewrite (to_Z_split y) at 1; rewrite (to_Z_split (x lor y)). @@ -1536,7 +1533,7 @@ Proof. apply to_Z_inj; rewrite to_Z_0; auto with zarith. apply to_Z_inj; rewrite to_Z_0; auto with zarith. intros n IH x y; rewrite inj_S. - unfold Zsucc; rewrite Zpower_exp, Zpower_1_r; auto with zarith. + unfold Z.succ; rewrite Zpower_exp, Zpower_1_r; auto with zarith. intros Hx Hy. split. intros Hn. @@ -1634,7 +1631,7 @@ Proof. split. case (to_Z_bounded (x >> 1 + y >> 1)); auto with zarith. rewrite add_spec. - apply Zle_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith. + apply Z.le_lt_trans with (([|x >> 1|] + [|y >> 1|]) * 2); auto with zarith. case (Zmod_le_first ([|x >> 1|] + [|y >> 1|]) wB); auto with zarith. case (to_Z_bounded (x >> 1)); case (to_Z_bounded (y >> 1)); auto with zarith. generalize Hb; rewrite (to_Z_split x) at 1; rewrite (to_Z_split y) at 1. @@ -1798,22 +1795,22 @@ Qed. Lemma leb_trans : forall x y z, x <= y = true -> y <= z = true -> x <= z = true. Proof. - intros x y z;rewrite !leb_spec;apply Zle_trans. + intros x y z;rewrite !leb_spec;apply Z.le_trans. Qed. Lemma ltb_trans : forall x y z, x < y = true -> y < z = true -> x < z = true. Proof. - intros x y z;rewrite !ltb_spec;apply Zlt_trans. + intros x y z;rewrite !ltb_spec;apply Z.lt_trans. Qed. Lemma ltb_leb_trans : forall x y z, x < y = true -> y <= z = true -> x < z = true. Proof. - intros x y z;rewrite leb_spec, !ltb_spec;apply Zlt_le_trans. + intros x y z;rewrite leb_spec, !ltb_spec;apply Z.lt_le_trans. Qed. Lemma leb_ltb_trans : forall x y z, x <= y = true -> y < z = true -> x < z = true. Proof. - intros x y z;rewrite leb_spec, !ltb_spec;apply Zle_lt_trans. + intros x y z;rewrite leb_spec, !ltb_spec;apply Z.le_lt_trans. Qed. Lemma gtb_not_leb : forall n m, m < n = true -> ~(n <= m = true). @@ -1828,7 +1825,7 @@ Qed. Lemma leb_refl : forall n, n <= n = true. Proof. - intros n;rewrite leb_spec;apply Zle_refl. + intros n;rewrite leb_spec;apply Z.le_refl. Qed. Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x). @@ -2083,7 +2080,7 @@ Qed. (* assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *) (* apply Z.mod_pos_bound;auto with zarith. *) (* change (2^1)%Z with 2%Z;split;try omega. *) -(* apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). *) +(* apply Z.lt_le_trans with (2 ^ Z_of_nat (S k)). *) (* rewrite inj_S, Zpower_Zsucc;omega. *) (* unfold wB;apply Zpower_le_monotone;auto with zarith. *) (* split;auto using inj_le with zarith. *) @@ -2100,7 +2097,7 @@ Qed. (* assert (W:0 <= Zpos p mod 2 ^ Z_of_nat k < 2 ^ Z_of_nat k). *) (* apply Z.mod_pos_bound;auto with zarith. *) (* change (2^1)%Z with 2%Z;split;try omega. *) -(* apply Zlt_le_trans with (2 ^ Z_of_nat (S k)). *) +(* apply Z.lt_le_trans with (2 ^ Z_of_nat (S k)). *) (* rewrite inj_S, Zpower_Zsucc;omega. *) (* unfold wB;apply Zpower_le_monotone;auto with zarith. *) (* split;auto using inj_le with zarith. *) diff --git a/src/versions/standard/Make b/src/versions/standard/Make index 543d6f0..e275b8f 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -33,7 +33,7 @@ -I versions/standard/Int63 -I versions/standard/Array --I "$(shell $(COQBIN)coqc -where)/plugins/micromega" +# -I "$(shell $(COQBIN)coqc -where)/plugins/micromega" -extra "test" "" "cd ../unit-tests; make" -extra "ztest" "" "cd ../unit-tests; make zchaff" diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 74caf8b..f259a70 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -14,8 +14,95 @@ open Entries (* Constr generation and manipulation *) +type id = Names.variable +let mkId = Names.Id.of_string + + +type name = Names.Name.t +let name_of_id i = Names.Name i +let mkName s = + let id = mkId s in + name_of_id id +let string_of_name = function + Names.Name id -> Names.Id.to_string id + | _ -> failwith "unnamed rel" + + +type constr = Constr.t +type types = Constr.types +let eq_constr = Constr.equal +let hash_constr = Constr.hash +let mkProp = Constr.mkProp +let mkConst = Constr.mkConst +let mkVar = Constr.mkVar +let mkRel = Constr.mkRel +let isRel = Constr.isRel +let destRel = Constr.destRel +let lift = Vars.lift +let mkApp = Constr.mkApp +let decompose_app = Constr.decompose_app +let mkLambda = Constr.mkLambda +let mkProd = Constr.mkProd +let mkLetIn = Constr.mkLetIn + +let pr_constr_env env = Printer.pr_constr_env env Evd.empty +let pr_constr = pr_constr_env Environ.empty_env + + +let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c -> + let env = Global.env () in + let evd = Evd.from_env env in + let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in + { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *) + const_entry_universes = Evd.const_univ_entry ~poly:false evd; + const_entry_opaque = false; + const_entry_inline_code = false } + +let mkTConst c noc ty = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in + { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some ty; + const_entry_universes = Evd.const_univ_entry ~poly:false evd; + const_entry_opaque = false; + const_entry_inline_code = false } + +(* TODO : Set -> Type *) +let declare_new_type t = + let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make t) in + Constr.mkVar t + +let declare_new_variable v constr_t = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in + let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make v) in + Constr.mkVar v -let mklApp f args = Term.mkApp (Lazy.force f, args) +let declare_constant n c = + Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition) + + + +type cast_kind = Constr.cast_kind +let vmcast = Constr.VMcast +let mkCast = Constr.mkCast + + +(* EConstr *) +type econstr = EConstr.t +let econstr_of_constr = EConstr.of_constr + + +(* Modules *) let gen_constant_in_modules s m n = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) @@ -23,12 +110,13 @@ let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules (* Int63 *) let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]] +(* 31-bits integers are "called" 63 bits (this is sound) *) let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]] let cD0 = gen_constant int31_module "D0" let cD1 = gen_constant int31_module "D1" let cI31 = gen_constant int31_module "I31" -let mkInt : int -> Term.constr = fun i -> +let mkInt : int -> constr = fun i -> let a = Array.make 31 (Lazy.force cD0) in let j = ref i in let k = ref 30 in @@ -37,7 +125,7 @@ let mkInt : int -> Term.constr = fun i -> j := !j lsr 1; decr k done; - mklApp cI31 a + mkApp (Lazy.force cI31, a) let cint = gen_constant int31_module "int31" @@ -49,7 +137,7 @@ let cmake = gen_constant parray_modules "make" let cset = gen_constant parray_modules "set" let max_array_size : int = 4194302 -let mkArray : Term.types * Term.constr array -> Term.constr = +let mkArray : Constr.types * Constr.t array -> Constr.t = fun (ty, a) -> let l = (Array.length a) - 1 in snd (Array.fold_left (fun (i,acc) c -> @@ -57,9 +145,9 @@ let mkArray : Term.types * Term.constr array -> Term.constr = if i = l then acc else - mklApp cset [|ty; acc; mkInt i; c|] in + mkApp (Lazy.force cset, [|ty; acc; mkInt i; c|]) in (i+1,acc') - ) (0,mklApp cmake [|ty; mkInt l; a.(l)|]) a) + ) (0, mkApp (Lazy.force cmake, [|ty; mkInt l; a.(l)|])) a) (* Traces *) @@ -67,81 +155,37 @@ let mkArray : Term.types * Term.constr array -> Term.constr = let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r = let rec mkTrace s = if s = size then - mklApp cnil [|step|] + mkApp (Lazy.force cnil, [|step|]) else ( r := next !r; let st = step_to_coq !r in - mklApp ccons [|step; st; mkTrace (s+1)|] + mkApp (Lazy.force ccons, [|step; st; mkTrace (s+1)|]) ) in - mklApp cpair [|mklApp clist [|step|]; step; mkTrace 0; def_step|] - - -(* Differences between the two versions of Coq *) -let mkUConst : Term.constr -> Safe_typing.private_constants Entries.definition_entry = fun c -> - let env = Global.env () in - let evd = Evd.from_env env in - let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in - { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), - Safe_typing.empty_private_constants); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Term.constr *) - const_entry_polymorphic = false; - const_entry_universes = snd (Evd.universe_context evd); - const_entry_opaque = false; - const_entry_inline_code = false } - -let mkTConst c noc ty = - let env = Global.env () in - let evd = Evd.from_env env in - let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in - { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), - Safe_typing.empty_private_constants); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some ty; - const_entry_polymorphic = false; - const_entry_universes = snd (Evd.universe_context evd); - const_entry_opaque = false; - const_entry_inline_code = false } - -let error s = CErrors.user_err (Pp.str s) + mkApp (Lazy.force cpair, [|mkApp (Lazy.force clist, [|step|]); step; mkTrace 0; def_step|]) -let coqtype = Future.from_val Term.mkSet - -let declare_new_type t = - let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (None, t) in - Term.mkVar t -let declare_new_variable v constr_t = - let env = Global.env () in - let evd = Evd.from_env env in - let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in - let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.universe_context_set evd) [] [] false Vernacexpr.NoInline (None, v) in - Term.mkVar v - -let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) - -let vernacentries_interp expr = - Vernacentries.interp (None, Vernacexpr.VernacCheckMayEval (Some (Genredexpr.CbvVm None), None, expr)) - -let pr_constr_env env = Printer.pr_constr_env env Evd.empty +(* Micromega *) +module Micromega_plugin_Certificate = Micromega_plugin.Certificate +module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega +module Micromega_plugin_Micromega = Micromega_plugin.Micromega +module Micromega_plugin_Mutils = Micromega_plugin.Mutils -let lift = Vars.lift +let micromega_coq_proofTerm = + (* Cannot contain evars *) + lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm))) -let destruct_rel_decl r = Context.Rel.Declaration.get_name r, - Context.Rel.Declaration.get_type r +let micromega_dump_proof_term p = + (* Cannot contain evars *) + EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) -let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst +(* Tactics *) +type tactic = unit Proofview.tactic let tclTHEN = Tacticals.New.tclTHEN let tclTHENLAST = Tacticals.New.tclTHENLAST let assert_before n c = Tactics.assert_before n (EConstr.of_constr c) -let vm_conv = Vconv.vm_conv let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c) -(* Cannot contain evars since it comes from a Term.constr *) -let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t)) let mk_tactic tac = Proofview.Goal.nf_enter (fun gl -> @@ -157,7 +201,21 @@ let set_evars_tac noc = let sigma, _ = Typing.type_of env sigma (EConstr.of_constr noc) in Proofview.Unsafe.tclEVARS sigma) + +(* Other differences between the two versions of Coq *) +type constr_expr = Constrexpr.constr_expr +let error s = CErrors.user_err (Pp.str s) + +let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) + +let destruct_rel_decl r = Context.Rel.Declaration.get_name r, + Context.Rel.Declaration.get_type r + +(* Cannot contain evars since it comes from a Constr.t *) +let interp_constr env sigma t = Constrintern.interp_constr env sigma t |> fst |> EConstr.Unsafe.to_constr + let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr + let constrextern_extern_constr c = let env = Global.env () in Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) @@ -166,30 +224,10 @@ let get_rel_dec_name = function | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n let retyping_get_type_of env sigma c = - (* Cannot contain evars since it comes from a Term.constr *) + (* Cannot contain evars since it comes from a Constr.t *) EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c)) +let vm_conv = Vconv.vm_conv -(* Micromega *) -module Micromega_plugin_Certificate = Micromega_plugin.Certificate -module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega -module Micromega_plugin_Micromega = Micromega_plugin.Micromega -module Micromega_plugin_Mutils = Micromega_plugin.Mutils - -let micromega_coq_proofTerm = - (* Cannot contain evars *) - lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm))) - -let micromega_dump_proof_term p = - (* Cannot contain evars *) - EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p) - - -(* Types in the Coq source code *) -type tactic = unit Proofview.tactic -type names_id = Names.Id.t -type constr_expr = Constrexpr.constr_expr - -(* EConstr *) -type econstr = EConstr.t -let econstr_of_constr = EConstr.of_constr +(* Cannot contain evars since it comes from a Constr.t *) +let cbv_vm env c t = EConstr.Unsafe.to_constr (Vnorm.cbv_vm env Evd.empty (EConstr.of_constr c) (EConstr.of_constr t)) diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli index 3d17203..3d6f6b2 100644 --- a/src/versions/standard/structures.mli +++ b/src/versions/standard/structures.mli @@ -10,74 +10,80 @@ (**************************************************************************) -(* Constr generation and manipulation *) (* WARNING: currently, we map all the econstr into constr: we suppose that the goal does not contain existencial variables *) -val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr -val gen_constant : string list list -> string -> Term.constr lazy_t + +(* Constr generation and manipulation *) +type id = Names.variable +val mkId : string -> id + +type name +val name_of_id : id -> name +val mkName : string -> name +val string_of_name : name -> string + +type constr = Constr.t +type types = constr +val eq_constr : constr -> constr -> bool +val hash_constr : constr -> int +val mkProp : types +val mkConst : Names.Constant.t -> constr +val mkVar : id -> constr +val mkRel : int -> constr +val isRel : constr -> bool +val destRel : constr -> int +val lift : int -> constr -> constr +val mkApp : constr * constr array -> constr +val decompose_app : constr -> constr * constr list +val mkLambda : name * types * constr -> constr +val mkProd : name * types * types -> types +val mkLetIn : name * constr * types * constr -> constr + +val pr_constr_env : Environ.env -> constr -> Pp.t +val pr_constr : constr -> Pp.t + +val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry +val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry +val declare_new_type : id -> types +val declare_new_variable : id -> types -> constr +val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t + +type cast_kind +val vmcast : cast_kind +val mkCast : constr * cast_kind * constr -> constr + + +(* EConstr *) +type econstr = EConstr.t +val econstr_of_constr : constr -> econstr + + +(* Modules *) +val gen_constant : string list list -> string -> constr lazy_t + (* Int63 *) val int63_modules : string list list -val int31_module : string list list -val cD0 : Term.constr lazy_t -val cD1 : Term.constr lazy_t -val cI31 : Term.constr lazy_t -val mkInt : int -> Term.constr -val cint : Term.constr lazy_t +val mkInt : int -> constr +val cint : constr lazy_t + (* PArray *) val parray_modules : string list list -val cmake : Term.constr lazy_t -val cset : Term.constr lazy_t val max_array_size : int -val mkArray : Term.types * Term.constr array -> Term.constr +val mkArray : types * constr array -> constr + (* Traces *) val mkTrace : - ('a -> Term.constr) -> + ('a -> constr) -> ('a -> 'a) -> 'b -> - Term.constr Lazy.t -> - Term.constr Lazy.t -> - Term.constr Lazy.t -> - Term.constr Lazy.t -> - int -> Term.constr -> Term.constr -> 'a ref -> Term.constr - -(* Differences between the two versions of Coq *) -val mkUConst : - Term.constr -> Safe_typing.private_constants Entries.definition_entry -val mkTConst : - Term.constr -> - Term.constr -> - Term.types -> Safe_typing.private_constants Entries.definition_entry -val error : string -> 'a -val coqtype : Term.types Future.computation -val declare_new_type : Names.variable -> Term.constr -val declare_new_variable : Names.variable -> Term.constr -> Term.constr -val extern_constr : Term.constr -> Constrexpr.constr_expr -val vernacentries_interp : Constrexpr.constr_expr -> unit -val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds -val lift : int -> Constr.constr -> Constr.constr -val destruct_rel_decl : Context.Rel.Declaration.t -> Names.Name.t * Constr.t -val interp_constr : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr -> Term.constr -val tclTHEN : - unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -val tclTHENLAST : - unit Proofview.tactic -> unit Proofview.tactic -> unit Proofview.tactic -val assert_before : Names.Name.t -> Term.types -> unit Proofview.tactic - -val vm_conv : Reduction.conv_pb -> Term.types Reduction.kernel_conversion_function -val vm_cast_no_check : Term.constr -> unit Proofview.tactic -val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr - -val mk_tactic : - (Environ.env -> Evd.evar_map -> Term.constr -> unit Proofview.tactic) -> - unit Proofview.tactic -val set_evars_tac : Term.constr -> unit Proofview.tactic -val ppconstr_lsimpleconstr : Ppconstr.precedence -val constrextern_extern_constr : Term.constr -> Constrexpr.constr_expr -val get_rel_dec_name : Context.Rel.Declaration.t -> Names.Name.t -val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr + constr Lazy.t -> + constr Lazy.t -> + constr Lazy.t -> + constr Lazy.t -> + int -> constr -> constr -> 'a ref -> constr (* Micromega *) @@ -86,15 +92,30 @@ module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega module Micromega_plugin_Micromega = Micromega_plugin.Micromega module Micromega_plugin_Mutils = Micromega_plugin.Mutils -val micromega_coq_proofTerm : Term.constr lazy_t -val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr +val micromega_coq_proofTerm : constr lazy_t +val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr -(* Types in the Coq source code *) +(* Tactics *) type tactic = unit Proofview.tactic -type names_id = Names.Id.t +val tclTHEN : tactic -> tactic -> tactic +val tclTHENLAST : tactic -> tactic -> tactic +val assert_before : name -> types -> tactic +val vm_cast_no_check : constr -> tactic +val mk_tactic : (Environ.env -> Evd.evar_map -> constr -> tactic) -> tactic +val set_evars_tac : constr -> tactic + + +(* Other differences between the two versions of Coq *) type constr_expr = Constrexpr.constr_expr +val error : string -> 'a +val extern_constr : constr -> constr_expr +val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr +val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr +val ppconstr_lsimpleconstr : Notation_term.tolerability +val constrextern_extern_constr : constr -> constr_expr +val get_rel_dec_name : Context.Rel.Declaration.t -> name +val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr -(* EConstr *) -type econstr = EConstr.t -val econstr_of_constr : Term.constr -> econstr +val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function +val cbv_vm : Environ.env -> constr -> types -> constr diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 11989c5..71b28a8 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -10,10 +10,6 @@ (**************************************************************************) -open Entries -open Declare -open Decl_kinds - open CoqTerms open SmtForm open SmtCertif @@ -168,7 +164,7 @@ let interp_roots first last = let h = if Form.is_pos l then ph else ph lxor 1 in try Hashtbl.find tbl h with Not_found -> - let p = Term.mkApp (Term.mkRel 1, [|mkInt (x+1)|]) in + let p = Structures.mkApp (Structures.mkRel 1, [|mkInt (x+1)|]) in let np = mklApp cnegb [|p|] in Hashtbl.add tbl ph p; Hashtbl.add tbl (ph lxor 1) np; @@ -199,14 +195,14 @@ let parse_certif dimacs trace fdimacs ftrace = let _,first,last,reloc = import_cnf fdimacs in let d = make_roots first last in let ce1 = Structures.mkUConst d in - let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in + let _ = Structures.declare_constant dimacs ce1 in let max_id, confl = import_cnf_trace reloc ftrace first last in let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in let ce2 = Structures.mkUConst certif in - let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in + let _ = Structures.declare_constant trace ce2 in () let cdimacs = gen_constant sat_checker_modules "dimacs" @@ -226,36 +222,36 @@ let theorems interp name fdimacs ftrace = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in - let vtype = Term.mkProd(Names.Anonymous, Lazy.force cint, Lazy.force cbool) in + let vtype = Term.mkArrow (Lazy.force cint) (Lazy.force cbool) in let theorem_type = - Term.mkProd (mkName "v", vtype, theorem_concl) in + Structures.mkProd (Structures.mkName "v", vtype, theorem_concl) in let theorem_proof_cast = - Term.mkCast ( - Term.mkLetIn (mkName "d", d, Lazy.force cdimacs, - Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, - Term.mkLambda (mkName "v", vtype, + Structures.mkCast ( + Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs, + Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif, + Structures.mkLambda (Structures.mkName "v", vtype, mklApp ctheorem_checker - [| Term.mkRel 3(*d*); Term.mkRel 2(*c*); + [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*); vm_cast_true_no_check - (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]); - Term.mkRel 1(*v*)|]))), - Term.VMcast, + (mklApp cchecker [|Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|]); + Structures.mkRel 1(*v*)|]))), + Structures.vmcast, theorem_type) in let theorem_proof_nocast = - Term.mkLetIn (mkName "d", d, Lazy.force cdimacs, - Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, - Term.mkLambda (mkName "v", vtype, + Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs, + Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif, + Structures.mkLambda (Structures.mkName "v", vtype, mklApp ctheorem_checker - [| Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]))) + [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|]))) in let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in - let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in + let _ = Structures.declare_constant name ce in () let theorem = theorems (fun _ -> interp_roots) let theorem_abs = - theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Term.mkRel 1(*v*)|]; d|]) + theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Structures.mkRel 1(*v*)|]; d|]) let checker fdimacs ftrace = @@ -270,8 +266,11 @@ let checker fdimacs ftrace = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in let tm = mklApp cchecker [|d; certif|] in - let expr = Structures.extern_constr tm in - Structures.vernacentries_interp expr + + let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in + Format.eprintf " = %s\n : bool@." + (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then + "true" else "false") @@ -359,22 +358,22 @@ let cchecker_eq_correct = let cchecker_eq = gen_constant cnf_checker_modules "checker_eq" let build_body reify_atom reify_form l b (max_id, confl) vm_cast = - let ntvar = mkName "t_var" in - let ntform = mkName "t_form" in - let nc = mkName "c" in + let ntvar = Structures.mkName "t_var" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in let (tres,_,_) = SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in - let vtvar = Term.mkRel 3 in - let vtform = Term.mkRel 2 in - let vc = Term.mkRel 1 in + let vtvar = Structures.mkRel 3 in + let vtform = Structures.mkRel 2 in + let vc = Structures.mkRel 1 in let add_lets t = - Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], - Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, + Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, Lazy.force ccertif, t))) in let cbc = @@ -392,22 +391,22 @@ let build_body reify_atom reify_form l b (max_id, confl) vm_cast = let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast = - let ntvar = mkName "t_var" in - let ntform = mkName "t_form" in - let nc = mkName "c" in + let ntvar = Structures.mkName "t_var" in + let ntform = Structures.mkName "t_form" in + let nc = Structures.mkName "c" in let tvar = Atom.interp_tbl reify_atom in let _, tform = Form.interp_tbl reify_form in let (tres,_,_) = SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in let certif = mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in - let vtvar = Term.mkRel 3 in - let vtform = Term.mkRel 2 in - let vc = Term.mkRel 1 in + let vtvar = Structures.mkRel 3 in + let vtform = Structures.mkRel 2 in + let vc = Structures.mkRel 1 in let add_lets t = - Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], - Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, + Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + Structures.mkLetIn (nc, certif, Lazy.force ccertif, t))) in let ceqc = add_lets (mklApp cchecker_eq [|vtform;l1;l2;l;vc|]) @@ -422,10 +421,10 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast = (proof_cast, proof_nocast) let get_arguments concl = - let f, args = Term.decompose_app concl in + let f, args = Structures.decompose_app concl in match args with - | [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b - | [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue + | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b + | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue | _ -> failwith ("Zchaff.get_arguments :can only deal with equality over bool") @@ -529,9 +528,9 @@ let core_tactic vm_cast env sigma concl = let reify_atom = Atom.create () in let reify_form = Form.create () in let (body_cast, body_nocast) = - if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then + if ((Structures.eq_constr b (Lazy.force ctrue)) || (Structures.eq_constr b (Lazy.force cfalse))) then let l = Form.of_coq (Atom.get reify_atom) reify_form a in - let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in + let l' = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in let atom_tbl = Atom.atom_tbl reify_atom in let pform_tbl = Form.pform_tbl reify_form in let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli index 6314927..63cf772 100644 --- a/src/zchaff/zchaff.mli +++ b/src/zchaff/zchaff.mli @@ -11,9 +11,9 @@ val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit -val parse_certif : Structures.names_id -> Structures.names_id -> string -> string -> unit +val parse_certif : Structures.id -> Structures.id -> string -> string -> unit val checker : string -> string -> unit -val theorem : Structures.names_id -> string -> string -> unit -val theorem_abs : Structures.names_id -> string -> string -> unit +val theorem : Structures.id -> string -> string -> unit +val theorem_abs : Structures.id -> string -> string -> unit val tactic : unit -> Structures.tactic val tactic_no_check : unit -> Structures.tactic |