From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- proofs/evar_refiner.ml | 181 ++++++------------------------------------------- 1 file changed, 21 insertions(+), 160 deletions(-) (limited to 'proofs/evar_refiner.ml') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ac4dd43a..4ee8001c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,183 +6,44 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_refiner.ml,v 1.36.2.2 2004/08/03 21:37:27 herbelin Exp $ *) +(* $Id: evar_refiner.ml 8654 2006-03-22 15:36:58Z msozeau $ *) -open Pp open Util open Names open Term -open Environ open Evd open Sign -open Reductionops -open Typing -open Instantiate -open Tacred open Proof_trees -open Proof_type -open Logic open Refiner -open Tacexpr -open Nameops - - -type wc = named_context sigma (* for a better reading of the following *) - -let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal -let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it - -type w_tactic = named_context sigma -> named_context sigma - -let startWalk gls = - let evc = project_with_focus gls in - (evc, - (fun wc' gls' -> - if not !Options.debug or (gls.it = gls'.it) then -(* if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then*) - tclIDTAC {it=gls'.it; sigma = (get_gc wc')} -(* else - (local_Constraints (get_focus (ids_it wc')) - {it=gls'.it; sigma = get_gc (ids_it wc')})*) - else error "Walking")) - -let extract_decl sp evc = - let evdmap = evc.sigma in - let evd = Evd.map evdmap sp in - { it = evd.evar_hyps; - sigma = Evd.rmv evdmap sp } - -let restore_decl sp evd evc = - (rc_add evc (sp,evd)) - - -(* [w_Focusing sp wt wc] - * - * Focuses the walking context WC onto the declaration SP, given that - * this declaration is UNDEFINED. Then, it runs the walking_tactic, - * WT, on this new context. When the result is returned, we recover - * the resulting focus (access list) and restore it to SP's declaration. - * - * It is an error to cause SP to change state while we are focused on it. *) - -(* let w_Focusing_THEN sp (wt : 'a result_w_tactic) (wt' : 'a -> w_tactic) - (wc : named_context sigma) = - let hyps = wc.it - and evd = Evd.map wc.sigma sp in - let (wc' : named_context sigma) = extract_decl sp wc in - let (wc'',rslt) = wt wc' in -(* if not (ids_eq wc wc'') then error "w_saving_focus"; *) - if wc'==wc'' then - wt' rslt wc - else - let wc''' = restore_decl sp evd wc'' in - wt' rslt {it = hyps; sigma = wc'''.sigma} *) - -let w_add_sign (id,t) (wc : named_context sigma) = - { it = Sign.add_named_decl (id,None,t) wc.it; - sigma = wc.sigma } - -let w_Focus sp wc = extract_decl sp wc - -let w_Underlying wc = wc.sigma -let w_whd wc c = Evarutil.whd_castappevar (w_Underlying wc) c -let w_type_of wc c = - type_of (Global.env_of_context wc.it) wc.sigma c -let w_env wc = get_env wc -let w_hyps wc = named_context (get_env wc) -let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k -let w_const_value wc = constant_value (w_env wc) -let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n -let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c -let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c - - -let w_Declare sp ty (wc : named_context sigma) = - let _ = w_type_of wc ty in (* Utile ?? *) - let sign = get_hyps wc in - let newdecl = mk_goal sign ty in - ((rc_add wc (sp,newdecl)): named_context sigma) - -let w_Define sp c wc = - let spdecl = Evd.map (w_Underlying wc) sp in - let cty = - try - w_type_of (w_Focus sp wc) (mkCast (c,spdecl.evar_concl)) - with - Not_found -> error "Instantiation contains unlegal variables" - | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> - errorlabstrm "w_Define" - (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ - str (string_of_existential sp)) - in - match spdecl.evar_body with - | Evar_empty -> - let spdecl' = { evar_hyps = spdecl.evar_hyps; - evar_concl = spdecl.evar_concl; - evar_body = Evar_defined c } - in - Proof_trees.rc_add wc (sp,spdecl') - | _ -> error "define_evar" - (******************************************) (* Instantiation of existential variables *) (******************************************) -(* The instantiate tactic *) +(* w_tactic pour instantiate *) -let evars_of evc c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) when Evd.in_dom evc n -> c :: acc - | _ -> fold_constr evrec acc c - in - evrec [] c +let w_refine env ev rawc evd = + if Evd.is_defined (evars_of evd) ev then + error "Instantiate called on already-defined evar"; + let e_info = Evd.map (evars_of evd) ev in + let env = Evd.evar_env e_info in + let sigma,typed_c = + Pretyping.Default.understand_tcc (evars_of evd) env + ~expected_type:e_info.evar_concl rawc in + evar_define ev typed_c (evars_reset_evd sigma evd) -let instantiate n c ido gl = - let wc = Refiner.project_with_focus gl in - let evl = - match ido with - None -> evars_of wc.sigma gl.it.evar_concl - | Some (id,_,_) -> - let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in - evars_of wc.sigma typ in - if List.length evl < n then error "not enough evars"; - let (n,_) as k = destEvar (List.nth evl (n-1)) in - if Evd.is_defined wc.sigma n then - error "Instantiate called on already-defined evar"; - let wc' = w_Define n c wc in - tclIDTAC {it = gl.it ; sigma = wc'.sigma} - -let pfic gls c = - let evc = gls.sigma in - Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c - -(* -let instantiate_tac = function - | [Integer n; Command com] -> - (fun gl -> instantiate n (pfic gl com) gl) - | [Integer n; Constr c] -> - (fun gl -> instantiate n c gl) - | _ -> invalid_arg "Instantiate called with bad arguments" -*) - -(* vernac command existential *) +(* vernac command Existential *) let instantiate_pf_com n com pfts = let gls = top_goal_of_pftreestate pfts in - let wc = project_with_focus gls in - let sigma = (w_Underlying wc) in - let (sp,evd) = + let sigma = gls.sigma in + let (sp,evi) (* as evc *) = try - List.nth (Evd.non_instantiated sigma) (n-1) + List.nth (Evarutil.non_instantiated sigma) (n-1) with Failure _ -> - error "not so many uninstantiated existential variables" - | Invalid_argument _ -> error "incorrect existential variable index" - in - let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in - let wc' = w_Define sp c wc in - let newgc = (w_Underlying wc') in - change_constraints_pftreestate newgc pfts - - + error "not so many uninstantiated existential variables" in + let env = Evd.evar_env evi in + let rawc = Constrintern.intern_constr sigma env com in + let evd = create_evar_defs sigma in + let evd' = w_refine env sp rawc evd in + change_constraints_pftreestate (evars_of evd') pfts -- cgit v1.2.3