Merge pull request #9 from gauravpartha/int_to_real_conversion

add support for integer to real conversion
gauravpartha · Oct 30, 2023 · ffc8688 · ffc8688
2 parents 4667c53 + 649486b
commit ffc8688
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 3 deletions.
diff --git 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

diff --git 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
@@ -1,5 +1,5 @@
 theory PassificationML
-imports Boogie_Lang.Semantics HelperML Passification
+imports Semantics HelperML Passification
 begin
 
 ML \<open>

diff --git a/BoogieLang/Semantics.thy b/BoogieLang/Semantics.thy
@@ -367,10 +367,16 @@ fun unop_minus :: "lit \<rightharpoonup> lit"
   | "unop_minus (LReal r) = Some (LReal (-r))"
   | "unop_minus _ = None"
 
+fun unop_int_to_real :: "lit \<rightharpoonup> lit"
+  where 
+    "unop_int_to_real (LInt i) = Some (LReal (real_of_int i))"
+  | "unop_int_to_real _ = None"
+
 fun unop_eval :: "unop \<Rightarrow> lit \<rightharpoonup> 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 \<Rightarrow> 'a val \<rightharpoonup> 'a val"
   where

diff --git a/BoogieLang/Typing.thy b/BoogieLang/Typing.thy
@@ -16,6 +16,9 @@ fun unop_type :: "unop \<Rightarrow> prim_ty \<Rightarrow> 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 \<Rightarrow> ((prim_ty \<times> prim_ty) set \<times> prim_ty) option"
   where