diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 4 | ||||
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/universes.ml | 34 | ||||
| -rw-r--r-- | engine/universes.mli | 9 |
4 files changed, 19 insertions, 30 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index af22de5cd..20a7c80ea 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -842,12 +842,12 @@ let universe_rigidity evd l = else UnivRigid let normalize_universe evd = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.normalize_universe_opt_subst vars in normalize let normalize_universe_instance evd l = - let vars = ref (UState.subst evd.universes) in + let vars = UState.subst evd.universes in let normalize = Universes.level_subst_of (Universes.normalize_univ_variable_opt_subst vars) in Univ.Instance.subst_fn normalize l diff --git a/engine/uState.ml b/engine/uState.ml index 6c8dbe3f4..df50bae86 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -156,7 +156,7 @@ let process_universe_constraints ctx cstrs = let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let weak = ref ctx.uctx_weak_constraints in - let normalize = normalize_univ_variable_opt_subst vars in + let normalize u = normalize_univ_variable_opt_subst !vars u in let nf_constraint = function | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v) | UWeak (u, v) -> UWeak (level_subst_of normalize u, level_subst_of normalize v) diff --git a/engine/universes.ml b/engine/universes.ml index 938f5ad9c..a13663cba 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -605,31 +605,25 @@ let fresh_universe_context_set_instance ctx = let cst' = subst_univs_level_constraints subst cst in subst, (univs', cst') -let normalize_univ_variable ~find ~update = +let normalize_univ_variable ~find = let rec aux cur = let b = find cur in let b' = subst_univs_universe aux b in if Universe.equal b' b then b - else update cur b' + else b' in aux let normalize_univ_variable_opt_subst ectx = let find l = - match Univ.LMap.find l !ectx with + match Univ.LMap.find l ectx with | Some b -> b | None -> raise Not_found in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false - in normalize_univ_variable ~find ~update + normalize_univ_variable ~find let normalize_univ_variable_subst subst = - let find l = Univ.LMap.find l !subst in - let update l b = - assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in - normalize_univ_variable ~find ~update + let find l = Univ.LMap.find l subst in + normalize_univ_variable ~find let normalize_universe_opt_subst subst = let normlevel = normalize_univ_variable_opt_subst subst in @@ -640,13 +634,10 @@ let normalize_universe_subst subst = subst_univs_universe normlevel let normalize_opt_subst ctx = - let ectx = ref ctx in - let normalize = normalize_univ_variable_opt_subst ectx in - let () = - Univ.LMap.iter (fun u v -> - if Option.is_empty v then () - else try ignore(normalize u) with Not_found -> assert(false)) ctx - in !ectx + let normalize = normalize_universe_opt_subst ctx in + Univ.LMap.mapi (fun u -> function + | None -> None + | Some v -> Some (normalize v)) ctx type universe_opt_subst = Universe.t option universe_map @@ -655,7 +646,7 @@ let subst_univs_fn_puniverses f (c, u as cu) = if u' == u then cu else (c, u') let nf_evars_and_universes_opt_subst f subst = - let subst = normalize_univ_variable_opt_subst (ref subst) in + let subst = normalize_univ_variable_opt_subst subst in let lsubst = level_subst_of subst in let rec aux c = match kind c with @@ -975,7 +966,7 @@ let normalize_context_set g ctx us algs weak = (* Process weak constraints: when one side is flexible and the 2 universes are unrelated unify them. *) let ctx, us, g = UPairSet.fold (fun (u,v) (ctx, us, g as acc) -> - let norm = let us = ref us in level_subst_of (normalize_univ_variable_opt_subst us) in + let norm = level_subst_of (normalize_univ_variable_opt_subst us) in let u = norm u and v = norm v in let set_to a b = (LSet.remove a ctx, @@ -994,7 +985,6 @@ let normalize_context_set g ctx us algs weak = (* Noneqs is now in canonical form w.r.t. equality constraints, and contains only inequality constraints. *) let noneqs = - let us = ref us in let norm = level_subst_of (normalize_univ_variable_opt_subst us) in Constraint.fold (fun (u,d,v) noneqs -> let u = norm u and v = norm v in diff --git a/engine/universes.mli b/engine/universes.mli index e6bee42bb..df2e961d6 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -184,19 +184,18 @@ val normalize_univ_variables : universe_opt_subst -> val normalize_univ_variable : find:(Level.t -> Universe.t) -> - update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t -val normalize_univ_variable_opt_subst : universe_opt_subst ref -> +val normalize_univ_variable_opt_subst : universe_opt_subst -> (Level.t -> Universe.t) -val normalize_univ_variable_subst : universe_subst ref -> +val normalize_univ_variable_subst : universe_subst -> (Level.t -> Universe.t) -val normalize_universe_opt_subst : universe_opt_subst ref -> +val normalize_universe_opt_subst : universe_opt_subst -> (Universe.t -> Universe.t) -val normalize_universe_subst : universe_subst ref -> +val normalize_universe_subst : universe_subst -> (Universe.t -> Universe.t) (** Create a fresh global in the global environment, without side effects. |