diff options
Diffstat (limited to 'src/zchaff/zchaff.ml')
-rw-r--r-- | src/zchaff/zchaff.ml | 55 |
1 files changed, 40 insertions, 15 deletions
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index 2f08d99..bd656aa 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -368,12 +368,22 @@ let build_body reify_atom reify_form l b (max_id, confl) = let vtvar = Term.mkRel 3 in let vtform = Term.mkRel 2 in let vc = Term.mkRel 1 in - Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], - Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, - mklApp cchecker_b_correct - [|vtvar; vtform; l; b; vc; - vm_cast_true (mklApp cchecker_b [|vtform;l;b;vc|])|]))) + let proof_cast = + Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, Lazy.force ccertif, + mklApp cchecker_b_correct + [|vtvar; vtform; l; b; vc; + vm_cast_true (mklApp cchecker_b [|vtform;l;b;vc|])|]))) + in + let proof_nocast = + Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, Lazy.force ccertif, + mklApp cchecker_b_correct + [|vtvar; vtform; l; b; vc|]))) + in + (proof_cast, proof_nocast) let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) = @@ -389,12 +399,22 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) = let vtvar = Term.mkRel 3 in let vtform = Term.mkRel 2 in let vc = Term.mkRel 1 in - Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], - Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], - Term.mkLetIn (nc, certif, Lazy.force ccertif, - mklApp cchecker_eq_correct - [|vtvar; vtform; l1; l2; l; vc; - vm_cast_true (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])|]))) + let proof_cast = + Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, Lazy.force ccertif, + mklApp cchecker_eq_correct + [|vtvar; vtform; l1; l2; l; vc; + vm_cast_true (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])|]))) + in + let proof_nocast = + Term.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|], + Term.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|], + Term.mkLetIn (nc, certif, Lazy.force ccertif, + mklApp cchecker_eq_correct + [|vtvar; vtform; l1; l2; l; vc|]))) + in + (proof_cast, proof_nocast) let get_arguments concl = let f, args = Term.decompose_app concl in @@ -501,7 +521,7 @@ let tactic env sigma t = let a, b = get_arguments concl in let reify_atom = Atom.create () in let reify_form = Form.create () in - let body = + let (body_cast, body_nocast) = if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then let l = Form.of_coq (Atom.get reify_atom) reify_form a in let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in @@ -519,7 +539,12 @@ let tactic env sigma t = build_body_eq reify_atom reify_form (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in + 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 - Structures.vm_cast_no_check res + let res_cast = compose_lam_assum forall_let body_cast in + let res_nocast = compose_lam_assum forall_let body_nocast in + + (Structures.tclTHEN + (Structures.set_evars_tac res_nocast) + (Structures.vm_cast_no_check res_cast)) |