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.

8 files changed, 35 insertions, 25 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index 8942b3b1..158b40a8 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -116,7 +116,7 @@ let mk_qi_kopt kopt = QI_aux (QI_id kopt, Parse_ast.Unknown)
 
 let mk_fundef funcls =
   let tannot_opt = Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown) in
-  let effect_opt = Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown) in
+  let effect_opt = Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown) in
   let rec_opt = Rec_aux (Rec_nonrec, Parse_ast.Unknown) in
   DEF_fundef
    (FD_aux (FD_function (rec_opt, tannot_opt, effect_opt, funcls), no_annot))
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) =
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 856e36d5..92a0ae01 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -201,7 +201,7 @@ let rec is_value (E_aux (e,(l,annot))) =
 
 let is_pure (Effect_opt_aux (e,_)) =
   match e with
-  | Effect_opt_pure -> true
+  | Effect_opt_none -> true
   | Effect_opt_effect (Effect_aux (Effect_set [],_)) -> true
   | _ -> false
 
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
 
 
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)
 
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 3c000f17..c78c9aee 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -3106,7 +3106,7 @@ let construct_toplevel_string_append_func env f_id pat =
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
   let no_tannot = (Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown)) in
-  let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+  let effect_none = (Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown)) in
   let s_id = fresh_stringappend_id () in
   let arg_pat = mk_pat (P_id s_id) in
   (* We can ignore guards here because we've already removed them *)
@@ -3211,7 +3211,7 @@ let construct_toplevel_string_append_func env f_id pat =
   in
   let wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_lit_exp L_unit])))) in
   let new_match = mk_exp (E_case (mk_exp (E_id s_id), [strip_pexp new_pexp; wildcard])) in
-  let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl f_id arg_pat new_match]), (unk,())) in
+  let new_fun_def = FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl f_id arg_pat new_match]), (unk,())) in
   let new_fun_def, env = Type_check.check_fundef env new_fun_def in
   List.flatten [new_val_spec; new_fun_def]
 
@@ -4339,7 +4339,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
 
     let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
-    let effect_pure = (Effect_opt_aux (Effect_opt_pure, Parse_ast.Unknown)) in
+    let effect_none = (Effect_opt_aux (Effect_opt_none, Parse_ast.Unknown)) in
     (* We need to make sure we get the environment for the last mapping clause *)
     let env = match List.rev mapcls with
       | MCL_aux (_, mapcl_annot) :: _ -> env_of_annot mapcl_annot
@@ -4373,10 +4373,10 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
     let forwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl true forwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
     let backwards_matches_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_bool_mapcl false backwards_matches_id) mapcls) |> List.flatten) @ [wildcard])) in
 
-    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
-    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
-    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
-    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
+    let forwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl forwards_id arg_pat forwards_match]), (l, ()))) in
+    let backwards_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl backwards_id arg_pat backwards_match]), (l, ()))) in
+    let forwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl forwards_matches_id arg_pat forwards_matches_match]), (l, ()))) in
+    let backwards_matches_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl backwards_matches_id arg_pat backwards_matches_match]), (l, ()))) in
 
     typ_debug (lazy (Printf.sprintf "forwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_fun |> Pretty_print_sail.to_string)));
     typ_debug (lazy (Printf.sprintf "backwards for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_fun |> Pretty_print_sail.to_string)));
@@ -4395,7 +4395,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
               let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
-              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
+              let forwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat forwards_prefix_match]), (l, ()))) in
               typ_debug (lazy (Printf.sprintf "forwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef forwards_prefix_fun |> Pretty_print_sail.to_string)));
               let forwards_prefix_fun, _ = Type_check.check_fundef env forwards_prefix_fun in
               forwards_prefix_spec @ forwards_prefix_fun
@@ -4405,7 +4405,7 @@ let rewrite_defs_realise_mappings _ (Defs defs) =
                 let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
-                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_pure, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
+                let backwards_prefix_fun = (FD_aux (FD_function (non_rec, no_tannot, effect_none, [mk_funcl prefix_id arg_pat backwards_prefix_match]), (l, ()))) in
                 typ_debug (lazy (Printf.sprintf "backwards prefix matches for mapping %s: %s\n%!" (string_of_id id) (Pretty_print_sail.doc_fundef backwards_prefix_fun |> Pretty_print_sail.to_string)));
                 let backwards_prefix_fun, _ = Type_check.check_fundef env backwards_prefix_fun in
                 backwards_prefix_spec @ backwards_prefix_fun
@@ -4937,7 +4937,7 @@ let rewrite_explicit_measure env (Defs defs) =
         match Bindings.find id measures with
         | (measure_pat, measure_exp) ->
            let e = match e with
-             | Effect_opt_aux (Effect_opt_pure, _) ->
+             | Effect_opt_aux (Effect_opt_none, _) ->
                 Effect_opt_aux (Effect_opt_effect (mk_effect [BE_escape]), loc)
              | Effect_opt_aux (Effect_opt_effect eff,_) ->
                 Effect_opt_aux (Effect_opt_effect (add_escape eff), loc)
diff --git a/src/scattered.ml b/src/scattered.ml
index de286e3f..92cb3561 100644
--- a/src/scattered.ml
+++ b/src/scattered.ml
@@ -66,8 +66,8 @@ let rec last_scattered_mapcl id = function
   | [] -> true
 
 (* Nothing cares about these and the AST should be changed *)
-let fake_effect_opt l = Effect_opt_aux (Effect_opt_pure, gen_loc l)
-let fake_rec_opt l = Rec_aux (Rec_rec, gen_loc l)
+let no_effect_opt l = Effect_opt_aux (Effect_opt_none, gen_loc l)
+let fake_rec_opt l = Rec_aux (Rec_nonrec, gen_loc l)
 
 let no_tannot_opt l = Typ_annot_opt_aux (Typ_annot_opt_none, gen_loc l)
 
@@ -95,7 +95,7 @@ let rec descatter' funcls mapcls = function
        | Some clauses -> List.rev (funcl :: clauses)
        | None -> [funcl]
      in
-     DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, fake_effect_opt l, clauses),
+     DEF_fundef (FD_aux (FD_function (fake_rec_opt l, no_tannot_opt l, no_effect_opt l, clauses),
                          (gen_loc l, Type_check.empty_tannot)))
      :: descatter' funcls mapcls defs
 
diff --git a/src/specialize.ml b/src/specialize.ml
index eaef1231..646b92f7 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -351,8 +351,9 @@ let specialize_id_valspec spec instantiations id ast =
 
 (* When we specialize a function definition we also need to specialize
    all the types that appear as annotations within the function
-   body. *)
-let specialize_annotations instantiation =
+   body. Also remove any type-annotation from the fundef itself,
+   because at this point we have that as a separate valspec.*)
+let specialize_annotations instantiation fdef =
   let open Type_check in
   let rw_pat = {
       id_pat_alg with
@@ -364,11 +365,20 @@ let specialize_annotations instantiation =
       lEXP_cast = (fun (typ, lexp) -> LEXP_cast (subst_unifiers instantiation typ, lexp));
       pat_alg = rw_pat
     } in
-  rewrite_fun {
-      rewriters_base with
-      rewrite_exp = (fun _ -> fold_exp rw_exp);
-      rewrite_pat = (fun _ -> fold_pat rw_pat)
-    }
+  let fdef =
+    rewrite_fun {
+        rewriters_base with
+        rewrite_exp = (fun _ -> fold_exp rw_exp);
+        rewrite_pat = (fun _ -> fold_pat rw_pat)
+      } fdef
+  in
+  match fdef with
+  | FD_aux (FD_function (rec_opt, _, eff_opt, funcls), annot) ->
+     FD_aux (FD_function (rec_opt,
+                          Typ_annot_opt_aux (Typ_annot_opt_none, Parse_ast.Unknown),
+                          eff_opt,
+                          funcls),
+             annot)
 
 let specialize_id_fundef instantiations id ast =
   match split_defs (is_fundef id) ast with