From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- proofs/clenv.ml | 31 +++++++--------- proofs/clenv.mli | 2 +- proofs/clenvtac.ml | 12 +++--- proofs/clenvtac.mli | 7 ++-- proofs/evar_refiner.ml | 8 ++-- proofs/goal.ml | 25 ++++--------- proofs/goal.mli | 5 +-- proofs/goal_select.ml | 68 ++++++++++++++++++++++++++++++++++ proofs/goal_select.mli | 26 +++++++++++++ proofs/logic.ml | 97 +++++++++++++++++++++++++++++++++++++++---------- proofs/logic.mli | 15 +++++++- proofs/miscprint.ml | 12 +----- proofs/miscprint.mli | 7 +--- proofs/pfedit.ml | 52 ++++++++++++++++---------- proofs/pfedit.mli | 9 +++-- proofs/proof.ml | 45 +++++++++++++++++++++++ proofs/proof.mli | 6 +++ proofs/proof_bullet.ml | 68 ++++++---------------------------- proofs/proof_bullet.mli | 19 +++++----- proofs/proof_global.ml | 35 ++++++++---------- proofs/proof_global.mli | 18 +++++---- proofs/proofs.mllib | 1 + proofs/redexpr.ml | 15 ++++---- proofs/refine.ml | 51 ++++++++++---------------- proofs/refiner.mli | 3 ++ proofs/tacmach.ml | 8 ++-- proofs/tacmach.mli | 5 ++- proofs/tactypes.ml | 54 +++++++++++++++++++++++++++ 28 files changed, 453 insertions(+), 251 deletions(-) create mode 100644 proofs/goal_select.ml create mode 100644 proofs/goal_select.mli create mode 100644 proofs/tactypes.ml (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 03ff580a..95e908c4 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -13,8 +13,8 @@ open CErrors open Util open Names open Nameops -open Term open Termops +open Constr open Namegen open Environ open Evd @@ -26,7 +26,7 @@ open Tacred open Pretype_errors open Evarutil open Unification -open Misctypes +open Tactypes (******************************************************************) (* Clausal environments *) @@ -62,9 +62,6 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause -let mk_freelisted c = - map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c)) - let clenv_push_prod cl = let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in let rec clrec typ = match EConstr.kind cl.evd typ with @@ -73,7 +70,7 @@ let clenv_push_prod cl = let mv = new_meta () in let dep = not (noccurn (cl_sigma cl) 1 u) in let na' = if dep then na else Anonymous in - let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in + let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in { templval = mk_freelisted def; @@ -107,8 +104,7 @@ let clenv_environments evd bound t = let mv = new_meta () in let dep = not (noccurn evd 1 t2) in let na' = if dep then na else Anonymous in - let t1 = EConstr.Unsafe.to_constr t1 in - let e' = meta_declare mv t1 ~name:na' e in + let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t) @@ -167,13 +163,13 @@ let clenv_assign mv rhs clenv = user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then - if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then + if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then error_incompatible_inst clenv mv else clenv else let st = (Conv,TypeNotProcessed) in - {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} + {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} with Not_found -> user_err Pp.(str "clenv_assign: undefined meta") @@ -218,7 +214,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right @@ -288,11 +284,11 @@ let adjust_meta_source evd mv = function in situations like "ex_intro (fun x => P) ?ev p" *) let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) -> if Metaset.mem mv t.freemetas then - let f,l = decompose_app evd (EConstr.of_constr t.rebus) in + let f,l = decompose_app evd t.rebus in match EConstr.kind evd f with | Meta mv'' -> (match meta_opt_fvalue evd mv'' with - | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l + | Some (c,_) -> match_name c.rebus l | None -> None) | _ -> None else None in @@ -502,7 +498,6 @@ let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in - let c = EConstr.Unsafe.to_constr c in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } let clenv_match_args bl clenv = @@ -515,7 +510,7 @@ let clenv_match_args bl clenv = (fun clenv {CAst.loc;v=(b,c)} -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then - if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv + if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else clenv_assign_binding clenv k c) @@ -580,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma let pr_clenv clenv = h 0 - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ - str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ + (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ + str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) (****************************************************************) @@ -677,7 +672,7 @@ let define_with_type sigma env ev c = let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in let (ev, _) = destEvar sigma ev in - let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in + let sigma = Evd.define ev j.Environ.uj_val sigma in sigma let solve_evar_clause env sigma hyp_only clause = function diff --git a/proofs/clenv.mli b/proofs/clenv.mli index b85c4fc5..f9506290 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -18,7 +18,7 @@ open Environ open Evd open EConstr open Unification -open Misctypes +open Tactypes (** {6 The Type of Constructions clausale environments.} *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 209104ac..544175c6 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -10,7 +10,7 @@ open Util open Names -open Term +open Constr open Termops open Evd open EConstr @@ -54,7 +54,7 @@ let clenv_cast_meta clenv = let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) -let clenv_pose_dependent_evars with_evars clenv = +let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then @@ -75,12 +75,12 @@ let check_tc evd = let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in (has_typeclass, !has_resolvable) -let clenv_refine with_evars ?(with_classes=true) clenv = +let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> - let clenv = clenv_pose_dependent_evars with_evars clenv in + let clenv = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then let (has_typeclass, has_resolvable) = check_tc clenv.evd in @@ -105,10 +105,10 @@ open Unification let dft = default_unify_flags -let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = +let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = Proofview.Goal.enter begin fun gl -> let clenv = clenv_unique_resolver ~flags clenv gl in - clenv_refine with_evars ~with_classes clenv + clenv_refine ?with_evars ~with_classes clenv end (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 7c1e300b..d1784784 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -13,12 +13,11 @@ open Clenv open EConstr open Unification -open Misctypes (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic -val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic -val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic +val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic +val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic -val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv +val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0d197c92..c80f370f 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,8 +25,6 @@ open Ltac_pretype type glob_constr_ltac_closure = ltac_var_map * glob_constr let depends_on_evar sigma evk _ (pbty,_,t1,t2) = - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in try Evar.equal (head_evar sigma t1) evk with NoHeadEvar -> try Evar.equal (head_evar sigma t2) evk @@ -35,12 +33,12 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) = let define_and_solve_constraints evk c env evd = if Termops.occur_evar evd evk c then Pretype_errors.error_occur_check env evd evk c; - let evd = define evk (EConstr.Unsafe.to_constr c) evd in + let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) + | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 | UnifFailure _ as x -> x) (Success evd) pbs with @@ -59,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags - env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc + env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err ?loc diff --git a/proofs/goal.ml b/proofs/goal.ml index ba7e458f..c14c0a8a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -48,7 +48,7 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - EConstr.of_constr evi.Evd.evar_concl + evi.Evd.evar_concl (* Access to ".evar_extra" *) let extra evars gl = @@ -61,7 +61,6 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) - let concl = EConstr.Unsafe.to_constr concl in let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; @@ -86,7 +85,7 @@ module V82 = struct if not (Evarutil.occur_evar_upto sigma evk c) then () else Pretype_errors.error_occur_check Environ.empty_env sigma evk c in - Evd.define evk (EConstr.Unsafe.to_constr c) sigma + Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = @@ -100,7 +99,9 @@ module V82 = struct let same_goal evars1 gl1 evars2 gl2 = let evi1 = Evd.find evars1 gl1 in let evi2 = Evd.find evars2 gl2 in - Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl && + let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in + let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in + Constr.equal c1 c2 && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps let weak_progress glss gls = @@ -117,20 +118,6 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl extra_hyps = - let evi = Evd.find sigma gl in - let hyps = evi.Evd.evar_hyps in - let new_hyps = - List.fold_right Environ.push_named_context_val extra_hyps hyps in - let filter = evi.Evd.evar_filter in - let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in - let new_evi = - { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in - let new_evi = Typeclasses.mark_unresolvable new_evi in - let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = sigma; } - (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = Evd.find sigma gl in @@ -156,3 +143,5 @@ module V82 = struct ) ~init:(concl sigma gl) env end + +module Set = Set.Make(struct type t = goal let compare = Evar.compare end) diff --git a/proofs/goal.mli b/proofs/goal.mli index dc986315..a033d6da 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -64,9 +64,6 @@ module V82 : sig (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool - (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma - (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map @@ -74,3 +71,5 @@ module V82 : sig val abstract_type : Evd.evar_map -> goal -> EConstr.types end + +module Set : sig include Set.S with type elt = goal end diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml new file mode 100644 index 00000000..65a94a2c --- /dev/null +++ b/proofs/goal_select.ml @@ -0,0 +1,68 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Pp.str "!" + | SelectAll -> Pp.str "all" + | SelectNth i -> Pp.int i + | SelectList l -> + Pp.(str "[" + ++ prlist_with_sep pr_comma pr_range_selector l + ++ str "]") + | SelectId id -> Names.Id.print id + +let parse_goal_selector = function + | "!" -> SelectAlreadyFocused + | "all" -> SelectAll + | i -> + let err_msg = "The default selector must be \"all\" or a natural number." in + begin try + let i = int_of_string i in + if i < 0 then CErrors.user_err Pp.(str err_msg); + SelectNth i + with Failure _ -> CErrors.user_err Pp.(str err_msg) + end + +let _ = let open Goptions in + declare_string_option + { optdepr = false; + optname = "default goal selector" ; + optkey = ["Default";"Goal";"Selector"] ; + optread = begin fun () -> + Pp.string_of_ppcmds + (pr_goal_selector !default_goal_selector) + end; + optwrite = begin fun n -> + default_goal_selector := parse_goal_selector n + end + } diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli new file mode 100644 index 00000000..b1c57238 --- /dev/null +++ b/proofs/goal_select.mli @@ -0,0 +1,26 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Pp.t +val get_default_goal_selector : unit -> t diff --git a/proofs/logic.ml b/proofs/logic.ml index e5294715..613581ad 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -23,7 +23,6 @@ open Typing open Proof_type open Type_errors open Retyping -open Misctypes module NamedDecl = Context.Named.Declaration @@ -63,6 +62,7 @@ let is_unification_error = function let catchable_exception = function | CErrors.UserError _ | TypeError _ + | Notation.NumeralNotationError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ (* reduction errors *) @@ -185,6 +185,22 @@ let check_decl_position env sigma sign d = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" + let move_location_eq m1 m2 = match m1, m2 with | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2 @@ -236,7 +252,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = (first, d::middle) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ - Miscprint.pr_move_location Id.print hto ++ + pr_move_location Id.print hto ++ str (if toleft then ": it occurs in the type of " else ": it depends on ") ++ Id.print hyp ++ str ".") else @@ -289,7 +305,15 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | (App _| Case _) -> Constr.fold (collrec deep) acc c + | Case(ci,p,c,br) -> + (* Hack assuming only two situations: the legacy one that branches, + if with Metas, are Meta, and the new one with eta-let-expanded + branches *) + let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in + Array.fold_left (collrec deep) + (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c) + br + | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c in @@ -301,9 +325,10 @@ let check_meta_variables env sigma c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in - if b then evm - else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in + match ans with + | Some evm -> evm + | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -387,12 +412,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma, rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -440,12 +460,7 @@ and mk_hdgoals sigma goal goalacc trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -483,7 +498,7 @@ and mk_arggoals sigma goal goalacc funty allargs = let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in - Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs + Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in @@ -497,6 +512,50 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') +and treat_case sigma goal ci lbrty lf acc' = + let rec strip_outer_cast c = match kind c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c in + let decompose_app_vect c = match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) in + let env = Goal.V82.env sigma goal in + Array.fold_left3 + (fun (lacc,sigma,bacc) ty fi l -> + if isMeta (strip_outer_cast fi) then + (* Support for non-eta-let-expanded Meta as found in *) + (* destruct/case with an non eta-let expanded elimination scheme *) + let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in + r,s,(fi'::bacc) + else + (* Deal with a branch in expanded form of the form + Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as + if it were not so, so as to preserve compatibility with when + destruct/case generated schemes of the form + Case(ci,p,c,[|Meta;...;Meta|]; + CAUTION: it does not deal with the general case of eta-zeta + reduced branches having a form different from Meta, as it + would be theoretically the case with third-party code *) + let n = List.length l in + let ctx, body = Term.decompose_lam_n_decls n fi in + let head, args = decompose_app_vect body in + (* Strip cast because clenv_cast_meta adds a cast when the branch is + eta-expanded but when not when the branch has the single-meta + form [Meta] *) + let head = strip_outer_cast head in + if isMeta head then begin + assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); + let head' = lift (-n) head in + let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in + let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in + (r,s,fi'::bacc) + end + else + (* Supposed to be meta-free *) + let sigma, t'ty = goal_type_of env sigma fi in + let sigma = check_conv_leq_goal env sigma fi t'ty ty in + (lacc,sigma,fi::bacc)) + (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in diff --git a/proofs/logic.mli b/proofs/logic.mli index dc471bb5..9db54732 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +val pr_move_location : + ('a -> Pp.t) -> 'a move_location -> Pp.t + val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Evd.evar_map -> - EConstr.named_declaration -> Id.t Misctypes.move_location -> + EConstr.named_declaration -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index 1a63ff67..ec17b807 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -10,7 +10,7 @@ open Pp open Names -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with | IntroNaming p -> pr_intro_pattern_naming p | IntroAction p -> pr_intro_pattern_action prc p -and pr_intro_pattern_naming = function +and pr_intro_pattern_naming = let open Namegen in function | IntroIdentifier id -> Id.print id | IntroFresh id -> str "?" ++ Id.print id | IntroAnonymous -> str "?" @@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - (** Printing of bindings *) let pr_binding prc = let open CAst in function | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index 79790a27..f4e2e683 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -18,13 +18,10 @@ val pr_intro_pattern : val pr_or_and_intro_pattern : ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t +val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t (** Printing of [move_location] *) -val pr_move_location : - ('a -> Pp.t) -> 'a move_location -> Pp.t - val pr_bindings : ('a -> Pp.t) -> ('a -> Pp.t) -> 'a bindings -> Pp.t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 5d137988..e6507332 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -51,23 +51,22 @@ let _ = CErrors.register_handler begin function | _ -> raise CErrors.Unhandled end -let get_nth_V82_goal i = - let p = Proof_global.give_me_the_proof () in +let get_nth_V82_goal p i = let goals,_,_,_,sigma = Proof.proof p in try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal -let get_goal_context_gen i = - let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in +let get_goal_context_gen p i = + let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = - try get_goal_context_gen i + try get_goal_context_gen (Proof_global.give_me_the_proof ()) i with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = - try get_goal_context_gen 1 + try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1 with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, @@ -75,14 +74,18 @@ let get_current_goal_context () = let env = Global.env () in (Evd.from_env env, env) -let get_current_context () = - try get_goal_context_gen 1 +let get_current_context ?p () = + let current_proof_by_default = function + | Some p -> p + | None -> Proof_global.give_me_the_proof () + in + try get_goal_context_gen (current_proof_by_default p) 1 with Proof_global.NoCurrentProof -> let env = Global.env () in (Evd.from_env env, env) | NoSuchGoal -> (* No more focused goals ? *) - let p = Proof_global.give_me_the_proof () in + let p = (current_proof_by_default p) in let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) @@ -100,11 +103,23 @@ let solve ?with_end_tac gi info_lvl tac pr = | None -> tac | Some _ -> Proofview.Trace.record_info_trace tac in - let tac = match gi with - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac - | Vernacexpr.SelectAll -> tac + let tac = let open Goal_select in match gi with + | SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if n == 1 then tac + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + Proofview.tclZERO e + + | SelectNth i -> Proofview.tclFOCUS i i tac + | SelectList l -> Proofview.tclFOCUSLIST l tac + | SelectId id -> Proofview.tclFOCUSID id tac + | SelectAll -> tac in let tac = if use_unification_heuristics () then @@ -121,7 +136,7 @@ let solve ?with_end_tac gi info_lvl tac pr = with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") -let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) +let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) @@ -161,7 +176,7 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in - let univs = UState.merge side_eff Evd.univ_rigid univs ctx in + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in cb, status, univs let refine_by_tactic env sigma ty tac = @@ -188,8 +203,7 @@ let refine_by_tactic env sigma ty tac = | [c, _] -> c | _ -> assert false in - let ans = Reductionops.nf_evar sigma ans in - let ans = EConstr.Unsafe.to_constr ans in + let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) @@ -233,7 +247,7 @@ let apply_implicit_tactic tac = (); fun env sigma evk -> (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in (try - let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in let c = EConstr.of_constr c in if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, ctx) = diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 65cde3a3..5feb5bd6 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -24,7 +24,7 @@ open Decl_kinds proof of mutually dependent theorems) *) val start_proof : - Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> + Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -60,7 +60,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env If there is no pending proof then it returns the current global environment and empty evar_map. *) -val get_current_context : unit -> Evd.evar_map * env +val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env (** [current_proof_statement] *) @@ -75,7 +75,7 @@ val current_proof_statement : tac] applies [tac] to all subgoals. *) val solve : ?with_end_tac:unit Proofview.tactic -> - Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> + Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current @@ -85,6 +85,9 @@ val solve : ?with_end_tac:unit Proofview.tactic -> val by : unit Proofview.tactic -> bool +(** Option telling if unification heuristics should be used. *) +val use_unification_heuristics : unit -> bool + (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th diff --git a/proofs/proof.ml b/proofs/proof.ml index 51e0a1d6..8bbd82bb 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -63,6 +63,7 @@ exception CannotUnfocusThisWay (* Cannot focus on non-existing subgoals *) exception NoSuchGoals of int * int +exception NoSuchGoal of Names.Id.t exception FullyUnfocused @@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) + | NoSuchGoal id -> + CErrors.user_err + ~hdr:"Focus" + Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -230,6 +235,37 @@ let focus cond inf i pr = try _focus cond (Obj.repr inf) i i pr with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i)) +(* Focus on the goal named id *) +let focus_id cond inf id pr = + let (focused_goals, evar_map) = Proofview.proofview pr.proofview in + begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with + | Some ev -> + begin match CList.safe_index Evar.equal ev focused_goals with + | Some i -> + (* goal is already under focus *) + _focus cond (Obj.repr inf) i i pr + | None -> + if CList.mem_f Evar.equal ev pr.shelf then + (* goal is on the shelf, put it in focus *) + let proofview = Proofview.unshelve [ev] pr.proofview in + let shelf = + CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf + in + let pr = { pr with proofview; shelf } in + let (focused_goals, _) = Proofview.proofview pr.proofview in + let i = + (* Now we know that this will succeed *) + try CList.index Evar.equal ev focused_goals + with Not_found -> assert false + in + _focus cond (Obj.repr inf) i i pr + else + raise CannotUnfocusThisWay + end + | None -> + raise (NoSuchGoal id) + end + let rec unfocus kind pr () = let cond = cond_of_focus pr in match test_cond cond kind pr.proofview with @@ -452,3 +488,12 @@ module V82 = struct { pr with proofview ; shelf } end + +let all_goals p = + let add gs set = + List.fold_left (fun s g -> Goal.Set.add g s) set gs in + let (goals,stack,shelf,given_up,_) = proof p in + let set = add goals Goal.Set.empty in + let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in + let set = add shelf set in + add given_up set diff --git a/proofs/proof.mli b/proofs/proof.mli index c0e832fb..511dcc2e 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition a need for it? *) val focus : 'a focus_condition -> 'a -> int -> t -> t +(* focus on goal named id *) +val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t + exception FullyUnfocused exception CannotUnfocusThisWay @@ -207,3 +210,6 @@ module V82 : sig (* Implements the Existential command *) val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end + +(* returns the set of all goals in the proof *) +val all_goals : t -> Goal.Set.t diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index e22d382f..cc3e79f8 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -10,19 +10,22 @@ open Proof -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int let bullet_eq b1 b2 = match b1, b2 with -| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 -| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 -| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 +| Dash n1, Dash n2 -> n1 = n2 +| Star n1, Star n2 -> n1 = n2 +| Plus n1, Plus n2 -> n1 = n2 | _ -> false let pr_bullet b = match b with - | Vernacexpr.Dash n -> Pp.(str (String.make n '-')) - | Vernacexpr.Star n -> Pp.(str (String.make n '*')) - | Vernacexpr.Plus n -> Pp.(str (String.make n '+')) + | Dash n -> Pp.(str (String.make n '-')) + | Star n -> Pp.(str (String.make n '*')) + | Plus n -> Pp.(str (String.make n '+')) type behavior = { @@ -195,52 +198,5 @@ let put p b = let suggest p = (!current_behavior).suggest p -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - - -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (Vernacexpr.SelectNth 1) -let get_default_goal_selector () = !default_goal_selector - -let pr_range_selector (i, j) = - if i = j then Pp.int i - else Pp.(int i ++ str "-" ++ int j) - -let pr_goal_selector = function - | Vernacexpr.SelectAll -> Pp.str "all" - | Vernacexpr.SelectNth i -> Pp.int i - | Vernacexpr.SelectList l -> - Pp.(str "[" - ++ prlist_with_sep pr_comma pr_range_selector l - ++ str "]") - | Vernacexpr.SelectId id -> Names.Id.print id - -let parse_goal_selector = function - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in - begin try - let i = int_of_string i in - if i < 0 then CErrors.user_err Pp.(str err_msg); - Vernacexpr.SelectNth i - with Failure _ -> CErrors.user_err Pp.(str err_msg) - end - -let _ = - Goptions.(declare_string_option{optdepr = false; - optname = "default goal selector" ; - optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> - Pp.string_of_ppcmds - (pr_goal_selector !default_goal_selector) - end; - optwrite = begin fun n -> - default_goal_selector := parse_goal_selector n - end - }) - +let pr_goal_selector = Goal_select.pr_goal_selector +let get_default_goal_selector = Goal_select.get_default_goal_selector diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index ffbaa0fa..a09a7ec1 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -14,7 +14,10 @@ (* *) (**********************************************************) -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int (** A [behavior] is the data of a put function which is called when a bullet prefixes a tactic, a suggest function @@ -42,12 +45,8 @@ val register_behavior : behavior -> unit val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - +(** Deprecated *) +val pr_goal_selector : Goal_select.t -> Pp.t +[@@ocaml.deprecated "Please use [Goal_select.pr_goal_selector]"] +val get_default_goal_selector : unit -> Goal_select.t +[@@ocaml.deprecated "Please use [Goal_select.get_default_goal_selector]"] diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d6c0e334..7e250faa 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -78,11 +78,14 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * - Misctypes.lident option * + | Proved of opacity_flag * + lident option * proof_object + type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator @@ -90,11 +93,11 @@ type pstate = { pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; - section_vars : Context.Named.t option; + section_vars : Constr.named_context option; proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; - universe_decl: Univdecls.universe_decl; + universe_decl: UState.universe_decl; } type t = pstate list @@ -235,13 +238,6 @@ let activate_proof_mode mode = let disactivate_current_proof_mode () = CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) -let default_universe_decl = - let open Misctypes in - { univdecl_instance = []; - univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; - univdecl_extensible_constraints = true } - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -250,7 +246,7 @@ let default_universe_decl = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = +let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -262,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = universe_decl = pl } in push initial_state pstates -let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator = +let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -340,8 +336,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now have existential variables in the initial types of goals, we need to normalise them for the kernel. *) let subst_evar k = - Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in - let nf = Universes.nf_evars_and_universes_opt_subst subst_evar + Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst universes) in let make_body = if poly || now then @@ -352,9 +348,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now not (Safe_typing.empty_private_constants = eff)) in let typ = if allow_deferred then t else nf t in - let env = Global.env () in - let used_univs_body = Univops.universes_of_constr env body in - let used_univs_typ = Univops.universes_of_constr env typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in @@ -441,8 +436,8 @@ let return_proof ?(allow_partial=false) () = (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) - let proofs = - List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in + let proofs = + List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~feedback_id proof = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index bf35fd65..854ceaa4 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t val get_all_proof_names : unit -> Names.Id.t list -val discard : Misctypes.lident -> unit +val discard : Names.lident -> unit val discard_current : unit -> unit val discard_all : unit -> unit @@ -48,11 +48,13 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * - Misctypes.lident option * + | Proved of opacity_flag * + Names.lident option * proof_object type proof_terminator type closed_proof = proof_object * proof_terminator @@ -69,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) val start_proof : - Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl -> + Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command @@ -124,11 +126,11 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Misctypes.lident list -val get_used_variables : unit -> Context.Named.t option + Names.Id.t list -> Constr.named_context * Names.lident list +val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : unit -> Univdecls.universe_decl +val get_universe_decl : unit -> UState.universe_decl module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 058e839b..197f71ca 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -5,6 +5,7 @@ Proof_type Logic Refine Proof +Goal_select Proof_bullet Proof_global Redexpr diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6fb41193..44685d2b 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open EConstr open Declarations open Globnames @@ -23,7 +23,6 @@ open Tacred open CClosure open RedFlags open Libobject -open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = @@ -53,7 +52,7 @@ let whd_cbn flags env sigma t = Reductionops.Stack.zip ~refold:true sigma state let strong_cbn flags = - strong (whd_cbn flags) + strong_with_flags whd_cbn flags let simplIsCbn = ref (false) let _ = Goptions.declare_bool_option { @@ -92,9 +91,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - List.smartmap + List.Smart.map (fun (k,ql as entry) -> - let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj @@ -200,8 +199,8 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") - | ArgArg x -> x + | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") + | Locus.ArgArg x -> x let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) @@ -263,7 +262,7 @@ let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) let subst_red_expr subs = - Miscops.map_red_expr_gen + Redops.map_red_expr_gen (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) diff --git a/proofs/refine.ml b/proofs/refine.ml index 909556b1..198e057e 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -15,7 +15,7 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in + let ctx1 = List.rev (EConstr.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in let rec share l1 l2 accu = match l1, l2 with | d1 :: l1, d2 :: l2 -> @@ -29,47 +29,34 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = EConstr.of_constr (NamedDecl.get_type decl) in - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref t in - let () = match decl with - | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t + let t = NamedDecl.get_type decl in + let sigma, _ = Typing.sort_of env sigma t in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,body,_) -> Typing.check env sigma body t in - (!evdref, Environ.push_named decl env) + (sigma, EConstr.push_named decl env) in let (common, changed) = extract_prefix env info in - let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in - !evdref - -let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in - !evdref + let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in + sigma let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () (* Get the side-effect's constant declarations to update the monad's * environmnent *) -let add_if_undefined kn cb env = - try ignore(Environ.lookup_constant kn env); env - with Not_found -> Environ.add_constant kn cb env +let add_if_undefined env eff = + let open Entries in + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env (* Add the side effects to the monad's environment, if not already done. *) -let add_side_effect env = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - add_if_undefined kn cb env - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.fold_left (fun env (_,kn,cb,eff_env) -> - add_if_undefined kn cb env) env l - -let add_side_effects env effects = - List.fold_left (fun env eff -> add_side_effect env eff) env effects +let add_side_effects env eff = + List.fold_left add_if_undefined env eff let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in @@ -93,7 +80,7 @@ let generic_refine ~typecheck f gl = let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in + let sigma = if typecheck then Typing.check env sigma c concl else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = @@ -106,7 +93,6 @@ let generic_refine ~typecheck f gl = let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) - let c = EConstr.Unsafe.to_constr c in let sigma = match Proofview.Unsafe.advance sigma self with | None -> (** Nothing to do, the goal has been solved by side-effect *) @@ -124,7 +110,8 @@ let generic_refine ~typecheck f gl = (** Mark goals *) let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in - let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in + let trace () = Pp.(hov 2 (str"simple refine"++spc()++ + Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 5cd703a2..0f83e16e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -23,9 +23,12 @@ val pf_env : goal sigma -> Environ.env val pf_hyps : goal sigma -> named_context val unpackage : 'a sigma -> evar_map ref * 'a +[@@ocaml.deprecated "Do not use [evar_map ref]"] val repackage : evar_map ref -> 'a -> 'a sigma +[@@ocaml.deprecated "Do not use [evar_map ref]"] val apply_sig_tac : evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list +[@@ocaml.deprecated "Do not use [evar_map ref]"] val refiner : rule -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 1889054f..182b38d3 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -33,9 +33,11 @@ let re_sig it gc = { it = it; sigma = gc; } type 'a sigma = 'a Evd.sigma;; type tactic = Proof_type.tactic;; +[@@@ocaml.warning "-3"] let unpackage = Refiner.unpackage let repackage = Refiner.repackage let apply_sig_tac = Refiner.apply_sig_tac +[@@@ocaml.warning "+3"] let sig_it = Refiner.sig_it let project = Refiner.project @@ -73,7 +75,7 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -125,8 +127,8 @@ open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in - let penv = print_named_context env in - let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in + let penv = Termops.Internal.print_named_context env in + let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 770d0940..31496fb3 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -30,9 +30,12 @@ val project : goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma val unpackage : 'a sigma -> evar_map ref * 'a +[@@ocaml.deprecated "Do not use [evar_map ref]"] val repackage : evar_map ref -> 'a -> 'a sigma +[@@ocaml.deprecated "Do not use [evar_map ref]"] val apply_sig_tac : evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) +[@@ocaml.deprecated "Do not use [evar_map ref]"] val pf_concl : goal sigma -> types val pf_env : goal sigma -> env @@ -95,7 +98,7 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a - val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference + val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml new file mode 100644 index 00000000..86a7e9c5 --- /dev/null +++ b/proofs/tactypes.ml @@ -0,0 +1,54 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Evd.evar_map -> Evd.evar_map * 'a + +type delayed_open_constr = EConstr.constr delayed_open +type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open + +type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t +type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t -- cgit v1.2.3