Conversation
spectec/src/il/eval.ml
Outdated
| {e1' with note = e.note} | ||
| | _ -> SubE (e1', t1', t2') $> e | ||
| ) | ||
| | AnnE (e1, _) -> reduce_exp env e1 |
There was a problem hiding this comment.
This is not enough, unfortunately. We now need to allow AnnE in all beta rules. Or reduce it away in places where it's redundant (e.g., around all intro forms that are already inferable, such as literals).
spectec/src/il/valid.ml
Outdated
| let as_list_typ phrase env dir t at : typ = | ||
| match expand_typ env t with | ||
| | IterT (t1, (List | List1 | ListN _)) -> t1 | ||
| | IterT (t1, (List | List1 | ListN _)) -> t1 (* QUEST(zilinc): Is it possible to be List1 or ListN in a type? *) |
There was a problem hiding this comment.
Not currently, this was just meant to be future-proof.
spectec/src/il/valid.ml
Outdated
| | _ -> error e.at "invalid case projection"; | ||
| ) | ||
| | OptE _ -> error e.at "cannot infer type of option" | ||
| | OptE (Some e1) -> let t1 = infer_exp env e1 in IterT (t1, Opt) $ e1.at |
There was a problem hiding this comment.
I have a tendency to leave this as is in favour of treating all OptE's uniformly.
spectec/src/il/valid.ml
Outdated
| else | ||
| error e.at "cannot infer type of concatenation" | ||
| | CaseE _ -> e.note (* error e.at "cannot infer type of case constructor" *) | ||
| | CaseE _ -> error e.at "cannot infer type of case constructor" |
There was a problem hiding this comment.
Yeah, you'll have to leave this alone until I have updated the elaborator.
spectec/src/il/valid.ml
Outdated
| equiv_typ env t2 t e.at; | ||
| sub_typ env t1 t2 e.at | ||
|
|
||
| | AnnE (e1, t1) -> valid_typ env t1; valid_exp ~side env e1 t1 |
There was a problem hiding this comment.
| | AnnE (e1, t1) -> valid_typ env t1; valid_exp ~side env e1 t1 | |
| | AnnE (e1, t1) → | |
| valid_exp ~side env e1 t1; | |
| valid_typ env t1 |
There was a problem hiding this comment.
Would you please elaborate the reason behind it?
There was a problem hiding this comment.
Just for visual uniformity with the other cases.
spectec/src/util/source.ml
Outdated
|
|
||
| let map_note f {it; at; note} = {it; at; note = f note} | ||
|
|
||
| let erase_note (x: ('a, 'b) note_phrase) = map_note (Fun.const ()) x |
There was a problem hiding this comment.
No, I'll remove. I initially wanted to erase all the notes in the AST, but later realised that the datatypes do not tie the knot, so it wouldn't work.
spectec/src/il/valid.mli
Outdated
| @@ -1 +1,2 @@ | |||
| val valid : Ast.script -> unit (* raises Error.Error *) | |||
| val elab : Ast.script -> Ast.script | |||
There was a problem hiding this comment.
FWIW, to extend validation with a note annotation mode, I'd rather make note a mutable field. Then it affects just a couple of lines of code instead of having to turn the entire validator into a mapping function.
There was a problem hiding this comment.
With a mutable note field, I would worry very much about the correctness of the code, as there's no type-level guarantee that I've changed all the note fields throughout the AST. There're only a couple of places that use the valid function in the codebase, so I hope it won't require too many changes.So unless you feel very strong about it, I prefer to keep it this way.
There was a problem hiding this comment.
I don't think it makes a difference for correctness. In either case, there is a single point where the note is updated. So it is equally easy/hard to screw that up.
OTOH, with mutation the code remains much simpler, plus it preserves its primary structure as a validator. So I think it's preferable overall, the impurity notwithstanding.
also address comments from Andreas
2 participants
No description provided.