diff options
| author | Alasdair | 2019-02-06 03:20:03 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-06 03:20:03 +0000 |
| commit | 0f736fcb7fd46d902dffa171d1458253b2070b79 (patch) | |
| tree | 06fc9008f7d3e60d3996c132f2db53811741450a /lib | |
| parent | 18d9a16b1cfd442fb05039a326795bcd64cb6a79 (diff) | |
Remove all sizeof rewriting from C compilation
All sizeof expressions now removed by the type-checker, so it's now
properly a type error if they cannot be removed rather than a bizarre
re-write error. This also greatly improves compilation speed overall, at
the expense of the first type-checking pass.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/smt.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/smt.sail b/lib/smt.sail index e73897b1..6a5a1327 100644 --- a/lib/smt.sail +++ b/lib/smt.sail @@ -19,7 +19,7 @@ val mod = { lem: "integerMod", c: "tmod_int", coq: "emod_with_eq" -} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o == mod('n, 'm). atom('o)} +} : forall 'n 'm. (atom('n), atom('m)) -> atom(mod('n, 'm)) overload operator % = {mod} @@ -29,7 +29,7 @@ val abs_atom = { lem: "abs_int", c: "abs_int", coq: "abs_with_eq" -} : forall 'n. atom('n) -> {'o, 'o == abs_atom('n). atom('o)} +} : forall 'n. atom('n) -> atom(abs('n)) $ifdef TEST |