flush-buff := λ(: tks List<String>)(: buff S). (: (
   (match buff (
      ()
      ( SNil () )
      ( _ (set tks (LCons(
         (clone-rope buff)
         (close tks)
      ))))
   ))
   tks
) List<String>);

tokenize := λ(: file-contents String). (: (
   (let tks (: LEOF List<String>))
   (let buff SNil)
   (while (head-string file-contents) (
      (let c (head-string file-contents))
      (if (||( (==( c 10_u8 ))
       (||( (==( c 33_u8 ))
        (||( (==( c 35_u8 ))
         (||( (==( c 36_u8 ))
          (||( (==( c 37_u8 ))
           (||( (==( c 38_u8 ))
            (||( (==( c 39_u8 ))
             (||( (==( c 40_u8 ))
              (||( (==( c 41_u8 ))
               (||( (==( c 42_u8 ))
                (||( (==( c 43_u8 ))
                 (||( (==( c 44_u8 ))
                  (||( (==( c 45_u8 ))
                   (||( (==( c 46_u8 ))
                    (||( (==( c 47_u8 ))
                     (||( (==( c 58_u8 ))
                      (||( (==( c 59_u8 ))
                       (||( (==( c 60_u8 ))
                        (||( (==( c 61_u8 ))
                         (||( (==( c 62_u8 ))
                          (||( (==( c 63_u8 ))
                           (||( (==( c 64_u8 ))
                            (||( (==( c 91_u8 ))
                             (||( (==( c 92_u8 ))
                              (||( (==( c 93_u8 ))
                               (||( (==( c 94_u8 ))
                                (||( (==( c 96_u8 ))
                                 (||( (==( c 123_u8 ))
                                  (||( (==( c 124_u8 ))
                                   (||( (==( c 125_u8 ))
                                    (||( (==( c 126_u8 ))
                                         (==( 1_u8 0_u8 ))
                                    ))
                                   ))
                                  ))
                                 ))
                                ))
                               ))
                              ))
                             ))
                            ))
                           ))
                          ))
                         ))
                        ))
                       ))
                      ))
                     ))
                    ))
                   ))
                  ))
                 ))
                ))
               ))
              ))
             ))
            ))
           ))
          ))
         ))
        ))
       ))
      )) (
         (set tks (flush-buff( tks buff )))
         (set tks (flush-buff( tks (SAtom(clone-rope c)) )))
         (set buff SNil)
      ) (
         (match c (
            ()
            ( 9_u8 ( (set tks (flush-buff( tks buff ))) (set buff SNil) ))
            ( 32_u8 ( (set tks (flush-buff( tks buff ))) (set buff SNil) ))
            ( 34_u8 (
               (set tks (flush-buff( tks buff )))
               (set file-contents (tail-string file-contents))
               (let sbuff (SAtom '"_s))
               (while (!=( (head-string file-contents) 34_u8 )) (
                  (match (head-string file-contents) (
                     ()
                     ( 0_u8 (set file-contents '"_s) )
                     ( 92_u8 (
                        (set sbuff (SCons(
                           (close sbuff)
                           (close(SAtom(clone-rope(head-string file-contents))))
                        )))
                        (set file-contents (tail-string file-contents))
                        (set sbuff (SCons(
                           (close sbuff)
                           (close(SAtom(clone-rope(head-string file-contents))))
                        )))
                        (set file-contents (tail-string file-contents))
                     ))
                     ( sc (
                        (set sbuff (SCons(
                           (close sbuff)
                           (close(SAtom(clone-rope sc)))
                        )))
                        (set file-contents (tail-string file-contents))
                     ))
                  ))
               ))
               (set sbuff (SCons(
                  (close sbuff)
                  (close(SAtom '"_s))
               )))
               (set tks (flush-buff( tks sbuff )))
               (set buff SNil)
            ))
            ( _ (set buff (SCons(
               (close buff)
               (close(SAtom(clone-rope c)))
            ))))
         ))
      ))
      (set file-contents (tail-string file-contents))
   ))
   (reverse tks)
) List<String>);

parse-gnu := λ(: fp String). (: (
   (let r (SAtom(read-file 'LIB/default_validator.v_s)))
   (set r (SCons(
      (close r)
      (close(SAtom 'Definition\scontrol_flow_graph\s:=\n\s\s\slet\scfg\s:=\sempty_control_flow_graph\sin\n_s))
   )))
   (let tk (tokenize(read-file fp)))
   (let linebuff (: LEOF List<String>))
   (while (non-zero tk) (match tk (
      ()
      ( (LCons( '\n_s tl )) (
         (set r (SCons(
            (close r)
            (close(parse-gnu-line (reverse linebuff)))
         )))
         (set linebuff (: LEOF List<String>))
         (set tk tl)
      ))
      ( (LCons( hd tl )) (
         (set linebuff (LCons( hd (close linebuff) )))
         (set tk tl)
      ))
   )))
   (set r (SCons(
      (close r)
      (close(parse-gnu-line (reverse linebuff)))
   )))
   (set r (SCons(
      (close r)
      (close(SAtom '\s\s\scfg.\n\nCheck\seq_refl\s:\s\[control_flow_graph_assertions_reachable\scontrol_flow_graph\]\s=\strue.\n_s))
   )))
   r
) S);

parse-gnu-line := λ(: line List<String>). (: (
   (let r SNil)
   (if (non-zero line) (match line (
      ()
      ( (LCons( '._s (LCons( 'global_s (LCons( glb LEOF )) )) )) (
         (set r (SCons(
            (close r)
            (close(SCons(
               (close(SAtom '\s\s\slet\scfg\s:=\s\[declare_global\scfg\s"_s))
               (close(SCons(
                  (close(SAtom glb))
                  (close(SAtom '"\]\sin\n_s))
               )))
            )))
         )))
      ))
      ( (LCons( '._s (LCons( 'text_s LEOF )) )) (
         (set r (SCons(
            (close r)
            (close(SAtom '\s\s\slet\scfg\s:=\s\[declare_text\scfg\]\sin\n_s))
         )))
      ))
      ( (LCons( '._s (LCons( 'data_s LEOF )) )) (
         (set r (SCons(
            (close r)
            (close(SAtom '\s\s\slet\scfg\s:=\s\[declare_data\scfg\]\sin\n_s))
         )))
      ))
      ( (LCons( '._s (LCons( 'ascii_s (LCons( lit LEOF )) )) )) (
         (set r (SCons(
            (close r)
            (close(SCons(
               (close(SAtom '\s\s\slet\scfg\s:=\s\[commit_ascii\scfg\s_s))
               (close(SCons(
                  (close(SAtom lit))
                  (close(SAtom '\]\sin\n_s))
               )))
            )))
         )))
      ))
      ( (LCons( '._s (LCons( 'zero_s (LCons( lit LEOF )) )) )) (
         (set r (SCons(
            (close r)
            (close(SCons(
               (close(SAtom '\s\s\slet\scfg\s:=\s\[commit_zero\scfg\s_s))
               (close(SCons(
                  (close(SAtom lit))
                  (close(SAtom '\]\sin\n_s))
               )))
            )))
         )))
      ))
      ( (LCons( lbl (LCons( ':_s LEOF )) )) (
         (set r (SCons(
            (close r)
            (close(SCons(
               (close(SAtom '\s\s\slet\scfg\s:=\s\[declare_label\scfg\s"_s))
               (close(SCons(
                  (close(SAtom lbl))
                  (close(SAtom '"\]\sin\n_s))
               )))
            )))
         )))
      ))

      ( (LCons( '\o_s (LCons( 'expect_s tl )) )) (print 'Ignoring\sAssertion\n_s) )

      ( (LCons( 'call_s tl )) (set r (parse-gnu-uop( 'call_s tl ))) )
      ( (LCons( 'ret_s LEOF )) (set r (parse-gnu-zop( 'ret_s ))) )
      ( (LCons( 'syscall_s LEOF )) (set r (parse-gnu-zop( 'syscall_s ))) )

      ( (LCons( 'push_s tl )) (set r (parse-gnu-uop( 'push_s tl ))) )
      ( (LCons( 'pushb_s tl )) (set r (parse-gnu-uop( 'pushb_s tl ))) )
      ( (LCons( 'pushs_s tl )) (set r (parse-gnu-uop( 'pushs_s tl ))) )
      ( (LCons( 'pushw_s tl )) (set r (parse-gnu-uop( 'pushw_s tl ))) )
      ( (LCons( 'pushl_s tl )) (set r (parse-gnu-uop( 'pushl_s tl ))) )
      ( (LCons( 'pushq_s tl )) (set r (parse-gnu-uop( 'pushq_s tl ))) )
      ( (LCons( 'pusht_s tl )) (set r (parse-gnu-uop( 'pusht_s tl ))) )

      ( (LCons( 'pop_s tl )) (set r (parse-gnu-uop( 'pop_s tl ))) )
      ( (LCons( 'popb_s tl )) (set r (parse-gnu-uop( 'popb_s tl ))) )
      ( (LCons( 'pops_s tl )) (set r (parse-gnu-uop( 'pops_s tl ))) )
      ( (LCons( 'popw_s tl )) (set r (parse-gnu-uop( 'popw_s tl ))) )
      ( (LCons( 'popl_s tl )) (set r (parse-gnu-uop( 'popl_s tl ))) )
      ( (LCons( 'popq_s tl )) (set r (parse-gnu-uop( 'popq_s tl ))) )
      ( (LCons( 'popt_s tl )) (set r (parse-gnu-uop( 'popt_s tl ))) )

      ( (LCons( 'mov_s tl )) (set r (parse-gnu-binop( 'mov_s tl ))) )
      ( (LCons( 'movb_s tl )) (set r (parse-gnu-binop( 'movb_s tl ))) )
      ( (LCons( 'movs_s tl )) (set r (parse-gnu-binop( 'movs_s tl ))) )
      ( (LCons( 'movw_s tl )) (set r (parse-gnu-binop( 'movw_s tl ))) )
      ( (LCons( 'movl_s tl )) (set r (parse-gnu-binop( 'movl_s tl ))) )
      ( (LCons( 'movq_s tl )) (set r (parse-gnu-binop( 'movq_s tl ))) )
      ( (LCons( 'movt_s tl )) (set r (parse-gnu-binop( 'movt_s tl ))) )

      ( (LCons( 'sub_s tl )) (set r (parse-gnu-binop( 'sub_s tl ))) )
      ( (LCons( 'subb_s tl )) (set r (parse-gnu-binop( 'subb_s tl ))) )
      ( (LCons( 'subs_s tl )) (set r (parse-gnu-binop( 'subs_s tl ))) )
      ( (LCons( 'subw_s tl )) (set r (parse-gnu-binop( 'subw_s tl ))) )
      ( (LCons( 'subl_s tl )) (set r (parse-gnu-binop( 'subl_s tl ))) )
      ( (LCons( 'subq_s tl )) (set r (parse-gnu-binop( 'subq_s tl ))) )
      ( (LCons( 'subt_s tl )) (set r (parse-gnu-binop( 'subt_s tl ))) )

      ( (LCons( 'add_s tl )) (set r (parse-gnu-binop( 'add_s tl ))) )
      ( (LCons( 'addb_s tl )) (set r (parse-gnu-binop( 'addb_s tl ))) )
      ( (LCons( 'adds_s tl )) (set r (parse-gnu-binop( 'adds_s tl ))) )
      ( (LCons( 'addw_s tl )) (set r (parse-gnu-binop( 'addw_s tl ))) )
      ( (LCons( 'addl_s tl )) (set r (parse-gnu-binop( 'addl_s tl ))) )
      ( (LCons( 'addq_s tl )) (set r (parse-gnu-binop( 'addq_s tl ))) )
      ( (LCons( 'addt_s tl )) (set r (parse-gnu-binop( 'addt_s tl ))) )

      ( u (
         (print 'Unexpected\sLine\s_s)
         (while (non-zero u) (match u (
            ()
            ( (LCons( hd tl )) (
               (print hd)(print '\s_s)
               (set u tl)
            ))
         )))
         (print '\n_s)
         (exit 1_u64)
      ) )
   )) ())
   r
) S);

parse-gnu-zop := λ(: op String). (: (
   (let r (SCons(
      (close(SAtom '\s\s\slet\scfg\s:=\s\[zero_op\scfg\s"_s))
      (close(SCons(
         (close(SAtom op))
         (close(SAtom '"\]\sin\n_s))
      )))
   )))
   r
) S);

parse-gnu-uop := λ(: op String)(: arg List<String>). (: (
   (let coq-arg (parse-gnu-arg arg))
   (let r (SCons(
      (close(SAtom '\s\s\slet\scfg\s:=\s\[unary_op\scfg\s"_s))
      (close(SCons(
         (close(SAtom op))
         (close(SCons(
            (close(SAtom '"\s_s))
            (close(SCons(
               (close coq-arg)
               (close(SAtom '\]\sin\n_s))
            )))
         )))
      )))
   )))
   r
) S);

parse-gnu-binop := λ(: op String)(: arg List<String>). (: (
   (let coq-arg-1 SNil)
   (let coq-arg-2 SNil)
   (match arg (
      ()
      ( (LCons( a1 (LCons( a2 (LCons( ',_s rst )) )) )) (
         (set coq-arg-1 (parse-gnu-arg (LCons(
            a1
            (close(LCons(
               a2
               (close(: LEOF List<String>))
            )))
         ))))
         (set coq-arg-2 (parse-gnu-arg rst))
      ))
      ( _ (
         (print 'Unexpected\sBinary\sOperation\sSplit\s_s)
         (print arg)
         (exit 1_u64)
      ))
   ))
   (let r (SCons(
      (close(SAtom '\s\s\slet\scfg\s:=\s\[binary_op\scfg\s"_s))
      (close(SCons(
         (close(SAtom op))
         (close(SCons(
            (close(SAtom '"\s_s))
            (close(SCons(
               (close coq-arg-1)
               (close(SCons(
                  (close(SAtom '\s_s))
                  (close(SCons(
                     (close coq-arg-2)
                     (close(SAtom '\]\sin\n_s))
                  )))
               )))
            )))
         )))
      )))
   )))
   r
) S);

parse-gnu-arg := λ(: arg List<String>). (: (
   (let r SNil)
   (match arg (
      ()
      ( (LCons( val LEOF )) (
         (set r (SCons(
            (close(SAtom '\[raw_value\s"_s))
            (close(SCons(
               (close(SAtom val))
               (close(SAtom '"\]_s))
            )))
         )))
      ))
      ( (LCons( '%_s (LCons( rg LEOF )) )) (
         (set r (SCons(
            (close(SAtom '\[register\s"_s))
            (close(SCons(
               (close(SAtom rg))
               (close(SAtom '"\]_s))
            )))
         )))
      ))
      ( (LCons( '$_s (LCons( val LEOF )) )) (
         (set r (SCons(
            (close(SAtom '\[address\s"_s))
            (close(SCons(
               (close(SAtom val))
               (close(SAtom '"\]_s))
            )))
         )))
      ))
      ( (LCons( offset (LCons( '\[_s (LCons( '%_s (LCons( rg (LCons( '\]_s LEOF )) )) )) )) )) (
         (set r (SCons(
            (close(SAtom '\[register_offset\s"_s))
            (close(SCons(
               (close(SAtom offset))
               (close(SCons(
                  (close(SAtom '"\s"_s))
                  (close(SCons(
                     (close(SAtom rg))
                     (close(SAtom '"\]_s))
                  )))
               )))
            )))
         )))
      ))
      ( _ (
         (print 'Unexpected\sArgument\s_s)(print arg)(print '\n_s)
      ))
   ))
   r
) S);