I have so far given a presentation of views that solely focuses on at-views and the views built on top of at-views. This is largely due to at-views being the form of most widely used views in practice and also being the first form of views supported in ATS. However, other forms of views can be readily introduced into ATS abstractly. Even in a case where a view can be defined based on at-views (or other forms of views), one may still want to introduce it as an abstract view (accompanied with certain proof functions for performing view-changes). Often what the programmer really needs is to figure out conceptually whether abstractly defined views and proof functions for manipulating them actually make sense. This is a bit like arguing whether a function is computable: There is rarely a need, if at all, to actually encode the function as a Turing-machine to prove its being computable. IMHO, learning proper use of abstract views and abstract viewtypes is a necessary step for one to take in order to employ linear types effectively in practice to deal with resource-related programming issues.
Objects in the physical world are conspicuously linear: They cannot be created from nothing or simply go vanished by turning into nothing. Thus, it is only natural to assign linear types to values that represent physical objects. I choose the name simple linear object here to refer to a linear value representing an object of some sort that does not contain built-in mechanism for supporting inheritance.
Let us now take a look at a concrete example of simple linear object. The following code presents an interface for a timer (that is, stopwatch):
// absvtype timer_vtype vtypedef timer = timer_vtype // fun timer_new (): timer fun timer_free (x: timer): void fun timer_start (x: !timer): void fun timer_finish (x: !timer): void fun timer_pause (x: !timer): void fun timer_resume (x: !timer): void fun timer_get_ntick (x: !timer): uint fun timer_reset (x: !timer): void //
// typedef timer_struct = @{ started= bool // the timer has started , running= bool // the timer is running // the tick number recorded when the timer , ntick_beg= uint // was turned on last time , ntick_acc= uint // the number of accumulated ticks } (* end of [timer_struct] *) //
Various functions on timers can now be readily implemented. Let us first see the code for creating and freeing timers:
implement timer_new () = let // val timer = TIMER (_) val TIMER (x) = timer // val () = x.started := false val () = x.running := false val () = x.ntick_beg := 0u val () = x.ntick_acc := 0u // prval () = fold@ (timer) // in timer end // end of [timer_new] implement timer_free (timer) = let val ~TIMER _ = timer in (*nothing*) end // end of [timer_free]
The function for starting a timer can be implemented as follows:
implement timer_start (timer) = let val+@TIMER(x) = timer val () = x.started := true val () = x.running := true val () = x.ntick_beg := the_current_tick_get () val () = x.ntick_acc := 0u prval () = fold@ (timer) in // nothing end // end of [timer_start]
A timer can be stopped or paused. The function for stopping a timer can be implemented as follows:
implement timer_finish (timer) = let val+@TIMER(x) = timer val () = x.started := false val () = if x.running then { val () = x.running := false val () = x.ntick_acc := x.ntick_acc + the_current_tick_get () - x.ntick_beg } (* end of [val] *) prval () = fold@ (timer) in // nothing end // end of [timer_finish]
A timer can be paused and then resumed. The following code implements the functions for pausing and resuming a timer:
implement timer_pause (timer) = let val+@TIMER(x) = timer val () = if x.running then { val () = x.running := false val () = x.ntick_acc := x.ntick_acc + the_current_tick_get () - x.ntick_beg } (* end of [val] *) prval () = fold@ (timer) in // nothing end // end of [timer_pause] implement timer_resume (timer) = let val+@TIMER(x) = timer val () = if x.started && ~(x.running) then { val () = x.running := true val () = x.ntick_beg := the_current_tick_get () } (* end of [if] *) // end of [val] prval () = fold@ (timer) in // nothing end // end of [timer_resume]
It is also possible to reset a timer by calling the function timer_reset:
implement timer_reset (timer) = let val+@TIMER(x) = timer val () = x.started := false val () = x.running := false val () = x.ntick_beg := 0u val () = x.ntick_acc := 0u prval () = fold@ (timer) in // nothing end // end of [timer_reset]
In order to read the time accumulated by a timer, the function timer_get_ntick can be called:
implement timer_get_ntick (timer) = let val+@TIMER(x) = timer var ntick: uint = x.ntick_acc val () = if x.running then ( ntick := ntick + the_current_tick_get () - x.ntick_beg ) (* end of [if] *) // end of [val] prval () = fold@ (timer) in ntick end // end of [timer_get_ntick]
A straightforward approach to implementing the_current_tick_get can be based directly on the function clock_gettime:
local staload "libc/SATS/time.sats" in (* in-of-local *) implement the_current_tick_get () = let var tv: timespec // uninitialized val err = clock_gettime (CLOCK_REALTIME, tv) val ((*void*)) = assertloc (err >= 0) prval ((*void*)) = opt_unsome{timespec}(tv) in $UNSAFE.cast2uint(tv.tv_sec) end // end of [the_current_tick_get] end // end of [local]
Please find on-line the entirety of the code presented in this section plus some testing code.