package p4spectec

  1. Overview
  2. Docs
P4-SpecTec: A mechanization toolchain for the P4 Programming Language

Install

dune-project
 Dependency

Authors

Maintainers

Sources

v0.1.2.tar.gz
md5=1a3bc0a385fe1ecf403c019f49aa6de6
sha512=5d20b5821f33e2a3a5419b208606f27c01511994c2b3b1e1cdf4c077056dfd0aa81682af0720e1060ee2bfb0341918fcc4c53159820205a2bc32b725e5c1a714

doc/src/p4spectec.stf/print.ml.html

Source file print.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
(* Copyright 2018-present Cornell University
 *
 * Licensed under the Apache License, Version 2.0 (the "License"); you may not
 * use this file except in compliance with the License. You may obtain a copy
 * of the License at
 *
 *   http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
 * WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
 * License for the specific language governing permissions and limitations
 * under the License.
 *)

open Ast
module F = Format

let convert_dollar_to_brackets (s : string) : string =
  Str.global_replace (Str.regexp "\\$\\([0-9]+\\)") "[\\1]" s

let pp_print_option pp fmt = function
  | None -> ()
  | Some x -> F.fprintf fmt " %a" pp x

let print_int fmt i = F.fprintf fmt "%d" i
let print_string fmt s = F.fprintf fmt "%s" s
let print_quoted_string fmt s = F.fprintf fmt "\"%s\"" s
let print_name fmt name = print_quoted_string fmt name
let print_id fmt id = print_quoted_string fmt id
let print_number fmt number = print_string fmt number
let print_session fmt session = print_string fmt session
let print_port fmt port = print_string fmt port
let print_exact fmt exact = if exact then F.fprintf fmt "$" else ()
let print_packet fmt packet = print_string fmt packet
let print_expect fmt expect = print_string fmt expect

let print_arg fmt arg =
  let id, number = arg in
  F.fprintf fmt "%a:%a" print_id id print_number number

let print_action fmt action =
  let name, args = action in
  F.fprintf fmt "%a(%a)" print_name name
    (F.pp_print_list ~pp_sep:(fun fmt () -> F.fprintf fmt ",") print_arg)
    args

let print_mtchkind fmt = function
  | Num number -> print_number fmt number
  | Slash (number_l, number_r) ->
      F.fprintf fmt "%a/%a" print_number number_l print_number number_r

let print_mtch fmt mtch =
  let name, mtchkind = mtch in
  F.fprintf fmt "%a:%a" print_name name print_mtchkind mtchkind

let print_id_or_index fmt = function
  | Id id -> print_string fmt id
  | Index number -> print_number fmt number

let print_cond fmt = function
  | Eq -> print_string fmt "=="
  | Ne -> print_string fmt "!="
  | Le -> print_string fmt "<="
  | Lt -> print_string fmt "<"
  | Ge -> print_string fmt ">="
  | Gt -> print_string fmt ">"

let print_ctr fmt = function
  | Bytes -> print_string fmt "bytes"
  | Packets -> print_string fmt "packets"

let print_stmt fmt = function
  | Wait -> print_string fmt "wait"
  | RemoveAll -> print_string fmt "remove_all"
  | Expect (port, Some expect, exact) ->
      F.fprintf fmt "expect %a %a%a" print_port port print_expect expect
        print_exact exact
  | Expect (port, None, exact) ->
      F.fprintf fmt "expect %a %a" print_port port print_exact exact
  | Packet (port, packet) ->
      F.fprintf fmt "packet %a %a" print_port port print_packet packet
  | NoPacket -> print_string fmt "no_packet"
  | Add (name, int_opt, mtchs, action, id_opt) ->
      F.fprintf fmt "add %a%a %a %a%a" print_name name
        (pp_print_option print_int)
        int_opt
        (F.pp_print_list ~pp_sep:(fun fmt () -> F.fprintf fmt " ") print_mtch)
        mtchs print_action action (pp_print_option print_id) id_opt
  | SetDefault (name, action) ->
      F.fprintf fmt "setdefault %a %a" print_name name print_action action
  | CheckCounter (id, id_or_index, (ctr, cond, number)) ->
      F.fprintf fmt "check_counter %a(%a)%a %a %a" print_id id print_id_or_index
        id_or_index
        (pp_print_option print_ctr)
        ctr print_cond cond print_number number
  | MirroringAdd (session, port) ->
      F.fprintf fmt "mirroring_add %a %a" print_session session print_port port
  | MirroringAddMc (session, id) ->
      F.fprintf fmt "mirroring_add_mc %a %a" print_session session print_id id
  | MirroringGet session ->
      F.fprintf fmt "mirroring_get %a" print_session session
  | McGroupCreate id -> F.fprintf fmt "mc_mgrp_create %a" print_number id
  | McNodeCreate (id, port) ->
      F.fprintf fmt "mc_node_create %a %a" print_number id
        (F.pp_print_list ~pp_sep:(fun fmt () -> F.fprintf fmt " ") print_number)
        port
  | McNodeAssociate (id, handle) ->
      F.fprintf fmt "mc_mgrp_associate %a %a" print_number id print_number
        handle
  | RegisterRead (name, index) ->
      F.fprintf fmt "register_read %a %a" print_name name print_number index
  | RegisterWrite (name, index, number) ->
      F.fprintf fmt "register_write %a %a %a" print_name name print_number index
        print_number number
  | RegisterReset name -> F.fprintf fmt "register_reset %a" print_name name

let print_stmts fmt stmts =
  F.pp_print_list
    ~pp_sep:(fun fmt () -> F.fprintf fmt "@.")
    print_stmt fmt stmts