From 067dc98d6395b5041680aa137909d9d5519908c9 Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sat, 19 Jan 2019 16:22:12 -0800 Subject: Simplify dispose_implicits --- interp/impargs.ml | 35 ++++++++++------------------------- 1 file changed, 10 insertions(+), 25 deletions(-) diff --git a/interp/impargs.ml b/interp/impargs.ml index d83a0ce918..6a0fa6f238 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -554,31 +554,16 @@ let add_section_impls vars extra_impls (cond,impls) = let discharge_implicits (_,(req,l)) = match req with | ImplLocal -> None - | ImplInteractive (ref,flags,exp) -> - (try - let vars = variable_section_segment_of_reference ref in - let extra_impls = impls_of_context vars in - let l' = [ref, List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in - Some (ImplInteractive (ref,flags,exp),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) - | ImplConstant (con,flags) -> - (try - let vars = variable_section_segment_of_reference (ConstRef con) in - let extra_impls = impls_of_context vars in - let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in - let l' = [ConstRef con,newimpls] in - Some (ImplConstant (con,flags),l') - with Not_found -> (* con not defined in this section *) Some (req,l)) - | ImplMutualInductive (kn,flags) -> - (try - let l' = List.map (fun (gr, l) -> - let vars = variable_section_segment_of_reference gr in - let extra_impls = impls_of_context vars in - (gr, - List.map (add_section_impls vars extra_impls) l)) l - in - Some (ImplMutualInductive (kn,flags),l') - with Not_found -> (* ref not defined in this section *) Some (req,l)) + | ImplMutualInductive _ | ImplInteractive _ | ImplConstant _ -> + let l' = + try + List.map (fun (gr, l) -> + let vars = variable_section_segment_of_reference gr in + let extra_impls = impls_of_context vars in + let newimpls = List.map (add_section_impls vars extra_impls) l in + (gr, newimpls)) l + with Not_found -> l in + Some (req,l') let rebuild_implicits (req,l) = match req with -- cgit v1.2.3 From 2c94706d810e371a416b8c2893eb88c40a09b75c Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Sat, 19 Jan 2019 20:41:24 -0800 Subject: Remove ref from some implicit_discharge_request --- interp/impargs.ml | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/interp/impargs.ml b/interp/impargs.ml index 6a0fa6f238..cb0f561c4c 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -499,9 +499,9 @@ type implicit_interactive_request = type implicit_discharge_request = | ImplLocal - | ImplConstant of Constant.t * implicits_flags + | ImplConstant of implicits_flags | ImplMutualInductive of MutInd.t * implicits_flags - | ImplInteractive of GlobRef.t * implicits_flags * + | ImplInteractive of implicits_flags * implicit_interactive_request let implicits_table = Summary.ref GlobRef.Map.empty ~name:"implicits" @@ -568,10 +568,10 @@ let discharge_implicits (_,(req,l)) = let rebuild_implicits (req,l) = match req with | ImplLocal -> assert false - | ImplConstant (con,flags) -> - let oldimpls = snd (List.hd l) in - let newimpls = compute_constant_implicits flags con in - req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] + | ImplConstant flags -> + let ref,oldimpls = List.hd l in + let newimpls = compute_global_implicits flags ref in + req, [ref, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags kn in let rec aux olds news = @@ -582,15 +582,14 @@ let rebuild_implicits (req,l) = | _, _ -> assert false in req, aux l newimpls - | ImplInteractive (ref,flags,o) -> + | ImplInteractive (flags,o) -> + let ref,oldimpls = List.hd l in (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let oldimpls = snd (List.hd l) in let newimpls = compute_global_implicits flags ref in [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let oldimpls = snd (List.hd l) in if flags.auto then let newimpls = List.hd (compute_global_implicits flags ref) in let p = List.length (snd newimpls) - userimplsize in @@ -625,7 +624,7 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with auto = true } in let req = - if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in + if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in declare_implicits_gen req flags ref let declare_var_implicits id = @@ -634,7 +633,7 @@ let declare_var_implicits id = let declare_constant_implicits con = let flags = !implicit_args in - declare_implicits_gen (ImplConstant (con,flags)) flags (ConstRef con) + declare_implicits_gen (ImplConstant flags) flags (ConstRef con) let declare_mib_implicits kn = let flags = !implicit_args in @@ -684,7 +683,7 @@ let declare_manual_implicits local ref ?enriching l = let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l])) let maybe_declare_manual_implicits local ref ?enriching l = @@ -743,7 +742,7 @@ let set_implicits local ref l = compute_implicit_statuses autoimpls imps)) l in let req = if is_local local ref then ImplLocal - else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) + else ImplInteractive(flags,ImplManual (List.length autoimpls)) in add_anonymous_leaf (inImplicits (req,[ref,l'])) let extract_impargs_data impls = -- cgit v1.2.3