Prevent overlapping of parameters in def-fun in SMT-LIB

CHANGES.md

@@ -16,6 +16,11 @@ next
 
 - Add a logic detection mechanism (PR#211)
 
+- Reject overlapping/shadowing between parameters of the
+  same function definition in SMT-LIB, since the prescribed
+  semantics in that case are highly unusual and incorrect
+  wrt to the typed term generated by dolmen currently (PR#247)
+
 - Reject overlapping parallel let-bindings (PR#246)
 
 - Reject application of SMT-LIB2's distinct to less than 2

src/loop/typer.ml

@@ -188,7 +188,7 @@ let print_reason ?(already=false) fmt r =
       Format.pp_print_text
       "Therefore, the definition of the model corner case would take \
        priority and prevent defining a value for this constant."
-  | Bound (file, ast) ->
+  | Bound (file, ast, _) ->
     Format.fprintf fmt "was%a bound at %a"
       pp_already () Dolmen.Std.Loc.fmt_pos (Dolmen.Std.Loc.loc file ast.loc)
   | Inferred (file, ast) ->
@@ -303,6 +303,9 @@ let print_reserved fmt = function
 (* Hint printers *)
 (* ************************************************************************ *)
 
+let raw_hint msg _ =
+  Some (Format.dprintf "%a" Format.pp_print_text msg)
+
 let fo_hint _ =
   Some (
     Format.dprintf "%a" Format.pp_print_text
@@ -650,6 +653,21 @@ let overlapping_parallel_bindings =
       )
     ~name:"Overlapping Parallel Bindings" ()
 
+let overlapping_smt_fun_def_params =
+  Report.Error.mk ~code ~mnemonic:"overlapping-smt-fun-def-params"
+    ~message:(fun fmt (id, old) ->
+        Format.fprintf fmt
+          "Parameter %a %a@ as another parameter of the same function definition"
+          (pp_wrap Dolmen.Std.Id.print) id
+          (print_reason_opt ~already:true) (T.binding_reason old))
+    ~hints:[raw_hint "Shadowing between parameters in the same function definition \
+                      in SMT-LIB2 has extremely un-inuitive semantics, and lead to \
+                      partially specified functions. It definitely doesn't do what you \
+                      expect and such definitions are therefore strongly discouraged. \
+                      For more information, read \
+                      https://github.com/SMT-LIB/SMT-LIB-2/issues/36"]
+    ~name:"Overlapping Parameters in Function Definition" ()
+
 let unhandled_builtin =
   Report.Error.mk ~code:Code.bug ~mnemonic:"typer-unhandled-builtin"
     ~message:(fun fmt b ->
@@ -1226,11 +1244,26 @@ module Typer(State : State.S) = struct
     | Local { name; } when String.length name >= 1 && name.[0] = '_' -> true
     | _ -> false
 
-  let smtlib2_6_shadow_rules (input : input) =
+  let smtlib2_shadow_rules (input : input) =
     match input with
-    | `Logic { lang = Some Smtlib2 (`Latest | `V2_6 | `Poly); _ }
-    | `Response { lang = Some Smtlib2 (`Latest | `V2_6); _ }
-      -> true
+    | `Logic { lang = Some Smtlib2 version; _ } ->
+      begin match version with
+        | `Latest | `V2_6 | `V2_7 | `Poly -> true
+      end
+    | `Response { lang = Some Smtlib2 version; _ } ->
+      begin match version with
+        | `Latest | `V2_6 | `V2_7 -> true
+      end
+    | _ -> false
+
+  let bound_by_same_fun_definition binding1 binding2 =
+    let extract_def b =
+      match T.binding_reason b with
+      | Some Bound (_, _, Definition_parameter d) -> Some d
+      | _ -> None
+    in
+    match extract_def binding1, extract_def binding2 with
+    | Some d, Some d' when Dolmen.Std.Loc.eq d.loc d'.loc -> true
     | _ -> false
 
   let typing_logic input =
@@ -1247,8 +1280,13 @@ module Typer(State : State.S) = struct
     (* typer warnings that are actually errors given some languages spec *)
     | T.Shadowing (id, ((`Builtin `Term | `Not_found) as old), `Variable _)
     | T.Shadowing (id, ((`Constant _ | `Builtin _ | `Not_found) as old), `Constant _)
-      when smtlib2_6_shadow_rules input ->
+      when smtlib2_shadow_rules input ->
       error ~input ~loc st multiple_declarations (id, old)
+    (* shadowing between parameters of a function definition: this does not do
+       what anyone expects *)
+    | T.Shadowing (id, last, curr)
+      when smtlib2_shadow_rules input && bound_by_same_fun_definition last curr ->
+      error ~input ~loc st overlapping_smt_fun_def_params (id, last)
 
     (* unused variables *)
     | T.Unused_type_variable (kind, v) ->

src/loop/typer.mli

@@ -36,10 +36,11 @@ val bad_arith_expr : (Dolmen_type.Arith.Smtlib2.config * string) Report.Warning.
     specification (e.g. linear arithmetic), but are close enough that they
     should probably be accepted. *)
 
-
 val unknown_logic : string Report.Warning.t
 (** Unknown logic warning *)
 
+
+
 module Ext : sig
   (** Define typing extensions.
 

src/typecheck/core.ml

@@ -616,7 +616,7 @@ module Smtlib2 = struct
         Type.builtin_term (Base.term_app_left (module Type) env s T.map_app)
 
       | Type.Builtin Ast.Map_lambda ->
-        Type.builtin_term (fun _ast args ->
+        Type.builtin_term (fun ast args ->
             match split_map_lambda_args args with
             | Error () -> assert false (* TODO: error message *)
             | Ok (params, body) ->
@@ -625,7 +625,9 @@ module Smtlib2 = struct
                     match Type.parse_var_in_binding_pos env param_ast with
                     | `Ty _ -> assert false (* TODO: error message *)
                     | `Term (id, var) ->
-                      let env = Type.add_term_var env id var param_ast in
+                      (* using `Fun` as binder is a bit of over-approximation here,
+                         ideally we'd use a dedicate Map_fun binder *)
+                      let env = Type.add_term_var env (Binder (Fun, ast)) id var param_ast in
                       var :: params, env
                   ) ([], env) params
               in

src/typecheck/intf.ml

@@ -156,10 +156,17 @@ module type Formulas = sig
       therefore cannot/should not occur at some positions. This type tries and explain
       the reason for such restrictions. *)
 
+  type bound_context =
+    | Pattern of Dolmen.Std.Term.t
+    | Binder of Dolmen.Std.Term.binder * Dolmen.Std.Term.t
+    | Definition_parameter of Dolmen.Std.Statement.def
+    | Declaration_parameter of Dolmen.Std.Statement.decl (**)
+  (** Context for where bound variables are bound. *)
+
   type reason =
     | Builtin
     | Reserved of reservation * string
-    | Bound of Dolmen.Std.Loc.file * Dolmen.Std.Term.t
+    | Bound of Dolmen.Std.Loc.file * Dolmen.Std.Term.t * bound_context
     | Inferred of Dolmen.Std.Loc.file * Dolmen.Std.Term.t
     | Defined of Dolmen.Std.Loc.file * Dolmen.Std.Statement.def
     | Declared of Dolmen.Std.Loc.file * Dolmen.Std.Statement.decl
@@ -612,11 +619,11 @@ module type Formulas = sig
   (** Return the reason (if any) for the given typed symbol. *)
 
   val add_type_var :
-    env -> Dolmen.Std.Id.t -> ty_var -> Dolmen.Std.Term.t -> env
+    env -> bound_context -> Dolmen.Std.Id.t -> ty_var -> Dolmen.Std.Term.t -> env
   (** Add a local type variable to the env *)
 
   val add_term_var :
-    env -> Dolmen.Std.Id.t -> term_var -> Dolmen.Std.Term.t -> env
+    env -> bound_context -> Dolmen.Std.Id.t -> term_var -> Dolmen.Std.Term.t -> env
   (** Add a local term variable to the env *)
 
   val decl_ty_const :