diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 1 | ||||
| -rw-r--r-- | kernel/univ.ml | 100 | ||||
| -rw-r--r-- | kernel/univ.mli | 27 |
3 files changed, 13 insertions, 115 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index cc56428fa4..ee4a404a7c 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -320,7 +320,6 @@ let typecheck_inductive env ctx mie = in match s with | Type u when expltype (* Explicitly polymorphic *) -> - (* && no_upper_constraints u (Univ.UContext.constraints mie.mind_entry_universes) -> *) (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) (* We enforce [u >= lev] in case [lev] has a strict upper *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 6a11251b06..256ce5e92c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1657,110 +1657,18 @@ let sort_universes orig = in Array.fold_left_i fold sorted types -(**********************************************************************) -(* Tools for sort-polymorphic inductive types *) - (* Miscellaneous functions to remove or test local univ assumed to - occur only in the le constraints *) + occur in a universe *) -let remove_large_constraint u v min = +let univ_level_mem u v = Huniv.mem (Expr.make u) v + +let univ_level_rem u v min = match Universe.level v with | Some u' -> if Level.equal u u' then min else v | None -> Huniv.remove (Universe.Expr.make u) v -(* [is_direct_constraint u v] if level [u] is a member of universe [v] *) -let is_direct_constraint u v = - match Universe.level v with - | Some u' -> Level.equal u u' - | None -> - let expr = Universe.Expr.make u in - Universe.exists (Universe.Expr.equal expr) v - -(* - Solve a system of universe constraint of the form - - u_s11, ..., u_s1p1, w1 <= u1 - ... - u_sn1, ..., u_snpn, wn <= un - -where - - - the ui (1 <= i <= n) are universe variables, - - the sjk select subsets of the ui for each equations, - - the wi are arbitrary complex universes that do not mention the ui. -*) - -let is_direct_sort_constraint s v = match s with - | Some u -> is_direct_constraint u v - | None -> false - -let solve_constraints_system levels level_bounds level_min = - let levels = - Array.map (Option.map (fun u -> match level u with Some u -> u | _ -> anomaly (Pp.str"expects Atom"))) - levels in - let v = Array.copy level_bounds in - let nind = Array.length v in - let clos = Array.map (fun _ -> Int.Set.empty) levels in - (* First compute the transitive closure of the levels dependencies *) - for i=0 to nind-1 do - for j=0 to nind-1 do - if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then - clos.(i) <- Int.Set.add j clos.(i); - done; - done; - let rec closure () = - let continue = ref false in - Array.iteri (fun i deps -> - let deps' = - Int.Set.fold (fun j acc -> Int.Set.union acc clos.(j)) deps deps - in - if Int.Set.equal deps deps' then () - else (clos.(i) <- deps'; continue := true)) - clos; - if !continue then closure () - else () - in - closure (); - for i=0 to nind-1 do - for j=0 to nind-1 do - if not (Int.equal i j) && Int.Set.mem j clos.(i) then - (v.(i) <- Universe.sup v.(i) level_bounds.(j); - level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) - done; - for j=0 to nind-1 do - match levels.(j) with - | Some u -> v.(i) <- remove_large_constraint u v.(i) level_min.(i) - | None -> () - done - done; - v - -let subst_large_constraint u u' v = - match level u with - | Some u -> - (* if is_direct_constraint u v then *) - Universe.sup u' (remove_large_constraint u v type0m_univ) - (* else v *) - | _ -> - anomaly (Pp.str "expect a universe level") - -let subst_large_constraints = - List.fold_right (fun (u,u') -> subst_large_constraint u u') - -let no_upper_constraints u cst = - match level u with - | Some u -> - let test (u1, _, _) = - not (Int.equal (Level.compare u1 u) 0) in - Constraint.for_all test cst - | _ -> anomaly (Pp.str "no_upper_constraints") - (* Is u mentionned in v (or equals to v) ? *) -let univ_depends u v = - match atom u with - | Some u -> Huniv.mem u v - | _ -> anomaly (Pp.str"univ_depends given a non-atomic 1st arg") (**********************************************************************) (** Universe polymorphism *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 8166d75e62..9b68dbc8ce 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -129,6 +129,15 @@ val super : universe -> universe val universe_level : universe -> universe_level option +(** [univ_level_mem l u] Is l is mentionned in u ? *) + +val univ_level_mem : universe_level -> universe -> bool + +(** [univ_level_rem u v min] removes [u] from [v], resulting in [min] + if [v] was exactly [u]. *) + +val univ_level_rem : universe_level -> universe -> universe -> universe + (** {6 Graphs of universes. } *) type universes @@ -211,24 +220,6 @@ val constraints_of_universes : universes -> constraints val check_constraint : universes -> univ_constraint -> bool val check_constraints : constraints -> universes -> bool -(** {6 Support for old-style sort-polymorphism } *) - -val solve_constraints_system : universe option array -> universe array -> universe array -> - universe array - -val remove_large_constraint : universe_level -> universe -> universe -> universe - -val subst_large_constraint : universe -> universe -> universe -> universe - -val subst_large_constraints : - (universe * universe) list -> universe -> universe - -val no_upper_constraints : universe -> constraints -> bool - -(** Is u mentionned in v (or equals to v) ? *) - -val univ_depends : universe -> universe -> bool - (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) |