diff options
Diffstat (limited to 'src/trace')
-rw-r--r-- | src/trace/coqTerms.ml | 67 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 4 | ||||
-rw-r--r-- | src/trace/smtForm.ml | 18 | ||||
-rw-r--r-- | src/trace/smtForm.mli | 8 | ||||
-rw-r--r-- | src/trace/smtMisc.ml | 2 | ||||
-rw-r--r-- | src/trace/smtTrace.ml | 4 |
6 files changed, 51 insertions, 52 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 65995b5..c6188b8 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 9cfc7c4..fa2a56b 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 a86fe8a..7f2ebd8 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 e3c3859..06a867f 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 2080a64..d750550 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 876e420..65994f9 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 |