From 315fb733dd2e7827b3f3ea8a07b725b2a46519ff Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 16 Dec 2017 00:43:38 +0100 Subject: Merge code paths in interp_definition and cleanup a bit. --- vernac/comDefinition.ml | 92 ++++++++++++++++++++++++------------------------- 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index af5f095fb..d376696f7 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -48,57 +48,57 @@ let warn_implicits_in_term = strbrk "Implicit arguments declaration relies on type." ++ spc () ++ strbrk "The term declares more implicits than the type here.") +let check_imps ~impsty ~impsbody = + let b = + try + List.for_all (fun (key, (va:bool*bool*bool)) -> + (* Pervasives.(=) is OK for this type *) + Pervasives.(=) (List.assoc_f Impargs.explicitation_eq key impsty) va) + impsbody + with Not_found -> false + in + if not b then warn_implicits_in_term () + let interp_definition pl bl poly red_option c ctypopt = + let open EConstr in let env = Global.env() in + (* Explicitly bound universes and constraints *) let evd, decl = Univdecls.interp_univ_decl_opt env pl in + (* Build the parameters *) let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in - let nb_args = Context.Rel.nhyps ctx in - let evd,imps,ce = - match ctypopt with - None -> - (* Closing a definition, first build the term, this is straightforward *) - let env_bl = EConstr.push_rel_context ctx env in - let evd, (c, imps2) = interp_constr_evars_impls ~impls env_bl evd c in - let body = EConstr.(it_mkLambda_or_LetIn c ctx) in - (* Second, we need to prepare the universes, including minimization. Not fun *) - let evd,_ = Evarutil.nf_evars_and_universes evd in - let vars = EConstr.universes_of_constr env evd body in - let evd = Evd.restrict_universe_context evd vars in - let uctx = Evd.check_univ_decl ~poly evd decl in - (* Third, we substitute all the evars to store in the kernel. *) - let body = EConstr.to_constr evd body in - (* Fourth, store *) - evd, imps1@(Impargs.lift_implicits nb_args imps2), - definition_entry ~univs:uctx body - | Some ctyp -> - (* 1 *) - let evd, (ty, impsty) = interp_type_evars_impls ~impls env_bl evd ctyp in - let env_bl = EConstr.push_rel_context ctx env in - let evd, (c, imps2) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in - let body = EConstr.(it_mkLambda_or_LetIn c ctx) in - let typ = EConstr.(it_mkProd_or_LetIn ty ctx) in - (* 2 *) - let beq b1 b2 = if b1 then b2 else not b2 in - let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in - (* Check that all implicit arguments inferable from the term - are inferable from the type *) - let chk (key,va) = - impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) - in - if not (try List.for_all chk imps2 with Not_found -> false) - then warn_implicits_in_term (); - (* 3 *) - let evd, _ = Evarutil.nf_evars_and_universes evd in - let bodyvars = EConstr.universes_of_constr env evd body in - let tyvars = EConstr.universes_of_constr env evd ty in - let vars = Univ.LSet.union bodyvars tyvars in - let evd = Evd.restrict_universe_context evd vars in - let uctx = Evd.check_univ_decl ~poly evd decl in - (* 4 *) - let body,typ = EConstr.(to_constr evd body, to_constr evd typ) in - evd, imps1@(Impargs.lift_implicits nb_args impsty), - definition_entry ~types:typ ~univs:uctx body + (* Build the type *) + let evd, tyopt = Option.fold_left_map + (interp_type_evars_impls ~impls env_bl) + evd ctypopt + in + (* Build the body, and merge implicits from parameters and from type/body *) + let evd, c, imps, tyopt = + match tyopt with + | None -> + let evd, (c, impsbody) = interp_constr_evars_impls ~impls env_bl evd c in + evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsbody, None + | Some (ty, impsty) -> + let evd, (c, impsbody) = interp_casted_constr_evars_impls ~impls env_bl evd c ty in + check_imps ~impsty ~impsbody; + evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty + in + (* universe minimization *) + let evd = Evd.nf_constraints evd in + (* Substitute evars and universes, and add parameters. + Note: in program mode some evars may remain. *) + let ctx = List.map (EConstr.to_rel_decl evd) ctx in + let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in + let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in + (* Keep only useful universes. *) + let uvars_fold uvars c = + Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) in + let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in + let evd = Evd.restrict_universe_context evd uvars in + (* Check we conform to declared universes *) + let uctx = Evd.check_univ_decl ~poly evd decl in + (* We're done! *) + let ce = definition_entry ?types:tyopt ~univs:uctx c in (red_constant_entry (Context.Rel.length ctx) ce evd red_option, evd, decl, imps) let check_definition (ce, evd, _, imps) = -- cgit v1.2.3