From 4197f42c15f0116eeb58df5b64b60f2fa6f6951f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 16 May 2019 13:59:25 +0200 Subject: Cleanup Implicit_quantifiers.implicit_application - fix misleading indentation - simplify "let a, b = e in a, b" -> "e" --- interp/implicit_quantifiers.ml | 48 ++++++++++++++++++++---------------------- 1 file changed, 23 insertions(+), 25 deletions(-) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index dffccf02fc..8d45290ac0 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -223,33 +223,31 @@ let implicit_application env ?(allow_partial=true) f ty = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in let gr = Nametab.locate qid in - if Typeclasses.is_class gr then Some (clapp, gr) else None + if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in - match is_class with - | None -> ty, env - | Some ({CAst.loc;v=(id, par, inst)}, gr) -> - let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in - let c, avoid = - let env = Global.env () in - let sigma = Evd.from_env env in - let c = class_info env sigma gr in - let (ci, rd) = c.cl_context in - if not allow_partial then - begin - let opt_succ x n = match x with - | None -> succ n - | Some _ -> n - in - let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in - let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in - if not (Int.equal needlen applen) then - mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd - end; - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid f par pars in - CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid - in c, avoid + match is_class with + | None -> ty, env + | Some ({CAst.loc;v=(id, par, inst)}, gr) -> + let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in + let env = Global.env () in + let sigma = Evd.from_env env in + let c = class_info env sigma gr in + let (ci, rd) = c.cl_context in + if not allow_partial then + begin + let opt_succ x n = match x with + | None -> succ n + | Some _ -> n + in + let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in + let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in + if not (Int.equal needlen applen) then + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd + end; + let pars = List.rev (List.combine ci rd) in + let args, avoid = combine_params avoid f par pars in + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" -- cgit v1.2.3 From 21269d0fef6794a672c36abdc5760889adc0e09c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 16 May 2019 14:21:37 +0200 Subject: binder_kind Generalized: remove 1st arg as it's always Implicit https://coq.inria.fr/distrib/current/refman/language/gallina-extensions.html#implicit-generalization >The generalizing binders `{ } and `( ) work similarly to their >explicit counterparts, only binding the generalized variables >implicitly, as maximally-inserted arguments. I guess this was meant to provide a way to get "(A:_) {B:bla A}" from "`{B:bla A}" (where A is generalizable) but there's no syntax for it so let's drop the ml side until such a syntax exists. --- interp/constrexpr.ml | 4 ++-- interp/constrexpr_ops.ml | 4 ++-- interp/constrintern.ml | 8 ++++---- interp/implicit_quantifiers.ml | 7 +++---- parsing/g_constr.mlg | 4 ++-- printing/ppconstr.ml | 3 +-- 6 files changed, 14 insertions(+), 16 deletions(-) diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 9f778d99e9..3ebbbdfb88 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -40,8 +40,8 @@ type explicitation = type binder_kind = | Default of binding_kind - | Generalized of binding_kind * binding_kind * bool - (** Inner binding, outer bindings, typeclass-specific flag + | Generalized of binding_kind * bool + (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses *) type abstraction_kind = AbsLambda | AbsPi diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 443473d5b6..bcb2f34377 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -34,8 +34,8 @@ let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with let binder_kind_eq b1 b2 = match b1, b2 with | Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 -| Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> - binding_kind_eq bk1 bk2 && binding_kind_eq ck1 ck2 && +| Generalized (ck1, b1), Generalized (ck2, b2) -> + binding_kind_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f06493b374..753065b7dd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -389,7 +389,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls} let intern_generalized_binder ?(global_level=false) intern_type ntnvars - env {loc;v=na} b b' t ty = + env {loc;v=na} b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = if t then ty, ids else @@ -403,7 +403,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars env fvs in let bl = List.map CAst.(map (fun id -> - (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) + (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None)))) fvs in let na = match na with @@ -433,8 +433,8 @@ let intern_assumption intern ntnvars env nal bk ty = (push_name_env ntnvars impls env locna, (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in + | Generalized (b',t) -> + let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b' t ty in env, b let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 8d45290ac0..f71ad14dd4 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -196,10 +196,9 @@ let combine_params avoid fn applied needed = user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") in aux [] avoid applied needed -let combine_params_freevar = - fun avoid (_, decl) -> - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) +let combine_params_freevar avoid (_, decl) = + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 4a9190c10a..6df97609f5 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -500,9 +500,9 @@ GRAMMAR EXTEND Gram | "{"; id=name; idl=LIST1 name; "}" -> { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) } | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc } | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc } + { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc } | "'"; p = pattern LEVEL "0" -> { let (p, ty) = match p.CAst.v with diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 78733784a7..9d3ed40f6c 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -339,8 +339,7 @@ let tag_var = tag Tag.variable let pr_binder many pr (nal,k,t) = match k with - | Generalized (b, b', t') -> - assert (match b with Implicit -> true | _ -> false); + | Generalized (b', t') -> begin match nal with |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' -- cgit v1.2.3 From 11533785773269d9632ef8925ed34ea2d541818b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 16 May 2019 14:32:09 +0200 Subject: Fix #10176: shadowing vs automatic class based generalization --- interp/implicit_quantifiers.ml | 6 ++++-- library/libnames.ml | 3 +++ library/libnames.mli | 3 +++ test-suite/bugs/closed/bug_10176.v | 7 +++++++ 4 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/bug_10176.v diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index f71ad14dd4..851109876b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -221,8 +221,10 @@ let implicit_application env ?(allow_partial=true) f ty = let is_class = try let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in - let gr = Nametab.locate qid in - if Typeclasses.is_class gr then Some (clapp, gr) else None + if Libnames.idset_mem_qualid qid env then None + else + let gr = Nametab.locate qid in + if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in match is_class with diff --git a/library/libnames.ml b/library/libnames.ml index 87c4de42e8..41b38e0378 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,6 +162,9 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath +let idset_mem_qualid qid s = + qualid_is_ident qid && Id.Set.mem (qualid_basename qid) s + (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index bbb4d2a058..7d77d95991 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,6 +88,9 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t +val idset_mem_qualid : qualid -> Id.Set.t -> bool +(** false when the qualid is not an ident *) + (** {6 ... } *) (** some preset paths *) diff --git a/test-suite/bugs/closed/bug_10176.v b/test-suite/bugs/closed/bug_10176.v new file mode 100644 index 0000000000..fdb0eb87a4 --- /dev/null +++ b/test-suite/bugs/closed/bug_10176.v @@ -0,0 +1,7 @@ +Class Foo (xxx:nat) := foo : nat. + +Lemma aa `{Foo} : nat. Abort. + +Fail Lemma xy (Foo:bool->Type) `{Foo} : nat. + +Fail Lemma yx (Fooo:bool->Type) `{Fooo} : nat. -- cgit v1.2.3 From 28dfb113c19f467fdc2b785d1c5a07a42aefa488 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 17 May 2019 14:03:33 +0200 Subject: Overlay for removing Generalized 1st arg --- dev/ci/user-overlays/10177-SkySkimmer-generalize.sh | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 dev/ci/user-overlays/10177-SkySkimmer-generalize.sh diff --git a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh new file mode 100644 index 0000000000..a89f6aca1b --- /dev/null +++ b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10177" ] || [ "$CI_BRANCH" = "generalize" ]; then + + quickchick_CI_REF=generalize + quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + +fi -- cgit v1.2.3