diff options
Diffstat (limited to 'pretyping/evarconv.ml')
-rw-r--r-- | pretyping/evarconv.ml | 120 |
1 files changed, 31 insertions, 89 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 15151ca9b..fd52e0fa0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -13,37 +13,6 @@ open Classops open Recordops open Evarutil -(* Pb: Mach cannot type evar in the general case (all Const must be applied - * to Vars). But evars may be applied to Rels or other terms! This is the - * difference between type_of_const and type_of_const2. - *) - -(* This code (i.e. try_solve_pb, solve_pb, etc.) takes a unification - * problem, and tries to solve it. If it solves it, then it removes - * all the conversion problems, and re-runs conversion on each one, in - * the hopes that the new solution will aid in solving them. - * - * The kinds of problems it knows how to solve are those in which - * the usable arguments of an existential var are all themselves - * universal variables. - * The solution to this problem is to do renaming for the Var's, - * to make them match up with the Var's which are found in the - * hyps of the existential, to do a "pop" for each Rel which is - * not an argument of the existential, and a subst1 for each which - * is, again, with the corresponding variable. This is done by - * Tradevar.evar_define - * - * Thus, we take the arguments of the existential which we are about - * to assign, and zip them with the identifiers in the hypotheses. - * Then, we process all the Var's in the arguments, and sort the - * Rel's into ascending order. Then, we just march up, doing - * subst1's and pop's. - * - * NOTE: We can do this more efficiently for the relative arguments, - * by building a long substituend by hand, but this is a pain in the - * ass. - *) - let evar_apprec env isevars stack c = let rec aux s = let (t,stack as s') = Reduction.apprec env !isevars s in @@ -53,56 +22,31 @@ let evar_apprec env isevars stack c = | _ -> (t, list_of_stack stack) in aux (c, append_stack (Array.of_list stack) empty_stack) - -let conversion_problems = ref ([] : (conv_pb * constr * constr) list) - -let reset_problems () = conversion_problems := [] - -let add_conv_pb pb = (conversion_problems := pb::!conversion_problems) - -let get_changed_pb lev = - let (pbs,pbs1) = - List.fold_left - (fun (pbs,pbs1) pb -> - if status_changed lev pb then - (pb::pbs,pbs1) - else - (pbs,pb::pbs1)) - ([],[]) - !conversion_problems - in - conversion_problems := pbs1; - pbs - (* Precondition: one of the terms of the pb is an uninstanciated evar, * possibly applied to arguments. *) -let rec solve_pb env isevars pb = - match solve_simple_eqn (evar_conv_x env isevars CONV) isevars pb with - | Some lsp -> - let pbs = get_changed_pb lsp in - List.for_all - (fun (pbty,t1,t2) -> evar_conv_x env isevars pbty t1 t2) - pbs - | None -> (add_conv_pb pb; true) - -and evar_conv_x env isevars pbty term1 term2 = +let rec evar_conv_x env isevars pbty term1 term2 = let term1 = whd_ise1 !isevars term1 in let term2 = whd_ise1 !isevars term2 in - if eq_constr term1 term2 then +(* + if eq_constr term1 term2 then true else if (not(has_undefined_isevars isevars term1)) & not(has_undefined_isevars isevars term2) then is_fconv pbty env !isevars term1 term2 - else if ise_undefined isevars term1 or ise_undefined isevars term2 - then - solve_pb env isevars (pbty,term1,term2) + else +*) + (is_fconv pbty env !isevars term1 term2) or + if ise_undefined isevars term1 then + solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) + else if ise_undefined isevars term2 then + solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1) else let (t1,l1) = evar_apprec env isevars [] term1 in let (t2,l2) = evar_apprec env isevars [] term2 in - if (head_is_embedded_exist isevars t1 & not(is_eliminator t2)) - or (head_is_embedded_exist isevars t2 & not(is_eliminator t1)) + if (head_is_embedded_evar isevars t1 & not(is_eliminator t2)) + or (head_is_embedded_evar isevars t2 & not(is_eliminator t1)) then (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true) else @@ -111,15 +55,17 @@ and evar_conv_x env isevars pbty term1 term2 = and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) match (kind_of_term term1, kind_of_term term2) with - | IsEvar (sp1,al1), IsEvar (sp2,al2) -> + | IsEvar (sp1,al1 as ev1), IsEvar (sp2,al2 as ev2) -> let f1 () = if List.length l1 > List.length l2 then let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - solve_pb env isevars(pbty,applist(term1,deb1),term2) + solve_simple_eqn evar_conv_x env isevars + (pbty,ev2,applist(term1,deb1)) & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 else let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - solve_pb env isevars(pbty,term1,applist(term2,deb2)) + solve_simple_eqn evar_conv_x env isevars + (pbty,ev1,applist(term2,deb2)) & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 and f2 () = (sp1 = sp2) @@ -128,11 +74,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f1; f2] - | IsEvar (sp1,al1), IsConst cst2 -> + | IsEvar ev1, IsConst cst2 -> let f1 () = (List.length l1 <= List.length l2) & let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - solve_pb env isevars(pbty,term1,applist(term2,deb2)) + solve_simple_eqn evar_conv_x env isevars + (pbty,ev1,applist(term2,deb2)) & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 and f4 () = match constant_opt_value env cst2 with @@ -143,11 +90,12 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f1; f4] - | IsConst cst1, IsEvar (sp2,al2) -> + | IsConst cst1, IsEvar ev2 -> let f1 () = (List.length l2 <= List.length l1) & let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - solve_pb env isevars(pbty,applist(term1,deb1),term2) + solve_simple_eqn evar_conv_x env isevars + (pbty,ev2,applist(term1,deb1)) & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 and f4 () = match constant_opt_value env cst1 with @@ -182,16 +130,18 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = in ise_try isevars [f2; f3; f4] - | IsEvar (_,_), _ -> + | IsEvar ev1, _ -> (List.length l1 <= List.length l2) & let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - solve_pb env isevars(pbty,term1,applist(term2,deb2)) + solve_simple_eqn evar_conv_x env isevars + (pbty,ev1,applist(term2,deb2)) & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2 - | _, IsEvar (_,_) -> + | _, IsEvar ev2 -> (List.length l2 <= List.length l1) & let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - solve_pb env isevars(pbty,applist(term1,deb1),term2) + solve_simple_eqn evar_conv_x env isevars + (pbty,ev2,applist(term1,deb1)) & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2 | IsConst cst1, _ -> @@ -342,14 +292,6 @@ and check_conv_record (t1,l1) (t2,l2) = with _ -> raise Not_found -let the_conv_x env isevars t1 t2 = - is_conv env !isevars t1 t2 or evar_conv_x env isevars CONV t1 t2 - -(* Si conv_x_leq repond true, pourquoi diable est-ce qu'on repasse une couche - * avec evar_conv_x! Si quelqu'un comprend pourquoi, qu'il remplace ce - * commentaire. Sinon, il va y avoir un bon coup de balai. B.B. - *) -let the_conv_x_leq env isevars t1 t2 = - is_conv_leq env !isevars t1 t2 - or evar_conv_x env isevars CONV_LEQ t1 t2 +let the_conv_x env isevars t1 t2 = evar_conv_x env isevars CONV t1 t2 +let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CONV_LEQ t1 t2 |