Code

[WIP] Pairs#10

Code

Open

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

Commits

Commits on Jan 7, 2016

• Stub in a Surface.Language module.

  robrix

  committed
  5417077

  Copy full SHA for 5417077

• Add a type synonym for Term Expression.

  robrix

  committed
  b18aa6d

  Copy full SHA for b18aa6d

• Export Surface.Language.

  robrix

  committed
  d106732

  Copy full SHA for d106732

• Move all of Surface to Surface.Language.

  robrix

  committed
  98b6b9f

  Copy full SHA for 98b6b9f

• Stub in a Surface.Pair module.

  robrix

  committed
  79d199f

  Copy full SHA for 79d199f

• Define a Pair type.

  robrix

  committed
  d94175e

  Copy full SHA for d94175e

• Export Pair.

  robrix

  committed
  a464292

  Copy full SHA for a464292

• Move checkIsType up a bit.

  robrix

  committed
  ea1c0fb

  Copy full SHA for ea1c0fb

• Remove a redundant import.

  robrix

  committed
  b8beb6d

  Copy full SHA for b8beb6d

• Write a few lambdas inline.

  robrix

  committed
  7f40acd

  Copy full SHA for 7f40acd

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

  robrix

  committed
  b6563ba

  Copy full SHA for b6563ba

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

  robrix

  committed
  80e7d35

  Copy full SHA for 80e7d35

• Check that the return type is a type.

  robrix

  committed
  9f6a92d

  Copy full SHA for 9f6a92d

• Just check against type.

  robrix

  committed
  73d0bd5

  Copy full SHA for 73d0bd5

• Unify the types.

  robrix

  committed
  82e1cc7

  Copy full SHA for 82e1cc7

• Move _type into the Language module.

  robrix

  committed
  9261a7d

  Copy full SHA for 9261a7d

• Remove a redundant import.

  robrix

  committed
  09a144d

  Copy full SHA for 09a144d

• Ignore the tags file.

  robrix

  committed
  f3a9a12

  Copy full SHA for f3a9a12

Commits on Jan 8, 2016

• Rename the parameters.

  robrix

  committed
  2c63002

  Copy full SHA for 2c63002

• Test the type of _Pair.

  robrix

  committed
  4fe94bd

  Copy full SHA for 4fe94bd

• Move the language tests into their own module.

  robrix

  committed
  11b820e

  Copy full SHA for 11b820e

• Stub in a Pair module.

  robrix

  committed
  70b7600

  Copy full SHA for 70b7600

• Don’t import Surface.Pair.

  robrix

  committed
  82b2d08

  Copy full SHA for 82b2d08

• Stub in a Definition type.

  robrix

  committed
  75fb47c

  Copy full SHA for 75fb47c

• Only represent the type of definitions for now.

  robrix

  committed
  5f74131

  Copy full SHA for 5f74131

• Modules are lists of definitions.

  robrix

  committed
  72e7f99

  Copy full SHA for 72e7f99

• Remove a redundant import.

  robrix

  committed
  3ac0257

  Copy full SHA for 3ac0257

• Remove a bogus $.

  robrix

  committed
  e7dcfeb

  Copy full SHA for e7dcfeb

• Define Definition using record syntax.

  robrix

  committed
  f2add1e

  Copy full SHA for f2add1e

• Add a lookup operator for Module.

  robrix

  committed
  68a1a71

  Copy full SHA for 68a1a71

• Export Data.Module.

  robrix

  committed
  0fdb668

  Copy full SHA for 0fdb668

• Definitions have types and values.

  robrix

  committed
  4562713

  Copy full SHA for 4562713

• Correct the type of Pair.

  robrix

  committed
  c869d4d

  Copy full SHA for c869d4d

• Add a function to typecheck a definition.

  robrix

  committed
  c4ebecc

  Copy full SHA for c4ebecc

• Add a function to typecheck modules.

  robrix

  committed
  46fe06f

  Copy full SHA for 46fe06f

• Rename the test subject.

  robrix

  committed
  c6977c8

  Copy full SHA for c6977c8

• None of this “should” business.

  robrix

  committed
  966ed36

  Copy full SHA for 966ed36

• Test that the module typechecks.

  robrix

  committed
  028a7fe

  Copy full SHA for 028a7fe

• Correct the inference of function types.

  robrix

  committed
  deba278

  Copy full SHA for deba278

• Unification carries a typechecker.

  robrix

  committed
  25cb9ff

  Copy full SHA for 25cb9ff

• Check pi types like function types.

  robrix

  committed
  0e49f82

  Copy full SHA for 0e49f82

Commits on Jan 9, 2016

• lts-4.

  robrix

  committed
  3aeaedf

  Copy full SHA for 3aeaedf

• Default compiler check.

  robrix

  committed
  5bd111b

  Copy full SHA for 5bd111b

• 4.0, that is.

  robrix

  committed
  94b6b94

  Copy full SHA for 94b6b94

• Add a checkFunctionType function.

  robrix

  committed
  6541127

  Copy full SHA for 6541127

• Use the Checker synonym.

  robrix

  committed
  b4f4b03

  Copy full SHA for b4f4b03

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

  robrix

  committed
  0b9d66a

  Copy full SHA for 0b9d66a

• Recur into abstractions.

  robrix

  committed
  40ed0d2

  Copy full SHA for 40ed0d2

• Add a type synonym for environments.

  robrix

  committed
  369ee1f

  Copy full SHA for 369ee1f

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

  robrix

  committed
  c41e8bf

  Copy full SHA for c41e8bf

• Lookup variables for whnf.

  robrix

  committed
  12de9d8

  Copy full SHA for 12de9d8

• Substitute inside applications in whnf.

  robrix

  committed
  cda5fec

  Copy full SHA for cda5fec

• Reduce applications to whnf correctly.

  robrix

  committed
  b793b40

  Copy full SHA for b793b40

• byUnifying recurs via expectUnifiable.

  robrix

  committed
  7d65f48

  Copy full SHA for 7d65f48

• Use the Term' shorthand everywhere we can.

  robrix

  committed
  05eb00b

  Copy full SHA for 05eb00b

• Module is defined in terms of Term'.

  robrix

  committed
  7a4651e

  Copy full SHA for 7a4651e

• Abstract Definition over a term type.

  robrix

  committed
  d1af2bb

  Copy full SHA for d1af2bb

• Abstract Definition over the expression type.

  robrix

  committed
  7c1a611

  Copy full SHA for 7c1a611

• Abstract Module over the expression type.

  robrix

  committed
  0b1b6fc

  Copy full SHA for 0b1b6fc

• Abstract Module and Definition over the term type.

  robrix

  committed
  74ac43f

  Copy full SHA for 74ac43f

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

  robrix

  committed
  4329f99

  Copy full SHA for 4329f99

• We’re no longer dependent on StandaloneDeriving.

  robrix

  committed
  1e98610

  Copy full SHA for 1e98610

• Equality of conflicts.

  robrix

  committed
  1a1a2d8

  Copy full SHA for 1a1a2d8

• Inequality of other comparisons.

  robrix

  committed
  c7aca05

  Copy full SHA for c7aca05

• Move the Unification module under Surface.

  robrix

  committed
  bc5c75f

  Copy full SHA for bc5c75f

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

  robrix

  committed
  bdd3daa

  Copy full SHA for bdd3daa

• Stub in a Surface.Renaming module.

  robrix

  committed
  444187a

  Copy full SHA for 444187a

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

  robrix

  committed
  3efe2a7

  Copy full SHA for 3efe2a7

• Resort the exports.

  robrix

  committed
  a51b467

  Copy full SHA for a51b467

• Export Surface.Renaming.

  robrix

  committed
  c70f301

  Copy full SHA for c70f301

• Move renaming into Surface.Renaming.

  robrix

  committed
  91a9e19

  Copy full SHA for 91a9e19

• Move unification into Surface.Unification.

  robrix

  committed
  30af305

  Copy full SHA for 30af305

• annotation typechecking doesn’t use expectUnifiable.

  robrix

  committed
  17bfaf1

  Copy full SHA for 17bfaf1

• Minimize the set of constraints necessary for annotation.

  robrix

  committed
  0d97693

  Copy full SHA for 0d97693

• Minimize the constraints necessary for rename.

  robrix

  committed
  905dde2

  Copy full SHA for 905dde2

• Minimize the constraints necessary for renameUnification.

  robrix

  committed
  9f18d6a

  Copy full SHA for 9f18d6a

• Remove a redundant import.

  robrix

  committed
  a75a412

  Copy full SHA for a75a412

• Typecheck types without checkInferred.

  robrix

  committed
  6f8d0fd

  Copy full SHA for 6f8d0fd