diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 12 | ||||
| -rw-r--r-- | engine/uState.ml | 6 | ||||
| -rw-r--r-- | engine/univMinim.ml | 11 |
3 files changed, 20 insertions, 9 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 0923ab6f4b..467b269e37 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -233,13 +233,13 @@ let pr_evar_universe_context ctx = if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ + h (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ - h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ + h (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ + h (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++ str "WEAK CONSTRAINTS:"++brk(0,1)++ - h 0 (UState.pr_weak prl ctx) ++ fnl ()) + h (UState.pr_weak prl ctx) ++ fnl ()) let print_env_short env sigma = let print_constr = print_kconstr in @@ -316,14 +316,14 @@ let pr_evar_list env sigma l = | Some ev' -> str " (aliased to " ++ Evar.print ev' ++ str ")" in let pr (ev, evi) = - h 0 (Evar.print ev ++ + h (Evar.print ev ++ str "==" ++ pr_evar_info env sigma evi ++ pr_alias ev ++ (if evi.evar_body == Evar_empty then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) in - h 0 (prlist_with_sep fnl pr l) + hv 0 (prlist_with_sep fnl pr l) let to_list d = let open Evd in diff --git a/engine/uState.ml b/engine/uState.ml index 8d1584cd95..9557111cfd 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -286,6 +286,10 @@ let process_universe_constraints ctx cstrs = 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 @@ -671,7 +675,7 @@ let subst_univs_context_with_def def usubst (ctx, cst) = (LSet.diff ctx def, UnivSubst.subst_univs_constraints usubst cst) let is_trivial_leq (l,d,r) = - Level.is_prop l && (d == Le || (d == Lt && Level.is_set r)) + Level.is_prop l && (d == Le || d == Lt) && Level.is_set r (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 1c7e716fc2..4ed6e97526 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -292,22 +292,29 @@ let is_bound l lbound = match lbound with | UGraph.Bound.Prop -> Level.is_prop l | UGraph.Bound.Set -> Level.is_set l +(* if [is_minimal u] then constraints [u <= v] may be dropped and get + used only for set_minimization. *) +let is_minimal ~lbound u = + Level.is_sprop u || Level.is_prop u || is_bound u lbound + (* TODO check is_small/sprop *) let normalize_context_set ~lbound g ctx us algs weak = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in (* Keep the Prop/Set <= i constraints separate for minimization *) let smallles, csts = - Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts + Constraint.partition (fun (l,d,r) -> d == Le && is_minimal ~lbound l) csts in let smallles = if get_set_minimization () then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles else Constraint.empty in + let smallles = Constraint.map (fun (_,_,r) -> Level.set, Le, r) smallles in let csts, partition = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) + let g = UGraph.initial_universes_with g in let g = LSet.fold (fun v g -> UGraph.add_universe ~lbound ~strict:false v g) - ctx UGraph.initial_universes + ctx g in let add_soft u g = if not (Level.is_small u || LSet.mem u ctx) |