From c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 25 Feb 2018 16:28:00 +0100 Subject: [VM] Unify Const_sorts and Const_type, and remove Vsort. This simplifies the representation of values, and brings it closer to the ones of the native compiler. --- kernel/vconv.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/vconv.ml') diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8c7658147..ad9aa4267 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -44,7 +44,6 @@ let rec conv_val env pb k v1 v2 cu = and conv_whd env pb k whd1 whd2 cu = (* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *) match whd1, whd2 with - | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu | Vuniv_level _ , _ | _ , Vuniv_level _ -> (** Both of these are invalid since universes are handled via @@ -81,7 +80,7 @@ and conv_whd env pb k whd1 whd2 cu = (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu - | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ + | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible @@ -119,8 +118,9 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Atype _ , _ | _, Atype _ -> assert false - | Aind _, _ | Aid _, _ -> raise NotConvertible + | Asort s1, Asort s2 -> + sort_cmp_universes env pb s1 s2 cu + | Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env k stk1 stk2 cu = match stk1, stk2 with -- cgit v1.2.3