max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
11937 commits 1 branch 0 tags 5.3 GiB
Commit graph

68 commits

Author SHA1 Message Date
Gabriel Ebner
c55579dd69 fix(frontends/lean/scanner): initialize m_pos 2017-03-24 07:04:35 +01:00
Sebastian Ullrich
9d8c84713c refactor(*): reduce exception context info from expr to pos_info 2017-02-17 13:45:57 +01:00
Leonardo de Moura
01414cf21c feat(frontends/lean): add token class, and procedure for consuming the tokens 2017-02-03 18:11:06 -08:00
Sebastian Ullrich
222952d5b8 chore(frontends/lean/scanner): another CLion fix 2017-01-13 07:34:54 -08:00
Leonardo de Moura
df91ae3738 fix(library/string,library/init/data/to_string): handle ASCII control characters 2017-01-11 23:44:33 -08:00
Leonardo de Moura
97dd2f34d5 feat(library,frontends/lean): add basic doc string support 2016-11-25 18:52:56 -08:00
Leonardo de Moura
d59bf05f20 feat(frontends/lean/scanner): allow ' in the beginning of identifiers 2016-11-17 11:53:21 -08:00
Leonardo de Moura
dfd2a23cd4 feat(frontends/lean): use #"c" instead of 'c' for character literals 
The new notation is the same one used in Standard ML.
It will also allow us to use ' in the beginning of identifiers like Standard ML.
 2016-11-17 11:35:54 -08:00
Joe Hendrix
8ceada5555 feat(frontends/lean): support binary, octal and hex literals 
Scanner will interpret numeric literals prefixed with '0b', '0o', and
'0x' as binary, octal, and hex decimal values respectively.  The prefix
character ('b', 'o', 'x') may be upper or lower case.
 2016-10-19 10:13:24 -07:00
Gabriel Ebner
8c188c59c5 feat(frontends/lean): remember column for snapshots 2016-10-13 18:49:10 -07:00
Leonardo de Moura
59ff0eef5c feat(frontends/lean/scanner): hexadecimal numerals 2016-07-19 13:04:27 -04:00
Leonardo de Moura
492c90ed1d feat(frontends/lean/scanner): hex scape in character literal 2016-07-19 12:38:20 -04:00
Leonardo de Moura
3218f91e35 feat(frontends/lean): add support for character literals 2016-07-18 14:07:10 -04:00
Leonardo de Moura
3996f9db4d feat(frontends/lean): add ( token and remove token 2016-06-15 13:22:31 -07:00
Leonardo de Moura
9cbda49297 chore(frontends/lean): remove script blocks 2016-02-11 17:26:44 -08:00
Leonardo de Moura
4821af8685 feat(frontends/lean/scanner): disallow superscripts in identifiers 
See new test for motivating example.
 2016-01-26 18:46:40 -08:00
Sebastian Ullrich
dbfebd5409 feat(frontends/lean/scanner): add more checks to read_quoted_symbol 2015-10-13 09:52:35 -07:00
Leonardo de Moura
c9af007994 chore(frontends/lean): fix style 2015-09-30 17:40:35 -07:00
Sebastian Ullrich
da08079af9 feat(frontends/lean): allow specifying notation spacing via quoted symbols 
Unquoted tokens inherit their spacing from the respective reserved definition.
 2015-09-30 17:36:32 -07:00
Sebastian Ullrich
189a300b11 feat(frontends/lean): improve pretty printing space insertion heuristic 2015-09-30 17:36:32 -07:00
Leonardo de Moura
b9451549d1 feat(frontends/lean): add type notation for referencing hypotheses 2015-07-20 21:43:47 -07:00
Leonardo de Moura
01f8f3c11d fix(frontends/lean): memory access violation 2015-06-14 15:37:45 -07:00
Leonardo de Moura
0502f46f9b fix(frontends/lean/scanner): another bug related to issue #626 2015-05-26 13:39:42 -07:00
Leonardo de Moura
25e41b9b09 fix(frontends/lean/scanner): fixes #626 2015-05-26 11:33:38 -07:00
Leonardo de Moura
cbcaf5a48e fix(frontends/lean/scanner): block comments 
fixes #600
 2015-05-13 22:14:28 -07:00
Leonardo de Moura
033f3b630d feat(frontends/lean/scanner): allow upper-case greek letters in identifiers but Pi and Sigma 2015-03-30 02:14:26 -07:00
Leonardo de Moura
ce889ddf60 feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1' 2014-11-09 12:55:13 -08:00
Leonardo de Moura
469368f090 refactor(frontends/lean/scanner): move basic UTF8 procedures to separate module 2014-10-19 13:29:15 -07:00
Leonardo de Moura
29d6bff785 refactor(frontends/lean): explicit initialization/finalization 2014-09-23 10:00:36 -07:00
Leonardo de Moura
b3e05a2fe9 refactor(frontends/lean/scanner): remove dependency to seekg and unget 
methods

It is not safe to use seekg for textual files. Here is a fragment from a
C++ manual:

seekg() and seekp()

This pair of functions serve respectively to change the position of stream pointers get and put. Both functions are overloaded with two different prototypes:

     seekg ( pos_type position );
     seekp ( pos_type position );

Using this prototype the stream pointer is changed to an absolute position from the beginning of the file. The type required is the same as that returned by functions tellg and tellp.

      seekg ( off_type offset, seekdir direction );
      seekp ( off_type offset, seekdir direction );

Using this prototype, an offset from a concrete point determined by
parameter direction can be specified. It can be:

          ios::beg	offset specified from the beginning of the stream
          ios::cur	offset specified from the current position of the stream pointer
          ios::end	offset specified from the end of the stream

The values of both stream pointers get and put are counted in different
ways for text files than for binary files, since in text mode files some
modifications to the appearance of some special characters can
occur. For that reason it is advisable to use only the first prototype
of seekg and seekp with files opened in text mode and always use
non-modified values returned by tellg or tellp. With binary files, you
can freely use all the implementations for these functions. They should
not have any unexpected behavior.
 2014-09-18 15:24:48 -07:00
Leonardo de Moura
e602c4ba49 feat(frontends/lean): change multicomment to /- ... -/ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 17:55:13 -07:00
Leonardo de Moura
e5a36467dd fix(frontends/lean/scanner): wrong column information produced by scanner 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-13 12:32:37 -07:00
Leonardo de Moura
0276f4c1c0 feat(frontends/lean): store 'overload' information, remove #setline 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-06 19:13:09 -07:00
Leonardo de Moura
8c37a95164 fix(frontends/lean/scanner): typo reported by clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 15:24:04 -07:00
Leonardo de Moura
a62e6f84e3 feat(frontends/lean/scanner): allow letter-like unicode characters and sub/super-scripts in identifiers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-02 00:47:58 -07:00
Leonardo de Moura
df57043861 fix(frontends/lean/scanner): decode utf8 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-01 19:58:02 -07:00
Leonardo de Moura
e7019ec840 feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 22:13:25 -07:00
Leonardo de Moura
282a35bd1b feat(frontends/lean): add '#setline' directive 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 07:28:56 -07:00
Leonardo de Moura
3dc26666b9 feat(frontends/lean): add parser interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 18:20:59 -07:00
Leonardo de Moura
d3e3301208 refactor(frontends/lean/scanner): use the parser configuration in the environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 10:59:12 -07:00
Leonardo de Moura
546f9dc00b chore(frontends/lean): use consistent name conventions, rename token_set to token_table 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-10 09:18:57 -07:00
Leonardo de Moura
d10d70423a feat(frontends/lean): add new scanner 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-05 18:57:26 -07:00
Leonardo de Moura
c6af56260e refactor(frontends/lean): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 15:51:41 -07:00
Leonardo de Moura
a2d2e36f04 refactor(frontends/lean): remove notation for creating tuples 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-10 09:03:42 -08:00
Leonardo de Moura
ad7b13104f feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-07 15:03:16 -08:00
Leonardo de Moura
ba9a8f9d98 feat(frontends/lean): add 'show' expression syntax sugar 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-06 07:50:22 -08:00
Leonardo de Moura
4fcc292332 feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 22:10:01 -08:00
Leonardo de Moura
5e5ab1429d feat(frontends/lean): parse and pretty print sigma types 
This commit also fixes some bugs in the implementation of Sigma types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-03 18:16:00 -08:00
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-16 17:39:12 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-09 11:01:27 -08:00