summaryrefslogtreecommitdiff
path: root/language
AgeCommit message (Collapse)Author
2014-01-07lem homs and type headersKathy Gray
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-17Convert coerce to a relation that generates a new expression, inserting ↵Kathy Gray
coercion function calls where applicable.
2013-12-16fix l2_rules to grammar updateKathy Gray
2013-12-10Fixed bug in interpreterKathy Gray
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-28Updated syntax with working examplesKathy 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-11Merge branch 'new-lem-lib'Gabriel Kerneis
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-07Most of the function type systemKathy Gray
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-25More type rulesKathy Gray
2013-10-23Thread type environment through expressions because of block adding new ↵Kathy Gray
variables, say in each branch of an if, that we want to be visible beyond it.
2013-10-23Don't export list of types to ML ASTGabriel Kerneis
2013-10-22More type systemKathy Gray
2013-10-18Typeing rules for patterns and easy expressionsKathy Gray
2013-10-11Supporting all expressions, although vector cacentation pattern matching can ↵Kathy Gray
only match simple patterns (until type information is available).
2013-10-09Adding memory writes. Cleaning up the let in the ott file to reflect what ↵Kathy Gray
actually parses
2013-10-09extend language of lexp to include memory writesKathy Gray
2013-10-04Clean up build systemGabriel Kerneis
2013-09-26Adding undefinedKathy Gray
Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)
2013-09-09Fixes bugs in pretty printer to generate legal lem syntax; split ott grammar ↵Kathy Gray
and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it.
2013-09-09Pretty printer to Lem ast added; accessed by -lem_ast on the command lineKathy Gray
2013-09-05workaround likely aux rule bugPeter Sewell
2013-09-05More type checking, and trying to generate Lem from the ottKathy Gray
2013-09-04Kind checking and part of type checking getting startedKathy Gray
2013-09-02Fix enumerate syntax in l2.ottGabriel Kerneis
2013-08-30Small clean up of ott files, start of environments for formal representation ↵Kathy Gray
of kind and type system
2013-08-22Pretty printer for whole AST; due to parenthesis not always being placed ↵Kathy Gray
where needed, what is generated may not parse
2013-08-19language.ott: update syntax of index rangesGabriel Kerneis
2013-08-19language.ott: syntax for types in patternsGabriel Kerneis
2013-08-19Add loops and document optionnal else in conditionalGabriel Kerneis
Syntax: foreach id from exp (to|downto) exp (by exp)? exp foreach and by are keywords; from, to and downto aren't.
2013-08-14More cases translating from parse_ast to ast. Plus parser changes to syntax ↵Kathy Gray
to support type casts; syntax changes not yet reflected in ott file
2013-08-08More forms converting from parse_ast to ast; also removed some annot aux ↵Kathy Gray
homs for terms that only need locations and not full annotations
2013-08-01More removal of ws from l2.ott, correction to parser, and adding finite-map ↵Kathy Gray
as preliminary to some minor type checking (for environments)
2013-08-01Lex and discard commentsGabriel Kerneis
2013-07-31Adding reporting basic from Lem development, also adding basic error ↵Kathy Gray
messages for syntax and lexical errors (i.e. syntax error and location information)
2013-07-26A parser without any conflicts.Kathy Gray
The ott files have been adjusted to reflect some syntax changes in typquant specifications, and the type annotations are not optional for function definitions; we need additional syntax to help the parser if we want to allow functions without type annotations.
2013-07-26Remove white space/terminal trackingKathy Gray
2013-07-24Parser compiles and compiles some very small test programs.Kathy Gray
Output is only given in the event of a parse or lex failure (with poor reporting for now) There are still 10 shift/reduce conflicts that may need further investigating and a few syntax changes that need discussion.
2013-07-24Missed files from previous commitKathy Gray
2013-07-23Down to 7 shift/reduce conflicts (with 0 reduce/reduce). Possibly some ↵Kathy Gray
syntax needs to change. ott file now builds a pdf again
2013-07-23wibPeter Sewell
2013-07-18More parsingKathy Gray
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-16 11:16:16 +0000