diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 56 |
1 files changed, 36 insertions, 20 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 1b396d57ba..77339aef44 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -402,20 +402,33 @@ let extract_level env evd min tys = sign_level env evd ((Anonymous, None, concl) :: ctx)) tys in sup_list min sorts +let is_flexible_sort evd u = + match Univ.Universe.level u with + | Some l -> Evd.is_flexible_level evd l + | None -> false + let inductive_levels env evdref poly arities inds = - let destarities = List.map (Reduction.dest_arity env) arities in - let levels = List.map (fun (ctx,a) -> + let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in + let levels = List.map (fun (x,(ctx,a)) -> if a = Prop Null then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = CList.split3 - (List.map2 (fun (_,tys,_) (ctx,du) -> + (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> let len = List.length tys in + let minlev = Sorts.univ_of_sort du in let minlev = if len > 1 && not (is_impredicative env du) then - Univ.type0_univ - else Univ.type0m_univ + Univ.sup minlev Univ.type0_univ + else minlev + in + let minlev = + (** Indices contribute. *) + if Indtypes.is_indices_matter () && List.length ctx > 0 then ( + let ilev = sign_level env !evdref ctx in + Univ.sup ilev minlev) + else minlev in let clev = extract_level env !evdref minlev tys in (clev, minlev, len)) inds destarities) @@ -425,32 +438,25 @@ let inductive_levels env evdref poly arities inds = let levels' = Universes.solve_constraints_system (Array.of_list levels) (Array.of_list cstrs_levels) (Array.of_list min_levels) in - let evd = - CList.fold_left3 (fun evd cu (ctx,du) len -> + let evd, arities = + CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len -> if is_impredicative env du then (** Any product is allowed here. *) - evd + evd, arity :: arities else (** If in a predicative sort, or asked to infer the type, we take the max of: - indices (if in indices-matter mode) - constructors - Type(1) if there is more than 1 constructor *) - let evd = - (** Indices contribute. *) - if Indtypes.is_indices_matter () && List.length ctx > 0 then ( - let ilev = sign_level env !evdref ctx in - Evd.set_leq_sort env evd (Type ilev) du) - else evd - in (** Constructors contribute. *) let evd = if Sorts.is_set du then if not (Evd.check_leq evd cu Univ.type0_univ) then raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) else evd - else - Evd.set_leq_sort env evd (Type cu) du + else evd + (* Evd.set_leq_sort env evd (Type cu) du *) in let evd = if len >= 2 && Univ.is_type0m_univ cu then @@ -459,9 +465,19 @@ let inductive_levels env evdref poly arities inds = land in Prop directly (no informative arguments as well). *) Evd.set_leq_sort env evd (Prop Pos) du else evd - in evd) - !evdref (Array.to_list levels') destarities sizes - in evdref := evd; arities + in + (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *) + let duu = Sorts.univ_of_sort du in + let evd = + if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then + if is_flexible_sort evd duu then + Evd.set_eq_sort env evd (Prop Null) du + else evd + else Evd.set_eq_sort env evd (Type cu) du + in + (evd, arity :: arities)) + (!evdref,[]) (Array.to_list levels') destarities sizes + in evdref := evd; List.rev arities let check_named (loc, na) = match na with | Name _ -> () |