Add typing extensions, and the bvconv extension (#208)

Add typing extensions + bvconv ext

src/bin/options.ml

@@ -268,6 +268,18 @@ let report_style =
   ]
 
 
+(* Typing extensions *)
+(* ************************************************************************ *)
+
+let typing_extension_list =
+  List.map
+    (fun ext -> Loop.Typer.Ext.name ext, ext)
+    (Loop.Typer.Ext.list ())
+
+let typing_ext =
+  Arg.enum typing_extension_list
+
+
 (* Smtlib2 logic and extensions *)
 (* ************************************************************************ *)
 
@@ -352,10 +364,10 @@ let mk_run_state
     time_limit size_limit
     response_file
     flow_check
-    header_check header_licenses
-    header_lang_version
+    header_check header_licenses header_lang_version
     smtlib2_forced_logic smtlib2_exts
-    type_check check_model (* check_model_mode *)
+    type_check extension_builtins
+    check_model (* check_model_mode *)
     debug report_style max_warn reports syntax_error_ref
   =
   (* Side-effects *)
@@ -380,7 +392,9 @@ let mk_run_state
   |> Loop.Parser.init
     ~syntax_error_ref
     ~interactive_prompt:Loop.Parser.interactive_prompt_lang
-  |> Loop.Typer.init ~smtlib2_forced_logic
+  |> Loop.Typer.init
+    ~smtlib2_forced_logic
+    ~extension_builtins
   |> Loop.Typer_Pipe.init ~type_check
   |> Loop.Check.init
     ~check_model
@@ -613,6 +627,14 @@ let state =
     Arg.(value & opt_all smtlib2_ext [] &
          info ["internal-smtlib2-extension"] ~docs:internal_section ~doc)
   in
+  let typing_ext =
+    let doc = Format.asprintf
+        "Enable typing extensions.
+         $(docv) must be %s" (Arg.doc_alts_enum typing_extension_list)
+    in
+    Arg.(value & opt_all typing_ext [] &
+         info ["ext"] ~docs ~doc)
+  in
   let debug =
     let doc = Format.asprintf
         "Activate debug mode. Among other things, this will make dolmen \
@@ -673,10 +695,10 @@ let state =
         time $ size $
         response_file $
         flow_check $
-        header_check $ header_licenses $
-        header_lang_version $
+        header_check $ header_licenses $ header_lang_version $
         force_smtlib2_logic $ smtlib2_extensions $
-        typing $ check_model $ (* check_model_mode $ *)
+        typing $ typing_ext $
+        check_model $ (* check_model_mode $ *)
         debug $ report_style $ max_warn $ reports $ syntax_error_ref)
 
 

src/interface/term.ml

@@ -1368,6 +1368,19 @@ module type Smtlib_Array = sig
 
 end
 
+module type Smtlib_Bvconv = sig
+
+  type t
+  (** The type of terms *)
+
+  val to_nat : t -> t
+  (** Application of the bv2nat conversion function. *)
+
+  val of_int : int -> t -> t
+  (** Application of the int2bv conversion function. *)
+
+end
+
 module type Smtlib_Bitv = sig
 
   type t

src/loop/typer.ml

@@ -55,6 +55,9 @@ module Smtlib2_Arrays =
 module Smtlib2_Bitv =
   Dolmen_type.Bitv.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
+module Smtlib2_Bvconv =
+  Dolmen_type.Bitv.Smtlib2.Bvconv(T)
+    (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv)
 module Smtlib2_Float =
   Dolmen_type.Float.Smtlib2.Tff(T)
     (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term)
@@ -1079,26 +1082,63 @@ module Typer(State : State.S) = struct
     | `Response of Response.language
   ]
 
+  (* Extensions builtins *)
+  (* ************************************************************************ *)
+
+  module Ext = struct
+
+    type t = {
+      name : string;
+      builtins : lang -> T.builtin_symbols;
+    }
+
+    let all = ref []
+    let list () = !all
+    let name { name; _ } = name
+    let builtins { builtins; _ } = builtins
+
+    let create ~name ~builtins =
+      let t = { name; builtins; } in
+      all := t :: !all;
+      t
+
+    let bv2nat =
+      create ~name:"bvconv"
+        ~builtins:(function
+            | `Logic Logic.Smtlib2 version ->
+              Smtlib2_Bvconv.parse (`Script version)
+            | _ -> Dolmen_type.Base.noop)
+
+  end
+
+  (* State setup *)
+  (* ************************************************************************ *)
+
   let pipe = "Typer"
   let ty_state : ty_state State.key =
     State.create_key ~pipe "ty_state"
   let check_model : bool State.key =
     State.create_key ~pipe:"Model" "check_model"
   let smtlib2_forced_logic : string option State.key =
     State.create_key ~pipe "smtlib2_forced_logic"
+  let extension_builtins : Ext.t list State.key =
+    State.create_key ~pipe "extensions_builtins"
   let additional_builtins : (state -> lang -> T.builtin_symbols) State.key =
     State.create_key ~pipe "additional_builtins"
 
   let init
       ?ty_state:(ty_state_value=new_state ())
       ?smtlib2_forced_logic:(smtlib2_forced_logic_value=None)
+      ?extension_builtins:(extension_builtins_value=[])
       ?additional_builtins:(additional_builtins_value=fun _ _ _ _ -> `Not_found)
       st =
     st
     |> State.set ty_state ty_state_value
     |> State.set smtlib2_forced_logic smtlib2_forced_logic_value
+    |> State.set extension_builtins extension_builtins_value
     |> State.set additional_builtins additional_builtins_value
 
+
   (* Input helpers *)
   (* ************************************************************************ *)
 
@@ -1450,7 +1490,13 @@ module Typer(State : State.S) = struct
         in
         raise (State.Error st)
     in
-    let additional_builtins = State.get additional_builtins st st lang in
+    let user_builtins =
+      let additional_builtins = State.get additional_builtins st st lang in
+      let extension_builtins =
+        List.map (fun ext -> Ext.builtins ext lang) (State.get extension_builtins st)
+      in
+      additional_builtins :: extension_builtins
+    in
     match lang with
     (* Dimacs & iCNF
        - these infer the declarations of their constants
@@ -1473,7 +1519,10 @@ module Typer(State : State.S) = struct
               preferred = Dolmen.Std.Expr.Ty.prop;
             });
         } in
-      let builtins = Dimacs.parse in
+      let builtins = Dolmen_type.Base.merge (
+          user_builtins @ [
+          Dimacs.parse
+        ]) in
       T.empty_env ~order:First_order
         ~st:(State.get ty_state st).typer
         ~var_infer ~sym_infer ~poly
@@ -1494,13 +1543,13 @@ module Typer(State : State.S) = struct
           infer_type_csts = false;
           infer_term_csts = No_inference;
         } in
-      let builtins = Dolmen_type.Base.merge [
-          additional_builtins;
+      let builtins = Dolmen_type.Base.merge (
+          user_builtins @ [
           Ae_Core.parse;
           Ae_Arith.parse;
           Ae_Arrays.parse;
           Ae_Bitv.parse;
-        ] in
+        ]) in
       T.empty_env ~order:First_order
         ~st:(State.get ty_state st).typer
         ~var_infer ~sym_infer ~poly
@@ -1524,11 +1573,11 @@ module Typer(State : State.S) = struct
           infer_type_csts = false;
           infer_term_csts = No_inference;
         } in
-      let builtins = Dolmen_type.Base.merge [
-          additional_builtins;
+      let builtins = Dolmen_type.Base.merge (
+          user_builtins @ [
           Zf_Core.parse;
           Zf_arith.parse
-        ] in
+        ]) in
       T.empty_env ~order:Higher_order
         ~st:(State.get ty_state st).typer
         ~var_infer ~sym_infer ~poly
@@ -1553,11 +1602,11 @@ module Typer(State : State.S) = struct
               infer_type_csts = false;
               infer_term_csts = No_inference;
             } in
-          let builtins = Dolmen_type.Base.merge [
-              additional_builtins;
+          let builtins = Dolmen_type.Base.merge (
+              user_builtins @ [
               Tptp_Core_Ho.parse v;
               Tptp_Arith.parse v;
-            ] in
+            ]) in
           T.empty_env ~order:Higher_order
             ~st:(State.get ty_state st).typer
             ~var_infer ~sym_infer ~poly
@@ -1590,11 +1639,11 @@ module Typer(State : State.S) = struct
                     };
                 });
             } in
-          let builtins = Dolmen_type.Base.merge [
-              additional_builtins;
+          let builtins = Dolmen_type.Base.merge (
+              user_builtins @ [
               Tptp_Core.parse v;
               Tptp_Arith.parse v;
-            ] in
+            ]) in
           T.empty_env ~order:First_order
             ~st:(State.get ty_state st).typer
             ~var_infer ~sym_infer ~poly
@@ -1640,7 +1689,7 @@ module Typer(State : State.S) = struct
           T._error env (Located loc) Missing_smtlib_logic
         | Smtlib2 logic ->
           let builtins = Dolmen_type.Base.merge (
-              additional_builtins ::
+              user_builtins @
               builtins_of_smtlib2_logic (`Script v) logic
             ) in
           let quants = logic.features.quantifiers in
@@ -1674,7 +1723,7 @@ module Typer(State : State.S) = struct
           T._error env (Located loc) Missing_smtlib_logic
         | Smtlib2 logic ->
           let builtins = Dolmen_type.Base.merge (
-              additional_builtins ::
+              user_builtins @
               builtins_of_smtlib2_logic (`Response v) logic
             ) in
           let quants = logic.features.quantifiers in

src/loop/typer_intf.ml

@@ -129,16 +129,6 @@ module type Typer_Full = sig
   type builtin_symbols
   (** The type of builin symbols for the type-checker. *)
 
-  val ty_state : ty_state key
-  (** Key to store the local typechecking state in the global pipeline state. *)
-
-  val check_model : bool key
-  (** The typechecker needs to know whether we are checking models or not. *)
-
-  val smtlib2_forced_logic : string option key
-  (** Force the typechecker to use the given logic (instead of using the one declared
-      in the `set-logic` statement). *)
-
   include Typer
     with type env := env
      and type state := state
@@ -153,11 +143,48 @@ module type Typer_Full = sig
   (** This signature includes the requirements to instantiate the {Pipes.Make:
       functor*)
 
-  val init :
-    ?ty_state:ty_state ->
-    ?smtlib2_forced_logic:string option ->
-    ?additional_builtins:(state -> lang -> builtin_symbols) ->
-    state -> state
+  module Ext : sig
+    (** Define typing extensions.
+
+        These extensions are typically extensions used by some community,
+        but not yet part of the standard.
+
+        @since 0.10 *)
+
+    type t
+    (** The type of typing extensions. *)
+
+    val name : t -> string
+    (** Extension name, sould be suitable for cli options. *)
+
+    val builtins : t -> lang -> builtin_symbols
+    (** Reutnrs the typing builtins from an extension. *)
+
+    val create : name:string -> builtins:(lang -> builtin_symbols) -> t
+    (** Create a new extension. *)
+
+    val list : unit -> t list
+    (** The list of all extensions. *)
+
+    val bv2nat : t
+    (** Typing extension to add the `bv2nat` function. *)
+
+  end
+
+  val ty_state : ty_state key
+  (** Key to store the local typechecking state in the global pipeline state. *)
+
+  val check_model : bool key
+  (** The typechecker needs to know whether we are checking models or not. *)
+
+  val smtlib2_forced_logic : string option key
+  (** Force the typechecker to use the given logic (instead of using the one declared
+      in the `set-logic` statement). *)
+
+  val extension_builtins : Ext.t list key
+  (** Use typing extensions defined by the typechecker.
+
+      @since 0.10 *)
 
   val additional_builtins : (state -> lang -> builtin_symbols) key
   (** Add new builtin symbols to the typechecker, depending on the current
@@ -167,6 +194,13 @@ module type Typer_Full = sig
 
       @before 0.9 [additional_builtins] had type [builtin_symbols ref]. *)
 
+  val init :
+    ?ty_state:ty_state ->
+    ?smtlib2_forced_logic:string option ->
+    ?extension_builtins:(Ext.t list) ->
+    ?additional_builtins:(state -> lang -> builtin_symbols) ->
+    state -> state
+
   val report_error : input:input -> state -> error -> state
   (** Report a typing error by calling the appropriate state function. *)
 

src/standard/builtin.ml

@@ -89,6 +89,8 @@ type _ t +=
 type _ t +=
   | Bitv of int
   | Bitvec of string
+  | Bitv_to_nat of { n : int; }
+  | Bitv_of_int of { n : int; }
   | Bitv_concat of { n : int; m : int }
   | Bitv_extract of { n : int; i : int; j : int }
   | Bitv_repeat of { n : int; k : int }

src/standard/builtin.mli

@@ -350,6 +350,12 @@ type _ t +=
   (** [Bitvec s: Bitv]: bitvector litteral. The string [s] should
       be a binary representation of bitvectors using characters
       ['0'], and ['1'] (lsb last) *)
+  | Bitv_to_nat of { n : int; }
+  (** [Bitv_to_nat(n): Bitv(n) -> Int]:
+      conversion from bitvectors to integers. *)
+  | Bitv_of_int of { n : int; }
+  (** [Bitv_of_int(n): Int -> Bitv(n)]:
+      conversion fromm (signed) integers to bitvectors. *)
   | Bitv_concat of { n : int; m : int }
   (** [Bitv_concat(n,m): Bitv(n) -> Bitv(m) -> Bitv(n+m)]:
       concatenation operator on bitvectors. *)