Quellcode-Bibliothek fseqs_ops_vect3.pvs

fseqs_ops_vect3: THEORY
%------------------------------------------------------------------------
%
%  Defines some convenient operations over finite sequences of Vect3
%
%  EXPERIMENTAL
%
%------------------------------------------------------------------------
BEGIN


  IMPORTING vectors_3D, structures@fseqs_ops[Vect3]

  fs,gs: VAR fseq[Vect3]
  nefs: VAR ne_fseq[Vect3]
  i,n: VAR nat
  x: VAR real

% ------------ pointwise addition, subtraction of a sequence of vectors

  mmin(m,n:nat): MACRO nat = IF m > n THEN n ELSE m ENDIF ;

  +(fs,gs): fseq[Vect3] = LET len = mmin(l(fs),l(gs)) IN
                    (# length := len,
                      seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n) 
                                        ELSE default
                                        ENDIF)
                    #) ;


  -(fs,gs): fseq[Vect3] = LET len = mmin(l(fs),l(gs)) IN
                    (# length := len,
                      seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n) 
                                        ELSE default
                                        ENDIF)
                    #) ;


% ---------- scalar product of a sequence of reals with a sequence of vectors

  IMPORTING structures@fseqs_ops_real

  c: VAR fseq[real]

  *(c,gs): fseq[Vect3] = (# length := l(gs),
                      seq := (LAMBDA n: IF n < l(gs) THEN c(n) * gs(n) 
                                        ELSE default
                                        ENDIF)
                    #) ;

END fseqs_ops_vect3