From c0de36691f70867bbe1f9cd01f0ee4340b7fb2d5 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 21 Feb 2019 00:51:12 +0000
Subject: 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.
---
 src/parser.mly | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/parser.mly')

diff --git a/src/parser.mly b/src/parser.mly
index bd832d28..4004f53d 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -133,7 +133,7 @@ let mk_recn = (Rec_aux((Rec_nonrec), Unknown))
 let mk_typqn = (TypQ_aux(TypQ_no_forall,Unknown))
 let mk_tannotn = Typ_annot_opt_aux(Typ_annot_opt_none,Unknown)
 let mk_tannot typq typ n m = Typ_annot_opt_aux(Typ_annot_opt_some (typq, typ), loc n m)
-let mk_eannotn = Effect_opt_aux(Effect_opt_pure,Unknown)
+let mk_eannotn = Effect_opt_aux(Effect_opt_none,Unknown)
 
 let mk_typq kopts nc n m = TypQ_aux (TypQ_tq (List.map qi_id_of_kopt kopts @ nc), loc n m)
 
-- 
cgit v1.2.3