diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/engine.mllib | 1 | ||||
| -rw-r--r-- | engine/evar_kinds.ml | 39 | ||||
| -rw-r--r-- | engine/evarutil.ml | 46 | ||||
| -rw-r--r-- | engine/evarutil.mli | 23 | ||||
| -rw-r--r-- | engine/universes.ml | 257 | ||||
| -rw-r--r-- | engine/universes.mli | 2 |
6 files changed, 203 insertions, 165 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml new file mode 100644 index 000000000..c964ecf1f --- /dev/null +++ b/engine/evar_kinds.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Names +open Globnames +open Misctypes + +(** The kinds of existential variable *) + +(** Should the obligation be defined (opaque or transparent (default)) or + defined transparent and expanded in the term? *) + +type obligation_definition_status = Define of bool | Expand + +type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar + +type subevar_kind = Domain | Codomain | Body + +type t = + | ImplicitArg of global_reference * (int * Id.t option) + * bool (** Force inference *) + | BinderType of Name.t + | NamedHole of Id.t (* coming from some ?[id] syntax *) + | QuestionMark of obligation_definition_status * Name.t + | CasesType of bool (* true = a subterm of the type *) + | InternalHole + | TomatchTypeParameter of inductive * int + | GoalEvar + | ImpossibleCase + | MatchingVar of matching_var_kind + | VarInstance of Id.t + | SubEvar of subevar_kind option * Evar.t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 065b42bf6..710491f84 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 8bb0d2f61..e3e8f16c8 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 @@ -227,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 @@ -243,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/universes.ml b/engine/universes.ml index e5f9212a7..e98708724 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 @@ -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 4823c5746..a0a7749f8 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 |