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. --- pretyping/inductiveops.mli | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7bd616591f..1cfdef6e58 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -130,7 +130,7 @@ val has_dependent_elim : mutual_inductive_body -> bool val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + EConstr.t -> EConstr.types -> types (** Extract information from an inductive family *) @@ -161,12 +161,12 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : constr -> pinductive * constr list -val find_mrectype : env -> evar_map -> types -> pinductive * constr list -val find_mrectype_vect : env -> evar_map -> types -> pinductive * constr array -val find_rectype : env -> evar_map -> types -> inductive_type -val find_inductive : env -> evar_map -> types -> pinductive * constr list -val find_coinductive : env -> evar_map -> types -> pinductive * constr list +val extract_mrectype : evar_map -> EConstr.t -> pinductive * constr list +val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array +val find_rectype : env -> evar_map -> EConstr.types -> inductive_type +val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list +val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list (********************) @@ -175,7 +175,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - env -> pinductive * constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info @@ -195,7 +195,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> evar_map -> Inductive.mind_specif puniverses -> types -> evar_map * types + env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * types (********************) val control_only_guard : env -> types -> unit -- cgit v1.2.3 From d528fdaf12b74419c47698cca7c6f1ec762245a3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Nov 2016 14:48:36 +0100 Subject: Retyping API using EConstr. --- pretyping/inductiveops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1cfdef6e58..e375a2c6be 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -195,7 +195,7 @@ i*) (********************) val type_of_inductive_knowing_conclusion : - env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * types + env -> evar_map -> Inductive.mind_specif puniverses -> EConstr.types -> evar_map * EConstr.types (********************) val control_only_guard : env -> types -> unit -- cgit v1.2.3 From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 10:57:05 +0100 Subject: Cases API using EConstr. --- pretyping/inductiveops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index e375a2c6be..cf5523a50d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -185,8 +185,8 @@ val make_case_info : env -> inductive -> case_style -> case_info Fail with an error if the elimination is dependent while the inductive type does not allow dependent elimination. *) val make_case_or_project : - env -> inductive_family -> case_info -> - (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + env -> evar_map -> inductive_family -> case_info -> + (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info -- 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. --- pretyping/inductiveops.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cf5523a50d..7af9731f9a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -175,7 +175,7 @@ val arity_of_case_predicate : env -> inductive_family -> bool -> sorts -> types val type_case_branches_with_names : - env -> evar_map -> pinductive * constr list -> constr -> constr -> types array * types + env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info -- cgit v1.2.3 From 7b43de20a4acd7c9da290f038d9a16fe67eccd59 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Nov 2016 01:59:07 +0100 Subject: Leminv API using EConstr. --- pretyping/inductiveops.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7af9731f9a..1614e1817e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -37,15 +37,15 @@ val substnl_ind_family : constr list -> int -> inductive_family -> inductive_family (** An inductive type with its parameters and real arguments *) -type inductive_type = IndType of inductive_family * constr list -val make_ind_type : inductive_family * constr list -> inductive_type -val dest_ind_type : inductive_type -> inductive_family * constr list -val map_inductive_type : (constr -> constr) -> inductive_type -> inductive_type +type inductive_type = IndType of inductive_family * EConstr.constr list +val make_ind_type : inductive_family * EConstr.constr list -> inductive_type +val dest_ind_type : inductive_type -> inductive_family * EConstr.constr list +val map_inductive_type : (EConstr.constr -> EConstr.constr) -> inductive_type -> inductive_type val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type +val substnl_ind_type : EConstr.constr list -> int -> inductive_type -> inductive_type -val mkAppliedInd : inductive_type -> constr +val mkAppliedInd : inductive_type -> EConstr.constr val mis_is_recursive_subset : int list -> wf_paths -> bool val mis_is_recursive : inductive * mutual_inductive_body * one_inductive_body -> bool -- cgit v1.2.3 From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Nov 2016 20:09:26 +0100 Subject: Eliminating parts of the right-hand side compatibility layer --- pretyping/inductiveops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1614e1817e..4bb4847591 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -161,9 +161,9 @@ val make_arity : env -> bool -> inductive_family -> sorts -> types val build_branch_type : env -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : evar_map -> EConstr.t -> pinductive * constr list -val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * constr list -val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * constr array +val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list +val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array val find_rectype : env -> evar_map -> EConstr.types -> inductive_type val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list -- 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. --- pretyping/inductiveops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 4bb4847591..ab470a540e 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -156,9 +156,9 @@ val get_arity : env -> inductive_family -> Context.Rel.t * sorts_family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr -val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t -val make_arity : env -> bool -> inductive_family -> sorts -> types -val build_branch_type : env -> bool -> constr -> constructor_summary -> types +val make_arity_signature : env -> evar_map -> bool -> inductive_family -> EConstr.rel_context +val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr.types +val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list -- cgit v1.2.3 From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- pretyping/inductiveops.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index ab470a540e..bdb6f996b9 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -161,12 +161,12 @@ val make_arity : env -> evar_map -> bool -> inductive_family -> sorts -> EConstr val build_branch_type : env -> evar_map -> bool -> constr -> constructor_summary -> types (** Raise [Not_found] if not given a valid inductive type *) -val extract_mrectype : evar_map -> EConstr.t -> pinductive * EConstr.constr list -val find_mrectype : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list -val find_mrectype_vect : env -> evar_map -> EConstr.types -> pinductive * EConstr.constr array +val extract_mrectype : evar_map -> EConstr.t -> (inductive * EConstr.EInstance.t) * EConstr.constr list +val find_mrectype : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr list +val find_mrectype_vect : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * EConstr.constr array val find_rectype : env -> evar_map -> EConstr.types -> inductive_type -val find_inductive : env -> evar_map -> EConstr.types -> pinductive * constr list -val find_coinductive : env -> evar_map -> EConstr.types -> pinductive * constr list +val find_inductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list +val find_coinductive : env -> evar_map -> EConstr.types -> (inductive * EConstr.EInstance.t) * constr list (********************) -- cgit v1.2.3