Skip to content

Commit

Permalink
pretype template poly as though sort poly restricted to above_prop
Browse files Browse the repository at this point in the history 
This allows us to stop using posthoc refresh_template
  • Loading branch information
@SkySkimmer
SkySkimmer committed Dec 19, 2024
1 parent e722755 commit b06c0df
Show file tree
Hide file tree
Showing 2 changed files with 100 additions and 47 deletions.
144 changes: 97 additions & 47 deletions pretyping/pretyping.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -929,25 +929,50 @@ struct
| CtorType of Declarations.template_universes * types
| IndType of Declarations.template_universes * rel_context * Sorts.t

let get_template_arity env ind ctoropt =
let get_template_arity env sigma ind ctoropt =
let mib, mip = Inductive.lookup_mind_specif env ind in
let template = match mib.mind_template with
| None -> assert false
| Some t -> t
in
let type_after_params = match ctoropt with
let sigma, quality, type_after_params = match ctoropt with
| None -> begin match mip.mind_arity with
| RegularArity _ -> assert false
| TemplateArity { template_level = s } ->
let ctx = List.rev @@ List.skipn (List.length mib.mind_params_ctxt) @@
List.rev mip.mind_arity_ctxt
in
IndType (template, EConstr.of_rel_context ctx, s)
let sigma, quality = match s with
| SProp | Prop | Set -> sigma, None
| QSort _ -> assert false
| Type u ->
(* if all template levels are instantiated to Prop, do we get Prop? *)
let template_levels = Univ.ContextSet.levels template.template_context in
if List.exists (fun (u,n) -> n > 0 || not (Univ.Level.Set.mem u template_levels))
(Univ.Universe.repr u)
then sigma, None
else
let sigma, q = Evd.new_quality_variable sigma in
(* make q in cumulativity with Prop/Type *)
let sigma =
Evd.set_leq_sort env sigma
ESorts.prop
(ESorts.make (Sorts.qsort q Univ.Universe.type0))
in
(* don't use the qvar for non used univs
eg with "Ind (A:Type@{u}) (B:Type@{v}) : Type@{u}"
"Ind True nat" should be Prop *)
let used_template_levels =
Univ.Level.Set.inter template_levels (Univ.Universe.levels u)
in
sigma, Some (used_template_levels,q)
in
sigma, quality, IndType (template, EConstr.of_rel_context ctx, s)
end
| Some ctor ->
let ctyp = mip.mind_user_lc.(ctor-1) in
let _, ctyp = Term.decompose_prod_n_decls (List.length mib.mind_params_ctxt) ctyp in
CtorType (template, EConstr.of_constr ctyp)
sigma, None, CtorType (template, EConstr.of_constr ctyp)
in
let rec aux is_template (params:Constr.rel_context) = match is_template, params with
| _, LocalDef (na,v,t) :: params ->
Expand All @@ -970,20 +995,26 @@ struct
let codom = aux is_template params in
TemplateArg (EConstr.of_binder_annot na, EConstr.of_rel_context ctx, u, codom)
in
aux template.template_param_arguments (List.rev mib.mind_params_ctxt)
let res = aux template.template_param_arguments (List.rev mib.mind_params_ctxt) in
sigma, quality, res

let enforce_template_csts sigma bound csts =
(* maybe could be smarter when something becomes Prop *)
let bound = Univ.Level.Map.map (fun u -> TemplateUniv (Univ.Universe.make u)) bound in
let bound = Univ.Level.Map.map (fun u -> TemplateUniv u) bound in
let csts = Inductive.instantiate_template_constraints bound csts in
Evd.add_constraints sigma csts

let template_sort boundus (s:Sorts.t) =
let template_sort qopt boundus (s:Sorts.t) =
match s with
| SProp | Prop | Set -> ESorts.make s
| Type u ->
let u = Univ.subst_univs_level_universe boundus u in
ESorts.make (Sorts.sort_of_univ u)
let subst_fn u = Univ.Level.Map.find_opt u boundus in
let u = UnivSubst.subst_univs_universe subst_fn u in
let s = match qopt with
| None -> Sorts.sort_of_univ u
| Some (_,q) -> Sorts.qsort q u
in
ESorts.make s
| QSort (q,u) -> assert false

let bind_template_univ ~domu u bound =
Expand All @@ -992,53 +1023,85 @@ struct
| Some u' -> CErrors.anomaly Pp.(str "non linear template univ"))
bound

let rec finish_template sigma boundus = function
let rec finish_template qopt sigma boundus = function
| CtorType (csts, typ) ->
let sigma = enforce_template_csts sigma boundus csts in
sigma, typ
| IndType (csts, ctx, s) ->
let sigma = enforce_template_csts sigma boundus csts in
let s = template_sort boundus s in
let s = template_sort qopt boundus s in
sigma, mkArity (ctx, s)
| DefParam (na, v, t, codom) ->
let sigma, codom = finish_template sigma boundus codom in
let sigma, codom = finish_template qopt sigma boundus codom in
sigma, mkLetIn (na,v,t,codom)
| NonTemplateArg (na,dom,codom) ->
let sigma, codom = finish_template sigma boundus codom in
let sigma, codom = finish_template qopt sigma boundus codom in
sigma, mkProd (na,dom,codom)
| TemplateArg (na,ctx,domu,codom) ->
(* partially applied template: use the global univ level *)
let boundus = bind_template_univ ~domu domu boundus in
let sigma, codom = finish_template sigma boundus codom in
(* partially applied template: use the global univ level, force quality = Type *)
let sigma = match qopt with
| Some (used_template_levels,q) when Univ.Level.Set.mem domu used_template_levels ->
Evd.add_quconstraints sigma
(Sorts.QConstraints.singleton (QVar q, Equal, QConstant QType),
Univ.Constraints.empty)
| _ -> sigma
in
let boundus = bind_template_univ ~domu (Univ.Universe.make domu) boundus in
let sigma, codom = finish_template qopt sigma boundus codom in
let s = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make domu in
sigma, mkProd (na,mkArity (ctx,s),codom)

let rec apply_template pretype_arg arg_state sigma body subst boundus todoargs typ =
let rec apply_template qopt pretype_arg arg_state env sigma body subst boundus todoargs typ =
match todoargs, typ with
| [], _
| _, (CtorType _ | IndType _) ->
let sigma, typ = finish_template sigma boundus typ in
let sigma, typ = finish_template qopt sigma boundus typ in
sigma, body, subst, typ, arg_state, todoargs
| _, DefParam (_, v, _, codom) ->
(* eager subst may be inefficient but template inductives with
letin params are hopefully rare enough that it doesn't
matter *)
let v = Vars.esubst Vars.lift_substituend subst v in
let subst = Esubst.subs_cons (Vars.make_substituend v) subst in
apply_template pretype_arg arg_state sigma body subst boundus todoargs codom
apply_template qopt pretype_arg arg_state env sigma body subst boundus todoargs codom
| arg :: todoargs, NonTemplateArg (na, dom, codom) ->
let dom = Vars.esubst Vars.lift_substituend subst dom in
let sigma, arg_state, body, arg = pretype_arg sigma arg_state body arg na dom in
let sigma, arg_state, body, arg = pretype_arg env sigma arg_state body arg na.binder_name dom in
let subst = Esubst.subs_cons (Vars.make_substituend arg) subst in
apply_template pretype_arg arg_state sigma body subst boundus todoargs codom
apply_template qopt pretype_arg arg_state env sigma body subst boundus todoargs codom
| arg :: todoargs, TemplateArg (na, ctx, domu, codom) ->
let sigma, u = Evd.new_univ_level_variable UState.univ_flexible_alg sigma in
let s = ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make u in
let s = match qopt with
| Some (used_template_levels, q) when Univ.Level.Set.mem domu used_template_levels ->
ESorts.make @@ Sorts.qsort q @@ Univ.Universe.make u
| _ -> ESorts.make @@ Sorts.sort_of_univ @@ Univ.Universe.make u
in
let dom = Vars.esubst Vars.lift_substituend subst (mkArity (ctx, s)) in
let sigma, arg_state, body, arg = pretype_arg sigma arg_state body arg na dom in
let sigma, arg_state, body, arg = pretype_arg env sigma arg_state body arg na.binder_name dom in
let u =
(* get an algebraic instead of the generated variable *)
let s =
try
snd @@ Reductionops.dest_arity !!env sigma @@ Retyping.get_type_of !!env sigma arg
with Reduction.NotArity ->
(* delayed constraints prevent getting the sort from retyping *)
s
in
match ESorts.kind sigma s with
| SProp -> assert false
| Prop ->
(* putting type0 here doesn't prevent getting Prop
because the return type will be "qsort q type0" *)
Univ.Universe.type0
| Set -> Univ.Universe.type0
| Type u -> u
| QSort (_,u) ->
(* quality guaranteed = Option.get qopt *)
u
in
let boundus = bind_template_univ ~domu u boundus in
let subst = Esubst.subs_cons (Vars.make_substituend arg) subst in
apply_template pretype_arg arg_state sigma body subst boundus todoargs codom
apply_template qopt pretype_arg arg_state env sigma body subst boundus todoargs codom

let pretype_app self (f, args) =
fun ?loc ~flags tycon env sigma ->
Expand Down Expand Up @@ -1081,19 +1144,7 @@ struct
with Not_found -> []
else []
in
let refresh_template env sigma resj =
(* apply_rec on a template poly head produces the type using the default (global) universes,
we retype afterwards to get the actual type *)
match EConstr.kind sigma resj.uj_val with
| App (f,args) ->
if Termops.is_template_polymorphic_ind !!env sigma f then
let c = mkApp (f, args) in
let t = Retyping.get_type_of !!env sigma c in
sigma, make_judge c (* use this for keeping evars: resj.uj_val *) t
else sigma, resj
| _ -> sigma, resj
in
let pretype_arg env sigma (n, val_before_bidi, bidiargs, candargs) trace body arg na tycon =
let pretype_arg ?(trace=Coercion.empty_coercion_trace) env sigma (n, val_before_bidi, bidiargs, candargs) body arg na tycon =
(* trace is the coercion trace from coercing the body to funclass *)
let bidi = n >= nargs_before_bidi in
let sigma, c, bidiargs =
Expand Down Expand Up @@ -1152,39 +1203,39 @@ struct
sigma, body, na, c1, Esubst.subs_id 0, c2, trace
in
let sigma, arg_state, body, arg =
pretype_arg env sigma arg_state trace body c na.binder_name c1
pretype_arg env sigma arg_state ~trace body c na.binder_name c1
in
let subs = Esubst.subs_cons (Vars.make_substituend arg) subs in
apply_rec env sigma arg_state body (subs, c2) rest
in
let body = (Coercion.start_app_body sigma fj.uj_val) in
let template_arity = match EConstr.kind sigma fj.uj_val with
let sigma, template_arity = match EConstr.kind sigma fj.uj_val with
| Ind (ind,u) | Construct ((ind,_),u) as k
when EInstance.is_empty u && Environ.template_polymorphic_ind ind !!env ->
let ctoropt = match k with
| Ind _ -> None
| Construct ((_,ctor),_) -> Some ctor
| _ -> assert false
in
Some (get_template_arity !!env ind ctoropt)
| _ -> None
let sigma, quality, arity = get_template_arity !!env sigma ind ctoropt in
sigma, Some (quality, arity)
| _ -> sigma, None
in
let arg_state = (0,body,[],candargs) in
let subst = Esubst.subs_id 0 in
let typ = fj.uj_type in
let sigma, body, subst, typ, arg_state, args =
match template_arity with
| None -> sigma, body, subst, typ, arg_state, args
| Some typ ->
let pretype_arg sigma arg_state body arg na dom =
pretype_arg env sigma arg_state Coercion.empty_coercion_trace body arg na.binder_name dom
| Some (q,typ) ->
let pretype_arg env sigma arg_state body arg na tycon =
pretype_arg env sigma arg_state body arg na tycon
in
apply_template pretype_arg arg_state sigma body subst Univ.Level.Map.empty args typ
apply_template q pretype_arg arg_state env sigma body subst Univ.Level.Map.empty args typ
in
let sigma, resj, val_before_bidi, bidiargs =
apply_rec env sigma arg_state body (subst,typ) args
in
let sigma, resj = refresh_template env sigma resj in
let sigma, resj, otrace = inh_conv_coerce_to_tycon ?loc ~flags env sigma resj tycon in
let refine_arg (sigma,t) (newarg,ty,origarg,trace) =
(* Refine an argument (originally `origarg`) represented by an evar
Expand Down Expand Up @@ -1212,7 +1263,6 @@ struct
| None -> resj
| Some trace ->
let resj = { resj with uj_val = t } in
let sigma, resj = refresh_template env sigma resj in
{ resj with uj_val = Coercion.reapply_coercions sigma trace t }
in
(sigma, resj)
Expand Down
3 changes: 3 additions & 0 deletions test-suite/success/Template.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,9 @@ Module TemplateAlg.

Check foo True nat : Prop.

Check fun A => foo A nat : Prop.
Fail Check fun A:Set => foo A nat : Prop.

Universes u v.

Axiom U : Type@{u}.
Expand Down

0 comments on commit b06c0df

Please sign in to comment.