Ajout du parsing de type de fonction polymorph.

Src/COLIBRI/simplex_ocaml/dolmen/src/loop/typer.ml

@@ -163,6 +163,7 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
     | None -> Format.fprintf fmt "<location missing>"
 
   let report_warning (T.Warning (_env, _fragment, warn)) =
+    let aux: type a. a T.warn -> _ = fun warn ->
     match warn with
     | T.Unused_type_variable v -> Some (fun fmt () ->
         Format.fprintf fmt
@@ -190,7 +191,19 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
       )
 
     | Smtlib2_Ints.Restriction msg
+              -> Some (fun fmt () ->
+          Format.fprintf fmt
+            "This is a non-linear expression according to the smtlib spec.%a"
+            pp_hint msg
+        )
+
     | Smtlib2_Reals.Restriction msg
+              -> Some (fun fmt () ->
+          Format.fprintf fmt
+            "This is a non-linear expression according to the smtlib spec.%a"
+            pp_hint msg
+        )
+
     | Smtlib2_Reals_Ints.Restriction msg
       -> Some (fun fmt () ->
           Format.fprintf fmt
@@ -212,6 +225,8 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
         Format.fprintf fmt
           "Unknown warning, please report upstream, ^^"
       )
+    in
+    aux warn
 
   (* Report type errors *)
   (* ************************************************************************ *)
@@ -389,8 +404,10 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
       Format.fprintf fmt "Forbidden array sort.%a" pp_hint msg
 
     (* Smtlib Arithmetic errors *)
-    | Smtlib2_Ints.Forbidden msg
-    | Smtlib2_Reals.Forbidden msg
+    | Smtlib2_Ints.Forbidden msg ->
+      Format.fprintf fmt "Non-linear expressions are forbidden by the logic.%a" pp_hint msg
+    | Smtlib2_Reals.Forbidden msg ->
+      Format.fprintf fmt "Non-linear expressions are forbidden by the logic.%a" pp_hint msg
     | Smtlib2_Reals_Ints.Forbidden msg ->
       Format.fprintf fmt "Non-linear expressions are forbidden by the logic.%a" pp_hint msg
     | Smtlib2_Reals_Ints.Expected_arith_type ty ->
@@ -490,12 +507,18 @@ module Make(S : State_intf.Typer with type ty_state := ty_state) = struct
       T._error env fragment (Warning_as_error w)
 
     | Smtlib2_Ints.Restriction _, fragment
+      when conf.strict_typing ->
+      T._error env fragment (Warning_as_error w)
     | Smtlib2_Reals.Restriction _, fragment
+      when conf.strict_typing ->
+      T._error env fragment (Warning_as_error w)
     | Smtlib2_Reals_Ints.Restriction _, fragment
       when conf.strict_typing ->
       T._error env fragment (Warning_as_error w)
 
     | Smtlib2_Float.Real_lit, fragment
+      when conf.strict_typing ->
+      T._error env fragment (Warning_as_error w)
     | Smtlib2_Float.Bitv_extended_lit, fragment
       when conf.strict_typing ->
       T._error env fragment (Warning_as_error w)