Thank you, this works with Z3:
// 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 | n <= m }
(x:int m, y:int n) : [safesub_b (m,n)] int
= let prval () = $solver_assert (lemma_safesub_b) in
x - y
end
b.t.w., the SF repository at git://git.code.sf.net/p/ats2-lang/code is
missing a few ./contrib/ sub directories:
- 'atscntrb-smt-z3'
- 'atscntrb-sdstring'
- 'ats2cpp'
and in the GitHub repository https://github.com/githwxi/ATS-Postiats is
missing ./install-sh required by the ./configure script.
On Tuesday, April 18, 2017 at 8:27:51 AM UTC-7, gmhwxi wrote:
>
> Yes, $solver_assert is only supported when Z3 is used for solving
> constraints.
>
> On Tuesday, April 18, 2017 at 8:26:10 AM UTC-4, spearman wrote:
>>
>> 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/973398a0-d26b-4625-a59f-0517a11cf73c%40googlegroups.com.
