From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- proofs/clenv.ml | 69 ++- proofs/clenv.mli | 5 +- proofs/clenvtac.ml | 42 +- proofs/clenvtac.mli | 2 + proofs/evar_refiner.ml | 19 +- proofs/evar_refiner.mli | 5 - proofs/goal.ml | 21 +- proofs/goal.mli | 6 +- proofs/logic.ml | 169 ++---- proofs/logic.mli | 7 +- proofs/logic_monad.ml | 321 ----------- proofs/logic_monad.mli | 162 ------ proofs/pfedit.ml | 88 +++- proofs/pfedit.mli | 16 +- proofs/proof.ml | 75 ++- proofs/proof_global.ml | 134 ++--- proofs/proof_global.mli | 19 +- proofs/proof_type.ml | 52 -- proofs/proof_type.mli | 47 +- proofs/proof_using.ml | 10 +- proofs/proof_using.mli | 2 + proofs/proofs.mllib | 7 +- proofs/proofview.ml | 1257 -------------------------------------------- proofs/proofview.mli | 580 -------------------- proofs/proofview_monad.ml | 275 ---------- proofs/proofview_monad.mli | 148 ------ proofs/redexpr.ml | 30 +- proofs/redexpr.mli | 2 + proofs/refine.ml | 162 ++++++ proofs/refine.mli | 50 ++ proofs/refiner.ml | 33 +- proofs/refiner.mli | 5 +- proofs/tacmach.ml | 71 ++- proofs/tacmach.mli | 70 +-- proofs/tactic_debug.ml | 318 ----------- proofs/tactic_debug.mli | 79 --- 36 files changed, 703 insertions(+), 3655 deletions(-) delete mode 100644 proofs/logic_monad.ml delete mode 100644 proofs/logic_monad.mli delete mode 100644 proofs/proof_type.ml delete mode 100644 proofs/proofview.ml delete mode 100644 proofs/proofview.mli delete mode 100644 proofs/proofview_monad.ml delete mode 100644 proofs/proofview_monad.mli create mode 100644 proofs/refine.ml create mode 100644 proofs/refine.mli delete mode 100644 proofs/tactic_debug.ml delete mode 100644 proofs/tactic_debug.mli (limited to 'proofs') diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 88e1bce9..0a90e0db 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -24,6 +24,7 @@ open Pretype_errors open Evarutil open Unification open Misctypes +open Sigma.Notations (* Abbreviations *) @@ -71,7 +72,7 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c exception NotExtensibleClause let clenv_push_prod cl = - let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in + let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in let rec clrec typ = match kind_of_term typ with | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> @@ -108,7 +109,7 @@ let clenv_environments evd bound t = | (n, Cast (t,_,_)) -> clrec (e,metas) n t | (n, Prod (na,t1,t2)) -> let mv = new_meta () in - let dep = dependent (mkRel 1) t2 in + let dep = not (noccurn 1 t2) in let na' = if dep then na else Anonymous in let e' = meta_declare mv t1 ~name:na' e in clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) @@ -119,7 +120,7 @@ let clenv_environments evd bound t = clrec (evd,[]) bound t let mk_clenv_from_env env sigma n (c,cty) = - let evd = create_goal_evar_defs sigma in + let evd = clear_metas sigma in let (evd,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; @@ -335,22 +336,15 @@ let clenv_pose_metas_as_evars clenv dep_mvs = else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in - let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in + let evd = Sigma.Unsafe.of_evar_map clenv.evd in + let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in + let evd = Sigma.to_evar_map evd in let clenv = clenv_assign mv evar {clenv with evd=evd} in fold clenv mvs in fold clenv dep_mvs (******************************************************************) -let connect_clenv gls clenv = - let evd = evars_reset_evd ~with_conv_pbs:true gls.sigma clenv.evd in - { clenv with - evd = evd ; - env = Goal.V82.env evd (sig_it gls) } - -(* let connect_clenv_key = Profile.declare_profile "connect_clenv";; *) -(* let connect_clenv = Profile.profile2 connect_clenv_key connect_clenv *) - (* [clenv_fchain mv clenv clenv'] * * Resolves the value of "mv" (which must be undefined) in clenv to be @@ -432,6 +426,44 @@ let check_bindings bl = str " occurs more than once in binding list.") | [] -> () +let explain_no_such_bound_variable evd id = + let fold l (n, clb) = + let na = match clb with + | Cltyp (na, _) -> na + | Clval (na, _, _) -> na + in + if na != Anonymous then out_name na :: l else l + in + let mvl = List.fold_left fold [] (Evd.meta_list evd) in + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id ++ + (if mvl == [] then str " (no bound variables at all in the expression)." + else + (str" (possible name" ++ + str (if List.length mvl == 1 then " is: " else "s are: ") ++ + pr_enum pr_id mvl ++ str")."))) + +let meta_with_name evd id = + let na = Name id in + let fold (l1, l2 as l) (n, clb) = + let (na',def) = match clb with + | Cltyp (na, _) -> (na, false) + | Clval (na, _, _) -> (na, true) + in + if Name.equal na na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l + in + let (mvl, mvnodef) = List.fold_left fold ([], []) (Evd.meta_list evd) in + match mvnodef, mvl with + | _,[] -> + explain_no_such_bound_variable evd id + | ([n],_|_,[n]) -> + n + | _ -> + errorlabstrm "Evd.meta_with_name" + (str "Binder name \"" ++ pr_id id ++ + strbrk "\" occurs more than once in clause.") + let meta_of_binder clause loc mvs = function | NamedHyp s -> meta_with_name clause.evd s | AnonHyp n -> @@ -459,7 +491,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c @@ -576,7 +609,9 @@ let make_evar_clause env sigma ?len t = | Cast (t, _, _) -> clrec (sigma, holes) 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 + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in + let sigma = Sigma.to_evar_map sigma in let dep = dependent (mkRel 1) t2 in let hole = { hole_evar = ev; @@ -628,7 +663,7 @@ let evar_of_binder holes = function try let h = List.nth holes (pred n) in h.hole_evar - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> errorlabstrm "" (str "No such binder.") let define_with_type sigma env ev c = diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 7ecc26ec..e9236b1d 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** This file defines clausenv, which is a deprecated way to handle open terms + in the proof engine. Most of the API here is legacy except for the + evar-based clauses. *) + open Names open Term open Environ @@ -49,7 +53,6 @@ val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst (** {6 linking of clenvs } *) -val connect_clenv : Goal.goal sigma -> clausenv -> clausenv val clenv_fchain : ?with_univs:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8e922599..98b5bc8b 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -16,7 +16,7 @@ open Logic open Reduction open Tacmach open Clenv - +open Proofview.Notations (* This function put casts around metavariables whose type could not be * infered by the refiner, that is head of applications, predicates and @@ -59,6 +59,19 @@ let clenv_pose_dependent_evars with_evars clenv = (RefinerError (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 = (** ppedrot: a Goal.enter here breaks things, because the tactic below may solve goals by side effects, while the compatibility layer keeps those @@ -67,9 +80,16 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = clenv_pose_dependent_evars with_evars clenv in let evd' = if with_classes then - let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars - ~fail:(not with_evars) clenv.env clenv.evd - in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd' + 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 + ~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' else clenv.evd in let clenv = { clenv with evd = evd' } in @@ -83,10 +103,10 @@ open Unification let dft = default_unify_flags let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let clenv gl = clenv_unique_resolver ~flags clenv gl in clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) - end + end } (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en particulier ne semblent pas vérifier que des instances différentes @@ -118,12 +138,12 @@ let fail_quick_unif_flags = { (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *) let unify ?(flags=fail_quick_unif_flags) m = - Proofview.Goal.enter begin fun gl -> + Proofview.Goal.enter { enter = begin fun gl -> let env = Tacmach.New.pf_env gl in - let n = Tacmach.New.pf_nf_concl gl in - let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in + let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in Proofview.Unsafe.tclEVARSADVANCE evd' - with e when Errors.noncritical e -> Proofview.tclZERO e - end + with e when CErrors.noncritical e -> Proofview.tclZERO e + end } diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 00e74a24..aa091aec 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy components of the previous proof engine. *) + open Term open Clenv open Tacexpr diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 059ae54c..29cad063 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Evd @@ -46,27 +46,16 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let sigma',typed_c = let flags = { Pretyping.use_typeclasses = true; - Pretyping.use_unif_heuristics = 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 evi.evar_concl) rawc - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc (loc,"", str "Instance is not well-typed in the environment of " ++ - str (string_of_existential evk)) + pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) - -(* vernac command Existential *) - -(* Main component of vernac command Existential *) -let instantiate_pf_com evk com sigma = - let evi = Evd.find sigma evk in - let env = Evd.evar_filtered_env evi in - let rawc = Constrintern.intern_constr env com in - let ltac_vars = Pretyping.empty_lvar in - let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in - sigma' diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 35a3e5d8..e3778e94 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -13,8 +13,3 @@ open Pretyping val w_refine : evar * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map - -val instantiate_pf_com : - Evd.evar -> Constrexpr.constr_expr -> Evd.evar_map -> Evd.evar_map - -(** the instantiate tactic was moved to [tactics/evar_tactics.ml] *) diff --git a/proofs/goal.ml b/proofs/goal.ml index 1dd5be0e..111a947a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -9,6 +9,8 @@ open Util open Pp open Term +open Sigma.Notations +open Context.Named.Declaration (* This module implements the abstract interface to goals *) (* A general invariant of the module, is that a goal whose associated @@ -70,10 +72,12 @@ module V82 = struct Evd.evar_extra = extra } in let evi = Typeclasses.mark_unresolvable evi in - let (evars, evk) = Evarutil.new_pure_evar_full evars evi in + let evars = Sigma.Unsafe.of_evar_map evars in + let Sigma (evk, evars, _) = Evarutil.new_pure_evar_full evars evi in + let evars = Sigma.to_evar_map evars in let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in let ctxt = Environ.named_context_of_val hyps in - let inst = Array.map_of_list (fun (id, _, _) -> mkVar id) ctxt in + let inst = Array.map_of_list (mkVar % get_id) ctxt in let ev = Term.mkEvar (evk,inst) in (evk, ev, evars) @@ -89,7 +93,10 @@ module V82 = struct (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = let id = Evd.evar_ident evk sigma in - Evd.rename evk' id (partial_solution sigma evk c) + let sigma = partial_solution sigma evk c in + match id with + | None -> sigma + | Some id -> Evd.rename evk' id sigma (* Parts of the progress tactical *) let same_goal evars1 gl1 evars2 gl2 = @@ -123,8 +130,10 @@ module V82 = struct 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 (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = new_sigma; } + let sigma = Sigma.Unsafe.of_evar_map Evd.empty in + let Sigma (evk, sigma, _) = Evarutil.new_pure_evar_full sigma new_evi in + let sigma = Sigma.to_evar_map sigma in + { Evd.it = evk ; sigma = sigma; } (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = @@ -139,7 +148,7 @@ module V82 = struct let env = env sigma gl in let genv = Global.env () in let is_proof_var decl = - try ignore (Environ.lookup_named (Util.pi1 decl) genv); false + try ignore (Environ.lookup_named (get_id decl) genv); false with Not_found -> true in Environ.fold_named_context_reverse (fun t decl -> if is_proof_var decl then diff --git a/proofs/goal.mli b/proofs/goal.mli index 6152826c..6a79c1f4 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -6,7 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* This module implements the abstract interface to goals *) +(** This module implements the abstract interface to goals. Most of the code + here is useless and should be eventually removed. Consider using + {!Proofview.Goal} instead. *) type goal = Evar.t @@ -67,7 +69,7 @@ module V82 : sig 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_context -> goal Evd.sigma + 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 diff --git a/proofs/logic.ml b/proofs/logic.ml index ed3a1df1..65497c80 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Nameops @@ -22,6 +22,7 @@ open Proof_type open Type_errors open Retyping open Misctypes +open Context.Named.Declaration type refiner_error = @@ -58,7 +59,7 @@ let is_unification_error = function | _ -> false let catchable_exception = function - | Errors.UserError _ | TypeError _ + | CErrors.UserError _ | TypeError _ | RefinerError _ | Indrec.RecursionSchemeError _ | Nametab.GlobalizationError _ (* reduction errors *) @@ -76,10 +77,10 @@ let with_check = Flags.with_option check (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) -let apply_to_hyp sign id f = +let apply_to_hyp check sign id f = try apply_to_hyp sign id f with Hyp_not_found -> - if !check then error_no_such_hypothesis id + if check then error_no_such_hypothesis id else sign let check_typability env sigma c = @@ -95,12 +96,12 @@ let check_typability env sigma c = forces the user to give them in order). *) let clear_hyps env sigma ids sign cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in (hyps, cl, !evdref) let clear_hyps2 env sigma ids sign t cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in + let evdref = ref (Evd.clear_metas sigma) in let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in (hyps, t, cl, !evdref) @@ -160,7 +161,8 @@ let reorder_context env sign ord = | _ -> (match ctxt_head with | [] -> error_no_such_hypothesis (List.hd ord) - | (x,_,_ as d) :: ctxt -> + | d :: ctxt -> + let x = get_id d in if Id.Set.mem x expected then step ord (Id.Set.remove x expected) ctxt (push_item x d moved_hyps) ctxt_tail @@ -175,7 +177,8 @@ let reorder_val_context env sign ord = -let check_decl_position env sign (x,_,_ as d) = +let check_decl_position env sign d = + let x = get_id d in let needed = global_vars_set_of_decl env d in let deps = dependency_closure env (named_context_of_val sign) needed in if Id.List.mem x deps then @@ -200,16 +203,17 @@ let move_location_eq m1 m2 = match m1, m2 with let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h - | (hyp,_,_) :: right -> - if Id.equal hyp h then - match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst + | d :: right -> + if Id.equal (get_id d) h then + match right with d' ::_ -> MoveBefore (get_id d') | [] -> MoveFirst else get_hyp_after h right let split_sign hfrom hto l = let rec splitrec left toleft = function | [] -> error_no_such_hypothesis hfrom - | (hyp,c,typ) as d :: right -> + | d :: right -> + let hyp,_,typ = to_tuple d in if Id.equal hyp hfrom then (left,right,d, toleft || move_location_eq hto MoveLast) else @@ -227,27 +231,28 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = +let move_hyp toleft (left,declfrom,right) hto = let env = Global.env() in - let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) = + let test_dep d d2 = if toleft - then occur_var_in_decl env hyp2 d - else occur_var_in_decl env hyp d2 + then occur_var_in_decl env (get_id d2) d + else occur_var_in_decl env (get_id d) d2 in let rec moverec first middle = function | [] -> if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle - | (hyp,_,_) :: _ as right when move_location_eq hto (MoveBefore hyp) -> + | d :: _ as right when move_location_eq hto (MoveBefore (get_id d)) -> List.rev first @ List.rev middle @ right - | (hyp,_,_) as d :: right -> + | d :: right -> + let hyp = get_id d in let (first',middle') = if List.exists (test_dep d) middle then if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ + errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++ Miscprint.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") @@ -271,6 +276,11 @@ let move_hyp toleft (left,(idfrom,_,_ as declfrom),right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left +let move_hyp_in_named_context hfrom hto sign = + let (left,right,declfrom,toleft) = + split_sign hfrom hto (named_context_of_val sign) in + move_hyp toleft (left,declfrom,right) hto + (**********************************************************************) @@ -458,7 +468,7 @@ and mk_hdgoals sigma goal goalacc trm = and mk_arggoals sigma goal goalacc funty allargs = let foldmap (goalacc, funty, sigma) harg = - let t = whd_betadeltaiota (Goal.V82.env sigma goal) sigma funty in + let t = whd_all (Goal.V82.env sigma goal) sigma funty in let rec collapse t = match kind_of_term t with | LetIn (_, c1, _, b) -> collapse (subst1 c1 b) | _ -> t @@ -483,12 +493,14 @@ and mk_casegoals sigma goal goalacc p c = (acc'',lbrty,conclty,sigma,p',c') -let convert_hyp check sign sigma (id,b,bt as d) = +let convert_hyp check sign sigma d = + let id,b,bt = to_tuple d in let env = Global.env() in let reorder = ref [] in let sign' = - apply_to_hyp sign id - (fun _ (_,c,ct) _ -> + apply_to_hyp check sign id + (fun _ d' _ -> + let _,c,ct = to_tuple d' in let env = Global.env_of_context sign in if check && not (is_conv env sigma bt ct) then errorlabstrm "Logic.convert_hyp" @@ -522,126 +534,23 @@ let prim_refiner r sigma goal = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp false ([],(id,None,t),named_context_of_val sign) + move_hyp false ([], LocalAssum (id,t),named_context_of_val sign) nexthyp, t,cl,sigma else - (if !check && mem_named_context id (named_context_of_val sign) then + (if !check && mem_named_context_val id sign then errorlabstrm "Logic.prim_refiner" (str "Variable " ++ pr_id id ++ str " is already declared."); - push_named_context_val (id,None,t) sign,t,cl,sigma) in + push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in let (sg2,ev2,sigma) = Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in - let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in + let oterm = Term.mkNamedLetIn id ev1 t ev2 in let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma) - | FixRule (f,n,rest,j) -> - let rec check_ind env k cl = - match kind_of_term (strip_outer_cast cl) with - | Prod (na,c1,b) -> - if Int.equal k 1 then - try - fst (find_inductive env sigma c1) - with Not_found -> - error "Cannot do a fixpoint on a non inductive type." - else - check_ind (push_rel (na,None,c1) env) (k-1) b - | _ -> error "Not enough products." - in - let ((sp,_),u) = check_ind env n cl in - let firsts,lasts = List.chop j rest in - let all = firsts@(f,n,cl)::lasts in - let rec mk_sign sign = function - | (f,n,ar)::oth -> - let ((sp',_),u') = check_ind env n ar in - if not (eq_mind sp sp') then - error "Fixpoints should be on the same mutual inductive declaration."; - if !check && mem_named_context f (named_context_of_val sign) then - errorlabstrm "Logic.prim_refiner" - (str "Name " ++ pr_id f ++ str " already used in the environment"); - mk_sign (push_named_context_val (f,None,ar) sign) oth - | [] -> - Evd.Monad.List.map (fun (_,_,c) sigma -> - let gl,ev,sig' = - Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in - (gl,ev),sig') - all sigma - in - let (gls_evs,sigma) = mk_sign sign all in - let (gls,evs) = List.split gls_evs in - let ids = List.map pi1 all in - let evs = List.map (Vars.subst_vars (List.rev ids)) evs in - let indxs = Array.of_list (List.map (fun n -> n-1) (List.map pi2 all)) in - let funnames = Array.of_list (List.map (fun i -> Name i) ids) in - let typarray = Array.of_list (List.map pi3 all) in - let bodies = Array.of_list evs in - let oterm = Term.mkFix ((indxs,0),(funnames,typarray,bodies)) in - let sigma = Goal.V82.partial_solution sigma goal oterm in - (gls,sigma) - - | Cofix (f,others,j) -> - let rec check_is_coind env cl = - let b = whd_betadeltaiota env sigma cl in - match kind_of_term b with - | Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b - | _ -> - try - let _ = find_coinductive env sigma b in () - with Not_found -> - error "All methods must construct elements in coinductive types." - in - let firsts,lasts = List.chop j others in - let all = firsts@(f,cl)::lasts in - List.iter (fun (_,c) -> check_is_coind env c) all; - let rec mk_sign sign = function - | (f,ar)::oth -> - (try - (let _ = lookup_named_val f sign in - error "Name already used in the environment.") - with - | Not_found -> - mk_sign (push_named_context_val (f,None,ar) sign) oth) - | [] -> - Evd.Monad.List.map (fun (_,c) sigma -> - let gl,ev,sigma = - Goal.V82.mk_goal sigma sign c (Goal.V82.extra sigma goal) in - (gl,ev),sigma) - all sigma - in - let (gls_evs,sigma) = mk_sign sign all in - let (gls,evs) = List.split gls_evs in - let (ids,types) = List.split all in - let evs = List.map (Vars.subst_vars (List.rev ids)) evs in - let funnames = Array.of_list (List.map (fun i -> Name i) ids) in - let typarray = Array.of_list types in - let bodies = Array.of_list evs in - let oterm = Term.mkCoFix (0,(funnames,typarray,bodies)) in - let sigma = Goal.V82.partial_solution sigma goal oterm in - (gls,sigma) - | Refine c -> check_meta_variables 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 oterm in (sgl, sigma) - - (* And now the structural rules *) - | Thin ids -> - let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in - let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in - let (gl,ev,sigma) = - Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal) - in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - ([gl], sigma) - - | Move (hfrom, hto) -> - let (left,right,declfrom,toleft) = - split_sign hfrom hto (named_context_of_val sign) in - let hyps' = - move_hyp toleft (left,declfrom,right) hto in - let (gl,ev,sigma) = mk_goal hyps' cl in - let sigma = Goal.V82.partial_solution_to sigma goal gl ev in - ([gl], sigma) diff --git a/proofs/logic.mli b/proofs/logic.mli index ed99d3a3..0dba9ef1 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Names open Term open Evd @@ -53,4 +55,7 @@ exception RefinerError of refiner_error val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> - Context.named_declaration -> Environ.named_context_val + Context.Named.Declaration.t -> Environ.named_context_val + +val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location -> + Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/logic_monad.ml b/proofs/logic_monad.ml deleted file mode 100644 index 68efa71e..00000000 --- a/proofs/logic_monad.ml +++ /dev/null @@ -1,321 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Errors.errorlabstrm "Some timeout function" (Pp.str"Timeout!") - | Exception e -> Errors.print e - | TacticFailure e -> Errors.print e - | _ -> Pervasives.raise Errors.Unhandled -end - -(** {6 Non-logical layer} *) - -(** The non-logical monad is a simple [unit -> 'a] (i/o) monad. The - operations are simple wrappers around corresponding usual - operations and require little documentation. *) -module NonLogical = -struct - - (* The functions in this module follow the pattern that they are - defined with the form [(); fun ()->...]. This is an optimisation - which signals to the compiler that the function is usually partially - applied up to the [();]. Without this annotation, partial - applications can be significantly slower. - - Documentation of this behaviour can be found at: - https://ocaml.janestreet.com/?q=node/30 *) - - include Monad.Make(struct - type 'a t = unit -> 'a - - let return a = (); fun () -> a - let (>>=) a k = (); fun () -> k (a ()) () - let (>>) a k = (); fun () -> a (); k () - let map f a = (); fun () -> f (a ()) - end) - - type 'a ref = 'a Pervasives.ref - - let ignore a = (); fun () -> ignore (a ()) - - let ref a = (); fun () -> Pervasives.ref a - - (** [Pervasives.(:=)] *) - let (:=) r a = (); fun () -> r := a - - (** [Pervasives.(!)] *) - let (!) = fun r -> (); fun () -> ! r - - (** [Pervasives.raise]. Except that exceptions are wrapped with - {!Exception}. *) - let raise ?info = fun e -> (); fun () -> Exninfo.raise ?info (Exception e) - - (** [try ... with ...] but restricted to {!Exception}. *) - let catch = fun s h -> (); - fun () -> try s () - with Exception e as src -> - let (src, info) = Errors.push src in - h (e, info) () - - let read_line = fun () -> try Pervasives.read_line () with e -> - let (e, info) = Errors.push e in raise ~info e () - - let print_char = fun c -> (); fun () -> print_char c - - let timeout = fun n t -> (); fun () -> - Control.timeout n t (Exception Timeout) - - let make f = (); fun () -> - try f () - with e when Errors.noncritical e -> - let (e, info) = Errors.push e in - Util.iraise (Exception e, info) - - (** Use the current logger. The buffer is also flushed. *) - let print_debug s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_info s = make (fun _ -> Pp.msg_info s;Pp.pp_flush ()) - let print_warning s = make (fun _ -> Pp.msg_warning s;Pp.pp_flush ()) - let print_error s = make (fun _ -> Pp.msg_error s;Pp.pp_flush ()) - let print_notice s = make (fun _ -> Pp.msg_notice s;Pp.pp_flush ()) - - let run = fun x -> - try x () with Exception e as src -> - let (src, info) = Errors.push src in - Util.iraise (e, info) -end - -(** {6 Logical layer} *) - -(** The logical monad is a backtracking monad on top of which is - layered a state monad (which is used to implement all of read/write, - read only, and write only effects). The state monad being layered on - top of the backtracking monad makes it so that the state is - backtracked on failure. - - Backtracking differs from regular exception in that, writing (+) - for exception catching and (>>=) for bind, we require the - following extra distributivity laws: - - x+(y+z) = (x+y)+z - - zero+x = x - - x+zero = x - - (x+y)>>=k = (x>>=k)+(y>>=k) *) - -(** A view type for the logical monad, which is a form of list, hence - we can decompose it with as a list. *) -type ('a, 'b) list_view = - | Nil of Exninfo.iexn - | Cons of 'a * 'b - -module type Param = sig - - (** Read only *) - type e - - (** Write only *) - type w - - (** [w] must be a monoid *) - val wunit : w - val wprod : w -> w -> w - - (** Read-write *) - type s - - (** Update-only. Essentially a writer on [u->u]. *) - type u - - (** [u] must be pointed. *) - val uunit : u - -end - - -module Logical (P:Param) = -struct - - (** All three of environment, writer and state are coded as a single - state-passing-style monad.*) - type state = { - rstate : P.e; - ustate : P.u; - wstate : P.w; - sstate : P.s; - } - - (** Double-continuation backtracking monads are reasonable folklore - for "search" implementations (including the Tac interactive - prover's tactics). Yet it's quite hard to wrap your head around - these. I recommand reading a few times the "Backtracking, - Interleaving, and Terminating Monad Transformers" paper by - O. Kiselyov, C. Shan, D. Friedman, and A. Sabry. The peculiar - shape of the monadic type is reminiscent of that of the - continuation monad transformer. - - The paper also contains the rationale for the [split] abstraction. - - An explanation of how to derive such a monad from mathematical - principles can be found in "Kan Extensions for Program - Optimisation" by Ralf Hinze. - - A somewhat concrete view is that the type ['a iolist] is, in fact - the impredicative encoding of the following stream type: - - [type 'a _iolist' = Nil of exn | Cons of 'a*'a iolist' - and 'a iolist = 'a _iolist NonLogical.t] - - Using impredicative encoding avoids intermediate allocation and - is, empirically, very efficient in Ocaml. It also has the - practical benefit that the monadic operation are independent of - the underlying monad, which simplifies the code and side-steps - the limited inlining of Ocaml. - - In that vision, [bind] is simply [concat_map] (though the cps - version is significantly simpler), [plus] is concatenation, and - [split] is pattern-matching. *) - type rich_exn = Exninfo.iexn - - type 'a iolist = - { iolist : 'r. state -> (rich_exn -> 'r NonLogical.t) -> - ('a -> state -> (rich_exn -> 'r NonLogical.t) -> 'r NonLogical.t) -> - 'r NonLogical.t } - - include Monad.Make(struct - - type 'a t = 'a iolist - - let return x = - { iolist = fun s nil cons -> cons x s nil } - - let (>>=) m f = - { iolist = fun s nil cons -> - m.iolist s nil (fun x s next -> (f x).iolist s next cons) } - - let (>>) m f = - { iolist = fun s nil cons -> - m.iolist s nil (fun () s next -> f.iolist s next cons) } - - let map f m = - { iolist = fun s nil cons -> m.iolist s nil (fun x s next -> cons (f x) s next) } - - end) - - let zero e = - { iolist = fun _ nil cons -> nil e } - - let plus m1 m2 = - { iolist = fun s nil cons -> m1.iolist s (fun e -> (m2 e).iolist s nil cons) cons } - - let ignore m = - { iolist = fun s nil cons -> m.iolist s nil (fun _ s next -> cons () s next) } - - let lift m = - { iolist = fun s nil cons -> NonLogical.(m >>= fun x -> cons x s nil) } - - (** State related *) - - let get = - { iolist = fun s nil cons -> cons s.sstate s nil } - - let set (sstate : P.s) = - { iolist = fun s nil cons -> cons () { s with sstate } nil } - - let modify (f : P.s -> P.s) = - { iolist = fun s nil cons -> cons () { s with sstate = f s.sstate } nil } - - let current = - { iolist = fun s nil cons -> cons s.rstate s nil } - - let local e m = - { iolist = fun s nil cons -> - m.iolist { s with rstate = e } nil - (fun x s' next -> cons x {s' with rstate = s.rstate} next) } - - let put w = - { iolist = fun s nil cons -> cons () { s with wstate = P.wprod s.wstate w } nil } - - let update (f : P.u -> P.u) = - { iolist = fun s nil cons -> cons () { s with ustate = f s.ustate } nil } - - (** List observation *) - - let once m = - { iolist = fun s nil cons -> m.iolist s nil (fun x s _ -> cons x s nil) } - - let break f m = - { iolist = fun s nil cons -> - m.iolist s nil (fun x s next -> cons x s (fun e -> match f e with None -> next e | Some e -> nil e)) - } - - (** For [reflect] and [split] see the "Backtracking, Interleaving, - and Terminating Monad Transformers" paper. *) - type 'a reified = ('a, rich_exn -> 'a reified) list_view NonLogical.t - - let rec reflect (m : ('a * state) reified) : 'a iolist = - { iolist = fun s0 nil cons -> - let next = function - | Nil e -> nil e - | Cons ((x, s), l) -> cons x s (fun e -> (reflect (l e)).iolist s0 nil cons) - in - NonLogical.(m >>= next) - } - - let split m : ('a, rich_exn -> 'a t) list_view t = - let rnil e = NonLogical.return (Nil e) in - let rcons p s l = NonLogical.return (Cons ((p, s), l)) in - { iolist = fun s nil cons -> - let open NonLogical in - m.iolist s rnil rcons >>= begin function - | Nil e -> cons (Nil e) s nil - | Cons ((x, s), l) -> - let l e = reflect (l e) in - cons (Cons (x, l)) s nil - end } - - let run m r s = - let s = { wstate = P.wunit; ustate = P.uunit; rstate = r; sstate = s } in - let rnil e = NonLogical.return (Nil e) in - let rcons x s l = - let p = (x, s.sstate, s.wstate, s.ustate) in - NonLogical.return (Cons (p, l)) - in - m.iolist s rnil rcons - - let repr x = x - - end diff --git a/proofs/logic_monad.mli b/proofs/logic_monad.mli deleted file mode 100644 index 96655d53..00000000 --- a/proofs/logic_monad.mli +++ /dev/null @@ -1,162 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a] (i/o) monad. The - operations are simple wrappers around corresponding usual - operations and require little documentation. *) -module NonLogical : sig - - include Monad.S - - val ignore : 'a t -> unit t - - type 'a ref - - val ref : 'a -> 'a ref t - (** [Pervasives.(:=)] *) - val (:=) : 'a ref -> 'a -> unit t - (** [Pervasives.(!)] *) - val (!) : 'a ref -> 'a t - - val read_line : string t - val print_char : char -> unit t - - (** Loggers. The buffer is also flushed. *) - val print_debug : Pp.std_ppcmds -> unit t - val print_warning : Pp.std_ppcmds -> unit t - val print_notice : Pp.std_ppcmds -> unit t - val print_info : Pp.std_ppcmds -> unit t - val print_error : Pp.std_ppcmds -> unit t - - (** [Pervasives.raise]. Except that exceptions are wrapped with - {!Exception}. *) - val raise : ?info:Exninfo.info -> exn -> 'a t - (** [try ... with ...] but restricted to {!Exception}. *) - val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t - val timeout : int -> 'a t -> 'a t - - (** Construct a monadified side-effect. Exceptions raised by the argument are - wrapped with {!Exception}. *) - val make : (unit -> 'a) -> 'a t - - (** [run] performs effects. *) - val run : 'a t -> 'a - -end - - -(** {6 Logical layer} *) - -(** The logical monad is a backtracking monad on top of which is - layered a state monad (which is used to implement all of read/write, - read only, and write only effects). The state monad being layered on - top of the backtracking monad makes it so that the state is - backtracked on failure. - - Backtracking differs from regular exception in that, writing (+) - for exception catching and (>>=) for bind, we require the - following extra distributivity laws: - - x+(y+z) = (x+y)+z - - zero+x = x - - x+zero = x - - (x+y)>>=k = (x>>=k)+(y>>=k) *) - -(** A view type for the logical monad, which is a form of list, hence - we can decompose it with as a list. *) -type ('a, 'b) list_view = -| Nil of Exninfo.iexn -| Cons of 'a * 'b - -(** The monad is parametrised in the types of state, environment and - writer. *) -module type Param = sig - - (** Read only *) - type e - - (** Write only *) - type w - - (** [w] must be a monoid *) - val wunit : w - val wprod : w -> w -> w - - (** Read-write *) - type s - - (** Update-only. Essentially a writer on [u->u]. *) - type u - - (** [u] must be pointed. *) - val uunit : u - -end - -module Logical (P:Param) : sig - - include Monad.S - - val ignore : 'a t -> unit t - - val set : P.s -> unit t - val get : P.s t - val modify : (P.s -> P.s) -> unit t - val put : P.w -> unit t - val current : P.e t - val local : P.e -> 'a t -> 'a t - val update : (P.u -> P.u) -> unit t - - val zero : Exninfo.iexn -> 'a t - val plus : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t - val split : 'a t -> (('a,(Exninfo.iexn->'a t)) list_view) t - val once : 'a t -> 'a t - val break : (Exninfo.iexn -> Exninfo.iexn option) -> 'a t -> 'a t - - val lift : 'a NonLogical.t -> 'a t - - type 'a reified - - val repr : 'a reified -> ('a, Exninfo.iexn -> 'a reified) list_view NonLogical.t - - val run : 'a t -> P.e -> P.s -> ('a * P.s * P.w * P.u) reified - -end diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index b635cc96..eddbf72a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -13,6 +13,17 @@ open Entries open Environ open Evd +let use_unification_heuristics_ref = ref true +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; 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 use_unification_heuristics () = !use_unification_heuristics_ref + let refining = Proof_global.there_are_pending_proofs let check_no_pending_proofs = Proof_global.check_no_pending_proof @@ -39,7 +50,7 @@ let cook_this_proof p = match p with | { Proof_global.id;entries=[constr];persistence;universes } -> (id,(constr,universes,persistence)) - | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") + | _ -> CErrors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") let cook_proof () = cook_this_proof (fst @@ -59,9 +70,9 @@ let get_universe_binders () = Proof_global.get_universe_binders () exception NoSuchGoal -let _ = Errors.register_handler begin function - | NoSuchGoal -> Errors.error "No such goal." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | NoSuchGoal -> CErrors.error "No such goal." + | _ -> raise CErrors.Unhandled end let get_nth_V82_goal i = let p = Proof_global.give_me_the_proof () in @@ -71,26 +82,38 @@ let get_nth_V82_goal i = with Failure _ -> raise NoSuchGoal let get_goal_context_gen i = - try -let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in -(sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) - with Proof_global.NoCurrentProof -> Errors.error "No focused proof." + let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in + (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context i = try get_goal_context_gen i - with NoSuchGoal -> Errors.error "No such goal." + with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + | NoSuchGoal -> CErrors.error "No such goal." let get_current_goal_context () = try get_goal_context_gen 1 - with NoSuchGoal -> + with Proof_global.NoCurrentProof -> CErrors.error "No focused proof." + | NoSuchGoal -> (* spiwack: returning empty evar_map, since if there is no goal, under focus, there is no accessible evar either *) - (Evd.empty, Global.env ()) + let env = Global.env () in + (Evd.from_env env, env) + +let get_current_context () = + try get_goal_context_gen 1 + with Proof_global.NoCurrentProof -> + let env = Global.env () in + (Evd.from_env env, env) + | NoSuchGoal -> + (* No more focused goals ? *) + let p = get_pftreestate () in + let evd = Proof.in_proof p (fun x -> x) in + (evd, Global.env ()) let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl - | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") + | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") let solve ?with_end_tac gi info_lvl tac pr = try @@ -103,24 +126,28 @@ let solve ?with_end_tac gi info_lvl tac pr = 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 - | Vernacexpr.SelectAllParallel -> - Errors.anomaly(str"SelectAllParallel not handled by Stm") + in + let tac = + if use_unification_heuristics () then + Proofview.tclTHEN tac Refine.solve_constraints + else tac in let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in let () = match info_lvl with | None -> () - | Some i -> Pp.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) + | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info ~lvl:i info)) in (p,status) with - | Proof_global.NoCurrentProof -> Errors.error "No focused proof" + | Proof_global.NoCurrentProof -> CErrors.error "No focused proof" | CList.IndexOutOfRange -> match gi with | Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in - Errors.errorlabstrm "" msg + CErrors.errorlabstrm "" msg | _ -> assert false let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac) @@ -138,22 +165,24 @@ 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 - start_proof id goal_kind evd sign typ (fun _ -> ()); + let terminator = Proof_global.make_terminator (fun _ -> ()) in + start_proof id goal_kind evd sign typ terminator; try let status = by tac in let _,(const,univs,_) = cook_proof () in delete_current_proof (); const, status, fst univs with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in - let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in + let ce, status, univs = + build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with @@ -176,7 +205,7 @@ let refine_by_tactic env sigma ty tac = try Proof.run_tactic env tac prf with Logic_monad.TacticFailure e as src -> (** Catch the inner error of the monad tactic *) - let (_, info) = Errors.push src in + let (_, info) = CErrors.push src in iraise (e, info) in (** Plug back the retrieved sigma *) @@ -203,7 +232,7 @@ let refine_by_tactic env sigma ty tac = (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) -let implicit_tactic = ref None +let implicit_tactic = Summary.ref None ~name:"implicit-tactic" let declare_implicit_tactic tac = implicit_tactic := Some tac @@ -214,12 +243,15 @@ let solve_by_implicit_tactic env sigma evk = match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) when - Context.named_context_equal (Environ.named_context_of_val evi.evar_hyps) + Context.Named.equal (Environ.named_context_of_val evi.evar_hyps) (Environ.named_context env) -> - let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) []) in + let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in (try - let (ans, _, _) = - build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in - ans + let c = Evarutil.nf_evars_universes sigma evi.evar_concl 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, ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index cd899201..ea604e08 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Global proof state. A quite redundant wrapper on {!Proof_global}. *) + open Loc open Names open Term @@ -93,6 +95,14 @@ val get_goal_context : int -> Evd.evar_map * env val get_current_goal_context : unit -> Evd.evar_map * env +(** [get_current_context ()] returns the context of the + current focused goal. If there is no focused goal but there + is a proof in progress, it returns the corresponding evar_map. + If there is no pending proof then it returns the current global + environment and empty evar_map. *) + +val get_current_context : unit -> Evd.evar_map * env + (** [current_proof_statement] *) val current_proof_statement : @@ -157,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * + Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> @@ -179,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -(* FIXME: interface: it may incur some new universes etc... *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr diff --git a/proofs/proof.ml b/proofs/proof.ml index 0489305a..5c963d53 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -64,17 +64,17 @@ exception NoSuchGoals of int * int exception FullyUnfocused -let _ = Errors.register_handler begin function +let _ = CErrors.register_handler begin function | CannotUnfocusThisWay -> - Errors.error "This proof is focused, but cannot be unfocused this way" + CErrors.error "This proof is focused, but cannot be unfocused this way" | NoSuchGoals (i,j) when Int.equal i j -> - Errors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").") + CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").") | NoSuchGoals (i,j) -> - Errors.errorlabstrm "Focus" Pp.( + CErrors.errorlabstrm "Focus" Pp.( str"Not every goal in range ["++ int i ++ str","++int j++str"] exist." ) - | FullyUnfocused -> Errors.error "The proof is not focused" - | _ -> raise Errors.Unhandled + | FullyUnfocused -> CErrors.error "The proof is not focused" + | _ -> raise CErrors.Unhandled end let check_cond_kind c k = @@ -300,12 +300,12 @@ exception UnfinishedProof exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar -let _ = Errors.register_handler begin function - | UnfinishedProof -> Errors.error "Some goals have not been solved." - | HasShelvedGoals -> Errors.error "Some goals have been left on the shelf." - | HasGivenUpGoals -> Errors.error "Some goals have been given up." - | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | UnfinishedProof -> CErrors.error "Some goals have not been solved." + | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf." + | HasGivenUpGoals -> CErrors.error "Some goals have been given up." + | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated." + | _ -> raise CErrors.Unhandled end let return p = @@ -334,21 +334,30 @@ let compact p = (*** Tactics ***) let run_tactic env tac pr = + let open Proofview.Notations in let sp = pr.proofview in - let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = + let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in + let tac = + tac >>= fun () -> + Proofview.tclEVARMAP >>= fun sigma -> + (* Already solved goals are not to be counted as shelved. Nor are + they to be marked as unresolvable. *) + let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT retrieved + in + let (retrieved,proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply env tac sp in - let sigma = Proofview.return tacticced_proofview in - (* Already solved goals are not to be counted as shelved. Nor are - they to be marked as unresolvable. *) - let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in - let retrieved = undef (List.rev (Evd.future_goals sigma)) in - let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in + let sigma = Proofview.return proofview in + let to_shelve = undef sigma to_shelve in + let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in let proofview = List.fold_left - Proofview.Unsafe.mark_as_goal - tacticced_proofview - retrieved + Proofview.Unsafe.mark_as_unresolvable + proofview + to_shelve in let given_up = pr.given_up@give_up in let proofview = Proofview.Unsafe.reset_future_goals proofview in @@ -387,9 +396,27 @@ module V82 = struct { p with proofview = Proofview.V82.grab p.proofview } + (* Main component of vernac command Existential *) let instantiate_evar n com pr = - let sp = pr.proofview in - let proofview = Proofview.V82.instantiate_evar n com sp in + let tac = + Proofview.tclBIND Proofview.tclEVARMAP begin fun sigma -> + let (evk, evi) = + let evl = Evarutil.non_instantiated sigma in + let evl = Evar.Map.bindings evl in + if (n <= 0) then + CErrors.error "incorrect existential variable index" + else if CList.length evl < n then + CErrors.error "not so many uninstantiated existential variables" + else + CList.nth evl (n-1) + in + let env = Evd.evar_filtered_env evi in + let rawc = Constrintern.intern_constr env com in + let ltac_vars = Pretyping.empty_lvar in + let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in + Proofview.Unsafe.tclEVARS sigma + end in + let ((), proofview, _, _) = Proofview.apply (Global.env ()) tac pr.proofview in let shelf = List.filter begin fun g -> Evd.is_undefined (Proofview.return proofview) g diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f22cdbcc..e753e972 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -23,8 +23,9 @@ open Names (* Type of proof modes : - A function [set] to set it *from standard mode* - A function [reset] to reset the *standard mode* from it *) +type proof_mode_name = string type proof_mode = { - name : string ; + name : proof_mode_name ; set : unit -> unit ; reset : unit -> unit } @@ -33,10 +34,10 @@ let proof_modes = Hashtbl.create 6 let find_proof_mode n = try Hashtbl.find proof_modes n with Not_found -> - Errors.error (Format.sprintf "No proof mode named \"%s\"." n) + CErrors.error (Format.sprintf "No proof mode named \"%s\"." n) let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (Ephemeron.create m) + Hashtbl.add proof_modes n (CEphemeron.create m) (* initial mode: standard mode *) let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } @@ -45,6 +46,9 @@ let _ = register_proof_mode standard (* Default proof mode, to be set at the beginning of proofs. *) let default_proof_mode = ref (find_proof_mode "No") +let get_default_proof_mode_name () = + (CEphemeron.default !default_proof_mode standard).name + let _ = Goptions.declare_string_option {Goptions. optsync = true ; @@ -52,7 +56,7 @@ let _ = optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; optread = begin fun () -> - (Ephemeron.default !default_proof_mode standard).name + (CEphemeron.default !default_proof_mode standard).name end; optwrite = begin fun n -> default_proof_mode := find_proof_mode n @@ -83,15 +87,18 @@ type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; - terminator : proof_terminator Ephemeron.key; + terminator : proof_terminator CEphemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; - mode : proof_mode Ephemeron.key; + mode : proof_mode CEphemeron.key; universe_binders: universe_binders option; } +let make_terminator f = f +let apply_terminator f = f + (* The head of [!pstates] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) @@ -103,11 +110,11 @@ let current_proof_mode = ref !default_proof_mode let update_proof_mode () = match !pstates with | { mode = m } :: _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := m; - Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ()) + CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) | _ -> - Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); current_proof_mode := find_proof_mode "No" (* combinators for the current_proof lists *) @@ -115,15 +122,15 @@ let push a l = l := a::!l; update_proof_mode () exception NoSuchProof -let _ = Errors.register_handler begin function - | NoSuchProof -> Errors.error "No such proof." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | NoSuchProof -> CErrors.error "No such proof." + | _ -> raise CErrors.Unhandled end exception NoCurrentProof -let _ = Errors.register_handler begin function - | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)." - | _ -> raise Errors.Unhandled +let _ = CErrors.register_handler begin function + | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)." + | _ -> raise CErrors.Unhandled end (*** Proof Global manipulation ***) @@ -183,7 +190,7 @@ let check_no_pending_proof () = if not (there_are_pending_proofs ()) then () else begin - Errors.error (Pp.string_of_ppcmds + CErrors.error (Pp.string_of_ppcmds (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++ str"Use \"Abort All\" first or complete proof(s).")) end @@ -195,7 +202,7 @@ let discard (loc,id) = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then - Errors.user_err_loc + CErrors.user_err_loc (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ()) let discard_current () = @@ -215,9 +222,9 @@ let set_proof_mode mn = set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) let activate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_proof_mode mode = - Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ()) + CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) +let disactivate_current_proof_mode () = + CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) (** [start_proof sigma id str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and @@ -230,7 +237,7 @@ let disactivate_proof_mode mode = let start_proof sigma id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.start sigma goals; endline_tactic = None; section_vars = None; @@ -242,7 +249,7 @@ let start_proof sigma id ?pl str goals terminator = let start_dependent_proof id ?pl str goals terminator = let initial_state = { pid = id; - terminator = Ephemeron.create terminator; + terminator = CEphemeron.create terminator; proof = Proof.dependent_start goals; endline_tactic = None; section_vars = None; @@ -264,18 +271,19 @@ let _ = Goptions.declare_bool_option Goptions.optwrite = (fun b -> proof_using_auto_clear := b) } let set_used_variables l = + let open Context.Named.Declaration in let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in let ctx = Environ.keep_hyps env ids in let ctx_set = - List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in + List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in let aux env entry (ctx, all_safe, to_clear as orig) = match entry with - | (x,None,_) -> + | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig else (ctx, all_safe, (Loc.ghost,x)::to_clear) - | (x,Some bo, ty) as decl -> + | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe @@ -288,7 +296,7 @@ let set_used_variables l = | [] -> raise NoCurrentProof | p :: rest -> if not (Option.is_empty p.section_vars) then - Errors.error "Used section variables can be declared only once"; + CErrors.error "Used section variables can be declared only once"; pstates := { p with section_vars = Some ctx} :: rest; ctx, to_clear @@ -299,6 +307,11 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf +let constrain_variables init uctx = + let levels = Univ.Instance.levels (Univ.UContext.instance init) in + let cstrs = UState.constrain_variables levels uctx in + Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) + let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in @@ -329,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* For vi2vo compilation proofs are computed now but we need to * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) @@ -338,7 +351,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in - let ctx = Evd.evar_universe_context_set initunivs universes in + let ctx = constrain_variables initunivs universes in (* Since the proof is computed now, we can simply have 1 set of * constraints in which we merge the ones for the body and the ones * for the typ *) @@ -353,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let initunivs = Evd.evar_context_universe_context initial_euctx in Future.from_val (initunivs, nf t), Future.chain ~pure:true p (fun (pt,eff) -> - (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff) + (pt,constrain_variables initunivs (Future.force univs)),eff) in let entries = Future.map2 (fun p (_, t) -> @@ -375,7 +388,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = in { id = pid; entries = entries; persistence = strength; universes = (universes, binders) }, - fun pr_ending -> Ephemeron.get terminator pr_ending + fun pr_ending -> CEphemeron.get terminator pr_ending type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context @@ -395,7 +408,7 @@ let return_proof ?(allow_partial=false) () = let evd = let error s = let prf = str " (in proof " ++ Id.print pid ++ str ")" in - raise (Errors.UserError("last tactic before Qed",s ++ prf)) + raise (CErrors.UserError("last tactic before Qed",s ++ prf)) in try Proof.return proof with | Proof.UnfinishedProof -> @@ -423,11 +436,11 @@ let close_proof ~keep_body_ucst_separate fix_exn = (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator +let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator let set_terminator hook = match !pstates with | [] -> raise NoCurrentProof - | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps + | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps @@ -458,7 +471,7 @@ module Bullet = struct type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> std_ppcmds } let behaviors = Hashtbl.create 4 @@ -468,7 +481,7 @@ module Bullet = struct let none = { name = "None"; put = (fun x _ -> x); - suggest = (fun _ -> None) + suggest = (fun _ -> mt ()) } let _ = register_behavior none @@ -484,36 +497,30 @@ module Bullet = struct (* give a message only if more informative than the standard coq message *) let suggest_on_solved_goal sugg = match sugg with - | NeedClosingBrace -> Some "Try unfocusing with \"}\"." - | NoBulletInUse -> None - | ProofFinished -> None - | Suggest b -> Some ("Focus next goal with bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^".") - | Unfinished b -> Some ("The current bullet " - ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is unfinished.") + | NeedClosingBrace -> str"Try unfocusing with \"}\"." + | NoBulletInUse -> mt () + | ProofFinished -> mt () + | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"." + | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished." (* give always a message. *) let suggest_on_error sugg = match sugg with - | NeedClosingBrace -> "Try unfocusing with \"}\"." + | NeedClosingBrace -> str"Try unfocusing with \"}\"." | NoBulletInUse -> assert false (* This should never raise an error. *) - | ProofFinished -> "No more subgoals." - | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is mandatory here.") - | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) - ^ " is not finished.") + | ProofFinished -> str"No more subgoals." + | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here." + | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished." exception FailedBullet of t * suggestion let _ = - Errors.register_handler + CErrors.register_handler (function | FailedBullet (b,sugg) -> - let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in - Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg)) - | _ -> raise Errors.Unhandled) + let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in + CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg) + | _ -> raise CErrors.Unhandled) (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *) @@ -610,7 +617,7 @@ module Bullet = struct let _ = register_behavior strict end - (* Current bullet behavior, controled by the option *) + (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict let _ = @@ -626,7 +633,7 @@ module Bullet = struct current_behavior := try Hashtbl.find behaviors n with Not_found -> - Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") + CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") end } @@ -657,21 +664,26 @@ let _ = let default_goal_selector = ref (Vernacexpr.SelectNth 1) let get_default_goal_selector () = !default_goal_selector +let print_range_selector (i, j) = + if i = j then string_of_int i + else string_of_int i ^ "-" ^ string_of_int j + let print_goal_selector = function | Vernacexpr.SelectAll -> "all" | Vernacexpr.SelectNth i -> string_of_int i + | Vernacexpr.SelectList l -> "[" ^ + String.concat ", " (List.map print_range_selector l) ^ "]" | Vernacexpr.SelectId id -> Id.to_string id - | Vernacexpr.SelectAllParallel -> "par" let parse_goal_selector = function | "all" -> Vernacexpr.SelectAll | i -> - let err_msg = "A selector must be \"all\" or a natural number." in + 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 Errors.error err_msg; + if i < 0 then CErrors.error err_msg; Vernacexpr.SelectNth i - with Failure _ -> Errors.error err_msg + with Failure _ -> CErrors.error err_msg end let _ = @@ -700,7 +712,7 @@ type state = pstate list let freeze ~marshallable = match marshallable with | `Yes -> - Errors.anomaly (Pp.str"full marshalling of proof state not supported") + CErrors.anomaly (Pp.str"full marshalling of proof state not supported") | `Shallow -> !pstates | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 7fbd183e..59daa296 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -16,8 +16,9 @@ - A function [reset] to reset the *standard mode* from it *) +type proof_mode_name = string type proof_mode = { - name : string ; + name : proof_mode_name ; set : unit -> unit ; reset : unit -> unit } @@ -27,6 +28,7 @@ type proof_mode = { One mode is already registered - the standard mode - named "No", It corresponds to Coq default setting are they are set when coqtop starts. *) val register_proof_mode : proof_mode -> unit +val get_default_proof_mode_name : unit -> proof_mode_name val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -40,7 +42,7 @@ val discard_all : unit -> unit (** [set_proof_mode] sets the proof mode to be used after it's called. It is typically called by the Proof Mode command. *) -val set_proof_mode : string -> unit +val set_proof_mode : proof_mode_name -> unit exception NoCurrentProof val give_me_the_proof : unit -> Proof.proof @@ -70,9 +72,12 @@ type proof_ending = | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object -type proof_terminator = proof_ending -> unit +type proof_terminator type closed_proof = proof_object * proof_terminator +val make_terminator : (proof_ending -> unit) -> proof_terminator +val apply_terminator : proof_terminator -> proof_ending -> unit + (** [start_proof id str 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 @@ -150,8 +155,8 @@ val get_universe_binders : unit -> universe_binders option (**********************************************************) -val activate_proof_mode : string -> unit -val disactivate_proof_mode : string -> unit +val activate_proof_mode : proof_mode_name -> unit +val disactivate_current_proof_mode : unit -> unit (**********************************************************) (* *) @@ -169,7 +174,7 @@ module Bullet : sig type behavior = { name : string; put : Proof.proof -> t -> Proof.proof; - suggest: Proof.proof -> string option + suggest: Proof.proof -> Pp.std_ppcmds } (** A registered behavior can then be accessed in Coq @@ -186,7 +191,7 @@ module Bullet : sig (** Handles focusing/defocusing with bullets: *) val put : Proof.proof -> t -> Proof.proof - val suggest : Proof.proof -> string option + val suggest : Proof.proof -> Pp.std_ppcmds end diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml deleted file mode 100644 index dd2c7b25..00000000 --- a/proofs/proof_type.ml +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* goal list sigma - -type prim_rule = - | Cut of bool * bool * Id.t * types - | FixRule of Id.t * int * (Id.t * int * constr) list * int - | Cofix of Id.t * (Id.t * constr) list * int - | Refine of constr - | Thin of Id.t list - | Move of Id.t * Id.t move_location - -(** Nowadays, the only rules we'll consider are the primitive rules *) - -type rule = prim_rule - -(** Ltac traces *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index aa05f58a..c1207962 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Legacy proof engine. Do not use in newly written code. *) + open Evd open Names open Term @@ -19,57 +21,12 @@ open Misctypes type prim_rule = | Cut of bool * bool * Id.t * types - | FixRule of Id.t * int * (Id.t * int * constr) list * int - | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr - | Thin of Id.t list - | Move of Id.t * Id.t move_location (** Nowadays, the only rules we'll consider are the primitive rules *) type rule = prim_rule -(** The type [goal sigma] is the type of subgoal. It has the following form -{v it = \{ evar_concl = [the conclusion of the subgoal] - evar_hyps = [the hypotheses of the subgoal] - evar_body = Evar_Empty; - evar_info = \{ pgm : [The Realizer pgm if any] - lc : [Set of evar num occurring in subgoal] \}\} - sigma = \{ stamp = [an int chardacterizing the ed field, for quick compare] - ed : [A set of existential variables depending in the subgoal] - number of first evar, - it = \{ evar_concl = [the type of first evar] - evar_hyps = [the context of the evar] - evar_body = [the body of the Evar if any] - evar_info = \{ pgm : [Useless ??] - lc : [Set of evars occurring - in the type of evar] \} \}; - ... - number of last evar, - it = \{ evar_concl = [the type of evar] - evar_hyps = [the context of the evar] - evar_body = [the body of the Evar if any] - evar_info = \{ pgm : [Useless ??] - lc : [Set of evars occurring - in the type of evar] \} \} \} v} -*) - type goal = Goal.goal type tactic = goal sigma -> goal list sigma - -(** Ltac traces *) - -(** TODO: Move those definitions somewhere sensible *) - -type ltac_call_kind = - | LtacMLCall of glob_tactic_expr - | LtacNotationCall of KerName.t - | LtacNameCall of ltac_constant - | LtacAtomCall of glob_atomic_tactic_expr - | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of glob_constr * Pretyping.ltac_var_map - -type ltac_trace = (Loc.t * ltac_call_kind) list - -val ltac_trace_info : ltac_trace Exninfo.t diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a69645b1..caa9b328 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -10,6 +10,7 @@ open Names open Environ open Util open Vernacexpr +open Context.Named.Declaration let to_string e = let rec aux = function @@ -33,7 +34,8 @@ let in_nameset = let rec close_fwd e s = let s' = - List.fold_left (fun s (id,b,ty) -> + List.fold_left (fun s decl -> + let (id,b,ty) = Context.Named.Declaration.to_tuple decl in let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in let vty = global_vars_set e ty in let vbty = Id.Set.union vb vty in @@ -61,13 +63,13 @@ and set_of_id env ty id = Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty else if CList.mem_assoc_f Id.equal id !known_names then process_expr env (CList.assoc_f Id.equal id !known_names) [] else Id.Set.singleton id and full_set env = - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in @@ -126,7 +128,7 @@ let suggest_Proof_using name env vars ids_typ context_ids = if S.equal all_needed fwd_typ then valid (str "Type*"); if S.equal all all_needed then valid(str "All"); valid (pr_set false needed); - msg_info ( + Feedback.msg_info ( str"The proof of "++ str name ++ spc() ++ str "should start with one of the following commands:"++spc()++ v 0 ( diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli index 1bf38b69..b2c65412 100644 --- a/proofs/proof_using.mli +++ b/proofs/proof_using.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Utility code for section variables handling in Proof using... *) + val process_expr : Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> Names.Id.t list diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 32bf5576..804a5436 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,18 +2,13 @@ Miscprint Goal Evar_refiner Proof_using -Proof_type -Proof_errors -Logic_monad -Proofview_monad Logic -Proofview +Refine Proof Proof_global Redexpr Refiner Tacmach Pfedit -Tactic_debug Clenv Clenvtac diff --git a/proofs/proofview.ml b/proofs/proofview.ml deleted file mode 100644 index a6d9735f..00000000 --- a/proofs/proofview.ml +++ /dev/null @@ -1,1257 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* i+1) solution 0 in - let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in - let pruned_solution = Evd.drop_all_defined solution in - let apply_subst_einfo _ ei = - Evd.({ ei with - evar_concl = nf ei.evar_concl; - evar_hyps = Environ.map_named_val nf ei.evar_hyps; - evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in - let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in - let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in - msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size)); - new_el, { pv with solution = new_solution; } - - -(** {6 Starting and querying a proof view} *) - -type telescope = - | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) - -let dependent_init = - (* Goals are created with a store which marks them as unresolvable - for type classes. *) - let store = Typeclasses.set_resolvable Evd.Store.empty false in - (* Goals don't have a source location. *) - let src = (Loc.ghost,Evar_kinds.GoalEvar) in - (* Main routine *) - let rec aux = function - | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } - | TCons (env, sigma, typ, t) -> - let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in - let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in - let (gl, _) = Term.destEvar econstr in - let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = gl :: comb; shelf = [] } - in - fun t -> - let entry, v = aux t in - (* The created goal are not to be shelved. *) - let solution = Evd.reset_future_goals v.solution in - entry, { v with solution } - -let init = - let rec aux sigma = function - | [] -> TNil sigma - | (env,g)::l -> TCons (env,sigma,g,(fun sigma _ -> aux sigma l)) - in - fun sigma l -> dependent_init (aux sigma l) - -let initial_goals initial = initial - -let finished = function - | {comb = []} -> true - | _ -> false - -let return { solution=defs } = defs - -let return_constr { solution = defs } c = Evarutil.nf_evar defs c - -let partial_proof entry pv = CList.map (return_constr pv) (CList.map fst entry) - - -(** {6 Focusing commands} *) - -(** A [focus_context] represents the part of the proof view which has - been removed by a focusing action, it can be used to unfocus later - on. *) -(* First component is a reverse list of the goals which come before - and second component is the list of the goals which go after (in - the expected order). *) -type focus_context = Evar.t list * Evar.t list - - -(** Returns a stylised view of a focus_context for use by, for - instance, ide-s. *) -(* spiwack: the type of [focus_context] will change as we push more - refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) -(* In this version: the goals in the context, as a "zipper" (the first - list is in reversed order). *) -let focus_context f = f - -(** This (internal) function extracts a sublist between two indices, - and returns this sublist together with its context: if it returns - [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the - original list. The focused list has lenght [j-i-1] and contains - the goals from number [i] to number [j] (both included) the first - goal of the list being numbered [1]. [focus_sublist i j l] raises - [IndexOutOfRange] if [i > length l], or [j > length l] or [j < - i]. *) -let focus_sublist i j l = - let (left,sub_right) = CList.goto (i-1) l in - let (sub, right) = - try CList.chop (j-i+1) sub_right - with Failure _ -> raise CList.IndexOutOfRange - in - (sub, (left,right)) - -(** Inverse operation to the previous one. *) -let unfocus_sublist (left,right) s = - CList.rev_append left (s@right) - - -(** [focus i j] focuses a proofview on the goals from index [i] to - index [j] (inclusive, goals are indexed from [1]). I.e. goals - number [i] to [j] become the only focused goals of the returned - proofview. It returns the focused proofview, and a context for - the focus stack. *) -let focus i j sp = - let (new_comb, context) = focus_sublist i j sp.comb in - ( { sp with comb = new_comb } , context ) - - -(** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) -(* spiwack: [advance] is probably performance critical, and the good - behaviour of its definition may depend sensitively to the actual - definition of [Evd.find]. Currently, [Evd.find] starts looking for - a value in the heap of undefined variable, which is small. Hence in - the most common case, where [advance] is applied to an unsolved - goal ([advance] is used to figure if a side effect has modified the - goal) it terminates quickly. *) -let rec advance sigma g = - let open Evd in - let evi = Evd.find sigma g in - match evi.evar_body with - | Evar_empty -> Some g - | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then - let (e,_) = Term.destEvar v in - advance sigma e - else - None - -(** [undefined defs l] is the list of goals in [l] which are still - unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (advance defs) l - -(** Unfocuses a proofview with respect to a context. *) -let unfocus c sp = - { sp with comb = undefined sp.solution (unfocus_sublist c sp.comb) } - - -(** {6 The tactic monad} *) - -(** - Tactics are objects which apply a transformation to all the - subgoals of the current view at the same time. By opposition to - the old vision of applying it to a single goal. It allows tactics - such as [shelve_unifiable], tactics to reorder the focused goals, - or global automation tactic for dependent subgoals (instantiating - an evar has influences on the other goals of the proof in - progress, not being able to take that into account causes the - current eauto tactic to fail on some instances where it could - succeed). Another benefit is that it is possible to write tactics - that can be executed even if there are no focused goals. - - Tactics form a monad ['a tactic], in a sense a tactic can be - seen as a function (without argument) which returns a value of - type 'a and modifies the environment (in our case: the view). - Tactics of course have arguments, but these are given at the - meta-level as OCaml functions. Most tactics in the sense we are - used to return [()], that is no really interesting values. But - some might pass information around. The tactics seen in Coq's - Ltac are (for now at least) only [unit tactic], the return values - are kept for the OCaml toolkit. The operation or the monad are - [Proofview.tclUNIT] (which is the "return" of the tactic monad) - [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN] - (which is a specialized bind on unit-returning tactics). - - Tactics have support for full-backtracking. Tactics can be seen - having multiple success: if after returning the first success a - failure is encountered, the tactic can backtrack and use a second - success if available. The state is backtracked to its previous - value, except the non-logical state defined in the {!NonLogical} - module below. -*) -(* spiwack: as far as I'm aware this doesn't really relate to - F. Kirchner and C. Muñoz. *) - -module Proof = Logical - -(** type of tactics: - - tactics can - - access the environment, - - report unsafe status, shelved goals and given up goals - - access and change the current [proofview] - - backtrack on previous changes of the proofview *) -type +'a tactic = 'a Proof.t - -(** Applies a tactic to the current proofview. *) -let apply env t sp = - let open Logic_monad in - let ans = Proof.repr (Proof.run t false (sp,env)) in - let ans = Logic_monad.NonLogical.run ans in - match ans with - | Nil (e, info) -> iraise (TacticFailure e, info) - | Cons ((r, (state, _), status, info), _) -> - let (status, gaveup) = status in - let status = (status, state.shelf, gaveup) in - let state = { state with shelf = [] } in - r, state, status, Trace.to_tree info - - - -(** {7 Monadic primitives} *) - -(** Unit of the tactic monad. *) -let tclUNIT = Proof.return - -(** Bind operation of the tactic monad. *) -let tclBIND = Proof.(>>=) - -(** Interpretes the ";" (semicolon) of Ltac. As a monadic operation, - it's a specialized "bind". *) -let tclTHEN = Proof.(>>) - -(** [tclIGNORE t] has the same operational content as [t], but drops - the returned value. *) -let tclIGNORE = Proof.ignore - -module Monad = Proof - - - -(** {7 Failure and backtracking} *) - - -(** [tclZERO e] fails with exception [e]. It has no success. *) -let tclZERO ?info e = - let info = match info with - | None -> Exninfo.null - | Some info -> info - in - Proof.zero (e, info) - -(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever - the successes of [t1] have been depleted and it failed with [e], - then it behaves as [t2 e]. In other words, [tclOR] inserts a - backtracking point. *) -let tclOR = Proof.plus - -(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one - success or [t2 e] if [t1] fails with [e]. It is analogous to - [try/with] handler of exception in that it is not a backtracking - point. *) -let tclORELSE t1 t2 = - let open Logic_monad in - let open Proof in - split t1 >>= function - | Nil e -> t2 e - | Cons (a,t1') -> plus (return a) t1' - -(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] - succeeds at least once then it behaves as [tclBIND a s] otherwise, - if [a] fails with [e], then it behaves as [f e]. *) -let tclIFCATCH a s f = - let open Logic_monad in - let open Proof in - split a >>= function - | Nil e -> f e - | Cons (x,a') -> plus (s x) (fun e -> (a' e) >>= fun x' -> (s x')) - -(** [tclONCE t] behave like [t] except it has at most one success: - [tclONCE t] stops after the first success of [t]. If [t] fails - with [e], [tclONCE t] also fails with [e]. *) -let tclONCE = Proof.once - -exception MoreThanOneSuccess -let _ = Errors.register_handler begin function - | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." - | _ -> raise Errors.Unhandled -end - -(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one - success. Otherwise it fails. The tactic [t] is run until its first - success, then a failure with exception [e] is simulated. It [t] - yields another success, then [tclEXACTLY_ONCE e t] fails with - [MoreThanOneSuccess] (it is a user error). Otherwise, - [tclEXACTLY_ONCE e t] succeeds with the first success of - [t]. Notice that the choice of [e] is relevant, as the presence of - further successes may depend on [e] (see {!tclOR}). *) -let tclEXACTLY_ONCE e t = - let open Logic_monad in - let open Proof in - split t >>= function - | Nil (e, info) -> tclZERO ~info e - | Cons (x,k) -> - Proof.split (k (e, Exninfo.null)) >>= function - | Nil _ -> tclUNIT x - | _ -> tclZERO MoreThanOneSuccess - - -(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *) -type 'a case = -| Fail of iexn -| Next of 'a * (iexn -> 'a tactic) -let tclCASE t = - let open Logic_monad in - let map = function - | Nil e -> Fail e - | Cons (x, t) -> Next (x, t) - in - Proof.map map (Proof.split t) - -let tclBREAK = Proof.break - - - -(** {7 Focusing tactics} *) - -exception NoSuchGoals of int - -(* This hook returns a string to be appended to the usual message. - Primarily used to add a suggestion about the right bullet to use to - focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> string option) ref = ref ((fun n -> None)) -let set_nosuchgoals_hook f = nosuchgoals_hook := f - - - -(* This uses the hook above *) -let _ = Errors.register_handler begin function - | NoSuchGoals n -> - let suffix:string option = (!nosuchgoals_hook) n in - Errors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." - ++ pr_opt str suffix) - | _ -> raise Errors.Unhandled -end - -(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where - only the goals numbered [i] to [j] are focused (the rest of the goals - is restored at the end of the tactic). If the range [i]-[j] is not - valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *) -let tclFOCUS_gen nosuchgoal i j t = - let open Proof in - Pv.get >>= fun initial -> - try - let (focused,context) = focus i j initial in - Pv.set focused >> - t >>= fun result -> - Pv.modify (fun next -> unfocus context next) >> - return result - with CList.IndexOutOfRange -> nosuchgoal - -let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t -let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t - -(** Like {!tclFOCUS} but selects a single goal by name. *) -let tclFOCUSID id t = - let open Proof in - Pv.get >>= fun initial -> - try - let ev = Evd.evar_key id initial.solution in - try - let n = CList.index Evar.equal ev initial.comb in - (* goal is already under focus *) - let (focused,context) = focus n n initial in - Pv.set focused >> - t >>= fun result -> - Pv.modify (fun next -> unfocus context next) >> - return result - with Not_found -> - (* otherwise, save current focus and work purely on the shelve *) - Comb.set [ev] >> - t >>= fun result -> - Comb.set initial.comb >> - return result - with Not_found -> tclZERO (NoSuchGoals 1) - -(** {7 Dispatching on goals} *) - -exception SizeMismatch of int*int -let _ = Errors.register_handler begin function - | SizeMismatch (i,_) -> - let open Pp in - let errmsg = - str"Incorrect number of goals" ++ spc() ++ - str"(expected "++int i++str(String.plural i " tactic") ++ str")." - in - Errors.errorlabstrm "" errmsg - | _ -> raise Errors.Unhandled -end - -(** A variant of [Monad.List.iter] where we iter over the focused list - of goals. The argument tactic is executed in a focus comprising - only of the current goal, a goal which has been solved by side - effect is skipped. The generated subgoals are concatenated in - order. *) -let iter_goal i = - let open Proof in - Comb.get >>= fun initial -> - Proof.List.fold_left begin fun (subgoals as cur) goal -> - Solution.get >>= fun step -> - match advance step goal with - | None -> return cur - | Some goal -> - Comb.set [goal] >> - i goal >> - Proof.map (fun comb -> comb :: subgoals) Comb.get - end [] initial >>= fun subgoals -> - Solution.get >>= fun evd -> - Comb.set CList.(undefined evd (flatten (rev subgoals))) - -(** A variant of [Monad.List.fold_left2] where the first list is the - list of focused goals. The argument tactic is executed in a focus - comprising only of the current goal, a goal which has been solved - by side effect is skipped. The generated subgoals are concatenated - in order. *) -let fold_left2_goal i s l = - let open Proof in - Pv.get >>= fun initial -> - let err = - return () >>= fun () -> (* Delay the computation of list lengths. *) - tclZERO (SizeMismatch (CList.length initial.comb,CList.length l)) - in - Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> - Solution.get >>= fun step -> - match advance step goal with - | None -> return cur - | Some goal -> - Comb.set [goal] >> - i goal a r >>= fun r -> - Proof.map (fun comb -> (r, comb :: subgoals)) Comb.get - end (s,[]) initial.comb l >>= fun (r,subgoals) -> - Solution.get >>= fun evd -> - Comb.set CList.(undefined evd (flatten (rev subgoals))) >> - return r - -(** Dispatch tacticals are used to apply a different tactic to each - goal under focus. They come in two flavours: [tclDISPATCH] takes a - list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL] - takes a list of ['a tactic] and returns an ['a list tactic]. - - They both work by applying each of the tactic in a focus - restricted to the corresponding goal (starting with the first - goal). In the case of [tclDISPATCHL], the tactic returns a list of - the same size as the argument list (of tactics), each element - being the result of the tactic executed in the corresponding goal. - - When the length of the tactic list is not the number of goal, - raises [SizeMismatch (g,t)] where [g] is the number of available - goals, and [t] the number of tactics passed. - - [tclDISPATCHGEN join tacs] generalises both functions as the - successive results of [tacs] are stored in reverse order in a - list, and [join] is used to convert the result into the expected - form. *) -let tclDISPATCHGEN0 join tacs = - match tacs with - | [] -> - begin - let open Proof in - Comb.get >>= function - | [] -> tclUNIT (join []) - | comb -> tclZERO (SizeMismatch (CList.length comb,0)) - end - | [tac] -> - begin - let open Proof in - Pv.get >>= function - | { comb=[goal] ; solution } -> - begin match advance solution goal with - | None -> tclUNIT (join []) - | Some _ -> Proof.map (fun res -> join [res]) tac - end - | {comb} -> tclZERO (SizeMismatch(CList.length comb,1)) - end - | _ -> - let iter _ t cur = Proof.map (fun y -> y :: cur) t in - let ans = fold_left2_goal iter [] tacs in - Proof.map join ans - -let tclDISPATCHGEN join tacs = - let branch t = InfoL.tag (Info.DBranch) t in - let tacs = CList.map branch tacs in - InfoL.tag (Info.Dispatch) (tclDISPATCHGEN0 join tacs) - -let tclDISPATCH tacs = tclDISPATCHGEN Pervasives.ignore tacs - -let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs - - -(** [extend_to_list startxs rx endxs l] builds a list - [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises - [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) -let extend_to_list startxs rx endxs l = - (* spiwack: I use [l] essentially as a natural number *) - let rec duplicate acc = function - | [] -> acc - | _::rest -> duplicate (rx::acc) rest - in - let rec tail to_match rest = - match rest, to_match with - | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *) - | _::rest , _::to_match -> tail to_match rest - | _ , [] -> duplicate endxs rest - in - let rec copy pref rest = - match rest,pref with - | [] , _::_ -> raise (SizeMismatch(0,0)) (* placeholder *) - | _::rest, a::pref -> a::(copy pref rest) - | _ , [] -> tail endxs rest - in - copy startxs l - -(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r] - tactic is "repeated" enough time such that every goal has a tactic - assigned to it ([b] is the list of tactics applied to the first - goals, [e] to the last goals, and [r] is applied to every goal in - between). *) -let tclEXTEND tacs1 rtac tacs2 = - let open Proof in - Comb.get >>= fun comb -> - try - let tacs = extend_to_list tacs1 rtac tacs2 comb in - tclDISPATCH tacs - with SizeMismatch _ -> - tclZERO (SizeMismatch( - CList.length comb, - (CList.length tacs1)+(CList.length tacs2))) -(* spiwack: failure occurs only when the number of goals is too - small. Hence we can assume that [rtac] is replicated 0 times for - any error message. *) - -(** [tclEXTEND [] tac []]. *) -let tclINDEPENDENT tac = - let open Proof in - Pv.get >>= fun initial -> - match initial.comb with - | [] -> tclUNIT () - | [_] -> tac - | _ -> - let tac = InfoL.tag (Info.DBranch) tac in - InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - - - -(** {7 Goal manipulation} *) - -(** Shelves all the goals under focus. *) -let shelve = - let open Proof in - Comb.get >>= fun initial -> - Comb.set [] >> - InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ initial) - - -(** [contained_in_info e evi] checks whether the evar [e] appears in - the hypotheses, the conclusion or the body of the evar_info - [evi]. Note: since we want to use it on goals, the body is actually - supposed to be empty. *) -let contained_in_info sigma e evi = - Evar.Set.mem e (Evd.evars_of_filtered_evar_info (Evarutil.nf_evar_info sigma evi)) - -(** [depends_on sigma src tgt] checks whether the goal [src] appears - as an existential variable in the definition of the goal [tgt] in - [sigma]. *) -let depends_on sigma src tgt = - let evi = Evd.find sigma tgt in - contained_in_info sigma src evi - -(** [unifiable sigma g l] checks whether [g] appears in another - subgoal of [l]. The list [l] may contain [g], but it does not - affect the result. *) -let unifiable sigma g l = - CList.exists (fun tgt -> not (Evar.equal g tgt) && depends_on sigma g tgt) l - -(** [partition_unifiable sigma l] partitions [l] into a pair [(u,n)] - where [u] is composed of the unifiable goals, i.e. the goals on - whose definition other goals of [l] depend, and [n] are the - non-unifiable goals. *) -let partition_unifiable sigma l = - CList.partition (fun g -> unifiable sigma g l) l - -(** Shelves the unifiable goals under focus, i.e. the goals which - appear in other goals under focus (the unfocused goals are not - considered). *) -let shelve_unifiable = - let open Proof in - Pv.get >>= fun initial -> - let (u,n) = partition_unifiable initial.solution initial.comb in - Comb.set n >> - InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >> - Shelf.modify (fun gls -> gls @ u) - -(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some - goals are unifiable (see {!shelve_unifiable}) in the current focus. *) -let guard_no_unifiable = - let open Proof in - Pv.get >>= fun initial -> - let (u,n) = partition_unifiable initial.solution initial.comb in - match u with - | [] -> tclUNIT () - | gls -> - let l = CList.map (fun g -> Evd.dependent_evar_ident g initial.solution) gls in - let l = CList.map (fun id -> Names.Name id) l in - tclZERO (Logic.RefinerError (Logic.UnresolvedBindings l)) - -(** [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) -let unshelve l p = - (* advance the goals in case of clear *) - let l = undefined p.solution l in - { p with comb = p.comb@l } - -let with_shelf tac = - let open Proof in - Pv.get >>= fun pv -> - let { shelf; solution } = pv in - Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >> - tac >>= fun ans -> - Pv.get >>= fun npv -> - let { shelf = gls; solution = sigma } = npv in - let gls' = Evd.future_goals sigma in - let fgoals = Evd.future_goals solution in - let pgoal = Evd.principal_future_goal solution in - let sigma = Evd.restore_future_goals sigma fgoals pgoal in - Pv.set { npv with shelf; solution = sigma } >> - tclUNIT (CList.rev_append gls' gls, ans) - -(** [goodmod p m] computes the representative of [p] modulo [m] in the - interval [[0,m-1]].*) -let goodmod p m = - let p' = p mod m in - (* if [n] is negative [n mod l] is negative of absolute value less - than [l], so [(n mod l)+l] is the representative of [n] in the - interval [[0,l-1]].*) - if p' < 0 then p'+m else p' - -let cycle n = - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >> - Comb.modify begin fun initial -> - let l = CList.length initial in - let n' = goodmod n l in - let (front,rear) = CList.chop n' initial in - rear@front - end - -let swap i j = - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >> - Comb.modify begin fun initial -> - let l = CList.length initial in - let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in - let i = goodmod i l and j = goodmod j l in - CList.map_i begin fun k x -> - match k with - | k when Int.equal k i -> CList.nth initial j - | k when Int.equal k j -> CList.nth initial i - | _ -> x - end 0 initial - end - -let revgoals = - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >> - Comb.modify CList.rev - -let numgoals = - let open Proof in - Comb.get >>= fun comb -> - return (CList.length comb) - - - -(** {7 Access primitives} *) - -let tclEVARMAP = Solution.get - -let tclENV = Env.get - - - -(** {7 Put-like primitives} *) - - -let emit_side_effects eff x = - { x with solution = Evd.emit_side_effects eff x.solution } - -let tclEFFECTS eff = - let open Proof in - return () >>= fun () -> (* The Global.env should be taken at exec time *) - Env.set (Global.env ()) >> - Pv.modify (fun initial -> emit_side_effects eff initial) - -let mark_as_unsafe = Status.put false - -(** Gives up on the goal under focus. Reports an unsafe status. Proofs - with given up goals cannot be closed. *) -let give_up = - let open Proof in - Comb.get >>= fun initial -> - Comb.set [] >> - mark_as_unsafe >> - InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >> - Giveup.put initial - - - -(** {7 Control primitives} *) - - -module Progress = struct - - let eq_constr = Evarutil.eq_constr_univs_test - - (** equality function on hypothesis contexts *) - let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = - let open Environ in - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Names.Id.equal i1 i2 && Option.equal (eq_constr sigma1 sigma2) c1 c2 - && (eq_constr sigma1 sigma2) t1 t2 - in List.equal eq_named_declaration c1 c2 - - let eq_evar_body sigma1 sigma2 b1 b2 = - let open Evd in - match b1, b2 with - | Evar_empty, Evar_empty -> true - | Evar_defined t1, Evar_defined t2 -> eq_constr sigma1 sigma2 t1 t2 - | _ -> false - - let eq_evar_info sigma1 sigma2 ei1 ei2 = - let open Evd in - eq_constr sigma1 sigma2 ei1.evar_concl ei2.evar_concl && - eq_named_context_val sigma1 sigma2 (ei1.evar_hyps) (ei2.evar_hyps) && - eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body - - (** Equality function on goals *) - let goal_equal evars1 gl1 evars2 gl2 = - let evi1 = Evd.find evars1 gl1 in - let evi2 = Evd.find evars2 gl2 in - eq_evar_info evars1 evars2 evi1 evi2 - -end - -let tclPROGRESS t = - let open Proof in - Pv.get >>= fun initial -> - t >>= fun res -> - Pv.get >>= fun final -> - (* [*_test] test absence of progress. [quick_test] is approximate - whereas [exhaustive_test] is complete. *) - let quick_test = - initial.solution == final.solution && initial.comb == final.comb - in - let exhaustive_test = - Util.List.for_all2eq begin fun i f -> - Progress.goal_equal initial.solution i final.solution f - end initial.comb final.comb - in - let test = - quick_test || exhaustive_test - in - if not test then - tclUNIT res - else - tclZERO (Errors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress.")) - -exception Timeout -let _ = Errors.register_handler begin function - | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!") - | _ -> Pervasives.raise Errors.Unhandled -end - -let tclTIMEOUT n t = - let open Proof in - (* spiwack: as one of the monad is a continuation passing monad, it - doesn't force the computation to be threaded inside the underlying - (IO) monad. Hence I force it myself by asking for the evaluation of - a dummy value first, lest [timeout] be called when everything has - already been computed. *) - let t = Proof.lift (Logic_monad.NonLogical.return ()) >> t in - Proof.get >>= fun initial -> - Proof.current >>= fun envvar -> - Proof.lift begin - Logic_monad.NonLogical.catch - begin - let open Logic_monad.NonLogical in - timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r -> - match r with - | Logic_monad.Nil e -> return (Util.Inr e) - | Logic_monad.Cons (r, _) -> return (Util.Inl r) - end - begin let open Logic_monad.NonLogical in function (e, info) -> - match e with - | Logic_monad.Timeout -> return (Util.Inr (Timeout, info)) - | Logic_monad.TacticFailure e -> - return (Util.Inr (e, info)) - | e -> Logic_monad.NonLogical.raise ~info e - end - end >>= function - | Util.Inl (res,s,m,i) -> - Proof.set s >> - Proof.put m >> - Proof.update (fun _ -> i) >> - return res - | Util.Inr (e, info) -> tclZERO ~info e - -let tclTIME s t = - let pr_time t1 t2 n msg = - let msg = - if n = 0 then - str msg - else - str (msg ^ " after ") ++ int n ++ str (String.plural n " backtracking") - in - msg_info(str "Tactic call" ++ pr_opt str s ++ str " ran for " ++ - System.fmt_time_difference t1 t2 ++ str " " ++ surround msg) in - let rec aux n t = - let open Proof in - tclUNIT () >>= fun () -> - let tstart = System.get_time() in - Proof.split t >>= let open Logic_monad in function - | Nil (e, info) -> - begin - let tend = System.get_time() in - pr_time tstart tend n "failure"; - tclZERO ~info e - end - | Cons (x,k) -> - let tend = System.get_time() in - pr_time tstart tend n "success"; - tclOR (tclUNIT x) (fun e -> aux (n+1) (k e)) - in aux 0 t - - - -(** {7 Unsafe primitives} *) - -module Unsafe = struct - - let tclEVARS evd = - Pv.modify (fun ps -> { ps with solution = evd }) - - let tclNEWGOALS gls = - Pv.modify begin fun step -> - let gls = undefined step.solution gls in - { step with comb = step.comb @ gls } - end - - let tclGETGOALS = Comb.get - - let tclSETGOALS = Comb.set - - let tclEVARSADVANCE evd = - Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) - - let tclEVARUNIVCONTEXT ctx = - Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) - - let reset_future_goals p = - { p with solution = Evd.reset_future_goals p.solution } - - let mark_as_goal_evm evd content = - let info = Evd.find evd content in - let info = - { info with Evd.evar_source = match info.Evd.evar_source with - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - in - let info = Typeclasses.mark_unresolvable info in - Evd.add evd content info - - let mark_as_goal p gl = - { p with solution = mark_as_goal_evm p.solution gl } - -end - - - -(** {7 Notations} *) - -module Notations = struct - let (>>=) = tclBIND - let (<*>) = tclTHEN - let (<+>) t1 t2 = tclOR t1 (fun _ -> t2) -end - -open Notations - - - -(** {6 Goal-dependent tactics} *) - -(* To avoid shadowing by the local [Goal] module *) -module GoalV82 = Goal.V82 - -let catchable_exception = function - | Logic_monad.Exception _ -> false - | e -> Errors.noncritical e - - -module Goal = struct - - type 'a t = { - env : Environ.env; - sigma : Evd.evar_map; - concl : Term.constr ; - self : Evar.t ; (* for compatibility with old-style definitions *) - } - - let assume (gl : 'a t) = (gl :> [ `NF ] t) - - let env { env=env } = env - let sigma { sigma=sigma } = sigma - let hyps { env=env } = Environ.named_context env - let concl { concl=concl } = concl - let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self - - let raw_concl { concl=concl } = concl - - - let gmake_with info env sigma goal = - { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; - sigma = sigma ; - concl = Evd.evar_concl info ; - self = goal } - - let nf_gmake env sigma goal = - let info = Evarutil.nf_evar_info sigma (Evd.find sigma goal) in - let sigma = Evd.add sigma goal info in - gmake_with info env sigma goal , sigma - - let nf_enter f = - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try - let (gl, sigma) = nf_gmake env sigma goal in - tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl)) - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - end - end - - let normalize { self } = - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma self in - tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) - - let gmake env sigma goal = - let info = Evd.find sigma goal in - gmake_with info env sigma goal - - let enter f = - let f gl = InfoL.tag (Info.DBranch) (f gl) in - InfoL.tag (Info.Dispatch) begin - iter_goal begin fun goal -> - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - try f (gmake env sigma goal) - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - end - end - - let goals = - Env.get >>= fun env -> - Pv.get >>= fun step -> - let sigma = step.solution in - let map goal = - match advance sigma goal with - | None -> None (** ppedrot: Is this check really necessary? *) - | Some goal -> - let gl = - tclEVARMAP >>= fun sigma -> - tclUNIT (gmake env sigma goal) - in - Some gl - in - tclUNIT (CList.map_filter map step.comb) - - (* compatibility *) - let goal { self=self } = self - -end - - - -(** {6 The refine tactic} *) - -module Refine = -struct - - let extract_prefix env info = - let ctx1 = List.rev (Environ.named_context env) in - let ctx2 = List.rev (Evd.evar_context info) in - let rec share l1 l2 accu = match l1, l2 with - | d1 :: l1, d2 :: l2 -> - if d1 == d2 then share l1 l2 (d1 :: accu) - else (accu, d2 :: l2) - | _ -> (accu, l2) - in - share ctx1 ctx2 [] - - let typecheck_evar ev env sigma = - let info = Evd.find sigma ev in - (** Typecheck the hypotheses. *) - let type_hyp (sigma, env) (na, body, t as decl) = - let evdref = ref sigma in - let _ = Typing.sort_of env evdref t in - let () = match body with - | None -> () - | Some body -> Typing.check env evdref body t - in - (!evdref, Environ.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 (sigma, env) = List.fold_left type_hyp (sigma, env) changed in - (** Typecheck the conclusion *) - let evdref = ref sigma in - let _ = Typing.sort_of env evdref (Evd.evar_concl info) in - !evdref - - let typecheck_proof c concl env sigma = - let evdref = ref sigma in - let () = Typing.check env evdref c concl in - !evdref - - let (pr_constrv,pr_constr) = - Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () - - let refine ?(unsafe = true) f = Goal.enter begin fun gl -> - let sigma = Goal.sigma gl in - let env = Goal.env gl in - let concl = Goal.concl gl in - (** Save the [future_goals] state to restore them after the - refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in - (** Create the refinement term *) - let (sigma, c) = f (Evd.reset_future_goals sigma) in - let evs = Evd.future_goals sigma in - let evkmain = Evd.principal_future_goal sigma in - (** Check that the introduced evars are well-typed *) - let fold accu ev = typecheck_evar ev env accu in - let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in - (** Check that the refined term is typesafe *) - let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in - (** Check that the goal itself does not appear in the refined term *) - let _ = - if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then () - else Pretype_errors.error_occur_check env sigma gl.Goal.self c - in - (** Proceed to the refinement *) - let sigma = match evkmain with - | None -> Evd.define gl.Goal.self c sigma - | Some evk -> - let id = Evd.evar_ident gl.Goal.self sigma in - Evd.rename evk id (Evd.define gl.Goal.self c sigma) - in - (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in - (** Select the goals *) - let comb = undefined sigma (CList.rev evs) in - let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in - let open Proof in - InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >> - Pv.modify (fun ps -> { ps with solution = sigma; comb; }) - end - - (** Useful definitions *) - - let with_type env evd c t = - let my_type = Retyping.get_type_of env evd c in - let j = Environ.make_judge c my_type in - let (evd,j') = - Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t - in - evd , j'.Environ.uj_val - - let refine_casted ?unsafe f = Goal.enter begin fun gl -> - let concl = Goal.concl gl in - let env = Goal.env gl in - let f h = let (h, c) = f h in with_type env h c concl in - refine ?unsafe f - end -end - - - -(** {6 Trace} *) - -module Trace = struct - - let record_info_trace = InfoL.record_trace - - let log m = InfoL.leaf (Info.Msg m) - let name_tactic m t = InfoL.tag (Info.Tactic m) t - - let pr_info ?(lvl=0) info = - assert (lvl >= 0); - Info.(print (collapse lvl info)) - -end - - - -(** {6 Non-logical state} *) - -module NonLogical = Logic_monad.NonLogical - -let tclLIFT = Proof.lift - -let tclCHECKINTERRUPT = - tclLIFT (NonLogical.make Control.check_for_interrupt) - - - - - -(*** Compatibility layer with <= 8.2 tactics ***) -module V82 = struct - type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - - let tactic tac = - (* spiwack: we ignore the dependencies between goals here, - expectingly preserving the semantics of <= 8.2 tactics *) - (* spiwack: convenience notations, waiting for ocaml 3.12 *) - let open Proof in - Pv.get >>= fun ps -> - try - let tac gl evd = - let glsigma = - tac { Evd.it = gl ; sigma = evd; } in - let sigma = glsigma.Evd.sigma in - let g = glsigma.Evd.it in - ( g, sigma ) - in - (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Evd.Monad.List.map (fun g s -> GoalV82.nf_evar s g) ps.comb ps.solution - in - let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in - let sgs = CList.flatten goalss in - let sgs = undefined evd sgs in - InfoL.leaf (Info.Tactic (fun () -> Pp.str"")) >> - Pv.set { ps with solution = evd; comb = sgs; } - with e when catchable_exception e -> - let (e, info) = Errors.push e in - tclZERO ~info e - - - (* normalises the evars in the goals, and stores the result in - solution. *) - let nf_evar_goals = - Pv.modify begin fun ps -> - let map g s = GoalV82.nf_evar s g in - let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in - { ps with solution = evd; comb = goals; } - end - - let has_unresolved_evar pv = - Evd.has_undefined pv.solution - - (* Main function in the implementation of Grab Existential Variables.*) - let grab pv = - let undef = Evd.undefined_map pv.solution in - let goals = CList.rev_map fst (Evar.Map.bindings undef) in - { pv with comb = goals } - - - - (* Returns the open goals of the proofview together with the evar_map to - interpret them. *) - let goals { comb = comb ; solution = solution; } = - { Evd.it = comb ; sigma = solution } - - let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar t)) initial in - { Evd.it = goals ; sigma=solution; } - - let top_evars initial = - let evars_of_initial (c,_) = - Evar.Set.elements (Evd.evars_of_term c) - in - CList.flatten (CList.map evars_of_initial initial) - - let instantiate_evar n com pv = - let (evk,_) = - let evl = Evarutil.non_instantiated pv.solution in - let evl = Evar.Map.bindings evl in - if (n <= 0) then - Errors.error "incorrect existential variable index" - else if CList.length evl < n then - Errors.error "not so many uninstantiated existential variables" - else - CList.nth evl (n-1) - in - { pv with - solution = Evar_refiner.instantiate_pf_com evk com pv.solution } - - let of_tactic t gls = - try - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in - let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in - { Evd.sigma = final.solution ; it = final.comb } - with Logic_monad.TacticFailure e as src -> - let (_, info) = Errors.push src in - iraise (e, info) - - let put_status = Status.put - - let catchable_exception = catchable_exception - - let wrap_exceptions f = - try f () - with e when catchable_exception e -> - let (e, info) = Errors.push e in tclZERO ~info e - -end diff --git a/proofs/proofview.mli b/proofs/proofview.mli deleted file mode 100644 index 2157459f..00000000 --- a/proofs/proofview.mli +++ /dev/null @@ -1,580 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Goal.goal list * Evd.evar_map - - -(** {6 Starting and querying a proof view} *) - -(** Abstract representation of the initial goals of a proof. *) -type entry - -(** Optimize memory consumption *) -val compact : entry -> proofview -> entry * proofview - -(** Initialises a proofview, the main argument is a list of - environments (including a [named_context] which are used as - hypotheses) pair with conclusion types, creating accordingly many - initial goals. Because a proof does not necessarily starts in an - empty [evar_map] (indeed a proof can be triggered by an incomplete - pretyping), [init] takes an additional argument to represent the - initial [evar_map]. *) -val init : Evd.evar_map -> (Environ.env * Term.types) list -> entry * proofview - -(** A [telescope] is a list of environment and conclusion like in - {!init}, except that each element may depend on the previous - goals. The telescope passes the goals in the form of a - [Term.constr] which represents the goal as an [evar]. The - [evar_map] is threaded in state passing style. *) -type telescope = - | TNil of Evd.evar_map - | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope) - -(** Like {!init}, but goals are allowed to be dependent on one - another. Dependencies between goals is represented with the type - [telescope] instead of [list]. Note that the first [evar_map] of - the telescope plays the role of the [evar_map] argument in - [init]. *) -val dependent_init : telescope -> entry * proofview - -(** [finished pv] is [true] if and only if [pv] is complete. That is, - if it has an empty list of focused goals. There could still be - unsolved subgoaled, but they would then be out of focus. *) -val finished : proofview -> bool - -(** Returns the current [evar] state. *) -val return : proofview -> Evd.evar_map - -val partial_proof : entry -> proofview -> constr list -val initial_goals : entry -> (constr * types) list - - - -(** {6 Focusing commands} *) - -(** A [focus_context] represents the part of the proof view which has - been removed by a focusing action, it can be used to unfocus later - on. *) -type focus_context - -(** Returns a stylised view of a focus_context for use by, for - instance, ide-s. *) -(* spiwack: the type of [focus_context] will change as we push more - refined functions to ide-s. This would be better than spawning a - new nearly identical function everytime. Hence the generic name. *) -(* In this version: the goals in the context, as a "zipper" (the first - list is in reversed order). *) -val focus_context : focus_context -> Goal.goal list * Goal.goal list - -(** [focus i j] focuses a proofview on the goals from index [i] to - index [j] (inclusive, goals are indexed from [1]). I.e. goals - number [i] to [j] become the only focused goals of the returned - proofview. It returns the focused proofview, and a context for - the focus stack. *) -val focus : int -> int -> proofview -> proofview * focus_context - -(** Unfocuses a proofview with respect to a context. *) -val unfocus : focus_context -> proofview -> proofview - - -(** {6 The tactic monad} *) - -(** - Tactics are objects which apply a transformation to all the - subgoals of the current view at the same time. By opposition to - the old vision of applying it to a single goal. It allows tactics - such as [shelve_unifiable], tactics to reorder the focused goals, - or global automation tactic for dependent subgoals (instantiating - an evar has influences on the other goals of the proof in - progress, not being able to take that into account causes the - current eauto tactic to fail on some instances where it could - succeed). Another benefit is that it is possible to write tactics - that can be executed even if there are no focused goals. - - Tactics form a monad ['a tactic], in a sense a tactic can be - seen as a function (without argument) which returns a value of - type 'a and modifies the environment (in our case: the view). - Tactics of course have arguments, but these are given at the - meta-level as OCaml functions. Most tactics in the sense we are - used to return [()], that is no really interesting values. But - some might pass information around. The tactics seen in Coq's - Ltac are (for now at least) only [unit tactic], the return values - are kept for the OCaml toolkit. The operation or the monad are - [Proofview.tclUNIT] (which is the "return" of the tactic monad) - [Proofview.tclBIND] (which is the "bind") and [Proofview.tclTHEN] - (which is a specialized bind on unit-returning tactics). - - Tactics have support for full-backtracking. Tactics can be seen - having multiple success: if after returning the first success a - failure is encountered, the tactic can backtrack and use a second - success if available. The state is backtracked to its previous - value, except the non-logical state defined in the {!NonLogical} - module below. -*) - - -(** The abstract type of tactics *) -type +'a tactic - -(** Applies a tactic to the current proofview. Returns a tuple - [a,pv,(b,sh,gu)] where [a] is the return value of the tactic, [pv] - is the updated proofview, [b] a boolean which is [true] if the - tactic has not done any action considered unsafe (such as - admitting a lemma), [sh] is the list of goals which have been - shelved by the tactic, and [gu] the list of goals on which the - tactic has given up. In case of multiple success the first one is - selected. If there is no success, fails with - {!Logic_monad.TacticFailure}*) -val apply : Environ.env -> 'a tactic -> proofview -> 'a - * proofview - * (bool*Goal.goal list*Goal.goal list) - * Proofview_monad.Info.tree - -(** {7 Monadic primitives} *) - -(** Unit of the tactic monad. *) -val tclUNIT : 'a -> 'a tactic - -(** Bind operation of the tactic monad. *) -val tclBIND : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - -(** Interprets the ";" (semicolon) of Ltac. As a monadic operation, - it's a specialized "bind". *) -val tclTHEN : unit tactic -> 'a tactic -> 'a tactic - -(** [tclIGNORE t] has the same operational content as [t], but drops - the returned value. *) -val tclIGNORE : 'a tactic -> unit tactic - -(** Generic monadic combinators for tactics. *) -module Monad : Monad.S with type +'a t = 'a tactic - -(** {7 Failure and backtracking} *) - -(** [tclZERO e] fails with exception [e]. It has no success. *) -val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic - -(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever - the successes of [t1] have been depleted and it failed with [e], - then it behaves as [t2 e]. In other words, [tclOR] inserts a - backtracking point. *) -val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic - -(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one - success or [t2 e] if [t1] fails with [e]. It is analogous to - [try/with] handler of exception in that it is not a backtracking - point. *) -val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic - -(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a] - succeeds at least once then it behaves as [tclBIND a s] otherwise, - if [a] fails with [e], then it behaves as [f e]. *) -val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic - -(** [tclONCE t] behave like [t] except it has at most one success: - [tclONCE t] stops after the first success of [t]. If [t] fails - with [e], [tclONCE t] also fails with [e]. *) -val tclONCE : 'a tactic -> 'a tactic - -(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one - success. Otherwise it fails. The tactic [t] is run until its first - success, then a failure with exception [e] is simulated. It [t] - yields another success, then [tclEXACTLY_ONCE e t] fails with - [MoreThanOneSuccess] (it is a user error). Otherwise, - [tclEXACTLY_ONCE e t] succeeds with the first success of - [t]. Notice that the choice of [e] is relevant, as the presence of - further successes may depend on [e] (see {!tclOR}). *) -exception MoreThanOneSuccess -val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic - -(** [tclCASE t] splits [t] into its first success and a - continuation. It is the most general primitive to control - backtracking. *) -type 'a case = - | Fail of iexn - | Next of 'a * (iexn -> 'a tactic) -val tclCASE : 'a tactic -> 'a case tactic - -(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of - stopping after the first success, it succeeds like [t] until a - failure with an exception [e] such that [p e = Some e'] is raised. At - which point it drops the remaining successes, failing with [e']. - [tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *) -val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic - - -(** {7 Focusing tactics} *) - -(** [tclFOCUS i j t] applies [t] after focusing on the goals number - [i] to [j] (see {!focus}). The rest of the goals is restored after - the tactic action. If the specified range doesn't correspond to - existing goals, fails with [NoSuchGoals] (a user error). this - exception is caught at toplevel with a default message + a hook - message that can be customized by [set_nosuchgoals_hook] below. - This hook is used to add a suggestion about bullets when - applicable. *) -exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> string option) -> unit - -val tclFOCUS : int -> int -> 'a tactic -> 'a tactic - -(** [tclFOCUSID x t] applies [t] on a (single) focused goal like - {!tclFOCUS}. The goal is found by its name rather than its - number.*) -val tclFOCUSID : Names.Id.t -> 'a tactic -> 'a tactic - -(** [tclTRYFOCUS i j t] behaves like {!tclFOCUS}, except that if the - specified range doesn't correspond to existing goals, behaves like - [tclUNIT ()] instead of failing. *) -val tclTRYFOCUS : int -> int -> unit tactic -> unit tactic - - -(** {7 Dispatching on goals} *) - -(** Dispatch tacticals are used to apply a different tactic to each - goal under focus. They come in two flavours: [tclDISPATCH] takes a - list of [unit tactic]-s and build a [unit tactic]. [tclDISPATCHL] - takes a list of ['a tactic] and returns an ['a list tactic]. - - They both work by applying each of the tactic in a focus - restricted to the corresponding goal (starting with the first - goal). In the case of [tclDISPATCHL], the tactic returns a list of - the same size as the argument list (of tactics), each element - being the result of the tactic executed in the corresponding goal. - - When the length of the tactic list is not the number of goal, - raises [SizeMismatch (g,t)] where [g] is the number of available - goals, and [t] the number of tactics passed. *) -exception SizeMismatch of int*int -val tclDISPATCH : unit tactic list -> unit tactic -val tclDISPATCHL : 'a tactic list -> 'a list tactic - -(** [tclEXTEND b r e] is a variant of {!tclDISPATCH}, where the [r] - tactic is "repeated" enough time such that every goal has a tactic - assigned to it ([b] is the list of tactics applied to the first - goals, [e] to the last goals, and [r] is applied to every goal in - between). *) -val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic - -(** [tclINDEPENDENT tac] runs [tac] on each goal successively, from - the first one to the last one. Backtracking in one goal is - independent of backtracking in another. It is equivalent to - [tclEXTEND [] tac []]. *) -val tclINDEPENDENT : unit tactic -> unit tactic - - -(** {7 Goal manipulation} *) - -(** Shelves all the goals under focus. The goals are placed on the - shelf for later use (or being solved by side-effects). *) -val shelve : unit tactic - -(** Shelves the unifiable goals under focus, i.e. the goals which - appear in other goals under focus (the unfocused goals are not - considered). *) -val shelve_unifiable : unit tactic - -(** [guard_no_unifiable] fails with error [UnresolvedBindings] if some - goals are unifiable (see {!shelve_unifiable}) in the current focus. *) -val guard_no_unifiable : unit tactic - -(** [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) -val unshelve : Goal.goal list -> proofview -> proofview - -(** [with_shelf tac] executes [tac] and returns its result together with the set - of goals shelved by [tac]. The current shelf is unchanged. *) -val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic - -(** If [n] is positive, [cycle n] puts the [n] first goal last. If [n] - is negative, then it puts the [n] last goals first.*) -val cycle : int -> unit tactic - -(** [swap i j] swaps the position of goals number [i] and [j] - (negative numbers can be used to address goals from the end. Goals - are indexed from [1]. For simplicity index [0] corresponds to goal - [1] as well, rather than raising an error. *) -val swap : int -> int -> unit tactic - -(** [revgoals] reverses the list of focused goals. *) -val revgoals : unit tactic - -(** [numgoals] returns the number of goals under focus. *) -val numgoals : int tactic - - -(** {7 Access primitives} *) - -(** [tclEVARMAP] doesn't affect the proof, it returns the current - [evar_map]. *) -val tclEVARMAP : Evd.evar_map tactic - -(** [tclENV] doesn't affect the proof, it returns the current - environment. It is not the environment of a particular goal, - rather the "global" environment of the proof. The goal-wise - environment is obtained via {!Proofview.Goal.env}. *) -val tclENV : Environ.env tactic - - -(** {7 Put-like primitives} *) - -(** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Safe_typing.private_constants -> unit tactic - -(** [mark_as_unsafe] declares the current tactic is unsafe. *) -val mark_as_unsafe : unit tactic - -(** Gives up on the goal under focus. Reports an unsafe status. Proofs - with given up goals cannot be closed. *) -val give_up : unit tactic - - -(** {7 Control primitives} *) - -(** [tclPROGRESS t] checks the state of the proof after [t]. It it is - identical to the state before, then [tclePROGRESS t] fails, otherwise - it succeeds like [t]. *) -val tclPROGRESS : 'a tactic -> 'a tactic - -(** Checks for interrupts *) -val tclCHECKINTERRUPT : unit tactic - -exception Timeout -(** [tclTIMEOUT n t] can have only one success. - In case of timeout if fails with [tclZERO Timeout]. *) -val tclTIMEOUT : int -> 'a tactic -> 'a tactic - -(** [tclTIME s t] displays time for each atomic call to t, using s as an - identifying annotation if present *) -val tclTIME : string option -> 'a tactic -> 'a tactic - -(** {7 Unsafe primitives} *) - -(** The primitives in the [Unsafe] module should be avoided as much as - possible, since they can make the proof state inconsistent. They are - nevertheless helpful, in particular when interfacing the pretyping and - the proof engine. *) -module Unsafe : sig - - (** [tclEVARS sigma] replaces the current [evar_map] by [sigma]. If - [sigma] has new unresolved [evar]-s they will not appear as - goal. If goals have been solved in [sigma] they will still - appear as unsolved goals. *) - val tclEVARS : Evd.evar_map -> unit tactic - - (** Like {!tclEVARS} but also checks whether goals have been solved. *) - val tclEVARSADVANCE : Evd.evar_map -> unit tactic - - (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently - being proved, appending them to the list of focused goals. If a - goal is already solved, it is not added. *) - val tclNEWGOALS : Goal.goal list -> unit tactic - - (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a - goal is already solved, it is not set. *) - val tclSETGOALS : Goal.goal list -> unit tactic - - (** [tclGETGOALS] returns the list of goals under focus. *) - val tclGETGOALS : Goal.goal list tactic - - (** Sets the evar universe context. *) - val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic - - (** Clears the future goals store in the proof view. *) - val reset_future_goals : proofview -> proofview - - (** Give an evar the status of a goal (changes its source location - and makes it unresolvable for type classes. *) - val mark_as_goal : proofview -> Evar.t -> proofview -end - -(** {7 Notations} *) - -module Notations : sig - - (** {!tclBIND} *) - val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic - (** {!tclTHEN} *) - val (<*>) : unit tactic -> 'a tactic -> 'a tactic - (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *) - val (<+>) : 'a tactic -> 'a tactic -> 'a tactic - -end - - -(** {6 Goal-dependent tactics} *) - -module Goal : sig - - (** The type of goals. The parameter type is a phantom argument indicating - whether the data contained in the goal has been normalized w.r.t. the - current sigma. If it is the case, it is flagged [ `NF ]. You may still - access the un-normalized data using {!assume} if you known you do not rely - on the assumption of being normalized, at your own risk. *) - type 'a t - - (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t - - (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic - - (** [concl], [hyps], [env] and [sigma] given a goal [gl] return - respectively the conclusion of [gl], the hypotheses of [gl], the - environment of [gl] (i.e. the global environment and the - hypotheses) and the current evar map. *) - val concl : [ `NF ] t -> Term.constr - val hyps : [ `NF ] t -> Context.named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t - - (** Returns the goal's conclusion even if the goal is not - normalised. *) - val raw_concl : 'a t -> Term.constr - - (** [nf_enter t] applies the goal-dependent tactic [t] in each goal - independently, in the manner of {!tclINDEPENDENT} except that - the current goal is also given as an argument to [t]. The goal - is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic - - (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic - - (** Recover the list of current goals under focus, without evar-normalization *) - val goals : [ `LZ ] t tactic list tactic - - (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t - -end - - -(** {6 The refine tactic} *) - -module Refine : sig - - (** Printer used to print the constr which refine refines. *) - val pr_constr : - (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t - - (** {7 Refinement primitives} *) - - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic - (** In [refine ?unsafe t], [t] is a term with holes under some - [evar_map] context. The term [t] is used as a partial solution - for the current goal (refine is a goal-dependent tactic), the - new holes created by [t] become the new subgoals. Exception - raised during the interpretation of [t] are caught and result in - tactic failures. If [unsafe] is [true] (default) [t] is - type-checked beforehand. *) - - (** {7 Helper functions} *) - - val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr - (** [with_type env sigma c t] ensures that [c] is of type [t] - inserting a coercion if needed. *) - - val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic - (** Like {!refine} except the refined term is coerced to the conclusion of the - current goal. *) - -end - - -(** {6 Trace} *) - -module Trace : sig - - (** [record_info_trace t] behaves like [t] except the [info] trace - is stored. *) - val record_info_trace : 'a tactic -> 'a tactic - - val log : Proofview_monad.lazy_msg -> unit tactic - val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic - - val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds - -end - - -(** {6 Non-logical state} *) - -(** The [NonLogical] module allows the execution of effects (including - I/O) in tactics (non-logical side-effects are not discarded at - failures). *) -module NonLogical : module type of Logic_monad.NonLogical - -(** [tclLIFT c] is a tactic which behaves exactly as [c]. *) -val tclLIFT : 'a NonLogical.t -> 'a tactic - - -(**/**) - -(*** Compatibility layer with <= 8.2 tactics ***) -module V82 : sig - type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma - val tactic : tac -> unit tactic - - (* normalises the evars in the goals, and stores the result in - solution. *) - val nf_evar_goals : unit tactic - - val has_unresolved_evar : proofview -> bool - - (* Main function in the implementation of Grab Existential Variables. - Resets the proofview's goals so that it contains all unresolved evars - (in chronological order of insertion). *) - val grab : proofview -> proofview - - (* Returns the open goals of the proofview together with the evar_map to - interpret them. *) - val goals : proofview -> Evar.t list Evd.sigma - - val top_goals : entry -> proofview -> Evar.t list Evd.sigma - - (* returns the existential variable used to start the proof *) - val top_evars : entry -> Evd.evar list - - (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview - - (* Caution: this function loses quite a bit of information. It - should be avoided as much as possible. It should work as - expected for a tactic obtained from {!V82.tactic} though. *) - val of_tactic : 'a tactic -> tac - - (* marks as unsafe if the argument is [false] *) - val put_status : bool -> unit tactic - - (* exception for which it is deemed to be safe to transmute into - tactic failure. *) - val catchable_exception : exn -> bool - - (* transforms every Ocaml (catchable) exception into a failure in - the monad. *) - val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic -end diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml deleted file mode 100644 index e9bc7761..00000000 --- a/proofs/proofview_monad.ml +++ /dev/null @@ -1,275 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* { head = a::head ; opened=[] } - | a::Seq(b,f)::opened -> { head ; opened=Seq(b,a::f)::opened } - | [] -> assert false - let leaf a s = close (opn a s) - - (** Returning a forest. It is the responsibility of the library - builder to close all the tags. *) - (* spiwack: I may want to close the tags instead, to deal with - interruptions. *) - let rec mirror f = List.rev_map mirror_tree f - and mirror_tree (Seq(a,f)) = Seq(a,mirror f) - - let to_tree = function - | { head ; opened=[] } -> mirror head - | { head ; opened=_::_} -> assert false - -end - - - -(** {6 State types} *) - -(** We typically label nodes of [Trace.tree] with messages to - print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds -let pr_lazy_msg msg = msg () - -(** Info trace. *) -module Info = struct - - (** The type of the tags for [info]. *) - type tag = - | Msg of lazy_msg (** A simple message *) - | Tactic of lazy_msg (** A tactic call *) - | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *) - | DBranch (** A special marker to delimit individual branch of a dispatch. *) - - type state = tag Trace.incr - type tree = tag Trace.forest - - - - let pr_in_comments m = Pp.(str"(* "++pr_lazy_msg m++str" *)") - - let unbranch = function - | Trace.Seq (DBranch,brs) -> brs - | _ -> assert false - - - let is_empty_branch = let open Trace in function - | Seq(DBranch,[]) -> true - | _ -> false - - (** Dispatch with empty branches are (supposed to be) equivalent to - [idtac] which need not appear, so they are removed from the - trace. *) - let dispatch brs = - let open Trace in - if CList.for_all is_empty_branch brs then None - else Some (Seq(Dispatch,brs)) - - let constr = let open Trace in function - | Dispatch -> dispatch - | t -> fun br -> Some (Seq(t,br)) - - let rec compress_tree = let open Trace in function - | Seq(t,f) -> constr t (compress f) - and compress f = - CList.map_filter compress_tree f - - let rec is_empty = let open Trace in function - | Seq(Dispatch,brs) -> List.for_all is_empty brs - | Seq(DBranch,br) -> List.for_all is_empty br - | _ -> false - - (** [with_sep] is [true] when [Tactic m] must be printed with a - trailing semi-colon. *) - let rec pr_tree with_sep = let open Trace in function - | Seq (Msg m,[]) -> pr_in_comments m - | Seq (Tactic m,_) -> - let tail = if with_sep then Pp.str";" else Pp.mt () in - Pp.(pr_lazy_msg m ++ tail) - | Seq (Dispatch,brs) -> - let tail = if with_sep then Pp.str";" else Pp.mt () in - Pp.(pr_dispatch brs++tail) - | Seq (Msg _,_::_) | Seq (DBranch,_) -> assert false - and pr_dispatch brs = - let open Pp in - let brs = List.map unbranch brs in - match brs with - | [br] -> pr_forest br - | _ -> - let sep () = spc()++str"|"++spc() in - let branches = prlist_with_sep sep pr_forest brs in - str"[>"++spc()++branches++spc()++str"]" - and pr_forest = function - | [] -> Pp.mt () - | [tr] -> pr_tree false tr - | tr::l -> Pp.(pr_tree true tr ++ pr_forest l) - - let print f = - pr_forest (compress f) - - let rec collapse_tree n t = - let open Trace in - match n , t with - | 0 , t -> [t] - | _ , (Seq(Tactic _,[]) as t) -> [t] - | n , Seq(Tactic _,f) -> collapse (pred n) f - | n , Seq(Dispatch,brs) -> [Seq(Dispatch, (collapse n brs))] - | n , Seq(DBranch,br) -> [Seq(DBranch, (collapse n br))] - | _ , (Seq(Msg _,_) as t) -> [t] - and collapse n f = - CList.map_append (collapse_tree n) f -end - - -(** Type of proof views: current [evar_map] together with the list of - focused goals. *) -type proofview = { - solution : Evd.evar_map; - comb : Goal.goal list; - shelf : Goal.goal list; -} - -(** {6 Instantiation of the logic monad} *) - -(** Parameters of the logic monads *) -module P = struct - - type s = proofview * Environ.env - - (** Recording info trace (true) or not. *) - type e = bool - - (** Status (safe/unsafe) * shelved goals * given up *) - type w = bool * Evar.t list - - let wunit = true , [] - let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2 - - type u = Info.state - - let uunit = Trace.empty_incr - -end - -module Logical = Logic_monad.Logical(P) - - -(** {6 Lenses to access to components of the states} *) - -module type State = sig - type t - val get : t Logical.t - val set : t -> unit Logical.t - val modify : (t->t) -> unit Logical.t -end - -module type Writer = sig - type t - val put : t -> unit Logical.t -end - -module Pv : State with type t := proofview = struct - let get = Logical.(map fst get) - let set p = Logical.modify (fun (_,e) -> (p,e)) - let modify f= Logical.modify (fun (p,e) -> (f p,e)) -end - -module Solution : State with type t := Evd.evar_map = struct - let get = Logical.map (fun {solution} -> solution) Pv.get - let set s = Pv.modify (fun pv -> { pv with solution = s }) - let modify f = Pv.modify (fun pv -> { pv with solution = f pv.solution }) -end - -module Comb : State with type t = Evar.t list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list - let get = Logical.map (fun {comb} -> comb) Pv.get - let set c = Pv.modify (fun pv -> { pv with comb = c }) - let modify f = Pv.modify (fun pv -> { pv with comb = f pv.comb }) -end - -module Env : State with type t := Environ.env = struct - let get = Logical.(map snd get) - let set e = Logical.modify (fun (p,_) -> (p,e)) - let modify f = Logical.modify (fun (p,e) -> (p,f e)) -end - -module Status : Writer with type t := bool = struct - let put s = Logical.put (s, []) -end - -module Shelf : State with type t = Evar.t list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list - let get = Logical.map (fun {shelf} -> shelf) Pv.get - let set c = Pv.modify (fun pv -> { pv with shelf = c }) - let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) -end - -module Giveup : Writer with type t = Evar.t list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = Evar.t list - let put gs = Logical.put (true, gs) -end - -(** Lens and utilies pertaining to the info trace *) -module InfoL = struct - let recording = Logical.current - let if_recording t = - let open Logical in - recording >>= fun r -> - if r then t else return () - - let record_trace t = Logical.local true t - - let raw_update = Logical.update - let update f = if_recording (raw_update f) - let opn a = update (Trace.opn a) - let close = update Trace.close - let leaf a = update (Trace.leaf a) - - let tag a t = - let open Logical in - recording >>= fun r -> - if r then begin - raw_update (Trace.opn a) >> - t >>= fun a -> - raw_update Trace.close >> - return a - end else - t -end diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli deleted file mode 100644 index 7a6ea10f..00000000 --- a/proofs/proofview_monad.mli +++ /dev/null @@ -1,148 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a forest - - (** [open a] opens a tag with name [a]. *) - val opn : 'a -> 'a incr -> 'a incr - - (** [close] closes the last open tag. It is the responsibility of - the user to close all the tags. *) - val close : 'a incr -> 'a incr - - (** [leaf] creates an empty tag with name [a]. *) - val leaf : 'a -> 'a incr -> 'a incr - -end - -(** {6 State types} *) - -(** We typically label nodes of [Trace.tree] with messages to - print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds - -(** Info trace. *) -module Info : sig - - (** The type of the tags for [info]. *) - type tag = - | Msg of lazy_msg (** A simple message *) - | Tactic of lazy_msg (** A tactic call *) - | Dispatch (** A call to [tclDISPATCH]/[tclEXTEND] *) - | DBranch (** A special marker to delimit individual branch of a dispatch. *) - - type state = tag Trace.incr - type tree = tag Trace.forest - - val print : tree -> Pp.std_ppcmds - - (** [collapse n t] flattens the first [n] levels of [Tactic] in an - info trace, effectively forgetting about the [n] top level of - names (if there are fewer, the last name is kept). *) - val collapse : int -> tree -> tree - -end - -(** Type of proof views: current [evar_map] together with the list of - focused goals. *) -type proofview = { - solution : Evd.evar_map; - comb : Goal.goal list; - shelf : Goal.goal list; -} - -(** {6 Instantiation of the logic monad} *) - -module P : sig - type s = proofview * Environ.env - - (** Status (safe/unsafe) * given up *) - type w = bool * Evar.t list - - val wunit : w - val wprod : w -> w -> w - - (** Recording info trace (true) or not. *) - type e = bool - - type u = Info.state - - val uunit : u -end - -module Logical : module type of Logic_monad.Logical(P) - - -(** {6 Lenses to access to components of the states} *) - -module type State = sig - type t - val get : t Logical.t - val set : t -> unit Logical.t - val modify : (t->t) -> unit Logical.t -end - -module type Writer = sig - type t - val put : t -> unit Logical.t -end - -(** Lens to the [proofview]. *) -module Pv : State with type t := proofview - -(** Lens to the [evar_map] of the proofview. *) -module Solution : State with type t := Evd.evar_map - -(** Lens to the list of focused goals. *) -module Comb : State with type t = Evar.t list - -(** Lens to the global environment. *) -module Env : State with type t := Environ.env - -(** Lens to the tactic status ([true] if safe, [false] if unsafe) *) -module Status : Writer with type t := bool - -(** Lens to the list of goals which have been shelved during the - execution of the tactic. *) -module Shelf : State with type t = Evar.t list - -(** Lens to the list of goals which were given up during the execution - of the tactic. *) -module Giveup : Writer with type t = Evar.t list - -(** Lens and utilies pertaining to the info trace *) -module InfoL : sig - (** [record_trace t] behaves like [t] and compute its [info] trace. *) - val record_trace : 'a Logical.t -> 'a Logical.t - - val update : (Info.state -> Info.state) -> unit Logical.t - val opn : Info.tag -> unit Logical.t - val close : unit Logical.t - val leaf : Info.tag -> unit Logical.t - - (** [tag a t] opens tag [a] runs [t] then closes the tag. *) - val tag : Info.tag -> 'a Logical.t -> 'a Logical.t -end diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index ea21917a..72cb05f1 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names open Term @@ -17,7 +17,7 @@ open Genredexpr open Pattern open Reductionops open Tacred -open Closure +open CClosure open RedFlags open Libobject open Misctypes @@ -29,17 +29,22 @@ let cbv_vm env sigma c = error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp +let warn_native_compute_disabled = + CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" + (fun () -> + strbrk "native_compute disabled at configure time; falling back to vm_compute.") + let cbv_native env sigma c = if Coq_config.no_native_compiler then - let () = msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in - cbv_vm env sigma c + (warn_native_compute_disabled (); + cbv_vm env sigma c) else let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp let whd_cbn flags env sigma t = let (state,_) = - (whd_state_gen true flags env sigma (t,Reductionops.Stack.empty)) + (whd_state_gen true true flags env sigma (t,Reductionops.Stack.empty)) in Reductionops.Stack.zip ~refold:true state let strong_cbn flags = @@ -141,7 +146,9 @@ let make_flag_constant = function let make_flag env f = let red = no_red in let red = if f.rBeta then red_add red fBETA else red in - let red = if f.rIota then red_add red fIOTA else red in + let red = if f.rMatch then red_add red fMATCH else red in + let red = if f.rFix then red_add red fFIX else red in + let red = if f.rCofix then red_add red fCOFIX else red in let red = if f.rZeta then red_add red fZETA else red in let red = if f.rDelta then (* All but rConst *) @@ -158,8 +165,6 @@ let make_flag env f = f.rConst red in red -let is_reference = function PRef _ | PVar _ -> true | _ -> false - (* table of custom reductino fonctions, not synchronized, filled via ML calls to [declare_reduction] *) let reduction_tab = ref String.Map.empty @@ -196,7 +201,7 @@ let out_arg = function let out_with_occurrences (occs,c) = (Locusops.occurrences_map (List.map out_arg) occs, c) -let e_red f env evm c = evm, f env evm c +let e_red f = { e_redfun = fun env evm c -> Sigma.here (f env (Sigma.to_evar_map evm) c) evm } let head_style = false (* Turn to true to have a semantics where simpl only reduce at the head when an evaluable reference is given, e.g. @@ -211,6 +216,11 @@ let contextualize f g = function e_red (contextually b (l,c) (fun _ -> h)) | None -> e_red g +let warn_simpl_unfolding_modifiers = + CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics" + (fun () -> + Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") + let reduction_of_red_expr env = let make_flag = make_flag env in let rec reduction_of_red_expr = function @@ -223,7 +233,7 @@ let reduction_of_red_expr env = let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in let () = if not (!simplIsCbn || List.is_empty f.rConst) then - Pp.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in + warn_simpl_unfolding_modifiers () in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) | Cbn f -> diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index b9191108..d4c2c4a6 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Interpretation layer of redexprs such as hnf, cbv, etc. *) + open Names open Term open Pattern diff --git a/proofs/refine.ml b/proofs/refine.ml new file mode 100644 index 00000000..3f552706 --- /dev/null +++ b/proofs/refine.ml @@ -0,0 +1,162 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + if d1 == d2 then share l1 l2 (d1 :: accu) + else (accu, d2 :: l2) + | _ -> (accu, l2) + in + share ctx1 ctx2 [] + +let typecheck_evar ev env sigma = + let info = Evd.find sigma ev in + (** Typecheck the hypotheses. *) + let type_hyp (sigma, env) decl = + let t = 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 body t + in + (!evdref, Environ.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 (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 (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"") () + +(* 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 + +(* 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 make_refine_enter ?(unsafe = true) f = + { enter = fun gl -> + let gl = Proofview.Goal.assume gl in + let sigma = Proofview.Goal.sigma gl in + let sigma = Sigma.to_evar_map sigma in + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in + (** Save the [future_goals] state to restore them after the + refinement. *) + let prev_future_goals = Evd.future_goals sigma in + let prev_principal_goal = Evd.principal_future_goal sigma in + (** Create the refinement term *) + let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in + let evs = Evd.future_goals sigma in + let evkmain = Evd.principal_future_goal sigma in + (** Redo the effects in sigma in the monad's env *) + let privates_csts = Evd.eval_side_effects sigma in + let sideff = Safe_typing.side_effects_of_private_constants privates_csts in + let env = add_side_effects env sideff in + (** Check that the introduced evars are well-typed *) + let fold accu ev = typecheck_evar ev env accu in + let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in + (** Check that the refined term is typesafe *) + let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in + (** Check that the goal itself does not appear in the refined term *) + let self = Proofview.Goal.goal gl in + let _ = + if not (Evarutil.occur_evar_upto sigma self c) then () + else Pretype_errors.error_occur_check env sigma self c + in + (** Proceed to the refinement *) + let sigma = match evkmain with + | None -> Evd.define self c sigma + | Some evk -> + let id = Evd.evar_ident self sigma in + let sigma = Evd.define self c sigma in + match id with + | None -> sigma + | Some id -> Evd.rename evk id sigma + in + (** Restore the [future goals] state. *) + let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in + (** Select the goals *) + let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in + let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in + let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in + Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> + Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.tclUNIT v + } + +let refine_one ?(unsafe = true) f = + Proofview.Goal.enter_one (make_refine_enter ~unsafe f) + +let refine ?(unsafe = true) f = + let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in + Proofview.Goal.enter (make_refine_enter ~unsafe f) + +(** Useful definitions *) + +let with_type env evd c t = + let my_type = Retyping.get_type_of env evd c in + let j = Environ.make_judge c my_type in + let (evd,j') = + Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t + in + evd , j'.Environ.uj_val + +let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> + let gl = Proofview.Goal.assume gl in + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let f = { run = fun h -> + let Sigma (c, h, p) = f.run h in + let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) + } in + refine ?unsafe f +end } + +(** {7 solve_constraints} + + Ensure no remaining unification problems are left. Run at every "." by default. *) + +let solve_constraints = + let open Proofview in + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + Unsafe.tclEVARSADVANCE sigma + with e -> tclZERO e diff --git a/proofs/refine.mli b/proofs/refine.mli new file mode 100644 index 00000000..a44632ef --- /dev/null +++ b/proofs/refine.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t + +(** {7 Refinement primitives} *) + +val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** In [refine ?unsafe t], [t] is a term with holes under some + [evar_map] context. The term [t] is used as a partial solution + for the current goal (refine is a goal-dependent tactic), the + new holes created by [t] become the new subgoals. Exceptions + raised during the interpretation of [t] are caught and result in + tactic failures. If [unsafe] is [false] (default is [true]) [t] is + type-checked beforehand. *) + +val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic +(** A generalization of [refine] which assumes exactly one goal under focus *) + +(** {7 Helper functions} *) + +val with_type : Environ.env -> Evd.evar_map -> + Term.constr -> Term.types -> Evd.evar_map * Term.constr +(** [with_type env sigma c t] ensures that [c] is of type [t] + inserting a coercion if needed. *) + +val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic +(** Like {!refine} except the refined term is coerced to the conclusion of the + current goal. *) + +(** {7 Unification constraint handling} *) + +val solve_constraints : unit tactic +(** Solve any remaining unification problems, applying heuristics. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458..ea8543b0 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -7,13 +7,13 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Evd open Environ open Proof_type open Logic - +open Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -57,7 +57,7 @@ let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls + Feedback.msg_info (hov 0 s); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) @@ -197,12 +197,12 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.named_context = pf_hyps goal in + let oldhyps:Context.Named.t = pf_hyps goal in let rslt:Proof_type.goal list Evd.sigma = tac goal in let { it = gls; sigma = sigma; } = rslt in - let hyps:Context.named_context list = + let hyps:Context.Named.t list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp (i1, c1, t1) (i2, c2, t2) = Names.Id.equal i1 i2 in + let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp hypl oldhyps) @@ -215,12 +215,13 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) List.fold_left (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") ^ (List.fold_left - (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in - pp (str (emacs_str "") + Feedback.msg_notice + (str (emacs_str "") ++ (hov 0 (str s)) - ++ (str (emacs_str "")) ++ fnl()); + ++ (str (emacs_str ""))); tclIDTAC goal;; @@ -239,8 +240,8 @@ let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e when Errors.noncritical e -> - let e = Errors.push e in catch_failerror e; t2 g + | e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -252,8 +253,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e when Errors.noncritical e -> - let e = Errors.push e in catch_failerror e; None + with e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; None with | None -> t2else gls | Some sgl -> @@ -283,12 +284,12 @@ let ite_gen tcal tac_if continue tac_else gl= try tac_else gl with - e' when Errors.noncritical e' -> iraise e in + e' when CErrors.noncritical e' -> iraise e in try tcal tac_if0 continue gl with (* Breakpoint *) - | e when Errors.noncritical e -> - let e = Errors.push e in catch_failerror e; tac_else0 e gl + | e when CErrors.noncritical e -> + let e = CErrors.push e in catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 13a9be59..6dcafb77 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Context +(** Legacy proof engine. Do not use in newly written code. *) + open Evd open Proof_type @@ -16,7 +17,7 @@ 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_hyps : goal sigma -> Context.Named.t val unpackage : 'a sigma -> evar_map ref * 'a val repackage : evar_map ref -> 'a -> 'a sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a75b6fa0..330594af 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -18,6 +18,8 @@ open Tacred open Proof_type open Logic open Refiner +open Sigma.Notations +open Context.Named.Declaration let re_sig it gc = { it = it; sigma = gc; } @@ -40,21 +42,22 @@ let pf_hyps = Refiner.pf_hyps let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls) let pf_hyps_types gls = let sign = Environ.named_context (pf_env gls) in - List.map (fun (id,_,x) -> (id, x)) sign + List.map (function LocalAssum (id,x) + | LocalDef (id,_,x) -> id, x) + sign -let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id +let pf_nth_hyp_id gls n = List.nth (pf_hyps gls) (n-1) |> get_id let pf_last_hyp gl = List.hd (pf_hyps gl) let pf_get_hyp gls id = try - Context.lookup_named id (pf_hyps gls) + Context.Named.lookup id (pf_hyps gls) with Not_found -> raise (RefinerError (NoSuchHyp id)) let pf_get_hyp_typ gls id = - let (_,_,ty)= (pf_get_hyp gls id) in - ty + pf_get_hyp gls id |> get_type let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) @@ -70,7 +73,10 @@ let pf_get_new_ids ids gls = let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_reduction_of_red_expr gls re c = - (fst (reduction_of_red_expr (pf_env gls) re)) (pf_env gls) (project gls) c + let (redfun, _) = reduction_of_red_expr (pf_env gls) re in + let sigma = Sigma.Unsafe.of_evar_map (project gls) in + let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in + (Sigma.to_evar_map sigma, c) let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = @@ -78,7 +84,7 @@ let pf_eapply f gls x = let pf_reduce = pf_apply let pf_e_reduce = pf_apply -let pf_whd_betadeltaiota = pf_reduce whd_betadeltaiota +let pf_whd_all = pf_reduce whd_all let pf_hnf_constr = pf_reduce hnf_constr let pf_nf = pf_reduce simpl let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) @@ -95,7 +101,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) +let pf_hnf_type_of gls = pf_whd_all gls % pf_get_type_of gls let pf_is_matching = pf_apply Constr_matching.is_matching_conv let pf_matches = pf_apply Constr_matching.matches_conv @@ -115,26 +121,11 @@ let internal_cut_rev_no_check replace id t gl = let refine_no_check c gl = refiner (Refine c) gl -(* This does not check dependencies *) -let thin_no_check ids gl = - if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl - -let move_hyp_no_check id1 id2 gl = - refiner (Move (id1,id2)) gl - -let mutual_fix f n others j gl = - with_check (refiner (FixRule (f,n,others,j))) gl - -let mutual_cofix f others j gl = - with_check (refiner (Cofix (f,others,j))) gl - (* Versions with consistency checks *) let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) -let thin c = with_check (thin_no_check c) -let move_hyp id id' = with_check (move_hyp_no_check id id') (* Pretty-printers *) @@ -158,11 +149,15 @@ let pr_glls glls = (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct + let project gl = + let sigma = Proofview.Goal.sigma gl in + Sigma.to_evar_map sigma + let pf_apply f gl = - f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) + f (Proofview.Goal.env gl) (project gl) let of_old f gl = - f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl } + f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } let pf_global id gl = (** We only check for the existence of an [id] in [hyps] *) @@ -176,6 +171,9 @@ module New = struct let pf_unsafe_type_of gl t = pf_apply unsafe_type_of gl t + let pf_get_type_of gl t = + pf_apply (Retyping.get_type_of ~lax:true) gl t + let pf_type_of gl t = pf_apply type_of gl t @@ -192,34 +190,35 @@ module New = struct next_ident_away id ids let pf_get_hyp id gl = - let hyps = Proofview.Goal.hyps gl in + let hyps = Proofview.Goal.env gl in let sign = - try Context.lookup_named id hyps + try Environ.lookup_named id hyps with Not_found -> raise (RefinerError (NoSuchHyp id)) in sign let pf_get_hyp_typ id gl = - let (_,_,ty) = pf_get_hyp id gl in - ty + pf_get_hyp id gl |> get_type let pf_hyps_types gl = let env = Proofview.Goal.env gl in let sign = Environ.named_context env in - List.map (fun (id,_,x) -> (id, x)) sign + List.map (function LocalAssum (id,x) + | LocalDef (id,_,x) -> id, x) + sign let pf_last_hyp gl = let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) = (** We normalize the conclusion just after *) let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = project gl in nf_evar sigma concl - let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + let pf_whd_all gl t = pf_apply whd_all gl t let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t @@ -228,13 +227,13 @@ module New = struct let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_betadeltaiota gl (pf_get_type_of gl t) + pf_whd_all gl (pf_get_type_of gl t) let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t + let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t - let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t + let pf_nf_evar gl t = nf_evar (project gl) t end diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7e943cb1..59f296f6 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Environ open Evd open Proof_type @@ -34,18 +33,18 @@ val apply_sig_tac : val pf_concl : goal sigma -> types val pf_env : goal sigma -> env -val pf_hyps : goal sigma -> named_context +val pf_hyps : goal sigma -> Context.Named.t (*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_last_hyp : goal sigma -> Context.Named.Declaration.t 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_get_hyp : goal sigma -> Id.t -> named_declaration +val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t @@ -64,7 +63,7 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_betadeltaiota : goal sigma -> constr -> 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 @@ -87,18 +86,12 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool val refiner : rule -> tactic val internal_cut_no_check : bool -> Id.t -> types -> tactic val refine_no_check : constr -> tactic -val thin_no_check : Id.t list -> tactic -val mutual_fix : - Id.t -> int -> (Id.t * int * constr) list -> int -> tactic -val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic (** {6 The most primitive tactics with consistency and type checking } *) val internal_cut : bool -> Id.t -> types -> tactic val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic -val thin : Id.t list -> tactic -val move_hyp : Id.t -> Id.t move_location -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds @@ -106,36 +99,47 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : identifier -> 'a Proofview.Goal.t -> constr - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + (** FIXME: encapsulate the level in an existential type. *) + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : [ `NF ] Proofview.Goal.t -> types + val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map + val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env + val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types - val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types - val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool + (** WRONG: To be avoided at all costs, it typechecks the term entirely but + forgets the universe constraints necessary to retypecheck it *) + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types - val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + (** This function does no type inference and expects an already well-typed term. + It recomputes its type in the fastest way possible (no conversion is ever involved) *) + val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types - val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> [ `NF ] Proofview.Goal.t -> types - val pf_last_hyp : [ `NF ] Proofview.Goal.t -> named_declaration + (** This function entirely type-checks the term and computes its type + and the implied universe constraints. *) + val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types + val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types + val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list + val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t + val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t - val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_all : ('a, 'r) Proofview.Goal.t -> constr -> constr + val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr + + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + + val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr end diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml deleted file mode 100644 index a4a447e8..00000000 --- a/proofs/tactic_debug.ml +++ /dev/null @@ -1,318 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* mt()) - -let explain_logic_error_no_anomaly = ref (fun e -> mt()) - -let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) -let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) - -(* Prints the goal *) - -let db_pr_goal gl = - let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - let penv = print_named_context env in - let pc = print_constr_env env concl in - str" " ++ hv 0 (penv ++ fnl () ++ - str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () - -let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> - let pg = db_pr_goal gl in - Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) - end - - -(* Prints the commands *) -let help () = - msg_tac_debug (str "Commands: = Continue" ++ fnl() ++ - str " h/? = Help" ++ fnl() ++ - str " r = Run times" ++ fnl() ++ - str " r = Run up to next idtac " ++ fnl() ++ - str " s = Skip" ++ fnl() ++ - str " x = Exit") - -(* Prints the goal and the command to be executed *) -let goal_com tac = - Proofview.tclTHEN - db_pr_goal - (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac))) - -(* [run (new_ref _)] gives us a ref shared among [NonLogical.t] - expressions. It avoids parametrizing everything over a - reference. *) -let skipped = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) -let skip = Proofview.NonLogical.run (Proofview.NonLogical.ref 0) -let breakpoint = Proofview.NonLogical.run (Proofview.NonLogical.ref None) - -let rec drop_spaces inst i = - if String.length inst > i && inst.[i] == ' ' then drop_spaces inst (i+1) - else i - -let possibly_unquote s = - if String.length s >= 2 && s.[0] == '"' && s.[String.length s - 1] == '"' then - String.sub s 1 (String.length s - 2) - else - s - -(* (Re-)initialize debugger *) -let db_initialize = - let open Proofview.NonLogical in - (skip:=0) >> (skipped:=0) >> (breakpoint:=None) - -let int_of_string s = - try Proofview.NonLogical.return (int_of_string s) - with e -> Proofview.NonLogical.raise e - -let string_get s i = - try Proofview.NonLogical.return (String.get s i) - with e -> Proofview.NonLogical.raise e - -(* Gives the number of steps or next breakpoint of a run command *) -let run_com inst = - let open Proofview.NonLogical in - string_get inst 0 >>= fun first_char -> - if first_char ='r' then - let i = drop_spaces inst 1 in - if String.length inst > i then - let s = String.sub inst i (String.length inst - i) in - if inst.[0] >= '0' && inst.[0] <= '9' then - int_of_string s >>= fun num -> - (if num<0 then invalid_arg "run_com" else return ()) >> - (skip:=num) >> (skipped:=0) - else - breakpoint:=Some (possibly_unquote s) - else - invalid_arg "run_com" - else - invalid_arg "run_com" - -(* Prints the run counter *) -let run ini = - let open Proofview.NonLogical in - if not ini then - begin - Proofview.NonLogical.print_notice (str"\b\r\b\r") >> - !skipped >>= fun skipped -> - msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl()) - end >> - !skipped >>= fun x -> - skipped := x+1 - else - return () - -(* Prints the prompt *) -let rec prompt level = - (* spiwack: avoid overriding by the open below *) - let runtrue = run true in - begin - let open Proofview.NonLogical in - Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> - let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in - Proofview.NonLogical.catch Proofview.NonLogical.read_line - begin function (e, info) -> match e with - | End_of_file -> exit - | e -> raise ~info e - end - >>= fun inst -> - match inst with - | "" -> return (DebugOn (level+1)) - | "s" -> return (DebugOff) - | "x" -> Proofview.NonLogical.print_char '\b' >> exit - | "h"| "?" -> - begin - help () >> - prompt level - end - | _ -> - Proofview.NonLogical.catch (run_com inst >> runtrue >> return (DebugOn (level+1))) - begin function (e, info) -> match e with - | Failure _ | Invalid_argument _ -> prompt level - | e -> raise ~info e - end - end - -(* Prints the state and waits for an instruction *) -(* spiwack: the only reason why we need to take the continuation [f] - as an argument rather than returning the new level directly seems to - be that [f] is wrapped in with "explain_logic_error". I don't think - it serves any purpose in the current design, so we could just drop - that. *) -let debug_prompt lev tac f = - (* spiwack: avoid overriding by the open below *) - let runfalse = run false in - let open Proofview.NonLogical in - let (>=) = Proofview.tclBIND in - (* What to print and to do next *) - let newlevel = - Proofview.tclLIFT !skip >= fun initial_skip -> - if Int.equal initial_skip 0 then - Proofview.tclLIFT !breakpoint >= fun breakpoint -> - if Option.is_empty breakpoint then Proofview.tclTHEN (goal_com tac) (Proofview.tclLIFT (prompt lev)) - else Proofview.tclLIFT(runfalse >> return (DebugOn (lev+1))) - else Proofview.tclLIFT begin - (!skip >>= fun s -> skip:=s-1) >> - runfalse >> - !skip >>= fun new_skip -> - (if Int.equal new_skip 0 then skipped:=0 else return ()) >> - return (DebugOn (lev+1)) - end in - newlevel >= fun newlevel -> - (* What to execute *) - Proofview.tclOR - (f newlevel) - begin fun (reraise, info) -> - Proofview.tclTHEN - (Proofview.tclLIFT begin - (skip:=0) >> (skipped:=0) >> - if Logic.catchable_exception reraise then - msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise) - else return () - end) - (Proofview.tclZERO ~info reraise) - end - -let is_debug db = - let open Proofview.NonLogical in - !breakpoint >>= fun breakpoint -> - match db, breakpoint with - | DebugOff, _ -> return false - | _, Some _ -> return false - | _ -> - !skip >>= fun skip -> - return (Int.equal skip 0) - -(* Prints a constr *) -let db_constr debug env c = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c) - else return () - -(* Prints the pattern rule *) -let db_pattern_rule debug num r = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - begin - msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++ - str "|" ++ spc () ++ Hook.get prmatchrl r) - end - else return () - -(* Prints the hypothesis pattern identifier if it exists *) -let hyp_bound = function - | Anonymous -> str " (unbound)" - | Name id -> str " (bound to " ++ pr_id id ++ str ")" - -(* Prints a matched hypothesis *) -let db_matched_hyp debug env (id,_,c) ido = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env c) - else return () - -(* Prints the matched conclusion *) -let db_matched_concl debug env c = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c) - else return () - -(* Prints a success message when the goal has been matched *) -let db_mc_pattern_success debug = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "The goal has been successfully matched!" ++ fnl() ++ - str "Let us execute the right-hand side part..." ++ fnl()) - else return () - -(* Prints a failure message for an hypothesis pattern *) -let db_hyp_pattern_failure debug env sigma (na,hyp) = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++ - str " cannot match: " ++ - Hook.get prmatchpatt env sigma hyp) - else return () - -(* Prints a matching failure message for a rule *) -let db_matching_failure debug = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - msg_tac_debug (str "This rule has failed due to matching errors!" ++ fnl() ++ - str "Let us try the next one...") - else return () - -(* Prints an evaluation failure message for a rule *) -let db_eval_failure debug s = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - let s = str "message \"" ++ s ++ str "\"" in - msg_tac_debug - (str "This rule has failed due to \"Fail\" tactic (" ++ - s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...") - else return () - -(* Prints a logic failure message for a rule *) -let db_logic_failure debug err = - let open Proofview.NonLogical in - is_debug debug >>= fun db -> - if db then - begin - msg_tac_debug (Pervasives.(!) explain_logic_error err) >> - msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++ - str "Let us try the next one...") - end - else return () - -let is_breakpoint brkname s = match brkname, s with - | Some s, MsgString s'::_ -> String.equal s s' - | _ -> false - -let db_breakpoint debug s = - let open Proofview.NonLogical in - !breakpoint >>= fun opt_breakpoint -> - match debug with - | DebugOn lev when not (CList.is_empty s) && is_breakpoint opt_breakpoint s -> - breakpoint:=None - | _ -> - return () diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli deleted file mode 100644 index 215c5b29..00000000 --- a/proofs/tactic_debug.mli +++ /dev/null @@ -1,79 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Pp.std_ppcmds) Hook.t -val match_pattern_printer : - (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t -val match_rule_printer : - ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t - -(** Debug information *) -type debug_info = - | DebugOn of int - | DebugOff - -(** Prints the state and waits *) -val debug_prompt : - int -> glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic - -(** Initializes debugger *) -val db_initialize : unit Proofview.NonLogical.t - -(** Prints a constr *) -val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t - -(** Prints the pattern rule *) -val db_pattern_rule : - debug_info -> int -> (Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t - -(** Prints a matched hypothesis *) -val db_matched_hyp : - debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t - -(** Prints the matched conclusion *) -val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t - -(** Prints a success message when the goal has been matched *) -val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t - -(** Prints a failure message for an hypothesis pattern *) -val db_hyp_pattern_failure : - debug_info -> env -> evar_map -> Name.t * constr_pattern match_pattern -> unit Proofview.NonLogical.t - -(** Prints a matching failure message for a rule *) -val db_matching_failure : debug_info -> unit Proofview.NonLogical.t - -(** Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t - -(** An exception handler *) -val explain_logic_error: (exn -> Pp.std_ppcmds) ref - -(** For use in the Ltac debugger: some exception that are usually - consider anomalies are acceptable because they are caught later in - the process that is being debugged. One should not require - from users that they report these anomalies. *) -val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref - -(** Prints a logic failure message for a rule *) -val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t - -(** Prints a logic failure message for a rule *) -val db_breakpoint : debug_info -> - Id.t Loc.located message_token list -> unit Proofview.NonLogical.t -- cgit v1.2.3