CN: add an "inline" CN-statement.

It seems that, in various cases, it would be nice to have the type-checking at
a function call site simply include the semantics of the called function rather
than have to write out a specification for it that captures its semantics with
enough precision.

One use case (sketched here in tests/cn/cn_inline.c) is where a static inline
function is used in the computation of a constant. We don't want to have to
write out a specification of the function that explains exactly the arithmetic
it does, we just want the checking at the call site to reduce the computation
down to the constant.

The current version is designed to work by annotating the call site with this
information rather than annotating the function to be inlined at every call
site. This might be revisited.

Adjusting the parser to include the new statement required purging and
rebuilding the parser error-messages file. Apologies if anyone has manually
edited that file, if so, restore from history prior to this point.

backend/cn/check.ml

@@ -1469,6 +1469,8 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr)
                       {loc; msg = Unproven_constraint {constr = lc; info = (loc, None); ctxt; model; trace}}
                     )
                end
+            | M_CN_inline _nms ->
+               return ()
           end
      in
      let@ () = ListM.iterM aux cn_progs in

backend/cn/cnprog.ml

@@ -21,6 +21,7 @@ type cn_statement =
   | M_CN_unfold of Sym.t * IndexTerms.t list
   | M_CN_apply of Sym.t * IndexTerms.t list
   | M_CN_assert of LogicalConstraints.t
+  | M_CN_inline of Sym.t list
 
 
 
@@ -61,6 +62,8 @@ let rec subst substitution = function
           M_CN_apply (fsym, List.map (IT.subst substitution) args)
        | M_CN_assert lc ->
           M_CN_assert (LC.subst substitution lc)
+       | M_CN_inline nms ->
+          M_CN_inline nms
      in
      M_CN_statement (loc, stmt)
 
@@ -117,6 +120,8 @@ let dtree_of_cn_statement = function
      Dnode (pp_ctor "Apply", List.map IT.dtree args)
   | M_CN_assert lc ->
      Dnode (pp_ctor "Assert", [LC.dtree lc])
+  | M_CN_inline nms ->
+     Dnode (pp_ctor "Inline", List.map (fun nm -> Dleaf (Sym.pp nm)) nms)
 
 
 let rec dtree = function

backend/cn/compile.ml

@@ -1424,6 +1424,8 @@ let translate_cn_statement
          let@ args = ListM.mapM (ET.translate_cn_expr SymSet.empty env) args in
          let args = List.map IT.term_of_sterm args in
          return (M_CN_statement (loc, M_CN_apply (s, args)))
+      | CN_inline nms ->
+         return (M_CN_statement (loc, M_CN_inline nms))
     )
 
 

frontend/model/cabs_to_ail.lem

@@ -4500,6 +4500,14 @@ let desugar_cn_statement (CN_statement loc stmt_) =
      let l = Cn.ensure_not_c_variable l_resolved in
      E.mapM desugar_cn_expr args >>= fun args ->
      E.return (CN_apply l args)
+  | CN_inline nms ->
+     CN_inline <$> E.mapM (fun nm ->
+       E.resolve_ordinary_identifier loc nm >>= function
+         | Just (_, E.OReg_other nm_sym _ _) ->
+           E.return nm_sym
+         | None ->
+           E.fail loc (Errors.Desugar_CN (CNErr_unknown_c_identifier nm))
+         end) nms
   end >>= fun stmt_ ->
   E.return (CN_statement loc stmt_)
 

frontend/model/cn.lem

@@ -205,6 +205,7 @@ type cn_statement_ 'a 'ty =
   | CN_unfold of 'a * list (cn_expr 'a 'ty)
   | CN_assert_stmt of cn_assertion 'a 'ty
   | CN_apply of 'a * list (cn_expr 'a 'ty)
+  | CN_inline of (list 'a)
 
 type cn_statement 'a 'ty =
   CN_statement of Loc.t * cn_statement_ 'a 'ty

ocaml_frontend/cn_ocaml.ml

@@ -349,6 +349,8 @@ module MakePp (Conf: PP_CN) = struct
        Dnode (pp_ctor "[CN]assert", [dtree_of_cn_assertion assrt])
     | CN_apply (s, args) ->
        Dnode (pp_ctor "[CN]apply", Dleaf (Conf.pp_ident s) :: List.map dtree_of_cn_expr args)
+    | CN_inline nms ->
+       Dnode (pp_ctor "[CN]inline", List.map (fun nm -> Dleaf (Conf.pp_ident nm)) nms)
 
 end
 

parsers/c/c_parser.mly

@@ -2416,6 +2416,9 @@ cn_statement:
 | ASSERT LPAREN e=assert_expr RPAREN SEMICOLON
     { let loc = Cerb_location.(region ($startpos, $endpos) NoCursor) in 
       CN_statement (loc, CN_assert_stmt e) }
+| INLINE names= separated_list(COMMA, cn_variable) SEMICOLON
+    { let loc = Cerb_location.(region ($startpos, $endpos) NoCursor) in
+      CN_statement (loc, CN_inline names) }
 
 cn_toplevel_elem:
 | pred= cn_predicate