diff options
| author | Matthieu Sozeau | 2014-05-08 13:43:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-08 19:23:51 +0200 |
| commit | f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 (patch) | |
| tree | eadad13bfd7e178d782bb46a9bd3e0daff84264b /checker/closure.mli | |
| parent | 0db1d850b940a5f2351c1ec6e26d1f8087064d40 (diff) | |
Adapt the checker to polymorphic universes and projections (untested).
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index 13bc0c07e0..9b152eb6a1 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -66,11 +66,13 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type table_key = - | ConstKey of constant +type 'a tableKey = + | ConstKey of 'a | VarKey of Id.t | RelKey of int +type table_key = constant puniverses tableKey + type 'a infos val ref_value_cache: 'a infos -> table_key -> 'a option val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos @@ -90,9 +92,10 @@ type fterm = | FAtom of constr (* Metas and Sorts *) | FCast of fconstr * cast_kind * fconstr | FFlex of table_key - | FInd of inductive - | FConstruct of constructor + | FInd of pinductive + | FConstruct of pconstructor | FApp of fconstr * fconstr array + | FProj of constant * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCases of case_info * fconstr * fconstr * fconstr array @@ -112,6 +115,7 @@ type fterm = type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array + | Zproj of int * int * constant | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -121,6 +125,12 @@ and stack = stack_member list val append_stack : fconstr array -> stack -> stack val eta_expand_stack : stack -> stack +val eta_expand_ind_stack : env -> lift -> pinductive -> fconstr -> stack -> + (lift * (fconstr * stack)) -> lift * (fconstr * stack) + +val eta_expand_ind_stacks : env -> inductive -> fconstr -> stack -> + (fconstr * stack) -> stack * stack + (* To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use a reduction function *) @@ -135,6 +145,8 @@ val destFLambda : (* Global and local constant cache *) type clos_infos val create_clos_infos : reds -> env -> clos_infos +val infos_env : clos_infos -> env +val infos_flags : clos_infos -> reds (* Reduction function *) |