Fix record/tuple literal elaboration

Cargo.toml

@@ -3,6 +3,7 @@ inherits = "release"
 debug = true
 
 [workspace]
+resolver = "2"
 members = [
     './fathom',
 ]

fathom/Cargo.toml

@@ -1,20 +1,20 @@
 [package]
-name = "fathom"
-version = "0.1.0"
-authors = ["YesLogic Pty. Ltd. <[email protected]>"]
-repository = "https://github.com/yeslogic/fathom"
-edition = "2021"
+name         = "fathom"
+version      = "0.1.0"
+authors      = ["YesLogic Pty. Ltd. <[email protected]>"]
+repository   = "https://github.com/yeslogic/fathom"
+edition      = "2021"
 rust-version = "1.67.0"
-publish = false
+publish      = false
 
 description = "A language for declaratively specifying binary data formats"
-readme = "../README.md"
-license = "Apache-2.0"
+readme      = "../README.md"
+license     = "Apache-2.0"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [[test]]
-name = "source_tests"
+name    = "source_tests"
 harness = false
 
 [dependencies]
@@ -23,25 +23,29 @@ clap = { version = "4.0", features = ["derive"] }
 codespan-reporting = "0.11.1"
 fxhash = "0.2"
 itertools = "0.10"
-lalrpop-util = "0.19.5"
-lasso = { version = "0.6.0", features = ["multi-threaded", "ahasher", "inline-more"] }
+lalrpop-util = "0.20.0"
 levenshtein = "1.0.5"
 logos = "0.12"
+lasso = { version = "0.6.0", features = [
+    "multi-threaded",
+    "ahasher",
+    "inline-more",
+] }
 once_cell = { version = "1.17.0", features = ["parking_lot"] }
 pretty = "0.11.2"
 rpds = "0.12.0"
 scoped-arena = "0.4.1"
 termsize = "0.1.6"
 
 [build-dependencies]
-lalrpop = { git = "https://github.com/kmeakin/lalrpop", branch = "raw-identifiers" }
+lalrpop = "0.20.0"
 
 [dev-dependencies]
-diff = "0.1.12"
-globwalk = "0.8"
-itertools = "0.10.1"
+diff          = "0.1.12"
+globwalk      = "0.8"
+itertools     = "0.10.1"
 libtest-mimic = "0.6.0"
-serde = { version = "1.0", features = ["derive"] }
-toml = "0.5"
-trycmd = "0.14.10"
-walkdir = "2.3.2"
+serde         = { version = "1.0", features = ["derive"] }
+toml          = "0.5"
+trycmd        = "0.14.10"
+walkdir       = "2.3.2"

fathom/src/core/semantics.rs

@@ -658,6 +658,21 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> {
         self.local_exprs.pop();
     }
 
+    /// Quote a [value][Value] back into a [term][Term], with `self.local_exprs`
+    /// offset by `offset`.
+    pub fn quote_offset<'out_arena>(
+        &mut self,
+        scope: &'out_arena Scope<'out_arena>,
+        value: &ArcValue<'in_arena>,
+        offset: EnvLen,
+    ) -> Term<'out_arena> {
+        let len = self.local_exprs;
+        self.local_exprs.append(offset);
+        let expr = self.quote(scope, value);
+        self.local_exprs.truncate(len);
+        expr
+    }
+
     /// Quote a [value][Value] back into a [term][Term].
     pub fn quote<'out_arena>(
         &mut self,

fathom/src/env.rs

@@ -162,6 +162,10 @@ impl EnvLen {
         self.0 -= 1;
     }
 
+    pub fn append(&mut self, other: EnvLen) {
+        self.0 += other.0;
+    }
+
     /// Truncate the environment to the given length.
     pub fn truncate(&mut self, len: EnvLen) {
         *self = len;

fathom/src/surface.rs

@@ -440,7 +440,7 @@ impl ParseMessage {
             LalrpopParseError::InvalidToken { location } => ParseMessage::InvalidToken {
                 range: ByteRange::new(location, location),
             },
-            LalrpopParseError::UnrecognizedEOF { location, expected } => {
+            LalrpopParseError::UnrecognizedEof { location, expected } => {
                 ParseMessage::UnrecognizedEof {
                     range: ByteRange::new(location, location),
                     expected, // TODO: convert to descriptions?

fathom/src/surface/elaboration.rs

@@ -1563,15 +1563,17 @@ impl<'arena> Context<'arena> {
                 let mut types = SliceVec::new(self.scope, labels.len());
                 let mut exprs = SliceVec::new(self.scope, labels.len());
 
+                let mut offset = EnvLen::new();
                 for expr_field in expr_fields {
                     let name_expr = Term::Name(expr_field.label.0, expr_field.label.1);
                     let expr = expr_field.expr.as_ref().unwrap_or(&name_expr);
                     let (expr, r#type) = self.synth(expr);
-                    types.push(self.quote_env().quote(self.scope, &r#type));
+                    types.push(self.quote_env().quote_offset(self.scope, &r#type, offset));
                     exprs.push(expr);
+                    offset.push();
                 }
 
-                let types = Telescope::new(self.local_env.exprs.clone(), types.into());
+                let types = Telescope::new(self.local_env.exprs.clone(), (types.into()));
 
                 (
                     core::Term::RecordLit(file_range.into(), labels, exprs.into()),
@@ -1585,10 +1587,12 @@ impl<'arena> Context<'arena> {
                 let mut exprs = SliceVec::new(self.scope, labels.len());
                 let mut types = SliceVec::new(self.scope, labels.len());
 
+                let mut offset = EnvLen::new();
                 for elem_exprs in elem_exprs.iter() {
                     let (expr, r#type) = self.synth(elem_exprs);
-                    types.push(self.quote_env().quote(self.scope, &r#type));
+                    types.push(self.quote_env().quote_offset(self.scope, &r#type, offset));
                     exprs.push(expr);
+                    offset.push();
                 }
 
                 let types = Telescope::new(self.local_env.exprs.clone(), types.into());

tests/cmd/fathom-data.md

@@ -17,7 +17,7 @@ Options:
       --module <MODULE_FILE>  Path to a module to load when reading
       --format <FORMAT>       Format used when reading the binary data [default: main]
       --allow-errors          Continue even if errors were encountered
-  -h, --help                  Print help information (use `--help` for more detail)
+  -h, --help                  Print help (see more with '--help')
 
 Examples:
 
@@ -56,7 +56,7 @@ Options:
           Continue even if errors were encountered
 
   -h, --help
-          Print help information (use `-h` for a summary)
+          Print help (see a summary with '-h')
 
 Binary data can be read using a term supplied by the `--format` option:
 
@@ -181,13 +181,13 @@ Arguments must be provided to `fathom data`
 ```console
 $ fathom data
 ? failed
-error: The following required arguments were not provided:
+error: the following required arguments were not provided:
   --format <FORMAT>
   <BINARY_FILE>
 
 Usage: fathom data --format <FORMAT> <BINARY_FILE>
 
-For more information try '--help'
+For more information, try '--help'.
 
 ```
 
@@ -196,12 +196,12 @@ The `--format` option must be present when `--module` is not supplied
 ```console
 $ fathom data formats/data/edid/dell-P2415Q.edid
 ? failed
-error: The following required arguments were not provided:
+error: the following required arguments were not provided:
   --format <FORMAT>
 
 Usage: fathom data --format <FORMAT> <BINARY_FILE>
 
-For more information try '--help'
+For more information, try '--help'.
 
 ```
 

tests/cmd/fathom-elab.md

@@ -15,7 +15,7 @@ Options:
       --term <TERM_FILE>      Path to a term to elaborate
       --allow-errors          Continue even if errors were encountered
       --pretty-core           Pretty print core module
-  -h, --help                  Print help information
+  -h, --help                  Print help
 
 ```
 
@@ -32,7 +32,7 @@ Options:
       --term <TERM_FILE>      Path to a term to elaborate
       --allow-errors          Continue even if errors were encountered
       --pretty-core           Pretty print core module
-  -h, --help                  Print help information
+  -h, --help                  Print help
 
 ```
 
@@ -72,13 +72,13 @@ Either a `--module` or a `--term` must be provided
 ```console
 $ fathom elab
 ? failed
-error: The following required arguments were not provided:
+error: the following required arguments were not provided:
   --module <MODULE_FILE>
   --term <TERM_FILE>
 
 Usage: fathom elab --module <MODULE_FILE> --term <TERM_FILE>
 
-For more information try '--help'
+For more information, try '--help'.
 
 ```
 
@@ -90,11 +90,11 @@ The `--module` and `--term` inputs conflict with each other
 $ fathom elab --module formats/object-id.fathom
 >             --term tests/succeed/record-type/pair-dependent.fathom
 ? failed
-error: The argument '--module <MODULE_FILE>' cannot be used with '--term <TERM_FILE>'
+error: the argument '--module <MODULE_FILE>' cannot be used with '--term <TERM_FILE>'
 
 Usage: fathom elab --module <MODULE_FILE>
 
-For more information try '--help'
+For more information, try '--help'.
 
 ```
 

tests/cmd/fathom-norm.md

@@ -13,7 +13,7 @@ Usage: fathom norm [OPTIONS] --term <TERM_FILE>
 Options:
       --term <TERM_FILE>  Path to a term to normalize
       --allow-errors      Continue even if errors were encountered
-  -h, --help              Print help information
+  -h, --help              Print help
 
 ```
 
@@ -28,7 +28,7 @@ Usage: fathom norm [OPTIONS] --term <TERM_FILE>
 Options:
       --term <TERM_FILE>  Path to a term to normalize
       --allow-errors      Continue even if errors were encountered
-  -h, --help              Print help information
+  -h, --help              Print help
 
 ```
 
@@ -53,12 +53,12 @@ At least a `--term` must be provided
 ```console
 $ fathom norm
 ? failed
-error: The following required arguments were not provided:
+error: the following required arguments were not provided:
   --term <TERM_FILE>
 
 Usage: fathom norm --term <TERM_FILE>
 
-For more information try '--help'
+For more information, try '--help'.
 
 ```
 

tests/cmd/fathom.md

@@ -17,8 +17,8 @@ Commands:
   help  Print this message or the help of the given subcommand(s)
 
 Options:
-  -h, --help     Print help information
-  -V, --version  Print version information
+  -h, --help     Print help
+  -V, --version  Print version
 
 ```
 
@@ -37,8 +37,8 @@ Commands:
   help  Print this message or the help of the given subcommand(s)
 
 Options:
-  -h, --help     Print help information
-  -V, --version  Print version information
+  -h, --help     Print help
+  -V, --version  Print version
 
 ```
 
@@ -60,7 +60,7 @@ Commands:
   help  Print this message or the help of the given subcommand(s)
 
 Options:
-  -h, --help     Print help information
-  -V, --version  Print version information
+  -h, --help     Print help
+  -V, --version  Print version
 
 ```

tests/succeed/record-type/generic-pair.fathom

@@ -1,3 +1,8 @@
 let fst = fun (A: Type) (B: Type) (p: {x: A, y: B}) => p.x;
 let snd = fun (A: Type) (B: Type) (p: {x: A, y: B}) => p.y;
-{}
+
+// Regression tests for https://github.com/yeslogic/fathom/issues/507
+let pair_make = fun (A: Type) (B: Type) (x: A) (y: B)     => {x = x, y = y};
+let pair_id   = fun (A: Type) (B: Type) (p: {x: A, y: B}) => {x = p.x, y = p.y};
+let pair_swap = fun (A: Type) (B: Type) (p: {x: A, y: B}) => {x = p.y, y = p.x};
+{}

tests/succeed/record-type/generic-pair.snap

@@ -1,6 +1,16 @@
 stdout = '''
 let fst : fun (A : Type) (B : Type) -> { x : A, y : B } -> A = fun A B p => p.x;
 let snd : fun (A : Type) (B : Type) -> { x : A, y : B } -> B = fun A B p => p.y;
+let pair_make : fun (A : Type) (B : Type) -> A -> B -> { x : A, y : B } =
+fun A B x y => { x, y };
+let pair_id : fun (A : Type) (B : Type) -> { x : A, y : B } -> {
+    x : A,
+    y : B,
+} = fun A B p => { x = p.x, y = p.y };
+let pair_swap : fun (A : Type) (B : Type) -> { x : A, y : B } -> {
+    x : B,
+    y : A,
+} = fun A B p => { x = p.y, y = p.x };
 () : ()
 '''
 stderr = ''

tests/succeed/tuple/generic-pair.fathom

@@ -1,3 +1,8 @@
 let fst = fun (A: Type) (B: Type) (p: {_0: A, _1: B}) => p._0;
 let snd = fun (A: Type) (B: Type) (p: (A, B)) => p._1;
+
+// Regression tests for https://github.com/yeslogic/fathom/issues/507
+let pair_make = fun (A: Type) (B: Type) (x: A) (y: B) => (x, y);
+let pair_id   = fun (A: Type) (B: Type) (p: (A, B))   => (p._0, p._1);
+let pair_swap = fun (A: Type) (B: Type) (p: (A, B))   => (p._1, p._0);
 {}

tests/succeed/tuple/generic-pair.snap

@@ -1,6 +1,18 @@
 stdout = '''
 let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => p._0;
 let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => p._1;
+let pair_make : fun (A : Type) (B : Type) -> A -> B -> (A, B) = fun A B x y => (
+    x,
+    y,
+);
+let pair_id : fun (A : Type) (B : Type) -> (A, B) -> (A, B) = fun A B p => (
+    p._0,
+    p._1,
+);
+let pair_swap : fun (A : Type) (B : Type) -> (A, B) -> (B, A) = fun A B p => (
+    p._1,
+    p._0,
+);
 () : ()
 '''
 stderr = ''