Leonardo de Moura
cca90b5f9f
chore: simplify withPtrEqDecEq
2020-02-27 11:45:02 -08:00
Leonardo de Moura
b83691baa2
feat: compute fvarSubst
2020-02-27 10:58:46 -08:00
Leonardo de Moura
021d906542
fix: remove filler fields (part 2)
2020-02-27 10:02:26 -08:00
Leonardo de Moura
966e5bc60d
perf: remove "filler" fields
...
See previous commit.
2020-02-27 10:02:26 -08:00
Leonardo de Moura
e5d824a748
feat: initialize last word
...
Motivation: trying to get rid of explicit "filler" fields because
they slow down modules such as `RBMap`.
2020-02-27 10:02:26 -08:00
Leonardo de Moura
2719eaeb63
fix: closes #119
2020-02-27 08:10:29 -08:00
Leonardo de Moura
657f3792b1
feat: maxsharing scalar arrays
2020-02-25 18:08:49 -08:00
Leonardo de Moura
131f2d202e
chore: ignore closures at maxsharing
...
Closures may capture huge objects that user may be unaware.
For example, any closure created by the interpreter contains
a reference to the `Environment`.
@dselsam @kha I don't see many applications for maximizing sharing in
values captured by closures. If we want this feature, we should at
least wrap the `Environment` and `Decl` using external objects
at `mk_stub_closure` at `ir_interpreter.cpp`.
2020-02-25 17:13:05 -08:00
Leonardo de Moura
1653e75b6b
feat: maxsharing for arrays and strings
2020-02-25 16:15:26 -08:00
Leonardo de Moura
46e8d193ca
feat: maxsharing for constructors
2020-02-25 15:43:10 -08:00
Leonardo de Moura
53b57af125
fix: dangling file
2020-02-25 14:33:54 -08:00
Leonardo de Moura
cfd7fc8a87
fix: message::get_text
...
It was still using the old representation.
2020-02-25 14:20:55 -08:00
Leonardo de Moura
1fb7a3a208
fix: position of first Bool field
2020-02-25 14:05:53 -08:00
Leonardo de Moura
9095f3caa0
chore: update stage0
2020-02-25 13:53:08 -08:00
Leonardo de Moura
7e96380711
chore: remove unnecessary import
2020-02-25 13:49:26 -08:00
Leonardo de Moura
7496296c1e
fix: "filler" fields
2020-02-25 13:49:18 -08:00
Leonardo de Moura
6a19069021
feat: add "filler" fields
2020-02-25 13:49:11 -08:00
Leonardo de Moura
1305824b03
chore: add get_bool_field helper function
...
Motivation: help us to adjust the code when we modify the position of
scalar fields.
2020-02-25 13:43:06 -08:00
Leonardo de Moura
d8ed4165b0
chore: remove cnstr_get_scalar and cnstr_set_scalar
2020-02-25 13:28:23 -08:00
Leonardo de Moura
16d88b04ea
chore: avoid cnstr_set_scalar and cnstr_get_scalar
2020-02-25 13:27:30 -08:00
Leonardo de Moura
6ada62a3ee
feat: export helper functions
...
Motivation: prevent changes in the scalar fields layout from breaking
C++ code.
Ideally, we should do that for all constructors, and implement a tool
that creates the C++ functions automatically for us.
We don't do it because we will delete most of this code after we
finish the Lean4 transition.
2020-02-25 13:00:22 -08:00
Leonardo de Moura
74d08e47e5
chore: style
2020-02-24 21:04:48 -08:00
Leonardo de Moura
dae1a3172e
fix: maxsharing hash and eq, and expand skeleton
2020-02-24 21:00:01 -08:00
Leonardo de Moura
fdc76934f5
feat: max_sharing_fn skeleton
2020-02-24 19:50:37 -08:00
Leonardo de Moura
191bfcddc1
chore: remove #exit
2020-02-24 19:32:57 -08:00
Leonardo de Moura
f84e1c2fbd
feat: add dummy implementation of MaxSharing primitives
2020-02-24 19:30:53 -08:00
Leonardo de Moura
46fd5ed929
feat: maxSharing primitives
2020-02-24 19:23:45 -08:00
Leonardo de Moura
0781c74754
chore: variable order consistency
2020-02-24 18:29:24 -08:00
Leonardo de Moura
370dada9a3
feat: add findEntry? functions
2020-02-24 15:47:59 -08:00
Leonardo de Moura
d6a7e9a308
chore: remove mutquot primitives
2020-02-24 14:28:32 -08:00
Leonardo de Moura
a68249393a
chore: minimize dependencies
2020-02-24 13:18:07 -08:00
Leonardo de Moura
55e21e13cf
chore: remove broken MutQuot
...
`MutQuot.mk` primitive is affected by the polymorphic reference issue.
2020-02-24 13:03:16 -08:00
Leonardo de Moura
605edd05ae
feat: handle alternatives
2020-02-23 19:29:54 -08:00
Leonardo de Moura
7602cea77d
fix: add missing file
2020-02-23 19:29:42 -08:00
Leonardo de Moura
b9dc76df35
feat: name minor premises using ctor names
2020-02-23 18:45:53 -08:00
Leonardo de Moura
a1303a6515
feat: use focusAux, and return new subgoals
2020-02-23 17:50:06 -08:00
Leonardo de Moura
d2801782de
fix: missing headBeta
2020-02-23 17:47:28 -08:00
Leonardo de Moura
6c34c3b14a
feat: add induction tactic
2020-02-23 17:23:52 -08:00
Leonardo de Moura
c4dac739be
feat: add support for user-defined recursors at getRecInfo
2020-02-23 12:42:08 -08:00
Leonardo de Moura
a5ad840ebe
feat: add getParamNames
2020-02-23 12:01:06 -08:00
Leonardo de Moura
346378b3a3
feat: add [recursor <major-pos>] attribute
2020-02-23 10:35:14 -08:00
Leonardo de Moura
325bb6b5b5
feat: helper function for user-defined recursors
2020-02-23 10:34:49 -08:00
Leonardo de Moura
72f57c923d
feat: helper functions for evalInduction
2020-02-22 19:57:44 -08:00
Leonardo de Moura
8baa376135
feat: allow _ at inductionAlt var names
2020-02-22 12:05:11 -08:00
Leonardo de Moura
472276f63f
feat: add mkRecFor
2020-02-22 11:24:46 -08:00
Leonardo de Moura
38cb8907a0
feat: add helper functions
2020-02-22 11:16:55 -08:00
Leonardo de Moura
4a8c192a00
feat: allow _ "else case" at inductionAlt
2020-02-22 11:16:20 -08:00
Leonardo de Moura
14b9e13dc1
fix: incorrect eraseMacroScopes
2020-02-22 11:16:05 -08:00
Leonardo de Moura
9abb749663
fix: preserve tag
2020-02-21 19:06:54 -08:00
Leonardo de Moura
09f504f376
feat: finish evalGeneralize
2020-02-21 18:32:00 -08:00
