Ah thank you for catching that, I have a habit of always writing my
inequalities with LT, forgot that the arguments were the other way around!
So having $solver_assertion (lemma_safesub_b) isn't going to work in this
case? Must reach for an external solver?
On Tuesday, April 18, 2017 at 4:58:35 AM UTC-7, gmhwxi wrote:
>
>
> >>stadef safesub_b = lte_int_int
>
> Should it be
>
> stadef safesub_b = gte_int_int
>
> ?
>
> For typechecking mysub_b, you need to use Z3 to solve the
> generated constraints.
>
> On Tuesday, April 18, 2017 at 7:44:33 AM UTC-4, spearman wrote:
>>
>> 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/ddf22c9f-4cb1-4374-96ea-a80d84b6d7d3%40googlegroups.com.
