Commit e8a484bf authored by Belpaire's avatar Belpaire
Browse files

Signed-off-by: Belpaire <belpairebram@hotmail.com>

parent c43ab4bc
......@@ -893,35 +893,35 @@ valueshiftminus d t =
Z
t
coercionSubstituteHelp sub c (CoercionVar hnat)
| hnat == c = coercionshiftplus c sub
coercionSubstituteHelp sub orig c (CoercionVar hnat)
| hnat == plus orig c = coercionshiftplus c sub
| otherwise = CoercionVar hnat
dirtSubstituteHelp sub c (DirtVariable hnat)
| hnat == c = dirtshiftplus c sub
dirtSubstituteHelp sub orig c (DirtVariable hnat)
| hnat == plus orig c = dirtshiftplus c sub
| otherwise = DirtVariable hnat
skeletonTypeSubstituteHelp sub c (SkelVar hnat)
| hnat == c = skeletonTypeshiftplus c sub
skeletonTypeSubstituteHelp sub orig c (SkelVar hnat)
| hnat == plus orig c = skeletonTypeshiftplus c sub
| otherwise = SkelVar hnat
valueTypeSubstituteHelp sub c (ValTyVar hnat)
| hnat == c = valueTypeshiftplus c sub
valueTypeSubstituteHelp sub orig c (ValTyVar hnat)
| hnat == plus orig c = valueTypeshiftplus c sub
| otherwise = ValTyVar hnat
valueSubstituteHelp sub c (TmVar hnat)
| hnat == c = valueshiftplus c sub
valueSubstituteHelp sub orig c (TmVar hnat)
| hnat == plus orig c = valueshiftplus c sub
| otherwise = TmVar hnat
coercioncoercionSubstitute :: Coercion -> HNat -> Coercion -> Coercion
coercioncoercionSubstitute sub orig t =
rewriteCoercion $
coercionmap
(coercionSubstituteHelp sub)
(coercionSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
coercionvalueTypeSubstitute :: ValueType -> HNat -> Coercion -> Coercion
......@@ -929,10 +929,10 @@ coercionvalueTypeSubstitute sub orig t =
rewriteCoercion $
coercionmap
(\c x -> x)
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
coercionskeletonTypeSubstitute :: SkeletonType -> HNat -> Coercion -> Coercion
......@@ -941,9 +941,9 @@ coercionskeletonTypeSubstitute sub orig t =
coercionmap
(\c x -> x)
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
coerciondirtSubstitute :: Dirt -> HNat -> Coercion -> Coercion
......@@ -953,18 +953,18 @@ coerciondirtSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(dirtSubstituteHelp sub)
orig
(dirtSubstituteHelp sub orig)
Z
t
computationTypevalueTypeSubstitute ::
ValueType -> HNat -> ComputationType -> ComputationType
computationTypevalueTypeSubstitute sub orig t =
computationTypemap
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
computationTypeskeletonTypeSubstitute ::
......@@ -972,32 +972,32 @@ computationTypeskeletonTypeSubstitute ::
computationTypeskeletonTypeSubstitute sub orig t =
computationTypemap
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
computationTypedirtSubstitute ::
Dirt -> HNat -> ComputationType -> ComputationType
computationTypedirtSubstitute sub orig t =
computationTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub) orig t
computationTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub orig) Z t
dirtdirtSubstitute :: Dirt -> HNat -> Dirt -> Dirt
dirtdirtSubstitute sub orig t = dirtmap (dirtSubstituteHelp sub) orig t
dirtdirtSubstitute sub orig t = dirtmap (dirtSubstituteHelp sub orig) Z t
skeletonTypeskeletonTypeSubstitute ::
SkeletonType -> HNat -> SkeletonType -> SkeletonType
skeletonTypeskeletonTypeSubstitute sub orig t =
skeletonTypemap (skeletonTypeSubstituteHelp sub) orig t
skeletonTypemap (skeletonTypeSubstituteHelp sub orig) Z t
simpleCoercionTypevalueTypeSubstitute ::
ValueType -> HNat -> SimpleCoercionType -> SimpleCoercionType
simpleCoercionTypevalueTypeSubstitute sub orig t =
simpleCoercionTypemap
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
simpleCoercionTypeskeletonTypeSubstitute ::
......@@ -1005,57 +1005,62 @@ simpleCoercionTypeskeletonTypeSubstitute ::
simpleCoercionTypeskeletonTypeSubstitute sub orig t =
simpleCoercionTypemap
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
simpleCoercionTypedirtSubstitute ::
Dirt -> HNat -> SimpleCoercionType -> SimpleCoercionType
simpleCoercionTypedirtSubstitute sub orig t =
simpleCoercionTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub) orig t
simpleCoercionTypemap
(\c x -> x)
(\c x -> x)
(dirtSubstituteHelp sub orig)
Z
t
coercionTypevalueTypeSubstitute ::
ValueType -> HNat -> CoercionType -> CoercionType
coercionTypevalueTypeSubstitute sub orig t =
coercionTypemap (valueTypeSubstituteHelp sub) (\c x -> x) (\c x -> x) orig t
coercionTypemap (valueTypeSubstituteHelp sub orig) (\c x -> x) (\c x -> x) Z t
coercionTypeskeletonTypeSubstitute ::
SkeletonType -> HNat -> CoercionType -> CoercionType
coercionTypeskeletonTypeSubstitute sub orig t =
coercionTypemap
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
coercionTypedirtSubstitute :: Dirt -> HNat -> CoercionType -> CoercionType
coercionTypedirtSubstitute sub orig t =
coercionTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub) orig t
coercionTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub orig) Z t
valueTypevalueTypeSubstitute :: ValueType -> HNat -> ValueType -> ValueType
valueTypevalueTypeSubstitute sub orig t =
valueTypemap (valueTypeSubstituteHelp sub) (\c x -> x) (\c x -> x) orig t
valueTypemap (valueTypeSubstituteHelp sub orig) (\c x -> x) (\c x -> x) Z t
valueTypeskeletonTypeSubstitute ::
SkeletonType -> HNat -> ValueType -> ValueType
valueTypeskeletonTypeSubstitute sub orig t =
valueTypemap (\c x -> x) (skeletonTypeSubstituteHelp sub) (\c x -> x) orig t
valueTypemap (\c x -> x) (skeletonTypeSubstituteHelp sub orig) (\c x -> x) Z t
valueTypedirtSubstitute :: Dirt -> HNat -> ValueType -> ValueType
valueTypedirtSubstitute sub orig t =
valueTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub) orig t
valueTypemap (\c x -> x) (\c x -> x) (dirtSubstituteHelp sub orig) Z t
computationvalueSubstitute :: Value -> HNat -> Computation -> Computation
computationvalueSubstitute sub orig t =
computationmap
(valueSubstituteHelp sub)
(valueSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
computationvalueTypeSubstitute ::
......@@ -1063,11 +1068,11 @@ computationvalueTypeSubstitute ::
computationvalueTypeSubstitute sub orig t =
computationmap
(\c x -> x)
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
computationskeletonTypeSubstitute ::
......@@ -1076,10 +1081,10 @@ computationskeletonTypeSubstitute sub orig t =
computationmap
(\c x -> x)
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
computationdirtSubstitute :: Dirt -> HNat -> Computation -> Computation
......@@ -1088,9 +1093,9 @@ computationdirtSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(dirtSubstituteHelp sub)
(dirtSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
computationcoercionSubstitute :: Coercion -> HNat -> Computation -> Computation
......@@ -1100,30 +1105,30 @@ computationcoercionSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(coercionSubstituteHelp sub)
orig
(coercionSubstituteHelp sub orig)
Z
t
handlervalueSubstitute :: Value -> HNat -> Handler -> Handler
handlervalueSubstitute sub orig t =
handlermap
(valueSubstituteHelp sub)
(valueSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
handlervalueTypeSubstitute :: ValueType -> HNat -> Handler -> Handler
handlervalueTypeSubstitute sub orig t =
handlermap
(\c x -> x)
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
handlerskeletonTypeSubstitute :: SkeletonType -> HNat -> Handler -> Handler
......@@ -1131,10 +1136,10 @@ handlerskeletonTypeSubstitute sub orig t =
handlermap
(\c x -> x)
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
handlerdirtSubstitute :: Dirt -> HNat -> Handler -> Handler
......@@ -1143,9 +1148,9 @@ handlerdirtSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(dirtSubstituteHelp sub)
(dirtSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
handlercoercionSubstitute :: Coercion -> HNat -> Handler -> Handler
......@@ -1155,20 +1160,20 @@ handlercoercionSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(coercionSubstituteHelp sub)
orig
(coercionSubstituteHelp sub orig)
Z
t
operationCompTuplevalueSubstitute ::
Value -> HNat -> OperationCompTuple -> OperationCompTuple
operationCompTuplevalueSubstitute sub orig t =
operationCompTuplemap
(valueSubstituteHelp sub)
(valueSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
operationCompTuplevalueTypeSubstitute ::
......@@ -1176,11 +1181,11 @@ operationCompTuplevalueTypeSubstitute ::
operationCompTuplevalueTypeSubstitute sub orig t =
operationCompTuplemap
(\c x -> x)
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
operationCompTupleskeletonTypeSubstitute ::
......@@ -1189,10 +1194,10 @@ operationCompTupleskeletonTypeSubstitute sub orig t =
operationCompTuplemap
(\c x -> x)
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
operationCompTupledirtSubstitute ::
......@@ -1202,9 +1207,9 @@ operationCompTupledirtSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(dirtSubstituteHelp sub)
(dirtSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
operationCompTuplecoercionSubstitute ::
......@@ -1215,30 +1220,30 @@ operationCompTuplecoercionSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(coercionSubstituteHelp sub)
orig
(coercionSubstituteHelp sub orig)
Z
t
valuevalueSubstitute :: Value -> HNat -> Value -> Value
valuevalueSubstitute sub orig t =
valuemap
(valueSubstituteHelp sub)
(valueSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
valuevalueTypeSubstitute :: ValueType -> HNat -> Value -> Value
valuevalueTypeSubstitute sub orig t =
valuemap
(\c x -> x)
(valueTypeSubstituteHelp sub)
(valueTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
(\c x -> x)
orig
Z
t
valueskeletonTypeSubstitute :: SkeletonType -> HNat -> Value -> Value
......@@ -1246,10 +1251,10 @@ valueskeletonTypeSubstitute sub orig t =
valuemap
(\c x -> x)
(\c x -> x)
(skeletonTypeSubstituteHelp sub)
(skeletonTypeSubstituteHelp sub orig)
(\c x -> x)
(\c x -> x)
orig
Z
t
valuedirtSubstitute :: Dirt -> HNat -> Value -> Value
......@@ -1258,9 +1263,9 @@ valuedirtSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(dirtSubstituteHelp sub)
(dirtSubstituteHelp sub orig)
(\c x -> x)
orig
Z
t
valuecoercionSubstitute :: Coercion -> HNat -> Value -> Value
......@@ -1270,8 +1275,8 @@ valuecoercionSubstitute sub orig t =
(\c x -> x)
(\c x -> x)
(\c x -> x)
(coercionSubstituteHelp sub)
orig
(coercionSubstituteHelp sub orig)
Z
t
freeVariablesCoercion :: HNat -> Coercion -> [HNat]
......
......@@ -193,27 +193,28 @@ typeshiftminus d t = typemap (typeshiftHelpminus d) Z t
termshiftminus :: HNat -> Term -> Term
termshiftminus d t = termmap (termshiftHelpminus d) (typeshiftHelpminus d) Z t
typeSubstituteHelp sub c (TyVar hnat)
| hnat == c = typeshiftplus c sub
typeSubstituteHelp sub orig c (TyVar hnat)
| hnat == plus orig c = typeshiftplus c sub
| otherwise = TyVar hnat
termSubstituteHelp sub c (TmVar hnat)
| hnat == c = termshiftplus c sub
termSubstituteHelp sub orig c (TmVar hnat)
| hnat == plus orig c = termshiftplus c sub
| otherwise = TmVar hnat
coerciontypeSubstitute :: Type -> HNat -> Coercion -> Coercion
coerciontypeSubstitute sub orig t = coercionmap (typeSubstituteHelp sub) orig t
coerciontypeSubstitute sub orig t =
coercionmap (typeSubstituteHelp sub orig) Z t
typetypeSubstitute :: Type -> HNat -> Type -> Type
typetypeSubstitute sub orig t = typemap (typeSubstituteHelp sub) orig t
typetypeSubstitute sub orig t = typemap (typeSubstituteHelp sub orig) Z t
termtermSubstitute :: Term -> HNat -> Term -> Term
termtermSubstitute sub orig t =
termmap (termSubstituteHelp sub) (\c x -> x) orig t
termmap (termSubstituteHelp sub orig) (\c x -> x) Z t
termtypeSubstitute :: Type -> HNat -> Term -> Term
termtypeSubstitute sub orig t =
termmap (\c x -> x) (typeSubstituteHelp sub) orig t
termmap (\c x -> x) (typeSubstituteHelp sub orig) Z t
freeVariablesCoercion :: HNat -> Coercion -> [HNat]
freeVariablesCoercion c (CoId) = nub ([])
......
......@@ -177,24 +177,25 @@ fiTermshiftminus :: HNat -> FiTerm -> FiTerm
fiTermshiftminus d t =
fiTermmap (fiTermshiftHelpminus d) (fiTypeshiftHelpminus d) Z t
fiTypeSubstituteHelp sub c (TyVar hnat)
| hnat == c = fiTypeshiftplus c sub
fiTypeSubstituteHelp sub orig c (TyVar hnat)
| hnat == plus orig c = fiTypeshiftplus c sub
| otherwise = TyVar hnat
fiTermSubstituteHelp sub c (TmVar hnat)
| hnat == c = fiTermshiftplus c sub
fiTermSubstituteHelp sub orig c (TmVar hnat)
| hnat == plus orig c = fiTermshiftplus c sub
| otherwise = TmVar hnat
fiTypefiTypeSubstitute :: FiType -> HNat -> FiType -> FiType
fiTypefiTypeSubstitute sub orig t = fiTypemap (fiTypeSubstituteHelp sub) orig t
fiTypefiTypeSubstitute sub orig t =
fiTypemap (fiTypeSubstituteHelp sub orig) Z t
fiTermfiTermSubstitute :: FiTerm -> HNat -> FiTerm -> FiTerm
fiTermfiTermSubstitute sub orig t =
fiTermmap (fiTermSubstituteHelp sub) (\c x -> x) orig t
fiTermmap (fiTermSubstituteHelp sub orig) (\c x -> x) Z t
fiTermfiTypeSubstitute :: FiType -> HNat -> FiTerm -> FiTerm
fiTermfiTypeSubstitute sub orig t =
fiTermmap (\c x -> x) (fiTypeSubstituteHelp sub) orig t
fiTermmap (\c x -> x) (fiTypeSubstituteHelp sub orig) Z t
freeVariablesFiType :: HNat -> FiType -> [HNat]
freeVariablesFiType c (TyTop) = nub ([])
......
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
module SEDEL.Target.Eval
( evaluate
) where
import Control.Monad.Except
import Data.IORef
import qualified Data.Map.Strict as M
import Unbound.Generics.LocallyNameless
import SEDEL.Common
import SEDEL.Target.Syntax
-- call-by-need environment
type Env = M.Map UName Thunk
type EvalM a = FreshMT (ExceptT String IO) a
newtype Thunk = Thunk
{ force :: EvalM Value
}
instance Show Thunk where
show _ = "<Thunk>"
mkThunk :: EvalM Value -> EvalM Thunk
mkThunk ev = do
ref <- liftIO $ newIORef Nothing
return $
Thunk $ do
mv <- liftIO $ readIORef ref
case mv of
Nothing -> do
v <- ev
liftIO $ writeIORef ref (Just v)
return v
Just v -> return v
data Value
= VLit !Double
| VBool !Bool
| VStr !String
| VPair !Thunk
!Thunk
| VUnit
| VLam !(Thunk -> EvalM Value)
instance Show Value where
show (VLit n) = show n
show (VBool True) = "true"
show (VBool False) = "false"
show (VPair _ _) = "<Pair>"
show VUnit = "()"
show (VStr s) = show s
show (VLam _) = "<Lambda>"
runEvalM :: EvalM a -> IO (Either String a)
runEvalM = runExceptT . runFreshMT
evaluate :: UExpr -> IO (Either String Value)
evaluate e = runEvalM (eval M.empty e)
-- | Lazy evaluation
eval :: Env -> UExpr -> EvalM Value
eval env (UVar n) = lookupValue env n >>= force
eval env (UApp f x) = do
f' <- eval env f
x' <- mkThunk (eval env x)
evalApp f' x'
eval env (ULam b) = do
(n, e) <- unbind b
return $ VLam $ \x -> eval (M.insert n x env) e
eval env (ULet b) =
mdo (n, (e1, e2)) <- unbind b
e1' <- mkThunk (eval (M.insert n e1' env) e1)
eval (M.insert n e1' env) e2
eval env (UPair e1 e2) = do
e1' <- mkThunk (eval env e1)
e2' <- mkThunk (eval env e2)
return $ VPair e1' e2'
eval env (UP1 e) = do
e' <- eval env e
evalP1 e'
eval env (UP2 e) = do
e' <- eval env e
evalP2 e'
eval _ (ULitV n) = return (VLit n)
eval _ (UBoolV n) = return (VBool n)
eval _ (UStrV n) = return (VStr n)
eval _ UUnit = return VUnit
eval env (UPrimOp op e1 e2) = do
e1' <- eval env e1
e2' <- eval env e2
evalOp op e1' e2'
eval env (UIf e1 e2 e3) = do
e1' <- eval env e1