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(-) (limited to 'interp') 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 +++---- 4 files changed, 11 insertions(+), 12 deletions(-) (limited to 'interp') 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 -- 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 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp') 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 -- cgit v1.2.3