Permalink
Browse files

Code cleaning & factorizing functions in Equality.

  • Loading branch information...
1 parent e681d58 commit 3507f3d81082f5f4aef165cc3f4b0207224fb0cb @ppedrot ppedrot committed May 9, 2014
Showing with 26 additions and 40 deletions.
  1. +14 −26 tactics/equality.ml
  2. +9 −4 tactics/tactics.ml
  3. +3 −10 tactics/tactics.mli
View
@@ -138,15 +138,14 @@ let side_tac tac sidetac =
| None -> tac
| Some sidetac -> tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac
-let instantiate_lemma_all frzevars env gl c ty l l2r concl =
+let instantiate_lemma_all frzevars gl c ty l l2r concl =
+ let env = Proofview.Goal.env gl in
let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
- let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
- let rec split_last_two = function
- | [c1;c2] -> [],(c1, c2)
- | x::y::z ->
- let l,res = split_last_two (y::z) in x::l, res
- | _ -> error "The term provided is not an applied relation." in
- let others,(c1,c2) = split_last_two args in
+ let (equiv, args) = decompose_appvect (Clenv.clenv_type eqclause) in
+ let arglen = Array.length args in
+ let () = if arglen < 2 then error "The term provided is not an applied relation." in
+ let c1 = args.(arglen - 2) in
+ let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
clenv_pose_dependent_evars true {eqclause with evd = evd'}
in
@@ -156,7 +155,7 @@ let instantiate_lemma_all frzevars env gl c ty l l2r concl =
((if l2r then c1 else c2),concl)
in List.map try_occ occs
-let instantiate_lemma env gl c ty l l2r concl =
+let instantiate_lemma gl c ty l l2r concl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
@@ -191,20 +190,10 @@ let rewrite_conv_closed_unif_flags = {
Unification.allow_K_in_toplevel_higher_order_unification = false
}
-let rewrite_elim with_evars frzevars c e =
- Proofview.Goal.raw_enter begin fun gl ->
- let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
- let elim gl = elimination_clause_scheme with_evars ~flags gl in
- let tac gl = general_elim_clause_gen elim c e gl in
- Proofview.V82.tactic tac
- end
-
-let rewrite_elim_in with_evars frzevars id c e =
+let rewrite_elim with_evars frzevars cls c e =
Proofview.Goal.raw_enter begin fun gl ->
let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
- let elim gl = elimination_in_clause_scheme with_evars ~flags id gl in
- let tac gl = general_elim_clause_gen elim c e gl in
- Proofview.V82.tactic tac
+ general_elim_clause with_evars flags cls c e
end
(* Ad hoc asymmetric general_elim_clause *)
@@ -216,8 +205,8 @@ let general_elim_clause with_evars frzevars cls rew elim =
(* was tclWEAK_PROGRESS which only fails for tactics generating one
subgoal and did not fail for useless conditional rewritings generating
an extra condition *)
- tclNOTSAMEGOAL (rewrite_elim with_evars frzevars rew elim)
- | Some id -> rewrite_elim_in with_evars frzevars id rew elim
+ tclNOTSAMEGOAL (rewrite_elim with_evars frzevars cls rew elim)
+ | Some _ -> rewrite_elim with_evars frzevars cls rew elim
end
begin function
| PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
@@ -241,10 +230,9 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
tac
in
Proofview.Goal.raw_enter begin fun gl ->
- let env = Proofview.Goal.env gl in
let instantiate_lemma concl =
- if not all then instantiate_lemma env gl c t l l2r concl
- else instantiate_lemma_all frzevars env gl c t l l2r concl
+ if not all then instantiate_lemma gl c t l l2r concl
+ else instantiate_lemma_all frzevars gl c t l l2r concl
in
let typ = match cls with
| None -> pf_nf_concl gl
View
@@ -839,15 +839,13 @@ let general_elim_clause_gen elimtac indclause elim gl =
match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
elimtac i (elimc, elimt, lbindelimc) indclause gl
-let general_elim_clause elimtac (c,lbindc) elim gl =
+let general_elim with_evars (c, lbindc) elim gl =
+ let elimtac = elimination_clause_scheme with_evars in
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
let indclause = pf_apply make_clenv_binding gl (c, t) lbindc in
general_elim_clause_gen elimtac indclause elim gl
-let general_elim with_evars c e =
- general_elim_clause (elimination_clause_scheme with_evars) c e
-
(* Case analysis tactics *)
let general_case_analysis_in_context with_evars (c,lbindc) gl =
@@ -958,6 +956,13 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i (elim, e
(str "Nothing to rewrite in " ++ pr_id id ++ str".");
clenv_refine_in with_evars id elimclause'' gl
+let general_elim_clause with_evars flags id c e =
+ let elim gl = match id with
+ | None -> elimination_clause_scheme with_evars ~flags gl
+ | Some id -> elimination_in_clause_scheme with_evars ~flags id gl
+ in
+ Proofview.V82.tactic (fun gl -> general_elim_clause_gen elim c e gl)
+
(* Apply a tactic below the products of the conclusion of a lemma *)
type conjunction_status =
View
@@ -247,19 +247,12 @@ type eliminator = {
elimbody : constr with_bindings
}
-val elimination_clause_scheme : evars_flag -> ?flags:unify_flags ->
- int -> (constr * types * constr bindings) -> clausenv -> tactic
-
-val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags ->
- Id.t -> int -> (constr * types * constr bindings) -> clausenv -> tactic
-
-val general_elim_clause_gen :
- (int -> (constr * types * constr bindings) -> 'a -> tactic) ->
- 'a -> eliminator -> tactic
-
val general_elim : evars_flag ->
constr with_bindings -> eliminator -> tactic
+val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
+ clausenv -> eliminator -> unit Proofview.tactic
+
val default_elim : evars_flag -> constr with_bindings -> unit Proofview.tactic
val simplest_elim : constr -> unit Proofview.tactic
val elim :

0 comments on commit 3507f3d

Please sign in to comment.