CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
950 stars 84 forks source link

Support for multi-case functions defined by pattern matching #264

Open xrchz opened 7 years ago

xrchz commented 7 years ago

Function declarations currently only accept variables as arguments, but in SML one can do pattern matching with a declaration. CakeML AST does not support that, but the parser could generate the corresponding case expression on the tuple of argument variables. Or the AST could be augmented, if necessary, to do something more sophisticated.

mn200 commented 7 years ago

Functions, the fn form and val all allow patterns already. See for example the tests in compiler/parsing/tests/cmlTestsScript.sml around line 192. Not to mention the grammar itself.

xrchz commented 7 years ago

@tanyongkiam Can you clarify what you meant by function definitions with patterns not working?

tanyongkiam commented 7 years ago

Hmm, something like

fun f [] = [] | f (x::xs) = x;

doesn't parse for me

mn200 commented 7 years ago

Ah. That's true. The syntax only allows for patterns; it doesn't allow for multiple cases separated by bars (except in the case syntax of course). I think something like

fun f [] _ = 3
   | f (x::xs) 2 = 1 + x
   | f _ _ = 0

would have to parsed into

fun f gv1 gv2 = 
   case (gv1, gv2) of 
       ([], _) => 3
   |  (x::xs, 2) => 1 + x
   | (_, _) => 0

Would this then cause the (unnecessary) allocation of the tuple?

xrchz commented 7 years ago

Yes, it would allocate the tuple. To avoid this, I think the AST (and compiler) would need to support this syntax. @sowens do you have any thoughts?

xrchz commented 7 years ago

From video meeting: There are three strategies: full syntactic sugar (the parser does all the work), add an AST entry for it but desugar it early in the compiler, or carry it all the way to patLang and compile it away without allocating the tuple. @SOwens prefers the middle one.

(However, the whole thing is high cost low benefit… similar to records, which might have a better ratio. So maybe we better spend our time on records...)

mn200 commented 7 years ago

I'm happy to do the parser part of all three strategies (the changes will all be pretty similar).