25.4 Evaluation

 < Free Open Study > 



25.4 Evaluation

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)       ... 

25.4.1 Exercise []

Why is the termShift needed in the first TmUnpack case?



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net