Library Mml_pre

Roots computation of a term in intermediate monadic form



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 FSets.
Require Import FSetAVL.
Require Import Ordered.
Require Import Compare_dec.

Open Scope nat_scope.

Lemma nat_eq: forall (v1 v2: nat), {v1=v2} + {v1<>v2}.

Lemma nat_eq_true:
  forall (A: Set) (a1 a2: A) (x: nat),
  (if nat_eq x x then a1 else a2) = a1.

Lemma nat_eq_false:
  forall (A: Set) (a1 a2: A) (x y: nat),
  x <> y -> (if nat_eq x y then a1 else a2) = a2.

Require Import Integers.

Module Identset := FSetAVL.Make(OrderedPositive).

Section correct_fterm_ind2.
I Induction scheme of term in intermediate monadic form
Variable
   (P: Fterm ->Prop)
   (Pp: fpat ->Prop)
   (Ppl: list fpat ->Prop).

Hypotheses
  (Hca : forall a, P (Atom a))
  (Happ: forall fid ca cal, P (Fapp fid ca cal) )
  (Hclos: forall fid cal , P (Fclos fid cal))
  (Hcon: forall n cal, P(Fcon n cal))
  (Hlet: forall id c1 c2, P c1 ->P c2 -> P (Flet id c1 c2))
  (Hmat: forall ca pl, Ppl pl -> P (Fmatch ca pl))
  (Hp: forall xl c, P c ->Pp (FPatc xl c))
  (Hcpn: Ppl nil) (Hcpc: forall ph pt, Pp ph->Ppl pt ->Ppl (ph::pt)) .

Fixpoint fterm_ind2 (c:Fterm): P c:=
 match c as x return P x with
 | Atom a => Hca a
 | Fapp fid ca cal => Happ fid ca cal
 | Fclos fid cal => Hclos fid cal
 |Fcon n cal=> Hcon n cal
 |Flet id c1 c2=> Hlet id c1 c2 (fterm_ind2 c1) (fterm_ind2 c2)
 |Fmatch ca pl => Hmat ca pl
      ( (fix fpl_ind2 (pl:list fpat ){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)
end
with pat_ind2 (p:fpat) {struct p}:Pp p:=
 match p as x return Pp x with
 |FPatc xl c => Hp xl c (fterm_ind2 c)
end.

End correct_fterm_ind2.

II. Free variables computation of terms in intermediate monadic form
Fixpoint fv_atom (a:atom) {struct a}:Identset.t:=
 match a with | Fvar a => Identset.add a Identset.empty
                       | Ffield m a => fv_atom a
end.

Fixpoint fv_atomlist (al : list atom) {struct al}:Identset.t:=
match al with | nil =>Identset.empty
| a::l => Identset.union (fv_atom a) (fv_atomlist l)
end.

Fixpoint fv_term (t:Fterm) {struct t}:Identset.t:=
 match t with
 | Atom a =>fv_atom a
 | Fapp info a al =>
     Identset.union (fv_atom a) (fv_atomlist al)
| Fclos fid al => fv_atomlist al
| Fcon n al => fv_atomlist al
| Flet x t1 t2 => Identset.union (fv_term t1)
                          (Identset.remove x (fv_term t2))
| Fmatch a pl =>
   let fix fv_plist (pl:list fpat) {struct pl}:=
    match pl with | nil => Identset.empty
   | p::l => Identset.union (fv_pat p) (fv_plist l) end
   in Identset.union (fv_atom a) (fv_plist pl)
end
with fv_pat ( fp:fpat) {struct fp}:Identset.t:= match fp with
 | FPatc xl p => (fold_right Identset.remove (fv_term p) xl)
end .

Fixpoint fv_plist (pl:list fpat) {struct pl}:Identset.t:=
    match pl with | nil => Identset.empty
   | p::l => Identset.union (fv_pat p) (fv_plist l) end.

III. Terms which can trigger a GC

Fixpoint comp_triggers_gc (f:Fterm):bool :=
 match f with
 | Atom a =>false
 | Fapp info a al => true
 | Fclos fid al => true
 | Fcon m al => true
 | Flet x t1 t2 => (orb (comp_triggers_gc t1)
                                           (comp_triggers_gc t2))
 | Fmatch a pl =>
       let fix comp_triggers_plist (pl:list fpat) :=
       match pl with | nil => false
      | a::m => orb (comp_triggers_pat a ) (comp_triggers_plist m) end
      in comp_triggers_plist pl
 end
with comp_triggers_pat (fp:fpat):bool :=
 match fp with | FPatc xl p => comp_triggers_gc p end.

Fixpoint comp_triggers_plist (pl:list fpat) :=
       match pl with | nil => false
      | a::m => orb (comp_triggers_pat a ) (comp_triggers_plist m) end.

IV. Roots computation of terms in intermediate monadic form
Fixpoint roots_term (t:Fterm) {struct t}:Identset.t:=
 match t with
 | Atom a => Identset.empty
 | Fapp info a al =>Identset.empty
 | Fclos fid al => fv_atomlist al
 | Fcon n al => fv_atomlist al
 | Flet x t1 t2 =>
   if (comp_triggers_gc t1) then
     Identset.union (roots_term t1) (Identset.remove x (fv_term t2))
     else Identset.remove x (roots_term t2)
| Fmatch a cases =>
   let fix roots_cases (cases:list fpat) {struct cases}:=
         match cases with | nil => Identset.empty
        | b::m => Identset.union (roots_case b) (roots_cases m) end
  in roots_cases cases
end
with roots_case (f:fpat) {struct f}:Identset.t:=
 match f with |FPatc xl p =>
   (fold_right Identset.remove (roots_term p) xl)
end.

Fixpoint roots_cases (cases:list fpat) {struct cases}:=
         match cases with | nil => Identset.empty
        | b::m => Identset.union (roots_case b) (roots_cases m) end.