2.0.7

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Parser:

  • New elpi:if version <name> <op> <ma>.<mi>.<p>

• API:

  • New Setup.init takes a ?versions dictionary to declare versions
    of external components
  • New Utils.parse_version

2.0.6

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Compiler:
  • Store timing info only optionally to restore build reproducibility
  • Fix collision between kinds and types in namespace handling

2.0.5

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Parser:
  • Fix loc issues involving quotations

2.0.4

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Type Checker:
  • Fix caching issue, units are now type checked every time they are processed

2.0.3

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Parser:
  • Fix parsing of infix ==> so that A,B ==> C,D means A, (B => (C,D))
    as it is intended to be.

2.0.2

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Really fix tests on 32 bits systems

2.0.1

CHANGES:

Requires Menhir 20211230 and OCaml 4.08 or above.

• Fix tests on 32 bits systems

2.0.0

CHANGES:

Requires Menhir 20211230 and OCaml 4.08 or above.

• Compiler:

  • Change the pipeline completely to make unit relocation unnecessary. Current
    phases are (roughly):

    1. Ast.program —[RecoverStructure]—> Ast.Structured.program
    2. Ast.Structured.program —[Scope,Quotation,Macro]—> Scoped.program (aka API.Compile.scoped_program)
    3. Scoped.program —[Flatten]—> Flat.program
    4. Flat.program —[Check]—> CheckedFlat.program (aka API.Compile.compilation_unit)
    5. CheckedFlat.program —[Spill,ToDbl]—> Assembled.program

    Steps 4 and 5 operate on a base, that is an Assembled.program being
    extended. ToDbl is in charge of allocating constants (numbers) for global
    names and takes place when the unit is assembled on the base. These
    constants don't need to be relocated as in the previous backend that
    would allocate these constants much earlier.

  • Change compilation units can declare new builtin predicates

  • Fix macros are hygienic

  • New type checker written in OCaml. The new type checker is faster,
    reports error messages with a precise location and performs checking
    incrementally when the API for separate compilation is used.
    The new type checker is a bit less permissive since the old one would
    merged together all types declaration before type checking the entire
    program, while the new one type checks each unit using the types declared
    inside the unit or declared in the base it extends, but not the types
    declared in units that (will) follow it.

  • Remove the need of typeabbrv string (ctype "string") and similar

  • New type check types and kinds (used to be ignored).

• API:

  • Change quotations generate Ast.Term.t and not RawData.t. The data
    type Ast.Term.t contains locations (for locating type errors) and
    has named (bound) variables and type annotations in Ast.Type.t.
  • New Compile.extend_signature and Compile.signature to extend a
    program with the signature (the types, not the code) of a unit
  • New Ast.Loc.t carries a opaque payload defined by the host application
  • Remove Query, only RawQuery is available (or Compile.query)

• Parser:

  • Remove legacy parser
  • New % elpi:if version op A.B.C and % elpi:endif lexing directives
  • New warning for A => B, C to be disabled by putting parentheses
    around A => B.

• Language:

  • New infix ==> standing for application but with "the right precedence™",
    i.e. A ==> B, C means A => (B, C).
  • New pred is allowed in anonymous predicates, eg:
    pred map i:list A, i:(pred i:A, o:B), o:list B declares that the first
    argument of map is a predicate whose first argument is in input and
    the second in output. Currently the mode checker is still in development,
    annotations for higher order arguments are ignored.
  • New attribute :functional can be passed to predicates (but not types).
    For example, :functional pred map i:list A, i:(:functional pred i:A, o:B), o:list B
    declares map to be a functional predicate iff its higher order argument is
    functional. Currently the determinacy checker is still in development, these
    annotations are ignored.
  • New func keyword standing for :functional pred. The declaration above
    can be shortened to func map i:list A, i:(func i:A, o:B), o:list B.
  • New type annotations on variables quantified by pi as in pi x : term \ ...
  • New type casts on terms, as in f (x : term)
  • New attribute :untyped to skip the type checking of a rule.

• Stdlib:

  • New std.list.init N E L builds a list L = [E, ..., E] with length N
  • New std.list.make N F L builds the list L = [F 0, F 1, ..., F (N-1)]
  • New triple data type with constructor triple and projections triple_1...

• Builtins:

  • Remove string_to_term, read, readterm, quote_syntax

• REPL:

  • Remove -no-tc, -legacy-parser, -legacy-parser-available
  • New -document-infix-syntax

1.20.0

CHANGES:

Requires Menhir 20211230 and OCaml 4.08 or above.

• Language:

  • attribute :remove to remove a clause from the program

• Compiler:

  • Build the index at assembly time, rather than optimization time.
    This makes compilation slower, but startup faster.
  • Adding clauses before the type/mode declaration of a predicate
    is now forbidden, since they are immediately inserted in the index
    and the type/mode declaration can change the index type

1.19.6

CHANGES:

Requires Menhir 20211230 and OCaml 4.08 or above.

• Runtime:
  • Fix bug in unification code for "automatic intro" (as in the intro tactic)
    of UVar arguments