From 96e78e0d4ab9e2c2ccf1bb0565384e4e0d322904 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 00:43:01 +0200 Subject: Move transparent_state to its own module. --- kernel/cClosure.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95546a83e1..c8028f713a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -93,8 +93,8 @@ module type RedFlagsSig = sig val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> transparent_state -> reds - val red_transparent : reds -> transparent_state + val red_add_transparent : reds -> TranspState.t -> reds + val red_transparent : reds -> TranspState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool @@ -110,7 +110,7 @@ module RedFlags = (struct r_beta : bool; r_delta : bool; r_eta : bool; - r_const : transparent_state; + r_const : TranspState.t; r_zeta : bool; r_match : bool; r_fix : bool; -- cgit v1.2.3 From ad5aea737ecc639c31dda84322b3550a4d380b47 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 21:06:01 +0200 Subject: Proper record type and accessors for transparent states. This is documented in dev/doc/changes.md. --- kernel/cClosure.ml | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c8028f713a..625a9a7277 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -72,11 +72,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = (Id.Pred.empty, Cpred.empty) -let all_transparent = (Id.Pred.full, Cpred.full) - -let is_transparent_variable (ids, _) id = Id.Pred.mem id ids -let is_transparent_constant (_, csts) cst = Cpred.mem cst csts +let all_opaque = TranspState.empty +let all_transparent = TranspState.full module type RedFlagsSig = sig type reds @@ -106,6 +103,8 @@ module RedFlags = (struct (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) + open TranspState + type reds = { r_beta : bool; r_delta : bool; @@ -143,30 +142,30 @@ module RedFlags = (struct | ETA -> { red with r_eta = true } | DELTA -> { red with r_delta = true; r_const = all_transparent } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.add kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.add kn r.tr_cst } } | MATCH -> { red with r_match = true } | FIX -> { red with r_fix = true } | COFIX -> { red with r_cofix = true } | ZETA -> { red with r_zeta = true } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.add id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.add id r.tr_var } } let red_sub red = function | BETA -> { red with r_beta = false } | ETA -> { red with r_eta = false } | DELTA -> { red with r_delta = false } | CONST kn -> - let (l1,l2) = red.r_const in - { red with r_const = l1, Cpred.remove kn l2 } + let r = red.r_const in + { red with r_const = { r with tr_cst = Cpred.remove kn r.tr_cst } } | MATCH -> { red with r_match = false } | FIX -> { red with r_fix = false } | COFIX -> { red with r_cofix = false } | ZETA -> { red with r_zeta = false } | VAR id -> - let (l1,l2) = red.r_const in - { red with r_const = Id.Pred.remove id l1, l2 } + let r = red.r_const in + { red with r_const = { r with tr_var = Id.Pred.remove id r.tr_var } } let red_transparent red = red.r_const @@ -179,12 +178,10 @@ module RedFlags = (struct | BETA -> incr_cnt red.r_beta beta | ETA -> incr_cnt red.r_eta eta | CONST kn -> - let (_,l) = red.r_const in - let c = Cpred.mem kn l in + let c = is_transparent_constant red.r_const kn in incr_cnt c delta | VAR id -> (* En attendant d'avoir des kn pour les Var *) - let (l,_) = red.r_const in - let c = Id.Pred.mem id l in + let c = is_transparent_variable red.r_const id in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta | MATCH -> incr_cnt red.r_match nb_match -- cgit v1.2.3 From 733cb74a2038ff92156b7209713fc2ea741ccca6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Nov 2018 08:12:28 +0100 Subject: Rename TranspState into TransparentState. --- kernel/cClosure.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/cClosure.ml') diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 625a9a7277..7e73609996 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -72,8 +72,8 @@ let with_stats c = end else Lazy.force c -let all_opaque = TranspState.empty -let all_transparent = TranspState.full +let all_opaque = TransparentState.empty +let all_transparent = TransparentState.full module type RedFlagsSig = sig type reds @@ -90,8 +90,8 @@ module type RedFlagsSig = sig val no_red : reds val red_add : reds -> red_kind -> reds val red_sub : reds -> red_kind -> reds - val red_add_transparent : reds -> TranspState.t -> reds - val red_transparent : reds -> TranspState.t + val red_add_transparent : reds -> TransparentState.t -> reds + val red_transparent : reds -> TransparentState.t val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool val red_projection : reds -> Projection.t -> bool @@ -103,13 +103,13 @@ module RedFlags = (struct (* [r_const=(false,cl)] means only those in [cl] *) (* [r_delta=true] just mean [r_const=(true,[])] *) - open TranspState + open TransparentState type reds = { r_beta : bool; r_delta : bool; r_eta : bool; - r_const : TranspState.t; + r_const : TransparentState.t; r_zeta : bool; r_match : bool; r_fix : bool; -- cgit v1.2.3