diff options
| author | Alasdair | 2019-02-21 00:51:12 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-21 01:01:51 +0000 |
| commit | c0de36691f70867bbe1f9cd01f0ee4340b7fb2d5 (patch) | |
| tree | ff51b2557192028ecbd735c06fac95df1178ec00 /language | |
| parent | 7253269fb62712e7e8fd94d5d0264d5bed9e8406 (diff) | |
Fix specialization bug involving function annotations not matching valspecs
Perhaps suprisingly to some, this did not mean that Sail was
unable to typecheck the identify function.
While doing this rename Effect_opt_pure to Effect_opt_none - as
Effect_opt_pure was the effect equivalent of Typ_annot_opt_none,
and actually means that the function definition lacks an effect
annnotation, not that the function is actually pure, so this was
*extremely* misleading. The effect_opt that actually indicated a
function is pure was (and still is) the succinct:
Effect_opt_aux (Effect_opt_effect (Effect_aux (Effect_set [], _)), _)
In fact because in the grammar we only specify effects on
valspecs (they can always be inferred for fundefs in the absence
of a valspec) effect_opts are basically vestigial and are always
Effect_opt_none.
What might actually be super nice would be to remove rec_opt,
effect_opt and typ_annot_opt from fundefs in ast.ml altogether
and if we want them in the syntax just have them in parse_ast.ml
and pull them into a valspec during the initial check.
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/language/sail.ott b/language/sail.ott index 7dbd3c9e..a47f3f9f 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -773,7 +773,7 @@ rec_opt :: 'Rec_' ::= effect_opt :: 'Effect_opt_' ::= {{ com optional effect annotation for functions }} {{ aux _ l }} - | :: :: pure {{ com sugar for empty effect set }} + | :: :: none {{ com no effect annotation }} | effectkw effect :: :: effect % Generate a pexp, but from slightly different syntax (= rather than ->) |