aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.ml131
-rw-r--r--kernel/reduction.ml53
-rw-r--r--kernel/reduction.mli7
3 files changed, 40 insertions, 151 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2ee2443ff..d29f8b08c 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -175,137 +175,6 @@ let unfold_red kn =
| EvalConstRef kn -> fCONST kn in
mkflags (flag::unfold_side_flags)
-(************************* Obsolète
-(* [r_const=(true,cl)] means all constants but those in [cl] *)
-(* [r_const=(false,cl)] means only those in [cl] *)
-type reds = {
- r_beta : bool;
- r_const : bool * constant_path list * identifier list;
- r_zeta : bool;
- r_evar : bool;
- r_iota : bool }
-
-let betadeltaiota_red = {
- r_beta = true;
- r_const = true,[],[];
- r_zeta = true;
- r_evar = true;
- r_iota = true }
-
-let betaiota_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = true }
-
-let beta_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = false }
-
-let no_red = {
- r_beta = false;
- r_const = false,[],[];
- r_zeta = false;
- r_evar = false;
- r_iota = false }
-
-let betaiotazeta_red = {
- r_beta = true;
- r_const = false,[],[];
- r_zeta = true;
- r_evar = false;
- r_iota = true }
-
-let unfold_red kn =
- let c = match kn with
- | EvalVarRef id -> false,[],[id]
- | EvalConstRef kn -> false,[kn],[]
- in {
- r_beta = true;
- r_const = c;
- r_zeta = true; (* false for finer behaviour ? *)
- r_evar = false;
- r_iota = true }
-
-(* Sets of reduction kinds.
- Main rule: delta implies all consts (both global (= by
- kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
- Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
- a LetIn expression is Letin reduction *)
-
-type red_kind =
- BETA | DELTA | ZETA | IOTA
- | CONST of constant_path list | CONSTBUT of constant_path list
- | VAR of identifier | VARBUT of identifier
-
-let rec red_add red = function
- | BETA -> { red with r_beta = true }
- | DELTA ->
- (match red.r_const with
- | _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
- | _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true })
- | CONST cl ->
- (match red.r_const with
- | true,_,_ -> error "Conflict in the reduction flags"
- | _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 })
- | CONSTBUT cl ->
- (match red.r_const with
- | false,_::_,_ | false,_,_::_ ->
- error "Conflict in the reduction flags"
- | _,l1,l2 ->
- { red with r_const = true, list_union cl l1, l2;
- r_zeta = true; r_evar = true })
- | IOTA -> { red with r_iota = true }
- | ZETA -> { red with r_zeta = true }
- | VAR id ->
- (match red.r_const with
- | true,_,_ -> error "Conflict in the reduction flags"
- | _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 })
- | VARBUT cl ->
- (match red.r_const with
- | false,_::_,_ | false,_,_::_ ->
- error "Conflict in the reduction flags"
- | _,l1,l2 ->
- { red with r_const = true, l1, list_union [cl] l2;
- r_zeta = true; r_evar = true })
-
-let red_delta_set red =
- let b,_,_ = red.r_const in b
-
-let red_local_const = red_delta_set
-
-(* to know if a redex is allowed, only a subset of red_kind is used ... *)
-let red_set red = function
- | BETA -> incr_cnt red.r_beta beta
- | CONST [kn] ->
- let (b,l,_) = red.r_const in
- let c = List.mem kn l in
- incr_cnt ((b & not c) or (c & not b)) delta
- | VAR id -> (* En attendant d'avoir des kn pour les Var *)
- let (b,_,l) = red.r_const in
- let c = List.mem id l in
- incr_cnt ((b & not c) or (c & not b)) delta
- | ZETA -> incr_cnt red.r_zeta zeta
- | EVAR -> incr_cnt red.r_zeta evar
- | IOTA -> incr_cnt red.r_iota iota
- | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*)
- (* Not for internal use *)
- | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented"
-
-(* Gives the constant list *)
-let red_get_const red =
- let b,l1,l2 = red.r_const in
- let l1' = List.map (fun x -> EvalConstRef x) l1 in
- let l2' = List.map (fun x -> EvalVarRef x) l2 in
- b, l1' @ l2'
-fin obsolète **************)
-(* specification of the reduction function *)
-
-
(* Flags of reduction and cache of constants: 'a is a type that may be
* mapped to constr. 'a infos implements a cache for constants and
* abstractions, storing a representation (of type 'a) of the body of
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 28176ecc5..7a6c560f8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -17,6 +17,12 @@ open Environ
open Closure
open Esubst
+let unfold_reference ((ids, csts), infos) k =
+ match k with
+ | VarKey id when not (Idpred.mem id ids) -> None
+ | ConstKey cst when not (Cpred.mem cst csts) -> None
+ | _ -> unfold_reference infos k
+
let rec is_empty_stack = function
[] -> true
| Zupdate _::s -> is_empty_stack s
@@ -117,6 +123,7 @@ let beta_appvect c v =
(* Conversion utility functions *)
type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
+type 'a trans_conversion_function = transparent_state -> env -> 'a -> 'a -> Univ.constraints
exception NotConvertible
exception NotConvertibleVect of int
@@ -171,8 +178,8 @@ let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty
let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
Util.check_for_interrupt ();
eqappr cv_pb infos
- (lft1, whd_stack infos term1 [])
- (lft2, whd_stack infos term2 [])
+ (lft1, whd_stack (snd infos) term1 [])
+ (lft2, whd_stack (snd infos) term2 [])
cuniv
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
@@ -216,17 +223,17 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
let (app1,app2) =
if Conv_oracle.oracle_order fl1 fl2 then
match unfold_reference infos fl1 with
- | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+ | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None ->
(match unfold_reference infos fl2 with
- | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+ | Some def2 -> (appr1, (lft2, whd_stack (snd infos) def2 v2))
| None -> raise NotConvertible)
else
match unfold_reference infos fl2 with
- | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+ | Some def2 -> (appr1, (lft2, whd_stack (snd infos) def2 v2))
| None ->
(match unfold_reference infos fl1 with
- | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+ | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
| None -> raise NotConvertible) in
eqappr cv_pb infos app1 app2 cuniv)
@@ -234,12 +241,12 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
| (FFlex fl1, _) ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr cv_pb infos (lft1, whd_stack infos def1 v1) appr2 cuniv
+ eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
| None -> raise NotConvertible)
| (_, FFlex fl2) ->
(match unfold_reference infos fl2 with
- | Some def2 ->
- eqappr cv_pb infos appr1 (lft2, whd_stack infos def2 v2) cuniv
+ | Some def2 ->
+ eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
| None -> raise NotConvertible)
(* other constructors *)
@@ -258,13 +265,13 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
(* Inductive types: MutInd MutConstruct Fix Cofix *)
| (FInd ind1, FInd ind2) ->
- if mind_equiv_infos infos ind1 ind2
+ if mind_equiv_infos (snd infos) ind1 ind2
then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
- if j1 = j2 && mind_equiv_infos infos ind1 ind2
+ if j1 = j2 && mind_equiv_infos (snd infos) ind1 ind2
then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
@@ -303,11 +310,11 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
on the other arg and coulb be no more in hnf... *)
| ( (FLetIn _, _) | (FCases _,_) | (FApp _,_)
| (FCLOS _, _) | (FLIFT _, _)) ->
- eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+ eqappr cv_pb infos (lft1, whd_stack (snd infos) hd1 v1) appr2 cuniv
| ( (_, FLetIn _) | (_,FCases _) | (_,FApp _)
| (_,FCLOS _) | (_,FLIFT _)) ->
- eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+ eqappr cv_pb infos (lft1, whd_stack (snd infos) hd1 v1) appr2 cuniv
(* Should not happen because whd_stack unlocks references *)
| ((FLOCKED,_) | (_,FLOCKED)) -> assert false
@@ -317,7 +324,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
(fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
- (mind_equiv_infos infos)
+ (mind_equiv_infos (snd infos))
lft1 stk1 lft2 stk2 cuniv
and convert_vect infos lft1 lft2 v1 v2 cuniv =
@@ -333,13 +340,19 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
fold 0 cuniv
else raise NotConvertible
-let clos_fconv cv_pb env t1 t2 =
- let infos = create_clos_infos betaiotazeta env in
+let clos_fconv trans cv_pb env t1 t2 =
+ let infos = trans, create_clos_infos betaiotazeta env in
ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
-let fconv cv_pb env t1 t2 =
+let trans_fconv reds cv_pb env t1 t2 =
if eq_constr t1 t2 then Constraint.empty
- else clos_fconv cv_pb env t1 t2
+ else clos_fconv reds cv_pb env t1 t2
+
+let trans_conv_cmp conv reds = trans_fconv reds conv
+let trans_conv reds = trans_fconv reds CONV
+let trans_conv_leq reds = trans_fconv reds CUMUL
+
+let fconv = trans_fconv (Idpred.full, Cpred.full)
let conv_cmp = fconv
let conv = fconv CONV
@@ -365,7 +378,7 @@ let vm_conv cv_pb env t1 t2 =
!vm_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- clos_fconv cv_pb env t1 t2
+ fconv cv_pb env t1 t2
let default_conv = ref fconv
@@ -377,7 +390,7 @@ let default_conv cv_pb env t1 t2 =
!default_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- clos_fconv cv_pb env t1 t2
+ fconv cv_pb env t1 t2
let default_conv_leq = default_conv CUMUL
(*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 60cd999d8..663c18e2c 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -11,6 +11,7 @@
(*i*)
open Term
open Environ
+open Closure
(*i*)
(************************************************************************)
@@ -28,6 +29,7 @@ val nf_betaiota : constr -> constr
exception NotConvertible
exception NotConvertibleVect of int
type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
+type 'a trans_conversion_function = Names.transparent_state -> env -> 'a -> 'a -> Univ.constraints
type conv_pb = CONV | CUMUL
@@ -37,6 +39,11 @@ val sort_cmp :
val conv_sort : sorts conversion_function
val conv_sort_leq : sorts conversion_function
+val trans_conv_cmp : conv_pb -> constr trans_conversion_function
+
+val trans_conv : constr trans_conversion_function
+val trans_conv_leq : types trans_conversion_function
+
val conv_cmp : conv_pb -> constr conversion_function
val conv : constr conversion_function
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 09:08:08 +0000