%%====================================================================
%%         Generic vector operations on real elements.
%%====================================================================


vectors [index_type: TYPE]: THEORY
BEGIN

vector:         TYPE = [index_type -> real]

i,j,k:          VAR index_type
a,b,c:          VAR real

U,V:            VAR vector

zero_vector:       vector = LAMBDA i: 0

vector_sum(U, V):  vector = LAMBDA i: U(i) + V(i)

vector_diff(U, V): vector = LAMBDA i: U(i) - V(i)

scalar_mult(a, V): vector = LAMBDA i: a * V(i)

END vectors


%%====================================================================
%%            The World According to Chronos  (Exercise 2)
%%====================================================================

chronos: THEORY
BEGIN

%% Insert new declarations in this theory.

% chr_axis: TYPE = <type expression>

% . . .

% precedes(x, y: point_in_time): bool =     %% x <= y
%     <expression>

% time_diff(y: point_in_time,               %% y - x in seconds
%           x: {t: point_in_time | precedes(t, y)}): real =
%     <expression>

% . . .

% final_position(x: point_in_time,
%                y: {t: point_in_time | precedes(x, t)},
%                position, velocity: chr_vector): chr_vector =
%     <expression>

% Gravity function g with monotonicity expressed in a predicate subtype:

% g: {f: gravity_fn | <constraint>}


% Split computation into two portions that lie on either side of
% midnight following the initial time x.

% final_speed(x: {T: point_in_time | T`day < Omega},
%            t: {d: real | 0 <= d & d < sec_per_day}): real =
%       LET delta_T_before =
%             <expression>,
%           delta_T_after =
%             <expression>
%       IN
%           <expression>

END chronos