From 25c9bb03094ccc389263b41353b27b04ab19127b Mon Sep 17 00:00:00 2001 From: Alex Altair Date: Tue, 17 Jul 2018 12:20:50 -0700 Subject: [PATCH 1/2] Rename op to uniop because it conflicts with Isabelle's op. --- lem/word160.lem | 2 +- lem/word256.lem | 2 +- lem/word32.lem | 2 +- lem/word4.lem | 2 +- lem/word64.lem | 2 +- lem/word8.lem | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lem/word160.lem b/lem/word160.lem index e24ede4..1a8eb81 100644 --- a/lem/word160.lem +++ b/lem/word160.lem @@ -39,7 +39,7 @@ val word160NatOp : (bitSequence -> nat -> bitSequence) -> word160 -> nat -> word let word160NatOp binop w1 n = bs_to_w160 (binop (w160_to_bs w1) n) val word160UnaryOp : (bitSequence -> bitSequence) -> word160 -> word160 -let word160UnaryOp op w = bs_to_w160 (op (w160_to_bs w)) +let word160UnaryOp uniop w = bs_to_w160 (uniop (w160_to_bs w)) val word160ToInteger : word160 -> integer let word160ToInteger w = integerFromBitSeq (w160_to_bs w) diff --git a/lem/word256.lem b/lem/word256.lem index b79ece8..4e843f8 100644 --- a/lem/word256.lem +++ b/lem/word256.lem @@ -43,7 +43,7 @@ val word256NatOp : (bitSequence -> nat -> bitSequence) -> word256 -> nat -> word let word256NatOp binop w1 n = bs_to_w256 (binop (w256_to_bs w1) n) val word256UnaryOp : (bitSequence -> bitSequence) -> word256 -> word256 -let word256UnaryOp op w = bs_to_w256 (op (w256_to_bs w)) +let word256UnaryOp uniop w = bs_to_w256 (uniop (w256_to_bs w)) val size256 : integer let size256 = 2 ** 256 diff --git a/lem/word32.lem b/lem/word32.lem index c264799..35c446e 100644 --- a/lem/word32.lem +++ b/lem/word32.lem @@ -40,7 +40,7 @@ val word32NatOp : (bitSequence -> nat -> bitSequence) -> word32 -> nat -> word32 let word32NatOp binop w1 n = bs_to_w32 (binop (w32_to_bs w1) n) val word32UnaryOp : (bitSequence -> bitSequence) -> word32 -> word32 -let word32UnaryOp op w = bs_to_w32 (op (w32_to_bs w)) +let word32UnaryOp uniop w = bs_to_w32 (uniop (w32_to_bs w)) val size32 : integer let size32 = 2 ** 32 diff --git a/lem/word4.lem b/lem/word4.lem index 94c512e..aa59318 100644 --- a/lem/word4.lem +++ b/lem/word4.lem @@ -39,7 +39,7 @@ val word4NatOp : (bitSequence -> nat -> bitSequence) -> word4 -> nat -> word4 let word4NatOp binop w1 n = bs_to_w4 (binop (w4_to_bs w1) n) val word4UnaryOp : (bitSequence -> bitSequence) -> word4 -> word4 -let word4UnaryOp op w = bs_to_w4 (op (w4_to_bs w)) +let word4UnaryOp uniop w = bs_to_w4 (uniop (w4_to_bs w)) val word4ToNat : word4 -> nat let word4ToNat w = natFromInt (intFromInteger (integerFromBitSeq (w4_to_bs w)) mod 16) diff --git a/lem/word64.lem b/lem/word64.lem index a361acc..b13c6a9 100644 --- a/lem/word64.lem +++ b/lem/word64.lem @@ -42,7 +42,7 @@ val word64NatOp : (bitSequence -> nat -> bitSequence) -> word64 -> nat -> word64 let word64NatOp binop w1 n = bs_to_w64 (binop (w64_to_bs w1) n) val word64UnaryOp : (bitSequence -> bitSequence) -> word64 -> word64 -let word64UnaryOp op w = bs_to_w64 (op (w64_to_bs w)) +let word64UnaryOp uniop w = bs_to_w64 (uniop (w64_to_bs w)) val size64 : integer let size64 = 2 ** 64 diff --git a/lem/word8.lem b/lem/word8.lem index 809a2c6..0fca5bf 100644 --- a/lem/word8.lem +++ b/lem/word8.lem @@ -39,7 +39,7 @@ val word8NatOp : (bitSequence -> nat -> bitSequence) -> word8 -> nat -> word8 let word8NatOp binop w1 n = bs_to_w8 (binop (w8_to_bs w1) n) val word8UnaryOp : (bitSequence -> bitSequence) -> word8 -> word8 -let word8UnaryOp op w = bs_to_w8 (op (w8_to_bs w)) +let word8UnaryOp uniop w = bs_to_w8 (uniop (w8_to_bs w)) val word8ToNat : word8 -> nat let word8ToNat w = natFromInt (intFromInteger (integerFromBitSeq (w8_to_bs w)) mod 256) From 4f78fa983daa98ed599fe1efa43e18bf9cf2f352 Mon Sep 17 00:00:00 2001 From: Alex Altair Date: Tue, 17 Jul 2018 18:17:57 -0700 Subject: [PATCH 2/2] Replace tl with tail to avoid another Isabelle naming conflict. --- lem/evm.lem | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lem/evm.lem b/lem/evm.lem index 735e351..c7c1220 100644 --- a/lem/evm.lem +++ b/lem/evm.lem @@ -1178,8 +1178,8 @@ end val jump : variable_ctx -> constant_ctx -> instruction_result let jump v c = match v.vctx_stack with | [] -> instruction_failure_result v [TooShortStack] - | pos :: tl -> - let v_new = <| v with vctx_stack = tl; vctx_pc = uint pos |> in + | pos :: tail -> + let v_new = <| v with vctx_stack = tail; vctx_pc = uint pos |> in match vctx_next_instruction v_new c with | Just (Pc JUMPDEST) -> InstructionContinue v_new | _ -> instruction_failure_result v [InvalidJumpDestination] @@ -1431,7 +1431,7 @@ let stop v _ = (* POP removes the topmost element of the stack: *) val pop : variable_ctx -> constant_ctx -> instruction_result let pop v c = match v.vctx_stack with - | _ :: tl -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = tl |>) + | _ :: tail -> InstructionContinue (vctx_advance_pc c <| v with vctx_stack = tail |>) | [] -> instruction_failure_result v [TooShortStack] end @@ -1986,7 +1986,7 @@ end val account_state_pop_ongoing_call : account_state -> account_state let account_state_pop_ongoing_call orig = match orig.account_ongoing_calls with - | _ :: tl -> <| orig with account_ongoing_calls = tl |> + | _ :: tail -> <| orig with account_ongoing_calls = tail |> | _ -> <| orig with account_ongoing_calls = [] |> end