Module ObcSyntax

From Velus Require Import Common.
From Velus Require Import Operators.

Open Scope bool_scope.
From Coq Require Import List.
Import List.ListNotations.
Open Scope list_scope.

Obc syntax



Module Type OBCSYNTAX
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op).

  Inductive exp : Type :=
  | Var : ident -> type -> exp
  | State : ident -> type -> exp
  | Const : const-> exp
  | Unop : unop -> exp -> type -> exp
  | Binop : binop -> exp -> exp -> type -> exp
  | Valid : ident -> type -> exp.

  Fixpoint typeof (e: exp): type :=
    match e with
    | Const c => type_const c
    | Var _ ty
    | State _ ty
    | Unop _ _ ty
    | Binop _ _ _ ty
    | Valid _ ty => ty
    end.

  Inductive stmt : Type :=
  | Assign : ident -> exp -> stmt
  | AssignSt : ident -> exp -> stmt
  | Ifte : exp -> stmt -> stmt -> stmt
  | Comp : stmt -> stmt -> stmt
  | Call : list ident -> ident -> ident -> ident -> list exp -> stmt
  | Skip.

  Record method : Type :=
    mk_method {
        m_name : ident;
        m_in : list (ident * type);
        m_vars : list (ident * type);
        m_out : list (ident * type);
        m_body : stmt;

        m_nodupvars : NoDupMembers (m_in ++ m_vars ++ m_out);
        m_good : Forall (AtomOrGensym (PSP.of_list gensym_prefs)) (map fst (m_in ++ m_vars ++ m_out)) /\
                      atom m_name
      }.

  Definition meth_vars m := m.(m_in) ++ m.(m_vars) ++ m.(m_out).
  Hint Resolve m_nodupvars.

  Lemma m_nodupout:
    forall f, NoDupMembers (m_out f).
Proof.
    intro; pose proof (m_nodupvars f) as Nodup;
    now repeat apply NoDupMembers_app_r in Nodup.
  Qed.

  Lemma m_nodupin:
    forall f, NoDupMembers (m_in f).
Proof.
    intro; pose proof (m_nodupvars f) as Nodup;
    now apply NoDupMembers_app_l in Nodup.
  Qed.

  Lemma m_nodupvars':
    forall f, NoDupMembers (m_vars f).
Proof.
    intro; pose proof (m_nodupvars f) as Nodup;
    now apply NoDupMembers_app_r, NoDupMembers_app_l in Nodup.
  Qed.

  Remark In_meth_vars_out:
    forall f x ty,
      InMembers x f.(m_out) ->
      In (x, ty) (meth_vars f) ->
      In (x, ty) f.(m_out).
Proof.
    intros * E ?.
    pose proof (m_nodupvars f) as Nodup.
    apply InMembers_In in E as (ty' &?).
    assert (In (x, ty') (meth_vars f))
      by (now apply in_or_app; right; apply in_or_app; right).
    now app_NoDupMembers_det.
  Qed.

  Lemma m_good_out:
    forall m x,
      In x m.(m_out) ->
      AtomOrGensym (PSP.of_list gensym_prefs) (fst x).
Proof.
    intros.
    pose proof (m_good m) as (G&_).
    eapply Forall_forall; eauto.
    apply in_map, in_app; right; apply in_app; now right.
  Qed.

  Lemma m_good_in:
    forall m x,
      In x m.(m_in) ->
      AtomOrGensym (PSP.of_list gensym_prefs) (fst x).
Proof.
    intros.
    pose proof (m_good m) as (G&_).
    eapply Forall_forall; eauto.
    apply in_map, in_app; now left.
  Qed.

  Lemma m_good_vars:
    forall m x,
      In x m.(m_vars) ->
      AtomOrGensym (PSP.of_list gensym_prefs) (fst x).
Proof.
    intros.
    pose proof (m_good m) as (G&_).
    eapply Forall_forall; eauto.
    apply in_map, in_app; right; apply in_app; now left.
  Qed.

  Lemma m_AtomOrGensym :
    forall x m,
      InMembers x (meth_vars m) ->
      AtomOrGensym (PSP.of_list gensym_prefs) x.
Proof.
    intros * Hinm.
    pose proof m.(m_good) as (Good&_).
    eapply fst_InMembers in Hinm.
    eapply Forall_forall in Good; eauto.
  Qed.

  Record class : Type :=
    mk_class {
        c_name : ident;
        c_mems : list (ident * type);
        c_objs : list (ident * ident);
        c_methods : list method;

        c_nodup : NoDup (map fst c_mems ++ map fst c_objs);
        c_nodupm : NoDup (map m_name c_methods);
        c_good : Forall (AtomOrGensym (PSP.of_list gensym_prefs)) (map fst c_objs) /\ atom c_name
      }.

  Lemma c_nodupmems:
    forall c, NoDupMembers (c_mems c).
Proof.
    intro.
    pose proof (c_nodup c) as Nodup.
    apply NoDup_app_weaken in Nodup.
    now rewrite fst_NoDupMembers.
  Qed.

  Lemma c_nodupobjs:
    forall c, NoDupMembers (c_objs c).
Proof.
    intro.
    pose proof (c_nodup c) as Nodup.
    rewrite Permutation.Permutation_app_comm in Nodup.
    apply NoDup_app_weaken in Nodup.
    now rewrite fst_NoDupMembers.
  Qed.

  Definition program : Type := list class.

  Definition find_method (f: ident): list method -> option method :=
    fix find ms := match ms with
                   | [] => None
                   | m :: ms' => if ident_eqb m.(m_name) f
                                then Some m else find ms'
                   end.

  Definition find_class (n: ident) : program -> option (class * list class) :=
    fix find p := match p with
                  | [] => None
                  | c :: p' => if ident_eqb c.(c_name) n
                              then Some (c, p') else find p'
                  end.

  Definition Forall_methods P p :=
    Forall (fun c => Forall P c.(c_methods)) p.

Properties of method lookups

  Remark find_method_In:
    forall fid ms f,
      find_method fid ms = Some f ->
      In f ms.
Proof.
    intros * Hfind.
    induction ms; inversion Hfind as [H].
    destruct (ident_eqb (m_name a) fid) eqn: E.
    - inversion H; subst.
      apply in_eq.
    - auto using in_cons.
  Qed.

  Remark find_method_name:
    forall fid fs f,
      find_method fid fs = Some f ->
      f.(m_name) = fid.
Proof.
    intros * Hfind.
    induction fs; inversion Hfind as [H].
    destruct (ident_eqb (m_name a) fid) eqn: E.
    - inversion H; subst.
      now apply ident_eqb_eq.
    - now apply IHfs.
  Qed.

  Lemma find_method_map:
    forall f,
      (forall m, (f m).(m_name) = m.(m_name)) ->
      forall n ms,
        find_method n (map f ms) = option_map f (find_method n ms).
Proof.
    intros f Hfname.
    induction ms as [|m ms IH]; auto. simpl.
    destruct (ident_eqb (f m).(m_name) n) eqn:Heq;
      rewrite Hfname in Heq; rewrite Heq; auto.
  Qed.

Properties of class lookups

  Lemma find_class_none:
    forall clsnm cls prog,
      find_class clsnm (cls::prog) = None
      <-> (cls.(c_name) <> clsnm /\ find_class clsnm prog = None).
Proof.
    intros clsnm cls prog.
    simpl; destruct (ident_eqb (c_name cls) clsnm) eqn: E.
    - split; intro HH; try discriminate.
      destruct HH.
      apply ident_eqb_eq in E; contradiction.
    - apply ident_eqb_neq in E; split; intro HH; tauto.
  Qed.

  Remark find_class_app:
    forall id cls c cls',
      find_class id cls = Some (c, cls') ->
      exists cls'',
        cls = cls'' ++ c :: cls'
        /\ find_class id cls'' = None.
Proof.
    intros * Hfind.
    induction cls; inversion Hfind as [H].
    destruct (ident_eqb (c_name a) id) eqn: E.
    - inversion H; subst.
      exists nil; auto.
    - specialize (IHcls H).
      destruct IHcls as (cls'' & Hcls'' & Hnone).
      rewrite Hcls''.
      exists (a :: cls''); split; auto.
      simpl; rewrite E; auto.
  Qed.

  Remark find_class_name:
    forall id cls c cls',
      find_class id cls = Some (c, cls') ->
      c.(c_name) = id.
Proof.
    intros * Hfind.
    induction cls; inversion Hfind as [H].
    destruct (ident_eqb (c_name a) id) eqn: E.
    - inversion H; subst.
      now apply ident_eqb_eq.
    - now apply IHcls.
  Qed.

  Remark find_class_In:
    forall id cls c cls',
      find_class id cls = Some (c, cls') ->
      In c cls.
Proof.
    intros * Hfind.
    induction cls; inversion Hfind as [H].
    destruct (ident_eqb (c_name a) id) eqn: E.
    - inversion H; subst.
      apply in_eq.
    - apply in_cons; auto.
  Qed.

  Lemma find_class_app':
    forall n xs ys,
      find_class n (xs ++ ys) = match find_class n xs with
                                 | None => find_class n ys
                                 | Some (c, prog) => Some (c, prog ++ ys)
                                 end.
Proof.
    induction xs as [|c xs IH]; simpl; auto.
    intro ys.
    destruct (ident_eqb c.(c_name) n); auto.
  Qed.

  Lemma not_In_find_class:
    forall n prog,
      ~In n (map c_name prog) ->
      find_class n prog = None.
Proof.
    induction prog as [|c prog IH]; auto.
    simpl; intro Hnin.
    apply Decidable.not_or in Hnin.
    destruct Hnin as (Hnin1 & Hnin2).
    rewrite (IH Hnin2).
    apply ident_eqb_neq in Hnin1.
    now rewrite Hnin1.
  Qed.

  Lemma find_class_ltsuffix:
    forall n prog c prog',
      find_class n prog = Some (c, prog') ->
      ltsuffix prog' prog.
Proof.
    induction prog as [|c prog IH]. now inversion 1.
    red; simpl. intros c' prog' Hfind.
    destruct (ident_eqb c.(c_name) n).
    - inv Hfind.
      exists [c']. simpl; split; auto; discriminate.
    - destruct (IH _ _ Hfind) as (xs & Hprog & Hxs). subst.
      exists (c::xs); simpl; split; auto; discriminate.
  Qed.

  Lemma find_class_ltsuffix2:
    forall n prog1 prog2 c1 c2 prog1' prog2',
      find_class n prog1 = Some (c1, prog1') ->
      find_class n prog2 = Some (c2, prog2') ->
      ltsuffix2 (prog1', prog2') (prog1, prog2).
Proof.
    split; eauto using find_class_ltsuffix.
  Qed.

  Lemma Forall_methods_find:
    forall prog P cid c prog' fid f,
      Forall_methods P prog ->
      find_class cid prog = Some (c, prog') ->
      find_method fid c.(c_methods) = Some f ->
      P f.
Proof.
    unfold Forall_methods; intros * Spec Findc Findf.
    apply find_class_In in Findc.
    apply find_method_In in Findf.
    do 2 eapply Forall_forall in Spec; eauto.
  Qed.

Syntactic predicates

  Inductive Is_free_in_exp : ident -> exp -> Prop :=
  | FreeVar: forall i ty,
      Is_free_in_exp i (Var i ty)
  | FreeState: forall i ty,
      Is_free_in_exp i (State i ty)
  | FreeUnop: forall i op e ty,
      Is_free_in_exp i e ->
      Is_free_in_exp i (Unop op e ty)
  | FreeBinop: forall i op e1 e2 ty,
      Is_free_in_exp i e1 \/ Is_free_in_exp i e2 ->
      Is_free_in_exp i (Binop op e1 e2 ty)
  | FreeValid: forall i t,
      Is_free_in_exp i (Valid i t).

  Lemma not_free_aux1 : forall i op e ty,
      ~Is_free_in_exp i (Unop op e ty) ->
      ~Is_free_in_exp i e.
Proof.
    auto using Is_free_in_exp.
  Qed.

  Lemma not_free_aux2 : forall i op e1 e2 ty,
      ~Is_free_in_exp i (Binop op e1 e2 ty) ->
      ~Is_free_in_exp i e1 /\ ~Is_free_in_exp i e2.
Proof.
    intros i op e1 e2 ty Hfree; split; intro H; apply Hfree;
      constructor; [now left | now right].
  Qed.

  Ltac not_free :=
    lazymatch goal with
    | H : ~Is_free_in_exp ?x (Var ?i ?ty) |- _ =>
        let HH := fresh in
        assert (HH : i <> x) by (intro; subst; apply H; constructor);
        clear H; rename HH into H
    | H : ~Is_free_in_exp ?x (State ?i ?ty) |- _ =>
        let HH := fresh in
        assert (HH : i <> x) by (intro; subst; apply H; constructor);
        clear H; rename HH into H
    | H : ~Is_free_in_exp ?x (Valid ?i ?ty) |- _ =>
        let HH := fresh in
        assert (HH : i <> x) by (intro; subst; apply H; constructor);
        clear H; rename HH into H
    | H : ~Is_free_in_exp ?x (Unop ?op ?e ?ty) |- _ =>
        apply not_free_aux1 in H
    | H : ~Is_free_in_exp ?x (Binop ?op ?e1 ?e2 ?ty) |- _ =>
        destruct (not_free_aux2 x op e1 e2 ty H)
    end.

Misc. properties

  Lemma exp_dec : forall e1 e2 : exp, {e1 = e2} + {e1 <> e2}.
Proof.
    decide equality;
    try apply equiv_dec.
  Qed.

  Instance: EqDec exp eq := { equiv_dec := exp_dec }.

End OBCSYNTAX.

Module ObcSyntaxFun
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (Import OpAux : OPERATORS_AUX Op) <: OBCSYNTAX Ids Op OpAux.
  Include OBCSYNTAX Ids Op OpAux.
End ObcSyntaxFun.
Generated by coq2html