CN: Add the ability to refer to resources by name

backend/cn/lib/compile.ml

@@ -1385,7 +1385,7 @@ let translate_cn_clause env clause =
   let rec translate_cn_clause_aux env st acc clause =
     let module LAT = LogicalArgumentTypes in
     match clause with
-    | CN_letResource (res_loc, sym, the_res, cl) ->
+    | CN_letResource (res_loc, sym, the_res, _opt_sym, cl) ->
       let@ (pt_ret, oa_bt), lcs, pointee_vals =
         handle st (ET.translate_cn_let_resource env (res_loc, sym, the_res))
       in
@@ -1471,7 +1471,7 @@ let translate_cn_predicate env (def : cn_predicate) =
 let rec make_lrt_generic env st =
   let open LocalState in
   function
-  | CN_cletResource (loc, name, resource) :: ensures ->
+  | CN_cletResource (loc, name, resource, _opt_name) :: ensures ->
     let@ (pt_ret, oa_bt), lcs, pointee_values =
       handle st (ET.translate_cn_let_resource env (loc, name, resource))
     in

backend/cn/lib/core_to_mucore.ml

@@ -883,7 +883,7 @@ let rec arguments_of_at f_i = function
 
 let make_largs f_i =
   let rec aux env st = function
-    | Cn.CN_cletResource (loc, name, resource) :: conditions ->
+    | Cn.CN_cletResource (loc, name, resource, _opt_name) :: conditions ->
       let@ (pt_ret, oa_bt), lcs, pointee_values =
         C.LocalState.handle st (C.ET.translate_cn_let_resource env (loc, name, resource))
       in
@@ -1070,11 +1070,18 @@ let desugar_access d_st global_types (loc, id) =
 
 
 let desugar_cond d_st = function
-  | Cn.CN_cletResource (loc, id, res) ->
+  | Cn.CN_cletResource (loc, id, res, opt_id) ->
     debug 6 (lazy (typ (string "desugaring a let-resource at") (Locations.pp loc)));
     let@ res = do_ail_desugar_rdonly d_st (Desugar.cn_resource res) in
     let@ sym, d_st = register_new_cn_local id d_st in
-    return (Cn.CN_cletResource (loc, sym, res), d_st)
+    let@ opt_sym, d_st =
+      match opt_id with
+      | Some id ->
+        let@ sym, d_st = register_new_cn_local id d_st in
+        return (Some sym, d_st)
+      | None -> return (None, d_st)
+    in
+    return (Cn.CN_cletResource (loc, sym, res, opt_sym), d_st)
   | Cn.CN_cletExpr (loc, id, expr) ->
     debug 6 (lazy (typ (string "desugaring a let-expr at") (Locations.pp loc)));
     let@ expr = do_ail_desugar_rdonly d_st (Desugar.cn_expr expr) in

backend/cn/lib/pp_mucore_coq.ml

@@ -1681,10 +1681,10 @@ let pp_cn_assertion ppfa ppfty = function
 
 
 let pp_cn_condition ppfa ppfty = function
-  | CF.Cn.CN_cletResource (loc, sym, res) ->
+  | CF.Cn.CN_cletResource (loc, sym, res, opt_sym) ->
     pp_constructor2
       "CN_cletResource"
-      [ pp_location loc; ppfa sym; pp_cn_resource ppfa ppfty res ]
+      [ pp_location loc; ppfa sym; pp_cn_resource ppfa ppfty res; pp_option ppfa opt_sym ]
   | CN_cletExpr (loc, sym, ex) ->
     pp_constructor2 "CN_cletExpr" [ pp_location loc; ppfa sym; pp_cn_expr ppfa ppfty ex ]
   | CN_cconstr (loc, assertion) ->

frontend/model/cabs.lem

@@ -55,7 +55,7 @@ type cabs_expression_ =
   | CabsEgeneric of cabs_expression * list cabs_generic_association
   (* §6.5.2 Postfix operators, Syntax *)
   | CabsEsubscript of cabs_expression * cabs_expression
-  | CabsEcall of cabs_expression * list cabs_expression
+  | CabsEcall of cabs_expression * list cabs_expression * Annot.attributes
   | CabsEmemberof of cabs_expression * Symbol.identifier
   | CabsEmemberofptr of cabs_expression * Symbol.identifier
   | CabsEpostincr of cabs_expression

frontend/model/cabs_to_ail.lem

@@ -2281,7 +2281,7 @@ STD_ "§6.5.2.1#2, sentence 2" $
                       <*> E.return (Arithmetic Add)
                       <*> desugar_expression e2)
         )
-    | CabsEcall e es ->
+    | CabsEcall e es _annots (* FIXME *) ->
         (* TODO: STD check + annot *)
         AilEcall <$> desugar_expression e <*> E.mapM desugar_expression es
     | CabsEmemberof e ident ->
@@ -4379,15 +4379,19 @@ let desugar_cn_assertion a =
       E.return (CN_assert_qexp sym bTy e1 e2)
   end
 
-
+let desugar_maybe_cn_ident = function
+  | Just ident -> Just <$> (E.register_cn_ident CN_vars ident)
+  | Nothing -> E.return Nothing
+end
 
 let rec desugar_cn_clause_aux clause =
   match clause with
-    | CN_letResource loc ident res c ->
+    | CN_letResource loc ident res opt_name c ->
         desugar_cn_resource res              >>= fun res' ->
         E.register_cn_ident CN_vars ident >>= fun sym  ->
+        desugar_maybe_cn_ident opt_name >>= fun opt_sym  ->
         desugar_cn_clause_aux c                  >>= fun c'   ->
-        E.return (CN_letResource loc sym res' c')
+        E.return (CN_letResource loc sym res' opt_sym c')
     | CN_letExpr loc ident e c ->
         desugar_cn_expr e                    >>= fun e'  ->
         E.register_cn_ident CN_vars ident >>= fun sym ->
@@ -4476,10 +4480,11 @@ let desugar_and_register_cn_function func =
 (* adapting desugar_cn_clause *)
 let desugar_cn_condition condition =
   match condition with
-  | CN_cletResource loc ident res ->
+  | CN_cletResource loc ident res opt_ident ->
      desugar_cn_resource res >>= fun res' ->
      E.register_cn_ident CN_vars ident >>= fun sym ->
-     E.return (CN_cletResource loc sym res')
+     desugar_maybe_cn_ident opt_ident >>= fun opt_sym ->
+     E.return (CN_cletResource loc sym res' opt_sym)
   | CN_cletExpr loc ident e ->
      desugar_cn_expr e >>= fun e' ->
      E.register_cn_ident CN_vars ident >>= fun sym ->

frontend/model/cn.lem

@@ -147,7 +147,7 @@ type cn_assertion 'a 'ty =
 
 
 type cn_clause 'a 'ty =
-  | CN_letResource of Loc.t * 'a * cn_resource 'a 'ty * cn_clause 'a 'ty
+  | CN_letResource of Loc.t * 'a * cn_resource 'a 'ty * maybe 'a * cn_clause 'a 'ty
   | CN_letExpr of Loc.t * 'a * cn_expr 'a 'ty * cn_clause 'a 'ty
   | CN_assert of Loc.t * cn_assertion 'a 'ty * cn_clause 'a 'ty
   | CN_return of Loc.t * cn_expr 'a 'ty
@@ -167,7 +167,7 @@ type cn_function 'a 'ty = <|
 |>
 
 type cn_condition 'a 'ty =
-  | CN_cletResource of Loc.t * 'a * cn_resource 'a 'ty
+  | CN_cletResource of Loc.t * 'a * cn_resource 'a 'ty * maybe 'a
   | CN_cletExpr of Loc.t * 'a * cn_expr 'a 'ty
   | CN_cconstr of Loc.t * cn_assertion 'a 'ty
 

ocaml_frontend/cn_ocaml.ml

@@ -297,11 +297,14 @@ module MakePp (Conf: PP_CN) = struct
               , [dtree_of_cn_expr e1; dtree_of_cn_expr e2])
 
 
+  let dtree_of_opt_ident = function
+    | None -> []
+    | Some name -> [ Dnode (!^"As", [Dleaf (P.squotes (Conf.pp_ident name))]) ]
 
   let rec dtree_of_cn_clause = function
-    | CN_letResource (_, ident, res, c) ->
+    | CN_letResource (_, ident, res, opt_ident, c) ->
         Dnode ( pp_stmt_ctor "CN_letResource" ^^^ P.squotes (Conf.pp_ident ident)
-              , [dtree_of_cn_resource res; dtree_of_cn_clause c])
+              , (dtree_of_cn_resource res) :: dtree_of_opt_ident opt_ident @ [ dtree_of_cn_clause c ])
     | CN_letExpr (_, ident, e, c) ->
         Dnode ( pp_stmt_ctor "CN_letExpr" ^^^ P.squotes (Conf.pp_ident ident)
               , [dtree_of_cn_expr e; dtree_of_cn_clause c])
@@ -312,9 +315,9 @@ module MakePp (Conf: PP_CN) = struct
 
   (* copied and adjusted from dtree_of_cn_clause *)
   let dtree_of_cn_condition = function
-    | CN_cletResource (_, ident, res) ->
+    | CN_cletResource (_, ident, res, opt_ident) ->
         Dnode ( pp_stmt_ctor "CN_letResource" ^^^ P.squotes (Conf.pp_ident ident)
-              , [dtree_of_cn_resource res])
+              , dtree_of_opt_ident opt_ident @ [dtree_of_cn_resource res])
     | CN_cletExpr (_, ident, e) ->
         Dnode ( pp_stmt_ctor "CN_letExpr" ^^^ P.squotes (Conf.pp_ident ident)
               , [dtree_of_cn_expr e])

ocaml_frontend/pprinters/pp_cabs.ml

@@ -191,7 +191,7 @@ let rec dtree_of_cabs_expression (CabsExpression (loc, expr)) =
               , let d_e1 = dtree_of_cabs_expression e1 in
                 let d_e2 = dtree_of_cabs_expression e2 in
                [ d_e1; d_e2 ] )
-    | CabsEcall (e, es) ->
+    | CabsEcall (e, es, _attrs (* FIXME *)) ->
         Dnode ( pp_stmt_ctor "CabsEcall" ^^^ d_loc
               , let d_e  = dtree_of_cabs_expression e in
                 let d_es = dtree_of_list dtree_of_cabs_expression es in

parsers/c/c_parser.mly

@@ -85,6 +85,10 @@ let magic_to_opt_attrs = function
   | [] -> None
   | magic -> Some (magic_to_attrs magic)
 
+let opt_magic_to_attrs = function
+  | None -> Annot.Attrs []
+  | Some magic -> magic_to_attrs [magic]
+
 (* use this to show a warning when a NON-STD 'extra' semicolon was parsed *)
 let warn_extra_semicolon pos ctx =
   if not (Cerb_global.isPermissive ()) then
@@ -153,7 +157,7 @@ type asm_qualifier =
 %token CN_LET CN_TAKE CN_OWNED CN_BLOCK CN_EACH CN_LIFT_FUNCTION CN_FUNCTION CN_LEMMA CN_PREDICATE
 %token CN_DATATYPE CN_TYPE_SYNONYM CN_SPEC CN_ARRAY_SHIFT CN_MEMBER_SHIFT
 %token CN_UNCHANGED CN_WILD CN_MATCH
-%token CN_GOOD CN_NULL CN_TRUE CN_FALSE CN_IMPLIES CN_TO_BYTES CN_FROM_BYTES
+%token CN_GOOD CN_NULL CN_TRUE CN_FALSE CN_IMPLIES CN_TO_BYTES CN_FROM_BYTES CN_AS
 %token <string * [`U|`I] * int> CN_CONSTANT
 
 %token EOF
@@ -535,9 +539,9 @@ postfix_expression:
 | expr1= postfix_expression LBRACK expr2= expression RBRACK
     { CabsExpression ( region ($startpos, $endpos) noCursor
                      , CabsEsubscript (expr1, expr2) ) }
-| expr= postfix_expression LPAREN exprs_opt= argument_expression_list? RPAREN
+| expr= postfix_expression LPAREN exprs_opt= argument_expression_list? opt_magic=option(CERB_MAGIC) RPAREN
     { CabsExpression ( region ($startpos, $endpos) noCursor
-                     , CabsEcall (expr, opt_to_rev_list exprs_opt) ) }
+                     , CabsEcall (expr, opt_to_rev_list exprs_opt, opt_magic_to_attrs opt_magic) ) }
 | expr= postfix_expression DOT i= general_identifier
     { CabsExpression ( region ($startpos, $endpos) (pointCursor $startpos($2))
                      , CabsEmemberof (expr, i) ) }
@@ -1405,35 +1409,33 @@ selection_statement:
 
 (* FIXME magic comments should be singletons, not a list *)
 magic_comment_list:
-| xs= magic_comment_list magic= CERB_MAGIC
-    { magic :: xs }
-|
-    { [] }
+| xs= list(CERB_MAGIC)
+    { xs }
 
 (* §6.8.5 Iteration statements *)
 iteration_statement:
 | WHILE LPAREN expr= expression RPAREN magic= magic_comment_list stmt= scoped(statement)
     {
       CabsStatement
         ( region ($startpos, $endpos) noCursor
-        , magic_to_attrs (List.rev magic)
+        , magic_to_attrs magic
         , CabsSwhile (expr, stmt) ) }
 | DO magic= magic_comment_list stmt= scoped(statement) WHILE LPAREN expr= expression RPAREN SEMICOLON
     { CabsStatement
         ( region ($startpos, $endpos) noCursor
-        , magic_to_attrs (List.rev magic)
+        , magic_to_attrs magic
         , CabsSdo (expr, stmt) ) }
 | FOR LPAREN expr1_opt= expression? SEMICOLON expr2_opt= expression? SEMICOLON
   expr3_opt= expression? RPAREN magic= magic_comment_list stmt= scoped(statement)
     { CabsStatement
         ( region ($startpos, $endpos) noCursor
-        , magic_to_attrs (List.rev magic)
+        , magic_to_attrs magic
         , CabsSfor (Option.map (fun x -> FC_expr x) expr1_opt, expr2_opt,expr3_opt, stmt) ) }
 | FOR LPAREN xs_decl= declaration expr2_opt= expression? SEMICOLON
   expr3_opt= expression? RPAREN magic= magic_comment_list stmt= scoped(statement)
     { CabsStatement
         ( region ($startpos, $endpos) noCursor
-        , magic_to_attrs(List.rev magic)
+        , magic_to_attrs magic
         , CabsSfor (Some (FC_decl (region $loc(xs_decl) noCursor, xs_decl)), expr2_opt, expr3_opt, stmt) ) }
 ;
 
@@ -1579,7 +1581,7 @@ function_definition:
     { if has_semi then warn_extra_semicolon $startpos(has_semi) AFTER_FUNCTION;
       let loc = region ($startpos, $endpos) noCursor in
       let (attr_opt, specifs, decltor, ctxt) = specifs_decltor_ctxt in
-      let magic_opt = magic_to_opt_attrs (List.rev magic) in
+      let magic_opt = magic_to_opt_attrs magic in
       LF.restore_context ctxt;
       LF.create_function_definition loc attr_opt magic_opt specifs decltor stmt rev_decl_opt }
 ;
@@ -2334,9 +2336,9 @@ cn_option_func_body:
     { None }
 
 clause:
-| CN_TAKE str= cn_variable EQ res= resource SEMICOLON c= clause
+| CN_TAKE str= cn_variable EQ res= resource as_name=option(preceded(CN_AS, cn_variable)) SEMICOLON c= clause
     { let loc = point $startpos(str) in
-      Cerb_frontend.Cn.CN_letResource (loc, str, res, c) }
+      Cerb_frontend.Cn.CN_letResource (loc, str, res, as_name, c) }
 | CN_LET str= cn_variable EQ e= expr SEMICOLON c= clause
     { let loc = point $startpos(str) in
       Cerb_frontend.Cn.CN_letExpr (loc, str, e, c) }
@@ -2395,9 +2397,9 @@ ctype:
 
 /* copying 'clause' and adjusting */
 condition:
-| CN_TAKE str= cn_variable EQ res= resource SEMICOLON
+| CN_TAKE str= cn_variable EQ res= resource as_name=option(preceded(CN_AS,cn_variable)) SEMICOLON
     { let loc = point $startpos(str) in
-      Cerb_frontend.Cn.CN_cletResource (loc, str, res) }
+      Cerb_frontend.Cn.CN_cletResource (loc, str, res, as_name) }
 | CN_LET str= cn_variable EQ e= expr SEMICOLON
     { let loc = point $startpos(str) in
       Cerb_frontend.Cn.CN_cletExpr (loc, str, e) }