diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 397fad3207992d67a177d9b5d0b132bb67e0fbf7..18d9d1cab1c9cf85ba664712c59e7b59b99bee85 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -815,16 +815,17 @@ module Base_checker = struct
| None ->
check_abort "Trying to use predicate %a as a term"
Printer.pp_logic_var lvi
- | Some typ ->
+ | Some rt ->
+ let ft = Logic_const.make_arrow_type li.l_profile rt in
if
not
- (Logic_utils.is_instance_of li.l_tparams t.term_type typ)
+ (Logic_utils.is_instance_of li.l_tparams t.term_type ft)
then
check_abort
"%a is declared with type %a. It cannot be used as \
a term of type %a"
Printer.pp_logic_var lvi
- Printer.pp_logic_type typ
+ Printer.pp_logic_type ft
Printer.pp_logic_type t.term_type)
with Not_found ->
check_abort
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 28623b64f5e98ada8da7101e9d014efaac3fac36..b7b632bb888340cb83f3e25e8f57bf00a17f316b 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -226,6 +226,11 @@ let transform_element f t = set_conversion (plain_or_set f t) t
let is_plain_type ty = not (is_set_type ty)
+let make_arrow_type args rt =
+ match args with
+ | [] -> rt
+ | _ -> Larrow(List.map (fun x -> x.lv_type) args, rt)
+
let rec is_boolean_type = function
| Ltype ({ lt_name = s }, []) when s = Utf8_logic.boolean -> true
| Ltype (tdef,_) as ty when is_unrollable_ltdef tdef ->
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index db448d2e6dee8acee4a803d9e5d82c6fc2bad78a..a18c91e6b7ef355de494c6f71b8fff0350306ebd 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -283,6 +283,13 @@ val transform_element: (logic_type -> logic_type) -> logic_type -> logic_type
@modify 18.0-Argon expands the logic type definition if necessary. *)
val is_plain_type: logic_type -> bool
+(** [make_arrow_type args rt] returns a [rt] if [args] is empty or the
+ corresponding [Larrow] type.
+
+ @since Frama-C+dev
+*)
+val make_arrow_type: logic_var list -> logic_type -> logic_type
+
(** @return true if the argument is the boolean type.
@modify 18.0-Argon expands the logic type definition if necessary. *)
val is_boolean_type: logic_type -> bool
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d7c956b7eb74223579b3007baff79a8f6db062fa..8950bee942e7e3b170c56269a8aa0383a916a3c3 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -2039,7 +2039,7 @@ struct
| _,typ ->
{ term with
term_node = Tlambda(quants, term);
- term_type = Larrow(List.map (fun x -> x.lv_type) quants,typ) }
+ term_type = make_arrow_type quants typ }
in
let rec aux known_vars kont term =
match term.term_node with
@@ -2948,7 +2948,7 @@ struct
| _ -> [],tdef
in
var.l_type <- Some tdef.term_type;
- var.l_var_info.lv_type <- tdef.term_type;
+ var.l_var_info.lv_type <- make_arrow_type args tdef.term_type;
var.l_profile <- args;
var.l_body <- LBterm tdef;
let env = Lenv.add_logic_info ident var env in
@@ -3455,10 +3455,8 @@ struct
in
let var = Cil_const.make_logic_info_local x in
var.l_profile <- args;
- var.l_var_info.lv_type <-
- (match typ with
- None -> Ctype (Cil.voidType)
- | Some t -> t);
+ let rt = Option.value typ ~default:(Ctype Cil.voidType) in
+ var.l_var_info.lv_type <- make_arrow_type args rt;
var.l_type <- typ;
var.l_body <- tdef;
let env = Lenv.add_logic_info x var env in
@@ -4003,13 +4001,8 @@ struct
- Polymorphism is not reflected on the lvar level.
- However, such lvar should rarely if at all be seen under a Tvar.
*)
- (match p,t with
- _,None -> ()
- | [], Some t ->
- info.l_var_info.lv_type <- t
- | _,Some t ->
- let typ = Larrow (List.map (fun x -> x.lv_type) p,t) in
- info.l_var_info.lv_type <- typ);
+ let rt = Option.value t ~default:(Ctype Cil.voidType) in
+ info.l_var_info.lv_type <- make_arrow_type p rt;
info.l_tparams <- poly;
info.l_profile <- p;
info.l_type <- t;
diff --git a/tests/spec/local_lambda.i b/tests/spec/local_lambda.i
new file mode 100644
index 0000000000000000000000000000000000000000..336c172135490c239a5e74352775085fefa6b908
--- /dev/null
+++ b/tests/spec/local_lambda.i
@@ -0,0 +1,9 @@
+/*@ logic integer id(integer x) = x; */
+
+/*@ lemma test1: 55 == \sum(1,10,id); */
+
+/*@ lemma test2: 5 == \let x = (\lambda integer y; y); x(5); */
+
+/*@ lemma test3: 55 == \sum(1,10,\lambda integer y; y); */
+
+/*@ lemma test4: 55 == \let x = (\lambda integer y; y); \sum(1,10,x); */
diff --git a/tests/spec/oracle/local_lambda.res.oracle b/tests/spec/oracle/local_lambda.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d77e1eb63c2dc3e33ef10b27bdf4e1c6c9d60e0c
--- /dev/null
+++ b/tests/spec/oracle/local_lambda.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/spec/local_lambda.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ logic ℤ id(ℤ x) = x;
+ */
+/*@ lemma test1: 55 ≡ \sum(1, 10, id);
+ */
+/*@ lemma test2: 5 ≡ (\let x = \lambda ℤ y; y; x(5));
+ */
+/*@ lemma test3: 55 ≡ \sum(1, 10, \lambda ℤ y; y);
+ */
+/*@ lemma test4: 55 ≡ (\let x = \lambda ℤ y; y; \sum(1, 10, x));
+ */
+
diff --git a/tests/syntax/oracle/reorder.res.oracle b/tests/syntax/oracle/reorder.res.oracle
index 446708bfa1ce0a04272dfc3ceb4dca721cb7b986..44b5d5c8aa5f0c844cdca1359850b5a5d45d20b7 100644
--- a/tests/syntax/oracle/reorder.res.oracle
+++ b/tests/syntax/oracle/reorder.res.oracle
@@ -30,10 +30,10 @@ void g(void);
/*@ logic ℤ l= 1;
*/
int x;
-/*@ logic ℤ k= l;
- */
/*@ logic ℤ j= l;
*/
+/*@ logic ℤ k= l;
+ */
/*@ logic ℤ i= j + k;
*/
/*@ ensures i ≡ i; */