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

Source file backtrack.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
open Error
open Util.Attempt
open Util.Source

(* Backtracking *)

type 'a backtrack =
  | Ok of 'a
  | Err of failtrace list
  | Unmatch of failtrace list

(* Backtracing *)

let back_err (at : region) (msg : string) : 'a backtrack =
  Err [ Failtrace (at, (fun () -> msg), []) ]

let back_unmatch_silent : 'a backtrack = Unmatch []

let back_unmatch (at : region) (msg : string) : 'a backtrack =
  Unmatch [ Failtrace (at, (fun () -> msg), []) ]

let back_nest (at : region) (msg : unit -> string) (backtrack : 'a backtrack) :
    'a backtrack =
  match backtrack with
  | Ok a -> Ok a
  | Err failtraces -> Err [ Failtrace (at, msg, failtraces) ]
  | Unmatch failtraces -> Unmatch [ Failtrace (at, msg, failtraces) ]

(* Check *)

let check_back_err (b : bool) (at : region) (msg : string) : unit backtrack =
  if b then Ok () else back_err at msg

(* Choose (sequential) *)

let rec choose_sequential = function
  | [] -> back_unmatch_silent
  | f :: fs -> (
      match f () with
      | Ok a -> Ok a
      | Err _ as backtrack -> backtrack
      | Unmatch failtraces -> (
          match choose_sequential fs with
          | Ok a -> Ok a
          | Err _ as backtrack -> backtrack
          | Unmatch failtraces_t -> Unmatch (failtraces @ failtraces_t)))

(* Monadic interface *)

let ( let* ) (backtrack : 'a backtrack) (f : 'a -> 'b) : 'b =
  match backtrack with
  | Ok a -> f a
  | Err _ as backtrack -> backtrack
  | Unmatch _ as backtrack -> backtrack

let ( let+ ) (backtrack : 'a backtrack) (f : 'a -> 'b) : 'b =
  match backtrack with
  | Ok a -> f a
  | Err failtraces | Unmatch failtraces ->
      error no_region (string_of_failtraces_short failtraces)