Extensible

Like Trees that Grow. When you give an extensible declaration. What it does is add extra field to every constructor. It does this via type fields for each constructor. For example on Either, we'd get Left a Annotation, Right b Annotation, and an extension field. The type families for each constructor also has the extension type. If the extension is a type annotation, you can add the primty and primval to have the primitive types.

These live in the Extend modules. We also generate a constructor

  extTerm =
    \_primTy _primVal ->
      IR.defaultExtTerm
        { IR.nameLam = "Lam0",
          IR.typeLam = Just [[t|NameSymbol.T|]],
          IR.namePi = "Pi0",
          IR.typePi = Just [[t|NameSymbol.T|]],
          IR.nameSig = "Sig0",
          IR.typeSig = Just [[t|NameSymbol.T|]],
          IR.nameLet = "Let0",
          IR.typeLet = Just [[t|NameSymbol.T|]]
        }

  extElim :: p1 -> p2 -> IR.ExtElim
  extElim =
    \_primTy _primVal ->
      IR.defaultExtElim
        { IR.typeBound = Nothing,
          IR.typeFree = Nothing,
          IR.typeElimX = [("Var", [[t|NameSymbol.T|]])]
        }

  IR.extendTerm "Term" [] [t|T|] extTerm

  -- TODO allow extendTerm to reorder fields?
  pattern Lam x t = Lam0 t x

• The typeElimX can add multiple constructors.

• The name<Constructor> is the new constructor name.

• The type<Constructor> talks about an extra argument.

• The extendTerm is how we instantiate the alias and extensions system.

• The pattern are for synonyms to make the argument order better

  • This is needed for more than 1 extra constructor, as it'll generate lefts and rights.