diff options
| -rw-r--r-- | pretyping/evarconv.ml | 47 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 23 | ||||
| -rwxr-xr-x | pretyping/recordops.mli | 1 | ||||
| -rw-r--r-- | test-suite/success/CanonicalStructure.v | 17 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 5 |
5 files changed, 66 insertions, 27 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 229b40a0d..0fdad5830 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 9681a7a63..7dbbf9933 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 348407ae1..d41ede8bb 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 diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v index 44d21b83b..b8cae4719 100644 --- a/test-suite/success/CanonicalStructure.v +++ b/test-suite/success/CanonicalStructure.v @@ -12,3 +12,20 @@ Record Silly (X : Set) : Set := mkSilly { x : X }. Definition anotherMk := mkSilly. Definition struct := anotherMk nat 3. Canonical Structure struct. + +(* Intertwinning canonical structures and delta-expansion *) +(* Assia's short example *) + +Open Scope bool_scope. + +Set Implicit Arguments. + +Structure test_struct : Type := mk_test {dom :> Type; f : dom -> dom -> bool}. + +Notation " x != y":= (f _ x y)(at level 10). + +Canonical Structure bool_test := mk_test (fun x y => x || y). + +Definition b := bool. + +Check (fun x : b => x != x). diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 082cbfbe1..3bc9c7f9e 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -198,6 +198,11 @@ Goal forall x : nat, F1 x -> G1 x. refine (fun x H => proj2 (_ x H) _). Abort. +(* First-order unification between beta-redex (is it useful ?) *) + +Check fun (y: (forall x:((fun y:Type => bool) nat), True)) + (z: (fun z:Type => bool) _) => y z. + (* Remark: the following example does not succeed any longer in 8.2 because, the algorithm is more general and does exclude a solution that it should exclude for typing reason. Handling of types and backtracking is still to |