From 409fe49ff0decf9002f3d14b15b5e2d0d1f07bfa Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Thu, 7 Nov 2019 10:35:59 -0600
Subject: [PATCH] feat(bin): use stmlib-utils 0.1, with versionned API and new
 statements

---
 sidekick-bin.opam             |  3 ---
 src/smtlib/Sidekick_smtlib.ml |  6 +++---
 src/smtlib/Typecheck.ml       | 31 ++++++++++++++++++++++++++-----
 src/smtlib/Typecheck.mli      |  4 ++--
 4 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/sidekick-bin.opam b/sidekick-bin.opam
index 26e8bfdf..b34c61e4 100644
--- a/sidekick-bin.opam
+++ b/sidekick-bin.opam
@@ -21,9 +21,6 @@ depends: [
   "msat" { >= "0.8" < "0.9" }
   "ocaml" { >= "4.03" } 
 ]
-pin-depends: [
-  ["smtlib-utils.0.1" "git+https://github.com/c-cube/smtlib-utils.git"]
-]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"
 dev-repo: "git+https://github.com/c-cube/sidekick.git"
diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml
index 1359cc4f..0f50de59 100644
--- a/src/smtlib/Sidekick_smtlib.ml
+++ b/src/smtlib/Sidekick_smtlib.ml
@@ -4,8 +4,8 @@ module ID = Sidekick_base_term.ID
 module Fmt = CCFormat
 module Ast = Ast
 module E = CCResult
-module Loc = Smtlib_utils.Loc
-module Parse_ast = Smtlib_utils.Ast
+module Loc = Smtlib_utils.V_2_6.Loc
+module Parse_ast = Smtlib_utils.V_2_6.Ast
 module Process = Process
 module Solver = Process.Solver
 
@@ -20,7 +20,7 @@ module Parse = struct
   let parse_chan_exn ?(filename="<no name>") ic =
     let lexbuf = Lexing.from_channel ic in
     Loc.set_file lexbuf filename;
-    Smtlib_utils.Parser.parse_list Smtlib_utils.Lexer.token lexbuf
+    Smtlib_utils.V_2_6.(Parser.parse_list Lexer.token) lexbuf
 
   let parse_file_exn file : Parse_ast.statement list =
     CCIO.with_in file (parse_chan_exn ~filename:file)
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index 01e0e638..705db130 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -3,12 +3,12 @@
 (** {1 Preprocessing AST} *)
 
 open Sidekick_base_term
-module Loc = Smtlib_utils.Loc
+module Loc = Smtlib_utils.V_2_6.Loc
 module Fmt = CCFormat
 module Log = Msat.Log
 
 module A = Ast
-module PA = Smtlib_utils.Ast
+module PA = Smtlib_utils.V_2_6.Ast
 
 type 'a or_error = ('a, string) CCResult.t
 
@@ -369,10 +369,13 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie
     let f, ty = conv_fun_decl ctx fr in
     let id = Ctx.add_id ctx f (Ctx.K_fun ty) in
     [A.Decl (id, ty)]
-  | PA.Stmt_data ([],l) ->
+  | PA.Stmt_data l when List.for_all (fun ((_,n),_) -> n=0) l ->
     (* first, read and declare each datatype (it can occur in the other
     datatypes' construtors) *)
-    let pre_parse (data_name,cases) =
+    let pre_parse ((data_name,arity),cases) =
+      if arity <> 0 then (
+        errorf_ctx ctx "cannot handle polymorphic datatype %s" data_name;
+      );
       let data_id = Ctx.add_id ctx data_name (Ctx.K_ty Ctx.K_data) in
       data_id, cases
     in
@@ -382,7 +385,10 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie
      List.map
        (fun (data_id, (cstors:PA.cstor list)) ->
          let data_ty = A.Ty.const data_id in
-         let parse_case {PA.cstor_name=c; cstor_args} =
+         let parse_case {PA.cstor_name=c; cstor_args; cstor_ty_vars} =
+           if cstor_ty_vars <> [] then (
+             errorf_ctx ctx "cannot handle polymorphic constructor %s" c;
+           );
            let selectors =
              List.map (fun (n,ty) -> Some n, conv_ty_fst ctx ty) cstor_args
            in
@@ -440,4 +446,19 @@ and conv_statement_aux ctx (stmt:PA.statement) : A.statement list = match PA.vie
     check_bool_ t;
     [A.Assert t]
   | PA.Stmt_check_sat -> [A.CheckSat]
+  | PA.Stmt_check_sat_assuming _
+  | PA.Stmt_get_assertions 
+  | PA.Stmt_get_option _
+  | PA.Stmt_get_info _
+  | PA.Stmt_get_model
+  | PA.Stmt_get_proof
+  | PA.Stmt_get_unsat_core
+  | PA.Stmt_get_unsat_assumptions
+  | PA.Stmt_get_assignment
+  | PA.Stmt_reset
+  | PA.Stmt_reset_assertions
+  | PA.Stmt_push _
+  | PA.Stmt_pop _
+  | PA.Stmt_get_value _
+      -> errorf_ctx ctx "cannot handle statement %a" PA.pp_stmt stmt
 
diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli
index bb5c46e5..23d1dac8 100644
--- a/src/smtlib/Typecheck.mli
+++ b/src/smtlib/Typecheck.mli
@@ -2,7 +2,7 @@
 
 (** {1 Preprocessing AST} *)
 
-module Loc = Smtlib_utils.Loc
+module Loc = Smtlib_utils.V_2_6.Loc
 
 type 'a or_error = ('a, string) CCResult.t
 
@@ -14,7 +14,7 @@ module Ctx : sig
   val pp : t CCFormat.printer
 end
 
-module PA = Smtlib_utils.Ast
+module PA = Smtlib_utils.V_2_6.Ast
 module A = Ast
 
 val conv_term : Ctx.t -> PA.term -> A.term