diff options
| author | Christopher Pulte | 2016-12-09 15:02:47 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2016-12-09 15:02:47 +0000 |
| commit | 66f2498b28fe4a9be40c2b4093f64827a146f371 (patch) | |
| tree | 40cac4e1c024638f5ade988ba235b41c7d619b7a /mips/hgen | |
| parent | 1495ba7749f9678c36e5fe130948d425d2a345ff (diff) | |
sail changes for making lem embedding Isabelle-friendlier
Diffstat (limited to 'mips/hgen')
| -rw-r--r-- | mips/hgen/herdtools_types_to_shallow_types.hgen | 12 | ||||
| -rw-r--r-- | mips/hgen/shallow_types_to_herdtools_types.hgen | 12 |
2 files changed, 12 insertions, 12 deletions
diff --git a/mips/hgen/herdtools_types_to_shallow_types.hgen b/mips/hgen/herdtools_types_to_shallow_types.hgen index 115de27c..5a0e3bfc 100644 --- a/mips/hgen/herdtools_types_to_shallow_types.hgen +++ b/mips/hgen/herdtools_types_to_shallow_types.hgen @@ -100,21 +100,21 @@ let translate_imm16 name value = let translate_imm5 name value = Sail_values.to_vec0 is_inc (Nat_big_num.of_int 5,Nat_big_num.of_int value) let translate_bool name = function - | true -> Sail_values.I - | false -> Sail_values.O + | true -> Sail_values.B1 + | false -> Sail_values.B0 let translate_wordsize _ = function - | MIPSByte -> Mips_embed_types.B0 + | MIPSByte -> Mips_embed_types.B2 | MIPSHalf -> Mips_embed_types.H | MIPSWord -> Mips_embed_types.W | MIPSDouble -> Mips_embed_types.D let translate_cmp _ = function - | MIPS_EQ -> EQ_ + | MIPS_EQ -> EQ' | MIPS_NE -> NE | MIPS_GE -> GE | MIPS_GEU -> GEU - | MIPS_GT -> GT_ + | MIPS_GT -> GT' | MIPS_LE -> LE - | MIPS_LT -> LT_ + | MIPS_LT -> LT' | MIPS_LTU -> LTU diff --git a/mips/hgen/shallow_types_to_herdtools_types.hgen b/mips/hgen/shallow_types_to_herdtools_types.hgen index 88743ac0..a02d83b7 100644 --- a/mips/hgen/shallow_types_to_herdtools_types.hgen +++ b/mips/hgen/shallow_types_to_herdtools_types.hgen @@ -17,23 +17,23 @@ let translate_out_simm16 imm = translate_out_signed_int imm 16 let translate_out_imm5 imm = translate_out_int imm let translate_out_bool = function - | Sail_values.I -> true - | Sail_values.O -> false + | Sail_values.B1 -> true + | Sail_values.B0 -> false | _ -> failwith "translate_out_bool Undef" let translate_out_wordWidth = function - | Mips_embed_types.B0 -> MIPSByte + | Mips_embed_types.B2 -> MIPSByte | Mips_embed_types.H -> MIPSHalf | Mips_embed_types.W -> MIPSWord | Mips_embed_types.D -> MIPSDouble let translate_out_cmp = function - | Mips_embed_types.EQ_ -> MIPS_EQ (* equal *) + | Mips_embed_types.EQ' -> MIPS_EQ (* equal *) | Mips_embed_types.NE -> MIPS_NE (* not equal *) | Mips_embed_types.GE -> MIPS_GE (* signed greater than or equal *) | Mips_embed_types.GEU -> MIPS_GEU (* unsigned greater than or equal *) - | Mips_embed_types.GT_ -> MIPS_GT (* signed strictly greater than *) + | Mips_embed_types.GT' -> MIPS_GT (* signed strictly greater than *) | Mips_embed_types.LE -> MIPS_LE (* signed less than or equal *) - | Mips_embed_types.LT_ -> MIPS_LT (* signed strictly less than *) + | Mips_embed_types.LT' -> MIPS_LT (* signed strictly less than *) | Mips_embed_types.LTU -> MIPS_LTU (* unsigned less than or qual *) |