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/lists.ml.html

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

(* dec $rev_<X>(X* ) : X* *)

let rev_ (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ = Extract.one at targs in
  let typ_list = Typ.Make.list typ in
  let values = Extract.one at values_input |> Value.Get.list in
  let value = Value.Make.list typ_list (List.rev values) in
  add value;
  value

(* dec $concat_<X>((X* )* ) : X* *)

let concat_ (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ = Extract.one at targs in
  let typ_list = Typ.Make.list typ in
  let values =
    Extract.one at values_input
    |> Value.Get.list
    |> List.concat_map Value.Get.list
  in
  let value = Value.Make.list typ_list values in
  add value;
  value

(* dec $distinct_<K>(K* ) : bool *)

let distinct_ (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let _typ = Extract.one at targs in
  let values = Extract.one at values_input |> Value.Get.list in
  let set = Sets.VSet.of_list values in
  let value = Value.Make.bool (Sets.VSet.cardinal set = List.length values) in
  add value;
  value

(* dec $partition_<X>(X*, nat) : (X*, X* ) *)

let partition_ (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ = Extract.one at targs in
  let typ_list = Typ.Make.list typ in
  let value_list, value_len = Extract.two at values_input in
  let values = Value.Get.list value_list in
  let len = value_len |> Value.Get.num |> Num.to_int |> Bigint.to_int_exn in
  let values_left, values_right =
    values
    |> List.mapi (fun idx value -> (idx, value))
    |> List.partition (fun (idx, _) -> idx < len)
  in
  let value_left = Value.Make.list typ_list (List.map snd values_left) in
  add value_left;
  let value_right = Value.Make.list typ_list (List.map snd values_right) in
  add value_right;
  let typ_tuple = Typ.Make.tuple [ typ; typ ] in
  let value = Value.Make.tuple typ_tuple [ value_left; value_right ] in
  add value;
  value

(* dec $assoc_<X, Y>(X, (X, Y)* ) : Y? *)

let assoc_ (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, value_list = Extract.two at values_input in
  let values =
    value_list |> Value.Get.list
    |> List.map (fun value ->
           match value.it with
           | TupleV [ value_key; value_value ] -> (value_key, value_value)
           | _ -> assert false)
  in
  let typ_opt = Typ.Make.opt typ_value in
  let value_opt =
    List.fold_left
      (fun value_found (value_key, value_value) ->
        match value_found with
        | Some _ -> value_found
        | None when Value.compare value value_key = 0 -> Some value_value
        | None -> None)
      None values
  in
  let value = Value.Make.opt typ_opt value_opt in
  add value;
  value

(* dec $sort_<X>((nat, X)* ) : (nat, X)* *)

let sort_ (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_value = Extract.one at targs in
  let typ = Typ.Make.tuple [ Typ.Make.nat; typ_value ] |> Typ.Make.list in
  let value_list = Extract.one at values_input in
  let values =
    value_list |> Value.Get.list
    |> List.map (fun value ->
           match value.it with
           | TupleV [ value_key; value_value ] ->
               let n_key = value_key |> Value.Get.num |> Num.to_int in
               (n_key, (value_key, value_value, value.at, value.note))
           | _ -> assert false)
  in
  let values =
    List.sort (fun (n_a, _) (n_b, _) -> Bigint.compare n_a n_b) values
  in
  let values =
    List.map
      (fun (_, (value_key, value_value, at, note)) ->
        TupleV [ value_key; value_value ] $$ (at, note))
      values
  in
  let value = Value.Make.list typ values in
  add value;
  value

(* builtin dec $transpose_<X>(X** ) : X** *)

let transpose_ (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ = Extract.one at targs in
  let typ_list = Typ.Make.list typ in
  let typ_matrix = Typ.Make.list typ_list in
  let value = Extract.one at values_input in
  let value_matrix =
    value |> Value.Get.list |> List.map (fun value -> value |> Value.Get.list)
  in
  let value_matrix =
    match value_matrix with
    | [] -> []
    | value_row_h :: _ -> (
        let width = List.length value_row_h in
        let value_cols = Array.make width [] in
        try
          List.iter
            (fun value_row ->
              if List.length value_row <> width then
                raise (Invalid_argument "cannot transpose a matrix of values");
              List.iteri
                (fun j value -> value_cols.(j) <- value :: value_cols.(j))
                value_row)
            (List.rev value_matrix);
          Array.to_list value_cols
        with Invalid_argument msg -> error no_region msg)
  in
  let value =
    value_matrix
    |> List.map (fun values_row ->
           let value_row = Value.Make.list typ_list values_row in
           add value_row;
           value_row)
    |> Value.Make.list typ_matrix
  in
  add value;
  value