zetzit / zz

πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

new constructor from instance method #123

Open aep opened 3 years ago

aep commented 3 years ago

this doesn't work, but it should

struct A{};
struct B{};
fn to(A mut*self, B mut new*nu) {}
fn main() {
   A a;
   new b = a.to();
}

the reason it's currently broken is actually generated tail arguments make argument ordering a mess. I want to get rid of auto-generated tail arguments anyway in favor of generic call-site assigns.

aep commented 3 years ago

@jwerle

opinions on syntax for callsite assigns?

fn foh(int a, int b, char * other)
   where a > 2
   with b = 2 * a
{

}
fn foh(int a, int b, char * other)
   where a > 2
   where b = 2 * a
{

}
fn foh(int a, int b = 2 * a, char * other)
   where a > 2
{

}

all of these are used by skipping the callsite arg:

fn main() {
  foh(2, "boh");
}

and i feel like the last version makes that more obvious, although long expressions can look hard to read

fn foh(int a, int b = if constrained(typeof(vec::itema))) { vec::item(a) } else { u8 } , char * other)
   where a > 2
{

}
jwerle commented 3 years ago
fn foh(int a, int b, char * other)
   where a > 2
   with b = 2 * a
{

}

I like with

fn foh(int a, int b, char * other)
   where a > 2
   where b = 2 * a
{

}

but I also like where...

fn foh(int a, int b = 2 * a, char * other)
   where a > 2
{

}

This is very easy to understand

fn main() {
  foh(2, "boh");
}

but I can see a reader having to come back to understand how it is used. Is there a keyword we could introduce in the argument signature the denotes the variable as a callsite argument?

fn foh(int a, int b = if constrained(typeof(vec::itema))) { vec::item(a) } else { u8 } , char * other)
   where a > 2
{

}

oof! yeah that is hard to read ;)

aep commented 3 years ago

Is there a keyword we could introduce in the argument signature the denotes the variable as a callsite argument?

yeah. probably we want that plus the full expression in the smt section, since its an smt expression, so...

fn foh(int a, callsite int b, char * other)
   where a > 2
   where b = 2 * a
{

}

or something. not sure about the keyword. this is too long

jwerle commented 3 years ago

yeah something short and sweet

aep commented 3 years ago

actually skipping arguments in the middle is weird anyway. I'm going to require callsite arguments be at the end, which makes them very similar to default arguments in other languages, so we're also going with that familiar syntax

jwerle commented 3 years ago

yep that makes a lot more sense and we can avoid the extra keyword for the reader!