Working coercions, with one assign-ouput

This commit is contained in:
Macocian Adrian Radu
2022-05-09 13:50:36 +02:00
parent 3caea6f18a
commit ee26710515
4 changed files with 51 additions and 32 deletions

View File

@@ -51,7 +51,7 @@ data ExplicitExpression = ExplicitEmpty
| ExplicitFunction {name :: String, args :: [(ExplicitExpression, Coercion)], returnCoercion :: Coercion} | ExplicitFunction {name :: String, args :: [(ExplicitExpression, Coercion)], returnCoercion :: Coercion}
| ExplicitIfSimple {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion} | ExplicitIfSimple {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion}
| ExplicitIfElse {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), block2 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion} | ExplicitIfElse {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), block2 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion}
deriving (Show) deriving (Show)
data TypeCoercion = data TypeCoercion =
MakeIdCoercion {toType :: Type} MakeIdCoercion {toType :: Type}

View File

@@ -7,6 +7,7 @@ import Model.Function
import PrettyPrinter.General import PrettyPrinter.General
import PrettyPrinter.Type import PrettyPrinter.Type
import Model.Type import Model.Type
import Semantic.ExpressionChecker(coercionIncluded)
-- show printStatementTree -- show printStatementTree
@@ -16,36 +17,48 @@ printFunction f = show $ vcat [printFunctionSignature (sign f), printFunctionBod
-- |Converts the body of a Function into a haskell valid Doc -- |Converts the body of a Function into a haskell valid Doc
printFunctionBody :: ExplicitFunction -> Doc a printFunctionBody :: ExplicitFunction -> Doc a
printFunctionBody (MakeExplicitFunction (MakeFunctionSignature name _ inp out) ex) = pretty name <+> printVariableNames inp <+> "=" <+> printExpression ex printFunctionBody (MakeExplicitFunction (MakeFunctionSignature name _ inp out) ex) = pretty name <+> printVariableNames inp <+> "=" <+> printExpression ex (createCoercion (attributeType out, Model.Type.cardinality out))
printExpression :: ExplicitExpression -> Doc a printExpression :: ExplicitExpression -> Coercion -> Doc a
printExpression ExplicitEmpty = "[]" printExpression ExplicitEmpty _ = "[]"
printExpression (ExplicitVariable name coer) = printCoercion coer $ pretty name printExpression (ExplicitVariable name coer) out = case coer `coercionIncluded` out of
printExpression (Value s coer) = printCoercion coer $ pretty s Left err -> error $ show err
printExpression (ExplicitParens ex) = "(" <> printExpression ex <> ")" Right c -> printCoercion c $ pretty name
printExpression (ExplicitList ex) = list (map printExpression ex) printExpression (Value s coer) out = case coer `coercionIncluded` out of
printExpression (ExplicitFunction "exists" args returnCoerce) = printCoercion returnCoerce "isJust" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) Left err -> error $ show err
printExpression (ExplicitFunction "is absent" args returnCoerce) = printCoercion returnCoerce "isNothing" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) Right c -> printCoercion c $ pretty s
printExpression (ExplicitFunction "single exists" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "==" <+> "1" printExpression (ExplicitParens ex) out = "(" <> printExpression ex out <> ")"
printExpression (ExplicitFunction "multiple exists" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> ">" <+> "1" printExpression (ExplicitList ex) out = list [printExpression x out | x <- ex]
printExpression (ExplicitFunction "count" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) printExpression (ExplicitFunction "exists" args returnCoerce) out = printCoercion returnCoerce "isJust" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
printExpression (ExplicitFunction "is absent" args returnCoerce) out = printCoercion returnCoerce "isNothing" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
printExpression (ExplicitFunction "single exists" args returnCoerce) out = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "==" <+> "1"
printExpression (ExplicitFunction "multiple exists" args returnCoerce) out = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> ">" <+> "1"
printExpression (ExplicitFunction "count" args returnCoerce) out = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
-- Equality expressions -- Equality expressions
-- [a] a all = -- [a] a all =
-- any <> -- any <>
printExpression (ExplicitFunction "=" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "==" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) printExpression (ExplicitFunction "=" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "==" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
printExpression (ExplicitFunction "<>" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "/=" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) printExpression (ExplicitFunction "<>" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "/=" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
printExpression (ExplicitFunction "any =" args returnCoerce) = printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)<+> "`elem`" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) printExpression (ExplicitFunction "any =" args returnCoerce) out = printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out) <+> "`elem`" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
printExpression (ExplicitFunction "all <>" args returnCoerce) = printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)<+> "`notElem`" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) printExpression (ExplicitFunction "all <>" args returnCoerce) out = printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out) <+> "`notElem`" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
printExpression (ExplicitFunction "all =" args returnCoerce) = "all (Eq)" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) printExpression (ExplicitFunction "all =" args returnCoerce) out = "all (Eq)" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out) <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
printExpression (ExplicitFunction "and" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "&&" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) printExpression (ExplicitFunction "and" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "&&" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
printExpression (ExplicitFunction "or" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "||" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) printExpression (ExplicitFunction "or" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "||" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
printExpression (ExplicitFunction name args returnCoerce) = pretty name <+> tupled (zipWith printCoercion [c | (e,c) <- args] [printExpression e | (e, c) <- args]) printExpression (ExplicitFunction name args returnCoerce) out = pretty name <+> tupled (zipWith printCoercion [c | (e,c) <- args] [printExpression e out | (e, c) <- args])
printExpression (ExplicitIfSimple cond thenBlock returnCoercion) = "if" <+> printCoercion (snd cond) (printExpression $ fst cond) <+> "then" <+> printCoercion (snd thenBlock) (printExpression $ fst thenBlock) <+> "else" <+> "Nothing" printExpression (ExplicitIfSimple cond thenBlock returnCoercion) out =
printExpression (ExplicitIfElse cond thenBlock elseBlock returnCoercion) = "if" <+> printCoercion (snd cond) (printExpression $ fst cond) <+> "then" <+> printCoercion (snd thenBlock) (printExpression $ fst thenBlock) <+> "else" <+> printCoercion (snd elseBlock) (printExpression $ fst elseBlock) "if" <+> printCoercion (snd cond) (printExpression (fst cond) (MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1))))) <+>
"then" <+> printCoercion (snd thenBlock) (printExpression (fst thenBlock) out) <+>
"else" <+> case MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion returnCoercion] (MakeCardinalityIdCoercion (Bounds (0, 0))) `coercionIncluded` out of
Left err -> error $ show err
Right c -> printCoercion c emptyDoc
printExpression (ExplicitIfElse cond thenBlock elseBlock returnCoercion) out =
"if" <+> printCoercion (snd cond) (printExpression (fst cond) (MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1))))) <+>
"then" <+> printCoercion (snd thenBlock) (printExpression (fst thenBlock) out) <+>
"else" <+> printCoercion (snd elseBlock) (printExpression (fst elseBlock) out)
-- |Converts a coercion into a haskell string -- |Converts a coercion into a haskell string
printCoercion :: Coercion -> Doc a -> Doc a printCoercion :: Coercion -> Doc a -> Doc a
printCoercion (MakeCoercion [] crd) d = printCardinalityCoercion crd d printCoercion (MakeCoercion [] crd) d = printCardinalityCoercion crd d
printCoercion (MakeCoercion (t: ts) crd) d = printTypeCoercion t <+> printCoercion (MakeCoercion ts crd) d printCoercion (MakeCoercion (t: ts) crd) d = printTypeCoercion t <> printCoercion (MakeCoercion ts crd) d
printCardinalityCoercion :: CardinalityCoercion -> Doc a -> Doc a printCardinalityCoercion :: CardinalityCoercion -> Doc a -> Doc a
printCardinalityCoercion (MakeCardinalityIdCoercion _) d = d printCardinalityCoercion (MakeCardinalityIdCoercion _) d = d
@@ -58,8 +71,8 @@ printCardinalityCoercion (MakeObject2ListCoercion _ _) d = "[" <> d <> "]"
printTypeCoercion :: TypeCoercion -> Doc a printTypeCoercion :: TypeCoercion -> Doc a
printTypeCoercion (MakeIdCoercion _) = emptyDoc printTypeCoercion (MakeIdCoercion _) = emptyDoc
printTypeCoercion (MakeSuperCoercion _ _) = "super" printTypeCoercion (MakeSuperCoercion _ _) = "super" <+> emptyDoc
printTypeCoercion (MakeTypeCoercion _ _ t) = pretty t printTypeCoercion (MakeTypeCoercion _ _ t) = pretty t <+> emptyDoc
-- |Converts a list of type attributes to a Doc with a list of variable names -- |Converts a list of type attributes to a Doc with a list of variable names
printVariableNames :: [TypeAttribute] -> Doc a printVariableNames :: [TypeAttribute] -> Doc a

View File

@@ -112,8 +112,12 @@ checkExpression symbolMap (IfSimple cond ex) =
Left err -> Left err Left err -> Left err
Right thenExp -> Right thenExp ->
Right $ ExplicitIfSimple (condType, condCoerce) Right $ ExplicitIfSimple (condType, condCoerce)
(thenExp, MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp] (thenExp, thenCoercion)
(MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion thenExp)) (returnCoercion thenExp) (MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp]
(MakeCardinalityIdCoercion $ smallestBound (Bounds (0, 0)) (toCardinality $ cardinalityCoercion $ returnCoercion thenExp)))
where
thenCoercion = MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp]
(MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion thenExp)
-- |Checks if the condition of the if statement is of type boolean, and then checks that both the then and else statements have the same type -- |Checks if the condition of the if statement is of type boolean, and then checks that both the then and else statements have the same type
checkExpression symbolMap (IfElse cond ex1 ex2) = checkExpression symbolMap (IfElse cond ex1 ex2) =
@@ -217,13 +221,13 @@ findVarType x (_:symbols) = findVarType x symbols
isSubType :: Type -> Type -> Either TypeCheckError [TypeCoercion] isSubType :: Type -> Type -> Either TypeCheckError [TypeCoercion]
isSubType (BasicType "Integer") (BasicType "Double") = Right [MakeTypeCoercion (BasicType "Integer") (BasicType "Double") "fromInteger"] isSubType (BasicType "Integer") (BasicType "Double") = Right [MakeTypeCoercion (BasicType "Integer") (BasicType "Double") "fromInteger"]
isSubType (BasicType x) y isSubType (BasicType x) y
| x == typeName y = Right [MakeTypeCoercion y y "id"] | x == typeName y = Right [MakeIdCoercion y]
| otherwise = Left $ TypeMismatch x (typeName y) | otherwise = Left $ TypeMismatch x (typeName y)
isSubType x y isSubType x y
| typeName x == typeName y = Right [MakeTypeCoercion x y "id"] | typeName x == typeName y = Right [MakeIdCoercion x]
| otherwise = case isSubType (superType x) y of | otherwise = case isSubType (superType x) y of
Left e -> Left e Left e -> Left e
Right transforms -> Right $ MakeTypeCoercion x y "super" : transforms Right transforms -> Right $ MakeSuperCoercion x y : transforms
-- |Checks whether the first cardinality is included into the second one -- |Checks whether the first cardinality is included into the second one
cardinalityIncluded :: Cardinality -> Cardinality -> Either TypeCheckError CardinalityCoercion cardinalityIncluded :: Cardinality -> Cardinality -> Either TypeCheckError CardinalityCoercion
@@ -238,6 +242,7 @@ cardinalityIncluded (Bounds (0, 1)) (OneBound 0) = Right $ MakeMaybe2ListCoercio
cardinalityIncluded (Bounds (1, 1)) (Bounds (0, 1)) = Right $ MakeObject2MaybeCoercion (Bounds (0, 1)) (Bounds (0, 1)) cardinalityIncluded (Bounds (1, 1)) (Bounds (0, 1)) = Right $ MakeObject2MaybeCoercion (Bounds (0, 1)) (Bounds (0, 1))
-- |Transform object into list -- |Transform object into list
cardinalityIncluded (Bounds (1, 1)) (OneBound 1) = Right $ MakeObject2ListCoercion (Bounds (0, 1)) (OneBound 1) cardinalityIncluded (Bounds (1, 1)) (OneBound 1) = Right $ MakeObject2ListCoercion (Bounds (0, 1)) (OneBound 1)
cardinalityIncluded (Bounds (1, 1)) (OneBound 0) = Right $ MakeObject2ListCoercion (Bounds (0, 1)) (OneBound 1)
-- |General -- |General
cardinalityIncluded (OneBound x) (OneBound y) cardinalityIncluded (OneBound x) (OneBound y)
| x >= y = Right $ MakeListCardinalityCoercion (OneBound x) (OneBound y) | x >= y = Right $ MakeListCardinalityCoercion (OneBound x) (OneBound y)

View File

@@ -19,7 +19,8 @@ checkFunction (definedTypes, symbols) (MakeFunction (MakeFunctionSignature name
Left err -> Left [err] Left err -> Left [err]
Right checkedEx -> case returnCoercion checkedEx `coercionIncluded` createCoercion (attributeType checkedOut, Model.Type.cardinality out) of Right checkedEx -> case returnCoercion checkedEx `coercionIncluded` createCoercion (attributeType checkedOut, Model.Type.cardinality out) of
Left err -> Left [err] Left err -> Left [err]
Right _ -> Right $ MakeExplicitFunction (MakeFunctionSignature (toLower (head name) : tail name) desc (rights checkedIn) checkedOut) checkedEx Right retCoercion -> Right $ MakeExplicitFunction (MakeFunctionSignature (toLower (head name) : tail name) desc (rights checkedIn) checkedOut) checkedEx
--Right _ -> error $ show (returnCoercion checkedEx) ++ " // " ++ show (createCoercion (attributeType checkedOut, Model.Type.cardinality out))
else else
Left $ lefts checkedIn Left $ lefts checkedIn
where checkedIn = checkAttributes definedTypes inp where checkedIn = checkAttributes definedTypes inp