Library CoLoR.Conversion.Coccinelle

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2008-02-22, 2009-10-20 (rpo)
convert CoLoR terms into Coccinelle terms

Set Implicit Arguments.


convert a CoLoR signature into a Coccinelle signature


Module Make_Signature (Import S : SIG) <: Signature.
  Module Symb <: decidable_set.S.
    Definition A := symbol Sig.
    Definition eq_bool := @beq_symb Sig.
    Lemma eq_bool_ok : forall a1 a2,
      match eq_bool a1 a2 with true => a1 = a2 | false => ~ a1 = a2 end.
  End Symb.
  Definition arity (f : Sig) := Free (arity f).
End Make_Signature.

convert CoLoR variables to Coccinelle variables


Module Var <: decidable_set.S.
  Definition A := nat.
  Definition eq_bool := beq_nat.
  Lemma eq_bool_ok : forall a1 a2,
    match eq_bool a1 a2 with true => a1 = a2 | false => ~ a1 = a2 end.
End Var.

convert CoLoR terms into Coccinelle terms


Module Make_Term (Import S : SIG) <: Term.

  Notation aterm := (term Sig). Notation aterms := (vector aterm).
  Notation AVar := ATerm.Var.

  Module Sig := Make_Signature S.

  Include (term.Make' Sig Var).

  Fixpoint term_of_aterm (t : aterm) :=
    match t with
      | AVar x => Var x
      | Fun f ts =>
        let fix terms_of_aterms n (ts : aterms n) :=
          match ts with
            | Vnil => nil
            | Vcons u us => term_of_aterm u :: terms_of_aterms _ us
          end in Term f (terms_of_aterms (arity f) ts)
    end.

  Fixpoint terms_of_aterms n (ts : aterms n) :=
    match ts with
      | Vnil => nil
      | Vcons u us => term_of_aterm u :: terms_of_aterms us
    end.

  Lemma terms_of_aterms_eq : forall n (ts : aterms n),
    (fix terms_of_aterms n (ts : aterms n) :=
      match ts with
        | Vnil => nil
        | Vcons u us => term_of_aterm u :: terms_of_aterms _ us
      end) n ts = terms_of_aterms ts.

  Lemma term_of_aterm_fun : forall f ts,
    term_of_aterm (Fun f ts) = Term f (terms_of_aterms ts).

  Import VecUtil.

  Lemma terms_of_aterms_cast : forall n (ts : aterms n) p (e : n=p),
    terms_of_aterms (Vcast ts e) = terms_of_aterms ts.

  Lemma terms_of_aterms_app : forall n (ts : aterms n) p (us : aterms p),
    terms_of_aterms (Vapp ts us) = terms_of_aterms ts ++ terms_of_aterms us.

  Lemma length_terms_of_aterms : forall n (ts : aterms n),
    length (terms_of_aterms ts) = n.

  Fixpoint sub_of_asub (s : ASubstitution.substitution Sig) n :=
    match n with
      | 0 => nil
      | S n' => (n', term_of_aterm (s n')) :: sub_of_asub s n'
    end.

Import more_list.

Notation find := (@find _ eq_var_bool _).

  Lemma find_sub_of_asub : forall s n v, find v (sub_of_asub s n) =
    if bgt_nat n v then Some (term_of_aterm (s v)) else None.

  Lemma term_of_aterm_sub : forall s k t, k > maxvar t ->
    term_of_aterm (sub s t) = apply_subst (sub_of_asub s k) (term_of_aterm t).

  Import APosition AContext.

  Lemma term_of_aterm_fill : forall u t c, term_of_aterm (fill c t) =
    replace_at_pos (term_of_aterm (fill c u)) (term_of_aterm t) (pos_context c).

  Lemma is_a_pos_context : forall u c,
    is_a_pos (term_of_aterm (fill c u)) (pos_context c) = true.

End Make_Term.

module type for using Coccinelle's RPO


Module Type PRECEDENCE.
  Parameter Sig : Signature.
  Parameter status : Sig -> status_type.
  Parameter prec_nat : Sig -> nat.
  Parameter bb : nat.
  Parameter prec_eq_status :
    forall f g, prec_eq prec_nat f g -> status f = status g.
End PRECEDENCE.

convert Coccinelle RPO into a CoLoR WeakRedPair


Module WP_RPO (Import P : PRECEDENCE) <: WeakRedPair.

  Definition Prec := Precedence status prec_nat prec_eq_status.

  Module S. Definition Sig := Sig. End S.

  Module Import Term := Make_Term S.

  Module Import Rpo := rpo.Make Term.

  Notation rpo := (rpo Prec P.bb).

  Definition Sig := Sig.
  Definition succ := transp (Rof rpo term_of_aterm).

  Import Inverse_Image.

  Lemma wf_succ : WF succ.

  Import Max.

  Lemma sc_succ : substitution_closed succ.

  Notation empty_rpo_infos := (empty_rpo_infos Prec P.bb).
  Notation rpo_eval := (rpo_eval empty_rpo_infos P.bb).
  Notation rpo_eval_is_sound := (rpo_eval_is_sound_weak empty_rpo_infos P.bb).

  Import ordered_set.

  Definition bsucc t u :=
    match rpo_eval (term_of_aterm t) (term_of_aterm u) with
      | Some Greater_than => true
      | _ => false
    end.

  Lemma bsucc_ok : forall t u, bsucc t u = true -> succ t u.

  Lemma bsucc_sub : rel_of_bool bsucc << succ.

  Definition equiv_aterm := Rof (equiv Prec) term_of_aterm.

  Definition succeq := succ U equiv_aterm.

  Lemma sc_succeq : substitution_closed succeq.

  Lemma cc_succ : context_closed succ.

  Lemma cc_equiv_aterm : context_closed equiv_aterm.

  Lemma cc_succeq : context_closed succeq.

  Lemma refl_succeq : reflexive succeq.

  Lemma succ_succeq_compat : absorbs_left succ succeq.

  Definition bsucceq t u :=
    match rpo_eval (term_of_aterm t) (term_of_aterm u) with
      | Some Greater_than | Some Equivalent => true
      | _ => false
    end.

  Lemma bsucceq_ok : forall t u, bsucceq t u = true -> succeq t u.

  Definition bsucceq_sub : rel_of_bool bsucceq << succeq.


  Lemma trans_succ : transitive succ.

  Lemma trans_equiv_aterm : transitive equiv_aterm.

  Lemma trans_succeq : transitive succeq.

End WP_RPO.

decide compatibility of statuses wrt precedences

Definition beq_status s1 s2 :=
  match s1, s2 with
    | Lex, Lex
    | Mul, Mul => true
    | _, _ => false
  end.

Lemma beq_status_ok : forall s1 s2, beq_status s1 s2 = true <-> s1 = s2.

Section prec_eq_status.

  Variables (Sig : Signature) (status : Sig -> status_type)
    (prec_nat : Sig -> nat).

  Lemma prec_eq_ok : forall f g,
    prec_eq_bool prec_nat f g = true <-> prec_eq prec_nat f g.

  Definition bprec_eq_status_symb f g :=
    implb (prec_eq_bool prec_nat f g) (beq_status (status f) (status g)).

  Lemma bprec_eq_status_symb_ok : forall f g,
    bprec_eq_status_symb f g = true
    <-> (prec_eq prec_nat f g -> status f = status g).

  Section bprec_eq_status_aux1.

    Variable f : Sig.

    Fixpoint bprec_eq_status_aux1 b gs :=
      match gs with
        | nil => b
        | g :: gs' => bprec_eq_status_aux1 (b && bprec_eq_status_symb f g) gs'
      end.

    Lemma bprec_eq_status_aux1_true : forall gs b,
      bprec_eq_status_aux1 b gs = true -> b = true.


    Lemma bprec_eq_status_aux1_ok : forall gs b,
      bprec_eq_status_aux1 b gs = true ->
      forall g, In g gs -> prec_eq prec_nat f g -> status f = status g.

  End bprec_eq_status_aux1.


  Fixpoint bprec_eq_status_aux2 b fs :=
    match fs with
      | nil => b
      | f :: fs' => bprec_eq_status_aux2 (bprec_eq_status_aux1 f b fs') fs'
    end.

  Lemma bprec_eq_status_aux2_true : forall fs b,
    bprec_eq_status_aux2 b fs = true -> b = true.


  Lemma bprec_eq_status_aux2_ok : forall fs b,
    bprec_eq_status_aux2 b fs = true -> forall f g, In f fs -> In g fs ->
      prec_eq prec_nat f g -> status f = status g.

  Definition bprec_eq_status := bprec_eq_status_aux2 true.

  Variable (Fs : list Sig) (Fs_ok : forall f, In f Fs).

  Lemma bprec_eq_status_ok : bprec_eq_status Fs = true ->
    forall f g, prec_eq prec_nat f g -> status f = status g.

End prec_eq_status.


Ltac prec_eq_status s p o := apply (bprec_eq_status_ok s p o); check_eq
  || fail 10 "statuses incompatible with precedences".