From 1aa3a9cb2171de7a68d00fb4c30b81c8d2689979 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Sat, 30 Apr 2016 19:54:54 +0200 Subject: Bring back the nice printing of automatically generated theorems --- src/trace/smtCommands.ml | 16 ++++++++-------- src/versions/native/structures.ml | 9 ++++++++- src/versions/standard/structures.ml | 16 +++++++++++++++- src/zchaff/zchaff.ml | 6 +++--- 4 files changed, 34 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 87ea41f..5e984a4 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -84,19 +84,19 @@ let interp_conseq_uf (prem, concl) = let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) = let t_i' = make_t_i rt in - let ce5 = Structures.mkConst t_i' in + let ce5 = Structures.mkUConst t_i' in let ct_i = Term.mkConst (declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition)) in let t_func' = make_t_func ro ct_i in - let ce6 = Structures.mkConst t_func' in + let ce6 = Structures.mkUConst t_func' in let ct_func = Term.mkConst (declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition)) in let t_atom' = Atom.interp_tbl ra in - let ce1 = Structures.mkConst t_atom' in + let ce1 = Structures.mkUConst t_atom' in let ct_atom = Term.mkConst (declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition)) in let t_form' = snd (Form.interp_tbl rf) in - let ce2 = Structures.mkConst t_form' in + let ce2 = Structures.mkUConst t_form' in let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in let (tres, last_root, _) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl false in @@ -112,14 +112,14 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, 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 = Structures.mkConst roots in + let ce3 = Structures.mkUConst roots in let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in - let ce3' = Structures.mkConst used_roots in + let ce3' = Structures.mkUConst used_roots in let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in let certif = mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce4 = Structures.mkConst certif in + let ce4 = Structures.mkUConst certif in let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in () @@ -180,7 +180,7 @@ let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) = vm_cast_true (mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))) in - let ce = Structures.mkConst theorem_proof in + let ce = Structures.mkTConst theorem_proof theorem_concl in let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in () diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 6eb1991..51e14d6 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -45,13 +45,20 @@ type names_id_t = Names.identifier let dummy_loc = Pp.dummy_loc -let mkConst c = +let mkUConst c = { const_entry_body = c; const_entry_type = None; const_entry_secctx = None; const_entry_opaque = false; const_entry_inline_code = false} +let mkTConst c ty = + { const_entry_body = c; + const_entry_type = Some ty; + const_entry_secctx = None; + const_entry_opaque = false; + const_entry_inline_code = false} + let error = Errors.error let coqtype = lazy Term.mkSet diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 74c484a..26a8cc1 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -68,7 +68,7 @@ type names_id_t = Names.Id.t let dummy_loc = Loc.ghost -let mkConst c = +let mkUConst c = let env = Global.env () in let evd = Evd.from_env env in let evd, ty = Typing.type_of env evd c in @@ -82,6 +82,20 @@ let mkConst c = const_entry_opaque = false; const_entry_inline_code = false } +let mkTConst c ty = + let env = Global.env () in + let evd = Evd.from_env env in + let evd, _ = Typing.type_of env evd c in + { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty), + Safe_typing.empty_private_constants); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some ty; + const_entry_polymorphic = false; + const_entry_universes = snd (Evd.universe_context evd); + const_entry_opaque = false; + const_entry_inline_code = false } + let error = Errors.error let coqtype = Future.from_val Term.mkSet diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 20b5463..523bd1d 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -200,14 +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 = Structures.mkConst d in + let ce1 = Structures.mkUConst 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) (fun _ -> assert false) certif_ops confl false in let certif = mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in - let ce2 = Structures.mkConst certif in + let ce2 = Structures.mkUConst certif in let _ = declare_constant trace (DefinitionEntry ce2, IsDefinition Definition) in () @@ -240,7 +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 = Structures.mkConst theorem_proof in + let ce = Structures.mkTConst theorem_proof theorem_type in let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in () -- cgit