Commit 36a22bbb authored by Heiko Becker's avatar Heiko Becker

Show correctness of expression level type validator

parent e1fa08a4
(** 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.NatSet Flover.Infra.RationalSimps Flover.Infra.RealRationalProps.
From Coq
Require Import Bool.Bool Reals.Reals QArith.QArith QArith.Qreals micromega.Psatz.
From Flover.Infra
Require Import RealSimps NatSet RationalSimps RealRationalProps Results.
Global Set Implicit Arguments.
......@@ -63,15 +65,31 @@ Definition optionBind (X: Type) (Y: Type) (v: option X) (f: X -> Y) (e: Y): Y :=
| None => e
end.
Definition resultBind (X:Type) (r:result X) (f: X -> result X) :result X :=
match r with
| Succes res => f res
| _ => r
end.
Definition resultReturn (X:Type) (r:X) :=
Succes r.
Notation "'olet' x ':=' u 'in' t" := (optionBind u (fun x => t) None)
(only parsing, at level 0, t at level 200).
Notation "'plet' x ':=' u 'in' t" := (optionBind u (fun x => t) False)
(only parsing, at level 0, t at level 200).
Notation "'rlet' x ':=' u 'in' t" := (resultBind u (fun x => t))
(only parsing, at level 0, t at level 200).
Notation "'ret' x" := (resultReturn x) (only parsing, at level 0 ).
Check (rlet x := (Succes true) in match x with | _ => ret true end).
Ltac optionD :=
match goal with
|H: context[resultBind ?v ?f] |- _ =>
destruct v eqn:?
|H: context[optionBind ?v ?default ?f] |- _ =>
destruct ?v eqn:?
destruct v eqn:?
end.
Lemma optionBind_eq (X Y: Type) v (f: X -> Y) (e: Y):
......@@ -94,6 +112,23 @@ Ltac remove_conds := rewrite <- andb_lazy_alt in *.
Ltac remove_conds_asm := rewrite <- andb_lazy_alt in * |- .
Ltac result_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [resultBind ?t _ ]]
=> rewrite H; cbn
| [ H1: ?t = ?u, H2: context [resultBind ?t _] |- _ ]
=> rewrite H1 in H2; cbn in H2
| [ H: context [resultBind ?t _ ] |- _ ]
=> destruct t eqn:?; cbn in H; try congruence
end.
Ltac result_factorize :=
result_factorize_asm ||
match goal with
| [ |- context [resultBind ?t _] ]
=> destruct t eqn:?; cbn; try congruence
end.
Ltac match_factorize_asm :=
match goal with
| [ H: ?t = ?u |- context [optionBind ?t _ _]]
......@@ -128,6 +163,7 @@ Ltac match_simpl :=
try remove_conds;
try remove_matches;
repeat match_factorize;
repeat result_factorize;
try pair_factorize.
Ltac bool_factorize :=
......@@ -140,6 +176,7 @@ Ltac Flover_compute_asm :=
(try remove_conds_asm;
try remove_matches_asm;
repeat match_factorize_asm;
repeat result_factorize_asm;
try pair_factorize) ||
bool_factorize).
......@@ -148,6 +185,7 @@ Ltac Flover_compute :=
(try remove_conds;
try remove_matches;
repeat match_factorize;
repeat result_factorize;
try pair_factorize) ||
bool_factorize).
......
......@@ -289,6 +289,12 @@ Definition morePrecise (m1:mType) (m2:mType) :=
| _, _ => false
end.
Lemma morePrecise_refl m:
morePrecise m m = true.
Proof.
destruct m; cbn; auto using Pos.leb_refl.
Qed.
Lemma morePrecise_trans m1 m2 m3:
morePrecise m1 m2 = true ->
morePrecise m2 m3 = true ->
......
From Coq
Require Import Strings.Ascii Strings.String Lists.List.
From Flover.Infra
Require Import Ltacs.
Set Implicit Arguments.
Inductive result (rT:Type) : Type :=
| Succes: rT -> result rT
......
This diff is collapsed.
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