aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--interp/constrextern.ml7
-rw-r--r--interp/constrintern.ml99
-rw-r--r--interp/constrintern.mli8
-rw-r--r--interp/topconstr.ml2
-rw-r--r--interp/topconstr.mli2
-rw-r--r--parsing/g_constr.ml417
-rw-r--r--parsing/g_vernac.ml418
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/ppconstr.ml19
-rw-r--r--parsing/ppvernac.ml13
-rw-r--r--theories/Classes/EquivDec.v25
-rw-r--r--toplevel/command.ml25
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/record.ml2
25 files changed, 221 insertions, 215 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 *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5047d1b98e..dedaf6af4a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -720,7 +720,12 @@ let rec extern inctx scopes vars r =
let (ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Idset.add) ids vars in
let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
- let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in
+ let n =
+ match fst nv.(i) with
+ | None -> None
+ | Some x -> Some (dummy_loc, out_name (List.nth ids x))
+ in
+ let ro = extern_recursion_order scopes vars (snd nv.(i)) in
(fi, (n, ro), bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fe1fca3489..65efc1f67b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -32,6 +32,8 @@ type var_internalisation_data =
type implicits_env = (identifier * var_internalisation_data) list
type full_implicits_env = identifier list * implicits_env
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
let interning_grammar = ref false
(* Historically for parsing grammar rules, but in fact used only for
@@ -848,23 +850,32 @@ let internalise sigma globalenv env allow_patvar lvar c =
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
let intern_ro_arg c f =
- let before, after = list_chop (succ (Option.get n)) bl in
- let ((ids',_,_),rafter) =
- List.fold_left intern_local_binder (env,[]) after in
- let ro = (intern (ids', tmp_scope, scopes) c) in
- f ro, List.fold_left intern_local_binder (env,rafter) before
+ let idx =
+ match n with
+ Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
+ | None -> 0
+ in
+ let before, after = list_chop idx bl in
+ let ((ids',_,_) as env',rbefore) =
+ List.fold_left intern_local_binder (env,[]) before in
+ let ro =
+ match c with
+ | None -> RStructRec
+ | Some c' -> f (intern (ids', tmp_scope, scopes) c')
+ in
+ let n' = Option.map (fun _ -> List.length before) n in
+ n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
- let ro, ((ids',_,_),rbl) =
+ let n, ro, ((ids',_,_),rbl) =
(match order with
- CStructRec ->
- RStructRec,
- List.fold_left intern_local_binder (env,[]) bl
- | CWfRec c ->
- intern_ro_arg c (fun r -> RWfRec r)
- | CMeasureRec c ->
- intern_ro_arg c (fun r -> RMeasureRec r))
- in
- let ids'' = List.fold_right Idset.add lf ids' in
+ | CStructRec ->
+ intern_ro_arg None (fun _ -> RStructRec)
+ | CWfRec c ->
+ intern_ro_arg (Some c) (fun r -> RWfRec r)
+ | CMeasureRec c ->
+ intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+ in
+ let ids'' = List.fold_right Idset.add lf ids' in
((n, ro), List.rev rbl,
intern_type (ids',tmp_scope,scopes) ty,
intern (ids'',None,scopes) bd)) dl in
@@ -1276,45 +1287,43 @@ let my_intern_constr sigma env acc c =
let my_intern_type sigma env acc c = my_intern_constr sigma env (set_type_scope acc) c
-let interp_context sigma env params =
- let ids, bl =
- List.fold_left
- (intern_local_binder_aux (my_intern_constr sigma env) (my_intern_type sigma env))
- ((extract_ids env,None,[]), []) params
- in
+let intern_context sigma env params =
+ snd (List.fold_left
+ (intern_local_binder_aux (my_intern_constr sigma env) (my_intern_type sigma env))
+ ((extract_ids env,None,[]), []) params)
+
+let interp_context_gen understand_type understand_judgment env bl =
+ let (env, par, _, impls) =
List.fold_left
- (fun (env,params) (na, k, b, t) ->
+ (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 = Default.understand_type sigma env t' in
+ let t = understand_type env t' in
let d = (na,None,t) in
- (push_rel d env, d::params)
+ 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 = Default.understand_judgment sigma env b in
+ let c = understand_judgment env b in
let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params))
- (env,[]) (List.rev bl)
+ (push_rel d env,d::params, succ n, impls))
+ (env,[],1,[]) (List.rev bl)
+ in (env, par), impls
+let interp_context sigma env params =
+ let bl = intern_context sigma env params in
+ interp_context_gen (Default.understand_type sigma)
+ (Default.understand_judgment sigma) env bl
+
let interp_context_evars evdref env params =
- let ids, bl =
- List.fold_left
- (intern_local_binder_aux (my_intern_constr evdref env) (my_intern_type evdref env))
- ((extract_ids env,None,[]), []) params
- in
- List.fold_left
- (fun (env,params) (na, k, b, t) ->
- match b with
- None ->
- let t' = locate_if_isevar (loc_of_rawconstr t) na t in
- let t = Default.understand_tcc_evars evdref env IsType t' in
- let d = (na,None,t) in
- (push_rel d env, d::params)
- | Some b ->
- let c = Default.understand_judgment_tcc evdref env b in
- let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env,d::params))
- (env,[]) (List.rev bl)
+ let bl = intern_context (Evd.evars_of !evdref) env params in
+ interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
+ (Default.understand_judgment_tcc evdref) env bl
(**********************************************************************)
(* Locating reference, possibly via an abbreviation *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f81b2ccd16..fb69460c4a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -49,6 +49,8 @@ type manual_implicits = (explicitation * (bool * bool)) list
type ltac_sign = identifier list * unbound_ltac_var_map
+type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
+
(*s Internalisation performs interpretation of global names and notations *)
val intern_constr : evar_map -> env -> constr_expr -> rawconstr
@@ -63,6 +65,8 @@ val intern_pattern : env -> cases_pattern_expr ->
Names.identifier list *
((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list
+val intern_context : evar_map -> env -> local_binder list -> raw_binder list
+
(*s Composing internalisation with pretyping *)
(* Main interpretation function *)
@@ -120,10 +124,10 @@ val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types
(* Interpret contexts: returns extended env and context *)
-val interp_context : evar_map -> env -> local_binder list -> env * rel_context
+val interp_context : evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits
val interp_context_evars :
- evar_defs ref -> env -> local_binder list -> env * rel_context
+ evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
(* Locating references of constructions, possibly via a syntactic definition *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e80065dce1..cad9ad602e 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -585,7 +585,7 @@ type constr_expr =
| CDynamic of loc * Dyn.t
and fixpoint_expr =
- identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and local_binder =
| LocalRawDef of name located * constr_expr
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3094be0e9d..f56550dd5a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -136,7 +136,7 @@ type constr_expr =
| CDynamic of loc * Dyn.t
and fixpoint_expr =
- identifier * (int option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
+ identifier * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
and cofixpoint_expr =
identifier * local_binder list * constr_expr * constr_expr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 41f89a541d..277d8b3c8c 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -43,12 +43,11 @@ let loc_of_binder_let = function
let rec index_and_rec_order_of_annot loc bl ann =
match names_of_local_assums bl,ann with
- | [_], (None, r) -> Some 0, r
- | lids, (Some x, ro) ->
- let ids = List.map snd lids in
- (try Some (list_index0 (snd x) ids), ro
- with Not_found ->
- user_err_loc(fst x,"index_of_annot", Pp.str"no such fix variable"))
+ | [loc,Name id], (None, r) -> Some (loc, id), r
+ | lids, (Some (loc, n), ro) ->
+ if List.exists (fun (_, x) -> x = Name n) lids then
+ Some (loc, n), ro
+ else user_err_loc(loc,"index_of_annot", Pp.str"no such fix variable")
| _, (None, r) -> None, r
let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -370,9 +369,9 @@ GEXTEND Gram
] ]
;
fixannot:
- [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec)
- | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel)
- | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel)
+ [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
+ | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
+ | "{"; IDENT "measure"; rel=constr; id=OPT identref; "}" -> (id, CMeasureRec rel)
] ]
;
binders_let_fixannot:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8285bbad37..76646a4f97 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -263,18 +263,22 @@ GEXTEND Gram
ty = type_cstr;
":="; def = lconstr; ntn = decl_notation ->
let bl, annot = (b :: fst bl, snd bl) in
- let names = List.map snd (names_of_local_assums bl) in
+ let names = names_of_local_assums bl in
let ni =
match fst annot with
- Some (_, id) ->
- (try Some (list_index0 id names)
- with Not_found -> Util.user_err_loc
- (loc,"Fixpoint",
- Pp.str "No argument named " ++ Nameops.pr_name id))
+ Some (loc, id) ->
+ (if List.exists (fun (_, id') -> Name id = id') names then
+ Some (loc, id)
+ else Util.user_err_loc
+ (loc,"Fixpoint",
+ Pp.str "No argument named " ++ Nameops.pr_id id))
| None ->
(* If there is only one argument, it is the recursive one,
otherwise, we search the recursive index later *)
- if List.length names = 1 then Some 0 else None
+ if List.length names = 1 then
+ let (loc, na) = List.hd names in
+ Some (loc, Nameops.out_name na)
+ else None
in
((id,(ni,snd annot),bl,ty,def),ntn) ] ]
;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d9d4139e95..6f6cff2752 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
val binder_let : local_binder Gram.Entry.e
val delimited_binder_let : local_binder Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
- val binders_let_fixannot : (local_binder list * (name located option * recursion_order_expr)) Gram.Entry.e
+ val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
val delimited_binders_let : local_binder list Gram.Entry.e
val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 21c5a343b4..41d98f2bc8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -395,16 +395,15 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
let annot =
- let ids = names_of_local_assums bl in
- match ro with
- CStructRec ->
- if List.length ids > 1 && n <> None then
- spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
- else mt()
- | CWfRec c ->
- spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
- | CMeasureRec c ->
- spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}"
+ match ro with
+ CStructRec ->
+ if List.length bl > 1 && n <> None then
+ spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}"
+ else mt()
+ | CWfRec c ->
+ spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
+ | CMeasureRec c ->
+ spc () ++ str "{measure " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
in
pr_recursive_decl pr prd dangling_with_for id bl annot t c
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 57e21c2ce6..352f58f6ba 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -594,23 +594,18 @@ let rec pr_vernac = function
let annot =
match n with
| None -> mt ()
- | Some n ->
- let name =
- try snd (List.nth ids n)
- with Failure _ ->
- warn (str "non-printable fixpoint \""++pr_id id++str"\"");
- Anonymous in
+ | Some (loc, id) ->
match (ro : Topconstr.recursion_order_expr) with
CStructRec ->
if List.length ids > 1 then
- spc() ++ str "{struct " ++ pr_name name ++ str"}"
+ spc() ++ str "{struct " ++ pr_id id ++ str"}"
else mt()
| CWfRec c ->
spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
- pr_name name ++ str"}"
+ pr_id id ++ str"}"
| CMeasureRec c ->
spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++
- pr_name name ++ str"}"
+ pr_id id ++ str"}"
in
pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 17f8970fc9..62744b1d1a 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -29,12 +29,12 @@ Require Import Coq.Logic.Decidable.
Open Scope equiv_scope.
-Class [ Equivalence A ] => DecidableEquivalence :=
+Class [ equiv : Equivalence A ] => DecidableEquivalence :=
setoid_decidable : forall x y : A, decidable (x === y).
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
-Class [ Equivalence A ] => EqDec :=
+Class [ equiv : Equivalence A ] => EqDec :=
equiv_dec : forall x y : A, { x === y } + { x =/= y }.
(** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -135,3 +135,24 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq
extensionality x.
destruct x ; auto.
Qed.
+
+Require Import List.
+
+Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! EqDec (list A) eq :=
+ equiv_dec :=
+ fix aux (x : list A) y { struct x } :=
+ match x, y with
+ | nil, nil => in_left
+ | cons hd tl, cons hd' tl' =>
+ if hd == hd' then
+ if aux tl tl' then in_left else in_right
+ else in_right
+ | _, _ => in_right
+ end.
+
+ Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
+
+ Next Obligation.
+ Proof. clear aux. red in H0. subst.
+ destruct y; intuition (discriminate || eauto).
+ Defined. \ No newline at end of file
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 860a542f41..7d2a437766 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -510,8 +510,7 @@ let interp_mutual paramsl indl notations finite =
check_all_names_different indl;
let env0 = Global.env() in
let evdref = ref (Evd.create_evar_defs Evd.empty) in
- let userimpls = Implicit_quantifiers.implicits_of_binders paramsl in
- let env_params, ctx_params = interp_context_evars evdref env0 paramsl in
+ let (env_params, ctx_params), userimpls = interp_context_evars evdref env0 paramsl in
let indnames = List.map (fun ind -> ind.ind_name) indl in
(* Names of parameters as arguments of the inductive type (defs removed) *)
@@ -752,7 +751,7 @@ let check_mutuality env kind fixl =
| _ -> ()
type fixpoint_kind =
- | IsFixpoint of (int option * recursion_order_expr) list
+ | IsFixpoint of (identifier located option * recursion_order_expr) list
| IsCoFixpoint
type fixpoint_expr = {
@@ -792,17 +791,19 @@ 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,_) fixl 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,
but doing it properly involves delta-reduction, and it finally
doesn't seem to worth the effort (except for huge mutual
fixpoints ?) *)
- (* FIXME, local_binders_length does not give the size of the final product if typeclasses are used *)
- let m = local_binders_length fixl.fix_binders in
+ let m = List.length fixctx in
let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
list_map_i (fun i _ -> i) 0 ctx
@@ -814,12 +815,8 @@ 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.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 env_rec = push_named_types env fixnames fixtypes in
@@ -849,7 +846,7 @@ let interp_recursive fixkind l boxed =
match fixkind with
| IsFixpoint wfl ->
let possible_indexes =
- list_map3 compute_possible_guardness_evidences wfl fixl fixtypes in
+ list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
let indexes = search_guard dummy_loc env possible_indexes fixdecls in
Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
| IsCoFixpoint ->
diff --git a/toplevel/command.mli b/toplevel/command.mli
index b37c6c359c..8448817f67 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -76,7 +76,7 @@ val declare_mutual_with_eliminations :
mutual_inductive
type fixpoint_kind =
- | IsFixpoint of (int option * recursion_order_expr) list
+ | IsFixpoint of (identifier located option * recursion_order_expr) list
| IsCoFixpoint
type fixpoint_expr = {
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 57a7e63b34..f6815d5379 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -43,7 +43,7 @@ let interp_decl sigma env = function
let typecheck_params_and_fields id t ps fs =
let env0 = Global.env () in
- let env1,newps = interp_context Evd.empty env0 ps in
+ let (env1,newps), _ = interp_context Evd.empty env0 ps in
let fullarity = it_mkProd_or_LetIn t newps in
let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
let env2,newfs =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:18:01 +0000