From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Thu, 14 Feb 2019 20:09:40 +0100
Subject: V8.7 (#36)

Port SMTCoq to Coq-8.7
---
 src/smtlib2/smtlib2_ast.ml        | 124 +++++++++++++++++++-------------------
 src/smtlib2/smtlib2_genConstr.ml  |   2 +-
 src/smtlib2/smtlib2_genConstr.mli |   1 +
 src/smtlib2/smtlib2_solver.ml     |   2 +-
 4 files changed, 64 insertions(+), 65 deletions(-)

(limited to 'src/smtlib2')

diff --git a/src/smtlib2/smtlib2_ast.ml b/src/smtlib2/smtlib2_ast.ml
index 7317b60..65dc3e3 100644
--- a/src/smtlib2/smtlib2_ast.ml
+++ b/src/smtlib2/smtlib2_ast.ml
@@ -16,8 +16,6 @@
 (**************************************************************************)
 
 
-open Smtlib2_util
-
 type loc = Lexing.position * Lexing.position
 
 type specconstant =
@@ -191,65 +189,65 @@ let loc_of e = loc_commands e;;
 
 
 
-let print_specconstant fmt = function
-  | SpecConstsDec (_, s)
-  | SpecConstNum (_, s)
-  | SpecConstString (_, s)
-  | SpecConstsHex (_, s)
-  | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s
-
-
-let print_symbol fmt = function
-  | Symbol (_, s)
-  | SymbolWithOr (_, s) -> Format.pp_print_string fmt s
-
-
-let print_identifier fmt = function
-  | IdSymbol (_, s) -> print_symbol fmt s
-  | IdUnderscoreSymNum (_, s, (_, l)) ->
-    Format.fprintf fmt "(_ %a" print_symbol s;
-    List.iter (Format.fprintf fmt " %s") l;
-    Format.fprintf fmt ")"  
-    
-let rec print_sort fmt = function
-  | SortIdentifier (_, i) -> print_identifier fmt i
-  | SortIdSortMulti (_, i, (_, ls)) ->
-    Format.fprintf fmt "(%a" print_identifier i;
-    List.iter (Format.fprintf fmt " %a" print_sort) ls;
-    Format.fprintf fmt ")"  
-
-let print_qualidentifier fmt = function
-  | QualIdentifierId (_, i) -> print_identifier fmt i
-  | QualIdentifierAs (_, i, s) ->
-    Format.fprintf fmt "(%a as %a)"
-      print_identifier i print_sort s 
-
-let print_sortedvar fmt = function
-  | SortedVarSymSort (_, v, s) ->
-    Format.fprintf fmt "(%a %a)" print_symbol v print_sort s
-
-let rec print_varbinding fmt = function
-  | VarBindingSymTerm (_, s, t) ->
-    Format.fprintf fmt "(%a %a)" print_symbol s print_term t
-
-and print_term fmt = function
-  | TermSpecConst (_, c) -> print_specconstant fmt c
-  | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
-  | TermQualIdTerm (_, i, (_, tl)) ->
-    Format.fprintf fmt "(%a" print_qualidentifier i;
-    List.iter (Format.fprintf fmt " %a" print_term) tl;
-    Format.fprintf fmt ")"  
-  | TermLetTerm (_, (_, vb), t) ->
-    Format.fprintf fmt "(let (";
-    List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
-    Format.fprintf fmt ") %a)" print_term t
-  | TermForAllTerm (_, (_, sv), t) ->
-    Format.fprintf fmt "(forall (";
-    List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
-    Format.fprintf fmt ") %a)" print_term t
-  | TermExistsTerm (_, (_, sv), t) ->
-    Format.fprintf fmt "(exists (";
-    List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
-    Format.fprintf fmt ") %a)" print_term t
-  | TermExclimationPt (_, t, _) -> print_term fmt t
+(* let print_specconstant fmt = function
+ *   | SpecConstsDec (_, s)
+ *   | SpecConstNum (_, s)
+ *   | SpecConstString (_, s)
+ *   | SpecConstsHex (_, s)
+ *   | SpecConstsBinary (_, s) -> Format.pp_print_string fmt s *)
+
+
+(* let print_symbol fmt = function
+ *   | Symbol (_, s)
+ *   | SymbolWithOr (_, s) -> Format.pp_print_string fmt s *)
+
+
+(* let print_identifier fmt = function
+ *   | IdSymbol (_, s) -> print_symbol fmt s
+ *   | IdUnderscoreSymNum (_, s, (_, l)) ->
+ *     Format.fprintf fmt "(_ %a" print_symbol s;
+ *     List.iter (Format.fprintf fmt " %s") l;
+ *     Format.fprintf fmt ")" *)
+
+(* let rec print_sort fmt = function
+ *   | SortIdentifier (_, i) -> print_identifier fmt i
+ *   | SortIdSortMulti (_, i, (_, ls)) ->
+ *     Format.fprintf fmt "(%a" print_identifier i;
+ *     List.iter (Format.fprintf fmt " %a" print_sort) ls;
+ *     Format.fprintf fmt ")" *)
+
+(* let print_qualidentifier fmt = function
+ *   | QualIdentifierId (_, i) -> print_identifier fmt i
+ *   | QualIdentifierAs (_, i, s) ->
+ *     Format.fprintf fmt "(%a as %a)"
+ *       print_identifier i print_sort s *)
+
+(* let print_sortedvar fmt = function
+ *   | SortedVarSymSort (_, v, s) ->
+ *     Format.fprintf fmt "(%a %a)" print_symbol v print_sort s *)
+
+(* let rec print_varbinding fmt = function
+ *   | VarBindingSymTerm (_, s, t) ->
+ *     Format.fprintf fmt "(%a %a)" print_symbol s print_term t *)
+
+(* and print_term fmt = function
+ *   | TermSpecConst (_, c) -> print_specconstant fmt c
+ *   | TermQualIdentifier (_, i) -> print_qualidentifier fmt i
+ *   | TermQualIdTerm (_, i, (_, tl)) ->
+ *     Format.fprintf fmt "(%a" print_qualidentifier i;
+ *     List.iter (Format.fprintf fmt " %a" print_term) tl;
+ *     Format.fprintf fmt ")"
+ *   | TermLetTerm (_, (_, vb), t) ->
+ *     Format.fprintf fmt "(let (";
+ *     List.iter (Format.fprintf fmt " %a" print_varbinding) vb;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermForAllTerm (_, (_, sv), t) ->
+ *     Format.fprintf fmt "(forall (";
+ *     List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermExistsTerm (_, (_, sv), t) ->
+ *     Format.fprintf fmt "(exists (";
+ *     List.iter (Format.fprintf fmt " %a" print_sortedvar) sv;
+ *     Format.fprintf fmt ") %a)" print_term t
+ *   | TermExclimationPt (_, t, _) -> print_term fmt t *)
 
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 692294d..203077b 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -50,7 +50,7 @@ let string_type s =
 let sort_of_string s = string_type s
 
 
-let sort_of_symbol s = sort_of_string (string_of_symbol s)
+(* let sort_of_symbol s = sort_of_string (string_of_symbol s) *)
 
 
 let rec bigint_binary_size acc i size =
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli
index 40f73c7..dabd99b 100644
--- a/src/smtlib2/smtlib2_genConstr.mli
+++ b/src/smtlib2/smtlib2_genConstr.mli
@@ -10,6 +10,7 @@
 (**************************************************************************)
 
 
+val pp_symbol : Smtlib2_ast.symbol -> string
 val parse_smt2bv : string -> bool list
 val bigint_bv : Big_int.big_int -> int -> string
 val import_smtlib2 :
diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml
index 3ee8229..8ae7202 100644
--- a/src/smtlib2/smtlib2_solver.ml
+++ b/src/smtlib2/smtlib2_solver.ml
@@ -82,7 +82,7 @@ let read_success s =
   | r -> error s r
 
 
-let no_response _ = ()
+(* let no_response _ = () *)
 
 
 let read_check_result s = 
-- 
cgit