diff options
| -rw-r--r-- | proofs/goal.ml | 93 | ||||
| -rw-r--r-- | proofs/goal.mli | 5 | ||||
| -rw-r--r-- | proofs/proofview.ml | 27 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 41 |
5 files changed, 39 insertions, 131 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index dea704a68..b0fccc42f 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -125,9 +125,6 @@ let partition_unifiable sigma l = (*** Goal tactics ***) -(* Goal tactics are [subgoal sensitive]-s *) -type subgoals = { subgoals: goal list } - (* type of the base elements of the goal API.*) (* it has an extra evar_info with respect to what would be expected, it is supposed to be the evar_info of the goal in the evar_map. @@ -153,96 +150,6 @@ let bind e f = (); fun env rdefs goal info -> let r = f a in r env rdefs goal info -(* Type of constr with holes used by refine. *) -(* The list of evars doesn't necessarily contain all the evars in the constr, - only those the constr has introduced. *) -(* The variables in [myevars] are supposed to be stored - in decreasing order. Breaking this invariant might cause - many things to go wrong. *) -type refinable = { - me: constr; - my_evars: Evd.evar list -} - -module Refinable = struct - - let make t = (); fun env rdefs gl info -> - let r = ref [] in - let me = t r in - let me = me env rdefs gl info in - { me = me; my_evars = !r } - - (* [with_type c typ] constrains term [c] to have type [typ]. *) - let with_type t typ = (); fun env rdefs _ _ -> - (* spiwack: this function assumes that no evars can be created during - this sort of coercion. - If it is not the case it could produce bugs. We would need to add a handle - and add the new evars to it. *) - let my_type = Retyping.get_type_of env !rdefs t in - let j = Environ.make_judge t my_type in - let (new_defs,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env !rdefs j typ - in - rdefs := new_defs; - j'.Environ.uj_val - - (* a pessimistic (i.e : there won't be many positive answers) filter - over evar_maps, acting only on undefined evars *) - let evar_map_filter_undefined f evm = - let fold ev evi accu = if f ev evi then ev :: accu else accu in - (** We rely on the LTR order of fold here... *) - Evar.Map.fold fold (Evd.undefined_map evm) [] - - (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *) - let rec fusion l1 l2 = match l1 , l2 with - | [] , _ -> l2 - | _ , [] -> l1 - | a::l1 , b::_ when a > b -> a::(fusion l1 l2) - | a::l1 , b::l2 when Evar.equal a b -> a::(fusion l1 l2) - | _ , b::l2 -> b::(fusion l1 l2) - - let update_handle handle init_defs post_defs = - (* [delta_list] holds the evars that have been introduced by this - refinement (but not immediatly solved) *) - let filter ev _ = not (Evd.mem init_defs ev) in - (* spiwack: this is the hackish part, don't know how to do any better though. *) - let delta_list = evar_map_filter_undefined filter post_defs in - (* The variables in [myevars] are supposed to be stored - in decreasing order. Breaking this invariant might cause - many things to go wrong. *) - handle := fusion delta_list !handle - - let constr_of_open_constr handle check_type (evars, c) = (); fun env rdefs gl info -> - let () = update_handle handle !rdefs evars in - rdefs := Evd.fold (fun ev evi evd -> if not (Evd.mem !rdefs ev) then Evd.add evd ev evi else evd) evars !rdefs; - if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info - else c - -end - -(* [refine t] takes a refinable term and use it as a partial proof for current - goal. *) -let refine step = (); fun env rdefs gl info -> - (* subgoals to return *) - (* The evars in [my_evars] are stored in reverse order. - It is expectingly better however to display the goal - in increasing order. *) - rdefs := Evarconv.consider_remaining_unif_problems env !rdefs ; - let subgoals = List.map (descendent gl) (List.rev step.my_evars) in - (* creates the new [evar_map] by defining the evar of the current goal - as being [refine_step]. *) - let new_defs = Evd.define gl.content (step.me) !rdefs in - rdefs := new_defs; - (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *) - let subgoals = - Option.List.flatten (List.map (advance !rdefs) subgoals) - in - { subgoals = subgoals } - -let refine_open_constr c = - let pf h = Refinable.constr_of_open_constr h true c in - bind (Refinable.make pf) refine - let enter f = (); fun env rdefs gl info -> let sigma = !rdefs in f env sigma (Evd.evar_concl info) gl diff --git a/proofs/goal.mli b/proofs/goal.mli index 4b85ec20b..4d4d0c2eb 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -120,9 +120,6 @@ end (*** Goal tactics. DEPRECATED. ***) -(* Goal tactics are [subgoal sensitive]-s *) -type subgoals = private { subgoals: goal list } - (* Goal sensitive values *) type +'a sensitive @@ -131,8 +128,6 @@ val eval : 'a sensitive -> Environ.env -> Evd.evar_map -> goal -> 'a * Evd.evar_map -val refine_open_constr : Evd.open_constr -> subgoals sensitive - (* [enter] combines [env], [defs], [hyps] and [concl] in a single primitive. *) val enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive diff --git a/proofs/proofview.ml b/proofs/proofview.ml index e63db14ab..931d4a2b3 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -545,33 +545,6 @@ let tclNEWGOALS gls = { step with comb = step.comb @ gls } end -(* No backtracking can happen here, hence, as opposed to the dispatch tacticals, - everything is done in one step. *) -let sensitive_on_proofview s env step = - let wrap g ((defs, partial_list) as partial_res) = - match Goal.advance defs g with - | None -> partial_res - | Some g -> - let { Goal.subgoals = sg } , d' = Goal.eval s env defs g in - (d', sg::partial_list) - in - let ( new_defs , combed_subgoals ) = - List.fold_right wrap step.comb (step.solution,[]) - in - { solution = new_defs; comb = List.flatten combed_subgoals; } - -let tclSENSITIVE s = - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let (>>=) = Proof.bind in - Proof.current >>= fun env -> - Proof.get >>= fun step -> - try - let next = sensitive_on_proofview s env step in - Proof.set next - with e when catchable_exception e -> - let e = Errors.push e in - tclZERO e - let tclPROGRESS t = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in diff --git a/proofs/proofview.mli b/proofs/proofview.mli index cdc2db796..a1213cde2 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -235,10 +235,6 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact backtracking in another. *) val tclINDEPENDENT : unit tactic -> unit tactic -(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*) -val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic - - (* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *) val tclPROGRESS : 'a tactic -> 'a tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f14810482..d06d78165 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4203,6 +4203,38 @@ module Simple = struct end + +(* [with_type c typ] constrains term [c] to have type [typ]. *) +let with_type t typ env sigma = + (* spiwack: this function assumes that no evars can be created during + this sort of coercion. + If it is not the case it could produce bugs. We would need to add a handle + and add the new evars to it. *) + let my_type = Retyping.get_type_of env sigma t in + let j = Environ.make_judge t my_type in + let (sigma, j') = + Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j typ + in + (sigma, j'.Environ.uj_val) + +let update_handle handle init_defs post_defs = + let filter ev _ = not (Evd.mem init_defs ev) in + let fold ev evi accu = if filter ev evi then Evar.Set.add ev accu else accu in + Evd.fold_undefined fold post_defs handle + +let constr_of_open_constr handle (evars, c) env sigma concl = + let () = handle := update_handle !handle sigma evars in + let fold ev evi evd = if not (Evd.mem sigma ev) then Evd.add evd ev evi else evd in + let sigma = Evd.fold fold evars sigma in + with_type c concl env sigma + +let refine_open_constr c env sigma concl = + let handle = ref Evar.Set.empty in + let sigma, pf = constr_of_open_constr handle c env sigma concl in + let sigma = Evarconv.consider_remaining_unif_problems env sigma in + let subgoals = List.map Goal.build (Evar.Set.elements !handle) in + (subgoals, pf, sigma) + (** Tacticals defined directly in term of Proofview *) module New = struct open Proofview.Notations @@ -4214,8 +4246,13 @@ module New = struct let refine c = Proofview.Goal.nf_enter begin fun gl -> - let pf = Goal.refine_open_constr c in - Proofview.tclSENSITIVE pf <*> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let concl = Proofview.Goal.concl gl in + let (gls, pf, sigma) = refine_open_constr c env sigma concl in + Proofview.V82.tclEVARS sigma <*> + Proofview.Refine.refine ~unsafe:true (fun h -> (h, pf)) <*> + Proofview.tclNEWGOALS gls <*> Proofview.V82.tactic (reduce (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) {onhyps=None; concl_occs=AllOccurrences } |