Library Fminor_well

Relation of well_bound of Fminor terms

Author: Zaynah Dargaye

Created: 29th April 2009

Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Mml.
Require Import Mml_pre.
Require Import FSets.
Require Import FSetAVL.
Require Import Ordered.
Require Import Compare_dec.
Require Import Fminor.
Require Import M2Fminor.
Require Import M2Fminor_proof.

Definition bound_test (n q:nat) :=
  Zle (8+Z_of_nat n*4+4) (8+(Z_of_nat q)*4+4).

Inductive list_param_bound :nat-> list Param->Prop :=
 | bnil : forall z ,list_param_bound z nil
  | vcons : forall id z l , list_param_bound z l ->
     list_param_bound z (VR id::l)
 | scons: forall n z l , bound_test n z ->
                   list_param_bound z l ->
     list_param_bound z (SL n::l).

Lemma list_param_bound_in :
 forall z l , list_param_bound z l ->
 (forall n , In (SL n) l -> bound_test n z).

Inductive well_atom_bound :nat->catom->Prop:=
 | wVar: forall id z , well_atom_bound z (Cvar id)
 | wField : forall n a z, well_atom_bound z a ->
        well_atom_bound z (Cfield n a)
 | wSlot: forall n z,
         bound_test n z ->
        well_atom_bound z (Cslot n).

Inductive well_atomlist_bound : nat->list catom->Prop:=
 |wAnil : forall z, well_atomlist_bound z nil
 |wAcons: forall z hd tl , well_atom_bound z hd ->
        well_atomlist_bound z tl -> well_atomlist_bound z (hd::tl).

Inductive well_bound : nat -> Cterm->Prop:=
 | wCat : forall a z,
        well_atom_bound z a -> well_bound z (Catom a)
 | wCa : forall fid a al z0 z ,
        le z0 z ->
        well_atom_bound z a ->
        well_atomlist_bound z al ->
        well_bound z (Capp fid a al z0)
 | wCc : forall f al z0 z,
         le z0 z ->
         well_atomlist_bound z al ->
         well_bound z (Cclos f al z0)
 | wCcn : forall n al z0 z,
         le z0 z ->
          well_atomlist_bound z al ->
         well_bound z (Ccon n al z0)
 | wCl : forall id c1 c2 z,
          well_bound z c1 -> well_bound z c2 ->
          well_bound z (Clet id c1 c2)
 | wCp : forall n c1 c2 z,
         bound_test n z ->
        well_bound z c1 -> well_bound z c2 ->
        well_bound z (Cpush n c1 c2)
 | wCm: forall a pl z ,
        well_atom_bound z a ->
        well_plist_bound z pl ->
        well_bound z (Cmatch a pl)
with well_pat_bound :nat->cpat->Prop :=
  |wPat : forall lp c z,
          list_param_bound z lp ->
          well_bound z c ->
          well_pat_bound z (CPatc lp c)
with well_plist_bound :nat->list cpat->Prop:=
 | wPnil : forall z , well_plist_bound z nil
 | wPcons : forall hd tl z , well_pat_bound z hd ->
        well_plist_bound z tl -> well_plist_bound z (hd::tl).

Scheme well_bound_ind6 := Minimality for well_bound Sort Prop
 with well_pat_ind6:= Minimality for well_pat_bound Sort Prop
 with well_ptlist_ind6 := Minimality for well_plist_bound Sort Prop.

Definition well_bound_func (f:cfunction) :=
    well_bound (cn_stackspace f) (cn_body f).

Definition well_bound_program (p:cprogram) :=
 (forall id f, In (id,f) (cprog_funct p) -> well_bound_func f) /\
 well_bound (cn_stackspace (cprog_main p))
                     (cn_body (cprog_main p)) .

Section correct_cterm_ind2.

   (P: Cterm ->Prop)
   (Pp: cpat ->Prop)
   (Ppl: list cpat ->Prop).

  (Hca : forall a, P (Catom a))
  (Happ: forall fid ca cal z, P (Capp fid ca cal z) )
  (Hclos: forall fid cal z, P (Cclos fid cal z))
  (Hcon: forall n cal z, P(Ccon n cal z))
  (Hlet: forall id c1 c2, P c1 ->P c2 -> P (Clet id c1 c2))
  (Hpush: forall n c1 c2, P c1 ->P c2 -> P (Cpush n c1 c2))
  (Hmat: forall ca pl, Ppl pl -> P (Cmatch ca pl))
  (Hp: forall xl c, P c ->Pp (CPatc xl c))
  (Hcpn: Ppl nil) (Hcpc: forall ph pt, Pp ph->Ppl pt ->Ppl (ph::pt)) .

Fixpoint cterm_ind2 (c:Cterm): P c:=
 match c as x return P x with
 | Catom a => Hca a
 | Capp fid ca cal z => Happ fid ca cal z
 | Cclos fid cal z => Hclos fid cal z
 |Ccon n cal z => Hcon n cal z
 |Clet id c1 c2=> Hlet id c1 c2 (cterm_ind2 c1) (cterm_ind2 c2)
 |Cpush n c1 c2=> Hpush n c1 c2 (cterm_ind2 c1) (cterm_ind2 c2)
 |Cmatch ca pl => Hmat ca pl
  ( (fix fpl_ind2 (pl:list cpat ){struct pl}: Ppl pl:=
        match pl as x return Ppl x with
        | nil => Hcpn
        | p::l => Hcpc p l (pat_ind2 p) (fpl_ind2 l) end) pl)
with pat_ind2 (p:cpat) {struct p}:Pp p:=
 match p as x return Pp x with
 |CPatc xl c => Hp xl c (cterm_ind2 c)

End correct_cterm_ind2.

Lemma max_commut:
 forall z x , max z x = max x z.

Lemma bound_test_ge:
   forall n z x, bound_test n z -> ge x z ->
   bound_test n x.

Lemma list_param_bound_ge:
 forall l z , list_param_bound z l -> forall x, ge x z ->
                 list_param_bound x l.

Lemma well_atom_bound_ge:
 forall z a , well_atom_bound z a ->
  forall x, ge x z ->
         well_atom_bound x a.

Lemma well_atlist_bound_ge:
 forall z a , well_atomlist_bound z a ->
  forall x, ge x z ->
         well_atomlist_bound x a.

Lemma well_bound_ge:
  forall z c , well_bound z c ->
     forall x, ge x z -> well_bound x c.

Lemma max_ge_left:
 forall x z, ge (max x z) x.

Lemma max_ge_right:
 forall x z, ge (max x z) z.

Lemma well_bound_max_left:
 forall z c x, well_bound z c -> well_bound (max z x) c.

Lemma well_bound_max_right:
 forall z c x, well_bound x c -> well_bound (max z x) c.

Lemma well_atom_bound_max_left:
   forall z c x, well_atom_bound z c -> well_atom_bound (max z x) c.

Lemma well_atom_bound_max_right:
 forall z c x, well_atom_bound x c -> well_atom_bound (max z x) c.

Lemma well_atomlist_bound_max_left:
   forall z c x, well_atomlist_bound z c ->
                       well_atomlist_bound (max z x) c.

Lemma well_atomlist_bound_max_right:
 forall z c x, well_atomlist_bound x c -> well_atomlist_bound (max z x) c.

Lemma well_pat_bound_ge:
  forall z a , well_pat_bound z a ->
     forall x, ge x z -> well_pat_bound x a.

Lemma well_pat_bound_max_left:
   forall z c x, well_pat_bound z c -> well_pat_bound (max z x) c.

Lemma well_pat_bound_max_right:
 forall z c x, well_pat_bound x c -> well_pat_bound (max z x) c.

Lemma well_plist_bound_ge:
  forall z a , well_plist_bound z a ->
     forall x, ge x z -> well_plist_bound x a.

Lemma well_plist_bound_max_left:
   forall z c x, well_plist_bound z c ->
                       well_plist_bound (max z x) c.

Lemma well_plist_bound_max_right:
 forall z c x, well_plist_bound x c -> well_plist_bound (max z x) c.

Lemma max_refl:
 forall n , max n n = n .

Lemma max_trans :
 forall n n1 n0, n <= n1 -> n <= n0 -> n <= (max n1 n0).

Lemma list_param_stack_monotone:
 forall xl n1 k,
  list_param_stack xl n1 = Some k ->
  n1 <= k<= n1+length xl.

Lemma stack_term_monotone:
 forall t n1 n2, stack_term t n1 = Some n2 -> n1 <= n2.

Lemma stack_case_monotone:
 forall t n1 n2, stack_case t n1 = Some n2 -> n1 <= n2.

 Lemma stack_cases_monotone:
 forall t n1 n2, stack_cases t n1 = Some n2 -> n1 <= n2.

Lemma well_atom_bound_germ_atom:
 forall a ce ca
   (GE: germ_atom a ce = Some ca )
    (SSz:stack_atom ca (cenv_height ce) = true),
    well_atom_bound (cenv_height ce) ca.

Lemma well_atomlist_bound_germ_atomlist:
 forall al ce ca
   (GE: germ_atomlist al ce = Some ca )
    (SSz:stack_atomlist ca (cenv_height ce) = true),
    well_atomlist_bound (cenv_height ce) ca.

Lemma l1:
forall l n k,
 list_param_stack l n = Some k->
 list_param_bound k l.

Lemma binds_1 :
 forall xl ce r l c1 l0
      (BD: bind_vars xl ce r l0 = Some (l,c1)) ,
      exists l3, l = l0++l3 /\ length l3 = length xl /\
      list_param_stack l3 (cenv_height ce) = Some (cenv_height c1).

Lemma well_bound_germ:
 forall t ce c n (GE: germ t ce = Some c)
   (SSz : stack_term c (cenv_height ce) = Some n) ,
    well_bound n c.

Lemma bind_pars_monotone:
 forall l ce r l0 l2 c0,
   bind_pars l ce r l0 = Some (l2,c0) ->
   cenv_height ce <= cenv_height c0.

Lemma bind_pars_bound:
 forall l ce r l0 l2 c0,
   bind_pars l ce r l0 = Some (l2,c0) ->
   exists l3, l2 = l0++l3 /\
   (forall n id , In (n,id) l3 -> n <= cenv_height c0).

Lemma cpush_bound:
 forall l k c
     (W:well_bound k c)
     (I:forall n id , In (n,id) l -> n <= k),
     well_bound k (Cpush_list l c).

Lemma well_bound_germ_cfunction:
  forall t c (GE: germ_cfunction t = Some c),
    well_bound_func c.

 Lemma well_bound_germ_cfunctions:
  forall t c (GE: germ_cfunctions t = Some c),
     (forall id f, In (id,f) c ->
                   well_bound_func f).

Theorem well_bound_germ_cprogram:
 forall p cp (GP: germ_cprogram p = Some cp),
  well_bound_program cp.