Sketch of Operational Semantics for Expressions #7
Conversation
|
|
||
| -- Evaluating expressions results in values, which | ||
| -- may contain tensors and tensor operators | ||
| inductive Value (tensor op : Type) where |
There was a problem hiding this comment.
I can see why the tensor type is abstract, but why is op there? Don't we have a concrete list?
There was a problem hiding this comment.
op is the type of operator values. So, if I look up "matmul" in the environment, it will return something that I can give to apply. I don't need to know what the something is, so it is abstract.
| inductive Value (tensor op : Type) where | ||
| | const (c : Const) | ||
| | tensor (t : tensor) (ix : List (Value tensor op)) | ||
| | slice (l u step : Value tensor op) |
There was a problem hiding this comment.
Chatted offline. step could be an int here, but in NumPy is also allowed to be a singleton "scalar" array like np.array(1). Not sure which type is better here.
There was a problem hiding this comment.
I guess, in the current syntax, this might be written like so: u=np.array(1); t[1:2:u]. It is weird to have just u and not u[0]. Will need to consider how to handle this, well.
| | slice (l u step : Value tensor op) | ||
| | oper (f : op) | ||
| | tuple (l : List (Value tensor op)) | ||
| | list (l : List (Value tensor op)) |
There was a problem hiding this comment.
Do we need both tuples and lists?
There was a problem hiding this comment.
No, probably not, it is just a left-over from the python syntax.
| StepExpr env (.bvar a) v | ||
| | var : | ||
| Env.lookup env a = v -> | ||
| StepExpr env (.var a b) v |
There was a problem hiding this comment.
What happens to b here? Is b the initial value that is then just carried around and ignored?
There was a problem hiding this comment.
Also, left-over from the python syntax. Perhaps we should define a cleaner core language and translate the initial python syntax down to remove this kind of stuff?
| Env.lookup env a = v -> | ||
| StepExpr env (.var a b) v | ||
| | subscript : | ||
| StepExpr env e (.tensor t []) -> |
There was a problem hiding this comment.
Great eye. I was going to bring this up. I have never seen expressions like t[a,b,...][x,y,...] in NKI kernels, and I am not sure it is allowed. That is, you have to write the indexes all at once t[a,b,...,x,y,..], and you can't subscript into a partial tensor. Of course, allowing this kind of nested indexing is more general, and maybe we should?
| StepExpr env u u' -> | ||
| StepExpr env step step' -> | ||
| StepExpr env (.slice l u step) (.slice l' u' step') | ||
| | binop : |
There was a problem hiding this comment.
Why do we have both binop and call?
There was a problem hiding this comment.
Another left over from python syntax. We could translate the binop to call and the gridcall to forloop and call... and cond can be eliminated, as can var and check. More arguments for a "core language".
No description provided.