-- This implements memories on top of finite maps

--#include "FiniteMaps2.alfa"

--#include "Alfa/Natural.alfa"

package Memories
  (FM::Set -> Set)(fm::FiniteMaps.FiniteMap FM Natural.Nat)(Word::Set)
 where
  open Natural
   use  Nat,  (+),  (*),  isZero,  natRec,  natEq,  max,  (-),  natLte,
        natLt,  natGt
  open Identity  use  (==)
  open Propositions  use  Absurdity
  open Types  use  List,  Pair
  Addr = Nat
  nullPtr :: Addr
    = Zero@_
  abstract Memory :: Set
    = data M (free::Addr) (fm::FM Word)
  Data = List Word
  abstract empty (init::Word) :: Memory
    = M@_ nullPtr (fm.empty Word init)
  abstract lookupM (m::Memory)(a::Addr) :: Word
    = case m of { (M free fm') -> fm.lookup Word fm' a;}
  abstract updateM (a::Addr)(w::Word)(m::Memory) :: Memory
    = case m of { (M free fm') -> M@_ free (fm.update Word a w fm');}
  Range :: Set
    = sig{base :: Addr;
          size :: Nat;}
  -- Initial dummy implementation of allocation and deallocation:
  abstract malloc (n::Nat)(m::Memory) :: Pair Range Memory
    = Pair@_
        (struct {
           base = nullPtr;
           size = n;})
        m
  abstract free (r::Range)(m::Memory) :: Memory
    = m
  abstract updatePropM (a::Addr)
                       (a'::Addr)
                       (w::Word)
                       (m1::Memory)
                       (m2::Memory)
                       (p::(==) Word (lookupM m1 a) (lookupM m2 a))
             :: (==)
                  Word
                  (lookupM (updateM a' w m1) a)
                  (lookupM (updateM a' w m2) a)
    = case m1 of {
        (M free1 fm1) ->
          case m2 of { (M free2 fm2) -> fm.updateProp Word a a' w fm1 fm2 p;};}
  abstract updateSameM (a::Addr)(w::Word)(m::Memory)
             :: (==) Word (lookupM (updateM a w m) a) w
    = case m of { (M free fm') -> fm.updateSame Word a w fm';}
  abstract updateOtherM (a::Addr)
                        (a'::Addr)
                        (w::Word)
                        (m::Memory)
                        (p::(==) Addr a a' -> Absurdity)
             :: (==) Word (lookupM (updateM a' w m) a) (lookupM m a)
    = case m of { (M free fm') -> fm.updateOther Word a a' w fm' p;}
  storeList (a::Addr)(ws::Data)(m::Memory) :: Memory
    = case ws of {
        (Nil) -> m;
        (Cons x xs) -> updateM a x (storeList (Succ@_ a) xs m);}
  loadList (a::Addr)(n::Nat)(m::Memory) :: Data
    = case n of {
        (Zero) -> Nil@_;
        (Succ n') -> Cons@_ (lookupM m a) (loadList (Succ@_ a) n' m);}
  loadRange (r::Range)(m::Memory) :: Data
    = loadList r.base r.size m
{-# Alfa unfoldgoals off
brief on
hidetypeannots off
wide

nd
hiding on
 #-}