aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace')
-rw-r--r--src/trace/coqTerms.ml67
-rw-r--r--src/trace/smtCommands.ml4
-rw-r--r--src/trace/smtForm.ml18
-rw-r--r--src/trace/smtForm.mli8
-rw-r--r--src/trace/smtMisc.ml2
-rw-r--r--src/trace/smtTrace.ml4
6 files changed, 51 insertions, 52 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 6cbdbc0..a5a95ea 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -10,7 +10,6 @@
(**************************************************************************)
-open Coqlib
open SmtMisc
@@ -25,12 +24,12 @@ let ceq63 = gen_constant Structures.int63_modules "eqb"
let carray = gen_constant Structures.parray_modules "array"
(* is_true *)
-let cis_true = gen_constant init_modules "is_true"
+let cis_true = gen_constant Structures.init_modules "is_true"
(* nat *)
-let cnat = gen_constant init_modules "nat"
-let cO = gen_constant init_modules "O"
-let cS = gen_constant init_modules "S"
+let cnat = gen_constant Structures.init_modules "nat"
+let cO = gen_constant Structures.init_modules "O"
+let cS = gen_constant Structures.init_modules "S"
(* Positive *)
let positive_modules = [["Coq";"Numbers";"BinNums"];
@@ -75,49 +74,49 @@ let ceqbZ = gen_constant z_modules "eqb"
(* Booleans *)
let bool_modules = [["Coq";"Bool";"Bool"]]
-let cbool = gen_constant init_modules "bool"
-let ctrue = gen_constant init_modules "true"
-let cfalse = gen_constant init_modules "false"
-let candb = gen_constant init_modules "andb"
-let corb = gen_constant init_modules "orb"
-let cxorb = gen_constant init_modules "xorb"
-let cnegb = gen_constant init_modules "negb"
-let cimplb = gen_constant init_modules "implb"
+let cbool = gen_constant Structures.init_modules "bool"
+let ctrue = gen_constant Structures.init_modules "true"
+let cfalse = gen_constant Structures.init_modules "false"
+let candb = gen_constant Structures.init_modules "andb"
+let corb = gen_constant Structures.init_modules "orb"
+let cxorb = gen_constant Structures.init_modules "xorb"
+let cnegb = gen_constant Structures.init_modules "negb"
+let cimplb = gen_constant Structures.init_modules "implb"
let ceqb = gen_constant bool_modules "eqb"
let cifb = gen_constant bool_modules "ifb"
-let ciff = gen_constant init_modules "iff"
+let ciff = gen_constant Structures.init_modules "iff"
let creflect = gen_constant bool_modules "reflect"
(* Lists *)
-let clist = gen_constant init_modules "list"
-let cnil = gen_constant init_modules "nil"
-let ccons = gen_constant init_modules "cons"
-let clength = gen_constant init_modules "length"
+let clist = gen_constant Structures.init_modules "list"
+let cnil = gen_constant Structures.init_modules "nil"
+let ccons = gen_constant Structures.init_modules "cons"
+let clength = gen_constant Structures.init_modules "length"
(* Option *)
-let coption = gen_constant init_modules "option"
-let cSome = gen_constant init_modules "Some"
-let cNone = gen_constant init_modules "None"
+let coption = gen_constant Structures.init_modules "option"
+let cSome = gen_constant Structures.init_modules "Some"
+let cNone = gen_constant Structures.init_modules "None"
(* Pairs *)
-let cpair = gen_constant init_modules "pair"
-let cprod = gen_constant init_modules "prod"
+let cpair = gen_constant Structures.init_modules "pair"
+let cprod = gen_constant Structures.init_modules "prod"
(* Dependent pairs *)
-let csigT = gen_constant init_modules "sigT"
-(* let cprojT1 = gen_constant init_modules "projT1" *)
-(* let cprojT2 = gen_constant init_modules "projT2" *)
-(* let cprojT3 = gen_constant init_modules "projT3" *)
+let csigT = gen_constant Structures.init_modules "sigT"
+(* let cprojT1 = gen_constant Structures.init_modules "projT1" *)
+(* let cprojT2 = gen_constant Structures.init_modules "projT2" *)
+(* let cprojT3 = gen_constant Structures.init_modules "projT3" *)
-(* let csigT2 = gen_constant init_modules "sigT2" *)
-(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *)
+(* let csigT2 = gen_constant Structures.init_modules "sigT2" *)
+(* let csigT_of_sigT2 = gen_constant Structures.init_modules "sigT_of_sigT2" *)
(* Logical Operators *)
-let cnot = gen_constant init_modules "not"
-let ceq = gen_constant init_modules "eq"
-let crefl_equal = gen_constant init_modules "eq_refl"
-let cconj = gen_constant init_modules "conj"
-let cand = gen_constant init_modules "and"
+let cnot = gen_constant Structures.init_modules "not"
+let ceq = gen_constant Structures.init_modules "eq"
+let crefl_equal = gen_constant Structures.init_modules "eq_refl"
+let cconj = gen_constant Structures.init_modules "conj"
+let cand = gen_constant Structures.init_modules "and"
(* Bit vectors *)
let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 080d6c6..f626a96 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) =
let tf = Hashtbl.create 17 in
let rec interp = function
| [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
- | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
+ | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
interp prem
@@ -689,7 +689,7 @@ let gen_rel_name =
let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
let warn () =
- Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr (Structures.extern_constr clemma))));
+ Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (Structures.extern_constr clemma))));
None
in
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 4e11709..3d56b6a 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -80,11 +80,11 @@ module type FORM =
val clear : reify -> unit
val get : ?declare:bool -> reify -> pform -> t
- (** Give a coq term, build the corresponding formula *)
+ (** Given a coq term, build the corresponding formula *)
val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
val hash_hform : (hatom -> hatom) -> reify -> t -> t
- (** Flattening of [Fand] and [For], removing of [Fnot2] *)
+ (* Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
(** Turn n-ary [Fand] and [For] into their right-associative
@@ -100,10 +100,10 @@ module type FORM =
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> Structures.constr * Structures.constr
val nvars : reify -> int
- (** Producing a Coq term corresponding to the interpretation
- of a formula *)
- (** [interp_atom] map [hatom] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation
+ of a formula *)
+ (* [interp_atom] map [hatom] to coq term, it is better if it produce
+ shared terms. *)
val interp_to_coq :
(hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
t -> Structures.constr
@@ -589,9 +589,9 @@ module Make (Atom:ATOM) =
(mkInt i, Structures.mkArray (Lazy.force cform, t))
let nvars reify = reify.count
- (** Producing a Coq term corresponding to the interpretation of a formula *)
- (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation of a formula *)
+ (* [interp_atom] map [Atom.t] to coq term, it is better if it produce
+ shared terms. *)
let interp_to_coq interp_atom form_tbl f =
let rec interp_form f =
let l = to_lit f in
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index ad7d2ca..fead657 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -97,10 +97,10 @@ module type FORM =
val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
val interp_tbl : reify -> Structures.constr * Structures.constr
val nvars : reify -> int
- (** Producing a Coq term corresponding to the interpretation
- of a formula *)
- (** [interp_atom] map [hatom] to coq term, it is better if it produce
- shared terms. *)
+ (* Producing a Coq term corresponding to the interpretation
+ of a formula *)
+ (* [interp_atom] map [hatom] to coq term, it is better if it produce
+ shared terms. *)
val interp_to_coq :
(hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
t -> Structures.constr
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 41c741d..0b6eeaa 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -46,7 +46,7 @@ type logic_item =
module SL = Set.Make (struct
type t = logic_item
- let compare = Pervasives.compare
+ let compare = Stdlib.compare
end)
type logic = SL.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index f397826..ef017a7 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -159,7 +159,7 @@ let order_roots init_index first =
r := n
| _ -> failwith "root value has unexpected form" end
done;
- let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc
+ let _, lr = List.sort (fun (i1, _) (i2, _) -> Stdlib.compare i1 i2) !acc
|> List.split in
let link_to c1 c2 =
let curr_id = c2.id -1 in
@@ -476,7 +476,7 @@ let to_coq to_lit interp (cstep,
let concl' = out_cl [concl] in
let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in
let app_var = Structures.mkVar app_name in
- let app_ty = Term.mkArrow clemma (interp ([], [concl])) in
+ let app_ty = Structures.mkArrow clemma (interp ([], [concl])) in
cuts := (app_name, app_ty)::!cuts;
mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
end
generated by cgit (git 2.34.1) at 2024-07-01 02:27:23 +0000