Nuprl Definition : C_TYPE_vs_DVALp

C_TYPE_vs_DVALp(env;ctyp) ==
  C_TYPE_ind(ctyp
  Void=>λdval.ff
  Int=>λdval.DVp_Int?(dval)
  Struct(fields)=>r.λdval.if DVp_Struct?(dval)
                          then let lbls = DVp_Struct-lbls(dval) in
                                let g = DVp_Struct-struct(dval) in
                                bdd-all(||fields||;i.eval a = fst(fields[i]) in
                                                     a ∈b lbls ∧b (r i (g a)))
                          else ff
                          fi 
  Array(n,elems)=>recA.λdval.if DVp_Array?(dval)
                             then let a = DVp_Array-lower(dval) in
                                   let b = DVp_Array-upper(dval) in
                                   let f = DVp_Array-arr(dval) in
                                   (n =z b - a) ∧b (∀i∈upto(n).recA (f (a + i)))_b
                             else ff
                             fi 
  Pointer(typ)=>recP.λdval.if DVp_Pointer?(dval)
                           then let ptr = DVp_Pointer-ptr(dval) in
                                    if isl(ptr)
                                    then let lval = outl(ptr) in
                                             if isl(C_TYPE-of-LVALUE(env;lval))
                                             then C_TYPE_eq(outl(C_TYPE-of-LVALUE(env;lval));typ)
                                             else ff
                                             fi 
                                    else tt
                                    fi 
                           else ff
                           fi )


Definitions occuring in Statement :  DVp_Struct-struct: DVp_Struct-struct(v),  DVp_Struct-lbls: DVp_Struct-lbls(v),  DVp_Struct?: DVp_Struct?(v),  DVp_Array-arr: DVp_Array-arr(v),  DVp_Array-upper: DVp_Array-upper(v),  DVp_Array-lower: DVp_Array-lower(v),  DVp_Array?: DVp_Array?(v),  DVp_Pointer-ptr: DVp_Pointer-ptr(v),  DVp_Pointer?: DVp_Pointer?(v),  DVp_Int?: DVp_Int?(v),  C_TYPE-of-LVALUE: C_TYPE-of-LVALUE(env;lval),  C_TYPE_eq: C_TYPE_eq(a;b),  C_TYPE_ind: C_TYPE_ind,  bl-all: (∀x∈L.P[x])_b,  upto: upto(n),  select: L[n],  length: ||as||,  deq-member: x ∈b L,  atom-deq: AtomDeq,  bdd-all: bdd-all(n;i.P[i]),  band: p ∧b q,  callbyvalue: callbyvalue,  outl: outl(x),  ifthenelse: if b then t else f fi ,  isl: isl(x),  eq_int: (i =z j),  bfalse: ff,  btrue: tt,  let: let,  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  subtract: n - m,  add: n + m
FDL editor aliases :  C_TYPE_vs_DVALp
Latex:
C\_TYPE\_vs\_DVALp(env;ctyp)  ==
    C\_TYPE\_ind(ctyp
    Void=>\mlambda{}dval.ff
    Int=>\mlambda{}dval.DVp\_Int?(dval)
    Struct(fields)=>r.\mlambda{}dval.if  DVp\_Struct?(dval)
                                                    then  let  lbls  =  DVp\_Struct-lbls(dval)  in
                                                                let  g  =  DVp\_Struct-struct(dval)  in
                                                                bdd-all(||fields||;i.eval  a  =  fst(fields[i])  in
                                                                                                          a  \mmember{}\msubb{}  lbls  \mwedge{}\msubb{}  (r  i  (g  a)))
                                                    else  ff
                                                    fi 
    Array(n,elems)=>recA.\mlambda{}dval.if  DVp\_Array?(dval)
                                                          then  let  a  =  DVp\_Array-lower(dval)  in
                                                                      let  b  =  DVp\_Array-upper(dval)  in
                                                                      let  f  =  DVp\_Array-arr(dval)  in
                                                                      (n  =\msubz{}  b  -  a)  \mwedge{}\msubb{}  (\mforall{}i\mmember{}upto(n).recA  (f  (a  +  i)))\_b
                                                          else  ff
                                                          fi 
    Pointer(typ)=>recP.\mlambda{}dval.if  DVp\_Pointer?(dval)
                                                      then  let  ptr  =  DVp\_Pointer-ptr(dval)  in
                                                                        if  isl(ptr)
                                                                        then  let  lval  =  outl(ptr)  in
                                                                                          if  isl(C\_TYPE-of-LVALUE(env;lval))
                                                                                          then  C\_TYPE\_eq(outl(C\_TYPE-of-LVALUE(env;lval));typ)
                                                                                          else  ff
                                                                                          fi 
                                                                        else  tt
                                                                        fi 
                                                      else  ff
                                                      fi  )


Date html generated: 2016_05_16-AM-08_51_11
Last ObjectModification: 2014_10_06-PM-04_16_47

Theory : C-semantics


Home Index