Commit e29df18b authored by Heiko Becker's avatar Heiko Becker

Merge branch 'reworked_type_validator' of gitlab.mpi-sws.org:AVA/FloVer into...

Merge branch 'reworked_type_validator' of gitlab.mpi-sws.org:AVA/FloVer into reworked_type_validator
parents 69e60d78 53eb2e1c
......@@ -289,8 +289,6 @@ Qed.
Lemma typing_expr_64_bit e:
forall Gamma,
(* noDowncast e ->
is64BitEval e -> *)
is64BitEnv Gamma ->
validTypes e Gamma ->
FloverMap.find e Gamma = Some M64.
......@@ -298,44 +296,9 @@ Proof.
destruct e; intros * Gamma_64Bit [mG [find_mG ?]];
erewrite <- Gamma_64Bit; eauto.
Qed.
(* - destruct typecheck_e as [? [? ?]].
rewrite types_valid in *; try set_tac.
- destruct typecheck_e as [? [? [? ?]]]; congruence.
- destruct typecheck_e as [? [? [[? [? [? ?]]]_]]]. erewrite IHe in *; eauto.
assert (x0 = M64) by congruence; subst.
unfold isCompat in H2; destruct x; simpl in *; try congruence;
type_conv; subst.
- destruct typecheck_e as [? [? [[? [? [? [? [? [? ?]]]]]] _]]].
repeat (match goal with
|H: _ /\ _ |- _=> destruct H
end).
erewrite IHe1 in *; try eauto.
+ erewrite IHe2 in *; try eauto.
* inversion H4; inversion H5; subst.
destruct x; cbn in H6; congruence.
* intros; apply types_valid; set_tac.
+ intros; apply types_valid; set_tac.
- repeat (match goal with
|H: _ /\ _ |- _=> destruct H
end).
destruct typecheck_e as [? [? [[? [? [? [? [? [? [? [? [? ?]]]]]]]]] _]]].
erewrite IHe1 with (Gamma:=Gamma) in *;
eauto;
[ | intros; apply types_valid; set_tac].
erewrite IHe2 with (Gamma:=Gamma) in *;
eauto;
[ | intros; apply types_valid; set_tac].
erewrite IHe3 with (Gamma:=Gamma) in *;
eauto;
[ | intros; apply types_valid; set_tac].
inversion H12; inversion H13; inversion H14; subst.
destruct x; cbn in *; congruence.
Qed. *)
Lemma typing_cmd_64_bit f:
forall Gamma,
(* noDowncastFun f ->
is64BitBstep f -> *)
is64BitEnv Gamma ->
validTypesCmd f Gamma ->
FloverMap.find (getRetExp f) Gamma = Some M64.
......@@ -345,49 +308,6 @@ Proof.
eapply IHf; eauto.
- destruct valid_f; simpl in *; eapply typing_expr_64_bit; auto.
Qed.
(* induction f; intros * noDowncast_f is64BitEval_f typecheck_f types_valid;
cbn in *;
subst; try eauto using typing_expr_64_bit;
Flover_compute; try congruence.
- destruct noDowncast_f; destruct is64BitEval_f as [Ha [Hb Hc]].
destruct typecheck_f as [[? [? [? [? [? ?]]]]] _];
eapply IHf; eauto.
intros.
destruct (v =? n) eqn:?.
+ rewrite Nat.eqb_eq in Heqb; subst.
auto.
+ apply types_valid.
rewrite NatSet.remove_spec, NatSet.union_spec.
split; try auto.
hnf; intros; subst. rewrite Nat.eqb_neq in Heqb.
congruence.
- eapply typing_expr_64_bit; eauto.
destruct typecheck_f; auto.
Qed. *)
(* Lemma typing_agrees_expr e: *)
(* forall E Gamma tMap v m1 m2 fBits, *)
(* typeCheck e Gamma tMap fBits = true -> *)
(* eval_expr E Gamma (toRBMap fBits) (toRExp e) v m1 -> *)
(* FloverMap.find e tMap = Some m2 -> *)
(* m1 = m2. *)
(* Proof. *)
(* intros. *)
(* pose proof (typingSoundnessExp _ _ H H0). *)
(* congruence. *)
(* Qed. *)
(* Lemma typing_agrees_cmd f: *)
(* forall E Gamma tMap v m1 m2 fBits, *)
(* typeCheckCmd f Gamma tMap fBits = true -> *)
(* bstep (toRCmd f) E Gamma (toRBMap fBits) v m1 -> *)
(* FloverMap.find (getRetExp f) tMap = Some m2 -> *)
(* m1 = m2. *)
(* Proof. *)
(* intros. *)
(* pose proof (typingSoundnessCmd _ _ H H0). *)
(* congruence. *)
(* Qed. *)
Lemma round_0_zero:
(Fcore_generic_fmt.round radix2 (Fcore_FLT.FLT_exp (3 - 1024 - 53) 53)
......
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