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/ac4f8646-b8e3-441c-8311-cb8da2d3a4ca%40googlegroups.com.
