From c8c1723747c7e0eb748861cc12aecca411848f4c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Sep 2020 12:25:02 +0200 Subject: First list in cl_context is just booleans Used only by implicit_quantifiers --- interp/implicit_quantifiers.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4016a3600e..c5324702dc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -150,12 +150,12 @@ let combine_params avoid applied needed = | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (LocalAssum ({binder_name=Name id}, _))) :: need -> + | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need -> aux (x :: ids) avoid app need - | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need + | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need - | _, (Some _, decl) :: need | [], (None, decl) :: need -> + | _, (true, decl) :: need | [], (false, decl) :: need -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in let t' = CAst.make @@ CRef (qualid_of_ident id',None) in aux (t' :: ids) (Id.Set.add id' avoid) app need -- cgit v1.2.3 From 661d84228fa1a6750b4a80f41c3e012e6de763bf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Sep 2020 12:32:31 +0200 Subject: Simplify Implicit_quantifiers.combine_params a bit --- interp/implicit_quantifiers.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index c5324702dc..0ed0b8a1a5 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -127,10 +127,7 @@ let combine_params avoid applied needed = List.partition (function (t, Some {CAst.loc;v=ExplByName id}) -> - let is_id (_, decl) = match RelDecl.get_name decl with - | Name id' -> Id.equal id id' - | Anonymous -> false - in + let is_id (_, decl) = Name.equal (Name id) (RelDecl.get_name decl) in if not (List.exists is_id needed) then user_err ?loc (str "Wrong argument name: " ++ Id.print id); true @@ -147,15 +144,13 @@ let combine_params avoid applied needed = | [], [] -> List.rev ids, avoid - | app, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> + | _, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (false, (LocalAssum ({binder_name=Name id}, _))) :: need -> - aux (x :: ids) avoid app need + | (x, _) :: app, (false, _) :: need -> aux (x :: ids) avoid app need - | x :: app, (false, _) :: need -> aux (fst x :: ids) avoid app need - - | _, (true, decl) :: need | [], (false, decl) :: need -> + | _, (true, decl) :: need + | [], (false, decl) :: need -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in let t' = CAst.make @@ CRef (qualid_of_ident id',None) in aux (t' :: ids) (Id.Set.add id' avoid) app need -- cgit v1.2.3 From 07b7bd7f8358d199b0464a673aec50dedae0a45d Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Sep 2020 12:50:37 +0200 Subject: Implicit_quantifiers don't use precomputed is_class data Fix #13117 We alternatively could fix the generation of the data with Existing Class but I prefer moving towards removing it. --- interp/implicit_quantifiers.ml | 47 +++++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 17 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 0ed0b8a1a5..0f05cc5e10 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -122,12 +122,24 @@ let next_name_away_from na avoid = | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon") | Name id -> make_fresh avoid (Global.env ()) id +let rec is_class_arg c = + let open Constr in + match kind c with + | Prod (_,_,c) + | Cast (c,_,_) + | LetIn (_,_,_,c) -> is_class_arg c + | _ -> + let c, _ = decompose_appvect c in + match destRef c with + | exception DestKO -> false + | r, _ -> is_class r + let combine_params avoid applied needed = let named, applied = List.partition (function (t, Some {CAst.loc;v=ExplByName id}) -> - let is_id (_, decl) = Name.equal (Name id) (RelDecl.get_name decl) in + let is_id decl = Name.equal (Name id) (RelDecl.get_name decl) in if not (List.exists is_id needed) then user_err ?loc (str "Wrong argument name: " ++ Id.print id); true @@ -138,25 +150,27 @@ let combine_params avoid applied needed = named in let rec aux ids avoid app need = - match app, need with - - | _, (_, LocalDef _) :: need -> aux ids avoid app need + match need with + | [] -> begin match app with + | [] -> List.rev ids, avoid + | (x, _) :: _ -> user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") + end - | [], [] -> List.rev ids, avoid + | LocalDef _ :: need -> aux ids avoid app need - | _, (_, (LocalAssum ({binder_name=Name id}, _))) :: need when Id.List.mem_assoc id named -> - aux (Id.List.assoc id named :: ids) avoid app need - | (x, _) :: app, (false, _) :: need -> aux (x :: ids) avoid app need + | LocalAssum ({binder_name=Name id}, _) :: need when Id.List.mem_assoc id named -> + aux (Id.List.assoc id named :: ids) avoid app need - | _, (true, decl) :: need - | [], (false, decl) :: need -> - let id' = next_name_away_from (RelDecl.get_name decl) avoid in - let t' = CAst.make @@ CRef (qualid_of_ident id',None) in - aux (t' :: ids) (Id.Set.add id' avoid) app need + | decl :: need -> + begin match app, is_class_arg (get_type decl) with + | (x, _) :: app, false -> aux (x :: ids) avoid app need - | (x,_) :: _, [] -> - user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") + | [], false | _, true -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + let t' = CAst.make @@ CRef (qualid_of_ident id',None) in + aux (t' :: ids) (Id.Set.add id' avoid) app need + end in aux [] avoid applied needed @@ -186,8 +200,7 @@ let implicit_application env ty = let sigma = Evd.from_env env in let c = class_info env sigma gr in let (ci, rd) = c.cl_context in - let pars = List.rev (List.combine ci rd) in - let args, avoid = combine_params avoid par pars in + let args, avoid = combine_params avoid par (List.rev rd) in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = -- cgit v1.2.3 From e23be6ebc7d9c9842f8c1036e145fb15c3154e17 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Sep 2020 12:54:59 +0200 Subject: Remove unused is_class info from cl_context --- interp/implicit_quantifiers.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 0f05cc5e10..2853eef5c5 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -199,8 +199,7 @@ let implicit_application env ty = 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 - let args, avoid = combine_params avoid par (List.rev rd) in + let args, avoid = combine_params avoid par (List.rev c.cl_context) in CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid let warn_ignoring_implicit_status = -- cgit v1.2.3