More transpiler functionality and fixes from Sprint 2 (started Aug 29) #431

ym-han · 2023-09-17T17:36:34Z

This PR fixes some of the bugs in the transpiler and adds more functionality. In a nutshell, most of the functionality required by the current encoding should be there, though there's still work to be done on testing, making the design more modular, improving error diagnostics, etc.

In particular, this PR

implements support for the ditto syntax in the transpiler
improves handling of RPrels in SimplifyL4.hs
adds more graceful error handling in SimplifyL4.hs
adds some notes on LE syntax in README.md
implements replacement of '%', '.', ','. These are currently hard-coded; in the future we can read in a .tsv with the desired replacements, a .tsv that can then be kept in sync with the web app side (since that also needs to be able to run the replacements in the other direction).
filters out superfluous templates, in part with heuristics --- we now filter out NLAs/templates that are subsumed by lib templates, as well as (i) the templates that have fewer vars than the templates whose regexes match them and (ii) templates with the same number of vars but that are less informative
generically derives prisms and other useful optics for the L4 Rule datatype

We can try to cache the PCRE installation step in the github workflow more effectively in future work.

Co-authored-by: johsi-k johsi.k@gmail.com

…tomics

it’s quite important that * there not be empty cells in the head or body between contentful cells, * there not be `""` below the `DECIDE` --- if there are `""` below the `DECIDE`, then the stuff below will get parsed as distinct Hornlikes but without the givens, and the only way to then figure out what the original givens were will be very fragile

…e: Check upfront for wehther there are non-text mtexpr variable names in the GIVENs; raise a `dispute` if so and print warning as comment in resulting .le

…ics` and `optics`

…eamline the code (remove overly complicated typeclass typeapplications stuff) while still getting compiler support for subtypes of RPRel, by using GADTs and my own RPRel-esque type 2. Add support for arith comparison

…not working on it right now

…nt places in NLAs (instead of just 'a var') and for more nuanced filtering downstream

…tification

…have to escape metachars in Pred)

…tions over concrete data structures

…g NLA has more vars than the subsumed one), among the non-lib NLAs. (Will need to handle subsumed but same-num-of-vars NLAs separately.)

…port the `NLA` record without exporting the accessors

…LENLA`; and add `regextravifyNLASection :: T.Text -> Maybe [RegexTrav]`

…eriod, just in case

…subsumed (etc) NLAs into one place (in LE.hs), to make code more modular and readable

…t-up-to-varnames (with same number of vars) NLAs

… var names (and have the same number of vars) as comments in case the user didn't mean for them to be removed

… of having `isReg` and `isHlike` functions, to avoid confusing people

ym-han added 30 commits September 4, 2023 20:10

Experiment with using optics to derive prisms for L4 Rule datatype

28694e5

Replace "." with "dot" and "," with "comma", in the Pred txts of ABPa…

54dbc8f

…tomics

remove the old check refine prevalidation stuff for now

cc8173c

idVars.hs: make replacePunctn safer by checking if input is empty

eb75155

LE.hs: clean up imports a bit

8af7cd1

SimplifyL4.hs: simplify code in simplifyL4rule; add comments

86c34d5

SimplifyL4.hs: remove error in mte2cell; add note abt MTB

6f1e10a

clean up

f83ae40

Simplify some applicative code in termIsNaryOpOf with HLint's help

f6fe846

SimplifyL4.hs: Remove error from gmtexpr2gvar; add TODO for futur…

aee9f90

…e: Check upfront for wehther there are non-text mtexpr variable names in the GIVENs; raise a `dispute` if so and print warning as comment in resulting .le

Improve haddock annotations

d582be0

SimplifyL4.hs: Simplify function for getting Givens with `generic-opt…

833825e

…ics` and `optics`

SimplifyL4.hs: remove viewpatterns -- didn't end up needing it

3210fbb

LogicalEnglish.Types: remove unused pragmas

fa6c305

SimplifyL4.hs: clean up internal logic of simpheadRPC

2b94fc4

add README.md: some quick notes on LE syntax

852da85

LE Pretty.hs: remove some of the unnecessary imports

354c4e9

ValidateL4Input.hs: temporarily disable warnings for this file since …

c0847e2

…not working on it right now

GenLEHCs.hs: remove some redundant imports

d1ea453

WIP: refactor NLAs to allow for adding partial info within the argume…

a9fe34d

…nt places in NLAs (instead of just 'a var') and for more nuanced filtering downstream

LE Types.hs: streamline mkNLA by using the onNonEmpty hof

a26033a

WIP: NLA refactoring to get smarter filtering and better NLAs for jus…

4570682

…tification

GenNLAs.hs: escape the pred txt for now (TODO: Add tests to check if …

f9f2004

…have to escape metachars in Pred)

GenNLAs.hs: first draft of subsumes

4407256

GenNLAs.hs: fix subsumes

15bf0e5

clean up GenNLAs.hs some

6fd34ea

start of utils for providing english-y translations of optics abstrac…

aeced88

…tions over concrete data structures

GenNLA.hs: add simple implementation of getNonSubsumed

0db02d7

ym-han added 22 commits September 14, 2023 15:50

GenNLAs.hs and LE.hs: feat. filter out subsumed NLAs (if the subsumin…

472dc47

…g NLA has more vars than the subsumed one), among the non-lib NLAs. (Will need to handle subsumed but same-num-of-vars NLAs separately.)

LETypes.hs: clean up; export prisms for TemplateVar

f5b83c4

LE.hs and GenNLAs.hs: more clean up; remove NLA pattern and just ex…

9f74b2d

…port the `NLA` record without exporting the accessors

GenNLA.hs: make iso for newtype NLATxt and other misc clean up

6293f14

WIP: filtering out lib templates

7f7a9c4

GenNLAs.hs: more clean up, mostly to do with the _MkNLATxt iso

64e5e3f

GenNLAs.hs: rename removeSubsumed to removeRegexMatched

2fd2543

GenNLAs.hs: clean up regextravify stuff; add comments to `rawregexify…

415fcd4

…LENLA`; and add `regextravifyNLASection :: T.Text -> Maybe [RegexTrav]`

update lib hcs

68c78b3

update lib templates

6afc96a

WIP: first attempt at filtering out things subsumed by lib templates

5089129

some clean up

a9f5bc9

IdVars.hs: replace '%' with ' percent' in Preds of VCells

e253b17

LE Pretty.hs: make sure that only the last lib template ends with a p…

ed12bec

…eriod, just in case

LE utils.hs: move HS import into doctest setup

f9d50ef

Consolidate all the 'top-level' orchestrating code for filtering out …

8f02faa

…subsumed (etc) NLAs into one place (in LE.hs), to make code more modular and readable

GenNLAs.hs: Implement removeDisprefdAmongEquivUpToVarNames, first pass

df1ec51

move (<||>) to LS.Utils

813d25c

Implement core functionality for filtering out dispreferred equivalen…

d5e87dc

…t-up-to-varnames (with same number of vars) NLAs

LE Pretty.hs: include the filtered out templates that are equiv up to…

c1cd7a7

… var names (and have the same number of vars) as comments in case the user didn't mean for them to be removed

LS.Rule: move the Data-Generics-Sum-Constructors to comments, instead…

0601d08

… of having `isReg` and `isHlike` functions, to avoid confusing people

cleanup

63fda5f

ym-han requested review from mengwong, joewatt95 and kharus September 17, 2023 17:36

ym-han force-pushed the aug29-more-le-transpiler-fixes branch from 0b1589c to 2757151 Compare September 17, 2023 18:25

haskell.yml: try installing pcre as prereq

725a4c4

ym-han force-pushed the aug29-more-le-transpiler-fixes branch from 2757151 to 725a4c4 Compare September 17, 2023 18:29

ym-han merged commit 0b6cbc4 into main Sep 17, 2023
3 checks passed

ym-han deleted the aug29-more-le-transpiler-fixes branch September 17, 2023 19:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

More transpiler functionality and fixes from Sprint 2 (started Aug 29) #431

More transpiler functionality and fixes from Sprint 2 (started Aug 29) #431

ym-han commented Sep 17, 2023 •

edited

Loading

More transpiler functionality and fixes from Sprint 2 (started Aug 29) #431

More transpiler functionality and fixes from Sprint 2 (started Aug 29) #431

Conversation

ym-han commented Sep 17, 2023 • edited Loading

ym-han commented Sep 17, 2023 •

edited

Loading