From 24b106d7d7523d9781e253571a909351d90ceaab Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 30 Oct 2023 14:50:21 +0100 Subject: [PATCH 1/2] add support for integer to real conversion --- BoogieLang/Lang.thy | 2 +- BoogieLang/PassificationML.thy | 2 +- BoogieLang/Semantics.thy | 6 ++++++ BoogieLang/Typing.thy | 3 +++ 4 files changed, 11 insertions(+), 2 deletions(-) diff --git a/BoogieLang/Lang.thy b/BoogieLang/Lang.thy index d0db732..b799431 100644 --- a/BoogieLang/Lang.thy +++ b/BoogieLang/Lang.thy @@ -11,7 +11,7 @@ type_synonym pname = string (* procedure name *) datatype lit = LBool bool | LInt int | LReal real datatype binop = Eq | Neq | Add | Sub | Mul | Div | RealDiv | Mod | Lt | Le | Gt | Ge | And | Or | Imp | Iff -datatype unop = Not | UMinus +datatype unop = Not | UMinus | IntToReal datatype prim_ty = TBool | TInt | TReal diff --git a/BoogieLang/PassificationML.thy b/BoogieLang/PassificationML.thy index 27c8802..9ecc06c 100644 --- a/BoogieLang/PassificationML.thy +++ b/BoogieLang/PassificationML.thy @@ -1,5 +1,5 @@ theory PassificationML -imports Boogie_Lang.Semantics HelperML Passification +imports Semantics HelperML Passification begin ML \ diff --git a/BoogieLang/Semantics.thy b/BoogieLang/Semantics.thy index 81e3c6f..eeef2f3 100644 --- a/BoogieLang/Semantics.thy +++ b/BoogieLang/Semantics.thy @@ -367,10 +367,16 @@ fun unop_minus :: "lit \ lit" | "unop_minus (LReal r) = Some (LReal (-r))" | "unop_minus _ = None" +fun unop_int_to_real :: "lit \ lit" + where + "unop_int_to_real (LInt i) = Some (LReal (real_of_int i))" + | "unop_int_to_real _ = None" + fun unop_eval :: "unop \ lit \ lit" where "unop_eval Not v = unop_not v" | "unop_eval UMinus v = unop_minus v" + | "unop_eval IntToReal v = unop_int_to_real v" fun unop_eval_val :: "unop \ 'a val \ 'a val" where diff --git a/BoogieLang/Typing.thy b/BoogieLang/Typing.thy index b756817..d17985d 100644 --- a/BoogieLang/Typing.thy +++ b/BoogieLang/Typing.thy @@ -16,6 +16,9 @@ fun unop_type :: "unop \ prim_ty \ prim_ty option" | "unop_type Not TInt = None" | "unop_type Not TReal = None" | "unop_type Not TBool = Some TBool" + | "unop_type IntToReal TInt = Some TReal" + | "unop_type IntToReal TReal = None" + | "unop_type IntToReal TBool = None" primrec binop_type :: "binop \ ((prim_ty \ prim_ty) set \ prim_ty) option" where From 649486bd4cc9befc2e0a8a3d2d19be61a1fbef55 Mon Sep 17 00:00:00 2001 From: gauravpartha Date: Mon, 30 Oct 2023 15:19:27 +0100 Subject: [PATCH 2/2] fix CI, since Isabelle 2022 is not anymore the current version --- .github/workflows/ci.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 351b59d..ffea94f 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -19,7 +19,7 @@ jobs: - name: Download and install Isabelle run: | - wget --quiet https://isabelle.in.tum.de/dist/Isabelle2022_linux.tar.gz + wget --quiet https://isabelle.in.tum.de/website-Isabelle2022/dist/Isabelle2022_linux.tar.gz tar -xf Isabelle2022_linux.tar.gz rm Isabelle2022_linux.tar.gz mv Isabelle2022 isabelle_dir