refactor(frontends/lean): add script for automatically generating tokens.h and tokens.cpp

script/gen_tokens_cpp.py

@@ -0,0 +1,88 @@
+#!/usr/bin/env python
+# -*- coding: utf-8 -*-
+#
+# Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
+#
+# Author: Leonardo de Moura
+#
+# Given a text file containing id and token strings,
+# this script generates .h and .cpp files for initialing/finalizing theses tokens
+# as C++ name objects.
+#
+# This script is used to generate src/frontends/lean/tokens.cpp and src/frontends/lean/tokens.h
+# from src/frontends/lean/tokens.txt
+import sys
+import os
+
+def error(msg):
+    print("Error: %s" % msg)
+    exit(1)
+
+def to_c_const(s):
+    out = ""
+    for c in s:
+        if c == '.' or c == '_':
+            out += '_'
+        elif c.isalpha() or c.isdigit():
+            out += c
+        else:
+            error("unsupported character in constant: %s" % s)
+    return out
+
+def main(argv=None):
+    if argv is None:
+        argv = sys.argv[1:]
+    infile        = argv[0]
+    basename, ext = os.path.splitext(infile)
+    cppfile       = basename + ".cpp"
+    hfile         = basename + ".h"
+    constants     = []
+    with open(infile, 'r') as f:
+        for line in f:
+            l = line.split()
+            if len(l) != 2:
+                error("invalid line: %s" % line)
+            constants.append([to_c_const(l[0].strip()), l[1].strip()])
+    with open(hfile, 'w') as f:
+        f.write('// Copyright (c) 2015 Microsoft Corporation. All rights reserved.\n')
+        f.write('// Released under Apache 2.0 license as described in the file LICENSE.\n')
+        f.write('// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n')
+        f.write('#include "util/name.h"\n')
+        f.write('namespace lean {\n')
+        f.write('void initialize_tokens();\n')
+        f.write('void finalize_tokens();\n')
+        for c in constants:
+            f.write('name const & get_%s_tk();\n' % c[0])
+        f.write('}\n')
+    with open(cppfile, 'w') as f:
+        f.write('// Copyright (c) 2015 Microsoft Corporation. All rights reserved.\n')
+        f.write('// Released under Apache 2.0 license as described in the file LICENSE.\n')
+        f.write('// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n')
+        f.write('#include "util/name.h"\n')
+        f.write('namespace lean{\n')
+        # declare constants
+        for c in constants:
+            f.write('name const * g_%s_tk = nullptr;\n' % c[0])
+        # initialize constants
+        f.write('void initialize_tokens() {\n')
+        for c in constants:
+            f.write('    g_%s_tk = new name{' % c[0])
+            f.write('"%s"' % c[1])
+            f.write('};\n')
+        f.write('}\n')
+        # finalize constants
+        f.write('void finalize_tokens() {\n')
+        for c in constants:
+            f.write('    delete g_%s_tk;\n' % c[0])
+        f.write('}\n')
+        # get methods
+        for c in constants:
+            f.write('name const & get_%s_tk() { return *g_%s_tk; }\n' % (c[0], c[0]))
+        # end namespace
+        f.write('}\n')
+    print("done")
+    return 0
+
+if __name__ == "__main__":
+    sys.exit(main())

src/frontends/lean/tokens.h

@@ -1,11 +1,7 @@
-/*
+// Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+// Released under Apache 2.0 license as described in the file LICENSE.
-Released under Apache 2.0 license as described in the file LICENSE.
+// DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py
-
-Author: Leonardo de Moura
-*/
 #include "util/name.h"
-
 namespace lean {
 void initialize_tokens();
 void finalize_tokens();
@@ -35,13 +31,13 @@ name const & get_bar_tk();
 name const & get_comma_tk();
 name const & get_add_tk();
 name const & get_sub_tk();
+name const & get_greater_tk();
 name const & get_question_tk();
 name const & get_question_lp_tk();
 name const & get_bang_tk();
 name const & get_slash_tk();
-name const & get_star_tk();
 name const & get_plus_tk();
-name const & get_greater_tk();
+name const & get_star_tk();
 name const & get_turnstile_tk();
 name const & get_explicit_tk();
 name const & get_max_tk();
@@ -88,9 +84,9 @@ name const & get_else_tk();
 name const & get_by_tk();
 name const & get_rewrite_tk();
 name const & get_proof_tk();
+name const & get_qed_tk();
 name const & get_begin_tk();
 name const & get_begin_plus_tk();
-name const & get_qed_tk();
 name const & get_end_tk();
 name const & get_private_tk();
 name const & get_definition_tk();
@@ -109,14 +105,19 @@ name const & get_unfold_f_tk();
 name const & get_constructor_tk();
 name const & get_coercion_tk();
 name const & get_reducible_tk();
-name const & get_semireducible_tk();
 name const & get_quasireducible_tk();
+name const & get_semireducible_tk();
 name const & get_irreducible_tk();
-name const & get_multiple_instances_tk();
-name const & get_attribute_tk();
 name const & get_parsing_only_tk();
-name const & get_class_tk();
+name const & get_symm_tk();
+name const & get_trans_tk();
+name const & get_refl_tk();
+name const & get_subst_tk();
+name const & get_recursor_tk();
+name const & get_attribute_tk();
 name const & get_with_tk();
+name const & get_class_tk();
+name const & get_multiple_instances_tk();
 name const & get_prev_tk();
 name const & get_scoped_tk();
 name const & get_foldr_tk();
@@ -136,9 +137,4 @@ name const & get_fields_tk();
 name const & get_trust_tk();
 name const & get_metaclasses_tk();
 name const & get_inductive_tk();
-name const & get_symm_tk();
-name const & get_trans_tk();
-name const & get_refl_tk();
-name const & get_subst_tk();
-name const & get_recursor_tk();
 }

src/frontends/lean/tokens.txt

@@ -0,0 +1,132 @@
+period       .
+placeholder  _
+colon        :
+semicolon    ;
+dcolon       ::
+lparen       (
+rparen       )
+llevel_curly .{
+lcurly       {
+rcurly       }
+ldcurly      ⦃
+rdcurly      ⦄
+lcurlybar    {|
+rcurlybar    |}
+lbracket     [
+rbracket     ]
+langle       ⟨
+rangle       ⟩
+triangle     ▸
+caret        ^
+up           ↑
+down         <d
+bar          |
+comma        ,
+add          +
+sub          -
+greater      >
+question     ?
+question_lp  ?(
+bang         !
+slash        /
+plus         +
+star         *
+turnstile    ⊢
+explicit     @
+max          max
+imax         imax
+cup          \u2294
+import       import
+prelude      prelude
+show         show
+have         have
+assert       assert
+assume       assume
+take         take
+fun          fun
+match        match
+ellipsis     ...
+raw          raw
+true         true
+false        false
+options      options
+commands     commands
+instances    instances
+classes      classes
+coercions    coercions
+arrow        ->
+declarations declarations
+decls        decls
+hiding       hiding
+exposing     exposing
+renaming     renaming
+replacing    replacing
+extends      extends
+as           as
+none         [none]
+whnf         [whnf]
+wf           [wf]
+in           in
+at           at
+assign       :=
+visible      [visible]
+from         from
+using        using
+then         then
+else         else
+by           by
+rewrite      rewrite
+proof        proof
+qed          qed
+begin        begin
+begin_plus   begin+
+end          end
+private      private
+definition   definition
+theorem      theorem
+abbreviation abbreviation
+axiom        axiom
+axioms       axioms
+constant     constant
+constants    constants
+variable     variable
+variables    variables
+instance     [instance]
+priority     [priority
+unfold_c     [unfold-c
+unfold_f     [unfold-f]
+constructor  [constructor]
+coercion     [coercion]
+reducible    [reducible]
+quasireducible [quasireducible]
+semireducible [semireducible]
+irreducible  [irreducible]
+parsing_only [parsing-only]
+symm         [symm]
+trans        [trans]
+refl         [refl]
+subst        [subst]
+recursor     [recursor]
+attribute    attribute
+with         with
+class        [class]
+multiple_instances [multiple-instances]
+prev         prev
+scoped       scoped
+foldr        foldr
+foldl        foldl
+binder       binder
+binders      binders
+infix        infix
+infixl       infixl
+infixr       infixr
+postfix      postfix
+prefix       prefix
+notation     notation
+call         call
+persistent   [persistent]
+root         _root_
+fields       fields
+trust        trust
+metaclasses  metaclasses
+inductive    inductive