diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /kernel/cClosure.mli | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'kernel/cClosure.mli')
| -rw-r--r-- | kernel/cClosure.mli | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 79092813bc..c1e5f12df7 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -95,10 +95,11 @@ module KeyTable : Hashtbl.S with type key = table_key (** [fconstr] is the type of frozen constr *) type fconstr - (** [fconstr] can be accessed by using the function [fterm_of] and by matching on type [fterm] *) +type finvert + type fterm = | FRel of int | FAtom of constr (** Metas and Sorts *) @@ -110,6 +111,7 @@ type fterm = | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) + | FCaseInvert of case_info * constr * finvert * fconstr * constr array * fconstr subs | FLambda of int * (Name.t Context.binder_annot * constr) list * constr * fconstr subs | FProd of Name.t Context.binder_annot * fconstr * constr * fconstr subs | FLetIn of Name.t Context.binder_annot * fconstr * fconstr * constr * fconstr subs @@ -173,15 +175,22 @@ val set_relevance : Sorts.relevance -> fconstr -> unit type clos_infos type clos_tab val create_clos_infos : - ?evars:(existential->constr option) -> reds -> env -> clos_infos + ?univs:UGraph.t -> ?evars:(existential->constr option) -> reds -> env -> clos_infos val oracle_of_infos : clos_infos -> Conv_oracle.oracle val create_tab : unit -> clos_tab val info_env : clos_infos -> env val info_flags: clos_infos -> reds +val info_univs : clos_infos -> UGraph.t val unfold_projection : clos_infos -> Projection.t -> stack_member option +val push_relevance : clos_infos -> 'b Context.binder_annot -> clos_infos +val push_relevances : clos_infos -> 'b Context.binder_annot array -> clos_infos +val set_info_relevances : clos_infos -> Sorts.relevance Range.t -> clos_infos + +val info_relevances : clos_infos -> Sorts.relevance Range.t + val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) @@ -214,6 +223,9 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** [unfold_reference] unfolds references in a [fconstr] *) val unfold_reference : clos_infos -> clos_tab -> table_key -> (fconstr, Util.Empty.t) constant_def +(** Hook for Reduction *) +val set_conv : (clos_infos -> clos_tab -> fconstr -> fconstr -> bool) -> unit + (*********************************************************************** i This is for lazy debug *) |