summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
2018-12-12Add a test case for various simple boolean propertiesAlasdair Armstrong
2018-12-12Generalise existentials for non-integer type variablesAlasdair
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
2018-12-10Various changes:Alasdair Armstrong
2018-12-08Compiling againAlasdair
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-12-04Remove FES_Fexps constructorAlasdair Armstrong
2018-12-04Simplify kinds in the ASTAlasdair Armstrong
2018-11-19Don't re-check AST repeatedly in exp_lift_assign re-writeAlasdair Armstrong
2018-11-19Ensure sizeof re-writing occurs for configuration registersAlasdair Armstrong
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-10-31Add rewriting pass for not-patternsAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
2018-10-22Coq: work around constructors with tupled argumentsBrian Campbell
2018-10-16rewrites: remove now-unnecessary temporary string hack from rewrite_defs_pat_...Jon French
2018-10-11Change the function type in the ASTAlasdair
2018-10-04rename stringappend ids for more readable generated codeJon French
2018-10-01Extend Coq pattern match completeness rewrite to let patternsBrian Campbell
2018-10-01New rewriting pass toplevel_string_appendJon French
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19rewrite_defs_pat_string_append: fix bug with guarded SomeJon French
2018-09-17Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on t...Jon French
2018-09-13C: Fix an issue with assigning to unitialized variables at end of blocksAlasdair Armstrong
2018-09-12Jenkins: Fix deprecation warningsAlasdair Armstrong
2018-09-04Add a rewrite to minimise the number of functions marked as recursiveBrian Campbell
2018-08-31rewrite_defs_pat_string_append: only guard the innermost recursive pattern, a...Jon French
2018-08-31mappings: Support for unidirectional mapping clausesJon French
2018-08-28add __POS__ argument to Err_unreachable for better error reportingJon French
2018-08-24Fix rewriter issuesAlasdair Armstrong
2018-08-24support for P_or and P_not patterns in rewrite_defs_mapping_patternsJon French
2018-08-24rewrite_defs_mapping_patterns: support for referring to mapping arguments in ...Jon French
2018-08-24pat_to_exp support for vector and string concat patterns; fix typing in exp_o...Jon French
2018-08-24rewrite_defs_pat_lits: rewrite away fewer lits when generating ocaml, for cle...Jon French
2018-08-23Fix interpreter after re-writer changeAlasdair Armstrong
2018-08-23Move vector_string_to_bit_list from its odd place in Rewriter.rewrite_pat to ...Jon French
2018-08-22Fix a bug in nested vector concatenation patternsAlasdair Armstrong
2018-08-22Revert "rewrite_defs_pat_lits: add an explicit type annotation around generat...Jon French
2018-08-22rewrite_defs_pat_lits: add an explicit type annotation around generated id pa...Jon French
2018-08-17Extend guarded patterns rewriting to exception catchingBrian Campbell
2018-08-16Add the type an expression was checked against to tannots, and use for CoqBrian Campbell
2018-08-13Coq: drop redundant final wildcard clausesBrian Campbell
2018-08-13Guarded clauses rewrite: variable patterns subsume enumsBrian Campbell
2018-08-12Coq: handle enums in binders, make top-level patterns exhaustiveBrian Campbell
2018-08-07Fix propagation of overly-specific types in early_return rewriteBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 10:21:48 +0000