accept.ml

type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)



type 'char c = 'char

type 'char re =
| Re_zero
| Re_unit
| Re_char of 'char c
| Re_plus of 'char re * 'char re
| Re_times of 'char re * 'char re
| Re_star of 'char re

type ('a, 'b) list_t = 'a option

(** val p_list_dec :
    ('a1 * 'a2) -> (('a1 * 'a2) -> __ -> bool) -> ('a1 -> 'a1 * 'a2) -> 'a1
    list -> ('a1, 'a2) list_t **)

let rec p_list_dec ab p_dec f = function
| [] -> None
| a :: l' -> if p_dec (f a) __ then Some a else p_list_dec ab p_dec f l'

type 'char regexps_no_c_t = 'char re list

(** val regexps_no_c_F :
    ('a1 -> 'a1 -> bool) -> ('a1 re * 'a1) -> (('a1 re * 'a1) -> __ -> 'a1
    regexps_no_c_t) -> 'a1 regexps_no_c_t **)

let regexps_no_c_F char_eq_dec rc regexps_no_c_rec =
  match fst rc with
  | Re_char c0 -> if char_eq_dec c0 (snd rc) then Re_unit :: [] else []
  | Re_plus (r1, r2) ->
    List.append (regexps_no_c_rec (r1, (snd rc)) __)
      (regexps_no_c_rec (r2, (snd rc)) __)
  | Re_times (r, r2) ->
    (match r with
     | Re_zero -> []
     | Re_unit -> regexps_no_c_rec (r2, (snd rc)) __
     | Re_char c0 -> if char_eq_dec c0 (snd rc) then r2 :: [] else []
     | Re_plus (r11, r12) ->
       List.append (regexps_no_c_rec ((Re_times (r11, r2)), (snd rc)) __)
         (regexps_no_c_rec ((Re_times (r12, r2)), (snd rc)) __)
     | Re_times (r11, r12) ->
       regexps_no_c_rec ((Re_times (r11, (Re_times (r12, r2)))), (snd rc)) __
     | Re_star r1 ->
       List.append (regexps_no_c_rec (r2, (snd rc)) __)
         (List.map (fun r' -> Re_times (r', (Re_times ((Re_star r1), r2))))
           (regexps_no_c_rec (r1, (snd rc)) __)))
  | Re_star r ->
    List.map (fun r' -> Re_times (r', (Re_star r)))
      (regexps_no_c_rec (r, (snd rc)) __)
  | _ -> []

(** val regexps_no_c :
    ('a1 -> 'a1 -> bool) -> ('a1 re * 'a1) -> 'a1 regexps_no_c_t **)

let rec regexps_no_c char_eq_dec a =
  regexps_no_c_F char_eq_dec a (fun y _ -> regexps_no_c char_eq_dec y)

type 'char accept_t = bool

(** val accept_list_dec :
    ('a1 re * 'a1 list) -> (('a1 re * 'a1 list) -> __ -> bool) -> ('a1 re ->
    'a1 re * 'a1 list) -> 'a1 re list -> ('a1 re, 'a1 list) list_t **)

let accept_list_dec =
  p_list_dec

(** val accept_F :
    ('a1 -> 'a1 -> bool) -> ('a1 re * 'a1 list) -> (('a1 re * 'a1 list) -> __
    -> 'a1 accept_t) -> 'a1 accept_t **)

let accept_F char_eq_dec rs accept_rec =
  match snd rs with
  | [] ->
    (match fst rs with
     | Re_zero -> false
     | Re_char _ -> false
     | Re_plus (r1, r2) ->
       if accept_rec (r1, []) __ then true else accept_rec (r2, []) __
     | Re_times (r1, r2) ->
       if accept_rec (r1, []) __ then accept_rec (r2, []) __ else false
     | _ -> true)
  | c0 :: s' ->
    (match fst rs with
     | Re_char c' -> (match s' with
                      | [] -> char_eq_dec c0 c'
                      | _ :: _ -> false)
     | Re_plus (r1, r2) ->
       if accept_rec (r1, (c0 :: s')) __
       then true
       else accept_rec (r2, (c0 :: s')) __
     | Re_times (r, r2) ->
       (match r with
        | Re_zero -> false
        | Re_unit -> accept_rec (r2, (c0 :: s')) __
        | Re_char c' ->
          if char_eq_dec c0 c' then accept_rec (r2, s') __ else false
        | Re_plus (r11, r12) ->
          if accept_rec ((Re_times (r11, r2)), (c0 :: s')) __
          then true
          else accept_rec ((Re_times (r12, r2)), (c0 :: s')) __
        | Re_times (r11, r12) ->
          accept_rec ((Re_times (r11, (Re_times (r12, r2)))), (c0 :: s')) __
        | Re_star r1 ->
          if accept_rec (r2, (c0 :: s')) __
          then true
          else (match accept_list_dec rs accept_rec (fun r0 -> ((Re_times
                        (r0, (Re_times ((Re_star r1), r2)))), s'))
                        (regexps_no_c char_eq_dec (r1, c0)) with
                | Some _ -> true
                | None -> false))
     | Re_star r' ->
       (match accept_list_dec rs accept_rec (fun r0 -> ((Re_times (r0,
                (Re_star r'))), s')) (regexps_no_c char_eq_dec (r', c0)) with
        | Some _ -> true
        | None -> false)
     | _ -> false)

(** val accept :
    ('a1 -> 'a1 -> bool) -> ('a1 re * 'a1 list) -> 'a1 accept_t **)

let rec accept char_eq_dec a =
  accept_F char_eq_dec a (fun y _ -> accept char_eq_dec y)