#
5417af9d |
|
31-Mar-2020 |
Arve Gengelbach <arve.gengelbach@it.uu.se> |
remove lcsymtacs (github issue #666) The lcsymtacs structure is regarded superseded as it plainly is a shorthand for opening the following modules: Abbrev HolKernel boolLib Tactic Tactical BasicProvers simpLib Rewrite bossLib Thm_cont
|
#
4ae757b5 |
|
14-Nov-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Clean up context-free/grammar a little
|
#
a083c115 |
|
13-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Deal with rebindings of ptree_{size,fringe}_def in grammarScript Ability to EVAL these constants is lost because of b98f5ead5 Not sure that anybody ever used this, but still. With regression test.
|
#
1a6b7f48 |
|
26-Mar-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Define valid_lptree constant (from CakeML). This constant asserts that the parse tree respects the provided grammar (as per valid_ptree), but also that every non-terminal node in the tree has the correct locations recorded (derived from the locations of the sub-trees, using the merge_list_locs constant.
|
#
1c655125 |
|
26-Mar-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in grammarScript.sml
|
#
4d564255 |
|
26-Mar-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Define real_fringe constant and prove some properties (from CakeML) The simpler ptree_fringe returns just the tokens; real_fringe returns the actual fringe, which couples the tokens with their locations.
|
#
a6274839 |
|
24-Feb-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Try a slightly different approach to handling locations in parse trees
|
#
1141eca6 |
|
15-Feb-2017 |
H.Feree <h.feree@kent.ac.uk> |
Location from parse_tree
|
#
c59c4caf |
|
13-Feb-2017 |
H.Feree <h.feree@kent.ac.uk> |
Location in parser done (up to a cheat)
|
#
8686858a |
|
29-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix CFG theories in light of pat_assum rename
|
#
05199544 |
|
20-Sep-2015 |
Konrad Slind <konrad.slind@gmail.com> |
playground for formal language theory developments.
|