diff options
author | 2017-07-13 15:05:48 +0200 | |
---|---|---|
committer | 2017-07-13 15:05:48 +0200 | |
commit | e3eb17a728d7b6874e67462e8a83fac436441872 (patch) | |
tree | c7932e27be16f4d2c20da8d61c3a61b101be7f70 /engine | |
parent | 9427b99b167842bc4a831def815c4824030d518f (diff) | |
parent | 95d65ae4ec8c01f0b8381dfa7029bb32a552bcb0 (diff) |
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Diffstat (limited to 'engine')
-rw-r--r-- | engine/universes.ml | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 28058aeed..fc441fd0b 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -282,28 +282,27 @@ let new_Type dp = mkType (new_univ dp) let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = - Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) - (AUContext.instance ctx) + let init _ = new_univ_level (Global.current_dirpath ()) in + Instance.of_array (Array.init (AUContext.size ctx) init) let fresh_instance_from_context ctx = let inst = fresh_universe_instance ctx in - let constraints = UContext.constraints (subst_instance_context inst ctx) in + let constraints = AUContext.instantiate inst ctx in inst, constraints let fresh_instance ctx = let ctx' = ref LSet.empty in - let inst = - Instance.subst_fn (fun v -> - let u = new_univ_level (Global.current_dirpath ()) in - ctx' := LSet.add u !ctx'; u) - (AUContext.instance ctx) + let init _ = + let u = new_univ_level (Global.current_dirpath ()) in + ctx' := LSet.add u !ctx'; u + in + let inst = Instance.of_array (Array.init (AUContext.size ctx) init) in !ctx', inst let existing_instance ctx inst = let () = - let a1 = Instance.to_array inst - and a2 = Instance.to_array (AUContext.instance ctx) in - let len1 = Array.length a1 and len2 = Array.length a2 in + let len1 = Array.length (Instance.to_array inst) + and len2 = AUContext.size ctx in if not (len1 == len2) then CErrors.user_err ~hdr:"Universes" (str "Polymorphic constant expected " ++ int len2 ++ @@ -317,7 +316,7 @@ let fresh_instance_from ctx inst = | Some inst -> existing_instance ctx inst | None -> fresh_instance ctx in - let constraints = UContext.constraints (subst_instance_context inst ctx) in + let constraints = AUContext.instantiate inst ctx in inst, (ctx', constraints) let unsafe_instance_from ctx = |