Integrate menhir parser and elaborator tests #1220

7h3kk1d · 2024-02-25T17:13:06Z

No description provided.

… more binops, etc)

…le forms done

cyrus- · 2024-02-27T20:17:25Z

@green726 are you taking a look at this PR or what is the plan? @7h3kk1d

7h3kk1d · 2024-02-27T21:35:34Z

@green726 are you taking a look at this PR or what is the plan? @7h3kk1d

This was still in dev from my perspective but @green726 is going to take over it from now and let me know if they need assistance.

…sues with the output from the menhir -> DHExp

…es & changed tests to reflect this

…ranch holes

…ng to better handle parens + added free var application elaboration test with menhir

…nelse test case

… added ids to the pats

…ory, added in the plus to the fix point function name

cyrus-

left some notes on tweaks. this is going to need to be reworked a bit (but should be mostly similar) with @Negabinary 's upcoming refactoring of DHExp / UExp. since that is coming soon, so will hold off on merging for now but you can make the syntactic changes in the grammar in anticipation of that at least

cyrus- · 2024-04-25T20:25:46Z

src/haz3lcore/dune

@@ -2,7 +2,7 @@

 (library
 (name haz3lcore)
- (libraries util re sexplib unionFind uuidm)
+ (libraries util re sexplib unionFind uuidm hazel_menhir)


the directory is called menhir-parser and the library is called hazel_menhir.

it may make more sense here to just put the parser in haz3lcore under a parser directory.

@cyrus- it seems that the standard/recommended way to do this is with a separate directory/library (see https://stackoverflow.com/questions/70805926/include-mly-files-nested-in-subdirectories-when-compiling-with-dune and ocaml/dune#4381) due to a bug in Dune - if you would prefer I could also place it in a subdirectory of haz3lcore with its own Dune file. I don't have a preference either way - what would you prefer? Thanks!

Can we put the necessary dune menhir invocations into the haz3lcore dune file or does it need its own in a subdirectory? No strong preference here, but would like the directory and library to at least have the same name.

Unfortunately it seems that we can't (that's a known bug with dune according to the stack overflow I linked) - we can put the parser in haz3lcore but the parser directory will also need its own dune file. I think that will keep it part of the same library as haz3lcore? I could try that and if that doesn't work I'll just change the current directory/library to have matching names?

sounds good

cyrus- · 2024-04-25T20:26:46Z

src/haz3lcore/dynamics/DH.re

- | Let(DHPat.t, t, t)
- | FixF(Var.t, Typ.t, t)
- | Fun(DHPat.t, Typ.t, t, option(Var.t))
+ | Filter(DHFilter.t, t) //pause a == 2 b


this can have a few different concrete forms depending on the filter... @tonyfettes

cyrus- · 2024-04-25T20:27:32Z

src/haz3lcore/dynamics/DH.re

- | EmptyHole(MetaVar.t, HoleInstanceId.t)
- | NonEmptyHole(ErrStatus.HoleReason.t, MetaVar.t, HoleInstanceId.t, t)
- | FreeVar(MetaVar.t, HoleInstanceId.t, Var.t)
+ | EmptyHole(MetaVar.t, HoleInstanceId.t) //()


() is the notation for unit values, so let's use ? for empty holes

cyrus- · 2024-04-26T01:06:27Z

src/haz3lcore/dynamics/DH.re

- | NonEmptyHole(ErrStatus.HoleReason.t, MetaVar.t, HoleInstanceId.t, t)
- | FreeVar(MetaVar.t, HoleInstanceId.t, Var.t)
+ | EmptyHole(MetaVar.t, HoleInstanceId.t) //()
+ | NonEmptyHole(ErrStatus.HoleReason.t, MetaVar.t, HoleInstanceId.t, t) //(_HOLE x)


let's use {{e}} for non-empty holes

cyrus- · 2024-04-26T01:08:36Z

src/haz3lcore/dynamics/DH.re

- | FreeVar(MetaVar.t, HoleInstanceId.t, Var.t)
+ | EmptyHole(MetaVar.t, HoleInstanceId.t) //()
+ | NonEmptyHole(ErrStatus.HoleReason.t, MetaVar.t, HoleInstanceId.t, t) //(_HOLE x)
+ | FreeVar(MetaVar.t, HoleInstanceId.t, Var.t) //(_FREE x)


let's use {{?x}} for free variables

cyrus- · 2024-04-26T01:28:29Z

src/haz3lcore/dynamics/DH.re

+ | BoundVar(Var.t) //x
+ | Sequence(t, t) //a; b
+ | Let(DHPat.t, t, t) //let x = y in z
+ | FixF(Var.t, Typ.t, t) //_FIX f Int -> Int fun: Int x -> 1 + x f in 55


I believe the syntax here should be fix x : ty -> e

Ok, I fixed that but I unfortunately cant use the "->" because it seems to create a conflict in Menhir between the exp and typ (I'm pretty sure it is conflicting with the "->" in arrow types) so instead I used "=>". The syntax is now fix x: ty => e, are you alright with that or would you prefer I try to find some way around the conflict?

Maybe have it be parenthesized, so fix x -> e or fix (x : ty) -> e? would prefer to keep the Hazel notation consistent here so if we change it here then we should change it in Hazel

That worked! Thank you!

cyrus- · 2024-04-26T01:29:07Z

src/haz3lcore/dynamics/DH.re

+ | Sequence(t, t) //a; b
+ | Let(DHPat.t, t, t) //let x = y in z
+ | FixF(Var.t, Typ.t, t) //_FIX f Int -> Int fun: Int x -> 1 + x f in 55
+ | Fun(DHPat.t, Typ.t, t, option(Var.t)) //fun: Int x -> x + 1


the syntax here should be fun p -> e

I had to add in manual annotations for the type of the function to be able to construct the dhexp with the type. The current elaborator gets the type from the pattern but uses the statics map - I thought it would be best to just add in the annotations rather than try to interface with that. What do you think?

cyrus- · 2024-04-26T01:29:18Z

src/haz3lcore/dynamics/DH.re

 | TypFun(Term.UTPat.t, t, option(Var.t))
 | TypAp(t, Typ.t)
- | Ap(t, t)
+ | Ap(t, t) //a(1)


cyrus- · 2024-04-26T01:30:12Z

src/haz3lcore/dynamics/DH.re

+ | Cons(t, t) //a :: b
+ | ListConcat(t, t) //a @ b
+ | Tuple(list(t)) //(a, b)
+ | Prj(t, int) //TODO


cyrus- · 2024-04-26T01:31:27Z

src/haz3lcore/dynamics/DH.re

+ | Constructor(string) //X
+ | ConsistentCase(case) //4 == 3 | true => 24 | false => false end
+ | Cast(t, Typ.t, Typ.t) //x <Unknown Internal => Int>
+ | FailedCast(t, Typ.t, Typ.t) //x ?<Int => Int>


e<ty1 =!> ty2> or something like that

green726 · 2024-04-26T03:52:46Z

Sounds good, thanks for the feedback. I'll make those syntactic changes and wait for the new UExp/DHExp to update then I'll mark as ready for review again.

…dh docs to use metavariables

…xtual syntax, fixed menhir conflict with fixf

green726 and others added 17 commits July 27, 2023 09:56

Initial project organization & setup

1b4a6a4

preliminary & minimal implementation of the lexer

d6a6e95

got initial version of parser to work - also added testing code

88f5cc7

drastically expanded parser, lexer, ast (reworked pats vs exps, added…

5cfd56a

… more binops, etc)

added cases & rules

4659076

Expanded the patterns and changed rules/cases

a3c77ed

Added arrow types & expanded test

7759144

formatting

a01b07c

Merge branch 'dev' into menhir_parser

556e8b4

started working on the menhir ast -> DHExp translation - got the simp…

c32dfb2

…le forms done

Merge branch 'dev' into menhir_parser

bfe2db1

finished up preliminary translation

9080650

Added in the cast syntax to the menhir parser; still need to test

af03c40

Merge remote-tracking branch 'origin/dev' into menhir_parser

8aff486

Reformat

951d4a2

Integrate menhir tests with the haz3ltests

97c5187

Try failing test

3bc4227

cyrus- added needs-polish for PRs that are substantially complete but need final polish needs-merge for PRs that need a merge from dev labels Mar 1, 2024

cyrus- changed the base branch from menhir_parser to dev March 1, 2024 05:23

cyrus- mentioned this pull request Mar 1, 2024

Menhir parser #1071

Closed

green726 and others added 3 commits March 11, 2024 11:05

Merge branch 'dev' into menhir_tests

191639e

fixed the menhir parser test for integer literal

db3b918

fixing some bugs with the functions expressions in the menhir parser

cdfc8ad

cyrus- removed the needs-merge for PRs that need a merge from dev label Mar 14, 2024

green726 added 3 commits March 20, 2024 12:53

changed the elaborator test to start adding in Menhir tests - some is…

d3a5995

…sues with the output from the menhir -> DHExp

modified the menhir parser to have manual annotations for fun exp typ…

8ecd025

…es & changed tests to reflect this

added support for the holes, closures, hole ids, and free vars

16b7e4a

green726 added 6 commits April 5, 2024 12:49

added inconsistent branch handling to the menhir parser for testing b…

e3060a7

…ranch holes

reworked hole syntax + added unknown types + changed expression parsi…

6b13317

…ng to better handle parens + added free var application elaboration test with menhir

fixed the ifthenelse menhir -> dhexp translation + added menhir ifthe…

0448846

…nelse test case

added if consistency & test case for inconsistent if

595c6f7

cleaned up the test_elaboration file and removed all non-menhir tests

2ba24df

added the docs as well as cons, seqs, and test to menhir parser

a4d7a93

green726 self-assigned this Apr 22, 2024

green726 added 3 commits April 22, 2024 18:06

added in the remaining pat forms & docs, cleaned up some of the code,…

76d1ef8

… added ids to the pats

merged main into menhir_test

b10b8ac

finished fixing conflicts with the elaborator file & new tests direct…

cd8ae48

…ory, added in the plus to the fix point function name

green726 marked this pull request as ready for review April 22, 2024 23:14

green726 requested a review from cyrus- April 22, 2024 23:14

green726 removed the needs-polish for PRs that are substantially complete but need final polish label Apr 23, 2024

cyrus- requested changes Apr 26, 2024

View reviewed changes

cyrus- marked this pull request as draft April 26, 2024 01:33

green726 added 6 commits April 26, 2024 00:13

changed the hole syntax to align with Cyrus comments; changed menhir …

a33b30d

…dh docs to use metavariables

fixed parser build error, updated DHPat and Typ docs to new menhir te…

27be64a

…xtual syntax, fixed menhir conflict with fixf

updated menhir elaboration unit tests to new menhir dhexp syntax

971945c

changed the fixf to match hazel syntax without menhir conflict

d9d07f9

renamed the menhir parser to match hazel naming conventions

cc2b5dc

updated elaboration tests to the new menhir parser module name

4aed0bc

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Integrate menhir parser and elaborator tests #1220

Integrate menhir parser and elaborator tests #1220

7h3kk1d commented Feb 25, 2024

cyrus- commented Feb 27, 2024

7h3kk1d commented Feb 27, 2024

cyrus- left a comment

cyrus- Apr 25, 2024

green726 May 27, 2024

cyrus- May 28, 2024

green726 May 28, 2024

cyrus- May 28, 2024

cyrus- Apr 25, 2024

cyrus- Apr 25, 2024

cyrus- Apr 26, 2024

cyrus- Apr 26, 2024

cyrus- Apr 26, 2024

green726 May 27, 2024

cyrus- May 28, 2024

green726 May 28, 2024

cyrus- Apr 26, 2024

green726 Apr 26, 2024

cyrus- Apr 26, 2024

cyrus- Apr 26, 2024

cyrus- Apr 26, 2024

green726 commented Apr 26, 2024 •

edited

Integrate menhir parser and elaborator tests #1220

Are you sure you want to change the base?

Integrate menhir parser and elaborator tests #1220

Conversation

7h3kk1d commented Feb 25, 2024

cyrus- commented Feb 27, 2024

7h3kk1d commented Feb 27, 2024

cyrus- left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

green726 commented Apr 26, 2024 • edited

green726 commented Apr 26, 2024 •

edited