diff options
Diffstat (limited to 'pretyping')
42 files changed, 833 insertions, 881 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c5cf74ccfb..c2c8065a98 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -95,7 +95,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (PatVar (Loc.ghost,Anonymous)) + List.make n (CAst.make @@ PatVar Anonymous) (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *) @@ -122,7 +122,7 @@ type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : Name.t list; - eqn_loc : Loc.t; + eqn_loc : Loc.t option; used : bool ref } type 'a matrix = 'a equation list @@ -178,7 +178,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [PatCstr (Loc.ghost, pci, args, Anonymous)] rh + [CAst.make @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -188,12 +188,12 @@ let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh + feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments") let pop_history h = - feed_history (PatVar (Loc.ghost, Anonymous)) h + feed_history (CAst.make @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -251,7 +251,7 @@ type 'a pattern_matching_problem = tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : Loc.t; + caseloc : Loc.t option; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } @@ -273,16 +273,16 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | PatVar _ :: l -> find_row_ind l - | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) + | { CAst.v = PatVar _ } :: l -> find_row_ind l + | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in let arsign = inductive_alldecls_env env indu in let indu = on_snd EInstance.make indu in let hole_source i = match tmloc with - | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) - | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in + | Some loc -> Loc.tag ~loc @@ Evar_kinds.TomatchTypeParameter (ind,i) + | None -> Loc.tag @@ Evar_kinds.TomatchTypeParameter (ind,i) in let (_,evarl,_) = List.fold_right (fun decl (subst,evarl,n) -> @@ -342,16 +342,16 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames = let find_tomatch_tycon evdref env loc = function (* Try if some 'in I ...' is present and can be used as a constraint *) - | Some (_,ind,realnal) -> + | Some (_,(ind,realnal)) -> mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal) | None -> empty_tycon,None let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = - let loc = Some (loc_of_glob_constr tomatch) in + let loc = loc_of_glob_constr tomatch in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref tomatch in - let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in + let evd, j = Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env !evdref j in evdref := evd; let typ = nf_evar !evdref j.uj_type in let t = @@ -360,7 +360,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = unify_tomatch_with_patterns evdref env loc typ pats realnames in (j.uj_val,t) -let coerce_to_indtype typing_fun evdref env matx tomatchl = +let coerce_to_indtype typing_fun evdref env matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in let matx' = match matrix_transpose pats with | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *) @@ -370,7 +370,7 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl = (************************************************************************) (* Utils *) -let mkExistential env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evdref = +let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e let evd_comb2 f evdref x y = @@ -402,7 +402,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let _ = e_cumul pb.env pb.evdref indt typ in current else - (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env) + (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env) pb.evdref (make_judge current typ) indt).uj_val in let sigma = !(pb.evdref) in (current,try_find_ind pb.env sigma indt names)) @@ -427,9 +427,10 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns") -let alias_of_pat = function - | PatVar (_,name) -> name - | PatCstr(_,_,_,name) -> name +let alias_of_pat = CAst.with_val (function + | PatVar name -> name + | PatCstr(_,_,name) -> name + ) let remove_current_pattern eqn = match eqn.patterns with @@ -468,17 +469,17 @@ let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns } exception NotAdjustable -let rec adjust_local_defs loc = function +let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> - pat :: adjust_local_defs loc (pats,decls) + pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls) + (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable let check_and_adjust_constructor env ind cstrs = function - | PatVar _ as pat -> pat - | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> + | { CAst.v = PatVar _ } as pat -> pat + | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -488,28 +489,28 @@ let check_and_adjust_constructor env ind cstrs = function if Int.equal (List.length args) nb_args_constr then pat else try - let args' = adjust_local_defs loc (args, List.rev ci.cs_args) - in PatCstr (loc, cstr, args', alias) + let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) + in CAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> - error_wrong_numarg_constructor ~loc env cstr nb_args_constr + error_wrong_numarg_constructor ?loc env cstr nb_args_constr else (* Try to insert a coercion *) try - Coercion.inh_pattern_coerce_to loc env pat ind' ind + Coercion.inh_pattern_coerce_to ?loc env pat ind' ind with Not_found -> - error_bad_constructor ~loc env cstr ind + error_bad_constructor ?loc env cstr ind let check_all_variables env sigma typ mat = List.iter (fun eqn -> match current_pattern eqn with - | PatVar (_,id) -> () - | PatCstr (loc,cstr_sp,_,_) -> - error_bad_pattern ~loc env sigma cstr_sp typ) + | { CAst.v = PatVar id } -> () + | { CAst.v = PatCstr (cstr_sp,_,_); loc } -> + error_bad_pattern ?loc env sigma cstr_sp typ) mat let check_unused_pattern env eqn = if not !(eqn.used) then - raise_pattern_matching_error ~loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns) + raise_pattern_matching_error ?loc:eqn.eqn_loc (env, Evd.empty, UnusedClause eqn.patterns) let set_used_pattern eqn = eqn.used := true @@ -529,8 +530,8 @@ let occur_in_rhs na rhs = | Name id -> Id.List.mem id rhs.rhs_vars let is_dep_patt_in eqn = function - | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs - | PatCstr _ -> true + | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | { CAst.v = PatCstr _ } -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -563,31 +564,30 @@ let dependencies_in_rhs sigma nargs current tms eqns = declarations [d(i+1);...;dn] the term [tmi] is dependent in. [find_dependencies_signature (used1,...,usedn) ((tm1,d1),...,(tmn,dn))] - returns [(deps1,...,depsn)] where [depsi] is a subset of n,..,i+1 + returns [(deps1,...,depsn)] where [depsi] is a subset of tm(i+1),..,tmn denoting in which of the d(i+1)...dn, the term tmi is dependent. - Dependencies are expressed by index, e.g. in dependency list - [n-2;1], [1] points to [dn] and [n-2] to [d3] *) let rec find_dependency_list sigma tmblock = function | [] -> [] - | (used,tdeps,d)::rest -> + | (used,tdeps,tm,d)::rest -> let deps = find_dependency_list sigma tmblock rest in if used && List.exists (fun x -> dependent_decl sigma x d) tmblock then - List.add_set Int.equal - (List.length rest + 1) (List.union Int.equal deps tdeps) + match EConstr.kind sigma tm with + | Rel n -> List.add_set Int.equal n (List.union Int.equal deps tdeps) + | _ -> List.union Int.equal deps tdeps else deps let find_dependencies sigma is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist = let deps = find_dependency_list sigma (tm::tmtypleaves) nextlist in if is_dep_or_cstr_in_rhs || not (List.is_empty deps) - then ((true ,deps,d)::nextlist) - else ((false,[] ,d)::nextlist) + then ((true ,deps,tm,d)::nextlist) + else ((false,[] ,tm,d)::nextlist) let find_dependencies_signature sigma deps_in_rhs typs = let l = List.fold_right2 (find_dependencies sigma) deps_in_rhs typs [] in - List.map (fun (_,deps,_) -> deps) l + List.map (fun (_,deps,_,_) -> deps) l (* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |- and xn:Tn has just been regeneralized into x:Tn so that the terms @@ -751,7 +751,7 @@ let recover_and_adjust_alias_names names sign = | x::names, LocalAssum (_,t)::sign -> (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (PatVar (Loc.ghost,na), decl) :: aux (names,sign) + (CAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -961,14 +961,13 @@ let expand_arg tms (p,ccl) ((_,t),_,na) = let k = length_of_tomatch_type_sign na t in (p+k,liftn_predicate (k-1) (p+1) ccl tms) - let use_unit_judge evd = let j, ctx = coq_unit_judge () in let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in + let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in @@ -978,7 +977,7 @@ let add_assert_false_case pb tomatch = avoid_ids = []; it = None }; alias_stack = Anonymous::aliasnames; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false } ] let adjust_impossible_cases pb pred tomatch submat = @@ -1166,8 +1165,8 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (* Sorting equations by constructor *) let rec irrefutable env = function - | PatVar (_,name) -> true - | PatCstr (_,cstr,args,_) -> + | { CAst.v = PatVar name } -> true + | { CAst.v = PatCstr (cstr,args,_) } -> let ind = inductive_of_constructor cstr in let (_,mip) = Inductive.lookup_mind_specif env ind in let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in @@ -1188,14 +1187,14 @@ let group_equations pb ind current cstrs mat = let rest = remove_current_pattern eqn in let pat = current_pattern eqn in match check_and_adjust_constructor pb.env ind cstrs pat with - | PatVar (_,name) -> + | { CAst.v = PatVar name } -> (* This is a default clause that we expand *) for i=1 to Array.length cstrs do let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in brs.(i-1) <- (args, name, rest) :: brs.(i-1) done; if !only_default == None then only_default := Some true - | PatCstr (loc,((_,i)),args,name) -> + | { CAst.v = PatCstr (((_,i)),args,name) ; loc } -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1246,6 +1245,12 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn let typs = List.map2 RelDecl.set_name names cs_args in + (* Beta-iota-normalize types to better compatibility of refine with 8.4 behavior *) + (* This is a bit too strong I think, in the sense that what we would *) + (* really like is to have beta-iota reduction only at the positions where *) + (* parameters are substituted *) + let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in + (* We build the matrix obtained by expanding the matching on *) (* "C x1..xn as x" followed by a residual matching on eqn into *) (* a matching on "x1 .. xn eqn" *) @@ -1535,7 +1540,7 @@ substituer après par les initiaux *) * and linearizing the _ patterns. * Syntactic correctness has already been done in astterm *) let matx_of_eqns env eqns = - let build_eqn (loc,ids,lpat,rhs) = + let build_eqn (loc,(ids,lpat,rhs)) = let initial_lpat,initial_rhs = lpat,rhs in let initial_rhs = rhs in let rhs = @@ -1629,11 +1634,11 @@ let rec list_assoc_in_triple x = function * similarly for each ti. *) -let abstract_tycon loc env evdref subst tycon extenv t = +let abstract_tycon ?loc env evdref subst tycon extenv t = let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with - | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk) - | _ -> (loc,Evar_kinds.CasesType true) in + | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) + | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in (* We traverse the type T of the original problem Xi looking for subterms that match the non-constructor part of the constraints (this part @@ -1687,7 +1692,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = in aux (0,extenv,subst0) t0 -let build_tycon loc env tycon_env s subst tycon extenv evdref t = +let build_tycon ?loc env tycon_env s subst tycon extenv evdref t = let t,tt = match t with | None -> (* This is the situation we are building a return predicate and @@ -1695,10 +1700,10 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context tycon_env) in let impossible_case_type, u = - e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in + e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in (lift (n'-n) impossible_case_type, mkSort u) | Some t -> - let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in + let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in let evd,tt = Typing.type_of extenv !evdref t in evdref := evd; (t,tt) in @@ -1719,16 +1724,16 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = let build_inversion_problem loc env sigma tms t = let make_patvar t (subst,avoid) = let id = next_name_away (named_hd env sigma t Anonymous) avoid in - PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in + CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in let rec reveal_pattern t (subst,avoid as acc) = match EConstr.kind sigma (whd_all env sigma t) with - | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc + | Construct (cstr,u) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_map' reveal_pattern l acc in - PatCstr (Loc.ghost,cstr,l,Anonymous), acc + CAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1786,7 +1791,7 @@ let build_inversion_problem loc env sigma tms t = let main_eqn = { patterns = patl; alias_stack = []; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; (* we assume all vars are used; in practice we discard dependent @@ -1804,9 +1809,9 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl; + [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl; alias_stack = []; - eqn_loc = Loc.ghost; + eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; rhs_vars = []; @@ -1827,7 +1832,7 @@ let build_inversion_problem loc env sigma tms t = mat = main_eqn :: catch_all_eqn; caseloc = loc; casestyle = RegularStyle; - typing_function = build_tycon loc env pb_env s subst} in + typing_function = build_tycon ?loc env pb_env s subst} in let pred = (compile pb).uj_val in (!evdref,pred) @@ -1852,8 +1857,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | None -> (match bo with | None -> [LocalAssum (na, lift n typ)] | Some b -> [LocalDef (na, lift n b, lift n typ)]) - | Some (loc,_,_) -> - user_err ~loc + | Some (loc,_) -> + user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in @@ -1863,9 +1868,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = match t with - | Some (loc,ind',realnal) -> + | Some (loc,(ind',realnal)) -> if not (eq_ind ind ind') then - user_err ~loc (str "Wrong inductive type."); + user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then anomaly (Pp.str "Ill-formed 'in' clause in cases"); List.rev realnal @@ -1880,10 +1885,10 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | _ -> assert false in List.rev (buildrec 0 (tomatchl,tmsign)) -let inh_conv_coerce_to_tycon loc env evdref j tycon = +let inh_conv_coerce_to_tycon ?loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in + let (evd',j) = Coercion.inh_conv_coerce_to ?loc true env !evdref j p in evdref := evd'; j | None -> j @@ -1966,7 +1971,7 @@ let noccur_with_meta sigma n m term = in try (occur_rec n term; true) with LocalOccur -> false -let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = +let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred = let refresh_tycon sigma t = (** If we put the typing constraint in the term, it has to be refreshed to preserve the invariant that no algebraic universe @@ -1997,7 +2002,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = | None -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((t, _), sigma, _) = - new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in + new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in let sigma = Sigma.to_evar_map sigma in sigma, t in @@ -2059,23 +2064,24 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = - GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false), +let hole = CAst.make @@ + GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = - match pat with - | PatVar (l,name) -> + let loc = pat.CAst.loc in + match pat.CAst.v with + | PatVar name -> let name, avoid = match name with Name n -> name, avoid | Anonymous -> let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, id :: avoid in - (PatVar (l, name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) - | PatCstr (l,((_, i) as cstr),args,alias) -> + | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) @@ -2084,7 +2090,7 @@ let constr_of_pat env evdref arsign pat avoid = in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in - if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind; + if not (eq_ind ind cind) then error_bad_constructor ?loc env cstr ind; let cstrs = get_constructors env indf in let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in @@ -2104,7 +2110,7 @@ let constr_of_pat env evdref arsign pat avoid = in let args = List.rev args in let patargs = List.rev patargs in - let pat' = PatCstr (l, cstr, patargs, alias) in + let pat' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in let app = applist (cstr, List.map (lift (List.length sign)) params) in let app = applist (app, args) in @@ -2160,21 +2166,21 @@ let vars_of_ctx sigma ctx = match decl with | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (GApp (Loc.ghost, - (GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)), - [hole; GVar (Loc.ghost, prev)])) :: vars + (CAst.make @@ GApp ( + (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole; CAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, GVar (Loc.ghost, n) :: vars) + | Name n -> n, (CAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y let rec is_included x y = - match x, y with + match CAst.(x.v, y.v) with | PatVar _, _ -> true | _, PatVar _ -> true - | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') -> + | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> if Int.equal i i' then List.for_all2 is_included args args' else false @@ -2289,13 +2295,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = - let bref = GVar (Loc.ghost, branch_name) in + let bref = CAst.make @@ GVar branch_name in match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> GApp (Loc.ghost, bref, l) + | l -> CAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> GApp (Loc.ghost, branch, [ hole ]) + Some _ -> CAst.make @@ GApp (branch, [ hole ]) | None -> branch in incr i; @@ -2438,7 +2444,7 @@ let context_of_arsign l = l ([], 0) in x -let compile_program_cases loc style (typing_function, evdref) tycon env +let compile_program_cases ?loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) = let typing_fun tycon env = function | Some t -> typing_function tycon env evdref t @@ -2545,9 +2551,9 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (**************************************************************************) (* Main entry of the matching compilation *) -let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = +let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) = if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then - compile_program_cases loc style (typing_fun, evdref) + compile_program_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) else @@ -2564,7 +2570,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e with the type of arguments to match; if none is provided, we build alternative possible predicates *) let arsign = extract_arity_signature env tomatchs tomatchl in - let preds = prepare_predicate loc typing_fun env !evdref tomatchs arsign tycon predopt in + let preds = prepare_predicate ?loc typing_fun env !evdref tomatchs arsign tycon predopt in let compile_for_one_predicate (sigma,nal,pred) = (* We push the initial terms to match and push their alias to rhs' envs *) @@ -2614,7 +2620,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e let j = compile pb in (* We coerce to the tycon (if an elim predicate was provided) *) - let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in + let j = inh_conv_coerce_to_tycon ?loc env myevdref j tycon in evdref := !myevdref; j in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 6c2b5bf68b..b16342db4b 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -38,7 +38,7 @@ val irrefutable : env -> cases_pattern -> bool (** {6 Compilation primitive. } *) val compile_cases : - Loc.t -> case_style -> + ?loc:Loc.t -> case_style -> (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> glob_constr option * tomatch_tuples * cases_clauses -> @@ -65,7 +65,7 @@ type 'a equation = { patterns : cases_pattern list; rhs : 'a rhs; alias_stack : Name.t list; - eqn_loc : Loc.t; + eqn_loc : Loc.t option; used : bool ref } type 'a matrix = 'a equation list @@ -106,14 +106,14 @@ type 'a pattern_matching_problem = tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; - caseloc : Loc.t; + caseloc : Loc.t option; casestyle : case_style; typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } val compile : 'a pattern_matching_problem -> unsafe_judgment -val prepare_predicate : Loc.t -> +val prepare_predicate : ?loc:Loc.t -> (Evarutil.type_constraint -> Environ.env -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) -> Environ.env -> diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index e18625c427..782552583d 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -175,6 +175,19 @@ let cofixp_reducible flgs _ stk = else false +let debug_cbv = ref false +let _ = Goptions.declare_bool_option { + Goptions.optdepr = false; + Goptions.optname = "cbv visited constants display"; + Goptions.optkey = ["Debug";"Cbv"]; + Goptions.optread = (fun () -> !debug_cbv); + Goptions.optwrite = (fun a -> debug_cbv:=a); +} + +let pr_key = function + | ConstKey (sp,_) -> Names.Constant.print sp + | VarKey id -> Names.Id.print id + | RelKey n -> Pp.(str "REL_" ++ int n) (* The main recursive functions * @@ -254,9 +267,17 @@ let rec norm_head info env t stack = and norm_head_ref k info env stack normt = if red_set_ref (info_flags info) normt then match ref_value_cache info normt with - | Some body -> strip_appl (shift_value k body) stack - | None -> (VAL(0,make_constr_ref k normt),stack) - else (VAL(0,make_constr_ref k normt),stack) + | Some body -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + strip_appl (shift_value k body) stack + | None -> + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + else + begin + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + (VAL(0,make_constr_ref k normt),stack) + end (* cbv_stack_term performs weak reduction on constr t under the subs * env, with context stack, i.e. ([env]t stack). First computes weak diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index b014af2c7f..eb25994bef 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Environ open CClosure diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 632ba0d9cd..9a973cff55 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -17,7 +17,6 @@ open Nametab open Environ open Libobject open Term -open Termops open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -388,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) = old_inheritance_graph end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in - if is_ambig && is_verbose () then + if is_ambig && not !quiet then Feedback.msg_info (message_ambig !ambig_paths) type coercion = { @@ -429,8 +428,7 @@ let automatically_import_coercions = ref false open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic import of coercions"; optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); @@ -557,7 +555,6 @@ module CoercionPrinting = let member_message x b = str "Explicit printing of coercion " ++ printer x ++ str (if b then " is set" else " is unset") - let synchronous = true end module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 0d741a5a5d..c4238e8b0d 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Evd diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 542db7fdfa..3ef17912f7 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -22,7 +22,6 @@ open Environ open EConstr open Vars open Reductionops -open Typeops open Pretype_errors open Classops open Evarutil @@ -34,14 +33,13 @@ open Globnames let use_typeclasses_for_conversion = ref true let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - optdepr = false; + Goptions.(declare_bool_option + { optdepr = false; optname = "use typeclass resolution during conversion"; optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; optread = (fun () -> !use_typeclasses_for_conversion); optwrite = (fun b -> use_typeclasses_for_conversion := b) } - + ) (* Typing operations dealing with coercions *) exception NoCoercion @@ -75,24 +73,25 @@ let apply_coercion_args env evd check isproj argl funj = !evdref, res (* appliquer le chemin de coercions de patterns p *) -let apply_pattern_coercion loc pat p = +let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> - let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in - Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous)) + let f i = + if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in + CAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) -let inh_pattern_coerce_to loc env pat ind1 ind2 = +let inh_pattern_coerce_to ?loc env pat ind1 ind2 = let p = lookup_pattern_path_between env (ind1,ind2) in - apply_pattern_coercion loc pat p + apply_pattern_coercion ?loc pat p (* Program coercions *) open Program -let make_existential loc ?(opaque = not (get_proofs_transparency ())) env evdref c = - let src = (loc, Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in +let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) env evdref c = + let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in Evarutil.e_new_evar env evdref ~src c let app_opt env evdref f t = @@ -141,7 +140,7 @@ let mu env evdref t = | None -> (None, v) in aux t -and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) +and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) : (EConstr.constr -> EConstr.constr) option = let open Context.Rel.Declaration in @@ -182,7 +181,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential loc env evdref eq in + let evar = make_existential ?loc env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -325,7 +324,7 @@ and coerce loc env evdref (x : EConstr.constr) (y : EConstr.constr) Some (fun x -> let cx = app_opt env evdref c x in - let evar = make_existential loc env evdref (mkApp (p, [| cx |])) + let evar = make_existential ?loc env evdref (mkApp (p, [| cx |])) in (papp evdref sig_intro [| u; p; cx; evar |])) | None -> @@ -339,9 +338,9 @@ let app_coercion env evdref coercion v = let v' = Typing.e_solve_evars env evdref (f v) in whd_betaiota !evdref v' -let coerce_itf loc env evd v t c1 = +let coerce_itf ?loc env evd v t c1 = let evdref = ref evd in - let coercion = coerce loc env evdref t c1 in + let coercion = coerce ?loc env evdref t c1 in let t = Option.map (app_coercion env evdref coercion) v in !evdref, t @@ -409,16 +408,16 @@ let type_judgment env sigma j = | Sort s -> {utj_val = j.uj_val; utj_type = ESorts.kind sigma s } | _ -> error_not_a_type env sigma j -let inh_tosort_force loc env evd j = +let inh_tosort_force ?loc env evd j = try let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in let j2 = on_judgment_type (whd_evar evd) j1 in (evd,type_judgment env evd j2) with Not_found | NoCoercion -> - error_not_a_type ~loc env evd j + error_not_a_type ?loc env evd j -let inh_coerce_to_sort loc env evd j = +let inh_coerce_to_sort ?loc env evd j = let typ = whd_all env evd j.uj_type in match EConstr.kind evd typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = ESorts.kind evd s }) @@ -426,9 +425,9 @@ let inh_coerce_to_sort loc env evd j = let (evd',s) = Evardefine.define_evar_as_sort env evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) | _ -> - inh_tosort_force loc env evd j + inh_tosort_force ?loc env evd j -let inh_coerce_to_base loc env evd j = +let inh_coerce_to_base ?loc env evd j = if Flags.is_program_mode () then let evdref = ref evd in let ct, typ' = mu env evdref j.uj_type in @@ -438,7 +437,7 @@ let inh_coerce_to_base loc env evd j = in !evdref, res else (evd, j) -let inh_coerce_to_prod loc env evd t = +let inh_coerce_to_prod ?loc env evd t = if Flags.is_program_mode () then let evdref = ref evd in let _, typ' = mu env evdref t in @@ -465,7 +464,7 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = try (the_conv_x_leq env t' c1 evd, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = +let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail env evd rigidonly v t c1 @@ -479,57 +478,58 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = (* We eta-expand (hence possibly modifying the original term!) *) (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) (* has type forall (x:u1), u2 (with v' recursively obtained) *) - (* Note: we retype the term because sort-polymorphism may have *) - (* weaken its type *) + (* Note: we retype the term because template polymorphism may have *) + (* weakened its type *) let name = match name with | Anonymous -> Name Namegen.default_dependent_ident | _ -> name in let open Context.Rel.Declaration in let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = - inh_conv_coerce_to_fail loc env1 evd rigidonly + inh_conv_coerce_to_fail ?loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in let v1 = Option.get v1 in let v2 = Option.map (fun v -> beta_applist evd' (lift 1 v,[v1])) v in let t2 = match v2 with | None -> subst_term evd' v1 t2 | Some v2 -> Retyping.get_type_of env1 evd' v2 in - let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in + let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = +let inh_conv_coerce_to_gen ?loc resolve_tc rigidonly env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if Flags.is_program_mode () then - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + coerce_itf ?loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> - error_actual_type ~loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in try if evd' == evd then - error_actual_type ~loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e else - inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type ~loc env best_failed_evd cj t e + error_actual_type ?loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) -let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false -let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true +let inh_conv_coerce_to ?loc resolve_tc = inh_conv_coerce_to_gen ?loc resolve_tc false + +let inh_conv_coerce_rigid_to ?loc resolve_tc = inh_conv_coerce_to_gen resolve_tc ?loc true -let inh_conv_coerces_to loc env evd t t' = +let inh_conv_coerces_to ?loc env evd t t' = try - fst (inh_conv_coerce_to_fail loc env evd true None t t') + fst (inh_conv_coerce_to_fail ?loc env evd true None t t') with NoCoercion -> evd (* Maybe not enough information to unify *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index bc63d092d9..ab1f6c110f 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -8,7 +8,6 @@ open Evd open Names -open Term open Environ open EConstr open Glob_term @@ -26,17 +25,17 @@ val inh_app_fun : bool -> (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a sort; it fails if no coercion is applicable *) -val inh_coerce_to_sort : Loc.t -> +val inh_coerce_to_sort : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type its base type (the notion depends on the coercion system) *) -val inh_coerce_to_base : Loc.t -> +val inh_coerce_to_base : ?loc:Loc.t -> env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) -val inh_coerce_to_prod : Loc.t -> +val inh_coerce_to_prod : ?loc:Loc.t -> env -> evar_map -> types -> evar_map * types (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an @@ -44,20 +43,20 @@ val inh_coerce_to_prod : Loc.t -> a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) -val inh_conv_coerce_to : bool -> Loc.t -> +val inh_conv_coerce_to : ?loc:Loc.t -> bool -> env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment -val inh_conv_coerce_rigid_to : bool -> Loc.t -> +val inh_conv_coerce_rigid_to : ?loc:Loc.t -> bool -> env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) -val inh_conv_coerces_to : Loc.t -> +val inh_conv_coerces_to : ?loc:Loc.t -> env -> evar_map -> types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; raises [Not_found] if no coercion found *) val inh_pattern_coerce_to : - Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern + ?loc:Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index efe03bc2e9..2cb837ba03 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -83,32 +83,70 @@ let add_binders na1 na2 binding_vars (names, terms as subst) = let rec build_lambda sigma vars ctx m = match vars with | [] -> - let len = List.length ctx in - EConstr.Vars.lift (-1 * len) m + if Vars.closed0 sigma m then m else raise PatternMatchingFailure | n :: vars -> - let open EConstr in (* change [ x1 ... xn y z1 ... zm |- t ] into [ x1 ... xn z1 ... zm |- lam y. t ] *) - let len = List.length ctx in - let init i = - if i < pred n then mkRel (i + 2) - else if Int.equal i (pred n) then mkRel 1 - else mkRel (i + 1) - in - let m = Vars.substl (List.init len init) m in let pre, suf = List.chop (pred n) ctx in - match suf with + let (na, t, suf) = match suf with | [] -> assert false - | (_, na, t) :: suf -> - let map i = if i > n then pred i else i in - let vars = List.map map vars in - (** Check that the abstraction is legal *) - let frels = free_rels sigma t in - let brels = List.fold_right Int.Set.add vars Int.Set.empty in - let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in - (** Create the abstraction *) - let m = mkLambda (na, t, m) in - build_lambda sigma vars (pre @ suf) m + | (_, na, t) :: suf -> (na, t, suf) + in + (** Check that the abstraction is legal by generating a transitive closure of + its dependencies. *) + let is_nondep t clear = match clear with + | [] -> true + | _ -> + let rels = free_rels sigma t in + let check i b = b || not (Int.Set.mem i rels) in + List.for_all_i check 1 clear + in + let fold (_, _, t) clear = is_nondep t clear :: clear in + (** Produce a list of booleans: true iff we keep the hypothesis *) + let clear = List.fold_right fold pre [false] in + let clear = List.drop_last clear in + (** If the conclusion depends on a variable we cleared, failure *) + let () = if not (is_nondep m clear) then raise PatternMatchingFailure in + (** Create the abstracted term *) + let fold (k, accu) keep = + if keep then + let k = succ k in + (k, Some k :: accu) + else (k, None :: accu) + in + let keep, shift = List.fold_left fold (0, []) clear in + let shift = List.rev shift in + let map = function + | None -> mkProp (** dummy term *) + | Some i -> mkRel (i + 1) + in + (** [x1 ... xn y z1 ... zm] -> [x1 ... xn f(z1) ... f(zm) y] *) + let subst = + List.map map shift @ + mkRel 1 :: + List.mapi (fun i _ -> mkRel (i + keep + 2)) suf + in + let map i (id, na, c) = + let i = succ i in + let subst = List.skipn i subst in + let subst = List.map (fun c -> Vars.lift (- i) c) subst in + (id, na, substl subst c) + in + let pre = List.mapi map pre in + let pre = List.filter_with clear pre in + let m = substl subst m in + let map i = + if i > n then i - n + keep + else match List.nth shift (i - 1) with + | None -> + (** We cleared a variable that we wanted to abstract! *) + raise PatternMatchingFailure + | Some k -> k + in + let vars = List.map map vars in + (** Create the abstraction *) + let m = mkLambda (na, Vars.lift keep t, m) in + build_lambda sigma vars (pre @ suf) m let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu @@ -182,9 +220,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PSoApp (n,args),m -> let fold (ans, seen) = function | PRel n -> - let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in + let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in (n :: ans, Int.Set.add n seen) - | _ -> error "Only bound indices allowed in second order pattern matching." + | _ -> user_err (str "Only bound indices allowed in second order pattern matching.") in let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in let frels = free_rels sigma cT in @@ -323,6 +361,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> + Array.fold_left2 (sorec ctx env) subst args1 args2 | _ -> raise PatternMatchingFailure in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 8ba4086795..752819aa39 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Term -open Environ open EConstr open Vars open Inductiveops @@ -29,8 +28,6 @@ open Misctypes open Decl_kinds open Context.Named.Declaration -let dl = Loc.ghost - (** Should we keep details of universes during detyping ? *) let print_universes = Flags.univ_print @@ -70,14 +67,14 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 let encode_bool r = let (x,lc) = encode_inductive r in if not (has_two_constructors lc) then - user_err ~loc:(loc_of_reference r) ~hdr:"encode_if" + user_err ?loc:(loc_of_reference r) ~hdr:"encode_if" (str "This type has not exactly two constructors."); x let encode_tuple r = let (x,lc) = encode_inductive r in if not (isomorphic_to_tuple lc) then - user_err ~loc:(loc_of_reference r) ~hdr:"encode_tuple" + user_err ?loc:(loc_of_reference r) ~hdr:"encode_tuple" (str "This type cannot be seen as a tuple type."); x @@ -136,8 +133,7 @@ let wildcard_value = ref true let force_wildcard () = !wildcard_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; optread = force_wildcard; @@ -147,8 +143,7 @@ let synth_type_value = ref true let synthetize_type () = !synth_type_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; optread = synthetize_type; @@ -158,8 +153,7 @@ let reverse_matching_value = ref true let reverse_matching () = !reverse_matching_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; optread = reverse_matching; @@ -169,8 +163,7 @@ let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; optread = print_primproj_params; @@ -180,8 +173,7 @@ let print_primproj_compatibility_value = ref false let print_primproj_compatibility () = !print_primproj_compatibility_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "backwards-compatible printing of primitive projections"; optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; optread = print_primproj_compatibility; @@ -285,7 +277,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = (avoid', add_name_opt na' body t env) sigma c let rec build_tree na isgoal e sigma ci cl = - let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = CAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in let cna = ci.ci_cstr_nargs in List.flatten @@ -308,7 +300,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with List.map (fun (hd,rest) -> pat::hd,rest) lines) clauses) | _ -> - let pat = PatVar(dl,update_name sigma na rhs) in + let pat = CAst.make @@ PatVar(update_name sigma na rhs) in let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat @@ -331,20 +323,20 @@ let is_nondep_branch sigma c l = let extract_nondep_branches test c b l = let rec strip l r = - match r,l with - | r, [] -> r - | GLambda (_,_,_,_,t), false::l -> strip l t - | GLetIn (_,_,_,_,t), true::l -> strip l t + match r.CAst.v, l with + | r', [] -> r + | GLambda (_,_,_,t), false::l -> strip l t + | GLetIn (_,_,_,t), true::l -> strip l t (* FIXME: do we need adjustment? *) | _,_ -> assert false in if test c l then Some (strip l b) else None let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = - match c, l with + match c.CAst.v, l with | _, [] -> (List.rev nal,c) - | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c - | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c + | GLambda (na,_,_,c), false::l -> aux l (na::nal) c + | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c | _, false::l -> (* eta-expansion *) @@ -355,11 +347,11 @@ let it_destRLambda_or_LetIn_names l c = x in let x = next (free_glob_vars c) in - let a = GVar (dl,x) in + let a = CAst.make @@ GVar x in aux l (Name x :: nal) (match c with - | GApp (loc,p,l) -> GApp (loc,p,l@[a]) - | _ -> (GApp (dl,c,[a]))) + | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a]) + | _ -> CAst.make @@ GApp (c,[a])) in aux l [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -375,12 +367,12 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | None -> Anonymous, None, None | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match typ with - | GLambda (_,x,_,t,c) -> x, c + let n,typ = match typ.CAst.v with + | GLambda (x,_,t,c) -> x, c | _ -> Anonymous, typ in let aliastyp = if List.for_all (Name.equal Anonymous) nl then None - else Some (dl,indsp,nl) in + else Some (Loc.tag (indsp,nl)) in n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in @@ -402,20 +394,20 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | LetStyle, None -> let bl' = Array.map detype bl in let (nal,d) = it_destRLambda_or_LetIn_names constagsl.(0) bl'.(0) in - GLetTuple (dl,nal,(alias,pred),tomatch,d) + GLetTuple (nal,(alias,pred),tomatch,d) | IfStyle, None -> let bl' = Array.map detype bl in let nondepbrs = Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in if Array.for_all ((!=) None) nondepbrs then - GIf (dl,tomatch,(alias,pred), + GIf (tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else let eqnl = detype_eqns constructs constagsl bl in - GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) + GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> let eqnl = detype_eqns constructs constagsl bl in - GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl) + GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) let detype_sort sigma = function | Prop Null -> GProp @@ -423,7 +415,9 @@ let detype_sort sigma = function | Type u -> GType (if !print_universes - then [dl, Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u)] + then + let u = Pp.string_of_ppcmds (Univ.Universe.pr_with (Termops.pr_evd_level sigma) u) in + [Loc.tag @@ Name.mk_name (Id.of_string_soft u)] else []) type binder_kind = BProd | BLambda | BLetIn @@ -431,36 +425,37 @@ type binder_kind = BProd | BLambda | BLetIn (**********************************************************************) (* Main detyping function *) -let detype_anonymous = ref (fun loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) +let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index to an anonymous variable")) let set_detype_anonymous f = detype_anonymous := f let detype_level sigma l = - GType (Some (dl, Pp.string_of_ppcmds (Termops.pr_evd_level sigma l))) + let l = Pp.string_of_ppcmds (Termops.pr_evd_level sigma l) in + GType (Some (Loc.tag @@ Name.mk_name (Id.of_string_soft l))) let detype_instance sigma l = let l = EInstance.kind sigma l in if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) -let rec detype flags avoid env sigma t = +let rec detype flags avoid env sigma t = CAst.make @@ match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with - | Name id -> GVar (dl, id) - | Anonymous -> !detype_anonymous dl n + | Name id -> GVar id + | Anonymous -> (!detype_anonymous n).CAst.v with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) - in GVar (dl, Id.of_string s)) + in GVar (Id.of_string s)) | Meta n -> (* Meta in constr are not user-parsable and are mapped to Evar *) (* using numbers to be unparsable *) - GEvar (dl, Id.of_string ("M" ^ string_of_int n), []) + GEvar (Id.of_string ("M" ^ string_of_int n), []) | Var id -> - (try let _ = Global.lookup_named id in GRef (dl, VarRef id, None) - with Not_found -> GVar (dl, id)) - | Sort s -> GSort (dl,detype_sort sigma (ESorts.kind sigma s)) + (try let _ = Global.lookup_named id in GRef (VarRef id, None) + with Not_found -> GVar id) + | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> - detype flags avoid env sigma c1 + (detype flags avoid env sigma c1).CAst.v | Cast (c1,k,c2) -> let d1 = detype flags avoid env sigma c1 in let d2 = detype flags avoid env sigma c2 in @@ -469,34 +464,34 @@ let rec detype flags avoid env sigma t = | NATIVEcast -> CastNative d2 | _ -> CastConv d2 in - GCast(dl,d1,cast) + GCast(d1,cast) | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> let mkapp f' args' = - match f' with - | GApp (dl',f',args'') -> - GApp (dl,f',args''@args') - | _ -> GApp (dl,f',args') + match f'.CAst.v with + | GApp (f',args'') -> + GApp (f',args''@args') + | _ -> GApp (f',args') in mkapp (detype flags avoid env sigma f) (Array.map_to_list (detype flags avoid env sigma) args) - | Const (sp,u) -> GRef (dl, ConstRef sp, detype_instance sigma u) + | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = let pb = Environ.lookup_projection p (snd env) in let pars = pb.Declarations.proj_npars in - let hole = GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in + let hole = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in let args = List.make pars hole in - GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), + GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), (args @ [detype flags avoid env sigma c])) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () with _ -> (* lax mode, used by debug printers only *) - GApp (dl, GRef (dl, ConstRef (Projection.constant p), None), + GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), [detype flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then @@ -514,12 +509,12 @@ let rec detype flags avoid env sigma t = substl (c :: List.rev args) body' with Retyping.RetypeError _ | Not_found -> anomaly (str"Cannot detype an unfolded primitive projection.") - in detype flags avoid env sigma c' + in (detype flags avoid env sigma c').CAst.v else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in - detype flags avoid env sigma c + (detype flags avoid env sigma c).CAst.v with Retyping.RetypeError _ -> noparams () else noparams () @@ -546,12 +541,12 @@ let rec detype flags avoid env sigma t = Id.of_string ("X" ^ string_of_int (Evar.repr evk)), (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in - GEvar (dl,id, + GEvar (id, List.map (on_snd (detype flags avoid env sigma)) l) | Ind (ind_sp,u) -> - GRef (dl, IndRef ind_sp, detype_instance sigma u) + GRef (IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,u) -> - GRef (dl, ConstructRef cstr_sp, detype_instance sigma u) + GRef (ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in detype_case comp (detype flags avoid env sigma) @@ -574,7 +569,7 @@ and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let v = Array.map3 (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in - GRec(dl,GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -590,7 +585,7 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) = let v = Array.map2 (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t)) bodies tys in - GRec(dl,GCoFix n,Array.of_list (List.rev lfi), + GRec(GCoFix n,Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) @@ -635,7 +630,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c)) + List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list @@ -644,17 +639,17 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = let make_pat x avoid env b body ty ids = if force_wildcard () && noccurn sigma 1 b then - PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids + CAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids else let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in let na,avoid' = compute_displayed_name_in sigma flag avoid x b in - PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na + CAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na in let rec buildrec ids patlist avoid env l b = match EConstr.kind sigma b, l with - | _, [] -> - (dl, Id.Set.elements ids, - [PatCstr(dl, constr, List.rev patlist,Anonymous)], + | _, [] -> Loc.tag @@ + (Id.Set.elements ids, + [CAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], detype flags avoid env sigma b) | Lambda (x,t,b), false::l -> let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in @@ -668,7 +663,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran buildrec ids patlist avoid env l c | _, true::l -> - let pat = PatVar (dl,Anonymous) in + let pat = CAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -690,14 +685,14 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = | _ -> compute_displayed_name_in sigma flag avoid na c in let r = detype flags avoid' (add_name na' body ty env) sigma c in match bk with - | BProd -> GProd (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r) - | BLambda -> GLambda (dl, na',Explicit,detype (lax,false) avoid env sigma ty, r) + | BProd -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r) + | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r) | BLetIn -> let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in - GLetIn (dl, na', c, t, r) + let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in + GLetIn (na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in @@ -741,11 +736,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | Name id -> Name (convert_id cl id) | Anonymous -> Anonymous in - let rec detype_closed_glob cl = function - | GVar (loc,id) -> + let rec detype_closed_glob cl cg : Glob_term.glob_constr = CAst.map (function + | GVar id -> (* if [id] is bound to a name. *) begin try - GVar(loc,Id.Map.find id cl.idents) + GVar(Id.Map.find id cl.idents) (* if [id] is bound to a typed term *) with Not_found -> try (* assumes [detype] does not raise [Not_found] exceptions *) @@ -755,127 +750,128 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = [Printer.pr_constr_under_binders_env] does. *) let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in let env = push_rel_context assums env in - detype ?lax isgoal avoid env sigma c + (detype ?lax isgoal avoid env sigma c).CAst.v (* if [id] is bound to a [closed_glob_constr]. *) with Not_found -> try let {closure;term} = Id.Map.find id cl.untyped in - detype_closed_glob closure term + (detype_closed_glob closure term).CAst.v (* Otherwise [id] stands for itself *) with Not_found -> - GVar(loc,id) + GVar id end - | GLambda (loc,id,k,t,c) -> + | GLambda (id,k,t,c) -> let id = convert_name cl id in - GLambda(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c) - | GProd (loc,id,k,t,c) -> + GLambda(id,k,detype_closed_glob cl t, detype_closed_glob cl c) + | GProd (id,k,t,c) -> let id = convert_name cl id in - GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c) - | GLetIn (loc,id,b,t,e) -> + GProd(id,k,detype_closed_glob cl t, detype_closed_glob cl c) + | GLetIn (id,b,t,e) -> let id = convert_name cl id in - GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e) - | GLetTuple (loc,ids,(n,r),b,e) -> + GLetIn(id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e) + | GLetTuple (ids,(n,r),b,e) -> let ids = List.map (convert_name cl) ids in let n = convert_name cl n in - GLetTuple (loc,ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e) - | GCases (loc,sty,po,tml,eqns) -> + GLetTuple (ids,(n,r),detype_closed_glob cl b, detype_closed_glob cl e) + | GCases (sty,po,tml,eqns) -> let (tml,eqns) = Glob_ops.map_pattern_binders (fun na -> convert_name cl na) tml eqns in let (tml,eqns) = Glob_ops.map_pattern (fun c -> detype_closed_glob cl c) tml eqns in - GCases(loc,sty,po,tml,eqns) + GCases(sty,po,tml,eqns) | c -> - Glob_ops.map_glob_constr (detype_closed_glob cl) c + (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v + ) cg in detype_closed_glob t.closure t.term (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst pat = - match pat with - | PatVar _ -> pat - | PatCstr (loc,((kn,i),j),cpl,n) -> +let rec subst_cases_pattern subst = CAst.map (function + | PatVar _ as pat -> pat + | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn and cpl' = List.smartmap (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else - PatCstr (loc,((kn',i),j),cpl',n) + PatCstr (((kn',i),j),cpl',n) + ) let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst raw = - match raw with - | GRef (loc,ref,u) -> +let rec subst_glob_constr subst = CAst.map (function + | GRef (ref,u) as raw -> let ref',t = subst_global subst ref in if ref' == ref then raw else - detype false [] (Global.env()) Evd.empty (EConstr.of_constr t) + (detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)).CAst.v - | GVar _ -> raw - | GEvar _ -> raw - | GPatVar _ -> raw + | GSort _ + | GVar _ + | GEvar _ + | GPatVar _ as raw -> raw - | GApp (loc,r,rl) -> + | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r and rl' = List.smartmap (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else - GApp(loc,r',rl') + GApp(r',rl') - | GLambda (loc,n,bk,r1,r2) -> + | GLambda (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else - GLambda (loc,n,bk,r1',r2') + GLambda (n,bk,r1',r2') - | GProd (loc,n,bk,r1,r2) -> + | GProd (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in if r1' == r1 && r2' == r2 then raw else - GProd (loc,n,bk,r1',r2') + GProd (n,bk,r1',r2') - | GLetIn (loc,n,r1,t,r2) -> + | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr subst r1 in - let t' = Option.smartmap (subst_glob_constr subst) t in let r2' = subst_glob_constr subst r2 in + let t' = Option.smartmap (subst_glob_constr subst) t in if r1' == r1 && t == t' && r2' == r2 then raw else - GLetIn (loc,n,r1',t',r2') + GLetIn (n,r1',t',r2') - | GCases (loc,sty,rtno,rl,branches) -> + | GCases (sty,rtno,rl,branches) as raw -> let rtno' = Option.smartmap (subst_glob_constr subst) rtno and rl' = List.smartmap (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in let topt' = Option.smartmap - (fun (loc,(sp,i),y as t) -> + (fun ((loc,((sp,i),y) as t)) -> let sp' = subst_mind subst sp in - if sp == sp' then t else (loc,(sp',i),y)) topt in + if sp == sp' then t else (loc,((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl and branches' = List.smartmap - (fun (loc,idl,cpl,r as branch) -> + (fun (loc,(idl,cpl,r) as branch) -> let cpl' = List.smartmap (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else - (loc,idl,cpl',r')) + (loc,(idl,cpl',r'))) branches in if rtno' == rtno && rl' == rl && branches' == branches then raw else - GCases (loc,sty,rtno',rl',branches') + GCases (sty,rtno',rl',branches') - | GLetTuple (loc,nal,(na,po),b,c) -> + | GLetTuple (nal,(na,po),b,c) as raw -> let po' = Option.smartmap (subst_glob_constr subst) po and b' = subst_glob_constr subst b and c' = subst_glob_constr subst c in if po' == po && b' == b && c' == c then raw else - GLetTuple (loc,nal,(na,po'),b',c') + GLetTuple (nal,(na,po'),b',c') - | GIf (loc,c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) as raw -> let po' = Option.smartmap (subst_glob_constr subst) po and b1' = subst_glob_constr subst b1 and b2' = subst_glob_constr subst b2 and c' = subst_glob_constr subst c in if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else - GIf (loc,c',(na,po'),b1',b2') + GIf (c',(na,po'),b1',b2') - | GRec (loc,fix,ida,bl,ra1,ra2) -> + | GRec (fix,ida,bl,ra1,ra2) as raw -> let ra1' = Array.smartmap (subst_glob_constr subst) ra1 and ra2' = Array.smartmap (subst_glob_constr subst) ra2 in let bl' = Array.smartmap @@ -885,11 +881,9 @@ let rec subst_glob_constr subst raw = if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else - GRec (loc,fix,ida,bl',ra1',ra2') - - | GSort _ -> raw + GRec (fix,ida,bl',ra1',ra2') - | GHole (loc, knd, naming, solve) -> + | GHole (knd, naming, solve) as raw -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -898,25 +892,26 @@ let rec subst_glob_constr subst raw = in let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw - else GHole (loc, nknd, naming, nsolve) + else GHole (nknd, naming, nsolve) - | GCast (loc,r1,k) -> + | GCast (r1,k) as raw -> let r1' = subst_glob_constr subst r1 in let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in - if r1' == r1 && k' == k then raw else GCast (loc,r1',k') + if r1' == r1 && k' == k then raw else GCast (r1',k') + ) (* Utilities to transform kernel cases to simple pattern-matching problem *) let simple_cases_matrix_of_branches ind brs = List.map (fun (i,n,b) -> let nal,c = it_destRLambda_or_LetIn_names n b in - let mkPatVar na = PatVar (Loc.ghost,na) in - let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = CAst.make @@ PatVar na in + let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let map name = try Some (Nameops.out_name name) with Failure _ -> None in let ids = List.map_filter map nal in - (Loc.ghost,ids,[p],c)) + Loc.tag @@ (ids,[p],c)) brs let return_type_of_predicate ind nrealargs_tags pred = let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in - (List.hd nal, Some (Loc.ghost, ind, List.tl nal)), Some p + (List.hd nal, Some (Loc.tag (ind, List.tl nal))), Some p diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 4c6f9129f6..da287ae9f0 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -35,14 +35,6 @@ val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> cons val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr -val detype_case : - bool -> (constr -> glob_constr) -> - (constructor array -> bool list array -> constr array -> - (Loc.t * Id.t list * cases_pattern list * glob_constr) list) -> - (constr -> bool list -> bool) -> - Id.t list -> inductive * case_style * bool list array * bool list -> - constr option -> constr -> constr array -> glob_constr - val detype_sort : evar_map -> sorts -> glob_sort val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> @@ -54,7 +46,9 @@ val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> cl val lookup_name_as_displayed : env -> evar_map -> constr -> Id.t -> int option val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option -val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit +(* XXX: This is a hack and should go away *) +val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit + val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4bb66b8e91..bf62cea6b6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -21,7 +21,6 @@ open Recordops open Evarutil open Evardefine open Evarsolve -open Globnames open Evd open Pretype_errors open Sigma.Notations @@ -35,7 +34,7 @@ type unify_fun = transparent_state -> let debug_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states sent to Evarconv unification"; Goptions.optkey = ["Debug";"Unification"]; @@ -43,6 +42,31 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_unification:=a); } +(*******************************************) +(* Functions to deal with impossible cases *) +(*******************************************) +(* XXX: we would like to search for this with late binding + "data.id.type" etc... *) +let impossible_default_case () = + let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in + let (_, u) = Term.destConst c in + Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) + +let coq_unit_judge = + let open Environ in + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in + let na1 = Name (Id.of_string "A") in + let na2 = Name (Id.of_string "H") in + fun () -> + match impossible_default_case () with + | Some (id, type_of_id, ctx) -> + make_judge id type_of_id, ctx + | None -> + (* In case the constants id/ID are not defined *) + Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) + (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + Univ.ContextSet.empty + let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then @@ -352,7 +376,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = match ground_test with | Some result -> result | None -> - (* Until pattern-unification is used consistently, use nohdbeta to not + (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) let term1 = apprec_nohdbeta (fst ts) env evd term1 in let term2 = apprec_nohdbeta (fst ts) env evd term2 in @@ -888,7 +912,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else - let dloc = (Loc.ghost,Evar_kinds.InternalHole) in + let dloc = Loc.tag Evar_kinds.InternalHole in let i = Sigma.Unsafe.of_evar_map i in let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in let i' = Sigma.to_evar_map i' in @@ -1052,7 +1076,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> - error "Cannot force abstraction on identity instance." + user_err Pp.(str "Cannot force abstraction on identity instance.") | None -> make_subst (ctxt',l,occsl) end @@ -1071,7 +1095,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let set_var k = match occs with | Some Locus.AllOccurrences -> mkVar id - | Some _ -> error "Selection of specific occurrences not supported" + | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in @@ -1109,10 +1133,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* This is an arbitrary choice *) let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> error "Cannot find an instance" + | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> evd else @@ -1214,7 +1238,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let error_cannot_unify env evd pb ?reason t1 t2 = Pretype_errors.error_cannot_unify - ~loc:(loc_of_conv_pb evd pb) env + ?loc:(loc_of_conv_pb evd pb) env evd ?reason (t1, t2) let check_problems_are_solved env evd = @@ -1246,7 +1270,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | None -> evd | Some (evk,ev_info,l) -> let rec aux = function - | [] -> error "Unsolvable existential variables." + | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> try let conv_algo = evar_conv_x ts in @@ -1268,7 +1292,7 @@ let solve_unconstrained_impossible_cases env evd = match ev_info.evar_source with | loc,Evar_kinds.ImpossibleCase -> let j, ctx = coq_unit_judge () in - let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in + let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in let evd' = check_evar_instance evd' evk ty conv_algo in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index fc07f0fbea..45857df2ae 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Environ open Reductionops @@ -81,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool -> Evarsolve.unification_result (**/**) +(** {6 Functions to deal with impossible cases } *) +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index c5ae684e3b..a116198465 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -11,7 +11,6 @@ open Pp open Names open Term open Termops -open Environ open EConstr open Vars open Namegen @@ -181,7 +180,7 @@ let define_evar_as_sort env evd (ev,args) = constraint on its domain and codomain. If the input constraint is an evar instantiate it with the product of 2 new evars. *) -let split_tycon loc env evd tycon = +let split_tycon ?loc env evd tycon = let rec real_split evd c = let t = Reductionops.whd_all env evd c in match EConstr.kind evd t with @@ -193,7 +192,7 @@ let split_tycon loc env evd tycon = | App (c,args) when isEvar evd c -> let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in real_split evd' (mkApp (lam,args)) - | _ -> error_not_product ~loc env evd c + | _ -> error_not_product ?loc env evd c in match tycon with | None -> evd,(Anonymous,None,None) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 2f7ac4efbe..b8134a28c5 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -31,7 +31,7 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> evar_map * existential val split_tycon : - Loc.t -> env -> evar_map -> type_constraint -> + ?loc:Loc.t -> env -> evar_map -> type_constraint -> evar_map * (Name.t * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 77086d046c..98e71c7fd9 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module CVars = Vars open Util open CErrors open Names @@ -471,23 +470,13 @@ let free_vars_and_rels_up_alias_expansion sigma aliases c = (* Managing pattern-unification *) (********************************) -let map_all f l = - let rec map_aux f l = match l with - | [] -> [] - | x :: l -> - match f x with - | None -> raise Exit - | Some y -> y :: map_aux f l - in - try Some (map_aux f l) with Exit -> None - let expand_and_check_vars sigma aliases l = let map a = match get_alias_chain_of sigma aliases a with | None, [] -> Some a | None, a :: _ -> Some a | Some _, _ -> None in - map_all map l + Option.List.map map l let alias_distinct l = let rec check (rels, vars) = function @@ -541,7 +530,7 @@ let is_unification_pattern_meta env evd nb m l t = | Rel n -> if n <= nb then Some (RelAlias n) else None | _ -> None in - match map_all map l with + match Option.List.map map l with | Some l -> begin match find_unification_pattern_args env evd l t with | Some _ as x when not (dependent evd (mkMeta m) t) -> x @@ -551,10 +540,10 @@ let is_unification_pattern_meta env evd nb m l t = None let is_unification_pattern_evar env evd (evk,args) l t = - match map_all (fun c -> to_alias evd c) l with + match Option.List.map (fun c -> to_alias evd c) l with | Some l when noccur_evar env evd evk t -> let args = remove_instance_local_defs evd evk args in - let args = map_all (fun c -> to_alias evd c) args in + let args = Option.List.map (fun c -> to_alias evd c) args in begin match args with | None -> None | Some args -> @@ -1061,7 +1050,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = | None -> None,candidates | Some filter -> restrict_hyps evd evk filter candidates in match candidates,filter with - | UpdateWith [], _ -> error "Not solvable." + | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) @@ -1241,7 +1230,7 @@ let check_evar_instance evd evk1 body conv_algo = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> error "Ill-typed evar instance" + with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with | Success evd -> evd diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index e3d3b74f10..d22f94e4e5 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -7,7 +7,6 @@ (************************************************************************) open Locus -open Term open Evd open Pretype_errors open Environ diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ebbfa195f0..923d7d9388 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -15,19 +15,17 @@ open Glob_term (* Untyped intermediate terms, after ASTs and before constr. *) -let cases_pattern_loc = function - PatVar(loc,_) -> loc - | PatCstr(loc,_,_,_) -> loc +let cases_pattern_loc c = c.CAst.loc let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] - | (tm,(na,Some (_,_,nal))) -> na::nal) tml) + | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp loc p t = - match p with - | GApp (loc,f,l) -> GApp (loc,f,l@[t]) - | _ -> GApp (loc,p,[t]) +let mkGApp ?loc p t = CAst.make ?loc @@ + match p.CAst.v with + | GApp (f,l) -> GApp (f,l@[t]) + | _ -> GApp (p,[t]) let map_glob_decl_left_to_right f (na,k,obd,ty) = let comp1 = Option.map f obd in @@ -47,9 +45,9 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | _ -> false -let rec cases_pattern_eq p1 p2 = match p1, p2 with -| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2 -| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) -> +let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with +| PatVar na1, PatVar na2 -> Name.equal na1 na2 +| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && Name.equal na1 na2 | _ -> false @@ -61,57 +59,57 @@ let cast_type_eq eq t1 t2 = match t1, t2 with | CastNative t1, CastNative t2 -> eq t1 t2 | _ -> false -let rec glob_constr_eq c1 c2 = match c1, c2 with -| GRef (_, gr1, _), GRef (_, gr2, _) -> eq_gr gr1 gr2 -| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2 -| GEvar (_, id1, arg1), GEvar (_, id2, arg2) -> +let rec glob_constr_eq { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with +| GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 +| GVar id1, GVar id2 -> Id.equal id1 id2 +| GEvar (id1, arg1), GEvar (id2, arg2) -> Id.equal id1 id2 && List.equal instance_eq arg1 arg2 -| GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) -> +| GPatVar (b1, pat1), GPatVar (b2, pat2) -> (b1 : bool) == b2 && Id.equal pat1 pat2 -| GApp (_, f1, arg1), GApp (_, f2, arg2) -> +| GApp (f1, arg1), GApp (f2, arg2) -> glob_constr_eq f1 f2 && List.equal glob_constr_eq arg1 arg2 -| GLambda (_, na1, bk1, t1, c1), GLambda (_, na2, bk2, t2, c2) -> +| GLambda (na1, bk1, t1, c1), GLambda (na2, bk2, t2, c2) -> Name.equal na1 na2 && binding_kind_eq bk1 bk2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) -> +| GProd (na1, bk1, t1, c1), GProd (na2, bk2, t2, c2) -> Name.equal na1 na2 && binding_kind_eq bk1 bk2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) -> +| GLetIn (na1, b1, t1, c1), GLetIn (na2, b2, t2, c2) -> Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) -> +| GCases (st1, c1, tp1, cl1), GCases (st2, c2, tp2, cl2) -> case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && List.equal tomatch_tuple_eq tp1 tp2 && List.equal cases_clause_eq cl1 cl2 -| GLetTuple (_, na1, (n1, p1), c1, t1), GLetTuple (_, na2, (n2, p2), c2, t2) -> +| GLetTuple (na1, (n1, p1), c1, t1), GLetTuple (na2, (n2, p2), c2, t2) -> List.equal Name.equal na1 na2 && Name.equal n1 n2 && Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && glob_constr_eq t1 t2 -| GIf (_, m1, (pat1, p1), c1, t1), GIf (_, m2, (pat2, p2), c2, t2) -> +| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) -> glob_constr_eq m1 m2 && Name.equal pat1 pat2 && Option.equal glob_constr_eq p1 p2 && glob_constr_eq c1 c2 && glob_constr_eq t1 t2 -| GRec (_, kn1, id1, decl1, c1, t1), GRec (_, kn2, id2, decl2, c2, t2) -> +| GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) -> fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 && Array.equal glob_constr_eq c1 c2 && Array.equal glob_constr_eq t1 t2 -| GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2 -| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) -> +| GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 +| GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) -> Option.equal (==) gn1 gn2 (** Only thing sensible *) && Miscops.intro_pattern_naming_eq nam1 nam2 -| GCast (_, c1, t1), GCast (_, c2, t2) -> +| GCast (c1, t1), GCast (c2, t2) -> glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 | _ -> false and tomatch_tuple_eq (c1, p1) (c2, p2) = - let eqp (_, i1, na1) (_, i2, na2) = + let eqp (_, (i1, na1)) (_, (i2, na2)) = eq_ind i1 i2 && List.equal Name.equal na1 na2 in let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in glob_constr_eq c1 c2 && eq_pred p1 p2 -and cases_clause_eq (_, id1, p1, c1) (_, id2, p2, c2) = +and cases_clause_eq (_, (id1, p1, c1)) (_, (id2, p2, c2)) = List.equal Id.equal id1 id2 && List.equal cases_pattern_eq p1 p2 && glob_constr_eq c1 c2 @@ -139,202 +137,148 @@ and fix_recursion_order_eq o1 o2 = match o1, o2 with and instance_eq (x1,c1) (x2,c2) = Id.equal x1 x2 && glob_constr_eq c1 c2 -let map_glob_constr_left_to_right f = function - | GApp (loc,g,args) -> +let map_glob_constr_left_to_right f = CAst.map (function + | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in - GApp (loc,comp1,comp2) - | GLambda (loc,na,bk,ty,c) -> + GApp (comp1,comp2) + | GLambda (na,bk,ty,c) -> let comp1 = f ty in let comp2 = f c in - GLambda (loc,na,bk,comp1,comp2) - | GProd (loc,na,bk,ty,c) -> + GLambda (na,bk,comp1,comp2) + | GProd (na,bk,ty,c) -> let comp1 = f ty in let comp2 = f c in - GProd (loc,na,bk,comp1,comp2) - | GLetIn (loc,na,b,t,c) -> + GProd (na,bk,comp1,comp2) + | GLetIn (na,b,t,c) -> let comp1 = f b in let compt = Option.map f t in let comp2 = f c in - GLetIn (loc,na,comp1,compt,comp2) - | GCases (loc,sty,rtntypopt,tml,pl) -> + GLetIn (na,comp1,compt,comp2) + | GCases (sty,rtntypopt,tml,pl) -> let comp1 = Option.map f rtntypopt in let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in - let comp3 = Util.List.map_left (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl in - GCases (loc,sty,comp1,comp2,comp3) - | GLetTuple (loc,nal,(na,po),b,c) -> + let comp3 = Util.List.map_left (fun (loc,(idl,p,c)) -> (loc,(idl,p,f c))) pl in + GCases (sty,comp1,comp2,comp3) + | GLetTuple (nal,(na,po),b,c) -> let comp1 = Option.map f po in let comp2 = f b in let comp3 = f c in - GLetTuple (loc,nal,(na,comp1),comp2,comp3) - | GIf (loc,c,(na,po),b1,b2) -> + GLetTuple (nal,(na,comp1),comp2,comp3) + | GIf (c,(na,po),b1,b2) -> let comp1 = Option.map f po in let comp2 = f b1 in let comp3 = f b2 in - GIf (loc,f c,(na,comp1),comp2,comp3) - | GRec (loc,fk,idl,bl,tyl,bv) -> + GIf (f c,(na,comp1),comp2,comp3) + | GRec (fk,idl,bl,tyl,bv) -> let comp1 = Array.map (Util.List.map_left (map_glob_decl_left_to_right f)) bl in let comp2 = Array.map f tyl in let comp3 = Array.map f bv in - GRec (loc,fk,idl,comp1,comp2,comp3) - | GCast (loc,c,k) -> + GRec (fk,idl,comp1,comp2,comp3) + | GCast (c,k) -> let comp1 = f c in let comp2 = Miscops.map_cast_type f k in - GCast (loc,comp1,comp2) + GCast (comp1,comp2) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x + ) let map_glob_constr = map_glob_constr_left_to_right let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt -let fold_glob_constr f acc = function +let fold_glob_constr f acc = CAst.with_val (function | GVar _ -> acc - | GApp (_,c,args) -> List.fold_left f (f acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) -> + | GApp (c,args) -> List.fold_left f (f acc c) args + | GLambda (_,_,b,c) | GProd (_,_,b,c) -> f (f acc b) c - | GLetIn (_,_,b,t,c) -> + | GLetIn (_,b,t,c) -> f (Option.fold_left f (f acc b) t) c - | GCases (_,_,rtntypopt,tml,pl) -> - let fold_pattern acc (_,idl,p,c) = f acc c in + | GCases (_,rtntypopt,tml,pl) -> + let fold_pattern acc (_,(idl,p,c)) = f acc c in List.fold_left fold_pattern (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml)) pl - | GLetTuple (_,_,rtntyp,b,c) -> + | GLetTuple (_,rtntyp,b,c) -> f (f (fold_return_type f acc rtntyp) b) c - | GIf (_,c,rtntyp,b1,b2) -> + | GIf (c,rtntyp,b1,b2) -> f (f (f (fold_return_type f acc rtntyp) c) b1) b2 - | GRec (_,_,_,bl,tyl,bv) -> + | GRec (_,_,bl,tyl,bv) -> let acc = Array.fold_left (List.fold_left (fun acc (na,k,bbd,bty) -> f (Option.fold_left f acc bbd) bty)) acc bl in Array.fold_left f (Array.fold_left f acc tyl) bv - | GCast (_,c,k) -> + | GCast (c,k) -> let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc + ) -let iter_glob_constr f = fold_glob_constr (fun () -> f) () +let fold_return_type_with_binders f g v acc (na,tyopt) = + Option.fold_left (f (name_fold g na v)) acc tyopt -let same_id na id = match na with -| Anonymous -> false -| Name id' -> Id.equal id id' +let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function + | GVar _ -> acc + | GApp (c,args) -> List.fold_left (f v) (f v acc c) args + | GLambda (na,_,b,c) | GProd (na,_,b,c) -> + f (name_fold g na v) (f v acc b) c + | GLetIn (na,b,t,c) -> + f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c + | GCases (_,rtntypopt,tml,pl) -> + let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in + let fold_tomatch (v',acc) (tm,(na,onal)) = + (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'') + (name_fold g na v') onal, + f v acc tm) in + let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in + let acc = Option.fold_left (f v') acc rtntypopt in + List.fold_left fold_pattern acc pl + | GLetTuple (nal,rtntyp,b,c) -> + f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c + | GIf (c,rtntyp,b1,b2) -> + f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 + | GRec (_,idl,bll,tyl,bv) -> + let f' i acc fid = + let v,acc = + List.fold_left + (fun (v,acc) (na,k,bbd,bty) -> + (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty)) + (v,acc) + bll.(i) in + f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in + Array.fold_left_i f' acc idl + | GCast (c,k) -> + let acc = match k with + | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in + f v acc c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc)) + +let iter_glob_constr f = fold_glob_constr (fun () -> f) () let occur_glob_constr id = - let rec occur = function - | GVar (loc,id') -> Id.equal id id' - | GApp (loc,f,args) -> (occur f) || (List.exists occur args) - | GLambda (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GProd (loc,na,bk,ty,c) -> - (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,t,c) -> - (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) - | GCases (loc,sty,rtntypopt,tml,pl) -> - (occur_option rtntypopt) - || (List.exists (fun (tm,_) -> occur tm) tml) - || (List.exists occur_pattern pl) - | GLetTuple (loc,nal,rtntyp,b,c) -> - occur_return_type rtntyp id - || (occur b) || (not (List.mem_f Name.equal (Name id) nal) && (occur c)) - | GIf (loc,c,rtntyp,b1,b2) -> - occur_return_type rtntyp id || (occur c) || (occur b1) || (occur b2) - | GRec (loc,fk,idl,bl,tyl,bv) -> - not (Array.for_all4 (fun fid bl ty bd -> - let rec occur_fix = function - [] -> not (occur ty) && (Id.equal fid id || not(occur bd)) - | (na,k,bbd,bty)::bl -> - not (occur bty) && - (match bbd with - Some bd -> not (occur bd) - | _ -> true) && - (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in - occur_fix bl) - idl bl tyl bv) - | GCast (loc,c,k) -> (occur c) || (match k with CastConv t - | CastVM t | CastNative t -> occur t | CastCoerce -> false) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false - - and occur_pattern (loc,idl,p,c) = not (Id.List.mem id idl) && (occur c) - - and occur_option = function None -> false | Some p -> occur p - - and occur_return_type (na,tyopt) id = not (same_id na id) && occur_option tyopt - - in occur - - -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set + let open CAst in + let rec occur barred acc = function + | { loc ; v = GVar id' } -> Id.equal id id' + | c -> + (* [g] looks if [id] appears in a binding position, in which + case, we don't have to look in the corresponding subterm *) + let g id' barred = barred || Id.equal id id' in + let f barred acc c = acc || not barred && occur false acc c in + fold_glob_constr_with_binders g f barred acc c in + occur false false let free_glob_vars = - let rec vars bounded vs = function - | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs - | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> - let vs' = vars bounded vs ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs' c - | GLetIn (loc,na,b,ty,c) -> - let vs' = vars bounded vs b in - let vs'' = Option.fold_left (vars bounded) vs' ty in - let bounded' = add_name_to_ids bounded na in - vars bounded' vs'' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bounded vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in - List.fold_left (vars_pattern bounded) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 b in - let bounded' = List.fold_left add_name_to_ids bounded nal in - vars bounded' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bounded vs rtntyp in - let vs2 = vars bounded vs1 c in - let vs3 = vars bounded vs2 b1 in - vars bounded vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bounded' = Array.fold_right Id.Set.add idl bounded in - let vars_fix i vs fid = - let vs1,bounded1 = - List.fold_left - (fun (vs,bounded) (na,k,bbd,bty) -> - let vs' = vars_option bounded vs bbd in - let vs'' = vars bounded vs' bty in - let bounded' = add_name_to_ids bounded na in - (vs'',bounded') - ) - (vs,bounded') - bl.(i) - in - let vs2 = vars bounded1 vs1 tyl.(i) in - vars bounded1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bounded vs c in - (match k with CastConv t | CastVM t | CastNative t -> vars bounded v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bounded vs (loc,idl,p,c) = - let bounded' = List.fold_right Id.Set.add idl bounded in - vars bounded' vs c - - and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p - - and vars_return_type bounded vs (na,tyopt) = - let bounded' = add_name_to_ids bounded na in - vars_option bounded' vs tyopt - in + let open CAst in + let rec vars bound vs = function + | { loc ; v = GVar id' } -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs let glob_visible_short_qualid c = let rec aux acc = function - | GRef (_,c,_) -> + | { CAst.v = GRef (c,_) } -> let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in let dir,id = Libnames.repr_qualid qualid in if DirPath.is_empty dir then id :: acc else acc @@ -353,57 +297,16 @@ let add_and_check_ident id set = Id.Set.add id set let bound_glob_vars = - let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> - let bound = name_fold add_and_check_ident na bound in - fold_glob_constr vars bound c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let bound = vars_option bound rtntypopt in - let bound = - List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in - List.fold_left vars_pattern bound pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound b in - let bound = List.fold_right (name_fold add_and_check_ident) nal bound in - vars bound c - | GIf (loc,c,rtntyp,b1,b2) -> - let bound = vars_return_type bound rtntyp in - let bound = vars bound c in - let bound = vars bound b1 in - vars bound b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound = Array.fold_right Id.Set.add idl bound in - let vars_fix i bound fid = - let bound = - List.fold_left - (fun bound (na,k,bbd,bty) -> - let bound = vars_option bound bbd in - let bound = vars bound bty in - name_fold add_and_check_ident na bound - ) - bound - bl.(i) - in - let bound = vars bound tyl.(i) in - vars bound bv.(i) - in - Array.fold_left_i vars_fix bound idl - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound - | GApp _ | GCast _ as c -> fold_glob_constr vars bound c - - and vars_pattern bound (loc,idl,p,c) = - let bound = List.fold_right add_and_check_ident idl bound in - vars bound c - - and vars_option bound = function None -> bound | Some p -> vars bound p - - and vars_return_type bound (na,tyopt) = - let bound = name_fold add_and_check_ident na bound in - vars_option bound tyopt + let rec vars bound = + fold_glob_constr_with_binders + (fun id () -> bound := add_and_check_ident id !bound) + (fun () () -> vars bound) + () () in fun rt -> - vars Id.Set.empty rt + let bound = ref Id.Set.empty in + vars bound rt; + !bound (** Mapping of names in binders *) @@ -413,37 +316,38 @@ let bound_glob_vars = probably be no significant penalty in doing reallocation as pattern-matching expressions are usually rather small. *) -let map_inpattern_binders f ((loc,id,nal) as x) = +let map_inpattern_binders f ((loc,(id,nal)) as x) = let r = CList.smartmap f nal in if r == nal then x - else loc,id,r + else loc,(id,r) let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = function - | PatVar (loc,na) as x -> +let rec map_case_pattern_binders f = CAst.map (function + | PatVar na as x -> let r = f na in if r == na then x - else PatVar (loc,r) - | PatCstr (loc,c,ps,na) as x -> + else PatVar r + | PatCstr (c,ps,na) as x -> let rna = f na in let rps = CList.smartmap (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x - else PatCstr(loc,c,rps,rna) + else PatCstr(c,rps,rna) + ) -let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause = +let map_cases_branch_binders f ((loc,(il,cll,rhs)) as x) : cases_clause = (* spiwack: not sure if I must do something with the list of idents. It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x - else loc,il,r,rhs + else loc,(il,r,rhs) let map_pattern_binders f tomatch branches = CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, @@ -453,29 +357,14 @@ let map_pattern_binders f tomatch branches = let map_tomatch f (c,pp) : tomatch_tuple = f c , pp -let map_cases_branch f (loc,il,cll,rhs) : cases_clause = - loc , il , cll , f rhs +let map_cases_branch f (loc,(il,cll,rhs)) : cases_clause = + loc , (il , cll , f rhs) let map_pattern f tomatch branches = List.map (fun tm -> map_tomatch f tm) tomatch, List.map (fun br -> map_cases_branch f br) branches -let loc_of_glob_constr = function - | GRef (loc,_,_) -> loc - | GVar (loc,_) -> loc - | GEvar (loc,_,_) -> loc - | GPatVar (loc,_) -> loc - | GApp (loc,_,_) -> loc - | GLambda (loc,_,_,_,_) -> loc - | GProd (loc,_,_,_,_) -> loc - | GLetIn (loc,_,_,_,_) -> loc - | GCases (loc,_,_,_,_) -> loc - | GLetTuple (loc,_,_,_,_) -> loc - | GIf (loc,_,_,_,_) -> loc - | GRec (loc,_,_,_,_,_) -> loc - | GSort (loc,_) -> loc - | GHole (loc,_,_,_) -> loc - | GCast (loc,_,_) -> loc +let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) @@ -507,77 +396,78 @@ let rename_var l id = if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else id -let rec rename_glob_vars l = function - | GVar (loc,id) as r -> +let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function + | GVar id as r -> let id' = rename_var l id in - if id == id' then r else GVar (loc,id') - | GRef (_,VarRef id,_) as r -> + if id == id' then r else GVar id' + | GRef (VarRef id,_) as r -> if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming else r - | GProd (loc,na,bk,t,c) -> + | GProd (na,bk,t,c) -> let na',l' = update_subst na l in - GProd (loc,na,bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLambda (loc,na,bk,t,c) -> + GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLambda (na,bk,t,c) -> let na',l' = update_subst na l in - GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLetIn (loc,na,b,t,c) -> + GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c) + | GLetIn (na,b,t,c) -> let na',l' = update_subst na l in - GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c) + GLetIn (na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c) (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) - | GCases (loc,ci,po,tomatchl,cls) -> + | GCases (ci,po,tomatchl,cls) -> let test_pred_pat (na,ino) = - test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in + test_na l na; Option.iter (fun (_,(_,nal)) -> List.iter (test_na l) nal) ino in let test_clause idl = List.iter (test_id l) idl in let po = Option.map (rename_glob_vars l) po in let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in - let cls = Util.List.map_left (fun (loc,idl,p,c) -> test_clause idl; (loc,idl,p,rename_glob_vars l c)) cls in - GCases (loc,ci,po,tomatchl,cls) - | GLetTuple (loc,nal,(na,po),c,b) -> + let cls = Util.List.map_left (fun (loc,(idl,p,c)) -> test_clause idl; (loc,(idl,p,rename_glob_vars l c))) cls in + GCases (ci,po,tomatchl,cls) + | GLetTuple (nal,(na,po),c,b) -> List.iter (test_na l) (na::nal); - GLetTuple (loc,nal,(na,Option.map (rename_glob_vars l) po), + GLetTuple (nal,(na,Option.map (rename_glob_vars l) po), rename_glob_vars l c,rename_glob_vars l b) - | GIf (loc,c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) -> test_na l na; - GIf (loc,rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), + GIf (rename_glob_vars l c,(na,Option.map (rename_glob_vars l) po), rename_glob_vars l b1,rename_glob_vars l b2) - | GRec (loc,k,idl,decls,bs,ts) -> + | GRec (k,idl,decls,bs,ts) -> Array.iter (test_id l) idl; - GRec (loc,k,idl, + GRec (k,idl, Array.map (List.map (fun (na,k,bbd,bty) -> test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls, Array.map (rename_glob_vars l) bs, Array.map (rename_glob_vars l) ts) - | r -> map_glob_constr (rename_glob_vars l) r + | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v + ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = function - | GVar (loc,id) -> +let rec cases_pattern_of_glob_constr na = CAst.map (function + | GVar id -> begin match na with | Name _ -> (* Unable to manage the presence of both an alias and a variable *) raise Not_found - | Anonymous -> PatVar (loc,Name id) + | Anonymous -> PatVar (Name id) end - | GHole (loc,_,_,_) -> PatVar (loc,na) - | GRef (loc,ConstructRef cstr,_) -> - PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | GHole (_,_,_) -> PatVar na + | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) + | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) -> + PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) | _ -> raise Not_found + ) (* Turn a closed cases pattern into a glob_constr *) -let rec glob_constr_of_closed_cases_pattern_aux = function - | PatCstr (loc,cstr,[],Anonymous) -> - GRef (loc,ConstructRef cstr,None) - | PatCstr (loc,cstr,l,Anonymous) -> - let ref = GRef (loc,ConstructRef cstr,None) in - GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l) +let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function + | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None) + | PatCstr (cstr,l,Anonymous) -> + let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in + GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) | _ -> raise Not_found + ) x let glob_constr_of_closed_cases_pattern = function - | PatCstr (loc,cstr,l,na) -> - na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous)) + | { CAst.loc ; v = PatCstr (cstr,l,na) } -> + na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 55e6b6533f..aa48516aff 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -20,12 +20,12 @@ val glob_constr_eq : glob_constr -> glob_constr -> bool (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> Loc.t +val cases_pattern_loc : cases_pattern -> Loc.t option val cases_predicate_names : tomatch_tuples -> Name.t list (** Apply one argument to a glob_constr *) -val mkGApp : Loc.t -> glob_constr -> glob_constr -> glob_constr +val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr @@ -37,11 +37,13 @@ val map_glob_constr_left_to_right : val warn_variable_collision : ?loc:Loc.t -> Id.t -> unit val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a +val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t -val loc_of_glob_constr : glob_constr -> Loc.t +(* Obsolete *) +val loc_of_glob_constr : glob_constr -> Loc.t option val glob_visible_short_qualid : glob_constr -> Id.t list (* Renaming free variables using a renaming map; fails with diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 5b42add285..7f3bafc685 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -97,7 +97,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = and ntypes = mib.mind_ntypes and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in - if j > nconstr then error "Not enough constructors in the type."; + if j > nconstr then user_err Pp.(str "Not enough constructors in the type."); substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1)) (* Number of constructors *) @@ -459,7 +459,6 @@ let extract_mrectype sigma t = | _ -> raise Not_found let find_mrectype_vect env sigma c = - let open EConstr in let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind -> (ind, l) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index e4fbf8d542..211ffbe01e 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -50,9 +50,9 @@ let is_nowhere = function let simple_clause_of enum_hyps cl = let error_occurrences () = - CErrors.error "This tactic does not support occurrences selection" in + CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in let error_body_selection () = - CErrors.error "This tactic does not support body selection" in + CErrors.user_err Pp.(str "This tactic does not support body selection") in let hyps = match cl.onhyps with | None -> diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 7fe81c9a43..69bc2d11ff 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,7 @@ let smartmap_cast_type f c = let glob_sort_eq g1 g2 = match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true -| GType l1, GType l2 -> List.equal (fun x y -> CString.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> List.equal (fun x y -> Names.Name.equal (snd x) (snd y)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with @@ -62,7 +62,7 @@ let map_red_expr_gen f g h = function (** Mapping bindings *) let map_explicit_bindings f l = - let map (loc, hyp, x) = (loc, hyp, f x) in + let map (loc, (hyp, x)) = (loc, (hyp, f x)) in List.map map l let map_bindings f = function diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0228f63cdc..afaa20b6f6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -383,7 +383,7 @@ let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in if Coq_config.no_native_compiler then - error "Native_compute reduction has been disabled at configure time." + user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in (* diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 318f94be24..1c8ad0cddd 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -14,13 +14,11 @@ open Nameops open Term open Vars open Glob_term -open Glob_ops open Pp open Mod_subst open Misctypes open Decl_kinds open Pattern -open Evd open Environ let case_info_pattern_eq i1 i2 = @@ -160,8 +158,11 @@ let pattern_of_constr env sigma t = (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> - PEvar (evk,Array.map (pattern_of_constr env) ctxt) + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) + if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) + else PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> PMeta None) | Case (ci,p,a,br) -> @@ -220,6 +221,8 @@ let instantiate_pattern env sigma lvar c = ctx in let c = substl inst c in + (** FIXME: Stupid workaround to pattern_of_constr being evar sensitive *) + let c = Evarutil.nf_evar sigma c in pattern_of_constr env sigma (EConstr.Unsafe.to_constr c) with Not_found (* List.index failed *) -> let vars = @@ -227,7 +230,7 @@ let instantiate_pattern env sigma lvar c = error_instantiate_pattern id (List.subtract Id.equal ctx vars) with Not_found (* Map.find failed *) -> x) - | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") + | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.") | c -> map_pattern_with_binders (fun id vars -> id::vars) aux vars c in aux [] c @@ -322,46 +325,46 @@ let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" (fun () -> Pp.strbrk "Casts are ignored in patterns") -let rec pat_of_raw metas vars = function - | GVar (_,id) -> +let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function + | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) - | GPatVar (_,(false,n)) -> + | GPatVar (false,n) -> metas := n::!metas; PMeta (Some n) - | GRef (_,gr,_) -> + | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp (_, GPatVar (_,(true,n)), cl) -> + | GApp ({ CAst.v = GPatVar (true,n) }, cl) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | GApp (_,c,cl) -> + | GApp (c,cl) -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) - | GLambda (_,na,bk,c1,c2) -> + | GLambda (na,bk,c1,c2) -> name_iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GProd (_,na,bk,c1,c2) -> + | GProd (na,bk,c1,c2) -> name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GLetIn (_,na,c1,t,c2) -> + | GLetIn (na,c1,t,c2) -> name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) - | GSort (_,s) -> + | GSort s -> PSort s | GHole _ -> PMeta None - | GCast (_,c,_) -> + | GCast (c,_) -> warn_cast_in_pattern (); pat_of_raw metas vars c - | GIf (_,c,(_,None),b1,b2) -> + | GIf (c,(_,None),b1,b2) -> PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) - | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = - GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in + | GLetTuple (nal,(_,None),b,c) -> + let mkGLambda c na = CAst.make ?loc @@ + GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; @@ -372,24 +375,24 @@ let rec pat_of_raw metas vars = function let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in PCase (cip, PMeta None, pat_of_raw metas vars b, [0,tags,pat_of_raw metas vars c]) - | GCases (loc,sty,p,[c,(na,indnames)],brs) -> + | GCases (sty,p,[c,(na,indnames)],brs) -> let get_ind = function - | (_,_,[PatCstr(_,(ind,_),_,_)],_)::_ -> Some ind + | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind | _ -> None in let ind_tags,ind = match indnames with - | Some (_,ind,nal) -> Some (List.length nal), Some ind + | Some (_,(ind,nal)) -> Some (List.length nal), Some ind | None -> None, get_ind brs in let ext,brs = pats_of_glob_branches loc metas vars ind brs in let pred = match p,indnames with - | Some p, Some (_,_,nal) -> + | Some p, Some (_,(_,nal)) -> let nvars = na :: List.rev nal @ vars in rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) - | (None | Some (GHole _)), _ -> PMeta None + | (None | Some { CAst.v = GHole _}), _ -> PMeta None | Some p, None -> - user_err ~loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") + user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; @@ -402,26 +405,27 @@ let rec pat_of_raw metas vars = function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) - | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.") + | r -> err ?loc (Pp.str "Non supported pattern.") + ) and pats_of_glob_branches loc metas vars ind brs = let get_arg = function - | PatVar(_,na) -> + | { CAst.v = PatVar na } -> name_iter (fun n -> metas := n::!metas) na; na - | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.") + | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,_,[PatVar(_,Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *) - | (_,_,[PatCstr(_,(indsp,j),lv,_)],br) :: brs -> + | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *) + | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs -> let () = match ind with | Some sp when eq_ind sp indsp -> () | _ -> - err ~loc (Pp.str "All constructors must be in the same inductive type.") + err ?loc (Pp.str "All constructors must be in the same inductive type.") in if Int.Set.mem (j-1) indexes then - err ~loc + err ?loc (str "No unique branch for " ++ int j ++ str"-th constructor."); let lna = List.map get_arg lv in let vars' = List.rev lna @ vars in @@ -429,7 +433,7 @@ and pats_of_glob_branches loc metas vars ind brs = let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in ext, ((j-1, tags, pat) :: pats) - | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.") + | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.") in get_pat Int.Set.empty brs diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 5694d345c1..791fd74ed3 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Globnames open Glob_term diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 24f6d16899..d7c04b08b0 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names open Term open Environ @@ -177,7 +176,7 @@ let unsatisfiable_constraints env evd ev comp = | Some ev -> let loc, kind = Evd.evar_source ev evd in let err = UnsatisfiableConstraints (Some (ev, kind), comp) in - Loc.raise ~loc (PretypeError (env,evd,err)) + Loc.raise ?loc (PretypeError (env,evd,err)) let unsatisfiable_exception exn = match exn with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ae87cd8c02..e72394fa28 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -33,7 +33,6 @@ open EConstr open Vars open Reductionops open Type_errors -open Typeops open Typing open Globnames open Nameops @@ -133,7 +132,7 @@ let nf_fix sigma (nas, cs, ts) = let inj c = EConstr.to_constr sigma c in (nas, Array.map inj cs, Array.map inj ts) -let search_guard loc env possible_indexes fixdefs = +let search_guard ?loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in @@ -143,7 +142,7 @@ let search_guard loc env possible_indexes fixdefs = (try check_fix env fix with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in iraise (e, info)); indexes else @@ -166,7 +165,7 @@ let search_guard loc env possible_indexes fixdefs = with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in - user_err ~loc ~hdr:"search_guard" (Pp.str errmsg) + user_err ?loc ~hdr:"search_guard" (Pp.str errmsg) with Found indexes -> indexes) (* To force universe name declaration before use *) @@ -176,8 +175,7 @@ let is_strict_universe_declarations () = !strict_universe_declarations let _ = Goptions.(declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict universe declaration"; optkey = ["Strict";"Universe";"Declaration"]; optread = is_strict_universe_declarations; @@ -185,53 +183,58 @@ let _ = let _ = Goptions.(declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "minimization to Set"; optkey = ["Universe";"Minimization";"ToSet"]; optread = Universes.is_set_minimization; optwrite = (:=) Universes.set_minimization }) - + (** Miscellaneous interpretation functions *) -let interp_universe_level_name evd (loc,s) = - let names, _ = Global.global_universe_names () in - if CString.string_contains s "." then - match List.rev (CString.split '.' s) with - | [] -> anomaly (str"Invalid universe name " ++ str s) - | n :: dp -> - let num = int_of_string n in - let dp = DirPath.make (List.map Id.of_string dp) in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - else - try - let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - try - let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Idmap.find id names) - with Not_found -> - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ~loc ~name:s univ_rigid evd - else user_err ~loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ str s)) +let interp_universe_level_name ~anon_rigidity evd (loc, s) = + match s with + | Anonymous -> + new_univ_level_variable ?loc anon_rigidity evd + | Name s -> + let s = Id.to_string s in + let names, _ = Global.global_universe_names () in + if CString.string_contains ~where:s ~what:"." then + match List.rev (CString.split '.' s) with + | [] -> anomaly (str"Invalid universe name " ++ str s) + | n :: dp -> + let num = int_of_string n in + let dp = DirPath.make (List.map Id.of_string dp) in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level + else + try + let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + try + let id = try Id.of_string s with _ -> raise Not_found in + evd, snd (Idmap.find id names) + with Not_found -> + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:s univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ str s)) let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in evd, Univ.Universe.make l | l -> List.fold_left (fun (evd, u) l -> - let evd', l = interp_universe_level_name evd l in + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l -let interp_level_info loc evd : Misctypes.level_info -> _ = function - | None -> new_univ_level_variable ~loc univ_rigid evd - | Some (loc,s) -> interp_universe_level_name evd (loc,s) +let interp_level_info ?loc evd : Misctypes.level_info -> _ = function + | None -> new_univ_level_variable ?loc univ_rigid evd + | Some (loc,s) -> interp_universe_level_name ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) let interp_sort ?loc evd = function | GProp -> evd, Prop Null @@ -337,7 +340,7 @@ let check_extra_evars_are_solved env current_sigma frozen = match frozen with match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - error_unsolvable_implicit ~loc env current_sigma evk None) pending + error_unsolvable_implicit ?loc env current_sigma evk None) pending (* [check_evars] fails if some unresolved evar remains *) @@ -349,7 +352,7 @@ let check_evars env initial_sigma sigma c = let (loc,k) = evar_source evk sigma in begin match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> Pretype_errors.error_unsolvable_implicit ~loc env sigma evk None + | _ -> Pretype_errors.error_unsolvable_implicit ?loc env sigma evk None end | _ -> EConstr.iter sigma proc_rec c in proc_rec c @@ -384,18 +387,18 @@ let process_inference_flags flags env initial_sigma (sigma,c) = let allow_anonymous_refs = ref false (* coerce to tycon if any *) -let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function +let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function | None -> j | Some t -> - evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env.ExtraEnv.env) evdref j t + evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc env.ExtraEnv.env) evdref j t let check_instance loc subst = function | [] -> () | (id,_) :: _ -> if List.mem_assoc id subst then - user_err ~loc (pr_id id ++ str "appears more than once.") + user_err ?loc (pr_id id ++ str "appears more than once.") else - user_err ~loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") + user_err ?loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -475,7 +478,7 @@ let pretype_id pretype k0 loc env evdref lvar id = (* and build a nice error message *) if Id.Map.mem id lvar.ltac_genargs then begin let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in - user_err ~loc + user_err ?loc (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; @@ -484,47 +487,47 @@ let pretype_id pretype k0 loc env evdref lvar id = { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } with Not_found -> (* [id] not found, standard error message *) - error_var_not_found ~loc id + error_var_not_found ?loc id (*************************************************************************) (* Main pretyping function *) -let interp_glob_level loc evd : Misctypes.glob_level -> _ = function +let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set - | GType s -> interp_level_info loc evd s + | GType s -> interp_level_info ?loc evd s -let interp_instance loc evd ~len l = +let interp_instance ?loc evd ~len l = if len != List.length l then - user_err ~loc ~hdr:"pretype" + user_err ?loc ~hdr:"pretype" (str "Universe instance should have length " ++ int len) else let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_glob_level loc evd l in + let evd, l = interp_glob_level ?loc evd l in (evd, l :: univs)) (evd, []) l in if List.exists (fun l -> Univ.Level.is_prop l) l' then - user_err ~loc ~hdr:"pretype" + user_err ?loc ~hdr:"pretype" (str "Universe instances cannot contain Prop, polymorphic" ++ str " universe instances must be greater or equal to Set."); evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) -let pretype_global loc rigid env evd gr us = +let pretype_global ?loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None | Some l -> let _, ctx = Universes.unsafe_constr_of_global gr in let len = Univ.UContext.size ctx in - interp_instance loc evd ~len l + interp_instance ?loc evd ~len l in - let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in + let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in (sigma, EConstr.of_constr c) -let pretype_ref loc evdref env ref us = +let pretype_ref ?loc evdref env ref us = match ref with | VarRef id -> (* Section variable *) @@ -533,24 +536,24 @@ let pretype_ref loc evdref env ref us = (* This may happen if env is a goal env and section variables have been cleared - section variables should be different from goal variables *) - Pretype_errors.error_var_not_found ~loc id) + Pretype_errors.error_var_not_found ?loc id) | ref -> - let evd, c = pretype_global loc univ_flexible env !evdref ref us in + let evd, c = pretype_global ?loc univ_flexible env !evdref ref us in let () = evdref := evd in let ty = unsafe_type_of env.ExtraEnv.env evd c in make_judge c ty -let judge_of_Type loc evd s = - let evd, s = interp_universe ~loc evd s in +let judge_of_Type ?loc evd s = + let evd, s = interp_universe ?loc evd s in let judge = { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in evd, judge -let pretype_sort loc evdref = function +let pretype_sort ?loc evdref = function | GProp -> judge_of_prop | GSet -> judge_of_set - | GType s -> evd_comb1 (judge_of_Type loc) evdref s + | GType s -> evd_comb1 (judge_of_Type ?loc) evdref s let new_type_evar env evdref loc = let sigma = Sigma.Unsafe.of_evar_map !evdref in @@ -561,42 +564,53 @@ let new_type_evar env evdref loc = evdref := Sigma.to_evar_map sigma; e -let (f_genarg_interp, genarg_interp_hook) = Hook.make () +module ConstrInterpObj = +struct + type ('r, 'g, 't) obj = + unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map + let name = "constr_interp" + let default _ = None +end + +module ConstrInterp = Genarg.Register(ConstrInterpObj) + +let register_constr_interp0 = ConstrInterp.register0 (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [evdref] and *) (* the type constraint tycon *) let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t = - let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in + let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in let pretype_type = pretype_type k0 resolve_tc in let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in - match t with - | GRef (loc,ref,u) -> - inh_conv_coerce_to_tycon loc env evdref - (pretype_ref loc evdref env ref u) + let loc = t.CAst.loc in + match t.CAst.v with + | GRef (ref,u) -> + inh_conv_coerce_to_tycon ?loc env evdref + (pretype_ref ?loc evdref env ref u) tycon - | GVar (loc, id) -> - inh_conv_coerce_to_tycon loc env evdref + | GVar id -> + inh_conv_coerce_to_tycon ?loc env evdref (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id) tycon - | GEvar (loc, id, inst) -> + | GEvar (id, inst) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) let evk = try Evd.evar_key id !evdref with Not_found -> - user_err ~loc (str "Unknown existential variable.") in + user_err ?loc (str "Unknown existential variable.") in let hyps = evar_filtered_context (Evd.find !evdref evk) in let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in let c = mkEvar (evk, args) in let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in - inh_conv_coerce_to_tycon loc env evdref j tycon + inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GPatVar (loc,(someta,n)) -> + | GPatVar (someta,n) -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with @@ -605,7 +619,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let k = Evar_kinds.MatchingVar (someta,n) in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } - | GHole (loc, k, naming, None) -> + | GHole (k, naming, None) -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with @@ -614,19 +628,22 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre new_type_evar env evdref loc in { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } - | GHole (loc, k, _naming, Some arg) -> + | GHole (k, _naming, Some arg) -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in + let open Genarg in let ist = lvar.ltac_genargs in - let (c, sigma) = Hook.get f_genarg_interp ty env.ExtraEnv.env !evdref ist arg in + let GenArg (Glbwit tag, arg) = arg in + let interp = ConstrInterp.obj tag in + let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in let () = evdref := sigma in { uj_val = c; uj_type = ty } - | GRec (loc,fixkind,names,bl,lar,vdef) -> + | GRec (fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt | (na,bk,None,ty)::bl -> @@ -674,7 +691,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in - Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; + Typing.check_type_fixpoint ?loc env.ExtraEnv.env evdref names ftys vdefj; let nf c = nf_evar !evdref c in let ftys = Array.map nf ftys in (** FIXME *) let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in @@ -696,7 +713,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) + ?loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls) in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> @@ -705,17 +722,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls) with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info)); make_judge (mkCoFix cofix) ftys.(i) in - inh_conv_coerce_to_tycon loc env evdref fixj tycon + inh_conv_coerce_to_tycon ?loc env evdref fixj tycon - | GSort (loc,s) -> - let j = pretype_sort loc evdref s in - inh_conv_coerce_to_tycon loc env evdref j tycon + | GSort s -> + let j = pretype_sort ?loc evdref s in + inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GApp (loc,f,args) -> + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in let length = List.length args in @@ -775,7 +792,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional - ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref + ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref resj [|hj|] in let resj = apply_rec env 1 fj candargs args in @@ -792,19 +809,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else resj | _ -> resj in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLambda(loc,name,bk,c1,c2) -> + | GLambda(name,bk,c1,c2) -> let tycon' = evd_comb1 (fun evd tycon -> match tycon with | None -> evd, tycon | Some ty -> - let evd, ty' = Coercion.inh_coerce_to_prod loc env.ExtraEnv.env evd ty in + let evd, ty' = Coercion.inh_coerce_to_prod ?loc env.ExtraEnv.env evd ty in evd, Some ty') evdref tycon in - let (name',dom,rng) = evd_comb1 (split_tycon loc env.ExtraEnv.env) evdref tycon' in + let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So @@ -814,9 +831,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GProd(loc,name,bk,c1,c2) -> + | GProd(name,bk,c1,c2) -> let j = pretype_type empty_valcon env evdref lvar c1 in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are @@ -836,11 +853,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre judge_of_product env.ExtraEnv.env name j j' with TypeError _ as e -> let (e, info) = CErrors.push e in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) in - inh_conv_coerce_to_tycon loc env evdref resj tycon + inh_conv_coerce_to_tycon ?loc env evdref resj tycon - | GLetIn(loc,name,c1,t,c2) -> + | GLetIn(name,c1,t,c2) -> let tycon1 = match t with | Some t -> @@ -861,21 +878,21 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } - | GLetTuple (loc,nal,(na,po),c,d) -> + | GLetTuple (nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj + error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 1) then - user_err ~loc (str "Destructing let is only for inductive types" ++ + user_err ?loc (str "Destructing let is only for inductive types" ++ str " with one constructor."); let cs = cstrs.(0) in if not (Int.equal (List.length nal) cs.cs_nargs) then - user_err ~loc:loc (str "Destructing let on this type expects " ++ + user_err ?loc:loc (str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables."); let fsign, record = let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in @@ -944,7 +961,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl else - error_cant_find_case_type ~loc env.ExtraEnv.env !evdref + error_cant_find_case_type ?loc env.ExtraEnv.env !evdref cj.uj_val in (* let ccl = refresh_universes ccl in *) let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in @@ -954,16 +971,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre obj ind p cj.uj_val fj.uj_val in { uj_val = v; uj_type = ccl }) - | GIf (loc,c,(na,po),b1,b2) -> + | GIf (c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in - error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in + error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in let cstrs = get_constructors env.ExtraEnv.env indf in if not (Int.equal (Array.length cstrs) 2) then - user_err ~loc + user_err ?loc (str "If is only for inductive types with two constructors."); let arsgn = @@ -1020,19 +1037,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in - inh_conv_coerce_to_tycon loc env evdref cj tycon + inh_conv_coerce_to_tycon ?loc env evdref cj tycon - | GCases (loc,sty,po,tml,eqns) -> - Cases.compile_cases loc sty + | GCases (sty,po,tml,eqns) -> + Cases.compile_cases ?loc sty ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref lvar),evdref) tycon env.ExtraEnv.env (* loc *) (po,tml,eqns) - | GCast (loc,c,k) -> + | GCast (c,k) -> let cj = match k with | CastCoerce -> let cj = pretype empty_tycon env evdref lvar c in - evd_comb1 (Coercion.inh_coerce_to_base loc env.ExtraEnv.env) evdref cj + evd_comb1 (Coercion.inh_coerce_to_base ?loc env.ExtraEnv.env) evdref cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in @@ -1048,9 +1065,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval + error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) - else user_err ~loc (str "Cannot check cast with vm: " ++ + else user_err ?loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in @@ -1059,7 +1076,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj tval + error_actual_type ?loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> @@ -1067,7 +1084,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } - in inh_conv_coerce_to_tycon loc env evdref cj tycon + in inh_conv_coerce_to_tycon ?loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let f decl (subst,update) = @@ -1087,7 +1104,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = let t' = env |> lookup_named id |> NamedDecl.get_type in if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found with Not_found -> - user_err ~loc (str "Cannot interpret " ++ + user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ str " in current context: no binding for " ++ pr_id id ++ str ".") in ((id,c)::subst, update) in @@ -1097,7 +1114,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function - | GHole (loc, knd, naming, None) -> + | { loc; CAst.v = GHole (knd, naming, None) } -> let rec is_Type c = match EConstr.kind !evdref c with | Sort s -> begin match ESorts.kind !evdref s with @@ -1128,14 +1145,14 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function | c -> let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in - let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env.ExtraEnv.env) evdref j in + let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in match valcon with | None -> tj | Some v -> if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type - ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v + ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f13c10b055..dcacd07209 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -24,7 +24,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) val search_guard : - Loc.t -> env -> int list list -> rec_declaration -> int array + ?loc:Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint @@ -163,6 +163,6 @@ val ise_pretype_gen : val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family -val genarg_interp_hook : - (types -> env -> evar_map -> unbound_ltac_var_map -> - Genarg.glob_generic_argument -> constr * evar_map) Hook.t +val register_constr_interp0 : + ('r, 'g, 't) Genarg.genarg_type -> + (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit diff --git a/pretyping/program.ml b/pretyping/program.ml index caa5a5c8a6..8769c5659e 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -6,27 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Util -open Names -open Term -let make_dir l = DirPath.make (List.rev_map Id.of_string l) - -let find_reference locstr dir s = - let dp = make_dir dir in - let sp = Libnames.make_path dp (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - user_err (str "Library " ++ Libnames.pr_dirpath dp ++ - str " has to be required first.") - -let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s -let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) - -let init_constant dir s () = coq_constant "Program" dir s -let init_reference dir s () = coq_reference "Program" dir s +let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s +let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = let open EConstr in @@ -88,8 +72,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "preferred transparency of Program obligations"; optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; @@ -97,8 +80,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "program cases"; optkey = ["Program";"Cases"]; optread = (fun () -> !program_cases); @@ -106,8 +88,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "program generalized coercion"; optkey = ["Program";"Generalized";"Coercion"]; optread = (fun () -> !program_generalized_coercion); diff --git a/pretyping/redops.ml b/pretyping/redops.ml index 7d65925e57..8e190f40b9 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -20,13 +20,13 @@ let make_red_flag l = | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l } lf | FDeltaBut l :: lf -> if red.rConst <> [] && not red.rDelta then - CErrors.error - "Cannot set both constants to unfold and constants not to unfold"; + CErrors.user_err Pp.(str + "Cannot set both constants to unfold and constants not to unfold"); add_flag { red with rConst = union_consts red.rConst l; rDelta = true } lf diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 2703205386..e7c9635829 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,7 +29,7 @@ exception Elimconst let refolding_in_reduction = ref false let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Perform refolding of fixpoints/constants like cbn during reductions"; Goptions.optkey = ["Refolding";"Reduction"]; @@ -239,6 +239,9 @@ sig | Shift of int | Update of 'a and 'a t = 'a member list + + exception IncompatibleFold2 + val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds val empty : 'a t val is_empty : 'a t -> bool @@ -413,6 +416,7 @@ struct | (_,_) -> false in compare_rec 0 stk1 stk2 + exception IncompatibleFold2 let fold2 f o sk1 sk2 = let rec aux o lft1 sk1 lft2 sk2 = let fold_array = @@ -442,7 +446,7 @@ struct aux o lft1 (List.rev params1) lft2 (List.rev params2) in aux o' lft1' q1 lft2' q2 | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> - raise (Invalid_argument "Reductionops.Stack.fold2") + raise IncompatibleFold2 in aux o 0 (List.rev sk1) 0 (List.rev sk2) let rec map f x = List.map (function @@ -807,7 +811,7 @@ let fix_recarg ((recindices,bodynum),_) stack = let debug_RAKAM = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states of the Reductionops abstract machine"; Goptions.optkey = ["Debug";"RAKAM"]; @@ -1117,7 +1121,9 @@ let local_whd_state_gen flags sigma = whrec let raw_whd_state_gen flags env = - let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in + let f sigma s = fst (whd_state_gen ~refold:(get_refolding_in_reduction ()) + ~tactic_mode:false + flags env sigma s) in f let stack_red_of_state_red f = @@ -1127,7 +1133,7 @@ let stack_red_of_state_red f = (* Drops the Cst_stack *) let iterate_whd_gen refold flags env sigma s = let rec aux t = - let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in + let (hd,sk),_ = whd_state_gen ~refold ~tactic_mode:false flags env sigma (t,Stack.empty) in let whd_sk = Stack.map aux sk in Stack.zip sigma ~refold (hd,whd_sk) in aux s @@ -1213,7 +1219,7 @@ let clos_norm_flags flgs env sigma t = EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let clos_whd_flags flgs env sigma t = try @@ -1221,7 +1227,7 @@ let clos_whd_flags flgs env sigma t = EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 752c30a8ac..af80481569 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -81,8 +81,11 @@ module Stack : sig val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) val compare_shape : 'a t -> 'a t -> bool + + exception IncompatibleFold2 (** [fold2 f x sk1 sk2] folds [f] on any pair of term in [(sk1,sk2)]. - @return the result and the lifts to apply on the terms *) + @return the result and the lifts to apply on the terms + @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *) val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> constr t -> constr t -> 'a * int * int val map : ('a -> 'a) -> 'a t -> 'a t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67221046bd..3d41d2ddd5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -858,7 +858,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "No head constant to reduce." + with Redelimination -> user_err (str "No head constant to reduce.") (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -1080,7 +1080,7 @@ let unfold env sigma name c = if is_evaluable env name then clos_norm_flags (unfold_red name) env sigma c else - error (string_of_evaluable_ref env name^" is opaque.") + user_err Pp.(str (string_of_evaluable_ref env name^" is opaque.")) (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)] * Unfolds the constant name in a term c following a list of occurrences occl. @@ -1090,7 +1090,7 @@ let unfoldoccs env sigma (occs,name) c = let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in if Int.equal nbocc 1 then - error ((string_of_evaluable_ref env name)^" does not occur."); + user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur.")); let rest = List.filter (fun o -> o >= nbocc) locs in let () = match rest with | [] -> () @@ -1112,7 +1112,7 @@ let unfoldn loccname env sigma c = let fold_one_com com env sigma c = let rcom = try red_product env sigma com - with Redelimination -> error "Not reducible." in + with Redelimination -> user_err Pp.(str "Not reducible.") in (* Reason first on the beta-iota-zeta normal form of the constant as unfold produces it, so that the "unfold f; fold f" configuration works to refold fix expressions *) @@ -1147,7 +1147,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env sigma ta Anonymous in - if occur_meta sigma ta then error "Cannot find a type for the generalisation."; + if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); if occur_meta sigma a then mkLambda (na,ta,c), sigma else diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 76d0bc241f..c31212e26a 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open Evd open EConstr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 93c71e6ea9..d7b4842810 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -30,8 +30,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "check that typeclasses proof search returns unique solutions"; optkey = ["Typeclasses";"Unique";"Solutions"]; optread = get_typeclasses_unique_solutions; @@ -423,7 +422,7 @@ let add_class cl = match inst with | Some (Backward, info) -> (match body with - | None -> CErrors.error "Non-definable projection can not be declared as a subinstance" + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") | Some b -> declare_instance (Some info) false (ConstRef b)) | _ -> ()) cl.cl_projs diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 2db0e9e881..754dacd193 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -8,7 +8,6 @@ (*i*) open Names -open Term open EConstr open Environ open Constrexpr diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 9bd430e4d6..558575ccce 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,7 +8,6 @@ open Loc open Names -open Term open EConstr open Environ open Constrexpr diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c2a030bcd2..757e12451e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -152,13 +152,13 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } -let check_type_fixpoint loc env evdref lna lar vdefj = +let check_type_fixpoint ?loc env evdref lna lar vdefj = let lt = Array.length vdefj in if Int.equal (Array.length lar) lt then for i = 0 to lt-1 do if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type (lift lt lar.(i))) then - error_ill_typed_rec_body ~loc env !evdref + error_ill_typed_rec_body ?loc env !evdref i lna vdefj lar done @@ -313,14 +313,13 @@ let rec execute env evdref cstr = let j = match EConstr.kind !evdref f with | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env !evdref (ind, u) jl) | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env -> - (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env !evdref (cst, u) jl) | _ -> + (* No template polymorphism *) execute env evdref f in e_judge_of_apply env evdref j jl @@ -361,7 +360,7 @@ and execute_recdef env evdref (names,lar,vdef) = let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in let vdefv = Array.map j_val vdefj in - let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in + let _ = check_type_fixpoint env1 evdref names lara vdefj in (names,lara,vdefv) and execute_array env evdref = Array.map (execute env evdref) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 91134b4999..1f3ba34e51 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -44,7 +44,7 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> (** Raise an error message if bodies have types not unifiable with the expected ones *) -val check_type_fixpoint : Loc.t -> env -> evar_map ref -> +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> Names.Name.t array -> types array -> unsafe_judgment array -> unit val judge_of_prop : unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 532cc8baa5..d1643a8c7d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -45,7 +45,7 @@ module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Unification is keyed"; Goptions.optkey = ["Keyed";"Unification"]; Goptions.optread = (fun () -> !keyed_unification); @@ -56,7 +56,7 @@ let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states sent to tactic unification"; Goptions.optkey = ["Debug";"Tactic";"Unification"]; @@ -257,8 +257,7 @@ let global_pattern_unification_flag = ref true open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "pattern-unification for existential variables in tactics"; optkey = ["Tactic";"Evars";"Pattern";"Unification"]; optread = (fun () -> !global_pattern_unification_flag); @@ -269,8 +268,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern-unification for existential variables in tactics"; optkey = ["Tactic";"Pattern";"Unification"]; optread = (fun () -> !global_pattern_unification_flag); @@ -1095,7 +1093,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) unirec_rec curenvnb pb opt' substn c1 app - with Invalid_argument "Reductionops.Stack.fold2" -> + with Reductionops.Stack.IncompatibleFold2 -> error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in @@ -1250,9 +1248,9 @@ let applyHead env (type r) (evd : r Sigma.t) n c = let sigma = Sigma.to_evar_map evd in match EConstr.kind sigma (whd_all env sigma cty) with | Prod (_,c1,c2) -> - let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in + let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd' - | _ -> error "Apply_Head_Then" + | _ -> user_err Pp.(str "Apply_Head_Then") in apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd @@ -1265,7 +1263,7 @@ let is_mimick_head sigma ts f = let try_to_coerce env evd c cty tycon = let j = make_judge c cty in - let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in + let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in (evd',j'.uj_val) @@ -1518,7 +1516,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 = let iter_fail f a = let n = Array.length a in let rec ffail i = - if Int.equal i n then error "iter_fail" + if Int.equal i n then user_err Pp.(str "iter_fail") else try f a.(i) with ex when precatchable_exception ex -> ffail (i+1) @@ -1535,9 +1533,6 @@ let indirectly_dependent sigma c d decls = way to see that the second hypothesis depends indirectly over 2 *) List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls -let indirect_dependency sigma d decls = - decls |> List.filter (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id - let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let current_sigma = Sigma.to_evar_map current_sigma in let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in @@ -1759,8 +1754,8 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = w_typed_unify_array env evd flags f1 l1 f2 l2,cl else w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> - bestexn := Some ex; error "Unsat") - else error "Bound 1" + bestexn := Some ex; user_err Pp.(str "Unsat")) + else user_err Pp.(str "Bound 1") with ex when precatchable_exception ex -> (match EConstr.kind evd cl with | App (f,args) -> @@ -1809,7 +1804,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) - | _ -> error "Match_subterm")) + | _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1825,7 +1820,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = let (evd,c as a) = a () in if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b in - let fail str _ = error str in + let fail str _ = user_err (Pp.str str) in let bind f g a = let a1 = try f a with ex @@ -1961,7 +1956,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 = | _, Meta p2 -> (* Find the predicate *) secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2) - | _ -> error "w_unify2" + | _ -> user_err Pp.(str "w_unify2") (* The unique unification algorithm works like this: If the pattern is flexible, and the goal has a lambda-abstraction at the head, then diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 148178f2fc..8d7e3521d6 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -45,7 +45,7 @@ val elim_no_delta_flags : unit -> unify_flags val is_keyed_unification : unit -> bool -(** The "unique" unification fonction *) +(** The "unique" unification function *) val w_unify : env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 74998349be..b08666483e 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -355,7 +355,7 @@ and nf_cofix env sigma cf = let cbv_vm env sigma c t = if Termops.occur_meta_or_existential sigma c then - CErrors.error "vm_compute does not support existential variables."; + CErrors.user_err Pp.(str "vm_compute does not support existential variables."); (** This evar-normalizes terms beforehand *) let c = EConstr.to_constr sigma c in let t = EConstr.to_constr sigma t in |