Commit 1facde36 authored by marton bognar's avatar marton bognar
Browse files

Fixes to STLC Prod specification and its processing

parent 56babced
......@@ -14,7 +14,7 @@ sort Term
sort Pat
inh ictx TermVar
syn sctx TermVar
| PVar (x: TermVar)
| PVar [x: TermVar]
lhs.sctx = lhs.ictx, x
| PProd (p1: Pat) (p2: Pat)
p1.ictx = lhs.ictx
......
......@@ -11,7 +11,8 @@ data ConvertFunctions = VF {
userTypes :: Language -> [(Type, [Constructor])],
variableInstances :: (Type, [Constructor]) -> [(Type, Type, [Function])],
variableFunctions :: Language -> (Type, [Constructor]) -> [Function],
envFunctions :: Language -> [Function]
envFunctions :: Language -> [Function],
nativeCode :: Language -> (Type, [Constructor])-> [String]
}
-- | Convert a language into a program using the specified variable functions
......@@ -25,5 +26,5 @@ convert lan@(nsd, sd, imp, cd) vf =
instances = (variableInstances vf) var,
functions = (variableFunctions vf) lan var ++
(envFunctions vf) lan,
code = cd
code = (nativeCode vf) lan var ++ cd
}
......@@ -24,7 +24,7 @@ myDef =
, "c"
, "rewrite"
, "import"
, "HaskellCode"
, "NativeCode"
]
, reservedOpNames = ["@", "=", ",", ".", ";", ":", "|"]
}
......
......@@ -48,8 +48,6 @@ printProgram name program =
printImports (("Data.List", []) : imports program),
printTypeDecls (types program),
nl,
freshVarFunctions (types program),
nl,
printFunctions (functions program),
printInstances (instances program),
printCode (code program)
......@@ -95,11 +93,3 @@ printInstances ids = intoLines $ map (
printCode :: [String] -> Doc String
printCode lns = intoLines $ map pretty lns
freshVarFunctions :: [(Type, [Constructor])] -> Doc String
freshVarFunctions types
= let ctors = fromJust (lookup "Variable" types)
names = map (\(Constr name _) -> tail name) ctors
in intoLines [
pretty ("fresh" ++ name ++ " x b = if not (x `elem` b) then x else head [S" ++ name ++ " ('v' : show n) | n <- [0..], not (S" ++ name ++ " ('v' : show n) `elem` b)]")
| name <- names]
......@@ -75,7 +75,7 @@ getEnvFunctions (nsd, sd, _, _)
collectRulesOfIdSyn iden = (iden, filter (\(LeftSub fieldname _, RightSub _ _) -> fieldname == iden) attrs)
navigateAttrs :: AttributeDef -> Expression
navigateAttrs (l, RightAdd expr _) = FnCall ("S" ++ xnamespace ctx) [navigateAttrs (l, expr)]
navigateAttrs (l, RightAdd expr _) = ConstrInst ("S" ++ xnamespace ctx) [navigateAttrs (l, expr)]
navigateAttrs (LeftLHS _, RightLHS _) = VarExpr "c"
navigateAttrs (LeftSub _ _, RightLHS _) = VarExpr "c"
navigateAttrs (_, RightSub iden _)
......
......@@ -17,7 +17,8 @@ getFunctions
userTypes = getTypes,
variableInstances = getVariableInstances,
variableFunctions = getVariableFunctions,
envFunctions = getEnvFunctions
envFunctions = getEnvFunctions,
nativeCode = (\_ _ -> [])
}
getVariableType :: Language -> (Type, [Constructor])
......
......@@ -18,9 +18,17 @@ getFunctions
userTypes = getTypes,
variableInstances = getVariableInstances,
variableFunctions = getVariableFunctions,
envFunctions = getEnvFunctions
envFunctions = getEnvFunctions,
nativeCode = freshVarFunctions
}
freshVarFunctions :: Language -> (Type, [Constructor]) -> [String]
freshVarFunctions _ varType
= let ctors = snd varType
names = map (\(Constr name _) -> tail name) ctors
in ["fresh" ++ name ++ " x b = if not (x `elem` b) then x else head [S" ++ name ++ " ('v' : show n) | n <- [0..], not (S" ++ name ++ " ('v' : show n) `elem` b)]"
| name <- names]
getVariableType :: Language -> (Type, [Constructor])
getVariableType (nsd, _, _, _) = ("Variable", map (\ns -> Constr ('S' : nname ns) ["String"]) nsd)
......
......@@ -10,8 +10,39 @@ import Data.Maybe
wellFormed :: Language -> Either String Bool
wellFormed ([], [], _, _) = Left "Empty Language"
wellFormed (namespaces, sorts, _, _) = do
_ <- helpWellFormedVariablesNamespace sorts namespaces
_ <- helpWellFormedVariablesNamespace sorts
helpWellFormed (namespaces, sorts) [] [] [] [] [] [] []
where
--variables should only refer to namespace they are part of
helpWellFormedVariablesNamespace :: [SortDef] -> Either String Bool
helpWellFormedVariablesNamespace [] = return True
helpWellFormedVariablesNamespace (MkDefSort sortName ctxs cons _:rest) = do
_ <- helpWellFormedVariablesCons sortName cons ctxs
helpWellFormedVariablesNamespace rest
helpWellFormedVariablesCons :: SortName -> [ConstructorDef] -> [Context] -> Either String Bool
helpWellFormedVariablesCons _ [] _ = Right True
helpWellFormedVariablesCons sortName (MkVarConstructor _ instanceName:rest) ctxs = do
_ <- helpWellFormedVarInst sortName instanceName ctxs
helpWellFormedVariablesCons sortName rest ctxs
helpWellFormedVariablesCons sortName (_:rest) ctxs =
helpWellFormedVariablesCons sortName rest ctxs
helpWellFormedVarInst :: SortName -> InstanceName -> [Context] -> Either String Bool
helpWellFormedVarInst _ name [] = Left ("No instance found with that name in " ++ name)
helpWellFormedVarInst sortName name (ctx:rest) =
if xinst ctx == name
then helpVarnamespace sortName (xnamespace ctx) namespaces
else helpWellFormedVarInst sortName name rest
helpVarnamespace :: SortName -> String -> [NamespaceDef] -> Either String Bool
helpVarnamespace _ _ [] = Left "Instance and namespace in variable do not coincide"
helpVarnamespace sortName name (MkNameSpace namespacename sortname _:rest) =
if namespacename == name
then (if sortName == sortname
then return True
else Left ("sort cannot use this namespace in " ++ sortName))
else helpVarnamespace sortName name rest
--accumulates the sortnames, constructornames, and the sortnames contained in the constructors,
--then looks up if all sortnames,namespacenames and contructornames are unique, if all sorts in the constructors exist,
......@@ -168,39 +199,6 @@ helpWellFormedInstances l l2 = shouldBeInSecondList l l2 "Instance does not refe
helpWellFormedInstanceNames :: [InstanceName] -> Either String Bool
helpWellFormedInstanceNames l = isUniqueInList l "Instance is not a unique name in the declaration "
--variables should only refer to namespace they are part of
helpWellFormedVariablesNamespace :: [SortDef] -> [NamespaceDef] -> Either String Bool
helpWellFormedVariablesNamespace [] _ = return True
helpWellFormedVariablesNamespace (MkDefSort sortName ctxs cons _:rest) namespaces = do
_ <- helpWellFormedVariablesCons sortName cons ctxs namespaces
helpWellFormedVariablesNamespace rest namespaces
helpWellFormedVariablesCons :: SortName -> [ConstructorDef] -> [Context] -> [NamespaceDef] -> Either String Bool
helpWellFormedVariablesCons _ [] _ _ = Right True
helpWellFormedVariablesCons sortName (MkVarConstructor _ instanceName:rest) ctxs namespaces = do
_ <- helpWellFormedVarInst sortName instanceName ctxs namespaces
helpWellFormedVariablesCons sortName rest ctxs namespaces
helpWellFormedVariablesCons sortName (_:rest) ctxs namespace =
helpWellFormedVariablesCons sortName rest ctxs namespace
helpWellFormedVarInst :: SortName -> InstanceName -> [Context] -> [NamespaceDef] -> Either String Bool
helpWellFormedVarInst _ name [] _ =
Left ("No instance found with that name in " ++ name)
helpWellFormedVarInst sortName name (ctx:rest) namespaces =
if xinst ctx == name
then helpVarnamespace sortName (xnamespace ctx) namespaces
else helpWellFormedVarInst sortName name rest namespaces
helpVarnamespace :: SortName -> String -> [NamespaceDef] -> Either String Bool
helpVarnamespace _ _ [] =
Left "Instance and namespace in variable do not coincide"
helpVarnamespace sortName name (MkNameSpace namespacename sortname _:rest) =
if namespacename == name
then (if sortName == sortname
then return True
else Left ("sort cannot use this namespace in " ++ sortName))
else helpVarnamespace sortName name rest
--function to detect if all identifiers used in the rules exist as fields
helpWellFormedRulesIdentifiers :: [IdenName] -> [IdenName] -> Either String Bool
helpWellFormedRulesIdentifiers l l2 = shouldBeInSecondList l l2 "identifier not used in constructor"
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment