Library M2Fminor
Conversion in Fminor : last transformation of MLCompCert
Author: Zaynah Dargaye
Created:29th April 2009
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import Integers.
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.
Require Import Mml_pre.
Require Import Fminor.
I. Translation environment
Inductive location :Set:=
| Loc_slot : nat->location
| Loc_var: location.
Definition cemap:= PTree.t location.
Record cenv:Set:=
mkCenv {cenv_map : cemap ; cenv_height: nat}.
Definition empty_cenv:=
(mkCenv (@PTree.empty location) 0).
Require Import Integers.
Definition stack_test (n:nat) :=
(Z_lt_dec (8+(Z_of_nat n)*4+4) Int.max_signed ).
Definition block_test (n:nat) :=
(Z_lt_dec ((Z_of_nat (S n))*4+4) Int.max_signed).
Definition bind_var (v:ident) (ce:cenv) (roots_cont:Identset.t):=
match (cenv_map ce)! v with | None =>
if (Identset.mem v roots_cont) then
( let pos:= (cenv_height ce) in
if (stack_test (pos+1)) then
Some
(SL pos , (mkCenv (PTree.set v (Loc_slot pos) (cenv_map ce))
(( cenv_height ce)+1))) else None )
else
Some (VR v , ( mkCenv ( PTree.set v Loc_var (cenv_map ce))
(cenv_height ce)))
| Some _ => None end.
Definition bind (A B: Set) (f: option A) (g: A -> option B) :=
match f with None => None | Some x => g x end.
Implicit Arguments bind [A B].
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200).
Fixpoint bind_vars (xl:list ident) (ce:cenv) (roots_cont:Identset.t)
(xlb:list Param) {struct xl}:=
match xl with | nil =>Some (xlb,ce)
| a::m =>
do bce0 <-bind_var a ce roots_cont;
(let (b,ce0):=bce0 in
bind_vars m ce0 roots_cont (xlb++b::nil) )
end.
II. variables translation
Fixpoint germ_atom (a:atom) (ce:cenv) {struct a}:=
match a with
| Fvar id => do info<- PTree.get id (cenv_map ce) ;
match info with | Loc_var => Some (Cvar id)
| Loc_slot n => Some (Cslot n)
end
| Ffield n a =>
do ca<- germ_atom a ce;
Some (Cfield n ca)
end.
Fixpoint germ_atomlist (al:list atom) (ce:cenv) {struct al}:=
match al with | nil => Some nil
| a::m => do ca<- germ_atom a ce ; do cm <-germ_atomlist m ce;
Some (ca::cm)
end.
III. Terms translation
Fixpoint germ (f:Fterm) (ce:cenv) {struct f}:=
match f with
| Atom a => do ga<-germ_atom a ce;Some (Catom ga)
| Fapp finfo a al =>
do ga<-germ_atom a ce; do gal<- germ_atomlist al ce;
Some (Capp finfo ga gal (cenv_height ce) )
| Flet id t1 t2 =>
(do g1<-germ t1 ce ;
do bce1<- bind_var id ce (roots_term t2);
let (b,ce1):=bce1 in
do g2<-germ t2 ce1 ;
match b with |SL n => Some (Cpush n g1 g2)
| VR _ => Some (Clet id g1 g2) end
)
|Fmatch a cp =>
let fix germ_patlist (pl:list fpat) (ce:cenv) {struct pl}:=
match pl with
| nil => Some nil
| p::l => do cp<-germ_pat p ce ;do cl<-germ_patlist l ce ;
Some (cp::cl)
end in
do ca<- germ_atom a ce;
do cases<-germ_patlist cp ce ;
if (Z_lt_dec (Z_of_nat (length cp)) Int.max_signed)
then Some (Cmatch ca cases) else None
| Fclos id al =>
if (block_test (length al)) then
do gal<- germ_atomlist al ce; Some (Cclos id gal (cenv_height ce) )
else None
| Fcon n al =>
if (block_test (length al )) then
do gal<- germ_atomlist al ce; Some (Ccon n gal (cenv_height ce) )
else None
end
with germ_pat (p:fpat) (ce:cenv) {struct p}:=
match p with
| FPatc xl f =>
do xlbce0<- bind_vars xl ce (roots_term f) nil;
let (xlb,ce0):=xlbce0 in
do gp <- germ f ce0 ; Some (CPatc xlb gp)
end.
Fixpoint germ_patlist (pl:list fpat) (ce:cenv) {struct pl}:=
match pl with
| nil => Some nil
| p::l => do cp<-germ_pat p ce ;do cl<-germ_patlist l ce ;
Some (cp::cl)
end.
IV. Translation of a program
Fixpoint only_var (xlb:list Param) :=
match xlb with | nil => Identset.empty | VR a::m => Identset.add a (only_var m)
| _ ::m=> only_var m end.
Fixpoint vars_atom (a:catom):Identset.t:=
match a with
| Cvar x => Identset.singleton x
| Cfield n a1 => vars_atom a1
| Cslot n => Identset.empty
end
.
Fixpoint vars_atomlist (al:list catom) :Identset.t:=
match al with | nil => Identset.empty
| a::m => Identset.union (vars_atom a) (vars_atomlist m)
end.
Fixpoint vars_term (c:Cterm) :Identset.t:=
match c with
| Catom a => vars_atom a
| Capp finfo a al z =>
Identset.union (vars_atom a) (vars_atomlist al)
| Cclos id al z => (vars_atomlist al)
| Ccon n al z => (vars_atomlist al)
| Clet id c1 c2 => Identset.add id (Identset.union (vars_term c1) (vars_term c2))
| Cpush n c1 c2 =>
(Identset.union (vars_term c1) (vars_term c2))
| Cmatch a pl =>
let fix vars_cases (cases:list cpat) {struct cases}:=
match cases with | nil => Identset.empty
| b::m => Identset.union (vars_case b) (vars_cases m) end
in Identset.union (vars_atom a) (vars_cases pl)
end
with vars_case (cp:cpat) :Identset.t:=
match cp with
| CPatc xlb c =>
Identset.union (vars_term c) (only_var xlb)
end.
Axiom ge_lt_dec: forall (p q: nat), {ge p q}+{lt p q} .
Definition max (p q:nat) :=
if ge_lt_dec p q then p else q.
Fixpoint stack_atom (ca:catom) (n:nat) {struct ca}:=
match ca with
| Cvar _ => true
| Cfield _ ca1 => stack_atom ca1 n
| Cslot k => ge_lt_dec n k
end.
Fixpoint stack_atomlist (cal:list catom) (n:nat) {struct cal}:=
match cal with | nil => true
| ca::m => if (stack_atom ca n) then stack_atomlist m n
else false
end.
Fixpoint list_param_stack (xl:list Param) (n:nat) {struct xl}:=
match xl with | nil => Some n
| VR _ ::m => list_param_stack m n
| SL k :: m =>
if (nat_eq k n ) then list_param_stack m (S n)
else None
end.
Fixpoint stack_term (c:Cterm) (n:nat) {struct c}:option nat:=
match c with
| Catom a => if (stack_atom a n) then Some n else None
| Capp _ a al _ =>
if (stack_atomlist (a::al) n) then Some n else None
| Cclos _ al _ =>
if (stack_atomlist al n) then Some n else None
| Ccon _ al _ =>
if (stack_atomlist al n) then Some n else None
| Clet _ c1 c2 =>
do n1 <- stack_term c1 n ;
do n2 <- stack_term c2 n;
Some (max n1 n2)
| Cpush m c1 c2 =>
if (nat_eq n m) then
do n1 <- stack_term c1 n ;
do n2 <- stack_term c2 (n+1);
Some ((max n1 n2)) else None
| Cmatch a pl =>
let fix stack_cases (cases:list cpat) (n:nat) {struct cases}:=
match cases with | nil => Some n
| b::m =>
do n1<- stack_case b n ;
do n2<- stack_cases m n ;
Some (max n1 n2)
end
in
if (stack_atom a n) then (stack_cases pl n) else None
end
with stack_case (cp:cpat) (n:nat) {struct cp}:option nat:=
match cp with
| CPatc xlb c =>
do x<-list_param_stack xlb n;
stack_term c x
end.
Fixpoint stack_cases (cases:list cpat) (n:nat) {struct cases}:=
match cases with | nil => Some n
| b::m =>
do n1<- stack_case b n ;
do n2<- stack_cases m n ;
Some (max n1 n2)
end.
Fixpoint bind_pars (xl:list ident) (ce:cenv) (roots_cont:Identset.t)
(c:list (nat*ident)) {struct xl}:=
match xl with
| nil =>Some (c,ce)
| a::m =>
do bce0 <-bind_var a ce roots_cont;
(let (b,ce0):=bce0 in
match b with
| SL pos =>
bind_pars m ce0 roots_cont (c++(pos,a)::nil)
| VR _ => bind_pars m ce0 roots_cont c
end)
end.
Fixpoint Cpush_list (l:list (nat*ident) ) (c:Cterm) {struct l}:=
match l with
| nil => c
| (pos,id)::m =>
Cpush pos (Catom (Cvar id)) (Cpush_list m c)
end.
Definition germ_cfunction (d:funct):=
do xlbce<-bind_pars (fun_par d)
empty_cenv (roots_term (fun_body d)) nil ;
let (xlb,ce):= xlbce in
do c<- germ (fun_body d) ce;
do q0 <- stack_term c (cenv_height ce);
if (stack_test q0) then
Some (mkCfun (fun_par d) q0
(Identset.elements
(List.fold_right Identset.remove (vars_term c)
(Roots::fun_par d)))
(Cpush_list xlb c))
else None .
Fixpoint germ_cfunctions (ld:list (ident*funct)) :=
match ld with | nil =>Some nil
| id_d::m =>
let (id,d):= id_d in
do cd<-germ_cfunction d;
do cm<-germ_cfunctions m ; Some ((id,cd)::cm)
end.
Definition germ_cprogram (p:fprog):=
do cmain<- germ (fprog_main p) empty_cenv;
do cd<-germ_cfunctions (fprog_def p) ;
do qm<- stack_term cmain 0;
if (stack_test qm ) then
Some (mkCprogram cd
(mkCfun nil qm
(Identset.elements (Identset.remove Roots
(vars_term cmain))) cmain))
else None.