Library n2f

From Nml to Nml for substitution : letrec elimination

Author : Zaynah Dargaye

Created : 29th April 2009




Require Import List.

Require Import Coqlib.

Require Import AST.

Require Import Nml.

Require Import Fml.




Fixpoint trans (t:Nterm) : term:= 

match t with 

 | NVar n=>  Var n

 |NLet t1 t2 => tLet (trans t1) (trans t2)

 |NFun n tb => Lamb n (trans tb) 

 |NLetrec n t1 t2 => tLet (Mu n (trans t1)) (trans t2) 

 |NApply t1 ln => 

      let fix trans_list (ln:list Nterm):= 

       match ln with 

       | nil => nil 

       |a::m => trans a::trans_list m 

      end in  App (trans t1) (trans_list ln)

 |NConstr n ln => 

        let fix trans_list (ln:list Nterm):= 

       match ln with 

       | nil => nil 

       |a::m => trans a::trans_list m 

      end in Con n (trans_list ln) 

 |NMatch t1 pl => 

      let fix trans_pat_list (pl:list npat):= 

      match pl with 

     | nil => nil 

     | a::m => trans_pat a :: trans_pat_list m 

     end in Match (trans t1) (trans_pat_list pl)

 end

with trans_pat (p:npat):pat  := 

 match p with 

 |NPatc n t => Patc n (trans t)

 end.