| < Free Open Study > |
|
The extensions to the eval function are straightforward transcriptions of the evaluation rules introduced in Figures 23-1 and 24-1. The hard work is done by the substitution functions defined in the previous section.
let rec eval1 ctx t = match t with ... | TmTApp(fi,TmTAbs(_,x,t11),tyT2) → tytermSubstTop tyT2 t11 | TmTApp(fi,t1,tyT2) → let t1' = eval1 ctx t1 in TmTApp(fi, t1', tyT2) | TmUnpack(fi,_,_,TmPack(_,tyT11,v12,_),t2) when isval ctx v12 → tytermSubstTop tyT11 (termSubstTop (termShift 1 v12) t2) | TmUnpack(fi,tyX,x,t1,t2) → let t1' = eval1 ctx t1 in TmUnpack(fi,tyX,x,t1',t2) | TmPack(fi,tyT1,t2,tyT3) → let t2' = eval1 ctx t2 in TmPack(fi,tyT1,t2',tyT3) ...
Why is the termShift needed in the first TmUnpack case?
| < Free Open Study > |
|