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/p4spectec.util/attempt.ml.html

Source file attempt.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
open Source

(* Backtracking *)

type failtrace = Failtrace of region * (unit -> string) * failtrace list
type 'a attempt = Ok of 'a | Fail of failtrace list

(* Failures *)

let rec depth_of (failtrace : failtrace) : int =
  let (Failtrace (_, _, subfailtraces)) = failtrace in
  let depth_sub = List.map depth_of subfailtraces |> List.fold_left max 0 in
  depth_sub + 1

let fail (at : region) (msg : string) : 'a attempt =
  Fail [ Failtrace (at, (fun () -> msg), []) ]

let fail_silent : 'a attempt = Fail []

(* Choosing between attempts *)

let rec choose_sequential = function
  | [] -> fail_silent
  | f :: fs -> (
      match f () with
      | Ok a -> Ok a
      | Fail failtraces_h -> (
          match choose_sequential fs with
          | Ok a -> Ok a
          | Fail failtraces_t -> Fail (failtraces_h @ failtraces_t)))

(* Nesting attempts *)

let nest at msg attempt =
  match attempt with
  | Ok a -> Ok a
  | Fail failtraces -> Fail [ Failtrace (at, (fun () -> msg), failtraces) ]

(* Error with backfailtraces

   Show at most [short_window] frames of each root-to-leaf path *)

let short_window = 10

let region_line (indent : string) (region : region) : string =
  if region = no_region then "" else string_of_region region ^ "\n" ^ indent

let rec string_of_failtrace ~(indent : string) ~(run : int) ~(root : bool)
    ~(last : bool) ~(bullet : string) (failtrace : failtrace) : string =
  let (Failtrace (region, msg, failtraces_sub)) = failtrace in
  if (not root) && depth_of failtrace > short_window then
    string_of_failtraces ~indent ~run:(run + 1) failtraces_sub
  else
    let msg = msg () in
    let marker =
      if run > 0 then
        Format.asprintf "%s│ ··· omitting %d traces ···\n" indent run
      else ""
    in
    let boundary = root || run > 0 in
    let node, indent_sub =
      if boundary then
        ( Format.asprintf "%s%s%s%s\n" indent
            (region_line indent region)
            bullet msg,
          indent )
      else
        let prefix = if last then "└── " else "├── " in
        let indent_sub = if last then indent ^ "    " else indent ^ "│   " in
        ( Format.asprintf "%s%s%s%s%s\n" indent prefix
            (region_line (indent ^ "    ") region)
            bullet msg,
          indent_sub )
    in
    marker ^ node
    ^ string_of_failtraces ~indent:indent_sub ~run:0 failtraces_sub

and string_of_failtraces ~(indent : string) ~(run : int)
    (failtraces : failtrace list) : string =
  match failtraces with
  | [] -> ""
  | [ failtrace ] ->
      string_of_failtrace ~indent ~run ~root:false ~last:true ~bullet:""
        failtrace
  | failtraces ->
      List.mapi
        (fun idx failtrace ->
          let last = idx = List.length failtraces - 1 in
          let bullet = string_of_int (idx + 1) ^ ". " in
          string_of_failtrace ~indent ~run ~root:false ~last ~bullet failtrace)
        failtraces
      |> String.concat ""

let string_of_failtraces_short (failtraces : failtrace list) : string =
  match failtraces with
  | [] -> ""
  | [ failtrace ] ->
      string_of_failtrace ~indent:"" ~run:0 ~root:true ~last:true ~bullet:""
        failtrace
  | failtraces ->
      List.mapi
        (fun idx failtrace ->
          let last = idx = List.length failtraces - 1 in
          let bullet = string_of_int (idx + 1) ^ ". " in
          string_of_failtrace ~indent:"" ~run:0 ~root:true ~last ~bullet
            failtrace)
        failtraces
      |> String.concat ""