With some hacking** I have got this to work!!
///////// FELIX INPUT ///////////////////////
type int = "int";
type INT = "int";
typeclass ADD[t] {
virtual fun add: t * t -> t;
virtual fun from_int: int -> t;
axiom sym(x:t, y:t): x + y = y + x;
axiom id(x:t): x + from_int 0 = x;
lemma idr(x:t): from_int 0 + x = x;
}
/// GENERATED WHY FILE (extract) /////////////
(****** ABSTRACT TYPES *******)
(* type int, at red.flx: line 1, cols 1 to 17 *)
(* type int -- USE why's builtin *)
(* type INT, at red.flx: line 2, cols 1 to 17 *)
type INT
(******* FUNCTIONS ******)
(* function add, at red.flx: line 5, cols 11 to 30 *)
logic add_10: 'T6, 'T6 -> 'T6
(* function from_int, at red.flx: line 8, cols 11 to 33 *)
logic from_int_19: int -> 'T6
(******* AXIOMS ******)
(* axiom id, at red.flx: line 11, cols 3 to 38 *)
axiom id:
forall x_40: 'T6.
add_10(x_40, from_int_19(0)) = x_40
(* axiom sym, at red.flx: line 10, cols 3 to 38 *)
axiom sym:
forall x_33: 'T6.
forall y_36: 'T6.
add_10(x_33, y_36) = add_10(y_36, x_33)
(* lemma idr, at red.flx: line 12, cols 3 to 38 *)
goal idr:
forall x_44: 'T6.
add_10(from_int_19(0), x_44) = x_44
/////// output from Simplify ////////////////////
[EMAIL PROTECTED]:/work/felix/svn/felix/felix/trunk$ simplify red_why.sx
Warning: triggerless quantifier body (will not warn of more for this
command)
(OR (EQ |$$1| |$$0|) (FORALL (v t) (EQ (access (update t |$$1| v) |$$0|)
(access t |$$0|))))
with 2 pattern variables, found while processing the formula
(FORALL (i j) (OR (EQ i j) (FORALL (v t) (EQ (access (update t i v) j)
(access t j)))))
Warning: triggerless quantifier body (will not warn of more for this
command)
(OR (> |$$3| |$$1|) (NOT (>= |$$2| |$$1|)) (> |$$3| |$$0|) (NOT (>= |
$$2| |$$0|)) (FORALL (t) (EQ |@true| (sub_permut |$$3| |$$2| t (update
(update t |$$1| (access t |$$0|)) |$$0| (access t |$$1|))))))
with 4 pattern variables, found while processing the formula
(FORALL (g d i j) (OR (> g i) (NOT (>= d i)) (> g j) (NOT (>= d j))
(FORALL (t) (EQ |@true| (sub_permut g d t (update (update t i (access t
j)) j (access t i)))))))
1: Valid.
/////////////////////////////////////////////
[Simplify doesn't report success in its return code ;(]
The hacks I had to do to make this work were to replace
an in program equality operator
logic eq: 't, 't -> bool
which generated axioms like
true = eq(L,R)
with actual equalities:
L = R
Still trying to figure out how to use this:
parameter decide_eq_8 : x:'T4 -> y:'T4 ->
{ } bool { if result then eq_8(x,y) else not eq_8(x,y) }
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
