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

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

(* dec $text_to_int(text) : int *)

let text_to_int (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  Extract.zero at targs;
  let text = Extract.one at values_input |> Value.Get.text in
  let i = Bigint.of_string text in
  let value = Value.Make.int i in
  add value;
  value

(* dec $int_to_text(int) : text *)

let int_to_text (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  Extract.zero at targs;
  let num = Extract.one at values_input |> Value.Get.num in
  let value = Value.Make.text (Num.string_of_num num) in
  add value;
  value

(* dec $split_text(text, text) : text* *)

let split_text (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  Extract.zero at targs;
  let value_text, value_separator = Extract.two at values_input in
  let text = Value.Get.text value_text in
  let separator = Value.Get.text value_separator in
  assert (String.length separator = 1);
  let parts = String.split_on_char (String.get separator 0) text in
  let values = List.map Value.Make.text parts in
  let typ_list = Typ.Make.list Typ.Make.bool in
  let value = Value.Make.list typ_list values in
  add value;
  value

(* dec $strip_prefix(text, text) : text *)

let strip_prefix (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  Extract.zero at targs;
  let value_text, value_prefix = Extract.two at values_input in
  let text = Value.Get.text value_text in
  let prefix = Value.Get.text value_prefix in
  assert (String.starts_with ~prefix text);
  let text =
    String.sub text (String.length prefix)
      (String.length text - String.length prefix)
  in
  let value = Value.Make.text text in
  add value;
  value

(* dec $strip_suffix(text, text) : text *)

let strip_suffix (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  Extract.zero at targs;
  let value_text, value_suffix = Extract.two at values_input in
  let text = Value.Get.text value_text in
  let suffix = Value.Get.text value_suffix in
  assert (String.ends_with ~suffix text);
  let text = String.sub text 0 (String.length text - String.length suffix) in
  let value = Value.Make.text text in
  add value;
  value

(* dec $strip_all_whitespace(text) : text *)

let strip_all_whitespace (add : value -> unit) (at : region) (targs : targ list)
    (values_input : value list) : value =
  Extract.zero at targs;
  let value = Extract.one at values_input in
  let text =
    value |> Value.Get.text |> String.split_on_char ' ' |> String.concat ""
  in
  let value = Value.Make.text text in
  add value;
  value