Require Import Atoms.
Require Import Kernel.
Require Export Certificate.
Require Import MiscUtils.

Record abs_term := {
  tconc: term ;
  tabs: var → kernel ;
  tproof: ∀ x s, Kangel_wlp (tabs x) (eq (add (vid x) (teval tconc s) s)) s
}.

Program Definition abs_assign (x:var) (t: abs_term) := {|
  concrete:= assign x (tconc t) ;
  abstract:= tabs t x ;
  certif_correctness:= _
|}.
Obligation 1.
  eapply Kangel_wlp_correctness.
  eauto.
  eapply tproof.
Qed.

Program Definition tret (t:term) :=
{|
  tconc := t ;
  tabs := fun x ⇒ assign x t ;
  tproof := _
|}.

Coercion tret: term >-> abs_term.

Record hoare_term (t:term) := {
  hname: string ;
  htpre: cond ;
  htpost: var → cond ;
  htproof: ∀ x s, eval htpre s → oeval (htpost x) s (add (vid x) (teval t s) s)
}.
Implicit Arguments hname [t].
Implicit Arguments htpre [t].
Implicit Arguments htpost [t].

Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..): list_scope.

Program Definition hoare_abs {t:term} (ht: hoare_term t) :=
{|
  tconc:= t ;
  tabs := fun x ⇒ Kseq (xrequire (htpre ht) (hname ht))
                        (guassign [x] (htpost ht x)) ;
  tproof:= _
|}.
Obligation 1.
  constructor 1 with (x:=add (vid x) (teval t s) s).
  simpl; intuition.
  unfold lframeeq; simpl.
  intros; rewrite add_out2; intuition.
  eapply htproof; auto.
Qed.

Coercion hoare_abs: hoare_term >-> abs_term.

Program Definition coq_abs_conj {t:term} (ht1 ht2: hoare_term t) : hoare_term t :=
{|
  hname:="coq_abs_conj" ;
  htpre:=bin AND (htpre ht1) (htpre ht2) ;
  htpost:=fun x ⇒ bin AND (htpost ht1 x) (htpost ht2 x) ;
  htproof:= _
|}.
Obligation 1.
  intuition; eapply htproof; auto.
Qed.

Program Definition abs_coerce {t1:term} (ht: hoare_term t1) (t2: term) : hoare_term t2 :=
{|
  hname:="abs_coerce" ;
  htpre:=if term_eq t2 t1 then htpre ht else absurd ;
  htpost:=htpost ht ;
  htproof:= _
|}.
Obligation 1.
  generalize H; clear H.
  casebool (term_eq t2 t1).
  rewrite (term_eq_eval _ _ _ H).
  eapply htproof; auto.
  intuition.
Qed.

Definition abs_conj {t1 t2:term} (ht1: hoare_term t1) (ht2: hoare_term t2): hoare_term t1 :=
  coq_abs_conj ht1 (abs_coerce ht2 t1).

Definition abs_rename (s: string) {t: term} (ht: hoare_term t) : hoare_term t :=
{|
  hname:=s ;
  htpre:=htpre ht ;
  htpost:=htpost ht ;
  htproof:=htproof _ ht
|}.

Program Definition abs_simplify_pre {t: term} (ht: hoare_term t) (c: cond | ∀ s, eval c s → eval (htpre ht) s): hoare_term t :=
{| hname:="abs_simplify_pre" ;
   htpre:=c ;
   htpost:=htpost ht ;
   htproof:=_
|}.
Obligation 1.
  eapply htproof; eauto.
Qed.

Record term_rewrite (rwout:term) := {
  rwin: term ;
  rwproof: ∀ s, teval rwin s = teval rwout s
}.
Implicit Arguments rwin [rwout].

Program Definition abs_rewrite (p: abs_term) (r: term_rewrite (tconc p)): abs_term :=
{|
  tconc := rwin r ;
  tabs := tabs p ;
  tproof := _
|}.
Obligation 1.
  rewrite rwproof; eapply tproof.
Qed.

Program Definition tbranch2 (label: alabel) (t: bool → abs_term) : abs_term :=
{|
   tconc := tconc (t true);
   tabs := if term_eq (tconc (t true)) (tconc (t false)) then
               fun y ⇒ Kbranch2 label (fun b:bool ⇒ tabs (t b) y)
            else
               fun y ⇒ xrequire absurd "tbranch: concrete branches are not equal"
|}.
Obligation 1.
  casebool (term_eq (tconc (t true)) (tconc (t false))); intuition.
  eapply tproof; eauto.
  rewrite (term_eq_eval _ _ _ H).
  eapply tproof; auto.
Qed.

Program Definition ht_branch2 {t:term} {A:Type} (ht: A → hoare_term t) (label: alabel) (select: bool → A) :=
{|
  tconc:= t ;
  tabs := fun x ⇒ Kbranch2 label (fun b:bool ⇒ let ht := (ht (select b)) in
                      Kseq (xrequire (htpre ht) (hname ht))
                           (guassign [x] (htpost ht x))) ;
  tproof:= _
|}.
Obligation 1.
  constructor 1;
  (constructor 1 with (x:=add (vid x) (teval t s) s);
   simpl; intuition;
   [ unfold lframeeq; simpl; intros; rewrite add_out2; intuition |
     eapply htproof; auto ]).
Qed.

Definition htb2 {t:term} (label: alabel) (ht: bool → hoare_term t) :=
 ht_branch2 ht label (fun x ⇒ x).

Program Definition ht_branch {t:term} {A:Type} (ht: A → hoare_term t) (label: alabel) (select: Z → A) :=
{|
  tconc:= t ;
  tabs := fun x ⇒ Kbranch label (fun z:Z ⇒ let ht := ht (select z) in
                      Kseq (xrequire (htpre ht) (hname ht))
                           (guassign [x] (htpost ht x))) ;
  tproof:= _
|}.
Obligation 1.
  constructor 1 with (x:=add (vid x) (teval t s) s);
   simpl; intuition;
   [ unfold lframeeq; simpl; intros; rewrite add_out2; intuition |
     eapply htproof; auto ].
Qed.

Require Import Coq.Logic.FunctionalExtensionality.

Program Definition tbind (x:var) (t1 t2: abs_term) : abs_term :=
 {|
  tconc := tsubst (tconc t2) (vid x) (tconc t1) ;
  tabs := fun y ⇒ if (var_eq x y) then Kseq (tabs t1 x) (tabs t2 x)
                                   else Kclone x (Kseq (tabs t1 x) (tabs t2 y)) ;
  tproof := _
|}.
Obligation 1.
   rewrite tsubst_teval.
   casebool (var_eq x x0).
   intros; eapply Kangel_wlp_monotonic.
   eapply tproof; eapply Kwlp_monotonic; eauto.
   intros; subst; eapply Kangel_wlp_monotonic.
   eapply tproof; eapply Kangel_wlp_correctness.
   intros; subst.
   rewrite (var_eq_eq _ _ H); clear H.
   intros; subst.
   apply functional_extensionality.
   unfold add at 1 3.
   intros x1; case (POrderedType.Positive_as_DT.eq_dec (vid x0) x1).
   intros; subst; auto.
   intros; rewrite add_out2; auto.
   intros; eapply Kangel_wlp_monotonic.
   eapply tproof; eapply Kwlp_monotonic; eauto.
   intros; subst; eapply Kangel_wlp_monotonic.
   eapply tproof; eapply Kangel_wlp_correctness.
   intros; subst.
   unfold var_eq in H.
   assert (X: (vid x)<>(vid x0)).
   case (Peqb_eq (vid x) (vid x0)). rewrite H. intuition.
   clear H.
   apply functional_extensionality.
   intros x1. unfold add at 1.
   case (POrderedType.Positive_as_DT.eq_dec (vid x0) x1).
   intros; subst.
   rewrite add_out2; auto.
   rewrite add_in; auto.
   unfold add at 1.
   case (POrderedType.Positive_as_DT.eq_dec (vid x) x1).
   intros; subst; auto.
   intros; repeat (rewrite add_out2; auto).
Qed.

Notation "'let_term' x := t1 'in' t2" := (tbind x t1 t2)
    (at level 95, t1 at level 93, right associativity): certif_scope.