Library cps2f
come-back translation from CPS to Nml for substitution
Author : Zaynah Dargaye
Created : 29th April 2009
flatting the two kinds of variables into one.
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import Fml.
Require Import CPS.
Definition Cenv:= list nat.
Definition Tenv:=list nat.
Definition liftup (l:list nat) (n:nat) :=
List.map (fun x => plus x n) l.
Fixpoint mkari (n:nat):list nat:=
match n with
| O => nil
| S k=> mkari k++ k::nil
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 flat (t: cpsterm) (ce:Cenv) (te:Tenv) {struct t}:option term:=
match t with
| TVar m => do k<- nth_error te m; Some (Var k)
| CVar m=> do k<-nth_error ce m ; Some (Var k)
| TLamb ari t1 =>
do m1<-flat t1 ( ari::liftup ce (S ari)) (mkari ari++liftup te (S ari));
Some (Lamb ari m1)
| TMu ari t1 =>
do m1<- flat t1 ( ari::liftup ce (S(S ari)))
(mkari ari++(S ari)::liftup te (S(S ari))) ;
Some (Mu ari m1)
|TApp t1 t2 => let
fix flat_list (tl:list cpsterm) (ce:Cenv) (te:Tenv) {struct tl}:option (list term):=
match tl with
| nil=>Some (nil)
| a::m=> do ma<-(flat a ce te);do mm<-(flat_list m ce te);
Some (ma::mm)
end in
do m1<-flat t1 ce te; do m2<-flat_list t2 ce te; Some (App m1 m2)
| TLet t1 t2=> do m1<-flat t1 ce te; do m2<-flat t2 (liftup ce 1) (O::liftup te 1);
Some (tLet m1 m2)
|TConstr m tl =>
let fix flat_list (tl:list cpsterm) (ce:Cenv) (te:Tenv) {struct tl}:option (list term):=
match tl with
| nil=>Some (nil)
| a::m=> do ma<-(flat a ce te);do mm<-(flat_list m ce te);
Some (ma::mm)
end in
do l<-flat_list tl ce te; Some (Con m l)
|TMatch t1 pl=>
let fix flat_plist (tl:list cpat) (ce:Cenv) (te:Tenv) {struct tl}:option (list pat) :=
match tl with
| nil=>Some (nil) | a::m=>
do pa<-(flat_pat a ce te);do pl<-(flat_plist m ce te);
Some (pa::pl) end in
do m1<- flat t1 ce te;
do l<-flat_plist pl ce te; Some (Match m1 l)
end
with flat_pat (p:cpat) (ce:Cenv) (te:Tenv) {struct p}:option pat:=
match p with
| TPatc m t1 => do m1<- flat t1 (liftup ce m) (mkari m++(liftup te m));
Some (Patc m m1)
end .
Fixpoint flat_plist (tl:list cpat) (ce:Cenv) (te:Tenv) {struct tl}:option (list pat) :=
match tl with
| nil=>Some (nil) | a::m=>
do pa<-(flat_pat a ce te);do pl<-(flat_plist m ce te);
Some (pa::pl) end.
Fixpoint flat_list (tl:list cpsterm) (ce:Cenv) (te:Tenv) {struct tl}:option (list term):=
match tl with
| nil=>Some (nil)
| a::m=> do ma<-(flat a ce te);do mm<-(flat_list m ce te);
Some (ma::mm)
end.
Definition ct2t (t:cpsterm) := flat t nil nil.