diff options
| -rw-r--r-- | language/sail.ott | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 2 | ||||
| -rw-r--r-- | src/initial_check.ml | 2 | ||||
| -rw-r--r-- | src/monomorphise.ml | 2 | ||||
| -rw-r--r-- | src/parse_ast.ml | 2 | ||||
| -rw-r--r-- | src/parser.mly | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 20 | ||||
| -rw-r--r-- | src/scattered.ml | 6 | ||||
| -rw-r--r-- | src/specialize.ml | 24 |
9 files changed, 36 insertions, 26 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 ->) 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 |