From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 1 Nov 2016 20:53:32 +0100 Subject: Reductionops API using EConstr. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index 948d624a27..88ae4695b8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -615,7 +615,7 @@ let find_scope_class_opt = function (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_classes t = - match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with + match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t)) with | Prod (_,t,u) -> let cl = try Some (compute_scope_class t) with Not_found -> None in cl :: compute_arguments_classes u -- cgit v1.2.3 From ce2b509734f3b70494a0a35b0b4eda593c1c8eb6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 7 Nov 2016 19:07:16 +0100 Subject: Classops API using EConstr. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index 88ae4695b8..d264a19047 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -585,7 +585,7 @@ let scope_class_compare : scope_class -> scope_class -> int = cl_typ_ord let compute_scope_class t = - let (cl,_,_) = find_class_type Evd.empty t in + let (cl,_,_) = find_class_type Evd.empty (EConstr.of_constr t) in cl module ScopeClassOrd = -- cgit v1.2.3 From 85ab3e298aa1d7333787c1fa44d25df189ac255c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 19:02:40 +0100 Subject: Pretyping API using EConstr. --- interp/constrintern.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 235e6e24f6..8d4d87f2a2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1937,7 +1937,7 @@ let extract_ids env = let scope_of_type_kind = function | IsType -> Notation.current_type_scope_name () - | OfType typ -> compute_type_scope typ + | OfType typ -> compute_type_scope (EConstr.Unsafe.to_constr typ) | WithoutTypeConstraint -> None let empty_ltac_sign = { @@ -1982,7 +1982,7 @@ let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = - interp_gen (OfType typ) env sigma ~impls c + interp_gen (OfType (EConstr.of_constr typ)) env sigma ~impls c (* Not all evars expected to be resolved *) @@ -2001,7 +2001,7 @@ let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c + interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls IsType c @@ -2016,7 +2016,7 @@ let interp_constr_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref WithoutTypeConstraint ~impls c let interp_casted_constr_evars env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen env evdref ~impls (OfType typ) c + interp_constr_evars_gen env evdref ~impls (OfType (EConstr.of_constr typ)) c let interp_type_evars env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen env evdref IsType ~impls c @@ -2102,7 +2102,7 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) -- cgit v1.2.3 From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- interp/stdarg.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/stdarg.mli b/interp/stdarg.mli index af3a734627..3047d2bce6 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -57,12 +57,12 @@ val wit_open_constr : val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type + EConstr.constr with_bindings delayed_open) genarg_type val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type + EConstr.constr bindings delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, -- cgit v1.2.3 From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index d264a19047..29e5a3bfd8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -615,7 +615,7 @@ let find_scope_class_opt = function (* Special scopes associated to arguments of a global reference *) let rec compute_arguments_classes t = - match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t)) with + match kind_of_term (EConstr.Unsafe.to_constr (Reductionops.whd_betaiotazeta Evd.empty (EConstr.of_constr t))) with | Prod (_,t,u) -> let cl = try Some (compute_scope_class t) with Not_found -> None in cl :: compute_arguments_classes u -- cgit v1.2.3 From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- interp/stdarg.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 3047d2bce6..113fe40ba7 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -11,6 +11,7 @@ open Loc open Names open Term +open EConstr open Libnames open Globnames open Genredexpr @@ -57,12 +58,12 @@ val wit_open_constr : val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, - EConstr.constr with_bindings delayed_open) genarg_type + constr with_bindings delayed_open) genarg_type val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, - EConstr.constr bindings delayed_open) genarg_type + constr bindings delayed_open) genarg_type val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- interp/constrintern.ml | 9 ++++++--- interp/constrintern.mli | 20 ++++++++++---------- 2 files changed, 16 insertions(+), 13 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d4d87f2a2..e5dd6a6ec3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1982,7 +1982,7 @@ let interp_type env sigma ?(impls=empty_internalization_env) c = interp_gen IsType env sigma ~impls c let interp_casted_constr env sigma ?(impls=empty_internalization_env) c typ = - interp_gen (OfType (EConstr.of_constr typ)) env sigma ~impls c + interp_gen (OfType typ) env sigma ~impls c (* Not all evars expected to be resolved *) @@ -2001,7 +2001,7 @@ let interp_constr_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls WithoutTypeConstraint c let interp_casted_constr_evars_impls env evdref ?(impls=empty_internalization_env) c typ = - interp_constr_evars_gen_impls env evdref ~impls (OfType (EConstr.of_constr typ)) c + interp_constr_evars_gen_impls env evdref ~impls (OfType typ) c let interp_type_evars_impls env evdref ?(impls=empty_internalization_env) c = interp_constr_evars_gen_impls env evdref ~impls IsType c @@ -2093,6 +2093,7 @@ let interp_rawcontext_evars env evdref k bl = let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> + let t = EConstr.Unsafe.to_constr t in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2102,7 +2103,9 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_tcc_evars env evdref ~expected_type:(OfType (EConstr.of_constr t)) b in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let t = EConstr.Unsafe.to_constr t in + let c = EConstr.Unsafe.to_constr c in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 61e7c6f5cb..2f6795ed48 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -101,7 +101,7 @@ val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> - constr_expr -> types -> constr Evd.in_evar_universe_context + constr_expr -> EConstr.types -> constr Evd.in_evar_universe_context val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context @@ -109,32 +109,32 @@ val interp_type : env -> evar_map -> ?impls:internalization_env -> (** Main interpretation function expecting all postponed problems to be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * EConstr.constr (** Accepting unresolved evars *) val interp_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> constr + ?impls:internalization_env -> constr_expr -> EConstr.constr val interp_casted_constr_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> constr + ?impls:internalization_env -> constr_expr -> types -> EConstr.constr val interp_type_evars : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types + ?impls:internalization_env -> constr_expr -> EConstr.types (** Accepting unresolved evars and giving back the manual implicit arguments *) val interp_constr_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - constr * Impargs.manual_implicits + EConstr.constr * Impargs.manual_implicits val interp_casted_constr_evars_impls : env -> evar_map ref -> - ?impls:internalization_env -> constr_expr -> types -> - constr * Impargs.manual_implicits + ?impls:internalization_env -> constr_expr -> EConstr.types -> + EConstr.constr * Impargs.manual_implicits val interp_type_evars_impls : env -> evar_map ref -> ?impls:internalization_env -> constr_expr -> - types * Impargs.manual_implicits + EConstr.types * Impargs.manual_implicits (** Interprets constr patterns *) @@ -153,7 +153,7 @@ val interp_reference : ltac_sign -> reference -> glob_constr val interp_binder : env -> evar_map -> Name.t -> constr_expr -> types Evd.in_evar_universe_context -val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types +val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConstr.types (** Interpret contexts: returns extended env and context *) -- cgit v1.2.3 From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 16:18:47 +0100 Subject: Definining EConstr-based contexts. This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. --- interp/constrintern.ml | 4 +--- interp/constrintern.mli | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e5dd6a6ec3..41e2e4e6ff 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2083,6 +2083,7 @@ let intern_context global_level env impl_env binders = user_err ~loc ~hdr:"internalize" (explain_internalization_error e) let interp_rawcontext_evars env evdref k bl = + let open EConstr in let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> @@ -2093,7 +2094,6 @@ let interp_rawcontext_evars env evdref k bl = let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t = EConstr.Unsafe.to_constr t in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2104,8 +2104,6 @@ let interp_rawcontext_evars env evdref k bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in - let t = EConstr.Unsafe.to_constr t in - let c = EConstr.Unsafe.to_constr c in let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 2f6795ed48..ae7f511f43 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -160,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> EConst val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map ref -> local_binder list -> - internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) + internalization_env * ((env * EConstr.rel_context) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) @@ -177,7 +177,7 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : Context.Named.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr val global_reference : Id.t -> constr val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr -- cgit v1.2.3 From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: Namegen primitives now apply on evar constrs. Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. --- interp/constrextern.ml | 8 ++++++-- interp/constrintern.ml | 2 +- interp/notation_ops.ml | 1 + interp/reserve.ml | 2 ++ 4 files changed, 10 insertions(+), 3 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3077231be0..8debc06bba 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -953,6 +953,7 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t = (* Not "goal_concl_style" means do alpha-conversion avoiding only *) (* those goal/section/rel variables that occurs in the subterm under *) (* consideration; see namegen.ml for further details *) + let t = EConstr.of_constr t in let avoid = if goal_concl_style then ids_of_context env else [] in let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in let vars = vars_of_env env in @@ -965,6 +966,7 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t = extern_constr_gen lax goal_concl_style None env sigma t let extern_type goal_concl_style env sigma t = + let t = EConstr.of_constr t in let avoid = if goal_concl_style then ids_of_context env else [] in let r = Detyping.detype goal_concl_style avoid env sigma t in extern_glob_type (vars_of_env env) r @@ -1042,14 +1044,16 @@ let rec glob_of_pat env sigma = function | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") in GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) - | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *) - | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c) + | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *) + | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)) | PSort s -> GSort (loc,s) let extern_constr_pattern env sigma pat = extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat) let extern_rel_context where env sigma sign = + let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in + let where = Option.map EConstr.of_constr where in let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 41e2e4e6ff..bac97aa3f6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1843,7 +1843,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (add_name match_acc (loc,x)) ((loc,x)::var_acc) | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in + Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (fresh::forbidden_names) ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc) | _ -> assert false in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7dbd94aa74..549e8e7879 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -441,6 +441,7 @@ let notation_constr_of_glob_constr nenv a = (* Substitution of kernel names, avoiding a list of bound identifiers *) let notation_constr_of_constr avoiding t = + let t = EConstr.of_constr t in let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in let nenv = { ninterp_var_type = Id.Map.empty; diff --git a/interp/reserve.ml b/interp/reserve.ml index a4d4f40277..1565ba4a92 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -107,7 +107,9 @@ let constr_key c = let revert_reserved_type t = try + let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in + let t = EConstr.of_constr t in let t = Detyping.detype false [] (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) -- cgit v1.2.3