Skip to content

Commit

Permalink
Test array as parking spots and fix issues
Browse files Browse the repository at this point in the history
  • Loading branch information
@igormoreno
igormoreno committed Apr 5, 2024
1 parent ca0e99b commit 71aa48e
Show file tree
Hide file tree
Showing 5 changed files with 124 additions and 87 deletions.
96 changes: 48 additions & 48 deletions notional-machines/src/NotionalMachines/Lang/TypedLambdaArray/AbstractSyntax.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -417,50 +417,50 @@ evalM' t = evalStateT (evalM t) emptyStore
step' :: Term -> StateT (Store Location) (Either Error) Term
step' = \case
-- Lambdas
App t1 t2 | not (isValue t1) -> (\t1' -> App t1' t2 ) <$> rec t1 -- E-App1
App v1 t2 | not (isValue t2) -> (\t2' -> App v1 t2') <$> rec t2 -- E-App2
App (Lambda name _ t1) t2 -> return $ subst name t2 t1 -- E-AppAbs
App t1 t2 | not (isValue t1) -> (\t1' -> App t1' t2 ) <$> rec t1 -- E-App1
App v1 t2 | not (isValue t2) -> (\t2' -> App v1 t2') <$> rec t2 -- E-App2
App (Lambda name _ t1) t2 -> return $ subst name t2 t1 -- E-AppAbs
-- Sequence
Seq Unit t2 -> return t2 -- E-NextSeq
Seq t1 t2 -> (\t1' -> Seq t1' t2) <$> rec t1 -- E-Seq
Seq Unit t2 -> return t2 -- E-NextSeq
Seq t1 t2 -> (\t1' -> Seq t1' t2) <$> rec t1 -- E-Seq
-- References
Ref v | isValue v -> stateToStateT $ Loc <$> alloc v -- E-RefV
Ref t | otherwise -> Ref <$> rec t -- E-Ref
Deref (Loc l) -> deref l -- E-DerefLoc
Deref Null -> err "can't dereference null" -- E-DerefNull
Deref t -> Deref <$> rec t -- E-Deref
Assign (Loc l) v | isValue v -> assign l v -- E-RefAssign
Assign Null _ -> err "can't assign to null" -- E-AssignNull
Ref v | isValue v -> stateToStateT $ Loc <$> alloc v -- E-RefV
Ref t | otherwise -> Ref <$> rec t -- E-Ref
Deref (Loc l) -> deref l -- E-DerefLoc
Deref Null -> err "can't dereference null" -- E-DerefNull
Deref t -> Deref <$> rec t -- E-Deref
Assign (Loc l) v | isValue v -> assign l v -- E-RefAssign
Assign Null _ -> err "can't assign to null" -- E-AssignNull
-- Arrays
ArrayAlloc ty i | isValue i -> Loc <$> allocArray ty i -- E-ArrayAlloc1
ArrayAlloc ty t | otherwise -> ArrayAlloc ty <$> rec t -- E-ArrayAlloc2
ArrayAlloc ty i | isNumVal i -> Loc <$> allocArray ty i -- E-ArrayAlloc1
ArrayAlloc ty t | otherwise -> ArrayAlloc ty <$> rec t -- E-ArrayAlloc2
Assign (ArrayAccess (Loc l) i) v
| isValue i && isValue v -> assignArray l i v -- E-ArrayAssign1
| isNumVal i && isValue v -> assignArray l i v -- E-ArrayAssign1
Assign a@(ArrayAccess (Loc _) i) t
| isValue i && not (isValue t) -> Assign a <$> rec t -- E-ArrayAssign2
Assign (ArrayAccess Null _) _ -> err "can't dereference null" -- E-ArrayAssignNull
Assign t1 t2 | not (isValue t1) -> (\t1' -> Assign t1' t2 ) <$> rec t1 -- E-Assign1
Assign v1 t2 | otherwise -> (\t2' -> Assign v1 t2') <$> rec t2 -- E-Assign2
ArrayAccess (Loc l) i | isValue i -> derefArray l i -- E-ArrayAccess1
ArrayAccess Null _ -> err "can't dereference null" -- E-ArrayAccessNull
ArrayAccess t1 t2 | not (isValue t1) -> (\t1' -> ArrayAccess t1' t2) <$> rec t1 -- E-ArrayAccess2
ArrayAccess v1 t2 | otherwise -> (\t2' -> ArrayAccess v1 t2') <$> rec t2 -- E-ArrayAccess3
| isNumVal i && not (isValue t) -> Assign a <$> rec t -- E-ArrayAssign2
Assign (ArrayAccess Null _) _ -> err "can't dereference null" -- E-ArrayAssignNull
Assign t1 t2 | not (isValue t1) -> (\t1' -> Assign t1' t2 ) <$> rec t1 -- E-Assign1
Assign v1 t2 | otherwise -> (\t2' -> Assign v1 t2') <$> rec t2 -- E-Assign2
ArrayAccess (Loc l) i | isNumVal i -> derefArray l i -- E-ArrayAccess1
ArrayAccess Null _ -> err "can't dereference null" -- E-ArrayAccessNull
ArrayAccess t1 t2 | not (isValue t1) -> (\t1' -> ArrayAccess t1' t2) <$> rec t1 -- E-ArrayAccess2
ArrayAccess v1 t2 | otherwise -> (\t2' -> ArrayAccess v1 t2') <$> rec t2 -- E-ArrayAccess3
-- Compound data
Tuple ts -> Tuple <$> mapFirstM (not . isValue) rec ts -- E-Tuple
Proj i t@(Tuple vs) | isValue t -> proj i vs -- E-ProjTuple
Proj i t -> Proj i <$> rec t -- E-Proj
Tuple ts -> Tuple <$> mapFirstM (not . isValue) rec ts -- E-Tuple
Proj i t@(Tuple vs) | isValue t -> proj i vs -- E-ProjTuple
Proj i t -> Proj i <$> rec t -- E-Proj
-- Booleans + Arith
If Tru t2 _ -> return t2 -- E-IfTrue
If Fls _ t3 -> return t3 -- E-IfFalse
If t1 t2 t3 -> (\t1' -> If t1' t2 t3) <$> rec t1 -- E-If
Succ t -> Succ <$> rec t -- E-Succ
Pred Zero -> return Zero -- E-PredZero
Pred (Succ v) | isNumVal v -> return v -- E-PredSucc
Pred t -> Pred <$> rec t -- E-Pred
IsZero Zero -> return Tru -- E-IsZeroZero
IsZero (Succ v) | isNumVal v -> return Fls -- E-IsZeroSucc
IsZero t -> IsZero <$> rec t -- E-IsZero
t -> return t
If Tru t2 _ -> return t2 -- E-IfTrue
If Fls _ t3 -> return t3 -- E-IfFalse
If t1 t2 t3 -> (\t1' -> If t1' t2 t3) <$> rec t1 -- E-If
Succ t -> Succ <$> rec t -- E-Succ
Pred Zero -> return Zero -- E-PredZero
Pred (Succ v) | isNumVal v -> return v -- E-PredSucc
Pred t -> Pred <$> rec t -- E-Pred
IsZero Zero -> return Tru -- E-IsZeroZero
IsZero (Succ v) | isNumVal v -> return Fls -- E-IsZeroSucc
IsZero t -> IsZero <$> rec t -- E-IsZero
t -> return t
where rec = step'
err = lift . Left . RuntimeError

Expand Down Expand Up @@ -522,7 +522,7 @@ fresh a = "_" ++ a
peanoToDec :: Term -> Integer
peanoToDec Zero = 0
peanoToDec (Succ n) = succ (peanoToDec n)
peanoToDec t = error $ "internal error: can't show term as number: " ++ show t
peanoToDec t = error $ "internal error: can't make Integer out of: " ++ show t

instance Pretty Term where
pretty = \case
Expand Down Expand Up @@ -595,15 +595,15 @@ instance Pretty NameEnv where
----------------------
-- Other utilities

redex :: Term -> Term
redex :: Term -> Term
redex e = case e of
-- Lambdas
App t1 _ | not (isValue t1) -> rec t1
App _ t2 | not (isValue t2) -> rec t2
App (Lambda _ _ _) _ -> e
App (Lambda _ _ _) _ -> e
-- Sequence
Seq Unit _ -> e
Seq t1 _ -> rec t1
Seq Unit _ -> e
Seq t1 _ -> rec t1
-- References
Ref v | isValue v -> e
Ref t | otherwise -> rec t
Expand All @@ -613,8 +613,8 @@ redex e = case e of
Assign (Loc _) v | isValue v -> e
Assign Null _ -> e -- err "can't assign to null"
-- Arrays
ArrayAlloc _ i | isValue i -> e
ArrayAlloc _ t | otherwise -> rec t
ArrayAlloc _ i | isValue i -> e
ArrayAlloc _ t | otherwise -> rec t
Assign (ArrayAccess (Loc _) i) v
| isValue i && isValue v -> e
Assign (ArrayAccess (Loc _) i) t
Expand All @@ -629,12 +629,12 @@ redex e = case e of
-- Compound data
Tuple ts | all isValue ts -> e
Tuple ts | otherwise -> rec (head (filter (not . isValue) ts))
Proj _ t@(Tuple _) | isValue t -> e
Proj _ t@(Tuple _) | isValue t -> e
Proj _ t -> rec t
-- Booleans + Arith
If Tru _ _ -> e
If Fls _ _ -> e
If t1 _ _ -> rec t1
If Tru _ _ -> e
If Fls _ _ -> e
If t1 _ _ -> rec t1
Succ t -> rec t
Pred Zero -> e
Pred (Succ v) | isNumVal v -> e
Expand Down
4 changes: 2 additions & 2 deletions notional-machines/src/NotionalMachines/Lang/TypedLambdaArray/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ module NotionalMachines.Lang.TypedLambdaArray.Main (
traceAlaRacket) where

import Control.Monad ((<=<))
import Control.Monad.State.Lazy (StateT, evalStateT, runStateT)
import Control.Monad.State.Lazy (StateT, runStateT)

import Prettyprinter (Pretty (pretty), align, line, list, vsep)

Expand All @@ -54,7 +54,7 @@ import NotionalMachines.Util.REPL (LangPipeline (LangPi
-------------------
-- REPL
--------------------
newtype Trace s = Trace [s]
newtype Trace s = Trace { rawTrace :: [s] }
instance Pretty s => Pretty (Trace s) where
pretty (Trace ss) = list (map (align . (<>) line . pretty) ss)

Expand Down
53 changes: 24 additions & 29 deletions notional-machines/src/NotionalMachines/LangInMachine/TypedLambdaArrayParkingSpaces.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,17 @@
module NotionalMachines.LangInMachine.TypedLambdaArrayParkingSpaces where

import Data.Bifunctor (bimap)
import Control.Monad.State.Lazy (lift, StateT, get, modify, runStateT, evalStateT)
import Control.Monad ((<=<))
import Control.Monad.State.Lazy (evalStateT)

import Prettyprinter (pretty)


import qualified NotionalMachines.Machine.ArrayAsParkingSpaces.Main as NM
import qualified NotionalMachines.Lang.TypedLambdaArray.AbstractSyntax as Lang
import NotionalMachines.Lang.TypedLambdaArray.Main

import NotionalMachines.Meta.Bisimulation (Bisimulation (..))
import NotionalMachines.Meta.Steppable (traceM, evalM)
import NotionalMachines.Lang.Error (Error (..))


Expand All @@ -33,17 +34,11 @@ tyLangToNM = \case Lang.TyFun _ _ -> NM.TyOtherPrim
Lang.TyTuple _ -> NM.TyOtherPrim



alpha_A :: (Lang.Term, Lang.Store Lang.Location) -> NM.Term
alpha_A (e, s) =
-- alpha_A :: StateT (Lang.Store Lang.Location) (Either Error) Lang.Term -> NM.Term
-- alpha_A t = case runStateT t Lang.emptyStore of
-- Left er -> error "can't get started: " ++ show (pretty er)
-- Right (e, s) ->
langToNM :: (Lang.Term, Lang.Store Lang.Location) -> NM.Term
langToNM (e, s) =
case Lang.redex e of
Lang.ArrayAlloc ty l | Lang.isValue l ->
let id = Lang.nextLocation s
in NM.ArrayAlloc (tyLangToNM ty) (fromIntegral (Lang.peanoToDec l)) (show id)
NM.ArrayAlloc (tyLangToNM ty) (fromIntegral (Lang.peanoToDec l)) (show (Lang.nextLocation s))
Lang.ArrayAccess (Lang.Loc l) i | Lang.isValue i ->
NM.ArrayAccess (NM.Loc l) (fromIntegral (Lang.peanoToDec i))
Lang.ArrayAccess Lang.Null i | Lang.isValue i ->
Expand All @@ -52,46 +47,46 @@ alpha_A (e, s) =
NM.ArrayWrite (NM.Loc l) (fromIntegral (Lang.peanoToDec i)) (rec v)
Lang.Assign (Lang.ArrayAccess Lang.Null i) v | Lang.isValue v ->
NM.ArrayWrite NM.Null (fromIntegral (Lang.peanoToDec i)) (rec v)
-- Values
-- Location
Lang.Loc l -> NM.Loc l
-- Numbers
Lang.Zero -> NM.PrimValue "0"
n@(Lang.Succ e') | Lang.isValue e' -> NM.PrimValue . show . Lang.peanoToDec $ n
-- Booleans
Lang.Tru -> NM.PrimValue "true"
Lang.Fls -> NM.PrimValue "false"
-- Unit
Lang.Unit -> NM.Unit
-- Null
Lang.Null -> NM.Null
-- Arrays can't contain values of other types
_ -> NM.Other
where rec t = alpha_A (t, s)
where rec t = langToNM (t, s)

alpha_A_trace :: Lang.Term -> Either NM.Problem [NM.Term]
alpha_A_trace = bimap convertIssue (map alpha_A) . trace
where trace :: Lang.Term -> Either Error [(Lang.Term, Lang.Store Lang.Location)]
trace = mapM (`runStateT` Lang.emptyStore) . traceM

convertIssue :: Error -> NM.Problem
convertIssue = NM.Problem . show . pretty

alpha_B_step :: StateT (Lang.Store Lang.Location) (Either Error) Lang.Term -> StateT NM.ParkingSpace (Either NM.Problem) NM.Term
alpha_B_step e = case evalStateT e Lang.emptyStore of
Left er -> lift . Left . convertIssue $ er
Right t -> return $ alpha_A (t, Lang.emptyStore)
--Right (t, _) -> return $ alpha_A (return t)

alpha_B_eval :: Either Error Lang.Term -> Either NM.Problem NM.Term
alpha_B_eval = bimap convertIssue (alpha_A . (, Lang.emptyStore))


convertIssue :: Error -> NM.Problem
convertIssue = NM.Problem . show . pretty

alpha_A :: Lang.Term -> Either NM.Problem [NM.Term]
alpha_A = bimap convertIssue (map langToNM . rawTrace) . trace' Lang.emptyStore id

alpha_B :: Either Error Lang.Term -> Either NM.Problem NM.Term
alpha_B = bimap convertIssue (langToNM . (, Lang.emptyStore))


bisimEval :: Bisimulation Lang.Term
(Either Error Lang.Term)
(Either NM.Problem [NM.Term])
(Either NM.Problem NM.Term)
bisimEval = MkBisim { fLang = Lang.evalM'
bisimEval = MkBisim { fLang = Lang.evalM' . fst <=< Lang.typecheck
, fNM = f_NM
, alphaA = alpha_A_trace
, alphaB = alpha_B_eval
, alphaA = alpha_A
, alphaB = alpha_B
}
where f_NM :: Either NM.Problem [NM.Term] -> Either NM.Problem NM.Term
f_NM t = t >>= ((`evalStateT` NM.emptyParkingSpace) . NM.fNM_Replay)

16 changes: 10 additions & 6 deletions notional-machines/src/NotionalMachines/Machine/ArrayAsParkingSpaces/Main.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,6 @@ import qualified Data.Map as Map

import Control.Monad.State.Lazy (StateT, get, modify, lift)

import NotionalMachines.Util.Util (nextKey)


---- Sublanguage needed for the parking space nm

Expand Down Expand Up @@ -44,7 +42,7 @@ isValue = \case
-------------------------------

data Problem = Problem String
deriving (Show)
deriving (Eq, Show)

type ParkingSpace = Map Address [Spot]
type Address = Location
Expand All @@ -55,6 +53,7 @@ newtype Car = Car Term
emptyParkingSpace :: ParkingSpace
emptyParkingSpace = Map.empty

problem :: String -> StateT ParkingSpace (Either Problem) a
problem = lift . Left . Problem

----- Parking space manipulation -----
Expand Down Expand Up @@ -83,9 +82,9 @@ getSpot :: Location -> Int -> StateT ParkingSpace (Either Problem) Term
getSpot loc i = do
ps <- get
case Map.lookup loc ps of
Nothing -> problem "no such location"
Nothing -> problem $ "no such location: " ++ show loc
Just spots -> case spots !! i of
Nothing -> problem "no such spot"
Nothing -> return Null
Just (Car v) -> return v

-- assign
Expand All @@ -106,8 +105,13 @@ fNM t = case t of
-- "no such location" is good
ArrayAccess (Loc loc) i -> getSpot loc i
ArrayAccess Null _ -> problem "null dereference"
-- Values
Loc _ -> return t
Unit -> return t
Null -> return t
PrimValue _ -> return t
_ -> return Other


fNM_Replay :: [Term] -> StateT ParkingSpace (Either Problem) Term
fNM_Replay [] = problem "no replay"
fNM_Replay = foldl (\s t -> s >>= const (fNM t)) (return Unit)
Loading

0 comments on commit 71aa48e

Please sign in to comment.