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

478 commits

Author SHA1 Message Date
Leonardo de Moura
3fe5cf1528 chore(library/init/core): remove another weirdness: the bs at bnot, band and bor 2019-03-22 12:57:31 -07:00
Leonardo de Moura
e1ea2b3948 chore(library/init): fix names and add HasEmptyc instances 2019-03-22 12:38:22 -07:00
Leonardo de Moura
87b066b87e refactor(library/init): move function.lean definitions to core.lean 2019-03-22 09:33:10 -07:00
Leonardo de Moura
e31c3fde56 chore(library/init): remove dead code, lemma => theorem 2019-03-22 09:27:30 -07:00
Leonardo de Moura
46cb2436d8 chore(library/init/core): remove dead code, and naming convention 2019-03-22 09:19:28 -07:00
Leonardo de Moura
7552b2e1e4 chore(library/init/data/list/basic): mem => Mem 2019-03-22 09:10:21 -07:00
Leonardo de Moura
452d5107ac chore(library/init/data/array): naming convention 
The array read and write operations are now called:

- "Comfortable" version (with runtime bound checks):
  `Array.get` and `Array.set` like OCaml.
   It is also consistent with `Ref.get` and `Ref.put`,
   and `get` and `set` for `MonadState`.

- `Fin` version (without runtime bound checks):
  `Array.index` and `Array.update` like in F*.

- `USize` version (without runtime bound checks and unboxing):
  `Array.idx` and `Array.updt`.

cc @kha
 2019-03-21 18:03:29 -07:00
Leonardo de Moura
4a08d6715a chore(library/init/data/array): add HasEmptyc instance 2019-03-21 17:06:56 -07:00
Leonardo de Moura
91204a52d6 chore(library/init/data/dlist): Dlist => DList 2019-03-21 17:03:22 -07:00
Leonardo de Moura
3befc219c9 chore(library/init): Empty => empty when it is a function 2019-03-21 17:03:15 -07:00
Leonardo de Moura
0a326c666f chore(library/init/data/list/basic): use Bool instead of Prop 2019-03-21 16:24:38 -07:00
Sebastian Ullrich
7615c9f92f chore(library/init/core): style review of the first half 2019-03-21 15:06:45 -07:00
Sebastian Ullrich
d5ec4a4606 chore(frontends/lean/pp): ppAnonymousCtor -> ppAsAnonymousCtor 2019-03-21 15:06:45 -07:00
Sebastian Ullrich
b9edaf888f chore(library/init/core): ne -> Ne, not -> Not 2019-03-21 15:06:45 -07:00
Sebastian Ullrich
97e5aa2411 chore(library): s/Punit/PUnit/g etc 2019-03-21 15:06:45 -07:00
Leonardo de Moura
1fe3f14ad0 chore(*): Uint => UInt, Usize => USize 2019-03-21 15:06:44 -07:00
Leonardo de Moura
79a8d9aa65 chore(*): decidablePred/decidableRel => DecidablePred/DecidableRel 2019-03-21 15:06:44 -07:00
Leonardo de Moura
0b5862b6ce chore(*): and => And 2019-03-21 15:06:44 -07:00
Leonardo de Moura
4c50859129 chore(*): or => Or 2019-03-21 15:06:44 -07:00
Leonardo de Moura
2be87ecd92 chore(library/init): Bool.tt => Bool.true and Bool.ff => Bool.false 2019-03-21 15:06:44 -07:00
Leonardo de Moura
f8113a01eb chore(library): unit => Unit 2019-03-21 15:06:44 -07:00
Leonardo de Moura
62e6341014 chore(*): lowercase file names 2019-03-21 15:06:44 -07:00
Leonardo de Moura
2ea0baeb99 chore(library): use lowercase in imports 2019-03-21 15:06:44 -07:00
Leonardo de Moura
ac27bd092b chore(*): small fixes 2019-03-21 15:06:44 -07:00
Leonardo de Moura
675003318e chore(*): small fixes 2019-03-21 15:06:44 -07:00
Leonardo de Moura
67fb78bb47 chore(*): renaming files 2019-03-21 15:06:44 -07:00
Sebastian Ullrich
beda5f5f43 chore(library): capitalize types and namespaces 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
f7aeeaf237 exclude export/extern, translate constants.txt 2019-03-21 15:06:43 -07:00
Sebastian Ullrich
b939162168 chore(library): switch from snake_case to camelCase 2019-03-21 15:06:43 -07:00
Leonardo de Moura
0b7d987699 feat(frontends/lean, library/init/lean): opaque constants 
@kha I have added support for opaque constants to the old C++ frontend,
and made sure the new frontend can still parse `library/init/core.lean`.
The kernel should enforce that opaque constants are really opaque, and
the following example should fail
```
constant x : nat := 0
theorem foo : x = 0 := rfl
```
If it doesn't, it is a bug.

Here are some remaining issues:
1- `environment.mk_empty` is currently an axiom because we cannot create
an inhabitant of an opaque type. A possible solution is to use
`option environment` instead of `environment`.

2- There is no support for opaque constants in the new
frontend. However, I modified it to handle axioms, and fixed the literal
values with decl_cmd_kind. I tried to mark some of my changes with
comments, but it is probably much easier for you to just check the
commit change list.

3- I did not add any support for automatically constructing `e`
at `constant x : t := e`. I think we can do this later
after we replace the old frontend with the new one. BTW, it took only a
few minutes to provide the inhabitants manually.
 2019-03-15 17:41:44 -07:00
Leonardo de Moura
ecdb9d6df0 feat(library/init, frontends/lean): add abbreviation for abbreviation 2019-03-15 16:01:25 -07:00
Leonardo de Moura
68ebc2a5c5 feat(library/init/data/string/basic): implement iterators using uft8 low level API 2019-03-12 06:56:05 -07:00
Leonardo de Moura
cf3bbd7e25 feat(runtime): add utf8_prev and utf8_set 
Next goal: implement string.iterator in Lean
 2019-03-11 18:05:40 -07:00
Leonardo de Moura
4ca9c6f22e feat(runtime): add efficient fixpoint implementation 2019-03-10 10:09:57 -07:00
Leonardo de Moura
c862ce4a75 feat(runtime, library/init/data/string/basic): add utf8_pos 
`utf8_pos` is a low level alternative for `string.iterator`.
TODO: implement `string.iterator` using it.
 2019-03-09 12:30:19 -08:00
Leonardo de Moura
2c3cfcf1dd feat(library/init/data/char/basic): add char.utf8_size 2019-03-09 10:46:29 -08:00
Leonardo de Moura
402034df1f chore(library/init/data): move usize to uint 2019-03-09 10:32:23 -08:00
Leonardo de Moura
2032b10482 feat(library/init/data): bitwise operations 2019-03-09 10:19:35 -08:00
Leonardo de Moura
6d7411cc07 perf(library/init/data/option/basic): missing [inline] 2019-03-06 10:58:12 -08:00
Leonardo de Moura
778e7e41f9 refactor(library/init/data/rbmap/basic): pass ins node-cell to balance1 and balance2. 
The idea is to reuse the cell. The trick is like the one we used for
improving state_t. It seems to work pretty well. Now, the Lean
version is 29% slower than the C++ one.

cc @kha
 2019-02-20 18:27:58 -08:00
Leonardo de Moura
835718955f refactor(library/init/data/rbmap/basic): store color in the node 
@kha Now the Lean version is approx. 50% slower than the C++ version.
 2019-02-20 17:52:03 -08:00
Leonardo de Moura
9e0b28d8ce feat(library/init/data/array/basic): improve 2019-02-16 16:08:10 -08:00
Leonardo de Moura
3c73c43ab2 feat(runtime,library/init/data/array/basic): add builtin support for arrays 2019-02-16 15:27:23 -08:00
Leonardo de Moura
c855094ecb feat(library/init/data/char/basic): mark char.of_nat as noinline 2019-02-16 10:45:52 -08:00
Leonardo de Moura
61274c7d35 feat(library/init/data/char): use uint32 instead of nat for defining char 2019-02-15 18:07:55 -08:00
Leonardo de Moura
542bd432f8 test(tests/compiler): uint constant folding tests 2019-02-15 14:53:29 -08:00
Leonardo de Moura
456ed23cc2 feat(library/init): use extern when declarating nat primitives 2019-02-12 18:12:29 -08:00
Leonardo de Moura
52db59eb87 fix(library/init/data/int/basic): nasty bug at int.repr 2019-02-12 15:58:59 -08:00
Leonardo de Moura
425a4b70d1 feat(library/init/data/int/basic): use extern attribute, and fix div/mod mess 
Now, int.div and int.mod behave like C++ `/` and `%` for int,
moreover, they satisfy

          (a/b)*b + (a%b) = a
 2019-02-12 11:41:46 -08:00
Leonardo de Moura
6be47dfb97 feat(library/init/data/string/basic): use extern attribute 2019-02-11 17:54:24 -08:00