(module cnf-parser mzscheme
  
  (require (lib "yacc.ss" "parser-tools")
           (lib "lex.ss" "parser-tools")
           (prefix : (lib "lex-sre.ss" "parser-tools")))
  
  (provide cnf-parser cnf-lexer)
  
  (define-tokens tok (NUM))
  (define-empty-tokens etok (EOF INITINFO ENDCLAUSE))
  
  (define-lex-abbrevs 
    (integer (:: (:? #\-) (:/ #\1 #\9) (:* (:/ #\0 #\9))))
    (comment (:: (:? #\newline) #\c (:* (:~ #\newline)) #\newline))
    (white-space (:or #\newline #\return #\tab #\space #\vtab))
    (initinfo (:: #\p (:+ whitespace) "cnf")))
  
  (define cnf-lexer
    (lexer
     [(eof) 'EOF]
     
     ;; Ignore comments and newlines
     [(:or comment white-space) (cnf-lexer input-port)]
    
     [#\0 'ENDCLAUSE]
     [initinfo 'INITINFO]
     [integer (token-NUM (string->number lexeme))]
     [any-char (printf "None Matched!")])) 
  
  (define cnf-parser
      (parser
       
       (start start)
       (end EOF)
       (tokens tok etok)
       (error (lambda (a b c) (printf "Token OK?: ~a~nToken Name: ~a~nToken Value:~a~n" a b c)))
       
       (grammar
        (start [(INITINFO NUM NUM clause-list)
                (cons (list $2 $3)
                      $4)])
       
        (clause-list [(clause) (list $1)]
                     [(clause-list clause) (cons $2 $1)])
        
        (clause [(literal-list ENDCLAUSE) $1])
        
        (literal-list [(NUM) (list $1)]
                      [(literal-list NUM) (cons $2 $1)])))))