MPoly.pvs

%%
%% This file is featured twice in the movie "The Martian". For details, see: 
%% http://shemesh.larc.nasa.gov/people/cam/TheMartian/
%% Authors: Cesar Munoz and Anthony Narkawicz 
%% NASA Langley Research Center
%%

MPoly : THEORY
BEGIN

  IMPORTING util,
            multi_polynomial

  mpoly        : VAR MultiPolynomial
  mdeg         : VAR DegreeMono
  mcoeff       : VAR Coeff
  nvars,terms  : VAR posnat
  rel          : VAR RealOrder
  Avars,Bvars  : VAR Vars
  boundedpts,
  intendpts    : VAR IntervalEndpoints

  MPoly : TYPE = [#
    mpoly  : MultiPolynomial,
    mdeg   : DegreeMono,
    terms  : posnat,
    mcoeff : Coeff
  #]
 
  mk_mpoly(mpoly,mdeg,terms,mcoeff) : MACRO MPoly = (#
    mpoly  := mpoly,
    mdeg   := mdeg,
    terms  := terms,
    mcoeff := mcoeff
  #)

  MPolyRel : TYPE = MPoly WITH [# rel:RealOrder #]

  mk_mpoly(mpoly,mdeg,terms,mcoeff,rel) : MACRO MPolyRel = (#
    mpoly  := mpoly,
    mdeg   := mdeg,
    terms  := terms,
    mcoeff := mcoeff,
    rel    := rel
  #)

  mpolyrel2mpoly(mpr:MPolyRel): MACRO MPoly = (#
    mpoly  := mpr`mpoly,
    mdeg   := mpr`mdeg,
    terms  := mpr`terms,
    mcoeff := mpr`mcoeff
  #)

  CONVERSION mpolyrel2mpoly

  MVars : TYPE = [#
    numvars : posnat,
    vars_lb,
    vars_ub : Vars, 
    iepts,
    bdpts   : IntervalEndpoints
  #]

  mk_mvars(nvars,Avars,Bvars,intendpts,boundedpts) : MACRO MVars = (#
    numvars := nvars,
    vars_lb := Avars,
    vars_ub := Bvars,
    iepts   := intendpts,
    bdpts   := boundedpts
  #)

  mvars_between?(mv:MVars) : MACRO [Vars->bool] =
    boxbetween?(mv`numvars)(mv`vars_lb,mv`vars_ub,mv`iepts,mv`bdpts)

  mpoly_eval(mp:MPoly,nvars) : MACRO [Vars->real] =
    multipoly_eval(mp`mpoly,mp`mdeg,mp`mcoeff,nvars,mp`terms)

END MPoly