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 /vernac/comInductive.ml | |
parent | a51dda2344679dc6d9145f3f34acad29721f6c75 (diff) |
Move solve_constraint_system near its only use site (comInductive)
Diffstat (limited to 'vernac/comInductive.ml')
-rw-r--r-- | vernac/comInductive.ml | 68 |
1 files changed, 67 insertions, 1 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 101298ef4..7d7f9e23f 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -178,6 +178,72 @@ let is_flexible_sort evd u = | Some l -> Evd.is_flexible_level evd l | None -> false +(**********************************************************************) +(* Tools for template 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.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 + let inductive_levels env evd poly arities inds = let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in let levels = List.map (fun (x,(ctx,a)) -> @@ -206,7 +272,7 @@ let inductive_levels env evd poly arities inds = in (* Take the transitive closure of the system of constructors *) (* level constraints and remove the recursive dependencies *) - let levels' = Universes.solve_constraints_system (Array.of_list levels) + let levels' = solve_constraints_system (Array.of_list levels) (Array.of_list cstrs_levels) (Array.of_list min_levels) in let evd, arities = |