Merge pull request #9 from gauravpartha/int_to_real_conversion

add support for integer to real conversion

Author: gauravpartha

.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

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

BoogieLang/PassificationML.thy

@@ -1,5 +1,5 @@
 theory PassificationML
-imports Boogie_Lang.Semantics HelperML Passification
+imports Semantics HelperML Passification
 begin
 
 ML \<open>

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

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