CHANGELOG

# Changelog
All notable changes to this project will be documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

## [0.0.6] - SNAPSHOT
  ### Added
  - Added support for a tuple type. Tuples can now be written as [x y z ...] in the B DSL.
  - Added another eval-ir-formula' function and deprecate eval-ir-formula.
    eval-ir-formula' gives the user more control over the representation of large and symbolic sets.
  - Added `bb` as a function that transforms DSL code into the IR.
  ### Changed
  - Moved `bfile->b` to `lisb.prob.animator` namespace
  - BREAKING (but only in rare cases): The `b` macro now may ignore the namespace of symbols, such as `<--` or `|`.

## [0.0.5]
  ### Added
  - Added Support for Event-B
  - Added Support for Reals in Classical-B
  - Added support for FREETYPES
  - Added working clj-kondo config
  ### Changed
  - Default state space (empty machine) is only loaded if needed (instead of on start-up).
  - Make `if` more similar to `let`: `if-expr` was replaced by `if` which works with both expressions and predicates
  - add support for n-ary tuples in `maplet`
  - add support for variadic version of `b=`
  ### Fixed
  - some nested operators were swallowed by the copy constructors (Java, BParser)

## [0.0.4]
  ### Added:
  - Added definitions
  - Added specs to ir2ast
  ### Changed
  - update ProB 2 dependency
  - Changed ir tag :general-union to :unite-sets
  - Changed ir tag :general-intersection to :intersect-sets
  - Changed ir tag :pre to :precondition
  - Changed ir tag :mul-or-cart to :cartesian-product-or-multiplication
  - Changed lisb2ir function bmul-or-cart to bcart-or-mult
  - Changed key :clauses of machines to :machine-clauses
  - Changed key :clauses of case to :cases
  - Changed ir op to always contain key :returns
  - Changed lisb representation of couple from vector to (|-> left right)/(maplet left right)
  - Changed ir of couple from vector to {:tag :maplet, :left left, :right right}
  - Changed application of to-vector for comprehension-set ids from ir2ast to lisb2ir
  - Changed ir op-call to always contain key :returns

## [0.0.3]
  ### we somehow messed up versions numbers; sorry.
  ### compiling a list of changes are left as an exercise to the reader

## [0.0.2]
  ### Added
  - Added work in progress lisb api doc
  - Added machine-headers refinement, implementation, model and system.
  - Added translation of USES, EXTENDS, INCLUDES, SEES, PROMOTES substitutions.
  - Added translation of case and operation substitution
  - Added parameter support to machine-name.
  - Added multiple arguments for constraints, properties, invariants and init.
      Arguments for constraints, properties and invariants are chained via AConjunctPredicate.
      Arguments for init are chained via ASequenceSubstitution.
  - Added example sebastian with tests.
  - Added multi-arity for subset and strict-subset.
  - Added multi-arity for contains.
  - Added multi-arity subs for any, let-sub, var, precondition and assert.
  - Added cartesian-product and mul to lisb-dsl and ir.
  - Added lisb-dsl:
      {ids | pred} -> (bcomprehension-set ids pred)
      (sets :E :F #{:a :b}) -> (bsets (bdeferred-set :E) (benumerated-set :F :a :b))
      equivalence -> bequivalence,
      implication -> bimplication,
      in -> bmember,
      π -> bpi,
      Σ -> bsigma,
      successor -> bsuccessor,
      predecessor -> bpredecessor,
      div -> bdiv,
      direct-product -> bdirect-product,
      override -> boverride,
      range-subtraction -> brange-subtraction,
      range-restriction -> brange-restriction,
      domain-subtraction -> bdomain-subtraction,
      domain-restriction -> bdomain-restriction,
      |-> bmaplet,
      relation -> brelation,
      <<-> -> btotal-relation,
      <->> -> bsurjective-relation,
      <<->> -> btotal-surjective-relation,
      <- -> bappend,
      -> -> bprepend,
      || -> bparallel-sub,
      becomes-member -> bbecomes-element-of,
      set! -> bassign
  ### Changed
  - Changed lisb-dsl machine layout.
  - Changed all machine-clause-ir-nodes to use :values instead of individually keys for arguments.
  - Changed operations.
  - Changed let.
  - Changed ir subset and strict-subset to support multi-arity.
  - Changed ir contains to support multi-arity.
  - Changed order of cons.
  - Changed comprehension-set ids from set to keyword or vector.
  - Changed ir keys:
      identifier[s] -> id[s],
      predicate[s] -> pred[s],
      expression[s] -> epxr[s],
      element[s] -> elem[s],
      number[s] -> num[s],
      relation[s] -> rel[s],
      operation[s] -> op[s],
      substitution[s] -> sub[s],
      record -> record,
      id-values -> id-vals,
      parameters -> args,
      return -> return-vals
  - Changed lisb2ir function names:
      b<=> -> bequivalence,
      b=> -> bimplication,
      bsubset-strict? -> bstrict-subset?,
      bsuperset-strict? -> bstrict-superset?,
      bcount -> bcard,
      bdifference -> set-,
      bcount-seq -> bsize,
      bcomp-set -> bcomprehension-set,
      binc -> bsuccessor,
      bdec -> bpredecessor,
      b* -> bmul-or-cart,
      b|| -> bparallel-product,
      bcomp -> bcomposition,
      b>< -> bdirect-product,
      b<+ -> boverride,
      b|>> -> brange-subtraction,
      b|> -> brange-restriction,
      b<<| -> bdomain-subtraction,
      b<| -> bdomain-restriction,
      bcouple -> bmaplet,
      b<-> -> brelation,
      bapply -> bfn-call,
      b>->> -> btotal-bijection,
      b>+>> -> bpartial-bijection,
      b>-> -> btotal-injection,
      b>+> -> bpartial-injection,
      b-->> -> btotal-surjection,
      b+->> -> bpartial-surjection,
      b--> -> btotal-function,
      b+-> -> bpartial-function,
      brest -> btail,
      bdrop-last -> bfront,
      bconj -> bappend,
      bcons -> bprepend,
      brec-get -> brecord-get,
      brec -> brecord,
      bop-subs -> bop-sub,
      bsequence-substitution -> bsequential-sub,
      bparallel-substitution -> bparallel-sub,
      boperation-call -> bop-call,
      binvariant -> binvariants
  - Changed ir tags:
      :not= -> :not-equal,
      := -> :equal,
      :subset-strict -> :strict-subset,
      :card -> :cardinality,
      :comp-set -> :comprehension-set,
      :inc -> :successor,
      :dec -> :predecessor,
      :mult-or-cart -> :mul-or-cart,
      :minus -> :sub,
      :plus -> :add,
      :less-eq -> :less-equals,
      :greater-eq -> :greater-equals,
      :relationise -> :rel,
      :functionise -> :fnc,
      :relational-composition -> :composition,
      :relational-override -> :override,
      :relational-image -> :image,
      :inverse-relation -> :inverse,
      :identity-relation -> :id,
      :range -> :ran,
      :domain -> :dom,
      :couple -> :maplet,
      :apply -> :fn-call,
      :restrict-tail -> :drop,
      :restrict-front -> :take,
      :insert-tail -> :append,
      :insert-front -> :prepend,
      :rec-get -> :record-get,
      :rec -> :record,
      :op-subs -> :op-sub,
      :assign -> :assignment,
      :sequence-substitution -> sequential-sub,
      :parallel-substitution -> parallel-sub,
      :operation-call -> op-call
  - Changed lisb-dsl:
      count -> card,
      comp-set -> comprehension-set,
      difference -> set-,
      count-seq -> size,
      subset-strict? -> strict-subset?,
      superset-strict? -> strict-superset?,
      || -> parallel-product,
      comp -> composition,
      identity -> id,
      couple -> maplet,
      apply -> fn-call,
      rec-get -> record-get,
      op-subs -> op-sub,
      sequence-substitution -> sequential-sub,
      parallel-substitution -> parallel-sub,
      operation-call -> op-call,
      invariant -> invariants
  ### Removed
  - Removed maplet/couple chaining.
  - Removed b machine examples for machine-clauses.
  - Removed multi-arity for cons.
  - Removed ir node :distinct. :distinct in now resolved in lisb2ir.


## [0.0.1] - 2021-09-17