Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Changed proposition syntax to the one I discussed in the journal.

  • Loading branch information...
commit f375de5a96ae5b5dd51f413de5100a692d7d0f71 1 parent 4b046d3
@luqui authored
Showing with 11 additions and 34 deletions.
  1. +1 −11 Sequent/Parser.hs
  2. +3 −16 Sequent/Syntax.hs
  3. +7 −7 examples/union/union.seq
View
12 Sequent/Parser.hs
@@ -29,17 +29,7 @@ clauseElem = idful <|> ((Right . (Nothing,)) <$> clauseAtom)
clauseAtom :: Parser ClauseAtom
clauseAtom = P.choice [ rel, cls ]
where
- 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]
+ rel = AProp <$> P.brackets lex expr
cls = AClause <$> P.parens lex clause
group :: Parser Group
View
19 Sequent/Syntax.hs
@@ -11,12 +11,10 @@ type Name = String
type Label = String
data ClauseAtom
- = ARel RelName [Expr]
+ = AProp Expr
| AClause Clause
deriving Eq
-type RelName = [Maybe String]
-
data Group = Group {
groupVars :: [Name],
groupHyps :: [(Label, ClauseAtom)]
@@ -41,16 +39,7 @@ instance Show Expr where
render1 = PP.renderStyle (PP.style { PP.mode=PP.OneLineMode })
showAtom :: ClauseAtom -> PP.Doc
-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 (AProp p) = PP.brackets (showExpr p)
showAtom (AClause c) = PP.parens (showClause c)
showExpr :: Expr -> PP.Doc
@@ -125,9 +114,7 @@ labelFree g l = isNothing (groupFindH g l)
subst :: Name -> Expr -> ClauseAtom -> ClauseAtom
subst n e = go
where
- go (ARel n' es)
- -- substitute n'? Higher order...
- = ARel n' (map (substExpr n e) es)
+ go (AProp p) = AProp (substExpr n e p)
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
14 examples/union/union.seq
@@ -1,10 +1,10 @@
union: (X Y -> union
- (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]))
+ (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)]))
nat real x
-['x in 'union(nat,real)]
+[in(x, union(nat,real))]
->
-['x in 'union(real,nat)]
+[in(x, union(real,nat))]
Please sign in to comment.
Something went wrong with that request. Please try again.