As an exercise I'm trying to define a safe subtraction function for natural
numbers in a few different ways (subsorts, props, or boolean predicates)
but I am having trouble figuring out the boolean predicate case:
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
// safe subtract subsort
fun mysub { m,n:nat | n <= m } (x:int m, y:int n) : int = x - y
// safe subtract prop
dataprop safesub_p (int, int)
= { m,n:nat | n <= m } mk_safesub_p (m,n)
fun mysub_p { m,n:int }
(pf : safesub_p (m,n) | x:int m, y:int n) : int
= x - y
// safe subtract pred
stacst safesub_b : (int, int) -> bool
extern praxi lemma_safesub_b { m,n:nat | n <= m }
() : [safesub_b (m,n)] unit_p
fun mysub_b { m,n:nat | safesub_b(m,n) }
(x:int m, y:int n) : int
= let prval () = $solver_assert (lemma_safesub_b) in
x - y
end
implement main0 () = (
println!("mysub (5,4): ", mysub (5,4));
println!("mysub_p (mk_safesub_p | 5,4): ",
mysub_p (mk_safesub_p | 5,4));
//println!("mysub_b (5,4): ", mysub_b (5,4)); // error: unresolved
constraint
)
The above should compile but un-commenting the last function call gives an
unresolved constraint.
There are a couple examples in the documentation around ATS that include
examples of the boolean predicate style for fibonacci and factorial
functions, but so far I haven't succeeded in translating that style to this
function. fib and fact functions are defined inductively, and the predicate
relates the input and output integers, so you have some existential
quantification on the output, and no restriction on the input (defined for
all naturals). This case (safesub) seems to be the opposite: the predicate
relates only the inputs to each other. Really it looks almost the same as
the first subsort implementation, but if I try this:
stadef safesub_b = lte_int_int
fun mysub_b { m,n:nat | safesub_b(m,n) } (x:int m, y:int n) : int = x - y
the unresolved constraint remains.
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/c8542d63-dadf-43b8-b964-7038ed02ced7%40googlegroups.com.
