First checked-in version.

2 files changed, 143 insertions, 0 deletions

diff --git a/coqtags b/coqtags
new file mode 100644
index 00000000..b6c72c78
--- /dev/null
+++ b/coqtags
@@ -0,0 +1,56 @@
+#!/usr/local/bin/perl4
+$/=0777;
+
+if($#ARGV<$[) {die "No Files\n";}
+open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n";
+
+while(<>)	
+{ 
+  print "Tagging $ARGV\n";
+  $a=$_;
+  $cp=1;
+  $lp=1;
+  $tagstring="";
+
+  while(1) 
+  { 
+
+#   ---- Get the next statement starting on a newline ---- 
+
+    if($a=~/^[ \t\n]*\(\*/)
+    { while($a=~/^\s*\(\*/) 
+      { $d=1; $a=$'; $cp+=length $&; $lp+=($&=~tr/\n/\n/);
+        while($d>0 && $a=~/\(\*|\*\)/)
+        { $a=$'; $cp+=2+length $`; $lp+=($`=~tr/\n/\n/);
+          if($& eq "(*") {$d++} else {$d--};
+        }
+        if($d!=0) {die "Unbalanced Comment?";}
+      }
+    }
+
+    if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;}
+    while($a=~/^\n/) {$cp++;$lp++;$a=$'}
+
+    if($a=~/^[^\.]*\./) 
+    { $stmt=$&; $newa=$'; $newcp=$cp+length $&; $newlp=$lp+($&=~tr/\n/\n/); }
+    else { last;}
+
+# ---- The above embarrasses itself if there are semicolons inside comments 
+# ---- inside commands. Could do better.
+
+#  print "----- (",$lp,",",$cp,")\n", $stmt, "\n";
+
+    if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/)
+       { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; }
+
+    elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+([\w\']+))\s*:/)
+       { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; }
+
+    elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/)
+       { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; }
+
+    $cp=$newcp; $lp=$newlp; $a=$newa;
+  }  
+  print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring;
+}
+close tagfile;
diff --git a/legotags b/legotags
new file mode 100644
index 00000000..a3c13eab
--- /dev/null
+++ b/legotags
@@ -0,0 +1,87 @@
+#!/usr/local/bin/perl
+
+undef $/;
+
+if($#ARGV<$[) {die "No Files\n";}
+open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n";
+
+while(<>)	
+{ 
+  print "Tagging $ARGV\n";
+  $a=$_;
+  $cp=1;
+  $lp=1;
+  $tagstring="";
+
+  while(1) 
+  { 
+
+#   ---- Get the next statement starting on a newline ---- 
+
+    if($a=~/^[ \t\n]*\(\*/)
+    { while($a=~/^\s*\(\*/) 
+      { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/);
+        while($d>0 && $a=~/\(\*|\*\)/)
+        { $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/);
+          if($& eq "(*") {$d++} else {$d--};
+        }
+        if($d!=0) {die "Unbalanced Comment?";}
+      }
+    }
+
+    if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;}
+    while($a=~/^\n/) {$cp++;$lp++;$a=$'}
+
+    if($a=~/^[^;]*;/) 
+    { $stmt=$&; 
+      $newa=$'; 
+      $newcp=$cp+length $&; 
+      $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); }
+    else { last;}
+
+# ---- The above embarrasses itself if there are semicolons inside comments 
+# ---- inside commands. Could do better.
+
+#  print "----- (",$lp,",",$cp,")\n", $stmt, "\n";
+
+    if($stmt=~/^([ \t]*\$?Goal\s*([\w\']+))\s*:/)
+       { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
+
+    elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/)
+       { do adddecs($stmt,$1) }
+
+    elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/)
+       { do adddecs($stmt,$1) }
+
+# ---- we don't need to tag saves: all goals should be named!
+
+#    elsif($stmt=~/([ \t]*\$?Save\s+([\w\']+))/)
+#       { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
+#
+#    elsif($stmt=~/^([ \t]*\$?SaveUnfrozen\s+([\w\']+))/)
+#       { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
+
+#   ---- Maybe do something smart with discharge as well?
+
+    $cp=$newcp; $lp=$newlp; $a=$newa;
+  }  
+  print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring;
+}
+close tagfile;
+
+
+sub adddecs {
+  $wk=$_[0];
+  $tag=$_[1];
+  while($wk=~/\[\s*([\w\']+)/)
+  { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$';
+    while($wk=~/^\s*,\s*([\w\']+)/)
+    { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; }
+    $d=1;
+    while($d>0 && $wk=~/\[|\]/)
+    { $wk=$'; if($& eq "[") {$d++} else {$d--};
+    }
+  }
+  0;
+}
+