diff options
| author | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-15 14:19:51 +0100 |
| commit | ed275fd5eb8b11003f8904010d853d2bd568db79 (patch) | |
| tree | e27b7778175cb0d9d19bd8bde9c593b335a85125 /pretyping | |
| parent | a44c4a34202fa6834520fcd6842cc98eecf044ec (diff) | |
| parent | 1ba29c062e30181bda9d931dffe48e457dfee9d6 (diff) | |
Merge PR #8817: SProp: the definitionally proof irrelevant universe
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
Diffstat (limited to 'pretyping')
35 files changed, 625 insertions, 438 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 08df9a2460..3b3de33d8e 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -13,6 +13,7 @@ open Names open Globnames open Term open Constr +open Context open Environ open Util open Libobject @@ -72,7 +73,7 @@ let arguments_names r = GlobRef.Map.find r !name_table let rename_type ty ref = let name_override old_name override = match override with - | Name _ as x -> x + | Name _ as x -> {old_name with binder_name=x} | Anonymous -> old_name in let rec rename_type_aux c = function | [] -> c diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 069ba9572a..e22368d5e5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -16,6 +16,7 @@ open Util open Names open Nameops open Constr +open Context open Termops open Environ open EConstr @@ -472,7 +473,8 @@ let push_current_pattern ~program_mode sigma (cur,ty) eqn = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in match eqn.patterns with | pat::pats -> - let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in + let r = Sorts.Relevant in (* TODO relevance *) + let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } @@ -762,7 +764,10 @@ let get_names avoid env sigma sign eqns = (fun (l,avoid) d na -> let na = merge_name - (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) + (fun decl -> + let na = get_name decl in + let t = get_type decl in + Name (next_name_away (named_hd env sigma t na) avoid)) d na in (na::l,Id.Set.add (Name.get_id na) avoid)) @@ -782,10 +787,10 @@ let recover_and_adjust_alias_names (_,avoid) names sign = let rec aux = function | [],[] -> [] - | x::names, LocalAssum (_,t)::sign -> - (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign) + | x::names, LocalAssum (x',t)::sign -> + (x, LocalAssum ({x' with binder_name=alias_of_pat x},t)) :: aux (names,sign) | names, (LocalDef (na,_,_) as decl)::sign -> - (DAst.make @@ PatVar na, decl) :: aux (names,sign) + (DAst.make @@ PatVar na.binder_name, decl) :: aux (names,sign) | _ -> assert false in List.split (aux (names,sign)) @@ -1247,7 +1252,7 @@ let rec generalize_problem names sigma pb = function let pb',deps = generalize_problem names sigma pb l in let d = map_constr (lift i) (lookup_rel i !!(pb.env)) in begin match d with - | LocalDef (Anonymous,_,_) -> pb', deps + | LocalDef ({binder_name=Anonymous},_,_) -> pb', deps | _ -> (* for better rendering *) let d = RelDecl.map_type (fun c -> whd_betaiota sigma c) d in @@ -1436,16 +1441,15 @@ let compile ~program_mode sigma pb = brvals pb.tomatch pb.pred deps cstrs in let brvals = Array.map (fun (sign,body) -> it_mkLambda_or_LetIn body sign) brvals in - let (pred,typ) = + let (pred,typ) = find_predicate pb.caseloc pb.env sigma - pred current indt (names,dep) tomatch in - let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in + pred current indt (names,dep) tomatch + in + let rci = Typing.check_allowed_sort !!(pb.env) sigma mind current pred in + let ci = make_case_info !!(pb.env) (fst mind) rci pb.casestyle in let pred = nf_betaiota !!(pb.env) sigma pred in - let case = - make_case_or_project !!(pb.env) sigma indf ci pred current brvals - in + let case = make_case_or_project !!(pb.env) sigma indf ci pred current brvals in let sigma, _ = Typing.type_of !!(pb.env) sigma pred in - Typing.check_allowed_sort !!(pb.env) sigma mind current pred; sigma, { uj_val = applist (case, inst); uj_type = prod_applist sigma typ inst } @@ -1460,7 +1464,7 @@ let compile ~program_mode sigma pb = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let pb = { pb with - env = snd (push_rel ~hypnaming sigma (LocalDef (na,current,ty)) env); + env = snd (push_rel ~hypnaming sigma (LocalDef (annotR na,current,ty)) env); tomatch = tomatch; pred = lift_predicate 1 pred tomatch; history = pop_history pb.history; @@ -1511,7 +1515,8 @@ let compile ~program_mode sigma pb = and compile_alias initial sigma pb (na,orig,(expanded,expanded_typ)) rest = let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let f c t = - let alias = LocalDef (na,c,t) in + let r = Retyping.relevance_of_type !!(pb.env) sigma t in + let alias = LocalDef (make_annot na r,c,t) in let pb = { pb with env = snd (push_rel ~hypnaming sigma alias pb.env); @@ -1524,7 +1529,7 @@ let compile ~program_mode sigma pb = if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then subst1 c j.uj_val else - mkLetIn (na,c,t,j.uj_val); + mkLetIn (make_annot na r,c,t,j.uj_val); uj_type = subst1 c j.uj_type } in (* spiwack: when an alias appears on a deep branch, its non-expanded form is automatically a variable of the same name. We avoid @@ -1812,7 +1817,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in - let d = LocalAssum (alias_of_pat pat,typ) in + let d = LocalAssum (annotR (alias_of_pat pat),typ) in let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming:KeepUserNameAndRenameExistingButSectionNames sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in let avoid0 = GlobEnv.vars_of_env env in @@ -1913,9 +1918,11 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> let sign = match bo with - | None -> [LocalAssum (na, lift n typ)] - | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign + | None -> + let r = Sorts.Relevant in (* TODO relevance *) + let sign = match bo with + | None -> [LocalAssum (make_annot na r, lift n typ)] + | Some b -> [LocalDef (make_annot na r, lift n b, lift n typ)] in sign | Some {CAst.loc} -> user_err ?loc (str"Unexpected type annotation for a term of non inductive type.")) @@ -1923,7 +1930,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in - let arsign = fst (get_arity env0 indf') in + let arsign, inds = get_arity env0 indf' in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = match t with @@ -1935,8 +1942,9 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = List.rev realnal | None -> List.make nrealargs_ctxt Anonymous in + let r = Sorts.relevance_of_sort_family inds in let t = EConstr.of_constr (build_dependent_inductive env0 indf') in - LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in + LocalAssum (make_annot na r, t) :: List.map2 RelDecl.set_name realnal arsign in let rec buildrec n = function | [],[] -> [] | (_,tm)::ltm, (_,x)::tmsign -> @@ -2143,9 +2151,10 @@ let constr_of_pat env sigma arsign pat avoid = | Anonymous -> let previd, id = prime avoid (Name (Id.of_string "wildcard")) in Name id, Id.Set.add id avoid - in - (sigma, (DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty, - (List.map (fun x -> mkRel 1) realargs), 1, avoid) + in + let r = Sorts.Relevant in (* TODO relevance *) + (sigma, (DAst.make ?loc @@ PatVar name), [LocalAssum (make_annot name r, 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 let IndType (indf, _) = @@ -2184,9 +2193,11 @@ let constr_of_pat env sigma arsign pat avoid = match alias with Anonymous -> sigma, pat', sign, app, apptype, realargs, n, avoid - | Name id -> - let sign = LocalAssum (alias, lift m ty) :: sign in - let avoid = Id.Set.add id avoid in + | Name id -> + let _, inds = get_arity env indf in + let r = Sorts.relevance_of_sort_family inds in + let sign = LocalAssum (make_annot alias r, lift m ty) :: sign in + let avoid = Id.Set.add id avoid in let sigma, sign, i, avoid = try let env = EConstr.push_rel_context sign env in @@ -2196,11 +2207,12 @@ let constr_of_pat env sigma arsign pat avoid = (mkRel 1) (* alias *) (lift 1 app) (* aliased term *) in - let neq = eq_id avoid id in - sigma, LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid + let neq = eq_id avoid id in + (* if we ever allow using a SProp-typed coq_eq_ind this relevance will be wrong *) + sigma, LocalDef (nameR neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid with Evarconv.UnableToUnify _ -> sigma, sign, 1, avoid in - (* Mark the equality as a hole *) + (* Mark the equality as a hole *) sigma, pat', sign, lift i app, lift i apptype, realargs, n + i, avoid in let sigma, pat', sign, patc, patty, args, z, avoid = typ env sigma (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in @@ -2222,18 +2234,18 @@ match EConstr.kind sigma t with let rels_of_patsign sigma = List.map (fun decl -> match decl with - | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) + | LocalDef (na,t',t) when is_topvar sigma t' -> LocalAssum (na,t) | _ -> decl) let vars_of_ctx sigma ctx = let _, y = List.fold_right (fun decl (prev, vars) -> match decl with - | LocalDef (na,t',t) when is_topvar sigma t' -> + | LocalDef (na,t',t) when is_topvar sigma t' -> prev, (DAst.make @@ GApp ( (DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), - [hole na; DAst.make @@ GVar prev])) :: vars + [hole na.binder_name; DAst.make @@ GVar prev])) :: vars | _ -> match RelDecl.get_name decl with Anonymous -> invalid_arg "vars_of_ctx" @@ -2343,12 +2355,13 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = let args = List.rev args in substl args (liftn signlen (succ nargs) arity) in - let rhs_rels', tycon = + let r = Sorts.Relevant in (* TODO relevance *) + let rhs_rels', tycon = let neqs_rels, arity = match ineqs with | None -> [], arity | Some ineqs -> - [LocalAssum (Anonymous, ineqs)], lift 1 arity + [LocalAssum (make_annot Anonymous r, ineqs)], lift 1 arity in let eqs_rels, arity = decompose_prod_n_assum sigma neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity @@ -2359,7 +2372,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let sigma, _btype = Typing.type_of !!env sigma bbody in 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_decl = LocalDef (make_annot (Name branch_name) r, lift !i bbody, lift !i btype) in let branch = let bref = DAst.make @@ GVar branch_name in match vars_of_ctx sigma rhs_rels with @@ -2407,9 +2420,10 @@ let abstract_tomatch env sigma tomatchs tycon = | _ -> let tycon = Option.map (fun t -> subst_term sigma (lift 1 c) (lift 1 t)) tycon in - let name = next_ident_away (Id.of_string "filtered_var") names in + let name = next_ident_away (Id.of_string "filtered_var") names in + let r = Sorts.Relevant in (* TODO relevance *) (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, + LocalDef (make_annot (Name name) r, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, Id.Set.add name names, tycon) ([], [], Id.Set.empty, tycon) tomatchs in List.rev prev, ctx, tycon @@ -2471,8 +2485,8 @@ let build_dependent_signature env sigma avoid tomatchs arsign = make_prime avoid name in (sigma, env, succ nargeqs, - (LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs, - refl_arg :: refl_args, + (LocalAssum (make_annot (Name (eq_id avoid previd)) Sorts.Relevant, eq)) :: argeqs, + refl_arg :: refl_args, pred slift, RelDecl.set_name (Name id) decl :: argsign')) (sigma, env, neqs, [], [], slift, []) args argsign @@ -2486,8 +2500,8 @@ let build_dependent_signature env sigma avoid tomatchs arsign = in let sigma, refl_eq = mk_JMeq_refl sigma ty tm in let previd, id = make_prime avoid appn in - (sigma, (LocalAssum (Name (eq_id avoid previd), eq) :: argeqs) :: eqs, - succ nargeqs, + (sigma, (LocalAssum (make_annot (Name (eq_id avoid previd)) Sorts.Relevant, eq) :: argeqs) :: eqs, + succ nargeqs, refl_eq :: refl_args, pred slift, ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns)) @@ -2503,8 +2517,9 @@ let build_dependent_signature env sigma avoid tomatchs arsign = (mkRel slift) (lift nar tm) in let sigma, refl = mk_eq_refl sigma tomatch_ty tm in + let na = make_annot (Name (eq_id avoid previd)) Sorts.Relevant in (sigma, - [LocalAssum (Name (eq_id avoid previd), eq)] :: eqs, succ neqs, + [LocalAssum (na, eq)] :: eqs, succ neqs, refl :: refl_args, pred slift, (arsign' :: []) :: arsigns)) (sigma, [], 0, [], nar, []) tomatchs arsign @@ -2580,11 +2595,12 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env (* We push the initial terms to match and push their alias to rhs' envs *) (* names of aliases will be recovered from patterns (hence Anonymous here) *) - let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) - | NotInd (Some b, t) -> LocalDef (na,b,t) - | IsInd (typ,_,_) -> LocalAssum (na,typ) in + (* TODO relevance *) + let out_tmt na = function NotInd (None,t) -> LocalAssum (make_annot na Sorts.Relevant,t) + | NotInd (Some b, t) -> LocalDef (make_annot na Sorts.Relevant,b,t) + | IsInd (typ,_,_) -> LocalAssum (make_annot na Sorts.Relevant,typ) in let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in - + let typs = List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in @@ -2654,10 +2670,11 @@ let compile_cases ?loc ~program_mode style (typing_fun, sigma) tycon env (predop (* names of aliases will be recovered from patterns (hence Anonymous *) (* here) *) + (* TODO relevance *) let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t) | NotInd (Some b,t) -> LocalDef (na,b,t) | IsInd (typ,_,_) -> LocalAssum (na,typ) in - let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in + let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt (make_annot na Sorts.Relevant) tmt)) nal tomatchs in let typs = List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index e27fc536eb..c9f18d89be 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -48,7 +48,7 @@ type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack | CBN of constr * cbv_value subs - | LAM of int * (Name.t * constr) list * constr * cbv_value subs + | LAM of int * (Name.t Context.binder_annot * 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 Univ.puniverses * cbv_value array @@ -281,11 +281,11 @@ and reify_value = function (* reduction under binders *) apply_env env @@ List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) b ctxt - | FIXP ((lij,(names,lty,bds)),env,args) -> - let fix = mkFix (lij, (names, lty, bds)) in + | FIXP ((lij,fix),env,args) -> + let fix = mkFix (lij, fix) in mkApp (apply_env env fix, Array.map reify_value args) - | COFIXP ((j,(names,lty,bds)),env,args) -> - let cofix = mkCoFix (j, (names,lty,bds)) in + | COFIXP ((j,cofix),env,args) -> + let cofix = mkCoFix (j, cofix) in mkApp (apply_env env cofix, Array.map reify_value args) | CONSTR (c,args) -> mkApp(mkConstructU c, Array.map reify_value args) @@ -550,7 +550,7 @@ and cbv_norm_value info = function (* reduction under binders *) | FIXP ((lij,(names,lty,bds)),env,args) -> mkApp (mkFix (lij, - (names, + (names, Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds)), @@ -558,7 +558,7 @@ and cbv_norm_value info = function (* reduction under binders *) | COFIXP ((j,(names,lty,bds)),env,args) -> mkApp (mkCoFix (j, - (names,Array.map (cbv_norm_term info env) lty, + (names,Array.map (cbv_norm_term info env) lty, Array.map (cbv_norm_term info (subs_liftn (Array.length lty) env)) bds)), Array.map (cbv_norm_value info) args) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 0a1e771921..d6c2ad146e 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -32,7 +32,7 @@ type cbv_value = | VAL of int * constr | STACK of int * cbv_value * cbv_stack | CBN of constr * cbv_value subs - | LAM of int * (Name.t * constr) list * constr * cbv_value subs + | LAM of int * (Name.t Context.binder_annot * 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 Univ.puniverses * cbv_value array diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 306a76e35e..54a1aa9aa0 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -179,7 +179,7 @@ let find_class_type sigma t = | Proj (p, c) when not (Projection.unfolded p) -> CL_PROJ (Projection.repr p), EInstance.empty, (c :: args) | Ind (ind_sp,u) -> CL_IND ind_sp, u, args - | Prod (_,_,_) -> CL_FUN, EInstance.empty, [] + | Prod _ -> CL_FUN, EInstance.empty, [] | Sort _ -> CL_SORT, EInstance.empty, [] | _ -> raise Not_found diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 0e6aaaa408..82411ba2ef 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -21,6 +21,7 @@ open Util open Names open Term open Constr +open Context open Environ open EConstr open Vars @@ -175,23 +176,23 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) try evdref := unify_leq_delay env !evdref hdx hdy; let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in - aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co + aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co with UnableToUnify _ -> - let (n, eqT), restT = dest_prod typ in + let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in let () = try evdref := unify_leq_delay env !evdref eqT eqT' with UnableToUnify _ -> raise NoSubtacCoercion - in + in (* Disallow equalities on arities *) if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion; let restargs = lift_args 1 (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i))))) in let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in - let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in + let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in - let evar = make_existential ?loc n env evdref eq in + let evar = make_existential ?loc n.binder_name env evdref eq in let eq_app x = papp evdref coq_eq_rect [| eqT; hdx; pred; x; hdy; evar|] in @@ -216,9 +217,12 @@ 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.vars_of_env env)) - in - let env' = push_rel (LocalAssum (name', a')) env in + {name' with + binder_name = + 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 (* env, x : a' |- c1 : lift 1 a' > lift 1 a *) let coec1 = app_opt env' evdref c1 (mkRel 1) in @@ -230,7 +234,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) | _, _ -> Some (fun f -> - mkLambda (name', a', + mkLambda (name', a', app_opt env' evdref c2 (mkApp (lift 1 f, [| coec1 |]))))) @@ -253,11 +257,11 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let c1 = coerce_unify env a a' in let remove_head a c = match EConstr.kind !evdref c with - | Lambda (n, t, t') -> c, t' + | Lambda (n, t, t') -> c, t' | Evar (k, args) -> let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in evdref := evs; - let (n, dom, rng) = destLambda !evdref t in + let (n, dom, rng) = destLambda !evdref t in if isEvar !evdref dom then let (domk, args) = destEvar !evdref dom in evdref := define domk a !evdref; @@ -265,8 +269,12 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) t, rng | _ -> raise NoSubtacCoercion in - let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in - let env' = push_rel (LocalAssum (Name Namegen.default_dependent_ident, a)) env in + let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in + let ra = Retyping.relevance_of_type env !evdref a in + let env' = push_rel + (LocalAssum (make_annot (Name Namegen.default_dependent_ident) ra, a)) + env + in let c2 = coerce_unify env' b b' in match c1, c2 with | None, None -> None @@ -396,9 +404,9 @@ let apply_coercion env sigma p hj typ_cl = let inh_app_fun_core ~program_mode env evd j = let t = whd_all env evd j.uj_type in match EConstr.kind evd t with - | Prod (_,_,_) -> (evd,j) + | Prod _ -> (evd,j) | Evar ev -> - let (evd',t) = Evardefine.define_evar_as_product evd ev in + let (evd',t) = Evardefine.define_evar_as_product env evd ev in (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> try let t,p = @@ -505,11 +513,11 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid (* has type forall (x:u1), u2 (with v' recursively obtained) *) (* Note: we retype the term because template polymorphism may have *) (* weakened its type *) - let name = match name with + let name = map_annot (function | Anonymous -> Name Namegen.default_dependent_ident - | _ -> name in + | na -> na) name in let open Context.Rel.Declaration in - let env1 = push_rel (LocalAssum (name,u1)) env in + let env1 = push_rel (LocalAssum (name,u1)) env in let (evd', v1) = inh_conv_coerce_to_fail ?loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in @@ -519,7 +527,7 @@ let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigid | None -> subst_term evd' v1 t2 | Some v2 -> Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail ?loc env1 evd' rigidonly v2 t2 u2 in - (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 94257fedd7..bc083ed9d9 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -14,6 +14,7 @@ open CErrors open Util open Names open Constr +open Context open Globnames open Termops open Term @@ -70,7 +71,7 @@ let constrain sigma n (ids, m) ((names,seen as names_seen), terms as subst) = (names_seen, Id.Map.add n (ids, m) terms) let add_binders na1 na2 binding_vars ((names,seen), terms as subst) = - match na1, na2 with + match na1, na2.binder_name with | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> if Id.Map.mem id1 names then let () = Glob_ops.warn_variable_collision id1 in @@ -94,7 +95,7 @@ let rec build_lambda sigma vars ctx m = match vars with let (na, t, suf) = match suf with | [] -> assert false | (_, id, t) :: suf -> - (Name id, t, suf) + (map_annot Name.mk_name id, t, suf) in (* Check that the abstraction is legal by generating a transitive closure of its dependencies. *) @@ -178,11 +179,12 @@ let make_renaming ids = function | _ -> 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 + let id2 = map_annot (function + | Name id2 -> id2 + | Anonymous -> + let avoid = Id.Set.of_list (List.map (fun (_,id,_) -> id.binder_name) ctx) in + Namegen.next_ident_away Namegen.default_non_dependent_ident avoid) na2 + in (na1, id2, t) :: ctx (* This is an optimization of the main pattern-matching which shares @@ -341,19 +343,19 @@ let matches_core env sigma allow_bound_rels sorec ctx env subst c1 c2 | PProd (na1,c1,d1), Prod(na2,c2,d2) -> - sorec (push_binder 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 (push_binder 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 (push_binder 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 (push_binder 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'|]) -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 99cd89cc2a..ac7c3d30d5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Constr +open Context open Term open EConstr open Vars @@ -40,9 +41,12 @@ let print_evar_arguments = ref false let add_name na b t (nenv, env) = let open Context.Rel.Declaration in + (* Is this just a dummy? Be careful, printing doesn't always give us + a correct env. *) + let r = Sorts.Relevant in add_name na nenv, push_rel (match b with - | None -> LocalAssum (na,t) - | Some b -> LocalDef (na,b,t) + | None -> LocalAssum (make_annot na r,t) + | Some b -> LocalDef (make_annot na r,b,t) ) env @@ -202,11 +206,11 @@ let computable sigma p k = let lookup_name_as_displayed env sigma t s = let rec lookup avoid n c = match EConstr.kind sigma c with | Prod (name,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with + (match compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> - (match compute_displayed_name_in sigma RenamingForGoal avoid name c' with + (match compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c @@ -216,7 +220,7 @@ let lookup_name_as_displayed env sigma t s = 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 Id.Set.empty name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -226,7 +230,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 Id.Set.empty name c' with + (match compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> if Int.equal n 0 then @@ -342,9 +346,9 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = | b::tags -> let na,c,f,body,t = match EConstr.kind sigma (strip_outer_cast sigma c), b with - | Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t - | LetIn (na,b,t,c),true -> - na,c,compute_displayed_name_in,Some b,Some t + | Lambda (na,t,c),false -> na.binder_name,c,compute_displayed_let_name_in,None,Some t + | LetIn (na,b,t,c),true -> + na.binder_name,c,compute_displayed_name_in,Some b,Some t | _, false -> Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), compute_displayed_name_in,None,None @@ -490,19 +494,16 @@ let rec share_names detype 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') -> - let na = match (na,na') with - Name _, _ -> na - | _, Name _ -> na' - | _ -> na in + let na = Nameops.Name.pick_annot na na' in let t' = detype avoid env sigma t in - let id = next_name_away na avoid in + let id = next_name_away na.binder_name avoid in let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in share_names detype (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 avoid env sigma t' in let b' = detype avoid env sigma b in - let id = next_name_away na avoid in + let id = next_name_away na.binder_name avoid in let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in share_names detype 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 *) @@ -511,7 +512,7 @@ let rec share_names detype n l avoid env sigma c t = (* If it is an open proof: we cheat and eta-expand *) | _, Prod (na',t',c') when n > 0 -> let t'' = detype avoid env sigma t' in - let id = next_name_away na' avoid in + let id = next_name_away na'.binder_name avoid 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 detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c' @@ -549,7 +550,7 @@ let detype_fix detype 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 + let id = next_name_away na.binder_name avoid in (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 @@ -565,7 +566,7 @@ let detype_cofix detype 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 + let id = next_name_away na.binder_name avoid in (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 @@ -597,6 +598,7 @@ let detype_universe sigma u = Univ.Universe.map fn u let detype_sort sigma = function + | SProp -> GSProp | Prop -> GProp | Set -> GSet | Type u -> @@ -702,9 +704,9 @@ and detype_r d flags avoid env sigma t = match decl with | LocalDef _ -> true | LocalAssum (id,_) -> - try let n = List.index Name.equal (Name id) (fst env) in + try let n = List.index Name.equal (Name id.binder_name) (fst env) in isRelN sigma n c - with Not_found -> isVarId sigma id c + with Not_found -> isVarId sigma id.binder_name c in let id,l = try @@ -765,11 +767,11 @@ and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs br [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 + let pat,new_avoid,new_env,new_ids = make_pat x.binder_name avoid env b None t ids in buildrec new_ids (pat::patlist) new_avoid new_env l b | LetIn (x,b,t,b'), true::l -> - let pat,new_avoid,new_env,new_ids = make_pat x avoid env b' (Some b) t ids in + let pat,new_avoid,new_env,new_ids = make_pat x.binder_name avoid env b' (Some b) t ids in buildrec new_ids (pat::patlist) new_avoid new_env l b' | Cast (c,_,_), l -> (* Oui, il y a parfois des cast *) @@ -791,7 +793,7 @@ and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs br in buildrec Id.Set.empty [] avoid env construct_nargs branch -and detype_binder d (lax,isgoal as flags) bk avoid env sigma na body ty c = +and detype_binder d (lax,isgoal as flags) bk avoid env sigma {binder_name=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 @@ -827,7 +829,7 @@ let detype_rel_context d ?(lax=false) where avoid env sigma sign = (RenamingElsewhereFor (fst env,c)) avoid na c in let b = match decl with | LocalAssum _ -> None - | LocalDef (_,b,_) -> Some b + | LocalDef (_,b,_) -> Some b 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 @@ -864,7 +866,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = (* spiwack: I'm not sure it is the right thing to do, but I'm computing the detyping environment like [Printer.pr_constr_under_binders_env] does. *) - let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in + let assums = List.map (fun id -> LocalAssum (make_annot (Name id) Sorts.Relevant,(* dummy *) mkProp)) b in let env = push_rel_context assums env in DAst.get (detype Now ?lax isgoal avoid env sigma c) (* if [id] is bound to a [closed_glob_constr]. *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8e273fb4a8..28a97bb91a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -15,6 +15,7 @@ open Constr open Termops open Environ open EConstr +open Context open Vars open Reduction open Reductionops @@ -78,8 +79,8 @@ let impossible_default_case env = let coq_unit_judge = let open Environ in let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in - let na1 = Name (Id.of_string "A") in - let na2 = Name (Id.of_string "H") in + let na1 = make_annot (Name (Id.of_string "A")) Sorts.Relevant in + let na2 = make_annot (Name (Id.of_string "H")) Sorts.Relevant in fun env -> match impossible_default_case env with | Some (id, type_of_id, ctx) -> @@ -87,7 +88,7 @@ let coq_unit_judge = | None -> (* In case the constants id/ID are not defined *) Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), + (mkProd (na1,mkProp,mkArrow (mkRel 1) Sorts.Relevant (mkRel 2))), Univ.ContextSet.empty let unfold_projection env evd ts p c = @@ -251,8 +252,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let canon_s,sk2_effective = try match EConstr.kind sigma t2 with - Prod (_,a,b) -> (* assert (l2=[]); *) - let _, a, b = destProd sigma t2 in + Prod (_,a,b) -> (* assert (l2=[]); *) + let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) @@ -815,10 +816,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.Name.pick na1 na2 in + let na = Nameops.Name.pick_annot na1 na2 in evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] - and f2 i = + and f2 i = let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1) and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2) in evar_eqappr_x flags env i pbty out1 out2 @@ -930,7 +931,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty [(fun i -> evar_conv_x flags env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.Name.pick na1 na2 in + let na = Nameops.Name.pick_annot na1 na2 in evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2); (* When in modulo_betaiota = false case, lambda's are not reduced *) (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] @@ -988,12 +989,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty UnifFailure (evd,UnifUnivInconsistency p) | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) - | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> + | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd [(fun i -> evar_conv_x flags env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.Name.pick n1 n2 in + let na = Nameops.Name.pick_annot n1 n2 in evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> @@ -1027,7 +1028,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | _, Construct u -> eta_constructor flags env evd sk2 u sk1 term1 - | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) + | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and evd [ (fun i -> ise_array2 i (fun i' -> evar_conv_x flags env i' CONV) tys1 tys2); @@ -1035,7 +1036,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] else UnifFailure (evd, NotSameHead) - | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> + | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> if Int.equal i1 i2 then ise_and evd [(fun i -> ise_array2 i @@ -1352,7 +1353,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = make_subst (ctxt',l,occsl) end | decl'::ctxt', c::l, occs::occsl -> - let id = NamedDecl.get_id decl' in + let id = NamedDecl.get_annot decl' in let t = NamedDecl.get_type decl' in let evs = ref [] in let c = nf_evar evd c in @@ -1369,7 +1370,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let c = nf_evar evd c in if !debug_ho_unification then Feedback.msg_debug Pp.(str"set holes for: " ++ - prc env_rhs evd (mkVar id) ++ spc () ++ + prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ prc env_rhs evd c ++ str" in " ++ prc env_rhs evd rhs); let occ = ref 1 in @@ -1381,7 +1382,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = incr occ; match occs with | AtOccurrences occs -> - if Locusops.is_selected oc occs then evd, mkVar id + if Locusops.is_selected oc occs then evd, mkVar id.binder_name else evd, inst | Unspecified prefer_abstraction -> let evd, evty = set_holes env_rhs evd cty subst in @@ -1436,6 +1437,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let rec abstract_free_holes evd = function | (id,idty,c,cty,evsref,_,_)::l -> + let id = id.binder_name in let c = nf_evar evd c in if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracting: " ++ diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index a62427834d..a51cb22c20 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -13,6 +13,7 @@ open Util open Pp open Names open Constr +open Context open Termops open EConstr open Vars @@ -72,7 +73,7 @@ let idx = Namegen.default_dependent_ident (* Refining an evar to a product *) -let define_pure_evar_as_product evd evk = +let define_pure_evar_as_product env evd evk = let open Context.Named.Declaration in let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in @@ -84,11 +85,12 @@ let define_pure_evar_as_product evd evk = let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~src ~filter:(evar_filter evi) in + let rdom = Sorts.Relevant in (* TODO relevance *) let evd2,rng = - let newenv = push_named (LocalAssum (id, dom)) evenv in + let newenv = push_named (LocalAssum (make_annot id rdom, dom)) evenv in let src = subterm_source evk ~where:Codomain evksrc in let filter = Filter.extend 1 (evar_filter evi) in - if Sorts.is_prop (ESorts.kind evd1 s) then + if Environ.is_impredicative_sort env (ESorts.kind evd1 s) then (* Impredicative product, conclusion must fall in [Prop]. *) new_evar newenv evd1 concl ~src ~filter else @@ -97,17 +99,17 @@ let define_pure_evar_as_product evd evk = new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) (ESorts.kind evd1 s) in + let evd3 = Evd.set_leq_sort evenv evd3 (Sorts.sort_of_univ prods) (ESorts.kind evd1 s) in evd3, rng in - let prod = mkProd (Name id, dom, subst_var id rng) in + let prod = mkProd (make_annot (Name id) rdom, dom, subst_var id rng) in let evd3 = Evd.define evk prod evd2 in evd3,prod (* Refine an applied evar to a product and returns its instantiation *) -let define_evar_as_product evd (evk,args) = - let evd,prod = define_pure_evar_as_product evd evk in +let define_evar_as_product env evd (evk,args) = + let evd,prod = define_pure_evar_as_product env evd evk in (* Quick way to compute the instantiation of evk with args *) let na,dom,rng = destProd evd prod in let evdom = mkEvar (fst (destEvar evd dom), args) in @@ -131,17 +133,19 @@ let define_pure_evar_as_lambda env evd evk = let typ = Reductionops.whd_all evenv evd (evar_concl evi) in let evd1,(na,dom,rng) = match EConstr.kind evd typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) - | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ + | Evar ev' -> let evd,typ = define_evar_as_product env evd ev' in evd,destProd evd typ | _ -> error_not_product env evd typ 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 + map_annot (fun na -> next_name_away_with_default_using_types "x" na avoid + (Reductionops.whd_evar evd dom)) na + in let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = subterm_source evk ~where:Body (evar_source evk evd1) in let abstract_arguments = Abstraction.abstract_last evi.evar_abstract_arguments in - let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter ~abstract_arguments in - let lam = mkLambda (Name id, dom, subst_var id body) in + let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id.binder_name) rng) ~filter ~abstract_arguments in + let lam = mkLambda (map_annot Name.mk_name id, dom, subst_var id.binder_name body) in Evd.define evk lam evd2, lam let define_evar_as_lambda env evd (evk,args) = @@ -164,13 +168,12 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function (* Refining an evar to a sort *) let define_evar_as_sort env evd (ev,args) = - let evd, u = new_univ_variable univ_rigid evd in + let evd, s = new_sort_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in - let s = Type u in let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in let sort = destSort evd concl in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s + Evd.set_leq_sort env evd' (Sorts.super s) (ESorts.kind evd' sort), s (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type @@ -181,21 +184,22 @@ let split_tycon ?loc env evd tycon = let rec real_split evd c = let t = Reductionops.whd_all env evd c in match EConstr.kind evd t with - | Prod (na,dom,rng) -> evd, (na, dom, rng) + | Prod (na,dom,rng) -> evd, (na, dom, rng) | Evar ev (* ev is undefined because of whd_all *) -> - let (evd',prod) = define_evar_as_product evd ev in - let (_,dom,rng) = destProd evd prod in - evd',(Anonymous, dom, rng) - | App (c,args) when isEvar evd c -> - let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in + let (evd',prod) = define_evar_as_product env evd ev in + let (na,dom,rng) = destProd evd prod in + let anon = {na with binder_name = Anonymous} in + evd',(anon, dom, rng) + | App (c,args) when isEvar evd c -> + let (evd',lam) = define_evar_as_lambda env evd (destEvar evd c) in real_split evd' (mkApp (lam,args)) | _ -> error_not_product ?loc env evd c in match tycon with - | None -> evd,(Anonymous,None,None) + | None -> evd,(make_annot Anonymous Relevant,None,None) | Some c -> - let evd', (n, dom, rng) = real_split evd c in - evd', (n, mk_tycon dom, mk_tycon rng) + let evd', (n, dom, rng) = real_split evd c in + evd', (n, mk_tycon dom, mk_tycon rng) let valcon_of_tycon x = x let lift_tycon n = Option.map (lift n) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index cd23f9c601..8ff113196b 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -33,12 +33,12 @@ val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> val split_tycon : ?loc:Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t * type_constraint * type_constraint) + evar_map * (Name.t Context.binder_annot * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : int -> type_constraint -> type_constraint -val define_evar_as_product : evar_map -> existential -> evar_map * types +val define_evar_as_product : env -> 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.t diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index e5f2207333..a4a078bfa0 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -12,6 +12,7 @@ open Sorts open Util open CErrors open Names +open Context open Constr open Environ open Termops @@ -193,9 +194,9 @@ let recheck_applications unify flags env evdref t = let rec aux i ty = if i < Array.length argsty then match EConstr.kind !evdref (whd_all env !evdref ty) with - | Prod (na, dom, codom) -> + | Prod (na, dom, codom) -> (match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with - | Success evd -> evdref := evd; + | Success evd -> evdref := evd; aux (succ i) (subst1 args.(i) codom) | UnifFailure (evd, reason) -> Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) @@ -353,7 +354,7 @@ let compute_rel_aliases var_aliases rels sigma = (fun decl (n,aliases) -> (n-1, match decl with - | LocalDef (_,t,u) -> + | LocalDef (_,t,u) -> (match EConstr.kind sigma t with | Var id' -> let aliases_of_n = @@ -640,7 +641,7 @@ let make_projectable_subst aliases sigma evi args = List.fold_right_i (fun i decl (args,all,cstrs,revmap) -> match decl,args with - | LocalAssum (id,c), a::rest -> + | LocalAssum ({binder_name=id},c), a::rest -> let revmap = Id.Map.add id i revmap in let cstrs = let a',args = decompose_app_vect sigma a in @@ -651,7 +652,7 @@ let make_projectable_subst aliases sigma evi args = | _ -> cstrs in let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in (rest,all,cstrs,revmap) - | LocalDef (id,c,_), a::rest -> + | LocalDef ({binder_name=id},c,_), a::rest -> let revmap = Id.Map.add id i revmap in (match EConstr.kind sigma c with | Var id' -> @@ -727,7 +728,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) -> let LocalAssum (na,t_in_env) | LocalDef (na,_,t_in_env) = d in - let id = next_name_away na avoid in + let id = map_annot (fun na -> next_name_away na avoid) na in let evd,t_in_sign = let s = Retyping.get_sort_of env evd t_in_env in let evd,ty_t_in_sign = refresh_universes @@ -743,7 +744,7 @@ 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.Set.add id avoid)) + push_rel d env,evd,Id.Set.add id.binder_name avoid)) rel_sign (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,avoid) in diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index d150f8e1cb..7019cdf046 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -70,7 +70,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl = in match decl,hyploc with | LocalAssum (id,_), InHypValueOnly -> - error_occurrences_error (IncorrectInValueOccurrence id) + error_occurrences_error (IncorrectInValueOccurrence id.Context.binder_name) | LocalAssum (id,typ), _ -> let acc,typ = f acc typ in acc, LocalAssum (id,typ) | LocalDef (id,body,typ), InHypTypeOnly -> diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index d6b204561e..cd82b1993b 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -92,7 +92,7 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env = let open Context.Rel.Declaration in let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in - Array.map get_name ctx, env + Array.map get_annot ctx, env let new_evar env sigma ?src ?naming typ = let open Context.Named.Declaration in diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 63f72e60bd..65ae495135 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -50,7 +50,7 @@ val vars_of_env : t -> Id.Set.t val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t -val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t array * constr array -> t -> Name.t array * t +val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t Context.binder_annot array * constr array -> t -> Name.t Context.binder_annot array * t (** Declare an evar using renaming information *) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 8670c1d964..c57cf88cc6 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -24,6 +24,7 @@ type existential_name = Id.t (** Sorts *) type 'a glob_sort_gen = + | GSProp (** representation of [SProp] literal *) | GProp (** representation of [Prop] literal *) | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index bd321d5886..4f940fa16a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -21,6 +21,7 @@ open Globnames open Nameops open Term open Constr +open Context open Vars open Namegen open Declarations @@ -43,8 +44,8 @@ exception RecursionSchemeError of env * recursion_scheme_error let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na let name_assumption env = function -| LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) -| LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) +| LocalAssum (na,t) -> LocalAssum (map_annot (named_hd env t) na, t) +| LocalDef (na,c,t) -> LocalDef (map_annot (named_hd env c) na, c, t) let mkLambda_or_LetIn_name env d b = mkLambda_or_LetIn (name_assumption env d) b let mkProd_or_LetIn_name env d b = mkProd_or_LetIn (name_assumption env d) b @@ -54,7 +55,7 @@ let it_mkProd_or_LetIn_name env b l = List.fold_left (fun c d -> mkProd_or_LetIn let it_mkLambda_or_LetIn_name env b l = List.fold_left (fun c d -> mkLambda_or_LetIn_name env d c) b l let make_prod_dep dep env = if dep then mkProd_name env else mkProd -let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) +let mkLambda_string s r t c = mkLambda (make_annot (Name (Id.of_string s)) r, t, c) (*******************************************) @@ -79,6 +80,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let indf = make_ind_family(pind, Context.Rel.to_extended_list mkRel 0 lnamespar) in let constrs = get_constructors env indf in let projs = get_projections env ind in + let relevance = Sorts.relevance_of_sort_family kind in let () = if Option.is_empty projs then check_privacy_block mib in let () = @@ -98,11 +100,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let nbprod = k+1 in let indf' = lift_inductive_family nbprod indf in - let arsign,_ = get_arity env indf' in + let arsign,sort = get_arity env indf' in + let r = Sorts.relevance_of_sort_family sort in let depind = build_dependent_inductive env indf' in - let deparsign = LocalAssum (Anonymous,depind)::arsign in + let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in - let ci = make_case_info env (fst pind) RegularStyle in + let rci = relevance in + let ci = make_case_info env (fst pind) rci RegularStyle in let pbody = appvect (mkRel (ndepar + nbprod), @@ -111,7 +115,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let p = it_mkLambda_or_LetIn_name env' ((if dep then mkLambda_name env' else mkLambda) - (Anonymous,depind,pbody)) + (make_annot Anonymous r,depind,pbody)) arsign in let obj = @@ -132,16 +136,16 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = else let cs = lift_constructor (k+1) constrs.(k) in let t = build_branch_type env sigma dep (mkRel (k+1)) cs in - mkLambda_string "f" t - (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) + mkLambda_string "f" relevance t + (add_branch (push_rel (LocalAssum (make_annot Anonymous relevance, t)) env) (k+1)) in let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg sigma kind in let typP = make_arity env' sigma dep indf s in let typP = EConstr.Unsafe.to_constr typP in let c = it_mkLambda_or_LetIn_name env - (mkLambda_string "P" typP - (add_branch (push_rel (LocalAssum (Anonymous,typP)) env') 0)) lnamespar + (mkLambda_string "P" Sorts.Relevant typP + (add_branch (push_rel (LocalAssum (make_annot Anonymous Sorts.Relevant,typP)) env') 0)) lnamespar in (sigma, c) @@ -171,12 +175,12 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in 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) - | LetIn (n,b,t,c) when List.is_empty largs -> - let d = LocalDef (n,b,t) in - mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) + | 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) + | LetIn (n,b,t,c) when List.is_empty largs -> + let d = LocalDef (n,b,t) in + mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c) | Ind (_,_) -> let realargs = List.skipn nparams largs in let base = applist (lift i pk,realargs) in @@ -208,23 +212,24 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match optionpos with | None -> make_prod env - (n,t, - process_constr (push_rel (LocalAssum (n,t)) env) (i+1) c_0 rest + (n,t, + process_constr (push_rel (LocalAssum (n,t)) env) (i+1) c_0 rest (nhyps-1) (i::li)) | Some(dep',p) -> let nP = lift (i+1+decP) p in let env' = push_rel (LocalAssum (n,t)) env in - let t_0 = process_pos env' dep' nP (lift 1 t) in + let t_0 = process_pos env' dep' nP (lift 1 t) in + let r_0 = Retyping.relevance_of_type env' sigma (EConstr.of_constr t_0) in make_prod_dep (dep || dep') env (n,t, - mkArrow t_0 + mkArrow t_0 r_0 (process_constr - (push_rel (LocalAssum (Anonymous,t_0)) env') + (push_rel (LocalAssum (make_annot Anonymous n.binder_relevance,t_0)) env') (i+2) (lift 1 c_0) rest (nhyps-1) (i::li)))) | LetIn (n,b,t,c_0) -> - mkLetIn (n,b,t, + mkLetIn (n,b,t, process_constr - (push_rel (LocalDef (n,b,t)) env) + (push_rel (LocalDef (n,b,t)) env) (i+1) c_0 recargs (nhyps-1) li) | _ -> assert false else @@ -250,12 +255,12 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let p' = EConstr.Unsafe.to_constr p' in let largs = List.map EConstr.Unsafe.to_constr largs in 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) - | LetIn (n,b,t,c) when List.is_empty largs -> - let d = LocalDef (n,b,t) in - mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) + | 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) + | LetIn (n,b,t,c) when List.is_empty largs -> + let d = LocalDef (n,b,t) in + mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c) | Ind _ -> let realargs = List.skipn nparrec largs and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect mkRel 0 hyps) in @@ -280,7 +285,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = (match optionpos with | None -> mkLambda_name env - (n,t,process_constr (push_rel d env) (i+1) + (n,t,process_constr (push_rel d env) (i+1) (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)]))))) (cprest,rest)) | Some(_,f_0) -> @@ -288,12 +293,12 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = let env' = push_rel d env in let arg = process_pos env' nF (lift 1 t) in mkLambda_name env - (n,t,process_constr env' (i+1) + (n,t,process_constr env' (i+1) (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg]))))) (cprest,rest))) | (LocalDef (n,c,t) as d)::cprest, rest -> mkLetIn - (n,c,t, + (n,c,t, process_constr (push_rel d env) (i+1) (lift 1 f) (cprest,rest)) | [],[] -> f @@ -329,25 +334,26 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let recargpar = recargparn [] (nparams-nparrec) in let make_one_rec p = let makefix nbconstruct = - let rec mrec i ln ltyp ldef = function - | ((indi,u),mibi,mipi,dep,_)::rest -> - let tyi = snd indi in - let nctyi = - Array.length mipi.mind_consnames in (* nb constructeurs du type*) + let rec mrec i ln lrelevance ltyp ldef = function + | ((indi,u),mibi,mipi,dep,target_sort)::rest -> + let tyi = snd indi in + let nctyi = + Array.length mipi.mind_consnames in (* nb constructeurs du type*) - (* arity in the context of the fixpoint, i.e. + (* arity in the context of the fixpoint, i.e. P1..P_nrec f1..f_nbconstruct *) - let args = Context.Rel.to_extended_list mkRel (nrec+nbconstruct) lnamesparrec in - let indf = make_ind_family((indi,u),args) in + let args = Context.Rel.to_extended_list mkRel (nrec+nbconstruct) lnamesparrec in + let indf = make_ind_family((indi,u),args) in - let arsign,_ = get_arity env indf in - let depind = build_dependent_inductive env indf in - let deparsign = LocalAssum (Anonymous,depind)::arsign in + let arsign,s = get_arity env indf in + let r = Sorts.relevance_of_sort_family s in + let depind = build_dependent_inductive env indf in + let deparsign = LocalAssum (make_annot Anonymous r,depind)::arsign in - let nonrecpar = Context.Rel.length lnonparrec in - let larsign = Context.Rel.length deparsign in - let ndepar = larsign - nonrecpar in - let dect = larsign+nrec+nbconstruct in + let nonrecpar = Context.Rel.length lnonparrec in + let larsign = Context.Rel.length deparsign in + let ndepar = larsign - nonrecpar in + let dect = larsign+nrec+nbconstruct in (* constructors in context of the Cases expr, i.e. P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *) @@ -375,9 +381,10 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = (* Predicate in the context of the case *) - let depind' = build_dependent_inductive env indf' in - let arsign',_ = get_arity env indf' in - let deparsign' = LocalAssum (Anonymous,depind')::arsign' in + let depind' = build_dependent_inductive env indf' in + let arsign',s = get_arity env indf' in + let r = Sorts.relevance_of_sort_family s in + let deparsign' = LocalAssum (make_annot Anonymous r,depind')::arsign' in let pargs = let nrpar = Context.Rel.to_extended_list mkRel (2*ndepar) lnonparrec @@ -388,13 +395,15 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = in (* body of i-th component of the mutual fixpoint *) + let target_relevance = Sorts.relevance_of_sort_family target_sort in let deftyi = - let ci = make_case_info env indi RegularStyle in + let rci = target_relevance in + let ci = make_case_info env indi rci RegularStyle in let concl = applist (mkRel (dect+j+ndepar),pargs) in let pred = it_mkLambda_or_LetIn_name env ((if dep then mkLambda_name env else mkLambda) - (Anonymous,depind',concl)) + (make_annot Anonymous r,depind',concl)) arsign' in let obj = @@ -416,20 +425,21 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = in it_mkProd_or_LetIn_name env concl deparsign - in - mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (typtyi::ltyp) + in + mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (target_relevance::lrelevance) (typtyi::ltyp) (deftyi::ldef) rest | [] -> let fixn = Array.of_list (List.rev ln) in let fixtyi = Array.of_list (List.rev ltyp) in let fixdef = Array.of_list (List.rev ldef) in - let names = Array.make nrec (Name(Id.of_string "F")) in - mkFix ((fixn,p),(names,fixtyi,fixdef)) + let lrelevance = CArray.rev_of_list lrelevance in + let names = Array.map (fun r -> make_annot (Name(Id.of_string "F")) r) lrelevance in + mkFix ((fixn,p),(names,fixtyi,fixdef)) in - mrec 0 [] [] [] + mrec 0 [] [] [] [] in let rec make_branch env i = function - | ((indi,u),mibi,mipi,dep,_)::rest -> + | ((indi,u),mibi,mipi,dep,sfam)::rest -> let tyi = snd indi in let nconstr = Array.length mipi.mind_consnames in let rec onerec env j = @@ -443,9 +453,10 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let p_0 = type_rec_branch true dep env !evdref (vargs,depPvec,i+j) tyi cs recarg - in - mkLambda_string "f" p_0 - (onerec (push_rel (LocalAssum (Anonymous,p_0)) env) (j+1)) + in + let r_0 = Sorts.relevance_of_sort_family sfam in + mkLambda_string "f" r_0 p_0 + (onerec (push_rel (LocalAssum (make_annot Anonymous r_0,p_0)) env) (j+1)) in onerec env 0 | [] -> makefix i listdepkind @@ -458,9 +469,9 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = evdref := sigma; res in let typP = make_arity env !evdref dep indf s in - let typP = EConstr.Unsafe.to_constr typP in - mkLambda_string "P" typP - (put_arity (push_rel (LocalAssum (Anonymous,typP)) env) (i+1) rest) + let typP = EConstr.Unsafe.to_constr typP in + mkLambda_string "P" Sorts.Relevant typP + (put_arity (push_rel (LocalAssum (anonR,typP)) env) (i+1) rest) | [] -> make_branch env 0 listdepkind in @@ -530,7 +541,7 @@ let weaken_sort_scheme env evd set sort npars term ty = mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else let c',term' = drec (np-1) c in - mkProd (n, t, c'), mkLambda (n, t, term') + mkProd (n, t, c'), mkLambda (n, t, term') | LetIn (n,b,t,c) -> let c',term' = drec np c in mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term') | _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.") @@ -588,6 +599,7 @@ let build_induction_scheme env sigma pind dep kind = (*s Eliminations. *) let elimination_suffix = function + | InSProp -> "_sind" | InProp -> "_ind" | InSet -> "_rec" | InType -> "_rect" diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d937456bcb..678aebfbe6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -15,6 +15,7 @@ open Univ open Term open Constr open Vars +open Context open Termops open Declarations open Declareops @@ -60,6 +61,8 @@ let lift_inductive_family n = liftn_inductive_family n 1 let substnl_ind_family l n = map_ind_family (substnl l n) +let relevance_of_inductive_family env ((ind,_),_ : inductive_family) = + Inductive.relevance_of_inductive env ind type inductive_type = IndType of inductive_family * EConstr.constr list @@ -75,6 +78,9 @@ let lift_inductive_type n = liftn_inductive_type n 1 let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n) +let relevance_of_inductive_type env (IndType (indf, _)) = + relevance_of_inductive_family env indf + let mkAppliedInd (IndType ((ind,params), realargs)) = let open EConstr in let ind = on_snd EInstance.make ind in @@ -276,7 +282,7 @@ let has_dependent_elim mib = | NotRecord | FakeRecord -> true (* Annotation for cases *) -let make_case_info env ind style = +let make_case_info env ind r style = let (mib,mip) = Inductive.lookup_mind_specif env ind in let ind_tags = Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in @@ -289,6 +295,7 @@ let make_case_info env ind style = ci_npar = mib.mind_nparams; ci_cstr_ndecls = mip.mind_consnrealdecls; ci_cstr_nargs = mip.mind_consnrealargs; + ci_relevance = r; ci_pp_info = print_info } (*s Useful functions *) @@ -419,12 +426,14 @@ let build_dependent_inductive env ((ind, params) as indf) = (* builds the arity of an elimination predicate in sort [s] *) let make_arity_signature env sigma dep indf = - let (arsign,_) = get_arity env indf in + let (arsign,s) = get_arity env indf in + let r = Sorts.relevance_of_sort_family s in + let anon = make_annot Anonymous r in let arsign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) arsign in if dep then (* We need names everywhere *) Namegen.name_context env sigma - ((LocalAssum (Anonymous,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) + ((LocalAssum (anon,EConstr.of_constr (build_dependent_inductive env indf)))::arsign) (* Costly: would be better to name once for all at definition time *) else (* No need to enforce names *) @@ -457,7 +466,9 @@ let compute_projections env (kn, i as ind) = let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") - | PrimRecord info-> Name (pi1 (info.(i))) + | PrimRecord info -> + let id, _, _, _ = info.(i) in + make_annot (Name id) mib.mind_packets.(i).mind_relevance in let pkt = mib.mind_packets.(i) in let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in @@ -491,7 +502,7 @@ let compute_projections env (kn, i as ind) = let subst = c1 :: subst in (proj_arg, j+1, pbs, subst) | LocalAssum (na,t) -> - match na with + match na.binder_name with | Name id -> let lab = Label.of_id id in let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab in @@ -601,7 +612,7 @@ let is_predicate_explicitly_dep env sigma pred arsign = From Coq > 8.2, using or not the effective dependency of the predicate is parametrable! *) - begin match na with + begin match na.binder_name with | Anonymous -> false | Name _ -> true end @@ -643,9 +654,10 @@ let type_case_branches_with_names env sigma indspec p c = (* Type of Case predicates *) let arity_of_case_predicate env (ind,params) dep k = - let arsign,_ = get_arity env (ind,params) in + let arsign,s = get_arity env (ind,params) in + let r = Sorts.relevance_of_sort_family s in let mind = build_dependent_inductive env (ind,params) in - let concl = if dep then mkArrow mind (mkSort k) else mkSort k in + let concl = if dep then mkArrow mind r (mkSort k) else mkSort k in Term.it_mkProd_or_LetIn concl arsign (***********************************************) @@ -720,7 +732,7 @@ let control_only_guard env sigma c = match kind c with | CoFix (_,(_,_,_) as cofix) -> Inductive.check_cofix e cofix - | Fix (_,(_,_,_) as fix) -> + | Fix fix -> Inductive.check_fix e fix | _ -> () in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 5a4257e175..c74bbfe98b 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -38,6 +38,8 @@ val lift_inductive_family : int -> inductive_family -> inductive_family val substnl_ind_family : constr list -> int -> inductive_family -> inductive_family +val relevance_of_inductive_family : env -> inductive_family -> Sorts.relevance + (** An inductive type with its parameters and real arguments *) type inductive_type = IndType of inductive_family * EConstr.constr list val make_ind_type : inductive_family * EConstr.constr list -> inductive_type @@ -47,6 +49,8 @@ val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type +val relevance_of_inductive_type : env -> inductive_type -> Sorts.relevance + val mkAppliedInd : inductive_type -> EConstr.constr val mis_is_recursive_subset : int list -> wf_paths -> bool val mis_is_recursive : @@ -176,7 +180,7 @@ val type_case_branches_with_names : env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types (** Annotation for cases *) -val make_case_info : env -> inductive -> case_style -> case_info +val make_case_info : env -> inductive -> Sorts.relevance -> case_style -> case_info (** Make a case or substitute projections if the inductive type is a record with primitive projections. diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index bf8a38a353..fefc15dfb2 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -201,7 +201,7 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in - let env = Typeops.check_context env params in + let env, params = Typeops.check_context env params in let variances = List.fold_left (fun variances entry -> let variances = infer_arity_constructor true env variances entry.mind_entry_arity diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 77ae09ee6f..0b2d760ca8 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -10,6 +10,7 @@ open CErrors open Term open Constr +open Context open Vars open Environ open Reduction @@ -89,10 +90,12 @@ let invert_tag cst tag reloc_tbl = with Find_at j -> (j+1) 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) - | _ -> res + let (name,dom,codom) = destProd (whd_all env t) in + let name = map_annot (function + | Anonymous -> Name (Id.of_string "x") + | na -> na) name + in + (name,dom,codom) let app_type env c = let t = whd_all env c in @@ -194,7 +197,7 @@ let rec nf_val env sigma v typ = | Vaccu accu -> nf_accu env sigma accu | Vfun f -> let lvl = nb_rel env in - let name,dom,codom = + let name,dom,codom = try decompose_prod env typ with DestKO -> CErrors.anomaly @@ -275,11 +278,13 @@ and nf_atom env sigma atom = | Asort s -> mkSort s | Avar id -> mkVar id | Aprod(n,dom,codom) -> - let dom = nf_type env sigma dom in - let vn = mk_rel_accu (nb_rel env) in - let env = push_rel (LocalAssum (n,dom)) env in - let codom = nf_type env sigma (codom vn) in - mkProd(n,dom,codom) + let dom, sdom = nf_type_sort env sigma dom in + let rdom = Sorts.relevance_of_sort sdom in + let n = make_annot n rdom in + let vn = mk_rel_accu (nb_rel env) in + let env = push_rel (LocalAssum (n,dom)) env in + let codom = nf_type env sigma (codom vn) in + mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv | Aproj (p, c) -> let c = nf_accu env sigma c in @@ -325,28 +330,34 @@ and nf_atom_type env sigma atom = let ci = ans.asw_ci in 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 tt = Array.map (fun t -> nf_type_sort env sigma t) tt in + let tt = Array.map fst tt and rt = Array.map snd tt in + let name = Name (Id.of_string "Ffix") in + let names = Array.map (fun s -> make_annot name (Sorts.relevance_of_sort s)) rt in let lvl = nb_rel env in let nbfix = Array.length ft in let fargs = mk_rels_accu lvl (Array.length ft) in - (* Third argument of the tuple is ignored by push_rec_types *) - let env = push_rec_types (name,tt,[||]) env in + (* Body argument of the tuple is ignored by push_rec_types *) + let env = push_rec_types (names,tt,[||]) env in (* We lift here because the types of arguments (in tt) will be evaluated in an environment where the fixpoints have been pushed *) let norm_body i v = nf_val env sigma (napply v fargs) (lift nbfix tt.(i)) in let ft = Array.mapi norm_body ft in - mkFix((rp,s),(name,tt,ft)), tt.(s) + mkFix((rp,s),(names,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 tt = Array.map (fun t -> nf_type_sort env sigma t) tt in + let tt = Array.map fst tt and rt = Array.map snd tt in + let name = Name (Id.of_string "Fcofix") in let lvl = nb_rel env in + let names = Array.map (fun s -> make_annot name (Sorts.relevance_of_sort s)) rt in let fargs = mk_rels_accu lvl (Array.length ft) in - let env = push_rec_types (name,tt,[||]) env in + let env = push_rec_types (names,tt,[||]) env in let ft = Array.mapi (fun i v -> nf_val env sigma (napply v fargs) tt.(i)) ft in - mkCoFix(s,(name,tt,ft)), tt.(s) + mkCoFix(s,(names,tt,ft)), tt.(s) | Aprod(n,dom,codom) -> let dom,s1 = nf_type_sort env sigma dom in + let r1 = Sorts.relevance_of_sort s1 in + let n = make_annot n r1 in 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 @@ -390,6 +401,8 @@ and nf_predicate env sigma ind mip params v pT = 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 let dom = mkApp(mkIndU ind,Array.append params rargs) in + let r = Inductive.relevance_of_inductive env (fst ind) in + let name = make_annot name r in let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in mkLambda(name,dom,body) | _ -> nf_type env sigma v diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 6803ea7d9b..13034d078a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -15,6 +15,7 @@ open Globnames open Nameops open Term open Constr +open Context open Glob_term open Pp open Mod_subst @@ -153,16 +154,20 @@ let pattern_of_constr env sigma t = | Rel n -> PRel n | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n))) | Var id -> PVar id + | Sort SProp -> PSort GSProp | Sort Prop -> PSort GProp | Sort Set -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c - | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), - pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) - | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) - | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + | LetIn (na,c,t,b) -> PLetIn (na.binder_name, + pattern_of_constr env c,Some (pattern_of_constr env t), + pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) + | Prod (na,c,b) -> PProd (na.binder_name, + pattern_of_constr env c, + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + | Lambda (na,c,b) -> PLambda (na.binder_name, + pattern_of_constr env c, + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match match kind f with @@ -206,12 +211,12 @@ let pattern_of_constr env sigma t = | Fix (lni,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in - PFix (lni,(lna,Array.map (pattern_of_constr env) tl, + PFix (lni,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | CoFix (ln,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in - PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl, + PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | Int i -> PInt i in pattern_of_constr env t diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index dc6607557d..35a7036af4 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -60,6 +60,7 @@ type pretype_error = | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option + | DisallowedSProp exception PretypeError of env * Evd.evar_map * pretype_error @@ -107,9 +108,9 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys = raise_type_error ?loc (env, sigma, IllTypedRecBody (i, na, jl, tys)) -let error_elim_arity ?loc env sigma pi s c j a = +let error_elim_arity ?loc env sigma pi c j a = raise_type_error ?loc - (env, sigma, ElimArity (pi, s, c, j, a)) + (env, sigma, ElimArity (pi, c, j, a)) let error_not_a_type ?loc env sigma j = raise_type_error ?loc (env, sigma, NotAType j) @@ -171,6 +172,9 @@ let error_var_not_found ?loc env sigma s = let error_evar_not_found ?loc env sigma id = raise_pretype_error ?loc (env, sigma, EvarNotFound id) +let error_disallowed_sprop env sigma = + raise (PretypeError (env, sigma, DisallowedSProp)) + (*s Typeclass errors *) let unsatisfiable_constraints env evd ev comp = diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index a0d459fe6b..a9e2b0ea8f 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -67,6 +67,7 @@ type pretype_error = | UnsatisfiableConstraints of (Evar.t * Evar_kinds.t) option * Evar.Set.t option (** unresolvable evar, connex component *) + | DisallowedSProp exception PretypeError of env * Evd.evar_map * pretype_error @@ -101,12 +102,12 @@ val error_number_branches : val error_ill_typed_rec_body : ?loc:Loc.t -> env -> Evd.evar_map -> - int -> Name.t array -> unsafe_judgment array -> types array -> 'b + int -> Name.t Context.binder_annot array -> unsafe_judgment array -> types array -> 'b 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 -> constr -> + unsafe_judgment -> (Sorts.family list * Sorts.family * Sorts.family * arity_error) option -> 'b val error_not_a_type : ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b @@ -158,6 +159,8 @@ val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b val error_evar_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b +val error_disallowed_sprop : env -> Evd.evar_map -> 'a + (** {6 Typeclass errors } *) val unsatisfiable_constraints : env -> Evd.evar_map -> Evar.t option -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9612932439..8e9a2e114b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -29,7 +29,7 @@ open Util open Names open Evd open Constr -open Term +open Context open Termops open Environ open EConstr @@ -399,11 +399,13 @@ let pretype_id pretype k0 loc env sigma id = (* Main pretyping function *) let interp_known_glob_level ?loc evd = function + | GSProp -> Univ.Level.sprop | GProp -> Univ.Level.prop | GSet -> Univ.Level.set | GType s -> interp_known_level_info ?loc evd s let interp_glob_level ?loc evd : glob_level -> _ = function + | GSProp -> evd, Univ.Level.sprop | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_level_info ?loc evd s @@ -448,11 +450,12 @@ let pretype_ref ?loc sigma env ref us = let judge_of_Type ?loc evd s = let evd, s = interp_universe ?loc evd s in let judge = - { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } + { uj_val = mkType s; uj_type = mkType (Univ.super s) } in evd, judge let pretype_sort ?loc sigma = function + | GSProp -> sigma, judge_of_sprop | GProp -> sigma, judge_of_prop | GSet -> sigma, judge_of_set | GType s -> judge_of_Type ?loc sigma s @@ -473,8 +476,8 @@ let mark_obligation_evar sigma k evc = let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t = let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in - let pretype_type = pretype_type k0 resolve_tc in - let pretype = pretype k0 resolve_tc in + let pretype_type = pretype_type ~program_mode k0 resolve_tc in + let pretype = pretype ~program_mode k0 resolve_tc in let open Context.Rel.Declaration in let loc = t.CAst.loc in match DAst.get t with @@ -483,7 +486,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo inh_conv_coerce_to_tycon ?loc env sigma t_ref tycon | GVar id -> - let sigma, t_id = pretype_id (fun e r t -> pretype ~program_mode tycon e r t) k0 loc env sigma id in + let sigma, t_id = pretype_id (fun e r t -> pretype tycon e r t) k0 loc env sigma id in inh_conv_coerce_to_tycon ?loc env sigma t_id tycon | GEvar (id, inst) -> @@ -535,21 +538,23 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let rec type_bl env sigma ctxt = function | [] -> sigma, ctxt | (na,bk,None,ty)::bl -> - let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in - let dcl = LocalAssum (na, ty'.utj_val) in + let sigma, ty' = pretype_type empty_valcon env sigma ty in + let rty' = Sorts.relevance_of_sort ty'.utj_type in + let dcl = LocalAssum (make_annot na rty', ty'.utj_val) in let dcl', env = push_rel ~hypnaming sigma dcl env in type_bl env sigma (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> - let sigma, ty' = pretype_type ~program_mode empty_valcon env sigma ty in - let sigma, bd' = pretype ~program_mode (mk_tycon ty'.utj_val) env sigma bd in - let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in + let sigma, ty' = pretype_type empty_valcon env sigma ty in + let rty' = Sorts.relevance_of_sort ty'.utj_type in + let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in + let dcl = LocalDef (make_annot na rty', bd'.uj_val, ty'.utj_val) in let dcl', env = push_rel ~hypnaming sigma dcl env in type_bl env sigma (Context.Rel.add dcl' ctxt) bl in let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in let sigma, larj = Array.fold_left2_map (fun sigma e ar -> - pretype_type ~program_mode empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar) + pretype_type empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar) sigma ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -568,6 +573,10 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo end | None -> sigma in + let names = Array.map2 (fun na t -> + make_annot na (Retyping.relevance_of_type !!(env) sigma t)) + names ftys + in (* Note: bodies are not used by push_rec_types, so [||] is safe *) let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in let sigma, vdefj = @@ -579,7 +588,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo decompose_prod_n_assum sigma (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in - let sigma, j = pretype ~program_mode (mk_tycon ty) nenv sigma def in + let sigma, j = pretype (mk_tycon ty) nenv sigma def in sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) sigma ctxtv vdef in @@ -602,10 +611,10 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) vn) in - let fixdecls = (names,ftys,fdefs) in + let fixdecls = (names,ftys,fdefs) in let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) - | GCoFix i -> + | GCoFix i -> let fixdecls = (names,ftys,fdefs) in let cofix = (i, fixdecls) in (try check_cofix !!env (i, nf_fix sigma fixdecls) @@ -622,7 +631,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo inh_conv_coerce_to_tycon ?loc env sigma j tycon | GApp (f,args) -> - let sigma, fj = pretype ~program_mode empty_tycon env sigma f in + let sigma, fj = pretype empty_tycon env sigma f in let floc = loc_of_glob_constr f in let length = List.length args in let candargs = @@ -665,7 +674,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo match EConstr.kind sigma resty with | Prod (na,c1,c2) -> let tycon = Some c1 in - let sigma, hj = pretype ~program_mode tycon env sigma c in + let sigma, hj = pretype tycon env sigma c in let sigma, candargs, ujval = match candargs with | [] -> sigma, [], j_val hj @@ -677,12 +686,12 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo sigma, args, nf_evar sigma (j_val hj) end in - let sigma, ujval = adjust_evar_source sigma na ujval in - let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in + let sigma, ujval = adjust_evar_source sigma na.binder_name ujval in + let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in let j = { uj_val = value; uj_type = typ } in apply_rec env sigma (n+1) j candargs rest | _ -> - let sigma, hj = pretype ~program_mode empty_tycon env sigma c in + let sigma, hj = pretype empty_tycon env sigma c in error_cant_apply_not_functional ?loc:(Loc.merge_opt floc argloc) !!env sigma resj [|hj|] in @@ -712,26 +721,28 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo in let sigma, (name',dom,rng) = split_tycon ?loc !!env sigma tycon' in let dom_valcon = valcon_of_tycon dom in - let sigma, j = pretype_type ~program_mode dom_valcon env sigma c1 in + let sigma, j = pretype_type dom_valcon env sigma c1 in + let name = {binder_name=name; binder_relevance=Sorts.relevance_of_sort j.utj_type} in let var = LocalAssum (name, j.utj_val) in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let var',env' = push_rel ~hypnaming sigma var env in - let sigma, j' = pretype ~program_mode rng env' sigma c2 in + let sigma, j' = pretype rng env' sigma c2 in let name = get_name var' in - let resj = judge_of_abstraction !!env (orelse_name name name') j j' in + let resj = judge_of_abstraction !!env (orelse_name name name'.binder_name) j j' in inh_conv_coerce_to_tycon ?loc env sigma resj tycon | GProd(name,bk,c1,c2) -> - let sigma, j = pretype_type ~program_mode empty_valcon env sigma c1 in + let sigma, j = pretype_type empty_valcon env sigma c1 in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let sigma, name, j' = match name with | Anonymous -> - let sigma, j = pretype_type ~program_mode empty_valcon env sigma c2 in + let sigma, j = pretype_type empty_valcon env sigma c2 in sigma, name, { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = LocalAssum (name, j.utj_val) in + let r = Sorts.relevance_of_sort j.utj_type in + let var = LocalAssum (make_annot name r, j.utj_val) in let var, env' = push_rel ~hypnaming sigma var env in - let sigma, c2_j = pretype_type ~program_mode empty_valcon env' sigma c2 in + let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in sigma, get_name var, c2_j in let resj = @@ -747,24 +758,25 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let sigma, tycon1 = match t with | Some t -> - let sigma, t_j = pretype_type ~program_mode empty_valcon env sigma t in + let sigma, t_j = pretype_type empty_valcon env sigma t in sigma, mk_tycon t_j.utj_val | None -> sigma, empty_tycon in - let sigma, j = pretype ~program_mode tycon1 env sigma c1 in + let sigma, j = pretype tycon1 env sigma c1 in let sigma, t = Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma j.uj_type in - let var = LocalDef (name, j.uj_val, t) in + let r = Retyping.relevance_of_term !!env sigma j.uj_val in + let var = LocalDef (make_annot name r, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let var, env = push_rel ~hypnaming sigma var env in - let sigma, j' = pretype ~program_mode tycon env sigma c2 in + let sigma, j' = pretype tycon env sigma c2 in let name = get_name var in - sigma, { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; + sigma, { uj_val = mkLetIn (make_annot name r, j.uj_val, t, j'.uj_val) ; uj_type = subst1 j.uj_val j'.uj_type } | GLetTuple (nal,(na,po),c,d) -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) = try find_rectype !!env sigma cj.uj_type with Not_found -> @@ -788,10 +800,11 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo | Some ps -> let rec aux n k names l = match names, l with - | na :: names, (LocalAssum (_,t) :: l) -> + | na :: names, (LocalAssum (na', t) :: l) -> let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - LocalDef (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) + LocalDef ({na' with binder_name = na}, + lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -801,27 +814,27 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let fsign = Context.Rel.map (whd_betaiota sigma) fsign in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in - let obj ind p v f = + let obj ind rci p v f = if not record then - let f = it_mkLambda_or_LetIn f fsign in - let ci = make_case_info !!env (fst ind) LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) + let f = it_mkLambda_or_LetIn f fsign in + let ci = make_case_info !!env (fst ind) rci LetStyle in + mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in (* Make dependencies from arity signature impossible *) - let arsgn = - let arsgn,_ = get_arity !!env indf in - List.map (set_name Anonymous) arsgn + let arsgn, indr = + let arsgn,s = get_arity !!env indf in + List.map (set_name Anonymous) arsgn, Sorts.relevance_of_sort_family s in let indt = build_dependent_inductive !!env indf in - let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let nar = List.length arsgn in let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in (match po with | Some p -> - let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in + let sigma, pj = pretype_type empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let p = it_mkLambda_or_LetIn ccl psign' in let inst = @@ -829,17 +842,17 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist !!env sigma lp inst in - let sigma, fj = pretype ~program_mode (mk_tycon fty) env_f sigma d in + let sigma, fj = pretype (mk_tycon fty) env_f sigma d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort !!env sigma ind cj.uj_val p; - obj ind p cj.uj_val fj.uj_val - in + let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in + obj ind rci p cj.uj_val fj.uj_val + in sigma, { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in - let sigma, fj = pretype ~program_mode tycon env_f sigma d in + let sigma, fj = pretype tycon env_f sigma d in let ccl = nf_evar sigma fj.uj_type in let ccl = if noccur_between sigma 1 cs.cs_nargs ccl then @@ -851,12 +864,12 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort !!env sigma ind cj.uj_val p; - obj ind p cj.uj_val fj.uj_val + let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val p in + obj ind rci p cj.uj_val fj.uj_val in sigma, { uj_val = v; uj_type = ccl }) | GIf (c,(na,po),b1,b2) -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let (IndType (indf,realargs)) = try find_rectype !!env sigma cj.uj_type with Not_found -> @@ -867,21 +880,21 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo user_err ?loc (str "If is only for inductive types with two constructors."); - let arsgn = - let arsgn,_ = get_arity !!env indf in + let arsgn, indr = + let arsgn,s = get_arity !!env indf in (* Make dependencies from arity signature impossible *) - List.map (set_name Anonymous) arsgn + List.map (set_name Anonymous) arsgn, Sorts.relevance_of_sort_family s in let nar = List.length arsgn in let indt = build_dependent_inductive !!env indf in - let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *) + let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *) let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in let sigma, pred, p = match po with | Some p -> - let sigma, pj = pretype_type ~program_mode empty_valcon env_p sigma p in + let sigma, pj = pretype_type empty_valcon env_p sigma p in let ccl = nf_evar sigma pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist sigma (pred,[cj.uj_val])) in @@ -904,38 +917,38 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo List.map (set_name Anonymous) cs_args in let _,env_c = push_rel_context ~hypnaming sigma csgn env in - let sigma, bj = pretype ~program_mode (mk_tycon pi) env_c sigma b in + let sigma, bj = pretype (mk_tycon pi) env_c sigma b in sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in let sigma, b1 = f sigma cstrs.(0) b1 in let sigma, b2 = f sigma cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in - let ci = make_case_info !!env (fst ind) IfStyle in let pred = nf_evar sigma pred in - Typing.check_allowed_sort !!env sigma ind cj.uj_val pred; - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + let rci = Typing.check_allowed_sort !!env sigma ind cj.uj_val pred in + let ci = make_case_info !!env (fst ind) rci IfStyle in + mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in let cj = { uj_val = v; uj_type = p } in inh_conv_coerce_to_tycon ?loc env sigma cj tycon | GCases (sty,po,tml,eqns) -> - Cases.compile_cases ?loc ~program_mode sty (pretype ~program_mode, sigma) tycon env (po,tml,eqns) + Cases.compile_cases ?loc ~program_mode sty (pretype, sigma) tycon env (po,tml,eqns) | GCast (c,k) -> let sigma, cj = match k with | CastCoerce -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in Coercion.inh_coerce_to_base ?loc ~program_mode !!env sigma cj | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in - let sigma, tj = pretype_type ~program_mode empty_valcon env sigma t in + let sigma, tj = pretype_type empty_valcon env sigma t in let sigma, tval = Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env sigma tj.utj_val in let tval = nf_evar sigma tval in let (sigma, cj), tval = match k with | VMcast -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in if not (occur_existential sigma cty || occur_existential sigma tval) then match Reductionops.vm_infer_conv !!env sigma cty tval with @@ -946,7 +959,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo else user_err ?loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> - let sigma, cj = pretype ~program_mode empty_tycon env sigma c in + let sigma, cj = pretype empty_tycon env sigma c in let cty = nf_evar sigma cj.uj_type and tval = nf_evar sigma tval in begin match Nativenorm.native_infer_conv !!env sigma cty tval with @@ -956,7 +969,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo (ConversionFailed (!!env,cty,tval)) end | _ -> - pretype ~program_mode (mk_tycon tval) env sigma c, tval + pretype (mk_tycon tval) env sigma c, tval in let v = mkCast (cj.uj_val, k, tval) in sigma, { uj_val = v; uj_type = tval } diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d0359b43f4..34a6cecc95 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -5,10 +5,10 @@ Pretype_errors Reductionops Inductiveops InferCumulativity -Vnorm Arguments_renaming -Nativenorm Retyping +Vnorm +Nativenorm Cbv Find_subterm Evardefine diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 98ca329117..71fbfe8716 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -12,6 +12,7 @@ open CErrors open Util open Names open Constr +open Context open Termops open Univ open Evd @@ -479,10 +480,10 @@ struct | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) - | Case (info,ty,br,alt) -> Case (info, f ty, Array.map f br, alt) - | Fix ((r,(na,ty,bo)),arg,alt) -> - Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt) - | Cst (cst,curr,remains,params,alt) -> + | Case (info,ty,br,alt) -> Case (info, f ty, Array.map f br, alt) + | Fix ((r,(na,ty,bo)),arg,alt) -> + Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt) + | Cst (cst,curr,remains,params,alt) -> Cst (cst,curr,remains,map f params,alt) | Primitive (p,c,args,kargs,cst_l) -> Primitive(p,c, map f args, kargs, cst_l) @@ -775,7 +776,7 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in + | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -817,7 +818,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies | Some e -> match reference with | None -> bd - | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind) in + | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in let closure = List.init nbodies make_Fi in substl closure bodies.(bodynum) @@ -1062,7 +1063,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA -> apply_subst (fun _ -> whrec) [] sigma refold cst_l x stack | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA -> - let env' = push_rel (LocalAssum (na, t)) env in + let env' = push_rel (LocalAssum (na, t)) env in let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in (match EConstr.kind sigma (Stack.zip ~refold sigma (fst (whrec' (c, Stack.empty)))) with | App (f,cl) -> @@ -1520,7 +1521,9 @@ let plain_instance sigma s c = match EConstr.kind sigma g with | App _ -> let l' = Array.Fun1.Smart.map lift 1 l' in - mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l')) + let r = Sorts.Relevant in (* TODO fix relevance *) + let na = make_annot (Name default_plain_instance_ident) r in + mkLetIn (na,g,t,mkApp(mkRel 1, l')) | _ -> mkApp (g,l') with Not_found -> mkApp (f,l')) | _ -> mkApp (irec n f,l')) @@ -1623,11 +1626,11 @@ let splay_prod_assum env sigma = let t = whd_allnolet env sigma c in match EConstr.kind sigma t with | Prod (x,t,c) -> - prodec_rec (push_rel (LocalAssum (x,t)) env) - (Context.Rel.add (LocalAssum (x,t)) l) c + prodec_rec (push_rel (LocalAssum (x,t)) env) + (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> - prodec_rec (push_rel (LocalDef (x,b,t)) env) - (Context.Rel.add (LocalDef (x,b,t)) l) c + prodec_rec (push_rel (LocalDef (x,b,t)) env) + (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> let t' = whd_all env sigma t in @@ -1648,8 +1651,8 @@ let splay_prod_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match EConstr.kind sigma (whd_all env sigma c) with | Prod (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_prod_n" in decrec env n Context.Rel.empty @@ -1658,8 +1661,8 @@ let splay_lam_n env sigma n = let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else match EConstr.kind sigma (whd_all env sigma c) with | Lambda (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 + decrec (push_rel (LocalAssum (n,a)) env) + (m-1) (Context.Rel.add (LocalAssum (n,a)) ln) c0 | _ -> invalid_arg "splay_lam_n" in decrec env n Context.Rel.empty diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index fae0b23b83..5938d9b367 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -235,9 +235,9 @@ val hnf_lam_app : env -> evar_map -> constr -> constr -> constr val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr -val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * ESorts.t +val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t val sort_of_arity : env -> evar_map -> constr -> ESorts.t val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a76a203e37..20120f4182 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -13,6 +13,7 @@ open CErrors open Util open Term open Constr +open Context open Inductive open Inductiveops open Names @@ -79,7 +80,8 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = match EConstr.kind sigma (whd_all env sigma ar), args with - | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l + | Prod (na, t, b), h::l -> + concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l | Sort s, [] -> ESorts.kind sigma s | _ -> retype_error NotASort in concl_of_arity env 0 ft (Array.to_list args) @@ -150,8 +152,8 @@ 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 | Set -> Sorts.type1 - | Type u -> Type (Univ.super u) + | SProp | Prop | Set -> Sorts.type1 + | Type u -> Sorts.sort_of_univ (Univ.super u) end | Prod (name,t,c2) -> let dom = sort_of env t in @@ -188,7 +190,7 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = | 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 + 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 Termops.is_template_polymorphic_ind env sigma f -> @@ -256,3 +258,41 @@ let expand_projection env sigma pr c args = in mkApp (mkConstU (Projection.constant pr,u), Array.of_list (ind_args @ (c :: args))) + +let relevance_of_term env sigma c = + if Environ.sprop_allowed env then + let rec aux rels c = + match kind sigma c with + | Rel n -> Retypeops.relevance_of_rel_extra env rels n + | Var x -> Retypeops.relevance_of_var env x + | Sort _ -> Sorts.Relevant + | Cast (c, _, _) -> aux rels c + | Prod ({binder_relevance=r}, _, codom) -> + aux (r::rels) codom + | Lambda ({binder_relevance=r}, _, bdy) -> + aux (r::rels) bdy + | LetIn ({binder_relevance=r}, _, _, bdy) -> + aux (r::rels) bdy + | App (c, _) -> aux rels c + | Const (c,_) -> Retypeops.relevance_of_constant env c + | Ind _ -> Sorts.Relevant + | Construct (c,_) -> Retypeops.relevance_of_constructor env c + | Case (ci, _, _, _) -> ci.ci_relevance + | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance + | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance + | Proj (p, _) -> Retypeops.relevance_of_projection env p + | Int _ -> Sorts.Relevant + + | Meta _ | Evar _ -> Sorts.Relevant + + in + aux [] c + else Sorts.Relevant + +let relevance_of_type env sigma t = + let s = get_sort_family_of env sigma t in + Sorts.relevance_of_sort_family s + +let relevance_of_sort s = Sorts.relevance_of_sort (EConstr.Unsafe.to_sorts s) + +let relevance_of_sort_family f = Sorts.relevance_of_sort_family f diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 2aff0c7775..252bfb1a84 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -53,3 +53,8 @@ val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.t + +val relevance_of_term : env -> evar_map -> constr -> Sorts.relevance +val relevance_of_type : env -> evar_map -> types -> Sorts.relevance +val relevance_of_sort : ESorts.t -> Sorts.relevance +val relevance_of_sort_family : Sorts.family -> Sorts.relevance diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 5db571433a..bcc20a41b4 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Constr +open Context open Libnames open Globnames open Termops @@ -229,7 +230,8 @@ let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) = (* Heuristic to look if global names are associated to other components of a mutual fixpoint *) -let invert_name labs l na0 env sigma ref = function +let invert_name labs l {binder_name=na0} env sigma ref na = + match na.binder_name with | Name id -> let minfxargs = List.length l in begin match na0 with @@ -249,7 +251,7 @@ let invert_name labs l na0 env sigma ref = function | Some c -> let labs',ccl = decompose_lam sigma c in let _, l' = whd_betalet_stack sigma ccl in - let labs' = List.map snd labs' in + let labs' = List.map snd labs' in (* ppedrot: there used to be generic equality on terms here *) let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in if List.equal eq_constr labs' labs && @@ -269,7 +271,7 @@ let compute_consteval_direct env sigma ref = match EConstr.kind sigma c' with | Lambda (id,t,g) when List.is_empty l && not onlyproj -> let open Context.Rel.Declaration in - srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g + srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g | Fix fix when not onlyproj -> (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) @@ -289,7 +291,7 @@ let compute_consteval_mutual_fix env sigma ref = match EConstr.kind sigma c' with | Lambda (na,t,g) when List.is_empty l -> let open Context.Rel.Declaration in - srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g + srec (push_rel (LocalAssum (na,t)) env) (minarg+1) (t::labs) ref g | Fix ((lv,i),(names,_,_)) -> (* Last known constant wrapping Fix is ref = [labs](Fix l) *) (match compute_consteval_direct env sigma ref with @@ -374,7 +376,8 @@ let make_elim_fun (names,(nbfix,lv,n)) u largs = List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) -> let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in let tij' = Vars.substl (List.rev subst) tij in - mkLambda (x,tij',c)) 1 body (List.rev lv) + let x = make_annot x Sorts.Relevant in (* TODO relevance *) + mkLambda (x,tij',c)) 1 body (List.rev lv) in Some (minargs,g) (* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]: @@ -384,7 +387,8 @@ let dummy = mkProp let vfx = Id.of_string "_expanded_fix_" let vfun = Id.of_string "_eliminator_function_" let venv = let open Context.Named.Declaration in - val_of_named_context [LocalAssum (vfx, dummy); LocalAssum (vfun, dummy)] + val_of_named_context [LocalAssum (make_annot vfx Sorts.Relevant, dummy); + LocalAssum (make_annot vfun Sorts.Relevant, dummy)] (* Mark every occurrence of substituted vars (associated to a function) as a problem variable: an evar that can be instantiated either by @@ -513,7 +517,7 @@ let reduce_mind_case_use_function func env sigma mia = let minargs = List.length mia.mcargs in fun i -> if Int.equal i bodynum then Some (minargs,func) - else match names.(i) with + else match names.(i).binder_name with | Anonymous -> None | Name id -> (* In case of a call to another component of a block of @@ -627,12 +631,12 @@ let whd_nothing_for_iota env sigma s = | Rel n -> let open Context.Rel.Declaration in (match lookup_rel n env with - | LocalDef (_,body,_) -> whrec (lift n body, stack) + | LocalDef (_,body,_) -> whrec (lift n body, stack) | _ -> s) | Var id -> let open Context.Named.Declaration in (match lookup_named id env with - | LocalDef (_,body,_) -> whrec (body, stack) + | LocalDef (_,body,_) -> whrec (body, stack) | _ -> s) | Evar ev -> s | Meta ev -> @@ -838,10 +842,10 @@ let try_red_product env sigma c = | Cast (c,_,_) -> redrec env c | Prod (x,a,b) -> let open Context.Rel.Declaration in - mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b) + mkProd (x, a, redrec (push_rel (LocalAssum (x, a)) env) b) | LetIn (x,a,b,t) -> redrec env (Vars.subst1 a t) | Case (ci,p,d,lf) -> simpfun (mkCase (ci,p,redrec env d,lf)) - | Proj (p, c) -> + | Proj (p, c) -> let c' = match EConstr.kind sigma c with | Construct _ -> c @@ -1150,6 +1154,7 @@ let compute = cbv_betadeltaiota let abstract_scheme env sigma (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env sigma ta Anonymous in + let na = make_annot na Sorts.Relevant in (* TODO relevance *) if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation."); if occur_meta sigma a then mkLambda (na,ta,c), sigma @@ -1192,7 +1197,7 @@ let reduce_to_ind_gen allow_product env sigma t = | Prod (n,ty,t') -> let open Context.Rel.Declaration in if allow_product then - elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) + elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else user_err (str"Not an inductive definition.") | _ -> @@ -1270,7 +1275,7 @@ let reduce_to_ref_gen allow_product env sigma ref t = | Prod (n,ty,t') -> if allow_product then let open Context.Rel.Declaration in - elimrec (push_rel (LocalAssum (n,t)) env) t' ((LocalAssum (n,ty))::l) + elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l) else error_cannot_recognize ref | _ -> diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ea6e52e1f8..89f72c874b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -15,6 +15,7 @@ open CErrors open Util open Term open Constr +open Context open Environ open EConstr open Vars @@ -65,7 +66,7 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in let (_,c1,c2) = destProd sigma t in sigma, (c1,c2) | _ -> @@ -90,7 +91,7 @@ let judge_of_apply env sigma funj argjv = match EConstr.kind sigma (whd_all env sigma typ) with | Prod (_,c1,c2) -> sigma, (c1,c2) | Evar ev -> - let (sigma,t) = Evardefine.define_evar_as_product sigma ev in + let (sigma,t) = Evardefine.define_evar_as_product env sigma ev in let (_,c1,c2) = destProd sigma t in sigma, (c1,c2) | _ -> @@ -122,7 +123,7 @@ let max_sort l = let is_correct_arity env sigma c pj ind specif params = let arsign = make_arity_signature env sigma true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = Pretype_errors.error_elim_arity env sigma ind allowed_sorts c pj None in + let error () = Pretype_errors.error_elim_arity env sigma ind c pj None in let rec srec env sigma pt ar = let pt' = whd_all env sigma pt in match EConstr.kind sigma pt', ar with @@ -136,11 +137,11 @@ let is_correct_arity env sigma c pj ind specif params = let s = ESorts.kind sigma s in if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () - else sigma + else sigma, s | Evar (ev,_), [] -> let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in let sigma = Evd.define ev (mkSort s) sigma in - sigma + sigma, s | _, (LocalDef _ as d)::ar' -> srec (push_rel d env) sigma (lift 1 pt') ar' | _ -> @@ -165,20 +166,20 @@ let type_case_branches env sigma (ind,largs) pj c = let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in let params = List.map EConstr.Unsafe.to_constr params in - let sigma = is_correct_arity env sigma c pj ind specif params in + let sigma, ps = is_correct_arity env sigma c pj ind specif params in let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in - sigma, (lc, ty) + sigma, (lc, ty, Sorts.relevance_of_sort ps) let judge_of_case env sigma ci pj cj lfj = let ((ind, u), spec) = try find_mrectype env sigma cj.uj_type with Not_found -> error_case_not_inductive env sigma cj in let indspec = ((ind, EInstance.kind sigma u), spec) in - let _ = check_case_info env (fst indspec) ci in - let sigma, (bty,rslty) = type_case_branches env sigma indspec pj cj.uj_val in + let sigma, (bty,rslty,rci) = type_case_branches env sigma indspec pj cj.uj_val in + let () = check_case_info env (fst indspec) rci ci in let sigma = check_branch_types env sigma (fst indspec) cj (lfj,bty) in sigma, { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } @@ -203,11 +204,13 @@ let check_allowed_sort env sigma ind c p = let _, s = splay_prod env sigma pj.uj_type in let ksort = match EConstr.kind sigma s with | Sort s -> Sorts.family (ESorts.kind sigma s) - | _ -> error_elim_arity env sigma ind sorts c pj None in + | _ -> error_elim_arity env sigma ind c pj None in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in - error_elim_arity env sigma ind sorts c pj - (Some(ksort,s,Type_errors.error_elim_explain ksort s)) + error_elim_arity env sigma ind c pj + (Some(sorts,ksort,s,Type_errors.error_elim_explain ksort s)) + else + Sorts.relevance_of_sort_family ksort let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in @@ -230,6 +233,10 @@ let check_cofix env sigma pcofix = (* The typing machine with universes and existential variables. *) +let judge_of_sprop = + { uj_val = EConstr.mkSProp; + uj_type = EConstr.type1 } + let judge_of_prop = { uj_val = EConstr.mkProp; uj_type = EConstr.mkSort Sorts.type1 } @@ -262,16 +269,19 @@ let judge_of_projection env sigma p cj = uj_type = ty} let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } + let r = Sorts.relevance_of_sort var.utj_type in + { uj_val = mkLambda (make_annot name r, var.utj_val, j.uj_val); + uj_type = mkProd (make_annot name r, var.utj_val, j.uj_type) } let judge_of_product env name t1 t2 = + let r = Sorts.relevance_of_sort t1.utj_type in let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); + { uj_val = mkProd (make_annot name r, t1.utj_val, t2.utj_val); uj_type = mkSort s } let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; + let r = Sorts.relevance_of_sort typj.utj_type in + { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } let check_hyps_inclusion env sigma f x hyps = @@ -349,7 +359,7 @@ let rec execute env sigma cstr = | Fix ((vn,i as vni),recdef) -> let sigma, (_,tys,_ as recdef') = execute_recdef env sigma recdef in - let fix = (vni,recdef') in + let fix = (vni,recdef') in check_fix env sigma fix; sigma, make_judge (mkFix fix) tys.(i) @@ -361,6 +371,9 @@ let rec execute env sigma cstr = | Sort s -> begin match ESorts.kind sigma s with + | SProp -> + if Environ.sprop_allowed env then sigma, judge_of_sprop + else error_disallowed_sprop env sigma | Prop -> sigma, judge_of_prop | Set -> sigma, judge_of_set | Type u -> sigma, judge_of_type u @@ -384,26 +397,29 @@ let rec execute env sigma cstr = | Lambda (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, var = type_judgment env sigma j in - let env1 = push_rel (LocalAssum (name, var.utj_val)) env in + let name = check_binder_annot var.utj_type name in + let env1 = push_rel (LocalAssum (name, var.utj_val)) env in let sigma, j' = execute env1 sigma c2 in - sigma, judge_of_abstraction env1 name var j' + sigma, judge_of_abstraction env1 name.binder_name var j' | Prod (name,c1,c2) -> let sigma, j = execute env sigma c1 in let sigma, varj = type_judgment env sigma j in - let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in + let name = check_binder_annot varj.utj_type name in + let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in let sigma, j' = execute env1 sigma c2 in let sigma, varj' = type_judgment env1 sigma j' in - sigma, judge_of_product env name varj varj' + sigma, judge_of_product env name.binder_name varj varj' | LetIn (name,c1,c2,c3) -> let sigma, j1 = execute env sigma c1 in let sigma, j2 = execute env sigma c2 in let sigma, j2 = type_judgment env sigma j2 in let sigma, _ = judge_of_cast env sigma j1 DEFAULTcast j2 in + let name = check_binder_annot j2.utj_type name in let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in let sigma, j3 = execute env1 sigma c3 in - sigma, judge_of_letin env name j1 j2 j3 + sigma, judge_of_letin env name.binder_name j1 j2 j3 | Cast (c,k,t) -> let sigma, cj = execute env sigma c in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1ea16bbf34..f68820429b 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -39,13 +39,14 @@ val solve_evars : env -> evar_map -> constr -> evar_map * constr (** Raise an error message if incorrect elimination for this inductive (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> - unit + Sorts.relevance (** Raise an error message if bodies have types not unifiable with the expected ones *) val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> - Names.Name.t array -> types array -> unsafe_judgment array -> evar_map + Names.Name.t Context.binder_annot array -> types array -> unsafe_judgment array -> evar_map +val judge_of_sprop : unsafe_judgment val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment val judge_of_apply : env -> evar_map -> unsafe_judgment -> unsafe_judgment array -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3de8c381d0..9ba51dcfa9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -13,6 +13,7 @@ open Pp open Util open Names open Constr +open Context open Termops open Environ open EConstr @@ -103,13 +104,13 @@ let occur_meta_evd sigma mv c = let abstract_scheme env evd c l lname_typ = let mkLambda_name env (n,a,b) = - mkLambda (named_hd env evd a n, a, b) + mkLambda (map_annot (named_hd env evd a) n, a, b) in List.fold_left2 (fun (t,evd) (locc,a) decl -> - let na = RelDecl.get_name decl in + let na = RelDecl.get_annot decl in let ta = RelDecl.get_type decl in - let na = match EConstr.kind evd a with Var id -> Name id | _ -> na in + let na = match EConstr.kind evd a with Var id -> {na with binder_name=Name id} | _ -> na in (* [occur_meta ta] test removed for support of eelim/ecase but consequences are unclear... if occur_meta ta then error "cannot find a type for the generalisation" @@ -117,7 +118,7 @@ let abstract_scheme env evd c l lname_typ = if occur_meta evd a then mkLambda_name env (na,ta,t), evd else let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in - mkLambda_name env (na,ta,t'), evd') + mkLambda_name env (na,ta,t'), evd') (c,evd) (List.rev l) lname_typ @@ -561,8 +562,8 @@ let is_rigid_head sigma flags t = | Ind (i,u) -> true | Construct _ | Int _ -> true | Fix _ | CoFix _ -> true - | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod (_, _, _) - | Lambda (_, _, _) | LetIn (_, _, _, _) | App (_, _) | Case (_, _, _, _) + | Rel _ | Var _ | Meta _ | Evar _ | Sort _ | Cast (_, _, _) | Prod _ + | Lambda _ | LetIn _ | App (_, _) | Case (_, _, _, _) | Proj (_, _) -> false (* Why aren't Prod, Sort rigid heads ? *) let force_eqs c = @@ -662,7 +663,7 @@ let is_eta_constructor_app env sigma ts f l1 term = let mib = lookup_mind (fst ind) env in (match mib.Declarations.mind_record with | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite && - let (_, projs, _) = info.(i) in + let (_, projs, _, _) = info.(i) in Array.length projs == Array.length l1 - mib.Declarations.mind_nparams -> (* Check that the other term is neutral *) is_neutral env sigma ts term @@ -782,14 +783,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e with e when CErrors.noncritical e -> error_cannot_unify curenv sigma (m,n)) - | Lambda (na,t1,c1), Lambda (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} + | Lambda (na,t1,c1), Lambda (__,t2,c2) -> + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 - | Prod (na,t1,c1), Prod (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} + | Prod (na,t1,c1), Prod (_,t2,c2) -> + unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 - | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN - | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) + | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN + | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (* Fast path for projections. *) | Proj (p1,c1), Proj (p2,c2) when Constant.equal @@ -800,11 +801,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e unify_not_same_head curenvnb pb opt substn cM cN) (* eta-expansion *) - | Lambda (na,t1,c1), _ when flags.modulo_eta -> - unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn + | Lambda (na,t1,c1), _ when flags.modulo_eta -> + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn c1 (mkApp (lift 1 cN,[|mkRel 1|])) - | _, Lambda (na,t2,c2) when flags.modulo_eta -> - unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn + | _, Lambda (na,t2,c2) when flags.modulo_eta -> + unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn (mkApp (lift 1 cM,[|mkRel 1|])) c2 (* For records *) @@ -1775,7 +1776,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = matchrec c with ex when precatchable_exception ex -> iter_fail matchrec lf) - | LetIn(_,c1,_,c2) -> + | LetIn(_,c1,_,c2) -> (try matchrec c1 with ex when precatchable_exception ex -> @@ -1783,13 +1784,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = | Proj (p,c) -> matchrec c - | Fix(_,(_,types,terms)) -> + | Fix(_,(_,types,terms)) -> (try iter_fail matchrec types with ex when precatchable_exception ex -> iter_fail matchrec terms) - | CoFix(_,(_,types,terms)) -> + | CoFix(_,(_,types,terms)) -> (try iter_fail matchrec types with ex when precatchable_exception ex -> @@ -1860,13 +1861,13 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = | Proj (p,c) -> matchrec c - | LetIn(_,c1,_,c2) -> + | LetIn(_,c1,_,c2) -> bind (matchrec c1) (matchrec c2) - | Fix(_,(_,types,terms)) -> + | Fix(_,(_,types,terms)) -> bind (bind_iter matchrec types) (bind_iter matchrec terms) - | CoFix(_,(_,types,terms)) -> + | CoFix(_,(_,types,terms)) -> bind (bind_iter matchrec types) (bind_iter matchrec terms) | Prod (_,t,c) -> diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index ff528bd2cf..62e9e477f7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -13,6 +13,7 @@ open Names open Declarations open Term open Constr +open Context open Vars open Environ open Inductive @@ -31,10 +32,12 @@ module NamedDecl = Context.Named.Declaration let crazy_type = mkSet 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) - | Name _ -> res + let (name,dom,codom) = destProd (whd_all env t) in + let name = map_annot (function + | Anonymous -> Name (Id.of_string "x") + | Name _ as na -> na) name + in + (name,dom,codom) exception Find_at of int @@ -138,6 +141,8 @@ and nf_whd env sigma whd typ = let dom = nf_vtype env sigma (dom p) in let name = Name (Id.of_string "x") in let vc = reduce_fun (nb_rel env) (codom p) in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr dom) in + let name = make_annot name r 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 @@ -307,6 +312,8 @@ and nf_predicate env sigma ind mip params v pT = 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 let dom = mkApp(mkIndU ind,Array.append params rargs) in + let r = Inductive.relevance_of_inductive env (fst ind) in + let name = make_annot name r in let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in mkLambda(name,dom,body) | _ -> assert false @@ -317,7 +324,7 @@ and nf_args env sigma vargs ?from:(f=0) t = let args = Array.init len (fun i -> - let _,dom,codom = decompose_prod env !t in + let _,dom,codom = decompose_prod env !t in let c = nf_val env sigma (arg vargs (f+i)) dom in t := subst1 c codom; c) in !t,args @@ -328,7 +335,7 @@ and nf_bargs env sigma b ofs t = let args = Array.init len (fun i -> - let _,dom,codom = decompose_prod env !t in + let _,dom,codom = decompose_prod env !t in let c = nf_val env sigma (bfield b (i+ofs)) dom in t := subst1 c codom; c) in args @@ -353,14 +360,17 @@ and nf_fix env sigma f = let vb, vt = reduce_fix k f in let ndef = Array.length vt in let ft = Array.map (fun v -> nf_val env sigma v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in - (* Third argument of the tuple is ignored by push_rec_types *) - let env = push_rec_types (name,ft,ft) env in + let name = Name (Id.of_string "Ffix") in + let names = Array.map (fun t -> + make_annot name @@ + Retyping.relevance_of_type env sigma (EConstr.of_constr t)) ft in + (* Body argument of the tuple is ignored by push_rec_types *) + let env = push_rec_types (names,ft,ft) env in (* We lift here because the types of arguments (in tt) will be evaluated in an environment where the fixpoints have been pushed *) let norm_vb v t = nf_fun env sigma v (lift ndef t) in let fb = Util.Array.map2 norm_vb vb ft in - mkFix ((rec_args,init),(name,ft,fb)) + mkFix ((rec_args,init),(names,ft,fb)) and nf_fix_app env sigma f vargs = let fd = nf_fix env sigma f in @@ -373,12 +383,14 @@ and nf_cofix env sigma cf = let init = current_cofix cf in let k = nb_rel env in let vb,vt = reduce_cofix k cf in - let ndef = Array.length vt in let cft = Array.map (fun v -> nf_val env sigma v crazy_type) vt in - let name = Array.init ndef (fun _ -> (Name (Id.of_string "Fcofix"))) in - let env = push_rec_types (name,cft,cft) env in + let name = Name (Id.of_string "Fcofix") in + let names = Array.map (fun t -> + make_annot name @@ + Retyping.relevance_of_type env sigma (EConstr.of_constr t)) cft in + let env = push_rec_types (names,cft,cft) env in let cfb = Util.Array.map2 (fun v t -> nf_val env sigma v t) vb cft in - mkCoFix (init,(name,cft,cfb)) + mkCoFix (init,(names,cft,cfb)) let cbv_vm env sigma c t = if Termops.occur_meta sigma c then |