------------SAFECode LLVM Syntax and Semantics--------------------------
fmod NAME is
  including QID .
  sort Name .
  subsort Qid < Name .
--- the following can be used instead of Qids if desired
  ops a b c d e f g h i j k l m n o p q r s t u v x y z w : -> Name .
  op main : -> Name .
endfm

fmod LIST is 
  sort List .
  op nil : -> List . 
  op _,_ : List List -> List [assoc id: nil] .
endfm

fmod NAME-LIST is
  including NAME .
  including LIST .
  sort NameList .
  subsort Name  List < NameList .
  op _,_ : NameList NameList -> NameList [ditto] .
endfm



----- First define primitive types
fmod PRIMITIVE-TYPE is
 sort PrimitiveType .
------ Primitive Types   
  sorts void ubyte ushort uint ulong float label .
  sorts bool sbyte short int long double .
  sorts SignedPrType UnsignedPrType IntType IntegralType FltType .
  
---Defining subtyping relation between diff primitive types 
  subsort label < PrimitiveType .
  subsorts sbyte short int long float double < SignedPrType < PrimitiveType .
  subsorts ulong ushort uint ubyte < UnsignedPrType < PrimitiveType .
  subsorts ubyte sbyte ushort short uint int ulong long < IntType < PrimitiveType .
  subsorts  bool ubyte sbyte ushort short uint int ulong long < IntegralType < PrimitiveType .
  subsorts float double < FltType .

  op int : -> int .
  op sbyte : -> sbyte .
  op short : -> short .
  op void : -> void .
  op unit : -> uint .
  op ubyte: -> ubyte .
  op ushort : -> ushort .
  op ulong : -> ulong .
  op float : -> float .
  op bool : -> bool .
  op long : -> long .
  op double : -> double .
 
endfm 


fmod TYPE is
  pr PRIMITIVE-TYPE .
  pr NAME-LIST .
  including LIST .
  sort Type DerivedType  FirstClassType TypeVar RegionType .
  subsorts TypeVar PrimitiveType DerivedType RegionType < Type .
  subsort Name < TypeVar .

  --- Region type 
  op region(_,_) : TypeVar Type -> RegionType .
  
------ Derived Types
  sorts ArrayType FunctionType StructureType PointerType .
  subsorts ArrayType FunctionType StructureType PointerType < DerivedType .

  sort TypeList .
  subsort Type List < TypeList .
  subsort NameList < TypeList .
  op _, _ : TypeList TypeList -> TypeList [ditto] .

----- (Type Name) List for formal arguments of a function 
  sorts FormalTypeVar FormalTypeVarList .
  subsort FormalTypeVar < FormalTypeVarList .
  op _,_ : FormalTypeVarList FormalTypeVarList -> FormalTypeVarList .
  op _ _ : Type Name -> FormalTypeVar .

--- Array type  
  op [_ x _ ] : int Type -> ArrayType .

--- Function Type     
----  op _ { _ } : Type TypeList -> FunctionType .

--- Structure Type  
---  op {_} : TypeList -> StructureType .

--- Pointer Type 
  op _ @ _  : Type TypeVar  -> PointerType .

----Defining first class types   
  subsorts void ubyte ushort uint ulong float bool sbyte short int long double PointerType < FirstClassType .
endfm


--- We have defined types so far. Now we define the syntax of the language




fmod LLVM-VALUE is
  protecting INT .
  pr TYPE .
  sorts BasicBlock Constant GlobalValue Instruction LLVMValue .
  --- In LLVM everything is derived from Value, so we use the following
  --- subsort (or subtyping relation)
  subsorts BasicBlock Constant GlobalValue Instruction Name < LLVMValue .
endfm

fmod LLVM-VALUELIST is
  including LLVM-VALUE .
  including NAME-LIST .
  sort LLVMValueList .
  subsort LLVMValue < LLVMValueList .
  subsort NameList < LLVMValueList .
  op _,_ : LLVMValueList LLVMValueList -> LLVMValueList [ditto] .
endfm



fmod LLVM-SYNTAX is
including LLVM-VALUELIST .  

--- GlobalValues

sorts Function GlobalVariabe StructureTypeDef .
subsorts Function GlobalVariabe < GlobalValue .


--- Different Types of Constants 

sorts ConstantArray ConstantExpr ConstantFP ConstantIntegral ConstantPointerNull ConstantPointerRef ConstantStruct . 

subsorts ConstantArray ConstantExpr ConstantFP ConstantIntegral ConstantPointerNull ConstantPointerRef ConstantStruct < Constant .

sorts ConstantBool ConstantInt .  
subsorts ConstantBool ConstantInt < ConstantIntegral .

---- first constant Ints 
subsort Int < ConstantInt .

---- constant bools 
op true : -> ConstantBool .
op false : -> ConstantBool .

--- rest of the constants later 
----FIXME Need to add signed and unsigned Int 



----- Instructions 
sorts TerminatorInst BinaryOperator AllocationInst CallInst CastInst FreeInst GetElementPtrInst LoadInst PHINode ShiftInst StoreInst RegionBlockInsts .

subsorts TerminatorInst BinaryOperator AllocationInst CallInst CastInst FreeInst GetElementPtrInst LoadInst PHINode ShiftInst StoreInst RegionBlockInsts < Instruction .

sorts AllocaInst MallocInst .

subsorts AllocaInst MallocInst < AllocationInst .

sort SetCondInst .
subsort SetCondInst < BinaryOperator .

sorts BranchInst InvokeInst ReturnInst SwitchInst UnwindInst .
subsorts BranchInst InvokeInst ReturnInst SwitchInst UnwindInst < TerminatorInst .

----op getVarName(_) : LLVMValue -> Name .
op getOp0 : LLVMValue -> LLVMValue .
op getOp1 : LLVMValue -> LLVMValue .


op ret _ _ : Type LLVMValue -> ReturnInst .
op ret void : -> ReturnInst .

op br _, label _, label _ : LLVMValue label label  -> BranchInst .
op br label _ : label -> BranchInst .

--- FIXME Switch instruction add later
--- FIXME Invoke instruction add later
--- FIXME Unwind instruction add later
--- Binary ops
sort  BinaryOp .

op add :  -> BinaryOp .
op sub :  -> BinaryOp .
op div : -> BinaryOp .
op mul : -> BinaryOp .
op rem : -> BinaryOp .

var nam : Name .
var typ : Type .
vars op1 op0 : LLVMValue .
var bop : BinaryOp .

op _ = _ _ _, _  : Name BinaryOp Type LLVMValue LLVMValue -> BinaryOperator .
op getBinaryOp : BinaryOperator -> BinaryOp .

op getVarName(_) : LLVMValue -> Name .
op getType(_) : LLVMValue -> Type .

eq getType(nam = bop typ op1, op0) = typ .
eq getVarName(nam = bop typ op1, op0) = nam .
eq getOp0(nam = bop typ op0, op1) = op0 .
eq getOp1(nam = bop typ op0, op1) = op1 .
eq getBinaryOp(nam = bop typ op1, op0) = bop .

--- SetCondInsts 
op _ = seteq _ _, _ : Name Type LLVMValue LLVMValue -> SetCondInst .
op _ = setne _ _, _ : Name Type LLVMValue LLVMValue -> SetCondInst .
op _ = setlt _ _, _ : Name Type LLVMValue LLVMValue -> SetCondInst .
op _ = setgt _ _, _ : Name Type LLVMValue LLVMValue -> SetCondInst .
op _ = setle _ _, _ : Name Type LLVMValue LLVMValue -> SetCondInst .
op _ = setge _ _, _ : Name Type LLVMValue LLVMValue -> SetCondInst .

---- Bitwise And ops
op _ = and _ _, _ : Name Type LLVMValue LLVMValue -> BinaryOperator .
op _ = or _ _, _ : Name Type LLVMValue LLVMValue -> BinaryOperator .
op _ = xor _ _, _ : Name Type LLVMValue LLVMValue -> BinaryOperator .
op _ = shl _ _, _ : Name Type LLVMValue LLVMValue -> BinaryOperator .
op _ = shr _ _, _ : Name Type LLVMValue LLVMValue -> BinaryOperator .


--- Mem Access

op _ = malloc _, uint _ : Name Type LLVMValue -> MallocInst .
op _ = malloc _ : Name Type -> MallocInst .
eq getVarName(nam = malloc typ, uint op1) = nam .
eq getVarName(nam = malloc typ) = nam .

op _ = alloca _, uint _ : Name Type LLVMValue -> AllocaInst .
op _ = alloca _ : Name Type -> AllocaInst .
---
op free _ _ : Type LLVMValue -> FreeInst .


op _ = load _ _ : Name PointerType LLVMValue -> LoadInst .
var ptype : PointerType .
eq getOp0(nam = load ptype op0) = op0 .
eq getVarName(nam = load ptype op0) = nam .

op store _ _, _ _ : Type LLVMValue PointerType LLVMValue -> StoreInst .
eq getOp0(store typ op0, ptype op1) = op0 .
eq getOp1(store typ op0, ptype op1) = op1 .

op _ = getelementptr _ _ _ : Name PointerType LLVMValue long -> GetElementPtrInst .

------FIXME : takes only two args now, should take multiple arguments.
op _ = phi _ [ _, _ ], [ _, _ ] : Name Type LLVMValue label LLVMValue label -> PHINode .

op _ = cast _ _ to _ : Name Type LLVMValue Type -> CastInst .

op _ = call _ _ { _ } : Name PointerType LLVMValue LLVMValueList -> CallInst .


sort Module .

----  GlobalValue Set (a set makes use of efficient AC matching)
sorts GlobalValueSet .
subsorts GlobalValue  < GlobalValueSet < Module .
---op _ _ : GlobalValueSet GlobalValueSet -> GlobalValueSet [assoc comm] .


---- Basic Block Set
sorts BasicBlockLabel BasicBlockLabelSet .
subsorts BasicBlockLabel  < BasicBlockLabelSet  .
op _: _ : label BasicBlock -> BasicBlockLabel .
op emptybb : -> BasicBlockLabelSet .
op _ _ : BasicBlockLabelSet BasicBlockLabelSet -> BasicBlockLabelSet [assoc comm id: emptybb ] .


var bbl : BasicBlockLabel .
var bbls : BasicBlockLabelSet .
var labl : label .
var bb : BasicBlock .

op getBasicBlock : BasicBlockLabel -> BasicBlock .
eq getBasicBlock(labl : bb) = bb .

op getBasicBlockList : BasicBlockLabelSet -> LLVMValueList .
eq getBasicBlockList(bbl bbls) = getBasicBlock(bbl), getBasicBlockList(bbls) .
eq getBasicBlockList(emptybb) = nil .

sort InstructionList .
subsorts Instruction  < InstructionList < BasicBlock .
op _ ; _  : InstructionList InstructionList -> InstructionList [assoc] .


-------- Now we can define a function

op declare _ _(_) : Type Name TypeList -> Function .
op _ _(_) { _ } :  Type Name FormalTypeVarList BasicBlockLabelSet -> Function .
op _ _() {_} :  Type Name  BasicBlockLabelSet -> Function .

var fv : Name .
var tvl : FormalTypeVarList .
var bbll : BasicBlockLabelSet .
op FnName : Function -> Name .
op Body : Function -> BasicBlockLabelSet .
op TypeVars : Function -> FormalTypeVarList .
eq FnName(t fv(tvl) { bbll }) = fv .
eq Body(t fv(tvl) { bbll }) = bbll .
eq TypeVars(t fv(tvl) { bbll }) = tvl .

----------Region based memory annotations
op poolinit(_,_) _ { _ } : TypeVar Type Name BasicBlockLabelSet -> RegionBlockInsts .
op getRegionTypeVar : RegionBlockInsts -> TypeVar .
op getTypeObjectsInRegion : RegionBlockInsts -> Type .
op getRegionVarName : RegionBlockInsts -> Name .
op getBBLS : RegionBlockInsts -> BasicBlockLabelSet .

var tvar : TypeVar .
eq getRegionTypeVar( poolinit(tvar, typ) nam { bbls }) = tvar .
eq getTypeObjectsInRegion(poolinit(tvar, typ) nam { bbls }) = typ .
eq getRegionVarName(poolinit(tvar, typ) nam { bbls }) = nam .
eq getBBLS(poolinit(tvar, typ) nam { bbls }) = bbls .

op _ = poolalloc(_) : LLVMValue LLVMValue -> MallocInst .
eq getVarName(nam = poolalloc(op0)) = nam .
eq getOp0(nam = poolalloc(op0)) = op0 .

op poolfree(_,_) : LLVMValue LLVMValue -> Instruction .
eq getOp0(poolfree(op0, op1)) = op0 .
eq getOp1(poolfree(op0, op1)) = op0 .

---- Other annotations



---- Global Variable With Initializeer 
op _ = constant _ _ : Name Type Constant -> GlobalVariabe .
op _ = internal constant _ _ : Name Type Constant -> GlobalVariabe .
----

op _ = type _ : TypeVar StructureType -> StructureTypeDef .

endfm




------------LLVM Type checker & Typing Rules--------------------------------
----- FIX me implement later.


-------------LLVM Semantics---------------------------------------------
--- Organization

--- Assume every ssa value is stored in memory.

--- Environment is a map between name and location

--- Store is the normal store a  map between the heap location and
--- the value stored in it.

fmod VALUE is
  pr INT .
  sort Value .
  op int : Int -> Value .
  op loc : Nat -> Value .
endfm

fmod VALUE-LIST is
  including VALUE .
  including LIST .
  including LLVM-VALUELIST .
  sort ValueList .
  subsort LLVMValue < Value .
  subsort Value List < ValueList .
  subsort LLVMValueList < ValueList .
  op _,_ : ValueList ValueList -> ValueList [ditto] .
endfm

fmod STORE is
  including VALUE-LIST .
  sort Store .
  op empty : -> Store .
  op [_ _] : Value Value -> Store .
  op __ : Store Store -> Store [assoc comm id: empty] .
  op _[_] : Store Value -> [Value] .
  op _[_<-_] : Store ValueList ValueList -> [Store] .
  vars L L' : Value .  var Mem : Store .  vars V V' : Value .
  var Ll : ValueList .  var Vl : ValueList .
  eq ([L V] Mem)[L] = V .
  eq ([L' V'] Mem)[L <- V]
   = if L == L' then [L' V] Mem else [L' V'] (Mem[L <- V]) fi .
  eq empty[L <- V] = [L V] .
  eq Mem[L,Ll <- V,Vl] = Mem[L <- V][Ll <- Vl] .
  eq Mem[nil <- nil] = Mem .
endfm


fmod ENVIRONMENT is
  including VALUE-LIST .
  including NAME-LIST .
  sort Entry FlatEnv Env .
  subsort Entry < FlatEnv < Env .
  op [_,_] : Name Value -> Entry .

  op empty : -> FlatEnv .
  op __ : FlatEnv FlatEnv -> FlatEnv [assoc id: empty] .

  op push : FlatEnv Env -> Env .
  op pop : Env -> Env .
  op addEntry : Entry Env -> Env .
  
  op _[# _ #] : Env LLVMValue -> Value [prec 10] .

  op _[_<-_] : Env NameList ValueList -> Env .
  op _[_<-_] : Env Name Value -> Env .
  subsort Int  < LLVMValue .
  var FlatEnv : FlatEnv .  var Env : Env .  var Il : ValueList .
  vars V V' : Name .  
  vars I I' : Value .
  var II : Int .
  var Sv : Name .  var Svl : NameList .

  eq Env[# II #] = II . 
  
  eq pop(push(FlatEnv, Env)) = Env .

  eq ([V',I'] FlatEnv)[# V #] =
     if V == V' then I' else FlatEnv[# V #] fi .
  eq empty[# V #] = int(0) .
  eq push([V',I'] FlatEnv, Env)[# V #] =
     if V == V' then I' else push(FlatEnv, Env)[# V #] fi .
  eq push(empty, Env)[# V #] = Env[# V #] .

  eq push([V',I'] FlatEnv, Env)[V <- I] =
     if V == V' then push([V,I] FlatEnv, Env)
     else addEntry([V',I'], push(FlatEnv, Env)[V <- I]) fi .
  eq push(empty, Env)[V <- I] = push(empty, Env[V <- I]) .
  eq addEntry([V',I'], push(FlatEnv, Env)) = push([V',I'] FlatEnv, Env) .
  eq ([V',I'] FlatEnv)[V <- I] =
     if V == V' then [V,I] FlatEnv else [V',I'] (FlatEnv[V <- I]) fi .
  eq empty[V <- I] = [V,I] .

  eq Env[(Sv,Svl) <- (I,Il)] = Env[Sv <- I][Svl <- Il] .
  eq Env[(Sv,Svl) <- nil] = Env[Sv <- int(0)][Svl <- nil]  .
  eq Env[Sv <- nil] = Env[Sv <- int(0)] .
  eq Env[nil <- nil] = Env .
endfm

----- We have defined environment and the
fmod SIMPLE-STATE is
  sorts PLStateAttribute PLState .
  including ENVIRONMENT .
  including STORE .
  including LLVM-SYNTAX .
  op empty : -> PLStateAttribute .
  op __ : PLStateAttribute PLStateAttribute -> PLStateAttribute [assoc comm id: empty] .
  op {_ ; _} : PLStateAttribute LLVMValueList -> PLState .
  op PLSA : PLState -> PLStateAttribute .
  op LLValue : PLState -> ValueList .
  var plsa : PLStateAttribute .
  var llvl : ValueList . 
  eq PLSA({ plsa ; llvl }) = plsa .
  eq LLValue({ plsa ; llvl }) = llvl .
  
  op nextLoc : Nat -> PLStateAttribute .
  op mem : Store -> PLStateAttribute .
  op input : ValueList -> PLStateAttribute .
  op output : ValueList -> PLStateAttribute .
  op env : Env -> PLStateAttribute .
  endfm


---- I am not using continuations to describe the semantics
---- Although it is possible to describe it them 
---  I want the semantics as close to SOP as possible
---  that way we can prove the safety of the type system in the
---- standard way.
fmod LLVM-SEMANTICS-HELPER is
  including LLVM-SYNTAX .
  including VALUE .
  op getBinary : Value Value BinaryOp -> Value .
  vars i1 i2 : Int .
  eq getBinary(int(i1), int(i2), add) = int(i1 + i2) .
  ---- Add the rest of binary operations later
  endfm
fmod LLVM-SEMANTICS is
  including SIMPLE-STATE .
  including LLVM-SYNTAX .
  including LLVM-SEMANTICS-HELPER .
  var bopr : BinaryOperator .
  var inst : Instruction .
  var instl : InstructionList .
  vars Env Env' : Env .
  var pls pls' : PLStateAttribute .
  vars i1  i2 : Int .
  vars varx y z : Name .
  var llval llval2 : LLVMValueList .
  vars llva llva2  : LLVMValue .
  vars val1 val2 : Value .
  ---- Binary operators 
  ceq { env(Env) pls ;  bopr } =  { env(Env'[getVarName(bopr) <- getBinary(val1, val2, getBinaryOp(bopr))]) pls' ; nil } if {env(Env') pls' ; val1 , val2 } := { env(Env) pls ; (getOp0(bopr), getOp1(bopr))} .

  ---- For variables 
  eq { env(Env) pls ; varx } = { env(Env) pls ; Env[# x #] } .

  ---- For constants 
  eq {pls ; i1 } = { pls ; int(i1) } .

  ---- For list of values 
  ceq { pls ; (llva, llva2, llval) } = { PLSA({ pls' ; llva2 , llval }) ; (val1 , LLValue({ pls' ; llva2, llval })) }
      if { pls' ; val1 } := { pls ; llva } .

  --- For the sequencing operation    
  ceq { pls ; inst ; instl } = { pls' ; instl } 
      if { pls' ; nil } := { pls ; inst } .

  --- For the malloc operation
  var malinst : MallocInst .
  var Mem : Store . 
  eq { nextLoc(i1) mem(Mem) env(Env) pls ; malinst } =
    { mem(Mem[loc(i1) <- int(0)]) env(Env[getVarName(malinst) <- loc(i1)]) nextLoc(i1 + 1) pls ; nil } .

  ---- For the store operation
  var storeinst : StoreInst .

  ceq { mem(Mem) env(Env) pls ; storeinst } = { mem(Mem[loc(i1) <- Env[# getOp0(storeinst)#]]) env(Env) pls ; nil } 
   if loc(i1) := Env[# getOp1(storeinst) #] .


  ---- For the load operation
  var loadinst : LoadInst .
 ceq { mem(Mem) env(Env) pls ; loadinst } = { mem(Mem) env(Env[getVarName(loadinst) <- Mem[loc(i1)] ]) pls ; nil } 
   if loc(i1) := Env[# getOp0(loadinst) #] .


 ---- Main missing, struct handling, free, pointer arithmetic  etc       

   
 endfm

fmod TYPE-ENVIRONMENT is
  protecting NAME-LIST .
  pr TYPE .
  sort TypeEnv .
  op empty : -> TypeEnv .
  op [_,_] : Name Type -> TypeEnv .
  op __ : TypeEnv TypeEnv -> TypeEnv [assoc comm id: empty] .
  op _[_] : TypeEnv Name -> [Type] .
  op _[_<-_] : TypeEnv NameList TypeList -> TypeEnv .
  var X : Name .  vars TEnv : TypeEnv .  vars T T' : Type .
  var Xl : NameList .  var Tl : TypeList .
  eq ([X,T] TEnv)[X] = T .
  eq TEnv[nil <- nil] = TEnv .
  eq ([X,T] TEnv)[X,Xl <- T' , Tl] = ([X,T'] TEnv)[Xl <- Tl] .
  eq TEnv[X,Xl <- T, Tl] = (TEnv [X,T])[Xl <- Tl] [owise] .
endfm

fmod TYPE-STATE is
  extending TYPE-ENVIRONMENT .
  including LLVM-SYNTAX .
  sorts TypeStateAttribute TypeState .
----  subsort TypeStateAttribute < TypeState .
  op empty : -> TypeStateAttribute .
  op __ : TypeStateAttribute TypeStateAttribute -> TypeStateAttribute [assoc comm id: empty] .
  op tenv : TypeEnv -> TypeStateAttribute .

  sort TypeOrLLVMValue .
  subsorts  LLVMValue Type  < TypeOrLLVMValue .

  sort TypeOrLLVMValueList .
  subsort TypeOrLLVMValue List < TypeOrLLVMValueList .
  op _,_ : TypeOrLLVMValueList TypeOrLLVMValueList -> TypeOrLLVMValueList [ditto] .
  subsorts  LLVMValueList TypeList < TypeOrLLVMValueList .
  
  op { _ ; _ } : TypeStateAttribute TypeOrLLVMValueList -> TypeState .
  op TSA : TypeState -> TypeStateAttribute .
  op TL : TypeState -> TypeList .

  var tsa : TypeStateAttribute .
  var tl : TypeList .
  eq TSA({tsa ; tl }) = tsa .
  eq TL({tsa ; tl}) = tl .
endfm


fmod STATIC-TYPING-SEMANTICS is
  including LLVM-SYNTAX .
  including TYPE-STATE .

  vars tsa tsa' : TypeStateAttribute .
  vars TEnv TEnv'  : TypeEnv .
  vars llva llva2 : LLVMValue .
  var llval : LLVMValueList .
  var I : Int .
  var varx : Name .

  --- type checking bopr
  var bopr : BinaryOperator .
  ceq { tenv(TEnv) tsa  ; bopr } = { tenv(TEnv[getVarName(bopr) <- int]) ; nil } 
     if { tenv(TEnv') tsa' ;   (int , int) } := { tenv(TEnv) ;  getOp0(bopr), getOp1(bopr) } .

  ---- List of LLVMValues
  var typ : Type .
   ceq { tsa ; (llva, llva2, llval) } = { TSA( {tsa' ; llva2, llval}) ; (typ , TL({tsa' ; llva2, llval})) }  if {tsa' ; typ } := { tsa ; llva } .

  ---- ints
  eq { tsa ; I } = {tsa ; int} .

  --- variables 
  eq { tenv(TEnv) tsa  ; varx } = { tenv(TEnv) tsa ; TEnv[varx] } .

  --- region types
  var regioninst : RegionBlockInsts .
  eq { tenv(TEnv) tsa ; regioninst } =
  { tenv(TEnv[getRegionVarName(regioninst) <- region(getRegionTypeVar(regioninst), getTypeObjectsInRegion(regioninst))]) tsa ; getBasicBlockList(getBBLS(regioninst)) } . 

  --- poolalloc instructions
   var poolallocinst : MallocInst .
   var rho : TypeVar .
  ceq { tenv(TEnv) tsa ; poolallocinst }  = { tsa' tenv(TEnv[getVarName(poolallocinst) <- (typ @ rho)]) ; nil } 
  if { tenv(TEnv') tsa' ; region(rho, typ) } := { tenv(TEnv) tsa ; getOp0(poolallocinst) } . 

  ---- For store operation
  var storeinst : StoreInst .
  var typ' : TypeOrLLVMValue .
  var rho' : TypeVar .
  ceq { tenv(TEnv) tsa ; storeinst } = { tenv(TEnv') tsa' ; nil }
    if { tenv(TEnv') tsa' ; (typ , typ @ rho') } := { tenv(TEnv) tsa ; (getOp0(storeinst), getOp1(storeinst)) }  .


  ---- For load operation
  var loadinst : LoadInst .
  ceq { tenv(TEnv) tsa ; loadinst } = { tenv(TEnv'[getVarName(loadinst) <- typ]) tsa' ; nil }
  if { tenv(TEnv') tsa' ; (typ @ rho) } := { tenv(TEnv) tsa ; getOp0(loadinst) } .
        
  ---- For the sequencing operation
  var inst : Instruction .
 var instl : InstructionList .
 ceq { tsa ; ( inst ; instl) } = { tsa' ; instl }
   if { tsa' ; nil } := { tsa ; inst } .
  
    
endfm 


fmod SIMPLE-PROGRAM is
extending LLVM-SYNTAX .
op pgm : -> Module .
op pgm2 : -> Module .
op F : -> Function . 
ops tests argc argv  x  y  main r : -> Name .
op rho : -> TypeVar .
op entry : -> label .
op regiontest : -> RegionBlockInsts .
op bbtest : -> BasicBlockLabelSet .
op bbtest2 : -> BasicBlock .
op inst1 : -> Instruction .
op inst2 : -> Instruction .

op typvar : -> FormalTypeVarList .
eq typvar = ( int x, int y) .

eq regiontest = (
poolinit(rho, int) r {
(entry :  
(x = add int 1, 4) ; 
(y = add int 1, x) ;
(z = poolalloc(r)) ;
(store int 3, int @ rho z) ;
(q = load int @ rho z)
)
}
) .

eq inst1 = (
(x = add int 1, 4) ;
(y = add int 2, 3) 
) . 
endfm


fmod SIMPLE-PROGRAM-SEMANTICS is
  including SIMPLE-PROGRAM .
  including LLVM-SYNTAX .
  including STATIC-TYPING-SEMANTICS .
endfm

--- LLVM Semantics
----red bbtest2 .
----red { mem(empty) env(empty) nextLoc(0)  ; bbtest2} .

---- Type Checking for SAFECode 
red inst1 .
red { tenv(empty) ; inst1 } .
red regiontest .
red { tenv(empty) ; regiontest } .