Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Implemented more sophisticated skolem parsing a la the spec.

  • Loading branch information...
commit 811727c05d577fff82b5bb2c65ffb6c4613d60c8 1 parent fe18c4b
@luqui authored
Showing with 14 additions and 7 deletions.
  1. +4 −6 Sequent/Parser.hs
  2. +10 −1 Sequent/Syntax.hs
View
10 Sequent/Parser.hs
@@ -58,10 +58,8 @@ expr :: Parser Expr
expr = atomExpr
atomExpr :: Parser Expr
-atomExpr = convert <$> P.identifier lex <*> P.optionMaybe argList
+atomExpr = convert <$> P.identifier lex <*> P.many skolemGroup
where
- argList = (\es v n -> SkolemExpr n es v)
- <$> P.parens lex (expr `P.sepBy` P.symbol lex ",")
- <*> (P.symbol lex "." *> atomExpr)
- convert n Nothing = VarExpr n
- convert n (Just f) = f n
+ skolemGroup = (,) <$> P.parens lex (expr `P.sepBy` P.symbol lex ",") <*> P.optionMaybe (P.symbol lex "." *> P.identifier lex)
+ convert v [] = VarExpr v
+ convert v ((es, newvar):sks) = SkolemExpr v es (convert (maybe v id newvar) sks)
View
11 Sequent/Syntax.hs
@@ -40,7 +40,16 @@ showAtom (AClause c) = "(" ++ showClause c ++ ")"
showExpr :: Expr -> String
showExpr (VarExpr n) = n
-showExpr (SkolemExpr l es v) = l ++ "(" ++ intercalate "," (map showExpr es) ++ ")." ++ showExpr v
+showExpr sk@(SkolemExpr l es v) = l ++ showSkolem l sk
+ where
+ showSkolem cx (VarExpr n)
+ | n == cx = ""
+ | otherwise = "." ++ n
+ showSkolem cx (SkolemExpr l es v)
+ | l == cx = args ++ showSkolem cx v
+ | otherwise = "." ++ l ++ args ++ showSkolem l v
+ where
+ args = "(" ++ intercalate "," (map showExpr es) ++ ")"
showRel :: RelName -> [String] -> String
showRel = \name args -> "[" ++ intercalate " " (atoms name args) ++ "]"
Please sign in to comment.
Something went wrong with that request. Please try again.