diff options
Diffstat (limited to 'src/trace')
| -rw-r--r-- | src/trace/smtCommands.ml | 8 | ||||
| -rw-r--r-- | src/trace/smtMisc.ml | 11 | ||||
| -rw-r--r-- | src/trace/smt_tactic.ml4 | 6 | ||||
| -rw-r--r-- | src/trace/structures.ml | 55 |
4 files changed, 11 insertions, 69 deletions
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 1941065..52450d1 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -177,8 +177,8 @@ let build_body rt ro ra rf l b (max_id, confl) = Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], + Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], mklApp cchecker_b_correct [|vti;vtfunc;vtatom; vtform; l; b; vc; vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|]))))) @@ -209,8 +209,8 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) = Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|], Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|], Term.mkLetIn (nc, certif, Lazy.force ccertif, - Term.mkLetIn (nti, Term.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], - Term.mkLetIn (ntfunc, Term.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], + Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|], + Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|], mklApp cchecker_eq_correct [|vti;vtfunc;vtatom; vtform; l1; l2; l; vc; vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|]))))) diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 893a9be..21d81dc 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -32,15 +32,8 @@ type 'a gen_hashed = { index : int; hval : 'a } let mklApp f args = Term.mkApp (Lazy.force f, args) (* TODO : Set -> Type *) -let coqtype = lazy Term.mkSet - -let declare_new_type t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (Structures.dummy_loc,t); - Term.mkVar t - -let declare_new_variable v constr_t = - Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Structures.dummy_loc,v); - Term.mkVar v +let declare_new_type = Structures.declare_new_type +let declare_new_variable = Structures.declare_new_variable let mkName s = let id = Names.id_of_string s in diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4 index 219810d..efac23b 100644 --- a/src/trace/smt_tactic.ml4 +++ b/src/trace/smt_tactic.ml4 @@ -14,6 +14,9 @@ (**************************************************************************) +(* Uncomment for 8.5 *) +(* DECLARE PLUGIN "SMTCoq_plugin" *) + VERNAC COMMAND EXTEND Parse_certif_zchaff | [ "Parse_certif_zchaff" ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> @@ -27,7 +30,7 @@ VERNAC COMMAND EXTEND Parse_certif_zchaff | [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] -> [ Zchaff.theorem name fdimacs fproof - ] + ] END VERNAC COMMAND EXTEND Parse_certif_verit @@ -46,6 +49,7 @@ VERNAC COMMAND EXTEND Parse_certif_verit ] END +(* Comment for 8.5 *) TACTIC EXTEND zchaff | [ "zchaff" ] -> [ Zchaff.tactic ] END diff --git a/src/trace/structures.ml b/src/trace/structures.ml deleted file mode 100644 index 2c3a8d2..0000000 --- a/src/trace/structures.ml +++ /dev/null @@ -1,55 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2015 *) -(* *) -(* Michaël Armand *) -(* Benjamin Grégoire *) -(* Chantal Keller *) -(* *) -(* Inria - École Polytechnique - MSR-Inria Joint Lab *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - - -open Entries -open Coqlib - - - -let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant) - - - -(* Int63 *) -let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] - -let mkInt : int -> Term.constr = - fun i -> Term.mkInt (Uint63.of_int i) - -let cint = gen_constant int63_modules "int" - -(* PArray *) -let parray_modules = [["Coq";"Array";"PArray"]] - -let max_array_size : int = - Parray.trunc_size (Uint63.of_int 4194303) -let mkArray : Term.types * Term.constr array -> Term.constr = - Term.mkArray - - -(* Differences between the two versions of Coq *) -let dummy_loc = Pp.dummy_loc - -let mkConst c = - { const_entry_body = c; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} - -let glob_term_CbvVm = Glob_term.CbvVm None - -let error = Errors.error |