diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:07:38 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:07:38 +0200 |
commit | a5bd782f300c3767936fc3f45df6a09cda185370 (patch) | |
tree | bb3c0753a54e035fec56f78edbae84485a50b878 /src/trace | |
parent | 048f0170612ee39f6bc736246fca82d960e79a18 (diff) | |
download | smtcoq-a5bd782f300c3767936fc3f45df6a09cda185370.tar.gz smtcoq-a5bd782f300c3767936fc3f45df6a09cda185370.zip |
Both native-coq and Coq 8.5 are fully supported
Diffstat (limited to 'src/trace')
-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 |
5 files changed, 34 insertions, 18 deletions
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 |