diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:46:10 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:46:10 +0200 |
commit | 3fac4bd6183b19e7980d9e0131dffa7a49f4c096 (patch) | |
tree | 626ed0a12332262a8506cd56a5d31e00aea321cb /src/trace | |
parent | a5bd782f300c3767936fc3f45df6a09cda185370 (diff) | |
download | smtcoq-3fac4bd6183b19e7980d9e0131dffa7a49f4c096.tar.gz smtcoq-3fac4bd6183b19e7980d9e0131dffa7a49f4c096.zip |
The tactic "verit" generates more user-friendly subgoals
Diffstat (limited to 'src/trace')
-rw-r--r-- | src/trace/coqTerms.ml | 4 | ||||
-rw-r--r-- | src/trace/smtAtom.ml | 25 |
2 files changed, 16 insertions, 13 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 1cc6d4f..429ed72 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -85,6 +85,9 @@ let cNone = gen_constant init_modules "None" (* Pairs *) let cpair = gen_constant init_modules "pair" +(* Dependent pairs *) +let csigT = gen_constant init_modules "sigT" + (* Logical Operators *) let cnot = gen_constant init_modules "not" let ceq = gen_constant init_modules "eq" @@ -112,7 +115,6 @@ 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" diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index bbad580..979e4e4 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -92,18 +92,19 @@ module Btype = 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 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 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 pair_ty = mklApp csigT [|eq_ty; refl_ty|] in + + reify.cuts <- (eq_name, pair_ty)::reify.cuts; let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in declare reify t ce |