Permalink
Browse files

Revert "Changed proposition syntax to the one I discussed in the jour…

…nal."

This reverts commit f375de5.
  • Loading branch information...
1 parent 71f710f commit 7192c7f44b3a9a6c2624d7807dc5a83fc4a45dfa @luqui committed Mar 7, 2012
Showing with 34 additions and 11 deletions.
  1. +11 −1 Sequent/Parser.hs
  2. +16 −3 Sequent/Syntax.hs
  3. +7 −7 examples/union/union.seq
View
@@ -29,7 +29,17 @@ clauseElem = idful <|> ((Right . (Nothing,)) <$> clauseAtom)
clauseAtom :: Parser ClauseAtom
clauseAtom = P.choice [ rel, cls ]
where
- rel = AProp <$> P.brackets lex expr
+ rel = convert <$> P.brackets lex (P.many relAtom)
+ where
+ relAtom = P.choice [
+ Left <$> P.identifier lex,
+ Right <$> (P.symbol lex "'" *> expr)
+ ]
+ convert xs = ARel (map toName xs) (concatMap toArg xs)
+ toName (Left i) = Just i
+ toName (Right j) = Nothing
+ toArg (Left i) = []
+ toArg (Right j) = [j]
cls = AClause <$> P.parens lex clause
group :: Parser Group
View
@@ -11,10 +11,12 @@ type Name = String
type Label = String
data ClauseAtom
- = AProp Expr
+ = ARel RelName [Expr]
| AClause Clause
deriving Eq
+type RelName = [Maybe String]
+
data Group = Group {
groupVars :: [Name],
groupHyps :: [(Label, ClauseAtom)]
@@ -39,7 +41,16 @@ instance Show Expr where
render1 = PP.renderStyle (PP.style { PP.mode=PP.OneLineMode })
showAtom :: ClauseAtom -> PP.Doc
-showAtom (AProp p) = PP.brackets (showExpr p)
+showAtom (ARel n xs) = showRel n (map showExpr xs)
+ where
+ showRel :: RelName -> [PP.Doc] -> PP.Doc
+ showRel name args = PP.brackets (PP.hsep (atoms name args))
+
+ atoms (Just s:ss) as = PP.text s : atoms ss as
+ atoms (Nothing:ss) (a:as) = (PP.text "'" PP.<> a) : atoms ss as
+ atoms (Nothing:ss) [] = error "Too few arguments to relation"
+ atoms [] (a:as) = error "Too many arguments to relation"
+ atoms [] [] = []
showAtom (AClause c) = PP.parens (showClause c)
showExpr :: Expr -> PP.Doc
@@ -114,7 +125,9 @@ labelFree g l = isNothing (groupFindH g l)
subst :: Name -> Expr -> ClauseAtom -> ClauseAtom
subst n e = go
where
- go (AProp p) = AProp (substExpr n e p)
+ go (ARel n' es)
+ -- substitute n'? Higher order...
+ = ARel n' (map (substExpr n e) es)
go (AClause (hyp :- con)) =
AClause (groupSubst n e hyp :- groupSubst n e con)
-- XXX if n is bound in hyp, our substitutions are overzealous
View
@@ -1,10 +1,10 @@
union: (X Y -> union
- (x [in(x,X)] -> [in(x,union)])
- (y [in(y,Y)] -> [in(y,union)])
- (Z (x [in(x,X)] -> [in(x,Z)])
- (y [in(y,Y)] -> [in(y,Z)])
- z [in(z,union)] -> [in(z,Z)]))
+ (x ['x in 'X] -> ['x in 'union])
+ (y ['y in 'Y] -> ['y in 'union])
+ (Z (x ['x in 'X] -> ['x in 'Z])
+ (y ['y in 'Y] -> ['y in 'Z])
+ z ['z in 'union] -> ['z in 'Z]))
nat real x
-[in(x, union(nat,real))]
+['x in 'union(nat,real)]
->
-[in(x, union(real,nat))]
+['x in 'union(real,nat)]

0 comments on commit 7192c7f

Please sign in to comment.