diff options
| -rw-r--r-- | checker/values.ml | 2 | ||||
| -rw-r--r-- | engine/univGen.ml | 3 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 41 | ||||
| -rw-r--r-- | kernel/univ.mli | 4 | ||||
| -rw-r--r-- | test-suite/vio/univ_constraints_statements_body.v | 7 | ||||
| -rw-r--r-- | toplevel/ccompile.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
8 files changed, 37 insertions, 26 deletions
diff --git a/checker/values.ml b/checker/values.ml index f7a367b986..1353435181 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -87,7 +87,7 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|] (** kernel/univ *) -let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|] +let v_level_global = v_tuple "Level.Global.t" [|v_dp;String;Int|] let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *) [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|] let v_level = v_tuple "level" [|Int;v_raw_level|] diff --git a/engine/univGen.ml b/engine/univGen.ml index 278ca6bf34..b98c15f245 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -20,7 +20,8 @@ let new_univ_id, set_remote_new_univ_id = ~build:(fun n -> n) let new_univ_global () = - Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ()) + let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in + Univ.Level.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ()) let fresh_level () = Univ.Level.make (new_univ_global ()) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 6cb61174d3..ddbd5fa0a7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -717,7 +717,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false -let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) +let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) "" 0)) let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = let anon = Context.make_annot Anonymous Sorts.Relevant in diff --git a/kernel/univ.ml b/kernel/univ.ml index a2fd14025e..c2496f10b0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -38,20 +38,22 @@ struct open Names module UGlobal = struct - type t = DirPath.t * int + type t = DirPath.t * string * int - let make dp i = (DirPath.hcons dp,i) + let make dp s i = (DirPath.hcons dp,s,i) let repr x : t = x - let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' + let equal (d, s, i) (d', s', i') = Int.equal i i' && DirPath.equal d d' && String.equal s s' - let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d) + let hash (d,s,i) = Hashset.Combine.combine3 i (String.hash s) (DirPath.hash d) - let compare (d, i) (d', i') = - let c = Int.compare i i' in - if Int.equal c 0 then DirPath.compare d d' - else c + let compare (d, s, i) (d', s', i') = + if i < i' then -1 + else if i' < i then 1 + else let c = DirPath.compare d d' in + if not (Int.equal c 0) then c + else String.compare s s' end type t = @@ -84,10 +86,7 @@ struct | Set, Set -> 0 | Set, _ -> -1 | _, Set -> 1 - | Level (dp1, i1), Level (dp2, i2) -> - if i1 < i2 then -1 - else if i1 > i2 then 1 - else DirPath.compare dp1 dp2 + | Level l1, Level l2 -> UGlobal.compare l1 l2 | Level _, _ -> -1 | _, Level _ -> 1 | Var n, Var m -> Int.compare n m @@ -98,8 +97,8 @@ struct | SProp, SProp -> true | Prop, Prop -> true | Set, Set -> true - | Level (n,d), Level (n',d') -> - n == n' && d == d' + | Level (d,s,n), Level (d',s',n') -> + n == n' && s==s' && d == d' | Var n, Var n' -> n == n' | _ -> false @@ -107,9 +106,10 @@ struct | SProp as x -> x | Prop as x -> x | Set as x -> x - | Level (d,n) as x -> + | Level (d,s,n) as x -> + let s' = CString.hcons s in let d' = Names.DirPath.hcons d in - if d' == d then x else Level (d',n) + if s' == s && d' == d then x else Level (d',s',n) | Var _n as x -> x open Hashset.Combine @@ -119,7 +119,7 @@ struct | Prop -> combinesmall 1 1 | Set -> combinesmall 1 2 | Var n -> combinesmall 2 n - | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d)) + | Level l -> combinesmall 3 (UGlobal.hash l) end @@ -200,7 +200,10 @@ module Level = struct | SProp -> "SProp" | Prop -> "Prop" | Set -> "Set" - | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n + | Level (d,s,n) -> + Names.DirPath.to_string d ^ + (if CString.is_empty s then "" else "." ^ s) ^ + "." ^ string_of_int n | Var n -> "Var(" ^ string_of_int n ^ ")" let pr u = str (to_string u) @@ -218,7 +221,7 @@ module Level = struct let name u = match data u with - | Level (d, n) -> Some (d, n) + | Level l -> Some l | _ -> None end diff --git a/kernel/univ.mli b/kernel/univ.mli index 7286fc84cb..eeaa1ad62d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -15,8 +15,8 @@ sig module UGlobal : sig type t - val make : Names.DirPath.t -> int -> t - val repr : t -> Names.DirPath.t * int + val make : Names.DirPath.t -> string -> int -> t + val repr : t -> Names.DirPath.t * string * int val equal : t -> t -> bool val hash : t -> int val compare : t -> t -> int diff --git a/test-suite/vio/univ_constraints_statements_body.v b/test-suite/vio/univ_constraints_statements_body.v new file mode 100644 index 0000000000..6302adefc2 --- /dev/null +++ b/test-suite/vio/univ_constraints_statements_body.v @@ -0,0 +1,7 @@ +Definition T := Type. +Definition T1 : T := Type. + +Lemma x : True. +Proof. +exact (let a : T := Type in I). +Qed. diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 041097d2d3..46651d1d8b 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -194,7 +194,7 @@ let compile opts stm_options injections copts ~echo ~f_in ~f_out = if mode = BuildVio then dump_empty_vos() | Vio2Vo -> - + Flags.async_proofs_worker_id := "Vio2Vo"; let sum, lib, univs, tasks, proofs = Library.load_library_todo long_f_dot_in in let univs, proofs = Stm.finish_tasks long_f_dot_out univs proofs tasks in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index af40292f18..54f034c74e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -413,7 +413,7 @@ let sort_universes g = let levels = traverse LMap.empty [normalize Level.set, 0] in let max_level = LMap.fold (fun _ n accu -> max n accu) levels 0 in let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] in - let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp i))) in + let ulevels = Array.init max_level (fun i -> Level.(make (UGlobal.make dummy_mp "" i))) in let ulevels = Array.cons Level.set ulevels in (* Add the normal universes *) let fold (cur, ans) u = |