From db3a8b4ea70d6fb3d301053bde3f19de7bfe0eeb Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Wed, 30 Oct 2024 10:36:59 +0100 Subject: [PATCH] reduce metaprogramming in incr example --- examples/riscv/incr/incrScript.sml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/examples/riscv/incr/incrScript.sml b/examples/riscv/incr/incrScript.sml index 836bf774a..b07eb9334 100644 --- a/examples/riscv/incr/incrScript.sml +++ b/examples/riscv/incr/incrScript.sml @@ -3,20 +3,19 @@ open HolKernel Parse; open bir_lifter_interfaceLib; open birs_auxLib; -val progname = "incr"; - val _ = Parse.current_backend := PPBackEnd.vt100_terminal; val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2; -val _ = new_theory progname; +val _ = new_theory "incr"; -val _ = lift_da_and_store progname (progname ^ ".da") da_riscv ((Arbnum.fromInt 0x10488), (Arbnum.fromInt 0x10498)); +val _ = lift_da_and_store "incr" "incr.da" da_riscv + ((Arbnum.fromInt 0x10488), (Arbnum.fromInt 0x10498)); (* ----------------------------------------- *) (* Program variable definitions and theorems *) (* ----------------------------------------- *) -val bir_prog_def = DB.fetch progname ("bir_"^progname^"_prog_def"); -val _ = gen_prog_vars_birenvtyl_defthms progname bir_prog_def; +val bir_prog_def = DB.fetch "-" "bir_incr_prog_def"; +val _ = gen_prog_vars_birenvtyl_defthms "incr" bir_prog_def; val _ = export_theory ();