Discussion about the Datalog model of GRIN#2
Discussion about the Datalog model of GRIN#2Anabra wants to merge 1 commit intosouffle-experimentfrom
Conversation
|
|
||
| // literal value | ||
| // example: result <- pure 1 | ||
| // QUESTION: why the type? |
There was a problem hiding this comment.
VariableSimpleType uses this.
|
|
||
| // bind pattern | ||
| // example: node@(Ctag param0 param1) <- pure input_value | ||
| // QUESTION: what about: node @ (Ctag param0) <- f x |
There was a problem hiding this comment.
Just initial design. Main motivation was to be simple.
| Call(node, f) | ||
| CallArgument(node, 0, x) | ||
| */ | ||
| /* QUESTION: is the third field of NodePattern redundant? |
There was a problem hiding this comment.
Keep AST simple, so that DL analysis is simple.
There was a problem hiding this comment.
Just use a transformation on the GRIN level.
| .decl Case(case_result:Variable, scrutinee:Variable) | ||
| .decl Alt(case_result:Variable, alt_value:Variable, t:Tag) | ||
| // NOTE: first could be just alt_value since it's unique | ||
| // QUESTION: why the tag here again? Maybe just store it here, and let case_result be alt_value |
There was a problem hiding this comment.
In general, we can add redundant fields to avoid additional JOINs in DL clauses. In this specific instance, the tag field can be omitted since that information is always available when using this AltParameter relation.
| // pure a.k.a. return value | ||
| // example: pure value | ||
| // QUESTION: shouldn't this be the return value of a function? | ||
| // QUESTION: can the return value of a function be only of form: pure <var_name> ? |
There was a problem hiding this comment.
Just use a transformation on the GRIN level.
| .decl EffectfulFunction(f:Function) | ||
| .output EffectfulFunction(delimiter=",") | ||
|
|
||
| // QUESTION: Why do we need f to have parameters? |
There was a problem hiding this comment.
This probably meant that f is function. Use a relation for that?
| , CodeNameInst(f,n) | ||
| , Effectful(n). | ||
|
|
||
| // QUESTION: CallArgument(n,_,_) means that it is not a nullary function? Why do we need this restriction? |
There was a problem hiding this comment.
This probably meant that n is the result of a function call.
There was a problem hiding this comment.
This is probably redundant?
|
|
||
| // QUESTION: CallArgument(n,_,_) means that it is not a nullary function? Why do we need this restriction? | ||
| Effectful(n) :- External(f,1), Call(n, f), CallArgument(n,_,_). | ||
| // QUESTION: Is Update really effectful? Didn't we settle on a conclusion that Updates can only be inside evals |
There was a problem hiding this comment.
This is faithful to the Boq PhD, but since then we changed the semantics of "effectful". In the original PhD everything that returned () was effectful, but now only externals that are marked effectful are effectful.
| seqAlg :: [G.ExpF (G.Exp, DL ()) -> DL ()] -> G.ExpF (G.Exp, DL ()) -> DL () | ||
| seqAlg algs exp = mapM_ ($ exp) algs | ||
|
|
||
| -- QUESTION: What is this? It doesn't interact with the AST and it has no side-effects. |
There was a problem hiding this comment.
This was just an experiment to define algebra compositions.
| -- call_result <- f value0 value1 | ||
| -- .decl Call(call_result:Variable, f:Function) | ||
| -- .decl CallArgument(call_result:Variable, i:number, value:Variable) | ||
| -- QUESTION: Why is this AST invalid? We can express this using the current model of the DL AST. |
There was a problem hiding this comment.
Yes, see the discussion above.
1 participant
This is just a placeholder PR where we discuss some questions about the Datalog model of GRIN.