diff options
Diffstat (limited to 'kernel/univ.ml')
| -rw-r--r-- | kernel/univ.ml | 76 |
1 files changed, 30 insertions, 46 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index be21381b7..9782312ca 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -456,10 +456,10 @@ struct let super l = if is_small l then type1 else - List.smartmap (fun x -> Expr.successor x) l + List.Smart.map (fun x -> Expr.successor x) l let addn n l = - List.smartmap (fun x -> Expr.addn n x) l + List.Smart.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with @@ -490,39 +490,6 @@ struct in List.fold_right (fun a acc -> aux a acc) u [] - (** [max_var_pred p u] returns the maximum variable level in [u] satisfying - [p], -1 if not found *) - let rec max_var_pred p u = - let open Level in - match u with - | [] -> -1 - | (v, _) :: u -> - match var_index v with - | Some i when p i -> max i (max_var_pred p u) - | _ -> max_var_pred p u - - let rec remap_var u i j = - let open Level in - match u with - | [] -> [] - | (v, incr) :: u when var_index v = Some i -> - (Level.var j, incr) :: remap_var u i j - | _ :: u -> remap_var u i j - - let rec compact u max_var i = - if i >= max_var then (u,[]) else - let j = max_var_pred (fun j -> j < i) u in - if Int.equal i (j+1) then - let (u,s) = compact u max_var (i+1) in - (u, i :: s) - else - let (u,s) = compact (remap_var u i j) max_var (i+1) in - (u, j+1 :: s) - - let compact u = - let max_var = max_var_pred (fun _ -> true) u in - compact u max_var 0 - (* Returns the formal universe that is greater than the universes u and v. Used to type the products. *) let sup x y = merge_univs x y @@ -533,7 +500,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map let map = List.map end @@ -574,11 +541,11 @@ let constraint_type_ord c1 c2 = match c1, c2 with (* Universe inconsistency: error raised when trying to enforce a relation that would create a cycle in the graph of universes. *) -type univ_inconsistency = constraint_type * universe * universe * explanation option +type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option exception UniverseInconsistency of univ_inconsistency -let error_inconsistency o u v (p:explanation option) = +let error_inconsistency o u v p = raise (UniverseInconsistency (o,make u,make v,p)) (* Constraints and sets of constraints. *) @@ -886,7 +853,7 @@ struct let length a = Array.length a let subst_fn fn t = - let t' = CArray.smartmap fn t in + let t' = CArray.Smart.map fn t in if t' == t then t else of_array t' let levels x = LSet.of_array x @@ -923,11 +890,11 @@ let subst_instance_level s l = | _ -> l let subst_instance_instance s i = - Array.smartmap (fun l -> subst_instance_level s l) i + Array.Smart.map (fun l -> subst_instance_level s l) i let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1133,7 +1100,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1208,6 +1175,20 @@ let abstract_cumulativity_info (univs, variance) = let subst, univs = abstract_universes univs in subst, (univs, variance) +let rec compact_univ s vars i u = + match u with + | [] -> (s, List.rev vars) + | (lvl, _) :: u -> + match Level.var_index lvl with + | Some k when not (LMap.mem lvl s) -> + let lvl' = Level.var i in + compact_univ (LMap.add lvl lvl' s) (k :: vars) (i+1) u + | _ -> compact_univ s vars i u + +let compact_univ u = + let (s, s') = compact_univ LMap.empty [] 0 u in + (subst_univs_level_universe s u, s') + (** Pretty-printing *) let pr_constraints prl = Constraint.pr prl @@ -1254,13 +1235,16 @@ let explain_universe_inconsistency prl (o,u,v,p) = | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" in let reason = match p with - | None | Some [] -> mt() + | None -> mt() | Some p -> - str " because" ++ spc() ++ pr_uni v ++ + let p = Lazy.force p in + if p = [] then mt () + else + str " because" ++ spc() ++ pr_uni v ++ prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v) - p ++ + p ++ (if Universe.equal (snd (List.last p)) u then mt() else - (spc() ++ str "= " ++ pr_uni u)) + (spc() ++ str "= " ++ pr_uni u)) in str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++ pr_rel o ++ spc() ++ pr_uni v ++ reason |