I'm trying to create a version of string_is_prefix
that prove that a string is longer than the prefix if it returns true.
Here's the code I have so far:
#include "share/atspre_staload.hats"
dataprop StringLen(bool) =
| LessThan(false)
| {m,n:nat | m >= n} GreaterThanEqual(true)
fun string_is_prefix {m, n: nat} (string_prefix: string(m), string: string(n)): [b:bool] (StringLen(b) | bool(b)) =
let val prefix_len = string_length(string_prefix)
val string_len = string_length(string)
fun is_prefix {i: nat | m <= n; i < m} (index: size_t(i)): [b:bool] bool(b) =
let val equal = g1ofg0(string_get_at(string, index) = string_get_at(string_prefix, index))
in
if index + 1 >= prefix_len then
equal
else
equal * is_prefix(index + 1)
end
in
if prefix_len > string_len then
(LessThan() | false)
else if prefix_len > 0 then
let val result = is_prefix(i2sz(0))
in
if result then
(GreaterThanEqual{n, m}() | result)
else
(LessThan() | result)
end
else
(GreaterThanEqual{n, m}() | true)
end
fun func(string: stringGte(1)) =
()
implement main0(argc, argv) = {
val prefix_string: string(1) = "t"
val string: [n:nat] string(n) = g1ofg0(argv[0])
val (pf | is_prefix) = string_is_prefix(prefix_string, string)
val () =
if is_prefix then
let prval GreaterThanEqual{n, m}() = pf
in
func(string)
end
}
Unfortunately, the call to func(string)
does not compile as if this proof was not working:
unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=); S2EVar(5277->S2Evar(n$8654(14309))), S2Eintinf(1)))
How can I make this proof work?
The type you used is incorrect.
The type for what you want can be given as follows:
extern
fun
string_is_prefix
{m,n: nat}
( prfix: string(m)
, strng: string(n)): [b:bool | ~b || m <= n ] bool(b)