Commit e1fa08a4 authored by Heiko Becker's avatar Heiko Becker
Browse files

more work on type validator

parent 934172b1
......@@ -177,13 +177,13 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
match mOldO with
| None => Fail _ "Undefined fixed-point type"
| Some mj =>
Succes (FloverMap.add e mj akk2_map)
addMono e mj akk2_map
match (join_fl t1 t2) with
| Some m =>
if (isMonotone mOldO m)
then Succes (FloverMap.add e m akk2_map)
then addMono e m akk2_map
else Fail _ "Wrong type annotation for binary operator"
| None => Fail _ "Could not compute join for arguments"
......@@ -264,6 +264,55 @@ Lemma no_cycle_unop e:
destruct (unopEq u Neg); congruence.
Lemma map_find_add e1 e2 m map1:
FloverMap.find e1 (FloverMap.add e2 m map1) =
match e2 e1 with
|Eq => Some m
|_ => FloverMap.find (elt:=mType) e1 map1
rewrite FloverMapFacts.P.F.add_o.
unfold FloverMapFacts.P.F.eq_dec.
destruct (Q_orderedExps.exprCompare e2 e1) eqn:?; congruence.
Ltac by_monotonicity find_akk mem_case:=
rewrite map_find_add;
match goal with
| [ H: _ |- context [ ?e1 ?e2] ] =>
destruct ( e1 e2) eqn:?; try congruence
erewrite <- FloverMapFacts.P.F.find_o in find_akk; try eauto;
rewrite FloverMapFacts.P.F.mem_find_b in mem_case;
rewrite find_akk in *; congruence.
Lemma getValidMap_mono e:
forall Gamma akk res,
getValidMap Gamma e akk = Succes res ->
forall e m, FloverMap.find e akk = Some m ->
FloverMap.find e res = Some m.
pose (eT := e);
induction e; intros * getMap_succeeds * find_akk;
destruct (FloverMap.mem eT akk) eqn:Hmem; subst;
cbn in getMap_succeeds; subst eT;
rewrite Hmem in *;
try (inversion getMap_succeeds; subst; auto; fail "");
Flover_compute; try congruence.
- inversion getMap_succeeds; subst.
by_monotonicity find_akk Hmem.
- unfold isMonotone in *.
+ destruct (mTypeEq m1 m) eqn:?; try congruence; type_conv; subst.
inversion getMap_succeeds; subst.
by_monotonicity find_akk Hmem.
+ inversion getMap_succeeds; subst.
by_monotonicity find_akk Hmem.
(* Lemma eval_expr_drop_unop_gamma e: *)
(* forall E Gamma u m v mres, *)
(* eval_expr E (toRTMap (FloverMap.add (Unop u e) m Gamma)) (toRExp e) v mres -> *)
......@@ -439,6 +488,8 @@ Proof.
destruct (isFixedPointB m && isFixedPointB m0) eqn:?.
+ destruct (FloverMap.find (elt:=mType) (Binop b e1 e2) Gamma) eqn:?;
try congruence.
unfold addMono in *.
inversion validMap_succ; subst.
exists m1; repeat split; try eauto using tMap_def.
* eapply validTypes_mono with (map1:=t0).
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