Quelle  newspeak.vdmsl

values

beta:nat1 = 2;
epsilon_r:real = 1;
epsilon_t:real = 1;
bytemax:int = 10000;
maxint:int = 100000;
Phi: Fl_elt = mk_Fl_elt(<phi>,1);

zerot:Time = mk_(0,0);
t_absreal:Time = mk_(1,1);
t_absint:Time = mk_(1,1);
t_realmonminus:Time = mk_(1,1);
t_intmonminus:Time = mk_(1,1);
t_not:Time = mk_(1,1);
t_discard:Time = mk_(1,1);
t_round:Time = mk_(1,1);
t_mantissa:Time = mk_(1,1);
t_exponent:Time = mk_(1,1);
t_odd:Time = mk_(1,1);
t_float:Time = mk_(1,1);
t_min:Time = mk_(1,1);
t_max:Time = mk_(1,1);
t_intbinop:Time = mk_(1,1);
t_realbinop:Time = mk_(1,1);
t_intcomp:Time = mk_(1,1);
t_realcomp:Time = mk_(1,1);
t_tr_eq:Time = mk_(1,1);
t_real_eq:Time = mk_(1,1);
t_int_eq:Time = mk_(1,1);
t_void_eq:Time = mk_(1,1);
t_and:Time = mk_(1,1);
t_skip:Time = mk_(1,1);
t_access:Time = mk_(1,1);
t_comp_extract:Time = mk_(1,1);
t_update:Time = mk_(1,1);
t_construct_ev:Time = mk_(1,1);
t_const_type:Time = mk_(1,1);
t_widen_type:Time = mk_(1,1);
t_if: Time = mk_(1,1)

types

Errvalue = <err>;

Id = token;

Flavdom = set of Fl_elt;

Fl_elt::label : token | <phi>
        dim : rat;

Tr:: val: bool
     type: TrType;

TrType:: range: set of bool
         fl: Flavdom;

EqOp = <EQ> | <NEQ>;

Int::val : int
     type : IntType;

IntType:: rep : <byte> | <word>
          range : set of int
          fl : Flavdom;

NumOp ::   <numplus> | <binaryminus> | <nummult> | <numdiv> | <nummod>
        | <nummax> | <nummin>;

CompOp = <numgt> | <numlt> | <numge> | <numle>;

Real::val:real
      type:Float;

Floatrng::lower:int
          upper:int;

Float::range:set of Floatrng
       abserr: real
       relerr: real
       fl:Flavdom;

Void::val:<nil>
      type: VoidType;

VoidType :: fl: Flavdom;

Structure:: val: StructValue
            type: StructureType;

StructValue = seq1 of Component;

Component = int | real | bool;

StructureType :: tps: seq1 of CompType
                 fl : Flavdom;

CompType = TrType | Float | IntType;

Vector::val: VectorValue
        type: VectorType;

VectorValue = seq1 of Tr | seq1 of Real | seq1 of Int | seq1 of Void |
              seq1 of Errvalue | seq1 of VectorValue | seq1 of StructValue;

VectorType :: lower: int
              upper: int
              type : Expressible_type
              fl : Flavdom;

Union:: val : UnionValue
        type : UnionType;

UnionValue = Int | Real | Tr | Void;

UnionType :: tps : set of (IntType | Float | TrType | VoidType)
             fl : Flavdom;

Expressible_type = TrType | Float | IntType | VoidType | VectorType |
                   StructureType | UnionType;

Location :: nat;

Expressible_value = Errvalue | Tr | Int | Real | Void | Structure |
                    Union | Vector;

Storable_value :: Tr | Real | Int | Void | Vector | Structure | Union;

Store = map Location to Storable_value;

Time = nat * nat;

PState:: sto : Store
          time : Time;

Denotable_value = Location | Storable_value | Errvalue |
                  Expressible_type | Proc;

Env = (map Id to Denotable_value) * Location;

EnvState = (Env * PState) | Errvalue;

EST_value:: val : Expressible_value
            sto : Store
            time : Time;

EST_Iterate :: expst : EST_value
               i : int;

Param = seq of Expressible_value;

Proc :: Param -> PState -> EST_value;

Formal_elt :: id : Id
              rep : Expressible_type
              fl : Flavdom;

Program :: Expression;

Expression :: Operation | InnerLoop | Assignment | Scope |
             GuardedScope | Assertion | TimedExpression;

Operation :: MonOperation | BinaryOperation;

MonOperation :: MonOpMonOperand | VectorOperation | Value;

MonOpMonOperand :: operator : MonOp
                   operand : MonOperation;

MonOp = <numabs> | <unaryminus> | <not> | CompileTimeOp | <odd> |
        <round> | <float> | <mantissa> | <exponent> | <discard>;

CompileTimeOp :: <inf> | <sup> | <relonly> | <absonly> | <relerr> |
                <abserr>;

VectorOperation :: vo : VectorOp
                   mo : MonOperation
                   mult : [Multiple];

VectorOp = <sum> | <product> | <all> | <some> | <vecmax> | <vecmin> |
           <flatten>;

Multiple :: op : Operation
            to_p : ToPart;

ToPart = Upto | Downto;

Upto =  Operation;

Downto = Operation;

BinaryOperation:: left : MonOperation
                  opr : BinaryOp
                  right : MonOperation;

BinaryOp :: NumOp | CompOp | EqOp | BoolOp | VecBinOp | <replaceflav>;

BoolOp = <and> | <or>;

VecBinOp = <concat>;

Value :: ConstantValue | NamedValue | VectorVal | Sequence | Call | 
        StructureValue | Widening | Conditional | OuterLoop;

ConstantValue :: IntegerDenotation | FloatingDenotation | Ascii_Char |
                BooleanDenotation | Ascii_string | Flavouring |
                <skip>;

IntegerDenotation :: int;

FloatingDenotation :: real;

BooleanDenotation :: bool;

Ascii_Char :: char;

Ascii_string :: seq1 of char;

NamedValue :: Id | FlavourExtract | FlavourStrip | VectorExtract |
             VectorTrimming; 

FlavourExtract :: nv : NamedValue
                  fl : Flavouring;

Flavouring :: seq of Flavour;

Flavour:: name : token
          index : [rat];

FlavourStrip :: nv:NamedValue
                fl : Flavouring;

VectorExtract :: named : NamedValue
                 index : Operation;

VectorTrimming :: named : NamedValue
                  to_p : <gtvalue> | <ltvalue> | <atvalue>
                  ctv : CompileTimeValue;

CompileTimeValue :: Operation;

VectorVal :: seq1 of Operation;

Sequence :: seq1 of Expression;

Call :: id : Id
        acts: seq of Operation;

StructureValue :: seq1 of Operation;

Widening :: expr : Expression
            tp : Type;

Type :: PrimitiveType | StrucType | VecType | FlavouredType | UnionTp |
       TypeName;

PrimitiveType :: Number | FloatType | VoidValType;

Number :: rep : <bit> | <byte> | <word>
          range : seq of Range;

Range::lower : [CompileTimeValue]
       upper : [CompileTimeValue];

FloatType :: range : seq of Range
            abserr : [CompileTimeValue]
            relerr : [CompileTimeValue];

VoidValType = Flavouring;

VecType :: range : Range
           tp : Type;

StrucType :: seq1 of Type;

FlavouredType::fl : Flavouring
               tp : Type;

UnionTp :: seq1 of Type;

TypeName :: Id;

Conditional :: IfThenOnly | IfThenElse | CaseExpr;

IfThenOnly :: prop : Expression
              action : Sequence;

IfThenElse :: prop : Expression
              thenaction : Sequence
              elseaction : Sequence;

CaseExpr :: expr : Expression
            limbs : seq1 of CaseLimb
            out : [Outlimb];

CaseLimb :: test : Tester
            sequ : Sequence;

Tester = SkeletonType | StrucTest | NonStrucTest;

SkeletonType :: Type | NumSkel | StrucSkel | FlavSkel | VecSkel |
               UnionSkel;

NumSkel :: ranges : [seq1 of Range]
           errors: [Errors];

Errors :: abserr : [CompileTimeValue]
          relerr : [CompileTimeValue];

StrucSkel :: seq1 of (SkeletonType | <nil>);

FlavSkel:: skel : SkeletonType
           fl : Flavouring;

VecSkel :: SkeletonType;

UnionSkel :: seq1 of (FlavouredType | VoidValType | FlavSkel);

StrucTest :: seq1 of (NonStrucTest | <nil>);

NonStrucTest :: id : [Id]
                fl : [Flavouring]
                tp : SkeletonType;

Outlimb = Sequence;

OuterLoop :: OuterIntLoop | OuterVecLoop;

OuterIntLoop :: ovr : OverRange
                actions : Sequence;

OverRange :: cnt : LoopId
             range : Range;

LoopId = Id;

OuterVecLoop :: ovs : OverVectors
                action : Sequence;

OverVectors :: cnt : [LoopId]
               ovv : seq1 of OverVector;

OverVector :: id : Id
              val : Operation;

InnerLoop :: IntLoop | VecLoop | TimeLoop;

IntLoop :: inc : InnerControl
           actions : Sequence;

InnerControl = OverRange | PartialRange;

PartialRange :: cnt : LoopId
                from_p : Operation
                to_p : ToPart
                inc : [Operation];

VecLoop :: ovs : OverVectors
           actions : Sequence;

TimeLoop :: time : TimeInterval
            actions : Sequence;

TimeInterval = Range;

Assignment :: NvAssignment | MultAssignment | StrAssignment;

NvAssignment :: dest : Id
                expr : Expression;

MultAssignment :: dest : Id
                  mult : Multiple
                  expr : Expression;

StrAssignment :: dest : seq1 of Id
                 expr : Expression;

Scope :: SimpleScope | PackageScope;

SimpleScope :: decls : seq1 of Declaration
               expr : Expression;

Declaration = ImportDecl | ExportDecl | LetDecl | VarDecl | ProcDec |
              TypeDec;

ImportDecl :: id : Id
              tp : Type;

ExportDecl :: id : Id
              expr : Expression;

LetDecl :: SimpleLetDecl | StrucLetDecl;

SimpleLetDecl :: id : Id
                 expr : Expression;

StrucLetDecl :: ids : seq1 of Id
                expr : Expression;

VarDecl :: id : Id
           expr : Expression;

ProcDec :: nls : [NonLocals]
           ph : ProcHeading
           expr : Expression;

NonLocals :: ids : [seq1 of Id]
             decls : [seq1 of Declaration];

ProcHeading :: id : Id
               formals : seq of Formal;

Formal :: id : Id
          rep : Representation
          fl : Flavouring;

Representation = PrimitiveRep | StrucRep | VecRep| UnionRep |
                 FlavouredRep | Type;

PrimitiveRep :: NumRep | FloatRep;

NumRep :: rep : <bit> | <byte> | <word>
          rnage : [seq1 of Range];

FloatRep :: range : [seq1 of Range]
            abserr : [CompileTimeValue]
            relerr : [CompileTimeValue];

StrucRep :: seq1 of Representation;

VecRep :: range : Range
          rep : Representation;

UnionRep :: seq1 of Representation;

FlavouredRep :: fl :Flavouring
                rep : Representation;

TypeDec :: id : Id
           tp : Type;

PackageScope :: ids : seq1 of Id
                decls : seq1 of Declaration
                expr : Expression;

GuardedScope :: decls : seq1 of GuardedDeclaration
                inseq : Sequence
                out : Sequence;

GuardedDeclaration = Declaration | WhereDecl;

WhereDecl :: type : SkeletonType
             expr : Expression
             id : [Id];

Assertion :: expr : Expression
             tp : SkeletonType;

TimedExpression :: TimeTakes | TimeAssertion;

TimeTakes :: expr : Expression
             time : TimeInterval;

TimeAssertion :: expr : Expression
                 time : TimeInterval

               





functions

fl_mult: Flavdom * Flavdom -> Flavdom
fl_mult(f1,f2) ==
  if Phi in set f1 union f2 
  then {Phi}
  else {mk_Fl_elt(f.label,f.dim + f'.dim) | f in set f1, f' in set f2
           & f.label = f'.label} union
       { f | f in set f1 & forall f' in set f2 & f'.label <> f.label} union
       { f | f in set f2 & forall f' in set f1 & f'.label <> f.label};

fl_div: Flavdom * Flavdom -> Flavdom
fl_div(f1,f2) ==
  if Phi in set f1 union f2 
  then {Phi}
  else {mk_Fl_elt(f.label,f.dim - f'.dim) | f in set f1, f' in set f2
           & f.label = f'.label} union
       { f | f in set f1 & forall f' in set f2 & f'.label <> f.label} union
       { mk_Fl_elt(f.label,-f.dim) | 
             f in set f2 & forall f' in set f1 & f'.label <> f.label};

phi_remove: Expressible_type -> Expressible_type
phi_remove(tp) ==
  cases tp:
    mk_VoidType(t) -> mk_VoidType(t\ {Phi}),
    mk_TrType(range,fl) -> mk_TrType(range,fl \ {Phi}),
    mk_IntType(rep,range,fl) -> mk_IntType(rep,range, fl \ {Phi}),
    mk_Float(range,abse,rele,fl) -> mk_Float(range,abse,rele,fl\{Phi}),
    mk_VectorType(lower,upper,tp,fl) ->
                      mk_VectorType(lower,upper,tp, fl\{Phi}),
    mk_StructureType(tps,fl) -> mk_StructureType(tps,fl\{Phi}),
    mk_UnionType(tps,fl) -> mk_UnionType(tps,fl\{Phi})
  end;

tr_eq: Tr * Tr * EqOp -> Expressible_value
tr_eq(t1,t2,op) ==
  if t1.type.fl <> t2.type.fl
  then <err>
  elseif op = <EQ>
  then mk_Tr(t1.val = t2.val, mk_TrType({b1 = b2 | b1 in set
                 t1.type.range, b2 in set t2.type.range},{}))
  else mk_Tr(t1.val <> t2.val, mk_TrType({b1 <> b2 | b1 in set
                 t1.type.range, b2 in set t2.type.range},{}));

tr_and: Tr * Tr -> Expressible_value
tr_and(t1,t2) ==
  if t1.type.fl <> t2.type.fl
  then <err>
  else mk_Tr(t1.val and t2.val,
             mk_TrType({b1 and b2 | b1 in set t1.type.range, b2 in set
                                t2.type.range },t1.type.fl));

tr_or: Tr * Tr -> Expressible_value
tr_or(t1,t2) ==
  if t1.type.fl <> t2.type.fl
  then <err>
  else mk_Tr(t1.val or t2.val,
             mk_TrType({b1 or b2 | b1 in set t1.type.range, b2 in set
                                t2.type.range },t1.type.fl));

tr_not: Tr -> Expressible_value
tr_not(t) ==
  mk_Tr(not t.val, mk_TrType({ not b | b in set t.type.range},t.type.fl));


int_eq: Int * Int * EqOp -> Expressible_value
int_eq(z1,z2,op) ==
  if z1.type.fl <> z2.type.fl
  then <err>
  elseif op = <EQ>
  then mk_Tr(z1.val = z2.val, mk_TrType({i = j | i in set
     z1.type.range, j in set z2.type.range},{}))
  else mk_Tr(z1.val <> z2.val, mk_TrType({i <> j | i in set
     z1.type.range, j in set z2.type.range},{}));


min: set1 of real -> real
min(s) ==
  let m in set s in
  if card s = 1 then m 
  else let sm = min(s\{m}) in
    if m < sm then m else sm;

max: set1 of real -> real
max(s) ==
  let m in set s in
  if card s = 1 then m 
  else let sm = max(s\{m}) in
    if m > sm then m else sm;

intbinop: Int * Int * NumOp -> Expressible_value
intbinop(x,y,mk_NumOp(op)) ==
  cases op:
    (<numplus>) -> intplus(x,y),
    (<binaryminus>) -> intbinminus(x,y),
    (<nummult>) -> intmult(x,y),
    (<numdiv>) -> intdiv(x,y),
    (<nummod>) -> intmod(x,y),
    (<nummax>) -> intmax(x,y),
    (<nummin>) -> intmin(x,y)
  end;

intplus: Int * Int -> Expressible_value
intplus(x,y) ==
  if x.type.fl <> y.type.fl 
  then <err>
  else let range = { i + j | i in set x.type.range, j in set
                                          y.type.range} in
       if max({abs min(range), abs max(range)}) >= maxint
       then <err>
       else let rep = if min({abs min(range),abs max(range)}) >= bytemax
                         or x.type.rep = <word> or y.type.rep = <word>
                      then <word>
                      else <byte> in
            mk_Int(x.val + y.val, mk_IntType(rep,range,x.type.fl));

intbinminus: Int * Int -> Expressible_value
intbinminus(x,y) ==
  if x.type.fl <> y.type.fl 
  then <err>
  else let range = { i - j | i in set x.type.range, j in set
                                          y.type.range} in
       if max({abs min(range), abs max(range)}) >= maxint
       then <err>
       else let rep = if min({abs min(range),abs max(range)}) >= bytemax
                         or x.type.rep = <word> or y.type.rep = <word>
                      then <word>
                      else <byte> in
            mk_Int(x.val - y.val, mk_IntType(rep,range,x.type.fl));

intmult: Int * Int -> Expressible_value
intmult(x,y) ==
  let fl = fl_mult(x.type.fl,y.type.fl),
      range = { i * j | i in set x.type.range, j in set y.type.range} in
  if max({abs min(range), abs max(range)}) >= maxint 
  then <err>
  else let rep = if min({abs min(range),abs max(range)}) >= bytemax
                   or x.type.rep = <word> or y.type.rep = <word>
                 then <word>
                 else <byte> in
    mk_Int(x.val * y.val, mk_IntType(rep,range,fl));

intdiv: Int * Int -> Expressible_value
intdiv(x,y) ==
  if 0 in set y.type.range
  then <err>
  else let fl = fl_div(x.type.fl,y.type.fl),
           range = { i div j | i in set x.type.range, j in set
                                     y.type.range} in
       if max({abs min(range), abs max(range)}) >= maxint
       then <err>
       else let rep = if exists r in set range & abs r >= bytemax
                      then <word> else <byte> in
            mk_Int(x.val div y.val, mk_IntType(rep,range,fl));

intmod: Int * Int -> Expressible_value
intmod(x,y) ==
  if 0 in set y.type.range
  then <err>
  else let range = { i mod j | i in set x.type.range, j in set
                                            y.type.range} in
       mk_Int(x.val mod y.val,mk_IntType(y.type.rep,range,x.type.fl));


intmax: Int * Int -> Expressible_value
intmax(x,y) ==
  if x.type.fl <> y.type.fl
  then <err>
  else let rep = if (x.type.rep = <word>) or (y.type.rep = <word>)
                 then <word> else <byte>,
           range = {max({i,j}) | i in set x.type.range, j in set
                                               y.type.range} in
       mk_Int(max({x.val,y.val}),mk_IntType(rep,range,x.type.fl));

intmin: Int * Int -> Expressible_value
intmin(x,y) ==
  if x.type.fl <> y.type.fl
  then <err>
  else let rep = if (x.type.rep = <word>) or (y.type.rep = <word>)
                 then <word> else <byte>,
           range = {min({i,j}) | i in set x.type.range, j in set
                                               y.type.range} in
       mk_Int(min({x.val,y.val}),mk_IntType(rep,range,x.type.fl));


absint: Int -> Int
absint(z) ==
  mk_Int(abs z.val, mk_IntType(z.type.rep, { abs i | i in set
                        z.type.range}, z.type.fl));

intmonminus: Int -> Int
intmonminus(z) ==
  mk_Int(-z.val, mk_IntType(z.type.rep, {-i | i in set z.type.range},
              z.type.fl)) ;

odd: Int -> Tr
odd(z) ==
 let range = { x mod 2 = 0 | x in set z.type.range} in
 mk_Tr(z.val mod 2 = 0, mk_TrType(range,{}));

intcomp: Int * Int * CompOp -> Expressible_value
intcomp(x,y,op) ==
  if x.type.fl <> y.type.fl 
  then <err>
  else let p = lambda mk_(i,j): int * int & 
             cases op:
               <numgt> -> i > j,
               <numlt> -> i < j,
               <numge> -> i >= j,
               <numle> -> i <= j
             end in
       let val = p(mk_(x.val,y.val)),
           range = {p(mk_(i,j)) | i in set x.type.range, j in set
                                 y.type.range} in
           mk_Tr(val,mk_TrType(range,{}));

ascii : char -> int
ascii(c) == 1;

float: Int -> Real
float(z) ==
  mk_Real(z.val,mk_Float({mk_Floatrng(min(z.type.range),max(z.type.range))}, 
      maxint,maxint,{}));

real_eq: Real * Real * EqOp -> Expressible_value
real_eq(r,s,op) ==
  if r.type.fl <> s.type.fl 
  then <err>
  else let r1 = 
               dunion {{floor((1-r.type.relerr) * range.lower - 
                  r.type.abserr),..., floor(0.5 + (1+r.type.relerr) *
                  range.upper + r.type.abserr)} | range in set r.type.range},
           r2 =
               dunion {{floor((1-s.type.relerr) * range.lower - 
                  s.type.abserr),..., floor(0.5 + (1+s.type.relerr) *
                  range.upper + s.type.abserr)} | range in set s.type.range} in
       let range = if r1 inter r2 = {} then {false} else {true,false} in
       if op = <EQ>
       then mk_Tr(r.val = s.val, mk_TrType(range,{}))
       else mk_Tr(r.val <> s.val, mk_TrType({ not t | t in set range},{}));


absreal: Real -> Real
absreal(r) ==
  let new_range = 
      { mk_Floatrng(min({abs range.lower, abs range.upper}),
                    max({abs range.lower, abs range.upper})) 
                            | range in set r.type.range} in
  mk_Real(abs r.val, mu (r.type, range |-> new_range));

realmonminus: Real -> Real
realmonminus(r) ==
  mk_Real(-r.val,mu (r.type, range |->
    { mk_Floatrng(- range.upper, -range.lower) | range in set r.type.range}));

realbinop: Real * Real * NumOp -> Expressible_value
realbinop(x,y,mk_NumOp(op)) ==
  cases op:
    <numplus> -> realplus(x,y),
    <binaryminus> -> realbinminus(x,y),
    <nummult> -> realmult(x,y),
    <numdiv> -> realdiv(x,y),
    <nummax> -> realmax(x,y),
    others -> <err>
  end;

realplus:Real * Real -> Expressible_value
realplus(x,y) ==
  if x.type.fl <> y.type.fl
  then <err>
  else let range = {mk_Floatrng(xrange.lower + yrange.lower,
                      xrange.upper + yrange.upper) | xrange in set
                        x.type.range, yrange in set y.type.range},
           Xmax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set x.type.range}),
           Ymax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set y.type.range}),
           XYmax = max({Xmax,Ymax}) in
       if max({max({abs r.lower, abs r.upper}) | r in set range})  >= maxint
       then <err>
       else let As = x.type.relerr + y.type.abserr + x.type.relerr *
                     Xmax + y.type.relerr * Ymax + epsilon_t*XYmax in
            let val = x.val + y.val,
                type = mk_Float(range,As,epsilon_r,x.type.fl) in
            mk_Real(val,type);

realbinminus: Real * Real -> Expressible_value
realbinminus(x,y) ==
  if x.type.fl <> y.type.fl
  then <err>
  else let range = {mk_Floatrng(xrange.lower - yrange.upper,
                      xrange.upper - yrange.lower) | xrange in set
                        x.type.range, yrange in set y.type.range},
           Xmax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set x.type.range}),
           Ymax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set y.type.range}),
           XYmax = max({Xmax,Ymax}) in
       if max({max({abs r.lower, abs r.upper}) | r in set range})  >= maxint
       then <err>
       else let As = x.type.relerr + y.type.abserr + x.type.relerr *
                     Xmax + y.type.relerr * Ymax + epsilon_t*XYmax in
            let val = x.val - y.val,
                type = mk_Float(range,As,epsilon_r,x.type.fl) in
            mk_Real(val,type);

realmult: Real * Real -> Expressible_value
realmult(x,y) ==
  let range = {mk_Floatrng(xrange.lower * yrange.lower,
                      xrange.upper * yrange.upper) | xrange in set
                        x.type.range, yrange in set y.type.range},
      Xmax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set x.type.range}),
      Ymax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set y.type.range}),
      XYmax = max({Xmax,Ymax}) in
      if max({max({abs r.lower, abs r.upper}) | r in set range})  
           >= maxint
      then <err>
      else let As = Xmax * Ymax * (x.type.relerr + y.type.relerr) +
                    x.type.abserr * Ymax * (1+y.type.relerr) +
                    y.type.abserr * Xmax * (1+x.type.relerr) +
                    x.type.abserr * y.type.abserr + epsilon_t *XYmax,
               fl = fl_mult(x.type.fl, y.type.fl) in
          mk_Real(x.val * y.val, mk_Float(range,As,epsilon_r,fl));

realdiv: Real * Real -> Expressible_value
realdiv(x,y) ==
  if (((1-y.type.relerr) * min({range.lower | range in set y.type.range}) 
           - y.type.abserr) <=0 ) and
     (((1+y.type.relerr) * max({range.upper | range in set y.type.range})
           + y.type.abserr) >=0 )
  then <err>
  else let range = {mk_Floatrng(floor (xrange.lower / yrange.upper),
                      floor(0.5+ xrange.upper / yrange.lower)) | 
                        xrange in set x.type.range, 
                        yrange in set y.type.range},
      Xmax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set x.type.range}),
      Ymax = max(dunion {{abs range.lower,abs range.upper} | 
                                range in set y.type.range}),
      XYmax = max({Xmax,Ymax}),
      Ymin = min(dunion {{abs range.lower,abs range.upper}
                           | range in set y.type.range}) in
       if max({max({abs r.lower, abs r.upper}) | r in set range}) 
              >= maxint
       then <err>
       else let As = ((Xmax * Ymax * max({x.type.relerr, y.type.relerr}) +
                       Ymax * x.type.abserr + Xmax * y.type.abserr)
                      /Ymin ** 2) + epsilon_t * XYmax,
                fl = fl_div(x.type.fl,y.type.fl) in
           mk_Real(x.val/y.val, mk_Float(range,As,epsilon_r,fl));


realmax: Real * Real -> Expressible_value
realmax(x,y) ==
  if x.type.fl <> y.type.fl
  then <err>
  else let val = max({x.val,y.val}),
           abserr = max({x.type.abserr,y.type.abserr}),
           relerr = max({x.type.relerr,y.type.relerr}),
           range = { mk_Floatrng(max({xr.lower,yr.lower}),
                      max({xr.upper,yr.upper})) | 
                       xr in set x.type.range,
                       yr in set y.type.range} in
       mk_Real(val,mk_Float(range,abserr,relerr,x.type.fl));
           

realmin: Real * Real -> Expressible_value
realmin(x,y) ==
  if x.type.fl <> y.type.fl
  then <err>
  else let val = min({x.val,y.val}),
           abserr = max({x.type.abserr,y.type.abserr}),
           relerr = max({x.type.relerr,y.type.relerr}),
           range = { mk_Floatrng(min({xr.lower,yr.lower}),
                      min({xr.upper,yr.upper})) | 
                       xr in set x.type.range,
                       yr in set y.type.range} in
       mk_Real(val,mk_Float(range,abserr,relerr,x.type.fl));

discard: Real -> Int
discard(r) ==
  mk_Int(floor (r.val + 0.5),
          mk_IntType(<word>,dunion {{range.lower,...,range.upper} |
             range in set r.type.range}, {}));

round: Real -> Int
round(r) ==
  if is_int(r.val)
  then mk_Int(r.val,mk_IntType(<word>, dunion {{range.lower,...,range.upper} |
             range in set r.type.range},{}))
  else mk_Int(floor (r.val + 0.5),mk_IntType(<word>,
             dunion {{range.lower,...,range.upper} |range in set r.type.range},
             {}));

realcomp: Real * Real * CompOp -> Expressible_value
realcomp(x,y,op) ==
  if x.type.fl <> y.type.fl 
  then <err>
  else let p = lambda mk_(i,j): real * real &
          cases op:
            <numgt> -> i > j,
            <numlt> -> i < j,
            <numle> -> i <= j,
            <numge> -> i >= j
          end,
           xrange = dunion {{(1-x.type.relerr)*range.lower - x.type.abserr,...,
                     (1+x.type.relerr)*range.upper + x.type.abserr} 
                      | range in set x.type.range},
           yrange = dunion {{(1-y.type.relerr)*range.lower - y.type.abserr,...,
                     (1+y.type.relerr)*range.upper + y.type.abserr} 
                      | range in set y.type.range} in
        let val = p(mk_(x.val,y.val)),
            range = if max(xrange) < min(yrange)
                    then {p(mk_(max(xrange),min(yrange)))}
                    elseif min(xrange) > max(yrange)
                    then {p(mk_(max(yrange),min(xrange)))}
                    else {true,false} in
        mk_Tr(val,mk_TrType(range,{}));

inf: Real -> Real
inf(r) ==
  let m = min({range.lower | range in set r.type.range}) * 
                   (1- r.type.relerr) - r.type.abserr in
  mk_Real(m,mk_Float({mk_Floatrng(m,m)},0,0,{Phi}));

sup: Real -> Real
sup(r) ==
  let m = max({range.upper | range in set r.type.range}) * 
                   (1+ r.type.relerr) + r.type.abserr in
  mk_Real(m,mk_Float({mk_Floatrng(m,m)},0,0,{Phi}));

absonly: Real -> Real
absonly(mk_Real(r,f)) ==
  let abse = f.abserr + (r * f.relerr) in
  mk_Real(r, mu(f, abserr |-> abse, relerr |-> 0));

relonly: Real -> Real
relonly(mk_Real(r,f)) ==
  if r = 0 then mk_Real(r,mu(f,relerr |-> 0, abserr |-> 0))
  else let rel = f.relerr + f.abserr/r in
    mk_Real(r,mu(f,relerr |-> rel, abserr |-> 0));

abserr: Real -> Real
abserr(r) ==
  mk_Real(r.type.abserr,
      mk_Float({mk_Floatrng(r.type.abserr,r.type.abserr)}, 0,0,{Phi}));

relerr: Real -> Real
relerr(r) ==
  mk_Real(r.type.relerr,
      mk_Float({mk_Floatrng(r.type.relerr,r.type.relerr)}, 0,0,{Phi}));


void_eq: Void * Void * EqOp -> Expressible_value
void_eq(v1,v2,op) ==
  if (v1.type = v2.type) and op = <EQ>
  then mk_Tr(true,mk_TrType({true},{}))
  elseif (v1.type <> v2.type) and op = <NEQ>
  then mk_Tr(true,mk_TrType({true},{}))
  else mk_Tr(false,mk_TrType({false},{}));

construct_ev: Component * CompType -> Expressible_value
construct_ev(v,t) ==
  if  is_real(v) then mk_Real(v,t)
  elseif is_bool(v) then mk_Tr(v,t)
  else mk_Int(v,t);

comp_extract: Structure * Flavdom -> Expressible_value
comp_extract(s,fl) ==
  let matches = { i | i in set inds s.val & s.type.tps(i).fl = fl} in
  if card matches <> 1 
  then <err>
  else let {i} = matches in
    construct_ev(s.val(i),s.type.tps(i));

struc_length:StructureType -> nat
struc_length(s) ==
  len s.tps;

vector_extract: Vector * int -> Expressible_value
vector_extract(v,i) ==
  v.val(i - v.type.lower + 1);

vector_subv: VectorValue * int * int -> VectorValue
vector_subv(v,l,u) ==
  v(l,...,u);

vector_length: VectorType -> nat
vector_length(v) ==
  v.type.upper - v.type.lower + 1;

vector_flatten:VectorValue -> VectorValue
vector_flatten(vs) ==
  conc vs;

vector_sum: VectorValue -> Expressible_value
vector_sum(v) ==
  if len v = 1 
  then hd v
  else let s = vector_sum(tl v) in
    if s = <err>
    then <err>
    elseif is_Real(hd v) 
    then realplus(hd v,s)
    else intplus(hd v,s);

vector_product: VectorValue -> Expressible_value
vector_product(v) ==
  if len v = 1 
  then hd v
  else let s = vector_product(tl v) in
    if s = <err>
    then <err>
    elseif is_Real(hd v) 
    then realmult(hd v,s)
    else intmult(hd v,s);
       

vector_all: VectorValue -> Expressible_value
vector_all(v) ==
  if len v = 1
  then hd v
  else let b = vector_all(tl v) in
       if b = <err>
       then <err>
       else tr_and(hd v,b);

vector_some: VectorValue -> Expressible_value
vector_some(v) ==
  if len v = 1
  then hd v
  else let b = vector_some(tl v) in
       if b = <err>
       then <err>
       else tr_or(hd v,b);

vector_max: VectorValue -> Expressible_value
vector_max(v) ==
  if len v = 1 
  then hd v
  else let s = vector_max(tl v) in
       if s = <err>
       then <err>
       elseif is_Real(hd v)
       then realmax(hd v,s)
       else intmax(hd v,s);

vector_min: VectorValue -> Expressible_value
vector_min(v) ==
  if len v = 1 
  then hd v
  else let s = vector_min(tl v) in
       if s = <err>
       then <err>
       elseif is_Real(hd v)
       then realmin(hd v,s)
       else intmin(hd v,s);

vector_concat: Vector * Vector -> Vector
vector_concat(v1,v2) ==
  let type = if tleq(v1.type.type,v2.type.type)
             then v2.type.type
             else v1.type.type,
      lower = v1.type.lower,
      upper = v1.type.upper + v2.type.upper - v2.type.lower + 1,
      fl = v1.type.fl,
      vec = v1.val^v2.val in
      let new_type = mk_VectorType(lower,upper,type,fl) in
      mk_Vector(vec,new_type);




widen_type: Expressible_value * Expressible_type -> Expressible_value
widen_type(x,type) ==
  if x = <err> or is_Void(x) 
  then <err>
  else mu(x,type |-> type);

const_type: Expressible_value -> (Expressible_type | Errvalue)
const_type(v) ==
  if is_Void(v) 
    then v.type
  elseif is_Vector(v) 
    then mk_VectorType(v.type.lower,v.type.upper,
              seqlub([const_type(i) | i in seq v.val]),v.type.fl)
  elseif is_Structure(v) 
    then mk_StructureType([const_type(construct_ev(v.val(i),v.type.tps(i)))
                            | i in set inds v.val],v.type.fl)
  elseif is_Union(v) 
    then const_type(v.val)
  elseif v = <err>
    then <err>
  elseif is_Real(v)
    then mk_Float({mk_Floatrng(floor v.val, if
                  is_int(v.val) then v.val else floor(v.val + 0.5))},
                  v.type.abserr,v.type.relerr,v.type.fl)
  elseif is_Int(v)
    then mk_IntType(v.type.rep,{v.val},v.type.fl)
  else mk_TrType({v.val},v.type.fl);

fleq: Expressible_type * Expressible_type -> bool
fleq(t1,t2) ==
  if (is_VoidType(t1) and is_VoidType(t2)) then  t1 = t2
  elseif not (is_VoidType(t1) and is_VoidType(t2)) then t1.fl = t2.fl
  else false;


replace_flavour: Expressible_type * Flavdom -> (Expressible_type|Errvalue)
replace_flavour(type,flav) ==
  cases type:
   mk_VoidType(fl) -> mk_VoidType(flav),
   mk_TrType(r,f) -> mk_TrType(r,flav),
   mk_Float(r,a,re,f) -> mk_Float(r,a,re,flav),
   mk_IntType(rep,r,f) -> mk_IntType(rep,r,flav),
   mk_VectorType(l,u,t,f) -> mk_VectorType(l,u,t,flav),
   mk_UnionType(tps,fl) -> mk_UnionType(tps, flav),
   mk_StructureType(tps,fl) -> mk_StructureType(tps, flav)
  end;


lub: Expressible_type * Expressible_type -> (Expressible_type | Errvalue)
lub(t1,t2) ==
  if is_TrType(t1) and is_TrType(t2) and fleq(t1,t2)
    then trlub(t1,t2)
  elseif is_Float(t1) and is_Float(t2) and fleq(t1,t2)
    then floatlub(t1,t2)
  elseif is_IntType(t1) and is_IntType(t2) and fleq(t1,t2)
    then intlub(t1,t2)
  elseif is_VectorType(t1) and is_VectorType(t2) and fleq(t1,t2)
    then vectorlub(t1,t2)
  elseif is_StructureType(t1) and is_StructureType(t2) and fleq(t1,t2)
    then struclub(t1,t2)
  elseif is_UnionType(t1) and is_UnionType(t2) and fleq(t1,t2)
    then unionlub(t1,t2)
  elseif is_VoidType(t1) and is_VoidType(t2) and fleq(t1,t2)
    then t1
  else <err>;

  
trlub : TrType * TrType -> TrType
trlub(t1,t2) ==
  mk_TrType(t1.range union t2.range,t1.fl);

floatlub: Float * Float -> Float
floatlub(t1,t2) ==
  mk_Float(t1.range union t2.range, max({t1.abserr,t2.abserr}), 
           max({t1.relerr,t2.relerr}),t1.fl);

intlub: IntType * IntType -> (IntType | Errvalue)
intlub(t1,t2) ==
  if t1.rep = <byte> and t2.rep = <byte>
    then mk_IntType(<byte>,t1.range union t2.range, t1.fl)
  elseif t1.rep = <word> and t2.rep = <word>
    then mk_IntType(<word>,t1.range union t2.range, t1.fl)
  else <err>;

vectorlub : VectorType * VectorType -> (VectorType | Errvalue)
vectorlub(t1,t2) ==
  if (t1.lower <> t2.lower) or (t1.upper <> t2.upper) or
     (lub(t1.type,t2.type) = <err>)
  then <err>
  else mk_VectorType(t1.lower,t1.upper,lub(t1.type,t2.type),t1.fl);

struclub: StructureType * StructureType -> (StructureType | Errvalue)
struclub(t1,t2) ==
  if len t1.tps <> len t2.tps
  then <err>
  elseif exists i in set inds t1.tps & lub(t1.tps(i),t2.tps(i)) = <err>
  then <err>
  else mk_StructureType([lub(t1.tps(i),t2.tps(i)) | i in set inds t1.tps],
                        t1.fl);

unionlub: UnionType * UnionType -> (UnionType | Errvalue)
unionlub(t1,t2) ==
  if card t1.tps <> card t2.tps
  then <err>
  else let lub = setlub(t1.tps union t2.tps) in 
       if lub = <err>
       then <err>
       elseif is_UnionType(lub)
       then mk_UnionType(lub.tps,t1.fl)
       else mk_UnionType({lub},t1.fl);

seqlub: seq1 of Expressible_type -> (Expressible_type | Errvalue)
seqlub(tps) ==
  if len tps = 1 
  then hd tps
  elseif lub(tps(1),tps(2)) = <err>
  then <err>
  else lub(lub(tps(1),tps(2)),seqlub(tl tps));

setlub : set of Expressible_type -> (Expressible_type | Errvalue)
setlub(s) ==
  if exists t1,t2 in set s & lub(t1,t2) = <err>
  then if forall t in set s & is_TrType(t) or is_IntType(t) or
                              is_Float(t) or is_VoidType(t)
       then let t1 = { setlub({ t' | t' in set s & is_TrType(t') and
                          t.fl = t'.fl}) | t in set s & is_TrType(t)},
                t2 = { setlub({ t' | t' in set s & is_IntType(t') and
                          t.fl = t'.fl}) | t in set s & is_IntType(t)},
                t3 = { setlub({ t' | t' in set s & is_Float(t') and
                          t.fl = t'.fl}) | t in set s & is_Float(t)},
                t4 = { setlub({ t' | t' in set s & is_VoidType(t') and
                          t.fl = t'.fl}) | t in set s & is_VoidType(t)} in
            if (exists t,t' in set dunion {t1,t2,t3,t4} & t.fl = t'.fl)
               or exists t in set dunion {t1,t2,t3}, 
                         mk_VoidType(f) in set t4 &
                    t.fl = f
            then <err>
            else mk_UnionType(t1 union t2 union t3 union t4,{})
       else <err>
  else let t in set s in
       if s = {t} 
       then t
       else lub(t,setlub(s \ {t}));


gt : Expressible_type * Expressible_type -> bool
gt(t1,t2) ==
  lub(t1,t2) = t1 or
  (fleq(t1,t2) and
    ( (is_TrType(t2) and let z in set power {0,1} be st
                           true in set t2.range => 1 in set z and
                           false in set t2.range => 0 in set z in
          (is_Float(t1) and z subset dunion {{lower,...,upper} | 
                            mk_Floatrng(lower,upper) in set t1.range}) or
          (is_IntType(t1) and z subset t1.range))
      or
      (is_IntType(t2) and t2.rep = <byte> and
          (is_Float(t1) and t2.range subset 
                   dunion {{lower,...,upper} | mk_Floatrng(lower,upper) 
                                      in set t1.range}) or
          (is_IntType(t1) and t1.rep = <word> and t2.range subset t1.range))
      or
      (is_IntType(t2) and t2.rep = <word> and is_Float(t1) and
           t2.range subset dunion {{lower,...,upper} | 
                        mk_Floatrng(lower,upper) in set t1.range})
      or
      (is_Float(t2) and is_Float(t1) and 
           dunion { {lower,...,upper} | mk_Floatrng(lower,upper) in set 
                   t2.range} subset
           dunion { {lower,...,upper} | mk_Floatrng(lower,upper) in set 
                   t1.range} and
           t2.abserr + t2.relerr * max({ abs max({lower,upper}) | 
                mk_Floatrng(lower,upper) in set t2.range}) <= t1.abserr + 
             t1.relerr * max({ abs max({lower,upper}) | 
                mk_Floatrng(lower,upper) in set t1.range}))
      or
      (is_UnionType(t1) and is_UnionType(t2) and
           forall t in set t1.tps & exists t' in set t2.tps &
                lub(t,t') = t))
   or
   (is_UnionType(t2) and exists t in set t2.tps & gt(t1,t)));     



tleq: Expressible_type * Expressible_type -> bool
tleq(t1,t2) ==
  lub(t1,t2) = t2;

next_locn: Location -> Location
next_locn(mk_Location(l)) ==
  mk_Location(l+1);

access: Location -> Store -> Storable_value
access(l)(s) ==
   s(l);

update : Location -> Storable_value -> Store -> Store
update(l)(v)(s) ==
  s ++ {l |-> v};

multi_update: seq of Location -> seq of Storable_value -> Store -> Store
multi_update(ls)(vs)(s) ==
  if ls = []
  then s
  else multi_update(tl ls)(tl vs)(s ++ { hd ls |-> hd vs})
pre len ls = len vs;

timeleq : Time * Time -> bool
timeleq(mk_(lt1,ut1),mk_(lt2,ut2)) ==
  lt2 <= lt1 and lt1 <= ut1 and ut1 <= ut2;

access_env : Id -> Env -> Denotable_value
access_env(i)(mk_(m,l)) ==
  m(i);

update_env : Id -> Denotable_value -> Env -> Env
update_env(i)(d)(mk_(m,l)) ==
  mk_(m ++ { i |-> d },l);

empty_env: Location -> Env
empty_env(l) ==
  mk_({|->},l);

multi_update_env : seq of (Id * Denotable_value) -> Env -> Env
multi_update_env(s)(e) ==
  if s = []
  then e
  else let mk_(id,v) = hd s in
    multi_update_env (tl s)(update_env(id)(v)(e));

reserve_locn : Env -> (Location * Env)
reserve_locn(mk_(m,l)) ==
  mk_(l,mk_(m,next_locn(l)));

instantiate_formals : (seq of Formal_elt) -> Param -> Env -> 
                      (Env | Errvalue)
instantiate_formals(formals)(params)(e) ==
  if len formals <> len params 
  then <err>
  else let lubs_eq = [ lub(formals(i).rep, (params(i)).type) =
                 formals(i).rep | i in set inds formals] in
       if false in set elems lubs_eq
       then <err>
       else let vals = [ if formals(i).fl = {}
                         then params(i)
                         else widen_type(params(i).val,
                                replace_flavour(params(i).type,
                                formals(i).fl)) | i in set inds params] in
            multi_update_env([mk_(formals(i).id,vals(i)) | i in set
                                 inds vals])(e);

mantissa : Real -> Real
mantissa(r) == r;

exponent : Real -> Real
exponent(r) == r;

tplus : Time * Time -> Time
tplus(mk_(l1,u1),mk_(l2,u2)) ==
  mk_(l1 + l2, u1 + u2);

dtplus : seq of Time -> Time
dtplus(ts) ==
  if ts = []
  then zerot
  else tplus(hd ts, dtplus(tl ts));

t_trimming_op:int -> Time 
t_trimming_op(l) == mk_(1,1);

t_vector_extract: int -> Time
t_vector_extract(l) == mk_(1,1);

t_vector_concat: int * int -> Time
t_vector_concat(l,m) == mk_(1,1);

t_vectorsum: int -> Time
t_vectorsum(l) == mk_(1,1);

t_vectorproduct: int -> Time
t_vectorproduct(l) == mk_(1,1);

t_vector_all: int -> Time
t_vector_all(l) == mk_(1,1);

t_vector_some: int -> Time
t_vector_some(l) == mk_(1,1);

t_vector_max: int -> Time
t_vector_max(l) == mk_(1,1);

t_vector_min: int -> Time
t_vector_min(l) == mk_(1,1);

t_vector_flatten: int -> Time
t_vector_flatten(l) == mk_(1,1);

t_vector_subv: int -> Time
t_vector_subv(l) == mk_(1,1);

t_multi_update : int -> Time
t_multi_update(l) == mk_(1,1);

choose : Expressible_type -> Expressible_value
choose(tp) ==
  let val: Expressible_value be st
    lub(const_type(val),tp) = tp in
  widen_type(const_type(val),tp);


eval_Program : Program -> Location -> Store -> EST_value
eval_Program(mk_Program(expr))(l)(sto) ==
  eval_Expression(expr)(empty_env(l))(mk_PState(sto,zerot)) ;

eval_Expression : Expression -> Env -> PState -> EST_value
eval_Expression(mk_Expression(expr))(env)(ps) ==
  cases expr:
   mk_Operation(op) -> eval_Operation(expr)(env)(ps),
   mk_InnerLoop(l) -> eval_InnerLoop(expr)(env)(ps),
   mk_Assignment(a) -> eval_Assignment(expr)(env)(ps),
   mk_Scope(s) -> eval_Scope(expr)(env)(ps),
   mk_GuardedScope(d,i,o) -> eval_GuardedScope(expr)(env)(ps),
   mk_Assertion(exp,tp) -> eval_Assertion(expr)(env)(ps),
   mk_TimedExpression(t) -> eval_TimedExpression(expr)(env)(ps)
  end;

eval_Operation : Operation -> Env -> PState -> EST_value
eval_Operation(mk_Operation(op))(e)(ps) ==
  cases op:
    mk_MonOperation(mo) -> eval_MonOperation(op)(e)(ps),
    mk_BinaryOperation(l,bo,r) -> eval_BinaryOperation(op)(e)(ps)
  end;

eval_MonOperation : MonOperation -> Env -> PState -> EST_value
eval_MonOperation(mk_MonOperation(mo))(e)(ps) ==
  cases mo:
    mk_MonOpMonOperand(opr,opnd) ->
           eval_MonOpMonOperand(mk_MonOpMonOperand(opr,opnd))(e)(ps),
    mk_VectorOperation(v,m,op) ->
           eval_VectorOperation(mk_VectorOperation(v,m,op))(e)(ps),
    mk_Value(v) -> eval_Value(mk_Value(v))(e)(ps)
  end;

eval_MonOpMonOperand: MonOpMonOperand -> Env -> PState -> EST_value
eval_MonOpMonOperand(mk_MonOpMonOperand(opr,opnd))(e)(ps) ==
  let x = eval_MonOperation(opnd)(e)(ps) in
  if x.val = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else cases opr:
        <numabs> -> eval_Abs(x),
        <unaryminus> -> eval_MonMinus(x),
        <not> -> eval_Not(x),
        mk_CompileTimeOp(o) -> eval_CompileTimeOp(opr)(x),
        <discard> -> eval_Discard(x),
        <round> -> eval_Round(x),
        <odd> -> eval_Odd(x),
        <float> -> eval_Float(x),
        <mantissa> -> eval_Mantissa(x),
        <exponent> -> eval_Exponent(x)
       end;

eval_Abs : EST_value -> EST_value
eval_Abs(mk_EST_value(val,sto,time)) ==
  if is_Real(val) 
  then mk_EST_value(absreal(val),sto,tplus(time,t_absreal))
  elseif is_Int(val)
  then mk_EST_value(absint(val),sto,tplus(time,t_absint))  
  else mk_EST_value(<err>,sto,zerot);

eval_MonMinus : EST_value -> EST_value
eval_MonMinus(mk_EST_value(val,sto,time)) ==
  if is_Real(val) 
  then mk_EST_value(realmonminus(val),sto,tplus(time,t_realmonminus))
  elseif is_Int(val)
  then mk_EST_value(intmonminus(val),sto,tplus(time,t_intmonminus))  
  else mk_EST_value(<err>,sto,zerot);

eval_Not : EST_value -> EST_value
eval_Not(mk_EST_value(val,sto,time)) ==
  if not is_Tr(val)
  then mk_EST_value(<err>, sto, zerot)
  else mk_EST_value(tr_not(val),sto, tplus(time,t_not));

eval_CompileTimeOp : CompileTimeOp -> EST_value -> EST_value
eval_CompileTimeOp(mk_CompileTimeOp(op))(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto,zerot)
  else cases op:
        <inf> -> mk_EST_value(inf(val),sto,time),
        <sup> -> mk_EST_value(sup(val),sto,time),
        <absonly> -> mk_EST_value(absonly(val),sto,time),
        <relonly> -> mk_EST_value(relonly(val),sto,time),
        <abserr> -> mk_EST_value(abserr(val),sto,time),
        <relerr> -> mk_EST_value(relerr(val),sto,time)
       end;

eval_Discard : EST_value -> EST_value
eval_Discard(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto, zerot)
  else mk_EST_value(discard(val),sto,tplus(time,t_discard));

eval_Round : EST_value -> EST_value
eval_Round(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto, zerot)
  else mk_EST_value(round(val),sto,tplus(time,t_round));

eval_Mantissa : EST_value -> EST_value
eval_Mantissa(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto, zerot)
  else mk_EST_value(mantissa(val),sto,tplus(time,t_mantissa));

eval_Exponent : EST_value -> EST_value
eval_Exponent(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto, zerot)
  else mk_EST_value(exponent(val),sto,tplus(time,t_exponent));

eval_Odd : EST_value -> EST_value
eval_Odd(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto, zerot)
  else mk_EST_value(odd(val),sto,tplus(time,t_odd));

eval_Float : EST_value -> EST_value
eval_Float(mk_EST_value(val,sto,time)) ==
  if not is_Real(val)
  then mk_EST_value(<err>,sto, zerot)
  else mk_EST_value(float(val),sto,tplus(time,t_float));

eval_VectorOperation : VectorOperation -> Env -> PState -> EST_value
eval_VectorOperation(mk_VectorOperation(vo,mo,mult))(e)(ps) ==
  let x = eval_MonOperation(mo)(e)(ps) in
  if not is_Vector(x.val)
  then mk_EST_value(<err>,ps.sto,zerot)
  else let v = if mult = nil then x
               else eval_VectorMult(mu(x,sto |-> ps.sto))(mult)(e) in
       if v.val = <err>
       then mk_EST_value(<err>,ps.sto,zerot)
       else cases vo:
             <sum> -> eval_VectorSum(v),
             <product> -> eval_VectorProduct(v),
             <vecmax> -> eval_VectorMax(v),
             <vecmin> -> eval_VectorMin(v),
             <all> -> eval_VectorAll(v),
             <some> -> eval_VectorSome(v),
             <flatten> -> eval_VectorFlatten(v)
            end;


eval_VectorMult : EST_value -> Multiple -> Env -> EST_value
eval_VectorMult(mk_EST_value(est_val,sto,time))(mk_Multiple(op,to_p))(e)
      ==
  let mk_Vector(val,type) = est_val in
  let b1 = eval_Operation(op)(e)(mk_PState(sto,time)) in
  let b2 = eval_Operation(to_p)(e)(mk_PState(sto,b1.time)) in
  if not (is_Int(b1.val) and is_Int(b2.val))
  then mk_EST_value(<err>,sto,zerot)
  elseif card(b1.val.type.range) <> 1 or card(b2.val.type.range) <> 1
  then mk_EST_value(<err>,sto,zerot)
  else let lower = min({b1.val.val,b2.val.val}),
           upper = max({b1.val.val,b2.val.val}) in
       if (lower < type.lower) or (type.upper < upper)
       then mk_EST_value(<err>,sto,zerot)
       else let new_val = vector_subv(val,lower,upper),
                new_type = mk_VectorType(lower,upper,type.type,type.fl) in
            let new_v = mk_Vector(new_val,new_type),
                new_t = tplus(tplus(b2.time,t_vector_subv(upper - lower)), 
                        tplus(t_min,t_max)) in
            mk_EST_value(new_v,sto,new_t);


eval_VectorSum : EST_value -> EST_value
eval_VectorSum(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if is_Float(type.type) or is_IntType(type.type)
  then mk_EST_value(vector_sum(val),sto,
                 tplus(time,t_vectorsum(type.upper - type.lower)))
  else mk_EST_value(<err>,sto,zerot);

eval_VectorProduct : EST_value -> EST_value
eval_VectorProduct(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if is_Float(type.type) or is_IntType(type.type)
  then mk_EST_value(vector_product(val),sto,
                 tplus(time,t_vectorproduct(type.upper - type.lower)))
  else mk_EST_value(<err>,sto,zerot);

eval_VectorMax : EST_value -> EST_value
eval_VectorMax(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if is_Float(type.type) or is_IntType(type.type)
  then mk_EST_value(vector_max(val),sto,
                 tplus(time,t_vector_max(type.upper - type.lower)))
  else mk_EST_value(<err>,sto,zerot);

eval_VectorMin : EST_value -> EST_value
eval_VectorMin(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if is_Float(type.type) or is_IntType(type.type)
  then mk_EST_value(vector_min(val),sto,
                 tplus(time,t_vector_min(type.upper - type.lower)))
  else mk_EST_value(<err>,sto,zerot);

eval_VectorAll : EST_value -> EST_value
eval_VectorAll(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if not is_TrType(type.type) 
  then mk_EST_value(<err>,sto,zerot)
  else mk_EST_value(vector_all(val),sto,
                 tplus(time,t_vector_all(type.upper - type.lower)));

eval_VectorSome : EST_value -> EST_value
eval_VectorSome(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if not is_TrType(type.type) 
  then mk_EST_value(<err>,sto,zerot)
  else mk_EST_value(vector_some(val),sto,
                 tplus(time,t_vector_some(type.upper - type.lower)));

eval_VectorFlatten : EST_value -> EST_value
eval_VectorFlatten(mk_EST_value(mk_Vector(val,type),sto,time)) ==
  if not is_VectorType(type.type)
  then mk_EST_value(<err>,sto,zerot)
  else let new_val = vector_flatten(val) in
       let new_upper = len new_val + type.lower - 1 in
       let new_time = tplus(time,t_vector_flatten(type.upper -
                      type.lower)),
           new_type = mk_VectorType(type.lower,
                          new_upper,type.type,type.fl) in
       mk_EST_value(mk_Vector(new_val,new_type),sto,new_time);



eval_BinaryOperation: BinaryOperation -> Env -> PState -> EST_value
eval_BinaryOperation(bo)(e)(ps) ==
 let mk_BinaryOp(op) = bo.opr in
  cases op:
    mk_NumOp(opr) -> eval_NumOp(bo)(e)(ps),
    <numgt>,<numlt>,<numge>,<numle> -> eval_CompOp(bo)(e)(ps),
    <and>,<or> -> eval_BoolOp(bo)(e)(ps),
    <EQ>,<NEQ> -> eval_EqOp(bo)(e)(ps),
    <concat> -> eval_Concat(bo)(e)(ps)
  end;

eval_NumOp : BinaryOperation -> Env -> PState -> EST_value
eval_NumOp(mk_BinaryOperation(left,mk_BinaryOp(opr),right))(e)(ps) ==
  let a1 = eval_MonOperation(left)(e)(ps) in
  let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
  cases opr:
    mk_NumOp(op) -> 
      cases mk_(a1.val,a2.val):
        mk_(mk_Int(v1,t1),mk_Int(v2,t2)) ->
          if op <> <numdiv>
          then let val = intbinop(mk_Int(v1,t1),mk_Int(v2,t2),mk_NumOp(op)) in
               if val = <err>
               then mk_EST_value(<err>, ps.sto, zerot)
               else mk_EST_value(val,ps.sto, tplus(a2.time,t_intbinop))
          else mk_EST_value(<err>,ps.sto,zerot),
        mk_(mk_Real(v1,t1),mk_Real(v2,t2)) -> 
          if op not in set {<numdiv>,<nummod>} 
          then let val = realbinop(mk_Real(v1,t1),mk_Real(v2,t2),mk_NumOp(op)) 
                          in
               if val = <err>
               then mk_EST_value(<err>,ps.sto,zerot)
               else mk_EST_value(val,ps.sto, tplus(a2.time,t_realbinop))
          else mk_EST_value(<err>,ps.sto,zerot),
        others -> mk_EST_value(<err>,ps.sto,zerot)
      end,
    <replaceflav> -> if a2.val <> <err> and is_Void(a2.val)
                     then let mk_VoidType(f) = a2.val.type in
                          mk_EST_value(mu(a1.val,type |-> 
                              replace_flavour(a1.val.type,f)),
                              ps.sto,a2.time)
                     else mk_EST_value(<err>,ps.sto, zerot),
    others -> mk_EST_value(<err>,ps.sto,zerot)
  end;

eval_CompOp : BinaryOperation -> Env -> PState -> EST_value
eval_CompOp(mk_BinaryOperation(left,mk_BinaryOp(opr),right))(e)(ps) ==
  let a1 = eval_MonOperation(left)(e)(ps) in
  let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
  if (is_Int(a1.val) and is_Int(a2.val))
  then mk_EST_value(intcomp(a1.val,a2.val,opr),
                                ps.sto,tplus(a2.time,t_intcomp))
  elseif is_Real(a1.val) and is_Real(a2.val)
  then mk_EST_value(realcomp(a1.val,a2.val,opr),
                                ps.sto,tplus(a2.time,t_realcomp))
  else mk_EST_value(<err>, ps.sto, zerot);

eval_EqOp : BinaryOperation -> Env -> PState -> EST_value
eval_EqOp(mk_BinaryOperation(left,mk_BinaryOp(op),right))(e)(ps)==
    let a1 = eval_MonOperation(left)(e)(ps) in
    let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
    if is_Tr(a1.val) and is_Tr(a2.val)
    then mk_EST_value(tr_eq(a1.val,a2.val,op),
                                   ps.sto,tplus(a2.time,t_tr_eq)) 
    elseif is_Real(a1.val) and is_Real(a2.val)
    then mk_EST_value(real_eq(a1.val,a2.val,op),
                                   ps.sto,tplus(a2.time,t_real_eq)) 
    elseif is_Int(a1.val) and is_Int(a2.val)
    then mk_EST_value(int_eq(a1.val,a2.val,op),
                                   ps.sto,tplus(a2.time,t_int_eq)) 
    elseif is_Void(a1.val) and is_Void(a2.val)
    then mk_EST_value(void_eq(a1.val,a2.val,op),
                                   ps.sto,tplus(a2.time,t_void_eq)) 
    else mk_EST_value(<err>,ps.sto,zerot);

eval_BoolOp : BinaryOperation -> Env -> PState -> EST_value
eval_BoolOp(mk_BinaryOperation(left,mk_BinaryOp(op),right))(e)(ps) ==
    let a1 = eval_MonOperation(left)(e)(ps) in
    let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
    if not (is_Tr(a2.val) and is_Tr(a2.val))
    then mk_EST_value(<err>,ps.sto,zerot)
    else cases op:
           <and> -> mk_EST_value(tr_and(a1.val,a2.val),ps.sto, 
                                       tplus(a2.time,t_and)),
           <or> -> mk_EST_value(tr_or(a1.val,a2.val),ps.sto,
                                     tplus(a2.time,t_and))
         end;

eval_Concat : BinaryOperation -> Env -> PState -> EST_value
eval_Concat(mk_BinaryOperation(left,op,right))(e)(ps)==
    let a1 = eval_MonOperation(left)(e)(ps) in
    let a2 = eval_MonOperation(right)(e)(mu(ps, time |-> a1.time)) in
    if not (is_Vector(a1.val) and is_Vector(a2.val))
    then mk_EST_value(<err>,ps.sto,zerot)
    elseif not (tleq(a1.val.type.type,a2.val.type.type) or
                tleq(a2.val.type.type,a1.val.type.type))
    then mk_EST_value(<err>, ps.sto,zerot)
    else let new_vec = vector_concat(a1.val,a2.val),
             new_time = tplus(a2.time, 
                   t_vector_concat(vector_length(a1.val.type),
                                   vector_length(a2.val.type))) in
         mk_EST_value(new_vec,ps.sto,new_time);

eval_Value: Value -> Env -> PState -> EST_value
eval_Value(mk_Value(val))(e)(ps) ==
  cases val:
    mk_ConstantValue(c) -> eval_ConstantValue(mk_ConstantValue(c))(ps),
    mk_NamedValue(n) -> eval_NamedValue(mk_NamedValue(n))(e)(ps),
    mk_VectorVal(v) -> eval_VectorVal(mk_VectorVal(v))(e)(ps),
    mk_StructureValue(s) -> eval_StructureValue(mk_StructureValue(s))(e)(ps),
    mk_Sequence(s) -> eval_Sequence(mk_Sequence(s))(e)(ps),
    mk_Call(id,acts) -> eval_Call(mk_Call(id,acts))(e)(ps),
    mk_Conditional(c) -> eval_Conditional(val)(e)(ps),
    mk_Widening(exp,t) -> eval_Widening(val)(e)(ps),
    mk_OuterLoop(l) -> eval_OuterLoop(val)(e)(ps)
  end;

eval_ConstantValue : ConstantValue -> PState -> EST_value
eval_ConstantValue(mk_ConstantValue(cv))(ps) ==
  cases cv:
    mk_IntegerDenotation(z) ->
        let rep = if abs z >= bytemax then <word> else <byte> in
        mk_EST_value(mk_Int(z,mk_IntType(rep,{z},{})),ps.sto,ps.time),
    mk_FloatingDenotation(r) ->
        mk_EST_value(mk_Real(r,mk_Float({mk_Floatrng(floor r, if
                          is_int(r) then r else floor (r +
                          0.5))},0,0,{})),ps.sto,ps.time),
    mk_BooleanDenotation(b) ->
        mk_EST_value(mk_Tr(b,mk_TrType({b},{})),ps.sto,ps.time),
    mk_Ascii_Char(c) ->
        mk_EST_value(mk_Int(ascii(c),mk_IntType(<byte>,{ascii(c)},{})), 
                ps.sto, ps.time),
    mk_Ascii_string(s) ->
        mk_EST_value(mk_Vector([mk_Int(ascii(a),
                                       mk_IntType(<byte>,{ascii(a)}, {})) 
                             |  a in seq s],
                     mk_VectorType(1,len s, seqlub([mk_IntType(<byte>,
                    {ascii(a)},{}) | a in seq s]),{})),ps.sto,ps.time),
    mk_Flavouring(fl) ->
  mk_EST_value(mk_Void(<nil>, mk_VoidType(eval_Flavouring(cv))), ps.sto, ps.time),
    <skip> -> mk_EST_value(mk_Void(<nil>,mk_VoidType({})), ps.sto,
                       tplus(ps.time, t_skip)) 
    end;

eval_NamedValue : NamedValue -> Env -> PState -> EST_value
eval_NamedValue(mk_NamedValue(nv))(e)(ps) ==
  cases nv :
    mk_FlavourExtract(n,fl) -> eval_FlavourExtract(nv)(e)(ps),
    mk_FlavourStrip(n,fl) -> eval_FlavourStrip(nv)(e)(ps),
    mk_VectorExtract(n,i) -> eval_VectorExtract(nv)(e)(ps),
    mk_VectorTrimming(n,t,i) -> eval_VectorTrimming(nv)(e)(ps),
    others -> eval_Identifier(nv)(e)(ps)
  end;


eval_Identifier : Id -> Env -> PState -> EST_value
eval_Identifier(id)(mk_(m,l))(mk_PState(sto,time)) ==
  if id in set dom m
  then cases access_env(id)(mk_(m,l)):
        mk_Location(l) -> let mk_Storable_value(v) = 
                               access (mk_Location(l))(sto) in
                   mk_EST_value(v,sto,tplus(time,t_access)),
        mk_Storable_value(v) -> mk_EST_value(v,sto,time)
       end
  else mk_EST_value(<err>,sto,time);

eval_FlavourExtract : FlavourExtract -> Env -> PState -> EST_value
eval_FlavourExtract(mk_FlavourExtract(nv,fl))(e)(ps) ==
  let n = eval_NamedValue(nv)(e)(ps),
      f = eval_Flavouring(fl) in
  if not is_Structure(n.val)
  then mk_EST_value(<err>,ps.sto,ps.time)
  else mk_EST_value(comp_extract(n.val,f),ps.sto,tplus(n.time,t_comp_extract));


eval_Flavouring : Flavouring -> Flavdom
eval_Flavouring(mk_Flavouring(fls)) ==
  if fls = []
  then {}
  else {eval_Flavour(hd fls)} union eval_Flavouring(mk_Flavouring(tl fls));

eval_Flavour : Flavour -> Fl_elt
eval_Flavour(mk_Flavour(name,index)) ==
  mk_Fl_elt(name,index);

eval_FlavourStrip : FlavourStrip -> Env -> PState -> EST_value
eval_FlavourStrip(mk_FlavourStrip(nv,fl))(e)(ps) ==
  let n = eval_NamedValue(nv)(e)(ps),
      f = eval_Flavouring(fl) in
  if not is_Structure(n.val)
  then mk_EST_value(<err>,ps.sto,ps.time)
  else let n' = comp_extract(n.val,f) in
       let n'' = mk_Structure(n'.val,mk_StructureType(n'.type.tps,{})) in
       mk_EST_value(n'',ps.sto,tplus(n.time,t_comp_extract));

eval_VectorExtract : VectorExtract -> Env -> PState -> EST_value
eval_VectorExtract(mk_VectorExtract(n,i))(e)(ps) ==
  let x = eval_NamedValue(n)(e)(ps) in
  if not is_Vector(x.val)
  then mk_EST_value(<err>,ps.sto,ps.time)
  else let index = eval_Operation(i)(e)(mu(ps, time |-> x.time)),
           length = x.val.type.upper - x.val.type.lower + 1 in
       if not is_Int(index.val)
       then mk_EST_value(<err>,ps.sto,ps.time)
       elseif not (index.val.type.range subset
                    {x.val.type.lower,...,x.val.type.upper}) 
       then mk_EST_value(<err>,ps.sto,ps.time)
       else mk_EST_value(vector_extract(x.val,index.val.val),
                          ps.sto,tplus(index.time,t_vector_extract(length)));



eval_VectorTrimming : VectorTrimming -> Env -> PState -> EST_value
eval_VectorTrimming(mk_VectorTrimming(name,to_p,ctv))(e)(ps)==
  let vec = eval_NamedValue(name)(e)(ps) in
  if not is_Vector(vec.val) or (is_Vector(vec.val) and
      not (is_Float(vec.val.type.type) or is_IntType(vec.val.type.type)))
  then mk_EST_value(<err>,ps.sto,zerot)
  else let v = eval_CompileTimeValue(ctv)(e) in
       if not (is_Real(v.val) or is_Int(v.val))
       then mk_EST_value(<err>,ps.sto,zerot)
       else let new_v = cases to_p:
                          <gtvalue> -> 
                             [i | i in seq vec.val.val & i >= v.val.val],
                          <ltvalue> -> 
                             [i | i in seq vec.val.val & i <= v.val.val],
                          <atvalue> -> 
                             [i | i in seq vec.val.val & i = v.val.val]
                        end in
            if new_v = []
            then mk_EST_value(<err>,ps.sto,zerot)
            else let new_l = vec.val.type.lower,
                     new_u = vec.val.type.lower + len new_v - 1,
                new_t = seqlub([const_type(v) | v in seq new_v]),
                     new_fl = vec.val.type.fl in
                 let new_vec = mk_Vector(new_v,mk_VectorType(new_l,new_u,new_t,
                                                   new_fl)),
                     new_time = tplus(vec.time,
                                         t_trimming_op(new_u-new_l)) in
                 mk_EST_value(new_vec,ps.sto,new_time);

eval_CompileTimeValue : CompileTimeValue -> Env -> EST_value
eval_CompileTimeValue(mk_CompileTimeValue(op))(mk_(m,l)) ==
  let locs = {id | id in set dom m & is_Location(m(id))} in
  let new_m = locs <-: m in
  let new_env = mk_(new_m,l) in
      eval_Operation(op)(new_env)(mk_PState({|->},zerot));

eval_VectorVal : VectorVal -> Env -> PState -> EST_value
eval_VectorVal(mk_VectorVal(ops))(e)(ps) ==
  let vals = [ eval_Operation(o)(e)(mk_PState(ps.sto,zerot)) | o in seq ops] in
  let val = [ v.val | v in seq vals],
      time = dtplus([v.time | v in seq vals]) in
  if <err> in set elems val
  then mk_EST_value(<err>,ps.sto,zerot)
  else let type = seqlub([v.type | v in seq val]) in
       if type = <err> 
       then mk_EST_value(<err>,ps.sto,zerot)
       else let tp = mk_VectorType(1,len val, type, {}) in
            let x = mk_Vector(val,tp) in
            mk_EST_value(x,ps.sto,time);

eval_StructureValue: StructureValue -> Env -> PState -> EST_value
eval_StructureValue(mk_StructureValue(ops))(e)(ps) ==
  let vals = [ eval_Operation(o)(e)(mk_PState(ps.sto,zerot)) | o in seq ops] in
  if (exists val in seq vals & 
        not (is_Tr(val.val) or is_Int(val.val) or is_Real(val.val)))
  then mk_EST_value(<err>,ps.sto,zerot)
  elseif exists v1,v2 in seq vals & fleq(v1.val.type,v2.val.type)
  then mk_EST_value(<err>,ps.sto, zerot)
  else let tps = [v.val.type | v in seq vals],
           time = dtplus([v.time | v in seq vals]),
           comps = [v.val.val | v in seq vals] in
       let type = mk_StructureType(tps,{}) in
       let val = mk_Structure(comps,type) in
       mk_EST_value(val,ps.sto,time);

eval_Sequence : Sequence -> Env -> PState -> EST_value
eval_Sequence(mk_Sequence(exprs))(e)(ps) ==
  let x = eval_Expression(hd exprs)(e)(ps) in
  if len exprs = 1 
  then x
  elseif is_Void(x.val)
  then eval_Sequence(mk_Sequence(tl exprs))(e)(mk_PState(x.sto,x.time))
  else mk_EST_value(<err>,ps.sto,zerot);

eval_Call : Call -> Env -> PState -> EST_value
eval_Call(mk_Call(id,acts))(mk_(m,l))(mk_PState(sto,time)) ==
  if id not in set dom m
  then mk_EST_value(<err>,sto,zerot)
  else let pp = access_env(id)(mk_(m,l)) in
       if not is_Proc(pp)
       then mk_EST_value(<err>,sto,zerot)
       else let mk_Proc(p) = pp in
            let params =  eval_Acts(acts)(mk_(m,l))(
                          mk_PState(sto,time)) in
              if <err> in set {x.val | x in seq params}
              then mk_EST_value(<err>,sto,zerot)
              else p([m.val | m in seq params]) 
                    (mk_PState(sto, params(len params).time));

eval_Acts: seq of Operation -> Env -> PState -> seq of EST_value
eval_Acts(ops)(e)(ps) ==
  if ops = []
  then []
  else let x = eval_Operation(hd ops)(e)(ps) in
       [x]^eval_Acts(tl ops)(e)(mk_PState(ps.sto,x.time));

eval_Widening : Widening -> Env -> PState -> EST_value
eval_Widening(mk_Widening(expr,dest_type))(e)(ps) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then mk_EST_value(<err>, ps.sto, zerot)
  else let xt = x.val.type,
           dt = eval_Type(dest_type)(e) in
       if dt=<err> 
       then mk_EST_value(<err>, ps.sto, zerot)
       else let dt' = phi_remove(dt) in
            if gt(dt',xt)
            then mk_EST_value(widen_type(x.val,dt'), ps.sto, x.time)
            else mk_EST_value(<err>, ps.sto, zerot);

eval_Type : Type -> Env -> (Expressible_type | Errvalue)
eval_Type(mk_Type(tp))(e) ==
  cases tp:
    mk_PrimitiveType(p) -> eval_PrimitiveType(tp)(e),
    mk_VecType(range,tpe) -> eval_VecType(tp)(e),
    mk_StrucType(tps) -> eval_StrucType(tp)(e),
    mk_FlavouredType(fl,tpe) -> eval_FlavouredType(tp)(e),
    mk_UnionTp(tps) -> eval_UnionTp(tp)(e),
    mk_TypeName(id) -> eval_TypeName(tp)(e)
  end;

eval_PrimitiveType : PrimitiveType -> Env -> (Expressible_type | Errvalue)
eval_PrimitiveType(mk_PrimitiveType(pt))(e) ==
  if is_Number(pt)
  then eval_Number(pt)(e)
  elseif is_FloatType(pt)
  then eval_FloatType(pt)(e)
  else eval_VoidValType(pt)(e);

eval_Number : Number -> Env -> (Expressible_type | Errvalue)
eval_Number(mk_Number(rep,range))(e) ==
  let ranges = { eval_Range(r)(e) | r in seq range} in
  if <err> in set ranges
  then <err>
  elseif rep = <bit>
  then if exists v in set dunion ranges & v not in set {0,1}
       then <err>
       else let m = { 0 |-> false, 1 |-> true} in
            mk_TrType({m(v) | v in set dunion ranges},{})
  elseif rep = <byte>
  then if exists v in set dunion ranges & abs v > bytemax
       then <err>
       else mk_IntType(rep,dunion ranges, {})
  elseif exists v in set dunion ranges & abs v > maxint
  then <err>
  else mk_IntType(rep,dunion ranges, {});

eval_Range : Range -> Env -> (set of int | Errvalue)
eval_Range(mk_Range(lower,upper))(e) ==
  if (lower = nil and upper = nil) or
     (lower <> nil and not is_Int((eval_CompileTimeValue(lower)(e)).val)) or
     (upper <> nil and not is_Int((eval_CompileTimeValue(upper)(e)).val))
  then <err>
  elseif lower=nil
  then { x | x: int & 0 <= x and x <= (eval_CompileTimeValue(upper)(e)).val.val}
  elseif upper = nil
  then { x | x: int & (eval_CompileTimeValue(lower)(e)).val.val <= x and
                      x <= maxint}
  else { x | x: int & (eval_CompileTimeValue(lower)(e)).val.val <= x and
                      x <= (eval_CompileTimeValue(upper)(e)).val.val};

eval_FloatType : FloatType -> Env -> (Expressible_type | Errvalue)
eval_FloatType(mk_FloatType(ranges,abserr,relerr))(e) ==
  if (abserr = nil and relerr = nil) or
     (exists range in seq ranges & (eval_Range(range)(e)) = <err>)
  then <err>
  else let abse = if abserr = nil
                  then mk_Real(0,mk_Float({mk_Floatrng(0,0)},0,0,{}))
                  else (eval_CompileTimeValue(abserr)(e)).val,
           rele = if relerr = nil
                  then mk_Real(0,mk_Float({mk_Floatrng(0,0)},0,0,{}))
                  else (eval_CompileTimeValue(relerr)(e)).val in
       if not(is_Real(abse) and is_Real(rele))
       then <err>
       else mk_Float({mk_Floatrng(min(eval_Range(range)(e)),
                                  max(eval_Range(range)(e))) | range
                        in seq ranges}, abse.val,rele.val,{});

eval_VoidValType : VoidValType -> (Env -> (Expressible_type | Errvalue))
eval_VoidValType(fl) == 
  lambda e: Env & mk_VoidType(eval_Flavouring(fl));

eval_StrucType : StrucType -> Env -> (Expressible_type | Errvalue)
eval_StrucType(mk_StrucType(tps))(e) ==
  let typs = [ eval_Type(t)(e) | t in seq tps] in
  if exists tp in seq typs & 
         not (is_TrType(tp) or is_Float(tp) or is_IntType(tp))
  then <err>
  elseif exists tp1,tp2 in seq typs & 
         tp1 <> tp2 and tp1.fl = tp2.fl
  then <err>
  else mk_StructureType(typs,{});

eval_VecType : VecType -> (Env -> (Expressible_type | Errvalue))
eval_VecType(mk_VecType(range,tp)) == lambda e : Env & 
  let typ = eval_Type(tp)(e),
      nrange = eval_Range(range)(e) in
  if typ = <err> or nrange = <err>
  then <err>
  else mk_VectorType(min(nrange),max(nrange),typ,{});

eval_FlavouredType : FlavouredType -> Env -> (Expressible_type | Errvalue)
eval_FlavouredType(mk_FlavouredType(fl,tp))(e) ==
  let flavour = eval_Flavouring(fl),
      typ = eval_Type(tp)(e) in
  if typ = <err>
  then <err>
  else   cases typ:
    mk_VoidType(t) -> mk_VoidType(t union flavour),
    mk_TrType(range,fl) -> mk_TrType(range,fl union flavour),
    mk_IntType(rep,range,fl) -> mk_IntType(rep,range, fl union flavour),
    mk_Float(range,abse,rele,fl) -> mk_Float(range,abse,rele,fl union flavour),
    mk_VectorType(lower,upper,tp,fl) ->
                      mk_VectorType(lower,upper,tp, fl union flavour),
    mk_StructureType(tps,fl) -> mk_StructureType(tps,fl union flavour),
    mk_UnionType(tps,fl) -> mk_UnionType(tps,fl union flavour)
  end;

eval_UnionTp : UnionTp -> Env -> (Expressible_type | Errvalue)
eval_UnionTp(mk_UnionTp(tps))(e) ==
  let typs = {eval_Type(t)(e) | t in seq tps} in
  if exists tp in set typs &  not (is_IntType(tp) or is_Float(tp) or 
                        is_TrType(tp) or is_VoidType(tp))
  then <err>
  elseif exists t1,t2 in set typs & fleq(t1,t2)
  then <err>
  else mk_UnionType(typs,{});

eval_TypeName : TypeName -> Env -> (Expressible_type | Errvalue)
eval_TypeName(mk_TypeName(id))(mk_(m,l)) ==
  if id in set dom m
  then cases access_env(id)(mk_(m,l)):
         mk_Location(l),mk_Storable_value(v),
              mk_Proc(p),<err> -> <err>,
         t -> t
       end
  else <err>;


eval_Scope : Scope -> Env -> PState -> EST_value
eval_Scope(mk_Scope(s))(e)(ps) ==
  if is_SimpleScope(s)
  then eval_SimpleScope(s)(e)(ps)
  else eval_PackageScope(s)(e)(ps);

eval_SimpleScope : SimpleScope -> Env -> PState -> EST_value
eval_SimpleScope(mk_SimpleScope(decls,expr))(e)(ps) ==
  let old_env_st = mk_(e,ps) in
  let new_env_st = eval_Decls(decls)(old_env_st) in
  if new_env_st = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let mk_(new_env,new_sto) = new_env_st in
       eval_Expression(expr)(new_env)(new_sto);

eval_Decls: seq of Declaration -> EnvState -> EnvState 
eval_Decls(decls)(env_st) ==
  if env_st = <err>
  then <err>
  elseif decls = []
  then env_st
  else eval_Decls(tl decls)(eval_Declaration(hd decls)(env_st));

eval_Declaration : Declaration -> EnvState -> EnvState
eval_Declaration(decl)(env_st) ==
  cases decl :
    mk_ImportDecl(id,tp) -> eval_ImportDecl(decl)(env_st),
    mk_ExportDecl(id,expr) -> eval_ExportDecl(decl)(env_st),
    mk_LetDecl(l) -> eval_LetDecl(decl)(env_st),
    mk_VarDecl(id,expr) -> eval_VarDecl(decl)(env_st),
    mk_ProcDec(nls,ph,expr) -> eval_ProcDec(decl)(env_st),
    mk_TypeDec(id,type) -> eval_TypeDec(decl)(env_st)
  end;

eval_ImportDecl : ImportDecl -> EnvState -> EnvState
eval_ImportDecl(mk_ImportDecl(id,tp))(mk_(e,ps)) ==
  let type = eval_Type(tp)(e) in
  if type = <err>
  then <err>
  else let val = choose(type),
           mk_(l,n_e) = reserve_locn(e) in
       let nn_e = update_env(id)(l)(n_e),
           sto = update(l)(mk_Storable_value(val))(ps.sto),
           t = tplus(ps.time,t_update) in
       mk_(nn_e,mk_PState(sto,t));

eval_ExportDecl : ExportDecl -> EnvState -> EnvState
eval_ExportDecl(mk_ExportDecl(id,expr))(mk_(e,ps)) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then <err>
  else let mk_(l,n_e) = reserve_locn(e) in
       let nn_e = update_env(id)(l)(n_e),
           sto = update(l)(mk_Storable_value(x.val))(ps.sto),
           t = tplus(ps.time,t_update) in
       mk_(nn_e,mk_PState(sto,t));

eval_LetDecl : LetDecl -> EnvState -> EnvState
eval_LetDecl(mk_LetDecl(decl))(es) ==
  if is_SimpleLetDecl(decl)
  then eval_SimpleLetDecl(decl)(es)
  else eval_StrucLetDecl(decl)(es);

eval_SimpleLetDecl : SimpleLetDecl -> EnvState -> EnvState
eval_SimpleLetDecl(mk_SimpleLetDecl(id,expr))(mk_(e,ps)) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then <err>
  else mk_((update_env(id)(x.val)(e)),
                   mk_PState(ps.sto, x.time));

eval_StrucLetDecl : StrucLetDecl -> EnvState -> EnvState
eval_StrucLetDecl(mk_StrucLetDecl(ids,expr))(mk_(e,ps)) ==
  let x = eval_Expression(expr)(e)(ps) in
  if not is_Structure(x.val)
  then <err>
  elseif len ids <> struc_length(x.val.type)
  then <err>
  else let id_vals = [ mk_(ids(i),
                          construct_ev(x.val.val(i),x.val.type.tps(i))) | 
                             i in set inds ids] in
       let new_env = multi_update_env(id_vals)(e) in
       mk_(new_env,mk_PState(ps.sto,x.time));

eval_VarDecl : VarDecl -> EnvState -> EnvState
eval_VarDecl(mk_VarDecl(id,expr))(mk_(e,ps)) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then <err>
  else let mk_(l,n_e) = reserve_locn(e) in
       let nn_e = update_env(id)(l)(n_e),
           sto = update(l)(mk_Storable_value(x.val))(ps.sto),
           t = tplus(ps.time,t_update) in
       mk_(nn_e,mk_PState(sto,t));

eval_ProcDec : ProcDec -> EnvState -> EnvState
eval_ProcDec(mk_ProcDec(nls,ph,expr))(mk_(e,ps)) ==
  let env_st = eval_NonLocals(nls)(e)(ps) in
  if env_st = <err>
  then <err>
  else let mk_ProcHeading(id,formals) = ph,
           mk_(ne,ns) = env_st in
       let fls = eval_Formals(formals)(e) in
       let pr = 
           mk_Proc(lambda a:Param & 
                     let nn_e = instantiate_formals(fls)(a)(ne) in
                     lambda nps: PState &
                       if nn_e = <err>
                       then mk_EST_value(<err>,nps.sto,zerot)
                       else let x = eval_Expression(expr)(nn_e)(nps) in
                            if x.val <> <err> and 
                               ((is_Void(x.val) and x.val.type = mk_VoidType({Phi}))
                                 or
                                 (not is_Void(x.val) and x.val.type.fl = {Phi}))
                            then mk_EST_value(<err>,nps.sto,zerot)
                            else x) in
       mk_(update_env(id)(pr)(e),mk_PState(ps.sto, ns.time));

eval_NonLocals : NonLocals -> Env -> PState -> EnvState
eval_NonLocals(mk_NonLocals(ids,decls))(mk_(m,l))(ps) ==
  let ids_map = if ids = nil then {|->} else (elems ids) <: m in
  if decls = nil
  then mk_(mk_(ids_map,l),ps)
  else eval_Decls(decls)(mk_(mk_(ids_map,l),ps));

eval_Formals : seq of Formal -> Env -> seq of Formal_elt
eval_Formals(fls)(e) ==
  [eval_Formal(f)(e) | f in seq fls];

eval_Formal : Formal -> Env -> Formal_elt
eval_Formal(mk_Formal(id,rep,fl))(e) ==
  let n_rep = eval_Representation(rep)(e),
      n_fl = eval_Flavouring(fl) in
  mk_Formal_elt(id,n_rep,n_fl);

eval_Representation : Representation -> Env -> (Expressible_type | Errvalue)
eval_Representation(rep)(e) ==
  cases rep:
    mk_PrimitiveRep(p) -> eval_PrimitiveRep(rep)(e),
    mk_StrucRep(rs) -> eval_StrucRep(rep)(e),
    mk_VecRep(range,r) -> eval_VecRep(rep)(e),
    mk_UnionRep(rs) -> eval_UnionRep(rep)(e),
    mk_FlavouredRep(f,r) -> eval_FlavouredRep(rep)(e),
    mk_Type(t) -> eval_Type(rep)(e)
  end;

eval_PrimitiveRep : PrimitiveRep -> Env -> (Expressible_type | Errvalue)
eval_PrimitiveRep(mk_PrimitiveRep(rep))(e) ==
  if is_NumRep(rep)
  then eval_NumRep(rep)(e)
  else eval_FloatRep(rep)(e);

eval_NumRep : NumRep -> Env -> (Expressible_type | Errvalue)
eval_NumRep(mk_NumRep(rep,range))(e) ==
  let ranges = if range = nil then {}
               else {eval_Range(r)(e) | r in seq range} in
  if <err> in set ranges
  then <err>
  elseif rep = <bit>
  then if exists v in set dunion ranges & v not in set {0,1}
       then <err>
       else let rngs = if range = nil then {true,false}
                       else {{0 |-> false, 1 |-> true}(r) | r in set
                            dunion ranges} in
            mk_TrType(rngs,{})
   elseif rep = <byte>
   then if exists v in set dunion ranges & abs v > bytemax
        then <err>
        else let rngs = if range = nil then {-bytemax,...,bytemax}
                        else dunion ranges in
             mk_IntType(rep,rngs,{})
   elseif exists v in set dunion ranges & abs v > maxint
   then <err>
   else let rngs = if range = nil then {-maxint,...,maxint}
                   else dunion ranges in
        mk_IntType(rep,rngs,{});

eval_FloatRep : FloatRep -> Env -> (Expressible_type | Errvalue)
eval_FloatRep(mk_FloatRep(range,abserr,relerr))(e) ==
  let ranges = if range = nil then {} 
               else {eval_Range(r)(e) | r in seq range},
      abse   = if abserr = nil 
               then mk_Real(maxint,
                            mk_Float({mk_Floatrng(maxint,maxint)},0,0,{}))
               else eval_CompileTimeValue(abserr)(e),
      rele   = if relerr = nil 
               then mk_Real(maxint,
                            mk_Float({mk_Floatrng(maxint,maxint)},0,0,{}))
               else eval_CompileTimeValue(relerr)(e) in
  if not (is_Real(abse.val) and is_Real(rele.val)) or <err> in set ranges 
  then <err>
  else let rngs = if range = nil
                  then {mk_Floatrng(-(beta ** maxint),beta ** maxint)}
                  else {mk_Floatrng(min(r),max(r)) | r in set ranges} in
       mk_Float(rngs, abse.val.val,rele.val.val,{});

eval_StrucRep : StrucRep -> Env -> (Expressible_type | Errvalue)
eval_StrucRep(mk_StrucRep(reps))(e) ==
  let tps = [ eval_Representation(r)(e) | r in seq reps] in
  if exists tp in seq tps & not(is_TrType(tp) or is_Float(tp) or
                                      is_IntType(tp))
  then <err>
  elseif exists tp1,tp2 in seq tps & fleq(tp1,tp2)
  then <err>
  else mk_StructureType(tps,{});

eval_VecRep : VecRep -> Env -> (Expressible_type | Errvalue)
eval_VecRep(mk_VecRep(range,rep))(e) ==
  let nrange = eval_Range(range)(e),
      type = eval_Representation(rep)(e) in
  if type = <err> or nrange = <err>
  then <err>
  else mk_VectorType(min(nrange),max(nrange),type,{});

eval_UnionRep : UnionRep -> Env -> (Expressible_type | Errvalue)
eval_UnionRep(mk_UnionRep(reps))(e) ==
  let tps = {eval_Representation(rep)(e) | rep in seq reps} in
  if exists tp in set tps & not (is_IntType(tp) or is_Float(tp) or
                                   is_TrType(tp) or is_VoidType(tp))
  then <err>
  elseif exists tp1,tp2 in set tps & fleq(tp1,tp2)
  then <err>
  else mk_UnionType(tps,{});

eval_FlavouredRep : FlavouredRep -> Env -> (Expressible_type | Errvalue)
eval_FlavouredRep(mk_FlavouredRep(fl,rep))(e) ==
  let type = eval_Representation(rep)(e),
      flav = eval_Flavouring(fl) in
  if type = <err> 
  then <err>
  else replace_flavour(type,flav); 

eval_TypeDec : TypeDec -> EnvState -> EnvState
eval_TypeDec(mk_TypeDec(id,tp))(mk_(e,ps)) ==
  let type = eval_Type(tp)(e) in
  if type = <err>
  then <err>
  else mk_(update_env(id)(type)(e),ps);

eval_PackageScope : PackageScope -> Env -> PState -> EST_value
eval_PackageScope(mk_PackageScope(ids,decls,expr))(mk_(m,l))(ps) ==
  let env_st = mk_(mk_(m,l),ps) in
  let new_env_st = eval_Decls(decls)(env_st) in
  if new_env_st = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let mk_(mk_(nm,nl),nps) = new_env_st in
       if not (elems ids subset (dom nm \ dom m))
       then mk_EST_value(<err>,ps.sto,zerot)
       else let ne = mk_(((elems ids) union dom m) <: nm, nl) in
            eval_Expression(expr)(ne)(nps);

eval_GuardedScope : GuardedScope -> Env -> PState -> EST_value
eval_GuardedScope(mk_GuardedScope(decls,incl,outcl))(e)(ps) ==
  let g_decl = eval_GuardedDeclarations(decls)(true)(e)(ps) in
  if g_decl = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let mk_(ne,nps,val) = g_decl in
       let in_val = eval_Sequence(incl)(ne)(nps),
           out_val = eval_Sequence(outcl)(ne)(nps) in
       if in_val.val = <err> or out_val.val = <err>
       then mk_EST_value(<err>,ps.sto, zerot)
       else let type = setlub({in_val.val.type,out_val.val.type}) in
            if type = <err>
            then mk_EST_value(<err>,ps.sto, zerot)
            else if val
                 then mk_EST_value(widen_type(in_val.val,type),in_val.sto,
                                   tplus(in_val.time,t_if))
                 else mk_EST_value(widen_type(out_val.val,type),out_val.sto,
                                   tplus(out_val.time,t_if));

eval_GuardedDeclarations : seq1 of GuardedDeclaration -> bool -> Env
                     -> PState -> ((Env * PState * bool) | Errvalue)
eval_GuardedDeclarations(decls)(b)(e)(ps) ==
  let gdcl = eval_GuardedDecl(hd decls)(e)(ps) in
  if len decls = 1
  then gdcl
  elseif gdcl = <err>
  then <err>
  else let mk_(ne,nps,tr) = gdcl in
       eval_GuardedDeclarations(tl decls)(b and tr)(ne)(nps);

eval_GuardedDecl : GuardedDeclaration -> Env -> PState -> ((Env *
                    PState * bool) | Errvalue) 
eval_GuardedDecl(decl)(e)(ps) ==
  if is_WhereDecl(decl)
  then eval_WhereDecl(decl)(e)(ps)
  else let d = eval_Declaration(decl)(mk_(e,ps)) in
       if d = <err> 
       then <err>
       else let mk_(ne,nps) = d in
            mk_(ne,nps,true);

eval_WhereDecl : WhereDecl -> Env -> PState -> ((Env * PState * bool) | Errvalue)
eval_WhereDecl(mk_WhereDecl(type,expr,id))(e)(ps) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then <err>
  else let t = eval_SkeletonType(type)(x.val.type)(e) in
       cases t: 
       <err> ->  <err>,
       others ->  let env = if id = nil
                            then e
                            else update_env(id)(x.val)(e) in
                  let xt = const_type(x.val) in
                  cases xt:
                     <err> -> <err>,
                     others -> let val = gt(t,xt) in
                               mk_(env, mk_PState(ps.sto,x.time),val)
                  end
       end;

eval_Assertion : Assertion -> Env -> PState -> EST_value
eval_Assertion(mk_Assertion(expr,tp))(e)(ps) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let type = eval_SkeletonType(tp)(x.val.type)(e) in
       if type = <err>
       then mk_EST_value(<err>,ps.sto,zerot)
       else let xt = const_type(x.val) in
            cases xt:
              <err> -> mk_EST_value(<err>,ps.sto,zerot),
              others -> 
                if not (tleq(type,x.val.type) and tleq(xt,type))
                then mk_EST_value(<err>,ps.sto,zerot)
                else let val = widen_type(x.val, phi_remove(type)) in
                     mk_EST_value(val,x.sto,tplus(x.time,t_widen_type))
            end;


eval_Conditional: Conditional -> Env -> PState -> EST_value
eval_Conditional(mk_Conditional(cond))(e)(ps) ==
  if is_IfThenOnly(cond)
  then eval_IfThenOnly(cond)(e)(ps)
  elseif is_IfThenElse(cond)
  then eval_IfThenElse(cond)(e)(ps)
  else eval_CaseExpr(cond)(e)(ps);

eval_IfThenOnly : IfThenOnly -> Env -> PState -> EST_value
eval_IfThenOnly(mk_IfThenOnly(prop,action))(e)(ps) ==
  let cond = eval_Expression(prop)(e)(ps),
      aseq = eval_Sequence(action)(e)(mu(ps,time |-> tplus(cond.time,t_if)))
                 in
  if not is_Tr(cond.val) or not is_Void(aseq.val)
  then mk_EST_value(<err>,ps.sto,zerot)
  elseif cond.val.val
  then aseq
  else mk_EST_value(mk_Void(<nil>,mk_VoidType({})),ps.sto,
                        tplus(ps.time,tplus(cond.time,t_if)));

eval_IfThenElse : IfThenElse -> Env -> PState -> EST_value
eval_IfThenElse(mk_IfThenElse(prop,thenaction,elseaction))(e)(ps) ==
  let cond = eval_Expression(prop)(e)(ps) in
  if not is_Tr(cond.val)
  then mk_EST_value(<err>,ps.sto,zerot)
  else let then_x = eval_Sequence(thenaction)(e)(ps),
           else_x = eval_Sequence(elseaction)(e)(ps) in
       let type = lub(then_x.val.type,else_x.val.type) in
       if type = <err>
       then mk_EST_value(<err>,ps.sto,zerot)
       elseif cond.val.val
       then mu(then_x, val |-> widen_type(then_x.val,type),
                       time |-> tplus(then_x.time,cond.time))
       else mu(else_x, val |-> widen_type(else_x.val,type),
                       time |-> tplus(else_x.time,cond.time));

eval_CaseExpr : CaseExpr -> Env -> PState -> EST_value
eval_CaseExpr(mk_CaseExpr(expr,limbs,outlimb))(e)(ps) ==
  let x = eval_Expression(expr)(e)(ps) in
  if x.val = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let type_x = x.val.type in
       let ls = eval_Limbs(limbs)(x.val)(e)(mu(ps,time |-> x.time)) in
       let os = if outlimb = nil
                then []
                else let mk_(t,v) = ls(len ls) in
                     [mk_(type_x,eval_Sequence(outlimb)(e)(mu(ps,time
                           |-> v.time)))] in
       let pats = ls^os in
       if exists mk_(t,v) in seq pats & v.val = <err>
       then mk_EST_value(<err>,ps.sto,zerot)
       else let patlub = setlub({t | mk_(t,v) in seq pats}) in
            if patlub = <err>
            then mk_EST_value(<err>,ps.sto,zerot)
            elseif lub(type_x,patlub) <> patlub
            then mk_EST_value(<err>,ps.sto,zerot)
            else let type = setlub({v.val.type | mk_(t,v) in seq pats}) in
                 if type = <err>
                 then mk_EST_value(<err>,ps.sto,zerot)
                 else let x_type = const_type(x.val) in
                      let matches = [p | p in seq pats &
                                      let mk_(t,v) = p in
                                      lub(x_type,t) = t] in
                      let mk_(mt,mv) = hd matches in
                      let time = 
                           dtplus([mv.time,t_const_type,t_widen_type]) in
                      mk_EST_value(widen_type(mv.val,type),mv.sto,time);

eval_Limbs : seq1 of CaseLimb -> Expressible_value -> Env -> PState ->
             seq1 of (Expressible_type * EST_value)
eval_Limbs(limbs)(x)(e)(ps) ==
  let mk_(t,v) = eval_Limb(hd limbs)(x)(e)(ps) in
  if len limbs = 1
  then [mk_(t,v)]
  else [mk_(t,v)]^(eval_Limbs(tl limbs)(x)(e)(mu(ps,time |-> v.time)));

eval_Limb : CaseLimb -> Expressible_value -> Env -> PState ->
            (Expressible_type * EST_value) 
eval_Limb(mk_CaseLimb(test,sequ))(x)(e)(ps) ==
  let t = eval_Tester(test)(x)(e)(ps) in
  if t = <err>
  then   mk_(mk_VoidType({}),mk_EST_value(<err>,ps.sto,zerot))
  else let mk_(type,env,tm) = t in
       let val = eval_Sequence(sequ)(env)(mu(ps,time |-> tm)) in
       if val.val = <err>
       then   mk_(mk_VoidType({}),mk_EST_value(<err>,ps.sto,zerot))
       else mk_(type,val);




eval_Tester : Tester -> Expressible_value -> Env -> PState -> 
              ((Expressible_type * Env * Time) | Errvalue)
eval_Tester(tester)(x)(e)(ps) ==
  cases tester:
    mk_SkeletonType(t) -> 
          let nt = eval_SkeletonType(tester)(x.type)(e) in
          if nt = <err> 
          then <err>
          else mk_(nt,e,ps.time),
    mk_StrucTest(s) -> eval_StrucTest(tester)(x)(e)(ps),
    mk_NonStrucTest(id,tp,fl) -> eval_NonStrucTest(tester)(x)(e)(ps)
  end;


eval_SkeletonType : SkeletonType -> Expressible_type -> Env ->
                     (Expressible_type | Errvalue)
eval_SkeletonType(mk_SkeletonType(skel))(t)(e) == 
  cases skel:
    mk_Type(t) -> eval_Type(skel)(e),
    mk_NumSkel(r,er) -> eval_NumSkel(skel)(t)(e),
    mk_StrucSkel(s) -> eval_StrucSkel(skel)(t)(e),
    mk_FlavSkel(s,fl) -> eval_FlavSkel(skel)(t)(e),
    mk_VecSkel(s) -> eval_VecSkel(skel)(t)(e),
    mk_UnionSkel(s) -> eval_UnionSkel(skel)(t)(e)
  end;

eval_NumSkel : NumSkel -> Expressible_type -> Env -> 
               (Expressible_type | Errvalue)
eval_NumSkel(mk_NumSkel(ranges,errors))(x_type)(e) ==
  if not (is_TrType(x_type) or is_IntType(x_type) or is_Float(x_type))
  then <err>
  else let rngs = if ranges = nil
                  then if is_Float(x_type) 
                       then {{l,...,u} | mk_Floatrng(l,u) in set x_type.range} 
                       else {x_type.range}
                  else {eval_Range(r)(e) | r in seq ranges} in
       if <err> in set rngs
       then <err>
       else cases x_type:
              mk_TrType(range,fl) -> 
                     if not (dunion rngs subset {0,1})
                     then <err>
                     else mk_TrType({{0 |->false, 1 |->
                          true}(v) | v in set dunion rngs},fl),
              mk_IntType(rep,range,fl) ->
                     if (rep = <byte> and exists v in set dunion rngs &
                                         abs v >= bytemax) or
                        (exists v in set dunion rngs & abs v >= maxint)
                     then <err>
                     else mk_IntType(rep,dunion rngs,fl),
              mk_Float(rs,abse,rele,fl) ->
                     if exists v in set dunion rngs & abs v >= maxint
                     then <err>
                     else
                       let abserr 
                         = if errors.abserr = nil 
                           then abse
                           else 
                            let v1 = 
                              (eval_CompileTimeValue(errors.abserr)(e)).val in
                            if v1 = <err>
                            then <err>
                            else v1.val,
                           relerr 
                         = if errors.relerr = nil 
                           then rele
                           else 
                            let v1 = 
                              (eval_CompileTimeValue(errors.relerr)(e)).val in
                            if v1 = <err>
                            then <err>
                            else v1.val in
                        if not (is_real(abserr) and is_real(relerr))
                        then <err>
                        else mk_Float({mk_Floatrng(min(r),max(r))
                              | r in set rngs},abserr,relerr,fl)
              end;

eval_StrucSkel : StrucSkel -> Expressible_type -> Env ->
                 (Expressible_type | Errvalue)
eval_StrucSkel(mk_StrucSkel(comps))(x_type)(e) ==
  if not is_StructureType(x_type)
  then <err>
  elseif struc_length(x_type) <> len comps
  then <err>
  else let t = [if comps(i) = <nil>
                then x_type.tps(i)
                else eval_SkeletonType(comps(i))(x_type.tps(i))(e) |
                      i in set inds comps] in
       if exists tp in seq t & not (is_TrType(tp) or
                   is_IntType(tp) or is_Float(tp))
       then <err>
       else mk_StructureType(t,x_type.fl);

eval_FlavSkel : FlavSkel -> Expressible_type -> Env ->
                (Expressible_type | Errvalue)
eval_FlavSkel(mk_FlavSkel(skel,fl))(x_type)(e) ==
  let t = eval_SkeletonType(skel)(x_type)(e),
      f = eval_Flavouring(fl) in
  if t = <err>
  then <err>
  else replace_flavour(t,f);

eval_VecSkel : VecSkel -> Expressible_type -> Env -> 
               (Expressible_type | Errvalue)
eval_VecSkel(mk_VecSkel(skel))(x_type)(e) ==
  let t = eval_SkeletonType(skel)(x_type)(e) in
  if t = <err> 
  then <err>
  else  cases x_type:
         mk_VectorType(l,u,tp,fl) -> mk_VectorType(l,u,t,fl),
         others -> <err>
        end;

eval_UnionSkel : UnionSkel -> Expressible_type -> Env ->
                 (Expressible_type | Errvalue)
eval_UnionSkel(mk_UnionSkel(skels))(x_type)(e) ==
  let fls = { skel |-> fl | skel in seq skels, fl : Flavdom & 
                   fl = cases skel:
                          mk_FlavSkel(skel,f) -> eval_Flavouring(f),
                          mk_FlavouredType(f,t) -> eval_Flavouring(f),
                          others -> eval_Flavouring(skel)
                        end} in
  if card dom fls <> card rng fls
  then <err>
  elseif is_UnionType(x_type)
  then let x_fls = merge{
                { mk_VoidType(f) |-> f | mk_VoidType(f) in set x_type.tps},
                { mk_IntType(rep,range,fl) |-> fl | 
                            mk_IntType(rep,range,fl) in set x_type.tps },
                { mk_TrType(range,fl) |-> fl | 
                            mk_TrType(range,fl) in set x_type.tps },
                { mk_Float(rs,a,r,fl) |-> fl | 
                            mk_Float(rs,a,r,fl) in set x_type.tps }}
                in
       if not (rng fls subset rng x_fls)
       then <err>
       else let tps = 
              { cases skel:
                  mk_FlavSkel(s,f)      ->  eval_FlavSkel(skel)(tp)(e),
                  mk_FlavouredType(f,t) -> eval_FlavouredType(skel)(e),
                  others                -> eval_VoidValType(skel)(e)
                end | skel in seq skels, tp in set x_type.tps &
                          fls(skel) = x_fls(tp)} in
            if exists tp in set tps & not (is_TrType(tp) or is_IntType(tp)
                   or is_Float(tp) or is_VoidType(tp))
            then <err>
            else mk_UnionType(tps,x_type.fl)
  else let fl = if is_VoidType(x_type)
                then x_type
                else x_type.fl in
       if fl not in set rng fls
       then <err>
       else let skel = iota s in set elems skels & fls(s) = fl in
            cases skel:
                  mk_FlavSkel(s,f)      -> eval_FlavSkel(skel)(x_type)(e),
                  mk_FlavouredType(f,t) -> eval_FlavouredType(skel)(e),
                  others                -> eval_VoidValType(skel)(e)
            end;

eval_NonStrucTest : NonStrucTest -> Expressible_value -> Env -> PState
                    -> ((Expressible_type * Env * Time) | Errvalue)
eval_NonStrucTest(mk_NonStrucTest(id,fl,skel))(x)(e)(ps) ==
  let t = eval_SkeletonType(skel)(x.type)(e) in
  if t = <err>
  then <err>
  else let t' = if fl = nil
                then t
                else replace_flavour(t,eval_Flavouring(fl)) in
       if id = nil
       then mk_(t',e,ps.time)
       else mk_(t',update_env(id)(x)(e), ps.time);

eval_StrucTest : StrucTest -> Expressible_value -> Env -> PState ->
                 ((Expressible_type * Env * Time) | Errvalue)
eval_StrucTest(mk_StrucTest(tests))(x)(e)(ps) ==
  if not is_Structure(x)
  then <err>
  elseif struc_length(x.type) <> len tests
  then <err>
  else let xs = [ construct_ev(x.val(i),x.type.tps(i)) | i in set inds
                                x.val] in
       let ts = eval_Testseq(tests)(xs)(e)(ps) in
       if ts = <err>
       then <err>
       else let mk_(tps,env,time) = ts in
            mk_(mk_StructureType(tps,x.type.fl),env,time);

eval_Testseq : seq of (NonStrucTest | <nil>) -> seq of Expressible_value 
               -> Env -> PState -> ((seq of Expressible_type * Env
               * Time) | Errvalue)
eval_Testseq(tests)(xs)(e)(ps) ==
  if tests = []
  then mk_([],e,ps.time)
  else let t = if hd tests = <nil>
               then mk_((hd xs).type, e, ps.time)
               else eval_NonStrucTest(hd tests)(hd xs)(e)(ps) in
       if t = <err>
       then <err>
       else let mk_(tp,env,time) = t in
            let ts = eval_Testseq(tl tests)(tl xs) (env) (mu(ps,time |-> time))
                    in
            if ts = <err>
            then <err>
            else let mk_(tps,n_env,n_time) = ts in
                 mk_([tp]^tps,n_env,n_time);

eval_OuterLoop : OuterLoop -> Env -> PState -> EST_value
eval_OuterLoop(mk_OuterLoop(oul))(e)(ps) ==
  if is_OuterIntLoop(oul)
  then eval_OuterIntLoop(oul)(e)(ps)
  else eval_OuterVecLoop(oul)(e)(ps);

eval_OuterIntLoop : OuterIntLoop -> Env -> PState -> EST_value
eval_OuterIntLoop(mk_OuterIntLoop(mk_OverRange(id,range),actns))(e)(ps) ==
  let nrange = eval_Range(range)(e) in
  if nrange = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let vec_elems = [eval_Sequence(actns)(update_env(id)
            (mk_Storable_value(mk_Int(i,mk_IntType(<word>,{i},{}))))(e))
                            (mu(ps,time |-> zerot)) | i in set nrange] in
       if <err> in set {x.val | x in seq vec_elems}
       then mk_EST_value(<err>,ps.sto,zerot)
       else let type = seqlub([i.val.type | i in seq vec_elems]),
                time = dtplus([i.time | i in seq vec_elems]) in
            if type = <err>
            then mk_EST_value(<err>,ps.sto,zerot)
            else let vec_val = if is_StructureType(type) or
                                  is_VectorType(type) 
                               then [ v.val.val | v in seq vec_elems]
                               else [ v.val | v in seq vec_elems]  in
                    mk_EST_value(mk_Vector(vec_val,mk_VectorType(1,len
                    vec_val,type,{})),ps.sto, tplus(ps.time,time));

eval_OuterVecLoop : OuterVecLoop -> Env -> PState -> EST_value
eval_OuterVecLoop(mk_OuterVecLoop(ovs,actions))(e)(ps) ==
  let idvs = eval_OverVectors(ovs)(e)(ps) in
  if idvs = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let time1 = dtplus([ let mk_(id,v,t) = i in t | i in seq idvs]),
           new_env = lambda i:nat &
                      (multi_update_env([ let mk_(id,v,t) = j in
                                        mk_(id,vector_extract(v,i)) |
                                            j in seq idvs]^(
                                        if ovs.cnt = nil then []
                                        else [mk_(ovs.cnt,i)]))(e)) in
       let vec_elems = [eval_Sequence(actions)(new_env(i))(mu(ps,time
                        |-> zerot)) | i in set let mk_(i1,v,t) =
                                 idvs(1) in inds (v.val)] in
       if <err> in set {x.val | x in seq vec_elems}
       then mk_EST_value(<err>,ps.sto,zerot)
       else let type = seqlub([i.val.type | i in seq vec_elems]),
                time = dtplus([i.time | i in seq vec_elems]^[time1]) in
            if type = <err>
            then mk_EST_value(<err>,ps.sto,zerot)
            else let new_tp = mk_VectorType(1,len vec_elems,type,{}) in
                 let vec_val = if is_StructureType(type) or
                                  is_VectorType(type) 
                               then [i.val.val | i in seq vec_elems]
                               else [i.val | i in seq vec_elems] in
                 let new_vec = mk_Vector(vec_val,new_tp) in
                 mk_EST_value(new_vec,ps.sto,tplus(ps.time,time));

eval_OverVectors : OverVectors -> Env -> PState -> (seq1 of (Id * Vector *
                   Time) | Errvalue)
eval_OverVectors(ovs)(e)(ps) ==
  let indices = [ let mk_OverVector(id,val) = o in
                  let x = eval_Operation(val)(e)(mu(ps,time |-> zerot)) in
                  mk_(id,x.val,x.time) | o in seq ovs.ovv] in
  if exists i in set inds indices & let mk_(id,v,t) = indices(i) in
                                    not is_Vector(v)
  then <err>
  else indices;

eval_InnerLoop : InnerLoop -> Env -> PState -> EST_value
eval_InnerLoop(mk_InnerLoop(innerl))(e)(ps) ==
  cases innerl:
    mk_IntLoop(inc,actions) -> eval_IntLoop(innerl)(e)(ps),
    mk_VecLoop(ovs,actions) -> eval_VecLoop(innerl)(e)(ps),
    mk_TimeLoop(time,actions) -> eval_TimeLoop(innerl)(e)(ps)
  end;

eval_IntLoop : IntLoop -> Env -> PState -> EST_value
eval_IntLoop(mk_IntLoop(inc,actions))(e)(ps) ==
  let idrng = eval_InnerControl(inc)(e)(ps) in
  if idrng = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let mk_(id,range) = idrng in
       let f: EST_Iterate -> EST_Iterate 
           = lambda x: EST_Iterate &
              let new_env = update_env(id)(
                              mk_Storable_value(mk_Int(range(x.i),
                                     mk_IntType(<word>,elems range,{}))))(e) in
              eval_SeqIterate(actions)(new_env)(x)         in
       let exi = (NIterate(f,(len range)))(mk_EST_Iterate(
                      mk_EST_value(mk_Void(<nil>,mk_VoidType({})),                              ps.sto,ps.time),1)) in
       exi.expst;

eval_InnerControl : InnerControl -> Env -> PState -> ((Id * seq of
                    int) | Errvalue)
eval_InnerControl(inc)(e)(ps) ==
  cases inc:
    mk_OverRange(cnt,range) ->
        let r = eval_Range(range)(e) in
        if r = <err> then <err> else mk_(cnt,[x | x in set r]),
    mk_PartialRange(cnt,from_b,to_b,inc) ->
        let b1 = eval_Operation(from_b)(e)(ps),
            b2 = eval_Operation(to_b)(e)(ps) in
        if not (is_Int(b1.val) and is_Int(b2.val))
        then <err>
        else let b3 = if inc = nil
                      then if b1.val.val <= b2.val.val
                           then mk_Int(1,mk_IntType(<byte>,{1,-1},{}))
                           else mk_Int(-1,mk_IntType(<byte>,{1,-1},{}))
                      else (eval_Operation(inc)(e)(ps)).val in
             if not (is_Int(b3.val)) or
                (is_Int(b3.val) and 
                   exists v1 in set b1.val.type.range, 
                          v2 in set b2.val.type.range, 
                          v3 in set b3.val.type.range & (v2-v1)*v3 < 0)
             then <err>
             else let r = [ b1.val.val + alpha * b3.val | alpha in set 
                         {0,...,floor(1+(b2.val.val-b1.val.val)/b3.val)} & 
                      abs (alpha * b3.val) <= abs (b2.val.val - b1.val.val)] in
                  mk_(cnt,r)
  end;

eval_SeqIterate : Sequence -> Env -> EST_Iterate -> EST_Iterate
eval_SeqIterate(sequ)(e)(exi) ==
  if exi.expst.val = <err>
  then mu(exi, i |-> exi.i + 1)
  else let new_expst = eval_Sequence(sequ)(e)(mk_PState(exi.expst.sto,exi.expst.time)) in
       mk_EST_Iterate(new_expst,exi.i + 1);

eval_VecLoop : VecLoop -> Env -> PState -> EST_value
eval_VecLoop(mk_VecLoop(ovs,actions))(e)(ps) ==
  let indices = eval_OverVectors(ovs)(e)(ps) in
  if indices = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  else let time = dtplus([let mk_(id,v,t) = i in t | i in seq indices]) in
       let f:EST_Iterate -> EST_Iterate
            = lambda x:EST_Iterate &
             let env = multi_update_env(
                   [let mk_(id,v,t) = indices(i) in
                   mk_(id,vector_extract(v,x.i)) |i in set inds indices])(e),
                 new_expst = mu(x.expst, time |-> x.expst.time)
                              in
             let new_env = if ovs.cnt = nil then env
                     else update_env(ovs.cnt)
        (mk_Storable_value(mk_Int(x.i,mk_IntType(<word>,{x.i},{}))))(env) in
             eval_SeqIterate(actions)(new_env)(mu(x,expst |-> new_expst)) in
       let mk_(-,v,-) = indices(1) in
       let exi = (NIterate(f,len v.val))(mk_EST_Iterate(mk_EST_value(
                     mk_Void(<nil>,mk_VoidType({})),
                         ps.sto,tplus(ps.time,time)),1))
                   in
       exi.expst;

eval_TimeLoop : TimeLoop -> Env -> PState -> EST_value
eval_TimeLoop(mk_TimeLoop(time,actions))(e)(ps) ==
  let t = eval_TimeInterval(time)(e),
      x = eval_Sequence(actions)(e)(mu(ps,time |-> zerot)) in
  if t = <err> or x.val = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  elseif exists n:nat & timeleq(dtplus([x.time | i in set {1,...,n}]),t)
  then let its = iota n:nat &
                  timeleq(dtplus([x.time | i in set {1,...,n}]),t) and
                  not (timeleq(dtplus([x.time | i in set {1,...,n+1}]),t)),
           f:EST_value ->EST_value = lambda exs:EST_value &
             eval_Sequence(actions)(e)(mk_PState(exs.sto,exs.time)) in
           (Iterate(f,its))(mk_EST_value(mk_Void(<nil>,mk_VoidType({})),
                                  ps.sto,ps.time))
  else mk_EST_value(<err>,ps.sto,zerot);

eval_Assignment : Assignment -> Env -> PState -> EST_value
eval_Assignment(mk_Assignment(ass))(env)(ps) ==
  cases ass:
    mk_NvAssignment(d,e) -> eval_NvAssignment(ass)(env)(ps),
    mk_MultAssignment(d,m,e) -> eval_MultAssignment(ass)(env)(ps),
    mk_StrAssignment(d,e) -> eval_StrAssignment(ass)(env)(ps)
  end;

eval_NvAssignment : NvAssignment -> Env -> PState -> EST_value
eval_NvAssignment(mk_NvAssignment(dest,expr))(e)(ps) ==
  let l = access_env(dest)(e) in
  if not is_Location(l)
  then mk_EST_value(<err>,ps.sto,zerot)
  else let x = eval_Expression(expr)(e)(ps) in
       if x.val = <err>
       then mk_EST_value(<err>,ps.sto,zerot)
       elseif cases x.val.type:
                mk_VoidType(t) -> t = {Phi},
                others -> x.val.type.fl = {Phi}
              end
       then mk_EST_value(<err>,ps.sto,zerot)
       else let mk_Storable_value(dest_val) = access(l)(ps.sto) in
            if gt(dest_val.type,x.val.type)
            then let new_sto =
       update(l)(mk_Storable_value(widen_type(x.val,dest_val.type)))(ps.sto) in
                 mk_EST_value(mk_Void(<nil>,mk_VoidType({})),new_sto,
                   tplus(tplus(ps.time,t_update),t_access))
            else mk_EST_value(<err>,ps.sto,zerot);

eval_MultAssignment : MultAssignment -> Env -> PState -> EST_value
eval_MultAssignment(mk_MultAssignment(dest,mult,expr))(e)(ps) ==
  let l = access_env(dest)(e) in
  if not is_Location(l)
  then mk_EST_value(<err>,ps.sto,zerot)
  else let mk_Storable_value(v) = access(l)(ps.sto) in
       if not is_Vector(v)
       then mk_EST_value(<err>,ps.sto,zerot)
       else let mk_Vector(val,type) = v in
            let v' = 
               eval_VectorMult(mk_EST_value(v,ps.sto,ps.time))(mult)(e) in
            let x = eval_Expression(expr)(e)(mk_PState(v'.sto,v'.time)) in
            if v'.val = <err> or not is_Vector(x.val)
            then mk_EST_value(<err>,ps.sto,zerot)
            elseif (x.val.type.upper - x.val.type.lower) <>
                     (v'.val.type.upper - v'.val.type.lower) or
                   not gt(v.type.type,x.val.type.type) or
              cases x.val.type.type:
                mk_VoidType(t) -> t = {Phi},
                others -> x.val.type.fl = {Phi}
              end
            then mk_EST_value(<err>,ps.sto,zerot)
            else let vleft = mk_Vector(vector_subv(val,type.lower,
                         v'.val.type.lower-1),mk_VectorType(type.lower,
                         v'.val.type.lower-1,type.type,type.fl)),
                     vmid = x.val,
                     vright = mk_Vector(vector_subv(val,v'.val.type.upper+1,
                         type.upper),mk_VectorType(v'.val.type.upper+1,
                         type.upper,type.type, type.fl)) in
                let new_vec = vector_concat(vector_concat(vleft,vmid),vright),
                    new_time = dtplus([x.time,t_vector_concat,
                              t_vector_concat, vector_subv,vector_subv]) in
                 mk_EST_value(mk_Void(<nil>,mk_VoidType({})), 
                                update(l)(mk_Storable_value(new_vec))(ps.sto),
                                 new_time);

eval_StrAssignment : StrAssignment -> Env -> PState -> EST_value
eval_StrAssignment(mk_StrAssignment(dest,expr))(e)(ps) ==
  let ls = [access_env(d)(e) | d in seq dest] in
  if exists l in seq ls & not is_Location(l)
  then mk_EST_value(<err>,ps.sto,zerot)
  else let x = eval_Expression(expr)(e)(ps) in
       if not is_Structure(x.val)
       then mk_EST_value(<err>,ps.sto,zerot)
       elseif len ls <> struc_length(x.val.type)
       then mk_EST_value(<err>,ps.sto,zerot)
       else let nvals = [ access(l)(ps.sto) | l in seq ls] in
            let vals = [ let mk_Storable_value(v) = i in v | i in seq nvals] in
            let dest_tps = [v.type | v in seq vals],
                x_tps = [i | i in seq x.val.type.tps] in
            if exists i in set inds dest_tps & not gt(dest_tps(i),x_tps(i))
            then mk_EST_value(<err>,ps.sto,zerot)
            else let ys = [mk_Storable_value(construct_ev(x.val.val(i),
                                x.val.type.tps(i))) | i in set inds x.val.val],
                     new_t = dtplus([x.time,t_access,t_construct_ev,
                                        t_multi_update(len ys)]) in
                 mk_EST_value(mk_Void(<nil>,mk_VoidType({})),
                    multi_update(ls)(ys)(ps.sto), new_t);


eval_TimedExpression : TimedExpression -> Env -> PState -> EST_value
eval_TimedExpression(mk_TimedExpression(texpr))(e)(ps) ==
  if is_TimeTakes(texpr)
  then eval_TimeTakes(texpr)(e)(ps)
  else eval_TimeAssertion(texpr)(e)(ps);

eval_TimeTakes : TimeTakes -> Env -> PState -> EST_value
eval_TimeTakes(mk_TimeTakes(expr,time))(e)(ps) ==
  let x = eval_Expression(expr)(e)(mu(ps, time |-> zerot)),
      t = eval_TimeInterval(time)(e) in
  if x.val = <err> or t = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  elseif timeleq(x.time,t)
  then mu(x,time |-> tplus(ps.time,x.time))
  else mk_EST_value(<err>,ps.sto,zerot);

eval_TimeInterval : TimeInterval -> Env -> (Time | Errvalue)
eval_TimeInterval(time)(e) ==
  let range = eval_Range(time)(e) in
  if range = <err> or min(range) < 0
  then <err>
  else mk_(min(range),max(range));

eval_TimeAssertion:TimeAssertion -> Env -> PState -> EST_value
eval_TimeAssertion(mk_TimeAssertion(expr,time))(e)(ps) ==
  let x = eval_Expression(expr)(e)(mu(ps, time |-> zerot)),
      t = eval_TimeInterval(time)(e) in
  if x.val = <err> or t = <err>
  then mk_EST_value(<err>,ps.sto,zerot)
  elseif timeleq(t,x.time)
  then mu(x,time |-> tplus(ps.time,t))
  else mk_EST_value(<err>,ps.sto,zerot);

Iterate: (EST_value -> EST_value) * nat -> (EST_value ->
           EST_value) 
Iterate(f,n) ==
  if n = 0 
  then lambda x:EST_value & x
  elseif n = 1
  then f
  else f comp (Iterate( f, n-1));

NIterate: (EST_Iterate -> EST_Iterate) * nat -> (EST_Iterate ->
           EST_Iterate) 
NIterate(f,n) ==
  if n = 0 
  then lambda x:EST_Iterate & x
  elseif n = 1
  then f
  else f comp (NIterate( f, n-1))