diff options
Diffstat (limited to 'kernel/vconv.ml')
-rw-r--r-- | kernel/vconv.ml | 50 |
1 files changed, 35 insertions, 15 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 2f6be0601..4610dbcb0 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -45,8 +45,15 @@ let rec conv_val env pb k v1 v2 cu = else conv_whd env pb k (whd_val v1) (whd_val 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 + ** special cases in the code. + **) + assert false | Vprod p1, Vprod p2 -> let cu = conv_val env CONV k (dom p1) (dom p2) cu in conv_fun env pb k (codom p1) (codom p2) cu @@ -81,26 +88,46 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = +(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with - | Aind ind1, Aind ind2 -> - if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2 + | Aind ((mi,i) as ind1) , Aind ind2 -> + if eq_ind ind1 ind2 && compare_stack stk1 stk2 then - conv_stack env k stk1 stk2 cu + if Environ.polymorphic_ind ind1 env + then + let mib = Environ.lookup_mind mi env in + let ulen = Univ.UContext.size mib.Declarations.mind_universes in + match stk1 , stk2 with + | [], [] -> assert (Int.equal ulen 0); cu + | Zapp args1 :: stk1' , Zapp args2 :: stk2' -> + assert (ulen <= nargs args1); + assert (ulen <= nargs args2); + let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in + let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in + let u1 = Univ.Instance.of_array u1 in + let u2 = Univ.Instance.of_array u2 in + let cu = convert_instances ~flex:false u1 u2 cu in + conv_arguments env ~from:ulen k args1 args2 + (conv_stack env k stk1' stk2' cu) + | _, _ -> assert false (* Should not happen if problem is well typed *) + else + conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> 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 -and conv_stack env k stk1 stk2 cu = +and conv_stack env ?from:(from=0) k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> conv_stack env k stk1 stk2 - (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) + (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in @@ -144,25 +171,18 @@ and conv_cofix env k cf1 cf2 cu = conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu else raise NotConvertible -and conv_arguments env k args1 args2 cu = +and conv_arguments env ?from:(from=0) k args1 args2 cu = if args1 == args2 then cu else let n = nargs args1 in if Int.equal n (nargs args2) then let rcu = ref cu in - for i = 0 to n - 1 do + for i = from to n - 1 do rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu done; !rcu else raise NotConvertible -let rec eq_puniverses f (x,l1) (y,l2) cu = - if f x y then conv_universes l1 l2 cu - else raise NotConvertible - -and conv_universes l1 l2 cu = - if Univ.Instance.equal l1 l2 then cu else raise NotConvertible - let vm_conv_gen cv_pb env univs t1 t2 = try let v1 = val_of_constr env t1 in |