Library CPS_subst
Big-step semantics based on substitution CBV of CPS
Author : Zaynah Dargaye
Created : 29th April 2009
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import CPS.
Open Scope nat_scope.
I. The simultaneous substitution for the 2 kinds of variables
Fixpoint CTsubst_rec
(cl tl : list cpsterm) (t:cpsterm) (nc nt : nat) {struct t}: cpsterm:=
match t with
|TVar m =>
let u:= length tl+nt in
match compare_bd_dec m nt u with
| INF _ => TVar m
| IN _ _ =>
match nth_error tl (m-nt) with |Some w => w | None =>TVar m end
| SUP _=> TVar (m+nt-u)
end
|CVar m=>
let u := length cl+nc in
match compare_bd_dec m nc u with
| INF _ => CVar m
| IN _ _ =>
match nth_error cl (m-nc) with |Some w => w | None =>CVar m end
| SUP _=> CVar (m+nc-u)
end
| TLamb ari b =>
TLamb ari (CTsubst_rec (CTlift_list cl ari) (CTlift_list tl ari) b (S nc) (nt+ari) )
| TMu ari b =>
TMu ari (CTsubst_rec(CTlift_list cl (S ari)) (CTlift_list tl (S ari)) b (S nc) (nt+S ari))
| TApp t1 t2 =>
let fix CTsubst_list_rec
(cl tl :list cpsterm) (l : list cpsterm) (nc nt :nat) {struct l}: list cpsterm:=
match l with
| nil => nil
| a::m => (CTsubst_rec cl tl a nc nt )::(CTsubst_list_rec cl tl m nc nt)
end in
TApp (CTsubst_rec cl tl t1 nc nt) (CTsubst_list_rec cl tl t2 nc nt)
|TLet t1 t2 =>
TLet (CTsubst_rec cl tl t1 nc nt)
(CTsubst_rec (Tlift_list cl 1) (Tlift_list tl 1) t2 nc (S nt))
|TConstr k l =>
let fix CTsubst_list_rec
(cl tl :list cpsterm) (l : list cpsterm) (nc nt :nat) {struct l}: list cpsterm:=
match l with
| nil => nil
| a::m => (CTsubst_rec cl tl a nc nt )::(CTsubst_list_rec cl tl m nc nt)
end in
TConstr k (CTsubst_list_rec cl tl l nc nt)
|TMatch t1 pl =>
let fix CTsubst_patlist_rec
(cl tl :list cpsterm) (l: list cpat) (nc nt : nat) {struct l}: list cpat:=
match l with
| nil => nil
| a::m => (CTsubst_pat_rec cl tl a nc nt )::(CTsubst_patlist_rec cl tl m nc nt )
end in TMatch (CTsubst_rec cl tl t1 nc nt) (CTsubst_patlist_rec cl tl pl nc nt)
end
with CTsubst_pat_rec (cl tl :list cpsterm) (p:cpat) (nc nt :nat) {struct p}:cpat:=
match p with
|TPatc n t => TPatc n (CTsubst_rec (Tlift_list cl n) (Tlift_list tl n) t nc (nt+n))
end.
Fixpoint CTsubst_list_rec
(cl tl :list cpsterm) (l : list cpsterm) (nc nt :nat) {struct l}: list cpsterm:=
match l with
| nil => nil
| a::m => (CTsubst_rec cl tl a nc nt )::(CTsubst_list_rec cl tl m nc nt)
end .
Fixpoint CTsubst_patlist_rec
(cl tl :list cpsterm) (l: list cpat) (nc nt : nat) {struct l}: list cpat:=
match l with
| nil => nil
| a::m => (CTsubst_pat_rec cl tl a nc nt )::(CTsubst_patlist_rec cl tl m nc nt )
end .
II. Semantics
Inductive ceval_term:cpsterm->cpsterm->Prop:=
| ctlamb: forall ari t,
ceval_term (TLamb ari t) (TLamb ari t)
| ctmu: forall ari t,
ceval_term (TMu ari t) (TMu ari t)
| capp: forall t1 c t2 cv vb t v ari ,
ceval_term t1 (TLamb ari t) ->
length t2 = ari ->
ceval_term c cv ->
ceval_list t2 vb->
ceval_term (CTsubst_rec (cv::nil) (rev vb) t O O ) v->
ceval_term (TApp t1 (c::t2)) v
| cappr: forall t1 c cv t v t2 vb ari,
ceval_term t1 (TMu ari t) ->
length t2 = ari ->
ceval_term c cv ->
ceval_list t2 vb->
ceval_term (CTsubst_rec (cv::nil) ((rev vb)++(TMu ari t)::nil) t O O) v->
ceval_term (TApp t1 (c::t2)) v
|clet: forall t1 t2 v1 v2,
ceval_term t1 v1->
ceval_term (CTsubst_rec nil (v1::nil) t2 O O) v2->
ceval_term (TLet t1 t2) v2
|ceconst : forall n l vl,
ceval_list l vl ->
ceval_term (TConstr n l) (TConstr n vl)
|cematch: forall t n lv p ca v,
ceval_term t (TConstr n lv) ->
nth_error p n = Some (TPatc (length lv) ca) ->
ceval_term (CTsubst_rec nil (rev lv) ca O O) v ->
ceval_term (TMatch t p) v
with ceval_list:list cpsterm->list cpsterm->Prop:=
| cenil: ceval_list nil nil
| cecons:forall a va m vm,
ceval_term a va -> ceval_list m vm->
ceval_list (a::m) (va::vm).
Scheme ceval_term_ind6 := Minimality for ceval_term Sort Prop
with ceval_list_ind6 := Minimality for ceval_list Sort Prop.
Lemma eval_unApp:
forall k t1 t2 cv r,
ceval_term k (TLamb 0 t1) ->
ceval_term t2 cv ->
ceval_term (CTsubst_rec (cv::nil) nil t1 O O ) r ->
ceval_term (unApp (TLamb 0 t1) t2) r.
Lemma ceval_app:
forall l1 l2 lv1 lv2, ceval_list l1 lv1 -> ceval_list l2 lv2 ->
ceval_list (l1++l2) (lv1++lv2).
Lemma ceval_length:
forall t v, ceval_list t v -> length t = length v.