{-# LANGUAGE OverloadedStrings #-}

module Hydra.Impl.Haskell.Sources.Core where

import Hydra.Kernel
import Hydra.Meta
import Hydra.Impl.Haskell.Dsl.Types as Types
import Hydra.Impl.Haskell.Dsl.Bootstrap


hydraCore :: Graph Meta
hydraCore :: Graph Meta
hydraCore = forall m. Maybe (Graph m) -> [Element m] -> Graph m
elementsToGraph forall a. Maybe a
Nothing (forall m. Module m -> [Element m]
moduleElements Module Meta
hydraCoreModule)

hydraCoreModule :: Module Meta
hydraCoreModule :: Module Meta
hydraCoreModule = forall m.
Namespace -> [Element m] -> [Module m] -> Maybe String -> Module m
Module Namespace
ns [Element Meta]
elements [] forall a b. (a -> b) -> a -> b
$
    forall a. a -> Maybe a
Just String
"Hydra's core data model, defining types, terms, and their dependencies"
  where
    ns :: Namespace
ns = String -> Namespace
Namespace String
"hydra/core"
    core :: String -> Type m
core = forall m. Namespace -> String -> Type m
nsref Namespace
ns
    def :: String -> Type m -> Element m
def = forall m. Namespace -> String -> Type m -> Element m
datatype Namespace
ns
    doc :: String -> Type Meta -> Type Meta
doc String
s = Context Meta -> Maybe String -> Type Meta -> Type Meta
setTypeDescription Context Meta
bootstrapContext (forall a. a -> Maybe a
Just String
s)

    elements :: [Element Meta]
elements = [

      forall {m}. String -> Type m -> Element m
def String
"Annotated" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"An object, such as a type or term, together with an annotation" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"a" forall a b. (a -> b) -> a -> b
$ forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"subject"forall m. String -> Type m -> FieldType m
>: Type Meta
"a",
          String
"annotation"forall m. String -> Type m -> FieldType m
>: Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Application" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A term which applies a function to an argument" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"function"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The left-hand side of the application" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"argument"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The right-hand side of the application" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"ApplicationType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"The type-level analog of an application term" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"function"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The left-hand side of the application" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"argument"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The right-hand side of the application" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"CaseStatement" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A union elimination; a case statement" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"typeName"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Name",
          String
"cases"forall m. String -> Type m -> FieldType m
>: forall m. Type m -> Type m
list forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"Field" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Elimination" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A corresponding elimination for an introduction term" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
union [
          String
"element"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Eliminates an element by mapping it to its data term. This is Hydra's delta function."
            forall m. Type m
unit,
          String
"list"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Eliminates a list using a fold function; this function has the signature b -> [a] -> b" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"nominal"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Eliminates a nominal term by extracting the wrapped term" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Name",
          String
"optional"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Eliminates an optional term by matching over the two possible cases" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"OptionalCases" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"record"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Eliminates a record by projecting a given field" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Projection",
          String
"union"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Eliminates a union term by matching over the fields of the union. This is a case statement." forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"CaseStatement" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Field" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A labeled term" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"name"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"FieldName",
          String
"term"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"FieldName" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"The name of a field, unique within a record or union type"
        forall m. Type m
string,

      forall {m}. String -> Type m -> Element m
def String
"FieldType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"The name and type of a field" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"name"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"FieldName",
          String
"type"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"FloatType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A floating-point type" forall a b. (a -> b) -> a -> b
$
        forall m. [String] -> Type m
enum [
          String
"bigfloat",
          String
"float32",
          String
"float64"],

      forall {m}. String -> Type m -> Element m
def String
"FloatValue" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A floating-point literal value" forall a b. (a -> b) -> a -> b
$
        forall m. [FieldType m] -> Type m
union [
          String
"bigfloat"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An arbitrary-precision floating-point value" forall m. Type m
bigfloat,
          String
"float32"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 32-bit floating-point value" forall m. Type m
float32,
          String
"float64"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 64-bit floating-point value" forall m. Type m
float64],

      forall {m}. String -> Type m -> Element m
def String
"Function" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A function" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
union [
          String
"compareTo"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"Compares a term with a given term of the same type, producing a Comparison" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"elimination"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An elimination for any of a few term variants" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Elimination" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"lambda"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A function abstraction (lambda)" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Lambda" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"primitive"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A reference to a built-in (primitive) function" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Name"],

      forall {m}. String -> Type m -> Element m
def String
"FunctionType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A function type, also known as an arrow type" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"domain"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"codomain"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"IntegerType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"An integer type" forall a b. (a -> b) -> a -> b
$
        forall m. [String] -> Type m
enum [
          String
"bigint",
          String
"int8",
          String
"int16",
          String
"int32",
          String
"int64",
          String
"uint8",
          String
"uint16",
          String
"uint32",
          String
"uint64"],

      forall {m}. String -> Type m -> Element m
def String
"IntegerValue" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"An integer literal value" forall a b. (a -> b) -> a -> b
$
        forall m. [FieldType m] -> Type m
union [
          String
"bigint"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An arbitrary-precision integer value" forall m. Type m
bigint,
          String
"int8"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An 8-bit signed integer value" forall m. Type m
int8,
          String
"int16"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 16-bit signed integer value (short value)" forall m. Type m
int16,
          String
"int32"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 32-bit signed integer value (int value)" forall m. Type m
int32,
          String
"int64"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 64-bit signed integer value (long value)" forall m. Type m
int64,
          String
"uint8"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An 8-bit unsigned integer value (byte)" forall m. Type m
uint8,
          String
"uint16"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 16-bit unsigned integer value" forall m. Type m
uint16,
          String
"uint32"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 32-bit unsigned integer value (unsigned int)" forall m. Type m
uint32,
          String
"uint64"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A 64-bit unsigned integer value (unsigned long)" forall m. Type m
uint64],

      forall {m}. String -> Type m -> Element m
def String
"Lambda" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A function abstraction (lambda)" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"parameter"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The parameter of the lambda" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Variable",
          String
"body"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The body of the lambda" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"LambdaType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A type abstraction; the type-level analog of a lambda term" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"parameter"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The parameter of the lambda" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"VariableType",
          String
"body"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The body of the lambda" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Let" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A 'let' binding" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"key"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Variable",
          String
"value"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"environment"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Literal" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A term constant; an instance of a literal type" forall a b. (a -> b) -> a -> b
$
        forall m. [FieldType m] -> Type m
union [
          String
"binary"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A binary literal" forall m. Type m
binary,
          String
"boolean"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A boolean literal" forall m. Type m
boolean,
          String
"float"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A floating-point literal" forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"FloatValue",
          String
"integer"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An integer literal" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"IntegerValue",
          String
"string"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A string literal" forall m. Type m
string],

      forall {m}. String -> Type m -> Element m
def String
"LiteralType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"Any of a fixed set of literal types, also called atomic types, base types, primitive types, or type constants" forall a b. (a -> b) -> a -> b
$
        forall m. [FieldType m] -> Type m
union [
          String
"binary"forall m. String -> Type m -> FieldType m
>: forall m. Type m
unit,
          String
"boolean"forall m. String -> Type m -> FieldType m
>: forall m. Type m
unit,
          String
"float"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"FloatType",
          String
"integer"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"IntegerType",
          String
"string"forall m. String -> Type m -> FieldType m
>: forall m. Type m
unit],

      forall {m}. String -> Type m -> Element m
def String
"MapType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A map type" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"keys"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"values"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Name" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A unique element name"
        forall m. Type m
string,

      forall {m}. String -> Type m -> Element m
def String
"Named" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A term annotated with a fixed, named type; an instance of a newtype" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"typeName"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Name",
          String
"term"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"OptionalCases" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A case statement for matching optional terms" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"nothing"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A term provided if the optional value is nothing" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"just"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A function which is applied of the optional value is non-nothing" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Projection" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A record elimination; a projection" forall a b. (a -> b) -> a -> b
$
        forall m. [FieldType m] -> Type m
record [
          String
"typeName"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Name",
          String
"field"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"FieldName"],

      forall {m}. String -> Type m -> Element m
def String
"Record" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A record, or labeled tuple; a map of field names to terms" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"typeName"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Name",
          String
"fields"forall m. String -> Type m -> FieldType m
>: forall m. Type m -> Type m
list forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"Field" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"RowType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A labeled record or union type" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"typeName"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The name of the row type, which must correspond to the name of a Type element" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Name",
          String
"extends"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc (String
"Optionally, the name of another row type which this one extends. To the extent that field order " forall a. [a] -> [a] -> [a]
++
                 String
"is preserved, the inherited fields of the extended type precede those of the extension.") forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m
optional forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"Name",
          String
"fields"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"The fields of this row type, excluding any inherited fields" forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m
list forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"FieldType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Stream" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"An infinite stream of terms" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"first"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"rest"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Stream" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],
      
      forall {m}. String -> Type m -> Element m
def String
"Sum" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"The unlabeled equivalent of a Union term" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"index"forall m. String -> Type m -> FieldType m
>: forall m. Type m
int32,
          String
"size"forall m. String -> Type m -> FieldType m
>: forall m. Type m
int32,
          String
"term"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"Term" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A data term" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
union [
          String
"annotated"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A term annotated with metadata" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Annotated" forall m. Type m -> Type m -> Type m
@@ (forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m") forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"application"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A function application" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Application" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"element"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An element reference" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Name",
          String
"function"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A function term" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Function" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"let"forall m. String -> Type m -> FieldType m
>:
            forall {m}. String -> Type m
core String
"Let" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"list"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A list" forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m
list forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          -- TODO: list elimination
          String
"literal"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A literal value" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Literal",
          String
"map"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A map of keys to values" forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m -> Type m
Types.map (forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m") (forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"),
          String
"nominal"forall m. String -> Type m -> FieldType m
>:
            forall {m}. String -> Type m
core String
"Named" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"optional"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An optional value" forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m
optional forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"product"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A tuple" forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m
list (forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"),
          String
"record"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A record term" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Record" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"set"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A set of values" forall a b. (a -> b) -> a -> b
$
            forall m. Type m -> Type m
set forall a b. (a -> b) -> a -> b
$ forall {m}. String -> Type m
core String
"Term" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"stream"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"An infinite stream of terms" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Stream" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"sum"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A variant tuple" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Sum" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"union"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A union term" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Union" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"variable"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A variable reference" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Variable"],

      forall {m}. String -> Type m -> Element m
def String
"Type" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A data type" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
union [
          String
"annotated"forall m. String -> Type m -> FieldType m
>:
            String -> Type Meta -> Type Meta
doc String
"A type annotated with metadata" forall a b. (a -> b) -> a -> b
$
            forall {m}. String -> Type m
core String
"Annotated" forall m. Type m -> Type m -> Type m
@@ (forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m") forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"application"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"ApplicationType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"element"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"function"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"FunctionType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"lambda"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"LambdaType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"list"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"literal"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"LiteralType",
          String
"map"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"MapType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"nominal"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Name",
          String
"optional"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"product"forall m. String -> Type m -> FieldType m
>: forall m. Type m -> Type m
list (forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"),
          String
"record"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"RowType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"set"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"stream"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"sum"forall m. String -> Type m -> FieldType m
>: forall m. Type m -> Type m
list (forall {m}. String -> Type m
core String
"Type" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"),
          String
"union"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"RowType" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m",
          String
"variable"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"VariableType"],

      forall {m}. String -> Type m -> Element m
def String
"Variable" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A symbol which stands in for a term"
        forall m. Type m
string,

      forall {m}. String -> Type m -> Element m
def String
"VariableType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"A symbol which stands in for a type"
        forall m. Type m
string,

      forall {m}. String -> Type m -> Element m
def String
"Union" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"An instance of a union type; i.e. a string-indexed generalization of inl() or inr()" forall a b. (a -> b) -> a -> b
$
        forall m. String -> Type m -> Type m
lambda String
"m" forall a b. (a -> b) -> a -> b
$ forall m. [FieldType m] -> Type m
record [
          String
"typeName"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Name",
          String
"field"forall m. String -> Type m -> FieldType m
>: forall {m}. String -> Type m
core String
"Field" forall m. Type m -> Type m -> Type m
@@ Type Meta
"m"],

      forall {m}. String -> Type m -> Element m
def String
"UnitType" forall a b. (a -> b) -> a -> b
$
        String -> Type Meta -> Type Meta
doc String
"An empty record type as a canonical unit type" forall a b. (a -> b) -> a -> b
$
        forall m. [FieldType m] -> Type m
record []]