summaryrefslogtreecommitdiff
path: root/src/type_check.mli
AgeCommit message (Expand)Author
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-09-23Allow more access to parts of Env (needed by minisail)Mark Wassell
2020-06-23Fix bug with duplicate enum identifiers in patternsAlasdair
2020-04-21Mono: Check for non-constant calls to make_the_valueThomas Bauereiss
2020-03-18Expose details of failed lexp bounds checksThomas Bauereiss
2019-12-10Introduce new bitfield syntax for ASL translationAlasdair Armstrong
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-04-16Coq: don't record assertions in the context if Sail doesn'tBrian Campbell
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-04Type_check: functions env/typ_of_tannotJon French
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-03-04Type_check: make prover reference in env an option defaulting to NoneJon French
2019-03-01WIP: Start working on being able to slice single instructions out of specsAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-18Add option to linearize constraints containing exponentialsAlasdair Armstrong
2019-02-18Rename Type_check.solve -> Type_check.solve_uniqueAlasdair Armstrong
2019-02-14Fix issues for versions of z3 confused by 2^nAlasdair Armstrong
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-12Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair Armstrong
2019-02-08Remove dead code from type-checkerAlasdair
2019-02-06Make sure type synonym errors have correct location infoAlasdair Armstrong
2019-02-04Fix behavior for fallthrough cases in catch blocksAlasdair Armstrong
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-31Fix an unnecessary cast insertion on assignmentsBrian Campbell
2019-01-31Monomorphisation: improve cast insertion and nexp rewriting on variantsBrian Campbell
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
2019-01-08Improvements for v85Alasdair Armstrong
2018-12-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
2018-12-18Ensure type-variables have consistent namesAlasdair
2018-12-18Revert "Experiment with generating type variable names in a repeatable way"Alasdair
2018-12-18Experiment with generating type variable names in a repeatable wayAlasdair Armstrong
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
2018-12-12Add a test case for various simple boolean propertiesAlasdair Armstrong
2018-12-12Generalise existentials for non-integer type variablesAlasdair
2018-12-10Various changes:Alasdair Armstrong
2018-12-08Compiling againAlasdair
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-12-04Simplify kinds in the ASTAlasdair Armstrong
2018-11-30Remove constraint synonymsAlasdair Armstrong
2018-11-15When outputing latex do not expand type synonyms in val specs during type check.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:06:45 +0000