Code

[WIP] Pairs#10

Code

Open

robrix wants to merge 78 commits intomasterantitypical/Surface:masterfrom pairsantitypical/Surface:pairsCopy head branch name to clipboard

+353-244

Commits

Commits on Jan 7, 2016

• Stub in a Surface.Language module.

  robrix

  committed
  5417077

• Add a type synonym for Term Expression.

  robrix

  committed
  b18aa6d

• Export Surface.Language.

  robrix

  committed
  d106732

• Move all of Surface to Surface.Language.

  robrix

  committed
  98b6b9f

• Stub in a Surface.Pair module.

  robrix

  committed
  79d199f

• Define a Pair type.

  robrix

  committed
  d94175e

• Export Pair.

  robrix

  committed
  a464292

• Move checkIsType up a bit.

  robrix

  committed
  ea1c0fb

• Remove a redundant import.

  robrix

  committed
  b8beb6d

• Write a few lambdas inline.

  robrix

  committed
  7f40acd

• Check function types more or less the same as pi types.

  robrix

  committed
  b6563ba

• Test for unification against the return type, not its kind.

  robrix

  committed
  80e7d35

• Check that the return type is a type.

  robrix

  committed
  9f6a92d

• Just check against type.

  robrix

  committed
  73d0bd5

• Unify the types.

  robrix

  committed
  82e1cc7

• Move _type into the Language module.

  robrix

  committed
  9261a7d

• Remove a redundant import.

  robrix

  committed
  09a144d

• Ignore the tags file.

  robrix

  committed
  f3a9a12

Commits on Jan 8, 2016

• Rename the parameters.

  robrix

  committed
  2c63002

• Test the type of _Pair.

  robrix

  committed
  4fe94bd

• Move the language tests into their own module.

  robrix

  committed
  11b820e

• Stub in a Pair module.

  robrix

  committed
  70b7600

• Don’t import Surface.Pair.

  robrix

  committed
  82b2d08

• Stub in a Definition type.

  robrix

  committed
  75fb47c

• Only represent the type of definitions for now.

  robrix

  committed
  5f74131

• Modules are lists of definitions.

  robrix

  committed
  72e7f99

• Remove a redundant import.

  robrix

  committed
  3ac0257

• Remove a bogus $.

  robrix

  committed
  e7dcfeb

• Define Definition using record syntax.

  robrix

  committed
  f2add1e

• Add a lookup operator for Module.

  robrix

  committed
  68a1a71

• Export Data.Module.

  robrix

  committed
  0fdb668

• Definitions have types and values.

  robrix

  committed
  4562713

• Correct the type of Pair.

  robrix

  committed
  c869d4d

• Add a function to typecheck a definition.

  robrix

  committed
  c4ebecc

• Add a function to typecheck modules.

  robrix

  committed
  46fe06f

• Rename the test subject.

  robrix

  committed
  c6977c8

• None of this “should” business.

  robrix

  committed
  966ed36

• Test that the module typechecks.

  robrix

  committed
  028a7fe

• Correct the inference of function types.

  robrix

  committed
  deba278

• Unification carries a typechecker.

  robrix

  committed
  25cb9ff

• Check pi types like function types.

  robrix

  committed
  0e49f82

Commits on Jan 9, 2016

• lts-4.

  robrix

  committed
  3aeaedf

• Default compiler check.

  robrix

  committed
  5bd111b

• 4.0, that is.

  robrix

  committed
  94b6b94

• Add a checkFunctionType function.

  robrix

  committed
  6541127

• Use the Checker synonym.

  robrix

  committed
  b4f4b03

• Use checkFunctionType for lambdas, pi types, and function types.

  robrix

  committed
  0b9d66a

• Recur into abstractions.

  robrix

  committed
  40ed0d2

• Add a type synonym for environments.

  robrix

  committed
  369ee1f

• Stub in the reduction of terms to weak head normal form.

  robrix

  committed
  c41e8bf

• Lookup variables for whnf.

  robrix

  committed
  12de9d8

• Substitute inside applications in whnf.

  robrix

  committed
  cda5fec

• Reduce applications to whnf correctly.

  robrix

  committed
  b793b40

• byUnifying recurs via expectUnifiable.

  robrix

  committed
  7d65f48

• Use the Term' shorthand everywhere we can.

  robrix

  committed
  05eb00b

• Module is defined in terms of Term'.

  robrix

  committed
  7a4651e

• Abstract Definition over a term type.

  robrix

  committed
  d1af2bb

• Abstract Definition over the expression type.

  robrix

  committed
  7c1a611

• Abstract Module over the expression type.

  robrix

  committed
  0b1b6fc

• Abstract Module and Definition over the term type.

  robrix

  committed
  74ac43f

• Move the Module types into Data.Term.Types.

  robrix

  committed
  4329f99

• We’re no longer dependent on StandaloneDeriving.

  robrix

  committed
  1e98610

• Equality of conflicts.

  robrix

  committed
  1a1a2d8

• Inequality of other comparisons.

  robrix

  committed
  c7aca05

• Move the Unification module under Surface.

  robrix

  committed
  bc5c75f

• Move the Unifiable instance for Expression into Surface.Unification.

  robrix

  committed
  bdd3daa

• Stub in a Surface.Renaming module.

  robrix

  committed
  444187a

• Move the Unifiable typeclass into Data.Term.Types.

  robrix

  committed
  3efe2a7

• Resort the exports.

  robrix

  committed
  a51b467

• Export Surface.Renaming.

  robrix

  committed
  c70f301

• Move renaming into Surface.Renaming.

  robrix

  committed
  91a9e19

• Move unification into Surface.Unification.

  robrix

  committed
  30af305

• annotation typechecking doesn’t use expectUnifiable.

  robrix

  committed
  17bfaf1

• Minimize the set of constraints necessary for annotation.

  robrix

  committed
  0d97693

• Minimize the constraints necessary for rename.

  robrix

  committed
  905dde2

• Minimize the constraints necessary for renameUnification.

  robrix

  committed
  9f18d6a

• Remove a redundant import.

  robrix

  committed
  a75a412

• Typecheck types without checkInferred.

  robrix

  committed
  6f8d0fd