package p4spectec

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

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (2)

Authors

  1. K
    KAIST PLRG

Maintainers

  1. 9
    99jaehyunlee@kaist.ac.kr

Sources

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

doc/src/builtin/maps.ml.html

Source file maps.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
module Mixfix = Domain.Mixfix
open Lang
open Il
module Typ = Runtime.Type.Typ
module Value = Runtime.Value
open Error
open Util.Source

(* Value map *)

type map = value list

let mixop_pair = Value.Mixops.of_string "k ':' v"
let mixop_map = Value.Mixops.of_string "`{ k `}"

let rec map_find_opt key = function
  | [] -> None
  | pair :: pairs -> (
      match pair.it with
      | CaseV valuecase when Mixfix.eq_mixop valuecase mixop_pair -> (
          match Mixfix.args valuecase with
          | [ value_key; value_value ] when Value.eq value_key key ->
              Some value_value
          | _ -> map_find_opt key pairs)
      | _ -> map_find_opt key pairs)

let make_pair (add : value -> unit) (typ_key : typ) (typ_value : typ)
    (value_key : value) (value_value : value) : value =
  let typ = Typ.Make.var ("pair" $ no_region) [ typ_key; typ_value ] in
  let valuecase = Mixfix.fill mixop_pair [ value_key; value_value ] in
  let value_pair = Value.Make.case typ valuecase in
  add value_pair;
  value_pair

let rec map_update make_pair key value = function
  | [] -> [ make_pair key value ]
  | pair :: pairs -> (
      match pair.it with
      | CaseV valuecase when Mixfix.eq_mixop valuecase mixop_pair -> (
          match Mixfix.args valuecase with
          | [ value_key; _ ] when Value.eq value_key key ->
              make_pair key value :: pairs
          | _ -> pair :: map_update make_pair key value pairs)
      | _ -> pair :: map_update make_pair key value pairs)

(* Conversion between meta-maps and OCaml lists *)

let map_of_value (value : value) : map =
  match value.it with
  | CaseV valuecase when Mixfix.eq_mixop valuecase mixop_map -> (
      match Mixfix.args valuecase with
      | [ value_pairs ] -> value_pairs |> Value.Get.list
      | _ ->
          error no_region
            (Format.asprintf "expected a map, but got %s"
               (Value.to_string value)))
  | _ ->
      error no_region
        (Format.asprintf "expected a map, but got %s" (Value.to_string value))

let value_of_map (add : value -> unit) (typ_key : typ) (typ_value : typ)
    (map : map) : value =
  let value_pairs =
    let typ =
      Typ.Make.var ("pair" $ no_region) [ typ_key; typ_value ] |> Typ.Make.list
    in
    Value.Make.list typ map
  in
  add value_pairs;
  let value =
    let typ = Typ.Make.var ("map" $ no_region) [ typ_key; typ_value ] in
    let valuecase = Mixfix.fill mixop_map [ value_pairs ] in
    Value.Make.case typ valuecase
  in
  add value;
  value

(* Built-in implementations *)

(* dec $find_map<K, V>(map<K, V>, K) : V? *)

let find_map (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let _typ_key, typ_value = Extract.two at targs in
  let value_map, value_key = Extract.two at values_input in
  let map = map_of_value value_map in
  let typ_opt = Typ.Make.opt typ_value in
  let value_opt = map_find_opt value_key map in
  let value = Value.Make.opt typ_opt value_opt in
  add value;
  value

(* dec $find_maps<K, V>(map<K, V>*, K) : V? *)

let find_maps (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let _typ_key, typ_value = Extract.two at targs in
  let value_maps, value_key = Extract.two at values_input in
  let maps = value_maps |> Value.Get.list |> List.map map_of_value in
  let typ_opt = Typ.Make.opt typ_value in
  let value_opt =
    List.fold_left
      (fun value_opt map ->
        match value_opt with
        | Some _ -> value_opt
        | None -> map_find_opt value_key map)
      None maps
  in
  let value = Value.Make.opt typ_opt value_opt in
  add value;
  value

(* dec $add_map<K, V>(map<K, V>, K, V) : map<K, V> *)

let add_map (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key, typ_value = Extract.two at targs in
  let value_map, value_key, value_value = Extract.three at values_input in
  let mk = make_pair add typ_key typ_value in
  map_of_value value_map
  |> map_update mk value_key value_value
  |> value_of_map add typ_key typ_value

(* dec $adds_map<K, V>(map<K, V>, K*, V* ) : map<K, V> *)

let adds_map (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key, typ_value = Extract.two at targs in
  let value_map, value_keys, value_values = Extract.three at values_input in
  let map = map_of_value value_map in
  let values_key = value_keys |> Value.Get.list in
  let values_value = value_values |> Value.Get.list in
  let mk = make_pair add typ_key typ_value in
  List.fold_left2
    (fun map value_key value_value -> map_update mk value_key value_value map)
    map values_key values_value
  |> value_of_map add typ_key typ_value

(* dec $update_map<K, V>(map<K, V>, K, V) : map<K, V> *)

let update_map (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key, typ_value = Extract.two at targs in
  let value_map, value_key, value_value = Extract.three at values_input in
  let mk = make_pair add typ_key typ_value in
  map_of_value value_map
  |> map_update mk value_key value_value
  |> value_of_map add typ_key typ_value