Well, that Dypgen GLR parser is great!
Here's some code:
/////
// equality: technically, equivalence relation
class Eq[t] {
virtual fun eq: t * t -> bool;
virtual fun ne (x:t,y:t):bool => not (eq (x,y));
axiom reflex(x:t): eq(x,x);
axiom sym(x:t, y:t): eq(x,y) == eq(y,x);
axiom trans(x:t, y:t, z:t): implies(eq(x,y) and eq(y,z), eq(x,z));
}
/////
This defines == to be an equivalence relation. It uses this grammar:
/////
x[scomparison_pri]:= x[>scomparison_pri] "==" x[>scomparison_pri] =># "(infix
'eq)";
x[scomparison_pri]:= x[>scomparison_pri] "!=" x[>scomparison_pri] =># "(infix
'ne)";
/////
To parse operator == and != and map them to function names "eq" and "ne".
Now, this has always disturbed me, that someone has to remember the operator
symbol
and separately the function name. Especially now I have added several hundred
AMSTeX/La-TeX/TeX symbols from MathJax to Felix. The TeXish names like \subset
and \cup and \delta have been added as identifiers to the grammar. So you can
write
this:
///
x[scomparison_pri]:= x[>scomparison_pri] "==" x[>scomparison_pri] =># "(infix
'eq)";
...
fun eq: T * T -> bool = "$1==$2";
...
println$ a == b;
///
Well it took a while for it to dawn on me. It works. The \subset in the function
definition works, it isn't a syntax error. Why? because Dypgen's GLR parser
isn't "expecting" an infix operator after "fun", just an identifier, which
"\subset"
is now. Well then, what about:
///
println$ \subset (a,b)
///
Hang on! That works too!! For the same reason. The same name can be used
BOTH as a prefix operator and an infix operator (a well known property of
standard notation: every operator can be both prefix and infix, or postfix
and infix, without ambiguity). Another such operator is "-": prefix negation
and infix subtraction (quite different operators).
And so:
///
fun f(g:int*int->bool) => fun (a:int, b:int) => not (g (a,b));
println$ 2 \subset 3, f (\subset) (3,4);
////
This "just works". The parens () around the second \subset
have no semantic impact, but they change the parser behaviour.
So .. here am I, writing new orders:
/////
// partial order
class Pord[t]{
inherit Eq[t];
virtual fun \subset: t * t -> bool;
virtual fun \supset(x:t,y:t):bool =>y \subset x;
virtual fun \subseteq(x:t,y:t):bool => x \subset y or x == y;
virtual fun \supseteq(x:t,y:t):bool => x \supset y or x == y;
axiom trans(x:t, y:t, z:t): implies(\subset(x,y) and \subset(y,z),
\subset(x,z));
axiom antisym(x:t, y:t): \subset(x,y) or \subset(y,x) or eq(x,y);
axiom reflex(x:t, y:t): implies(\subseteq(x,y) and \subseteq(y,x), eq(x,y));
}
/////
and thinking I should define and use \implies instead of implies,
the latter is NOT in the grammar as an operator at the moment.
(and the former is, but it is considered an arrow, which has the wrong
precedence for implication).
... but then Eureka strikes! Another great simplification of Felix!
If I add < > <= etc as identifiers to the grammar ... I should be able to do
this:
////
fun == : T * T -> bool = "$1==$2";
fun < : T * T -> bool = "$1<$2";
fun \lt : T * T -> bool = "$1<$2";
///
etc. No more need to remember == maps to eq!
Actually the problem is reversed now: we have to specify somehow
that both < and \lt both map to the same function, perhaps:
///
fun <,\lt: T * T -> bool = $1<$2;
///
would do it (i.e., define multiple symbols at once): perhaps also:
///
val x,y,z = 1;
///
although we have to decide if we're dealing with aliases for the same
function, or several functions with the same definition: for the "val"
case it has to be the latter.
Food for thought! Documentation driven programming!
--
john skaller
skal...@users.sourceforge.net
------------------------------------------------------------------------------
Ridiculously easy VDI. With Citrix VDI-in-a-Box, you don't need a complex
infrastructure or vast IT resources to deliver seamless, secure access to
virtual desktops. With this all-in-one solution, easily deploy virtual
desktops for less than the cost of PCs and save 60% on VDI infrastructure
costs. Try it free! http://p.sf.net/sfu/Citrix-VDIinabox
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
