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

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

(* Value set *)

module VSet = Set.Make (Value)

type set = VSet.t

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

let mixop_set = Value.Mixops.of_string "`{ k `}"

let set_of_value (value : value) : set =
  match value.it with
  | CaseV valuecase when Mixfix.eq_mixop valuecase mixop_set -> (
      match Mixfix.args valuecase with
      | [ value_elements ] -> value_elements |> Value.Get.list |> VSet.of_list
      | _ -> assert false)
  | _ ->
      error no_region
        (Format.asprintf "expected a set, but got %s" (Value.to_string value))

let value_of_set (add : value -> unit) (typ_key : typ) (set : set) : value =
  let values_element = VSet.elements set in
  let typ_list = Typ.Make.list typ_key in
  let value_elements = Value.Make.list typ_list values_element in
  add value_elements;
  let value =
    let typ = Typ.Make.var ("set" $ no_region) [ typ_key ] in
    let valuecase = Mixfix.fill mixop_set [ value_elements ] in
    Value.Make.case typ valuecase
  in
  add value;
  value

(* dec $intersect_set<K>(set<K>, set<K>) : set<K> *)

let intersect_set (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key = Extract.one at targs in
  let value_set_a, value_set_b = Extract.two at values_input in
  let set_a = set_of_value value_set_a in
  let set_b = set_of_value value_set_b in
  VSet.inter set_a set_b |> value_of_set add typ_key

(* dec $union_set<K>(set<K>, set<K>) : set<K> *)

let union_set (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key = Extract.one at targs in
  let value_set_a, value_set_b = Extract.two at values_input in
  let set_a = set_of_value value_set_a in
  let set_b = set_of_value value_set_b in
  VSet.union set_a set_b |> value_of_set add typ_key

(* dec $unions_set<K>(set<K>* ) : set<K> *)

let unions_set (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key = Extract.one at targs in
  let value_sets = Extract.one at values_input in
  let sets = value_sets |> Value.Get.list |> List.map set_of_value in
  sets |> List.fold_left VSet.union VSet.empty |> value_of_set add typ_key

(* dec $diff_set<K>(set<K>, set<K>) : set<K> *)

let diff_set (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let typ_key = Extract.one at targs in
  let value_set_a, value_set_b = Extract.two at values_input in
  let set_a = set_of_value value_set_a in
  let set_b = set_of_value value_set_b in
  VSet.diff set_a set_b |> value_of_set add typ_key

(* dec $sub_set<K>(set<K>, set<K>) : bool *)

let sub_set (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let _typ_key = Extract.one at targs in
  let value_set_a, value_set_b = Extract.two at values_input in
  let set_a = set_of_value value_set_a in
  let set_b = set_of_value value_set_b in
  let value = Value.Make.bool (VSet.subset set_a set_b) in
  add value;
  value

(* dec $eq_set<K>(set<K>, set<K>) : bool *)

let eq_set (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  let _typ_key = Extract.one at targs in
  let value_set_a, value_set_b = Extract.two at values_input in
  let set_a = set_of_value value_set_a in
  let set_b = set_of_value value_set_b in
  let value = Value.Make.bool (VSet.equal set_a set_b) in
  add value;
  value