summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-08-23TypoBrian Campbell
2017-08-23Update monomorphisation test scriptBrian Campbell
2017-08-23Syntax updates in monomorphisationBrian Campbell
2017-08-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-22Type quantification elimination working for hexapod specAlasdair Armstrong
2017-08-22Added debugging output for E_record and E_record_update in ast_utilAlasdair Armstrong
2017-08-22Add option to dump monomorphised ast before (re-)typecheckingBrian Campbell
2017-08-22Adapt first part of union monomorphisation to existential typesBrian Campbell
2017-08-22Added basic support for pure record definitions and functional recordAlasdair Armstrong
updates to the new typechecker
2017-08-22More work on quantifier eliminationAlasdair Armstrong
2017-08-21More work on quantifier elimination passAlasdair Armstrong
Also added a rewriting pass that removes the cast annotations and operator overloading declarations from the AST because they arn't supported by the interpreter.
2017-08-21Modified sizeof rewriting pass so it can correctly deal with existentials.Alasdair Armstrong
Basically we needed to make the rewriting step for E_sizeof and E_constraint more aggressively try to rewrite those expressions from variables in scope, without adding new parameters to pass the type variables at runtime, as this can break in the presence of existential quantification. Still some cleanup to do in this code, but tests on the arm spec show that it now introduces the minimal amount of new parameters.
2017-08-21Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-18Correct indexing and equality for bitvectorsBrian Campbell
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
Also: Merge remote-tracking branch 'origin/sail_new_tc' into experiments
2017-08-17Work on E_constraint removal pass and diagnosing bugs in E_sizeof removal passAlasdair Armstrong
2017-08-17Add E_constraint support to re-writerAlasdair Armstrong
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
Make state monad parametric in register state, and generate a record with registers from the Sail spec
2017-08-17Various sail fixes for ASL hexapodAlasdair Armstrong
2017-08-17Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into ↵Brian Campbell
mono-experiments
2017-08-17Merge remote-tracking branch 'origin' into mono-experimentsBrian Campbell
# Conflicts: # src/type_internal.ml
2017-08-17fixed the RISC-V fences (3 types: "rw,rw"/"r,rw"/"rw,w")Shaked Flur
2017-08-16Added the feature to bind type variables in patterns.Alasdair Armstrong
The reason you want this is to do something like (note new parser only): ********* default Order dec type bits 'n:Int = vector('n - 1, 'n, dec, bit) val zeros : forall 'n. atom('n) -> bits('n) val decode : bool -> unit function decode b = { let 'datasize: {|32, 64|} = if b then 32 else 64; let imm: bits('datasize) = zeros(datasize); () } ********* for the ASL decode functions, where the typechecker now knows that the datasize variable and the length of imm are the same.
2017-08-16Eta-expansion in sail_values to make OCaml happyBrian Campbell
2017-08-16lem_interp: remove broken val_to_string_internal functions, replace with ↵Jon French
string_of_value as used everywhere else
2017-08-15Merge remote-tracking branch 'origin/mono-experiments' into experimentsAlasdair Armstrong
2017-08-15Removed Typ_arg_effect - nobody used it and it isn't supported by the backends.Alasdair Armstrong
2017-08-15Export existential destructuring function in type_check.mli.Alasdair Armstrong
Also rename some functions for consistency.
2017-08-15Export utility functions from type_check.mlAlasdair Armstrong
2017-08-15Menhir parser support for try/catchAlasdair Armstrong
2017-08-15Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-15Added exceptions and try/catch blocks to AST and typechecker in orderAlasdair Armstrong
to translate exceptions in ASL. See test/typecheck/pass/trycatch.sail.
2017-08-14Existentials in free type var functionsBrian Campbell
2017-08-14Some overloaded equality support in monomorphisationBrian Campbell
2017-08-14Merge remote-tracking branch 'origin/master' into experimentsAlasdair Armstrong
2017-08-14Merge remote-tracking branch 'origin/mono-experiments' into experimentsAlasdair Armstrong
2017-08-14More constructs in menhir parser, plus support for both left and right infix ↵Alasdair Armstrong
operators.
2017-08-14Keep all asserts in the program during type checkingBrian Campbell
2017-08-14Don't reverse lexp tuple during type checkingBrian Campbell
2017-08-12Resolve ambiguity between negation of integers and boolsThomas Bauereiss
2017-08-12Fix compilation issue for 32-bit systemsThomas Bauereiss
2017-08-11Menhir for new parser, ocamlyacc for oldBrian Campbell
2017-08-11Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-11Make type checking just clever enough to solve 8*n = constantBrian Campbell
2017-08-10Merge remote-tracking branch 'origin/sail_new_tc' into experimentsAlasdair Armstrong
Conflicts: src/pretty_print_common.ml
2017-08-10Fix bug with subtyping in let bindingsAlasdair Armstrong
2017-08-10Improved operator support for test menhir parserAlasdair Armstrong
2017-08-10Experimenting with alternate parserAlasdair Armstrong
2017-08-10Add support for early return to Lem backendThomas Bauereiss
Implemented using the exception monad, by throwing and catching the return value
2017-08-10Disable menhir on this branchBrian Campbell
(until location information is updated)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 14:18:39 +0000