diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 47 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 23 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 1 |
3 files changed, 44 insertions, 27 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 229b40a0d1..0fdad58309 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -99,7 +99,7 @@ let check_conv_record (t1,l1) (t2,l2) = lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] | _ -> - let c2 = try global_of_constr t2 with _ -> raise Not_found in + let c2 = global_of_constr t2 in lookup_canonical_conversion (proji, Const_cs c2),l2 with Not_found -> lookup_canonical_conversion (proji,Default_cs),[] @@ -109,11 +109,11 @@ let check_conv_record (t1,l1) (t2,l2) = let params1, c1, extra_args1 = match list_chop (List.length params) l1 with | params1, c1::extra_args1 -> params1, c1, extra_args1 - | _ -> assert false in + | _ -> raise Not_found in let us2,extra_args2 = list_chop (List.length us) l2_effective in c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1, (n,applist(t2,l2)) - with _ -> + with Failure _ | Not_found -> raise Not_found (* Precondition: one of the terms of the pb is an uninstantiated evar, @@ -272,33 +272,42 @@ and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = ise_try evd [f1; f4] | MaybeFlexible flex1, MaybeFlexible flex2 -> - let f2 i = - if flex1 = flex2 then - ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2 - else (i,false) - and f3 i = + let f1 i = + if l1 <> [] && l2 <> [] then + ise_list2 i (fun i -> evar_conv_x env i CONV) + (flex1::l1) (flex2::l2) + else + (i,false) + and f2 i = (try conv_record env i (try check_conv_record appr1 appr2 with Not_found -> check_conv_record appr2 appr1) with Not_found -> (i,false)) - and f4 i = + and f3 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant - only if necessary) *) - let val2 = - match kind_of_term flex1 with - Lambda _ -> None - | _ -> eval_flexible_term env flex2 in - match val2 with + only if necessary) or the second argument is potentially + usable as a canonical projection *) + if isLambda flex1 or is_canonical_projection flex2 then + match eval_flexible_term env flex1 with + | Some v1 -> + evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 + | None -> + match eval_flexible_term env flex2 with + | Some v2 -> + evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) + | None -> (i,false) + else + match eval_flexible_term env flex2 with | Some v2 -> evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) | None -> match eval_flexible_term env flex1 with - | Some v1 -> - evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 - | None -> (i,false) + | Some v1 -> + evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 + | None -> (i,false) in - ise_try evd [f2; f3; f4] + ise_try evd [f1; f2; f3] | Flexible ev1, Rigid _ -> if diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 9681a7a63d..7dbbf99334 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -126,10 +126,11 @@ type cs_pattern = | Sort_cs of sorts_family | Default_cs -let object_table = - (ref [] : ((global_reference * cs_pattern) * obj_typ) list ref) +let object_table = ref (Refmap.empty : (cs_pattern * obj_typ) list Refmap.t) -let canonical_projections () = !object_table +let canonical_projections () = + Refmap.fold (fun x -> List.fold_right (fun (y,c) acc -> ((x,y),c)::acc)) + !object_table [] let keep_true_projections projs kinds = map_succeed (function (p,true) -> p | _ -> failwith "") @@ -183,9 +184,10 @@ let compute_canonical_projections (con,ind) = let open_canonical_structure i (_,o) = if i=1 then let lo = compute_canonical_projections o in - List.iter (fun (o,_ as x) -> - if not (List.mem_assoc o !object_table) then - object_table := x :: (!object_table)) lo + List.iter (fun ((proj,cs_pat),s) -> + let l = try Refmap.find proj !object_table with Not_found -> [] in + let l' = list_add_set (cs_pat,s) l in + object_table := Refmap.add proj l' !object_table) lo let cache_canonical_structure o = open_canonical_structure 1 o @@ -241,7 +243,12 @@ let declare_canonical_structure ref = let outCanonicalStructure x = fst (outCanonStruct x) -let lookup_canonical_conversion o = List.assoc o !object_table +let lookup_canonical_conversion (proj,pat) = + List.assoc pat (Refmap.find proj !object_table) + +let is_canonical_projection c = + try Refmap.mem (global_of_constr c) !object_table + with Not_found -> false let freeze () = !structure_table, !projection_table, !object_table @@ -251,7 +258,7 @@ let unfreeze (s,p,o) = let init () = structure_table := Indmap.empty; projection_table := Cmap.empty; - object_table:=[] + object_table := Refmap.empty let _ = init() diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 348407ae11..d41ede8bbd 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -53,5 +53,6 @@ val cs_pattern_of_constr : constr -> cs_pattern * int * constr list val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ val declare_canonical_structure : global_reference -> unit +val is_canonical_projection : constr -> bool val canonical_projections : unit -> ((global_reference * cs_pattern) * obj_typ) list |