diff options
-rw-r--r-- | kernel/reduction.ml | 90 | ||||
-rw-r--r-- | kernel/reduction.mli | 2 | ||||
-rw-r--r-- | pretyping/coercion.ml | 8 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 3 | ||||
-rw-r--r-- | pretyping/evd.ml | 2 |
5 files changed, 55 insertions, 50 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index a4d8872fe..03fe895e5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -26,6 +26,8 @@ open Environ open Closure open Esubst +let left2right = ref false + let conv_key k = match k with | VarKey id -> VarKey id @@ -191,10 +193,11 @@ let sort_cmp_universes pb s0 s1 (u, check) = let convert_instances flex u u' (s, check) = (check.compare_instances flex u u' s, check) -let conv_table_key k1 k2 cuniv = +let conv_table_key infos k1 k2 cuniv = match k1, k2 with | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' -> - convert_instances true u u' cuniv + let flex = evaluable_constant cst (info_env infos) in + convert_instances flex u u' cuniv | _ -> raise NotConvertible let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = @@ -203,7 +206,10 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = | (z1::s1, z2::s2) -> let cu1 = cmp_rec s1 s2 cuniv in (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 + | (Zlapp a1,Zlapp a2) -> + if !left2right then + Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2 + else Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> if not (eq_constant c1 c2) then raise NotConvertible @@ -320,29 +326,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> - (try (* try first intensional equality *) - if eq_table_key fl1 fl2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - else - (let cuniv = conv_table_key fl1 fl2 cuniv in - convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) - with NotConvertible -> - (* else the oracle tells which constant is to be expanded *) - let (app1,app2) = - if Conv_oracle.oracle_order (Closure.oracle_of_infos infos) l2r (conv_key fl1) (conv_key fl2) then - match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) - | None -> - (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) - | None -> raise NotConvertible) - else - match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) - | None -> - (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) - | None -> raise NotConvertible) in - eqappr cv_pb l2r infos app1 app2 cuniv) + (try + if eq_table_key fl1 fl2 then (* try first intensional equality *) + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + else (let cuniv = conv_table_key infos fl1 fl2 cuniv in + convert_stacks l2r infos lft1 lft2 v1 v2 cuniv) + with NotConvertible -> + (* else the oracle tells which constant is to be expanded *) + let oracle = Closure.oracle_of_infos infos in + let (app1,app2) = + if Conv_oracle.oracle_order oracle l2r (conv_key fl1) (conv_key fl2) then + match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd def1 v1), appr2) + | None -> + (match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd def2 v2)) + | None -> raise NotConvertible) + else + match unfold_reference infos fl2 with + | Some def2 -> (appr1, (lft2, whd def2 v2)) + | None -> + (match unfold_reference infos fl1 with + | Some def1 -> ((lft1, whd def1 v1), appr2) + | None -> raise NotConvertible) + in + eqappr cv_pb l2r infos app1 app2 cuniv) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, @@ -418,12 +426,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some def1 -> eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv | None -> - match c2 with + match c2 with | FConstruct ((ind2,j2),u2) -> (try - let v2, v1 = - eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let v2, v1 = + eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -432,12 +440,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some def2 -> eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv | None -> - match c1 with + match c1 with | FConstruct ((ind1,j1),u1) -> - (try let v1, v2 = - eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) + (try let v1, v2 = + eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) @@ -459,16 +467,16 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> (try - let v1, v2 = - eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let v1, v2 = + eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (_, FConstruct ((ind2,j2),u2)) -> (try - let v2, v1 = - eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + let v2, v1 = + eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) -> diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b45dca03e..cfeafd75c 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -10,6 +10,8 @@ open Term open Context open Environ +val left2right : bool ref + (*********************************************************************** s Reduction functions *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3b82e52a3..dfaff327a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -445,10 +445,8 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = try (the_conv_x_leq env t' c1 evd, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail ?(cumul=true) loc env evd rigidonly v t c1 = - try if cumul then - (the_conv_x_leq env t c1 evd, v) - else (the_conv_x env t c1 evd, v) +let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = + try (the_conv_x_leq env t c1 evd, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> @@ -468,7 +466,7 @@ let rec inh_conv_coerce_to_fail ?(cumul=true) loc env evd rigidonly v t c1 = | _ -> name in let env1 = push_rel (name,None,u1) env in let (evd', v1) = - inh_conv_coerce_to_fail ~cumul:false loc env1 evd rigidonly + inh_conv_coerce_to_fail loc env1 evd rigidonly (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in let v1 = Option.get v1 in let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d6e8a9660..b0718ed7e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -135,9 +135,6 @@ let has_undefined_evars or_sorts evd t = has_ev c; Array.iter has_ev args | Evar_empty -> raise NotInstantiatedEvar) - | Ind (_,l) | Const (_,l) | Construct (_,l) - when or_sorts && not (Univ.Instance.is_empty l) -> - raise Not_found | _ -> iter_constr has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ed3459a52..a003716f9 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1589,7 +1589,7 @@ let pr_evar_universe_context ctx = (str"UNIVERSES:"++brk(0,1)++ h 0 (Univ.pr_universe_context_set ctx.uctx_local) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++h 0 (Univ.LSet.pr ctx.uctx_univ_algebraic) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ - h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables)) + h 0 (Universes.pr_universe_opt_subst ctx.uctx_univ_variables) ++ fnl()) let print_env_short env = let pr_body n = function |