diff options
| author | Thomas Bauereiss | 2017-12-05 17:05:22 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-12-06 14:54:28 +0000 |
| commit | c3c3c40a1d4f81448d8356317e88be2b04363df7 (patch) | |
| tree | 4caeea3f28af968a59241df7a7ebd1828fd61086 /src/lem_interp/sail_impl_base.lem | |
| parent | 4a7d6e6d7e9221a19bc50c627b5714e45b1748bc (diff) | |
Make AST after rewriting for Lem backend type-checkable
- Add support for some internal nodes to type checker
- Add more explicit type annotations during rewriting
- Remove hardcoded rewrites for E_vector_update etc from Lem pretty-printer;
these will be resolved by the type checker during rewriting now
Diffstat (limited to 'src/lem_interp/sail_impl_base.lem')
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index eb2e1a4e..c7c6cd20 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -643,7 +643,7 @@ instance (Ord write_kind) let (>=) = write_kindGreaterEq end -(* Barrier comparison that uses less memory in Isabelle/HOL +(* Barrier comparison that uses less memory in Isabelle/HOL *) let ~{ocaml} barrier_number = function | Barrier_Sync -> (0 : natural) | Barrier_LwSync -> 1 @@ -660,15 +660,15 @@ let ~{ocaml} barrier_number = function | Barrier_MIPS_SYNC -> 12 end - let ~{ocaml} barrier_kindCompare bk1 bk2 = +let ~{ocaml} barrier_kindCompare bk1 bk2 = let n1 = barrier_number bk1 in let n2 = barrier_number bk2 in if n1 < n2 then LT else if n1 = n2 then EQ else GT -*) +let inline {ocaml} barrier_kindCompare = defaultCompare -let ~{ocaml} barrier_kindCompare bk1 bk2 = +(*let ~{ocaml} barrier_kindCompare bk1 bk2 = match (bk1, bk2) with | (Barrier_Sync, Barrier_Sync) -> EQ | (Barrier_Sync, _) -> LT @@ -722,8 +722,7 @@ let ~{ocaml} barrier_kindCompare bk1 bk2 = (* | (Barrier_MIPS_SYNC, _) -> LT | (_, Barrier_MIPS_SYNC) -> GT *) - end -let inline {ocaml} barrier_kindCompare = defaultCompare + end*) let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT |