Release 0.1.0

.ocamlformat

@@ -25,7 +25,7 @@ let-binding-spacing=compact
 let-module=compact
 margin=80
 max-indent=2
-module-item-spacing=compact
+module-item-spacing=sparse
 ocaml-version=4.14.0
 ocp-indent-compat=false
 parens-ite=false

bin/main.ml

@@ -23,8 +23,12 @@ let prover_conv =
     ; ("Colibri2", Colibri2_prover)
     ]
 
-let parse_cmdline =
-  let aux files prover incremental debug =
+let files =
+  let doc = "Source file(s)." in
+  Cmdliner.Arg.(value & pos_all non_dir_file [] & info [] ~doc)
+
+let run_cmd =
+  let run files prover incremental debug =
     let module Mappings =
       ( val match prover with
             | Z3_prover -> (module Z3_mappings)
@@ -52,24 +56,51 @@ let parse_cmdline =
            None files
   in
   let open Cmdliner in
-  let files =
-    Arg.(value & pos_all string [] & info [] ~docv:"files" ~doc:"files to read")
-  and prover =
-    Arg.(
-      value & opt prover_conv Z3_prover
-      & info [ "p"; "prover" ] ~doc:"SMT solver to use" )
+  let prover =
+    let doc = "SMT solver to use" in
+    Arg.(value & opt prover_conv Z3_prover & info [ "p"; "prover" ] ~doc)
   and incremental =
-    Arg.(
-      value & flag
-      & info [ "incremental" ] ~doc:"Use the SMT solver in the incremental mode" )
+    let doc = "Use the SMT solver in the incremental mode" in
+    Arg.(value & flag & info [ "incremental" ] ~doc)
   and debug =
-    Arg.(value & flag & info [ "debug" ] ~doc:"Print debugging messages")
+    let doc = "Print debugging messages" in
+    Arg.(value & flag & info [ "debug" ] ~doc)
+  in
+  let info = Cmd.info "run" in
+  Cmd.v info Term.(const run $ files $ prover $ incremental $ debug)
+
+let fmt_cmd =
+  let open Cmdliner in
+  let fmt files inplace =
+    let open Format in
+    let pp_ast fmt ast =
+      pp_print_list ~pp_sep:pp_print_newline Ast.pp fmt ast
+    in
+    match files with
+    | [] -> pp_ast std_formatter (parse_file "-")
+    | _ ->
+      List.iter
+        (fun file ->
+          let ast = parse_file file in
+          if inplace then
+            Out_channel.with_open_text file (fun out ->
+                Format.fprintf (formatter_of_out_channel out) "%a@." pp_ast ast )
+          else Format.printf "%a@." pp_ast ast )
+        files
+  in
+  let inplace =
+    let doc = "Format in-place, overwriting input file(s)." in
+    Cmdliner.Arg.(value & flag & info [ "inplace"; "i" ] ~doc)
   in
-  Cmd.v
-    (Cmd.info "smtml" ~version:"%%VERSION%%")
-    Term.(const aux $ files $ prover $ incremental $ debug)
+  let info = Cmd.info "fmt" in
+  Cmd.v info Term.(const fmt $ files $ inplace)
+
+let cli =
+  let open Cmdliner in
+  let info = Cmd.info "smtml" ~version:"%%VERSION%%" in
+  Cmd.group info [ run_cmd; fmt_cmd ]
 
 let () =
-  match Cmdliner.Cmd.eval_value parse_cmdline with
+  match Cmdliner.Cmd.eval_value cli with
   | Error (`Parse | `Term | `Exn) -> exit 2
   | Ok (`Ok () | `Version | `Help) -> ()

lib/ast.ml

@@ -1,20 +1,36 @@
+open Format
+
 type t =
-  | Assert of Expr.t
+  | Assert of term
   | Check_sat
   | Push
   | Pop of int
   | Let_const of Symbol.t
   | Get_model
 
+and term =
+  | E of Expr.t
+  | Let of binding list * term
+
+and binding = string * term
+
+let rec pp_term fmt = function
+  | E e -> Expr.pp fmt e
+  | Let (binds, t) ->
+    fprintf fmt "@[<v>(let@[<hov>@ (%a)@]@ %a)@]"
+      (pp_print_list ~pp_sep:pp_print_space pp_binding)
+      binds pp_term t
+
+and pp_binding fmt (x, t) = fprintf fmt "(%s %a)" x pp_term t
+
 let pp fmt (instr : t) =
   match instr with
-  | Assert e -> Format.fprintf fmt "(assert @[<h 2>%a@])" Expr.pp e
-  | Check_sat -> Format.pp_print_string fmt "(check-sat)"
-  | Push -> Format.pp_print_string fmt "(push)"
-  | Pop n -> Format.fprintf fmt "(pop %d)" n
+  | Assert t -> fprintf fmt "@[<hov 2>(assert@ %a)@]" pp_term t
+  | Check_sat -> pp_print_string fmt "(check-sat)"
+  | Push -> pp_print_string fmt "(push)"
+  | Pop n -> fprintf fmt "(pop %d)" n
   | Let_const s ->
-    let ty = Symbol.type_of s in
-    Format.fprintf fmt "(let-const %a %a)" Symbol.pp s Ty.pp ty
-  | Get_model -> Format.pp_print_string fmt "(get-model)"
+    fprintf fmt "(let-const %a %a)" Symbol.pp s Ty.pp (Symbol.ty s)
+  | Get_model -> pp_print_string fmt "(get-model)"
 
-let to_string (instr : t) : string = Format.asprintf "%a" pp instr
+let to_string (instr : t) : string = asprintf "%a" pp instr

lib/ast.mli

@@ -1,10 +1,17 @@
 type t =
-  | Assert of Expr.t
+  | Assert of term
   | Check_sat
   | Push
   | Pop of int
   | Let_const of Symbol.t
   | Get_model
 
+and term =
+  | E of Expr.t
+  | Let of binding list * term
+
+and binding = string * term
+
 val pp : Format.formatter -> t -> unit
+
 val to_string : t -> string

lib/colibri2_mappings.ml

@@ -18,28 +18,39 @@ module Fresh = struct
     include DTerm.Var
 
     let is_int _ = false
+
     let print = pp
   end
 
   module Ex = struct
     type t = unit
 
     let print fmt () = Fmt.pf fmt "()"
+
     let empty = ()
+
     let union () () = ()
   end
 
   module Rat = struct
     include A
 
     let m_one = A.minus_one
+
     let print = A.pp
+
     let is_int = A.is_integer
+
     let is_zero v = A.equal v A.zero
+
     let is_one v = A.equal v A.one
+
     let mult = A.mul
+
     let minus = A.neg
+
     let is_m_one v = A.equal v m_one
+
     let ceiling = ceil
   end
 
@@ -56,6 +67,7 @@ module Fresh = struct
     module Sim = OcplibSimplex.Basic.Make (Var) (Rat) (Ex)
 
     type optimize = Sim.Core.t
+
     type handle = optimize * (Sim.Core.P.t * bool) option
 
     type solver =
@@ -89,7 +101,9 @@ module Fresh = struct
         DExpr.{ arity = 0; alias = No_alias }
 
     let string_ty = DTy.apply string_ty_cst []
+
     let float32_ty = DTy.float 8 24
+
     let float64_ty = DTy.float 11 53
 
     let int_to_string : DExpr.term_cst =
@@ -805,7 +819,9 @@ module Fresh = struct
        add_string_axiom env f64_to_string string_to_f64 float64_ty *)
 
     let encode_expr e = encore_expr_aux e
+
     let pp_smt ?status:_ _ _ = ()
+
     let interrupt () = ()
 
     module Solver = struct
@@ -898,9 +914,13 @@ module Fresh = struct
 
     module Optimizer = struct
       let make () : optimize = Sim.Core.empty ~is_int:false ~check_invs:false
+
       let push _ = ()
+
       let pop _ = ()
+
       let add _ _ = assert false
+
       let check _ = assert false
 
       let model o =
@@ -915,7 +935,9 @@ module Fresh = struct
           None
 
       let maximize _ _ = assert false
+
       let minimize _ _ = assert false
+
       let pp_statistics _ _ = ()
     end
 

lib/ctor_intf.ml

@@ -0,0 +1,115 @@
+module type Bitv_sig = sig
+  type t
+
+  type elt
+
+  val v : elt -> t
+
+  val sym : string -> t
+
+  val ( ~- ) : t -> t
+
+  val clz : t -> t
+
+  val add : t -> t -> t
+
+  val sub : t -> t -> t
+
+  val mul : t -> t -> t
+
+  val div : t -> t -> t
+
+  val div_u : t -> t -> t
+
+  val rem : t -> t -> t
+
+  val rem_u : t -> t -> t
+
+  val logand : t -> t -> t
+
+  val logor : t -> t -> t
+
+  val logxor : t -> t -> t
+
+  val shl : t -> t -> t
+
+  val shr_s : t -> t -> t
+
+  val shr_u : t -> t -> t
+
+  val rotl : t -> t -> t
+
+  val rotr : t -> t -> t
+
+  val ( = ) : t -> t -> t
+
+  val ( != ) : t -> t -> t
+
+  val ( > ) : t -> t -> t
+
+  val gt_u : t -> t -> t
+
+  val ( >= ) : t -> t -> t
+
+  val ge_u : t -> t -> t
+
+  val ( < ) : t -> t -> t
+
+  val lt_u : t -> t -> t
+
+  val ( <= ) : t -> t -> t
+
+  val le_u : t -> t -> t
+
+  val bits_of_float : t -> t
+end
+
+module type Fp_sig = sig
+  type t
+
+  type elt
+
+  val v : elt -> t
+
+  val sym : string -> t
+
+  val abs : t -> t
+
+  val ( ~- ) : t -> t
+
+  val sqrt : t -> t
+
+  val ceil : t -> t
+
+  val floor : t -> t
+
+  val trunc : t -> t
+
+  val nearest : t -> t
+
+  val add : t -> t -> t
+
+  val sub : t -> t -> t
+
+  val mul : t -> t -> t
+
+  val div : t -> t -> t
+
+  val min : t -> t -> t
+
+  val max : t -> t -> t
+
+  val ( = ) : t -> t -> t
+
+  val ( != ) : t -> t -> t
+
+  val ( > ) : t -> t -> t
+
+  val ( >= ) : t -> t -> t
+
+  val ( < ) : t -> t -> t
+
+  val ( <= ) : t -> t -> t
+
+  val float_of_bits : t -> t
+end

lib/dune

@@ -10,7 +10,7 @@
  (modules
   ast
   ;axioms
-  constructors_intf
+  ctor_intf
   eval_numeric
   expr
   interpret