Skip to content

GitLab

I
iTypes
Commit 1aeae616 authored by André Pacak's avatar André Pacak
Browse files
Options

renamed packages to have a consistent strucutre and removed records

parent efabcfbd
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 205 additions and 1135 deletions
inca-translation/.mps/workspace.xml
View file @ 1aeae616
This diff is collapsed.
inca-translation/languages/NewLanguage/models/editor.mps
View file @ 1aeae616
......@@ -19,12 +19,16 @@
</concept>
<concept id="1106270571710" name="jetbrains.mps.lang.editor.structure.CellLayout_Vertical" flags="nn" index="2iRkQZ" />
<concept id="1237303669825" name="jetbrains.mps.lang.editor.structure.CellLayout_Indent" flags="nn" index="l2Vlx" />
<concept id="1237307900041" name="jetbrains.mps.lang.editor.structure.IndentLayoutIndentStyleClassItem" flags="ln" index="lj46D" />
<concept id="1080736578640" name="jetbrains.mps.lang.editor.structure.BaseEditorComponent" flags="ig" index="2wURMF">
<child id="1080736633877" name="cellModel" index="2wV5jI" />
</concept>
<concept id="1078939183254" name="jetbrains.mps.lang.editor.structure.CellModel_Component" flags="sg" stub="3162947552742194261" index="PMmxH">
<reference id="1078939183255" name="editorComponent" index="PMmxG" />
</concept>
<concept id="1186414536763" name="jetbrains.mps.lang.editor.structure.BooleanStyleSheetItem" flags="ln" index="VOi$J">
<property id="1186414551515" name="flag" index="VOm3f" />
</concept>
<concept id="1186414928363" name="jetbrains.mps.lang.editor.structure.SelectableStyleSheetItem" flags="ln" index="VPM3Z" />
<concept id="1630016958697344083" name="jetbrains.mps.lang.editor.structure.IMenu_Concept" flags="ng" index="2ZABuq">
<reference id="6591946374543067572" name="conceptDeclaration" index="aqKnT" />
......@@ -273,6 +277,9 @@
<node concept="3XFhqQ" id="6m6bBlJmbTP" role="3EZMnx" />
<node concept="3F0A7n" id="6m6bBlJmbU8" role="3EZMnx">
<ref role="1NtTu8" to="xkot:6m6bBlJafKa" resolve="name1" />
<node concept="lj46D" id="6m6bBlJno_$" role="3F10Kt">
<property role="VOm3f" value="true" />
</node>
</node>
<node concept="3F0ifn" id="6m6bBlJmbUm" role="3EZMnx">
<property role="3F0ifm" value="-&gt;" />
......
src/ExtendedTLC/PartialOrd.hs deleted 100644 → 0
View file @ efabcfbd
module ExtendedTLC.PartialOrd where
import Prelude hiding (Ord, (<=))
import ExtendedTLC.Language(Type(..))
import Util.PartialOrd as PO
-- structural ordering
-- ordering of functions is not contravariant
-- instance PO.PartialOrd Type where
-- _ <= AnyType = True
-- (Fun t1 t2) <= (Fun u1 u2) = t1 <= u1 && t2 <= u2
-- (Prod t1 t2) <= (Prod u1 u2) = t1 <= u1 && t2 <= u2
-- (Record pairs) <= (Record pairs') = all (\((x, ty), (x', ty')) -> if x == x' then ty <= ty' else False) zipped
-- where zipped = zip pairs pairs'
--
-- (Sum t1 t2) <= (Sum u1 u2) = t1 <= u1 && t2 <= u2
-- ty1 <= ty2 = ty1 == ty2
src/ExtendedTLC/Base.hs → src/SumTypes/Base.hs
View file @ 1aeae616
module ExtendedTLC.Base where
module SumTypes.Base where
import Prelude hiding ((>=), (<=), lookup)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map (lookup)
import ExtendedTLC.Language
import SumTypes.Language
import Util.ErrorMessages
type Error = String
......@@ -50,19 +48,10 @@ matchType ty1 ty2 _
| ty1 == ty2 = return ()
matchType ty1 ty2 err = fail $ generalError (show ty1) ty2 err
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail $ recordError ty err
matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail $ sumError ty err
liftMaybe :: Monad m => Maybe a -> String -> m a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail err
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail $ "Unbound variable " ++ show x
lookup (Bind c x t) y
......@@ -102,10 +91,6 @@ inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
......@@ -116,17 +101,6 @@ checkType ctx p@(Pair t1 t2 _) ty = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1 ty1
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t lty
) tpairs
foldl (>>) (return ()) subresults
else
fail "Length of term labels and type labels does not match"
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
src/ExtendedTLC/ContinueAfterCheckFail.hs → src/SumTypes/ContinueAfterCheckFail.hs
View file @ 1aeae616
......@@ -2,15 +2,12 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RebindableSyntax #-}
module ExtendedTLC.ContinueAfterCheckFail where
module SumTypes.ContinueAfterCheckFail where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map
import ExtendedTLC.Language
import SumTypes.Language
import Util.ErrorMessages
import Util.PartialOrd
......@@ -45,11 +42,6 @@ instance WithTop () where
instance (WithTop a, WithTop b) => WithTop (a, b) where
top = (top, top)
instance WithTop a => WithTop [a] where
top = [top]
instance WithTop a => WithTop (Map Name a) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
......@@ -93,19 +85,10 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = return ()
matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail [recordError ty err]
matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail [sumError ty err]
liftMaybe :: WithTop a => Maybe a -> String -> Infer a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail [err]
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail ["Unbound variable " ++ show x]
lookup (Bind c x t) y | x == y = return t
......@@ -144,10 +127,6 @@ inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail ["Cannot infer type of term " ++ show t]
checkType :: Ctx -> Term -> Type -> Check
......@@ -158,17 +137,6 @@ checkType ctx p@(Pair t1 t2 _) ty = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1 ty1
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t lty
) tpairs
foldl (>>) (return ()) subresults
else
fail ["Length of term labels and type labels does not match"]
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
src/ExtendedTLC/EliminateContextArgument.hs → src/SumTypes/EliminateContextArgument.hs
View file @ 1aeae616
......@@ -2,16 +2,12 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RebindableSyntax #-}
module ExtendedTLC.EliminateContextArgument where
module SumTypes.EliminateContextArgument where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (isJust, fromJust)
import ExtendedTLC.Language
import SumTypes.Language
import Util.ErrorMessages
import Util.PartialOrd
......@@ -46,14 +42,6 @@ instance WithTop () where
instance (WithTop a, WithTop b) => WithTop (a, b) where
top = (top, top)
instance WithTop Ctx where
top = Empty
instance WithTop a => WithTop [a] where
top = [top]
instance WithTop a => WithTop (Map Name a) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
......@@ -97,19 +85,10 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = Inferred ()
matchType ty1 ty2 err = NotInferred [generalError (show ty1) ty2 err]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail [recordError ty err]
matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail [sumError ty err]
liftMaybe :: WithTop a => Maybe a -> String -> Infer a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail [err]
-- try to inline lookup
-- assume that ctx != Empty if not otherwise stated because this case was already covered in the previous step
-- if there is a bind replace lookup definition with it
......@@ -157,14 +136,6 @@ lookup t x = case parent t of
lookup p x
Just p@(Pair t1 t2 _) | t == t2 -> do
lookup p x
Just p@(Sel n term _) | t == term -> do
lookup p x
-- For every term we just call lookup on parent because the contex is not extended
-- Thus we have a single case without a guard simply call lookup on parent
-- because every entry of list has same parent
-- TODO: what would happen if the context is extended in different ways?
Just p@(Rec tpairs _) -> do
lookup p x
Just p@(InL term _) -> do
lookup p x
Just p@(InR term _) -> do
......@@ -220,10 +191,6 @@ inferType (Snd t _) = do
ty <- inferType t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType (Sel n t _) = do
ty <- inferType t
typairs <- matchRecord ty (show t)
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType t = fail ["Cannot infer type of term " ++ show t]
checkType :: Term -> Check
......@@ -236,17 +203,6 @@ checkType p@(Pair t1 t2 _) = do
(ty1, ty2) <- matchProd ty (show p)
checkType t1
checkType t2
checkType p@(Rec tpairs _) = do
ty <- requiredType p
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType t
) tpairs
foldl (>>) (return ()) subresults
else fail ["Length of term labels and type labels does not match"]
checkType p@(InL t _) = do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......@@ -294,18 +250,6 @@ requiredType t = case parent t of
ty <- requiredType p
(ty1, ty2) <- matchProd ty (show p)
return ty2
Just p@(Rec tpairs _) -> do
ty <- requiredType p
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
-- TODO what happens if two labels have the same term?
-- TODO what happens if a label is used twice in a record?
let labeledterm = find (\(l, lt) -> lt == t) tpairs
if isJust labeledterm
then liftMaybe (Map.lookup (fst $ fromJust labeledterm) typairs) ""
else fail ["label associated with term not found"]
else fail ["Length of term labels and type labels does not match"]
Just p@(InL term _) | t == term -> do
ty <- requiredType p
(ty1, ty2) <- matchSum ty (show p)
......
src/ExtendedTLC/EliminateTypeArgumentOfCheck.hs → src/SumTypes/EliminateTypeArgumentOfCheck.hs
View file @ 1aeae616
......@@ -2,16 +2,12 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RebindableSyntax #-}
module ExtendedTLC.EliminateTypeArgumentOfCheck where
module SumTypes.EliminateTypeArgumentOfCheck where
import Prelude hiding (Monad(..), (>=), (<=), lookup)
import GHC.Exts (Constraint)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (isJust, fromJust)
import ExtendedTLC.Language
import SumTypes.Language
import Util.ErrorMessages
import Util.PartialOrd
......@@ -46,12 +42,6 @@ instance WithTop () where
instance (WithTop a, WithTop b) => WithTop (a, b) where
top = (top, top)
instance WithTop a => WithTop [a] where
top = [top]
instance WithTop a => WithTop (Map Name a) where
top = Map.empty
-- Had to define an own monad type class.
-- It is not possible otherwise to get the type constraint WithTop a.
-- We use the extension ConstraintKinds to support this.
......@@ -98,14 +88,6 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 >= ty2 = return ()
matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err]
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail [recordError ty err]
liftMaybe :: WithTop a => Maybe a -> String -> Infer a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail [err]
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail ["Unbound variable " ++ show x]
lookup (Bind c x t) y | x == y = return t
......@@ -144,10 +126,6 @@ inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail ["Cannot infer type of term " ++ show t]
checkType :: Ctx -> Term -> Check
......@@ -161,46 +139,6 @@ checkType ctx p@(Pair t1 t2 _) = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1
checkType ctx t2
checkType ctx p@(Rec tpairs _) = do
ty <- requiredType ctx p
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t
) tpairs
foldl (>>) (return ()) subresults
else fail ["Length of term labels and type labels does not match"]
-- checkType ctx p@(Rec [(x, t)] _) = do
-- ty <- requiredType ctx p
-- [(x', tty)] <- matchRecord ty (show p)
-- if x == x'
-- then checkType ctx t
-- else fail ["Does not match"]
--
-- checkType ctx p@(Rec [(x1, t1), (x2, t2)] _) = do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2)] <- matchRecord ty (show p)
-- if x1 == x1'
-- then checkType ctx t1
-- else fail ["Does not match"]
-- if x2 == x2'
-- then checkType ctx t2
-- else fail ["Does not match"]
--
-- checkType ctx p@(Rec [(x1, t1), (x2, t2), (x3, t3)] _) = do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2), (x3', tty3)] <- matchRecord ty (show p)
-- if x1 == x1'
-- then checkType ctx t1
-- else fail ["Does not match"]
-- if x2 == x2'
-- then checkType ctx t2
-- else fail ["Does not match"]
-- if x3 == x3'
-- then checkType ctx t3
-- else fail ["Does not match"]
checkType ctx p@(InL t _) = do
ty <- requiredType ctx p
(ty1, ty2) <- matchSum ty (show p)
......@@ -250,25 +188,6 @@ requiredType ctx t = case parent t of
ty <- requiredType ctx p
(ty1, ty2) <- matchProd ty (show p)
return ty2
-- TODO: What does that mean for a map function that contains the call site?
-- Basic Idea: transform the map call into a find call where the predicate is the guard within the map that precedes the checkType call
-- We know what we want to select, but how can we derive which projections are needed?
-- TODO: Are the functions (map, find) valid in Datalog? What do the correspond to?
-- TODO: this code does not work the way it should be? We need to find the entry that belongs to the term in question and check that the labels are the same in the zipped list. This results in a guard t == t' && x == x'
-- x == x' can be derived based on the the guard in the map function call
-- TODO: How can we derive the other guard t == t'? Is this basically the top level guard?
Just p@(Rec tpairs _) -> do
ty <- requiredType ctx p
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
-- TODO what happens if two labels have the same term?
-- TODO what happens if a label is used twice in a record?
let labeledterm = find (\(l, lt) -> lt == t) tpairs
if isJust labeledterm
then liftMaybe (Map.lookup (fst $ fromJust labeledterm) typairs) ""
else fail ["label associated with term not found"]
else fail ["Length of term labels and type labels does not match"]
Just p@(InL term _) | t == term -> do
ty <- requiredType ctx p
(ty1, ty2) <- matchSum ty (show p)
......@@ -278,7 +197,6 @@ requiredType ctx t = case parent t of
(ty1, ty2) <- matchSum ty (show p)
return ty2
Just p@(Case e n1 t1 n2 t2 _) | t == t1 -> do
-- TODO Does using deconstructed context for complete slice yield correct required?
let (Bind ctx' _ _) = ctx
ety <- inferType ctx' e
(ty1, ty2) <- matchSum ety (show e)
......@@ -291,45 +209,3 @@ requiredType ctx t = case parent t of
ty <- requiredType ctx' p
return ty
_ -> fail ["Could not determine required type"]
-- checkType ctx p@(Case e n1 t1 n2 t2 _) = do
-- ety <- inferType ctx e
-- (ty1, ty2) <- matchSum ety (show e)
-- ty <- requiredType ctx p
-- checkType (Bind ctx n1 ty1) t1
-- checkType (Bind ctx n2 ty2) t2
-- Just p@(Rec [(x, t')] _) | t == t' -> do
-- ty <- requiredType ctx p
-- [(x', tty)] <- matchRecord ty (show p)
-- if x == x'
-- then return tty
-- else fail ["Does not match"]
-- Just p@(Rec [(x1, t1), (x2, t2)] _) | t == t1 -> do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2)] <- matchRecord ty (show p)
-- if x1 == x1'
-- then return tty1
-- else fail ["Does not match"]
-- Just p@(Rec [(x1, t1), (x2, t2)] _) | t == t2 -> do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2)] <- matchRecord ty (show p)
-- if x2 == x2'
-- then return tty2
-- else fail ["Does not match"]
-- Just p@(Rec [(x1, t1), (x2, t2), (x3, t3)] _) | t == t1 -> do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2), (x3', tty3)] <- matchRecord ty (show p)
-- if x1 == x1'
-- then return tty1
-- else fail ["Does not match"]
-- Just p@(Rec [(x1, t1), (x2, t2), (x3, t3)] _) | t == t2 -> do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2), (x3', tty3)] <- matchRecord ty (show p)
-- if x2 == x2'
-- then return tty2
-- else fail ["Does not match"]
-- Just p@(Rec [(x1, t1), (x2, t2), (x3, t3)] _) | t == t3 -> do
-- ty <- requiredType ctx p
-- [(x1', tty1), (x2', tty2), (x3', tty3)] <- matchRecord ty (show p)
-- if x3 == x3'
-- then return tty3
-- else fail ["Does not match"]
src/ExtendedTLC/ErrorList.hs → src/SumTypes/ErrorList.hs
View file @ 1aeae616
module ExtendedTLC.ErrorList where
module SumTypes.ErrorList where
import Prelude hiding (lookup, Ord)
import Data.List(find)
import Data.Map (Map)
import qualified Data.Map as Map (lookup)
import ExtendedTLC.Language
import SumTypes.Language
import Util.ErrorMessages
type Error = [String]
......@@ -46,18 +44,10 @@ matchType :: Type -> Type -> String -> Check
matchType ty1 ty2 _ | ty1 == ty2 = return ()
matchType ty1 ty2 err = fail $ generalError (show ty1) ty2 err
matchRecord :: Type -> String -> Infer (Map Name Type)
matchRecord (Record pairs) _ = return pairs
matchRecord ty err = fail $ recordError ty err
matchSum :: Type -> String -> Infer (Type, Type)
matchSum (Sum ty1 ty2) _ = return (ty1, ty2)
matchSum ty err = fail $ sumError ty err
liftMaybe :: Monad m => Maybe a -> String -> m a
liftMaybe (Just a) _ = return a
liftMaybe Nothing err = fail err
lookup :: Ctx -> Name -> Infer Type
lookup Empty x = fail $ "Unbound variable " ++ show x
lookup (Bind c x t) y | x == y = return t
......@@ -96,10 +86,6 @@ inferType ctx (Snd t _) = do
ty <- inferType ctx t
(_, ty2) <- matchProd ty (show t)
return ty2
inferType ctx (Sel n t _) = do
ty <- inferType ctx t
typairs <- matchRecord ty (show t)
liftMaybe (Map.lookup n typairs) $ "Could not project" ++ (show n)
inferType _ t = fail $ "Cannot infer type of term " ++ show t
checkType :: Ctx -> Term -> Type -> Check
......@@ -110,17 +96,6 @@ checkType ctx p@(Pair t1 t2 _) ty = do
(ty1, ty2) <- matchProd ty (show p)
checkType ctx t1 ty1
checkType ctx t2 ty2
checkType ctx p@(Rec tpairs _) ty = do
typairs <- matchRecord ty (show p)
if length tpairs == length typairs
then do
let subresults = map (\(tl, t) -> do
lty <- liftMaybe (Map.lookup tl typairs) ""
checkType ctx t lty
) tpairs
foldl (>>) (return ()) subresults
else
fail "Length of term labels and type labels does not match"
checkType ctx p@(InL t _) ty = do
(ty1, ty2) <- matchSum ty (show p)
checkType ctx t ty1
......
src/ExtendedTLC/Language.hs → src/SumTypes/Language.hs
View file @ 1aeae616
module ExtendedTLC.Language where
import Data.Map (Map)
import qualified Data.Map as Map
module SumTypes.Language where
import Prelude hiding (Ord, (<=), (>=))
import Util.PartialOrd as PO
......@@ -25,9 +22,6 @@ data Term =
Snd Term Parent |
-- let binding
Let Name Term Term Parent |
-- records
Rec [(Name, Term)] Parent |
Sel Name Term Parent |
-- sum types
InL Term Parent |
InR Term Parent |
......@@ -46,8 +40,6 @@ instance Eq Term where
(Fst t _) == (Fst t' _) = t == t'
(Snd t _) == (Snd t' _) = t == t'
(Let n t1 t2 _) == (Let n' t1' t2' _) = n == n' && t1 == t1' && t2 == t2'
(Rec p _) == (Rec p' _) = p == p'
(Sel n t _) == (Sel n' t' _) = n == n' && t == t'
(InL t _) == (InL t' _) = t == t'
(InR t _) == (InR t' _) = t == t'
(Case e n1 t1 n2 t2 _) == (Case e' n1' t1' n2' t2' _) = e == e' && n1 == n1' && t1 == t1' && n2 == n2' && t2 == t2'
......@@ -68,8 +60,6 @@ parent (Pair _ _ p) = p
parent (Fst _ p) = p
parent (Snd _ p) = p
parent (Let _ _ _ p) = p
parent (Rec _ p) = p
parent (Sel _ _ p) = p
parent (InL _ p) = p
parent (InR _ p) = p
parent (Case _ _ _ _ _ p) = p
......@@ -109,16 +99,11 @@ snd' = cons1 Snd
let' n = cons2 (Let n)
sel n = cons1 (Sel n)
inl = cons1 InL
inr = cons1 InR
case' e n1 t1 n2 t2 parent = let res = Case (e (Just res)) n1 (t1 (Just res)) n2 (t2 (Just res)) parent in res
rec0 parent = let res = Rec [] parent in res
rec1 (l1, t1) parent = let res = Rec [(l1, (t1 (Just res)))] parent in res
rec2 (l1, t1) (l2, t2) parent = let res = Rec [(l1, (t1 (Just res))), (l2, (t2 (Just res)))] parent in res
rec3 (l1, t1) (l2, t2) (l3, t3) parent = let res = Rec [(l1, (t1 (Just res))), (l2, (t2 (Just res))), (l3, (t3 (Just res)))] parent in res
instance Show Term where
showsPrec _ (Var x _) = showString x
......@@ -142,18 +127,14 @@ instance Show Term where
showString "let " . showString n . showString " = " . showsPrec (p + 1) e . showString " in " . showsPrec (p + 1) b
showsPrec p (InL t _) = showString "InL " . showsPrec (p + 1) t
showsPrec p (InR t _) = showString "InR " . showsPrec (p + 1) t
showsPrec p (Sel n t _) = showString "Sel " . showsPrec (p + 1) t . showString "." . showString n
showsPrec p (Rec pairs _) = showString "pair"
data Type = Nat | Fun Type Type | Prod Type Type | Record (Map Name Type) | Sum Type Type | SumI [Type] | AnyType
data Type = Nat | Fun Type Type | Prod Type Type | Sum Type Type | AnyType
deriving (Show, Eq)
instance PO.PartialOrd Type where
_ <= AnyType = True
(Fun t1 t2) <= (Fun u1 u2) = t1 <= u1 && t2 <= u2
(Prod t1 t2) <= (Prod u1 u2) = t1 <= u1 && t2 <= u2
(Record pairs) <= (Record pairs') = all (\((x, ty), (x', ty')) -> if x == x' then ty <= ty' else False) zipped where zipped = zip (Map.toList pairs) (Map.toList pairs')
(Sum t1 t2) <= (Sum u1 u2) = t1 <= u1 && t2 <= u2
ty1 <= ty2 = ty1 == ty2
......
test/ExtendedTLC/EqualOutputSharedSpecs.hs deleted 100644 → 0
View file @ efabcfbd
module ExtendedTLC.EqualOutputSharedSpecs where
import Prelude
import Test.Hspec
import ExtendedTLC.TestCases
import ExtendedTLC.Language
import Util.PartialOrd
contained :: (Eq a) => [a] -> [a] -> Bool
contained xs ys = all (\x -> x `elem` ys) xs
-- sharedSpec :: (b -> i Type -> Bool) -> (Term -> b) -> (Term -> i Type) -> Spec
-- sharedSpec compareResult base other= do
-- describe "compare the results of two equvilant transformations " $ do
-- it "should infer Zero to be of type Nat" $ do
-- compareResult (base tOkZero) (other tOkZero) `shouldBe` True
-- it "should infer (Succ Zero) to be of type Nat" $ do
-- compareResult (base tOkSucc) (other tOkSucc) `shouldBe` True
-- it "should infer arithmetic expression to be of type Nat" $ do
-- compareResult (base tOkArithmetic) (other tOkArithmetic) `shouldBe` True
-- it "should infer let binding with arithmetic expression to be of type Nat" $ do
-- compareResult (base tOkLetBindingWithArith) (other tOkLetBindingWithArith) `shouldBe` True
-- it "should infer expression to be of type (Prod Nat (Prod Nat Nat))" $ do
-- compareResult (base tOkProd) (other tOkProd) `shouldBe` True
-- it "should infer projection for first element to be of type Nat" $ do
-- compareResult (base tOkProjection1) (other tOkProjection1) `shouldBe` True
-- it "should infer projection for second element to be of type (Prod Nat Nat)" $ do
-- compareResult (base tOkProjection2) (other tOkProjection2) `shouldBe` True
-- it "should infer nested lambda expressions" $ do
-- compareResult (base tOkAppLambdaAnno) (other tOkAppLambdaAnno) `shouldBe` True
-- it "should infer annotated lambda to be of type (Fun Nat Nat)" $ do
-- compareResult (base tOkLambdaAnno) (other tOkLambdaAnno) `shouldBe` True
-- it "should infer application of lambda expression" $ do
-- compareResult (base tOkAnno) (other tOkAnno) `shouldBe` True
-- it "should infer let binding with annotation in named expression" $ do
-- compareResult (base tOkAnnoInBindingLet) (other tOkAnnoInBindingLet) `shouldBe` True
-- it "should infer let binding in pair(fst)" $ do
-- compar