diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 46 | ||||
| -rw-r--r-- | engine/evarutil.mli | 26 | ||||
| -rw-r--r-- | engine/evd.ml | 32 | ||||
| -rw-r--r-- | engine/universes.ml | 315 | ||||
| -rw-r--r-- | engine/universes.mli | 2 |
5 files changed, 203 insertions, 218 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 065b42bf62..710491f848 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -342,7 +342,15 @@ let update_var src tgt subst = let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in { subst with csubst_var; csubst_rev } -let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + +let push_rel_decl_to_named_context + ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) + sigma decl (subst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = @@ -373,7 +381,9 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> + | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames || + hypnaming = KeepUserNameAndRenameExistingButSectionNames && + not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given by the user) and rename [id0] into [id] in the named @@ -382,6 +392,8 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = List.map (replace_var_named_declaration id0 id) nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) + | Some id0 when hypnaming = FailIfConflict -> + user_err Pp.(Id.print id0 ++ str " is already used.") | _ -> (* spiwack: if [id0] is a section variable renaming it is incorrect. We revert to a less robust behaviour where @@ -390,7 +402,7 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in (push_var id subst, Id.Set.add id avoid, d :: nc) -let push_rel_context_to_named_context env sigma typ = +let push_rel_context_to_named_context ?hypnaming env sigma typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in let open EConstr in @@ -405,7 +417,7 @@ let push_rel_context_to_named_context env sigma typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, _, env) = - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc) (rel_context env) ~init:(empty_csubst, avoid, named_context env) in (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) @@ -468,8 +480,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in +let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = + let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = @@ -478,13 +490,13 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal rigid = +let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in +let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid = + let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in evdref := evd; c @@ -498,8 +510,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = evdref := evd'; EConstr.mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in evdref := evd'; ev @@ -522,7 +534,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option exception Depends of Id.t @@ -533,13 +545,13 @@ let rec check_and_clear_in_constr env evdref err ids global c = is a section variable *) match kind c with | Var id' -> - if Id.Set.mem id' ids then raise (ClearDependencyError (id', err)) else c + if Id.Set.mem id' ids then raise (ClearDependencyError (id', err, None)) else c | ( Const _ | Ind _ | Construct _ ) -> let () = if global then let check id' = if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err)) + raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) in Id.Set.iter check (Environ.vars_of_global env c) in @@ -587,8 +599,8 @@ let rec check_and_clear_in_constr env evdref err ids global c = let global = Id.Set.exists is_section_variable nids in let concl = EConstr.Unsafe.to_constr (evar_concl evi) in check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids global concl - with ClearDependencyError (rid,err) -> - raise (ClearDependencyError (Id.Map.find rid rids,err)) in + with ClearDependencyError (rid,err,where) -> + raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in if Id.Map.is_empty rids then c else diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 40c1ee0820..e3e8f16c8b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -30,11 +30,17 @@ val new_evar_from_context : ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> evar_map * EConstr.t +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + val new_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t val new_pure_evar : named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> @@ -49,18 +55,20 @@ val e_new_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> evar_map * (constr * Sorts.t) val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr @@ -178,11 +186,14 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t @@ -224,7 +235,7 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types @@ -240,10 +251,11 @@ val csubst_subst : csubst -> constr -> constr type ext_named_context = csubst * Id.Set.t * named_context -val push_rel_decl_to_named_context : +val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> +val push_rel_context_to_named_context : ?hypnaming:naming_mode -> + Environ.env -> evar_map -> types -> named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index 6dcec2760b..af22de5cd4 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -1290,30 +1290,14 @@ module MiniEConstr = struct let unsafe_eq = Refl let to_constr ?(abort_on_undefined_evars=true) sigma c = - let rec to_constr c = match Constr.kind c with - | Evar ev -> - begin match safe_evar_value sigma ev with - | Some c -> to_constr c - | None -> - if abort_on_undefined_evars then - anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") - else - Constr.map (fun c -> to_constr c) c - end - | Sort (Sorts.Type u) -> - let u' = normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> Constr.map (fun c -> to_constr c) c - in to_constr c + let evar_value = + if not abort_on_undefined_evars then fun ev -> safe_evar_value sigma ev + else fun ev -> + match safe_evar_value sigma ev with + | Some _ as v -> v + | None -> anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term") + in + Universes.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c let of_named_decl d = d let unsafe_to_named_decl d = d diff --git a/engine/universes.ml b/engine/universes.ml index e5f9212a71..0410d1aeaf 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -524,8 +524,6 @@ let new_global_univ () = (** Simplification *) -module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) - let add_list_map u t map = try let l = LMap.find u map in @@ -533,8 +531,6 @@ let add_list_map u t map = with Not_found -> LMap.add u [t] map -module UF = LevelUnionFind - (** Precondition: flexible <= ctx *) let choose_canonical ctx flexible algs s = let global = LSet.diff s ctx in @@ -596,35 +592,6 @@ let subst_univs_constr = CProfile.profile2 subst_univs_constr_key subst_univs_constr else subst_univs_constr -let subst_univs_fn_puniverses lsubst (c, u as cu) = - let u' = Instance.subst_fn lsubst u in - if u' == u then cu else (c, u') - -let nf_evars_and_universes_opt_subst f subst = - let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in - let lsubst = level_subst_of subst in - let rec aux c = - match kind c with - | Evar (evk, args) -> - let args = Array.map aux args in - (match try f (evk, args) with Not_found -> None with - | None -> c - | Some c -> aux c) - | Const pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstU pu' - | Ind pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkIndU pu' - | Construct pu -> - let pu' = subst_univs_fn_puniverses lsubst pu in - if pu' == pu then c else mkConstructU pu' - | Sort (Type u) -> - let u' = Univ.subst_univs_universe subst u in - if u' == u then c else mkSort (sort_of_univ u') - | _ -> Constr.map aux c - in aux - let fresh_universe_context_set_instance ctx = if ContextSet.is_empty ctx then LMap.empty, ctx else @@ -683,6 +650,35 @@ let normalize_opt_subst ctx = type universe_opt_subst = Universe.t option universe_map +let subst_univs_fn_puniverses f (c, u as cu) = + let u' = Instance.subst_fn f u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_opt_subst f subst = + let subst = normalize_univ_variable_opt_subst (ref subst) in + let lsubst = level_subst_of subst in + let rec aux c = + match kind c with + | Evar (evk, args) -> + let args = Array.map aux args in + (match try f (evk, args) with Not_found -> None with + | None -> mkEvar (evk, args) + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> Constr.map aux c + in aux + let make_opt_subst s = fun x -> (match Univ.LMap.find x s with @@ -709,6 +705,7 @@ let pr_universe_body = function let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body +(* Eq < Le < Lt *) let compare_constraint_type d d' = match d, d' with | Eq, Eq -> 0 @@ -742,10 +739,12 @@ let lower_add l c m = let lower_of_list l = List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l +type lbound = { enforce : bool; alg : bool; lbound: Universe.t; lower : lowermap } + exception Found of Level.t * lowermap let find_inst insts v = - try LMap.iter (fun k (enf,alg,v',lower) -> - if not alg && enf && Universe.equal v' v then raise (Found (k, lower))) + try LMap.iter (fun k {enforce;alg;lbound=v';lower} -> + if not alg && enforce && Universe.equal v' v then raise (Found (k, lower))) insts; raise Not_found with Found (f,l) -> (f,l) @@ -765,18 +764,18 @@ let compute_lbound left = sup (Universe.super l) lbound else None)) None left - -let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) = + +let instantiate_with_lbound u lbound lower ~alg ~enforce (ctx, us, algs, insts, cstrs) = if enforce then let inst = Universe.make u in let cstrs' = enforce_leq lbound inst cstrs in (ctx, us, LSet.remove u algs, - LMap.add u (enforce,alg,lbound,lower) insts, cstrs'), - (enforce, alg, inst, lower) + LMap.add u {enforce;alg;lbound;lower} insts, cstrs'), + {enforce; alg; lbound=inst; lower} else (* Actually instantiate *) (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u (enforce,alg,lbound,lower) insts, cstrs), - (enforce, alg, lbound, lower) + LMap.add u {enforce;alg;lbound;lower} insts, cstrs), + {enforce; alg; lbound; lower} type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t @@ -790,73 +789,82 @@ let _pr_constraints_map (cmap:constraints_map) = let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) -let remove_lower u lower = - let levels = Universe.levels u in - LSet.fold (fun l acc -> LMap.remove l acc) levels lower - +let not_lower lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + +exception UpperBoundedAlg +(** [enforce_uppers upper lbound cstrs] interprets [upper] as upper + constraints to [lbound], adding them to [cstrs]. + + @raise UpperBoundedAlg if any [upper] constraints are strict and + [lbound] algebraic. *) +let enforce_uppers upper lbound cstrs = + List.fold_left (fun cstrs (d, r) -> + if d == Univ.Le then + enforce_leq lbound (Universe.make r) cstrs + else + match Universe.level lbound with + | Some lev -> Constraint.add (lev, d, r) cstrs + | None -> raise UpperBoundedAlg) + cstrs upper + let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc else (* Fixed universe, just compute its glb for sharing *) - let lbounds' = + let lbounds = match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with | None -> lbounds - | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower) + | Some lbound -> LMap.add r {enforce=true; alg=false; lbound; lower=lower_of_list lower} lbounds - in (Univ.LMap.remove r left, lbounds')) + in (Univ.LMap.remove r left, lbounds)) left (left, Univ.LMap.empty) in - let rec instance (ctx', us, algs, insts, cstrs as acc) u = + let rec instance (ctx, us, algs, insts, cstrs as acc) u = let acc, left, lower = - try - let l = LMap.find u left in + match LMap.find u left with + | exception Not_found -> acc, [], LMap.empty + | l -> let acc, left, newlow, lower = List.fold_left - (fun (acc, left', newlow, lower') (d, l) -> - let acc', (enf,alg,l',lower) = aux acc l in + (fun (acc, left, newlow, lower') (d, l) -> + let acc', {enforce=enf;alg;lbound=l';lower} = aux acc l in let l' = if enf then Universe.make l else l' - in acc', (d, l') :: left', + in acc', (d, l') :: left, lower_add l d newlow, lower_union lower lower') (acc, [], LMap.empty, LMap.empty) l in - let not_lower (d,l) = - (* We're checking if (d,l) is already implied by the lower - constraints on some level u. If it represents l < u (d is Lt - or d is Le and i > 0, the i < 0 case is impossible due to - invariants of Univ), and the lower constraints only have l <= - u then it is not implied. *) - Univ.Universe.exists - (fun (l,i) -> - let d = - if i == 0 then d - else match d with - | Le -> Lt - | d -> d - in - try let d' = LMap.find l lower in - (* If d is stronger than the already implied lower - * constraints we must keep it. *) - compare_constraint_type d d' > 0 - with Not_found -> - (** No constraint existing on l *) true) l - in - let left = List.uniquize (List.filter not_lower left) in + let left = List.uniquize (List.filter (not_lower lower) left) in (acc, left, LMap.union newlow lower) - with Not_found -> acc, [], LMap.empty - and right = - try Some (LMap.find u right) - with Not_found -> None in let instantiate_lbound lbound = let alg = LSet.mem u algs in if alg then (* u is algebraic: we instantiate it with its lower bound, if any, or enforce the constraints if it is bounded from the top. *) - let lower = remove_lower lbound lower in - instantiate_with_lbound u lbound lower true false acc + let lower = LSet.fold LMap.remove (Universe.levels lbound) lower in + instantiate_with_lbound u lbound lower ~alg:true ~enforce:false acc else (* u is non algebraic *) match Universe.level lbound with | Some l -> (* The lowerbound is directly a level *) @@ -867,125 +875,96 @@ let minimize_univ_variables ctx us algs left right cstrs = if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) - let acc' = remove_alg l acc in - instantiate_with_lbound u lbound lower false false acc' - else acc, (true, false, lbound, lower) + let acc = remove_alg l acc in + instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc + else acc, {enforce=true; alg=false; lbound; lower} | None -> - try - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let can, lower = find_inst insts lbound in - let lower = LMap.remove can lower in - instantiate_with_lbound u (Universe.make can) lower false false acc - with Not_found -> - (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound lower false true acc + begin match find_inst insts lbound with + | can, lower -> + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc + | exception Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc + end in - let acc' acc = - match right with - | None -> acc - | Some cstrs -> - let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in - if List.is_empty dangling then acc - else - let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in - let cstrs' = List.fold_left (fun cstrs (d, r) -> - if d == Univ.Le then - enforce_leq inst (Universe.make r) cstrs - else - try let lev = Option.get (Universe.level inst) in - Constraint.add (lev, d, r) cstrs - with Option.IsNone -> failwith "") - cstrs dangling - in - (ctx', us, algs, insts, cstrs'), b + let enforce_uppers ((ctx,us,algs,insts,cstrs), b as acc) = + match LMap.find u right with + | exception Not_found -> acc + | upper -> + let upper = List.filter (fun (d, r) -> not (LMap.mem r us)) upper in + let cstrs = enforce_uppers upper b.lbound cstrs in + (ctx, us, algs, insts, cstrs), b in - if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower)) - else - let lbound = compute_lbound left in - match lbound with - | None -> (* Nothing to do *) - acc' (acc, (true, false, Universe.make u, lower)) - | Some lbound -> - try acc' (instantiate_lbound lbound) - with Failure _ -> acc' (acc, (true, false, Universe.make u, lower)) - and aux (ctx', us, algs, seen, cstrs as acc) u = + if not (LSet.mem u ctx) + then enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + else + let lbound = compute_lbound left in + match lbound with + | None -> (* Nothing to do *) + enforce_uppers (acc, {enforce=true;alg=false;lbound=Universe.make u; lower}) + | Some lbound -> + try enforce_uppers (instantiate_lbound lbound) + with UpperBoundedAlg -> + enforce_uppers (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + and aux (ctx, us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u in - LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> + LMap.fold (fun u v (ctx, us, algs, seen, cstrs as acc) -> if v == None then fst (aux acc u) - else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) + else LSet.remove u ctx, us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) let normalize_context_set g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in - let uf = UF.create () in (** Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> - if d == Le then - if Univ.Level.is_small l then - if is_set_minimization () && LSet.mem r ctx then - (Constraint.add cstr smallles, noneqs) - else (smallles, noneqs) - else if Level.is_small r then - if Level.is_prop r then - raise (Univ.UniverseInconsistency - (Le,Universe.make l,Universe.make r,None)) - else (smallles, Constraint.add (l,Eq,r) noneqs) - else (smallles, Constraint.add cstr noneqs) - else (smallles, Constraint.add cstr noneqs)) - csts (Constraint.empty, Constraint.empty) + Constraint.partition (fun (l,d,r) -> d == Le && Level.is_small l) csts + in + let smallles = if is_set_minimization () + then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx) smallles + else Constraint.empty in - let csts = + let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) - let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) + let g = LSet.fold (fun v g -> UGraph.add_universe v false g) ctx UGraph.initial_universes in - let g = - Univ.Constraint.fold - (fun (l, d, r) g -> - let g = - if not (Level.is_small l || LSet.mem l ctx) then - try UGraph.add_universe l false g - with UGraph.AlreadyDeclared -> g - else g - in - let g = - if not (Level.is_small r || LSet.mem r ctx) then - try UGraph.add_universe r false g - with UGraph.AlreadyDeclared -> g - else g - in g) csts g + let add_soft u g = + if not (Level.is_small u || LSet.mem u ctx) + then try UGraph.add_universe u false g with UGraph.AlreadyDeclared -> g + else g + in + let g = Constraint.fold + (fun (l, d, r) g -> add_soft r (add_soft l g)) + csts g in - let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in + let g = UGraph.merge_constraints csts g in UGraph.constraints_of_universes g in + (* We ignore the trivial Prop/Set <= i constraints. *) let noneqs = - Constraint.fold (fun (l,d,r as cstr) noneqs -> - if d == Eq then (UF.union l r uf; noneqs) - else (* We ignore the trivial Prop/Set <= i constraints. *) - if d == Le && Univ.Level.is_small l then noneqs - else if Univ.Level.is_prop l && d == Lt && Univ.Level.is_set r - then noneqs - else Constraint.add cstr noneqs) - csts Constraint.empty + Constraint.filter + (fun (l,d,r) -> not ((d == Le && Level.is_small l) || + (Level.is_prop l && d == Lt && Level.is_set r))) + csts in let noneqs = Constraint.union noneqs smallles in - let partition = UF.partition uf in let flex x = LMap.mem x us in let ctx, us, eqs = List.fold_left (fun (ctx, us, cstrs) s -> let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) global + Constraint.add (canon, Eq, g) cst) global cstrs in (* Also add equalities for rigid variables *) let cstrs = LSet.fold (fun g cst -> - Constraint.add (canon, Univ.Eq, g) cst) rigid + Constraint.add (canon, Eq, g) cst) rigid cstrs in let canonu = Some (Universe.make canon) in diff --git a/engine/universes.mli b/engine/universes.mli index 4823c57463..a0a7749f8b 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -162,8 +162,6 @@ val extend_context : 'a in_universe_context_set -> ContextSet.t -> (a global one if there is one) and transitively saturate the constraints w.r.t to the equalities. *) -module UF : Unionfind.PartitionSig with type elt = Level.t - val level_subst_of : universe_subst_fn -> universe_level_subst_fn val subst_univs_constraints : universe_subst_fn -> Constraint.t -> Constraint.t |