summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-01-08Fix pretty-printing of switch-casesGabriel Kerneis
Weird bug, cf. test/pattern.sail.
2014-01-08Add support for letbound toplevel defs in interpreterKathy Gray
2014-01-08type eq firstKathy Gray
2014-01-07Add first operationnal tests for vectorsGabriel Kerneis
2014-01-07interp: recover identifiers in error messagesGabriel Kerneis
Not displayed currently because of new-lem's lack of string concatenation.
2014-01-07Lex bitzero and bitone literalsGabriel Kerneis
2014-01-07bug: unbound let-defined (and local?) variablesGabriel Kerneis
In test/test1.sail, trying to resolve variable v1 in main yields: test1: error: unbound identifier
2014-01-07Add bit and bitvector literal testGabriel Kerneis
2014-01-07lem homs and type headersKathy Gray
2013-12-19pretty-print: missing quotes for num literals (lem)Gabriel Kerneis
2013-12-19pretty-print: pattern-matching of indexed vectors in Lem outputGabriel Kerneis
Lem tuples must be surrounded by parentheses (contrary to OCaml ones).
2013-12-18More lem homsKathy Gray
2013-12-18Tweak formatting in pretty printer, and resolve bugs.Kathy Gray
Start specifying lem homs for rules.
2013-12-17pretty-printer: fix union constructor applicationGabriel Kerneis
Foo (1,2,3) is stored internally as the function Foo applied to [1; 2; 3]. We need to add commas when pretty-printing. This should not affect pretty-printing of regular functions application, since those always take a single parameter anyway (which may be a tuple).
2013-12-17Convert coerce to a relation that generates a new expression, inserting ↵Kathy Gray
coercion function calls where applicable.
2013-12-17Remove spurious lexing tokensGabriel Kerneis
2013-12-16fix l2_rules to grammar updateKathy Gray
2013-12-16minor wip on tiny modelGabriel Kerneis
2013-12-16test: catch and print exceptionsGabriel Kerneis
2013-12-16pretty-printer: typoGabriel Kerneis
2013-12-16lexer: inc and dec keywordsGabriel Kerneis
2013-12-13Fix effect annotation bug, take 2Kathy Gray
2013-12-13Fix effect annotation pretty-printingGabriel Kerneis
There is also a bug for parsing effect annotations (in fundecl). But for some reason, my fix for the parser does not work: test/test2.sail still refuses to parse (chokes on "effect pure"), even with "Effect" added to parser.mly.
2013-12-10Fixed bug in interpreterKathy Gray
2013-12-06Output test name on startGabriel Kerneis
2013-12-03Syntax changes per discussion with Peter, as well as L2.ott document clean up.Kathy Gray
Could not at this time return lists to [| |] from [|| ||] as the parser cannot distinguish a cast with enum’s syntactic sugar from the start of a parenthesised list (i.e. ( [|3|] ) And there are still conflicts with moving enums to [3], so those changes can’t be pushed in with current parser technology.
2013-11-29Push syntax changes to type rulesKathy Gray
2013-11-29minor syntax fixupsKathy Gray
2013-11-28Updated syntax with working examplesKathy Gray
2013-11-27More front-end passes for type identifiersKathy Gray
2013-11-22Syntax changes per discussions on Thursday.Kathy Gray
First pass parser to identify type names is in progress (current test files fail, will correct once pre-parser is in place)
2013-11-21Begin tiny conversionGabriel Kerneis
2013-11-20Remove workaround in test3Gabriel Kerneis
2013-11-20Fixed the parsing of applicationKathy Gray
2013-11-12Define and test addition in libraryGabriel Kerneis
Notice the need for double parentheses in test/test3.sail, because the interpreter does not perform curryfication automatically (only the first parameter in kept with List_extra.head): add ((1, 3)) (* works *) add (1, 3) (* fails, equivalent to: add (1) *) Fortunately enough, infix functions work correctly by default. A dirty quickfix would be easy, but I'm not sure at which level this should be addressed properly (interpreter? typing? etc.).
2013-11-11Merge branch 'new-lem-lib'Gabriel Kerneis
2013-11-11Remove workaround for a bug fixed in LemGabriel Kerneis
2013-11-11Remove lem-lib hackGabriel Kerneis
Lem has now switched to the new library by default (remember to "make ocaml-libs" in Lem to build it).
2013-11-09Fix up multiple parses issueKathy Gray
2013-11-08Type system, almost certainly has omissions or flaws I've forgotten, but ↵Kathy Gray
seems to be complete. Will update with corrections as necessary during implementation phase.
2013-11-07Port L2 to new LemGabriel Kerneis
Tests compile and run properly. There is a lot of hackery going on to workaround the rough edges of new Lem. Use at your own risk (you need the "library-format" branch of lem).
2013-11-07Stub for external callsGabriel Kerneis
2013-11-07Most of the function type systemKathy Gray
2013-11-05De-infix operator before looking it up in the interpreterGabriel Kerneis
2013-11-05Parsing of infix operatorsGabriel Kerneis
The interpreter is broken for infix calls (fails to find the relevant function, either internal or external).
2013-11-05Support parsing for extern callsGabriel Kerneis
2013-11-05Clean-up build-related filesGabriel Kerneis
2013-11-01Moved metatheory grammars into l2_rules.ottKathy Gray
Added val extern specification to language, parser, printer, and interpreter Added various def level type system support, expressions type system in place Except for assignment
2013-10-30Type coercions and let expressionsKathy Gray
2013-10-29gave Jan write access to repo and added him to email-diffPeter Sewell
created l3-to-l2 directory added notes01 describing the initial plan we just talked about
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 14:16:52 +0000