diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 64 | ||||
| -rw-r--r-- | proofs/clenv.mli | 4 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 47 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 7 | ||||
| -rw-r--r-- | proofs/dune | 6 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/goal.ml | 46 | ||||
| -rw-r--r-- | proofs/goal.mli | 15 | ||||
| -rw-r--r-- | proofs/goal_select.ml | 68 | ||||
| -rw-r--r-- | proofs/goal_select.mli (renamed from proofs/proof_type.ml) | 34 | ||||
| -rw-r--r-- | proofs/logic.ml | 138 | ||||
| -rw-r--r-- | proofs/logic.mli | 36 | ||||
| -rw-r--r-- | proofs/miscprint.ml | 12 | ||||
| -rw-r--r-- | proofs/miscprint.mli | 7 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 136 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 45 | ||||
| -rw-r--r-- | proofs/proof.ml | 103 | ||||
| -rw-r--r-- | proofs/proof.mli | 24 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 69 | ||||
| -rw-r--r-- | proofs/proof_bullet.mli | 15 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 107 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 40 | ||||
| -rw-r--r-- | proofs/proofs.mllib | 4 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 40 | ||||
| -rw-r--r-- | proofs/refine.ml | 56 | ||||
| -rw-r--r-- | proofs/refine.mli | 4 | ||||
| -rw-r--r-- | proofs/refiner.ml | 17 | ||||
| -rw-r--r-- | proofs/refiner.mli | 13 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 41 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 102 | ||||
| -rw-r--r-- | proofs/tactypes.ml | 54 |
31 files changed, 696 insertions, 668 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 03ff580ad3..b7ccd647b5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -13,8 +13,8 @@ open CErrors open Util open Names open Nameops -open Term open Termops +open Constr open Namegen open Environ open Evd @@ -26,7 +26,7 @@ open Tacred open Pretype_errors open Evarutil open Unification -open Misctypes +open Tactypes (******************************************************************) (* Clausal environments *) @@ -62,9 +62,6 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause -let mk_freelisted c = - map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c)) - let clenv_push_prod cl = let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in let rec clrec typ = match EConstr.kind cl.evd typ with @@ -73,7 +70,7 @@ let clenv_push_prod cl = let mv = new_meta () in let dep = not (noccurn (cl_sigma cl) 1 u) in let na' = if dep then na else Anonymous in - let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in + let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in let def = applist (cl.templval.rebus,[mkMeta mv]) in { templval = mk_freelisted def; @@ -107,8 +104,7 @@ let clenv_environments evd bound t = let mv = new_meta () in let dep = not (noccurn evd 1 t2) in let na' = if dep then na else Anonymous in - let t1 = EConstr.Unsafe.to_constr t1 in - let e' = meta_declare mv t1 ~name:na' e in + let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t) @@ -167,13 +163,13 @@ let clenv_assign mv rhs clenv = user_err Pp.(str "clenv_assign: circularity in unification"); try if meta_defined clenv.evd mv then - if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then + if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then error_incompatible_inst clenv mv else clenv else let st = (Conv,TypeNotProcessed) in - {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd} + {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd} with Not_found -> user_err Pp.(str "clenv_assign: undefined meta") @@ -218,7 +214,7 @@ let clenv_assign mv rhs clenv = *) let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas + (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right @@ -288,11 +284,11 @@ let adjust_meta_source evd mv = function in situations like "ex_intro (fun x => P) ?ev p" *) let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) -> if Metaset.mem mv t.freemetas then - let f,l = decompose_app evd (EConstr.of_constr t.rebus) in + let f,l = decompose_app evd t.rebus in match EConstr.kind evd f with | Meta mv'' -> (match meta_opt_fvalue evd mv'' with - | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l + | Some (c,_) -> match_name c.rebus l | None -> None) | _ -> None else None in @@ -328,21 +324,21 @@ let adjust_meta_source evd mv = function *) let clenv_pose_metas_as_evars clenv dep_mvs = - let rec fold clenv = function - | [] -> clenv + 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 (mvs@[mv]) + 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 mvs in - fold clenv dep_mvs + fold clenv (fst (destEvar evd evar) :: evs) mvs in + fold clenv [] dep_mvs (******************************************************************) @@ -502,7 +498,6 @@ let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in - let c = EConstr.Unsafe.to_constr c in { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd } let clenv_match_args bl clenv = @@ -515,7 +510,7 @@ let clenv_match_args bl clenv = (fun clenv {CAst.loc;v=(b,c)} -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then - if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv + if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else clenv_assign_binding clenv k c) @@ -580,9 +575,9 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma let pr_clenv clenv = h 0 - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ - str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - pr_evar_map (Some 2) clenv.evd) + (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 *) @@ -608,13 +603,20 @@ let make_evar_clause env sigma ?len t = in (** FIXME: do the renaming online *) let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in - let rec clrec (sigma, holes) n t = + 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) n t + | Cast (t, _, _) -> clrec (sigma, holes) inst n t | Prod (na, t1, t2) -> - let store = Typeclasses.set_resolvable Evd.Store.empty false in - let (sigma, ev) = new_evar ~store env sigma t1 in + (** 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; @@ -624,11 +626,11 @@ let make_evar_clause env sigma ?len t = hole_name = na; } in let t2 = if dep then subst1 ev t2 else t2 in - clrec (sigma, hole :: holes) (pred n) t2 - | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t) + 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, []) bound 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) @@ -677,7 +679,7 @@ let define_with_type sigma env ev c = let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in let (ev, _) = destEvar sigma ev in - let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in + let sigma = Evd.define ev j.Environ.uj_val sigma in sigma let solve_evar_clause env sigma hyp_only clause = function diff --git a/proofs/clenv.mli b/proofs/clenv.mli index b85c4fc51b..03acb9e46e 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -18,7 +18,7 @@ open Environ open Evd open EConstr open Unification -open Misctypes +open Tactypes (** {6 The Type of Constructions clausale environments.} *) @@ -72,7 +72,7 @@ val clenv_unique_resolver : val clenv_dependent : clausenv -> metavariable list -val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv +val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list (** {6 Bindings } *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 209104ac32..4720328893 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -9,15 +9,13 @@ (************************************************************************) open Util -open Names -open Term +open Constr open Termops open Evd open EConstr open Refiner open Logic open Reduction -open Tacmach open Clenv (* This function put casts around metavariables whose type could not be @@ -54,7 +52,7 @@ let clenv_cast_meta clenv = let clenv_value_cast_meta clenv = clenv_cast_meta clenv (clenv_value clenv) -let clenv_pose_dependent_evars with_evars clenv = +let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in if not (List.is_empty dep_mvs) && not with_evars then @@ -62,53 +60,38 @@ let clenv_pose_dependent_evars with_evars clenv = (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs))); clenv_pose_metas_as_evars clenv dep_mvs -(** Use our own fast path, more informative than from Typeclasses *) -let check_tc evd = - let has_resolvable = ref false in - let check _ evi = - let res = Typeclasses.is_resolvable evi in - if res then - let () = has_resolvable := true in - Typeclasses.is_class_evar evd evi - else false - in - let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in - (has_typeclass, !has_resolvable) - -let clenv_refine with_evars ?(with_classes=true) clenv = +let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those useless goals. That deserves a FIXME. *) Proofview.V82.tactic begin fun gl -> - let clenv = clenv_pose_dependent_evars with_evars clenv in + let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in let evd' = if with_classes then - let (has_typeclass, has_resolvable) = check_tc clenv.evd in let evd' = - if has_typeclass then - Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars + Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:(not with_evars) clenv.env clenv.evd - else clenv.evd in - if has_resolvable then - Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' - else evd' + 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')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (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=false) ?(with_classes=true) ?(flags=dft ()) clenv = +let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv = Proofview.Goal.enter begin fun gl -> let clenv = clenv_unique_resolver ~flags clenv gl in - clenv_refine with_evars ~with_classes clenv + clenv_refine ?with_evars ~with_classes clenv end (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en @@ -117,11 +100,11 @@ let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = provenant de w_Unify. (Utilisé seulement dans prolog.ml) *) let fail_quick_core_unif_flags = { - modulo_conv_on_closed_terms = Some full_transparent_state; + 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 = empty_transparent_state; - modulo_delta_types = full_transparent_state; + modulo_delta = TransparentState.empty; + modulo_delta_types = TransparentState.full; check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 7c1e300b8f..d178478425 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -13,12 +13,11 @@ open Clenv open EConstr open Unification -open Misctypes (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic -val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic -val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic +val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic +val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic -val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv +val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr diff --git a/proofs/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 index 0d197c92c5..6c4193c66b 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -10,7 +10,6 @@ open CErrors open Util -open Names open Evd open Evarutil open Evarsolve @@ -25,8 +24,6 @@ open Ltac_pretype type glob_constr_ltac_closure = ltac_var_map * glob_constr let depends_on_evar sigma evk _ (pbty,_,t1,t2) = - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in try Evar.equal (head_evar sigma t1) evk with NoHeadEvar -> try Evar.equal (head_evar sigma t2) evk @@ -35,12 +32,12 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) = let define_and_solve_constraints evk c env evd = if Termops.occur_evar evd evk c then Pretype_errors.error_occur_check env evd evk c; - let evd = define evk (EConstr.Unsafe.to_constr c) evd in + let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) + | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2 | UnifFailure _ as x -> x) (Success evd) pbs with @@ -55,11 +52,10 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let flags = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = None; Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags - env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc + env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err ?loc diff --git a/proofs/goal.ml b/proofs/goal.ml index ba7e458f3a..7245d4a004 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -48,31 +48,23 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - EConstr.of_constr evi.Evd.evar_concl - - (* Access to ".evar_extra" *) - let extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra + evi.Evd.evar_concl (* Old style mk_goal primitive *) - let mk_goal evars hyps concl extra = + 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 concl = EConstr.Unsafe.to_constr concl in let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); - Evd.evar_candidates = None; - Evd.evar_extra = extra } + Evd.evar_candidates = None } in - let evi = Typeclasses.mark_unresolvable evi in - let (evars, evk) = Evarutil.new_pure_evar_full evars evi 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 @@ -80,18 +72,18 @@ module V82 = struct (evk, ev, evars) (* Instantiates a goal with an open term *) - let partial_solution sigma evk c = + 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 Environ.empty_env sigma evk c + else Pretype_errors.error_occur_check env sigma evk c in - Evd.define evk (EConstr.Unsafe.to_constr c) sigma + Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) - let partial_solution_to sigma evk evk' c = + let partial_solution_to env sigma evk evk' c = let id = Evd.evar_ident evk sigma in - let sigma = partial_solution sigma evk c in + let sigma = partial_solution env sigma evk c in match id with | None -> sigma | Some id -> Evd.rename evk' id sigma @@ -100,7 +92,9 @@ module V82 = struct let same_goal evars1 gl1 evars2 gl2 = let evi1 = Evd.find evars1 gl1 in let evi2 = Evd.find evars2 gl2 in - Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl && + let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in + let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in + Constr.equal c1 c2 && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps let weak_progress glss gls = @@ -117,20 +111,6 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl extra_hyps = - let evi = Evd.find sigma gl in - let hyps = evi.Evd.evar_hyps in - let new_hyps = - List.fold_right Environ.push_named_context_val extra_hyps hyps in - let filter = evi.Evd.evar_filter in - let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in - let new_evi = - { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in - let new_evi = Typeclasses.mark_unresolvable new_evi in - let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = sigma; } - (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = Evd.find sigma gl in @@ -156,3 +136,5 @@ module V82 = struct ) ~init:(concl sigma gl) env end + +module Set = Set.Make(struct type t = goal let compare = Evar.compare end) diff --git a/proofs/goal.mli b/proofs/goal.mli index dc9863156c..af9fb662bf 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -39,24 +39,20 @@ module V82 : sig (* Access to ".evar_concl" *) val concl : Evd.evar_map -> goal -> EConstr.constr - (* Access to ".evar_extra" *) - val extra : Evd.evar_map -> goal -> Evd.Store.t - - (* Old style mk_goal primitive, returns a new goal with corresponding + (* 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 -> - Evd.Store.t -> goal * EConstr.constr * Evd.evar_map (* Instantiates a goal with an open term *) - val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map + 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 : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map + 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 @@ -64,9 +60,6 @@ module V82 : sig (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool - (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma - (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map @@ -74,3 +67,5 @@ module V82 : sig val abstract_type : Evd.evar_map -> goal -> EConstr.types end + +module Set : sig include Set.S with type elt = goal end diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml new file mode 100644 index 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/proof_type.ml b/proofs/goal_select.mli index 149f30c673..b1c5723885 100644 --- a/proofs/proof_type.ml +++ b/proofs/goal_select.mli @@ -8,21 +8,19 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Legacy proof engine. Do not use in newly written code. *) - -open Evd -open Constr - -(** This module defines the structure of proof tree and the tactic type. So, it - is used by [Proof_tree] and [Refiner] *) - -type prim_rule = - | Refine of constr - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -type goal = Goal.goal - -type tactic = goal sigma -> goal list sigma +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 index e5294715e0..15ba0a704f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -20,10 +20,8 @@ open Environ open Reductionops open Inductiveops open Typing -open Proof_type open Type_errors open Retyping -open Misctypes module NamedDecl = Context.Named.Declaration @@ -63,6 +61,9 @@ let is_unification_error = function let catchable_exception = function | CErrors.UserError _ | TypeError _ + | Proof.OpenProof _ + (* abstract will call close_proof inside a tactic *) + | Notation.NumeralNotationError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ (* reduction errors *) @@ -185,6 +186,22 @@ let check_decl_position env sigma sign d = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +(** Printing of [move_location] *) + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" + let move_location_eq m1 m2 = match m1, m2 with | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2 @@ -214,8 +231,7 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp sigma toleft (left,declfrom,right) hto = - let env = Global.env() in +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 @@ -236,7 +252,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto = (first, d::middle) else user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ - Miscprint.pr_move_location Id.print hto ++ + pr_move_location Id.print hto ++ str (if toleft then ": it occurs in the type of " else ": it depends on ") ++ Id.print hyp ++ str ".") else @@ -264,11 +280,11 @@ 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 sigma toleft (left,declfrom,right) hto + move_hyp env sigma toleft (left,declfrom,right) hto -let insert_decl_in_named_context sigma decl hto sign = +let insert_decl_in_named_context env sigma decl hto sign = let open EConstr in - move_hyp sigma false ([],decl,named_context_of_val sign) hto + move_hyp env sigma false ([],decl,named_context_of_val sign) hto (**********************************************************************) @@ -289,7 +305,15 @@ let collect_meta_variables c = let rec collrec deep acc c = match kind c with | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc | Cast(c,_,_) -> collrec deep acc c - | (App _| Case _) -> Constr.fold (collrec deep) acc c + | Case(ci,p,c,br) -> + (* Hack assuming only two situations: the legacy one that branches, + if with Metas, are Meta, and the new one with eta-let-expanded + branches *) + let br = Array.map2 (fun n b -> try snd (Term.decompose_lam_n_decls n b) with UserError _ -> b) ci.ci_cstr_ndecls br in + Array.fold_left (collrec deep) + (Constr.fold (collrec deep) (Constr.fold (collrec deep) acc p) c) + br + | App _ -> Constr.fold (collrec deep) acc c | Proj (_, c) -> collrec deep acc c | _ -> Constr.fold (collrec true) acc c in @@ -301,9 +325,10 @@ let check_meta_variables env sigma c = let check_conv_leq_goal env sigma arg ty conclty = if !check then - let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in - if b then evm - else raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) + let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in + match ans with + | Some evm -> evm + | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty))) else sigma exception Stop of EConstr.t list @@ -326,7 +351,7 @@ 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 (Goal.V82.extra sigma goal) + 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 @@ -360,7 +385,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) then + 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 @@ -387,12 +412,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in let sigma = check_conv_leq_goal env sigma trm conclty' conclty in - let (acc'',sigma, rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -414,7 +434,7 @@ 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 (Goal.V82.extra sigma goal) in + Goal.V82.mk_goal sigma hyps concl in match kind trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; @@ -428,7 +448,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) + 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) @@ -440,12 +460,7 @@ and mk_hdgoals sigma goal goalacc trm = | Case (ci,p,c,lf) -> let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in - let (acc'',sigma,rbranches) = - Array.fold_left2 - (fun (lacc,sigma,bacc) ty fi -> - let (r,_,s,b') = mk_refgoals sigma goal lacc ty fi in r,s,(b'::bacc)) - (acc',sigma,[]) lbrty lf - in + let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in let lf' = Array.rev_of_list rbranches in let ans = if p' == p && c' == c && Array.equal (==) lf' lf then trm @@ -483,7 +498,7 @@ and mk_arggoals sigma goal goalacc funty allargs = let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in - Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs + Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in @@ -497,6 +512,50 @@ and mk_casegoals sigma goal goalacc p c = let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') +and treat_case sigma goal ci lbrty lf acc' = + let rec strip_outer_cast c = match kind c with + | Cast (c,_,_) -> strip_outer_cast c + | _ -> c in + let decompose_app_vect c = match kind c with + | App (f,cl) -> (f, cl) + | _ -> (c,[||]) in + let env = Goal.V82.env sigma goal in + Array.fold_left3 + (fun (lacc,sigma,bacc) ty fi l -> + if isMeta (strip_outer_cast fi) then + (* Support for non-eta-let-expanded Meta as found in *) + (* destruct/case with an non eta-let expanded elimination scheme *) + let (r,_,s,fi') = mk_refgoals sigma goal lacc ty fi in + r,s,(fi'::bacc) + else + (* Deal with a branch in expanded form of the form + Case(ci,p,c,[|eta-let-exp(Meta);...;eta-let-exp(Meta)|]) as + if it were not so, so as to preserve compatibility with when + destruct/case generated schemes of the form + Case(ci,p,c,[|Meta;...;Meta|]; + CAUTION: it does not deal with the general case of eta-zeta + reduced branches having a form different from Meta, as it + would be theoretically the case with third-party code *) + let n = List.length l in + let ctx, body = Term.decompose_lam_n_decls n fi in + let head, args = decompose_app_vect body in + (* Strip cast because clenv_cast_meta adds a cast when the branch is + eta-expanded but when not when the branch has the single-meta + form [Meta] *) + let head = strip_outer_cast head in + if isMeta head then begin + assert (args = Context.Rel.to_extended_vect mkRel 0 ctx); + let head' = lift (-n) head in + let (r,_,s,head'') = mk_refgoals sigma goal lacc ty head' in + let fi' = it_mkLambda_or_LetIn (mkApp (head'',args)) ctx in + (r,s,fi'::bacc) + end + else + (* Supposed to be meta-free *) + let sigma, t'ty = goal_type_of env sigma fi in + let sigma = check_conv_leq_goal env sigma fi t'ty ty in + (lacc,sigma,fi::bacc)) + (acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags let convert_hyp check sign sigma d = let id = NamedDecl.get_id d in @@ -525,12 +584,15 @@ let convert_hyp check sign sigma d = let prim_refiner r sigma goal = let env = Goal.V82.env sigma goal in let cl = Goal.V82.concl sigma goal in - match r with - (* Logical rules *) - | Refine c -> - let cl = EConstr.Unsafe.to_constr cl in - check_meta_variables env sigma c; - let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in - let sgl = List.rev sgl in - let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in - (sgl, sigma) + 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 index dc471bb5fe..f99076db23 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -13,27 +13,20 @@ open Names open Constr open Evd -open Proof_type -(** This suppresses check done in [prim_refiner] for the tactic given in - argument; works by side-effect *) - -val with_check : tactic -> tactic - -(** [without_check] respectively means:\\ - [Intro]: no check that the name does not exist\\ - [Intro_after]: no check that the name does not exist and that variables in +(** [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]: no check that the name does not exist and that + [Intro_replacing]: check that the name does not exist and that variables in its type does not escape their scope\\ [Convert_hyp]: - no check that the name exist and that its type is convertible\\ + check that the name exist and that its type is convertible\\ *) (** The primitive refiner. *) -val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map - +val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map (** {6 Refiner errors. } *) @@ -58,12 +51,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a val catchable_exception : exn -> bool +(** Move destination for hypothesis *) + +type 'id move_location = + | MoveAfter of 'id + | MoveBefore of 'id + | MoveFirst + | MoveLast (** can be seen as "no move" when doing intro *) + +val pr_move_location : + ('a -> Pp.t) -> 'a move_location -> Pp.t + val convert_hyp : bool -> Environ.named_context_val -> evar_map -> EConstr.named_declaration -> Environ.named_context_val -val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val -val insert_decl_in_named_context : Evd.evar_map -> - EConstr.named_declaration -> Id.t Misctypes.move_location -> +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 index 1a63ff6734..ec17b8076f 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -10,7 +10,7 @@ open Pp open Names -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with | IntroNaming p -> pr_intro_pattern_naming p | IntroAction p -> pr_intro_pattern_action prc p -and pr_intro_pattern_naming = function +and pr_intro_pattern_naming = let open Namegen in function | IntroIdentifier id -> Id.print id | IntroFresh id -> str "?" ++ Id.print id | IntroAnonymous -> str "?" @@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) ++ str "]" -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - (** Printing of bindings *) let pr_binding prc = let open CAst in function | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index 79790a277b..f4e2e683d1 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Misctypes +open Tactypes (** Printing of [intro_pattern] *) @@ -18,13 +18,10 @@ val pr_intro_pattern : val pr_or_and_intro_pattern : ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t +val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t (** Printing of [move_location] *) -val pr_move_location : - ('a -> Pp.t) -> 'a move_location -> Pp.t - val pr_bindings : ('a -> Pp.t) -> ('a -> Pp.t) -> 'a bindings -> Pp.t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 8725f51cd7..886a62cb89 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -16,58 +16,38 @@ open Environ open Evd let use_unification_heuristics_ref = ref true -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = "Solve unification constraints at every \".\""; - Goptions.optkey = ["Solve";"Unification";"Constraints"]; - Goptions.optread = (fun () -> !use_unification_heuristics_ref); - Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); -} +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 -let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator = - let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof sigma id ?pl str goals terminator; - let env = Global.env () in - ignore (Proof_global.with_current_proof (fun _ p -> - match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic env tac p)) - -let cook_this_proof p = - match p with - | { Proof_global.id;entries=[constr];persistence;universes } -> - (id,(constr,universes,persistence)) - | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") - -let cook_proof () = - cook_this_proof (fst - (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x))) - exception NoSuchGoal -let _ = CErrors.register_handler begin function +let () = CErrors.register_handler begin function | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") | _ -> raise CErrors.Unhandled end -let get_nth_V82_goal i = - let p = Proof_global.give_me_the_proof () in +let get_nth_V82_goal p i = let goals,_,_,_,sigma = Proof.proof p in try { it = List.nth goals (i-1) ; sigma } with Failure _ -> raise NoSuchGoal -let get_goal_context_gen i = - let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in +let get_goal_context_gen p i = + let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = - try get_goal_context_gen i + try get_goal_context_gen (Proof_global.give_me_the_proof ()) i with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.") let get_current_goal_context () = - try get_goal_context_gen 1 + try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1 with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.") | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, @@ -75,14 +55,18 @@ let get_current_goal_context () = let env = Global.env () in (Evd.from_env env, env) -let get_current_context () = - try get_goal_context_gen 1 +let get_current_context ?p () = + let current_proof_by_default = function + | Some p -> p + | None -> Proof_global.give_me_the_proof () + in + try get_goal_context_gen (current_proof_by_default p) 1 with Proof_global.NoCurrentProof -> let env = Global.env () in (Evd.from_env env, env) | NoSuchGoal -> (* No more focused goals ? *) - let p = Proof_global.give_me_the_proof () in + let p = (current_proof_by_default p) in let evd = Proof.in_proof p (fun x -> x) in (evd, Global.env ()) @@ -100,11 +84,23 @@ let solve ?with_end_tac gi info_lvl tac pr = | None -> tac | Some _ -> Proofview.Trace.record_info_trace tac in - let tac = match gi with - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac - | Vernacexpr.SelectAll -> tac + let tac = let open Goal_select in match gi with + | SelectAlreadyFocused -> + let open Proofview.Notations in + Proofview.numgoals >>= fun n -> + if n == 1 then tac + else + let e = CErrors.UserError + (None, + Pp.(str "Expected a single focused goal but " ++ + int n ++ str " goals are focused.")) + in + Proofview.tclZERO e + + | SelectNth i -> Proofview.tclFOCUS i i tac + | SelectList l -> Proofview.tclFOCUSLIST l tac + | SelectId id -> Proofview.tclFOCUSID id tac + | SelectAll -> tac in let tac = if use_unification_heuristics () then @@ -121,7 +117,7 @@ let solve ?with_end_tac gi info_lvl tac pr = with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof") -let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) +let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) let instantiate_nth_evar_com n com = Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.instantiate_evar n com p) @@ -137,13 +133,19 @@ 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 - start_proof id goal_kind evd sign typ terminator; + 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 _,(const,univs,_) = cook_proof () in - Proof_global.discard_current (); - let univs = UState.demote_seff_univs const univs in - const, status, univs + 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 (); @@ -161,8 +163,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in - let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - cb, status, Evd.evar_universe_context univs' + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + cb, status, univs let refine_by_tactic env sigma ty tac = (** Save the initial side-effects to restore them afterwards. We set the @@ -188,8 +190,7 @@ let refine_by_tactic env sigma ty tac = | [c, _] -> c | _ -> assert false in - let ans = Reductionops.nf_evar sigma ans in - let ans = EConstr.Unsafe.to_constr ans in + let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in (** [neff] contains the freshly generated side-effects *) let neff = Evd.eval_side_effects sigma in (** Reset the old side-effects *) @@ -213,36 +214,3 @@ let refine_by_tactic env sigma ty tac = this hack will work in most cases. *) let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma - -(**********************************************************************) -(* Support for resolution of evars in tactic interpretation, including - resolution by application of tactics *) - -let implicit_tactic = Summary.ref None ~name:"implicit-tactic" - -let declare_implicit_tactic tac = implicit_tactic := Some tac - -let clear_implicit_tactic () = implicit_tactic := None - -let apply_implicit_tactic tac = (); fun env sigma evk -> - let evi = Evd.find_undefined sigma evk in - match snd (evar_source evk sigma) with - | (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) - when - Context.Named.equal Constr.equal (Environ.named_context_of_val evi.evar_hyps) - (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in - (try - let c = Evarutil.nf_evars_universes sigma evi.evar_concl in - let c = EConstr.of_constr c in - if Evarutil.has_undefined_evars sigma c then raise Exit; - let (ans, _, ctx) = - build_by_tactic env (Evd.evar_universe_context sigma) c tac in - let sigma = Evd.set_universe_context sigma ctx in - sigma, EConstr.of_constr ans - with e when Logic.catchable_exception e -> raise Exit) - | _ -> raise Exit - -let solve_by_implicit_tactic () = match !implicit_tactic with -| None -> None -| Some tac -> Some (apply_implicit_tactic tac) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 65cde3a3ae..155221947a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -16,34 +16,6 @@ open Environ open Decl_kinds (** {6 ... } *) -(** [start_proof s str env t hook tac] starts a proof of name [s] and - conclusion [t]; [hook] is optionally a function to be applied at - proof end (e.g. to declare the built constructions as a coercion - or a setoid morphism); init_tac is possibly a tactic to - systematically apply at initialization time (e.g. to start the - proof of mutually dependent theorems) *) - -val start_proof : - Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> - ?init_tac:unit Proofview.tactic -> - Proof_global.proof_terminator -> unit - -(** {6 ... } *) -(** [cook_proof opacity] turns the current proof (assumed completed) into - a constant with its name, kind and possible hook (see [start_proof]); - it fails if there is no current proof of if it is not completed; - it also tells if the guardness condition has to be inferred. *) - -val cook_this_proof : - Proof_global.proof_object -> - (Id.t * - (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) - -val cook_proof : unit -> - (Id.t * - (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) - -(** {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 *) @@ -60,7 +32,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env If there is no pending proof then it returns the current global environment and empty evar_map. *) -val get_current_context : unit -> Evd.evar_map * env +val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env (** [current_proof_statement] *) @@ -75,7 +47,7 @@ val current_proof_statement : tac] applies [tac] to all subgoals. *) val solve : ?with_end_tac:unit Proofview.tactic -> - Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> + Goal_select.t -> int option -> unit Proofview.tactic -> Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current @@ -85,6 +57,9 @@ val solve : ?with_end_tac:unit Proofview.tactic -> val by : unit Proofview.tactic -> bool +(** Option telling if unification heuristics should be used. *) +val use_unification_heuristics : unit -> bool + (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th @@ -113,13 +88,3 @@ val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.ta 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. *) - -(** Declare the default tactic to fill implicit arguments *) - -val declare_implicit_tactic : unit Proofview.tactic -> unit - -(** To remove the default tactic *) -val clear_implicit_tactic : unit -> unit - -(* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option diff --git a/proofs/proof.ml b/proofs/proof.ml index 51e0a1d614..6c13c4946a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -63,6 +63,7 @@ exception CannotUnfocusThisWay (* Cannot focus on non-existing subgoals *) exception NoSuchGoals of int * int +exception NoSuchGoal of Names.Id.t exception FullyUnfocused @@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function CErrors.user_err ~hdr:"Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) + | NoSuchGoal id -> + CErrors.user_err + ~hdr:"Focus" + Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".") | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused") | _ -> raise CErrors.Unhandled end @@ -117,8 +122,6 @@ type t = { initial_euctx : UState.t } -type proof = t - (*** General proof functions ***) let proof p = @@ -230,6 +233,37 @@ let focus cond inf i pr = try _focus cond (Obj.repr inf) i i pr with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i)) +(* Focus on the goal named id *) +let focus_id cond inf id pr = + let (focused_goals, evar_map) = Proofview.proofview pr.proofview in + begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with + | Some ev -> + begin match CList.safe_index Evar.equal ev focused_goals with + | Some i -> + (* goal is already under focus *) + _focus cond (Obj.repr inf) i i pr + | None -> + if CList.mem_f Evar.equal ev pr.shelf then + (* goal is on the shelf, put it in focus *) + let proofview = Proofview.unshelve [ev] pr.proofview in + let shelf = + CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf + in + let pr = { pr with proofview; shelf } in + let (focused_goals, _) = Proofview.proofview pr.proofview in + let i = + (* Now we know that this will succeed *) + try CList.index Evar.equal ev focused_goals + with Not_found -> assert false + in + _focus cond (Obj.repr inf) i i pr + else + raise CannotUnfocusThisWay + end + | None -> + raise (NoSuchGoal id) + end + let rec unfocus kind pr () = let cond = cond_of_focus pr in match test_cond cond kind pr.proofview with @@ -301,28 +335,42 @@ let dependent_start goals = let number_of_goals = List.length (Proofview.initial_goals pr.entry) in _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr -exception UnfinishedProof -exception HasShelvedGoals -exception HasGivenUpGoals -exception HasUnresolvedEvar -let _ = CErrors.register_handler begin function - | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.") - | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.") - | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.") - | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.") - | _ -> raise CErrors.Unhandled -end +type open_error_reason = + | UnfinishedProof + | HasShelvedGoals + | HasGivenUpGoals + | HasUnresolvedEvar -let return p = +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 UnfinishedProof + raise (OpenProof(pid, UnfinishedProof)) else if has_shelved_goals p then - raise HasShelvedGoals + raise (OpenProof(pid, HasShelvedGoals)) else if has_given_up_goals p then - raise HasGivenUpGoals + raise (OpenProof(pid, HasGivenUpGoals)) else if has_unresolved_evar p then (* spiwack: for compatibility with <= 8.3 proof engine *) - raise HasUnresolvedEvar + raise (OpenProof(pid, HasUnresolvedEvar)) else let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview @@ -352,7 +400,7 @@ let run_tactic env tac pr = (* 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 = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in + let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved in @@ -399,9 +447,6 @@ let pr_proof p = (*** Compatibility layer with <=v8.2 ***) module V82 = struct - let subgoals p = - let it, sigma = Proofview.proofview p.proofview in - Evd.{ it; sigma } let background_subgoals p = let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in @@ -418,11 +463,10 @@ module V82 = struct let grab_evars p = if not (is_done p) then - raise UnfinishedProof + raise (OpenProof(None, UnfinishedProof)) else { p with proofview = Proofview.V82.grab p.proofview } - (* Main component of vernac command Existential *) let instantiate_evar n com pr = let tac = @@ -452,3 +496,14 @@ module V82 = struct { pr with proofview ; shelf } end + +let all_goals p = + let add gs set = + List.fold_left (fun s g -> Goal.Set.add g s) set gs in + let (goals,stack,shelf,given_up,_) = proof p in + let set = add goals Goal.Set.empty in + let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in + let set = add shelf set in + let set = add given_up set in + let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in + add bgoals set diff --git a/proofs/proof.mli b/proofs/proof.mli index c0e832fb8c..aaabea3454 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -33,8 +33,6 @@ (* Type of a proof. *) type t -type proof = t -[@@ocaml.deprecated "please use [Proof.t]"] (* Returns a stylised view of a proof for use by, for instance, ide-s. *) @@ -91,11 +89,15 @@ val compact : t -> t 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. *) -exception UnfinishedProof -exception HasShelvedGoals -exception HasGivenUpGoals -exception HasUnresolvedEvar -val return : t -> Evd.evar_map +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 ***) @@ -137,6 +139,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition a need for it? *) val focus : 'a focus_condition -> 'a -> int -> t -> t +(* focus on goal named id *) +val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t + exception FullyUnfocused exception CannotUnfocusThisWay @@ -189,8 +194,6 @@ val pr_proof : t -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig - val subgoals : t -> Goal.goal list Evd.sigma - [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) val background_subgoals : t -> Goal.goal list Evd.sigma @@ -207,3 +210,6 @@ module V82 : sig (* Implements the Existential command *) val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end + +(* returns the set of all goals in the proof *) +val all_goals : t -> Goal.Set.t diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index e22d382f7d..2ca4f0afb4 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -10,19 +10,22 @@ open Proof -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int let bullet_eq b1 b2 = match b1, b2 with -| Vernacexpr.Dash n1, Vernacexpr.Dash n2 -> n1 = n2 -| Vernacexpr.Star n1, Vernacexpr.Star n2 -> n1 = n2 -| Vernacexpr.Plus n1, Vernacexpr.Plus n2 -> n1 = n2 +| Dash n1, Dash n2 -> n1 = n2 +| Star n1, Star n2 -> n1 = n2 +| Plus n1, Plus n2 -> n1 = n2 | _ -> false let pr_bullet b = match b with - | Vernacexpr.Dash n -> Pp.(str (String.make n '-')) - | Vernacexpr.Star n -> Pp.(str (String.make n '*')) - | Vernacexpr.Plus n -> Pp.(str (String.make n '+')) + | Dash n -> Pp.(str (String.make n '-')) + | Star n -> Pp.(str (String.make n '*')) + | Plus n -> Pp.(str (String.make n '+')) type behavior = { @@ -173,7 +176,7 @@ end (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "bullet behavior"; @@ -194,53 +197,3 @@ let put p b = let suggest p = (!current_behavior).suggest p - -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - - -(* Default goal selector: selector chosen when a tactic is applied - without an explicit selector. *) -let default_goal_selector = ref (Vernacexpr.SelectNth 1) -let get_default_goal_selector () = !default_goal_selector - -let pr_range_selector (i, j) = - if i = j then Pp.int i - else Pp.(int i ++ str "-" ++ int j) - -let pr_goal_selector = function - | Vernacexpr.SelectAll -> Pp.str "all" - | Vernacexpr.SelectNth i -> Pp.int i - | Vernacexpr.SelectList l -> - Pp.(str "[" - ++ prlist_with_sep pr_comma pr_range_selector l - ++ str "]") - | Vernacexpr.SelectId id -> Names.Id.print id - -let parse_goal_selector = function - | "all" -> Vernacexpr.SelectAll - | i -> - let err_msg = "The default selector must be \"all\" or a natural number." in - begin try - let i = int_of_string i in - if i < 0 then CErrors.user_err Pp.(str err_msg); - Vernacexpr.SelectNth i - with Failure _ -> CErrors.user_err Pp.(str err_msg) - end - -let _ = - Goptions.(declare_string_option{optdepr = false; - optname = "default goal selector" ; - optkey = ["Default";"Goal";"Selector"] ; - optread = begin fun () -> - Pp.string_of_ppcmds - (pr_goal_selector !default_goal_selector) - end; - optwrite = begin fun n -> - default_goal_selector := parse_goal_selector n - end - }) - diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index ffbaa0fac9..0fcc647a6f 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -14,7 +14,10 @@ (* *) (**********************************************************) -type t = Vernacexpr.bullet +type t = + | Dash of int + | Star of int + | Plus of int (** A [behavior] is the data of a put function which is called when a bullet prefixes a tactic, a suggest function @@ -41,13 +44,3 @@ val register_behavior : behavior -> unit *) val put : Proof.t -> t -> Proof.t val suggest : Proof.t -> Pp.t - -(**********************************************************) -(* *) -(* Default goal selector *) -(* *) -(**********************************************************) - -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t -val get_default_goal_selector : unit -> Vernacexpr.goal_selector - diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d6c0e33414..095aa36f03 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -53,7 +53,7 @@ let default_proof_mode = ref (find_proof_mode "No") let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name -let _ = +let () = Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; @@ -78,11 +78,14 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * - Misctypes.lident option * + | Proved of opacity_flag * + lident option * proof_object + type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator @@ -90,15 +93,14 @@ type pstate = { pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; - section_vars : Context.Named.t option; + section_vars : Constr.named_context option; proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; - universe_decl: Univdecls.universe_decl; + universe_decl: UState.universe_decl; } type t = pstate list -type state = t let make_terminator f = f let apply_terminator f = f @@ -126,13 +128,13 @@ let push a l = l := a::!l; update_proof_mode () exception NoSuchProof -let _ = CErrors.register_handler begin function +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 +let () = CErrors.register_handler begin function | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).") | _ -> raise CErrors.Unhandled end @@ -174,7 +176,6 @@ 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 @@ -235,13 +236,6 @@ let activate_proof_mode mode = let disactivate_current_proof_mode () = CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) -let default_universe_decl = - let open Misctypes in - { univdecl_instance = []; - univdecl_extensible_instance = true; - univdecl_constraints = Univ.Constraint.empty; - univdecl_extensible_constraints = true } - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -250,7 +244,7 @@ let default_universe_decl = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = +let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -262,7 +256,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator = universe_decl = pl } in push initial_state pstates -let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator = +let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator = let initial_state = { pid = id; terminator = CEphemeron.create terminator; @@ -278,12 +272,12 @@ let get_used_variables () = (cur_pstate ()).section_vars let get_universe_decl () = (cur_pstate ()).universe_decl let proof_using_auto_clear = ref false -let _ = Goptions.declare_bool_option - { Goptions.optdepr = false; - Goptions.optname = "Proof using Clear Unused"; - Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; - Goptions.optread = (fun () -> !proof_using_auto_clear); - Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } +let () = Goptions.(declare_bool_option + { optdepr = false; + optname = "Proof using Clear Unused"; + optkey = ["Proof";"Using";"Clear";"Unused"]; + optread = (fun () -> !proof_using_auto_clear); + optwrite = (fun b -> proof_using_auto_clear := b) }) let set_used_variables l = let open Context.Named.Declaration in @@ -324,10 +318,23 @@ let get_open_goals () = type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t -let close_proof ~keep_body_ucst_separate ?feedback_id ~now +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 { pid; section_vars; strength; proof; terminator; universe_decl } = cur_pstate () in + let opaque = match opaque with Opaque -> true | Transparent -> false in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let initial_euctx = Proof.initial_euctx proof in @@ -340,8 +347,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now have existential variables in the initial types of goals, we need to normalise them for the kernel. *) let subst_evar k = - Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in - let nf = Universes.nf_evars_and_universes_opt_subst subst_evar + Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in + let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar (UState.subst universes) in let make_body = if poly || now then @@ -352,9 +359,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now not (Safe_typing.empty_private_constants = eff)) in let typ = if allow_deferred then t else nf t in - let env = Global.env () in - let used_univs_body = Univops.universes_of_constr env body in - let used_univs_typ = Univops.universes_of_constr env typ in + let used_univs_body = 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 @@ -365,6 +371,16 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now 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 @@ -401,7 +417,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_feedback = feedback_id; const_entry_type = Some typ; const_entry_inline_code = false; - const_entry_opaque = true; + const_entry_opaque = opaque; const_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl initial_goals in @@ -422,33 +438,20 @@ let return_proof ?(allow_partial=false) () = proofs, Evd.evar_universe_context evd end else let initial_goals = Proof.initial_goals proof in - let evd = - let error s = - let prf = str " (in proof " ++ Id.print pid ++ str ")" in - raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf)) - in - try Proof.return proof with - | Proof.UnfinishedProof -> - error(str"Attempt to save an incomplete proof") - | Proof.HasShelvedGoals -> - error(str"Attempt to save a proof with shelved goals") - | Proof.HasGivenUpGoals -> - error(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.") - | Proof.HasUnresolvedEvar-> - error(strbrk"Attempt to save a proof with existential variables still non-instantiated") 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, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in + let proofs = + List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~feedback_id proof = - close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof -let close_proof ~keep_body_ucst_separate fix_exn = - close_proof ~keep_body_ucst_separate ~now:true +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 @@ -487,7 +490,7 @@ let update_global_env () = (p, ()))) (* XXX: Bullet hook, should be really moved elsewhere *) -let _ = +let () = let hook n = try let prf = give_me_the_proof () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index bf35fd6599..d9c32cf9d5 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,8 +13,6 @@ environment. *) type t -type state = t -[@@ocaml.deprecated "please use [Proof_global.t]"] val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -22,7 +20,7 @@ val check_no_pending_proof : unit -> unit val get_current_proof_name : unit -> Names.Id.t val get_all_proof_names : unit -> Names.Id.t list -val discard : Misctypes.lident -> unit +val discard : Names.lident -> unit val discard_current : unit -> unit val discard_all : unit -> unit @@ -48,11 +46,13 @@ type proof_object = { universes: UState.t; } +type opacity_flag = Opaque | Transparent + type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Vernacexpr.opacity_flag * - Misctypes.lident option * + | Proved of opacity_flag * + Names.lident option * proof_object type proof_terminator type closed_proof = proof_object * proof_terminator @@ -60,23 +60,23 @@ 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 (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. *) +(** [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:Univdecls.universe_decl -> + Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command @@ -86,7 +86,7 @@ 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 : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof +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 @@ -97,7 +97,7 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt (* 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 : feedback_id:Stateid.t -> +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 @@ -124,11 +124,11 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Misctypes.lident list -val get_used_variables : unit -> Context.Named.t option + Names.Id.t list -> Constr.named_context * Names.lident list +val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : unit -> Univdecls.universe_decl +val get_universe_decl : unit -> UState.universe_decl module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 058e839b47..dbd5be23ab 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -1,10 +1,10 @@ Miscprint Goal Evar_refiner -Proof_type -Logic Refine Proof +Logic +Goal_select Proof_bullet Proof_global Redexpr diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6fb4119387..6658c37f41 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -12,10 +12,9 @@ open Pp open CErrors open Util open Names -open Term +open Constr open EConstr open Declarations -open Globnames open Genredexpr open Pattern open Reductionops @@ -23,7 +22,6 @@ open Tacred open CClosure open RedFlags open Libobject -open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = @@ -53,17 +51,17 @@ let whd_cbn flags env sigma t = Reductionops.Stack.zip ~refold:true sigma state let strong_cbn flags = - strong (whd_cbn flags) + strong_with_flags whd_cbn flags let simplIsCbn = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; - Goptions.optname = +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = "Plug the simpl tactic to the new cbn mechanism"; - Goptions.optkey = ["SimplIsCbn"]; - Goptions.optread = (fun () -> !simplIsCbn); - Goptions.optwrite = (fun a -> simplIsCbn:=a); -} + optkey = ["SimplIsCbn"]; + optread = (fun () -> !simplIsCbn); + optwrite = (fun a -> simplIsCbn:=a); +}) let set_strategy_one ref l = let k = @@ -80,7 +78,7 @@ let set_strategy_one ref l = | OpaqueDef _ -> user_err ~hdr:"set_transparent_const" (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++ + Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++ spc () ++ str "transparent because it was declared opaque."); | _ -> Csymtable.set_transparent_const sp) | _ -> () @@ -92,9 +90,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - List.smartmap + List.Smart.map (fun (k,ql as entry) -> - let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj @@ -115,10 +113,8 @@ let classify_strategy (local,_ as obj) = let disch_ref ref = match ref with - EvalConstRef c -> - let c' = Lib.discharge_con c in - if c==c' then Some ref else Some (EvalConstRef c') - | EvalVarRef id -> if Lib.is_in_section (VarRef id) then None else Some ref + EvalConstRef c -> Some ref + | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref let discharge_strategy (_,(local,obj)) = if local then None else @@ -164,7 +160,7 @@ let make_flag env f = (fun v red -> red_sub red (make_flag_constant v)) f.rConst red else (* Only rConst *) - let red = red_add_transparent (red_add red fDELTA) all_opaque in + let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in List.fold_right (fun v red -> red_add red (make_flag_constant v)) f.rConst red @@ -200,8 +196,8 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") - | ArgArg x -> x + | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") + | Locus.ArgArg x -> x let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) @@ -263,7 +259,7 @@ let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) let subst_red_expr subs = - Miscops.map_red_expr_gen + Redops.map_red_expr_gen (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) (Patternops.subst_pattern subs) diff --git a/proofs/refine.ml b/proofs/refine.ml index 909556b1ee..540a8bb420 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -15,7 +15,7 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in + let ctx1 = List.rev (EConstr.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in let rec share l1 l2 accu = match l1, l2 with | d1 :: l1, d2 :: l2 -> @@ -29,47 +29,31 @@ let typecheck_evar ev env sigma = let info = Evd.find sigma ev in (** Typecheck the hypotheses. *) let type_hyp (sigma, env) decl = - let t = EConstr.of_constr (NamedDecl.get_type decl) in - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref t in - let () = match decl with - | LocalAssum _ -> () - | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t + let t = NamedDecl.get_type decl in + let sigma, _ = Typing.sort_of env sigma t in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,body,_) -> Typing.check env sigma body t in - (!evdref, Environ.push_named decl env) + (sigma, EConstr.push_named decl env) in let (common, changed) = extract_prefix env info in - let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in + let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in - !evdref - -let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.e_check env evdref c concl in - !evdref - -let (pr_constrv,pr_constr) = - Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") () + 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 kn cb env = - try ignore(Environ.lookup_constant kn env); env - with Not_found -> Environ.add_constant kn cb env +let add_if_undefined env eff = + let open Entries in + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env (* Add the side effects to the monad's environment, if not already done. *) -let add_side_effect env = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - add_if_undefined kn cb env - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.fold_left (fun env (_,kn,cb,eff_env) -> - add_if_undefined kn cb env) env l - -let add_side_effects env effects = - List.fold_left (fun env eff -> add_side_effect env eff) env effects +let add_side_effects env eff = + List.fold_left add_if_undefined env eff let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in @@ -93,7 +77,7 @@ let generic_refine ~typecheck f gl = let fold accu ev = typecheck_evar ev env accu in let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in (** Check that the refined term is typesafe *) - let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in + let sigma = if typecheck then Typing.check env sigma c concl else sigma in (** Check that the goal itself does not appear in the refined term *) let self = Proofview.Goal.goal gl in let _ = @@ -106,7 +90,6 @@ let generic_refine ~typecheck f gl = let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (** Proceed to the refinement *) - let c = EConstr.Unsafe.to_constr c in let sigma = match Proofview.Unsafe.advance sigma self with | None -> (** Nothing to do, the goal has been solved by side-effect *) @@ -122,9 +105,10 @@ let generic_refine ~typecheck f gl = | Some id -> Evd.rename evk id sigma in (** Mark goals *) - let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + 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 () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in + let trace () = 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 <*> diff --git a/proofs/refine.mli b/proofs/refine.mli index 70a23a9fba..1af6463a02 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -17,10 +17,6 @@ open Proofview (** {6 The refine tactic} *) -(** Printer used to print the constr which refine refines. *) -val pr_constr : - (Environ.env -> Evd.evar_map -> Constr.constr -> Pp.t) Hook.t - (** {7 Refinement primitives} *) val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic diff --git a/proofs/refiner.ml b/proofs/refiner.ml index be32aadd91..bce227dabb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -12,9 +12,10 @@ open Pp open CErrors open Util open Evd -open Proof_type open Logic +type tactic = Proofview.V82.tac + module NamedDecl = Context.Named.Declaration let sig_it x = x.it @@ -25,16 +26,16 @@ let project x = x.sigma 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 pr goal_sigma = - let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in +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 = +let refiner ~check = if Flags.profile then let refiner_key = CProfile.declare_profile "refiner" in - CProfile.profile2 refiner_key refiner - else refiner + CProfile.profile2 refiner_key (refiner ~check) + else refiner ~check (*********************) (* Tacticals *) @@ -178,9 +179,9 @@ let tclPROGRESS tac ptree = 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) - :Proof_type.goal list Evd.sigma = + : Goal.goal list Evd.sigma = let oldhyps = pf_hyps goal in - let rslt:Proof_type.goal list Evd.sigma = tac 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 diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 5cd703a25c..52cbf7658b 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -11,23 +11,18 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Proof_type 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 sigma -> Environ.env -val pf_hyps : goal sigma -> named_context +val pf_env : Goal.goal sigma -> Environ.env +val pf_hyps : Goal.goal sigma -> named_context -val unpackage : 'a sigma -> evar_map ref * 'a -val repackage : evar_map ref -> 'a -> 'a sigma -val apply_sig_tac : - evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list - -val refiner : rule -> tactic +val refiner : check:bool -> Constr.t -> tactic (** {6 Tacticals. } *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 1889054f86..64d7630d55 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -17,9 +17,7 @@ open Evd open Typing open Redexpr open Tacred -open Proof_type open Logic -open Refiner open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -30,12 +28,7 @@ let re_sig it gc = { it = it; sigma = gc; } (* Operations for handling terms under a local typing context *) (**************************************************************) -type 'a sigma = 'a Evd.sigma;; -type tactic = Proof_type.tactic;; - -let unpackage = Refiner.unpackage -let repackage = Refiner.repackage -let apply_sig_tac = Refiner.apply_sig_tac +type tactic = Proofview.V82.tac let sig_it = Refiner.sig_it let project = Refiner.project @@ -73,7 +66,10 @@ let pf_ids_set_of_hyps gls = let pf_get_new_id id gls = next_ident_away id (pf_ids_set_of_hyps gls) -let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) +let pf_global gls id = + 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_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -105,37 +101,23 @@ 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 -(********************************************) -(* Definition of the most primitive tactics *) -(********************************************) - -let refiner = refiner - -let refine_no_check c gl = - let c = EConstr.Unsafe.to_constr c in - refiner (Refine c) gl - -(* Versions with consistency checks *) - -let refine c = with_check (refine_no_check c) - (* Pretty-printers *) open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in - let penv = print_named_context env in - let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in + let penv = Termops.Internal.print_named_context env in + let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () let pr_gls gls = - hov 0 (pr_evar_map (Some 2) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it 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) (sig_sig glls) ++ fnl () ++ + 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 *) @@ -225,4 +207,9 @@ module New = struct 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 index 770d0940a3..ef6a1544e4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,92 +12,78 @@ open Names open Constr open Environ open EConstr -open Proof_type open Redexpr open Locus (** Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Evd.sigma -[@@ocaml.deprecated "alias of Evd.sigma"] - open Evd -type tactic = Proof_type.tactic;; + +type tactic = Proofview.V82.tac val sig_it : 'a sigma -> 'a -val project : goal sigma -> evar_map +val project : Goal.goal sigma -> evar_map val re_sig : 'a -> evar_map -> 'a sigma -val unpackage : 'a sigma -> evar_map ref * 'a -val repackage : evar_map ref -> 'a -> 'a sigma -val apply_sig_tac : - evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list) - -val pf_concl : goal sigma -> types -val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context -(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*) -val pf_hyps_types : goal sigma -> (Id.t * types) list -val pf_nth_hyp_id : goal sigma -> int -> Id.t -val pf_last_hyp : goal sigma -> named_declaration -val pf_ids_of_hyps : goal sigma -> Id.t list -val pf_global : goal sigma -> Id.t -> constr -val pf_unsafe_type_of : goal sigma -> constr -> types -val pf_type_of : goal sigma -> constr -> evar_map * types -val pf_hnf_type_of : goal sigma -> constr -> types +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 sigma -> Id.t -> named_declaration -val pf_get_hyp_typ : goal sigma -> Id.t -> 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 sigma -> Id.t +val pf_get_new_id : Id.t -> Goal.goal sigma -> Id.t -val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr +val pf_reduction_of_red_expr : Goal.goal sigma -> red_expr -> constr -> evar_map * constr -val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a +val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> - goal sigma -> 'a -> goal sigma * 'b + Goal.goal sigma -> 'a -> Goal.goal sigma * 'b val pf_reduce : (env -> evar_map -> constr -> constr) -> - goal sigma -> constr -> constr + Goal.goal sigma -> constr -> constr val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> - goal sigma -> constr -> evar_map * constr - -val pf_whd_all : goal sigma -> constr -> constr -val pf_hnf_constr : goal sigma -> constr -> constr -val pf_nf : goal sigma -> constr -> constr -val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> (inductive * EInstance.t) * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> (inductive * EInstance.t) * types -val pf_compute : goal sigma -> constr -> 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 sigma -> constr -> constr - -val pf_const_value : goal sigma -> pconstant -> constr -val pf_conv_x : goal sigma -> constr -> constr -> bool -val pf_conv_x_leq : goal sigma -> constr -> constr -> bool - -(** {6 The most primitive tactics. } *) + -> Goal.goal sigma -> constr -> constr -val refiner : rule -> tactic -val refine_no_check : constr -> tactic - -(** {6 The most primitive tactics with consistency and type checking } *) - -val refine : constr -> tactic +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 sigma -> Pp.t -val pr_glls : goal list sigma -> Pp.t +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 *) +(** Variants of [Tacmach] functions built with the new proof engine *) module New : sig + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a - val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference + val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t + (** FIXME: encapsulate the level in an existential type. *) - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + 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 @@ -136,4 +122,6 @@ module New : sig 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 |