CN: add struct literals to frontend

Currently the syntax is `struct tag { f1 : e1 , ... , fn : en }`,
which is not quite what C has but avoids cast-like syntax.

backend/cn/compile.ml

@@ -201,6 +201,8 @@ let rec free_in_expr (CNExpr (_loc, expr_)) =
      free_in_expr e
   | CNExpr_record members ->
      free_in_exprs (List.map snd members)
+  | CNExpr_struct (_tag, members) ->
+     free_in_exprs (List.map snd members)
   | CNExpr_memberupdates (e, updates) ->
      free_in_exprs (e :: List.map snd updates)
   | CNExpr_arrayindexupdates (e, updates) ->
@@ -712,6 +714,9 @@ module EffectfulTranslation = struct
            let@ members = ListM.mapsndM self members in
            let bts = List.map_snd IT.bt members in
            return (IT (IT.Record members, SBT.Record bts, loc))
+        | CNExpr_struct (tag, members) ->
+           let@ members = ListM.mapsndM self members in
+           return (IT (IT.Struct (tag, members), SBT.Struct tag, loc))
         | CNExpr_memberupdates (e, updates) ->
            let@ e = self e in
            let bt = IT.bt e in

frontend/model/cabs_to_ail.lem

@@ -4194,6 +4194,15 @@ let rec desugar_cn_expr (CNExpr loc expr_) =
                         <*> (E.return ident_membr)
     | CNExpr_record members ->
       CNExpr_record <$> sort_record_members desugar_cn_expr members
+    | CNExpr_struct tag members ->
+      (* copying from CNExpr_membershift case *)
+      E.resolve_extraordinary_identifier tag E.Namespace_tag >>= function
+          | Just (_, (tag_sym, _)) ->
+             CNExpr_struct <$> (E.return tag_sym)
+                           <*> sort_record_members desugar_cn_expr members
+          | Nothing ->
+              E.fail loc (Errors.Desugar_CN CNErr_invalid_tag)
+      end
     | CNExpr_memberupdates e updates ->
         CNExpr_memberupdates <$> desugar_cn_expr e
                              <*> unique_record_members desugar_cn_expr updates

frontend/model/cn.lem

@@ -93,6 +93,7 @@ type cn_expr_ 'a 'ty =
   | CNExpr_list of list (cn_expr 'a 'ty)
   | CNExpr_memberof of cn_expr 'a 'ty * Symbol.identifier
   | CNExpr_record of list (Symbol.identifier * cn_expr 'a 'ty)
+  | CNExpr_struct of 'a * list (Symbol.identifier * cn_expr 'a 'ty)
   | CNExpr_memberupdates of cn_expr 'a 'ty * list (Symbol.identifier * cn_expr 'a 'ty)
   | CNExpr_arrayindexupdates of cn_expr 'a 'ty * list (cn_expr 'a 'ty * cn_expr 'a 'ty)
   | CNExpr_binop of cn_binop * cn_expr 'a 'ty * cn_expr 'a 'ty

ocaml_frontend/cn_ocaml.ml

@@ -160,6 +160,16 @@ module MakePp (Conf: PP_CN) = struct
                 ])
              ) members
            )
+      | CNExpr_struct (tag, members) ->
+         Dnode (pp_ctor "CNExpr_struct", 
+             Dleaf (Conf.pp_ident tag) ::
+             List.map (fun (id, e) -> 
+                Dnode (pp_ctor "member", [
+                  Dleaf (pp_identifier id);
+                  dtree_of_cn_expr e
+                ])
+             ) members
+           )
       | CNExpr_memberupdates (e, updates) ->
          let updates = 
            List.map (fun (z,v) -> 

parsers/c/c_parser.mly

@@ -1881,6 +1881,9 @@ prim_expr:
 | LBRACE a=expr RBRACE PERCENT l=NAME VARIABLE
     { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos, $endpos) (PointCursor $startpos($4)))
                                , CNExpr_at_env (a, l))) }
+| STRUCT tag=cn_variable LBRACE members=record_def RBRACE
+    { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos,$endpos) NoCursor)
+                               , CNExpr_struct (tag, members))) }
 | LBRACE members=record_def RBRACE
     { Cerb_frontend.Cn.(CNExpr ( Cerb_location.(region ($startpos,$endpos) NoCursor)
                                , CNExpr_record members)) }
@@ -2505,4 +2508,4 @@ cn_toplevel:
     { elems }
 
 
-(* END CN *)
+(* END CN *)