From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001 From: ckeller Date: Thu, 14 Feb 2019 20:09:40 +0100 Subject: V8.7 (#36) Port SMTCoq to Coq-8.7 --- src/lfsc/ast.ml | 96 ++++++++++++++++++++++++------------------------- src/lfsc/builtin.ml | 15 ++++---- src/lfsc/converter.ml | 20 +++++------ src/lfsc/lfsc.ml | 8 ++--- src/lfsc/lfscLexer.mll | 2 +- src/lfsc/lfscParser.mly | 1 - src/lfsc/tosmtcoq.ml | 8 ++--- 7 files changed, 71 insertions(+), 79 deletions(-) (limited to 'src/lfsc') 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 = -- cgit