diff options
Diffstat (limited to 'pretyping')
57 files changed, 1843 insertions, 1250 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index ea33f1c0d6..8ac471404a 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -10,6 +10,7 @@ open Names open Globnames open Term +open Constr open Environ open Util open Libobject @@ -39,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) = let r' = fst (subst_global subst r) in if r==r' then orig else (r', names) -let section_segment_of_reference = function - | ConstRef con -> Lib.section_segment_of_constant con - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.AUContext.empty - let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> (try - let vars,_,_ = section_segment_of_reference c in + let vars = Lib.variable_section_segment_of_reference c in let c' = pop_global_reference c in let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in let names' = var_names @ names in @@ -103,7 +98,7 @@ let rename_type_of_constructor env cstruct = let rename_typing env c = let j = Typeops.infer env c in let j' = - match kind_of_term c with + match kind c with | Const (c,u) -> { j with uj_type = rename_type j.uj_type (ConstRef c) } | Ind (i,u) -> { j with uj_type = rename_type j.uj_type (IndRef i) } | Construct (k,u) -> { j with uj_type = rename_type j.uj_type (ConstructRef k) } diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 804e38216c..b499da3ab7 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -9,7 +9,7 @@ open Names open Globnames open Environ -open Term +open Constr val rename_arguments : bool -> global_reference -> Name.t list -> unit diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 63775d7373..a0434f9279 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -13,7 +13,7 @@ open CErrors open Util open Names open Nameops -open Term +open Constr open Termops open Environ open EConstr @@ -33,6 +33,7 @@ open Evarsolve open Evarconv open Evd open Context.Rel.Declaration +open Ltac_pretype module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -94,7 +95,7 @@ let msg_may_need_inversion () = (* Utils *) let make_anonymous_patvars n = - List.make n (CAst.make @@ PatVar Anonymous) + List.make n (DAst.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'] *) @@ -113,8 +114,8 @@ let rec relocate_index sigma n1 n2 k t = type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = @@ -177,7 +178,7 @@ and build_glob_pattern args = function | Top -> args | MakeConstructor (pci, rh) -> glob_pattern_of_partial_history - [CAst.make @@ PatCstr (pci, args, Anonymous)] rh + [DAst.make @@ PatCstr (pci, args, Anonymous)] rh let complete_history = glob_pattern_of_partial_history [] @@ -187,12 +188,12 @@ let pop_history_pattern = function | Continuation (0, l, Top) -> Result (List.rev l) | Continuation (0, l, MakeConstructor (pci, rh)) -> - feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh + feed_history (DAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh | _ -> anomaly (Pp.str "Constructor not yet filled with its arguments.") let pop_history h = - feed_history (CAst.make @@ PatVar Anonymous) h + feed_history (DAst.make @@ PatVar Anonymous) h (* Builds a continuation expecting [n] arguments and building [ci] applied to this [n] arguments *) @@ -245,7 +246,7 @@ let push_history_pattern n pci cont = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -273,8 +274,10 @@ type 'a pattern_matching_problem = let rec find_row_ind = function [] -> None - | { CAst.v = PatVar _ } :: l -> find_row_ind l - | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c) + | p :: l -> + match DAst.get p with + | PatVar _ -> find_row_ind l + | PatCstr(c,_,_) -> Some (p.CAst.loc,c) let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in @@ -348,7 +351,7 @@ let find_tomatch_tycon evdref env loc = function empty_tycon,None let make_return_predicate_ltac_lvar sigma na tm c lvar = - match na, tm.CAst.v with + match na, DAst.get tm with | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' -> if Id.Map.mem id lvar.ltac_genargs then let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in @@ -447,11 +450,6 @@ let current_pattern eqn = | pat::_ -> pat | [] -> anomaly (Pp.str "Empty list of patterns.") -let alias_of_pat = CAst.with_val (function - | PatVar name -> name - | PatCstr(_,_,name) -> name - ) - let remove_current_pattern eqn = match eqn.patterns with | pat::pats -> @@ -493,13 +491,14 @@ let rec adjust_local_defs ?loc = function | (pat :: pats, LocalAssum _ :: decls) -> pat :: adjust_local_defs ?loc (pats,decls) | (pats, LocalDef _ :: decls) -> - (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) + (DAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls) | [], [] -> [] | _ -> raise NotAdjustable -let check_and_adjust_constructor env ind cstrs = function - | { CAst.v = PatVar _ } as pat -> pat - | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat -> +let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with + | PatVar _ -> pat + | PatCstr (((_,i) as cstr),args,alias) -> + let loc = pat.CAst.loc in (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in if eq_ind ind' ind then @@ -510,7 +509,7 @@ let check_and_adjust_constructor env ind cstrs = function else try let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args) - in CAst.make ?loc @@ PatCstr (cstr, args', alias) + in DAst.make ?loc @@ PatCstr (cstr, args', alias) with NotAdjustable -> error_wrong_numarg_constructor ?loc env cstr nb_args_constr else @@ -522,9 +521,12 @@ let check_and_adjust_constructor env ind cstrs = function let check_all_variables env sigma typ mat = List.iter - (fun eqn -> match current_pattern eqn with - | { CAst.v = PatVar id } -> () - | { CAst.v = PatCstr (cstr_sp,_,_); loc } -> + (fun eqn -> + let pat = current_pattern eqn in + match DAst.get pat with + | PatVar id -> () + | PatCstr (cstr_sp,_,_) -> + let loc = pat.CAst.loc in error_bad_pattern ?loc env sigma cstr_sp typ) mat @@ -547,11 +549,11 @@ let extract_rhs pb = let occur_in_rhs na rhs = match na with | Anonymous -> false - | Name id -> Id.List.mem id rhs.rhs_vars + | Name id -> Id.Set.mem id rhs.rhs_vars -let is_dep_patt_in eqn = function - | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs - | { CAst.v = PatCstr _ } -> true +let is_dep_patt_in eqn pat = match DAst.get pat with + | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs + | PatCstr _ -> true let mk_dep_patt_row (pats,_,eqn) = List.map (is_dep_patt_in eqn) pats @@ -741,8 +743,8 @@ let get_names env sigma sign eqns = (* Otherwise, we take names from the parameters of the constructor but avoiding conflicts with user ids *) let allvars = - List.fold_left (fun l (_,_,eqn) -> List.union Id.equal l eqn.rhs.avoid_ids) - [] eqns in + List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids) + Id.Set.empty eqns in let names3,_ = List.fold_left2 (fun (l,avoid) d na -> @@ -751,7 +753,7 @@ let get_names env sigma sign eqns = (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(Name.get_id na)::avoid)) + (na::l,Id.Set.add (Name.get_id na) avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname @@ -771,7 +773,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 -> - (CAst.make @@ PatVar na, decl) :: aux (names,sign) + (DAst.make @@ PatVar na, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -987,14 +989,14 @@ let use_unit_judge evd = evd', j let add_assert_false_case pb tomatch = - let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in + let pats = List.map (fun _ -> DAst.make @@ PatVar Anonymous) tomatch in let aliasnames = List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch in [ { patterns = pats; rhs = { rhs_env = pb.env; - rhs_vars = []; - avoid_ids = []; + rhs_vars = Id.Set.empty; + avoid_ids = Id.Set.empty; it = None }; alias_stack = Anonymous::aliasnames; eqn_loc = None; @@ -1007,7 +1009,7 @@ let adjust_impossible_cases pb pred tomatch submat = this means that the Evd.define below may redefine an already defined evar. See e.g. first definition of test for bug #3388. *) let pred = EConstr.Unsafe.to_constr pred in - begin match kind_of_term pred with + begin match Constr.kind pred with | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin let evd, default = use_unit_judge !(pb.evdref) in @@ -1184,9 +1186,9 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = (************************************************************************) (* Sorting equations by constructor *) -let rec irrefutable env = function - | { CAst.v = PatVar name } -> true - | { CAst.v = PatCstr (cstr,args,_) } -> +let rec irrefutable env pat = match DAst.get pat with + | PatVar name -> true + | 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 @@ -1206,15 +1208,15 @@ let group_equations pb ind current cstrs mat = (fun eqn () -> let rest = remove_current_pattern eqn in let pat = current_pattern eqn in - match check_and_adjust_constructor pb.env ind cstrs pat with - | { CAst.v = PatVar name } -> + match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with + | 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 - | { CAst.v = PatCstr (((_,i)),args,name) ; loc } -> + | PatCstr (((_,i)),args,name) -> (* This is a regular clause *) only_default := Some false; brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in @@ -1269,7 +1271,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* 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 + let typs = List.map (map_type (nf_betaiota pb.env !(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 *) @@ -1419,7 +1421,7 @@ and match_current pb (initial,tomatch) = find_predicate pb.caseloc pb.env pb.evdref pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in - let pred = nf_betaiota !(pb.evdref) pred in + let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in @@ -1559,15 +1561,15 @@ substituer après par les initiaux *) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) + * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,lpat,rhs)) = - let initial_lpat,initial_rhs = lpat,rhs in - let initial_rhs = rhs in + let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = + let avoid = ids_of_named_context_val (named_context_val env) in + let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = { rhs_env = env; rhs_vars = free_glob_vars initial_rhs; - avoid_ids = ids@(ids_of_named_context (named_context env)); + avoid_ids = avoid; it = Some initial_rhs } in { patterns = initial_lpat; alias_stack = []; @@ -1656,7 +1658,7 @@ let rec list_assoc_in_triple x = function *) 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 t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*) let src = match EConstr.kind !evdref t with | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk) | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in @@ -1745,16 +1747,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 - CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in + DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add 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) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc + | Construct (cstr,u) -> DAst.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_right_map reveal_pattern l acc in - CAst.make (PatCstr (cstr,l,Anonymous)), acc + DAst.make (PatCstr (cstr,l,Anonymous)), acc | _ -> make_patvar t acc in let rec aux n env acc_sign tms acc = match tms with @@ -1775,7 +1777,7 @@ let build_inversion_problem loc env sigma tms t = let d = LocalAssum (alias_of_pat pat,typ) in let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in - let avoid0 = ids_of_context env in + let avoid0 = vars_of_env env in (* [patl] is a list of patterns revealing the substructure of constructors present in the constraints on the type of the multiple terms t1..tn that are matched in the original problem; @@ -1817,7 +1819,7 @@ let build_inversion_problem loc env sigma tms t = rhs = { rhs_env = pb_env; (* we assume all vars are used; in practice we discard dependent vars so that the field rhs_vars is normally not used *) - rhs_vars = List.map fst subst; + rhs_vars = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty subst; avoid_ids = avoid; it = Some (lift n t) } } in (* [catch_all] is a catch-all default clause of the auxiliary @@ -1830,12 +1832,12 @@ let build_inversion_problem loc env sigma tms t = (* No need for a catch all clause *) [] else - [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl; + [ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl; alias_stack = []; eqn_loc = None; used = ref false; rhs = { rhs_env = pb_env; - rhs_vars = []; + rhs_vars = Id.Set.empty; avoid_ids = avoid0; it = None } } ] in (* [pb] is the auxiliary pattern-matching serving as skeleton for the @@ -2079,7 +2081,7 @@ let prime avoid name = let make_prime avoid prevname = let previd, id = prime !avoid prevname in - avoid := id :: !avoid; + avoid := Id.Set.add id !avoid; previd, id let eq_id avoid id = @@ -2094,22 +2096,22 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole na = CAst.make @@ +let hole na = DAst.make @@ GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = let loc = pat.CAst.loc in - match pat.CAst.v with + match DAst.get pat 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 + Name id, Id.Set.add id avoid in - ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, + ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid) | PatCstr (((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in @@ -2140,7 +2142,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' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in + let pat' = DAst.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 @@ -2151,7 +2153,7 @@ let constr_of_pat env evdref arsign pat avoid = pat', sign, app, apptype, realargs, n, avoid | Name id -> let sign = LocalAssum (alias, lift m ty) :: sign in - let avoid = id :: avoid in + let avoid = Id.Set.add id avoid in let sign, i, avoid = try let env = push_rel_context sign env in @@ -2162,7 +2164,7 @@ let constr_of_pat env evdref arsign pat avoid = (lift 1 app) (* aliased term *) in let neq = eq_id avoid id in - LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, neq :: avoid + LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid with Reduction.NotConvertible -> sign, 1, avoid in (* Mark the equality as a hole *) @@ -2176,7 +2178,7 @@ let constr_of_pat env evdref arsign pat avoid = let eq_id avoid id = let hid = Id.of_string ("Heq_" ^ Id.to_string id) in let hid' = next_ident_away hid !avoid in - avoid := hid' :: !avoid; + avoid := Id.Set.add hid' !avoid; hid' let is_topvar sigma t = @@ -2196,18 +2198,18 @@ let vars_of_ctx sigma ctx = match decl with | LocalDef (na,t',t) when is_topvar sigma t' -> prev, - (CAst.make @@ GApp ( - (CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole na; CAst.make @@ GVar prev])) :: vars + (DAst.make @@ GApp ( + (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), + [hole na; DAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" - | Name n -> n, (CAst.make @@ GVar n) :: vars) + | Name n -> n, (DAst.make @@ GVar n) :: vars) ctx (Id.of_string "vars_of_ctx_error", []) in List.rev y let rec is_included x y = - match CAst.(x.v, y.v) with + match DAst.get x, DAst.get y with | PatVar _, _ -> true | _, PatVar _ -> true | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias') -> @@ -2272,7 +2274,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = (fun (idents, newpatterns, pats) pat arsign -> let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in (idents, pat' :: newpatterns, cpat :: pats)) - ([], [], []) eqn.patterns sign + (Id.Set.empty, [], []) eqn.patterns sign in let newpatterns = List.rev newpatterns and opats = List.rev pats in let rhs_rels, pats, signlen = @@ -2325,13 +2327,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 = CAst.make @@ GVar branch_name in + let bref = DAst.make @@ GVar branch_name in match vars_of_ctx !evdref rhs_rels with [] -> bref - | l -> CAst.make @@ GApp (bref, l) + | l -> DAst.make @@ GApp (bref, l) in let branch = match ineqs with - Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ]) + Some _ -> DAst.make @@ GApp (branch, [ hole Anonymous ]) | None -> branch in incr i; @@ -2373,8 +2375,8 @@ let abstract_tomatch env sigma tomatchs tycon = let name = next_ident_away (Id.of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, - name :: names, tycon) - ([], [], [], tycon) tomatchs + Id.Set.add name names, tycon) + ([], [], Id.Set.empty, tycon) tomatchs in List.rev prev, ctx, tycon let build_dependent_signature env evdref avoid tomatchs arsign = @@ -2496,7 +2498,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *) (* Build the dependent arity signature, the equalities which makes the first part of the predicate and their instantiations. *) - let avoid = [] in + let avoid = Id.Set.empty in build_dependent_signature env evdref avoid tomatchs arsign in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 428f64b999..43dbc31058 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -7,13 +7,14 @@ (************************************************************************) open Names -open Term +open Constr open Evd open Environ open EConstr open Inductiveops open Glob_term -open Evarutil +open Ltac_pretype +open Evardefine (** {5 Compilation of pattern-matching } *) @@ -49,16 +50,16 @@ val constr_of_pat : Evd.evar_map ref -> rel_context -> Glob_term.cases_pattern -> - Names.Id.t list -> + Names.Id.Set.t -> Glob_term.cases_pattern * (rel_context * constr * (types * constr list) * Glob_term.cases_pattern) * - Names.Id.t list + Names.Id.Set.t type 'a rhs = { rhs_env : env; - rhs_vars : Id.t list; - avoid_ids : Id.t list; + rhs_vars : Id.Set.t; + avoid_ids : Id.Set.t; it : 'a option} type 'a equation = @@ -101,7 +102,7 @@ and pattern_continuation = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -115,15 +116,15 @@ type 'a pattern_matching_problem = val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : ?loc:Loc.t -> - (Evarutil.type_constraint -> + (type_constraint -> Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> + Ltac_pretype.ltac_var_map -> (types * tomatch_type) list -> (rel_context * rel_context) list -> constr option -> - glob_constr option -> (Evd.evar_map * Names.name list * constr) list + glob_constr option -> (Evd.evar_map * Name.t list * constr) list -val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> - Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map +val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t -> + Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 19d61a64db..e42576d95b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -8,7 +8,7 @@ open Util open Names -open Term +open Constr open Vars open CClosure open Esubst @@ -45,7 +45,7 @@ type cbv_value = | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array - | CONSTR of constructor puniverses * cbv_value array + | CONSTR of constructor Univ.puniverses * cbv_value array (* type of terms with a hole. This hole can appear only under App or Case. * TOP means the term is considered without context @@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk = let cofixp_reducible flgs _ stk = if red_set flgs fCOFIX then match stk with - | (CASE _ | APP(_,CASE _)) -> true + | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true | _ -> false else false @@ -208,25 +208,32 @@ and reify_value = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (reify_stack (reify_value v) stk) | CBN(t,env) -> - t - (* map_constr_with_binders subs_lift (cbv_norm_term) env t *) - | LAM (n,ctxt,b,env) -> - List.fold_left (fun c (n,t) -> Term.mkLambda (n, t, c)) b ctxt + apply_env env t + | LAM (k,ctxt,b,env) -> + apply_env env @@ + List.fold_left (fun c (n,t) -> + mkLambda (n, t, c)) b ctxt | FIXP ((lij,(names,lty,bds)),env,args) -> - mkApp - (mkFix (lij, - (names, - lty, - bds)), - Array.map reify_value args) + let fix = mkFix (lij, (names, lty, bds)) in + mkApp (apply_env env fix, Array.map reify_value args) | COFIXP ((j,(names,lty,bds)),env,args) -> - mkApp - (mkCoFix (j, - (names,lty,bds)), - Array.map reify_value args) + let cofix = mkCoFix (j, (names,lty,bds)) in + mkApp (apply_env env cofix, Array.map reify_value args) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) +and apply_env env t = + match kind t with + | Rel i -> + begin match expand_rel i env with + | Inl (k, v) -> + reify_value (shift_value k v) + | Inr (k,_) -> + mkRel k + end + | _ -> + map_with_binders subs_lift apply_env env t + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -240,7 +247,7 @@ and reify_value = function (* reduction under binders *) let rec norm_head info env t stack = (* no reduction under binders *) - match kind_of_term t with + match kind t with (* stack grows (remove casts) *) | App (head,args) -> (* Applied terms are normalized immediately; they could be computed when getting out of the stack *) @@ -290,11 +297,14 @@ let rec norm_head info env t stack = | Evar ev -> (match evar_value info.infos.i_cache ev with Some c -> norm_head info env c stack - | None -> (VAL(0, t), stack)) + | None -> + let e, xs = ev in + let xs' = Array.map (apply_env env) xs in + (VAL(0, mkEvar (e,xs')), stack)) (* non-neutral cases *) | Lambda _ -> - let ctxt,b = decompose_lam t in + let ctxt,b = Term.decompose_lam t in (LAM(List.length ctxt, List.rev ctxt,b,env), stack) | Fix fix -> (FIXP(fix,env,[||]), stack) | CoFix cofix -> (COFIXP(cofix,env,[||]), stack) @@ -411,12 +421,12 @@ and cbv_norm_value info = function (* reduction under binders *) | STACK (n,v,stk) -> lift n (apply_stack info (cbv_norm_value info v) stk) | CBN(t,env) -> - map_constr_with_binders subs_lift (cbv_norm_term info) env t + Constr.map_with_binders subs_lift (cbv_norm_term info) env t | LAM (n,ctxt,b,env) -> let nctxt = List.map_i (fun i (x,ty) -> (x,cbv_norm_term info (subs_liftn i env) ty)) 0 ctxt in - compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) + Term.compose_lam (List.rev nctxt) (cbv_norm_term info (subs_liftn n env) b) | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 3ee7bebf08..1d4c88ea22 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -24,7 +24,7 @@ val cbv_norm : cbv_infos -> constr -> constr (*********************************************************************** i This is for cbv debug *) -open Term +open Constr type cbv_value = | VAL of int * constr @@ -33,7 +33,7 @@ type cbv_value = | LAM of int * (Name.t * constr) list * constr * cbv_value subs | FIXP of fixpoint * cbv_value subs * cbv_value array | COFIXP of cofixpoint * cbv_value subs * cbv_value array - | CONSTR of constructor puniverses * cbv_value array + | CONSTR of constructor Univ.puniverses * cbv_value array and cbv_stack = | TOP diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1cc072a2a2..6d5ee504e5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -9,14 +9,13 @@ open CErrors open Util open Pp -open Flags open Names +open Constr open Libnames open Globnames open Nametab open Environ open Libobject -open Term open Mod_subst (* usage qque peu general: utilise aussi dans record *) @@ -28,9 +27,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t type cl_info_typ = { cl_param : int @@ -44,7 +43,7 @@ type coe_info_typ = { coe_value : constr; coe_type : types; coe_local : bool; - coe_context : Univ.universe_context_set; + coe_context : Univ.ContextSet.t; coe_is_identity : bool; coe_is_projection : bool; coe_param : int } @@ -60,8 +59,8 @@ let coe_info_typ_equal c1 c2 = let cl_typ_ord t1 t2 = match t1, t2 with | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2 - | CL_CONST c1, CL_CONST c2 -> con_ord c1 c2 - | CL_PROJ c1, CL_PROJ c2 -> con_ord c1 c2 + | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2 + | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2 | CL_IND i1, CL_IND i2 -> ind_ord i1 i2 | _ -> Pervasives.compare t1 t2 (** OK *) @@ -323,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) -let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) +let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ _ _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path x = !path_printer x +let print_path env sigma x = !path_printer env sigma x -let message_ambig l = - (str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path ijp) l) +let message_ambig env sigma l = + str"Ambiguous paths:" ++ spc () ++ + prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -345,8 +344,8 @@ let different_class_params i = | CL_IND i -> Global.is_polymorphic (IndRef i) | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false - -let add_coercion_in_graph (ic,source,target) = + +let add_coercion_in_graph env sigma (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -387,8 +386,8 @@ 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 && not !quiet then - Feedback.msg_info (message_ambig !ambig_paths) + if is_ambig && not !Flags.quiet then + Feedback.msg_info (message_ambig env sigma !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -434,13 +433,13 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion (_, c) = +let cache_coercion env sigma (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in let it, _ = class_info c.coercion_target in - let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in - let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in + let value, ctx = Universes.fresh_global_instance env c.coercion_type in + let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in let typ = EConstr.Unsafe.to_constr typ in let xf = { coe_value = value; @@ -451,15 +450,15 @@ let cache_coercion (_, c) = coe_is_projection = c.coercion_is_proj; coe_param = c.coercion_params } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph (xf,is,it) + add_coercion_in_graph env sigma (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let open_coercion i o = if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion o + cache_coercion (Global.env ()) Evd.empty o let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -498,7 +497,9 @@ let inCoercion : coercion -> obj = declare_object {(default_object "COERCION") with open_function = open_coercion; load_function = load_coercion; - cache_function = cache_coercion; + cache_function = (fun objn -> + let env = Global.env () in cache_coercion env Evd.empty objn + ); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 8707078b58..47b41f17b2 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -17,9 +17,9 @@ type cl_typ = | CL_SORT | CL_FUN | CL_SECVAR of variable - | CL_CONST of constant + | CL_CONST of Constant.t | CL_IND of inductive - | CL_PROJ of constant + | CL_PROJ of Constant.t (** Equality over [cl_typ] *) val cl_typ_eq : cl_typ -> cl_typ -> bool @@ -96,7 +96,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 535a62046a..7cfd2e27d9 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -77,8 +77,8 @@ let apply_pattern_coercion ?loc pat p = List.fold_left (fun pat (co,n) -> 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)) + if i<n then (DAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in + DAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous)) pat p (* raise Not_found if no coercion found *) @@ -205,7 +205,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> let name' = - Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.ids_of_context env)) + Name (Namegen.next_ident_away Namegen.default_dependent_ident (Termops.vars_of_env env)) in let env' = push_rel (LocalAssum (name', a')) env in let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 886cfd880f..c3a221944d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -12,9 +12,7 @@ open CErrors open Util open Names open Globnames -open Nameops open Termops -open Reductionops open Term open EConstr open Vars @@ -22,6 +20,7 @@ open Pattern open Patternops open Misctypes open Context.Rel.Declaration +open Ltac_pretype (*i*) (* Given a term with second-order variables in it, @@ -54,7 +53,7 @@ exception PatternMatchingFailure let warn_meta_collision = CWarnings.create ~name:"meta-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variable " ++ pr_id name ++ + strbrk "Collision between bound variable " ++ Id.print name ++ strbrk " and a metavariable of same name.") @@ -90,7 +89,8 @@ let rec build_lambda sigma vars ctx m = match vars with let pre, suf = List.chop (pred n) ctx in let (na, t, suf) = match suf with | [] -> assert false - | (_, na, t) :: suf -> (na, t, suf) + | (_, id, t) :: suf -> + (Name id, t, suf) in (** Check that the abstraction is legal by generating a transitive closure of its dependencies. *) @@ -126,11 +126,11 @@ let rec build_lambda sigma vars ctx m = match vars with mkRel 1 :: List.mapi (fun i _ -> mkRel (i + keep + 2)) suf in - let map i (id, na, c) = + let map i (na, id, 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) + (na, id, substl subst c) in let pre = List.mapi map pre in let pre = List.filter_with clear pre in @@ -150,11 +150,10 @@ let rec build_lambda sigma vars ctx m = match vars with let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu -| (na1, na2, _) :: ctx -> +| (na, _, _) :: ctx -> if Int.Set.mem k frels then - begin match na1 with + begin match na with | Name id -> - let () = assert (match na2 with Anonymous -> false | Name _ -> true) in let () = if Id.Set.mem id accu then raise PatternMatchingFailure in extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx | Anonymous -> raise PatternMatchingFailure @@ -167,13 +166,21 @@ let extract_bound_vars frels ctx = let dummy_constr = EConstr.mkProp let make_renaming ids = function -| (Name id, Name _, _) -> +| (Name id, _, _) -> begin try EConstr.mkRel (List.index Id.equal id ids) with Not_found -> dummy_constr end | _ -> dummy_constr +let push_binder na1 na2 t ctx = + let id2 = match na2 with + | Name id2 -> id2 + | Anonymous -> + let avoid = Id.Set.of_list (List.map pi2 ctx) in + Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in + (na1, id2, t) :: ctx + let to_fix (idx, (nas, cs, ts)) = let inj = EConstr.of_constr in (idx, (nas, Array.map inj cs, Array.map inj ts)) @@ -199,20 +206,16 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = match ref, EConstr.kind sigma c with - | VarRef id, Var id' -> Names.id_eq id id' - | ConstRef c, Const (c',_) -> Names.eq_constant c c' + | VarRef id, Var id' -> Names.Id.equal id id' + | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -257,7 +260,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (PApp (h, a1), a2), _ -> sorec ctx env subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) -> (let diff = Array.length args2 - Array.length args1 in if diff >= 0 then let args21, args22 = Array.chop diff args2 in @@ -277,7 +280,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PApp (c1,arg1), App (c2,arg2) -> (match c1, EConstr.kind sigma c2 with - | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) + | PRef (ConstRef r), Proj (pr,c) when not (Constant.equal r (Projection.constant pr)) || Projection.unfolded pr -> raise PatternMatchingFailure | PProj (pr1,c1), Proj (pr,c) -> @@ -294,7 +297,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels with Invalid_argument _ -> raise PatternMatchingFailure) | PApp (PRef (ConstRef c1), _), Proj (pr, c2) - when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> + when Projection.unfolded pr || not (Constant.equal c1 (Projection.constant pr)) -> raise PatternMatchingFailure | PApp (c, args), Proj (pr, c2) -> @@ -306,19 +309,19 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) + sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> - sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) + sorec (push_binder na1 na2 c2 ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> - sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) + sorec (push_binder na1 na2 t2 ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> @@ -327,7 +330,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let n = Context.Rel.length ctx_b2 in let n' = Context.Rel.length ctx_b2' in if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then - let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in + let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = push_binder Anonymous na t l in let ctx_br = List.fold_left f ctx ctx_b2 in let ctx_br' = List.fold_left f ctx ctx_b2' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in @@ -363,19 +366,21 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | 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 + | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _ + | PProd _ | PLetIn _ | PSort _ | PIf _ | PCase _ + | PFix _ | PCoFix _| PEvar _), _ -> raise PatternMatchingFailure in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma pat c = + let names, subst = matches_core env sigma false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma (Id.Set.empty,pat) c) let special_meta = (-1) @@ -400,9 +405,9 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx = +let authorized_occ env sigma closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -411,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx = let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) -let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = +let sub_match ?(closed=true) env sigma pat c = let open EConstr in let rec aux env c mk_ctx next = - let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let here = authorized_occ env sigma closed pat c mk_ctx in let next () = match EConstr.kind sigma c with | Cast (c1,k,c2) -> let next_mk_ctx = function @@ -444,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let topdown = true in - if partial_app then - if topdown then - let lc1 = Array.sub lc 0 (Array.length lc - 1) in - let app = mkApp (c1,lc1) in - let mk_ctx = function - | [app';c] -> mk_ctx (mkApp (app',[|c|])) - | _ -> assert false in - try_aux [(env, app); (env, Array.last lc)] mk_ctx next - else - let rec aux2 app args next = - match args with - | [] -> - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next - | arg :: args -> - let app = mkApp (app,[|arg|]) in - let next () = aux2 app args next in - let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in - aux env app mk_ctx next in - aux2 c1 (Array.to_list lc) next - else - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [(env, app); (env, Array.last lc)] mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) @@ -479,29 +462,28 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = in let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next - | Fix (indx,(names,types,bodies)) -> + | Fix (indx,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next - | CoFix (i,(names,types,bodies)) -> + | CoFix (i,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - if partial_app then - try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () - else - try_aux [env, c'] next_mk_ctx next + begin try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> next () + end | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> next () in @@ -522,13 +504,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let result () = aux env c (fun x -> x) lempty in IStream.thunk result -let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c - -let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c - -let match_subterm_gen env sigma app pat c = - sub_match ~partial_app:app env sigma pat c +let match_subterm env sigma pat c = sub_match env sigma pat c let is_matching env sigma pat c = try let _ = matches env sigma pat c in true @@ -540,12 +516,5 @@ let is_matching_head env sigma pat c = let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in - let results = sub_match ~partial_app:true ~closed env sigma pat c in + let results = sub_match ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 1d7019d09f..e4d9ff9e1e 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -9,10 +9,11 @@ (** This module implements pattern-matching on terms *) open Names -open Term +open Constr open EConstr open Environ open Pattern +open Ltac_pretype type binding_bound_vars = Id.Set.t @@ -54,38 +55,19 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = { m_sub : bound_ident_map * patvar_map; m_ctx : EConstr.t } -(** [match_subterm n pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat]. *) -val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_appsubterm pat c] returns the substitution and the context +(** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], considering application contexts as well. *) -val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> - bool (** true = with app context *) -> +val match_subterm : env -> Evd.evar_map -> binding_bound_vars * constr_pattern -> constr -> matching_result IStream.t (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b9cb7ba1b1..18ecbf8ed3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -27,6 +27,11 @@ open Mod_subst open Misctypes open Decl_kinds open Context.Named.Declaration +open Ltac_pretype + +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) let print_universes = Flags.univ_print @@ -217,12 +222,12 @@ let lookup_name_as_displayed env sigma t s = | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None - in lookup (ids_of_named_context (named_context env)) 1 t + in lookup (Environ.ids_of_named_context_val (Environ.named_context_val env)) 1 t let lookup_index_as_renamed env sigma t n = let rec lookup n d c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal [] name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -232,7 +237,7 @@ let lookup_index_as_renamed env sigma t n = else lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal [] name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -247,6 +252,89 @@ let lookup_index_as_renamed env sigma t n = in lookup n 1 t (**********************************************************************) +(* Factorization of match patterns *) + +let print_factorize_match_patterns = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "factorization of \"match\" patterns in printing"; + optkey = ["Printing";"Factorizable";"Match";"Patterns"]; + optread = (fun () -> !print_factorize_match_patterns); + optwrite = (fun b -> print_factorize_match_patterns := b) } + +let print_allow_match_default_clause = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "possible use of \"match\" default pattern in printing"; + optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; + optread = (fun () -> !print_allow_match_default_clause); + optwrite = (fun b -> print_allow_match_default_clause := b) } + +let rec join_eqns (ids,rhs as x) patll = function + | (loc,(ids',patl',rhs') as eqn')::rest -> + if not !Flags.raw_print && !print_factorize_match_patterns && + List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' + then + join_eqns x (patl'::patll) rest + else + let eqn,rest = join_eqns x patll rest in + eqn, eqn'::rest + | [] -> + patll, [] + +let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll + +let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = [] + +let rec move_more_factorized_default_candidate_to_end eqn n = function + | eqn' :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in + if isbest then false, dft, eqns else false, dft, eqn' :: eqns + else + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in + isbest, dft, eqn' :: eqns + | [] -> true, Some eqn, [] + +let rec select_default_clause = function + | eqn :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in + if isbest then dft, eqns else dft, eqn :: eqns + else + let dft, eqns = select_default_clause eqns in dft, eqn :: eqns + | [] -> None, [] + +let factorize_eqns eqns = + let rec aux found = function + | (loc,(ids,patl,rhs))::rest -> + let patll,rest = join_eqns (ids,rhs) [patl] rest in + aux ((loc,(ids,patll,rhs))::found) rest + | [] -> + found in + let eqns = aux [] (List.rev eqns) in + let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in + if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + match select_default_clause eqns with + (* At least two clauses and the last one is disjunctive with no variables *) + | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)] + (* Only one clause which is disjunctive with no variables: we keep at least one constructor *) + (* so that it is not interpreted as a dummy "match" *) + | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)] + | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false + | None, eqns -> eqns + else + eqns + +(**********************************************************************) (* Fragile algorithm to reverse pattern-matching compilation *) let update_name sigma na ((_,(e,_)),c) = @@ -277,15 +365,14 @@ 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 = CAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in + let mkpat n rhs pl = DAst.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 (List.init (Array.length cl) - (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) + (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) sigma = match nal with - | [] -> [[],rhs] + | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with | Case (ci,p,c,cl) when @@ -295,19 +382,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e sigma ci cl in List.flatten - (List.map (fun (pat,rhs) -> + (List.map (fun (ids,pat,rhs) -> let lines = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) lines) + List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines) clauses) | _ -> - 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 + let na = update_name sigma na rhs in + let pat = DAst.make @@ PatVar na in + let mat = align_tree nal isgoal rhs sigma in + List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat -and contract_branch isgoal e sigma (cdn,can,mkpat,b) = - let nal,rhs = decomp_branch cdn [] isgoal e sigma b in +and contract_branch isgoal e sigma (cdn,mkpat,rhs) = + let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat + List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) @@ -323,7 +411,7 @@ let is_nondep_branch sigma c l = let extract_nondep_branches test c b l = let rec strip l r = - match r.CAst.v, l with + match DAst.get r, l with | r', [] -> r | GLambda (_,_,_,t), false::l -> strip l t | GLetIn (_,_,_,t), true::l -> strip l t @@ -333,7 +421,7 @@ let extract_nondep_branches test c b l = let it_destRLambda_or_LetIn_names l c = let rec aux l nal c = - match c.CAst.v, l with + match DAst.get c, 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 @@ -347,11 +435,11 @@ let it_destRLambda_or_LetIn_names l c = x in let x = next (free_glob_vars c) in - let a = CAst.make @@ GVar x in + let a = DAst.make @@ GVar x in aux l (Name x :: nal) - (match c with - | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a]) - | _ -> CAst.make @@ GApp (c,[a])) + (match DAst.get c with + | GApp (p,l) -> DAst.make ?loc:c.CAst.loc @@ GApp (p,l@[a]) + | _ -> DAst.make @@ GApp (c,[a])) in aux l [] c let detype_case computable detype detype_eqns testdep avoid data p c bl = @@ -363,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match Option.map detype p with - | None -> Anonymous, None, None - | Some p -> - let nl,typ = it_destRLambda_or_LetIn_names k p in - 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 (Loc.tag (indsp,nl)) in - n, aliastyp, Some typ + let p = detype p in + let nl,typ = it_destRLambda_or_LetIn_names k p in + let n,typ = match DAst.get typ with + | GLambda (x,_,t,c) -> x, c + | _ -> Anonymous, typ in + let aliastyp = + if List.for_all (Name.equal Anonymous) nl then None + 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 let tag = @@ -409,15 +495,17 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) +let detype_universe sigma u = + let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in + Univ.Universe.map fn u + let detype_sort sigma = function | Prop Null -> GProp | Prop Pos -> GSet | Type u -> GType (if !print_universes - 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)] + then detype_universe sigma u else []) type binder_kind = BProd | BLambda | BLetIn @@ -429,70 +517,76 @@ let detype_anonymous = ref (fun ?loc n -> anomaly ~label:"detype" (Pp.str "index let set_detype_anonymous f = detype_anonymous := f let detype_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 l = Termops.reference_of_level sigma l in + GType (UNamed 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 = CAst.make @@ +let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g = + match d with + | Now -> DAst.make (f d flags env avoid sigma t) + | Later -> DAst.delay (fun () -> f d flags env avoid sigma t) + +let rec detype d flags avoid env sigma t = + delay d detype_r flags avoid env sigma t + +and detype_r d flags avoid env sigma t = match EConstr.kind sigma (collapse_appl sigma t) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar id - | Anonymous -> (!detype_anonymous n).CAst.v + | Anonymous -> GVar (!detype_anonymous n) with Not_found -> let s = "_UNBOUND_REL_"^(string_of_int n) 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 (Id.of_string ("M" ^ string_of_int n), []) + if n = Constr_matching.special_meta then + (* Using a dash to be unparsable *) + GEvar (Id.of_string_soft "CONTEXT-HOLE", []) + else + GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (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).CAst.v + DAst.get (detype d flags avoid env sigma c1) | Cast (c1,k,c2) -> - let d1 = detype flags avoid env sigma c1 in - let d2 = detype flags avoid env sigma c2 in + let d1 = detype d flags avoid env sigma c1 in + let d2 = detype d flags avoid env sigma c2 in let cast = match k with | VMcast -> CastVM d2 | NATIVEcast -> CastNative d2 | _ -> CastConv d2 in 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 + | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma na None ty c + | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma na None ty c + | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> let mkapp f' args' = - match f'.CAst.v with + match DAst.get f' 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) + mkapp (detype d flags avoid env sigma f) + (Array.map_to_list (detype d flags avoid env sigma) args) | 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 = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - let args = List.make pars hole in - GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype flags avoid env sigma c])) + GProj (p, detype d 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 (CAst.make @@ GRef (ConstRef (Projection.constant p), None), - [detype flags avoid env sigma c]) + GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), + [detype d flags avoid env sigma c]) else if print_primproj_compatibility () && Projection.unfolded p then (** Print the compatibility match version *) @@ -509,12 +603,12 @@ let rec detype flags avoid env sigma t = CAst.make @@ 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').CAst.v + in DAst.get (detype d flags avoid env sigma c') else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in - (detype flags avoid env sigma c).CAst.v + DAst.get (detype d flags avoid env sigma c) with Retyping.RetypeError _ -> noparams () else noparams () @@ -538,59 +632,59 @@ let rec detype flags avoid env sigma t = CAst.make @@ let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in id,l with Not_found -> - Id.of_string ("X" ^ string_of_int (Evar.repr evk)), + Id.of_string ("X" ^ string_of_int (Evar.repr evk)), (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl) in GEvar (id, - List.map (on_snd (detype flags avoid env sigma)) l) + List.map (on_snd (detype d flags avoid env sigma)) l) | Ind (ind_sp,u) -> GRef (IndRef ind_sp, detype_instance sigma u) | Construct (cstr_sp,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) - (detype_eqns flags avoid env sigma ci comp) + detype_case comp (detype d flags avoid env sigma) + (detype_eqns d flags avoid env sigma ci comp) (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) - (Some p) c bl - | Fix (nvn,recdef) -> detype_fix flags avoid env sigma nvn recdef - | CoFix (n,recdef) -> detype_cofix flags avoid env sigma n recdef + p c bl + | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef + | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef -and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = +and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> let id = next_name_away na avoid in - (id::avoid, add_name (Name id) None ty env, id::l)) + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) (avoid, env, []) names tys in let n = Array.length tys in let v = Array.map3 - (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t)) + (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in 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) -and detype_cofix flags avoid env sigma n (names,tys,bodies) = +and detype_cofix d flags avoid env sigma n (names,tys,bodies) = let def_avoid, def_env, lfi = Array.fold_left2 (fun (avoid, env, l) na ty -> let id = next_name_away na avoid in - (id::avoid, add_name (Name id) None ty env, id::l)) + (Id.Set.add id avoid, add_name (Name id) None ty env, id::l)) (avoid, env, []) names tys in let ntys = Array.length tys in let v = Array.map2 - (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t)) + (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t)) bodies tys in 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) -and share_names flags n l avoid env sigma c t = +and share_names d flags n l avoid env sigma c t = match EConstr.kind sigma c, EConstr.kind sigma t with (* factorize even when not necessary to have better presentation *) | Lambda (na,t,c), Prod (na',t',c') -> @@ -598,59 +692,59 @@ and share_names flags n l avoid env sigma c t = Name _, _ -> na | _, Name _ -> na' | _ -> na in - let t' = detype flags avoid env sigma t in + let t' = detype d flags avoid env sigma t in let id = next_name_away na avoid in - let avoid = id::avoid and env = add_name (Name id) None t env in - share_names flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in + share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c' (* May occur for fix built interactively *) | LetIn (na,b,t',c), _ when n > 0 -> - let t'' = detype flags avoid env sigma t' in - let b' = detype flags avoid env sigma b in + let t'' = detype d flags avoid env sigma t' in + let b' = detype d flags avoid env sigma b in let id = next_name_away na avoid in - let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in - share_names flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) + let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in + share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t) (* Only if built with the f/n notation or w/o let-expansion in types *) | _, LetIn (_,b,_,t) when n > 0 -> - share_names flags n l avoid env sigma c (subst1 b t) + share_names d flags n l avoid env sigma c (subst1 b t) (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> - let t'' = detype flags avoid env sigma t' in + let t'' = detype d flags avoid env sigma t' in let id = next_name_away na' avoid in - let avoid = id::avoid and env = add_name (Name id) None t' env in + let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in let appc = mkApp (lift 1 c,[|mkRel 1|]) in - share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' + share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough"); - let c = detype flags avoid env sigma c in - let t = detype flags avoid env sigma t in + let c = detype d flags avoid env sigma c in + let t = detype d flags avoid env sigma t in (List.rev l,c,t) -and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = +and detype_eqns d 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)) -> Loc.tag ([],[pat],detype flags avoid env sigma c)) + List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list - (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl) + (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl) -and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch = +and detype_eqn d (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 - CAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids + DAst.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 - CAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na + DAst.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 | _, [] -> Loc.tag @@ (Id.Set.elements ids, - [CAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], - detype flags avoid env sigma b) + [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)], + detype d 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 buildrec new_ids (pat::patlist) new_avoid new_env l b @@ -663,7 +757,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 = CAst.make @@ PatVar Anonymous in + let pat = DAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> @@ -678,23 +772,23 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = +and detype_binder d (lax,isgoal as flags) bk avoid env sigma na body ty c = let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in let na',avoid' = match bk with | BLetIn -> compute_displayed_let_name_in sigma flag avoid na 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 + let r = detype d flags avoid' (add_name na' body ty env) sigma c in match bk with - | BProd -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r) - | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r) + | BProd -> GProd (na',Explicit,detype d (lax,false) avoid env sigma ty, r) + | BLambda -> GLambda (na',Explicit,detype d (lax,false) avoid env sigma ty, r) | BLetIn -> - let c = detype (lax,false) avoid env sigma (Option.get body) in + let c = detype d (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 && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in + let t = if s != InProp && not !Flags.raw_print then None else Some (detype d (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) -let detype_rel_context ?(lax=false) where avoid env sigma sign = +let detype_rel_context d ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] @@ -716,15 +810,18 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign = | LocalAssum _ -> None | LocalDef (_,b,_) -> Some b in - let b' = Option.map (detype (lax,false) avoid env sigma) b in - let t' = detype (lax,false) avoid env sigma t in + let b' = Option.map (detype d (lax,false) avoid env sigma) b in + let t' = detype d (lax,false) avoid env sigma t in (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest in aux avoid env (List.rev sign) let detype_names isgoal avoid nenv env sigma t = - detype (false,isgoal) avoid (nenv,env) sigma t -let detype ?(lax=false) isgoal avoid env sigma t = - detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t + detype Now (false,isgoal) avoid (nenv,env) sigma t +let detype d ?(lax=false) isgoal avoid env sigma t = + detype d (lax,isgoal) avoid (names_of_rel_context env, env) sigma t + +let detype_rel_context d ?lax where avoid env sigma sign = + detype_rel_context d ?lax where avoid env sigma sign let detype_closed_glob ?lax isgoal avoid env sigma t = let open Context.Rel.Declaration in @@ -736,7 +833,7 @@ 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 cg : Glob_term.glob_constr = CAst.map (function + let rec detype_closed_glob cl cg : Glob_term.glob_constr = DAst.map (function | GVar id -> (* if [id] is bound to a name. *) begin try @@ -750,11 +847,11 @@ 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).CAst.v + DAst.get (detype Now ?lax isgoal avoid env sigma c) (* 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).CAst.v + DAst.get (detype_closed_glob closure term) (* Otherwise [id] stands for itself *) with Not_found -> GVar id @@ -781,7 +878,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = in GCases(sty,po,tml,eqns) | c -> - (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v + DAst.get (Glob_ops.map_glob_constr (detype_closed_glob cl) cg) ) cg in detype_closed_glob t.closure t.term @@ -789,7 +886,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (**********************************************************************) (* Module substitution: relies on detyping *) -let rec subst_cases_pattern subst = CAst.map (function +let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn @@ -800,11 +897,11 @@ let rec subst_cases_pattern subst = CAst.map (function let (f_subst_genarg, subst_genarg_hook) = Hook.make () -let rec subst_glob_constr subst = CAst.map (function +let rec subst_glob_constr subst = DAst.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)).CAst.v + DAst.get (detype Now false Id.Set.empty (Global.env()) Evd.empty (EConstr.of_constr t)) | GSort _ | GVar _ @@ -898,6 +995,13 @@ let rec subst_glob_constr subst = CAst.map (function 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 (r1',k') + + | GProj (p,c) as raw -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_glob_constr subst c in + if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c') ) (* Utilities to transform kernel cases to simple pattern-matching problem *) @@ -905,8 +1009,8 @@ let rec subst_glob_constr subst = CAst.map (function 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 = CAst.make @@ PatVar na in - let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in + let mkPatVar na = DAst.make @@ PatVar na in + let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in let ids = List.map_filter Nameops.Name.to_option nal in Loc.tag @@ (ids,[p],c)) brs diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 59f3f967d3..f150cb1956 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Glob_term @@ -15,6 +14,11 @@ open Termops open Mod_subst open Misctypes open Evd +open Ltac_pretype + +type _ delay = +| Now : 'a delay +| Later : [ `thunk ] delay (** Should we keep details of universes during detyping ? *) val print_universes : bool ref @@ -22,32 +26,42 @@ val print_universes : bool ref (** If true, prints full local context of evars *) val print_evar_arguments : bool ref +(** If true, contract branches with same r.h.s. and same matching + variables in a disjunctive pattern *) +val print_factorize_match_patterns : bool ref + +(** If true and the last non unique clause of a "match" is a + variable-free disjunctive pattern, turn it into a catch-call case *) +val print_allow_match_default_clause : bool ref + val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern val subst_glob_constr : substitution -> glob_constr -> glob_constr +val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g + (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in [avoid] [isgoal] tells if naming must avoid global-level synonyms as intro does [ctx] gives the names of the free variables *) -val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr +val detype_names : bool -> Id.Set.t -> names_context -> env -> evar_map -> constr -> glob_constr -val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr +val detype : 'a delay -> ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> constr -> 'a glob_constr_g -val detype_sort : evar_map -> sorts -> glob_sort +val detype_sort : evar_map -> Sorts.t -> glob_sort -val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> - evar_map -> rel_context -> glob_decl list +val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) -> + evar_map -> rel_context -> 'a glob_decl_g list -val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr +val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr (** look for the index of a named var or a nondep var as it is renamed *) 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 (* XXX: This is a hack and should go away *) -val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit +val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit val force_wildcard : unit -> bool val synthetize_type : unit -> bool diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cb76df4e8a..dc3acbc3e2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Termops open Environ open EConstr @@ -48,8 +48,8 @@ let _ = Goptions.declare_bool_option { "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 (_, u) = Constr.destConst c in + Some (c, Constr.mkConstU (Coqlib.type_of_id, u), ctx) let coq_unit_judge = let open Environ in @@ -175,7 +175,13 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Sort s -> let s = ESorts.kind sigma s in lookup_canonical_conversion - (proji, Sort_cs (family_of_sort s)),[] + (proji, Sort_cs (Sorts.family s)),[] + | Proj (p, c) -> + let c2 = Globnames.ConstRef (Projection.constant p) in + let c = Retyping.expand_projection env sigma p c [] in + let _, args = destApp sigma c in + let sk2 = Stack.append_app args sk2 in + lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> let (c2, _) = Termops.global_of_constr sigma t2 in lookup_canonical_conversion (proji, Const_cs c2),sk2 @@ -212,6 +218,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let t' = EConstr.of_constr t' in let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in + let params = List.map (fun c -> subst_univs_level_constr subst c) params in + let us = List.map (fun c -> subst_univs_level_constr subst c) us in let h, _ = decompose_app_vect sigma t' in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, @@ -268,11 +276,6 @@ let rec ise_app_stack2 env f evd sk1 sk2 = end | _, _ -> (sk1,sk2), Success evd -let push_rec_types pfix env = - let (i, c, t) = pfix in - let inj c = EConstr.Unsafe.to_constr c in - push_rec_types (i, Array.map inj c, Array.map inj t) env - (* This function tries to unify 2 stacks element by element. It works from the end to the beginning. If it unifies a non empty suffix of stacks but not the entire stacks, the first part of the answer is @@ -291,7 +294,7 @@ let ise_stack2 no_app env evd f sk1 sk2 = | UnifFailure _ as x -> fail x) | UnifFailure _ as x -> fail x) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 true i q1 q2 else fail (UnifFailure (i, NotSameHead)) | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, @@ -304,8 +307,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i' -> ise_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin match ise_app_stack2 env f i sk1 sk2 with @@ -335,11 +336,9 @@ let exact_ise_stack2 env evd f sk1 sk2 = (fun i -> ise_stack2 i a1 a2)] else UnifFailure (i,NotSameHead) | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> - if eq_constant (Projection.constant p1) (Projection.constant p2) + if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> begin match ise_app_stack2 env f i sk1 sk2 with |_,(UnifFailure _ as x) -> x @@ -354,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - begin - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in - Evd.add_constraints evd comp_cst - end + Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u') let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in @@ -451,7 +438,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 @@ -765,7 +752,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f1; f2] (* Catch the p.c ~= p c' cases *) - | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> + | Proj (p,c), Const (p',u) when Constant.equal (Projection.constant p) p' -> let res = try Some (destApp evd (Retyping.expand_projection env evd p c [])) with Retyping.RetypeError _ -> None @@ -776,7 +763,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (appr2,csts2) | None -> UnifFailure (evd,NotSameHead)) - | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> + | Const (p,u), Proj (p',c') when Constant.equal p (Projection.constant p') -> let res = try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) with Retyping.RetypeError _ -> None @@ -1040,7 +1027,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let mib = lookup_mind (fst ind) env in match mib.Declarations.mind_record with - | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in @@ -1061,8 +1048,8 @@ let evar_conv_x ts = evar_conv_x (ts, true) (* Profiling *) let evar_conv_x = if Flags.profile then - let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in - Profile.profile6 evar_conv_xkey evar_conv_x + let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in + CProfile.profile6 evar_conv_xkey evar_conv_x else evar_conv_x let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index c30d1d26bf..d793b06d3d 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -47,7 +47,7 @@ val check_problems_are_solved : env -> evar_map -> unit val check_conv_record : env -> evar_map -> state -> state -> - Univ.universe_context_set * (constr * constr) + Univ.ContextSet.t * (constr * constr) * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * (constr Stack.t * constr Stack.t) * constr * diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 7f5a780f9c..fd83795f55 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open Pp open Names -open Term +open Constr open Termops open EConstr open Vars @@ -27,8 +28,8 @@ let env_nf_evar sigma env = let env_nf_betaiotaevar sigma env = process_rel_context - (fun d e -> - push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env + (fun d env -> + push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota env sigma c) d) env) env (****************************************) (* Operations on value/type constraints *) @@ -72,7 +73,7 @@ let define_pure_evar_as_product evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in + let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in let s = destSort evd concl in let evd1,(dom,u1) = @@ -82,7 +83,7 @@ let define_pure_evar_as_product evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let src = evar_source evk evd1 in let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort (ESorts.kind evd1 s) then + if Sorts.is_prop (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else @@ -127,7 +128,7 @@ let define_pure_evar_as_lambda env evd evk = | Prod (na,dom,rng) -> (evd,(na,dom,rng)) | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ | _ -> error_not_product env evd typ in - let avoid = ids_of_named_context (evar_context evi) in + let avoid = Environ.ids_of_named_context_val evi.evar_hyps in let id = next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in let newenv = push_named (LocalAssum (id, dom)) evenv in diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index 5477c5c99d..869e3adbf9 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Evd open Environ @@ -39,7 +38,7 @@ val lift_tycon : int -> type_constraint -> type_constraint val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types -val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * Sorts.t (** {6 debug pretty-printer:} *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ef0fb8ea6e..e6d1e59b3a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Sorts open Util open CErrors open Names -open Term +open Constr open Environ open Termops open Evd @@ -679,6 +680,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let filter1 = evar_filter evi1 in let src = subterm_source evk1 evi1.evar_source in let ids1 = List.map get_id (named_context_of_val sign1) in + let avoid = Environ.ids_of_named_context_val sign1 in let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in let open Context.Rel.Declaration in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = @@ -700,9 +702,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = (push_named_context_val d' sign, Filter.extend 1 filter, (mkRel 1)::(List.map (lift 1) inst_in_env), (mkRel 1)::(List.map (lift 1) inst_in_sign), - push_rel d env,evd,id::avoid)) + push_rel d env,evd,Id.Set.add id avoid)) rel_sign - (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1) + (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in @@ -841,6 +843,25 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false +let is_preferred_projection_over sign (id,p) (id',p') = + (* We give priority to projection of variables over instantiation of + an evar considering that the latter is a stronger decision which + may even procude an incorrect (ill-typed) solution *) + match p, p' with + | ProjectEvar _, ProjectVar -> false + | ProjectVar, ProjectEvar _ -> true + | _, _ -> + List.index Id.equal id sign < List.index Id.equal id' sign + +let choose_projection evi sols = + let sign = List.map get_id (evar_filtered_context evi) in + match sols with + | y::l -> + List.fold_right (fun (id,p as x) (id',_ as y) -> + if is_preferred_projection_over sign x y then x else y) + l y + | _ -> assert false + (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -1001,7 +1022,7 @@ let closure_of_filter evd evk = function | Some filter -> let evi = Evd.find_undefined evd evk in let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in - let test b decl = b || Idset.mem (get_id decl) vars || + let test b decl = b || Id.Set.mem (get_id decl) vars || match decl with | LocalAssum _ -> false @@ -1371,7 +1392,7 @@ let occur_evar_upto_types sigma n c = let c = EConstr.Unsafe.to_constr c in let seen = ref Evar.Set.empty in (** FIXME: Is that supposed to be evar-insensitive? *) - let rec occur_rec c = match kind_of_term c with + let rec occur_rec c = match Constr.kind c with | Evar (sp,_) when Evar.equal sp n -> raise Occur | Evar (sp,args as e) -> if Evar.Set.mem sp !seen then @@ -1428,8 +1449,12 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | (id,p)::_::_ -> - if choose then (mkVar id, p) else raise (NotUniqueInType sols) + | _ -> + if choose then + let (id,p) = choose_projection evi sols in + (mkVar id, p) + else + raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in @@ -1550,19 +1575,19 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in - let names = ref Idset.empty in + let names = ref Id.Set.empty in let rec is_id_subst ctxt s = match ctxt, s with | (decl :: ctxt'), (c :: s') -> let id = get_id decl in - names := Idset.add id !names; + names := Id.Set.add id !names; isVarId evd id c && is_id_subst ctxt' s' | [], [] -> true | _ -> false in is_id_subst filter_ctxt (Array.to_list argsv) && closed0 evd rhs && - Idset.subset (collect_vars evd rhs) !names + Id.Set.subset (collect_vars evd rhs) !names in let body = if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 811b4dc18f..703c4616c7 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Evd open Environ @@ -49,7 +48,7 @@ val refresh_universes : env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> - bool option -> existential_key -> constr array -> constr array -> evar_map + bool option -> Evar.t -> constr array -> constr array -> evar_map val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> @@ -78,10 +77,10 @@ exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : - evar_map -> existential_key -> constr -> conv_fun -> evar_map + evar_map -> Evar.t -> constr -> conv_fun -> evar_map val remove_instance_local_defs : - evar_map -> existential_key -> 'a array -> 'a list + evar_map -> Evar.t -> 'a array -> 'a list val get_type_of_refresh : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 9e7652da64..fd6bfe0a2c 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -12,7 +12,6 @@ open CErrors open Names open Locus open EConstr -open Nameops open Termops open Pretype_errors @@ -30,7 +29,7 @@ let explain_invalid_occurrence l = ++ prlist_with_sep spc int l ++ str "." let explain_incorrect_in_value_occurrence id = - pr_id id ++ str " has no value." + Id.print id ++ str " has no value." let explain_occurrence_error = function | InvalidOccurrence l -> explain_invalid_occurrence l diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml new file mode 100644 index 0000000000..768ef3cfd9 --- /dev/null +++ b/pretyping/geninterp.ml @@ -0,0 +1,100 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Genarg + +module TacStore = Store.Make () + +(** Dynamic toplevel values *) + +module ValT = Dyn.Make () + +module Val = +struct + + type 'a typ = 'a ValT.tag + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + let eq = ValT.eq + let repr = ValT.repr + let create = ValT.create + + let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t) + + let typ_list = ValT.create "list" + let typ_opt = ValT.create "option" + let typ_pair = ValT.create "pair" + + let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with + | Base t -> Dyn (t, x) + | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x) + | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x) + | Pair (tag1, tag2) -> + Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x))) + +end + +module ValTMap = ValT.Map + +module ValReprObj = +struct + type ('raw, 'glb, 'top) obj = 'top Val.tag + let name = "valrepr" + let default _ = None +end + +module ValRepr = Register(ValReprObj) + +let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function +| ListArg t -> Val.List (val_tag t) +| OptArg t -> Val.Opt (val_tag t) +| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) +| ExtraArg s -> ValRepr.obj (ExtraArg s) + +let val_tag = function Topwit t -> val_tag t + +let register_val0 wit tag = + let tag = match tag with + | None -> + let name = match wit with + | ExtraArg s -> ArgT.repr s + | _ -> assert false + in + Val.Base (Val.create name) + | Some tag -> tag + in + ValRepr.register0 wit tag + +(** Interpretation functions *) + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +module InterpObj = +struct + type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun + let name = "interp" + let default _ = None +end + +module Interp = Register(InterpObj) + +let interp = Interp.obj + +let register_interp0 = Interp.register0 diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli new file mode 100644 index 0000000000..ae0b26e594 --- /dev/null +++ b/pretyping/geninterp.mli @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Interpretation functions for generic arguments and interpreted Ltac + values. *) + +open Names +open Genarg + +(** {6 Dynamic toplevel values} *) + +module Val : +sig + type 'a typ + + val create : string -> 'a typ + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option + val repr : 'a typ -> string + val pr : 'a typ -> Pp.t + + val typ_list : t list typ + val typ_opt : t option typ + val typ_pair : (t * t) typ + + val inject : 'a tag -> 'a -> t + +end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + +(** Dynamic types for toplevel values. While the generic types permit to relate + objects at various levels of interpretation, toplevel values are wearing + their own type regardless of where they came from. This allows to use the + same runtime representation for several generic types. *) + +val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag +(** Retrieve the dynamic type associated to a toplevel genarg. *) + +val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit +(** Register the representation of a generic argument. If no tag is given as + argument, a new fresh tag with the same name as the argument is associated + to the generic type. *) + +(** {6 Interpretation functions} *) + +module TacStore : Store.S + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index b94228e75e..25817478e7 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -13,18 +13,29 @@ open Globnames open Misctypes open Glob_term open Evar_kinds +open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) let cases_pattern_loc c = c.CAst.loc +let alias_of_pat pat = DAst.with_val (function + | PatVar name -> name + | PatCstr(_,_,name) -> name + ) pat + +let set_pat_alias id = DAst.map (function + | PatVar Anonymous -> PatVar (Name id) + | PatCstr (cstr,patl,Anonymous) -> PatCstr (cstr,patl,Name id) + | pat -> assert false) + let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml) -let mkGApp ?loc p t = CAst.make ?loc @@ - match p.CAst.v with +let mkGApp ?loc p t = DAst.make ?loc @@ + match DAst.get p with | GApp (f,l) -> GApp (f,l@[t]) | _ -> GApp (p,[t]) @@ -46,7 +57,7 @@ let case_style_eq s1 s2 = match s1, s2 with | RegularStyle, RegularStyle -> true | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false -let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 with +let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get 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 && @@ -98,7 +109,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with let instance_eq f (x1,c1) (x2,c2) = Id.equal x1 x2 && f c1 c2 -let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with +let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2 | GVar id1, GVar id2 -> Id.equal id1 id2 | GEvar (id1, arg1), GEvar (id2, arg2) -> @@ -132,12 +143,14 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 + | GProj (p1, t1), GProj (p2, t2) -> + Projection.equal p1 p2 && f t1 t2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | - GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c -let map_glob_constr_left_to_right f = CAst.map (function +let map_glob_constr_left_to_right f = DAst.map (function | GApp (g,args) -> let comp1 = f g in let comp2 = Util.List.map_left f args in @@ -179,6 +192,8 @@ let map_glob_constr_left_to_right f = CAst.map (function let comp1 = f c in let comp2 = Miscops.map_cast_type f k in GCast (comp1,comp2) + | GProj (p,c) -> + GProj (p, f c) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x ) @@ -186,7 +201,7 @@ 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 = CAst.with_val (function +let fold_glob_constr f acc = DAst.with_val (function | GVar _ -> acc | GApp (c,args) -> List.fold_left f (f acc c) args | GLambda (_,_,b,c) | GProd (_,_,b,c) -> @@ -211,13 +226,15 @@ let fold_glob_constr f acc = CAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c + | GProj(_,c) -> + f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc ) let fold_return_type_with_binders f g v acc (na,tyopt) = Option.fold_left (f (Name.fold_right g na v)) acc tyopt -let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function +let fold_glob_constr_with_binders g f v acc = DAst.(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) -> @@ -234,7 +251,8 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function 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 + f (List.fold_right (Name.fold_right g) nal 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) -> @@ -251,15 +269,16 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c + | GProj(_,c) -> + 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 open CAst in - let rec occur barred acc = function - | { loc ; v = GVar id' } -> Id.equal id id' - | c -> + let rec occur barred acc c = match DAst.get c with + | GVar id' -> Id.equal id id' + | _ -> (* [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 @@ -268,29 +287,28 @@ let occur_glob_constr id = occur false false let free_glob_vars = - 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 + let rec vars bound vs c = match DAst.get c with + | GVar id' -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs + | _ -> 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 + vs let glob_visible_short_qualid c = - let rec aux acc = function - | { CAst.v = GRef (c,_) } -> + let rec aux acc c = match DAst.get c with + | 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 - | c -> + if DirPath.is_empty dir then Id.Set.add id acc else acc + | _ -> fold_glob_constr aux acc c - in aux [] c + in aux Id.Set.empty c let warn_variable_collision = let open Pp in CWarnings.create ~name:"variable-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variables of name " ++ pr_id name) + strbrk "Collision between bound variables of name " ++ Id.print name) let add_and_check_ident id set = if Id.Set.mem id set then warn_variable_collision id; @@ -326,7 +344,7 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple = if r == inp then x else c,(f na, r) -let rec map_case_pattern_binders f = CAst.map (function +let rec map_case_pattern_binders f = DAst.map (function | PatVar na as x -> let r = f na in if r == na then x @@ -396,7 +414,9 @@ 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 c = CAst.map_with_loc (fun ?loc -> function +let force c = DAst.make ?loc:c.CAst.loc (DAst.get c) + +let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function | GVar id as r -> let id' = rename_var l id in if id == id' then r else GVar id' @@ -436,13 +456,17 @@ let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function 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) - | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v + | _ -> DAst.get (map_glob_constr (rename_glob_vars l) c) ) c (**********************************************************************) (* Conversion from glob_constr to cases pattern, if possible *) -let rec cases_pattern_of_glob_constr na = CAst.map (function +let is_gvar id c = match DAst.get c with +| GVar id' -> Id.equal id id' +| _ -> false + +let rec cases_pattern_of_glob_constr na = DAst.map (function | GVar id -> begin match na with | Name _ -> @@ -452,8 +476,15 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function end | GHole (_,_,_) -> PatVar na | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na) - | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) -> + | GApp (c, l) -> + begin match DAst.get c with + | GRef (ConstructRef cstr,_) -> PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | _ -> raise Not_found + end + | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous -> + (* A canonical encoding of aliases *) + DAst.get (cases_pattern_of_glob_constr na' b) | _ -> raise Not_found ) @@ -469,7 +500,7 @@ let drop_local_defs typi args = | [], [] -> [] | Rel.Declaration.LocalDef _ :: decls, pat :: args -> begin - match pat.CAst.v with + match DAst.get pat with | PatVar Anonymous -> aux decls args | _ -> raise Not_found (* The pattern is used, one cannot drop it *) end @@ -487,24 +518,36 @@ let add_patterns_for_params_remove_local_defs (ind,j) l = let typi = mip.mind_nf_lc.(j-1) in let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in drop_local_defs typi l in - Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l + Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l + +let add_alias ?loc na c = + match na with + | Anonymous -> c + | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id)) (* Turn a closed cases pattern into a glob_constr *) -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 +let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function + | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None)) + | PatCstr (cstr,l,na) -> + let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in let l = add_patterns_for_params_remove_local_defs cstr l in - GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l) + add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l)) + | PatVar (Name id) when not isclosed -> + GVar id + | PatVar Anonymous when not isclosed -> + GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None) | _ -> raise Not_found ) x -let glob_constr_of_closed_cases_pattern = function - | { CAst.loc ; v = PatCstr (cstr,l,na) } -> - na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) +let glob_constr_of_closed_cases_pattern p = match DAst.get p with + | PatCstr (cstr,l,na) -> + let loc = p.CAst.loc in + na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous)) | _ -> raise Not_found +let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p + (**********************************************************************) (* Interpreting ltac variables *) @@ -517,7 +560,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function try Name (Id.Map.find id ltac_idents) with Not_found -> if Id.Map.mem id ltac_genargs then - user_err (str"Ltac variable"++spc()++ pr_id id ++ + user_err (str"Ltac variable"++spc()++ Id.print id ++ spc()++str"is not bound to an identifier."++spc()++ str"It cannot be used in a binder.") else n diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index bd9e111f5c..0d9fb1f453 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -11,21 +11,25 @@ open Glob_term (** Equalities *) -val cases_pattern_eq : cases_pattern -> cases_pattern -> bool +val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool + +val alias_of_pat : 'a cases_pattern_g -> Name.t + +val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g val cast_type_eq : ('a -> 'a -> bool) -> 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool -val glob_constr_eq : glob_constr -> glob_constr -> bool +val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> Loc.t option +val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option -val cases_predicate_names : tomatch_tuples -> Name.t list +val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list (** Apply one argument to a glob_constr *) -val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr +val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr @@ -42,12 +46,12 @@ val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) -> 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 occur_glob_constr : Id.t -> 'a glob_constr_g -> bool +val free_glob_vars : 'a glob_constr_g -> Id.Set.t val bound_glob_vars : glob_constr -> Id.Set.t (* Obsolete *) -val loc_of_glob_constr : glob_constr -> Loc.t option -val glob_visible_short_qualid : glob_constr -> Id.t list +val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option +val glob_visible_short_qualid : 'a glob_constr_g -> Id.Set.t (* Renaming free variables using a renaming map; fails with [UnsoundRenaming] if applying the renaming would introduce @@ -57,14 +61,14 @@ val glob_visible_short_qualid : glob_constr -> Id.t list exception UnsoundRenaming val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t -val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr +val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. It is used to interpret Ltac-bound names both in pretyping and printing of terms. *) -val map_pattern_binders : (name -> name) -> +val map_pattern_binders : (Name.t -> Name.t) -> tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses) (** [map_pattern f m c] applies [f] to the return predicate and the @@ -78,11 +82,15 @@ val map_pattern : (glob_constr -> glob_constr) -> Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern +val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g + +val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g -val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr +(** A canonical encoding of cases pattern into constr such that + composed with [cases_pattern_of_glob_constr Anonymous] gives identity *) +val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g -val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list +val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name -val empty_lvar : Glob_term.ltac_var_map +val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t +val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index aced42f839..b7b5b1662a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -18,6 +18,7 @@ open Libnames open Globnames open Nameops open Term +open Constr open Vars open Namegen open Declarations @@ -33,7 +34,7 @@ type dep_flag = bool (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive @@ -168,7 +169,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in - match kind_of_term p' with + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in make_prod env (n,t,prec (push_rel d env) (i+1) (d::sign) c) @@ -186,13 +187,13 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | _ -> let t' = whd_all env sigma (EConstr.of_constr p) in let t' = EConstr.Unsafe.to_constr t' in - if Term.eq_constr p' t' then assert false + if Constr.equal p' t' then assert false else prec env i sign t' in prec env 0 [] in let rec process_constr env i c recargs nhyps li = - if nhyps > 0 then match kind_of_term c with + if nhyps > 0 then match kind c with | Prod (n,t,c_0) -> let (optionpos,rest) = match recargs with @@ -247,7 +248,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let p',largs = whd_allnolet_stack env sigma (EConstr.of_constr p) in let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in - match kind_of_term p' with + match kind p' with | Prod (n,t,c) -> let d = LocalAssum (n,t) in mkLambda_name env (n,t,prec (push_rel d env) (i+1) (d::hyps) c) @@ -261,7 +262,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = | _ -> let t' = whd_all env sigma (EConstr.of_constr p) in let t' = EConstr.Unsafe.to_constr t' in - if Term.eq_constr t' p' then assert false + if Constr.equal t' p' then assert false else prec env i hyps t' in prec env 0 [] @@ -505,7 +506,7 @@ let build_case_analysis_scheme_default env sigma pity kind = [rec] by [s] *) let change_sort_arity sort = - let rec drec a = match kind_of_term a with + let rec drec a = match kind a with | Cast (c,_,_) -> drec c | Prod (n,t,c) -> let s, c' = drec c in s, mkProd (n, t, c') | LetIn (n,b,t,c) -> let s, c' = drec c in s, mkLetIn (n,b,t,c') @@ -519,7 +520,7 @@ let change_sort_arity sort = let weaken_sort_scheme env evd set sort npars term ty = let evdref = ref evd in let rec drec np elim = - match kind_of_term elim with + match kind elim with | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in @@ -566,7 +567,7 @@ let build_mutual_induction_scheme env sigma = function (List.map (function ((mind',u'),dep',s') -> let (sp',_) = mind' in - if eq_mind sp sp' then + if MutInd.equal sp sp' then let (mibi',mipi') = lookup_mind_specif env mind' in ((mind',u'),mibi',mipi',dep',s') else @@ -605,7 +606,7 @@ let lookup_eliminator ind_sp s = (* Try first to get an eliminator defined in the same section as the *) (* inductive type *) try - let cst =Global.constant_of_delta_kn (make_kn mp dp (Label.of_id id)) in + let cst =Global.constant_of_delta_kn (KerName.make mp dp (Label.of_id id)) in let _ = Global.lookup_constant cst in ConstRef cst with Not_found -> @@ -615,7 +616,7 @@ let lookup_eliminator ind_sp s = with Not_found -> user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ - pr_id id ++ strbrk ", the elimination of the inductive definition " ++ + Id.print id ++ strbrk ", the elimination of the inductive definition " ++ pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 2825c4d83a..a9838cffe5 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -7,14 +7,14 @@ (************************************************************************) open Names -open Term +open Constr open Environ open Evd (** Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive + | NotAllowedCaseAnalysis of (*isrec:*) bool * Sorts.t * pinductive | NotMutualInScheme of inductive * inductive | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive @@ -27,25 +27,25 @@ type dep_flag = bool (** Build a case analysis elimination scheme in some sort family *) val build_case_analysis_scheme : env -> Evd.evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * Constr.t + dep_flag -> Sorts.family -> evar_map * Constr.t (** Build a dependent case elimination predicate unless type is in Prop or is a recursive record with primitive projections. *) val build_case_analysis_scheme_default : env -> evar_map -> pinductive -> - sorts_family -> evar_map * Constr.t + Sorts.family -> evar_map * Constr.t (** Builds a recursive induction scheme (Peano-induction style) in the same sort family as the inductive family; it is dependent if not in Prop or a recursive record with primitive projections. *) val build_induction_scheme : env -> evar_map -> pinductive -> - dep_flag -> sorts_family -> evar_map * constr + dep_flag -> Sorts.family -> evar_map * constr (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * sorts_family) list -> evar_map * constr list + env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) @@ -54,13 +54,13 @@ val build_mutual_induction_scheme : scheme quantified on sort [s]. [set] asks for [s] be declared equal to [i], otherwise just less or equal to [i]. *) -val weaken_sort_scheme : env -> evar_map -> bool -> sorts -> int -> constr -> types -> +val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr -> types -> evar_map * types * constr (** Recursor names utilities *) -val lookup_eliminator : inductive -> sorts_family -> Globnames.global_reference -val elimination_suffix : sorts_family -> string -val make_elimination_ident : Id.t -> sorts_family -> Id.t +val lookup_eliminator : inductive -> Sorts.family -> Globnames.global_reference +val elimination_suffix : Sorts.family -> string +val make_elimination_ident : Id.t -> Sorts.family -> Id.t val case_suffix : string diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 88ca9b5ca8..275a079d5d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -11,6 +11,7 @@ open Util open Names open Univ open Term +open Constr open Vars open Termops open Declarations @@ -83,7 +84,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec (_,i) -> Int.List.mem i listind + | Mrec (_,i) -> Int.List.mem i listind | _ -> false) rvec in Array.exists one_is_rec (dest_subterms rarg) @@ -274,7 +275,7 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | Some (Some _) -> mib.mind_finite == BiFinite | _ -> true (* Annotation for cases *) @@ -360,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches = if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" - Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in let n, subst = List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) + ctx (0, []) in Vars.substl subst br (* substitution in a signature *) @@ -397,8 +398,8 @@ let get_arity env ((ind,u),params) = mib.mind_params_ctxt else begin assert (Int.equal nparams mib.mind_nparams_rec); - let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in - snd (List.chop nnonrecparamdecls mib.mind_params_ctxt) + let nnonrecparamdecls = mib.mind_nparams - mib.mind_nparams_rec in + snd (Termops.context_chop nnonrecparamdecls mib.mind_params_ctxt) end in let parsign = Vars.subst_instance_context u parsign in let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in @@ -485,7 +486,7 @@ let find_inductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found @@ -495,7 +496,7 @@ let find_coinductive env sigma c = let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind - when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> + when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == CoFinite -> let l = List.map EConstr.Unsafe.to_constr l in (ind, l) | _ -> raise Not_found @@ -510,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign = let pv' = whd_all env sigma pval in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> - srec (push_rel_assum (na, t) env) b arsign + srec (push_rel_assum (na, t) env) b arsign | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names - given by the tactics "case" and "inversion": when the - elimination is not dependent, "case" uses Anonymous for - inductive types in Prop and names created by mkProd_name for - inductive types in Set/Type while "inversion" uses anonymous - for inductive types both in Prop and Set/Type !! - - Previously, whether names were created or not relied on - whether the predicate created in Indrec.make_case_com had a - dependent arity or not. To avoid different predicates - printed the same in v8, all predicates built in indrec.ml - got a dependent arity (Aug 2004). The new way to decide - whether names have to be created or not is to use an - Anonymous or Named variable to enforce the expected - dependency status (of course, Anonymous implies non - dependent, but not conversely). + given by the tactics "case" and "inversion": when the + elimination is not dependent, "case" uses Anonymous for + inductive types in Prop and names created by mkProd_name for + inductive types in Set/Type while "inversion" uses anonymous + for inductive types both in Prop and Set/Type !! + + Previously, whether names were created or not relied on + whether the predicate created in Indrec.make_case_com had a + dependent arity or not. To avoid different predicates + printed the same in v8, all predicates built in indrec.ml + got a dependent arity (Aug 2004). The new way to decide + whether names have to be created or not is to use an + Anonymous or Named variable to enforce the expected + dependency status (of course, Anonymous implies non + dependent, but not conversely). From Coq > 8.2, using or not the the effective dependency of the predicate is parametrable! *) @@ -599,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function let ctx,_ = Reduction.dest_arity env ty in let u = Univ.Universe.make l in let s = - (* Does the sort of parameter [u] appear in (or equal) + (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) if univ_level_mem l is then scl (* constrained sort: replace by scl *) else (* unconstrained sort: replace by fresh universe *) let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in - let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in - evdref := evm; s + let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in + evdref := evm; s in (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp) | sign, [] -> sign (* Uniform parameters are exhausted *) @@ -643,7 +644,7 @@ let type_of_projection_knowing_arg env sigma p c ty = syntactic conditions *) let control_only_guard env c = - let check_fix_cofix e c = match kind_of_term c with + let check_fix_cofix e c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix | Fix (_,(_,_,_) as fix) -> @@ -655,93 +656,3 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c - -(* inference of subtyping condition for inductive types *) - -let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let update_contexts (env, evd, csts) csts' = - (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') - in - let basic_check (env, evd, csts) tp = - let result = - if !numchecked >= numparams then - let csts' = - Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) - in update_contexts (env, evd, csts) csts' - else - (env, evd, csts) - in - numchecked := !numchecked + 1; result - in - let infer_typ typ ctxs = - match typ with - | LocalAssum (_, typ') -> - begin - try - let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) - with Reduction.NotConvertible -> - anomaly ~label:"inference of record/inductive subtyping relation failed" - (Pp.str "Can't infer subtyping for record/inductive type") - end - | _ -> anomaly (Pp.str "") - in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in - let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in - if not is_arity then basic_check last_contexts codom else last_contexts - -let infer_inductive_subtyping env evd mind_ent = - let { Entries.mind_entry_params = params; - Entries.mind_entry_inds = entries; - Entries.mind_entry_universes = ground_univs; - } = mind_ent - in - let uinfind = - match ground_univs with - | Entries.Monomorphic_ind_entry _ - | Entries.Polymorphic_ind_entry _ -> ground_univs - | Entries.Cumulative_ind_entry cumi -> - begin - let uctx = Univ.CumulativityInfo.univ_context cumi in - let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in - let dosubst = subst_univs_level_constr sbsubst in - let instance_other = - Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) - in - let constraints_other = - Univ.subst_univs_level_constraints - sbsubst (Univ.UContext.constraints uctx) - in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env in - let env = Environ.push_context uctx_other env in - let evd = - Evd.merge_universe_context - evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) - in - let (_, _, subtyp_constraints) = - List.fold_left - (fun ctxs indentry -> - let _, params = Typeops.infer_local_decls env params in - let ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true params - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor - ctxs dosubst cons false params - ) - ctxs' indentry.Entries.mind_entry_lc - ) (env, evd, Univ.Constraint.empty) entries - in - Entries.Cumulative_ind_entry - (Univ.CumulativityInfo.make - (Univ.CumulativityInfo.univ_context cumi, - Univ.UContext.make - (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), - subtyp_constraints))) - end - in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index aa38d3b47d..55149552aa 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Declarations open Environ open Evd @@ -28,8 +28,8 @@ val arities_of_constructors : env -> pinductive -> types array reasoning either with only recursively uniform parameters or with all parameters including the recursively non-uniform ones *) type inductive_family -val make_ind_family : inductive puniverses * constr list -> inductive_family -val dest_ind_family : inductive_family -> inductive puniverses * constr list +val make_ind_family : inductive Univ.puniverses * constr list -> inductive_family +val dest_ind_family : inductive_family -> inductive Univ.puniverses * constr list val map_ind_family : (constr -> constr) -> inductive_family -> inductive_family val liftn_inductive_family : int -> int -> inductive_family -> inductive_family val lift_inductive_family : int -> inductive_family -> inductive_family @@ -120,7 +120,7 @@ val constructor_nrealdecls_env : env -> constructor -> int val constructor_has_local_defs : constructor -> bool val inductive_has_local_defs : inductive -> bool -val allowed_sorts : env -> inductive -> sorts_family list +val allowed_sorts : env -> inductive -> Sorts.family list (** (Co)Inductive records with primitive projections do not have eta-conversion, hence no dependent elimination. *) @@ -147,17 +147,17 @@ val get_constructor : pinductive * mutual_inductive_body * one_inductive_body * constr list -> int -> constructor_summary val get_constructors : env -> inductive_family -> constructor_summary array -val get_projections : env -> inductive_family -> constant array option +val get_projections : env -> inductive_family -> Constant.t array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family +val get_arity : env -> inductive_family -> Context.Rel.t * Sorts.family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context -val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types +val make_arity : env -> evar_map -> bool -> inductive_family -> Sorts.t -> EConstr.types val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) @@ -172,7 +172,7 @@ val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr. (** Builds the case predicate arity (dependent or not) *) val arity_of_case_predicate : - env -> inductive_family -> bool -> sorts -> types + env -> inductive_family -> bool -> Sorts.t -> types val type_case_branches_with_names : env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types @@ -195,16 +195,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types + env -> evar_map -> Inductive.mind_specif Univ.puniverses -> EConstr.types -> evar_map * EConstr.types (********************) val control_only_guard : env -> types -> unit - -(* inference of subtyping condition for inductive types *) -(* for debugging purposes only to be removed *) -val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> -(Term.constr -> Term.constr) -> -Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t - -val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml new file mode 100644 index 0000000000..a4097237ff --- /dev/null +++ b/pretyping/inferCumulativity.ml @@ -0,0 +1,208 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Reduction +open Declarations +open Constr +open Univ +open Util + +(** Throughout this module we modify a map [variances] from local + universes to [Variance.t]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. *) + +let infer_level_eq u variances = + if LMap.mem u variances + then LMap.set u Variance.Invariant variances + else variances + +let infer_level_leq u variances = + match LMap.find u variances with + | exception Not_found -> variances + | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let variance_pb cv_pb var = + let open Variance in + match cv_pb, var with + | _, Irrelevant -> Irrelevant + | _, Invariant -> Invariant + | CONV, Covariant -> Invariant + | CUMUL, Covariant -> Covariant + +let infer_cumulative_ind_instance cv_pb cumi variances u = + Array.fold_left2 (fun variances varu u -> + match LMap.find u variances with + | exception Not_found -> variances + | varu' -> + LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) + variances (ACumulativityInfo.variance cumi) (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb cumi variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance CONV cumi variances u + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key infos variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let open CClosure in + let hd,stk = whd_stack infos hd stk in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> variances + | FFlex fl -> + let variances = infer_table_key infos variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances codom [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env infos) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env infos) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (ci,p,br,e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let infos = create_clos_infos all env in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor is_arity env variances arcn = + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, infer_term CUMUL env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let typs, codom = Reduction.dest_prod env arcn in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then infer_term CUMUL env variances codom else variances + +let infer_inductive env mie = + let open Entries in + let { mind_entry_params = params; + mind_entry_inds = entries; } = mie + in + let univs = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ + | Polymorphic_ind_entry _ as univs -> univs + | Cumulative_ind_entry cumi -> + let uctx = CumulativityInfo.univ_context cumi in + let uarray = Instance.to_array @@ UContext.instance uctx in + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) + LMap.empty uarray + in + let env, _ = Typeops.infer_local_decls env params in + let variances = List.fold_left (fun variances entry -> + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity + in + List.fold_left (infer_arity_constructor false env) + variances entry.mind_entry_lc) + variances + entries + in + let variances = Array.map (fun u -> LMap.find u variances) uarray in + Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + in + { mie with mind_entry_universes = univs } diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli new file mode 100644 index 0000000000..a5037ea475 --- /dev/null +++ b/pretyping/inferCumulativity.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml new file mode 100644 index 0000000000..be8579c2e5 --- /dev/null +++ b/pretyping/ltac_pretype.ml @@ -0,0 +1,68 @@ +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index bc563b46dc..f0cb8fd1f2 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,7 +30,8 @@ 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 -> Names.Name.equal (snd x) (snd y)) l1 l2 +| GType l1, GType l2 -> + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 | _ -> false let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 39c2ceeba8..b41e15f5a6 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -5,13 +5,12 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Term +open Constr open Vars open Environ open Reduction -open Univ open Declarations open Names open Inductive @@ -20,8 +19,6 @@ open Nativecode open Nativevalues open Context.Rel.Declaration -module RelDecl = Context.Rel.Declaration - (** This module implements normalization by evaluation to OCaml code *) exception Find_at of int @@ -92,7 +89,7 @@ let invert_tag cst tag reloc_tbl = let decompose_prod env t = let (name,dom,codom as res) = destProd (whd_all env t) in match name with - | Anonymous -> (Name (id_of_string "x"),dom,codom) + | Anonymous -> (Name (Id.of_string "x"),dom,codom) | _ -> res let app_type env c = @@ -102,7 +99,7 @@ let app_type env c = let find_rectype_a env c = let (t, l) = app_type env c in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -135,7 +132,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = let construct_of_constr const env tag typ = let t, l = app_type env typ in - match kind_of_term t with + match kind t with | Ind (ind,u) -> construct_of_constr_notnative const env tag ind u l | _ -> assert false @@ -177,44 +174,6 @@ let build_case_type dep p realargs c = if dep then mkApp(mkApp(p, realargs), [|c|]) else mkApp(p, realargs) -(* TODO move this function *) -let type_of_rel env n = - env |> lookup_rel n |> RelDecl.get_type |> lift n - -let type_of_prop = mkSort type1_sort - -let type_of_sort s = - match s with - | Prop _ -> type_of_prop - | Type u -> mkType (Univ.super u) - -let type_of_var env id = - let open Context.Named.Declaration in - try env |> lookup_named id |> get_type - with Not_found -> - anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.") - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - if is_impredicative_set env then - (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) - rangsort - else - (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (sup u1 type0_univ) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (sup type0_univ u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (sup u1 u2) - (* normalisation of values *) let branch_of_switch lvl ans bs = @@ -265,7 +224,7 @@ and nf_accu env sigma accu = if Int.equal (accu_nargs accu) 0 then nf_atom env sigma atom else let a,typ = nf_atom_type env sigma atom in - let _, args = nf_args env sigma accu typ in + let _, args = nf_args env sigma (args_of_accu accu) typ in mkApp(a,Array.of_list args) and nf_accu_type env sigma accu = @@ -273,10 +232,10 @@ and nf_accu_type env sigma accu = if Int.equal (accu_nargs accu) 0 then nf_atom_type env sigma atom else let a,typ = nf_atom_type env sigma atom in - let t, args = nf_args env sigma accu typ in + let t, args = nf_args env sigma (args_of_accu accu) typ in mkApp(a,Array.of_list args), t -and nf_args env sigma accu t = +and nf_args env sigma args t = let aux arg (t,l) = let _,dom,codom = try decompose_prod env t with @@ -287,7 +246,7 @@ and nf_args env sigma accu t = let c = nf_val env sigma arg dom in (subst1 c codom, c::l) in - let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in + let t,l = Array.fold_right aux args (t,[]) in t, List.rev l and nf_bargs env sigma b t = @@ -318,7 +277,6 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aevar (ev,_) -> mkEvar ev | Aproj(p,c) -> let c = nf_accu env sigma c in mkProj(Projection.make p true,c) @@ -328,15 +286,15 @@ and nf_atom_type env sigma atom = match atom with | Arel i -> let n = (nb_rel env - i) in - mkRel n, type_of_rel env n + mkRel n, Typeops.type_of_relative env n | Aconstant cst -> mkConstU cst, Typeops.type_of_constant_in env cst | Aind ind -> mkIndU ind, Inductiveops.type_of_inductive env ind | Asort s -> - mkSort s, type_of_sort s + mkSort s, Typeops.type_of_sort s | Avar id -> - mkVar id, type_of_var env id + mkVar id, Typeops.type_of_variable env id | Acase(ans,accu,p,bs) -> let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in @@ -363,7 +321,7 @@ and nf_atom_type env sigma atom = mkCase(ci, p, a, branchs), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type env sigma t) tt in - let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in + let name = Array.map (fun _ -> (Name (Id.of_string "Ffix"))) tt in let lvl = nb_rel env in let nbfix = Array.length ft in let fargs = mk_rels_accu lvl (Array.length ft) in @@ -376,7 +334,7 @@ and nf_atom_type env sigma atom = mkFix((rp,s),(name,tt,ft)), tt.(s) | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) -> let tt = Array.map (nf_type env sigma) tt in - let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in + let name = Array.map (fun _ -> (Name (Id.of_string "Fcofix"))) tt in let lvl = nb_rel env in let fargs = mk_rels_accu lvl (Array.length ft) in let env = push_rec_types (name,tt,[||]) env in @@ -387,10 +345,10 @@ and nf_atom_type env sigma atom = let vn = mk_rel_accu (nb_rel env) in let env = push_rel (LocalAssum (n,dom)) env in let codom,s2 = nf_type_sort env sigma (codom vn) in - mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2) - | Aevar(ev,ty) -> - let ty = nf_type env sigma ty in - mkEvar ev, ty + mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2 + | Aevar(evk,ty,args) -> + let ty = nf_type env sigma ty in + nf_evar env sigma evk ty args | Ameta(mv,ty) -> let ty = nf_type env sigma ty in mkMeta mv, ty @@ -402,7 +360,7 @@ and nf_atom_type env sigma atom = and nf_predicate env sigma ind mip params v pT = - match kind_of_value v, kind_of_term pT with + match kind_of_value v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in let vb = f (mk_rel_accu k) in @@ -418,7 +376,7 @@ and nf_predicate env sigma ind mip params v pT = | Vfun f, _ -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let name = Name (id_of_string "c") in + let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in let params = if Int.equal n 0 then params else Array.map (lift n) params in @@ -427,6 +385,19 @@ and nf_predicate env sigma ind mip params v pT = true, mkLambda(name,dom,body) | _, _ -> false, nf_type env sigma v +and nf_evar env sigma evk ty args = + let evi = try Evd.find sigma evk with Not_found -> assert false in + let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in + if List.is_empty hyps then begin + assert (Int.equal (Array.length args) 0); + mkEvar (evk, [||]), ty + end + else + let fold accu d = Term.mkNamedProd_or_LetIn d accu in + let t = List.fold_left fold ty hyps in + let ty, args = nf_args env sigma args t in + mkEvar (evk, Array.of_list args), ty + let evars_of_evar_map sigma = { Nativelambda.evars_val = Evd.existential_opt_value sigma; Nativelambda.evars_typ = Evd.existential_type sigma; @@ -477,11 +448,11 @@ let stop_profiler m_pid = match profiler_platform() with "Unix (Linux)" -> stop_profiler_linux m_pid | _ -> () - + 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 + if not Coq_config.native_compiler then 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 5826cc1355..1bec4a6f15 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -12,6 +12,7 @@ open Names open Globnames open Nameops open Term +open Constr open Vars open Glob_term open Pp @@ -58,7 +59,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with fixpoint_eq f1 f2 | PCoFix f1, PCoFix f2 -> cofixpoint_eq f1 f2 -| _ -> false +| PProj (p1, t1), PProj (p2, t2) -> + Projection.equal p1 p2 && constr_pattern_eq t1 t2 +| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ + | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _ + | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = @@ -75,8 +80,8 @@ and cofixpoint_eq (i1, r1) (i2, r2) = and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) = Array.equal Name.equal n1 n2 && - Array.equal Term.eq_constr c1 c2 && - Array.equal Term.eq_constr r1 r2 + Array.equal Constr.equal c1 c2 && + Array.equal Constr.equal r1 r2 let rec occur_meta_pattern = function | PApp (f,args) -> @@ -96,6 +101,31 @@ let rec occur_meta_pattern = function | PMeta _ | PSoApp _ -> true | PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false +let rec occurn_pattern n = function + | PRel p -> Int.equal n p + | PApp (f,args) -> + (occurn_pattern n f) || (Array.exists (occurn_pattern n) args) + | PProj (_,arg) -> occurn_pattern n arg + | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) + | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c) + | PLetIn (na,b,t,c) -> + Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t || + (occurn_pattern (n+1) c) + | PIf (c,c1,c2) -> + (occurn_pattern n c) || + (occurn_pattern n c1) || (occurn_pattern n c2) + | PCase(_,p,c,br) -> + (occurn_pattern n p) || + (occurn_pattern n c) || + (List.exists (fun (_,_,p) -> occurn_pattern n p) br) + | PMeta _ | PSoApp _ -> true + | PEvar (_,args) -> Array.exists (occurn_pattern n) args + | PVar _ | PRef _ | PSort _ -> false + | PFix fix -> not (noccurn n (mkFix fix)) + | PCoFix cofix -> not (noccurn n (mkCoFix cofix)) + +let noccurn_pattern n c = not (occurn_pattern n c) + exception BoundPattern;; let rec head_pattern_bound t = @@ -107,8 +137,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id - | PProj (p,c) -> ConstRef (Projection.constant p) - | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern @@ -124,7 +153,7 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with let pattern_of_constr env sigma t = let rec pattern_of_constr env t = let open Context.Rel.Declaration in - match kind_of_term t with + match kind t with | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id @@ -140,7 +169,7 @@ let pattern_of_constr env sigma t = pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match - match kind_of_term f with + match kind f with | Evar (evk,args) -> (match snd (Evd.evar_source evk sigma) with Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar id) -> Some id @@ -149,7 +178,7 @@ let pattern_of_constr env sigma t = with | Some n -> PSoApp (n,Array.to_list (Array.map (pattern_of_constr env) a)) | None -> PApp (pattern_of_constr env f,Array.map (pattern_of_constr env) a)) - | Const (sp,u) -> PRef (ConstRef (constant_of_kn(canonical_con sp))) + | Const (sp,u) -> PRef (ConstRef (Constant.make1 (Constant.canonical sp))) | Ind (sp,u) -> PRef (canonical_gr (IndRef sp)) | Construct (sp,u) -> PRef (canonical_gr (ConstructRef sp)) | Proj (p, c) -> @@ -204,8 +233,8 @@ let error_instantiate_pattern id l = | [_] -> "is" | _ -> "are" in - user_err (str "Cannot substitute the term bound to " ++ pr_id id - ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l + user_err (str "Cannot substitute the term bound to " ++ Id.print id + ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") let instantiate_pattern env sigma lvar c = @@ -326,7 +355,7 @@ 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 = CAst.with_loc_val (fun ?loc -> function +let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function | GVar id -> (try PRel (List.index Name.equal (Name id) vars) with Not_found -> PVar id) @@ -335,11 +364,14 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | GRef (gr,_) -> PRef (canonical_gr gr) (* Hack to avoid rewriting a complete interpretation of patterns *) - | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) -> + | GApp (c, cl) -> + begin match DAst.get c with + | GPatVar (Evar_kinds.SecondOrderPatVar n) -> metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl) - | GApp (c,cl) -> + | _ -> PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) + end | GLambda (na,bk,c1,c2) -> Name.iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, @@ -364,8 +396,8 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (nal,(_,None),b,c) -> - let mkGLambda na c = CAst.make ?loc @@ - GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in + let mkGLambda na c = DAst.make ?loc @@ + GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; @@ -377,8 +409,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function PCase (cip, PMeta None, pat_of_raw metas vars b, [0,tags,pat_of_raw metas vars c]) | GCases (sty,p,[c,(na,indnames)],brs) -> + let get_ind p = match DAst.get p with + | PatCstr((ind,_),_,_) -> Some ind + | _ -> None + in let get_ind = function - | (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind + | (_,(_,[p],_))::_ -> get_ind p | _ -> None in let ind_tags,ind = match indnames with @@ -391,8 +427,11 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function | 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 { CAst.v = GHole _}), _ -> PMeta None + | None, _ -> PMeta None | Some p, None -> + match DAst.get p with + | GHole _ -> PMeta None + | _ -> user_err ?loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = @@ -406,34 +445,43 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) - | r -> err ?loc (Pp.str "Non supported pattern.") - ) + | GProj(p,c) -> + PProj(p, pat_of_raw metas vars c) + + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> + err ?loc (Pp.str "Non supported pattern.")) and pats_of_glob_branches loc metas vars ind brs = - let get_arg = function - | { CAst.v = PatVar na } -> + let get_arg p = match DAst.get p with + | PatVar na -> Name.iter (fun n -> metas := n::!metas) na; na - | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.") + | PatCstr(_,_,_) -> err ?loc:p.CAst.loc (Pp.str "Non supported pattern.") in let rec get_pat indexes = function | [] -> false, [] - | [(_,(_,[{ 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 -> () + | (loc',(_,[p], br)) :: brs -> + begin match DAst.get p, DAst.get br, brs with + | PatVar Anonymous, GHole _, [] -> + true, [] (* ends with _ => _ *) + | PatCstr((indsp,j),lv,_), _, _ -> + let () = match ind with + | Some sp when eq_ind sp indsp -> () + | _ -> + err ?loc (Pp.str "All constructors must be in the same inductive type.") + in + if Int.Set.mem (j-1) indexes then + 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 + let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in + 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) | _ -> - err ?loc (Pp.str "All constructors must be in the same inductive type.") - in - if Int.Set.mem (j-1) indexes then - 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 - let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in - 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) + err ?loc:loc' (Pp.str "Non supported pattern.") + end | (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 3a1faf1c77..2d1ce1dbc9 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -12,6 +12,7 @@ open Glob_term open Mod_subst open Misctypes open Pattern +open Ltac_pretype (** {5 Functions on patterns} *) @@ -21,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool val subst_pattern : substitution -> constr_pattern -> constr_pattern +val noccurn_pattern : int -> constr_pattern -> bool + exception BoundPattern (** [head_pattern_bound t] extracts the head variable/constant of the diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 54b477bed9..7149d62a19 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -7,20 +7,19 @@ (************************************************************************) open Names -open Term open Environ open EConstr open Type_errors type unification_error = - | OccurCheck of existential_key * constr + | OccurCheck of Evar.t * constr | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr (* Non convertible closed terms *) - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | MetaOccurInBody of Evar.t + | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities @@ -39,8 +38,8 @@ type pretype_error = (* Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (* Tactic unification *) - | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option + | UnifOccurCheck of Evar.t * constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -57,7 +56,7 @@ type pretype_error = | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of - (existential_key * Evar_kinds.t) option * Evar.Set.t option + (Evar.t * Evar_kinds.t) option * Evar.Set.t option exception PretypeError of env * Evd.evar_map * pretype_error diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 124fa6e06c..430755ea04 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Type_errors @@ -15,14 +15,14 @@ open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * constr + | OccurCheck of Evar.t * constr | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | MetaOccurInBody of Evar.t + | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities @@ -41,8 +41,8 @@ type pretype_error = (** Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option + | UnifOccurCheck of Evar.t * constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -59,7 +59,7 @@ type pretype_error = | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of - (existential_key * Evar_kinds.t) option * Evar.Set.t option + (Evar.t * Evar_kinds.t) option * Evar.Set.t option (** unresolvable evar, connex component *) exception PretypeError of env * Evd.evar_map * pretype_error @@ -99,8 +99,8 @@ val error_ill_typed_rec_body : val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> - pinductive -> sorts_family list -> constr -> - unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b + pinductive -> Sorts.family list -> constr -> + unsafe_judgment -> (Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b @@ -112,10 +112,10 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b +val error_occur_check : env -> Evd.evar_map -> Evar.t -> constr -> 'b val error_unsolvable_implicit : - ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> + ?loc:Loc.t -> env -> Evd.evar_map -> Evar.t -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> @@ -154,7 +154,7 @@ val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b (** {6 Typeclass errors } *) -val unsatisfiable_constraints : env -> Evd.evar_map -> Evd.evar option -> +val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option -> Evar.Set.t option -> 'a val unsatisfiable_exception : exn -> bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 40b8bcad92..6700748ebc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,7 @@ open Glob_term open Glob_ops open Evarconv open Misctypes +open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -69,7 +70,7 @@ let get_extra env sigma = let ids = List.map get_id (named_context env) in let avoid = List.fold_right Id.Set.add ids Id.Set.empty in Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) - (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) + (rel_context env) ~init:(empty_csubst, avoid, named_context env) let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) } let rel_context env = rel_context env.env @@ -89,12 +90,11 @@ let push_rel_context sigma ctx env = { let lookup_named id env = lookup_named id env.env let e_new_evar env evdref ?src ?naming typ = - let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in let open Context.Named.Declaration in let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in - let (subst, vsubst, _, nc) = Lazy.force env.extra in - let typ' = subst2 subst vsubst typ in + let (subst, _, nc) = Lazy.force env.extra in + let typ' = csubst_subst subst typ in let instance = inst_rels @ inst_vars in let sign = val_of_named_context nc in let sigma = !evdref in @@ -176,65 +176,79 @@ let _ = optwrite = (:=) Universes.set_minimization }) (** Miscellaneous interpretation functions *) -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 ++ str".") - | 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_known_universe_level evd r = + let loc, qid = Libnames.qualid_of_reference r in + try + match r with + | Libnames.Ident (loc, id) -> Evd.universe_of_name evd id + | Libnames.Qualid _ -> raise Not_found + with Not_found -> + let univ, k = Nametab.locate_universe qid in + Univ.Level.make univ k + +let interp_universe_level_name ~anon_rigidity evd r = + try evd, interp_known_universe_level evd r + with Not_found -> + match r with (* Qualified generated name *) + | Libnames.Qualid (loc, qid) -> + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) + 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 + | Libnames.Ident (loc, id) -> (* Undeclared *) + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc ~name:id univ_rigid evd + else user_err ?loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) 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 -> - (* [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))) + List.fold_left (fun (evd, u) l -> + let evd', u' = + match l with + | Some (l,n) -> + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let anon_rigidity = univ_flexible in + let evd', l = interp_universe_level_name ~anon_rigidity evd l in + let u' = Univ.Universe.make l in + (match n with + | 0 -> evd', u' + | 1 -> evd', Univ.Universe.super u' + | _ -> + user_err ?loc ~hdr:"interp_universe" + (Pp.(str "Cannot interpret universe increment +" ++ int n))) + | None -> + let evd, l = new_univ_level_variable ?loc univ_flexible evd in + evd, Univ.Universe.make l + in (evd', Univ.sup u u')) (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 ~anon_rigidity:univ_flexible evd (Loc.tag ?loc s) - -let interp_sort ?loc evd = function - | GProp -> evd, Prop Null - | GSet -> evd, Prop Pos - | GType n -> - let evd, u = interp_universe ?loc evd n in - evd, Type u +let interp_known_level_info ?loc evd = function + | UUnknown | UAnonymous -> + user_err ?loc ~hdr:"interp_known_level_info" + (str "Anonymous universes not allowed here.") + | UNamed ref -> + try interp_known_universe_level evd ref + with Not_found -> + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) -let interp_elimination_sort = function - | GProp -> InProp - | GSet -> InSet - | GType _ -> InType +let interp_level_info ?loc evd : Misctypes.level_info -> _ = function + | UUnknown -> new_univ_level_variable ?loc univ_rigid evd + | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd + | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s -type inference_hook = env -> evar_map -> evar -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; @@ -364,10 +378,10 @@ let check_evars_are_solved env current_sigma init_sigma = let frozen = frozen_and_pending_holes (init_sigma, current_sigma) in check_evars_are_solved env current_sigma frozen -let process_inference_flags flags env initial_sigma (sigma,c) = +let process_inference_flags flags env initial_sigma (sigma,c,cty) = let sigma = solve_remaining_evars flags env sigma initial_sigma in let c = if flags.expand_evars then nf_evar sigma c else c in - sigma,c + sigma,c,cty let adjust_evar_source evdref na c = match na, kind !evdref c with @@ -393,9 +407,9 @@ 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 (Id.print 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: " ++ Id.print id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -421,8 +435,8 @@ let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id' (rel_context env))) with Not_found -> - user_err (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ + user_err (str "Ltac variable " ++ Id.print id0 ++ + str " depends on pattern variable name " ++ Id.print id ++ str " which is not bound in current context.") let protected_get_type_of env sigma c = @@ -465,7 +479,7 @@ let pretype_id pretype k0 loc env evdref lvar id = 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 - (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ + (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; (* Check if [id] is a section or goal variable *) @@ -478,6 +492,11 @@ let pretype_id pretype k0 loc env evdref lvar id = (*************************************************************************) (* Main pretyping function *) +let interp_known_glob_level ?loc evd = function + | GProp -> Univ.Level.prop + | GSet -> Univ.Level.set + | GType s -> interp_known_level_info ?loc evd s + let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set @@ -572,7 +591,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pretype = pretype k0 resolve_tc in let open Context.Rel.Declaration in let loc = t.CAst.loc in - match t.CAst.v with + match DAst.get t with | GRef (ref,u) -> inh_conv_coerce_to_tycon ?loc env evdref (pretype_ref ?loc evdref env ref u) @@ -718,6 +737,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_sort ?loc evdref s in inh_conv_coerce_to_tycon ?loc env evdref j tycon + | GProj (p, c) -> + (* TODO: once GProj is used as an input syntax, use bidirectional typing here *) + let cj = pretype empty_tycon env evdref lvar c in + judge_of_projection env.ExtraEnv.env !evdref p cj + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in @@ -899,6 +923,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in + let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) fsign + else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in @@ -1008,6 +1035,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in + let cs_args = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) cs_args + else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = List.map (set_name Anonymous) cs_args in @@ -1093,24 +1124,16 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ - str " in current context: no binding for " ++ pr_id id ++ str ".") in + str " in current context: no binding for " ++ Id.print id ++ str ".") in ((id,c)::subst, update) in let subst,inst = List.fold_right f hyps ([],update) in check_instance loc subst inst; Array.map_of_list snd subst (* [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 - | { 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 - | Type _ -> true - | Prop _ -> false - end - | Cast (c, _, _) -> is_Type c - | _ -> false - in +and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with + | GHole (knd, naming, None) -> + let loc = loc_of_glob_constr c in (match valcon with | Some v -> let s = @@ -1118,7 +1141,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let t = Retyping.get_type_of env.ExtraEnv.env sigma v in match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with | Sort s -> ESorts.kind sigma s - | Evar ev when is_Type (existential_type sigma ev) -> + | Evar ev when is_Type sigma (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in @@ -1134,7 +1157,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) - | 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 @@ -1150,15 +1173,18 @@ let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env sigma in let evdref = ref sigma in let k0 = Context.Rel.length (rel_context env) in - let c' = match kind with + let c', c'_ty = match kind with | WithoutTypeConstraint -> - (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in + j.uj_val, j.uj_type | OfType exptyp -> - (pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val + let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in + j.uj_val, j.uj_type | IsType -> - (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val + let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in + tj.utj_val, mkSort tj.utj_type in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty) let default_inference_flags fail = { use_typeclasses = true; @@ -1178,7 +1204,7 @@ let all_and_fail_flags = default_inference_flags true let all_no_fail_flags = default_inference_flags false let ise_pretype_gen_ctx flags env sigma lvar kind c = - let evd, c = ise_pretype_gen flags env sigma lvar kind c in + let evd, c, _ = ise_pretype_gen flags env sigma lvar kind c in let evd, f = Evarutil.nf_evars_and_universes evd in f (EConstr.Unsafe.to_constr c), Evd.evar_universe_context evd @@ -1190,12 +1216,15 @@ let understand env sigma c = ise_pretype_gen_ctx flags env sigma empty_lvar expected_type c -let understand_tcc ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = - let (sigma, c) = ise_pretype_gen flags env sigma empty_lvar expected_type c in - (sigma, c) +let understand_tcc_ty ?(flags=all_no_fail_flags) env sigma ?(expected_type=WithoutTypeConstraint) c = + ise_pretype_gen flags env sigma empty_lvar expected_type c + +let understand_tcc ?flags env sigma ?expected_type c = + let sigma, c, _ = understand_tcc_ty ?flags env sigma ?expected_type c in + sigma, c let understand_ltac flags env sigma lvar kind c = - let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in + let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) let pretype k0 resolve_tc typcon env evdref lvar t = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7395e94a09..864768fe56 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,13 +12,16 @@ into elementary ones, insertion of coercions and resolution of implicit arguments. *) -open Term +open Constr open Environ open Evd open EConstr open Glob_term -open Evarutil -open Misctypes +open Ltac_pretype +open Evardefine + +val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> + Misctypes.glob_level -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) @@ -27,7 +30,7 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type inference_hook = env -> evar_map -> evar -> evar_map * constr +type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; @@ -55,6 +58,11 @@ val all_and_fail_flags : inference_flags val understand_tcc : ?flags:inference_flags -> env -> evar_map -> ?expected_type:typing_constraint -> glob_constr -> evar_map * constr +(** As [understand_tcc] but also returns the type of the elaborated term. + The [expand_evars] flag is not applied to the type (only to the term). *) +val understand_tcc_ty : ?flags:inference_flags -> env -> evar_map -> + ?expected_type:typing_constraint -> glob_constr -> evar_map * constr * types + (** More general entry point with evars from ltac *) (** Generic call to the interpreter from glob_constr to constr @@ -113,15 +121,12 @@ val pretype_type : val ise_pretype_gen : inference_flags -> env -> evar_map -> - ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types (**/**) (** To embed constr in glob_constr *) -val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts -val interp_elimination_sort : glob_sort -> sorts_family - 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/pretyping.mllib b/pretyping/pretyping.mllib index c8b3307d76..ae4ad0be7d 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,7 +1,10 @@ +Geninterp +Ltac_pretype Locusops Pretype_errors Reductionops Inductiveops +InferCumulativity Vnorm Arguments_renaming Nativenorm @@ -29,3 +32,4 @@ Indrec Cases Pretyping Unification +Univdecls diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index a23579609a..ab1f3cd320 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -19,7 +19,7 @@ open Pp open Names open Globnames open Nametab -open Term +open Constr open Libobject open Mod_subst open Reductionops @@ -37,7 +37,7 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } let structure_table = Summary.ref (Indmap.empty : struc_typ Indmap.t) ~name:"record-structs" @@ -48,7 +48,7 @@ let projection_table = is the inductive always (fst constructor) ? It seems so... *) type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in @@ -144,7 +144,7 @@ type obj_typ = { type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs let eq_cs_pattern p1 p2 = match p1, p2 with @@ -171,8 +171,8 @@ let keep_true_projections projs kinds = let filter (p, (_, b)) = if b then Some p else None in List.map_filter filter (List.combine projs kinds) -let cs_pattern_of_constr t = - match kind_of_term t with +let cs_pattern_of_constr env t = + match kind t with App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs @@ -180,7 +180,11 @@ let cs_pattern_of_constr t = end | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Sort s -> Sort_cs (family_of_sort s), None, [] + | Proj (p, c) -> + let { Environ.uj_type = ty } = Typeops.infer env c in + let _, params = Inductive.find_rectype env ty in + Const_cs (ConstRef (Projection.constant p)), None, params @ [c] + | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> begin try Const_cs (global_of_constr t) , None, [] @@ -190,7 +194,6 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" (fun (sign,env,t,con,proji_sp) -> - let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in @@ -207,14 +210,16 @@ let compute_canonical_projections warn (con,ind) = let v = (mkConstU (con,u)) in let c = Environ.constant_value_in env (con,u) in let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in + let lt = List.rev_map snd sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in let params, projs = List.chop p args in let lpj = keep_true_projections lpj kl in let lps = List.combine lpj projs in + let nenv = Termops.push_rels_assum sign env in let comp = List.fold_left (fun l (spopt,t) -> (* comp=components *) @@ -222,7 +227,7 @@ let compute_canonical_projections warn (con,ind) = | Some proji_sp -> begin try - let patt, n , args = cs_pattern_of_constr t in + let patt, n , args = cs_pattern_of_constr nenv t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); @@ -281,7 +286,7 @@ let subst_canonical_structure (subst,(cst,ind as obj)) = let discharge_canonical_structure (_,(cst,ind)) = Some (Lib.discharge_con cst,Lib.discharge_inductive ind) -let inCanonStruc : constant * inductive -> obj = +let inCanonStruc : Constant.t * inductive -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with open_function = open_canonical_structure; cache_function = cache_canonical_structure; @@ -293,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) (*s High-level declaration of a canonical structure *) -let error_not_structure ref = +let error_not_structure ref description = user_err ~hdr:"object_declare" - (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") + (str"Could not declare a canonical structure " ++ + (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + str(description))) let check_and_decompose_canonical_structure ref = - let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in + let sp = + match ref with + ConstRef sp -> sp + | _ -> error_not_structure ref "Expected an instance of a record or structure." + in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref in + | None -> error_not_structure ref "Could not find its value in the global environment." in let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let body = EConstr.Unsafe.to_constr body in - let f,args = match kind_of_term body with + let f,args = match kind body with | App (f,args) -> f,args - | _ -> error_not_structure ref in - let indsp = match kind_of_term f with + | _ -> + error_not_structure ref "Expected a record or structure constructor applied to arguments." in + let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref in - let s = try lookup_structure indsp with Not_found -> error_not_structure ref in + | _ -> error_not_structure ref "Expected an instance of a record or structure." in + let s = + try lookup_structure indsp + with Not_found -> + error_not_structure ref + ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref; + error_not_structure ref "Got too few arguments to the record or structure constructor."; (sp,indsp) let declare_canonical_structure ref = @@ -324,15 +340,25 @@ let declare_canonical_structure ref = let lookup_canonical_conversion (proj,pat) = assoc_pat pat (Refmap.find proj !object_table) +let decompose_projection sigma c args = + match EConstr.kind sigma c with + | Const (c, u) -> + let n = find_projection_nparams (ConstRef c) in + (** Check if there is some canonical projection attached to this structure *) + let _ = Refmap.find (ConstRef c) !object_table in + let arg = Stack.nth args n in + arg + | Proj (p, c) -> + let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in + c + | _ -> raise Not_found + let is_open_canonical_projection env sigma (c,args) = let open EConstr in try - let (ref, _) = Termops.global_of_constr sigma c in - let n = find_projection_nparams ref in - (** Check if there is some canonical projection attached to this structure *) - let _ = Refmap.find ref !object_table in + let arg = decompose_projection sigma c args in try - let arg = whd_all env sigma (Stack.nth args n) in + let arg = whd_all env sigma arg in let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in not (isConstruct sigma hd) with Failure _ -> false diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5480b14af0..f15418577d 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Globnames (** Operations concerning records and canonical structures *) @@ -20,10 +20,10 @@ type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; s_PROJKIND : (Name.t * bool) list; - s_PROJ : constant option list } + s_PROJ : Constant.t option list } type struc_tuple = - inductive * constructor * (Name.t * bool) list * constant option list + inductive * constructor * (Name.t * bool) list * Constant.t option list val declare_structure : struc_tuple -> unit @@ -35,7 +35,7 @@ val lookup_structure : inductive -> struc_typ (** [lookup_projections isp] returns the projections associated to the inductive path [isp] if it corresponds to a structure, otherwise it fails with [Not_found] *) -val lookup_projections : inductive -> constant option list +val lookup_projections : inductive -> Constant.t option list (** raise [Not_found] if not a projection *) val find_projection_nparams : global_reference -> int @@ -52,7 +52,7 @@ val find_projection : global_reference -> struc_typ type cs_pattern = Const_cs of global_reference | Prod_cs - | Sort_cs of sorts_family + | Sort_cs of Sorts.family | Default_cs type obj_typ = { @@ -65,7 +65,7 @@ type obj_typ = { o_TCOMPS : constr list } (** ordered *) (** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list +val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list val pr_cs_pattern : cs_pattern -> Pp.t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3563235434..418ea271cd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Termops open Univ open Evd @@ -121,10 +121,10 @@ module ReductionBehaviour = struct let r' = fst (subst_global subst r) in if r==r' then orig else (r',o) let discharge = function - | _,(ReqGlobal (ConstRef c, req), (_, b)) -> + | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) -> let b = - if Lib.is_in_section (ConstRef c) then - let vars, _, _ = Lib.section_segment_of_constant c in + if Lib.is_in_section gr then + let vars = Lib.variable_section_segment_of_reference gr in let extra = List.length vars in let nargs' = if b.b_nargs = max_int then max_int @@ -284,8 +284,6 @@ sig | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list exception IncompatibleFold2 @@ -296,12 +294,12 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) - val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool) - -> 'a t -> 'a t -> (int * int) option + val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool) + -> 'a t -> 'a t -> bool val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val append_app_list : 'a list -> 'a t -> 'a t val strip_app : 'a t -> 'a t * 'a t val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -339,12 +337,10 @@ struct type 'a member = | App of 'a app_node - | Case of Term.case_info * 'a * 'a array * Cst_stack.t + | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list let rec pr_member pr_c member = @@ -358,7 +354,7 @@ struct ++ str ")" | Proj (n,m,p,cst) -> str "ZProj(" ++ int n ++ pr_comma () ++ int m ++ - pr_comma () ++ pr_con (Projection.constant p) ++ str ")" + pr_comma () ++ Constant.print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -367,8 +363,6 @@ struct ++ pr_comma () ++ prlist_with_sep pr_semicolon int remains ++ pr_comma () ++ pr pr_c params ++ str ")" - | Shift i -> str "ZShift(" ++ int i ++ str ")" - | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l @@ -403,54 +397,42 @@ struct else (l.(j), sk) let equal f f_fix sk1 sk2 = - let equal_cst_member x lft1 y lft2 = + let equal_cst_member x y = match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + Constant.equal (Projection.constant p1) (Projection.constant p2) | _, _ -> false in - let rec equal_rec sk1 lft1 sk2 lft2 = + let rec equal_rec sk1 sk2 = match sk1,sk2 with - | [],[] -> Some (lft1,lft2) - | (Update _ :: _, _ | _, Update _ :: _) -> assert false - | Shift k :: s1, _ -> equal_rec s1 (lft1+k) sk2 lft2 - | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k) + | [],[] -> true | App a1 :: s1, App a2 :: s2 -> - let t1,s1' = decomp_node_last a1 s1 in - let t2,s2' = decomp_node_last a2 s2 in - if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None + let t1,s1' = decomp_node_last a1 s1 in + let t2,s2' = decomp_node_last a2 s2 in + (f t1 t2) && (equal_rec s1' s2') | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> - if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2 - then equal_rec s1 lft1 s2 lft2 - else None + f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> - if Int.equal n1 n2 && Int.equal m1 m2 - && Constant.equal (Projection.constant p) (Projection.constant p2) - then equal_rec s1 lft1 s2 lft2 - else None + Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) + && equal_rec s1 s2 | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> - if f_fix (f1,lft1) (f2,lft2) then - match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with - | None -> None - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - else None + f_fix f1 f2 + && equal_rec (List.rev s1) (List.rev s2) + && equal_rec s1' s2' | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> - if equal_cst_member c1 lft1 c2 lft2 then - match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - | None -> None - else None - | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None - in equal_rec (List.rev sk1) 0 (List.rev sk2) 0 + equal_cst_member c1 c2 + && equal_rec (List.rev params1) (List.rev params2) + && equal_rec s1' s2' + | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false + in equal_rec (List.rev sk1) (List.rev sk2) let compare_shape stk1 stk2 = let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with ([],[]) -> Int.equal bal 0 - | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2 - | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> @@ -466,40 +448,29 @@ struct exception IncompatibleFold2 let fold2 f o sk1 sk2 = - let rec aux o lft1 sk1 lft2 sk2 = - let fold_array = - Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y)) - in + let rec aux o sk1 sk2 = match sk1,sk2 with - | [], [] -> o,lft1,lft2 - | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2 - | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2 + | [], [] -> o | App n1 :: q1, App n2 :: q2 -> - let t1,l1 = decomp_node_last n1 q1 in - let t2,l2 = decomp_node_last n2 q2 in - aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - lft1 l1 lft2 l2 + let t1,l1 = decomp_node_last n1 q1 in + let t2,l2 = decomp_node_last n2 q2 in + aux (f o t1 t2) l1 l2 | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> - aux (fold_array - (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - a1 a2) lft1 q1 lft2 q2 + aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> - aux o lft1 q1 lft2 q2 + aux o q1 q2 | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> - let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2) - lft1 (List.rev s1) lft2 (List.rev s2) in - aux o' lft1' q1 lft2' q2 + let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in + aux o' q1 q2 | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> - let (o',lft1',lft2') = - aux o lft1 (List.rev params1) lft2 (List.rev params2) - in aux o' lft1' q1 lft2' q2 - | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> - raise IncompatibleFold2 - in aux o 0 (List.rev sk1) 0 (List.rev sk2) + let o' = aux o (List.rev params1) (List.rev params2) in + aux o' q1 q2 + | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + raise IncompatibleFold2 + in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function - | Update _ -> assert false - | (Proj (_,_,_,_) | Shift _) as e -> e + | (Proj (_,_,_,_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -516,18 +487,15 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | Shift(_)::s -> args_size s - | Update(_)::s -> args_size s | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 let strip_app s = let rec aux out = function - | ( App _ | Shift _ as e) :: s -> aux (e :: out) s + | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s let strip_n_app n s = let rec aux n out = function - | Shift k as e :: s -> aux n (e :: out) s | App (i,a,j) as e :: s -> let nb = j - i + 1 in if n >= nb then @@ -552,14 +520,12 @@ struct let list_of_app_stack s = let rec aux = function | App (i,a,j) :: s -> - let (k,(args',s')) = aux s in - let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in - k,(Array.fold_right (fun x y -> x::y) a' args', s') - | Shift n :: s -> - let (k,(args',s')) = aux s in (k+n,(args', s')) - | s -> (0,([],s)) in - let (lft,(out,s')) = aux s in - let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in + let (args',s') = aux s in + let a' = Array.sub a i (j - i + 1) in + (Array.fold_right (fun x y -> x::y) a' args', s') + | s -> ([],s) in + let (out,s') = aux s in + let init = match s' with [] -> true | _ -> false in Option.init init out let assign s p c = @@ -568,20 +534,18 @@ struct | None -> assert false let tail n0 s0 = - let rec aux lft n s = - let out s = if Int.equal lft 0 then s else Shift lft :: s in - if Int.equal n 0 then out s else + let rec aux n s = + if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> let nb = j - i + 1 in if n >= nb then - aux lft (n - nb) s + aux (n - nb) s else let p = i+n in if j >= p then App(p,a,j)::s else s - | Shift k :: s' -> aux (lft+k) n s' | _ -> raise (Invalid_argument "Reductionops.Stack.tail") - in aux 0 n0 s0 + in aux n0 s0 let nth s p = match strip_n_app p s with @@ -627,11 +591,9 @@ struct zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Shift n::s) -> zip (lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) - | _, (Update _::_) -> assert false in zip s @@ -868,11 +830,9 @@ let _ = Goptions.declare_bool_option { } let equal_stacks sigma (x, l) (y, l') = - let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in - let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in - match Stack.equal f_equal eq_fix l l' with - | None -> false - | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) + let f_equal x y = eq_constr sigma x y in + let eq_fix a b = f_equal (mkFix a) (mkFix b) in + Stack.equal f_equal eq_fix l l' && f_equal x y let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in @@ -1074,7 +1034,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg, Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end - |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1155,7 +1115,7 @@ let local_whd_state_gen flags sigma = |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) - |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1167,7 +1127,8 @@ let local_whd_state_gen flags sigma = |_ -> s else s - | x -> s + | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s + in whrec @@ -1280,9 +1241,9 @@ let clos_whd_flags flgs env sigma t = (CClosure.inject (EConstr.Unsafe.to_constr t))) 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 ()) -let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ()) +let nf_beta = clos_norm_flags CClosure.beta +let nf_betaiota = clos_norm_flags CClosure.betaiota +let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta let nf_all env sigma = clos_norm_flags CClosure.all env sigma @@ -1291,11 +1252,11 @@ let nf_all env sigma = (* Conversion *) (********************************************************************) (* -let fkey = Profile.declare_profile "fhnf";; -let fhnf info v = Profile.profile2 fkey fhnf info v;; +let fkey = CProfile.declare_profile "fhnf";; +let fhnf info v = CProfile.profile2 fkey fhnf info v;; -let fakey = Profile.declare_profile "fhnf_apply";; -let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; +let fakey = CProfile.declare_profile "fhnf_apply";; +let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;; *) let is_transparent e k = @@ -1305,7 +1266,7 @@ let is_transparent e k = (* Conversion utility functions *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t let pb_is_equal pb = pb == Reduction.CONV @@ -1314,7 +1275,9 @@ let pb_equal = function | Reduction.CONV -> Reduction.CONV let report_anomaly e = - let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in + let msg = Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) in + let e = UserError (None,msg) in let e = CErrors.push e in iraise e @@ -1361,94 +1324,28 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let len_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) - in - let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((len_instance = Univ.Instance.length u) && - (len_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_sbctx - in - let comp_cst = - match cv_pb with - Reduction.CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in - Univ.Constraint.union comp_cst comp_cst' - | Reduction.CUMUL -> comp_cst - in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible - -let sigma_conv_inductives - cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - if not (num_param_arity = sv1 && num_param_arity = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances cv_pb cumi u1 u2 sigma - -let sigma_conv_constructors - (mind, ind, cns) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - nparamsctxt + - mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) - in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma +let sigma_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = - { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances; - Reduction.conv_inductives = sigma_conv_inductives; - Reduction.conv_constructors = sigma_conv_constructors} + let open Reduction in + { compare_sorts = sigma_compare_sorts; + compare_instances = sigma_compare_instances; + compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) - let open Universes in - let x = EConstr.Unsafe.to_constr x in - let y = EConstr.Unsafe.to_constr y in try - let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + EConstr.leq_constr_universes sigma x y else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + EConstr.eq_constr_universes sigma x y in let ans = match ans with | None -> None @@ -1462,6 +1359,8 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) in if b then sigma, true else + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in @@ -1684,7 +1583,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' - |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' + |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = @@ -1771,8 +1670,8 @@ let meta_reducible_instance evd b = let is_coerce = match s with CoerceToType -> true | _ -> false in if not is_coerce then irec g else u with Not_found -> u) - | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) -> - let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) in + | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) -> + let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in (match try let g, s = Metamap.find m metas in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1828196fe4..0565baf45f 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open EConstr open Univ open Evd @@ -82,8 +82,6 @@ module Stack : sig | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list val pr : ('a -> Pp.t) -> 'a t -> Pp.t @@ -102,12 +100,12 @@ module Stack : sig @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 + constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App or Shift *) + start by App *) val strip_app : 'a t -> 'a t * 'a t (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -170,9 +168,9 @@ val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) -val nf_beta : local_reduction_function -val nf_betaiota : local_reduction_function -val nf_betaiotazeta : local_reduction_function +val nf_beta : reduction_function +val nf_betaiota : reduction_function +val nf_betaiotazeta : reduction_function val nf_all : reduction_function val nf_evar : evar_map -> constr -> constr @@ -258,11 +256,11 @@ val contract_fix : ?env:Environ.env -> evar_map -> ?reference:Constant.t -> fixp val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) -val is_transparent : Environ.env -> constant tableKey -> bool +val is_transparent : Environ.env -> Constant.t tableKey -> bool (** {6 Conversion Functions (uses closures, lazy strategy) } *) -type conversion_test = constraints -> constraints +type conversion_test = Constraint.t -> Constraint.t val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 079524f344..00b175c486 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -10,6 +10,7 @@ open Pp open CErrors open Util open Term +open Constr open Inductive open Inductiveops open Names @@ -146,7 +147,7 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> type1_sort + | Prop _ -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> @@ -165,23 +166,6 @@ let retype ?(polyprop=true) sigma = | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> decomp_sort env sigma (type_of env t) - and sort_family_of env t = - match EConstr.kind sigma t with - | Cast (c,_, s) when isSort sigma s -> family_of_sort (destSort sigma s) - | Sort _ -> InType - | Prod (name,t,c2) -> - let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in - if not (is_impredicative_set env) && - s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> - let t = type_of_global_reference_knowing_parameters env f args in - family_of_sort (sort_of_atomic_type env sigma t args) - | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) - | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | _ -> - family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in @@ -197,15 +181,34 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (type_of_constructor env (cstr, u)) | _ -> assert false - in type_of, sort_of, sort_family_of, - type_of_global_reference_knowing_parameters + in type_of, sort_of, type_of_global_reference_knowing_parameters + +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = + let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in + let rec sort_family_of env t = + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) + | Sort _ -> InType + | Prod (name,t,c2) -> + let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in + if not (is_impredicative_set env) && + s2 == InSet && sort_family_of env t == InType then InType else s2 + | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else + let t = type_of_global_reference_knowing_parameters env f args in + Sorts.family (sort_of_atomic_type env sigma t args) + | App(f,args) -> + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) + | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | _ -> + Sorts.family (decomp_sort env sigma (type_of env t)) + in sort_family_of env t let get_sort_of ?(polyprop=true) env sigma t = - let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t -let get_sort_family_of ?(polyprop=true) env sigma c = - let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c + let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = match EConstr.kind sigma c with @@ -214,7 +217,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty | Const (cst, u) -> let t = constant_type_in env (cst, EInstance.kind sigma u) in - (* TODO *) sigma, EConstr.of_constr t | Var id -> sigma, type_of_var env id | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) @@ -225,14 +227,14 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = - let f,_,_,_ = retype ~polyprop sigma in + let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index ed3a9d0f96..6fdde90463 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Evd open Environ open EConstr @@ -30,10 +29,13 @@ val get_type_of : ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types val get_sort_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts + ?polyprop:bool -> env -> evar_map -> types -> Sorts.t +(* When [truncation_style] is [true], tells if the type has been explicitly + truncated to Prop or (impredicative) Set; in particular, singleton type and + small inductive types, which have all eliminations to Type, are in Type *) val get_sort_family_of : - ?polyprop:bool -> env -> evar_map -> types -> sorts_family + ?truncation_style:bool -> ?polyprop:bool -> env -> evar_map -> types -> Sorts.family (** Makes an unsafe judgment from a constr *) val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment @@ -44,7 +46,7 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr -> val type_of_global_reference_knowing_conclusion : env -> evar_map -> constr -> types -> evar_map * types -val sorts_of_context : env -> evar_map -> rel_context -> sorts list +val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 708788ab87..9b9408698d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u = match evref with | EvalConstRef con -> let u = Unsafe.to_instance u in - EConstr.of_constr (try constant_value_in env (con,u) - with NotEvaluableConst IsProj -> - raise (Invalid_argument "value_of_evaluable_ref")) + EConstr.of_constr (constant_value_in env (con, u)) | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function @@ -75,13 +73,13 @@ let global_of_evaluable_reference = function | EvalVarRef id -> VarRef id type evaluable_reference = - | EvalConst of constant + | EvalConst of Constant.t | EvalVar of Id.t | EvalRel of int | EvalEvar of EConstr.existential let evaluable_reference_eq sigma r1 r2 = match r1, r2 with -| EvalConst c1, EvalConst c2 -> eq_constant c1 c2 +| EvalConst c1, EvalConst c2 -> Constant.equal c1 c2 | EvalVar id1, EvalVar id2 -> Id.equal id1 id2 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) -> @@ -240,7 +238,7 @@ let invert_name labs l na0 env sigma ref = function | EvalRel _ | EvalEvar _ -> None | EvalVar id' -> Some (EvalVar id) | EvalConst kn -> - Some (EvalConst (con_with_label kn (Label.of_id id))) in + Some (EvalConst (Constant.change_label kn (Label.of_id id))) in match refi with | None -> None | Some ref -> @@ -476,7 +474,7 @@ let contract_fix_use_function env sigma f let nbodies = Array.length recindices in let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in let lbodies = List.init nbodies make_Fi in - substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum)) + substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum)) let reduce_fix_use_function env sigma f whfun fix stack = match fix_recarg fix (Stack.append_app_list stack Stack.empty) with @@ -500,7 +498,7 @@ let contract_cofix_use_function env sigma f let make_Fi j = (mkCoFix(j,typedbodies), f j) in let subbodies = List.init nbodies make_Fi in substl_checking_arity env (List.rev subbodies) - sigma (nf_beta sigma bodies.(bodynum)) + sigma (nf_beta env sigma bodies.(bodynum)) let reduce_mind_case_use_function func env sigma mia = match EConstr.kind sigma mia.mconstr with @@ -521,7 +519,7 @@ let reduce_mind_case_use_function func env sigma mia = the block was indeed initially built as a global definition *) let (kn, u) = destConst sigma func in - let kn = con_with_label kn (Label.of_id id) in + let kn = Constant.change_label kn (Label.of_id id) in let cst = (kn, EInstance.kind sigma u) in try match constant_opt_value_in env cst with | None -> None @@ -697,7 +695,7 @@ let rec red_elim_const env sigma ref u largs = let whfun = whd_construct_stack env sigma in (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase) + | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min -> let rec descend (ref,u) args = let c = reference_value env sigma ref u in @@ -712,7 +710,7 @@ let rec red_elim_const env sigma ref u largs = let whfun = whd_construct_stack env sigma in (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with | NotReducible -> raise Redelimination - | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase) + | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase) | NotAnElimination when unfold_nonelim -> let c = reference_value env sigma ref u in (whd_betaiotazeta sigma (applist (c, largs)), []), nocase @@ -927,8 +925,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c = let whd_simpl_stack = if Flags.profile then - let key = Profile.declare_profile "whd_simpl_stack" in - Profile.profile3 key whd_simpl_stack + let key = CProfile.declare_profile "whd_simpl_stack" in + CProfile.profile3 key whd_simpl_stack else whd_simpl_stack (* Same as [whd_simpl] but also reduces constants that do not hide a @@ -944,7 +942,7 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | CoFix _ | Fix _ -> s' | Proj (p,t) when (match EConstr.kind sigma constr with - | Const (c', _) -> eq_constant (Projection.constant p) c' + | Const (c', _) -> Constant.equal (Projection.constant p) c' | _ -> false) -> let pb = Environ.lookup_projection p env in if List.length stack <= pb.Declarations.proj_npars then @@ -1050,8 +1048,8 @@ let contextually byhead occs f env sigma t = let match_constr_evaluable_ref sigma c evref = match EConstr.kind sigma c, evref with - | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u - | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty + | Const (c,u), EvalConstRef c' when Constant.equal c c' -> Some u + | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None let substlin env sigma evalref n (nowhere_except_in,locs) c = @@ -1103,7 +1101,7 @@ let unfoldoccs env sigma (occs,name) c = | [] -> () | _ -> error_invalid_occurrence rest in - nf_betaiotazeta sigma uc + nf_betaiotazeta env sigma uc in match occs with | NoOccurrences -> c @@ -1284,7 +1282,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = else raise Not_found with Not_found -> try - let t' = nf_betaiota sigma (one_step_reduce env sigma t) in + let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in elimrec env t' l with NotStepReducible -> error_cannot_recognize ref in diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 91726e8c6d..a6b8262f7f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -15,6 +15,7 @@ open Pattern open Globnames open Locus open Univ +open Ltac_pretype type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 375a8a983f..3f947fd23f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,6 +11,7 @@ open Names open Globnames open Decl_kinds open Term +open Constr open Vars open Evd open Util @@ -64,14 +65,14 @@ type typeclass = { cl_impl : global_reference; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + cl_context : global_reference option list * Context.Rel.t; (* Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option - * constant option) list; + * Constant.t option) list; cl_strict : bool; @@ -86,7 +87,6 @@ type instance = { (* Sections where the instance should be redeclared, None for discard, Some 0 for none. *) is_global: int option; - is_poly: bool; is_impl: global_reference; } @@ -96,7 +96,7 @@ let instance_impl is = is.is_impl let hint_priority is = is.is_info.Vernacexpr.hint_priority -let new_instance cl info glob poly impl = +let new_instance cl info glob impl = let global = if glob then Some (Lib.sections_depth ()) else None @@ -106,7 +106,6 @@ let new_instance cl info glob poly impl = { is_class = cl.cl_impl; is_info = info ; is_global = global ; - is_poly = poly; is_impl = impl } (* @@ -174,7 +173,7 @@ let subst_class (subst,cl) = and do_subst_gr gr = fst (subst_global subst gr) in let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs, + List.smartmap (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in @@ -212,15 +211,16 @@ let discharge_class (_,cl) = let newgrs = List.map (fun decl -> match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with | None -> None - | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true)) + | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs + List.smartmap (Option.smartmap Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, _, _ as info = abs_context cl in + let info = abs_context cl in + let ctx = info.Lib.abstr_ctx in let ctx, subst = rel_of_variable_context ctx in let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in @@ -419,7 +419,7 @@ let declare_instance info local glob = match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); - add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob) + add_instance (new_instance tc info (not local) glob) | None -> () let add_class cl = @@ -441,19 +441,20 @@ let add_class cl = let instance_constructor (cl,u) args = let lenpars = List.count is_local_assum (snd cl.cl_context) in + let open EConstr in let pars = fst (List.chop lenpars args) in match cl.cl_impl with | IndRef ind -> let ind = ind, u in - (Some (applistc (mkConstructUi (ind, 1)) args), - applistc (mkIndU ind) pars) + (Some (applist (mkConstructUi (ind, 1), args)), + applist (mkIndU ind, pars)) | ConstRef cst -> let cst = cst, u in let term = match args with | [] -> None | _ -> Some (List.last args) in - (term, applistc (mkConstU cst) pars) + (term, applist (mkConstU cst, pars)) | _ -> assert false let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes [] @@ -520,7 +521,7 @@ let mark_unresolvable evi = mark_resolvability false evi let mark_resolvable evi = mark_resolvability true evi open Evar_kinds -type evar_filter = existential_key -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t -> bool let all_evars _ _ = true let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false @@ -551,8 +552,8 @@ let solve_all_instances env evd filter unique split fail = Hook.get get_solve_all_instances env evd filter unique split fail (** Profiling resolution of typeclasses *) -(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) -(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) +(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) +(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 99cdbd3a36..ee28ec173b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -8,7 +8,7 @@ open Names open Globnames -open Term +open Constr open Evd open Environ @@ -25,9 +25,8 @@ type typeclass = { cl_impl : global_reference; (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. - The boolean indicates if the typeclass argument is a direct superclass and the global reference - gives a direct link to the class itself. *) - cl_context : (global_reference * bool) option list * Context.Rel.t; + The global reference gives a direct link to the class itself. *) + cl_context : global_reference option list * Context.Rel.t; (** Context of definitions and properties on defs, will not be shared *) cl_props : Context.Rel.t; @@ -36,7 +35,7 @@ type typeclass = { Some may be undefinable due to sorting restrictions or simply undefined if no name is provided. The [int option option] indicates subclasses whose hint has the given priority. *) - cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * constant option) list; + cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option * Constant.t option) list; (** Whether we use matching or full unification during resolution *) cl_strict : bool; @@ -54,7 +53,7 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> Decl_kinds.polymorphic -> +val new_instance : typeclass -> Vernacexpr.hint_info_expr -> bool -> global_reference -> instance val add_instance : instance -> unit val remove_instance : instance -> unit @@ -68,7 +67,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) -val typeclass_univ_instance : typeclass puniverses -> typeclass +val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option @@ -83,11 +82,11 @@ val is_instance : global_reference -> bool (** Returns the term and type for the given instance of the parameters and fields of the type class. *) -val instance_constructor : typeclass puniverses -> constr list -> - constr option * types +val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list -> + EConstr.t option * EConstr.t (** Filter which evars to consider for resolution. *) -type evar_filter = existential_key -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t -> bool val all_evars : evar_filter val all_goals : evar_filter val no_goals : evar_filter diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1f35fa19aa..3cc1520179 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -23,11 +23,6 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration -let push_rec_types pfix env = - let (i, c, t) = pfix in - let inj c = EConstr.Unsafe.to_constr c in - push_rec_types (i, Array.map inj c, Array.map inj t) env - let meta_type evd mv = let ty = try Evd.meta_ftype evd mv @@ -39,7 +34,7 @@ let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in - EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp) + Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp let e_type_judgment env evdref j = match EConstr.kind !evdref (whd_all env !evdref j.uj_type) with @@ -54,6 +49,30 @@ let e_assumption_of_judgment env evdref j = with Type_errors.TypeError _ | PretypeError _ -> error_assumption env !evdref j +let e_judge_of_applied_inductive_knowing_parameters env evdref funj ind argjv = + let rec apply_rec n typ = function + | [] -> + { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = + let ar = inductive_type_knowing_parameters env !evdref ind argjv in + hnf_prod_appvect env !evdref (EConstr.of_constr ar) (Array.map j_val argjv) } + | hj::restjl -> + match EConstr.kind !evdref (whd_all env !evdref typ) with + | Prod (_,c1,c2) -> + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + else + error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv + | Evar ev -> + let (evd',t) = Evardefine.define_evar_as_product !evdref ev in + evdref := evd'; + let (_,_,c2) = destProd evd' t in + apply_rec (n+1) (subst1 hj.uj_val c2) restjl + | _ -> + error_cant_apply_not_functional env !evdref funj argjv + in + apply_rec 1 funj.uj_type (Array.to_list argjv) + let e_judge_of_apply env evdref funj argjv = let rec apply_rec n typ = function | [] -> @@ -160,7 +179,7 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in - let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in + let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then @@ -195,11 +214,11 @@ let check_cofix env sigma pcofix = let judge_of_prop = { uj_val = EConstr.mkProp; - uj_type = EConstr.mkSort type1_sort } + uj_type = EConstr.mkSort Sorts.type1 } let judge_of_set = { uj_val = EConstr.mkSet; - uj_type = EConstr.mkSort type1_sort } + uj_type = EConstr.mkSort Sorts.type1 } let judge_of_prop_contents = function | Null -> judge_of_prop @@ -305,16 +324,14 @@ let rec execute env evdref cstr = | App (f,args) -> let jl = execute_array env evdref args in - let j = - match EConstr.kind !evdref f with - | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - make_judge f - (inductive_type_knowing_parameters env !evdref (ind, u) jl) - | _ -> - (* No template polymorphism *) - execute env evdref f - in - e_judge_of_apply env evdref j jl + (match EConstr.kind !evdref f with + | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> + let fj = execute env evdref f in + e_judge_of_applied_inductive_knowing_parameters env evdref fj (ind, u) jl + | _ -> + (* No template polymorphism *) + let fj = execute env evdref f in + e_judge_of_apply env evdref fj jl) | Lambda (name,c1,c2) -> let j = execute env evdref c1 in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1e20788268..153a48a710 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Environ open EConstr open Evd @@ -26,7 +26,7 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types (** Typecheck a type and return its sort *) -val e_sort_of : env -> evar_map ref -> types -> sorts +val e_sort_of : env -> evar_map ref -> types -> Sorts.t (** Typecheck a term has a given type (assuming the type is OK) *) val e_check : env -> evar_map ref -> constr -> types -> unit @@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f090921e5c..e1720ec955 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,13 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -module CVars = Vars - open CErrors open Pp open Util open Names -open Term +open Constr open Termops open Environ open EConstr @@ -68,10 +66,10 @@ let _ = Goptions.declare_bool_option { let unsafe_occur_meta_or_existential c = let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Evar _ -> raise Occur | Meta _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> Constr.iter occrec c in try occrec c; false with Occur -> true @@ -79,7 +77,7 @@ let occur_meta_or_undefined_evar evd c = (** This is performance-critical. Using the evar-insensitive API changes the resulting heuristic. *) let c = EConstr.Unsafe.to_constr c in - let rec occrec c = match kind_of_term c with + let rec occrec c = match Constr.kind c with | Meta _ -> raise Occur | Evar (ev,args) -> (match evar_body (Evd.find evd ev) with @@ -194,6 +192,10 @@ let pose_all_metas_as_evars env evd t = let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in + let ty = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) + else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar env evdref ~src ty in evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref; @@ -501,6 +503,10 @@ let expand_key ts env sigma = function in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red | None -> None +let isApp_or_Proj sigma c = + match kind sigma c with + | App _ | Proj _ -> true + | _ -> false type unirec_flags = { at_top: bool; @@ -550,10 +556,10 @@ let oracle_order env cf1 cf2 = | Some k2 -> match k1, k2 with | IsProj (p, _), IsKey (ConstKey (p',_)) - when eq_constant (Projection.constant p) p' -> + when Constant.equal (Projection.constant p) p' -> Some (not (Projection.unfolded p)) | IsKey (ConstKey (p,_)), IsProj (p', _) - when eq_constant p (Projection.constant p') -> + when Constant.equal p (Projection.constant p') -> Some (Projection.unfolded p') | _ -> Some (Conv_oracle.oracle_order (fun x -> x) @@ -565,7 +571,9 @@ let is_rigid_head sigma flags t = | Ind (i,u) -> true | Construct _ -> true | Fix _ | CoFix _ -> true - | _ -> false + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _) + | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _) + | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = Universes.Constraints.fold @@ -605,7 +613,7 @@ let subst_defined_metas_evars sigma (bl,el) c = (** This seems to be performance-critical, and using the evar-insensitive primitives blow up the time passed in this function. *) let c = EConstr.Unsafe.to_constr c in - let rec substrec c = match kind_of_term c with + let rec substrec c = match Constr.kind c with | Meta i -> let select (j,_,_) = Int.equal i j in substrec (EConstr.Unsafe.to_constr (pi2 (List.find select bl))) @@ -646,14 +654,17 @@ let rec is_neutral env sigma ts t = | Evar _ | Meta _ -> true | Case (_, p, c, cl) -> is_neutral env sigma ts c | Proj (p, c) -> is_neutral env sigma ts c - | _ -> false + | Lambda _ | LetIn _ | Construct _ | CoFix _ -> false + | Sort _ | Cast (_, _, _) | Prod (_, _, _) | Ind _ -> false (* Really? *) + | Fix _ -> false (* This is an approximation *) + | App _ -> assert false let is_eta_constructor_app env sigma ts f l1 term = match EConstr.kind sigma f with | Construct (((_, i as ind), j), u) when i == 0 && j == 1 -> let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with - | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite && + | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite && Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (** Check that the other term is neutral *) is_neutral env sigma ts term @@ -780,7 +791,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (** Fast path for projections. *) - | Proj (p1,c1), Proj (p2,c2) when eq_constant + | Proj (p1,c1), Proj (p2,c2) when Constant.equal (Projection.constant p1) (Projection.constant p2) -> (try unify_same_proj curenvnb cv_pb {opt with at_top = true} substn c1 c2 @@ -1020,7 +1031,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = - if isApp sigma cM then + if isApp_or_Proj sigma cM then let f1l1 = whd_nored_state sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then let f2l2 = whd_nored_state sigma (cN,Stack.empty) in @@ -1036,7 +1047,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e error_cannot_unify (fst curenvnb) sigma (cM,cN) else try f1 () with e when precatchable_exception e -> - if isApp sigma cN then + if isApp_or_Proj sigma cN then let f2l2 = whd_nored_state sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then let f1l1 = whd_nored_state sigma (cM, Stack.empty) in @@ -1064,13 +1075,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e in try let opt' = {opt with with_types = false} in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in + let substn = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in 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 @@ -1266,7 +1277,7 @@ let w_coerce env evd mv c = let unify_to_type env sigma flags c status u = let sigma, c = refresh_universes (Some false) env sigma c in let t = get_type_of env sigma (nf_meta sigma c) in - let t = nf_betaiota sigma (nf_meta sigma t) in + let t = nf_betaiota env sigma (nf_meta sigma t) in unify_0 env sigma CUMUL flags t u let unify_type env sigma flags mv status c = @@ -1514,7 +1525,7 @@ let indirectly_dependent sigma c d decls = let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in let sigma, subst = nf_univ_variables sigma in - (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) + (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c)))) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1604,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) = | Some (sigma,_,l) -> let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in let univs, subst = nf_univ_variables sigma in - Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) + Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c)))) let make_eq_test env evd c = let out cstr = @@ -1616,11 +1627,11 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = let t = match ty with Some t -> t | None -> get_type_of env sigma c in let x = id_of_name_using_hdchar (Global.env()) sigma t name in - let ids = ids_of_named_context (named_context env) in + let ids = Environ.ids_of_named_context_val (named_context_val env) in if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context_val x (named_context_val env) then user_err ~hdr:"Unification.make_abstraction_core" - (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") + (str "The variable " ++ Id.print x ++ str " is already declared.") else x in @@ -1780,7 +1791,9 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = with ex when precatchable_exception ex -> matchrec c) - | _ -> user_err Pp.(str "Match_subterm"))) + | Cast (_, _, _) (* Is this expected? *) + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ + | Construct _ -> user_err Pp.(str "Match_subterm"))) in try matchrec cl with ex when precatchable_exception ex -> @@ -1846,7 +1859,11 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | Lambda (_,t,c) -> bind (matchrec t) (matchrec c) - | _ -> fail "Match_subterm")) + | Cast (_, _, _) -> fail "Match_subterm" (* Is this expected? *) + + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Const _ | Ind _ + | Construct _ -> fail "Match_subterm")) + in let res = matchrec cl [] in match res with @@ -1996,8 +2013,8 @@ let w_unify env evd cv_pb flags ty1 ty2 = let w_unify = if Flags.profile then - let wunifkey = Profile.declare_profile "w_unify" in - Profile.profile6 wunifkey w_unify + let wunifkey = CProfile.declare_profile "w_unify" in + CProfile.profile6 wunifkey w_unify else w_unify let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index fce17d5641..085e8c5b8b 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open EConstr open Environ open Evd diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml new file mode 100644 index 0000000000..89f1185a99 --- /dev/null +++ b/pretyping/univdecls.ml @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CErrors + +(** Local universes and constraints declarations *) +type universe_decl = + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let default_univ_decl = + let open Misctypes in + { univdecl_instance = []; + univdecl_extensible_instance = true; + univdecl_constraints = Univ.Constraint.empty; + univdecl_extensible_constraints = true } + +let interp_univ_constraints env evd cstrs = + let interp (evd,cstrs) (u, d, u') = + let ul = Pretyping.interp_known_glob_level evd u in + let u'l = Pretyping.interp_known_glob_level evd u' in + let cstr = (ul,d,u'l) in + let cstrs' = Univ.Constraint.add cstr cstrs in + try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in + evd, cstrs' + with Univ.UniverseInconsistency e -> + user_err ~hdr:"interp_constraint" + (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e) + in + List.fold_left interp (evd,Univ.Constraint.empty) cstrs + +let interp_univ_decl env decl = + let open Misctypes in + let pl : lident list = decl.univdecl_instance in + let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in + let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in + let decl = { univdecl_instance = pl; + univdecl_extensible_instance = decl.univdecl_extensible_instance; + univdecl_constraints = cstrs; + univdecl_extensible_constraints = decl.univdecl_extensible_constraints } + in evd, decl + +let interp_univ_decl_opt env l = + match l with + | None -> Evd.from_env env, default_univ_decl + | Some decl -> interp_univ_decl env decl diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli new file mode 100644 index 0000000000..706d3a157f --- /dev/null +++ b/pretyping/univdecls.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Local universe and constraint declarations. *) +type universe_decl = + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val default_univ_decl : universe_decl + +val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> + Evd.evar_map * universe_decl + +val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> + Evd.evar_map * universe_decl diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 66cc42cb61..c93b41786b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -10,10 +10,12 @@ open Util open Names open Declarations open Term +open Constr open Vars open Environ open Inductive open Reduction +open Vmvalues open Vm open Context.Rel.Declaration @@ -51,7 +53,7 @@ let invert_tag cst tag reloc_tbl = let find_rectype_a env c = let (t, l) = decompose_appvect (whd_all env c) in - match kind_of_term t with + match kind t with | Ind ind -> (ind, l) | _ -> assert false @@ -133,7 +135,7 @@ let build_case_type dep p realargs c = (* La fonction de normalisation *) -let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t +let rec nf_val env sigma v t = nf_whd env sigma (Vmvalues.whd_val v) t and nf_vtype env sigma v = nf_val env sigma v crazy_type @@ -143,7 +145,7 @@ and nf_whd env sigma whd typ = | Vprod p -> let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in - let vc = body_of_vfun (nb_rel env) (codom p) in + let vc = reduce_fun (nb_rel env) (codom p) in let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in mkProd(name,dom,codom) | Vfun f -> nf_fun env sigma f typ @@ -190,7 +192,7 @@ and nf_univ_args ~nb_univs mk env sigma stk = else match stk with | Zapp args :: _ -> let inst = - Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i)) + Array.init nb_univs (fun i -> uni_lvl_val (arg args i)) in Univ.Instance.of_array inst | _ -> assert false @@ -238,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) @@ -253,7 +256,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in - let ci = case_info sw in + let ci = sw.sw_annot.Cbytecodes.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; @@ -262,17 +265,17 @@ and nf_stk ?from:(from=0) env sigma c t stk = nf_stk env sigma (mkProj(p',c)) ty stk and nf_predicate env sigma ind mip params v pT = - match whd_val v, kind_of_term pT with + match whd_val v, kind pT with | Vfun f, Prod _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = decompose_prod env pT in let dep,body = nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in dep, mkLambda(name,dom,body) | Vfun f, _ -> let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in @@ -306,7 +309,7 @@ and nf_bargs env sigma b ofs t = and nf_fun env sigma f typ = let k = nb_rel env in - let vb = body_of_vfun k f in + let vb = reduce_fun k f in let name,dom,codom = try decompose_prod env typ with DestKO -> @@ -364,4 +367,4 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) ~catch_incon:true ~pb env sigma t1 t2 -let _ = Reductionops.set_vm_infer_conv vm_infer_conv +let _ = if Coq_config.bytecode_compiler then Reductionops.set_vm_infer_conv vm_infer_conv |