1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <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 Univ open UnivSubst type t = | ULe of Universe.t * Universe.t | UEq of Universe.t * Universe.t | ULub of Level.t * Level.t | UWeak of Level.t * Level.t let is_trivial = function | ULe (u, v) | UEq (u, v) -> Universe.equal u v | ULub (u, v) | UWeak (u, v) -> Level.equal u v let subst_univs fn = function | ULe (u, v) -> let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in if Universe.equal u' v' then None else Some (ULe (u',v')) | UEq (u, v) -> let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in if Universe.equal u' v' then None else Some (ULe (u',v')) | ULub (u, v) -> let u' = level_subst_of fn u and v' = level_subst_of fn v in if Level.equal u' v' then None else Some (ULub (u',v')) | UWeak (u, v) -> let u' = level_subst_of fn u and v' = level_subst_of fn v in if Level.equal u' v' then None else Some (UWeak (u',v')) module Set = struct module S = Set.Make( struct type nonrec t = t let compare x y = match x, y with | ULe (u, v), ULe (u', v') -> let i = Universe.compare u u' in if Int.equal i 0 then Universe.compare v v' else i | UEq (u, v), UEq (u', v') -> let i = Universe.compare u u' in if Int.equal i 0 then Universe.compare v v' else if Universe.equal u v' && Universe.equal v u' then 0 else i | ULub (u, v), ULub (u', v') | UWeak (u, v), UWeak (u', v') -> let i = Level.compare u u' in if Int.equal i 0 then Level.compare v v' else if Level.equal u v' && Level.equal v u' then 0 else i | ULe _, _ -> -1 | _, ULe _ -> 1 | UEq _, _ -> -1 | _, UEq _ -> 1 | ULub _, _ -> -1 | _, ULub _ -> 1 end) include S let add cst s = if is_trivial cst then s else add cst s let pr_one = let open Pp in function | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v | UWeak (u, v) -> Level.pr u ++ str " ~ " ++ Level.pr v let pr c = let open Pp in fold (fun cst pp_std -> pp_std ++ pr_one cst ++ fnl ()) c (str "") let equal x y = x == y || equal x y let subst_univs subst csts = fold (fun c -> Option.fold_right add (subst_univs subst c)) csts empty end type 'a accumulator = Set.t -> 'a -> 'a option type 'a constrained = 'a * Set.t type 'a constraint_function = 'a -> 'a -> Set.t -> Set.t let enforce_eq_instances_univs strict x y c = let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in let ax = Instance.to_array x and ay = Instance.to_array y in if Array.length ax != Array.length ay then CErrors.anomaly Pp.(str "Invalid argument: enforce_eq_instances_univs called with" ++ str " instances of different lengths."); CArray.fold_right2 (fun x y -> Set.add (mk x y)) ax ay c let to_constraints ~force_weak g s = let invalid () = raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes") in let tr cst acc = match cst with | ULub (l, l') -> Constraint.add (l, Eq, l') acc | UWeak (l, l') when force_weak -> Constraint.add (l, Eq, l') acc | UWeak _-> acc | ULe (l, l') -> begin match Universe.level l, Universe.level l' with | Some l, Some l' -> Constraint.add (l, Le, l') acc | None, Some _ -> enforce_leq l l' acc | _, None -> if UGraph.check_leq g l l' then acc else invalid () end | UEq (l, l') -> begin match Universe.level l, Universe.level l' with | Some l, Some l' -> Constraint.add (l, Eq, l') acc | None, _ | _, None -> if UGraph.check_eq g l l' then acc else invalid () end in Set.fold tr s Constraint.empty (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = (* spiwack: duplicates the code of [eq_constr_univs_infer] because I haven't find a way to factor the code without destroying pointer-equality optimisations in [eq_constr_univs_infer]. Pointer equality is not sufficient to ensure equality up to [kind1,kind2], because [kind1] and [kind2] may be different, typically evaluating [m] and [n] in different evar maps. *) let cstrs = ref accu in let eq_universes _ _ = UGraph.check_eq_instances univs in let eq_sorts s1 s2 = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in match fold (Set.singleton (UEq (u1, u2))) !cstrs with | None -> false | Some accu -> cstrs := accu; true in let rec eq_constr' nargs m n = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' nargs m n in let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' 0 m n in if res then Some !cstrs else None