aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/extraction/common.ml7
-rw-r--r--plugins/extraction/common.mli1
-rw-r--r--plugins/extraction/ocaml.ml18
-rw-r--r--plugins/ltac/tacinterp.ml70
-rw-r--r--plugins/ssr/ssrcommon.ml4
-rw-r--r--plugins/ssr/ssrequality.ml2
6 files changed, 65 insertions, 37 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 4a41f4c890..d215a7673d 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -604,6 +604,13 @@ let pp_global k r =
| Haskell -> if modular () then pp_haskell_gen k mp rls else s
| Ocaml -> pp_ocaml_gen k mp rls (Some l)
+(* Main name printing function for declaring a reference *)
+
+let pp_global_name k r =
+ let ls = ref_renaming (k,r) in
+ assert (List.length ls > 1);
+ List.hd ls
+
(* The next function is used only in Ocaml extraction...*)
let pp_module mp =
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 0bd9efd255..a482cfc03d 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -55,6 +55,7 @@ val opened_libraries : unit -> ModPath.t list
type kind = Term | Type | Cons | Mod
val pp_global : kind -> GlobRef.t -> string
+val pp_global_name : kind -> GlobRef.t -> string
val pp_module : ModPath.t -> string
val top_visible_mp : unit -> ModPath.t
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 088405da5d..6425c3111e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -99,6 +99,8 @@ let str_global k r =
let pp_global k r = str (str_global k r)
+let pp_global_name k r = str (Common.pp_global k r)
+
let pp_modname mp = str (Common.pp_module mp)
(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
@@ -451,7 +453,7 @@ let pp_val e typ =
let pp_Dfix (rv,c,t) =
let names = Array.map
- (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+ (fun r -> if is_inline_custom r then mt () else pp_global_name Term r) rv
in
let rec pp init i =
if i >= Array.length rv then mt ()
@@ -504,7 +506,7 @@ let pp_logical_ind packet =
fnl ()
let pp_singleton kn packet =
- let name = pp_global Type (GlobRef.IndRef (kn,0)) in
+ let name = pp_global_name Type (GlobRef.IndRef (kn,0)) in
let l = rename_tvars keywords packet.ip_vars in
hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -513,7 +515,7 @@ let pp_singleton kn packet =
let pp_record kn fields ip_equiv packet =
let ind = GlobRef.IndRef (kn,0) in
- let name = pp_global Type ind in
+ let name = pp_global_name Type ind in
let fieldnames = pp_fields ind fields in
let l = List.combine fieldnames packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
@@ -535,7 +537,7 @@ let pp_ind co kn ind =
let nextkwd = fnl () ++ str "and " in
let names =
Array.mapi (fun i p -> if p.ip_logical then mt () else
- pp_global Type (GlobRef.IndRef (kn,i)))
+ pp_global_name Type (GlobRef.IndRef (kn,i)))
ind.ind_packets
in
let cnames =
@@ -575,7 +577,7 @@ let pp_decl = function
| Dterm (r,_,_) when is_inline_custom r -> mt ()
| Dind (kn,i) -> pp_mind kn i
| Dtype (r, l, t) ->
- let name = pp_global Type r in
+ let name = pp_global_name Type r in
let l = rename_tvars keywords l in
let ids, def =
try
@@ -592,7 +594,7 @@ let pp_decl = function
if is_custom r then str (" = " ^ find_custom r)
else pp_function (empty_env ()) a
in
- let name = pp_global Term r in
+ let name = pp_global_name Term r in
pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
| Dfix (rv,defs,typs) ->
pp_Dfix (rv,defs,typs)
@@ -603,10 +605,10 @@ let pp_spec = function
| Sind (kn,i) -> pp_mind kn i
| Sval (r,t) ->
let def = pp_type false [] t in
- let name = pp_global Term r in
+ let name = pp_global_name Term r in
hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
| Stype (r,vl,ot) ->
- let name = pp_global Type r in
+ let name = pp_global_name Type r in
let l = rename_tvars keywords vl in
let ids, def =
try
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fdebe14a23..2ca9a0e69d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -161,27 +161,45 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let update_loc ?loc (e, info) =
- (e, Option.cata (Loc.add_loc info) info loc)
+let update_loc loc use_finer (e, info as e') =
+ match loc with
+ | Some loc ->
+ if use_finer then
+ (* ensure loc if there is none *)
+ match Loc.get_loc info with
+ | None -> (e, Loc.add_loc info loc)
+ | _ -> (e, info)
+ else
+ (* override loc (because loc refers to inside of Ltac functions) *)
+ (e, Loc.add_loc info loc)
+ | None -> e'
-let catch_error ?loc call_trace f x =
+let catch_error_with_trace_loc loc use_finer call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
- let e = update_loc ?loc e in
+ let e = update_loc loc use_finer e in
catching_error call_trace Exninfo.iraise e
-let catch_error_loc ?loc tac =
- Proofview.tclOR tac (fun exn ->
- let (e, info) = update_loc ?loc exn in
+let catch_error_loc loc use_finer tac =
+ Proofview.tclORELSE tac (fun exn ->
+ let (e, info) = update_loc loc use_finer exn in
Proofview.tclZERO ~info e)
-let wrap_error ?loc tac k =
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
+let wrap_error_loc loc use_finer tac k =
if is_traced () then Proofview.tclORELSE tac k
- else catch_error_loc ?loc tac
+ else catch_error_loc loc use_finer tac
+
+let catch_error_tac call_trace tac =
+ wrap_error
+ tac
+ (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
-let catch_error_tac ?loc call_trace tac =
- wrap_error ?loc
+let catch_error_tac_loc loc use_finer call_trace tac =
+ wrap_error_loc loc use_finer
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -553,7 +571,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let loc = loc_of_glob_constr term in
let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
+ catch_error_with_trace_loc loc true trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -1066,12 +1084,12 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-and eval_tactic ist tac : unit Proofview.tactic = match tac with
+and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacAtom {loc;v=t} ->
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac ?loc trace (interp_atomic ist t))
+ (catch_error_tac_loc loc true trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1145,7 +1163,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
- | TacArg a -> interp_tactic ist (TacArg a)
+ | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v))
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1162,7 +1180,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
; poly
; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
+ Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v))
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1191,7 +1209,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac_loc loc false trace (tac args ist))
in
Ftactic.run args tac
@@ -1225,7 +1243,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
- (val_interp ~appl ist (Tacenv.interp_ltac r))
+ (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
@@ -1294,7 +1312,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1341,7 +1359,7 @@ and tactic_of_value ist vle =
lfun = lfun;
poly;
extra = TacStore.set ist.extra f_trace []; } in
- let tac = name_if_glob appl (eval_tactic ist t) in
+ let tac = name_if_glob appl (eval_tactic_ist ist t) in
Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
| VFun (appl,_,vmap,vars,_) ->
let tactic_nm =
@@ -1428,7 +1446,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
; poly
; extra = TacStore.set ist.extra f_trace trace
} in
- let tac = eval_tactic ist t in
+ let tac = eval_tactic_ist ist t in
let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
| _ -> Ftactic.return v
@@ -1909,11 +1927,11 @@ let default_ist () =
let eval_tactic t =
Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
Proofview.tclLIFT db_initialize <*>
- interp_tactic (default_ist ()) t
+ eval_tactic_ist (default_ist ()) t
let eval_tactic_ist ist t =
Proofview.tclLIFT db_initialize <*>
- interp_tactic ist t
+ eval_tactic_ist ist t
(** FFI *)
@@ -1959,7 +1977,7 @@ let interp_tac_gen lfun avoid_ids debug t =
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun; poly; extra } in
let ltacvars = Id.Map.domain lfun in
- interp_tactic ist
+ eval_tactic_ist ist
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
end
@@ -2076,7 +2094,7 @@ let () =
register_interp0 wit_tactic interp
let () =
- let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
+ let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in
register_interp0 wit_ltac interp
let () =
@@ -2103,7 +2121,7 @@ let _ =
let eval lfun poly env sigma ty tac =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun; poly; extra; } in
- let tac = interp_tactic ist tac in
+ let tac = eval_tactic_ist ist tac in
(* EJGA: We should also pass the proof name if desired, for now
poly seems like enough to get reasonable behavior in practice
*)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1b7768852e..d859fe51ab 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1047,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
let uct = Evd.evar_universe_context (fst oc) in
let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
- Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
+ Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
(fun _ -> Proofview.tclZERO dependent_apply_error)
end
@@ -1352,7 +1352,7 @@ let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = Environ.named_context_val env in
let nctx = EConstr.push_named_context_val decl ctx in
- let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
+ let inst = EConstr.identity_subst_val (Environ.named_context_val env) in
let ninst = EConstr.mkRel 1 :: inst in
let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index da623703a2..38b26d06b9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr =
Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0
in
let cvtac' =
- Proofview.tclOR cvtac begin function
+ Proofview.tclORELSE cvtac begin function
| (PRtype_error e, _) ->
let error = Option.cata (fun (env, sigma, te) ->
Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:38:01 +0000