Commit d6d0d10c authored by marton bognar's avatar marton bognar
Browse files

Fix some issues with more complicated identifier sorts

parent 697cefbe
......@@ -137,14 +137,16 @@ sort Coercion rewrite
HaskellCode
-- You need to delete the "b" binder parameters if using De Bruijn indices
rewriteTypeToCoercion:: ValueType ->Coercion
rewriteTypeToCoercion (ValTyVar hnat) = CoTypeVar (ValTyVar hnat)
rewriteTypeToCoercion (ValTUnit) = CoUnit
rewriteTypeToCoercion (ValTyArr ty1 (ComputationTy ty2 dirt))= CoArrow (rewriteTypeToCoercion ty1) (CoComputation (rewriteTypeToCoercion ty2) (CoDirt dirt))
rewriteTypeToCoercion (ValTyHandler (ComputationTy ty1 dirt1) (ComputationTy ty2 dirt2)) = CoHandler (CoComputation (rewriteTypeToCoercion ty1) (CoDirt dirt1)) (CoComputation (rewriteTypeToCoercion ty2) (CoDirt dirt2))
rewriteTypeToCoercion (ValTyAllSkel ty) = CoskeletonAll (rewriteTypeToCoercion ty)
rewriteTypeToCoercion (ValTyAll valty skel)= CoTypeAll (rewriteTypeToCoercion valty) skel
rewriteTypeToCoercion (ValTyAllDirt valty)=CodirtAll (rewriteTypeToCoercion valty )
rewriteTypeToCoercion (ValTyAllSkel b ty) = CoskeletonAll b (rewriteTypeToCoercion ty)
rewriteTypeToCoercion (ValTyAll b valty skel)= CoTypeAll b (rewriteTypeToCoercion valty) skel
rewriteTypeToCoercion (ValTyAllDirt b valty)=CodirtAll b (rewriteTypeToCoercion valty )
rewriteTypeToCoercion (ValTyCoArr pi ty)= CoCoArrow pi (rewriteTypeToCoercion ty)
......@@ -153,8 +155,8 @@ rewriteCoercion (CoTypeVar ty) = rewriteTypeToCoercion ty
rewriteCoercion (CoArrow co1 co2) = CoArrow (rewriteCoercion co1) (rewriteCoercion co2)
rewriteCoercion (CoHandler co1 co2) = CoHandler (rewriteCoercion co1) (rewriteCoercion co2)
rewriteCoercion (UnionOp co1 op) = UnionOp (rewriteCoercion co1) op
rewriteCoercion (CoskeletonAll co) = CoskeletonAll (rewriteCoercion co)
rewriteCoercion (CoTypeAll co skel) = CoTypeAll (rewriteCoercion co ) skel
rewriteCoercion (CoskeletonAll b co) = CoskeletonAll b (rewriteCoercion co)
rewriteCoercion (CoTypeAll b co skel) = CoTypeAll b (rewriteCoercion co ) skel
rewriteCoercion (CoCoArrow pi co) = CoCoArrow pi (rewriteCoercion co )
rewriteCoercion (CoComputation co1 co2) = CoComputation (rewriteCoercion co1) (rewriteCoercion co2)
rewriteCoercion co = co
......@@ -116,12 +116,24 @@ replaceFunctions (nsd, sd, _, _) =
binder = if isBind ctor
then [FnCall
("fresh" ++ snd (fromJust (cbinder ctor)))
[VarExpr "b", FnCall "concat" [ListExpr (ListExpr [VarExpr "new"] : map (\(iden, namespace) -> FnCall ("freeVariables" ++ namespace) [ListExpr [], VarExpr iden]) (dropFold (cfolds ctor) ++ clists ctor ++ csorts ctor))]]]
[VarExpr "b", FnCall "concat" [ListExpr (ListExpr [VarExpr "new"] : map freeVariablesCall (folds ++ lists ++ csorts ctor))]]]
else []
idensAndAttrs = attrsByIden ctor
folds = dropFold (cfolds ctor)
lists = clists ctor
freeVariablesCall :: (IdenName, SortName) -> Expression
freeVariablesCall (iden, idenSort)
= if iden `elem` map fst folds
then FnCall "concat" [FnCall "fmap" [FnCall fnName substParams, idenExpr]]
else if iden `elem` map fst lists
then FnCall "concat" [FnCall "map" [FnCall fnName substParams, idenExpr]]
else FnCall fnName (substParams ++ [idenExpr])
where
fnName = "freeVariables" ++ idenSort
idenExpr = VarExpr iden
substParams = [ListExpr []]
-- | Returns whether the given constructor has a binder
isBind :: ConstructorDef -> Bool
isBind MkBindConstructor{} = True
......@@ -141,12 +153,22 @@ replaceFunctions (nsd, sd, _, _) =
fnName = sortNameForIden iden ctor ++ "VarReplace"
idenExpr = if null binder
then VarExpr iden
else FnCall
(sortNameForIden iden ctor ++ "VarReplace")
[VarExpr "b", head binder, VarExpr iden]
else varReplaceCall iden
substParams = [VarExpr "orig", VarExpr "new"]
sortNameOfIden = sortNameForIden iden ctor
varReplaceCall :: IdenName -> Expression
varReplaceCall iden
= if iden `elem` map fst folds
then FnCall "fmap" [FnCall fnName substParams, idenExpr]
else if iden `elem` map fst lists
then FnCall "map" [FnCall fnName substParams, idenExpr]
else FnCall fnName (substParams ++ [idenExpr])
where
fnName = (sortNameForIden iden ctor ++ "VarReplace")
idenExpr = VarExpr iden
substParams = [VarExpr "b", head binder]
sortHasCtxForSort :: SortName -> SortName -> Bool
sortHasCtxForSort sortName ctxSort
= let ctxs = [INH x y | INH x y <- fromJust (lookup sortName ctxsBySname)]
......@@ -204,12 +226,30 @@ substFunctionsC (nsd, sd, _, _) =
binder = if isBind ctor
then [FnCall
("fresh" ++ snd (fromJust (cbinder ctor)))
[VarExpr "b", FnCall "concat" [ListExpr (map (\(iden, namespace) -> FnCall ("freeVariables" ++ namespace) [ListExpr [], VarExpr iden]) (("sub", sortOfCtxNamespace) : dropFold (cfolds ctor) ++ clists ctor ++ csorts ctor))]]]
[VarExpr "b", FnCall "concat" [
ListExpr (
map
freeVariablesCall
(("sub", sortOfCtxNamespace) : folds ++ lists ++ csorts ctor)
)
]]]
else []
idensAndAttrs = attrsByIden ctor
folds = dropFold (cfolds ctor)
lists = clists ctor
freeVariablesCall :: (IdenName, SortName) -> Expression
freeVariablesCall (iden, idenSort)
= if iden `elem` map fst folds
then FnCall "concat" [FnCall "fmap" [FnCall fnName substParams, idenExpr]]
else if iden `elem` map fst lists
then FnCall "concat" [FnCall "map" [FnCall fnName substParams, idenExpr]]
else FnCall fnName (substParams ++ [idenExpr])
where
fnName = "freeVariables" ++ idenSort
idenExpr = VarExpr iden
substParams = [ListExpr []]
-- | Returns whether the given constructor has a binder
isBind :: ConstructorDef -> Bool
isBind MkBindConstructor{} = True
......@@ -231,12 +271,22 @@ substFunctionsC (nsd, sd, _, _) =
fnName = sortNameForIden iden ctor ++ sortOfCtxNamespace ++ "Substitute"
idenExpr = if null binder
then VarExpr iden
else FnCall
(sortNameForIden iden ctor ++ "VarReplace")
[VarExpr "b", head binder, VarExpr iden]
else varReplaceCall iden
substParams = [VarExpr "orig", VarExpr "sub"]
sortNameOfIden = sortNameForIden iden ctor
varReplaceCall :: IdenName -> Expression
varReplaceCall iden
= if iden `elem` map fst folds
then FnCall "fmap" [FnCall fnName substParams, idenExpr]
else if iden `elem` map fst lists
then FnCall "map" [FnCall fnName substParams, idenExpr]
else FnCall fnName (substParams ++ [idenExpr])
where
fnName = (sortNameForIden iden ctor ++ "VarReplace")
idenExpr = VarExpr iden
substParams = [VarExpr "b", head binder]
sortHasCtxForSort :: SortName -> SortName -> Bool
sortHasCtxForSort sortName ctxSort
= let ctxs = [INH x y | INH x y <- fromJust (lookup sortName ctxsBySname)]
......
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