Remove support for type annotations for non-empty map and set literals

Author: lorchrob

src/lustre/lustreAstHelpers.ml

@@ -2084,12 +2084,6 @@ let pos_of_type ty = match ty with
   | TupleType (p, _)  | RecordType (p, _, _)  
   | RefinementType (p, _, _) -> p
 
-let rec find_type_annotation e = match e with 
-| StructUpdate (_, e, _, _) -> find_type_annotation e
-| EmptySet (_, ta) -> ta
-| EmptyMap (p, Some (kt, vt)) -> Some (Map (p, kt, vt))
-| _ -> None
-
 (* Return the node_id of a declaration if it is a node/func/contract decl *)
 let node_id_of_decl = function
   | NodeDecl (_, (id, _, _, _, _, _, _, _, _))

src/lustre/lustreAstHelpers.mli

@@ -212,7 +212,4 @@ val contains_subtype_satisfying: (lustre_type -> bool) -> lustre_type -> bool
 val pos_of_type: lustre_type -> Lib.position 
 (** `pos_of_type ty` returns the position of `ty` *)
 
-val find_type_annotation: expr -> lustre_type option
-(** `find_type_annotation e` recurses down `StructUpdates` to find the leaf-level type annotation, if one exists *)
-
 val node_id_of_decl: declaration -> NodeId.t option

src/lustre/lustreAstNormalizer.ml

@@ -2284,29 +2284,17 @@ and normalize_expr ?guard info (node_id : NI.t option) map =
     let nexpr = A.Ident (pos, name) in
     nexpr, union (union gids1 gids2) gids3, warnings1 @ warnings2
   | StructUpdate (pos, expr1, [A.MapIndex (_, expr2)], Some expr3) as expr ->
-    let gids1, warnings1 = match AH.find_type_annotation expr1 with 
-    | Some (Map (_, kt, vt)) -> 
-      let gids, warnings = mk_fresh_refinement_type_constraint Local info map pos node_id expr2 kt in 
-      let gids', warnings' = mk_fresh_refinement_type_constraint Local info map pos node_id expr3 vt in  
-      let gids'', warnings'' = mk_fresh_subrange_constraint ~force_prop:true Local info map pos node_id expr2 kt in 
-      let gids''', warnings''' = mk_fresh_subrange_constraint ~force_prop:true Local info map pos node_id expr3 vt in  
-      let gids = List.fold_left union (empty ()) [gids; gids'; gids''; gids'''] in 
-      let warnings = warnings @ warnings' @ warnings'' @ warnings''' in
-      gids,  warnings 
-    | None -> empty (), []
-    | _ -> assert false (* Type annotation must be `Map` type, enforced by the parser *) 
-    in
     (* Don't supply the guard when normalizing subexpressions, 
        because we need to generate oracle variables in initial step 
        if there are unguarded pres *)
-    let nexpr1, gids2, _ = normalize_expr info node_id map expr1 in 
-    let nexpr2, gids3, _ = normalize_expr info node_id map expr2 in 
-    let nexpr3, gids4, _ = normalize_expr info node_id map expr3 in 
+    let nexpr1, gids1, _ = normalize_expr info node_id map expr1 in 
+    let nexpr2, gids2, _ = normalize_expr info node_id map expr2 in 
+    let nexpr3, gids3, _ = normalize_expr info node_id map expr3 in 
     (* Hacky: to generate correct user-facing warnings, we call normalize_expr 
        while supplying the guard, but ignore all other outputs *)
-    let _, _, warnings2 = normalize_expr ?guard info node_id map expr1 in 
-    let _, _, warnings3 = normalize_expr ?guard info node_id map expr2 in 
-    let _, _, warnings4 = normalize_expr ?guard info node_id map expr3 in 
+    let _, _, warnings1 = normalize_expr ?guard info node_id map expr1 in 
+    let _, _, warnings2 = normalize_expr ?guard info node_id map expr2 in 
+    let _, _, warnings3 = normalize_expr ?guard info node_id map expr3 in 
     i := !i + 1; 
     let prefix = HString.mk_hstring (string_of_int !i) in 
     let name1 = HString.concat2 prefix (HString.mk_hstring "_map_update") in 
@@ -2318,30 +2306,23 @@ and normalize_expr ?guard info (node_id : NI.t option) map =
     (* Use base types *)
     let kt = Chk.expand_type_syn_reftype_history_subrange info.context kt |> Result.get_ok in
     let vt = Chk.expand_type_syn_reftype_history_subrange info.context vt |> Result.get_ok in
-    let gids5 = { (empty ()) with   
+    let gids4 = { (empty ()) with   
       map_element_updates = [ name1, nexpr1, nexpr2, nexpr3, name2, kt, vt ]; 
       locals = StringMap.add name2 kt (StringMap.singleton name1 (A.Map (pos, kt, vt)));
     } in 
     let nexpr = A.Ident (pos, name1) in 
-    let gids = List.fold_left union (empty ()) [gids1; gids2; gids3; gids4; gids5] in 
-    nexpr, gids, warnings1 @ warnings2 @ warnings3 @ warnings4
+    let gids = List.fold_left union (empty ()) [gids1; gids2; gids3; gids4] in 
+    nexpr, gids, warnings1 @ warnings2 @ warnings3 
     | StructUpdate (pos, expr1, [A.SetIndex (_, expr2)], None) as expr ->
-    let gids1, warnings1 = match AH.find_type_annotation expr1 with 
-    | Some ty -> 
-      let gids, warnings =  mk_fresh_refinement_type_constraint Local info map pos node_id expr2 ty in
-      let gids', warnings' = mk_fresh_subrange_constraint ~force_prop:true Local info map pos node_id expr2 ty in  
-      union gids gids', warnings @ warnings'
-    | None -> empty (), [] 
-    in
     (* Don't supply the guard when normalizing subexpressions, 
        because we need to generate oracle variables in initial step 
        if there are unguarded pres *)
-    let nexpr1, gids2, _ = normalize_expr info node_id map expr1 in 
-    let nexpr2, gids3, _ = normalize_expr info node_id map expr2 in 
+    let nexpr1, gids1, _ = normalize_expr info node_id map expr1 in 
+    let nexpr2, gids2, _ = normalize_expr info node_id map expr2 in 
     (* Hacky: to generate correct user-facing warnings, we call normalize_expr 
        while supplying the guard, but ignore all other outputs *)
-    let _, _, warnings2 = normalize_expr ?guard info node_id map expr1 in 
-    let _, _, warnings3 = normalize_expr ?guard info node_id map expr2 in 
+    let _, _, warnings1 = normalize_expr ?guard info node_id map expr1 in 
+    let _, _, warnings2 = normalize_expr ?guard info node_id map expr2 in 
     i := !i + 1; 
     let prefix = HString.mk_hstring (string_of_int !i) in 
     let name1 = HString.concat2 prefix (HString.mk_hstring "_set_update") in 
@@ -2352,13 +2333,13 @@ and normalize_expr ?guard info (node_id : NI.t option) map =
     in 
     (* Use base types *)
     let ty = Chk.expand_type_syn_reftype_history_subrange info.context ty |> Result.get_ok in
-    let gids4 = { (empty ()) with   
+    let gids3 = { (empty ()) with   
       set_insertions = [ name1, nexpr1, nexpr2, name2, ty ]; 
       locals = StringMap.add name2 ty (StringMap.singleton name1 (A.Set (pos, ty)));
     } in 
     let nexpr = A.Ident (pos, name1) in 
-    let gids = List.fold_left union (empty ()) [gids1; gids2; gids3; gids4] in 
-    nexpr, gids, warnings1 @ warnings2 @ warnings3
+    let gids = List.fold_left union (empty ()) [gids1; gids2; gids3] in 
+    nexpr, gids, warnings1 @ warnings2 
 
   | RecordProject (pos, expr, i) ->
     let nexpr, gids, warnings = normalize_expr ?guard info node_id map expr in

src/lustre/lustreParser.mly

@@ -960,38 +960,38 @@ pexpr(Q):
   (* An array constructor (not quantified) *)
   | e1 = pexpr(Q); CARET; e2 = expr { A.ArrayConstr (mk_pos $startpos, e1, e2) }
 
+  (* Empty map *)
+  | MAP; LSQBRACKET; RSQBRACKET;
+    ta = map_type_annotation
+  { A.EmptyMap (mk_pos $startpos, Some ta) }
+
   (* Map literals *)
   | MAP LSQBRACKET 
-    updates = separated_list(SEMICOLON, assign); 
+    updates = separated_nonempty_list(SEMICOLON, assign); 
     RSQBRACKET 
-    ta = option(map_type_annotation)
   {
-    match ta, updates with 
-    | None, [] -> 
-      let pos = mk_pos $startpos in 
-      fail_at_position pos "Empty map must have a type annotation"
-    | ta, updates -> 
-      List.fold_left (fun acc (e2, e3) -> 
-        A.StructUpdate (mk_pos $startpos, acc, [A.MapIndex (mk_pos $startpos, e2)], Some e3) 
-      )  (A.EmptyMap (mk_pos $startpos, ta)) updates 
+    List.fold_left (fun acc (e2, e3) -> 
+      A.StructUpdate (mk_pos $startpos, acc, [A.MapIndex (mk_pos $startpos, e2)], Some e3) 
+    )  (A.EmptyMap (mk_pos $startpos, None)) updates 
   }
 
+  (* Empty set *)
+  | LCURLYBRACKET 
+    RCURLYBRACKET 
+    ta = type_annotation; 
+  { A.EmptySet (mk_pos $startpos, Some ta) }
+
   (* Set literals *)
   | LCURLYBRACKET 
-    elements = separated_list(COMMA, expr);
+    elements = separated_nonempty_list(COMMA, expr);
     RCURLYBRACKET 
-    ta = option(type_annotation); 
   {
-    match ta, elements with 
-    | None, [] -> 
-      let pos = mk_pos $startpos in 
-      fail_at_position pos "Empty set must have a type annotation"
-    | ta, elements -> 
-      List.fold_left (fun acc e -> 
-        A.StructUpdate (mk_pos $startpos, acc, [A.SetIndex (mk_pos $startpos, e)], None) 
-      ) (A.EmptySet (mk_pos $startpos, ta)) elements
+    List.fold_left (fun acc e -> 
+      A.StructUpdate (mk_pos $startpos, acc, [A.SetIndex (mk_pos $startpos, e)], None) 
+    ) (A.EmptySet (mk_pos $startpos, None)) elements
   }
 
+  (* Map element updates *)
   | e1 = pexpr(Q); 
     LSQBRACKET; 
     updates = separated_nonempty_list(SEMICOLON, assign); 

tests/ounit/lustre/lustreTypeChecker/bad_ty_annot.lus

@@ -1,5 +1,5 @@
 node N(x: int) returns (y: set<int>);
 let
-  y = { x }@<bool>;
+  y = { }@<bool>;
   check x in y;
 tel

tests/regression/falsifiable/enforce_ty_annots.lus

@@ -1,6 +1,6 @@
 node N () returns (out: map<int, int>) 
 let
-  out = map[1 := 2; 3 := 4]@<int, int>;
+  out = map[1 := 2; 3 := 4];
   check 1 in out;
   check 3 in out;
   check forall (i: int) i <> 1 and i <> 3 => not (i in out);

tests/regression/success/empty_map_update_test.lus

@@ -6,8 +6,8 @@ type R = struct { x: int; y: int };
 
 node N() returns (o: S; o2: set<[int, int]>; o3: set<[[int, int], int]>; o4: set<[int, int]>; o6: set<R>) 
 let
-    o = { 3, 4 }@<int>;
-    o2 ={ '(3, 4), '(6, 7) }@<[int, int]>;
+    o = { 3, 4 };
+    o2 ={ '(3, 4), '(6, 7) };
 
     check 3 in o; 
     check 4 in o; 
@@ -16,9 +16,9 @@ let
     check forall (i: int) i <> 3 and i <> 4 => not (i in o);
     check forall (i: [int, int]) i <> '(3, 4) and i <> '(6, 7) => not (i in o2);
 
-    o3 = { '('(3, 4), 5), '('(6, 7), 8) }@<[[int, int], int]>; 
-    o4 = { '(3, 4), '(7, 8) }@<[int, int]>;
-    o6 = { R {x = 3; y = 4}, R {x = 5; y = 6} }@<R>;
+    o3 = { '('(3, 4), 5), '('(6, 7), 8) }; 
+    o4 = { '(3, 4), '(7, 8) };
+    o6 = { R {x = 3; y = 4}, R {x = 5; y = 6} };
 
     check '('(3, 4), 5) in o3;
     check '('(6, 7), 8) in o3;