package p4spectec

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

Source file ctx.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
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
open Domain.Lib
open Lang
open Il
open Al
module Typdef = Runtime.Type.Typdef
open Runtime.Dynamic_Al
open Envs
open Error
open Backtrack
open Util.Source

(* Error *)

let error_undef (at : region) (kind : string) (id : string) =
  error at (Format.asprintf "%s `%s` is undefined" kind id)

let error_dup (at : region) (kind : string) (id : string) =
  error at (Format.asprintf "%s `%s` was already defined" kind id)

module Make () = struct
  (* Cursor *)

  type cursor = Global | Local

  (* Mode *)

  let is_det : bool ref = ref false

  (* Context *)

  (* Global layer *)

  type global = {
    (* Map from syntax ids to type definitions *)
    tdtbl : TDTbl.t;
    (* Map from relation ids to relations *)
    rtbl : RTbl.t;
    (* Map from function ids to functions *)
    ftbl : FTbl.t;
  }

  (* Local layer *)

  type local = {
    (* Map from syntax ids to type definitions *)
    tdenv : TDEnv.t;
    (* Map from function ids to functions *)
    fenv : FEnv.t;
    (* Map from variables to values *)
    venv : VEnv.t;
  }

  type t = {
    (* Global layer *)
    global : global;
    (* Local layer *) local : local;
  }

  (* Global constructor *)

  let global : global =
    let tdtbl = TDTbl.create ~size:500 in
    let rtbl = RTbl.create ~size:500 in
    let ftbl = FTbl.create ~size:500 in
    { tdtbl; rtbl; ftbl }

  (* Adders for globals *)

  let add_typdef_global (tid : TId.t) (td : Typdef.t) : unit =
    if TDTbl.find_opt tid global.tdtbl |> Option.is_some then
      error_dup tid.at "type" tid.it;
    TDTbl.add tid td global.tdtbl

  let add_rel_global (rid : RId.t) (rel : Rel.t) : unit =
    if RTbl.find_opt rid global.rtbl |> Option.is_some then
      error_dup rid.at "relation" rid.it;
    RTbl.add rid rel global.rtbl

  let add_func_global (fid : FId.t) (func : Func.t) : unit =
    if FTbl.find_opt fid global.ftbl |> Option.is_some then
      error_dup fid.at "function" fid.it;
    FTbl.add fid func global.ftbl

  (* Global initializer *)

  let load_def (def : def) : unit =
    match def.it with
    | ExternTypD (id, _) ->
        let td = Typdef.Extern in
        add_typdef_global id td
    | TypD (id, tparams, deftyp, _) ->
        let td = Typdef.Defined (tparams, deftyp) in
        add_typdef_global id td
    | VarD _ -> ()
    | ExternRelD (id, nottyp, inputs, _) ->
        let rel = Rel.Extern (nottyp, inputs) in
        add_rel_global id rel
    | RelD (id, nottyp, input, rulegroups, elsegroup_opt, _) ->
        let rel = Rel.Defined (nottyp, input, rulegroups, elsegroup_opt) in
        add_rel_global id rel
    | ExternDecD (id, tparams, params, typ, _) ->
        let func = Func.Extern (tparams, params, typ) in
        add_func_global id func
    | BuiltinDecD (id, tparams, params, typ, _) ->
        let func = Func.Builtin (tparams, params, typ) in
        add_func_global id func
    | TableDecD (id, params, typ, tablerows, _) ->
        let func = Func.Table (params, typ, tablerows) in
        add_func_global id func
    | FuncDecD (id, tparams, params, typ, clauses, elseclause_opt, _) ->
        let func =
          Func.Defined (tparams, params, typ, clauses, elseclause_opt)
        in
        add_func_global id func

  let init ~(det : bool) (spec : spec) : unit =
    is_det := det;
    List.iter load_def spec

  (* Constructor *)

  let empty_local () : local =
    { tdenv = TDEnv.empty; fenv = FEnv.empty; venv = VEnv.empty }

  let empty : t = { global; local = empty_local () }

  (* Finders *)

  (* Finders for values *)

  let find_value_opt (ctx : t) (var : Var.t) : Value.t option =
    VEnv.find_opt var ctx.local.venv

  let find_value (ctx : t) (var : Var.t) : Value.t =
    match find_value_opt ctx var with
    | Some value -> value
    | None ->
        let id, _ = var in
        error_undef id.at "value" (Var.to_string var)

  let bound_value (ctx : t) (var : Var.t) : bool =
    find_value_opt ctx var |> Option.is_some

  (* Finders for type definitions *)

  let find_typdef_opt (ctx : t) (tid : TId.t) : Typdef.t option =
    match TDEnv.find_opt tid ctx.local.tdenv with
    | Some td -> Some td
    | None -> TDTbl.find_opt tid ctx.global.tdtbl

  let find_typdef (ctx : t) (tid : TId.t) : Typdef.t =
    match find_typdef_opt ctx tid with
    | Some td -> td
    | None -> error_undef tid.at "type" tid.it

  let find_defined_typdef (ctx : t) (tid : TId.t) : tparam list * deftyp =
    match find_typdef ctx tid with
    | Param | Extern | Defining _ -> error_undef tid.at "defined type" tid.it
    | Defined (tparams, deftyp) -> (tparams, deftyp)

  let bound_typdef (ctx : t) (tid : TId.t) : bool =
    find_typdef_opt ctx tid |> Option.is_some

  (* Finders for rules *)

  let find_rel_opt (ctx : t) (rid : RId.t) : Rel.t option =
    RTbl.find_opt rid ctx.global.rtbl

  let find_rel (ctx : t) (rid : RId.t) : Rel.t =
    match find_rel_opt ctx rid with
    | Some rel -> rel
    | None -> error_undef rid.at "relation" rid.it

  let find_rel_signature_opt (ctx : t) (rid : RId.t) :
      (nottyp * Hints.Input.t) option =
    find_rel_opt ctx rid |> Option.map Rel.get_signature

  let find_rel_signature (ctx : t) (rid : RId.t) : nottyp * Hints.Input.t =
    match find_rel_signature_opt ctx rid with
    | Some (nottyp, inputs) -> (nottyp, inputs)
    | None -> error_undef rid.at "relation" rid.it

  let bound_rel (ctx : t) (rid : RId.t) : bool =
    find_rel_opt ctx rid |> Option.is_some

  (* Finders for definitions *)

  let find_func_opt (ctx : t) (fid : FId.t) : (cursor * Func.t) option =
    match FEnv.find_opt fid ctx.local.fenv with
    | Some func -> Some (Local, func)
    | None ->
        FTbl.find_opt fid ctx.global.ftbl
        |> Option.map (fun func -> (Global, func))

  let find_func (ctx : t) (fid : FId.t) : cursor * Func.t =
    match find_func_opt ctx fid with
    | Some (cursor, func) -> (cursor, func)
    | None -> error_undef fid.at "function" fid.it

  let find_func_signature_opt (ctx : t) (fid : FId.t) :
      (tparam list * typ list * typ) option =
    find_func_opt ctx fid
    |> Option.map (fun (_, func) -> Func.get_signature func)

  let find_func_signature (ctx : t) (fid : FId.t) : tparam list * typ list * typ
      =
    match find_func_signature_opt ctx fid with
    | Some (tparams, typs, typ) -> (tparams, typs, typ)
    | None -> error_undef fid.at "function" fid.it

  let bound_func (ctx : t) (fid : FId.t) : bool =
    find_func_opt ctx fid |> Option.is_some

  (* Adders *)

  (* Adders for values *)

  let add_value (ctx : t) (var : Var.t) (value : Value.t) : t =
    let venv = VEnv.add var value ctx.local.venv in
    { ctx with local = { ctx.local with venv } }

  (* Adders for type definitions *)

  let add_typdef (ctx : t) (tid : TId.t) (td : Typdef.t) : t =
    if bound_typdef ctx tid then error_dup tid.at "type" tid.it;
    let tdenv = TDEnv.add tid td ctx.local.tdenv in
    { ctx with local = { ctx.local with tdenv } }

  (* Adders for functions *)

  let add_func (ctx : t) (fid : FId.t) (func : Func.t) : t =
    if bound_func ctx fid then error_dup fid.at "function" fid.it;
    let fenv = FEnv.add fid func ctx.local.fenv in
    { ctx with local = { ctx.local with fenv } }

  (* Constructors *)

  (* Constructing a local context *)

  let localize (ctx : t) : t =
    let local = empty_local () in
    { ctx with local }

  (* Constructing sub-contexts *)

  (* Transpose a matrix of values, as a list of value batches
     that are to be each fed into an iterated expression *)

  let transpose (value_matrix : value list list) : value list list backtrack =
    match value_matrix with
    | [] -> Ok []
    | row_h :: _ -> (
        let width = List.length row_h in
        let cols = Array.make width [] in
        try
          List.iter
            (fun row ->
              if List.length row <> width then
                raise
                  (Invalid_argument "cannot transpose a matrix of value batches");
              List.iteri (fun j v -> cols.(j) <- v :: cols.(j)) row)
            (List.rev value_matrix);
          Ok (Array.to_list cols)
        with Invalid_argument msg -> back_err no_region msg)

  let sub_opt (ctx : t) (vars : var list) : t option backtrack =
    (* First collect the values that are to be iterated over *)
    let values =
      List.map
        (fun (id, _typ, iters) ->
          find_value ctx (id, iters @ [ Opt ]) |> Value.Get.opt)
        vars
    in
    (* Iteration is valid when all variables agree on their optionality *)
    if List.for_all Option.is_some values then
      let values = List.map Option.get values in
      let ctx_sub =
        List.fold_left2
          (fun ctx_sub (id, _typ, iters) value ->
            add_value ctx_sub (id, iters) value)
          ctx vars values
      in
      Ok (Some ctx_sub)
    else if List.for_all Option.is_none values then Ok None
    else back_err no_region "mismatch in optionality of iterated variables"

  let sub_list (ctx : t) (vars : var list) : t list backtrack =
    (* First break the values that are to be iterated over,
       into a batch of values *)
    let* values_batch =
      List.map
        (fun (id, _typ, iters) ->
          find_value ctx (id, iters @ [ List ]) |> Value.Get.list)
        vars
      |> transpose
    in
    (* For each batch of values, create a sub-context *)
    let ctxs_sub =
      List.fold_left
        (fun ctxs_sub value_batch ->
          let ctx_sub =
            List.fold_left2
              (fun ctx_sub (id, _typ, iters) value ->
                add_value ctx_sub (id, iters) value)
              ctx vars value_batch
          in
          ctxs_sub @ [ ctx_sub ])
        [] values_batch
    in
    Ok ctxs_sub
end