octalgo.octalgo.extract_static

Require Import syntax.
Require Import occurrences.
Require Import subs.
Require Import pmatch.
Require Import soundness.
Require Import bSemantics.
Require Import tSemantics.
Require Import static.
Require Import norec_sem.
Require Import rinstance.
Require Import completeness.

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

Set Implicit Arguments.

Combining the static analysis and the rule instantiation

Section Transformation.

Definition of dependent substitutions of clauses for a typing

p a program and i an interpretation

Variable p : program.
Variable i : interp.

The variables are not shared across rules

Hypothesis Hvns : vars_not_shared p.

The variables appearing in the head of a clause are a subset of those in the body of the same rule.

Hypothesis Hpsafe : prog_safe p.

Only intensional predicataes are used as head of clauses

Hypothesis Hpsafehds : prog_safe_hds p.

No constant in the head of clauses

Hypothesis Hvarinhead : only_variables_in_heads p.

Only extensional predicates in the interpretation

Hypothesis Hsafe_edb : safe_edb i.

Variable def : syntax.constant.
Variable df : symtype.
Variable dv : 'I_n.
Variable dga : gatom.
Variable docc : t_occ p.

Variable v : 'I_n.

Definition analysis := analyze_var p (Val def) dv v #|rul_gr_finType |.

Extraction of the substitutions via the static analysis

Definition extract_subs_spec : {set sub } :=
    [set s : sub | (dom s == [set v ]) &&
      [∃ ct in analysis ,
        [∀ br in pred_of_set ct , @br_adequate p df def br s v i ]]].

Definition extract_vals_br (br: dbranch p) : {set syntax.constant } :=
  [set (nth def (arg_gatom f) (branch_t_ind br)) | f : gatom in i & sym_gatom f == branch_pred df br ].

Definition extract_vals_conj (cj : {set dbranch p }) : {set syntax.constant } :=
  \bigcap_(br in cj ) extract_vals_br br.

Definition extract_vals_disj (disj : {set {set dbranch p }}) : {set syntax.constant } :=
  \bigcup_(cj in disj ) extract_vals_conj cj.

Definition extract_vals : {set syntax.constant } :=
  extract_vals_disj analysis.

Definition extract_vals_sub : {set sub } :=
  [set (add emptysub v c ) | c in extract_vals ].

Lemma extract_vals_sub_adequate :
  extract_vals_sub = extract_subs_spec.

Lemma static_extract_spec :
  [∀ cl in p ,
   (0 < #|tail_vars (body_cl cl) :&: [set v ]|) ==>
   [∀ s, bmatch def (ffp p i def) cl s ==> (sub_filter s [set v ] \in extract_subs_spec )]].

Adequacy of the transformation

Theorem static_extraction_adequacy (m : nat)
: (sem (@tprog p [set v ] extract_vals_sub) def m i ) = (sem p def m i ).

End Transformation.