From 78167cc85a2f580691ef08ce8ccd3391158167d3 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 13 Jan 2015 18:30:16 +0100 Subject: Identify ML functions that are implemented differently in native-coq and in standard coq --- src/trace/coqTerms.ml | 2 +- src/trace/smtMisc.ml | 4 +-- src/verit/verit.ml | 58 ++++++--------------------------------- src/versions/native/structures.ml | 28 +++++++++++++++++-- src/zchaff/zchaff.ml | 25 ++++------------- 5 files changed, 42 insertions(+), 75 deletions(-) diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 8046a47..d71ba45 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -170,7 +170,7 @@ let make_certif_ops modules = gen_constant modules "LiaMicromega", gen_constant modules "LiaDiseq", gen_constant modules "SplArith", gen_constant modules "SplDistinctElim") -(** Usefull construction *) +(** Useful construction *) let ceq_refl_true = lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|]) diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 849c0d7..893a9be 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -35,11 +35,11 @@ let mklApp f args = Term.mkApp (Lazy.force f, args) 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 (Pp.dummy_loc,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 (Pp.dummy_loc,v); + Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (Structures.dummy_loc,v); Term.mkVar v let mkName s = diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 0ae0bc9..cb670c4 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -145,12 +145,7 @@ let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof = let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce4 = - { const_entry_body = certif; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce4 = Structures.mkConst certif in let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in let used_roots = compute_roots roots last_root in let roots = @@ -164,49 +159,19 @@ let parse_certif t_i t_func t_atom t_form root used_root trace fsmt fproof = let i = ref (l-1) in List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots; mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in - let ce3 = - { const_entry_body = roots; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce3 = Structures.mkConst roots in let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in - let ce3' = - { const_entry_body = used_roots; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce3' = Structures.mkConst used_roots in let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in let t_i' = make_t_i rt in let t_func' = make_t_func ro t_i' in - let ce5 = - { const_entry_body = t_i'; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce5 = Structures.mkConst t_i' in let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in - let ce6 = - { const_entry_body = t_func'; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce6 = Structures.mkConst t_func' in let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in - let ce1 = - { const_entry_body = Atom.interp_tbl ra; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce1 = Structures.mkConst (Atom.interp_tbl ra) in let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in - let ce2 = - { const_entry_body = snd (Form.interp_tbl rf); - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in () @@ -263,12 +228,7 @@ let theorem name fsmt fproof = [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3; vm_cast_true (mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in - let ce = - { const_entry_body = theorem_proof; - const_entry_type = Some theorem_concl; - const_entry_secctx = None; - const_entry_opaque = true; - const_entry_inline_code = false} in + let ce = Structures.mkConst theorem_proof in let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in () @@ -421,7 +381,7 @@ let call_verit rt ro fl root = try import_trace logfilename (Some root) with - | VeritSyntax.Sat -> Errors.error "veriT can't prove this" + | VeritSyntax.Sat -> Structures.error "veriT can't prove this" let cchecker_b_correct = diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 8f74c32..de2879c 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -13,14 +13,36 @@ (* *) (**************************************************************************) + +open Entries + + (* Int63 *) let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]] -let mkInt i = Term.mkInt (Uint63.of_int i) +let mkInt : int -> Term.constr = + fun i -> Term.mkInt (Uint63.of_int i) (* PArray *) let parray_modules = [["Coq";"Array";"PArray"]] -let max_array_size = Parray.trunc_size (Uint63.of_int 4194303) -let mkArray = Term.mkArray +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 diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 8c07fc7..e843d1f 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -200,24 +200,14 @@ let parse_certif dimacs trace fdimacs ftrace = SmtTrace.clear (); let _,first,last,reloc = import_cnf fdimacs in let d = make_roots first last in - let ce1 = - { const_entry_body = d; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce1 = Structures.mkConst d in let _ = declare_constant dimacs (DefinitionEntry ce1, IsDefinition Definition) in let max_id, confl = import_cnf_trace reloc ftrace first last in let (tres,_) = SmtTrace.to_coq (fun _ -> assert false) certif_ops confl in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce2 = - { const_entry_body = certif; - const_entry_type = None; - const_entry_secctx = None; - const_entry_opaque = false; - const_entry_inline_code = false} in + let ce2 = Structures.mkConst certif in let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in () @@ -250,12 +240,7 @@ let theorem name fdimacs ftrace = vm_cast_true (mklApp cchecker [|Term.mkRel 3(*d*); Term.mkRel 2(*c*)|]); Term.mkRel 1(*v*)|]))) in - let ce = - { const_entry_body = theorem_proof; - const_entry_type = Some theorem_type; - const_entry_secctx = None; - const_entry_opaque = true; - const_entry_inline_code = false} in + let ce = Structures.mkConst theorem_proof in let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in () @@ -273,7 +258,7 @@ let checker fdimacs ftrace = let tm = mklApp cchecker [|d; certif|] in let expr = Constrextern.extern_constr true Environ.empty_env tm in - Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some (Glob_term.CbvVm None), None, expr)) + Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some Structures.glob_term_CbvVm, None, expr)) @@ -479,7 +464,7 @@ let make_proof pform_tbl atom_tbl env reify_form l = let (reloc, resfilename, logfilename, last) = call_zchaff (Form.nvars reify_form) root in (try check_unsat resfilename with - | Sat model -> Errors.error (List.fold_left (fun acc i -> + | Sat model -> Structures.error (List.fold_left (fun acc i -> let index = if i > 0 then i-1 else -i-1 in let ispos = i > 0 in try ( -- cgit