diff options
-rw-r--r-- | src/SMT_terms.v | 16 | ||||
-rw-r--r-- | src/trace/coqTerms.ml | 2 | ||||
-rw-r--r-- | src/trace/smtAtom.ml | 33 | ||||
-rw-r--r-- | src/trace/smtAtom.mli | 2 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 11 | ||||
-rw-r--r-- | src/trace/smt_tactic.ml4 | 4 | ||||
-rw-r--r-- | src/verit/verit.ml | 4 | ||||
-rw-r--r-- | src/verit/veritSyntax.ml | 2 | ||||
-rw-r--r-- | src/versions/native/structures.ml | 12 | ||||
-rw-r--r-- | src/versions/standard/structures.ml | 14 | ||||
-rw-r--r-- | unit-tests/Tests_verit.v | 32 |
11 files changed, 91 insertions, 41 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 2d16d3e..6c5ba27 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -234,6 +234,22 @@ Record typ_eqb : Type := Typ_eqb { te_reflect : forall x y, reflect (x = y) (te_eqb x y) }. +Section Typ_eqb_param. + + Variable A : Type. + + Record typ_eqb_param : Type := Typ_eqb_param { + te_eqb_param : A -> A -> bool; + te_reflect_param : forall x y, reflect (x = y) (te_eqb_param x y) + }. + + Variable r : typ_eqb_param. + + Definition typ_eqb_of_typ_eqb_param := + Typ_eqb A (te_eqb_param r) (te_reflect_param r). + +End Typ_eqb_param. + (* Common used types into which we interpret *) (* Unit *) diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index e8a7737..1cc6d4f 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -112,6 +112,8 @@ let ctyp_eqb = gen_constant smt_modules "typ_eqb" let cTyp_eqb = gen_constant smt_modules "Typ_eqb" let cte_carrier = gen_constant smt_modules "te_carrier" let cte_eqb = gen_constant smt_modules "te_eqb" +let ctyp_eqb_param = gen_constant smt_modules "typ_eqb_param" +let ctyp_eqb_of_typ_eqb_param = gen_constant smt_modules "typ_eqb_of_typ_eqb_param" let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb" let ctval = gen_constant smt_modules "tval" diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index 80c012f..bbad580 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -61,7 +61,8 @@ module Btype = (* reify table *) type reify_tbl = { mutable count : int; - tbl : (Term.constr, btype) Hashtbl.t + tbl : (Term.constr, btype) Hashtbl.t; + mutable cuts : (Structures.names_id_t * Term.types) list } let create () = @@ -70,7 +71,10 @@ module Btype = Hashtbl.add htbl (Lazy.force cbool) Tbool; (* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *) { count = 0; - tbl = htbl } + tbl = htbl; + cuts = [] } + + let get_cuts reify = reify.cuts let declare reify t typ_eqb = (* TODO: allows to have only typ_eqb *) @@ -84,14 +88,23 @@ module Btype = try Hashtbl.find reify.tbl t with | Not_found -> - let eq_t = declare_new_variable (Names.id_of_string "eq") (Term.mkArrow t (Term.mkArrow t (Lazy.force cbool))) in - let x = mkName "x" in - let y = mkName "y" in - let rx = Term.mkRel 2 in - let ry = Term.mkRel 1 in - let eq_refl = Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|];mklApp (lazy eq_t) [|rx;ry|]|])) in - let eq_refl_v = declare_new_variable (Names.id_of_string ("eq_refl")) eq_refl in - let ce = mklApp cTyp_eqb [|t;eq_t;eq_refl_v|] in + let n = string_of_int (List.length reify.cuts) in + let eq_name = Names.id_of_string ("eq"^n) in + let eq_var = Term.mkVar eq_name in + + (* let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in *) + + (* let eq = mkName "eq" in *) + (* let x = mkName "x" in *) + (* let y = mkName "y" in *) + (* let req = Term.mkRel 3 in *) + (* let rx = Term.mkRel 2 in *) + (* let ry = Term.mkRel 1 in *) + (* let eq_refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in *) + + let eq_ty = mklApp ctyp_eqb_param [|t|] in + reify.cuts <- (eq_name, eq_ty)::reify.cuts; + let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in declare reify t ce let interp_tbl reify = diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli index 9b8a613..fd0a30c 100644 --- a/src/trace/smtAtom.mli +++ b/src/trace/smtAtom.mli @@ -48,6 +48,8 @@ module Btype : val interp_to_coq : reify_tbl -> btype -> Term.constr + val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list + end (** Operators *) diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index 53ea75c..b019f24 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -230,11 +230,7 @@ let make_proof call_solver rt ro rf l = call_solver rt ro fl (root,l) -let tactic call_solver rt ro ra rf gl = - let env = Tacmach.pf_env gl in - let sigma = Tacmach.project gl in - let t = Tacmach.pf_concl gl in - +let tactic call_solver rt ro ra rf env sigma t = let (forall_let, concl) = Term.decompose_prod_assum t in let env = Environ.push_rel_context forall_let env in let a, b = get_arguments concl in @@ -253,4 +249,7 @@ let tactic call_solver rt ro ra rf gl = let compose_lam_assum forall_let body = List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in let res = compose_lam_assum forall_let body in - Tactics.exact_no_check res gl + let cuts = Btype.get_cuts rt in + List.fold_right (fun (eqn, eqt) tac -> + Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac + ) cuts (Structures.vm_cast_no_check res) diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4 index c3cae79..a1f8790 100644 --- a/src/trace/smt_tactic.ml4 +++ b/src/trace/smt_tactic.ml4 @@ -51,9 +51,9 @@ END TACTIC EXTEND Tactic_zchaff -| [ "zchaff" ] -> [ Structures.mk_tactic Zchaff.tactic ] +| [ "zchaff" ] -> [ Structures.mk_sat_tactic Zchaff.tactic ] END TACTIC EXTEND Tactic_verit -| [ "verit" ] -> [ Structures.mk_tactic Verit.tactic ] +| [ "verit" ] -> [ Structures.mk_smt_tactic Verit.tactic ] END diff --git a/src/verit/verit.ml b/src/verit/verit.ml index 3a1abc0..d2db93e 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -149,10 +149,10 @@ let call_verit rt ro fl root = | VeritSyntax.Sat -> Structures.error "veriT can't prove this" -let tactic gl = +let tactic env sigma t = clear_all (); let rt = Btype.create () in let ro = Op.create () in let ra = VeritSyntax.ra in let rf = VeritSyntax.rf in - SmtCommands.tactic call_verit rt ro ra rf gl + SmtCommands.tactic call_verit rt ro ra rf env sigma t diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml index 3ff11e9..33c059d 100644 --- a/src/verit/veritSyntax.ml +++ b/src/verit/veritSyntax.ml @@ -136,7 +136,7 @@ let mkCongrPred p = Other (EqCgrP (p_p,c,cert)) else failwith "VeritSyntax.mkCongrPred: unmatching predicates" | _ -> failwith "VeritSyntax.mkCongrPred : not pred app") - |_ -> failwith "VeritSyntax.mkCongr: no or more than one predicate app premice in congruence") + |_ -> failwith "VeritSyntax.mkCongr: no or more than one predicate app premise in congruence") |[] -> failwith "VeritSyntax.mkCongrPred: no conclusion in congruence" |_ -> failwith "VeritSyntax.mkCongrPred: more than one conclusion in congruence" diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml index 62907d1..919f2f1 100644 --- a/src/versions/native/structures.ml +++ b/src/versions/native/structures.ml @@ -41,6 +41,8 @@ let mkArray : Term.types * Term.constr array -> Term.constr = (* Differences between the two versions of Coq *) +type names_id_t = Names.identifier + let dummy_loc = Pp.dummy_loc let mkConst c = @@ -71,4 +73,12 @@ let pr_constr_env = Printer.pr_constr_env let lift = Term.lift -let mk_tactic t = t +let mk_sat_tactic tac = tac +let tclTHENLAST = Tacticals.tclTHENLAST +let assert_before = Tactics.assert_tac +let vm_cast_no_check = Tactics.vm_cast_no_check +let mk_smt_tactic tac gl = + let env = Tacmach.pf_env gl in + let sigma = Tacmach.project gl in + let t = Tacmach.pf_concl gl in + tac env sigma t gl diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 93546b3..66106a6 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -64,6 +64,8 @@ let mkArray : Term.types * Term.constr array -> Term.constr = (* Differences between the two versions of Coq *) +type names_id_t = Names.Id.t + let dummy_loc = Loc.ghost let mkConst c = @@ -101,4 +103,14 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty let lift = Vars.lift -let mk_tactic = Proofview.V82.tactic +let mk_sat_tactic = Proofview.V82.tactic +let tclTHENLAST = Tacticals.New.tclTHENLAST +let assert_before = Tactics.assert_before +let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t) +let mk_smt_tactic tac = + Proofview.Goal.nf_enter (fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let t = Proofview.Goal.concl gl in + tac env sigma t + ) diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v index 7e356bb..e63bbaf 100644 --- a/unit-tests/Tests_verit.v +++ b/unit-tests/Tests_verit.v @@ -842,25 +842,21 @@ Proof. verit. Qed. -Section Concrete. - Goal forall (i j:int), +Goal forall (i j:int), (i == j) && (negb (i == j)) = false. - Proof. - verit. - Qed. -End Concrete. - -Section Concrete2. - Lemma concrete2 : forall i j, (i == j) || (negb (i == j)). - Proof. - verit. - Qed. - Check concrete2. -End Concrete2. -Check concrete2. - - -(* Congruence in which some premices are REFL *) +Proof. + verit. + econstructor; eexact Int63Properties.reflect_eqb. +Qed. + +Goal forall i j, (i == j) || (negb (i == j)). +Proof. + verit. + econstructor; eexact Int63Properties.reflect_eqb. +Qed. + + +(* Congruence in which some premises are REFL *) Goal forall (f:Z -> Z -> Z) x y z, implb (Zeq_bool x y) (Zeq_bool (f z x) (f z y)). |