!import "prelude" !Local
!import "intensional" !Local

-- Runtime-guarded wrappers around partial or structurally-sensitive base/list
-- functions. Each wrapper uses the frontend @ / =@ desugaring and is exported
-- with an advertised contract so manifests carry the contract terms.

safeHead xs@(nonEmptyListOf anyC) =@anyC head xs
safeTail xs@(nonEmptyListOf anyC) =@(listOf anyC) tail xs

safeDiv a@nat? b@(andC nat? nonZero?) =@nat? div a b

safeHalf n@(andC nat? evenC?) =@nat? div n 2

-- last is only guaranteed to return the maximum if the input list is sorted.
sortedMax xs@(sortedList? nat?) =@nat? last xs

!export safeHead : fnContract (nonEmptyListOf anyC) anyC
!export safeTail : fnContract (nonEmptyListOf anyC) (listOf anyC)
!export safeDiv : fn2 nat? nonZero? nat?
!export safeHalf : fnContract (andC nat? evenC?) nat?
!export sortedMax : fnContract (sortedList? nat?) nat?