From 886a9c2fb25e32bd87b3fce38023b3e701134d23 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 27 Dec 2017 20:22:23 +0100 Subject: [econstr] Continue consolidation of EConstr API under `interp`. This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag. --- plugins/funind/glob_term_to_relation.ml | 47 +++++++++++++++++---------------- plugins/funind/indfun.ml | 7 +++-- plugins/funind/recdef.ml | 9 ++++--- 3 files changed, 33 insertions(+), 30 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 22881c32c..7159614d9 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -352,9 +352,9 @@ let raw_push_named (na,raw_value,raw_typ) env = let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in (match raw_value with | None -> - Environ.push_named (NamedDecl.LocalAssum (id,typ)) env + EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env | Some value -> - Environ.push_named (NamedDecl.LocalDef (id, value, typ)) env) + EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env) let add_pat_variables pat typ env : Environ.env = @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = The "value" of this branch is then simply [res] *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in - let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in + let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -631,12 +631,11 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in - let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in - let v_type = EConstr.Unsafe.to_constr v_type in + let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in let new_env = match n with Anonymous -> env - | Name id -> Environ.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env + | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res @@ -648,7 +647,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> @@ -680,7 +679,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = nal in let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in - let b_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr b_as_constr) in + let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> @@ -726,7 +725,7 @@ and build_entry_lc_from_case env funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in - EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr case_arg_as_constr)) + EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr) ) el in (****** The next works only if the match is not dependent ****) @@ -948,7 +947,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -983,7 +982,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let subst_b = if is_in_b then b else replace_var_by_term id rt b in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -995,7 +994,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = with Continue -> let jmeq = Globnames.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in - let ind,args' = Inductive.find_inductive env ty' in + let ind,args' = Inductiveops.find_inductive env Evd.(from_env env) ty' in let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in let params,arg' = @@ -1017,14 +1016,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "computing new type for jmeq : " ++ pr_glob_constr_env env eq'); let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; + let sigma = Evd.(from_env env) in let new_args = - match Constr.kind eq'_as_constr with + match EConstr.kind sigma eq'_as_constr with | App(_,[|_;_;ty;_|]) -> - let ty = Array.to_list (snd (destApp ty)) in + let ty = Array.to_list (snd (EConstr.destApp sigma ty)) in let ty' = snd (Util.List.chop nparam ty) in List.fold_left2 (fun acc var_as_constr arg -> - let arg = EConstr.of_constr arg in if isRel var_as_constr then let na = RelDecl.get_name (Environ.lookup_rel (destRel var_as_constr) env) in @@ -1065,7 +1064,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in let new_env = let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in - Environ.push_rel (LocalAssum (n,t')) env + EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons @@ -1103,7 +1102,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1119,7 +1118,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1140,7 +1139,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> - let new_env = Environ.push_rel (LocalAssum (n,t')) env in + let new_env = EConstr.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1163,7 +1162,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in - let type_t' = Typing.unsafe_type_of env evd (EConstr.of_constr t') in + let type_t' = Typing.unsafe_type_of env evd t' in + let t' = EConstr.Unsafe.to_constr t' in let type_t' = EConstr.Unsafe.to_constr type_t' in let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = @@ -1189,7 +1189,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = depth t in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (LocalAssum (na,t')) env in + let new_env = EConstr.push_rel (LocalAssum (na,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1369,8 +1369,9 @@ let do_build_inductive *) let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (LocalAssum (rel_name, - fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities + let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in + let rex = EConstr.Unsafe.to_constr rex in + Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e19fc9b62..13eda3952 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -141,8 +141,7 @@ let rec abstract_glob_constr c = function | Constrexpr.CLocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = - Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls - c + Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls c (* Construct a fixpoint as a Glob_term @@ -160,9 +159,9 @@ let build_newrecursive let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in - let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in + let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) + (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 8fe05b497..e2d7de6d5 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -210,6 +210,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in + let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = @@ -1400,7 +1401,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (fun c -> Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [intros; - Simple.apply (EConstr.of_constr (fst (interp_constr (Global.env()) Evd.empty c))) (*FIXME*); + Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*); Tacticals.New.tclCOMPLETE Auto.default_auto ]) ) @@ -1599,7 +1600,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num + (EConstr.of_constr rec_arg_type) + (nb_prod evd (EConstr.of_constr res)) relation; Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1614,7 +1617,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num tcc_lemma_constr is_mes functional_ref (EConstr.of_constr rec_arg_type) - (EConstr.of_constr relation) rec_arg_num + relation rec_arg_num term_id using_lemmas (List.length res_vars) -- cgit v1.2.3