diff options
61 files changed, 353 insertions, 336 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index a890f2cef..4846a9af8 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -33,11 +33,10 @@ open Names (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type sorts = - | Prop of contents (** Prop and Set *) - | Type of Univ.universe (** Type *) + | Prop + | Set + | Type of Univ.universe (** {6 The sorts family of CCI. } *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 916934a81..bcb71fe55 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -107,11 +107,11 @@ let rec sorts_of_constr_args env t = (* Prop and Set are small *) let is_small_sort = function - | Prop _ -> true + | Prop | Set -> true | _ -> false let is_logic_sort = function -| Prop Null -> true +| Prop -> true | _ -> false (* [infos] is a sequence of pair [islogic,issmall] for each type in @@ -186,10 +186,10 @@ let check_predicativity env s small level = (* (universes env) in *) if not (Univ.check_leq (universes env) level u) then failwith "impredicative Type inductive type" - | Prop Pos, ImpredicativeSet -> () - | Prop Pos, _ -> + | Set, ImpredicativeSet -> () + | Set, _ -> if not small then failwith "impredicative Set inductive type" - | Prop Null,_ -> () + | Prop,_ -> () let sort_of_ind = function diff --git a/checker/inductive.ml b/checker/inductive.ml index e1c6b135d..b1edec556 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -101,7 +101,7 @@ let instantiate_params full t u args sign = substl subs ty let full_inductive_instantiate mib u params sign = - let dummy = Prop Null in + let dummy = Prop in let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) @@ -137,8 +137,8 @@ Remark: Set (predicative) is encoded as Type(0) let sort_as_univ = function | Type u -> u -| Prop Null -> Univ.type0m_univ -| Prop Pos -> Univ.type0_univ +| Prop -> Univ.type0m_univ +| Set -> Univ.type0_univ (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) (* in the domain or add [u |-> sup x su] if [u] is already mapped *) @@ -195,9 +195,9 @@ let instantiate_universes env ctx ar argsorts = let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) - if Univ.is_type0m_univ level then Prop Null + if Univ.is_type0m_univ level then Prop (* Non singleton type not containing types are interpretable in Set *) - else if Univ.is_type0_univ level then Prop Pos + else if Univ.is_type0_univ level then Set (* This is a Type with constraints *) else Type level in @@ -226,8 +226,8 @@ let type_of_inductive env mip = (* The max of an array of universes *) let cumulate_constructor_univ u = function - | Prop Null -> u - | Prop Pos -> Univ.sup Univ.type0_univ u + | Prop -> u + | Set -> Univ.sup Univ.type0_univ u | Type u' -> Univ.sup u u' let max_inductive_sort = diff --git a/checker/print.ml b/checker/print.ml index fc9cd687e..247c811f8 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -57,8 +57,8 @@ let print_pure_constr fmt csr = fprintf fmt "Proj(%a,@,@[%a@])" sp_con_display (Projection.constant p) pp_term c and pp_sort fmt = function - | Prop(Pos) -> pp_print_string fmt "Set" - | Prop(Null) -> pp_print_string fmt "Prop" + | Set -> pp_print_string fmt "Set" + | Prop -> pp_print_string fmt "Prop" | Type u -> fprintf fmt "Type(%a)" chk_pp (Univ.pr_uni u) and pp_name fmt = function diff --git a/checker/reduction.ml b/checker/reduction.ml index 4e508dc77..16c701213 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -210,29 +210,26 @@ let convert_constructors let sort_cmp env univ pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible - | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible - | (Prop c1, Type u) -> + | Prop, Prop | Set, Set -> () + | Prop, (Set | Type _) | Set, Type _ -> + if not (pb = CUMUL) then raise NotConvertible + | Type u1, Type u2 -> + (** FIXME: handle type-in-type option here *) + if (* snd (engagement env) == StratifiedType && *) + not (match pb with - CUMUL -> () - | _ -> raise NotConvertible) - | (Type u1, Type u2) -> - (** FIXME: handle type-in-type option here *) - if (* snd (engagement env) == StratifiedType && *) - not - (match pb with - | CONV -> Univ.check_eq univ u1 u2 - | CUMUL -> Univ.check_leq univ u1 u2) - then begin - if !Flags.debug then begin - let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( - str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() - ++ Univ.pr_universes univ) - end; - raise NotConvertible - end - | (_, _) -> raise NotConvertible + | CONV -> Univ.check_eq univ u1 u2 + | CUMUL -> Univ.check_leq univ u1 u2) + then begin + if !Flags.debug then begin + let op = match pb with CONV -> "=" | CUMUL -> "<=" in + Format.eprintf "sort_cmp: @[%a@]\n%!" Pp.pp_with Pp.( + str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() + ++ Univ.pr_universes univ) + end; + raise NotConvertible + end + | Set, Prop | Type _, (Prop | Set) -> raise NotConvertible let rec no_arg_available = function | [] -> true diff --git a/checker/term.ml b/checker/term.ml index 509634bdb..d84491b38 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -20,15 +20,15 @@ open Cic (* Sorts. *) let family_of_sort = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type _ -> InType let family_equal = (==) let sort_of_univ u = - if Univ.is_type0m_univ u then Prop Null - else if Univ.is_type0_univ u then Prop Pos + if Univ.is_type0m_univ u then Prop + else if Univ.is_type0_univ u then Set else Type u (********************************************************************) @@ -356,15 +356,11 @@ let rec isArity c = (* alpha conversion : ignore print names and casts *) let compare_sorts s1 s2 = match s1, s2 with -| Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> true - | Pos, Null -> false - | Null, Pos -> false - end +| Prop, Prop | Set, Set -> true | Type u1, Type u2 -> Univ.Universe.equal u1 u2 -| Prop _, Type _ -> false -| Type _, Prop _ -> false +| Prop, Set | Set, Prop -> false +| (Prop | Set), Type _ -> false +| Type _, (Prop | Set) -> false let eq_puniverses f (c1,u1) (c2,u2) = Univ.Instance.equal u1 u2 && f c1 c2 diff --git a/checker/typeops.ml b/checker/typeops.ml index 345ee5b8f..19ede4b9a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -103,11 +103,11 @@ let judge_of_apply env (f,funj) argjv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | _, Prop -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | (Prop | Set), Set -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | Type u1, Set -> if engagement env = ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -115,11 +115,11 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Univ.sup u1 Univ.type0_univ) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Univ.sup Univ.type0_univ u2) + | Set, Type u2 -> Type (Univ.sup Univ.type0_univ u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | Prop, Type _ -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Univ.sup u1 u2) + | Type u1, Type u2 -> Type (Univ.sup u1 u2) (* Type of a type cast *) @@ -239,7 +239,7 @@ let type_fixpoint env lna lar lbody vdefj = let rec execute env cstr = match cstr with (* Atomic terms *) - | Sort (Prop _) -> judge_of_prop + | Sort (Prop | Set) -> judge_of_prop | Sort (Type u) -> judge_of_type u diff --git a/checker/values.ml b/checker/values.ml index 4f28d6e44..88cdb644d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli +MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli *) @@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) -let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|] +let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|] let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] diff --git a/dev/ci/user-overlays/07863-rm-sorts-contents.sh b/dev/ci/user-overlays/07863-rm-sorts-contents.sh new file mode 100644 index 000000000..374a61484 --- /dev/null +++ b/dev/ci/user-overlays/07863-rm-sorts-contents.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7863" ] || [ "$CI_BRANCH" = "rm-sorts-contents" ]; then + Elpi_CI_BRANCH=fix-sorts-contents + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/ci/user-overlays/07906-univs-of-constr.sh b/dev/ci/user-overlays/07906-univs-of-constr.sh new file mode 100644 index 000000000..071665087 --- /dev/null +++ b/dev/ci/user-overlays/07906-univs-of-constr.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7906" ] || [ "$CI_BRANCH" = "univs-of-constr-noseff" ]; then + Equations_CI_BRANCH=fix-univs-of-constr + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git + + Elpi_CI_BRANCH=fix-universes-of-constr + Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 844ad9188..811abd67f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -301,8 +301,8 @@ let constr_display csr = incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ()) and sort_display = function - | Prop(Pos) -> "Prop(Pos)" - | Prop(Null) -> "Prop(Null)" + | Set -> "Set" + | Prop -> "Prop" | Type u -> univ_display u; "Type("^(string_of_int !cnt)^")" @@ -423,8 +423,8 @@ let print_pure_constr csr = Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u) and sort_display = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> open_hbox(); print_string "Type("; pp (pr_uni u); print_string ")"; close_box() diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 7589e5348..c8385da61 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -26,8 +26,8 @@ let print_vfix_app () = print_string "vfix_app" let print_vswith () = print_string "switch" let ppsort = function - | Prop(Pos) -> print_string "Set" - | Prop(Null) -> print_string "Prop" + | Set -> print_string "Set" + | Prop -> print_string "Prop" | Type u -> print_string "Type" diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 6810626ad..005ef1635 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -592,25 +592,14 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr env sigma c = +let universes_of_constr sigma c = let open Univ in - let open Declarations in let rec aux s c = match kind sigma c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e9d3e782b..913825a9f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1625f6fc8..0c044f20d 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -426,10 +426,6 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let restrict_evar evd evk filter ?src candidates = - let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in - Evd.declare_future_goal evk' evd, evk' - let new_pure_evar_full evd evi = let (evd, evk) = Evd.new_evar evd evi in let evd = Evd.declare_future_goal evk evd in @@ -547,11 +543,33 @@ let generalize_evar_over_rels sigma (ev,args) = type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential +| NoCandidatesLeft of Evar.t exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option exception Depends of Id.t +let set_of_evctx l = + List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l + +let filter_effective_candidates evd evi filter candidates = + let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in + List.filter (fun a -> Id.Set.subset (collect_vars evd a) ids) candidates + +let restrict_evar evd evk filter ?src candidates = + let evar_info = Evd.find_undefined evd evk in + let candidates = Option.map (filter_effective_candidates evd evar_info filter) candidates in + match candidates with + | Some [] -> raise (ClearDependencyError (*FIXME*)(Id.of_string "blah", (NoCandidatesLeft evk), None)) + | _ -> + let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in + (** Mark new evar as future goal, removing previous one, + circumventing Proofview.advance but making Proof.run_tactic catch these. *) + let future_goals = Evd.save_future_goals evd in + let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in + let evd = Evd.restore_future_goals evd future_goals in + (Evd.declare_future_goal evk' evd, evk') + let rec check_and_clear_in_constr env evdref err ids global c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of @@ -621,7 +639,9 @@ let rec check_and_clear_in_constr env evdref err ids global c = let origfilter = Evd.evar_filter evi in let filter = Evd.Filter.apply_subfilter origfilter filter in let evd = !evdref in - let (evd,_) = restrict_evar evd evk filter None in + let candidates = Evd.evar_candidates evi in + let candidates = Option.map (List.map EConstr.of_constr) candidates in + let (evd,_) = restrict_evar evd evk filter candidates in evdref := evd; Evd.existential_value0 !evdref ev diff --git a/engine/evarutil.mli b/engine/evarutil.mli index db638be9e..8ce1b625f 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -65,9 +65,6 @@ val new_type_evar : val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr -val restrict_evar : evar_map -> Evar.t -> Filter.t -> - ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t - (** Polymorphic constants *) val new_global : evar_map -> GlobRef.t -> evar_map * constr @@ -231,9 +228,18 @@ raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential +| NoCandidatesLeft of Evar.t exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option +(** Restrict an undefined evar according to a (sub)filter and candidates. + The evar will be defined if there is only one candidate left, +@raise ClearDependencyError NoCandidatesLeft if the filter turns the candidates + into an empty list. *) + +val restrict_evar : evar_map -> Evar.t -> Filter.t -> + ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t + val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types -> Id.Set.t -> evar_map * named_context_val * types diff --git a/engine/evd.ml b/engine/evd.ml index 714a0b645..761ae7983 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -171,6 +171,8 @@ let evar_context evi = named_context_of_val evi.evar_hyps let evar_filtered_context evi = Filter.filter_list (evar_filter evi) (evar_context evi) +let evar_candidates evi = evi.evar_candidates + let evar_hyps evi = evi.evar_hyps let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with @@ -620,6 +622,7 @@ let merge_universe_context evd uctx' = let set_universe_context evd uctx' = { evd with universes = uctx' } +(* TODO: make unique *) let add_conv_pb ?(tail=false) pb d = if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -852,7 +855,7 @@ let normalize_universe_instance evd l = let normalize_sort evars s = match s with - | Prop _ -> s + | Prop | Set -> s | Type u -> let u' = normalize_universe evars u in if u' == u then s else Type u' diff --git a/engine/evd.mli b/engine/evd.mli index d166fd804..64db70451 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -113,6 +113,7 @@ val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body +val evar_candidates : evar_info -> constr list option val evar_filter : evar_info -> Filter.t val evar_env : evar_info -> env val evar_filtered_env : evar_info -> env @@ -243,7 +244,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t (** Restrict an undefined evar into a new evar by filtering context and - possibly limiting the instances to a set of candidates *) + possibly limiting the instances to a set of candidates (candidates + are filtered according to the filter) *) val is_restricted_evar : evar_info -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) diff --git a/engine/namegen.ml b/engine/namegen.ml index 23c691139..978f33b68 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -137,8 +137,9 @@ let lowercase_first_char id = (* First character of a constr *) s ^ Unicode.lowercase_first_char s' let sort_hdchar = function - | Prop(_) -> "P" - | Type(_) -> "T" + | Prop -> "P" + | Set -> "S" + | Type _ -> "T" let hdchar env sigma c = let rec hdrec k c = diff --git a/engine/termops.ml b/engine/termops.ml index 2db2e07bf..2b179c43b 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -25,8 +25,8 @@ module CompactedDecl = Context.Compacted.Declaration (* Sorts and sort family *) let print_sort = function - | Prop Pos -> (str "Set") - | Prop Null -> (str "Prop") + | Set -> (str "Set") + | Prop -> (str "Prop") | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")") let pr_sort_family = function @@ -1162,15 +1162,14 @@ let is_template_polymorphic env sigma f = let base_sort_cmp pb s0 s1 = match (s0,s1) with - | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos (* Prop <= Set *) - | (Prop c1, Type u) -> pb == Reduction.CUMUL - | (Type u1, Type u2) -> true - | _ -> false + | Prop, Prop | Set, Set | Type _, Type _ -> true + | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL + | Set, Prop | Type _, Prop | Type _, Set -> false let rec is_Prop sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Null -> true + | Prop -> true | _ -> false end | Cast (c,_,_) -> is_Prop sigma c @@ -1179,7 +1178,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with let rec is_Set sigma c = match EConstr.kind sigma c with | Sort u -> begin match EConstr.ESorts.kind sigma u with - | Prop Pos -> true + | Set -> true | _ -> false end | Cast (c,_,_) -> is_Set sigma c diff --git a/engine/univops.ml b/engine/univops.ml index 3fd518490..7f9672f82 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -11,24 +11,13 @@ open Univ open Constr -let universes_of_constr env c = - let open Declarations in - let rec aux s c = +let universes_of_constr c = + let rec aux s c = match kind c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s diff --git a/engine/univops.mli b/engine/univops.mli index 0b37ab975..57a53597b 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -11,8 +11,8 @@ open Constr open Univ -(** The universes of monomorphic constants appear. *) -val universes_of_constr : Environ.env -> constr -> LSet.t +(** Return the set of all universes appearing in [constr]. *) +val universes_of_constr : constr -> LSet.t (** [restrict_universe_context (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e217b2cd..18d6c1a5b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -710,10 +710,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env (c, (tmp_scope, subscopes)) = + let mk_env id (c, (tmp_scope, subscopes)) map = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let gc = intern nenv c in - (gc, Some c) + try + let gc = intern nenv c in + Id.Map.add id (gc, Some c) map + with GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -725,7 +727,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | [pat] -> (glob_constr_of_cases_pattern pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in - let terms = Id.Map.map mk_env terms in + let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 6931fec03..3095ce148 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -236,8 +236,8 @@ open Util let pp_sort s = let open Sorts in match s with - | Prop Null -> str "Prop" - | Prop Pos -> str "Set" + | Prop -> str "Prop" + | Set -> str "Set" | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let rec pp_struct_const = function diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index f17313230..6677db2fd 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -511,7 +511,7 @@ let rec compile_lam env cenv lam sz cont = else comp_app compile_structured_constant compile_universe cenv (Const_ind ind) (Univ.Instance.to_array u) sz cont - | Lsort (Sorts.Prop _ as s) -> + | Lsort (Sorts.Prop | Sorts.Set as s) -> compile_structured_constant cenv (Const_sort s) sz cont | Lsort (Sorts.Type u) -> (* We represent universes as a global constant with local universes diff --git a/kernel/constr.ml b/kernel/constr.ml index e68f906ec..45812b5a1 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -130,8 +130,8 @@ let mkProp = Sort Sorts.prop let mkSet = Sort Sorts.set let mkType u = Sort (Sorts.Type u) let mkSort = function - | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *) - | Sorts.Prop Sorts.Pos -> mkSet + | Sorts.Prop -> mkProp (* Easy sharing *) + | Sorts.Set -> mkSet | s -> Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) @@ -260,17 +260,17 @@ let isSort c = match kind c with | _ -> false let rec isprop c = match kind c with - | Sort (Sorts.Prop _) -> true + | Sort (Sorts.Prop | Sorts.Set) -> true | Cast (c,_,_) -> isprop c | _ -> false let rec is_Prop c = match kind c with - | Sort (Sorts.Prop Sorts.Null) -> true + | Sort Sorts.Prop -> true | Cast (c,_,_) -> is_Prop c | _ -> false let rec is_Set c = match kind c with - | Sort (Sorts.Prop Sorts.Pos) -> true + | Sort Sorts.Set -> true | Cast (c,_,_) -> is_Set c | _ -> false diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9130b8778..584c1af03 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -130,11 +130,6 @@ where Remark: Set (predicative) is encoded as Type(0) *) -let sort_as_univ = let open Sorts in function -| Type u -> u -| Prop Null -> Universe.type0m -| Prop Pos -> Universe.type0 - (* Template polymorphism *) (* cons_subst add the mapping [u |-> su] in subst if [u] is not *) @@ -168,7 +163,7 @@ let make_subst env = (* arity is a global level which, at typing time, will be enforce *) (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in + let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) | LocalAssum (na,t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) @@ -236,8 +231,8 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args = (* The max of an array of universes *) let cumulate_constructor_univ u = let open Sorts in function - | Prop Null -> u - | Prop Pos -> Universe.sup Universe.type0 u + | Prop -> u + | Set -> Universe.sup Universe.type0 u | Type u' -> Universe.sup u u' let max_inductive_sort = diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index da4413a0a..3901cb9ce 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -116,7 +116,7 @@ let mk_ind_accu ind u = let mk_sort_accu s u = let open Sorts in match s with - | Prop _ -> mk_accu (Asort s) + | Prop | Set -> mk_accu (Asort s) | Type s -> let u = Univ.Instance.of_array u in let s = Univ.subst_instance_universe u s in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2c61b7a01..3228a155f 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -649,23 +649,19 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in if not (type_in_type env) then + let check_pb u0 u1 = + match pb with + | CUMUL -> check_leq univs u0 u1 + | CONV -> check_eq univs u0 u1 + in match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + | Prop, Prop | Set, Set -> () + | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible + | Set, Prop -> raise NotConvertible + | Set, Type u -> check_pb Univ.type0_univ u + | Type u, Prop -> raise NotConvertible + | Type u, Set -> check_pb u Univ.type0_univ + | Type u0, Type u1 -> check_pb u0 u1 let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -697,26 +693,23 @@ let infer_leq (univs, cstrs as cuniv) u u' = univs, Univ.Constraint.union cstrs cstrs' let infer_cmp_universes env pb s0 s1 univs = - let open Sorts in - if type_in_type env then univs + if type_in_type env + then univs else + let open Sorts in + let infer_pb u0 u1 = + match pb with + | CUMUL -> infer_leq univs u0 u1 + | CONV -> infer_eq univs u0 u1 + in match (s0,s1) with - | (Prop c1, Prop c2) when is_cumul pb -> - begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible - end - | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible - | (Prop c1, Type u) -> - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) - | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) + | Prop, Prop | Set, Set -> univs + | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs + | Set, Prop -> raise NotConvertible + | Set, Type u -> infer_pb Univ.type0_univ u + | Type u, Prop -> raise NotConvertible + | Type u, Set -> infer_pb u Univ.type0_univ + | Type u0, Type u1 -> infer_pb u0 u1 let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = diff --git a/kernel/sorts.ml b/kernel/sorts.ml index daeb90be7..a7bb08f5b 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -10,22 +10,21 @@ open Univ -type contents = Pos | Null - type family = InProp | InSet | InType type t = - | Prop of contents (* proposition types *) + | Prop + | Set | Type of Universe.t -let prop = Prop Null -let set = Prop Pos +let prop = Prop +let set = Set let type1 = Type type1_univ let univ_of_sort = function | Type u -> u - | Prop Pos -> Universe.type0 - | Prop Null -> Universe.type0m + | Set -> Universe.type0 + | Prop -> Universe.type0m let sort_of_univ u = if is_type0m_univ u then prop @@ -34,36 +33,34 @@ let sort_of_univ u = let compare s1 s2 = if s1 == s2 then 0 else - match s1, s2 with - | Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> 0 - | Pos, Null -> -1 - | Null, Pos -> 1 - end - | Type u1, Type u2 -> Universe.compare u1 u2 - | Prop _, Type _ -> -1 - | Type _, Prop _ -> 1 + match s1, s2 with + | Prop, Prop -> 0 + | Prop, _ -> -1 + | Set, Prop -> 1 + | Set, Set -> 0 + | Set, _ -> -1 + | Type u1, Type u2 -> Universe.compare u1 u2 + | Type _, _ -> -1 let equal s1 s2 = Int.equal (compare s1 s2) 0 let is_prop = function - | Prop Null -> true + | Prop -> true | Type u when Universe.equal Universe.type0m u -> true | _ -> false let is_set = function - | Prop Pos -> true + | Set -> true | Type u when Universe.equal Universe.type0 u -> true | _ -> false let is_small = function - | Prop _ -> true + | Prop | Set -> true | Type u -> is_small_univ u let family = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type u when is_type0m_univ u -> InProp | Type u when is_type0_univ u -> InSet | Type _ -> InType @@ -73,15 +70,11 @@ let family_equal = (==) open Hashset.Combine let hash = function -| Prop p -> - let h = match p with - | Pos -> 0 - | Null -> 1 - in - combinesmall 1 h -| Type u -> - let h = Univ.Universe.hash u in - combinesmall 2 h + | Prop -> combinesmall 1 0 + | Set -> combinesmall 1 1 + | Type u -> + let h = Univ.Universe.hash u in + combinesmall 2 h module List = struct let mem = List.memq @@ -101,7 +94,7 @@ module Hsorts = if u' == u then c else Type u' | s -> s let eq s1 s2 = match (s1,s2) with - | (Prop c1, Prop c2) -> c1 == c2 + | Prop, Prop | Set, Set -> true | (Type u1, Type u2) -> u1 == u2 |_ -> false diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 1bbde2608..cac6229b9 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -10,13 +10,12 @@ (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type family = InProp | InSet | InType type t = -| Prop of contents (** Prop and Set *) -| Type of Univ.Universe.t (** Type *) + | Prop + | Set + | Type of Univ.Universe.t val set : t val prop : t diff --git a/kernel/term.ml b/kernel/term.ml index b44e038e9..81e344e73 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -16,14 +16,11 @@ open Vars open Constr (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/term.mli b/kernel/term.mli index f651d1a58..4d340399d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -190,13 +190,10 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 34ed2afb2..7c0057696 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -69,7 +69,7 @@ let type_of_type u = mkType uu let type_of_sort = function - | Prop c -> type1 + | Prop | Set -> type1 | Type u -> type_of_type u (*s Type of a de Bruijn index. *) @@ -178,11 +178,11 @@ let type_of_apply env func funt argsv argstv = let sort_of_product env domsort rangsort = match (domsort, rangsort) with (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort + | (_, Prop) -> rangsort (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort + | ((Prop | Set), Set) -> rangsort (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> + | (Type u1, Set) -> if is_impredicative_set env then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort @@ -190,9 +190,9 @@ let sort_of_product env domsort rangsort = (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) Type (Universe.sup Universe.type0 u1) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) + | (Set, Type u2) -> Type (Universe.sup Universe.type0 u2) (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort + | (Prop, Type _) -> rangsort (* Product rule (Type_i,Type_i,Type_i) *) | (Type u1, Type u2) -> Type (Universe.sup u1 u2) @@ -481,10 +481,6 @@ let judge_of_prop = make_judge mkProp type1 let judge_of_set = make_judge mkSet type1 let judge_of_type u = make_judge (mkType u) (type_of_type u) -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 546f2d2b4..3b2abc777 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -43,7 +43,6 @@ val type1 : types val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment -val judge_of_prop_contents : Sorts.contents -> unsafe_judgment val judge_of_type : Universe.t -> unsafe_judgment (** {6 Type of a bound variable. } *) diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml index 61eb1dafd..c2bcd73ff 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml @@ -90,30 +90,50 @@ let rec post_canonize f = exception Parsing_error of string -let rec parse_string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string s) - | [< >] -> "" -and parse_string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) - | [< >] -> raise (Parsing_error "unterminated string") -and parse_skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> parse_skip_comment s - | [< >] -> [< >] -and parse_args = parser - | [< '' ' | '\n' | '\t'; s >] -> parse_args s - | [< ''#'; s >] -> parse_args (parse_skip_comment s) - | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s - | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s) - | [< >] -> [] +let buffer buf = + let ans = Buffer.contents buf in + let () = Buffer.clear buf in + ans + +let rec parse_string buf s = match Stream.next s with +| ' ' | '\n' | '\t' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string buf s +| exception Stream.Failure -> buffer buf + +and parse_string2 buf s = match Stream.next s with +| '"' -> buffer buf +| c -> + let () = Buffer.add_char buf c in + parse_string2 buf s +| exception Stream.Failure -> raise (Parsing_error "unterminated string") + +and parse_skip_comment s = match Stream.next s with +| '\n' -> () +| _ -> parse_skip_comment s +| exception Stream.Failure -> () + +and parse_args buf accu s = match Stream.next s with +| ' ' | '\n' | '\t' -> parse_args buf accu s +| '#' -> + let () = parse_skip_comment s in + parse_args buf accu s +| '"' -> + let str = parse_string2 buf s in + parse_args buf (str :: accu) s +| c -> + let () = Buffer.add_char buf c in + let str = parse_string buf s in + parse_args buf (str :: accu) s +| exception Stream.Failure -> accu let parse f = let c = open_in f in - let res = parse_args (Stream.of_channel c) in + let buf = Buffer.create 64 in + let res = parse_args buf [] (Stream.of_channel c) in close_in c; - res + List.rev res ;; (* Copy from minisys.ml, since we don't see that file here *) @@ -143,7 +163,7 @@ let process_cmd_line orig_dir proj args = error "Use \"-install none\" instead of \"-no-install\"" | "-custom" :: _ -> error "Use \"-extra[-phony] target deps command\" instead of \"-custom command deps target\"" - + | ("-no-opt"|"-byte") :: r -> aux { proj with use_ocamlopt = false } r | ("-full"|"-opt") :: r -> aux { proj with use_ocamlopt = true } r | "-install" :: d :: r -> @@ -189,7 +209,7 @@ let process_cmd_line orig_dir proj args = error "Output file must be in the current directory"; if proj.makefile <> None then error "Option -o given more than once"; - aux { proj with makefile = Some file } r + aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> aux { proj with defs = proj.defs @ [sourced (v,def)] } r | "-arg" :: a :: r -> diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 4c6156a38..4a691e442 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -130,8 +130,8 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with - | Prop Pos, Prop Pos - | Prop Null, Prop Null + | Set, Set + | Prop, Prop | Type _, Type _ -> true | _ -> false diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index cc9c2046d..84baea964 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,11 +199,12 @@ let id_of_name = function let basename = Nametab.basename_of_global ref in basename | Sort s -> - begin + begin match ESorts.kind sigma s with - | Sorts.Prop _ -> Label.to_id (Label.make "Prop") - | Sorts.Type _ -> Label.to_id (Label.make "Type") - end + | Sorts.Prop -> Label.to_id (Label.make "Prop") + | Sorts.Set -> Label.to_id (Label.make "Set") + | Sorts.Type _ -> Label.to_id (Label.make "Type") + end | _ -> fail() diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 84b29a0bf..e4d17f250 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -148,8 +148,7 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let env = Global.env () in - let vars = Univops.universes_of_constr env c in + let vars = Univops.universes_of_constr c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bf9e37aa7..5c4cbefad 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) match (EConstr.kind !evdref x, EConstr.kind !evdref y) with | Sort s, Sort s' -> (match ESorts.kind !evdref s, ESorts.kind !evdref s' with - | Prop x, Prop y when x == y -> None - | Prop _, Type _ -> None + | Prop, Prop | Set, Set -> None + | (Prop | Set), Type _ -> None | Type x, Type y when Univ.Universe.equal x y -> None (* false *) | _ -> subco ()) | Prod (name, a, b), Prod (name', a', b') -> diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2bc603a90..d7118efd7 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -281,8 +281,8 @@ let matches_core env sigma allow_bound_rels let open Glob_term in begin match ps, ESorts.kind sigma s with - | GProp, Prop Null -> subst - | GSet, Prop Pos -> subst + | GProp, Prop -> subst + | GSet, Set -> subst | GType _, Type _ -> subst | _ -> raise PatternMatchingFailure end diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 23a985dc3..d0de2f8c0 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -597,8 +597,8 @@ let detype_universe sigma u = Univ.Universe.map fn u let detype_sort sigma = function - | Prop Null -> GProp - | Prop Pos -> GSet + | Prop -> GProp + | Set -> GSet | Type u -> GType (if !print_universes diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 8afb9b942..3f5d186d4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) - | Prop Pos when refreshset && not direction -> + | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) refresh_sort status ~direction s diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 622a8e982..685aa400b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -150,8 +150,8 @@ 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 (Prop Null) -> PSort GProp - | Sort (Prop Pos) -> PSort GSet + | 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), diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 746a68b21..7e43c5e41 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -149,18 +149,13 @@ 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 _ -> Sorts.type1 + | Prop | Set -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> - (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with - | _, (Prop Null as s) -> s - | Prop _, (Prop Pos as s) -> s - | Type _, (Prop Pos as s) when is_impredicative_set env -> s - | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ) - | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) - | Prop Null, (Type _ as s) -> s - | Type u1, Type u2 -> Type (Univ.sup u1 u2)) + let dom = sort_of env t in + let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in + Typeops.sort_of_product env dom rang | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args diff --git a/pretyping/typing.ml b/pretyping/typing.ml index cf34ac016..a66ecaaac 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -241,10 +241,6 @@ let judge_of_set = { uj_val = EConstr.mkSet; uj_type = EConstr.mkSort Sorts.type1 } -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - let judge_of_type u = let uu = Univ.Universe.super u in { uj_val = EConstr.mkType u; @@ -333,10 +329,9 @@ let rec execute env sigma cstr = | Sort s -> begin match ESorts.kind sigma s with - | Prop c -> - sigma, judge_of_prop_contents c - | Type u -> - sigma, judge_of_type u + | Prop -> sigma, judge_of_prop + | Set -> sigma, judge_of_set + | Type u -> sigma, judge_of_type u end | Proj (p, c) -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3120c97b5..47c9c51ee 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -348,9 +348,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now not (Safe_typing.empty_private_constants = eff)) in let typ = if allow_deferred then t else nf t in - let env = Global.env () in - let used_univs_body = Univops.universes_of_constr env body in - let used_univs_typ = Univops.universes_of_constr env typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if allow_deferred then let initunivs = UState.const_univ_entry ~poly initial_euctx in let ctx = constrain_variables universes in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 773fc1520..9c5fdcd1c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -477,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false diff --git a/tactics/equality.ml b/tactics/equality.ml index 91c577405..0e3921570 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -942,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkSort (Prop Null)) + kont sigma subval (false_0,mkProp) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the diff --git a/tactics/hints.ml b/tactics/hints.ml index 85ff02824..d28d4848c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -828,38 +828,48 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in - match EConstr.kind sigma cty with - | Prod _ -> - let sigma' = Evd.merge_context_set univ_flexible sigma ctx in - let ce = mk_clenv_from_env env sigma' None (c,cty) in - let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in - let hd = - try head_pattern_bound pat - with BoundPattern -> failwith "make_apply_entry" in - let nmiss = List.length (clenv_missing ce) in - let secvars = secvars_of_constr env sigma c in - let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in - let pat = match info.hint_pattern with - | Some p -> snd p | None -> pat - in - if Int.equal nmiss 0 then - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; - secvars; - code = with_uid (Res_pf(c,cty,ctx)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then - Feedback.msg_info (str "the hint: eapply " ++ pr_leconstr_env env sigma' c ++ - str " will only be used by eauto"); - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; secvars; - code = with_uid (ERes_pf(c,cty,ctx)); }) - end - | _ -> failwith "make_apply_entry" + match EConstr.kind sigma cty with + | Prod _ -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let c' = clenv_type (* ~reduce:false *) ce in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry" in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let secvars = secvars_of_constr env sigma c in + let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in + let pat = match info.hint_pattern with + | Some p -> snd p | None -> pat + in + if Int.equal nmiss 0 then + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; + secvars; + code = with_uid (Res_pf(c,cty,ctx)); }) + else begin + if not eapply then failwith "make_apply_entry"; + if verbose then begin + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + end; + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; secvars; + code = with_uid (ERes_pf(c,cty,ctx)); }) + end + | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose c is a constr diff --git a/tactics/inv.ml b/tactics/inv.ml index 755494c2d..e467eacd9 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> + (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c430edf2e..928530744 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -212,6 +212,9 @@ let clear_dependency_msg env sigma id err inglobal = str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." let error_clear_dependency env sigma id err inglobal = user_err (clear_dependency_msg env sigma id err inglobal) @@ -228,6 +231,9 @@ let replacing_dependency_msg env sigma id err inglobal = str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." let error_replacing_dependency env sigma id err inglobal = user_err (replacing_dependency_msg env sigma id err inglobal) diff --git a/test-suite/bugs/closed/5696.v b/test-suite/bugs/closed/5696.v new file mode 100644 index 000000000..a20ad1b4d --- /dev/null +++ b/test-suite/bugs/closed/5696.v @@ -0,0 +1,5 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation "'var2' x .. y = z ; e" := (ltac:(exact z), (fun x => .. (fun y => e) +..)) (at level 200, x binder, y binder, e at level 220). +Check (var2 a = 1; a). diff --git a/test-suite/bugs/closed/7903.v b/test-suite/bugs/closed/7903.v new file mode 100644 index 000000000..55c7ee99a --- /dev/null +++ b/test-suite/bugs/closed/7903.v @@ -0,0 +1,4 @@ +(* Slightly improving interpretation of Ltac subterms in notations *) + +Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)). +Check bar x (x + x). diff --git a/vernac/classes.ml b/vernac/classes.ml index 382d18b09..26d105ecf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -116,9 +116,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = let kind = IsDefinition Instance in let sigma = - let env = Global.env () in - let levels = Univ.LSet.union (Univops.universes_of_constr env termtype) - (Univops.universes_of_constr env term) in + let levels = Univ.LSet.union (Univops.universes_of_constr termtype) + (Univops.universes_of_constr term) in Evd.restrict_universe_context sigma levels in let uctx = Evd.check_univ_decl ~poly sigma decl in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index a8ac52846..750ed35cb 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -163,7 +163,7 @@ let do_assumptions kind nl l = let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in - let uvars = Univ.LSet.union uvars (Univops.universes_of_constr env t) in + let uvars = Univ.LSet.union uvars (Univops.universes_of_constr t) in uvars, (coe,t,imps)) Univ.LSet.empty l in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index f55c852c0..a8d794642 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -93,7 +93,7 @@ let interp_definition pl bl poly red_option c ctypopt = let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = - Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) + Univ.LSet.union uvars (universes_of_constr evd (of_constr c)) in let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in let evd = Evd.restrict_universe_context evd uvars in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1d1cc62de..37258c2d4 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -262,7 +262,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Univops.universes_of_constr env (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -295,8 +295,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let env = Global.env () in - let vars = Univops.universes_of_constr env (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 6057c05f5..0387b32ba 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly = else sigma let is_impredicative env u = - u = Prop Null || (is_impredicative_set env && u = Prop Pos) + u = Prop || (is_impredicative_set env && u = Set) let interp_ind_arity env sigma ind = let c = intern_gen IsType env sigma ind.ind_arity in @@ -245,7 +245,7 @@ let solve_constraints_system levels level_bounds = let inductive_levels env evd poly arities inds = 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 + if a = Prop then None else Some (univ_of_sort a)) destarities in let cstrs_levels, min_levels, sizes = @@ -298,14 +298,14 @@ let inductive_levels env evd poly arities inds = (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort env evd (Prop Pos) du + Evd.set_leq_sort env evd Set du else evd in let duu = Sorts.univ_of_sort du in let evd = if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then - Evd.set_eq_sort env evd (Prop Null) du + Evd.set_eq_sort env evd Prop du else evd else Evd.set_eq_sort env evd (Type cu) du in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e0b1349f7..fa6a9adf1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -480,10 +480,9 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in let body = nf body in - let env = Global.env () in let uvars = Univ.LSet.union - (Univops.universes_of_constr env typ) - (Univops.universes_of_constr env body) in + (Univops.universes_of_constr typ) + (Univops.universes_of_constr body) in let uctx = UState.restrict prg.prg_ctx uvars in let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in diff --git a/vernac/record.ml b/vernac/record.ml index 202c9b92f..2d7800827 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -164,8 +164,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma (Prop Pos) sort, - EConstr.mkSort (Sorts.sort_of_univ univ) + Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in let sigma = Evd.minimize_universes sigma in |