Module Qcert.NNRSimp.Lang.NNRSimpEval

Require Import String.
Require Import List.
Require Import Arith.
Require Import EquivDec.
Require Import Morphisms.
Require Import Arith.
Require Import Max.
Require Import Bool.
Require Import Peano_dec.
Require Import EquivDec.
Require Import Decidable.
Require Import Utils.
Require Import DataRuntime.
Require Import NNRSimp.
Require Import NNRSimpVars.

Section NNRSimpEval.
  Import ListNotations.

  Context {fruntime:foreign_runtime}.

  Context (h:brand_relation_t).

  Local Open Scope nnrs_imp.
  Local Open Scope string.

Evaluation Semantics

  Section Evaluation.


    Fixpoint nnrs_imp_expr_eval
             (σc:bindings) (σ:pd_bindings) (e:nnrs_imp_expr)
    : option data
      := match e with
         | NNRSimpGetConstant v =>
           edot σc v

         | NNRSimpVar v =>
           olift id (lookup equiv_dec σ v)

         | NNRSimpConst d =>
           Some (normalize_data h d)

         | NNRSimpBinop bop e₁ e₂ =>
           olift2 (fun d₁ d₂ => binary_op_eval h bop d₁ d₂)
                  (nnrs_imp_expr_eval σc σ e₁)
                  (nnrs_imp_expr_eval σc σ e₂)

         | NNRSimpUnop uop e =>
           olift (fun d => unary_op_eval h uop d)
                 (nnrs_imp_expr_eval σc σ e)

         | NNRSimpGroupBy g sl e =>
           match nnrs_imp_expr_eval σc σ e with
           | Some (dcoll dl) => lift dcoll (group_by_nested_eval_table g sl dl)
           | _ => None
           end
         end.

    Fixpoint nnrs_imp_stmt_eval
             (σc:bindings) (s:nnrs_imp_stmt)
             (σ:pd_bindings) : option (pd_bindings)
      := match s with
         | NNRSimpSkip => Some σ
         | NNRSimpSeq s₁ s₂ =>
           olift (nnrs_imp_stmt_eval σc s₂)
                 (nnrs_imp_stmt_eval σc s₁ σ)
                 
         | NNRSimpAssign v e =>
           match nnrs_imp_expr_eval σc σ e, lookup string_dec σ v with
           | Some d, Some _ => Some (update_first string_dec σ v (Some d))
           | _, _ => None
           end
             
         | NNRSimpLet v eo s₀ =>
           let evals := (fun init =>
                           match nnrs_imp_stmt_eval σc s₀ ((v,init)::σ) with
                           | Some (_::σ') => Some σ'
                           | _ => None
                           end) in
           match eo with
           | Some e => olift evals (lift Some (nnrs_imp_expr_eval σc σ e))
           | None => evals None
           end
             
         | NNRSimpFor v e s₀ =>
           match nnrs_imp_expr_eval σc σ e with
           | Some (dcoll c1) =>
             let fix for_fun (dl:list data) σ₁ :=
                 match dl with
                 | nil => Some σ₁
                 | d::dl' =>
                   match nnrs_imp_stmt_eval σc s₀ ((v,Some d)::σ₁) with
                   | Some (_::σ₂) => for_fun dl' σ₂
                   | _ => None
                   end
                 end in
             for_fun c1 σ
           | _ => None
           end

         | NNRSimpIf e s₁ s₂ =>
           match nnrs_imp_expr_eval σc σ e with
           | Some (dbool true) => nnrs_imp_stmt_eval σc s₁ σ
           | Some (dbool false) => nnrs_imp_stmt_eval σc s₂ σ
           | _ => None
           end

         | NNRSimpEither e x₁ s₁ x₂ s₂ =>
           match nnrs_imp_expr_eval σc σ e with
           | Some (dleft d) =>
             match nnrs_imp_stmt_eval σc s₁ ((x₁,Some d)::σ) with
             | Some (_::σ₂) => Some σ₂
             | _ => None
             end
           | Some (dright d) =>
             match nnrs_imp_stmt_eval σc s₂ ((x₂,Some d)::σ) with
             | Some (_::σ₂) => Some σ₂
             | _ => None
             end
           | _ => None
           end
         end.

    Definition nnrs_imp_eval σc (q:nnrs_imp) : option (option data) :=
      let (s, ret) := q in
      match nnrs_imp_stmt_eval σc s ((ret, None)::nil) with
      | Some ((_,o)::_) => Some o
      | _ => None
      end.

    Definition nnrs_imp_eval_top σc (q:nnrs_imp) :=
      olift id (nnrs_imp_eval (rec_sort σc) q).

  End Evaluation.

  Section Core.
    Program Definition nnrs_imp_core_eval σc (q:nnrs_imp_core)
      := nnrs_imp_eval σc q.

    Program Definition nnrs_imp_core_eval_top σc (q:nnrs_imp_core)
      := olift id (nnrs_imp_core_eval (rec_sort σc) q).
    
  End Core.

  Section props.

    Ltac destr H :=
      let eqq := fresh "eqq" in
      first [
          match goal with
            [H: _ * _ |- _ ] => destruct H
          end |
          (match_case_in H;
           [intros [???] eqq | intros eqq]; rewrite eqq in H; try discriminate)
          | (match_case_in H;
             [intros [??] eqq | intros eqq]; rewrite eqq in H; try discriminate)
          | (match_case_in H;
             [intros ?? eqq | intros eqq]; rewrite eqq in H; try discriminate)
          | (match_case_in H;
             [intros ? eqq | intros eqq]; rewrite eqq in H; try discriminate)
          | (match_case_in H;
             [intros eqq | intros ? ? eqq]; try rewrite eqq in H; try discriminate)
          | (match_case_in H;
             [intros eqq | intros ? eqq]; try rewrite eqq in H; try discriminate)
        ]; subst.

    Instance preserves_some_pre {A} :
      PreOrder (fun x y: option A => x <> None -> y <> None).
    
    Lemma nnrs_imp_stmt_eval_preserves_some {s σc σ₁ σ₂} :
      nnrs_imp_stmt_eval σc s σ₁ = Some σ₂ ->
      Forall2 (fun x y => x <> None -> y <> None) (codomain σ₁) (codomain σ₂).
    
    Lemma nnrs_imp_stmt_eval_domain_stack {s σc σ₁ σ₂} :
      nnrs_imp_stmt_eval σc s σ₁ = Some σ₂ -> domain σ₁ = domain σ₂.

    Lemma nnrs_imp_stmt_eval_lookup_some_some {σc s σ σ' }:
      nnrs_imp_stmt_eval σc s σ = Some σ' ->
      forall x d,
        lookup equiv_dec σ x = Some (Some d) ->
        exists o : data, lookup equiv_dec σ' x = Some (Some o).

    Local Open Scope list.


    Ltac disect_tac H stac
      :=
        unfold var in *
        ; cut_to H; unfold domain in *; [ | solve[stac]..]
        ; unfold lift2P in H
        ; (repeat match_option_in H; try contradiction).

    Ltac pcong
      := solve[repeat (match goal with
                       | [H: _ = _ |- _ ] => rewrite H in *; clear H
                       end; try tauto)].

    Ltac fuse_t stac
      := repeat progress (
                  repeat rewrite in_app_iff in *
                  ; repeat
                      match goal with
                      | [H : ~ (_ \/ _ ) |- _ ] => apply not_or in H
                      | [H : (_ \/ _ ) -> False |- _ ] => apply not_or in H
                      | [H: _ /\ _ |- _ ] => destruct H
                      | [ H : _ * _ |- _ ] => destruct H
                      | [H: _::_ = _::_ |- _ ] => invcs H
                      | [ H: domain (_ ++ _) = domain _ |- _ ] =>
                        rewrite domain_app in H
                        ; unfold domain in H
                        ; symmetry in H; apply map_app_break in H
                        ; destruct H as [? [?[?[??]]]]; subst; simpl in *
                      | [ H: map (_ ++ _) = map _ |- _ ] =>
                        rewrite map_app in H
                        ; symmetry in H; apply map_app_break in H
                        ; destruct H as [? [?[?[??]]]]; subst; simpl in *
                      | [ H: _ :: _ = map _ ?x |- _ ] =>
                        destruct x; try discriminate; simpl in H; invcs H
                      | [ H: _ :: _ = domain ?x |- _ ] =>
                        destruct x; try discriminate; simpl in H; invcs H
                      | [H : ~ In _ (remove _ _ _) |- _ ] =>
                        apply not_in_remove_impl_not_in in H; [| congruence]
                      | [H : ?x ++ _ = ?y ++ _ |- _ ] =>
                        let HH := fresh in
                        assert (HH:domain y = domain x) by
                            (unfold domain in *;
                             try (intuition congruence)
                             ; pcong)
                        ; apply app_inv_head_domain in H;[clear HH|apply HH]

                      | [H : nnrs_imp_stmt_eval _ _ _ ?p1 = ?p2 |- _ ] =>
                        apply nnrs_imp_stmt_eval_domain_stack in H

                      | [ H: forall a b c, _ -> ?x1 :: ?dd :: ?x2 = _ ++ _ :: _ -> _ |- _] =>
                        specialize (H (x1::nil) (snd dd) x2); simpl in H
                        ; match dd with
                          | (_,_) => idtac
                          | _ => destruct dd
                          end
                        ; simpl in *
                        ; cut_to H; [ | eauto 3 | reflexivity]
                      end
                  ; simpl in *; trivial; intros; try subst; try contradiction; try solve [congruence | f_equal; congruence]).

    Ltac fuse_tt := fuse_t ltac:(try tauto; try congruence).

    Lemma nnrs_imp_stmt_eval_lookup_preserves_unwritten {σc s} l l' σ σ' :
      nnrs_imp_stmt_eval σc s (l++σ) = Some (l'++σ') ->
      domain l = domain l' ->
      forall x,
        In x (domain l) \/ ~ In x (nnrs_imp_stmt_maybewritten_vars s) ->
        lookup equiv_dec σ x = lookup equiv_dec σ' x.

    Lemma nnrs_imp_expr_eval_same σc pd₁ pd₂ s :
      lookup_equiv_on (nnrs_imp_expr_free_vars s) pd₁ pd₂ ->
      nnrs_imp_expr_eval σc pd₁ s = nnrs_imp_expr_eval σc pd₂ s.

    Lemma nnrs_imp_expr_eval_group_by_unfold σc σ g sl e :
      nnrs_imp_expr_eval σc σ (NNRSimpGroupBy g sl e) =
      match nnrs_imp_expr_eval σc σ e with
      | Some (dcoll dl) => lift dcoll (group_by_nested_eval_table g sl dl)
      | _ => None
      end.

    Global Instance nnrs_imp_expr_eval_proper
      : Proper (eq ==> lookup_equiv ==> eq ==> eq) nnrs_imp_expr_eval.

  End props.

  Section eval_eqs.

    Local Close Scope string.

    Lemma nnrs_imp_expr_eval_free σc (l1 l2 l3:pd_bindings) e :
      disjoint (nnrs_imp_expr_free_vars e) (domain l2) ->
      nnrs_imp_expr_eval σc (l1 ++ l2 ++ l3) e
      =
      nnrs_imp_expr_eval σc (l1 ++ l3) e.

    Lemma nnrs_imp_expr_eval_free_tail σc (l1 l2:pd_bindings) e :
      disjoint (nnrs_imp_expr_free_vars e) (domain l2) ->
      nnrs_imp_expr_eval σc (l1 ++ l2) e
      =
      nnrs_imp_expr_eval σc l1 e.
    
    Lemma nnrs_imp_expr_eval_unused c l σ e v d :
      (In v (domain l)
       \/ ~ In v (nnrs_imp_expr_free_vars e)) ->
      nnrs_imp_expr_eval c (l ++ (v, d) :: σ) e
      = nnrs_imp_expr_eval c (l ++ σ) e.

    Section swap.
      
      Lemma nnrs_imp_expr_eval_swap c l σ e v₁ v₂ d₁ d₂:
        v₁ <> v₂ ->
        nnrs_imp_expr_eval c (l++(v₁,d₁)::(v₂,d₂)::σ) e =
        nnrs_imp_expr_eval c (l++(v₂,d₂)::(v₁,d₁)::σ) e.

      Lemma nnrs_imp_stmt_eval_swap c l σ s v₁ v₂ d₁ d₂:
        v₁ <> v₂ ->
        lift2P
          (fun σ₁' σ₂' =>
             (forall l' d₁' d₂' σ'',
                 domain l' = domain l ->
                 σ₁' = l' ++ (v₁,d₁')::(v₂,d₂')::σ'' ->
                 σ₂' = l' ++ (v₂,d₂')::(v₁,d₁')::σ'')
          )
          (nnrs_imp_stmt_eval c s (l++(v₁,d₁)::(v₂,d₂)::σ))
          (nnrs_imp_stmt_eval c s (l++(v₂,d₂)::(v₁,d₁)::σ)).
      
    End swap.

    Section unused.

      
      Ltac disect_tac H stac
        :=
          unfold var in *
          ; cut_to H; unfold domain in *; [ | solve[stac]..]
          ; unfold lift2P in H
          ; (repeat match_option_in H; try contradiction).

      Ltac unused_eval_t stac
        := repeat progress (
                    intros
                    ; repeat rewrite in_app_iff in *
                    ; repeat
                        match goal with
                        | [H : ~ (_ \/ _ ) |- _ ] => apply not_or in H
                        | [H : (_ \/ _ ) -> False |- _ ] => apply not_or in H
                        | [H: _ /\ _ |- _ ] => destruct H
                        | [ H : _ * _ |- _ ] => destruct H
                        | [H: _::_ = _::_ |- _ ] => invcs H
                        | [ H: domain (_ ++ _) = domain _ |- _ ] =>
                          rewrite domain_app in H
                          ; unfold domain in H
                          ; symmetry in H; apply map_app_break in H
                          ; destruct H as [? [?[?[??]]]]; subst; simpl in *
                        | [ H: map (_ ++ _) = map _ |- _ ] =>
                          rewrite map_app in H
                          ; symmetry in H; apply map_app_break in H
                          ; destruct H as [? [?[?[??]]]]; subst; simpl in *
                        | [ H: _ :: _ = map _ ?x |- _ ] =>
                          destruct x; try discriminate; simpl in H; invcs H
                        | [ H: _ :: _ = domain ?x |- _ ] =>
                          destruct x; try discriminate; simpl in H; invcs H
                        | [H : ~ In _ (remove _ _ _) |- _ ] =>
                          apply not_in_remove_impl_not_in in H; [| congruence]
                        | [H : ?x ++ _ = ?y ++ _ |- _ ] =>
                          let HH := fresh in
                          assert (HH:domain y = domain x) by (unfold domain in *; intuition congruence)
                          ; apply app_inv_head_domain in H;[clear HH|apply HH]
                                                             

                        | [ H: forall a b c, _ -> ?x1 ++ ?dd :: ?x2 = _ ++ _ :: _ -> _ |- _] =>
                          specialize (H x1 (snd dd) x2); simpl in H
                          ; match dd with
                            | (_,_) => idtac
                            | _ => destruct dd
                            end
                          ; simpl in *
                          ; cut_to H; [ | eauto 3 | reflexivity]
                        | [ H: forall a b c, _ -> ?dd0::?x1 ++ ?dd :: ?x2 = _ ++ _ :: _ -> _ |- _] =>
                          specialize (H (dd0::x1) (snd dd) x2); simpl in H
                          ; match dd with
                            | (_,_) => idtac
                            | _ => destruct dd
                            end
                          ; simpl in *
                          ; cut_to H; [ | eauto 3 | reflexivity]

                                        
                        | [H : nnrs_imp_stmt_eval _ _ ?p1 = ?p2 |- _ ] =>
                          match p1 with
                          | p2 => fail 1
                          | _ => apply nnrs_imp_stmt_eval_domain_stack in H
                          end
                        | [H:forall l σ d,
                              _ -> _ -> _ -> _ -> lift2P _ (nnrs_imp_stmt_eval _ ?s _) _
                                                         
                              |- lift2P _ (olift _ (nnrs_imp_stmt_eval _ ?s (?l ++ (_, ?d) :: ?σ) ))
                                        _ ] =>
                          specialize (H l σ d)
                          ; disect_tac H stac
                        | [H:forall l σ d,
                              _ -> _ -> _ -> _ -> lift2P _ (nnrs_imp_stmt_eval _ ?s _) _
                                                         
                              |- lift2P _ (nnrs_imp_stmt_eval _ ?s (?l ++ (_, ?d) :: ?σ) )
                                        _ ] =>
                          specialize (H l σ d)
                          ; disect_tac H stac
                        | [H:forall l σ d,
                              _ -> _ -> _ -> _ -> lift2P _ (nnrs_imp_stmt_eval _ ?s _) _
                                                         
                              |- lift2P _ (match nnrs_imp_stmt_eval _ ?s (?x::?l ++ (_, ?d) :: ?σ)
                                           with | Some _ => _ | None => _ end)
                                        _ ] =>
                          specialize (H (x::l) σ d); simpl in H
                          ; disect_tac H stac
                        end; simpl in *; trivial; try tauto; try solve [try unfold domain in *; try congruence]).

      Ltac unused_eval_tt := unused_eval_t ltac:(try tauto; try congruence).

      Lemma nnrs_imp_stmt_eval_unused c l σ s v d:
        (In v (domain l) \/
         ~ In v (nnrs_imp_stmt_free_vars s)) ->
        lift2P
          (fun σ₁' σ₂' =>
             (forall l' d' σ'',
                 domain l' = domain l ->
                 σ₁' = l' ++ (v,d')::σ'' ->
                 σ₂' = l' ++ σ''
                 /\ d = d')
          )
          (nnrs_imp_stmt_eval c s (l++(v,d)::σ))
          (nnrs_imp_stmt_eval c s (l++σ)).

    End unused.

  End eval_eqs.

End NNRSimpEval.

Arguments nnrs_imp_stmt_eval_domain_stack {fruntime h s σc σ₁ σ₂}.
Arguments nnrs_imp_stmt_eval_preserves_some {fruntime h s σc σ₁ σ₂}.
Arguments nnrs_imp_stmt_eval_lookup_some_some {fruntime h σc s σ σ' }.
Arguments nnrs_imp_stmt_eval_lookup_preserves_unwritten {fruntime h σc s}.