From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- proofs/evar_refiner.ml | 187 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 187 insertions(+) create mode 100644 proofs/evar_refiner.ml (limited to 'proofs/evar_refiner.ml') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml new file mode 100644 index 00000000..d59ff835 --- /dev/null +++ b/proofs/evar_refiner.ml @@ -0,0 +1,187 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) + +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 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 *) + +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) = + try + List.nth (Evd.non_instantiated sigma) (n-1) + with Failure _ -> + error "not so many uninstantiated existential variables" + 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 + + -- cgit v1.2.3