diff options
| -rw-r--r-- | .depend.coq | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 10 | ||||
| -rw-r--r-- | contrib/setoid_ring/InitialRing.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 50 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 66 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 29 | ||||
| -rw-r--r-- | kernel/byterun/coq_values.h | 1 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 10 | ||||
| -rw-r--r-- | kernel/typeops.mli | 5 |
9 files changed, 106 insertions, 69 deletions
diff --git a/.depend.coq b/.depend.coq index aab713c5f..2ea701f0a 100644 --- a/.depend.coq +++ b/.depend.coq @@ -361,7 +361,7 @@ contrib/rtauto/Bintree.vo: contrib/rtauto/Bintree.v theories/Lists/List.vo theor contrib/rtauto/Rtauto.vo: contrib/rtauto/Rtauto.v theories/Lists/List.vo contrib/rtauto/Bintree.vo theories/Bool/Bool.vo theories/NArith/BinPos.vo contrib/recdef/Recdef.vo: contrib/recdef/Recdef.v theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo contrib/setoid_ring/BinList.vo: contrib/setoid_ring/BinList.v theories/NArith/BinPos.vo theories/Lists/List.vo theories/Lists/ListTactics.vo -contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/Setoids/Setoid.vo +contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index 9852ddf21..17d05c9c3 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -88,9 +88,9 @@ Let eq_refl := Setoid.Seq_refl _ _ Rsth. Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) . Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe) (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext. -Hint Resolve (ARadd_0_l ARth) (ARadd_sym ARth) (ARadd_assoc ARth) +Hint Resolve (ARadd_0_l ARth) (ARadd_comm ARth) (ARadd_assoc ARth) (ARmul_1_l ARth) (ARmul_0_l ARth) - (ARmul_sym ARth) (ARmul_assoc ARth) (ARdistr_l ARth) + (ARmul_comm ARth) (ARmul_assoc ARth) (ARdistr_l ARth) (ARopp_mul_l ARth) (ARopp_add ARth) (ARsub_def ARth) . @@ -172,7 +172,7 @@ Qed. Theorem rdiv_r_r : forall r, ~ r == 0 -> r / r == 1. intros. rewrite (AFdiv_def AFth) in |- *. -rewrite (ARmul_sym ARth) in |- *. +rewrite (ARmul_comm ARth) in |- *. apply (AFinv_l AFth). trivial. Qed. @@ -317,7 +317,7 @@ transitivity (r1 / r2 * (r4 / r4)). apply (ARmul_1_r Rsth ARth). rewrite rdiv4 in |- *; trivial. rewrite H1 in |- *. - rewrite (ARmul_sym ARth r2 r4) in |- *. + rewrite (ARmul_comm ARth r2 r4) in |- *. rewrite <- rdiv4 in |- *; trivial. rewrite rdiv_r_r in |- *. trivial. @@ -1384,7 +1384,7 @@ transitivity (x + (1 + - (1))). repeat rewrite <- (ARplus_assoc ARth) in |- *. repeat rewrite (ARadd_assoc ARth) in |- *. apply (Radd_ext Reqe). - repeat rewrite <- (ARadd_sym ARth 1) in |- *. + repeat rewrite <- (ARadd_comm ARth 1) in |- *. trivial. reflexivity. rewrite (Ropp_def Rth) in |- *. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index 19ffe1d53..44f2f9501 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -196,7 +196,7 @@ Section ZMORPHISM. replace Eq with (CompOpp Eq);trivial. rewrite <- Pcompare_antisym;simpl. rewrite match_compOpp. - rewrite (Radd_sym Rth). + rewrite (Radd_comm Rth). apply gen_phiZ1_add_pos_neg. rewrite (ARgen_phiPOS_add ARth); norm. Qed. diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index 989ec5ce2..7317ab212 100644 --- a/contrib/setoid_ring/Ring_polynom.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -606,7 +606,7 @@ Section MakeRingPol. induction P';simpl;intros;Esimpl2. generalize P p l;clear P p l. induction P;simpl;intros. - Esimpl2;apply (ARadd_sym ARth). + Esimpl2;apply (ARadd_comm ARth). assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). rewrite H;Esimpl. rewrite IHP';rrefl. rewrite H;Esimpl. rewrite IHP';Esimpl. @@ -635,9 +635,9 @@ Section MakeRingPol. add_push (P3 @ (tail l));rrefl. assert (forall P k l, (PaddX Padd P'1 k P) @ l == P@l + P'1@l * pow (hd 0 l) k). - induction P;simpl;intros;try apply (ARadd_sym ARth). - destruct p2;simpl;try apply (ARadd_sym ARth). - rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth). + induction P;simpl;intros;try apply (ARadd_comm ARth). + destruct p2;simpl;try apply (ARadd_comm ARth). + rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth). assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2. rewrite IHP'1;rsimpl; rewrite H1;add_push (P5 @ (tail l0));rrefl. rewrite IHP'1;simpl;Esimpl. @@ -659,7 +659,7 @@ Section MakeRingPol. induction P';simpl;intros;Esimpl2;trivial. generalize P p l;clear P p l. induction P;simpl;intros. - Esimpl2;apply (ARadd_sym ARth). + Esimpl2;apply (ARadd_comm ARth). assert (H := ZPminus_spec p p0);destruct (ZPminus p p0). rewrite H;Esimpl. rewrite IHP';rsimpl. rewrite H;Esimpl. rewrite IHP';Esimpl. @@ -689,11 +689,11 @@ Section MakeRingPol. assert (forall P k l, (PsubX Psub P'1 k P) @ l == P@l + - P'1@l * pow (hd 0 l) k). induction P;simpl;intros. - rewrite Popp_ok;rsimpl;apply (ARadd_sym ARth);trivial. + rewrite Popp_ok;rsimpl;apply (ARadd_comm ARth);trivial. destruct p2;simpl;rewrite Popp_ok;rsimpl. - apply (ARadd_sym ARth);trivial. - rewrite jump_Pdouble_minus_one;apply (ARadd_sym ARth);trivial. - apply (ARadd_sym ARth);trivial. + apply (ARadd_comm ARth);trivial. + rewrite jump_Pdouble_minus_one;apply (ARadd_comm ARth);trivial. + apply (ARadd_comm ARth);trivial. assert (H1 := ZPminus_spec p2 k);destruct (ZPminus p2 k);Esimpl2;rsimpl. rewrite IHP'1;rsimpl;add_push (P5 @ (tail l0));rewrite H1;rrefl. rewrite IHP'1;rewrite H1;rewrite Pplus_comm. @@ -715,7 +715,7 @@ Section MakeRingPol. (PmulI Pmul_aux P' p P) @ l == P @ l * P' @ (jump p l). Proof. induction P;simpl;intros. - Esimpl2;apply (ARmul_sym ARth). + Esimpl2;apply (ARmul_comm ARth). assert (H1 := ZPminus_spec p p0);destruct (ZPminus p p0);Esimpl2. rewrite H1; rewrite H;rrefl. rewrite H1; rewrite H. @@ -745,13 +745,13 @@ Section MakeRingPol. Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l. Proof. destruct P;simpl;intros. - Esimpl2;apply (ARmul_sym ARth). + Esimpl2;apply (ARmul_comm ARth). rewrite (PmulI_ok P (Pmul_aux_ok P)). - apply (ARmul_sym ARth). + apply (ARmul_comm ARth). rewrite Padd_ok; Esimpl2. rewrite (PmulI_ok P3 (Pmul_aux_ok P3));trivial. rewrite Pmul_aux_ok;mul_push (P' @ l). - rewrite (ARmul_sym ARth (P' @ l));rrefl. + rewrite (ARmul_comm ARth (P' @ l));rrefl. Qed. @@ -795,9 +795,9 @@ Section MakeRingPol. repeat rewrite mkPX_ok; simpl. rsimpl. apply radd_ext; rsimpl. - rewrite (ARadd_sym ARth); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. - rewrite (ARadd_sym ARth); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. case j; simpl; auto; try intros j1; rsimpl. rewrite jump_Pdouble_minus_one; rsimpl. intros j M1. @@ -808,12 +808,12 @@ Section MakeRingPol. rewrite H; rewrite mkPX_ok; rsimpl. repeat (rewrite <-(ARadd_assoc ARth)). apply radd_ext; rsimpl. - rewrite (ARadd_sym ARth); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. repeat (rewrite <-(ARmul_assoc ARth)). rewrite mkZmon_ok. apply rmul_ext; rsimpl. - rewrite (ARmul_sym ARth); rsimpl. + rewrite (ARmul_comm ARth); rsimpl. generalize (Hrec1 (vmon (j - i) M1) l); case (MFactor P2 (vmon (j - i) M1)); simpl; intros P3 Q3 H; repeat rewrite mkPinj_ok; auto. @@ -821,11 +821,11 @@ Section MakeRingPol. rewrite mkPX_ok; rsimpl. repeat (rewrite <-(ARadd_assoc ARth)). apply radd_ext; rsimpl. - rewrite (ARadd_sym ARth); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. repeat (rewrite <-(ARmul_assoc ARth)). apply rmul_ext; rsimpl. - rewrite (ARmul_sym ARth); rsimpl. + rewrite (ARmul_comm ARth); rsimpl. apply rmul_ext; rsimpl. rewrite <- pow_Pplus. rewrite (Pplus_minus _ _ (ZC2 _ _ He)); rsimpl. @@ -836,16 +836,16 @@ Section MakeRingPol. rewrite mkPX_ok; rsimpl. repeat (rewrite <-(ARadd_assoc ARth)). apply radd_ext; rsimpl. - rewrite (ARadd_sym ARth); rsimpl. + rewrite (ARadd_comm ARth); rsimpl. apply radd_ext; rsimpl. rewrite mkZmon_ok. repeat (rewrite <-(ARmul_assoc ARth)). apply rmul_ext; rsimpl. - rewrite (ARmul_sym ARth); rsimpl. + rewrite (ARmul_comm ARth); rsimpl. rewrite mkPX_ok; simpl; rsimpl. rewrite (morph0 CRmorph); rsimpl. repeat (rewrite <-(ARmul_assoc ARth)). - rewrite (ARmul_sym ARth (Q3@l)); rsimpl. + rewrite (ARmul_comm ARth (Q3@l)); rsimpl. apply rmul_ext; rsimpl. rewrite <- pow_Pplus. rewrite (Pplus_minus _ _ He); rsimpl. @@ -1005,7 +1005,7 @@ Section MakeRingPol. | |- context [(?P1 ++ ?P2)@?l] => rewrite (Padd_ok P2 P1 l) | |- context [(?P1 -- ?P2)@?l] => rewrite (Psub_ok P2 P1 l) | |- context [(norm (PEopp ?pe))@?l] => rewrite (norm_PEopp l pe) - end;Esimpl2;try rrefl;try apply (ARadd_sym ARth). + end;Esimpl2;try rrefl;try apply (ARadd_comm ARth). Lemma norm_ok : forall l pe, PEeval l pe == (norm pe)@l. Proof. @@ -1104,7 +1104,7 @@ Section MakeRingPol. induction lm; simpl in |- *; intros. rrefl. rewrite IHlm; simpl in |- *. - repeat rewrite <- (ARmul_sym ARth a); rewrite <- mul_mkmult. + repeat rewrite <- (ARmul_comm ARth a); rewrite <- mul_mkmult. rrefl. Qed. @@ -1123,7 +1123,7 @@ Section MakeRingPol. setoid_replace (pow x p * (pow x p * r) ) with (pow x p * pow x p * r);Esimpl. unfold rev';simpl. repeat rewrite mkmult_rev_append;simpl. - rewrite (ARmul_sym ARth);rrefl. + rewrite (ARmul_comm ARth);rrefl. Qed. Lemma Pphi_add_mult_dev : forall P rP fv lm, diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 552e0dec7..dd83b05a8 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -39,11 +39,11 @@ Section DEFINITIONS. (** Semi Ring *) Record semi_ring_theory : Prop := mk_srt { SRadd_0_l : forall n, 0 + n == n; - SRadd_sym : forall n m, n + m == m + n ; + SRadd_comm : forall n m, n + m == m + n ; SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p; SRmul_1_l : forall n, 1*n == n; SRmul_0_l : forall n, 0*n == 0; - SRmul_sym : forall n m, n*m == m*n; + SRmul_comm : forall n m, n*m == m*n; SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p; SRdistr_l : forall n m p, (n + m)*p == n*p + m*p }. @@ -52,11 +52,11 @@ Section DEFINITIONS. (*Almost ring are no ring : Ropp_def is missing **) Record almost_ring_theory : Prop := mk_art { ARadd_0_l : forall x, 0 + x == x; - ARadd_sym : forall x y, x + y == y + x; + ARadd_comm : forall x y, x + y == y + x; ARadd_assoc : forall x y z, x + (y + z) == (x + y) + z; ARmul_1_l : forall x, 1 * x == x; ARmul_0_l : forall x, 0 * x == 0; - ARmul_sym : forall x y, x * y == y * x; + ARmul_comm : forall x y, x * y == y * x; ARmul_assoc : forall x y z, x * (y * z) == (x * y) * z; ARdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); ARopp_mul_l : forall x y, -(x * y) == -x * y; @@ -67,10 +67,10 @@ Section DEFINITIONS. (** Ring *) Record ring_theory : Prop := mk_rt { Radd_0_l : forall x, 0 + x == x; - Radd_sym : forall x y, x + y == y + x; + Radd_comm : forall x y, x + y == y + x; Radd_assoc : forall x y z, x + (y + z) == (x + y) + z; Rmul_1_l : forall x, 1 * x == x; - Rmul_sym : forall x y, x * y == y * x; + Rmul_comm : forall x y, x * y == y * x; Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z; Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z); Rsub_def : forall x y, x - y == x + -y; @@ -200,9 +200,9 @@ Section ALMOST_RING. Lemma SRth_ARth : almost_ring_theory 0 1 radd rmul SRsub SRopp req. Proof (mk_art 0 1 radd rmul SRsub SRopp req - (SRadd_0_l SRth) (SRadd_sym SRth) (SRadd_assoc SRth) + (SRadd_0_l SRth) (SRadd_comm SRth) (SRadd_assoc SRth) (SRmul_1_l SRth) (SRmul_0_l SRth) - (SRmul_sym SRth) (SRmul_assoc SRth) (SRdistr_l SRth) + (SRmul_comm SRth) (SRmul_assoc SRth) (SRdistr_l SRth) SRopp_mul_l SRopp_add SRsub_def). (** Identity morphism for semi-ring equipped with their almost-ring structure*) @@ -253,17 +253,17 @@ Section ALMOST_RING. rewrite (Rdistr_l Rth);rewrite (Rmul_1_l Rth). rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite (Radd_sym Rth); rewrite (Radd_0_l Rth);sreflexivity. + rewrite (Radd_comm Rth); rewrite (Radd_0_l Rth);sreflexivity. Qed. Lemma Ropp_mul_l : forall x y, -(x * y) == -x * y. Proof. intros x y;rewrite <-(Radd_0_l Rth (- x * y)). - rewrite (Radd_sym Rth). + rewrite (Radd_comm Rth). rewrite <-(Ropp_def Rth (x*y)). rewrite (Radd_assoc Rth). rewrite <- (Rdistr_l Rth). - rewrite (Rth.(Radd_sym) (-x));rewrite (Ropp_def Rth). + rewrite (Rth.(Radd_comm) (-x));rewrite (Ropp_def Rth). rewrite Rmul_0_l;rewrite (Radd_0_l Rth);sreflexivity. Qed. @@ -273,17 +273,17 @@ Section ALMOST_RING. rewrite <- ((Ropp_def Rth) x). rewrite <- ((Radd_0_l Rth) (x + - x + - (x + y))). rewrite <- ((Ropp_def Rth) y). - rewrite ((Radd_sym Rth) x). - rewrite ((Radd_sym Rth) y). + rewrite ((Radd_comm Rth) x). + rewrite ((Radd_comm Rth) y). rewrite <- ((Radd_assoc Rth) (-y)). rewrite <- ((Radd_assoc Rth) (- x)). rewrite ((Radd_assoc Rth) y). - rewrite ((Radd_sym Rth) y). + rewrite ((Radd_comm Rth) y). rewrite <- ((Radd_assoc Rth) (- x)). rewrite ((Radd_assoc Rth) y). - rewrite ((Radd_sym Rth) y);rewrite (Ropp_def Rth). - rewrite ((Radd_sym Rth) (-x) 0);rewrite (Radd_0_l Rth). - apply (Radd_sym Rth). + rewrite ((Radd_comm Rth) y);rewrite (Ropp_def Rth). + rewrite ((Radd_comm Rth) (-x) 0);rewrite (Radd_0_l Rth). + apply (Radd_comm Rth). Qed. Lemma Ropp_opp : forall x, - -x == x. @@ -291,13 +291,13 @@ Section ALMOST_RING. intros x; rewrite <- (Radd_0_l Rth (- -x)). rewrite <- (Ropp_def Rth x). rewrite <- (Radd_assoc Rth); rewrite (Ropp_def Rth). - rewrite ((Radd_sym Rth) x);apply (Radd_0_l Rth). + rewrite ((Radd_comm Rth) x);apply (Radd_0_l Rth). Qed. Lemma Rth_ARth : almost_ring_theory 0 1 radd rmul rsub ropp req. Proof - (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_sym Rth) (Radd_assoc Rth) - (Rmul_1_l Rth) Rmul_0_l (Rmul_sym Rth) (Rmul_assoc Rth) (Rdistr_l Rth) + (mk_art 0 1 radd rmul rsub ropp req (Radd_0_l Rth) (Radd_comm Rth) (Radd_assoc Rth) + (Rmul_1_l Rth) Rmul_0_l (Rmul_comm Rth) (Rmul_assoc Rth) (Rdistr_l Rth) Ropp_mul_l Ropp_add (Rsub_def Rth)). (** Every semi morphism between two rings is a morphism*) @@ -322,12 +322,12 @@ Section ALMOST_RING. Proof. intros x;rewrite <- (Rth.(Radd_0_l) [-!x]). rewrite <- ((Ropp_def Rth) [x]). - rewrite ((Radd_sym Rth) [x]). + rewrite ((Radd_comm Rth) [x]). rewrite <- (Radd_assoc Rth). rewrite <- (Smorph_add Smorph). rewrite (Ropp_def Cth). rewrite (Smorph0 Smorph). - rewrite (Radd_sym Rth (-[x])). + rewrite (Radd_comm Rth (-[x])). apply (Radd_0_l Rth);sreflexivity. Qed. @@ -371,15 +371,15 @@ Qed. Ltac mrewrite := repeat first [ rewrite (ARadd_0_l ARth) - | rewrite <- ((ARadd_sym ARth) 0) + | rewrite <- ((ARadd_comm ARth) 0) | rewrite (ARmul_1_l ARth) - | rewrite <- ((ARmul_sym ARth) 1) + | rewrite <- ((ARmul_comm ARth) 1) | rewrite (ARmul_0_l ARth) - | rewrite <- ((ARmul_sym ARth) 0) + | rewrite <- ((ARmul_comm ARth) 0) | rewrite (ARdistr_l ARth) | sreflexivity | match goal with - | |- context [?z * (?x + ?y)] => rewrite ((ARmul_sym ARth) z (x+y)) + | |- context [?z * (?x + ?y)] => rewrite ((ARmul_comm ARth) z (x+y)) end]. Lemma ARadd_0_r : forall x, (x + 0) == x. @@ -394,37 +394,37 @@ Qed. Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. Proof. intros;mrewrite. - repeat rewrite (ARth.(ARmul_sym) z);sreflexivity. + repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. Qed. Lemma ARadd_assoc1 : forall x y z, (x + y) + z == (y + z) + x. Proof. intros;rewrite <-(ARth.(ARadd_assoc) x). - rewrite (ARth.(ARadd_sym) x);sreflexivity. + rewrite (ARth.(ARadd_comm) x);sreflexivity. Qed. Lemma ARadd_assoc2 : forall x y z, (y + x) + z == (y + z) + x. Proof. intros; repeat rewrite <- (ARadd_assoc ARth); - rewrite ((ARadd_sym ARth) x); sreflexivity. + rewrite ((ARadd_comm ARth) x); sreflexivity. Qed. Lemma ARmul_assoc1 : forall x y z, (x * y) * z == (y * z) * x. Proof. intros;rewrite <-((ARmul_assoc ARth) x). - rewrite ((ARmul_sym ARth) x);sreflexivity. + rewrite ((ARmul_comm ARth) x);sreflexivity. Qed. Lemma ARmul_assoc2 : forall x y z, (y * x) * z == (y * z) * x. Proof. intros; repeat rewrite <- (ARmul_assoc ARth); - rewrite ((ARmul_sym ARth) x); sreflexivity. + rewrite ((ARmul_comm ARth) x); sreflexivity. Qed. Lemma ARopp_mul_r : forall x y, - (x * y) == x * -y. Proof. - intros;rewrite ((ARmul_sym ARth) x y); - rewrite (ARopp_mul_l ARth); apply (ARmul_sym ARth). + intros;rewrite ((ARmul_comm ARth) x y); + rewrite (ARopp_mul_l ARth); apply (ARmul_comm ARth). Qed. Lemma ARopp_zero : -0 == 0. diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 81880464b..0f91a7e3f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -55,7 +55,7 @@ sp is a local copy of the global variable extern_sp. */ # define Next break #endif -/*#define _COQ_DEBUG_ */ +/* #define _COQ_DEBUG_ */ #ifdef _COQ_DEBUG_ # define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s) @@ -821,11 +821,34 @@ value coq_interprete } Instruct(SETFIELD1){ + int i, j, size, size_aux; print_instr("SETFIELD1"); CAML_MODIFY(&Field(accu, 1),*sp); - sp++; - Next; + sp++; + Next; } + + /* *sp = accu; + * Netoyage des cofix * + size = Wosize_val(accu); + for (i = 2; i < size; i++) { + accu = Field(*sp, i); + if (IS_EVALUATED_COFIX(accu)) { + size_aux = Wosize_val(accu); + *--sp = accu; + Alloc_small(accu, size_aux, Accu_tag); + for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j); + *sp = accu; + Alloc_small(accu, 1, ATOM_COFIX_TAG); + Field(accu, 0) = Field(Field(*sp, 1), 0); + CAML_MODIFY(&Field(*sp, 1), accu); + accu = *sp; sp++; + CAML_MODIFY(&Field(*sp, i), accu); + } + } + sp++; + Next; + } */ Instruct(SETFIELD){ print_instr("SETFIELD"); diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h index 48fba64bf..a5176f3f5 100644 --- a/kernel/byterun/coq_values.h +++ b/kernel/byterun/coq_values.h @@ -32,6 +32,7 @@ /* Les blocs accumulate */ #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag)) +#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG)) #endif /* _COQ_VALUES_ */ diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index e3105fb90..6fac9e050 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -24,7 +24,15 @@ val translate_local_def : env -> constr * types option -> val translate_local_assum : env -> types -> types * Univ.constraints - + +val infer_declaration : env -> constant_entry -> + Declarations.constr_substituted option * Term.types * Univ.constraints * + bool * bool + +val build_constant_declaration : env -> 'a -> + Declarations.constr_substituted option * Term.types * Univ.constraints * + bool * bool -> Declarations.constant_body + val translate_constant : env -> constant -> constant_entry -> constant_body val translate_mind : diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 516caf3ed..aeb4d294b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -93,3 +93,8 @@ val type_fixpoint : env -> name array -> types array (* Kernel safe typing but applicable to partial proofs *) val typing : env -> constr -> unsafe_judgment +(* A virer *) +val execute : Environ.env -> + Term.types -> + Univ.Constraint.t * Univ.universes -> + Environ.unsafe_judgment * (Univ.Constraint.t * Univ.universes) |