Source file Parser.ml

module MenhirBasics = struct
  
  exception Error
  
  let _eRR : exn =
    Error
  
  type token = 
    | ZERO
    | P
    | LIT of (
# 13 "src/dimacs/Parser.mly"
       (int)
# 16 "src/dimacs/Parser.ml"
  )
    | EOF
    | CNF
  
end

include MenhirBasics

type _menhir_env = {
  _menhir_lexer: Lexing.lexbuf -> token;
  _menhir_lexbuf: Lexing.lexbuf;
  _menhir_token: token;
  mutable _menhir_error: bool
}

and _menhir_state = 
  | MenhirState15
  | MenhirState8
  | MenhirState6

# 3 "src/dimacs/Parser.mly"
  
  open Mc2_core

  let lnum pos = pos.Lexing.pos_lnum
  let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
  let pp_pos out (start,stop) =
    Format.fprintf out "(at %d:%d - %d:%d)"
      (lnum start) (cnum start) (lnum stop) (cnum stop)

# 47 "src/dimacs/Parser.ml"

let rec _menhir_goto_list_clause_ : _menhir_env -> 'ttv_tail -> _menhir_state -> 'tv_list_clause_ -> 'ttv_return =
  fun _menhir_env _menhir_stack _menhir_s _v ->
    match _menhir_s with
    | MenhirState6 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv69) = Obj.magic _menhir_stack in
        let (_menhir_s : _menhir_state) = _menhir_s in
        let (_v : 'tv_list_clause_) = _v in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv67) = Obj.magic _menhir_stack in
        let (_menhir_s : _menhir_state) = _menhir_s in
        let ((l : 'tv_list_clause_) : 'tv_list_clause_) = _v in
        ((let _v : 'tv_clauses = 
# 32 "src/dimacs/Parser.mly"
              ( l )
# 64 "src/dimacs/Parser.ml"
         in
        _menhir_goto_clauses _menhir_env _menhir_stack _menhir_s _v) : 'freshtv68)) : 'freshtv70)
    | MenhirState15 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv73 * _menhir_state * 'tv_clause) = Obj.magic _menhir_stack in
        let (_menhir_s : _menhir_state) = _menhir_s in
        let (_v : 'tv_list_clause_) = _v in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv71 * _menhir_state * 'tv_clause) = Obj.magic _menhir_stack in
        let (_ : _menhir_state) = _menhir_s in
        let ((xs : 'tv_list_clause_) : 'tv_list_clause_) = _v in
        ((let (_menhir_stack, _menhir_s, (x : 'tv_clause)) = _menhir_stack in
        let _v : 'tv_list_clause_ = 
# 213 "<standard.mly>"
    ( x :: xs )
# 80 "src/dimacs/Parser.ml"
         in
        _menhir_goto_list_clause_ _menhir_env _menhir_stack _menhir_s _v) : 'freshtv72)) : 'freshtv74)
    | _ ->
        let (() : unit) = () in
        ((Printf.eprintf "Internal failure -- please contact the parser generator's developers.\n%!";
        assert false) : 'freshtv75)

and _menhir_goto_nonempty_list_LIT_ : _menhir_env -> 'ttv_tail -> _menhir_state -> 'tv_nonempty_list_LIT_ -> 'ttv_return =
  fun _menhir_env _menhir_stack _menhir_s _v ->
    let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
    match _menhir_s with
    | MenhirState8 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : ('freshtv53 * _menhir_state * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 97 "src/dimacs/Parser.ml"
        )) * _menhir_state * 'tv_nonempty_list_LIT_) = Obj.magic _menhir_stack in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : ('freshtv51 * _menhir_state * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 103 "src/dimacs/Parser.ml"
        )) * _menhir_state * 'tv_nonempty_list_LIT_) = Obj.magic _menhir_stack in
        ((let ((_menhir_stack, _menhir_s, (x : (
# 13 "src/dimacs/Parser.mly"
       (int)
# 108 "src/dimacs/Parser.ml"
        ))), _, (xs : 'tv_nonempty_list_LIT_)) = _menhir_stack in
        let _v : 'tv_nonempty_list_LIT_ = 
# 223 "<standard.mly>"
    ( x :: xs )
# 113 "src/dimacs/Parser.ml"
         in
        _menhir_goto_nonempty_list_LIT_ _menhir_env _menhir_stack _menhir_s _v) : 'freshtv52)) : 'freshtv54)
    | MenhirState15 | MenhirState6 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv65 * _menhir_state * 'tv_nonempty_list_LIT_) = Obj.magic _menhir_stack in
        ((assert (not _menhir_env._menhir_error);
        let _tok = _menhir_env._menhir_token in
        match _tok with
        | ZERO ->
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv61 * _menhir_state * 'tv_nonempty_list_LIT_) = Obj.magic _menhir_stack in
            ((let _menhir_env = _menhir_discard _menhir_env in
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv59 * _menhir_state * 'tv_nonempty_list_LIT_) = Obj.magic _menhir_stack in
            ((let (_menhir_stack, _menhir_s, (l : 'tv_nonempty_list_LIT_)) = _menhir_stack in
            let _v : 'tv_clause = 
# 43 "src/dimacs/Parser.mly"
                ( l )
# 132 "src/dimacs/Parser.ml"
             in
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv57) = _menhir_stack in
            let (_menhir_s : _menhir_state) = _menhir_s in
            let (_v : 'tv_clause) = _v in
            ((let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv55 * _menhir_state * 'tv_clause) = Obj.magic _menhir_stack in
            ((assert (not _menhir_env._menhir_error);
            let _tok = _menhir_env._menhir_token in
            match _tok with
            | LIT _v ->
                _menhir_run8 _menhir_env (Obj.magic _menhir_stack) MenhirState15 _v
            | EOF ->
                _menhir_reduce5 _menhir_env (Obj.magic _menhir_stack) MenhirState15
            | _ ->
                assert (not _menhir_env._menhir_error);
                _menhir_env._menhir_error <- true;
                _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState15) : 'freshtv56)) : 'freshtv58)) : 'freshtv60)) : 'freshtv62)
        | _ ->
            assert (not _menhir_env._menhir_error);
            _menhir_env._menhir_error <- true;
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv63 * _menhir_state * 'tv_nonempty_list_LIT_) = Obj.magic _menhir_stack in
            ((let (_menhir_stack, _menhir_s, _) = _menhir_stack in
            _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s) : 'freshtv64)) : 'freshtv66)

and _menhir_goto_clauses : _menhir_env -> 'ttv_tail -> _menhir_state -> 'tv_clauses -> 'ttv_return =
  fun _menhir_env _menhir_stack _menhir_s _v ->
    let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
    let (_menhir_env : _menhir_env) = _menhir_env in
    let (_menhir_stack : ('freshtv49 * 'tv_prelude) * _menhir_state * 'tv_clauses) = Obj.magic _menhir_stack in
    ((assert (not _menhir_env._menhir_error);
    let _tok = _menhir_env._menhir_token in
    match _tok with
    | EOF ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : ('freshtv45 * 'tv_prelude) * _menhir_state * 'tv_clauses) = Obj.magic _menhir_stack in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : ('freshtv43 * 'tv_prelude) * _menhir_state * 'tv_clauses) = Obj.magic _menhir_stack in
        ((let ((_menhir_stack, _), _, (l : 'tv_clauses)) = _menhir_stack in
        let _v : (
# 18 "src/dimacs/Parser.mly"
      (int list list)
# 177 "src/dimacs/Parser.ml"
        ) = 
# 40 "src/dimacs/Parser.mly"
                          ( l )
# 181 "src/dimacs/Parser.ml"
         in
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv41) = _menhir_stack in
        let (_v : (
# 18 "src/dimacs/Parser.mly"
      (int list list)
# 188 "src/dimacs/Parser.ml"
        )) = _v in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv39) = Obj.magic _menhir_stack in
        let (_v : (
# 18 "src/dimacs/Parser.mly"
      (int list list)
# 195 "src/dimacs/Parser.ml"
        )) = _v in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv37) = Obj.magic _menhir_stack in
        let ((_1 : (
# 18 "src/dimacs/Parser.mly"
      (int list list)
# 202 "src/dimacs/Parser.ml"
        )) : (
# 18 "src/dimacs/Parser.mly"
      (int list list)
# 206 "src/dimacs/Parser.ml"
        )) = _v in
        (Obj.magic _1 : 'freshtv38)) : 'freshtv40)) : 'freshtv42)) : 'freshtv44)) : 'freshtv46)
    | _ ->
        assert (not _menhir_env._menhir_error);
        _menhir_env._menhir_error <- true;
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : ('freshtv47 * 'tv_prelude) * _menhir_state * 'tv_clauses) = Obj.magic _menhir_stack in
        ((let (_menhir_stack, _menhir_s, _) = _menhir_stack in
        _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s) : 'freshtv48)) : 'freshtv50)

and _menhir_reduce5 : _menhir_env -> 'ttv_tail -> _menhir_state -> 'ttv_return =
  fun _menhir_env _menhir_stack _menhir_s ->
    let _v : 'tv_list_clause_ = 
# 211 "<standard.mly>"
    ( [] )
# 222 "src/dimacs/Parser.ml"
     in
    _menhir_goto_list_clause_ _menhir_env _menhir_stack _menhir_s _v

and _menhir_run8 : _menhir_env -> 'ttv_tail -> _menhir_state -> (
# 13 "src/dimacs/Parser.mly"
       (int)
# 229 "src/dimacs/Parser.ml"
) -> 'ttv_return =
  fun _menhir_env _menhir_stack _menhir_s _v ->
    let _menhir_stack = (_menhir_stack, _menhir_s, _v) in
    let _menhir_env = _menhir_discard _menhir_env in
    let _tok = _menhir_env._menhir_token in
    match _tok with
    | LIT _v ->
        _menhir_run8 _menhir_env (Obj.magic _menhir_stack) MenhirState8 _v
    | ZERO ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv35 * _menhir_state * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 243 "src/dimacs/Parser.ml"
        )) = Obj.magic _menhir_stack in
        ((let (_menhir_stack, _menhir_s, (x : (
# 13 "src/dimacs/Parser.mly"
       (int)
# 248 "src/dimacs/Parser.ml"
        ))) = _menhir_stack in
        let _v : 'tv_nonempty_list_LIT_ = 
# 221 "<standard.mly>"
    ( [ x ] )
# 253 "src/dimacs/Parser.ml"
         in
        _menhir_goto_nonempty_list_LIT_ _menhir_env _menhir_stack _menhir_s _v) : 'freshtv36)
    | _ ->
        assert (not _menhir_env._menhir_error);
        _menhir_env._menhir_error <- true;
        _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState8

and _menhir_errorcase : _menhir_env -> 'ttv_tail -> _menhir_state -> 'ttv_return =
  fun _menhir_env _menhir_stack _menhir_s ->
    match _menhir_s with
    | MenhirState15 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv25 * _menhir_state * 'tv_clause) = Obj.magic _menhir_stack in
        ((let (_menhir_stack, _menhir_s, _) = _menhir_stack in
        _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s) : 'freshtv26)
    | MenhirState8 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv27 * _menhir_state * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 274 "src/dimacs/Parser.ml"
        )) = Obj.magic _menhir_stack in
        ((let (_menhir_stack, _menhir_s, _) = _menhir_stack in
        _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) _menhir_s) : 'freshtv28)
    | MenhirState6 ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv33 * 'tv_prelude) = Obj.magic _menhir_stack in
        ((let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv31) = Obj.magic _menhir_stack in
        let (_endpos : Lexing.position) = _menhir_env._menhir_lexbuf.Lexing.lex_curr_p in
        let (_menhir_s : _menhir_state) = MenhirState6 in
        let (_startpos : Lexing.position) = _menhir_env._menhir_lexbuf.Lexing.lex_start_p in
        ((let _menhir_env = _menhir_discard _menhir_env in
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv29) = Obj.magic _menhir_stack in
        let (_endpos__1_ : Lexing.position) = _endpos in
        let (_menhir_s : _menhir_state) = _menhir_s in
        let (_startpos__1_ : Lexing.position) = _startpos in
        ((let _v : 'tv_clauses = let _endpos = _endpos__1_ in
        let _startpos = _startpos__1_ in
        
# 34 "src/dimacs/Parser.mly"
    (
      Error.errorf "expected list of clauses %a"
        pp_pos (_startpos,_endpos)
    )
# 300 "src/dimacs/Parser.ml"
         in
        _menhir_goto_clauses _menhir_env _menhir_stack _menhir_s _v) : 'freshtv30)) : 'freshtv32)) : 'freshtv34)

and _menhir_error0 : _menhir_env -> 'ttv_tail -> 'ttv_return =
  fun _menhir_env _menhir_stack ->
    let (_menhir_env : _menhir_env) = _menhir_env in
    let (_menhir_stack : 'freshtv23) = Obj.magic _menhir_stack in
    let (_endpos : Lexing.position) = _menhir_env._menhir_lexbuf.Lexing.lex_curr_p in
    let (_startpos : Lexing.position) = _menhir_env._menhir_lexbuf.Lexing.lex_start_p in
    ((let _menhir_env = _menhir_discard _menhir_env in
    let (_menhir_env : _menhir_env) = _menhir_env in
    let (_menhir_stack : 'freshtv21) = Obj.magic _menhir_stack in
    let (_endpos__1_ : Lexing.position) = _endpos in
    let (_startpos__1_ : Lexing.position) = _startpos in
    ((let _v : 'tv_prelude = let _endpos = _endpos__1_ in
    let _startpos = _startpos__1_ in
    
# 27 "src/dimacs/Parser.mly"
    (
      Error.errorf "expected prelude %a" pp_pos (_startpos,_endpos)
    )
# 322 "src/dimacs/Parser.ml"
     in
    _menhir_goto_prelude _menhir_env _menhir_stack _v) : 'freshtv22)) : 'freshtv24)

and _menhir_goto_prelude : _menhir_env -> 'ttv_tail -> 'tv_prelude -> 'ttv_return =
  fun _menhir_env _menhir_stack _v ->
    let _menhir_stack = (_menhir_stack, _v) in
    let (_menhir_env : _menhir_env) = _menhir_env in
    let (_menhir_stack : 'freshtv19 * 'tv_prelude) = Obj.magic _menhir_stack in
    ((if _menhir_env._menhir_error then
      _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState6
    else
      let _tok = _menhir_env._menhir_token in
      match _tok with
      | LIT _v ->
          _menhir_run8 _menhir_env (Obj.magic _menhir_stack) MenhirState6 _v
      | EOF ->
          _menhir_reduce5 _menhir_env (Obj.magic _menhir_stack) MenhirState6
      | _ ->
          (assert (not _menhir_env._menhir_error);
          _menhir_env._menhir_error <- true;
          _menhir_errorcase _menhir_env (Obj.magic _menhir_stack) MenhirState6)) : 'freshtv20)

and _menhir_discard : _menhir_env -> _menhir_env =
  fun _menhir_env ->
    let lexer = _menhir_env._menhir_lexer in
    let lexbuf = _menhir_env._menhir_lexbuf in
    let _tok = lexer lexbuf in
    {
      _menhir_lexer = lexer;
      _menhir_lexbuf = lexbuf;
      _menhir_token = _tok;
      _menhir_error = false;
    }

and file : (Lexing.lexbuf -> token) -> Lexing.lexbuf -> (
# 18 "src/dimacs/Parser.mly"
      (int list list)
# 360 "src/dimacs/Parser.ml"
) =
  fun lexer lexbuf ->
    let _menhir_env = {
      _menhir_lexer = lexer;
      _menhir_lexbuf = lexbuf;
      _menhir_token = Obj.magic ();
      _menhir_error = false;
    } in
    Obj.magic (let (_menhir_env : _menhir_env) = _menhir_env in
    let (_menhir_stack : 'freshtv17) = ((), _menhir_env._menhir_lexbuf.Lexing.lex_curr_p) in
    ((let _menhir_env = _menhir_discard _menhir_env in
    let _tok = _menhir_env._menhir_token in
    match _tok with
    | P ->
        let (_menhir_env : _menhir_env) = _menhir_env in
        let (_menhir_stack : 'freshtv15) = Obj.magic _menhir_stack in
        ((let _menhir_env = _menhir_discard _menhir_env in
        let _tok = _menhir_env._menhir_token in
        match _tok with
        | CNF ->
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv11) = Obj.magic _menhir_stack in
            ((let _menhir_env = _menhir_discard _menhir_env in
            let _tok = _menhir_env._menhir_token in
            match _tok with
            | LIT _v ->
                let (_menhir_env : _menhir_env) = _menhir_env in
                let (_menhir_stack : ('freshtv7)) = Obj.magic _menhir_stack in
                let (_v : (
# 13 "src/dimacs/Parser.mly"
       (int)
# 392 "src/dimacs/Parser.ml"
                )) = _v in
                ((let _menhir_stack = (_menhir_stack, _v) in
                let _menhir_env = _menhir_discard _menhir_env in
                let _tok = _menhir_env._menhir_token in
                match _tok with
                | LIT _v ->
                    let (_menhir_env : _menhir_env) = _menhir_env in
                    let (_menhir_stack : (('freshtv3)) * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 403 "src/dimacs/Parser.ml"
                    )) = Obj.magic _menhir_stack in
                    let (_v : (
# 13 "src/dimacs/Parser.mly"
       (int)
# 408 "src/dimacs/Parser.ml"
                    )) = _v in
                    ((let _menhir_env = _menhir_discard _menhir_env in
                    let (_menhir_env : _menhir_env) = _menhir_env in
                    let (_menhir_stack : (('freshtv1)) * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 415 "src/dimacs/Parser.ml"
                    )) = Obj.magic _menhir_stack in
                    let (_ : (
# 13 "src/dimacs/Parser.mly"
       (int)
# 420 "src/dimacs/Parser.ml"
                    )) = _v in
                    ((let (_menhir_stack, _) = _menhir_stack in
                    let _v : 'tv_prelude = 
# 25 "src/dimacs/Parser.mly"
                  ( () )
# 426 "src/dimacs/Parser.ml"
                     in
                    _menhir_goto_prelude _menhir_env _menhir_stack _v) : 'freshtv2)) : 'freshtv4)
                | _ ->
                    assert (not _menhir_env._menhir_error);
                    _menhir_env._menhir_error <- true;
                    let (_menhir_env : _menhir_env) = _menhir_env in
                    let (_menhir_stack : (('freshtv5)) * (
# 13 "src/dimacs/Parser.mly"
       (int)
# 436 "src/dimacs/Parser.ml"
                    )) = Obj.magic _menhir_stack in
                    ((let (_menhir_stack, _) = _menhir_stack in
                    _menhir_error0 _menhir_env (Obj.magic _menhir_stack)) : 'freshtv6)) : 'freshtv8)
            | _ ->
                assert (not _menhir_env._menhir_error);
                _menhir_env._menhir_error <- true;
                let (_menhir_env : _menhir_env) = _menhir_env in
                let (_menhir_stack : ('freshtv9)) = Obj.magic _menhir_stack in
                (_menhir_error0 _menhir_env (Obj.magic _menhir_stack) : 'freshtv10)) : 'freshtv12)
        | _ ->
            assert (not _menhir_env._menhir_error);
            _menhir_env._menhir_error <- true;
            let (_menhir_env : _menhir_env) = _menhir_env in
            let (_menhir_stack : 'freshtv13) = Obj.magic _menhir_stack in
            (_menhir_error0 _menhir_env (Obj.magic _menhir_stack) : 'freshtv14)) : 'freshtv16)
    | _ ->
        assert (not _menhir_env._menhir_error);
        _menhir_env._menhir_error <- true;
        _menhir_error0 _menhir_env (Obj.magic _menhir_stack)) : 'freshtv18))

# 269 "<standard.mly>"
  

# 460 "src/dimacs/Parser.ml"