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

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

(* Deterministic backtracking *)

type failtrace = Util.Attempt.failtrace

type ('a, 'b) backtrack_det =
  | Ok_det of 'a
  | Err_det of failtrace list
  | Unmatch_det of failtrace list
  | Nondet_det of 'b * 'b

(* Conversion *)

let as_det (backtrack : 'a backtrack) : ('a, 'b) backtrack_det =
  match backtrack with
  | Ok a -> Ok_det a
  | Err failtraces -> Err_det failtraces
  | Unmatch failtraces -> Unmatch_det failtraces

(* Backtracking *)

let back_unmatch_silent : ('a, 'b) backtrack_det = Unmatch_det []

(* Choice (deterministic) *)

let choose_deterministic (items : 'b list) fs =
  let choose_deterministic (items : 'b list) fs =
    List.fold_left2
      (fun backtrack_det item f ->
        match backtrack_det with
        | Ok_det (item_det, a_det) -> (
            match f () with
            | Ok _ -> Nondet_det (item_det, item)
            | Err failtraces -> Err_det failtraces
            | Unmatch _ -> Ok_det (item_det, a_det))
        | Err_det failtraces_det -> Err_det failtraces_det
        | Unmatch_det failtraces_det -> (
            match f () with
            | Ok a -> Ok_det (item, a)
            | Err failtraces -> Err_det failtraces
            | Unmatch failtraces -> Unmatch_det (failtraces_det @ failtraces))
        | Nondet_det _ -> backtrack_det)
      back_unmatch_silent items fs
  in
  match choose_deterministic items fs with
  | Ok_det (_, a_det) -> Ok_det a_det
  | Err_det failtraces -> Err_det failtraces
  | Unmatch_det failtraces -> Unmatch_det failtraces
  | Nondet_det (item_a, item_b) -> Nondet_det (item_a, item_b)