Library c2p
Constructor Numbering
author : Zaynah Dargayecreated : 29th April 2009
The constructor numbering is the first transformation of MLCompCert. This is the translation of program in EpsilonML to program in EpsilonML with numbered constructors.
Require Import List.
Require Import Coqlib.
Require Import AST.
Require Import Epsml.
Require Import Pml.
Require Import Compare_dec.
Require Import EqNat.
The error monad
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).
I. the translation environment numbers of constructors
Definition gamma := list (ident*nat).
Fixpoint num_list (pos:nat) (l:list ident){struct l}:list (ident*nat):=
match l with
| nil => nil
| a::m => (a,pos)::(num_list (S pos) m)
end.
Fixpoint list_flat (l:list (list ident)) {struct l}:list (ident*nat):=
match l with
| nil => nil
| ll::m => (num_list O ll)++(list_flat m)
end.
Fixpoint get_num
(gam:gamma) (C:ident) {struct gam}:option nat:=
match gam with
| nil => None
| (a,n)::m => if (peq a C) then (Some n) else (get_num m C)
end.
II. Pattern-matching transformation
Fixpoint insert
(n :nat) (p:pat) (l : list (nat*pat)) {struct l}: option (list (nat*pat)) :=
match l with
| nil => Some ((n,p)::nil)
| (k,e)::b =>
if (lt_eq_lt_dec n k) then
(if (beq_nat n k) then None else Some ((n,p)::l) )
else do nl<- insert n p b ;Some ((k,e) :: nl)
end .
Fixpoint sort (l : list (nat*pat)) {struct l}: option (list (nat *pat)) :=
match l with
| nil => Some nil
| (n,p) :: m =>
do sl <- sort m ;
insert n p sl
end.
III. The constructor numbering of a term
Section PMTRANSL.
Variable gam: gamma.
Fixpoint c2p (c: Epsterm) {struct c}:option PMterm:=
match c with
| EpsVar n => Some (TVar n)
| EpsLet c1 c2 =>
do p1<- c2p c1;
do p2 <- c2p c2;
Some (TLet p1 p2)
| EpsFun c1 =>
do p1 <- c2p c1;
Some (TFun p1)
| EpsLetrec c1 c2 =>
do p1<- c2p c1;
do p2 <- c2p c2;
Some (TLetrec p1 p2)
| EpsApply c1 c2 =>
do p1<- c2p c1;
do p2 <- c2p c2;
Some (TApply p1 p2)
| EpsConstr c lc =>
let fix c2pl (lc : list Epsterm) :option (list PMterm):=
match lc with
| nil => Some nil
| c::l => do p<- c2p c ;
do lp<- c2pl l ;
Some (p::lp)
end in
do numC<- get_num gam c ;
do lp<- c2pl lc;
Some (TConstr numC lp)
| EpsMatch c1 cpl =>
let fix c2p_cpat_list (cpl : list cpat) {struct cpl}: option (list (nat*pat)) :=
match cpl with
| nil => Some nil
| c::l => do p <- c2p_cpat c ; do pl <- c2p_cpat_list l ;
Some (p::pl)
end in
do p1<- c2p c1 ;
do ppl <- c2p_cpat_list cpl ;
do pl <- sort ppl ;
Some (TMatch p1 (List.map (@snd nat pat) pl))
end
with c2p_cpat (cp : cpat) : option (nat*pat):=
match cp with
| Epsatc C n c =>
do numC<- get_num gam C;
do p <- c2p c;
Some (numC , (Patc n p))
end.
End PMTRANSL.
IV. The constructor numbering of a program
Definition trad_prg (p: program) :=
c2p (list_flat p.(prog_type)) p.(prog_term).