Translation from Internal to JuvixCore

[lukaszcz]

Depends on PR #1421

Requirements

• The translation should preserve as much information from the Internal layer as possible.
  • Runtime-relevant information should be translated to the Node data structure.
  • Runtime-irrelevant information should be preserved in InfoTable and in the Infos associated with each Node. The InfoTable data structure might need to be extended, e.g., by information about module structure. New types of Info might need to be defined.
  • An exception is type application and abstraction, i.e., things like x A with A : Type and \A : Type . t. The types used as arguments should be at first translated directly into Nodes using Pi, Univ and TypeConstr. Type abstraction should at first be translated to Lambda (with a BinderInfo which specifies that the type of the bound variable is a universe). Type applications and type abstractions will be removed further down the pipeline.
• The translation should rely as little as possible on the typing information, ideally not at all.
  • The translation should preserve the type information, but not depend on it.
• Natural numbers should be translated to Integers.
  • Builtin arithmetic operations should be translated to corresponding JuvixCore builtins.
• Boolean true and false should be translated to JuvixCore builtin boolean constructors.

Starting point

• JuvixCore parser: Core/Translation/FromSource.hs. The JuvixCore parser shows how to use InfoTableBuilder (which will need to be extended).
• Core/Extra/Base.hs contains useful functions on Node, including the mkIf convenience function.

[lukaszcz]

Closed by #1567