Frédéric Tuong
|
115e5fa90a
|
implement the dynamic definition of C commands
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13715 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 21:33:28 +00:00 |
|
Frédéric Tuong
|
ba7b8eecb2
|
simplify
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13714 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 15:59:17 +00:00 |
|
Frédéric Tuong
|
59b76da106
|
add ignored tokens in the parsing env
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13713 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 15:01:03 +00:00 |
|
Frédéric Tuong
|
4cb1ac12b2
|
generalize
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13712 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 12:12:56 +00:00 |
|
Frédéric Tuong
|
af97900479
|
delay at most the reading
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13711 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 10:54:16 +00:00 |
|
Frédéric Tuong
|
020d99cf2c
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13710 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 10:33:07 +00:00 |
|
Frédéric Tuong
|
ac888ae957
|
generalize
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13709 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-19 10:31:38 +00:00 |
|
Frédéric Tuong
|
2f2033e19b
|
parse cpp-directives
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13708 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 21:03:20 +00:00 |
|
Frédéric Tuong
|
901c4cb7eb
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13707 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 20:35:11 +00:00 |
|
Frédéric Tuong
|
a7a5ed3d97
|
simplify
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13706 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 20:34:13 +00:00 |
|
Frédéric Tuong
|
9182e41558
|
alpha-rename
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13705 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 19:35:03 +00:00 |
|
Frédéric Tuong
|
72e4682bdf
|
permute some paragraphs
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13704 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 19:22:36 +00:00 |
|
Frédéric Tuong
|
419fd5ebbb
|
split
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13703 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 18:58:49 +00:00 |
|
Frédéric Tuong
|
ebd74f892b
|
permute some paragraphs
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13702 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 18:40:21 +00:00 |
|
Frédéric Tuong
|
2bbb85a9ba
|
permute some paragraphs
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13701 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 18:34:40 +00:00 |
|
Frédéric Tuong
|
9ab680325e
|
split
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13700 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 18:28:13 +00:00 |
|
Frédéric Tuong
|
a1ea4b8cc6
|
alpha-rename
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13699 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 18:21:49 +00:00 |
|
Frédéric Tuong
|
13ec8be28c
|
simplify
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13698 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 16:50:04 +00:00 |
|
Frédéric Tuong
|
4226e6fdfd
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13697 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 16:49:44 +00:00 |
|
Frédéric Tuong
|
6f2b6c4bcc
|
cancel the repeated initialization of reports for nested hooks by adding a persistent reports field with context in env_tree
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13696 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 16:46:40 +00:00 |
|
Frédéric Tuong
|
0a84d9e82b
|
signal markups for permissive antiquotations everytime, unless all are failing together
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13695 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 10:07:54 +00:00 |
|
Frédéric Tuong
|
90bd9a1909
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13694 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 09:56:59 +00:00 |
|
Frédéric Tuong
|
f0189271af
|
parameterize the parsing part to receive env in input, and take an abstract err function in output (hook actions are generalized from theory to context as well)
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13693 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-18 09:54:07 +00:00 |
|
Frédéric Tuong
|
42dcf1b634
|
update the generated files
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13692 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-15 15:44:21 +00:00 |
|
Frédéric Tuong
|
2785fe2364
|
parse define and undef
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13690 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 19:08:49 +00:00 |
|
Frédéric Tuong
|
cb0a70fb89
|
fix
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13689 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 18:58:37 +00:00 |
|
Frédéric Tuong
|
86bcb917bb
|
output traces
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13688 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 18:56:36 +00:00 |
|
Frédéric Tuong
|
9588bfeea1
|
alpha-rename
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13687 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 18:53:48 +00:00 |
|
Frédéric Tuong
|
4beb379349
|
fix
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13686 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 18:49:47 +00:00 |
|
Frédéric Tuong
|
b3392d1ad9
|
simplify
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13685 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 13:43:12 +00:00 |
|
Frédéric Tuong
|
154800e4be
|
separate blanks from directives
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13684 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 12:19:14 +00:00 |
|
Frédéric Tuong
|
6573e8c92e
|
simplify
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13683 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 11:29:00 +00:00 |
|
Frédéric Tuong
|
8ac09a261b
|
output traces
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13681 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 09:21:55 +00:00 |
|
Frédéric Tuong
|
08e1411dfd
|
output traces
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13680 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-14 09:14:12 +00:00 |
|
Frédéric Tuong
|
5909b19b31
|
report positions of typedef
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13679 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 20:45:54 +00:00 |
|
Frédéric Tuong
|
29e5bfbcaa
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13678 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 20:05:35 +00:00 |
|
Frédéric Tuong
|
33cef91a5e
|
pair the environment with the corresponding ML functions together
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13677 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 20:02:25 +00:00 |
|
Frédéric Tuong
|
087bc1c6a8
|
output traces
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13676 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 19:55:38 +00:00 |
|
Frédéric Tuong
|
2de014aaf1
|
update the generated files
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13675 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 19:36:53 +00:00 |
|
Frédéric Tuong
|
0a4c0f2114
|
provide additional information for manual copy and edits
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13674 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 19:36:15 +00:00 |
|
Frédéric Tuong
|
c48169669d
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13672 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 08:02:44 +00:00 |
|
Frédéric Tuong
|
c2841a4489
|
output traces
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13671 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-13 08:01:00 +00:00 |
|
Frédéric Tuong
|
54696b15a4
|
output traces
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13670 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-12 14:48:21 +00:00 |
|
Frédéric Tuong
|
3503ee14cf
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13669 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 16:18:22 +00:00 |
|
Frédéric Tuong
|
73b3dcf9aa
|
continue
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13668 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 15:35:26 +00:00 |
|
Frédéric Tuong
|
3a530356f4
|
permute some paragraphs
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13667 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 15:29:41 +00:00 |
|
Frédéric Tuong
|
e1b8abc526
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13666 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 15:25:11 +00:00 |
|
Frédéric Tuong
|
df6b7a9d96
|
update the generated files
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13665 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 14:13:12 +00:00 |
|
Frédéric Tuong
|
1434608708
|
copy
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13664 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 14:10:28 +00:00 |
|
Frédéric Tuong
|
42674c06fa
|
implement the top-down execution of static ML functions at each node (using a stack storing tree elements, as they are provided in bottom-up order in reduce rules)
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@13663 3260e6d1-4efc-4170-b0a7-36055960796d
|
2019-03-11 14:04:34 +00:00 |