Commit c5a76189 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Ensure compilation (of changed things) after merge

parent 99aecf45
This diff is collapsed.
......@@ -425,12 +425,12 @@ Proof.
rewrite <- (H n); auto.
Qed.
Lemma eval_exp_ignore_bind e:
Lemma eval_expr_ignore_bind e:
forall x v m Gamma E,
eval_exp E Gamma e v m ->
eval_expr E Gamma e v m ->
~ NatSet.In x (usedVars e) ->
forall m_new v_new,
eval_exp (updEnv x v_new E) (updDefVars x m_new Gamma) e v m.
eval_expr (updEnv x v_new E) (updDefVars x m_new Gamma) e v m.
Proof.
induction e; intros * eval_e no_usedVar *; cbn in *;
inversion eval_e; subst; try eauto.
......
......@@ -2,7 +2,7 @@
Some abbreviations that require having defined exprressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
**)
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts.
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QOrderedType Coq.FSets.FMapAVL Coq.FSets.FMapFacts Recdef.
Require Import Flover.AffineForm.
Require Export Flover.Infra.Abbrevs Flover.Expressions Flover.OrderedExpressions.
......@@ -10,6 +10,21 @@ Require Export Flover.Infra.Abbrevs Flover.Expressions Flover.OrderedExpressions
Module Q_orderedExps := ExprOrderedType (Q_as_OT).
Module legacy_OrderedQExps := Structures.OrdersAlt.Backport_OT (Q_orderedExps).
Functional Scheme exprCompare_ind := Induction for Q_orderedExps.exprCompare Sort Prop.
Lemma expr_compare_eq_eval_compat (e1 e2: expr Q):
Q_orderedExps.exprCompare e1 e2 = Eq -> (toRExp e1) = (toRExp e2).
Proof.
intros Heq.
functional induction (Q_orderedExps.exprCompare e1 e2); simpl in Heq;
try congruence; try (simpl; f_equal; auto); try (now rewrite <- mTypeEq_compat_eq);
try now apply Nat.compare_eq.
all: admit.
(* - rewrite Q_orderedExps.V_orderedFacts.compare_eq_iff in Heq. *)
(* now apply Qeq_eqR in Heq. *)
(* - now rewrite <- unopEq_compat_eq. *)
Admitted.
Module FloverMap := FMapAVL.Make(legacy_OrderedQExps).
Module FloverMapFacts := OrdProperties (FloverMap).
......@@ -17,7 +32,7 @@ Definition analysisResult :Type := FloverMap.t (intv * error).
Definition expressionsAffine: Type := FloverMap.t (affine_form Q).
Definition contained_flover_map V expmap1 expmap2 :=
forall (e: exp Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.
forall (e: expr Q) (v: V), FloverMap.find e expmap1 = Some v -> FloverMap.find e expmap2 = Some v.
Instance contained_flover_map_preorder (V: Type) : PreOrder (@contained_flover_map V).
Proof.
......@@ -30,7 +45,7 @@ Lemma contained_flover_map_extension V (expmap: FloverMap.t V) e v:
Proof.
intros Hnone e' v' Hcont.
rewrite <- Hcont.
destruct (Q_orderedExps.expCompare e e') eqn: Hcomp.
destruct (Q_orderedExps.exprCompare e e') eqn: Hcomp.
- assert (FloverMap.find e expmap = FloverMap.find e' expmap) by (apply FloverMapFacts.P.F.find_o; auto); congruence.
- apply FloverMapFacts.P.F.add_neq_o; congruence.
- apply FloverMapFacts.P.F.add_neq_o; congruence.
......@@ -42,7 +57,7 @@ Lemma contained_flover_map_add_compat V (expmap1 expmap2: FloverMap.t V) e v:
Proof.
unfold contained_flover_map.
intros A e' v' B.
destruct (Q_orderedExps.expCompare e e') eqn: Hcomp.
destruct (Q_orderedExps.exprCompare e e') eqn: Hcomp.
- rewrite FloverMapFacts.P.F.add_eq_o in B; auto.
rewrite FloverMapFacts.P.F.add_eq_o; auto.
- rewrite FloverMapFacts.P.F.add_neq_o in B; try congruence.
......
(** Ltac definitions **)
Require Import Coq.Bool.Bool Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals Coq.micromega.Psatz.
Require Import Flover.Infra.RealSimps Flover.Infra.Abbrevs Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Require Import Flover.Infra.RealSimps Flover.Infra.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
Global Set Implicit Arguments.
......
From Coq
Require Import QArith.QArith Structures.Orders.
Require Import QArith.QArith Structures.Orders Recdef.
From Flover
Require Import Infra.RealRationalProps Infra.RationalSimps Infra.Ltacs
......@@ -914,4 +914,4 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
Close Scope positive_scope.
End ExprOrderedType.
\ No newline at end of file
End ExprOrderedType.
......@@ -201,7 +201,7 @@ Proof.
case_eq (n =? y); auto.
Qed.
Lemma ssa_inv_let V (e:exp V) m x g inVars outVars:
Lemma ssa_inv_let V (e: expr V) m x g inVars outVars:
ssa (Let m x e g) inVars outVars ->
~ NatSet.In x inVars /\ ~ NatSet.In x (usedVars e).
Proof.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment