package p4spectec

  1. Overview
  2. Docs
package p4spectec
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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)