# 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".