diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 88 | ||||
| -rw-r--r-- | proofs/clenv.mli | 12 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 14 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.ml | 13 | ||||
| -rw-r--r-- | proofs/goal.mli | 6 | ||||
| -rw-r--r-- | proofs/logic.ml | 172 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 195 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 89 | ||||
| -rw-r--r-- | proofs/proof.ml | 10 | ||||
| -rw-r--r-- | proofs/proof.mli | 6 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 314 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 121 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
17 files changed, 169 insertions, 889 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0dcc55a1cb..58c0f7db53 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -51,11 +51,11 @@ let refresh_undefined_univs clenv = match EConstr.kind clenv.evd clenv.templval.rebus with | Var _ -> clenv, Univ.empty_level_subst | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst - | _ -> + | _ -> let evd', subst = Evd.refresh_undefined_universes clenv.evd in let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in { clenv with evd = evd'; templval = map_freelisted clenv.templval; - templtyp = map_freelisted clenv.templtyp }, subst + templtyp = map_freelisted clenv.templtyp }, subst let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t @@ -68,16 +68,16 @@ let clenv_push_prod cl = let rec clrec typ = match EConstr.kind cl.evd typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> - let mv = new_meta () in - let dep = not (noccurn (cl_sigma cl) 1 u) in + let mv = new_meta () in + let dep = not (noccurn (cl_sigma cl) 1 u) in let na' = if dep then na.binder_name else Anonymous 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; - templtyp = mk_freelisted concl; - evd = e'; - env = cl.env } + 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; + templtyp = mk_freelisted concl; + evd = e'; + env = cl.env } | _ -> raise NotExtensibleClause in clrec typ @@ -102,12 +102,12 @@ let clenv_environments evd bound t = | (Some 0, _) -> (e, List.rev metas, t) | (n, Cast (t,_,_)) -> clrec (e,metas) n t | (n, Prod (na,t1,t2)) -> - let mv = new_meta () in - let dep = not (noccurn evd 1 t2) in + let mv = new_meta () in + let dep = not (noccurn evd 1 t2) in let na' = if dep then na.binder_name else Anonymous 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) + 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) | (n, _) -> (e, List.rev metas, t) in @@ -167,7 +167,7 @@ let clenv_assign mv rhs clenv = if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then error_incompatible_inst clenv mv else - clenv + clenv else let st = (Conv,TypeNotProcessed) in {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} @@ -226,8 +226,8 @@ let dependent_closure clenv mvs = let rec aux mvs acc = Metaset.fold (fun mv deps -> - let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in - aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in + aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) mvs acc in aux mvs mvs @@ -241,9 +241,9 @@ let clenv_dependent_gen hyps_only ?(iter=true) clenv = List.filter (fun mv -> if hyps_only then - Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl) + Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl) else - Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl) + Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl) all_undefined let clenv_missing ce = clenv_dependent_gen true ce @@ -336,8 +336,8 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = clenv.evd in - let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in - let clenv = clenv_assign mv evar {clenv with evd=evd} in + let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in + let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv (fst (destEvar evd evar) :: evs) mvs in fold clenv [] dep_mvs @@ -415,13 +415,13 @@ let qhyp_eq h1 h2 = match h1, h2 with let check_bindings bl = match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with | NamedHyp s :: _ -> - user_err - (str "The variable " ++ Id.print s ++ - str " occurs more than once in binding list."); + user_err + (str "The variable " ++ Id.print s ++ + str " occurs more than once in binding list."); | AnonHyp n :: _ -> - user_err - (str "The position " ++ int n ++ - str " occurs more than once in binding list.") + user_err + (str "The position " ++ int n ++ + str " occurs more than once in binding list.") | [] -> () let explain_no_such_bound_variable evd id = @@ -472,7 +472,7 @@ let meta_of_binder clause loc mvs = function let error_already_defined b = match b with | NamedHyp id -> - user_err + user_err (str "Binder name \"" ++ Id.print id ++ str"\" already defined with incompatible value.") | AnonHyp n -> @@ -488,12 +488,12 @@ let clenv_unify_binding_type clenv c t u = try let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c - with + with | PretypeError (_,_,ActualTypeNotCoercible (_,_, (NotClean _ | ConversionFailed _))) as e -> - raise e + raise e | e when precatchable_exception e -> - TypeNotProcessed, clenv, c + TypeNotProcessed, clenv, c let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in @@ -509,12 +509,12 @@ let clenv_match_args bl clenv = check_bindings bl; List.fold_left (fun clenv {CAst.loc;v=(b,c)} -> - let k = meta_of_binder clenv loc mvs b in + let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then 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) + clenv_assign_binding clenv k c) clenv bl exception NoSuchBinding @@ -525,7 +525,7 @@ let clenv_constrain_last_binding c clenv = clenv_assign_binding clenv k c let error_not_right_number_missing_arguments n = - user_err + user_err (strbrk "Not the right number of missing arguments (expected " ++ int n ++ str ").") @@ -538,14 +538,14 @@ let clenv_constrain_dep_args hyps_only bl clenv = List.fold_left2 clenv_assign_binding clenv occlist bl else if hyps_only then - (* Tolerance for compatibility <= 8.3 *) - let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in - if Int.equal (List.length occlist') (List.length bl) then - List.fold_left2 clenv_assign_binding clenv occlist' bl - else - error_not_right_number_missing_arguments (List.length occlist) + (* Tolerance for compatibility <= 8.3 *) + let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in + if Int.equal (List.length occlist') (List.length bl) then + List.fold_left2 clenv_assign_binding clenv occlist' bl + else + error_not_right_number_missing_arguments (List.length occlist) else - error_not_right_number_missing_arguments (List.length occlist) + error_not_right_number_missing_arguments (List.length occlist) (****************************************************************) (* Clausal environment for an application *) @@ -557,7 +557,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function | ExplicitBindings lbind -> let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in let clause = mk_clenv_from_env env sigma n - (c, t) + (c, t) in clenv_match_args lbind clause | NoBindings -> mk_clenv_from_env env sigma n (c,t) @@ -567,7 +567,7 @@ let make_clenv_binding_env_apply env sigma n = let make_clenv_binding_env env sigma = make_clenv_binding_gen false None env sigma - + let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma @@ -659,7 +659,7 @@ let evar_with_name holes id = | [] -> explain_no_such_bound_variable holes id | [h] -> h.hole_evar | _ -> - user_err + user_err (str "Binder name \"" ++ Id.print id ++ str "\" occurs more than once in clause.") diff --git a/proofs/clenv.mli b/proofs/clenv.mli index eecd318287..3fca967395 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -24,10 +24,10 @@ open Tactypes type clausenv = { env : env; (** the typing context *) - evd : evar_map; (** the mapping from metavar and evar numbers to their - types and values *) - templval : constr freelisted; (** the template which we are trying to fill - out *) + evd : evar_map; (** the mapping from metavar and evar numbers to their + types and values *) + templval : constr freelisted; (** the template which we are trying to fill + out *) templtyp : constr freelisted (** its type *)} @@ -92,8 +92,8 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** start with a clenv to refine with a given term with bindings *) -(** the arity of the lemma is fixed - the optional int tells how many prods of the lemma have to be used +(** the arity of the lemma is fixed + the optional int tells how many prods of the lemma have to be used use all of them if None *) val make_clenv_binding_env_apply : env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 1904d9b112..611671255d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -35,15 +35,15 @@ let clenv_cast_meta clenv = and crec_hd u = match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with | Meta mv -> - (try + (try let b = Typing.meta_type clenv.evd mv in - assert (not (occur_meta clenv.evd b)); - if occur_meta clenv.evd b then u + assert (not (occur_meta clenv.evd b)); + if occur_meta clenv.evd b then u else mkCast (mkMeta mv, DEFAULTcast, b) - with Not_found -> u) + with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> - mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) + mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) | Proj (p, c) -> mkProj (p, crec_hd c) | _ -> u in @@ -108,7 +108,7 @@ let fail_quick_core_unif_flags = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - frozen_evars = Evar.Set.empty; + allowed_evars = AllowAll; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; @@ -130,6 +130,6 @@ let unify ?(flags=fail_quick_unif_flags) m = let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in - Proofview.Unsafe.tclEVARSADVANCE evd' + Proofview.Unsafe.tclEVARSADVANCE evd' with e when CErrors.noncritical e -> Proofview.tclZERO e end diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 6c9c95e342..59918ab2f9 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -61,7 +61,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = 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 + user_err ?loc (str "Instance is not well-typed in the environment of " ++ Termops.pr_existential_key sigma evk ++ str ".") in diff --git a/proofs/goal.ml b/proofs/goal.ml index 888c4785df..426fba7f63 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -91,7 +91,8 @@ module V82 = struct let weak_progress glss gls = match glss.Evd.it with - | [ g ] -> not (Proofview.Progress.goal_equal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) + | [ g ] -> not (Proofview.Progress.goal_equal ~evd:gls.Evd.sigma + ~extended_evd:glss.Evd.sigma gls.Evd.it g) | _ -> true let progress glss gls = @@ -120,12 +121,12 @@ module V82 = struct try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> - if is_proof_var decl then + if is_proof_var decl then let decl = Termops.map_named_decl EConstr.of_constr decl in - mkNamedProd_or_LetIn decl t - else - t - ) ~init:(concl sigma gl) env + mkNamedProd_or_LetIn decl t + else + t + ) ~init:(concl sigma gl) env end diff --git a/proofs/goal.mli b/proofs/goal.mli index 46b54f9c2c..7b16d869e9 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -21,7 +21,7 @@ val uid : goal -> string (* Debugging help *) val pr_goal : goal -> Pp.t -(* Layer to implement v8.2 tactic engine ontop of the new architecture. +(* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the internal types. *) module V82 : sig @@ -42,7 +42,7 @@ module V82 : sig (* Old style mk_goal primitive, returns a new goal with corresponding hypotheses and conclusion, together with a term which is precisely the evar corresponding to the goal, and an updated evar_map. *) - val mk_goal : Evd.evar_map -> + val mk_goal : Evd.evar_map -> Environ.named_context_val -> EConstr.constr -> goal * EConstr.constr * Evd.evar_map @@ -61,7 +61,7 @@ module V82 : sig val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map (* Goal represented as a type, doesn't take into account section variables *) - val abstract_type : Evd.evar_map -> goal -> EConstr.types + val abstract_type : Evd.evar_map -> goal -> EConstr.types end diff --git a/proofs/logic.ml b/proofs/logic.ml index a9843e080e..a361c4208e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -68,7 +68,7 @@ let catchable_exception = function (* reduction errors *) | Tacred.ReductionTacticError _ -> true (* unification and typing errors *) - | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e + | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e | _ -> false let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id)) @@ -207,15 +207,15 @@ let split_sign env sigma hfrom hto l = | [] -> error_no_such_hypothesis env sigma hfrom | d :: right -> let hyp = NamedDecl.get_id d in - if Id.equal hyp hfrom then - (left,right,d, toleft || move_location_eq hto MoveLast) - else + if Id.equal hyp hfrom then + (left,right,d, toleft || move_location_eq hto MoveLast) + else let is_toleft = match hto with | MoveAfter h' | MoveBefore h' -> Id.equal hyp h' | _ -> false in - splitrec (d::left) (toleft || is_toleft) - right + splitrec (d::left) (toleft || is_toleft) + right in splitrec [] false l @@ -232,29 +232,29 @@ let move_hyp env sigma toleft (left,declfrom,right) hto = in let rec moverec first middle = function | [] -> - if match hto with MoveFirst | MoveLast -> false | _ -> true then + if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis env sigma (hyp_of_move_location hto); - List.rev first @ List.rev middle + List.rev first @ List.rev middle | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> - List.rev first @ List.rev middle @ right + List.rev first @ List.rev middle @ right | d :: right -> let hyp = NamedDecl.get_id d in - let (first',middle') = - if List.exists (test_dep d) middle then - if not (move_location_eq hto (MoveAfter hyp)) then - (first, d::middle) + let (first',middle') = + if List.exists (test_dep d) middle then + if not (move_location_eq hto (MoveAfter hyp)) then + (first, d::middle) else - user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ + user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ pr_move_location Id.print hto ++ - str (if toleft then ": it occurs in the type of " else ": it depends on ") - ++ Id.print hyp ++ str ".") + str (if toleft then ": it occurs in the type of " else ": it depends on ") + ++ Id.print hyp ++ str ".") else - (d::first, middle) - in - if move_location_eq hto (MoveAfter hyp) then - List.rev first' @ List.rev middle' @ right - else - moverec first' middle' right + (d::first, middle) + in + if move_location_eq hto (MoveAfter hyp) then + List.rev first' @ List.rev middle' @ right + else + moverec first' middle' right in let open EConstr in if toleft then @@ -265,7 +265,7 @@ let move_hyp env sigma toleft (left,declfrom,right) hto = else let right = List.fold_right push_named_context_val - (moverec [] [declfrom] right) empty_named_context_val in + (moverec [] [declfrom] right) empty_named_context_val in List.fold_left (fun sign d -> push_named_context_val d sign) right left @@ -328,7 +328,7 @@ exception Stop of EConstr.t list let meta_free_prefix sigma a = try let a = Array.map EConstr.of_constr a in - let _ = Array.fold_left (fun acc a -> + let _ = Array.fold_left (fun acc a -> if occur_meta sigma a then raise (Stop acc) else a :: acc) [] a in a @@ -355,69 +355,69 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind trm with | Meta _ -> let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in - if !check && occur_meta sigma conclty then + if !check && occur_meta sigma conclty then raise (RefinerError (env, sigma, MetaInType conclty)); - let (gl,ev,sigma) = mk_goal hyps conclty in - let ev = EConstr.Unsafe.to_constr ev in - let conclty = EConstr.Unsafe.to_constr conclty in - gl::goalacc, conclty, sigma, ev + let (gl,ev,sigma) = mk_goal hyps conclty in + let ev = EConstr.Unsafe.to_constr ev in + let conclty = EConstr.Unsafe.to_constr conclty in + gl::goalacc, conclty, sigma, ev | Cast (t,k, ty) -> - check_typability env sigma ty; + check_typability env sigma ty; let sigma = check_conv_leq_goal env sigma trm ty conclty in - let res = mk_refgoals sigma goal goalacc ty t in + let res = mk_refgoals sigma goal goalacc ty t in (* we keep the casts (in particular VMcast and NATIVEcast) except when they are annotating metas *) - if isMeta t then begin - assert (k != VMcast && k != NATIVEcast); - res - end else - let (gls,cty,sigma,ans) = res in + if isMeta t then begin + assert (k != VMcast && k != NATIVEcast); + res + end else + let (gls,cty,sigma,ans) = res in let ans = if ans == t then trm else mkCast(ans,k,ty) in - (gls,cty,sigma,ans) + (gls,cty,sigma,ans) | App (f,l) -> - let (acc',hdty,sigma,applicand) = + let (acc',hdty,sigma,applicand) = if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then - let ty = - (* Template polymorphism of definitions and inductive types *) - let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in - let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in - type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) - in - let ty = EConstr.Unsafe.to_constr ty in - goalacc, ty, sigma, f - else - mk_hdgoals sigma goal goalacc f - in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + let ty = + (* Template polymorphism of definitions and inductive types *) + let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in + let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in + type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) + in + let ty = EConstr.Unsafe.to_constr ty in + goalacc, ty, sigma, f + else + mk_hdgoals sigma goal goalacc f + in + let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in let sigma = check_conv_leq_goal env sigma trm conclty' conclty in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in (acc'',conclty',sigma, ans) | Proj (p,c) -> - let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in - let c = mkProj (p, c') in - let ty = get_type_of env sigma (EConstr.of_constr c) in - let ty = EConstr.Unsafe.to_constr ty in - (acc',ty,sigma,c) + let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in + let c = mkProj (p, c') in + let ty = get_type_of env sigma (EConstr.of_constr c) in + let ty = EConstr.Unsafe.to_constr ty in + (acc',ty,sigma,c) | 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',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) = 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 else mkCase (ci,p',c',lf') in - (acc'',conclty',sigma, ans) + (acc'',conclty',sigma, ans) | _ -> - if occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refiner called with a meta in non app/case subterm."); - let (sigma, t'ty) = goal_type_of env sigma trm in - let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + if occur_meta sigma (EConstr.of_constr trm) then + anomaly (Pp.str "refiner called with a meta in non app/case subterm."); + let (sigma, t'ty) = goal_type_of env sigma trm in + let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) (* Same as mkREFGOALS but without knowing the type of the term. Therefore, @@ -426,53 +426,53 @@ let rec mk_refgoals sigma goal goalacc conclty trm = and mk_hdgoals sigma goal goalacc trm = let env = Goal.V82.env sigma goal in let hyps = Goal.V82.hyps sigma goal in - let mk_goal hyps concl = + let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> - check_typability env sigma ty; + check_typability env sigma ty; let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in - let ev = EConstr.Unsafe.to_constr ev in - gl::goalacc,ty,sigma,ev + let ev = EConstr.Unsafe.to_constr ev in + gl::goalacc,ty,sigma,ev | Cast (t,_, ty) -> - check_typability env sigma ty; - mk_refgoals sigma goal goalacc ty t + check_typability env sigma ty; + mk_refgoals sigma goal goalacc ty t | App (f,l) -> - let (acc',hdty,sigma,applicand) = + let (acc',hdty,sigma,applicand) = if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) - then - let l' = meta_free_prefix sigma l in - (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) - else mk_hdgoals sigma goal goalacc f - in - let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in + then + let l' = meta_free_prefix sigma l in + (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) + else mk_hdgoals sigma goal goalacc f + in + let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in - (acc'',conclty',sigma, ans) + (acc'',conclty',sigma, ans) | Case (ci,p,c,lf) -> - let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in + let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in - let lf' = Array.rev_of_list rbranches in - let ans = + let lf' = Array.rev_of_list rbranches in + let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm else mkCase (ci,p',c',lf') - in - (acc'',conclty',sigma, ans) + in + (acc'',conclty',sigma, ans) | Proj (p,c) -> let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in - let c = mkProj (p, c') in + let c = mkProj (p, c') in let ty = get_type_of env sigma (EConstr.of_constr c) in let ty = EConstr.Unsafe.to_constr ty in - (acc',ty,sigma,c) + (acc',ty,sigma,c) | _ -> - if !check && occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refine called with a dependent meta."); + if !check && occur_meta sigma (EConstr.of_constr trm) then + anomaly (Pp.str "refine called with a dependent meta."); let (sigma, ty) = goal_type_of env sigma trm in - goalacc, ty, sigma, trm + goalacc, ty, sigma, trm and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml deleted file mode 100644 index 99a254652c..0000000000 --- a/proofs/pfedit.ml +++ /dev/null @@ -1,195 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Util -open Names -open Environ -open Evd - -let use_unification_heuristics_ref = ref true -let () = Goptions.(declare_bool_option { - optdepr = false; - optname = "Solve unification constraints at every \".\""; - optkey = ["Solve";"Unification";"Constraints"]; - optread = (fun () -> !use_unification_heuristics_ref); - optwrite = (fun a -> use_unification_heuristics_ref:=a); -}) - -let use_unification_heuristics () = !use_unification_heuristics_ref - -exception NoSuchGoal -let () = CErrors.register_handler begin function - | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") - | _ -> raise CErrors.Unhandled -end - -let get_nth_V82_goal p i = - let Proof.{ sigma; goals } = Proof.data p in - try { it = List.nth goals (i-1) ; sigma } - with Failure _ -> raise NoSuchGoal - -let get_goal_context_gen pf i = - let { it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in - (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) - -let get_goal_context pf i = - let p = Proof_global.get_proof pf in - get_goal_context_gen p i - -let get_current_goal_context pf = - let p = Proof_global.get_proof pf in - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* spiwack: returning empty evar_map, since if there is no goal, - under focus, there is no accessible evar either. EJGA: this - seems strange, as we have pf *) - let env = Global.env () in - Evd.from_env env, env - -let get_current_context pf = - let p = Proof_global.get_proof pf in - try get_goal_context_gen p 1 - with - | NoSuchGoal -> - (* No more focused goals *) - let { Proof.sigma } = Proof.data p in - sigma, Global.env () - -let solve ?with_end_tac gi info_lvl tac pr = - let tac = match with_end_tac with - | None -> tac - | Some etac -> Proofview.tclTHEN tac etac in - let tac = match info_lvl with - | None -> tac - | Some _ -> Proofview.Trace.record_info_trace tac - in - let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in - 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 ~nosuchgoal i i tac - | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac - | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac - | SelectAll -> tac - in - let tac = - if use_unification_heuristics () then - Proofview.tclTHEN tac Refine.solve_constraints - else tac - in - let env = Global.env () in - let (p,(status,info),()) = Proof.run_tactic env tac pr in - let env = Global.env () in - let sigma = Evd.from_env env in - let () = - match info_lvl with - | None -> () - | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info)) - in - (p,status) - -let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None tac) - -(**********************************************************************) -(* Shortcut to build a term using tactics *) - -let next = let n = ref 0 in fun () -> incr n; !n - -let build_constant_by_tactic ~name ctx sign ~poly typ tac = - let evd = Evd.from_ctx ctx in - let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in - try - let pf, status = by tac pf in - let open Proof_global in - let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in - match entries with - | [entry] -> - let univs = UState.demote_seff_univs entry.Proof_global.proof_entry_universes universes in - entry, status, univs - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - with reraise -> - let reraise = CErrors.push reraise in - iraise reraise - -let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = - let name = Id.of_string ("temporary_proof"^string_of_int (next())) in - let sign = val_of_named_context (named_context env) in - let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in - let body, eff = Future.force ce.Proof_global.proof_entry_body in - let (cb, ctx) = - if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) - else body - in - let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in - cb, status, univs - -let refine_by_tactic ~name ~poly env sigma ty tac = - (* Save the initial side-effects to restore them afterwards. We set the - current set of side-effects to be empty so that we can retrieve the - ones created during the tactic invocation easily. *) - let eff = Evd.eval_side_effects sigma in - let sigma = Evd.drop_side_effects sigma in - (* Save the existing goals *) - let prev_future_goals = save_future_goals sigma in - (* Start a proof *) - let prf = Proof.start ~name ~poly sigma [env, ty] in - let (prf, _, ()) = - try Proof.run_tactic env tac prf - with Logic_monad.TacticFailure e as src -> - (* Catch the inner error of the monad tactic *) - let (_, info) = CErrors.push src in - iraise (e, info) - in - (* Plug back the retrieved sigma *) - let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in - assert (stack = []); - let ans = match Proofview.initial_goals entry with - | [c, _] -> c - | _ -> assert false - 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 *) - let sigma = Evd.drop_side_effects sigma in - let sigma = Evd.emit_side_effects eff sigma in - (* Restore former goals *) - let sigma = restore_future_goals sigma prev_future_goals in - (* Push remaining goals as future_goals which is the only way we - have to inform the caller that there are goals to collect while - not being encapsulated in the monad *) - (* Goals produced by tactic "shelve" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in - (* Goals produced by tactic "give_up" *) - let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in - (* Other goals *) - let sigma = List.fold_right Evd.declare_future_goal goals sigma in - (* Get rid of the fresh side-effects by internalizing them in the term - itself. Note that this is unsound, because the tactic may have solved - other goals that were already present during its invocation, so that - those goals rely on effects that are not present anymore. Hopefully, - this hack will work in most cases. *) - let neff = neff.Evd.seff_private in - let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in - ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli deleted file mode 100644 index 0626e40047..0000000000 --- a/proofs/pfedit.mli +++ /dev/null @@ -1,89 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Global proof state. A quite redundant wrapper on {!Proof_global}. *) - -open Names -open Constr -open Environ - -(** {6 ... } *) - -exception NoSuchGoal - -(** [get_goal_context n] returns the context of the [n]th subgoal of - the current focused proof or raises a [UserError] if there is no - focused proof or if there is no more subgoals *) - -val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env - -(** [get_current_goal_context ()] works as [get_goal_context 1] *) -val get_current_goal_context : Proof_global.t -> Evd.evar_map * env - -(** [get_current_context ()] returns the context of the - current focused goal. If there is no focused goal but there - is a proof in progress, it returns the corresponding evar_map. - If there is no pending proof then it returns the current global - environment and empty evar_map. *) -val get_current_context : Proof_global.t -> Evd.evar_map * env - -(** {6 ... } *) - -(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th - subgoal of the current focused proof. [solve SelectAll - tac] applies [tac] to all subgoals. *) - -val solve : ?with_end_tac: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 - focused proof. - Returns [false] if an unsafe tactic has been used. *) - -val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool - -(** Option telling if unification heuristics should be used. *) -val use_unification_heuristics : unit -> bool - -(** [build_by_tactic typ tac] returns a term of type [typ] by calling - [tac]. The return boolean, if [false] indicates the use of an unsafe - tactic. *) - -val build_constant_by_tactic - : name:Id.t - -> UState.t - -> named_context_val - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> Evd.side_effects Proof_global.proof_entry * bool * UState.t - -val build_by_tactic - : ?side_eff:bool - -> env - -> UState.t - -> poly:bool - -> EConstr.types - -> unit Proofview.tactic - -> constr * bool * UState.t - -val refine_by_tactic - : name:Id.t - -> poly:bool - -> env -> Evd.evar_map - -> EConstr.types - -> unit Proofview.tactic - -> constr * Evd.evar_map -(** A variant of the above function that handles open terms as well. - Caveat: all effects are purged in the returned term at the end, but other - evars solved by side-effects are NOT purged, so that unexpected failures may - occur. Ideally all code using this function should be rewritten in the - monad. *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 5f07cc1acc..2ee006631a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -19,7 +19,7 @@ - Focus: a proof has a focus stack: the top of the stack contains the context in which to unfocus the current view to a view focused with the rest of the stack. - In addition, this contains, for each of the focus context, a + In addition, this contains, for each of the focus context, a "focus kind" and a "focus condition" (in practice, and for modularity, the focus kind is actually stored inside the condition). To unfocus, one needs to know the focus kind, and the condition (for instance "no condition" or @@ -179,7 +179,7 @@ let cond_of_focus pr = | (cond,_,_)::_ -> cond | _ -> raise FullyUnfocused -(* An auxiliary function to pop and read the last {!Proofview.focus_context} +(* An auxiliary function to pop and read the last {!Proofview.focus_context} on the focus stack. *) let pop_focus pr = match pr.focus_stack with @@ -202,7 +202,7 @@ let _unfocus pr = { pr with proofview = Proofview.unfocus fc pr.proofview } (* Focus command (focuses on the [i]th subgoal) *) -(* spiwack: there could also, easily be a focus-on-a-range tactic, is there +(* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) let focus cond inf i pr = try _focus cond (Obj.repr inf) i i pr @@ -250,7 +250,7 @@ let rec unfocus kind pr () = | Loose -> begin try let pr = _unfocus pr in - unfocus kind pr () + unfocus kind pr () with FullyUnfocused -> raise CannotUnfocusThisWay end @@ -412,7 +412,7 @@ module V82 = struct let top_goal p = let { Evd.it=gls ; sigma=sigma; } = - Proofview.V82.top_goals p.entry p.proofview + Proofview.V82.top_goals p.entry p.proofview in { Evd.it=List.hd gls ; sigma=sigma; } diff --git a/proofs/proof.mli b/proofs/proof.mli index 9973df492d..134b0146b6 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -19,7 +19,7 @@ - Focus: a proof has a focus stack: the top of the stack contains the context in which to unfocus the current view to a view focused with the rest of the stack. - In addition, this contains, for each of the focus context, a + In addition, this contains, for each of the focus context, a "focus kind" and a "focus condition" (in practice, and for modularity, the focus kind is actually stored inside the condition). To unfocus, one needs to know the focus kind, and the condition (for instance "no condition" or @@ -107,7 +107,7 @@ val new_focus_kind : unit -> 'a focus_kind the action which focused. Conditions always carry a focus kind, and inherit their type parameter from it.*) -type 'a focus_condition +type 'a focus_condition (* [no_cond] only checks that the unfocusing command uses the right [focus_kind]. If [loose_end] (default [false]) is [true], then if the [focus_kind] @@ -126,7 +126,7 @@ val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) -(* spiwack: there could also, easily be a focus-on-a-range tactic, is there +(* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) val focus : 'a focus_condition -> 'a -> int -> t -> t diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 5702156b65..66e2ae5c29 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -50,7 +50,7 @@ module Strict = struct | Suggest of t (* this bullet is mandatory here *) | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *) | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending, - some focused goals exists. *) + some focused goals exists. *) | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) | ProofFinished (* No more goal anywhere *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml deleted file mode 100644 index 851a3d1135..0000000000 --- a/proofs/proof_global.ml +++ /dev/null @@ -1,314 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(***********************************************************************) -(* *) -(* This module defines proof facilities relevant to the *) -(* toplevel. In particular it defines the global proof *) -(* environment. *) -(* *) -(***********************************************************************) - -open Util -open Names -open Context - -module NamedDecl = Context.Named.Declaration - -(*** Proof Global Environment ***) - -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - -type proof_object = - { name : Names.Id.t - ; entries : Evd.side_effects proof_entry list - ; poly : bool - ; universes: UState.t - ; udecl : UState.universe_decl - } - -type opacity_flag = Opaque | Transparent - -type t = - { endline_tactic : Genarg.glob_generic_argument option - ; section_vars : Constr.named_context option - ; proof : Proof.t - ; udecl: UState.universe_decl - (** Initial universe declarations *) - ; initial_euctx : UState.t - (** The initial universe context (for the statement) *) - } - -(*** Proof Global manipulation ***) - -let get_proof ps = ps.proof -let get_proof_name ps = (Proof.data ps.proof).Proof.name - -let get_initial_euctx ps = ps.initial_euctx - -let map_proof f p = { p with proof = f p.proof } -let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res - -let map_fold_proof_endline f ps = - let et = - match ps.endline_tactic with - | None -> Proofview.tclUNIT () - | Some tac -> - let open Geninterp in - let {Proof.poly} = Proof.data ps.proof in - let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in - let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in - let tac = Geninterp.interp tag ist tac in - Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) - in - let (newpr,ret) = f et ps.proof in - let ps = { ps with proof = newpr } in - ps, ret - -let compact_the_proof pf = map_proof Proof.compact pf - -(* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac ps = - { ps with endline_tactic = Some tac } - -(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of - name [name] with goals [goals] (a list of pairs of environment and - conclusion). The proof is started in the evar map [sigma] (which - can typically contain universe constraints), and with universe - bindings [udecl]. *) -let start_proof ~name ~udecl ~poly sigma goals = - let proof = Proof.start ~name ~poly sigma goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in - { proof - ; endline_tactic = None - ; section_vars = None - ; udecl - ; initial_euctx - } - -let start_dependent_proof ~name ~udecl ~poly goals = - let proof = Proof.dependent_start ~name ~poly goals in - let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in - { proof - ; endline_tactic = None - ; section_vars = None - ; udecl - ; initial_euctx - } - -let get_used_variables pf = pf.section_vars -let get_universe_decl pf = pf.udecl - -let set_used_variables ps l = - let open Context.Named.Declaration in - let env = Global.env () in - let ids = List.fold_right Id.Set.add l Id.Set.empty in - let ctx = Environ.keep_hyps env ids in - let ctx_set = - List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in - let vars_of = Environ.global_vars_set in - let aux env entry (ctx, all_safe as orig) = - match entry with - | LocalAssum ({binder_name=x},_) -> - if Id.Set.mem x all_safe then orig - else (ctx, all_safe) - | LocalDef ({binder_name=x},bo, ty) as decl -> - if Id.Set.mem x all_safe then orig else - let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in - if Id.Set.subset vars all_safe - then (decl :: ctx, Id.Set.add x all_safe) - else (ctx, all_safe) in - let ctx, _ = - Environ.fold_named_context aux env ~init:(ctx,ctx_set) in - if not (Option.is_empty ps.section_vars) then - CErrors.user_err Pp.(str "Used section variables can be declared only once"); - (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), { ps with section_vars = Some ctx} - -let get_open_goals ps = - let Proof.{ goals; stack; shelf } = Proof.data ps.proof in - List.length goals + - List.fold_left (+) 0 - (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + - List.length shelf - -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t - -let private_poly_univs = - let b = ref true in - let _ = Goptions.(declare_bool_option { - optdepr = false; - optname = "use private polymorphic universes for Qed constants"; - optkey = ["Private";"Polymorphic";"Universes"]; - optread = (fun () -> !b); - optwrite = ((:=) b); - }) - in - fun () -> !b - -let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now - (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; udecl; initial_euctx } = ps in - let Proof.{ name; poly; entry } = Proof.data proof in - let opaque = match opaque with Opaque -> true | Transparent -> false in - let constrain_variables ctx = - UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx - in - let fpl, univs = Future.split2 fpl in - let universes = if poly || now then Future.force univs else initial_euctx in - (* Because of dependent subgoals at the beginning of proofs, we could - have existential variables in the initial types of goals, we need to - normalise them for the kernel. *) - let subst_evar k = - let { Proof.sigma } = Proof.data proof in - Evd.existential_opt_value0 sigma k in - let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar - (UState.subst universes) in - - let make_body = - if poly || now then - let make_body t (c, eff) = - let body = c in - let allow_deferred = - not poly && (keep_body_ucst_separate || - not (Safe_typing.empty_private_constants = eff.Evd.seff_private)) - in - let typ = if allow_deferred then t else nf t in - let used_univs_body = Vars.universes_of_constr body in - let used_univs_typ = Vars.universes_of_constr typ in - if allow_deferred then - let initunivs = UState.univ_entry ~poly initial_euctx in - let ctx = constrain_variables universes in - (* For vi2vo compilation proofs are computed now but we need to - complement the univ constraints of the typ with the ones of - the body. So we keep the two sets distinct. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = UState.restrict ctx used_univs in - let univs = UState.check_mono_univ_decl ctx_body udecl in - (initunivs, typ), ((body, univs), eff) - else if poly && opaque && private_poly_univs () then - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let universes = UState.restrict universes used_univs in - let typus = UState.restrict universes used_univs_typ in - let udecl = UState.check_univ_decl ~poly typus udecl in - let ubody = Univ.ContextSet.diff - (UState.context_set universes) - (UState.context_set typus) - in - (udecl, typ), ((body, ubody), eff) - else - (* Since the proof is computed now, we can simply have 1 set of - constraints in which we merge the ones for the body and the ones - for the typ. We recheck the declaration after restricting with - the actually used universes. - TODO: check if restrict is really necessary now. *) - let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = UState.restrict universes used_univs in - let univs = UState.check_univ_decl ~poly ctx udecl in - (univs, typ), ((body, Univ.ContextSet.empty), eff) - in - fun t p -> Future.split2 (Future.chain p (make_body t)) - else - fun t p -> - (* Already checked the univ_decl for the type universes when starting the proof. *) - let univctx = UState.univ_entry ~poly:false universes in - let t = nf t in - Future.from_val (univctx, t), - Future.chain p (fun (pt,eff) -> - (* Deferred proof, we already checked the universe declaration with - the initial universes, ensure that the final universes respect - the declaration as well. If the declaration is non-extensible, - this will prevent the body from adding universes and constraints. *) - let univs = Future.force univs in - let univs = constrain_variables univs in - let used_univs = Univ.LSet.union - (Vars.universes_of_constr t) - (Vars.universes_of_constr pt) - in - let univs = UState.restrict univs used_univs in - let univs = UState.check_mono_univ_decl univs udecl in - (pt,univs),eff) - in - let entry_fn p (_, t) = - let t = EConstr.Unsafe.to_constr t in - let univstyp, body = make_body t p in - let univs, typ = Future.force univstyp in - { - proof_entry_body = body; - proof_entry_secctx = section_vars; - proof_entry_feedback = feedback_id; - proof_entry_type = Some typ; - proof_entry_inline_code = false; - proof_entry_opaque = opaque; - proof_entry_universes = univs; } - in - let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { name; entries = entries; poly; universes; udecl } - -let return_proof ?(allow_partial=false) ps = - let { proof } = ps in - if allow_partial then begin - let proofs = Proof.partial_proof proof in - let Proof.{sigma=evd} = Proof.data proof in - let eff = Evd.eval_side_effects evd in - (* 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 -> EConstr.Unsafe.to_constr c, eff) proofs in - proofs, Evd.evar_universe_context evd - end else - let Proof.{name=pid;entry} = Proof.data proof in - let initial_goals = Proofview.initial_goals entry in - let evd = Proof.return ~pid proof in - let eff = Evd.eval_side_effects evd in - let evd = Evd.minimize_universes evd in - let proof_opt c = - match EConstr.to_constr_opt evd c with - | Some p -> p - | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") - in - (* 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... *) - (* EJGA: actually side-effects de-duplication and this codepath is - unrelated. Duplicated side-effects arise from incorrect scheme - generation code, the main bulk of it was mostly fixed by #9836 - but duplication can still happen because of rewriting schemes I - think; however the code below is mostly untested, the only - code-paths that generate several proof entries are derive and - equations and so far there is no code in the CI that will - actually call those and do a side-effect, TTBOMK *) - let proofs = - List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in - proofs, Evd.evar_universe_context evd - -let close_future_proof ~opaque ~feedback_id ps proof = - close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps - -let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = - close_proof ~opaque ~keep_body_ucst_separate ~now:true - (Future.from_val ~fix_exn (return_proof ps)) ps - -let update_global_env = - map_proof (fun p -> - let { Proof.sigma } = Proof.data p in - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let p, (status,info), _ = Proof.run_tactic (Global.env ()) tac p in - p) diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli deleted file mode 100644 index 54d5c2087a..0000000000 --- a/proofs/proof_global.mli +++ /dev/null @@ -1,121 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** This module defines proof facilities relevant to the - toplevel. In particular it defines the global proof - environment. *) - -type t - -(* Should be moved into a proper view *) -val get_proof : t -> Proof.t -val get_proof_name : t -> Names.Id.t -val get_used_variables : t -> Constr.named_context option - -(** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl - -(** Get initial universe state *) -val get_initial_euctx : t -> UState.t - -val compact_the_proof : t -> t - -(** When a proof is closed, it is reified into a [proof_object], where - [id] is the name of the proof, [entries] the list of the proof terms - (in a form suitable for definitions). Together with the [terminator] - function which takes a [proof_object] together with a [proof_end] - (i.e. an proof ending command) and registers the appropriate - values. *) -type 'a proof_entry = { - proof_entry_body : 'a Entries.const_entry_body; - (* List of section variables *) - proof_entry_secctx : Constr.named_context option; - (* State id on which the completion of type checking is reported *) - proof_entry_feedback : Stateid.t option; - proof_entry_type : Constr.types option; - proof_entry_universes : Entries.universes_entry; - proof_entry_opaque : bool; - proof_entry_inline_code : bool; -} - -(** When a proof is closed, it is reified into a [proof_object] *) -type proof_object = - { name : Names.Id.t - (** name of the proof *) - ; entries : Evd.side_effects proof_entry list - (** list of the proof terms (in a form suitable for definitions). *) - ; poly : bool - (** polymorphic status *) - ; universes: UState.t - (** universe state *) - ; udecl : UState.universe_decl - (** universe declaration *) - } - -type opacity_flag = Opaque | Transparent - -(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of - name [name] with goals [goals] (a list of pairs of environment and - conclusion); [poly] determines if the proof is universe - polymorphic. The proof is started in the evar map [sigma] (which - can typically contain universe constraints), and with universe - bindings [udecl]. *) -val start_proof - : name:Names.Id.t - -> udecl:UState.universe_decl - -> poly:bool - -> Evd.evar_map - -> (Environ.env * EConstr.types) list - -> t - -(** Like [start_proof] except that there may be dependencies between - initial goals. *) -val start_dependent_proof - : name:Names.Id.t - -> udecl:UState.universe_decl - -> poly:bool - -> Proofview.telescope - -> t - -(** Update the proofs global environment after a side-effecting command - (e.g. a sublemma definition) has been run inside it. Assumes - there_are_pending_proofs. *) -val update_global_env : t -> t - -(* Takes a function to add to the exceptions data relative to the - state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object - -(* Intermediate step necessary to delegate the future. - * Both access the current proof state. The former is supposed to be - * chained with a computation that completed the proof *) - -type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t - -(* If allow_partial is set (default no) then an incomplete proof - * is allowed (no error), and a warn is given if the proof is complete. *) -val return_proof : ?allow_partial:bool -> t -> closed_proof_output -val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> proof_object - -val get_open_goals : t -> int - -val map_proof : (Proof.t -> Proof.t) -> t -> t -val map_fold_proof : (Proof.t -> Proof.t * 'a) -> t -> t * 'a -val map_fold_proof_endline : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a - -(** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Genarg.glob_generic_argument -> t -> t - -(** Sets the section variables assumed by the proof, returns its closure - * (w.r.t. type dependencies and let-ins covered by it) + a list of - * ids to be cleared *) -val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 0ce726db25..756fef0511 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -6,9 +6,7 @@ Proof Logic Goal_select Proof_bullet -Proof_global Refiner Tacmach -Pfedit Clenv Clenvtac diff --git a/proofs/refiner.ml b/proofs/refiner.ml index e1896d51e3..832a749ef2 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -89,7 +89,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = let gll = (List.map_i (fun i -> apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) - 0 gs) in + 0 gs) in (sigr,List.flatten gll) (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) @@ -188,13 +188,13 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun hypl -> List.subtract cmp hypl oldhyps) hyps in - let s = + let s = let frst = ref true in List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) - "" lh)) + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) + "" lh)) "" newhyps in Feedback.msg_notice (str "<infoH>" @@ -273,5 +273,5 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -let tclPUSHEVARUNIVCONTEXT ctx gl = +let tclPUSHEVARUNIVCONTEXT ctx gl = tclEVARS (Evd.merge_universe_context (project gl) ctx) gl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index def67abad7..aed1c89bfe 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -43,7 +43,7 @@ val pf_get_hyp_typ : Goal.goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a -val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> +val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> Goal.goal sigma -> 'a -> Goal.goal sigma * 'b val pf_reduce : (env -> evar_map -> constr -> constr) -> |