diff options
Diffstat (limited to 'plugins')
33 files changed, 667 insertions, 489 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f09b35a6d1..e5665c59b8 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -40,7 +40,7 @@ let start_deriving f suchthat name : Lemmas.t = TNil sigma)))))) in - let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in + let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in Lemmas.pf_map (Declare.Proof.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index f7d78551d8..a0627dbe63 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -581,7 +581,7 @@ let rec locate_ref = function with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found qid + | None, None -> Nametab.error_global_not_found ~info:Exninfo.null qid | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index afc83b780b..0f96b9bbe8 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -259,7 +259,7 @@ let parse_ind_args si args relmax = let rec extract_type env sg db j c args = - match EConstr.kind sg (whd_betaiotazeta sg c) with + match EConstr.kind sg (whd_betaiotazeta env sg c) with | App (d, args') -> (* We just accumulate the arguments. *) extract_type env sg db j d (Array.to_list args' @ args) @@ -380,7 +380,7 @@ and extract_type_app env sg db (r,s) args = and extract_type_scheme env sg db c p = if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta sg c in + let c = whd_betaiotazeta env sg c in match EConstr.kind sg c with | Lambda (n,t,d) -> extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 834e4251d3..f13901c36d 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -57,12 +57,12 @@ let make_simple_atoms seq= | None->[] in {negative=seq.latoms;positive=ratoms} -let do_sequent sigma setref triv id seq i dom atoms= +let do_sequent env sigma setref triv id seq i dom atoms= let flag=ref true in let phref=ref triv in let do_atoms a1 a2 = let do_pair t1 t2 = - match unif_atoms sigma i dom t1 t2 with + match unif_atoms env sigma i dom t1 t2 with None->() | Some (Phantom _) ->phref:=true | Some c ->flag:=false;setref:=IS.add (c,id) !setref in @@ -72,16 +72,16 @@ let do_sequent sigma setref triv id seq i dom atoms= do_atoms atoms (make_simple_atoms seq); !flag && !phref -let match_one_quantified_hyp sigma setref seq lf= +let match_one_quantified_hyp env sigma setref seq lf= match lf.pat with Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))-> - if do_sequent sigma setref triv lf.id seq i dom lf.atoms then + if do_sequent env sigma setref triv lf.id seq i dom lf.atoms then setref:=IS.add ((Phantom dom),lf.id) !setref | _ -> anomaly (Pp.str "can't happen.") -let give_instances sigma lf seq= +let give_instances env sigma lf seq= let setref=ref IS.empty in - List.iter (match_one_quantified_hyp sigma setref seq) lf; + List.iter (match_one_quantified_hyp env sigma setref seq) lf; IS.elements !setref (* collector for the engine *) @@ -129,9 +129,10 @@ let left_instance_tac (inst,id) continue seq= let open EConstr in Proofview.Goal.enter begin fun gl -> let sigma = project gl in + let env = Proofview.Goal.env gl in match inst with Phantom dom-> - if lookup sigma (id,None) seq then + if lookup env sigma (id,None) seq then tclFAIL 0 (Pp.str "already done") else tclTHENS (cut dom) @@ -148,7 +149,7 @@ let left_instance_tac (inst,id) continue seq= tclTRY assumption] | Real((m,t),_)-> let c = (m, EConstr.to_constr sigma t) in - if lookup sigma (id,Some c) seq then + if lookup env sigma (id,Some c) seq then tclFAIL 0 (Pp.str "already done") else let special_generalize= @@ -205,7 +206,8 @@ let instance_tac inst= let quantified_tac lf backtrack continue seq = Proofview.Goal.enter begin fun gl -> - let insts=give_instances (project gl) lf seq in + let env = Proofview.Goal.env gl in + let insts=give_instances env (project gl) lf seq in tclORELSE (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts)) backtrack diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index c0f4c78ff3..08c2c4d916 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -13,7 +13,7 @@ open Rules val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t -val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t -> +val give_instances : Environ.env -> Evd.evar_map -> Formula.t list -> Sequent.t -> (Unify.instance * GlobRef.t) list val quantified_tac : Formula.t list -> seqtac with_backtracking diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7bf13fd25b..3dd5059e5d 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -109,7 +109,7 @@ let deepen seq={seq with depth=seq.depth-1} let record item seq={seq with history=History.add item seq.history} -let lookup sigma item seq= +let lookup env sigma item seq= History.mem item seq.history || match item with (_,None)->false @@ -117,7 +117,7 @@ let lookup sigma item seq= let p (id2,o)= match o with None -> false - | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in + | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general env sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in History.exists p seq.history let add_formula env sigma side nam t seq = diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 3a5da6ad14..bba89c823c 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -39,7 +39,7 @@ val deepen: t -> t val record: h_item -> t -> t -val lookup: Evd.evar_map -> h_item -> t -> bool +val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index e58e80116d..9c3debe48f 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -29,7 +29,7 @@ let subst_meta subst t = let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t)) -let unif evd t1 t2= +let unif env evd t1 t2= let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -46,8 +46,8 @@ let unif evd t1 t2= Queue.add (t1,t2) bige; try while true do let t1,t2=Queue.take bige in - let nt1=head_reduce (whd_betaiotazeta evd t1) - and nt2=head_reduce (whd_betaiotazeta evd t2) in + let nt1=head_reduce (whd_betaiotazeta env evd t1) + and nt2=head_reduce (whd_betaiotazeta env evd t2) in match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with Meta i,Meta j-> if not (Int.equal i j) then @@ -123,9 +123,9 @@ let mk_rel_inst evd t= in let nt=renum_rec 0 t in (!new_rel - 1,nt) -let unif_atoms evd i dom t1 t2= +let unif_atoms env evd i dom t1 t2= try - let t=Int.List.assoc i (unif evd t1 t2) in + let t=Int.List.assoc i (unif env evd t1 t2) in if isMeta evd t then Some (Phantom dom) else Some (Real(mk_rel_inst evd t,value evd i t1)) with @@ -136,11 +136,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *) let l=List.init n (fun i->mkMeta (k+i)) in substl l t -let more_general evd (m1,t1) (m2,t2)= +let more_general env evd (m1,t1) (m2,t2)= let mt1=renum_metas_from 0 m1 t1 and mt2=renum_metas_from m1 m2 t2 in try - let sigma=unif evd mt1 mt2 in + let sigma=unif env evd mt1 mt2 in let p (n,t)= n<m1 || isMeta evd t in List.for_all p sigma with UFAIL(_,_)->false diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index 71e786eb90..c6767f04ac 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -13,12 +13,12 @@ open EConstr exception UFAIL of constr*constr -val unif : Evd.evar_map -> constr -> constr -> (int*constr) list +val unif : Environ.env -> Evd.evar_map -> constr -> constr -> (int*constr) list type instance= Real of (int*constr)*int (* nb trous*terme*valeur heuristique *) | Phantom of constr (* domaine de quantification *) -val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option +val unif_atoms : Environ.env -> Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option -val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool +val more_general : Environ.env -> Evd.evar_map -> (int*constr) -> (int*constr) -> bool diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 49fc513dd2..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) = refine to_refine g) ] let find_rectype env sigma c = - let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in + let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in match EConstr.kind sigma t with | Ind ind -> (t, l) | Construct _ -> (t, l) diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 68e1087b74..a1094e39a4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -18,6 +18,7 @@ open Indfun_common open Indfun open Stdarg open Tacarg +open Extraargs open Tactypes open Pcoq.Prim open Pcoq.Constr @@ -96,14 +97,12 @@ let functional_induction b c x pat = } TACTIC EXTEND newfunind -| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - { - let c = match cl with - | [] -> assert false - | [c] -> c - | c::cl -> EConstr.applist(c,cl) - in - Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl } +| ["functional" "induction" lconstr(c) fun_ind_using(princl) with_names(pat)] -> + { + (Extratactics.onSomeWithHoles + (fun x -> functional_induction true c x pat) princl) + } + END (***** debug only ***) TACTIC EXTEND snewfunind diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 0f0341f123..35c90444b1 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -54,16 +54,23 @@ END { +let pr_search_strategy_name _prc _prlc _prt = function + | Dfs -> Pp.str "dfs" + | Bfs -> Pp.str "bfs" + let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" + | Some s -> pr_search_strategy_name _prc _prlc _prt s | None -> Pp.mt () } +ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name } +| [ "bfs" ] -> { Bfs } +| [ "dfs" ] -> { Dfs } +END + ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } -| [ "(bfs)" ] -> { Some Bfs } -| [ "(dfs)" ] -> { Some Dfs } +| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s } | [ ] -> { None } END @@ -135,7 +142,9 @@ let progress_evars t = let sigma = Tacmach.New.project gl' in let newconcl = Proofview.Goal.concl gl' in if eq_constr_mod_evars sigma concl newconcl - then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") + then + let info = Exninfo.reify () in + Tacticals.New.tclFAIL ~info 0 (Pp.str"No progress made (modulo evars)") else Proofview.tclUNIT () end in t <*> check diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index aef5f645f4..0e661543db 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram ; match_key: [ [ "match" -> { Once } - | "lazymatch" -> { Select } - | "multimatch" -> { General } ] ] + | IDENT "lazymatch" -> { Select } + | IDENT "multimatch" -> { General } ] ] ; input_fun: [ [ "_" -> { Name.Anonymous } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 6a158bde17..e51b1f051d 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -30,9 +30,6 @@ open Pcoq let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] -let tactic_kw = [ "->"; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw - let err () = raise Stream.Failure (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3b8fb48eb0..4bc8d61258 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite." let rec decompose_app_rel env evd t = (* Head normalize for compatibility with the old meta mechanism *) - let t = Reductionops.whd_betaiota evd t in + let t = Reductionops.whd_betaiota env evd t in match EConstr.kind evd t with | App (f, [||]) -> assert false | App (f, [|arg|]) -> @@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs) let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs) ~fail:true env sigma in let evd = solve_remaining_by env sigma holes by in - let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in + let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in let c1 = nf c1 and c2 = nf c2 and rew_car = nf car and rel = nf rel and prf = nf prf in @@ -971,7 +971,7 @@ let unfold_match env sigma sk app = | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in - Reductionops.whd_beta sigma (mkApp (v, args)) + Reductionops.whd_beta env sigma (mkApp (v, args)) | _ -> app let is_rew_cast = function RewCast _ -> true | _ -> false @@ -1566,7 +1566,8 @@ let assert_replacing id newt tac = Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) let newfail n s = - Proofview.tclZERO (Refiner.FailError (n, lazy s)) + let info = Exninfo.reify () in + Proofview.tclZERO ~info (Refiner.FailError (n, lazy s)) let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in @@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let treat sigma res = match res with | None -> newfail 0 (str "Nothing to rewrite") - | Some None -> if progress then newfail 0 (str"Failed to progress") - else Proofview.tclUNIT () + | Some None -> + if progress + then newfail 0 (str"Failed to progress") + else Proofview.tclUNIT () | Some (Some res) -> let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in @@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let tactic_init_setoid () = try init_setoid (); Proofview.tclUNIT () - with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded") + with e when CErrors.noncritical e -> + let _, info = Exninfo.capture e in + Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded") let cl_rewrite_clause_strat progress strat clause = tactic_init_setoid () <*> @@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause = (cl_rewrite_clause_newtac ~progress strat clause) (fun (e, info) -> match e with | RewriteFailure e -> - tclZEROMSG (str"setoid rewrite failed: " ++ e) + tclZEROMSG ~info (str"setoid rewrite failed: " ++ e) | Refiner.FailError (n, pp) -> - tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) - | e -> Proofview.tclZERO ~info e)) + tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) + | e -> + Proofview.tclZERO ~info e)) (** Setoid rewriting when called with "setoid_rewrite" *) let cl_rewrite_clause l left2right occs clause = @@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals = (cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl))) (fun (e, info) -> match e with | RewriteFailure e -> - tclFAIL 0 (str"setoid rewrite failed: " ++ e) + tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e) | e -> Proofview.tclZERO ~info e) end @@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) -let not_declared env sigma ty rel = - tclFAIL 0 +let not_declared ~info env sigma ty rel = + tclFAIL ~info 0 (str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") @@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback = let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel - with e -> Proofview.tclZERO e + with e -> + (* XXX what is the right test here as to whether e can be converted ? *) + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e end begin function | e -> @@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback = | Hipattern.NoEquationFound -> begin match e with | (Not_found, _) -> - let rel, _, _ = decompose_app_rel env sigma concl in - not_declared env sigma ty rel - | (e, info) -> Proofview.tclZERO ~info e + let rel, _, _ = decompose_app_rel env sigma concl in + not_declared ~info env sigma ty rel + | (e, info) -> + Proofview.tclZERO ~info e end | e' -> Proofview.tclZERO ~info e' end diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 1aa3af0087..bcfdb5318e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -14,7 +14,6 @@ open CAst open Pattern open Genredexpr open Glob_term -open Tacred open Util open Names open Libnames @@ -98,13 +97,19 @@ let intern_global_reference ist qid = else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then let id = qualid_basename qid in ArgArg (qid.CAst.loc, GlobRef.VarRef id) - else match locate_global_with_alias qid with - | r -> ArgArg (qid.CAst.loc, r) - | exception Not_found -> - if not !strict_check && qualid_is_ident qid then - let id = qualid_basename qid in - ArgArg (qid.CAst.loc, GlobRef.VarRef id) - else Nametab.error_global_not_found qid + else + let r = + try locate_global_with_alias ~head:true qid + with + | Not_found as exn -> + if not !strict_check && qualid_is_ident qid then + let id = qualid_basename qid in + GlobRef.VarRef id + else + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid + in + ArgArg (qid.CAst.loc, r) let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -149,9 +154,10 @@ let intern_isolated_tactic_reference strict ist qid = with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) - with Not_found -> - (* Reference not found *) - Nametab.error_global_not_found qid + with Not_found as exn -> + (* Reference not found *) + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid (* Internalize an applied tactic reference *) @@ -168,9 +174,10 @@ let intern_applied_tactic_reference ist qid = with Not_found -> (* A global tactic *) try intern_applied_global_tactic_reference qid - with Not_found -> - (* Reference not found *) - Nametab.error_global_not_found qid + with Not_found as exn -> + (* Reference not found *) + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid (* Intern a reference parsed in a non-tactic entry *) @@ -183,7 +190,7 @@ let intern_non_tactic_reference strict ist qid = with Not_found -> (* Tolerance for compatibility, allow not to use "ltac:" *) try intern_isolated_global_tactic_reference qid - with Not_found -> + with Not_found as exn -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) if qualid_is_ident qid && not strict then let id = qualid_basename qid in @@ -191,7 +198,8 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - Nametab.error_global_not_found qid + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -294,45 +302,43 @@ let intern_destruction_arg ist = function else clear,ElimOnIdent (make ?loc id) -let short_name = function - | {v=AN qid} when qualid_is_ident qid && not !strict_check -> +let short_name qid = + if qualid_is_ident qid && not !strict_check then Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) - | _ -> None - -let intern_evaluable_global_reference ist qid = - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) - with Not_found -> - if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else Nametab.error_global_not_found qid - -let intern_evaluable_reference_or_by_notation ist = function - | {v=AN r} -> intern_evaluable_global_reference ist r + else None + +let evalref_of_globref ?loc ?short = function + | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short) + | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short) + | r -> + let tpe = match r with + | GlobRef.IndRef _ -> "inductive" + | GlobRef.ConstructRef _ -> "constructor" + | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false + in + user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++ + Nametab.pr_global_env Id.Set.empty r ++ spc () ++ + str "into an evaluable reference.") + +let intern_evaluable ist = function + | {v=AN qid} -> + begin match intern_global_reference ist qid with + | ArgVar _ as v -> v + | ArgArg (loc, r) -> + let short = short_name qid in + evalref_of_globref ?loc ?short r + end | {v=ByNotation (ntn,sc);loc} -> - evaluable_of_global_reference ist.genv - (Notation.interp_notation_as_global_reference ?loc - GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) + let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in + let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in + evalref_of_globref ?loc r let intern_smart_global ist = function | {v=AN r} -> intern_global_reference ist r | {v=ByNotation (ntn,sc);loc} -> - ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc + ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)) -(* Globalize a reduction expression *) -let intern_evaluable ist r = - let f ist r = - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) - in - match r with - | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> - ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) - | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> - let id = qualid_basename qid in - ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) - | _ -> f ist r - let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) let intern_flag ist red = @@ -393,10 +399,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = let c = Constrintern.interp_reference sign r in match DAst.get c with | GRef (r,None) -> - Inl (ArgArg (evaluable_of_global_reference ist.genv r,None)) + Inl (evalref_of_globref r) | GVar id -> - let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in - Inl (ArgArg (r,None)) + let r = evalref_of_globref (GlobRef.VarRef id) in + Inl r | _ -> let bound_names = Glob_ops.bound_glob_vars c in Inr (bound_names,(c,None),dummy_pat) in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6d350ade8d..97f7a198e6 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -378,7 +378,9 @@ let interp_reference ist env sigma = function with Not_found -> try GlobRef.VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -391,17 +393,21 @@ let interp_evaluable ist env sigma = function (* Maybe [id] has been introduced by Intro-like tactics *) begin try try_interp_evaluable env (loc, id) - with Not_found -> + with Not_found as exn -> match r with | EvalConstRef _ -> r - | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) + | _ -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -663,8 +669,9 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let c = coerce_to_closed_constr env x in Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) - with Not_found -> - Nametab.error_global_not_found (qualid_of_ident ?loc id)) + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -774,7 +781,9 @@ let interp_message_token ist = function | MsgIdent {loc;v=id} -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with - | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) + | None -> Ftactic.lift ( + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (Id.print id ++ str" not found.")) | Some v -> message_of_value v let interp_message ist l = @@ -1087,11 +1096,15 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end | TacFail (g,n,s) -> let msg = interp_message ist s in - let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in + let tac ~info l = Tacticals.New.tclFAIL ~info (interp_int_or_var ist n) l in let tac = match g with - | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l) - | TacGlobal -> tac + | TacLocal -> + let info = Exninfo.reify () in + fun l -> Proofview.tclINDEPENDENT (tac ~info l) + | TacGlobal -> + let info = Exninfo.reify () in + tac ~info in Ftactic.run msg tac | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) @@ -1174,8 +1187,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let len1 = List.length alias.Tacenv.alias_args in let len2 = List.length l in if len1 = len2 then tac - else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \ - expected " ++ int len1 ++ str ", found " ++ int len2) + else + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info + (str "Arguments length mismatch: \ + expected " ++ int len1 ++ str ", found " ++ int len2) in Ftactic.run tac (fun () -> Proofview.tclUNIT ()) @@ -1267,7 +1283,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t = and interp_app loc ist fv largs : Val.t Ftactic.t = Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let (>>=) = Ftactic.bind in - let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in + let fail ~info = Tacticals.New.tclZEROMSG ~info (str "Illegal tactic application.") in if has_type fv (topwit wit_tacvalue) then match to_tacvalue fv with (* if var=[] and body has been delayed by val_interp, then body @@ -1313,12 +1329,18 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body))) | (VFun(appl,trace,olfun,[],body)) -> let extra_args = List.length largs in - Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++ - str (string_of_int extra_args) ++ - str " extra " ++ str (String.plural extra_args "argument") ++ - str ".") - | VRec(_,_) -> fail - else fail + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info + (str "Illegal tactic application: got " ++ + str (string_of_int extra_args) ++ + str " extra " ++ str (String.plural extra_args "argument") ++ + str ".") + | VRec(_,_) -> + let info = Exninfo.reify () in + fail ~info + else + let info = Exninfo.reify () in + fail ~info (* Gives the tactic corresponding to the tactic value *) and tactic_of_value ist vle = @@ -1346,7 +1368,8 @@ and tactic_of_value ist vle = let givenargs = List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in let numgiven = List.length givenargs in - Tacticals.New.tclZEROMSG + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++ (match numargs with 0 -> assert false @@ -1364,11 +1387,15 @@ and tactic_of_value ist vle = | _ -> Pp.str "arguments were provided for variables " ++ pr_enum Pp.str givenargs ++ Pp.str ".") - | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") + | VRec _ -> + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in tactic_of_value ist tac - else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.") + else + let info = Exninfo.reify () in + Tacticals.New.tclZEROMSG ~info (str "Expression does not evaluate to a tactic.") (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist llc u = @@ -1562,10 +1589,12 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t = pr_econstr_env env sigma cresult) end <*> Ftactic.return cresult - with CannotCoerceTo _ -> + with CannotCoerceTo _ as exn -> + let _, info = Exninfo.capture exn in let env = Proofview.Goal.env gl in - Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++ - str "offending expression: " ++ fnl() ++ pr_inspect env e result) + Tacticals.New.tclZEROMSG ~info + (str "Must evaluate to a closed term" ++ fnl() ++ + str "offending expression: " ++ fnl() ++ pr_inspect env e result) end diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 525199735d..2b43b11fe1 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -186,7 +186,9 @@ module PatternMatching (E:StaticEnvironment) = struct { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx } (** Failure of the pattern-matching monad: no success. *) - let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error } + let fail (type a) : a m = { stream = fun _ _ -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info matching_error } let run (m : 'a m) = let ctx = { @@ -209,7 +211,11 @@ module PatternMatching (E:StaticEnvironment) = struct (** Declares a substitution, a context substitution and a term substitution. *) let put subst context terms : unit m = let s = { subst ; context ; terms ; lhs = () } in - { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s } + { stream = fun k ctx -> match merge s ctx with + | None -> + let info = Exninfo.reify () in + Proofview.tclZERO ~info matching_error + | Some s -> k () s } (** Declares a substitution. *) let put_subst subst : unit m = put subst empty_context_subst empty_term_subst diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ee2c87d19a..0f8d941b41 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1897,8 +1897,6 @@ type provername = string * int option * The caching mechanism. *) -open Persistent_cache - module MakeCache (T : sig type prover_option type coeff @@ -1922,7 +1920,7 @@ struct Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0) end - include PHashtable (E) + include Persistent_cache.PHashtable (E) let memo_opt use_cache cache_file f = let memof = memo cache_file f in diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 9051bbb5ca..3360a9a51c 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -93,9 +93,9 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct there is a pending lock which could cause a deadlock. Should it be an anomaly or produce a warning ? *) - () + ignore (lseek fd pos SEEK_SET) in - ignore (lseek fd pos SEEK_SET) + () (* We make the assumption that an acquired lock can always be released *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 79d6c05e1d..3ba6365783 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1475,7 +1475,9 @@ let coq_omega = let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system") + with NO_CONTRADICTION as e -> + let _, info = Exninfo.capture e in + tclZEROMSG ~info (Pp.str"Omega can't solve this system") end end @@ -1890,7 +1892,9 @@ let destructure_goal = end) intro with Undecidable -> Tactics.elim_type (Lazy.force coq_False) - | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e + | e when Proofview.V82.catchable_exception e -> + let e, info = Exninfo.capture e in + Proofview.tclZERO ~info e in tclTHEN goal_tac destructure_hyps in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e8257b5dba..01e8daf82d 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -950,7 +950,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_ let open EConstr in if n = 0 then let args = List.rev args in - (if beta then Reductionops.whd_beta sigma else fun x -> x) + (if beta then Reductionops.whd_beta env sigma else fun x -> x) (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma else match kind_of_type sigma ty with | ProdType (_, src, tgt) -> @@ -1065,11 +1065,12 @@ end let introid ?(orig=ref Anonymous) name = let open Proofview.Notations in Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let g = Proofview.Goal.concl gl in match EConstr.kind sigma g with | App (hd, _) when EConstr.isLambda sigma hd -> - convert_concl_no_check (Reductionops.whd_beta sigma g) + convert_concl_no_check (Reductionops.whd_beta env sigma g) | _ -> Tacticals.New.tclIDTAC end <*> (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name)) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index ab07dd5be9..29a9c65561 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -281,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) = | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) | Proj _ when same_proj sigma0 c t -> body env t c | _ -> - let c = Reductionops.whd_betaiotazeta sigma0 c in + let c = Reductionops.whd_betaiotazeta env sigma0 c in match EConstr.kind sigma0 c with | Const _ when EConstr.eq_constr sigma0 c t -> body env t t | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a) @@ -516,7 +516,7 @@ let rwprocess_rule env dir rule = let rec loop d sigma r t0 rs red = let t = if red = 1 then Tacred.hnf_constr env sigma t0 - else Reductionops.whd_betaiotazeta sigma t0 in + else Reductionops.whd_betaiotazeta env sigma t0 in ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4b78e64d98..24772a8514 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -15,7 +15,6 @@ open Names module CoqConstr = Constr open CoqConstr -open Termops open Constrexpr open Constrexpr_ops open Pcoq @@ -23,8 +22,6 @@ open Pcoq.Prim open Pcoq.Constr open Pvernac.Vernac_ open Ltac_plugin -open Notation_ops -open Notation_term open Glob_term open Stdarg open Pp @@ -32,10 +29,8 @@ open Ppconstr open Printer open Util open Extraargs -open Evar_kinds open Ssrprinters open Ssrcommon -open Ssrparser } @@ -129,7 +124,7 @@ GRAMMAR EXTEND Gram ] ]; END -(** Vernacular commands: Prenex Implicits and Search *)(***********************) +(** Vernacular commands: Prenex Implicits *) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -187,298 +182,6 @@ GRAMMAR EXTEND Gram ; END -(** Extend Search to subsume SearchAbout, also adding hidden Type coercions. *) - -(* Main prefilter *) - -{ - -type raw_glob_search_about_item = - | RGlobSearchSubPattern of constr_expr - | RGlobSearchString of Loc.t * string * string option - -let pr_search_item env sigma = function - | RGlobSearchString (_,s,_) -> str s - | RGlobSearchSubPattern p -> pr_constr_expr env sigma p - -let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item - -let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma - -(* Workaround the notation API that can only print notations *) - -let is_ident s = try CLexer.check_ident s; true with _ -> false - -let is_ident_part s = is_ident ("H" ^ s) - -let interp_search_notation ?loc tag okey = - let err msg = CErrors.user_err ?loc ~hdr:"interp_search_notation" msg in - let mk_pntn s for_key = - let n = String.length s in - let s' = Bytes.make (n + 2) ' ' in - let rec loop i i' = - if i >= n then s', i' - 2 else if s.[i] = ' ' then loop (i + 1) i' else - let j = try String.index_from s (i + 1) ' ' with _ -> n in - let m = j - i in - if s.[i] = '\'' && i < j - 2 && s.[j - 1] = '\'' then - (String.blit s (i + 1) s' i' (m - 2); loop (j + 1) (i' + m - 1)) - else if for_key && is_ident (String.sub s i m) then - (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) - else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in - loop 0 1 in - let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in - let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in - let pr_and_list pr = function - | [x] -> pr x - | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x - | [] -> mt () in - let pr_sc sc = str (if sc = "" then "independently" else sc) in - let pr_scs = function - | [""] -> pr_sc "" - | scs -> str "in " ++ pr_and_list pr_sc scs in - let generator, pr_tag_sc = - let ign _ = mt () in match okey with - | Some key -> - let sc = Notation.find_delimiters_scope ?loc key in - let pr_sc s_in = str s_in ++ spc() ++ str sc ++ pr_comma() in - Notation.pr_scope ign sc, pr_sc - | None -> Notation.pr_scopes ign, ign in - let qtag s_in = pr_tag_sc s_in ++ qstring tag ++ spc()in - let ptag, ttag = - let ptag, m = mk_pntn tag false in - if m <= 0 then err (str "empty notation fragment"); - ptag, trim_ntn (ptag, m) in - let last = ref "" and last_sc = ref "" in - let scs = ref [] and ntns = ref [] in - let push_sc sc = match !scs with - | "" :: scs' -> scs := "" :: sc :: scs' - | scs' -> scs := sc :: scs' in - let get s _ _ = match !last with - | "Scope " -> last_sc := s; last := "" - | "Lonely notation" -> last_sc := ""; last := "" - | "\"" -> - let pntn, m = mk_pntn s true in - if String.string_contains ~where:(Bytes.to_string pntn) ~what:(Bytes.to_string ptag) then begin - let ntn = trim_ntn (pntn, m) in - match !ntns with - | [] -> ntns := [ntn]; scs := [!last_sc] - | ntn' :: _ when ntn' = ntn -> push_sc !last_sc - | _ when ntn = ttag -> ntns := ntn :: !ntns; scs := [!last_sc] - | _ :: ntns' when List.mem ntn ntns' -> () - | ntn' :: ntns' -> ntns := ntn' :: ntn :: ntns' - end; - last := "" - | _ -> last := s in - pp_with (Format.make_formatter get (fun _ -> ())) generator; - let ntn = match !ntns with - | [] -> - err (hov 0 (qtag "in" ++ str "does not occur in any notation")) - | ntn :: ntns' when ntn = ttag -> - if ntns' <> [] then begin - let pr_ntns' = pr_and_list pr_ntn ntns' in - Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns')) - end; ntn - | [ntn] -> - Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn - | ntns' -> - let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in - err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in - let (nvars, body), ((_, pat), osc) = match !scs with - | [sc] -> Notation.interp_notation ?loc ntn (None, [sc]) - | scs' -> - try Notation.interp_notation ?loc ntn (None, []) with _ -> - let e = pr_ntn ntn ++ spc() ++ str "is defined " ++ pr_scs scs' in - err (hov 4 (str "ambiguous: " ++ pr_tag_sc "in" ++ e)) in - let sc = Option.default "" osc in - let _ = - let m_sc = - if osc <> None then str "In " ++ str sc ++ pr_comma() else mt() in - let ntn_pat = trim_ntn (mk_pntn pat false) in - let rbody = glob_constr_of_notation_constr ?loc body in - let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in - let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in - Feedback.msg_notice (hov 0 m) in - if List.length !scs > 1 then - let scs' = List.remove (=) sc !scs in - let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in - Feedback.msg_warning (hov 4 w) - else if String.string_contains ~where:(snd ntn) ~what:" .. " then - err (pr_ntn ntn ++ str " is an n-ary notation"); - let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in - let rec sub () = function - | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x) - | c -> - glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in - let _, npat = Patternops.pattern_of_glob_constr (sub () body) in - Search.GlobSearchSubPattern npat - -} - -ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem - PRINTED BY { pr_ssr_search_item env sigma } - | [ string(s) ] -> { RGlobSearchString (loc,s,None) } - | [ string(s) "%" preident(key) ] -> { RGlobSearchString (loc,s,Some key) } - | [ constr_pattern(p) ] -> { RGlobSearchSubPattern p } -END - -{ - -let pr_ssr_search_arg env sigma _ _ _ = - let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in - pr_list spc pr_item - -} - -ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list - PRINTED BY { pr_ssr_search_arg env sigma } - | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> { (false, p) :: a } - | [ ssr_search_item(p) ssr_search_arg(a) ] -> { (true, p) :: a } - | [ ] -> { [] } -END - -{ - -(* Main type conclusion pattern filter *) - -let rec splay_search_pattern na = function - | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp - | Pattern.PLetIn (_, _, _, bp) -> splay_search_pattern na bp - | Pattern.PRef hr -> hr, na - | _ -> CErrors.user_err (Pp.str "no head constant in head search pattern") - -let push_rels_assum l e = - let l = List.map (fun (n,t) -> n, EConstr.Unsafe.to_constr t) l in - push_rels_assum l e - -let coerce_search_pattern_to_sort hpat = - let env = Global.env () in - let sigma = Evd.(from_env env) in - let mkPApp fp n_imps args = - let args' = Array.append (Array.make n_imps (Pattern.PMeta None)) args in - Pattern.PApp (fp, args') in - let hr, na = splay_search_pattern 0 hpat in - let dc, ht = - let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in - Reductionops.splay_prod env sigma (EConstr.of_constr hr) in - let np = List.length dc in - if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else - let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in - let warn () = - Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ - pr_constr_pattern_env env sigma hpat') in - if EConstr.isSort sigma ht then begin warn (); true, hpat' end else - let filter_head, coe_path = - try - let _, cp = - Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in - warn (); - true, cp - with _ -> false, [] in - let coerce hp coe_index = - let coe_ref = coe_index.Coercionops.coe_value in - try - let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in - mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with Not_found | Option.IsNone -> - errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () - ++ str "to interpret head search pattern as type") in - filter_head, List.fold_left coerce hpat' coe_path - -let interp_head_pat hpat = - let filter_head, p = coerce_search_pattern_to_sort hpat in - let rec loop c = match CoqConstr.kind c with - | Cast (c', _, _) -> loop c' - | Prod (_, _, c') -> loop c' - | LetIn (_, _, _, c') -> loop c' - | _ -> - let env = Global.env () in - let sigma = Evd.from_env env in - Constr_matching.is_matching env sigma p (EConstr.of_constr c) in - filter_head, loop - -let all_true _ = true - -let rec interp_search_about args accu = match args with -| [] -> accu -| (flag, arg) :: rem -> - fun gr env typ -> - let ans = Search.search_filter arg gr env typ in - (if flag then ans else not ans) && interp_search_about rem accu gr env typ - -let interp_search_arg arg = - let arg = List.map (fun (x,arg) -> x, match arg with - | RGlobSearchString (loc,s,key) -> - if is_ident_part s then Search.GlobSearchString s else - interp_search_notation ~loc s key - | RGlobSearchSubPattern p -> - let env = Global.env () in - let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in - Search.GlobSearchSubPattern p) arg - in - let hpat, a1 = match arg with - | (_, Search.GlobSearchSubPattern (Pattern.PMeta _)) :: a' -> all_true, a' - | (true, Search.GlobSearchSubPattern p) :: a' -> - let filter_head, p = interp_head_pat p in - if filter_head then p, a' else all_true, arg - | _ -> all_true, arg in - let is_string = - function (_, Search.GlobSearchString _) -> true | _ -> false in - let a2, a3 = List.partition is_string a1 in - interp_search_about (a2 @ a3) (fun gr env typ -> hpat typ) - -(* Module path postfilter *) - -let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m - -let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc) - -let pr_ssr_modlocs _ _ _ ml = - if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml - -} - -ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY { pr_ssr_modlocs } - | [ ] -> { [] } -END - -GRAMMAR EXTEND Gram - GLOBAL: ssr_modlocs; - modloc: [[ "-"; m = global -> { true, m } | m = global -> { false, m } ]]; - ssr_modlocs: [[ "in"; ml = LIST1 modloc -> { ml } ]]; -END - -{ - -let interp_modloc mr = - let interp_mod (_, qid) = - try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in - let mr_out, mr_in = List.partition fst mr in - let interp_bmod b = function - | [] -> fun _ _ _ -> true - | rmods -> Search.module_filter (List.map interp_mod rmods, b) in - let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in - fun gr env typ -> is_in gr env typ && is_out gr env typ - -(* The unified, extended vernacular "Search" command *) - -let ssrdisplaysearch gr env t = - let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in - Feedback.msg_notice (hov 2 pr_res ++ fnl ()) - -} - -VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY -| [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> - { let hpat = interp_search_arg a in - let in_mod = interp_modloc mr in - let post_filter gr env typ = in_mod gr env typ && hpat gr env typ in - let display gr env typ = - if post_filter gr env typ then ssrdisplaysearch gr env typ - in - Search.generic_search None display } -END - (** View hint database and View application. *)(* ******************************) (* There are three databases of lemmas used to mediate the application *) @@ -597,6 +300,35 @@ VERNAC COMMAND EXTEND HintView CLASSIFIED AS SIDEFF Ssrview.AdaptorDb.declare k hints } END +(** Search compatibility *) + +{ + + let warn_search_moved_enabled = ref true + let warn_search_moved = CWarnings.create ~name:"ssr-search-moved" + ~category:"deprecated" ~default:CWarnings.Enabled + (fun () -> + (Pp.strbrk + "SSReflect's Search command has been moved to the \ + ssrsearch module; please Require that module if you \ + still want to use SSReflect's Search command")) + +open G_vernac +} + +GRAMMAR EXTEND Gram + GLOBAL: query_command; + + query_command: + [ [ IDENT "Search"; s = search_query; l = search_queries; "." -> + { let (sl,m) = l in + if !warn_search_moved_enabled then warn_search_moved (); + fun g -> + Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) } + ] ] +; +END + (** Keyword compatibility fixes. *) (* Coq v8.1 notation uses "by" and "of" quasi-keywords, i.e., reserved *) diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli index 327a2d4660..93339313f0 100644 --- a/plugins/ssr/ssrvernac.mli +++ b/plugins/ssr/ssrvernac.mli @@ -9,3 +9,5 @@ (************************************************************************) (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) + +val warn_search_moved_enabled : bool ref diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 88a3e85211..ad0a31622c 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term)); tclUNIT (env,sigma,term) with e -> + (* XXX this is another catch all! *) + let e, info = Exninfo.capture e in Ssrprinters.ppdebug (lazy Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob)); - tclZERO e + tclZERO ~info e end (* Commits the term to the monad *) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index ce6fd4939b..5d6e7c51d0 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -410,7 +410,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = (* p_origin can be passed to obtain a better error message *) let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let k, f, a = - let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in + let f, a = Reductionops.whd_betaiota_stack env ise (EConstr.of_constr p) in let f = EConstr.Unsafe.to_constr f in let a = List.map EConstr.Unsafe.to_constr a in match kind f with diff --git a/plugins/ssrsearch/dune b/plugins/ssrsearch/dune new file mode 100644 index 0000000000..2851835eae --- /dev/null +++ b/plugins/ssrsearch/dune @@ -0,0 +1,7 @@ +(library + (name ssrsearch_plugin) + (public_name coq.plugins.ssrsearch) + (synopsis "Deprecated Search command from SSReflect") + (libraries coq.plugins.ssreflect)) + +(coq.pp (modules g_search)) diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg new file mode 100644 index 0000000000..6d68cc13ab --- /dev/null +++ b/plugins/ssrsearch/g_search.mlg @@ -0,0 +1,325 @@ +(** Extend Search to subsume SearchAbout, also adding hidden Type coercions. *) + +(* Main prefilter *) + +{ + +module CoqConstr = Constr +open CoqConstr +open Constrexpr +open Evar_kinds +open Glob_term +open Ltac_plugin +open Notation_ops +open Notation_term +open Pcoq.Prim +open Pcoq.Constr +open Pp +open Ppconstr +open Printer +open Stdarg +open Ssreflect_plugin.Ssrprinters +open Ssreflect_plugin.Ssrcommon +open Ssreflect_plugin.Ssrparser +open Termops +open Util + +type raw_glob_search_about_item = + | RGlobSearchSubPattern of constr_expr + | RGlobSearchString of Loc.t * string * string option + +let pr_search_item env sigma = function + | RGlobSearchString (_,s,_) -> str s + | RGlobSearchSubPattern p -> pr_constr_expr env sigma p + +let wit_ssr_searchitem = add_genarg "ssr_searchitem" pr_search_item + +let pr_ssr_search_item env sigma _ _ _ = pr_search_item env sigma + +(* Workaround the notation API that can only print notations *) + +let is_ident s = try CLexer.check_ident s; true with _ -> false + +let is_ident_part s = is_ident ("H" ^ s) + +let interp_search_notation ?loc tag okey = + let err msg = CErrors.user_err ?loc ~hdr:"interp_search_notation" msg in + let mk_pntn s for_key = + let n = String.length s in + let s' = Bytes.make (n + 2) ' ' in + let rec loop i i' = + if i >= n then s', i' - 2 else if s.[i] = ' ' then loop (i + 1) i' else + let j = try String.index_from s (i + 1) ' ' with _ -> n in + let m = j - i in + if s.[i] = '\'' && i < j - 2 && s.[j - 1] = '\'' then + (String.blit s (i + 1) s' i' (m - 2); loop (j + 1) (i' + m - 1)) + else if for_key && is_ident (String.sub s i m) then + (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) + else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in + loop 0 1 in + let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in + let pr_and_list pr = function + | [x] -> pr x + | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x + | [] -> mt () in + let pr_sc sc = str (if sc = "" then "independently" else sc) in + let pr_scs = function + | [""] -> pr_sc "" + | scs -> str "in " ++ pr_and_list pr_sc scs in + let generator, pr_tag_sc = + let ign _ = mt () in match okey with + | Some key -> + let sc = Notation.find_delimiters_scope ?loc key in + let pr_sc s_in = str s_in ++ spc() ++ str sc ++ pr_comma() in + Notation.pr_scope ign sc, pr_sc + | None -> Notation.pr_scopes ign, ign in + let qtag s_in = pr_tag_sc s_in ++ qstring tag ++ spc()in + let ptag, ttag = + let ptag, m = mk_pntn tag false in + if m <= 0 then err (str "empty notation fragment"); + ptag, trim_ntn (ptag, m) in + let last = ref "" and last_sc = ref "" in + let scs = ref [] and ntns = ref [] in + let push_sc sc = match !scs with + | "" :: scs' -> scs := "" :: sc :: scs' + | scs' -> scs := sc :: scs' in + let get s _ _ = match !last with + | "Scope " -> last_sc := s; last := "" + | "Lonely notation" -> last_sc := ""; last := "" + | "\"" -> + let pntn, m = mk_pntn s true in + if String.string_contains ~where:(Bytes.to_string pntn) ~what:(Bytes.to_string ptag) then begin + let ntn = trim_ntn (pntn, m) in + match !ntns with + | [] -> ntns := [ntn]; scs := [!last_sc] + | ntn' :: _ when ntn' = ntn -> push_sc !last_sc + | _ when ntn = ttag -> ntns := ntn :: !ntns; scs := [!last_sc] + | _ :: ntns' when List.mem ntn ntns' -> () + | ntn' :: ntns' -> ntns := ntn' :: ntn :: ntns' + end; + last := "" + | _ -> last := s in + pp_with (Format.make_formatter get (fun _ -> ())) generator; + let ntn = match !ntns with + | [] -> + err (hov 0 (qtag "in" ++ str "does not occur in any notation")) + | ntn :: ntns' when ntn = ttag -> + if ntns' <> [] then begin + let pr_ntns' = pr_and_list pr_ntn ntns' in + Feedback.msg_warning (hov 4 (qtag "In" ++ str "also occurs in " ++ pr_ntns')) + end; ntn + | [ntn] -> + Feedback.msg_notice (hov 4 (qtag "In" ++ str "is part of notation " ++ pr_ntn ntn)); ntn + | ntns' -> + let e = str "occurs in" ++ spc() ++ pr_and_list pr_ntn ntns' in + err (hov 4 (str "ambiguous: " ++ qtag "in" ++ e)) in + let (nvars, body), ((_, pat), osc) = match !scs with + | [sc] -> Notation.interp_notation ?loc ntn (None, [sc]) + | scs' -> + try Notation.interp_notation ?loc ntn (None, []) with _ -> + let e = pr_ntn ntn ++ spc() ++ str "is defined " ++ pr_scs scs' in + err (hov 4 (str "ambiguous: " ++ pr_tag_sc "in" ++ e)) in + let sc = Option.default "" osc in + let _ = + let m_sc = + if osc <> None then str "In " ++ str sc ++ pr_comma() else mt() in + let ntn_pat = trim_ntn (mk_pntn pat false) in + let rbody = glob_constr_of_notation_constr ?loc body in + let m_body = hov 0 (Constrextern.without_symbols prl_glob_constr rbody) in + let m = m_sc ++ pr_ntn ntn_pat ++ spc () ++ str "denotes " ++ m_body in + Feedback.msg_notice (hov 0 m) in + if List.length !scs > 1 then + let scs' = List.remove (=) sc !scs in + let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in + Feedback.msg_warning (hov 4 w) + else if String.string_contains ~where:(snd ntn) ~what:" .. " then + err (pr_ntn ntn ++ str " is an n-ary notation"); + let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in + let rec sub () = function + | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x) + | c -> + glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), None, x) sub () c in + let _, npat = Patternops.pattern_of_glob_constr (sub () body) in + Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,npat) + +} + +ARGUMENT EXTEND ssr_search_item TYPED AS ssr_searchitem + PRINTED BY { pr_ssr_search_item env sigma } + | [ string(s) ] -> { RGlobSearchString (loc,s,None) } + | [ string(s) "%" preident(key) ] -> { RGlobSearchString (loc,s,Some key) } + | [ constr_pattern(p) ] -> { RGlobSearchSubPattern p } +END + +{ + +let pr_ssr_search_arg env sigma _ _ _ = + let pr_item (b, p) = str (if b then "-" else "") ++ pr_search_item env sigma p in + pr_list spc pr_item + +} + +ARGUMENT EXTEND ssr_search_arg TYPED AS (bool * ssr_searchitem) list + PRINTED BY { pr_ssr_search_arg env sigma } + | [ "-" ssr_search_item(p) ssr_search_arg(a) ] -> { (false, p) :: a } + | [ ssr_search_item(p) ssr_search_arg(a) ] -> { (true, p) :: a } + | [ ] -> { [] } +END + +{ + +(* Main type conclusion pattern filter *) + +let rec splay_search_pattern na = function + | Pattern.PApp (fp, args) -> splay_search_pattern (na + Array.length args) fp + | Pattern.PLetIn (_, _, _, bp) -> splay_search_pattern na bp + | Pattern.PRef hr -> hr, na + | _ -> CErrors.user_err (Pp.str "no head constant in head search pattern") + +let push_rels_assum l e = + let l = List.map (fun (n,t) -> n, EConstr.Unsafe.to_constr t) l in + push_rels_assum l e + +let coerce_search_pattern_to_sort hpat = + let env = Global.env () in + let sigma = Evd.(from_env env) in + let mkPApp fp n_imps args = + let args' = Array.append (Array.make n_imps (Pattern.PMeta None)) args in + Pattern.PApp (fp, args') in + let hr, na = splay_search_pattern 0 hpat in + let dc, ht = + let hr, _ = Typeops.type_of_global_in_context env hr (* FIXME *) in + Reductionops.splay_prod env sigma (EConstr.of_constr hr) in + let np = List.length dc in + if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else + let hpat' = if np = na then hpat else mkPApp hpat (np - na) [||] in + let warn () = + Feedback.msg_warning (str "Listing only lemmas with conclusion matching " ++ + pr_constr_pattern_env env sigma hpat') in + if EConstr.isSort sigma ht then begin warn (); true, hpat' end else + let filter_head, coe_path = + try + let _, cp = + Coercionops.lookup_path_to_sort_from (push_rels_assum dc env) sigma ht in + warn (); + true, cp + with _ -> false, [] in + let coerce hp coe_index = + let coe_ref = coe_index.Coercionops.coe_value in + try + let n_imps = Option.get (Coercionops.hide_coercion coe_ref) in + mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () + ++ str "to interpret head search pattern as type") in + filter_head, List.fold_left coerce hpat' coe_path + +let interp_head_pat hpat = + let filter_head, p = coerce_search_pattern_to_sort hpat in + let rec loop c = match CoqConstr.kind c with + | Cast (c', _, _) -> loop c' + | Prod (_, _, c') -> loop c' + | LetIn (_, _, _, c') -> loop c' + | _ -> + let env = Global.env () in + let sigma = Evd.from_env env in + Constr_matching.is_matching env sigma p (EConstr.of_constr c) in + filter_head, loop + +let all_true _ = true + +let rec interp_search_about args accu = match args with +| [] -> accu +| (flag, arg) :: rem -> + fun gr kind env typ -> + let ans = Search.search_filter arg gr kind env (Evd.from_env env) typ in + (if flag then ans else not ans) && interp_search_about rem accu gr kind env typ + +let interp_search_arg arg = + let arg = List.map (fun (x,arg) -> x, match arg with + | RGlobSearchString (loc,s,key) -> + if is_ident_part s then Search.GlobSearchString s else + interp_search_notation ~loc s key + | RGlobSearchSubPattern p -> + let env = Global.env () in + let _, p = Constrintern.intern_constr_pattern env (Evd.from_env env) p in + Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,p)) arg + in + let hpat, a1 = match arg with + | (_, Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,Pattern.PMeta _)) :: a' -> all_true, a' + | (true, Search.GlobSearchSubPattern (Vernacexpr.Anywhere,false,p)) :: a' -> + let filter_head, p = interp_head_pat p in + if filter_head then p, a' else all_true, arg + | (_, (Search.GlobSearchSubPattern (Vernacexpr.(InHyp|InConcl),_,_) + |Search.GlobSearchSubPattern (Vernacexpr.Anywhere,true,_))) :: a' -> CErrors.user_err (str "Unsupported.") + | _ -> all_true, arg in + let is_string = + function (_, Search.GlobSearchString _) -> true | _ -> false in + let a2, a3 = List.partition is_string a1 in + interp_search_about (a2 @ a3) (fun gr kind env typ -> hpat typ) + +(* Module path postfilter *) + +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m + +let wit_ssrmodloc = add_genarg "ssrmodloc" (fun env sigma -> pr_modloc) + +let pr_ssr_modlocs _ _ _ ml = + if ml = [] then str "" else spc () ++ str "in " ++ pr_list spc pr_modloc ml + +} + +ARGUMENT EXTEND ssr_modlocs TYPED AS ssrmodloc list PRINTED BY { pr_ssr_modlocs } + | [ ] -> { [] } +END + +GRAMMAR EXTEND Gram + GLOBAL: ssr_modlocs; + modloc: [[ "-"; m = global -> { true, m } | m = global -> { false, m } ]]; + ssr_modlocs: [[ "in"; ml = LIST1 modloc -> { ml } ]]; +END + +{ + +let interp_modloc mr = + let interp_mod (_, qid) = + try Nametab.full_name_module qid with Not_found -> + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in + let mr_out, mr_in = List.partition fst mr in + let interp_bmod b = function + | [] -> fun _ _ _ _ _ -> true + | rmods -> Search.module_filter (List.map interp_mod rmods, b) in + let is_in = interp_bmod false mr_in and is_out = interp_bmod true mr_out in + fun gr kind env typ -> is_in gr kind env (Evd.from_env env) typ && is_out gr kind env (Evd.from_env env) typ + +(* The unified, extended vernacular "Search" command *) + +let ssrdisplaysearch gr env t = + let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in + Feedback.msg_notice (hov 2 pr_res ++ fnl ()) + +(* Remove the warning entirely when this plugin is loaded. *) +let _ = + Ssreflect_plugin.Ssrvernac.warn_search_moved_enabled := false + +let deprecated_search = + CWarnings.create + ~name:"deprecated-ssr-search" + ~category:"deprecated" + (fun () -> Pp.(str"SSReflect's Search command is deprecated.")) + +} + +VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY +| [ "Search" ssr_search_arg(a) ssr_modlocs(mr) ] -> + { deprecated_search (); + let hpat = interp_search_arg a in + let in_mod = interp_modloc mr in + let post_filter gr kind env typ = in_mod gr kind env typ && hpat gr kind env typ in + let display gr kind env typ = + if post_filter gr kind env typ then ssrdisplaysearch gr env typ + in + let env = Global.env () in + Search.generic_search env display } +END diff --git a/plugins/ssrsearch/ssrsearch_plugin.mlpack b/plugins/ssrsearch/ssrsearch_plugin.mlpack new file mode 100644 index 0000000000..0c32130d65 --- /dev/null +++ b/plugins/ssrsearch/ssrsearch_plugin.mlpack @@ -0,0 +1 @@ +G_search diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index e0a9906689..8e87fc13ca 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -28,8 +28,8 @@ let warn_inexact_float = Pp.strbrk (Printf.sprintf "The constant %s is not a binary64 floating-point value. \ - A closest value will be used and unambiguously printed %s." - sn (Float64.to_string f))) + A closest value %s will be used and unambiguously printed %s." + sn (Float64.to_hex_string f) (Float64.to_string f))) let interp_float ?loc n = let sn = NumTok.Signed.to_string n in @@ -42,7 +42,7 @@ let interp_float ?loc n = | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n) | Float64.(PNormal | NNormal | PSubn | NSubn) -> let m, e = - let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in + let (_, i), f, e = NumTok.Signed.to_int_frac_and_exponent n in let i = NumTok.UnsignedNat.to_string i in let f = match f with | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in @@ -70,7 +70,8 @@ let interp_float ?loc n = else (* e < 0 *) if e' <= e then check m' (-e) m (e - e') else check' m' (-e) (e' - e) m in - if inexact () then warn_inexact_float ?loc (sn, f); + if NumTok.(Signed.classify n = CDec) && inexact () then + warn_inexact_float ?loc (sn, f); DAst.make ?loc (GFloat f) (* Pretty printing is already handled in constrextern.ml *) diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 2250d57809..2db76719b8 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -55,24 +55,45 @@ let locate_z () = }, mkRefC q_z) else None -let locate_decimal () = - let int = "num.int.type" in - let uint = "num.uint.type" in +let locate_numeral () = + let dint = "num.int.type" in + let duint = "num.uint.type" in let dec = "num.decimal.type" in - if Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref dec + let hint = "num.hexadecimal_int.type" in + let huint = "num.hexadecimal_uint.type" in + let hex = "num.hexadecimal.type" in + let int = "num.num_int.type" in + let uint = "num.num_uint.type" in + let num = "num.numeral.type" in + if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec + && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex + && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num then + let q_dint = qualid_of_ref dint in + let q_duint = qualid_of_ref duint in + let q_dec = qualid_of_ref dec in + let q_hint = qualid_of_ref hint in + let q_huint = qualid_of_ref huint in + let q_hex = qualid_of_ref hex in let q_int = qualid_of_ref int in let q_uint = qualid_of_ref uint in - let q_dec = qualid_of_ref dec in + let q_num = qualid_of_ref num in let int_ty = { + dec_int = unsafe_locate_ind q_dint; + dec_uint = unsafe_locate_ind q_duint; + hex_int = unsafe_locate_ind q_hint; + hex_uint = unsafe_locate_ind q_huint; int = unsafe_locate_ind q_int; uint = unsafe_locate_ind q_uint; } in - let dec_ty = { + let num_ty = { int = int_ty; decimal = unsafe_locate_ind q_dec; + hexadecimal = unsafe_locate_ind q_hex; + numeral = unsafe_locate_ind q_num; } in - Some (int_ty, mkRefC q_int, mkRefC q_uint, dec_ty, mkRefC q_dec) + Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, + num_ty, mkRefC q_num, mkRefC q_dec) else None let locate_int63 () = @@ -90,20 +111,27 @@ let has_type env sigma f ty = let type_error_to f ty = CErrors.user_err - (pr_qualid f ++ str " should go from Decimal.int to " ++ + (pr_qualid f ++ str " should go from Numeral.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") + fnl () ++ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ - str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ - str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") + str " to Numeral.int or (option Numeral.int)." ++ fnl () ++ + str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") + +let warn_deprecated_decimal = + CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Deprecated Numeral Notation for Decimal.uint, \ + Decimal.int or Decimal.decimal. Use Numeral.uint, \ + Numeral.int or Numeral.numeral respectively.") let vernac_numeral_notation local ty f g scope opts = let env = Global.env () in let sigma = Evd.from_env env in - let dec_ty = locate_decimal () in + let num_ty = locate_numeral () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in let tyc = Smartlocate.global_inductive_with_alias ty in @@ -118,13 +146,19 @@ let vernac_numeral_notation local ty f g scope opts = let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = - match dec_ty with - | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct - | Some (int_ty, _, cuint, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option - | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal dec_ty, Direct - | Some (_, _, _, dec_ty, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal dec_ty, Option + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct @@ -137,13 +171,19 @@ let vernac_numeral_notation local ty f g scope opts = in (* Check the type of g *) let of_kind = - match dec_ty with - | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct - | Some (int_ty, _, cuint, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option - | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal dec_ty, Direct - | Some (_, _, _, dec_ty, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal dec_ty, Option + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option | _ -> match z_pos_ty with | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct @@ -154,6 +194,11 @@ let vernac_numeral_notation local ty f g scope opts = | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option | _ -> type_error_of g ty in + (match to_kind, of_kind with + | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ + | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> + warn_deprecated_decimal () + | _ -> ()); let o = { to_kind; to_ty; of_kind; of_ty; ty_name = ty; warning = opts } diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index c4e9c8b73d..23a7cc07c5 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -114,20 +114,21 @@ let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow let r_of_rawnum ?loc n = let n,e = NumTok.Signed.to_bigint_and_exponent n in + let e,p = NumTok.(match e with EDec e -> e, 10 | EBin e -> e, 2) in let izr z = DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in let rmult r r' = DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in let rdiv r r' = DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in - let pow10 e = - let ten = z_of_int ?loc (Bigint.of_int 10) in + let pow p e = + let p = z_of_int ?loc (Bigint.of_int p) in let e = pos_of_bignat e in - DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [ten; e]) in + DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in let n = izr (z_of_int ?loc n) in - if Bigint.is_strictly_pos e then rmult n (izr (pow10 e)) - else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e))) + if Bigint.is_strictly_pos e then rmult n (izr (pow p e)) + else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e))) else n (* e = 0 *) (**********************************************************************) @@ -149,7 +150,8 @@ let rawnum_of_r c = let le = String.length (Bigint.to_string e) in Bigint.(less_than (add (of_int li) (of_int le)) e) in (* print 123 * 10^-2 as 123e-2 *) - let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in + let numTok_exponent () = + NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in (* print 123 * 10^-2 as 1.23, precondition e < 0 *) let numTok_dot () = let s, i = @@ -163,12 +165,12 @@ let rawnum_of_r c = else "0", String.make (e - ni) '0' ^ i in let i = s, NumTok.UnsignedNat.of_string i in let f = NumTok.UnsignedNat.of_string f in - NumTok.Signed.of_decimal_and_exponent i (Some f) None in + NumTok.Signed.of_int_frac_and_exponent i (Some f) None in if choose_exponent then numTok_exponent () else numTok_dot () in match DAst.get c with | GApp (r, [a]) when is_gr r glob_IZR -> let n = bigint_of_z a in - NumTok.Signed.of_bigint n + NumTok.(Signed.of_bigint CDec n) | GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv -> begin match DAst.get l, DAst.get r with | GApp (i, [l]), GApp (i', [r]) |