From 7a39bd5650cc49c5c77788fb42fe2caaf35dfdac Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 6 May 2008 14:05:20 +0000 Subject: Postpone the search for the recursive argument index from the user given name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/funind/indfun.ml | 25 ++------- contrib/interface/xlate.ml | 24 ++------- contrib/subtac/eterm.ml | 9 ++-- contrib/subtac/eterm.mli | 5 +- contrib/subtac/subtac.ml | 2 +- contrib/subtac/subtac_cases.ml | 2 +- contrib/subtac/subtac_coercion.ml | 4 +- contrib/subtac/subtac_command.ml | 87 ++++++++++++++---------------- contrib/subtac/subtac_obligations.ml | 31 +++++++---- contrib/subtac/subtac_obligations.mli | 4 +- contrib/subtac/subtac_utils.ml | 2 +- interp/constrextern.ml | 7 ++- interp/constrintern.ml | 99 +++++++++++++++++++---------------- interp/constrintern.mli | 8 ++- interp/topconstr.ml | 2 +- interp/topconstr.mli | 2 +- parsing/g_constr.ml4 | 17 +++--- parsing/g_vernac.ml4 | 18 ++++--- parsing/pcoq.mli | 2 +- parsing/ppconstr.ml | 19 ++++--- parsing/ppvernac.ml | 13 ++--- theories/Classes/EquivDec.v | 25 ++++++++- toplevel/command.ml | 25 ++++----- toplevel/command.mli | 2 +- toplevel/record.ml | 2 +- 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 = -- cgit v1.2.3