<commit_before>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Univ

module UNameMap = Names.Id.Map

type uinfo = {
  uname : Id.t option;
  uloc : Loc.t option;
}

module UPairSet = UnivMinim.UPairSet

(* 2nd part used to check consistency on the fly. *)
type t =
 { names : UnivNames.universe_binders * uinfo LMap.t; (** Printing/location information *)
   local : ContextSet.t; (** The local graph of universes (variables and constraints) *)
   seff_univs : LSet.t; (** Local universes used through private constants *)
   univ_variables : UnivSubst.universe_opt_subst;
   (** The local universes that are unification variables *)
   univ_algebraic : LSet.t;
   (** The subset of unification variables that can be instantiated with
        algebraic universes as they appear in inferred types only. *)
   universes : UGraph.t; (** The current graph extended with the local constraints *)
   universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *)
   initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
   weak_constraints : UPairSet.t
 }

let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes

let empty =
  { names = UNameMap.empty, LMap.empty;
    local = ContextSet.empty;
    seff_univs = LSet.empty;
    univ_variables = LMap.empty;
    univ_algebraic = LSet.empty;
    universes = initial_sprop_cumulative;
    universes_lbound = UGraph.Bound.Set;
    initial_universes = initial_sprop_cumulative;
    weak_constraints = UPairSet.empty; }

let elaboration_sprop_cumul =
  Goptions.declare_bool_option_and_ref ~depr:false
    ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true

let make ~lbound univs =
  let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) univs in
  { empty with
    universes = univs;
    universes_lbound = lbound;
    initial_universes = univs}

let is_empty uctx =
  ContextSet.is_empty uctx.local &&
    LMap.is_empty uctx.univ_variables

let uname_union s t =
  if s == t then s
  else
    UNameMap.merge (fun k l r ->
        match l, r with
        | Some _, _ -> l
        | _, _ -> r) s t

let union uctx uctx' =
  if uctx == uctx' then uctx
  else if is_empty uctx' then uctx
  else
    let local = ContextSet.union uctx.local uctx'.local in
    let seff = LSet.union uctx.seff_univs uctx'.seff_univs in
    let names = uname_union (fst uctx.names) (fst uctx'.names) in
    let names_rev = LMap.lunion (snd uctx.names) (snd uctx'.names) in
    let newus = LSet.diff (ContextSet.levels uctx'.local)
                               (ContextSet.levels uctx.local) in
    let newus = LSet.diff newus (LMap.domain uctx.univ_variables) in
    let weak = UPairSet.union uctx.weak_constraints uctx'.weak_constraints in
    let declarenew g =
      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:uctx.universes_lbound ~strict:false g) newus g
    in
      { names = (names, names_rev);
        local = local;
        seff_univs = seff;
        univ_variables =
          LMap.subst_union uctx.univ_variables uctx'.univ_variables;
        univ_algebraic =
          LSet.union uctx.univ_algebraic uctx'.univ_algebraic;
        initial_universes = declarenew uctx.initial_universes;
        universes =
          (if local == uctx.local then uctx.universes
           else
             let cstrsr = ContextSet.constraints uctx'.local in
             UGraph.merge_constraints cstrsr (declarenew uctx.universes));
        universes_lbound = uctx.universes_lbound;
        weak_constraints = weak}

let context_set uctx = uctx.local

let constraints uctx = snd uctx.local

let context uctx = ContextSet.to_context uctx.local

let compute_instance_binders inst ubinders =
  let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in
  let map lvl =
    try Name (LMap.find lvl revmap)
    with Not_found -> Anonymous
  in
  Array.map map (Instance.to_array inst)

let univ_entry ~poly uctx =
  let open Entries in
  if poly then
    let (binders, _) = uctx.names in
    let uctx = context uctx in
    let nas = compute_instance_binders (UContext.instance uctx) binders in
    Polymorphic_entry (nas, uctx)
  else Monomorphic_entry (context_set uctx)

let of_context_set local = { empty with local }

let subst uctx = uctx.univ_variables

let ugraph uctx = uctx.universes

let initial_graph uctx = uctx.initial_universes

let algebraics uctx = uctx.univ_algebraic

let add_names ?loc s l (names, names_rev) =
  if UNameMap.mem s names
  then user_err ?loc ~hdr:"add_names"
      Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound.");
  (UNameMap.add s l names, LMap.add l { uname = Some s; uloc = loc } names_rev)

let add_loc l loc (names, names_rev) =
  match loc with
  | None -> (names, names_rev)
  | Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev)

let of_binders names =
  let rev_map =
    UNameMap.fold (fun id l rmap ->
        LMap.add l { uname = Some id; uloc = None } rmap)
      names LMap.empty
  in
  { empty with names = (names, rev_map) }

let invent_name (named,cnt) u =
  let rec aux i =
    let na = Id.of_string ("u"^(string_of_int i)) in
    if Id.Map.mem na named then aux (i+1)
    else Id.Map.add na u named, i+1
  in
  aux cnt

let universe_binders uctx =
  let named, rev = uctx.names in
  let named, _ = LSet.fold (fun u named ->
      match LMap.find u rev with
      | exception Not_found -> (* not sure if possible *) invent_name named u
      | { uname = None } -> invent_name named u
      | { uname = Some _ } -> named)
      (ContextSet.levels uctx.local) (named, 0)
  in
  named

let instantiate_variable l b v =
  try v := LMap.set l (Some b) !v
  with Not_found -> assert false

exception UniversesDiffer

let drop_weak_constraints =
  Goptions.declare_bool_option_and_ref
    ~depr:false
    ~key:["Cumulativity";"Weak";"Constraints"]
    ~value:false

let process_universe_constraints uctx cstrs =
  let open UnivSubst in
  let open UnivProblem in
  let univs = uctx.universes in
  let vars = ref uctx.univ_variables in
  let weak = ref uctx.weak_constraints in
  let normalize u = normalize_univ_variable_opt_subst !vars u in
  let nf_constraint = function
    | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
    | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)
    | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v)
    | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v)
  in
  let is_local l = LMap.mem l !vars in
  let varinfo x =
    match Universe.level x with
    | None -> Inl x
    | Some l -> Inr l
  in
  let equalize_variables fo l l' r r' local =
    (* Assumes l = [l',0] and r = [r',0] *)
    let () =
      if is_local l' then
        instantiate_variable l' r vars
      else if is_local r' then
        instantiate_variable r' l vars
      else if not (UGraph.check_eq_level univs l' r') then
        (* Two rigid/global levels, none of them being local,
            one of them being Prop/Set, disallow *)
        if Level.is_small l' || Level.is_small r' then
          raise (UniverseInconsistency (Eq, l, r, None))
        else if fo then
          raise UniversesDiffer
    in
    enforce_eq_level l' r' local
  in
  let equalize_universes l r local = match varinfo l, varinfo r with
  | Inr l', Inr r' -> equalize_variables false l l' r r' local
  | Inr l, Inl r | Inl r, Inr l ->
    let alg = LSet.mem l uctx.univ_algebraic in
    let inst = univ_level_rem l r r in
      if alg && not (LSet.mem l (Universe.levels inst)) then
        (instantiate_variable l inst vars; local)
      else
        let lu = Universe.make l in
        if univ_level_mem l r then
          enforce_leq inst lu local
        else raise (UniverseInconsistency (Eq, lu, r, None))
  | Inl _, Inl _ (* both are algebraic *) ->
    if UGraph.check_eq univs l r then local
    else raise (UniverseInconsistency (Eq, l, r, None))
  in
  let unify_universes cst local =
    let cst = nf_constraint cst in
      if UnivProblem.is_trivial cst then local
      else
          match cst with
          | ULe (l, r) ->
            begin match Univ.Universe.level r with
            | None ->
              if UGraph.check_leq univs l r then local
              else user_err Pp.(str "Algebraic universe on the right")
            | Some r' ->
              if Level.is_small r' then
                  if not (Universe.is_levels l)
                  then (* l contains a +1 and r=r' small so l <= r impossible *)
                    raise (UniverseInconsistency (Le, l, r, None))
                  else
                    if UGraph.check_leq univs l r then match Univ.Universe.level l with
                    | Some l ->
                      Univ.Constraint.add (l, Le, r') local
                    | None -> local
                    else
                    let levels = Universe.levels l in
                    let fold l' local =
                      let l = Universe.make l' in
                      if Level.is_small l' || is_local l' then
                        equalize_variables false l l' r r' local
                      else raise (UniverseInconsistency (Le, l, r, None))
                    in
                    LSet.fold fold levels local
              else
                match Univ.Universe.level l with
                | Some l ->
                  Univ.Constraint.add (l, Le, r') local
                | None ->
                  if UGraph.check_leq univs l r then local else enforce_leq l r local
              end
          | ULub (l, r) ->
              equalize_variables true (Universe.make l) l (Universe.make r) r local
          | UWeak (l, r) ->
            if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
          | UEq (l, r) -> equalize_universes l r local
  in
  let unify_universes cst local =
    if not (UGraph.type_in_type univs) then unify_universes cst local
    else try unify_universes cst local with UniverseInconsistency _ -> local
  in
  let local =
    UnivProblem.Set.fold unify_universes cstrs Constraint.empty
  in
    !vars, !weak, local

let add_constraints uctx cstrs =
  let univs, old_cstrs = uctx.local in
  let cstrs' = Constraint.fold (fun (l,d,r) acc ->
    let l = Universe.make l and r = Universe.make r in
    let cstr' = let open UnivProblem in
      match d with
      | Lt ->
        ULe (Universe.super l, r)
      | Le -> ULe (l, r)
      | Eq -> UEq (l, r)
    in UnivProblem.Set.add cstr' acc)
    cstrs UnivProblem.Set.empty
  in
  let vars, weak, cstrs' = process_universe_constraints uctx cstrs' in
  { uctx with
    local = (univs, Constraint.union old_cstrs cstrs');
    univ_variables = vars;
    universes = UGraph.merge_constraints cstrs' uctx.universes;
    weak_constraints = weak; }

(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)

let add_universe_constraints uctx cstrs =
  let univs, local = uctx.local in
  let vars, weak, local' = process_universe_constraints uctx cstrs in
  { uctx with
    local = (univs, Constraint.union local local');
    univ_variables = vars;
    universes = UGraph.merge_constraints local' uctx.universes;
    weak_constraints = weak; }

let constrain_variables diff uctx =
  let univs, local = uctx.local in
  let univs, vars, local =
    LSet.fold
      (fun l (univs, vars, cstrs) ->
        try
          match LMap.find l vars with
          | Some u ->
             (LSet.add l univs,
              LMap.remove l vars,
              Constraint.add (l, Eq, Option.get (Universe.level u)) cstrs)
          | None -> (univs, vars, cstrs)
        with Not_found | Option.IsNone -> (univs, vars, cstrs))
      diff (univs, uctx.univ_variables, local)
  in
  { uctx with local = (univs, local); univ_variables = vars }

let id_of_level uctx l =
  try Some (Option.get (LMap.find l (snd uctx.names)).uname)
  with Not_found | Option.IsNone ->
    None

let qualid_of_level uctx l =
  let map, map_rev = uctx.names in
  try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
  with Not_found | Option.IsNone ->
    UnivNames.qualid_of_level map l

let pr_uctx_level uctx l =
  match qualid_of_level uctx l with
  | Some qid -> Libnames.pr_qualid qid
  | None -> Level.pr l

type ('a, 'b) gen_universe_decl = {
  univdecl_instance : 'a; (* Declared universes *)
  univdecl_extensible_instance : bool; (* Can new universes be added *)
  univdecl_constraints : 'b; (* Declared constraints *)
  univdecl_extensible_constraints : bool (* Can new constraints be added *) }

type universe_decl =
  (lident list, Constraint.t) gen_universe_decl

let default_univ_decl =
  { univdecl_instance = [];
    univdecl_extensible_instance = true;
    univdecl_constraints = Constraint.empty;
    univdecl_extensible_constraints = true }

let error_unbound_universes left uctx =
  let n = LSet.cardinal left in
  let loc =
    try
      let info =
        LMap.find (LSet.choose left) (snd uctx.names) in
      info.uloc
    with Not_found -> None
  in
  user_err ?loc ~hdr:"universe_context"
    ((str(CString.plural n "Universe") ++ spc () ++
      LSet.pr (pr_uctx_level uctx) left ++
      spc () ++ str (CString.conjugate_verb_to_be n) ++
      str" unbound."))

let universe_context ~names ~extensible uctx =
  let levels = ContextSet.levels uctx.local in
  let newinst, left =
    List.fold_right
      (fun { CAst.loc; v = id } (newinst, acc) ->
         let l =
           try UNameMap.find id (fst uctx.names)
           with Not_found -> assert false
         in (l :: newinst, LSet.remove l acc))
      names ([], levels)
  in
  if not extensible && not (LSet.is_empty left)
  then error_unbound_universes left uctx
  else
    let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
    let inst = Array.append (Array.of_list newinst) left in
    let inst = Instance.of_array inst in
    let uctx = UContext.make (inst, ContextSet.constraints uctx.local) in
    uctx

let check_universe_context_set ~names ~extensible uctx =
  if extensible then ()
  else
    let left = List.fold_left (fun left { CAst.loc; v = id } ->
        let l =
          try UNameMap.find id (fst uctx.names)
          with Not_found -> assert false
        in LSet.remove l left)
        (ContextSet.levels uctx.local) names
    in
    if not (LSet.is_empty left)
    then error_unbound_universes left uctx

let check_implication uctx cstrs cstrs' =
  let gr = initial_graph uctx in
  let grext = UGraph.merge_constraints cstrs gr in
  if UGraph.check_constraints cstrs' grext then ()
  else CErrors.user_err ~hdr:"check_univ_decl"
      (str "Universe constraints are not implied by the ones declared.")

let check_mono_univ_decl uctx decl =
  let () =
    let names = decl.univdecl_instance in
    let extensible = decl.univdecl_extensible_instance in
    check_universe_context_set ~names ~extensible uctx
  in
  if not decl.univdecl_extensible_constraints then
    check_implication uctx
      decl.univdecl_constraints
      (ContextSet.constraints uctx.local);
  uctx.local

let check_univ_decl ~poly uctx decl =
  if not decl.univdecl_extensible_constraints then
    check_implication uctx
      decl.univdecl_constraints
      (ContextSet.constraints uctx.local);
  let names = decl.univdecl_instance in
  let extensible = decl.univdecl_extensible_instance in
  if poly then
    let (binders, _) = uctx.names in
    let uctx = universe_context ~names ~extensible uctx in
    let nas = compute_instance_binders (UContext.instance uctx) binders in
    Entries.Polymorphic_entry (nas, uctx)
  else
    let () = check_universe_context_set ~names ~extensible uctx in
    Entries.Monomorphic_entry uctx.local

let is_bound l lbound = match lbound with
  | UGraph.Bound.Prop -> Level.is_prop l
  | UGraph.Bound.Set -> Level.is_set l

let restrict_universe_context ~lbound (univs, csts) keep =
  let removed = LSet.diff univs keep in
  if LSet.is_empty removed then univs, csts
  else
  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in<commit_msg>compute_instance_binders: use prebuilt reverse map<commit_after>(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Pp
open CErrors
open Util
open Names
open Univ

module UNameMap = Names.Id.Map

type uinfo = {
  uname : Id.t option;
  uloc : Loc.t option;
}

module UPairSet = UnivMinim.UPairSet

(* 2nd part used to check consistency on the fly. *)
type t =
 { names : UnivNames.universe_binders * uinfo LMap.t; (** Printing/location information *)
   local : ContextSet.t; (** The local graph of universes (variables and constraints) *)
   seff_univs : LSet.t; (** Local universes used through private constants *)
   univ_variables : UnivSubst.universe_opt_subst;
   (** The local universes that are unification variables *)
   univ_algebraic : LSet.t;
   (** The subset of unification variables that can be instantiated with
        algebraic universes as they appear in inferred types only. *)
   universes : UGraph.t; (** The current graph extended with the local constraints *)
   universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *)
   initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
   weak_constraints : UPairSet.t
 }

let initial_sprop_cumulative = UGraph.set_cumulative_sprop true UGraph.initial_universes

let empty =
  { names = UNameMap.empty, LMap.empty;
    local = ContextSet.empty;
    seff_univs = LSet.empty;
    univ_variables = LMap.empty;
    univ_algebraic = LSet.empty;
    universes = initial_sprop_cumulative;
    universes_lbound = UGraph.Bound.Set;
    initial_universes = initial_sprop_cumulative;
    weak_constraints = UPairSet.empty; }

let elaboration_sprop_cumul =
  Goptions.declare_bool_option_and_ref ~depr:false
    ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true

let make ~lbound univs =
  let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul ()) univs in
  { empty with
    universes = univs;
    universes_lbound = lbound;
    initial_universes = univs}

let is_empty uctx =
  ContextSet.is_empty uctx.local &&
    LMap.is_empty uctx.univ_variables

let uname_union s t =
  if s == t then s
  else
    UNameMap.merge (fun k l r ->
        match l, r with
        | Some _, _ -> l
        | _, _ -> r) s t

let union uctx uctx' =
  if uctx == uctx' then uctx
  else if is_empty uctx' then uctx
  else
    let local = ContextSet.union uctx.local uctx'.local in
    let seff = LSet.union uctx.seff_univs uctx'.seff_univs in
    let names = uname_union (fst uctx.names) (fst uctx'.names) in
    let names_rev = LMap.lunion (snd uctx.names) (snd uctx'.names) in
    let newus = LSet.diff (ContextSet.levels uctx'.local)
                               (ContextSet.levels uctx.local) in
    let newus = LSet.diff newus (LMap.domain uctx.univ_variables) in
    let weak = UPairSet.union uctx.weak_constraints uctx'.weak_constraints in
    let declarenew g =
      LSet.fold (fun u g -> UGraph.add_universe u ~lbound:uctx.universes_lbound ~strict:false g) newus g
    in
      { names = (names, names_rev);
        local = local;
        seff_univs = seff;
        univ_variables =
          LMap.subst_union uctx.univ_variables uctx'.univ_variables;
        univ_algebraic =
          LSet.union uctx.univ_algebraic uctx'.univ_algebraic;
        initial_universes = declarenew uctx.initial_universes;
        universes =
          (if local == uctx.local then uctx.universes
           else
             let cstrsr = ContextSet.constraints uctx'.local in
             UGraph.merge_constraints cstrsr (declarenew uctx.universes));
        universes_lbound = uctx.universes_lbound;
        weak_constraints = weak}

let context_set uctx = uctx.local

let constraints uctx = snd uctx.local

let context uctx = ContextSet.to_context uctx.local

let compute_instance_binders inst ubinders =
  let map lvl =
    try Name (Option.get (LMap.find lvl ubinders).uname)
    with Option.IsNone | Not_found -> Anonymous
  in
  Array.map map (Instance.to_array inst)

let univ_entry ~poly uctx =
  let open Entries in
  if poly then
    let (_, rbinders) = uctx.names in
    let uctx = context uctx in
    let nas = compute_instance_binders (UContext.instance uctx) rbinders in
    Polymorphic_entry (nas, uctx)
  else Monomorphic_entry (context_set uctx)

let of_context_set local = { empty with local }

let subst uctx = uctx.univ_variables

let ugraph uctx = uctx.universes

let initial_graph uctx = uctx.initial_universes

let algebraics uctx = uctx.univ_algebraic

let add_names ?loc s l (names, names_rev) =
  if UNameMap.mem s names
  then user_err ?loc ~hdr:"add_names"
      Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound.");
  (UNameMap.add s l names, LMap.add l { uname = Some s; uloc = loc } names_rev)

let add_loc l loc (names, names_rev) =
  match loc with
  | None -> (names, names_rev)
  | Some _ -> (names, LMap.add l { uname = None; uloc = loc } names_rev)

let of_binders names =
  let rev_map =
    UNameMap.fold (fun id l rmap ->
        LMap.add l { uname = Some id; uloc = None } rmap)
      names LMap.empty
  in
  { empty with names = (names, rev_map) }

let invent_name (named,cnt) u =
  let rec aux i =
    let na = Id.of_string ("u"^(string_of_int i)) in
    if Id.Map.mem na named then aux (i+1)
    else Id.Map.add na u named, i+1
  in
  aux cnt

let universe_binders uctx =
  let named, rev = uctx.names in
  let named, _ = LSet.fold (fun u named ->
      match LMap.find u rev with
      | exception Not_found -> (* not sure if possible *) invent_name named u
      | { uname = None } -> invent_name named u
      | { uname = Some _ } -> named)
      (ContextSet.levels uctx.local) (named, 0)
  in
  named

let instantiate_variable l b v =
  try v := LMap.set l (Some b) !v
  with Not_found -> assert false

exception UniversesDiffer

let drop_weak_constraints =
  Goptions.declare_bool_option_and_ref
    ~depr:false
    ~key:["Cumulativity";"Weak";"Constraints"]
    ~value:false

let process_universe_constraints uctx cstrs =
  let open UnivSubst in
  let open UnivProblem in
  let univs = uctx.universes in
  let vars = ref uctx.univ_variables in
  let weak = ref uctx.weak_constraints in
  let normalize u = normalize_univ_variable_opt_subst !vars u in
  let nf_constraint = function
    | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
    | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v)
    | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v)
    | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v)
  in
  let is_local l = LMap.mem l !vars in
  let varinfo x =
    match Universe.level x with
    | None -> Inl x
    | Some l -> Inr l
  in
  let equalize_variables fo l l' r r' local =
    (* Assumes l = [l',0] and r = [r',0] *)
    let () =
      if is_local l' then
        instantiate_variable l' r vars
      else if is_local r' then
        instantiate_variable r' l vars
      else if not (UGraph.check_eq_level univs l' r') then
        (* Two rigid/global levels, none of them being local,
            one of them being Prop/Set, disallow *)
        if Level.is_small l' || Level.is_small r' then
          raise (UniverseInconsistency (Eq, l, r, None))
        else if fo then
          raise UniversesDiffer
    in
    enforce_eq_level l' r' local
  in
  let equalize_universes l r local = match varinfo l, varinfo r with
  | Inr l', Inr r' -> equalize_variables false l l' r r' local
  | Inr l, Inl r | Inl r, Inr l ->
    let alg = LSet.mem l uctx.univ_algebraic in
    let inst = univ_level_rem l r r in
      if alg && not (LSet.mem l (Universe.levels inst)) then
        (instantiate_variable l inst vars; local)
      else
        let lu = Universe.make l in
        if univ_level_mem l r then
          enforce_leq inst lu local
        else raise (UniverseInconsistency (Eq, lu, r, None))
  | Inl _, Inl _ (* both are algebraic *) ->
    if UGraph.check_eq univs l r then local
    else raise (UniverseInconsistency (Eq, l, r, None))
  in
  let unify_universes cst local =
    let cst = nf_constraint cst in
      if UnivProblem.is_trivial cst then local
      else
          match cst with
          | ULe (l, r) ->
            begin match Univ.Universe.level r with
            | None ->
              if UGraph.check_leq univs l r then local
              else user_err Pp.(str "Algebraic universe on the right")
            | Some r' ->
              if Level.is_small r' then
                  if not (Universe.is_levels l)
                  then (* l contains a +1 and r=r' small so l <= r impossible *)
                    raise (UniverseInconsistency (Le, l, r, None))
                  else
                    if UGraph.check_leq univs l r then match Univ.Universe.level l with
                    | Some l ->
                      Univ.Constraint.add (l, Le, r') local
                    | None -> local
                    else
                    let levels = Universe.levels l in
                    let fold l' local =
                      let l = Universe.make l' in
                      if Level.is_small l' || is_local l' then
                        equalize_variables false l l' r r' local
                      else raise (UniverseInconsistency (Le, l, r, None))
                    in
                    LSet.fold fold levels local
              else
                match Univ.Universe.level l with
                | Some l ->
                  Univ.Constraint.add (l, Le, r') local
                | None ->
                  if UGraph.check_leq univs l r then local else enforce_leq l r local
              end
          | ULub (l, r) ->
              equalize_variables true (Universe.make l) l (Universe.make r) r local
          | UWeak (l, r) ->
            if not (drop_weak_constraints ()) then weak := UPairSet.add (l,r) !weak; local
          | UEq (l, r) -> equalize_universes l r local
  in
  let unify_universes cst local =
    if not (UGraph.type_in_type univs) then unify_universes cst local
    else try unify_universes cst local with UniverseInconsistency _ -> local
  in
  let local =
    UnivProblem.Set.fold unify_universes cstrs Constraint.empty
  in
    !vars, !weak, local

let add_constraints uctx cstrs =
  let univs, old_cstrs = uctx.local in
  let cstrs' = Constraint.fold (fun (l,d,r) acc ->
    let l = Universe.make l and r = Universe.make r in
    let cstr' = let open UnivProblem in
      match d with
      | Lt ->
        ULe (Universe.super l, r)
      | Le -> ULe (l, r)
      | Eq -> UEq (l, r)
    in UnivProblem.Set.add cstr' acc)
    cstrs UnivProblem.Set.empty
  in
  let vars, weak, cstrs' = process_universe_constraints uctx cstrs' in
  { uctx with
    local = (univs, Constraint.union old_cstrs cstrs');
    univ_variables = vars;
    universes = UGraph.merge_constraints cstrs' uctx.universes;
    weak_constraints = weak; }

(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)

let add_universe_constraints uctx cstrs =
  let univs, local = uctx.local in
  let vars, weak, local' = process_universe_constraints uctx cstrs in
  { uctx with
    local = (univs, Constraint.union local local');
    univ_variables = vars;
    universes = UGraph.merge_constraints local' uctx.universes;
    weak_constraints = weak; }

let constrain_variables diff uctx =
  let univs, local = uctx.local in
  let univs, vars, local =
    LSet.fold
      (fun l (univs, vars, cstrs) ->
        try
          match LMap.find l vars with
          | Some u ->
             (LSet.add l univs,
              LMap.remove l vars,
              Constraint.add (l, Eq, Option.get (Universe.level u)) cstrs)
          | None -> (univs, vars, cstrs)
        with Not_found | Option.IsNone -> (univs, vars, cstrs))
      diff (univs, uctx.univ_variables, local)
  in
  { uctx with local = (univs, local); univ_variables = vars }

let id_of_level uctx l =
  try Some (Option.get (LMap.find l (snd uctx.names)).uname)
  with Not_found | Option.IsNone ->
    None

let qualid_of_level uctx l =
  let map, map_rev = uctx.names in
  try Some (Libnames.qualid_of_ident (Option.get (LMap.find l map_rev).uname))
  with Not_found | Option.IsNone ->
    UnivNames.qualid_of_level map l

let pr_uctx_level uctx l =
  match qualid_of_level uctx l with
  | Some qid -> Libnames.pr_qualid qid
  | None -> Level.pr l

type ('a, 'b) gen_universe_decl = {
  univdecl_instance : 'a; (* Declared universes *)
  univdecl_extensible_instance : bool; (* Can new universes be added *)
  univdecl_constraints : 'b; (* Declared constraints *)
  univdecl_extensible_constraints : bool (* Can new constraints be added *) }

type universe_decl =
  (lident list, Constraint.t) gen_universe_decl

let default_univ_decl =
  { univdecl_instance = [];
    univdecl_extensible_instance = true;
    univdecl_constraints = Constraint.empty;
    univdecl_extensible_constraints = true }

let error_unbound_universes left uctx =
  let n = LSet.cardinal left in
  let loc =
    try
      let info =
        LMap.find (LSet.choose left) (snd uctx.names) in
      info.uloc
    with Not_found -> None
  in
  user_err ?loc ~hdr:"universe_context"
    ((str(CString.plural n "Universe") ++ spc () ++
      LSet.pr (pr_uctx_level uctx) left ++
      spc () ++ str (CString.conjugate_verb_to_be n) ++
      str" unbound."))

let universe_context ~names ~extensible uctx =
  let levels = ContextSet.levels uctx.local in
  let newinst, left =
    List.fold_right
      (fun { CAst.loc; v = id } (newinst, acc) ->
         let l =
           try UNameMap.find id (fst uctx.names)
           with Not_found -> assert false
         in (l :: newinst, LSet.remove l acc))
      names ([], levels)
  in
  if not extensible && not (LSet.is_empty left)
  then error_unbound_universes left uctx
  else
    let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
    let inst = Array.append (Array.of_list newinst) left in
    let inst = Instance.of_array inst in
    let uctx = UContext.make (inst, ContextSet.constraints uctx.local) in
    uctx

let check_universe_context_set ~names ~extensible uctx =
  if extensible then ()
  else
    let left = List.fold_left (fun left { CAst.loc; v = id } ->
        let l =
          try UNameMap.find id (fst uctx.names)
          with Not_found -> assert false
        in LSet.remove l left)
        (ContextSet.levels uctx.local) names
    in
    if not (LSet.is_empty left)
    then error_unbound_universes left uctx

let check_implication uctx cstrs cstrs' =
  let gr = initial_graph uctx in
  let grext = UGraph.merge_constraints cstrs gr in
  if UGraph.check_constraints cstrs' grext then ()
  else CErrors.user_err ~hdr:"check_univ_decl"
      (str "Universe constraints are not implied by the ones declared.")

let check_mono_univ_decl uctx decl =
  let () =
    let names = decl.univdecl_instance in
    let extensible = decl.univdecl_extensible_instance in
    check_universe_context_set ~names ~extensible uctx
  in
  if not decl.univdecl_extensible_constraints then
    check_implication uctx
      decl.univdecl_constraints
      (ContextSet.constraints uctx.local);
  uctx.local

let check_univ_decl ~poly uctx decl =
  if not decl.univdecl_extensible_constraints then
    check_implication uctx
      decl.univdecl_constraints
      (ContextSet.constraints uctx.local);
  let names = decl.univdecl_instance in
  let extensible = decl.univdecl_extensible_instance in
  if poly then
    let (_, rbinders) = uctx.names in
    let uctx = universe_context ~names ~extensible uctx in
    let nas = compute_instance_binders (UContext.instance uctx) rbinders in
    Entries.Polymorphic_entry (nas, uctx)
  else
    let () = check_universe_context_set ~names ~extensible uctx in
    Entries.Monomorphic_entry uctx.local

let is_bound l lbound = match lbound with
  | UGraph.Bound.Prop -> Level.is_prop l
  | UGraph.Bound.Set -> Level.is_set l

let restrict_universe_context ~lbound (univs, csts) keep =
  let removed = LSet.diff univs keep in
  if LSet.is_empty removed then univs, csts
  else
  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
{'fraction_non_alphanumeric': 0.09608793286845527, 'fraction_numerical': 0.0005909466966079659, 'mean_word_length': 2.6557571829768847, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 110, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3049132', 'n_tokens_mistral': 11432, 'n_tokens_neox': 11239, 'n_words': 3485}