Skip to content
This repository has been archived by the owner on Apr 2, 2023. It is now read-only.

Make lines Immortal. #431

Merged
merged 11 commits into from
Nov 11, 2017
Merged

Make lines Immortal. #431

merged 11 commits into from
Nov 11, 2017

Conversation

favonia
Copy link
Contributor

@favonia favonia commented Nov 10, 2017 •
edited
Loading

  • Rename PATH_ABS to ABS and PATH_APP to DIM_APP.
  • Get rid of the _TY suffix.
  • Embrace the Immortal syntax (-> dim A).

@favonia favonia self-assigned this Nov 10, 2017
favonia
favonia commented Nov 11, 2017
View reviewed changes
src/redprl/pretty.sml
Atomic.squares @@ hsep
[seq [ppTerm r1, Atomic.equals, ppTerm r2],
nest 1 @@ hvsep [Atomic.braces @@ ppVar u, ppTerm mu]]
nest 1 @@ ppBinder tube]
Copy link
Contributor Author

@favonia favonia Nov 11, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@jonsterling Is Was there a reason not to group them?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't remember

@favonia
Copy link
Contributor Author

favonia commented Nov 11, 2017

@jonsterling How to enable backtracking in something like Lcf.rule o Path.EqApp orelse_ Lcf.rule o Line.EqApp? The current auto tactic mightl be stuck with (line [_] a) match path @ 0 and I want it to (1) automatically fail and (2) go back to some branching point.

@jonsterling
Copy link
Contributor

@favonia It should be possible to use tac1 par tac2 in the ML code; let me know if that works. I've had some trouble with the backtracking stuff so far.

@favonia
Copy link
Contributor Author

favonia commented Nov 11, 2017

Hmm it's still not working. Not sure how to make this work:

a : (U 0 kan)
l : (line [_] a)
>> (@ l 0) in a

@jonsterling
Copy link
Contributor

@favonia OK; it's hard to debug that stuff, so I don't know for sure what to do. At the moment, I recommend using refine, until we figure out what is going on.

@favonia
Copy link
Contributor Author

favonia commented Nov 11, 2017

Suddenly MLton on travis is running out of time...

@favonia favonia requested a review from jonsterling November 11, 2017 04:04
jonsterling
jonsterling approved these changes Nov 11, 2017
View reviewed changes
Copy link
Contributor

@jonsterling jonsterling left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks fine!

@favonia favonia merged commit 3b79836 into master Nov 11, 2017
@favonia favonia deleted the immortal-lines branch November 11, 2017 04:34
@favonia favonia mentioned this pull request Nov 11, 2017
Closed
@favonia favonia restored the immortal-lines branch November 11, 2017 13:46
@favonia favonia deleted the immortal-lines branch November 11, 2017 13:55
@favonia favonia mentioned this pull request Nov 11, 2017
Closed
@favonia favonia restored the immortal-lines branch November 11, 2017 16:41
@favonia
Copy link
Contributor Author

favonia commented Jan 13, 2018

The branch is now deleted because #437 is no longer active.

@favonia favonia deleted the immortal-lines branch January 13, 2018 04:41
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@jonsterling jonsterling jonsterling approved these changes

Assignees

@favonia favonia

Labels
A-parser A-printer
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@favonia @jonsterling @cangiuli