From 10d9569a643c47758446816a6e76b427deea01d9 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 10 Oct 2023 11:24:40 +1100 Subject: [PATCH] Fix machine-code compiler code in face of thm rebinding restrictions Fix is to explicitly allow rebinds when this code makes its definitions and does its theorem-saving. --- examples/machine-code/decompiler/decompilerLib.sml | 6 +++++- examples/machine-code/hoare-triple/tailrecLib.sml | 3 +++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/examples/machine-code/decompiler/decompilerLib.sml b/examples/machine-code/decompiler/decompilerLib.sml index fae6e430c7..201319ce55 100644 --- a/examples/machine-code/decompiler/decompilerLib.sml +++ b/examples/machine-code/decompiler/decompilerLib.sml @@ -12,7 +12,11 @@ struct val (Type, Term) = parse_from_grammars addressTheory.address_grammars end -val new_definition = Definition.new_definition (* not boolSyntax! *) +fun allow_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x +val new_definition = + allow_rebinds Definition.new_definition (* not boolSyntax! *) +val save_thm = allow_rebinds save_thm + (* -------------------------------------------------------------------------- *) (* Decompilation stages: *) diff --git a/examples/machine-code/hoare-triple/tailrecLib.sml b/examples/machine-code/hoare-triple/tailrecLib.sml index 71a5e1569a..ab2d735cd1 100644 --- a/examples/machine-code/hoare-triple/tailrecLib.sml +++ b/examples/machine-code/hoare-triple/tailrecLib.sml @@ -11,6 +11,9 @@ struct end val tailrec_definitions = ref ([]:thm list); +fun allow_rebinds f x = Feedback.trace ("Theory.allow_rebinds", 1) f x +val new_definition = allow_rebinds new_definition +val save_thm = allow_rebinds save_thm (* tactic, move to helperLib? *)