summaryrefslogtreecommitdiff
path: root/src/initial_check.ml
AgeCommit message (Collapse)Author
2017-02-03fix headersPeter Sewell
2016-08-14Start adding form for (a,b,c) := foo()Kathy Gray
Not working yet
2016-07-24Make sure that all type constructors with unit type have a type union with ↵Kathy Gray
just an id (hopefully fixes Christopher issue).
2016-07-23Add a return exp form to Sail, supported in type checker and in interpreter.Kathy Gray
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-05-27Add sizeof to sail. Documentation to followKathy Gray
2016-03-02Add new language feature to permit definitions of items of kind Nat, etc as ↵Kathy Gray
well as items of kind Type. Syntax for the feature is: def Nat id = nexp Note: some useful nexps may not parse properly. All typedef forms can also be used as def Type ... if desired, but this is not required.
2016-02-23Several fixesKathy Gray
Improve printing for asl to sail readability; Add -o option for selecting the name of file generation; Add additional initial check module for turning generated ast nodes into ready-to-type-check ast nodes
2016-01-06Add new assert expression to SailKathy Gray
This splits the former functionality of exit into errors, which should now use assert(bool,option<string>), and a means of signalling actions such as instruction-level exceptions, interrupts, or other features that impact the ISA. The latter will now be tracked with an effect escape, and so any function containing exit and declared pure will generate a type error. WARNING: ARM spec will not build with this commit until I modify it. MIPS spec will not build with this commit until modified.
2015-06-24Support new memory write events in the sail front end and pretty printerKathy Gray
Events are eamem to signal the memory address to write to and wmv to pass the value to write
2015-06-15Fix strange resulting type for functions with val spec, favouring the ↵Kathy Gray
declared return type when consistent instead of using the derived one.
2015-05-13Add dynamic footprint dependency check event/outcomeKathy Gray
Also fix type checker bug in not reporting modifications to parameter values
2015-03-26Add subtraction to nexp grammar (removing the need to do a + (-1 * b))Kathy Gray
Fix up parsing on 2** precedence Fix errors on type variables in function definition
2014-12-16Fix bug on nat/type/order/effect variable bindingKathy Gray
Fix bug allowing function types in too many places
2014-09-30Add type annotations to funcls to track effects and constraints from one ↵Kathy Gray
function-clause
2014-08-28fixes to bugs exposed by arm modelKathy Gray
2014-07-29A file can now declare that a default order is either inc or dec, and this ↵Kathy Gray
will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *) default order inc register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon.
2014-07-18Writing to concatenated aliasesKathy Gray
2014-07-14Initial support for aliases and exit through the type system and the ↵Kathy Gray
interpreter. An alias can be read within the interpreter, but not written to. Exits aren't yet taken in the interpreter.
2014-06-26Adding better support for unspecified values in indexed vectorsKathy Gray
Also begining to add support for nondeterministic blocks and cleaning up some of the Many warnings on pattern matches
2014-06-25Add support for memory barrierKathy Gray
2014-06-23Get indexed vectors, particularly with default values, workingKathy Gray
2014-06-04Fixup type coercions and overloadingKathy Gray
Reduce the number of implicit coercions we're doing, expanding overloading and fixing up types of functions. Warning: test_power does not run as not all overloaded funcitons are implemented Warning: vector concatenation does not pretty print to sail source yet
2014-05-14More interface update for connecting externally (interp_interface provides ↵Kathy Gray
functions for connecting the interpreter to a memory model) Also adding default values to index vectors for supporting sparse vectors/maps
2014-04-28Add support for overloading for better constraints, and for reducing the ↵Kathy Gray
number of coercions
2014-04-15Put conditional path information into constraint gathering so that checking ↵Kathy Gray
uses appropriate information gleaned from pattern matching
2014-04-08Reduce redundant information in ASTKathy Gray
2014-03-31Extend constraint checking, and add casts for base of a vector shifts (i.e. ↵Kathy Gray
from 0 to 32 etc, doesn't change order yet.).
2014-03-03Fixing assorted bugs. Adding ability to put a type on the identifier being ↵Kathy Gray
assigned to in assignments.
2014-02-28Correct bug in parsing and handling a['a:'b] typesKathy Gray
2014-02-21Add type annotations to lem grammar, including printing out the annotated ↵Kathy Gray
ast, and extending the interpreter to expect annotations. Annotations and locations are still not used by the interpreter.
2014-02-18Adding explicit order to for loopsKathy Gray
2014-02-05Fix type id parsing error ans associated type checking bugs in scatteredsKathy Gray
2014-01-17Type check through type definitions and val specifications, building ↵Kathy Gray
definition environment. Skipping function definition, let bind, and expression checking for this commit (to come).
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-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-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-14Fix pattern match so that P_id is selected when P_app has no parametersKathy Gray
2013-10-09Adding memory writes. Cleaning up the let in the ott file to reflect what ↵Kathy Gray
actually parses
2013-09-26Adding undefinedKathy Gray
Also interpreter now supports reading and writing of basic registers (i.e with no subranges yet)
2013-08-20Set some initial kind environments; start pretty printingKathy Gray
2013-08-19Translate foreach from Parse_ast to AstGabriel Kerneis
2013-08-16Full translation from parse_ast to ast; which includes kind checking and ↵Kathy Gray
pulling scattered defintiions together, with checking on name overlap and not "ending" definitions
2013-08-15Checks up to scattered defsKathy Gray
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-13more translation from parse_ast to astKathy Gray
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-07Starting checks and translation from parse_ast to ast, including an internal ↵Kathy Gray
representation of types to support unification; importing support modules from Lem including pp and util
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:56:03 +0000