Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Utilopen Names
type reds = {flags : int; ts : TransparentState.t}
type red_kind = | FLAG of int | CONST of Constant.t | PROJ of Projection.Repr.t | VAR of Id.t
let fBETA = FLAG 0b000001let fDELTA = FLAG 0b000010let fMATCH = FLAG 0b000100let fFIX = FLAG 0b001000let fCOFIX = FLAG 0b010000let fZETA = FLAG 0b100000let fCONST kn = CONST knlet fPROJ p = PROJ plet fVAR id = VAR id
let no_red = {flags = 0; ts = TransparentState.empty}
let red_add ({flags; ts} as red) = function | FLAG f -> {red with flags = flags lor f} | CONST kn -> {red with ts = {ts with tr_cst = Cpred.add kn ts.tr_cst}} | PROJ p -> {red with ts = {ts with tr_prj = PRpred.add p ts.tr_prj}} | VAR id -> {red with ts = {ts with tr_var = Id.Pred.add id ts.tr_var}}
let red_sub ({flags; ts} as red) = function | FLAG f -> {red with flags = flags land (0b111111 lxor f)} | CONST kn -> {red with ts = {ts with tr_cst = Cpred.remove kn ts.tr_cst}} | PROJ p -> {red with ts = {ts with tr_prj = PRpred.remove p ts.tr_prj}} | VAR id -> { red with ts = {ts with tr_var = Id.Pred.remove id ts.tr_var}}
let red_sub_list = List.fold_left red_sublet red_add_list = List.fold_left red_add
let red_transparent red = red.tslet red_add_transparent red ts = {red with ts}
let mkflags = List.fold_left red_add no_red
let mkfullflags = List.fold_left red_add { no_red with ts = TransparentState.full }
let red_set red = function | FLAG f -> red.flags land f != 0 | CONST kn -> TransparentState.is_transparent_constant red.ts kn | PROJ p -> TransparentState.is_transparent_projection red.ts p | VAR id -> TransparentState.is_transparent_variable red.ts id
let red_projection red p = Projection.unfolded p || red_set red (fPROJ (Projection.repr p))
let all = mkfullflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX]let allnolet = mkfullflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX]let beta = mkflags [fBETA]let betadeltazeta = mkfullflags [fBETA;fDELTA;fZETA]let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX]let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA]let betazeta = mkflags [fBETA;fZETA]let delta = mkfullflags [fDELTA]let zeta = mkflags [fZETA]let nored = no_red