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/initial_check.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/initial_check.ml')
| -rw-r--r-- | src/initial_check.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/initial_check.ml b/src/initial_check.ml index 003da64e..5893563b 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -595,7 +595,7 @@ let to_ast_typschm_opt ctx (P.TypSchm_opt_aux(aux,l)) : tannot_opt ctx_out = let to_ast_effects_opt (P.Effect_opt_aux(e,l)) : effect_opt = match e with - | P.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l) + | P.Effect_opt_none -> Effect_opt_aux(Effect_opt_none,l) | P.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects typ),l) let to_ast_funcl ctx (P.FCL_aux(fcl,l) : P.funcl) : (unit funcl) = |