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 /src/parse_ast.ml | |
| 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 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index eb5c3dc6..2ff7b5e2 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -324,7 +324,7 @@ typschm_opt = type effect_opt_aux = (* Optional effect annotation for functions *) - Effect_opt_pure (* sugar for empty effect set *) + Effect_opt_none (* sugar for empty effect set *) | Effect_opt_effect of atyp |