octalgo.octalgo.occurrences


Require Import syntax.


Require Import bigop_aux.
Require Import utils.
Require Import finseqs.

Set Implicit Arguments.

Occurrences of atoms or terms

Section occurrences.

Section t_occ.

Variable p : program.

Atom occurrence

occ is a pair representing a position in a program. (occ x y) is the yth atom in the body of the xth clause of the program
Definition occ := ('I_(size p) × 'I_bn)%type.

Term occurrence

a term occurrence is a triple made of a clause position in the program, atom position in the body of the clause and term position in the atom
Record t_occ := T_occ {r_ind : 'I_(size p) ; b_ind : 'I_bn ; t_ind : 'I_max_ar}.

Type for the representation of t_occ
Definition tocc_countprod := prod_countType (prod_countType (ordinal_countType (size p)) (ordinal_countType bn)) (ordinal_countType max_ar).

Representation and cancellation lemma for t_occ
Definition t_occ_rep (a : t_occ) : tocc_countprod :=
  let: T_occ b c d := a in (b,c,d).
Definition t_occ_pre (a : tocc_countprod) :=
  let: (b,c,d) := a in T_occ b c d.

Lemma prod_of_t_occK : cancel t_occ_rep t_occ_pre.

t_occ is a finite type
Definition t_occ_eqMixin :=
  CanEqMixin prod_of_t_occK.
Canonical t_occ_eqType :=
  Eval hnf in EqType t_occ t_occ_eqMixin.
Definition t_occ_choiceMixin :=
  CanChoiceMixin prod_of_t_occK.
Canonical t_occ_choiceType :=
  Eval hnf in ChoiceType t_occ t_occ_choiceMixin.
Definition t_occ_countMixin :=
  (@CanCountMixin tocc_countprod _ t_occ_rep t_occ_pre prod_of_t_occK).
Canonical t_occ_countType :=
  Eval hnf in CountType t_occ t_occ_countMixin.
Definition t_occ_finMixin :=
  CanFinMixin prod_of_t_occK.
Canonical t_occ_finType :=
  Eval hnf in FinType t_occ t_occ_finMixin.

Accessing the atom matching a given t_occ
Definition at_at (o : t_occ) : option atom :=
  match nth_error p (r_ind o) with
    | None ⇒ None
    | Some cl ⇒ nth_error (body_cl cl) (b_ind o) end.

Accessing the term matching a given t_occ
Definition t_at (o : t_occ) : option term.
Defined.

Accessing the predicate matching a given t_occ
Definition p_at (t : t_occ) := match (at_at t) with
  | None ⇒ None
  | Some ato ⇒ Some (sym_atom ato) end.

If t_at returns a variable, it an actual var of a clause.
Lemma t_at_vars_in (tocc : t_occ) v cl :
    t_at tocc = Some (Var v)
  → Some cl = nth_error p (r_ind tocc)
  → v \in tail_vars (body_cl cl).

End t_occ.

Section a_occ.

Variable p : program.

Atom occurrence

an atom occurrence is a couple made of a clause position in the program and atom position in the body of the clause
Record a_occ := A_occ {ar_ind : 'I_(size p) ; ab_ind : 'I_bn}.

Extract the atom occurence from the term occurence
Definition atom_occ (t : t_occ p) := A_occ (r_ind t) (b_ind t).

Type for the representation of t_occ
Definition aocc_countprod := prod_countType (ordinal_countType (size p)) (ordinal_countType bn).

Representation and cancellation lemma for t_occ
Definition a_occ_rep (a : a_occ) : aocc_countprod :=
  let: A_occ b c := a in (b,c).
Definition a_occ_pre (a : aocc_countprod) :=
  let: (b,c) := a in A_occ b c.

Lemma prod_of_a_occK : cancel a_occ_rep a_occ_pre.

a_occ is a finite type
Definition a_occ_eqMixin :=
  CanEqMixin prod_of_a_occK.
Canonical a_occ_eqType :=
  Eval hnf in EqType a_occ a_occ_eqMixin.
Definition a_occ_choiceMixin :=
  CanChoiceMixin prod_of_a_occK.
Canonical a_occ_choiceType :=
  Eval hnf in ChoiceType a_occ a_occ_choiceMixin.
Definition a_occ_countMixin :=
  (@CanCountMixin aocc_countprod _ a_occ_rep a_occ_pre prod_of_a_occK).
Canonical a_occ_countType :=
  Eval hnf in CountType a_occ a_occ_countMixin.
Definition a_occ_finMixin :=
  CanFinMixin prod_of_a_occK.
Canonical a_occ_finType :=
  Eval hnf in FinType a_occ a_occ_finMixin.

End a_occ.

Section prog_occ.

Collecting occurrences of a variable

Set of term occurrences for p
Definition tocs p := {set (t_occ p)}.

Computing of occurrences of variables in terms, atoms, clauses

Given a list of pair with a bounded number as first element gives back the list with the numbers incremented
Definition shift1 {k : nat} {A : finType} (l : {set ('I_k × A)%type}) : {set ('I_k.+1 × A)%type} :=
  [set ((ord_shift x.1), x.2) | x in l].

For a given list of terms l gives back the set of indices of terms of l that are a variable
Definition occsInTermList (v : 'I_n) (l : seq term) : {set 'I_max_ar} :=
  [set i : 'I_max_ar | nth_error l i == Some (Var v)].

Gives back the indexes of the variables in an atom
Definition occsInAtom (a : atom) (v : 'I_n) : {set 'I_max_ar} :=
  (@occsInTermList v (arg_atom a)).

Accessing the term in atom a at an index from occsInAtom a will indeed give back a variable
Lemma occsInAtomV occ a v : occ \in occsInAtom a v → nth_error (arg_atom a) occ = Some (Var v).

Given a list of atoms, computes the positions of the variables in that list
Fixpoint occsInAtomList (al : seq atom) (v : 'I_n) : {set ('I_(size al) × 'I_max_ar)} :=
  match al with
  | [::] ⇒ set0
  | a::al ⇒ ([set (Ordinal (ltn0Sn _), x) | x in (occsInAtom a v)] :|: (shift1 (@occsInAtomList al v))) end.

occsInAtomList computes correct positions coresponding to atoms and to variables in those atoms
Lemma occsInAtomListVint (tl : seq atom) v aton termn :
               ((aton, termn) \in occsInAtomList tl v)
            → (∃ ato, nth_error tl aton = Some ato ∧ nth_error (arg_atom ato) termn = Some (Var v)).

occsInAtomList can be augmented with the clause index to get a tocc that references to a variable term in the program
Lemma occsInAtomListV {p} (cl : clause) (cln : 'I_(size p)) v aton termn : Some cl = nth_error p cln
            → ((aton, termn) \in occsInAtomList (body_cl cl) v)
            → @t_at p {| r_ind := cln; b_ind := widen_ord
                (wlist_to_seq_size (body_cl cl)) aton;
                      t_ind := termn |} = Some (Var v).

occsInRule is ocssInAtomList where the first element of the pairs is widened to be 'I_bn
Definition occsInRule (v : 'I_n) (cl : clause) : {set ('I_bn × 'I_max_ar)} :=
  [set ((widen_ord (wlist_to_seq_size (body_cl cl)) (fst x)), (snd x)) | x in (occsInAtomList (body_cl cl) v)].

ocssInRule designates also valid variable indexes
Lemma occsInRuleV {p} cl v aton termn : ((aton, termn) \in occsInRule v (tnth (in_tuple p) cl))
                             → t_at {| r_ind := cl; b_ind := aton; t_ind := termn |} = Some (Var v).

A function to compute t_occs from a clause index and a list of pairs of bounded indexes.
Definition attach_cl_nb p (cl_nb : 'I_(size p)) (occs : {set ('I_bn × 'I_max_ar)}) : tocs p :=
  [set @T_occ p cl_nb (fst x) (snd x) | x in occs].
Computes all the variables t_occurence of a program
Definition occsInProgram p (v : 'I_n) : tocs p :=
  \bigcup_(cln in 'I_(size p)) attach_cl_nb cln (@occsInRule v (tnth (in_tuple p) cln)).

There is a variable indexed by each element of occsInProgram p
Lemma occsInProgramV {p} v (xocc : t_occ p) : xocc \in occsInProgram p v → t_at (xocc) = Some (Var v).

All vars of an atom arguments are in atom_vars
Lemma arg_atom_vars_in (v : 'I_n) (ato : atom) : (Var v \in arg_atom ato) ↔ v \in atom_vars ato.

End prog_occ.

default values
Variable dt : term.
Variable dv : 'I_n.
Variable df : symtype.

Definition term_to_var (t : term) :=
  match t with
    | Val c ⇒ dv
    | Var v ⇒ v end.

Returns (as a variable) the jth term in the head of cl
Definition get_cl_var (cl : clause) (j : nat) : 'I_n :=
  term_to_var (nth dt (arg_atom (head_cl cl)) j).

Lemma get_cl_var_leq (cl : clause) (j : nat) :
   only_variables_head cl
→ j < size (arg_atom (head_cl cl))
→ Var (get_cl_var cl j) \in arg_atom (head_cl cl).

End occurrences.