diff --git a/compiler/ast_schema.json b/compiler/ast_schema.json index af04af01..a2971d23 100644 --- a/compiler/ast_schema.json +++ b/compiler/ast_schema.json @@ -139,7 +139,7 @@ { "name": "names", "type": "NonEmptyList", "optional": false }, { "name": "is_aliased", "type": "Boolean", "optional": false }, { "name": "is_constant", "type": "Boolean", "optional": false }, - { "name": "object_type", "type": "NodeRef", "optional": false }, + { "name": "object_type", "type": "NodeRef", "optional": false }, { "name": "initializer", "type": "Option", "optional": true }, { "name": "span", "type": "Span", "optional": false } ] @@ -312,7 +312,7 @@ "production": "index_subtype_definition", "source_section": "8.4", "fields": [ - { "name": "subtype_mark", "type": "NodeRef", "optional": false }, + { "name": "subtype_mark", "type": "NodeRef", "optional": false }, { "name": "span", "type": "Span", "optional": false } ] }, @@ -332,7 +332,7 @@ "source_section": "8.4", "fields": [ { "name": "is_aliased", "type": "Boolean", "optional": false }, - { "name": "type_spec", "type": "NodeRef", "optional": false }, + { "name": "type_spec", "type": "NodeRef", "optional": false }, { "name": "span", "type": "Span", "optional": false } ] }, @@ -345,6 +345,16 @@ { "name": "span", "type": "Span", "optional": false } ] }, + { + "node_type": "MapTypeSpec", + "production": "map_type_spec", + "source_section": "8.4", + "fields": [ + { "name": "key_type", "type": "NodeRef", "optional": false }, + { "name": "value_type", "type": "NodeRef", "optional": false }, + { "name": "span", "type": "Span", "optional": false } + ] + }, { "node_type": "GrowableArrayTypeSpec", "production": "growable_array_type_spec", @@ -359,7 +369,7 @@ "production": "tuple_type_spec", "source_section": "8.4", "fields": [ - { "name": "elements", "type": "NonEmptyList", "optional": false }, + { "name": "elements", "type": "NonEmptyList", "optional": false }, { "name": "span", "type": "Span", "optional": false } ] }, @@ -368,7 +378,7 @@ "production": "optional_type_spec", "source_section": "8.4", "fields": [ - { "name": "element_type", "type": "NodeRef", "optional": false }, + { "name": "element_type", "type": "NodeRef", "optional": false }, { "name": "span", "type": "Span", "optional": false } ] }, @@ -1041,7 +1051,7 @@ "fields": [ { "name": "name", "type": "Identifier", "optional": false }, { "name": "is_aliased", "type": "Boolean", "optional": false }, - { "name": "return_type", "type": "NodeRef", "optional": false }, + { "name": "return_type", "type": "NodeRef", "optional": false }, { "name": "initializer", "type": "Option", "optional": true }, { "name": "body", "type": "NodeRef", "optional": false }, { "name": "span", "type": "Span", "optional": false } @@ -1218,7 +1228,7 @@ "fields": [ { "name": "name", "type": "Identifier", "optional": false }, { "name": "formal_part", "type": "Option", "optional": true }, - { "name": "return_type", "type": "NodeRef", "optional": false }, + { "name": "return_type", "type": "NodeRef", "optional": false }, { "name": "span", "type": "Span", "optional": false } ] }, @@ -1239,7 +1249,7 @@ { "name": "names", "type": "NonEmptyList", "optional": false }, { "name": "is_aliased", "type": "Boolean", "optional": false }, { "name": "mode", "type": "ParameterMode", "optional": false, "note": "Borrow (default) or Mut" }, - { "name": "param_type", "type": "NodeRef", "optional": false }, + { "name": "param_type", "type": "NodeRef", "optional": false }, { "name": "default_expression", "type": "Option", "optional": true }, { "name": "span", "type": "Span", "optional": false } ] diff --git a/compiler_impl/src/safe_frontend-ada_emit.adb b/compiler_impl/src/safe_frontend-ada_emit.adb index 73f18ba5..c3cde97e 100644 --- a/compiler_impl/src/safe_frontend-ada_emit.adb +++ b/compiler_impl/src/safe_frontend-ada_emit.adb @@ -3796,6 +3796,7 @@ package body Safe_Frontend.Ada_Emit is Match : GM.Type_Descriptor := (others => <>); procedure Check_Info (Info : GM.Type_Descriptor); + procedure Check_Expr (Expr : CM.Expr_Access); procedure Check_Decls (Decls : CM.Resolved_Object_Decl_Vectors.Vector); procedure Check_Decls (Decls : CM.Object_Decl_Vectors.Vector); procedure Check_Statements @@ -3808,16 +3809,65 @@ package body Safe_Frontend.Ada_Emit is end if; if FT.To_String (Info.Name) = Target_Name then + if Starts_With (Target_Name, "__tuple") + and then Info.Tuple_Element_Types.Is_Empty + then + return; + end if; Match := Info; Found := True; end if; end Check_Info; + procedure Check_Expr (Expr : CM.Expr_Access) is + begin + if Found or else Expr = null then + return; + end if; + + if Expr.Kind = CM.Expr_Tuple + and then Has_Text (Expr.Type_Name) + and then FT.To_String (Expr.Type_Name) = Target_Name + then + Match.Name := Expr.Type_Name; + Match.Kind := FT.To_UString ("tuple"); + for Element of Expr.Elements loop + if Element /= null and then Has_Text (Element.Type_Name) then + Match.Tuple_Element_Types.Append (Element.Type_Name); + end if; + end loop; + Found := True; + return; + end if; + + Check_Expr (Expr.Prefix); + Check_Expr (Expr.Callee); + Check_Expr (Expr.Inner); + Check_Expr (Expr.Left); + Check_Expr (Expr.Right); + Check_Expr (Expr.Value); + Check_Expr (Expr.Target); + for Item of Expr.Args loop + exit when Found; + Check_Expr (Item); + end loop; + for Item of Expr.Elements loop + exit when Found; + Check_Expr (Item); + end loop; + for Field of Expr.Fields loop + exit when Found; + Check_Expr (Field.Expr); + end loop; + end Check_Expr; + procedure Check_Decls (Decls : CM.Resolved_Object_Decl_Vectors.Vector) is begin for Decl of Decls loop Check_Info (Decl.Type_Info); exit when Found; + Check_Expr (Decl.Initializer); + exit when Found; end loop; end Check_Decls; @@ -3826,6 +3876,8 @@ package body Safe_Frontend.Ada_Emit is for Decl of Decls loop Check_Info (Decl.Type_Info); exit when Found; + Check_Expr (Decl.Initializer); + exit when Found; end loop; end Check_Decls; @@ -3841,23 +3893,33 @@ package body Safe_Frontend.Ada_Emit is case Item.Kind is when CM.Stmt_Object_Decl => Check_Info (Item.Decl.Type_Info); + Check_Expr (Item.Decl.Initializer); when CM.Stmt_Destructure_Decl => Check_Info (Item.Destructure.Type_Info); + Check_Expr (Item.Destructure.Initializer); when CM.Stmt_If => + Check_Expr (Item.Condition); Check_Statements (Item.Then_Stmts); for Part of Item.Elsifs loop exit when Found; + Check_Expr (Part.Condition); Check_Statements (Part.Statements); end loop; if Item.Has_Else then Check_Statements (Item.Else_Stmts); end if; when CM.Stmt_Case => + Check_Expr (Item.Case_Expr); for Arm of Item.Case_Arms loop exit when Found; + Check_Expr (Arm.Choice); Check_Statements (Arm.Statements); end loop; when CM.Stmt_While | CM.Stmt_Loop | CM.Stmt_For => + Check_Expr (Item.Condition); + Check_Expr (Item.Loop_Iterable); + Check_Expr (Item.Loop_Range.Low_Expr); + Check_Expr (Item.Loop_Range.High_Expr); Check_Decls (Item.Declarations); Check_Statements (Item.Body_Stmts); when CM.Stmt_Select => @@ -3866,15 +3928,24 @@ package body Safe_Frontend.Ada_Emit is case Arm.Kind is when CM.Select_Arm_Channel => Check_Info (Arm.Channel_Data.Type_Info); + Check_Expr (Arm.Channel_Data.Channel_Name); Check_Statements (Arm.Channel_Data.Statements); when CM.Select_Arm_Delay => + Check_Expr (Arm.Delay_Data.Duration_Expr); Check_Statements (Arm.Delay_Data.Statements); when others => null; end case; end loop; when others => - null; + Check_Expr (Item.Target); + Check_Expr (Item.Value); + Check_Expr (Item.Call); + Check_Expr (Item.Condition); + Check_Expr (Item.Case_Expr); + Check_Expr (Item.Match_Expr); + Check_Expr (Item.Channel_Name); + Check_Expr (Item.Success_Var); end case; end if; end loop; @@ -6154,6 +6225,10 @@ package body Safe_Frontend.Ada_Emit is return "Safe_String_RT.Empty"; elsif Type_Name = "float" or else Type_Name = "long_float" then return "0.0"; + elsif Starts_With (Type_Name, "__growable_array_") + or else Starts_With (Type_Name, "Safe_growable_array_") + then + return Ada_Safe_Name (Type_Name) & "_RT.Empty"; elsif Starts_With (Type_Name, "access ") or else Starts_With (Type_Name, "not null access ") or else Starts_With (Type_Name, "access constant ") @@ -6629,13 +6704,7 @@ package body Safe_Frontend.Ada_Emit is elsif FT.Lowercase (Name) = "result" then Add_From_Info (BT.Result_Type); elsif Starts_With (Name, "__tuple") then - declare - Info : GM.Type_Descriptor; - begin - Info.Name := FT.To_UString (Name); - Info.Kind := FT.To_UString ("tuple"); - Add_Unique (Info); - end; + Add_From_Info (Resolve_Type_Name (Unit, Document, Name)); end if; end Add_From_Name; @@ -6747,6 +6816,21 @@ package body Safe_Frontend.Ada_Emit is end loop; end Add_From_Statements; begin + for Item of Unit.Types loop + if Has_Text (Item.Name) + and then not Contains_Name (Seen, FT.To_String (Item.Name)) + then + Seen.Append (Item.Name); + end if; + end loop; + for Item of Unit.Imported_Types loop + if Has_Text (Item.Name) + and then not Contains_Name (Seen, FT.To_String (Item.Name)) + then + Seen.Append (Item.Name); + end if; + end loop; + for Item of Unit.Types loop Add_From_Info (Item); end loop; @@ -18539,6 +18623,7 @@ package body Safe_Frontend.Ada_Emit is Synthetic_Types : GM.Type_Descriptor_Vectors.Vector; Owner_Access_Helper_Types : GM.Type_Descriptor_Vectors.Vector; Deferred_Package_Init_Names : FT.UString_Vectors.Vector; + Emit_Result_Builtin_First : Boolean := False; procedure Add_Body_With (Name : String) is begin @@ -18597,6 +18682,18 @@ package body Safe_Frontend.Ada_Emit is return False; end Decl_Uses_Package_Subprogram_Name; + function Unit_Defines_Result_Type return Boolean is + begin + for Type_Item of Unit.Types loop + if Is_Result_Builtin (Type_Item) + or else FT.Lowercase (FT.To_String (Type_Item.Name)) = "result" + then + return True; + end if; + end loop; + return False; + end Unit_Defines_Result_Type; + function Should_Defer_Package_Object_Initializer (Decl : CM.Resolved_Object_Decl; Names : FT.UString_Vectors.Vector) return Boolean @@ -18938,6 +19035,20 @@ package body Safe_Frontend.Ada_Emit is Append_Line (Spec_Inner, "pragma Elaborate_Body;", 1); Append_Line (Spec_Inner); Append_Bounded_String_Instantiations (Spec_Inner, State); + Collect_Synthetic_Types (Unit, Document, Synthetic_Types); + Collect_Owner_Access_Helper_Types (Unit, Document, Owner_Access_Helper_Types); + + Emit_Result_Builtin_First := + not Unit_Defines_Result_Type + and then (for some Type_Item of Synthetic_Types => Is_Result_Builtin (Type_Item)); + + if Emit_Result_Builtin_First then + Append_Line + (Spec_Inner, + Render_Type_Decl (Unit, Document, BT.Result_Type, State), + 1); + Append_Line (Spec_Inner); + end if; for Type_Item of Unit.Types loop Append_Line (Spec_Inner, Render_Type_Decl (Unit, Document, Type_Item, State), 1); @@ -18946,11 +19057,11 @@ package body Safe_Frontend.Ada_Emit is end if; end loop; - Collect_Synthetic_Types (Unit, Document, Synthetic_Types); - Collect_Owner_Access_Helper_Types (Unit, Document, Owner_Access_Helper_Types); for Type_Item of Synthetic_Types loop - Append_Line (Spec_Inner, Render_Type_Decl (Unit, Document, Type_Item, State), 1); - Append_Line (Spec_Inner); + if not (Emit_Result_Builtin_First and then Is_Result_Builtin (Type_Item)) then + Append_Line (Spec_Inner, Render_Type_Decl (Unit, Document, Type_Item, State), 1); + Append_Line (Spec_Inner); + end if; end loop; for Type_Item of Owner_Access_Helper_Types loop diff --git a/compiler_impl/src/safe_frontend-check_emit.adb b/compiler_impl/src/safe_frontend-check_emit.adb index c0fd12a8..37c20a3c 100644 --- a/compiler_impl/src/safe_frontend-check_emit.adb +++ b/compiler_impl/src/safe_frontend-check_emit.adb @@ -400,6 +400,15 @@ package body Safe_Frontend.Check_Emit is & ",""span"":" & JS.Span_Object (Spec.Span) & "}"; + elsif Spec.Kind = CM.Type_Spec_Map then + return + "{""node_type"":""MapTypeSpec"",""key_type"":" + & Object_Type_Node (Spec.Key_Type.all) + & ",""value_type"":" + & Object_Type_Node (Spec.Value_Type.all) + & ",""span"":" + & JS.Span_Object (Spec.Span) + & "}"; elsif Spec.Kind = CM.Type_Spec_Growable_Array then return "{""node_type"":""GrowableArrayTypeSpec"",""element_type"":" @@ -544,6 +553,8 @@ package body Safe_Frontend.Check_Emit is return Access_Definition_Node (Spec); elsif Spec.Kind = CM.Type_Spec_List then return Type_Spec_Name (Spec); + elsif Spec.Kind = CM.Type_Spec_Map then + return Type_Spec_Name (Spec); elsif Spec.Kind = CM.Type_Spec_Growable_Array then return Type_Spec_Name (Spec); elsif Spec.Kind = CM.Type_Spec_Tuple then diff --git a/compiler_impl/src/safe_frontend-check_model.ads b/compiler_impl/src/safe_frontend-check_model.ads index 8b31869c..2b27d2d5 100644 --- a/compiler_impl/src/safe_frontend-check_model.ads +++ b/compiler_impl/src/safe_frontend-check_model.ads @@ -95,6 +95,7 @@ package Safe_Frontend.Check_Model is Type_Spec_Binary, Type_Spec_Tuple, Type_Spec_List, + Type_Spec_Map, Type_Spec_Growable_Array, Type_Spec_Optional, Type_Spec_Subtype_Indication, @@ -122,6 +123,8 @@ package Safe_Frontend.Check_Model is Target_Name : Expr_Access := null; Binary_Width_Expr : Expr_Access := null; Element_Type : Type_Spec_Access := null; + Key_Type : Type_Spec_Access := null; + Value_Type : Type_Spec_Access := null; Tuple_Elements : Type_Spec_Access_Vectors.Vector; Has_Range_Constraint : Boolean := False; Range_Low : Expr_Access := null; diff --git a/compiler_impl/src/safe_frontend-check_parse.adb b/compiler_impl/src/safe_frontend-check_parse.adb index dc964b75..0f65b52b 100644 --- a/compiler_impl/src/safe_frontend-check_parse.adb +++ b/compiler_impl/src/safe_frontend-check_parse.adb @@ -660,6 +660,30 @@ package body Safe_Frontend.Check_Parse is return Result; end Parse_List_Type_Spec; + function Parse_Map_Type_Spec + (State : in out Parser_State) return CM.Type_Spec + is + Start : constant FL.Token := Expect (State, "map"); + Result : CM.Type_Spec; + Opener : FL.Token; + Ender : FL.Token; + pragma Unreferenced (Opener); + begin + Require (State, "of"); + Opener := Expect (State, "("); + Result.Kind := CM.Type_Spec_Map; + Result.Key_Type := + new CM.Type_Spec' + (Parse_Type_Spec_Internal (State, Allow_Access_Def => True)); + Require (State, ","); + Result.Value_Type := + new CM.Type_Spec' + (Parse_Type_Spec_Internal (State, Allow_Access_Def => True)); + Ender := Expect (State, ")"); + Result.Span := CM.Join (Start.Span, Ender.Span); + return Result; + end Parse_Map_Type_Spec; + function Sanitize_Type_Name_Component (Value : String) return String is Result : FT.UString := FT.To_UString (""); begin @@ -716,6 +740,18 @@ package body Safe_Frontend.Check_Parse is ("__optional_" & Sanitize_Type_Name_Component (FT.To_String (Type_Spec_Internal_Name (Spec.Element_Type.all)))); + when CM.Type_Spec_Map => + if Spec.Key_Type = null or else Spec.Value_Type = null then + return FT.To_UString ("__growable_array___tuple_key_value"); + end if; + return + FT.To_UString + ("__growable_array___tuple_" + & Sanitize_Type_Name_Component + (FT.To_String (Type_Spec_Internal_Name (Spec.Key_Type.all))) + & "_" + & Sanitize_Type_Name_Component + (FT.To_String (Type_Spec_Internal_Name (Spec.Value_Type.all)))); when CM.Type_Spec_Tuple => Result := FT.To_UString ("__tuple"); for Item of Spec.Tuple_Elements loop @@ -927,6 +963,8 @@ package body Safe_Frontend.Check_Parse is return Parse_Optional_Type_Spec (State, Allow_Access_Def); elsif Current_Lower (State) = "list" then return Parse_List_Type_Spec (State); + elsif Current_Lower (State) = "map" then + return Parse_Map_Type_Spec (State); elsif Current_Lower (State) = "array" and then FT.To_String (Next (State).Lexeme) /= "(" then @@ -996,6 +1034,10 @@ package body Safe_Frontend.Check_Parse is Result := Parse_List_Type_Spec (State); Result.Span := CM.Join (Start, Result.Span); return Result; + elsif Current_Lower (State) = "map" then + Result := Parse_Map_Type_Spec (State); + Result.Span := CM.Join (Start, Result.Span); + return Result; elsif Current_Lower (State) = "optional" then Result := Parse_Optional_Type_Spec (State, Allow_Access_Def => False); Result.Span := CM.Join (Start, Result.Span); @@ -2982,6 +3024,7 @@ package body Safe_Frontend.Check_Parse is begin if Current_Lower (State) = "binary" or else Current_Lower (State) = "optional" + or else Current_Lower (State) = "map" or else (Current_Lower (State) = "array" and then FT.To_String (Next (State).Lexeme) /= "(") or else FT.To_String (Current (State).Lexeme) = "(" diff --git a/compiler_impl/src/safe_frontend-check_resolve.adb b/compiler_impl/src/safe_frontend-check_resolve.adb index 009e1c3d..f8776186 100644 --- a/compiler_impl/src/safe_frontend-check_resolve.adb +++ b/compiler_impl/src/safe_frontend-check_resolve.adb @@ -610,6 +610,16 @@ package body Safe_Frontend.Check_Resolve is (Info : GM.Type_Descriptor; Type_Env : Type_Maps.Map) return GM.Type_Descriptor; + function Try_Map_Key_Value_Types + (Info : GM.Type_Descriptor; + Type_Env : Type_Maps.Map; + Key_Type : out GM.Type_Descriptor; + Value_Type : out GM.Type_Descriptor) return Boolean; + + function Is_Map_Key_Type_Allowed + (Info : GM.Type_Descriptor; + Type_Env : Type_Maps.Map) return Boolean; + function Bool_Expr (Value : Boolean; Span : FT.Source_Span) return CM.Expr_Access; @@ -672,6 +682,30 @@ package body Safe_Frontend.Check_Resolve is Functions : Function_Maps.Map; Type_Env : Type_Maps.Map) return Boolean; + function Is_Contains_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean; + + function Is_Get_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean; + + function Is_Set_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean; + + function Is_Remove_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean; + function Sanitize_Type_Name_Component (Value : String) return String; function Hidden_Reference_Target_Name (Name : String) return String; @@ -1310,6 +1344,51 @@ package body Safe_Frontend.Check_Resolve is return Default_Integer; end Growable_Array_Element_Type; + function Try_Map_Key_Value_Types + (Info : GM.Type_Descriptor; + Type_Env : Type_Maps.Map; + Key_Type : out GM.Type_Descriptor; + Value_Type : out GM.Type_Descriptor) return Boolean + is + Entry_Type : GM.Type_Descriptor := Default_Integer; + begin + Key_Type := Default_Integer; + Value_Type := Default_Integer; + + if not Is_Growable_Array_Type (Info, Type_Env) then + return False; + end if; + + Entry_Type := Base_Type (Growable_Array_Element_Type (Info, Type_Env), Type_Env); + if FT.Lowercase (UString_Value (Entry_Type.Kind)) /= "tuple" + or else Natural (Entry_Type.Tuple_Element_Types.Length) /= 2 + then + return False; + end if; + + Key_Type := + Resolve_Type + (UString_Value (Entry_Type.Tuple_Element_Types (Entry_Type.Tuple_Element_Types.First_Index)), + Type_Env, + "", + FT.Null_Span); + Value_Type := + Resolve_Type + (UString_Value (Entry_Type.Tuple_Element_Types (Entry_Type.Tuple_Element_Types.First_Index + 1)), + Type_Env, + "", + FT.Null_Span); + return True; + end Try_Map_Key_Value_Types; + + function Is_Map_Key_Type_Allowed + (Info : GM.Type_Descriptor; + Type_Env : Type_Maps.Map) return Boolean is + begin + return Is_Discrete_Case_Type (Info, Type_Env) + or else Is_String_Type (Info, Type_Env); + end Is_Map_Key_Type_Allowed; + function Bool_Expr (Value : Boolean; Span : FT.Source_Span) return CM.Expr_Access is @@ -2617,6 +2696,55 @@ package body Safe_Frontend.Check_Resolve is end if; return Make_Growable_Array_Type (Element_Type); end; + when CM.Type_Spec_Map => + if Spec.Key_Type = null or else Spec.Value_Type = null then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Spec.Span, + Message => "map type is missing a key or value type")); + end if; + declare + Key_Type : constant GM.Type_Descriptor := + Resolve_Type_Spec + (Spec.Key_Type.all, + Type_Env, + Const_Env, + Path, + Current_Record_Name, + Family_By_Name, + Families); + Value_Type : constant GM.Type_Descriptor := + Resolve_Type_Spec + (Spec.Value_Type.all, + Type_Env, + Const_Env, + Path, + Current_Record_Name, + Family_By_Name, + Families); + begin + if not Is_Map_Key_Type_Allowed (Key_Type, Type_Env) then + Raise_Diag + (CM.Unsupported_Source_Construct + (Path => Path, + Span => Spec.Key_Type.Span, + Message => + "`map of (K, V)` keys are limited to the admitted discrete/string subset in PR11.10c")); + elsif not Is_Container_Element_Type_Allowed (Value_Type, Type_Env) then + Raise_Diag + (CM.Unsupported_Source_Construct + (Path => Path, + Span => Spec.Value_Type.Span, + Message => + "`map of (K, V)` values are limited to the admitted value-type subset in PR11.10c")); + end if; + + Element_Types.Clear; + Element_Types.Append (Key_Type.Name); + Element_Types.Append (Value_Type.Name); + return Make_Growable_Array_Type (Make_Tuple_Type (Element_Types)); + end; when CM.Type_Spec_Optional => if Spec.Element_Type = null then Raise_Diag @@ -2951,6 +3079,44 @@ package body Safe_Frontend.Check_Resolve is Type_Env); end if; end; + elsif Is_Contains_Builtin_Call (Expr, Var_Types, Functions, Type_Env) + and then Natural (Expr.Args.Length) = 2 + then + return BT.Boolean_Type; + elsif Is_Get_Builtin_Call (Expr, Var_Types, Functions, Type_Env) + and then Natural (Expr.Args.Length) = 2 + then + declare + Map_Type : constant GM.Type_Descriptor := + Expr_Type + (Expr.Args (Expr.Args.First_Index), + Var_Types, + Functions, + Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + begin + if Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + return Make_Optional_Type (Value_Type, Type_Env); + end if; + end; + elsif Is_Remove_Builtin_Call (Expr, Var_Types, Functions, Type_Env) + and then Natural (Expr.Args.Length) = 2 + then + declare + Map_Type : constant GM.Type_Descriptor := + Expr_Type + (Expr.Args (Expr.Args.First_Index), + Var_Types, + Functions, + Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + begin + if Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + return Make_Optional_Type (Value_Type, Type_Env); + end if; + end; elsif UString_Value (Name) = "long_float.copy_sign" then return Resolve_Type ("long_float", Type_Env, "", FT.Null_Span); elsif Has_Type (Var_Types, UString_Value (Name)) then @@ -3457,6 +3623,99 @@ package body Safe_Frontend.Check_Resolve is Make_Optional_Type (Element_Type, Type_Env).Name; end; end if; + elsif Is_Contains_Builtin_Call (Result, Var_Types, Functions, Type_Env) + or else Is_Get_Builtin_Call (Result, Var_Types, Functions, Type_Env) + or else Is_Remove_Builtin_Call (Result, Var_Types, Functions, Type_Env) + then + declare + Builtin_Name : constant String := + (if Is_Contains_Builtin_Call (Result, Var_Types, Functions, Type_Env) + then "contains" + elsif Is_Get_Builtin_Call (Result, Var_Types, Functions, Type_Env) + then "get" + else "remove"); + begin + if Natural (Result.Args.Length) /= 2 then + Raise_Diag + (CM.Source_Frontend_Error + (Path => "", + Span => (if Result.Has_Call_Span then Result.Call_Span else Result.Span), + Message => "`" & Builtin_Name & "(m, key)` expects exactly two arguments")); + end if; + + declare + Map_Expr : constant CM.Expr_Access := + Result.Args (Result.Args.First_Index); + Key_Expr : CM.Expr_Access := + Result.Args (Result.Args.First_Index + 1); + Map_Type : constant GM.Type_Descriptor := + Expr_Type (Map_Expr, Var_Types, Functions, Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + begin + if Builtin_Name = "remove" + and then not Is_Assignable_Target (Map_Expr) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => "", + Span => Map_Expr.Span, + Message => "`remove` first argument must be a writable map name")); + elsif not Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + Raise_Diag + (CM.Source_Frontend_Error + (Path => "", + Span => Map_Expr.Span, + Message => "`" & Builtin_Name & "` expects a `map of (K, V)` first argument")); + elsif not Is_Map_Key_Type_Allowed (Key_Type, Type_Env) then + Raise_Diag + (CM.Unsupported_Source_Construct + (Path => "", + Span => Map_Expr.Span, + Message => + "`map of (K, V)` keys are limited to the admitted discrete/string subset in PR11.10c")); + elsif not Is_Container_Element_Type_Allowed (Value_Type, Type_Env) then + Raise_Diag + (CM.Unsupported_Source_Construct + (Path => "", + Span => Map_Expr.Span, + Message => + "`map of (K, V)` values are limited to the admitted value-type subset in PR11.10c")); + else + Key_Expr := + Contextualize_Expr_To_Target_Type + (Key_Expr, + Key_Type, + Var_Types, + Functions, + Type_Env, + ""); + Reject_Uncontextualized_None (Key_Expr, ""); + if not Compatible_Source_Expr_To_Target_Type + (Key_Expr, + Expr_Type (Key_Expr, Var_Types, Functions, Type_Env), + Key_Type, + Var_Types, + Functions, + Type_Env, + Const_Env, + Exact_Length_Maps.Empty_Map) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => "", + Span => Key_Expr.Span, + Message => "`" & Builtin_Name & "` key type does not match the map key type")); + end if; + Result.Args.Replace_Element (Result.Args.First_Index + 1, Key_Expr); + if Builtin_Name = "contains" then + Result.Type_Name := FT.To_UString ("boolean"); + else + Result.Type_Name := Make_Optional_Type (Value_Type, Type_Env).Name; + end if; + end if; + end; + end; end if; else Result := new CM.Expr_Node'(Resolved.all); @@ -3754,6 +4013,46 @@ package body Safe_Frontend.Check_Resolve is Is_Unshadowed_Builtin_Call (Expr, Var_Types, Functions, Type_Env, "pop_last"); end Is_Pop_Last_Builtin_Call; + function Is_Contains_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean is + begin + return + Is_Unshadowed_Builtin_Call (Expr, Var_Types, Functions, Type_Env, "contains"); + end Is_Contains_Builtin_Call; + + function Is_Get_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean is + begin + return + Is_Unshadowed_Builtin_Call (Expr, Var_Types, Functions, Type_Env, "get"); + end Is_Get_Builtin_Call; + + function Is_Set_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean is + begin + return + Is_Unshadowed_Builtin_Call (Expr, Var_Types, Functions, Type_Env, "set"); + end Is_Set_Builtin_Call; + + function Is_Remove_Builtin_Call + (Expr : CM.Expr_Access; + Var_Types : Type_Maps.Map; + Functions : Function_Maps.Map; + Type_Env : Type_Maps.Map) return Boolean is + begin + return + Is_Unshadowed_Builtin_Call (Expr, Var_Types, Functions, Type_Env, "remove"); + end Is_Remove_Builtin_Call; + procedure Validate_Pr112_Expr_Boundaries (Expr : CM.Expr_Access; Var_Types : Type_Maps.Map; @@ -5347,6 +5646,12 @@ package body Safe_Frontend.Check_Resolve is return Result; elsif Is_Optional_Type (Info, Type_Env) then return Build_Optional_None_Expr (Info, Span); + elsif Kind = "array" and then Info.Growable then + Result := new CM.Expr_Node; + Result.Kind := CM.Expr_Array_Literal; + Result.Type_Name := Info.Name; + Result.Span := Span; + return Result; elsif Kind = "record" then Result := new CM.Expr_Node; Result.Kind := CM.Expr_Aggregate; @@ -5448,6 +5753,90 @@ package body Safe_Frontend.Check_Resolve is return Result; end Synthetic_If_Stmt; + function Synthetic_If_Else_Stmt + (Condition : CM.Expr_Access; + Then_Stmts : CM.Statement_Access_Vectors.Vector; + Else_Stmts : CM.Statement_Access_Vectors.Vector; + Span : FT.Source_Span) return CM.Statement_Access + is + Result : constant CM.Statement_Access := new CM.Statement; + begin + Result.Kind := CM.Stmt_If; + Result.Is_Synthetic := True; + Result.Span := Span; + Result.Condition := Condition; + Result.Then_Stmts := Then_Stmts; + Result.Has_Else := True; + Result.Else_Stmts := Else_Stmts; + return Result; + end Synthetic_If_Else_Stmt; + + function Synthetic_While_Stmt + (Condition : CM.Expr_Access; + Body_Stmts : CM.Statement_Access_Vectors.Vector; + Span : FT.Source_Span) return CM.Statement_Access + is + Result : constant CM.Statement_Access := new CM.Statement; + begin + Result.Kind := CM.Stmt_While; + Result.Is_Synthetic := True; + Result.Span := Span; + Result.Condition := Condition; + Result.Body_Stmts := Body_Stmts; + return Result; + end Synthetic_While_Stmt; + + function Synthetic_For_Stmt + (Loop_Var : String; + Low_Expr : CM.Expr_Access; + High_Expr : CM.Expr_Access; + Body_Stmts : CM.Statement_Access_Vectors.Vector; + Span : FT.Source_Span) return CM.Statement_Access + is + Result : constant CM.Statement_Access := new CM.Statement; + begin + Result.Kind := CM.Stmt_For; + Result.Is_Synthetic := True; + Result.Span := Span; + Result.Loop_Var := FT.To_UString (Loop_Var); + Result.Loop_Range.Kind := CM.Range_Explicit; + Result.Loop_Range.Span := Span; + Result.Loop_Range.Low_Expr := Low_Expr; + Result.Loop_Range.High_Expr := High_Expr; + Result.Body_Stmts := Body_Stmts; + return Result; + end Synthetic_For_Stmt; + + function Synthetic_For_Of_Stmt + (Loop_Var : String; + Loop_Iterable : CM.Expr_Access; + Body_Stmts : CM.Statement_Access_Vectors.Vector; + Span : FT.Source_Span) return CM.Statement_Access + is + Result : constant CM.Statement_Access := new CM.Statement; + begin + Result.Kind := CM.Stmt_For; + Result.Is_Synthetic := True; + Result.Span := Span; + Result.Loop_Var := FT.To_UString (Loop_Var); + Result.Loop_Iterable := Loop_Iterable; + Result.Body_Stmts := Body_Stmts; + return Result; + end Synthetic_For_Of_Stmt; + + function Synthetic_Exit_Stmt + (Span : FT.Source_Span; + Condition : CM.Expr_Access := null) return CM.Statement_Access + is + Result : constant CM.Statement_Access := new CM.Statement; + begin + Result.Kind := CM.Stmt_Exit; + Result.Is_Synthetic := True; + Result.Span := Span; + Result.Condition := Condition; + return Result; + end Synthetic_Exit_Stmt; + function Desugar_Executable_Expr (Expr : CM.Expr_Access; Var_Types : Type_Maps.Map; @@ -5722,45 +6111,911 @@ package body Safe_Frontend.Check_Resolve is return Result; end; end if; - Result.Expr := new CM.Expr_Node'(Expr.all); - Result.Expr.Args.Clear; - Child := - Desugar_Executable_Expr - (Expr.Callee, - Var_Types, - Functions, - Type_Env, - Has_Enclosing_Return, - Enclosing_Return_Type, - Path, - Reject_Short_Circuit_Try); - Result.Expr.Callee := Child.Expr; - Result.Preludes := Child.Preludes; - for Item of Expr.Args loop - Child := - Desugar_Executable_Expr - (Item, - Var_Types, - Functions, - Type_Env, - Has_Enclosing_Return, - Enclosing_Return_Type, - Path, - Reject_Short_Circuit_Try); - Append_Statements (Result.Preludes, Child.Preludes); - Result.Expr.Args.Append (Child.Expr); - end loop; - - when CM.Expr_Conversion | CM.Expr_Annotated | CM.Expr_Unary => - Result.Expr := new CM.Expr_Node'(Expr.all); - Child := - Desugar_Executable_Expr - (Expr.Inner, - Var_Types, - Functions, - Type_Env, - Has_Enclosing_Return, - Enclosing_Return_Type, + if Is_Contains_Builtin_Call (Expr, Var_Types, Functions, Type_Env) then + declare + Map_Child : constant Desugared_Expr_Result := + Desugar_Executable_Expr + (Expr.Args (Expr.Args.First_Index), + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Key_Child : constant Desugared_Expr_Result := + Desugar_Executable_Expr + (Expr.Args (Expr.Args.First_Index + 1), + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Map_Type : constant GM.Type_Descriptor := + Expr_Type (Map_Child.Expr, Var_Types, Functions, Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + Snapshot_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Value")); + Key_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Key")); + Length_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Len")); + Index_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Index")); + Result_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Contains")); + Entry_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Entry")); + Snapshot_Expr : CM.Expr_Access; + Key_Temp : CM.Expr_Access; + Length_Temp : CM.Expr_Access; + Index_Temp : CM.Expr_Access; + Result_Temp : CM.Expr_Access; + Entry_Expr : CM.Expr_Access; + Match_Then : CM.Statement_Access_Vectors.Vector; + Index_Guard_Then : CM.Statement_Access_Vectors.Vector; + Advance_Then : CM.Statement_Access_Vectors.Vector; + Advance_Else : CM.Statement_Access_Vectors.Vector; + Loop_Body : CM.Statement_Access_Vectors.Vector; + Entry_Type : GM.Type_Descriptor := Default_Integer; + Entry_Elements : FT.UString_Vectors.Vector; + begin + Append_Statements (Result.Preludes, Map_Child.Preludes); + Append_Statements (Result.Preludes, Key_Child.Preludes); + if not Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Expr.Span, + Message => "`contains` expects a `map of (K, V)` first argument")); + end if; + Entry_Elements.Append (Key_Type.Name); + Entry_Elements.Append (Value_Type.Name); + Entry_Type := Make_Tuple_Type (Entry_Elements); + + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Snapshot_Name), + Map_Type, + Map_Child.Expr, + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Key_Name), + Key_Type, + Key_Child.Expr, + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Length_Name), + Default_Integer, + Selector_Expr + (Ident_Expr + (UString_Value (Snapshot_Name), + Expr.Span, + UString_Value (Map_Type.Name)), + "length", + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Index_Name), + Default_Integer, + Int_Expr (1, Expr.Span), + Expr.Span, + Is_Constant => False)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Result_Name), + BT.Boolean_Type, + Bool_Expr (False, Expr.Span), + Expr.Span, + Is_Constant => False)); + + Snapshot_Expr := + Ident_Expr + (UString_Value (Snapshot_Name), + Expr.Span, + UString_Value (Map_Type.Name)); + Key_Temp := + Ident_Expr + (UString_Value (Key_Name), + Expr.Span, + UString_Value (Key_Type.Name)); + Length_Temp := + Ident_Expr + (UString_Value (Length_Name), + Expr.Span, + UString_Value (Default_Integer.Name)); + Index_Temp := + Ident_Expr + (UString_Value (Index_Name), + Expr.Span, + UString_Value (Default_Integer.Name)); + Result_Temp := + Ident_Expr + (UString_Value (Result_Name), + Expr.Span, + UString_Value (BT.Boolean_Type.Name)); + Entry_Expr := + Ident_Expr + (UString_Value (Entry_Name), + Expr.Span, + UString_Value (Entry_Type.Name)); + Index_Guard_Then.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Index_Temp, + "<", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + Index_Guard_Then, + Expr.Span)); + + Match_Then.Append + (Synthetic_Assign_Stmt + (Result_Temp, + Bool_Expr (True, Expr.Span), + Expr.Span)); + Match_Then.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Entry_Name), + Entry_Type, + Resolved_Index_Expr + (Snapshot_Expr, + Index_Temp, + Expr.Span, + UString_Value (Entry_Type.Name)), + Expr.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Unary_Expr + ("not", + Result_Temp, + Expr.Span, + "boolean"), + "and then", + Binary_Expr + (Selector_Expr + (Entry_Expr, + "1", + Expr.Span, + UString_Value (Key_Type.Name)), + "==", + Key_Temp, + Expr.Span, + "boolean"), + Expr.Span, + "boolean"), + Match_Then, + Expr.Span)); + Advance_Then.Append + (Synthetic_Assign_Stmt + (Index_Temp, + Binary_Expr + (Index_Temp, + "+", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span)); + Advance_Else.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_If_Else_Stmt + (Binary_Expr + (Index_Temp, + "<", + Length_Temp, + Expr.Span, + "boolean"), + Advance_Then, + Advance_Else, + Expr.Span)); + Result.Preludes.Append + (Synthetic_While_Stmt + (Binary_Expr + (Index_Temp, + "<=", + Length_Temp, + Expr.Span, + "boolean"), + Loop_Body, + Expr.Span)); + Result.Expr := Result_Temp; + return Result; + end; + end if; + if Is_Get_Builtin_Call (Expr, Var_Types, Functions, Type_Env) then + declare + Map_Child : constant Desugared_Expr_Result := + Desugar_Executable_Expr + (Expr.Args (Expr.Args.First_Index), + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Key_Child : constant Desugared_Expr_Result := + Desugar_Executable_Expr + (Expr.Args (Expr.Args.First_Index + 1), + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Map_Type : constant GM.Type_Descriptor := + Expr_Type (Map_Child.Expr, Var_Types, Functions, Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + Snapshot_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Value")); + Key_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Key")); + Length_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Len")); + Index_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Index")); + Result_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Get")); + Entry_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Entry")); + Snapshot_Expr : CM.Expr_Access; + Key_Temp : CM.Expr_Access; + Length_Temp : CM.Expr_Access; + Index_Temp : CM.Expr_Access; + Result_Temp : CM.Expr_Access; + Present_Expr : CM.Expr_Access; + Entry_Expr : CM.Expr_Access; + Match_Then : CM.Statement_Access_Vectors.Vector; + Index_Guard_Then : CM.Statement_Access_Vectors.Vector; + Advance_Then : CM.Statement_Access_Vectors.Vector; + Advance_Else : CM.Statement_Access_Vectors.Vector; + Loop_Body : CM.Statement_Access_Vectors.Vector; + Optional_Type : GM.Type_Descriptor := Default_Integer; + Entry_Type : GM.Type_Descriptor := Default_Integer; + Entry_Elements : FT.UString_Vectors.Vector; + begin + Append_Statements (Result.Preludes, Map_Child.Preludes); + Append_Statements (Result.Preludes, Key_Child.Preludes); + if not Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Expr.Span, + Message => "`get` expects a `map of (K, V)` first argument")); + end if; + + Optional_Type := Make_Optional_Type (Value_Type, Type_Env); + Entry_Elements.Append (Key_Type.Name); + Entry_Elements.Append (Value_Type.Name); + Entry_Type := Make_Tuple_Type (Entry_Elements); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Snapshot_Name), + Map_Type, + Map_Child.Expr, + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Key_Name), + Key_Type, + Key_Child.Expr, + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Length_Name), + Default_Integer, + Selector_Expr + (Ident_Expr + (UString_Value (Snapshot_Name), + Expr.Span, + UString_Value (Map_Type.Name)), + "length", + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Index_Name), + Default_Integer, + Int_Expr (1, Expr.Span), + Expr.Span, + Is_Constant => False)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Result_Name), + Optional_Type, + Build_Optional_None_Expr (Optional_Type, Expr.Span), + Expr.Span, + Is_Constant => False)); + + Snapshot_Expr := + Ident_Expr + (UString_Value (Snapshot_Name), + Expr.Span, + UString_Value (Map_Type.Name)); + Key_Temp := + Ident_Expr + (UString_Value (Key_Name), + Expr.Span, + UString_Value (Key_Type.Name)); + Length_Temp := + Ident_Expr + (UString_Value (Length_Name), + Expr.Span, + UString_Value (Default_Integer.Name)); + Index_Temp := + Ident_Expr + (UString_Value (Index_Name), + Expr.Span, + UString_Value (Default_Integer.Name)); + Result_Temp := + Ident_Expr + (UString_Value (Result_Name), + Expr.Span, + UString_Value (Optional_Type.Name)); + Present_Expr := + Selector_Expr + (Result_Temp, + "present", + Expr.Span, + "boolean"); + Entry_Type := Growable_Array_Element_Type (Map_Type, Type_Env); + Entry_Expr := + Ident_Expr + (UString_Value (Entry_Name), + Expr.Span, + UString_Value (Entry_Type.Name)); + Index_Guard_Then.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Index_Temp, + "<", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + Index_Guard_Then, + Expr.Span)); + + Match_Then.Append + (Synthetic_Assign_Stmt + (Result_Temp, + Build_Optional_Some_Expr + (Optional_Type, + Selector_Expr + (Entry_Expr, + "2", + Expr.Span, + UString_Value (Value_Type.Name)), + Expr.Span), + Expr.Span)); + Match_Then.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Entry_Name), + Entry_Type, + Resolved_Index_Expr + (Snapshot_Expr, + Index_Temp, + Expr.Span, + UString_Value (Entry_Type.Name)), + Expr.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Unary_Expr + ("not", + Present_Expr, + Expr.Span, + "boolean"), + "and then", + Binary_Expr + (Selector_Expr + (Entry_Expr, + "1", + Expr.Span, + UString_Value (Key_Type.Name)), + "==", + Key_Temp, + Expr.Span, + "boolean"), + Expr.Span, + "boolean"), + Match_Then, + Expr.Span)); + Advance_Then.Append + (Synthetic_Assign_Stmt + (Index_Temp, + Binary_Expr + (Index_Temp, + "+", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span)); + Advance_Else.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_If_Else_Stmt + (Binary_Expr + (Index_Temp, + "<", + Length_Temp, + Expr.Span, + "boolean"), + Advance_Then, + Advance_Else, + Expr.Span)); + Result.Preludes.Append + (Synthetic_While_Stmt + (Binary_Expr + (Index_Temp, + "<=", + Length_Temp, + Expr.Span, + "boolean"), + Loop_Body, + Expr.Span)); + Result.Expr := Result_Temp; + return Result; + end; + end if; + if Is_Remove_Builtin_Call (Expr, Var_Types, Functions, Type_Env) then + declare + Map_Child : constant Desugared_Expr_Result := + Desugar_Executable_Expr + (Expr.Args (Expr.Args.First_Index), + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Key_Child : constant Desugared_Expr_Result := + Desugar_Executable_Expr + (Expr.Args (Expr.Args.First_Index + 1), + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Map_Type : constant GM.Type_Descriptor := + Expr_Type (Map_Child.Expr, Var_Types, Functions, Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + Optional_Type : GM.Type_Descriptor := Default_Integer; + Snapshot_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Value")); + Key_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Key")); + Length_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Len")); + Index_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Index")); + Result_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Remove")); + Entry_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Entry")); + Snapshot_Expr : CM.Expr_Access; + Key_Temp : CM.Expr_Access; + Length_Temp : CM.Expr_Access; + Index_Temp : CM.Expr_Access; + Result_Temp : CM.Expr_Access; + Entry_Expr : CM.Expr_Access; + Last_Entry_Expr : CM.Expr_Access; + Match_Then : CM.Statement_Access_Vectors.Vector; + Trim_Then : CM.Statement_Access_Vectors.Vector; + Trim_Else : CM.Statement_Access_Vectors.Vector; + Rebuild_Then : CM.Statement_Access_Vectors.Vector; + Prefix_Then : CM.Statement_Access_Vectors.Vector; + Prefix_Else : CM.Statement_Access_Vectors.Vector; + Suffix_Then : CM.Statement_Access_Vectors.Vector; + Index_Guard_Then : CM.Statement_Access_Vectors.Vector; + Loop_Body : CM.Statement_Access_Vectors.Vector; + Advance_Then : CM.Statement_Access_Vectors.Vector; + Advance_Else : CM.Statement_Access_Vectors.Vector; + Empty_Map_Expr : constant CM.Expr_Access := new CM.Expr_Node; + Last_Literal_Expr : constant CM.Expr_Access := new CM.Expr_Node; + Entry_Type : GM.Type_Descriptor := Default_Integer; + Entry_Elements : FT.UString_Vectors.Vector; + begin + Append_Statements (Result.Preludes, Map_Child.Preludes); + Append_Statements (Result.Preludes, Key_Child.Preludes); + if not Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Expr.Span, + Message => "`remove` expects a `map of (K, V)` first argument")); + end if; + + Optional_Type := Make_Optional_Type (Value_Type, Type_Env); + Entry_Elements.Append (Key_Type.Name); + Entry_Elements.Append (Value_Type.Name); + Entry_Type := Make_Tuple_Type (Entry_Elements); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Snapshot_Name), + Map_Type, + Map_Child.Expr, + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Key_Name), + Key_Type, + Key_Child.Expr, + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Length_Name), + Default_Integer, + Selector_Expr + (Ident_Expr + (UString_Value (Snapshot_Name), + Expr.Span, + UString_Value (Map_Type.Name)), + "length", + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Index_Name), + Default_Integer, + Int_Expr (1, Expr.Span), + Expr.Span, + Is_Constant => False)); + Result.Preludes.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Result_Name), + Optional_Type, + Build_Optional_None_Expr (Optional_Type, Expr.Span), + Expr.Span, + Is_Constant => False)); + Snapshot_Expr := + Ident_Expr + (UString_Value (Snapshot_Name), + Expr.Span, + UString_Value (Map_Type.Name)); + Key_Temp := + Ident_Expr + (UString_Value (Key_Name), + Expr.Span, + UString_Value (Key_Type.Name)); + Length_Temp := + Ident_Expr + (UString_Value (Length_Name), + Expr.Span, + UString_Value (Default_Integer.Name)); + Index_Temp := + Ident_Expr + (UString_Value (Index_Name), + Expr.Span, + UString_Value (Default_Integer.Name)); + Result_Temp := + Ident_Expr + (UString_Value (Result_Name), + Expr.Span, + UString_Value (Optional_Type.Name)); + Entry_Expr := + Ident_Expr + (UString_Value (Entry_Name), + Expr.Span, + UString_Value (Entry_Type.Name)); + Last_Entry_Expr := + Resolved_Index_Expr + (Snapshot_Expr, + Length_Temp, + Expr.Span, + UString_Value (Entry_Type.Name)); + Empty_Map_Expr.Kind := CM.Expr_Array_Literal; + Empty_Map_Expr.Span := Expr.Span; + Empty_Map_Expr.Type_Name := Map_Type.Name; + Last_Literal_Expr.Kind := CM.Expr_Array_Literal; + Last_Literal_Expr.Span := Expr.Span; + Last_Literal_Expr.Type_Name := Map_Type.Name; + Last_Literal_Expr.Elements.Append (Last_Entry_Expr); + Index_Guard_Then.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Index_Temp, + "<", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + Index_Guard_Then, + Expr.Span)); + + Match_Then.Append + (Synthetic_Assign_Stmt + (Result_Temp, + Build_Optional_Some_Expr + (Optional_Type, + Selector_Expr + (Entry_Expr, + "2", + Expr.Span, + UString_Value (Value_Type.Name)), + Expr.Span), + Expr.Span)); + Trim_Then.Append + (Synthetic_Assign_Stmt + (Map_Child.Expr, + Empty_Map_Expr, + Expr.Span)); + Trim_Else.Append + (Synthetic_Assign_Stmt + (Map_Child.Expr, + Resolved_Index_Expr + (Map_Child.Expr, + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Map_Type.Name), + Binary_Expr + (Length_Temp, + "-", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name))), + Expr.Span)); + Prefix_Then.Append + (Synthetic_Assign_Stmt + (Map_Child.Expr, + Last_Literal_Expr, + Expr.Span)); + Prefix_Else.Append + (Synthetic_Assign_Stmt + (Map_Child.Expr, + Binary_Expr + (Resolved_Index_Expr + (Snapshot_Expr, + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Map_Type.Name), + Binary_Expr + (Index_Temp, + "-", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name))), + "&", + Last_Literal_Expr, + Expr.Span, + UString_Value (Map_Type.Name)), + Expr.Span)); + Rebuild_Then.Append + (Synthetic_If_Else_Stmt + (Binary_Expr + (Index_Temp, + "==", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + Prefix_Then, + Prefix_Else, + Expr.Span)); + Suffix_Then.Append + (Synthetic_Assign_Stmt + (Map_Child.Expr, + Binary_Expr + (Map_Child.Expr, + "&", + Resolved_Index_Expr + (Snapshot_Expr, + Binary_Expr + (Index_Temp, + "+", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span, + UString_Value (Map_Type.Name), + Binary_Expr + (Length_Temp, + "-", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name))), + Expr.Span, + UString_Value (Map_Type.Name)), + Expr.Span)); + Rebuild_Then.Append + (Synthetic_If_Stmt + (Binary_Expr + (Index_Temp, + "<", + Binary_Expr + (Length_Temp, + "-", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span, + "boolean"), + Suffix_Then, + Expr.Span)); + Match_Then.Append + (Synthetic_If_Stmt + (Binary_Expr + (Length_Temp, + "==", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + Trim_Then, + Expr.Span)); + Match_Then.Append + (Synthetic_If_Stmt + (Binary_Expr + (Binary_Expr + (Length_Temp, + ">", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + "and then", + Binary_Expr + (Index_Temp, + "==", + Length_Temp, + Expr.Span, + "boolean"), + Expr.Span, + "boolean"), + Trim_Else, + Expr.Span)); + Match_Then.Append + (Synthetic_If_Stmt + (Binary_Expr + (Binary_Expr + (Length_Temp, + ">", + Int_Expr (1, Expr.Span), + Expr.Span, + "boolean"), + "and then", + Binary_Expr + (Index_Temp, + "<", + Length_Temp, + Expr.Span, + "boolean"), + Expr.Span, + "boolean"), + Rebuild_Then, + Expr.Span)); + Match_Then.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Entry_Name), + Entry_Type, + Resolved_Index_Expr + (Snapshot_Expr, + Index_Temp, + Expr.Span, + UString_Value (Entry_Type.Name)), + Expr.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Selector_Expr + (Entry_Expr, + "1", + Expr.Span, + UString_Value (Key_Type.Name)), + "==", + Key_Temp, + Expr.Span, + "boolean"), + Match_Then, + Expr.Span)); + Advance_Then.Append + (Synthetic_Assign_Stmt + (Index_Temp, + Binary_Expr + (Index_Temp, + "+", + Int_Expr (1, Expr.Span), + Expr.Span, + UString_Value (Default_Integer.Name)), + Expr.Span)); + Advance_Else.Append + (Synthetic_Exit_Stmt (Expr.Span)); + Loop_Body.Append + (Synthetic_If_Else_Stmt + (Binary_Expr + (Index_Temp, + "<", + Length_Temp, + Expr.Span, + "boolean"), + Advance_Then, + Advance_Else, + Expr.Span)); + Result.Preludes.Append + (Synthetic_While_Stmt + (Binary_Expr + (Index_Temp, + "<=", + Length_Temp, + Expr.Span, + "boolean"), + Loop_Body, + Expr.Span)); + Result.Expr := Result_Temp; + return Result; + end; + end if; + if Is_Set_Builtin_Call (Expr, Var_Types, Functions, Type_Env) then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => (if Expr.Has_Call_Span then Expr.Call_Span else Expr.Span), + Message => "`set(m, key, value)` mutates a writable map and must be used as a statement")); + end if; + Result.Expr := new CM.Expr_Node'(Expr.all); + Result.Expr.Args.Clear; + Child := + Desugar_Executable_Expr + (Expr.Callee, + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Result.Expr.Callee := Child.Expr; + Result.Preludes := Child.Preludes; + for Item of Expr.Args loop + Child := + Desugar_Executable_Expr + (Item, + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, + Path, + Reject_Short_Circuit_Try); + Append_Statements (Result.Preludes, Child.Preludes); + Result.Expr.Args.Append (Child.Expr); + end loop; + + when CM.Expr_Conversion | CM.Expr_Annotated | CM.Expr_Unary => + Result.Expr := new CM.Expr_Node'(Expr.all); + Child := + Desugar_Executable_Expr + (Expr.Inner, + Var_Types, + Functions, + Type_Env, + Has_Enclosing_Return, + Enclosing_Return_Type, Path, Reject_Short_Circuit_Try); Result.Expr.Inner := Child.Expr; @@ -6816,6 +8071,437 @@ package body Safe_Frontend.Check_Resolve is Exact_Length_Facts, Path, Has_Enclosing_Return, + Enclosing_Return_Type); + end; + end if; + elsif Is_Set_Builtin_Call + (Normalized_Call, Var_Types, Functions, Type_Env) + then + if Natural (Normalized_Call.Args.Length) /= 3 then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => (if Normalized_Call.Has_Call_Span + then Normalized_Call.Call_Span + else Normalized_Call.Span), + Message => "`set(m, key, value)` expects exactly three arguments")); + elsif not Is_Assignable_Target + (Normalized_Call.Args (Normalized_Call.Args.First_Index)) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Normalized_Call.Args (Normalized_Call.Args.First_Index).Span, + Message => "`set` first argument must be a writable map name")); + else + declare + Map_Target : constant CM.Expr_Access := + Normalized_Call.Args (Normalized_Call.Args.First_Index); + Map_Type : constant GM.Type_Descriptor := + Expr_Type (Map_Target, Var_Types, Functions, Type_Env); + Key_Type : GM.Type_Descriptor; + Value_Type : GM.Type_Descriptor; + Key_Expr : CM.Expr_Access := + Normalized_Call.Args (Normalized_Call.Args.First_Index + 1); + Value_Expr : CM.Expr_Access := + Normalized_Call.Args (Normalized_Call.Args.First_Index + 2); + Entry_Type : GM.Type_Descriptor := Default_Integer; + Key_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Key")); + Value_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Value")); + Length_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Len")); + Index_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Index")); + Found_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Found")); + Key_Temp : CM.Expr_Access; + Value_Temp : CM.Expr_Access; + Length_Temp : CM.Expr_Access; + Index_Temp : CM.Expr_Access; + Found_Temp : CM.Expr_Access; + Entry_Expr : CM.Expr_Access; + Entry_Value : CM.Expr_Access; + Literal : constant CM.Expr_Access := new CM.Expr_Node; + Loop_Body : CM.Statement_Access_Vectors.Vector; + Match_Then : CM.Statement_Access_Vectors.Vector; + Append_Missing_Then : CM.Statement_Access_Vectors.Vector; + Rebuild_Then : CM.Statement_Access_Vectors.Vector; + Prefix_Then : CM.Statement_Access_Vectors.Vector; + Prefix_Else : CM.Statement_Access_Vectors.Vector; + Suffix_Then : CM.Statement_Access_Vectors.Vector; + Index_Guard_Then : CM.Statement_Access_Vectors.Vector; + Advance_Then : CM.Statement_Access_Vectors.Vector; + Advance_Else : CM.Statement_Access_Vectors.Vector; + Rewritten_Stmts : CM.Statement_Access_Vectors.Vector; + Entry_Elements : FT.UString_Vectors.Vector; + begin + if not Try_Map_Key_Value_Types (Map_Type, Type_Env, Key_Type, Value_Type) then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Map_Target.Span, + Message => "`set` expects a `mut map of (K, V)` first argument")); + elsif not Is_Map_Key_Type_Allowed (Key_Type, Type_Env) then + Raise_Diag + (CM.Unsupported_Source_Construct + (Path => Path, + Span => Map_Target.Span, + Message => + "`map of (K, V)` keys are limited to the admitted discrete/string subset in PR11.10c")); + elsif not Is_Container_Element_Type_Allowed (Value_Type, Type_Env) then + Raise_Diag + (CM.Unsupported_Source_Construct + (Path => Path, + Span => Map_Target.Span, + Message => + "`map of (K, V)` values are limited to the admitted value-type subset in PR11.10c")); + end if; + Entry_Elements.Append (Key_Type.Name); + Entry_Elements.Append (Value_Type.Name); + + Ensure_Writable_Target + (Map_Target, + Imported_Objects, + Local_Constants, + Local_Static_Constants, + Path, + "assignment to imported package-qualified objects is outside the current PR08.3 interface subset"); + + Key_Expr := + Contextualize_Expr_To_Target_Type + (Key_Expr, + Key_Type, + Var_Types, + Functions, + Type_Env, + Path); + Value_Expr := + Contextualize_Expr_To_Target_Type + (Value_Expr, + Value_Type, + Var_Types, + Functions, + Type_Env, + Path); + Reject_Uncontextualized_None (Key_Expr, Path); + Reject_Uncontextualized_None (Value_Expr, Path); + if not Compatible_Source_Expr_To_Target_Type + (Key_Expr, + Expr_Type (Key_Expr, Var_Types, Functions, Type_Env), + Key_Type, + Var_Types, + Functions, + Type_Env, + Local_Static_Constants, + Exact_Length_Facts) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Key_Expr.Span, + Message => "`set` key type does not match the map key type")); + elsif not Compatible_Source_Expr_To_Target_Type + (Value_Expr, + Expr_Type (Value_Expr, Var_Types, Functions, Type_Env), + Value_Type, + Var_Types, + Functions, + Type_Env, + Local_Static_Constants, + Exact_Length_Facts) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => Value_Expr.Span, + Message => "`set` value type does not match the map value type")); + end if; + + declare + Snapshot_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Value")); + Entry_Name : constant FT.UString := + FT.To_UString (Next_Synthetic_Name ("Safe_Map_Entry")); + Snapshot_Expr : CM.Expr_Access; + begin + Rewritten_Stmts.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Snapshot_Name), + Map_Type, + Map_Target, + Stmt.Span)); + Rewritten_Stmts.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Key_Name), + Key_Type, + Key_Expr, + Stmt.Span)); + Rewritten_Stmts.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Value_Name), + Value_Type, + Value_Expr, + Stmt.Span)); + Rewritten_Stmts.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Length_Name), + Default_Integer, + Selector_Expr + (Ident_Expr + (UString_Value (Snapshot_Name), + Stmt.Span, + UString_Value (Map_Type.Name)), + "length", + Stmt.Span, + UString_Value (Default_Integer.Name)), + Stmt.Span)); + Rewritten_Stmts.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Index_Name), + Default_Integer, + Int_Expr (1, Stmt.Span), + Stmt.Span, + Is_Constant => False)); + Rewritten_Stmts.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Found_Name), + BT.Boolean_Type, + Bool_Expr (False, Stmt.Span), + Stmt.Span, + Is_Constant => False)); + + Entry_Type := Make_Tuple_Type (Entry_Elements); + Snapshot_Expr := + Ident_Expr + (UString_Value (Snapshot_Name), + Stmt.Span, + UString_Value (Map_Type.Name)); + Key_Temp := + Ident_Expr + (UString_Value (Key_Name), + Stmt.Span, + UString_Value (Key_Type.Name)); + Value_Temp := + Ident_Expr + (UString_Value (Value_Name), + Stmt.Span, + UString_Value (Value_Type.Name)); + Length_Temp := + Ident_Expr + (UString_Value (Length_Name), + Stmt.Span, + UString_Value (Default_Integer.Name)); + Index_Temp := + Ident_Expr + (UString_Value (Index_Name), + Stmt.Span, + UString_Value (Default_Integer.Name)); + Found_Temp := + Ident_Expr + (UString_Value (Found_Name), + Stmt.Span, + UString_Value (BT.Boolean_Type.Name)); + Entry_Expr := + Ident_Expr + (UString_Value (Entry_Name), + Stmt.Span, + UString_Value (Entry_Type.Name)); + Entry_Value := + Tuple_Expr + (Key_Temp, + Value_Temp, + Stmt.Span, + UString_Value (Entry_Type.Name)); + Index_Guard_Then.Append + (Synthetic_Exit_Stmt (Stmt.Span)); + + Literal.Kind := CM.Expr_Array_Literal; + Literal.Span := Stmt.Span; + Literal.Type_Name := Map_Type.Name; + Literal.Elements.Append (Entry_Value); + Append_Missing_Then.Append + (Synthetic_Assign_Stmt + (Map_Target, + Binary_Expr + (Snapshot_Expr, + "&", + Literal, + Stmt.Span, + UString_Value (Map_Type.Name)), + Stmt.Span)); + Prefix_Then.Append + (Synthetic_Assign_Stmt + (Map_Target, + Literal, + Stmt.Span)); + Prefix_Else.Append + (Synthetic_Assign_Stmt + (Map_Target, + Binary_Expr + (Resolved_Index_Expr + (Snapshot_Expr, + Int_Expr (1, Stmt.Span), + Stmt.Span, + UString_Value (Map_Type.Name), + Binary_Expr + (Index_Temp, + "-", + Int_Expr (1, Stmt.Span), + Stmt.Span, + UString_Value (Default_Integer.Name))), + "&", + Literal, + Stmt.Span, + UString_Value (Map_Type.Name)), + Stmt.Span)); + Rebuild_Then.Append + (Synthetic_If_Else_Stmt + (Binary_Expr + (Index_Temp, + "==", + Int_Expr (1, Stmt.Span), + Stmt.Span, + "boolean"), + Prefix_Then, + Prefix_Else, + Stmt.Span)); + Suffix_Then.Append + (Synthetic_Assign_Stmt + (Map_Target, + Binary_Expr + (Map_Target, + "&", + Resolved_Index_Expr + (Snapshot_Expr, + Binary_Expr + (Index_Temp, + "+", + Int_Expr (1, Stmt.Span), + Stmt.Span, + UString_Value (Default_Integer.Name)), + Stmt.Span, + UString_Value (Map_Type.Name), + Length_Temp), + Stmt.Span, + UString_Value (Map_Type.Name)), + Stmt.Span)); + Rebuild_Then.Append + (Synthetic_If_Stmt + (Binary_Expr + (Index_Temp, + "<", + Length_Temp, + Stmt.Span, + "boolean"), + Suffix_Then, + Stmt.Span)); + Match_Then.Append + (Synthetic_Assign_Stmt + (Found_Temp, + Bool_Expr (True, Stmt.Span), + Stmt.Span)); + Match_Then.Append + (Synthetic_If_Stmt + (Found_Temp, + Rebuild_Then, + Stmt.Span)); + Match_Then.Append + (Synthetic_Exit_Stmt (Stmt.Span)); + + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Index_Temp, + "<", + Int_Expr (1, Stmt.Span), + Stmt.Span, + "boolean"), + Index_Guard_Then, + Stmt.Span)); + Loop_Body.Append + (Synthetic_Object_Decl_Stmt + (UString_Value (Entry_Name), + Entry_Type, + Resolved_Index_Expr + (Snapshot_Expr, + Index_Temp, + Stmt.Span, + UString_Value (Entry_Type.Name)), + Stmt.Span)); + Loop_Body.Append + (Synthetic_If_Stmt + (Binary_Expr + (Selector_Expr + (Entry_Expr, + "1", + Stmt.Span, + UString_Value (Key_Type.Name)), + "==", + Key_Temp, + Stmt.Span, + "boolean"), + Match_Then, + Stmt.Span)); + Advance_Then.Append + (Synthetic_Assign_Stmt + (Index_Temp, + Binary_Expr + (Index_Temp, + "+", + Int_Expr (1, Stmt.Span), + Stmt.Span, + UString_Value (Default_Integer.Name)), + Stmt.Span)); + Advance_Else.Append + (Synthetic_Exit_Stmt (Stmt.Span)); + Loop_Body.Append + (Synthetic_If_Else_Stmt + (Binary_Expr + (Index_Temp, + "<", + Length_Temp, + Stmt.Span, + "boolean"), + Advance_Then, + Advance_Else, + Stmt.Span)); + Rewritten_Stmts.Append + (Synthetic_While_Stmt + (Binary_Expr + (Index_Temp, + "<=", + Length_Temp, + Stmt.Span, + "boolean"), + Loop_Body, + Stmt.Span)); + + Rewritten_Stmts.Append + (Synthetic_If_Stmt + (Unary_Expr + ("not", + Found_Temp, + Stmt.Span, + "boolean"), + Append_Missing_Then, + Stmt.Span)); + end; + + return + Normalize_Statement_List + (Rewritten_Stmts, + Var_Types, + Functions, + Type_Env, + Channel_Env, + Imported_Objects, + Local_Constants, + Local_Static_Constants, + Exact_Length_Facts, + Path, + Has_Enclosing_Return, Enclosing_Return_Type); end; end if; @@ -6829,6 +8515,36 @@ package body Safe_Frontend.Check_Resolve is then Normalized_Call.Call_Span else Normalized_Call.Span), Message => "`pop_last(items)` returns an `optional T` value and must be used in an expression")); + elsif Is_Contains_Builtin_Call + (Normalized_Call, Var_Types, Functions, Type_Env) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => (if Normalized_Call.Has_Call_Span + then Normalized_Call.Call_Span + else Normalized_Call.Span), + Message => "`contains(m, key)` returns a `boolean` value and must be used in an expression")); + elsif Is_Get_Builtin_Call + (Normalized_Call, Var_Types, Functions, Type_Env) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => (if Normalized_Call.Has_Call_Span + then Normalized_Call.Call_Span + else Normalized_Call.Span), + Message => "`get(m, key)` returns an `optional V` value and must be used in an expression")); + elsif Is_Remove_Builtin_Call + (Normalized_Call, Var_Types, Functions, Type_Env) + then + Raise_Diag + (CM.Source_Frontend_Error + (Path => Path, + Span => (if Normalized_Call.Has_Call_Span + then Normalized_Call.Call_Span + else Normalized_Call.Span), + Message => "`remove(m, key)` mutates a map and returns an `optional V` value, so it must be used in an expression")); end if; end; declare @@ -8248,6 +9964,13 @@ package body Safe_Frontend.Check_Resolve is if Spec.Element_Type /= null then Collect_Type_Spec_Dependencies (Spec.Element_Type.all, Deps); end if; + when CM.Type_Spec_Map => + if Spec.Key_Type /= null then + Collect_Type_Spec_Dependencies (Spec.Key_Type.all, Deps); + end if; + if Spec.Value_Type /= null then + Collect_Type_Spec_Dependencies (Spec.Value_Type.all, Deps); + end if; when CM.Type_Spec_Tuple => for Item of Spec.Tuple_Elements loop Collect_Type_Spec_Dependencies (Item.all, Deps); @@ -9198,11 +10921,7 @@ package body Safe_Frontend.Check_Resolve is end loop; for Helper_Name of Synthetic_Helper_Order loop - if Helper_Name'Length < 8 - or else Helper_Name (Helper_Name'First .. Helper_Name'First + 7) /= "__tuple_" - then - Result.Types.Append (Get_Type (Synthetic_Helper_Types, Helper_Name)); - end if; + Result.Types.Append (Get_Type (Synthetic_Helper_Types, Helper_Name)); end loop; for Optional_Name of Synthetic_Optional_Order loop diff --git a/docs/PR11.x-series-proposed.md b/docs/PR11.x-series-proposed.md index 4a323928..1f5c7efe 100644 --- a/docs/PR11.x-series-proposed.md +++ b/docs/PR11.x-series-proposed.md @@ -2008,20 +2008,42 @@ Follows PR11.10a. Key-value lookup container. The third container type. +### Locked decisions + +- **No brace literal** in this slice. Maps are constructed from an empty + default value and populated via `set`. Brace literal syntax is deferred + to avoid new lexer tokens and disambiguation work before real usage + patterns are established. +- **Free builtins**, not selector methods: `contains(m, k)`, `get(m, k)`, + `set(m, k, v)`, `remove(m, k)`. These become `m.contains(k)` etc. + automatically when PR11.11a method syntax ships. +- **`remove` returns `optional V`**: `some(old_value)` if the key existed, + `none` if not. Consistent with `pop_last` returning `optional T`. +- **Iteration order is unspecified**: `for entry of m` visits every entry + exactly once; the order is deterministic for a given map state but is + not guaranteed to be insertion order or key order. + ### Scope - `map of (K, V)` as a built-in type constructor. -- Construction: `{key1: value1, key2: value2}` brace literals. -- Operations: `.length`, `.contains(key)`, `.get(key)` returning - `optional V`, `.set(key, value)`, `.remove(key)`, `for entry of m` - iteration yielding `(K, V)` tuples. +- Construction: empty default initialization; populated via `set(m, k, v)`. +- Operations (free builtins): + - `contains(m, k)` returns `boolean` + - `get(m, k)` returns `optional V` + - `set(m, k, v)` — statement-only; `m` must be writable + - `remove(m, k)` returns `optional V` — expression-only; `m` must be writable + - `.length` as a selector + - `for entry of m` iteration yielding `(K, V)` tuples - Key types must support equality (`==`). Admitted key types: scalars, enums, bounded strings, plain strings. - Value types: same as `optional T` — value types only. - Value-type semantics: assignment copies, scope exit frees. -- Internally, the compiler instantiates a monomorphic Ada implementation. - The implementation strategy (hash table, sorted array, or other) is - compiler-internal and not exposed to the user. +- Internally, `map of (K, V)` reuses the growable-container pipeline as an + unsorted sequence of synthetic `(K, V)` tuples. +- `set` does a linear scan and replaces an existing value in place when the + key is present; otherwise it appends a new entry. +- `remove` does a linear scan and uses swap-with-last removal, so iteration + order remains intentionally unspecified in this slice. ### Dependency @@ -2691,6 +2713,20 @@ exists so that no deferred item drifts without a name. | Expression-form `match` | Statement-form `match` shipped first; expression-form needs type-flow and emission work across both arms | | Ownership-specific discriminant extensions | No accepted example currently requires them in the admitted surface | +### Deferred from PR11.10b + +| Item | Why deferred | Future home | +|------|-------------|-------------| +| Non-static / non-singleton indexed `mut` alias paths | PR11.10b ships only statically provable singleton disjoint indices; broader container-element alias reasoning deferred | Post-PR11.10; scope after real usage patterns emerge | +| Empty-list `pop_last` proof closure | `pr1110b_list_empty_build.safe` is a runtime-only witness; static empty-length lowering triggers GNATprove ineffectual-branch warnings | Proof exclusion with documented reason; revisit if GNATprove improves branch-elimination handling | + +### Deferred from PR11.10c + +| Item | Why deferred | Future home | +|------|-------------|-------------| +| Brace literal for map construction (`{k: v, ...}`) | Requires new lexer tokens and parser productions; deferred to avoid syntax design before real usage patterns | Post-PR11.11 or standalone syntax slice when brace semantics are clear | +| Guaranteed map iteration order (insertion or key order) | Constrains internal implementation; unspecified-but-deterministic is sufficient for the first slice | Add as `sorted_map of (K, V)` or explicit `sorted_keys(m)` if ordered iteration is needed | + ### Deferred indefinitely / not scheduled | Item | Why | diff --git a/docs/tutorial.md b/docs/tutorial.md index d73cdf67..33690ab8 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -326,6 +326,35 @@ function tail_or_zero returns integer `array of T` still works. `list of T` is an alias surface over the same growable representation, not a second runtime. +`PR11.10c` adds the next container slice: + +- `map of (K, V)` is the user-facing spelling for a growable sequence of + `(K, V)` entries, +- maps default-initialize to empty values, +- free builtins provide the first surface: + - `contains(m, key)` returns `boolean` + - `get(m, key)` returns `optional V` + - `set(m, key, value)` mutates a writable map in place + - `remove(m, key)` mutates a writable map and returns `optional V` +- `for entry of values` iterates `(K, V)` tuples, but iteration order is + intentionally unspecified in this first wedge. + +Example: + +```safe +function lookup_or_zero returns integer + var values : map of (integer, integer); + found : optional integer = none; + + set (values, 1, 10); + set (values, 1, 15); + found = get (values, 1); + if found.present + return found.value; + else + return 0; +``` + ## 6. "Silver By Construction": D27 In One Page Safe's Silver level is built around a simple premise: diff --git a/scripts/_lib/proof_inventory.py b/scripts/_lib/proof_inventory.py index 8b061a10..e1029c2f 100644 --- a/scripts/_lib/proof_inventory.py +++ b/scripts/_lib/proof_inventory.py @@ -191,6 +191,14 @@ class EmittedProofExclusion: ] +PR11_10C_CHECKPOINT_FIXTURES = [ + "tests/positive/pr1110c_map_basics.safe", + "tests/build/pr1110c_map_build.safe", + "tests/build/pr1110c_map_string_build.safe", + "tests/build/pr1110c_map_list_build.safe", +] + + PR11_8I1_CHECKPOINT_FIXTURES = [ "tests/positive/pr115_case_terminator.safe", "tests/positive/pr115_var_basic.safe", @@ -258,6 +266,7 @@ class EmittedProofExclusion: + PR11_8K_CHECKPOINT_FIXTURES + PR11_10A_CHECKPOINT_FIXTURES + PR11_10B_CHECKPOINT_FIXTURES + + PR11_10C_CHECKPOINT_FIXTURES + EMITTED_PROOF_REGRESSION_FIXTURES ) diff --git a/scripts/run_proofs.py b/scripts/run_proofs.py index aeb736ca..9b38df67 100644 --- a/scripts/run_proofs.py +++ b/scripts/run_proofs.py @@ -30,6 +30,7 @@ PR11_8K_CHECKPOINT_FIXTURES, PR11_10A_CHECKPOINT_FIXTURES, PR11_10B_CHECKPOINT_FIXTURES, + PR11_10C_CHECKPOINT_FIXTURES, PROOF_COVERAGE_ROOTS, iter_proof_coverage_paths, ) @@ -78,6 +79,7 @@ def validate_manifests() -> None: validate_manifest("PR11.8k checkpoint manifest", PR11_8K_CHECKPOINT_FIXTURES) validate_manifest("PR11.10a checkpoint manifest", PR11_10A_CHECKPOINT_FIXTURES) validate_manifest("PR11.10b checkpoint manifest", PR11_10B_CHECKPOINT_FIXTURES) + validate_manifest("PR11.10c checkpoint manifest", PR11_10C_CHECKPOINT_FIXTURES) validate_manifest("emitted proof regression manifest", EMITTED_PROOF_REGRESSION_FIXTURES) validate_manifest("emitted proof manifest", EMITTED_PROOF_FIXTURES) validate_manifest( @@ -215,6 +217,8 @@ def main() -> int: checkpoint_10a_failures: list[tuple[str, str]] = [] checkpoint_10b_passed = 0 checkpoint_10b_failures: list[tuple[str, str]] = [] + checkpoint_10c_passed = 0 + checkpoint_10c_failures: list[tuple[str, str]] = [] regression_passed = 0 regression_failures: list[tuple[str, str]] = [] @@ -288,6 +292,11 @@ def main() -> int: temp_root=temp_root, toolchain=toolchain, ) + checkpoint_10c_passed, checkpoint_10c_failures = run_fixture_group( + fixtures=PR11_10C_CHECKPOINT_FIXTURES, + temp_root=temp_root, + toolchain=toolchain, + ) regression_passed, regression_failures = run_fixture_group( fixtures=EMITTED_PROOF_REGRESSION_FIXTURES, temp_root=temp_root, @@ -307,6 +316,7 @@ def main() -> int: + checkpoint_k_passed + checkpoint_10a_passed + checkpoint_10b_passed + + checkpoint_10c_passed + regression_passed ) total_failures = ( @@ -322,6 +332,7 @@ def main() -> int: + checkpoint_k_failures + checkpoint_10a_failures + checkpoint_10b_failures + + checkpoint_10c_failures + regression_failures ) @@ -397,6 +408,12 @@ def main() -> int: title="PR11.10b checkpoint", trailing_blank_line=True, ) + print_summary( + passed=checkpoint_10c_passed, + failures=checkpoint_10c_failures, + title="PR11.10c checkpoint", + trailing_blank_line=True, + ) print_summary( passed=regression_passed, failures=regression_failures, diff --git a/scripts/run_tests.py b/scripts/run_tests.py index e8ee71ab..d66acafd 100644 --- a/scripts/run_tests.py +++ b/scripts/run_tests.py @@ -198,6 +198,12 @@ REPO_ROOT / "tests" / "interfaces" / "client_list.safe", 0, ), + ( + "map", + REPO_ROOT / "tests" / "interfaces" / "provider_map.safe", + REPO_ROOT / "tests" / "interfaces" / "client_map.safe", + 0, + ), ] INTERFACE_REJECT_CASES = [ @@ -249,6 +255,7 @@ REPO_ROOT / "tests" / "positive" / "pr118k_match.safe", REPO_ROOT / "tests" / "positive" / "pr1110a_optional_guarded.safe", REPO_ROOT / "tests" / "positive" / "pr1110b_list_basics.safe", + REPO_ROOT / "tests" / "positive" / "pr1110c_map_basics.safe", ] DIAGNOSTIC_GOLDEN_CASES = [ @@ -471,6 +478,21 @@ "2\n8\n1\n", False, ), + ( + REPO_ROOT / "tests" / "build" / "pr1110c_map_build.safe", + "15\n20\n1\n2\n", + False, + ), + ( + REPO_ROOT / "tests" / "build" / "pr1110c_map_string_build.safe", + "Bob\nAda\n", + False, + ), + ( + REPO_ROOT / "tests" / "build" / "pr1110c_map_list_build.safe", + "3\n3\n", + False, + ), ( REPO_ROOT / "tests" / "build" / "pr118d_tuple_string_build.safe", "ok\n", diff --git a/spec/08-syntax-summary.md b/spec/08-syntax-summary.md index 959bd8f2..52561c26 100644 --- a/spec/08-syntax-summary.md +++ b/spec/08-syntax-summary.md @@ -284,6 +284,7 @@ subtype_indication ::= [ 'not' 'null' ] subtype_mark [ constraint | inline_range_constraint ] | binary_type_definition | list_type_spec + | map_type_spec | optional_type_spec subtype_mark ::= @@ -293,11 +294,15 @@ type_target ::= subtype_mark | binary_type_definition | list_type_spec + | map_type_spec | optional_type_spec list_type_spec ::= 'list' 'of' subtype_indication +map_type_spec ::= + 'map' 'of' '(' subtype_indication ',' subtype_indication ')' + optional_type_spec ::= 'optional' subtype_indication @@ -589,10 +594,18 @@ assignment_statement ::= procedure_call_statement ::= name [ actual_parameter_part ] statement_terminator -The contextual builtins `append(items, value)` and `pop_last(items)` use -ordinary call syntax. `append` is admitted only as a procedure-call statement -on a writable `list of T` name. `pop_last` is admitted only as an expression -and returns `optional T`. +The contextual builtins `append(items, value)`, `pop_last(items)`, +`contains(m, key)`, `get(m, key)`, `set(m, key, value)`, and +`remove(m, key)` use ordinary call syntax. + +- `append` is admitted only as a procedure-call statement on a writable + `list of T` name. +- `pop_last` is admitted only as an expression and returns `optional T`. +- `contains` and `get` are expression-only map builtins. +- `set` is statement-only and requires a writable `map of (K, V)` first + argument. +- `remove` is expression-only, mutates a writable `map of (K, V)`, and + returns `optional V`. print_statement ::= 'print' '(' expression ')' statement_terminator diff --git a/tests/build/pr1110c_map_build.safe b/tests/build/pr1110c_map_build.safe new file mode 100644 index 00000000..777a462d --- /dev/null +++ b/tests/build/pr1110c_map_build.safe @@ -0,0 +1,53 @@ +package pr1110c_map_build + + function seeded returns map of (integer, integer) + var values : map of (integer, integer); + + set (values, 1, 10); + set (values, 2, 20); + set (values, 1, 15); + return values; + + function updated_value returns integer + var found : optional integer; + + found = get (seeded, 1); + if found.present + return found.value; + else + return 0; + + function removed_value returns integer + var values : map of (integer, integer) = seeded; + var removed : optional integer; + + removed = remove (values, 2); + if removed.present and then values.length == 1 and then not contains (values, 2) + return removed.value; + else + return 0; + + function remaining_length returns integer + var values : map of (integer, integer) = seeded; + var removed : optional integer; + + removed = remove (values, 2); + if removed.present and then not contains (values, 2) + return values.length; + else + return 0; + + function missing_length returns integer + var values : map of (integer, integer) = seeded; + var removed : optional integer; + + removed = remove (values, 3); + if removed.present + return 0; + else + return values.length; + + print (updated_value); + print (removed_value); + print (remaining_length); + print (missing_length); diff --git a/tests/build/pr1110c_map_list_build.safe b/tests/build/pr1110c_map_list_build.safe new file mode 100644 index 00000000..55b9f69e --- /dev/null +++ b/tests/build/pr1110c_map_list_build.safe @@ -0,0 +1,40 @@ +package pr1110c_map_list_build + + function seeded returns map of (string, list of integer) + var values : map of (string, list of integer); + nums : list of integer = [1, 2, 3]; + + set (values, "Ada", nums); + return values; + + function stored_length returns integer + var found : optional list of integer; + + if found.present + return 0; + found = get (seeded, "Ada"); + if found.present + return found.value.length; + else + return 0; + + function removed_length returns integer + var values : map of (string, list of integer) = seeded; + var removed : optional list of integer; + + if removed.present + return 0; + removed = remove (values, "Ada"); + if removed.present + if values.length == 0 + if contains (values, "Ada") + return 0; + else + return removed.value.length; + else + return 0; + else + return 0; + + print (stored_length); + print (removed_length); diff --git a/tests/build/pr1110c_map_string_build.safe b/tests/build/pr1110c_map_string_build.safe new file mode 100644 index 00000000..8177e552 --- /dev/null +++ b/tests/build/pr1110c_map_string_build.safe @@ -0,0 +1,40 @@ +package pr1110c_map_string_build + + function seeded returns map of (string, string) + var values : map of (string, string); + + set (values, "ada", "Ada"); + set (values, "bob", "Bob"); + return values; + + function lookup_text returns string + var found : optional string; + + if found.present + return "none"; + found = get (seeded, "bob"); + if found.present + return found.value; + else + return "none"; + + function removed_text returns string + var values : map of (string, string) = seeded; + var removed : optional string; + + if removed.present + return "none"; + removed = remove (values, "ada"); + if removed.present + if values.length == 1 + if contains (values, "ada") + return "none"; + else + return removed.value; + else + return "none"; + else + return "none"; + + print (lookup_text); + print (removed_text); diff --git a/tests/interfaces/client_map.safe b/tests/interfaces/client_map.safe new file mode 100644 index 00000000..7f7c8b48 --- /dev/null +++ b/tests/interfaces/client_map.safe @@ -0,0 +1,6 @@ +with provider_map; + +package client_map + + function total returns integer + return provider_map.lookup (provider_map.seeded, 2); diff --git a/tests/interfaces/provider_map.safe b/tests/interfaces/provider_map.safe new file mode 100644 index 00000000..ecdd5533 --- /dev/null +++ b/tests/interfaces/provider_map.safe @@ -0,0 +1,17 @@ +package provider_map + + public function seeded returns map of (integer, integer) + var values : map of (integer, integer); + + set (values, 1, 10); + set (values, 2, 20); + return values; + + public function lookup (values : map of (integer, integer); key : integer) returns integer + var found : optional integer; + + found = get (values, key); + if found.present + return found.value; + else + return 0; diff --git a/tests/negative/neg_pr1110c_map_bad_key.safe b/tests/negative/neg_pr1110c_map_bad_key.safe new file mode 100644 index 00000000..7a54f3d3 --- /dev/null +++ b/tests/negative/neg_pr1110c_map_bad_key.safe @@ -0,0 +1,8 @@ +-- Test: neg_pr1110c_map_bad_key +-- Description: `map of (K, V)` rejects disallowed key types. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_map_bad_key + + var values : map of (list of integer, integer); diff --git a/tests/negative/neg_pr1110c_map_key_mismatch.safe b/tests/negative/neg_pr1110c_map_key_mismatch.safe new file mode 100644 index 00000000..e794bbcf --- /dev/null +++ b/tests/negative/neg_pr1110c_map_key_mismatch.safe @@ -0,0 +1,9 @@ +-- Test: neg_pr1110c_map_key_mismatch +-- Description: Map builtin key arguments must match the map key type. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_map_key_mismatch + + var values : map of (integer, integer); + found : optional integer = get (values, "Ada"); diff --git a/tests/negative/neg_pr1110c_map_value_mismatch.safe b/tests/negative/neg_pr1110c_map_value_mismatch.safe new file mode 100644 index 00000000..34c75d79 --- /dev/null +++ b/tests/negative/neg_pr1110c_map_value_mismatch.safe @@ -0,0 +1,10 @@ +-- Test: neg_pr1110c_map_value_mismatch +-- Description: Map builtin value arguments must match the map value type. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_map_value_mismatch + + var values : map of (integer, integer); + + set (values, 1, "Ada"); diff --git a/tests/negative/neg_pr1110c_remove_constant.safe b/tests/negative/neg_pr1110c_remove_constant.safe new file mode 100644 index 00000000..6ba7970b --- /dev/null +++ b/tests/negative/neg_pr1110c_remove_constant.safe @@ -0,0 +1,9 @@ +-- Test: neg_pr1110c_remove_constant +-- Description: `remove(m, key)` requires a writable map target. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_remove_constant + + values : constant map of (integer, integer); + prior : optional integer = remove (values, 1); diff --git a/tests/negative/neg_pr1110c_remove_stmt.safe b/tests/negative/neg_pr1110c_remove_stmt.safe new file mode 100644 index 00000000..0a59edaf --- /dev/null +++ b/tests/negative/neg_pr1110c_remove_stmt.safe @@ -0,0 +1,11 @@ +-- Test: neg_pr1110c_remove_stmt +-- Description: `remove(m, key)` returns an `optional V` value and must be +-- used in an expression. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_remove_stmt + + var values : map of (integer, integer); + + remove (values, 1); diff --git a/tests/negative/neg_pr1110c_set_constant.safe b/tests/negative/neg_pr1110c_set_constant.safe new file mode 100644 index 00000000..1d6b65aa --- /dev/null +++ b/tests/negative/neg_pr1110c_set_constant.safe @@ -0,0 +1,10 @@ +-- Test: neg_pr1110c_set_constant +-- Description: `set(m, key, value)` requires a writable map target. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_set_constant + + values : constant map of (integer, integer); + + set (values, 1, 2); diff --git a/tests/negative/neg_pr1110c_set_non_map.safe b/tests/negative/neg_pr1110c_set_non_map.safe new file mode 100644 index 00000000..d1a2d3ac --- /dev/null +++ b/tests/negative/neg_pr1110c_set_non_map.safe @@ -0,0 +1,11 @@ +-- Test: neg_pr1110c_set_non_map +-- Description: `set(m, key, value)` requires a `mut map of (K, V)` first +-- argument. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: REJECT + +package neg_pr1110c_set_non_map + + var count : integer = 0; + + set (count, 1, 2); diff --git a/tests/positive/pr1110c_map_basics.safe b/tests/positive/pr1110c_map_basics.safe new file mode 100644 index 00000000..95d949ce --- /dev/null +++ b/tests/positive/pr1110c_map_basics.safe @@ -0,0 +1,44 @@ +-- Test: pr1110c_map_basics +-- Description: Built-in `map of (K, V)` reuses growable tuple storage with +-- default-empty construction, free builtins, and order-insensitive +-- iteration. +-- Clause: SAFE@468cf72:docs/PR11.x-series-proposed.md#pr1110c-built-in-map-of-k-v +-- Expected: ACCEPT + +package pr1110c_map_basics + + function singleton returns map of (integer, integer) + var values : map of (integer, integer); + + set (values, 1, 15); + return values; + + function entries_ok returns boolean + var values : map of (integer, integer) = singleton; + var saw_first : boolean = false; + + for item of values + if item.1 == 1 and then item.2 == 15 + saw_first = true; + + return saw_first; + + function default_is_empty returns boolean + var values : map of (integer, integer); + + return values.length == 0; + + function operations_ok returns boolean + var values : map of (integer, integer) = singleton; + var found : optional integer; + var missing : optional integer; + + found = get (values, 1); + missing = get (values, 2); + if not default_is_empty + return false; + if missing.present + return false; + if not found.present + return false; + return values.length == 1 and then found.value == 15 and then contains (values, 1) and then not contains (values, 2) and then entries_ok;