Library CPS_env
Big-step semantics with environments of CPS terms
Author : Zaynah Dargaye
Created : 29th April 2009
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import CPS.
Inductive CPSval:Set:=
|CTc : nat->list CPSval->CPSval
|CTcl: nat->list CPSval->list CPSval->cpsterm->CPSval
|CTclr: nat->list CPSval->list CPSval->cpsterm->CPSval.
Definition env:=list CPSval.
Inductive CPSeval: env->env->cpsterm->CPSval->Prop:=
| etvar: forall ce te n v,
nth_error te n=Some v ->
CPSeval ce te (TVar n) v
| ecvar : forall ce te n v,
nth_error ce n =Some v->
CPSeval ce te (CVar n) v
|elamb: forall ce te t ari,
CPSeval ce te (TLamb ari t) (CTcl ari ce te t)
| emu: forall ce te t ari,
CPSeval ce te (TMu ari t) (CTclr ari ce te t)
|eapp : forall ce te t1 tl n vl cv res t ce1 te1,
CPSeval ce te t1 (CTcl n ce1 te1 t) ->
CPSeval_list ce te tl (cv::vl)->
List.length tl = S n ->
CPSeval (cv::ce1) (rev vl++te1) t res->
CPSeval ce te (TApp t1 tl) res
|eappr: forall ce te t1 n tl cv vl res t ce1 te1,
CPSeval ce te t1 (CTclr n ce1 te1 t) ->
CPSeval_list ce te tl (cv::vl)->
List.length tl = S n ->
CPSeval (cv::ce1) (rev vl++ (CTclr n ce1 te1 t)::te1) t res->
CPSeval ce te (TApp t1 tl) res
|econstr : forall ce te tl vl n ,
CPSeval_list ce te tl vl ->
CPSeval ce te (TConstr n tl) (CTc n vl)
|ematch : forall ce te t n pl vl m tn v,
CPSeval ce te t (CTc n vl) ->
nth_error pl n = Some (TPatc m tn) ->
length vl = m ->
CPSeval ce ((rev vl)++te) tn v ->
CPSeval ce te (TMatch t pl) v
| etlet: forall ce te t1 t2 v1 v ,
CPSeval ce te t1 v1 ->
CPSeval ce (v1::te) t2 v ->
CPSeval ce te (TLet t1 t2) v
with
CPSeval_list : env->env->list cpsterm-> list CPSval ->Prop:=
| enil : forall ce te , CPSeval_list ce te nil nil
| econs : forall ce te t lt v lv , CPSeval ce te t v -> CPSeval_list ce te lt lv ->
CPSeval_list ce te (t::lt) (v::lv)
.
Scheme eval_ind6 := Minimality for CPSeval Sort Prop
with evall_ind6 := Minimality for CPSeval_list Sort Prop.