With only one exception, failure, Felix now produces
*.why files for every compilation that pass thru why
syntax checks. The exception is a stupid test case:
test/regress/rt-1.01.26-0
axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t):
sym(x,y) == sym(y,x)
;
which generates this:
axiom poly:
forall sym_47: (dunno, 'T46) fn.
forall eq_50: (dunno, bool) fn.
forall x_53: 'T46.
forall y_56: 'T46.
true=
(eq_50)(((sym_47)((x_53, y_56)), (sym_47)((y_56, x_53))))
File "test/regress/rt-1.01.26-0.why", line 48, characters 21-23:
Syntax error
If I clean up the syntax I get this:
sym_47(x_53, y_56) = sym_47(y_56, x_53)
Unbound variable sym_47
The first problem is that why doesn't support higher order functions.
To fix this I think is easy: the type I'm using in lieu is:
type ('a,'b) fn (* functions *)
so i just need a something like:
logic apply: ('a, 'b) fn, 'a -> 'b
The second problem is the 'dunno', which is an encoding
for an untranslatable data type, in this case a tuple (pair).
I guess I just have to introduce
type ('a, 'b) tup2
type ('a, 'b, 'c) tup3
...
I'm not sure how to handle Felix arrays. In Felix arrays
are tuples so
t ^ 2 = t * t
and the array form is canonical so
f: int * int -> int
is always represented by
f: int ^ 2 -> int
The next step, I plan to add:
lemma L(x:int): x + 1 = 1 + x;
which is the same form as an axiom, but is labelled as a lemma
to indicate it should be derivable from the axioms.
These will become Why goals, and it should be possible to
prove them by processing the *.why file with --simplify
and then passing the result to simplify.
Another thing to do is translate Felix pre- and post-conditions.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Take Surveys. Earn Cash. Influence the Future of IT
Join SourceForge.net's Techsay panel and you'll get the chance to share your
opinions on IT & business topics through brief surveys-and earn cash
http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
