From 43c46c5398704e78c609f9ee3a51d515f2746f0e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 Dec 2017 22:33:53 +0100 Subject: [vernac] Cleanup of do_definition. We remove a few old-style normalization and try to use the newer APIs, however, it is hard to say whether the right magic is being used. --- vernac/comDefinition.ml | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) (limited to 'vernac/comDefinition.ml') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 883121479..af5f095fb 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -11,7 +11,6 @@ open Util open Constr open Environ open Entries -open Termops open Redexpr open Declare open Constrintern @@ -53,34 +52,32 @@ let interp_definition pl bl poly red_option c ctypopt = let env = Global.env() in let evd, decl = Univdecls.interp_univ_decl_opt env pl in let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in - let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in let nb_args = Context.Rel.nhyps ctx in let evd,imps,ce = match ctypopt with None -> - let evd, subst = Evd.nf_univ_variables evd in - let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in - let env_bl = push_rel_context ctx env in + (* 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 c = EConstr.Unsafe.to_constr c in - let evd,nf = Evarutil.nf_evars_and_universes evd in - let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = EConstr.universes_of_constr env evd (EConstr.of_constr body) 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 evd, subst = Evd.nf_univ_variables evd in - let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in - let env_bl = push_rel_context ctx env 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 c = EConstr.Unsafe.to_constr c in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let body = nf (it_mkLambda_or_LetIn c ctx) in - let ty = EConstr.Unsafe.to_constr ty in - let typ = nf (Term.it_mkProd_or_LetIn ty ctx) 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 @@ -90,11 +87,15 @@ let interp_definition pl bl poly red_option c ctypopt = in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); - let bodyvars = EConstr.universes_of_constr env evd (EConstr.of_constr body) in - let tyvars = EConstr.universes_of_constr env evd (EConstr.of_constr ty) in + (* 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 in -- cgit v1.2.3