Code

Complete rewrite of the parser#84

Code

Open

redelmann wants to merge 120 commits intoscala-2.13epfl-lara/inox:scala-2.13from refactor-parserepfl-lara/inox:refactor-parserCopy head branch name to clipboard

+7,019-4,775

Commits

Commits on Jul 31, 2018

• Add HoleType, which indicates the type of values expected by a hole

  redelmann

  committed
  a399596

  Copy full SHA for a399596

• Add an interpolator implemented with macros

  redelmann

  committed
  fb2cb3a

  Copy full SHA for fb2cb3a

• Add implicit store argument to getDefinitions

  redelmann

  committed
  b4a4941

  Copy full SHA for b4a4941

• Add HoleValues class

  redelmann

  committed
  992bc06

  Copy full SHA for 992bc06

• Parse holes in function application position to identifier by default

  Show description for 38d9a9f
  redelmann

  committed
  38d9a9f

  Copy full SHA for 38d9a9f

• Add replaceHoles functions

  redelmann

  committed
  5207dd8

  Copy full SHA for 5207dd8

• Fix macros implementations

  redelmann

  committed
  70c693b

  Copy full SHA for 70c693b

• Use replaceHoles to feed parameters of quasiquotes

  redelmann

  committed
  267926f

  Copy full SHA for 267926f

• Code quality and comment

  redelmann

  committed
  0dd8c2d

  Copy full SHA for 0dd8c2d

• Add macro extractor for types

  Show description for bc2e3be
  redelmann

  committed
  bc2e3be

  Copy full SHA for bc2e3be

Commits on Aug 2, 2018

• Refactoring

  redelmann

  committed
  304b999

  Copy full SHA for 304b999

• Use MacroInterpolator as the default interpolator

  redelmann

  committed
  b04eb26

  Copy full SHA for b04eb26

• Handle implicit symbols

  redelmann

  committed
  7ba44a7

  Copy full SHA for 7ba44a7

• Comment out the warning for using default

  redelmann

  committed
  66b60de

  Copy full SHA for 66b60de

• Remove useless import

  redelmann

  committed
  972da12

  Copy full SHA for 972da12

• Rename interpolator-related classes and fix their hierarchy

  redelmann

  committed
  6861e4b

  Copy full SHA for 6861e4b

• Add unapply for expressions

  redelmann

  committed
  ba8a399

  Copy full SHA for ba8a399

• Refactor

  redelmann

  committed
  4ad9907

  Copy full SHA for 4ad9907

• Add s to MacroInterpolator

  redelmann

  committed
  d318c59

  Copy full SHA for d318c59

• Add definition interpolators to the macro interpolator

  redelmann

  committed
  dd8aef7

  Copy full SHA for dd8aef7

• Add the concept of a Binding to the IRs

  redelmann

  committed
  e3a0955

  Copy full SHA for e3a0955

• Add different constructors for bindings

  redelmann

  committed
  dede1ca

  Copy full SHA for dede1ca

• Some fixes

  redelmann

  committed
  96866dc

  Copy full SHA for 96866dc

Commits on Aug 3, 2018

• First draft

  redelmann

  committed
  8e55f16

  Copy full SHA for 8e55f16

• More work

  redelmann

  committed
  9d3fa24

  Copy full SHA for 9d3fa24

• Simplify constrained.

  redelmann

  committed
  4503a96

  Copy full SHA for 4503a96

Commits on Aug 4, 2018

• Refactor harder, structure looks better now

  redelmann

  committed
  46ae7c2

  Copy full SHA for 46ae7c2

• Yet more refactoring

  redelmann

  committed
  834e118

  Copy full SHA for 834e118

Commits on Aug 6, 2018

• Refactor harder

  redelmann

  committed
  a53fb38

  Copy full SHA for a53fb38

• Greatly simplify the types IR, use Store to resolve all names, even primitives

  redelmann

  committed
  944d23b

  Copy full SHA for 944d23b

• More work on Expr, refactor HSeq

  redelmann

  committed
  344d7e8

  Copy full SHA for 344d7e8

• Remove context for elaborators, add result for matchings

  redelmann

  committed
  13cc34a

  Copy full SHA for 13cc34a

• Also split binding extractor in two

  redelmann

  committed
  9e127bc

  Copy full SHA for 9e127bc

• Yet in the middle of refactoring

  redelmann

  committed
  7d3f7dd

  Copy full SHA for 7d3f7dd

Commits on Aug 7, 2018

• More work on extractor and elaborator

  redelmann

  committed
  f8cea27

  Copy full SHA for f8cea27

• Add a size specification parameter to the Bits typeclass, to support casts

  redelmann

  committed
  cdc3807

  Copy full SHA for cdc3807

• Done with extractors

  redelmann

  committed
  1792417

  Copy full SHA for 1792417

• Finish expression elaborator

  redelmann

  committed
  dc1f710

  Copy full SHA for dc1f710

• Add bidirectional conversions between simple types and inox types

  redelmann

  committed
  43ad977

  Copy full SHA for 43ad977

Commits on Aug 8, 2018

• Implement constraint solver

  redelmann

  committed
  e5aa08e

  Copy full SHA for e5aa08e

Commits on Aug 9, 2018

• Work towards elaboration of function definitions

  redelmann

  committed
  4d84f96

  Copy full SHA for 4d84f96

• Add function extractor

  redelmann

  committed
  d182bc9

  Copy full SHA for d182bc9

• Add simple adts and fully implement store

  redelmann

  committed
  93b5696

  Copy full SHA for 93b5696

Commits on Aug 10, 2018

• Add ADT elaborator and extractor

  redelmann

  committed
  fd8f6ba

  Copy full SHA for fd8f6ba

Commits on Aug 15, 2018

• Add lexer and parsers, fix some bugs

  redelmann

  committed
  ee6c027

  Copy full SHA for ee6c027

• Separate the namespaces of types and expressions

  redelmann

  committed
  8d4894a

  Copy full SHA for 8d4894a

• Add Liftable instances for the various IRs

  redelmann

  committed
  c8986a4

  Copy full SHA for c8986a4

• Add macro interpolator for types

  redelmann

  committed
  3e6ea5f

  Copy full SHA for 3e6ea5f

Commits on Aug 16, 2018

• Add macro interpolators for expressions

  redelmann

  committed
  ecad27c

  Copy full SHA for ecad27c

• Add function definition macros interpolators

  redelmann

  committed
  cb44839

  Copy full SHA for cb44839

• Fix bugs in parser and hseq extractor

  redelmann

  committed
  08c000f

  Copy full SHA for 08c000f

• Add explicit type argument to HSeq call in macro

  redelmann

  committed
  d75951c

  Copy full SHA for d75951c

• Accept syntactic sugar for refinement types, fix bugs

  redelmann

  committed
  2918334

  Copy full SHA for 2918334

• Add macro interpolator for value definitions and type definitions

  redelmann

  committed
  84cb940

  Copy full SHA for 84cb940

• Package all internal values in companion object of Interpolator

  redelmann

  committed
  12578f4

  Copy full SHA for 12578f4

• Fix bug in elaboration of IsConstructor

  redelmann

  committed
  052aa44

  Copy full SHA for 052aa44

• Add interpolator for programs

  redelmann

  committed
  e5936b4

  Copy full SHA for e5936b4

Commits on Aug 17, 2018

• Handle invocations made to variables

  redelmann

  committed
  94319e0

  Copy full SHA for 94319e0

• Fix bug in macro

  redelmann

  committed
  4ca54ba

  Copy full SHA for 4ca54ba

• Attach positions to IRs

  redelmann

  committed
  49de17b

  Copy full SHA for 49de17b

• Begin working on providing good error messages

  redelmann

  committed
  77686ef

  Copy full SHA for 77686ef

• Continue work on error messages

  redelmann

  committed
  8def752

  Copy full SHA for 8def752

• More work on error messages

  Show description for 3e54005
  redelmann

  committed
  3e54005

  Copy full SHA for 3e54005

Commits on Oct 26, 2018

• Better error messages, add constructors for sets, maps and bags

  redelmann

  committed
  4d5e9a9

  Copy full SHA for 4d5e9a9

Commits on Oct 29, 2018

• Remove old parser, fix bugs, update doc

  redelmann

  committed
  bb42f19

  Copy full SHA for bb42f19

• Fix last merge errors

  redelmann

  committed
  0b0f176

  Copy full SHA for 0b0f176

Commits on Oct 30, 2018

• Use a Macros implementation for interpolators by default in inox.ast.Trees

  redelmann

  committed
  7cf875c

  Copy full SHA for 7cf875c

• Overridable macro interpolators

  samarion

  committed
  ad1019d

  Copy full SHA for ad1019d

Commits on Oct 31, 2018

• Fix bugs, add tests

  redelmann

  committed
  65a7d31

  Copy full SHA for 65a7d31

Commits on Nov 1, 2018

• Remove warning about implicit conversions

  redelmann

  committed
  6db8245

  Copy full SHA for 6db8245

• Add test

  redelmann

  committed
  d984ee2

  Copy full SHA for d984ee2

• Remove debug print

  redelmann

  committed
  2f0b213

  Copy full SHA for 2f0b213

• Fix priority in parser

  redelmann

  committed
  614b5db

  Copy full SHA for 614b5db

• Add tests for elaboration of function definitions

  redelmann

  committed
  619945a

  Copy full SHA for 619945a

• Make the annotated types of macro-generated terms shorter

  redelmann

  committed
  2c6fc13

  Copy full SHA for 2c6fc13

Commits on Nov 5, 2018

• Fix bug with hole in return type of function definition

  redelmann

  committed
  62ff2a7

  Copy full SHA for 62ff2a7

• Add some tests for function definition parsing

  redelmann

  committed
  22e418a

  Copy full SHA for 22e418a

• Fix error message in case of wrong number of arguments

  redelmann

  committed
  32691f1

  Copy full SHA for 32691f1

• Make sure the definitions appear in the same order as they are defined

  redelmann

  committed
  0950745

  Copy full SHA for 0950745

• Tests for program parser

  redelmann

  committed
  89067fc

  Copy full SHA for 89067fc

• Switch from objects to class/val instead, so that it is easier to override

  redelmann

  committed
  ee608ca

  Copy full SHA for ee608ca

Commits on Nov 6, 2018

• Made Lexer and operators overridable

  redelmann

  committed
  8b09b46

  Copy full SHA for 8b09b46

• Unseal all IRs

  redelmann

  committed
  e8a844b

  Copy full SHA for e8a844b

• Add widening and narrowing casts to the parser

  redelmann

  committed
  ca065f4

  Copy full SHA for ca065f4

Commits on Nov 7, 2018

• Unseal HoleType

  redelmann

  committed
  f2cdd47

  Copy full SHA for f2cdd47

Commits on Nov 8, 2018

• Add unsigned bit vectors to the parser

  redelmann

  committed
  f950d85

  Copy full SHA for f950d85

• Simplify complement computation

  redelmann

  committed
  9fab8e4

  Copy full SHA for 9fab8e4

Commits on Nov 21, 2018

• New syntax for sigma and pi types, as well as let expressions

  redelmann

  committed
  71a1910

  Copy full SHA for 71a1910

Commits on Nov 22, 2018

• Add more tests for lets

  redelmann

  committed
  8207d12

  Copy full SHA for 8207d12

• Add block syntax

  redelmann

  committed
  84baa99

  Copy full SHA for 84baa99

• Change syntax for lambda, forall and choose expressions

  redelmann

  committed
  040d038

  Copy full SHA for 040d038

Commits on Nov 23, 2018

• Fix syntax in tests with quantifiers

  redelmann

  committed
  a135c5b

  Copy full SHA for a135c5b

• Fix documentation

  redelmann

  committed
  50acc5b

  Copy full SHA for 50acc5b

• Add test for if-expressions

  redelmann

  committed
  55cc979

  Copy full SHA for 55cc979

• Add syntax for assume

  redelmann

  committed
  2637294

  Copy full SHA for 2637294

• Accept single argument without type to omit parentheses in lambda, forall, choose

  redelmann

  committed
  afb59c0

  Copy full SHA for afb59c0

• Work on a new pretty printer

  redelmann

  committed
  4d358f3

  Copy full SHA for 4d358f3

Commits on Nov 28, 2018

• Add check that the fields have unique names in an ADT

  redelmann

  committed
  2e9cfd8

  Copy full SHA for 2e9cfd8

• Fix broken test

  redelmann

  committed
  019c677

  Copy full SHA for 019c677

• Add literal trait for IR expressions

  redelmann

  committed
  80b1ca3

  Copy full SHA for 80b1ca3

Commits on Dec 3, 2018

• Make it possible to refer to earlier identifiers in sequences of bindings

  redelmann

  committed
  8c7e0b7

  Copy full SHA for 8c7e0b7

Commits on Dec 13, 2018

• Added OneOf to inox solver

  

  Stevan Ognjanovic

  committed
  f92eed2

  Copy full SHA for f92eed2

• Added store changes which are prerequisite for the overloading

  

  Stevan Ognjanovic

  committed
  2e5b958

  Copy full SHA for 2e5b958

Commits on Dec 14, 2018

• Added overloading, all previous tests pass

  

  Stevan Ognjanovic

  committed
  68f28af

  Copy full SHA for 68f28af

• Overloading before extensive testing

  

  Stevan Ognjanovic

  committed
  7b2a68e

  Copy full SHA for 7b2a68e

Commits on Jan 2, 2019

• Function overloading

  

  Stevan Ognjanovic

  committed
  9261ddb

  Copy full SHA for 9261ddb

• Added comments for function name overloading

  

  Stevan Ognjanovic

  committed
  e442a40

  Copy full SHA for e442a40

• Comments for solver

  

  Stevan Ognjanovic

  committed
  d0f01cd

  Copy full SHA for d0f01cd

Commits on Jan 6, 2019

• Before adding examples to report

  

  Stevan Ognjanovic

  committed
  1e6df5b

  Copy full SHA for 1e6df5b

• Solved the problem with OneOf

  

  Stevan Ognjanovic

  committed
  d3a5d4d

  Copy full SHA for d3a5d4d

Commits on Jan 7, 2019

• Overloading should be done

  

  Stevan Ognjanovic

  committed
  f99ecbc

  Copy full SHA for f99ecbc

• Fixed the OneOf

  

  Stevan Ognjanovic

  committed
  9ab927a

  Copy full SHA for 9ab927a

• Fixed another bug

  

  Stevan Ognjanovic

  committed
  a7f26ee

  Copy full SHA for a7f26ee

• Another change to solver

  

  Stevan Ognjanovic

  committed
  03cc038

  Copy full SHA for 03cc038

Commits on Jan 21, 2019

• Added more tests

  

  Stevan Ognjanovic

  committed
  c57f7ab

  Copy full SHA for c57f7ab

• Fixed more bugs

  

  Stevan Ognjanovic

  committed
  987dc1d

  Copy full SHA for 987dc1d

Commits on Jan 22, 2019

• One bug fixed

  

  Stevan Ognjanovic

  committed
  0f22471

  Copy full SHA for 0f22471

Commits on Jan 23, 2019

• Final for presentation

  

  Stevan Ognjanovic

  committed
  e8fbc4e

  Copy full SHA for e8fbc4e

Commits on Jan 24, 2019

• More general unification for pairs, coding style fixes

  

  Stevan Ognjanovic

  committed
  da2c7b5

  Copy full SHA for da2c7b5

Commits on Feb 8, 2019

• Merge pull request #90 from OStevan/overloading

  Show description for 8441ed7
  redelmann

  authored
  8441ed7

  Copy full SHA for 8441ed7