package p4spectec

  1. Overview
  2. Docs
package p4spectec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file interface.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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
open Lang
module Typ = Runtime.Type.Typ
module Value = Runtime.Value
module Run = Runtime.Dynamic_Runner.Signature
open Util.Error
open Util.Source

(* Interfaces *)

(* P4 *)

module P4 = struct
  (* Program unparser *)

  let unparser = ref (fun (_ : Value.t) -> "")

  (* Program parsing *)

  let parse_program (includes_p4 : string list) (paths_p4 : string list) :
      Run.parse_result =
    try
      match paths_p4 with
      | [ path_p4 ] ->
          let value_program = P4.Parse.parse_file includes_p4 path_p4 in
          Run.Pass value_program
      | _ ->
          Run.Fail (`Syntax (no_region, "exactly one P4 file must be provided"))
    with ParseError (at, msg) -> Run.Fail (`Syntax (at, msg))

  let parse_string (path_p4 : string) (str : string) : Run.parse_result =
    try
      let value_program = P4.Parse.parse_string path_p4 str in
      Run.Pass value_program
    with ParseError (at, msg) -> Run.Fail (`Syntax (at, msg))

  (* Program unparsing *)

  let unparse_program (value_program : Value.t) : string =
    !unparser value_program

  (* Builtins *)

  module Builtin_P4_Ext = struct
    (* dec $print_<X>(X) : text *)

    let print (add : Value.t -> unit) (at : region) (targs : Typ.t list)
        (values_input : Value.t list) : Value.t =
      let _typ = Builtin.Extract.one at targs in
      let value = Builtin.Extract.one at values_input in
      let text = !unparser value in
      let value = Value.Make.text text in
      add value;
      value

    (* Builtin extension entries *)

    let entries = [ ("print_", print) ]
  end

  module Builtin_P4 = Builtin.Call.Make (Builtin_P4_Ext) ()

  let call_builtin = Builtin_P4.invoke

  (* State management *)

  let checkpoint = Builtin_P4.checkpoint
  let seff = Builtin_P4.seff

  (* Cache management *)

  module Cache = struct
    let cache_on () = ()
    let cache_off () = ()
  end

  (* Initialization *)

  let init (spec : Run.spec) : unit =
    let printer (value : Value.t) =
      match spec with
      | AL spec_al ->
          let henv = P4.Unparse.hints_of_spec_al spec_al in
          Format.asprintf "%a" (P4.Unparse.pp_value henv) value
      | SL spec_sl ->
          let henv = P4.Unparse.hints_of_spec_sl spec_sl in
          Format.asprintf "%a" (P4.Unparse.pp_value henv) value
      | PL spec_pl ->
          let henv = P4.Unparse.hints_of_spec_pl spec_pl in
          Format.asprintf "%a" (P4.Unparse.pp_value henv) value
      | Empty -> assert false
    in
    unparser := printer
end

(* SpecTec IL *)

module SpecTec_AL = struct
  include Spectec.Common.Boot
  include Spectec.Common.Unboot
  include Spectec.Ali.Boot
  include Spectec.Ali.Unboot
  include Spectec.Caches

  (* Program parsing *)

  let parse_program (_includes : string list) (paths : string list) :
      Run.parse_result =
    try
      let value_spec = Spectec.Parse.parse_files Run.AL_mode paths in
      Run.Pass value_spec
    with
    | ParseError (at, msg) -> Run.Fail (`Syntax (at, msg))
    | ElabError (at, msg) -> Run.Fail (`Syntax (at, msg))

  let parse_string (path : string) (str : string) : Run.parse_result =
    try
      let value_spec = Spectec.Parse.parse_string Run.AL_mode path str in
      Run.Pass value_spec
    with
    | ParseError (at, msg) -> Run.Fail (`Syntax (at, msg))
    | ElabError (at, msg) -> Run.Fail (`Syntax (at, msg))

  (* Program unparsing *)

  let unparse_program (value_script : Value.t) : string =
    value_script |> unboot_script |> Al.Print.string_of_spec

  (* Builtins *)

  module Builtin_SpecTec = Builtin.Call.Make (Builtin.Call.No_ext) ()

  let call_builtin = Builtin_SpecTec.invoke

  (* State management *)

  let checkpoint = Builtin_SpecTec.checkpoint
  let seff = Builtin_SpecTec.seff

  (* Initialization *)

  let init (_spec : Run.spec) : unit = ()
end

(* SpecTec SL *)

module SpecTec_SL = struct
  include Spectec.Common.Boot
  include Spectec.Common.Unboot
  include Spectec.Sli.Boot
  include Spectec.Sli.Unboot
  include Spectec.Caches

  (* Program parsing *)

  let parse_program (_includes : string list) (paths : string list) :
      Run.parse_result =
    try
      let value_spec = Spectec.Parse.parse_files Run.SL_mode paths in
      Run.Pass value_spec
    with
    | ParseError (at, msg) -> Run.Fail (`Syntax (at, msg))
    | ElabError (at, msg) -> Run.Fail (`Syntax (at, msg))

  let parse_string (path : string) (str : string) : Run.parse_result =
    try
      let value_spec = Spectec.Parse.parse_string Run.SL_mode path str in
      Run.Pass value_spec
    with
    | ParseError (at, msg) -> Run.Fail (`Syntax (at, msg))
    | ElabError (at, msg) -> Run.Fail (`Syntax (at, msg))

  (* Program unparsing *)

  let unparse_program (value_script : Value.t) : string =
    value_script |> unboot_script |> Sl.Print.string_of_spec

  (* Builtins *)

  module Builtin_SpecTec = Builtin.Call.Make (Builtin.Call.No_ext) ()

  let call_builtin = Builtin_SpecTec.invoke

  (* State management *)

  let checkpoint = Builtin_SpecTec.checkpoint
  let seff = Builtin_SpecTec.seff

  (* Initialization *)

  let init (_spec : Run.spec) : unit = ()
end