package p4spectec

You can search for identifiers within the package.

in-package search v0.2.0

p4spectec
- README
- Library builtin
  - Builtin
    
    Call
    
    Fresh_
    
    Typ
    
    Value
    
    Run
    
    EXT
    
    No_ext
    
    Make
    
    Funcs
    
    Error
    
    Extract
    
    Fresh
    
    Value
    
    Ints
    
    Value
    
    Lists
    
    Typ
    
    Value
    
    Maps
    
    Mixfix
    
    Typ
    
    Value
    
    Nats
    
    Value
    
    Numerics
    
    Typ
    
    Value
    
    Sets
    
    Mixfix
    
    Typ
    
    Value
    
    VSet
    
    Texts
    
    Typ
    
    Value
- Library dangling
  - Dangling
    
    Multi
    
    Branch
    
    Cover
    
    Single
    
    Branch
    
    Cover
- Library dynamic
  - Dynamic
    
    Caches
    
    ValueEntry
    
    ValueCache
    
    Table
    
    CallEntry
    
    CallCache
    
    Table
    
    Envs
    
    VarMap
    
    MakeVarEnv
    
    VEnv
    
    TDEnv
    
    TDTbl
    
    T
    
    Var
- Library dynamic_al
  - Dynamic_al
    
    Envs_Al
    
    Caches
    
    Var
    
    Rel
    
    Func
    
    Envs
    
    VEnv
    
    TDEnv
    
    TDTbl
    
    REnv
    
    RTbl
    
    T
    
    FEnv
    
    FTbl
    
    T
- Library dynamic_pl
  - Dynamic_pl
    
    Envs_Pl
    
    Caches
    
    Var
    
    Rel
    
    Func
    
    Envs
    
    VEnv
    
    TDEnv
    
    TDTbl
    
    REnv
    
    RTbl
    
    T
    
    FEnv
    
    FTbl
    
    T
- Library dynamic_runner
  - Dynamic_runner
    
    Caches
    
    Envs
    
    Var
    
    Signature
    
    Typ
    
    CACHE
    
    INTERFACE
    
    EXTERN
    
    Cache
    
    INTERP
    
    Cache
    
    INTERP_AL
    
    Cache
    
    INTERP_SL
    
    Cache
    
    INTERP_PL
    
    Cache
    
    RUNNER
    
    Cache
    
    Interface
    
    Interp
    
    Cache
- Library dynamic_sl
  - Dynamic_sl
    
    Envs_Sl
    
    Caches
    
    Var
    
    Rel
    
    Func
    
    Envs
    
    VEnv
    
    TDEnv
    
    TDTbl
    
    REnv
    
    RTbl
    
    T
    
    FEnv
    
    FTbl
    
    T
- Library error_runtime
  - Error
- Library inst
  - Inst
    
    Coverage_dangling
    
    DCov
    
    Value
    
    Coverage_instr
    
    ICov
    
    Value
    
    Handler
    
    Value
    
    Dep
    
    Run
    
    ICov
    
    HANDLER
    
    Default
    
    Hook
    
    Value
    
    Dep
    
    Profile
    
    Value
    
    Stat
    
    Trace
    
    Value
    
    Value_dependency
    
    Value
    
    Dep
- Library instr
  - Instr
    
    Log
    
    Multi
    
    Node
    
    Cover
    
    Single
    
    Node
    
    Cover
- Library interp_al
  - Interp_al
    
    Backtrack
    
    Ctx
    
    Typdef
    
    Make
    
    Error
    
    Interp
    
    Mixfix
    
    Type
    
    Typ
    
    CCache
    
    Run
    
    Dep
    
    Hook
    
    F
    
    Make
    
    Cache
    
    Nondet
- Library interp_common
  - Interp_common
    
    Backtrace
    
    Error
    
    Flow
    
    Nondet
- Library interp_pl
  - Interp_pl
    
    Ctx
    
    Typdef
    
    Make
    
    Interp
    
    Mixfix
    
    Type
    
    Typ
    
    CCache
    
    Run
    
    Dep
    
    Hook
    
    Flow
    
    F
    
    Make
    
    Cache
- Library interp_sl
  - Interp_sl
    
    Ctx
    
    Typdef
    
    Make
    
    Interp
    
    Mixfix
    
    Type
    
    Typ
    
    CCache
    
    Run
    
    Dep
    
    Hook
    
    Flow
    
    F
    
    Make
    
    Cache
- Library p4
  - P4
    
    Context
    
    SMap
    
    Extract
    
    Value
    
    F
    
    Lexer
    
    Value
    
    F
    
    Parse
    
    Value
    
    Parser
    
    MenhirInterpreter
    
    Incremental
    
    Tables
    
    Preprocessor
    
    Unparse
    
    Atom
    
    Mixfix
    
    Mixop
    
    Value
    
    F
    
    HEnv
- Library p4spectec.backend_boot
  - Backend_boot
    
    Build
    
    Run
    
    Config
    
    Run
    
    Error
    
    P4
    
    Make
    
    Cache
    
    Interface
    
    Interp
    
    Cache
    
    Patch
    
    Value
    
    Run
    
    Spectec
    
    Typ
    
    Value
    
    CCache
    
    Run
    
    INTERFACE_SPECTEC
    
    Make_null
    
    Cache
    
    Make_parametric
    
    Cache
- Library p4spectec.backend_sim
  - Backend_sim
    
    Build
    
    Sim
    
    Core
    
    Func
    
    Typ
    
    Value
    
    Make
    
    Object
    
    Mixfix
    
    Typ
    
    Value
    
    PacketIn
    
    PacketOut
    
    Make
    
    PacketIn
    
    PacketOut
    
    Packet
    
    Ebpf
    
    Object
    
    Typ
    
    Value
    
    Make
    
    CounterArray
    
    Pipe
    
    Typ
    
    Value
    
    IO
    
    Sim
    
    Make
    
    Error
    
    Extern
    
    Value
    
    Typ
    
    Run
    
    IMPL
    
    Make
    
    Cache
    
    Hash
    
    Make
    
    Typ
    
    Value
    
    Make
    
    Cache
    
    Interface
    
    Interp
    
    Cache
    
    Placeholder
    
    Typ
    
    Value
    
    IO
    
    Sim
    
    Make
    
    Psa
    
    Arch
    
    Typ
    
    Value
    
    Mirror
    
    Json
    
    Table
    
    M
    
    Multicast
    
    Json
    
    GroupMap
    
    M
    
    NodeMap
    
    M
    
    State
    
    Object
    
    Typ
    
    Value
    
    Make
    
    Counter
    
    Meter
    
    Register
    
    HashExtern
    
    InternetChecksum
    
    Packet
    
    Value
    
    Pipe
    
    Typ
    
    Value
    
    IO
    
    Sim
    
    Make
    
    Scheduler
    
    Spec
    
    Func
    
    Rel
    
    Pgm
    
    Pack
    
    Unpack
    
    S
    
    Func
    
    Rel
    
    Pgm
    
    Make
    
    Func
    
    Rel
    
    Pgm
    
    Spec_impl
    
    Func
    
    Typ
    
    Value
    
    IO
    
    Make
    
    S
    
    Pack
    
    Value
    
    Pgm
    
    Value
    
    IO
    
    Make
    
    S
    
    Rel
    
    Value
    
    IO
    
    Make
    
    S
    
    Unpack
    
    Num
    
    Value
    
    State
    
    Value
    
    IO
    
    Table
    
    Typ
    
    Value
    
    Make
    
    Spec
    
    Func
    
    V1model
    
    Arch
    
    Typ
    
    Value
    
    Exception
    
    Value
    
    Func
    
    Typ
    
    Value
    
    Make
    
    Core
    
    Object
    
    PacketIn
    
    PacketOut
    
    Packet
    
    Mirror
    
    Table
    
    M
    
    Multicast
    
    Json
    
    GroupMap
    
    M
    
    NodeMap
    
    M
    
    State
    
    Object
    
    Typ
    
    Value
    
    Make
    
    Core
    
    Object
    
    PacketIn
    
    PacketOut
    
    Packet
    
    Counter
    
    Register
    
    DirectCounter
    
    DirectMeter
    
    Packet
    
    Value
    
    CloneInfo
    
    ResubmitInfo
    
    RecirculateInfo
    
    Pipe
    
    Typ
    
    Value
    
    IO
    
    Sim
    
    Make
    
    Scheduler
- Library p4spectec.backend_splice
  - Backend_splice
    
    Driver
    
    Error
    
    Parser
    
    Source
    
    Splicer
    
    KEY
    
    VALUE
    
    INIT
    
    STORE
    
    Make_store
    
    ANCHOR
    
    SPLICER
    
    Make
    
    Splicers
    
    Func
    
    Key
    
    Source
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Prose
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Func_title
    
    Key
    
    Source
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Prose
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Rel_title
    
    Key
    
    Source
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Prose
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Rulegroup
    
    Key
    
    Source
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Prose
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Rulegroup_dispatch
    
    Key
    
    Prose
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Syntax
    
    Key
    
    Source
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Table
    
    Key
    
    Source
    
    Value
    
    Init
    
    Anchor
    
    Splicer
    
    Prose
    
    Value
    
    Init
    
    Anchor
    
    Splicer
- Library p4spectec.backend_testgen_neg
  - Backend_testgen_neg
    
    Boot
    
    DCov_multi
    
    Sim
    
    Config
    
    DCov_single
    
    DCov_multi
    
    Type
    
    Sim
    
    Derive
    
    DCov_single
    
    Sim
    
    Dep
    
    F
    
    Gen
    
    DCov_single
    
    DCov_multi
    
    Dep
    
    Sim
    
    F
    
    Logger
    
    Modes
    
    Mutate
    
    Type
    
    Value
    
    Mixfix
    
    Mixop
    
    Query
    
    Rand
    
    Runner
    
    DCov_single
    
    DCov_multi
    
    Dep
    
    Sim
    
    Target
- Library p4spectec.cache
  - Cache
    
    Entry
    
    ENTRY
    
    Make
    
    Make
    
    Table
- Library p4spectec.coverage
  - Coverage
    
    Instr
    
    Dangling
- Library p4spectec.domain
  - Domain
    
    Atom
    
    Caches
    
    MixopEntry
    
    MixopCache
    
    Table
    
    Lib
    
    HashTable
    
    T
    
    VId
    
    VIdSet
    
    VIdMap
    
    VIdTbl
    
    T
    
    IId
    
    IIdSet
    
    IIdMap
    
    IIdTbl
    
    Id
    
    IdSet
    
    IdMap
    
    IdTbl
    
    T
    
    TId
    
    TIdSet
    
    TIdMap
    
    TIdTbl
    
    RId
    
    RIdSet
    
    RIdMap
    
    RIdTbl
    
    FId
    
    FIdSet
    
    FIdMap
    
    FIdTbl
    
    HId
    
    HIdSet
    
    HIdMap
    
    MixId
    
    MixIdSet
    
    MixIdMap
    
    MixIdTbl
    
    T
    
    CaseId
    
    CaseIdSet
    
    CaseIdMap
    
    CaseIdTbl
    
    T
    
    MakeVIdEnv
    
    MakeVIdTbl
    
    T
    
    MakeIIdEnv
    
    MakeIIdTbl
    
    MakeIdEnv
    
    MakeIdTbl
    
    T
    
    MakeTIdEnv
    
    MakeTIdTbl
    
    MakeRIdEnv
    
    MakeRIdTbl
    
    MakeFIdEnv
    
    MakeFIdTbl
    
    MakeHIdEnv
    
    MakeHIdTbl
    
    MakeMixIdEnv
    
    MakeMixIdTbl
    
    T
    
    MakeCaseIdEnv
    
    MakeCaseIdTbl
    
    T
    
    Mixfix
    
    Mixop
- Library p4spectec.frontend
  - Frontend
    
    Error
    
    Lexer
    
    Source
    
    Parse
    
    Source
    
    Parser
- Library p4spectec.interface
  - Interface
    
    Typ
    
    Value
    
    Run
    
    P4
    
    Builtin_P4_Ext
    
    Builtin_P4
    
    Funcs
    
    Cache
    
    SpecTec_AL
    
    Mixop
    
    Atom
    
    Mixfix
    
    Typ
    
    Value
    
    Il
    
    VCache
    
    MCache
    
    Builtin_SpecTec
    
    Funcs
    
    SpecTec_SL
    
    Mixop
    
    Atom
    
    Mixfix
    
    Typ
    
    Value
    
    Il
    
    VCache
    
    MCache
    
    Builtin_SpecTec
    
    Funcs
- Library p4spectec.interp
  - Interp
    
    Inst
    
    Interp_Al
    
    Interp_Sl
- Library p4spectec.lang
  - Lang
    
    Al
    
    Eq
    
    Free
    
    Mixfix
    
    Fresh
    
    Var
    
    Print
    
    Mixfix
    
    Walk
    
    Collect
    
    Mixfix
    
    El
    
    Free
    
    Print
    
    Render
    
    Hints
    
    Alter
    
    Fields
    
    Flag
    
    Hint
    
    Input
    
    Il
    
    Eq
    
    Free
    
    Mixfix
    
    Fresh
    
    Var
    
    Print
    
    Mixfix
    
    Pl
    
    Annot
    
    Print
    
    Group
    
    Annot
    
    Partial
    
    Mixfix
    
    Render
    
    F
    
    Block
    
    F
    
    Fallthrough
    
    F
    
    Sl
    
    Eq
    
    Mixfix
    
    Free
    
    Mixfix
    
    Print
    
    Xl
    
    Bool
    
    Num
    
    Utf8
    
    String
    
    Var
- Library p4spectec.pass
  - Pass
    
    Elaborate
    
    Attempt
    
    Ctx
    
    Dimension
    
    Mixfix
    
    Dimctx
    
    Elab
    
    Mixfix
    
    F
    
    Error
    
    Algo
    
    Structure
    
    Antiunify
    
    Mixfix
    
    UEnv
    
    Ctx
    
    Dangle
    
    Error
    
    Merge
    
    Ol
    
    Ast
    
    Eq
    
    Free
    
    Print
    
    Eq
    
    Mixfix
    
    Free
    
    Mixfix
    
    Print
    
    Opt
    
    Loop
    
    Casify
    
    Typ
    
    Merge_binding
    
    Typ
    
    Bind
    
    Merge_hold
    
    Mixfix
    
    Typ
    
    Merge_if
    
    Typ
    
    Overlap
    
    Typ
    
    Post
    
    Remove_let_dead
    
    Mixfix
    
    Defined
    
    Used
    
    Remove_match_singleton
    
    Typ
    
    Pre
    
    Matchify_if_eq_terminal
    
    Mixfix
    
    Remove_group
    
    Remove_let_alias
    
    Optimize
    
    Prettify
    
    Pretty
    
    Rename_tick
    
    Mixfix
    
    Revive_underscore
    
    Mixfix
    
    Underscore
    
    Re
    
    Renamer
    
    Mixfix
    
    Rename
    
    Replacer
    
    Mixfix
    
    Exp
    
    Replace
    
    Struct
    
    Mixfix
    
    Typ
    
    Typdef
    
    Totalize
    
    Mixop
    
    Typ
    
    Annotate
    
    Mixfix
    
    Annot
- Library p4spectec.runner
  - Runner
    
    Make
    
    Value
    
    Make_rec
    
    Cache
    
    Interface
    
    Interp
    
    Cache
    
    Make_nonrec
    
    Cache
    
    Interface
    
    Interp
    
    Cache
- Library p4spectec.runtime
  - Runtime
    
    Type
    
    Value
    
    Static
    
    Dynamic
    
    Dynamic_Al
    
    Dynamic_Sl
    
    Dynamic_Pl
    
    Dynamic_Runner
    
    Testgen_neg
    
    Sim
    
    Prose
- Library p4spectec.stf
  - Stf
    
    Ast
    
    Compare
    
    Lexer
    
    Parse
    
    Parser
    
    Print
    
    F
    
    Transform
    
    Name
    
    Match
    
    Action
- Library p4spectec.util
  - Util
    
    Attempt
    
    Checks
    
    Deque
    
    Error
    
    Filesys
    
    Json
    
    Map
    
    Make
    
    M
    
    Print
    
    Source
    
    Strings
    
    Test
    
    Time
- Library prose
  - Prose
    
    Kinds
    
    Kind
    
    TypHints
    
    RelHints
    
    FuncHints
    
    Envs
    
    TDEnv
    
    MEnv
    
    IHEnv
    
    HEnv
- Library sim
  - Sim
    
    Caches
    
    Envs
    
    Var
    
    Io
    
    Signature
    
    IO
    
    Typ
    
    CACHE
    
    INTERFACE
    
    EXTERN
    
    INTERP
    
    INTERP_AL
    
    INTERP_SL
    
    INTERP_PL
    
    RUNNER
    
    ARCH
    
    SIM
    
    Cache
    
    Interface
    
    Interp
    
    Cache
- Library spectec
  - Spectec
    
    Ali
    
    Boot
    
    Mixops
    
    Value
    
    Typs
    
    Typ
    
    Unboot
    
    Caches
    
    Il
    
    VCache
    
    MCache
    
    Common
    
    Boot
    
    Atom
    
    Mixop
    
    Mixfix
    
    Il
    
    Value
    
    VCache
    
    MCache
    
    Mixops
    
    Value
    
    Stub
    
    Mixfix
    
    Value
    
    Typs
    
    Typ
    
    Unboot
    
    Atom
    
    Mixfix
    
    Il
    
    Typ
    
    Value
    
    VCache
    
    Parse
    
    Value
    
    Run
    
    Sli
    
    Boot
    
    Mixops
    
    Value
    
    Stub
    
    Typs
    
    Typ
    
    Unboot
- Library static
  - Static
    
    Envs
    
    VEnv
    
    MEnv
    
    TDEnv
    
    REnv
    
    IHEnv
    
    FEnv
    
    Func
    
    Rel
    
    Typdim
- Library testgen_neg
  - Testgen_neg
    
    Envs_Testgen_neg
    
    Caches
    
    Var
    
    Mixops
    
    Family
    
    Envs
    
    TDEnv
    
    MixopEnv
    
    Dep
    
    Edges
    
    E
    
    Graph
    
    Mixfix
    
    G
    
    Node
- Library type
  - Type
    
    Envs
    
    TDEnv
    
    TDTbl
    
    T
    
    Equiv
    
    Fresh_
    
    Expand
    
    Fresh
    
    Sub
    
    Subst
    
    Fresh_
    
    Mixfix
    
    Typ
    
    Make
    
    Typdef
- Library value
  - Value
    
    Fresh_
    
    Match
    
    Mixfix
    
    Mixfix
    
    Typ
    
    Mixops
    
    Make
    
    Get
    
    MixopHashed
    
    MtchTbl
- Sources
  - builtin
    
    builtin.ml
    
    call.ml
    
    error.ml
    
    extract.ml
    
    fresh.ml
    
    ints.ml
    
    lists.ml
    
    maps.ml
    
    nats.ml
    
    numerics.ml
    
    sets.ml
    
    texts.ml
  - dangling
    
    dangling.ml
    
    multi.ml
    
    single.ml
  - dynamic
    
    caches.ml
    
    dynamic.ml
    
    envs.ml
    
    var.ml
  - dynamic_al
    
    dynamic_al.ml
    
    dynamic_al__.ml
    
    envs.ml
    
    func.ml
    
    rel.ml
  - dynamic_pl
    
    dynamic_pl.ml
    
    dynamic_pl__.ml
    
    envs.ml
    
    func.ml
    
    rel.ml
  - dynamic_runner
    
    dynamic_runner.ml
    
    dynamic_runner__.ml
    
    signature.ml
  - dynamic_sl
    
    dynamic_sl.ml
    
    dynamic_sl__.ml
    
    envs.ml
    
    func.ml
    
    rel.ml
  - error_runtime
    
    error.ml
  - inst
    
    coverage_dangling.ml
    
    coverage_instr.ml
    
    handler.ml
    
    hook.ml
    
    inst.ml
    
    profile.ml
    
    trace.ml
    
    value_dependency.ml
  - instr
    
    instr.ml
    
    log.ml
    
    multi.ml
    
    single.ml
  - interp_al
    
    backtrack.ml
    
    ctx.ml
    
    error.ml
    
    interp.ml
    
    interp_al.ml
    
    nondet.ml
  - interp_common
    
    backtrace.ml
    
    error.ml
    
    flow.ml
    
    interp_common.ml
    
    nondet.ml
  - interp_pl
    
    ctx.ml
    
    interp.ml
    
    interp_pl.ml
  - interp_sl
    
    ctx.ml
    
    interp.ml
    
    interp_sl.ml
  - p4
    
    context.ml
    
    extract.ml
    
    lexer.ml
    
    p4.ml
    
    parse.ml
    
    parser.ml
    
    preprocessor.ml
    
    unparse.ml
  - p4spectec.backend_boot
    
    backend_boot.ml
    
    build.ml
    
    config.ml
    
    error.ml
    
    p4.ml
    
    patch.ml
    
    spectec.ml
  - p4spectec.backend_sim
    
    backend_sim.ml
    
    build.ml
    
    error.ml
    
    extern.ml
    
    hash.ml
    
    make.ml
    
    placeholder.ml
    
    spec.ml
    
    state.ml
    
    table.ml
  - p4spectec.backend_splice
    
    backend_splice.ml
    
    driver.ml
    
    error.ml
    
    parser.ml
    
    source.ml
    
    splicer.ml
  - p4spectec.backend_testgen_neg
    
    backend_testgen_neg.ml
    
    boot.ml
    
    config.ml
    
    derive.ml
    
    gen.ml
    
    logger.ml
    
    modes.ml
    
    mutate.ml
    
    query.ml
    
    rand.ml
    
    runner.ml
    
    target.ml
  - p4spectec.cache
    
    cache.ml
    
    entry.ml
    
    make.ml
  - p4spectec.coverage
    
    coverage.ml
  - p4spectec.domain
    
    atom.ml
    
    caches.ml
    
    domain.ml
    
    lib.ml
    
    mixfix.ml
    
    mixop.ml
  - p4spectec.frontend
    
    error.ml
    
    frontend.ml
    
    lexer.ml
    
    parse.ml
    
    parser.ml
  - p4spectec.interface
    
    interface.ml
  - p4spectec.interp
    
    interp.ml
  - p4spectec.lang
    
    lang.ml
    
    lang__Al__.ml
    
    lang__El__.ml
    
    lang__El__Render__.ml
    
    lang__Il__.ml
    
    lang__Pl__.ml
    
    lang__Pl__Render__.ml
    
    lang__Sl__.ml
  - p4spectec.pass
    
    pass.ml
    
    pass__.ml
    
    pass__Algo__.ml
    
    pass__Annotate__.ml
    
    pass__Annotate__Expand__.ml
  - p4spectec.runner
    
    make.ml
    
    runner.ml
  - p4spectec.runtime
    
    runtime.ml
  - p4spectec.stf
    
    ast.ml
    
    compare.ml
    
    lexer.ml
    
    parse.ml
    
    parser.ml
    
    print.ml
    
    stf.ml
    
    transform.ml
  - p4spectec.util
    
    attempt.ml
    
    checks.ml
    
    deque.ml
    
    error.ml
    
    filesys.ml
    
    json.ml
    
    print.ml
    
    source.ml
    
    strings.ml
    
    test.ml
    
    time.ml
    
    util.ml
  - prose
    
    envs.ml
    
    hintkinds.ml
    
    kinds.ml
    
    prose.ml
    
    prose__.ml
  - sim
    
    io.ml
    
    signature.ml
    
    sim.ml
    
    sim__.ml
  - spectec
    
    caches.ml
    
    parse.ml
    
    spectec.ml
  - static
    
    envs.ml
    
    func.ml
    
    rel.ml
    
    static.ml
    
    typdim.ml
  - testgen_neg
    
    envs.ml
    
    mixops.ml
    
    testgen_neg.ml
    
    testgen_neg__.ml
  - type
    
    envs.ml
    
    equiv.ml
    
    expand.ml
    
    fresh.ml
    
    sub.ml
    
    subst.ml
    
    typ.ml
    
    typdef.ml
    
    type.ml
  - value
    
    fresh.ml
    
    match.ml
    
    value.ml
    
    value__.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Spec.Rel`

type call_rel =
  string ->
  Backend_sim.Spec_impl.Rel.Value.t list ->
  Backend_sim.Spec_impl.Rel.Value.t list

val call : call_rel ref

val register : call_rel -> unit

val lvalue_read_var : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_read_var_global : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_read_dot : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_read_dot_global : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_write_var : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_write_dot : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_write_var_local : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_write_dot_global : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val lvalue_write_dot_local : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  string ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val v1model_init_packet_in : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val v1model_init_packet_out : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val v1model_init_globals : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.IO.port ->
  Backend_sim.Spec_impl.Rel.Value.t

val v1model_parser : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val v1model_verify : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val v1model_ingress : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val v1model_egress : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val v1model_check : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val v1model_deparse : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val v1model_setup_preserved_meta_fields : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val ebpf_init_packet_in : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val ebpf_init_globals : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t

val ebpf_parse : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val ebpf_filter : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress_init_packet_in : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress_init_packet_out : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress_init_metadata : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.IO.port ->
  string ->
  Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress_init_globals : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.IO.port ->
  Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress_parser : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val psa_ingress_deparser : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val psa_egress_init_packet_in : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val psa_egress_init_packet_out : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t * Backend_sim.Spec_impl.Rel.Value.t

val psa_egress_init_metadata : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.IO.port ->
  string ->
  int ->
  int ->
  Backend_sim.Spec_impl.Rel.Value.t

val psa_egress_init_globals : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.IO.port ->
  Backend_sim.Spec_impl.Rel.Value.t

val psa_egress_parser : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val psa_egress : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

val psa_egress_deparser : 
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t ->
  Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t
  * Backend_sim.Spec_impl.Rel.Value.t

package p4spectec

Module Spec.Rel

Module `Spec.Rel`