diff options
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 53 |
1 files changed, 32 insertions, 21 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 560beb6f..284af0cb 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -13,7 +13,7 @@ (* This file registers properties of records: projections and canonical structures *) -open Errors +open CErrors open Util open Pp open Names @@ -176,7 +176,7 @@ let cs_pattern_of_constr t = App (f,vargs) -> begin try Const_cs (global_of_constr f) , None, Array.to_list vargs - with e when Errors.noncritical e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b] @@ -184,11 +184,18 @@ let cs_pattern_of_constr t = | _ -> begin try Const_cs (global_of_constr t) , None, [] - with e when Errors.noncritical e -> raise Not_found + with e when CErrors.noncritical e -> raise Not_found end +let warn_projection_no_head_constant = + CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" + (fun (t,con_pp,proji_sp_pp) -> + strbrk "Projection value has no head constant: " + ++ Termops.print_constr t ++ strbrk " in canonical instance " + ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") + (* Intended to always succeed *) -let compute_canonical_projections (con,ind) = +let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in let u = Univ.UContext.instance ctx in @@ -213,13 +220,10 @@ let compute_canonical_projections (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - if Flags.is_verbose () then - (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - msg_warning (strbrk "No global reference exists for projection value" - ++ Termops.print_constr t ++ strbrk " in instance " - ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")); - l + if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + l end | _ -> l) [] lps in @@ -235,9 +239,15 @@ let pr_cs_pattern = function | Default_cs -> str "_" | Sort_cs s -> Termops.pr_sort_family s -let open_canonical_structure i (_,o) = - if Int.equal i 1 then - let lo = compute_canonical_projections o in +let warn_redundant_canonical_projection = + CWarnings.create ~name:"redundant-canonical-projection" ~category:"typechecker" + (fun (hd_val,prj,new_can_s,old_can_s) -> + strbrk "Ignoring canonical projection to " ++ hd_val + ++ strbrk " by " ++ prj ++ strbrk " in " + ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) + +let add_canonical_structure warn o = + let lo = compute_canonical_projections warn o in List.iter (fun ((proj,(cs_pat,_ as pat)),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in let ocs = try Some (assoc_pat cs_pat l) @@ -245,17 +255,18 @@ let open_canonical_structure i (_,o) = in match ocs with | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - if Flags.is_verbose () then let old_can_s = (Termops.print_constr cs.o_DEF) and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val - ++ strbrk " by " ++ prj ++ strbrk " in " - ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo + if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) + lo + +let open_canonical_structure i (_, o) = + if Int.equal i 1 then add_canonical_structure false o -let cache_canonical_structure o = - open_canonical_structure 1 o +let cache_canonical_structure (_, o) = + add_canonical_structure true o let subst_canonical_structure (subst,(cst,ind as obj)) = (* invariant: cst is an evaluable reference. Thus we can take *) @@ -299,7 +310,7 @@ let check_and_decompose_canonical_structure ref = | Construct ((indsp,1),u) -> indsp | _ -> error_not_structure ref in let s = try lookup_structure indsp with Not_found -> error_not_structure ref in - let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in + let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref; (sp,indsp) @@ -317,7 +328,7 @@ let is_open_canonical_projection env sigma (c,args) = (** Check if there is some canonical projection attached to this structure *) let _ = Refmap.find ref !object_table in try - let arg = whd_betadeltaiota env sigma (Stack.nth args n) in + let arg = whd_all env sigma (Stack.nth args n) in let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in not (isConstruct hd) with Failure _ -> false |