diff options
Diffstat (limited to 'proofs')
32 files changed, 5379 insertions, 0 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml new file mode 100644 index 0000000000..1f1bdf4da7 --- /dev/null +++ b/proofs/clenv.ml @@ -0,0 +1,720 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 CErrors +open Util +open Names +open Nameops +open Termops +open Constr +open Namegen +open Environ +open Evd +open EConstr +open Vars +open Reduction +open Reductionops +open Tacred +open Pretype_errors +open Evarutil +open Unification +open Tactypes + +(******************************************************************) +(* Clausal environments *) + +type clausenv = { + env : env; + evd : evar_map; + templval : constr freelisted; + templtyp : constr freelisted } + +let cl_env ce = ce.env +let cl_sigma ce = ce.evd + +let clenv_nf_meta clenv c = nf_meta clenv.evd c +let clenv_term clenv c = meta_instance clenv.evd c +let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv +let clenv_value clenv = meta_instance clenv.evd clenv.templval +let clenv_type clenv = meta_instance clenv.evd clenv.templtyp + +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 + +let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t + +let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c + +exception NotExtensibleClause + +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 + | Cast (t,_,_) -> clrec t + | Prod (na,t,u) -> + 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 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 } + | _ -> raise NotExtensibleClause + in clrec typ + +(* Instantiate the first [bound] products of [t] with metas (all products if + [bound] is [None]; unfold local defs *) + +(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where + [lmetas] is a list of metas to be applied to a proof of [t] so that + it produces the unification pattern [ccl]; [sigma'] is [sigma] + extended with [lmetas]; if [n] is defined, it limits the size of + the list even if [ccl] is still a product; otherwise, it stops when + [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] + and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and + [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] + and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) + +let clenv_environments evd bound t = + let open EConstr in + let open Vars in + let rec clrec (e,metas) n t = + match n, EConstr.kind evd t with + | (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 na' = if dep then na 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) + | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t) + | (n, _) -> (e, List.rev metas, t) + in + clrec (evd,[]) bound t + +let mk_clenv_from_env env sigma n (c,cty) = + let evd = clear_metas sigma in + let (evd,args,concl) = clenv_environments evd n cty in + { templval = mk_freelisted (applist (c,args)); + templtyp = mk_freelisted concl; + evd = evd; + env = env } + +let mk_clenv_from_n gls n (c,cty) = + let env = Proofview.Goal.env gls in + let sigma = Tacmach.New.project gls in + mk_clenv_from_env env sigma n (c, cty) + +let mk_clenv_from gls = mk_clenv_from_n gls None + +let mk_clenv_type_of gls t = mk_clenv_from gls (t,Tacmach.New.pf_unsafe_type_of gls t) + +(******************************************************************) + +(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions + * mv0, or if one of the free vars on mv1's freelist mentions + * mv0 *) + +let mentions clenv mv0 = + let rec menrec mv1 = + Int.equal mv0 mv1 || + let mlist = + try match meta_opt_fvalue clenv.evd mv1 with + | Some (b,_) -> b.freemetas + | None -> Metaset.empty + with Not_found -> Metaset.empty in + Metaset.exists menrec mlist + in menrec + +let error_incompatible_inst clenv mv = + let na = meta_name clenv.evd mv in + match na with + Name id -> + user_err ~hdr:"clenv_assign" + (str "An incompatible instantiation has already been found for " ++ + Id.print id) + | _ -> + anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.") + +(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) +let clenv_assign mv rhs clenv = + let rhs_fls = mk_freelisted rhs in + if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then + user_err Pp.(str "clenv_assign: circularity in unification"); + try + if meta_defined clenv.evd mv 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 (rhs_fls.rebus,st) clenv.evd} + with Not_found -> + user_err Pp.(str "clenv_assign: undefined meta") + + + +(* [clenv_dependent hyps_only clenv] + * returns a list of the metavars which appear in the template of clenv, + * and which are dependent, This is computed by taking the metavars of the + * template in right-to-left order, and collecting the metavars which appear + * in their types, and adding in all the metavars appearing in the + * type of clenv. + * If [hyps_only] then metavariables occurring in the concl are _excluded_ + * If [iter] is also set then all metavariables *recursively* occurring + * in the concl are _excluded_ + + Details of the strategies used for computing the set of unresolved + dependent metavariables + + We typically have a clause of the form + + lem(?T:Type,?T,?U:Type,?V:Type,?x:?T,?y:?U,?z:?V,?H:hyp(?x,?z)) :concl(?y,?z) + + Then, we compute: + A = the set of all unresolved metas + C = the set of metas occurring in concl (here ?y, ?z) + C* = the recursive closure of C wrt types (here ?y, ?z, ?U, ?V) + D = the set of metas occurring in a type of meta (here ?x, ?T, ?z, ?U, ?V) + NL = the set of duplicated metas even if non dependent (here ?T) + (we make the assumption that duplicated metas have internal dependencies) + + Then, for the "apply"-style tactic (hyps_only), missing metas are + A inter ((D minus C) union NL) + + for the optimized "apply"-style tactic (taking in care, f_equal style + lemma, from 2/8/10, Coq > 8.3), missing metas are + A inter (( D minus C* ) union NL) + + for the "elim"-style tactic, missing metas are + A inter (D union C union NL) + + In any case, we respect the order given in A. +*) + +let clenv_metas_in_type_of_meta evd mv = + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas + +let dependent_in_type_of_metas clenv mvs = + List.fold_right + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.evd mv)) + mvs Metaset.empty + +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)) + mvs acc in + aux mvs mvs + +let clenv_dependent_gen hyps_only ?(iter=true) clenv = + let all_undefined = undefined_metas clenv.evd in + let deps_in_concl = (mk_freelisted (clenv_type clenv)).freemetas in + let deps_in_hyps = dependent_in_type_of_metas clenv all_undefined in + let deps_in_concl = + if hyps_only && iter then dependent_closure clenv deps_in_concl + else deps_in_concl in + List.filter + (fun mv -> + if hyps_only then + 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) + all_undefined + +let clenv_missing ce = clenv_dependent_gen true ce +let clenv_dependent ce = clenv_dependent_gen false ce + +(******************************************************************) + +let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv = + { clenv with + evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 } + +let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = + { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } + +let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then + clenv_unify CUMUL ~flags (clenv_type clenv) concl + (clenv_unify_meta_types ~flags clenv) + else + clenv_unify CUMUL ~flags + (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv + +let old_clenv_unique_resolver ?flags clenv gl = + let concl = Goal.V82.concl clenv.evd (sig_it gl) in + clenv_unique_resolver_gen ?flags clenv concl + +let clenv_unique_resolver ?flags clenv gl = + let concl = Proofview.Goal.concl gl in + clenv_unique_resolver_gen ?flags clenv concl + +let adjust_meta_source evd mv = function + | loc,Evar_kinds.VarInstance id -> + let rec match_name c l = + match EConstr.kind evd c, l with + | Lambda (Name id,_,c), a::l when EConstr.eq_constr evd a (mkMeta mv) -> Some id + | Lambda (_,_,c), a::l -> match_name c l + | _ -> None in + (* This is very ad hoc code so that an evar inherits the name of the binder + 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 t.rebus in + match EConstr.kind evd f with + | Meta mv'' -> + (match meta_opt_fvalue evd mv'' with + | Some (c,_) -> match_name c.rebus l + | None -> None) + | _ -> None + else None in + let id = try List.find_map f (Evd.meta_list evd) with Not_found -> id in + loc,Evar_kinds.VarInstance id + | src -> src + +(* [clenv_pose_metas_as_evars clenv dep_mvs] + * For each dependent evar in the clause-env which does not have a value, + * pose a value for it by constructing a fresh evar. We do this in + * left-to-right order, so that every evar's type is always closed w.r.t. + * metas. + + * Node added 14/4/08 [HH]: before this date, evars were collected in + clenv_dependent by collect_metas in the fold_constr order which is + (almost) the left-to-right order of dependencies in term. However, + due to K-redexes, collect_metas was sometimes missing some metas. + The call to collect_metas has been replaced by a call to + undefined_metas, but then the order was the one of definition of + the metas (numbers in increasing order) which is _not_ the + dependency order when a clenv_fchain occurs (because clenv_fchain + plugs a term with a list of consecutive metas in place of a - a priori - + arbitrary metavariable belonging to another sequence of consecutive metas: + e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of + (nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2). + To ensure the dependency order, we check that the type of each meta + to pose is already meta-free, otherwise we postpone the transformation, + hoping that no cycle may happen. + + Another approach could have been to use decimal numbers for metas so that + in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2) + then making the numeric order match the dependency order. +*) + +let clenv_pose_metas_as_evars clenv dep_mvs = + let rec fold clenv evs = function + | [] -> clenv, evs + | mv::mvs -> + let ty = clenv_meta_type clenv mv in + (* Postpone the evar-ization if dependent on another meta *) + (* This assumes no cycle in the dependencies - is it correct ? *) + if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv]) + else + 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 + fold clenv (fst (destEvar evd evar) :: evs) mvs in + fold clenv [] dep_mvs + +(******************************************************************) + +(* [clenv_fchain mv clenv clenv'] + * + * Resolves the value of "mv" (which must be undefined) in clenv to be + * the template of clenv' be the value "c", applied to "n" fresh + * metavars, whose types are chosen by destructing "clf", which should + * be a clausale forme generated from the type of "c". The process of + * resolution can cause unification of already-existing metavars, and + * of the fresh ones which get created. This operation is a composite + * of operations which pose new metavars, perform unification on + * terms, and make bindings. + + Otherwise said, from + + [clenv] = [env;sigma;metas |- c:T] + [clenv'] = [env';sigma';metas' |- d:U] + [mv] = [mi] of type [Ti] in [metas] + + then, if the unification of [Ti] and [U] produces map [rho], the + chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for + [rho'] being [rho;mi:=d]. + + In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma]. +*) + +let fchain_flags () = + { (default_unify_flags ()) with + allow_K_in_toplevel_higher_order_unification = true } + +let clenv_fchain ?with_univs ?(flags=fchain_flags ()) mv clenv nextclenv = + (* Add the metavars of [nextclenv] to [clenv], with their name-environment *) + let clenv' = + { templval = clenv.templval; + templtyp = clenv.templtyp; + evd = meta_merge ?with_univs nextclenv.evd clenv.evd; + env = nextclenv.env } in + (* unify the type of the template of [nextclenv] with the type of [mv] *) + let clenv'' = + clenv_unify ~flags CUMUL + (clenv_term clenv' nextclenv.templtyp) + (clenv_meta_type clenv' mv) + clenv' in + (* assign the metavar *) + let clenv''' = + clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv'' + in + clenv''' + +(***************************************************************) +(* Bindings *) + +type arg_bindings = constr explicit_bindings + +(* [clenv_independent clenv] + * returns a list of metavariables which appear in the term cval, + * and which are not dependent. That is, they do not appear in + * the types of other metavars which are in cval, nor in the type + * of cval, ctyp. *) + +let clenv_independent clenv = + let mvs = collect_metas clenv.evd (clenv_value clenv) in + let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in + let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in + List.filter (fun mv -> not (Metaset.mem mv deps)) mvs + +let qhyp_eq h1 h2 = match h1, h2 with +| NamedHyp n1, NamedHyp n2 -> Id.equal n1 n2 +| AnonHyp i1, AnonHyp i2 -> Int.equal i1 i2 +| _ -> false + +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."); + | AnonHyp n :: _ -> + user_err + (str "The position " ++ int n ++ + str " occurs more than once in binding list.") + | [] -> () + +let explain_no_such_bound_variable evd id = + let fold l (n, clb) = + let na = match clb with + | Cltyp (na, _) -> na + | Clval (na, _, _) -> na + in + if na != Anonymous then Name.get_id na :: l else l + in + let mvl = List.fold_left fold [] (Evd.meta_list evd) in + user_err ~hdr:"Evd.meta_with_name" + (str"No such bound variable " ++ Id.print id ++ + (if mvl == [] then str " (no bound variables at all in the expression)." + else + (str" (possible name" ++ + str (if List.length mvl == 1 then " is: " else "s are: ") ++ + pr_enum Id.print mvl ++ str")."))) + +let meta_with_name evd id = + let na = Name id in + let fold (l1, l2 as l) (n, clb) = + let (na',def) = match clb with + | Cltyp (na, _) -> (na, false) + | Clval (na, _, _) -> (na, true) + in + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l + in + let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in + match mvnodef, mvl with + | _,[] -> + explain_no_such_bound_variable evd id + | ([n],_|_,[n]) -> + n + | _ -> + user_err ~hdr:"Evd.meta_with_name" + (str "Binder name \"" ++ Id.print id ++ + strbrk "\" occurs more than once in clause.") + +let meta_of_binder clause loc mvs = function + | NamedHyp s -> meta_with_name clause.evd s + | AnonHyp n -> + try List.nth mvs (n-1) + with (Failure _|Invalid_argument _) -> + user_err (str "No such binder.") + +let error_already_defined b = + match b with + | NamedHyp id -> + user_err + (str "Binder name \"" ++ Id.print id ++ + str"\" already defined with incompatible value.") + | AnonHyp n -> + anomaly + (str "Position " ++ int n ++ str" already defined.") + +let clenv_unify_binding_type clenv c t u = + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then + (* Not enough information to know if some subtyping is needed *) + CoerceToType, clenv, c + else + (* Enough information so as to try a coercion now *) + try + let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in + TypeProcessed, { clenv with evd = evd }, c + with + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> + raise e + | e when precatchable_exception e -> + TypeNotProcessed, clenv, c + +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 + { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } + +let clenv_match_args bl clenv = + if List.is_empty bl then + clenv + else + let mvs = clenv_independent clenv in + check_bindings bl; + List.fold_left + (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 (fst (meta_fvalue clenv.evd k)).rebus c then clenv + else error_already_defined b + else + clenv_assign_binding clenv k c) + clenv bl + +exception NoSuchBinding + +let clenv_constrain_last_binding c clenv = + let all_mvs = collect_metas clenv.evd clenv.templval.rebus in + let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in + clenv_assign_binding clenv k c + +let error_not_right_number_missing_arguments n = + user_err + (strbrk "Not the right number of missing arguments (expected " ++ + int n ++ str ").") + +let clenv_constrain_dep_args hyps_only bl clenv = + if List.is_empty bl then + clenv + else + let occlist = clenv_dependent_gen hyps_only clenv in + if Int.equal (List.length occlist) (List.length bl) then + 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) + else + error_not_right_number_missing_arguments (List.length occlist) + +(****************************************************************) +(* Clausal environment for an application *) + +let make_clenv_binding_gen hyps_only n env sigma (c,t) = function + | ImplicitBindings largs -> + let clause = mk_clenv_from_env env sigma n (c,t) in + clenv_constrain_dep_args hyps_only largs clause + | 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) + in clenv_match_args lbind clause + | NoBindings -> + mk_clenv_from_env env sigma n (c,t) + +let make_clenv_binding_env_apply env sigma n = + make_clenv_binding_gen true n env sigma + +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 + +(****************************************************************) +(* Pretty-print *) + +let pr_clenv clenv = + h 0 + (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.env clenv.evd) + +(****************************************************************) +(** Evar version of mk_clenv *) + +type hole = { + hole_evar : EConstr.constr; + hole_type : EConstr.types; + hole_deps : bool; + hole_name : Name.t; +} + +type clause = { + cl_holes : hole list; + cl_concl : EConstr.types; +} + +let make_evar_clause env sigma ?len t = + let open EConstr in + let open Vars in + let bound = match len with + | None -> -1 + | Some n -> assert (0 <= n); n + in + (* FIXME: do the renaming online *) + let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in + let rec clrec (sigma, holes) inst n t = + if n = 0 then (sigma, holes, t) + else match EConstr.kind sigma t with + | Cast (t, _, _) -> clrec (sigma, holes) inst n t + | Prod (na, t1, t2) -> + (* Share the evar instances as we are living in the same context *) + let inst, ctx, args, subst = match inst with + | None -> + (* Dummy type *) + let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in + Some (ctx, args, subst), ctx, args, subst + | Some (ctx, args, subst) -> inst, ctx, args, subst + in + let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in + let dep = not (noccurn sigma 1 t2) in + let hole = { + hole_evar = ev; + hole_type = t1; + hole_deps = dep; + (* We fix it later *) + hole_name = na; + } in + let t2 = if dep then subst1 ev t2 else t2 in + clrec (sigma, hole :: holes) inst (pred n) t2 + | LetIn (na, b, _, t) -> clrec (sigma, holes) inst n (subst1 b t) + | _ -> (sigma, holes, t) + in + let (sigma, holes, t) = clrec (sigma, []) None bound t in + let holes = List.rev holes in + let clause = { cl_concl = t; cl_holes = holes } in + (sigma, clause) + +let explain_no_such_bound_variable holes id = + let fold h accu = match h.hole_name with + | Anonymous -> accu + | Name id -> id :: accu + in + let mvl = List.fold_right fold holes [] in + let expl = match mvl with + | [] -> str " (no bound variables at all in the expression)." + | [id] -> str "(possible name is: " ++ Id.print id ++ str ")." + | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")." + in + user_err (str "No such bound variable " ++ Id.print id ++ expl) + +let evar_with_name holes id = + let map h = match h.hole_name with + | Anonymous -> None + | Name id' -> if Id.equal id id' then Some h else None + in + let hole = List.map_filter map holes in + match hole with + | [] -> explain_no_such_bound_variable holes id + | [h] -> h.hole_evar + | _ -> + user_err + (str "Binder name \"" ++ Id.print id ++ + str "\" occurs more than once in clause.") + +let evar_of_binder holes = function +| NamedHyp s -> evar_with_name holes s +| AnonHyp n -> + try + let nondeps = List.filter (fun hole -> not hole.hole_deps) holes in + let h = List.nth nondeps (pred n) in + h.hole_evar + with e when CErrors.noncritical e -> + user_err (str "No such binder.") + +let define_with_type sigma env ev c = + let open EConstr in + let t = Retyping.get_type_of env sigma ev in + let ty = Retyping.get_type_of env sigma c in + 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 j.Environ.uj_val sigma in + sigma + +let solve_evar_clause env sigma hyp_only clause = function +| NoBindings -> sigma +| ImplicitBindings largs -> + let open EConstr in + let fold holes h = + if h.hole_deps then + (* Some subsequent term uses the hole *) + let (ev, _) = destEvar sigma h.hole_evar in + let is_dep hole = occur_evar sigma ev hole.hole_type in + let in_hyp = List.exists is_dep holes in + let in_ccl = occur_evar sigma ev clause.cl_concl in + let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in + let h = { h with hole_deps = dep } in + h :: holes + else + (* The hole does not occur anywhere *) + h :: holes + in + let holes = List.fold_left fold [] (List.rev clause.cl_holes) in + let map h = if h.hole_deps then Some h.hole_evar else None in + let evs = List.map_filter map holes in + let len = List.length evs in + if Int.equal len (List.length largs) then + let fold sigma ev arg = define_with_type sigma env ev arg in + let sigma = List.fold_left2 fold sigma evs largs in + sigma + else + error_not_right_number_missing_arguments len +| ExplicitBindings lbind -> + let () = check_bindings lbind in + let fold sigma {CAst.v=(binder, c)} = + let ev = evar_of_binder clause.cl_holes binder in + define_with_type sigma env ev c + in + let sigma = List.fold_left fold sigma lbind in + sigma diff --git a/proofs/clenv.mli b/proofs/clenv.mli new file mode 100644 index 0000000000..03acb9e46e --- /dev/null +++ b/proofs/clenv.mli @@ -0,0 +1,173 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 file defines clausenv, which is a deprecated way to handle open terms + in the proof engine. Most of the API here is legacy except for the + evar-based clauses. *) + +open Names +open Constr +open Environ +open Evd +open EConstr +open Unification +open Tactypes + +(** {6 The Type of Constructions clausale environments.} *) + +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 *) + templtyp : constr freelisted (** its type *)} + + +(** subject of clenv (instantiated) *) +val clenv_value : clausenv -> constr + +(** type of clenv (instantiated) *) +val clenv_type : clausenv -> types + +(** substitute resolved metas *) +val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr + +(** type of a meta in clenv context *) +val clenv_meta_type : clausenv -> metavariable -> types + +val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from_n : + Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv +val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv + +(** Refresh the universes in a clenv *) +val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst + +(** {6 linking of clenvs } *) + +val clenv_fchain : + ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv + +(** {6 Unification with clenvs } *) + +(** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) +val clenv_unify : + ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv + +(** unifies the concl of the goal with the type of the clenv *) +val old_clenv_unique_resolver : + ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv + +val clenv_unique_resolver : + ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv + +val clenv_dependent : clausenv -> metavariable list + +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list + +(** {6 Bindings } *) + +type arg_bindings = constr explicit_bindings + +(** bindings where the key is the position in the template of the + clenv (dependent or not). Positions can be negative meaning to + start from the rightmost argument of the template. *) +val clenv_independent : clausenv -> metavariable list +val clenv_missing : clausenv -> metavariable list + +(** for the purpose of inversion tactics *) +exception NoSuchBinding +val clenv_constrain_last_binding : constr -> clausenv -> clausenv + +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 + use all of them if None *) +val make_clenv_binding_env_apply : + env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> + clausenv + +val make_clenv_binding_apply : + env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> + clausenv + +val make_clenv_binding_env : + env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv + +val make_clenv_binding : + env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv + +(** if the clause is a product, add an extra meta for this product *) +exception NotExtensibleClause +val clenv_push_prod : clausenv -> clausenv + +(** {6 Pretty-print (debug only) } *) +val pr_clenv : clausenv -> Pp.t + +(** {6 Evar-based clauses} *) + +(** The following code is an adaptation of the [make_clenv_*] functions above, + except that it uses evars instead of metas, and naturally fits in the new + refinement monad. It should eventually replace all uses of the + aforementioned functions. + + A clause is constructed as follows: assume a type [t := forall (x1 : A1) ... + (xn : An), T], we instantiate all the [xi] with a fresh evar [ei] and + return [T(xi := ei)] together with the [ei] enriched with a bit of + additional data. This is the simple part done by [make_evar_clause]. + + The problem lies in the fact we want to solve such holes with some + [constr bindings]. This entails some subtleties, because the provided terms + may only be well-typed up to a coercion, which we can only infer if we have + enough typing information. The meta machinery could insert coercions through + tricky instantiation delays. The only solution we have now is to delay the + tentative resolution of clauses by providing the [solve_evar_clause] + function, to be called at a smart enough time. +*) + +type hole = { + hole_evar : EConstr.constr; + (** The hole itself. Guaranteed to be an evar. *) + hole_type : EConstr.types; + (** Type of the hole in the current environment. *) + hole_deps : bool; + (** Whether the remainder of the clause was dependent in the hole. Note that + because let binders are substituted, it does not mean that it actually + appears somewhere in the returned clause. *) + hole_name : Name.t; + (** Name of the hole coming from its binder. *) +} + +type clause = { + cl_holes : hole list; + cl_concl : EConstr.types; +} + +val make_evar_clause : env -> evar_map -> ?len:int -> EConstr.types -> + (evar_map * clause) +(** An evar version of {!make_clenv_binding}. Given a type [t], + [evar_environments env sigma ~len t bl] tries to eliminate at most [len] + products of the type [t] by filling it with evars. It returns the resulting + type together with the list of holes generated. Assumes that [t] is + well-typed in the environment. *) + +val solve_evar_clause : env -> evar_map -> bool -> clause -> EConstr.constr bindings -> + evar_map +(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained + in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in + the environment. The boolean [hyps] is a compatibility flag that allows to + consider arguments to be dependent only when they appear in hypotheses and + not in the conclusion. This boolean is only used when [bl] is of the form + [ImplicitBindings _]. *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml new file mode 100644 index 0000000000..c36b0fa337 --- /dev/null +++ b/proofs/clenvtac.ml @@ -0,0 +1,135 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Util +open Constr +open Termops +open Evd +open EConstr +open Refiner +open Logic +open Reduction +open Clenv + +(* This function put casts around metavariables whose type could not be + * infered by the refiner, that is head of applications, predicates and + * subject of Cases. + * Does check that the casted type is closed. Anyway, the refiner would + * fail in this case... *) + +let clenv_cast_meta clenv = + let rec crec u = + match EConstr.kind clenv.evd u with + | App _ | Case _ -> crec_hd u + | Cast (c,_,_) when isMeta clenv.evd c -> u + | Proj (p, c) -> mkProj (p, crec_hd c) + | _ -> EConstr.map clenv.evd crec u + + and crec_hd u = + match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with + | Meta mv -> + (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 + else mkCast (mkMeta mv, DEFAULTcast, b) + 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) + | Proj (p, c) -> mkProj (p, crec_hd c) + | _ -> u + in + crec + +let clenv_value_cast_meta clenv = + clenv_cast_meta clenv (clenv_value 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 + raise + (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); + clenv_pose_metas_as_evars clenv dep_mvs + +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, evars = clenv_pose_dependent_evars ~with_evars clenv in + let evd' = + if with_classes then + let evd' = + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars + ~fail:(not with_evars) clenv.env clenv.evd + in + Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd' + else clenv.evd + in + let clenv = { clenv with evd = evd' } in + tclTHEN + (tclEVARS (Evd.clear_metas evd')) + (refiner ~check:false EConstr.Unsafe.(to_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl + end + +let clenv_pose_dependent_evars ?(with_evars=false) clenv = + fst (clenv_pose_dependent_evars ~with_evars clenv) + +open Unification + +let dft = default_unify_flags + +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 + end + +(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en + particulier ne semblent pas vérifier que des instances différentes + d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas + provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) + +let fail_quick_core_unif_flags = { + modulo_conv_on_closed_terms = Some TransparentState.full; + use_metas_eagerly_in_conv_on_closed_terms = false; + use_evars_eagerly_in_conv_on_closed_terms = false; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; + check_applied_meta_types = false; + use_pattern_unification = false; + use_meta_bound_pattern_unification = true; (* ? *) + frozen_evars = Evar.Set.empty; + restrict_conv_on_strict_subterms = false; (* ? *) + modulo_betaiota = false; + modulo_eta = true; +} + +let fail_quick_unif_flags = { + core_unify_flags = fail_quick_core_unif_flags; + merge_unify_flags = fail_quick_core_unif_flags; + subterm_unify_flags = fail_quick_core_unif_flags; + allow_K_in_toplevel_higher_order_unification = false; + resolve_evars = false +} + +(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) +let unify ?(flags=fail_quick_unif_flags) m = + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let n = Tacmach.New.pf_concl gl in + 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' + with e when CErrors.noncritical e -> Proofview.tclZERO e + end diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli new file mode 100644 index 0000000000..d178478425 --- /dev/null +++ b/proofs/clenvtac.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(** Legacy components of the previous proof engine. *) + +open Clenv +open EConstr +open Unification + +(** Tactics *) +val unify : ?flags:unify_flags -> constr -> 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 : ?with_evars:bool -> clausenv -> clausenv +val clenv_value_cast_meta : clausenv -> constr diff --git a/proofs/doc.tex b/proofs/doc.tex new file mode 100644 index 0000000000..431027ef02 --- /dev/null +++ b/proofs/doc.tex @@ -0,0 +1,14 @@ + +\newpage +\section*{The Proof Engine} + +\ocwsection \label{proofs} +This chapter describes the \Coq\ proof engine, which is also called +the ``refiner'', since it provides a way to build terms by successive +refining steps. Those steps are either primitive rules or higher-level +tactics. +The modules of the proof engine are organized as follows. + +\bigskip +\begin{center}\epsfig{file=proofs.dep.ps,width=\linewidth}\end{center} + diff --git a/proofs/dune b/proofs/dune new file mode 100644 index 0000000000..679c45f6bf --- /dev/null +++ b/proofs/dune @@ -0,0 +1,6 @@ +(library + (name proofs) + (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure") + (public_name coq.proofs) + (wrapped false) + (libraries interp)) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml new file mode 100644 index 0000000000..6c4193c66b --- /dev/null +++ b/proofs/evar_refiner.ml @@ -0,0 +1,65 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 CErrors +open Util +open Evd +open Evarutil +open Evarsolve +open Pp +open Glob_term +open Ltac_pretype + +(******************************************) +(* Instantiation of existential variables *) +(******************************************) + +type glob_constr_ltac_closure = ltac_var_map * glob_constr + +let depends_on_evar sigma evk _ (pbty,_,t1,t2) = + try Evar.equal (head_evar sigma t1) evk + with NoHeadEvar -> + try Evar.equal (head_evar sigma t2) evk + with NoHeadEvar -> false + +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 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 TransparentState.full env evd pbty t1 t2 + | UnifFailure _ as x -> x) (Success evd) + pbs + with + | Success evd -> evd + | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.") + +let w_refine (evk,evi) (ltac_var,rawc) sigma = + if Evd.is_defined sigma evk then + user_err Pp.(str "Instantiate called on already-defined evar"); + let env = Evd.evar_filtered_env evi in + let sigma',typed_c = + let flags = { + Pretyping.use_typeclasses = true; + Pretyping.solve_unification_constraints = true; + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } in + try Pretyping.understand_ltac flags + 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 + (str "Instance is not well-typed in the environment of " ++ + Termops.pr_existential_key sigma evk ++ str ".") + in + define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli new file mode 100644 index 0000000000..e8f3c4d173 --- /dev/null +++ b/proofs/evar_refiner.mli @@ -0,0 +1,20 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Evd +open Glob_term +open Ltac_pretype + +(** Refinement of existential variables. *) + +type glob_constr_ltac_closure = ltac_var_map * glob_constr + +val w_refine : Evar.t * evar_info -> + glob_constr_ltac_closure -> evar_map -> evar_map diff --git a/proofs/goal.ml b/proofs/goal.ml new file mode 100644 index 0000000000..7245d4a004 --- /dev/null +++ b/proofs/goal.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Util +open Pp + +module NamedDecl = Context.Named.Declaration + +(* This module implements the abstract interface to goals *) +(* A general invariant of the module, is that a goal whose associated + evar is defined in the current evar_map, should not be accessed. *) + +(* type of the goals *) +type goal = Evar.t + +let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e) + +let uid e = string_of_int (Evar.repr e) + +(* 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 = struct + + (* Old style env primitive *) + let env evars gl = + let evi = Evd.find evars gl in + Evd.evar_filtered_env evi + + (* Old style hyps primitive *) + let hyps evars gl = + let evi = Evd.find evars gl in + Evd.evar_filtered_hyps evi + + (* same as [hyps], but ensures that existential variables are + normalised. *) + let nf_hyps evars gl = + let hyps = Environ.named_context_of_val (hyps evars gl) in + Environ.val_of_named_context (Evarutil.nf_named_context_evar evars hyps) + + (* Access to ".evar_concl" *) + let concl evars gl = + let evi = Evd.find evars gl in + evi.Evd.evar_concl + + (* Old style mk_goal primitive *) + let mk_goal evars hyps concl = + (* A goal created that way will not be used by refine and will not + 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 prev_future_goals = Evd.save_future_goals evars in + let evi = { Evd.evar_hyps = hyps; + Evd.evar_concl = concl; + Evd.evar_filter = Evd.Filter.identity; + Evd.evar_body = Evd.Evar_empty; + Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); + Evd.evar_candidates = None } + in + let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in + let evars = Evd.restore_future_goals evars prev_future_goals in + let ctxt = Environ.named_context_of_val hyps in + let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in + let ev = EConstr.mkEvar (evk,inst) in + (evk, ev, evars) + + (* Instantiates a goal with an open term *) + let partial_solution env sigma evk c = + (* Check that the goal itself does not appear in the refined term *) + let _ = + if not (Evarutil.occur_evar_upto sigma evk c) then () + else Pretype_errors.error_occur_check env sigma evk c + in + Evd.define evk c sigma + + (* Instantiates a goal with an open term, using name of goal for evk' *) + let partial_solution_to env sigma evk evk' c = + let id = Evd.evar_ident evk sigma in + let sigma = partial_solution env sigma evk c in + match id with + | None -> sigma + | Some id -> Evd.rename evk' id sigma + + (* Parts of the progress tactical *) + let same_goal evars1 gl1 evars2 gl2 = + let evi1 = Evd.find evars1 gl1 in + let evi2 = Evd.find evars2 gl2 in + 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 = + match glss.Evd.it with + | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it) + | _ -> true + + let progress glss gls = + weak_progress glss gls + (* spiwack: progress normally goes like this: + (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls) + This is immensly slow in the current implementation. Maybe we could + reimplement progress_evar_map with restricted folds like "fold_undefined", + with a good implementation of them. + *) + + (* Used by the compatibility layer and typeclasses *) + let nf_evar sigma gl = + let evi = Evd.find sigma gl in + let evi = Evarutil.nf_evar_info sigma evi in + let sigma = Evd.add sigma gl evi in + (gl, sigma) + + (* Goal represented as a type, doesn't take into account section variables *) + let abstract_type sigma gl = + let open EConstr in + let (gl,sigma) = nf_evar sigma gl in + let env = env sigma gl in + let genv = Global.env () in + let is_proof_var decl = + 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 + let decl = Termops.map_named_decl EConstr.of_constr decl in + mkNamedProd_or_LetIn decl t + else + t + ) ~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 new file mode 100644 index 0000000000..af9fb662bf --- /dev/null +++ b/proofs/goal.mli @@ -0,0 +1,71 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 implements the abstract interface to goals. Most of the code + here is useless and should be eventually removed. Consider using + {!Proofview.Goal} instead. *) + +type goal = Evar.t + +(* Gives a unique identifier to each goal. The identifier is + guaranteed to contain no space. *) +val uid : goal -> string + +(* Debugging help *) +val pr_goal : goal -> Pp.t + +(* 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 + + (* Old style env primitive *) + val env : Evd.evar_map -> goal -> Environ.env + + (* Old style hyps primitive *) + val hyps : Evd.evar_map -> goal -> Environ.named_context_val + + (* same as [hyps], but ensures that existential variables are + normalised. *) + val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val + + (* Access to ".evar_concl" *) + val concl : Evd.evar_map -> goal -> EConstr.constr + + (* 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 -> + Environ.named_context_val -> + EConstr.constr -> + goal * EConstr.constr * Evd.evar_map + + (* Instantiates a goal with an open term *) + val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map + + (* Instantiates a goal with an open term, reusing name of goal for + second goal *) + val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map + + (* Principal part of the progress tactical *) + val progress : goal list Evd.sigma -> goal Evd.sigma -> bool + + (* Principal part of tclNOTSAMEGOAL *) + val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool + + (* Used by the compatibility layer and typeclasses *) + 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 + +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 0000000000..cef3fd3f5e --- /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 *) +(* <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 Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +(* Default goal selector: selector chosen when a tactic is applied + without an explicit selector. *) +let default_goal_selector = ref (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 + | SelectAlreadyFocused -> 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 0000000000..b1c5723885 --- /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 *) +(* <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 Names + +(* spiwack: I'm choosing, for now, to have [goal_selector] be a + different type than [goal_reference] mostly because if it makes sense + to print a goal that is out of focus (or already solved) it doesn't + make sense to apply a tactic to it. Hence it the types may look very + similar, they do not seem to mean the same thing. *) +type t = + | SelectAlreadyFocused + | SelectNth of int + | SelectList of (int * int) list + | SelectId of Id.t + | SelectAll + +val pr_goal_selector : t -> Pp.t +val get_default_goal_selector : unit -> t diff --git a/proofs/logic.ml b/proofs/logic.ml new file mode 100644 index 0000000000..3581e90b79 --- /dev/null +++ b/proofs/logic.ml @@ -0,0 +1,598 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 CErrors +open Util +open Names +open Nameops +open Constr +open Vars +open Termops +open Environ +open Reductionops +open Inductiveops +open Typing +open Type_errors +open Retyping + +module NamedDecl = Context.Named.Declaration + +type refiner_error = + + (* Errors raised by the refiner *) + | BadType of constr * constr * constr + | UnresolvedBindings of Name.t list + | CannotApply of constr * constr + | NotWellTyped of constr + | NonLinearProof of constr + | MetaInType of EConstr.constr + + (* Errors raised by the tactics *) + | IntroNeedsProduct + | DoesNotOccurIn of constr * Id.t + | NoSuchHyp of Id.t + +exception RefinerError of Environ.env * Evd.evar_map * refiner_error + +open Pretype_errors + +(** FIXME: this is quite brittle. Why not accept any PretypeError? *) +let is_typing_error = function +| UnexpectedType (_, _) | NotProduct _ +| VarNotFound _ | TypingError _ -> true +| _ -> false + +let is_unification_error = function +| CannotUnify _ | CannotUnifyLocal _| CannotGeneralize _ +| NoOccurrenceFound _ | CannotUnifyBindingType _ +| ActualTypeNotCoercible _ | UnifOccurCheck _ +| CannotFindWellTypedAbstraction _ | WrongAbstractionType _ +| UnsolvableImplicit _| AbstractionOverMeta _ +| UnsatisfiableConstraints _ -> true +| _ -> false + +let catchable_exception = function + | CErrors.UserError _ | TypeError _ + | Proof.OpenProof _ + (* abstract will call close_proof inside a tactic *) + | Notation.PrimTokenNotationError _ + | RefinerError _ | Indrec.RecursionSchemeError _ + | Nametab.GlobalizationError _ + (* reduction errors *) + | Tacred.ReductionTacticError _ -> true + (* unification and typing errors *) + | 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)) + +(* Tells if the refiner should check that the submitted rules do not + produce invalid subgoals *) +let check = ref false +let with_check = Flags.with_option check + +(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and + returns [tail::(f head (id,_,_) (rev tail))] *) +let apply_to_hyp env sigma check sign id f = + try apply_to_hyp sign id f + with Hyp_not_found -> + if check then error_no_such_hypothesis env sigma id + else sign + +let check_typability env sigma c = + if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in () + +(************************************************************************) +(************************************************************************) +(* Implementation of the structural rules (moving and deleting + hypotheses around) *) + +(* The ClearBody tactic *) + +(* Reordering of the context *) + +(* faire le minimum d'echanges pour que l'ordre donne soit un *) +(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *) +(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *) +(* reculees par rapport aux autres (faire le contraire!) *) + +let mt_q = (Id.Map.empty,[]) +let push_val y = function + (_,[] as q) -> q + | (m, (x,l)::q) -> (m, (x,Id.Set.add y l)::q) +let push_item x v (m,l) = + (Id.Map.add x v m, (x,Id.Set.empty)::l) +let mem_q x (m,_) = Id.Map.mem x m +let find_q x (m,q) = + let v = Id.Map.find x m in + let m' = Id.Map.remove x m in + let rec find accs acc = function + [] -> raise Not_found + | [(x',l)] -> + if Id.equal x x' then ((v,Id.Set.union accs l),(m',List.rev acc)) + else raise Not_found + | (x',l as i)::((x'',l'')::q as itl) -> + if Id.equal x x' then + ((v,Id.Set.union accs l), + (m',List.rev acc@(x'',Id.Set.add x (Id.Set.union l l''))::q)) + else find (Id.Set.union l accs) (i::acc) itl in + find Id.Set.empty [] q + +let occur_vars_in_decl env sigma hyps d = + if Id.Set.is_empty hyps then false else + let ohyps = global_vars_set_of_decl env sigma d in + Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps + +let reorder_context env sigma sign ord = + let ords = List.fold_right Id.Set.add ord Id.Set.empty in + if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then + user_err Pp.(str "Order list has duplicates"); + let rec step ord expected ctxt_head moved_hyps ctxt_tail = + match ord with + | [] -> List.rev ctxt_tail @ ctxt_head + | top::ord' when mem_q top moved_hyps -> + let ((d,h),mh) = find_q top moved_hyps in + if occur_vars_in_decl env sigma h d then + user_err ~hdr:"reorder_context" + (str "Cannot move declaration " ++ Id.print top ++ spc() ++ + str "before " ++ + pr_sequence Id.print + (Id.Set.elements (Id.Set.inter h + (global_vars_set_of_decl env sigma d)))); + step ord' expected ctxt_head mh (d::ctxt_tail) + | _ -> + (match ctxt_head with + | [] -> error_no_such_hypothesis env sigma (List.hd ord) + | d :: ctxt -> + let x = NamedDecl.get_id d in + if Id.Set.mem x expected then + step ord (Id.Set.remove x expected) + ctxt (push_item x d moved_hyps) ctxt_tail + else + step ord expected + ctxt (push_val x moved_hyps) (d::ctxt_tail)) in + step ord ords sign mt_q [] + +let reorder_val_context env sigma sign ord = + let open EConstr in + val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) + + + + +let check_decl_position env sigma sign d = + let open EConstr in + let x = NamedDecl.get_id d in + let needed = global_vars_set_of_decl env sigma d in + let deps = dependency_closure env sigma (named_context_of_val sign) needed in + if Id.List.mem x deps then + user_err ~hdr:"Logic.check_decl_position" + (str "Cannot create self-referring hypothesis " ++ Id.print x); + x::deps + +(* Auxiliary functions for primitive MOVE tactic + * + * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves + * hyp [hfrom] at location [hto] which belongs to the hyps on the + * left side [left] of the full signature if [toleft=true] or to the hyps + * 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 +| MoveLast, MoveLast -> true +| MoveFirst, MoveFirst -> true +| _ -> false + +let split_sign env sigma hfrom hto l = + let rec splitrec left toleft = function + | [] -> 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 + let is_toleft = match hto with + | MoveAfter h' | MoveBefore h' -> Id.equal hyp h' + | _ -> false + in + splitrec (d::left) (toleft || is_toleft) + right + in + splitrec [] false l + +let hyp_of_move_location = function + | MoveAfter id -> id + | MoveBefore id -> id + | _ -> assert false + +let move_hyp env sigma toleft (left,declfrom,right) hto = + let test_dep d d2 = + if toleft + then occur_var_in_decl env sigma (NamedDecl.get_id d2) d + else occur_var_in_decl env sigma (NamedDecl.get_id d) d2 + in + let rec moverec first middle = function + | [] -> + 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 + | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> + 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) + else + 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 ".") + 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 + in + let open EConstr in + if toleft then + let right = + List.fold_right push_named_context_val right empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right (moverec [] [declfrom] left) + else + let right = + List.fold_right push_named_context_val + (moverec [] [declfrom] right) empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right left + +let move_hyp_in_named_context env sigma hfrom hto sign = + let open EConstr in + let (left,right,declfrom,toleft) = + split_sign env sigma hfrom hto (named_context_of_val sign) in + move_hyp env sigma toleft (left,declfrom,right) hto + +let insert_decl_in_named_context env sigma decl hto sign = + let open EConstr in + move_hyp env sigma false ([],decl,named_context_of_val sign) hto + +(**********************************************************************) + + +(************************************************************************) +(************************************************************************) +(* Implementation of the logical rules *) + +(* Will only be used on terms given to the Refine rule which have meta +variables only in Application and Case *) + +let error_unsupported_deep_meta c = + user_err (strbrk "Application of lemmas whose beta-iota normal " ++ + strbrk "form contains metavariables deep inside the term is not " ++ + strbrk "supported; try \"refine\" instead.") + +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 + | 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 + List.rev (collrec false [] c) + +let check_meta_variables env sigma c = + if not (List.distinct_f Int.compare (collect_meta_variables c)) then + raise (RefinerError (env, sigma, NonLinearProof c)) + +let check_conv_leq_goal env sigma arg ty conclty = + if !check then + 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 +let meta_free_prefix sigma a = + try + let a = Array.map EConstr.of_constr a in + let _ = Array.fold_left (fun acc a -> + if occur_meta sigma a then raise (Stop acc) + else a :: acc) [] a + in a + with Stop acc -> Array.rev_of_list acc + +let goal_type_of env sigma c = + if !check then + let (sigma,t) = type_of env sigma (EConstr.of_constr c) in + (sigma, EConstr.Unsafe.to_constr t) + else (sigma, EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))) + +let rec mk_refgoals sigma goal goalacc conclty trm = + let env = Goal.V82.env sigma goal in + let hyps = Goal.V82.hyps sigma goal in + let mk_goal hyps concl = + Goal.V82.mk_goal sigma hyps concl + in + if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then + let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in + let t'ty = EConstr.Unsafe.to_constr t'ty in + let sigma = check_conv_leq_goal env sigma trm t'ty conclty in + (goalacc,t'ty,sigma,trm) + else + match kind trm with + | Meta _ -> + let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in + 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 + + | Cast (t,k, 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 + (* 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 + let ans = if ans == t then trm else mkCast(ans,k,ty) in + (gls,cty,sigma,ans) + + | App (f,l) -> + 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 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) + + | 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) = 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) + + | _ -> + 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, + * Metas should be casted. *) + +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 = + Goal.V82.mk_goal sigma hyps concl in + match kind trm with + | Cast (c,_, ty) when isMeta c -> + 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 + + | Cast (t,_, ty) -> + check_typability env sigma ty; + mk_refgoals sigma goal goalacc ty t + + | App (f,l) -> + 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 + let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in + (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'',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) + + | 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) + + | _ -> + 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 + +and mk_arggoals sigma goal goalacc funty allargs = + let foldmap (goalacc, funty, sigma) harg = + let t = whd_all (Goal.V82.env sigma goal) sigma (EConstr.of_constr funty) in + let t = EConstr.Unsafe.to_constr t in + let rec collapse t = match kind t with + | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) + | _ -> t + in + let t = collapse t in + match kind t with + | Prod (_, c1, b) -> + let (acc, hargty, sigma, arg) = mk_refgoals sigma goal goalacc c1 harg in + (acc, subst1 harg b, sigma), arg + | _ -> + let env = Goal.V82.env sigma goal in + raise (RefinerError (env,sigma,CannotApply (t, harg))) + in + 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 + let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in + let ct = EConstr.of_constr ct in + let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in + let ((ind, u), spec) = + try Tacred.find_hnf_rectype env sigma ct + with Not_found -> anomaly (Pp.str "mk_casegoals.") in + let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in + 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 + let b = NamedDecl.get_value d in + let env = Global.env () in + let reorder = ref [] in + let sign' = + apply_to_hyp env sigma check sign id + (fun _ d' _ -> + let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in + let env = Global.env_of_context sign in + if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the type of " ++ Id.print id ++ str "."); + if check && not (Option.equal (is_conv env sigma) b c) then + user_err ~hdr:"Logic.convert_hyp" + (str "Incorrect change of the body of "++ Id.print id ++ str "."); + if check then reorder := check_decl_position env sigma sign d; + map_named_decl EConstr.Unsafe.to_constr d) in + reorder_val_context env sigma sign' !reorder + +(************************************************************************) +(************************************************************************) +(* Primitive tactics are handled here *) + +let prim_refiner r sigma goal = + let env = Goal.V82.env sigma goal in + let cl = Goal.V82.concl sigma goal in + let cl = EConstr.Unsafe.to_constr cl in + check_meta_variables env sigma r; + let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl r in + let sgl = List.rev sgl in + let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in + (sgl, sigma) + +let prim_refiner ~check r sigma goal = + if check then + with_check (prim_refiner r sigma) goal + else + prim_refiner r sigma goal diff --git a/proofs/logic.mli b/proofs/logic.mli new file mode 100644 index 0000000000..f99076db23 --- /dev/null +++ b/proofs/logic.mli @@ -0,0 +1,73 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(** Legacy proof engine. Do not use in newly written code. *) + +open Names +open Constr +open Evd + +(** [check] respectively means:\\ + [Intro]: check that the name does not exist\\ + [Intro_after]: check that the name does not exist and that variables in + its type does not escape their scope\\ + [Intro_replacing]: check that the name does not exist and that + variables in its type does not escape their scope\\ + [Convert_hyp]: + check that the name exist and that its type is convertible\\ +*) + +(** The primitive refiner. *) + +val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map + +(** {6 Refiner errors. } *) + +type refiner_error = + + (*i Errors raised by the refiner i*) + | BadType of constr * constr * constr + | UnresolvedBindings of Name.t list + | CannotApply of constr * constr + | NotWellTyped of constr + | NonLinearProof of constr + | MetaInType of EConstr.constr + + (*i Errors raised by the tactics i*) + | IntroNeedsProduct + | DoesNotOccurIn of constr * Id.t + | NoSuchHyp of Id.t + +exception RefinerError of Environ.env * evar_map * refiner_error + +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 move_location -> + Environ.named_context_val -> Environ.named_context_val + +val insert_decl_in_named_context : Environ.env -> Evd.evar_map -> + 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 new file mode 100644 index 0000000000..ec17b8076f --- /dev/null +++ b/proofs/miscprint.ml @@ -0,0 +1,69 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Names +open Tactypes + +(** Printing of [intro_pattern] *) + +let rec pr_intro_pattern prc {CAst.v=pat} = match pat with + | IntroForthcoming true -> str "*" + | IntroForthcoming false -> str "**" + | IntroNaming p -> pr_intro_pattern_naming p + | IntroAction p -> pr_intro_pattern_action prc p + +and pr_intro_pattern_naming = let open Namegen in function + | IntroIdentifier id -> Id.print id + | IntroFresh id -> str "?" ++ Id.print id + | IntroAnonymous -> str "?" + +and pr_intro_pattern_action prc = function + | IntroWildcard -> str "_" + | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll + | IntroInjection pl -> + str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ + str "]" + | IntroApplyOn ({CAst.v=c},pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c + | IntroRewrite true -> str "->" + | IntroRewrite false -> str "<-" + +and pr_or_and_intro_pattern prc = function + | IntroAndPattern pl -> + str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" + | IntroOrPattern pll -> + str "[" ++ + hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) + ++ str "]" + +(** 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) + | {loc;v=(AnonHyp n, c)} -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) + +let pr_bindings prc prlc = function + | ImplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + pr_sequence prc l + | ExplicitBindings l -> + brk (1,1) ++ str "with" ++ brk (1,1) ++ + pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + +let pr_bindings_no_with prc prlc = function + | ImplicitBindings l -> + brk (0,1) ++ prlist_with_sep spc prc l + | ExplicitBindings l -> + brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l + | NoBindings -> mt () + +let pr_with_bindings prc prlc (c,bl) = + hov 1 (prc c ++ pr_bindings prc prlc bl) + diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli new file mode 100644 index 0000000000..f4e2e683d1 --- /dev/null +++ b/proofs/miscprint.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Tactypes + +(** Printing of [intro_pattern] *) + +val pr_intro_pattern : + ('a -> Pp.t) -> 'a intro_pattern_expr CAst.t -> Pp.t + +val pr_or_and_intro_pattern : + ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t + +val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t + +(** Printing of [move_location] *) + +val pr_bindings : + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a bindings -> Pp.t + +val pr_bindings_no_with : + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a bindings -> Pp.t + +val pr_with_bindings : + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a * 'a bindings -> Pp.t + diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml new file mode 100644 index 0000000000..7f1ae6d12b --- /dev/null +++ b/proofs/pfedit.ml @@ -0,0 +1,220 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Entries +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 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 (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 (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, + there is no accessible evar either *) + let env = Global.env () in + (Evd.from_env env, env) + +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 = (current_proof_by_default p) in + let evd = Proof.in_proof p (fun x -> x) in + (evd, Global.env ()) + +let current_proof_statement () = + match Proof_global.V82.get_current_initial_conclusions () with + | (id,([concl],strength)) -> id,strength,concl + | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") + +let solve ?with_end_tac gi info_lvl tac pr = + try + 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 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 + 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) + with + Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") + +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 Global.(env ())n com p) + + +(**********************************************************************) +(* Shortcut to build a term using tactics *) + +open Decl_kinds + +let next = let n = ref 0 in fun () -> incr n; !n + +let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac = + let evd = Evd.from_ctx ctx in + let terminator = Proof_global.make_terminator (fun _ -> ()) in + let goals = [ (Global.env_of_context sign , typ) ] in + Proof_global.start_proof evd id goal_kind goals terminator; + try + let status = by tac in + let open Proof_global in + let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in + match entries with + | [entry] -> + discard_current (); + let univs = UState.demote_seff_univs entry 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 + Proof_global.discard_current (); + iraise reraise + +let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = + let id = Id.of_string ("temporary_proof"^string_of_int (next())) in + let sign = val_of_named_context (named_context env) in + let gk = Global, poly, Proof Theorem in + let ce, status, univs = + build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in + let ce = + if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce + else { ce with + 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 ~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 ans = Safe_typing.inline_private_constants_in_constr env ans neff in + ans, sigma diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli new file mode 100644 index 0000000000..5699320af5 --- /dev/null +++ b/proofs/pfedit.mli @@ -0,0 +1,95 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 +open Decl_kinds + +(** {6 ... } *) +(** [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 : int -> Evd.evar_map * env + +(** [get_current_goal_context ()] works as [get_goal_context 1] *) + +val get_current_goal_context : unit -> 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 : ?p:Proof.t -> unit -> Evd.evar_map * env + +(** [current_proof_statement] *) + +val current_proof_statement : + unit -> Id.t * goal_kind * EConstr.types + +(** {6 ... } *) + +(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th + subgoal of the current focused proof or raises a [UserError] if no + proof is focused or if there is no [n]th subgoal. [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 or raises a UserError if there is no focused proof or + if there is no more subgoals. + Returns [false] if an unsafe tactic has been used. *) + +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 + existential variable *) + +val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit + +(** [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 : + Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> + EConstr.types -> unit Proofview.tactic -> + Safe_typing.private_constants Entries.definition_entry * bool * + UState.t + +val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> + 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 new file mode 100644 index 0000000000..1aeb24606b --- /dev/null +++ b/proofs/proof.ml @@ -0,0 +1,554 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(* Module defining the last essential tiles of interactive proofs. + A proof deals with the focusing commands (including the braces and bullets), + the shelf (see the [shelve] tactic) and given up goal (see the [give_up] + tactic). A proof is made of the following: + - Proofview: a proof is primarily the data of the current view. + That which is shown to the user (as a remainder, a proofview + is mainly the logical state of the proof, together with the + currently focused goals). + - 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 + "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 + the proof under focused must be complete) must be met. + - Shelf: A list of goals which have been put aside during the proof. They can be + retrieved with the [Unshelve] command, or solved by side effects + - Given up goals: as long as there is a given up goal, the proof is not completed. + Given up goals cannot be retrieved, the user must go back where the tactic + [give_up] was run and solve the goal there. +*) + +open Util + +type _focus_kind = int +type 'a focus_kind = _focus_kind +type focus_info = Obj.t +type reason = NotThisWay | AlreadyNoFocus +type unfocusable = + | Cannot of reason + | Loose + | Strict +type _focus_condition = + | CondNo of bool * _focus_kind + | CondDone of bool * _focus_kind + | CondEndStack of _focus_kind (* loose_end is false here *) +type 'a focus_condition = _focus_condition + +let next_kind = ref 0 +let new_focus_kind () = + let r = !next_kind in + incr next_kind; + r + +(* To be authorized to unfocus one must meet the condition prescribed by + the action which focused.*) +(* spiwack: we could consider having a list of authorized focus_kind instead + of just one, if anyone needs it *) + +exception CannotUnfocusThisWay + +(* Cannot focus on non-existing subgoals *) +exception NoSuchGoals of int * int + +exception NoSuchGoal of Names.Id.t + +exception FullyUnfocused + +let _ = CErrors.register_handler begin function + | CannotUnfocusThisWay -> + CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way") + | NoSuchGoals (i,j) when Int.equal i j -> + CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").") + | NoSuchGoals (i,j) -> + 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 + +let check_cond_kind c k = + let kind_of_cond = function + | CondNo (_,k) | CondDone(_,k) | CondEndStack k -> k in + Int.equal (kind_of_cond c) k + +let test_cond c k1 pw = + match c with + | CondNo(_, k) when Int.equal k k1 -> Strict + | CondNo(true, _) -> Loose + | CondNo(false, _) -> Cannot NotThisWay + | CondDone(_, k) when Int.equal k k1 && Proofview.finished pw -> Strict + | CondDone(true, _) -> Loose + | CondDone(false, _) -> Cannot NotThisWay + | CondEndStack k when Int.equal k k1 -> Strict + | CondEndStack _ -> Cannot AlreadyNoFocus + +let no_cond ?(loose_end=false) k = CondNo (loose_end, k) +let done_cond ?(loose_end=false) k = CondDone (loose_end,k) + +(* Subpart of the type of proofs. It contains the parts of the proof which + are under control of the undo mechanism *) +type t = + { proofview: Proofview.proofview + (** Current focused proofview *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; focus_stack: (_focus_condition*focus_info*Proofview.focus_context) list + (** History of the focusings, provides information on how to unfocus + the proof and the extra information stored while focusing. The + list is empty when the proof is fully unfocused. *) + ; shelf : Goal.goal list + (** List of goals that have been shelved. *) + ; given_up : Goal.goal list + (** List of goals that have been given up *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** the name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let initial_goals pf = Proofview.initial_goals pf.entry +let initial_euctx pf = pf.initial_euctx + +(*** General proof functions ***) + +let proof p = + let (goals,sigma) = Proofview.proofview p.proofview in + (* spiwack: beware, the bottom of the stack is used by [Proof] + internally, and should not be exposed. *) + let rec map_minus_one f = function + | [] -> assert false + | [_] -> [] + | a::l -> f a :: (map_minus_one f l) + in + let stack = + map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack + in + let shelf = p.shelf in + let given_up = p.given_up in + (goals,stack,shelf,given_up,sigma) + +type 'a pre_goals = { + fg_goals : 'a list; + (** List of the focussed goals *) + bg_goals : ('a list * 'a list) list; + (** Zipper representing the unfocussed background goals *) + shelved_goals : 'a list; + (** List of the goals on the shelf. *) + given_up_goals : 'a list; + (** List of the goals that have been given up *) +} + +let map_structured_proof pfts process_goal: 'a pre_goals = + let (goals, zipper, shelf, given_up, sigma) = proof pfts in + let fg = List.map (process_goal sigma) goals in + let map_zip (lg, rg) = + let lg = List.map (process_goal sigma) lg in + let rg = List.map (process_goal sigma) rg in + (lg, rg) + in + let bg = List.map map_zip zipper in + let shelf = List.map (process_goal sigma) shelf in + let given_up = List.map (process_goal sigma) given_up in + { fg_goals = fg; + bg_goals = bg; + shelved_goals = shelf; + given_up_goals = given_up; } + +let rec unroll_focus pv = function + | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk + | [] -> pv + +(* spiwack: a proof is considered completed even if its still focused, if the focus + doesn't hide any goal. + Unfocusing is handled in {!return}. *) +let is_done p = + Proofview.finished p.proofview && + Proofview.finished (unroll_focus p.proofview p.focus_stack) + +(* spiwack: for compatibility with <= 8.2 proof engine *) +let has_unresolved_evar p = + Proofview.V82.has_unresolved_evar p.proofview +let has_shelved_goals p = not (CList.is_empty (p.shelf)) +let has_given_up_goals p = not (CList.is_empty (p.given_up)) + +let is_complete p = + is_done p && not (has_unresolved_evar p) && + not (has_shelved_goals p) && not (has_given_up_goals p) + +(* Returns the list of partial proofs to initial goals *) +let partial_proof p = Proofview.partial_proof p.entry p.proofview + +(*** The following functions implement the basic internal mechanisms + of proofs, they are not meant to be exported in the .mli ***) + +(* An auxiliary function to push a {!focus_context} on the focus stack. *) +let push_focus cond inf context pr = + { pr with focus_stack = (cond,inf,context)::pr.focus_stack } + +(* An auxiliary function to read the kind of the next focusing step *) +let cond_of_focus pr = + match pr.focus_stack with + | (cond,_,_)::_ -> cond + | _ -> raise FullyUnfocused + +(* 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 + | focus::other_focuses -> + { pr with focus_stack = other_focuses }, focus + | _ -> + raise FullyUnfocused + +(* This function focuses the proof [pr] between indices [i] and [j] *) +let _focus cond inf i j pr = + let focused, context = Proofview.focus i j pr.proofview in + let pr = push_focus cond inf context pr in + { pr with proofview = focused } + +(* This function unfocuses the proof [pr], it raises [FullyUnfocused], + if the proof is already fully unfocused. + This function does not care about the condition of the current focus. *) +let _unfocus pr = + let pr, (_,_,fc) = pop_focus pr in + { 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 + a need for it? *) +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 + | Cannot NotThisWay -> raise CannotUnfocusThisWay + | Cannot AlreadyNoFocus -> raise FullyUnfocused + | Strict -> + let pr = _unfocus pr in + pr + | Loose -> + begin try + let pr = _unfocus pr in + unfocus kind pr () + with FullyUnfocused -> raise CannotUnfocusThisWay + end + +exception NoSuchFocus +(* no handler: should not be allowed to reach toplevel. *) +let rec get_in_focus_stack kind stack = + match stack with + | (cond,inf,_)::stack -> + if check_cond_kind cond kind then inf + else get_in_focus_stack kind stack + | [] -> raise NoSuchFocus +let get_at_focus kind pr = + Obj.magic (get_in_focus_stack kind pr.focus_stack) + +let is_last_focus kind pr = + let (cond,_,_) = List.hd pr.focus_stack in + check_cond_kind cond kind + +let no_focused_goal p = + Proofview.finished p.proofview + +let rec maximal_unfocus k p = + if no_focused_goal p then + try maximal_unfocus k (unfocus k p ()) + with FullyUnfocused | CannotUnfocusThisWay -> p + else p + +(*** Proof Creation/Termination ***) + +(* [end_of_stack] is unfocused by return to close every loose focus. *) +let end_of_stack_kind = new_focus_kind () +let end_of_stack = CondEndStack end_of_stack_kind + +let unfocused = is_last_focus end_of_stack_kind + +let start ~name ~poly sigma goals = + let entry, proofview = Proofview.init sigma goals in + let pr = { + proofview; + entry; + focus_stack = [] ; + shelf = [] ; + given_up = []; + initial_euctx = + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in + _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr + +let dependent_start ~name ~poly goals = + let entry, proofview = Proofview.dependent_init goals in + let pr = { + proofview; + entry; + focus_stack = [] ; + shelf = [] ; + given_up = []; + initial_euctx = + Evd.evar_universe_context (snd (Proofview.proofview proofview)) + ; name + ; poly + } in + let number_of_goals = List.length (Proofview.initial_goals pr.entry) in + _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr + +type open_error_reason = + | UnfinishedProof + | HasShelvedGoals + | HasGivenUpGoals + | HasUnresolvedEvar + +let print_open_error_reason er = let open Pp in match er with + | UnfinishedProof -> + str "Attempt to save an incomplete proof" + | HasShelvedGoals -> + str "Attempt to save a proof with shelved goals" + | HasGivenUpGoals -> + strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed." + | HasUnresolvedEvar -> + strbrk "Attempt to save a proof with existential variables still non-instantiated" + +exception OpenProof of Names.Id.t option * open_error_reason + +let _ = CErrors.register_handler begin function + | OpenProof (pid, reason) -> + let open Pp in + Option.cata (fun pid -> + str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason + | _ -> raise CErrors.Unhandled + end + +let return ?pid (p : t) = + if not (is_done p) then + raise (OpenProof(pid, UnfinishedProof)) + else if has_shelved_goals p then + raise (OpenProof(pid, HasShelvedGoals)) + else if has_given_up_goals p then + raise (OpenProof(pid, HasGivenUpGoals)) + else if has_unresolved_evar p then + (* spiwack: for compatibility with <= 8.3 proof engine *) + raise (OpenProof(pid, HasUnresolvedEvar)) + else + let p = unfocus end_of_stack_kind p () in + Proofview.return p.proofview + +let compact p = + let entry, proofview = Proofview.compact p.entry p.proofview in + { p with proofview; entry } + +(*** Function manipulation proof extra informations ***) + +(*** Tactics ***) + +let run_tactic env tac pr = + let open Proofview.Notations in + let sp = pr.proofview in + let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in + let tac = + tac >>= fun () -> + Proofview.tclEVARMAP >>= fun sigma -> + (* Already solved goals are not to be counted as shelved. Nor are + they to be marked as unresolvable. *) + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in + (* Check that retrieved given up is empty *) + if not (List.is_empty retrieved_given_up) then + CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); + let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT retrieved + in + let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = + Proofview.apply env tac sp + in + let sigma = Proofview.return proofview in + let to_shelve = undef sigma to_shelve in + let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in + let proofview = + List.fold_left + Proofview.Unsafe.mark_as_unresolvable + proofview + to_shelve + in + let given_up = pr.given_up@give_up in + let proofview = Proofview.Unsafe.reset_future_goals proofview in + { pr with proofview ; shelf ; given_up },(status,info_trace) + +(*** Commands ***) + +let in_proof p k = k (Proofview.return p.proofview) + +(* Remove all the goals from the shelf and adds them at the end of the + focused goals. *) +let unshelve p = + { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } + +let pr_proof p = + let p = map_structured_proof p (fun _sigma g -> g) in + Pp.( + let pr_goal_list = prlist_with_sep spc Goal.pr_goal in + let rec aux acc = function + | [] -> acc + | (before,after)::stack -> + aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ + pr_goal_list after) stack in + str "[" ++ str "focus structure: " ++ + aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++ + str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++ + str "given up: " ++ pr_goal_list p.given_up_goals ++ + str "]" + ) + +(*** Compatibility layer with <=v8.2 ***) +module V82 = struct + + let background_subgoals p = + let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in + Evd.{ it; sigma } + + let top_goal p = + let { Evd.it=gls ; sigma=sigma; } = + Proofview.V82.top_goals p.entry p.proofview + in + { Evd.it=List.hd gls ; sigma=sigma; } + + let top_evars p = + Proofview.V82.top_evars p.entry + + let grab_evars p = + if not (is_done p) then + raise (OpenProof(None, UnfinishedProof)) + else + { p with proofview = Proofview.V82.grab p.proofview } + + (* Main component of vernac command Existential *) + let instantiate_evar env n com pr = + let tac = + Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> + let (evk, evi) = + let evl = Evarutil.non_instantiated sigma in + let evl = Evar.Map.bindings evl in + if (n <= 0) then + CErrors.user_err Pp.(str "incorrect existential variable index") + else if CList.length evl < n then + CErrors.user_err Pp.(str "not so many uninstantiated existential variables") + else + CList.nth evl (n-1) + in + let env = Evd.evar_filtered_env evi in + let rawc = Constrintern.intern_constr env sigma com in + let ltac_vars = Glob_ops.empty_lvar in + let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in + Proofview.Unsafe.tclEVARS sigma + end in + let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in + let shelf = + List.filter begin fun g -> + Evd.is_undefined (Proofview.return proofview) g + end pr.shelf + in + { 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 + let set = add given_up set in + let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in + add bgoals set + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool + (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) + } + +let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } = + let goals, sigma = Proofview.proofview proofview in + (* spiwack: beware, the bottom of the stack is used by [Proof] + internally, and should not be exposed. *) + let rec map_minus_one f = function + | [] -> assert false + | [_] -> [] + | a::l -> f a :: (map_minus_one f l) + in + let stack = + map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in + { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } diff --git a/proofs/proof.mli b/proofs/proof.mli new file mode 100644 index 0000000000..fd5e905a3b --- /dev/null +++ b/proofs/proof.mli @@ -0,0 +1,260 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(* Module defining the last essential tiles of interactive proofs. + A proof deals with the focusing commands (including the braces and bullets), + the shelf (see the [shelve] tactic) and given up goal (see the [give_up] + tactic). A proof is made of the following: + - Proofview: a proof is primarily the data of the current view. + That which is shown to the user (as a remainder, a proofview + is mainly the logical state of the proof, together with the + currently focused goals). + - 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 + "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 + the proof under focused must be complete) must be met. + - Shelf: A list of goals which have been put aside during the proof. They can be + retrieved with the [Unshelve] command, or solved by side effects + - Given up goals: as long as there is a given up goal, the proof is not completed. + Given up goals cannot be retrieved, the user must go back where the tactic + [give_up] was run and solve the goal there. +*) + +(* Type of a proof. *) +type t + +(* Returns a stylised view of a proof for use by, for instance, + ide-s. *) +(* spiwack: the type of [proof] will change as we push more refined + functions to ide-s. This would be better than spawning a new nearly + identical function everytime. Hence the generic name. *) +(* In this version: returns the focused goals, a representation of the + focus stack (the goals at each level), a representation of the + shelf (the list of goals on the shelf), a representation of the + given up goals (the list of the given up goals) and the underlying + evar_map *) +val proof : t -> + Goal.goal list + * (Goal.goal list * Goal.goal list) list + * Goal.goal list + * Goal.goal list + * Evd.evar_map +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_goals : t -> (EConstr.constr * EConstr.types) list +[@@ocaml.deprecated "use [Proof.data]"] + +val initial_euctx : t -> UState.t +[@@ocaml.deprecated "use [Proof.data]"] + +type data = + { sigma : Evd.evar_map + (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) + ; goals : Evar.t list + (** Focused goals *) + ; entry : Proofview.entry + (** Entry for the proofview *) + ; stack : (Evar.t list * Evar.t list) list + (** A representation of the focus stack *) + ; shelf : Evar.t list + (** A representation of the shelf *) + ; given_up : Evar.t list + (** A representation of the given up goals *) + ; initial_euctx : UState.t + (** The initial universe context (for the statement) *) + ; name : Names.Id.t + (** The name of the theorem whose proof is being constructed *) + ; poly : bool; + (** polymorphism *) + } + +val data : t -> data + +(* Generic records structured like the return type of proof *) +type 'a pre_goals = { + fg_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] + (** List of the focussed goals *) + bg_goals : ('a list * 'a list) list; + [@ocaml.deprecated "use [Proof.data]"] + (** Zipper representing the unfocussed background goals *) + shelved_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] + (** List of the goals on the shelf. *) + given_up_goals : 'a list; + [@ocaml.deprecated "use [Proof.data]"] + (** List of the goals that have been given up *) +} +[@@ocaml.deprecated "use [Proof.data]"] + +(* needed in OCaml 4.05.0, not needed in newer ones *) +[@@@ocaml.warning "-3"] +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"] +[@@ocaml.deprecated "use [Proof.data]"] +[@@@ocaml.warning "+3"] + +(*** General proof functions ***) +val start + : name:Names.Id.t + -> poly:bool + -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t + +val dependent_start + : name:Names.Id.t + -> poly:bool + -> Proofview.telescope -> t + +(* Returns [true] if the considered proof is completed, that is if no goal remain + to be considered (this does not require that all evars have been solved). *) +val is_done : t -> bool + +(* Like is_done, but this time it really means done (i.e. nothing left to do) *) +val is_complete : t -> bool + +(* Returns the list of partial proofs to initial goals. *) +val partial_proof : t -> EConstr.constr list + +val compact : t -> t + +(* Returns the proofs (with their type) of the initial goals. + Raises [UnfinishedProof] is some goals remain to be considered. + Raises [HasShelvedGoals] if some goals are left on the shelf. + Raises [HasGivenUpGoals] if some goals have been given up. + Raises [HasUnresolvedEvar] if some evars have been left undefined. *) +type open_error_reason = + | UnfinishedProof + | HasShelvedGoals + | HasGivenUpGoals + | HasUnresolvedEvar + +exception OpenProof of Names.Id.t option * open_error_reason + +val return : ?pid:Names.Id.t -> t -> Evd.evar_map + +(*** Focusing actions ***) + +(* ['a focus_kind] is the type used by focusing and unfocusing + commands to synchronise. Focusing and unfocusing commands use + a particular ['a focus_kind], and if they don't match, the unfocusing command + will fail. + When focusing with an ['a focus_kind], an information of type ['a] is + stored at the focusing point. An example use is the "induction" tactic + of the declarative mode where sub-tactics must be aware of the current + induction argument. *) +type 'a focus_kind +val new_focus_kind : unit -> 'a focus_kind + +(* To be authorized to unfocus one must meet the condition prescribed by + the action which focused. + Conditions always carry a focus kind, and inherit their type parameter + from it.*) +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] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{- solve_goal. }] because they use a loose-end condition. *) +val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition +(* [done_cond] checks that the unfocusing command uses the right [focus_kind] + and that the focused proofview is complete. + If [loose_end] (default [false]) is [true], then if the [focus_kind] + doesn't match, then unfocusing can occur, provided it unfocuses + an earlier focus. + For instance bullets can be unfocused in the following situation + [{ - solve_goal. }] because they use a loose-end 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 + 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 + +(* This is raised when trying to focus on non-existing subgoals. It is + handled by an error message but one may need to catch it and + settle a better error message in some case (suggesting a better + bullet for example), see proof_global.ml function Bullet.pop and + Bullet.push. *) +exception NoSuchGoals of int * int + +(* Unfocusing command. + Raises [FullyUnfocused] if the proof is not focused. + Raises [CannotUnfocusThisWay] if the proof the unfocusing condition + is not met. *) +val unfocus : 'a focus_kind -> t -> unit -> t + +(* [unfocused p] returns [true] when [p] is fully unfocused. *) +val unfocused : t -> bool + +(* [get_at_focus k] gets the information stored at the closest focus point + of kind [k]. + Raises [NoSuchFocus] if there is no focus point of kind [k]. *) +exception NoSuchFocus +val get_at_focus : 'a focus_kind -> t -> 'a + +(* [is_last_focus k] check if the most recent focus is of kind [k] *) +val is_last_focus : 'a focus_kind -> t -> bool + +(* returns [true] if there is no goal under focus. *) +val no_focused_goal : t -> bool + +(*** Tactics ***) + +(* the returned boolean signal whether an unsafe tactic has been + used. In which case it is [false]. *) +val run_tactic + : Environ.env + -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) + +val maximal_unfocus : 'a focus_kind -> t -> t + +(*** Commands ***) + +val in_proof : t -> (Evd.evar_map -> 'a) -> 'a + +(* Remove all the goals from the shelf and adds them at the end of the + focused goals. *) +val unshelve : t -> t + +val pr_proof : t -> Pp.t + +(*** Compatibility layer with <=v8.2 ***) +module V82 : sig + + (* All the subgoals of the proof, including those which are not focused. *) + val background_subgoals : t -> Goal.goal list Evd.sigma + + val top_goal : t -> Goal.goal Evd.sigma + + (* returns the existential variable used to start the proof *) + val top_evars : t -> Evar.t list + + (* Turns the unresolved evars into goals. + Raises [UnfinishedProof] if there are still unsolved goals. *) + val grab_evars : t -> t + + (* Implements the Existential command *) + val instantiate_evar : + Environ.env -> 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 new file mode 100644 index 0000000000..2ca4f0afb4 --- /dev/null +++ b/proofs/proof_bullet.ml @@ -0,0 +1,199 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Proof + +type t = + | Dash of int + | Star of int + | Plus of int + +let bullet_eq b1 b2 = match b1, b2 with +| 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 + | Dash n -> Pp.(str (String.make n '-')) + | Star n -> Pp.(str (String.make n '*')) + | Plus n -> Pp.(str (String.make n '+')) + + +type behavior = { + name : string; + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t +} + +let behaviors = Hashtbl.create 4 +let register_behavior b = Hashtbl.add behaviors b.name b + +(*** initial modes ***) +let none = { + name = "None"; + put = (fun x _ -> x); + suggest = (fun _ -> Pp.mt ()) +} +let _ = register_behavior none + +module Strict = struct + type suggestion = + | 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. *) + | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *) + | ProofFinished (* No more goal anywhere *) + + (* give a message only if more informative than the standard coq message *) + let suggest_on_solved_goal sugg = + match sugg with + | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".") + | NoBulletInUse -> Pp.mt () + | ProofFinished -> Pp.mt () + | Suggest b -> Pp.(str"Focus next goal with bullet " ++ pr_bullet b ++ str".") + | Unfinished b -> Pp.(str"The current bullet " ++ pr_bullet b ++ str" is unfinished.") + + (* give always a message. *) + let suggest_on_error sugg = + match sugg with + | NeedClosingBrace -> Pp.(str"Try unfocusing with \"}\".") + | NoBulletInUse -> assert false (* This should never raise an error. *) + | ProofFinished -> Pp.(str"No more subgoals.") + | Suggest b -> Pp.(str"Expecting " ++ pr_bullet b ++ str".") + | Unfinished b -> Pp.(str"Current bullet " ++ pr_bullet b ++ str" is not finished.") + + exception FailedBullet of t * suggestion + + let _ = + CErrors.register_handler + (function + | FailedBullet (b,sugg) -> + let prefix = Pp.(str"Wrong bullet " ++ pr_bullet b ++ str": ") in + CErrors.user_err ~hdr:"Focus" Pp.(prefix ++ suggest_on_error sugg) + | _ -> raise CErrors.Unhandled) + + + (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) + let bullet_kind = (new_focus_kind () : t list focus_kind) + let bullet_cond = done_cond ~loose_end:true bullet_kind + + (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command + experience will tell if this is the right discipline of if we want to be finer and + reset them only for a choice of bullets. *) + let get_bullets pr = + if is_last_focus bullet_kind pr then + get_at_focus bullet_kind pr + else + [] + + let has_bullet bul pr = + let rec has_bullet = function + | b'::_ when bullet_eq bul b' -> true + | _::l -> has_bullet l + | [] -> false + in + has_bullet (get_bullets pr) + + (* pop a bullet from proof [pr]. There should be at least one + bullet in use. If pop impossible (pending proofs on this level + of bullet or higher) then raise [Proof.CannotUnfocusThisWay]. *) + let pop pr = + match get_bullets pr with + | b::_ -> unfocus bullet_kind pr () , b + | _ -> assert false + + let push (b:t) pr = + focus bullet_cond (b::get_bullets pr) 1 pr + + let suggest_bullet (prf : Proof.t): suggestion = + if is_done prf then ProofFinished + else if not (no_focused_goal prf) + then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) + match get_bullets prf with + | b::_ -> Unfinished b + | _ -> NoBulletInUse + else (* There is no goal under focus but some are unfocussed, + let us look at the bullet needed. *) + let rec loop prf = + match pop prf with + | prf, b -> + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + begin + try ignore (push b prf); Suggest b + with _ -> + (* b could not be pushed, so we must look for a outer bullet *) + loop prf + end + | exception _ -> + (* No pop was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + NeedClosingBrace + in + loop prf + + let rec pop_until (prf : Proof.t) bul : Proof.t = + let prf', b = pop prf in + if bullet_eq bul b then prf' + else pop_until prf' bul + + let put p bul = + try + if not (has_bullet bul p) then + (* bullet is not in use, so pushing it is always ok unless + no goal under focus. *) + push bul p + else + match suggest_bullet p with + | Suggest suggested_bullet when bullet_eq bul suggested_bullet + -> (* suggested_bullet is mandatory and you gave the right one *) + let p' = pop_until p bul in + push bul p' + (* the bullet you gave is in use but not the right one *) + | sugg -> raise (FailedBullet (bul,sugg)) + with NoSuchGoals _ -> (* push went bad *) + raise (FailedBullet (bul,suggest_bullet p)) + + let strict = { + name = "Strict Subproofs"; + put = put; + suggest = (fun prf -> suggest_on_solved_goal (suggest_bullet prf)) + + } + let _ = register_behavior strict +end + +(* Current bullet behavior, controlled by the option *) +let current_behavior = ref Strict.strict + +let () = + Goptions.(declare_string_option { + optdepr = false; + optname = "bullet behavior"; + optkey = ["Bullet";"Behavior"]; + optread = begin fun () -> + (!current_behavior).name + end; + optwrite = begin fun n -> + current_behavior := + try Hashtbl.find behaviors n + with Not_found -> + CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\".")) + end + }) + +let put p b = + (!current_behavior).put p b + +let suggest p = + (!current_behavior).suggest p diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli new file mode 100644 index 0000000000..0fcc647a6f --- /dev/null +++ b/proofs/proof_bullet.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(**********************************************************) +(* *) +(* Bullets *) +(* *) +(**********************************************************) + +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 + suggesting the right bullet to use on a given proof, together + with a name to identify the behavior. *) +type behavior = { + name : string; + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t +} + +(** A registered behavior can then be accessed in Coq + through the command [Set Bullet Behavior "name"]. + + Two modes are registered originally: + * "Strict Subproofs": + - If this bullet follows another one of its kind, defocuses then focuses + (which fails if the focused subproof is not complete). + - If it is the first bullet of its kind, then focuses a new subproof. + * "None": bullets don't do anything *) +val register_behavior : behavior -> unit + +(** Handles focusing/defocusing with bullets: + *) +val put : Proof.t -> t -> Proof.t +val suggest : Proof.t -> Pp.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml new file mode 100644 index 0000000000..f8adc58921 --- /dev/null +++ b/proofs/proof_global.ml @@ -0,0 +1,498 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Pp +open Names + +module NamedDecl = Context.Named.Declaration + +(*** Proof Modes ***) + +(* Type of proof modes : + - A function [set] to set it *from standard mode* + - A function [reset] to reset the *standard mode* from it *) +type proof_mode_name = string +type proof_mode = { + name : proof_mode_name ; + set : unit -> unit ; + reset : unit -> unit +} + +let proof_modes = Hashtbl.create 6 +let find_proof_mode n = + try Hashtbl.find proof_modes n + with Not_found -> + CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) + +let register_proof_mode ({name = n} as m) = + Hashtbl.add proof_modes n (CEphemeron.create m) + +(* initial mode: standard mode *) +let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } +let _ = register_proof_mode standard + +(* Default proof mode, to be set at the beginning of proofs. *) +let default_proof_mode = ref (find_proof_mode "No") + +let get_default_proof_mode_name () = + (CEphemeron.default !default_proof_mode standard).name + +let proof_mode_opt_name = ["Default";"Proof";"Mode"] +let () = + Goptions.(declare_string_option { + optdepr = false; + optname = "default proof mode" ; + optkey = proof_mode_opt_name ; + optread = begin fun () -> + (CEphemeron.default !default_proof_mode standard).name + end; + optwrite = begin fun n -> + default_proof_mode := find_proof_mode n + end + }) + +(*** Proof Global Environment ***) + +(* Extra info on proofs. *) +type lemma_possible_guards = int list list + +type proof_object = { + id : Names.Id.t; + entries : Safe_typing.private_constants Entries.definition_entry list; + persistence : Decl_kinds.goal_kind; + 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 opacity_flag * + lident option * + proof_object + +type proof_terminator = proof_ending -> unit +type closed_proof = proof_object * proof_terminator + +type pstate = { + terminator : proof_terminator CEphemeron.key; + endline_tactic : Genarg.glob_generic_argument option; + section_vars : Constr.named_context option; + proof : Proof.t; + mode : proof_mode CEphemeron.key; + universe_decl: UState.universe_decl; + strength : Decl_kinds.goal_kind; +} + +type t = pstate list + +let make_terminator f = f +let apply_terminator f = f + +(* The head of [!pstates] is the actual current proof, the other ones are + to be resumed when the current proof is closed or aborted. *) +let pstates = ref ([] : pstate list) + +(* Current proof_mode, for bookkeeping *) +let current_proof_mode = ref !default_proof_mode + +(* combinators for proof modes *) +let update_proof_mode () = + match !pstates with + | { mode = m } :: _ -> + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + current_proof_mode := m; + CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) + | _ -> + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + current_proof_mode := find_proof_mode "No" + +(* combinators for the current_proof lists *) +let push a l = l := a::!l; + update_proof_mode () + +exception NoSuchProof +let () = CErrors.register_handler begin function + | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.") + | _ -> raise CErrors.Unhandled +end + +exception NoCurrentProof +let () = CErrors.register_handler begin function + | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") + | _ -> raise CErrors.Unhandled +end + +(*** Proof Global manipulation ***) + +let get_all_proof_names () = + List.map Proof.(function pf -> (data pf.proof).name) !pstates + +let cur_pstate () = + match !pstates with + | np::_ -> np + | [] -> raise NoCurrentProof + +let give_me_the_proof () = (cur_pstate ()).proof +let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None +let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name + +let with_current_proof f = + match !pstates with + | [] -> raise NoCurrentProof + | p :: rest -> + let et = + match p.endline_tactic with + | None -> Proofview.tclUNIT () + | Some tac -> + let open Geninterp in + let ist = { lfun = Id.Map.empty; 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 p.proof in + let p = { p with proof = newpr } in + pstates := p :: rest; + ret + +let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ()) + +let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact) + +(* Sets the tactic to be used when a tactic line is closed with [...] *) +let set_endline_tactic tac = + match !pstates with + | [] -> raise NoCurrentProof + | p :: rest -> pstates := { p with endline_tactic = Some tac } :: rest + +(* spiwack: it might be considered to move error messages away. + Or else to remove special exceptions from Proof_global. + Arguments for the former: there is no reason Proof_global is only + accessed directly through vernacular commands. Error message should be + pushed to external layers, and so we should be able to have a finer + control on error message on complex actions. *) +let msg_proofs () = + match get_all_proof_names () with + | [] -> (spc () ++ str"(No proof-editing in progress).") + | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ + (pr_sequence Id.print l) ++ str".") + +let there_is_a_proof () = not (List.is_empty !pstates) +let there_are_pending_proofs () = there_is_a_proof () +let check_no_pending_proof () = + if not (there_are_pending_proofs ()) then + () + else begin + CErrors.user_err + (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ + str"Use \"Abort All\" first or complete proof(s).") + end + +let pf_name_eq id ps = + let Proof.{ name } = Proof.data ps.proof in + Id.equal name id + +let discard_gen id = + pstates := List.filter (fun pf -> not (pf_name_eq id pf)) !pstates + +let discard {CAst.loc;v=id} = + let n = List.length !pstates in + discard_gen id; + if Int.equal (List.length !pstates) n then + CErrors.user_err ?loc + ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ()) + +let discard_current () = + if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates + +let discard_all () = pstates := [] + +(* [set_proof_mode] sets the proof mode to be used after it's called. It is + typically called by the Proof Mode command. *) +let set_proof_mode m id = + pstates := List.map + (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) + !pstates; + update_proof_mode () + +let set_proof_mode mn = + set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) + +let activate_proof_mode mode = + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) +let disactivate_current_proof_mode () = + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) + +(** [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 + is (spiwack: for potential printing, I believe is used only by + closing commands and the xml plugin); [terminator] is used at the + 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 name ?(pl=UState.default_univ_decl) kind goals terminator = + let initial_state = { + terminator = CEphemeron.create terminator; + proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; + endline_tactic = None; + section_vars = None; + mode = find_proof_mode "No"; + universe_decl = pl; + strength = kind } in + push initial_state pstates + +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = + let initial_state = { + terminator = CEphemeron.create terminator; + proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; + endline_tactic = None; + section_vars = None; + mode = find_proof_mode "No"; + universe_decl = pl; + strength = kind } in + push initial_state pstates + +let get_used_variables () = (cur_pstate ()).section_vars +let get_universe_decl () = (cur_pstate ()).universe_decl + +let set_used_variables 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 (x,_) -> + if Id.Set.mem x all_safe then orig + else (ctx, all_safe) + | LocalDef (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 + match !pstates with + | [] -> raise NoCurrentProof + | p :: rest -> + if not (Option.is_empty p.section_vars) then + CErrors.user_err Pp.(str "Used section variables can be declared only once"); + pstates := { p with section_vars = Some ctx} :: rest; + ctx, [] + +let get_open_goals () = + let Proof.{ goals; stack; shelf } = Proof.data (cur_pstate ()).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 * Safe_typing.private_constants) 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) = + let { section_vars; proof; terminator; universe_decl; strength } = cur_pstate () in + let Proof.{ name; poly; entry; initial_euctx } = 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 = + 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 + 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)) + 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.const_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 universe_decl 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 universe_decl 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 universe_decl 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 = Entries.Monomorphic_const_entry (UState.context_set 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 universe_decl 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 + {Entries. + const_entry_body = body; + const_entry_secctx = section_vars; + const_entry_feedback = feedback_id; + const_entry_type = Some typ; + const_entry_inline_code = false; + const_entry_opaque = opaque; + const_entry_universes = univs; } + in + let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in + { id = name; entries = entries; persistence = strength; + universes }, + fun pr_ending -> CEphemeron.get terminator pr_ending + +let return_proof ?(allow_partial=false) () = + let { proof } = cur_pstate () 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 + (* 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.to_constr evd c, eff)) initial_goals in + proofs, Evd.evar_universe_context evd + +let close_future_proof ~opaque ~feedback_id proof = + close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof +let close_proof ~opaque ~keep_body_ucst_separate fix_exn = + close_proof ~opaque ~keep_body_ucst_separate ~now:true + (Future.from_val ~fix_exn (return_proof ())) + +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator +let set_terminator hook = + match !pstates with + | [] -> raise NoCurrentProof + | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps + +module V82 = struct + let get_current_initial_conclusions () = + let { proof; strength } = cur_pstate () in + let Proof.{ name; entry } = Proof.data proof in + let initial = Proofview.initial_goals entry in + let goals = List.map (fun (o, c) -> c) initial in + name, (goals, strength) +end + +let freeze ~marshallable = + if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") + else !pstates +let unfreeze s = pstates := s; update_proof_mode () +let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof +let copy_terminators ~src ~tgt = + assert(List.length src = List.length tgt); + List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt + +let update_global_env pf_info = + with_current_proof (fun _ p -> + Proof.in_proof p (fun sigma -> + 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, ()))) + +(* XXX: Bullet hook, should be really moved elsewhere *) +let () = + let hook n = + try + let prf = give_me_the_proof () in + (Proof_bullet.suggest prf) + with NoCurrentProof -> mt () + in + Proofview.set_nosuchgoals_hook hook + diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli new file mode 100644 index 0000000000..e762f3b7dc --- /dev/null +++ b/proofs/proof_global.mli @@ -0,0 +1,185 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 + +val there_are_pending_proofs : unit -> bool +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 : Names.lident -> unit +val discard_current : unit -> unit +val discard_all : unit -> unit + +val give_me_the_proof_opt : unit -> Proof.t option +exception NoCurrentProof +val give_me_the_proof : unit -> Proof.t +(** @raise NoCurrentProof when outside proof mode. *) + +val compact_the_proof : unit -> unit + +(** 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 lemma_possible_guards = int list list + +type proof_object = { + id : Names.Id.t; + entries : Safe_typing.private_constants Entries.definition_entry list; + persistence : Decl_kinds.goal_kind; + 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 opacity_flag * + Names.lident option * + proof_object +type proof_terminator +type closed_proof = proof_object * proof_terminator + +val make_terminator : (proof_ending -> unit) -> proof_terminator +val apply_terminator : proof_terminator -> proof_ending -> unit + +(** [start_proof id str pl 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 + is; [terminator] is used at the end of the proof to close the proof + (e.g. to declare the built constructions as a coercion or a setoid + morphism). The proof is started in the evar map [sigma] (which can + typically contain universe constraints), and with universe bindings + pl. *) +val start_proof : + 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:UState.universe_decl -> Decl_kinds.goal_kind -> + Proofview.telescope -> proof_terminator -> unit + +(** 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 : unit -> unit + +(* 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 -> closed_proof + +(* 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 * Safe_typing.private_constants) 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 -> unit -> closed_proof_output +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> + closed_proof_output Future.computation -> closed_proof + +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +val get_terminator : unit -> proof_terminator +val set_terminator : proof_terminator -> unit + +exception NoSuchProof + +val get_open_goals : unit -> int + +(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is + no current proof. + The return boolean is set to [false] if an unsafe tactic has been used. *) +val with_current_proof : + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a +val simple_with_current_proof : + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit + +(** Sets the tactic to be used when a tactic line is closed with [...] *) +val set_endline_tactic : Genarg.glob_generic_argument -> unit + +(** 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 : + 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 -> UState.universe_decl + +module V82 : sig + val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * + Decl_kinds.goal_kind) +end + +val freeze : marshallable:bool -> t +val unfreeze : t -> unit +val proof_of_state : t -> Proof.t +val copy_terminators : src:t -> tgt:t -> t + + +(**********************************************************) +(* Proof Mode API *) +(* The current Proof Mode API is deprecated and a new one *) +(* will be (hopefully) defined in 8.8 *) +(**********************************************************) + +(** Type of proof modes : + - A name + - A function [set] to set it *from standard mode* + - A function [reset] to reset the *standard mode* from it + +*) +type proof_mode_name = string +type proof_mode = { + name : proof_mode_name ; + set : unit -> unit ; + reset : unit -> unit +} + +(** Registers a new proof mode which can then be adressed by name + in [set_default_proof_mode]. + One mode is already registered - the standard mode - named "No", + It corresponds to Coq default setting are they are set when coqtop starts. *) +val register_proof_mode : proof_mode -> unit +(* Can't make this deprecated due to limitations of camlp5 *) +(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *) + +val proof_mode_opt_name : string list + +val get_default_proof_mode_name : unit -> proof_mode_name +[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] + +(** [set_proof_mode] sets the proof mode to be used after it's called. It is + typically called by the Proof Mode command. *) +val set_proof_mode : proof_mode_name -> unit +[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] + +val activate_proof_mode : proof_mode_name -> unit +[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] + +val disactivate_current_proof_mode : unit -> unit +[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib new file mode 100644 index 0000000000..0ce726db25 --- /dev/null +++ b/proofs/proofs.mllib @@ -0,0 +1,14 @@ +Miscprint +Goal +Evar_refiner +Refine +Proof +Logic +Goal_select +Proof_bullet +Proof_global +Refiner +Tacmach +Pfedit +Clenv +Clenvtac diff --git a/proofs/refine.ml b/proofs/refine.ml new file mode 100644 index 0000000000..1d796fece5 --- /dev/null +++ b/proofs/refine.ml @@ -0,0 +1,169 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Util +open Proofview.Notations +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration + +let extract_prefix env info = + 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 -> + if d1 == d2 then share l1 l2 (d1 :: accu) + else (accu, d2 :: l2) + | _ -> (accu, l2) + in + share ctx1 ctx2 [] + +let typecheck_evar ev env sigma = + let info = Evd.find sigma ev in + (* Typecheck the hypotheses. *) + let type_hyp (sigma, env) decl = + 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 + (sigma, EConstr.push_named decl env) + in + let (common, changed) = extract_prefix env info 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 sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in + sigma + +(* Get the side-effect's constant declarations to update the monad's + * environmnent *) +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_effects env eff = + List.fold_left add_if_undefined env eff + +let generic_refine ~typecheck f gl = + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + let state = Proofview.Goal.state gl in + (* Save the [future_goals] state to restore them after the + refinement. *) + let prev_future_goals = Evd.save_future_goals sigma in + (* Create the refinement term *) + Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> + f >>= fun (v, c) -> + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.V82.wrap_exceptions begin fun () -> + let evs = Evd.save_future_goals sigma in + (* Redo the effects in sigma in the monad's env *) + let privates_csts = Evd.eval_side_effects sigma in + let sideff = Safe_typing.side_effects_of_private_constants privates_csts in + let env = add_side_effects env sideff in + (* Check that the introduced evars are well-typed *) + 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 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 _ = + if not (Evarutil.occur_evar_upto sigma self c) then () + else Pretype_errors.error_occur_check env sigma self c + in + (* Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals in + (* Select the goals *) + 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 sigma = match Proofview.Unsafe.advance sigma self with + | None -> + (* Nothing to do, the goal has been solved by side-effect *) + sigma + | Some self -> + match evkmain with + | None -> Evd.define self c sigma + | Some evk -> + let id = Evd.evar_ident self sigma in + let sigma = Evd.define self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma + in + (* Mark goals *) + let sigma = Proofview.Unsafe.mark_as_goals sigma comb in + let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in + let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ + Termops.Internal.print_constr_env env sigma c)) in + Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> + Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.Unsafe.tclPUTSHELF shelf <*> + Proofview.Unsafe.tclPUTGIVENUP given_up <*> + Proofview.tclUNIT v + end + +let lift c = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.V82.wrap_exceptions begin fun () -> + let (sigma, c) = c sigma in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT c + end + +let make_refine_enter ~typecheck f gl = generic_refine ~typecheck (lift f) gl + +let refine_one ~typecheck f = + Proofview.Goal.enter_one (make_refine_enter ~typecheck f) + +let refine ~typecheck f = + let f evd = + let (evd,c) = f evd in (evd,((), c)) + in + Proofview.Goal.enter (make_refine_enter ~typecheck f) + +(** Useful definitions *) + +let with_type env evd c t = + let my_type = Retyping.get_type_of env evd c in + let j = Environ.make_judge c my_type in + let (evd,j') = + Coercion.inh_conv_coerce_to true env evd j t + in + evd , j'.Environ.uj_val + +let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let f h = + let (h, c) = f h in + with_type env h c concl + in + refine ~typecheck f +end + +(** {7 solve_constraints} + + Ensure no remaining unification problems are left. Run at every "." by default. *) + +let solve_constraints = + let open Proofview in + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + Unsafe.tclEVARSADVANCE sigma + with e -> tclZERO e diff --git a/proofs/refine.mli b/proofs/refine.mli new file mode 100644 index 0000000000..1af6463a02 --- /dev/null +++ b/proofs/refine.mli @@ -0,0 +1,51 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(** The primitive refine tactic used to fill the holes in partial proofs. This + is the recommanded way to write tactics when the proof term is easy to + write down. Note that this is not the user-level refine tactic defined + in Ltac which is actually based on the one below. *) + +open Proofview + +(** {6 The refine tactic} *) + +(** {7 Refinement primitives} *) + +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) + +val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr.t)) -> 'a tactic +(** A variant of [refine] which assumes exactly one goal under focus *) + +val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> + Proofview.Goal.t -> 'a tactic +(** The general version of refine. *) + +(** {7 Helper functions} *) + +val with_type : Environ.env -> Evd.evar_map -> + EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr +(** [with_type env sigma c t] ensures that [c] is of type [t] + inserting a coercion if needed. *) + +val refine_casted : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** Like {!refine} except the refined term is coerced to the conclusion of the + current goal. *) + +(** {7 Unification constraint handling} *) + +val solve_constraints : unit tactic +(** Solve any remaining unification problems, applying heuristics. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml new file mode 100644 index 0000000000..bce227dabb --- /dev/null +++ b/proofs/refiner.ml @@ -0,0 +1,332 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 CErrors +open Util +open Evd +open Logic + +type tactic = Proofview.V82.tac + +module NamedDecl = Context.Named.Declaration + +let sig_it x = x.it +let project x = x.sigma + +(* Getting env *) + +let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) +let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) + +let refiner ~check pr goal_sigma = + let (sgl,sigma') = prim_refiner ~check pr goal_sigma.sigma goal_sigma.it in + { it = sgl; sigma = sigma'; } + +(* Profiling refiner *) +let refiner ~check = + if Flags.profile then + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key (refiner ~check) + else refiner ~check + +(*********************) +(* Tacticals *) +(*********************) + + +let unpackage glsig = (ref (glsig.sigma)), glsig.it + +let repackage r v = {it = v; sigma = !r; } + +let apply_sig_tac r tac g = + Control.check_for_interrupt (); (* Breakpoint *) + let glsigma = tac (repackage r g) in + r := glsigma.sigma; + glsigma.it + +(* [goal_goal_list : goal sigma -> goal list sigma] *) +let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } + +(* identity tactic without any message *) +let tclIDTAC gls = goal_goal_list gls + +(* the message printing identity tactic *) +let tclIDTAC_MESSAGE s gls = + Feedback.msg_info (hov 0 s); tclIDTAC gls + +(* General failure tactic *) +let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) + +(* A special exception for levels for the Fail tactic *) +exception FailError of int * Pp.t Lazy.t + +(* The Fail tactic *) +let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) + +let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) + +let start_tac gls = + let sigr, g = unpackage gls in + (sigr, [g]) + +let finish_tac (sigr,gl) = repackage sigr gl + +(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last + m subgoals, and [tac] on the others *) +let thens3parts_tac tacfi tac tacli (sigr,gs) = + let nf = Array.length tacfi in + let nl = Array.length tacli in + let ng = List.length gs in + if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals."); + 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 + (sigr,List.flatten gll) + +(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) +let thensf_tac taci tac = thens3parts_tac taci tac [||] + +(* Apply [tac i] on the ith subgoal (no subgoals number check) *) +let thensi_tac tac (sigr,gs) = + let gll = + List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in + (sigr, List.flatten gll) + +let then_tac tac = thensf_tac [||] tac + +(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] + applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to + the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] + subgoals and [tac2] to the rest of the subgoals in the middle. Raises an + error if the number of resulting subgoals is strictly less than [n+m] *) +let tclTHENS3PARTS tac1 tacfi tac tacli gls = + finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls))) + +(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the first [n] resulting + subgoals, and [tac2] to the others subgoals. Raises an error if + the number of resulting subgoals is strictly less than [n] *) +let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||] + +(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1] + to [gls] and applies [t1], ..., [tn] to the last [n] resulting + subgoals, and [tac2] to the other subgoals. Raises an error if the + number of resulting subgoals is strictly less than [n] *) +let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci + +(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies + [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the + number of subgoals is *) +let tclTHEN_i tac taci gls = + finish_tac (thensi_tac taci (then_tac tac (start_tac gls))) + +let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci +let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC + +(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||] + +(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to + [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises + an error if the number of resulting subgoals is not [n] *) +let tclTHENSV tac1 tac2v = + tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||] + +let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l) + +(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal *) +let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|] + +(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the first resulting subgoal *) +let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC + +(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More + convenient than [tclTHEN] when [n] is large. *) +let rec tclTHENLIST = function + [] -> tclIDTAC + | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl) + +(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +let tclMAP tacfun l = + List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC + +(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves +the goal unchanged *) +let tclPROGRESS tac ptree = + let rslt = tac ptree in + if Goal.V82.progress rslt ptree then rslt + else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") + +(* Execute tac, show the names of new hypothesis names created by tac + in the "as" format and then forget everything. From the logical + point of view [tclSHOWHYPS tac] is therefore equivalent to idtac, + except that it takes the time and memory of tac and prints "as" + information). The resulting (unchanged) goals are printed *after* + the as-expression, which forces pg to some gymnastic. + TODO: Have something similar (better?) in the xml protocol. + NOTE: some tactics delete hypothesis and reuse names (induction, + destruct), this is not detected by this tactical. *) +let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) + : Goal.goal list Evd.sigma = + let oldhyps = pf_hyps goal in + let rslt:Goal.goal list Evd.sigma = tac goal in + let { it = gls; sigma = sigma; } = rslt in + let hyps = + List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in + let newhyps = + List.map + (fun hypl -> List.subtract cmp hypl oldhyps) + hyps + in + 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)) + "" newhyps in + Feedback.msg_notice + (str "<infoH>" + ++ (hov 0 (str s)) + ++ (str "</infoH>")); + tclIDTAC goal;; + + +let catch_failerror (e, info) = + if catchable_exception e then Control.check_for_interrupt () + else match e with + | FailError (0,_) -> + Control.check_for_interrupt () + | FailError (lvl,s) -> + iraise (FailError (lvl - 1, s), info) + | e -> iraise (e, info) + (** FIXME: do we need to add a [Errors.push] here? *) + +(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) +let tclORELSE0 t1 t2 g = + try + t1 g + with (* Breakpoint *) + | e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; t2 g + +(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, + then applies t2 *) +let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 + +(* applies t1;t2then if t1 succeeds or t2else if t1 fails + t2* are called in terminal position (unless t1 produces more than + 1 subgoal!) *) +let tclORELSE_THEN t1 t2then t2else gls = + match + try Some(tclPROGRESS t1 gls) + with e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; None + with + | None -> t2else gls + | Some sgl -> + let sigr, gl = unpackage sgl in + finish_tac (then_tac t2then (sigr,gl)) + +(* TRY f tries to apply f, and if it fails, leave the goal unchanged *) +let tclTRY f = (tclORELSE0 f tclIDTAC) + +let tclTHENTRY f g = (tclTHEN f (tclTRY g)) + +(* Try the first tactic that does not fail in a list of tactics *) + +let rec tclFIRST = function + | [] -> tclFAIL_s "No applicable tactic." + | t::rest -> tclORELSE0 t (tclFIRST rest) + +let ite_gen tcal tac_if continue tac_else gl= + let success=ref false in + let tac_if0 gl= + let result=tac_if gl in + success:=true;result in + let tac_else0 e gl= + if !success then + iraise e + else + try + tac_else gl + with + e' when CErrors.noncritical e' -> iraise e in + try + tcal tac_if0 continue gl + with (* Breakpoint *) + | e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; tac_else0 e gl + +(* Try the first tactic and, if it succeeds, continue with + the second one, and if it fails, use the third one *) + +let tclIFTHENELSE=ite_gen tclTHEN + +(* Idem with tclTHENS and tclTHENSV *) + +let tclIFTHENSELSE=ite_gen tclTHENS + +let tclIFTHENSVELSE=ite_gen tclTHENSV + +let tclIFTHENTRYELSEMUST tac1 tac2 gl = + tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl + +(* Fails if a tactic did not solve the goal *) +let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") + +(* Try the first thats solves the current goal *) +let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) + + +(* Iteration tacticals *) + +let tclDO n t = + let rec dorec k = + if k < 0 then user_err ~hdr:"Refiner.tclDO" + (str"Wrong argument : Do needs a positive integer."); + if Int.equal k 0 then tclIDTAC + else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) + in + dorec n + + +(* Beware: call by need of CAML, g is needed *) +let rec tclREPEAT t g = + tclORELSE_THEN t (tclREPEAT t) tclIDTAC g + +let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) + +(* Repeat on the first subgoal (no failure if no more subgoal) *) +let rec tclREPEAT_MAIN t g = + (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else + tclIDTAC)) tclIDTAC) g + +(* Change evars *) +let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} + +let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} + +(* Push universe context *) +let tclPUSHCONTEXT rigid ctx tac gl = + tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl + +let tclPUSHEVARUNIVCONTEXT ctx gl = + tclEVARS (Evd.merge_universe_context (project gl) ctx) gl + +let tclPUSHCONSTRAINTS cst gl = + tclEVARS (Evd.add_constraints (project gl) cst) gl diff --git a/proofs/refiner.mli b/proofs/refiner.mli new file mode 100644 index 0000000000..52cbf7658b --- /dev/null +++ b/proofs/refiner.mli @@ -0,0 +1,133 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(** Legacy proof engine. Do not use in newly written code. *) + +open Evd +open EConstr + +(** The refiner (handles primitive rules and high-level tactics). *) +type tactic = Proofview.V82.tac + +val sig_it : 'a sigma -> 'a +val project : 'a sigma -> evar_map + +val pf_env : Goal.goal sigma -> Environ.env +val pf_hyps : Goal.goal sigma -> named_context + +val refiner : check:bool -> Constr.t -> tactic + +(** {6 Tacticals. } *) + +(** [tclIDTAC] is the identity tactic without message printing*) +val tclIDTAC : tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic + +(** [tclEVARS sigma] changes the current evar map *) +val tclEVARS : evar_map -> tactic +val tclEVARUNIVCONTEXT : UState.t -> tactic + +val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic +val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic + +val tclPUSHCONSTRAINTS : Univ.Constraint.t -> tactic + +(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [tac2] to every resulting subgoals *) +val tclTHEN : tactic -> tactic -> tactic + +(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More + convenient than [tclTHEN] when [n] is large *) +val tclTHENLIST : tactic list -> tactic + +(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *) +val tclMAP : ('a -> tactic) -> 'a list -> tactic + +(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies + [(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *) +val tclTHEN_i : tactic -> (int -> tactic) -> tactic + +(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the last resulting subgoal (previously called [tclTHENL]) *) +val tclTHENLAST : tactic -> tactic -> tactic + +(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] + to the first resulting subgoal *) +val tclTHENFIRST : tactic -> tactic -> tactic + +(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to + [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises + an error if the number of resulting subgoals is not [n] *) +val tclTHENSV : tactic -> tactic array -> tactic + +(** Same with a list of tactics *) +val tclTHENS : tactic -> tactic list -> tactic + +(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] + applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to + the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] + subgoals and [tac2] to the rest of the subgoals in the middle. Raises an + error if the number of resulting subgoals is strictly less than [n+m] *) +val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic + +(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the + last [n] resulting subgoals and [tac2] on the remaining first subgoals *) +val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic + +(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then + applies [t1],...,[tn] on the first [n] resulting subgoals and + [tac2] for the remaining last subgoals (previously called tclTHENST) *) +val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic + +(** [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, + applies [t1],...,[tn] on the last [n] resulting subgoals and leaves + unchanged the other subgoals *) +val tclTHENLASTn : tactic -> tactic array -> tactic + +(** [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then, + applies [t1],...,[tn] on the first [n] resulting subgoals and leaves + unchanged the other subgoals (previously called [tclTHENSI]) *) +val tclTHENFIRSTn : tactic -> tactic array -> tactic + +(** A special exception for levels for the Fail tactic *) +exception FailError of int * Pp.t Lazy.t + +(** Takes an exception and either raise it at the next + level or do nothing. *) +val catch_failerror : Exninfo.iexn -> unit + +val tclORELSE0 : tactic -> tactic -> tactic +val tclORELSE : tactic -> tactic -> tactic +val tclREPEAT : tactic -> tactic +val tclREPEAT_MAIN : tactic -> tactic +val tclFIRST : tactic list -> tactic +val tclSOLVE : tactic list -> tactic +val tclTRY : tactic -> tactic +val tclTHENTRY : tactic -> tactic -> tactic +val tclCOMPLETE : tactic -> tactic +val tclAT_LEAST_ONCE : tactic -> tactic +val tclFAIL : int -> Pp.t -> tactic +val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic +val tclDO : int -> tactic -> tactic +val tclPROGRESS : tactic -> tactic +val tclSHOWHYPS : tactic -> tactic + +(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, + if it succeeds, applies [tac2] to the resulting subgoals, + and if not applies [tac3] to the initial goal [gls] *) +val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic +val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic +val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic + +(** [tclIFTHENTRYELSEMUST tac1 tac2 gls] applies [tac1] then [tac2]. If [tac1] + has been successful, then [tac2] may fail. Otherwise, [tac2] must succeed. + Equivalent to [(tac1;try tac2)||tac2] *) + +val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml new file mode 100644 index 0000000000..df90354717 --- /dev/null +++ b/proofs/tacmach.ml @@ -0,0 +1,209 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Util +open Namegen +open Termops +open Environ +open Reductionops +open Evd +open Typing +open Tacred +open Logic +open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration + +let re_sig it gc = { it = it; sigma = gc; } + +(**************************************************************) +(* Operations for handling terms under a local typing context *) +(**************************************************************) + +type tactic = Proofview.V82.tac + +let sig_it = Refiner.sig_it +let project = Refiner.project +let pf_env = Refiner.pf_env +let pf_hyps = Refiner.pf_hyps + +let test_conversion env sigma pb c1 c2 = + Reductionops.check_conv ~pb env sigma c1 c2 + +let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) +let pf_hyps_types gls = + let sign = Environ.named_context (pf_env gls) in + List.map (function LocalAssum (id,x) + | LocalDef (id,_,x) -> id, EConstr.of_constr x) + sign + +let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> NamedDecl.get_id + +let pf_last_hyp gl = List.hd (pf_hyps gl) + +let pf_get_hyp gls id = + let env, sigma = pf_env gls, project gls in + try + Context.Named.lookup id (pf_hyps gls) + with Not_found -> + raise (RefinerError (env, sigma, NoSuchHyp id)) + +let pf_get_hyp_typ gls id = + id |> pf_get_hyp gls |> NamedDecl.get_type + +let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) +let pf_ids_set_of_hyps gls = + Environ.ids_of_named_context_val (Environ.named_context_val (pf_env gls)) + +let pf_get_new_id id gls = + next_ident_away id (pf_ids_set_of_hyps gls) + +let pf_global gls id = + let env = pf_env gls in + let sigma = project gls in + Evd.fresh_global env sigma (Constrintern.construct_reference (pf_hyps gls) id) + +let pf_apply f gls = f (pf_env gls) (project gls) +let pf_eapply f gls x = + on_sig gls (fun evm -> f (pf_env gls) evm x) +let pf_reduce = pf_apply +let pf_e_reduce = pf_apply + +let pf_whd_all = pf_reduce whd_all +let pf_hnf_constr = pf_reduce hnf_constr +let pf_nf = pf_reduce simpl +let pf_nf_betaiota = pf_reduce nf_betaiota +let pf_compute = pf_reduce compute +let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of +let pf_type_of = pf_reduce type_of +let pf_get_type_of = pf_reduce Retyping.get_type_of + +let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV +let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL +let pf_const_value = pf_reduce (fun env _ c -> EConstr.of_constr (constant_value_in env c)) + +let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind +let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind + +let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls + +(* Pretty-printers *) + +open Pp + +let db_pr_goal sigma g = + let env = Goal.V82.env 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 () + +let pr_gls gls = + hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) + +let pr_glls glls = + hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++ + prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) + +(* Variants of [Tacmach] functions built with the new proof engine *) +module New = struct + + let project gl = + Proofview.Goal.sigma gl + + let pf_apply f gl = + f (Proofview.Goal.env gl) (project gl) + + let of_old f gl = + f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } + + let pf_global id gl = + (* We only check for the existence of an [id] in [hyps] *) + let hyps = Proofview.Goal.hyps gl in + Constrintern.construct_reference hyps id + + let pf_env = Proofview.Goal.env + let pf_concl = Proofview.Goal.concl + + let pf_unsafe_type_of gl t = + pf_apply unsafe_type_of gl t + + let pf_type_of gl t = + pf_apply type_of gl t + + let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 + + let pf_ids_of_hyps gl = + (* We only get the identifiers in [hyps] *) + let hyps = Proofview.Goal.hyps gl in + ids_of_named_context hyps + + let pf_ids_set_of_hyps gl = + (* We only get the identifiers in [hyps] *) + let env = Proofview.Goal.env gl in + Environ.ids_of_named_context_val (Environ.named_context_val env) + + let pf_get_new_id id gl = + let ids = pf_ids_set_of_hyps gl in + next_ident_away id ids + + let pf_get_hyp id gl = + let hyps = Proofview.Goal.env gl in + let sigma = project gl in + let sign = + try EConstr.lookup_named id hyps + with Not_found -> raise (RefinerError (hyps, sigma, NoSuchHyp id)) + in + sign + + let pf_get_hyp_typ id gl = + pf_get_hyp id gl |> NamedDecl.get_type + + let pf_hyps_types gl = + let env = Proofview.Goal.env gl in + let sign = Environ.named_context env in + List.map (function LocalAssum (id,x) + | LocalDef (id,_,x) -> id, EConstr.of_constr x) + sign + + let pf_last_hyp gl = + let hyps = Proofview.Goal.hyps gl in + List.hd hyps + + let pf_nf_concl (gl : Proofview.Goal.t) = + (* We normalize the conclusion just after *) + let concl = Proofview.Goal.concl gl in + let sigma = project gl in + nf_evar sigma concl + + let pf_whd_all gl t = pf_apply whd_all gl t + + let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t + + let pf_reduce_to_quantified_ind gl t = + pf_apply reduce_to_quantified_ind gl t + + let pf_hnf_constr gl t = pf_apply hnf_constr gl t + let pf_hnf_type_of gl t = + pf_whd_all gl (pf_get_type_of gl t) + + let pf_whd_all gl t = pf_apply whd_all gl t + let pf_compute gl t = pf_apply compute gl t + + let pf_nf_evar gl t = nf_evar (project gl) t + + let pf_undefined_evars gl = + let sigma = Proofview.Goal.sigma gl in + let ev = Proofview.Goal.goal gl in + let evi = Evd.find sigma ev in + Evarutil.filtered_undefined_evars_of_evar_info sigma evi +end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli new file mode 100644 index 0000000000..213ed7bfda --- /dev/null +++ b/proofs/tacmach.mli @@ -0,0 +1,123 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Names +open Constr +open Environ +open EConstr +open Locus + +(** Operations for handling terms under a local typing context. *) + +open Evd + +type tactic = Proofview.V82.tac + +val sig_it : 'a sigma -> 'a +val project : Goal.goal sigma -> evar_map + +val re_sig : 'a -> evar_map -> 'a sigma + +val pf_concl : Goal.goal sigma -> types +val pf_env : Goal.goal sigma -> env +val pf_hyps : Goal.goal sigma -> named_context +(*i val pf_untyped_hyps : Goal.goal sigma -> (Id.t * constr) list i*) +val pf_hyps_types : Goal.goal sigma -> (Id.t * types) list +val pf_nth_hyp_id : Goal.goal sigma -> int -> Id.t +val pf_last_hyp : Goal.goal sigma -> named_declaration +val pf_ids_of_hyps : Goal.goal sigma -> Id.t list +val pf_global : Goal.goal sigma -> Id.t -> evar_map * constr +val pf_unsafe_type_of : Goal.goal sigma -> constr -> types +val pf_type_of : Goal.goal sigma -> constr -> evar_map * types +val pf_hnf_type_of : Goal.goal sigma -> constr -> types + +val pf_get_hyp : Goal.goal sigma -> Id.t -> named_declaration +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) -> + Goal.goal sigma -> 'a -> Goal.goal sigma * 'b +val pf_reduce : + (env -> evar_map -> constr -> constr) -> + Goal.goal sigma -> constr -> constr +val pf_e_reduce : + (env -> evar_map -> constr -> evar_map * constr) -> + Goal.goal sigma -> constr -> evar_map * constr + +val pf_whd_all : Goal.goal sigma -> constr -> constr +val pf_hnf_constr : Goal.goal sigma -> constr -> constr +val pf_nf : Goal.goal sigma -> constr -> constr +val pf_nf_betaiota : Goal.goal sigma -> constr -> constr +val pf_reduce_to_quantified_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +val pf_reduce_to_atomic_ind : Goal.goal sigma -> types -> (inductive * EInstance.t) * types +val pf_compute : Goal.goal sigma -> constr -> constr +val pf_unfoldn : (occurrences * evaluable_global_reference) list + -> Goal.goal sigma -> constr -> constr + +val pf_const_value : Goal.goal sigma -> pconstant -> constr +val pf_conv_x : Goal.goal sigma -> constr -> constr -> bool +val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool + +(** {6 Pretty-printing functions (debug only). } *) +val pr_gls : Goal.goal sigma -> Pp.t +val pr_glls : Goal.goal list sigma -> Pp.t +[@@ocaml.deprecated "Please move to \"new\" proof engine"] + +(** 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 -> GlobRef.t + + (** FIXME: encapsulate the level in an existential type. *) + val of_old : (Goal.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + + val project : Proofview.Goal.t -> Evd.evar_map + val pf_env : Proofview.Goal.t -> Environ.env + val pf_concl : Proofview.Goal.t -> types + + (** WRONG: To be avoided at all costs, it typechecks the term entirely but + forgets the universe constraints necessary to retypecheck it *) + val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types + + (** This function does no type inference and expects an already well-typed term. + It recomputes its type in the fastest way possible (no conversion is ever involved) *) + val pf_get_type_of : Proofview.Goal.t -> constr -> types + + (** This function entirely type-checks the term and computes its type + and the implied universe constraints. *) + val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : Proofview.Goal.t -> t -> t -> bool + + val pf_get_new_id : Id.t -> Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list + val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t + val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list + + val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> Proofview.Goal.t -> types + val pf_last_hyp : Proofview.Goal.t -> named_declaration + + val pf_nf_concl : Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * types + + val pf_hnf_constr : Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : Proofview.Goal.t -> constr -> types + + val pf_whd_all : Proofview.Goal.t -> constr -> constr + val pf_compute : Proofview.Goal.t -> constr -> constr + + val pf_nf_evar : Proofview.Goal.t -> constr -> constr + + (** Gathers the undefined evars of the given goal. *) + val pf_undefined_evars : Proofview.Goal.t -> Evar.Set.t +end diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml new file mode 100644 index 0000000000..86a7e9c527 --- /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 *) +(* <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) *) +(************************************************************************) + +(** Tactic-related types that are not totally Ltac specific and still used in + lower API. It's not clear whether this is a temporary API or if this is + meant to stay. *) + +open Names + +(** Introduction patterns *) + +type 'constr intro_pattern_expr = + | IntroForthcoming of bool + | IntroNaming of Namegen.intro_pattern_naming_expr + | IntroAction of 'constr intro_pattern_action_expr +and 'constr intro_pattern_action_expr = + | IntroWildcard + | IntroOrAndPattern of 'constr or_and_intro_pattern_expr + | IntroInjection of ('constr intro_pattern_expr) CAst.t list + | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t + | IntroRewrite of bool +and 'constr or_and_intro_pattern_expr = + | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list + | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list + +(** Bindings *) + +type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t + +type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list + +type 'a bindings = + | ImplicitBindings of 'a list + | ExplicitBindings of 'a explicit_bindings + | NoBindings + +type 'a with_bindings = 'a * 'a bindings + +type 'a delayed_open = Environ.env -> 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 |