aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/xml/proof2aproof.ml2
-rw-r--r--contrib/xml/proofTree2Xml.ml47
-rw-r--r--kernel/environ.ml29
-rw-r--r--kernel/environ.mli8
-rw-r--r--parsing/printer.ml7
-rw-r--r--parsing/tactic_printer.ml12
-rw-r--r--pretyping/evarutil.ml133
-rw-r--r--pretyping/evarutil.mli7
-rw-r--r--pretyping/evd.ml2
-rw-r--r--pretyping/evd.mli2
-rw-r--r--proofs/logic.ml249
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/proof_type.ml2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/refiner.ml79
-rw-r--r--tactics/decl_proof_instr.ml2
16 files changed, 292 insertions, 253 deletions
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 92cbf6df5..30dc7b710 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -112,8 +112,6 @@ let extract_open_proof sigma pf =
ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ;
proof_extractor vl flat_proof
- | {PT.ref=Some(PT.Change_evars,[pf])} -> (proof_extractor vl) pf
-
| {PT.ref=None;PT.goal=goal} ->
let visible_rels =
Util.map_succeed
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index dbdc79a80..9afd07a61 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -93,7 +93,7 @@ let string_of_prim_rule x = match x with
| Proof_type.ThinBody _-> "ThinBody"
| Proof_type.Move (_,_,_) -> "Move"
| Proof_type.Rename (_,_) -> "Rename"
-
+ | Proof_type.Change_evars -> "Change_evars"
let
print_proof_tree curi sigma pf proof_tree_to_constr
@@ -189,11 +189,6 @@ Pp.ppnl (Pp.(++) (Pp.str
[<(build_hyps new_hyps) ; (aux flat_proof nhyps)>]
end
- | {PT.ref=Some(PT.Change_evars,nodes)} ->
- X.xml_nempty "Change_evars" of_attribute
- (List.fold_left
- (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes)
-
| {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} ->
Util.anomaly "Not Implemented"
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 57043057a..2d821991e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -241,9 +241,9 @@ let global_vars_set env constr =
let rec filtrec acc c =
let vl = vars_of_global env c in
let acc = List.fold_right Idset.add vl acc in
- fold_constr filtrec acc c
+ fold_constr filtrec acc c
in
- filtrec Idset.empty constr
+ filtrec Idset.empty constr
(* like [global_vars] but don't get through evars *)
let global_vars_set_drop_evar env constr =
@@ -339,18 +339,6 @@ type unsafe_type_judgment = {
let compile_constant_body = Cbytegen.compile_constant_body
-(*s Special functions for the refiner (logic.ml) *)
-
-let clear_hyps ids check (ctxt,vals) =
- let ctxt,vals,rmv =
- List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) ->
- if List.mem id ids then (ctxt,vals,id::rmv)
- else begin
- check rmv d;
- (d::ctxt,v::vals,rmv)
- end) ctxt vals ([],[],[])
- in ((ctxt,vals),rmv)
-
exception Hyp_not_found
let rec apply_to_hyp (ctxt,vals) id f =
@@ -393,3 +381,16 @@ let insert_after_hyp (ctxt,vals) id d check =
| [],[] -> raise Hyp_not_found
| _, _ -> assert false
in aux ctxt vals
+
+(* To be used in Logic.clear_hyps *)
+let remove_hyps ids check (ctxt, vals) =
+ let ctxt,vals,rmv =
+ List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) ->
+ if List.mem id ids then
+ (ctxt,vals,id::rmv)
+ else
+ let nd = check d in
+ (nd::ctxt,v::vals,rmv))
+ ctxt vals ([],[],[])
+ in ((ctxt,vals),rmv)
+
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5fa5f5674..175b18b24 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -195,11 +195,6 @@ val compile_constant_body :
env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
(* opaque *) (* boxed *)
-(*s Functions for proofs/logic.ml *)
-val clear_hyps :
- variable list -> (variable list -> named_declaration -> unit) ->
- named_context_val -> named_context_val * variable list
-
exception Hyp_not_found
(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
@@ -221,3 +216,6 @@ val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
val insert_after_hyp : named_context_val -> variable ->
named_declaration ->
(named_context -> unit) -> named_context_val
+
+val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> named_context_val -> named_context_val * identifier list
+
diff --git a/parsing/printer.ml b/parsing/printer.ml
index f777a37ed..dd8264ea7 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -458,6 +458,13 @@ let pr_prim_rule = function
| Rename (id1,id2) ->
(str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)
+ | Change_evars ->
+ (* This is internal tactic and cannot be replayed at user-level.
+ Function pr_rule_dot below is used when we want to hide
+ Change_evars *)
+ str "Evar change"
+
+
(* Backwards compatibility *)
let prterm = pr_lconstr
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 5eedeec07..c2e0e27fb 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -39,11 +39,6 @@ let pr_rule = function
end
| Daimon -> str "<Daimon>"
| Decl_proof _ -> str "proof"
- | Change_evars ->
- (* This is internal tactic and cannot be replayed at user-level.
- Function pr_rule_dot below is used when we want to hide
- Change_evars *)
- str "Evar change"
let uses_default_tac = function
| Nested(Tactic(_,dflt),_) -> dflt
@@ -51,7 +46,7 @@ let uses_default_tac = function
(* Does not print change of evars *)
let pr_rule_dot = function
- | Change_evars -> mt ()
+ | Prim Change_evars -> mt ()
| r ->
pr_rule r ++ if uses_default_tac r then str "..." else str"."
@@ -189,9 +184,6 @@ let print_treescript nochange sigma pf =
((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++
prlist_with_sep pr_fnl
(print_script nochange sigma) spfl )
- | Some(Change_evars,[spf]) ->
- (if nochange then mt () else pr_change pf.goal ++ fnl ()) ++
- aux spf
| Some(r,spfl) ->
let indent = if List.length spfl >= 2 then 1 else 0 in
(if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++
@@ -202,8 +194,6 @@ let rec print_info_script sigma osign pf =
let {evar_hyps=sign; evar_concl=cl} = pf.goal in
match pf.ref with
| None -> (mt ())
- | Some(Change_evars,[spf]) ->
- print_info_script sigma osign spf
| Some(r,spfl) ->
(pr_rule r ++
match spfl with
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 207ad88b3..3c93e5882 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -57,8 +57,8 @@ let tj_nf_evar = Pretype_errors.tj_nf_evar
let nf_evar_info evc info =
{ info with
- evar_concl = Reductionops.nf_evar evc info.evar_concl;
- evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
+ evar_concl = Reductionops.nf_evar evc info.evar_concl;
+ evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
evm Evd.empty
@@ -99,7 +99,7 @@ let push_dependent_evars sigma emap =
(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
(sigma',emap') (collect_evars emap' ccl))
emap (sigma,emap)
-
+
(* replaces a mapping of existentials into a mapping of metas.
Problem if an evar appears in the type of another one (pops anomaly) *)
let evars_to_metas sigma (emap, c) =
@@ -141,12 +141,12 @@ let new_untyped_evar =
(* All ids of sign must be distincts! *)
let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance =
let ctxt = named_context_of_val sign in
- assert (List.length instance = named_context_length ctxt);
- if not (list_distinct (ids_of_named_context ctxt)) then
- anomaly "new_evar_instance: two vars have the same name";
- let newev = new_untyped_evar() in
- (evar_declare sign newev typ ~src:src evd,
- mkEvar (newev,Array.of_list instance))
+ assert (List.length instance = named_context_length ctxt);
+ if not (list_distinct (ids_of_named_context ctxt)) then
+ anomaly "new_evar_instance: two vars have the same name";
+ let newev = new_untyped_evar() in
+ (evar_declare sign newev typ ~src:src evd,
+ mkEvar (newev,Array.of_list instance))
let make_subst env args =
snd (fold_named_context
@@ -166,38 +166,38 @@ let push_rel_context_to_named_context env typ =
(* compute the instance relative to the named context *)
let vars =
fold_named_context (fun env (id,b,_) l -> mkVar id :: l) env ~init:[] in
- (* move the rel context to a named context and extend the instance
- with vars of the rel context *)
-(*
- let fv = free_rels typ in
-*)
+ (* move the rel context to a named context and extend the instance
+ with vars of the rel context *)
+ (*
+ let fv = free_rels typ in
+ *)
let avoid = ids_of_named_context (named_context env) in
let n = rel_context_length (rel_context env) in
let (subst, _, _, inst, env) =
Sign.fold_rel_context
(fun (na,c,t) (subst, n, avoid, inst, env) ->
-(*
- match na with
- | Anonymous when not (Intset.mem n fv) ->
- (dummy_var::subst, n-1, avoid, inst, env)
- | _ ->
-*)
- let id = next_name_away na avoid in
- ((mkVar id)::subst, n-1, id::avoid, mkRel n::inst,
- push_named (id,option_map (substl subst) c,substl subst t) env))
+ (*
+ match na with
+ | Anonymous when not (Intset.mem n fv) ->
+ (dummy_var::subst, n-1, avoid, inst, env)
+ | _ ->
+ *)
+ let id = next_name_away na avoid in
+ ((mkVar id)::subst, n-1, id::avoid, mkRel n::inst,
+ push_named (id,option_map (substl subst) c,substl subst t) env))
(rel_context env) ~init:([], n, avoid, vars, env) in
- (named_context_val env, substl subst typ, inst)
-
+ (named_context_val env, substl subst typ, inst)
+
let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ =
let sign,typ',instance = push_rel_context_to_named_context env typ in
- assert (not (dependent dummy_var typ));
- new_evar_instance sign evd typ' ~src:src instance
+ assert (not (dependent dummy_var typ));
+ new_evar_instance sign evd typ' ~src:src instance
-(* The same using side-effect *)
+ (* The same using side-effect *)
let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty =
let (evd',ev) = new_evar !evd env ~src:src ty in
- evd := evd';
- ev
+ evd := evd';
+ ev
(*------------------------------------*
* operations on the evar constraints *
@@ -293,33 +293,74 @@ let do_restrict_hyps env k evd ev args =
let evi = Evd.find (evars_of !evd) ev in
let hyps = evar_context evi in
let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in
- (* No care is taken in case the evar type uses vars filtered out!
- Assuming that the restriction comes from a well-typed Flex/Flex
- unification problem (see real_clean), the type of the evar cannot
- depend on variables that are not in the scope of the other evar,
- since this other evar has the same type (up to unification).
+ (* No care is taken in case the evar type uses vars filtered out!
+ Assuming that the restriction comes from a well-typed Flex/Flex
+ unification problem (see real_clean), the type of the evar cannot
+ depend on variables that are not in the scope of the other evar,
+ since this other evar has the same type (up to unification).
Since moreover, the evar contexts uses names only, the
- restriction raise no de Bruijn reallocation problem *)
+ restriction raise no de Bruijn reallocation problem *)
let env' =
Sign.fold_named_context push_named hyps' ~init:(reset_context env) in
let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in
- evd := Evd.evar_define ev nc !evd;
- let (evn,_) = destEvar nc in
- mkEvar(evn,Array.of_list ncargs)
+ evd := Evd.evar_define ev nc !evd;
+ let (evn,_) = destEvar nc in
+ mkEvar(evn,Array.of_list ncargs)
+
+let clear_evar_hyps_in_evar evd evn args ids =
+ (* Creates a new evar ev' from ev such that all ids are removed from
+ the context of ev' *)
+ (* ATTN: il faut vérifier que le type associé à ev ne dépend pas de
+ l'un des ids *)
+ let args = Array.to_list args in
+ let evi = Evd.find (evars_of !evd) evn in
+ let hyps = evar_context evi in
+ let (hyps',args') = list_filter2
+ (fun _ c -> match kind_of_term c with Var id -> not (List.mem id ids) | _ -> true)
+ (hyps,args) in
+ let env = Sign.fold_named_context push_named hyps' ~init:(empty_env) in
+ let ev' = e_new_evar evd env ~src:(evar_source evn !evd) evi.evar_concl in
+ evd := Evd.evar_define evn ev' !evd;
+ let (evn',_) = destEvar ev' in
+ mkEvar(evn',Array.of_list args')
+
+let clear_evar_hyps_in_constr evd c ids =
+ let rec aux c =
+ match kind_of_term c with
+ | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Evar (e,l) ->
+ (* aux may have defined e earlier, so we have to check *)
+ if Evd.is_defined_evar !evd (e,l) then
+ let nc = nf_evar (evars_of !evd) c in aux nc
+ else
+ clear_evar_hyps_in_evar evd e l ids
+ | _ -> map_constr aux c
+ in
+ aux c
+
+let clear_evar_hyps sigma evi ids =
+ let evd = Evd.create_evar_defs sigma in
+ let aux c = clear_evar_hyps_in_constr (ref evd) c ids in
+ let goal = evar_concl evi in
+ let hyps = evar_hyps evi in
+ ({ evi with
+ evar_concl = aux goal;
+ evar_hyps = map_named_val aux hyps}, evars_of evd)
let need_restriction k args = not (array_for_all (closedn k) args)
(* We try to instantiate the evar assuming the body won't depend
* on arguments that are not Rels or Vars, or appearing several times
- (i.e. we tackle only Miller-Pfenning patterns unification)
+ * (i.e. we tackle only Miller-Pfenning patterns unification)
- 1) Let a unification problem "env |- ev[hyps:=args] = rhs"
- 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
- where only Rel's and Var's are relevant in subst
- 3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
+ * 1) Let a unification problem "env |- ev[hyps:=args] = rhs"
+ * 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
+ * where only Rel's and Var's are relevant in subst
+ * 3) We recur on rhs, "imitating" the term failing if some Rel/Var not in scope
- Note: we don't assume rhs in normal form, it may fail while it would
- have succeeded after some reductions
+ * Note: we don't assume rhs in normal form, it may fail while it would
+ * have succeeded after some reductions
*)
(* Note: error_not_clean should not be an error: it simply means that the
* conversion test that lead to the faulty call to [real_clean] should return
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 670b74270..9ad7b6e58 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -158,3 +158,10 @@ val whd_castappevar : evar_map -> constr -> constr
val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
+
+
+(**********************************)
+(* Removing hyps in evars'context *)
+val clear_evar_hyps_in_evar : evar_defs ref -> evar -> constr array -> identifier list -> constr
+val clear_evar_hyps_in_constr : evar_defs ref -> constr -> identifier list -> constr
+val clear_evar_hyps : evar_map -> evar_info -> identifier list -> evar_info * evar_map
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index fb4321bc3..2afe4601f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -77,6 +77,8 @@ let is_defined sigma ev =
let info = find sigma ev in
not (info.evar_body = Evar_empty)
+let evar_concl ev = ev.evar_concl
+let evar_hyps ev = ev.evar_hyps
let evar_body ev = ev.evar_body
let evar_env evd = Global.env_of_context evd.evar_hyps
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b4aa5fa5e..8b9c7fc67 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -56,6 +56,8 @@ val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
+val evar_concl : evar_info -> constr
+val evar_hyps : evar_info -> Environ.named_context_val
val evar_body : evar_info -> evar_body
val evar_env : evar_info -> Environ.env
diff --git a/proofs/logic.ml b/proofs/logic.ml
index f56a92475..57b5d677f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -69,26 +69,37 @@ let with_check = Options.with_option check
(* The Clear tactic: it scans the context for hypotheses to be removed
(instead of iterating on the list of identifier to be removed, which
forces the user to give them in order). *)
-let clear_hyps ids gl =
+let clear_hyps sigma ids gl =
let env = Global.env() in
- let (nhyps,cleared_ids) =
- let fcheck cleared_ids (id,_,_ as d) =
- if !check && cleared_ids<>[] then
- Idset.iter
- (fun id' ->
- if List.mem id' cleared_ids then
- error (string_of_id id'^
- " is used in hypothesis "^string_of_id id))
- (global_vars_set_of_decl env d) in
- clear_hyps ids fcheck gl.evar_hyps in
- let ncl = gl.evar_concl in
+ let evd = ref (Evd.create_evar_defs sigma) in
+ let (nhyps, cleared_ids) =
+ let check_and_clear_in_evar_hyps (id,ob,c) =
+ let rec aux c =
+ match kind_of_term c with
+ | (Rel _ | Meta _ | Sort _ | Const _ | Ind _
+ | Construct _) -> c
+ | Var id' -> if !check && List.mem id' ids then
+ error (string_of_id id' ^ " is used in hypothesis "
+ ^ string_of_id id); mkVar id'
+ | Evar (e,l) ->
+ (* If e is already define, we replace it by its definition *)
+ if Evd.is_defined_evar !evd (e,l) then
+ let nc = nf_evar (evars_of !evd) c in aux nc
+ else
+ Evarutil.clear_evar_hyps_in_evar evd e l ids
+ | _ -> map_constr aux c
+ in
+ (id, (match ob with None -> None | Some b -> Some (aux b)), aux c)
+ in
+ remove_hyps ids check_and_clear_in_evar_hyps (evar_hyps gl) in
+ let ncl = Evarutil.clear_evar_hyps_in_constr evd (evar_concl gl) ids in
if !check && cleared_ids<>[] then
Idset.iter
(fun id' ->
if List.mem id' cleared_ids then
error (string_of_id id'^" is used in conclusion"))
- (global_vars_set_drop_evar env ncl);
- mk_goal nhyps ncl gl.evar_extra
+ (global_vars_set env ncl);
+ (mk_goal nhyps ncl gl.evar_extra, evars_of !evd)
(* The ClearBody tactic *)
@@ -216,7 +227,7 @@ let check_forward_dependencies id tail =
let check_goal_dependency id cl =
let env = Global.env() in
- if Idset.mem id (global_vars_set_drop_evar env cl) then
+ if Idset.mem id (global_vars_set env cl) then
error (string_of_id id^" is used in conclusion")
let rename_hyp id1 id2 sign =
@@ -398,6 +409,19 @@ let convert_hyp sign sigma (id,b,bt as d) =
error ("Incorrect change of the body of "^(string_of_id id));
d)
+(* Normalizing evars in a goal. Called by tactic Local_constraints
+ (i.e. when the sigma of the proof tree changes). Detect if the
+ goal is unchanged *)
+let norm_goal sigma gl =
+ let red_fun = Evarutil.nf_evar sigma in
+ let ncl = red_fun gl.evar_concl in
+ let ngl =
+ { gl with
+ evar_concl = ncl;
+ evar_hyps = map_named_val red_fun gl.evar_hyps } in
+ if Evd.eq_evar_info ngl gl then None else Some ngl
+
+
(************************************************************************)
(************************************************************************)
@@ -418,13 +442,13 @@ let prim_refiner r sigma goal =
if occur_meta c1 then error_use_instantiate();
let sg = mk_goal (push_named_context_val (id,None,c1) sign)
(subst1 (mkVar id) b) in
- [sg]
+ ([sg], sigma)
| LetIn (_,c1,t1,b) ->
if occur_meta c1 or occur_meta t1 then error_use_instantiate();
let sg =
mk_goal (push_named_context_val (id,Some c1,t1) sign)
(subst1 (mkVar id) b) in
- [sg]
+ ([sg], sigma)
| _ ->
raise (RefinerError IntroNeedsProduct))
@@ -434,12 +458,12 @@ let prim_refiner r sigma goal =
if occur_meta c1 then error_use_instantiate();
let sign' = replace_hyp sign id (id,None,c1) cl in
let sg = mk_goal sign' (subst1 (mkVar id) b) in
- [sg]
+ ([sg], sigma)
| LetIn (_,c1,t1,b) ->
if occur_meta c1 then error_use_instantiate();
let sign' = replace_hyp sign id (id,Some c1,t1) cl in
let sg = mk_goal sign' (subst1 (mkVar id) b) in
- [sg]
+ ([sg], sigma)
| _ ->
raise (RefinerError IntroNeedsProduct))
@@ -449,7 +473,7 @@ let prim_refiner r sigma goal =
if occur_meta t then error_use_instantiate();
let sg1 = mk_goal sign (nf_betaiota t) in
let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in
- if b then [sg1;sg2] else [sg2;sg1]
+ if b then ([sg1;sg2],sigma) else ([sg2;sg1], sigma)
| FixRule (f,n,rest) ->
let rec check_ind env k cl =
@@ -478,7 +502,7 @@ let prim_refiner r sigma goal =
| [] ->
List.map (fun (_,_,c) -> mk_goal sign c) all
in
- mk_sign sign all
+ (mk_sign sign all, sigma)
| Cofix (f,others) ->
let rec check_is_coind env cl =
@@ -505,47 +529,48 @@ e types")
mk_sign (push_named_context_val (f,None,ar) sign) oth)
| [] -> List.map (fun (_,c) -> mk_goal sign c) all
in
- mk_sign sign all
+ (mk_sign sign all, sigma)
| Refine c ->
if not (list_distinct (collect_meta_variables c)) then
raise (RefinerError (NonLinearProof c));
let (sgl,cl') = mk_refgoals sigma goal [] cl c in
let sgl = List.rev sgl in
- sgl
+ (sgl, sigma)
(* Conversion rules *)
| Convert_concl (cl',_) ->
check_typability env sigma cl';
if (not !check) || is_conv_leq env sigma cl' cl then
let sg = mk_goal sign cl' in
- [sg]
+ ([sg], sigma)
else
error "convert-concl rule passed non-converting term"
| Convert_hyp (id,copt,ty) ->
- [mk_goal (convert_hyp sign sigma (id,copt,ty)) cl]
+ ([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
(* And now the structural rules *)
| Thin ids ->
- [clear_hyps ids goal]
-
+ let (ngl, nsigma) = clear_hyps sigma ids goal in
+ ([ngl], nsigma)
+
| ThinBody ids ->
let clear_aux env id =
let env' = remove_hyp_body env sigma id in
- if !check then recheck_typability (None,id) env' sigma cl;
- env'
+ if !check then recheck_typability (None,id) env' sigma cl;
+ env'
in
let sign' = named_context_val (List.fold_left clear_aux env ids) in
let sg = mk_goal sign' cl in
- [sg]
+ ([sg], sigma)
| Move (withdep, hfrom, hto) ->
let (left,right,declfrom,toleft) =
split_sign hfrom hto (named_context_of_val sign) in
let hyps' =
move_after withdep toleft (left,declfrom,right) hto in
- [mk_goal hyps' cl]
+ ([mk_goal hyps' cl], sigma)
| Rename (id1,id2) ->
if !check & id1 <> id2 &&
@@ -553,7 +578,12 @@ e types")
error ((string_of_id id2)^" is already used");
let sign' = rename_hyp id1 id2 sign in
let cl' = replace_vars [id1,mkVar id2] cl in
- [mk_goal sign' cl']
+ ([mk_goal sign' cl'], sigma)
+
+ | Change_evars as r ->
+ match norm_goal sigma goal with
+ Some ngl -> ([ngl],sigma)
+ | None -> ([goal], sigma)
(************************************************************************)
(************************************************************************)
@@ -596,80 +626,83 @@ let proof_variable_index x =
let prim_extractor subfun vl pft =
let cl = pft.goal.evar_concl in
- match pft.ref with
- | Some (Prim (Intro id), [spf]) ->
- (match kind_of_term (strip_outer_cast cl) with
- | Prod (_,ty,_) ->
- let cty = subst_proof_vars vl ty in
- mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
- | LetIn (_,b,ty,_) ->
- let cb = subst_proof_vars vl b in
- let cty = subst_proof_vars vl ty in
- mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
- | _ -> error "incomplete proof!")
-
- | Some (Prim (Intro_replacing id),[spf]) ->
- (match kind_of_term (strip_outer_cast cl) with
- | Prod (_,ty,_) ->
- let cty = subst_proof_vars vl ty in
- mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
- | LetIn (_,b,ty,_) ->
- let cb = subst_proof_vars vl b in
- let cty = subst_proof_vars vl ty in
- mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
- | _ -> error "incomplete proof!")
-
- | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
- let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
- mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
- subfun (add_proof_var id vl) spf2)
-
- | Some (Prim (FixRule (f,n,others)),spfl) ->
- let all = Array.of_list ((f,n,cl)::others) in
- let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
- let names = Array.map (fun (f,_,_) -> Name f) all in
- let vn = Array.map (fun (_,n,_) -> n-1) all in
- let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
- (add_proof_var f vl) others in
- let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkFix ((vn,0),(names,lcty,lfix))
-
- | Some (Prim (Cofix (f,others)),spfl) ->
- let all = Array.of_list ((f,cl)::others) in
- let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
- let names = Array.map (fun (f,_) -> Name f) all in
- let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
- (add_proof_var f vl) others in
- let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkCoFix (0,(names,lcty,lfix))
-
- | Some (Prim (Refine c),spfl) ->
- let mvl = collect_meta_variables c in
- let metamap = List.combine mvl (List.map (subfun vl) spfl) in
- let cc = subst_proof_vars vl c in
- plain_instance metamap cc
-
- (* Structural and conversion rules do not produce any proof *)
- | Some (Prim (Convert_concl (t,k)),[pf]) ->
- if k = DEFAULTcast then subfun vl pf
- else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
- | Some (Prim (Convert_hyp _),[pf]) ->
- subfun vl pf
-
- | Some (Prim (Thin _),[pf]) ->
- (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
- subfun vl pf
-
- | Some (Prim (ThinBody _),[pf]) ->
- subfun vl pf
-
- | Some (Prim (Move _),[pf]) ->
- subfun vl pf
-
- | Some (Prim (Rename (id1,id2)),[pf]) ->
- subfun (rebind id1 id2 vl) pf
-
- | Some _ -> anomaly "prim_extractor"
-
- | None-> error "prim_extractor handed incomplete proof"
+ match pft.ref with
+ | Some (Prim (Intro id), [spf]) ->
+ (match kind_of_term (strip_outer_cast cl) with
+ | Prod (_,ty,_) ->
+ let cty = subst_proof_vars vl ty in
+ mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
+ | LetIn (_,b,ty,_) ->
+ let cb = subst_proof_vars vl b in
+ let cty = subst_proof_vars vl ty in
+ mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
+ | _ -> error "incomplete proof!")
+
+ | Some (Prim (Intro_replacing id),[spf]) ->
+ (match kind_of_term (strip_outer_cast cl) with
+ | Prod (_,ty,_) ->
+ let cty = subst_proof_vars vl ty in
+ mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
+ | LetIn (_,b,ty,_) ->
+ let cb = subst_proof_vars vl b in
+ let cty = subst_proof_vars vl ty in
+ mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
+ | _ -> error "incomplete proof!")
+
+ | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
+ let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
+ mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
+ subfun (add_proof_var id vl) spf2)
+
+ | Some (Prim (FixRule (f,n,others)),spfl) ->
+ let all = Array.of_list ((f,n,cl)::others) in
+ let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
+ let names = Array.map (fun (f,_,_) -> Name f) all in
+ let vn = Array.map (fun (_,n,_) -> n-1) all in
+ let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
+ (add_proof_var f vl) others in
+ let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+ mkFix ((vn,0),(names,lcty,lfix))
+
+ | Some (Prim (Cofix (f,others)),spfl) ->
+ let all = Array.of_list ((f,cl)::others) in
+ let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
+ let names = Array.map (fun (f,_) -> Name f) all in
+ let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
+ (add_proof_var f vl) others in
+ let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
+ mkCoFix (0,(names,lcty,lfix))
+
+ | Some (Prim (Refine c),spfl) ->
+ let mvl = collect_meta_variables c in
+ let metamap = List.combine mvl (List.map (subfun vl) spfl) in
+ let cc = subst_proof_vars vl c in
+ plain_instance metamap cc
+
+ (* Structural and conversion rules do not produce any proof *)
+ | Some (Prim (Convert_concl (t,k)),[pf]) ->
+ if k = DEFAULTcast then subfun vl pf
+ else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
+ | Some (Prim (Convert_hyp _),[pf]) ->
+ subfun vl pf
+
+ | Some (Prim (Thin _),[pf]) ->
+ (* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
+ subfun vl pf
+
+ | Some (Prim (ThinBody _),[pf]) ->
+ subfun vl pf
+
+ | Some (Prim (Move _),[pf]) ->
+ subfun vl pf
+
+ | Some (Prim (Rename (id1,id2)),[pf]) ->
+ subfun (rebind id1 id2 vl) pf
+
+ | Some (Prim Change_evars, [pf]) ->
+ subfun vl pf
+
+ | Some _ -> anomaly "prim_extractor"
+
+ | None-> error "prim_extractor handed incomplete proof"
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 4af70cfb7..081d02f37 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -34,7 +34,7 @@ val with_check : tactic -> tactic
(* The primitive refiner. *)
-val prim_refiner : prim_rule -> evar_map -> goal -> goal list
+val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
type proof_variable
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 5c9d2406e..20ce39775 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -39,6 +39,7 @@ type prim_rule =
| ThinBody of identifier list
| Move of bool * identifier * identifier
| Rename of identifier * identifier
+ | Change_evars
type proof_tree = {
open_subgoals : int;
@@ -50,7 +51,6 @@ and rule =
| Nested of compound_rule * proof_tree
| Decl_proof of bool
| Daimon
- | Change_evars
and compound_rule=
| Tactic of tactic_expr * bool
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 9c82239ef..f835e2ef4 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -39,6 +39,7 @@ type prim_rule =
| ThinBody of identifier list
| Move of bool * identifier * identifier
| Rename of identifier * identifier
+ | Change_evars
(* The type [goal sigma] is the type of subgoal. It has the following form
\begin{verbatim}
@@ -84,7 +85,6 @@ and rule =
| Nested of compound_rule * proof_tree
| Decl_proof of bool
| Daimon
- | Change_evars
and compound_rule=
(* the boolean of Tactic tells if the default tactic is used *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ff74d89d3..a03e0b9e6 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -68,18 +68,6 @@ let descend n p =
else
error "Too few subproofs"
-(* Normalizing evars in a goal. Called by tactic Local_constraints
- (i.e. when the sigma of the proof tree changes). Detect if the
- goal is unchanged *)
-let norm_goal sigma gl =
- let red_fun = Evarutil.nf_evar sigma in
- let ncl = red_fun gl.evar_concl in
- let ngl =
- { gl with
- evar_concl = ncl;
- evar_hyps = map_named_val red_fun gl.evar_hyps } in
- if Evd.eq_evar_info ngl gl then None else Some ngl
-
(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
gives
@@ -192,11 +180,11 @@ let abstract_operation syntax semantics gls =
let (sgl_sigma,validation) = semantics gls in
let hidden_proof = validation (List.map leaf sgl_sigma.it) in
(sgl_sigma,
- fun spfl ->
- assert (check_subproof_connection sgl_sigma.it spfl);
- { open_subgoals = and_status (List.map pf_status spfl);
- goal = gls.it;
- ref = Some(Nested(syntax,hidden_proof),spfl)})
+ fun spfl ->
+ assert (check_subproof_connection sgl_sigma.it spfl);
+ { open_subgoals = and_status (List.map pf_status spfl);
+ goal = gls.it;
+ ref = Some(Nested(syntax,hidden_proof),spfl)})
let abstract_tactic_expr ?(dflt=false) te tacfun gls =
abstract_operation (Tactic(te,dflt)) tacfun gls
@@ -210,14 +198,14 @@ let abstract_extended_tactic ?(dflt=false) s args =
let refiner = function
| Prim pr as r ->
let prim_fun = prim_refiner pr in
- (fun goal_sigma ->
- let sgl = prim_fun goal_sigma.sigma goal_sigma.it in
- ({it=sgl; sigma = goal_sigma.sigma},
- (fun spfl ->
- assert (check_subproof_connection sgl spfl);
- { open_subgoals = and_status (List.map pf_status spfl);
- goal = goal_sigma.it;
- ref = Some(r,spfl) })))
+ (fun goal_sigma ->
+ let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
+ ({it=sgl; sigma = sigma'},
+ (fun spfl ->
+ assert (check_subproof_connection sgl spfl);
+ { open_subgoals = and_status (List.map pf_status spfl);
+ goal = goal_sigma.it;
+ ref = Some(r,spfl) })))
| Nested (_,_) | Decl_proof _ ->
@@ -234,44 +222,23 @@ let refiner = function
goal = gls.it;
ref = Some(Daimon,[])})
- (* [Local_constraints lc] makes the local constraints be [lc] and
- normalizes evars *)
-
- | Change_evars as r ->
- (fun goal_sigma ->
- let gl = goal_sigma.it in
- (match norm_goal goal_sigma.sigma gl with
- Some ngl ->
- ({it=[ngl];sigma=goal_sigma.sigma},
- (fun spfl ->
- assert (check_subproof_connection [ngl] spfl);
- { open_subgoals = (List.hd spfl).open_subgoals;
- goal = gl;
- ref = Some(r,spfl) }))
- (* if the evar change does not affect the goal, leave the
- proof tree unchanged *)
- | None -> ({it=[gl];sigma=goal_sigma.sigma},
- (fun spfl ->
- assert (List.length spfl = 1);
- List.hd spfl))))
-
-
-let local_Constraints gl = refiner Change_evars gl
+
+let local_Constraints gl = refiner (Prim Change_evars) gl
let norm_evar_tac = local_Constraints
let norm_evar_proof sigma pf =
let nf_subgoal i sgl =
let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
- v (List.map leaf gll.it) in
- frontier_mapi nf_subgoal pf
+ v (List.map leaf gll.it) in
+ frontier_mapi nf_subgoal pf
(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
- takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
- where pfterm is the constr corresponding to the proof
- and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
- where the mi are metavariables numbers, and ci are their types.
- Their proof should be completed in order to complete the initial proof *)
+ takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
+ where pfterm is the constr corresponding to the proof
+ and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
+ where the mi are metavariables numbers, and ci are their types.
+ Their proof should be completed in order to complete the initial proof *)
let extract_open_proof sigma pf =
let next_meta =
@@ -291,8 +258,6 @@ let extract_open_proof sigma pf =
let flat_proof = v spfl in
proof_extractor vl flat_proof
- | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf
-
| {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
| {ref=(None|Some(Daimon,[]));goal=goal} ->
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 244cb288e..4ac92fbae 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -54,7 +54,7 @@ let tcl_change_info_gen info_gen =
[pftree] ->
{pftree with
goal=gl;
- ref=Some (Change_evars,[pftree])}
+ ref=Some (Prim Change_evars,[pftree])}
| _ -> anomaly "change_info : Wrong number of subtrees")
let tcl_change_info info gls = tcl_change_info_gen (Some (pm_in info)) gls
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 19:52:27 +0000