~ehmry/dhall-nim

3b8e458902381c24b7b3d837bcae08870eb11eb0 — Emery Hemingway 10 months ago c1e3542
Asynchronous import, type check
M dhall-lang => dhall-lang +1 -1
@@ 1,1 1,1 @@
Subproject commit bf757ba1ee526714278568012c6bc98d7ea9757e
Subproject commit e35f69d966f205fdc0d6a5e8d0209e7b600d90b3

M dhall.nimble => dhall.nimble +3 -2
@@ 2,12 2,13 @@

version       = "0.1.0"
author        = "Emery Hemingway"
description   = "Dhall interpreter"
description   = "Dhall language evaluator"
license       = "GPL-3.0"
srcDir        = "src"
installExt    = @["nim"]



# Dependencies

requires "nim >= 1.2.0", "bigints", "cbor", "npeg"
requires "nim >= 1.2.0", "bigints", "cbor >= 0.7.0", "npeg", "nimSHA2"

A flake.lock => flake.lock +25 -0
@@ 0,0 1,25 @@
{
  "nodes": {
    "nixpkgs": {
      "locked": {
        "lastModified": 1604832196,
        "narHash": "sha256-6UH69Ezew96pQiTuKdRa0WrLVsJmti4/2avwEd/Iz10=",
        "owner": "NixOS",
        "repo": "nixpkgs",
        "rev": "6519e0b796addb4d28f7852bdcafcbb0b8b3fe62",
        "type": "github"
      },
      "original": {
        "id": "nixpkgs",
        "type": "indirect"
      }
    },
    "root": {
      "inputs": {
        "nixpkgs": "nixpkgs"
      }
    }
  },
  "root": "root",
  "version": 7
}

A flake.nix => flake.nix +15 -0
@@ 0,0 1,15 @@
{
  description = "Nim Dhall evaluator";

  outputs = { self, nixpkgs }:
    let
      systems = [ "x86_64-linux" "aarch64-linux" ];
      forAllSystems = f: nixpkgs.lib.genAttrs systems (system: f system);
    in {

      devShell = forAllSystems (system:
        with nixpkgs.legacyPackages.${system};
        mkShell { buildInputs = [ nim openssl ]; });

    };
}

D src/dhall.abnf => src/dhall.abnf +0 -932
@@ 1,932 0,0 @@
; ABNF syntax based on RFC 5234
;
; The character encoding for Dhall is UTF-8
;
; Some notes on implementing this grammar:
;
; First, do not use a lexer to tokenize the file before parsing.  Instead, treat
; the individual characters of the file as the tokens to feed into the parser.
; You should not use a lexer because Dhall's grammar supports two features which
; cannot be correctly supported by a lexer:
;
; * String interpolation (i.e. "foo ${Natural/toInteger bar} baz")
; * Nested block comments (i.e. "{- foo {- bar -} baz -}")
;
; Second, this grammar assumes that your parser can backtrack and/or try
; multiple parses simultaneously.  For example, consider this expression:
;
;     List ./MyType
;
; A parser might first try to parse the period as the beginning of a field
; selector, only to realize immediately afterwards that `/MyType` is not a valid
; name for a field.  A conforming parser must backtrack so that the expression
; `./MyType` can instead be correctly interpreted as a relative path
;
; Third, if there are multiple valid parses then prefer the first parse
; according to the ordering of alternatives. That is, the order of evaluation
; of the alternatives is left-to-right.
;
; For example, the grammar for single quoted string literals is:
;
;     single-quote-continue =
;           "'''"               single-quote-continue
;         / "${" complete-expression "}" single-quote-continue
;         / "''${"              single-quote-continue
;         / "''"
;         / %x20-10FFFF         single-quote-continue
;         / tab                 single-quote-continue
;         / end-of-line         single-quote-continue
;
;         single-quote-literal = "''" single-quote-continue
;
; ... which permits valid parses for the following code:
;
;     "''''''''''''''''"
;
; If you tried to parse all alternatives then there are at least two valid
; interpretations for the above code:
;
; * A single quoted literal with four escape sequences of the form "'''"
;     * i.e. "''" followed by "'''"  four times in a row followed by "''"
; * Four empty single quoted literals
;     * i.e. "''''" four times in a row
;
; The correct interpretation is the first one because parsing the escape
; sequence "'''" takes precedence over parsing the termination sequence "''",
; according to the order of the alternatives in the `single-quote-continue`
; rule.
;
; Some parsing libraries do not backtrack by default but allow the user to
; selectively backtrack in certain parts of the grammar.  Usually parsing
; libraries do this to improve efficiency and error messages.  Dhall's grammar
; takes that into account by minimizing the number of rules that require the
; parser to backtrack and comments below will highlight where you need to
; explicitly backtrack
;
; Specifically, if you see an uninterrupted literal in a grammar rule such as:
;
;     "->"
;
; ... or:
;
;     %x66.6f.72.61.6c.6c
;
; ... then that string literal is parsed as a single unit, meaning that you
; should backtrack if you parse only part of the literal
;
; In all other cases you can assume that you do not need to backtrack unless
; there is a comment explicitly asking you to backtrack
;
; When parsing a repeated construct, prefer alternatives that parse as many
; repetitions as possible.  On in other words:
;
;     [a] = a / ""
;
;     a* = a* a / ""
;
; Note that the latter rule also specifies that repetition produces
; left-associated expressions.  For example, function application is
; left-associative and all operators are left-associative when they are not
; parenthesized.
;
; Additionally, try alternatives in an order that minimizes backtracking
; according to the following rule:
;
;     (a / b) (c / d) = a c / a d / b c / b d

; NOTE: There are many line endings in the wild
;
; See: https://en.wikipedia.org/wiki/Newline
;
; For simplicity this supports Unix and Windows line-endings, which are the most
; common
end-of-line =
      %x0A     ; "\n"
    / %x0D.0A  ; "\r\n"

; This rule matches all characters that are not:
;
; * not ASCII
; * not part of a surrogate pair
; * not a "non-character"
valid-non-ascii =
      %x80-D7FF
    ; %xD800-DFFF = surrogate pairs
    / %xE000-FFFD
    ; %xFFFE-FFFF = non-characters
    / %x10000-1FFFD
    ; %x1FFFE-1FFFF = non-characters
    / %x20000-2FFFD
    ; %x2FFFE-2FFFF = non-characters
    / %x30000-3FFFD
    ; %x3FFFE-3FFFF = non-characters
    / %x40000-4FFFD
    ; %x4FFFE-4FFFF = non-characters
    / %x50000-5FFFD
    ; %x5FFFE-5FFFF = non-characters
    / %x60000-6FFFD
    ; %x6FFFE-6FFFF = non-characters
    / %x70000-7FFFD
    ; %x7FFFE-7FFFF = non-characters
    / %x80000-8FFFD
    ; %x8FFFE-8FFFF = non-characters
    / %x90000-9FFFD
    ; %x9FFFE-9FFFF = non-characters
    / %xA0000-AFFFD
    ; %xAFFFE-AFFFF = non-characters
    / %xB0000-BFFFD
    ; %xBFFFE-BFFFF = non-characters
    / %xC0000-CFFFD
    ; %xCFFFE-CFFFF = non-characters
    / %xD0000-DFFFD
    ; %xDFFFE-DFFFF = non-characters
    / %xE0000-EFFFD
    ; %xEFFFE-EFFFF = non-characters
    / %xF0000-FFFFD
    ; %xFFFFE-FFFFF = non-characters
    / %x100000-10FFFD
    ; %x10FFFE-10FFFF = non-characters

tab = %x09  ; "\t"

block-comment = "{-" block-comment-continue

block-comment-char =
      %x20-7F
    / valid-non-ascii
    / tab
    / end-of-line

block-comment-continue =
    "-}"
    / block-comment block-comment-continue
    / block-comment-char block-comment-continue

not-end-of-line = %x20-7F / valid-non-ascii / tab

; NOTE: Slightly different from Haskell-style single-line comments because this
; does not require a space after the dashes
line-comment = "--" *not-end-of-line end-of-line

whitespace-chunk =
      " "
    / tab
    / end-of-line
    / line-comment
    / block-comment

whsp = *whitespace-chunk

; nonempty whitespace
whsp1 = 1*whitespace-chunk

; Uppercase or lowercase ASCII letter
ALPHA = %x41-5A / %x61-7A

; ASCII digit
DIGIT = %x30-39  ; 0-9

ALPHANUM = ALPHA / DIGIT

HEXDIG = DIGIT / "A" / "B" / "C" / "D" / "E" / "F"

; A simple label cannot be one of the reserved keywords
; listed in the `keyword` rule.
; A PEG parser could use negative lookahead to
; enforce this, e.g. as follows:
; simple-label =
;       keyword 1*simple-label-next-char
;     / !keyword (simple-label-first-char *simple-label-next-char)
simple-label-first-char = ALPHA / "_"
simple-label-next-char = ALPHANUM / "-" / "/" / "_"
simple-label = simple-label-first-char *simple-label-next-char

quoted-label-char =
      %x20-5F
        ; %x60 = '`'
    / %x61-7E

quoted-label = *quoted-label-char

; NOTE: Dhall does not support Unicode labels, mainly to minimize the potential
; for code obfuscation
label = ("`" quoted-label "`" / simple-label)

; A nonreserved-label cannot not be any of the reserved identifiers for builtins
; (unless quoted).
; Their list can be found in the `builtin` rule.
; The only place where this restriction applies is bound variables.
; A PEG parser could use negative lookahead to avoid parsing those identifiers,
; e.g. as follows:
; nonreserved-label =
;      builtin 1*simple-label-next-char
;    / !builtin label
nonreserved-label = label

; An any-label is allowed to be one of the reserved identifiers (but not a keyword).
any-label = label

; Allow specifically `Some` in record and union labels.
any-label-or-some = any-label / Some

; Dhall's double-quoted strings are similar to JSON strings (RFC7159) except:
;
; * Dhall strings support string interpolation
;
; * Dhall strings also support escaping string interpolation by adding a new
;   `\$` escape sequence
;
; * Dhall strings also allow Unicode escape sequences of the form `\u{XXX}`
double-quote-chunk =
      interpolation
      ; '\'    Beginning of escape sequence
    / %x5C double-quote-escaped
    / double-quote-char

double-quote-escaped =
      %x22                 ; '"'    quotation mark  U+0022
    / %x24                 ; '$'    dollar sign     U+0024
    / %x5C                 ; '\'    reverse solidus U+005C
    / %x2F                 ; '/'    solidus         U+002F
    / %x62                 ; 'b'    backspace       U+0008
    / %x66                 ; 'f'    form feed       U+000C
    / %x6E                 ; 'n'    line feed       U+000A
    / %x72                 ; 'r'    carriage return U+000D
    / %x74                 ; 't'    tab             U+0009
    / %x75 unicode-escape  ; 'uXXXX' / 'u{XXXX}'    U+XXXX

; Valid Unicode escape sequences are as follows:
;
; * Exactly 4 hexadecimal digits without braces:
;       `\uXXXX`
; * 1-6 hexadecimal digits within braces (with optional zero padding):
;       `\u{XXXX}`, `\u{000X}`, `\u{XXXXX}`, `\u{00000XXXXX}`, etc.
;   Any number of leading zeros are allowed within the braces preceding the 1-6
;   digits specifying the codepoint.
;
; From these sequences, the parser must also reject any codepoints that are in
; the following ranges:
;
; * Surrogate pairs: `%xD800-DFFF`
; * Non-characters: `%xNFFFE-NFFFF` / `%x10FFFE-10FFFF` for `N` in `{ 0 .. F }`
;
; See the `valid-non-ascii` rule for the exact ranges that are not allowed
unicode-escape = unbraced-escape / "{" braced-escape "}"

; All valid last 4 digits for unicode codepoints (outside Plane 0): `0000-FFFD`
unicode-suffix = (DIGIT / "A" / "B" / "C" / "D" / "E") 3HEXDIG
               / "F" 2HEXDIG (DIGIT / "A" / "B" / "C" / "D")

; All 4-hex digit unicode escape sequences that are not:
;
; * Surrogate pairs (i.e. `%xD800-DFFF`)
; * Non-characters (i.e. `%xFFFE-FFFF`)
;
unbraced-escape =
      (DIGIT / "A" / "B" / "C") 3HEXDIG
    / "D" ("0" / "1" / "2" / "3" / "4" / "5" / "6" / "7") HEXDIG HEXDIG
    ; %xD800-DFFF Surrogate pairs
    / "E" 3HEXDIG
    / "F" 2HEXDIG (DIGIT / "A" / "B" / "C" / "D")
    ; %xFFFE-FFFF Non-characters

; All 1-6 digit unicode codepoints that are not:
;
; * Surrogate pairs: `%xD800-DFFF`
; * Non-characters: `%xNFFFE-NFFFF` / `%x10FFFE-10FFFF` for `N` in `{ 0 .. F }`
;
; See the `valid-non-ascii` rule for the exact ranges that are not allowed
braced-codepoint =
      ("1" / "2" / "3" / "4" / "5" / "6" / "7" / "8" / "9" / "A" / "B" / "C" / "D" / "E" / "F" / "10") unicode-suffix; (Planes 1-16)
    / unbraced-escape ; (Plane 0)
    / 1*3HEXDIG ; %x000-FFF

; Allow zero padding for braced codepoints
braced-escape = *"0" braced-codepoint

; Printable characters except double quote and backslash
double-quote-char =
      %x20-21
        ; %x22 = '"'
    / %x23-5B
        ; %x5C = "\"
    / %x5D-7F
    / valid-non-ascii

double-quote-literal = %x22 *double-quote-chunk %x22

; NOTE: The only way to end a single-quote string literal with a single quote is
; to either interpolate the single quote, like this:
;
;     ''ABC${"'"}''
;
; ... or concatenate another string, like this:
;
;     ''ABC'' ++ "'"
;
; If you try to end the string literal with a single quote then you get "'''",
; which is interpreted as an escaped pair of single quotes
single-quote-continue =
      interpolation single-quote-continue
    / escaped-quote-pair single-quote-continue
    / escaped-interpolation single-quote-continue
    / "''" ; End of text literal
    / single-quote-char single-quote-continue

; Escape two single quotes (i.e. replace this sequence with "''")
escaped-quote-pair = "'''"

; Escape interpolation (i.e. replace this sequence with "${")
escaped-interpolation = "''${"

single-quote-char =
      %x20-7F
    / valid-non-ascii
    / tab
    / end-of-line

single-quote-literal = "''" end-of-line single-quote-continue

interpolation = "${" complete-expression "}"

text-literal = (double-quote-literal / single-quote-literal)

; RFC 5234 interprets string literals as case-insensitive and recommends using
; hex instead for case-sensitive strings
;
; If you don't feel like reading hex, these are all the same as the rule name.
; Keywords that should never be parsed as identifiers
if                    = %x69.66
then                  = %x74.68.65.6e
else                  = %x65.6c.73.65
let                   = %x6c.65.74
in                    = %x69.6e
as                    = %x61.73
using                 = %x75.73.69.6e.67
merge                 = %x6d.65.72.67.65
missing               = %x6d.69.73.73.69.6e.67
Infinity              = %x49.6e.66.69.6e.69.74.79
NaN                   = %x4e.61.4e
Some                  = %x53.6f.6d.65
toMap                 = %x74.6f.4d.61.70
assert                = %x61.73.73.65.72.74
forall-keyword        = %x66.6f.72.61.6c.6c ; "forall"
forall-symbol         = %x2200 ; Unicode FOR ALL
forall                = forall-symbol / forall-keyword
with                  = %x77.69.74.68

; Unused rule that could be used as negative lookahead in the
; `simple-label` rule for parsers that support this.
keyword =
      if / then / else
    / let / in
    / using / missing 
    / assert / as
    / Infinity / NaN
    / merge / Some / toMap
    / forall-keyword
    / with

; Note that there is a corresponding parser test in
; `tests/parser/success/builtinsA.dhall`. Please update it when
; you modify this `builtin` rule.
builtin =
      Natural-fold
    / Natural-build
    / Natural-isZero
    / Natural-even
    / Natural-odd
    / Natural-toInteger
    / Natural-show
    / Integer-toDouble
    / Integer-show
    / Integer-negate
    / Integer-clamp
    / Natural-subtract
    / Double-show
    / List-build
    / List-fold
    / List-length
    / List-head
    / List-last
    / List-indexed
    / List-reverse
    / Text-show
    / Bool
    / True
    / False
    / Optional
    / None
    / Natural
    / Integer
    / Double
    / Text
    / List
    / Type
    / Kind
    / Sort

; Reserved identifiers, needed for some special cases of parsing
Optional              = %x4f.70.74.69.6f.6e.61.6c
Text                  = %x54.65.78.74
List                  = %x4c.69.73.74
Location              = %x4c.6f.63.61.74.69.6f.6e

; Reminder of the reserved identifiers, needed for the `builtin` rule
Bool              = %x42.6f.6f.6c
True              = %x54.72.75.65
False             = %x46.61.6c.73.65
None              = %x4e.6f.6e.65
Natural           = %x4e.61.74.75.72.61.6c
Integer           = %x49.6e.74.65.67.65.72
Double            = %x44.6f.75.62.6c.65
Type              = %x54.79.70.65
Kind              = %x4b.69.6e.64
Sort              = %x53.6f.72.74
Natural-fold      = %x4e.61.74.75.72.61.6c.2f.66.6f.6c.64
Natural-build     = %x4e.61.74.75.72.61.6c.2f.62.75.69.6c.64
Natural-isZero    = %x4e.61.74.75.72.61.6c.2f.69.73.5a.65.72.6f
Natural-even      = %x4e.61.74.75.72.61.6c.2f.65.76.65.6e
Natural-odd       = %x4e.61.74.75.72.61.6c.2f.6f.64.64
Natural-toInteger = %x4e.61.74.75.72.61.6c.2f.74.6f.49.6e.74.65.67.65.72
Natural-show      = %x4e.61.74.75.72.61.6c.2f.73.68.6f.77
Natural-subtract  = %x4e.61.74.75.72.61.6c.2f.73.75.62.74.72.61.63.74
Integer-toDouble  = %x49.6e.74.65.67.65.72.2f.74.6f.44.6f.75.62.6c.65
Integer-show      = %x49.6e.74.65.67.65.72.2f.73.68.6f.77
Integer-negate    = %x49.6e.74.65.67.65.72.2f.6e.65.67.61.74.65
Integer-clamp     = %x49.6e.74.65.67.65.72.2f.63.6c.61.6d.70
Double-show       = %x44.6f.75.62.6c.65.2f.73.68.6f.77
List-build        = %x4c.69.73.74.2f.62.75.69.6c.64
List-fold         = %x4c.69.73.74.2f.66.6f.6c.64
List-length       = %x4c.69.73.74.2f.6c.65.6e.67.74.68
List-head         = %x4c.69.73.74.2f.68.65.61.64
List-last         = %x4c.69.73.74.2f.6c.61.73.74
List-indexed      = %x4c.69.73.74.2f.69.6e.64.65.78.65.64
List-reverse      = %x4c.69.73.74.2f.72.65.76.65.72.73.65
Text-show         = %x54.65.78.74.2f.73.68.6f.77

; Operators
combine       = %x2227 / "/\"
combine-types = %x2A53 / "//\\"
equivalent    = %x2261 / "==="
prefer        = %x2AFD / "//"
lambda        = %x3BB  / "\"
arrow         = %x2192 / "->"
complete      = "::"

exponent = "e" [ "+" / "-" ] 1*DIGIT

numeric-double-literal = [ "+" / "-" ] 1*DIGIT ( "." 1*DIGIT [ exponent ] / exponent)

minus-infinity-literal = "-" Infinity
plus-infinity-literal = Infinity

double-literal =
    ; "2.0"
      numeric-double-literal
    ; "-Infinity"
    / minus-infinity-literal
    ; "Infinity"
    / plus-infinity-literal
    ; "NaN"
    / NaN

natural-literal =
    ; Hexadecimal with "0x" prefix
      "0" %x78 1*HEXDIG
    ; Decimal; leading 0 digits are not allowed
    / ("1" / "2" / "3" / "4" / "5" / "6" / "7" / "8" / "9") *DIGIT
    ; ... except for 0 itself
    / "0"

integer-literal = ( "+" / "-" ) natural-literal

; If the identifier matches one of the names in the `builtin` rule, then it is a
; builtin, and should be treated as the corresponding item in the list of
; "Reserved identifiers for builtins" specified in the `standard/README.md` document.
; It is a syntax error to specify a de Bruijn index in this case.
; Otherwise, this is a variable with name and index matching the label and index.
identifier = variable / builtin

variable = nonreserved-label [ whsp "@" whsp natural-literal ]

; Printable characters other than " ()[]{}<>/\,"
;
; Excluding those characters ensures that paths don't have to end with trailing
; whitespace most of the time
path-character =
        ; %x20 = " "
      %x21
        ; %x22 = "\""
        ; %x23 = "#"
    / %x24-27
        ; %x28 = "("
        ; %x29 = ")"
    / %x2A-2B
        ; %x2C = ","
    / %x2D-2E
        ; %x2F = "/"
    / %x30-3B
        ; %x3C = "<"
    / %x3D
        ; %x3E = ">"
        ; %x3F = "?"
    / %x40-5A
        ; %x5B = "["
        ; %x5C = "\"
        ; %x5D = "]"
    / %x5E-7A
        ; %x7B = "{"
    / %x7C
        ; %x7D = "}"
    / %x7E

quoted-path-character =
      %x20-21
        ; %x22 = "\""
    / %x23-2E
        ; %x2F = "/"
    / %x30-7F
    / valid-non-ascii

unquoted-path-component = 1*path-character
quoted-path-component = 1*quoted-path-character

path-component = "/" ( unquoted-path-component / %x22 quoted-path-component %x22 )

; The last path-component matched by this rule is referred to as "file" in the semantics,
; and the other path-components as "directory".
path = 1*path-component

local =
    parent-path
    / here-path
    / home-path
    ; NOTE: Backtrack if parsing this alternative fails
    ;
    ; This is because the first character of this alternative will be "/", but
    ; if the second character is "/" or "\" then this should have been parsed
    ; as an operator instead of a path
    / absolute-path

parent-path = ".." path  ; Relative path
here-path = "."  path  ; Relative path
home-path = "~"  path  ; Home-anchored path
absolute-path = path  ; Absolute path

; `http[s]` URI grammar based on RFC7230 and RFC 3986 with some differences
; noted below

scheme = %x68.74.74.70 [ %x73 ]  ; "http" [ "s" ]

; NOTE: This does not match the official grammar for a URI.  Specifically:
;
; * this does not support fragment identifiers, which have no meaning within
;   Dhall expressions and do not affect import resolution
; * the characters "(" ")" and "," are not included in the `sub-delims` rule:
;   in particular, these characters can't be used in authority, path or query
;   strings.  This is because those characters have other meaning in Dhall
;   and it would be confusing for the comma in
;       [http://example.com/foo, bar]
;   to be part of the URL instead of part of the list.  If you need a URL
;   which contains parens or a comma, you must percent-encode them.
;
; Reserved characters in quoted path components should be percent-encoded
; according to https://tools.ietf.org/html/rfc3986#section-2
http-raw = scheme "://" authority path-abempty [ "?" query ]

path-abempty = *( "/" segment )

; NOTE: Backtrack if parsing the optional user info prefix fails
authority = [ userinfo "@" ] host [ ":" port ]

userinfo = *( unreserved / pct-encoded / sub-delims / ":" )

host = IP-literal / IPv4address / domain

port = *DIGIT

IP-literal = "[" ( IPv6address / IPvFuture  ) "]"

IPvFuture = "v" 1*HEXDIG "." 1*( unreserved / sub-delims / ":" )

; NOTE: Backtrack when parsing each alternative
IPv6address =                            6( h16 ":" ) ls32
            /                       "::" 5( h16 ":" ) ls32
            / [ h16               ] "::" 4( h16 ":" ) ls32
            / [ h16 *1( ":" h16 ) ] "::" 3( h16 ":" ) ls32
            / [ h16 *2( ":" h16 ) ] "::" 2( h16 ":" ) ls32
            / [ h16 *3( ":" h16 ) ] "::"    h16 ":"   ls32
            / [ h16 *4( ":" h16 ) ] "::"              ls32
            / [ h16 *5( ":" h16 ) ] "::"              h16
            / [ h16 *6( ":" h16 ) ] "::"

h16 = 1*4HEXDIG

ls32 = h16 ":" h16 / IPv4address

IPv4address = dec-octet "." dec-octet "." dec-octet "." dec-octet

; NOTE: Backtrack when parsing these alternatives
dec-octet = "25" %x30-35       ; 250-255
          / "2" %x30-34 DIGIT  ; 200-249
          / "1" 2DIGIT         ; 100-199
          / %x31-39 DIGIT      ; 10-99
          / DIGIT              ; 0-9

; Look in RFC3986 3.2.2 for
; "A registered name intended for lookup in the DNS"
domain = domainlabel *("." domainlabel) [ "." ]

domainlabel = 1*ALPHANUM *(1*"-" 1*ALPHANUM)

segment = *pchar

pchar = unreserved / pct-encoded / sub-delims / ":" / "@"

query = *( pchar / "/" / "?" )

pct-encoded = "%" HEXDIG HEXDIG

unreserved  = ALPHANUM / "-" / "." / "_" / "~"

; this is the RFC3986 sub-delims rule, without "(", ")" or ","
; see comments above the `http-raw` rule above
sub-delims = "!" / "$" / "&" / "'" / "*" / "+" / ";" / "="

http = http-raw [ whsp using whsp1 import-expression ]

; Dhall supports unquoted environment variables that are Bash-compliant or
; quoted environment variables that are POSIX-compliant
env = "env:"
    ( bash-environment-variable
    / %x22 posix-environment-variable %x22
    )

; Bash supports a restricted subset of POSIX environment variables.  From the
; Bash `man` page, an environment variable name is:
;
; > A word consisting only of  alphanumeric  characters  and  under-scores,  and
; > beginning with an alphabetic character or an under-score
bash-environment-variable = (ALPHA / "_") *(ALPHANUM / "_")

; The POSIX standard is significantly more flexible about legal environment
; variable names, which can contain alerts (i.e. '\a'), whitespace, or
; punctuation, for example.  The POSIX standard says about environment variable
; names:
;
; > The value of an environment variable is a string of characters. For a
; > C-language program, an array of strings called the environment shall be made
; > available when a process begins. The array is pointed to by the external
; > variable environ, which is defined as:
; >
; >     extern char **environ;
; >
; > These strings have the form name=value; names shall not contain the
; > character '='. For values to be portable across systems conforming to IEEE
; > Std 1003.1-2001, the value shall be composed of characters from the portable
; > character set (except NUL and as indicated below).
;
; Note that the standard does not explicitly state that the name must have at
; least one character, but `env` does not appear to support this and `env`
; claims to be POSIX-compliant.  To be safe, Dhall requires at least one
; character like `env`
posix-environment-variable = 1*posix-environment-variable-character

; These are all the characters from the POSIX Portable Character Set except for
; '\0' (NUL) and '='.  Note that the POSIX standard does not explicitly state
; that environment variable names cannot have NUL.  However, this is implicit
; in the fact that environment variables are passed to the program as
; NUL-terminated `name=value` strings, which implies that the `name` portion of
; the string cannot have NUL characters
posix-environment-variable-character =
      %x5C                 ; '\'    Beginning of escape sequence
      ( %x22               ; '"'    quotation mark  U+0022
      / %x5C               ; '\'    reverse solidus U+005C
      / %x61               ; 'a'    alert           U+0007
      / %x62               ; 'b'    backspace       U+0008
      / %x66               ; 'f'    form feed       U+000C
      / %x6E               ; 'n'    line feed       U+000A
      / %x72               ; 'r'    carriage return U+000D
      / %x74               ; 't'    tab             U+0009
      / %x76               ; 'v'    vertical tab    U+000B
      )
    ; Printable characters except double quote, backslash and equals
    / %x20-21
        ; %x22 = '"'
    / %x23-3C
        ; %x3D = '='
    / %x3E-5B
        ; %x5C = "\"
    / %x5D-7E

import-type = missing / local / http / env

hash = %x73.68.61.32.35.36.3a 64HEXDIG ; "sha256:XXX...XXX"

import-hashed = import-type [ whsp1 hash ]

; "http://example.com"
; "./foo/bar"
; "env:FOO"
import = import-hashed [ whsp as whsp1 (Text / Location) ]

expression =
    ; "\(x : a) -> b"
      lambda whsp "(" whsp nonreserved-label whsp ":" whsp1 expression whsp ")" whsp arrow whsp expression
    
    ; "if a then b else c"
    / if whsp1 expression whsp then whsp1 expression whsp else whsp1 expression
    
    ; "let x : t = e1 in e2"
    ; "let x     = e1 in e2"
    ; We allow dropping the `in` between adjacent let-expressions; the following are equivalent:
    ; "let x = e1 let y = e2 in e3"
    ; "let x = e1 in let y = e2 in e3"
    / 1*let-binding in whsp1 expression
    
    ; "forall (x : a) -> b"
    / forall whsp "(" whsp nonreserved-label whsp ":" whsp1 expression whsp ")" whsp arrow whsp expression
    
    ; "a -> b"
    ;
    ; NOTE: Backtrack if parsing this alternative fails
    / operator-expression whsp arrow whsp expression
    
    ; "a with x = b"
    ;
    ; NOTE: Backtrack if parsing this alternative fails
    / with-expression
    
    ; "merge e1 e2 : t"
    ;
    ; NOTE: Backtrack if parsing this alternative fails since we can't tell
    ; from the keyword whether there will be a type annotation or not
    / merge whsp1 import-expression whsp1 import-expression whsp ":" whsp1 application-expression
    
    ; "[] : t"
    ;
    ; NOTE: Backtrack if parsing this alternative fails since we can't tell
    ; from the opening bracket whether or not this will be an empty list or
    ; a non-empty list
    / empty-list-literal
    
    ; "toMap e : t"
    ;
    ; NOTE: Backtrack if parsing this alternative fails since we can't tell
    ; from the keyword whether there will be a type annotation or not
    / toMap whsp1 import-expression whsp ":" whsp1 application-expression
    
    ; "assert : Natural/even 1 === False"
    / assert whsp ":" whsp1 expression
    
    ; "x : t"
    / annotated-expression

; Nonempty-whitespace to disambiguate `env:VARIABLE` from type annotations
annotated-expression = operator-expression [ whsp ":" whsp1 expression ]

; "let x = e1"
let-binding = let whsp1 nonreserved-label whsp [ ":" whsp1 expression whsp ] "=" whsp expression whsp

; "[] : t"
empty-list-literal =
    "[" whsp [ "," whsp ] "]" whsp ":" whsp1 application-expression

with-expression =
    import-expression 1*(whsp1 with whsp1 with-clause)

with-clause =
    any-label-or-some *(whsp "." whsp any-label-or-some) whsp "=" whsp operator-expression

operator-expression = equivalent-expression

; Nonempty-whitespace to disambiguate `http://a/a?a`
equivalent-expression    = import-alt-expression    *(whsp equivalent whsp import-alt-expression)
import-alt-expression    = or-expression            *(whsp "?" whsp1 or-expression)
or-expression            = plus-expression          *(whsp "||" whsp plus-expression)
; Nonempty-whitespace to disambiguate `f +2`
plus-expression          = text-append-expression   *(whsp "+" whsp1 text-append-expression)
text-append-expression   = list-append-expression   *(whsp "++" whsp list-append-expression)
list-append-expression   = and-expression           *(whsp "#" whsp and-expression)
and-expression           = combine-expression       *(whsp "&&" whsp combine-expression)
combine-expression       = prefer-expression        *(whsp combine whsp prefer-expression)
prefer-expression        = combine-types-expression *(whsp prefer whsp combine-types-expression)
combine-types-expression = times-expression         *(whsp combine-types whsp times-expression)
times-expression         = equal-expression         *(whsp "*" whsp equal-expression)
equal-expression         = not-equal-expression     *(whsp "==" whsp not-equal-expression)
not-equal-expression     = application-expression   *(whsp "!=" whsp application-expression)


; Import expressions need to be separated by some whitespace, otherwise there
; would be ambiguity: `./ab` could be interpreted as "import the file `./ab`",
; or "apply the import `./a` to label `b`"
application-expression =
    first-application-expression *(whsp1 import-expression)

first-application-expression =
    ; "merge e1 e2"
      merge whsp1 import-expression whsp1 import-expression
    
    ; "Some e"
    / Some whsp1 import-expression
    
    ; "toMap e"
    / toMap whsp1 import-expression
    
    / import-expression

import-expression = import / completion-expression

completion-expression =
    selector-expression [ whsp complete whsp selector-expression ]

; `record.field` extracts one field of a record
;
; `record.{ field0, field1, field2 }` projects out several fields of a record
;
; NOTE: Backtrack when parsing the `*("." ...)`.  The reason why is that you
; can't tell from parsing just the period whether "foo." will become "foo.bar"
; (i.e. accessing field `bar` of the record `foo`) or `foo./bar` (i.e. applying
; the function `foo` to the relative path `./bar`)
selector-expression = primitive-expression *(whsp "." whsp selector)

selector = any-label / labels / type-selector

labels = "{" whsp [ any-label-or-some whsp *("," whsp any-label-or-some whsp) ] "}"

type-selector = "(" whsp expression whsp ")"
; NOTE: Backtrack when parsing the first three alternatives (i.e. the numeric
; literals).  This is because they share leading characters in common
primitive-expression =
    ; "2.0"
      double-literal
    
    ; "2"
    / natural-literal
    
    ; "+2"
    / integer-literal
    
    ; '"ABC"'
    / text-literal
    
    ; "{ foo = 1      , bar = True }"
    ; "{ foo : Integer, bar : Bool }"
    / "{" whsp [ "," whsp ] record-type-or-literal whsp "}"
    
    ; "< Foo : Integer | Bar : Bool >"
    ; "< Foo | Bar : Bool >"
    / "<" whsp [ "|" whsp ] union-type whsp ">"
    
    ; "[1, 2, 3]"
    / non-empty-list-literal
    
    ; "x"
    ; "x@2"
    / identifier
    
    ; "( e )"
    / "(" complete-expression ")"


record-type-or-literal =
      empty-record-literal
    / [non-empty-record-type-or-literal]

empty-record-literal = "="

non-empty-record-type-or-literal =
    (non-empty-record-type / non-empty-record-literal)

non-empty-record-type =
    record-type-entry *(whsp "," whsp record-type-entry)

record-type-entry = any-label-or-some whsp ":" whsp1 expression

non-empty-record-literal =
    record-literal-entry *(whsp "," whsp record-literal-entry)

; If the `record-literal-normal-entry` is absent, that represents a punned
; record entry, such as in `{ x }`, which is a short-hand for `{ x = x }`
record-literal-entry =
    any-label-or-some [record-literal-normal-entry]

record-literal-normal-entry =
    *(whsp "." whsp any-label-or-some) whsp "=" whsp expression

; If the `union-type-entry` is absent, that represents an empty union
; alternative, such as in `< Heads | Tails >`
union-type =
    [union-type-entry *(whsp "|" whsp union-type-entry)]

; x : Natural
; x
union-type-entry = any-label-or-some [ whsp ":" whsp1 expression ]


non-empty-list-literal =
    "[" whsp [ "," whsp ] expression whsp *("," whsp expression whsp) "]"

; This just adds surrounding whitespace for the top-level of the program
complete-expression = whsp expression whsp

A src/dhall.nim => src/dhall.nim +30 -0
@@ 0,0 1,30 @@
import ./dhall/normalization, ./dhall/parse, ./dhall/resolution, ./dhall/terms

export normalization.eval
export parse.parseDhall

import std/asyncfutures, std/strutils, std/os, std/uri

proc newTerm(path: string): Term =
  result = Term(kind: tImport,
    importKind: iCode,
    importScheme: iHere,
    importElements: path.normalizedPath.split('/'))
  if path.isAbsolute:
    result.importScheme = iAbs
    result.importElements =
      result.importElements[1..result.importElements.high]

proc importDhall*(path: string): Future[Term] =
  path.newTerm.resolve

proc importDhall*(uri: Uri): Future[Term] =
  uri.newTerm.resolve

proc text*(v: Value): string =
  ## Extract a text string from Dhall value ``v``.
  ## If ``v`` is not a fully normalized text literal
  ## then a ``TypeError`` exception will be raised.
  if not v.isSimpleText:
    raise newException(TypeError, "not a normalized text value")
  v.textSuffix

M src/dhall/binary.nim => src/dhall/binary.nim +135 -95
@@ 1,78 1,84 @@
import ./term

export term.`==`
import ./quotation, ./terms

import cbor, cbor/bignum, bigints

import std/algorithm, std/math, std/options, std/streams, std/tables

const httpSchemes = {iHttp, iHttps}

proc writeCbor*(s: Stream; t: Term)

proc `%`*(k: TermKind): CborNode = %BiggestUint(k)

proc `%`*(t: Term): CborNode = initCborOther t

proc writeCbor*(s: Stream; table: Table[string, Term]) =
proc writeCbor*(s: Stream; table: Table[string, Node]) =
  var keys = newSeqOfCap[string](table.len)
  for k in table.keys:
    keys.add k
  sort(keys)
  s.writeMapLen(keys.len)
  s.writeCborMapLen(keys.len)
  for k in keys:
    s.writeCbor(k)
    s.writeCbor(table[k])

proc writeCbor*(s: Stream; tk: TermKind) {.inline.} = s.writeCbor(tk.ord)

proc writeApp(s: Stream; t: Term; depth: Natural) =
  if t.kind == tApp:
    s.writeApp(t.appFun, depth+1)
    s.writeCbor(t.appArg)
  else:
    s.writeCborArrayLen(2+depth)
    s.writeCbor(tApp)
    s.writeCbor(t)
      # now unwind

proc writeCbor*(s: Stream; t: Term) =
  # TODO: macro this stuff
  template wr(x: untyped) = writeCbor(s, x)
  template wrL(n: Natural) = writeArrayLen(s, n)
  template wrL(n: Natural) = writeCborArrayLen(s, n)
  if t.isNil:
    wr(%nil.pointer)
    return
  case t.kind
  of tVar:
  of tVar, tFreeVar, tLocalVar, tQuoteVar:
    # TODO: only one should be valid here
    if t.varName == "_":
      wr t.varIndex
    else:
      s.writeArrayLen 2
      s.writeCborArrayLen 2
      wr t.varName
      wr t.varIndex
  of tUniverse:
    wr $t.universe
  of tBuiltin:
    assert(t.builtinArgs == @[])
    wr $t.builtin
  of tApp:
    wrL(2 + t.appArgs.len)
    wr t.kind
    wr t.appFun
    for arg in t.appArgs:
      wr arg
    s.writeApp(t, 0)
  of tLambda:
    if t.lambdaLabel == "_":
    if t.funcLabel == "_":
      wrL 3
      wr t.kind
      wr t.lambdaType
      wr t.lambdaBody
      wr t.funcType
      wr t.funcBody
    else:
      wrL 4
      wr t.kind
      wr t.lambdaLabel
      wr t.lambdaType
      wr t.lambdaBody
      wr t.funcLabel
      wr t.funcType
      wr t.funcBody
  of tPi:
    if t.piLabel == "_":
    if t.funcLabel == "_":
      wrL 3
      wr t.kind
      wr t.piType
      wr t.piBody
      wr t.funcType
      wr t.funcBody
    else:
      wrL 4
      wr t.kind
      wr t.piLabel
      wr t.piType
      wr t.piBody
      wr t.funcLabel
      wr t.funcType
      wr t.funcBody
  of tOp:
    wrL 4
    wr t.kind


@@ 83,7 89,7 @@ proc writeCbor*(s: Stream; t: Term) =
    wrL(2+t.list.len)
    wr t.kind
    if t.list.len == 0:
      wr t.listType
      wr t.listType.get
    else:
      wr %nil.pointer
      for x in t.list:


@@ 91,13 97,13 @@ proc writeCbor*(s: Stream; t: Term) =
  of tSome:
    wrL 3
    wr t.kind
    if t.someType.isNil:
    if t.someType.isNone:
      wr %nil.pointer
    else:
      wr t.someType
      wr t.someType.get
    wr t.someVal
  of tMerge:
    if t.mergeAnn.isNil:
    if t.mergeAnn.isNone:
      wrL 3
      wr t.kind
      wr t.mergeHandler


@@ 107,15 113,11 @@ proc writeCbor*(s: Stream; t: Term) =
      wr t.kind
      wr t.mergeHandler
      wr t.mergeUnion
      wr t.mergeAnn
  of tRecordType:
    wrL 2
    wr t.kind
    wr t.recordType
  of tRecordLiteral:
      wr t.mergeAnn.get
  of tRecordType, tRecordLiteral:
    wrL 2
    wr t.kind
    wr t.recordLiteral
    wr t.table
  of tField:
    wrL 3
    wr t.kind


@@ 136,7 138,7 @@ proc writeCbor*(s: Stream; t: Term) =
  of tUnionType:
    wrL 2
    wr t.kind
    wr t.union
    wr t.table
  of tBoolLiteral:
    wr t.bool
  of tIf:


@@ 168,16 170,16 @@ proc writeCbor*(s: Stream; t: Term) =
    wr t.assertAnn
  of tImport:
    let check = if t.importCheck == @[]: %nil.pointer
      else: %t.importCheck
    var tmp = %[%t.kind, check, %t.importKind.uint8, %t.importScheme]
    if t.importScheme in {0, 1}:
      if t.importHeaders.isNil:
      else: %(@[0x12'u8, 0x20'u8] & t.importCheck)
    var tmp = %[%t.kind, check, %t.importKind.uint8, %t.importScheme.uint8]
    if t.importScheme in httpSchemes:
      if t.importHeaders.isNone:
        tmp.seq.add(%nil.pointer)
      else:
        tmp.seq.add(%t.importHeaders)
        tmp.seq.add(%t.importHeaders.get)
    for i, elem in t.importElements:
      tmp.seq.add(%elem)
    if t.importScheme in {0, 1}:
    if t.importScheme in httpSchemes:
      if t.importQuery.isSome:
        tmp.seq.add(%t.importQuery.get)
      else:


@@ 187,12 189,12 @@ proc writeCbor*(s: Stream; t: Term) =
    wrL(2+t.letBinds.len*3)
    wr t.kind
    for b in t.letBinds:
      wr b.key
      if b.ann.isNil:
      wr b.letKey
      if b.letAnn.isNone:
        wr %nil.pointer
      else:
        wr b.ann
      wr b.val
        wr b.letAnn.get
      wr b.letVal
    wr t.letBody
  of tAnnotation:
    wrL 3


@@ 200,7 202,7 @@ proc writeCbor*(s: Stream; t: Term) =
    wr t.annExpr
    wr t.annAnn
  of tToMap:
    if t.toMapAnn.isNil:
    if t.toMapAnn.isNone:
      wrL 2
      wr t.kind
      wr t.toMapBody


@@ 208,20 210,29 @@ proc writeCbor*(s: Stream; t: Term) =
      wrL 3
      wr t.kind
      wr t.toMapBody
      wr t.toMapAnn
      wr t.toMapAnn.get
  of tEmptyList:
    wrL 2
    wr t.kind
    wr t.emptyListType
  of tWith:
    wrL 4
    wr t.kind
    wr t.withExpr
    wr t.withFields
    wr t.withUpdate
  else:
    assert(false, $t.kind & " escaped from parser")

proc encode*(expr: Term): string =
proc writeCbor*(s: Stream; v: Value) =
  writeCbor(s, quote(v))

proc encode*(t: Term): string {.gcsafe.} =
  let str = newStringStream()
  str.writeCbor(expr)
  str.writeCbor(t)
  str.data

proc parseAssert(check: bool; msg = "invalid Dhall encoding") {.inline.} =
func parseAssert(check: bool; msg = "invalid Dhall encoding") {.inline.} =
  if not check: raise newException(CborParseError, msg)

proc nextBytesOrNil(c: var CborParser): seq[byte] =


@@ 244,7 255,7 @@ proc nextTextOrNil(c: var CborParser): string =
  else:
    parseAssert(false)

proc nextTerm(parser: var CborParser): Term
proc nextTerm(parser: var CborParser): Term {.gcsafe.}

proc nextTable(parser: var CborParser): Table[string, Term] =
  let tableLen = parser.mapLen()


@@ 273,32 284,33 @@ proc nextTerm(parser: var CborParser): Term =
      of tApp:
        parseAssert(arrayLen > 2)
        let argsLen = arrayLen - 2
        result = Term(kind: kind, appFun: parser.nextTerm(),
            appArgs: newSeq[Term](argsLen))
        for m in result.appArgs.mitems:
          m = parser.nextTerm()
        result = parser.nextTerm()
        for _ in 1..argsLen:
          result = Term(kind: kind,
              appFun: result,
              appArg: parser.nextTerm())

      of tLambda:
        case arrayLen:
        of 3:
          result = Term(kind: kind, lambdaLabel: "_",
              lambdaType: parser.nextTerm(), lambdaBody: parser.nextTerm())
          result = Term(kind: kind, funcLabel: "_",
              funcType: parser.nextTerm(), funcBody: parser.nextTerm())
        of 4:
          result = Term(kind: kind, lambdaLabel: parser.nextText(),
              lambdaType: parser.nextTerm(), lambdaBody: parser.nextTerm())
          parseAssert(result.lambdaLabel != "_")
          result = Term(kind: kind, funcLabel: parser.nextText(),
              funcType: parser.nextTerm(), funcBody: parser.nextTerm())
          parseAssert(result.funcLabel != "_")
        else:
          parseAssert(false)

      of tPi:
        case arrayLen:
        of 3:
          result = Term(kind: kind, piLabel: "_", piType: parser.nextTerm(),
              piBody: parser.nextTerm())
          result = Term(kind: kind, funcLabel: "_", funcType: parser.nextTerm(),
              funcBody: parser.nextTerm())
        of 4:
          result = Term(kind: kind, piLabel: parser.nextText(),
              piType: parser.nextTerm(), piBody: parser.nextTerm())
          parseAssert(result.piLabel != "_")
          result = Term(kind: kind, funcLabel: parser.nextText(),
              funcType: parser.nextTerm(), funcBody: parser.nextTerm())
          parseAssert(result.funcLabel != "_")
        else:
          parseAssert(false)



@@ 306,20 318,25 @@ proc nextTerm(parser: var CborParser): Term =
        parseAssert(arrayLen == 4)
        let op = parser.nextInt()
        parseAssert(op <= high(OpKind).BiggestInt)
        result = Term(kind: kind, op: op.OpKind, opL: parser.nextTerm(), opR: parser.nextTerm())
        result = Term(kind: kind, op: op.OpKind,
            opL: parser.nextTerm(),
            opR: parser.nextTerm())

      of tList:
        parseAssert(arrayLen >= 2)
        result = Term(kind: kind, list: newSeq[Term](arrayLen-2), listType: parser.nextTerm())
        result = Term(kind: kind,
            list: newSeq[Term](arrayLen-2),
            listType: option parser.nextTerm())
        for m in result.list.mitems:
          m = parser.nextTerm()
        parseAssert(
          (result.listType.isNil and result.list.len > 0) or
          (not result.listType.isNil and result.list.len == 0))
          (result.listType.isNone and result.list.len > 0) or
          (not result.listType.isNone and result.list.len == 0))

      of tSome:
        parseAssert(arrayLen == 3)
        result = Term(kind: kind, someType: parser.nextTerm(),
        result = Term(kind: kind,
            someType: option parser.nextTerm(),
            someVal: parser.nextTerm())

      of tMerge:


@@ 329,17 346,18 @@ proc nextTerm(parser: var CborParser): Term =
              mergeUnion: parser.nextTerm())
        of 4:
          result = Term(kind: kind, mergeHandler: parser.nextTerm(),
              mergeUnion: parser.nextTerm(), mergeAnn: parser.nextTerm())
              mergeUnion: parser.nextTerm(),
              mergeAnn: option parser.nextTerm())
        else:
          parseAssert(false)

      of tRecordType:
        parseAssert(arrayLen == 2)
        result = Term(kind: kind, recordType: parser.nextTable())
        result = Term(kind: kind, table: parser.nextTable())

      of tRecordLiteral:
        parseAssert(arrayLen == 2)
        result = Term(kind: kind, recordLiteral: parser.nextTable())
        result = Term(kind: kind, table: parser.nextTable())

      of tField:
        parseAssert(arrayLen == 3)


@@ 364,7 382,7 @@ proc nextTerm(parser: var CborParser): Term =

      of tUnionType:
        parseAssert(arrayLen == 2)
        result = Term(kind: kind, union: parser.nextTable())
        result = Term(kind: kind, table: parser.nextTable())

      of tIf:
        parseAssert(arrayLen == 4)


@@ 396,20 414,27 @@ proc nextTerm(parser: var CborParser): Term =

      of tImport:
        parseAssert(arrayLen >= 3)
        result = Term(kind: kind, importCheck: parser.nextBytesOrNil(),
        var check = parser.nextBytesOrNil()
        if check != @[]:
          parseAssert(
            check.len == 34 and
            check[0] == 0x12 and
            check[1] == 0x20)
          check = check[2..33]
        result = Term(kind: kind, importCheck: check,
            importKind: parser.nextInt().ImportKind,
            importScheme: parser.nextInt().uint8,
            importScheme: parser.nextInt().ImportScheme,
            importQuery: none(string))
        if result.importScheme in {0, 1}:
          result.importHeaders = parser.nextTerm()
        if result.importScheme in httpSchemes:
          result.importHeaders = option parser.nextTerm()
          result.importElements = newSeq[string](arrayLen - 6)
          for m in result.importElements.mitems:
            m = parser.nextText()
          if parser.kind == CborEventKind.cborText:
            result.importQuery = some parser.nextText()
            result.importQuery = option parser.nextText()
          else:
            doAssert(isNull parser.nextNode())
        elif result.importScheme == 7:
        elif result.importScheme == iMiss:
          discard
        else:
          result.importElements = newSeq[string](arrayLen - 4)


@@ 421,10 446,10 @@ proc nextTerm(parser: var CborParser): Term =
        let bindsLen = (arrayLen - 2) div 3
        result = Term(kind: kind, letBinds: newSeq[Term](bindsLen))
        for m in result.letBinds.mitems:
          m = Term(kind: tBinding,
              key: parser.nextText(),
              ann: parser.nextTerm(),
              val: parser.nextTerm())
          m = Term(kind: tLetBinding,
              letKey: parser.nextText(),
              letAnn: option parser.nextTerm(),
              letVal: parser.nextTerm())
        result.letBody = parser.nextTerm()

      of tAnnotation:


@@ 437,8 462,9 @@ proc nextTerm(parser: var CborParser): Term =
        of 2:
          result = Term(kind: kind, toMapBody: parser.nextTerm())
        of 3:
          result = Term(kind: kind, toMapBody: parser.nextTerm(),
              toMapAnn: parser.nextTerm())
          result = Term(kind: kind,
              toMapBody: parser.nextTerm(),
              toMapAnn: option parser.nextTerm())
        else:
          parseAssert(false)



@@ 446,6 472,20 @@ proc nextTerm(parser: var CborParser): Term =
        parseAssert(arrayLen == 2)
        result = Term(kind: kind, emptyListType: parser.nextTerm())

      of tWith:
        parseAssert(arrayLen == 4)
        let expr = parser.nextTerm()
        var fields = newSeq[string](parser.arrayLen)
        parser.next()
        for f in fields.mitems:
          f = parser.nextText()
          # TODO: are these all Variables?
        let update = parser.nextTerm()
        result = Term(kind: kind,
          withExpr: expr,
          withFields: fields,
          withUpdate: update)

      else:
        parseAssert(false)



@@ 478,16 518,16 @@ proc nextTerm(parser: var CborParser): Term =
  else:
    parseAssert(false)

proc decode*(str: Stream): Term =
proc decodeDhall*(str: Stream): Term =
  var parser: CborParser
  parser.open(str)
  parser.next()
  parser.nextTerm()

proc decode*(buf: string): Term =
  buf.newStringStream.decode
proc decodeDhall*(buf: string): Term =
  buf.newStringStream.decodeDhall

proc decodeFile*(path: string): Term =
proc decodeDhallFile*(path: string): Term =
  let str = newFileStream(path)
  defer: close str
  decode str
  decodeDhall str

A src/dhall/normalization.nim => src/dhall/normalization.nim +788 -0
@@ 0,0 1,788 @@
import ./quotation, ./render, ./terms

import bigints

import std/algorithm, std/asyncfutures, std/hashes,
    std/math, std/options, std/strutils,
    std/tables, std/unicode

const zero = initBigInt(0)

type
  ImportError* = object of ValueError
  TypeError* = object of ValueError

func toBiggestFloat(a: BigInt): BiggestFloat =
  for i in countdown(a.limbs.high, 0):
    result = result * BiggestFloat(1 shl 32) + a.limbs[i].BiggestFloat
  if Negative in a.flags:
    result = - result

func addEscaped(result: var string; s: string) =
  for r in s.runes:
    case r
    of Rune '"': result.add "\\\""
    of Rune '$': result.add "\\u0024"
    of Rune '\\': result.add "\\\\"
    of Rune '\b': result.add "\\b"
    of Rune '\f': result.add "\\f"
    of Rune '\n': result.add "\\n"
    of Rune '\r': result.add "\\r"
    of RUne '\t': result.add "\\t"
    else:
      if r <=% Rune(0x1f):
        result.add("\\u")
        result.add(r.int.toHex(4))
      else: result.add r

type Env* = Table[string, seq[Value]]

func eval*(env: Env; t: Term): Value {.gcsafe.}

func eval*(t: Term): Value =
  let env = initTable[string, seq[Value]]()
  env.eval(t)

func toBeta*(expr: Term): Value =
  ## β-normalization.
  assert(not expr.isNil)
  result = eval(expr)
  while result.isFuture:
    result = result.future.read

func toAlpha*(expr: Value): Term =
  ## α-normalization.
  quote(expr, alpha)

func cramText(v: Value): Value =
  ## Reduce a text literal to the mimimum amount of chunks.
  if v.textChunks == @[]:
    result = v
  else:
    var
      chunks = newSeqOfCap[Value](v.textChunks.len)
      tmp: string
    for tc in v.textChunks.mitems:
      tmp.add tc.textPrefix
      if not tc.textExpr.isNil:
        if tc.textExpr.isTextLiteral:
          for tctc in tc.textExpr.textChunks:
            tmp.add tctc.textPrefix
            chunks.add Value(kind: tTextChunk, textPrefix: move tmp,
                textExpr: tctc.textExpr)
          tmp.add tc.textExpr.textSuffix
        else:
          chunks.add Value(kind: tTextChunk,
              textPrefix: move tmp, textExpr: tc.textExpr)
    tmp.add v.textSuffix
    if tmp == "" and chunks.len == 1 and chunks[0].textPrefix == "":
      result = chunks[0].textExpr
    else:
      result = Value(kind: tTextLiteral,
          textChunks: chunks, textSuffix: move tmp)

func newApp(b: BuiltinKind; args: varargs[Value]): Value =
  result = newValue(b)
  for arg in args:
    result = Value(kind: tApp, appFun: result, appArg: arg)

func operate(env: Env; op: OpKind; opL, opR: Value): Value =
  case op
  of opBoolOr:
    if opL == opR:
      result = opL
    if opL.kind == tBoolLiteral:
      result = if opL.bool: opL else: opR
    if opR.kind == tBoolLiteral:
      result = if opR.bool: opR else: opL
  of opBoolAnd:
    if opL == opR:
      result = opL
    if opL.kind == tBoolLiteral:
      result = if opL.bool: opR else: opL
    if opR.kind == tBoolLiteral:
      result = if opR.bool: opL else: opR
  of opBoolEquality:
    if opL.kind == tBoolLiteral and opR.kind == tBoolLiteral:
      result = Value(kind: tBoolLiteral, bool: opL.bool == opR.bool)
    elif opL.isBool and opL.bool:
      result = opR
    elif opR.isBool and opR.bool:
      result = opL
    elif opR == opL:
      result = Value(kind: tBoolLiteral, bool: true)
  of opBoolInequality:
    if opL.kind == tBoolLiteral and opR.kind == tBoolLiteral:
      result = Value(kind: tBoolLiteral,
          bool: opL.bool != opR.bool)
    elif opL.isBool and not opL.bool:
      result = opR
    elif opR.isBool and not opR.bool:
      result = opL
    elif opR == opL:
      result = Value(kind: tBoolLiteral, bool: false)
  of opNaturalAdd:
    if opL.isNatural and opL.natural == 0:
      result = opR
    elif opR.isNatural and opR.natural == 0:
      result = opL
    elif opR.isNatural and opL.isNatural:
      result = Value(kind: tNaturalLiteral, natural: opL.natural + opR.natural)
  of opNaturalMultiplication:
    if (opL.isNatural and opL.natural == 0) or
        (opR.isNatural and opR.natural == 0):
      result = Value(kind: tNaturalLiteral, natural: initBigInt 0)
    elif opL.isNatural and opL.natural == 1:
      result = opR
    elif opR.isNatural and opR.natural == 1:
      result = opL
    elif opL.isNatural and opR.isNatural:
      result = Value(kind: tNaturalLiteral, natural: opL.natural * opR.natural)
  of opListAppend:
    if opL.kind == tEmptyList or (opL.kind == tList and opL.list == @[]):
      result = opR
    elif opR.kind == tEmptyList or (opR.kind == tList and opR.list == @[]):
      result = opL
    elif opL.isList and opR.isList:
      result = Value(kind: tList,
        listType: opL.listType,
        list: opL.list & opR.list)
  of opRecordRecursiveMerge:
    if opL.isRecordLiteral and opL.table.len == 0:
      result = opR
    elif opR.isRecordLiteral and opR.table.len == 0:
      result = opL
    elif opL.isRecordLiteral and opR.isRecordLiteral:
      result = opL
      for key, val in opR.table.pairs:
        if result.table.hasKeyOrPut(key, val):
          result.table.withValue(key, other):
            let e = operate(env, opRecordRecursiveMerge, other[], val)
            other[] = eval(env, e.quote)
              # TODO: looks expensive
  of opRecordBiasedMerge:
    if opL.isRecordLiteral and opL.table.len == 0:
      result = opR
    elif opR.isRecordLiteral and opR.table.len == 0:
      result = opL
    elif opL.isRecordLiteral and opR.isRecordLiteral:
      result = Value(kind: tRecordLiteral, table: opL.table)
      for key, val in opR.table.pairs:
        if result.table.hasKeyOrPut(key, val):
          # duplicate key
          result.table.withValue(key, other):
            if val.isRecordLiteral:
              let e = operate(env, opRecordBiasedMerge, other[], val)
              other[] = eval(env, e.quote)
            else:
              other[] = val
    elif opL == opR:
      result = opL
  of opRecordTypeMerge:
    if opL.isRecordType and opL.table.len == 0:
      result = opR
    elif opR.isRecordType and opR.table.len == 0:
      result = opL
    elif opL.isRecordType and opR.isRecordType:
      result = opL
      for key, val in opR.table.pairs:
        if result.table.hasKeyOrPut(key, val):
          # duplicate key
          result.table.withValue(key, other):
            let e = operate(env, opRecordTypeMerge, other[], val)
            other[] = eval(env, e.quote)
  of opEquivalience:
    result = Value(kind: tOp, op: op, opL: opL, opR: opR)
  of opComplete:
    if opL.isRecordLiteral and opR.isRecordLiteral:
      # TODO: the length of the resulting record is known to be
      # the same as the length of opL.table["Type"],
      # could optimize allocation from this.
      result = operate(env,
        opRecordBiasedMerge,
        opL.table["default"],
        opR)
  else: discard
  if result.isNil:
    result = Value(kind: tOp, op: op, opL: opL, opR: opR)

func eval(env: Env; builtin: BuiltinKind; args: seq[Value]): Value {.gcsafe.}

func apply(env: Env; appFun, appArg: Value): Value =
  case appFun.kind
  of tLambdaCallback, tPiCallback:
    result = appFun.callBack(appArg)
  of tBuiltin:
    result = eval(env, appFun.builtin, appFun.builtinArgs & @[appArg])
  of tApp, tField, tFreeVar, tLocalVar, tQuoteVar, tIf:
    result = Value(kind: tApp, appFun: appFun, appArg: appArg)
  else:
    raiseAssert("invalid value for application " & $appFun)

func apply(env: Env; appFun: Value; appArgs: varargs[Value]): Value =
  result = appFun
  for arg in appArgs:
    result = apply(env, result, arg)

func eval(env: Env; builtin: BuiltinKind; args: seq[Value]): Value =
  template whenArgs(count: Natural; body: untyped) =
    if count <= args.len:
      body
    if result.isNil:
      result = Value(kind: tBuiltin, builtin: builtin, builtinArgs: args)
    for i in count..args.high:
      result = newApp(result, args[i])
  case builtin:
  of bNaturalBuild:
    whenArgs(1):
      let f = args[0]
      result = apply(env, apply(env,
          apply(env, f, newValue(bNatural)),
              newLambda("x", newValue(bNatural)) do (x: Value) -> Value:
                operate(env, opNaturalAdd, x, newNatural(1))),
          newNatural(0))
  of bNaturalFold:
    whenArgs(4):
      let
        count = args[0]
        succ = args[2]
        zero = args[3]
      if count.isNatural:
        var i = initBigInt(0)
        result = zero
        while i < count.natural:
          inc i
          result = apply(env, succ, result)
  of bNaturalIsZero:
    whenArgs(1):
      let arg = args[0]
      if arg.isNatural:
        result = newValue(arg.natural == initBigInt(0))
  of bNaturalEven:
    whenArgs(1):
      let arg = args[0]
      if arg.isNatural:
        result = newValue((arg.natural.limbs[0] and 1) == 0)
  of bNaturalOdd:
    whenArgs(1):
      let arg = args[0]
      if arg.isNatural:
        result = newValue((arg.natural.limbs[0] and 1) == 1)
  of bNaturalToInteger:
    whenArgs(1):
      let arg = args[0]
      if arg.isNatural:
        result = newInteger(arg.natural)
  of bNaturalShow:
    whenArgs(1):
      let arg = args[0]
      if arg.isNatural:
        result = newValue($arg.natural)
  of bNaturalSubtract:
    whenArgs(2):
      let x = args[0]
      let y = args[1]
      if x.isNatural and y.isNatural:
        let n = y.natural - x.natural
        result = newNatural(if Negative in n.flags: zero else: n)
      elif x.isNatural and x.natural == zero:
        result = y
      elif y.isNatural and y.natural == zero or x == y:
        # TODO: gcsafe `==`
        result = newNatural(zero)
  of bIntegerToDouble:
    whenArgs(1):
      let arg = args[0]
      if arg.isInteger:
        result = newValue(arg.integer.toBiggestFloat)
  of bIntegerShow:
    whenArgs(1):
      let arg = args[0]
      if arg.isInteger:
        result = newValue(
          if Negative in arg.integer.flags: $arg.integer
          else: "+" & $arg.integer)
  of bIntegerNegate:
    whenArgs(1):
      let arg = args[0]
      if arg.isInteger:
        result = newInteger(arg.integer)
        result.integer.flags =
          if result.integer.flags.contains Negative: {}
          else: {Negative}
  of bIntegerClamp:
    whenArgs(1):
      let arg = args[0]
      if arg.isInteger:
        result =
          if Negative in arg.integer.flags: newNatural(zero)
          else: newNatural(arg.integer)
  of bDoubleShow:
    whenArgs(1):
      let arg = args[0]
      if arg.kind == tDoubleLiteral:
        result = newValue(
          case arg.double.classify
          of fcNormal, fcSubnormal: $arg.double
          of fcZero: "+0.0"
          of fcNegZero: "-0.0"
          of fcNan: "NaN"
          of fcInf: "Infinity"
          of fcNegInf: "-Infinity")
  of bListBuild:
    whenArgs(1):
      let
        a = args[0]
        funType = newPi("list", newValue(bType)) do (list: Value) -> Value:
          newPi("cons",
              newPi(a, newPi(list, list)),
              newPi("nil", list, list))
      result = newLambda("f", funType) do (f: Value) -> Value:
        let listType = newListType(a)
        let cons = newLambda("a", a) do (a: Value) -> Value:
          newLambda("as", listType) do (`as`: Value) -> Value:
            operate(env, opListAppend, newValue(@[a]), `as`)
        let null = Value(kind: tList, listType: some a)
        apply(env, f, newListType(a), cons, null)
#[
      let
        a = args[0]
        f = args[1]
      if f.kind == tLambda:
        let listType = newListType(a)
        let cons = newLambda("a", a) do (a: Value) -> Value:
          newLambda("as", listType) do (`as`: Value) -> Value:
            operate(env, opListAppend, newValue(@[a]), `as`)
        let null = Value(kind: tList, listType: some a)
        result = apply(env, f, newListType(a), cons, null)
]#

  of bListFold:
    whenArgs(3):
      let
        a = args[0]
        `as` = args[1]
        list = args[2]
      if `as`.kind notin {tList, tEmptyList}:
        result = newApp(builtin, a, `as`, list)
      else:
        result = newLambda("cons", newPi(a, newPi(list, list))) do (cons: Value) -> Value:
          newLambda("nil", list) do (`nil`: Value) -> Value:
            result = `nil`
            if `as`.kind == tList and `as`.list != @[]:
              for i in countDown(`as`.list.high, 0):
                result = apply(env, apply(env, cons, `as`.list[i]), result)

#[
    whenArgs(5):
      let
        a = args[0]
        list = args[1]
        `as` = args[2]
        cons = args[3]
        `nil` = args[4]
      if `as`.kind in {tList, tEmptyList}:
        result = `nil`
        if `as`.kind == tList and `as`.list != @[]:
          for i in countDown(`as`.list.high, 0):
            result = apply(env, apply(env, cons, `as`.list[i]), result)
]#

  of bListLength:
    whenArgs(2):
      let arg = args[1]
      case arg.kind
      of tList: result = newNatural(arg.list.len)
      of tEmptyList: result = newNatural(0)
        # TODO: does empty list make it to eval?
      else: discard
  of bListHead, bListLast:
    whenArgs(2):
      let
        a = args[0]
        list = args[1]
      if list.kind in {tList, tEmptyList}:
        if list.kind == tEmptyList or list.list == @[]:
          result = Value(kind: tBuiltin, builtin: bNone, builtinArgs: @[a])
        else:
          let index =
            if builtin == bListHead: list.list.low
            else: list.list.high
          result = Value(kind: tSome, someVal: list.list[index])
  of bListIndexed:
    whenArgs(2):
      let
        a = args[0]
        list = args[1]
      if list.kind in {tList, tEmptyList}:
        if (list.kind == tEmptyList) or (list.list.len == 0):
          let listType = newRecordType(
              [("index", newValue bNatural), ("value", a)])
          result = Value(kind: tList, listType: some listType)
        else:
          result = Value(kind: tList, list: newSeq[Value](list.list.len))
          for i, e in list.list:
            result.list[i] = newRecordLiteral(
              [("index", newNatural i), ("value", e)])
  of bListReverse:
    whenArgs(2):
      let
        a = args[0]
        list = args[1]
      if list.kind in {tList, tEmptyList}:
        if (list.kind == tEmptyList) or (list.list.len == 0):
          result = Value(kind: tList, listType: some a)
        else:
          result = Value(kind: tList, list: newSeq[Value](list.list.len))
          for i, e in list.list:
            result.list[result.list.high-i] = e
  of bTextShow:
    whenArgs(1):
      let arg = args[0]
      if arg.isSimpleText:
        var s = newStringOfCap(arg.textSuffix.len+16)
        s.add '"'
        for tc in arg.textChunks:
          s.addEscaped tc.textPrefix
        s.addEscaped arg.textSuffix
        s.add '"'
        result = Value(kind: tTextLiteral, textSuffix: s)
  of bTextReplace:
    whenArgs(3):
      let
        nee = args[0]
        rep = args[1]
        hay = args[2]
      if not (nee.isSimpleText and hay.isTextLiteral):
        result = newApp(builtin, nee, rep, hay)
      elif nee.textSuffix == "":
        result = hay
      elif hay.isSimpleText:
        proc newChunk(s: string): Value =
          Value(kind: tTextChunk, textPrefix: s)
        let repChunks =
          if rep.isTextLiteral:
            if rep.textSuffix == "":
              rep.textChunks
            else:
              rep.textChunks & @[(newChunk rep.textSuffix)]
          else:
            @[Value(kind: tTextChunk, textExpr: rep)]
        var tmp = Value(kind: tTextLiteral)
        if hay.textSuffix == nee.textSuffix:
          tmp.textChunks.add(repChunks)
        else:
          let ss = split(hay.textSuffix, nee.textSuffix)
          for i, s in ss:
            if i == ss.high:
              tmp.textSuffix = s
            else:
              if s != "":
                tmp.textChunks.add(newChunk(s))
              tmp.textChunks.add(repChunks)
        result = cramText(tmp)
  of bOptional, bList, bNone:
    whenArgs(1):
      result = newApp(newValue(builtin), args[0])
  else: discard
  assert(not result.isNil)

func eval(env: Env; expr: Option[Term]): Option[Value] =
  if expr.isSome:
    result = some eval(env, expr.get)

func eval*(env: Env; t: Term): Value {.gcsafe.} =
  result = walk(t) do (t: Term) -> Value:
    if t.isNil: return nil
    case t.kind
    of tApp:
      result = apply(env, eval(env, t.appFun), eval(env, t.appArg))
    of tLambda, tPi:
      result =
        if t.kind == tPi: Value(kind: tPiCallback)
        else: Value(kind: tLambdaCallback)
      result.callbackLabel = t.funcLabel
      assert(not t.funcType.isNil)
      result.domain = eval(env, t.funcType)
      result.callback = func (v: Value): Value =
        var fresh = env
        fresh[t.funcLabel] = @[v] & fresh.getOrDefault(t.funcLabel)
        eval(fresh, t.funcBody)
    of tOp:
      case t.op
      of opTextAppend:
        func textChunk(t: Term): Term = Term(kind: tTextChunk, textExpr: t)
        result = eval(env, Term(kind: tTextLiteral,
            textChunks: @[t.opL.textChunk, t.opR.textChunk]))
      of opAlternateImport:
        # TODO: resolution should take care of this?
        try:
          result = eval(env, t.opL)
        except ValueError:
          result = eval(env, t.opR)
      else:
        result = operate(env, t.op, eval(env, t.opL), eval(env, t.opR))
    of tMerge:
      let handler = eval(env, t.mergeHandler)
      let union = eval(env, t.mergeUnion)
      if handler.isRecordLiteral:
        case union.kind
        of tApp:
          case union.appFun.kind
          of tField:
            let name = union.appFun.fieldName
            result = apply(env, handler.table[name], union.appArg)
          of tBuiltin:
            if union.appFun.builtin == bNone:
              result = handler.table["None"]
          else: discard
        of tSome:
          result = apply(env, handler.table["Some"], @[union.someVal])
        of tField:
          if union.fieldRecord.isUnion:
            result = handler.table[union.fieldName]
        else: discard
      if result.isNil:
        result = Value(kind: tMerge,
            mergeHandler: handler,
                mergeUnion: union, mergeAnn: eval(env, t.mergeAnn))
    of tField:
      result = Value(kind: tField, fieldName: t.fieldName, fieldRecord: eval(
          env, t.fieldRecord))
      while true:
        case result.fieldRecord.kind
        of tProject:
          result.fieldRecord = result.fieldRecord.projectRecord
        of tProjectType:
          result.fieldRecord = result.fieldRecord.projectTypeRecord
        else: break
      let name = result.fieldName
      block fieldLoop:
        while result.kind == tField:
          case result.fieldRecord.kind
          of tRecordType, tRecordLiteral:
            result = result.fieldRecord.table[name]
          of tOp:
            case result.fieldRecord.op
            of opRecordRecursiveMerge:
              let opL = result.fieldRecord.opL
              let opR = result.fieldRecord.opR
              if opL.isRecordLiteral:
                opL.table.withValue(name, p) do:
                  result.fieldRecord.opL = newRecordLiteral([(name, p[])])
                  break fieldLoop
                do:
                  result.fieldRecord = opR
              elif opR.isRecordLiteral:
                opR.table.withValue(name, p) do:
                  result.fieldRecord.opR = newRecordLiteral([(name, p[])])
                  break fieldLoop
                do:
                  result.fieldRecord = opL
            of opRecordBiasedMerge:
              let opL = result.fieldRecord.opL
              let opR = result.fieldRecord.opR
              if opR.isRecordLiteral:
                opR.table.withValue(name, p) do:
                  result = p[]
                do:
                  result = Value(kind: tField,
                    fieldName: name, fieldRecord: opL)
              elif opL.isRecordLiteral:
                opL.table.withValue(name, p) do:
                  result.fieldRecord.opL = newRecordLiteral([(name, p[])])
                  break fieldLoop
                do:
                  result.fieldRecord = opR
            of opRecordTypeMerge:
              let opL = result.fieldRecord.opL
              let opR = result.fieldRecord.opR
              if opL.isRecordType:
                opL.table.withValue(name, p) do:
                  result.fieldRecord.opL = newRecordType([(name, p[])])
                  break fieldLoop
                do:
                  result.fieldRecord = opR
              elif opR.isRecordType:
                opR.table.withValue(name, p) do:
                  result.fieldRecord.opR = newRecordType([(name, p[])])
                  break fieldLoop
                do:
                  result.fieldRecord = opL
            else: break
          of tProject:
            result.fieldRecord = result.fieldRecord.projectRecord
              # Type check guarantees that the field is projected
          else: break
    of tProject:
      # TODO: normalize only until this is a record literal?
      var record = eval(env, t.projectRecord)
      while true:
        case record.kind
        of tProject:
          record = record.projectRecord
        of tProjectType:
          record = record.projectTypeRecord
        else: break
      let names = t.projectNames
      if names == @[]:
        result = newRecordLiteral(0)
      else:
        case t.projectRecord.kind
        of tRecordLiteral:
          let record = t.projectRecord.table
          result = newRecordLiteral(names.len)
          for name in names:
            result.table[name] = eval(env, record[name])
        of tOp:
          case t.projectRecord.op
          of opRecordBiasedMerge:
            let tmp = Term(kind: tOp, op: opRecordBiasedMerge)
            let opR = t.projectRecord.opR
            let opL = t.projectRecord.opL
            if opR.isRecordLiteral:
              var namesL, namesR: seq[string]
              for name in names:
                if opR.table.hasKey name:
                  namesR.add name
                else:
                  namesL.add name
              tmp.opL = Term(kind: tProject,
                projectNames: namesL, projectRecord: opL)
              tmp.opR = Term(kind: tProject,
                  projectNames: namesR, projectRecord: opR)
            else:
              tmp.opR = Term(kind: tProject,
                projectNames: names, projectRecord: opR)
              tmp.opL = Term(kind: tProject,
                  projectNames: names, projectRecord: opL)
            result = eval(env, tmp)
          else: discard
        else: result = Value(kind: tProject,
            projectRecord: record,
            projectNames: names.sorted)
    of tProjectType:
      let selectorRecord = eval(env, t.projectTypeSelector).table
      if selectorRecord.len == 0:
        result = newRecordLiteral(0)
      else:
        var names = newSeqOfCap[string](selectorRecord.len)
        for key in selectorRecord.keys:
          names.add key
        result = eval(env, Term(kind: tProject,
            projectNames: names, projectRecord: t.projectTypeRecord))
    of tIf:
      var ifCond, ifTrue, ifFalse: Value
      ifCond = eval(env, t.ifCond)
      if ifCond.kind == tBoolLiteral:
        var e =
          if ifCond.bool: t.ifTrue
          else: t.ifFalse
        result = eval(env, e)
      else:
        ifTrue = eval(env, t.ifTrue)
        ifFalse = eval(env, t.ifFalse)
        if ifTrue == ifFalse:
          result = ifTrue
        elif ifTrue.isBool and ifTrue.bool == true and
            ifFalse.isBool and ifFalse.bool == false:
          result = ifCond
        else:
          result = Value(kind: tIf,
              ifCond: ifCond, ifTrue: ifTrue, ifFalse: ifFalse)
    of tTextLiteral:
      var tmp = Value(kind: tTextLiteral,
          textChunks: newSeq[Value](t.textChunks.len),
          textSuffix: t.textSuffix)
      for i, tc in t.textChunks:
        tmp.textChunks[i] = Value(kind: tTextChunk,
            textPrefix: tc.textPrefix,
            textExpr: eval(env, tc.textExpr))
      result = cramText(tmp)
    of tLet:
      var fresh = env
      for b in t.letBinds:
        let val = eval(fresh, b.letVal)
        fresh[b.letKey] = @[val] & fresh.getOrDefault(b.letKey)
      result = eval(fresh, t.letBody)
    of tAnnotation:
      result = eval(env, t.annExpr)
    of tToMap:
      var body = eval(env, t.toMapBody)
      if not body.isRecordLiteral:
        result = Value(kind: tToMap,
            toMapBody: body,
            toMapAnn: eval(env, t.toMapAnn))
      else:
        let record = body.table
        let n = record.len
        if n == 0:
          var ann = eval(env, t.toMapAnn.get)
          if ann.isApp and ann.appFun.isBuiltin(bList):
            ann = ann.appArg
          result = Value(kind: tList, listType: some ann)
        else:
          var list = newSeqOfCap[Value](n)
          var keys = newSeqOfCap[string](n)
          for key in record.keys:
            keys.add key
          sort keys
          for key in keys:
            list.add newRecordLiteral(
              [("mapKey", newValue key), ("mapValue", record[key])])
          result = Value(kind: tList, list: list, listType: eval(env,
              t.toMapAnn))
    of tEmptyList:
      var T = eval(env, t.emptyListType)
      if T.kind == tApp and
          T.appFun.kind == tBuiltin and
          T.appFun.builtin == bList:
        T = T.appArg
      result = Value(kind: tList, listType: some T)
    of tWith:
      let update = eval(env, t.withUpdate)
      var expr = eval(env, t.withExpr)
      if not expr.isRecordLiteral:
        result = Value(kind: tWith,
            withExpr: expr, withUpdate: update,
            withFields: t.withFields)
      else:
        result = expr
        for i, field in t.withFields:
          if i == t.withFields.high:
            expr.table[field] = update
          else:
            let next = expr.table.getOrDefault(field)
            if next.isNil:
              let next = newRecordLiteral(2)
              expr.table[field] = next
              expr = next
            elif next.isRecordLiteral:
              expr = next
            else:
              expr.table[field] = Value(kind: tWith,
                withExpr: next,
                withUpdate: update,
                withFields: t.withFields[i.succ..t.withFields.high])
              break
    of tVar:
      let
        name = t.varName
        stack = env.getOrDefault(name)
      if 0 < t.varIndex and stack.len < t.varIndex:
        result = Value(kind: tFreeVar,
            varName: t.varName,
            varIndex: t.varIndex - stack.len)
      elif t.varIndex < stack.len:
        result = stack[t.varIndex]
    of tFuture:
      result = eval(env, t.future.read)
    of tImport:
      raise newException(ValueError,
          "expression must be fully resolved for β normalization")
    of tFreeVar, tQuoteVar:
      assert(false, $t.kind & " invalid for eval")
    else:
      discard

# RebindLocal rebindAtLevel

M src/dhall/parse.nim => src/dhall/parse.nim +288 -266
@@ 1,88 1,92 @@
import term

export term.`==`
import terms

import bigints, npeg, npeg/lib/uri, npeg/lib/utf8

import algorithm, math, options, parseutils, tables, unicode
import algorithm, math, options, parseutils, strutils, tables, unicode

func isHex(s: string): bool {.inline.} =
  s.len > 2 and s[0] == '0' and s[1] == 'x'

proc parseBigInt(s: string): BigInt =
func parseBigInt(s: string): BigInt =
  if s.isHex:
    initBigInt(s[2..s.high], 16)
  else:
    initBigInt(s, 10)

when not defined(release):
  template dumpCapture(label: string) =
    echo label, " stack: ", stack
    if capture.len == 1:
      echo label, " capture: ", capture[0].s
    else:
      echo label, " capture:"
      for i in 0..<capture.len:
        echo label, "\t$", i, " ", capture[i].s
type
  Frame = tuple[term: Term, pos: int]
  Stack = seq[Frame]

template backtrack(n = 1) =
  stack.setLen(stack.len-n)
  fail()

proc flattenOperator(stack: var seq[Term]; kind: OpKind; n: int) =
func flattenOperator(stack: var Stack; kind: OpKind; n: int) =
  assert(n < stack.len)
  let off = stack.high-n
  for i in off+1..stack.high:
    stack[off] = Term(kind: tOp, op: kind, opL: move(stack[off]), opR: move(stack[i]))
    stack[off].term = Term(kind: tOp, op: kind,
        opL: stack[off].term,
        opR: stack[i].term)
  stack.setLen(stack.len-n)

template flattenOperator(stack: seq[Term]; kind: OpKind) =
template flattenOperator(stack: Stack; kind: OpKind) =
  let n = capture.len-1
  if n > 0:
    flattenOperator(stack, kind, n)

template push(t: Term) = add(stack, t)
template peek(): var Term = stack[stack.high].term
template pop(): Term = pop(stack).term
template push(t: Term) = stack.add((t, capture[0].si))

template appendTextLiteral(s: string) =
  # TODO: don't parse rune-by-rune
  # TODO: optimize!
  #[
  if stack.len > 0 and
      stack[stack.high].kind == tTextChunk and
          stack[stack.high].textExpr.isNil:
    stack[stack.high].textPrefix.add s
      peek().kind == tTextChunk and
          peek().textExpr.isNil:
    peek().textPrefix.add s
  else:
  ]#
    push Term(kind: tTextChunk, textPrefix: s)

proc joinTextChunks(stack: var seq[Term]) =
    var n: int
    while n < stack.len and stack[stack.high-n].kind == tTextChunk:
      inc n
    let t = Term(kind: tTextLiteral,
        textChunks: newSeq[Term](n), textSuffix: "")
    let chunkOff = stack.len-n
    for i in 0..<n:
      t.textChunks[i] = move stack[chunkOff+i]
    if t.textChunks.len > 0 and t.textChunks[t.textChunks.high].textExpr.isNil:
      t.textSuffix = move t.textChunks.pop.textPrefix
    stack.setLen(succ chunkOff)
    stack[chunkOff] = t
func joinTextChunks(stack: var Stack; pos: int) =
  var n: int
  while n < stack.len and
      stack[stack.high-n].pos > pos and
      stack[stack.high-n].term.kind == tTextChunk:
    inc n
  let t = Term(kind: tTextLiteral,
      textChunks: newSeqOfCap[Term](n), textSuffix: "")
  let chunkOff = stack.len-n
  var tmp = ""
  for i in 0..<n:
    let tc = stack[chunkOff+i].term
    tmp.add(tc.textPrefix)
    if not tc.textExpr.isNil:
      t.textChunks.add Term(kind: tTextChunk,
        textPrefix: move tmp, textExpr: tc.textExpr)
  t.textSuffix = move tmp
  stack.setLen(succ chunkOff)
  stack[chunkOff].term = t

type IndentParser = tuple[indent: string, tailLine: bool]

# TODO: break windows compatiblity in release builds

proc parse(ip: var IndentParser; s: string) =
func parse(ip: var IndentParser; s: string) =
  ## Determine the common indentation level of ``s``.
  var i: int
  if not ip.tailLine:
    i = s.skipWhile({'\r','\n'}, 0)
    i = s.skipWhile({'\r', '\n'}, 0)
      # Skip empty lines.
    i.inc(s.parseWhile(ip.indent, {'\t',' '}, i))
    i.inc(s.parseWhile(ip.indent, {'\t', ' '}, i))
      # Take the leading whitespace of the first non-empty line.
    ip.tailLine = true
  while i < s.len:
    let lineLen = s.skipUntil({'\r','\n'}, i)
    let lineLen = s.skipUntil({'\r', '\n'}, i)
    i.inc(lineLen)
    i.inc(s.skipWhile({'\r','\n'}, i))
    i.inc(s.skipWhile({'\r', '\n'}, i))
      # Skip empty lines.
    let remain = s.len-i
    if 0 < remain and remain < ip.indent.len:


@@ 95,18 99,18 @@ proc parse(ip: var IndentParser; s: string) =
        break
    i.inc(ip.indent.len)

proc dedent(headLine: var bool; s: var string; n: int) =
func dedent(headLine: var bool; s: var string; n: int) =
  ## Remove ``n`` leading whitespace characters from every line.
  assert(n > 0)
  var j: int
  var i = if headLine: n else: 0
  headLine = false
  while i < s.len:
    while i < s.len and s[i] notin {'\r','\n'}:
    while i < s.len and s[i] notin {'\r', '\n'}:
      s[j] = s[i]
      inc j
      inc i
    while i < s.len and s[i] in {'\r','\n'}:
    while i < s.len and s[i] in {'\r', '\n'}:
      if s[i] != '\r':
        s[j] = '\n'
        inc j


@@ 114,7 118,7 @@ proc dedent(headLine: var bool; s: var string; n: int) =
    inc i, n
  s.setLen(j)

let parser = peg("final_expression", stack: seq[Term]):
const parser = peg("final_expression", stack: Stack):

  final_expression <- complete_expression * !1



@@ 133,22 137,25 @@ let parser = peg("final_expression", stack: seq[Term]):
      assert_expression |
      annotated_expression

  lamba_expression <- lambda * whsp * '(' * whsp * nonreserved_label * whsp * ':' * whsp1 * expression * whsp * ')' * whsp * arrow * whsp * expression:
  lamba_expression <- lambda * whsp * '(' * whsp * nonreserved_label * whsp *
      ':' * whsp1 * expression * whsp * ')' * whsp * arrow * whsp * expression:
    push Term(kind: tLambda,
        lambdaLabel: move($1), lambdaBody: stack.pop(), lambdaType: stack.pop())
        funcLabel: $1, funcBody: pop(), funcType: pop())

  if_expression <- If * whsp1 * expression * whsp * Then * whsp1 * expression * whsp * Else * whsp1 * expression:
    push Term(kind: tIf, ifFalse: stack.pop, ifTrue: stack.pop, ifCond: stack.pop)
  if_expression <- If * whsp1 * expression * whsp * Then * whsp1 * expression *
      whsp * Else * whsp1 * expression:
    push Term(kind: tIf, ifFalse: pop(), ifTrue: pop(),
        ifCond: pop())

  let_bindings <- +let_binding * In * whsp1 * expression:
    var n: int
    for i in countDown(stack.high.pred, 0):
      if stack[i].kind != tBinding:
      if stack[i].term.kind != tLetBinding:
        break
      inc n
    var t = Term(kind: tLet, letBinds: newSeq[Term](n), letBody: stack.pop())
    var t = Term(kind: tLet, letBinds: newSeq[Term](n), letBody: pop())
    for i in 0..<n:
      t.letBinds[i] = move stack[stack.len-n+i]
      t.letBinds[i] = stack[stack.len-n+i].term
    if t.letBody.kind == tLet:
      t.letBinds = t.letBinds & t.letBody.letBinds
      t.letBody = t.letBody.letBody


@@ 157,44 164,45 @@ let parser = peg("final_expression", stack: seq[Term]):

  forall_expression <- forall * whsp * '(' * whsp * (>'_' | nonreserved_label) * whsp * ':' * whsp1 * expression * whsp * ')' * whsp * arrow * whsp * expression:
    push Term(kind: tPi,
        piBody: stack.pop(),
        piType: stack.pop(),
        piLabel: move($1))
        funcBody: pop(),
        funcType: pop(),
        funcLabel: $1)

  toMap_annotated_expression <- toMap_expression * ?(whsp * >':' * whsp1 * application_expression):
    if capture.len != 2:
      backtrack()
    stack[pred stack.high].toMapAnn = stack.pop()
    stack[pred stack.high].term.toMapAnn = some pop()

  Import <- import_hashed * ?( whsp * As * whsp1 * >(Text | Location) ):
  Import <- import_hashed * ?(whsp * As * whsp1 * >(Text | Location)):
    case capture.len
    of 1: discard
    of 2:
      stack[stack.high].importKind = case $1
      peek().importKind = case $1
        of "Text": iText
        of "Location": iLocation
        else: fail()
    else: fail()

  assert_expression <- Assert * whsp * ':' * whsp1 * expression:
    push Term(kind: tAssert, assertAnn: stack.pop())
    push Term(kind: tAssert, assertAnn: pop())

  annotated_expression <- operator_expression * ?( whsp * >':' * whsp1 * expression ):
  annotated_expression <- operator_expression * ?(whsp * >':' * whsp1 * expression):
    case capture.len
    of 1: discard
    of 2:
      push Term(kind: tAnnotation,
          annAnn: stack.pop(), annExpr: stack.pop())
          annAnn: pop(), annExpr: pop())
    else: fail()

  let_binding <- Let * whsp1 * nonreserved_label * whsp * ?( >':' * whsp1 * expression * whsp ) * '=' * whsp * expression * whsp:
  let_binding <- Let * whsp1 * nonreserved_label * whsp *
      ?( >':' * whsp1 * expression * whsp) * '=' * whsp * expression * whsp:
    case capture.len
    of 2:
      push Term(kind: tBinding,
          key: move($1), val: stack.pop())
      push Term(kind: tLetBinding,
          letKey: $1, letVal: pop())
    of 3:
      push Term(kind: tBinding,
          key: move($1), val: stack.pop(), ann: stack.pop())
      push Term(kind: tLetBinding,
          letKey: $1, letVal: pop(), letAnn: some pop())
    else: fail()

  arrow_expression <- operator_expression * ?(whsp * >arrow * whsp * expression):


@@ 202,40 210,43 @@ let parser = peg("final_expression", stack: seq[Term]):
    if capture.len != 2:
      backtrack()
    push Term(kind: tPi,
        piLabel: "_", piBody: stack.pop(), piType: stack.pop())
        funcLabel: "_", funcBody: pop(), funcType: pop())

  with_clause <- any_label_or_some * *(whsp * '.' * whsp * any_label_or_some) *
      whsp * '=' * whsp * operator_expression:
    var fields = newSeq[string](capture.len-1)
    for i in 1..<capture.len:
      fields[pred i] = capture[i].s
    let t = Term(kind: tWith, withFields: fields, withUpdate: pop())
    push(t)

  with_expression <- import_expression * *(whsp1 * >with * whsp1 * with_clause):
    if capture.len == 1:
      backtrack()
    let n = capture.len-1
    if n > 0:
      let off = stack.high-n
      for i in off+1..stack.high:
        let t = stack[i]
        let record = Term(kind: tRecordLiteral,
          recordLiteral: toTable [(move t.entryKey, move t.entryVal)])
        stack[off] = Term(kind: tOp,
            op: opRecordBiasedMerge,
            opL: move(stack[off]),
            opR: record)
      stack.setLen(stack.len-n)

  merge_annotated_expression <- merge_expression * ?(whsp * >':' * whsp1 * application_expression):
    let pos = capture[0].si
    var stackOff = stack.high.pred
    while stack[stackOff].pos > pos and stack[stackOff].term.kind == tWith:
      dec stackOff
    var expr = stack[stackOff].term
    for i in stackOff.succ..stack.high:
      var next = move stack[i].term
      next.withExpr = expr
      expr = next
    stack.setLen(stackOff)
    push(expr)

  merge_annotated_expression <- merge_expression * ?(whsp * >':' * whsp1 *
      application_expression):
    if capture.len != 2:
      backtrack()
    stack[pred stack.high].mergeAnn = stack.pop()
    stack[pred stack.high].term.mergeAnn = some pop()

  empty_list_literal <- '[' * whsp * ?( ',' * whsp ) * ']' * whsp * ':' * whsp1 * application_expression:
    let listType = stack.pop
  empty_list_literal <- '[' * whsp * ?(',' * whsp) * ']' * whsp * ':' * whsp1 * application_expression:
    var listType = pop()
    if listType.kind == tApp and
        listType.appFun.kind == tBuiltin and
            listType.appFun.builtin == bList:
      # applicaton of the List builtin
      if listType.appArgs.len == 1:
        # eliminate the List builtin and promote the single argument
        push Term(kind: tList, listType: move listType.appArgs[0])
      else:
        push Term(kind: tEmptyList, emptyListType: listType)
      push Term(kind: tList, listType: some(listType.appArg))
    else:
      push Term(kind: tEmptyList, emptyListType: listType)



@@ 249,8 260,8 @@ let parser = peg("final_expression", stack: seq[Term]):

  double_quote_escaping <- '\\' * double_quote_escaped

  double_quote_char <- {'\x20'..'\x21'} | {'\x23'..'\x5b'} | {'\x5d'..'\x7e'} | valid_non_ascii:
    appendTextLiteral(move $0)
  double_quote_char <- +({'\x20'..'\x21'} | '\x23' | {'\x25'..'\x5b'} | {'\x5d'..'\x7a'} | valid_non_ascii) | '$' | {'\x7b'..'\x7e'}:
    appendTextLiteral($0)

  double_quote_escaped <- double_quote_escaped_char | double_quote_escaped_unicode



@@ 261,7 272,7 @@ let parser = peg("final_expression", stack: seq[Term]):
    of "n": appendTextLiteral("\n")
    of "r": appendTextLiteral("\r")
    of "t": appendTextLiteral("\t")
    else: appendTextLiteral(move $0)
    else: appendTextLiteral($0)

  double_quote_escaped_unicode <- 'u' * unicode_escape:
    var r: uint32


@@ 288,14 299,14 @@ let parser = peg("final_expression", stack: seq[Term]):
    appendTextLiteral("${")

  single_quote_char <- Print | valid_non_ascii | tab | end_of_line:
    appendTextLiteral(move $0)
    appendTextLiteral($0)

  interpolation <- "${" * complete_expression * '}':
    let textExpr = stack.pop()
    let textExpr = pop()
    if stack.len > 0 and
        stack[stack.high].kind == tTextChunk and
            stack[stack.high].textExpr.isNil:
      stack[stack.high].textExpr = textExpr
        peek().kind == tTextChunk and
            peek().textExpr.isNil:
      peek().textExpr = textExpr
    else:
      push Term(kind: tTextChunk, textExpr: textExpr)



@@ 306,7 317,7 @@ let parser = peg("final_expression", stack: seq[Term]):
  numeric_double_literal <- ?pos_or_neg * +Digit * (('.' * +Digit * ?exponent) | exponent):
    var t = Term(kind: tDoubleLiteral)
    if parseBiggestFloat($0, t.double) > 0 and
        classify(t.double) in {fcNormal,fcZero,fcNegZero}:
        classify(t.double) in {fcNormal, fcZero, fcNegZero}:
      push t
    else:
      validate(false)


@@ 326,7 337,7 @@ let parser = peg("final_expression", stack: seq[Term]):
    let t = Term(kind: tImport,
        importElements: newSeq[string](capture.len-1))
    for i in 1..<capture.len:
      t.importElements[pred i] = move capture[i].s
      t.importElements[pred i] = capture[i].s
    push t

  path_component <- '/' * ( >unquoted_path_component | ('"' * >quoted_path_component * '"') )


@@ 351,52 362,52 @@ let parser = peg("final_expression", stack: seq[Term]):
  local <- parent_path | here_path | home_path | absolute_path

  absolute_path <- path:
    stack[stack.high].importScheme = 2
    peek().importScheme = iAbs

  here_path <- '.' * path:
    stack[stack.high].importScheme = 3
    peek().importScheme = iHere

  parent_path <- ".." * path:
    stack[stack.high].importScheme = 4
    peek().importScheme = iParent

  home_path <- '~' * path:
    stack[stack.high].importScheme = 5
    peek().importScheme = iHome

  scheme <- "http" * ?'s'

  query <- *( uri.pchar | "/" | "|" | "?" )
  query <- *(uri.pchar | "/" | "|" | "?")

  http_raw <- >scheme * "://" * (>uri.authority * >uri.path) * ?( '?' * >query):
  http_raw <- >scheme * "://" * ( > uri.authority * >uri.path) * ?('?' * >query):
    let t = Term(kind: tImport,
        importScheme: case $1
            of "http": 0
            of "https": 1
            of "http": iHttp
            of "https": iHttps
            else: fail())
    if $3 != "":
      t.importElements = split($3, Rune('/'))
      t.importElements[0] = move($2)
      t.importElements[0] = $2
    else:
      t.importElements = @[move($2), ""]
      t.importElements = @[$2, ""]
    if capture.len > 4:
      t.importQuery = some move($4)
      t.importQuery = some $4
    push t

  http <- http_raw * ?( whsp * >Using * whsp1 * import_expression ):
  http <- http_raw * ?(whsp * >Using * whsp1 * import_expression):
    case capture.len
    of 1: discard
    of 2:
      assert(stack.len > 1)
      stack[pred stack.high].importHeaders = stack.pop()
      stack[pred stack.high].term.importHeaders = some pop()
    else: fail()

  env <- "env:" * (bash_environment_variable | posix_environment_variable)

  missing <- "missing" * !simple_label_next_char:
    push Term(kind: tImport, importScheme: 7)
    push Term(kind: tImport, importScheme: iMiss)

  bash_environment_variable <- >( (Alpha | '_') * *(Alnum | '_') ):
    push Term(kind: tImport,
        importScheme: 6, importElements: @[move($1)])
        importScheme: iEnv, importElements: @[$1])

  posix_environment_variable <- '"' * >( +posix_environment_variable_character ) * '"':
    let s = $1


@@ 422,51 433,22 @@ let parser = peg("final_expression", stack: seq[Term]):
        inc(i)
    ev.add(s[s.high])
    push Term(kind: tImport,
        importScheme: 6, importElements: @[ev])
        importScheme: iEnv, importElements: @[ev])

  posix_environment_variable_character <- ('\\' *
      ( '"' | '\\' | 'a' | 'b' | 'f' | 'n' | 'r' | 't' | 'v')) |
      ('"' | '\\' | 'a' | 'b' | 'f' | 'n' | 'r' | 't' | 'v')) |
      {'\x20'..'\x21'} |
      {'\x23'..'\x3c'} |
      {'\x3e'..'\x5b'} |
      {'\x5d'..'\x7e'}

  hash <- "sha256:" * >Xdigit[64]:
    var check = newSeq[byte](2+32)
    check[0] = 0x12'u8
    check[1] = 0x20'u8
    var check = newSeq[byte](32)
    for i in 0..31:
      validate(parseHex($1, check[2+i], 2*i, 2) == 2)
    stack[stack.high].importCheck = check

  import_hashed <- import_type * ?( whsp1 * hash )

  with_clause <- any_label_or_some * *(whsp * '.' * whsp * any_label_or_some) * whsp * '=' * whsp * operator_expression:
    var tR = stack.pop()
    if capture.len > 2:
      # TODO: dubious implementation
      tR = Term(kind: tRecordLiteral,
          recordLiteral: toTable [(capture[pred capture.len].s, tR)])
    for i in countDown(capture.len-2, 1):
      var tL = stack[stack.high]
      if tL.kind == tEntry:
        tL = Term(kind: tOp,
          op: opRecordBiasedMerge,
          opL: stack[pred stack.high],
          opR: Term(kind: tRecordLiteral,
              recordLiteral: toTable [(tL.entryKey, tL.entryVal)]))
      for j in countUp(1, i):
        tL = Term(kind: tField,
            fieldRecord: tL,
            fieldName: capture[j].s)
      tR = Term(kind: tOp,
          op: opRecordBiasedMerge,
          opL: tL, opR: tR)
      if 1 < i:
        tR = Term(kind: tRecordLiteral,
            recordLiteral: toTable [(capture[i].s, tR)])
    push Term(kind: tEntry,
        entryKey: move capture[1].s, entryVal: tR)
      validate(parseHex($1, check[i], 2*i, 2) == 2)
    peek().importCheck = check

  import_hashed <- import_type * ?(whsp1 * hash)

  not_equal_expression <- application_expression * *(whsp * >"!=" * whsp * application_expression):
    stack.flattenOperator(opBoolInequality)


@@ 518,21 500,21 @@ let parser = peg("final_expression", stack: seq[Term]):
  application_expression <- first_application_expression * *(whsp1 * >import_expression):
    if capture.len > 1:
      let stackOff = stack.high - (capture.len - 1)
      let t = Term(kind: tApp,
        appFun: move(stack[stackOff]),
        appArgs: stack[stackOff+1..stack.high])
      var app = stack[stackOff].term
      for i in stackOff+1..stack.high:
        app = Term(kind: tApp, appFun: app, appArg: stack[i].term)
      stack.setLen(stackOff+1)
      stack[stackOff] = t
      stack[stackOff].term = app

  merge_expression <- merge * whsp1 * import_expression * whsp1 * import_expression:
    push Term(kind: tMerge,
        mergeUnion: stack.pop(), mergeHandler: stack.pop())
        mergeUnion: pop(), mergeHandler: pop())

  Some_expression <- Some * whsp1 * import_expression:
    push Term(kind: tSome, someVal: stack.pop())
    push Term(kind: tSome, someVal: pop())

  toMap_expression <- toMap * whsp1 * import_expression:
    push Term(kind: tToMap, toMapBody: stack.pop())
    push Term(kind: tToMap, toMapBody: pop())

  primitive_expression <-
      double_literal |


@@ 545,7 527,7 @@ let parser = peg("final_expression", stack: seq[Term]):
      union_type |
      non_empty_list_literal |
      identifier |
      ( '(' * complete_expression * ')' )
      ('(' * complete_expression * ')')

  selector_expression <- primitive_expression * *(whsp * '.' * whsp * selector)
    # NOTE: Backtrack when parsing the `*("." ...)`.  The reason why is that you


@@ 555,7 537,7 @@ let parser = peg("final_expression", stack: seq[Term]):

  completion_expression <- selector_expression * ?( whsp * >complete * whsp * selector_expression ):
    if capture.len == 2:
      push Term(kind: tOp, op: opComplete, opR: stack.pop, opL: stack.pop)
      push Term(kind: tOp, op: opComplete, opR: pop(), opL: pop())

  import_expression <- Import | completion_expression



@@ 571,7 553,7 @@ let parser = peg("final_expression", stack: seq[Term]):
      minus_infinity_literal | plus_infinity_literal | NaN_literal

  integer_literal <- >pos_or_neg * >natural:
    var t =  Term(kind: tIntegerLiteral, integer: parseBigInt($2))
    var t = Term(kind: tIntegerLiteral, integer: parseBigInt($2))
    if $1 == "-": t.integer.flags = {Negative}
    push t



@@ 581,14 563,14 @@ let parser = peg("final_expression", stack: seq[Term]):
  text_literal <- double_quote_literal | single_quote_literal

  double_quote_literal <- '"' * *double_quote_chunk * '"':
    joinTextChunks(stack)
    joinTextChunks(stack, capture[0].si)

  single_quote_literal <- "''" * end_of_line * single_quote_continue:
    joinTextChunks(stack)
    joinTextChunks(stack, capture[0].si)
    # Longest common whitespace indentation
    # is stripped from single quote literals.
    let literal = stack[stack.high]
    if literal.textSuffix[literal.textSuffix.high] != '\n':
    let literal = peek()
    if not literal.textSuffix.endsWith('\n'):
      # Only if the closing '' has leading whitespace.
      var ip: IndentParser
      for tc in literal.textChunks:


@@ 606,7 588,7 @@ let parser = peg("final_expression", stack: seq[Term]):
    push Term(kind: tBuiltin, builtin: parseBuiltin($0))

  variable <- nonreserved_label * ?(whsp * '@' * whsp * >natural):
    var t = Term(kind: tVar, varName: move($1))
    var t = Term(kind: tVar, varName: $1)
    if capture.len == 3:
      let n = if isHex($2):
          parseHex($2, t.varIndex)


@@ 621,110 603,130 @@ let parser = peg("final_expression", stack: seq[Term]):

  label_selector <- any_label:
    for i in 1..<capture.len:
      push Term(kind: tField, fieldRecord: stack.pop(), fieldName: move capture[i].s)
      push Term(kind: tField, fieldRecord: pop(), fieldName: capture[i].s)

  labels <- '{' * whsp * ?( ',' * whsp ) * ?( any_label_or_some * whsp * *(',' * whsp * any_label_or_some * whsp) ) * ?( ',' * whsp ) * '}'
  labels <- '{' * whsp * ?( ',' * whsp ) * ?( any_label_or_some * whsp * *(',' * whsp * any_label_or_some * whsp) * ?( ',' * whsp )) * '}'

  fields_selector <- labels:
    var t = Term(kind: tProject,
        projectRecord: stack.pop(),
        projectRecord: pop(),
        projectNames: newSeq[string](pred capture.len))
    for i in 1..<capture.len:
      t.projectNames[pred i] = move capture[i].s
      t.projectNames[pred i] = capture[i].s
    push t

  type_selector <- '(' * whsp * expression * whsp * ')':
    push Term(kind: tProjectType,
        projectTypeSelector: stack.pop(),
        projectTypeRecord: stack.pop())
        projectTypeSelector: pop(),
        projectTypeRecord: pop())

  record_type <- '{' * whsp * ?( ',' * whsp ) * (non_empty_record_type | empty_record_type) * whsp * '}'

  record_literal <- '{' * whsp * ?( ',' * whsp ) * (non_empty_record_literal | empty_record_literal) * whsp * '}'

  empty_record_literal <- '=' * ?( whsp * ',' ):
    push Term(kind: tRecordLiteral, recordLiteral: initTable[string, Term](2))
    push Term(kind: tRecordLiteral, table: initTable[string, Term](2))

  empty_record_type <- 0:
    push Term(kind: tRecordType, recordType: initTable[string, Term](2))
    push Term(kind: tRecordType, table: initTable[string, Term](2))

  non_empty_record_type <- record_type_entry * *(whsp * >',' * whsp * record_type_entry) * ?( whsp * ',' ):
    let n = capture.len
  non_empty_record_type <- record_type_entry * *(whsp * ',' * whsp * record_type_entry) * ?( whsp * ',' ):
    let pos = capture[0].si
    var n: int
    while n < stack.len and
        stack[stack.high-n].pos >= pos and
        stack[stack.high-n].term.kind == tRecordBinding:
      inc n
    var t = Term(kind: tRecordType,
        recordType: initTable[string, Term](nextPowerOfTwo n))
        table: initTable[string, Term](nextPowerOfTwo n))
    for i in stack.len-n..stack.high:
      if t.recordType.hasKey stack[i].entryKey:
        t.recordType[stack[i].entryKey] = Term(kind: tOp,
      if t.table.hasKey stack[i].term.recKey:
        t.table[stack[i].term.recKey] = Term(kind: tOp,
            op: opRecordTypeMerge,
            opL: t.recordType[stack[i].entryKey],
            opR: stack[i].entryVal)
            opL: t.table[stack[i].term.recKey],
            opR: stack[i].term.recVal)
      else:
        t.recordType.add(stack[i].entryKey, stack[i].entryVal)
        t.table.add(stack[i].term.recKey, stack[i].term.recVal)
    stack.setLen(stack.len-n)
    push t

  record_type_entry <- any_label_or_some * whsp * ':' * whsp1 * expression:
    push Term(kind: tEntry, entryKey: move($1), entryVal: stack.pop())
    push Term(kind: tRecordBinding, recKey: $1, recVal: pop())

  non_empty_record_literal <- record_literal_entry * *(whsp * >',' * whsp * record_literal_entry) * ?( whsp * ',' ):
    let n = capture.len
    let pos = capture[0].si
    var n: int
    while n < stack.len and
        stack[stack.high-n].pos >= pos and
        stack[stack.high-n].term.kind == tRecordBinding:
      inc n
    var t = Term(kind: tRecordLiteral,
        recordLiteral: initTable[string, Term](nextPowerOfTwo n))
        table: initTable[string, Term](nextPowerOfTwo n))
    for i in stack.len-n..stack.high:
      if t.recordLiteral.hasKey stack[i].entryKey:
        t.recordLiteral[stack[i].entryKey] = Term(kind: tOp,
      if t.table.hasKey stack[i].term.recKey:
        t.table[stack[i].term.recKey] = Term(kind: tOp,
            op: opRecordRecursiveMerge,
            opL: t.recordLiteral[stack[i].entryKey],
            opR: stack[i].entryVal)
            opL: t.table[stack[i].term.recKey],
            opR: stack[i].term.recVal)
      else:
        t.recordLiteral.add(stack[i].entryKey, stack[i].entryVal)
        t.table.add(stack[i].term.recKey, stack[i].term.recVal)
    stack.setLen(stack.len-n)
    push t

  record_literal_entry <- record_literal_normal_entry | record_literal_punned_entry

  record_literal_normal_entry <- any_label_or_some * *(whsp * '.' * whsp * any_label_or_some) * whsp * '=' * whsp * expression:
    var t = stack.pop()
    var t = pop()
    for i in countDown(capture.len.pred, 2):
      t = Term(kind: tRecordLiteral,
          recordLiteral: toTable [(move capture[i].s, t)])
    push Term(kind: tEntry, entryKey: move($1), entryVal: t)
          table: toTable [(capture[i].s, t)])
    push Term(kind: tRecordBinding, recKey: $1, recVal: t)

  record_literal_punned_entry <- any_label_or_some * !(whsp * ':') * 0:
    var t = Term(kind: tVar, varName: $1)
    push Term(kind: tEntry, entryKey: $1, entryVal: t)
    push Term(kind: tRecordBinding, recKey: $1, recVal: t)

  union_type <- '<' * whsp * ?( '|' * whsp ) * (non_empty_union_type | empty_union_type) * whsp * '>'

  empty_union_type <- 0:
    push Term(kind: tUnionType, union: initTable[string, Term](2))
    push Term(kind: tUnionType, table: initTable[string, Term](2))

  non_empty_union_type <- union_type_entry * *(whsp * >'|' * whsp * union_type_entry) * ?( whsp * '|' ):
    let n = capture.len
    let pos = capture[0].si
    var n: int
    while n < stack.len and
        stack[stack.high-n].pos >= pos and
        stack[stack.high-n].term.kind == tRecordBinding:
      inc n
    var t = Term(kind: tUnionType,
        union: initTable[string, Term](nextPowerOfTwo n))
        table: initTable[string, Term](nextPowerOfTwo n))
    for i in stack.len-n..stack.high:
      validate(not t.union.hasKey(stack[i].entryKey))
      t.union.add(stack[i].entryKey, stack[i].entryVal)
      validate(not t.table.hasKey(stack[i].term.recKey))
      t.table.add(stack[i].term.recKey, stack[i].term.recVal)
    stack.setLen(stack.len-n)
    push t

  union_type_entry <- any_label_or_some * ?( whsp * >':' * whsp1 * expression ):
    push Term(kind: tEntry,
        entryKey: move($1),
        entryVal: case capture.len
            of 2: nil
            of 3: stack.pop()
            else: fail())

  non_empty_list_literal <- '[' * whsp * ?( ',' * whsp ) * expression * whsp * *(>',' * whsp * expression * whsp) * ?( ',' * whsp ) * ']':
  union_type_entry <- any_label_or_some * ?(whsp * >':' * whsp1 * expression):
    let t = Term(kind: tRecordBinding,
        recKey: $1,
        recVal: case capture.len
      of 2: nil
      of 3: pop()
      else: fail())
    push(t)

  non_empty_list_literal <- '[' * whsp * ?( ',' * whsp ) * expression * whsp * *(',' * whsp * expression * whsp) * ?( ',' * whsp ) * ']':
    let pos = capture[0].si
    var n: int
    while n < stack.len and
        stack[stack.high-n].pos > pos:
      inc n
    let
      n = capture.len
      off = stack.len-n
      t = Term(kind: tList, list: newSeq[Term](n))
    for i in 0..<n:
      t.list[i] = move stack[off+i]
    stack[off] = t
      t.list[i] = stack[off+i].term
    stack[off].term = t
    stack.setLen(succ off)

  nonreserved_label <- >(builtin * +simple_label_next_char) | (!builtin * label)


@@ 743,64 745,63 @@ let parser = peg("final_expression", stack: seq[Term]):
  simple_label_first_char <- Alpha | '_'
  simple_label_next_char <- Alnum | '-' | '/' | '_'
  simple_label <- >( (keyword * +simple_label_next_char) |
      (!keyword * simple_label_first_char * *simple_label_next_char) )

  If       <- "if"
  Then     <- "then"
  Else     <- "else"
  Let      <- "let"
  In       <- "in"
  As       <- "as"
  Using    <- "using"
  merge    <- "merge"
      (!keyword * simple_label_first_char * *simple_label_next_char))

  If <- "if"
  Then <- "then"
  Else <- "else"
  Let <- "let"
  In <- "in"
  As <- "as"
  Using <- "using"
  merge <- "merge"
  Infinity <- "Infinity"
  NaN      <- "NaN"
  Some     <- "Some"
  toMap    <- "toMap"
  Assert   <- "assert"
  forall   <- "∀" | "forall"
  with     <- "with"
  NaN <- "NaN"
  Some <- "Some"
  toMap <- "toMap"
  Assert <- "assert"
  forall <- "∀" | "forall"
  with <- "with"

  keyword <- If | Then | Else | Let | In | As | Using | merge | "missing" | Infinity | NaN | Some | toMap | Assert | forall | with
  keyword <- If | Then | Else | Let | In | Using | "missing" | Assert | As | Infinity | NaN | merge | Some | toMap | forall | with

  Optional <- "Optional"
  Text     <- "Text"
  List     <- "List"
  Text <- "Text"
  List <- "List"
  Location <- "Location"

  Bool    <- "Bool"
  True    <- "True"
  False   <- "False"
  None    <- "None"
  Bool <- "Bool"
  True <- "True"
  False <- "False"
  None <- "None"
  Natural <- "Natural"
  Integer <- "Integer"
  Double  <- "Double"
  Type    <- "Type"
  Kind    <- "Kind"
  Sort    <- "Sort"
  Natural_fold      <- "Natural/fold"
  Natural_build     <- "Natural/build"
  Natural_isZero    <- "Natural/isZero"
  Natural_even      <- "Natural/even"
  Natural_odd       <- "Natural/odd"
  Double <- "Double"
  Type <- "Type"
  Kind <- "Kind"
  Sort <- "Sort"
  Natural_fold <- "Natural/fold"
  Natural_build <- "Natural/build"
  Natural_isZero <- "Natural/isZero"
  Natural_even <- "Natural/even"
  Natural_odd <- "Natural/odd"
  Natural_toInteger <- "Natural/toInteger"
  Natural_show      <- "Natural/show"
  Natural_subtract  <- "Natural/subtract"
  Integer_toDouble  <- "Integer/toDouble"
  Integer_show      <- "Integer/show"
  Integer_negate    <- "Integer/negate"
  Integer_clamp     <- "Integer/clamp"
  Double_show       <- "Double/show"
  List_build        <- "List/build"
  List_fold         <- "List/fold"
  List_length       <- "List/length"
  List_head         <- "List/head"
  List_last         <- "List/last"
  List_indexed      <- "List/indexed"
  List_reverse      <- "List/reverse"
  Optional_fold     <- "Optional/fold"
  Optional_build    <- "Optional/build"
  Text_show         <- "Text/show"
  Natural_show <- "Natural/show"
  Natural_subtract <- "Natural/subtract"
  Integer_toDouble <- "Integer/toDouble"
  Integer_show <- "Integer/show"
  Integer_negate <- "Integer/negate"
  Integer_clamp <- "Integer/clamp"
  Double_show <- "Double/show"
  List_build <- "List/build"
  List_fold <- "List/fold"
  List_length <- "List/length"
  List_head <- "List/head"
  List_last <- "List/last"
  List_indexed <- "List/indexed"
  List_reverse <- "List/reverse"
  Text_show <- "Text/show"
  Text_replace <- "Text/replace"

  combine <- "∧" | "/\\"
  combine_types <- "⩓" | "//\\\\"


@@ 816,7 817,7 @@ let parser = peg("final_expression", stack: seq[Term]):

  integer_builtin <- Integer_toDouble | Integer_show | Integer_negate | Integer_clamp | Integer

  builtin <- list_builtin | natural_builtin | integer_builtin | Double_show | Optional_fold | Optional_build | Text_show | Bool | True | False | Optional | None | Double | Text | Type | Kind | Sort
  builtin <- list_builtin | natural_builtin | integer_builtin | Double_show | Text_show | Text_replace | Bool | True | False | Optional | None | Double | Text | Type | Kind | Sort
  tab <- '\t'

  end_of_line <- '\n' | "\r\n" # fuck off windows


@@ 868,15 869,36 @@ let parser = peg("final_expression", stack: seq[Term]):
    exclude(0xffffe, 0xfffff)
    exclude(0x10fffe, 0x10ffff)

proc parse*(code: string): Term =
  var stack = newSeqOfCap[Term](32)
proc parseDhall*(code: string): Term {.gcsafe.} =
  if code == "":
    # The code is misssing.
    return newMissing()
  var stack = newSeqOfCap[Frame](32)
    # TODO: how big does this stack grow?
  let match = parser.match(code, stack)
  if not match.ok:
    raise newException(ValueError, "parse did not match")
    raise newException(ValueError, "failed to parse Dhall expression")
  assert(stack.len == 1, "parser did not backtrack during match")
  stack.pop()
  pop()

when isMainModule:
  let str = newFileStream(stdin)
  echo str.readAll.parse
  import ./binary, ./render, ./resolution
  import std/nimprof, std/times
  let buf = stdin.readAll
  if buf != "":
    let
      a = cpuTime()
      term = parseDhall(buf)
      b = cpuTime()
    echo "parse time: ", b - a
    let
      c = cpuTime()
      bin = term.encode
      d = cpuTime()
    echo "encode time: ", d - c
    let
      e = cpuTime()
      dec = bin.decodeDhall
      f = cpuTIme()
    echo "decode time: ", f - e
    stdout.write $term.semanticHash, "\n"

A src/dhall/quotation.nim => src/dhall/quotation.nim +46 -0
@@ 0,0 1,46 @@
import ./terms

import std/tables

type QuoteContext = Table[string, int]

func extend(ctx: QuoteContext; label: string): QuoteContext =
  result = ctx
  result.mgetOrPut(label, 0).inc()

func quote(ctx: QuoteContext; v: Value; form: Form): Term =
  result = walk[Value, Term](v) do (v: Value) -> Term:
    case v.kind
    of tLambdaCallback, tPiCallback:
      let
        label = if form == alpha: "_" else: v.callbackLabel
        qv = Value(kind: tQuoteVar,
            varName: label, varIndex: ctx.getOrDefault(label))
      let body = v.callback(qv)
      result = Term(kind:
        if v.kind == tPiCallback: tPi
        else: tLambda)
      result.funcLabel = label
      result.funcType = quote(ctx, v.domain, form)
      result.funcBody = quote(ctx.extend(label), body, form)
    of tFreeVar:
      result = Term(kind: tVar,
          varName: v.varName, varIndex: v.varIndex)
    of tQuoteVar:
      let name = v.varName
      result = Term(kind: tVar,
          varName: name,
          varIndex: ctx.getOrDefault(name) - v.varIndex - 1)
    of tBuiltin:
      result = newTerm(v.builtin)
      for arg in v.builtinArgs:
        result = newApp(result, quote(ctx, arg, form))
    of  tLambda, tPi:
      assert(false, "tVar invalid for quote")
    else:
      discard
  assert(result.kind != tPi or result.funcLabel != "")
  assert(result.kind != tPiCallback or result.callbackLabel != "")

func quote*(v: Value; form = Form.beta): Term =
  quote(initTable[string, int](), v, form)

M src/dhall/render.nim => src/dhall/render.nim +116 -65
@@ 1,50 1,64 @@
import ./term
import ./quotation, ./terms

import bigints

import std/options, std/strutils, std/tables
import std/algorithm, std/asyncfutures, std/math, std/options, std/strutils, std/tables

func quoteLabel(s: string): string =
  case s
  of "", "if", "then", "else", "let", "in", "as", "using", "merge", "Infinity", "NaN", "Some", "toMap", "assert", "∀", "forall", "with":
    "`" & s & "`"
  else: s

iterator sortedPairs(n: Node): (string, Node) =
  var keys = newSeqOfCap[string](n.table.len)
  for key in n.table.keys:
    keys.add(key)
  sort(keys)
  for key in keys:
    yield((quoteLabel(key), n.table[key]))

func `$`*(t: Term): string =
  if t.isNil: return "null"
  case t.kind:
  of tUniverse:
    result = $t.universe
  of tBuiltin:
    result = $t.builtin
  of tBoolLiteral:
    result = if t.bool: "True" else: "False"
  of tVar:
    if t.varIndex > 0:
      result = t.varName & "@" & $t.varIndex
  of tVar, tFreeVar, tLocalVar, tQuoteVar:
    assert(t.varName != "")
    if t.varIndex != 0:
      result.add(t.varName & "@" & $t.varIndex)
    else:
      result = t.varName
      result.add(t.varName)
  of tLambda:
    result = "(λ(" & t.lambdaLabel & " : " & $t.lambdaType & ") → " &
        $t.lambdaBody & ")"
    result = "λ($# : $#) → $#" %
      [ $t.funcLabel, $t.funcType, $t.funcBody]
  of tPi:
    if t.piLabel == "_":
      result = $t.piType & " → " & $t.piBody
    if t.funcLabel == "_":
      result = $t.funcType & " → " & $t.funcBody
    else:
      result = "∀(" & t.piLabel & " : " & $t.piType & ") → " & $t.piBody
      result = "∀($# : $#) → $#" %
        [ $t.funcLabel, $t.funcType, $t.funcBody]
  of tApp:
    result = "(" & $t.appFun
    for arg in t.appArgs:
      result.add(" ")
      result.add($arg)
    result.add(" )")
    case t.appArg.kind
    of tLambda:
      result = "$# ($#)" % [ $t.appFun, $t.appArg]
    else:
      result = "$# $#" % [ $t.appFun, $t.appArg]
  of tOp:
    result = "(" & $t.opL & " " & $t.op & " " & $t.opR & ")"
  of tLet:
    result = ""
    for b in t.letBinds:
      result.add("let ")
      result.add(b.key)
      if not b.ann.isNil:
        result.add(": ")
        result.add($b.ann)
      result.add(quoteLabel(b.letKey))
      if b.letAnn.isSome:
        result.add(" : " & $b.letAnn.get)
      result.add(" = ")
      result.add($b.val)
    result.add(" in ")
      result.add($b.letVal)
      result.add(" ")
    result.add("in ")
    result.add($t.letBody)
  of tAnnotation:
    result = $t.annExpr & " : " & $t.annAnn


@@ 52,7 66,7 @@ func `$`*(t: Term): string =
    result = $t.natural
  of tList:
    if t.list.len == 0:
      result = "[] : " & $t.listType
      result = "[] : List " & $t.listType.get
    else:
      result = "[ " & join(t.list, ", ") & " ]"
  of tTextLiteral:


@@ 75,63 89,68 @@ func `$`*(t: Term): string =
  of tAssert:
    result = "assert : " & $t.assertAnn
  of tImport:
    result = "import "
    result.add case t.importKind
      of iCode: ""
      of iText: "as Text "
      of iLocation: "as Location "
    result.add case t.importScheme
      of 0: "http://"
      of 1: "https://"
      of 2: "/"
      of 3: "./"
      of 4: "../"
      of 5: "~/"
      of 6: "env:"
      of 7: "missing"
      else: raiseAssert("unhandled import scheme " & $t.importScheme)
      of iHttp: "http://"
      of iHttps: "https://"
      of iAbs: "/"
      of iHere: "./"
      of iParent: "../"
      of iHome: "~/"
      of iEnv: "env:"
      of iMiss: "missing"
    result.add(join(t.importElements, "/"))
    if t.importQuery.isSome:
      result.add("?")
      result.add(t.importQuery.get)
    if not t.importCheck.len == 0:
    if t.importCheck != @[]:
      assert(t.importCheck.len == 32)
      result.add " sha256:"
      for i in 2..31:
        result.add t.importCheck[i].toHex
      for b in t.importCheck:
        result.add b.toHex.toLowerAscii
  of tIf:
    result = "if " & $t.ifCond & " then " & $t.ifTrue & " else " & $t.ifFalse
  of tDoubleLiteral:
    result = $t.double
    case t.double.classify
    of fcNormal, fcSubnormal:
      result = $t.double
    of fcZero:
      result = "+0.0"
    of fcNegZero:
      result = "-0.0"
    of fcNan:
      result = "NaN"
    of fcInf:
      result = "Infinity"
    of fcNegInf:
      result = "-Infinity"
  of tIntegerLiteral:
    result = if t.integer > 0:
    result = if bigints.`<`(0'i32, t.integer):
        "+" & $t.integer
      else: $t.integer
  of tSome:
    result = "Some " & $t.someVal
  of tRecordType:
    if t.recordType.len == 0:
    if t.table.len == 0:
      result = "{}"
    else:
      result = "{ "
      for key, val in t.recordType.pairs:
        if key == "" or key.startsWith(' ') or key.endsWith(' '):
          # TODO: builtin labels
          result.add "`"
          result.add(key)
          result.add "`"
        else:
          result.add(key)
      for key, val in t.sortedPairs:
        result.add(key)
        result.add(" : ")
        result.add($val)
        result.add(", ")
      result[^2] = ' '
      result[^1] = '}'
  of tRecordLiteral:
    if t.recordLiteral.len == 0:
    if t.table.len == 0:
      result = "{=}"
    else:
      result = "{ "
      for key, val in t.recordLiteral.pairs:
      for key, val in t.sortedPairs:
        result.add(key)
        result.add(" = ")
        result.add($val)


@@ 139,12 158,18 @@ func `$`*(t: Term): string =
      result[^2] = ' '
      result[^1] = '}'
  of tToMap:
    if t.toMapAnn.isNil:
      result = "toMap " & $t.toMapBody
    else:
      result = "toMap " & $t.toMapBody & " : " & $t.toMapAnn
    result = "toMap " & $t.toMapBody
    if t.toMapAnn.isSome:
      result.add(" : " & $t.toMapAnn.get)
  of tEmptyList:
    result = "[] : " & $t.emptyListType
  of tWith:
    result = $t.withExpr & " with " & t.withFields[0]
    for i in 1..t.withFields.high:
      result.add '.'
      result.add t.withFields[i]
    result.add " = "
    result.add $t.withUpdate
  of tField:
    result = "(" & $t.fieldRecord & ")." & t.fieldName
  of tProject:


@@ 152,27 177,53 @@ func `$`*(t: Term): string =
  of tProjectType:
    result = $t.projectTypeRecord & ".(" & $t.projectTypeSelector & ")"
  of tUnionType:
    if t.union.len == 0:
    if t.table.len == 0:
      result = "<>"
    else:
      result = "< "
      for key, val in t.union.pairs:
      for key, val in t.sortedPairs:
        result.add(key)
        if not val.isNil:
          result.add(" : ")
          result.add($val)
        result.add(" | ")
      result[^2] = ' '
      result[^1] = '>'
      result.setLen(result.high)
      result[result.high] = '>'
  of tMerge:
    if t.mergeAnn.isNil:
    if t.mergeAnn.isNone:
      result = "merge (" & $t.mergeHandler & ") (" & $t.mergeUnion & ")"
    else:
      result = "merge (" & $t.mergeHandler & ") (" & $t.mergeUnion &
          ") : " & $t.mergeAnn
  of tEntry:
    result = "« " & $t.entryKey & " = " & $t.entryVal & " »"
          ") : " & $t.mergeAnn.get
  of tTextChunk:
    result = t.textPrefix & "${" & $t.textExpr & "}"
  of tBinding:
    result = "« " & $t.key & " = " & $t.val & " »"
  of tRecordBinding:
    result = "« " & $t.recKey & " = " & $t.recVal & " »"
  of tLetBinding:
    if t.letAnn.isNone:
      result = "« $# = $# »" % [ $t.letKey, $t.letVal]
    else:
      result = "« $# = $# : $# »" % [ $t.letKey, $t.letVal, $t.letAnn]

  of tFuture:
    if t.future.finished:
      if t.future.failed:
        result = "«" & t.future.readError.msg & "»"
      else:
        result = "«" & $t.future.read & "»"
    else:
      when not defined(release):
        result = "«" & $t.source & "»"
      else:
        result = "«…»"
  of tLambdaCallback:
    result = "λ($# : $#) → «…»" %
      [ $t.callbackLabel, $t.domain]
  of tPiCallback:
    if t.callbackLabel == "_":
      result = $t.domain & " → «…»"
    else:
      result = "∀($# : $#) → «…»" %
        [ $t.callbackLabel, $t.domain ]

func `$`*(v: Value): string = $quote(v)

A src/dhall/resolution.nim => src/dhall/resolution.nim +392 -0
@@ 0,0 1,392 @@
import ./binary, ./normalization, ./parse, ./quotation, ./render, ./type_inference, ./terms

import nimSHA2

import std/asyncdispatch, std/asyncfile, std/hashes,
    std/httpclient, std/math, std/options, std/os, std/strutils,
    std/tables, std/unicode, std/uri

type SemanticHash* = SHA256Digest

func `$`*(h: SemanticHash): string =
  "sha256:" & h.toHex.toLower

func `==`*(s: seq[byte]; a: SemanticHash): bool =
  if s.len == a.len:
    for i, b in s:
      if a[i] != b.char: return false
    result = true

proc semanticHash(bin: string): SemanticHash =
  var ctx: SHA256
  ctx.initSHA()
  ctx.update bin
  ctx.final()

proc semanticHash*(expr: Term): SemanticHash =
  ## Generate a hash of an expression.
  ## Semantic hashes are only valid for α-normalized expressions.
  expr.encode.semanticHash

type
  Link = ref object
    uri: Uri
    headers: Option[HttpHeaders]
    scheme: ImportScheme
    futures: seq[Future[Term]]
    chain: seq[Hash]

  CachedImport = object
    code: string
    term: Option[Term]

  ImportCache* = Table[Link, FutureVar[CachedImport]]
    ## Type for caching imports during evaluation.
    ## This is to ensure that importing the same path
    ## twice resolves to the same expression.
    ## Note that this is an in-memory cache and is
    ## distinct from expressions protected by an
    ## integrity check and cached at the file-system.

  Resolver = ref object
    ## Import caching object.
    cache: ImportCache
    warn*: proc (msg: string) {.gcsafe.}

func hash(link: Link): Hash =
  var h = hash(link.scheme) !& hash($link.uri)
  link.headers.map do (hh: HttpHeaders): h = h !& hash($hh)
  !$h

when defined(posix):
  proc defaultWarn(msg: string) =
    stderr.writeLine(msg)

proc newResolver(): Resolver =
  Resolver(
    cache: initTable[Link, FutureVar[CachedImport]](),
    warn: defaultWarn)

# TODO: don't cache gigantic imports, just hash them and ensure
# the hash matches for successive imports

proc cacheDir(): string =
  when defined(genode):
    "/cache/dhall"
  else:
    for key in ["XDG_CACHE_HOME", "HOME", "LOCALAPPDATA"]:
      if existsEnv key:
        result = getEnv(key) / "dhall"
        break

proc checkReferentiallySanity(link: Link; t: Term) =
  const
    transparent = {iHttp, iHttps, iMiss}
    opaque = {iAbs, iHome, iEnv}
  if link.scheme in transparent and t.importScheme in opaque:
    raise newException(ImportError,
      "referential sanity check failed for importing " & $t &
      " from " & $link.scheme & " import")

proc resolve(state: Resolver; link: Link; expr: Term): Term {.gcsafe.}

proc next(link: Link; t: Term): Link =
  result = Link(uri: link.uri, headers: link.headers, scheme: link.scheme)
  case t.importScheme
  of iHttp, iHttps:
    result.scheme = t.importScheme
    result.uri.scheme = $result.scheme
    result.uri.hostname = t.importElements[0]
    result.uri.path =
      t.importElements[1..t.importElements.high].joinPath.normalizedPath
    result.uri.query = t.importQuery.get("")
    if t.importHeaders.isSome:
      if result.uri.hostname != link.uri.hostname:
        # Do not reuse headers across domains
        result.headers = some newHttpHeaders()
      elif result.headers.isNone:
        result.headers = some newHttpHeaders()
      let ht = t.importHeaders.get
      assert(ht.isList)
      for e in ht.list.items:
        assert(e.isRecordLiteral)
        assert(e.table.len == 2)
        let key = e.field("mapKey")
        let val = e.field("mapValue")
        if not (key.isSimpleText and val.isSimpleText):
          raise newException(ImportError, "invalid import headers")
        get(result.headers)[key.textSuffix] = val.textSuffix
  of iEnv:
    result.scheme = t.importScheme
    result.uri.path = t.importElements.joinPath
  of iAbs:
    result.scheme = t.importScheme
    result.uri.path = "/" & t.importElements.joinPath
    normalizePath result.uri.path
  of iHere:
    result.uri.path = joinPath(
      @[result.uri.path.parentDir] & t.importElements)
  of iParent:
    result.uri.path = joinPath(
      @[result.uri.path.parentDir, ".."] & t.importElements)
  of iHome:
    result.scheme = t.importScheme
    result.uri.path = getHomeDir() / t.importElements.joinPath
  of iMiss:
    result.scheme = t.importScheme
  result.chain = link.chain & @[link.hash]

proc loadUncached(state: Resolver; link: Link; t: Term; cacheFut: FutureVar[
    CachedImport]) =
  case link.scheme
  of iHttp, iHttps:
    let client = newAsyncHttpClient(userAgent = "dhall")
    link.headers.map do (h: HttpHeaders):
      client.headers = h
    client.getContent($link.uri).addCallback do (codeFut: Future[string]):
      close client
      cacheFut.complete CachedImport(code: codeFut.read())
  of iAbs, iHere, iParent, iHome:
    try:
      let
        file = openAsync(link.uri.path)
      file.readAll.addCallback do (codeFut: Future[string]):
        close file
        cacheFut.complete CachedImport(code: codeFut.read())
    except OSError:
      cacheFut.complete CachedImport(term: some newMissing())
      state.warn("could not import " & link.uri.path & ", " &
          getCurrentExceptionMsg())
  of iEnv:
    let code = getEnv(link.uri.path)
    let cached =
      if code == "": CachedImport(term: some newMissing())
      else: CachedImport(code: code)
    cacheFut.complete cached
  of iMiss:
    assert(not t.isMissing, "cannot resolve missing import")
  # TODO: save protected imports to FS cache

proc loadCachedOrUncached(state: Resolver; link: Link;
    t: Term; cacheFut: FutureVar[CachedImport]) =
  let key = t.importCheck
  if key.len == 32:
    let cacheDir = cacheDir()
    if cacheDir != "":
      var cachePath = newStringOfCap(cacheDir.len + 1 + key.len*2)
      cachePath.add(cacheDir)
      cachePath.add(DirSep & "1220")
      for b in key: cachePath.add b.toHex.toLowerAscii
        # just reimplement hex encoding, fuck this uppercase stuff
      try:
        var file = openAsync(cachePath)
        proc cb(dataFut: Future[string]) =
          close file
          let buf = read dataFut
          let digest = computeSHA256(buf)
          for i in 0..31:
            if digest[i].byte != key[i]:
              let msg = "corrupt cache entry: " & cachePath
              state.warn(msg)
              loadUncached(state, link, t, cacheFut)
              return
          cacheFut.complete CachedImport(term: some buf.decodeDhall)
        file.readAll.addCallback(cb)
        return
      except OSError:
        if osLastError() != OSErrorCode(2):
          # missing file?
          state.warn("failed to load " & cachePath & ": " &
              getCurrentExceptionMsg())
  loadUncached(state, link, t, cacheFut)

proc saveCache(state: Resolver; binary: string; key: SemanticHash): Future[void] =
  let cacheDir = cacheDir()
  if cacheDir != "":
    var cachePath = newStringOfCap(cacheDir.len + 1 + key.len*2)
    cachePath.add(cacheDir)
    cachePath.add(DirSep & "1220")
    cachePath.add(key.toHex.toLowerAscii)
    try:
      let file = openAsync(cachePath, fmWrite)
      result = file.write(binary)
      result.addCallback:
        close file
    except:
      state.warn("failed to save " & cachePath & ": " &
          getCurrentExceptionMsg())

proc resolveImport(state: Resolver; link: Link; t: Term): Term =
  result = Term(kind: tFuture,
      source: t, future: newFuture[Term]("resolveImport"))
  let termFut = result.future
  var cacheFut: FutureVar[CachedImport]
  if state.cache.hasKey(link):
    cacheFut = state.cache[link]
  else:
    cacheFut = newFutureVar[CachedImport]("resolveImport")
    state.cache[link] = cacheFut
    loadCachedOrUncached(state, link, t, cacheFut)
  proc cb() {.gcsafe.} =
    proc completeTerm(e: Term) {.gcsafe.} =
      if e.isMissing:
        termFut.fail newException(ImportError, $t)
      else:
        assert(e.kind notin {tImport, tFuture}, $e)
        block:
          discard e.inferType
        try:
          if t.importCheck != @[]:
            let alpha = e.toBeta.toAlpha
            let hash = alpha.semanticHash
              # TODO: memioize?
            if t.importCheck != hash:
              let msg = "hash mismatch for " & $link.uri
              state.warn(msg)
              termFut.fail newException(ImportError, msg)
              return
          termFut.complete e
        except TypeError:
          let msg = getCurrentExceptionMsg()
          state.warn("type-check failed of import " & $t)
          fail(termFut, newException(ImportError, msg))
    var cache = mget cacheFut
    assert(cache.code != "" or cache.term.isSome,
      "cache entry has neither code nor term")
    case t.importKind
    of iCode:
      if cache.term.isSome:
        completeTerm cache.term.get
      else:
        try:
          var expr = cache.code.parseDhall
          expr = resolve(state, link, expr)
          if link.futures == @[]:
            cache.term = some expr
            completeTerm expr
          else:
            var pendingCount = link.futures.len
            let importsCallback = proc () =
              dec pendingCount
              if pendingCount == 0:
                var expr = resolve(state, link, expr)
                if expr.isFuture:
                  assert(expr.future.finished, $expr)
                  expr = expr.future.read
                block:
                  cache.term = some expr
                  completeTerm expr
            for f in link.futures:
              f.addCallback(importsCallback)
        except ValueError:
          let e = getCurrentException()
          cache.term = some newMissing()
          termFut.fail e
    of iText:
      if cache.term.isSome and cache.term.get.isMissing:
        completeTerm cache.term.get
      else:
        if cache.code == "":
          cache.code = $cache.term.get
        completeTerm Term(kind: tTextLiteral, textSuffix: cache.code)
    else:
      assert(false, "resolveImport called on location import")
  if cacheFut.finished:
    cb()
  else: cast[FutureBase](cacheFut).addCallback(cb)

proc importLocation(link: Link): Term =
  let
    Text = newTerm bText
    union = Term(kind: tUnionType,
        table: toTable([("Environment", Text), ("Local", Text), ("Missing", nil), ("Remote", Text)]))
  result = case link.scheme
    of iHttp, iHttps:
      union.newField("Remote").newApp(newTerm($(link.uri)))
    of iAbs:
      union.newField("Local").newApp(
        newTerm(link.uri.path))
    of iHere, iParent:
      union.newField("Local").newApp(
        newTerm("./" & link.uri.path.relativePath(getCurrentDir())))
    of iHome:
      union.newField("Local").newApp(
        newTerm("~/" & link.uri.path.relativePath(getHomeDir())))
    of iEnv:
      union.newField("Environment").newApp(newTerm(link.uri.path))
    of iMiss:
      union.newField "Missing"

proc resolve(state: Resolver; link: Link; expr: Term): Term {.gcsafe.} =
  walk(expr) do (expr: Term) -> Term:
    case expr.kind
    of tOp:
      if expr.op == opAlternateImport:
        # Eliminate the `?` operator during resolution
        try:
          let opL = resolve(state, link, expr.opL)
          if opL.isFuture:
            let res = Term(kind: tFuture,
              source: expr,
              future: newFuture[Term]("opAlternateImport"))
            opL.future.addCallback do (fut: Future[Term]):
              if not fut.failed:
                res.future.complete(fut.read())
              else:
                let opR = resolve(state, link, expr.opR)
                if opR.isFuture:
                  opR.future.addCallback do (fut: Future[Term]):
                    if fut.failed:
                      res.future.fail(fut.readError())
                    else:
                      res.future.complete(fut.read())
                else: res.future.complete(opR)
            link.futures.add(res.future)
            result = res
          else:
            result = opL
        except ImportError:
          result = resolve(state, link, expr.opR)
    of tImport:
      if expr.importKind == iLocation:
        result = importLocation(link.next(expr))
      elif expr.isMissing and expr.importCheck == @[]:
        raise newException(ImportError, "")
      else:
        let nextLink = link.next(expr)
        if nextLink.hash in nextLink.chain:
          raise newException(ImportError, "import cycle detected")
        checkReferentiallySanity(link, expr)
        result = resolveImport(state, nextLink, expr)
        link.futures.add result.future
    else:
      discard

proc resolve*(expr: Term; workingDir = "."): Future[Term] =
  ## Resolve the import terms of an expression.
  let
    initialDir =
      if workingDir.isAbsolute: workingDir
      else: getCurrentDir() / workingDir
    state = newResolver()
    link = Link(uri: Uri(path: initialDir / "_"), scheme: iHere)
  var expr = resolve(state, link, expr)
  while expr.isFuture and expr.future.finished and not expr.future.failed:
    expr = expr.future.read
  if expr.isFuture:
    result = expr.future
  else:
    result = newFuture[Term]("resolve")
    if link.futures == @[]:
      # term is fully resolved
      result.complete(expr)
    else:
      # top of term is ready but there are pending imports
      let finalFut = result
      var pending = link.futures.len
      for fut in link.futures:
        fut.addCallback do:
          dec(pending)
          if pending == 0:
            finalFut.complete(expr)
      assert(not result.finished)

A src/dhall/substitutions.nim => src/dhall/substitutions.nim +63 -0
@@ 0,0 1,63 @@
import ./terms

func shift[Node: Term|Value](expr: Node; d: int; name: string; m = 0): Node =
  assert(d == -1 or d == 1)
  # TODO: constrain d to -1 or 1 by type
  result = walk(expr) do (expr: Node) -> Node:
    case expr.kind
    of tLambda, tPi:
      result = Node(kind: expr.kind)
      result.funcLabel = expr.funcLabel
      result.funcType = expr.funcType.shift(d, name, m)
      result.funcBody =
        if expr.funcLabel == name:
          expr.funcBody.shift(d, name, m+1)
        else:
          expr.funcBody.shift(d, name, m)
    of tLet:
      result = Node(kind: tLet, letBinds: newSeq[Node](expr.letBinds.len))
      var m = m
      for i, b in expr.letBinds:
        result.letBinds[i] = b.shift(d, name, m)
        if b.letKey == name: inc m
      result.letBody = expr.letBody.shift(d, name, m)
    of tFreeVar:
      result = Node(kind: tFreeVar,
          varName: expr.varName,
          varIndex: expr.varIndex)
      if expr.varName == name and expr.varIndex >= m:
        result.varIndex = max(0, result.varIndex + d)
    else: discard

func substitute*[Node: Term|Value](
    expr: Node; name: string; val: Node; level = 0): Node =
  assert(not expr.isNil)
  assert(0 <= level)
  result = walk(expr) do (expr: Node) -> Node:
    case expr.kind
    of tLambda, tPi:
      result = Node(kind: expr.kind)
      result.funcLabel = expr.funcLabel
      result.funcType = expr.funcType.substitute(name, val, level)
      var val = val.shift(1, expr.funcLabel)
      if expr.funcLabel == name:
        result.funcBody = expr.funcBody.substitute(name, val, level+1)
      else:
        result.funcBody = expr.funcBody.substitute(name, val, level)
    of tLet:
      var val = val
      var level = level
      result = Node(kind: tLet,
          letBinds: newSeq[Node](expr.letBinds.len))
      for i, b in expr.letBinds:
        result.letBinds[i] = b.substitute(name, val, level)
        if b.letKey == name: inc level
        val = val.shift(1, b.letKey)
      result.letBody = expr.letBody.substitute(name, val, level)
    of tVar, tFreeVar, tLocalVar, tQuoteVar:
      # TODO: don't need to handle all of these, localize this proc in some other module
      if expr.varName == name and expr.varIndex == level:
        deepCopy(result, val)
      else:
        result = expr
    else: discard

D src/dhall/term.nim => src/dhall/term.nim +0 -299
@@ 1,299 0,0 @@
import bigints

import std/options, std/strutils, std/tables

type
  UniverseKind* = enum
    uType = "Type", uKind = "Kind", uSort = "Sort"

  BuiltinKind* = enum
    bNaturalBuild = "Natural/build",
    bNaturalFold = "Natural/fold",
    bNaturalIsZero = "Natural/isZero",
    bNaturalEven = "Natural/even",
    bNaturalOdd = "Natural/odd",
    bNaturalToInteger = "Natural/toInteger",
    bNaturalShow = "Natural/show",
    bNaturalSubtract = "Natural/subtract",
    bIntegerDouble = "Integer/toDouble",
    bIntegerShow = "Integer/show",
    bIntegerNegate = "Integer/negate",
    bIntegerClamp = "Integer/clamp",
    bDoubleShow = "Double/show",
    bListBuild = "List/build",
    bListFold = "List/fold",
    bListLength = "List/length",
    bListHead = "List/head",
    bListLast = "List/last",
    bListIndexed = "List/indexed",
    bListReverse = "List/reverse",
    bOptionalBuild = "Optional/build",
    bOptionalFold = "Optional/fold",
    bTextShow = "Text/show",
    bBool = "Bool",
    bOptional = "Optional",
    bNatural = "Natural",
    bInteger = "Integer",
    bDouble = "Double",
    bText = "Text",
    bList = "List",
    bTrue = "True",
    bFalse = "False",
    bNone = "None",
    bType = "Type",
    bKind = "Kind",
    bSort = "Sort"

  OpKind* = enum
    opBoolOr = (0, "||"),
    opBoolAnd = (1, "&&"),
    opBoolEquality = (2, "=="),
    opBoolInequality = (3, "!="),
    opNaturalAdd = (4, "+"),
    opNaturalMultiplication = (5, "*"),
    opTextAppend = (6, "++"),
    opListAppend = (7, "#"),
    opRecordRecursiveMerge = (8, "∧"),
    opRecordBiasedMerge = (9, "⫽"),
    opRecordTypeMerge = (10, "⩓"),
    opAlternateImport = (11, "?"),
    opEquivalience = (12, "≡"),
    opComplete = (13, "::")

  ImportKind* = enum
    iCode = 0,
    iText = 1,
    iLocation = 2

  TermKind* = enum
    tApp = 0,
    tLambda = 1,
    tPi = 2,
    tOp = 3,
    tList = 4,
    tSome = 5,
    tMerge = 6,
    tRecordType = 7,
    tRecordLiteral = 8,
    tField = 9,
    tProject = 10,
    tUnionType = 11,
    tIf = 14,
    tNaturalLiteral = 15,
    tIntegerLiteral = 16,
    tTextLiteral = 18,
    tAssert = 19,
    tImport = 24,
    tLet = 25,
    tAnnotation = 26,
    tToMap = 27
    tEmptyList = 28
    tVar,
    tBuiltin,
    tUniverse,
    tProjectType,
    tBoolLiteral,
    tDoubleLiteral,

    tEntry,
    tTextChunk,
    tBinding

  Term* = ref object
    case kind*: TermKind
    of tVar:
      varName*: string
      varIndex*: int
    of tBuiltin:
      builtin*: BuiltinKind
    of tUniverse:
      universe*: UniverseKind
    of tApp:
      appFun*: Term
      appArgs*: seq[Term]
    of tLambda:
      lambdaLabel*: string
      lambdaType*, lambdaBody*: Term
    of tPi:
      piLabel*: string
      piType*, piBody*: Term
      # TODO: share these fields with tLambda?
    of tOp:
      op*: OpKind
      opL*, opR*: Term
    of tList:
      listType*: Term
      list*: seq[Term]
    of tSome:
      someType*, someVal*: Term
    of tMerge:
      mergeHandler*, mergeUnion*, mergeAnn*: Term
    of tRecordType:
      recordType*: Table[string, Term]
    of tRecordLiteral:
      recordLiteral*: Table[string, Term]
    of tField:
      fieldRecord*: Term
      fieldName*: string
    of tProject:
      projectRecord*: Term
      projectNames*: seq[string]
    of tProjectType:
      projectTypeRecord*: Term
      projectTypeSelector*: Term
    of tUnionType:
      union*: Table[string, Term]
    of tBoolLiteral:
      bool*: bool
    of tIf:
      ifCond*, ifTrue*, ifFalse*: Term
    of tNaturalLiteral:
      natural*: BigInt
    of tIntegerLiteral:
      integer*: BigInt
    of tDoubleLiteral:
      double*: BiggestFloat
    of tTextLiteral:
      textChunks*: seq[Term]
      textSuffix*: string
    of tAssert:
      assertAnn*: Term
    of tImport:
      importCheck*: seq[byte]
      importKind*: ImportKind
      importScheme*: uint8
      importHeaders*: Term
      importElements*: seq[string]
      importQuery*: Option[string]
    of tLet:
      letBinds*: seq[Term] # binding terms
      letBody*: Term
    of tAnnotation:
      annExpr*, annAnn*: Term
    of tToMap:
      toMapBody*, toMapAnn*: Term
    of tEmptyList:
      emptyListType*: Term

    of tEntry:
      # TODO: probably redundant with tBinding
      entryKey*: string
      entryVal*: Term
    of tTextChunk:
      textPrefix*: string
      textExpr*: Term
    of tBinding:
      key*: string
      val*, ann*: Term

func parseBuiltin*(s: string): BuiltinKind =
  case s
  of "Natural/build": bNaturalBuild
  of "Natural/fold": bNaturalFold
  of "Natural/isZero": bNaturalIsZero
  of "Natural/even": bNaturalEven
  of "Natural/odd": bNaturalOdd
  of "Natural/toInteger": bNaturalToInteger
  of "Natural/show": bNaturalShow
  of "Natural/subtract": bNaturalSubtract
  of "Integer/toDouble": bIntegerDouble
  of "Integer/show": bIntegerShow
  of "Integer/negate": bIntegerNegate
  of "Integer/clamp": bIntegerClamp
  of "Double/show": bDoubleShow
  of "List/build": bListBuild
  of "List/fold": bListFold
  of "List/length": bListLength
  of "List/head": bListHead
  of "List/last": bListLast
  of "List/indexed": bListIndexed
  of "List/reverse": bListReverse
  of "Optional/build": bOptionalBuild
  of "Optional/fold": bOptionalFold
  of "Text/show": bTextShow
  of "Bool": bBool
  of "Optional": bOptional
  of "Natural": bNatural
  of "Integer": bInteger
  of "Double": bDouble
  of "Text": bText
  of "List": bList
  of "True": bTrue
  of "False": bFalse
  of "None": bNone
  of "Type": bType
  of "Kind": bKind
  of "Sort": bSort
  else:
    raise newException(ValueError, "invalid builtin " & s)

func `==`*(x, y: Term): bool =
  if x.isNil and y.isNil: result = true
  else:
    if x.kind == y.kind:
      template eq(field: untyped): bool = x.field == y.field
      result = case x.kind
      of tVar:
        eq(varName) and eq(varIndex)
      of tBuiltin:
        eq(builtin)
      of tUniverse:
        eq(universe)
      of tApp:
        eq(appFun) and eq(appArgs)
      of tLambda:
        eq(lambdaLabel) and eq(lambdaType) and eq(lambdaBody)
      of tPi:
        eq(piLabel) and eq(piType) and eq(piBody)
      of tOp:
        eq(op) and eq(opL) and eq(opR)
      of tList:
        eq(listType) and eq(list)
      of tSome:
        eq(someType) and eq(someVal)
      of tMerge:
        eq(mergeHandler) and eq(mergeUnion) and eq(mergeAnn)
      of tRecordType:
        eq(recordType)
      of tRecordLiteral:
        eq(recordLiteral)
      of tField:
        eq(fieldRecord) and eq(fieldName)
      of tProject:
        eq(projectRecord) and eq(projectNames)
      of tProjectType:
        eq(projectTypeRecord) and eq(projectTypeSelector)
      of tUnionType:
        eq(union)
      of tBoolLiteral:
        eq(bool)
      of tIf:
        eq(ifCond) and eq(ifTrue) and eq(ifFalse)
      of tNaturalLiteral:
        eq(natural)
      of tIntegerLiteral:
        eq(integer)
      of tDoubleLiteral:
        eq(double)
      of tTextLiteral:
        eq(textChunks) and eq(textSuffix)
      of tAssert:
        eq(assertAnn)
      of tImport:
        eq(importCheck) and eq(importKind) and eq(importScheme) and eq(
            importHeaders) and eq(importElements) and eq(importQuery)
      of tLet:
        eq(letBinds) and eq(letBody)
      of tAnnotation:
        eq(annExpr) and eq(annAnn)
      of tToMap:
        eq(toMapBody) and eq(toMapAnn)
      of tEmptyList:
        eq(emptyListType)
      of tTextChunk:
        eq(textPrefix) and eq(textExpr)
      of tBinding:
        eq(key) and eq(val) and eq(ann)
      else: false
        # the rest are only intermediate representations


A src/dhall/terms.nim => src/dhall/terms.nim +685 -0
@@ 0,0 1,685 @@
import bigints

import std/asyncfutures, std/math, std/options, std/strutils, std/tables, std/uri

type
  UniverseKind* = enum
    uType = "Type", uKind = "Kind", uSort = "Sort"

  BuiltinKind* = enum
    bNaturalBuild = "Natural/build",
    bNaturalFold = "Natural/fold",
    bNaturalIsZero = "Natural/isZero",
    bNaturalEven = "Natural/even",
    bNaturalOdd = "Natural/odd",
    bNaturalToInteger = "Natural/toInteger",
    bNaturalShow = "Natural/show",
    bNaturalSubtract = "Natural/subtract",
    bIntegerToDouble = "Integer/toDouble",
    bIntegerShow = "Integer/show",
    bIntegerNegate = "Integer/negate",
    bIntegerClamp = "Integer/clamp",
    bDoubleShow = "Double/show",
    bListBuild = "List/build",
    bListFold = "List/fold",
    bListLength = "List/length",
    bListHead = "List/head",
    bListLast = "List/last",
    bListIndexed = "List/indexed",
    bListReverse = "List/reverse",
    bTextShow = "Text/show",
    bTextReplace = "Text/replace",
    bBool = "Bool",
    bOptional = "Optional",
    bNatural = "Natural",
    bInteger = "Integer",
    bDouble = "Double",
    bText = "Text",
    bList = "List",
    bTrue = "True",
    bFalse = "False",
    bNone = "None",
    bType = "Type",
    bKind = "Kind",
    bSort = "Sort"

  OpKind* = enum
    opBoolOr = (0, "||"),
    opBoolAnd = (1, "&&"),
    opBoolEquality = (2, "=="),
    opBoolInequality = (3, "!="),
    opNaturalAdd = (4, "+"),
    opNaturalMultiplication = (5, "*"),
    opTextAppend = (6, "++"),
    opListAppend = (7, "#"),
    opRecordRecursiveMerge = (8, "∧"),
    opRecordBiasedMerge = (9, "⫽"),
    opRecordTypeMerge = (10, "⩓"),
    opAlternateImport = (11, "?"),
    opEquivalience = (12, "≡"),
    opComplete = (13, "::")

  ImportKind* = enum
    iCode = 0,
    iText = 1,
    iLocation = 2

  ImportScheme* = enum
    iHttp = (0, "http"),
    iHttps = (1, "https"),
    iAbs = (2, "absolute"),
    iHere = (3, "here"),
    iParent = (4, "parent"),
    iHome = (5, "home"),
    iEnv = (6, "environment"),
    iMiss = (7, "missing")

  TermKind* = enum
    tApp = 0,
    tLambda = 1,
    tPi = 2,
    tOp = 3,
    tList = 4,
    tSome = 5,
    tMerge = 6,
    tRecordType = 7,
    tRecordLiteral = 8,
    tField = 9,
    tProject = 10,
    tUnionType = 11,
    tIf = 14,
    tNaturalLiteral = 15,
    tIntegerLiteral = 16,
    tTextLiteral = 18,
    tAssert = 19,
    tImport = 24,
    tLet = 25,
    tAnnotation = 26,
    tToMap = 27,
    tEmptyList = 28,
    tWith = 29,
    tVar, tFreeVar, tLocalVar, tQuoteVar,
    tBuiltin,
    tProjectType,
    tBoolLiteral,
    tDoubleLiteral,

    tTextChunk,
      ## Chunk of a text literal
    tRecordBinding,
      ## Used by the parser
    tLetBinding,
      ## A let binding in a let statement
    tFuture,
      ## A pending import
    tLambdaCallback, tPiCallback

  NodeObj[Term] = object of RootObj
    case kind*: TermKind
    of tApp:
      appFun*, appArg*: Term
    of tLambda, tPi:
      funcLabel*: string
      funcType*, funcBody*: Term
    of tOp:
      op*: OpKind
      opL*, opR*: Term
    of tList:
      listType*: Option[Term]
      list*: seq[Term]
    of tSome:
      someVal*: Term
      someType*: Option[Term]
    of tMerge:
      mergeHandler*, mergeUnion*: Term
      mergeAnn*: Option[Term]
    of tRecordType, tRecordLiteral, tUnionType:
      table*: Table[string, Term]
    of tField:
      fieldRecord*: Term
      fieldName*: string
    of tProject:
      projectRecord*: Term
      projectNames*: seq[string]
    of tProjectType:
      projectTypeRecord*: Term
      projectTypeSelector*: Term
    of tBoolLiteral:
      bool*: bool
    of tIf:
      ifCond*, ifTrue*, ifFalse*: Term
    of tNaturalLiteral:
      natural*: BigInt
    of tIntegerLiteral:
      integer*: BigInt
    of tDoubleLiteral:
      double*: BiggestFloat
    of tTextLiteral:
      textChunks*: seq[Term]
      textSuffix*: string
    of tAssert:
      assertAnn*: Term
    of tImport:
      importCheck*: seq[byte]
      importKind*: ImportKind
      importScheme*: ImportScheme
      importHeaders*: Option[Term]
      importElements*: seq[string]
      importQuery*: Option[string]
    of tLet:
      letBinds*: seq[Term] # binding terms
      letBody*: Term
    of tAnnotation:
      annExpr*, annAnn*: Term
    of tToMap:
      toMapBody*: Term
      toMapAnn*: Option[Term]
    of tEmptyList:
      emptyListType*: Term
    of tWith:
      withExpr*, withUpdate*: Term
      withFields*: seq[string]
    of tVar, tFreeVar, tLocalVar, tQuoteVar:
      varName*: string
      varIndex*: int
      # TODO varType*: Option[Term]
    of tBuiltin:
      builtinArgs*: seq[Term]
      builtin*: BuiltinKind

    of tTextChunk:
      textPrefix*: string
      textExpr*: Term
    of tRecordBinding:
      recKey*: string
      recVal*: Term
    of tLetBinding:
      letKey*: string
      letVal*: Term
      letAnn*: Option[Term]
    of tFuture:
      source*: Term
      future*: Future[Term]
    of tLambdaCallback, tPiCallback:
      callbackLabel*: string
      domain*: Term
      callback*: proc (e: Term): Term {.gcsafe,noSideEffect.}

  Term* = ref object of NodeObj[Term]
    ## Raw expression type.

  Value* = ref object of NodeObj[Value]
    ## Normalized expression type.

  Node* = Term | Value

func parseBuiltin*(s: string): BuiltinKind =
  case s
  of "Natural/build": bNaturalBuild
  of "Natural/fold": bNaturalFold
  of "Natural/isZero": bNaturalIsZero
  of "Natural/even": bNaturalEven
  of "Natural/odd": bNaturalOdd
  of "Natural/toInteger": bNaturalToInteger
  of "Natural/show": bNaturalShow
  of "Natural/subtract": bNaturalSubtract
  of "Integer/toDouble": bIntegerToDouble
  of "Integer/show": bIntegerShow
  of "Integer/negate": bIntegerNegate
  of "Integer/clamp": bIntegerClamp
  of "Double/show": bDoubleShow
  of "List/build": bListBuild
  of "List/fold": bListFold
  of "List/length": bListLength
  of "List/head": bListHead
  of "List/last": bListLast
  of "List/indexed": bListIndexed
  of "List/reverse": bListReverse
  of "Text/show": bTextShow
  of "Text/replace": bTextReplace
  of "Bool": bBool
  of "Optional": bOptional
  of "Natural": bNatural
  of "Integer": bInteger
  of "Double": bDouble
  of "Text": bText
  of "List": bList
  of "True": bTrue
  of "False": bFalse
  of "None": bNone
  of "Type": bType
  of "Kind": bKind
  of "Sort": bSort
  else:
    raise newException(ValueError, "invalid builtin " & s)

func callQuoted(v: Value, index: Natural): Value =
  let qv = Value(kind: tQuoteVar, varName: "_", varIndex: index)
  v.callback(qv)

func alphaEquivalent*(x, y: Value; level: Natural): bool

func alphaEquivalent*(x, y: Option[Value]; level: Natural): bool =
  if x.isSome and y.isSome:
    result = alphaEquivalent(x.get, y.get, level)

func alphaEquivalent(x, y: seq[Value]; level: Natural): bool =
  if x.len == y.len:
    for i in x.low..x.high:
      if not alphaEquivalent(x[i], y[i], level): return
    result = true

func alphaEquivalent(x, y: Table[string, Value]; level: Natural): bool =
  if x.len == y.len:
    for key, val in x:
      if not alphaEquivalent(val, y[key], level): return
    result = true

type FlatField = int | string | Natural | BuiltinKind | OpKind | seq[string] | bool | BigInt | BiggestFloat | seq[byte] | ImportKind | ImportScheme | Option[string]

func alphaEquivalent(x, y: FlatField; level: Natural): bool =
  x == y

func alphaEquivalent*(x, y: Value; level: Natural): bool =
  if x.isNil and y.isNil: return true
  if x.isNil or y.isNil: return false
  if x.kind != y.kind: return false
  template eq(field: untyped): bool =
    alphaEquivalent(x.field, y.field, level)
  result = case x.kind
    of tVar, tFreeVar, tLocalVar, tQuoteVar:
      eq(varName) and eq(varIndex)
    of tBuiltin:
      eq(builtin) and eq(builtinArgs)
    of tApp:
      eq(appFun) and eq(appArg)
    of tLambda:
      eq(funcLabel) and eq(funcType) and eq(funcBody)
    of tPi:
      eq(funcLabel) and eq(funcType) and eq(funcBody)
    of tOp:
      eq(op) and eq(opL) and eq(opR)
    of tList:
      eq(list)
      # do not compare listType
    of tSome:
      eq(someType) and eq(someVal)
    of tMerge:
      eq(mergeHandler) and eq(mergeUnion) and eq(mergeAnn)
    of tRecordType, tRecordLiteral, tUnionType:
      eq(table)
    of tField:
      eq(fieldRecord) and eq(fieldName)
    of tProject:
      eq(projectRecord) and eq(projectNames)
    of tProjectType:
      eq(projectTypeRecord) and eq(projectTypeSelector)
    of tBoolLiteral:
      eq(bool)
    of tIf:
      eq(ifCond) and eq(ifTrue) and eq(ifFalse)
    of tNaturalLiteral:
      eq(natural)
    of tIntegerLiteral:
      eq(integer)
    of tDoubleLiteral:
      eq(double)
    of tTextLiteral:
      eq(textChunks) and eq(textSuffix)
    of tAssert:
      eq(assertAnn)
    of tImport:
      eq(importCheck) and eq(importKind) and eq(importScheme) and eq(
          importHeaders) and eq(importElements) and eq(importQuery)
    of tLet:
      eq(letBinds) and eq(letBody)
    of tAnnotation:
      eq(annExpr) and eq(annAnn)
    of tToMap:
      eq(toMapBody) and eq(toMapAnn)
    of tEmptyList:
      eq(emptyListType)
    of tWith:
      eq(withExpr) and eq(withFields) and eq(withUpdate)
    of tTextChunk:
      eq(textPrefix) and eq(textExpr)
    of tRecordBinding:
      eq(recKey) and eq(recVal)
    of tLetBinding:
      eq(letKey) and eq(letVal) and eq(letAnn)
    of tFuture:
      false
    of tLambdaCallback, tPiCallback:
      alphaEquivalent(x.domain, x.domain, level) and
          alphaEquivalent(callQuoted(x, level), callQuoted(y, level), level+1)

func `==`*(a, b: Value): bool = alphaEquivalent(a, b, 0)

func walk*[A, B](expr: A; f: proc (n: A): B {.gcsafe.}): B

func walk*[A, B](expr: Option[A]; f: proc (n: A): B {.gcsafe.}): Option[B] =
  if expr.isSome:
    result = some walk[A,B](expr.get, f)

func walk*[A, B](s: seq[A]; f: proc (n: A): B {.gcsafe.}): seq[B] =
  result = newSeq[B](s.len)
  for i in s.low..s.high:
    result[i] = walk(s[i], f)

func walk*[A, B](table: Table[string, A]; f: proc (n: A): B {.gcsafe.}): Table[string, B] =
  result = initTable[string, B](table.len.nextPowerOfTwo)
  for key, val in table.pairs:
    if val.isNil: # unions
      result[key] = nil
    else:
      result[key] = walk(val, f)

func walk*[A, B](expr: A; f: proc (n: A): B {.gcsafe.}): B =
  ## Map ``expr`` using procedure ``f``. If ``f`` produces a nil value then
  ## copy ``expr`` and apply ``f`` to each of its constituent terms.
  result = f(expr)
  if result.isNil:
    result = B(kind: expr.kind)
    case result.kind
    of tApp:
      result.appFun = walk(expr.appFun, f)
      result.appArg = walk(expr.appArg, f)
    of tLambda, tPi:
      result.funcLabel = expr.funcLabel
      result.funcType = walk(expr.funcType, f)
      result.funcBody = walk(expr.funcBody, f)
    of tOp:
      result.op = expr.op
      result.opL = walk(expr.opL, f)
      result.opR = walk(expr.opR, f)
    of tList:
      result.listType = walk(expr.listType, f)
      result.list = walk(expr.list, f)
    of tSome:
      result.someVal = walk(expr.someVal, f)
      result.someType = walk(expr.someType, f)
    of tMerge:
      result.mergeHandler = walk(expr.mergeHandler, f)
      result.mergeUnion = walk(expr.mergeUnion, f)
      result.mergeAnn = walk(expr.mergeAnn, f)
    of tRecordType, tRecordLiteral, tUnionType:
      result.table = walk(expr.table, f)
    of tField:
      result.fieldRecord = walk(expr.fieldRecord, f)
      result.fieldName = expr.fieldName
    of tProject:
      result.projectRecord = walk(expr.projectRecord, f)
      result.projectNames = expr.projectNames
    of tProjectType:
      result.projectTypeRecord = walk(expr.projectTypeRecord, f)
      result.projectTypeSelector = walk(expr.projectTypeSelector, f)
    of tIf:
      result.ifCond = walk(expr.ifCond, f)
      result.ifTrue = walk(expr.ifTrue, f)
      result.ifFalse = walk(expr.ifFalse, f)
    of tTextLiteral:
      result.textChunks = walk(expr.textChunks, f)
      result.textSuffix = expr.textSuffix
    of tAssert:
      result.assertAnn = walk(expr.assertAnn, f)
    of tImport:
      result.importCheck = expr.importCheck
      result.importKind = expr.importKind
      result.importScheme = expr.importScheme
      result.importHeaders = walk(expr.importHeaders, f)
      result.importElements = expr.importElements
      result.importQuery = expr.importQuery
    of tLet:
      result.letBinds = walk(expr.letBinds, f)
      result.letBody = walk(expr.letBody, f)
    of tAnnotation:
      result.annExpr = walk(expr.annExpr, f)
      result.annAnn = walk(expr.annAnn, f)
    of tToMap:
      result.toMapBody = walk(expr.toMapBody, f)
      result.toMapAnn = walk(expr.toMapAnn, f)
    of tEmptyList:
      result.emptyListType = walk(expr.emptyListType, f)
    of tWith:
      result.withUpdate = walk(expr.withUpdate, f)
      result.withExpr = walk(expr.withExpr, f)
      result.withFields = expr.withFields
    of tBuiltin:
      result.builtin = expr.builtin
      result.builtinArgs = walk(expr.builtinArgs, f)
    of tTextChunk:
      result.textPrefix = expr.textPrefix
      if not expr.textExpr.isNil:
        result.textExpr = walk(expr.textExpr, f)
    of tRecordBinding:
      result.recKey = expr.recKey
      result.recVal = walk(expr.recVal, f)
    of tLetBinding:
      result.letKey = expr.letKey
      result.letVal = walk(expr.letVal, f)
      result.letAnn = walk(expr.letAnn, f)
    of tFuture:
      let e = expr.future.read
      result = walk(e, f)
    else:
      result = cast[B](expr)
    assert(not result.isNil)

func isBoolType*(t: Node): bool = t.kind == tBuiltin and t.builtin == bBool
func isList*(t: Node): bool = t.kind in {tList, tEmptyList}
func isNaturalType*(t: Node): bool = t.kind == tBuiltin and t.builtin == bNatural
func isNatural*(t: Node): bool = t.kind == tNaturalLiteral
func isRecordLiteral*(t: Node): bool = t.kind == tRecordLiteral
func isRecordType*(t: Node): bool = t.kind == tRecordType
func isTextType*(t: Node): bool = t.kind == tBuiltin and t.builtin == bText
func isTextLiteral*(t: Node): bool = t.kind == tTextLiteral
func isSimpleText*(t: Node): bool =
  if t.kind == tTextLiteral:
    result = true
    for c in t.textChunks:
      if not c.textExpr.isNil:
        return false
func isType*(t: Node): bool = t.kind == tBuiltin and t.builtin == bType
func isKind*(t: Node): bool = t.kind == tBuiltin and t.builtin == bKind
func isSort*(t: Node): bool = t.kind == tBuiltin and t.builtin == bSort
func isImport*(t: Node): bool = t.kind == tImport
func isUnion*(t: Node): bool = t.kind == tUnionType
func isBool*(t: Node): bool = t.kind == tBoolLiteral
func isLambda*(t: Node): bool = t.kind == tLambda
func isVar*(t: Node): bool =
  t.kind in {tVar,tFreeVar,tLocalVar,tQuoteVar}
func isApp*(t: Node): bool = t.kind == tApp
func isPi*(t: Term): bool = t.kind == tPi
func isFunction*(t: Term): bool = t.kind in {tLambda, tPi}
func isPi*(t: Value): bool = t.kind == tPiCallback
func isFunction*(t: Value): bool = t.kind in {tLambdaCallback, tPiCallback}
func isBuiltin*(t: Node): bool = t.kind == tBuiltin
func isBuiltin*(t: Node; b: BuiltinKind): bool =
  t.kind == tBuiltin and t.builtin == b
func isOp*(t: Node; op: OpKind): bool =
  t.kind == tOp and t.op == op
func isFuture*(t: Node): bool = t.kind == tFuture
func isInteger*(t: Node): bool = t.kind == tIntegerLiteral

func isUniversal*(t: Node): bool =
  t.kind == tBuiltin and t.builtin in {bType, bKind, bSort}

func toTerm*(k: BuiltinKind): Term = Term(kind: tBuiltin, builtin: k)

func newTerm*(k: BuiltinKind): Term = Term(kind: tBuiltin, builtin: k)
func newValue*(k: BuiltinKind): Value = Value(kind: tBuiltin, builtin: k)

func newTerm*(op: OpKind; opL, opR: Term): Term =
  Term(kind: tOp, op: op, opL: opL, opR: opR)

func newValue*(op: OpKind; opL, opR: Value): Value =
  Value(kind: tOp, op: op, opL: opL, opR: opR)

func newTerm*(s: string): Term =
  Term(kind: tTextLiteral, textSuffix: s)

func newValue*(s: string): Value =
  Value(kind: tTextLiteral, textSuffix: s)

func newTerm*(i: Natural): Term =
  Term(kind: tNaturalLiteral, natural: initBigInt i)

func newTerm*(l: seq[Term]): Term =
  Term(kind: tList, list: l)

func newValue*(b: bool): Value =
  Value(kind: tBoolLiteral, bool: b)

func newInteger*(i: BigInt): Value =
  Value(kind: tIntegerLiteral, integer: i)

func newNatural*(i: Natural): Value =
  Value(kind: tNaturalLiteral, natural: initBigInt(i))

func newNatural*(i: BigInt): Value =
  Value(kind: tNaturalLiteral, natural: i)

func newValue*(f: float): Value =
  Value(kind: tDoubleLiteral, double: f)

func newValue*(vs: seq[Value]): Value =
  assert(vs.len > 0)
  Value(kind: tList, list: vs)

func newTerm*(uri: Uri): Term =
  let pathElems = uri.path.split('/')
  result = Term(kind: tImport, importKind: iCode)
  case uri.scheme
  of "http", "https":
    case uri.scheme
    of "http": result.importScheme = iHttp
    of "https": result.importScheme = iHttps
    else: discard
    result.importElements = @[uri.hostName] & pathElems
    if uri.query != "":
      result.importQuery = some uri.query
  else:
    result.importScheme = iAbs
    result.importElements = pathElems

func newVar*(name: string; index = 0): Term =
  Term(kind: tVar, varName: name, varIndex: index)

func newFreeVar*(name: string; index = 0): Value =
  Value(kind: tFreeVar, varName: name, varIndex: index)

func newQuoteVar*(name: string; index = 0): Value =
  Value(kind: tQuoteVar, varName: name, varIndex: index)

func newApp*(b: BuiltinKind; arg: Term): Term =
  Term(kind: tApp, appFun: newTerm(b), appArg: arg)

func newApp*(b: BuiltinKind; arg: Value): Value =
  Value(kind: tApp, appFun: newValue(b), appArg: arg)

func newApp*(fun: Value; args: varargs[Value]): Value =
  result = fun
  for arg in args:
    result = Value(kind: tApp, appFun: result, appArg: arg)

func newApp*[Node: Term|Value](fun, arg: Node): Node =
  result = Node(kind: tApp, appFun: fun, appArg: arg)

func newListType*(n: Term): Term = newApp(bList, n)
func newListType*(n: Value): Value = newApp(bList, n)

func newOptionalType*(T: Value): Value = newApp(bOptional, T)

func newLambda*(
    label: string; argType: Value; callback: proc (v: Value): Value {.gcsafe,noSideEffect.}): Value =
  Value(kind: tLambdaCallback,
      callbackLabel: label, domain: argType, callback: callback)

func newLambda*(
    argType: Value; callback: proc (v: Value): Value {.gcsafe,noSideEffect.}): Value =
  newLambda("_", argType, callback)

func newPi*(label: string; domain, codomain: Term): Term =
  Term(kind: tPi, funcLabel: label, funcType: domain, funcBody: codomain)

func newPi*(domain, codomain: Term): Term =
  newPi("_", domain, codomain)

func newPi*(label: string; domain: Value; callback: proc (v: Value): Value {.gcsafe,noSideEffect.}): Value =
  Value(kind: tPiCallback, callbackLabel: label, domain: domain, callback: callback)

func newPi*(label: string; domain, codomain: Value): Value =
  newPi(label, domain) do (_: Value) -> Value:
    codomain

func newPi*(domain, codomain: Value): Value =
  newPi("_", domain, codomain)

func newRecordType*(pairs: openArray[(string, Term)]): Term =
  Term(kind: tRecordType, table: pairs.toTable)

func newRecordType*(pairs: openArray[(string, Value)]): Value =
  Value(kind: tRecordType, table: pairs.toTable)

func newRecordLiteral*(pairs: openArray[(string, Term)]): Term =
  Term(kind: tRecordLiteral, table: pairs.toTable)

func newRecordLiteral*(pairs: openArray[(string, Value)]): Value =
  Value(kind: tRecordLiteral, table: pairs.toTable)

func newUnion*(pairs: openArray[(string, Term)]): Term =
  Term(kind: tUnionType, table: pairs.toTable)

func newUnion*(pairs: openArray[(string, Value)]): Value =
  Value(kind: tUnionType, table: pairs.toTable)

func newRecordType*(len: Natural): Value =
  Value(kind: tRecordType,
      table: initTable[string, Value](nextPowerOfTwo len))

func newRecordLiteral*(len: Natural): Value =
  Value(kind: tRecordLiteral,
      table: initTable[string, Value](nextPowerOfTwo len))

func newUnion*(len: Natural): Value =
  Value(kind: tUnionType, table: initTable[string, Value](nextPowerOfTwo len))

func newField*(t: Term; s: string): Term =
  Term(kind: tField, fieldRecord: t, fieldName: s)

func newField*(t: Value; s: string): Value =
  Value(kind: tField, fieldRecord: t, fieldName: s)

func newMissing*(): Term = Term(kind: tImport, importScheme: iMiss)

func text*(t: Term): string =
  assert(t.kind == tTextLiteral)
  if t.textChunks == @[]:
    result = t.textSuffix
  else:
    for c in t.textChunks:
      assert(c.textExpr.isNil)
      result.add c.textPrefix
    result.add t.textSuffix

func field*(t: Term; key: string): Term =
  case t.kind
  of tRecordType, tRecordLiteral, tUnionType:
    result = t.table[key]
  else: raiseAssert "field access of a non-record type"

template withField*(t: Term; key: string; value, body: untyped) =
  case t.kind
  of tRecordType, tRecordLiteral, tUnionType:
    t.table.withValue(key, value, body)
  else: discard

func isMissing*(t: Term): bool =
  t.kind == tImport and
      t.importScheme == iMiss and
          t.importCheck == @[] and
            t.importKind != iLocation

type Form* = enum
  beta, alpha


A src/dhall/type_inference.nim => src/dhall/type_inference.nim +547 -0
@@ 0,0 1,547 @@
import ./binary, ./terms, ./normalization, ./quotation, ./render, ./substitutions

import std/math, std/options, std/tables

type Context* = Table[string, seq[Value]]

func extend(ctx: Context; label: string; v: Value): Context =
  # TODO: probably a shallow copy?
  result = ctx
  result.mgetOrPut(label, newSeqOfCap[Value](2)).add(v)

func freshLocal(ctx: Context; label: string): Term =
  Term(kind: tLocalVar,
      varName: label,
      varIndex: ctx.getOrDefault(label).len)

func rebindLocal(t, local: Term; level: Natural = 0): Term =
  assert(local.kind == tLocalVar, $local)
  result = walk(t) do (t: Term) -> Term:
    case t.kind
    of tLambda, tPi:
      let next =
        if t.funcLabel == local.varName: level + 1
        else: level
      result = Term(kind: t.kind)
      result.funcLabel = t.funcLabel
      result.funcType = t.funcType.rebindLocal(local, level)
      result.funcBody = t.funcBody.rebindLocal(local, next)
    of tLet:
      var level = level
      result = Term(kind: tLet,
          letBinds: newSeq[Term](t.letBinds.len))
      for i, b in t.letBinds:
        result.letBinds[i] = b.rebindLocal(local, level)
        if b.letKey == local.varName: inc(level)
      result.letBody = t.letBody.rebindLocal(local, level)
    of tLocalVar:
      if t.varName == local.varName and
          t.varIndex == local.varIndex:
        result = Term(kind: tVar,
          varName: t.varName, varIndex: level)
    else: discard

func mergeRecordType(result: Value; other: Value) =
  assert(result.isRecordType)
  assert(other.isRecordType)
  for key, val in other.table.pairs:
    if result.table.hasKey(key):
      result.table[key].mergeRecordType(val)
    else:
      result.table[key] = val

template raiseTypeError(msg: string) =
  raise newException(TypeError, msg)

func infer(ctx: Context; expr: Term): Value =
  {.noSideEffect.}:
    func typeCheck(cond: bool; msg: string) =
      if not cond: raise newException(TypeError, msg & ": " & $expr)
    func typeMatch(a, b: Value; msg = "") =
      if not alphaEquivalent(a, b, 0):
        raise newException(TypeError,
            if msg == "":
              "mismatch of " & $quote(a) & " and " & $quote(b) & " at " & $expr
            else: msg)
    func checkMerge(l, r: Value) =
      typeCheck(l.kind == r.kind, "invalid terms for merge")
      for key, val in l.table.pairs:
        if r.table.contains(key):
          typeCheck(val.kind == l.kind, "invalid terms for merge")
          checkMerge(val, r.table[key])
    result = walk(expr) do (t: Term) -> Value:
      case t.kind
      of tApp:
        let funType = ctx.infer(t.appFun)
        typeCheck(funType.isPi, "not a function for application - " & $funType.kind)
        let argType = ctx.infer(t.appArg)
        # TODO:
        # typeMatch(argType, funType.domain)
        result = funType.callback(eval(t.appArg))

      of tLambda:
        assert(t.funcLabel != "")
        let argUniverse = ctx.infer(t.funcType)
        #typeCheck(argUniverse.isUniversal,
        #    "function argument must be a type")
        let
          argType = eval(t.funcType)
          freshLocal = ctx.freshLocal(t.funcLabel)
          bodyType = infer(
              ctx.extend(t.funcLabel, argType),
              t.funcBody.substitute(t.funcLabel, freshLocal))
        result = newPi(t.funcLabel, argType) do (v: Value) -> Value:
          let
            rebound = bodyType.quote.rebindLocal(freshLocal)
            localEnv = [(t.funcLabel, @[v])].toTable
          eval(localEnv, rebound)
        discard ctx.infer(quote(result))

      of tPi:
        let argUniverse = ctx.infer(t.funcType)
        typeCheck(argUniverse.isUniversal, "pi input must be universal")
        let freshLocal = ctx.freshLocal(t.funcLabel)
        let outUniverse = infer(
            ctx.extend(t.funcLabel, eval(t.funcType)),
            substitute(t.funcBody, t.funcLabel, freshLocal))
        typeCheck(outUniverse.isUniversal, "pi output must be universal")
        if outUniverse.isType:
          result = outUniverse
        elif argUniverse.builtin < outUniverse.builtin:
          result = outUniverse
        else:
          result = argUniverse

      of tOp:
        case t.op
        of opComplete:
          let
            op = newTerm(opRecordBiasedMerge,
                newField(t.opL, "default"), t.opR)
            ann = Term(kind: tAnnotation,
                annExpr: op, annAnn: newField(t.opL, "Type"))
          result = infer(ctx, ann)
        else: # infer the operands before continuing
          let
            opL = ctx.infer t.opL
            opR = ctx.infer t.opR
          case t.op
          of opBoolOr, opBoolAnd, opBoolEquality, opBoolInequality:
            typeCheck(opL.isBoolType and opR.isBoolType,
                "boolean operator on non-boolean value")
            result = newValue(bBool)
          of opNaturalAdd, opNaturalMultiplication:
            typeCheck(opL.isNaturalType and opR.isNaturalType,
                "natural number operator on non-natural number")
            result = newValue(bNatural)
          of opTextAppend:
            typeCheck(opL.isTextType and opR.isTextType,
                "text concatentation on non-text value")
            result = newValue(bText)
          of opListAppend:
            typeCheck(
                opL.isApp and opL.appFun.isBuiltin(bList) and opL == opR,
                "invalid list concatentation")
            result = opL
          of opRecordRecursiveMerge:
            typeCheck(opL.isRecordType, "invalid terms for merge")
            checkMerge(opL, opR)
            result = opL
            result.mergeRecordType(opR)
          of opRecordBiasedMerge:
            typeCheck(opL.isRecordType and opR.isRecordType,
              "invalid merge")
            let len = opL.table.len + opR.table.len
            result = Value(kind: tRecordType,
                table: initTable[string, Value](nextPowerOfTwo len))
            for t in [opL, opR]:
              for key, val in t.table.pairs:
                result.table[key] = val
          of opRecordTypeMerge:
            let
              l = eval(t.opL)
              r = eval(t.opR)
            typeCheck(l.isRecordType and r.isRecordType,
                "invalid record type merge")
            checkMerge(l, r)
            if opL.isUniversal and opR.isUniversal:
              if opL.isSort or opR.isSort:
                result = newValue bSort
              elif opL.isKind or opR.isKind:
                result = newValue bKind
              else:
                result = newValue bType
          of opEquivalience:
            typeCheck(not opL.isUniversal and not opR.isUniversal,
                "invalid type for equivalence")
            typeMatch(opL, opR)
            result = newValue bType
          else: discard

      of tList:
        var listType: Value
        if t.listType.isSome:
          listType = eval(t.listType.get)
        for val in t.list:
          let T = ctx.infer val
          if listType.isNil:
            listType = T
          else:
            typeMatch(T, listType, "list type is not heterogeneous")
        typeCheck(not listType.isUniversal, "invalid list type")
        result = newApp(bList, listType)

      of tSome:
        let T = ctx.infer t.someVal
        t.someType.map do (someType: Term):
          typeMatch(T, eval(someType),
              "type of Some value does not match annotation")