V8.7 (#36)

Port SMTCoq to Coq-8.7

7 files changed, 71 insertions, 79 deletions

diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml
index 29a4afc..454bc0a 100644
--- a/src/lfsc/ast.ml
+++ b/src/lfsc/ast.ml
@@ -83,12 +83,12 @@ let value t = (deref t).value
 let ttype t = deref (deref t).ttype
 
 
-let rec name c = match value c with
+let name c = match value c with
   | Const {sname=Name n} -> Some n
   | _ -> None
 
 
-let rec app_name r = match value r with
+let app_name r = match value r with
   | App ({value=Const{sname=Name n}}, args) -> Some (n, args)
   | _ -> None
 
@@ -298,36 +298,36 @@ end
 
 
 
-let rec holes_address acc t = match t.value with
-  | Hole i -> (i, t) :: acc
-  | Type | Kind |  Mpz | Mpq | Int _ | Rat _  -> acc
-  | SideCond (name, args, exp, t) -> acc
-  | Const _ -> acc
-  | App (f, args) ->
-    List.fold_left holes_address acc args 
-  | Pi (s, x) -> holes_address acc x
-  | Lambda (s, x) -> holes_address acc x
-  | Ptr t -> holes_address acc t
-
-let holes_address = holes_address []
-
-
-let check_holes_integrity where h1 h2 =
-  List.iter (fun (i, a) ->
-      List.iter (fun (j, b) ->
-          if j = i && a != b then
-            (
-              eprintf "\n%s: Hole _%d was at %nx, now at %nx\n@." where i
-                (address_of a) (address_of b);
-              (* eprintf "\n%s: Hole _%d has changed\n@." where i; *)
-              assert false)
-        ) h2
-    ) h1
-
-let check_term_integrity where t = 
-  let h = holes_address t in
-  check_holes_integrity (where ^ "term has != _") h h
-    
+(* let rec holes_address acc t = match t.value with
+ *   | Hole i -> (i, t) :: acc
+ *   | Type | Kind |  Mpz | Mpq | Int _ | Rat _  -> acc
+ *   | SideCond (name, args, exp, t) -> acc
+ *   | Const _ -> acc
+ *   | App (f, args) ->
+ *     List.fold_left holes_address acc args
+ *   | Pi (s, x) -> holes_address acc x
+ *   | Lambda (s, x) -> holes_address acc x
+ *   | Ptr t -> holes_address acc t *)
+
+(* let holes_address = holes_address [] *)
+
+
+(* let check_holes_integrity where h1 h2 =
+ *   List.iter (fun (i, a) ->
+ *       List.iter (fun (j, b) ->
+ *           if j = i && a != b then
+ *             (
+ *               eprintf "\n%s: Hole _%d was at %nx, now at %nx\n@." where i
+ *                 (address_of a) (address_of b);
+ *               (\* eprintf "\n%s: Hole _%d has changed\n@." where i; *\)
+ *               assert false)
+ *         ) h2
+ *     ) h1 *)
+
+(* let check_term_integrity where t =
+ *   let h = holes_address t in
+ *   check_holes_integrity (where ^ "term has != _") h h *)
+
 
 
 let eq_name s1 s2 = match s1, s2 with
@@ -471,10 +471,10 @@ module MSym = Map.Make (struct
 
 let empty_subst = MSym.empty
 
-let fresh_alpha =
-  let cpt = ref 0 in
-  fun ty -> incr cpt;
-    mk_symbol ("'a"^string_of_int !cpt) ty
+(* let fresh_alpha =
+ *   let cpt = ref 0 in
+ *   fun ty -> incr cpt;
+ *     mk_symbol ("'a"^string_of_int !cpt) ty *)
 
 
 let get_t ?(gen=true) sigma s =
@@ -834,20 +834,20 @@ let rec hole_nbs acc t = match value t with
   | _ -> acc
 
 
-let rec min_hole acc t = match value t with
-  | Hole nb ->
-    (match acc with Some n when nb < n -> Some nb  | None -> Some nb | _ -> acc)
-  | App (f, args) -> List.fold_left min_hole (min_hole acc f) args 
-  | Pi (s, x) | Lambda (s, x) -> min_hole acc x
-  | Ptr t -> min_hole acc t
-  | _ -> acc
+(* let rec min_hole acc t = match value t with
+ *   | Hole nb ->
+ *     (match acc with Some n when nb < n -> Some nb  | None -> Some nb | _ -> acc)
+ *   | App (f, args) -> List.fold_left min_hole (min_hole acc f) args
+ *   | Pi (s, x) | Lambda (s, x) -> min_hole acc x
+ *   | Ptr t -> min_hole acc t
+ *   | _ -> acc *)
 
 
-let compare_int_opt m1 m2 = match m1, m2 with
-  | None, None -> 0
-  | Some _, None -> -1
-  | None, Some _ -> 1
-  | Some n1, Some n2 -> compare n1 n2
+(* let compare_int_opt m1 m2 = match m1, m2 with
+ *   | None, None -> 0
+ *   | Some _, None -> -1
+ *   | None, Some _ -> 1
+ *   | Some n1, Some n2 -> compare n1 n2 *)
 
 
 let compare_sc_checks (_, args1, exp1) (_, args2, exp2) =
diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml
index 7d0151b..86899df 100644
--- a/src/lfsc/builtin.ml
+++ b/src/lfsc/builtin.ml
@@ -11,7 +11,6 @@
 
 
 open Ast
-open Format
 
 
 module H = struct
@@ -90,7 +89,7 @@ module H = struct
 
   let var_bv = Hstring.make "var_bv"
 
-  let a_var_bv = Hstring.make "a_var_bv"
+  (* let a_var_bv = Hstring.make "a_var_bv" *)
   let a_bv = Hstring.make "a_bv"
   let a_int = Hstring.make "a_int"
 
@@ -98,7 +97,7 @@ module H = struct
   let bitof = Hstring.make "bitof"
   let bblast_term = Hstring.make "bblast_term"
 
-  let eq = Hstring.make "="
+  (* let eq = Hstring.make "=" *)
   let bvand = Hstring.make "bvand"
   let bvor = Hstring.make "bvor"
   let bvxor = Hstring.make "bvxor"
@@ -163,7 +162,7 @@ module H = struct
   let tfalse = Hstring.make "false"
   let a_var_bv = Hstring.make "a_var_bv"
   let eq = Hstring.make "="
-  let trust_f = Hstring.make "trust_f"
+  (* let trust_f = Hstring.make "trust_f" *)
   let ext = Hstring.make "ext"
   let decl_atom = Hstring.make "decl_atom"
   let asf = Hstring.make "asf"
@@ -179,7 +178,7 @@ module H = struct
   let or_elim_1 = Hstring.make "or_elim_1"
   let or_elim_2 = Hstring.make "or_elim_2"
   let iff_elim_1 = Hstring.make "iff_elim_1"
-  let iff_elim_2 = Hstring.make "iff_elim_2"
+  (* let iff_elim_2 = Hstring.make "iff_elim_2" *)
   let impl_elim = Hstring.make "impl_elim"
   let not_and_elim = Hstring.make "not_and_elim"
   let xor_elim_1 = Hstring.make "xor_elim_1"
@@ -232,8 +231,8 @@ module H = struct
   let bv_bbl_bvneg = Hstring.make "bv_bbl_bvneg"
   let bv_bbl_bvadd = Hstring.make "bv_bbl_bvadd"
   let bv_bbl_bvmul = Hstring.make "bv_bbl_bvmul"
-  let bv_bbl_bvult = Hstring.make "bv_bbl_bvult"
-  let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt"
+  (* let bv_bbl_bvult = Hstring.make "bv_bbl_bvult" *)
+  (* let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt" *)
   let bv_bbl_concat = Hstring.make "bv_bbl_concat"
   let bv_bbl_extract = Hstring.make "bv_bbl_extract"
   let bv_bbl_zero_extend = Hstring.make "bv_bbl_zero_extend"
@@ -1172,7 +1171,7 @@ let rec bblast_bvult x y n =
   | _ -> failwith "bblast_bvult"
 
 
-let rec bblast_bvslt x y n =
+let bblast_bvslt x y n =
   match value x with
   | App (ff, [xi; x']) when term_equal ff bbltc_s ->
     (match value y with
diff --git a/src/lfsc/converter.ml b/src/lfsc/converter.ml
index d586e37..2dfbed3 100644
--- a/src/lfsc/converter.ml
+++ b/src/lfsc/converter.ml
@@ -874,19 +874,19 @@ module Make (T : Translator_sig.S) = struct
       | _ -> raise Not_found
              
 
-  let rec reso_of_QR acc qr = match app_name qr with
-    | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
-      reso_of_QR (reso_of_QR acc u1) u2
-    | _ -> clause_qr qr :: acc
+  (* let rec reso_of_QR acc qr = match app_name qr with
+   *   | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
+   *     reso_of_QR (reso_of_QR acc u1) u2
+   *   | _ -> clause_qr qr :: acc *)
 
   (** Returns clauses used in a linear resolution chain *)
-  let reso_of_QR qr = reso_of_QR [] qr |> List.rev
+  (* let reso_of_QR qr = reso_of_QR [] qr |> List.rev *)
 
 
-  let rec reso_of_QR qr = match app_name qr with
-    | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
-      reso_of_QR u1 @ reso_of_QR u2
-    | _ -> [clause_qr qr]
+  (* let rec reso_of_QR qr = match app_name qr with
+   *   | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
+   *     reso_of_QR u1 @ reso_of_QR u2
+   *   | _ -> [clause_qr qr] *)
 
   let rec reso_of_QR depth acc qr = match app_name qr with
     | Some (n, [_; _; u1; u2; _]) when n == H.q || n == H.r ->
@@ -963,7 +963,7 @@ module Make (T : Translator_sig.S) = struct
       | None -> assert false
 
 
-  let rec bb_lem env p =
+  let bb_lem env p =
     let env, p = bb_trim_intro_unit env p in
     let id = bb_lem_res None p in
     { env with clauses = id :: env.clauses }
diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml
index 0f9fd8d..a11139d 100644
--- a/src/lfsc/lfsc.ml
+++ b/src/lfsc/lfsc.ml
@@ -11,13 +11,9 @@
 
 
 open Format
-open Entries
-open Declare
-open Decl_kinds
 
 open SmtMisc
 open CoqTerms
-open SmtForm
 open SmtCertif
 open SmtTrace
 open SmtAtom
@@ -163,8 +159,8 @@ let checker_debug fsmt fproof =
 let theorem name fsmt fproof =
   SmtCommands.theorem name (import_all fsmt fproof)
 
-let checker fsmt fproof =
-  SmtCommands.checker (import_all fsmt fproof)
+(* let checker fsmt fproof =
+ *   SmtCommands.checker (import_all fsmt fproof) *)
 
 (* Same but print runtime *)
 let checker fsmt fproof =
diff --git a/src/lfsc/lfscLexer.mll b/src/lfsc/lfscLexer.mll
index 3e8d5f9..242df00 100644
--- a/src/lfsc/lfscLexer.mll
+++ b/src/lfsc/lfscLexer.mll
@@ -245,7 +245,7 @@ and scan_string buf start = parse
       {
         let ofs = lexbuf.lex_start_pos in
         let len = lexbuf.lex_curr_pos - ofs in
-        Quoted_string_buffer.add_substring buf lexbuf.lex_buffer ofs len;
+        Quoted_string_buffer.add_substring buf (Bytes.to_string lexbuf.lex_buffer) ofs len;
         Quoted_string_buffer.add_lexeme buf lexbuf;
         scan_string buf start lexbuf
       }
diff --git a/src/lfsc/lfscParser.mly b/src/lfsc/lfscParser.mly
index 26de090..3d6749f 100644
--- a/src/lfsc/lfscParser.mly
+++ b/src/lfsc/lfscParser.mly
@@ -16,7 +16,6 @@
 open Ast
 open Lexing
 open Format
-open Builtin
 
 let parse_failure what =
   let pos = Parsing.symbol_start_pos () in
diff --git a/src/lfsc/tosmtcoq.ml b/src/lfsc/tosmtcoq.ml
index 0395244..f520ba7 100644
--- a/src/lfsc/tosmtcoq.ml
+++ b/src/lfsc/tosmtcoq.ml
@@ -12,8 +12,6 @@
 
 open SmtAtom
 open SmtForm
-open SmtCertif
-open SmtTrace
 open VeritSyntax
 open Ast
 open Builtin
@@ -42,7 +40,7 @@ module HT = struct
   let add h k v = h := M.add k v !h
   let find h k = M.find k !h
   let clear h = h := M.empty
-  let iter f h = M.iter f !h
+  (* let iter f h = M.iter f !h *)
 end
 
 
@@ -499,8 +497,8 @@ let register_clause_id cl id =
   Hashtbl.add ids_clauses id cl
 
 
-let register_termclause_id t id =
-  register_clause_id (to_clause t) id
+(* let register_termclause_id t id =
+ *   register_clause_id (to_clause t) id *)
 
 
 let new_clause_id ?(reuse=true) cl =