octalgo.octalgo.norec_sem

Require Import syntax.
Require Import occurrences.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import monotonicity.
Require Import soundness.
Require Import tSemantics.

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

Require Import Sumbool.

Set Implicit Arguments.

Implicit Types (s r : sub) (d def : syntax.constant) (t : term) (a : atom)
(ga : gatom) (tl : list atom) (cl : clause) (i : interp).

No recursion traces: extracting bounded sequences from deduction traces

Section no_rec_traces.

Program to analyze

Variable p : program.

default ground atom for the trace semantics

Variable gat_def : gatom.

Default term, variable and predicate, actually unsused but required by the nth or nth_error functions

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

A branch is a sequence without repetition of t_occ

Definition dbranch := (@uniq_seq_finType (t_occ_finType p)).

the predicate corresponding to the last occurrence of the branch

Definition branch_pred (br : seq (t_occ p)) :=
  match br with
    | [::] ⇒ df
    | a :: l ⇒ match p_at (last a l) with
        | None ⇒ df
        | Some f ⇒ f end end.

branch_pred stable wrt. cons

Lemma branch_pred_eq h (s : seq (t_occ p)) :
size s > 0 → branch_pred s = branch_pred (h ::s).

t_ind (term index) of the last occurrence of the branch

Definition branch_t_ind (br : seq (t_occ p)) :=
  match br with
    | [::] ⇒ 0
    | a :: l ⇒ t_ind (last a l) end.

branch_t_ind stable wrt. cons

Lemma branch_t_ind_eq h (s : seq (t_occ p)) :
size s > 0 → branch_t_ind s = branch_t_ind (h ::s).

The actual extraction

prev is the set of previously visited t_occs tr is the trace to "unrec" v is the variable we focus on count is the fuel used for termination The function computes the sequences of t_occs the values of v go through, and eliminates the repetition of t_occs

Fixpoint unrec_trace_gen (prev : (tocs p)) (tr : (ABtree rul_gr_finType gatom_finType)) (v : 'I_n) (count : nat) : {set dbranch } :=
  match count with | 0 ⇒ set0 | count.+1 ⇒
  match tr with
    | ABLeaf _ ⇒ [set unil ]
    | ABNode (RS cl s) descs ⇒
          let unrec_b (o : t_occ p) : {set dbranch } :=
            match (nth_error descs (b_ind o)) with
              | None ⇒ set0
              | Some (ABLeaf _) ⇒ [set unil ]
              | Some (ABNode (RS clb sb) descsb) ⇒
                  unrec_trace_gen (o |: prev)
                                  (ABNode (RS clb sb) descsb)
                                  (get_cl_var dt dv clb (t_ind o))
                                  count end
        in
        let occs := (occsInProgram p v ) :\: prev in
        \bigcup_(occ in occs ) [set pucons occ l | l in unrec_b occ ]
         end end.

Version used in practice, where prev is empty

Definition unrec_trace (tr : (ABtree rul_gr_finType gatom_finType)) (v : 'I_n) (count : nat) : {set dbranch } :=
unrec_trace_gen set0 tr v count.

The sequences in the no recursion trace are disjoint from prev

Lemma unrec_trace_gen_notin (prev : (tocs p)) (tr : (ABtree rul_gr_finType gatom_finType)) (v : 'I_n) (count : nat) :
[∀ br in unrec_trace_gen prev tr v count , [disjoint [set x | x \in (useq br )] & prev ]].

The no recursion trace is monotonuous wrt. its fuel

Lemma unrec_trace_gen_count_incr (prev : (tocs p)) (tr : (ABtree rul_gr_finType gatom_finType)) (v : 'I_n) (c1 c2 : nat) br :
c1 ≤ c2 → br \in unrec_trace_gen prev tr v c1 → br \in unrec_trace_gen prev tr v c2.

unrec_trace_gen has a normal form wrt. its fuel

Lemma unrec_trace_gen_normal_form (prev : (tocs p)) (tr : (ABtree rul_gr_finType gatom_finType)) (v : 'I_n) (count : nat) :
∀ br, br \in unrec_trace_gen prev tr v count → br \in unrec_trace_gen prev tr v (ABheight tr ).+1.

A substitution s is adequate wrt. a branch br, ending with an occurrence o referring to an occurrence of predicate f, and an interpretation i iff. s v = c, st. i contains a f-fact that has c at the position matching o

Definition br_adequate def (br : dbranch) (s : sub) (v : 'I_n) (i : interp) : bool :=
  [∃ c : syntax.constant , (s v == Some c ) &&
         [∃ ga in i , (sym_gatom ga == branch_pred br )
                       && (nth def (arg_gatom ga) (branch_t_ind br) == c )]].

Core result: any value v can take in practice during an execution of p

is captured by the no-recursion trace

Theorem no_rec_needed def prev (tr : trace_sem_trees gat_def) (i : interp) (m : nat) cl s v :
vars_not_shared p
→ prog_safe p
→ only_variables_in_heads p
→ tr \in sem_t p gat_def def m i
→ ABroot (val tr) = inl (RS cl s)
→ v \in tail_vars (body_cl cl)
→ [∀ br in unrec_trace_gen prev (val tr) v (ABheight (val tr)).+1 ,
br_adequate def br s v i ].

End no_rec_traces.