diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 19:47:48 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
commit | a7153b347f8196122394e9ce912055cdf9e575ae (patch) | |
tree | 50b3d27f0165e8fd8748f48a5f087374677fb14c /engine | |
parent | a51dda2344679dc6d9145f3f34acad29721f6c75 (diff) |
Move solve_constraint_system near its only use site (comInductive)
Diffstat (limited to 'engine')
-rw-r--r-- | engine/universes.ml | 67 | ||||
-rw-r--r-- | engine/universes.mli | 5 |
2 files changed, 0 insertions, 72 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 29c9bd017..01660fe04 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -717,73 +717,6 @@ let refresh_constraints univs (ctx, cstrs) = cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') - -(**********************************************************************) -(* Tools for sort-polymorphic inductive types *) - -(* Miscellaneous functions to remove or test local univ assumed to - occur only in the le constraints *) - -(* - 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 -> univ_level_mem u v - | None -> false - -let solve_constraints_system levels level_bounds level_min = - let open Univ in - let levels = - Array.mapi (fun i o -> - match o with - | Some u -> - (match Universe.level u with - | Some u -> Some u - | _ -> level_bounds.(i) <- Universe.sup level_bounds.(i) u; None) - | None -> None) - 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)); - done; - done; - v - (** Deprecated *) (** UnivNames *) diff --git a/engine/universes.mli b/engine/universes.mli index da4a00751..bd315f277 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -124,11 +124,6 @@ val refresh_constraints : UGraph.t -> ContextSet.t -> ContextSet.t * UGraph.t val pr_universe_opt_subst : universe_opt_subst -> Pp.t -(** {6 Support for template polymorphism } *) - -val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array -> - Universe.t array - (** *********************************** Deprecated *) [@@@ocaml.warning "-3"] |