aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/indfun.ml25
-rw-r--r--contrib/interface/xlate.ml24
-rw-r--r--contrib/subtac/eterm.ml9
-rw-r--r--contrib/subtac/eterm.mli5
-rw-r--r--contrib/subtac/subtac.ml2
-rw-r--r--contrib/subtac/subtac_cases.ml2
-rw-r--r--contrib/subtac/subtac_coercion.ml4
-rw-r--r--contrib/subtac/subtac_command.ml87
-rw-r--r--contrib/subtac/subtac_obligations.ml31
-rw-r--r--contrib/subtac/subtac_obligations.mli4
-rw-r--r--contrib/subtac/subtac_utils.ml2
11 files changed, 84 insertions, 111 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 4f78c8c59c..fa49d4aa86 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -510,13 +510,8 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
List.map
(function
| (name,Some (Struct id),args,types,body),_ ->
- let names =
- List.map
- snd
- (Topconstr.names_of_local_assums args)
- in
let annot =
- try Some (list_index0 (Name id) names), Topconstr.CStructRec
+ try Some (dummy_loc, id), Topconstr.CStructRec
with Not_found ->
raise (UserError("",str "Cannot find argument " ++
Ppconstr.pr_id id))
@@ -529,7 +524,8 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
(dummy_loc,"Function",
Pp.str "the recursive argument needs to be specified in Function")
else
- (name,(Some 0, Topconstr.CStructRec),args,types,body),
+ let loc, na = List.hd names in
+ (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
(None:Vernacexpr.decl_notation)
| (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
error
@@ -713,20 +709,7 @@ let make_graph (f_ref:global_reference) =
let l =
List.map
(fun (id,(n,recexp),bl,t,b) ->
- let bl' =
- List.flatten
- (List.map
- (function
- | Topconstr.LocalRawDef (na,_)-> []
- | Topconstr.LocalRawAssum (nal,_,_) -> nal
- )
- bl
- )
- in
- let rec_id =
- match List.nth bl' (Option.get n) with
- |(_,Name id) -> id | _ -> anomaly ""
- in
+ let loc, rec_id = Option.get n in
let new_args =
List.flatten
(List.map
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 82277be4df..20bb3a4a1f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -305,11 +305,7 @@ let make_fix_struct (n,bl) =
let names = names_of_local_assums bl in
let nn = List.length names in
if nn = 1 || n = None then ctv_ID_OPT_NONE
- else
- let n = Option.get n in
- if n < nn then xlate_id_opt(List.nth names n)
- else xlate_error "unexpected result of parsing for Fixpoint";;
-
+ else ctf_ID_OPT_SOME(CT_ident (string_of_id (snd (Option.get n))));;
let rec xlate_binder = function
(l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t)
@@ -425,14 +421,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
(CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
| CFix (_, (_, id), lm::lmi) ->
let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
- let (struct_arg,bl,arf,ardef) =
- (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
- (* By the way, how could [bl = []] happen in V8 syntax ? *)
- if bl = [] then
- let n = Option.get n in
- let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
- (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
- else (make_fix_struct (n, bl),bl,arf,ardef) in
+ let struct_arg = make_fix_struct (n, bl) in
let arf = xlate_formula arf in
let ardef = xlate_formula ardef in
match xlate_binder_list bl with
@@ -1953,14 +1942,7 @@ let rec xlate_vernac =
| VernacFixpoint ([],_) -> xlate_error "mutual recursive"
| VernacFixpoint ((lm :: lmi),boxed) ->
let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) =
- let (struct_arg,bl,arf,ardef) =
- (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *)
- (* By the way, how could [bl = []] happen in V8 syntax ? *)
- if bl = [] then
- let n = Option.get n in
- let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
- (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
- else (make_fix_struct (n, bl),bl,arf,ardef) in
+ let struct_arg = make_fix_struct (n, bl) in
let arf = xlate_formula arf in
let ardef = xlate_formula ardef in
match xlate_binder_list bl with
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 8f319f9efc..9bfb33ea77 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -28,7 +28,7 @@ let subst_evar_constr evs n t =
let evar_info id = List.assoc id evs in
let rec substrec (depth, fixrels) c = match kind_of_term c with
| Evar (k, args) ->
- let (id, idstr), hyps, chop, _, _ =
+ let (id, idstr), hyps, chop, _, _, _ =
try evar_info k
with Not_found ->
anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
@@ -158,7 +158,7 @@ let eterm_obligations env name isevars evm fs t ty =
let loc, k = evar_source id isevars in
let opacity = match k with QuestionMark o -> o | _ -> true in
let opaque = if not opacity || chop <> fs then None else Some chop in
- let y' = (id, ((n, nstr), hyps, opaque, evtyp, deps)) in
+ let y' = (id, ((n, nstr), hyps, opaque, loc, evtyp, deps)) in
y' :: l)
evn []
in
@@ -167,13 +167,14 @@ let eterm_obligations env name isevars evm fs t ty =
in
let ty, _, _ = subst_evar_constr evts 0 ty in
let evars =
- List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None) && not (Idset.mem name transparent), deps) evts
+ List.map (fun (_, ((_, name), _, opaque, loc, typ, deps)) ->
+ name, typ, loc, not (opaque = None) && not (Idset.mem name transparent), deps) evts
in
(try
trace (str "Term constructed in eterm" ++ spc () ++
Termops.print_constr_env (Global.env ()) t');
ignore(iter
- (fun (name, typ, _, deps) ->
+ (fun (name, typ, _, _, deps) ->
trace (str "Evar :" ++ spc () ++ str (string_of_id name) ++
Termops.print_constr_env (Global.env ()) typ))
evars);
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index e23fd535ca..5f10ac1d38 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -21,7 +21,8 @@ val mkMetas : int -> constr list
(* env, id, evars, number of
function prototypes to try to clear from evars contexts, object and type *)
val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types ->
- (identifier * types * bool * Intset.t) array * constr * types
- (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *)
+ (identifier * types * loc * bool * Intset.t) array * constr * types
+ (* Obl. name, type as product, location of the original evar,
+ opacity (true = opaque) and dependencies as indexes into the array *)
val etermtac : open_constr -> tactic
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 9641794bea..06c67e60b1 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -54,7 +54,7 @@ let solve_tccs_in_type env id isevars evm c typ =
let stmt_id = Nameops.add_suffix id "_stmt" in
let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in
(** Make all obligations transparent so that real dependencies can be sorted out by the user *)
- let obls = Array.map (fun (id, t, op, d) -> (id, t, false, d)) obls in
+ let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
match Subtac_obligations.add_definition stmt_id c' typ obls with
Subtac_obligations.Defined cst -> constant_value (Global.env()) cst
| _ ->
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 6e9b741ef5..6a470afc6a 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1745,7 +1745,7 @@ let build_ineqs prevpatterns pats liftsign =
len',
succ n, (* nth pattern *)
mkApp (Lazy.force eq_ind,
- [| lift (succ len') curpat_ty ;
+ [| lift (len' + liftsign) curpat_ty;
liftn (len + liftsign) (succ lens) ppat_c ;
lift len' curpat_c |]) ::
List.map (lift lens (* Jump over this prevpat signature *)) c)
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 218c697c68..5ca313d0bb 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -150,7 +150,7 @@ module Coercion = struct
let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
let eq = mkApp (Lazy.force eq_ind, [| eqT; hdx; hdy |]) in
(* let jmeq = mkApp (Lazy.force jmeq_ind, [| eqT; hdx; eqT; hdy |]) in *)
- let evar = make_existential dummy_loc env isevars eq in
+ let evar = make_existential loc env isevars eq in
let eq_app x = mkApp (Lazy.force eq_rect,
[| eqT; hdx; pred; x; hdy; evar|]) in
(* trace (str"Inserting coercion at application"); *)
@@ -300,7 +300,7 @@ module Coercion = struct
Some
(fun x ->
let cx = app_opt c x in
- let evar = make_existential dummy_loc env isevars (mkApp (p, [| cx |]))
+ let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
in
(mkApp
((Lazy.force sig_).intro,
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index c29d677f55..da0e4a8e56 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -98,24 +98,30 @@ let locate_if_isevar loc na = function
let interp_binder sigma env na t =
let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
-
-let interp_context_evars sigma env params =
- List.fold_left
- (fun (env,params) d -> match d with
- | LocalRawAssum ([_,na],k,(CHole _ as t)) ->
- let t = interp_binder sigma env na t in
- let d = (na,None,t) in
- (push_rel d env, d::params)
- | LocalRawAssum (nal,k,t) ->
- let t = interp_type_evars sigma env t in
- let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
- let ctx = List.rev ctx in
- (push_rel_context ctx env, ctx@params)
- | LocalRawDef ((_,na),c) ->
- let c = interp_constr_judgment sigma env c in
- let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params))
- (env,[]) params
+
+let interp_context_evars evdref env params =
+ let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in
+ let (env, par, _, impls) =
+ List.fold_left
+ (fun (env,params,n,impls) (na, k, b, t) ->
+ match b with
+ None ->
+ let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+ let t = SPretyping.understand_tcc_evars evdref env IsType t' in
+ let d = (na,None,t) in
+ let impls =
+ if k = Implicit then
+ let na = match na with Name n -> Some n | Anonymous -> None in
+ (ExplByPos (n, na), (true, true)) :: impls
+ else impls
+ in
+ (push_rel d env, d::params, succ n, impls)
+ | Some b ->
+ let c = SPretyping.understand_judgment_tcc evdref env b in
+ let d = (na, Some c.uj_val, c.uj_type) in
+ (push_rel d env,d::params, succ n, impls))
+ (env,[],1,[]) (List.rev bl)
+ in (env, par), impls
(* try to find non recursive definitions *)
@@ -191,8 +197,10 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
(* Ppconstr.pr_constr_expr body) *)
(* with _ -> () *)
(* in *)
- let env', binders_rel = interp_context_evars isevars env bl in
- let after, ((argname, _, argtyp) as arg), before = split_args (succ n) binders_rel in
+ let (env', binders_rel), impls = interp_context_evars isevars env bl in
+ let after, ((argname, _, argtyp) as arg), before =
+ let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in
+ split_args idx binders_rel in
let before_length, after_length = List.length before, List.length after in
let argid = match argname with Name n -> n | _ -> assert(false) in
let liftafter = lift_binders 1 after_length after in
@@ -232,7 +240,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
let top_env = push_rel_context top_bl env in
let top_arity = interp_type_evars isevars top_env arityc in
let intern_bl = wfarg 1 :: arg :: before in
- let intern_env = push_rel_context intern_bl env in
+ let _intern_env = push_rel_context intern_bl env in
let proj = (Lazy.force sig_).Coqlib.proj1 in
let projection =
mkApp (proj, [| argtyp ;
@@ -242,32 +250,19 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
|])
in
let intern_arity = it_mkProd_or_LetIn top_arity after in
- trace (str "After length: " ++ int after_length ++ str "Top env: " ++ prr top_bl ++ spc () ++
- str "Intern arity: " ++ my_print_constr
- (push_rel_context (arg :: before) env) intern_arity);
(* Intern arity is in top_env = arg :: before *)
let intern_arity = liftn 2 2 intern_arity in
- trace (str "After lifting arity: " ++
- my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env)
- intern_arity);
+(* trace (str "After lifting arity: " ++ *)
+(* my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *)
+(* intern_arity); *)
(* arity is now in something :: wfarg :: arg :: before
where what refered to arg now refers to something *)
let intern_arity = substl [projection] intern_arity in
(* substitute the projection of wfarg for something *)
- (try trace (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
-(* let intern_arity = liftn 1 (succ after_length) intern_arity in (\* back in after :: wfarg :: arg :: before (ie, jump over arg) *\) *)
-(* (try trace (str "Top arity after subst and lift: " ++ my_print_constr (Global.env ()) intern_arity) with _ -> ()); *)
let intern_before_env = push_rel_context before env in
-(* let intern_fun_bl = liftafter @ [wfarg 1] in (\* FixMe dependencies *\) *)
-(* (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ()); *)
- (try trace (str "Intern arity: " ++
- my_print_constr intern_env intern_arity) with _ -> ());
let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
- (try trace (str "Intern fun arity product: " ++
- my_print_constr (push_rel_context [arg] intern_before_env) intern_fun_arity_prod) with _ -> ());
let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
-(* (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ()); *)
let fun_env = push_rel_context fun_bl intern_before_env in
let fun_arity = interp_type_evars isevars fun_env arityc in
let intern_body = interp_casted_constr isevars fun_env body fun_arity in
@@ -338,9 +333,12 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs =
let names = List.map (fun id -> Name id) fixnames in
(Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
-let compute_possible_guardness_evidences (n,_) fixtype =
+let rel_index n ctx =
+ list_index0 (Name n) (List.rev_map (fun (na, _, _) -> na) ctx)
+
+let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
match n with
- | Some n -> [n]
+ | Some (loc, n) -> [rel_index n fixctx]
| None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
@@ -360,12 +358,7 @@ let interp_recursive fixkind l boxed =
(* Interp arities allowing for unresolved types *)
let evdref = ref (Evd.create_evar_defs Evd.empty) in
- let fiximps =
- List.map
- (fun x -> Implicit_quantifiers.implicits_of_binders x.Command.fix_binders)
- fixl
- in
- let fixctxs = List.map (interp_fix_context evdref env) fixl in
+ let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
let fixtypes = List.map2 build_fix_type fixctxs fixccls in
let rec_sign =
@@ -421,7 +414,7 @@ let interp_recursive fixkind l boxed =
(match fixkind with
| Command.IsFixpoint wfl ->
let possible_indexes =
- List.map2 compute_possible_guardness_evidences wfl fixtypes in
+ list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
Array.of_list fixtypes,
Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
@@ -433,7 +426,7 @@ let interp_recursive fixkind l boxed =
let out_n = function
Some n -> n
- | None -> 0
+ | None -> raise Not_found
let build_recursive l b =
let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index c15bfb528c..bc6d5dee1a 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -24,11 +24,12 @@ let explain_no_obligations = function
Some ident -> str "No obligations for program " ++ str (string_of_id ident)
| None -> str "No obligations remaining"
-type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
+type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
type obligation =
{ obl_name : identifier;
obl_type : types;
+ obl_location : loc;
obl_body : constr option;
obl_opaque : bool;
obl_deps : Intset.t;
@@ -179,9 +180,16 @@ let declare_definition prg =
open Pp
open Ppconstr
-let compute_possible_guardness_evidences (n,_) fixtype =
+let rec lam_index n t acc =
+ match kind_of_term t with
+ | Lambda (na, _, b) ->
+ if na = Name n then acc
+ else lam_index n b (succ acc)
+ | _ -> raise Not_found
+
+let compute_possible_guardness_evidences (n,_) fixbody fixtype =
match n with
- | Some n -> [n]
+ | Some (loc, n) -> [lam_index n fixbody 0]
| None ->
(* If recursive argument was not given by user, we try all args.
An earlier approach was to look only for inductive arguments,
@@ -210,7 +218,7 @@ let declare_mutual_definition l =
match fixkind with
| IsFixpoint wfl ->
let possible_indexes =
- List.map2 compute_possible_guardness_evidences wfl fixtypes in
+ list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
| IsCoFixpoint ->
@@ -254,10 +262,10 @@ let red = Reductionops.nf_betaiota
let init_prog_info n b t deps fixkind notations obls impls kind hook =
let obls' =
Array.mapi
- (fun i (n, t, o, d) ->
+ (fun i (n, t, l, o, d) ->
debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
{ obl_name = n ; obl_body = None;
- obl_type = red t; obl_opaque = o;
+ obl_location = l; obl_type = red t; obl_opaque = o;
obl_deps = d })
obls
in
@@ -346,6 +354,7 @@ let obligations_of_evars evars =
(fun (n, t) ->
{ obl_name = n;
obl_type = t;
+ obl_location = dummy_loc;
obl_body = None;
obl_opaque = false;
obl_deps = Intset.empty;
@@ -397,7 +406,7 @@ and solve_obligation_by_tac prg obls i tac =
Some _ -> false
| None ->
(try
- if deps_remaining obls obl.obl_deps = [] then
+ if deps_remaining obls obl.obl_deps = [] then
let obl = subst_deps_obl obls obl in
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
if obl.obl_opaque then
@@ -405,8 +414,12 @@ and solve_obligation_by_tac prg obls i tac =
else
obls.(i) <- { obl with obl_body = Some t };
true
- else false
- with _ -> false)
+ else false
+ with
+ | Stdpp.Exc_located(_, Refiner.FailError (_, s))
+ | Refiner.FailError (_, s) ->
+ user_err_loc (obl.obl_location, "solve_obligation", s)
+ | e -> false)
and solve_prg_obligations prg tac =
let obls, rem = prg.prg_obligations in
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 8ed6ce7e44..997c2479de 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,8 +1,8 @@
open Names
open Util
-type obligation_info = (Names.identifier * Term.types * bool * Intset.t) array
- (* ident, type, opaque or transparent, dependencies *)
+type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
+ (* ident, type, location, opaque or transparent, dependencies *)
type progress = (* Resolution status of a program *)
| Remain of int (* n obligations remaining *)
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 647db2c9c5..4af18f52d3 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -373,7 +373,7 @@ let solve_by_tac evi t =
Pfedit.delete_current_proof (); const.Entries.const_entry_body
with e ->
Pfedit.delete_current_proof();
- raise Exit
+ raise e
(* let apply_tac t goal = t goal *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:03:39 +0000