#! /usr/bin/perl -w

#   Copyright (C) 1999, 2000, 2001 Free Software Foundation, Inc.

# This file is part of GNU CC.

# GNU CC is free software; you can redistribute it and/or modify
# it under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2, or (at your option)
# any later version.

# GNU CC is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
# GNU General Public License for more details.

# You should have received a copy of the GNU General Public License
# along with GNU CC; see the file COPYING.  If not, write to
# the Free Software Foundation, 59 Temple Place - Suite 330,
# Boston MA 02111-1307, USA.

# This does trivial (and I mean _trivial_) conversion of Texinfo
# markup to Perl POD format.  It's intended to be used to extract
# something suitable for a manpage from a Texinfo document.

$output = 0;
$skipping = 0;
%sects = ();
$section = "";
@icstack = ();
@endwstack = ();
@skstack = ();
@instack = ();
$shift = "";
%defs = ();
$fnno = 1;
$inf = "";
$ibase = "";

while ($_ = shift) {
    if (/^-D(.*)$/) {
	if ($1 ne "") {
	    $flag = $1;
	} else {
	    $flag = shift;
	}
	$value = "";
	($flag, $value) = ($flag =~ /^([^=]+)(?:=(.+))?/);
	die "no flag specified for -D\n"
	    unless $flag ne "";
	die "flags may only contain letters, digits, hyphens, dashes and underscores\n"
	    unless $flag =~ /^[a-zA-Z0-9_-]+$/;
	$defs{$flag} = $value;
    } elsif (/^-/) {
	usage();
    } else {
	$in = $_, next unless defined $in;
	$out = $_, next unless defined $out;
	usage();
    }
}

if (defined $in) {
    $inf = gensym();
    open($inf, "<$in") or die "opening \"$in\": $!\n";
    $ibase = $1 if $in =~ m|^(.+)/[^/]+$|;
} else {
    $inf = \*STDIN;
}

if (defined $out) {
    open(STDOUT, ">$out") or die "opening \"$out\": $!\n";
}

while(defined $inf) {
while(<$inf>) {
    # Certain commands are discarded without further processing.
    /^\@(?:
	 [a-z]+index		# @*index: useful only in complete manual
	 |need			# @need: useful only in printed manual
	 |(?:end\s+)?group	# @group .. @end group: ditto
	 |page			# @page: ditto
	 |node			# @node: useful only in .info file
	 |(?:end\s+)?ifnottex   # @ifnottex .. @end ifnottex: use contents
	)\b/x and next;

    chomp;

    # Look for filename and title markers.
    /^\@setfilename\s+([^.]+)/ and $fn = $1, next;
    /^\@settitle\s+([^.]+)/ and $tl = postprocess($1), next;

    # Identify a man title but keep only the one we are interested in.
    /^\@c\s+man\s+title\s+([A-Za-z0-9-]+)\s+(.+)/ and do {
	if (exists $defs{$1}) {
	    $fn = $1;
	    $tl = postprocess($2);
	}
	next;
    };

    # Look for blocks surrounded by @c man begin SECTION ... @c man end.
    # This really oughta be @ifman ... @end ifman and the like, but such
    # would require rev'ing all other Texinfo translators.
    /^\@c\s+man\s+begin\s+([A-Z]+)\s+([A-Za-z0-9-]+)/ and do {
	$output = 1 if exists $defs{$2};
        $sect = $1;
	next;
    };
    /^\@c\s+man\s+begin\s+([A-Z]+)/ and $sect = $1, $output = 1, next;
    /^\@c\s+man\s+end/ and do {
	$sects{$sect} = "" unless exists $sects{$sect};
	$sects{$sect} .= postprocess($section);
	$section = "";
	$output = 0;
	next;
    };

    # handle variables
    /^\@set\s+([a-zA-Z0-9_-]+)\s*(.*)$/ and do {
	$defs{$1} = $2;
	next;
    };
    /^\@clear\s+([a-zA-Z0-9_-]+)/ and do {
	de<style>pre { line-height: 125%; margin: 0; }
td.linenos pre { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
span.linenos { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
td.linenos pre.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
span.linenos.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
.highlight .hll { background-color: #ffffcc }
.highlight { background: #ffffff; }
.highlight .c { color: #888888 } /* Comment */
.highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */
.highlight .k { color: #008800; font-weight: bold } /* Keyword */
.highlight .ch { color: #888888 } /* Comment.Hashbang */
.highlight .cm { color: #888888 } /* Comment.Multiline */
.highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */
.highlight .cpf { color: #888888 } /* Comment.PreprocFile */
.highlight .c1 { color: #888888 } /* Comment.Single */
.highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */
.highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .gr { color: #aa0000 } /* Generic.Error */
.highlight .gh { color: #333333 } /* Generic.Heading */
.highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */
.highlight .go { color: #888888 } /* Generic.Output */
.highlight .gp { color: #555555 } /* Generic.Prompt */
.highlight .gs { font-weight: bold } /* Generic.Strong */
.highlight .gu { color: #666666 } /* Generic.Subheading */
.highlight .gt { color: #aa0000 } /* Generic.Traceback */
.highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: #008800 } /* Keyword.Pseudo */
.highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */
.highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */
.highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */
.highlight .na { color: #336699 } /* Name.Attribute */
.highlight .nb { color: #003388 } /* Name.Builtin */
.highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */
.highlight .no { color: #003366; font-weight: bold } /* Name.Constant */
.highlight .nd { color: #555555 } /* Name.Decorator */
.highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */
.highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */
.highlight .nl { color: #336699; font-style: italic } /* Name.Label */
.highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */
.highlight .py { color: #336699; font-weight: bold } /* Name.Property */
.highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */
.highlight .nv { color: #336699 } /* Name.Variable */
.highlight .ow { color: #008800 } /* Operator.Word */
.highlight .w { color: #bbbbbb } /* Text.Whitespace */
.highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */
.highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */
.highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */
.highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */
.highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */
.highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */
.highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */
.highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */
.highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */
.highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */
.highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */
.highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */
.highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */
.highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */
.highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */
.highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */
.highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */
.highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */
.highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */
.highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */
.highlight .vc { color: #336699 } /* Name.Variable.Class */
.highlight .vg { color: #dd7700 } /* Name.Variable.Global */
.highlight .vi { color: #3333bb } /* Name.Variable.Instance */
.highlight .vm { color: #336699 } /* Name.Variable.Magic */
.highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */</style><div class="highlight"><pre><span></span><span class="ch">#!/bin/bash</span>
<span class="nb">set</span> -ex
yosys -p <span class="s1">&#39;</span>
<span class="s1">	read_verilog -formal demo.v</span>
<span class="s1">	prep -flatten -nordff -top demo</span>
<span class="s1">	write_smt2 -wires demo.smt2</span>
<span class="s1">	flatten demo; delete -output</span>
<span class="s1">	memory_map; opt -full</span>
<span class="s1">	techmap; opt -fast</span>
<span class="s1">	abc -fast -g AND; opt_clean</span>
<span class="s1">	write_aiger -map demo.aim demo.aig</span>
<span class="s1">&#39;</span>
super_prove demo.aig &gt; demo.aiw
yosys-smtbmc --dump-vcd demo.vcd --aig demo demo.smt2
</pre></div>
</code></pre></td></tr></table>
</div> <!-- class=content -->
<div class='footer'>generated by <a href='https://git.zx2c4.com/cgit/about/'>cgit v1.2.3</a> (<a href='https://git-scm.com/'>git 2.25.1</a>) at 2025-08-30 09:18:45 +0000</div>
</div> <!-- id=cgit -->
</body>
</html>
ef\{([^\},]*),([^\},]*),([^\},]*)\}/$3/g;

    # Turn B<blah I<blah> blah> into B<blah> I<blah> B<blah> to
    # match Texinfo semantics of @emph inside @samp.  Also handle @r
    # inside bold.
    s/&LT;/</g;
    s/&GT;/>/g;
    1 while s/B<((?:[^<>]|I<[^<>]*>)*)R<([^>]*)>/B<$1>${2}B</g;
    1 while (s/B<([^<>]*)I<([^>]+)>/B<$1>I<$2>B</g);
    1 while (s/I<([^<>]*)B<([^>]+)>/I<$1>B<$2>I</g);
    s/[BI]<>//g;
    s/([BI])<(\s+)([^>]+)>/$2$1<$3>/g;
    s/([BI])<([^>]+?)(\s+)>/$1<$2>$3/g;

    # Extract footnotes.  This has to be done after all other
    # processing because otherwise the regexp will choke on formatting
    # inside @footnote.
    while (/\@footnote/g) {
	s/\@footnote\{([^\}]+)\}/[$fnno]/;
	add_footnote($1, $fnno);
	$fnno++;
    }

    return $_;
}

sub unmunge
{
    # Replace escaped symbols with their equivalents.
    local $_ = $_[0];

    s/&lt;/E<lt>/g;
    s/&gt;/E<gt>/g;
    s/&lbrace;/\{/g;
    s/&rbrace;/\}/g;
    s/&at;/\@/g;
    s/&amp;/&/g;
    return $_;
}

sub add_footnote
{
    unless (exists $sects{FOOTNOTES}) {
	$sects{FOOTNOTES} = "\n=over 4\n\n";
    }

    $sects{FOOTNOTES} .= "=item $fnno.\n\n"; $fnno++;
    $sects{FOOTNOTES} .= $_[0];
    $sects{FOOTNOTES} .= "\n\n";
}

# stolen from Symbol.pm
{
    my $genseq = 0;
    sub gensym
    {
	my $name = "GEN" . $genseq++;
	my $ref = \*{$name};
	delete $::{$name};
	return $ref;
    }
}